%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM611+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 : n002.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.42s 0.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM611+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.08/0.34 % Computer : n002.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Mon Sep 21 02:47:01 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 1.42/0.65 % Refutation found
% 1.42/0.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.42/0.65 % SZS output start CNFRefutation for theBenchmark
% 1.42/0.65 fof(f10,definition,(
% 1.42/0.65 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f11,axiom,(
% 1.42/0.65 (! [W0] :( ( aSet0(W0)& isFinite0(W0) )=> (! [W1] :( aSubsetOf0(W1,W0)=> isFinite0(W1) ) )) )),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f23,axiom,(
% 1.42/0.65 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f26,axiom,(
% 1.42/0.65 (! [W0,W1] :( ( aElementOf0(W0,szNzAzT0)& aElementOf0(W1,szNzAzT0) )=> ( szszuzczcdt0(W0) = szszuzczcdt0(W1)=> W0 = W1 ) ) )),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f41,axiom,(
% 1.42/0.65 (! [W0] :( aSet0(W0)=> ( aElementOf0(sbrdtbr0(W0),szNzAzT0)<=> isFinite0(W0) ) ) )),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f44,axiom,(
% 1.42/0.65 (! [W0] :( aSet0(W0)=> (! [W1] :( ( isFinite0(W0)& aElementOf0(W1,W0) )=> szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1))) = sbrdtbr0(W0) ) )) )),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f57,definition,(
% 1.42/0.65 (! [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.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f74,hypothesis,(
% 1.42/0.65 aElementOf0(xK,szNzAzT0) ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f75,hypothesis,(
% 1.42/0.65 ( aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f76,hypothesis,(
% 1.42/0.65 ( aFunction0(xc)& szDzozmdt0(xc) = slbdtsldtrb0(xS,xK)& aSubsetOf0(sdtlcdtrc0(xc,szDzozmdt0(xc)),xT) ) ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f80,hypothesis,(
% 1.42/0.65 ( aElementOf0(xk,szNzAzT0)& szszuzczcdt0(xk) = xK ) ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f95,hypothesis,(
% 1.42/0.65 ( aSet0(xO)& xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f100,hypothesis,(
% 1.42/0.65 ( aSubsetOf0(xQ,xO)& xQ != slcrc0 ) ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f102,hypothesis,(
% 1.42/0.65 aElementOf0(xQ,szDzozmdt0(xc)) ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f103,hypothesis,(
% 1.42/0.65 xp = szmzizndt0(xQ) ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f104,hypothesis,(
% 1.42/0.65 ( aSet0(xP)& xP = sdtmndt0(xQ,szmzizndt0(xQ)) ) ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f105,hypothesis,(
% 1.42/0.65 aElementOf0(xp,xQ) ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f107,hypothesis,(
% 1.42/0.65 aSubsetOf0(xP,xQ) ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f109,conjecture,(
% 1.42/0.65 sbrdtbr0(xP) = xk ),
% 1.42/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.42/0.65 fof(f110,negated_conjecture,(
% 1.42/0.65 ~(sbrdtbr0(xP) = xk )),
% 1.42/0.65 inference(negated_conjecture,[status(cth)],[f109])).
% 1.42/0.65 fof(f135,plain,(
% 1.42/0.65 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 1.42/0.65 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 1.42/0.65 fof(f136,plain,(
% 1.42/0.65 ![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.42/0.65 inference(NNF_transformation,[status(thm)],[f135])).
% 1.42/0.65 fof(f137,plain,(
% 1.42/0.65 ![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.42/0.65 inference(miniscoping,[status(thm)],[f136])).
% 1.42/0.65 fof(f138,plain,(
% 1.42/0.65 ![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.42/0.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f137])).
% 1.42/0.66 fof(f139,plain,(
% 1.42/0.66 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f138])).
% 1.42/0.66 fof(f143,plain,(
% 1.42/0.66 ![W0]: ((~aSet0(W0)|~isFinite0(W0))|(![W1]: (~aSubsetOf0(W1,W0)|isFinite0(W1))))),
% 1.42/0.66 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 1.42/0.66 fof(f144,plain,(
% 1.42/0.66 ![X0,X1]: (~aSet0(X0)|~isFinite0(X0)|~aSubsetOf0(X1,X0)|isFinite0(X1))),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f143])).
% 1.42/0.66 fof(f187,plain,(
% 1.42/0.66 aSet0(szNzAzT0)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f23])).
% 1.42/0.66 fof(f193,plain,(
% 1.42/0.66 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|(~szszuzczcdt0(W0)=szszuzczcdt0(W1)|W0=W1))),
% 1.42/0.66 inference(pre_NNF_transformation,[status(thm)],[f26])).
% 1.42/0.66 fof(f194,plain,(
% 1.42/0.66 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~szszuzczcdt0(X0)=szszuzczcdt0(X1)|X0=X1)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f193])).
% 1.42/0.66 fof(f227,plain,(
% 1.42/0.66 ![W0]: (~aSet0(W0)|(aElementOf0(sbrdtbr0(W0),szNzAzT0)<=>isFinite0(W0)))),
% 1.42/0.66 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 1.42/0.66 fof(f228,plain,(
% 1.42/0.66 ![W0]: (~aSet0(W0)|((~aElementOf0(sbrdtbr0(W0),szNzAzT0)|isFinite0(W0))&(aElementOf0(sbrdtbr0(W0),szNzAzT0)|~isFinite0(W0))))),
% 1.42/0.66 inference(NNF_transformation,[status(thm)],[f227])).
% 1.42/0.66 fof(f229,plain,(
% 1.42/0.66 ![X0]: (~aSet0(X0)|~aElementOf0(sbrdtbr0(X0),szNzAzT0)|isFinite0(X0))),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f228])).
% 1.42/0.66 fof(f230,plain,(
% 1.42/0.66 ![X0]: (~aSet0(X0)|aElementOf0(sbrdtbr0(X0),szNzAzT0)|~isFinite0(X0))),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f228])).
% 1.42/0.66 fof(f237,plain,(
% 1.42/0.66 ![W0]: (~aSet0(W0)|(![W1]: ((~isFinite0(W0)|~aElementOf0(W1,W0))|szszuzczcdt0(sbrdtbr0(sdtmndt0(W0,W1)))=sbrdtbr0(W0))))),
% 1.42/0.66 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 1.42/0.66 fof(f238,plain,(
% 1.42/0.66 ![X0,X1]: (~aSet0(X0)|~isFinite0(X0)|~aElementOf0(X1,X0)|szszuzczcdt0(sbrdtbr0(sdtmndt0(X0,X1)))=sbrdtbr0(X0))),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f237])).
% 1.42/0.66 fof(f292,plain,(
% 1.42/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.42/0.66 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 1.42/0.66 fof(f293,plain,(
% 1.42/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))&(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.42/0.66 inference(NNF_transformation,[status(thm)],[f292])).
% 1.42/0.66 fof(f294,plain,(
% 1.42/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)))&(![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.42/0.66 inference(miniscoping,[status(thm)],[f293])).
% 1.42/0.66 fof(f295,plain,(
% 1.42/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)))&(![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.42/0.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W3,sK10_skl(W2,W1,W0))],[f294])).
% 1.42/0.66 fof(f298,plain,(
% 1.42/0.66 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|~aElementOf0(X3,X2)|sbrdtbr0(X3)=X1)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f295])).
% 1.42/0.66 fof(f369,plain,(
% 1.42/0.66 aElementOf0(xK,szNzAzT0)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f74])).
% 1.42/0.66 fof(f370,plain,(
% 1.42/0.66 aSubsetOf0(xS,szNzAzT0)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f75])).
% 1.42/0.66 fof(f373,plain,(
% 1.42/0.66 szDzozmdt0(xc)=slbdtsldtrb0(xS,xK)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f76])).
% 1.42/0.66 fof(f383,plain,(
% 1.42/0.66 aElementOf0(xk,szNzAzT0)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f80])).
% 1.42/0.66 fof(f384,plain,(
% 1.42/0.66 szszuzczcdt0(xk)=xK),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f80])).
% 1.42/0.66 fof(f431,plain,(
% 1.42/0.66 aSet0(xO)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f95])).
% 1.42/0.66 fof(f442,plain,(
% 1.42/0.66 aSubsetOf0(xQ,xO)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f100])).
% 1.42/0.66 fof(f445,plain,(
% 1.42/0.66 aElementOf0(xQ,szDzozmdt0(xc))),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f102])).
% 1.42/0.66 fof(f446,plain,(
% 1.42/0.66 xp=szmzizndt0(xQ)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f103])).
% 1.42/0.66 fof(f447,plain,(
% 1.42/0.66 aSet0(xP)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f104])).
% 1.42/0.66 fof(f448,plain,(
% 1.42/0.66 xP=sdtmndt0(xQ,szmzizndt0(xQ))),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f104])).
% 1.42/0.66 fof(f449,plain,(
% 1.42/0.66 aElementOf0(xp,xQ)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f105])).
% 1.42/0.66 fof(f451,plain,(
% 1.42/0.66 aSubsetOf0(xP,xQ)),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f107])).
% 1.42/0.66 fof(f453,plain,(
% 1.42/0.66 ~sbrdtbr0(xP)=xk),
% 1.42/0.66 inference(cnf_transformation,[status(thm)],[f110])).
% 1.42/0.66 fof(f485,plain,(
% 1.42/0.66 ![X0,X1,X2]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~aElementOf0(X2,slbdtsldtrb0(X0,X1))|sbrdtbr0(X2)=X1)),
% 1.42/0.66 inference(destructive_equality_resolution,[status(thm)],[f298])).
% 1.42/0.66 fof(f505,plain,(
% 1.42/0.66 aElementOf0(sbrdtbr0(xP),szNzAzT0)|~isFinite0(xP)),
% 1.42/0.66 inference(resolution,[status(thm)],[f230,f447])).
% 1.42/0.66 fof(f587,plain,(
% 1.42/0.66 ~aSet0(szNzAzT0)|aSet0(xS)),
% 1.42/0.66 inference(resolution,[status(thm)],[f370,f139])).
% 1.42/0.66 fof(f589,plain,(
% 1.42/0.66 aSet0(xS)),
% 1.42/0.66 inference(forward_subsumption_resolution,[status(thm)],[f587,f187])).
% 1.42/0.66 fof(f670,plain,(
% 1.42/0.66 ~aSet0(xO)|aSet0(xQ)),
% 1.42/0.66 inference(resolution,[status(thm)],[f442,f139])).
% 1.42/0.66 fof(f672,plain,(
% 1.42/0.66 aSet0(xQ)),
% 1.42/0.66 inference(forward_subsumption_resolution,[status(thm)],[f670,f431])).
% 1.42/0.66 fof(f683,plain,(
% 1.42/0.66 xP=sdtmndt0(xQ,xp)),
% 1.42/0.66 inference(backward_demodulation,[status(thm)],[f446,f448])).
% 1.42/0.66 fof(f715,plain,(
% 1.42/0.66 ~aSet0(xQ)|~isFinite0(xQ)|isFinite0(xP)),
% 1.42/0.66 inference(resolution,[status(thm)],[f144,f451])).
% 1.42/0.66 fof(f716,plain,(
% 1.42/0.66 ~isFinite0(xQ)|isFinite0(xP)),
% 1.42/0.66 inference(forward_subsumption_resolution,[status(thm)],[f715,f672])).
% 1.42/0.66 fof(f1514,plain,(
% 1.42/0.66 ![X0]: (~aSet0(xS)|~aElementOf0(xK,szNzAzT0)|~aElementOf0(X0,szDzozmdt0(xc))|sbrdtbr0(X0)=xK)),
% 1.42/0.66 inference(paramodulation,[status(thm)],[f373,f485])).
% 1.42/0.66 fof(f1517,plain,(
% 1.42/0.66 ![X0]: (~aElementOf0(xK,szNzAzT0)|~aElementOf0(X0,szDzozmdt0(xc))|sbrdtbr0(X0)=xK)),
% 1.42/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1514,f589])).
% 1.42/0.66 fof(f1610,plain,(
% 1.42/0.66 ![X0]: (~aElementOf0(X0,szDzozmdt0(xc))|sbrdtbr0(X0)=xK)),
% 1.42/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1517,f369])).
% 1.42/0.66 fof(f1611,plain,(
% 1.42/0.66 sbrdtbr0(xQ)=xK),
% 1.42/0.66 inference(resolution,[status(thm)],[f1610,f445])).
% 1.42/0.66 fof(f1622,plain,(
% 1.42/0.66 ~aSet0(xQ)|~aElementOf0(xK,szNzAzT0)|isFinite0(xQ)),
% 1.42/0.66 inference(paramodulation,[status(thm)],[f1611,f229])).
% 1.42/0.66 fof(f1628,plain,(
% 1.42/0.66 ~aElementOf0(xK,szNzAzT0)|isFinite0(xQ)),
% 1.42/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1622,f672])).
% 1.42/0.66 fof(f2032,plain,(
% 1.42/0.66 isFinite0(xP)),
% 1.42/0.66 inference(backward_subsumption_resolution,[status(thm)],[f716,f2033])).
% 1.42/0.66 fof(f2033,plain,(
% 1.42/0.66 isFinite0(xQ)),
% 1.42/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1628,f369])).
% 1.42/0.66 fof(f2037,plain,(
% 1.42/0.66 aElementOf0(sbrdtbr0(xP),szNzAzT0)),
% 1.42/0.66 inference(backward_subsumption_resolution,[status(thm)],[f505,f2032])).
% 1.42/0.66 fof(f2501,plain,(
% 1.42/0.66 ![X0]: (~aElementOf0(xk,szNzAzT0)|~aElementOf0(X0,szNzAzT0)|~xK=szszuzczcdt0(X0)|xk=X0)),
% 1.42/0.66 inference(paramodulation,[status(thm)],[f384,f194])).
% 1.42/0.66 fof(f2504,plain,(
% 1.42/0.66 ![X0]: (~aElementOf0(X0,szNzAzT0)|~xK=szszuzczcdt0(X0)|xk=X0)),
% 1.42/0.66 inference(forward_subsumption_resolution,[status(thm)],[f2501,f383])).
% 1.42/0.66 fof(f2589,plain,(
% 1.42/0.66 ~xK=szszuzczcdt0(sbrdtbr0(xP))|xk=sbrdtbr0(xP)),
% 1.42/0.66 inference(resolution,[status(thm)],[f2504,f2037])).
% 1.42/0.67 fof(f2593,plain,(
% 1.42/0.67 ~xK=szszuzczcdt0(sbrdtbr0(xP))),
% 1.42/0.67 inference(forward_subsumption_resolution,[status(thm)],[f2589,f453])).
% 1.42/0.67 fof(f4022,plain,(
% 1.42/0.67 ~aSet0(xQ)|~isFinite0(xQ)|szszuzczcdt0(sbrdtbr0(sdtmndt0(xQ,xp)))=sbrdtbr0(xQ)),
% 1.42/0.67 inference(resolution,[status(thm)],[f238,f449])).
% 1.42/0.67 fof(f4047,plain,(
% 1.42/0.67 ~aSet0(xQ)|~isFinite0(xQ)|szszuzczcdt0(sbrdtbr0(xP))=sbrdtbr0(xQ)),
% 1.42/0.67 inference(forward_demodulation,[status(thm)],[f683,f4022])).
% 1.42/0.67 fof(f4048,plain,(
% 1.42/0.67 ~aSet0(xQ)|~isFinite0(xQ)|szszuzczcdt0(sbrdtbr0(xP))=xK),
% 1.42/0.67 inference(forward_demodulation,[status(thm)],[f1611,f4047])).
% 1.42/0.67 fof(f4049,plain,(
% 1.42/0.67 ~isFinite0(xQ)|szszuzczcdt0(sbrdtbr0(xP))=xK),
% 1.42/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4048,f672])).
% 1.42/0.67 fof(f4310,plain,(
% 1.42/0.67 ~xK=xK),
% 1.42/0.67 inference(backward_demodulation,[status(thm)],[f4312,f2593])).
% 1.42/0.67 fof(f4312,plain,(
% 1.42/0.67 szszuzczcdt0(sbrdtbr0(xP))=xK),
% 1.42/0.67 inference(forward_subsumption_resolution,[status(thm)],[f4049,f2033])).
% 1.42/0.67 fof(f4320,plain,(
% 1.42/0.67 $false),
% 1.42/0.67 inference(trivial_equality_resolution,[status(thm)],[f4310])).
% 1.42/0.67 % SZS output end CNFRefutation for theBenchmark.p
% 1.42/0.67 % Elapsed time: 0.324190 seconds
% 1.42/0.67 % CPU time: 2.292961 seconds
% 1.42/0.67 % Total memory used: 149.180 MB
% 1.42/0.67 % Net memory used: 146.142 MB
%------------------------------------------------------------------------------