%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : RNG082+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 : n015.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 02:05:18 PM UTC 2026
% Result : Theorem 49.28s 6.80s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : RNG082+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.43 % Computer : n015.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 04:21:36 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 49.28/6.80 % Refutation found
% 49.28/6.80 % SZS status Theorem for theBenchmark: Theorem is valid
% 49.28/6.80 % SZS output start CNFRefutation for theBenchmark
% 49.28/6.80 fof(f2,axiom,(
% 49.28/6.80 aElement0(sz00) ),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f3,axiom,(
% 49.28/6.80 aElement0(sz10) ),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f4,axiom,(
% 49.28/6.80 (! [W0] :( aElement0(W0)=> aElement0(smndt0(W0)) ) )),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f6,axiom,(
% 49.28/6.80 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> aElement0(sdtasdt0(W0,W1)) ) )),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f7,axiom,(
% 49.28/6.80 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> sdtpldt0(W0,W1) = sdtpldt0(W1,W0) ) )),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f8,axiom,(
% 49.28/6.80 (! [W0,W1,W2] :( ( aElement0(W0)& aElement0(W1)& aElement0(W2) )=> sdtpldt0(sdtpldt0(W0,W1),W2) = sdtpldt0(W0,sdtpldt0(W1,W2)) ) )),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f9,axiom,(
% 49.28/6.80 (! [W0] :( aElement0(W0)=> ( sdtpldt0(W0,sz00) = W0& W0 = sdtpldt0(sz00,W0) ) ) )),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f10,axiom,(
% 49.28/6.80 (! [W0] :( aElement0(W0)=> ( sdtpldt0(W0,smndt0(W0)) = sz00& sz00 = sdtpldt0(smndt0(W0),W0) ) ) )),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f11,axiom,(
% 49.28/6.80 (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ) )),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f12,axiom,(
% 49.28/6.80 (! [W0,W1,W2] :( ( aElement0(W0)& aElement0(W1)& aElement0(W2) )=> sdtasdt0(sdtasdt0(W0,W1),W2) = sdtasdt0(W0,sdtasdt0(W1,W2)) ) )),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f13,axiom,(
% 49.28/6.80 (! [W0] :( aElement0(W0)=> ( sdtasdt0(W0,sz10) = W0& W0 = sdtasdt0(sz10,W0) ) ) )),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f14,axiom,(
% 49.28/6.80 (! [W0,W1,W2] :( ( aElement0(W0)& aElement0(W1)& aElement0(W2) )=> ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))& sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ) )),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f15,hypothesis,(
% 49.28/6.80 aElement0(xx) ),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f16,conjecture,(
% 49.28/6.80 sdtasdt0(smndt0(sz10),xx) = smndt0(xx) ),
% 49.28/6.80 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 49.28/6.80 fof(f17,negated_conjecture,(
% 49.28/6.80 ~(sdtasdt0(smndt0(sz10),xx) = smndt0(xx) )),
% 49.28/6.80 inference(negated_conjecture,[status(cth)],[f16])).
% 49.28/6.80 fof(f21,plain,(
% 49.28/6.80 aElement0(sz00)),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f2])).
% 49.28/6.80 fof(f22,plain,(
% 49.28/6.80 aElement0(sz10)),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f3])).
% 49.28/6.80 fof(f23,plain,(
% 49.28/6.80 ![W0]: (~aElement0(W0)|aElement0(smndt0(W0)))),
% 49.28/6.80 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 49.28/6.80 fof(f24,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|aElement0(smndt0(X0)))),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f23])).
% 49.28/6.80 fof(f27,plain,(
% 49.28/6.80 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|aElement0(sdtasdt0(W0,W1)))),
% 49.28/6.80 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 49.28/6.80 fof(f28,plain,(
% 49.28/6.80 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|aElement0(sdtasdt0(X0,X1)))),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f27])).
% 49.28/6.80 fof(f29,plain,(
% 49.28/6.80 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|sdtpldt0(W0,W1)=sdtpldt0(W1,W0))),
% 49.28/6.80 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 49.28/6.80 fof(f30,plain,(
% 49.28/6.80 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(X0,X1)=sdtpldt0(X1,X0))),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f29])).
% 49.28/6.80 fof(f31,plain,(
% 49.28/6.80 ![W0,W1,W2]: (((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|sdtpldt0(sdtpldt0(W0,W1),W2)=sdtpldt0(W0,sdtpldt0(W1,W2)))),
% 49.28/6.80 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 49.28/6.80 fof(f32,plain,(
% 49.28/6.80 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sdtpldt0(sdtpldt0(X0,X1),X2)=sdtpldt0(X0,sdtpldt0(X1,X2)))),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f31])).
% 49.28/6.80 fof(f33,plain,(
% 49.28/6.80 ![W0]: (~aElement0(W0)|(sdtpldt0(W0,sz00)=W0&W0=sdtpldt0(sz00,W0)))),
% 49.28/6.80 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 49.28/6.80 fof(f34,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtpldt0(X0,sz00)=X0)),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f33])).
% 49.28/6.80 fof(f35,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|X0=sdtpldt0(sz00,X0))),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f33])).
% 49.28/6.80 fof(f36,plain,(
% 49.28/6.80 ![W0]: (~aElement0(W0)|(sdtpldt0(W0,smndt0(W0))=sz00&sz00=sdtpldt0(smndt0(W0),W0)))),
% 49.28/6.80 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 49.28/6.80 fof(f37,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtpldt0(X0,smndt0(X0))=sz00)),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f36])).
% 49.28/6.80 fof(f38,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sz00=sdtpldt0(smndt0(X0),X0))),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f36])).
% 49.28/6.80 fof(f39,plain,(
% 49.28/6.80 ![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|sdtasdt0(W0,W1)=sdtasdt0(W1,W0))),
% 49.28/6.80 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 49.28/6.80 fof(f40,plain,(
% 49.28/6.80 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtasdt0(X0,X1)=sdtasdt0(X1,X0))),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f39])).
% 49.28/6.80 fof(f41,plain,(
% 49.28/6.80 ![W0,W1,W2]: (((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|sdtasdt0(sdtasdt0(W0,W1),W2)=sdtasdt0(W0,sdtasdt0(W1,W2)))),
% 49.28/6.80 inference(pre_NNF_transformation,[status(thm)],[f12])).
% 49.28/6.80 fof(f42,plain,(
% 49.28/6.80 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sdtasdt0(sdtasdt0(X0,X1),X2)=sdtasdt0(X0,sdtasdt0(X1,X2)))),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f41])).
% 49.28/6.80 fof(f43,plain,(
% 49.28/6.80 ![W0]: (~aElement0(W0)|(sdtasdt0(W0,sz10)=W0&W0=sdtasdt0(sz10,W0)))),
% 49.28/6.80 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 49.28/6.80 fof(f44,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sz10)=X0)),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f43])).
% 49.28/6.80 fof(f45,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|X0=sdtasdt0(sz10,X0))),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f43])).
% 49.28/6.80 fof(f46,plain,(
% 49.28/6.80 ![W0,W1,W2]: (((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|(sdtasdt0(W0,sdtpldt0(W1,W2))=sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))&sdtasdt0(sdtpldt0(W1,W2),W0)=sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0))))),
% 49.28/6.80 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 49.28/6.80 fof(f47,plain,(
% 49.28/6.80 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sdtasdt0(X0,sdtpldt0(X1,X2))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)))),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f46])).
% 49.28/6.80 fof(f49,plain,(
% 49.28/6.80 aElement0(xx)),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f15])).
% 49.28/6.80 fof(f50,plain,(
% 49.28/6.80 ~sdtasdt0(smndt0(sz10),xx)=smndt0(xx)),
% 49.28/6.80 inference(cnf_transformation,[status(thm)],[f17])).
% 49.28/6.80 fof(f51,plain,(
% 49.28/6.80 aElement0(smndt0(sz10))),
% 49.28/6.80 inference(resolution,[status(thm)],[f24,f22])).
% 49.28/6.80 fof(f56,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|aElement0(sdtasdt0(sz00,X0)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f28,f21])).
% 49.28/6.80 fof(f63,plain,(
% 49.28/6.80 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,X1),sz10)=sdtpldt0(X0,sdtpldt0(X1,sz10)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f32,f22])).
% 49.28/6.80 fof(f65,plain,(
% 49.28/6.80 sdtpldt0(sz10,sz00)=sz10),
% 49.28/6.80 inference(resolution,[status(thm)],[f34,f22])).
% 49.28/6.80 fof(f70,plain,(
% 49.28/6.80 sdtpldt0(sz10,smndt0(sz10))=sz00),
% 49.28/6.80 inference(resolution,[status(thm)],[f37,f22])).
% 49.28/6.80 fof(f72,plain,(
% 49.28/6.80 sz00=sdtpldt0(smndt0(sz10),sz10)),
% 49.28/6.80 inference(resolution,[status(thm)],[f38,f22])).
% 49.28/6.80 fof(f74,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sz10)=sdtasdt0(sz10,X0))),
% 49.28/6.80 inference(resolution,[status(thm)],[f40,f22])).
% 49.28/6.80 fof(f75,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sz00)=sdtasdt0(sz00,X0))),
% 49.28/6.80 inference(resolution,[status(thm)],[f40,f21])).
% 49.28/6.80 fof(f78,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(sdtasdt0(X0,sz00),sz00)=sdtasdt0(X0,sdtasdt0(sz00,sz00)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f42,f21])).
% 49.28/6.80 fof(f83,plain,(
% 49.28/6.80 sdtasdt0(sz00,sz10)=sz00),
% 49.28/6.80 inference(resolution,[status(thm)],[f44,f21])).
% 49.28/6.80 fof(f86,plain,(
% 49.28/6.80 sz00=sdtasdt0(sz10,sz00)),
% 49.28/6.80 inference(resolution,[status(thm)],[f45,f21])).
% 49.28/6.80 fof(f88,plain,(
% 49.28/6.80 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtasdt0(X0,sdtpldt0(sz10,X1))=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,X1)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f47,f22])).
% 49.28/6.80 fof(f91,plain,(
% 49.28/6.80 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtasdt0(X0,sdtpldt0(X1,sz10))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,sz10)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f47,f22])).
% 49.28/6.80 fof(f92,plain,(
% 49.28/6.80 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtasdt0(X0,sdtpldt0(X1,sz00))=sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,sz00)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f47,f21])).
% 49.28/6.80 fof(f110,plain,(
% 49.28/6.80 sdtasdt0(xx,sz10)=xx),
% 49.28/6.80 inference(resolution,[status(thm)],[f49,f44])).
% 49.28/6.80 fof(f115,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,xx)=sdtasdt0(xx,X0))),
% 49.28/6.80 inference(resolution,[status(thm)],[f49,f40])).
% 49.28/6.80 fof(f117,plain,(
% 49.28/6.80 sdtpldt0(xx,smndt0(xx))=sz00),
% 49.28/6.80 inference(resolution,[status(thm)],[f49,f37])).
% 49.28/6.80 fof(f119,plain,(
% 49.28/6.80 sdtpldt0(xx,sz00)=xx),
% 49.28/6.80 inference(resolution,[status(thm)],[f49,f34])).
% 49.28/6.80 fof(f123,plain,(
% 49.28/6.80 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtpldt0(sdtpldt0(X0,xx),X1)=sdtpldt0(X0,sdtpldt0(xx,X1)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f49,f32])).
% 49.28/6.80 fof(f124,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtpldt0(X0,xx)=sdtpldt0(xx,X0))),
% 49.28/6.80 inference(resolution,[status(thm)],[f49,f30])).
% 49.28/6.80 fof(f125,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|aElement0(sdtasdt0(xx,X0)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f49,f28])).
% 49.28/6.80 fof(f127,plain,(
% 49.28/6.80 aElement0(smndt0(xx))),
% 49.28/6.80 inference(resolution,[status(thm)],[f49,f24])).
% 49.28/6.80 fof(f137,plain,(
% 49.28/6.80 sdtasdt0(smndt0(sz10),sz10)=smndt0(sz10)),
% 49.28/6.80 inference(resolution,[status(thm)],[f51,f44])).
% 49.28/6.80 fof(f142,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,smndt0(sz10))=sdtasdt0(smndt0(sz10),X0))),
% 49.28/6.80 inference(resolution,[status(thm)],[f51,f40])).
% 49.28/6.80 fof(f151,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtpldt0(X0,smndt0(sz10))=sdtpldt0(smndt0(sz10),X0))),
% 49.28/6.80 inference(resolution,[status(thm)],[f51,f30])).
% 49.28/6.80 fof(f270,plain,(
% 49.28/6.80 aElement0(sdtasdt0(sz00,smndt0(sz10)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f56,f51])).
% 49.28/6.80 fof(f271,plain,(
% 49.28/6.80 aElement0(sdtasdt0(sz00,xx))),
% 49.28/6.80 inference(resolution,[status(thm)],[f56,f49])).
% 49.28/6.80 fof(f273,plain,(
% 49.28/6.80 aElement0(sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(resolution,[status(thm)],[f56,f21])).
% 49.28/6.80 fof(f304,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,smndt0(sz10)),sz10)=sdtpldt0(X0,sdtpldt0(smndt0(sz10),sz10)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f63,f51])).
% 49.28/6.80 fof(f308,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,smndt0(sz10)),sz10)=sdtpldt0(X0,sz00))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f72,f304])).
% 49.28/6.80 fof(f329,plain,(
% 49.28/6.80 sdtasdt0(smndt0(sz10),sz00)=sdtasdt0(sz00,smndt0(sz10))),
% 49.28/6.80 inference(resolution,[status(thm)],[f75,f51])).
% 49.28/6.80 fof(f330,plain,(
% 49.28/6.80 sdtasdt0(xx,sz00)=sdtasdt0(sz00,xx)),
% 49.28/6.80 inference(resolution,[status(thm)],[f75,f49])).
% 49.28/6.80 fof(f333,plain,(
% 49.28/6.80 aElement0(sdtasdt0(xx,sz00))),
% 49.28/6.80 inference(backward_demodulation,[status(thm)],[f330,f271])).
% 49.28/6.80 fof(f343,plain,(
% 49.28/6.80 sdtasdt0(sdtasdt0(smndt0(sz10),sz00),sz00)=sdtasdt0(smndt0(sz10),sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(resolution,[status(thm)],[f78,f51])).
% 49.28/6.80 fof(f345,plain,(
% 49.28/6.80 sdtasdt0(sdtasdt0(sz10,sz00),sz00)=sdtasdt0(sz10,sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(resolution,[status(thm)],[f78,f22])).
% 49.28/6.80 fof(f346,plain,(
% 49.28/6.80 sdtasdt0(sdtasdt0(sz00,sz00),sz00)=sdtasdt0(sz00,sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(resolution,[status(thm)],[f78,f21])).
% 49.28/6.80 fof(f347,plain,(
% 49.28/6.80 sdtasdt0(sdtasdt0(sz00,smndt0(sz10)),sz00)=sdtasdt0(smndt0(sz10),sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f329,f343])).
% 49.28/6.80 fof(f348,plain,(
% 49.28/6.80 sdtasdt0(sz00,sz00)=sdtasdt0(sz10,sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f86,f345])).
% 49.28/6.80 fof(f386,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sdtpldt0(sz10,smndt0(sz10)))=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,smndt0(sz10))))),
% 49.28/6.80 inference(resolution,[status(thm)],[f88,f51])).
% 49.28/6.80 fof(f389,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sdtpldt0(sz10,sz00))=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,sz00)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f88,f21])).
% 49.28/6.80 fof(f390,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sz00)=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,smndt0(sz10))))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f70,f386])).
% 49.28/6.80 fof(f392,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sz10)=sdtpldt0(sdtasdt0(X0,sz10),sdtasdt0(X0,sz00)))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f65,f389])).
% 49.28/6.80 fof(f411,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sdtpldt0(smndt0(sz10),sz10))=sdtpldt0(sdtasdt0(X0,smndt0(sz10)),sdtasdt0(X0,sz10)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f91,f51])).
% 49.28/6.80 fof(f415,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sz00)=sdtpldt0(sdtasdt0(X0,smndt0(sz10)),sdtasdt0(X0,sz10)))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f72,f411])).
% 49.28/6.80 fof(f431,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,sdtpldt0(xx,sz00))=sdtpldt0(sdtasdt0(X0,xx),sdtasdt0(X0,sz00)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f92,f49])).
% 49.28/6.80 fof(f435,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtasdt0(X0,xx)=sdtpldt0(sdtasdt0(X0,xx),sdtasdt0(X0,sz00)))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f119,f431])).
% 49.28/6.80 fof(f533,plain,(
% 49.28/6.80 sdtasdt0(smndt0(sz10),xx)=sdtasdt0(xx,smndt0(sz10))),
% 49.28/6.80 inference(resolution,[status(thm)],[f115,f51])).
% 49.28/6.80 fof(f537,plain,(
% 49.28/6.80 ~sdtasdt0(xx,smndt0(sz10))=smndt0(xx)),
% 49.28/6.80 inference(backward_demodulation,[status(thm)],[f533,f50])).
% 49.28/6.80 fof(f570,plain,(
% 49.28/6.80 aElement0(sdtasdt0(xx,smndt0(sz10)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f125,f51])).
% 49.28/6.80 fof(f583,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xx),smndt0(xx))=sdtpldt0(X0,sdtpldt0(xx,smndt0(xx))))),
% 49.28/6.80 inference(resolution,[status(thm)],[f127,f123])).
% 49.28/6.80 fof(f645,plain,(
% 49.28/6.80 smndt0(xx)=sdtpldt0(sz00,smndt0(xx))),
% 49.28/6.80 inference(resolution,[status(thm)],[f127,f35])).
% 49.28/6.80 fof(f657,plain,(
% 49.28/6.80 ![X0]: (~aElement0(X0)|sdtpldt0(sdtpldt0(X0,xx),smndt0(xx))=sdtpldt0(X0,sz00))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f117,f583])).
% 49.28/6.80 fof(f1353,plain,(
% 49.28/6.80 sdtasdt0(sdtasdt0(sz00,smndt0(sz10)),sz00)=sdtasdt0(sz00,sdtasdt0(sz00,smndt0(sz10)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f270,f75])).
% 49.28/6.80 fof(f1384,plain,(
% 49.28/6.80 sdtasdt0(sz00,smndt0(sz10))=sdtpldt0(sz00,sdtasdt0(sz00,smndt0(sz10)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f270,f35])).
% 49.28/6.80 fof(f1422,plain,(
% 49.28/6.80 sdtasdt0(sz00,sdtasdt0(sz00,smndt0(sz10)))=sdtasdt0(smndt0(sz10),sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(backward_demodulation,[status(thm)],[f1353,f347])).
% 49.28/6.80 fof(f1471,plain,(
% 49.28/6.80 sdtpldt0(sdtasdt0(sz00,sz00),smndt0(sz10))=sdtpldt0(smndt0(sz10),sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(resolution,[status(thm)],[f273,f151])).
% 49.28/6.80 fof(f1473,plain,(
% 49.28/6.80 sdtasdt0(sdtasdt0(sz00,sz00),smndt0(sz10))=sdtasdt0(smndt0(sz10),sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(resolution,[status(thm)],[f273,f142])).
% 49.28/6.80 fof(f1518,plain,(
% 49.28/6.80 sdtasdt0(sdtasdt0(sz00,sz00),sz10)=sdtasdt0(sz10,sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(resolution,[status(thm)],[f273,f74])).
% 49.28/6.80 fof(f1549,plain,(
% 49.28/6.80 sdtpldt0(sdtasdt0(sz00,sz00),sz00)=sdtasdt0(sz00,sz00)),
% 49.28/6.80 inference(resolution,[status(thm)],[f273,f34])).
% 49.28/6.80 fof(f1561,plain,(
% 49.28/6.80 sdtasdt0(sdtasdt0(sz00,sz00),smndt0(sz10))=sdtasdt0(sz00,sdtasdt0(sz00,smndt0(sz10)))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f1422,f1473])).
% 49.28/6.80 fof(f1594,plain,(
% 49.28/6.80 sdtasdt0(sdtasdt0(sz00,sz00),sz10)=sdtasdt0(sz00,sz00)),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f348,f1518])).
% 49.28/6.80 fof(f1708,plain,(
% 49.28/6.80 sdtpldt0(sdtpldt0(sdtasdt0(sz00,sz00),smndt0(sz10)),sz10)=sdtpldt0(sdtasdt0(sz00,sz00),sz00)),
% 49.28/6.80 inference(resolution,[status(thm)],[f308,f273])).
% 49.28/6.80 fof(f1718,plain,(
% 49.28/6.80 sdtpldt0(sdtpldt0(smndt0(sz10),sdtasdt0(sz00,sz00)),sz10)=sdtpldt0(sdtasdt0(sz00,sz00),sz00)),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f1471,f1708])).
% 49.28/6.80 fof(f1719,plain,(
% 49.28/6.80 sdtpldt0(sdtpldt0(smndt0(sz10),sdtasdt0(sz00,sz00)),sz10)=sdtasdt0(sz00,sz00)),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f1549,f1718])).
% 49.28/6.80 fof(f2091,plain,(
% 49.28/6.80 sdtpldt0(sdtasdt0(xx,sz00),xx)=sdtpldt0(xx,sdtasdt0(xx,sz00))),
% 49.28/6.80 inference(resolution,[status(thm)],[f333,f124])).
% 49.28/6.80 fof(f2155,plain,(
% 49.28/6.80 sdtpldt0(sdtasdt0(xx,sz00),sz00)=sdtasdt0(xx,sz00)),
% 49.28/6.80 inference(resolution,[status(thm)],[f333,f34])).
% 49.28/6.80 fof(f2387,plain,(
% 49.28/6.80 sdtasdt0(sdtasdt0(sz00,sz00),sz00)=sdtpldt0(sdtasdt0(sdtasdt0(sz00,sz00),sz10),sdtasdt0(sdtasdt0(sz00,sz00),smndt0(sz10)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f390,f273])).
% 49.28/6.80 fof(f2395,plain,(
% 49.28/6.80 sdtasdt0(sz00,sz00)=sdtpldt0(sdtasdt0(sz00,sz10),sdtasdt0(sz00,smndt0(sz10)))),
% 49.28/6.80 inference(resolution,[status(thm)],[f390,f21])).
% 49.28/6.80 fof(f2399,plain,(
% 49.28/6.80 sdtasdt0(sz00,sdtasdt0(sz00,sz00))=sdtpldt0(sdtasdt0(sdtasdt0(sz00,sz00),sz10),sdtasdt0(sdtasdt0(sz00,sz00),smndt0(sz10)))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f346,f2387])).
% 49.28/6.80 fof(f2400,plain,(
% 49.28/6.80 sdtasdt0(sz00,sdtasdt0(sz00,sz00))=sdtpldt0(sdtasdt0(sz00,sz00),sdtasdt0(sdtasdt0(sz00,sz00),smndt0(sz10)))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f1594,f2399])).
% 49.28/6.80 fof(f2401,plain,(
% 49.28/6.80 sdtasdt0(sz00,sdtasdt0(sz00,sz00))=sdtpldt0(sdtasdt0(sz00,sz00),sdtasdt0(sz00,sdtasdt0(sz00,smndt0(sz10))))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f1561,f2400])).
% 49.28/6.80 fof(f2419,plain,(
% 49.28/6.80 sdtasdt0(sz00,smndt0(sz10))=sdtasdt0(sz00,sz00)),
% 49.28/6.80 inference(backward_demodulation,[status(thm)],[f2420,f1384])).
% 49.28/6.80 fof(f2420,plain,(
% 49.28/6.80 sdtasdt0(sz00,sz00)=sdtpldt0(sz00,sdtasdt0(sz00,smndt0(sz10)))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f83,f2395])).
% 49.28/6.80 fof(f2423,plain,(
% 49.28/6.80 sdtasdt0(smndt0(sz10),sz00)=sdtasdt0(sz00,sz00)),
% 49.28/6.80 inference(backward_demodulation,[status(thm)],[f2419,f329])).
% 49.28/6.80 fof(f2428,plain,(
% 49.28/6.80 sdtasdt0(sz00,sdtasdt0(sz00,sz00))=sdtpldt0(sdtasdt0(sz00,sz00),sdtasdt0(sz00,sdtasdt0(sz00,sz00)))),
% 49.28/6.80 inference(backward_demodulation,[status(thm)],[f2419,f2401])).
% 49.28/6.80 fof(f2480,plain,(
% 49.28/6.80 sdtasdt0(sz00,sdtasdt0(sz00,sz00))=sdtasdt0(smndt0(sz10),sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(backward_demodulation,[status(thm)],[f2419,f1422])).
% 49.28/6.80 fof(f2739,plain,(
% 49.28/6.80 sdtasdt0(sdtasdt0(sz00,sz00),sz10)=sdtpldt0(sdtasdt0(sdtasdt0(sz00,sz00),sz10),sdtasdt0(sdtasdt0(sz00,sz00),sz00))),
% 49.28/6.80 inference(resolution,[status(thm)],[f392,f273])).
% 49.28/6.80 fof(f2743,plain,(
% 49.28/6.80 sdtasdt0(smndt0(sz10),sz10)=sdtpldt0(sdtasdt0(smndt0(sz10),sz10),sdtasdt0(smndt0(sz10),sz00))),
% 49.28/6.80 inference(resolution,[status(thm)],[f392,f51])).
% 49.28/6.80 fof(f2744,plain,(
% 49.28/6.80 sdtasdt0(xx,sz10)=sdtpldt0(sdtasdt0(xx,sz10),sdtasdt0(xx,sz00))),
% 49.28/6.80 inference(resolution,[status(thm)],[f392,f49])).
% 49.28/6.80 fof(f2751,plain,(
% 49.28/6.80 sdtasdt0(sz00,sz00)=sdtpldt0(sdtasdt0(sdtasdt0(sz00,sz00),sz10),sdtasdt0(sdtasdt0(sz00,sz00),sz00))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f1594,f2739])).
% 49.28/6.80 fof(f2752,plain,(
% 49.28/6.80 sdtasdt0(sz00,sz00)=sdtpldt0(sdtasdt0(sz00,sz00),sdtasdt0(sdtasdt0(sz00,sz00),sz00))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f1594,f2751])).
% 49.28/6.80 fof(f2753,plain,(
% 49.28/6.80 sdtasdt0(sz00,sdtasdt0(sz00,sz00))=sdtasdt0(sz00,sz00)),
% 49.28/6.80 inference(backward_demodulation,[status(thm)],[f2754,f2428])).
% 49.28/6.80 fof(f2754,plain,(
% 49.28/6.80 sdtasdt0(sz00,sz00)=sdtpldt0(sdtasdt0(sz00,sz00),sdtasdt0(sz00,sdtasdt0(sz00,sz00)))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f346,f2752])).
% 49.28/6.80 fof(f2764,plain,(
% 49.28/6.80 smndt0(sz10)=sdtpldt0(sdtasdt0(smndt0(sz10),sz10),sdtasdt0(smndt0(sz10),sz00))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f137,f2743])).
% 49.28/6.80 fof(f2765,plain,(
% 49.28/6.80 smndt0(sz10)=sdtpldt0(smndt0(sz10),sdtasdt0(smndt0(sz10),sz00))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f137,f2764])).
% 49.28/6.80 fof(f2767,plain,(
% 49.28/6.80 sdtpldt0(smndt0(sz10),sz10)=sdtasdt0(sz00,sz00)),
% 49.28/6.80 inference(backward_demodulation,[status(thm)],[f2777,f1719])).
% 49.28/6.80 fof(f2777,plain,(
% 49.28/6.80 smndt0(sz10)=sdtpldt0(smndt0(sz10),sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f2423,f2765])).
% 49.28/6.80 fof(f2778,plain,(
% 49.28/6.80 xx=sdtpldt0(sdtasdt0(xx,sz10),sdtasdt0(xx,sz00))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f110,f2744])).
% 49.28/6.80 fof(f2788,plain,(
% 49.28/6.80 sdtpldt0(sdtasdt0(xx,sz00),xx)=xx),
% 49.28/6.80 inference(backward_demodulation,[status(thm)],[f2790,f2091])).
% 49.28/6.80 fof(f2790,plain,(
% 49.28/6.80 xx=sdtpldt0(xx,sdtasdt0(xx,sz00))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f110,f2778])).
% 49.28/6.80 fof(f2828,plain,(
% 49.28/6.80 sdtasdt0(sz00,sz00)=sdtasdt0(smndt0(sz10),sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(backward_demodulation,[status(thm)],[f2753,f2480])).
% 49.28/6.80 fof(f2918,plain,(
% 49.28/6.80 sz00=sdtasdt0(sz00,sz00)),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f72,f2767])).
% 49.28/6.80 fof(f2958,plain,(
% 49.28/6.80 sz00=sdtasdt0(smndt0(sz10),sdtasdt0(sz00,sz00))),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f2918,f2828])).
% 49.28/6.80 fof(f2959,plain,(
% 49.28/6.80 sz00=sdtasdt0(smndt0(sz10),sz00)),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f2918,f2958])).
% 49.28/6.80 fof(f3181,plain,(
% 49.28/6.80 sdtasdt0(xx,sz00)=sdtpldt0(sdtasdt0(xx,smndt0(sz10)),sdtasdt0(xx,sz10))),
% 49.28/6.80 inference(resolution,[status(thm)],[f415,f49])).
% 49.28/6.80 fof(f3197,plain,(
% 49.28/6.80 sdtasdt0(xx,sz00)=sdtpldt0(sdtasdt0(xx,smndt0(sz10)),xx)),
% 49.28/6.80 inference(forward_demodulation,[status(thm)],[f110,f3181])).
% 49.28/6.80 fof(f3268,plain,(
% 49.28/6.80 sdtasdt0(smndt0(sz10),xx)=sdtpldt0(sdtasdt0(smndt0(sz10),xx),sdtasdt0(smndt0(sz10),sz00))),
% 21.56/6.84 inference(resolution,[status(thm)],[f435,f51])).
% 21.56/6.84 fof(f3284,plain,(
% 21.56/6.84 sdtasdt0(xx,smndt0(sz10))=sdtpldt0(sdtasdt0(smndt0(sz10),xx),sdtasdt0(smndt0(sz10),sz00))),
% 21.56/6.84 inference(forward_demodulation,[status(thm)],[f533,f3268])).
% 21.56/6.84 fof(f3285,plain,(
% 21.56/6.84 sdtasdt0(xx,smndt0(sz10))=sdtpldt0(sdtasdt0(xx,smndt0(sz10)),sdtasdt0(smndt0(sz10),sz00))),
% 21.56/6.84 inference(forward_demodulation,[status(thm)],[f533,f3284])).
% 21.56/6.84 fof(f3286,plain,(
% 21.56/6.84 sdtasdt0(xx,smndt0(sz10))=sdtpldt0(sdtasdt0(xx,smndt0(sz10)),sz00)),
% 21.56/6.84 inference(forward_demodulation,[status(thm)],[f2959,f3285])).
% 21.56/6.84 fof(f5195,plain,(
% 21.56/6.84 sdtpldt0(sdtpldt0(sdtasdt0(xx,smndt0(sz10)),xx),smndt0(xx))=sdtpldt0(sdtasdt0(xx,smndt0(sz10)),sz00)),
% 21.56/6.84 inference(resolution,[status(thm)],[f657,f570])).
% 21.56/6.84 fof(f5196,plain,(
% 21.56/6.84 sdtpldt0(sdtpldt0(sdtasdt0(xx,sz00),xx),smndt0(xx))=sdtpldt0(sdtasdt0(xx,sz00),sz00)),
% 21.56/6.84 inference(resolution,[status(thm)],[f657,f333])).
% 21.56/6.84 fof(f5210,plain,(
% 21.56/6.84 sdtpldt0(sdtasdt0(xx,sz00),smndt0(xx))=sdtpldt0(sdtasdt0(xx,smndt0(sz10)),sz00)),
% 21.56/6.84 inference(forward_demodulation,[status(thm)],[f3197,f5195])).
% 21.56/6.84 fof(f5211,plain,(
% 21.56/6.84 sdtpldt0(sdtasdt0(xx,sz00),smndt0(xx))=sdtasdt0(xx,smndt0(sz10))),
% 21.56/6.84 inference(forward_demodulation,[status(thm)],[f3286,f5210])).
% 21.56/6.84 fof(f5212,plain,(
% 21.56/6.84 sdtpldt0(xx,smndt0(xx))=sdtpldt0(sdtasdt0(xx,sz00),sz00)),
% 21.56/6.84 inference(forward_demodulation,[status(thm)],[f2788,f5196])).
% 21.56/6.84 fof(f5213,plain,(
% 21.56/6.84 sz00=sdtasdt0(xx,sz00)),
% 21.56/6.84 inference(backward_demodulation,[status(thm)],[f5214,f2155])).
% 21.56/6.84 fof(f5214,plain,(
% 21.56/6.84 sz00=sdtpldt0(sdtasdt0(xx,sz00),sz00)),
% 21.56/6.84 inference(forward_demodulation,[status(thm)],[f117,f5212])).
% 21.56/6.84 fof(f5240,plain,(
% 21.56/6.84 sdtpldt0(sz00,smndt0(xx))=sdtasdt0(xx,smndt0(sz10))),
% 21.56/6.84 inference(backward_demodulation,[status(thm)],[f5213,f5211])).
% 21.56/6.84 fof(f5420,plain,(
% 21.56/6.84 smndt0(xx)=sdtasdt0(xx,smndt0(sz10))),
% 21.56/6.84 inference(forward_demodulation,[status(thm)],[f645,f5240])).
% 21.56/6.84 fof(f5421,plain,(
% 21.56/6.84 $false),
% 21.56/6.84 inference(forward_subsumption_resolution,[status(thm)],[f5420,f537])).
% 21.56/6.84 % SZS output end CNFRefutation for theBenchmark.p
% 21.56/6.85 % Elapsed time: 6.403104 seconds
% 21.56/6.85 % CPU time: 50.204912 seconds
% 21.56/6.85 % Total memory used: 386.452 MB
% 21.56/6.85 % Net memory used: 358.387 MB
%------------------------------------------------------------------------------