%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM435+1 : 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 : n007.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:53 PM UTC 2026
% Result : Theorem 19.76s 2.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM435+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 02:26:50 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Drodi V4.1.1
% 19.76/2.94 % Refutation found
% 19.76/2.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 19.76/2.94 % SZS output start CNFRefutation for theBenchmark
% 19.76/2.94 fof(f11,axiom,(
% 19.76/2.94 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2) ) )),
% 19.76/2.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.76/2.94 fof(f12,axiom,(
% 19.76/2.94 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 19.76/2.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.76/2.94 fof(f23,hypothesis,(
% 19.76/2.94 ( aInteger0(xa)& aInteger0(xb)& aInteger0(xp)& xp != sz00& aInteger0(xq)& xq != sz00 ) ),
% 19.76/2.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.76/2.94 fof(f25,hypothesis,(
% 19.76/2.94 ( aInteger0(xm)& sdtasdt0(sdtasdt0(xp,xq),xm) = sdtpldt0(xa,smndt0(xb)) ) ),
% 19.76/2.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.76/2.94 fof(f26,conjecture,(
% 19.76/2.94 sdtpldt0(xa,smndt0(xb)) = sdtasdt0(xq,sdtasdt0(xp,xm)) ),
% 19.76/2.94 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 19.76/2.94 fof(f27,negated_conjecture,(
% 19.76/2.94 ~(sdtpldt0(xa,smndt0(xb)) = sdtasdt0(xq,sdtasdt0(xp,xm)) )),
% 19.76/2.94 inference(negated_conjecture,[status(cth)],[f26])).
% 19.76/2.94 fof(f49,plain,(
% 19.76/2.94 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtasdt0(W0,sdtasdt0(W1,W2))=sdtasdt0(sdtasdt0(W0,W1),W2))),
% 19.76/2.94 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 19.76/2.94 fof(f50,plain,(
% 19.76/2.94 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(X0,sdtasdt0(X1,X2))=sdtasdt0(sdtasdt0(X0,X1),X2))),
% 19.76/2.94 inference(cnf_transformation,[status(thm)],[f49])).
% 19.76/2.94 fof(f51,plain,(
% 19.76/2.94 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 19.76/2.94 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 19.76/2.94 fof(f52,plain,(
% 19.76/2.94 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 19.76/2.94 inference(cnf_transformation,[status(thm)],[f51])).
% 19.76/2.94 fof(f88,plain,(
% 19.76/2.94 aInteger0(xp)),
% 19.76/2.94 inference(cnf_transformation,[status(thm)],[f23])).
% 19.76/2.94 fof(f90,plain,(
% 19.76/2.94 aInteger0(xq)),
% 19.76/2.94 inference(cnf_transformation,[status(thm)],[f23])).
% 19.76/2.94 fof(f93,plain,(
% 19.76/2.94 aInteger0(xm)),
% 19.76/2.94 inference(cnf_transformation,[status(thm)],[f25])).
% 19.76/2.94 fof(f94,plain,(
% 19.76/2.94 sdtasdt0(sdtasdt0(xp,xq),xm)=sdtpldt0(xa,smndt0(xb))),
% 19.76/2.94 inference(cnf_transformation,[status(thm)],[f25])).
% 19.76/2.94 fof(f95,plain,(
% 19.76/2.94 ~sdtpldt0(xa,smndt0(xb))=sdtasdt0(xq,sdtasdt0(xp,xm))),
% 19.76/2.94 inference(cnf_transformation,[status(thm)],[f27])).
% 19.76/2.94 fof(f146,plain,(
% 19.76/2.94 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,xp)=sdtasdt0(xp,X0))),
% 19.76/2.94 inference(resolution,[status(thm)],[f88,f52])).
% 19.76/2.94 fof(f150,plain,(
% 19.76/2.94 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,sdtasdt0(xp,X1))=sdtasdt0(sdtasdt0(X0,xp),X1))),
% 19.76/2.94 inference(resolution,[status(thm)],[f88,f50])).
% 19.76/2.94 fof(f675,plain,(
% 19.76/2.94 sdtasdt0(xm,xp)=sdtasdt0(xp,xm)),
% 19.76/2.94 inference(resolution,[status(thm)],[f146,f93])).
% 19.76/2.94 fof(f676,plain,(
% 19.76/2.94 sdtasdt0(xq,xp)=sdtasdt0(xp,xq)),
% 19.76/2.94 inference(resolution,[status(thm)],[f146,f90])).
% 19.76/2.94 fof(f702,plain,(
% 19.76/2.94 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(xp,xm))=sdtasdt0(sdtasdt0(X0,xp),xm))),
% 19.76/2.94 inference(resolution,[status(thm)],[f150,f93])).
% 19.76/2.94 fof(f6166,plain,(
% 19.76/2.94 ~sdtpldt0(xa,smndt0(xb))=sdtasdt0(xq,sdtasdt0(xm,xp))),
% 19.76/2.94 inference(backward_demodulation,[status(thm)],[f675,f95])).
% 19.76/2.94 fof(f6173,plain,(
% 19.76/2.94 sdtasdt0(sdtasdt0(xq,xp),xm)=sdtpldt0(xa,smndt0(xb))),
% 19.76/2.94 inference(backward_demodulation,[status(thm)],[f676,f94])).
% 19.76/2.94 fof(f6392,plain,(
% 19.76/2.94 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(xm,xp))=sdtasdt0(sdtasdt0(X0,xp),xm))),
% 19.76/2.94 inference(forward_demodulation,[status(thm)],[f675,f702])).
% 19.76/2.94 fof(f6405,plain,(
% 19.76/2.94 sdtasdt0(xq,sdtasdt0(xm,xp))=sdtasdt0(sdtasdt0(xq,xp),xm)),
% 19.76/2.94 inference(resolution,[status(thm)],[f6392,f90])).
% 19.76/2.94 fof(f6415,plain,(
% 19.76/2.94 sdtasdt0(xq,sdtasdt0(xm,xp))=sdtpldt0(xa,smndt0(xb))),
% 19.76/2.94 inference(forward_demodulation,[status(thm)],[f6173,f6405])).
% 19.76/2.94 fof(f6416,plain,(
% 19.76/2.94 $false),
% 19.76/2.94 inference(forward_subsumption_resolution,[status(thm)],[f6415,f6166])).
% 19.76/2.94 % SZS output end CNFRefutation for theBenchmark.p
% 19.76/2.96 % Elapsed time: 2.583719 seconds
% 19.76/2.96 % CPU time: 20.173535 seconds
% 19.76/2.96 % Total memory used: 339.272 MB
% 19.76/2.96 % Net memory used: 317.659 MB
%------------------------------------------------------------------------------