%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM581+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 : n004.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:16 PM UTC 2026
% Result : Theorem 105.05s 14.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM581+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.97 % Computer : n004.cluster.edu
% 0.08/0.97 % Model : x86_64 x86_64
% 0.08/0.97 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.97 % Memory : 8046.5625MB
% 0.08/0.97 % OS : Linux 6.8.0-71-generic
% 0.08/0.97 % CPULimit : 300
% 0.08/0.97 % WCLimit : 300
% 0.08/0.97 % DateTime : Mon Sep 21 02:42:06 UTC 2026
% 0.08/0.97 % CPUTime :
% 0.08/1.00 % Drodi V4.1.1
% 105.05/14.31 % Refutation found
% 105.05/14.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 105.05/14.31 % SZS output start CNFRefutation for theBenchmark
% 105.05/14.31 fof(f3,axiom,(
% 105.05/14.31 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 105.05/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.05/14.31 fof(f15,definition,(
% 105.05/14.31 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtpldt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& ( aElementOf0(W3,W0)| W3 = W1 ) ) ) )) ) )) )),
% 105.05/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.05/14.31 fof(f23,axiom,(
% 105.05/14.31 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 105.05/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.05/14.31 fof(f24,axiom,(
% 105.05/14.31 aElementOf0(sz00,szNzAzT0) ),
% 105.05/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.05/14.31 fof(f30,axiom,(
% 105.05/14.31 (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlseqdt0(sz00,W0) ) )),
% 105.05/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.05/14.31 fof(f81,hypothesis,(
% 105.05/14.31 ( aFunction0(xN)& szDzozmdt0(xN) = szNzAzT0& sdtlpdtrp0(xN,sz00) = xS& (! [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)) )=> ( 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)) ) ))& aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))& (! [W1] :( aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))=> aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))) ))& aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0))))& isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0))) ) ) ) )) ),
% 105.05/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.05/14.31 fof(f82,hypothesis,(
% 105.05/14.31 (! [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)) ) ) )),
% 105.05/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.05/14.31 fof(f83,hypothesis,(
% 105.05/14.31 (! [W0,W1] :( ( aElementOf0(W0,szNzAzT0)& aElementOf0(W1,szNzAzT0) )=> ( sdtlseqdt0(W1,W0)=> ( (! [W2] :( aElementOf0(W2,sdtlpdtrp0(xN,W0))=> aElementOf0(W2,sdtlpdtrp0(xN,W1)) ))& aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1)) ) ) ) )),
% 105.05/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.05/14.31 fof(f85,hypothesis,(
% 105.05/14.31 aElementOf0(xi,szNzAzT0) ),
% 105.05/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.05/14.31 fof(f86,hypothesis,(
% 105.05/14.31 ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))& (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) ))& aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))& (! [W0] :( aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))<=> ( aElement0(W0)& aElementOf0(W0,sdtlpdtrp0(xN,xi))& W0 != szmzizndt0(sdtlpdtrp0(xN,xi)) ) ))& aSet0(xQ)& (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ))& aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))& sbrdtbr0(xQ) = xk& aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk)) ) ),
% 105.05/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.05/14.31 fof(f88,conjecture,(
% 105.05/14.31 ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))& (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) ) ))=> ( ( aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))& (! [W0] :( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))<=> ( aElement0(W0)& ( aElementOf0(W0,xQ)| W0 = szmzizndt0(sdtlpdtrp0(xN,xi)) ) ) ) ))=> ( (! [W0] :( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))=> aElementOf0(W0,xS) ))| aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS) ) ) ) ),
% 105.05/14.31 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.05/14.31 fof(f89,negated_conjecture,(
% 105.05/14.31 ~(( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))& (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) ) ))=> ( ( aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))& (! [W0] :( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))<=> ( aElement0(W0)& ( aElementOf0(W0,xQ)| W0 = szmzizndt0(sdtlpdtrp0(xN,xi)) ) ) ) ))=> ( (! [W0] :( aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))=> aElementOf0(W0,xS) ))| aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS) ) ) ) )),
% 105.05/14.31 inference(negated_conjecture,[status(cth)],[f88])).
% 105.05/14.31 fof(f96,plain,(
% 105.05/14.31 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 105.05/14.31 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 105.05/14.31 fof(f97,plain,(
% 105.05/14.31 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f96])).
% 105.05/14.31 fof(f130,plain,(
% 105.05/14.31 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtpldt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))),
% 105.05/14.31 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 105.05/14.31 fof(f131,plain,(
% 105.05/14.31 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: ((~W2=sdtpldt0(W0,W1)|(aSet0(W2)&(![W3]: ((~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1)))&(aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))))))&(W2=sdtpldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))&(aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))))),
% 105.05/14.31 inference(NNF_transformation,[status(thm)],[f130])).
% 105.05/14.31 fof(f132,plain,(
% 105.05/14.31 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtpldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))&(![W3]: (aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1))))))))&(![W2]: (W2=sdtpldt0(W0,W1)|(~aSet0(W2)|(?[W3]: ((~aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1)))&(aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))))),
% 105.05/14.31 inference(miniscoping,[status(thm)],[f131])).
% 105.05/14.31 fof(f133,plain,(
% 105.05/14.31 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|((![W2]: (~W2=sdtpldt0(W0,W1)|(aSet0(W2)&((![W3]: (~aElementOf0(W3,W2)|(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))&(![W3]: (aElementOf0(W3,W2)|(~aElement0(W3)|(~aElementOf0(W3,W0)&~W3=W1))))))))&(![W2]: (W2=sdtpldt0(W0,W1)|(~aSet0(W2)|((~aElementOf0(sK2_skl(W2,W1,W0),W2)|(~aElement0(sK2_skl(W2,W1,W0))|(~aElementOf0(sK2_skl(W2,W1,W0),W0)&~sK2_skl(W2,W1,W0)=W1)))&(aElementOf0(sK2_skl(W2,W1,W0),W2)|(aElement0(sK2_skl(W2,W1,W0))&(aElementOf0(sK2_skl(W2,W1,W0),W0)|sK2_skl(W2,W1,W0)=W1)))))))))),
% 105.05/14.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W3,sK2_skl(W2,W1,W0))],[f132])).
% 105.05/14.31 fof(f136,plain,(
% 105.05/14.31 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtpldt0(X0,X1)|~aElementOf0(X3,X2)|aElementOf0(X3,X0)|X3=X1)),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f133])).
% 105.05/14.31 fof(f166,plain,(
% 105.05/14.31 aSet0(szNzAzT0)),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f23])).
% 105.05/14.31 fof(f168,plain,(
% 105.05/14.31 aElementOf0(sz00,szNzAzT0)),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f24])).
% 105.05/14.31 fof(f182,plain,(
% 105.05/14.31 ![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlseqdt0(sz00,W0))),
% 105.05/14.31 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 105.05/14.31 fof(f183,plain,(
% 105.05/14.31 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlseqdt0(sz00,X0))),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f182])).
% 105.05/14.31 fof(f386,plain,(
% 105.05/14.31 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![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)))|(((((((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))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0))))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))|aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 105.05/14.31 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 105.05/14.31 fof(f387,definition,(
% 105.05/14.31 ![W0]: (sP4_prd(W0)<=>(((~aSet0(sdtlpdtrp0(xN,W0))|(?[W1]: (aElementOf0(W1,sdtlpdtrp0(xN,W0))&~aElementOf0(W1,szNzAzT0))))&~aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0))|~isCountable0(sdtlpdtrp0(xN,W0))))),
% 105.05/14.31 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 105.05/14.31 fof(f388,plain,(
% 105.05/14.31 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(sP4_prd(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))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0))))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))|aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 105.05/14.31 inference(formula_renaming,[status(thm)],[f386,f387])).
% 105.05/14.31 fof(f389,plain,(
% 105.05/14.31 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(sP4_prd(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)))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0))))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))|aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 105.05/14.31 inference(NNF_transformation,[status(thm)],[f388])).
% 105.05/14.31 fof(f390,plain,(
% 105.05/14.31 ((aFunction0(xN)&szDzozmdt0(xN)=szNzAzT0)&sdtlpdtrp0(xN,sz00)=xS)&(![W0]: (~aElementOf0(W0,szNzAzT0)|(sP4_prd(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)))))))&aSet0(sdtlpdtrp0(xN,szszuzczcdt0(W0))))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,szszuzczcdt0(W0)))|aElementOf0(W1,sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))))&aSubsetOf0(sdtlpdtrp0(xN,szszuzczcdt0(W0)),sdtmndt0(sdtlpdtrp0(xN,W0),szmzizndt0(sdtlpdtrp0(xN,W0)))))&isCountable0(sdtlpdtrp0(xN,szszuzczcdt0(W0)))))))),
% 105.05/14.31 inference(miniscoping,[status(thm)],[f389])).
% 105.05/14.31 fof(f393,plain,(
% 105.05/14.31 sdtlpdtrp0(xN,sz00)=xS),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f390])).
% 105.05/14.31 fof(f405,plain,(
% 105.05/14.31 ![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))))),
% 105.05/14.31 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 105.05/14.31 fof(f407,plain,(
% 105.05/14.31 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,sdtlpdtrp0(xN,X0))|aElementOf0(X1,szNzAzT0))),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f405])).
% 105.05/14.31 fof(f410,plain,(
% 105.05/14.31 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|(~sdtlseqdt0(W1,W0)|((![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,W0))|aElementOf0(W2,sdtlpdtrp0(xN,W1))))&aSubsetOf0(sdtlpdtrp0(xN,W0),sdtlpdtrp0(xN,W1)))))),
% 105.05/14.31 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 105.05/14.31 fof(f411,plain,(
% 105.05/14.31 ![X0,X1,X2]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X1,X0)|~aElementOf0(X2,sdtlpdtrp0(xN,X0))|aElementOf0(X2,sdtlpdtrp0(xN,X1)))),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f410])).
% 105.05/14.31 fof(f420,plain,(
% 105.05/14.31 aElementOf0(xi,szNzAzT0)),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f85])).
% 105.05/14.31 fof(f421,plain,(
% 105.05/14.31 (((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))<=>((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))&aSet0(xQ))&(![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&sbrdtbr0(xQ)=xk)&aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))),
% 105.05/14.31 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 105.05/14.31 fof(f422,plain,(
% 105.05/14.31 (((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&(![W0]: ((~aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))&(aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|((~aElement0(W0)|~aElementOf0(W0,sdtlpdtrp0(xN,xi)))|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aSet0(xQ))&(![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&sbrdtbr0(xQ)=xk)&aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))),
% 105.05/14.31 inference(NNF_transformation,[status(thm)],[f421])).
% 105.05/14.31 fof(f423,plain,(
% 105.05/14.31 (((((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&((![W0]: (~aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))&(![W0]: (aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|((~aElement0(W0)|~aElementOf0(W0,sdtlpdtrp0(xN,xi)))|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aSet0(xQ))&(![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&aSubsetOf0(xQ,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))&sbrdtbr0(xQ)=xk)&aElementOf0(xQ,slbdtsldtrb0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))),xk))),
% 105.05/14.31 inference(miniscoping,[status(thm)],[f422])).
% 105.05/14.31 fof(f424,plain,(
% 105.05/14.31 aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f423])).
% 105.05/14.31 fof(f428,plain,(
% 105.05/14.31 ![X0]: (~aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|aElementOf0(X0,sdtlpdtrp0(xN,xi)))),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f423])).
% 105.05/14.31 fof(f431,plain,(
% 105.05/14.31 aSet0(xQ)),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f423])).
% 105.05/14.31 fof(f432,plain,(
% 105.05/14.31 ![X0]: (~aElementOf0(X0,xQ)|aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f423])).
% 105.05/14.31 fof(f447,plain,(
% 105.05/14.31 ((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&((aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&(![W0]: (aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))<=>(aElement0(W0)&(aElementOf0(W0,xQ)|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))))&((?[W0]: (aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS))))),
% 105.05/14.31 inference(pre_NNF_transformation,[status(thm)],[f89])).
% 105.05/14.31 fof(f448,plain,(
% 105.05/14.31 (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&((aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&(![W0]: ((~aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|(aElement0(W0)&(aElementOf0(W0,xQ)|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))&(aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|(~aElement0(W0)|(~aElementOf0(W0,xQ)&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))))&((?[W0]: (aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)))),
% 105.05/14.31 inference(NNF_transformation,[status(thm)],[f447])).
% 105.05/14.31 fof(f449,plain,(
% 105.05/14.31 (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&((aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&((![W0]: (~aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|(aElement0(W0)&(aElementOf0(W0,xQ)|W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))&(![W0]: (aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|(~aElement0(W0)|(~aElementOf0(W0,xQ)&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))))&((?[W0]: (aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)))),
% 105.05/14.31 inference(miniscoping,[status(thm)],[f448])).
% 105.05/14.31 fof(f450,plain,(
% 105.05/14.31 (aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&((aSet0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&((![W0]: (~aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|(aElement0(W0)&(aElementOf0(W0,xQ)|W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))&(![W0]: (aElementOf0(W0,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))|(~aElement0(W0)|(~aElementOf0(W0,xQ)&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))))&((aElementOf0(sK24_skl,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))&~aElementOf0(sK24_skl,xS))&~aSubsetOf0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))),xS)))),
% 105.05/14.31 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W0,sK24_skl)],[f449])).
% 105.05/14.31 fof(f458,plain,(
% 105.05/14.31 aElementOf0(sK24_skl,sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f450])).
% 105.05/14.31 fof(f459,plain,(
% 105.05/14.31 ~aElementOf0(sK24_skl,xS)),
% 105.05/14.31 inference(cnf_transformation,[status(thm)],[f450])).
% 105.05/14.31 fof(f544,plain,(
% 105.05/14.31 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~aElementOf0(X2,sdtpldt0(X0,X1))|aElementOf0(X2,X0)|X2=X1)),
% 105.05/14.31 inference(destructive_equality_resolution,[status(thm)],[f136])).
% 105.05/14.31 fof(f649,plain,(
% 105.05/14.31 ~aSet0(xQ)|~aElement0(szmzizndt0(sdtlpdtrp0(xN,xi)))|aElementOf0(sK24_skl,xQ)|sK24_skl=szmzizndt0(sdtlpdtrp0(xN,xi))),
% 105.05/14.31 inference(resolution,[status(thm)],[f544,f458])).
% 105.05/14.31 fof(f652,plain,(
% 105.05/14.31 ~aElement0(szmzizndt0(sdtlpdtrp0(xN,xi)))|aElementOf0(sK24_skl,xQ)|sK24_skl=szmzizndt0(sdtlpdtrp0(xN,xi))),
% 105.05/14.31 inference(forward_subsumption_resolution,[status(thm)],[f649,f431])).
% 105.05/14.31 fof(f843,plain,(
% 105.05/14.31 ~aElementOf0(xi,szNzAzT0)|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),szNzAzT0)),
% 105.05/14.31 inference(resolution,[status(thm)],[f407,f424])).
% 105.05/14.31 fof(f847,plain,(
% 105.05/14.31 aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),szNzAzT0)),
% 105.05/14.31 inference(forward_subsumption_resolution,[status(thm)],[f843,f420])).
% 105.05/14.31 fof(f853,plain,(
% 99.35/14.40 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X0,szNzAzT0)|~aElementOf0(sz00,szNzAzT0)|~aElementOf0(X1,sdtlpdtrp0(xN,X0))|aElementOf0(X1,sdtlpdtrp0(xN,sz00)))),
% 99.35/14.40 inference(resolution,[status(thm)],[f183,f411])).
% 99.35/14.40 fof(f856,plain,(
% 99.35/14.40 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X0,szNzAzT0)|~aElementOf0(sz00,szNzAzT0)|~aElementOf0(X1,sdtlpdtrp0(xN,X0))|aElementOf0(X1,xS))),
% 99.35/14.40 inference(forward_demodulation,[status(thm)],[f393,f853])).
% 99.35/14.40 fof(f857,plain,(
% 99.35/14.40 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(sz00,szNzAzT0)|~aElementOf0(X1,sdtlpdtrp0(xN,X0))|aElementOf0(X1,xS))),
% 99.35/14.40 inference(duplicate_literals_removal,[status(thm)],[f856])).
% 99.35/14.40 fof(f858,plain,(
% 99.35/14.40 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,sdtlpdtrp0(xN,X0))|aElementOf0(X1,xS))),
% 99.35/14.40 inference(forward_subsumption_resolution,[status(thm)],[f857,f168])).
% 99.35/14.40 fof(f1055,plain,(
% 99.35/14.40 ~aSet0(szNzAzT0)|aElement0(szmzizndt0(sdtlpdtrp0(xN,xi)))),
% 99.35/14.40 inference(resolution,[status(thm)],[f847,f97])).
% 99.35/14.40 fof(f1056,plain,(
% 99.35/14.40 aElementOf0(sK24_skl,xQ)|sK24_skl=szmzizndt0(sdtlpdtrp0(xN,xi))),
% 99.35/14.40 inference(backward_subsumption_resolution,[status(thm)],[f652,f1058])).
% 99.35/14.40 fof(f1058,plain,(
% 99.35/14.40 aElement0(szmzizndt0(sdtlpdtrp0(xN,xi)))),
% 99.35/14.40 inference(forward_subsumption_resolution,[status(thm)],[f1055,f166])).
% 99.35/14.40 fof(f1204,plain,(
% 99.35/14.40 aElementOf0(sK24_skl,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|sK24_skl=szmzizndt0(sdtlpdtrp0(xN,xi))),
% 99.35/14.40 inference(resolution,[status(thm)],[f432,f1056])).
% 99.35/14.40 fof(f4672,plain,(
% 99.35/14.40 ~aElementOf0(xi,szNzAzT0)|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),xS)),
% 99.35/14.40 inference(resolution,[status(thm)],[f858,f424])).
% 99.35/14.40 fof(f4678,plain,(
% 99.35/14.40 aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),xS)),
% 99.35/14.40 inference(forward_subsumption_resolution,[status(thm)],[f4672,f420])).
% 99.35/14.40 fof(f6769,plain,(
% 99.35/14.40 aElementOf0(sK24_skl,sdtlpdtrp0(xN,xi))|sK24_skl=szmzizndt0(sdtlpdtrp0(xN,xi))),
% 99.35/14.40 inference(resolution,[status(thm)],[f428,f1204])).
% 99.35/14.40 fof(f6777,plain,(
% 99.35/14.40 sK24_skl=szmzizndt0(sdtlpdtrp0(xN,xi))|~aElementOf0(xi,szNzAzT0)|aElementOf0(sK24_skl,xS)),
% 99.35/14.40 inference(resolution,[status(thm)],[f6769,f858])).
% 99.35/14.40 fof(f6783,plain,(
% 99.35/14.40 sK24_skl=szmzizndt0(sdtlpdtrp0(xN,xi))|aElementOf0(sK24_skl,xS)),
% 99.35/14.40 inference(forward_subsumption_resolution,[status(thm)],[f6777,f420])).
% 99.35/14.40 fof(f6787,plain,(
% 99.35/14.40 sK24_skl=szmzizndt0(sdtlpdtrp0(xN,xi))),
% 99.35/14.40 inference(resolution,[status(thm)],[f6783,f459])).
% 99.35/14.40 fof(f6799,plain,(
% 99.35/14.40 aElementOf0(sK24_skl,xS)),
% 99.35/14.40 inference(backward_demodulation,[status(thm)],[f6787,f4678])).
% 99.35/14.40 fof(f7156,plain,(
% 99.35/14.40 $false),
% 99.35/14.40 inference(forward_subsumption_resolution,[status(thm)],[f6799,f459])).
% 99.35/14.40 % SZS output end CNFRefutation for theBenchmark.p
% 16.48/14.43 % Elapsed time: 13.436308 seconds
% 16.48/14.43 % CPU time: 106.287709 seconds
% 16.48/14.43 % Total memory used: 703.355 MB
% 16.48/14.43 % Net memory used: 660.756 MB
%------------------------------------------------------------------------------