%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU156+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 : n004.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:21:49 PM UTC 2026
% Result : Theorem 1.29s 0.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU156+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.36 % Computer : n004.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 05:53:35 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 1.29/0.65 % Refutation found
% 1.29/0.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.29/0.65 % SZS output start CNFRefutation for theBenchmark
% 1.29/0.65 fof(f1,axiom,(
% 1.29/0.65 (! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) )),
% 1.29/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.29/0.65 fof(f2,axiom,(
% 1.29/0.65 (! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) )),
% 1.29/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.29/0.65 fof(f10,axiom,(
% 1.29/0.65 (! [A,B,C,D] :~ ( unordered_pair(A,B) = unordered_pair(C,D)& A != C& A != D ) )),
% 1.29/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.29/0.65 fof(f11,conjecture,(
% 1.29/0.65 (! [A,B,C,D] :( ordered_pair(A,B) = ordered_pair(C,D)=> ( A = C& B = D ) ) )),
% 1.29/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.29/0.65 fof(f12,negated_conjecture,(
% 1.29/0.65 ~((! [A,B,C,D] :( ordered_pair(A,B) = ordered_pair(C,D)=> ( A = C& B = D ) ) ))),
% 1.29/0.65 inference(negated_conjecture,[status(cth)],[f11])).
% 1.29/0.65 fof(f13,axiom,(
% 1.29/0.65 (! [A] : unordered_pair(A,A) = singleton(A) )),
% 1.29/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.29/0.65 fof(f15,axiom,(
% 1.29/0.65 (! [A,B,C] :( singleton(A) = unordered_pair(B,C)=> A = B ) )),
% 1.29/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.29/0.65 fof(f16,axiom,(
% 1.29/0.65 (! [A,B,C] :( singleton(A) = unordered_pair(B,C)=> B = C ) )),
% 1.29/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.29/0.65 fof(f17,plain,(
% 1.29/0.65 ![X0,X1]: (unordered_pair(X0,X1)=unordered_pair(X1,X0))),
% 1.29/0.65 inference(cnf_transformation,[status(thm)],[f1])).
% 1.29/0.65 fof(f18,plain,(
% 1.29/0.65 ![X0,X1]: (ordered_pair(X0,X1)=unordered_pair(unordered_pair(X0,X1),singleton(X0)))),
% 1.29/0.65 inference(cnf_transformation,[status(thm)],[f2])).
% 1.29/0.65 fof(f26,plain,(
% 1.29/0.65 ![A,B,C,D]: ((~unordered_pair(A,B)=unordered_pair(C,D)|A=C)|A=D)),
% 1.29/0.65 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 1.29/0.65 fof(f27,plain,(
% 1.29/0.65 ![A,D]: ((![C]: ((![B]: ~unordered_pair(A,B)=unordered_pair(C,D))|A=C))|A=D)),
% 1.29/0.65 inference(miniscoping,[status(thm)],[f26])).
% 1.29/0.65 fof(f28,plain,(
% 1.29/0.65 ![X0,X1,X2,X3]: (~unordered_pair(X0,X1)=unordered_pair(X2,X3)|X0=X2|X0=X3)),
% 1.29/0.65 inference(cnf_transformation,[status(thm)],[f27])).
% 1.29/0.66 fof(f29,plain,(
% 1.29/0.66 (?[A,B,C,D]: (ordered_pair(A,B)=ordered_pair(C,D)&(~A=C|~B=D)))),
% 1.29/0.66 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 1.29/0.66 fof(f30,plain,(
% 1.29/0.66 (ordered_pair(sK2_skl,sK3_skl)=ordered_pair(sK4_skl,sK5_skl)&(~sK2_skl=sK4_skl|~sK3_skl=sK5_skl))),
% 1.29/0.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl,sK4_skl,sK5_skl]),skolemize(A,sK2_skl),skolemize(B,sK3_skl),skolemize(C,sK4_skl),skolemize(D,sK5_skl)],[f29])).
% 1.29/0.66 fof(f31,plain,(
% 1.29/0.66 ordered_pair(sK2_skl,sK3_skl)=ordered_pair(sK4_skl,sK5_skl)),
% 1.29/0.66 inference(cnf_transformation,[status(thm)],[f30])).
% 1.29/0.66 fof(f32,plain,(
% 1.29/0.66 ~sK2_skl=sK4_skl|~sK3_skl=sK5_skl),
% 1.29/0.66 inference(cnf_transformation,[status(thm)],[f30])).
% 1.29/0.66 fof(f33,plain,(
% 1.29/0.66 ![X0]: (unordered_pair(X0,X0)=singleton(X0))),
% 1.29/0.66 inference(cnf_transformation,[status(thm)],[f13])).
% 1.29/0.66 fof(f36,plain,(
% 1.29/0.66 ![A,B,C]: (~singleton(A)=unordered_pair(B,C)|A=B)),
% 1.29/0.66 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 1.29/0.66 fof(f37,plain,(
% 1.29/0.66 ![A,B]: ((![C]: ~singleton(A)=unordered_pair(B,C))|A=B)),
% 1.29/0.66 inference(miniscoping,[status(thm)],[f36])).
% 1.29/0.66 fof(f38,plain,(
% 1.29/0.66 ![X0,X1,X2]: (~singleton(X0)=unordered_pair(X1,X2)|X0=X1)),
% 1.29/0.66 inference(cnf_transformation,[status(thm)],[f37])).
% 1.29/0.66 fof(f39,plain,(
% 1.29/0.66 ![A,B,C]: (~singleton(A)=unordered_pair(B,C)|B=C)),
% 1.29/0.66 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 1.29/0.66 fof(f40,plain,(
% 1.29/0.66 ![B,C]: ((![A]: ~singleton(A)=unordered_pair(B,C))|B=C)),
% 1.29/0.66 inference(miniscoping,[status(thm)],[f39])).
% 1.29/0.66 fof(f41,plain,(
% 1.29/0.66 ![X0,X1,X2]: (~singleton(X0)=unordered_pair(X1,X2)|X1=X2)),
% 1.29/0.66 inference(cnf_transformation,[status(thm)],[f40])).
% 1.29/0.66 fof(f42,definition,(
% 1.29/0.66 sQ0_spl <=> (sK2_skl=sK4_skl)),
% 1.29/0.66 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.29/0.66 fof(f43,plain,(
% 1.29/0.66 sK2_skl=sK4_skl|~sQ0_spl),
% 1.29/0.66 inference(component_clause,[status(thm)],[f42])).
% 1.29/0.66 fof(f44,plain,(
% 1.29/0.66 ~sK2_skl=sK4_skl|sQ0_spl),
% 1.29/0.66 inference(component_clause,[status(thm)],[f42])).
% 1.29/0.66 fof(f45,definition,(
% 1.29/0.66 sQ1_spl <=> (sK3_skl=sK5_skl)),
% 1.29/0.66 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.29/0.66 fof(f47,plain,(
% 1.29/0.66 ~sK3_skl=sK5_skl|sQ1_spl),
% 1.29/0.66 inference(component_clause,[status(thm)],[f45])).
% 1.29/0.66 fof(f48,plain,(
% 1.29/0.66 ~sQ0_spl|~sQ1_spl),
% 1.29/0.66 inference(split_clause,[status(thm)],[f32,f42,f45])).
% 1.29/0.66 fof(f89,plain,(
% 1.29/0.66 ![X0,X1]: (ordered_pair(X0,X1)=unordered_pair(singleton(X0),unordered_pair(X0,X1)))),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f18,f17])).
% 1.29/0.66 fof(f101,plain,(
% 1.29/0.66 ![X0,X1]: (ordered_pair(X0,X1)=unordered_pair(unordered_pair(X1,X0),singleton(X0)))),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f17,f18])).
% 1.29/0.66 fof(f114,plain,(
% 1.29/0.66 ![X0,X1,X2,X3]: (~ordered_pair(X0,X1)=unordered_pair(X2,X3)|unordered_pair(X0,X1)=X2|unordered_pair(X0,X1)=X3)),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f18,f28])).
% 1.29/0.66 fof(f115,plain,(
% 1.29/0.66 ![X0,X1,X2,X3]: (~unordered_pair(X0,X1)=unordered_pair(X2,X3)|X1=X2|X1=X3)),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f17,f28])).
% 1.29/0.66 fof(f120,plain,(
% 1.29/0.66 ![X0,X1,X2,X3]: (~unordered_pair(X0,X1)=ordered_pair(X2,X3)|X0=unordered_pair(X2,X3)|X0=singleton(X2))),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f18,f28])).
% 1.29/0.66 fof(f234,plain,(
% 1.29/0.66 ![X0]: (ordered_pair(X0,X0)=unordered_pair(singleton(X0),singleton(X0)))),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f33,f101])).
% 1.29/0.66 fof(f243,plain,(
% 1.29/0.66 ![X0]: (ordered_pair(X0,X0)=singleton(singleton(X0)))),
% 1.29/0.66 inference(forward_demodulation,[status(thm)],[f33,f234])).
% 1.29/0.66 fof(f261,plain,(
% 1.29/0.66 ![X0,X1]: (~singleton(X0)=singleton(X1)|X0=X1)),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f33,f38])).
% 1.29/0.66 fof(f262,plain,(
% 1.29/0.66 ![X0,X1,X2]: (~singleton(X0)=unordered_pair(X1,X2)|X0=X2)),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f17,f38])).
% 1.29/0.66 fof(f273,plain,(
% 1.29/0.66 ![X0,X1,X2]: (~singleton(X0)=ordered_pair(X1,X2)|unordered_pair(X1,X2)=singleton(X1))),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f18,f41])).
% 1.29/0.66 fof(f362,plain,(
% 1.29/0.66 ![X0,X1]: (~ordered_pair(sK2_skl,sK3_skl)=unordered_pair(X0,X1)|unordered_pair(sK4_skl,sK5_skl)=X0|unordered_pair(sK4_skl,sK5_skl)=X1)),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f31,f114])).
% 1.29/0.66 fof(f414,plain,(
% 1.29/0.66 ![X0,X1]: (~unordered_pair(X0,X1)=ordered_pair(sK2_skl,sK3_skl)|X0=unordered_pair(sK4_skl,sK5_skl)|X0=singleton(sK4_skl))),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f31,f120])).
% 1.29/0.66 fof(f423,plain,(
% 1.29/0.66 unordered_pair(sK4_skl,sK5_skl)=unordered_pair(sK3_skl,sK2_skl)|unordered_pair(sK4_skl,sK5_skl)=singleton(sK2_skl)),
% 1.29/0.66 inference(resolution,[status(thm)],[f362,f101])).
% 1.29/0.66 fof(f433,definition,(
% 1.29/0.66 sQ14_spl <=> (unordered_pair(sK4_skl,sK5_skl)=singleton(sK2_skl))),
% 1.29/0.66 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 1.29/0.66 fof(f434,plain,(
% 1.29/0.66 unordered_pair(sK4_skl,sK5_skl)=singleton(sK2_skl)|~sQ14_spl),
% 1.29/0.66 inference(component_clause,[status(thm)],[f433])).
% 1.29/0.66 fof(f440,definition,(
% 1.29/0.66 sQ16_spl <=> (unordered_pair(sK4_skl,sK5_skl)=unordered_pair(sK3_skl,sK2_skl))),
% 1.29/0.66 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 1.29/0.66 fof(f441,plain,(
% 1.29/0.66 unordered_pair(sK4_skl,sK5_skl)=unordered_pair(sK3_skl,sK2_skl)|~sQ16_spl),
% 1.29/0.66 inference(component_clause,[status(thm)],[f440])).
% 1.29/0.66 fof(f443,plain,(
% 1.29/0.66 sQ16_spl|sQ14_spl),
% 1.29/0.66 inference(split_clause,[status(thm)],[f423,f440,f433])).
% 1.29/0.66 fof(f476,plain,(
% 1.29/0.66 ![X0]: (~singleton(X0)=ordered_pair(sK2_skl,sK3_skl)|unordered_pair(sK4_skl,sK5_skl)=singleton(sK4_skl))),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f31,f273])).
% 1.29/0.66 fof(f480,definition,(
% 1.29/0.66 ![X0]: (sQ17_spl <=> (~singleton(X0)=singleton(ordered_pair(sK2_skl,sK3_skl))))),
% 1.29/0.66 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 1.29/0.66 fof(f481,plain,(
% 1.29/0.66 ![X0]: (~singleton(X0)=singleton(ordered_pair(sK2_skl,sK3_skl))|~sQ17_spl)),
% 1.29/0.66 inference(component_clause,[status(thm)],[f480])).
% 1.29/0.66 fof(f487,definition,(
% 1.29/0.66 ![X0]: (sQ19_spl <=> (~singleton(X0)=ordered_pair(sK2_skl,sK3_skl)))),
% 1.29/0.66 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 1.29/0.66 fof(f488,plain,(
% 1.29/0.66 ![X0]: (~singleton(X0)=ordered_pair(sK2_skl,sK3_skl)|~sQ19_spl)),
% 1.29/0.66 inference(component_clause,[status(thm)],[f487])).
% 1.29/0.66 fof(f490,definition,(
% 1.29/0.66 sQ20_spl <=> (unordered_pair(sK4_skl,sK5_skl)=singleton(sK4_skl))),
% 1.29/0.66 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 1.29/0.66 fof(f491,plain,(
% 1.29/0.66 unordered_pair(sK4_skl,sK5_skl)=singleton(sK4_skl)|~sQ20_spl),
% 1.29/0.66 inference(component_clause,[status(thm)],[f490])).
% 1.29/0.66 fof(f493,plain,(
% 1.29/0.66 sQ19_spl|sQ20_spl),
% 1.29/0.66 inference(split_clause,[status(thm)],[f476,f487,f490])).
% 1.29/0.66 fof(f578,plain,(
% 1.29/0.66 singleton(sK2_skl)=unordered_pair(sK4_skl,sK5_skl)|singleton(sK2_skl)=singleton(sK4_skl)),
% 1.29/0.66 inference(resolution,[status(thm)],[f414,f89])).
% 1.29/0.66 fof(f590,definition,(
% 1.29/0.66 sQ21_spl <=> (singleton(sK2_skl)=singleton(sK4_skl))),
% 1.29/0.66 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 1.29/0.66 fof(f591,plain,(
% 1.29/0.66 singleton(sK2_skl)=singleton(sK4_skl)|~sQ21_spl),
% 1.29/0.66 inference(component_clause,[status(thm)],[f590])).
% 1.29/0.66 fof(f593,plain,(
% 1.29/0.66 sQ14_spl|sQ21_spl),
% 1.29/0.66 inference(split_clause,[status(thm)],[f578,f433,f590])).
% 1.29/0.66 fof(f603,plain,(
% 1.29/0.66 sK2_skl=sK4_skl|~sQ21_spl),
% 1.29/0.66 inference(resolution,[status(thm)],[f591,f261])).
% 1.29/0.66 fof(f616,plain,(
% 1.29/0.66 $false|sQ0_spl|~sQ21_spl),
% 1.29/0.66 inference(forward_subsumption_resolution,[status(thm)],[f603,f44])).
% 1.29/0.66 fof(f617,plain,(
% 1.29/0.66 sQ0_spl|~sQ21_spl),
% 1.29/0.66 inference(contradiction_clause,[status(thm)],[f616])).
% 1.29/0.66 fof(f619,plain,(
% 1.29/0.66 ordered_pair(sK2_skl,sK3_skl)=ordered_pair(sK2_skl,sK5_skl)|~sQ0_spl),
% 1.29/0.66 inference(backward_demodulation,[status(thm)],[f43,f31])).
% 1.29/0.66 fof(f637,plain,(
% 1.29/0.66 sK2_skl=sK4_skl|~sQ14_spl),
% 1.29/0.66 inference(resolution,[status(thm)],[f434,f38])).
% 1.29/0.66 fof(f642,plain,(
% 1.29/0.66 ![X0]: (~singleton(X0)=singleton(sK2_skl)|sK4_skl=sK5_skl|~sQ14_spl)),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f434,f41])).
% 1.29/0.66 fof(f652,plain,(
% 1.29/0.66 sQ0_spl|~sQ14_spl),
% 1.29/0.66 inference(split_clause,[status(thm)],[f637,f42,f433])).
% 1.29/0.66 fof(f654,definition,(
% 1.29/0.66 ![X0]: (sQ25_spl <=> (~singleton(X0)=singleton(sK2_skl)))),
% 1.29/0.66 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 1.29/0.66 fof(f655,plain,(
% 1.29/0.66 ![X0]: (~singleton(X0)=singleton(sK2_skl)|~sQ25_spl)),
% 1.29/0.66 inference(component_clause,[status(thm)],[f654])).
% 1.29/0.66 fof(f657,definition,(
% 1.29/0.66 sQ26_spl <=> (sK4_skl=sK5_skl)),
% 1.29/0.66 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 1.29/0.66 fof(f658,plain,(
% 1.29/0.66 sK4_skl=sK5_skl|~sQ26_spl),
% 1.29/0.66 inference(component_clause,[status(thm)],[f657])).
% 1.29/0.66 fof(f660,plain,(
% 1.29/0.66 sQ25_spl|sQ26_spl|~sQ14_spl),
% 1.29/0.66 inference(split_clause,[status(thm)],[f642,f654,f657,f433])).
% 1.29/0.66 fof(f687,plain,(
% 1.29/0.66 ordered_pair(sK2_skl,sK3_skl)=ordered_pair(sK2_skl,sK5_skl)|~sQ0_spl),
% 1.29/0.66 inference(backward_demodulation,[status(thm)],[f43,f31])).
% 1.29/0.66 fof(f701,plain,(
% 1.29/0.66 sK2_skl=sK5_skl|~sQ0_spl|~sQ26_spl),
% 1.29/0.66 inference(forward_demodulation,[status(thm)],[f43,f658])).
% 1.29/0.66 fof(f702,plain,(
% 1.29/0.66 ordered_pair(sK2_skl,sK3_skl)=ordered_pair(sK2_skl,sK2_skl)|~sQ26_spl|~sQ0_spl),
% 1.29/0.66 inference(forward_demodulation,[status(thm)],[f701,f687])).
% 1.29/0.66 fof(f704,plain,(
% 1.29/0.66 ![X0]: (~singleton(X0)=ordered_pair(sK2_skl,sK2_skl)|unordered_pair(sK2_skl,sK3_skl)=singleton(sK2_skl)|~sQ26_spl|~sQ0_spl)),
% 1.29/0.66 inference(paramodulation,[status(thm)],[f702,f273])).
% 1.29/0.66 fof(f712,definition,(
% 1.29/0.66 ![X0]: (sQ27_spl <=> (~singleton(X0)=ordered_pair(sK2_skl,sK2_skl)))),
% 1.29/0.66 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 1.29/0.66 fof(f713,plain,(
% 1.29/0.66 ![X0]: (~singleton(X0)=ordered_pair(sK2_skl,sK2_skl)|~sQ27_spl)),
% 1.29/0.66 inference(component_clause,[status(thm)],[f712])).
% 1.29/0.66 fof(f715,definition,(
% 1.29/0.66 sQ28_spl <=> (unordered_pair(sK2_skl,sK3_skl)=singleton(sK2_skl))),
% 1.29/0.66 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 1.29/0.66 fof(f716,plain,(
% 1.29/0.66 unordered_pair(sK2_skl,sK3_skl)=singleton(sK2_skl)|~sQ28_spl),
% 1.29/0.66 inference(component_clause,[status(thm)],[f715])).
% 1.29/0.66 fof(f718,plain,(
% 1.29/0.66 sQ27_spl|sQ28_spl|~sQ26_spl|~sQ0_spl),
% 1.29/0.66 inference(split_clause,[status(thm)],[f704,f712,f715,f657,f42])).
% 1.29/0.66 fof(f736,plain,(
% 1.29/0.66 $false|~sQ25_spl),
% 1.29/0.66 inference(equality_resolution,[status(thm)],[f655])).
% 1.29/0.66 fof(f737,plain,(
% 1.29/0.66 ~sQ25_spl),
% 1.29/0.66 inference(contradiction_clause,[status(thm)],[f736])).
% 1.29/0.66 fof(f813,plain,(
% 1.29/0.66 $false|~sQ27_spl),
% 1.29/0.66 inference(resolution,[status(thm)],[f713,f243])).
% 1.29/0.66 fof(f815,plain,(
% 1.29/0.66 ~sQ27_spl),
% 1.29/0.66 inference(contradiction_clause,[status(thm)],[f813])).
% 1.29/0.66 fof(f818,plain,(
% 1.29/0.66 unordered_pair(sK2_skl,sK5_skl)=singleton(sK4_skl)|~sQ0_spl|~sQ20_spl),
% 1.29/0.67 inference(forward_demodulation,[status(thm)],[f43,f491])).
% 1.29/0.67 fof(f820,plain,(
% 1.29/0.67 unordered_pair(sK2_skl,sK5_skl)=singleton(sK2_skl)|~sQ0_spl|~sQ20_spl),
% 1.29/0.67 inference(forward_demodulation,[status(thm)],[f43,f818])).
% 1.29/0.67 fof(f828,plain,(
% 1.29/0.67 ![X0]: (~singleton(X0)=singleton(sK2_skl)|sK2_skl=sK5_skl|~sQ0_spl|~sQ20_spl)),
% 1.29/0.67 inference(paramodulation,[status(thm)],[f820,f41])).
% 1.29/0.67 fof(f841,definition,(
% 1.29/0.67 sQ29_spl <=> (sK2_skl=sK5_skl)),
% 1.29/0.67 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 1.29/0.67 fof(f842,plain,(
% 1.29/0.67 sK2_skl=sK5_skl|~sQ29_spl),
% 1.29/0.67 inference(component_clause,[status(thm)],[f841])).
% 1.29/0.67 fof(f844,plain,(
% 1.29/0.67 sQ25_spl|sQ29_spl|~sQ0_spl|~sQ20_spl),
% 1.29/0.67 inference(split_clause,[status(thm)],[f828,f654,f841,f42,f490])).
% 1.29/0.67 fof(f863,plain,(
% 1.29/0.67 ordered_pair(sK2_skl,sK3_skl)=ordered_pair(sK2_skl,sK2_skl)|~sQ29_spl|~sQ0_spl),
% 1.29/0.67 inference(backward_demodulation,[status(thm)],[f842,f619])).
% 1.29/0.67 fof(f866,plain,(
% 1.29/0.67 ![X0]: (~singleton(X0)=ordered_pair(sK2_skl,sK2_skl)|unordered_pair(sK2_skl,sK3_skl)=singleton(sK2_skl)|~sQ29_spl|~sQ0_spl)),
% 1.29/0.67 inference(paramodulation,[status(thm)],[f863,f273])).
% 1.29/0.67 fof(f874,plain,(
% 1.29/0.67 sQ27_spl|sQ28_spl|~sQ29_spl|~sQ0_spl),
% 1.29/0.67 inference(split_clause,[status(thm)],[f866,f712,f715,f841,f42])).
% 1.29/0.67 fof(f1017,definition,(
% 1.29/0.67 sQ35_spl <=> (sK2_skl=sK3_skl)),
% 1.29/0.67 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 1.29/0.67 fof(f1018,plain,(
% 1.29/0.67 sK2_skl=sK3_skl|~sQ35_spl),
% 1.29/0.67 inference(component_clause,[status(thm)],[f1017])).
% 1.29/0.67 fof(f1026,plain,(
% 1.29/0.67 ![X0]: (~singleton(X0)=ordered_pair(sK2_skl,sK2_skl)|~sQ35_spl|~sQ19_spl)),
% 1.29/0.67 inference(backward_demodulation,[status(thm)],[f1018,f488])).
% 1.29/0.67 fof(f1028,plain,(
% 1.29/0.67 ~sK2_skl=sK5_skl|~sQ35_spl|sQ1_spl),
% 1.29/0.67 inference(backward_demodulation,[status(thm)],[f1018,f47])).
% 1.29/0.67 fof(f1029,plain,(
% 1.29/0.67 sQ27_spl|~sQ35_spl|~sQ19_spl),
% 1.29/0.67 inference(split_clause,[status(thm)],[f1026,f712,f1017,f487])).
% 1.29/0.67 fof(f1244,plain,(
% 1.29/0.67 sK2_skl=sK3_skl|~sQ28_spl),
% 1.29/0.67 inference(resolution,[status(thm)],[f716,f262])).
% 1.29/0.67 fof(f1264,plain,(
% 1.29/0.67 sQ35_spl|~sQ28_spl),
% 1.29/0.67 inference(split_clause,[status(thm)],[f1244,f1017,f715])).
% 1.29/0.67 fof(f1653,plain,(
% 1.29/0.67 $false|~sQ17_spl),
% 1.29/0.67 inference(equality_resolution,[status(thm)],[f481])).
% 1.29/0.67 fof(f1654,plain,(
% 1.29/0.67 ~sQ17_spl),
% 1.29/0.67 inference(contradiction_clause,[status(thm)],[f1653])).
% 1.29/0.67 fof(f1848,plain,(
% 1.29/0.67 unordered_pair(sK2_skl,sK5_skl)=unordered_pair(sK3_skl,sK2_skl)|~sQ0_spl|~sQ16_spl),
% 1.29/0.67 inference(forward_demodulation,[status(thm)],[f43,f441])).
% 1.29/0.67 fof(f1849,plain,(
% 1.29/0.67 sK5_skl=sK3_skl|sK5_skl=sK2_skl|~sQ0_spl|~sQ16_spl),
% 1.29/0.67 inference(resolution,[status(thm)],[f1848,f115])).
% 1.29/0.67 fof(f1879,plain,(
% 1.29/0.67 sQ1_spl|sQ29_spl|~sQ0_spl|~sQ16_spl),
% 1.29/0.67 inference(split_clause,[status(thm)],[f1849,f45,f841,f42,f440])).
% 1.29/0.67 fof(f1902,plain,(
% 1.29/0.67 ~sQ29_spl|~sQ35_spl|sQ1_spl),
% 1.29/0.67 inference(split_clause,[status(thm)],[f1028,f841,f1017,f45])).
% 1.29/0.67 fof(f1910,plain,(
% 1.29/0.67 $false),
% 1.29/0.67 inference(sat_refutation,[status(thm)],[f48,f443,f493,f593,f617,f652,f660,f718,f737,f815,f844,f874,f1029,f1264,f1654,f1879,f1902])).
% 1.29/0.67 % SZS output end CNFRefutation for theBenchmark.p
% 1.29/0.67 % Elapsed time: 0.305765 seconds
% 1.29/0.67 % CPU time: 2.045051 seconds
% 1.29/0.67 % Total memory used: 160.033 MB
% 1.29/0.67 % Net memory used: 157.276 MB
%------------------------------------------------------------------------------