%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM422+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 : n002.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:51 PM UTC 2026
% Result : Theorem 42.14s 6.32s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : NUM422+1 : 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/0.44 % Computer : n002.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 02:30:46 UTC 2026
% 0.17/0.45 % CPUTime :
% 0.17/0.47 % Drodi V4.1.1
% 42.14/6.32 % Refutation found
% 42.14/6.32 % SZS status Theorem for theBenchmark: Theorem is valid
% 42.14/6.32 % SZS output start CNFRefutation for theBenchmark
% 42.14/6.32 fof(f2,axiom,(
% 42.14/6.32 aInteger0(sz00) ),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f3,axiom,(
% 42.14/6.32 aInteger0(sz10) ),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f4,axiom,(
% 42.14/6.32 (! [W0] :( aInteger0(W0)=> aInteger0(smndt0(W0)) ) )),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f6,axiom,(
% 42.14/6.32 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> aInteger0(sdtasdt0(W0,W1)) ) )),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f7,axiom,(
% 42.14/6.32 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) )),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f9,axiom,(
% 42.14/6.32 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f10,axiom,(
% 42.14/6.32 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,smndt0(W0)) = sz00& sz00 = sdtpldt0(smndt0(W0),W0) ) ) )),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f12,axiom,(
% 42.14/6.32 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f13,axiom,(
% 42.14/6.32 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f14,axiom,(
% 42.14/6.32 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))& sdtasdt0(sdtpldt0(W0,W1),W2) = sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2)) ) ) )),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f15,axiom,(
% 42.14/6.32 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(W0,sz00) = sz00& sz00 = sdtasdt0(sz00,W0) ) ) )),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f16,hypothesis,(
% 42.14/6.32 aInteger0(xa) ),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f17,conjecture,(
% 42.14/6.32 sdtasdt0(smndt0(sz10),xa) = smndt0(xa) ),
% 42.14/6.32 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 42.14/6.32 fof(f18,negated_conjecture,(
% 42.14/6.32 ~(sdtasdt0(smndt0(sz10),xa) = smndt0(xa) )),
% 42.14/6.32 inference(negated_conjecture,[status(cth)],[f17])).
% 42.14/6.32 fof(f22,plain,(
% 42.14/6.32 aInteger0(sz00)),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f2])).
% 42.14/6.32 fof(f23,plain,(
% 42.14/6.32 aInteger0(sz10)),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f3])).
% 42.14/6.32 fof(f24,plain,(
% 42.14/6.32 ![W0]: (~aInteger0(W0)|aInteger0(smndt0(W0)))),
% 42.14/6.32 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 42.14/6.32 fof(f25,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|aInteger0(smndt0(X0)))),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f24])).
% 42.14/6.32 fof(f28,plain,(
% 42.14/6.32 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|aInteger0(sdtasdt0(W0,W1)))),
% 42.14/6.32 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 42.14/6.32 fof(f29,plain,(
% 42.14/6.32 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|aInteger0(sdtasdt0(X0,X1)))),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f28])).
% 42.14/6.32 fof(f30,plain,(
% 42.14/6.32 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtpldt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtpldt0(W0,W1),W2))),
% 42.14/6.32 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 42.14/6.32 fof(f31,plain,(
% 42.14/6.32 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtpldt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtpldt0(X0,X1),X2))),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f30])).
% 42.14/6.32 fof(f34,plain,(
% 42.14/6.32 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 42.14/6.32 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 42.14/6.32 fof(f35,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=X0)),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f34])).
% 42.14/6.32 fof(f36,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|X0=sdtpldt0(sz00,X0))),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f34])).
% 42.14/6.32 fof(f37,plain,(
% 42.14/6.32 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,smndt0(W0))=sz00&sz00=sdtpldt0(smndt0(W0),W0)))),
% 42.14/6.32 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 42.14/6.32 fof(f38,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(X0))=sz00)),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f37])).
% 42.14/6.32 fof(f39,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|sz00=sdtpldt0(smndt0(X0),X0))),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f37])).
% 42.14/6.32 fof(f42,plain,(
% 42.14/6.32 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 42.14/6.32 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 42.14/6.32 fof(f43,plain,(
% 42.14/6.32 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f42])).
% 42.14/6.32 fof(f44,plain,(
% 42.14/6.32 ![W0]: (~aInteger0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 42.14/6.32 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 42.14/6.32 fof(f45,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz10)=X0)),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f44])).
% 42.14/6.32 fof(f47,plain,(
% 42.14/6.32 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|(sdtasdt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))&sdtasdt0(sdtpldt0(W0,W1),W2)=sdtpldt0(sdtasdt0(W0,W2),sdtasdt0(W1,W2))))),
% 42.14/6.32 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 42.14/6.32 fof(f48,plain,(
% 42.14/6.32 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f47])).
% 42.14/6.32 fof(f50,plain,(
% 42.14/6.32 ![W0]: (~aInteger0(W0)|(sdtasdt0(W0,sz00)=sz00&sz00=sdtasdt0(sz00,W0)))),
% 42.14/6.32 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 42.14/6.32 fof(f51,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz00)=sz00)),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f50])).
% 42.14/6.32 fof(f53,plain,(
% 42.14/6.32 aInteger0(xa)),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f16])).
% 42.14/6.32 fof(f54,plain,(
% 42.14/6.32 ~sdtasdt0(smndt0(sz10),xa)=smndt0(xa)),
% 42.14/6.32 inference(cnf_transformation,[status(thm)],[f18])).
% 42.14/6.32 fof(f55,plain,(
% 42.14/6.32 aInteger0(smndt0(sz10))),
% 42.14/6.32 inference(resolution,[status(thm)],[f25,f23])).
% 42.14/6.32 fof(f76,plain,(
% 42.14/6.32 sz00=sdtpldt0(smndt0(sz10),sz10)),
% 42.14/6.32 inference(resolution,[status(thm)],[f39,f23])).
% 42.14/6.32 fof(f95,plain,(
% 42.14/6.32 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,sdtpldt0(X1,sz10))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,sz10)))),
% 42.14/6.32 inference(resolution,[status(thm)],[f48,f23])).
% 42.14/6.32 fof(f96,plain,(
% 42.14/6.32 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,sdtpldt0(X1,sz00))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,sz00)))),
% 42.14/6.32 inference(resolution,[status(thm)],[f48,f22])).
% 42.14/6.32 fof(f109,plain,(
% 42.14/6.32 sdtasdt0(xa,sz00)=sz00),
% 42.14/6.32 inference(resolution,[status(thm)],[f53,f51])).
% 42.14/6.32 fof(f119,plain,(
% 42.14/6.32 sdtasdt0(xa,sz10)=xa),
% 42.14/6.32 inference(resolution,[status(thm)],[f53,f45])).
% 42.14/6.32 fof(f120,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,xa)=sdtasdt0(xa,X0))),
% 42.14/6.32 inference(resolution,[status(thm)],[f53,f43])).
% 42.14/6.32 fof(f126,plain,(
% 42.14/6.32 sdtpldt0(xa,smndt0(xa))=sz00),
% 42.14/6.32 inference(resolution,[status(thm)],[f53,f38])).
% 42.14/6.32 fof(f133,plain,(
% 42.14/6.32 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(xa,X1))=sdtpldt0(sdtpldt0(X0,xa),X1))),
% 42.14/6.32 inference(resolution,[status(thm)],[f53,f31])).
% 42.14/6.32 fof(f134,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|aInteger0(sdtasdt0(xa,X0)))),
% 42.14/6.32 inference(resolution,[status(thm)],[f53,f29])).
% 42.14/6.32 fof(f136,plain,(
% 42.14/6.32 aInteger0(smndt0(xa))),
% 42.14/6.32 inference(resolution,[status(thm)],[f53,f25])).
% 42.14/6.32 fof(f160,plain,(
% 42.14/6.32 sdtpldt0(smndt0(sz10),sz00)=smndt0(sz10)),
% 42.14/6.32 inference(resolution,[status(thm)],[f55,f35])).
% 42.14/6.32 fof(f455,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtpldt0(smndt0(sz10),sz10))=sdtpldt0(sdtasdt0(X0,smndt0(sz10)),sdtasdt0(X0,sz10)))),
% 42.14/6.32 inference(resolution,[status(thm)],[f95,f55])).
% 42.14/6.32 fof(f459,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz00)=sdtpldt0(sdtasdt0(X0,smndt0(sz10)),sdtasdt0(X0,sz10)))),
% 42.14/6.32 inference(forward_demodulation,[status(thm)],[f76,f455])).
% 42.14/6.32 fof(f461,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtpldt0(smndt0(sz10),sz00))=sdtpldt0(sdtasdt0(X0,smndt0(sz10)),sdtasdt0(X0,sz00)))),
% 42.14/6.32 inference(resolution,[status(thm)],[f96,f55])).
% 42.14/6.32 fof(f465,plain,(
% 42.14/6.32 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,smndt0(sz10))=sdtpldt0(sdtasdt0(X0,smndt0(sz10)),sdtasdt0(X0,sz00)))),
% 42.14/6.32 inference(forward_demodulation,[status(thm)],[f160,f461])).
% 42.14/6.32 fof(f582,plain,(
% 42.14/6.32 sdtasdt0(smndt0(sz10),xa)=sdtasdt0(xa,smndt0(sz10))),
% 42.14/6.32 inference(resolution,[status(thm)],[f120,f55])).
% 42.14/6.32 fof(f586,plain,(
% 42.14/6.32 ~sdtasdt0(xa,smndt0(sz10))=smndt0(xa)),
% 42.14/6.32 inference(backward_demodulation,[status(thm)],[f582,f54])).
% 15.34/6.38 fof(f640,plain,(
% 15.34/6.38 aInteger0(sdtasdt0(xa,smndt0(sz10)))),
% 15.34/6.38 inference(resolution,[status(thm)],[f134,f55])).
% 15.34/6.38 fof(f653,plain,(
% 15.34/6.38 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(xa,smndt0(xa)))=sdtpldt0(sdtpldt0(X0,xa),smndt0(xa)))),
% 15.34/6.38 inference(resolution,[status(thm)],[f136,f133])).
% 15.34/6.38 fof(f718,plain,(
% 15.34/6.38 smndt0(xa)=sdtpldt0(sz00,smndt0(xa))),
% 15.34/6.38 inference(resolution,[status(thm)],[f136,f36])).
% 15.34/6.38 fof(f729,plain,(
% 15.34/6.38 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=sdtpldt0(sdtpldt0(X0,xa),smndt0(xa)))),
% 15.34/6.38 inference(forward_demodulation,[status(thm)],[f126,f653])).
% 15.34/6.38 fof(f2146,plain,(
% 15.34/6.38 sdtasdt0(xa,sz00)=sdtpldt0(sdtasdt0(xa,smndt0(sz10)),sdtasdt0(xa,sz10))),
% 15.34/6.38 inference(resolution,[status(thm)],[f459,f53])).
% 15.34/6.38 fof(f2159,plain,(
% 15.34/6.38 sz00=sdtpldt0(sdtasdt0(xa,smndt0(sz10)),sdtasdt0(xa,sz10))),
% 15.34/6.38 inference(forward_demodulation,[status(thm)],[f109,f2146])).
% 15.34/6.38 fof(f2160,plain,(
% 15.34/6.38 sz00=sdtpldt0(sdtasdt0(xa,smndt0(sz10)),xa)),
% 15.34/6.38 inference(forward_demodulation,[status(thm)],[f119,f2159])).
% 15.34/6.38 fof(f2201,plain,(
% 15.34/6.38 sdtasdt0(xa,smndt0(sz10))=sdtpldt0(sdtasdt0(xa,smndt0(sz10)),sdtasdt0(xa,sz00))),
% 15.34/6.38 inference(resolution,[status(thm)],[f465,f53])).
% 15.34/6.38 fof(f2212,plain,(
% 15.34/6.38 sdtasdt0(xa,smndt0(sz10))=sdtpldt0(sdtasdt0(xa,smndt0(sz10)),sz00)),
% 15.34/6.38 inference(forward_demodulation,[status(thm)],[f109,f2201])).
% 15.34/6.38 fof(f3730,plain,(
% 15.34/6.38 sdtpldt0(sdtasdt0(xa,smndt0(sz10)),sz00)=sdtpldt0(sdtpldt0(sdtasdt0(xa,smndt0(sz10)),xa),smndt0(xa))),
% 15.34/6.38 inference(resolution,[status(thm)],[f729,f640])).
% 15.34/6.38 fof(f3743,plain,(
% 15.34/6.38 sdtasdt0(xa,smndt0(sz10))=sdtpldt0(sdtpldt0(sdtasdt0(xa,smndt0(sz10)),xa),smndt0(xa))),
% 15.34/6.38 inference(forward_demodulation,[status(thm)],[f2212,f3730])).
% 15.34/6.38 fof(f3744,plain,(
% 15.34/6.38 sdtasdt0(xa,smndt0(sz10))=sdtpldt0(sz00,smndt0(xa))),
% 15.34/6.38 inference(forward_demodulation,[status(thm)],[f2160,f3743])).
% 15.34/6.38 fof(f3745,plain,(
% 15.34/6.38 sdtasdt0(xa,smndt0(sz10))=smndt0(xa)),
% 15.34/6.38 inference(forward_demodulation,[status(thm)],[f718,f3744])).
% 15.34/6.38 fof(f3746,plain,(
% 15.34/6.38 $false),
% 15.34/6.38 inference(forward_subsumption_resolution,[status(thm)],[f3745,f586])).
% 15.34/6.38 % SZS output end CNFRefutation for theBenchmark.p
% 15.34/6.39 % Elapsed time: 5.927330 seconds
% 15.34/6.39 % CPU time: 46.129888 seconds
% 15.34/6.39 % Total memory used: 367.354 MB
% 15.34/6.39 % Net memory used: 338.810 MB
%------------------------------------------------------------------------------