%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NUM507+3 : 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 : n025.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 12:28:21 PM UTC 2025
% Result : Theorem 197.38s 25.09s
% Output : CNFRefutation 197.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 13
% Syntax : Number of formulae : 75 ( 43 unt; 0 def)
% Number of atoms : 194 ( 49 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 198 ( 79 ~; 70 |; 36 &)
% ( 0 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 36 ( 0 sgn 16 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__,plain,
( sdtpldt0(sdtpldt0(xn,xm),xr) != sdtpldt0(sdtpldt0(xn,xm),xp)
& ( ? [W0] :
( aNaturalNumber0(W0)
& sdtpldt0(sdtpldt0(sdtpldt0(xn,xm),xr),W0) = sdtpldt0(sdtpldt0(xn,xm),xp) )
| sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__) ).
fof(m___negated,plain,
~ ( sdtpldt0(sdtpldt0(xn,xm),xr) != sdtpldt0(sdtpldt0(xn,xm),xp)
& ( ? [W0] :
( aNaturalNumber0(W0)
& sdtpldt0(sdtpldt0(sdtpldt0(xn,xm),xr),W0) = sdtpldt0(sdtpldt0(xn,xm),xp) )
| sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp)) ) ),
inference(negate_conjecture,[status(cth)],[m__]) ).
cnf(132,plain,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(sdtpldt0(xn,xm),xr) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(cnf,[status(esa)],[m___negated]) ).
cnf(l0,plain,
( ~ sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp))
| sdtpldt0(sdtpldt0(xn,xm),xr) = sdtpldt0(sdtpldt0(xn,xm),xp) ),
inference(instantiation,[status(thm)],[132]) ).
fof(mMonAdd,plain,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( ( W0 != W1
& sdtlseqdt0(W0,W1) )
=> ! [W2] :
( aNaturalNumber0(W2)
=> ( sdtpldt0(W2,W0) != sdtpldt0(W2,W1)
& sdtlseqdt0(sdtpldt0(W2,W0),sdtpldt0(W2,W1))
& sdtpldt0(W0,W2) != sdtpldt0(W1,W2)
& sdtlseqdt0(sdtpldt0(W0,W2),sdtpldt0(W1,W2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mMonAdd) ).
cnf(36,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1)
| X0 = X1
| sdtlseqdt0(sdtpldt0(X2,X0),sdtpldt0(X2,X1)) ),
inference(cnf,[status(esa)],[mMonAdd]) ).
cnf(l7,plain,
( ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ sdtlseqdt0(xr,xp)
| xr = xp
| sdtlseqdt0(sdtpldt0(sdtpldt0(xn,xm),xr),sdtpldt0(sdtpldt0(xn,xm),xp)) ),
inference(instantiation,[status(thm)],[36]) ).
fof(m__2342,plain,
( aNaturalNumber0(xr)
& ? [W0] :
( aNaturalNumber0(W0)
& xk = sdtasdt0(xr,W0) )
& doDivides0(xr,xk)
& xr != sz00
& xr != sz10
& ! [W0] :
( ( aNaturalNumber0(W0)
& ( ? [W1] :
( aNaturalNumber0(W1)
& xr = sdtasdt0(W0,W1) )
| doDivides0(W0,xr) ) )
=> ( W0 = sz10
| W0 = xr ) )
& isPrime0(xr) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2342) ).
cnf(113,plain,
aNaturalNumber0(xr),
inference(cnf,[status(esa)],[m__2342]) ).
cnf(l12,plain,
aNaturalNumber0(xr),
inference(instantiation,[status(thm)],[113]) ).
fof(m__1837,plain,
( aNaturalNumber0(xn)
& aNaturalNumber0(xm)
& aNaturalNumber0(xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__1837) ).
cnf(70,plain,
aNaturalNumber0(xp),
inference(cnf,[status(esa)],[m__1837]) ).
cnf(l168,plain,
aNaturalNumber0(xp),
inference(instantiation,[status(thm)],[70]) ).
fof(mSortsB,plain,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> aNaturalNumber0(sdtpldt0(W0,W1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mSortsB) ).
cnf(3,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| aNaturalNumber0(sdtpldt0(X0,X1)) ),
inference(cnf,[status(esa)],[mSortsB]) ).
cnf(l47,plain,
( ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm)
| aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(68,plain,
aNaturalNumber0(xn),
inference(cnf,[status(esa)],[m__1837]) ).
cnf(l203,plain,
aNaturalNumber0(xn),
inference(instantiation,[status(thm)],[68]) ).
fof(mAddCanc,plain,
! [W0,W1,W2] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1)
& aNaturalNumber0(W2) )
=> ( ( sdtpldt0(W0,W1) = sdtpldt0(W0,W2)
| sdtpldt0(W1,W0) = sdtpldt0(W2,W0) )
=> W1 = W2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mAddCanc) ).
cnf(17,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sdtpldt0(X0,X1) != sdtpldt0(X0,X2)
| X1 = X2 ),
inference(cnf,[status(esa)],[mAddCanc]) ).
cnf(l1,plain,
( ~ aNaturalNumber0(sdtpldt0(xn,xm))
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp)
| sdtpldt0(sdtpldt0(xn,xm),xr) != sdtpldt0(sdtpldt0(xn,xm),xp)
| xr = xp ),
inference(instantiation,[status(thm)],[17]) ).
fof(mLETran,plain,
! [W0,W1,W2] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1)
& aNaturalNumber0(W2) )
=> ( ( sdtlseqdt0(W0,W1)
& sdtlseqdt0(W1,W2) )
=> sdtlseqdt0(W0,W2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLETran) ).
cnf(32,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X2)
| sdtlseqdt0(X0,X2) ),
inference(cnf,[status(esa)],[mLETran]) ).
cnf(l159,plain,
( ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(xp)
| ~ sdtlseqdt0(xr,xk)
| ~ sdtlseqdt0(xk,xp)
| sdtlseqdt0(xr,xp) ),
inference(instantiation,[status(thm)],[32]) ).
cnf(l160,plain,
aNaturalNumber0(xr),
inference(instantiation,[status(thm)],[113]) ).
cnf(l527,plain,
aNaturalNumber0(xp),
inference(instantiation,[status(thm)],[70]) ).
cnf(l161,plain,
aNaturalNumber0(xp),
inference(instantiation,[status(thm)],[70]) ).
fof(mDivLE,plain,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( ( doDivides0(W0,W1)
& W1 != sz00 )
=> sdtlseqdt0(W0,W1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mDivLE) ).
cnf(56,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ doDivides0(X0,X1)
| X1 = sz00
| sdtlseqdt0(X0,X1) ),
inference(cnf,[status(esa)],[mDivLE]) ).
cnf(l170,plain,
( ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xk)
| ~ doDivides0(xr,xk)
| xk = sz00
| sdtlseqdt0(xr,xk) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l914,plain,
( ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xk)
| ~ doDivides0(xr,xk)
| xk = sz00
| sdtlseqdt0(xr,xk) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l952,plain,
aNaturalNumber0(xr),
inference(instantiation,[status(thm)],[113]) ).
fof(m__2306,plain,
( aNaturalNumber0(xk)
& sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
& xk = sdtsldt0(sdtasdt0(xn,xm),xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2306) ).
cnf(106,plain,
aNaturalNumber0(xk),
inference(cnf,[status(esa)],[m__2306]) ).
cnf(l169,plain,
aNaturalNumber0(xk),
inference(instantiation,[status(thm)],[106]) ).
cnf(l229,plain,
aNaturalNumber0(xr),
inference(instantiation,[status(thm)],[113]) ).
cnf(116,plain,
doDivides0(xr,xk),
inference(cnf,[status(esa)],[m__2342]) ).
cnf(l916,plain,
doDivides0(xr,xk),
inference(instantiation,[status(thm)],[116]) ).
fof(m__2327,plain,
( xk != sz00
& xk != sz10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2327) ).
cnf(111,plain,
xk != sz00,
inference(cnf,[status(esa)],[m__2327]) ).
cnf(l228,plain,
xk != sz00,
inference(instantiation,[status(thm)],[111]) ).
fof(m__2377,plain,
( xk != xp
& ? [W0] :
( aNaturalNumber0(W0)
& sdtpldt0(xk,W0) = xp )
& sdtlseqdt0(xk,xp) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2377) ).
cnf(130,plain,
sdtlseqdt0(xk,xp),
inference(cnf,[status(esa)],[m__2377]) ).
cnf(l163,plain,
sdtlseqdt0(xk,xp),
inference(instantiation,[status(thm)],[130]) ).
cnf(l3,plain,
aNaturalNumber0(xr),
inference(instantiation,[status(thm)],[113]) ).
cnf(l956,plain,
xk != sz00,
inference(instantiation,[status(thm)],[111]) ).
cnf(l173,plain,
doDivides0(xr,xk),
inference(instantiation,[status(thm)],[116]) ).
cnf(l950,plain,
aNaturalNumber0(xk),
inference(instantiation,[status(thm)],[106]) ).
cnf(l206,plain,
aNaturalNumber0(xk),
inference(instantiation,[status(thm)],[106]) ).
cnf(69,plain,
aNaturalNumber0(xm),
inference(cnf,[status(esa)],[m__1837]) ).
cnf(l218,plain,
aNaturalNumber0(xm),
inference(instantiation,[status(thm)],[69]) ).
fof(mLEAsym,plain,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( ( sdtlseqdt0(W0,W1)
& sdtlseqdt0(W1,W0) )
=> W0 = W1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mLEAsym) ).
cnf(31,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ sdtlseqdt0(X0,X1)
| ~ sdtlseqdt0(X1,X0)
| X0 = X1 ),
inference(cnf,[status(esa)],[mLEAsym]) ).
cnf(l934,plain,
( ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(xp)
| ~ sdtlseqdt0(xk,xp)
| ~ sdtlseqdt0(xp,xk)
| xk = xp ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l27,plain,
( ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xm)
| aNaturalNumber0(sdtpldt0(xn,xm)) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l939,plain,
aNaturalNumber0(xk),
inference(instantiation,[status(thm)],[106]) ).
cnf(l936,plain,
aNaturalNumber0(xp),
inference(instantiation,[status(thm)],[70]) ).
cnf(l29,plain,
aNaturalNumber0(xm),
inference(instantiation,[status(thm)],[69]) ).
cnf(l31,plain,
aNaturalNumber0(xn),
inference(instantiation,[status(thm)],[68]) ).
cnf(127,plain,
xk != xp,
inference(cnf,[status(esa)],[m__2377]) ).
cnf(l937,plain,
xk != xp,
inference(instantiation,[status(thm)],[127]) ).
cnf(l595,plain,
( ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(xp)
| ~ sdtlseqdt0(xk,xp)
| ~ sdtlseqdt0(xp,xk)
| xk = xp ),
inference(instantiation,[status(thm)],[31]) ).
cnf(l938,plain,
sdtlseqdt0(xk,xp),
inference(instantiation,[status(thm)],[130]) ).
cnf(l620,plain,
aNaturalNumber0(xp),
inference(instantiation,[status(thm)],[70]) ).
cnf(l623,plain,
sdtlseqdt0(xk,xp),
inference(instantiation,[status(thm)],[130]) ).
cnf(l621,plain,
aNaturalNumber0(xk),
inference(instantiation,[status(thm)],[106]) ).
cnf(l1036,plain,
xk != xp,
inference(instantiation,[status(thm)],[127]) ).
cnf(l612,plain,
( ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xk)
| ~ doDivides0(xr,xk)
| xk = sz00
| sdtlseqdt0(xr,xk) ),
inference(instantiation,[status(thm)],[56]) ).
cnf(l625,plain,
doDivides0(xr,xk),
inference(instantiation,[status(thm)],[116]) ).
cnf(l624,plain,
aNaturalNumber0(xr),
inference(instantiation,[status(thm)],[113]) ).
fof(m__2315,plain,
~ ( xk = sz00
| xk = sz10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m__2315) ).
cnf(109,plain,
xk != sz00,
inference(cnf,[status(esa)],[m__2315]) ).
cnf(l619,plain,
xk != sz00,
inference(instantiation,[status(thm)],[109]) ).
cnf(l618,plain,
aNaturalNumber0(xk),
inference(instantiation,[status(thm)],[106]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l7,l12,l168,l47,l203,l1,l159,l160,l527,l161,l170,l914,l952,l169,l229,l916,l228,l163,l3,l956,l173,l950,l206,l218,l934,l27,l939,l936,l29,l31,l937,l595,l938,l620,l623,l621,l1036,l612,l625,l624,l619,l618]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM507+3 : TPTP v9.0.0. Released v4.0.0.
% 0.03/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.34 % Computer : n025.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Jul 21 12:33:19 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.12/0.35 % launching worker at depth: 1
% 0.12/0.35 % launching worker at depth: 3
% 0.12/0.35 % launching worker at depth: 5
% 0.12/0.35 % launching worker at depth: 8
% 0.12/0.35 % launching worker at depth: 2
% 0.12/0.35 % launching worker at depth: 6
% 0.12/0.35 % launching worker at depth: 7
% 0.12/0.35 % launching worker at depth: 4
% 0.12/0.35 % launching worker at depth: 9
% 0.12/0.36 % launching worker at depth: 10
% 1.69/0.55 % launching worker at depth: 11
% 197.38/25.09 % SZS status Theorem for theBenchmark
% 197.38/25.09 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------