%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM435+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 : n010.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 38.38s 5.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM435+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.17/1.06 % Computer : n010.cluster.edu
% 0.17/1.06 % Model : x86_64 x86_64
% 0.17/1.06 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/1.06 % Memory : 8046.5625MB
% 0.17/1.06 % OS : Linux 6.8.0-71-generic
% 0.17/1.06 % CPULimit : 300
% 0.17/1.06 % WCLimit : 300
% 0.17/1.06 % DateTime : Mon Sep 21 02:29:27 UTC 2026
% 0.17/1.07 % CPUTime :
% 0.17/1.08 % Drodi V4.1.1
% 38.38/5.99 % Refutation found
% 38.38/5.99 % SZS status Theorem for theBenchmark: Theorem is valid
% 38.38/5.99 % SZS output start CNFRefutation for theBenchmark
% 38.38/5.99 fof(f11,axiom,(
% 38.38/5.99 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2) ) )),
% 38.38/5.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.38/5.99 fof(f12,axiom,(
% 38.38/5.99 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 38.38/5.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.38/5.99 fof(f23,hypothesis,(
% 38.38/5.99 ( aInteger0(xa)& aInteger0(xb)& aInteger0(xp)& xp != sz00& aInteger0(xq)& xq != sz00 ) ),
% 38.38/5.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.38/5.99 fof(f25,hypothesis,(
% 38.38/5.99 ( aInteger0(xm)& sdtasdt0(sdtasdt0(xp,xq),xm) = sdtpldt0(xa,smndt0(xb)) ) ),
% 38.38/5.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.38/5.99 fof(f26,conjecture,(
% 38.38/5.99 sdtpldt0(xa,smndt0(xb)) = sdtasdt0(xq,sdtasdt0(xp,xm)) ),
% 38.38/5.99 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 38.38/5.99 fof(f27,negated_conjecture,(
% 38.38/5.99 ~(sdtpldt0(xa,smndt0(xb)) = sdtasdt0(xq,sdtasdt0(xp,xm)) )),
% 38.38/5.99 inference(negated_conjecture,[status(cth)],[f26])).
% 38.38/5.99 fof(f49,plain,(
% 38.38/5.99 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtasdt0(W0,sdtasdt0(W1,W2))=sdtasdt0(sdtasdt0(W0,W1),W2))),
% 38.38/5.99 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 38.38/5.99 fof(f50,plain,(
% 38.38/5.99 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(X0,sdtasdt0(X1,X2))=sdtasdt0(sdtasdt0(X0,X1),X2))),
% 38.38/5.99 inference(cnf_transformation,[status(thm)],[f49])).
% 38.38/5.99 fof(f51,plain,(
% 38.38/5.99 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 38.38/5.99 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 38.38/5.99 fof(f52,plain,(
% 38.38/5.99 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 38.38/5.99 inference(cnf_transformation,[status(thm)],[f51])).
% 38.38/5.99 fof(f88,plain,(
% 38.38/5.99 aInteger0(xp)),
% 38.38/5.99 inference(cnf_transformation,[status(thm)],[f23])).
% 38.38/5.99 fof(f90,plain,(
% 38.38/5.99 aInteger0(xq)),
% 38.38/5.99 inference(cnf_transformation,[status(thm)],[f23])).
% 38.38/5.99 fof(f98,plain,(
% 38.38/5.99 aInteger0(xm)),
% 38.38/5.99 inference(cnf_transformation,[status(thm)],[f25])).
% 38.38/5.99 fof(f99,plain,(
% 38.38/5.99 sdtasdt0(sdtasdt0(xp,xq),xm)=sdtpldt0(xa,smndt0(xb))),
% 38.38/5.99 inference(cnf_transformation,[status(thm)],[f25])).
% 38.38/5.99 fof(f100,plain,(
% 38.38/5.99 ~sdtpldt0(xa,smndt0(xb))=sdtasdt0(xq,sdtasdt0(xp,xm))),
% 38.38/5.99 inference(cnf_transformation,[status(thm)],[f27])).
% 38.38/5.99 fof(f151,plain,(
% 38.38/5.99 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,xp)=sdtasdt0(xp,X0))),
% 38.38/5.99 inference(resolution,[status(thm)],[f88,f52])).
% 38.38/5.99 fof(f155,plain,(
% 38.38/5.99 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,sdtasdt0(xp,X1))=sdtasdt0(sdtasdt0(X0,xp),X1))),
% 38.38/5.99 inference(resolution,[status(thm)],[f88,f50])).
% 38.38/5.99 fof(f743,plain,(
% 38.38/5.99 sdtasdt0(xm,xp)=sdtasdt0(xp,xm)),
% 38.38/5.99 inference(resolution,[status(thm)],[f151,f98])).
% 38.38/5.99 fof(f745,plain,(
% 38.38/5.99 sdtasdt0(xq,xp)=sdtasdt0(xp,xq)),
% 38.38/5.99 inference(resolution,[status(thm)],[f151,f90])).
% 38.38/5.99 fof(f773,plain,(
% 38.38/5.99 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(xp,xm))=sdtasdt0(sdtasdt0(X0,xp),xm))),
% 38.38/5.99 inference(resolution,[status(thm)],[f155,f98])).
% 38.38/5.99 fof(f7579,plain,(
% 38.38/5.99 ~sdtpldt0(xa,smndt0(xb))=sdtasdt0(xq,sdtasdt0(xm,xp))),
% 38.38/5.99 inference(backward_demodulation,[status(thm)],[f743,f100])).
% 38.38/5.99 fof(f7586,plain,(
% 38.38/5.99 sdtasdt0(sdtasdt0(xq,xp),xm)=sdtpldt0(xa,smndt0(xb))),
% 38.38/5.99 inference(backward_demodulation,[status(thm)],[f745,f99])).
% 38.38/5.99 fof(f7862,plain,(
% 38.38/5.99 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(xm,xp))=sdtasdt0(sdtasdt0(X0,xp),xm))),
% 38.38/5.99 inference(forward_demodulation,[status(thm)],[f743,f773])).
% 38.38/5.99 fof(f7877,plain,(
% 38.38/5.99 sdtasdt0(xq,sdtasdt0(xm,xp))=sdtasdt0(sdtasdt0(xq,xp),xm)),
% 38.38/5.99 inference(resolution,[status(thm)],[f7862,f90])).
% 38.38/5.99 fof(f7888,plain,(
% 38.38/5.99 sdtasdt0(xq,sdtasdt0(xm,xp))=sdtpldt0(xa,smndt0(xb))),
% 38.38/5.99 inference(forward_demodulation,[status(thm)],[f7586,f7877])).
% 38.38/5.99 fof(f7889,plain,(
% 38.38/5.99 $false),
% 38.38/5.99 inference(forward_subsumption_resolution,[status(thm)],[f7888,f7579])).
% 38.38/5.99 % SZS output end CNFRefutation for theBenchmark.p
% 1.32/6.01 % Elapsed time: 4.931237 seconds
% 1.32/6.01 % CPU time: 38.726522 seconds
% 1.32/6.01 % Total memory used: 359.317 MB
% 1.32/6.01 % Net memory used: 336.960 MB
%------------------------------------------------------------------------------