%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU156+3 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:50 PM UTC 2026
% Result : Theorem 0.90s 0.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU156+3 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n019.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 05:53:34 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.90/0.69 % Refutation found
% 0.90/0.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.90/0.69 % SZS output start CNFRefutation for theBenchmark
% 0.90/0.69 fof(f1,axiom,(
% 0.90/0.69 (! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) )),
% 0.90/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.90/0.69 fof(f2,axiom,(
% 0.90/0.69 (! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) )),
% 0.90/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.90/0.69 fof(f7,axiom,(
% 0.90/0.69 (! [A,B,C,D] :~ ( unordered_pair(A,B) = unordered_pair(C,D)& A != C& A != D ) )),
% 0.90/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.90/0.69 fof(f8,conjecture,(
% 0.90/0.69 (! [A,B,C,D] :( ordered_pair(A,B) = ordered_pair(C,D)=> ( A = C& B = D ) ) )),
% 0.90/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.90/0.69 fof(f9,negated_conjecture,(
% 0.90/0.69 ~((! [A,B,C,D] :( ordered_pair(A,B) = ordered_pair(C,D)=> ( A = C& B = D ) ) ))),
% 0.90/0.69 inference(negated_conjecture,[status(cth)],[f8])).
% 0.90/0.69 fof(f10,axiom,(
% 0.90/0.69 (! [A] : unordered_pair(A,A) = singleton(A) )),
% 0.90/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.90/0.69 fof(f12,axiom,(
% 0.90/0.69 (! [A,B,C] :( singleton(A) = unordered_pair(B,C)=> A = B ) )),
% 0.90/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.90/0.69 fof(f13,axiom,(
% 0.90/0.69 (! [A,B,C] :( singleton(A) = unordered_pair(B,C)=> B = C ) )),
% 0.90/0.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.90/0.69 fof(f14,plain,(
% 0.90/0.69 ![X0,X1]: (unordered_pair(X0,X1)=unordered_pair(X1,X0))),
% 0.90/0.69 inference(cnf_transformation,[status(thm)],[f1])).
% 0.90/0.69 fof(f15,plain,(
% 0.90/0.69 ![X0,X1]: (ordered_pair(X0,X1)=unordered_pair(unordered_pair(X0,X1),singleton(X0)))),
% 0.90/0.69 inference(cnf_transformation,[status(thm)],[f2])).
% 0.90/0.69 fof(f23,plain,(
% 0.90/0.69 ![A,B,C,D]: ((~unordered_pair(A,B)=unordered_pair(C,D)|A=C)|A=D)),
% 0.90/0.69 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.90/0.69 fof(f24,plain,(
% 0.90/0.69 ![A,D]: ((![C]: ((![B]: ~unordered_pair(A,B)=unordered_pair(C,D))|A=C))|A=D)),
% 0.90/0.69 inference(miniscoping,[status(thm)],[f23])).
% 0.90/0.69 fof(f25,plain,(
% 0.90/0.69 ![X0,X1,X2,X3]: (~unordered_pair(X0,X1)=unordered_pair(X2,X3)|X0=X2|X0=X3)),
% 0.90/0.69 inference(cnf_transformation,[status(thm)],[f24])).
% 0.90/0.69 fof(f26,plain,(
% 0.90/0.69 (?[A,B,C,D]: (ordered_pair(A,B)=ordered_pair(C,D)&(~A=C|~B=D)))),
% 0.90/0.69 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.90/0.69 fof(f27,plain,(
% 0.90/0.69 (ordered_pair(sK2_skl,sK3_skl)=ordered_pair(sK4_skl,sK5_skl)&(~sK2_skl=sK4_skl|~sK3_skl=sK5_skl))),
% 0.90/0.69 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)],[f26])).
% 0.90/0.69 fof(f28,plain,(
% 0.90/0.69 ordered_pair(sK2_skl,sK3_skl)=ordered_pair(sK4_skl,sK5_skl)),
% 0.90/0.69 inference(cnf_transformation,[status(thm)],[f27])).
% 0.90/0.69 fof(f29,plain,(
% 0.90/0.69 ~sK2_skl=sK4_skl|~sK3_skl=sK5_skl),
% 0.90/0.69 inference(cnf_transformation,[status(thm)],[f27])).
% 0.90/0.69 fof(f30,plain,(
% 0.90/0.69 ![X0]: (unordered_pair(X0,X0)=singleton(X0))),
% 0.90/0.69 inference(cnf_transformation,[status(thm)],[f10])).
% 0.90/0.69 fof(f33,plain,(
% 0.90/0.69 ![A,B,C]: (~singleton(A)=unordered_pair(B,C)|A=B)),
% 0.90/0.69 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 0.90/0.69 fof(f34,plain,(
% 0.90/0.69 ![A,B]: ((![C]: ~singleton(A)=unordered_pair(B,C))|A=B)),
% 0.90/0.69 inference(miniscoping,[status(thm)],[f33])).
% 0.90/0.69 fof(f35,plain,(
% 0.90/0.69 ![X0,X1,X2]: (~singleton(X0)=unordered_pair(X1,X2)|X0=X1)),
% 0.90/0.69 inference(cnf_transformation,[status(thm)],[f34])).
% 0.90/0.69 fof(f36,plain,(
% 0.90/0.69 ![A,B,C]: (~singleton(A)=unordered_pair(B,C)|B=C)),
% 0.90/0.69 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.90/0.69 fof(f37,plain,(
% 0.90/0.69 ![B,C]: ((![A]: ~singleton(A)=unordered_pair(B,C))|B=C)),
% 0.90/0.69 inference(miniscoping,[status(thm)],[f36])).
% 0.90/0.69 fof(f38,plain,(
% 0.90/0.69 ![X0,X1,X2]: (~singleton(X0)=unordered_pair(X1,X2)|X1=X2)),
% 0.90/0.69 inference(cnf_transformation,[status(thm)],[f37])).
% 0.90/0.69 fof(f39,definition,(
% 0.90/0.69 sQ0_spl <=> (sK2_skl=sK4_skl)),
% 0.90/0.69 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.90/0.69 fof(f40,plain,(
% 0.90/0.69 sK2_skl=sK4_skl|~sQ0_spl),
% 0.90/0.69 inference(component_clause,[status(thm)],[f39])).
% 0.90/0.69 fof(f41,plain,(
% 0.90/0.69 ~sK2_skl=sK4_skl|sQ0_spl),
% 0.90/0.69 inference(component_clause,[status(thm)],[f39])).
% 0.90/0.69 fof(f42,definition,(
% 0.90/0.69 sQ1_spl <=> (sK3_skl=sK5_skl)),
% 0.90/0.69 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.90/0.69 fof(f44,plain,(
% 0.90/0.69 ~sK3_skl=sK5_skl|sQ1_spl),
% 0.90/0.69 inference(component_clause,[status(thm)],[f42])).
% 0.90/0.69 fof(f45,plain,(
% 0.90/0.69 ~sQ0_spl|~sQ1_spl),
% 0.90/0.69 inference(split_clause,[status(thm)],[f29,f39,f42])).
% 0.90/0.69 fof(f86,plain,(
% 0.90/0.69 ![X0,X1]: (ordered_pair(X0,X1)=unordered_pair(singleton(X0),unordered_pair(X0,X1)))),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f15,f14])).
% 0.90/0.69 fof(f98,plain,(
% 0.90/0.69 ![X0,X1]: (ordered_pair(X0,X1)=unordered_pair(unordered_pair(X1,X0),singleton(X0)))),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f14,f15])).
% 0.90/0.69 fof(f111,plain,(
% 0.90/0.69 ![X0,X1,X2,X3]: (~ordered_pair(X0,X1)=unordered_pair(X2,X3)|unordered_pair(X0,X1)=X2|unordered_pair(X0,X1)=X3)),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f15,f25])).
% 0.90/0.69 fof(f112,plain,(
% 0.90/0.69 ![X0,X1,X2,X3]: (~unordered_pair(X0,X1)=unordered_pair(X2,X3)|X1=X2|X1=X3)),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f14,f25])).
% 0.90/0.69 fof(f117,plain,(
% 0.90/0.69 ![X0,X1,X2,X3]: (~unordered_pair(X0,X1)=ordered_pair(X2,X3)|X0=unordered_pair(X2,X3)|X0=singleton(X2))),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f15,f25])).
% 0.90/0.69 fof(f231,plain,(
% 0.90/0.69 ![X0]: (ordered_pair(X0,X0)=unordered_pair(singleton(X0),singleton(X0)))),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f30,f98])).
% 0.90/0.69 fof(f240,plain,(
% 0.90/0.69 ![X0]: (ordered_pair(X0,X0)=singleton(singleton(X0)))),
% 0.90/0.69 inference(forward_demodulation,[status(thm)],[f30,f231])).
% 0.90/0.69 fof(f258,plain,(
% 0.90/0.69 ![X0,X1]: (~singleton(X0)=singleton(X1)|X0=X1)),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f30,f35])).
% 0.90/0.69 fof(f259,plain,(
% 0.90/0.69 ![X0,X1,X2]: (~singleton(X0)=unordered_pair(X1,X2)|X0=X2)),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f14,f35])).
% 0.90/0.69 fof(f270,plain,(
% 0.90/0.69 ![X0,X1,X2]: (~singleton(X0)=ordered_pair(X1,X2)|unordered_pair(X1,X2)=singleton(X1))),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f15,f38])).
% 0.90/0.69 fof(f359,plain,(
% 0.90/0.69 ![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)),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f28,f111])).
% 0.90/0.69 fof(f411,plain,(
% 0.90/0.69 ![X0,X1]: (~unordered_pair(X0,X1)=ordered_pair(sK2_skl,sK3_skl)|X0=unordered_pair(sK4_skl,sK5_skl)|X0=singleton(sK4_skl))),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f28,f117])).
% 0.90/0.69 fof(f420,plain,(
% 0.90/0.69 unordered_pair(sK4_skl,sK5_skl)=unordered_pair(sK3_skl,sK2_skl)|unordered_pair(sK4_skl,sK5_skl)=singleton(sK2_skl)),
% 0.90/0.69 inference(resolution,[status(thm)],[f359,f98])).
% 0.90/0.69 fof(f430,definition,(
% 0.90/0.69 sQ14_spl <=> (unordered_pair(sK4_skl,sK5_skl)=singleton(sK2_skl))),
% 0.90/0.69 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.90/0.69 fof(f431,plain,(
% 0.90/0.69 unordered_pair(sK4_skl,sK5_skl)=singleton(sK2_skl)|~sQ14_spl),
% 0.90/0.69 inference(component_clause,[status(thm)],[f430])).
% 0.90/0.69 fof(f437,definition,(
% 0.90/0.69 sQ16_spl <=> (unordered_pair(sK4_skl,sK5_skl)=unordered_pair(sK3_skl,sK2_skl))),
% 0.90/0.69 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.90/0.69 fof(f438,plain,(
% 0.90/0.69 unordered_pair(sK4_skl,sK5_skl)=unordered_pair(sK3_skl,sK2_skl)|~sQ16_spl),
% 0.90/0.69 inference(component_clause,[status(thm)],[f437])).
% 0.90/0.69 fof(f440,plain,(
% 0.90/0.69 sQ16_spl|sQ14_spl),
% 0.90/0.69 inference(split_clause,[status(thm)],[f420,f437,f430])).
% 0.90/0.69 fof(f473,plain,(
% 0.90/0.69 ![X0]: (~singleton(X0)=ordered_pair(sK2_skl,sK3_skl)|unordered_pair(sK4_skl,sK5_skl)=singleton(sK4_skl))),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f28,f270])).
% 0.90/0.69 fof(f477,definition,(
% 0.90/0.69 ![X0]: (sQ17_spl <=> (~singleton(X0)=singleton(ordered_pair(sK2_skl,sK3_skl))))),
% 0.90/0.69 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.90/0.69 fof(f478,plain,(
% 0.90/0.69 ![X0]: (~singleton(X0)=singleton(ordered_pair(sK2_skl,sK3_skl))|~sQ17_spl)),
% 0.90/0.69 inference(component_clause,[status(thm)],[f477])).
% 0.90/0.69 fof(f484,definition,(
% 0.90/0.69 ![X0]: (sQ19_spl <=> (~singleton(X0)=ordered_pair(sK2_skl,sK3_skl)))),
% 0.90/0.69 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.90/0.69 fof(f485,plain,(
% 0.90/0.69 ![X0]: (~singleton(X0)=ordered_pair(sK2_skl,sK3_skl)|~sQ19_spl)),
% 0.90/0.69 inference(component_clause,[status(thm)],[f484])).
% 0.90/0.69 fof(f487,definition,(
% 0.90/0.69 sQ20_spl <=> (unordered_pair(sK4_skl,sK5_skl)=singleton(sK4_skl))),
% 0.90/0.69 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.90/0.69 fof(f488,plain,(
% 0.90/0.69 unordered_pair(sK4_skl,sK5_skl)=singleton(sK4_skl)|~sQ20_spl),
% 0.90/0.69 inference(component_clause,[status(thm)],[f487])).
% 0.90/0.69 fof(f490,plain,(
% 0.90/0.69 sQ19_spl|sQ20_spl),
% 0.90/0.69 inference(split_clause,[status(thm)],[f473,f484,f487])).
% 0.90/0.69 fof(f575,plain,(
% 0.90/0.69 singleton(sK2_skl)=unordered_pair(sK4_skl,sK5_skl)|singleton(sK2_skl)=singleton(sK4_skl)),
% 0.90/0.69 inference(resolution,[status(thm)],[f411,f86])).
% 0.90/0.69 fof(f587,definition,(
% 0.90/0.69 sQ21_spl <=> (singleton(sK2_skl)=singleton(sK4_skl))),
% 0.90/0.69 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.90/0.69 fof(f588,plain,(
% 0.90/0.69 singleton(sK2_skl)=singleton(sK4_skl)|~sQ21_spl),
% 0.90/0.69 inference(component_clause,[status(thm)],[f587])).
% 0.90/0.69 fof(f590,plain,(
% 0.90/0.69 sQ14_spl|sQ21_spl),
% 0.90/0.69 inference(split_clause,[status(thm)],[f575,f430,f587])).
% 0.90/0.69 fof(f600,plain,(
% 0.90/0.69 sK2_skl=sK4_skl|~sQ21_spl),
% 0.90/0.69 inference(resolution,[status(thm)],[f588,f258])).
% 0.90/0.69 fof(f613,plain,(
% 0.90/0.69 $false|sQ0_spl|~sQ21_spl),
% 0.90/0.69 inference(forward_subsumption_resolution,[status(thm)],[f600,f41])).
% 0.90/0.69 fof(f614,plain,(
% 0.90/0.69 sQ0_spl|~sQ21_spl),
% 0.90/0.69 inference(contradiction_clause,[status(thm)],[f613])).
% 0.90/0.69 fof(f616,plain,(
% 0.90/0.69 ordered_pair(sK2_skl,sK3_skl)=ordered_pair(sK2_skl,sK5_skl)|~sQ0_spl),
% 0.90/0.69 inference(backward_demodulation,[status(thm)],[f40,f28])).
% 0.90/0.69 fof(f634,plain,(
% 0.90/0.69 sK2_skl=sK4_skl|~sQ14_spl),
% 0.90/0.69 inference(resolution,[status(thm)],[f431,f35])).
% 0.90/0.69 fof(f639,plain,(
% 0.90/0.69 ![X0]: (~singleton(X0)=singleton(sK2_skl)|sK4_skl=sK5_skl|~sQ14_spl)),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f431,f38])).
% 0.90/0.69 fof(f649,plain,(
% 0.90/0.69 sQ0_spl|~sQ14_spl),
% 0.90/0.69 inference(split_clause,[status(thm)],[f634,f39,f430])).
% 0.90/0.69 fof(f651,definition,(
% 0.90/0.69 ![X0]: (sQ25_spl <=> (~singleton(X0)=singleton(sK2_skl)))),
% 0.90/0.69 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.90/0.69 fof(f652,plain,(
% 0.90/0.69 ![X0]: (~singleton(X0)=singleton(sK2_skl)|~sQ25_spl)),
% 0.90/0.69 inference(component_clause,[status(thm)],[f651])).
% 0.90/0.69 fof(f654,definition,(
% 0.90/0.69 sQ26_spl <=> (sK4_skl=sK5_skl)),
% 0.90/0.69 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.90/0.69 fof(f655,plain,(
% 0.90/0.69 sK4_skl=sK5_skl|~sQ26_spl),
% 0.90/0.69 inference(component_clause,[status(thm)],[f654])).
% 0.90/0.69 fof(f657,plain,(
% 0.90/0.69 sQ25_spl|sQ26_spl|~sQ14_spl),
% 0.90/0.69 inference(split_clause,[status(thm)],[f639,f651,f654,f430])).
% 0.90/0.69 fof(f684,plain,(
% 0.90/0.69 ordered_pair(sK2_skl,sK3_skl)=ordered_pair(sK2_skl,sK5_skl)|~sQ0_spl),
% 0.90/0.69 inference(backward_demodulation,[status(thm)],[f40,f28])).
% 0.90/0.69 fof(f698,plain,(
% 0.90/0.69 sK2_skl=sK5_skl|~sQ0_spl|~sQ26_spl),
% 0.90/0.69 inference(forward_demodulation,[status(thm)],[f40,f655])).
% 0.90/0.69 fof(f699,plain,(
% 0.90/0.69 ordered_pair(sK2_skl,sK3_skl)=ordered_pair(sK2_skl,sK2_skl)|~sQ26_spl|~sQ0_spl),
% 0.90/0.69 inference(forward_demodulation,[status(thm)],[f698,f684])).
% 0.90/0.69 fof(f701,plain,(
% 0.90/0.69 ![X0]: (~singleton(X0)=ordered_pair(sK2_skl,sK2_skl)|unordered_pair(sK2_skl,sK3_skl)=singleton(sK2_skl)|~sQ26_spl|~sQ0_spl)),
% 0.90/0.69 inference(paramodulation,[status(thm)],[f699,f270])).
% 0.90/0.69 fof(f709,definition,(
% 0.90/0.69 ![X0]: (sQ27_spl <=> (~singleton(X0)=ordered_pair(sK2_skl,sK2_skl)))),
% 0.90/0.69 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.90/0.69 fof(f710,plain,(
% 0.90/0.69 ![X0]: (~singleton(X0)=ordered_pair(sK2_skl,sK2_skl)|~sQ27_spl)),
% 0.90/0.69 inference(component_clause,[status(thm)],[f709])).
% 0.90/0.69 fof(f712,definition,(
% 0.90/0.69 sQ28_spl <=> (unordered_pair(sK2_skl,sK3_skl)=singleton(sK2_skl))),
% 0.90/0.69 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.90/0.69 fof(f713,plain,(
% 0.90/0.69 unordered_pair(sK2_skl,sK3_skl)=singleton(sK2_skl)|~sQ28_spl),
% 0.90/0.69 inference(component_clause,[status(thm)],[f712])).
% 0.90/0.69 fof(f715,plain,(
% 0.90/0.69 sQ27_spl|sQ28_spl|~sQ26_spl|~sQ0_spl),
% 0.90/0.69 inference(split_clause,[status(thm)],[f701,f709,f712,f654,f39])).
% 0.90/0.69 fof(f733,plain,(
% 0.90/0.69 $false|~sQ25_spl),
% 0.90/0.69 inference(equality_resolution,[status(thm)],[f652])).
% 0.90/0.69 fof(f734,plain,(
% 0.90/0.69 ~sQ25_spl),
% 0.90/0.69 inference(contradiction_clause,[status(thm)],[f733])).
% 0.90/0.69 fof(f810,plain,(
% 0.90/0.69 $false|~sQ27_spl),
% 0.90/0.69 inference(resolution,[status(thm)],[f710,f240])).
% 0.90/0.69 fof(f812,plain,(
% 0.90/0.69 ~sQ27_spl),
% 0.90/0.69 inference(contradiction_clause,[status(thm)],[f810])).
% 0.90/0.69 fof(f815,plain,(
% 0.90/0.69 unordered_pair(sK2_skl,sK5_skl)=singleton(sK4_skl)|~sQ0_spl|~sQ20_spl),
% 0.90/0.70 inference(forward_demodulation,[status(thm)],[f40,f488])).
% 0.90/0.70 fof(f817,plain,(
% 0.90/0.70 unordered_pair(sK2_skl,sK5_skl)=singleton(sK2_skl)|~sQ0_spl|~sQ20_spl),
% 0.90/0.70 inference(forward_demodulation,[status(thm)],[f40,f815])).
% 0.90/0.70 fof(f825,plain,(
% 0.90/0.70 ![X0]: (~singleton(X0)=singleton(sK2_skl)|sK2_skl=sK5_skl|~sQ0_spl|~sQ20_spl)),
% 0.90/0.70 inference(paramodulation,[status(thm)],[f817,f38])).
% 0.90/0.70 fof(f838,definition,(
% 0.90/0.70 sQ29_spl <=> (sK2_skl=sK5_skl)),
% 0.90/0.70 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.90/0.70 fof(f839,plain,(
% 0.90/0.70 sK2_skl=sK5_skl|~sQ29_spl),
% 0.90/0.70 inference(component_clause,[status(thm)],[f838])).
% 0.90/0.70 fof(f841,plain,(
% 0.90/0.70 sQ25_spl|sQ29_spl|~sQ0_spl|~sQ20_spl),
% 0.90/0.70 inference(split_clause,[status(thm)],[f825,f651,f838,f39,f487])).
% 0.90/0.70 fof(f860,plain,(
% 0.90/0.70 ordered_pair(sK2_skl,sK3_skl)=ordered_pair(sK2_skl,sK2_skl)|~sQ29_spl|~sQ0_spl),
% 0.90/0.70 inference(backward_demodulation,[status(thm)],[f839,f616])).
% 0.90/0.70 fof(f863,plain,(
% 0.90/0.70 ![X0]: (~singleton(X0)=ordered_pair(sK2_skl,sK2_skl)|unordered_pair(sK2_skl,sK3_skl)=singleton(sK2_skl)|~sQ29_spl|~sQ0_spl)),
% 0.90/0.70 inference(paramodulation,[status(thm)],[f860,f270])).
% 0.90/0.70 fof(f871,plain,(
% 0.90/0.70 sQ27_spl|sQ28_spl|~sQ29_spl|~sQ0_spl),
% 0.90/0.70 inference(split_clause,[status(thm)],[f863,f709,f712,f838,f39])).
% 0.90/0.70 fof(f1014,definition,(
% 0.90/0.70 sQ35_spl <=> (sK2_skl=sK3_skl)),
% 0.90/0.70 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.90/0.70 fof(f1015,plain,(
% 0.90/0.70 sK2_skl=sK3_skl|~sQ35_spl),
% 0.90/0.70 inference(component_clause,[status(thm)],[f1014])).
% 0.90/0.70 fof(f1023,plain,(
% 0.90/0.70 ![X0]: (~singleton(X0)=ordered_pair(sK2_skl,sK2_skl)|~sQ35_spl|~sQ19_spl)),
% 0.90/0.70 inference(backward_demodulation,[status(thm)],[f1015,f485])).
% 0.90/0.70 fof(f1025,plain,(
% 0.90/0.70 ~sK2_skl=sK5_skl|~sQ35_spl|sQ1_spl),
% 0.90/0.70 inference(backward_demodulation,[status(thm)],[f1015,f44])).
% 0.90/0.70 fof(f1026,plain,(
% 0.90/0.70 sQ27_spl|~sQ35_spl|~sQ19_spl),
% 0.90/0.70 inference(split_clause,[status(thm)],[f1023,f709,f1014,f484])).
% 0.90/0.70 fof(f1241,plain,(
% 0.90/0.70 sK2_skl=sK3_skl|~sQ28_spl),
% 0.90/0.70 inference(resolution,[status(thm)],[f713,f259])).
% 0.90/0.70 fof(f1261,plain,(
% 0.90/0.70 sQ35_spl|~sQ28_spl),
% 0.90/0.70 inference(split_clause,[status(thm)],[f1241,f1014,f712])).
% 0.90/0.70 fof(f1650,plain,(
% 0.90/0.70 $false|~sQ17_spl),
% 0.90/0.70 inference(equality_resolution,[status(thm)],[f478])).
% 0.90/0.70 fof(f1651,plain,(
% 0.90/0.70 ~sQ17_spl),
% 0.90/0.70 inference(contradiction_clause,[status(thm)],[f1650])).
% 0.90/0.70 fof(f1845,plain,(
% 0.90/0.70 unordered_pair(sK2_skl,sK5_skl)=unordered_pair(sK3_skl,sK2_skl)|~sQ0_spl|~sQ16_spl),
% 0.90/0.70 inference(forward_demodulation,[status(thm)],[f40,f438])).
% 0.90/0.70 fof(f1846,plain,(
% 0.90/0.70 sK5_skl=sK3_skl|sK5_skl=sK2_skl|~sQ0_spl|~sQ16_spl),
% 0.90/0.70 inference(resolution,[status(thm)],[f1845,f112])).
% 0.90/0.70 fof(f1876,plain,(
% 0.90/0.70 sQ1_spl|sQ29_spl|~sQ0_spl|~sQ16_spl),
% 0.90/0.70 inference(split_clause,[status(thm)],[f1846,f42,f838,f39,f437])).
% 0.90/0.70 fof(f1899,plain,(
% 0.90/0.70 ~sQ29_spl|~sQ35_spl|sQ1_spl),
% 0.90/0.70 inference(split_clause,[status(thm)],[f1025,f838,f1014,f42])).
% 0.90/0.70 fof(f1907,plain,(
% 0.90/0.70 $false),
% 0.90/0.70 inference(sat_refutation,[status(thm)],[f45,f440,f490,f590,f614,f649,f657,f715,f734,f812,f841,f871,f1026,f1261,f1651,f1876,f1899])).
% 0.90/0.70 % SZS output end CNFRefutation for theBenchmark.p
% 0.41/0.72 % Elapsed time: 0.340785 seconds
% 0.41/0.72 % CPU time: 2.442699 seconds
% 0.41/0.72 % Total memory used: 162.347 MB
% 0.41/0.72 % Net memory used: 159.225 MB
%------------------------------------------------------------------------------