%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : COM020+1 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Jul 24 10:54:56 AM UTC 2025
% Result : Theorem 17.14s 2.50s
% Output : CNFRefutation 17.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 13
% Syntax : Number of formulae : 138 ( 91 unt; 0 def)
% Number of atoms : 328 ( 0 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 339 ( 149 ~; 146 |; 30 &)
% ( 3 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-3 aty)
% Number of variables : 53 ( 0 sgn 19 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__,plain,
? [W0] :
( aElement0(W0)
& sdtmndtasgtdt0(xb,xR,W0)
& sdtmndtasgtdt0(xd,xR,W0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(m___negated,plain,
~ ? [W0] :
( aElement0(W0)
& sdtmndtasgtdt0(xb,xR,W0)
& sdtmndtasgtdt0(xd,xR,W0) ),
inference(negate_conjecture,[status(cth)],[m__]) ).
cnf(60,plain,
( ~ sdtmndtasgtdt0(xb,xR,X0)
| ~ sdtmndtasgtdt0(xd,xR,X0)
| ~ aElement0(X0) ),
inference(cnf,[status(esa)],[m___negated]) ).
cnf(l0,plain,
( ~ sdtmndtasgtdt0(xb,xR,sK17(xu,xd,xb))
| ~ sdtmndtasgtdt0(xd,xR,sK17(xu,xd,xb))
| ~ aElement0(sK17(xu,xd,xb)) ),
inference(instantiation,[status(thm)],[60]) ).
fof(m__715,plain,
! [W0,W1,W2] :
( ( aElement0(W0)
& aElement0(W1)
& aElement0(W2)
& sdtmndtasgtdt0(W0,xR,W1)
& sdtmndtasgtdt0(W0,xR,W2) )
=> ( iLess0(W0,xa)
=> ? [W3] :
( aElement0(W3)
& sdtmndtasgtdt0(W1,xR,W3)
& sdtmndtasgtdt0(W2,xR,W3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__715) ).
cnf(47,plain,
( ~ iLess0(X0,xa)
| ~ sdtmndtasgtdt0(X0,xR,X1)
| ~ sdtmndtasgtdt0(X0,xR,X2)
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2)
| sdtmndtasgtdt0(X2,xR,sK17(X0,X1,X2)) ),
inference(cnf,[status(esa)],[m__715]) ).
cnf(l3,plain,
( ~ iLess0(xu,xa)
| ~ sdtmndtasgtdt0(xu,xR,xd)
| ~ sdtmndtasgtdt0(xu,xR,xb)
| ~ aElement0(xu)
| ~ aElement0(xd)
| ~ aElement0(xb)
| sdtmndtasgtdt0(xb,xR,sK17(xu,xd,xb)) ),
inference(instantiation,[status(thm)],[47]) ).
fof(m__755,plain,
( aElement0(xu)
& aReductOfIn0(xu,xa,xR)
& sdtmndtasgtdt0(xu,xR,xb) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__755) ).
cnf(50,plain,
aElement0(xu),
inference(cnf,[status(esa)],[m__755]) ).
cnf(l39,plain,
aElement0(xu),
inference(instantiation,[status(thm)],[50]) ).
cnf(46,plain,
( ~ iLess0(X0,xa)
| ~ sdtmndtasgtdt0(X0,xR,X1)
| ~ sdtmndtasgtdt0(X0,xR,X2)
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2)
| sdtmndtasgtdt0(X1,xR,sK17(X0,X1,X2)) ),
inference(cnf,[status(esa)],[m__715]) ).
cnf(l1,plain,
( ~ iLess0(xu,xa)
| ~ sdtmndtasgtdt0(xu,xR,xd)
| ~ sdtmndtasgtdt0(xu,xR,xb)
| ~ aElement0(xu)
| ~ aElement0(xd)
| ~ aElement0(xb)
| sdtmndtasgtdt0(xd,xR,sK17(xu,xd,xb)) ),
inference(instantiation,[status(thm)],[46]) ).
fof(mTCRTrans,plain,
! [W0,W1,W2,W3] :
( ( aElement0(W0)
& aRewritingSystem0(W1)
& aElement0(W2)
& aElement0(W3) )
=> ( ( sdtmndtasgtdt0(W0,W1,W2)
& sdtmndtasgtdt0(W2,W1,W3) )
=> sdtmndtasgtdt0(W0,W1,W3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mTCRTrans) ).
cnf(10,plain,
( ~ aRewritingSystem0(X0)
| ~ sdtmndtasgtdt0(X1,X0,X2)
| ~ sdtmndtasgtdt0(X2,X0,X3)
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ aElement0(X3)
| sdtmndtasgtdt0(X1,X0,X3) ),
inference(cnf,[status(esa)],[mTCRTrans]) ).
cnf(l5,plain,
( ~ aRewritingSystem0(xR)
| ~ sdtmndtasgtdt0(xu,xR,xw)
| ~ sdtmndtasgtdt0(xw,xR,xd)
| ~ aElement0(xu)
| ~ aElement0(xw)
| ~ aElement0(xd)
| sdtmndtasgtdt0(xu,xR,xd) ),
inference(instantiation,[status(thm)],[10]) ).
fof(mNFRDef,plain,
! [W0,W1] :
( ( aElement0(W0)
& aRewritingSystem0(W1) )
=> ! [W2] :
( aNormalFormOfIn0(W2,W0,W1)
<=> ( aElement0(W2)
& sdtmndtasgtdt0(W0,W1,W2)
& ~ ? [W3] : aReductOfIn0(W3,W2,W1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mNFRDef) ).
cnf(34,plain,
( ~ aRewritingSystem0(X0)
| ~ aElement0(X1)
| ~ aNormalFormOfIn0(X2,X1,X0)
| aElement0(X2) ),
inference(cnf,[status(esa)],[mNFRDef]) ).
cnf(l497,plain,
( ~ aRewritingSystem0(xR)
| ~ aElement0(xw)
| ~ aNormalFormOfIn0(xd,xw,xR)
| aElement0(xd) ),
inference(instantiation,[status(thm)],[34]) ).
fof(m__731,plain,
( aElement0(xa)
& aElement0(xb)
& aElement0(xc) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__731) ).
cnf(43,plain,
aElement0(xb),
inference(cnf,[status(esa)],[m__731]) ).
cnf(l42,plain,
aElement0(xb),
inference(instantiation,[status(thm)],[43]) ).
fof(mTermin,plain,
! [W0] :
( aRewritingSystem0(W0)
=> ( isTerminating0(W0)
<=> ! [W1,W2] :
( ( aElement0(W1)
& aElement0(W2) )
=> ( sdtmndtplgtdt0(W1,W0,W2)
=> iLess0(W2,W1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mTermin) ).
cnf(29,plain,
( ~ aRewritingSystem0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2)
| ~ sdtmndtplgtdt0(X1,X0,X2)
| ~ isTerminating0(X0)
| iLess0(X2,X1) ),
inference(cnf,[status(esa)],[mTermin]) ).
cnf(l7,plain,
( ~ aRewritingSystem0(xR)
| ~ aElement0(xa)
| ~ aElement0(xu)
| ~ sdtmndtplgtdt0(xa,xR,xu)
| ~ isTerminating0(xR)
| iLess0(xu,xa) ),
inference(instantiation,[status(thm)],[29]) ).
fof(mReduct,plain,
! [W0,W1] :
( ( aElement0(W0)
& aRewritingSystem0(W1) )
=> ! [W2] :
( aReductOfIn0(W2,W0,W1)
=> aElement0(W2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mReduct) ).
cnf(0,plain,
( ~ aReductOfIn0(X0,X1,X2)
| ~ aRewritingSystem0(X2)
| ~ aElement0(X1)
| aElement0(X0) ),
inference(cnf,[status(esa)],[mReduct]) ).
cnf(l11,plain,
( ~ aReductOfIn0(xu,xa,xR)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xa)
| aElement0(xu) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(45,plain,
( ~ iLess0(X0,xa)
| ~ sdtmndtasgtdt0(X0,xR,X1)
| ~ sdtmndtasgtdt0(X0,xR,X2)
| ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aElement0(X2)
| aElement0(sK17(X0,X1,X2)) ),
inference(cnf,[status(esa)],[m__715]) ).
cnf(l4,plain,
( ~ iLess0(xu,xa)
| ~ sdtmndtasgtdt0(xu,xR,xd)
| ~ sdtmndtasgtdt0(xu,xR,xb)
| ~ aElement0(xu)
| ~ aElement0(xd)
| ~ aElement0(xb)
| aElement0(sK17(xu,xd,xb)) ),
inference(instantiation,[status(thm)],[45]) ).
cnf(l6,plain,
( ~ aRewritingSystem0(xR)
| ~ aElement0(xa)
| ~ aElement0(xu)
| ~ sdtmndtplgtdt0(xa,xR,xu)
| ~ isTerminating0(xR)
| iLess0(xu,xa) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(51,plain,
aReductOfIn0(xu,xa,xR),
inference(cnf,[status(esa)],[m__755]) ).
cnf(l23,plain,
aReductOfIn0(xu,xa,xR),
inference(instantiation,[status(thm)],[51]) ).
cnf(35,plain,
( ~ aRewritingSystem0(X0)
| ~ aElement0(X1)
| ~ aNormalFormOfIn0(X2,X1,X0)
| sdtmndtasgtdt0(X1,X0,X2) ),
inference(cnf,[status(esa)],[mNFRDef]) ).
cnf(l28,plain,
( ~ aRewritingSystem0(xR)
| ~ aElement0(xw)
| ~ aNormalFormOfIn0(xd,xw,xR)
| sdtmndtasgtdt0(xw,xR,xd) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(52,plain,
sdtmndtasgtdt0(xu,xR,xb),
inference(cnf,[status(esa)],[m__755]) ).
cnf(l83,plain,
sdtmndtasgtdt0(xu,xR,xb),
inference(instantiation,[status(thm)],[52]) ).
cnf(l751,plain,
aElement0(xu),
inference(instantiation,[status(thm)],[50]) ).
cnf(l717,plain,
aElement0(xu),
inference(instantiation,[status(thm)],[50]) ).
cnf(l31,plain,
aElement0(xb),
inference(instantiation,[status(thm)],[43]) ).
fof(m__656,plain,
aRewritingSystem0(xR),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__656) ).
cnf(39,plain,
aRewritingSystem0(xR),
inference(cnf,[status(esa)],[m__656]) ).
cnf(l16,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l447,plain,
aElement0(xb),
inference(instantiation,[status(thm)],[43]) ).
cnf(l38,plain,
( ~ aRewritingSystem0(xR)
| ~ aElement0(xw)
| ~ aNormalFormOfIn0(xd,xw,xR)
| aElement0(xd) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l64,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l10,plain,
( ~ aRewritingSystem0(xR)
| ~ aElement0(xw)
| ~ aNormalFormOfIn0(xd,xw,xR)
| aElement0(xd) ),
inference(instantiation,[status(thm)],[34]) ).
fof(m__818,plain,
aNormalFormOfIn0(xd,xw,xR),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__818) ).
cnf(59,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(cnf,[status(esa)],[m__818]) ).
cnf(l539,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(instantiation,[status(thm)],[59]) ).
cnf(l498,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(instantiation,[status(thm)],[59]) ).
cnf(l22,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l26,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(instantiation,[status(thm)],[59]) ).
cnf(l29,plain,
( ~ aRewritingSystem0(xR)
| ~ sdtmndtasgtdt0(xu,xR,xw)
| ~ sdtmndtasgtdt0(xw,xR,xd)
| ~ aElement0(xu)
| ~ aElement0(xw)
| ~ aElement0(xd)
| sdtmndtasgtdt0(xu,xR,xd) ),
inference(instantiation,[status(thm)],[10]) ).
fof(mTCDef,plain,
! [W0,W1,W2] :
( ( aElement0(W0)
& aRewritingSystem0(W1)
& aElement0(W2) )
=> ( sdtmndtplgtdt0(W0,W1,W2)
<=> ( aReductOfIn0(W2,W0,W1)
| ? [W3] :
( aElement0(W3)
& aReductOfIn0(W3,W0,W1)
& sdtmndtplgtdt0(W3,W1,W2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mTCDef) ).
cnf(4,plain,
( ~ aReductOfIn0(X0,X1,X2)
| ~ aRewritingSystem0(X2)
| ~ aElement0(X1)
| ~ aElement0(X0)
| sdtmndtplgtdt0(X1,X2,X0) ),
inference(cnf,[status(esa)],[mTCDef]) ).
cnf(l422,plain,
( ~ aReductOfIn0(xu,xa,xR)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xa)
| ~ aElement0(xu)
| sdtmndtplgtdt0(xa,xR,xu) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l451,plain,
( ~ aReductOfIn0(xu,xa,xR)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xa)
| aElement0(xu) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l724,plain,
aReductOfIn0(xu,xa,xR),
inference(instantiation,[status(thm)],[51]) ).
cnf(l723,plain,
aElement0(xu),
inference(instantiation,[status(thm)],[50]) ).
cnf(l24,plain,
sdtmndtasgtdt0(xu,xR,xb),
inference(instantiation,[status(thm)],[52]) ).
cnf(l476,plain,
aReductOfIn0(xu,xa,xR),
inference(instantiation,[status(thm)],[51]) ).
cnf(l35,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l166,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(42,plain,
aElement0(xa),
inference(cnf,[status(esa)],[m__731]) ).
cnf(l719,plain,
aElement0(xa),
inference(instantiation,[status(thm)],[42]) ).
fof(m__799,plain,
( aElement0(xw)
& sdtmndtasgtdt0(xu,xR,xw)
& sdtmndtasgtdt0(xv,xR,xw) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__799) ).
cnf(56,plain,
aElement0(xw),
inference(cnf,[status(esa)],[m__799]) ).
cnf(l452,plain,
aElement0(xw),
inference(instantiation,[status(thm)],[56]) ).
cnf(l722,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l188,plain,
( ~ aRewritingSystem0(xR)
| ~ aElement0(xw)
| ~ aNormalFormOfIn0(xd,xw,xR)
| sdtmndtasgtdt0(xw,xR,xd) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l399,plain,
aElement0(xa),
inference(instantiation,[status(thm)],[42]) ).
fof(m__656_01,plain,
( isLocallyConfluent0(xR)
& isTerminating0(xR) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__656_01) ).
cnf(41,plain,
isTerminating0(xR),
inference(cnf,[status(esa)],[m__656_01]) ).
cnf(l810,plain,
isTerminating0(xR),
inference(instantiation,[status(thm)],[41]) ).
cnf(57,plain,
sdtmndtasgtdt0(xu,xR,xw),
inference(cnf,[status(esa)],[m__799]) ).
cnf(l74,plain,
sdtmndtasgtdt0(xu,xR,xw),
inference(instantiation,[status(thm)],[57]) ).
cnf(l59,plain,
( ~ aRewritingSystem0(xR)
| ~ aElement0(xa)
| ~ aElement0(xu)
| ~ sdtmndtplgtdt0(xa,xR,xu)
| ~ isTerminating0(xR)
| iLess0(xu,xa) ),
inference(instantiation,[status(thm)],[29]) ).
cnf(l379,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(instantiation,[status(thm)],[59]) ).
cnf(l629,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l65,plain,
aElement0(xw),
inference(instantiation,[status(thm)],[56]) ).
cnf(l423,plain,
( ~ aReductOfIn0(xu,xa,xR)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xa)
| aElement0(xu) ),
inference(instantiation,[status(thm)],[0]) ).
cnf(l2,plain,
aElement0(xu),
inference(instantiation,[status(thm)],[50]) ).
cnf(l514,plain,
( ~ aReductOfIn0(xu,xa,xR)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xa)
| ~ aElement0(xu)
| sdtmndtplgtdt0(xa,xR,xu) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l536,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l20,plain,
aElement0(xw),
inference(instantiation,[status(thm)],[56]) ).
cnf(l551,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l524,plain,
aElement0(xu),
inference(instantiation,[status(thm)],[50]) ).
cnf(l522,plain,
aReductOfIn0(xu,xa,xR),
inference(instantiation,[status(thm)],[51]) ).
cnf(l396,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l550,plain,
aElement0(xa),
inference(instantiation,[status(thm)],[42]) ).
cnf(l640,plain,
isTerminating0(xR),
inference(instantiation,[status(thm)],[41]) ).
cnf(l18,plain,
aElement0(xa),
inference(instantiation,[status(thm)],[42]) ).
cnf(l754,plain,
( ~ aReductOfIn0(xu,xa,xR)
| ~ aRewritingSystem0(xR)
| ~ aElement0(xa)
| ~ aElement0(xu)
| sdtmndtplgtdt0(xa,xR,xu) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l99,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l14,plain,
aElement0(xu),
inference(instantiation,[status(thm)],[50]) ).
cnf(l433,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l47,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l402,plain,
aElement0(xa),
inference(instantiation,[status(thm)],[42]) ).
cnf(l450,plain,
( ~ aRewritingSystem0(xR)
| ~ aElement0(xw)
| ~ aNormalFormOfIn0(xd,xw,xR)
| aElement0(xd) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l775,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l515,plain,
aElement0(xa),
inference(instantiation,[status(thm)],[42]) ).
cnf(l630,plain,
aElement0(xw),
inference(instantiation,[status(thm)],[56]) ).
cnf(l404,plain,
aElement0(xw),
inference(instantiation,[status(thm)],[56]) ).
cnf(l521,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l746,plain,
isTerminating0(xR),
inference(instantiation,[status(thm)],[41]) ).
cnf(l15,plain,
( ~ aRewritingSystem0(xR)
| ~ sdtmndtasgtdt0(xu,xR,xw)
| ~ sdtmndtasgtdt0(xw,xR,xd)
| ~ aElement0(xu)
| ~ aElement0(xw)
| ~ aElement0(xd)
| sdtmndtasgtdt0(xu,xR,xd) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l58,plain,
sdtmndtasgtdt0(xu,xR,xw),
inference(instantiation,[status(thm)],[57]) ).
cnf(l523,plain,
aReductOfIn0(xu,xa,xR),
inference(instantiation,[status(thm)],[51]) ).
cnf(l755,plain,
aElement0(xa),
inference(instantiation,[status(thm)],[42]) ).
cnf(l446,plain,
( ~ aRewritingSystem0(xR)
| ~ aElement0(xw)
| ~ aNormalFormOfIn0(xd,xw,xR)
| aElement0(xd) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l19,plain,
aElement0(xu),
inference(instantiation,[status(thm)],[50]) ).
cnf(l615,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l30,plain,
( ~ aRewritingSystem0(xR)
| ~ aElement0(xw)
| ~ aNormalFormOfIn0(xd,xw,xR)
| sdtmndtasgtdt0(xw,xR,xd) ),
inference(instantiation,[status(thm)],[35]) ).
cnf(l63,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(instantiation,[status(thm)],[59]) ).
cnf(l242,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(instantiation,[status(thm)],[59]) ).
cnf(l17,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l756,plain,
aReductOfIn0(xu,xa,xR),
inference(instantiation,[status(thm)],[51]) ).
cnf(l81,plain,
aElement0(xa),
inference(instantiation,[status(thm)],[42]) ).
cnf(l425,plain,
aElement0(xa),
inference(instantiation,[status(thm)],[42]) ).
cnf(l117,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l189,plain,
aElement0(xw),
inference(instantiation,[status(thm)],[56]) ).
cnf(l696,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(instantiation,[status(thm)],[59]) ).
cnf(l70,plain,
aElement0(xw),
inference(instantiation,[status(thm)],[56]) ).
cnf(l37,plain,
sdtmndtasgtdt0(xu,xR,xw),
inference(instantiation,[status(thm)],[57]) ).
cnf(l345,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l467,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(instantiation,[status(thm)],[59]) ).
cnf(l113,plain,
aElement0(xw),
inference(instantiation,[status(thm)],[56]) ).
cnf(l927,plain,
aElement0(xu),
inference(instantiation,[status(thm)],[50]) ).
cnf(l502,plain,
aElement0(xw),
inference(instantiation,[status(thm)],[56]) ).
cnf(l195,plain,
( ~ aRewritingSystem0(xR)
| ~ aElement0(xw)
| ~ aNormalFormOfIn0(xd,xw,xR)
| aElement0(xd) ),
inference(instantiation,[status(thm)],[34]) ).
cnf(l196,plain,
aNormalFormOfIn0(xd,xw,xR),
inference(instantiation,[status(thm)],[59]) ).
cnf(l471,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(l592,plain,
aElement0(xw),
inference(instantiation,[status(thm)],[56]) ).
cnf(l198,plain,
aElement0(xw),
inference(instantiation,[status(thm)],[56]) ).
cnf(l240,plain,
aElement0(xw),
inference(instantiation,[status(thm)],[56]) ).
cnf(l41,plain,
sdtmndtasgtdt0(xu,xR,xb),
inference(instantiation,[status(thm)],[52]) ).
cnf(l199,plain,
aRewritingSystem0(xR),
inference(instantiation,[status(thm)],[39]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l3,l39,l1,l5,l497,l42,l7,l11,l4,l6,l23,l28,l83,l751,l717,l31,l16,l447,l38,l64,l10,l539,l498,l22,l26,l29,l422,l451,l724,l723,l24,l476,l35,l166,l719,l452,l722,l188,l399,l810,l74,l59,l379,l629,l65,l423,l2,l514,l536,l20,l551,l524,l522,l396,l550,l640,l18,l754,l99,l14,l433,l47,l402,l450,l775,l515,l630,l404,l521,l746,l15,l58,l523,l755,l446,l19,l615,l30,l63,l242,l17,l756,l81,l425,l117,l189,l696,l70,l37,l345,l467,l113,l927,l502,l195,l196,l471,l592,l198,l240,l41,l199]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : COM020+1 : TPTP v9.0.0. Released v4.0.0.
% 0.03/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n018.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Sun Jul 20 06:10:04 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 3
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 6
% 0.12/0.34 % launching worker at depth: 7
% 0.12/0.34 % launching worker at depth: 4
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % launching worker at depth: 10
% 1.92/0.56 % launching worker at depth: 11
% 17.14/2.50 % SZS status Theorem for theBenchmark
% 17.14/2.50 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------