%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM623+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 : n002.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:22 PM UTC 2026
% Result : Theorem 9.44s 1.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM623+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.35 % Computer : n002.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 02:48:02 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 9.44/1.63 % Refutation found
% 9.44/1.63 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.44/1.63 % SZS output start CNFRefutation for theBenchmark
% 9.44/1.63 fof(f5,definition,(
% 9.44/1.63 (! [W0] :( W0 = slcrc0<=> ( aSet0(W0)& ~ (? [W1] : aElementOf0(W1,W0) )) ) )),
% 9.44/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.44/1.63 fof(f49,axiom,(
% 9.44/1.63 (! [W0,W1] :( ( aSubsetOf0(W0,szNzAzT0)& aSubsetOf0(W1,szNzAzT0)& W0 != slcrc0& W1 != slcrc0 )=> ( ( aElementOf0(szmzizndt0(W0),W1)& aElementOf0(szmzizndt0(W1),W0) )=> szmzizndt0(W0) = szmzizndt0(W1) ) ) )),
% 9.44/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.44/1.63 fof(f82,hypothesis,(
% 9.44/1.63 (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)& isCountable0(sdtlpdtrp0(xN,W0)) ) ) )),
% 9.44/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.44/1.63 fof(f100,hypothesis,(
% 9.44/1.63 ( aSubsetOf0(xQ,xO)& xQ != slcrc0 ) ),
% 9.44/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.44/1.63 fof(f101,hypothesis,(
% 9.44/1.63 aSubsetOf0(xQ,szNzAzT0) ),
% 9.44/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.44/1.63 fof(f103,hypothesis,(
% 9.44/1.63 xp = szmzizndt0(xQ) ),
% 9.44/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.44/1.63 fof(f115,hypothesis,(
% 9.44/1.63 ( aElementOf0(xm,szNzAzT0)& xx = sdtlpdtrp0(xe,xm) ) ),
% 9.44/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.44/1.63 fof(f116,hypothesis,(
% 9.44/1.63 xx = szmzizndt0(sdtlpdtrp0(xN,xm)) ),
% 9.44/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.44/1.63 fof(f119,hypothesis,(
% 9.44/1.63 ( aElementOf0(xp,sdtlpdtrp0(xN,xm))& aElementOf0(xx,xQ) ) ),
% 9.44/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.44/1.63 fof(f120,conjecture,(
% 9.44/1.63 xp = xx ),
% 9.44/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.44/1.63 fof(f121,negated_conjecture,(
% 9.44/1.63 ~(xp = xx )),
% 9.44/1.63 inference(negated_conjecture,[status(cth)],[f120])).
% 9.44/1.63 fof(f132,plain,(
% 9.44/1.63 ![W0]: (W0=slcrc0<=>(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))),
% 9.44/1.63 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 9.44/1.63 fof(f133,plain,(
% 9.44/1.63 ![W0]: ((~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0))))&(W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 9.44/1.63 inference(NNF_transformation,[status(thm)],[f132])).
% 9.44/1.63 fof(f134,plain,(
% 9.44/1.63 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|(?[W1]: aElementOf0(W1,W0)))))),
% 9.44/1.63 inference(miniscoping,[status(thm)],[f133])).
% 9.44/1.63 fof(f135,plain,(
% 9.44/1.63 (![W0]: (~W0=slcrc0|(aSet0(W0)&(![W1]: ~aElementOf0(W1,W0)))))&(![W0]: (W0=slcrc0|(~aSet0(W0)|aElementOf0(sK0_skl(W0),W0))))),
% 9.44/1.63 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(W1,sK0_skl(W0))],[f134])).
% 9.44/1.63 fof(f137,plain,(
% 9.44/1.63 ![X0,X1]: (~X0=slcrc0|~aElementOf0(X1,X0))),
% 9.44/1.63 inference(cnf_transformation,[status(thm)],[f135])).
% 9.44/1.63 fof(f272,plain,(
% 9.44/1.63 ![W0,W1]: ((((~aSubsetOf0(W0,szNzAzT0)|~aSubsetOf0(W1,szNzAzT0))|W0=slcrc0)|W1=slcrc0)|((~aElementOf0(szmzizndt0(W0),W1)|~aElementOf0(szmzizndt0(W1),W0))|szmzizndt0(W0)=szmzizndt0(W1)))),
% 9.44/1.63 inference(pre_NNF_transformation,[status(thm)],[f49])).
% 9.44/1.63 fof(f273,plain,(
% 9.44/1.63 ![X0,X1]: (~aSubsetOf0(X0,szNzAzT0)|~aSubsetOf0(X1,szNzAzT0)|X0=slcrc0|X1=slcrc0|~aElementOf0(szmzizndt0(X0),X1)|~aElementOf0(szmzizndt0(X1),X0)|szmzizndt0(X0)=szmzizndt0(X1))),
% 9.44/1.63 inference(cnf_transformation,[status(thm)],[f272])).
% 9.44/1.63 fof(f402,plain,(
% 9.44/1.63 ![W0]: (~aElementOf0(W0,szNzAzT0)|(aSubsetOf0(sdtlpdtrp0(xN,W0),szNzAzT0)&isCountable0(sdtlpdtrp0(xN,W0))))),
% 9.44/1.63 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 9.44/1.63 fof(f403,plain,(
% 9.44/1.63 ![X0]: (~aElementOf0(X0,szNzAzT0)|aSubsetOf0(sdtlpdtrp0(xN,X0),szNzAzT0))),
% 9.44/1.63 inference(cnf_transformation,[status(thm)],[f402])).
% 9.44/1.63 fof(f454,plain,(
% 9.44/1.63 ~xQ=slcrc0),
% 9.44/1.63 inference(cnf_transformation,[status(thm)],[f100])).
% 9.44/1.63 fof(f455,plain,(
% 9.44/1.63 aSubsetOf0(xQ,szNzAzT0)),
% 9.44/1.63 inference(cnf_transformation,[status(thm)],[f101])).
% 9.44/1.63 fof(f457,plain,(
% 9.44/1.63 xp=szmzizndt0(xQ)),
% 9.44/1.63 inference(cnf_transformation,[status(thm)],[f103])).
% 9.44/1.63 fof(f473,plain,(
% 9.44/1.63 aElementOf0(xm,szNzAzT0)),
% 9.44/1.63 inference(cnf_transformation,[status(thm)],[f115])).
% 9.44/1.63 fof(f475,plain,(
% 9.44/1.63 xx=szmzizndt0(sdtlpdtrp0(xN,xm))),
% 9.44/1.63 inference(cnf_transformation,[status(thm)],[f116])).
% 9.44/1.63 fof(f478,plain,(
% 9.44/1.63 aElementOf0(xp,sdtlpdtrp0(xN,xm))),
% 9.44/1.63 inference(cnf_transformation,[status(thm)],[f119])).
% 9.44/1.63 fof(f479,plain,(
% 9.44/1.64 aElementOf0(xx,xQ)),
% 9.44/1.64 inference(cnf_transformation,[status(thm)],[f119])).
% 9.44/1.64 fof(f480,plain,(
% 9.44/1.64 ~xp=xx),
% 9.44/1.64 inference(cnf_transformation,[status(thm)],[f121])).
% 9.44/1.64 fof(f488,plain,(
% 9.44/1.64 ![X0]: (~aElementOf0(X0,slcrc0))),
% 9.44/1.64 inference(destructive_equality_resolution,[status(thm)],[f137])).
% 9.44/1.64 fof(f977,plain,(
% 9.44/1.64 ![X0]: (~aSubsetOf0(X0,szNzAzT0)|X0=slcrc0|xQ=slcrc0|~aElementOf0(szmzizndt0(X0),xQ)|~aElementOf0(szmzizndt0(xQ),X0)|szmzizndt0(X0)=szmzizndt0(xQ))),
% 9.44/1.64 inference(resolution,[status(thm)],[f455,f273])).
% 9.44/1.64 fof(f991,plain,(
% 9.44/1.64 ![X0]: (~aSubsetOf0(X0,szNzAzT0)|X0=slcrc0|xQ=slcrc0|~aElementOf0(szmzizndt0(X0),xQ)|~aElementOf0(xp,X0)|szmzizndt0(X0)=szmzizndt0(xQ))),
% 9.44/1.64 inference(forward_demodulation,[status(thm)],[f457,f977])).
% 9.44/1.64 fof(f992,plain,(
% 9.44/1.64 ![X0]: (~aSubsetOf0(X0,szNzAzT0)|X0=slcrc0|xQ=slcrc0|~aElementOf0(szmzizndt0(X0),xQ)|~aElementOf0(xp,X0)|szmzizndt0(X0)=xp)),
% 9.44/1.64 inference(forward_demodulation,[status(thm)],[f457,f991])).
% 9.44/1.64 fof(f993,plain,(
% 9.44/1.64 ![X0]: (~aSubsetOf0(X0,szNzAzT0)|X0=slcrc0|~aElementOf0(szmzizndt0(X0),xQ)|~aElementOf0(xp,X0)|szmzizndt0(X0)=xp)),
% 9.44/1.64 inference(forward_subsumption_resolution,[status(thm)],[f992,f454])).
% 9.44/1.64 fof(f2068,plain,(
% 9.44/1.64 aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0)),
% 9.44/1.64 inference(resolution,[status(thm)],[f403,f473])).
% 9.44/1.64 fof(f2831,plain,(
% 9.44/1.64 ~aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0)|sdtlpdtrp0(xN,xm)=slcrc0|~aElementOf0(xx,xQ)|~aElementOf0(xp,sdtlpdtrp0(xN,xm))|szmzizndt0(sdtlpdtrp0(xN,xm))=xp),
% 9.44/1.64 inference(paramodulation,[status(thm)],[f475,f993])).
% 9.44/1.64 fof(f2841,plain,(
% 9.44/1.64 ~aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0)|sdtlpdtrp0(xN,xm)=slcrc0|~aElementOf0(xx,xQ)|~aElementOf0(xp,sdtlpdtrp0(xN,xm))|xx=xp),
% 9.44/1.64 inference(forward_demodulation,[status(thm)],[f475,f2831])).
% 9.44/1.64 fof(f2842,plain,(
% 9.44/1.64 ~aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0)|sdtlpdtrp0(xN,xm)=slcrc0|~aElementOf0(xp,sdtlpdtrp0(xN,xm))|xx=xp),
% 9.44/1.64 inference(forward_subsumption_resolution,[status(thm)],[f2841,f479])).
% 9.44/1.64 fof(f4441,plain,(
% 9.44/1.64 ~aSubsetOf0(sdtlpdtrp0(xN,xm),szNzAzT0)|sdtlpdtrp0(xN,xm)=slcrc0|xx=xp),
% 9.44/1.64 inference(forward_subsumption_resolution,[status(thm)],[f2842,f478])).
% 9.44/1.64 fof(f7818,plain,(
% 9.44/1.64 sdtlpdtrp0(xN,xm)=slcrc0|xx=xp),
% 9.44/1.64 inference(backward_subsumption_resolution,[status(thm)],[f4441,f2068])).
% 9.44/1.64 fof(f7838,plain,(
% 9.44/1.64 sdtlpdtrp0(xN,xm)=slcrc0),
% 9.44/1.64 inference(forward_subsumption_resolution,[status(thm)],[f7818,f480])).
% 9.44/1.64 fof(f7955,plain,(
% 9.44/1.64 aElementOf0(xp,slcrc0)),
% 9.44/1.64 inference(backward_demodulation,[status(thm)],[f7838,f478])).
% 9.44/1.64 fof(f7971,plain,(
% 9.44/1.64 $false),
% 9.44/1.64 inference(forward_subsumption_resolution,[status(thm)],[f7955,f488])).
% 9.44/1.64 % SZS output end CNFRefutation for theBenchmark.p
% 9.44/1.67 % Elapsed time: 1.295971 seconds
% 9.44/1.67 % CPU time: 9.837427 seconds
% 9.44/1.67 % Total memory used: 218.476 MB
% 9.44/1.67 % Net memory used: 210.729 MB
%------------------------------------------------------------------------------