%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM474+2 : 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:42:59 PM UTC 2026
% Result : Theorem 28.82s 4.20s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM474+2 : 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.17/0.43 % Computer : n020.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 02:34:02 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.46 % Drodi V4.1.1
% 28.82/4.20 % Refutation found
% 28.82/4.20 % SZS status Theorem for theBenchmark: Theorem is valid
% 28.82/4.20 % SZS output start CNFRefutation for theBenchmark
% 28.82/4.20 fof(f9,axiom,(
% 28.82/4.20 (! [W0,W1] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 28.82/4.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.82/4.20 fof(f13,axiom,(
% 28.82/4.20 (! [W0,W1,W2] :( ( aNaturalNumber0(W0)& aNaturalNumber0(W1)& aNaturalNumber0(W2) )=> ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))& sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) )),
% 28.82/4.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.82/4.20 fof(f34,hypothesis,(
% 28.82/4.20 ( aNaturalNumber0(xl)& aNaturalNumber0(xm)& aNaturalNumber0(xn) ) ),
% 28.82/4.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.82/4.20 fof(f37,hypothesis,(
% 28.82/4.20 ( aNaturalNumber0(xp)& xm = sdtasdt0(xl,xp)& xp = sdtsldt0(xm,xl) ) ),
% 28.82/4.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.82/4.20 fof(f38,hypothesis,(
% 28.82/4.20 ( aNaturalNumber0(xq)& sdtpldt0(xm,xn) = sdtasdt0(xl,xq)& xq = sdtsldt0(sdtpldt0(xm,xn),xl) ) ),
% 28.82/4.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.82/4.20 fof(f40,hypothesis,(
% 28.82/4.20 ( aNaturalNumber0(xr)& sdtpldt0(xp,xr) = xq& xr = sdtmndt0(xq,xp) ) ),
% 28.82/4.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.82/4.20 fof(f41,conjecture,(
% 28.82/4.20 sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr)) = sdtpldt0(sdtasdt0(xl,xp),xn) ),
% 28.82/4.20 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 28.82/4.20 fof(f42,negated_conjecture,(
% 28.82/4.20 ~(sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr)) = sdtpldt0(sdtasdt0(xl,xp),xn) )),
% 28.82/4.20 inference(negated_conjecture,[status(cth)],[f41])).
% 28.82/4.20 fof(f60,plain,(
% 28.82/4.20 ![W0,W1]: ((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 28.82/4.20 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 28.82/4.20 fof(f61,plain,(
% 28.82/4.20 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 28.82/4.20 inference(cnf_transformation,[status(thm)],[f60])).
% 28.82/4.20 fof(f70,plain,(
% 28.82/4.20 ![W0,W1,W2]: (((~aNaturalNumber0(W0)|~aNaturalNumber0(W1))|~aNaturalNumber0(W2))|(sdtasdt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))&sdtasdt0(sdtpldt0(W1,W2),W0)=sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0))))),
% 28.82/4.20 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 28.82/4.20 fof(f71,plain,(
% 28.82/4.20 ![X0,X1,X2]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|~aNaturalNumber0(X2)|sdtasdt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 28.82/4.20 inference(cnf_transformation,[status(thm)],[f70])).
% 28.82/4.20 fof(f140,plain,(
% 28.82/4.20 aNaturalNumber0(xl)),
% 28.82/4.20 inference(cnf_transformation,[status(thm)],[f34])).
% 28.82/4.20 fof(f151,plain,(
% 28.82/4.20 aNaturalNumber0(xp)),
% 28.82/4.20 inference(cnf_transformation,[status(thm)],[f37])).
% 28.82/4.20 fof(f152,plain,(
% 28.82/4.20 xm=sdtasdt0(xl,xp)),
% 28.82/4.20 inference(cnf_transformation,[status(thm)],[f37])).
% 28.82/4.20 fof(f155,plain,(
% 28.82/4.20 sdtpldt0(xm,xn)=sdtasdt0(xl,xq)),
% 28.82/4.20 inference(cnf_transformation,[status(thm)],[f38])).
% 28.82/4.20 fof(f161,plain,(
% 28.82/4.20 aNaturalNumber0(xr)),
% 28.82/4.20 inference(cnf_transformation,[status(thm)],[f40])).
% 28.82/4.20 fof(f162,plain,(
% 28.82/4.20 sdtpldt0(xp,xr)=xq),
% 28.82/4.20 inference(cnf_transformation,[status(thm)],[f40])).
% 28.82/4.20 fof(f164,plain,(
% 28.82/4.20 ~sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr))=sdtpldt0(sdtasdt0(xl,xp),xn)),
% 28.82/4.20 inference(cnf_transformation,[status(thm)],[f42])).
% 28.82/4.20 fof(f180,plain,(
% 28.82/4.20 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,xl)=sdtasdt0(xl,X0))),
% 28.82/4.20 inference(resolution,[status(thm)],[f140,f61])).
% 28.82/4.20 fof(f212,plain,(
% 28.82/4.20 ![X0,X1]: (~aNaturalNumber0(X0)|~aNaturalNumber0(X1)|sdtasdt0(X0,sdtpldt0(xp,X1))=sdtpldt0(sdtasdt0(X0,xp),sdtasdt0(X0,X1)))),
% 28.82/4.20 inference(resolution,[status(thm)],[f151,f71])).
% 28.82/4.20 fof(f224,plain,(
% 28.82/4.20 ~sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr))=sdtpldt0(xm,xn)),
% 28.82/4.20 inference(backward_demodulation,[status(thm)],[f152,f164])).
% 28.82/4.20 fof(f225,plain,(
% 28.82/4.20 ~sdtpldt0(xm,sdtasdt0(xl,xr))=sdtpldt0(xm,xn)),
% 28.82/4.20 inference(forward_demodulation,[status(thm)],[f152,f224])).
% 28.82/4.20 fof(f511,plain,(
% 28.82/4.20 ~sdtpldt0(xm,sdtasdt0(xl,xr))=sdtasdt0(xl,xq)),
% 28.82/4.20 inference(forward_demodulation,[status(thm)],[f155,f225])).
% 28.82/4.20 fof(f646,plain,(
% 28.82/4.20 sdtasdt0(xr,xl)=sdtasdt0(xl,xr)),
% 28.82/4.20 inference(resolution,[status(thm)],[f180,f161])).
% 28.82/4.20 fof(f906,plain,(
% 28.82/4.20 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,sdtpldt0(xp,xr))=sdtpldt0(sdtasdt0(X0,xp),sdtasdt0(X0,xr)))),
% 28.82/4.23 inference(resolution,[status(thm)],[f212,f161])).
% 28.82/4.23 fof(f911,plain,(
% 28.82/4.23 ![X0]: (~aNaturalNumber0(X0)|sdtasdt0(X0,xq)=sdtpldt0(sdtasdt0(X0,xp),sdtasdt0(X0,xr)))),
% 28.82/4.23 inference(forward_demodulation,[status(thm)],[f162,f906])).
% 28.82/4.23 fof(f2248,plain,(
% 28.82/4.23 ~sdtpldt0(xm,sdtasdt0(xr,xl))=sdtasdt0(xl,xq)),
% 28.82/4.23 inference(backward_demodulation,[status(thm)],[f646,f511])).
% 28.82/4.23 fof(f5098,plain,(
% 28.82/4.23 sdtasdt0(xl,xq)=sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr))),
% 28.82/4.23 inference(resolution,[status(thm)],[f911,f140])).
% 28.82/4.23 fof(f5107,plain,(
% 28.82/4.23 sdtasdt0(xl,xq)=sdtpldt0(xm,sdtasdt0(xl,xr))),
% 28.82/4.23 inference(forward_demodulation,[status(thm)],[f152,f5098])).
% 28.82/4.23 fof(f5108,plain,(
% 28.82/4.23 sdtasdt0(xl,xq)=sdtpldt0(xm,sdtasdt0(xr,xl))),
% 28.82/4.23 inference(forward_demodulation,[status(thm)],[f646,f5107])).
% 28.82/4.23 fof(f5109,plain,(
% 28.82/4.23 $false),
% 28.82/4.23 inference(forward_subsumption_resolution,[status(thm)],[f5108,f2248])).
% 28.82/4.23 % SZS output end CNFRefutation for theBenchmark.p
% 4.18/4.26 % Elapsed time: 3.806362 seconds
% 4.18/4.26 % CPU time: 29.612084 seconds
% 4.18/4.26 % Total memory used: 242.109 MB
% 4.18/4.26 % Net memory used: 232.861 MB
%------------------------------------------------------------------------------