%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM620+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 : n020.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 4.07s 1.12s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM620+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.07/0.35 % Computer : n020.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 02:46:03 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.37 % Drodi V4.1.1
% 4.07/1.12 % Refutation found
% 4.07/1.12 % SZS status Theorem for theBenchmark: Theorem is valid
% 4.07/1.12 % SZS output start CNFRefutation for theBenchmark
% 4.07/1.12 fof(f91,hypothesis,(
% 4.07/1.12 ( aFunction0(xe)& szDzozmdt0(xe) = szNzAzT0& (! [W0] :( aElementOf0(W0,szNzAzT0)=> ( aElementOf0(sdtlpdtrp0(xe,W0),sdtlpdtrp0(xN,W0))& (! [W1] :( aElementOf0(W1,sdtlpdtrp0(xN,W0))=> sdtlseqdt0(sdtlpdtrp0(xe,W0),W1) ))& sdtlpdtrp0(xe,W0) = szmzizndt0(sdtlpdtrp0(xN,W0)) ) ) )) ),
% 4.07/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.07/1.12 fof(f115,hypothesis,(
% 4.07/1.12 ( aElementOf0(xm,szNzAzT0)& xx = sdtlpdtrp0(xe,xm) ) ),
% 4.07/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.07/1.12 fof(f117,conjecture,(
% 4.07/1.12 ( ( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xm))=> aElementOf0(W0,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ))& aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn))) )=> aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ) ),
% 4.07/1.12 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.07/1.12 fof(f118,negated_conjecture,(
% 4.07/1.12 ~(( ( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xm))=> aElementOf0(W0,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ))& aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn))) )=> aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))) ) )),
% 4.07/1.12 inference(negated_conjecture,[status(cth)],[f117])).
% 4.07/1.12 fof(f550,plain,(
% 4.07/1.12 (aFunction0(xe)&szDzozmdt0(xe)=szNzAzT0)&(![W0]: (~aElementOf0(W0,szNzAzT0)|((aElementOf0(sdtlpdtrp0(xe,W0),sdtlpdtrp0(xN,W0))&(![W1]: (~aElementOf0(W1,sdtlpdtrp0(xN,W0))|sdtlseqdt0(sdtlpdtrp0(xe,W0),W1))))&sdtlpdtrp0(xe,W0)=szmzizndt0(sdtlpdtrp0(xN,W0)))))),
% 4.07/1.12 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 4.07/1.12 fof(f553,plain,(
% 4.07/1.12 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(sdtlpdtrp0(xe,X0),sdtlpdtrp0(xN,X0)))),
% 4.07/1.12 inference(cnf_transformation,[status(thm)],[f550])).
% 4.07/1.12 fof(f666,plain,(
% 4.07/1.12 aElementOf0(xm,szNzAzT0)),
% 4.07/1.12 inference(cnf_transformation,[status(thm)],[f115])).
% 4.07/1.12 fof(f667,plain,(
% 4.07/1.12 xx=sdtlpdtrp0(xe,xm)),
% 4.07/1.12 inference(cnf_transformation,[status(thm)],[f115])).
% 4.07/1.12 fof(f670,plain,(
% 4.07/1.12 (((![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xm))|aElementOf0(W0,sdtlpdtrp0(xN,szszuzczcdt0(xn)))))&aSubsetOf0(sdtlpdtrp0(xN,xm),sdtlpdtrp0(xN,szszuzczcdt0(xn))))&~aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn))))),
% 4.07/1.12 inference(pre_NNF_transformation,[status(thm)],[f118])).
% 4.07/1.12 fof(f671,plain,(
% 4.07/1.12 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xm))|aElementOf0(X0,sdtlpdtrp0(xN,szszuzczcdt0(xn))))),
% 4.07/1.12 inference(cnf_transformation,[status(thm)],[f670])).
% 4.07/1.12 fof(f673,plain,(
% 4.07/1.12 ~aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 4.07/1.12 inference(cnf_transformation,[status(thm)],[f670])).
% 4.07/1.12 fof(f5877,plain,(
% 4.07/1.12 aElementOf0(sdtlpdtrp0(xe,xm),sdtlpdtrp0(xN,xm))),
% 4.07/1.12 inference(resolution,[status(thm)],[f553,f666])).
% 4.07/1.12 fof(f5882,plain,(
% 4.07/1.12 aElementOf0(xx,sdtlpdtrp0(xN,xm))),
% 4.07/1.12 inference(forward_demodulation,[status(thm)],[f667,f5877])).
% 4.07/1.12 fof(f7912,plain,(
% 4.07/1.12 aElementOf0(xx,sdtlpdtrp0(xN,szszuzczcdt0(xn)))),
% 4.07/1.12 inference(resolution,[status(thm)],[f5882,f671])).
% 4.07/1.12 fof(f7919,plain,(
% 4.07/1.12 $false),
% 4.07/1.12 inference(forward_subsumption_resolution,[status(thm)],[f7912,f673])).
% 4.07/1.12 % SZS output end CNFRefutation for theBenchmark.p
% 4.07/1.13 % Elapsed time: 0.756980 seconds
% 4.07/1.13 % CPU time: 5.659101 seconds
% 4.07/1.13 % Total memory used: 188.293 MB
% 4.07/1.13 % Net memory used: 183.506 MB
%------------------------------------------------------------------------------