%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM623+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 : 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:23 PM UTC 2026
% Result : Theorem 1.08s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM623+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.35 % Computer : n008.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:46:09 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.12/0.39 % Drodi V4.1.1
% 1.08/0.67 % Refutation found
% 1.08/0.67 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.08/0.67 % SZS output start CNFRefutation for theBenchmark
% 1.08/0.67 fof(f35,axiom,(
% 1.08/0.67 (! [W0,W1] :( ( aElementOf0(W0,szNzAzT0)& aElementOf0(W1,szNzAzT0) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W1,W0) )=> W0 = W1 ) ) )),
% 1.08/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.08/0.67 fof(f82,hypothesis,(
% 1.08/0.67 (! [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)) ) ) )),
% 1.08/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.08/0.67 fof(f103,hypothesis,(
% 1.08/0.67 ( aElementOf0(xp,xQ)& (! [W0] :( aElementOf0(W0,xQ)=> sdtlseqdt0(xp,W0) ))& xp = szmzizndt0(xQ) ) ),
% 1.08/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.08/0.67 fof(f113,hypothesis,(
% 1.08/0.67 ( aElement0(xx)& aElementOf0(xx,xQ)& xx != szmzizndt0(xQ)& aElementOf0(xx,xP) ) ),
% 1.08/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.08/0.67 fof(f114,hypothesis,(
% 1.08/0.67 ( aElementOf0(xx,szNzAzT0)& (? [W0] :( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))& sdtlpdtrp0(xe,W0) = xx ) )) ),
% 1.08/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.08/0.67 fof(f115,hypothesis,(
% 1.08/0.67 ( aElementOf0(xm,szNzAzT0)& xx = sdtlpdtrp0(xe,xm) ) ),
% 1.08/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.08/0.67 fof(f116,hypothesis,(
% 1.08/0.67 (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xm))=> sdtlseqdt0(xx,W0) ) )),
% 1.08/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.08/0.67 fof(f119,hypothesis,(
% 1.08/0.67 ( aElementOf0(xp,sdtlpdtrp0(xN,xm))& aElementOf0(xx,xQ) ) ),
% 1.08/0.67 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 1.08/0.67 fof(f226,plain,(
% 1.08/0.67 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W0))|W0=W1))),
% 1.08/0.67 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 1.08/0.67 fof(f227,plain,(
% 1.08/0.67 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,X0)|X0=X1)),
% 1.08/0.67 inference(cnf_transformation,[status(thm)],[f226])).
% 1.08/0.67 fof(f437,plain,(
% 1.08/0.67 ![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))))),
% 1.08/0.67 inference(pre_NNF_transformation,[status(thm)],[f82])).
% 1.08/0.67 fof(f439,plain,(
% 1.08/0.67 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,sdtlpdtrp0(xN,X0))|aElementOf0(X1,szNzAzT0))),
% 1.08/0.67 inference(cnf_transformation,[status(thm)],[f437])).
% 1.08/0.67 fof(f629,plain,(
% 1.08/0.67 (aElementOf0(xp,xQ)&(![W0]: (~aElementOf0(W0,xQ)|sdtlseqdt0(xp,W0))))&xp=szmzizndt0(xQ)),
% 1.08/0.67 inference(pre_NNF_transformation,[status(thm)],[f103])).
% 1.08/0.67 fof(f631,plain,(
% 1.08/0.67 ![X0]: (~aElementOf0(X0,xQ)|sdtlseqdt0(xp,X0))),
% 1.08/0.67 inference(cnf_transformation,[status(thm)],[f629])).
% 1.08/0.67 fof(f632,plain,(
% 1.08/0.67 xp=szmzizndt0(xQ)),
% 1.08/0.67 inference(cnf_transformation,[status(thm)],[f629])).
% 1.08/0.67 fof(f662,plain,(
% 1.08/0.67 aElementOf0(xx,xQ)),
% 1.08/0.67 inference(cnf_transformation,[status(thm)],[f113])).
% 1.08/0.67 fof(f663,plain,(
% 1.08/0.67 ~xx=szmzizndt0(xQ)),
% 1.08/0.67 inference(cnf_transformation,[status(thm)],[f113])).
% 1.08/0.67 fof(f665,plain,(
% 1.08/0.67 aElementOf0(xx,szNzAzT0)&(aElementOf0(sK38_skl,sdtlbdtrb0(xd,szDzizrdt0(xd)))&sdtlpdtrp0(xe,sK38_skl)=xx)),
% 1.08/0.67 inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl]),skolemize(W0,sK38_skl)],[f114])).
% 1.08/0.67 fof(f666,plain,(
% 1.08/0.67 aElementOf0(xx,szNzAzT0)),
% 1.08/0.67 inference(cnf_transformation,[status(thm)],[f665])).
% 1.08/0.67 fof(f669,plain,(
% 1.08/0.67 aElementOf0(xm,szNzAzT0)),
% 1.08/0.67 inference(cnf_transformation,[status(thm)],[f115])).
% 1.08/0.67 fof(f671,plain,(
% 1.08/0.67 ![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xm))|sdtlseqdt0(xx,W0))),
% 1.08/0.67 inference(pre_NNF_transformation,[status(thm)],[f116])).
% 1.08/0.67 fof(f672,plain,(
% 1.08/0.67 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xm))|sdtlseqdt0(xx,X0))),
% 1.08/0.67 inference(cnf_transformation,[status(thm)],[f671])).
% 1.08/0.67 fof(f681,plain,(
% 1.08/0.67 aElementOf0(xp,sdtlpdtrp0(xN,xm))),
% 1.08/0.67 inference(cnf_transformation,[status(thm)],[f119])).
% 1.08/0.67 fof(f947,plain,(
% 1.08/0.67 ~xx=xp),
% 1.08/0.67 inference(forward_demodulation,[status(thm)],[f632,f663])).
% 1.08/0.67 fof(f969,plain,(
% 1.08/0.67 sdtlseqdt0(xp,xx)),
% 1.08/0.67 inference(resolution,[status(thm)],[f662,f631])).
% 1.08/0.67 fof(f980,plain,(
% 1.08/0.67 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xm))|aElementOf0(X0,szNzAzT0))),
% 1.08/0.68 inference(resolution,[status(thm)],[f669,f439])).
% 1.08/0.68 fof(f985,plain,(
% 1.08/0.68 sdtlseqdt0(xx,xp)),
% 1.08/0.68 inference(resolution,[status(thm)],[f672,f681])).
% 1.08/0.68 fof(f1001,plain,(
% 1.08/0.68 aElementOf0(xp,szNzAzT0)),
% 1.08/0.68 inference(resolution,[status(thm)],[f980,f681])).
% 1.08/0.68 fof(f1100,plain,(
% 1.08/0.68 ![X0]: (~aElementOf0(X0,szNzAzT0)|~sdtlseqdt0(X0,xx)|~sdtlseqdt0(xx,X0)|X0=xx)),
% 1.08/0.68 inference(resolution,[status(thm)],[f227,f666])).
% 1.08/0.68 fof(f1124,plain,(
% 1.08/0.68 ~aElementOf0(xp,szNzAzT0)|~sdtlseqdt0(xp,xx)|xp=xx),
% 1.08/0.68 inference(resolution,[status(thm)],[f1100,f985])).
% 1.08/0.68 fof(f1127,plain,(
% 1.08/0.68 ~sdtlseqdt0(xp,xx)|xp=xx),
% 1.08/0.68 inference(forward_subsumption_resolution,[status(thm)],[f1124,f1001])).
% 1.08/0.68 fof(f1231,plain,(
% 1.08/0.68 xp=xx),
% 1.08/0.68 inference(resolution,[status(thm)],[f1127,f969])).
% 1.08/0.68 fof(f1233,plain,(
% 1.08/0.68 $false),
% 1.08/0.68 inference(forward_subsumption_resolution,[status(thm)],[f1231,f947])).
% 1.08/0.68 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.71 % Elapsed time: 0.339400 seconds
% 0.19/0.71 % CPU time: 2.136199 seconds
% 0.19/0.71 % Total memory used: 153.868 MB
% 0.19/0.71 % Net memory used: 151.535 MB
%------------------------------------------------------------------------------