%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU258+1 : 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 : n011.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:09 PM UTC 2026
% Result : Theorem 246.09s 31.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU258+1 : 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.09/0.37 % Computer : n011.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 06:04:10 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 246.09/31.79 % Refutation found
% 246.09/31.79 % SZS status Theorem for theBenchmark: Theorem is valid
% 246.09/31.79 % SZS output start CNFRefutation for theBenchmark
% 246.09/31.79 fof(f7,axiom,(
% 246.09/31.79 (! [A,B] :( A = B<=> ( subset(A,B)& subset(B,A) ) ) )),
% 246.09/31.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 246.09/31.79 fof(f8,axiom,(
% 246.09/31.79 (! [A,B] :( subset(A,B)<=> (! [C] :( in(C,A)=> in(C,B) ) )) )),
% 246.09/31.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 246.09/31.79 fof(f9,axiom,(
% 246.09/31.79 (! [A] :( relation(A)=> ( well_ordering(A)<=> ( reflexive(A)& transitive(A)& antisymmetric(A)& connected(A)& well_founded_relation(A) ) ) ) )),
% 246.09/31.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 246.09/31.79 fof(f19,axiom,(
% 246.09/31.79 (! [A,B] :( relation(A)=> relation(relation_restriction(A,B)) ) )),
% 246.09/31.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 246.09/31.79 fof(f33,axiom,(
% 246.09/31.79 (! [A] :( relation(A)=> ( reflexive(A)<=> (! [B] :( in(B,relation_field(A))=> in(ordered_pair(B,B),A) ) )) ) )),
% 246.09/31.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 246.09/31.79 fof(f40,axiom,(
% 246.09/31.79 (! [A,B,C,D] :( in(ordered_pair(A,B),cartesian_product2(C,D))<=> ( in(A,C)& in(B,D) ) ) )),
% 246.09/31.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 246.09/31.79 fof(f41,axiom,(
% 246.09/31.79 (! [A,B,C] :( relation(C)=> ( in(A,relation_restriction(C,B))<=> ( in(A,C)& in(A,cartesian_product2(B,B)) ) ) ) )),
% 246.09/31.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 246.09/31.79 fof(f44,axiom,(
% 246.09/31.79 (! [A,B] :( relation(B)=> ( subset(relation_field(relation_restriction(B,A)),relation_field(B))& subset(relation_field(relation_restriction(B,A)),A) ) ) )),
% 246.09/31.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 246.09/31.79 fof(f47,axiom,(
% 246.09/31.79 (! [A,B,C] :( relation(C)=> ( in(ordered_pair(A,B),C)=> ( in(A,relation_field(C))& in(B,relation_field(C)) ) ) ) )),
% 246.09/31.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 246.09/31.79 fof(f48,conjecture,(
% 246.09/31.79 (! [A,B] :( relation(B)=> ( ( well_ordering(B)& subset(A,relation_field(B)) )=> relation_field(relation_restriction(B,A)) = A ) ) )),
% 246.09/31.79 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 246.09/31.79 fof(f49,negated_conjecture,(
% 246.09/31.79 ~((! [A,B] :( relation(B)=> ( ( well_ordering(B)& subset(A,relation_field(B)) )=> relation_field(relation_restriction(B,A)) = A ) ) ))),
% 246.09/31.79 inference(negated_conjecture,[status(cth)],[f48])).
% 246.09/31.79 fof(f67,plain,(
% 246.09/31.79 ![A,B]: ((~A=B|(subset(A,B)&subset(B,A)))&(A=B|(~subset(A,B)|~subset(B,A))))),
% 246.09/31.79 inference(NNF_transformation,[status(thm)],[f7])).
% 246.09/31.79 fof(f68,plain,(
% 246.09/31.79 (![A,B]: (~A=B|(subset(A,B)&subset(B,A))))&(![A,B]: (A=B|(~subset(A,B)|~subset(B,A))))),
% 246.09/31.79 inference(miniscoping,[status(thm)],[f67])).
% 246.09/31.79 fof(f71,plain,(
% 246.09/31.79 ![X0,X1]: (X0=X1|~subset(X0,X1)|~subset(X1,X0))),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f68])).
% 246.09/31.79 fof(f72,plain,(
% 246.09/31.79 ![A,B]: (subset(A,B)<=>(![C]: (~in(C,A)|in(C,B))))),
% 246.09/31.79 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 246.09/31.79 fof(f73,plain,(
% 246.09/31.79 ![A,B]: ((~subset(A,B)|(![C]: (~in(C,A)|in(C,B))))&(subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 246.09/31.79 inference(NNF_transformation,[status(thm)],[f72])).
% 246.09/31.79 fof(f74,plain,(
% 246.09/31.79 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(?[C]: (in(C,A)&~in(C,B)))))),
% 246.09/31.79 inference(miniscoping,[status(thm)],[f73])).
% 246.09/31.79 fof(f75,plain,(
% 246.09/31.79 (![A,B]: (~subset(A,B)|(![C]: (~in(C,A)|in(C,B)))))&(![A,B]: (subset(A,B)|(in(sK0_skl(B,A),A)&~in(sK0_skl(B,A),B))))),
% 246.09/31.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(C,sK0_skl(B,A))],[f74])).
% 246.09/31.79 fof(f76,plain,(
% 246.09/31.79 ![X0,X1,X2]: (~subset(X0,X1)|~in(X2,X0)|in(X2,X1))),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f75])).
% 246.09/31.79 fof(f77,plain,(
% 246.09/31.79 ![X0,X1]: (subset(X0,X1)|in(sK0_skl(X1,X0),X0))),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f75])).
% 246.09/31.79 fof(f78,plain,(
% 246.09/31.79 ![X0,X1]: (subset(X0,X1)|~in(sK0_skl(X1,X0),X1))),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f75])).
% 246.09/31.79 fof(f79,plain,(
% 246.09/31.79 ![A]: (~relation(A)|(well_ordering(A)<=>((((reflexive(A)&transitive(A))&antisymmetric(A))&connected(A))&well_founded_relation(A))))),
% 246.09/31.79 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 246.09/31.79 fof(f80,plain,(
% 246.09/31.79 ![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)))))),
% 246.09/31.79 inference(NNF_transformation,[status(thm)],[f79])).
% 246.09/31.79 fof(f81,plain,(
% 246.09/31.79 ![X0]: (~relation(X0)|~well_ordering(X0)|reflexive(X0))),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f80])).
% 246.09/31.79 fof(f92,plain,(
% 246.09/31.79 ![A,B]: (~relation(A)|relation(relation_restriction(A,B)))),
% 246.09/31.79 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 246.09/31.79 fof(f93,plain,(
% 246.09/31.79 ![A]: (~relation(A)|(![B]: relation(relation_restriction(A,B))))),
% 246.09/31.79 inference(miniscoping,[status(thm)],[f92])).
% 246.09/31.79 fof(f94,plain,(
% 246.09/31.79 ![X0,X1]: (~relation(X0)|relation(relation_restriction(X0,X1)))),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f93])).
% 246.09/31.79 fof(f109,plain,(
% 246.09/31.79 ![A]: (~relation(A)|(reflexive(A)<=>(![B]: (~in(B,relation_field(A))|in(ordered_pair(B,B),A)))))),
% 246.09/31.79 inference(pre_NNF_transformation,[status(thm)],[f33])).
% 246.09/31.79 fof(f110,plain,(
% 246.09/31.79 ![A]: (~relation(A)|((~reflexive(A)|(![B]: (~in(B,relation_field(A))|in(ordered_pair(B,B),A))))&(reflexive(A)|(?[B]: (in(B,relation_field(A))&~in(ordered_pair(B,B),A))))))),
% 246.09/31.79 inference(NNF_transformation,[status(thm)],[f109])).
% 246.09/31.79 fof(f111,plain,(
% 246.09/31.79 ![A]: (~relation(A)|((~reflexive(A)|(![B]: (~in(B,relation_field(A))|in(ordered_pair(B,B),A))))&(reflexive(A)|(in(sK2_skl(A),relation_field(A))&~in(ordered_pair(sK2_skl(A),sK2_skl(A)),A)))))),
% 246.09/31.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(B,sK2_skl(A))],[f110])).
% 246.09/31.79 fof(f112,plain,(
% 246.09/31.79 ![X0,X1]: (~relation(X0)|~reflexive(X0)|~in(X1,relation_field(X0))|in(ordered_pair(X1,X1),X0))),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f111])).
% 246.09/31.79 fof(f132,plain,(
% 246.09/31.79 ![A,B,C,D]: ((~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D)))&(in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 246.09/31.79 inference(NNF_transformation,[status(thm)],[f40])).
% 246.09/31.79 fof(f133,plain,(
% 246.09/31.79 (![A,B,C,D]: (~in(ordered_pair(A,B),cartesian_product2(C,D))|(in(A,C)&in(B,D))))&(![A,B,C,D]: (in(ordered_pair(A,B),cartesian_product2(C,D))|(~in(A,C)|~in(B,D))))),
% 246.09/31.79 inference(miniscoping,[status(thm)],[f132])).
% 246.09/31.79 fof(f136,plain,(
% 246.09/31.79 ![X0,X1,X2,X3]: (in(ordered_pair(X0,X1),cartesian_product2(X2,X3))|~in(X0,X2)|~in(X1,X3))),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f133])).
% 246.09/31.79 fof(f137,plain,(
% 246.09/31.79 ![A,B,C]: (~relation(C)|(in(A,relation_restriction(C,B))<=>(in(A,C)&in(A,cartesian_product2(B,B)))))),
% 246.09/31.79 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 246.09/31.79 fof(f138,plain,(
% 246.09/31.79 ![A,B,C]: (~relation(C)|((~in(A,relation_restriction(C,B))|(in(A,C)&in(A,cartesian_product2(B,B))))&(in(A,relation_restriction(C,B))|(~in(A,C)|~in(A,cartesian_product2(B,B))))))),
% 246.09/31.79 inference(NNF_transformation,[status(thm)],[f137])).
% 246.09/31.79 fof(f139,plain,(
% 246.09/31.79 ![C]: (~relation(C)|((![A,B]: (~in(A,relation_restriction(C,B))|(in(A,C)&in(A,cartesian_product2(B,B)))))&(![A,B]: (in(A,relation_restriction(C,B))|(~in(A,C)|~in(A,cartesian_product2(B,B)))))))),
% 246.09/31.79 inference(miniscoping,[status(thm)],[f138])).
% 246.09/31.79 fof(f142,plain,(
% 246.09/31.79 ![X0,X1,X2]: (~relation(X0)|in(X1,relation_restriction(X0,X2))|~in(X1,X0)|~in(X1,cartesian_product2(X2,X2)))),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f139])).
% 246.09/31.79 fof(f146,plain,(
% 246.09/31.79 ![A,B]: (~relation(B)|(subset(relation_field(relation_restriction(B,A)),relation_field(B))&subset(relation_field(relation_restriction(B,A)),A)))),
% 246.09/31.79 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 246.09/31.79 fof(f147,plain,(
% 246.09/31.79 ![B]: (~relation(B)|((![A]: subset(relation_field(relation_restriction(B,A)),relation_field(B)))&(![A]: subset(relation_field(relation_restriction(B,A)),A))))),
% 246.09/31.79 inference(miniscoping,[status(thm)],[f146])).
% 246.09/31.79 fof(f149,plain,(
% 246.09/31.79 ![X0,X1]: (~relation(X0)|subset(relation_field(relation_restriction(X0,X1)),X1))),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f147])).
% 246.09/31.79 fof(f153,plain,(
% 246.09/31.79 ![A,B,C]: (~relation(C)|(~in(ordered_pair(A,B),C)|(in(A,relation_field(C))&in(B,relation_field(C)))))),
% 246.09/31.79 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 246.09/31.79 fof(f154,plain,(
% 246.09/31.79 ![C]: (~relation(C)|(![A,B]: (~in(ordered_pair(A,B),C)|(in(A,relation_field(C))&in(B,relation_field(C))))))),
% 246.09/31.79 inference(miniscoping,[status(thm)],[f153])).
% 246.09/31.79 fof(f156,plain,(
% 246.09/31.79 ![X0,X1,X2]: (~relation(X0)|~in(ordered_pair(X1,X2),X0)|in(X2,relation_field(X0)))),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f154])).
% 246.09/31.79 fof(f157,plain,(
% 246.09/31.79 (?[A,B]: (relation(B)&((well_ordering(B)&subset(A,relation_field(B)))&~relation_field(relation_restriction(B,A))=A)))),
% 246.09/31.79 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 246.09/31.79 fof(f158,plain,(
% 246.09/31.79 ?[B]: (relation(B)&(?[A]: ((well_ordering(B)&subset(A,relation_field(B)))&~relation_field(relation_restriction(B,A))=A)))),
% 246.09/31.79 inference(miniscoping,[status(thm)],[f157])).
% 246.09/31.79 fof(f159,plain,(
% 246.09/31.79 (relation(sK8_skl)&((well_ordering(sK8_skl)&subset(sK9_skl,relation_field(sK8_skl)))&~relation_field(relation_restriction(sK8_skl,sK9_skl))=sK9_skl))),
% 246.09/31.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl]),skolemize(B,sK8_skl),skolemize(A,sK9_skl)],[f158])).
% 246.09/31.79 fof(f160,plain,(
% 246.09/31.79 relation(sK8_skl)),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f159])).
% 246.09/31.79 fof(f161,plain,(
% 246.09/31.79 well_ordering(sK8_skl)),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f159])).
% 246.09/31.79 fof(f162,plain,(
% 246.09/31.79 subset(sK9_skl,relation_field(sK8_skl))),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f159])).
% 246.09/31.79 fof(f163,plain,(
% 246.09/31.79 ~relation_field(relation_restriction(sK8_skl,sK9_skl))=sK9_skl),
% 246.09/31.79 inference(cnf_transformation,[status(thm)],[f159])).
% 246.09/31.79 fof(f184,plain,(
% 246.09/31.79 ![X0]: (relation(relation_restriction(sK8_skl,X0)))),
% 246.09/31.79 inference(resolution,[status(thm)],[f94,f160])).
% 246.09/31.79 fof(f189,plain,(
% 246.09/31.79 ![X0]: (~in(X0,sK9_skl)|in(X0,relation_field(sK8_skl)))),
% 246.09/31.79 inference(resolution,[status(thm)],[f76,f162])).
% 246.09/31.79 fof(f193,plain,(
% 246.09/31.79 ![X0]: (subset(relation_field(relation_restriction(sK8_skl,X0)),X0))),
% 246.09/31.79 inference(resolution,[status(thm)],[f149,f160])).
% 246.09/31.79 fof(f250,plain,(
% 246.09/31.79 ![X0]: (X0=relation_field(relation_restriction(sK8_skl,X0))|~subset(X0,relation_field(relation_restriction(sK8_skl,X0))))),
% 246.09/31.79 inference(resolution,[status(thm)],[f193,f71])).
% 246.09/31.79 fof(f251,plain,(
% 246.09/31.79 ![X0]: (in(sK0_skl(X0,sK9_skl),relation_field(sK8_skl))|subset(sK9_skl,X0))),
% 246.09/31.79 inference(resolution,[status(thm)],[f189,f77])).
% 246.09/31.79 fof(f1508,plain,(
% 246.09/31.79 ~relation(sK8_skl)|reflexive(sK8_skl)),
% 246.09/31.79 inference(resolution,[status(thm)],[f81,f161])).
% 246.09/31.79 fof(f1509,plain,(
% 246.09/31.79 reflexive(sK8_skl)),
% 246.09/31.79 inference(forward_subsumption_resolution,[status(thm)],[f1508,f160])).
% 246.09/31.79 fof(f3038,plain,(
% 246.09/31.79 ![X0]: (~relation(sK8_skl)|~reflexive(sK8_skl)|in(ordered_pair(sK0_skl(X0,sK9_skl),sK0_skl(X0,sK9_skl)),sK8_skl)|subset(sK9_skl,X0))),
% 246.09/31.79 inference(resolution,[status(thm)],[f112,f251])).
% 246.09/31.79 fof(f3054,plain,(
% 246.09/31.79 ![X0]: (~reflexive(sK8_skl)|in(ordered_pair(sK0_skl(X0,sK9_skl),sK0_skl(X0,sK9_skl)),sK8_skl)|subset(sK9_skl,X0))),
% 246.09/31.79 inference(forward_subsumption_resolution,[status(thm)],[f3038,f160])).
% 246.09/31.79 fof(f3091,plain,(
% 246.09/31.79 ![X0]: (in(ordered_pair(sK0_skl(X0,sK9_skl),sK0_skl(X0,sK9_skl)),sK8_skl)|subset(sK9_skl,X0))),
% 246.09/31.79 inference(forward_subsumption_resolution,[status(thm)],[f3054,f1509])).
% 246.09/31.79 fof(f4723,plain,(
% 246.09/31.79 ![X0,X1,X2,X3]: (in(ordered_pair(X0,sK0_skl(X1,X2)),cartesian_product2(X3,X2))|~in(X0,X3)|subset(X2,X1))),
% 246.09/31.79 inference(resolution,[status(thm)],[f136,f77])).
% 246.09/31.79 fof(f10040,plain,(
% 246.09/31.79 ![X0,X1,X2,X3]: (in(ordered_pair(sK0_skl(X0,X1),sK0_skl(X2,X3)),cartesian_product2(X1,X3))|subset(X3,X2)|subset(X1,X0))),
% 246.09/31.79 inference(resolution,[status(thm)],[f4723,f77])).
% 246.09/31.79 fof(f12826,plain,(
% 246.09/31.79 ![X0,X1,X2,X3]: (~relation(X0)|in(ordered_pair(sK0_skl(X1,X2),sK0_skl(X3,X2)),relation_restriction(X0,X2))|~in(ordered_pair(sK0_skl(X1,X2),sK0_skl(X3,X2)),X0)|subset(X2,X3)|subset(X2,X1))),
% 246.09/31.79 inference(resolution,[status(thm)],[f142,f10040])).
% 246.09/31.79 fof(f33607,plain,(
% 246.09/31.79 ![X0]: (~relation(sK8_skl)|in(ordered_pair(sK0_skl(X0,sK9_skl),sK0_skl(X0,sK9_skl)),relation_restriction(sK8_skl,sK9_skl))|subset(sK9_skl,X0)|subset(sK9_skl,X0)|subset(sK9_skl,X0))),
% 246.09/31.79 inference(resolution,[status(thm)],[f12826,f3091])).
% 246.09/31.79 fof(f33631,plain,(
% 246.09/31.79 ![X0]: (~relation(sK8_skl)|in(ordered_pair(sK0_skl(X0,sK9_skl),sK0_skl(X0,sK9_skl)),relation_restriction(sK8_skl,sK9_skl))|subset(sK9_skl,X0))),
% 246.09/31.79 inference(duplicate_literals_removal,[status(thm)],[f33607])).
% 246.09/31.79 fof(f33632,plain,(
% 246.09/31.79 ![X0]: (in(ordered_pair(sK0_skl(X0,sK9_skl),sK0_skl(X0,sK9_skl)),relation_restriction(sK8_skl,sK9_skl))|subset(sK9_skl,X0))),
% 12.59/32.07 inference(forward_subsumption_resolution,[status(thm)],[f33631,f160])).
% 12.59/32.07 fof(f34611,plain,(
% 12.59/32.07 ![X0]: (subset(sK9_skl,X0)|~relation(relation_restriction(sK8_skl,sK9_skl))|in(sK0_skl(X0,sK9_skl),relation_field(relation_restriction(sK8_skl,sK9_skl))))),
% 12.59/32.07 inference(resolution,[status(thm)],[f33632,f156])).
% 12.59/32.07 fof(f34649,plain,(
% 12.59/32.07 ![X0]: (subset(sK9_skl,X0)|in(sK0_skl(X0,sK9_skl),relation_field(relation_restriction(sK8_skl,sK9_skl))))),
% 12.59/32.07 inference(forward_subsumption_resolution,[status(thm)],[f34611,f184])).
% 12.59/32.07 fof(f34653,plain,(
% 12.59/32.07 subset(sK9_skl,relation_field(relation_restriction(sK8_skl,sK9_skl)))|subset(sK9_skl,relation_field(relation_restriction(sK8_skl,sK9_skl)))),
% 12.59/32.07 inference(resolution,[status(thm)],[f34649,f78])).
% 12.59/32.07 fof(f34688,plain,(
% 12.59/32.07 subset(sK9_skl,relation_field(relation_restriction(sK8_skl,sK9_skl)))),
% 12.59/32.07 inference(duplicate_literals_removal,[status(thm)],[f34653])).
% 12.59/32.07 fof(f39592,plain,(
% 12.59/32.07 sK9_skl=relation_field(relation_restriction(sK8_skl,sK9_skl))),
% 12.59/32.07 inference(resolution,[status(thm)],[f34688,f250])).
% 12.59/32.07 fof(f39596,plain,(
% 12.59/32.07 $false),
% 12.59/32.07 inference(forward_subsumption_resolution,[status(thm)],[f39592,f163])).
% 12.59/32.07 % SZS output end CNFRefutation for theBenchmark.p
% 12.59/32.07 % Elapsed time: 31.666583 seconds
% 12.59/32.07 % CPU time: 249.203592 seconds
% 12.59/32.07 % Total memory used: 1.235 GB
% 12.59/32.07 % Net memory used: 1.158 GB
%------------------------------------------------------------------------------