%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COM018+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 : n026.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.13s 0.65s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM018+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.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 14:17:22 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.13/0.65 % Refutation found
% 0.13/0.65 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.65 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.65 fof(f14,axiom,(
% 0.13/0.65 (! [W0] :( ( aRewritingSystem0(W0)& isTerminating0(W0) )=> (! [W1] :( aElement0(W1)=> (? [W2] : aNormalFormOfIn0(W2,W1,W0) )) )) )),
% 0.13/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.65 fof(f15,hypothesis,(
% 0.13/0.65 aRewritingSystem0(xR) ),
% 0.13/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.65 fof(f16,hypothesis,(
% 0.13/0.65 ( (! [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) ) ),
% 0.13/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.65 fof(f22,hypothesis,(
% 0.13/0.65 ( 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) ) ),
% 0.13/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.65 fof(f23,conjecture,(
% 0.13/0.65 (? [W0] :( ( aElement0(W0)& ( xw = W0| aReductOfIn0(W0,xw,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xw,xR)& sdtmndtplgtdt0(W1,xR,W0) ))| sdtmndtplgtdt0(xw,xR,W0)| sdtmndtasgtdt0(xw,xR,W0) )& ~ (? [W1] : aReductOfIn0(W1,W0,xR) ))| aNormalFormOfIn0(W0,xw,xR) ) )),
% 0.13/0.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.65 fof(f24,negated_conjecture,(
% 0.13/0.65 ~((? [W0] :( ( aElement0(W0)& ( xw = W0| aReductOfIn0(W0,xw,xR)| (? [W1] :( aElement0(W1)& aReductOfIn0(W1,xw,xR)& sdtmndtplgtdt0(W1,xR,W0) ))| sdtmndtplgtdt0(xw,xR,W0)| sdtmndtasgtdt0(xw,xR,W0) )& ~ (? [W1] : aReductOfIn0(W1,W0,xR) ))| aNormalFormOfIn0(W0,xw,xR) ) ))),
% 0.13/0.65 inference(negated_conjecture,[status(cth)],[f23])).
% 0.13/0.65 fof(f96,plain,(
% 0.13/0.65 ![W0]: ((~aRewritingSystem0(W0)|~isTerminating0(W0))|(![W1]: (~aElement0(W1)|(?[W2]: aNormalFormOfIn0(W2,W1,W0)))))),
% 0.13/0.65 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.13/0.65 fof(f97,plain,(
% 0.13/0.65 ![W0]: ((~aRewritingSystem0(W0)|~isTerminating0(W0))|(![W1]: (~aElement0(W1)|aNormalFormOfIn0(sK12_skl(W1,W0),W1,W0))))),
% 0.13/0.65 inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(W2,sK12_skl(W1,W0))],[f96])).
% 0.13/0.65 fof(f98,plain,(
% 0.13/0.65 ![X0,X1]: (~aRewritingSystem0(X0)|~isTerminating0(X0)|~aElement0(X1)|aNormalFormOfIn0(sK12_skl(X1,X0),X1,X0))),
% 0.13/0.65 inference(cnf_transformation,[status(thm)],[f97])).
% 0.13/0.65 fof(f99,plain,(
% 0.13/0.65 aRewritingSystem0(xR)),
% 0.13/0.65 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.65 fof(f100,plain,(
% 0.13/0.65 (((![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)),
% 0.13/0.65 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.13/0.65 fof(f101,plain,(
% 0.13/0.65 (((![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)),
% 0.13/0.66 inference(miniscoping,[status(thm)],[f100])).
% 0.13/0.66 fof(f102,plain,(
% 0.13/0.66 (((![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)),
% 0.13/0.66 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))],[f101])).
% 0.13/0.66 fof(f118,plain,(
% 0.13/0.66 isTerminating0(xR)),
% 0.13/0.66 inference(cnf_transformation,[status(thm)],[f102])).
% 0.13/0.66 fof(f206,plain,(
% 0.13/0.66 (((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)),
% 0.13/0.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(W0,sK23_skl),skolemize(W0,sK24_skl)],[f22])).
% 0.13/0.66 fof(f207,plain,(
% 0.13/0.66 aElement0(xw)),
% 0.13/0.66 inference(cnf_transformation,[status(thm)],[f206])).
% 0.13/0.66 fof(f218,plain,(
% 0.13/0.66 (![W0]: (((~aElement0(W0)|((((~xw=W0&~aReductOfIn0(W0,xw,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xw,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xw,xR,W0))&~sdtmndtasgtdt0(xw,xR,W0)))|(?[W1]: aReductOfIn0(W1,W0,xR)))&~aNormalFormOfIn0(W0,xw,xR)))),
% 0.13/0.66 inference(pre_NNF_transformation,[status(thm)],[f24])).
% 0.13/0.66 fof(f219,plain,(
% 0.13/0.66 (![W0]: ((~aElement0(W0)|((((~xw=W0&~aReductOfIn0(W0,xw,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xw,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xw,xR,W0))&~sdtmndtasgtdt0(xw,xR,W0)))|(?[W1]: aReductOfIn0(W1,W0,xR))))&(![W0]: ~aNormalFormOfIn0(W0,xw,xR))),
% 0.13/0.66 inference(miniscoping,[status(thm)],[f218])).
% 0.13/0.66 fof(f220,plain,(
% 0.13/0.66 (![W0]: ((~aElement0(W0)|((((~xw=W0&~aReductOfIn0(W0,xw,xR))&(![W1]: ((~aElement0(W1)|~aReductOfIn0(W1,xw,xR))|~sdtmndtplgtdt0(W1,xR,W0))))&~sdtmndtplgtdt0(xw,xR,W0))&~sdtmndtasgtdt0(xw,xR,W0)))|aReductOfIn0(sK25_skl(W0),W0,xR)))&(![W0]: ~aNormalFormOfIn0(W0,xw,xR))),
% 0.13/0.66 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(W1,sK25_skl(W0))],[f219])).
% 0.13/0.66 fof(f226,plain,(
% 0.13/0.66 ![X0]: (~aNormalFormOfIn0(X0,xw,xR))),
% 0.13/0.66 inference(cnf_transformation,[status(thm)],[f220])).
% 0.13/0.66 fof(f1581,plain,(
% 0.13/0.66 ![X0]: (~aRewritingSystem0(xR)|~aElement0(X0)|aNormalFormOfIn0(sK12_skl(X0,xR),X0,xR))),
% 0.13/0.66 inference(resolution,[status(thm)],[f98,f118])).
% 0.13/0.66 fof(f1582,plain,(
% 0.13/0.66 ![X0]: (~aElement0(X0)|aNormalFormOfIn0(sK12_skl(X0,xR),X0,xR))),
% 0.13/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1581,f99])).
% 0.13/0.66 fof(f1740,plain,(
% 0.13/0.66 aNormalFormOfIn0(sK12_skl(xw,xR),xw,xR)),
% 0.13/0.66 inference(resolution,[status(thm)],[f1582,f207])).
% 0.13/0.66 fof(f1743,plain,(
% 0.13/0.66 $false),
% 0.13/0.66 inference(forward_subsumption_resolution,[status(thm)],[f1740,f226])).
% 0.13/0.66 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.69 % Elapsed time: 0.311288 seconds
% 0.13/0.69 % CPU time: 2.114694 seconds
% 0.13/0.69 % Total memory used: 102.861 MB
% 0.13/0.69 % Net memory used: 100.260 MB
%------------------------------------------------------------------------------