%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : RNG073+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 : 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:48 PM UTC 2025
% Result : Theorem 73.79s 9.66s
% Output : CNFRefutation 73.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 17
% Syntax : Number of formulae : 81 ( 47 unt; 0 def)
% Number of atoms : 170 ( 20 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 155 ( 66 ~; 63 |; 17 &)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 14 con; 0-2 aty)
% Number of variables : 26 ( 0 sgn 13 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__,plain,
sdtpldt0(xR,xS) = sdtpldt0(xP,xP),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(m___negated,plain,
sdtpldt0(xR,xS) != sdtpldt0(xP,xP),
inference(negate_conjecture,[status(cth)],[m__]) ).
cnf(93,plain,
sdtpldt0(xR,xS) != sdtpldt0(xP,xP),
inference(cnf,[status(esa)],[m___negated]) ).
cnf(l0,plain,
sdtpldt0(xR,xS) != sdtpldt0(xP,xP),
inference(instantiation,[status(thm)],[93]) ).
fof(mSqrt,plain,
! [W0,W1] :
( ( aScalar0(W0)
& aScalar0(W1) )
=> ( ( sdtlseqdt0(sz0z00,W0)
& sdtlseqdt0(sz0z00,W1)
& sdtasdt0(W0,W0) = sdtasdt0(W1,W1) )
=> W0 = W1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSqrt) ).
cnf(38,plain,
( ~ aScalar0(X0)
| ~ aScalar0(X1)
| sdtasdt0(X0,X0) != sdtasdt0(X1,X1)
| ~ sdtlseqdt0(sz0z00,X0)
| ~ sdtlseqdt0(sz0z00,X1)
| X0 = X1 ),
inference(cnf,[status(esa)],[mSqrt]) ).
cnf(l1,plain,
( ~ aScalar0(sdtpldt0(xR,xS))
| ~ aScalar0(sdtpldt0(xP,xP))
| sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)) != sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))
| ~ sdtlseqdt0(sz0z00,sdtpldt0(xR,xS))
| ~ sdtlseqdt0(sz0z00,sdtpldt0(xP,xP))
| sdtpldt0(xR,xS) = sdtpldt0(xP,xP) ),
inference(instantiation,[status(thm)],[38]) ).
fof(m__2628,plain,
( sdtlseqdt0(sz0z00,sdtpldt0(xR,xS))
& sdtlseqdt0(sz0z00,sdtpldt0(xP,xP)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2628) ).
cnf(90,plain,
sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)),
inference(cnf,[status(esa)],[m__2628]) ).
cnf(l176,plain,
sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)),
inference(instantiation,[status(thm)],[90]) ).
fof(mLETot,plain,
! [W0,W1] :
( ( aScalar0(W0)
& aScalar0(W1) )
=> ( sdtlseqdt0(W0,W1)
| sdtlseqdt0(W1,W0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETot) ).
cnf(34,plain,
( ~ aScalar0(X0)
| ~ aScalar0(X1)
| sdtlseqdt0(X0,X1)
| sdtlseqdt0(X1,X0) ),
inference(cnf,[status(esa)],[mLETot]) ).
cnf(l421,plain,
( ~ aScalar0(sdtpldt0(xP,xP))
| ~ aScalar0(sz0z00)
| sdtlseqdt0(sdtpldt0(xP,xP),sz0z00)
| sdtlseqdt0(sz0z00,sdtpldt0(xP,xP)) ),
inference(instantiation,[status(thm)],[34]) ).
fof(mLEASm,plain,
! [W0,W1] :
( ( aScalar0(W0)
& aScalar0(W1) )
=> ( ( sdtlseqdt0(W0,W1)
& sdtlseqdt0(W1,W0) )
=> W0 = W1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLEASm) ).
cnf(30,plain,
( ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| X0 = X1 ),
inference(cnf,[status(esa)],[mLEASm]) ).
cnf(l175,plain,
( ~ aScalar0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)))
| ~ aScalar0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)))
| ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)))
| ~ sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)))
| sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)) = sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)) ),
inference(instantiation,[status(thm)],[30]) ).
fof(m__2654,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2654) ).
cnf(92,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))),
inference(cnf,[status(esa)],[m__2654]) ).
cnf(l177,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS)),sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))),
inference(instantiation,[status(thm)],[92]) ).
fof(mSumSc,plain,
! [W0,W1] :
( ( aScalar0(W0)
& aScalar0(W1) )
=> aScalar0(sdtpldt0(W0,W1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSumSc) ).
cnf(8,plain,
( ~ aScalar0(X0)
| ~ aScalar0(X1)
| aScalar0(sdtpldt0(X0,X1)) ),
inference(cnf,[status(esa)],[mSumSc]) ).
cnf(l424,plain,
( ~ aScalar0(xP)
| ~ aScalar0(xP)
| aScalar0(sdtpldt0(xP,xP)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l5,plain,
( ~ aScalar0(xP)
| ~ aScalar0(xP)
| aScalar0(sdtpldt0(xP,xP)) ),
inference(instantiation,[status(thm)],[8]) ).
fof(mSZeroSc,plain,
aScalar0(sz0z00),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mSZeroSc) ).
cnf(7,plain,
aScalar0(sz0z00),
inference(cnf,[status(esa)],[mSZeroSc]) ).
cnf(l436,plain,
aScalar0(sz0z00),
inference(instantiation,[status(thm)],[7]) ).
fof(mMulSc,plain,
! [W0,W1] :
( ( aScalar0(W0)
& aScalar0(W1) )
=> aScalar0(sdtasdt0(W0,W1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mMulSc) ).
cnf(9,plain,
( ~ aScalar0(X0)
| ~ aScalar0(X1)
| aScalar0(sdtasdt0(X0,X1)) ),
inference(cnf,[status(esa)],[mMulSc]) ).
cnf(l201,plain,
( ~ aScalar0(sdtpldt0(xR,xS))
| ~ aScalar0(sdtpldt0(xR,xS))
| aScalar0(sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))) ),
inference(instantiation,[status(thm)],[9]) ).
fof(m__1911,plain,
( aScalar0(xP)
& xP = sdtasdt0(xE,xH) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1911) ).
cnf(78,plain,
aScalar0(xP),
inference(cnf,[status(esa)],[m__1911]) ).
cnf(l24,plain,
aScalar0(xP),
inference(instantiation,[status(thm)],[78]) ).
fof(m__2405,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2405) ).
cnf(87,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))),
inference(cnf,[status(esa)],[m__2405]) ).
cnf(l468,plain,
sdtlseqdt0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP)),sdtasdt0(sdtpldt0(xR,xS),sdtpldt0(xR,xS))),
inference(instantiation,[status(thm)],[87]) ).
cnf(l434,plain,
aScalar0(xP),
inference(instantiation,[status(thm)],[78]) ).
cnf(l428,plain,
aScalar0(xP),
inference(instantiation,[status(thm)],[78]) ).
cnf(l211,plain,
( ~ aScalar0(xR)
| ~ aScalar0(xS)
| aScalar0(sdtpldt0(xR,xS)) ),
inference(instantiation,[status(thm)],[8]) ).
fof(m__1930,plain,
( aScalar0(xS)
& xS = sdtasdt0(xF,xD) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1930) ).
cnf(80,plain,
aScalar0(xS),
inference(cnf,[status(esa)],[m__1930]) ).
cnf(l251,plain,
aScalar0(xS),
inference(instantiation,[status(thm)],[80]) ).
cnf(l206,plain,
( ~ aScalar0(xR)
| ~ aScalar0(xS)
| aScalar0(sdtpldt0(xR,xS)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l76,plain,
( ~ aScalar0(xE)
| ~ aScalar0(xH)
| aScalar0(sdtasdt0(xE,xH)) ),
inference(instantiation,[status(thm)],[9]) ).
fof(m__1820,plain,
( aScalar0(xE)
& xE = sdtasasdt0(xp,xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1820) ).
cnf(68,plain,
aScalar0(xE),
inference(cnf,[status(esa)],[m__1820]) ).
cnf(l81,plain,
aScalar0(xE),
inference(instantiation,[status(thm)],[68]) ).
fof(m__1892,plain,
( aScalar0(xR)
& xR = sdtasdt0(xC,xG) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1892) ).
cnf(76,plain,
aScalar0(xR),
inference(cnf,[status(esa)],[m__1892]) ).
cnf(l252,plain,
aScalar0(xR),
inference(instantiation,[status(thm)],[76]) ).
cnf(l193,plain,
( ~ aScalar0(sdtpldt0(xP,xP))
| ~ aScalar0(sdtpldt0(xP,xP))
| aScalar0(sdtasdt0(sdtpldt0(xP,xP),sdtpldt0(xP,xP))) ),
inference(instantiation,[status(thm)],[9]) ).
fof(m__1873,plain,
( aScalar0(xH)
& xH = sdtasdt0(xA,xB) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1873) ).
cnf(74,plain,
aScalar0(xH),
inference(cnf,[status(esa)],[m__1873]) ).
cnf(l82,plain,
aScalar0(xH),
inference(instantiation,[status(thm)],[74]) ).
cnf(79,plain,
xP = sdtasdt0(xE,xH),
inference(cnf,[status(esa)],[m__1911]) ).
cnf(l79,plain,
xP = sdtasdt0(xE,xH),
inference(instantiation,[status(thm)],[79]) ).
cnf(l2,plain,
( ~ aScalar0(xR)
| ~ aScalar0(xS)
| aScalar0(sdtpldt0(xR,xS)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l11,plain,
aScalar0(xS),
inference(instantiation,[status(thm)],[80]) ).
cnf(l204,plain,
( ~ aScalar0(xP)
| ~ aScalar0(xP)
| aScalar0(sdtpldt0(xP,xP)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l205,plain,
aScalar0(xP),
inference(instantiation,[status(thm)],[78]) ).
cnf(l199,plain,
( ~ aScalar0(xP)
| ~ aScalar0(xP)
| aScalar0(sdtpldt0(xP,xP)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l225,plain,
aScalar0(xP),
inference(instantiation,[status(thm)],[78]) ).
cnf(l279,plain,
aScalar0(xS),
inference(instantiation,[status(thm)],[80]) ).
fof(mLETrn,plain,
! [W0,W1,W2] :
( ( aScalar0(W0)
& aScalar0(W1)
& aScalar0(W2) )
=> ( ( sdtlseqdt0(W0,W1)
& sdtlseqdt0(W1,W2) )
=> sdtlseqdt0(W0,W2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mLETrn) ).
cnf(31,plain,
( ~ aScalar0(X0)
| ~ aScalar0(X1)
| ~ aScalar0(X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| sdtlseqdt0(X0,X2) ),
inference(cnf,[status(esa)],[mLETrn]) ).
cnf(l433,plain,
( ~ aScalar0(sdtpldt0(xP,xP))
| ~ aScalar0(sz0z00)
| ~ aScalar0(sdtpldt0(xR,xS))
| ~ sdtlseqdt0(sdtpldt0(xP,xP),sz0z00)
| ~ sdtlseqdt0(sz0z00,sdtpldt0(xR,xS))
| sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)) ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l265,plain,
aScalar0(xP),
inference(instantiation,[status(thm)],[78]) ).
cnf(l3,plain,
aScalar0(xR),
inference(instantiation,[status(thm)],[76]) ).
cnf(l270,plain,
aScalar0(xR),
inference(instantiation,[status(thm)],[76]) ).
cnf(l454,plain,
( ~ aScalar0(xP)
| ~ aScalar0(xP)
| aScalar0(sdtpldt0(xP,xP)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l470,plain,
aScalar0(xP),
inference(instantiation,[status(thm)],[78]) ).
cnf(l213,plain,
aScalar0(xP),
inference(instantiation,[status(thm)],[78]) ).
cnf(l520,plain,
aScalar0(xP),
inference(instantiation,[status(thm)],[78]) ).
cnf(l486,plain,
aScalar0(sz0z00),
inference(instantiation,[status(thm)],[7]) ).
fof(m__2590,plain,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__2590) ).
cnf(88,plain,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
inference(cnf,[status(esa)],[m__2590]) ).
cnf(l1041,plain,
~ sdtlseqdt0(sdtpldt0(xP,xP),sdtpldt0(xR,xS)),
inference(instantiation,[status(thm)],[88]) ).
cnf(l996,plain,
( ~ aScalar0(xR)
| ~ aScalar0(xS)
| aScalar0(sdtpldt0(xR,xS)) ),
inference(instantiation,[status(thm)],[8]) ).
cnf(l1026,plain,
sdtlseqdt0(sz0z00,sdtpldt0(xR,xS)),
inference(instantiation,[status(thm)],[90]) ).
cnf(l998,plain,
aScalar0(xR),
inference(instantiation,[status(thm)],[76]) ).
cnf(l1003,plain,
aScalar0(xS),
inference(instantiation,[status(thm)],[80]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l176,l421,l175,l177,l424,l5,l436,l201,l24,l468,l434,l428,l211,l251,l206,l76,l81,l252,l193,l82,l79,l2,l11,l204,l205,l199,l225,l279,l433,l265,l3,l270,l454,l470,l213,l520,l486,l1041,l996,l1026,l998,l1003]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : RNG073+1 : TPTP v9.0.0. Released v4.0.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n017.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Jul 21 17:50:04 EDT 2025
% 0.13/0.34 % CPUTime :
% 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: 5
% 0.13/0.34 % launching worker at depth: 1
% 0.13/0.34 % launching worker at depth: 3
% 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: 8
% 0.13/0.34 % launching worker at depth: 9
% 0.13/0.35 % launching worker at depth: 10
% 0.13/0.37 % launching worker at depth: 11
% 3.04/0.77 % launching worker at depth: 12
% 73.79/9.66 % SZS status Theorem for theBenchmark
% 73.79/9.66 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------