%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM592+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 : n006.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:18 PM UTC 2026
% Result : Theorem 20.49s 8.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM592+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/5.40 % Computer : n006.cluster.edu
% 0.15/5.40 % Model : x86_64 x86_64
% 0.15/5.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.40 % Memory : 8046.5625MB
% 0.15/5.40 % OS : Linux 6.8.0-71-generic
% 0.15/5.40 % CPULimit : 300
% 0.15/5.40 % WCLimit : 300
% 0.15/5.40 % DateTime : Mon Sep 21 02:42:49 UTC 2026
% 0.15/5.40 % CPUTime :
% 0.15/5.44 % Drodi V4.1.1
% 20.49/8.47 % Refutation found
% 20.49/8.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 20.49/8.47 % SZS output start CNFRefutation for theBenchmark
% 20.49/8.47 fof(f91,hypothesis,(
% 20.49/8.47 ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))& (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0) ))& aSet0(xY)& (! [W0] :( aElementOf0(W0,xY)<=> ( aElement0(W0)& aElementOf0(W0,sdtlpdtrp0(xN,xi))& W0 != szmzizndt0(sdtlpdtrp0(xN,xi)) ) ))& xY = sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))& xd = sdtlpdtrp0(xC,xi) ) ),
% 20.49/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.49/8.47 fof(f93,hypothesis,(
% 20.49/8.47 ( aElementOf0(xu,xT)& aSet0(xX)& (! [W0] :( aElementOf0(W0,xX)=> aElementOf0(W0,xY) ))& aSubsetOf0(xX,xY)& isCountable0(xX)& (! [W0] :( ( aSet0(W0)& ( ( ( (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xX) ))| aSubsetOf0(W0,xX) )& sbrdtbr0(W0) = xk )| aElementOf0(W0,slbdtsldtrb0(xX,xk)) ) )=> sdtlpdtrp0(xd,W0) = xu ) )) ),
% 20.49/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.49/8.47 fof(f94,conjecture,(
% 20.49/8.47 (? [W0] :( aElementOf0(W0,xT)& (? [W1] :( ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))& (! [W2] :( aElementOf0(W2,sdtlpdtrp0(xN,xi))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W2) ) ))=> ( ( aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))& (! [W2] :( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))<=> ( aElement0(W2)& aElementOf0(W2,sdtlpdtrp0(xN,xi))& W2 != szmzizndt0(sdtlpdtrp0(xN,xi)) ) ) ))=> ( ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ) ))| aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ) ) )& isCountable0(W1)& (! [W2] :( ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)=> aElementOf0(W3,W1) ))& aSubsetOf0(W2,W1)& sbrdtbr0(W2) = xk& aElementOf0(W2,slbdtsldtrb0(W1,xk)) )=> sdtlpdtrp0(sdtlpdtrp0(xC,xi),W2) = W0 ) )) )) )),
% 20.49/8.47 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 20.49/8.47 fof(f95,negated_conjecture,(
% 20.49/8.47 ~((? [W0] :( aElementOf0(W0,xT)& (? [W1] :( ( ( aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))& (! [W2] :( aElementOf0(W2,sdtlpdtrp0(xN,xi))=> sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W2) ) ))=> ( ( aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))& (! [W2] :( aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))<=> ( aElement0(W2)& aElementOf0(W2,sdtlpdtrp0(xN,xi))& W2 != szmzizndt0(sdtlpdtrp0(xN,xi)) ) ) ))=> ( ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ) ))| aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))) ) ) )& isCountable0(W1)& (! [W2] :( ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)=> aElementOf0(W3,W1) ))& aSubsetOf0(W2,W1)& sbrdtbr0(W2) = xk& aElementOf0(W2,slbdtsldtrb0(W1,xk)) )=> sdtlpdtrp0(sdtlpdtrp0(xC,xi),W2) = W0 ) )) )) ))),
% 20.49/8.47 inference(negated_conjecture,[status(cth)],[f94])).
% 20.49/8.47 fof(f502,plain,(
% 20.49/8.47 ((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(xY))&(![W0]: (aElementOf0(W0,xY)<=>((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))))&xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&xd=sdtlpdtrp0(xC,xi)),
% 20.49/8.47 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 20.49/8.47 fof(f503,plain,(
% 20.49/8.47 ((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(xY))&(![W0]: ((~aElementOf0(W0,xY)|((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xi))))&(aElementOf0(W0,xY)|((~aElement0(W0)|~aElementOf0(W0,sdtlpdtrp0(xN,xi)))|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))))&xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&xd=sdtlpdtrp0(xC,xi)),
% 20.49/8.47 inference(NNF_transformation,[status(thm)],[f502])).
% 20.49/8.47 fof(f504,plain,(
% 20.49/8.47 ((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W0))))&aSet0(xY))&((![W0]: (~aElementOf0(W0,xY)|((aElement0(W0)&aElementOf0(W0,sdtlpdtrp0(xN,xi)))&~W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))&(![W0]: (aElementOf0(W0,xY)|((~aElement0(W0)|~aElementOf0(W0,sdtlpdtrp0(xN,xi)))|W0=szmzizndt0(sdtlpdtrp0(xN,xi)))))))&xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&xd=sdtlpdtrp0(xC,xi)),
% 20.49/8.47 inference(miniscoping,[status(thm)],[f503])).
% 20.49/8.47 fof(f512,plain,(
% 20.49/8.47 xY=sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))),
% 20.49/8.47 inference(cnf_transformation,[status(thm)],[f504])).
% 20.49/8.47 fof(f513,plain,(
% 20.49/8.47 xd=sdtlpdtrp0(xC,xi)),
% 20.49/8.47 inference(cnf_transformation,[status(thm)],[f504])).
% 20.49/8.47 fof(f533,plain,(
% 20.49/8.47 ((((aElementOf0(xu,xT)&aSet0(xX))&(![W0]: (~aElementOf0(W0,xX)|aElementOf0(W0,xY))))&aSubsetOf0(xX,xY))&isCountable0(xX))&(![W0]: ((~aSet0(W0)|((((?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xX)))&~aSubsetOf0(W0,xX))|~sbrdtbr0(W0)=xk)&~aElementOf0(W0,slbdtsldtrb0(xX,xk))))|sdtlpdtrp0(xd,W0)=xu))),
% 20.49/8.47 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 20.49/8.47 fof(f534,plain,(
% 20.49/8.47 ((((aElementOf0(xu,xT)&aSet0(xX))&(![W0]: (~aElementOf0(W0,xX)|aElementOf0(W0,xY))))&aSubsetOf0(xX,xY))&isCountable0(xX))&(![W0]: ((~aSet0(W0)|((((aElementOf0(sK29_skl(W0),W0)&~aElementOf0(sK29_skl(W0),xX))&~aSubsetOf0(W0,xX))|~sbrdtbr0(W0)=xk)&~aElementOf0(W0,slbdtsldtrb0(xX,xk))))|sdtlpdtrp0(xd,W0)=xu))),
% 20.49/8.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK29_skl]),skolemize(W1,sK29_skl(W0))],[f533])).
% 20.49/8.47 fof(f535,plain,(
% 20.49/8.47 aElementOf0(xu,xT)),
% 20.49/8.47 inference(cnf_transformation,[status(thm)],[f534])).
% 20.49/8.47 fof(f538,plain,(
% 20.49/8.47 aSubsetOf0(xX,xY)),
% 20.49/8.47 inference(cnf_transformation,[status(thm)],[f534])).
% 20.49/8.47 fof(f539,plain,(
% 20.49/8.47 isCountable0(xX)),
% 20.49/8.47 inference(cnf_transformation,[status(thm)],[f534])).
% 20.49/8.47 fof(f543,plain,(
% 20.49/8.47 ![X0]: (~aSet0(X0)|~aElementOf0(X0,slbdtsldtrb0(xX,xk))|sdtlpdtrp0(xd,X0)=xu)),
% 20.49/8.47 inference(cnf_transformation,[status(thm)],[f534])).
% 20.49/8.47 fof(f544,plain,(
% 20.49/8.47 (![W0]: (~aElementOf0(W0,xT)|(![W1]: ((((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W2))))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&(![W2]: (aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))<=>((aElement0(W2)&aElementOf0(W2,sdtlpdtrp0(xN,xi)))&~W2=szmzizndt0(sdtlpdtrp0(xN,xi))))))&((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))|~isCountable0(W1))|(?[W2]: (((((aSet0(W2)&(![W3]: (~aElementOf0(W3,W2)|aElementOf0(W3,W1))))&aSubsetOf0(W2,W1))&sbrdtbr0(W2)=xk)&aElementOf0(W2,slbdtsldtrb0(W1,xk)))&~sdtlpdtrp0(sdtlpdtrp0(xC,xi),W2)=W0))))))),
% 20.49/8.47 inference(pre_NNF_transformation,[status(thm)],[f95])).
% 20.49/8.47 fof(f545,definition,(
% 20.49/8.47 ![W1]: (sP9_prd(W1)<=>(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W2))))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&(![W2]: (aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))<=>((aElement0(W2)&aElementOf0(W2,sdtlpdtrp0(xN,xi)))&~W2=szmzizndt0(sdtlpdtrp0(xN,xi))))))&((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))|~isCountable0(W1)))),
% 20.49/8.47 introduced(definition,[new_symbols(definition,[sP9_prd])],[])).
% 20.49/8.47 fof(f546,plain,(
% 20.49/8.47 ![W0]: (~aElementOf0(W0,xT)|(![W1]: (sP9_prd(W1)|(?[W2]: (((((aSet0(W2)&(![W3]: (~aElementOf0(W3,W2)|aElementOf0(W3,W1))))&aSubsetOf0(W2,W1))&sbrdtbr0(W2)=xk)&aElementOf0(W2,slbdtsldtrb0(W1,xk)))&~sdtlpdtrp0(sdtlpdtrp0(xC,xi),W2)=W0)))))),
% 20.49/8.47 inference(formula_renaming,[status(thm)],[f544,f545])).
% 20.49/8.47 fof(f547,plain,(
% 20.49/8.47 ![W0]: (~aElementOf0(W0,xT)|(![W1]: (sP9_prd(W1)|(((((aSet0(sK30_skl(W1,W0))&(![W3]: (~aElementOf0(W3,sK30_skl(W1,W0))|aElementOf0(W3,W1))))&aSubsetOf0(sK30_skl(W1,W0),W1))&sbrdtbr0(sK30_skl(W1,W0))=xk)&aElementOf0(sK30_skl(W1,W0),slbdtsldtrb0(W1,xk)))&~sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK30_skl(W1,W0))=W0))))),
% 20.49/8.47 inference(skolemize,[status(esa),new_symbols(skolem,[sK30_skl]),skolemize(W2,sK30_skl(W1,W0))],[f546])).
% 20.49/8.47 fof(f548,plain,(
% 20.49/8.47 ![X0,X1]: (~aElementOf0(X0,xT)|sP9_prd(X1)|aSet0(sK30_skl(X1,X0)))),
% 20.49/8.47 inference(cnf_transformation,[status(thm)],[f547])).
% 20.49/8.47 fof(f552,plain,(
% 20.49/8.47 ![X0,X1]: (~aElementOf0(X0,xT)|sP9_prd(X1)|aElementOf0(sK30_skl(X1,X0),slbdtsldtrb0(X1,xk)))),
% 20.49/8.47 inference(cnf_transformation,[status(thm)],[f547])).
% 20.49/8.47 fof(f553,plain,(
% 20.49/8.47 ![X0,X1]: (~aElementOf0(X0,xT)|sP9_prd(X1)|~sdtlpdtrp0(sdtlpdtrp0(xC,xi),sK30_skl(X1,X0))=X0)),
% 20.49/8.47 inference(cnf_transformation,[status(thm)],[f547])).
% 20.49/8.47 fof(f675,definition,(
% 20.49/8.47 ![W2]: (sP16_prd(W2)<=>(aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))<=>((aElement0(W2)&aElementOf0(W2,sdtlpdtrp0(xN,xi)))&~W2=szmzizndt0(sdtlpdtrp0(xN,xi)))))),
% 20.49/8.47 introduced(definition,[new_symbols(definition,[sP16_prd])],[])).
% 20.49/8.47 fof(f676,plain,(
% 20.49/8.47 ![W1]: (sP9_prd(W1)<=>(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W2))))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&(![W2]: sP16_prd(W2)))&((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))|~isCountable0(W1)))),
% 20.49/8.47 inference(formula_renaming,[status(thm)],[f545,f675])).
% 20.49/8.47 fof(f677,plain,(
% 20.49/8.47 ![W1]: ((~sP9_prd(W1)|(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W2))))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&(![W2]: sP16_prd(W2)))&((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))|~isCountable0(W1)))&(sP9_prd(W1)|(((~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))|(?[W2]: (aElementOf0(W2,sdtlpdtrp0(xN,xi))&~sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W2))))|((~aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|(?[W2]: ~sP16_prd(W2)))|((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))|aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&isCountable0(W1))))),
% 20.49/8.47 inference(NNF_transformation,[status(thm)],[f676])).
% 20.49/8.47 fof(f678,plain,(
% 20.49/8.47 (![W1]: (~sP9_prd(W1)|(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W2))))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&(![W2]: sP16_prd(W2)))&((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))|~isCountable0(W1))))&(![W1]: (sP9_prd(W1)|(((~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))|(?[W2]: (aElementOf0(W2,sdtlpdtrp0(xN,xi))&~sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W2))))|((~aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|(?[W2]: ~sP16_prd(W2)))|((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))|aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&isCountable0(W1))))),
% 20.49/8.47 inference(miniscoping,[status(thm)],[f677])).
% 20.49/8.47 fof(f679,plain,(
% 20.49/8.47 (![W1]: (~sP9_prd(W1)|(((aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))&(![W2]: (~aElementOf0(W2,sdtlpdtrp0(xN,xi))|sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),W2))))&((aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))&(![W2]: sP16_prd(W2)))&((~aSet0(W1)|(aElementOf0(sK53_skl(W1),W1)&~aElementOf0(sK53_skl(W1),sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))))&~aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))|~isCountable0(W1))))&(![W1]: (sP9_prd(W1)|(((~aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))|(aElementOf0(sK54_skl(W1),sdtlpdtrp0(xN,xi))&~sdtlseqdt0(szmzizndt0(sdtlpdtrp0(xN,xi)),sK54_skl(W1))))|((~aSet0(sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~sP16_prd(sK55_skl(W1)))|((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))|aSubsetOf0(W1,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi)))))))&isCountable0(W1))))),
% 20.49/8.50 inference(skolemize,[status(esa),new_symbols(skolem,[sK53_skl,sK54_skl,sK55_skl]),skolemize(W2,sK53_skl(W1)),skolemize(W2,sK54_skl(W1)),skolemize(W2,sK55_skl(W1))],[f678])).
% 20.49/8.50 fof(f686,plain,(
% 20.49/8.50 ![X0]: (~sP9_prd(X0)|~aSubsetOf0(X0,sdtmndt0(sdtlpdtrp0(xN,xi),szmzizndt0(sdtlpdtrp0(xN,xi))))|~isCountable0(X0))),
% 20.49/8.50 inference(cnf_transformation,[status(thm)],[f679])).
% 20.49/8.50 fof(f1996,plain,(
% 20.49/8.50 ![X0,X1]: (~aElementOf0(X0,xT)|sP9_prd(X1)|~sdtlpdtrp0(xd,sK30_skl(X1,X0))=X0)),
% 20.49/8.50 inference(backward_demodulation,[status(thm)],[f513,f553])).
% 20.49/8.50 fof(f2082,plain,(
% 20.49/8.50 ![X0]: (sP9_prd(X0)|~sdtlpdtrp0(xd,sK30_skl(X0,xu))=xu)),
% 20.49/8.50 inference(resolution,[status(thm)],[f1996,f535])).
% 20.49/8.50 fof(f4265,plain,(
% 20.49/8.50 ![X0]: (~sP9_prd(X0)|~aSubsetOf0(X0,xY)|~isCountable0(X0))),
% 20.49/8.50 inference(backward_demodulation,[status(thm)],[f512,f686])).
% 20.49/8.50 fof(f4601,plain,(
% 20.49/8.50 ![X0]: (~aSet0(sK30_skl(xX,X0))|sdtlpdtrp0(xd,sK30_skl(xX,X0))=xu|~aElementOf0(X0,xT)|sP9_prd(xX))),
% 20.49/8.50 inference(resolution,[status(thm)],[f543,f552])).
% 20.49/8.50 fof(f4604,plain,(
% 20.49/8.50 ![X0]: (sdtlpdtrp0(xd,sK30_skl(xX,X0))=xu|~aElementOf0(X0,xT)|sP9_prd(xX))),
% 20.49/8.50 inference(forward_subsumption_resolution,[status(thm)],[f4601,f548])).
% 20.49/8.50 fof(f7085,plain,(
% 20.49/8.50 sdtlpdtrp0(xd,sK30_skl(xX,xu))=xu|sP9_prd(xX)),
% 20.49/8.50 inference(resolution,[status(thm)],[f4604,f535])).
% 20.49/8.50 fof(f7090,plain,(
% 20.49/8.50 sP9_prd(xX)),
% 20.49/8.50 inference(forward_subsumption_resolution,[status(thm)],[f7085,f2082])).
% 20.49/8.50 fof(f7096,plain,(
% 20.49/8.50 ~aSubsetOf0(xX,xY)|~isCountable0(xX)),
% 20.49/8.50 inference(resolution,[status(thm)],[f7090,f4265])).
% 20.49/8.50 fof(f7101,plain,(
% 20.49/8.50 ~isCountable0(xX)),
% 20.49/8.50 inference(forward_subsumption_resolution,[status(thm)],[f7096,f538])).
% 20.49/8.50 fof(f7103,plain,(
% 20.49/8.50 $false),
% 20.49/8.50 inference(forward_subsumption_resolution,[status(thm)],[f7101,f539])).
% 20.49/8.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.90/8.52 % Elapsed time: 3.104118 seconds
% 0.90/8.52 % CPU time: 22.087118 seconds
% 0.90/8.52 % Total memory used: 283.464 MB
% 0.90/8.52 % Net memory used: 270.769 MB
%------------------------------------------------------------------------------