%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : RNG099+2 : 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 : n017.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 4.19s 0.90s
% Output : CNFRefutation 4.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 10
% Syntax : Number of formulae : 43 ( 23 unt; 0 def)
% Number of atoms : 95 ( 5 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 77 ( 25 ~; 26 |; 16 &)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 22 ( 0 sgn 12 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__,plain,
? [W0] :
( aElement0(W0)
& ( aElementOf0(sdtpldt0(W0,smndt0(xx)),xI)
| sdteqdtlpzmzozddtrp0(W0,xx,xI) )
& ( aElementOf0(sdtpldt0(W0,smndt0(xy)),xJ)
| sdteqdtlpzmzozddtrp0(W0,xy,xJ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(m___negated,plain,
~ ? [W0] :
( aElement0(W0)
& ( aElementOf0(sdtpldt0(W0,smndt0(xx)),xI)
| sdteqdtlpzmzozddtrp0(W0,xx,xI) )
& ( aElementOf0(sdtpldt0(W0,smndt0(xy)),xJ)
| sdteqdtlpzmzozddtrp0(W0,xy,xJ) ) ),
inference(negate_conjecture,[status(cth)],[m__]) ).
cnf(80,plain,
( ~ aElement0(X0)
| ~ aElementOf0(sdtpldt0(X0,smndt0(xx)),xI)
| sP4(X0) ),
inference(cnf,[status(esa)],[m___negated]) ).
cnf(l0,plain,
( ~ aElement0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)))
| ~ aElementOf0(sdtpldt0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),smndt0(xx)),xI)
| sP4(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb))) ),
inference(instantiation,[status(thm)],[80]) ).
fof(m__1332,plain,
aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1332) ).
cnf(78,plain,
aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
inference(cnf,[status(esa)],[m__1332]) ).
cnf(l4,plain,
aElementOf0(sdtpldt0(xw,smndt0(xx)),xI),
inference(instantiation,[status(thm)],[78]) ).
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(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(77,plain,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
inference(cnf,[status(esa)],[m__1319]) ).
cnf(l36,plain,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
inference(instantiation,[status(thm)],[77]) ).
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(l23,plain,
( ~ aElement0(xy)
| ~ aElement0(xa)
| aElement0(sdtasdt0(xy,xa)) ),
inference(instantiation,[status(thm)],[4]) ).
cnf(83,plain,
( ~ aElementOf0(sdtpldt0(X0,smndt0(xy)),xJ)
| ~ sP4(X0) ),
inference(cnf,[status(esa)],[m___negated]) ).
cnf(l5,plain,
( ~ aElementOf0(sdtpldt0(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),smndt0(xy)),xJ)
| ~ sP4(sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb))) ),
inference(instantiation,[status(thm)],[83]) ).
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(l46,plain,
( ~ aElementOf0(xa,xI)
| ~ aSet0(xI)
| aElement0(xa) ),
inference(instantiation,[status(thm)],[23]) ).
fof(m__1205,plain,
( aSet0(xI)
& ! [W0] :
( aElementOf0(W0,xI)
=> ( ! [W1] :
( aElementOf0(W1,xI)
=> aElementOf0(sdtpldt0(W0,W1),xI) )
& ! [W1] :
( aElement0(W1)
=> aElementOf0(sdtasdt0(W1,W0),xI) ) ) )
& aIdeal0(xI)
& aSet0(xJ)
& ! [W0] :
( aElementOf0(W0,xJ)
=> ( ! [W1] :
( aElementOf0(W1,xJ)
=> aElementOf0(sdtpldt0(W0,W1),xJ) )
& ! [W1] :
( aElement0(W1)
=> aElementOf0(sdtasdt0(W1,W0),xJ) ) ) )
& aIdeal0(xJ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1205) ).
cnf(60,plain,
aSet0(xI),
inference(cnf,[status(esa)],[m__1205]) ).
cnf(l97,plain,
aSet0(xI),
inference(instantiation,[status(thm)],[60]) ).
fof(m__1217,plain,
( aElement0(xx)
& aElement0(xy) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1217) ).
cnf(73,plain,
aElement0(xy),
inference(cnf,[status(esa)],[m__1217]) ).
cnf(l43,plain,
aElement0(xy),
inference(instantiation,[status(thm)],[73]) ).
cnf(l66,plain,
xw = sdtpldt0(sdtasdt0(xy,xa),sdtasdt0(xx,xb)),
inference(instantiation,[status(thm)],[77]) ).
cnf(l14,plain,
( ~ aElement0(xx)
| ~ aElement0(xb)
| aElement0(sdtasdt0(xx,xb)) ),
inference(instantiation,[status(thm)],[4]) ).
fof(m__1294,plain,
( aElementOf0(xa,xI)
& aElementOf0(xb,xJ)
& sdtpldt0(xa,xb) = sz10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1294) ).
cnf(74,plain,
aElementOf0(xa,xI),
inference(cnf,[status(esa)],[m__1294]) ).
cnf(l95,plain,
aElementOf0(xa,xI),
inference(instantiation,[status(thm)],[74]) ).
cnf(l121,plain,
( ~ aElementOf0(xb,xJ)
| ~ aSet0(xJ)
| aElement0(xb) ),
inference(instantiation,[status(thm)],[23]) ).
cnf(75,plain,
aElementOf0(xb,xJ),
inference(cnf,[status(esa)],[m__1294]) ).
cnf(l128,plain,
aElementOf0(xb,xJ),
inference(instantiation,[status(thm)],[75]) ).
cnf(64,plain,
aSet0(xJ),
inference(cnf,[status(esa)],[m__1205]) ).
cnf(l122,plain,
aSet0(xJ),
inference(instantiation,[status(thm)],[64]) ).
cnf(72,plain,
aElement0(xx),
inference(cnf,[status(esa)],[m__1217]) ).
cnf(l120,plain,
aElement0(xx),
inference(instantiation,[status(thm)],[72]) ).
fof(m__1409,plain,
aElementOf0(sdtpldt0(xw,smndt0(xy)),xJ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1409) ).
cnf(79,plain,
aElementOf0(sdtpldt0(xw,smndt0(xy)),xJ),
inference(cnf,[status(esa)],[m__1409]) ).
cnf(l51,plain,
aElementOf0(sdtpldt0(xw,smndt0(xy)),xJ),
inference(instantiation,[status(thm)],[79]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l4,l2,l36,l23,l5,l46,l97,l43,l66,l14,l95,l121,l128,l122,l120,l51]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : RNG099+2 : TPTP v9.0.0. Released v4.0.0.
% 0.04/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n017.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 : Mon Jul 21 17:58:49 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.34 % launching worker at depth: 5
% 0.12/0.34 % launching worker at depth: 1
% 0.12/0.34 % launching worker at depth: 3
% 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: 6
% 0.12/0.34 % launching worker at depth: 2
% 0.12/0.34 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % launching worker at depth: 10
% 0.18/0.47 % launching worker at depth: 11
% 4.19/0.90 % SZS status Theorem for theBenchmark
% 4.19/0.90 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------