%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU261+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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 02:22:10 PM UTC 2026
% Result : Theorem 60.84s 8.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU261+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n003.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 06:06:30 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.40 % Drodi V4.1.1
% 60.84/8.14 % Refutation found
% 60.84/8.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 60.84/8.14 % SZS output start CNFRefutation for theBenchmark
% 60.84/8.14 fof(f31,axiom,(
% 60.84/8.14 (! [A] :( A = empty_set<=> (! [B] : ~ in(B,A) )) )),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f51,axiom,(
% 60.84/8.14 (! [A] :( relation(A)=> ( well_ordering(A)<=> ( reflexive(A)& transitive(A)& antisymmetric(A)& connected(A)& well_founded_relation(A) ) ) ) )),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f93,axiom,(
% 60.84/8.14 (! [A] :( relation(A)=> relation(relation_inverse(A)) ) )),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f108,axiom,(
% 60.84/8.14 (! [A] :( empty(A)=> ( empty(relation_inverse(A))& relation(relation_inverse(A)) ) ) )),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f109,axiom,(
% 60.84/8.14 ( empty(empty_set)& relation(empty_set)& relation_empty_yielding(empty_set) ) ),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f144,lemma,(
% 60.84/8.14 (! [A] : singleton(A) != empty_set )),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f163,axiom,(
% 60.84/8.14 (? [A] :( empty(A)& relation(A) ) )),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f166,axiom,(
% 60.84/8.14 (? [A] :( relation(A)& empty(A)& function(A) ) )),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f171,axiom,(
% 60.84/8.14 (? [A] :( relation(A)& function(A)& one_to_one(A) ) )),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f173,axiom,(
% 60.84/8.14 (? [A] :( relation(A)& relation_empty_yielding(A) ) )),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f280,lemma,(
% 60.84/8.14 (! [A] :( relation(A)=> (! [B] :( relation(B)=> (! [C] :( ( relation(C)& function(C) )=> ( relation_isomorphism(A,B,C)=> ( ( reflexive(A)=> reflexive(B) )& ( transitive(A)=> transitive(B) )& ( connected(A)=> connected(B) )& ( antisymmetric(A)=> antisymmetric(B) )& ( well_founded_relation(A)=> well_founded_relation(B) ) ) ) ) )) )) )),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f283,conjecture,(
% 60.84/8.14 (! [A] :( relation(A)=> (! [B] :( relation(B)=> (! [C] :( ( relation(C)& function(C) )=> ( ( well_ordering(A)& relation_isomorphism(A,B,C) )=> well_ordering(B) ) ) )) )) )),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f284,negated_conjecture,(
% 60.84/8.14 ~((! [A] :( relation(A)=> (! [B] :( relation(B)=> (! [C] :( ( relation(C)& function(C) )=> ( ( well_ordering(A)& relation_isomorphism(A,B,C) )=> well_ordering(B) ) ) )) )) ))),
% 60.84/8.14 inference(negated_conjecture,[status(cth)],[f283])).
% 60.84/8.14 fof(f299,axiom,(
% 60.84/8.14 (! [A] :( empty(A)=> A = empty_set ) )),
% 60.84/8.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 60.84/8.14 fof(f490,plain,(
% 60.84/8.14 ![A]: ((~A=empty_set|(![B]: ~in(B,A)))&(A=empty_set|(?[B]: in(B,A))))),
% 60.84/8.14 inference(NNF_transformation,[status(thm)],[f31])).
% 60.84/8.14 fof(f491,plain,(
% 60.84/8.14 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|(?[B]: in(B,A))))),
% 60.84/8.14 inference(miniscoping,[status(thm)],[f490])).
% 60.84/8.14 fof(f492,plain,(
% 60.84/8.14 (![A]: (~A=empty_set|(![B]: ~in(B,A))))&(![A]: (A=empty_set|in(sK26_skl(A),A)))),
% 60.84/8.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(B,sK26_skl(A))],[f491])).
% 60.84/8.14 fof(f493,plain,(
% 60.84/8.14 ![X0,X1]: (~X0=empty_set|~in(X1,X0))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f492])).
% 60.84/8.14 fof(f640,plain,(
% 60.84/8.14 ![A]: (~relation(A)|(well_ordering(A)<=>((((reflexive(A)&transitive(A))&antisymmetric(A))&connected(A))&well_founded_relation(A))))),
% 60.84/8.14 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 60.84/8.14 fof(f641,plain,(
% 60.84/8.14 ![A]: (~relation(A)|((~well_ordering(A)|((((reflexive(A)&transitive(A))&antisymmetric(A))&connected(A))&well_founded_relation(A)))&(well_ordering(A)|((((~reflexive(A)|~transitive(A))|~antisymmetric(A))|~connected(A))|~well_founded_relation(A)))))),
% 60.84/8.14 inference(NNF_transformation,[status(thm)],[f640])).
% 60.84/8.14 fof(f642,plain,(
% 60.84/8.14 ![X0]: (~relation(X0)|~well_ordering(X0)|reflexive(X0))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f641])).
% 60.84/8.14 fof(f643,plain,(
% 60.84/8.14 ![X0]: (~relation(X0)|~well_ordering(X0)|transitive(X0))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f641])).
% 60.84/8.14 fof(f644,plain,(
% 60.84/8.14 ![X0]: (~relation(X0)|~well_ordering(X0)|antisymmetric(X0))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f641])).
% 60.84/8.14 fof(f645,plain,(
% 60.84/8.14 ![X0]: (~relation(X0)|~well_ordering(X0)|connected(X0))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f641])).
% 60.84/8.14 fof(f646,plain,(
% 60.84/8.14 ![X0]: (~relation(X0)|~well_ordering(X0)|well_founded_relation(X0))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f641])).
% 60.84/8.14 fof(f647,plain,(
% 60.84/8.14 ![X0]: (~relation(X0)|well_ordering(X0)|~reflexive(X0)|~transitive(X0)|~antisymmetric(X0)|~connected(X0)|~well_founded_relation(X0))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f641])).
% 60.84/8.14 fof(f787,plain,(
% 60.84/8.14 ![A]: (~relation(A)|relation(relation_inverse(A)))),
% 60.84/8.14 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 60.84/8.14 fof(f788,plain,(
% 60.84/8.14 ![X0]: (~relation(X0)|relation(relation_inverse(X0)))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f787])).
% 60.84/8.14 fof(f811,plain,(
% 60.84/8.14 ![A]: (~empty(A)|(empty(relation_inverse(A))&relation(relation_inverse(A))))),
% 60.84/8.14 inference(pre_NNF_transformation,[status(thm)],[f108])).
% 60.84/8.14 fof(f812,plain,(
% 60.84/8.14 ![X0]: (~empty(X0)|empty(relation_inverse(X0)))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f811])).
% 60.84/8.14 fof(f814,plain,(
% 60.84/8.14 empty(empty_set)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f109])).
% 60.84/8.14 fof(f908,plain,(
% 60.84/8.14 ![X0]: (~singleton(X0)=empty_set)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f144])).
% 60.84/8.14 fof(f984,plain,(
% 60.84/8.14 (empty(sK91_skl)&relation(sK91_skl))),
% 60.84/8.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK91_skl]),skolemize(A,sK91_skl)],[f163])).
% 60.84/8.14 fof(f985,plain,(
% 60.84/8.14 empty(sK91_skl)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f984])).
% 60.84/8.14 fof(f993,plain,(
% 60.84/8.14 ((relation(sK94_skl)&empty(sK94_skl))&function(sK94_skl))),
% 60.84/8.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK94_skl]),skolemize(A,sK94_skl)],[f166])).
% 60.84/8.14 fof(f995,plain,(
% 60.84/8.14 empty(sK94_skl)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f993])).
% 60.84/8.14 fof(f1013,plain,(
% 60.84/8.14 ((relation(sK99_skl)&function(sK99_skl))&one_to_one(sK99_skl))),
% 60.84/8.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK99_skl]),skolemize(A,sK99_skl)],[f171])).
% 60.84/8.14 fof(f1016,plain,(
% 60.84/8.14 one_to_one(sK99_skl)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1013])).
% 60.84/8.14 fof(f1022,plain,(
% 60.84/8.14 (relation(sK101_skl)&relation_empty_yielding(sK101_skl))),
% 60.84/8.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK101_skl]),skolemize(A,sK101_skl)],[f173])).
% 60.84/8.14 fof(f1023,plain,(
% 60.84/8.14 relation(sK101_skl)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1022])).
% 60.84/8.14 fof(f1353,plain,(
% 60.84/8.14 ![A]: (~relation(A)|(![B]: (~relation(B)|(![C]: ((~relation(C)|~function(C))|(~relation_isomorphism(A,B,C)|(((((~reflexive(A)|reflexive(B))&(~transitive(A)|transitive(B)))&(~connected(A)|connected(B)))&(~antisymmetric(A)|antisymmetric(B)))&(~well_founded_relation(A)|well_founded_relation(B)))))))))),
% 60.84/8.14 inference(pre_NNF_transformation,[status(thm)],[f280])).
% 60.84/8.14 fof(f1354,plain,(
% 60.84/8.14 ![X0,X1,X2]: (~relation(X0)|~relation(X1)|~relation(X2)|~function(X2)|~relation_isomorphism(X0,X1,X2)|~reflexive(X0)|reflexive(X1))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1353])).
% 60.84/8.14 fof(f1355,plain,(
% 60.84/8.14 ![X0,X1,X2]: (~relation(X0)|~relation(X1)|~relation(X2)|~function(X2)|~relation_isomorphism(X0,X1,X2)|~transitive(X0)|transitive(X1))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1353])).
% 60.84/8.14 fof(f1356,plain,(
% 60.84/8.14 ![X0,X1,X2]: (~relation(X0)|~relation(X1)|~relation(X2)|~function(X2)|~relation_isomorphism(X0,X1,X2)|~connected(X0)|connected(X1))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1353])).
% 60.84/8.14 fof(f1357,plain,(
% 60.84/8.14 ![X0,X1,X2]: (~relation(X0)|~relation(X1)|~relation(X2)|~function(X2)|~relation_isomorphism(X0,X1,X2)|~antisymmetric(X0)|antisymmetric(X1))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1353])).
% 60.84/8.14 fof(f1358,plain,(
% 60.84/8.14 ![X0,X1,X2]: (~relation(X0)|~relation(X1)|~relation(X2)|~function(X2)|~relation_isomorphism(X0,X1,X2)|~well_founded_relation(X0)|well_founded_relation(X1))),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1353])).
% 60.84/8.14 fof(f1375,plain,(
% 60.84/8.14 (?[A]: (relation(A)&(?[B]: (relation(B)&(?[C]: ((relation(C)&function(C))&((well_ordering(A)&relation_isomorphism(A,B,C))&~well_ordering(B))))))))),
% 60.84/8.14 inference(pre_NNF_transformation,[status(thm)],[f284])).
% 60.84/8.14 fof(f1376,plain,(
% 60.84/8.14 (relation(sK118_skl)&(relation(sK119_skl)&((relation(sK120_skl)&function(sK120_skl))&((well_ordering(sK118_skl)&relation_isomorphism(sK118_skl,sK119_skl,sK120_skl))&~well_ordering(sK119_skl)))))),
% 60.84/8.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK118_skl,sK119_skl,sK120_skl]),skolemize(A,sK118_skl),skolemize(B,sK119_skl),skolemize(C,sK120_skl)],[f1375])).
% 60.84/8.14 fof(f1377,plain,(
% 60.84/8.14 relation(sK118_skl)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1376])).
% 60.84/8.14 fof(f1378,plain,(
% 60.84/8.14 relation(sK119_skl)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1376])).
% 60.84/8.14 fof(f1379,plain,(
% 60.84/8.14 relation(sK120_skl)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1376])).
% 60.84/8.14 fof(f1380,plain,(
% 60.84/8.14 function(sK120_skl)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1376])).
% 60.84/8.14 fof(f1381,plain,(
% 60.84/8.14 well_ordering(sK118_skl)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1376])).
% 60.84/8.14 fof(f1382,plain,(
% 60.84/8.14 relation_isomorphism(sK118_skl,sK119_skl,sK120_skl)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1376])).
% 60.84/8.14 fof(f1383,plain,(
% 60.84/8.14 ~well_ordering(sK119_skl)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1376])).
% 60.84/8.14 fof(f1430,plain,(
% 60.84/8.14 ![A]: (~empty(A)|A=empty_set)),
% 60.84/8.14 inference(pre_NNF_transformation,[status(thm)],[f299])).
% 60.84/8.14 fof(f1431,plain,(
% 60.84/8.14 ![X0]: (~empty(X0)|X0=empty_set)),
% 60.84/8.14 inference(cnf_transformation,[status(thm)],[f1430])).
% 60.84/8.14 fof(f1584,plain,(
% 60.84/8.14 ![X0]: (~in(X0,empty_set))),
% 60.84/8.14 inference(destructive_equality_resolution,[status(thm)],[f493])).
% 60.84/8.14 fof(f1646,plain,(
% 60.84/8.14 ~relation(sK118_skl)|well_founded_relation(sK118_skl)),
% 60.84/8.14 inference(resolution,[status(thm)],[f1381,f646])).
% 60.84/8.14 fof(f1647,plain,(
% 60.84/8.14 ~relation(sK118_skl)|connected(sK118_skl)),
% 60.84/8.14 inference(resolution,[status(thm)],[f1381,f645])).
% 60.84/8.14 fof(f1648,definition,(
% 60.84/8.14 sQ2_spl <=> (relation(sK118_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f1650,plain,(
% 60.84/8.14 ~relation(sK118_skl)|sQ2_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f1648])).
% 60.84/8.14 fof(f1651,definition,(
% 60.84/8.14 sQ3_spl <=> (well_founded_relation(sK118_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f1654,plain,(
% 60.84/8.14 ~sQ2_spl|sQ3_spl),
% 60.84/8.14 inference(split_clause,[status(thm)],[f1646,f1648,f1651])).
% 60.84/8.14 fof(f1655,definition,(
% 60.84/8.14 sQ4_spl <=> (connected(sK118_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f1658,plain,(
% 60.84/8.14 ~sQ2_spl|sQ4_spl),
% 60.84/8.14 inference(split_clause,[status(thm)],[f1647,f1648,f1655])).
% 60.84/8.14 fof(f1659,plain,(
% 60.84/8.14 $false|sQ2_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f1650,f1377])).
% 60.84/8.14 fof(f1660,plain,(
% 60.84/8.14 sQ2_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f1659])).
% 60.84/8.14 fof(f1662,definition,(
% 60.84/8.14 sQ5_spl <=> (relation(sK119_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f1664,plain,(
% 60.84/8.14 ~relation(sK119_skl)|sQ5_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f1662])).
% 60.84/8.14 fof(f1665,definition,(
% 60.84/8.14 sQ6_spl <=> (relation(sK120_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f1667,plain,(
% 60.84/8.14 ~relation(sK120_skl)|sQ6_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f1665])).
% 60.84/8.14 fof(f1668,definition,(
% 60.84/8.14 sQ7_spl <=> (function(sK120_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f1670,plain,(
% 60.84/8.14 ~function(sK120_skl)|sQ7_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f1668])).
% 60.84/8.14 fof(f1680,plain,(
% 60.84/8.14 $false|sQ7_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f1670,f1380])).
% 60.84/8.14 fof(f1681,plain,(
% 60.84/8.14 sQ7_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f1680])).
% 60.84/8.14 fof(f1682,plain,(
% 60.84/8.14 $false|sQ6_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f1667,f1379])).
% 60.84/8.14 fof(f1683,plain,(
% 60.84/8.14 sQ6_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f1682])).
% 60.84/8.14 fof(f1684,plain,(
% 60.84/8.14 $false|sQ5_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f1664,f1378])).
% 60.84/8.14 fof(f1685,plain,(
% 60.84/8.14 sQ5_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f1684])).
% 60.84/8.14 fof(f2274,definition,(
% 60.84/8.14 sQ88_spl <=> (one_to_one(sK99_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f2276,plain,(
% 60.84/8.14 ~one_to_one(sK99_skl)|sQ88_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f2274])).
% 60.84/8.14 fof(f2287,definition,(
% 60.84/8.14 sQ91_spl <=> (antisymmetric(sK118_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f3142,definition,(
% 60.84/8.14 sQ202_spl <=> (transitive(sK118_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ202_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f3934,definition,(
% 60.84/8.14 sQ317_spl <=> (sK94_skl=empty_set)),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ317_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f3936,plain,(
% 60.84/8.14 ~sK94_skl=empty_set|sQ317_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f3934])).
% 60.84/8.14 fof(f4019,definition,(
% 60.84/8.14 sQ339_spl <=> (sK91_skl=empty_set)),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ339_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f4021,plain,(
% 60.84/8.14 ~sK91_skl=empty_set|sQ339_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f4019])).
% 60.84/8.14 fof(f5613,definition,(
% 60.84/8.14 sQ452_spl <=> (well_founded_relation(sK119_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ452_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f8335,plain,(
% 60.84/8.14 ~relation(sK118_skl)|antisymmetric(sK118_skl)),
% 60.84/8.14 inference(resolution,[status(thm)],[f1381,f644])).
% 60.84/8.14 fof(f8336,plain,(
% 60.84/8.14 ~relation(sK118_skl)|transitive(sK118_skl)),
% 60.84/8.14 inference(resolution,[status(thm)],[f1381,f643])).
% 60.84/8.14 fof(f8337,plain,(
% 60.84/8.14 ~relation(sK118_skl)|reflexive(sK118_skl)),
% 60.84/8.14 inference(resolution,[status(thm)],[f1381,f642])).
% 60.84/8.14 fof(f8343,plain,(
% 60.84/8.14 ~sQ2_spl|sQ91_spl),
% 60.84/8.14 inference(split_clause,[status(thm)],[f8335,f1648,f2287])).
% 60.84/8.14 fof(f8344,plain,(
% 60.84/8.14 ~sQ2_spl|sQ202_spl),
% 60.84/8.14 inference(split_clause,[status(thm)],[f8336,f1648,f3142])).
% 60.84/8.14 fof(f8345,definition,(
% 60.84/8.14 sQ624_spl <=> (reflexive(sK118_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ624_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f8348,plain,(
% 60.84/8.14 ~sQ2_spl|sQ624_spl),
% 60.84/8.14 inference(split_clause,[status(thm)],[f8337,f1648,f8345])).
% 60.84/8.14 fof(f10195,definition,(
% 60.84/8.14 sQ749_spl <=> (relation(relation_inverse(sK119_skl)))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ749_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f10197,plain,(
% 60.84/8.14 ~relation(relation_inverse(sK119_skl))|sQ749_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f10195])).
% 60.84/8.14 fof(f10202,definition,(
% 60.84/8.14 sQ751_spl <=> (relation(relation_inverse(sK120_skl)))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ751_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f10204,plain,(
% 60.84/8.14 ~relation(relation_inverse(sK120_skl))|sQ751_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f10202])).
% 60.84/8.14 fof(f11871,plain,(
% 60.84/8.14 relation(relation_inverse(sK119_skl))),
% 60.84/8.14 inference(resolution,[status(thm)],[f788,f1378])).
% 60.84/8.14 fof(f11872,plain,(
% 60.84/8.14 relation(relation_inverse(sK101_skl))),
% 60.84/8.14 inference(resolution,[status(thm)],[f788,f1023])).
% 60.84/8.14 fof(f11873,plain,(
% 60.84/8.14 relation(relation_inverse(sK120_skl))),
% 60.84/8.14 inference(resolution,[status(thm)],[f788,f1379])).
% 60.84/8.14 fof(f11877,plain,(
% 60.84/8.14 relation(relation_inverse(sK118_skl))),
% 60.84/8.14 inference(resolution,[status(thm)],[f788,f1377])).
% 60.84/8.14 fof(f12473,plain,(
% 60.84/8.14 empty(relation_inverse(empty_set))),
% 60.84/8.14 inference(resolution,[status(thm)],[f812,f814])).
% 60.84/8.14 fof(f14364,definition,(
% 60.84/8.14 sQ1019_spl <=> (well_ordering(sK119_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ1019_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f14365,plain,(
% 60.84/8.14 well_ordering(sK119_skl)|~sQ1019_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f14364])).
% 60.84/8.14 fof(f14553,definition,(
% 60.84/8.14 sQ1036_spl <=> (reflexive(sK119_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ1036_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f14554,plain,(
% 60.84/8.14 reflexive(sK119_skl)|~sQ1036_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f14553])).
% 60.84/8.14 fof(f14608,plain,(
% 60.84/8.14 ~relation(sK119_skl)|well_ordering(sK119_skl)|~transitive(sK119_skl)|~antisymmetric(sK119_skl)|~connected(sK119_skl)|~well_founded_relation(sK119_skl)|~sQ1036_spl),
% 60.84/8.14 inference(resolution,[status(thm)],[f14554,f647])).
% 60.84/8.14 fof(f14613,definition,(
% 60.84/8.14 sQ1052_spl <=> (transitive(sK119_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ1052_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f14616,definition,(
% 60.84/8.14 sQ1053_spl <=> (antisymmetric(sK119_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ1053_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f14619,definition,(
% 60.84/8.14 sQ1054_spl <=> (connected(sK119_skl))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ1054_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f14622,plain,(
% 60.84/8.14 ~sQ5_spl|sQ1019_spl|~sQ1052_spl|~sQ1053_spl|~sQ1054_spl|~sQ452_spl|~sQ1036_spl),
% 60.84/8.14 inference(split_clause,[status(thm)],[f14608,f1662,f14364,f14613,f14616,f14619,f5613,f14553])).
% 60.84/8.14 fof(f14623,plain,(
% 60.84/8.14 $false|~sQ1019_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f14365,f1383])).
% 60.84/8.14 fof(f14624,plain,(
% 60.84/8.14 ~sQ1019_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f14623])).
% 60.84/8.14 fof(f15146,definition,(
% 60.84/8.14 sQ1104_spl <=> (in(ordered_pair(sK81_skl(empty_set),sK83_skl(empty_set)),empty_set))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ1104_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f15147,plain,(
% 60.84/8.14 in(ordered_pair(sK81_skl(empty_set),sK83_skl(empty_set)),empty_set)|~sQ1104_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f15146])).
% 60.84/8.14 fof(f15178,plain,(
% 60.84/8.14 $false|~sQ1104_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f15147,f1584])).
% 60.84/8.14 fof(f15179,plain,(
% 60.84/8.14 ~sQ1104_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f15178])).
% 60.84/8.14 fof(f15376,definition,(
% 60.84/8.14 sQ1126_spl <=> (in(ordered_pair(sK83_skl(empty_set),sK82_skl(empty_set)),empty_set))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ1126_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f15377,plain,(
% 60.84/8.14 in(ordered_pair(sK83_skl(empty_set),sK82_skl(empty_set)),empty_set)|~sQ1126_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f15376])).
% 60.84/8.14 fof(f15408,plain,(
% 60.84/8.14 $false|~sQ1126_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f15377,f1584])).
% 60.84/8.14 fof(f15409,plain,(
% 60.84/8.14 ~sQ1126_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f15408])).
% 60.84/8.14 fof(f15678,definition,(
% 60.84/8.14 sQ1161_spl <=> (in(ordered_pair(sK84_skl(empty_set),sK85_skl(empty_set)),empty_set))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ1161_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f15679,plain,(
% 60.84/8.14 in(ordered_pair(sK84_skl(empty_set),sK85_skl(empty_set)),empty_set)|~sQ1161_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f15678])).
% 60.84/8.14 fof(f15710,plain,(
% 60.84/8.14 $false|~sQ1161_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f15679,f1584])).
% 60.84/8.14 fof(f15711,plain,(
% 60.84/8.14 ~sQ1161_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f15710])).
% 60.84/8.14 fof(f15854,definition,(
% 60.84/8.14 sQ1189_spl <=> (in(ordered_pair(sK85_skl(empty_set),sK84_skl(empty_set)),empty_set))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ1189_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f15855,plain,(
% 60.84/8.14 in(ordered_pair(sK85_skl(empty_set),sK84_skl(empty_set)),empty_set)|~sQ1189_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f15854])).
% 60.84/8.14 fof(f15886,plain,(
% 60.84/8.14 $false|~sQ1189_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f15855,f1584])).
% 60.84/8.14 fof(f15887,plain,(
% 60.84/8.14 ~sQ1189_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f15886])).
% 60.84/8.14 fof(f16716,definition,(
% 60.84/8.14 ![X0]: (sQ1275_spl <=> (empty_set=singleton(X0)))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ1275_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f16717,plain,(
% 60.84/8.14 ![X0]: (empty_set=singleton(X0)|~sQ1275_spl)),
% 60.84/8.14 inference(component_clause,[status(thm)],[f16716])).
% 60.84/8.14 fof(f16720,plain,(
% 60.84/8.14 $false|~sQ1275_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f16717,f908])).
% 60.84/8.14 fof(f16721,plain,(
% 60.84/8.14 ~sQ1275_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f16720])).
% 60.84/8.14 fof(f17952,plain,(
% 60.84/8.14 $false|sQ749_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f11871,f10197])).
% 60.84/8.14 fof(f17953,plain,(
% 60.84/8.14 sQ749_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f17952])).
% 60.84/8.14 fof(f18090,plain,(
% 60.84/8.14 $false|sQ751_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f11873,f10204])).
% 60.84/8.14 fof(f18091,plain,(
% 60.84/8.14 sQ751_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f18090])).
% 60.84/8.14 fof(f18635,definition,(
% 60.84/8.14 sQ1554_spl <=> (in(ordered_pair(sK29_skl(empty_set,sK118_skl),sK30_skl(empty_set,sK118_skl)),empty_set))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ1554_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f18636,plain,(
% 60.84/8.14 in(ordered_pair(sK29_skl(empty_set,sK118_skl),sK30_skl(empty_set,sK118_skl)),empty_set)|~sQ1554_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f18635])).
% 60.84/8.14 fof(f18646,plain,(
% 60.84/8.14 $false|~sQ1554_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f18636,f1584])).
% 60.84/8.14 fof(f18647,plain,(
% 60.84/8.14 ~sQ1554_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f18646])).
% 60.84/8.14 fof(f21162,plain,(
% 60.84/8.14 sK94_skl=empty_set),
% 60.84/8.14 inference(resolution,[status(thm)],[f1431,f995])).
% 60.84/8.14 fof(f21163,plain,(
% 60.84/8.14 sK91_skl=empty_set),
% 60.84/8.14 inference(resolution,[status(thm)],[f1431,f985])).
% 60.84/8.14 fof(f21166,plain,(
% 60.84/8.14 $false|sQ317_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f21162,f3936])).
% 60.84/8.14 fof(f21167,plain,(
% 60.84/8.14 sQ317_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f21166])).
% 60.84/8.14 fof(f21168,plain,(
% 60.84/8.14 $false|sQ339_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f21163,f4021])).
% 60.84/8.14 fof(f21169,plain,(
% 60.84/8.14 sQ339_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f21168])).
% 60.84/8.14 fof(f22459,plain,(
% 60.84/8.14 $false|sQ88_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f2276,f1016])).
% 60.84/8.14 fof(f22460,plain,(
% 60.84/8.14 sQ88_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f22459])).
% 60.84/8.14 fof(f28898,definition,(
% 60.84/8.14 sQ2781_spl <=> (relation(relation_inverse(sK118_skl)))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ2781_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f28900,plain,(
% 60.84/8.14 ~relation(relation_inverse(sK118_skl))|sQ2781_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f28898])).
% 60.84/8.14 fof(f28909,plain,(
% 60.84/8.14 $false|sQ2781_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f28900,f11877])).
% 60.84/8.14 fof(f28910,plain,(
% 60.84/8.14 sQ2781_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f28909])).
% 60.84/8.14 fof(f32328,plain,(
% 60.84/8.14 empty(relation_inverse(sK91_skl))),
% 60.84/8.14 inference(forward_demodulation,[status(thm)],[f21163,f12473])).
% 60.84/8.14 fof(f32686,definition,(
% 60.84/8.14 sQ3262_spl <=> (empty(relation_inverse(sK91_skl)))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ3262_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f32688,plain,(
% 60.84/8.14 ~empty(relation_inverse(sK91_skl))|sQ3262_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f32686])).
% 60.84/8.14 fof(f32690,plain,(
% 60.84/8.14 $false|sQ3262_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f32688,f32328])).
% 60.84/8.14 fof(f32691,plain,(
% 60.84/8.14 sQ3262_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f32690])).
% 60.84/8.14 fof(f32808,definition,(
% 60.84/8.14 sQ3266_spl <=> (relation(relation_inverse(sK101_skl)))),
% 60.84/8.14 introduced(definition,[new_symbols(definition,[sQ3266_spl])],[split_symbol_definition])).
% 60.84/8.14 fof(f32810,plain,(
% 60.84/8.14 ~relation(relation_inverse(sK101_skl))|sQ3266_spl),
% 60.84/8.14 inference(component_clause,[status(thm)],[f32808])).
% 60.84/8.14 fof(f32819,plain,(
% 60.84/8.14 $false|sQ3266_spl),
% 60.84/8.14 inference(forward_subsumption_resolution,[status(thm)],[f32810,f11872])).
% 60.84/8.14 fof(f32820,plain,(
% 60.84/8.14 sQ3266_spl),
% 60.84/8.14 inference(contradiction_clause,[status(thm)],[f32819])).
% 60.84/8.14 fof(f32827,plain,(
% 60.84/8.14 ~relation(sK118_skl)|~relation(sK119_skl)|~relation(sK120_skl)|~function(sK120_skl)|~reflexive(sK118_skl)|reflexive(sK119_skl)),
% 60.84/8.14 inference(resolution,[status(thm)],[f1354,f1382])).
% 60.84/8.14 fof(f32828,plain,(
% 60.84/8.14 ~sQ2_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ624_spl|sQ1036_spl),
% 60.84/8.14 inference(split_clause,[status(thm)],[f32827,f1648,f1662,f1665,f1668,f8345,f14553])).
% 60.84/8.14 fof(f32829,plain,(
% 60.84/8.14 ~relation(sK118_skl)|~relation(sK119_skl)|~relation(sK120_skl)|~function(sK120_skl)|~transitive(sK118_skl)|transitive(sK119_skl)),
% 60.84/8.14 inference(resolution,[status(thm)],[f1355,f1382])).
% 60.84/8.14 fof(f32830,plain,(
% 60.84/8.14 ~sQ2_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ202_spl|sQ1052_spl),
% 60.84/8.14 inference(split_clause,[status(thm)],[f32829,f1648,f1662,f1665,f1668,f3142,f14613])).
% 60.84/8.14 fof(f32831,plain,(
% 60.84/8.14 ~relation(sK118_skl)|~relation(sK119_skl)|~relation(sK120_skl)|~function(sK120_skl)|~connected(sK118_skl)|connected(sK119_skl)),
% 60.84/8.14 inference(resolution,[status(thm)],[f1356,f1382])).
% 60.84/8.14 fof(f32832,plain,(
% 60.84/8.14 ~sQ2_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ4_spl|sQ1054_spl),
% 60.84/8.14 inference(split_clause,[status(thm)],[f32831,f1648,f1662,f1665,f1668,f1655,f14619])).
% 60.84/8.20 fof(f32854,plain,(
% 60.84/8.20 ~relation(sK118_skl)|~relation(sK119_skl)|~relation(sK120_skl)|~function(sK120_skl)|~antisymmetric(sK118_skl)|antisymmetric(sK119_skl)),
% 60.84/8.20 inference(resolution,[status(thm)],[f1357,f1382])).
% 60.84/8.20 fof(f32855,plain,(
% 60.84/8.20 ~sQ2_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ91_spl|sQ1053_spl),
% 60.84/8.20 inference(split_clause,[status(thm)],[f32854,f1648,f1662,f1665,f1668,f2287,f14616])).
% 60.84/8.20 fof(f32856,plain,(
% 60.84/8.20 ~relation(sK118_skl)|~relation(sK119_skl)|~relation(sK120_skl)|~function(sK120_skl)|~well_founded_relation(sK118_skl)|well_founded_relation(sK119_skl)),
% 60.84/8.20 inference(resolution,[status(thm)],[f1358,f1382])).
% 60.84/8.20 fof(f32857,plain,(
% 60.84/8.20 ~sQ2_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ3_spl|sQ452_spl),
% 60.84/8.20 inference(split_clause,[status(thm)],[f32856,f1648,f1662,f1665,f1668,f1651,f5613])).
% 60.84/8.20 fof(f32858,plain,(
% 60.84/8.20 $false),
% 60.84/8.20 inference(sat_refutation,[status(thm)],[f1654,f1658,f1660,f1681,f1683,f1685,f8343,f8344,f8348,f14622,f14624,f15179,f15409,f15711,f15887,f16721,f17953,f18091,f18647,f21167,f21169,f22460,f28910,f32691,f32820,f32828,f32830,f32832,f32855,f32857])).
% 60.84/8.20 % SZS output end CNFRefutation for theBenchmark.p
% 9.85/8.22 % Elapsed time: 7.833148 seconds
% 9.85/8.22 % CPU time: 61.641596 seconds
% 9.85/8.22 % Total memory used: 565.543 MB
% 9.85/8.22 % Net memory used: 522.205 MB
%------------------------------------------------------------------------------