%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM622+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 : n009.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 6.31s 1.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM622+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n009.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:12 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.52 % Drodi V4.1.1
% 6.31/1.45 % Refutation found
% 6.31/1.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.31/1.45 % SZS output start CNFRefutation for theBenchmark
% 6.31/1.45 fof(f91,hypothesis,(
% 6.31/1.45 ( 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)) ) ) )) ),
% 6.31/1.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.31/1.45 fof(f111,hypothesis,(
% 6.31/1.45 ( aElementOf0(xn,szDzozmdt0(xd))& sdtlpdtrp0(xd,xn) = szDzizrdt0(xd)& aElementOf0(xn,sdtlbdtrb0(xd,szDzizrdt0(xd)))& aElementOf0(xn,szNzAzT0)& sdtlpdtrp0(xe,xn) = xp ) ),
% 6.31/1.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.31/1.45 fof(f118,hypothesis,(
% 6.31/1.45 ( (! [W0] :( aElementOf0(W0,sdtlpdtrp0(xN,xn))=> aElementOf0(W0,sdtlpdtrp0(xN,xm)) ))& aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm)) ) ),
% 6.31/1.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.31/1.45 fof(f119,conjecture,(
% 6.31/1.45 aElementOf0(xp,sdtlpdtrp0(xN,xm)) ),
% 6.31/1.45 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 6.31/1.45 fof(f120,negated_conjecture,(
% 6.31/1.45 ~(aElementOf0(xp,sdtlpdtrp0(xN,xm)) )),
% 6.31/1.45 inference(negated_conjecture,[status(cth)],[f119])).
% 6.31/1.45 fof(f552,plain,(
% 6.31/1.45 (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)))))),
% 6.31/1.45 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 6.31/1.45 fof(f555,plain,(
% 6.31/1.45 ![X0]: (~aElementOf0(X0,szNzAzT0)|aElementOf0(sdtlpdtrp0(xe,X0),sdtlpdtrp0(xN,X0)))),
% 6.31/1.45 inference(cnf_transformation,[status(thm)],[f552])).
% 6.31/1.45 fof(f657,plain,(
% 6.31/1.45 aElementOf0(xn,szNzAzT0)),
% 6.31/1.45 inference(cnf_transformation,[status(thm)],[f111])).
% 6.31/1.45 fof(f658,plain,(
% 6.31/1.45 sdtlpdtrp0(xe,xn)=xp),
% 6.31/1.45 inference(cnf_transformation,[status(thm)],[f111])).
% 6.31/1.45 fof(f677,plain,(
% 6.31/1.45 (![W0]: (~aElementOf0(W0,sdtlpdtrp0(xN,xn))|aElementOf0(W0,sdtlpdtrp0(xN,xm))))&aSubsetOf0(sdtlpdtrp0(xN,xn),sdtlpdtrp0(xN,xm))),
% 6.31/1.45 inference(pre_NNF_transformation,[status(thm)],[f118])).
% 6.31/1.45 fof(f678,plain,(
% 6.31/1.45 ![X0]: (~aElementOf0(X0,sdtlpdtrp0(xN,xn))|aElementOf0(X0,sdtlpdtrp0(xN,xm)))),
% 6.31/1.45 inference(cnf_transformation,[status(thm)],[f677])).
% 6.31/1.45 fof(f680,plain,(
% 6.31/1.45 ~aElementOf0(xp,sdtlpdtrp0(xN,xm))),
% 6.31/1.45 inference(cnf_transformation,[status(thm)],[f120])).
% 6.31/1.45 fof(f5842,plain,(
% 6.31/1.45 aElementOf0(sdtlpdtrp0(xe,xn),sdtlpdtrp0(xN,xn))),
% 6.31/1.45 inference(resolution,[status(thm)],[f555,f657])).
% 6.31/1.45 fof(f5852,plain,(
% 6.31/1.45 aElementOf0(xp,sdtlpdtrp0(xN,xn))),
% 6.31/1.45 inference(forward_demodulation,[status(thm)],[f658,f5842])).
% 6.31/1.45 fof(f5896,plain,(
% 6.31/1.45 aElementOf0(xp,sdtlpdtrp0(xN,xm))),
% 6.31/1.45 inference(resolution,[status(thm)],[f5852,f678])).
% 6.31/1.45 fof(f5901,plain,(
% 6.31/1.45 $false),
% 6.31/1.45 inference(forward_subsumption_resolution,[status(thm)],[f5896,f680])).
% 6.31/1.45 % SZS output end CNFRefutation for theBenchmark.p
% 6.50/1.47 % Elapsed time: 1.013719 seconds
% 6.50/1.47 % CPU time: 7.192782 seconds
% 6.50/1.47 % Total memory used: 193.409 MB
% 6.50/1.47 % Net memory used: 187.821 MB
%------------------------------------------------------------------------------