%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM022+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 : n017.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:44 PM UTC 2026
% Result : Theorem 0.13s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM022+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n017.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.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Mon Sep 21 14:09:57 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.36 % Drodi V4.1.1
% 0.13/0.42 % Refutation found
% 0.13/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.42 fof(f8,definition,(
% 0.13/0.42 (! [W0,W1,W2] :( ( aElement0(W0)& aRewritingSystem0(W1)& aElement0(W2) )=> ( sdtmndtasgtdt0(W0,W1,W2)<=> ( W0 = W2| sdtmndtplgtdt0(W0,W1,W2) ) ) ) )),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f13,definition,(
% 0.13/0.42 (! [W0,W1] :( ( aElement0(W0)& aRewritingSystem0(W1) )=> (! [W2] :( aNormalFormOfIn0(W2,W0,W1)<=> ( aElement0(W2)& sdtmndtasgtdt0(W0,W1,W2)& ~ (? [W3] : aReductOfIn0(W3,W2,W1) )) ) )) )),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f15,hypothesis,(
% 0.13/0.42 aRewritingSystem0(xR) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f16,hypothesis,(
% 0.13/0.42 ( isLocallyConfluent0(xR)& isTerminating0(xR) ) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f17,hypothesis,(
% 0.13/0.42 ( aElement0(xa)& aElement0(xb)& aElement0(xc) ) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f19,conjecture,(
% 0.13/0.42 ( ( ( sdtmndtplgtdt0(xa,xR,xb)& sdtmndtplgtdt0(xa,xR,xc) )=> (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtasgtdt0(W0,xR,xb)& (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xa,xR)& sdtmndtasgtdt0(W1,xR,xc)& (? [W2] :( aElement0(W2)& sdtmndtasgtdt0(W0,xR,W2)& sdtmndtasgtdt0(W1,xR,W2)& (? [W3] :( aNormalFormOfIn0(W3,W2,xR)& sdtmndtasgtdt0(xb,xR,W3)& sdtmndtasgtdt0(xc,xR,W3) ) )) )) )) ))=> ( ( sdtmndtasgtdt0(xa,xR,xb)& sdtmndtasgtdt0(xa,xR,xc) )=> (? [W0] :( aElement0(W0)& sdtmndtasgtdt0(xb,xR,W0)& sdtmndtasgtdt0(xc,xR,W0) ) )) ) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f20,negated_conjecture,(
% 0.13/0.42 ~(( ( ( sdtmndtplgtdt0(xa,xR,xb)& sdtmndtplgtdt0(xa,xR,xc) )=> (? [W0] :( aElement0(W0)& aReductOfIn0(W0,xa,xR)& sdtmndtasgtdt0(W0,xR,xb)& (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xa,xR)& sdtmndtasgtdt0(W1,xR,xc)& (? [W2] :( aElement0(W2)& sdtmndtasgtdt0(W0,xR,W2)& sdtmndtasgtdt0(W1,xR,W2)& (? [W3] :( aNormalFormOfIn0(W3,W2,xR)& sdtmndtasgtdt0(xb,xR,W3)& sdtmndtasgtdt0(xc,xR,W3) ) )) )) )) ))=> ( ( sdtmndtasgtdt0(xa,xR,xb)& sdtmndtasgtdt0(xa,xR,xc) )=> (? [W0] :( aElement0(W0)& sdtmndtasgtdt0(xb,xR,W0)& sdtmndtasgtdt0(xc,xR,W0) ) )) ) )),
% 0.13/0.42 inference(negated_conjecture,[status(cth)],[f19])).
% 0.13/0.42 fof(f43,plain,(
% 0.13/0.42 ![W0,W1,W2]: (((~aElement0(W0)|~aRewritingSystem0(W1))|~aElement0(W2))|(sdtmndtasgtdt0(W0,W1,W2)<=>(W0=W2|sdtmndtplgtdt0(W0,W1,W2))))),
% 0.13/0.42 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.13/0.42 fof(f44,plain,(
% 0.13/0.42 ![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)))))),
% 0.13/0.42 inference(NNF_transformation,[status(thm)],[f43])).
% 0.13/0.42 fof(f45,plain,(
% 0.13/0.42 ![X0,X1,X2]: (~aElement0(X0)|~aRewritingSystem0(X1)|~aElement0(X2)|~sdtmndtasgtdt0(X0,X1,X2)|X0=X2|sdtmndtplgtdt0(X0,X1,X2))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.42 fof(f46,plain,(
% 0.13/0.42 ![X0,X1,X2]: (~aElement0(X0)|~aRewritingSystem0(X1)|~aElement0(X2)|sdtmndtasgtdt0(X0,X1,X2)|~X0=X2)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.42 fof(f84,plain,(
% 0.13/0.42 ![W0,W1]: ((~aElement0(W0)|~aRewritingSystem0(W1))|(![W2]: (aNormalFormOfIn0(W2,W0,W1)<=>((aElement0(W2)&sdtmndtasgtdt0(W0,W1,W2))&(![W3]: ~aReductOfIn0(W3,W2,W1))))))),
% 0.13/0.42 inference(pre_NNF_transformation,[status(thm)],[f13])).
% 0.13/0.42 fof(f85,plain,(
% 0.13/0.42 ![W0,W1]: ((~aElement0(W0)|~aRewritingSystem0(W1))|(![W2]: ((~aNormalFormOfIn0(W2,W0,W1)|((aElement0(W2)&sdtmndtasgtdt0(W0,W1,W2))&(![W3]: ~aReductOfIn0(W3,W2,W1))))&(aNormalFormOfIn0(W2,W0,W1)|((~aElement0(W2)|~sdtmndtasgtdt0(W0,W1,W2))|(?[W3]: aReductOfIn0(W3,W2,W1)))))))),
% 0.13/0.42 inference(NNF_transformation,[status(thm)],[f84])).
% 0.13/0.42 fof(f86,plain,(
% 0.13/0.42 ![W0,W1]: ((~aElement0(W0)|~aRewritingSystem0(W1))|((![W2]: (~aNormalFormOfIn0(W2,W0,W1)|((aElement0(W2)&sdtmndtasgtdt0(W0,W1,W2))&(![W3]: ~aReductOfIn0(W3,W2,W1)))))&(![W2]: (aNormalFormOfIn0(W2,W0,W1)|((~aElement0(W2)|~sdtmndtasgtdt0(W0,W1,W2))|(?[W3]: aReductOfIn0(W3,W2,W1)))))))),
% 0.13/0.42 inference(miniscoping,[status(thm)],[f85])).
% 0.13/0.42 fof(f87,plain,(
% 0.13/0.42 ![W0,W1]: ((~aElement0(W0)|~aRewritingSystem0(W1))|((![W2]: (~aNormalFormOfIn0(W2,W0,W1)|((aElement0(W2)&sdtmndtasgtdt0(W0,W1,W2))&(![W3]: ~aReductOfIn0(W3,W2,W1)))))&(![W2]: (aNormalFormOfIn0(W2,W0,W1)|((~aElement0(W2)|~sdtmndtasgtdt0(W0,W1,W2))|aReductOfIn0(sK11_skl(W2,W1,W0),W2,W1))))))),
% 0.13/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl]),skolemize(W3,sK11_skl(W2,W1,W0))],[f86])).
% 0.13/0.42 fof(f88,plain,(
% 0.13/0.42 ![X0,X1,X2]: (~aElement0(X0)|~aRewritingSystem0(X1)|~aNormalFormOfIn0(X2,X0,X1)|aElement0(X2))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f87])).
% 0.13/0.42 fof(f95,plain,(
% 0.13/0.42 aRewritingSystem0(xR)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.42 fof(f96,plain,(
% 0.13/0.42 isLocallyConfluent0(xR)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f16])).
% 0.13/0.42 fof(f98,plain,(
% 0.13/0.42 aElement0(xa)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.42 fof(f99,plain,(
% 0.13/0.42 aElement0(xb)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.42 fof(f100,plain,(
% 0.13/0.42 aElement0(xc)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.42 fof(f106,plain,(
% 0.13/0.42 (((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(?[W0]: (((aElement0(W0)&aReductOfIn0(W0,xa,xR))&sdtmndtasgtdt0(W0,xR,xb))&(?[W1]: (((aElement0(W1)&aReductOfIn0(W1,xa,xR))&sdtmndtasgtdt0(W1,xR,xc))&(?[W2]: (((aElement0(W2)&sdtmndtasgtdt0(W0,xR,W2))&sdtmndtasgtdt0(W1,xR,W2))&(?[W3]: ((aNormalFormOfIn0(W3,W2,xR)&sdtmndtasgtdt0(xb,xR,W3))&sdtmndtasgtdt0(xc,xR,W3))))))))))&((sdtmndtasgtdt0(xa,xR,xb)&sdtmndtasgtdt0(xa,xR,xc))&(![W0]: ((~aElement0(W0)|~sdtmndtasgtdt0(xb,xR,W0))|~sdtmndtasgtdt0(xc,xR,W0)))))),
% 0.13/0.42 inference(pre_NNF_transformation,[status(thm)],[f20])).
% 0.13/0.42 fof(f107,plain,(
% 0.13/0.42 ((~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc))|(((aElement0(sK14_skl)&aReductOfIn0(sK14_skl,xa,xR))&sdtmndtasgtdt0(sK14_skl,xR,xb))&(((aElement0(sK15_skl)&aReductOfIn0(sK15_skl,xa,xR))&sdtmndtasgtdt0(sK15_skl,xR,xc))&(((aElement0(sK16_skl)&sdtmndtasgtdt0(sK14_skl,xR,sK16_skl))&sdtmndtasgtdt0(sK15_skl,xR,sK16_skl))&((aNormalFormOfIn0(sK17_skl,sK16_skl,xR)&sdtmndtasgtdt0(xb,xR,sK17_skl))&sdtmndtasgtdt0(xc,xR,sK17_skl))))))&((sdtmndtasgtdt0(xa,xR,xb)&sdtmndtasgtdt0(xa,xR,xc))&(![W0]: ((~aElement0(W0)|~sdtmndtasgtdt0(xb,xR,W0))|~sdtmndtasgtdt0(xc,xR,W0))))),
% 0.13/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl,sK15_skl,sK16_skl,sK17_skl]),skolemize(W0,sK14_skl),skolemize(W1,sK15_skl),skolemize(W2,sK16_skl),skolemize(W3,sK17_skl)],[f106])).
% 0.13/0.42 fof(f114,plain,(
% 0.13/0.42 ~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc)|aElement0(sK16_skl)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.42 fof(f117,plain,(
% 0.13/0.42 ~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc)|aNormalFormOfIn0(sK17_skl,sK16_skl,xR)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.42 fof(f118,plain,(
% 0.13/0.42 ~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc)|sdtmndtasgtdt0(xb,xR,sK17_skl)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.42 fof(f119,plain,(
% 0.13/0.42 ~sdtmndtplgtdt0(xa,xR,xb)|~sdtmndtplgtdt0(xa,xR,xc)|sdtmndtasgtdt0(xc,xR,sK17_skl)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.42 fof(f120,plain,(
% 0.13/0.42 sdtmndtasgtdt0(xa,xR,xb)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.42 fof(f121,plain,(
% 0.13/0.42 sdtmndtasgtdt0(xa,xR,xc)),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.42 fof(f122,plain,(
% 0.13/0.42 ![X0]: (~aElement0(X0)|~sdtmndtasgtdt0(xb,xR,X0)|~sdtmndtasgtdt0(xc,xR,X0))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f107])).
% 0.13/0.42 fof(f123,definition,(
% 0.13/0.42 sQ0_spl <=> (sdtmndtplgtdt0(xa,xR,xb))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f126,definition,(
% 0.13/0.42 sQ1_spl <=> (sdtmndtplgtdt0(xa,xR,xc))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f153,definition,(
% 0.13/0.42 sQ8_spl <=> (aElement0(sK16_skl))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f156,plain,(
% 0.13/0.42 ~sQ0_spl|~sQ1_spl|sQ8_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f114,f123,f126,f153])).
% 0.13/0.42 fof(f165,definition,(
% 0.13/0.42 sQ11_spl <=> (aNormalFormOfIn0(sK17_skl,sK16_skl,xR))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f166,plain,(
% 0.13/0.42 aNormalFormOfIn0(sK17_skl,sK16_skl,xR)|~sQ11_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f165])).
% 0.13/0.42 fof(f168,plain,(
% 0.13/0.42 ~sQ0_spl|~sQ1_spl|sQ11_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f117,f123,f126,f165])).
% 0.13/0.42 fof(f169,definition,(
% 0.13/0.42 sQ12_spl <=> (sdtmndtasgtdt0(xb,xR,sK17_skl))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f172,plain,(
% 0.13/0.42 ~sQ0_spl|~sQ1_spl|sQ12_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f118,f123,f126,f169])).
% 0.13/0.42 fof(f173,definition,(
% 0.13/0.42 sQ13_spl <=> (sdtmndtasgtdt0(xc,xR,sK17_skl))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f174,plain,(
% 0.13/0.42 sdtmndtasgtdt0(xc,xR,sK17_skl)|~sQ13_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f173])).
% 0.13/0.42 fof(f176,plain,(
% 0.13/0.42 ~sQ0_spl|~sQ1_spl|sQ13_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f119,f123,f126,f173])).
% 0.13/0.42 fof(f177,plain,(
% 0.13/0.42 ![X2,X1]: (~aElement0(X2)|~aRewritingSystem0(X1)|~aElement0(X2)|sdtmndtasgtdt0(X2,X1,X2))),
% 0.13/0.42 inference(destructive_equality_resolution,[status(thm)],[f46])).
% 0.13/0.42 fof(f178,plain,(
% 0.13/0.42 ![X0,X1]: (~aElement0(X0)|~aRewritingSystem0(X1)|sdtmndtasgtdt0(X0,X1,X0))),
% 0.13/0.42 inference(duplicate_literals_removal,[status(thm)],[f177])).
% 0.13/0.42 fof(f189,plain,(
% 0.13/0.42 ~sdtmndtasgtdt0(xb,xR,xb)|~sdtmndtasgtdt0(xc,xR,xb)),
% 0.13/0.42 inference(resolution,[status(thm)],[f99,f122])).
% 0.13/0.42 fof(f190,definition,(
% 0.13/0.42 sQ16_spl <=> (sdtmndtasgtdt0(xb,xR,xb))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f192,plain,(
% 0.13/0.42 ~sdtmndtasgtdt0(xb,xR,xb)|sQ16_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f190])).
% 0.13/0.42 fof(f193,definition,(
% 0.13/0.42 sQ17_spl <=> (sdtmndtasgtdt0(xc,xR,xb))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f195,plain,(
% 0.13/0.42 ~sdtmndtasgtdt0(xc,xR,xb)|sQ17_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f193])).
% 0.13/0.42 fof(f196,plain,(
% 0.13/0.42 ~sQ16_spl|~sQ17_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f189,f190,f193])).
% 0.13/0.42 fof(f198,plain,(
% 0.13/0.42 ~sdtmndtasgtdt0(xb,xR,xc)|~sdtmndtasgtdt0(xc,xR,xc)),
% 0.13/0.42 inference(resolution,[status(thm)],[f100,f122])).
% 0.13/0.42 fof(f199,definition,(
% 0.13/0.42 sQ18_spl <=> (sdtmndtasgtdt0(xb,xR,xc))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f201,plain,(
% 0.13/0.42 ~sdtmndtasgtdt0(xb,xR,xc)|sQ18_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f199])).
% 0.13/0.42 fof(f202,definition,(
% 0.13/0.42 sQ19_spl <=> (sdtmndtasgtdt0(xc,xR,xc))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f204,plain,(
% 0.13/0.42 ~sdtmndtasgtdt0(xc,xR,xc)|sQ19_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f202])).
% 0.13/0.42 fof(f205,plain,(
% 0.13/0.42 ~sQ18_spl|~sQ19_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f198,f199,f202])).
% 0.13/0.42 fof(f212,plain,(
% 0.13/0.42 ![X0]: (~aElement0(X0)|sdtmndtasgtdt0(X0,xR,X0))),
% 0.13/0.42 inference(resolution,[status(thm)],[f178,f95])).
% 0.13/0.42 fof(f213,plain,(
% 0.13/0.42 ~aElement0(xb)|sQ16_spl),
% 0.13/0.42 inference(resolution,[status(thm)],[f212,f192])).
% 0.13/0.42 fof(f214,plain,(
% 0.13/0.42 $false|sQ16_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f213,f99])).
% 0.13/0.42 fof(f215,plain,(
% 0.13/0.42 sQ16_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f214])).
% 0.13/0.42 fof(f216,plain,(
% 0.13/0.42 ![X0,X1]: (~aElement0(X0)|~aElement0(X1)|~sdtmndtasgtdt0(X0,xR,X1)|X0=X1|sdtmndtplgtdt0(X0,xR,X1))),
% 0.13/0.42 inference(resolution,[status(thm)],[f45,f95])).
% 0.13/0.42 fof(f217,plain,(
% 0.13/0.42 ![X0]: (~aElement0(X0)|~sdtmndtasgtdt0(X0,xR,xc)|X0=xc|sdtmndtplgtdt0(X0,xR,xc))),
% 0.13/0.42 inference(resolution,[status(thm)],[f216,f100])).
% 0.13/0.42 fof(f218,plain,(
% 0.13/0.42 ![X0]: (~aElement0(X0)|~sdtmndtasgtdt0(X0,xR,xb)|X0=xb|sdtmndtplgtdt0(X0,xR,xb))),
% 0.13/0.42 inference(resolution,[status(thm)],[f216,f99])).
% 0.13/0.42 fof(f220,plain,(
% 0.13/0.42 ~aElement0(xa)|xa=xc|sdtmndtplgtdt0(xa,xR,xc)),
% 0.13/0.42 inference(resolution,[status(thm)],[f217,f121])).
% 0.13/0.42 fof(f222,definition,(
% 0.13/0.42 sQ20_spl <=> (aElement0(xa))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f224,plain,(
% 0.13/0.42 ~aElement0(xa)|sQ20_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f222])).
% 0.13/0.42 fof(f225,definition,(
% 0.13/0.42 sQ21_spl <=> (xa=xc)),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f226,plain,(
% 0.13/0.42 xa=xc|~sQ21_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f225])).
% 0.13/0.42 fof(f228,plain,(
% 0.13/0.42 ~sQ20_spl|sQ21_spl|sQ1_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f220,f222,f225,f126])).
% 0.13/0.42 fof(f229,definition,(
% 0.13/0.42 sQ22_spl <=> (aElement0(xc))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f231,plain,(
% 0.13/0.42 ~aElement0(xc)|sQ22_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f229])).
% 0.13/0.42 fof(f239,plain,(
% 0.13/0.42 $false|sQ22_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f231,f100])).
% 0.13/0.42 fof(f240,plain,(
% 0.13/0.42 sQ22_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f239])).
% 0.13/0.42 fof(f246,plain,(
% 0.13/0.42 sdtmndtasgtdt0(xc,xR,xb)|~sQ21_spl),
% 0.13/0.42 inference(backward_demodulation,[status(thm)],[f226,f120])).
% 0.13/0.42 fof(f247,plain,(
% 0.13/0.42 $false|sQ17_spl|~sQ21_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f246,f195])).
% 0.13/0.42 fof(f248,plain,(
% 0.13/0.42 sQ17_spl|~sQ21_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f247])).
% 0.13/0.42 fof(f266,definition,(
% 0.13/0.42 sQ27_spl <=> (aRewritingSystem0(xR))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f268,plain,(
% 0.13/0.42 ~aRewritingSystem0(xR)|sQ27_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f266])).
% 0.13/0.42 fof(f289,plain,(
% 0.13/0.42 $false|sQ20_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f224,f98])).
% 0.13/0.42 fof(f290,plain,(
% 0.13/0.42 sQ20_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f289])).
% 0.13/0.42 fof(f291,plain,(
% 0.13/0.42 $false|sQ27_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f268,f95])).
% 0.13/0.42 fof(f292,plain,(
% 0.13/0.42 sQ27_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f291])).
% 0.13/0.42 fof(f339,plain,(
% 0.13/0.42 ~aElement0(xc)|sQ19_spl),
% 0.13/0.42 inference(resolution,[status(thm)],[f204,f212])).
% 0.13/0.42 fof(f340,plain,(
% 0.13/0.42 ~sQ22_spl|sQ19_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f339,f229,f202])).
% 0.13/0.42 fof(f410,plain,(
% 0.13/0.42 ~sdtmndtasgtdt0(xa,xR,xb)|xa=xb|sdtmndtplgtdt0(xa,xR,xb)),
% 0.13/0.42 inference(resolution,[status(thm)],[f218,f98])).
% 0.13/0.42 fof(f413,definition,(
% 0.13/0.42 sQ52_spl <=> (sdtmndtasgtdt0(xa,xR,xb))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f415,plain,(
% 0.13/0.42 ~sdtmndtasgtdt0(xa,xR,xb)|sQ52_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f413])).
% 0.13/0.42 fof(f416,definition,(
% 0.13/0.42 sQ53_spl <=> (xa=xb)),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f417,plain,(
% 0.13/0.42 xa=xb|~sQ53_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f416])).
% 0.13/0.42 fof(f419,plain,(
% 0.13/0.42 ~sQ52_spl|sQ53_spl|sQ0_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f410,f413,f416,f123])).
% 0.13/0.42 fof(f434,plain,(
% 0.13/0.42 $false|sQ52_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f415,f120])).
% 0.13/0.42 fof(f435,plain,(
% 0.13/0.42 sQ52_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f434])).
% 0.13/0.42 fof(f447,plain,(
% 0.13/0.42 sdtmndtasgtdt0(xb,xR,xc)|~sQ53_spl),
% 0.13/0.42 inference(backward_demodulation,[status(thm)],[f417,f121])).
% 0.13/0.42 fof(f452,plain,(
% 0.13/0.42 $false|sQ18_spl|~sQ53_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f447,f201])).
% 0.13/0.42 fof(f453,plain,(
% 0.13/0.42 sQ18_spl|~sQ53_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f452])).
% 0.13/0.42 fof(f616,definition,(
% 0.13/0.42 sQ83_spl <=> (aElement0(sK17_skl))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f757,plain,(
% 0.13/0.42 ~aElement0(sK16_skl)|~aRewritingSystem0(xR)|aElement0(sK17_skl)|~sQ11_spl),
% 0.13/0.42 inference(resolution,[status(thm)],[f166,f88])).
% 0.13/0.42 fof(f762,plain,(
% 0.13/0.42 ~sQ8_spl|~sQ27_spl|sQ83_spl|~sQ11_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f757,f153,f266,f616,f165])).
% 0.13/0.42 fof(f781,definition,(
% 0.13/0.42 sQ105_spl <=> (aElement0(xb))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f783,plain,(
% 0.13/0.42 ~aElement0(xb)|sQ105_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f781])).
% 0.13/0.42 fof(f812,plain,(
% 0.13/0.42 $false|sQ105_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f783,f99])).
% 0.13/0.42 fof(f813,plain,(
% 0.13/0.42 sQ105_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f812])).
% 0.13/0.42 fof(f1001,definition,(
% 0.13/0.42 sQ135_spl <=> (isLocallyConfluent0(xR))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f1003,plain,(
% 0.13/0.42 ~isLocallyConfluent0(xR)|sQ135_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f1001])).
% 0.13/0.42 fof(f1008,plain,(
% 0.13/0.42 $false|sQ135_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1003,f96])).
% 0.13/0.42 fof(f1009,plain,(
% 0.13/0.42 sQ135_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f1008])).
% 0.13/0.42 fof(f1290,plain,(
% 0.13/0.42 ~aElement0(sK17_skl)|~sdtmndtasgtdt0(xb,xR,sK17_skl)|~sQ13_spl),
% 0.13/0.42 inference(resolution,[status(thm)],[f174,f122])).
% 0.13/0.42 fof(f1291,plain,(
% 0.13/0.42 ~sQ83_spl|~sQ12_spl|~sQ13_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f1290,f616,f169,f173])).
% 0.13/0.42 fof(f1292,plain,(
% 0.13/0.42 $false),
% 0.13/0.42 inference(sat_refutation,[status(thm)],[f156,f168,f172,f176,f196,f205,f215,f228,f240,f248,f290,f292,f340,f419,f435,f453,f762,f813,f1009,f1291])).
% 0.13/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.44 % Elapsed time: 0.086997 seconds
% 0.13/0.44 % CPU time: 0.425985 seconds
% 0.13/0.44 % Total memory used: 88.354 MB
% 0.13/0.44 % Net memory used: 87.923 MB
%------------------------------------------------------------------------------