%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM580+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 : n019.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 22.91s 3.48s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM580+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.11/0.36 % Computer : n019.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 02:41:37 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.38 % Drodi V4.1.1
% 22.91/3.48 % Refutation found
% 22.91/3.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 22.91/3.48 % SZS output start CNFRefutation for theBenchmark
% 22.91/3.48 fof(f3,axiom,(
% 22.91/3.48 (! [W0] :( aSet0(W0)=> (! [W1] :( aElementOf0(W1,W0)=> aElement0(W1) ) )) )),
% 22.91/3.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.91/3.48 fof(f10,definition,(
% 22.91/3.48 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 22.91/3.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.91/3.48 fof(f12,axiom,(
% 22.91/3.48 (! [W0] :( aSet0(W0)=> aSubsetOf0(W0,W0) ) )),
% 22.91/3.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.91/3.48 fof(f41,axiom,(
% 22.91/3.48 (! [W0] :( aSet0(W0)=> ( aElementOf0(sbrdtbr0(W0),szNzAzT0)<=> isFinite0(W0) ) ) )),
% 22.91/3.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.91/3.48 fof(f43,axiom,(
% 22.91/3.48 (! [W0] :( ( aSet0(W0)& isFinite0(W0) )=> (! [W1] :( aElement0(W1)=> ( ~ aElementOf0(W1,W0)=> sbrdtbr0(sdtpldt0(W0,W1)) = szszuzczcdt0(sbrdtbr0(W0)) ) ) )) )),
% 22.91/3.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.91/3.48 fof(f80,hypothesis,(
% 22.91/3.48 ( aElementOf0(xk,szNzAzT0)& szszuzczcdt0(xk) = xK ) ),
% 22.91/3.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.91/3.48 fof(f82,hypothesis,(
% 22.91/3.48 (! [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)) ) ) )),
% 22.91/3.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.91/3.48 fof(f85,hypothesis,(
% 22.91/3.48 aElementOf0(xi,szNzAzT0) ),
% 22.91/3.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.91/3.48 fof(f86,hypothesis,(
% 22.91/3.48 ( 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)) ) ),
% 22.91/3.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.91/3.48 fof(f87,conjecture,(
% 22.91/3.48 ( ( 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)) ) ) ) ))=> sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = xK ) ) ),
% 22.91/3.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 22.91/3.48 fof(f88,negated_conjecture,(
% 22.91/3.48 ~(( ( 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)) ) ) ) ))=> sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi)))) = xK ) ) )),
% 22.91/3.48 inference(negated_conjecture,[status(cth)],[f87])).
% 22.91/3.48 fof(f95,plain,(
% 22.91/3.48 ![W0]: (~aSet0(W0)|(![W1]: (~aElementOf0(W1,W0)|aElement0(W1))))),
% 22.91/3.48 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 22.91/3.48 fof(f96,plain,(
% 22.91/3.48 ![X0,X1]: (~aSet0(X0)|~aElementOf0(X1,X0)|aElement0(X1))),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f95])).
% 22.91/3.48 fof(f113,plain,(
% 22.91/3.48 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 22.91/3.48 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 22.91/3.48 fof(f114,plain,(
% 22.91/3.48 ![W0]: (~aSet0(W0)|(![W1]: ((~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))&(aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 22.91/3.48 inference(NNF_transformation,[status(thm)],[f113])).
% 22.91/3.48 fof(f115,plain,(
% 22.91/3.48 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,W0))))))))),
% 22.91/3.48 inference(miniscoping,[status(thm)],[f114])).
% 22.91/3.48 fof(f116,plain,(
% 22.91/3.48 ![W0]: (~aSet0(W0)|((![W1]: (~aSubsetOf0(W1,W0)|(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0))))))&(![W1]: (aSubsetOf0(W1,W0)|(~aSet0(W1)|(aElementOf0(sK1_skl(W1,W0),W1)&~aElementOf0(sK1_skl(W1,W0),W0)))))))),
% 22.91/3.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f115])).
% 22.91/3.48 fof(f118,plain,(
% 22.91/3.48 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f116])).
% 22.91/3.48 fof(f123,plain,(
% 22.91/3.48 ![W0]: (~aSet0(W0)|aSubsetOf0(W0,W0))),
% 22.91/3.48 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 22.91/3.48 fof(f124,plain,(
% 22.91/3.48 ![X0]: (~aSet0(X0)|aSubsetOf0(X0,X0))),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f123])).
% 22.91/3.48 fof(f205,plain,(
% 22.91/3.48 ![W0]: (~aSet0(W0)|(aElementOf0(sbrdtbr0(W0),szNzAzT0)<=>isFinite0(W0)))),
% 22.91/3.48 inference(pre_NNF_transformation,[status(thm)],[f41])).
% 22.91/3.48 fof(f206,plain,(
% 22.91/3.48 ![W0]: (~aSet0(W0)|((~aElementOf0(sbrdtbr0(W0),szNzAzT0)|isFinite0(W0))&(aElementOf0(sbrdtbr0(W0),szNzAzT0)|~isFinite0(W0))))),
% 22.91/3.48 inference(NNF_transformation,[status(thm)],[f205])).
% 22.91/3.48 fof(f207,plain,(
% 22.91/3.48 ![X0]: (~aSet0(X0)|~aElementOf0(sbrdtbr0(X0),szNzAzT0)|isFinite0(X0))),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f206])).
% 22.91/3.48 fof(f213,plain,(
% 22.91/3.48 ![W0]: ((~aSet0(W0)|~isFinite0(W0))|(![W1]: (~aElement0(W1)|(aElementOf0(W1,W0)|sbrdtbr0(sdtpldt0(W0,W1))=szszuzczcdt0(sbrdtbr0(W0))))))),
% 22.91/3.48 inference(pre_NNF_transformation,[status(thm)],[f43])).
% 22.91/3.48 fof(f214,plain,(
% 22.91/3.48 ![X0,X1]: (~aSet0(X0)|~isFinite0(X0)|~aElement0(X1)|aElementOf0(X1,X0)|sbrdtbr0(sdtpldt0(X0,X1))=szszuzczcdt0(sbrdtbr0(X0)))),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f213])).
% 22.91/3.48 fof(f383,plain,(
% 22.91/3.48 aElementOf0(xk,szNzAzT0)),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f80])).
% 22.91/3.48 fof(f384,plain,(
% 22.91/3.48 szszuzczcdt0(xk)=xK),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f80])).
% 22.91/3.48 fof(f404,plain,(
% 22.91/3.48 ![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))))),
% 22.91/3.48 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 22.91/3.48 fof(f405,plain,(
% 22.91/3.48 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSet0(sdtlpdtrp0(xN,X0)))),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f404])).
% 22.91/3.48 fof(f419,plain,(
% 22.91/3.48 aElementOf0(xi,szNzAzT0)),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f85])).
% 22.91/3.48 fof(f420,plain,(
% 22.91/3.48 (((((((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))),
% 22.91/3.48 inference(pre_NNF_transformation,[status(thm)],[f86])).
% 22.91/3.48 fof(f421,plain,(
% 22.91/3.48 (((((((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))),
% 22.91/3.48 inference(NNF_transformation,[status(thm)],[f420])).
% 22.91/3.48 fof(f422,plain,(
% 22.91/3.48 (((((((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))),
% 22.91/3.48 inference(miniscoping,[status(thm)],[f421])).
% 22.91/3.48 fof(f428,plain,(
% 22.91/3.48 ![X0]: (~aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~X0=szmzizndt0(sdtlpdtrp0(xN,xi)))),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f422])).
% 22.91/3.48 fof(f430,plain,(
% 22.91/3.48 aSet0(xQ)),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f422])).
% 22.91/3.48 fof(f431,plain,(
% 22.91/3.48 ![X0]: (~aElementOf0(X0,xQ)|aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f422])).
% 22.91/3.48 fof(f433,plain,(
% 22.91/3.48 sbrdtbr0(xQ)=xk),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f422])).
% 22.91/3.48 fof(f435,plain,(
% 22.91/3.48 ((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)))))))&~sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))=xK))),
% 22.91/3.48 inference(pre_NNF_transformation,[status(thm)],[f88])).
% 22.91/3.48 fof(f436,plain,(
% 22.91/3.48 (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))))))))&~sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))=xK)),
% 22.91/3.48 inference(NNF_transformation,[status(thm)],[f435])).
% 22.91/3.48 fof(f437,plain,(
% 22.91/3.48 (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))))))))&~sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))=xK)),
% 22.91/3.48 inference(miniscoping,[status(thm)],[f436])).
% 22.91/3.48 fof(f438,plain,(
% 22.91/3.48 aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f437])).
% 22.91/3.48 fof(f445,plain,(
% 22.91/3.48 ~sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))=xK),
% 22.91/3.48 inference(cnf_transformation,[status(thm)],[f437])).
% 22.91/3.48 fof(f563,plain,(
% 22.91/3.48 ~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))),
% 22.91/3.48 inference(destructive_equality_resolution,[status(thm)],[f428])).
% 22.91/3.48 fof(f581,plain,(
% 22.91/3.48 ~aSet0(sdtlpdtrp0(xN,xi))|aElement0(szmzizndt0(sdtlpdtrp0(xN,xi)))),
% 22.91/3.53 inference(resolution,[status(thm)],[f96,f438])).
% 22.91/3.53 fof(f740,plain,(
% 22.91/3.53 aSubsetOf0(xQ,xQ)),
% 22.91/3.53 inference(resolution,[status(thm)],[f124,f430])).
% 22.91/3.53 fof(f1499,plain,(
% 22.91/3.53 ![X0]: (~isFinite0(xQ)|~aElement0(X0)|aElementOf0(X0,xQ)|sbrdtbr0(sdtpldt0(xQ,X0))=szszuzczcdt0(sbrdtbr0(xQ)))),
% 22.91/3.53 inference(resolution,[status(thm)],[f214,f430])).
% 22.91/3.53 fof(f1543,plain,(
% 22.91/3.53 ![X0]: (~isFinite0(xQ)|~aElement0(X0)|aElementOf0(X0,xQ)|sbrdtbr0(sdtpldt0(xQ,X0))=szszuzczcdt0(xk))),
% 22.91/3.53 inference(forward_demodulation,[status(thm)],[f433,f1499])).
% 22.91/3.53 fof(f1544,plain,(
% 22.91/3.53 ![X0]: (~isFinite0(xQ)|~aElement0(X0)|aElementOf0(X0,xQ)|sbrdtbr0(sdtpldt0(xQ,X0))=xK)),
% 22.91/3.53 inference(forward_demodulation,[status(thm)],[f384,f1543])).
% 22.91/3.53 fof(f1831,plain,(
% 22.91/3.53 aSet0(sdtlpdtrp0(xN,xi))),
% 22.91/3.53 inference(resolution,[status(thm)],[f405,f419])).
% 22.91/3.53 fof(f1854,plain,(
% 22.91/3.53 aElement0(szmzizndt0(sdtlpdtrp0(xN,xi)))),
% 22.91/3.53 inference(backward_subsumption_resolution,[status(thm)],[f581,f1831])).
% 22.91/3.53 fof(f2762,plain,(
% 22.91/3.53 ~aSet0(xQ)|~aElementOf0(xk,szNzAzT0)|isFinite0(xQ)),
% 22.91/3.53 inference(paramodulation,[status(thm)],[f433,f207])).
% 22.91/3.53 fof(f2764,plain,(
% 22.91/3.53 ~aElementOf0(xk,szNzAzT0)|isFinite0(xQ)),
% 22.91/3.53 inference(forward_subsumption_resolution,[status(thm)],[f2762,f430])).
% 22.91/3.53 fof(f3119,plain,(
% 22.91/3.53 ![X0,X1]: (aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~aSet0(xQ)|~aSubsetOf0(X1,xQ)|~aElementOf0(X0,X1))),
% 22.91/3.53 inference(resolution,[status(thm)],[f431,f118])).
% 22.91/3.53 fof(f3120,plain,(
% 22.91/3.53 ![X0,X1]: (aElementOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~aSubsetOf0(X1,xQ)|~aElementOf0(X0,X1))),
% 22.91/3.53 inference(forward_subsumption_resolution,[status(thm)],[f3119,f430])).
% 22.91/3.53 fof(f5508,plain,(
% 22.91/3.53 isFinite0(xQ)),
% 22.91/3.53 inference(forward_subsumption_resolution,[status(thm)],[f2764,f383])).
% 22.91/3.53 fof(f17467,plain,(
% 22.91/3.53 ![X0]: (~aElement0(X0)|aElementOf0(X0,xQ)|sbrdtbr0(sdtpldt0(xQ,X0))=xK)),
% 22.91/3.53 inference(forward_subsumption_resolution,[status(thm)],[f1544,f5508])).
% 22.91/3.53 fof(f17490,plain,(
% 22.91/3.53 aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),xQ)|sbrdtbr0(sdtpldt0(xQ,szmzizndt0(sdtlpdtrp0(xN,xi))))=xK),
% 22.91/3.53 inference(resolution,[status(thm)],[f17467,f1854])).
% 22.91/3.53 fof(f17591,plain,(
% 22.91/3.53 aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),xQ)),
% 22.91/3.53 inference(forward_subsumption_resolution,[status(thm)],[f17490,f445])).
% 22.91/3.53 fof(f37129,plain,(
% 22.91/3.53 aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~aSubsetOf0(xQ,xQ)),
% 22.91/3.53 inference(resolution,[status(thm)],[f3120,f17591])).
% 22.91/3.53 fof(f37137,plain,(
% 22.91/3.53 ~aSubsetOf0(xQ,xQ)),
% 22.91/3.53 inference(forward_subsumption_resolution,[status(thm)],[f37129,f563])).
% 22.91/3.53 fof(f37142,plain,(
% 22.91/3.53 $false),
% 22.91/3.53 inference(forward_subsumption_resolution,[status(thm)],[f37137,f740])).
% 22.91/3.53 % SZS output end CNFRefutation for theBenchmark.p
% 1.83/3.54 % Elapsed time: 3.162867 seconds
% 1.83/3.54 % CPU time: 24.664806 seconds
% 1.83/3.54 % Total memory used: 361.478 MB
% 1.83/3.54 % Net memory used: 343.204 MB
%------------------------------------------------------------------------------