%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SET957+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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:12:55 PM UTC 2026
% Result : Theorem 0.20s 0.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SET957+1 : TPTP v9.3.1. Bugfixed v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.62 % Computer : n014.cluster.edu
% 0.15/0.62 % Model : x86_64 x86_64
% 0.15/0.62 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.62 % Memory : 8046.5625MB
% 0.15/0.62 % OS : Linux 6.8.0-71-generic
% 0.15/0.62 % CPULimit : 300
% 0.15/0.62 % WCLimit : 300
% 0.15/0.62 % DateTime : Mon Sep 21 05:45:50 UTC 2026
% 0.15/0.63 % CPUTime :
% 0.15/0.64 % Drodi V4.1.1
% 0.20/0.71 % Refutation found
% 0.20/0.71 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.20/0.71 % SZS output start CNFRefutation for theBenchmark
% 0.20/0.71 fof(f1,axiom,(
% 0.20/0.71 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 0.20/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.71 fof(f8,axiom,(
% 0.20/0.71 (! [A,B,C,D] :~ ( subset(A,cartesian_product2(B,C))& in(D,A)& (! [E,F] :~ ( in(E,B)& in(F,C)& D = ordered_pair(E,F) ) )) )),
% 0.20/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.71 fof(f9,conjecture,(
% 0.20/0.71 (! [A,B,C,D,E,F] :( ( subset(A,cartesian_product2(B,C))& subset(D,cartesian_product2(E,F))& (! [G,H] :( in(ordered_pair(G,H),A)<=> in(ordered_pair(G,H),D) ) ))=> A = D ) )),
% 0.20/0.71 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.71 fof(f10,negated_conjecture,(
% 0.20/0.71 ~((! [A,B,C,D,E,F] :( ( subset(A,cartesian_product2(B,C))& subset(D,cartesian_product2(E,F))& (! [G,H] :( in(ordered_pair(G,H),A)<=> in(ordered_pair(G,H),D) ) ))=> A = D ) ))),
% 0.20/0.71 inference(negated_conjecture,[status(cth)],[f9])).
% 0.20/0.71 fof(f11,axiom,(
% 0.20/0.71 (! [A,B] :( (! [C] :( in(C,A)<=> in(C,B) ))=> A = B ) )),
% 0.20/0.72 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.20/0.72 fof(f12,plain,(
% 0.20/0.72 ![A,B]: (~in(A,B)|~in(B,A))),
% 0.20/0.72 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.20/0.72 fof(f13,plain,(
% 0.20/0.72 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 0.20/0.72 inference(cnf_transformation,[status(thm)],[f12])).
% 0.20/0.72 fof(f23,plain,(
% 0.20/0.72 ![A,B,C,D]: ((~subset(A,cartesian_product2(B,C))|~in(D,A))|(?[E,F]: ((in(E,B)&in(F,C))&D=ordered_pair(E,F))))),
% 0.20/0.72 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.20/0.72 fof(f24,plain,(
% 0.20/0.72 ![B,C,D]: ((![A]: (~subset(A,cartesian_product2(B,C))|~in(D,A)))|(?[E,F]: ((in(E,B)&in(F,C))&D=ordered_pair(E,F))))),
% 0.20/0.72 inference(miniscoping,[status(thm)],[f23])).
% 0.20/0.72 fof(f25,plain,(
% 0.20/0.72 ![B,C,D]: ((![A]: (~subset(A,cartesian_product2(B,C))|~in(D,A)))|((in(sK2_skl(D,C,B),B)&in(sK3_skl(D,C,B),C))&D=ordered_pair(sK2_skl(D,C,B),sK3_skl(D,C,B))))),
% 0.20/0.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(E,sK2_skl(D,C,B)),skolemize(F,sK3_skl(D,C,B))],[f24])).
% 0.20/0.72 fof(f28,plain,(
% 0.20/0.72 ![X0,X1,X2,X3]: (~subset(X0,cartesian_product2(X1,X2))|~in(X3,X0)|X3=ordered_pair(sK2_skl(X3,X2,X1),sK3_skl(X3,X2,X1)))),
% 0.20/0.72 inference(cnf_transformation,[status(thm)],[f25])).
% 0.20/0.72 fof(f29,plain,(
% 0.20/0.72 (?[A,B,C,D,E,F]: (((subset(A,cartesian_product2(B,C))&subset(D,cartesian_product2(E,F)))&(![G,H]: (in(ordered_pair(G,H),A)<=>in(ordered_pair(G,H),D))))&~A=D))),
% 0.20/0.72 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 0.20/0.72 fof(f30,plain,(
% 0.20/0.72 ?[A,B,C,D,E,F]: (((subset(A,cartesian_product2(B,C))&subset(D,cartesian_product2(E,F)))&(![G,H]: ((~in(ordered_pair(G,H),A)|in(ordered_pair(G,H),D))&(in(ordered_pair(G,H),A)|~in(ordered_pair(G,H),D)))))&~A=D)),
% 0.20/0.72 inference(NNF_transformation,[status(thm)],[f29])).
% 0.20/0.72 fof(f31,plain,(
% 0.20/0.72 ?[A,D]: ((((?[B,C]: subset(A,cartesian_product2(B,C)))&(?[E,F]: subset(D,cartesian_product2(E,F))))&((![G,H]: (~in(ordered_pair(G,H),A)|in(ordered_pair(G,H),D)))&(![G,H]: (in(ordered_pair(G,H),A)|~in(ordered_pair(G,H),D)))))&~A=D)),
% 0.20/0.72 inference(miniscoping,[status(thm)],[f30])).
% 0.20/0.72 fof(f32,plain,(
% 0.20/0.72 (((subset(sK4_skl,cartesian_product2(sK6_skl,sK7_skl))&subset(sK5_skl,cartesian_product2(sK8_skl,sK9_skl)))&((![G,H]: (~in(ordered_pair(G,H),sK4_skl)|in(ordered_pair(G,H),sK5_skl)))&(![G,H]: (in(ordered_pair(G,H),sK4_skl)|~in(ordered_pair(G,H),sK5_skl)))))&~sK4_skl=sK5_skl)),
% 0.20/0.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(A,sK4_skl),skolemize(D,sK5_skl),skolemize(B,sK6_skl),skolemize(C,sK7_skl),skolemize(E,sK8_skl),skolemize(F,sK9_skl)],[f31])).
% 0.20/0.72 fof(f33,plain,(
% 0.20/0.72 subset(sK4_skl,cartesian_product2(sK6_skl,sK7_skl))),
% 0.20/0.72 inference(cnf_transformation,[status(thm)],[f32])).
% 0.20/0.72 fof(f34,plain,(
% 0.20/0.72 subset(sK5_skl,cartesian_product2(sK8_skl,sK9_skl))),
% 0.20/0.72 inference(cnf_transformation,[status(thm)],[f32])).
% 0.20/0.72 fof(f35,plain,(
% 0.20/0.72 ![X0,X1]: (~in(ordered_pair(X0,X1),sK4_skl)|in(ordered_pair(X0,X1),sK5_skl))),
% 0.20/0.72 inference(cnf_transformation,[status(thm)],[f32])).
% 0.20/0.72 fof(f36,plain,(
% 0.20/0.72 ![X0,X1]: (in(ordered_pair(X0,X1),sK4_skl)|~in(ordered_pair(X0,X1),sK5_skl))),
% 0.20/0.72 inference(cnf_transformation,[status(thm)],[f32])).
% 0.20/0.72 fof(f37,plain,(
% 0.20/0.72 ~sK4_skl=sK5_skl),
% 0.20/0.72 inference(cnf_transformation,[status(thm)],[f32])).
% 0.20/0.72 fof(f38,plain,(
% 0.20/0.72 ![A,B]: ((?[C]: (in(C,A)<~>in(C,B)))|A=B)),
% 0.20/0.72 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.20/0.72 fof(f39,plain,(
% 0.20/0.72 ![A,B]: ((?[C]: ((in(C,A)|in(C,B))&(~in(C,A)|~in(C,B))))|A=B)),
% 0.20/0.72 inference(NNF_transformation,[status(thm)],[f38])).
% 0.20/0.72 fof(f40,plain,(
% 0.20/0.72 ![A,B]: (((in(sK10_skl(B,A),A)|in(sK10_skl(B,A),B))&(~in(sK10_skl(B,A),A)|~in(sK10_skl(B,A),B)))|A=B)),
% 0.20/0.72 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(C,sK10_skl(B,A))],[f39])).
% 0.20/0.72 fof(f41,plain,(
% 0.20/0.72 ![X0,X1]: (in(sK10_skl(X0,X1),X1)|in(sK10_skl(X0,X1),X0)|X1=X0)),
% 0.20/0.72 inference(cnf_transformation,[status(thm)],[f40])).
% 0.20/0.72 fof(f42,plain,(
% 0.20/0.72 ![X0,X1]: (~in(sK10_skl(X0,X1),X1)|~in(sK10_skl(X0,X1),X0)|X1=X0)),
% 0.20/0.72 inference(cnf_transformation,[status(thm)],[f40])).
% 0.20/0.72 fof(f43,plain,(
% 0.20/0.72 ![X0,X1]: (~in(sK5_skl,ordered_pair(X0,X1))|~in(ordered_pair(X0,X1),sK4_skl))),
% 0.20/0.72 inference(resolution,[status(thm)],[f13,f35])).
% 0.20/0.72 fof(f87,plain,(
% 0.20/0.72 ![X0]: (~in(X0,sK5_skl)|X0=ordered_pair(sK2_skl(X0,sK9_skl,sK8_skl),sK3_skl(X0,sK9_skl,sK8_skl)))),
% 0.20/0.72 inference(resolution,[status(thm)],[f28,f34])).
% 0.20/0.72 fof(f88,plain,(
% 0.20/0.72 ![X0]: (~in(X0,sK4_skl)|X0=ordered_pair(sK2_skl(X0,sK7_skl,sK6_skl),sK3_skl(X0,sK7_skl,sK6_skl)))),
% 0.20/0.72 inference(resolution,[status(thm)],[f28,f33])).
% 0.20/0.72 fof(f92,plain,(
% 0.20/0.72 ![X0,X1]: (ordered_pair(X0,X1)=ordered_pair(sK2_skl(ordered_pair(X0,X1),sK9_skl,sK8_skl),sK3_skl(ordered_pair(X0,X1),sK9_skl,sK8_skl))|~in(ordered_pair(X0,X1),sK4_skl))),
% 0.20/0.72 inference(resolution,[status(thm)],[f87,f35])).
% 0.20/0.72 fof(f112,plain,(
% 0.20/0.72 ![X0]: (in(sK10_skl(X0,sK4_skl),X0)|sK4_skl=X0|sK10_skl(X0,sK4_skl)=ordered_pair(sK2_skl(sK10_skl(X0,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(X0,sK4_skl),sK7_skl,sK6_skl)))),
% 0.20/0.72 inference(resolution,[status(thm)],[f41,f88])).
% 0.20/0.72 fof(f225,plain,(
% 0.20/0.72 sK4_skl=sK5_skl|sK10_skl(sK5_skl,sK4_skl)=ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl))|sK10_skl(sK5_skl,sK4_skl)=ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl))),
% 0.20/0.72 inference(resolution,[status(thm)],[f112,f87])).
% 0.20/0.72 fof(f232,definition,(
% 0.20/0.72 sQ5_spl <=> (sK4_skl=sK5_skl)),
% 0.20/0.72 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.20/0.72 fof(f233,plain,(
% 0.20/0.72 sK4_skl=sK5_skl|~sQ5_spl),
% 0.20/0.72 inference(component_clause,[status(thm)],[f232])).
% 0.20/0.72 fof(f235,definition,(
% 0.20/0.72 sQ6_spl <=> (sK10_skl(sK5_skl,sK4_skl)=ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl)))),
% 0.20/0.72 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.20/0.72 fof(f236,plain,(
% 0.20/0.72 sK10_skl(sK5_skl,sK4_skl)=ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl))|~sQ6_spl),
% 0.20/0.72 inference(component_clause,[status(thm)],[f235])).
% 0.20/0.72 fof(f238,definition,(
% 0.20/0.72 sQ7_spl <=> (sK10_skl(sK5_skl,sK4_skl)=ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl)))),
% 0.20/0.72 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.20/0.72 fof(f239,plain,(
% 0.20/0.72 sK10_skl(sK5_skl,sK4_skl)=ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl))|~sQ7_spl),
% 0.20/0.72 inference(component_clause,[status(thm)],[f238])).
% 0.20/0.72 fof(f241,plain,(
% 0.20/0.72 sQ5_spl|sQ6_spl|sQ7_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f225,f232,f235,f238])).
% 0.20/0.72 fof(f263,plain,(
% 0.20/0.72 $false|~sQ5_spl),
% 0.20/0.72 inference(forward_subsumption_resolution,[status(thm)],[f233,f37])).
% 0.20/0.72 fof(f264,plain,(
% 0.20/0.72 ~sQ5_spl),
% 0.20/0.72 inference(contradiction_clause,[status(thm)],[f263])).
% 0.20/0.72 fof(f269,plain,(
% 0.20/0.72 ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl))=ordered_pair(sK2_skl(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl)),sK9_skl,sK8_skl),sK3_skl(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl)),sK9_skl,sK8_skl))|~in(sK10_skl(sK5_skl,sK4_skl),sK4_skl)|~sQ6_spl),
% 0.20/0.72 inference(paramodulation,[status(thm)],[f236,f92])).
% 0.20/0.72 fof(f271,plain,(
% 0.20/0.72 ~in(sK5_skl,sK10_skl(sK5_skl,sK4_skl))|~in(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl)),sK4_skl)|~sQ6_spl),
% 0.20/0.72 inference(paramodulation,[status(thm)],[f236,f43])).
% 0.20/0.72 fof(f272,plain,(
% 0.20/0.72 in(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl)),sK4_skl)|~in(sK10_skl(sK5_skl,sK4_skl),sK5_skl)|~sQ6_spl),
% 0.20/0.72 inference(paramodulation,[status(thm)],[f236,f36])).
% 0.20/0.72 fof(f273,plain,(
% 0.20/0.72 ~in(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl)),sK4_skl)|in(sK10_skl(sK5_skl,sK4_skl),sK5_skl)|~sQ6_spl),
% 0.20/0.72 inference(paramodulation,[status(thm)],[f236,f35])).
% 0.20/0.72 fof(f274,definition,(
% 0.20/0.72 sQ11_spl <=> (ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl))=ordered_pair(sK2_skl(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl)),sK9_skl,sK8_skl),sK3_skl(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl)),sK9_skl,sK8_skl)))),
% 0.20/0.72 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.20/0.72 fof(f277,definition,(
% 0.20/0.72 sQ12_spl <=> (in(sK10_skl(sK5_skl,sK4_skl),sK4_skl))),
% 0.20/0.72 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.20/0.72 fof(f279,plain,(
% 0.20/0.72 ~in(sK10_skl(sK5_skl,sK4_skl),sK4_skl)|sQ12_spl),
% 0.20/0.72 inference(component_clause,[status(thm)],[f277])).
% 0.20/0.72 fof(f280,plain,(
% 0.20/0.72 sQ11_spl|~sQ12_spl|~sQ6_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f269,f274,f277,f235])).
% 0.20/0.72 fof(f281,definition,(
% 0.20/0.72 sQ13_spl <=> (in(sK5_skl,sK10_skl(sK5_skl,sK4_skl)))),
% 0.20/0.72 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.20/0.72 fof(f284,definition,(
% 0.20/0.72 sQ14_spl <=> (in(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl)),sK4_skl))),
% 0.20/0.72 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.20/0.72 fof(f285,plain,(
% 0.20/0.72 in(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl)),sK4_skl)|~sQ14_spl),
% 0.20/0.72 inference(component_clause,[status(thm)],[f284])).
% 0.20/0.72 fof(f286,plain,(
% 0.20/0.72 ~in(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK7_skl,sK6_skl)),sK4_skl)|sQ14_spl),
% 0.20/0.72 inference(component_clause,[status(thm)],[f284])).
% 0.20/0.72 fof(f287,plain,(
% 0.20/0.72 ~sQ13_spl|~sQ14_spl|~sQ6_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f271,f281,f284,f235])).
% 0.20/0.72 fof(f288,definition,(
% 0.20/0.72 sQ15_spl <=> (in(sK10_skl(sK5_skl,sK4_skl),sK5_skl))),
% 0.20/0.72 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.20/0.72 fof(f291,plain,(
% 0.20/0.72 sQ14_spl|~sQ15_spl|~sQ6_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f272,f284,f288,f235])).
% 0.20/0.72 fof(f292,plain,(
% 0.20/0.72 ~sQ14_spl|sQ15_spl|~sQ6_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f273,f284,f288,f235])).
% 0.20/0.72 fof(f296,plain,(
% 0.20/0.72 in(sK10_skl(sK5_skl,sK4_skl),sK4_skl)|~sQ6_spl|~sQ14_spl),
% 0.20/0.72 inference(forward_demodulation,[status(thm)],[f236,f285])).
% 0.20/0.72 fof(f297,plain,(
% 0.20/0.72 ~in(sK10_skl(sK5_skl,sK4_skl),sK5_skl)|sK4_skl=sK5_skl|~sQ6_spl|~sQ14_spl),
% 0.20/0.72 inference(resolution,[status(thm)],[f296,f42])).
% 0.20/0.72 fof(f300,plain,(
% 0.20/0.72 ~sQ15_spl|sQ5_spl|~sQ6_spl|~sQ14_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f297,f288,f232,f235,f284])).
% 0.20/0.72 fof(f301,plain,(
% 0.20/0.72 ~in(sK10_skl(sK5_skl,sK4_skl),sK4_skl)|~sQ6_spl|sQ14_spl),
% 0.20/0.72 inference(forward_demodulation,[status(thm)],[f236,f286])).
% 0.20/0.72 fof(f302,plain,(
% 0.20/0.72 in(sK10_skl(sK5_skl,sK4_skl),sK5_skl)|sK4_skl=sK5_skl|~sQ6_spl|sQ14_spl),
% 0.20/0.72 inference(resolution,[status(thm)],[f301,f41])).
% 0.20/0.72 fof(f303,plain,(
% 0.20/0.72 sQ15_spl|sQ5_spl|~sQ6_spl|sQ14_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f302,f288,f232,f235,f284])).
% 0.20/0.72 fof(f380,plain,(
% 0.20/0.72 ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl))=ordered_pair(sK2_skl(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl)),sK9_skl,sK8_skl),sK3_skl(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl)),sK9_skl,sK8_skl))|~in(sK10_skl(sK5_skl,sK4_skl),sK4_skl)|~sQ7_spl),
% 0.20/0.72 inference(paramodulation,[status(thm)],[f239,f92])).
% 0.20/0.72 fof(f382,plain,(
% 0.20/0.72 ~in(sK5_skl,sK10_skl(sK5_skl,sK4_skl))|~in(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl)),sK4_skl)|~sQ7_spl),
% 0.20/0.72 inference(paramodulation,[status(thm)],[f239,f43])).
% 0.20/0.72 fof(f383,plain,(
% 0.20/0.72 in(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl)),sK4_skl)|~in(sK10_skl(sK5_skl,sK4_skl),sK5_skl)|~sQ7_spl),
% 0.20/0.72 inference(paramodulation,[status(thm)],[f239,f36])).
% 0.20/0.72 fof(f384,plain,(
% 0.20/0.72 ~in(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl)),sK4_skl)|in(sK10_skl(sK5_skl,sK4_skl),sK5_skl)|~sQ7_spl),
% 0.20/0.72 inference(paramodulation,[status(thm)],[f239,f35])).
% 0.20/0.72 fof(f385,definition,(
% 0.20/0.72 sQ21_spl <=> (ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl))=ordered_pair(sK2_skl(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl)),sK9_skl,sK8_skl),sK3_skl(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl)),sK9_skl,sK8_skl)))),
% 0.20/0.72 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.20/0.72 fof(f388,plain,(
% 0.20/0.72 sQ21_spl|~sQ12_spl|~sQ7_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f380,f385,f277,f238])).
% 0.20/0.72 fof(f389,definition,(
% 0.20/0.72 sQ22_spl <=> (in(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl)),sK4_skl))),
% 0.20/0.72 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.20/0.72 fof(f390,plain,(
% 0.20/0.72 in(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl)),sK4_skl)|~sQ22_spl),
% 0.20/0.72 inference(component_clause,[status(thm)],[f389])).
% 0.20/0.72 fof(f391,plain,(
% 0.20/0.72 ~in(ordered_pair(sK2_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl),sK3_skl(sK10_skl(sK5_skl,sK4_skl),sK9_skl,sK8_skl)),sK4_skl)|sQ22_spl),
% 0.20/0.72 inference(component_clause,[status(thm)],[f389])).
% 0.20/0.72 fof(f392,plain,(
% 0.20/0.72 ~sQ13_spl|~sQ22_spl|~sQ7_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f382,f281,f389,f238])).
% 0.20/0.72 fof(f393,plain,(
% 0.20/0.72 sQ22_spl|~sQ15_spl|~sQ7_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f383,f389,f288,f238])).
% 0.20/0.72 fof(f394,plain,(
% 0.20/0.72 ~sQ22_spl|sQ15_spl|~sQ7_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f384,f389,f288,f238])).
% 0.20/0.72 fof(f395,plain,(
% 0.20/0.72 in(sK10_skl(sK5_skl,sK4_skl),sK4_skl)|~sQ7_spl|~sQ22_spl),
% 0.20/0.72 inference(forward_demodulation,[status(thm)],[f239,f390])).
% 0.20/0.72 fof(f396,plain,(
% 0.20/0.72 in(sK10_skl(sK5_skl,sK4_skl),sK5_skl)|sK4_skl=sK5_skl|sQ12_spl),
% 0.20/0.72 inference(resolution,[status(thm)],[f279,f41])).
% 0.20/0.72 fof(f397,plain,(
% 0.20/0.72 sQ15_spl|sQ5_spl|sQ12_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f396,f288,f232,f277])).
% 0.20/0.72 fof(f415,plain,(
% 0.20/0.72 ~in(sK10_skl(sK5_skl,sK4_skl),sK5_skl)|sK4_skl=sK5_skl|~sQ7_spl|~sQ22_spl),
% 0.20/0.72 inference(resolution,[status(thm)],[f395,f42])).
% 0.20/0.72 fof(f418,plain,(
% 0.20/0.72 ~sQ15_spl|sQ5_spl|~sQ7_spl|~sQ22_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f415,f288,f232,f238,f389])).
% 0.20/0.72 fof(f420,plain,(
% 0.20/0.72 ~in(sK10_skl(sK5_skl,sK4_skl),sK4_skl)|~sQ7_spl|sQ22_spl),
% 0.20/0.72 inference(forward_demodulation,[status(thm)],[f239,f391])).
% 0.20/0.72 fof(f421,plain,(
% 0.20/0.72 in(sK10_skl(sK5_skl,sK4_skl),sK5_skl)|sK4_skl=sK5_skl|~sQ7_spl|sQ22_spl),
% 0.20/0.72 inference(resolution,[status(thm)],[f420,f41])).
% 0.20/0.72 fof(f422,plain,(
% 0.20/0.72 sQ15_spl|sQ5_spl|~sQ7_spl|sQ22_spl),
% 0.20/0.72 inference(split_clause,[status(thm)],[f421,f288,f232,f238,f389])).
% 0.20/0.72 fof(f423,plain,(
% 0.20/0.72 $false),
% 0.20/0.72 inference(sat_refutation,[status(thm)],[f241,f264,f280,f287,f291,f292,f300,f303,f388,f392,f393,f394,f397,f418,f422])).
% 0.20/0.74 % SZS output end CNFRefutation for theBenchmark.p
% 0.20/0.75 % Elapsed time: 0.102953 seconds
% 0.20/0.75 % CPU time: 0.538731 seconds
% 0.20/0.75 % Total memory used: 110.479 MB
% 0.20/0.75 % Net memory used: 110.051 MB
%------------------------------------------------------------------------------