%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM629+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 : n020.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:23 PM UTC 2026
% Result : Theorem 165.87s 21.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM629+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.09/0.36 % Computer : n020.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 02:46:32 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.42 % Drodi V4.1.1
% 165.87/21.56 % Refutation found
% 165.87/21.56 % SZS status Theorem for theBenchmark: Theorem is valid
% 165.87/21.56 % SZS output start CNFRefutation for theBenchmark
% 165.87/21.56 fof(f3,axiom,(
% 165.87/21.56 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f10,definition,(
% 165.87/21.56 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f14,axiom,(
% 165.87/21.56 (! [W0,W1,W2] :( ( aSet0(W0)& aSet0(W1)& aSet0(W2) )=> ( ( aSubsetOf0(W0,W1)& aSubsetOf0(W1,W2) )=> aSubsetOf0(W0,W2) ) ) )),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f16,definition,(
% 165.87/21.56 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtmndt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& aElementOf0(W3,W0)& W3 != W1 ) ) )) ) )) )),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f23,axiom,(
% 165.87/21.56 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f57,definition,(
% 165.87/21.56 (! [W0,W1] :( ( aSet0(W0)& aElementOf0(W1,szNzAzT0) )=> (! [W2] :( W2 = slbdtsldtrb0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aSubsetOf0(W3,W0)& sbrdtbr0(W3) = W1 ) ) )) ) )) )),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f80,hypothesis,(
% 165.87/21.56 ( aElementOf0(xk,szNzAzT0)& szszuzczcdt0(xk) = xK ) ),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f81,hypothesis,(
% 165.87/21.56 ( aFunction0(xN)& szDzozmdt0(xN) = szNzAzT0& sdtlpdtrp0(xN,sz00) = xS& (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)& isCountable0(sdtlpdtrp0(xN,W0)) )=> ( aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0))) ) ) ) )) ),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f82,hypothesis,(
% 165.87/21.56 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)& isCountable0(sdtlpdtrp0(xN,W0)) ) ) )),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f91,hypothesis,(
% 165.87/21.56 ( aFunction0(xe)& szDzozmdt0(xe) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0)) ) )) ),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f95,hypothesis,(
% 165.87/21.56 ( aSet0(xO)& xO = sdtlcdtrc0(xe,sdtlbdtrb0(xd,szDzizrdt0(xd))) ) ),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f100,hypothesis,(
% 165.87/21.56 ( aSubsetOf0(xQ,xO)& xQ != slcrc0 ) ),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f105,hypothesis,(
% 165.87/21.56 aElementOf0(xp,xQ) ),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f109,hypothesis,(
% 165.87/21.56 sbrdtbr0(xP) = xk ),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f111,hypothesis,(
% 165.87/21.56 ( aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))& aElementOf0(xn,szNzAzT0)& sdtlpdtrp0(xe,xn) = xp ) ),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f113,hypothesis,(
% 165.87/21.56 aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f114,hypothesis,(
% 165.87/21.56 xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))) ),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f115,conjecture,(
% 165.87/21.56 aElementOf0(xP,slbdtsldtrb0(xD,xk)) ),
% 165.87/21.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 165.87/21.56 fof(f116,negated_conjecture,(
% 165.87/21.56 ~(aElementOf0(xP,slbdtsldtrb0(xD,xk)) )),
% 165.87/21.56 inference(negated_conjecture,[status(cth)],[f115])).
% 165.87/21.56 fof(f123,plain,(
% 165.87/21.56 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 165.87/21.56 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 165.87/21.56 fof(f124,plain,(
% 165.87/21.56 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f123])).
% 165.87/21.56 fof(f141,plain,(
% 165.87/21.56 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 165.87/21.56 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 165.87/21.56 fof(f142,plain,(
% 165.87/21.56 ![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))))))))),
% 165.87/21.56 inference(NNF_transformation,[status(thm)],[f141])).
% 165.87/21.56 fof(f143,plain,(
% 165.87/21.56 ![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))))))))),
% 165.87/21.56 inference(miniscoping,[status(thm)],[f142])).
% 165.87/21.56 fof(f144,plain,(
% 165.87/21.56 ![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)))))))),
% 165.87/21.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f143])).
% 165.87/21.56 fof(f145,plain,(
% 165.87/21.56 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f144])).
% 165.87/21.56 fof(f155,plain,(
% 165.87/21.56 ![W0,W1,W2]: (((~aSet0(W0)|~aSet0(W1))|~aSet0(W2))|((~aSubsetOf0(W0,W1)|~aSubsetOf0(W1,W2))|aSubsetOf0(W0,W2)))),
% 165.87/21.56 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 165.87/21.56 fof(f156,plain,(
% 165.87/21.56 ![X0,X1,X2]: (~aSet0(X0)|~aSet0(X1)|~aSet0(X2)|~aSubsetOf0(X0,X1)|~aSubsetOf0(X1,X2)|aSubsetOf0(X0,X2))),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f155])).
% 165.87/21.56 fof(f170,plain,(
% 165.87/21.56 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1)))))))),
% 165.87/21.56 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 165.87/21.56 fof(f171,definition,(
% 165.87/21.56 ![W0,W1,W3]: (sP0_prd(W3,W1,W0)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1))),
% 165.87/21.56 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 165.87/21.56 fof(f172,plain,(
% 165.87/21.56 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>sP0_prd(W3,W1,W0)))))))),
% 165.87/21.56 inference(formula_renaming,[status(thm)],[f170,f171])).
% 165.87/21.56 fof(f173,plain,(
% 165.87/21.56 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: ((~W2=sdtmndt0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|sP0_prd(W3,W1,W0))&(aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0))))))&(W2=sdtmndt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0))&(aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))))))))),
% 165.87/21.56 inference(NNF_transformation,[status(thm)],[f172])).
% 165.87/21.56 fof(f174,plain,(
% 165.87/21.56 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtmndt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))&(![W3]: (aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0)))))))&(![W2]: (W2=sdtmndt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0))&(aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))))))))),
% 165.87/21.56 inference(miniscoping,[status(thm)],[f173])).
% 165.87/21.56 fof(f175,plain,(
% 165.87/21.56 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtmndt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|sP0_prd(W3,W1,W0)))&(![W3]: (aElementOf0(W3,W2)|~sP0_prd(W3,W1,W0)))))))&(![W2]: (W2=sdtmndt0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK3_skl(W2,W1,W0),W2)|~sP0_prd(sK3_skl(W2,W1,W0),W1,W0))&(aElementOf0(sK3_skl(W2,W1,W0),W2)|sP0_prd(sK3_skl(W2,W1,W0),W1,W0))))))))),
% 165.87/21.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W3,sK3_skl(W2,W1,W0))],[f174])).
% 165.87/21.56 fof(f176,plain,(
% 165.87/21.56 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtmndt0(X0,X1)|aSet0(X2))),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f175])).
% 165.87/21.56 fof(f193,plain,(
% 165.87/21.56 aSet0(szNzAzT0)),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f23])).
% 165.87/21.56 fof(f298,plain,(
% 165.87/21.56 ![W0,W1]: ((~aSet0(W0)|~aElementOf0(W1,szNzAzT0))|(![W2]: (W2=slbdtsldtrb0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aSubsetOf0(W3,W0)&sbrdtbr0(W3)=W1)))))))),
% 165.87/21.56 inference(pre_NNF_transformation,[status(thm)],[f57])).
% 165.87/21.56 fof(f299,plain,(
% 165.87/21.56 ![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)))))))))),
% 165.87/21.56 inference(NNF_transformation,[status(thm)],[f298])).
% 165.87/21.56 fof(f300,plain,(
% 165.87/21.56 ![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)))))))))),
% 165.87/21.56 inference(miniscoping,[status(thm)],[f299])).
% 165.87/21.56 fof(f301,plain,(
% 165.87/21.56 ![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))))))))),
% 165.87/21.56 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(W3,sK10_skl(W2,W1,W0))],[f300])).
% 165.87/21.56 fof(f305,plain,(
% 165.87/21.56 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElementOf0(X1,szNzAzT0)|~X2=slbdtsldtrb0(X0,X1)|aElementOf0(X3,X2)|~aSubsetOf0(X3,X0)|~sbrdtbr0(X3)=X1)),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f301])).
% 165.87/21.56 fof(f389,plain,(
% 165.87/21.56 aElementOf0(xk,szNzAzT0)),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f80])).
% 165.87/21.56 fof(f391,plain,(
% 165.87/21.56 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|((~aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)|~isCountable0(sdtlpdtrp0(xN,W0)))|(aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 165.87/21.56 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 165.87/21.56 fof(f395,plain,(
% 165.87/21.56 ![X0]: (~aElementOf0(X0,szNzAzT0)|~aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)|~isCountable0(sdtlpdtrp0(xN,X0))|aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))))),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f391])).
% 165.87/21.56 fof(f397,plain,(
% 165.87/21.56 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)&isCountable0(sdtlpdtrp0(xN,W0))))),
% 165.87/21.56 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 165.87/21.56 fof(f398,plain,(
% 165.87/21.56 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0))),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f397])).
% 165.87/21.56 fof(f399,plain,(
% 165.87/21.56 ![X0]: (~aElementOf0(X0,szNzAzT0)|isCountable0(sdtlpdtrp0(xN,X0)))),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f397])).
% 165.87/21.56 fof(f426,plain,(
% 165.87/21.56 (aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlpdtrp0(xe,W0)=szmzizndt0(sdtlpdtrp0(xN,W0))))),
% 165.87/21.56 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 165.87/21.56 fof(f429,plain,(
% 165.87/21.56 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlpdtrp0(xe,X0)=szmzizndt0(sdtlpdtrp0(xN,X0)))),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f426])).
% 165.87/21.56 fof(f437,plain,(
% 165.87/21.56 aSet0(xO)),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f95])).
% 165.87/21.56 fof(f448,plain,(
% 165.87/21.56 aSubsetOf0(xQ,xO)),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f100])).
% 165.87/21.56 fof(f455,plain,(
% 165.87/21.56 aElementOf0(xp,xQ)),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f105])).
% 165.87/21.56 fof(f459,plain,(
% 165.87/21.56 sbrdtbr0(xP)=xk),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f109])).
% 165.87/21.56 fof(f462,plain,(
% 165.87/21.56 aElementOf0(xn,szNzAzT0)),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f111])).
% 165.87/21.56 fof(f463,plain,(
% 165.87/21.56 sdtlpdtrp0(xe,xn)=xp),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f111])).
% 165.87/21.56 fof(f465,plain,(
% 165.87/21.56 aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f113])).
% 165.87/21.56 fof(f466,plain,(
% 165.87/21.56 xD=sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f114])).
% 165.87/21.56 fof(f467,plain,(
% 165.87/21.56 ~aElementOf0(xP,slbdtsldtrb0(xD,xk))),
% 165.87/21.56 inference(cnf_transformation,[status(thm)],[f116])).
% 165.87/21.56 fof(f483,plain,(
% 165.87/21.56 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aSet0(sdtmndt0(X0,X1)))),
% 165.87/21.56 inference(destructive_equality_resolution,[status(thm)],[f176])).
% 165.87/21.56 fof(f500,plain,(
% 165.87/21.56 ![X0,X1]: (~aSet0(X0)|~aElementOf0(sbrdtbr0(X1),szNzAzT0)|aElementOf0(X1,slbdtsldtrb0(X0,sbrdtbr0(X1)))|~aSubsetOf0(X1,X0))),
% 165.87/21.56 inference(destructive_equality_resolution,[status(thm)],[f305])).
% 165.87/21.56 fof(f569,plain,(
% 165.87/21.56 ![X0,X1,X2]: (~aSet0(X0)|~aSet0(X1)|~aSubsetOf0(X2,X0)|~aSubsetOf0(X0,X1)|aSubsetOf0(X2,X1))),
% 165.87/21.56 inference(forward_subsumption_resolution,[status(thm)],[f156,f145])).
% 165.87/21.56 fof(f623,plain,(
% 165.87/21.56 ~aSet0(sdtlpdtrp0(xN,xn))|~aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))|aSet0(xD)),
% 165.87/21.56 inference(paramodulation,[status(thm)],[f466,f483])).
% 165.87/21.56 fof(f1171,plain,(
% 165.87/21.56 ~aSet0(xO)|aSet0(xQ)),
% 165.87/21.56 inference(resolution,[status(thm)],[f448,f145])).
% 165.87/21.56 fof(f1175,plain,(
% 165.87/21.56 aSet0(xQ)),
% 165.87/21.56 inference(forward_subsumption_resolution,[status(thm)],[f1171,f437])).
% 165.87/21.56 fof(f1287,plain,(
% 165.87/21.56 ~aSet0(xQ)|aElement0(xp)),
% 165.87/21.56 inference(resolution,[status(thm)],[f455,f124])).
% 165.87/21.56 fof(f1288,plain,(
% 165.87/21.56 aElement0(xp)),
% 165.87/21.56 inference(forward_subsumption_resolution,[status(thm)],[f1287,f1175])).
% 165.87/21.56 fof(f1544,plain,(
% 165.87/21.56 ![X0]: (~aSet0(X0)|~aElementOf0(xk,szNzAzT0)|aElementOf0(xP,slbdtsldtrb0(X0,sbrdtbr0(xP)))|~aSubsetOf0(xP,X0))),
% 165.87/21.56 inference(paramodulation,[status(thm)],[f459,f500])).
% 165.87/21.56 fof(f1547,plain,(
% 165.87/21.56 ![X0]: (~aSet0(X0)|~aElementOf0(xk,szNzAzT0)|aElementOf0(xP,slbdtsldtrb0(X0,xk))|~aSubsetOf0(xP,X0))),
% 165.87/21.56 inference(forward_demodulation,[status(thm)],[f459,f1544])).
% 165.87/21.56 fof(f1548,plain,(
% 165.87/21.56 ![X0]: (~aSet0(X0)|aElementOf0(xP,slbdtsldtrb0(X0,xk))|~aSubsetOf0(xP,X0))),
% 165.87/21.56 inference(forward_subsumption_resolution,[status(thm)],[f1547,f389])).
% 165.87/21.56 fof(f1627,plain,(
% 165.87/21.56 ~aSet0(xD)|~aSubsetOf0(xP,xD)),
% 165.87/21.56 inference(resolution,[status(thm)],[f1548,f467])).
% 165.87/21.56 fof(f2701,plain,(
% 165.87/21.56 ![X0]: (~aElementOf0(X0,szNzAzT0)|~isCountable0(sdtlpdtrp0(xN,X0))|aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))))),
% 165.87/21.56 inference(backward_subsumption_resolution,[status(thm)],[f395,f398])).
% 165.87/21.56 fof(f2709,plain,(
% 165.87/21.56 ![X0]: (~aElementOf0(X0,szNzAzT0)|~aSet0(szNzAzT0)|aSet0(sdtlpdtrp0(xN,X0)))),
% 165.87/21.56 inference(resolution,[status(thm)],[f398,f145])).
% 165.87/21.56 fof(f2714,plain,(
% 165.87/21.56 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSet0(sdtlpdtrp0(xN,X0)))),
% 165.87/21.56 inference(forward_subsumption_resolution,[status(thm)],[f2709,f193])).
% 165.87/21.56 fof(f3158,plain,(
% 165.87/21.56 sdtlpdtrp0(xe,xn)=szmzizndt0(sdtlpdtrp0(xN,xn))),
% 165.87/21.56 inference(resolution,[status(thm)],[f429,f462])).
% 165.87/21.56 fof(f3172,plain,(
% 165.87/21.56 xp=szmzizndt0(sdtlpdtrp0(xN,xn))),
% 165.87/21.56 inference(forward_demodulation,[status(thm)],[f463,f3158])).
% 165.87/21.56 fof(f3507,plain,(
% 165.87/21.56 ![X0]: (~aSet0(sdtlpdtrp0(xN,szszuzczcdt0(xn)))|~aSet0(X0)|~aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),X0)|aSubsetOf0(xP,X0))),
% 165.87/21.56 inference(resolution,[status(thm)],[f465,f569])).
% 165.87/21.56 fof(f3511,plain,(
% 165.87/21.56 ![X0]: (~aSet0(X0)|~aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),X0)|aSubsetOf0(xP,X0))),
% 165.87/21.56 inference(forward_subsumption_resolution,[status(thm)],[f3507,f145])).
% 165.87/21.56 fof(f3633,plain,(
% 165.87/21.56 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(X0)),sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))))),
% 165.87/21.56 inference(forward_subsumption_resolution,[status(thm)],[f2701,f399])).
% 165.87/21.56 fof(f3643,plain,(
% 165.87/21.56 ~aElementOf0(xn,szNzAzT0)|aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xD)),
% 165.87/21.56 inference(paramodulation,[status(thm)],[f466,f3633])).
% 165.87/21.56 fof(f3655,plain,(
% 165.87/21.56 aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xD)),
% 165.87/21.56 inference(forward_subsumption_resolution,[status(thm)],[f3643,f462])).
% 165.87/21.56 fof(f21849,plain,(
% 165.87/21.56 aSet0(sdtlpdtrp0(xN,xn))),
% 165.87/21.56 inference(resolution,[status(thm)],[f2714,f462])).
% 165.87/21.56 fof(f22226,plain,(
% 165.87/21.56 ~aElement0(szmzizndt0(sdtlpdtrp0(xN,xn)))|aSet0(xD)),
% 165.87/21.56 inference(backward_subsumption_resolution,[status(thm)],[f623,f21849])).
% 165.87/21.56 fof(f23684,plain,(
% 165.87/21.56 ~aElement0(xp)|aSet0(xD)),
% 165.87/21.56 inference(backward_demodulation,[status(thm)],[f3172,f22226])).
% 165.87/21.56 fof(f23721,plain,(
% 165.87/21.56 aSet0(xD)),
% 165.87/21.56 inference(forward_subsumption_resolution,[status(thm)],[f23684,f1288])).
% 165.87/21.56 fof(f23944,plain,(
% 165.87/21.56 ~aSubsetOf0(xP,xD)),
% 165.87/21.56 inference(backward_subsumption_resolution,[status(thm)],[f1627,f23721])).
% 165.87/21.56 fof(f24890,plain,(
% 165.87/21.56 ~aSet0(xD)|aSubsetOf0(xP,xD)),
% 165.87/21.56 inference(resolution,[status(thm)],[f3511,f3655])).
% 93.32/21.68 fof(f24897,plain,(
% 93.32/21.68 aSubsetOf0(xP,xD)),
% 93.32/21.68 inference(forward_subsumption_resolution,[status(thm)],[f24890,f23721])).
% 93.32/21.68 fof(f24972,plain,(
% 93.32/21.68 $false),
% 93.32/21.68 inference(forward_subsumption_resolution,[status(thm)],[f24897,f23944])).
% 93.32/21.68 % SZS output end CNFRefutation for theBenchmark.p
% 77.42/21.72 % Elapsed time: 21.319530 seconds
% 77.42/21.72 % CPU time: 167.752348 seconds
% 77.42/21.72 % Total memory used: 716.460 MB
% 77.42/21.72 % Net memory used: 668.227 MB
%------------------------------------------------------------------------------