%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM621+3 : 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 : n008.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:22 PM UTC 2026
% Result : Theorem 20.69s 3.13s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM621+3 : 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.37 % Computer : n008.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Mon Sep 21 02:45:54 UTC 2026
% 0.08/0.38 % CPUTime :
% 0.08/0.46 % Drodi V4.1.1
% 20.69/3.13 % Refutation found
% 20.69/3.13 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.69/3.13 % SZS output start CNFRefutation for theBenchmark
% 20.69/3.13 fof(f35,axiom,(
% 20.69/3.13 (! [W0,W1] :( ( aElementOf0(W0,szNzAzT0)& aElementOf0(W1,szNzAzT0) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W1,W0) )=> W0 = W1 ) ) )),
% 20.69/3.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.69/3.13 fof(f82,hypothesis,(
% 20.69/3.13 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aSet0(sdtlpdtrp0(xN,W0))& (! [W1] :( aElementOf0(W1,sdtlpdtrp0(xN,W0))=> aElementOf0(W1,szNzAzT0) ))& aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)& isCountable0(sdtlpdtrp0(xN,W0)) ) ) )),
% 20.69/3.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.69/3.13 fof(f86,hypothesis,(
% 20.69/3.13 ( aFunction0(xC)& szDzozmdt0(xC) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aFunction0(sdtlpdtrp0(xC,W0))& aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))& (! [W1] :( aElementOf0(W1,sdtlpdtrp0(xN,W0))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1) ))& aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& (! [W1] :( aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=> ( aElement0(W1)& aElementOf0(W1,sdtlpdtrp0(xN,W0))& W1 != szmzizndt0(sdtlpdtrp0(xN,W0)) ) ))& (! [W1] :( ( aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ))& aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& sbrdtbr0(W1) = xk ) )& ( ( ( ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ))| aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )& sbrdtbr0(W1) = xk )=> aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0))) ) ))& szDzozmdt0(sdtlpdtrp0(xC,W0)) = slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)& (! [W1] :( ( aSet0(W1)& ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))& (! [W2] :( aElementOf0(W2,sdtlpdtrp0(xN,W0))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2) ) ))=> ( ( aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& (! [W2] :( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=> ( aElement0(W2)& aElementOf0(W2,sdtlpdtrp0(xN,W0))& W2 != szmzizndt0(sdtlpdtrp0(xN,W0)) ) ) ))=> ( ( ( (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ))| aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) )& sbrdtbr0(W1) = xk )| aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk)) ) ) ) )=> ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))& (! [W2] :( aElementOf0(W2,sdtlpdtrp0(xN,W0))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2) ))& (! [W2] :( aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))<=> ( aElement0(W2)& ( aElementOf0(W2,W1)| W2 = szmzizndt0(sdtlpdtrp0(xN,W0)) ) ) ))& sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1) = sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0)))) ) ) )) ) )) ),
% 20.69/3.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.69/3.13 fof(f91,hypothesis,(
% 20.69/3.13 ( aFunction0(xe)& szDzozmdt0(xe) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aElementOf0(sdtlpdtrp0(xe,W0),sdtlpdtrp0(xN,W0))& (! [W1] :( aElementOf0(W1,sdtlpdtrp0(xN,W0))=> sdtlseqdt0(sdtlpdtrp0(xe,W0),W1) ))& sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0)) ) ) )) ),
% 20.69/3.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.69/3.13 fof(f103,hypothesis,(
% 20.69/3.13 ( aElementOf0(xp,xQ)& (! [W0] :( aElementOf0(W0,xQ)=> sdtlseqdt0(xp,W0) ))& xp = szmzizndt0(xQ) ) ),
% 20.69/3.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.69/3.13 fof(f111,hypothesis,(
% 20.69/3.13 ( aElementOf0(xn,szDzozmdt0(xd))& sdtlpdtrp0(xd,xn) = szDzizrdt0(xd)& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))& aElementOf0(xn,szNzAzT0)& sdtlpdtrp0(xe,xn) = xp ) ),
% 20.69/3.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.69/3.13 fof(f113,hypothesis,(
% 20.69/3.13 ( aElement0(xx)& aElementOf0(xx,xQ)& xx != szmzizndt0(xQ)& aElementOf0(xx,xP) ) ),
% 20.69/3.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.69/3.13 fof(f114,hypothesis,(
% 20.69/3.13 ( aElementOf0(xx,szNzAzT0)& (? [W0] :( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))& sdtlpdtrp0(xe,W0) = xx ) )) ),
% 20.69/3.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.69/3.13 fof(f115,hypothesis,(
% 20.69/3.13 ( aElementOf0(xm,szNzAzT0)& xx = sdtlpdtrp0(xe,xm) ) ),
% 20.69/3.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.69/3.13 fof(f118,conjecture,(
% 20.69/3.13 ( ( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xn))=> aElementOf0(W0,sdtlpdtrp0(xN,xm)) ))& aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)) )=> aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ) ),
% 20.69/3.13 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.69/3.13 fof(f119,negated_conjecture,(
% 20.69/3.13 ~(( ( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xn))=> aElementOf0(W0,sdtlpdtrp0(xN,xm)) ))& aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)) )=> aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ) )),
% 20.69/3.13 inference(negated_conjecture,[status(cth)],[f118])).
% 20.69/3.13 fof(f224,plain,(
% 20.69/3.13 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W0))|W0=W1))),
% 20.69/3.13 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 20.69/3.13 fof(f225,plain,(
% 20.69/3.13 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,X0)|X0=X1)),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f224])).
% 20.69/3.13 fof(f435,plain,(
% 20.69/3.13 ![W0]: (~aElementOf0(W0,szNzAzT0)|(((aSet0(sdtlpdtrp0(xN,W0))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|aElementOf0(W1,szNzAzT0))))&aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0))&isCountable0(sdtlpdtrp0(xN,W0))))),
% 20.69/3.13 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 20.69/3.13 fof(f437,plain,(
% 20.69/3.13 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,sdtlpdtrp0(xN,X0))|aElementOf0(X1,szNzAzT0))),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f435])).
% 20.69/3.13 fof(f466,plain,(
% 20.69/3.13 (aFunction0(xC)&szDzozmdt0(xC)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(((((((aFunction0(sdtlpdtrp0(xC,W0))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: (aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=>((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0))))))&(![W1]: ((~aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&sbrdtbr0(W1)=xk))&((((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))|~sbrdtbr0(W1)=xk)|aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))))))&szDzozmdt0(sdtlpdtrp0(xC,W0))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))&(![W1]: ((~aSet0(W1)|((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2))))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))&(![W2]: (aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=>((aElement0(W2)&aElementOf0(W2,sdtlpdtrp0(xN,W0)))&~W2=szmzizndt0(sdtlpdtrp0(xN,W0))))))&((((?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))|~sbrdtbr0(W1)=xk)&~aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))))))|(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2))))&(![W2]: (aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))<=>(aElement0(W2)&(aElementOf0(W2,W1)|W2=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)=sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))))))))),
% 20.69/3.13 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 20.69/3.13 fof(f467,definition,(
% 20.69/3.13 ![W0,W1]: (sP6_prd(W1,W0)<=>((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2))))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))&(![W2]: (aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=>((aElement0(W2)&aElementOf0(W2,sdtlpdtrp0(xN,W0)))&~W2=szmzizndt0(sdtlpdtrp0(xN,W0))))))&((((?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))|~sbrdtbr0(W1)=xk)&~aElementOf0(W1,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))))))),
% 20.69/3.13 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 20.69/3.13 fof(f468,plain,(
% 20.69/3.13 (aFunction0(xC)&szDzozmdt0(xC)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(((((((aFunction0(sdtlpdtrp0(xC,W0))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: (aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))<=>((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0))))))&(![W1]: ((~aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&sbrdtbr0(W1)=xk))&((((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))|~sbrdtbr0(W1)=xk)|aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))))))&szDzozmdt0(sdtlpdtrp0(xC,W0))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))&(![W1]: ((~aSet0(W1)|sP6_prd(W1,W0))|(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2))))&(![W2]: (aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))<=>(aElement0(W2)&(aElementOf0(W2,W1)|W2=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)=sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))))))))),
% 20.69/3.13 inference(formula_renaming,[status(thm)],[f466,f467])).
% 20.69/3.13 fof(f469,plain,(
% 20.69/3.13 (aFunction0(xC)&szDzozmdt0(xC)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(((((((aFunction0(sdtlpdtrp0(xC,W0))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: ((~aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0))))&(aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((~aElement0(W1)|~aElementOf0(W1,sdtlpdtrp0(xN,W0)))|W1=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&(![W1]: ((~aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&sbrdtbr0(W1)=xk))&((((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))|~sbrdtbr0(W1)=xk)|aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))))))&szDzozmdt0(sdtlpdtrp0(xC,W0))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))&(![W1]: ((~aSet0(W1)|sP6_prd(W1,W0))|(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2))))&(![W2]: ((~aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))|(aElement0(W2)&(aElementOf0(W2,W1)|W2=szmzizndt0(sdtlpdtrp0(xN,W0)))))&(aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))|(~aElement0(W2)|(~aElementOf0(W2,W1)&~W2=szmzizndt0(sdtlpdtrp0(xN,W0))))))))&sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)=sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))))))))),
% 20.69/3.13 inference(NNF_transformation,[status(thm)],[f468])).
% 20.69/3.13 fof(f470,plain,(
% 20.69/3.13 (aFunction0(xC)&szDzozmdt0(xC)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(((((((aFunction0(sdtlpdtrp0(xC,W0))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&((![W1]: (~aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: (aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((~aElement0(W1)|~aElementOf0(W1,sdtlpdtrp0(xN,W0)))|W1=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&((![W1]: (~aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&sbrdtbr0(W1)=xk)))&(![W1]: ((((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))|~sbrdtbr0(W1)=xk)|aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))))))&szDzozmdt0(sdtlpdtrp0(xC,W0))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))&(![W1]: ((~aSet0(W1)|sP6_prd(W1,W0))|(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2))))&((![W2]: (~aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))|(aElement0(W2)&(aElementOf0(W2,W1)|W2=szmzizndt0(sdtlpdtrp0(xN,W0))))))&(![W2]: (aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))|(~aElement0(W2)|(~aElementOf0(W2,W1)&~W2=szmzizndt0(sdtlpdtrp0(xN,W0))))))))&sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)=sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))))))))),
% 20.69/3.13 inference(miniscoping,[status(thm)],[f469])).
% 20.69/3.13 fof(f471,plain,(
% 20.69/3.13 (aFunction0(xC)&szDzozmdt0(xC)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(((((((aFunction0(sdtlpdtrp0(xC,W0))&aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0)))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W1))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&((![W1]: (~aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((aElement0(W1)&aElementOf0(W1,sdtlpdtrp0(xN,W0)))&~W1=szmzizndt0(sdtlpdtrp0(xN,W0)))))&(![W1]: (aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))|((~aElement0(W1)|~aElementOf0(W1,sdtlpdtrp0(xN,W0)))|W1=szmzizndt0(sdtlpdtrp0(xN,W0)))))))&((![W1]: (~aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&sbrdtbr0(W1)=xk)))&(![W1]: ((((~aSet0(W1)|(aElementOf0(sK24_skl(W1,W0),W1)&~aElementOf0(sK24_skl(W1,W0),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))|~sbrdtbr0(W1)=xk)|aElementOf0(W1,szDzozmdt0(sdtlpdtrp0(xC,W0)))))))&szDzozmdt0(sdtlpdtrp0(xC,W0))=slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))),xk))&(![W1]: ((~aSet0(W1)|sP6_prd(W1,W0))|(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,W0)),sdtlpdtrp0(xN,W0))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,W0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,W0)),W2))))&((![W2]: (~aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))|(aElement0(W2)&(aElementOf0(W2,W1)|W2=szmzizndt0(sdtlpdtrp0(xN,W0))))))&(![W2]: (aElementOf0(W2,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))|(~aElement0(W2)|(~aElementOf0(W2,W1)&~W2=szmzizndt0(sdtlpdtrp0(xN,W0))))))))&sdtlpdtrp0(sdtlpdtrp0(xC,W0),W1)=sdtlpdtrp0(xc,sdtpldt0(W1,szmzizndt0(sdtlpdtrp0(xN,W0))))))))))),
% 20.69/3.13 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W2,sK24_skl(W1,W0))],[f470])).
% 20.69/3.13 fof(f476,plain,(
% 20.69/3.13 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,sdtlpdtrp0(xN,X0))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,X0)),X1))),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f471])).
% 20.69/3.13 fof(f551,plain,(
% 20.69/3.13 (aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|((aElementOf0(sdtlpdtrp0(xe,W0),sdtlpdtrp0(xN,W0))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(sdtlpdtrp0(xe,W0),W1))))&sdtlpdtrp0(xe,W0)=szmzizndt0(sdtlpdtrp0(xN,W0)))))),
% 20.69/3.13 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 20.69/3.13 fof(f554,plain,(
% 20.69/3.13 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(sdtlpdtrp0(xe,X0),sdtlpdtrp0(xN,X0)))),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f551])).
% 20.69/3.13 fof(f556,plain,(
% 20.69/3.13 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlpdtrp0(xe,X0)=szmzizndt0(sdtlpdtrp0(xN,X0)))),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f551])).
% 20.69/3.13 fof(f627,plain,(
% 20.69/3.13 (aElementOf0(xp,xQ)&(![W0]: (~aElementOf0(W0,xQ)|sdtlseqdt0(xp,W0))))&xp=szmzizndt0(xQ)),
% 20.69/3.13 inference(pre_NNF_transformation,[status(thm)],[f103])).
% 20.69/3.13 fof(f629,plain,(
% 20.69/3.13 ![X0]: (~aElementOf0(X0,xQ)|sdtlseqdt0(xp,X0))),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f627])).
% 20.69/3.13 fof(f630,plain,(
% 20.69/3.13 xp=szmzizndt0(xQ)),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f627])).
% 20.69/3.13 fof(f656,plain,(
% 20.69/3.13 aElementOf0(xn,szNzAzT0)),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f111])).
% 20.69/3.13 fof(f657,plain,(
% 20.69/3.13 sdtlpdtrp0(xe,xn)=xp),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f111])).
% 20.69/3.13 fof(f660,plain,(
% 20.69/3.13 aElementOf0(xx,xQ)),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f113])).
% 20.69/3.13 fof(f661,plain,(
% 20.69/3.13 ~xx=szmzizndt0(xQ)),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f113])).
% 20.69/3.13 fof(f663,plain,(
% 20.69/3.13 aElementOf0(xx,szNzAzT0)&(aElementOf0(sK38_skl,sdtlbdtrb0(xd,szDzizrdt0(xd)))&sdtlpdtrp0(xe,sK38_skl)=xx)),
% 20.69/3.13 inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl]),skolemize(W0,sK38_skl)],[f114])).
% 20.69/3.13 fof(f664,plain,(
% 20.69/3.13 aElementOf0(xx,szNzAzT0)),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f663])).
% 20.69/3.13 fof(f667,plain,(
% 20.69/3.13 aElementOf0(xm,szNzAzT0)),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f115])).
% 20.69/3.13 fof(f668,plain,(
% 20.69/3.13 xx=sdtlpdtrp0(xe,xm)),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f115])).
% 20.69/3.13 fof(f676,plain,(
% 20.69/3.13 (((![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xn))|aElementOf0(W0,sdtlpdtrp0(xN,xm))))&aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)))&~aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))))),
% 20.69/3.13 inference(pre_NNF_transformation,[status(thm)],[f119])).
% 20.69/3.13 fof(f677,plain,(
% 20.69/3.13 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xn))|aElementOf0(X0,sdtlpdtrp0(xN,xm)))),
% 20.69/3.13 inference(cnf_transformation,[status(thm)],[f676])).
% 20.69/3.13 fof(f2028,plain,(
% 20.69/3.13 ~xx=xp),
% 20.69/3.13 inference(backward_demodulation,[status(thm)],[f630,f661])).
% 20.69/3.13 fof(f3802,plain,(
% 20.69/3.13 ![X0]: (~aElementOf0(xm,szNzAzT0)|aElementOf0(X0,szNzAzT0)|~aElementOf0(X0,sdtlpdtrp0(xN,xn)))),
% 20.69/3.13 inference(resolution,[status(thm)],[f437,f677])).
% 20.69/3.13 fof(f3809,plain,(
% 20.69/3.13 ![X0]: (aElementOf0(X0,szNzAzT0)|~aElementOf0(X0,sdtlpdtrp0(xN,xn)))),
% 20.69/3.13 inference(forward_subsumption_resolution,[status(thm)],[f3802,f667])).
% 20.69/3.13 fof(f4607,plain,(
% 20.69/3.13 ![X0]: (~aElementOf0(xm,szNzAzT0)|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),X0)|~aElementOf0(X0,sdtlpdtrp0(xN,xn)))),
% 20.69/3.13 inference(resolution,[status(thm)],[f476,f677])).
% 20.69/3.13 fof(f4612,plain,(
% 20.69/3.13 ![X0]: (sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xm)),X0)|~aElementOf0(X0,sdtlpdtrp0(xN,xn)))),
% 20.69/3.13 inference(forward_subsumption_resolution,[status(thm)],[f4607,f667])).
% 20.69/3.13 fof(f4685,plain,(
% 20.69/3.13 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xn))|~aElementOf0(X0,szNzAzT0)|~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),szNzAzT0)|~sdtlseqdt0(X0,szmzizndt0(sdtlpdtrp0(xN,xm)))|X0=szmzizndt0(sdtlpdtrp0(xN,xm)))),
% 20.69/3.13 inference(resolution,[status(thm)],[f4612,f225])).
% 20.69/3.13 fof(f4686,plain,(
% 20.69/3.13 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xn))|~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),szNzAzT0)|~sdtlseqdt0(X0,szmzizndt0(sdtlpdtrp0(xN,xm)))|X0=szmzizndt0(sdtlpdtrp0(xN,xm)))),
% 20.69/3.13 inference(forward_subsumption_resolution,[status(thm)],[f4685,f3809])).
% 20.69/3.15 fof(f6550,plain,(
% 20.69/3.15 aElementOf0(sdtlpdtrp0(xe,xn),sdtlpdtrp0(xN,xn))),
% 20.69/3.15 inference(resolution,[status(thm)],[f554,f656])).
% 20.69/3.15 fof(f6555,plain,(
% 20.69/3.15 aElementOf0(xp,sdtlpdtrp0(xN,xn))),
% 20.69/3.15 inference(forward_demodulation,[status(thm)],[f657,f6550])).
% 20.69/3.15 fof(f6765,plain,(
% 20.69/3.15 sdtlpdtrp0(xe,xm)=szmzizndt0(sdtlpdtrp0(xN,xm))),
% 20.69/3.15 inference(resolution,[status(thm)],[f556,f667])).
% 20.69/3.15 fof(f6774,plain,(
% 20.69/3.15 xx=szmzizndt0(sdtlpdtrp0(xN,xm))),
% 20.69/3.15 inference(forward_demodulation,[status(thm)],[f668,f6765])).
% 20.69/3.15 fof(f8381,plain,(
% 20.69/3.15 sdtlseqdt0(xp,xx)),
% 20.69/3.15 inference(resolution,[status(thm)],[f629,f660])).
% 20.69/3.15 fof(f9445,plain,(
% 20.69/3.15 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xn))|~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xm)),szNzAzT0)|~sdtlseqdt0(X0,szmzizndt0(sdtlpdtrp0(xN,xm)))|X0=xx)),
% 20.69/3.15 inference(backward_demodulation,[status(thm)],[f6774,f4686])).
% 20.69/3.15 fof(f9499,plain,(
% 20.69/3.15 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xn))|~aElementOf0(xx,szNzAzT0)|~sdtlseqdt0(X0,szmzizndt0(sdtlpdtrp0(xN,xm)))|X0=xx)),
% 20.69/3.15 inference(forward_demodulation,[status(thm)],[f6774,f9445])).
% 20.69/3.15 fof(f9500,plain,(
% 20.69/3.15 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xn))|~aElementOf0(xx,szNzAzT0)|~sdtlseqdt0(X0,xx)|X0=xx)),
% 20.69/3.15 inference(forward_demodulation,[status(thm)],[f6774,f9499])).
% 20.69/3.15 fof(f9501,plain,(
% 20.69/3.15 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xn))|~sdtlseqdt0(X0,xx)|X0=xx)),
% 20.69/3.15 inference(forward_subsumption_resolution,[status(thm)],[f9500,f664])).
% 20.69/3.15 fof(f12887,plain,(
% 20.69/3.15 ~sdtlseqdt0(xp,xx)|xp=xx),
% 20.69/3.15 inference(resolution,[status(thm)],[f9501,f6555])).
% 20.69/3.15 fof(f12893,plain,(
% 20.69/3.15 xp=xx),
% 20.69/3.15 inference(forward_subsumption_resolution,[status(thm)],[f12887,f8381])).
% 20.69/3.15 fof(f12899,plain,(
% 20.69/3.15 $false),
% 20.69/3.15 inference(forward_subsumption_resolution,[status(thm)],[f12893,f2028])).
% 20.69/3.15 % SZS output end CNFRefutation for theBenchmark.p
% 20.69/3.16 % Elapsed time: 2.760223 seconds
% 20.69/3.16 % CPU time: 21.056781 seconds
% 20.69/3.16 % Total memory used: 322.113 MB
% 20.69/3.16 % Net memory used: 305.599 MB
%------------------------------------------------------------------------------