%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM604+1 : 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:19 PM UTC 2026
% Result : Theorem 65.00s 8.69s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM604+1 : 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.08/0.36 % Computer : n008.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.02/0.36 % CPULimit : 300
% 0.02/0.36 % WCLimit : 300
% 0.02/0.36 % DateTime : Mon Sep 21 02:44:53 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.38 % Drodi V4.1.1
% 65.00/8.69 % Refutation found
% 65.00/8.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 65.00/8.69 % SZS output start CNFRefutation for theBenchmark
% 65.00/8.69 fof(f5,definition,(
% 65.00/8.69 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 65.00/8.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.00/8.69 fof(f9,axiom,(
% 65.00/8.69 (! [W0] :( ( aSet0(W0)& isCountable0(W0) )=> W0 != slcrc0 ) )),
% 65.00/8.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.00/8.69 fof(f10,definition,(
% 65.00/8.69 (! [W0] :( aSet0(W0)=> (! [W1] :( aSubsetOf0(W1,W0)<=> ( aSet0(W1)& (! [W2] :( aElementOf0(W2,W1)=> aElementOf0(W2,W0) ) )) ) )) )),
% 65.00/8.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.00/8.69 fof(f23,axiom,(
% 65.00/8.69 ( aSet0(szNzAzT0)& isCountable0(szNzAzT0) ) ),
% 65.00/8.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.00/8.69 fof(f47,definition,(
% 65.00/8.69 (! [W0] :( ( aSubsetOf0(W0,szNzAzT0)& W0 != slcrc0 )=> (! [W1] :( W1 = szmzizndt0(W0)<=> ( aElementOf0(W1,W0)& (! [W2] :( aElementOf0(W2,W0)=> sdtlseqdt0(W1,W2) ) )) ) )) )),
% 65.00/8.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.00/8.69 fof(f75,hypothesis,(
% 65.00/8.69 ( aSubsetOf0(xS,szNzAzT0)& isCountable0(xS) ) ),
% 65.00/8.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.00/8.69 fof(f82,hypothesis,(
% 65.00/8.69 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)& isCountable0(sdtlpdtrp0(xN,W0)) ) ) )),
% 65.00/8.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.00/8.69 fof(f91,hypothesis,(
% 65.00/8.69 ( aFunction0(xe)& szDzozmdt0(xe) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0)) ) )) ),
% 65.00/8.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.00/8.69 fof(f99,hypothesis,(
% 65.00/8.69 ( aElementOf0(xi,szNzAzT0)& sdtlpdtrp0(xe,xi) = xx ) ),
% 65.00/8.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.00/8.69 fof(f100,hypothesis,(
% 65.00/8.69 aSubsetOf0(sdtlpdtrp0(xN,xi),xS) ),
% 65.00/8.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.00/8.69 fof(f101,conjecture,(
% 65.00/8.69 aElementOf0(xx,xS) ),
% 65.00/8.69 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 65.00/8.69 fof(f102,negated_conjecture,(
% 65.00/8.69 ~(aElementOf0(xx,xS) )),
% 65.00/8.69 inference(negated_conjecture,[status(cth)],[f101])).
% 65.00/8.69 fof(f113,plain,(
% 65.00/8.69 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 65.00/8.69 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 65.00/8.69 fof(f114,plain,(
% 65.00/8.69 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 65.00/8.69 inference(NNF_transformation,[status(thm)],[f113])).
% 65.00/8.69 fof(f115,plain,(
% 65.00/8.69 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 65.00/8.69 inference(miniscoping,[status(thm)],[f114])).
% 65.00/8.69 fof(f116,plain,(
% 65.00/8.69 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 65.00/8.69 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f115])).
% 65.00/8.69 fof(f117,plain,(
% 65.00/8.69 ![X0]: (~X0=slcrc0|aSet0(X0))),
% 65.00/8.69 inference(cnf_transformation,[status(thm)],[f116])).
% 65.00/8.69 fof(f125,plain,(
% 65.00/8.69 ![W0]: ((~aSet0(W0)|~isCountable0(W0))|~W0=slcrc0)),
% 65.00/8.69 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 65.00/8.69 fof(f126,plain,(
% 65.00/8.69 ![X0]: (~aSet0(X0)|~isCountable0(X0)|~X0=slcrc0)),
% 65.00/8.69 inference(cnf_transformation,[status(thm)],[f125])).
% 65.00/8.69 fof(f127,plain,(
% 65.00/8.69 ![W0]: (~aSet0(W0)|(![W1]: (aSubsetOf0(W1,W0)<=>(aSet0(W1)&(![W2]: (~aElementOf0(W2,W1)|aElementOf0(W2,W0)))))))),
% 65.00/8.69 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 65.00/8.69 fof(f128,plain,(
% 65.00/8.69 ![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))))))))),
% 65.00/8.69 inference(NNF_transformation,[status(thm)],[f127])).
% 65.00/8.69 fof(f129,plain,(
% 65.00/8.69 ![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))))))))),
% 65.00/8.69 inference(miniscoping,[status(thm)],[f128])).
% 65.00/8.69 fof(f130,plain,(
% 65.00/8.69 ![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)))))))),
% 65.00/8.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(W2,sK1_skl(W1,W0))],[f129])).
% 65.00/8.70 fof(f131,plain,(
% 65.00/8.70 ![X0,X1]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|aSet0(X1))),
% 65.00/8.70 inference(cnf_transformation,[status(thm)],[f130])).
% 65.00/8.70 fof(f132,plain,(
% 65.00/8.70 ![X0,X1,X2]: (~aSet0(X0)|~aSubsetOf0(X1,X0)|~aElementOf0(X2,X1)|aElementOf0(X2,X0))),
% 65.00/8.70 inference(cnf_transformation,[status(thm)],[f130])).
% 65.00/8.70 fof(f179,plain,(
% 65.00/8.70 aSet0(szNzAzT0)),
% 65.00/8.70 inference(cnf_transformation,[status(thm)],[f23])).
% 65.00/8.70 fof(f237,plain,(
% 65.00/8.70 ![W0]: ((~aSubsetOf0(W0,szNzAzT0)|W0=slcrc0)|(![W1]: (W1=szmzizndt0(W0)<=>(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2)))))))),
% 65.00/8.70 inference(pre_NNF_transformation,[status(thm)],[f47])).
% 65.00/8.70 fof(f238,plain,(
% 65.00/8.70 ![W0]: ((~aSubsetOf0(W0,szNzAzT0)|W0=slcrc0)|(![W1]: ((~W1=szmzizndt0(W0)|(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2)))))&(W1=szmzizndt0(W0)|(~aElementOf0(W1,W0)|(?[W2]: (aElementOf0(W2,W0)&~sdtlseqdt0(W1,W2))))))))),
% 65.00/8.70 inference(NNF_transformation,[status(thm)],[f237])).
% 65.00/8.70 fof(f239,plain,(
% 65.00/8.70 ![W0]: ((~aSubsetOf0(W0,szNzAzT0)|W0=slcrc0)|((![W1]: (~W1=szmzizndt0(W0)|(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2))))))&(![W1]: (W1=szmzizndt0(W0)|(~aElementOf0(W1,W0)|(?[W2]: (aElementOf0(W2,W0)&~sdtlseqdt0(W1,W2))))))))),
% 65.00/8.70 inference(miniscoping,[status(thm)],[f238])).
% 65.00/8.70 fof(f240,plain,(
% 65.00/8.70 ![W0]: ((~aSubsetOf0(W0,szNzAzT0)|W0=slcrc0)|((![W1]: (~W1=szmzizndt0(W0)|(aElementOf0(W1,W0)&(![W2]: (~aElementOf0(W2,W0)|sdtlseqdt0(W1,W2))))))&(![W1]: (W1=szmzizndt0(W0)|(~aElementOf0(W1,W0)|(aElementOf0(sK6_skl(W1,W0),W0)&~sdtlseqdt0(W1,sK6_skl(W1,W0))))))))),
% 65.00/8.70 inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(W2,sK6_skl(W1,W0))],[f239])).
% 65.00/8.70 fof(f241,plain,(
% 65.00/8.70 ![X0,X1]: (~aSubsetOf0(X0,szNzAzT0)|X0=slcrc0|~X1=szmzizndt0(X0)|aElementOf0(X1,X0))),
% 65.00/8.70 inference(cnf_transformation,[status(thm)],[f240])).
% 65.00/8.70 fof(f362,plain,(
% 65.00/8.70 aSubsetOf0(xS,szNzAzT0)),
% 65.00/8.70 inference(cnf_transformation,[status(thm)],[f75])).
% 65.00/8.70 fof(f383,plain,(
% 65.00/8.70 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)&isCountable0(sdtlpdtrp0(xN,W0))))),
% 65.00/8.70 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 65.00/8.70 fof(f384,plain,(
% 65.00/8.70 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0))),
% 65.00/8.70 inference(cnf_transformation,[status(thm)],[f383])).
% 65.00/8.70 fof(f385,plain,(
% 65.00/8.70 ![X0]: (~aElementOf0(X0,szNzAzT0)|isCountable0(sdtlpdtrp0(xN,X0)))),
% 65.00/8.70 inference(cnf_transformation,[status(thm)],[f383])).
% 65.00/8.70 fof(f412,plain,(
% 65.00/8.70 (aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|sdtlpdtrp0(xe,W0)=szmzizndt0(sdtlpdtrp0(xN,W0))))),
% 65.00/8.70 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 65.00/8.70 fof(f415,plain,(
% 65.00/8.70 ![X0]: (~aElementOf0(X0,szNzAzT0)|sdtlpdtrp0(xe,X0)=szmzizndt0(sdtlpdtrp0(xN,X0)))),
% 65.00/8.70 inference(cnf_transformation,[status(thm)],[f412])).
% 65.00/8.70 fof(f433,plain,(
% 65.00/8.70 aElementOf0(xi,szNzAzT0)),
% 65.00/8.70 inference(cnf_transformation,[status(thm)],[f99])).
% 65.00/8.70 fof(f434,plain,(
% 65.00/8.70 sdtlpdtrp0(xe,xi)=xx),
% 65.00/8.70 inference(cnf_transformation,[status(thm)],[f99])).
% 65.00/8.70 fof(f435,plain,(
% 65.00/8.70 aSubsetOf0(sdtlpdtrp0(xN,xi),xS)),
% 65.00/8.70 inference(cnf_transformation,[status(thm)],[f100])).
% 65.00/8.70 fof(f436,plain,(
% 65.00/8.70 ~aElementOf0(xx,xS)),
% 65.00/8.70 inference(cnf_transformation,[status(thm)],[f102])).
% 65.00/8.70 fof(f443,plain,(
% 65.00/8.70 aSet0(slcrc0)),
% 65.00/8.70 inference(destructive_equality_resolution,[status(thm)],[f117])).
% 65.00/8.70 fof(f445,plain,(
% 65.00/8.70 ~aSet0(slcrc0)|~isCountable0(slcrc0)),
% 65.00/8.70 inference(destructive_equality_resolution,[status(thm)],[f126])).
% 65.00/8.70 fof(f456,plain,(
% 65.00/8.70 ![X0]: (~aSubsetOf0(X0,szNzAzT0)|X0=slcrc0|aElementOf0(szmzizndt0(X0),X0))),
% 65.00/8.70 inference(destructive_equality_resolution,[status(thm)],[f241])).
% 65.00/8.70 fof(f491,plain,(
% 65.00/8.70 ~isCountable0(slcrc0)),
% 65.00/8.70 inference(forward_subsumption_resolution,[status(thm)],[f445,f443])).
% 65.00/8.70 fof(f492,plain,(
% 65.00/8.70 ~aSet0(szNzAzT0)|aSet0(xS)),
% 65.00/8.70 inference(resolution,[status(thm)],[f131,f362])).
% 65.00/8.70 fof(f493,plain,(
% 65.00/8.70 aSet0(xS)),
% 65.00/8.70 inference(forward_subsumption_resolution,[status(thm)],[f492,f179])).
% 65.00/8.70 fof(f3047,plain,(
% 65.00/8.70 ![X0]: (~aSet0(xS)|~aElementOf0(X0,sdtlpdtrp0(xN,xi))|aElementOf0(X0,xS))),
% 61.75/8.75 inference(resolution,[status(thm)],[f435,f132])).
% 61.75/8.75 fof(f3052,plain,(
% 61.75/8.75 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xi))|aElementOf0(X0,xS))),
% 61.75/8.75 inference(forward_subsumption_resolution,[status(thm)],[f3047,f493])).
% 61.75/8.75 fof(f3238,plain,(
% 61.75/8.75 aSubsetOf0(sdtlpdtrp0(xN,xi),szNzAzT0)),
% 61.75/8.75 inference(resolution,[status(thm)],[f384,f433])).
% 61.75/8.75 fof(f3554,plain,(
% 61.75/8.75 sdtlpdtrp0(xe,xi)=szmzizndt0(sdtlpdtrp0(xN,xi))),
% 61.75/8.75 inference(resolution,[status(thm)],[f415,f433])).
% 61.75/8.75 fof(f3563,plain,(
% 61.75/8.75 xx=szmzizndt0(sdtlpdtrp0(xN,xi))),
% 61.75/8.75 inference(forward_demodulation,[status(thm)],[f434,f3554])).
% 61.75/8.75 fof(f11113,plain,(
% 61.75/8.75 sdtlpdtrp0(xN,xi)=slcrc0|aElementOf0(szmzizndt0(sdtlpdtrp0(xN,xi)),sdtlpdtrp0(xN,xi))),
% 61.75/8.75 inference(resolution,[status(thm)],[f3238,f456])).
% 61.75/8.75 fof(f11124,plain,(
% 61.75/8.75 sdtlpdtrp0(xN,xi)=slcrc0|aElementOf0(xx,sdtlpdtrp0(xN,xi))),
% 61.75/8.75 inference(forward_demodulation,[status(thm)],[f3563,f11113])).
% 61.75/8.75 fof(f27055,plain,(
% 61.75/8.75 sdtlpdtrp0(xN,xi)=slcrc0|aElementOf0(xx,xS)),
% 61.75/8.75 inference(resolution,[status(thm)],[f11124,f3052])).
% 61.75/8.75 fof(f27059,plain,(
% 61.75/8.75 sdtlpdtrp0(xN,xi)=slcrc0),
% 61.75/8.75 inference(forward_subsumption_resolution,[status(thm)],[f27055,f436])).
% 61.75/8.75 fof(f27160,plain,(
% 61.75/8.75 ~aElementOf0(xi,szNzAzT0)|isCountable0(slcrc0)),
% 61.75/8.75 inference(paramodulation,[status(thm)],[f27059,f385])).
% 61.75/8.75 fof(f27399,plain,(
% 61.75/8.75 isCountable0(slcrc0)),
% 61.75/8.75 inference(forward_subsumption_resolution,[status(thm)],[f27160,f433])).
% 61.75/8.75 fof(f27459,plain,(
% 61.75/8.75 $false),
% 61.75/8.75 inference(forward_subsumption_resolution,[status(thm)],[f27399,f491])).
% 61.75/8.75 % SZS output end CNFRefutation for theBenchmark.p
% 61.75/8.78 % Elapsed time: 8.405873 seconds
% 61.75/8.78 % CPU time: 66.272562 seconds
% 61.75/8.78 % Total memory used: 561.596 MB
% 61.75/8.78 % Net memory used: 527.162 MB
%------------------------------------------------------------------------------