%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM020+4 : 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 : n010.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 12:10:43 PM UTC 2026
% Result : Theorem 29.20s 14.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM020+4 : 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.11/10.39 % Computer : n010.cluster.edu
% 0.11/10.39 % Model : x86_64 x86_64
% 0.11/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/10.39 % Memory : 8046.5625MB
% 0.11/10.39 % OS : Linux 6.8.0-71-generic
% 0.11/10.39 % CPULimit : 300
% 0.11/10.39 % WCLimit : 300
% 0.11/10.39 % DateTime : Mon Sep 21 14:15:05 UTC 2026
% 0.11/10.39 % CPUTime :
% 0.16/10.40 % Drodi V4.1.1
% 29.20/14.14 % Refutation found
% 29.20/14.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 29.20/14.14 % SZS output start CNFRefutation for theBenchmark
% 29.20/14.14 fof(f3,axiom,(
% 29.20/14.14 (! [W0,W1] :( ( aElement0(W0)& aRewritingSystem0(W1) )=> (! [W2] :( aReductOfIn0(W2,W0,W1)=> aElement0(W2) ) )) )),
% 29.20/14.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.20/14.14 fof(f8,definition,(
% 29.20/14.14 (! [W0,W1,W2] :( ( aElement0(W0)& aRewritingSystem0(W1)& aElement0(W2) )=> ( sdtmndtasgtdt0(W0,W1,W2)<=> ( W0 = W2| sdtmndtplgtdt0(W0,W1,W2) ) ) ) )),
% 29.20/14.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.20/14.14 fof(f9,axiom,(
% 29.20/14.14 (! [W0,W1,W2,W3] :( ( aElement0(W0)& aRewritingSystem0(W1)& aElement0(W2)& aElement0(W3) )=> ( ( sdtmndtasgtdt0(W0,W1,W2)& sdtmndtasgtdt0(W2,W1,W3) )=> sdtmndtasgtdt0(W0,W1,W3) ) ) )),
% 29.20/14.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.20/14.14 fof(f15,hypothesis,(
% 29.20/14.14 aRewritingSystem0(xR) ),
% 29.20/14.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.20/14.14 fof(f16,hypothesis,(
% 29.20/14.14 ( (! [W0,W1,W2] :( ( aElement0(W0)& aElement0(W1)& aElement0(W2)& aReductOfIn0(W1,W0,xR)& aReductOfIn0(W2,W0,xR) )=> (? [W3] :( aElement0(W3)& ( W1 = W3| ( ( aReductOfIn0(W3,W1,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,W1,xR)& sdtmndtplgtdt0(W4,xR,W3) ) ))& sdtmndtplgtdt0(W1,xR,W3) ) )& sdtmndtasgtdt0(W1,xR,W3)& ( W2 = W3| ( ( aReductOfIn0(W3,W2,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,W2,xR)& sdtmndtplgtdt0(W4,xR,W3) ) ))& sdtmndtplgtdt0(W2,xR,W3) ) )& sdtmndtasgtdt0(W2,xR,W3) ) )))& isLocallyConfluent0(xR)& (! [W0,W1] :( ( aElement0(W0)& aElement0(W1) )=> ( ( aReductOfIn0(W1,W0,xR)| (? [W2] :( aElement0(W2)& aReductOfIn0(W2,W0,xR)& sdtmndtplgtdt0(W2,xR,W1) ))| sdtmndtplgtdt0(W0,xR,W1) )=> iLess0(W1,W0) ) ))& isTerminating0(xR) ) ),
% 29.20/14.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.20/14.14 fof(f17,hypothesis,(
% 29.20/14.14 ( aElement0(xa)& aElement0(xb)& aElement0(xc) ) ),
% 29.20/14.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.20/14.14 fof(f18,hypothesis,(
% 29.20/14.14 (! [W0,W1,W2] :( ( aElement0(W0)& aElement0(W1)& aElement0(W2)& ( W0 = W1| aReductOfIn0(W1,W0,xR)| (? [W3] :( aElement0(W3)& aReductOfIn0(W3,W0,xR)& sdtmndtplgtdt0(W3,xR,W1) ))| sdtmndtplgtdt0(W0,xR,W1)| sdtmndtasgtdt0(W0,xR,W1) )& ( W0 = W2| aReductOfIn0(W2,W0,xR)| (? [W3] :( aElement0(W3)& aReductOfIn0(W3,W0,xR)& sdtmndtplgtdt0(W3,xR,W2) ))| sdtmndtplgtdt0(W0,xR,W2)| sdtmndtasgtdt0(W0,xR,W2) ) )=> ( iLess0(W0,xa)=> (? [W3] :( aElement0(W3)& ( W1 = W3| ( ( aReductOfIn0(W3,W1,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,W1,xR)& sdtmndtplgtdt0(W4,xR,W3) ) ))& sdtmndtplgtdt0(W1,xR,W3) ) )& sdtmndtasgtdt0(W1,xR,W3)& ( W2 = W3| ( ( aReductOfIn0(W3,W2,xR)| (? [W4] :( aElement0(W4)& aReductOfIn0(W4,W2,xR)& sdtmndtplgtdt0(W4,xR,W3) ) ))& sdtmndtplgtdt0(W2,xR,W3) ) )& sdtmndtasgtdt0(W2,xR,W3) ) )) ) )),
% 29.20/14.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.20/14.14 fof(f19,hypothesis,(
% 29.20/14.14 ( ( aReductOfIn0(xb,xa,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtplgtdt0(W0,xR,xb) ) ))& sdtmndtplgtdt0(xa,xR,xb)& ( aReductOfIn0(xc,xa,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtplgtdt0(W0,xR,xc) ) ))& sdtmndtplgtdt0(xa,xR,xc) ) ),
% 29.20/14.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.20/14.14 fof(f20,hypothesis,(
% 29.20/14.14 ( aElement0(xu)& aReductOfIn0(xu,xa,xR)& ( xu = xb| ( ( aReductOfIn0(xb,xu,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xu,xR)& sdtmndtplgtdt0(W0,xR,xb) ) ))& sdtmndtplgtdt0(xu,xR,xb) ) )& sdtmndtasgtdt0(xu,xR,xb) ) ),
% 29.20/14.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.20/14.14 fof(f22,hypothesis,(
% 29.20/14.14 ( aElement0(xw)& ( xu = xw| ( ( aReductOfIn0(xw,xu,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xu,xR)& sdtmndtplgtdt0(W0,xR,xw) ) ))& sdtmndtplgtdt0(xu,xR,xw) ) )& sdtmndtasgtdt0(xu,xR,xw)& ( xv = xw| ( ( aReductOfIn0(xw,xv,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xv,xR)& sdtmndtplgtdt0(W0,xR,xw) ) ))& sdtmndtplgtdt0(xv,xR,xw) ) )& sdtmndtasgtdt0(xv,xR,xw) ) ),
% 29.20/14.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.20/14.14 fof(f23,hypothesis,(
% 29.20/14.14 ( aElement0(xd)& ( xw = xd| ( ( aReductOfIn0(xd,xw,xR)| (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xw,xR)& sdtmndtplgtdt0(W0,xR,xd) ) ))& sdtmndtplgtdt0(xw,xR,xd) ) )& sdtmndtasgtdt0(xw,xR,xd)& ~ (? [W0] : aReductOfIn0(W0,xd,xR))& aNormalFormOfIn0(xd,xw,xR) ) ),
% 29.20/14.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.20/14.14 fof(f24,conjecture,(
% 29.20/14.14 (? [W0] :( aElement0(W0)& ( xb = W0| aReductOfIn0(W0,xb,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xb,xR)& sdtmndtplgtdt0(W1,xR,W0) ))| sdtmndtplgtdt0(xb,xR,W0)| sdtmndtasgtdt0(xb,xR,W0) )& ( xd = W0| aReductOfIn0(W0,xd,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xd,xR)& sdtmndtplgtdt0(W1,xR,W0) ))| sdtmndtplgtdt0(xd,xR,W0)| sdtmndtasgtdt0(xd,xR,W0) ) ) )),
% 29.20/14.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.20/14.14 fof(f25,negated_conjecture,(
% 29.20/14.14 ~((? [W0] :( aElement0(W0)& ( xb = W0| aReductOfIn0(W0,xb,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xb,xR)& sdtmndtplgtdt0(W1,xR,W0) ))| sdtmndtplgtdt0(xb,xR,W0)| sdtmndtasgtdt0(xb,xR,W0) )& ( xd = W0| aReductOfIn0(W0,xd,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xd,xR)& sdtmndtplgtdt0(W1,xR,W0) ))| sdtmndtplgtdt0(xd,xR,W0)| sdtmndtasgtdt0(xd,xR,W0) ) ) ))),
% 29.20/14.14 inference(negated_conjecture,[status(cth)],[f24])).
% 29.20/14.14 fof(f32,plain,(
% 29.20/14.14 ![W0,W1]: ((~aElement0(W0)|~aRewritingSystem0(W1))|(![W2]: (~aReductOfIn0(W2,W0,W1)|aElement0(W2))))),
% 29.20/14.14 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 29.20/14.14 fof(f33,plain,(
% 29.20/14.14 ![X0,X1,X2]: (~aElement0(X0)|~aRewritingSystem0(X1)|~aReductOfIn0(X2,X0,X1)|aElement0(X2))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f32])).
% 29.20/14.14 fof(f48,plain,(
% 29.20/14.14 ![W0,W1,W2]: (((~aElement0(W0)|~aRewritingSystem0(W1))|~aElement0(W2))|(sdtmndtasgtdt0(W0,W1,W2)<=>(W0=W2|sdtmndtplgtdt0(W0,W1,W2))))),
% 29.20/14.14 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 29.20/14.14 fof(f49,plain,(
% 29.20/14.14 ![W0,W1,W2]: (((~aElement0(W0)|~aRewritingSystem0(W1))|~aElement0(W2))|((~sdtmndtasgtdt0(W0,W1,W2)|(W0=W2|sdtmndtplgtdt0(W0,W1,W2)))&(sdtmndtasgtdt0(W0,W1,W2)|(~W0=W2&~sdtmndtplgtdt0(W0,W1,W2)))))),
% 29.20/14.14 inference(NNF_transformation,[status(thm)],[f48])).
% 29.20/14.14 fof(f50,plain,(
% 29.20/14.14 ![X0,X1,X2]: (~aElement0(X0)|~aRewritingSystem0(X1)|~aElement0(X2)|~sdtmndtasgtdt0(X0,X1,X2)|X0=X2|sdtmndtplgtdt0(X0,X1,X2))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f49])).
% 29.20/14.14 fof(f52,plain,(
% 29.20/14.14 ![X0,X1,X2]: (~aElement0(X0)|~aRewritingSystem0(X1)|~aElement0(X2)|sdtmndtasgtdt0(X0,X1,X2)|~sdtmndtplgtdt0(X0,X1,X2))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f49])).
% 29.20/14.14 fof(f53,plain,(
% 29.20/14.14 ![W0,W1,W2,W3]: ((((~aElement0(W0)|~aRewritingSystem0(W1))|~aElement0(W2))|~aElement0(W3))|((~sdtmndtasgtdt0(W0,W1,W2)|~sdtmndtasgtdt0(W2,W1,W3))|sdtmndtasgtdt0(W0,W1,W3)))),
% 29.20/14.14 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 29.20/14.14 fof(f54,plain,(
% 29.20/14.14 ![X0,X1,X2,X3]: (~aElement0(X0)|~aRewritingSystem0(X1)|~aElement0(X2)|~aElement0(X3)|~sdtmndtasgtdt0(X0,X1,X2)|~sdtmndtasgtdt0(X2,X1,X3)|sdtmndtasgtdt0(X0,X1,X3))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f53])).
% 29.20/14.14 fof(f100,plain,(
% 29.20/14.14 aRewritingSystem0(xR)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f15])).
% 29.20/14.14 fof(f101,plain,(
% 29.20/14.14 (((![W0,W1,W2]: (((((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|~aReductOfIn0(W1,W0,xR))|~aReductOfIn0(W2,W0,xR))|(?[W3]: ((((aElement0(W3)&(W1=W3|((aReductOfIn0(W3,W1,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W1,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W1,xR,W3))))&sdtmndtasgtdt0(W1,xR,W3))&(W2=W3|((aReductOfIn0(W3,W2,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W2,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W2,xR,W3))))&sdtmndtasgtdt0(W2,xR,W3)))))&isLocallyConfluent0(xR))&(![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|(((~aReductOfIn0(W1,W0,xR)&(![W2]: ((~aElement0(W2)|~aReductOfIn0(W2,W0,xR))|~sdtmndtplgtdt0(W2,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))|iLess0(W1,W0)))))&isTerminating0(xR)),
% 29.20/14.14 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 29.20/14.14 fof(f102,plain,(
% 29.20/14.14 (((![W1,W2]: ((![W0]: ((((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|~aReductOfIn0(W1,W0,xR))|~aReductOfIn0(W2,W0,xR)))|(?[W3]: ((((aElement0(W3)&(W1=W3|((aReductOfIn0(W3,W1,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W1,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W1,xR,W3))))&sdtmndtasgtdt0(W1,xR,W3))&(W2=W3|((aReductOfIn0(W3,W2,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W2,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W2,xR,W3))))&sdtmndtasgtdt0(W2,xR,W3)))))&isLocallyConfluent0(xR))&(![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|(((~aReductOfIn0(W1,W0,xR)&(![W2]: ((~aElement0(W2)|~aReductOfIn0(W2,W0,xR))|~sdtmndtplgtdt0(W2,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))|iLess0(W1,W0)))))&isTerminating0(xR)),
% 29.20/14.14 inference(miniscoping,[status(thm)],[f101])).
% 29.20/14.14 fof(f103,plain,(
% 29.20/14.14 (((![W1,W2]: ((![W0]: ((((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|~aReductOfIn0(W1,W0,xR))|~aReductOfIn0(W2,W0,xR)))|((((aElement0(sK13_skl(W2,W1))&(W1=sK13_skl(W2,W1)|((aReductOfIn0(sK13_skl(W2,W1),W1,xR)|((aElement0(sK14_skl(W2,W1))&aReductOfIn0(sK14_skl(W2,W1),W1,xR))&sdtmndtplgtdt0(sK14_skl(W2,W1),xR,sK13_skl(W2,W1))))&sdtmndtplgtdt0(W1,xR,sK13_skl(W2,W1)))))&sdtmndtasgtdt0(W1,xR,sK13_skl(W2,W1)))&(W2=sK13_skl(W2,W1)|((aReductOfIn0(sK13_skl(W2,W1),W2,xR)|((aElement0(sK15_skl(W2,W1))&aReductOfIn0(sK15_skl(W2,W1),W2,xR))&sdtmndtplgtdt0(sK15_skl(W2,W1),xR,sK13_skl(W2,W1))))&sdtmndtplgtdt0(W2,xR,sK13_skl(W2,W1)))))&sdtmndtasgtdt0(W2,xR,sK13_skl(W2,W1)))))&isLocallyConfluent0(xR))&(![W0,W1]: ((~aElement0(W0)|~aElement0(W1))|(((~aReductOfIn0(W1,W0,xR)&(![W2]: ((~aElement0(W2)|~aReductOfIn0(W2,W0,xR))|~sdtmndtplgtdt0(W2,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))|iLess0(W1,W0)))))&isTerminating0(xR)),
% 29.20/14.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(W3,sK13_skl(W2,W1)),skolemize(W4,sK14_skl(W2,W1)),skolemize(W4,sK15_skl(W2,W1))],[f102])).
% 29.20/14.14 fof(f116,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|~aReductOfIn0(X1,X0,xR)|iLess0(X1,X0))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f103])).
% 29.20/14.14 fof(f118,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|~sdtmndtplgtdt0(X0,xR,X1)|iLess0(X1,X0))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f103])).
% 29.20/14.14 fof(f120,plain,(
% 29.20/14.14 aElement0(xa)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f17])).
% 29.20/14.14 fof(f121,plain,(
% 29.20/14.14 aElement0(xb)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f17])).
% 29.20/14.14 fof(f123,plain,(
% 29.20/14.14 ![W0,W1,W2]: (((((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|((((~W0=W1&~aReductOfIn0(W1,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))&~sdtmndtasgtdt0(W0,xR,W1)))|((((~W0=W2&~aReductOfIn0(W2,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W2))))&~sdtmndtplgtdt0(W0,xR,W2))&~sdtmndtasgtdt0(W0,xR,W2)))|(~iLess0(W0,xa)|(?[W3]: ((((aElement0(W3)&(W1=W3|((aReductOfIn0(W3,W1,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W1,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W1,xR,W3))))&sdtmndtasgtdt0(W1,xR,W3))&(W2=W3|((aReductOfIn0(W3,W2,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W2,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W2,xR,W3))))&sdtmndtasgtdt0(W2,xR,W3)))))),
% 29.20/14.14 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 29.20/14.14 fof(f124,definition,(
% 29.20/14.14 ![W0,W1]: (sP0_prd(W1,W0)<=>((((~W0=W1&~aReductOfIn0(W1,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))&~sdtmndtasgtdt0(W0,xR,W1)))),
% 29.20/14.14 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 29.20/14.14 fof(f125,plain,(
% 29.20/14.14 ![W0,W1,W2]: (((((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|sP0_prd(W1,W0))|((((~W0=W2&~aReductOfIn0(W2,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W2))))&~sdtmndtplgtdt0(W0,xR,W2))&~sdtmndtasgtdt0(W0,xR,W2)))|(~iLess0(W0,xa)|(?[W3]: ((((aElement0(W3)&(W1=W3|((aReductOfIn0(W3,W1,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W1,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W1,xR,W3))))&sdtmndtasgtdt0(W1,xR,W3))&(W2=W3|((aReductOfIn0(W3,W2,xR)|(?[W4]: ((aElement0(W4)&aReductOfIn0(W4,W2,xR))&sdtmndtplgtdt0(W4,xR,W3))))&sdtmndtplgtdt0(W2,xR,W3))))&sdtmndtasgtdt0(W2,xR,W3)))))),
% 29.20/14.14 inference(formula_renaming,[status(thm)],[f123,f124])).
% 29.20/14.14 fof(f126,plain,(
% 29.20/14.14 ![W0,W1,W2]: (((((~aElement0(W0)|~aElement0(W1))|~aElement0(W2))|sP0_prd(W1,W0))|((((~W0=W2&~aReductOfIn0(W2,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W2))))&~sdtmndtplgtdt0(W0,xR,W2))&~sdtmndtasgtdt0(W0,xR,W2)))|(~iLess0(W0,xa)|((((aElement0(sK16_skl(W2,W1,W0))&(W1=sK16_skl(W2,W1,W0)|((aReductOfIn0(sK16_skl(W2,W1,W0),W1,xR)|((aElement0(sK17_skl(W2,W1,W0))&aReductOfIn0(sK17_skl(W2,W1,W0),W1,xR))&sdtmndtplgtdt0(sK17_skl(W2,W1,W0),xR,sK16_skl(W2,W1,W0))))&sdtmndtplgtdt0(W1,xR,sK16_skl(W2,W1,W0)))))&sdtmndtasgtdt0(W1,xR,sK16_skl(W2,W1,W0)))&(W2=sK16_skl(W2,W1,W0)|((aReductOfIn0(sK16_skl(W2,W1,W0),W2,xR)|((aElement0(sK18_skl(W2,W1,W0))&aReductOfIn0(sK18_skl(W2,W1,W0),W2,xR))&sdtmndtplgtdt0(sK18_skl(W2,W1,W0),xR,sK16_skl(W2,W1,W0))))&sdtmndtplgtdt0(W2,xR,sK16_skl(W2,W1,W0)))))&sdtmndtasgtdt0(W2,xR,sK16_skl(W2,W1,W0)))))),
% 29.20/14.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(W3,sK16_skl(W2,W1,W0)),skolemize(W4,sK17_skl(W2,W1,W0)),skolemize(W4,sK18_skl(W2,W1,W0))],[f125])).
% 29.20/14.14 fof(f127,plain,(
% 29.20/14.14 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X0)|~X0=X2|~iLess0(X0,xa)|aElement0(sK16_skl(X2,X1,X0)))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f126])).
% 29.20/14.14 fof(f132,plain,(
% 29.20/14.14 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X0)|~X0=X2|~iLess0(X0,xa)|sdtmndtasgtdt0(X1,xR,sK16_skl(X2,X1,X0)))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f126])).
% 29.20/14.14 fof(f137,plain,(
% 29.20/14.14 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X0)|~X0=X2|~iLess0(X0,xa)|sdtmndtasgtdt0(X2,xR,sK16_skl(X2,X1,X0)))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f126])).
% 29.20/14.14 fof(f160,plain,(
% 29.20/14.14 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X0)|~sdtmndtplgtdt0(X0,xR,X2)|~iLess0(X0,xa)|aElement0(sK16_skl(X2,X1,X0)))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f126])).
% 29.20/14.14 fof(f165,plain,(
% 29.20/14.14 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X0)|~sdtmndtplgtdt0(X0,xR,X2)|~iLess0(X0,xa)|sdtmndtasgtdt0(X1,xR,sK16_skl(X2,X1,X0)))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f126])).
% 29.20/14.14 fof(f170,plain,(
% 29.20/14.14 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X0)|~sdtmndtplgtdt0(X0,xR,X2)|~iLess0(X0,xa)|sdtmndtasgtdt0(X2,xR,sK16_skl(X2,X1,X0)))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f126])).
% 29.20/14.14 fof(f182,plain,(
% 29.20/14.14 (((aReductOfIn0(xb,xa,xR)|((aElement0(sK19_skl)&aReductOfIn0(sK19_skl,xa,xR))&sdtmndtplgtdt0(sK19_skl,xR,xb)))&sdtmndtplgtdt0(xa,xR,xb))&(aReductOfIn0(xc,xa,xR)|((aElement0(sK20_skl)&aReductOfIn0(sK20_skl,xa,xR))&sdtmndtplgtdt0(sK20_skl,xR,xc))))&sdtmndtplgtdt0(xa,xR,xc)),
% 29.20/14.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(W0,sK19_skl),skolemize(W0,sK20_skl)],[f19])).
% 29.20/14.14 fof(f186,plain,(
% 29.20/14.14 sdtmndtplgtdt0(xa,xR,xb)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f182])).
% 29.20/14.14 fof(f191,plain,(
% 29.20/14.14 ((aElement0(xu)&aReductOfIn0(xu,xa,xR))&(xu=xb|((aReductOfIn0(xb,xu,xR)|((aElement0(sK21_skl)&aReductOfIn0(sK21_skl,xu,xR))&sdtmndtplgtdt0(sK21_skl,xR,xb)))&sdtmndtplgtdt0(xu,xR,xb))))&sdtmndtasgtdt0(xu,xR,xb)),
% 29.20/14.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(W0,sK21_skl)],[f20])).
% 29.20/14.14 fof(f192,plain,(
% 29.20/14.14 aElement0(xu)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f191])).
% 29.20/14.14 fof(f193,plain,(
% 29.20/14.14 aReductOfIn0(xu,xa,xR)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f191])).
% 29.20/14.14 fof(f197,plain,(
% 29.20/14.14 xu=xb|sdtmndtplgtdt0(xu,xR,xb)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f191])).
% 29.20/14.14 fof(f207,plain,(
% 29.20/14.14 (((aElement0(xw)&(xu=xw|((aReductOfIn0(xw,xu,xR)|((aElement0(sK23_skl)&aReductOfIn0(sK23_skl,xu,xR))&sdtmndtplgtdt0(sK23_skl,xR,xw)))&sdtmndtplgtdt0(xu,xR,xw))))&sdtmndtasgtdt0(xu,xR,xw))&(xv=xw|((aReductOfIn0(xw,xv,xR)|((aElement0(sK24_skl)&aReductOfIn0(sK24_skl,xv,xR))&sdtmndtplgtdt0(sK24_skl,xR,xw)))&sdtmndtplgtdt0(xv,xR,xw))))&sdtmndtasgtdt0(xv,xR,xw)),
% 29.20/14.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(W0,sK23_skl),skolemize(W0,sK24_skl)],[f22])).
% 29.20/14.14 fof(f208,plain,(
% 29.20/14.14 aElement0(xw)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f207])).
% 29.20/14.14 fof(f212,plain,(
% 29.20/14.14 xu=xw|sdtmndtplgtdt0(xu,xR,xw)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f207])).
% 29.20/14.14 fof(f213,plain,(
% 29.20/14.14 sdtmndtasgtdt0(xu,xR,xw)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f207])).
% 29.20/14.14 fof(f219,plain,(
% 29.20/14.14 (((aElement0(xd)&(xw=xd|((aReductOfIn0(xd,xw,xR)|(?[W0]: ((aElement0(W0)&aReductOfIn0(W0,xw,xR))&sdtmndtplgtdt0(W0,xR,xd))))&sdtmndtplgtdt0(xw,xR,xd))))&sdtmndtasgtdt0(xw,xR,xd))&(![W0]: ~aReductOfIn0(W0,xd,xR)))&aNormalFormOfIn0(xd,xw,xR)),
% 29.20/14.14 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 29.20/14.14 fof(f220,plain,(
% 29.20/14.14 (((aElement0(xd)&(xw=xd|((aReductOfIn0(xd,xw,xR)|((aElement0(sK25_skl)&aReductOfIn0(sK25_skl,xw,xR))&sdtmndtplgtdt0(sK25_skl,xR,xd)))&sdtmndtplgtdt0(xw,xR,xd))))&sdtmndtasgtdt0(xw,xR,xd))&(![W0]: ~aReductOfIn0(W0,xd,xR)))&aNormalFormOfIn0(xd,xw,xR)),
% 29.20/14.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(W0,sK25_skl)],[f219])).
% 29.20/14.14 fof(f221,plain,(
% 29.20/14.14 aElement0(xd)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f220])).
% 29.20/14.14 fof(f226,plain,(
% 29.20/14.14 sdtmndtasgtdt0(xw,xR,xd)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f220])).
% 29.20/14.14 fof(f229,plain,(
% 29.20/14.14 (![W0]: ((~aElement0(W0)|((((~xb=W0&~aReductOfIn0(W0,xb,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xb,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xb,xR,W0))&~sdtmndtasgtdt0(xb,xR,W0)))|((((~xd=W0&~aReductOfIn0(W0,xd,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xd,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xd,xR,W0))&~sdtmndtasgtdt0(xd,xR,W0))))),
% 29.20/14.14 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 29.20/14.14 fof(f230,definition,(
% 29.20/14.14 ![W0]: (sP1_prd(W0)<=>((((~xb=W0&~aReductOfIn0(W0,xb,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xb,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xb,xR,W0))&~sdtmndtasgtdt0(xb,xR,W0)))),
% 29.20/14.14 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 29.20/14.14 fof(f231,plain,(
% 29.20/14.14 ![W0]: ((~aElement0(W0)|sP1_prd(W0))|((((~xd=W0&~aReductOfIn0(W0,xd,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xd,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xd,xR,W0))&~sdtmndtasgtdt0(xd,xR,W0)))),
% 29.20/14.14 inference(formula_renaming,[status(thm)],[f229,f230])).
% 29.20/14.14 fof(f232,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|sP1_prd(X0)|~xd=X0)),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f231])).
% 29.20/14.14 fof(f236,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|sP1_prd(X0)|~sdtmndtasgtdt0(xd,xR,X0))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f231])).
% 29.20/14.14 fof(f237,plain,(
% 29.20/14.14 ![W0,W1]: ((~sP0_prd(W1,W0)|((((~W0=W1&~aReductOfIn0(W1,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))&~sdtmndtasgtdt0(W0,xR,W1)))&(sP0_prd(W1,W0)|((((W0=W1|aReductOfIn0(W1,W0,xR))|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W1))))|sdtmndtplgtdt0(W0,xR,W1))|sdtmndtasgtdt0(W0,xR,W1))))),
% 29.20/14.14 inference(NNF_transformation,[status(thm)],[f124])).
% 29.20/14.14 fof(f238,plain,(
% 29.20/14.14 (![W0,W1]: (~sP0_prd(W1,W0)|((((~W0=W1&~aReductOfIn0(W1,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))&~sdtmndtasgtdt0(W0,xR,W1))))&(![W0,W1]: (sP0_prd(W1,W0)|((((W0=W1|aReductOfIn0(W1,W0,xR))|(?[W3]: ((aElement0(W3)&aReductOfIn0(W3,W0,xR))&sdtmndtplgtdt0(W3,xR,W1))))|sdtmndtplgtdt0(W0,xR,W1))|sdtmndtasgtdt0(W0,xR,W1))))),
% 29.20/14.14 inference(miniscoping,[status(thm)],[f237])).
% 29.20/14.14 fof(f239,plain,(
% 29.20/14.14 (![W0,W1]: (~sP0_prd(W1,W0)|((((~W0=W1&~aReductOfIn0(W1,W0,xR))&(![W3]: ((~aElement0(W3)|~aReductOfIn0(W3,W0,xR))|~sdtmndtplgtdt0(W3,xR,W1))))&~sdtmndtplgtdt0(W0,xR,W1))&~sdtmndtasgtdt0(W0,xR,W1))))&(![W0,W1]: (sP0_prd(W1,W0)|((((W0=W1|aReductOfIn0(W1,W0,xR))|((aElement0(sK26_skl(W1,W0))&aReductOfIn0(sK26_skl(W1,W0),W0,xR))&sdtmndtplgtdt0(sK26_skl(W1,W0),xR,W1)))|sdtmndtplgtdt0(W0,xR,W1))|sdtmndtasgtdt0(W0,xR,W1))))),
% 29.20/14.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK26_skl]),skolemize(W3,sK26_skl(W1,W0))],[f238])).
% 29.20/14.14 fof(f243,plain,(
% 29.20/14.14 ![X0,X1]: (~sP0_prd(X0,X1)|~sdtmndtplgtdt0(X1,xR,X0))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f239])).
% 29.20/14.14 fof(f244,plain,(
% 29.20/14.14 ![X0,X1]: (~sP0_prd(X0,X1)|~sdtmndtasgtdt0(X1,xR,X0))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f239])).
% 29.20/14.14 fof(f248,plain,(
% 29.20/14.14 ![W0]: ((~sP1_prd(W0)|((((~xb=W0&~aReductOfIn0(W0,xb,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xb,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xb,xR,W0))&~sdtmndtasgtdt0(xb,xR,W0)))&(sP1_prd(W0)|((((xb=W0|aReductOfIn0(W0,xb,xR))|(?[W1]: ((aElement0(W1)&aReductOfIn0(W1,xb,xR))&sdtmndtplgtdt0(W1,xR,W0))))|sdtmndtplgtdt0(xb,xR,W0))|sdtmndtasgtdt0(xb,xR,W0))))),
% 29.20/14.14 inference(NNF_transformation,[status(thm)],[f230])).
% 29.20/14.14 fof(f249,plain,(
% 29.20/14.14 (![W0]: (~sP1_prd(W0)|((((~xb=W0&~aReductOfIn0(W0,xb,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xb,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xb,xR,W0))&~sdtmndtasgtdt0(xb,xR,W0))))&(![W0]: (sP1_prd(W0)|((((xb=W0|aReductOfIn0(W0,xb,xR))|(?[W1]: ((aElement0(W1)&aReductOfIn0(W1,xb,xR))&sdtmndtplgtdt0(W1,xR,W0))))|sdtmndtplgtdt0(xb,xR,W0))|sdtmndtasgtdt0(xb,xR,W0))))),
% 29.20/14.14 inference(miniscoping,[status(thm)],[f248])).
% 29.20/14.14 fof(f250,plain,(
% 29.20/14.14 (![W0]: (~sP1_prd(W0)|((((~xb=W0&~aReductOfIn0(W0,xb,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xb,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xb,xR,W0))&~sdtmndtasgtdt0(xb,xR,W0))))&(![W0]: (sP1_prd(W0)|((((xb=W0|aReductOfIn0(W0,xb,xR))|((aElement0(sK27_skl(W0))&aReductOfIn0(sK27_skl(W0),xb,xR))&sdtmndtplgtdt0(sK27_skl(W0),xR,W0)))|sdtmndtplgtdt0(xb,xR,W0))|sdtmndtasgtdt0(xb,xR,W0))))),
% 29.20/14.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK27_skl]),skolemize(W1,sK27_skl(W0))],[f249])).
% 29.20/14.14 fof(f255,plain,(
% 29.20/14.14 ![X0]: (~sP1_prd(X0)|~sdtmndtasgtdt0(xb,xR,X0))),
% 29.20/14.14 inference(cnf_transformation,[status(thm)],[f250])).
% 29.20/14.14 fof(f266,plain,(
% 29.20/14.14 ![X2,X1]: (~aElement0(X2)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X2)|~iLess0(X2,xa)|aElement0(sK16_skl(X2,X1,X2)))),
% 29.20/14.14 inference(destructive_equality_resolution,[status(thm)],[f127])).
% 29.20/14.14 fof(f267,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sP0_prd(X1,X0)|~iLess0(X0,xa)|aElement0(sK16_skl(X0,X1,X0)))),
% 29.20/14.14 inference(duplicate_literals_removal,[status(thm)],[f266])).
% 29.20/14.14 fof(f276,plain,(
% 29.20/14.14 ![X2,X1]: (~aElement0(X2)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X2)|~iLess0(X2,xa)|sdtmndtasgtdt0(X1,xR,sK16_skl(X2,X1,X2)))),
% 29.20/14.14 inference(destructive_equality_resolution,[status(thm)],[f132])).
% 29.20/14.14 fof(f277,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sP0_prd(X1,X0)|~iLess0(X0,xa)|sdtmndtasgtdt0(X1,xR,sK16_skl(X0,X1,X0)))),
% 29.20/14.14 inference(duplicate_literals_removal,[status(thm)],[f276])).
% 29.20/14.14 fof(f286,plain,(
% 29.20/14.14 ![X2,X1]: (~aElement0(X2)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X2)|~iLess0(X2,xa)|sdtmndtasgtdt0(X2,xR,sK16_skl(X2,X1,X2)))),
% 29.20/14.14 inference(destructive_equality_resolution,[status(thm)],[f137])).
% 29.20/14.14 fof(f287,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sP0_prd(X1,X0)|~iLess0(X0,xa)|sdtmndtasgtdt0(X0,xR,sK16_skl(X0,X1,X0)))),
% 29.20/14.14 inference(duplicate_literals_removal,[status(thm)],[f286])).
% 29.20/14.14 fof(f288,plain,(
% 29.20/14.14 ~aElement0(xd)|sP1_prd(xd)),
% 29.20/14.14 inference(destructive_equality_resolution,[status(thm)],[f232])).
% 29.20/14.14 fof(f289,plain,(
% 29.20/14.14 sP1_prd(xd)),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f288,f221])).
% 29.20/14.14 fof(f314,plain,(
% 29.20/14.14 ~aElement0(xa)|~aElement0(xb)|iLess0(xb,xa)),
% 29.20/14.14 inference(resolution,[status(thm)],[f118,f186])).
% 29.20/14.14 fof(f317,plain,(
% 29.20/14.14 ~aElement0(xb)|iLess0(xb,xa)),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f314,f120])).
% 29.20/14.14 fof(f326,plain,(
% 29.20/14.14 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|~sdtmndtasgtdt0(X0,xR,X1)|~sdtmndtasgtdt0(X1,xR,X2)|sdtmndtasgtdt0(X0,xR,X2))),
% 29.20/14.14 inference(resolution,[status(thm)],[f100,f54])).
% 29.20/14.14 fof(f330,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|~sdtmndtasgtdt0(X0,xR,X1)|X0=X1|sdtmndtplgtdt0(X0,xR,X1))),
% 29.20/14.14 inference(resolution,[status(thm)],[f100,f50])).
% 29.20/14.14 fof(f331,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sdtmndtasgtdt0(X0,xR,X1)|~sdtmndtplgtdt0(X0,xR,X1))),
% 29.20/14.14 inference(resolution,[status(thm)],[f100,f52])).
% 29.20/14.14 fof(f334,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aReductOfIn0(X1,X0,xR)|aElement0(X1))),
% 29.20/14.14 inference(resolution,[status(thm)],[f100,f33])).
% 29.20/14.14 fof(f360,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aReductOfIn0(X1,X0,xR)|iLess0(X1,X0))),
% 29.20/14.14 inference(backward_subsumption_resolution,[status(thm)],[f116,f334])).
% 29.20/14.14 fof(f398,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|sdtmndtasgtdt0(X0,xR,xw)|~sdtmndtplgtdt0(X0,xR,xw))),
% 29.20/14.14 inference(resolution,[status(thm)],[f331,f208])).
% 29.20/14.14 fof(f404,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|~sdtmndtasgtdt0(X0,xR,xd)|X0=xd|sdtmndtplgtdt0(X0,xR,xd))),
% 29.20/14.14 inference(resolution,[status(thm)],[f330,f221])).
% 29.20/14.14 fof(f513,plain,(
% 29.20/14.14 sP1_prd(xu)|~sdtmndtasgtdt0(xd,xR,xu)),
% 29.20/14.14 inference(resolution,[status(thm)],[f192,f236])).
% 29.20/14.14 fof(f595,plain,(
% 29.20/14.14 ~aElement0(xa)|iLess0(xu,xa)),
% 29.20/14.14 inference(resolution,[status(thm)],[f360,f193])).
% 29.20/14.14 fof(f602,plain,(
% 29.20/14.14 iLess0(xu,xa)),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f595,f120])).
% 29.20/14.14 fof(f742,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sP0_prd(X1,X0)|~iLess0(X0,xa)|sP1_prd(sK16_skl(X0,X1,X0))|~sdtmndtasgtdt0(xd,xR,sK16_skl(X0,X1,X0)))),
% 29.20/14.14 inference(resolution,[status(thm)],[f267,f236])).
% 29.20/14.14 fof(f1064,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|~aElement0(xd)|sP0_prd(xd,X0)|~iLess0(X0,xa)|~aElement0(X0)|~aElement0(xd)|sP0_prd(xd,X0)|~iLess0(X0,xa)|sP1_prd(sK16_skl(X0,xd,X0)))),
% 29.20/14.14 inference(resolution,[status(thm)],[f277,f742])).
% 29.20/14.14 fof(f1067,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|~aElement0(xd)|sP0_prd(xd,X0)|~iLess0(X0,xa)|sP1_prd(sK16_skl(X0,xd,X0)))),
% 29.20/14.14 inference(duplicate_literals_removal,[status(thm)],[f1064])).
% 29.20/14.14 fof(f1068,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|sP0_prd(xd,X0)|~iLess0(X0,xa)|sP1_prd(sK16_skl(X0,xd,X0)))),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f1067,f221])).
% 29.20/14.14 fof(f1399,plain,(
% 29.20/14.14 ![X0]: (~aElement0(xb)|~aElement0(X0)|sP0_prd(X0,xb)|~iLess0(xb,xa)|~sP1_prd(sK16_skl(xb,X0,xb)))),
% 29.20/14.14 inference(resolution,[status(thm)],[f287,f255])).
% 29.20/14.14 fof(f1403,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|sP0_prd(X0,xb)|~iLess0(xb,xa)|~sP1_prd(sK16_skl(xb,X0,xb)))),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f1399,f121])).
% 29.20/14.14 fof(f1412,plain,(
% 29.20/14.14 ![X0,X1,X2]: (~aElement0(X0)|~aElement0(X1)|~aElement0(X2)|sP0_prd(X1,X0)|~sdtmndtplgtdt0(X0,xR,X2)|~iLess0(X0,xa)|sP1_prd(sK16_skl(X2,X1,X0))|~sdtmndtasgtdt0(xd,xR,sK16_skl(X2,X1,X0)))),
% 29.20/14.14 inference(resolution,[status(thm)],[f160,f236])).
% 29.20/14.14 fof(f1442,plain,(
% 29.20/14.14 ~aElement0(xd)|sP0_prd(xd,xb)|~iLess0(xb,xa)|~aElement0(xb)|sP0_prd(xd,xb)|~iLess0(xb,xa)),
% 29.20/14.14 inference(resolution,[status(thm)],[f1403,f1068])).
% 29.20/14.14 fof(f1443,plain,(
% 29.20/14.14 ~aElement0(xd)|sP0_prd(xd,xb)|~iLess0(xb,xa)|~aElement0(xb)),
% 29.20/14.14 inference(duplicate_literals_removal,[status(thm)],[f1442])).
% 29.20/14.14 fof(f1444,plain,(
% 29.20/14.14 sP0_prd(xd,xb)|~iLess0(xb,xa)|~aElement0(xb)),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f1443,f221])).
% 29.20/14.14 fof(f1445,plain,(
% 29.20/14.14 sP0_prd(xd,xb)|~iLess0(xb,xa)),
% 29.20/14.14 inference(resolution,[status(thm)],[f1444,f121])).
% 29.20/14.14 fof(f1448,plain,(
% 29.20/14.14 sP0_prd(xd,xb)|~aElement0(xb)),
% 29.20/14.14 inference(resolution,[status(thm)],[f1445,f317])).
% 29.20/14.14 fof(f1450,plain,(
% 29.20/14.14 sP0_prd(xd,xb)),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f1448,f121])).
% 29.20/14.14 fof(f1454,plain,(
% 29.20/14.14 ~sdtmndtplgtdt0(xb,xR,xd)),
% 29.20/14.14 inference(resolution,[status(thm)],[f1450,f243])).
% 29.20/14.14 fof(f1781,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|~aElement0(xw)|~aElement0(xd)|~sdtmndtasgtdt0(X0,xR,xw)|sdtmndtasgtdt0(X0,xR,xd))),
% 29.20/14.14 inference(resolution,[status(thm)],[f326,f226])).
% 29.20/14.14 fof(f1813,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|~aElement0(xd)|~sdtmndtasgtdt0(X0,xR,xw)|sdtmndtasgtdt0(X0,xR,xd))),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f1781,f208])).
% 29.20/14.14 fof(f1873,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|~sdtmndtasgtdt0(X0,xR,xw)|sdtmndtasgtdt0(X0,xR,xd))),
% 29.20/14.14 inference(resolution,[status(thm)],[f1813,f221])).
% 29.20/14.14 fof(f1875,plain,(
% 29.20/14.14 ~aElement0(xb)|~sdtmndtasgtdt0(xb,xR,xw)|~sP1_prd(xd)),
% 29.20/14.14 inference(resolution,[status(thm)],[f1873,f255])).
% 29.20/14.14 fof(f1876,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|~sdtmndtasgtdt0(X0,xR,xw)|~aElement0(X0)|X0=xd|sdtmndtplgtdt0(X0,xR,xd))),
% 29.20/14.14 inference(resolution,[status(thm)],[f1873,f404])).
% 29.20/14.14 fof(f1878,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|~sdtmndtasgtdt0(X0,xR,xw)|~sP0_prd(xd,X0))),
% 29.20/14.14 inference(resolution,[status(thm)],[f1873,f244])).
% 29.20/14.14 fof(f1880,plain,(
% 29.20/14.14 ~sdtmndtasgtdt0(xb,xR,xw)|~sP1_prd(xd)),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f1875,f121])).
% 29.20/14.14 fof(f1881,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|~sdtmndtasgtdt0(X0,xR,xw)|X0=xd|sdtmndtplgtdt0(X0,xR,xd))),
% 29.20/14.14 inference(duplicate_literals_removal,[status(thm)],[f1876])).
% 29.20/14.14 fof(f1884,plain,(
% 29.20/14.14 ~sdtmndtasgtdt0(xb,xR,xw)),
% 29.20/14.14 inference(resolution,[status(thm)],[f1880,f289])).
% 29.20/14.14 fof(f1886,plain,(
% 29.20/14.14 ~aElement0(xb)|~sdtmndtplgtdt0(xb,xR,xw)),
% 29.20/14.14 inference(resolution,[status(thm)],[f1884,f398])).
% 29.20/14.14 fof(f1888,plain,(
% 29.20/14.14 ~sdtmndtplgtdt0(xb,xR,xw)),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f1886,f121])).
% 29.20/14.14 fof(f1890,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(xd)|~aElement0(X1)|sP0_prd(xd,X0)|~sdtmndtplgtdt0(X0,xR,X1)|~iLess0(X0,xa)|~aElement0(X0)|~aElement0(xd)|~aElement0(X1)|sP0_prd(xd,X0)|~sdtmndtplgtdt0(X0,xR,X1)|~iLess0(X0,xa)|sP1_prd(sK16_skl(X1,xd,X0)))),
% 29.20/14.14 inference(resolution,[status(thm)],[f165,f1412])).
% 29.20/14.14 fof(f1896,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(xd)|~aElement0(X1)|sP0_prd(xd,X0)|~sdtmndtplgtdt0(X0,xR,X1)|~iLess0(X0,xa)|sP1_prd(sK16_skl(X1,xd,X0)))),
% 29.20/14.14 inference(duplicate_literals_removal,[status(thm)],[f1890])).
% 29.20/14.14 fof(f1897,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sP0_prd(xd,X0)|~sdtmndtplgtdt0(X0,xR,X1)|~iLess0(X0,xa)|sP1_prd(sK16_skl(X1,xd,X0)))),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f1896,f221])).
% 29.20/14.14 fof(f2002,plain,(
% 29.20/14.14 ~aElement0(xu)|xu=xd|sdtmndtplgtdt0(xu,xR,xd)),
% 29.20/14.14 inference(resolution,[status(thm)],[f1881,f213])).
% 29.20/14.14 fof(f2006,plain,(
% 29.20/14.14 xu=xd|sdtmndtplgtdt0(xu,xR,xd)),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f2002,f192])).
% 29.20/14.14 fof(f2150,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|~aElement0(xb)|sP0_prd(X1,X0)|~sdtmndtplgtdt0(X0,xR,xb)|~iLess0(X0,xa)|~sP1_prd(sK16_skl(xb,X1,X0)))),
% 29.20/14.14 inference(resolution,[status(thm)],[f170,f255])).
% 29.20/14.14 fof(f2157,plain,(
% 29.20/14.14 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|sP0_prd(X1,X0)|~sdtmndtplgtdt0(X0,xR,xb)|~iLess0(X0,xa)|~sP1_prd(sK16_skl(xb,X1,X0)))),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f2150,f121])).
% 29.20/14.14 fof(f2848,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|~aElement0(xb)|sP0_prd(xd,X0)|~sdtmndtplgtdt0(X0,xR,xb)|~iLess0(X0,xa)|~aElement0(X0)|~aElement0(xd)|sP0_prd(xd,X0)|~sdtmndtplgtdt0(X0,xR,xb)|~iLess0(X0,xa))),
% 29.20/14.14 inference(resolution,[status(thm)],[f1897,f2157])).
% 29.20/14.14 fof(f2852,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|~aElement0(xb)|sP0_prd(xd,X0)|~sdtmndtplgtdt0(X0,xR,xb)|~iLess0(X0,xa)|~aElement0(xd))),
% 29.20/14.14 inference(duplicate_literals_removal,[status(thm)],[f2848])).
% 29.20/14.14 fof(f2853,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|sP0_prd(xd,X0)|~sdtmndtplgtdt0(X0,xR,xb)|~iLess0(X0,xa)|~aElement0(xd))),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f2852,f121])).
% 29.20/14.14 fof(f2854,plain,(
% 29.20/14.14 ![X0]: (~aElement0(X0)|sP0_prd(xd,X0)|~sdtmndtplgtdt0(X0,xR,xb)|~iLess0(X0,xa))),
% 29.20/14.14 inference(resolution,[status(thm)],[f2853,f221])).
% 29.20/14.14 fof(f2856,plain,(
% 29.20/14.14 ~aElement0(xu)|sP0_prd(xd,xu)|~iLess0(xu,xa)|xu=xb),
% 29.20/14.14 inference(resolution,[status(thm)],[f2854,f197])).
% 29.20/14.14 fof(f2863,plain,(
% 29.20/14.14 sP0_prd(xd,xu)|~iLess0(xu,xa)|xu=xb),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f2856,f192])).
% 29.20/14.14 fof(f2870,plain,(
% 29.20/14.14 sP0_prd(xd,xu)|xu=xb),
% 29.20/14.14 inference(resolution,[status(thm)],[f2863,f602])).
% 29.20/14.14 fof(f2872,plain,(
% 29.20/14.14 xu=xb|~aElement0(xu)|~sdtmndtasgtdt0(xu,xR,xw)),
% 29.20/14.14 inference(resolution,[status(thm)],[f2870,f1878])).
% 29.20/14.14 fof(f2876,plain,(
% 29.20/14.14 xu=xb|~sdtmndtasgtdt0(xu,xR,xw)),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f2872,f192])).
% 29.20/14.14 fof(f2877,plain,(
% 29.20/14.14 xu=xb),
% 29.20/14.14 inference(resolution,[status(thm)],[f2876,f213])).
% 29.20/14.14 fof(f2903,plain,(
% 29.20/14.14 xu=xd|sdtmndtplgtdt0(xb,xR,xd)),
% 29.20/14.14 inference(backward_demodulation,[status(thm)],[f2877,f2006])).
% 29.20/14.14 fof(f2951,plain,(
% 29.20/14.14 xu=xw|sdtmndtplgtdt0(xb,xR,xw)),
% 29.20/14.14 inference(backward_demodulation,[status(thm)],[f2877,f212])).
% 29.20/14.14 fof(f2956,plain,(
% 29.20/14.14 sP1_prd(xu)|~sdtmndtasgtdt0(xd,xR,xb)),
% 29.20/14.14 inference(backward_demodulation,[status(thm)],[f2877,f513])).
% 29.20/14.14 fof(f2962,plain,(
% 29.20/14.14 sdtmndtasgtdt0(xb,xR,xw)),
% 29.20/14.14 inference(backward_demodulation,[status(thm)],[f2877,f213])).
% 29.20/14.14 fof(f3063,plain,(
% 29.20/14.14 xb=xd|sdtmndtplgtdt0(xb,xR,xd)),
% 29.20/14.14 inference(forward_demodulation,[status(thm)],[f2877,f2903])).
% 29.20/14.14 fof(f3411,plain,(
% 29.20/14.14 xb=xd),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f3063,f1454])).
% 29.20/14.14 fof(f3480,plain,(
% 29.20/14.14 xb=xw|sdtmndtplgtdt0(xb,xR,xw)),
% 29.20/14.14 inference(forward_demodulation,[status(thm)],[f2877,f2951])).
% 29.20/14.14 fof(f3585,plain,(
% 29.20/14.14 xb=xw),
% 29.20/14.14 inference(forward_subsumption_resolution,[status(thm)],[f3480,f1888])).
% 29.20/14.14 fof(f3596,plain,(
% 29.20/14.14 sP1_prd(xb)|~sdtmndtasgtdt0(xd,xR,xb)),
% 29.20/14.14 inference(forward_demodulation,[status(thm)],[f2877,f2956])).
% 29.20/14.16 fof(f3597,plain,(
% 29.20/14.16 sP1_prd(xb)|~sdtmndtasgtdt0(xb,xR,xb)),
% 29.20/14.16 inference(forward_demodulation,[status(thm)],[f3411,f3596])).
% 29.20/14.16 fof(f3598,plain,(
% 29.20/14.16 ~sdtmndtasgtdt0(xb,xR,xb)),
% 29.20/14.16 inference(forward_subsumption_resolution,[status(thm)],[f3597,f255])).
% 29.20/14.16 fof(f3602,plain,(
% 29.20/14.16 sdtmndtasgtdt0(xb,xR,xb)),
% 29.20/14.16 inference(forward_demodulation,[status(thm)],[f3585,f2962])).
% 29.20/14.16 fof(f3603,plain,(
% 29.20/14.16 $false),
% 29.20/14.16 inference(forward_subsumption_resolution,[status(thm)],[f3602,f3598])).
% 29.20/14.16 % SZS output end CNFRefutation for theBenchmark.p
% 29.20/14.17 % Elapsed time: 3.778392 seconds
% 29.20/14.17 % CPU time: 29.719310 seconds
% 29.20/14.17 % Total memory used: 239.625 MB
% 29.20/14.17 % Net memory used: 217.287 MB
%------------------------------------------------------------------------------