%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM624+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 : n005.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 0.28s 0.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM624+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n005.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 02:45:18 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.53 % Drodi V4.1.1
% 0.28/0.87 % Refutation found
% 0.28/0.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.28/0.87 % SZS output start CNFRefutation for theBenchmark
% 0.28/0.87 fof(f35,axiom,(
% 0.28/0.87 (! [W0,W1] :( ( aElementOf0(W0,szNzAzT0)& aElementOf0(W1,szNzAzT0) )=> ( ( sdtlseqdt0(W0,W1)& sdtlseqdt0(W1,W0) )=> W0 = W1 ) ) )),
% 0.28/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.87 fof(f103,hypothesis,(
% 0.28/0.87 ( aElementOf0(xp,xQ)& (! [W0] :( aElementOf0(W0,xQ)=> sdtlseqdt0(xp,W0) ))& xp = szmzizndt0(xQ) ) ),
% 0.28/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.87 fof(f113,hypothesis,(
% 0.28/0.87 ( aElement0(xx)& aElementOf0(xx,xQ)& xx != szmzizndt0(xQ)& aElementOf0(xx,xP) ) ),
% 0.28/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.87 fof(f114,hypothesis,(
% 0.28/0.87 ( aElementOf0(xx,szNzAzT0)& (? [W0] :( aElementOf0(W0,sdtlbdtrb0(xd,szDzizrdt0(xd)))& sdtlpdtrp0(xe,W0) = xx ) )) ),
% 0.28/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.87 fof(f116,hypothesis,(
% 0.28/0.87 (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xm))=> sdtlseqdt0(xx,W0) ) )),
% 0.28/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.87 fof(f119,hypothesis,(
% 0.28/0.87 ( aElementOf0(xp,sdtlpdtrp0(xN,xm))& aElementOf0(xx,xQ) ) ),
% 0.28/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.87 fof(f120,hypothesis,(
% 0.28/0.87 ( (! [W0] :( aElementOf0(W0,xQ)=> aElementOf0(W0,szNzAzT0) ))& (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xm))=> aElementOf0(W0,szNzAzT0) ))& ~ ~ (? [W0] : aElementOf0(W0,xQ))& ~ ~ (? [W0] : aElementOf0(W0,sdtlpdtrp0(xN,xm)) )) ),
% 0.28/0.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.28/0.87 fof(f227,plain,(
% 0.28/0.87 ![W0,W1]: ((~aElementOf0(W0,szNzAzT0)|~aElementOf0(W1,szNzAzT0))|((~sdtlseqdt0(W0,W1)|~sdtlseqdt0(W1,W0))|W0=W1))),
% 0.28/0.87 inference(pre_NNF_transformation,[status(thm)],[f35])).
% 0.28/0.87 fof(f228,plain,(
% 0.28/0.87 ![X0,X1]: (~aElementOf0(X0,szNzAzT0)|~aElementOf0(X1,szNzAzT0)|~sdtlseqdt0(X0,X1)|~sdtlseqdt0(X1,X0)|X0=X1)),
% 0.28/0.87 inference(cnf_transformation,[status(thm)],[f227])).
% 0.28/0.87 fof(f630,plain,(
% 0.28/0.87 (aElementOf0(xp,xQ)&(![W0]: (~aElementOf0(W0,xQ)|sdtlseqdt0(xp,W0))))&xp=szmzizndt0(xQ)),
% 0.28/0.87 inference(pre_NNF_transformation,[status(thm)],[f103])).
% 0.28/0.87 fof(f632,plain,(
% 0.28/0.87 ![X0]: (~aElementOf0(X0,xQ)|sdtlseqdt0(xp,X0))),
% 0.28/0.87 inference(cnf_transformation,[status(thm)],[f630])).
% 0.28/0.87 fof(f633,plain,(
% 0.28/0.87 xp=szmzizndt0(xQ)),
% 0.28/0.87 inference(cnf_transformation,[status(thm)],[f630])).
% 0.28/0.87 fof(f663,plain,(
% 0.28/0.87 aElementOf0(xx,xQ)),
% 0.28/0.87 inference(cnf_transformation,[status(thm)],[f113])).
% 0.28/0.87 fof(f664,plain,(
% 0.28/0.87 ~xx=szmzizndt0(xQ)),
% 0.28/0.87 inference(cnf_transformation,[status(thm)],[f113])).
% 0.28/0.87 fof(f666,plain,(
% 0.28/0.87 aElementOf0(xx,szNzAzT0)&(aElementOf0(sK38_skl,sdtlbdtrb0(xd,szDzizrdt0(xd)))&sdtlpdtrp0(xe,sK38_skl)=xx)),
% 0.28/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl]),skolemize(W0,sK38_skl)],[f114])).
% 0.28/0.87 fof(f667,plain,(
% 0.28/0.87 aElementOf0(xx,szNzAzT0)),
% 0.28/0.87 inference(cnf_transformation,[status(thm)],[f666])).
% 0.28/0.87 fof(f672,plain,(
% 0.28/0.87 ![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xm))|sdtlseqdt0(xx,W0))),
% 0.28/0.87 inference(pre_NNF_transformation,[status(thm)],[f116])).
% 0.28/0.87 fof(f673,plain,(
% 0.28/0.87 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xm))|sdtlseqdt0(xx,X0))),
% 0.28/0.87 inference(cnf_transformation,[status(thm)],[f672])).
% 0.28/0.87 fof(f682,plain,(
% 0.28/0.87 aElementOf0(xp,sdtlpdtrp0(xN,xm))),
% 0.28/0.87 inference(cnf_transformation,[status(thm)],[f119])).
% 0.28/0.87 fof(f684,plain,(
% 0.28/0.87 (((![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,szNzAzT0)))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xm))|aElementOf0(W0,szNzAzT0))))&(?[W0]: aElementOf0(W0,xQ)))&(?[W0]: aElementOf0(W0,sdtlpdtrp0(xN,xm)))),
% 0.28/0.87 inference(pre_NNF_transformation,[status(thm)],[f120])).
% 0.28/0.87 fof(f685,plain,(
% 0.28/0.87 (((![W0]: (~aElementOf0(W0,xQ)|aElementOf0(W0,szNzAzT0)))&(![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xm))|aElementOf0(W0,szNzAzT0))))&aElementOf0(sK40_skl,xQ))&aElementOf0(sK41_skl,sdtlpdtrp0(xN,xm))),
% 0.28/0.87 inference(skolemize,[status(esa),new_symbols(skolem,[sK40_skl,sK41_skl]),skolemize(W0,sK40_skl),skolemize(W0,sK41_skl)],[f684])).
% 0.28/0.87 fof(f687,plain,(
% 0.28/0.87 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xm))|aElementOf0(X0,szNzAzT0))),
% 0.28/0.87 inference(cnf_transformation,[status(thm)],[f685])).
% 0.28/0.87 fof(f954,plain,(
% 0.28/0.87 ~xx=xp),
% 0.28/0.87 inference(forward_demodulation,[status(thm)],[f633,f664])).
% 0.28/0.87 fof(f976,plain,(
% 0.28/0.87 sdtlseqdt0(xp,xx)),
% 0.28/0.87 inference(resolution,[status(thm)],[f663,f632])).
% 0.28/0.88 fof(f978,plain,(
% 0.28/0.88 sdtlseqdt0(xx,xp)),
% 0.28/0.88 inference(resolution,[status(thm)],[f682,f673])).
% 0.28/0.88 fof(f992,plain,(
% 0.28/0.88 aElementOf0(xp,szNzAzT0)),
% 0.28/0.88 inference(resolution,[status(thm)],[f687,f682])).
% 0.28/0.88 fof(f1106,plain,(
% 0.28/0.88 ![X0]: (~aElementOf0(X0,szNzAzT0)|~sdtlseqdt0(X0,xx)|~sdtlseqdt0(xx,X0)|X0=xx)),
% 0.28/0.88 inference(resolution,[status(thm)],[f228,f667])).
% 0.28/0.88 fof(f1140,plain,(
% 0.28/0.88 ~aElementOf0(xp,szNzAzT0)|~sdtlseqdt0(xp,xx)|xp=xx),
% 0.28/0.88 inference(resolution,[status(thm)],[f1106,f978])).
% 0.28/0.88 fof(f1144,plain,(
% 0.28/0.88 ~sdtlseqdt0(xp,xx)|xp=xx),
% 0.28/0.88 inference(forward_subsumption_resolution,[status(thm)],[f1140,f992])).
% 0.28/0.88 fof(f1245,plain,(
% 0.28/0.88 xp=xx),
% 0.28/0.88 inference(resolution,[status(thm)],[f1144,f976])).
% 0.28/0.88 fof(f1247,plain,(
% 0.28/0.88 $false),
% 0.28/0.88 inference(forward_subsumption_resolution,[status(thm)],[f1245,f954])).
% 0.28/0.88 % SZS output end CNFRefutation for theBenchmark.p
% 0.28/0.91 % Elapsed time: 0.446886 seconds
% 0.28/0.91 % CPU time: 2.672676 seconds
% 0.28/0.91 % Total memory used: 148.594 MB
% 0.28/0.91 % Net memory used: 146.842 MB
%------------------------------------------------------------------------------