%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : NUM474+2 : 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 : n029.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:15 PM UTC 2025
% Result : Theorem 234.89s 29.98s
% Output : CNFRefutation 234.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 11
% Syntax : Number of formulae : 51 ( 34 unt; 0 def)
% Number of atoms : 115 ( 47 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 102 ( 38 ~; 34 |; 23 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-2 aty)
% Number of variables : 24 ( 0 sgn 9 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m__,plain,
sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr)) = sdtpldt0(sdtasdt0(xl,xp),xn),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__) ).
fof(m___negated,plain,
sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr)) != sdtpldt0(sdtasdt0(xl,xp),xn),
inference(negate_conjecture,[status(cth)],[m__]) ).
cnf(77,plain,
sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr)) != sdtpldt0(sdtasdt0(xl,xp),xn),
inference(cnf,[status(esa)],[m___negated]) ).
cnf(l0,plain,
sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr)) != sdtpldt0(sdtasdt0(xl,xp),xn),
inference(instantiation,[status(thm)],[77]) ).
fof(mAMDistr,plain,
! [W0,W1,W2] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1)
& aNaturalNumber0(W2) )
=> ( sdtasdt0(W0,sdtpldt0(W1,W2)) = sdtpldt0(sdtasdt0(W0,W1),sdtasdt0(W0,W2))
& sdtasdt0(sdtpldt0(W1,W2),W0) = sdtpldt0(sdtasdt0(W1,W0),sdtasdt0(W2,W0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mAMDistr) ).
cnf(15,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| ~ aNaturalNumber0(X2)
| sdtasdt0(X0,sdtpldt0(X1,X2)) = sdtpldt0(sdtasdt0(X0,X1),sdtasdt0(X0,X2)) ),
inference(cnf,[status(esa)],[mAMDistr]) ).
cnf(l17,plain,
( ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xr)
| sdtasdt0(xl,sdtpldt0(xp,xr)) = sdtpldt0(sdtasdt0(xl,xp),sdtasdt0(xl,xr)) ),
inference(instantiation,[status(thm)],[15]) ).
fof(mDefQuot,plain,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( ( W0 != sz00
& doDivides0(W0,W1) )
=> ! [W2] :
( W2 = sdtsldt0(W1,W0)
<=> ( aNaturalNumber0(W2)
& W1 = sdtasdt0(W0,W2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefQuot) ).
cnf(50,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| X2 != sdtsldt0(X1,X0)
| ~ doDivides0(X0,X1)
| aNaturalNumber0(X2)
| X0 = sz00 ),
inference(cnf,[status(esa)],[mDefQuot]) ).
cnf(l28,plain,
( ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm)
| xp != sdtsldt0(xm,xl)
| ~ doDivides0(xl,xm)
| aNaturalNumber0(xp)
| xl = sz00 ),
inference(instantiation,[status(thm)],[50]) ).
fof(m__1324,plain,
( aNaturalNumber0(xl)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1324) ).
cnf(56,plain,
aNaturalNumber0(xm),
inference(cnf,[status(esa)],[m__1324]) ).
cnf(l158,plain,
aNaturalNumber0(xm),
inference(instantiation,[status(thm)],[56]) ).
cnf(55,plain,
aNaturalNumber0(xl),
inference(cnf,[status(esa)],[m__1324]) ).
cnf(l152,plain,
aNaturalNumber0(xl),
inference(instantiation,[status(thm)],[55]) ).
fof(mDefDiff,plain,
! [W0,W1] :
( ( aNaturalNumber0(W0)
& aNaturalNumber0(W1) )
=> ( sdtlseqdt0(W0,W1)
=> ! [W2] :
( W2 = sdtmndt0(W1,W0)
<=> ( aNaturalNumber0(W2)
& sdtpldt0(W0,W2) = W1 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mDefDiff) ).
cnf(27,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| X2 != sdtmndt0(X1,X0)
| ~ sdtlseqdt0(X0,X1)
| aNaturalNumber0(X2) ),
inference(cnf,[status(esa)],[mDefDiff]) ).
cnf(l27,plain,
( ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xq)
| xr != sdtmndt0(xq,xp)
| ~ sdtlseqdt0(xp,xq)
| aNaturalNumber0(xr) ),
inference(instantiation,[status(thm)],[27]) ).
fof(m__1422,plain,
( aNaturalNumber0(xr)
& sdtpldt0(xp,xr) = xq
& xr = sdtmndt0(xq,xp) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1422) ).
cnf(76,plain,
xr = sdtmndt0(xq,xp),
inference(cnf,[status(esa)],[m__1422]) ).
cnf(l30,plain,
xr = sdtmndt0(xq,xp),
inference(instantiation,[status(thm)],[76]) ).
fof(m__1360,plain,
( aNaturalNumber0(xp)
& xm = sdtasdt0(xl,xp)
& xp = sdtsldt0(xm,xl) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1360) ).
cnf(65,plain,
aNaturalNumber0(xp),
inference(cnf,[status(esa)],[m__1360]) ).
cnf(l87,plain,
aNaturalNumber0(xp),
inference(instantiation,[status(thm)],[65]) ).
cnf(67,plain,
xp = sdtsldt0(xm,xl),
inference(cnf,[status(esa)],[m__1360]) ).
cnf(l154,plain,
xp = sdtsldt0(xm,xl),
inference(instantiation,[status(thm)],[67]) ).
fof(m__1324_04,plain,
( ? [W0] :
( aNaturalNumber0(W0)
& xm = sdtasdt0(xl,W0) )
& doDivides0(xl,xm)
& ? [W0] :
( aNaturalNumber0(W0)
& sdtpldt0(xm,xn) = sdtasdt0(xl,W0) )
& doDivides0(xl,sdtpldt0(xm,xn)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1324_04) ).
cnf(60,plain,
doDivides0(xl,xm),
inference(cnf,[status(esa)],[m__1324_04]) ).
cnf(l153,plain,
doDivides0(xl,xm),
inference(instantiation,[status(thm)],[60]) ).
fof(m__1395,plain,
( ? [W0] :
( aNaturalNumber0(W0)
& sdtpldt0(xp,W0) = xq )
& sdtlseqdt0(xp,xq) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1395) ).
cnf(73,plain,
sdtlseqdt0(xp,xq),
inference(cnf,[status(esa)],[m__1395]) ).
cnf(l88,plain,
sdtlseqdt0(xp,xq),
inference(instantiation,[status(thm)],[73]) ).
cnf(l91,plain,
aNaturalNumber0(xl),
inference(instantiation,[status(thm)],[55]) ).
fof(m__1347,plain,
xl != sz00,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1347) ).
cnf(64,plain,
xl != sz00,
inference(cnf,[status(esa)],[m__1347]) ).
cnf(l157,plain,
xl != sz00,
inference(instantiation,[status(thm)],[64]) ).
fof(m__1379,plain,
( aNaturalNumber0(xq)
& sdtpldt0(xm,xn) = sdtasdt0(xl,xq)
& xq = sdtsldt0(sdtpldt0(xm,xn),xl) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m__1379) ).
cnf(68,plain,
aNaturalNumber0(xq),
inference(cnf,[status(esa)],[m__1379]) ).
cnf(l34,plain,
aNaturalNumber0(xq),
inference(instantiation,[status(thm)],[68]) ).
cnf(51,plain,
( ~ aNaturalNumber0(X0)
| ~ aNaturalNumber0(X1)
| X2 != sdtsldt0(X1,X0)
| ~ doDivides0(X0,X1)
| X0 = sz00
| X1 = sdtasdt0(X0,X2) ),
inference(cnf,[status(esa)],[mDefQuot]) ).
cnf(l56,plain,
( ~ aNaturalNumber0(xl)
| ~ aNaturalNumber0(xm)
| xp != sdtsldt0(xm,xl)
| ~ doDivides0(xl,xm)
| xl = sz00
| xm = sdtasdt0(xl,xp) ),
inference(instantiation,[status(thm)],[51]) ).
cnf(l285,plain,
doDivides0(xl,xm),
inference(instantiation,[status(thm)],[60]) ).
cnf(l240,plain,
xp = sdtsldt0(xm,xl),
inference(instantiation,[status(thm)],[67]) ).
cnf(75,plain,
sdtpldt0(xp,xr) = xq,
inference(cnf,[status(esa)],[m__1422]) ).
cnf(l166,plain,
sdtpldt0(xp,xr) = xq,
inference(instantiation,[status(thm)],[75]) ).
cnf(l242,plain,
aNaturalNumber0(xl),
inference(instantiation,[status(thm)],[55]) ).
cnf(l195,plain,
aNaturalNumber0(xm),
inference(instantiation,[status(thm)],[56]) ).
cnf(69,plain,
sdtpldt0(xm,xn) = sdtasdt0(xl,xq),
inference(cnf,[status(esa)],[m__1379]) ).
cnf(l390,plain,
sdtpldt0(xm,xn) = sdtasdt0(xl,xq),
inference(instantiation,[status(thm)],[69]) ).
cnf(l372,plain,
xl != sz00,
inference(instantiation,[status(thm)],[64]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l17,l28,l158,l152,l27,l30,l87,l154,l153,l88,l91,l157,l34,l56,l285,l240,l166,l242,l195,l390,l372]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : NUM474+2 : TPTP v9.0.0. Released v4.0.0.
% 0.10/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.33 % Computer : n029.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 12:20:19 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.33 % launching worker at depth: 1
% 0.12/0.33 % launching worker at depth: 5
% 0.12/0.33 % launching worker at depth: 4
% 0.12/0.33 % launching worker at depth: 3
% 0.12/0.33 % launching worker at depth: 2
% 0.12/0.33 % launching worker at depth: 6
% 0.12/0.33 % launching worker at depth: 7
% 0.12/0.33 % launching worker at depth: 8
% 0.12/0.34 % launching worker at depth: 9
% 0.12/0.34 % launching worker at depth: 10
% 0.12/0.38 % launching worker at depth: 11
% 9.55/1.54 % launching worker at depth: 12
% 234.89/29.98 % SZS status Theorem for theBenchmark
% 234.89/29.98 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------