%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM629+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/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:24 PM UTC 2026
% Result : Theorem 12.49s 2.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM629+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n008.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 02:46:24 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.40 % Drodi V4.1.1
% 12.49/2.09 % Refutation found
% 12.49/2.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.49/2.09 % SZS output start CNFRefutation for theBenchmark
% 12.49/2.09 fof(f81,hypothesis,(
% 12.49/2.09 ( 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))) ) ) ) )) ),
% 12.49/2.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.49/2.09 fof(f82,hypothesis,(
% 12.49/2.09 (! [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)) ) ) )),
% 12.49/2.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.49/2.09 fof(f111,hypothesis,(
% 12.49/2.09 ( aElementOf0(xn,szDzozmdt0(xd))& sdtlpdtrp0(xd,xn) = szDzizrdt0(xd)& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))& aElementOf0(xn,szNzAzT0)& sdtlpdtrp0(xe,xn) = xp ) ),
% 12.49/2.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.49/2.09 fof(f113,hypothesis,(
% 12.49/2.09 ( (! [W0] :( aElementOf0(W0,xP)=> aElementOf0(W0,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ))& aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ) ),
% 12.49/2.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.49/2.09 fof(f114,hypothesis,(
% 12.49/2.09 ( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xn))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0) ))& aSet0(xD)& (! [W0] :( aElementOf0(W0,xD)<=> ( aElement0(W0)& aElementOf0(W0,sdtlpdtrp0(xN,xn))& W0 != szmzizndt0(sdtlpdtrp0(xN,xn)) ) ))& xD = sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))) ) ),
% 12.49/2.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.49/2.09 fof(f115,conjecture,(
% 12.49/2.09 ( (! [W0] :( aElementOf0(W0,xP)=> aElementOf0(W0,xD) ))| aSubsetOf0(xP,xD)| aElementOf0(xP,slbdtsldtrb0(xD,xk)) ) ),
% 12.49/2.09 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 12.49/2.09 fof(f116,negated_conjecture,(
% 12.49/2.09 ~(( (! [W0] :( aElementOf0(W0,xP)=> aElementOf0(W0,xD) ))| aSubsetOf0(xP,xD)| aElementOf0(xP,slbdtsldtrb0(xD,xk)) ) )),
% 12.49/2.09 inference(negated_conjecture,[status(cth)],[f115])).
% 12.49/2.09 fof(f413,plain,(
% 12.49/2.09 ((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)))))))),
% 12.49/2.09 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 12.49/2.09 fof(f414,definition,(
% 12.49/2.09 ![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))))),
% 12.49/2.09 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 12.49/2.09 fof(f415,plain,(
% 12.49/2.09 ((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)))))))),
% 12.49/2.09 inference(formula_renaming,[status(thm)],[f413,f414])).
% 12.49/2.09 fof(f416,plain,(
% 12.49/2.09 ((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)))))))),
% 12.49/2.09 inference(NNF_transformation,[status(thm)],[f415])).
% 12.49/2.09 fof(f417,plain,(
% 12.49/2.09 ((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)))))))),
% 12.49/2.09 inference(miniscoping,[status(thm)],[f416])).
% 12.49/2.09 fof(f429,plain,(
% 12.49/2.09 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|sP4_prd(X0)|~aElementOf0(X1,sdtlpdtrp0(xN,szszuzczcdt0(X0)))|aElementOf0(X1,sdtmndt0(sdtlpdtrp0(xN,X0),szmzizndt0(sdtlpdtrp0(xN,X0)))))),
% 12.49/2.09 inference(cnf_transformation,[status(thm)],[f417])).
% 12.49/2.09 fof(f432,plain,(
% 12.49/2.09 ![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))))),
% 12.49/2.09 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 12.49/2.09 fof(f435,plain,(
% 12.49/2.09 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0))),
% 12.49/2.09 inference(cnf_transformation,[status(thm)],[f432])).
% 12.49/2.09 fof(f436,plain,(
% 12.49/2.09 ![X0]: (~aElementOf0(X0,szNzAzT0)|isCountable0(sdtlpdtrp0(xN,X0)))),
% 12.49/2.09 inference(cnf_transformation,[status(thm)],[f432])).
% 12.49/2.09 fof(f653,plain,(
% 12.49/2.09 aElementOf0(xn,szNzAzT0)),
% 12.49/2.09 inference(cnf_transformation,[status(thm)],[f111])).
% 12.49/2.09 fof(f656,plain,(
% 12.49/2.09 (![W0]: (~aElementOf0(W0,xP)|aElementOf0(W0,sdtlpdtrp0(xN,szszuzczcdt0(xn)))))&aSubsetOf0(xP,sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 12.49/2.09 inference(pre_NNF_transformation,[status(thm)],[f113])).
% 12.49/2.09 fof(f657,plain,(
% 12.49/2.09 ![X0]: (~aElementOf0(X0,xP)|aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn))))),
% 12.49/2.09 inference(cnf_transformation,[status(thm)],[f656])).
% 12.49/2.09 fof(f659,plain,(
% 12.49/2.09 (((![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xn))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)))&aSet0(xD))&(![W0]: (aElementOf0(W0,xD)<=>((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xn)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xn))))))&xD=sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))),
% 12.49/2.09 inference(pre_NNF_transformation,[status(thm)],[f114])).
% 12.49/2.09 fof(f660,plain,(
% 12.49/2.09 (((![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xn))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)))&aSet0(xD))&(![W0]: ((~aElementOf0(W0,xD)|((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xn)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xn))))&(aElementOf0(W0,xD)|((~aElement0(W0)|~aElementOf0(W0,sdtlpdtrp0(xN,xn)))|W0=szmzizndt0(sdtlpdtrp0(xN,xn)))))))&xD=sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))),
% 12.49/2.09 inference(NNF_transformation,[status(thm)],[f659])).
% 12.49/2.09 fof(f661,plain,(
% 12.49/2.09 (((![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xn))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xn)),W0)))&aSet0(xD))&((![W0]: (~aElementOf0(W0,xD)|((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xn)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xn)))))&(![W0]: (aElementOf0(W0,xD)|((~aElement0(W0)|~aElementOf0(W0,sdtlpdtrp0(xN,xn)))|W0=szmzizndt0(sdtlpdtrp0(xN,xn)))))))&xD=sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))),
% 12.49/2.09 inference(miniscoping,[status(thm)],[f660])).
% 12.49/2.09 fof(f668,plain,(
% 12.49/2.09 xD=sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn)))),
% 12.49/2.09 inference(cnf_transformation,[status(thm)],[f661])).
% 12.49/2.09 fof(f669,plain,(
% 12.49/2.09 (((?[W0]: (aElementOf0(W0,xP)&~aElementOf0(W0,xD)))&~aSubsetOf0(xP,xD))&~aElementOf0(xP,slbdtsldtrb0(xD,xk)))),
% 12.49/2.09 inference(pre_NNF_transformation,[status(thm)],[f116])).
% 12.49/2.09 fof(f670,plain,(
% 12.49/2.09 ((aElementOf0(sK38_skl,xP)&~aElementOf0(sK38_skl,xD))&~aSubsetOf0(xP,xD))&~aElementOf0(xP,slbdtsldtrb0(xD,xk))),
% 12.49/2.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl]),skolemize(W0,sK38_skl)],[f669])).
% 12.49/2.09 fof(f671,plain,(
% 12.49/2.09 aElementOf0(sK38_skl,xP)),
% 12.49/2.09 inference(cnf_transformation,[status(thm)],[f670])).
% 12.49/2.09 fof(f672,plain,(
% 12.49/2.09 ~aElementOf0(sK38_skl,xD)),
% 12.49/2.09 inference(cnf_transformation,[status(thm)],[f670])).
% 12.49/2.09 fof(f726,plain,(
% 12.49/2.09 ![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)))))),
% 12.49/2.09 inference(NNF_transformation,[status(thm)],[f414])).
% 12.49/2.09 fof(f727,plain,(
% 12.49/2.09 (![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)))))),
% 12.49/2.09 inference(miniscoping,[status(thm)],[f726])).
% 12.49/2.09 fof(f728,plain,(
% 12.49/2.09 (![W0]: (~sP4_prd(W0)|(((~aSet0(sdtlpdtrp0(xN,W0))|(aElementOf0(sK50_skl(W0),sdtlpdtrp0(xN,W0))&~aElementOf0(sK50_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)))))),
% 12.49/2.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK50_skl]),skolemize(W1,sK50_skl(W0))],[f727])).
% 12.49/2.09 fof(f731,plain,(
% 12.49/2.09 ![X0]: (~sP4_prd(X0)|~aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0)|~isCountable0(sdtlpdtrp0(xN,X0)))),
% 12.49/2.09 inference(cnf_transformation,[status(thm)],[f728])).
% 10.48/2.12 fof(f2356,plain,(
% 10.48/2.12 aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0)),
% 10.48/2.12 inference(resolution,[status(thm)],[f653,f435])).
% 10.48/2.12 fof(f7899,plain,(
% 10.48/2.12 aElementOf0(sK38_skl,sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 10.48/2.12 inference(resolution,[status(thm)],[f657,f671])).
% 10.48/2.12 fof(f7927,plain,(
% 10.48/2.12 ~aElementOf0(xn,szNzAzT0)|sP4_prd(xn)|aElementOf0(sK38_skl,sdtmndt0(sdtlpdtrp0(xN,xn),szmzizndt0(sdtlpdtrp0(xN,xn))))),
% 10.48/2.12 inference(resolution,[status(thm)],[f7899,f429])).
% 10.48/2.12 fof(f7933,plain,(
% 10.48/2.12 ~aElementOf0(xn,szNzAzT0)|sP4_prd(xn)|aElementOf0(sK38_skl,xD)),
% 10.48/2.12 inference(forward_demodulation,[status(thm)],[f668,f7927])).
% 10.48/2.12 fof(f7934,plain,(
% 10.48/2.12 sP4_prd(xn)|aElementOf0(sK38_skl,xD)),
% 10.48/2.12 inference(forward_subsumption_resolution,[status(thm)],[f7933,f653])).
% 10.48/2.12 fof(f7936,plain,(
% 10.48/2.12 sP4_prd(xn)),
% 10.48/2.12 inference(forward_subsumption_resolution,[status(thm)],[f7934,f672])).
% 10.48/2.12 fof(f9009,plain,(
% 10.48/2.12 ~aSubsetOf0(sdtlpdtrp0(xN,xn),szNzAzT0)|~isCountable0(sdtlpdtrp0(xN,xn))),
% 10.48/2.12 inference(resolution,[status(thm)],[f731,f7936])).
% 10.48/2.12 fof(f9010,plain,(
% 10.48/2.12 ~isCountable0(sdtlpdtrp0(xN,xn))),
% 10.48/2.12 inference(forward_subsumption_resolution,[status(thm)],[f9009,f2356])).
% 10.48/2.12 fof(f9044,plain,(
% 10.48/2.12 ~aElementOf0(xn,szNzAzT0)),
% 10.48/2.12 inference(resolution,[status(thm)],[f9010,f436])).
% 10.48/2.12 fof(f9045,plain,(
% 10.48/2.12 $false),
% 10.48/2.12 inference(forward_subsumption_resolution,[status(thm)],[f9044,f653])).
% 10.48/2.12 % SZS output end CNFRefutation for theBenchmark.p
% 10.48/2.13 % Elapsed time: 1.751887 seconds
% 10.48/2.13 % CPU time: 13.414400 seconds
% 10.48/2.13 % Total memory used: 259.169 MB
% 10.48/2.13 % Net memory used: 248.097 MB
%------------------------------------------------------------------------------