%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM604+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 : n001.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 18.21s 3.20s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM604+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.16/0.44 % Computer : n001.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.45 % CPULimit : 300
% 0.16/0.45 % WCLimit : 300
% 0.16/0.45 % DateTime : Mon Sep 21 02:49:43 UTC 2026
% 0.16/0.45 % CPUTime :
% 0.16/0.53 % Drodi V4.1.1
% 18.21/3.20 % Refutation found
% 18.21/3.20 % SZS status Theorem for theBenchmark: Theorem is valid
% 18.21/3.20 % SZS output start CNFRefutation for theBenchmark
% 18.21/3.20 fof(f91,hypothesis,(
% 18.21/3.20 ( 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)) ) ) )) ),
% 18.21/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/3.20 fof(f99,hypothesis,(
% 18.21/3.20 ( aElementOf0(xi,szNzAzT0)& sdtlpdtrp0(xe,xi) = xx ) ),
% 18.21/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/3.20 fof(f100,hypothesis,(
% 18.21/3.20 ( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xi))=> aElementOf0(W0,xS) ))& aSubsetOf0(sdtlpdtrp0(xN,xi),xS) ) ),
% 18.21/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/3.20 fof(f101,conjecture,(
% 18.21/3.20 aElementOf0(xx,xS) ),
% 18.21/3.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 18.21/3.20 fof(f102,negated_conjecture,(
% 18.21/3.20 ~(aElementOf0(xx,xS) )),
% 18.21/3.20 inference(negated_conjecture,[status(cth)],[f101])).
% 18.21/3.20 fof(f534,plain,(
% 18.21/3.20 (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)))))),
% 18.21/3.20 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 18.21/3.20 fof(f537,plain,(
% 18.21/3.20 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(sdtlpdtrp0(xe,X0),sdtlpdtrp0(xN,X0)))),
% 18.21/3.20 inference(cnf_transformation,[status(thm)],[f534])).
% 18.21/3.20 fof(f591,plain,(
% 18.21/3.20 aElementOf0(xi,szNzAzT0)),
% 18.21/3.20 inference(cnf_transformation,[status(thm)],[f99])).
% 18.21/3.20 fof(f592,plain,(
% 18.21/3.20 sdtlpdtrp0(xe,xi)=xx),
% 18.21/3.20 inference(cnf_transformation,[status(thm)],[f99])).
% 18.21/3.20 fof(f593,plain,(
% 18.21/3.20 (![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xi))|aElementOf0(W0,xS)))&aSubsetOf0(sdtlpdtrp0(xN,xi),xS)),
% 18.21/3.20 inference(pre_NNF_transformation,[status(thm)],[f100])).
% 18.21/3.20 fof(f594,plain,(
% 18.21/3.20 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xi))|aElementOf0(X0,xS))),
% 18.21/3.20 inference(cnf_transformation,[status(thm)],[f593])).
% 18.21/3.20 fof(f596,plain,(
% 18.21/3.20 ~aElementOf0(xx,xS)),
% 18.21/3.20 inference(cnf_transformation,[status(thm)],[f102])).
% 18.21/3.20 fof(f10015,plain,(
% 18.21/3.20 aElementOf0(sdtlpdtrp0(xe,xi),sdtlpdtrp0(xN,xi))),
% 18.21/3.20 inference(resolution,[status(thm)],[f537,f591])).
% 18.21/3.20 fof(f10021,plain,(
% 18.21/3.20 aElementOf0(xx,sdtlpdtrp0(xN,xi))),
% 18.21/3.20 inference(forward_demodulation,[status(thm)],[f592,f10015])).
% 18.21/3.20 fof(f12361,plain,(
% 18.21/3.20 aElementOf0(xx,xS)),
% 18.21/3.20 inference(resolution,[status(thm)],[f594,f10021])).
% 18.21/3.20 fof(f12362,plain,(
% 18.21/3.20 $false),
% 18.21/3.20 inference(forward_subsumption_resolution,[status(thm)],[f12361,f596])).
% 18.21/3.20 % SZS output end CNFRefutation for theBenchmark.p
% 18.21/3.24 % Elapsed time: 2.772294 seconds
% 18.21/3.24 % CPU time: 21.096775 seconds
% 18.21/3.24 % Total memory used: 262.692 MB
% 18.21/3.24 % Net memory used: 251.032 MB
%------------------------------------------------------------------------------