%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM454+1 : 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 : n001.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:56 PM UTC 2026
% Result : Theorem 3.41s 0.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM454+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n001.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % 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:36:43 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 3.41/0.87 % Refutation found
% 3.41/0.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.41/0.87 % SZS output start CNFRefutation for theBenchmark
% 3.41/0.87 fof(f3,axiom,(
% 3.41/0.87 aInteger0(sz10) ),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f4,axiom,(
% 3.41/0.87 (! [W0] :( aInteger0(W0)=> aInteger0(smndt0(W0)) ) )),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f7,axiom,(
% 3.41/0.87 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) )),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f8,axiom,(
% 3.41/0.87 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f9,axiom,(
% 3.41/0.87 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f10,axiom,(
% 3.41/0.87 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,smndt0(W0)) = sz00& sz00 = sdtpldt0(smndt0(W0),W0) ) ) )),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f12,axiom,(
% 3.41/0.87 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f13,axiom,(
% 3.41/0.87 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f14,axiom,(
% 3.41/0.87 (! [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)) ) ) )),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f16,axiom,(
% 3.41/0.87 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0)& smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) )),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f17,axiom,(
% 3.41/0.87 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> ( sdtasdt0(W0,W1) = sz00=> ( W0 = sz00| W1 = sz00 ) ) ) )),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f46,hypothesis,(
% 3.41/0.87 ( aInteger0(xp)& xp != sz00& aSubsetOf0(szAzrzSzezqlpdtcmdtrp0(sz10,xp),stldt0(sbsmnsldt0(xS))) ) ),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f49,conjecture,(
% 3.41/0.87 ( sdtpldt0(sz10,xp) != smndt0(sz10)| sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10) ) ),
% 3.41/0.87 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 3.41/0.87 fof(f50,negated_conjecture,(
% 3.41/0.87 ~(( sdtpldt0(sz10,xp) != smndt0(sz10)| sdtpldt0(sz10,smndt0(xp)) != smndt0(sz10) ) )),
% 3.41/0.87 inference(negated_conjecture,[status(cth)],[f49])).
% 3.41/0.87 fof(f55,plain,(
% 3.41/0.87 aInteger0(sz10)),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f3])).
% 3.41/0.87 fof(f56,plain,(
% 3.41/0.87 ![W0]: (~aInteger0(W0)|aInteger0(smndt0(W0)))),
% 3.41/0.87 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 3.41/0.87 fof(f57,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|aInteger0(smndt0(X0)))),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f56])).
% 3.41/0.87 fof(f62,plain,(
% 3.41/0.87 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtpldt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtpldt0(W0,W1),W2))),
% 3.41/0.87 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 3.41/0.87 fof(f63,plain,(
% 3.41/0.87 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtpldt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtpldt0(X0,X1),X2))),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f62])).
% 3.41/0.87 fof(f64,plain,(
% 3.41/0.87 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 3.41/0.87 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 3.41/0.87 fof(f65,plain,(
% 3.41/0.87 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f64])).
% 3.41/0.87 fof(f66,plain,(
% 3.41/0.87 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 3.41/0.87 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 3.41/0.87 fof(f68,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|X0=sdtpldt0(sz00,X0))),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f66])).
% 3.41/0.87 fof(f69,plain,(
% 3.41/0.87 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,smndt0(W0))=sz00&sz00=sdtpldt0(smndt0(W0),W0)))),
% 3.41/0.87 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 3.41/0.87 fof(f70,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(X0))=sz00)),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f69])).
% 3.41/0.87 fof(f71,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|sz00=sdtpldt0(smndt0(X0),X0))),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f69])).
% 3.41/0.87 fof(f74,plain,(
% 3.41/0.87 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 3.41/0.87 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 3.41/0.87 fof(f75,plain,(
% 3.41/0.87 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f74])).
% 3.41/0.87 fof(f76,plain,(
% 3.41/0.87 ![W0]: (~aInteger0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 3.41/0.87 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 3.41/0.87 fof(f77,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz10)=X0)),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f76])).
% 3.41/0.87 fof(f79,plain,(
% 3.41/0.87 ![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))))),
% 3.41/0.87 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 3.41/0.87 fof(f80,plain,(
% 3.41/0.87 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f79])).
% 3.41/0.87 fof(f85,plain,(
% 3.41/0.87 ![W0]: (~aInteger0(W0)|(sdtasdt0(smndt0(sz10),W0)=smndt0(W0)&smndt0(W0)=sdtasdt0(W0,smndt0(sz10))))),
% 3.41/0.87 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 3.41/0.87 fof(f86,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|sdtasdt0(smndt0(sz10),X0)=smndt0(X0))),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f85])).
% 3.41/0.87 fof(f88,plain,(
% 3.41/0.87 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|(~sdtasdt0(W0,W1)=sz00|(W0=sz00|W1=sz00)))),
% 3.41/0.87 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 3.41/0.87 fof(f89,plain,(
% 3.41/0.87 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|~sdtasdt0(X0,X1)=sz00|X0=sz00|X1=sz00)),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f88])).
% 3.41/0.87 fof(f230,plain,(
% 3.41/0.87 aInteger0(xp)),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f46])).
% 3.41/0.87 fof(f231,plain,(
% 3.41/0.87 ~xp=sz00),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f46])).
% 3.41/0.87 fof(f237,plain,(
% 3.41/0.87 (sdtpldt0(sz10,xp)=smndt0(sz10)&sdtpldt0(sz10,smndt0(xp))=smndt0(sz10))),
% 3.41/0.87 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 3.41/0.87 fof(f238,plain,(
% 3.41/0.87 sdtpldt0(sz10,xp)=smndt0(sz10)),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f237])).
% 3.41/0.87 fof(f239,plain,(
% 3.41/0.87 sdtpldt0(sz10,smndt0(xp))=smndt0(sz10)),
% 3.41/0.87 inference(cnf_transformation,[status(thm)],[f237])).
% 3.41/0.87 fof(f289,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz10)=sdtpldt0(sz10,X0))),
% 3.41/0.87 inference(resolution,[status(thm)],[f65,f55])).
% 3.41/0.87 fof(f291,plain,(
% 3.41/0.87 sz10=sdtpldt0(sz00,sz10)),
% 3.41/0.87 inference(resolution,[status(thm)],[f68,f55])).
% 3.41/0.87 fof(f293,plain,(
% 3.41/0.87 sdtasdt0(smndt0(sz10),sz10)=smndt0(sz10)),
% 3.41/0.87 inference(resolution,[status(thm)],[f86,f55])).
% 3.41/0.87 fof(f296,plain,(
% 3.41/0.87 sdtasdt0(smndt0(sz10),xp)=smndt0(xp)),
% 3.41/0.87 inference(resolution,[status(thm)],[f230,f86])).
% 3.41/0.87 fof(f298,plain,(
% 3.41/0.87 xp=sdtpldt0(sz00,xp)),
% 3.41/0.87 inference(resolution,[status(thm)],[f230,f68])).
% 3.41/0.87 fof(f301,plain,(
% 3.41/0.87 aInteger0(smndt0(xp))),
% 3.41/0.87 inference(resolution,[status(thm)],[f57,f230])).
% 3.41/0.87 fof(f302,plain,(
% 3.41/0.87 aInteger0(smndt0(sz10))),
% 3.41/0.87 inference(resolution,[status(thm)],[f57,f55])).
% 3.41/0.87 fof(f306,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,xp)=sdtasdt0(xp,X0))),
% 3.41/0.87 inference(resolution,[status(thm)],[f75,f230])).
% 3.41/0.87 fof(f333,plain,(
% 3.41/0.87 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(X1,xp))=sdtpldt0(sdtpldt0(X0,X1),xp))),
% 3.41/0.87 inference(resolution,[status(thm)],[f63,f230])).
% 3.41/0.87 fof(f334,plain,(
% 3.41/0.87 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(X1,sz10))=sdtpldt0(sdtpldt0(X0,X1),sz10))),
% 3.41/0.87 inference(resolution,[status(thm)],[f63,f55])).
% 3.41/0.87 fof(f342,plain,(
% 3.41/0.87 sdtpldt0(xp,smndt0(xp))=sz00),
% 3.41/0.87 inference(resolution,[status(thm)],[f70,f230])).
% 3.41/0.87 fof(f355,plain,(
% 3.41/0.87 sz00=sdtpldt0(smndt0(xp),xp)),
% 3.41/0.87 inference(resolution,[status(thm)],[f71,f230])).
% 3.41/0.87 fof(f356,plain,(
% 3.41/0.87 sz00=sdtpldt0(smndt0(sz10),sz10)),
% 3.41/0.87 inference(resolution,[status(thm)],[f71,f55])).
% 3.41/0.87 fof(f367,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(sz10,xp))=sdtpldt0(sdtpldt0(X0,sz10),xp))),
% 3.41/0.87 inference(resolution,[status(thm)],[f333,f55])).
% 3.41/0.87 fof(f369,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(sz10))=sdtpldt0(sdtpldt0(X0,sz10),xp))),
% 3.41/0.87 inference(forward_demodulation,[status(thm)],[f238,f367])).
% 3.41/0.87 fof(f371,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(xp,sz10))=sdtpldt0(sdtpldt0(X0,xp),sz10))),
% 3.41/0.87 inference(resolution,[status(thm)],[f334,f230])).
% 3.41/0.87 fof(f407,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtpldt0(sz10,sz10))=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,sz10)))),
% 3.41/0.87 inference(resolution,[status(thm)],[f80,f55])).
% 3.41/0.87 fof(f425,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|~sdtasdt0(X0,xp)=sz00|X0=sz00|xp=sz00)),
% 3.41/0.87 inference(resolution,[status(thm)],[f89,f230])).
% 3.41/0.87 fof(f427,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|~sdtasdt0(X0,xp)=sz00|X0=sz00)),
% 3.41/0.87 inference(forward_subsumption_resolution,[status(thm)],[f425,f231])).
% 3.41/0.87 fof(f429,plain,(
% 3.41/0.87 sdtpldt0(xp,sz10)=sdtpldt0(sz10,xp)),
% 3.41/0.87 inference(resolution,[status(thm)],[f289,f230])).
% 3.41/0.87 fof(f433,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(sz10))=sdtpldt0(sdtpldt0(X0,xp),sz10))),
% 3.41/0.87 inference(backward_demodulation,[status(thm)],[f434,f371])).
% 3.41/0.87 fof(f434,plain,(
% 3.41/0.87 sdtpldt0(xp,sz10)=smndt0(sz10)),
% 3.41/0.87 inference(forward_demodulation,[status(thm)],[f238,f429])).
% 3.41/0.87 fof(f448,plain,(
% 3.41/0.87 sdtpldt0(smndt0(xp),smndt0(sz10))=sdtpldt0(sdtpldt0(smndt0(xp),xp),sz10)),
% 3.41/0.87 inference(resolution,[status(thm)],[f301,f433])).
% 3.41/0.87 fof(f449,plain,(
% 3.41/0.87 sdtpldt0(smndt0(xp),sz10)=sdtpldt0(sz10,smndt0(xp))),
% 3.41/0.87 inference(resolution,[status(thm)],[f301,f289])).
% 3.41/0.87 fof(f464,plain,(
% 3.41/0.87 sdtpldt0(smndt0(xp),smndt0(sz10))=sdtpldt0(sdtpldt0(smndt0(xp),sz10),xp)),
% 3.41/0.87 inference(resolution,[status(thm)],[f301,f369])).
% 3.41/0.87 fof(f469,plain,(
% 3.41/0.87 sdtasdt0(smndt0(xp),sz10)=smndt0(xp)),
% 3.41/0.87 inference(resolution,[status(thm)],[f301,f77])).
% 3.41/0.87 fof(f474,plain,(
% 3.41/0.87 sdtasdt0(smndt0(xp),xp)=sdtasdt0(xp,smndt0(xp))),
% 3.41/0.87 inference(resolution,[status(thm)],[f301,f306])).
% 3.41/0.87 fof(f492,plain,(
% 3.41/0.87 sdtpldt0(smndt0(xp),smndt0(sz10))=sdtpldt0(sz00,sz10)),
% 3.41/0.87 inference(forward_demodulation,[status(thm)],[f355,f448])).
% 3.41/0.87 fof(f493,plain,(
% 3.41/0.87 sdtpldt0(smndt0(xp),smndt0(sz10))=sz10),
% 3.41/0.87 inference(forward_demodulation,[status(thm)],[f291,f492])).
% 3.41/0.87 fof(f494,plain,(
% 3.41/0.87 sdtpldt0(smndt0(xp),sz10)=smndt0(sz10)),
% 3.41/0.87 inference(forward_demodulation,[status(thm)],[f239,f449])).
% 3.41/0.87 fof(f496,plain,(
% 3.41/0.87 sz10=sdtpldt0(sdtpldt0(smndt0(xp),sz10),xp)),
% 3.41/0.87 inference(forward_demodulation,[status(thm)],[f493,f464])).
% 3.41/0.87 fof(f498,plain,(
% 3.41/0.87 sz10=sdtpldt0(smndt0(sz10),xp)),
% 3.41/0.87 inference(forward_demodulation,[status(thm)],[f494,f496])).
% 3.41/0.87 fof(f511,plain,(
% 3.41/0.87 sdtpldt0(smndt0(sz10),smndt0(sz10))=sdtpldt0(sdtpldt0(smndt0(sz10),xp),sz10)),
% 3.41/0.87 inference(resolution,[status(thm)],[f302,f433])).
% 3.41/0.87 fof(f527,plain,(
% 3.41/0.87 sdtpldt0(smndt0(sz10),smndt0(sz10))=sdtpldt0(sdtpldt0(smndt0(sz10),sz10),xp)),
% 3.41/0.87 inference(resolution,[status(thm)],[f302,f369])).
% 3.41/0.87 fof(f555,plain,(
% 3.41/0.87 sdtpldt0(smndt0(sz10),smndt0(sz10))=sdtpldt0(sz10,sz10)),
% 3.41/0.87 inference(forward_demodulation,[status(thm)],[f498,f511])).
% 3.41/0.87 fof(f560,plain,(
% 3.41/0.87 sdtpldt0(sz10,sz10)=sdtpldt0(sdtpldt0(smndt0(sz10),sz10),xp)),
% 3.41/0.87 inference(forward_demodulation,[status(thm)],[f555,f527])).
% 3.41/0.87 fof(f561,plain,(
% 3.41/0.87 sdtpldt0(sz10,sz10)=sdtpldt0(sz00,xp)),
% 3.41/0.87 inference(forward_demodulation,[status(thm)],[f356,f560])).
% 3.41/0.87 fof(f564,plain,(
% 3.41/0.87 sdtpldt0(smndt0(sz10),smndt0(sz10))=xp),
% 3.41/0.87 inference(backward_demodulation,[status(thm)],[f567,f555])).
% 3.41/0.87 fof(f565,plain,(
% 3.41/0.87 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,xp)=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,sz10)))),
% 3.41/0.87 inference(backward_demodulation,[status(thm)],[f567,f407])).
% 3.41/0.87 fof(f567,plain,(
% 3.41/0.87 sdtpldt0(sz10,sz10)=xp),
% 3.41/0.87 inference(forward_demodulation,[status(thm)],[f298,f561])).
% 3.41/0.87 fof(f680,plain,(
% 3.41/0.87 sdtasdt0(smndt0(sz10),xp)=sdtpldt0(sdtasdt0(smndt0(sz10),sz10),sdtasdt0(smndt0(sz10),sz10))),
% 3.41/0.87 inference(resolution,[status(thm)],[f565,f302])).
% 3.41/0.87 fof(f681,plain,(
% 3.41/0.87 sdtasdt0(smndt0(xp),xp)=sdtpldt0(sdtasdt0(smndt0(xp),sz10),sdtasdt0(smndt0(xp),sz10))),
% 3.41/0.87 inference(resolution,[status(thm)],[f565,f301])).
% 3.41/0.87 fof(f685,plain,(
% 3.41/0.87 smndt0(xp)=sdtpldt0(sdtasdt0(smndt0(sz10),sz10),sdtasdt0(smndt0(sz10),sz10))),
% 3.41/0.87 inference(forward_demodulation,[status(thm)],[f296,f680])).
% 3.41/0.87 fof(f686,plain,(
% 3.41/0.88 smndt0(xp)=sdtpldt0(smndt0(sz10),sdtasdt0(smndt0(sz10),sz10))),
% 3.41/0.88 inference(forward_demodulation,[status(thm)],[f293,f685])).
% 3.41/0.88 fof(f687,plain,(
% 3.41/0.88 smndt0(xp)=sdtpldt0(smndt0(sz10),smndt0(sz10))),
% 3.41/0.88 inference(forward_demodulation,[status(thm)],[f293,f686])).
% 3.41/0.88 fof(f735,plain,(
% 3.41/0.88 smndt0(xp)=xp),
% 3.41/0.88 inference(forward_demodulation,[status(thm)],[f564,f687])).
% 3.41/0.88 fof(f736,plain,(
% 3.41/0.88 sdtasdt0(xp,smndt0(xp))=sdtpldt0(sdtasdt0(smndt0(xp),sz10),sdtasdt0(smndt0(xp),sz10))),
% 3.41/0.88 inference(forward_demodulation,[status(thm)],[f474,f681])).
% 3.41/0.88 fof(f737,plain,(
% 3.41/0.88 sdtasdt0(xp,xp)=sdtpldt0(sdtasdt0(smndt0(xp),sz10),sdtasdt0(smndt0(xp),sz10))),
% 3.41/0.88 inference(forward_demodulation,[status(thm)],[f735,f736])).
% 3.41/0.88 fof(f738,plain,(
% 3.41/0.88 sdtasdt0(xp,xp)=sdtpldt0(smndt0(xp),sdtasdt0(smndt0(xp),sz10))),
% 3.41/0.88 inference(forward_demodulation,[status(thm)],[f469,f737])).
% 3.41/0.88 fof(f739,plain,(
% 3.41/0.88 sdtasdt0(xp,xp)=sdtpldt0(xp,sdtasdt0(smndt0(xp),sz10))),
% 3.41/0.88 inference(forward_demodulation,[status(thm)],[f735,f738])).
% 3.41/0.88 fof(f740,plain,(
% 3.41/0.88 sdtasdt0(xp,xp)=sdtpldt0(xp,smndt0(xp))),
% 3.41/0.88 inference(forward_demodulation,[status(thm)],[f469,f739])).
% 3.41/0.88 fof(f743,plain,(
% 3.41/0.88 sdtasdt0(xp,xp)=sz00),
% 3.41/0.88 inference(forward_demodulation,[status(thm)],[f342,f740])).
% 3.41/0.88 fof(f1409,plain,(
% 3.41/0.88 ~sdtasdt0(xp,xp)=sz00|xp=sz00),
% 3.41/0.88 inference(resolution,[status(thm)],[f427,f230])).
% 3.41/0.88 fof(f1412,plain,(
% 3.41/0.88 ~sz00=sz00|xp=sz00),
% 3.41/0.88 inference(forward_demodulation,[status(thm)],[f743,f1409])).
% 3.41/0.88 fof(f1413,plain,(
% 3.41/0.88 xp=sz00),
% 3.41/0.88 inference(trivial_equality_resolution,[status(thm)],[f1412])).
% 3.41/0.88 fof(f1414,plain,(
% 3.41/0.88 $false),
% 3.41/0.88 inference(forward_subsumption_resolution,[status(thm)],[f1413,f231])).
% 3.41/0.88 % SZS output end CNFRefutation for theBenchmark.p
% 0.34/0.89 % Elapsed time: 0.522936 seconds
% 0.34/0.89 % CPU time: 3.775526 seconds
% 0.34/0.89 % Total memory used: 151.748 MB
% 0.34/0.89 % Net memory used: 147.777 MB
%------------------------------------------------------------------------------