%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM410+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:42:50 PM UTC 2026
% Result : Theorem 0.13s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM410+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n006.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 02:27:12 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 0.13/0.39 % Refutation found
% 0.13/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.39 fof(f8,axiom,(
% 0.13/0.39 (! [A] :( ( relation(A)& function(A) )=> ( transfinite_sequence(A)<=> ordinal(relation_dom(A)) ) ) )),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f9,axiom,(
% 0.13/0.39 (! [A,B] :( ( relation(B)& function(B)& transfinite_sequence(B) )=> ( transfinite_sequence_of(B,A)<=> subset(relation_rng(B),A) ) ) )),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f36,axiom,(
% 0.13/0.39 (! [A,B] : subset(A,A) )),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f40,conjecture,(
% 0.13/0.39 (! [A] :( ( relation(A)& function(A) )=> ( ordinal(relation_dom(A))=> transfinite_sequence_of(A,relation_rng(A)) ) ) )),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f41,negated_conjecture,(
% 0.13/0.39 ~((! [A] :( ( relation(A)& function(A) )=> ( ordinal(relation_dom(A))=> transfinite_sequence_of(A,relation_rng(A)) ) ) ))),
% 0.13/0.39 inference(negated_conjecture,[status(cth)],[f40])).
% 0.13/0.39 fof(f66,plain,(
% 0.13/0.39 ![A]: ((~relation(A)|~function(A))|(transfinite_sequence(A)<=>ordinal(relation_dom(A))))),
% 0.13/0.39 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.13/0.39 fof(f67,plain,(
% 0.13/0.39 ![A]: ((~relation(A)|~function(A))|((~transfinite_sequence(A)|ordinal(relation_dom(A)))&(transfinite_sequence(A)|~ordinal(relation_dom(A)))))),
% 0.13/0.39 inference(NNF_transformation,[status(thm)],[f66])).
% 0.13/0.39 fof(f69,plain,(
% 0.13/0.39 ![X0]: (~relation(X0)|~function(X0)|transfinite_sequence(X0)|~ordinal(relation_dom(X0)))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f67])).
% 0.13/0.39 fof(f70,plain,(
% 0.13/0.39 ![A,B]: (((~relation(B)|~function(B))|~transfinite_sequence(B))|(transfinite_sequence_of(B,A)<=>subset(relation_rng(B),A)))),
% 0.13/0.39 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.13/0.39 fof(f71,plain,(
% 0.13/0.39 ![A,B]: (((~relation(B)|~function(B))|~transfinite_sequence(B))|((~transfinite_sequence_of(B,A)|subset(relation_rng(B),A))&(transfinite_sequence_of(B,A)|~subset(relation_rng(B),A))))),
% 0.13/0.39 inference(NNF_transformation,[status(thm)],[f70])).
% 0.13/0.39 fof(f72,plain,(
% 0.13/0.39 ![B]: (((~relation(B)|~function(B))|~transfinite_sequence(B))|((![A]: (~transfinite_sequence_of(B,A)|subset(relation_rng(B),A)))&(![A]: (transfinite_sequence_of(B,A)|~subset(relation_rng(B),A)))))),
% 0.13/0.39 inference(miniscoping,[status(thm)],[f71])).
% 0.13/0.39 fof(f74,plain,(
% 0.13/0.39 ![X0,X1]: (~relation(X0)|~function(X0)|~transfinite_sequence(X0)|transfinite_sequence_of(X0,X1)|~subset(relation_rng(X0),X1))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f72])).
% 0.13/0.39 fof(f163,plain,(
% 0.13/0.39 ![A]: subset(A,A)),
% 0.13/0.39 inference(miniscoping,[status(thm)],[f36])).
% 0.13/0.39 fof(f164,plain,(
% 0.13/0.39 ![X0]: (subset(X0,X0))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f163])).
% 0.13/0.39 fof(f173,plain,(
% 0.13/0.39 (?[A]: ((relation(A)&function(A))&(ordinal(relation_dom(A))&~transfinite_sequence_of(A,relation_rng(A)))))),
% 0.13/0.39 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 0.13/0.39 fof(f174,plain,(
% 0.13/0.39 ((relation(sK16_skl)&function(sK16_skl))&(ordinal(relation_dom(sK16_skl))&~transfinite_sequence_of(sK16_skl,relation_rng(sK16_skl))))),
% 0.13/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl]),skolemize(A,sK16_skl)],[f173])).
% 0.13/0.39 fof(f175,plain,(
% 0.13/0.39 relation(sK16_skl)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f174])).
% 0.13/0.39 fof(f176,plain,(
% 0.13/0.39 function(sK16_skl)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f174])).
% 0.13/0.39 fof(f177,plain,(
% 0.13/0.39 ordinal(relation_dom(sK16_skl))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f174])).
% 0.13/0.39 fof(f178,plain,(
% 0.13/0.39 ~transfinite_sequence_of(sK16_skl,relation_rng(sK16_skl))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f174])).
% 0.13/0.39 fof(f224,plain,(
% 0.13/0.39 ~relation(sK16_skl)|~function(sK16_skl)|transfinite_sequence(sK16_skl)),
% 0.13/0.39 inference(resolution,[status(thm)],[f69,f177])).
% 0.13/0.39 fof(f226,plain,(
% 0.13/0.39 ~function(sK16_skl)|transfinite_sequence(sK16_skl)),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f224,f175])).
% 0.13/0.39 fof(f279,plain,(
% 0.13/0.39 transfinite_sequence(sK16_skl)),
% 0.13/0.39 inference(resolution,[status(thm)],[f226,f176])).
% 0.13/0.39 fof(f290,plain,(
% 0.13/0.39 ![X0]: (~relation(sK16_skl)|~function(sK16_skl)|transfinite_sequence_of(sK16_skl,X0)|~subset(relation_rng(sK16_skl),X0))),
% 0.13/0.39 inference(resolution,[status(thm)],[f74,f279])).
% 0.13/0.39 fof(f291,plain,(
% 0.13/0.39 ![X0]: (~function(sK16_skl)|transfinite_sequence_of(sK16_skl,X0)|~subset(relation_rng(sK16_skl),X0))),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f290,f175])).
% 0.13/0.39 fof(f295,plain,(
% 0.13/0.39 ![X0]: (transfinite_sequence_of(sK16_skl,X0)|~subset(relation_rng(sK16_skl),X0))),
% 0.13/0.39 inference(resolution,[status(thm)],[f291,f176])).
% 0.13/0.39 fof(f369,plain,(
% 0.13/0.39 transfinite_sequence_of(sK16_skl,relation_rng(sK16_skl))),
% 0.13/0.39 inference(resolution,[status(thm)],[f164,f295])).
% 0.13/0.39 fof(f370,plain,(
% 0.13/0.39 $false),
% 0.13/0.39 inference(forward_subsumption_resolution,[status(thm)],[f369,f178])).
% 0.13/0.39 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.41 % Elapsed time: 0.051987 seconds
% 0.13/0.41 % CPU time: 0.148163 seconds
% 0.13/0.41 % Total memory used: 83.029 MB
% 0.13/0.41 % Net memory used: 83.000 MB
%------------------------------------------------------------------------------