%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM612+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 01:43:21 PM UTC 2026
% Result : Theorem 1.30s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM612+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n005.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 02:44:17 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 1.30/0.66 % Refutation found
% 1.30/0.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.30/0.66 % SZS output start CNFRefutation for theBenchmark
% 1.30/0.66 fof(f5,definition,(
% 1.30/0.66 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f6,axiom,(
% 1.30/0.66 isFinite0(slcrc0) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f10,definition,(
% 1.30/0.66 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f11,axiom,(
% 1.30/0.66 (! [W0] :( ( aSet0(W0)& isFinite0(W0) )=> (! [W1] :( aSubsetOf0(W1,W0)=> isFinite0(W1) ) )) )),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f12,axiom,(
% 1.30/0.66 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f23,axiom,(
% 1.30/0.66 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f24,axiom,(
% 1.30/0.66 aElementOf0(sz00,szNzAzT0) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f28,axiom,(
% 1.30/0.66 (! [W0] :( aElementOf0(W0,szNzAzT0)=> W0 != szszuzczcdt0(W0) ) )),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f30,axiom,(
% 1.30/0.66 (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlseqdt0(sz00,W0) ) )),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f34,axiom,(
% 1.30/0.66 (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlseqdt0(W0,W0) ) )),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f41,axiom,(
% 1.30/0.66 (! [W0] :( aSet0(W0)=> ( aElementOf0(sbrdtbr0(W0),szNzAzT0)<=> isFinite0(W0) ) ) )),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f44,axiom,(
% 1.30/0.66 (! [W0] :( aSet0(W0)=> (! [W1] :( ( isFinite0(W0)& aElementOf0(W1,W0) )=> szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) )) )),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f57,definition,(
% 1.30/0.66 (! [W0,W1] :( ( aSet0(W0)& aElementOf0(W1,szNzAzT0) )=> (! [W2] :( W2 = slbdtsldtrb0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aSubsetOf0(W3,W0)& sbrdtbr0(W3) = W1 ) ) )) ) )) )),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f64,axiom,(
% 1.30/0.66 (! [W0] :( aFunction0(W0)=> aSet0(szDzozmdt0(W0)) ) )),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f73,hypothesis,(
% 1.30/0.66 ( aSet0(xT)& isFinite0(xT) ) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f74,hypothesis,(
% 1.30/0.66 aElementOf0(xK,szNzAzT0) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f76,hypothesis,(
% 1.30/0.66 ( aFunction0(xc)& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f78,hypothesis,(
% 1.30/0.66 xK != sz00 ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f80,hypothesis,(
% 1.30/0.66 ( aElementOf0(xk,szNzAzT0)& szszuzczcdt0(xk) = xK ) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f94,hypothesis,(
% 1.30/0.66 ( aElementOf0(szDzizrdt0(xd),xT)& isCountable0(sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f95,hypothesis,(
% 1.30/0.66 ( aSet0(xO)& xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f99,hypothesis,(
% 1.30/0.66 aElementOf0(xQ,slbdtsldtrb0(xO,xK)) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f100,hypothesis,(
% 1.30/0.66 ( aSubsetOf0(xQ,xO)& xQ != slcrc0 ) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f101,hypothesis,(
% 1.30/0.66 aSubsetOf0(xQ,szNzAzT0) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f103,hypothesis,(
% 1.30/0.66 xp = szmzizndt0(xQ) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f104,hypothesis,(
% 1.30/0.66 ( aSet0(xP)& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f105,hypothesis,(
% 1.30/0.66 aElementOf0(xp,xQ) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f107,hypothesis,(
% 1.30/0.66 aSubsetOf0(xP,xQ) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f109,conjecture,(
% 1.30/0.66 ( szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ)& aElementOf0(sbrdtbr0(xP),szNzAzT0) ) ),
% 1.30/0.66 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.30/0.66 fof(f110,negated_conjecture,(
% 1.30/0.66 ~(( szszuzczcdt0(sbrdtbr0(xP)) = sbrdtbr0(xQ)& aElementOf0(sbrdtbr0(xP),szNzAzT0) ) )),
% 1.30/0.66 inference(negated_conjecture,[status(cth)],[f109])).
% 1.30/0.66 fof(f121,plain,(
% 1.30/0.66 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 1.30/0.66 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 1.30/0.66 fof(f122,plain,(
% 1.30/0.66 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 1.30/0.66 inference(NNF_transformation,[status(thm)],[f121])).
% 1.30/0.66 fof(f123,plain,(
% 1.30/0.66 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 1.30/0.66 inference(miniscoping,[status(thm)],[f122])).
% 1.30/0.66 fof(f124,plain,(
% 1.30/0.66 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 1.30/0.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f123])).
% 1.30/0.66 fof(f126,plain,(
% 1.30/0.66 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 1.30/0.66 inference(cnf_transformation,[status(thm)],[f124])).
% 1.30/0.66 fof(f128,plain,(
% 1.30/0.66 isFinite0(slcrc0)),
% 1.30/0.66 inference(cnf_transformation,[status(thm)],[f6])).
% 1.30/0.66 fof(f135,plain,(
% 1.30/0.66 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 1.30/0.66 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 1.30/0.66 fof(f136,plain,(
% 1.30/0.66 ![W0]: (~aSet0(W0)|(![W1]: ((~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))&(aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 1.30/0.66 inference(NNF_transformation,[status(thm)],[f135])).
% 1.30/0.66 fof(f137,plain,(
% 1.30/0.66 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 1.30/0.66 inference(miniscoping,[status(thm)],[f136])).
% 1.30/0.66 fof(f138,plain,(
% 1.30/0.66 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(aElementOf0(sK1_skl(W1,W0),W1)&~aElementOf0(sK1_skl(W1,W0),W0)))))))),
% 1.30/0.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f137])).
% 1.30/0.66 fof(f139,plain,(
% 1.30/0.66 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 1.30/0.66 inference(cnf_transformation,[status(thm)],[f138])).
% 1.30/0.66 fof(f143,plain,(
% 1.30/0.66 ![W0]: ((~aSet0(W0)|~isFinite0(W0))|(![W1]: (~aSubsetOf0(W1,W0)|isFinite0(W1))))),
% 1.30/0.66 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 1.30/0.66 fof(f144,plain,(
% 1.30/0.66 ![X0,X1]: (~aSet0(X0)|~isFinite0(X0)|~aSubsetOf0(X1,X0)|isFinite0(X1))),
% 1.30/0.66 inference(cnf_transformation,[status(thm)],[f143])).
% 1.30/0.66 fof(f145,plain,(
% 1.30/0.66 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 1.30/0.66 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 1.30/0.67 fof(f146,plain,(
% 1.30/0.67 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f145])).
% 1.30/0.67 fof(f187,plain,(
% 1.30/0.67 aSet0(szNzAzT0)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f23])).
% 1.30/0.67 fof(f189,plain,(
% 1.30/0.67 aElementOf0(sz00,szNzAzT0)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f24])).
% 1.30/0.67 fof(f199,plain,(
% 1.30/0.67 ![W0]: (~aElementOf0(W0,szNzAzT0)|~W0=szszuzczcdt0(W0))),
% 1.30/0.67 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 1.30/0.67 fof(f200,plain,(
% 1.30/0.67 ![X0]: (~aElementOf0(X0,szNzAzT0)|~X0=szszuzczcdt0(X0))),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f199])).
% 1.30/0.67 fof(f203,plain,(
% 1.30/0.67 ![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlseqdt0(sz00,W0))),
% 1.30/0.67 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 1.30/0.67 fof(f204,plain,(
% 1.30/0.67 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlseqdt0(sz00,X0))),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f203])).
% 1.30/0.67 fof(f213,plain,(
% 1.30/0.67 ![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlseqdt0(W0,W0))),
% 1.30/0.67 inference(pre_NNF_transformation,[status(thm)],[f34])).
% 1.30/0.67 fof(f214,plain,(
% 1.30/0.67 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlseqdt0(X0,X0))),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f213])).
% 1.30/0.67 fof(f227,plain,(
% 1.30/0.67 ![W0]: (~aSet0(W0)|(aElementOf0(sbrdtbr0(W0),szNzAzT0)<=>isFinite0(W0)))),
% 1.30/0.67 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 1.30/0.67 fof(f228,plain,(
% 1.30/0.67 ![W0]: (~aSet0(W0)|((~aElementOf0(sbrdtbr0(W0),szNzAzT0)|isFinite0(W0))&(aElementOf0(sbrdtbr0(W0),szNzAzT0)|~isFinite0(W0))))),
% 1.30/0.67 inference(NNF_transformation,[status(thm)],[f227])).
% 1.30/0.67 fof(f229,plain,(
% 1.30/0.67 ![X0]: (~aSet0(X0)|~aElementOf0(sbrdtbr0(X0),szNzAzT0)|isFinite0(X0))),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f228])).
% 1.30/0.67 fof(f230,plain,(
% 1.30/0.67 ![X0]: (~aSet0(X0)|aElementOf0(sbrdtbr0(X0),szNzAzT0)|~isFinite0(X0))),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f228])).
% 1.30/0.67 fof(f237,plain,(
% 1.30/0.67 ![W0]: (~aSet0(W0)|(![W1]: ((~isFinite0(W0)|~aElementOf0(W1,W0))|szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1)))=sbrdtbr0(W0))))),
% 1.30/0.67 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 1.30/0.67 fof(f238,plain,(
% 1.30/0.67 ![X0,X1]: (~aSet0(X0)|~isFinite0(X0)|~aElementOf0(X1,X0)|szszuzczcdt0(sbrdtbr0(sdtmndt0(X0,X1)))=sbrdtbr0(X0))),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f237])).
% 1.30/0.67 fof(f292,plain,(
% 1.30/0.67 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|(![W2]: (W2=slbdtsldtrb0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))))))),
% 1.30/0.67 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 1.30/0.67 fof(f293,plain,(
% 1.30/0.67 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|(![W2]: ((~W2=slbdtsldtrb0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1))&(aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1))))))&(W2=slbdtsldtrb0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1))&(aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))))))))),
% 1.30/0.67 inference(NNF_transformation,[status(thm)],[f292])).
% 1.30/0.67 fof(f294,plain,(
% 1.30/0.67 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|((![W2]: (~W2=slbdtsldtrb0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))&(![W3]: (aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1)))))))&(![W2]: (W2=slbdtsldtrb0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1))&(aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))))))))),
% 1.30/0.67 inference(miniscoping,[status(thm)],[f293])).
% 1.30/0.67 fof(f295,plain,(
% 1.30/0.67 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|((![W2]: (~W2=slbdtsldtrb0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))&(![W3]: (aElementOf0(W3,W2)|(~aSubsetOf0(W3,W0)|~sbrdtbr0(W3)=W1)))))))&(![W2]: (W2=slbdtsldtrb0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK10_skl(W2,W1,W0),W2)|(~aSubsetOf0(sK10_skl(W2,W1,W0),W0)|~sbrdtbr0(sK10_skl(W2,W1,W0))=W1))&(aElementOf0(sK10_skl(W2,W1,W0),W2)|(aSubsetOf0(sK10_skl(W2,W1,W0),W0)&sbrdtbr0(sK10_skl(W2,W1,W0))=W1))))))))),
% 1.30/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W3,sK10_skl(W2,W1,W0))],[f294])).
% 1.30/0.67 fof(f298,plain,(
% 1.30/0.67 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|~aElementOf0(X3,X2)|sbrdtbr0(X3)=X1)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f295])).
% 1.30/0.67 fof(f319,plain,(
% 1.30/0.67 ![W0]: (~aFunction0(W0)|aSet0(szDzozmdt0(W0)))),
% 1.30/0.67 inference(pre_NNF_transformation,[status(thm)],[f64])).
% 1.30/0.67 fof(f320,plain,(
% 1.30/0.67 ![X0]: (~aFunction0(X0)|aSet0(szDzozmdt0(X0)))),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f319])).
% 1.30/0.67 fof(f367,plain,(
% 1.30/0.67 aSet0(xT)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f73])).
% 1.30/0.67 fof(f369,plain,(
% 1.30/0.67 aElementOf0(xK,szNzAzT0)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f74])).
% 1.30/0.67 fof(f372,plain,(
% 1.30/0.67 aFunction0(xc)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f76])).
% 1.30/0.67 fof(f381,plain,(
% 1.30/0.67 ~xK=sz00),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f78])).
% 1.30/0.67 fof(f383,plain,(
% 1.30/0.67 aElementOf0(xk,szNzAzT0)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f80])).
% 1.30/0.67 fof(f429,plain,(
% 1.30/0.67 aElementOf0(szDzizrdt0(xd),xT)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f94])).
% 1.30/0.67 fof(f431,plain,(
% 1.30/0.67 aSet0(xO)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f95])).
% 1.30/0.67 fof(f441,plain,(
% 1.30/0.67 aElementOf0(xQ,slbdtsldtrb0(xO,xK))),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f99])).
% 1.30/0.67 fof(f443,plain,(
% 1.30/0.67 ~xQ=slcrc0),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f100])).
% 1.30/0.67 fof(f444,plain,(
% 1.30/0.67 aSubsetOf0(xQ,szNzAzT0)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f101])).
% 1.30/0.67 fof(f446,plain,(
% 1.30/0.67 xp=szmzizndt0(xQ)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f103])).
% 1.30/0.67 fof(f447,plain,(
% 1.30/0.67 aSet0(xP)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f104])).
% 1.30/0.67 fof(f448,plain,(
% 1.30/0.67 xP=sdtmndt0(xQ,szmzizndt0(xQ))),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f104])).
% 1.30/0.67 fof(f449,plain,(
% 1.30/0.67 aElementOf0(xp,xQ)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f105])).
% 1.30/0.67 fof(f451,plain,(
% 1.30/0.67 aSubsetOf0(xP,xQ)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f107])).
% 1.30/0.67 fof(f453,plain,(
% 1.30/0.67 (~szszuzczcdt0(sbrdtbr0(xP))=sbrdtbr0(xQ)|~aElementOf0(sbrdtbr0(xP),szNzAzT0))),
% 1.30/0.67 inference(pre_NNF_transformation,[status(thm)],[f110])).
% 1.30/0.67 fof(f454,plain,(
% 1.30/0.67 ~szszuzczcdt0(sbrdtbr0(xP))=sbrdtbr0(xQ)|~aElementOf0(sbrdtbr0(xP),szNzAzT0)),
% 1.30/0.67 inference(cnf_transformation,[status(thm)],[f453])).
% 1.30/0.67 fof(f461,definition,(
% 1.30/0.67 sQ0_spl <=> (szszuzczcdt0(sbrdtbr0(xP))=sbrdtbr0(xQ))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f463,plain,(
% 1.30/0.67 ~szszuzczcdt0(sbrdtbr0(xP))=sbrdtbr0(xQ)|sQ0_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f461])).
% 1.30/0.67 fof(f464,definition,(
% 1.30/0.67 sQ1_spl <=> (aElementOf0(sbrdtbr0(xP),szNzAzT0))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f467,plain,(
% 1.30/0.67 ~sQ0_spl|~sQ1_spl),
% 1.30/0.67 inference(split_clause,[status(thm)],[f454,f461,f464])).
% 1.30/0.67 fof(f469,plain,(
% 1.30/0.67 ![X0]: (~aElementOf0(X0,slcrc0))),
% 1.30/0.67 inference(destructive_equality_resolution,[status(thm)],[f126])).
% 1.30/0.67 fof(f493,plain,(
% 1.30/0.67 ![X0,X1,X2]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,slbdtsldtrb0(X0,X1))|sbrdtbr0(X2)=X1)),
% 1.30/0.67 inference(destructive_equality_resolution,[status(thm)],[f298])).
% 1.30/0.67 fof(f510,plain,(
% 1.30/0.67 aElementOf0(sbrdtbr0(xP),szNzAzT0)|~isFinite0(xP)),
% 1.30/0.67 inference(resolution,[status(thm)],[f230,f447])).
% 1.30/0.67 fof(f511,definition,(
% 1.30/0.67 sQ2_spl <=> (isFinite0(xP))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f514,plain,(
% 1.30/0.67 sQ1_spl|~sQ2_spl),
% 1.30/0.67 inference(split_clause,[status(thm)],[f510,f464,f511])).
% 1.30/0.67 fof(f521,definition,(
% 1.30/0.67 sQ4_spl <=> (isFinite0(slcrc0))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f523,plain,(
% 1.30/0.67 ~isFinite0(slcrc0)|sQ4_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f521])).
% 1.30/0.67 fof(f572,definition,(
% 1.30/0.67 sQ15_spl <=> (xT=slcrc0)),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f573,plain,(
% 1.30/0.67 xT=slcrc0|~sQ15_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f572])).
% 1.30/0.67 fof(f617,definition,(
% 1.30/0.67 sQ24_spl <=> (aSet0(szNzAzT0))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f619,plain,(
% 1.30/0.67 ~aSet0(szNzAzT0)|sQ24_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f617])).
% 1.30/0.67 fof(f640,plain,(
% 1.30/0.67 $false|sQ24_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f619,f187])).
% 1.30/0.67 fof(f641,plain,(
% 1.30/0.67 sQ24_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f640])).
% 1.30/0.67 fof(f658,definition,(
% 1.30/0.67 sQ29_spl <=> (aSet0(xO))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f660,plain,(
% 1.30/0.67 ~aSet0(xO)|sQ29_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f658])).
% 1.30/0.67 fof(f665,definition,(
% 1.30/0.67 sQ31_spl <=> (aSet0(xQ))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f668,definition,(
% 1.30/0.67 sQ32_spl <=> (isFinite0(xQ))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f683,plain,(
% 1.30/0.67 $false|sQ29_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f660,f431])).
% 1.30/0.67 fof(f684,plain,(
% 1.30/0.67 sQ29_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f683])).
% 1.30/0.67 fof(f726,plain,(
% 1.30/0.67 ~aSet0(szNzAzT0)|aSet0(xQ)),
% 1.30/0.67 inference(resolution,[status(thm)],[f139,f444])).
% 1.30/0.67 fof(f730,plain,(
% 1.30/0.67 ~sQ24_spl|sQ31_spl),
% 1.30/0.67 inference(split_clause,[status(thm)],[f726,f617,f665])).
% 1.30/0.67 fof(f752,plain,(
% 1.30/0.67 ~aSet0(xO)|~aElementOf0(xK,szNzAzT0)|sbrdtbr0(xQ)=xK),
% 1.30/0.67 inference(resolution,[status(thm)],[f493,f441])).
% 1.30/0.67 fof(f753,definition,(
% 1.30/0.67 sQ43_spl <=> (aElementOf0(xK,szNzAzT0))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f755,plain,(
% 1.30/0.67 ~aElementOf0(xK,szNzAzT0)|sQ43_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f753])).
% 1.30/0.67 fof(f756,definition,(
% 1.30/0.67 sQ44_spl <=> (sbrdtbr0(xQ)=xK)),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f757,plain,(
% 1.30/0.67 sbrdtbr0(xQ)=xK|~sQ44_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f756])).
% 1.30/0.67 fof(f759,plain,(
% 1.30/0.67 ~sQ29_spl|~sQ43_spl|sQ44_spl),
% 1.30/0.67 inference(split_clause,[status(thm)],[f752,f658,f753,f756])).
% 1.30/0.67 fof(f767,definition,(
% 1.30/0.67 sQ45_spl <=> (aSet0(xT))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f769,plain,(
% 1.30/0.67 ~aSet0(xT)|sQ45_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f767])).
% 1.30/0.67 fof(f789,plain,(
% 1.30/0.67 ![X0]: (~aElementOf0(X0,xT)|~sQ15_spl)),
% 1.30/0.67 inference(forward_demodulation,[status(thm)],[f573,f469])).
% 1.30/0.67 fof(f793,plain,(
% 1.30/0.67 ~sz00=szszuzczcdt0(sz00)),
% 1.30/0.67 inference(resolution,[status(thm)],[f189,f200])).
% 1.30/0.67 fof(f801,plain,(
% 1.30/0.67 $false|sQ43_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f369,f755])).
% 1.30/0.67 fof(f802,plain,(
% 1.30/0.67 sQ43_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f801])).
% 1.30/0.67 fof(f869,plain,(
% 1.30/0.67 $false|sQ45_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f769,f367])).
% 1.30/0.67 fof(f870,plain,(
% 1.30/0.67 sQ45_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f869])).
% 1.30/0.67 fof(f895,plain,(
% 1.30/0.67 ~aSet0(xQ)|~aElementOf0(xK,szNzAzT0)|isFinite0(xQ)|~sQ44_spl),
% 1.30/0.67 inference(paramodulation,[status(thm)],[f757,f229])).
% 1.30/0.67 fof(f900,plain,(
% 1.30/0.67 ~sQ31_spl|~sQ43_spl|sQ32_spl|~sQ44_spl),
% 1.30/0.67 inference(split_clause,[status(thm)],[f895,f665,f753,f668,f756])).
% 1.30/0.67 fof(f958,definition,(
% 1.30/0.67 sQ68_spl <=> (aElementOf0(xk,szNzAzT0))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f960,plain,(
% 1.30/0.67 ~aElementOf0(xk,szNzAzT0)|sQ68_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f958])).
% 1.30/0.67 fof(f971,plain,(
% 1.30/0.67 $false|sQ68_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f960,f383])).
% 1.30/0.67 fof(f972,plain,(
% 1.30/0.67 sQ68_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f971])).
% 1.30/0.67 fof(f980,plain,(
% 1.30/0.67 xP=sdtmndt0(xQ,xp)),
% 1.30/0.67 inference(backward_demodulation,[status(thm)],[f446,f448])).
% 1.30/0.67 fof(f990,plain,(
% 1.30/0.67 ~aSet0(xQ)|~isFinite0(xQ)|isFinite0(xP)),
% 1.30/0.67 inference(resolution,[status(thm)],[f144,f451])).
% 1.30/0.67 fof(f996,plain,(
% 1.30/0.67 ~sQ31_spl|~sQ32_spl|sQ2_spl),
% 1.30/0.67 inference(split_clause,[status(thm)],[f990,f665,f668,f511])).
% 1.30/0.67 fof(f999,plain,(
% 1.30/0.67 ~szszuzczcdt0(sbrdtbr0(xP))=xK|~sQ44_spl|sQ0_spl),
% 1.30/0.67 inference(forward_demodulation,[status(thm)],[f757,f463])).
% 1.30/0.67 fof(f1003,plain,(
% 1.30/0.67 aSubsetOf0(xO,xO)),
% 1.30/0.67 inference(resolution,[status(thm)],[f146,f431])).
% 1.30/0.67 fof(f1004,plain,(
% 1.30/0.67 aSubsetOf0(xT,xT)),
% 1.30/0.67 inference(resolution,[status(thm)],[f146,f367])).
% 1.30/0.67 fof(f1005,plain,(
% 1.30/0.67 aSubsetOf0(szNzAzT0,szNzAzT0)),
% 1.30/0.67 inference(resolution,[status(thm)],[f146,f187])).
% 1.30/0.67 fof(f1006,plain,(
% 1.30/0.67 aSubsetOf0(xP,xP)),
% 1.30/0.67 inference(resolution,[status(thm)],[f146,f447])).
% 1.30/0.67 fof(f1244,definition,(
% 1.30/0.67 sQ103_spl <=> (aSubsetOf0(xP,xP))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f1246,plain,(
% 1.30/0.67 ~aSubsetOf0(xP,xP)|sQ103_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f1244])).
% 1.30/0.67 fof(f1313,definition,(
% 1.30/0.67 sQ112_spl <=> (aSubsetOf0(xO,xO))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f1315,plain,(
% 1.30/0.67 ~aSubsetOf0(xO,xO)|sQ112_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f1313])).
% 1.30/0.67 fof(f1326,plain,(
% 1.30/0.67 $false|sQ112_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f1315,f1003])).
% 1.30/0.67 fof(f1327,plain,(
% 1.30/0.67 sQ112_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f1326])).
% 1.30/0.67 fof(f1337,definition,(
% 1.30/0.67 sQ116_spl <=> (aSubsetOf0(xT,xT))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f1339,plain,(
% 1.30/0.67 ~aSubsetOf0(xT,xT)|sQ116_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f1337])).
% 1.30/0.67 fof(f1350,plain,(
% 1.30/0.67 $false|sQ116_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f1339,f1004])).
% 1.30/0.67 fof(f1351,plain,(
% 1.30/0.67 sQ116_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f1350])).
% 1.30/0.67 fof(f1361,definition,(
% 1.30/0.67 sQ120_spl <=> (aSubsetOf0(szNzAzT0,szNzAzT0))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f1363,plain,(
% 1.30/0.67 ~aSubsetOf0(szNzAzT0,szNzAzT0)|sQ120_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f1361])).
% 1.30/0.67 fof(f1374,plain,(
% 1.30/0.67 $false|sQ120_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f1363,f1005])).
% 1.30/0.67 fof(f1375,plain,(
% 1.30/0.67 sQ120_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f1374])).
% 1.30/0.67 fof(f1694,definition,(
% 1.30/0.67 sQ157_spl <=> (sdtlseqdt0(sz00,sz00))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f1696,plain,(
% 1.30/0.67 ~sdtlseqdt0(sz00,sz00)|sQ157_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f1694])).
% 1.30/0.67 fof(f1723,plain,(
% 1.30/0.67 aSet0(szDzozmdt0(xc))),
% 1.30/0.67 inference(resolution,[status(thm)],[f320,f372])).
% 1.30/0.67 fof(f1748,definition,(
% 1.30/0.67 sQ167_spl <=> (aElementOf0(sz00,szNzAzT0))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f1750,plain,(
% 1.30/0.67 ~aElementOf0(sz00,szNzAzT0)|sQ167_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f1748])).
% 1.30/0.67 fof(f1761,plain,(
% 1.30/0.67 $false|sQ103_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f1246,f1006])).
% 1.30/0.67 fof(f1762,plain,(
% 1.30/0.67 sQ103_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f1761])).
% 1.30/0.67 fof(f1772,definition,(
% 1.30/0.67 sQ172_spl <=> (aSet0(szDzozmdt0(xc)))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f1774,plain,(
% 1.30/0.67 ~aSet0(szDzozmdt0(xc))|sQ172_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f1772])).
% 1.30/0.67 fof(f1776,plain,(
% 1.30/0.67 $false|sQ172_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f1774,f1723])).
% 1.30/0.67 fof(f1777,plain,(
% 1.30/0.67 sQ172_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f1776])).
% 1.30/0.67 fof(f1868,plain,(
% 1.30/0.67 $false|sQ167_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f1750,f189])).
% 1.30/0.67 fof(f1869,plain,(
% 1.30/0.67 sQ167_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f1868])).
% 1.30/0.67 fof(f1872,plain,(
% 1.30/0.67 $false|sQ4_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f523,f128])).
% 1.30/0.67 fof(f1873,plain,(
% 1.30/0.67 sQ4_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f1872])).
% 1.30/0.67 fof(f2319,plain,(
% 1.30/0.67 $false|~sQ15_spl),
% 1.30/0.67 inference(backward_subsumption_resolution,[status(thm)],[f429,f789])).
% 1.30/0.67 fof(f2321,plain,(
% 1.30/0.67 ~sQ15_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f2319])).
% 1.30/0.67 fof(f2560,definition,(
% 1.30/0.67 sQ228_spl <=> (xK=sz00)),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f2561,plain,(
% 1.30/0.67 xK=sz00|~sQ228_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f2560])).
% 1.30/0.67 fof(f2585,plain,(
% 1.30/0.67 $false|~sQ228_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2561,f381])).
% 1.30/0.67 fof(f2586,plain,(
% 1.30/0.67 ~sQ228_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f2585])).
% 1.30/0.67 fof(f2706,definition,(
% 1.30/0.67 sQ249_spl <=> (szszuzczcdt0(sz00)=sz00)),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f2707,plain,(
% 1.30/0.67 szszuzczcdt0(sz00)=sz00|~sQ249_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f2706])).
% 1.30/0.67 fof(f2722,plain,(
% 1.30/0.67 $false|~sQ249_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2707,f793])).
% 1.30/0.67 fof(f2723,plain,(
% 1.30/0.67 ~sQ249_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f2722])).
% 1.30/0.67 fof(f2832,plain,(
% 1.30/0.67 sdtlseqdt0(sz00,sz00)),
% 1.30/0.67 inference(resolution,[status(thm)],[f204,f189])).
% 1.30/0.67 fof(f2853,plain,(
% 1.30/0.67 sdtlseqdt0(xk,xk)),
% 1.30/0.67 inference(resolution,[status(thm)],[f214,f383])).
% 1.30/0.67 fof(f2925,plain,(
% 1.30/0.67 $false|sQ157_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2832,f1696])).
% 1.30/0.67 fof(f2926,plain,(
% 1.30/0.67 sQ157_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f2925])).
% 1.30/0.67 fof(f3062,definition,(
% 1.30/0.67 sQ279_spl <=> (sdtlseqdt0(xk,xk))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ279_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f3064,plain,(
% 1.30/0.67 ~sdtlseqdt0(xk,xk)|sQ279_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f3062])).
% 1.30/0.67 fof(f3094,plain,(
% 1.30/0.67 $false|sQ279_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3064,f2853])).
% 1.30/0.67 fof(f3095,plain,(
% 1.30/0.67 sQ279_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f3094])).
% 1.30/0.67 fof(f3278,definition,(
% 1.30/0.67 sQ294_spl <=> (xQ=slcrc0)),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ294_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f3279,plain,(
% 1.30/0.67 xQ=slcrc0|~sQ294_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f3278])).
% 1.30/0.67 fof(f3282,plain,(
% 1.30/0.67 $false|~sQ294_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3279,f443])).
% 1.30/0.67 fof(f3283,plain,(
% 1.30/0.67 ~sQ294_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f3282])).
% 1.30/0.67 fof(f3503,plain,(
% 1.30/0.67 ~aSet0(xQ)|~isFinite0(xQ)|szszuzczcdt0(sbrdtbr0(sdtmndt0(xQ,xp)))=sbrdtbr0(xQ)),
% 1.30/0.67 inference(resolution,[status(thm)],[f238,f449])).
% 1.30/0.67 fof(f3577,definition,(
% 1.30/0.67 sQ334_spl <=> (szszuzczcdt0(sbrdtbr0(sdtmndt0(xQ,xp)))=sbrdtbr0(xQ))),
% 1.30/0.67 introduced(definition,[new_symbols(definition,[sQ334_spl])],[split_symbol_definition])).
% 1.30/0.67 fof(f3578,plain,(
% 1.30/0.67 szszuzczcdt0(sbrdtbr0(sdtmndt0(xQ,xp)))=sbrdtbr0(xQ)|~sQ334_spl),
% 1.30/0.67 inference(component_clause,[status(thm)],[f3577])).
% 1.30/0.67 fof(f3580,plain,(
% 1.30/0.67 ~sQ31_spl|~sQ32_spl|sQ334_spl),
% 1.30/0.67 inference(split_clause,[status(thm)],[f3503,f665,f668,f3577])).
% 1.30/0.67 fof(f3586,plain,(
% 1.30/0.67 szszuzczcdt0(sbrdtbr0(xP))=sbrdtbr0(xQ)|~sQ334_spl),
% 1.30/0.67 inference(forward_demodulation,[status(thm)],[f980,f3578])).
% 1.30/0.67 fof(f3587,plain,(
% 1.30/0.67 szszuzczcdt0(sbrdtbr0(xP))=xK|~sQ44_spl|~sQ334_spl),
% 1.30/0.67 inference(forward_demodulation,[status(thm)],[f757,f3586])).
% 1.30/0.67 fof(f3588,plain,(
% 1.30/0.67 $false|sQ0_spl|~sQ44_spl|~sQ334_spl),
% 1.30/0.67 inference(forward_subsumption_resolution,[status(thm)],[f3587,f999])).
% 1.30/0.67 fof(f3589,plain,(
% 1.30/0.67 sQ0_spl|~sQ44_spl|~sQ334_spl),
% 1.30/0.67 inference(contradiction_clause,[status(thm)],[f3588])).
% 1.30/0.67 fof(f3590,plain,(
% 1.30/0.67 $false),
% 1.30/0.67 inference(sat_refutation,[status(thm)],[f467,f514,f641,f684,f730,f759,f802,f870,f900,f972,f996,f1327,f1351,f1375,f1762,f1777,f1869,f1873,f2321,f2586,f2723,f2926,f3095,f3283,f3580,f3589])).
% 1.30/0.67 % SZS output end CNFRefutation for theBenchmark.p
% 1.30/0.69 % Elapsed time: 0.316214 seconds
% 1.30/0.69 % CPU time: 2.139605 seconds
% 1.30/0.69 % Total memory used: 140.015 MB
% 1.30/0.69 % Net memory used: 137.806 MB
%------------------------------------------------------------------------------