%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM633+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 : n016.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 7.17s 1.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM633+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.55 % Computer : n016.cluster.edu
% 0.08/0.55 % Model : x86_64 x86_64
% 0.08/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.55 % Memory : 8046.5625MB
% 0.08/0.55 % OS : Linux 6.8.0-71-generic
% 0.08/0.55 % CPULimit : 300
% 0.08/0.55 % WCLimit : 300
% 0.08/0.55 % DateTime : Mon Sep 21 02:50:53 UTC 2026
% 0.08/0.55 % CPUTime :
% 0.12/0.58 % Drodi V4.1.1
% 7.17/1.58 % Refutation found
% 7.17/1.58 % SZS status Theorem for theBenchmark: Theorem is valid
% 7.17/1.58 % SZS output start CNFRefutation for theBenchmark
% 7.17/1.58 fof(f94,hypothesis,(
% 7.17/1.58 ( aElementOf0(szDzizrdt0(xd),xT)& aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd)))& (! [W0] :( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))<=> ( aElementOf0(W0,szDzozmdt0(xd))& sdtlpdtrp0(xd,W0) = szDzizrdt0(xd) ) ) )) ),
% 7.17/1.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.17/1.58 fof(f96,hypothesis,(
% 7.17/1.58 ( aSet0(xO)& isCountable0(xO) ) ),
% 7.17/1.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.17/1.58 fof(f98,hypothesis,(
% 7.17/1.58 ( (! [W0] :( aElementOf0(W0,xO)=> aElementOf0(W0,xS) ))& aSubsetOf0(xO,xS) ) ),
% 7.17/1.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.17/1.58 fof(f99,conjecture,(
% 7.17/1.58 ( (! [W0] :( ( ( ( ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xO) ) ))| aSubsetOf0(W0,xO) )& sbrdtbr0(W0) = xK )| aElementOf0(W0,slbdtsldtrb0(xO,xK)) )=> ( ~ ( ~ (? [W1] : aElementOf0(W1,W0))| W0 = slcrc0 )& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,szNzAzT0) ))& aSubsetOf0(W0,szNzAzT0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xS) ))& aSubsetOf0(W0,xS)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xS) ))& aSubsetOf0(W0,xS)& aElementOf0(W0,szDzozmdt0(xc))& sdtlpdtrp0(xc,W0) = szDzizrdt0(xd) ) ))=> (? [W0] :( aElementOf0(W0,xT)& (? [W1] :( ( ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,xS) ) ))| aSubsetOf0(W1,xS) )& isCountable0(W1)& (! [W2] :( ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)=> aElementOf0(W3,W1) ))& aSubsetOf0(W2,W1)& sbrdtbr0(W2) = xK& aElementOf0(W2,slbdtsldtrb0(W1,xK)) )=> sdtlpdtrp0(xc,W2) = W0 ) )) )) )) ),
% 7.17/1.58 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 7.17/1.58 fof(f100,negated_conjecture,(
% 7.17/1.58 ~(( (! [W0] :( ( ( ( ( aSet0(W0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xO) ) ))| aSubsetOf0(W0,xO) )& sbrdtbr0(W0) = xK )| aElementOf0(W0,slbdtsldtrb0(xO,xK)) )=> ( ~ ( ~ (? [W1] : aElementOf0(W1,W0))| W0 = slcrc0 )& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,szNzAzT0) ))& aSubsetOf0(W0,szNzAzT0)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xS) ))& aSubsetOf0(W0,xS)& (! [W1] :( aElementOf0(W1,W0)=> aElementOf0(W1,xS) ))& aSubsetOf0(W0,xS)& aElementOf0(W0,szDzozmdt0(xc))& sdtlpdtrp0(xc,W0) = szDzizrdt0(xd) ) ))=> (? [W0] :( aElementOf0(W0,xT)& (? [W1] :( ( ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,xS) ) ))| aSubsetOf0(W1,xS) )& isCountable0(W1)& (! [W2] :( ( aSet0(W2)& (! [W3] :( aElementOf0(W3,W2)=> aElementOf0(W3,W1) ))& aSubsetOf0(W2,W1)& sbrdtbr0(W2) = xK& aElementOf0(W2,slbdtsldtrb0(W1,xK)) )=> sdtlpdtrp0(xc,W2) = W0 ) )) )) )) )),
% 7.17/1.58 inference(negated_conjecture,[status(cth)],[f99])).
% 7.17/1.58 fof(f556,plain,(
% 7.17/1.58 (aElementOf0(szDzizrdt0(xd),xT)&aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))))&(![W0]: ((~aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(aElementOf0(W0,szDzozmdt0(xd))&sdtlpdtrp0(xd,W0)=szDzizrdt0(xd)))&(aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(~aElementOf0(W0,szDzozmdt0(xd))|~sdtlpdtrp0(xd,W0)=szDzizrdt0(xd)))))),
% 7.17/1.58 inference(NNF_transformation,[status(thm)],[f94])).
% 7.17/1.58 fof(f557,plain,(
% 7.17/1.58 (aElementOf0(szDzizrdt0(xd),xT)&aSet0(sdtlbdtrb0(xd,szDzizrdt0(xd))))&((![W0]: (~aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(aElementOf0(W0,szDzozmdt0(xd))&sdtlpdtrp0(xd,W0)=szDzizrdt0(xd))))&(![W0]: (aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))|(~aElementOf0(W0,szDzozmdt0(xd))|~sdtlpdtrp0(xd,W0)=szDzizrdt0(xd)))))),
% 7.17/1.58 inference(miniscoping,[status(thm)],[f556])).
% 7.17/1.58 fof(f558,plain,(
% 7.17/1.58 aElementOf0(szDzizrdt0(xd),xT)),
% 7.17/1.58 inference(cnf_transformation,[status(thm)],[f557])).
% 7.17/1.58 fof(f576,plain,(
% 7.17/1.58 isCountable0(xO)),
% 7.17/1.58 inference(cnf_transformation,[status(thm)],[f96])).
% 7.17/1.58 fof(f585,plain,(
% 7.17/1.58 (![W0]: (~aElementOf0(W0,xO)|aElementOf0(W0,xS)))&aSubsetOf0(xO,xS)),
% 7.17/1.58 inference(pre_NNF_transformation,[status(thm)],[f98])).
% 7.17/1.58 fof(f587,plain,(
% 7.17/1.58 aSubsetOf0(xO,xS)),
% 7.17/1.58 inference(cnf_transformation,[status(thm)],[f585])).
% 7.17/1.58 fof(f588,plain,(
% 7.17/1.58 ((![W0]: (((((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xO))))&~aSubsetOf0(W0,xO))|~sbrdtbr0(W0)=xK)&~aElementOf0(W0,slbdtsldtrb0(xO,xK)))|((((((((((?[W1]: aElementOf0(W1,W0))&~W0=slcrc0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,szNzAzT0))))&aSubsetOf0(W0,szNzAzT0))&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&aElementOf0(W0,szDzozmdt0(xc)))&sdtlpdtrp0(xc,W0)=szDzizrdt0(xd))))&(![W0]: (~aElementOf0(W0,xT)|(![W1]: ((((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,xS))))&~aSubsetOf0(W1,xS))|~isCountable0(W1))|(?[W2]: (((((aSet0(W2)&(![W3]: (~aElementOf0(W3,W2)|aElementOf0(W3,W1))))&aSubsetOf0(W2,W1))&sbrdtbr0(W2)=xK)&aElementOf0(W2,slbdtsldtrb0(W1,xK)))&~sdtlpdtrp0(xc,W2)=W0)))))))),
% 7.17/1.58 inference(pre_NNF_transformation,[status(thm)],[f100])).
% 7.17/1.58 fof(f589,definition,(
% 7.17/1.58 ![W0]: (sP10_prd(W0)<=>((((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xO))))&~aSubsetOf0(W0,xO))|~sbrdtbr0(W0)=xK)&~aElementOf0(W0,slbdtsldtrb0(xO,xK))))),
% 7.17/1.58 introduced(definition,[new_symbols(definition,[sP10_prd])],[])).
% 7.17/1.58 fof(f590,definition,(
% 7.17/1.58 ![W1]: (sP11_prd(W1)<=>(((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,xS))))&~aSubsetOf0(W1,xS))|~isCountable0(W1)))),
% 7.17/1.58 introduced(definition,[new_symbols(definition,[sP11_prd])],[])).
% 7.17/1.58 fof(f591,plain,(
% 7.17/1.58 (![W0]: (sP10_prd(W0)|((((((((((?[W1]: aElementOf0(W1,W0))&~W0=slcrc0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,szNzAzT0))))&aSubsetOf0(W0,szNzAzT0))&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&aElementOf0(W0,szDzozmdt0(xc)))&sdtlpdtrp0(xc,W0)=szDzizrdt0(xd))))&(![W0]: (~aElementOf0(W0,xT)|(![W1]: (sP11_prd(W1)|(?[W2]: (((((aSet0(W2)&(![W3]: (~aElementOf0(W3,W2)|aElementOf0(W3,W1))))&aSubsetOf0(W2,W1))&sbrdtbr0(W2)=xK)&aElementOf0(W2,slbdtsldtrb0(W1,xK)))&~sdtlpdtrp0(xc,W2)=W0))))))),
% 7.17/1.58 inference(formula_renaming,[status(thm)],[f588,f590,f589])).
% 7.17/1.58 fof(f592,plain,(
% 7.17/1.58 (![W0]: (sP10_prd(W0)|(((((((((aElementOf0(sK36_skl(W0),W0)&~W0=slcrc0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,szNzAzT0))))&aSubsetOf0(W0,szNzAzT0))&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xS))))&aSubsetOf0(W0,xS))&aElementOf0(W0,szDzozmdt0(xc)))&sdtlpdtrp0(xc,W0)=szDzizrdt0(xd))))&(![W0]: (~aElementOf0(W0,xT)|(![W1]: (sP11_prd(W1)|(((((aSet0(sK37_skl(W1,W0))&(![W3]: (~aElementOf0(W3,sK37_skl(W1,W0))|aElementOf0(W3,W1))))&aSubsetOf0(sK37_skl(W1,W0),W1))&sbrdtbr0(sK37_skl(W1,W0))=xK)&aElementOf0(sK37_skl(W1,W0),slbdtsldtrb0(W1,xK)))&~sdtlpdtrp0(xc,sK37_skl(W1,W0))=W0)))))),
% 7.17/1.58 inference(skolemize,[status(esa),new_symbols(skolem,[sK36_skl,sK37_skl]),skolemize(W1,sK36_skl(W0)),skolemize(W2,sK37_skl(W1,W0))],[f591])).
% 7.17/1.58 fof(f602,plain,(
% 7.17/1.58 ![X0]: (sP10_prd(X0)|sdtlpdtrp0(xc,X0)=szDzizrdt0(xd))),
% 7.17/1.58 inference(cnf_transformation,[status(thm)],[f592])).
% 7.17/1.58 fof(f607,plain,(
% 7.17/1.58 ![X0,X1]: (~aElementOf0(X0,xT)|sP11_prd(X1)|aElementOf0(sK37_skl(X1,X0),slbdtsldtrb0(X1,xK)))),
% 7.17/1.58 inference(cnf_transformation,[status(thm)],[f592])).
% 7.17/1.58 fof(f608,plain,(
% 7.17/1.58 ![X0,X1]: (~aElementOf0(X0,xT)|sP11_prd(X1)|~sdtlpdtrp0(xc,sK37_skl(X1,X0))=X0)),
% 7.17/1.58 inference(cnf_transformation,[status(thm)],[f592])).
% 7.17/1.58 fof(f737,plain,(
% 7.17/1.58 ![W0]: ((~sP10_prd(W0)|((((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xO))))&~aSubsetOf0(W0,xO))|~sbrdtbr0(W0)=xK)&~aElementOf0(W0,slbdtsldtrb0(xO,xK))))&(sP10_prd(W0)|((((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xO))))|aSubsetOf0(W0,xO))&sbrdtbr0(W0)=xK)|aElementOf0(W0,slbdtsldtrb0(xO,xK)))))),
% 7.17/1.58 inference(NNF_transformation,[status(thm)],[f589])).
% 7.17/1.58 fof(f738,plain,(
% 7.17/1.58 (![W0]: (~sP10_prd(W0)|((((~aSet0(W0)|(?[W1]: (aElementOf0(W1,W0)&~aElementOf0(W1,xO))))&~aSubsetOf0(W0,xO))|~sbrdtbr0(W0)=xK)&~aElementOf0(W0,slbdtsldtrb0(xO,xK)))))&(![W0]: (sP10_prd(W0)|((((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xO))))|aSubsetOf0(W0,xO))&sbrdtbr0(W0)=xK)|aElementOf0(W0,slbdtsldtrb0(xO,xK)))))),
% 7.17/1.58 inference(miniscoping,[status(thm)],[f737])).
% 7.17/1.58 fof(f739,plain,(
% 7.17/1.58 (![W0]: (~sP10_prd(W0)|((((~aSet0(W0)|(aElementOf0(sK61_skl(W0),W0)&~aElementOf0(sK61_skl(W0),xO)))&~aSubsetOf0(W0,xO))|~sbrdtbr0(W0)=xK)&~aElementOf0(W0,slbdtsldtrb0(xO,xK)))))&(![W0]: (sP10_prd(W0)|((((aSet0(W0)&(![W1]: (~aElementOf0(W1,W0)|aElementOf0(W1,xO))))|aSubsetOf0(W0,xO))&sbrdtbr0(W0)=xK)|aElementOf0(W0,slbdtsldtrb0(xO,xK)))))),
% 7.17/1.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK61_skl]),skolemize(W1,sK61_skl(W0))],[f738])).
% 7.17/1.59 fof(f743,plain,(
% 7.17/1.59 ![X0]: (~sP10_prd(X0)|~aElementOf0(X0,slbdtsldtrb0(xO,xK)))),
% 7.17/1.59 inference(cnf_transformation,[status(thm)],[f739])).
% 7.17/1.59 fof(f747,plain,(
% 7.17/1.59 ![W1]: ((~sP11_prd(W1)|(((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,xS))))&~aSubsetOf0(W1,xS))|~isCountable0(W1)))&(sP11_prd(W1)|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,xS))))|aSubsetOf0(W1,xS))&isCountable0(W1))))),
% 7.17/1.59 inference(NNF_transformation,[status(thm)],[f590])).
% 7.17/1.59 fof(f748,plain,(
% 7.17/1.59 (![W1]: (~sP11_prd(W1)|(((~aSet0(W1)|(?[W2]: (aElementOf0(W2,W1)&~aElementOf0(W2,xS))))&~aSubsetOf0(W1,xS))|~isCountable0(W1))))&(![W1]: (sP11_prd(W1)|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,xS))))|aSubsetOf0(W1,xS))&isCountable0(W1))))),
% 7.17/1.59 inference(miniscoping,[status(thm)],[f747])).
% 7.17/1.59 fof(f749,plain,(
% 7.17/1.59 (![W1]: (~sP11_prd(W1)|(((~aSet0(W1)|(aElementOf0(sK62_skl(W1),W1)&~aElementOf0(sK62_skl(W1),xS)))&~aSubsetOf0(W1,xS))|~isCountable0(W1))))&(![W1]: (sP11_prd(W1)|(((aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,xS))))|aSubsetOf0(W1,xS))&isCountable0(W1))))),
% 7.17/1.59 inference(skolemize,[status(esa),new_symbols(skolem,[sK62_skl]),skolemize(W2,sK62_skl(W1))],[f748])).
% 7.17/1.59 fof(f752,plain,(
% 7.17/1.59 ![X0]: (~sP11_prd(X0)|~aSubsetOf0(X0,xS)|~isCountable0(X0))),
% 7.17/1.59 inference(cnf_transformation,[status(thm)],[f749])).
% 7.17/1.59 fof(f1451,plain,(
% 7.17/1.59 ~sP11_prd(xO)|~isCountable0(xO)),
% 7.17/1.59 inference(resolution,[status(thm)],[f587,f752])).
% 7.17/1.59 fof(f1454,plain,(
% 7.17/1.59 ~sP11_prd(xO)),
% 7.17/1.59 inference(forward_subsumption_resolution,[status(thm)],[f1451,f576])).
% 7.17/1.59 fof(f2431,plain,(
% 7.17/1.59 ![X0]: (sP11_prd(X0)|aElementOf0(sK37_skl(X0,szDzizrdt0(xd)),slbdtsldtrb0(X0,xK)))),
% 7.17/1.59 inference(resolution,[status(thm)],[f558,f607])).
% 7.17/1.59 fof(f2966,plain,(
% 7.17/1.59 sP11_prd(xO)|~sP10_prd(sK37_skl(xO,szDzizrdt0(xd)))),
% 7.17/1.59 inference(resolution,[status(thm)],[f2431,f743])).
% 7.17/1.59 fof(f2974,plain,(
% 7.17/1.59 ~sP10_prd(sK37_skl(xO,szDzizrdt0(xd)))),
% 7.17/1.59 inference(forward_subsumption_resolution,[status(thm)],[f2966,f1454])).
% 7.17/1.59 fof(f3509,plain,(
% 7.17/1.59 sdtlpdtrp0(xc,sK37_skl(xO,szDzizrdt0(xd)))=szDzizrdt0(xd)),
% 7.17/1.59 inference(resolution,[status(thm)],[f2974,f602])).
% 7.17/1.59 fof(f7349,plain,(
% 7.17/1.59 ~aElementOf0(szDzizrdt0(xd),xT)|sP11_prd(xO)),
% 7.17/1.59 inference(resolution,[status(thm)],[f3509,f608])).
% 7.17/1.59 fof(f7351,plain,(
% 7.17/1.59 sP11_prd(xO)),
% 7.17/1.59 inference(forward_subsumption_resolution,[status(thm)],[f7349,f558])).
% 7.17/1.59 fof(f7354,plain,(
% 7.17/1.59 $false),
% 7.17/1.59 inference(forward_subsumption_resolution,[status(thm)],[f7351,f1454])).
% 7.17/1.59 % SZS output end CNFRefutation for theBenchmark.p
% 0.37/1.60 % Elapsed time: 1.041622 seconds
% 0.37/1.60 % CPU time: 7.961281 seconds
% 0.37/1.60 % Total memory used: 210.761 MB
% 0.37/1.60 % Net memory used: 202.581 MB
%------------------------------------------------------------------------------