%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM627+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 : n009.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 175.52s 27.59s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM627+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.09/5.36 % Computer : n009.cluster.edu
% 0.09/5.36 % Model : x86_64 x86_64
% 0.09/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.36 % Memory : 8046.5625MB
% 0.09/5.36 % OS : Linux 6.8.0-71-generic
% 0.09/5.36 % CPULimit : 300
% 0.09/5.36 % WCLimit : 300
% 0.09/5.36 % DateTime : Mon Sep 21 02:45:47 UTC 2026
% 0.09/5.36 % CPUTime :
% 0.09/5.39 % Drodi V4.1.1
% 175.52/27.59 % Refutation found
% 175.52/27.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 175.52/27.59 % SZS output start CNFRefutation for theBenchmark
% 175.52/27.59 fof(f15,definition,(
% 175.52/27.59 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtpldt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& ( aElementOf0(W3,W0)| W3 = W1 ) ) ) )) ) )) )),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f16,definition,(
% 175.52/27.59 (! [W0,W1] :( ( aSet0(W0)& aElement0(W1) )=> (! [W2] :( W2 = sdtmndt0(W0,W1)<=> ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)<=> ( aElement0(W3)& aElementOf0(W3,W0)& W3 != W1 ) ) )) ) )) )),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f18,axiom,(
% 175.52/27.59 (! [W0,W1] :( ( aElement0(W0)& aSet0(W1) )=> ( ~ aElementOf0(W0,W1)=> sdtmndt0(sdtpldt0(W1,W0),W0) = W1 ) ) )),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f25,axiom,(
% 175.52/27.59 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aElementOf0(szszuzczcdt0(W0),szNzAzT0)& szszuzczcdt0(W0) != sz00 ) ) )),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f27,axiom,(
% 175.52/27.59 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( W0 = sz00| (? [W1] :( aElementOf0(W1,szNzAzT0)& W0 = szszuzczcdt0(W1) ) )) ) )),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f37,axiom,(
% 175.52/27.59 (! [W0,W1] :( ( aElementOf0(W0,szNzAzT0)& aElementOf0(W1,szNzAzT0) )=> ( sdtlseqdt0(W0,W1)| sdtlseqdt0(szszuzczcdt0(W1),W0) ) ) )),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f81,hypothesis,(
% 175.52/27.59 ( 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))) ) ) ) )) ),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f82,hypothesis,(
% 175.52/27.59 (! [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)) ) ) )),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f83,hypothesis,(
% 175.52/27.59 (! [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)) ) ) ) )),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f86,hypothesis,(
% 175.52/27.59 ( 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)))) ) ) )) ) )) ),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f91,hypothesis,(
% 175.52/27.59 ( 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)) ) ) )) ),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f111,hypothesis,(
% 175.52/27.59 ( aElementOf0(xn,szDzozmdt0(xd))& sdtlpdtrp0(xd,xn) = szDzizrdt0(xd)& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))& aElementOf0(xn,szNzAzT0)& sdtlpdtrp0(xe,xn) = xp ) ),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f113,hypothesis,(
% 175.52/27.59 ( aElement0(xx)& aElementOf0(xx,xQ)& xx != szmzizndt0(xQ)& aElementOf0(xx,xP) ) ),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f115,hypothesis,(
% 175.52/27.59 ( aElementOf0(xm,szNzAzT0)& xx = sdtlpdtrp0(xe,xm) ) ),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f118,hypothesis,(
% 175.52/27.59 ~ ( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xn))=> aElementOf0(W0,sdtlpdtrp0(xN,xm)) ))| aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)) ) ),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f119,conjecture,(
% 175.52/27.59 aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ),
% 175.52/27.59 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 175.52/27.59 fof(f120,negated_conjecture,(
% 175.52/27.59 ~(aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) )),
% 175.52/27.59 inference(negated_conjecture,[status(cth)],[f119])).
% 175.52/27.59 fof(f161,plain,(
% 175.52/27.59 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtpldt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>(aElement0(W3)&(aElementOf0(W3,W0)|W3=W1))))))))),
% 175.52/27.59 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 175.52/27.59 fof(f162,plain,(
% 175.52/27.59 ![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))))))))))),
% 175.52/27.59 inference(NNF_transformation,[status(thm)],[f161])).
% 175.52/27.59 fof(f163,plain,(
% 175.52/27.59 ![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))))))))))),
% 175.52/27.59 inference(miniscoping,[status(thm)],[f162])).
% 175.52/27.59 fof(f164,plain,(
% 175.52/27.59 ![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)))))))))),
% 175.52/27.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl]),skolemize(W3,sK2_skl(W2,W1,W0))],[f163])).
% 175.52/27.59 fof(f165,plain,(
% 175.52/27.59 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtpldt0(X0,X1)|aSet0(X2))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f164])).
% 175.52/27.59 fof(f174,plain,(
% 175.52/27.59 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1)))))))),
% 175.52/27.59 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 175.52/27.59 fof(f175,definition,(
% 175.52/27.59 ![W0,W1,W3]: (sP0_prd(W3,W1,W0)<=>((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1))),
% 175.52/27.59 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 175.52/27.59 fof(f176,plain,(
% 175.52/27.59 ![W0,W1]: ((~aSet0(W0)|~aElement0(W1))|(![W2]: (W2=sdtmndt0(W0,W1)<=>(aSet0(W2)&(![W3]: (aElementOf0(W3,W2)<=>sP0_prd(W3,W1,W0)))))))),
% 175.52/27.59 inference(formula_renaming,[status(thm)],[f174,f175])).
% 175.52/27.59 fof(f177,plain,(
% 175.52/27.59 ![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)))))))))),
% 175.52/27.59 inference(NNF_transformation,[status(thm)],[f176])).
% 175.52/27.59 fof(f178,plain,(
% 175.52/27.59 ![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)))))))))),
% 175.52/27.59 inference(miniscoping,[status(thm)],[f177])).
% 175.52/27.59 fof(f179,plain,(
% 175.52/27.59 ![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))))))))),
% 175.52/27.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(W3,sK3_skl(W2,W1,W0))],[f178])).
% 175.52/27.59 fof(f181,plain,(
% 175.52/27.59 ![X0,X1,X2,X3]: (~aSet0(X0)|~aElement0(X1)|~X2=sdtmndt0(X0,X1)|~aElementOf0(X3,X2)|sP0_prd(X3,X1,X0))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f179])).
% 175.52/27.59 fof(f187,plain,(
% 175.52/27.59 ![W0,W1]: ((~aElement0(W0)|~aSet0(W1))|(aElementOf0(W0,W1)|sdtmndt0(sdtpldt0(W1,W0),W0)=W1))),
% 175.52/27.59 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 175.52/27.59 fof(f188,plain,(
% 175.52/27.59 ![X0,X1]: (~aElement0(X0)|~aSet0(X1)|aElementOf0(X0,X1)|sdtmndt0(sdtpldt0(X1,X0),X0)=X1)),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f187])).
% 175.52/27.59 fof(f200,plain,(
% 175.52/27.59 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aElementOf0(szszuzczcdt0(W0),szNzAzT0)&~szszuzczcdt0(W0)=sz00))),
% 175.52/27.59 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 175.52/27.59 fof(f201,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(szszuzczcdt0(X0),szNzAzT0))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f200])).
% 175.52/27.59 fof(f202,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,szNzAzT0)|~szszuzczcdt0(X0)=sz00)),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f200])).
% 175.52/27.59 fof(f205,plain,(
% 175.52/27.59 ![W0]: (~aElementOf0(W0,szNzAzT0)|(W0=sz00|(?[W1]: (aElementOf0(W1,szNzAzT0)&W0=szszuzczcdt0(W1)))))),
% 175.52/27.59 inference(pre_NNF_transformation,[status(thm)],[f27])).
% 175.52/27.59 fof(f206,plain,(
% 175.52/27.59 ![W0]: (~aElementOf0(W0,szNzAzT0)|(W0=sz00|(aElementOf0(sK4_skl(W0),szNzAzT0)&W0=szszuzczcdt0(sK4_skl(W0)))))),
% 175.52/27.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(W1,sK4_skl(W0))],[f205])).
% 175.52/27.59 fof(f207,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,szNzAzT0)|X0=sz00|aElementOf0(sK4_skl(X0),szNzAzT0))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f206])).
% 175.52/27.59 fof(f208,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,szNzAzT0)|X0=sz00|X0=szszuzczcdt0(sK4_skl(X0)))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f206])).
% 175.52/27.59 fof(f229,plain,(
% 175.52/27.59 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|(sdtlseqdt0(W0,W1)|sdtlseqdt0(szszuzczcdt0(W1),W0)))),
% 175.52/27.59 inference(pre_NNF_transformation,[status(thm)],[f37])).
% 175.52/27.59 fof(f230,plain,(
% 175.52/27.59 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|sdtlseqdt0(X0,X1)|sdtlseqdt0(szszuzczcdt0(X1),X0))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f229])).
% 175.52/27.59 fof(f417,plain,(
% 175.52/27.59 ((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)))))))),
% 175.52/27.59 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 175.52/27.59 fof(f418,definition,(
% 175.52/27.59 ![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))))),
% 175.52/27.59 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 175.52/27.59 fof(f419,plain,(
% 175.52/27.59 ((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)))))))),
% 175.52/27.59 inference(formula_renaming,[status(thm)],[f417,f418])).
% 175.52/27.59 fof(f420,plain,(
% 175.52/27.59 ((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)))))))),
% 175.52/27.59 inference(NNF_transformation,[status(thm)],[f419])).
% 175.52/27.59 fof(f421,plain,(
% 175.52/27.59 ((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)))))))),
% 175.52/27.59 inference(miniscoping,[status(thm)],[f420])).
% 175.52/27.59 fof(f432,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,szNzAzT0)|sP4_prd(X0)|aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0))))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f421])).
% 175.52/27.59 fof(f436,plain,(
% 175.52/27.59 ![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))))),
% 175.52/27.59 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 175.52/27.59 fof(f437,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSet0(sdtlpdtrp0(xN,X0)))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f436])).
% 175.52/27.59 fof(f439,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f436])).
% 175.52/27.59 fof(f440,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,szNzAzT0)|isCountable0(sdtlpdtrp0(xN,X0)))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f436])).
% 175.52/27.59 fof(f441,plain,(
% 175.52/27.59 ![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)))))),
% 175.52/27.59 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 175.52/27.59 fof(f442,plain,(
% 175.52/27.59 ![X0,X1,X2]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X1,X0)|~aElementOf0(X2,sdtlpdtrp0(xN,X0))|aElementOf0(X2,sdtlpdtrp0(xN,X1)))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f441])).
% 175.52/27.59 fof(f443,plain,(
% 175.52/27.59 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X1,X0)|aSubsetOf0(sdtlpdtrp0(xN,X0),sdtlpdtrp0(xN,X1)))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f441])).
% 175.52/27.59 fof(f467,plain,(
% 175.52/27.59 (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))))))))))),
% 175.52/27.59 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 175.52/27.59 fof(f468,definition,(
% 175.52/27.59 ![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))))))),
% 175.52/27.59 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 175.52/27.59 fof(f469,plain,(
% 175.52/27.59 (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))))))))))),
% 175.52/27.59 inference(formula_renaming,[status(thm)],[f467,f468])).
% 175.52/27.59 fof(f470,plain,(
% 175.52/27.59 (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))))))))))),
% 175.52/27.59 inference(NNF_transformation,[status(thm)],[f469])).
% 175.52/27.59 fof(f471,plain,(
% 175.52/27.59 (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))))))))))),
% 175.52/27.59 inference(miniscoping,[status(thm)],[f470])).
% 175.52/27.59 fof(f472,plain,(
% 175.52/27.59 (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))))))))))),
% 175.52/27.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK24_skl]),skolemize(W2,sK24_skl(W1,W0))],[f471])).
% 175.52/27.59 fof(f476,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X0)))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f472])).
% 175.52/27.59 fof(f552,plain,(
% 175.52/27.59 (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)))))),
% 175.52/27.59 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 175.52/27.59 fof(f557,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlpdtrp0(xe,X0)=szmzizndt0(sdtlpdtrp0(xN,X0)))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f552])).
% 175.52/27.59 fof(f657,plain,(
% 175.52/27.59 aElementOf0(xn,szNzAzT0)),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f111])).
% 175.52/27.59 fof(f660,plain,(
% 175.52/27.59 aElement0(xx)),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f113])).
% 175.52/27.59 fof(f668,plain,(
% 175.52/27.59 aElementOf0(xm,szNzAzT0)),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f115])).
% 175.52/27.59 fof(f669,plain,(
% 175.52/27.59 xx=sdtlpdtrp0(xe,xm)),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f115])).
% 175.52/27.59 fof(f677,plain,(
% 175.52/27.59 ((?[W0]: (aElementOf0(W0,sdtlpdtrp0(xN,xn))&~aElementOf0(W0,sdtlpdtrp0(xN,xm))))&~aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)))),
% 175.52/27.59 inference(pre_NNF_transformation,[status(thm)],[f118])).
% 175.52/27.59 fof(f678,plain,(
% 175.52/27.59 (aElementOf0(sK40_skl,sdtlpdtrp0(xN,xn))&~aElementOf0(sK40_skl,sdtlpdtrp0(xN,xm)))&~aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm))),
% 175.52/27.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK40_skl]),skolemize(W0,sK40_skl)],[f677])).
% 175.52/27.59 fof(f681,plain,(
% 175.52/27.59 ~aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f678])).
% 175.52/27.59 fof(f682,plain,(
% 175.52/27.59 ~aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f120])).
% 175.52/27.59 fof(f683,plain,(
% 175.52/27.59 ![W0,W1,W3]: ((~sP0_prd(W3,W1,W0)|((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1))&(sP0_prd(W3,W1,W0)|((~aElement0(W3)|~aElementOf0(W3,W0))|W3=W1)))),
% 175.52/27.59 inference(NNF_transformation,[status(thm)],[f175])).
% 175.52/27.59 fof(f684,plain,(
% 175.52/27.59 (![W0,W1,W3]: (~sP0_prd(W3,W1,W0)|((aElement0(W3)&aElementOf0(W3,W0))&~W3=W1)))&(![W0,W1,W3]: (sP0_prd(W3,W1,W0)|((~aElement0(W3)|~aElementOf0(W3,W0))|W3=W1)))),
% 175.52/27.59 inference(miniscoping,[status(thm)],[f683])).
% 175.52/27.59 fof(f687,plain,(
% 175.52/27.59 ![X0,X1,X2]: (~sP0_prd(X0,X1,X2)|~X0=X1)),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f684])).
% 175.52/27.59 fof(f734,plain,(
% 175.52/27.59 ![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))))&(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)))))),
% 175.52/27.59 inference(NNF_transformation,[status(thm)],[f418])).
% 175.52/27.59 fof(f735,plain,(
% 175.52/27.59 (![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)))))&(![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)))))),
% 175.52/27.59 inference(miniscoping,[status(thm)],[f734])).
% 175.52/27.59 fof(f736,plain,(
% 175.52/27.59 (![W0]: (~sP4_prd(W0)|(((~aSet0(sdtlpdtrp0(xN,W0))|(aElementOf0(sK52_skl(W0),sdtlpdtrp0(xN,W0))&~aElementOf0(sK52_skl(W0),szNzAzT0)))&~aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0))|~isCountable0(sdtlpdtrp0(xN,W0)))))&(![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)))))),
% 175.52/27.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK52_skl]),skolemize(W1,sK52_skl(W0))],[f735])).
% 175.52/27.59 fof(f739,plain,(
% 175.52/27.59 ![X0]: (~sP4_prd(X0)|~aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)|~isCountable0(sdtlpdtrp0(xN,X0)))),
% 175.52/27.59 inference(cnf_transformation,[status(thm)],[f736])).
% 175.52/27.59 fof(f868,plain,(
% 175.52/27.59 ![X0,X1]: (~aSet0(X0)|~aElement0(X1)|aSet0(sdtpldt0(X0,X1)))),
% 175.52/27.59 inference(destructive_equality_resolution,[status(thm)],[f165])).
% 175.52/27.59 fof(f875,plain,(
% 175.52/27.59 ![X0,X1,X2]: (~aSet0(X0)|~aElement0(X1)|~aElementOf0(X2,sdtmndt0(X0,X1))|sP0_prd(X2,X1,X0))),
% 175.52/27.59 inference(destructive_equality_resolution,[status(thm)],[f181])).
% 175.52/27.59 fof(f916,plain,(
% 175.52/27.59 ![X0,X1]: (~sP0_prd(X0,X0,X1))),
% 175.52/27.59 inference(destructive_equality_resolution,[status(thm)],[f687])).
% 175.52/27.59 fof(f981,plain,(
% 175.52/27.59 ![X0]: (~aSet0(X0)|aSet0(sdtpldt0(X0,xx)))),
% 175.52/27.59 inference(resolution,[status(thm)],[f868,f660])).
% 175.52/27.59 fof(f1048,plain,(
% 175.52/27.59 ![X0]: (~aSet0(X0)|aElementOf0(xx,X0)|sdtmndt0(sdtpldt0(X0,xx),xx)=X0)),
% 175.52/27.59 inference(resolution,[status(thm)],[f188,f660])).
% 175.52/27.59 fof(f1126,plain,(
% 175.52/27.59 ![X0]: (szszuzczcdt0(X0)=sz00|aElementOf0(sK4_skl(szszuzczcdt0(X0)),szNzAzT0)|~aElementOf0(X0,szNzAzT0))),
% 175.52/27.59 inference(resolution,[status(thm)],[f207,f201])).
% 175.52/27.59 fof(f1127,plain,(
% 175.52/27.59 ![X0]: (aElementOf0(sK4_skl(szszuzczcdt0(X0)),szNzAzT0)|~aElementOf0(X0,szNzAzT0))),
% 175.52/27.59 inference(forward_subsumption_resolution,[status(thm)],[f1126,f202])).
% 175.52/27.59 fof(f1177,plain,(
% 175.52/27.59 aElementOf0(sK4_skl(szszuzczcdt0(xn)),szNzAzT0)),
% 175.52/27.59 inference(resolution,[status(thm)],[f1127,f657])).
% 175.52/27.59 fof(f1202,plain,(
% 175.52/27.59 ![X0]: (szszuzczcdt0(X0)=sz00|szszuzczcdt0(X0)=szszuzczcdt0(sK4_skl(szszuzczcdt0(X0)))|~aElementOf0(X0,szNzAzT0))),
% 175.52/27.59 inference(resolution,[status(thm)],[f208,f201])).
% 175.52/27.59 fof(f1203,plain,(
% 175.52/27.59 ![X0]: (szszuzczcdt0(X0)=szszuzczcdt0(sK4_skl(szszuzczcdt0(X0)))|~aElementOf0(X0,szNzAzT0))),
% 175.52/27.59 inference(forward_subsumption_resolution,[status(thm)],[f1202,f202])).
% 175.52/27.59 fof(f1264,plain,(
% 175.52/27.59 szszuzczcdt0(xn)=szszuzczcdt0(sK4_skl(szszuzczcdt0(xn)))),
% 175.52/27.59 inference(resolution,[status(thm)],[f1203,f657])).
% 175.52/27.59 fof(f4250,plain,(
% 175.52/27.59 sP4_prd(xn)|aSet0(sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 175.52/27.59 inference(resolution,[status(thm)],[f432,f657])).
% 175.52/27.59 fof(f4367,plain,(
% 175.52/27.59 sP4_prd(xn)|aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn)))|sdtmndt0(sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx),xx)=sdtlpdtrp0(xN,szszuzczcdt0(xn))),
% 175.52/27.59 inference(resolution,[status(thm)],[f4250,f1048])).
% 175.52/27.59 fof(f4376,plain,(
% 175.52/27.59 sP4_prd(xn)|sdtmndt0(sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx),xx)=sdtlpdtrp0(xN,szszuzczcdt0(xn))),
% 175.52/27.59 inference(forward_subsumption_resolution,[status(thm)],[f4367,f682])).
% 175.52/27.59 fof(f4460,plain,(
% 175.52/27.59 ![X0]: (aSet0(sdtlpdtrp0(xN,szszuzczcdt0(X0)))|~aElementOf0(X0,szNzAzT0))),
% 175.52/27.59 inference(resolution,[status(thm)],[f437,f201])).
% 175.52/27.59 fof(f4479,plain,(
% 175.52/27.59 aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0)),
% 175.52/27.59 inference(resolution,[status(thm)],[f439,f657])).
% 175.52/27.59 fof(f4565,plain,(
% 175.52/27.59 aSet0(sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 175.52/27.59 inference(resolution,[status(thm)],[f4460,f657])).
% 175.52/27.59 fof(f5467,plain,(
% 175.52/27.59 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X1,X0)|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X1)))),
% 175.52/27.59 inference(resolution,[status(thm)],[f476,f442])).
% 175.52/27.59 fof(f5476,plain,(
% 175.52/27.59 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X1,X0)|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,X0)),sdtlpdtrp0(xN,X1)))),
% 175.52/27.59 inference(duplicate_literals_removal,[status(thm)],[f5467])).
% 175.52/27.59 fof(f7218,plain,(
% 175.52/27.59 ~aElementOf0(sK4_skl(szszuzczcdt0(xn)),szNzAzT0)|aElementOf0(szszuzczcdt0(xn),szNzAzT0)),
% 175.52/27.59 inference(paramodulation,[status(thm)],[f1264,f201])).
% 175.52/27.59 fof(f7245,plain,(
% 175.52/27.59 aElementOf0(szszuzczcdt0(xn),szNzAzT0)),
% 175.52/27.59 inference(forward_subsumption_resolution,[status(thm)],[f7218,f1177])).
% 175.52/27.59 fof(f8496,plain,(
% 175.52/27.59 sdtlpdtrp0(xe,xm)=szmzizndt0(sdtlpdtrp0(xN,xm))),
% 175.52/27.59 inference(resolution,[status(thm)],[f557,f668])).
% 175.52/27.59 fof(f8517,plain,(
% 175.52/27.59 xx=szmzizndt0(sdtlpdtrp0(xN,xm))),
% 175.52/27.59 inference(forward_demodulation,[status(thm)],[f669,f8496])).
% 175.52/27.59 fof(f10799,plain,(
% 175.52/27.59 ~aElementOf0(xn,szNzAzT0)|~aElementOf0(xm,szNzAzT0)|~sdtlseqdt0(xm,xn)),
% 175.52/27.59 inference(resolution,[status(thm)],[f681,f443])).
% 175.52/27.59 fof(f10800,plain,(
% 175.52/27.59 ~aElementOf0(xm,szNzAzT0)|~sdtlseqdt0(xm,xn)),
% 175.52/27.59 inference(forward_subsumption_resolution,[status(thm)],[f10799,f657])).
% 175.52/27.59 fof(f10851,plain,(
% 175.52/27.59 ~sdtlseqdt0(xm,xn)),
% 175.52/27.59 inference(forward_subsumption_resolution,[status(thm)],[f10800,f668])).
% 175.52/27.59 fof(f12239,plain,(
% 175.52/27.59 ~aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0)|~isCountable0(sdtlpdtrp0(xN,xn))|sdtmndt0(sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx),xx)=sdtlpdtrp0(xN,szszuzczcdt0(xn))),
% 175.52/27.59 inference(resolution,[status(thm)],[f739,f4376])).
% 175.52/27.59 fof(f12240,plain,(
% 175.52/27.59 ~isCountable0(sdtlpdtrp0(xN,xn))|sdtmndt0(sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx),xx)=sdtlpdtrp0(xN,szszuzczcdt0(xn))),
% 175.52/27.59 inference(forward_subsumption_resolution,[status(thm)],[f12239,f4479])).
% 175.52/27.59 fof(f12278,plain,(
% 175.52/27.59 sdtmndt0(sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx),xx)=sdtlpdtrp0(xN,szszuzczcdt0(xn))|~aElementOf0(xn,szNzAzT0)),
% 175.52/27.59 inference(resolution,[status(thm)],[f12240,f440])).
% 175.52/27.59 fof(f12279,plain,(
% 175.52/27.59 sdtmndt0(sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx),xx)=sdtlpdtrp0(xN,szszuzczcdt0(xn))),
% 175.52/27.59 inference(forward_subsumption_resolution,[status(thm)],[f12278,f657])).
% 175.52/27.59 fof(f12297,plain,(
% 175.52/27.59 ![X0]: (~aSet0(sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx))|~aElement0(xx)|~aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn)))|sP0_prd(X0,xx,sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx)))),
% 175.52/27.59 inference(paramodulation,[status(thm)],[f12279,f875])).
% 175.52/27.59 fof(f12314,plain,(
% 175.52/27.59 ![X0]: (~aSet0(sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx))|~aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn)))|sP0_prd(X0,xx,sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx)))),
% 175.52/27.59 inference(forward_subsumption_resolution,[status(thm)],[f12297,f660])).
% 175.52/27.59 fof(f13669,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn)))|sP0_prd(X0,xx,sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx))|~aSet0(sdtlpdtrp0(xN,szszuzczcdt0(xn))))),
% 175.52/27.59 inference(resolution,[status(thm)],[f12314,f981])).
% 175.52/27.59 fof(f32190,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn)))|sP0_prd(X0,xx,sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx)))),
% 175.52/27.59 inference(backward_subsumption_resolution,[status(thm)],[f13669,f4565])).
% 175.52/27.59 fof(f53080,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(szszuzczcdt0(xn),szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(xn),X0)|sP0_prd(szmzizndt0(sdtlpdtrp0(xN,X0)),xx,sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx)))),
% 175.52/27.59 inference(resolution,[status(thm)],[f5476,f32190])).
% 175.52/27.59 fof(f53102,plain,(
% 175.52/27.59 ![X0]: (~aElementOf0(X0,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(xn),X0)|sP0_prd(szmzizndt0(sdtlpdtrp0(xN,X0)),xx,sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx)))),
% 175.52/27.59 inference(forward_subsumption_resolution,[status(thm)],[f53080,f7245])).
% 175.52/27.59 fof(f54093,plain,(
% 175.52/27.59 ~aElementOf0(xm,szNzAzT0)|~sdtlseqdt0(szszuzczcdt0(xn),xm)|sP0_prd(xx,xx,sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx))),
% 175.52/27.59 inference(paramodulation,[status(thm)],[f8517,f53102])).
% 175.52/27.59 fof(f54099,plain,(
% 175.52/27.59 ~sdtlseqdt0(szszuzczcdt0(xn),xm)|sP0_prd(xx,xx,sdtpldt0(sdtlpdtrp0(xN,szszuzczcdt0(xn)),xx))),
% 175.52/27.59 inference(forward_subsumption_resolution,[status(thm)],[f54093,f668])).
% 175.52/27.59 fof(f55318,plain,(
% 175.52/27.59 ~sdtlseqdt0(szszuzczcdt0(xn),xm)),
% 175.52/27.59 inference(forward_subsumption_resolution,[status(thm)],[f54099,f916])).
% 175.52/27.59 fof(f55319,plain,(
% 175.52/27.59 ~aElementOf0(xm,szNzAzT0)|~aElementOf0(xn,szNzAzT0)|sdtlseqdt0(xm,xn)),
% 176.30/27.70 inference(resolution,[status(thm)],[f55318,f230])).
% 176.30/27.70 fof(f55322,plain,(
% 176.30/27.70 ~aElementOf0(xn,szNzAzT0)|sdtlseqdt0(xm,xn)),
% 176.30/27.70 inference(forward_subsumption_resolution,[status(thm)],[f55319,f668])).
% 176.30/27.70 fof(f55933,plain,(
% 176.30/27.70 sdtlseqdt0(xm,xn)),
% 176.30/27.70 inference(forward_subsumption_resolution,[status(thm)],[f55322,f657])).
% 176.30/27.70 fof(f55934,plain,(
% 176.30/27.70 $false),
% 176.30/27.70 inference(backward_subsumption_resolution,[status(thm)],[f10851,f55933])).
% 176.30/27.70 % SZS output end CNFRefutation for theBenchmark.p
% 27.71/27.77 % Elapsed time: 22.385129 seconds
% 27.71/27.77 % CPU time: 177.142740 seconds
% 27.71/27.77 % Total memory used: 1.041 GB
% 27.71/27.77 % Net memory used: 980.016 MB
%------------------------------------------------------------------------------