%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM518+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:17:15 AM UTC 2026
% Result : Theorem 31.95s 5.21s
% Output : CNFRefutation 31.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 15
% Syntax : Number of formulae : 94 ( 30 unt; 0 def)
% Number of atoms : 276 ( 82 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 319 ( 137 ~; 137 |; 30 &)
% ( 3 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 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 : 63 ( 0 sgn 28 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(m_MulZero,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 ) ),
file('theBenchmark.p',m_MulZero) ).
fof(mLEAsym,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('theBenchmark.p',mLEAsym) ).
fof(mLETran,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W2)
& sdtlseqdt0(W0,W1) )
=> sdtlseqdt0(W0,W2) ) ),
file('theBenchmark.p',mLETran) ).
fof(mDefDiv,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( doDivides0(W0,W1)
<=> ? [W2] :
( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) ) ),
file('theBenchmark.p',mDefDiv) ).
fof(mDefQuot,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( doDivides0(W0,W1)
& W0 != sz00 )
=> ! [W2] :
( W2 = sdtsldt0(W1,W0)
<=> ( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) ) ) ),
file('theBenchmark.p',mDefQuot) ).
fof(mDivLE,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( W1 != sz00
& doDivides0(W0,W1) )
=> sdtlseqdt0(W0,W1) ) ),
file('theBenchmark.p',mDivLE) ).
fof(mDefPrime,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( isPrime0(W0)
<=> ( ! [W1] :
( ( doDivides0(W1,W0)
& aNaturalNumber0(W1) )
=> ( W1 = W0
| W1 = sz10 ) )
& W0 != sz10
& W0 != sz00 ) ) ),
file('theBenchmark.p',mDefPrime) ).
fof(m__1837,axiom,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('theBenchmark.p',m__1837) ).
fof(m__2287,axiom,
( sdtlseqdt0(xm,xp)
& xm != xp
& sdtlseqdt0(xn,xp)
& xn != xp ),
file('theBenchmark.p',m__2287) ).
fof(m__2342,axiom,
( isPrime0(xr)
& doDivides0(xr,xk)
& aNaturalNumber0(xr) ),
file('theBenchmark.p',m__2342) ).
fof(m__2504,axiom,
( sdtlseqdt0(sdtsldt0(xn,xr),xn)
& sdtsldt0(xn,xr) != xn ),
file('theBenchmark.p',m__2504) ).
fof(m__,conjecture,
( doDivides0(xp,xm)
| doDivides0(xp,xn) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( doDivides0(xp,xm)
| doDivides0(xp,xn) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_52,plain,
( sz00 != A
| ~ isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefPrime]) ).
cnf(c_59,plain,
isPrime0(xr),
inference(clausify,[status(thm)],[m__2342]) ).
cnf(c_60,plain,
( sz00 != xr
| ~ aNaturalNumber0(xr) ),
inference(resolve,[status(thm)],[c_59,c_52]) ).
cnf(c_61,plain,
( xr != sz00
| ~ aNaturalNumber0(xr) ),
inference(copy,[status(thm)],[c_60]) ).
cnf(c_97,negated_conjecture,
~ doDivides0(xp,xm),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_98,negated_conjecture,
~ doDivides0(xp,xn),
inference(clausify,[status(thm)],[m___neg]) ).
fof(m__2645,axiom,
( doDivides0(xp,xm)
| doDivides0(xp,sdtsldt0(xn,xr)) ),
file('theBenchmark.p',m__2645) ).
cnf(c_99,plain,
( doDivides0(xp,xm)
| doDivides0(xp,sdtsldt0(xn,xr)) ),
inference(clausify,[status(thm)],[m__2645]) ).
cnf(c_100,negated_conjecture,
doDivides0(xp,sdtsldt0(xn,xr)),
inference(resolve,[status(thm)],[c_97,c_99]) ).
cnf(c_102,plain,
sdtlseqdt0(sdtsldt0(xn,xr),xn),
inference(clausify,[status(thm)],[m__2504]) ).
cnf(c_103,plain,
sdtsldt0(xn,xr) != xn,
inference(clausify,[status(thm)],[m__2504]) ).
fof(m__2487,axiom,
doDivides0(xr,xn),
file('theBenchmark.p',m__2487) ).
cnf(c_104,plain,
doDivides0(xr,xn),
inference(clausify,[status(thm)],[m__2487]) ).
cnf(c_110,plain,
aNaturalNumber0(xr),
inference(clausify,[status(thm)],[m__2342]) ).
cnf(c_117,plain,
sdtlseqdt0(xn,xp),
inference(clausify,[status(thm)],[m__2287]) ).
cnf(c_123,plain,
aNaturalNumber0(xp),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_125,plain,
aNaturalNumber0(xn),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_129,plain,
( sdtlseqdt0(A,B)
| B = sz00
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDivLE]) ).
cnf(c_130,plain,
( sdtlseqdt0(A,B)
| sz00 = B
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_129]) ).
cnf(c_134,plain,
( sdtasdt0(A,C) != B
| ~ aNaturalNumber0(C)
| sdtsldt0(B,A) = C
| ~ doDivides0(A,B)
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefQuot]) ).
fof(nnf_29,plain,
! [W0,W1] :
( ( ( ! [W2] :
( sdtasdt0(W0,W2) != W1
| ~ aNaturalNumber0(W2) )
| doDivides0(W0,W1) )
& ( ? [X0] :
( sdtasdt0(W0,X0) = W1
& aNaturalNumber0(X0) )
| ~ doDivides0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(fof_nnf,[status(thm)],[mDefDiv]) ).
fof(sk_mDefDiv_sk,plain,
! [W0,W1] :
( ( ( ! [W2] :
( sdtasdt0(W0,W2) != W1
| ~ aNaturalNumber0(W2) )
| doDivides0(W0,W1) )
& ( ( sdtasdt0(W0,sK0(W0,W1)) = W1
& aNaturalNumber0(sK0(W0,W1)) )
| ~ doDivides0(W0,W1) ) )
| ~ aNaturalNumber0(W1)
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0(W0,W1))],[nnf_29]) ).
fof(sk_mDefDiv,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( sdtasdt0(VAR_0,VAR_2) != VAR_1
| ~ aNaturalNumber0(VAR_2)
| doDivides0(VAR_0,VAR_1)
| ~ aNaturalNumber0(VAR_1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(VAR_0,sK0(VAR_0,VAR_1)) = VAR_1
| ~ doDivides0(VAR_0,VAR_1)
| ~ aNaturalNumber0(VAR_1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aNaturalNumber0(sK0(VAR_0,VAR_1))
| ~ doDivides0(VAR_0,VAR_1)
| ~ aNaturalNumber0(VAR_1)
| ~ aNaturalNumber0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_mDefDiv_sk]) ).
cnf(c_137,plain,
( sdtasdt0(A,C) != B
| ~ aNaturalNumber0(C)
| doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefDiv]) ).
cnf(c_138,plain,
( sdtasdt0(A,sK0(A,B)) = B
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefDiv]) ).
cnf(c_139,plain,
( aNaturalNumber0(sK0(A,B))
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefDiv]) ).
cnf(c_153,plain,
( sdtlseqdt0(A,C)
| ~ sdtlseqdt0(B,C)
| ~ sdtlseqdt0(A,B)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLETran]) ).
cnf(c_154,plain,
( B = A
| ~ sdtlseqdt0(B,A)
| ~ sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLEAsym]) ).
cnf(c_174,plain,
( sdtasdt0(A,sz00) = sz00
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_MulZero]) ).
fof(mSortsC,axiom,
aNaturalNumber0(sz00),
file('theBenchmark.p',mSortsC) ).
cnf(c_187,plain,
aNaturalNumber0(sz00),
inference(clausify,[status(thm)],[mSortsC]) ).
cnf(c_217,plain,
xr != sz00,
inference(resolve,[status(thm)],[c_110,c_61]) ).
cnf(c_594,plain,
( sdtlseqdt0(xp,A)
| sz00 = A
| ~ doDivides0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_130,c_123]) ).
cnf(c_20928,plain,
( sdtasdt0(xr,A) != xn
| ~ aNaturalNumber0(A)
| sdtsldt0(xn,xr) = A
| sz00 = xr
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xr) ),
inference(resolve,[status(thm)],[c_134,c_104]) ).
cnf(c_20929,plain,
( sdtasdt0(xr,A) != xn
| ~ aNaturalNumber0(A)
| sdtsldt0(xn,xr) = A
| xr = sz00
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xr) ),
inference(copy,[status(thm)],[c_20928]) ).
cnf(c_20930,plain,
( sdtasdt0(xr,A) != xn
| ~ aNaturalNumber0(A)
| sdtsldt0(xn,xr) = A
| xr = sz00
| ~ aNaturalNumber0(xn) ),
inference(resolve,[status(thm)],[c_110,c_20929]) ).
cnf(c_20931,plain,
( sdtasdt0(xr,A) != xn
| ~ aNaturalNumber0(A)
| sdtsldt0(xn,xr) = A
| xr = sz00 ),
inference(resolve,[status(thm)],[c_125,c_20930]) ).
cnf(c_716,plain,
( sdtasdt0(xr,A) != xn
| ~ aNaturalNumber0(A)
| sdtsldt0(xn,xr) = A ),
inference(resolve,[status(thm)],[c_217,c_20931]) ).
cnf(c_20932,plain,
( sdtasdt0(xr,sK0(xr,xn)) = xn
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xr) ),
inference(resolve,[status(thm)],[c_138,c_104]) ).
cnf(c_20933,plain,
( sdtasdt0(xr,sK0(xr,xn)) = xn
| ~ aNaturalNumber0(xn) ),
inference(resolve,[status(thm)],[c_110,c_20932]) ).
cnf(c_809,plain,
sdtasdt0(xr,sK0(xr,xn)) = xn,
inference(resolve,[status(thm)],[c_125,c_20933]) ).
cnf(c_20934,plain,
( aNaturalNumber0(sK0(xr,xn))
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xr) ),
inference(resolve,[status(thm)],[c_139,c_104]) ).
cnf(c_20935,plain,
( aNaturalNumber0(sK0(xr,xn))
| ~ aNaturalNumber0(xn) ),
inference(resolve,[status(thm)],[c_110,c_20934]) ).
cnf(c_822,plain,
aNaturalNumber0(sK0(xr,xn)),
inference(resolve,[status(thm)],[c_125,c_20935]) ).
cnf(c_20936,plain,
( sdtlseqdt0(xn,A)
| ~ sdtlseqdt0(xp,A)
| ~ aNaturalNumber0(A)
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xn) ),
inference(resolve,[status(thm)],[c_153,c_117]) ).
cnf(c_20937,plain,
( sdtlseqdt0(xn,A)
| ~ sdtlseqdt0(xp,A)
| ~ aNaturalNumber0(A)
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_125,c_20936]) ).
cnf(c_976,plain,
( sdtlseqdt0(xn,A)
| ~ sdtlseqdt0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_123,c_20937]) ).
cnf(c_20938,plain,
( xn = sdtsldt0(xn,xr)
| ~ sdtlseqdt0(xn,sdtsldt0(xn,xr))
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(resolve,[status(thm)],[c_154,c_102]) ).
cnf(c_20939,plain,
( sdtsldt0(xn,xr) = xn
| ~ sdtlseqdt0(xn,sdtsldt0(xn,xr))
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(copy,[status(thm)],[c_20938]) ).
cnf(c_20940,plain,
( sdtsldt0(xn,xr) = xn
| ~ sdtlseqdt0(xn,sdtsldt0(xn,xr))
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(resolve,[status(thm)],[c_125,c_20939]) ).
cnf(c_986,plain,
( ~ sdtlseqdt0(xn,sdtsldt0(xn,xr))
| ~ aNaturalNumber0(sdtsldt0(xn,xr)) ),
inference(resolve,[status(thm)],[c_103,c_20940]) ).
cnf(c_1219,plain,
sdtasdt0(xp,sz00) = sz00,
inference(resolve,[status(thm)],[c_174,c_123]) ).
cnf(c_1220,plain,
sdtasdt0(xr,sz00) = sz00,
inference(resolve,[status(thm)],[c_174,c_110]) ).
cnf(c_3621,plain,
( sdtlseqdt0(xn,sK0(xr,xn))
| ~ sdtlseqdt0(xp,sK0(xr,xn)) ),
inference(resolve,[status(thm)],[c_822,c_976]) ).
cnf(c_20941,plain,
( sz00 != A
| ~ aNaturalNumber0(sz00)
| doDivides0(xp,A)
| ~ aNaturalNumber0(A)
| ~ aNaturalNumber0(xp) ),
inference(paramod,[status(thm)],[c_1219,c_137]) ).
cnf(c_20942,plain,
( sz00 != A
| ~ aNaturalNumber0(sz00)
| doDivides0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_123,c_20941]) ).
cnf(c_12483,plain,
( sz00 != A
| doDivides0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_187,c_20942]) ).
cnf(c_20943,plain,
( sz00 != xn
| doDivides0(xp,xn) ),
inference(resolve,[status(thm)],[c_12483,c_125]) ).
cnf(c_20944,plain,
( xn != sz00
| doDivides0(xp,xn) ),
inference(copy,[status(thm)],[c_20943]) ).
cnf(c_12514,negated_conjecture,
xn != sz00,
inference(resolve,[status(thm)],[c_98,c_20944]) ).
cnf(c_20945,plain,
( sdtlseqdt0(xp,sK0(xr,xn))
| sz00 = sK0(xr,xn)
| ~ doDivides0(xp,sK0(xr,xn)) ),
inference(resolve,[status(thm)],[c_594,c_822]) ).
cnf(c_16819,plain,
( sdtlseqdt0(xp,sK0(xr,xn))
| sK0(xr,xn) = sz00
| ~ doDivides0(xp,sK0(xr,xn)) ),
inference(copy,[status(thm)],[c_20945]) ).
cnf(c_20946,plain,
( sdtasdt0(xr,sK0(xr,xn)) != xn
| sdtsldt0(xn,xr) = sK0(xr,xn) ),
inference(resolve,[status(thm)],[c_716,c_822]) ).
cnf(c_20947,plain,
( xn != xn
| sdtsldt0(xn,xr) = sK0(xr,xn) ),
inference(paramod,[status(thm)],[c_809,c_20946]) ).
cnf(c_20948,plain,
( xn != xn
| sK0(xr,xn) = sdtsldt0(xn,xr) ),
inference(copy,[status(thm)],[c_20947]) ).
cnf(c_20781,plain,
sK0(xr,xn) = sdtsldt0(xn,xr),
inference(copy,[status(thm)],[c_20948]) ).
cnf(c_20949,plain,
( sdtlseqdt0(xp,sK0(xr,xn))
| sK0(xr,xn) = sz00
| ~ doDivides0(xp,sdtsldt0(xn,xr)) ),
inference(paramod,[status(thm)],[c_20781,c_16819]) ).
cnf(c_20950,plain,
( sdtlseqdt0(xp,sK0(xr,xn))
| sdtsldt0(xn,xr) = sz00
| ~ doDivides0(xp,sdtsldt0(xn,xr)) ),
inference(paramod,[status(thm)],[c_20781,c_20949]) ).
cnf(c_20951,plain,
( sdtlseqdt0(xp,sdtsldt0(xn,xr))
| sdtsldt0(xn,xr) = sz00
| ~ doDivides0(xp,sdtsldt0(xn,xr)) ),
inference(paramod,[status(thm)],[c_20781,c_20950]) ).
cnf(c_20826,plain,
( sdtlseqdt0(xp,sdtsldt0(xn,xr))
| sdtsldt0(xn,xr) = sz00 ),
inference(resolve,[status(thm)],[c_100,c_20951]) ).
cnf(c_20952,plain,
( sdtlseqdt0(xn,sK0(xr,xn))
| ~ sdtlseqdt0(xp,sdtsldt0(xn,xr)) ),
inference(paramod,[status(thm)],[c_20781,c_3621]) ).
cnf(c_20884,plain,
( sdtlseqdt0(xn,sdtsldt0(xn,xr))
| ~ sdtlseqdt0(xp,sdtsldt0(xn,xr)) ),
inference(paramod,[status(thm)],[c_20781,c_20952]) ).
cnf(c_20903,plain,
aNaturalNumber0(sdtsldt0(xn,xr)),
inference(paramod,[status(thm)],[c_20781,c_822]) ).
cnf(c_20904,plain,
sdtasdt0(xr,sdtsldt0(xn,xr)) = xn,
inference(paramod,[status(thm)],[c_20781,c_809]) ).
cnf(c_20914,plain,
~ sdtlseqdt0(xn,sdtsldt0(xn,xr)),
inference(resolve,[status(thm)],[c_20903,c_986]) ).
cnf(c_20922,plain,
~ sdtlseqdt0(xp,sdtsldt0(xn,xr)),
inference(resolve,[status(thm)],[c_20914,c_20884]) ).
cnf(c_20925,plain,
sdtsldt0(xn,xr) = sz00,
inference(resolve,[status(thm)],[c_20922,c_20826]) ).
cnf(c_20953,plain,
sdtasdt0(xr,sz00) = xn,
inference(paramod,[status(thm)],[c_20925,c_20904]) ).
cnf(c_20954,plain,
sz00 = xn,
inference(paramod,[status(thm)],[c_1220,c_20953]) ).
cnf(c_20955,plain,
xn = sz00,
inference(copy,[status(thm)],[c_20954]) ).
cnf(c_20927,plain,
$false,
inference(resolve,[status(thm)],[c_12514,c_20955]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM518+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n019.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 03:05:34 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 262544 was started by sandbox2 on n019,
% 0.08/0.35 % Sat Sep 26 03:05:34 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.37
% 0.13/0.37 % From the command line: assign(max_seconds, 300).
% 31.95/5.21
% 31.95/5.21 % given #500 (W,wt=14): 2134 aNaturalNumber0(sdtpldt0(xp,xp)). [resolve(302,a,123,a)].
% 31.95/5.21
% 31.95/5.21 % given #1000 (F,wt=18): 17044 -doDivides0(xn,xm) | -doDivides0(xn,sdtpldt0(xm,sz10)). [resolve(17006,a,124,a)].
% 31.95/5.21
% 31.95/5.21 % SZS status Theorem for theBenchmark
% 31.95/5.21
% 31.95/5.21 % Proof 1 at 3.52 (+ 1.01) seconds.
% 31.95/5.21 % Length of proof is 59.
% 31.95/5.21 % Level of proof is 11.
% 31.95/5.21 % Maximum clause weight is 32.000.
% 31.95/5.21 % Given clauses 1450.
% 31.95/5.21
% 31.95/5.21 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------