%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM017+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 : 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 0.18s 1.05s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM017+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.12/0.98 % Computer : n010.cluster.edu
% 0.12/0.98 % Model : x86_64 x86_64
% 0.12/0.98 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.98 % Memory : 8046.5625MB
% 0.12/0.98 % OS : Linux 6.8.0-71-generic
% 0.12/0.98 % CPULimit : 300
% 0.12/0.98 % WCLimit : 300
% 0.12/0.98 % DateTime : Mon Sep 21 14:14:42 UTC 2026
% 0.12/0.98 % CPUTime :
% 0.12/1.00 % Drodi V4.1.1
% 0.18/1.05 % Refutation found
% 0.18/1.05 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.18/1.05 % SZS output start CNFRefutation for theBenchmark
% 0.18/1.05 fof(f3,axiom,(
% 0.18/1.05 (! [W0,W1] :( ( aElement0(W0)& aRewritingSystem0(W1) )=> (! [W2] :( aReductOfIn0(W2,W0,W1)=> aElement0(W2) ) )) )),
% 0.18/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/1.05 fof(f11,definition,(
% 0.18/1.05 (! [W0] :( aRewritingSystem0(W0)=> ( isLocallyConfluent0(W0)<=> (! [W1,W2,W3] :( ( aElement0(W1)& aElement0(W2)& aElement0(W3)& aReductOfIn0(W2,W1,W0)& aReductOfIn0(W3,W1,W0) )=> (? [W4] :( aElement0(W4)& sdtmndtasgtdt0(W2,W0,W4)& sdtmndtasgtdt0(W3,W0,W4) ) )) )) ) )),
% 0.18/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/1.05 fof(f15,hypothesis,(
% 0.18/1.05 aRewritingSystem0(xR) ),
% 0.18/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/1.05 fof(f16,hypothesis,(
% 0.18/1.05 ( isLocallyConfluent0(xR)& isTerminating0(xR) ) ),
% 0.18/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/1.05 fof(f17,hypothesis,(
% 0.18/1.05 ( aElement0(xa)& aElement0(xb)& aElement0(xc) ) ),
% 0.18/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/1.05 fof(f20,hypothesis,(
% 0.18/1.05 ( aElement0(xu)& aReductOfIn0(xu,xa,xR)& sdtmndtasgtdt0(xu,xR,xb) ) ),
% 0.18/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/1.05 fof(f21,hypothesis,(
% 0.18/1.05 ( aElement0(xv)& aReductOfIn0(xv,xa,xR)& sdtmndtasgtdt0(xv,xR,xc) ) ),
% 0.18/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/1.05 fof(f22,conjecture,(
% 0.18/1.05 (? [W0] :( aElement0(W0)& sdtmndtasgtdt0(xu,xR,W0)& sdtmndtasgtdt0(xv,xR,W0) ) )),
% 0.18/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.18/1.05 fof(f23,negated_conjecture,(
% 0.18/1.05 ~((? [W0] :( aElement0(W0)& sdtmndtasgtdt0(xu,xR,W0)& sdtmndtasgtdt0(xv,xR,W0) ) ))),
% 0.18/1.05 inference(negated_conjecture,[status(cth)],[f22])).
% 0.18/1.05 fof(f30,plain,(
% 0.18/1.05 ![W0,W1]: ((~aElement0(W0)|~aRewritingSystem0(W1))|(![W2]: (~aReductOfIn0(W2,W0,W1)|aElement0(W2))))),
% 0.18/1.05 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.18/1.05 fof(f31,plain,(
% 0.18/1.05 ![X0,X1,X2]: (~aElement0(X0)|~aRewritingSystem0(X1)|~aReductOfIn0(X2,X0,X1)|aElement0(X2))),
% 0.18/1.05 inference(cnf_transformation,[status(thm)],[f30])).
% 0.18/1.05 fof(f66,plain,(
% 0.18/1.05 ![W0]: (~aRewritingSystem0(W0)|(isLocallyConfluent0(W0)<=>(![W1,W2,W3]: (((((~aElement0(W1)|~aElement0(W2))|~aElement0(W3))|~aReductOfIn0(W2,W1,W0))|~aReductOfIn0(W3,W1,W0))|(?[W4]: ((aElement0(W4)&sdtmndtasgtdt0(W2,W0,W4))&sdtmndtasgtdt0(W3,W0,W4)))))))),
% 0.18/1.05 inference(pre_NNF_transformation,[status(thm)],[f11])).
% 0.18/1.05 fof(f67,plain,(
% 0.18/1.05 ![W0]: (~aRewritingSystem0(W0)|((~isLocallyConfluent0(W0)|(![W1,W2,W3]: (((((~aElement0(W1)|~aElement0(W2))|~aElement0(W3))|~aReductOfIn0(W2,W1,W0))|~aReductOfIn0(W3,W1,W0))|(?[W4]: ((aElement0(W4)&sdtmndtasgtdt0(W2,W0,W4))&sdtmndtasgtdt0(W3,W0,W4))))))&(isLocallyConfluent0(W0)|(?[W1,W2,W3]: (((((aElement0(W1)&aElement0(W2))&aElement0(W3))&aReductOfIn0(W2,W1,W0))&aReductOfIn0(W3,W1,W0))&(![W4]: ((~aElement0(W4)|~sdtmndtasgtdt0(W2,W0,W4))|~sdtmndtasgtdt0(W3,W0,W4))))))))),
% 0.18/1.05 inference(NNF_transformation,[status(thm)],[f66])).
% 0.18/1.05 fof(f68,plain,(
% 0.18/1.05 ![W0]: (~aRewritingSystem0(W0)|((~isLocallyConfluent0(W0)|(![W2,W3]: ((![W1]: ((((~aElement0(W1)|~aElement0(W2))|~aElement0(W3))|~aReductOfIn0(W2,W1,W0))|~aReductOfIn0(W3,W1,W0)))|(?[W4]: ((aElement0(W4)&sdtmndtasgtdt0(W2,W0,W4))&sdtmndtasgtdt0(W3,W0,W4))))))&(isLocallyConfluent0(W0)|(?[W2,W3]: ((?[W1]: ((((aElement0(W1)&aElement0(W2))&aElement0(W3))&aReductOfIn0(W2,W1,W0))&aReductOfIn0(W3,W1,W0)))&(![W4]: ((~aElement0(W4)|~sdtmndtasgtdt0(W2,W0,W4))|~sdtmndtasgtdt0(W3,W0,W4))))))))),
% 0.18/1.05 inference(miniscoping,[status(thm)],[f67])).
% 0.18/1.05 fof(f69,plain,(
% 0.18/1.05 ![W0]: (~aRewritingSystem0(W0)|((~isLocallyConfluent0(W0)|(![W2,W3]: ((![W1]: ((((~aElement0(W1)|~aElement0(W2))|~aElement0(W3))|~aReductOfIn0(W2,W1,W0))|~aReductOfIn0(W3,W1,W0)))|((aElement0(sK5_skl(W3,W2,W0))&sdtmndtasgtdt0(W2,W0,sK5_skl(W3,W2,W0)))&sdtmndtasgtdt0(W3,W0,sK5_skl(W3,W2,W0))))))&(isLocallyConfluent0(W0)|(((((aElement0(sK8_skl(W0))&aElement0(sK6_skl(W0)))&aElement0(sK7_skl(W0)))&aReductOfIn0(sK6_skl(W0),sK8_skl(W0),W0))&aReductOfIn0(sK7_skl(W0),sK8_skl(W0),W0))&(![W4]: ((~aElement0(W4)|~sdtmndtasgtdt0(sK6_skl(W0),W0,W4))|~sdtmndtasgtdt0(sK7_skl(W0),W0,W4)))))))),
% 0.18/1.05 inference(skolemize,[status(esa),new_symbols(skolem,[sK5_skl,sK6_skl,sK7_skl,sK8_skl]),skolemize(W4,sK5_skl(W3,W2,W0)),skolemize(W2,sK6_skl(W0)),skolemize(W3,sK7_skl(W0)),skolemize(W1,sK8_skl(W0))],[f68])).
% 0.18/1.05 fof(f70,plain,(
% 0.18/1.05 ![X0,X1,X2,X3]: (~aRewritingSystem0(X0)|~isLocallyConfluent0(X0)|~aElement0(X1)|~aElement0(X2)|~aElement0(X3)|~aReductOfIn0(X2,X1,X0)|~aReductOfIn0(X3,X1,X0)|aElement0(sK5_skl(X3,X2,X0)))),
% 0.18/1.05 inference(cnf_transformation,[status(thm)],[f69])).
% 0.18/1.05 fof(f71,plain,(
% 0.18/1.05 ![X0,X1,X2,X3]: (~aRewritingSystem0(X0)|~isLocallyConfluent0(X0)|~aElement0(X1)|~aElement0(X2)|~aElement0(X3)|~aReductOfIn0(X2,X1,X0)|~aReductOfIn0(X3,X1,X0)|sdtmndtasgtdt0(X2,X0,sK5_skl(X3,X2,X0)))),
% 0.18/1.05 inference(cnf_transformation,[status(thm)],[f69])).
% 0.18/1.05 fof(f72,plain,(
% 0.18/1.05 ![X0,X1,X2,X3]: (~aRewritingSystem0(X0)|~isLocallyConfluent0(X0)|~aElement0(X1)|~aElement0(X2)|~aElement0(X3)|~aReductOfIn0(X2,X1,X0)|~aReductOfIn0(X3,X1,X0)|sdtmndtasgtdt0(X3,X0,sK5_skl(X3,X2,X0)))),
% 0.18/1.05 inference(cnf_transformation,[status(thm)],[f69])).
% 0.18/1.05 fof(f98,plain,(
% 0.18/1.05 aRewritingSystem0(xR)),
% 0.18/1.05 inference(cnf_transformation,[status(thm)],[f15])).
% 0.18/1.05 fof(f99,plain,(
% 0.18/1.05 isLocallyConfluent0(xR)),
% 0.18/1.05 inference(cnf_transformation,[status(thm)],[f16])).
% 0.18/1.05 fof(f101,plain,(
% 0.18/1.05 aElement0(xa)),
% 0.18/1.05 inference(cnf_transformation,[status(thm)],[f17])).
% 0.18/1.05 fof(f103,plain,(
% 0.18/1.05 aElement0(xc)),
% 0.18/1.05 inference(cnf_transformation,[status(thm)],[f17])).
% 0.18/1.05 fof(f112,plain,(
% 0.18/1.05 aReductOfIn0(xu,xa,xR)),
% 0.18/1.05 inference(cnf_transformation,[status(thm)],[f20])).
% 0.18/1.05 fof(f115,plain,(
% 0.18/1.05 aReductOfIn0(xv,xa,xR)),
% 0.18/1.05 inference(cnf_transformation,[status(thm)],[f21])).
% 0.18/1.05 fof(f117,plain,(
% 0.18/1.05 (![W0]: ((~aElement0(W0)|~sdtmndtasgtdt0(xu,xR,W0))|~sdtmndtasgtdt0(xv,xR,W0)))),
% 0.18/1.05 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.18/1.05 fof(f118,plain,(
% 0.18/1.05 ![X0]: (~aElement0(X0)|~sdtmndtasgtdt0(xu,xR,X0)|~sdtmndtasgtdt0(xv,xR,X0))),
% 0.18/1.05 inference(cnf_transformation,[status(thm)],[f117])).
% 0.18/1.05 fof(f123,plain,(
% 0.18/1.05 ![X0,X1,X2,X3]: (~aRewritingSystem0(X0)|~isLocallyConfluent0(X0)|~aElement0(X1)|~aElement0(X2)|~aReductOfIn0(X3,X1,X0)|~aReductOfIn0(X2,X1,X0)|aElement0(sK5_skl(X2,X3,X0)))),
% 0.18/1.05 inference(forward_subsumption_resolution,[status(thm)],[f70,f31])).
% 0.18/1.05 fof(f124,plain,(
% 0.18/1.05 ![X0,X1,X2,X3]: (~aRewritingSystem0(X0)|~isLocallyConfluent0(X0)|~aElement0(X1)|~aElement0(X2)|~aReductOfIn0(X3,X1,X0)|~aReductOfIn0(X2,X1,X0)|sdtmndtasgtdt0(X3,X0,sK5_skl(X2,X3,X0)))),
% 0.18/1.05 inference(forward_subsumption_resolution,[status(thm)],[f71,f31])).
% 0.18/1.05 fof(f125,plain,(
% 0.18/1.05 ![X0,X1,X2,X3]: (~aRewritingSystem0(X0)|~isLocallyConfluent0(X0)|~aElement0(X1)|~aElement0(X2)|~aReductOfIn0(X3,X1,X0)|~aReductOfIn0(X2,X1,X0)|sdtmndtasgtdt0(X2,X0,sK5_skl(X2,X3,X0)))),
% 0.18/1.05 inference(forward_subsumption_resolution,[status(thm)],[f72,f31])).
% 0.18/1.05 fof(f131,plain,(
% 0.18/1.05 ~aElement0(xa)|~aRewritingSystem0(xR)|aElement0(xu)),
% 0.18/1.05 inference(resolution,[status(thm)],[f31,f112])).
% 0.18/1.05 fof(f132,definition,(
% 0.18/1.05 sQ0_spl <=> (aElement0(xa))),
% 0.18/1.05 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.18/1.05 fof(f134,plain,(
% 0.18/1.05 ~aElement0(xa)|sQ0_spl),
% 0.18/1.05 inference(component_clause,[status(thm)],[f132])).
% 0.18/1.05 fof(f135,definition,(
% 0.18/1.05 sQ1_spl <=> (aRewritingSystem0(xR))),
% 0.18/1.05 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.18/1.05 fof(f137,plain,(
% 0.18/1.05 ~aRewritingSystem0(xR)|sQ1_spl),
% 0.18/1.05 inference(component_clause,[status(thm)],[f135])).
% 0.18/1.05 fof(f142,definition,(
% 0.18/1.05 sQ3_spl <=> (aElement0(xu))),
% 0.18/1.05 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.18/1.05 fof(f145,plain,(
% 0.18/1.05 ~sQ0_spl|~sQ1_spl|sQ3_spl),
% 0.18/1.05 inference(split_clause,[status(thm)],[f131,f132,f135,f142])).
% 0.18/1.05 fof(f146,plain,(
% 0.18/1.05 $false|sQ1_spl),
% 0.18/1.05 inference(forward_subsumption_resolution,[status(thm)],[f137,f98])).
% 0.18/1.05 fof(f147,plain,(
% 0.18/1.05 sQ1_spl),
% 0.18/1.05 inference(contradiction_clause,[status(thm)],[f146])).
% 0.18/1.05 fof(f148,plain,(
% 0.18/1.05 $false|sQ0_spl),
% 0.18/1.05 inference(forward_subsumption_resolution,[status(thm)],[f134,f101])).
% 0.18/1.05 fof(f149,plain,(
% 0.18/1.05 sQ0_spl),
% 0.18/1.05 inference(contradiction_clause,[status(thm)],[f148])).
% 0.18/1.05 fof(f189,definition,(
% 0.18/1.05 sQ12_spl <=> (isLocallyConfluent0(xR))),
% 0.18/1.05 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.18/1.05 fof(f191,plain,(
% 0.18/1.05 ~isLocallyConfluent0(xR)|sQ12_spl),
% 0.18/1.05 inference(component_clause,[status(thm)],[f189])).
% 0.18/1.05 fof(f957,plain,(
% 0.18/1.05 ![X0]: (~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|~aElement0(X0)|~aReductOfIn0(X0,xa,xR)|aElement0(sK5_skl(X0,xv,xR)))),
% 0.18/1.05 inference(resolution,[status(thm)],[f123,f115])).
% 0.18/1.05 fof(f959,definition,(
% 0.18/1.05 ![X0]: (sQ154_spl <=> (~aElement0(X0)|~aReductOfIn0(X0,xa,xR)|aElement0(sK5_skl(X0,xv,xR))))),
% 0.18/1.05 introduced(definition,[new_symbols(definition,[sQ154_spl])],[split_symbol_definition])).
% 0.18/1.05 fof(f960,plain,(
% 0.18/1.05 ![X0]: (~aElement0(X0)|~aReductOfIn0(X0,xa,xR)|aElement0(sK5_skl(X0,xv,xR))|~sQ154_spl)),
% 0.18/1.05 inference(component_clause,[status(thm)],[f959])).
% 0.18/1.05 fof(f962,plain,(
% 0.18/1.05 ~sQ1_spl|~sQ12_spl|~sQ0_spl|sQ154_spl),
% 0.18/1.05 inference(split_clause,[status(thm)],[f957,f135,f189,f132,f959])).
% 0.18/1.05 fof(f967,plain,(
% 0.18/1.05 $false|sQ12_spl),
% 0.18/1.05 inference(forward_subsumption_resolution,[status(thm)],[f191,f99])).
% 0.18/1.05 fof(f968,plain,(
% 0.18/1.05 sQ12_spl),
% 0.18/1.05 inference(contradiction_clause,[status(thm)],[f967])).
% 0.18/1.05 fof(f969,plain,(
% 0.18/1.05 ![X0]: (~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|~aElement0(X0)|~aReductOfIn0(X0,xa,xR)|sdtmndtasgtdt0(xv,xR,sK5_skl(X0,xv,xR)))),
% 0.18/1.05 inference(resolution,[status(thm)],[f124,f115])).
% 0.18/1.05 fof(f971,definition,(
% 0.18/1.05 ![X0]: (sQ156_spl <=> (~aElement0(X0)|~aReductOfIn0(X0,xa,xR)|sdtmndtasgtdt0(xv,xR,sK5_skl(X0,xv,xR))))),
% 0.18/1.05 introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition])).
% 0.18/1.05 fof(f972,plain,(
% 0.18/1.05 ![X0]: (~aElement0(X0)|~aReductOfIn0(X0,xa,xR)|sdtmndtasgtdt0(xv,xR,sK5_skl(X0,xv,xR))|~sQ156_spl)),
% 0.18/1.05 inference(component_clause,[status(thm)],[f971])).
% 0.18/1.05 fof(f974,plain,(
% 0.18/1.05 ~sQ1_spl|~sQ12_spl|~sQ0_spl|sQ156_spl),
% 0.18/1.05 inference(split_clause,[status(thm)],[f969,f135,f189,f132,f971])).
% 0.18/1.05 fof(f979,plain,(
% 0.18/1.05 ![X0]: (~aRewritingSystem0(xR)|~isLocallyConfluent0(xR)|~aElement0(xa)|~aElement0(X0)|~aReductOfIn0(X0,xa,xR)|sdtmndtasgtdt0(X0,xR,sK5_skl(X0,xv,xR)))),
% 0.18/1.05 inference(resolution,[status(thm)],[f125,f115])).
% 0.18/1.05 fof(f981,definition,(
% 0.18/1.05 ![X0]: (sQ158_spl <=> (~aElement0(X0)|~aReductOfIn0(X0,xa,xR)|sdtmndtasgtdt0(X0,xR,sK5_skl(X0,xv,xR))))),
% 0.18/1.05 introduced(definition,[new_symbols(definition,[sQ158_spl])],[split_symbol_definition])).
% 0.18/1.05 fof(f982,plain,(
% 0.18/1.05 ![X0]: (~aElement0(X0)|~aReductOfIn0(X0,xa,xR)|sdtmndtasgtdt0(X0,xR,sK5_skl(X0,xv,xR))|~sQ158_spl)),
% 0.18/1.05 inference(component_clause,[status(thm)],[f981])).
% 0.18/1.05 fof(f984,plain,(
% 0.18/1.05 ~sQ1_spl|~sQ12_spl|~sQ0_spl|sQ158_spl),
% 0.18/1.05 inference(split_clause,[status(thm)],[f979,f135,f189,f132,f981])).
% 0.18/1.05 fof(f1028,plain,(
% 0.18/1.05 ~aElement0(xu)|aElement0(sK5_skl(xu,xv,xR))|~sQ154_spl),
% 0.18/1.05 inference(resolution,[status(thm)],[f960,f112])).
% 0.18/1.05 fof(f1033,definition,(
% 0.18/1.05 sQ169_spl <=> (aElement0(sK5_skl(xu,xv,xR)))),
% 0.18/1.05 introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition])).
% 0.18/1.05 fof(f1036,plain,(
% 0.18/1.05 ~sQ3_spl|sQ169_spl|~sQ154_spl),
% 0.18/1.05 inference(split_clause,[status(thm)],[f1028,f142,f1033,f959])).
% 0.18/1.05 fof(f1048,plain,(
% 0.18/1.05 ~aElement0(xu)|sdtmndtasgtdt0(xv,xR,sK5_skl(xu,xv,xR))|~sQ156_spl),
% 0.18/1.05 inference(resolution,[status(thm)],[f972,f112])).
% 0.18/1.05 fof(f1053,definition,(
% 0.18/1.05 sQ173_spl <=> (sdtmndtasgtdt0(xv,xR,sK5_skl(xu,xv,xR)))),
% 0.18/1.05 introduced(definition,[new_symbols(definition,[sQ173_spl])],[split_symbol_definition])).
% 0.18/1.05 fof(f1054,plain,(
% 0.18/1.05 sdtmndtasgtdt0(xv,xR,sK5_skl(xu,xv,xR))|~sQ173_spl),
% 0.18/1.05 inference(component_clause,[status(thm)],[f1053])).
% 0.18/1.05 fof(f1056,plain,(
% 0.18/1.05 ~sQ3_spl|sQ173_spl|~sQ156_spl),
% 0.18/1.05 inference(split_clause,[status(thm)],[f1048,f142,f1053,f971])).
% 0.18/1.05 fof(f1068,plain,(
% 0.18/1.05 ~aElement0(xu)|sdtmndtasgtdt0(xu,xR,sK5_skl(xu,xv,xR))|~sQ158_spl),
% 0.18/1.05 inference(resolution,[status(thm)],[f982,f112])).
% 0.18/1.05 fof(f1070,definition,(
% 0.18/1.05 sQ176_spl <=> (sdtmndtasgtdt0(xu,xR,sK5_skl(xu,xv,xR)))),
% 0.18/1.05 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 0.18/1.05 fof(f1073,plain,(
% 0.18/1.05 ~sQ3_spl|sQ176_spl|~sQ158_spl),
% 0.18/1.05 inference(split_clause,[status(thm)],[f1068,f142,f1070,f981])).
% 0.18/1.05 fof(f1087,definition,(
% 0.18/1.05 sQ178_spl <=> (aElement0(xc))),
% 0.18/1.05 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 0.18/1.05 fof(f1089,plain,(
% 0.18/1.05 ~aElement0(xc)|sQ178_spl),
% 0.18/1.05 inference(component_clause,[status(thm)],[f1087])).
% 0.18/1.05 fof(f1120,plain,(
% 0.18/1.05 $false|sQ178_spl),
% 0.18/1.05 inference(forward_subsumption_resolution,[status(thm)],[f1089,f103])).
% 0.18/1.05 fof(f1121,plain,(
% 0.18/1.05 sQ178_spl),
% 0.18/1.05 inference(contradiction_clause,[status(thm)],[f1120])).
% 0.18/1.05 fof(f1223,plain,(
% 0.18/1.05 ~aElement0(sK5_skl(xu,xv,xR))|~sdtmndtasgtdt0(xu,xR,sK5_skl(xu,xv,xR))|~sQ173_spl),
% 0.18/1.05 inference(resolution,[status(thm)],[f1054,f118])).
% 0.18/1.05 fof(f1234,plain,(
% 0.18/1.05 ~sQ169_spl|~sQ176_spl|~sQ173_spl),
% 0.18/1.05 inference(split_clause,[status(thm)],[f1223,f1033,f1070,f1053])).
% 0.18/1.05 fof(f1265,plain,(
% 0.18/1.05 $false),
% 0.18/1.05 inference(sat_refutation,[status(thm)],[f145,f147,f149,f962,f968,f974,f984,f1036,f1056,f1073,f1121,f1234])).
% 0.18/1.05 % SZS output end CNFRefutation for theBenchmark.p
% 0.18/1.07 % Elapsed time: 0.079207 seconds
% 0.18/1.07 % CPU time: 0.320592 seconds
% 0.18/1.07 % Total memory used: 85.989 MB
% 0.18/1.07 % Net memory used: 85.601 MB
%------------------------------------------------------------------------------