%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM603+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 : 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:19 PM UTC 2026
% Result : Theorem 5.02s 1.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM603+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/0.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 02:44:53 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.40 % Drodi V4.1.1
% 5.02/1.09 % Refutation found
% 5.02/1.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.02/1.09 % SZS output start CNFRefutation for theBenchmark
% 5.02/1.09 fof(f24,axiom,(
% 5.02/1.09 aElementOf0(sz00,szNzAzT0) ),
% 5.02/1.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.02/1.09 fof(f30,axiom,(
% 5.02/1.09 (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlseqdt0(sz00,W0) ) )),
% 5.02/1.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.02/1.09 fof(f81,hypothesis,(
% 5.02/1.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))) ) ) ) )) ),
% 5.02/1.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.02/1.09 fof(f83,hypothesis,(
% 5.02/1.09 (! [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)) ) ) ) )),
% 5.02/1.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.02/1.09 fof(f99,hypothesis,(
% 5.02/1.09 ( aElementOf0(xi,szNzAzT0)& sdtlpdtrp0(xe,xi) = xx ) ),
% 5.02/1.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.02/1.09 fof(f100,conjecture,(
% 5.02/1.09 ( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> aElementOf0(W0,xS) ))| aSubsetOf0(sdtlpdtrp0(xN,xi),xS) ) ),
% 5.02/1.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 5.02/1.09 fof(f101,negated_conjecture,(
% 5.02/1.09 ~(( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> aElementOf0(W0,xS) ))| aSubsetOf0(sdtlpdtrp0(xN,xi),xS) ) )),
% 5.02/1.09 inference(negated_conjecture,[status(cth)],[f100])).
% 5.02/1.09 fof(f180,plain,(
% 5.02/1.09 aElementOf0(sz00,szNzAzT0)),
% 5.02/1.09 inference(cnf_transformation,[status(thm)],[f24])).
% 5.02/1.09 fof(f194,plain,(
% 5.02/1.09 ![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlseqdt0(sz00,W0))),
% 5.02/1.09 inference(pre_NNF_transformation,[status(thm)],[f30])).
% 5.02/1.09 fof(f195,plain,(
% 5.02/1.09 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlseqdt0(sz00,X0))),
% 5.02/1.09 inference(cnf_transformation,[status(thm)],[f194])).
% 5.02/1.09 fof(f398,plain,(
% 5.02/1.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)))))))),
% 5.02/1.09 inference(pre_NNF_transformation,[status(thm)],[f81])).
% 5.02/1.09 fof(f399,definition,(
% 5.02/1.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))))),
% 5.02/1.09 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 5.02/1.09 fof(f400,plain,(
% 5.02/1.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)))))))),
% 5.02/1.09 inference(formula_renaming,[status(thm)],[f398,f399])).
% 5.02/1.09 fof(f401,plain,(
% 5.02/1.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)))))))),
% 5.02/1.09 inference(NNF_transformation,[status(thm)],[f400])).
% 5.02/1.09 fof(f402,plain,(
% 5.02/1.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)))))))),
% 5.02/1.09 inference(miniscoping,[status(thm)],[f401])).
% 5.02/1.09 fof(f405,plain,(
% 5.02/1.09 sdtlpdtrp0(xN,sz00)=xS),
% 5.02/1.09 inference(cnf_transformation,[status(thm)],[f402])).
% 5.02/1.09 fof(f422,plain,(
% 5.02/1.09 ![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)))))),
% 5.02/1.09 inference(pre_NNF_transformation,[status(thm)],[f83])).
% 5.02/1.09 fof(f423,plain,(
% 5.02/1.09 ![X0,X1,X2]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X1,X0)|~aElementOf0(X2,sdtlpdtrp0(xN,X0))|aElementOf0(X2,sdtlpdtrp0(xN,X1)))),
% 5.02/1.09 inference(cnf_transformation,[status(thm)],[f422])).
% 5.02/1.09 fof(f590,plain,(
% 5.02/1.09 aElementOf0(xi,szNzAzT0)),
% 5.02/1.09 inference(cnf_transformation,[status(thm)],[f99])).
% 5.02/1.09 fof(f592,plain,(
% 5.02/1.09 ((?[W0]: (aElementOf0(W0,sdtlpdtrp0(xN,xi))&~aElementOf0(W0,xS)))&~aSubsetOf0(sdtlpdtrp0(xN,xi),xS))),
% 5.02/1.09 inference(pre_NNF_transformation,[status(thm)],[f101])).
% 5.02/1.09 fof(f593,plain,(
% 5.02/1.09 (aElementOf0(sK37_skl,sdtlpdtrp0(xN,xi))&~aElementOf0(sK37_skl,xS))&~aSubsetOf0(sdtlpdtrp0(xN,xi),xS)),
% 5.02/1.11 inference(skolemize,[status(esa),new_symbols(skolem,[sK37_skl]),skolemize(W0,sK37_skl)],[f592])).
% 5.02/1.11 fof(f594,plain,(
% 5.02/1.11 aElementOf0(sK37_skl,sdtlpdtrp0(xN,xi))),
% 5.02/1.11 inference(cnf_transformation,[status(thm)],[f593])).
% 5.02/1.11 fof(f595,plain,(
% 5.02/1.11 ~aElementOf0(sK37_skl,xS)),
% 5.02/1.11 inference(cnf_transformation,[status(thm)],[f593])).
% 5.02/1.11 fof(f3894,plain,(
% 5.02/1.11 ![X0]: (~aElementOf0(xi,szNzAzT0)|~aElementOf0(X0,szNzAzT0)|~sdtlseqdt0(X0,xi)|aElementOf0(sK37_skl,sdtlpdtrp0(xN,X0)))),
% 5.02/1.11 inference(resolution,[status(thm)],[f423,f594])).
% 5.02/1.11 fof(f3899,plain,(
% 5.02/1.11 ![X0]: (~aElementOf0(X0,szNzAzT0)|~sdtlseqdt0(X0,xi)|aElementOf0(sK37_skl,sdtlpdtrp0(xN,X0)))),
% 5.02/1.11 inference(forward_subsumption_resolution,[status(thm)],[f3894,f590])).
% 5.02/1.11 fof(f3970,plain,(
% 5.02/1.11 ~aElementOf0(sz00,szNzAzT0)|aElementOf0(sK37_skl,sdtlpdtrp0(xN,sz00))|~aElementOf0(xi,szNzAzT0)),
% 5.02/1.11 inference(resolution,[status(thm)],[f3899,f195])).
% 5.02/1.11 fof(f3975,plain,(
% 5.02/1.11 ~aElementOf0(sz00,szNzAzT0)|aElementOf0(sK37_skl,xS)|~aElementOf0(xi,szNzAzT0)),
% 5.02/1.11 inference(forward_demodulation,[status(thm)],[f405,f3970])).
% 5.02/1.11 fof(f3976,plain,(
% 5.02/1.11 aElementOf0(sK37_skl,xS)|~aElementOf0(xi,szNzAzT0)),
% 5.02/1.11 inference(forward_subsumption_resolution,[status(thm)],[f3975,f180])).
% 5.02/1.11 fof(f4171,plain,(
% 5.02/1.11 ~aElementOf0(xi,szNzAzT0)),
% 5.02/1.11 inference(forward_subsumption_resolution,[status(thm)],[f3976,f595])).
% 5.02/1.11 fof(f4172,plain,(
% 5.02/1.11 $false),
% 5.02/1.11 inference(backward_subsumption_resolution,[status(thm)],[f590,f4171])).
% 5.02/1.11 % SZS output end CNFRefutation for theBenchmark.p
% 1.28/1.14 % Elapsed time: 0.760784 seconds
% 1.28/1.14 % CPU time: 5.420187 seconds
% 1.28/1.14 % Total memory used: 171.765 MB
% 1.28/1.14 % Net memory used: 167.791 MB
%------------------------------------------------------------------------------