%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM426+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 : n003.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:52 PM UTC 2026
% Result : Theorem 110.80s 14.52s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM426+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n003.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:30:00 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.14/0.38 % Drodi V4.1.1
% 110.80/14.52 % Refutation found
% 110.80/14.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 110.80/14.52 % SZS output start CNFRefutation for theBenchmark
% 110.80/14.52 fof(f2,axiom,(
% 110.80/14.52 aInteger0(sz00) ),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f3,axiom,(
% 110.80/14.52 aInteger0(sz10) ),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f4,axiom,(
% 110.80/14.52 (! [W0] :( aInteger0(W0)=> aInteger0(smndt0(W0)) ) )),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f7,axiom,(
% 110.80/14.52 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) )),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f8,axiom,(
% 110.80/14.52 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f9,axiom,(
% 110.80/14.52 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f10,axiom,(
% 110.80/14.52 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,smndt0(W0)) = sz00& sz00 = sdtpldt0(smndt0(W0),W0) ) ) )),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f11,axiom,(
% 110.80/14.52 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtasdt0(W0,sdtasdt0(W1,W2)) = sdtasdt0(sdtasdt0(W0,W1),W2) ) )),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f12,axiom,(
% 110.80/14.52 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f13,axiom,(
% 110.80/14.52 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f14,axiom,(
% 110.80/14.52 (! [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)) ) ) )),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f16,axiom,(
% 110.80/14.52 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(smndt0(sz10),W0) = smndt0(W0)& smndt0(W0) = sdtasdt0(W0,smndt0(sz10)) ) ) )),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f21,hypothesis,(
% 110.80/14.52 ( aInteger0(xa)& aInteger0(xb)& aInteger0(xq)& xq != sz00 ) ),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f23,hypothesis,(
% 110.80/14.52 ( aInteger0(xn)& sdtasdt0(xq,xn) = sdtpldt0(xa,smndt0(xb)) ) ),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f24,conjecture,(
% 110.80/14.52 sdtasdt0(xq,smndt0(xn)) = sdtpldt0(xb,smndt0(xa)) ),
% 110.80/14.52 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 110.80/14.52 fof(f25,negated_conjecture,(
% 110.80/14.52 ~(sdtasdt0(xq,smndt0(xn)) = sdtpldt0(xb,smndt0(xa)) )),
% 110.80/14.52 inference(negated_conjecture,[status(cth)],[f24])).
% 110.80/14.52 fof(f29,plain,(
% 110.80/14.52 aInteger0(sz00)),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f2])).
% 110.80/14.52 fof(f30,plain,(
% 110.80/14.52 aInteger0(sz10)),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f3])).
% 110.80/14.52 fof(f31,plain,(
% 110.80/14.52 ![W0]: (~aInteger0(W0)|aInteger0(smndt0(W0)))),
% 110.80/14.52 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 110.80/14.52 fof(f32,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|aInteger0(smndt0(X0)))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f31])).
% 110.80/14.52 fof(f37,plain,(
% 110.80/14.52 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtpldt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtpldt0(W0,W1),W2))),
% 110.80/14.52 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 110.80/14.52 fof(f38,plain,(
% 110.80/14.52 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtpldt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtpldt0(X0,X1),X2))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f37])).
% 110.80/14.52 fof(f39,plain,(
% 110.80/14.52 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 110.80/14.52 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 110.80/14.52 fof(f40,plain,(
% 110.80/14.52 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f39])).
% 110.80/14.52 fof(f41,plain,(
% 110.80/14.52 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 110.80/14.52 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 110.80/14.52 fof(f42,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=X0)),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f41])).
% 110.80/14.52 fof(f43,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|X0=sdtpldt0(sz00,X0))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f41])).
% 110.80/14.52 fof(f44,plain,(
% 110.80/14.52 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,smndt0(W0))=sz00&sz00=sdtpldt0(smndt0(W0),W0)))),
% 110.80/14.52 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 110.80/14.52 fof(f45,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(X0))=sz00)),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f44])).
% 110.80/14.52 fof(f46,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sz00=sdtpldt0(smndt0(X0),X0))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f44])).
% 110.80/14.52 fof(f47,plain,(
% 110.80/14.52 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtasdt0(W0,sdtasdt0(W1,W2))=sdtasdt0(sdtasdt0(W0,W1),W2))),
% 110.80/14.52 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 110.80/14.52 fof(f48,plain,(
% 110.80/14.52 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(X0,sdtasdt0(X1,X2))=sdtasdt0(sdtasdt0(X0,X1),X2))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f47])).
% 110.80/14.52 fof(f49,plain,(
% 110.80/14.52 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 110.80/14.52 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 110.80/14.52 fof(f50,plain,(
% 110.80/14.52 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f49])).
% 110.80/14.52 fof(f51,plain,(
% 110.80/14.52 ![W0]: (~aInteger0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 110.80/14.52 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 110.80/14.52 fof(f53,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|X0=sdtasdt0(sz10,X0))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f51])).
% 110.80/14.52 fof(f54,plain,(
% 110.80/14.52 ![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))))),
% 110.80/14.52 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 110.80/14.52 fof(f55,plain,(
% 110.80/14.52 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f54])).
% 110.80/14.52 fof(f56,plain,(
% 110.80/14.52 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(sdtpldt0(X0,X1),X2)=sdtpldt0(sdtasdt0(X0,X2),sdtasdt0(X1,X2)))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f54])).
% 110.80/14.52 fof(f60,plain,(
% 110.80/14.52 ![W0]: (~aInteger0(W0)|(sdtasdt0(smndt0(sz10),W0)=smndt0(W0)&smndt0(W0)=sdtasdt0(W0,smndt0(sz10))))),
% 110.80/14.52 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 110.80/14.52 fof(f61,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(smndt0(sz10),X0)=smndt0(X0))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f60])).
% 110.80/14.52 fof(f62,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|smndt0(X0)=sdtasdt0(X0,smndt0(sz10)))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f60])).
% 110.80/14.52 fof(f80,plain,(
% 110.80/14.52 aInteger0(xa)),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f21])).
% 110.80/14.52 fof(f81,plain,(
% 110.80/14.52 aInteger0(xb)),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f21])).
% 110.80/14.52 fof(f82,plain,(
% 110.80/14.52 aInteger0(xq)),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f21])).
% 110.80/14.52 fof(f85,plain,(
% 110.80/14.52 aInteger0(xn)),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f23])).
% 110.80/14.52 fof(f86,plain,(
% 110.80/14.52 sdtasdt0(xq,xn)=sdtpldt0(xa,smndt0(xb))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f23])).
% 110.80/14.52 fof(f87,plain,(
% 110.80/14.52 ~sdtasdt0(xq,smndt0(xn))=sdtpldt0(xb,smndt0(xa))),
% 110.80/14.52 inference(cnf_transformation,[status(thm)],[f25])).
% 110.80/14.52 fof(f95,plain,(
% 110.80/14.52 aInteger0(smndt0(xa))),
% 110.80/14.52 inference(resolution,[status(thm)],[f80,f32])).
% 110.80/14.52 fof(f106,plain,(
% 110.80/14.52 aInteger0(smndt0(xb))),
% 110.80/14.52 inference(resolution,[status(thm)],[f81,f32])).
% 110.80/14.52 fof(f117,plain,(
% 110.80/14.52 aInteger0(smndt0(xq))),
% 110.80/14.52 inference(resolution,[status(thm)],[f82,f32])).
% 110.80/14.52 fof(f122,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,xq)=sdtasdt0(xq,X0))),
% 110.80/14.52 inference(resolution,[status(thm)],[f82,f50])).
% 110.80/14.52 fof(f128,plain,(
% 110.80/14.52 aInteger0(smndt0(xn))),
% 110.80/14.52 inference(resolution,[status(thm)],[f85,f32])).
% 110.80/14.52 fof(f152,plain,(
% 110.80/14.52 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(X1,xq))=sdtpldt0(sdtpldt0(X0,X1),xq))),
% 110.80/14.52 inference(resolution,[status(thm)],[f38,f82])).
% 110.80/14.52 fof(f153,plain,(
% 110.80/14.52 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(X1,xb))=sdtpldt0(sdtpldt0(X0,X1),xb))),
% 110.80/14.52 inference(resolution,[status(thm)],[f38,f81])).
% 110.80/14.52 fof(f164,plain,(
% 110.80/14.52 xq=sdtpldt0(sz00,xq)),
% 110.80/14.52 inference(resolution,[status(thm)],[f43,f82])).
% 110.80/14.52 fof(f165,plain,(
% 110.80/14.52 xb=sdtpldt0(sz00,xb)),
% 110.80/14.52 inference(resolution,[status(thm)],[f43,f81])).
% 110.80/14.52 fof(f167,plain,(
% 110.80/14.52 sdtasdt0(smndt0(sz10),xn)=smndt0(xn)),
% 110.80/14.52 inference(resolution,[status(thm)],[f61,f85])).
% 110.80/14.52 fof(f168,plain,(
% 110.80/14.52 sdtasdt0(smndt0(sz10),xq)=smndt0(xq)),
% 110.80/14.52 inference(resolution,[status(thm)],[f61,f82])).
% 110.80/14.52 fof(f171,plain,(
% 110.80/14.52 smndt0(xn)=sdtasdt0(xn,smndt0(sz10))),
% 110.80/14.52 inference(resolution,[status(thm)],[f62,f85])).
% 110.80/14.52 fof(f174,plain,(
% 110.80/14.52 smndt0(xa)=sdtasdt0(xa,smndt0(sz10))),
% 110.80/14.52 inference(resolution,[status(thm)],[f62,f80])).
% 110.80/14.52 fof(f196,plain,(
% 110.80/14.52 sdtasdt0(smndt0(sz10),sz00)=smndt0(sz00)),
% 110.80/14.52 inference(resolution,[status(thm)],[f29,f61])).
% 110.80/14.52 fof(f199,plain,(
% 110.80/14.52 sdtpldt0(sz00,smndt0(sz00))=sz00),
% 110.80/14.52 inference(resolution,[status(thm)],[f29,f45])).
% 110.80/14.52 fof(f210,plain,(
% 110.80/14.52 aInteger0(smndt0(sz00))),
% 110.80/14.52 inference(resolution,[status(thm)],[f29,f32])).
% 110.80/14.52 fof(f212,plain,(
% 110.80/14.52 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,sdtpldt0(X1,sz00))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,sz00)))),
% 110.80/14.52 inference(resolution,[status(thm)],[f29,f55])).
% 110.80/14.52 fof(f244,plain,(
% 110.80/14.52 aInteger0(smndt0(sz10))),
% 110.80/14.52 inference(resolution,[status(thm)],[f30,f32])).
% 110.80/14.52 fof(f249,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz10)=sdtasdt0(sz10,X0))),
% 110.80/14.52 inference(resolution,[status(thm)],[f30,f50])).
% 110.80/14.52 fof(f254,plain,(
% 110.80/14.52 sz00=sdtpldt0(smndt0(xq),xq)),
% 110.80/14.52 inference(resolution,[status(thm)],[f46,f82])).
% 110.80/14.52 fof(f255,plain,(
% 110.80/14.52 sz00=sdtpldt0(smndt0(xb),xb)),
% 110.80/14.52 inference(resolution,[status(thm)],[f46,f81])).
% 110.80/14.52 fof(f271,plain,(
% 110.80/14.52 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,sdtasdt0(X1,xn))=sdtasdt0(sdtasdt0(X0,X1),xn))),
% 110.80/14.52 inference(resolution,[status(thm)],[f48,f85])).
% 110.80/14.52 fof(f272,plain,(
% 110.80/14.52 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,sdtasdt0(X1,xq))=sdtasdt0(sdtasdt0(X0,X1),xq))),
% 110.80/14.52 inference(resolution,[status(thm)],[f48,f82])).
% 110.80/14.52 fof(f343,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(sz10,xn))=sdtasdt0(sdtasdt0(X0,sz10),xn))),
% 110.80/14.52 inference(resolution,[status(thm)],[f271,f30])).
% 110.80/14.52 fof(f387,plain,(
% 110.80/14.52 xn=sdtasdt0(sz10,xn)),
% 110.80/14.52 inference(resolution,[status(thm)],[f53,f85])).
% 110.80/14.52 fof(f388,plain,(
% 110.80/14.52 xq=sdtasdt0(sz10,xq)),
% 110.80/14.52 inference(resolution,[status(thm)],[f53,f82])).
% 110.80/14.52 fof(f391,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,xn)=sdtasdt0(sdtasdt0(X0,sz10),xn))),
% 110.80/14.52 inference(backward_demodulation,[status(thm)],[f387,f343])).
% 110.80/14.52 fof(f675,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(xa))=sdtpldt0(smndt0(xa),X0))),
% 110.80/14.52 inference(resolution,[status(thm)],[f95,f40])).
% 110.80/14.52 fof(f866,plain,(
% 110.80/14.52 sdtpldt0(xb,smndt0(xa))=sdtpldt0(smndt0(xa),xb)),
% 110.80/14.52 inference(resolution,[status(thm)],[f675,f81])).
% 110.80/14.52 fof(f1096,plain,(
% 110.80/14.52 sz00=sdtpldt0(smndt0(smndt0(xb)),smndt0(xb))),
% 110.80/14.52 inference(resolution,[status(thm)],[f106,f46])).
% 110.80/14.52 fof(f1098,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(smndt0(xb),xb))=sdtpldt0(sdtpldt0(X0,smndt0(xb)),xb))),
% 110.80/14.52 inference(resolution,[status(thm)],[f106,f153])).
% 110.80/14.52 fof(f1101,plain,(
% 110.80/14.52 smndt0(smndt0(xb))=sdtasdt0(smndt0(xb),smndt0(sz10))),
% 110.80/14.52 inference(resolution,[status(thm)],[f106,f62])).
% 110.80/14.52 fof(f1102,plain,(
% 110.80/14.52 sdtasdt0(smndt0(sz10),smndt0(xb))=smndt0(smndt0(xb))),
% 110.80/14.52 inference(resolution,[status(thm)],[f106,f61])).
% 110.80/14.52 fof(f1104,plain,(
% 110.80/14.52 sdtpldt0(smndt0(xb),sz00)=smndt0(xb)),
% 110.80/14.52 inference(resolution,[status(thm)],[f106,f42])).
% 110.80/14.52 fof(f1115,plain,(
% 110.80/14.52 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(sdtpldt0(X0,smndt0(xb)),X1)=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(smndt0(xb),X1)))),
% 110.80/14.52 inference(resolution,[status(thm)],[f106,f56])).
% 110.80/14.52 fof(f1116,plain,(
% 110.80/14.52 aInteger0(smndt0(smndt0(xb)))),
% 110.80/14.52 inference(resolution,[status(thm)],[f106,f32])).
% 110.80/14.52 fof(f1166,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=sdtpldt0(sdtpldt0(X0,smndt0(xb)),xb))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f255,f1098])).
% 110.80/14.52 fof(f1628,plain,(
% 110.80/14.52 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,sdtasdt0(smndt0(xq),X1))=sdtasdt0(sdtasdt0(X0,smndt0(xq)),X1))),
% 110.80/14.52 inference(resolution,[status(thm)],[f117,f48])).
% 110.80/14.52 fof(f1629,plain,(
% 110.80/14.52 sz00=sdtpldt0(smndt0(smndt0(xq)),smndt0(xq))),
% 110.80/14.52 inference(resolution,[status(thm)],[f117,f46])).
% 110.80/14.52 fof(f1632,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(smndt0(xq),xq))=sdtpldt0(sdtpldt0(X0,smndt0(xq)),xq))),
% 110.80/14.52 inference(resolution,[status(thm)],[f117,f152])).
% 110.80/14.52 fof(f1634,plain,(
% 110.80/14.52 smndt0(smndt0(xq))=sdtasdt0(smndt0(xq),smndt0(sz10))),
% 110.80/14.52 inference(resolution,[status(thm)],[f117,f62])).
% 110.80/14.52 fof(f1635,plain,(
% 110.80/14.52 sdtasdt0(smndt0(sz10),smndt0(xq))=smndt0(smndt0(xq))),
% 110.80/14.52 inference(resolution,[status(thm)],[f117,f61])).
% 110.80/14.52 fof(f1637,plain,(
% 110.80/14.52 sdtpldt0(smndt0(xq),sz00)=smndt0(xq)),
% 110.80/14.52 inference(resolution,[status(thm)],[f117,f42])).
% 110.80/14.52 fof(f1649,plain,(
% 110.80/14.52 aInteger0(smndt0(smndt0(xq)))),
% 110.80/14.52 inference(resolution,[status(thm)],[f117,f32])).
% 110.80/14.52 fof(f1654,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,smndt0(xq))=sdtasdt0(smndt0(xq),X0))),
% 110.80/14.52 inference(resolution,[status(thm)],[f117,f50])).
% 110.80/14.52 fof(f1720,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=sdtpldt0(sdtpldt0(X0,smndt0(xq)),xq))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f254,f1632])).
% 110.80/14.52 fof(f1879,plain,(
% 110.80/14.52 sdtasdt0(xn,xq)=sdtasdt0(xq,xn)),
% 110.80/14.52 inference(resolution,[status(thm)],[f122,f85])).
% 110.80/14.52 fof(f1891,plain,(
% 110.80/14.52 sdtasdt0(xn,xq)=sdtpldt0(xa,smndt0(xb))),
% 110.80/14.52 inference(backward_demodulation,[status(thm)],[f1879,f86])).
% 110.80/14.52 fof(f2176,plain,(
% 110.80/14.52 sdtasdt0(smndt0(xn),smndt0(xq))=sdtasdt0(smndt0(xq),smndt0(xn))),
% 110.80/14.52 inference(resolution,[status(thm)],[f128,f1654])).
% 110.80/14.52 fof(f2179,plain,(
% 110.80/14.52 sdtasdt0(smndt0(xn),xq)=sdtasdt0(xq,smndt0(xn))),
% 110.80/14.52 inference(resolution,[status(thm)],[f128,f122])).
% 110.80/14.52 fof(f3803,plain,(
% 110.80/14.52 smndt0(sz00)=sdtpldt0(sz00,smndt0(sz00))),
% 110.80/14.52 inference(resolution,[status(thm)],[f210,f43])).
% 110.80/14.52 fof(f4016,plain,(
% 110.80/14.52 sdtasdt0(smndt0(sz10),sz00)=sz00),
% 110.80/14.52 inference(backward_demodulation,[status(thm)],[f4095,f196])).
% 110.80/14.52 fof(f4095,plain,(
% 110.80/14.52 smndt0(sz00)=sz00),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f199,f3803])).
% 110.80/14.52 fof(f4449,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtpldt0(smndt0(xq),sz00))=sdtpldt0(sdtasdt0(X0,smndt0(xq)),sdtasdt0(X0,sz00)))),
% 110.80/14.52 inference(resolution,[status(thm)],[f212,f117])).
% 110.80/14.52 fof(f4450,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtpldt0(smndt0(xb),sz00))=sdtpldt0(sdtasdt0(X0,smndt0(xb)),sdtasdt0(X0,sz00)))),
% 110.80/14.52 inference(resolution,[status(thm)],[f212,f106])).
% 110.80/14.52 fof(f4459,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,smndt0(xq))=sdtpldt0(sdtasdt0(X0,smndt0(xq)),sdtasdt0(X0,sz00)))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f1637,f4449])).
% 110.80/14.52 fof(f4460,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,smndt0(xb))=sdtpldt0(sdtasdt0(X0,smndt0(xb)),sdtasdt0(X0,sz00)))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f1104,f4450])).
% 110.80/14.52 fof(f4901,plain,(
% 110.80/14.52 sdtasdt0(smndt0(sz10),smndt0(xb))=sdtpldt0(sdtasdt0(smndt0(sz10),smndt0(xb)),sdtasdt0(smndt0(sz10),sz00))),
% 110.80/14.52 inference(resolution,[status(thm)],[f244,f4460])).
% 110.80/14.52 fof(f4902,plain,(
% 110.80/14.52 sdtasdt0(smndt0(sz10),smndt0(xq))=sdtpldt0(sdtasdt0(smndt0(sz10),smndt0(xq)),sdtasdt0(smndt0(sz10),sz00))),
% 110.80/14.52 inference(resolution,[status(thm)],[f244,f4459])).
% 110.80/14.52 fof(f5045,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(smndt0(sz10),xq))=sdtasdt0(sdtasdt0(X0,smndt0(sz10)),xq))),
% 110.80/14.52 inference(resolution,[status(thm)],[f244,f272])).
% 110.80/14.52 fof(f5046,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(smndt0(sz10),xn))=sdtasdt0(sdtasdt0(X0,smndt0(sz10)),xn))),
% 110.80/14.52 inference(resolution,[status(thm)],[f244,f271])).
% 110.80/14.52 fof(f5110,plain,(
% 110.80/14.52 smndt0(smndt0(xb))=sdtpldt0(sdtasdt0(smndt0(sz10),smndt0(xb)),sdtasdt0(smndt0(sz10),sz00))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f1102,f4901])).
% 110.80/14.52 fof(f5111,plain,(
% 110.80/14.52 smndt0(smndt0(xb))=sdtpldt0(smndt0(smndt0(xb)),sdtasdt0(smndt0(sz10),sz00))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f1102,f5110])).
% 110.80/14.52 fof(f5112,plain,(
% 110.80/14.52 smndt0(smndt0(xb))=sdtpldt0(smndt0(smndt0(xb)),sz00)),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f4016,f5111])).
% 110.80/14.52 fof(f5113,plain,(
% 110.80/14.52 smndt0(smndt0(xq))=sdtpldt0(sdtasdt0(smndt0(sz10),smndt0(xq)),sdtasdt0(smndt0(sz10),sz00))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f1635,f4902])).
% 110.80/14.52 fof(f5114,plain,(
% 110.80/14.52 smndt0(smndt0(xq))=sdtpldt0(smndt0(smndt0(xq)),sdtasdt0(smndt0(sz10),sz00))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f1635,f5113])).
% 110.80/14.52 fof(f5115,plain,(
% 110.80/14.52 smndt0(smndt0(xq))=sdtpldt0(smndt0(smndt0(xq)),sz00)),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f4016,f5114])).
% 110.80/14.52 fof(f5287,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,smndt0(xq))=sdtasdt0(sdtasdt0(X0,smndt0(sz10)),xq))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f168,f5045])).
% 110.80/14.52 fof(f5288,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,smndt0(xn))=sdtasdt0(sdtasdt0(X0,smndt0(sz10)),xn))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f167,f5046])).
% 110.80/14.52 fof(f5617,plain,(
% 110.80/14.52 sdtasdt0(xn,smndt0(xq))=sdtasdt0(sdtasdt0(xn,smndt0(sz10)),xq)),
% 110.80/14.52 inference(resolution,[status(thm)],[f5287,f85])).
% 110.80/14.52 fof(f5631,plain,(
% 110.80/14.52 sdtasdt0(xn,smndt0(xq))=sdtasdt0(xq,smndt0(xn))),
% 110.80/14.52 inference(backward_demodulation,[status(thm)],[f5632,f2179])).
% 110.80/14.52 fof(f5632,plain,(
% 110.80/14.52 sdtasdt0(xn,smndt0(xq))=sdtasdt0(smndt0(xn),xq)),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f171,f5617])).
% 110.80/14.52 fof(f5636,plain,(
% 110.80/14.52 ~sdtasdt0(xn,smndt0(xq))=sdtpldt0(xb,smndt0(xa))),
% 110.80/14.52 inference(backward_demodulation,[status(thm)],[f5631,f87])).
% 110.80/14.52 fof(f5657,plain,(
% 110.80/14.52 sdtasdt0(smndt0(xq),smndt0(xn))=sdtasdt0(sdtasdt0(smndt0(xq),smndt0(sz10)),xn)),
% 110.80/14.52 inference(resolution,[status(thm)],[f5288,f117])).
% 110.80/14.52 fof(f5669,plain,(
% 110.80/14.52 sdtasdt0(smndt0(xn),smndt0(xq))=sdtasdt0(sdtasdt0(smndt0(xq),smndt0(sz10)),xn)),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f2176,f5657])).
% 110.80/14.52 fof(f5670,plain,(
% 110.80/14.52 sdtasdt0(smndt0(xn),smndt0(xq))=sdtasdt0(smndt0(smndt0(xq)),xn)),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f1634,f5669])).
% 110.80/14.52 fof(f10335,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xb)),smndt0(sz10))=sdtpldt0(sdtasdt0(X0,smndt0(sz10)),sdtasdt0(smndt0(xb),smndt0(sz10))))),
% 110.80/14.52 inference(resolution,[status(thm)],[f1115,f244])).
% 110.80/14.52 fof(f10346,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xb)),smndt0(sz10))=sdtpldt0(sdtasdt0(X0,smndt0(sz10)),smndt0(smndt0(xb))))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f1101,f10335])).
% 110.80/14.52 fof(f10594,plain,(
% 110.80/14.52 sdtpldt0(smndt0(smndt0(xb)),sz00)=sdtpldt0(sdtpldt0(smndt0(smndt0(xb)),smndt0(xb)),xb)),
% 110.80/14.52 inference(resolution,[status(thm)],[f1116,f1166])).
% 110.80/14.52 fof(f10972,plain,(
% 110.80/14.52 smndt0(smndt0(xb))=sdtpldt0(sdtpldt0(smndt0(smndt0(xb)),smndt0(xb)),xb)),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f5112,f10594])).
% 110.80/14.52 fof(f10973,plain,(
% 110.80/14.52 smndt0(smndt0(xb))=sdtpldt0(sz00,xb)),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f1096,f10972])).
% 110.80/14.52 fof(f11109,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(sdtpldt0(X0,smndt0(xb)),smndt0(sz10))=sdtpldt0(sdtasdt0(X0,smndt0(sz10)),xb))),
% 110.80/14.52 inference(backward_demodulation,[status(thm)],[f11125,f10346])).
% 110.80/14.52 fof(f11125,plain,(
% 110.80/14.52 smndt0(smndt0(xb))=xb),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f165,f10973])).
% 110.80/14.52 fof(f11984,plain,(
% 110.80/14.52 sdtasdt0(sdtpldt0(xa,smndt0(xb)),smndt0(sz10))=sdtpldt0(sdtasdt0(xa,smndt0(sz10)),xb)),
% 110.80/14.52 inference(resolution,[status(thm)],[f11109,f80])).
% 110.80/14.52 fof(f12004,plain,(
% 110.80/14.52 sdtasdt0(sdtasdt0(xn,xq),smndt0(sz10))=sdtpldt0(sdtasdt0(xa,smndt0(sz10)),xb)),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f1891,f11984])).
% 110.80/14.52 fof(f12005,plain,(
% 110.80/14.52 sdtasdt0(sdtasdt0(xn,xq),smndt0(sz10))=sdtpldt0(smndt0(xa),xb)),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f174,f12004])).
% 110.80/14.52 fof(f12006,plain,(
% 110.80/14.52 sdtasdt0(sdtasdt0(xn,xq),smndt0(sz10))=sdtpldt0(xb,smndt0(xa))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f866,f12005])).
% 110.80/14.52 fof(f13721,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtasdt0(smndt0(xq),smndt0(sz10)))=sdtasdt0(sdtasdt0(X0,smndt0(xq)),smndt0(sz10)))),
% 110.80/14.52 inference(resolution,[status(thm)],[f1628,f244])).
% 110.80/14.52 fof(f13732,plain,(
% 110.80/14.52 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,smndt0(smndt0(xq)))=sdtasdt0(sdtasdt0(X0,smndt0(xq)),smndt0(sz10)))),
% 110.80/14.52 inference(forward_demodulation,[status(thm)],[f1634,f13721])).
% 110.80/14.52 fof(f14047,plain,(
% 110.80/14.52 sdtasdt0(smndt0(smndt0(xq)),xn)=sdtasdt0(sdtasdt0(smndt0(smndt0(xq)),sz10),xn)),
% 110.80/14.52 inference(resolution,[status(thm)],[f1649,f391])).
% 110.80/14.52 fof(f14082,plain,(
% 110.80/14.52 sdtasdt0(smndt0(smndt0(xq)),sz10)=sdtasdt0(sz10,smndt0(smndt0(xq)))),
% 110.80/14.52 inference(resolution,[status(thm)],[f1649,f249])).
% 110.80/14.52 fof(f14179,plain,(
% 110.80/14.52 sdtpldt0(smndt0(smndt0(xq)),sz00)=sdtpldt0(sdtpldt0(smndt0(smndt0(xq)),smndt0(xq)),xq)),
% 111.58/14.60 inference(resolution,[status(thm)],[f1649,f1720])).
% 111.58/14.60 fof(f14439,plain,(
% 111.58/14.60 sdtasdt0(smndt0(xn),smndt0(xq))=sdtasdt0(sdtasdt0(smndt0(smndt0(xq)),sz10),xn)),
% 111.58/14.60 inference(forward_demodulation,[status(thm)],[f5670,f14047])).
% 111.58/14.60 fof(f14490,plain,(
% 111.58/14.60 sdtasdt0(smndt0(xn),smndt0(xq))=sdtasdt0(sdtasdt0(sz10,smndt0(smndt0(xq))),xn)),
% 111.58/14.60 inference(backward_demodulation,[status(thm)],[f14082,f14439])).
% 111.58/14.60 fof(f14645,plain,(
% 111.58/14.60 smndt0(smndt0(xq))=sdtpldt0(sdtpldt0(smndt0(smndt0(xq)),smndt0(xq)),xq)),
% 111.58/14.60 inference(forward_demodulation,[status(thm)],[f5115,f14179])).
% 111.58/14.60 fof(f14646,plain,(
% 111.58/14.60 smndt0(smndt0(xq))=sdtpldt0(sz00,xq)),
% 111.58/14.60 inference(forward_demodulation,[status(thm)],[f1629,f14645])).
% 111.58/14.60 fof(f14818,plain,(
% 111.58/14.60 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,xq)=sdtasdt0(sdtasdt0(X0,smndt0(xq)),smndt0(sz10)))),
% 111.58/14.60 inference(backward_demodulation,[status(thm)],[f14838,f13732])).
% 111.58/14.60 fof(f14838,plain,(
% 111.58/14.60 smndt0(smndt0(xq))=xq),
% 111.58/14.60 inference(forward_demodulation,[status(thm)],[f164,f14646])).
% 111.58/14.60 fof(f15195,plain,(
% 111.58/14.60 sdtasdt0(smndt0(xn),smndt0(xq))=sdtasdt0(sdtasdt0(sz10,xq),xn)),
% 111.58/14.60 inference(forward_demodulation,[status(thm)],[f14838,f14490])).
% 111.58/14.60 fof(f15196,plain,(
% 111.58/14.60 sdtasdt0(smndt0(xn),smndt0(xq))=sdtasdt0(xq,xn)),
% 111.58/14.60 inference(forward_demodulation,[status(thm)],[f388,f15195])).
% 111.58/14.60 fof(f15224,plain,(
% 111.58/14.60 sdtasdt0(smndt0(xn),smndt0(xq))=sdtasdt0(xn,xq)),
% 111.58/14.60 inference(forward_demodulation,[status(thm)],[f1879,f15196])).
% 111.58/14.60 fof(f15799,plain,(
% 111.58/14.60 sdtasdt0(smndt0(xn),xq)=sdtasdt0(sdtasdt0(smndt0(xn),smndt0(xq)),smndt0(sz10))),
% 111.58/14.60 inference(resolution,[status(thm)],[f14818,f128])).
% 111.58/14.60 fof(f15811,plain,(
% 111.58/14.60 sdtasdt0(xn,smndt0(xq))=sdtasdt0(sdtasdt0(smndt0(xn),smndt0(xq)),smndt0(sz10))),
% 111.58/14.60 inference(forward_demodulation,[status(thm)],[f5632,f15799])).
% 111.58/14.60 fof(f15812,plain,(
% 111.58/14.60 sdtasdt0(xn,smndt0(xq))=sdtasdt0(sdtasdt0(xn,xq),smndt0(sz10))),
% 111.58/14.60 inference(forward_demodulation,[status(thm)],[f15224,f15811])).
% 111.58/14.60 fof(f15813,plain,(
% 111.58/14.60 sdtasdt0(xn,smndt0(xq))=sdtpldt0(xb,smndt0(xa))),
% 111.58/14.60 inference(forward_demodulation,[status(thm)],[f12006,f15812])).
% 111.58/14.60 fof(f15814,plain,(
% 111.58/14.60 $false),
% 111.58/14.60 inference(forward_subsumption_resolution,[status(thm)],[f15813,f5636])).
% 111.58/14.60 % SZS output end CNFRefutation for theBenchmark.p
% 111.58/14.64 % Elapsed time: 14.265351 seconds
% 111.58/14.64 % CPU time: 112.207315 seconds
% 111.58/14.64 % Total memory used: 651.243 MB
% 111.58/14.64 % Net memory used: 598.134 MB
%------------------------------------------------------------------------------