%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : RNG099+1 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/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 : Fri Jul 25 03:02:53 PM UTC 2025
% Result : Theorem 143.36s 18.34s
% Output : CNFRefutation 143.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 12
% Syntax : Number of formulae : 85 ( 44 unt; 0 def)
% Number of atoms : 176 ( 5 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 161 ( 70 ~; 67 |; 14 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 29 ( 0 sgn 13 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__,plain,
? [W0] :
( aElement0(W0)
& sdteqdtlpzmzozddtrp0(W0,xx,xI)
& sdteqdtlpzmzozddtrp0(W0,xy,xJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(m___negated,plain,
~ ? [W0] :
( aElement0(W0)
& sdteqdtlpzmzozddtrp0(W0,xx,xI)
& sdteqdtlpzmzozddtrp0(W0,xy,xJ) ),
inference(negate_conjecture,[status(cth)],[m__]) ).
cnf(71,plain,
( ~ aElement0(X0)
| ~ sdteqdtlpzmzozddtrp0(X0,xx,xI)
| ~ sdteqdtlpzmzozddtrp0(X0,xy,xJ) ),
inference(cnf,[status(esa)],[m___negated]) ).
cnf(l0,plain,
( ~ aElement0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)))
| ~ sdteqdtlpzmzozddtrp0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),xx,xI)
| ~ sdteqdtlpzmzozddtrp0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),xy,xJ) ),
inference(instantiation,[status(thm)],[71]) ).
fof(mDefMod,plain,
! [W0,W1,W2] :
( ( aElement0(W0)
& aElement0(W1)
& aIdeal0(W2) )
=> ( sdteqdtlpzmzozddtrp0(W0,W1,W2)
<=> aElementOf0(sdtpldt0(W0,smndt0(W1)),W2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefMod) ).
cnf(59,plain,
( ~ aElement0(X0)
| ~ aElement0(X1)
| ~ aIdeal0(X2)
| ~ aElementOf0(sdtpldt0(X0,smndt0(X1)),X2)
| sdteqdtlpzmzozddtrp0(X0,X1,X2) ),
inference(cnf,[status(esa)],[mDefMod]) ).
cnf(l1,plain,
( ~ aElement0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)))
| ~ aElement0(xx)
| ~ aIdeal0(xI)
| ~ aElementOf0(sdtpldt0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),smndt0(xx)),xI)
| sdteqdtlpzmzozddtrp0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),xx,xI) ),
inference(instantiation,[status(thm)],[59]) ).
fof(m__1205,plain,
( aIdeal0(xI)
& aIdeal0(xJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1205) ).
cnf(60,plain,
aIdeal0(xI),
inference(cnf,[status(esa)],[m__1205]) ).
cnf(l25,plain,
aIdeal0(xI),
inference(instantiation,[status(thm)],[60]) ).
fof(m__1217,plain,
( aElement0(xx)
& aElement0(xy) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1217) ).
cnf(63,plain,
aElement0(xx),
inference(cnf,[status(esa)],[m__1217]) ).
cnf(l6,plain,
aElement0(xx),
inference(instantiation,[status(thm)],[63]) ).
fof(m__1332,plain,
aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1332) ).
cnf(69,plain,
aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
inference(cnf,[status(esa)],[m__1332]) ).
cnf(l7,plain,
aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
inference(instantiation,[status(thm)],[69]) ).
cnf(l19,plain,
( ~ aElement0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)))
| ~ aElement0(xy)
| ~ aIdeal0(xJ)
| ~ aElementOf0(sdtpldt0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),smndt0(xy)),xJ)
| sdteqdtlpzmzozddtrp0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),xy,xJ) ),
inference(instantiation,[status(thm)],[59]) ).
fof(mSortsB,plain,
! [W0,W1] :
( ( aElement0(W0)
& aElement0(W1) )
=> aElement0(sdtpldt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB) ).
cnf(3,plain,
( ~ aElement0(X0)
| ~ aElement0(X1)
| aElement0(sdtpldt0(X0,X1)) ),
inference(cnf,[status(esa)],[mSortsB]) ).
cnf(l3,plain,
( ~ aElement0(sdtasdt0(xy,xa))
| ~ aElement0(sdtasdt0(xx,xb))
| aElement0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l2,plain,
( ~ aElement0(sdtasdt0(xy,xa))
| ~ aElement0(sdtasdt0(xx,xb))
| aElement0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb))) ),
inference(instantiation,[status(thm)],[3]) ).
fof(m__1319,plain,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1319) ).
cnf(68,plain,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
inference(cnf,[status(esa)],[m__1319]) ).
cnf(l58,plain,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
inference(instantiation,[status(thm)],[68]) ).
cnf(64,plain,
aElement0(xy),
inference(cnf,[status(esa)],[m__1217]) ).
cnf(l94,plain,
aElement0(xy),
inference(instantiation,[status(thm)],[64]) ).
cnf(61,plain,
aIdeal0(xJ),
inference(cnf,[status(esa)],[m__1205]) ).
cnf(l54,plain,
aIdeal0(xJ),
inference(instantiation,[status(thm)],[61]) ).
fof(mEOfElem,plain,
! [W0] :
( aSet0(W0)
=> ! [W1] :
( aElementOf0(W1,W0)
=> aElement0(W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mEOfElem) ).
cnf(23,plain,
( ~ aElementOf0(X0,X1)
| ~ aSet0(X1)
| aElement0(X0) ),
inference(cnf,[status(esa)],[mEOfElem]) ).
cnf(l230,plain,
( ~ aElementOf0(sdtasdt0(xx,xb),xJ)
| ~ aSet0(xJ)
| aElement0(sdtasdt0(xx,xb)) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l79,plain,
( ~ aElement0(sdtasdt0(xy,xa))
| ~ aElement0(sdtasdt0(xx,xb))
| aElement0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l81,plain,
( ~ aElementOf0(sdtasdt0(xx,xb),xJ)
| ~ aSet0(xJ)
| aElement0(sdtasdt0(xx,xb)) ),
inference(instantiation,[status(thm)],[23]) ).
fof(mDefIdeal,plain,
! [W0] :
( aIdeal0(W0)
<=> ( aSet0(W0)
& ! [W1] :
( aElementOf0(W1,W0)
=> ( ! [W2] :
( aElementOf0(W2,W0)
=> aElementOf0(sdtpldt0(W1,W2),W0) )
& ! [W2] :
( aElement0(W2)
=> aElementOf0(sdtasdt0(W2,W1),W0) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDefIdeal) ).
cnf(50,plain,
( ~ aElement0(X0)
| ~ aIdeal0(X1)
| ~ aElementOf0(X2,X1)
| aElementOf0(sdtasdt0(X0,X2),X1) ),
inference(cnf,[status(esa)],[mDefIdeal]) ).
cnf(l238,plain,
( ~ aElement0(xx)
| ~ aIdeal0(xJ)
| ~ aElementOf0(xb,xJ)
| aElementOf0(sdtasdt0(xx,xb),xJ) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l20,plain,
( ~ aElementOf0(sdtasdt0(xy,xa),xI)
| ~ aSet0(xI)
| aElement0(sdtasdt0(xy,xa)) ),
inference(instantiation,[status(thm)],[23]) ).
fof(m__1409,plain,
aElementOf0(sdtpldt0(xw,smndt0(xy)),xJ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1409) ).
cnf(70,plain,
aElementOf0(sdtpldt0(xw,smndt0(xy)),xJ),
inference(cnf,[status(esa)],[m__1409]) ).
cnf(l225,plain,
aElementOf0(sdtpldt0(xw,smndt0(xy)),xJ),
inference(instantiation,[status(thm)],[70]) ).
cnf(l118,plain,
( ~ aElementOf0(sdtasdt0(xy,xa),xI)
| ~ aSet0(xI)
| aElement0(sdtasdt0(xy,xa)) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l243,plain,
aIdeal0(xJ),
inference(instantiation,[status(thm)],[61]) ).
cnf(48,plain,
( ~ aIdeal0(X0)
| aSet0(X0) ),
inference(cnf,[status(esa)],[mDefIdeal]) ).
cnf(l231,plain,
( ~ aIdeal0(xJ)
| aSet0(xJ) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l31,plain,
( ~ aElementOf0(sdtasdt0(xy,xa),xI)
| ~ aSet0(xI)
| aElement0(sdtasdt0(xy,xa)) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l247,plain,
aElement0(xx),
inference(instantiation,[status(thm)],[63]) ).
cnf(l24,plain,
( ~ aElement0(xy)
| ~ aIdeal0(xI)
| ~ aElementOf0(xa,xI)
| aElementOf0(sdtasdt0(xy,xa),xI) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l83,plain,
( ~ aElement0(xx)
| ~ aIdeal0(xJ)
| ~ aElementOf0(xb,xJ)
| aElementOf0(sdtasdt0(xx,xb),xJ) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l69,plain,
( ~ aElement0(xy)
| ~ aIdeal0(xI)
| ~ aElementOf0(xa,xI)
| aElementOf0(sdtasdt0(xy,xa),xI) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l360,plain,
( ~ aElement0(xy)
| ~ aIdeal0(xI)
| ~ aElementOf0(xa,xI)
| aElementOf0(sdtasdt0(xy,xa),xI) ),
inference(instantiation,[status(thm)],[50]) ).
cnf(l384,plain,
aElement0(xx),
inference(instantiation,[status(thm)],[63]) ).
fof(m__1294,plain,
( aElementOf0(xa,xI)
& aElementOf0(xb,xJ)
& sdtpldt0(xa,xb) = sz10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1294) ).
cnf(66,plain,
aElementOf0(xb,xJ),
inference(cnf,[status(esa)],[m__1294]) ).
cnf(l359,plain,
aElementOf0(xb,xJ),
inference(instantiation,[status(thm)],[66]) ).
cnf(l494,plain,
aElementOf0(xb,xJ),
inference(instantiation,[status(thm)],[66]) ).
cnf(l352,plain,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
inference(instantiation,[status(thm)],[68]) ).
cnf(l369,plain,
( ~ aIdeal0(xJ)
| aSet0(xJ) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l78,plain,
( ~ aIdeal0(xI)
| aSet0(xI) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(65,plain,
aElementOf0(xa,xI),
inference(cnf,[status(esa)],[m__1294]) ).
cnf(l743,plain,
aElementOf0(xa,xI),
inference(instantiation,[status(thm)],[65]) ).
cnf(l533,plain,
aIdeal0(xJ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l563,plain,
aElement0(xy),
inference(instantiation,[status(thm)],[64]) ).
cnf(l495,plain,
aIdeal0(xI),
inference(instantiation,[status(thm)],[60]) ).
cnf(l88,plain,
aElement0(xy),
inference(instantiation,[status(thm)],[64]) ).
cnf(l96,plain,
aIdeal0(xI),
inference(instantiation,[status(thm)],[60]) ).
cnf(l47,plain,
( ~ aIdeal0(xI)
| aSet0(xI) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l409,plain,
( ~ aIdeal0(xI)
| aSet0(xI) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l129,plain,
aIdeal0(xI),
inference(instantiation,[status(thm)],[60]) ).
cnf(l89,plain,
aIdeal0(xI),
inference(instantiation,[status(thm)],[60]) ).
cnf(l160,plain,
aElementOf0(xa,xI),
inference(instantiation,[status(thm)],[65]) ).
cnf(l97,plain,
aElementOf0(xa,xI),
inference(instantiation,[status(thm)],[65]) ).
cnf(l62,plain,
aIdeal0(xI),
inference(instantiation,[status(thm)],[60]) ).
cnf(l126,plain,
aElement0(xy),
inference(instantiation,[status(thm)],[64]) ).
fof(mSortsB_02,plain,
! [W0,W1] :
( ( aElement0(W0)
& aElement0(W1) )
=> aElement0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB_02) ).
cnf(4,plain,
( ~ aElement0(X0)
| ~ aElement0(X1)
| aElement0(sdtasdt0(X0,X1)) ),
inference(cnf,[status(esa)],[mSortsB_02]) ).
cnf(l4,plain,
( ~ aElement0(xx)
| ~ aElement0(xb)
| aElement0(sdtasdt0(xx,xb)) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(l457,plain,
aIdeal0(xJ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l493,plain,
aIdeal0(xI),
inference(instantiation,[status(thm)],[60]) ).
cnf(l239,plain,
aIdeal0(xJ),
inference(instantiation,[status(thm)],[61]) ).
cnf(l268,plain,
aElement0(xx),
inference(instantiation,[status(thm)],[63]) ).
cnf(l259,plain,
( ~ aElementOf0(xb,xJ)
| ~ aSet0(xJ)
| aElement0(xb) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(l280,plain,
aElementOf0(xb,xJ),
inference(instantiation,[status(thm)],[66]) ).
cnf(l265,plain,
( ~ aIdeal0(xJ)
| aSet0(xJ) ),
inference(instantiation,[status(thm)],[48]) ).
cnf(l1059,plain,
aIdeal0(xJ),
inference(instantiation,[status(thm)],[61]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l25,l6,l7,l19,l3,l2,l58,l94,l54,l230,l79,l81,l238,l20,l225,l118,l243,l231,l31,l247,l24,l83,l69,l360,l384,l359,l494,l352,l369,l78,l743,l533,l563,l495,l88,l96,l47,l409,l129,l89,l160,l97,l62,l126,l4,l457,l493,l239,l268,l259,l280,l265,l1059]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : RNG099+1 : TPTP v9.0.0. Released v4.0.0.
% 0.06/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.33 % Computer : n018.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Mon Jul 21 17:58:19 EDT 2025
% 0.13/0.33 % CPUTime :
% 0.13/0.34 % launching worker at depth: 6
% 0.13/0.34 % launching worker at depth: 7
% 0.13/0.34 % launching worker at depth: 2
% 0.13/0.34 % launching worker at depth: 4
% 0.13/0.34 % launching worker at depth: 3
% 0.13/0.34 % launching worker at depth: 1
% 0.13/0.34 % launching worker at depth: 8
% 0.13/0.34 % launching worker at depth: 5
% 0.13/0.34 % launching worker at depth: 9
% 0.13/0.34 % launching worker at depth: 10
% 0.19/0.39 % launching worker at depth: 11
% 6.94/1.27 % launching worker at depth: 12
% 143.36/18.34 % SZS status Theorem for theBenchmark
% 143.36/18.34 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------