%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM421+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 : n006.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 27.55s 3.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM421+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.09/0.36 % Computer : n006.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 02:27:57 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 27.55/3.93 % Refutation found
% 27.55/3.93 % SZS status Theorem for theBenchmark: Theorem is valid
% 27.55/3.93 % SZS output start CNFRefutation for theBenchmark
% 27.55/3.93 fof(f2,axiom,(
% 27.55/3.93 aInteger0(sz00) ),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f3,axiom,(
% 27.55/3.93 aInteger0(sz10) ),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f4,axiom,(
% 27.55/3.93 (! [W0] :( aInteger0(W0)=> aInteger0(smndt0(W0)) ) )),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f5,axiom,(
% 27.55/3.93 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> aInteger0(sdtpldt0(W0,W1)) ) )),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f6,axiom,(
% 27.55/3.93 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> aInteger0(sdtasdt0(W0,W1)) ) )),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f7,axiom,(
% 27.55/3.93 (! [W0,W1,W2] :( ( aInteger0(W0)& aInteger0(W1)& aInteger0(W2) )=> sdtpldt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtpldt0(W0,W1),W2) ) )),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f8,axiom,(
% 27.55/3.93 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f9,axiom,(
% 27.55/3.93 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f10,axiom,(
% 27.55/3.93 (! [W0] :( aInteger0(W0)=> ( sdtpldt0(W0,smndt0(W0)) = sz00& sz00 = sdtpldt0(smndt0(W0),W0) ) ) )),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f12,axiom,(
% 27.55/3.93 (! [W0,W1] :( ( aInteger0(W0)& aInteger0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f13,axiom,(
% 27.55/3.93 (! [W0] :( aInteger0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f14,axiom,(
% 27.55/3.93 (! [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)) ) ) )),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f15,hypothesis,(
% 27.55/3.93 aInteger0(xa) ),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f16,conjecture,(
% 27.55/3.93 ( sdtasdt0(xa,sz00) = sz00& sz00 = sdtasdt0(sz00,xa) ) ),
% 27.55/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 27.55/3.93 fof(f17,negated_conjecture,(
% 27.55/3.93 ~(( sdtasdt0(xa,sz00) = sz00& sz00 = sdtasdt0(sz00,xa) ) )),
% 27.55/3.93 inference(negated_conjecture,[status(cth)],[f16])).
% 27.55/3.93 fof(f21,plain,(
% 27.55/3.93 aInteger0(sz00)),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f2])).
% 27.55/3.93 fof(f22,plain,(
% 27.55/3.93 aInteger0(sz10)),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f3])).
% 27.55/3.93 fof(f23,plain,(
% 27.55/3.93 ![W0]: (~aInteger0(W0)|aInteger0(smndt0(W0)))),
% 27.55/3.93 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 27.55/3.93 fof(f24,plain,(
% 27.55/3.93 ![X0]: (~aInteger0(X0)|aInteger0(smndt0(X0)))),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f23])).
% 27.55/3.93 fof(f25,plain,(
% 27.55/3.93 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|aInteger0(sdtpldt0(W0,W1)))),
% 27.55/3.93 inference(pre_NNF_transformation,[status(thm)],[f5])).
% 27.55/3.93 fof(f26,plain,(
% 27.55/3.93 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|aInteger0(sdtpldt0(X0,X1)))),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f25])).
% 27.55/3.93 fof(f27,plain,(
% 27.55/3.93 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|aInteger0(sdtasdt0(W0,W1)))),
% 27.55/3.93 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 27.55/3.93 fof(f28,plain,(
% 27.55/3.93 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|aInteger0(sdtasdt0(X0,X1)))),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f27])).
% 27.55/3.93 fof(f29,plain,(
% 27.55/3.93 ![W0,W1,W2]: (((~aInteger0(W0)|~aInteger0(W1))|~aInteger0(W2))|sdtpldt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtpldt0(W0,W1),W2))),
% 27.55/3.93 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 27.55/3.93 fof(f30,plain,(
% 27.55/3.93 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtpldt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtpldt0(X0,X1),X2))),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f29])).
% 27.55/3.93 fof(f31,plain,(
% 27.55/3.93 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 27.55/3.93 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 27.55/3.93 fof(f32,plain,(
% 27.55/3.93 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f31])).
% 27.55/3.93 fof(f33,plain,(
% 27.55/3.93 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 27.55/3.93 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 27.55/3.93 fof(f34,plain,(
% 27.55/3.93 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=X0)),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f33])).
% 27.55/3.93 fof(f36,plain,(
% 27.55/3.93 ![W0]: (~aInteger0(W0)|(sdtpldt0(W0,smndt0(W0))=sz00&sz00=sdtpldt0(smndt0(W0),W0)))),
% 27.55/3.93 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 27.55/3.93 fof(f37,plain,(
% 27.55/3.93 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,smndt0(X0))=sz00)),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f36])).
% 27.55/3.93 fof(f41,plain,(
% 27.55/3.93 ![W0,W1]: ((~aInteger0(W0)|~aInteger0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 27.55/3.93 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 27.55/3.93 fof(f42,plain,(
% 27.55/3.93 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f41])).
% 27.55/3.93 fof(f43,plain,(
% 27.55/3.93 ![W0]: (~aInteger0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 27.55/3.93 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 27.55/3.93 fof(f44,plain,(
% 27.55/3.93 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz10)=X0)),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f43])).
% 27.55/3.93 fof(f46,plain,(
% 27.55/3.93 ![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))))),
% 27.55/3.93 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 27.55/3.93 fof(f47,plain,(
% 27.55/3.93 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|~aInteger0(X2)|sdtasdt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f46])).
% 27.55/3.93 fof(f49,plain,(
% 27.55/3.93 aInteger0(xa)),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f15])).
% 27.55/3.93 fof(f50,plain,(
% 27.55/3.93 (~sdtasdt0(xa,sz00)=sz00|~sz00=sdtasdt0(sz00,xa))),
% 27.55/3.93 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 27.55/3.93 fof(f51,plain,(
% 27.55/3.93 ~sdtasdt0(xa,sz00)=sz00|~sz00=sdtasdt0(sz00,xa)),
% 27.55/3.93 inference(cnf_transformation,[status(thm)],[f50])).
% 27.55/3.93 fof(f54,plain,(
% 27.55/3.93 sdtpldt0(sz10,sz00)=sz10),
% 27.55/3.93 inference(resolution,[status(thm)],[f34,f22])).
% 27.55/3.93 fof(f55,plain,(
% 27.55/3.93 sdtpldt0(sz00,sz00)=sz00),
% 27.55/3.93 inference(resolution,[status(thm)],[f34,f21])).
% 27.55/3.93 fof(f67,plain,(
% 27.55/3.93 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(sdtasdt0(X0,X1),sz00)=sdtasdt0(X0,X1))),
% 27.55/3.93 inference(resolution,[status(thm)],[f28,f34])).
% 27.55/3.93 fof(f72,plain,(
% 27.55/3.93 sdtasdt0(xa,sz10)=xa),
% 27.55/3.93 inference(resolution,[status(thm)],[f44,f49])).
% 27.55/3.93 fof(f92,plain,(
% 27.55/3.93 ![X0,X1,X2]: (~aInteger0(X0)|~aInteger0(X1)|sdtpldt0(X0,sdtpldt0(X1,smndt0(X2)))=sdtpldt0(sdtpldt0(X0,X1),smndt0(X2))|~aInteger0(X2))),
% 27.55/3.93 inference(resolution,[status(thm)],[f30,f24])).
% 27.55/3.93 fof(f109,plain,(
% 27.55/3.93 sdtpldt0(xa,smndt0(xa))=sz00),
% 27.55/3.93 inference(resolution,[status(thm)],[f37,f49])).
% 27.55/3.93 fof(f116,plain,(
% 27.55/3.93 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,xa)=sdtpldt0(xa,X0))),
% 27.55/3.93 inference(resolution,[status(thm)],[f32,f49])).
% 27.55/3.93 fof(f165,plain,(
% 27.55/3.93 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,xa)=sdtasdt0(xa,X0))),
% 27.55/3.93 inference(resolution,[status(thm)],[f42,f49])).
% 27.55/3.93 fof(f193,plain,(
% 27.55/3.93 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtpldt0(xa,xa))=sdtpldt0(sdtasdt0(X0,xa),sdtasdt0(X0,xa)))),
% 27.55/3.93 inference(resolution,[status(thm)],[f47,f49])).
% 27.55/3.93 fof(f196,plain,(
% 27.55/3.93 ![X0,X1]: (~aInteger0(X0)|~aInteger0(X1)|sdtasdt0(X0,sdtpldt0(sz10,X1))=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,X1)))),
% 27.55/3.93 inference(resolution,[status(thm)],[f47,f22])).
% 27.55/3.93 fof(f197,plain,(
% 27.55/3.93 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtpldt0(sz00,sz00))=sdtpldt0(sdtasdt0(X0,sz00),sdtasdt0(X0,sz00)))),
% 27.55/3.93 inference(resolution,[status(thm)],[f47,f21])).
% 27.55/3.93 fof(f206,plain,(
% 27.55/3.93 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz00)=sdtpldt0(sdtasdt0(X0,sz00),sdtasdt0(X0,sz00)))),
% 27.55/3.93 inference(forward_demodulation,[status(thm)],[f55,f197])).
% 27.55/3.93 fof(f266,plain,(
% 27.55/3.93 sdtasdt0(sz00,xa)=sdtasdt0(xa,sz00)),
% 27.55/3.93 inference(resolution,[status(thm)],[f165,f21])).
% 27.55/3.93 fof(f269,plain,(
% 27.55/3.93 ~sdtasdt0(sz00,xa)=sz00|~sz00=sdtasdt0(sz00,xa)),
% 27.55/3.93 inference(forward_demodulation,[status(thm)],[f266,f51])).
% 27.55/3.93 fof(f270,plain,(
% 27.55/3.93 ~sdtasdt0(sz00,xa)=sz00),
% 27.55/3.93 inference(duplicate_literals_removal,[status(thm)],[f269])).
% 27.55/3.94 fof(f399,plain,(
% 27.55/3.94 ![X0]: (~aInteger0(X0)|sdtpldt0(sdtasdt0(X0,xa),sz00)=sdtasdt0(X0,xa))),
% 27.55/3.94 inference(resolution,[status(thm)],[f67,f49])).
% 27.55/3.94 fof(f689,plain,(
% 27.55/3.94 sdtpldt0(sdtasdt0(sz00,xa),sz00)=sdtasdt0(sz00,xa)),
% 27.55/3.94 inference(resolution,[status(thm)],[f399,f21])).
% 27.55/3.94 fof(f1116,plain,(
% 27.55/3.94 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sdtpldt0(xa,smndt0(xa)))=sdtpldt0(sdtpldt0(X0,xa),smndt0(xa)))),
% 27.55/3.94 inference(resolution,[status(thm)],[f92,f49])).
% 27.55/3.94 fof(f1129,plain,(
% 27.55/3.94 ![X0]: (~aInteger0(X0)|sdtpldt0(X0,sz00)=sdtpldt0(sdtpldt0(X0,xa),smndt0(xa)))),
% 27.55/3.94 inference(forward_demodulation,[status(thm)],[f109,f1116])).
% 27.55/3.94 fof(f1467,plain,(
% 27.55/3.94 sdtasdt0(xa,sz00)=sdtpldt0(sdtasdt0(xa,sz00),sdtasdt0(xa,sz00))),
% 27.55/3.94 inference(resolution,[status(thm)],[f206,f49])).
% 27.55/3.94 fof(f1470,plain,(
% 27.55/3.94 sdtasdt0(sz00,xa)=sdtpldt0(sdtasdt0(xa,sz00),sdtasdt0(xa,sz00))),
% 27.55/3.94 inference(forward_demodulation,[status(thm)],[f266,f1467])).
% 27.55/3.94 fof(f1471,plain,(
% 27.55/3.94 sdtasdt0(sz00,xa)=sdtpldt0(sdtasdt0(sz00,xa),sdtasdt0(xa,sz00))),
% 27.55/3.94 inference(forward_demodulation,[status(thm)],[f266,f1470])).
% 27.55/3.94 fof(f1472,plain,(
% 27.55/3.94 sdtasdt0(sz00,xa)=sdtpldt0(sdtasdt0(sz00,xa),sdtasdt0(sz00,xa))),
% 27.55/3.94 inference(forward_demodulation,[status(thm)],[f266,f1471])).
% 27.55/3.94 fof(f4179,plain,(
% 27.55/3.94 sdtasdt0(sz00,sdtpldt0(xa,xa))=sdtpldt0(sdtasdt0(sz00,xa),sdtasdt0(sz00,xa))),
% 27.55/3.94 inference(resolution,[status(thm)],[f193,f21])).
% 27.55/3.94 fof(f4182,plain,(
% 27.55/3.94 sdtasdt0(sz00,sdtpldt0(xa,xa))=sdtasdt0(sz00,xa)),
% 27.55/3.94 inference(forward_demodulation,[status(thm)],[f1472,f4179])).
% 27.55/3.94 fof(f4183,plain,(
% 27.55/3.94 ~aInteger0(sz00)|~aInteger0(sdtpldt0(xa,xa))|aInteger0(sdtasdt0(sz00,xa))),
% 27.55/3.94 inference(paramodulation,[status(thm)],[f4182,f28])).
% 27.55/3.94 fof(f4184,plain,(
% 27.55/3.94 ~aInteger0(sdtpldt0(xa,xa))|aInteger0(sdtasdt0(sz00,xa))),
% 27.55/3.94 inference(forward_subsumption_resolution,[status(thm)],[f4183,f21])).
% 27.55/3.94 fof(f4185,plain,(
% 27.55/3.94 aInteger0(sdtasdt0(sz00,xa))|~aInteger0(xa)|~aInteger0(xa)),
% 27.55/3.94 inference(resolution,[status(thm)],[f4184,f26])).
% 27.55/3.94 fof(f4186,plain,(
% 27.55/3.94 aInteger0(sdtasdt0(sz00,xa))|~aInteger0(xa)),
% 27.55/3.94 inference(duplicate_literals_removal,[status(thm)],[f4185])).
% 27.55/3.94 fof(f4187,plain,(
% 27.55/3.94 aInteger0(sdtasdt0(sz00,xa))),
% 27.55/3.94 inference(forward_subsumption_resolution,[status(thm)],[f4186,f49])).
% 27.55/3.94 fof(f4342,plain,(
% 27.55/3.94 sdtpldt0(sdtasdt0(sz00,xa),sz00)=sdtpldt0(sdtpldt0(sdtasdt0(sz00,xa),xa),smndt0(xa))),
% 27.55/3.94 inference(resolution,[status(thm)],[f4187,f1129])).
% 27.55/3.94 fof(f4454,plain,(
% 27.55/3.94 sdtpldt0(sdtasdt0(sz00,xa),xa)=sdtpldt0(xa,sdtasdt0(sz00,xa))),
% 27.55/3.94 inference(resolution,[status(thm)],[f4187,f116])).
% 27.55/3.94 fof(f4567,plain,(
% 27.55/3.94 sdtasdt0(sz00,xa)=sdtpldt0(sdtpldt0(sdtasdt0(sz00,xa),xa),smndt0(xa))),
% 27.55/3.94 inference(forward_demodulation,[status(thm)],[f689,f4342])).
% 27.55/3.94 fof(f5081,plain,(
% 27.55/3.94 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sdtpldt0(sz10,sz00))=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,sz00)))),
% 27.55/3.94 inference(resolution,[status(thm)],[f196,f21])).
% 27.55/3.94 fof(f5082,plain,(
% 27.55/3.94 ![X0]: (~aInteger0(X0)|sdtasdt0(X0,sz10)=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,sz00)))),
% 27.55/3.94 inference(forward_demodulation,[status(thm)],[f54,f5081])).
% 27.55/3.94 fof(f5511,plain,(
% 27.55/3.94 sdtasdt0(xa,sz10)=sdtpldt0(sdtasdt0(xa,sz10),sdtasdt0(xa,sz00))),
% 27.55/3.94 inference(resolution,[status(thm)],[f5082,f49])).
% 27.55/3.94 fof(f5520,plain,(
% 27.55/3.94 xa=sdtpldt0(sdtasdt0(xa,sz10),sdtasdt0(xa,sz00))),
% 27.55/3.94 inference(forward_demodulation,[status(thm)],[f72,f5511])).
% 27.55/3.94 fof(f5521,plain,(
% 27.55/3.94 xa=sdtpldt0(xa,sdtasdt0(xa,sz00))),
% 27.55/3.94 inference(forward_demodulation,[status(thm)],[f72,f5520])).
% 27.55/3.94 fof(f5522,plain,(
% 27.55/3.94 xa=sdtpldt0(xa,sdtasdt0(sz00,xa))),
% 27.55/3.94 inference(forward_demodulation,[status(thm)],[f266,f5521])).
% 27.55/3.94 fof(f5528,plain,(
% 27.55/3.94 sdtpldt0(sdtasdt0(sz00,xa),xa)=xa),
% 27.55/3.94 inference(backward_demodulation,[status(thm)],[f5522,f4454])).
% 27.55/3.94 fof(f10417,plain,(
% 27.55/3.94 sdtasdt0(sz00,xa)=sdtpldt0(xa,smndt0(xa))),
% 27.55/3.94 inference(forward_demodulation,[status(thm)],[f5528,f4567])).
% 27.55/3.94 fof(f10418,plain,(
% 27.55/3.94 sdtasdt0(sz00,xa)=sz00),
% 27.55/3.94 inference(forward_demodulation,[status(thm)],[f109,f10417])).
% 27.55/3.94 fof(f10419,plain,(
% 27.55/3.94 $false),
% 27.55/3.94 inference(forward_subsumption_resolution,[status(thm)],[f10418,f270])).
% 27.55/3.94 % SZS output end CNFRefutation for theBenchmark.p
% 27.55/3.96 % Elapsed time: 3.584557 seconds
% 27.55/3.96 % CPU time: 28.025395 seconds
% 27.55/3.96 % Total memory used: 252.735 MB
% 27.55/3.96 % Net memory used: 233.279 MB
%------------------------------------------------------------------------------