%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM483+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 : n020.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:09 AM UTC 2026
% Result : Theorem 21.60s 3.28s
% Output : CNFRefutation 21.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 18
% Syntax : Number of formulae : 146 ( 35 unt; 0 def)
% Number of atoms : 512 ( 204 equ)
% Maximal formula atoms : 32 ( 3 avg)
% Number of connectives : 567 ( 201 ~; 289 |; 53 &)
% ( 2 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 95 ( 0 sgn 40 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mSortsC_01,axiom,
( sz10 != sz00
& aNaturalNumber0(sz10) ),
file('theBenchmark.p',mSortsC_01) ).
fof(mSortsB_02,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> aNaturalNumber0(sdtasdt0(W0,W1)) ),
file('theBenchmark.p',mSortsB_02) ).
fof(m_MulUnit,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
file('theBenchmark.p',m_MulUnit) ).
fof(m_MulZero,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( sz00 = sdtasdt0(sz00,W0)
& sdtasdt0(W0,sz00) = sz00 ) ),
file('theBenchmark.p',m_MulZero) ).
fof(mMulCanc,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 != sz00
=> ! [W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1) )
=> ( ( sdtasdt0(W1,W0) = sdtasdt0(W2,W0)
| sdtasdt0(W0,W1) = sdtasdt0(W0,W2) )
=> W1 = W2 ) ) ) ),
file('theBenchmark.p',mMulCanc) ).
fof(mLEAsym,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('theBenchmark.p',mLEAsym) ).
fof(mMonMul2,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( W0 != sz00
=> sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ),
file('theBenchmark.p',mMonMul2) ).
fof(mIH_03,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W0,W1)
& W0 != W1 )
=> iLess0(W0,W1) ) ),
file('theBenchmark.p',mIH_03) ).
fof(mDefDiv,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( doDivides0(W0,W1)
<=> ? [W2] :
( W1 = sdtasdt0(W0,W2)
& aNaturalNumber0(W2) ) ) ),
file('theBenchmark.p',mDefDiv) ).
fof(mDivTrans,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( doDivides0(W1,W2)
& doDivides0(W0,W1) )
=> doDivides0(W0,W2) ) ),
file('theBenchmark.p',mDivTrans) ).
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__1700,axiom,
! [W0] :
( ( W0 != sz10
& W0 != sz00
& aNaturalNumber0(W0) )
=> ( iLess0(W0,xk)
=> ? [W1] :
( isPrime0(W1)
& doDivides0(W1,W0)
& aNaturalNumber0(W1) ) ) ),
file('theBenchmark.p',m__1700) ).
fof(m__1716_04,axiom,
( xk != sz10
& xk != sz00 ),
file('theBenchmark.p',m__1716_04) ).
fof(m__,conjecture,
? [W0] :
( isPrime0(W0)
& doDivides0(W0,xk)
& aNaturalNumber0(W0) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ? [W0] :
( isPrime0(W0)
& doDivides0(W0,xk)
& aNaturalNumber0(W0) ),
inference(assume_negation,[status(cth)],[m__]) ).
fof(mSortsC,axiom,
aNaturalNumber0(sz00),
file('theBenchmark.p',mSortsC) ).
cnf(c_40,plain,
aNaturalNumber0(sz00),
inference(clausify,[status(thm)],[mSortsC]) ).
cnf(c_41,plain,
aNaturalNumber0(sz10),
inference(clausify,[status(thm)],[mSortsC_01]) ).
cnf(c_44,plain,
( aNaturalNumber0(sdtasdt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mSortsB_02]) ).
cnf(c_52,plain,
( sdtasdt0(sz10,A) = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_MulUnit]) ).
cnf(c_53,plain,
( sdtasdt0(A,sz00) = sz00
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_MulZero]) ).
cnf(c_62,plain,
( C = B
| sdtasdt0(C,A) != sdtasdt0(B,A)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mMulCanc]) ).
cnf(c_75,plain,
( B = A
| ~ sdtlseqdt0(B,A)
| ~ sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLEAsym]) ).
cnf(c_84,plain,
( sdtlseqdt0(B,sdtasdt0(B,A))
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mMonMul2]) ).
cnf(c_85,plain,
( iLess0(A,B)
| ~ sdtlseqdt0(A,B)
| B = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mIH_03]) ).
cnf(c_88,plain,
( sdtasdt0(A,C) != B
| ~ aNaturalNumber0(C)
| doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefDiv]) ).
cnf(c_92,plain,
( doDivides0(A,C)
| ~ doDivides0(B,C)
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDivTrans]) ).
cnf(c_95,plain,
( sdtlseqdt0(A,B)
| B = sz00
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDivLE]) ).
cnf(c_96,plain,
( sdtlseqdt0(A,B)
| sz00 = B
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_95]) ).
fof(nnf_36,plain,
! [W0] :
( ( ( ? [W1] :
( W1 != W0
& W1 != sz10
& doDivides0(W1,W0)
& aNaturalNumber0(W1) )
| sz10 = W0
| sz00 = W0
| isPrime0(W0) )
& ( ( ! [X0] :
( X0 = W0
| X0 = sz10
| ~ doDivides0(X0,W0)
| ~ aNaturalNumber0(X0) )
& sz10 != W0
& sz00 != W0 )
| ~ isPrime0(W0) ) )
| ~ aNaturalNumber0(W0) ),
inference(fof_nnf,[status(thm)],[mDefPrime]) ).
fof(sk_mDefPrime_sk,plain,
! [W0] :
( ( ( ( sK0(W0) != W0
& sK0(W0) != sz10
& doDivides0(sK0(W0),W0)
& aNaturalNumber0(sK0(W0)) )
| sz10 = W0
| sz00 = W0
| isPrime0(W0) )
& ( ( ! [X0] :
( X0 = W0
| X0 = sz10
| ~ doDivides0(X0,W0)
| ~ aNaturalNumber0(X0) )
& sz10 != W0
& sz00 != W0 )
| ~ isPrime0(W0) ) )
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(W1,sK0(W0))],[nnf_36]) ).
fof(sk_mDefPrime,plain,
( ! [VAR_0] :
( sK0(VAR_0) != VAR_0
| sz10 = VAR_0
| sz00 = VAR_0
| isPrime0(VAR_0)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( sK0(VAR_0) != sz10
| sz10 = VAR_0
| sz00 = VAR_0
| isPrime0(VAR_0)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( doDivides0(sK0(VAR_0),VAR_0)
| sz10 = VAR_0
| sz00 = VAR_0
| isPrime0(VAR_0)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( aNaturalNumber0(sK0(VAR_0))
| sz10 = VAR_0
| sz00 = VAR_0
| isPrime0(VAR_0)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1] :
( VAR_1 = VAR_0
| VAR_1 = sz10
| ~ doDivides0(VAR_1,VAR_0)
| ~ aNaturalNumber0(VAR_1)
| ~ isPrime0(VAR_0)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( sz10 != VAR_0
| ~ isPrime0(VAR_0)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( sz00 != VAR_0
| ~ isPrime0(VAR_0)
| ~ aNaturalNumber0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_mDefPrime_sk]) ).
cnf(c_102,plain,
( aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefPrime]) ).
cnf(c_103,plain,
( doDivides0(sK0(A),A)
| sz10 = A
| sz00 = A
| isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefPrime]) ).
cnf(c_104,plain,
( sK0(A) != sz10
| sz10 = A
| sz00 = A
| isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefPrime]) ).
cnf(c_105,plain,
( sK0(A) != A
| sz10 = A
| sz00 = A
| isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefPrime]) ).
fof(m__1716,axiom,
aNaturalNumber0(xk),
file('theBenchmark.p',m__1716) ).
cnf(c_106,plain,
aNaturalNumber0(xk),
inference(clausify,[status(thm)],[m__1716]) ).
fof(nnf_37,plain,
! [W0] :
( ? [W1] :
( isPrime0(W1)
& doDivides0(W1,W0)
& aNaturalNumber0(W1) )
| ~ iLess0(W0,xk)
| sz10 = W0
| sz00 = W0
| ~ aNaturalNumber0(W0) ),
inference(fof_nnf,[status(thm)],[m__1700]) ).
fof(sk_m__1700_sk,plain,
! [W0] :
( ( isPrime0(sK1(W0))
& doDivides0(sK1(W0),W0)
& aNaturalNumber0(sK1(W0)) )
| ~ iLess0(W0,xk)
| sz10 = W0
| sz00 = W0
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(W1,sK1(W0))],[nnf_37]) ).
fof(sk_m__1700,plain,
( ! [VAR_0] :
( isPrime0(sK1(VAR_0))
| ~ iLess0(VAR_0,xk)
| sz10 = VAR_0
| sz00 = VAR_0
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( doDivides0(sK1(VAR_0),VAR_0)
| ~ iLess0(VAR_0,xk)
| sz10 = VAR_0
| sz00 = VAR_0
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( aNaturalNumber0(sK1(VAR_0))
| ~ iLess0(VAR_0,xk)
| sz10 = VAR_0
| sz00 = VAR_0
| ~ aNaturalNumber0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_m__1700_sk]) ).
cnf(c_107,plain,
( aNaturalNumber0(sK1(A))
| ~ iLess0(A,xk)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_m__1700]) ).
cnf(c_108,plain,
( doDivides0(sK1(A),A)
| ~ iLess0(A,xk)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_m__1700]) ).
cnf(c_109,plain,
( isPrime0(sK1(A))
| ~ iLess0(A,xk)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_m__1700]) ).
cnf(c_110,plain,
xk != sz00,
inference(clausify,[status(thm)],[m__1716_04]) ).
cnf(c_111,plain,
xk != sz10,
inference(clausify,[status(thm)],[m__1716_04]) ).
fof(m__1725,axiom,
~ isPrime0(xk),
file('theBenchmark.p',m__1725) ).
cnf(c_112,plain,
~ isPrime0(xk),
inference(clausify,[status(thm)],[m__1725]) ).
cnf(c_113,negated_conjecture,
( ~ isPrime0(A)
| ~ doDivides0(A,xk)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_115,plain,
( aNaturalNumber0(sdtasdt0(A,A))
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_44]) ).
cnf(c_159,plain,
( sdtlseqdt0(A,sdtasdt0(A,A))
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_84]) ).
cnf(c_4375,plain,
( sK0(xk) != xk
| sz10 = xk
| sz00 = xk
| isPrime0(xk) ),
inference(resolve,[status(thm)],[c_106,c_105]) ).
cnf(c_4376,plain,
( sK0(xk) != xk
| sz10 = xk
| xk = sz00
| isPrime0(xk) ),
inference(copy,[status(thm)],[c_4375]) ).
cnf(c_4377,plain,
( sK0(xk) != xk
| xk = sz10
| xk = sz00
| isPrime0(xk) ),
inference(copy,[status(thm)],[c_4376]) ).
cnf(c_4378,plain,
( sK0(xk) != xk
| xk = sz10
| xk = sz00 ),
inference(resolve,[status(thm)],[c_112,c_4377]) ).
cnf(c_4379,plain,
( sK0(xk) != xk
| xk = sz10 ),
inference(resolve,[status(thm)],[c_110,c_4378]) ).
cnf(c_319,plain,
sK0(xk) != xk,
inference(resolve,[status(thm)],[c_111,c_4379]) ).
cnf(c_4380,plain,
( sK0(xk) != sz10
| sz10 = xk
| sz00 = xk
| isPrime0(xk) ),
inference(resolve,[status(thm)],[c_106,c_104]) ).
cnf(c_4381,plain,
( sK0(xk) != sz10
| sz10 = xk
| xk = sz00
| isPrime0(xk) ),
inference(copy,[status(thm)],[c_4380]) ).
cnf(c_4382,plain,
( sK0(xk) != sz10
| xk = sz10
| xk = sz00
| isPrime0(xk) ),
inference(copy,[status(thm)],[c_4381]) ).
cnf(c_4383,plain,
( sK0(xk) != sz10
| xk = sz10
| xk = sz00 ),
inference(resolve,[status(thm)],[c_112,c_4382]) ).
cnf(c_4384,plain,
( sK0(xk) != sz10
| xk = sz10 ),
inference(resolve,[status(thm)],[c_110,c_4383]) ).
cnf(c_320,plain,
sK0(xk) != sz10,
inference(resolve,[status(thm)],[c_111,c_4384]) ).
cnf(c_4385,plain,
( doDivides0(sK0(xk),xk)
| sz10 = xk
| sz00 = xk
| isPrime0(xk) ),
inference(resolve,[status(thm)],[c_106,c_103]) ).
cnf(c_4386,plain,
( doDivides0(sK0(xk),xk)
| sz10 = xk
| xk = sz00
| isPrime0(xk) ),
inference(copy,[status(thm)],[c_4385]) ).
cnf(c_4387,plain,
( doDivides0(sK0(xk),xk)
| xk = sz10
| xk = sz00
| isPrime0(xk) ),
inference(copy,[status(thm)],[c_4386]) ).
cnf(c_4388,plain,
( doDivides0(sK0(xk),xk)
| xk = sz10
| xk = sz00 ),
inference(resolve,[status(thm)],[c_112,c_4387]) ).
cnf(c_4389,plain,
( doDivides0(sK0(xk),xk)
| xk = sz10 ),
inference(resolve,[status(thm)],[c_110,c_4388]) ).
cnf(c_321,plain,
doDivides0(sK0(xk),xk),
inference(resolve,[status(thm)],[c_111,c_4389]) ).
cnf(c_4390,plain,
( aNaturalNumber0(sK0(xk))
| sz10 = xk
| sz00 = xk
| isPrime0(xk) ),
inference(resolve,[status(thm)],[c_106,c_102]) ).
cnf(c_4391,plain,
( aNaturalNumber0(sK0(xk))
| sz10 = xk
| xk = sz00
| isPrime0(xk) ),
inference(copy,[status(thm)],[c_4390]) ).
cnf(c_4392,plain,
( aNaturalNumber0(sK0(xk))
| xk = sz10
| xk = sz00
| isPrime0(xk) ),
inference(copy,[status(thm)],[c_4391]) ).
cnf(c_4393,plain,
( aNaturalNumber0(sK0(xk))
| xk = sz10
| xk = sz00 ),
inference(resolve,[status(thm)],[c_112,c_4392]) ).
cnf(c_4394,plain,
( aNaturalNumber0(sK0(xk))
| xk = sz10 ),
inference(resolve,[status(thm)],[c_110,c_4393]) ).
cnf(c_322,plain,
aNaturalNumber0(sK0(xk)),
inference(resolve,[status(thm)],[c_111,c_4394]) ).
cnf(c_357,plain,
sdtasdt0(sz10,xk) = xk,
inference(resolve,[status(thm)],[c_106,c_52]) ).
cnf(c_4395,plain,
( B = A
| sdtasdt0(B,xk) != sdtasdt0(A,xk)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A)
| sz00 = xk ),
inference(resolve,[status(thm)],[c_62,c_106]) ).
cnf(c_4396,plain,
sz00 != xk,
inference(copy,[status(thm)],[c_110]) ).
cnf(c_4397,plain,
( B = A
| sdtasdt0(B,xk) != sdtasdt0(A,xk)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4395,c_4396]) ).
cnf(c_4398,plain,
( A = sz10
| sdtasdt0(A,xk) != sdtasdt0(sz10,xk)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4397,c_41]) ).
cnf(c_4399,plain,
( xk = sz10
| sdtasdt0(xk,xk) != sdtasdt0(sz10,xk) ),
inference(resolve,[status(thm)],[c_4398,c_106]) ).
cnf(c_4400,plain,
sdtasdt0(xk,xk) != sdtasdt0(sz10,xk),
inference(resolve,[status(thm)],[c_4399,c_111]) ).
cnf(c_403,plain,
sdtasdt0(xk,xk) != xk,
inference(paramod,[status(thm)],[c_357,c_4400]) ).
cnf(c_410,plain,
aNaturalNumber0(sdtasdt0(xk,xk)),
inference(resolve,[status(thm)],[c_115,c_106]) ).
cnf(c_4401,plain,
( sdtlseqdt0(xk,sdtasdt0(xk,xk))
| sz00 = xk ),
inference(resolve,[status(thm)],[c_159,c_106]) ).
cnf(c_4402,plain,
( sdtlseqdt0(xk,sdtasdt0(xk,xk))
| xk = sz00 ),
inference(copy,[status(thm)],[c_4401]) ).
cnf(c_460,plain,
sdtlseqdt0(xk,sdtasdt0(xk,xk)),
inference(resolve,[status(thm)],[c_110,c_4402]) ).
cnf(c_4403,plain,
( sdtlseqdt0(sK0(xk),xk)
| sz00 = xk
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(sK0(xk)) ),
inference(resolve,[status(thm)],[c_321,c_96]) ).
cnf(c_4404,plain,
( sdtlseqdt0(sK0(xk),xk)
| xk = sz00
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(sK0(xk)) ),
inference(copy,[status(thm)],[c_4403]) ).
cnf(c_4405,plain,
( sdtlseqdt0(sK0(xk),xk)
| xk = sz00
| ~ aNaturalNumber0(xk) ),
inference(resolve,[status(thm)],[c_322,c_4404]) ).
cnf(c_4406,plain,
( sdtlseqdt0(sK0(xk),xk)
| xk = sz00 ),
inference(resolve,[status(thm)],[c_106,c_4405]) ).
cnf(c_684,plain,
sdtlseqdt0(sK0(xk),xk),
inference(resolve,[status(thm)],[c_110,c_4406]) ).
cnf(c_1071,plain,
sdtasdt0(sdtasdt0(xk,xk),sz00) = sz00,
inference(resolve,[status(thm)],[c_410,c_53]) ).
cnf(c_4407,plain,
( iLess0(sK0(xk),xk)
| xk = sK0(xk)
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(sK0(xk)) ),
inference(resolve,[status(thm)],[c_684,c_85]) ).
cnf(c_4408,plain,
( iLess0(sK0(xk),xk)
| sK0(xk) = xk
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(sK0(xk)) ),
inference(copy,[status(thm)],[c_4407]) ).
cnf(c_4409,plain,
( iLess0(sK0(xk),xk)
| sK0(xk) = xk
| ~ aNaturalNumber0(xk) ),
inference(resolve,[status(thm)],[c_322,c_4408]) ).
cnf(c_4410,plain,
( iLess0(sK0(xk),xk)
| sK0(xk) = xk ),
inference(resolve,[status(thm)],[c_106,c_4409]) ).
cnf(c_2604,plain,
iLess0(sK0(xk),xk),
inference(resolve,[status(thm)],[c_319,c_4410]) ).
cnf(c_4411,plain,
( isPrime0(sK1(sK0(xk)))
| sz10 = sK0(xk)
| sz00 = sK0(xk)
| ~ aNaturalNumber0(sK0(xk)) ),
inference(resolve,[status(thm)],[c_2604,c_109]) ).
cnf(c_4412,plain,
( isPrime0(sK1(sK0(xk)))
| sz10 = sK0(xk)
| sK0(xk) = sz00
| ~ aNaturalNumber0(sK0(xk)) ),
inference(copy,[status(thm)],[c_4411]) ).
cnf(c_4413,plain,
( isPrime0(sK1(sK0(xk)))
| sK0(xk) = sz10
| sK0(xk) = sz00
| ~ aNaturalNumber0(sK0(xk)) ),
inference(copy,[status(thm)],[c_4412]) ).
cnf(c_4414,plain,
( isPrime0(sK1(sK0(xk)))
| sK0(xk) = sz10
| sK0(xk) = sz00 ),
inference(resolve,[status(thm)],[c_322,c_4413]) ).
cnf(c_2617,plain,
( isPrime0(sK1(sK0(xk)))
| sK0(xk) = sz00 ),
inference(resolve,[status(thm)],[c_320,c_4414]) ).
cnf(c_4415,plain,
( doDivides0(sK1(sK0(xk)),sK0(xk))
| sz10 = sK0(xk)
| sz00 = sK0(xk)
| ~ aNaturalNumber0(sK0(xk)) ),
inference(resolve,[status(thm)],[c_2604,c_108]) ).
cnf(c_4416,plain,
( doDivides0(sK1(sK0(xk)),sK0(xk))
| sz10 = sK0(xk)
| sK0(xk) = sz00
| ~ aNaturalNumber0(sK0(xk)) ),
inference(copy,[status(thm)],[c_4415]) ).
cnf(c_4417,plain,
( doDivides0(sK1(sK0(xk)),sK0(xk))
| sK0(xk) = sz10
| sK0(xk) = sz00
| ~ aNaturalNumber0(sK0(xk)) ),
inference(copy,[status(thm)],[c_4416]) ).
cnf(c_4418,plain,
( doDivides0(sK1(sK0(xk)),sK0(xk))
| sK0(xk) = sz10
| sK0(xk) = sz00 ),
inference(resolve,[status(thm)],[c_322,c_4417]) ).
cnf(c_2618,plain,
( doDivides0(sK1(sK0(xk)),sK0(xk))
| sK0(xk) = sz00 ),
inference(resolve,[status(thm)],[c_320,c_4418]) ).
cnf(c_4419,plain,
( aNaturalNumber0(sK1(sK0(xk)))
| sz10 = sK0(xk)
| sz00 = sK0(xk)
| ~ aNaturalNumber0(sK0(xk)) ),
inference(resolve,[status(thm)],[c_2604,c_107]) ).
cnf(c_4420,plain,
( aNaturalNumber0(sK1(sK0(xk)))
| sz10 = sK0(xk)
| sK0(xk) = sz00
| ~ aNaturalNumber0(sK0(xk)) ),
inference(copy,[status(thm)],[c_4419]) ).
cnf(c_4421,plain,
( aNaturalNumber0(sK1(sK0(xk)))
| sK0(xk) = sz10
| sK0(xk) = sz00
| ~ aNaturalNumber0(sK0(xk)) ),
inference(copy,[status(thm)],[c_4420]) ).
cnf(c_4422,plain,
( aNaturalNumber0(sK1(sK0(xk)))
| sK0(xk) = sz10
| sK0(xk) = sz00 ),
inference(resolve,[status(thm)],[c_322,c_4421]) ).
cnf(c_2619,plain,
( aNaturalNumber0(sK1(sK0(xk)))
| sK0(xk) = sz00 ),
inference(resolve,[status(thm)],[c_320,c_4422]) ).
cnf(c_4423,plain,
( xk = sdtasdt0(xk,xk)
| ~ sdtlseqdt0(sdtasdt0(xk,xk),xk)
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(sdtasdt0(xk,xk)) ),
inference(resolve,[status(thm)],[c_460,c_75]) ).
cnf(c_4424,plain,
( sdtasdt0(xk,xk) = xk
| ~ sdtlseqdt0(sdtasdt0(xk,xk),xk)
| ~ aNaturalNumber0(xk)
| ~ aNaturalNumber0(sdtasdt0(xk,xk)) ),
inference(copy,[status(thm)],[c_4423]) ).
cnf(c_4425,plain,
( sdtasdt0(xk,xk) = xk
| ~ sdtlseqdt0(sdtasdt0(xk,xk),xk)
| ~ aNaturalNumber0(xk) ),
inference(resolve,[status(thm)],[c_410,c_4424]) ).
cnf(c_4426,plain,
( sdtasdt0(xk,xk) = xk
| ~ sdtlseqdt0(sdtasdt0(xk,xk),xk) ),
inference(resolve,[status(thm)],[c_106,c_4425]) ).
cnf(c_2990,plain,
~ sdtlseqdt0(sdtasdt0(xk,xk),xk),
inference(resolve,[status(thm)],[c_403,c_4426]) ).
cnf(c_4427,plain,
( sdtlseqdt0(sdtasdt0(xk,xk),A)
| sz00 = A
| ~ doDivides0(sdtasdt0(xk,xk),A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_96,c_410]) ).
cnf(c_4428,plain,
( sdtlseqdt0(sdtasdt0(xk,xk),xk)
| sz00 = xk
| ~ doDivides0(sdtasdt0(xk,xk),xk) ),
inference(resolve,[status(thm)],[c_4427,c_106]) ).
cnf(c_4429,plain,
sz00 != xk,
inference(copy,[status(thm)],[c_110]) ).
cnf(c_4430,plain,
( sdtlseqdt0(sdtasdt0(xk,xk),xk)
| ~ doDivides0(sdtasdt0(xk,xk),xk) ),
inference(resolve,[status(thm)],[c_4428,c_4429]) ).
cnf(c_3020,plain,
~ doDivides0(sdtasdt0(xk,xk),xk),
inference(resolve,[status(thm)],[c_4430,c_2990]) ).
cnf(c_4431,plain,
( doDivides0(sdtasdt0(xk,xk),B)
| ~ doDivides0(A,B)
| ~ doDivides0(sdtasdt0(xk,xk),A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_92,c_410]) ).
cnf(c_4432,plain,
( doDivides0(sdtasdt0(xk,xk),A)
| ~ doDivides0(sK0(xk),A)
| ~ doDivides0(sdtasdt0(xk,xk),sK0(xk))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4431,c_322]) ).
cnf(c_4433,plain,
( doDivides0(sdtasdt0(xk,xk),xk)
| ~ doDivides0(sK0(xk),xk)
| ~ doDivides0(sdtasdt0(xk,xk),sK0(xk)) ),
inference(resolve,[status(thm)],[c_4432,c_106]) ).
cnf(c_4434,plain,
( doDivides0(sdtasdt0(xk,xk),xk)
| ~ doDivides0(sdtasdt0(xk,xk),sK0(xk)) ),
inference(resolve,[status(thm)],[c_4433,c_321]) ).
cnf(c_3038,plain,
~ doDivides0(sdtasdt0(xk,xk),sK0(xk)),
inference(resolve,[status(thm)],[c_4434,c_3020]) ).
cnf(c_4435,plain,
( sdtasdt0(sdtasdt0(xk,xk),B) != A
| ~ aNaturalNumber0(B)
| doDivides0(sdtasdt0(xk,xk),A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_88,c_410]) ).
cnf(c_4436,plain,
( sdtasdt0(sdtasdt0(xk,xk),A) != sK0(xk)
| ~ aNaturalNumber0(A)
| doDivides0(sdtasdt0(xk,xk),sK0(xk)) ),
inference(resolve,[status(thm)],[c_4435,c_322]) ).
cnf(c_4437,plain,
( sdtasdt0(sdtasdt0(xk,xk),A) != sK0(xk)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4436,c_3038]) ).
cnf(c_4438,plain,
sdtasdt0(sdtasdt0(xk,xk),sz00) != sK0(xk),
inference(resolve,[status(thm)],[c_4437,c_40]) ).
cnf(c_4439,plain,
sz00 != sK0(xk),
inference(paramod,[status(thm)],[c_1071,c_4438]) ).
cnf(c_3376,plain,
sK0(xk) != sz00,
inference(copy,[status(thm)],[c_4439]) ).
cnf(c_3377,plain,
aNaturalNumber0(sK1(sK0(xk))),
inference(resolve,[status(thm)],[c_3376,c_2619]) ).
cnf(c_3378,plain,
doDivides0(sK1(sK0(xk)),sK0(xk)),
inference(resolve,[status(thm)],[c_3376,c_2618]) ).
cnf(c_3379,plain,
isPrime0(sK1(sK0(xk))),
inference(resolve,[status(thm)],[c_3376,c_2617]) ).
cnf(c_4440,negated_conjecture,
( ~ isPrime0(sK1(sK0(xk)))
| ~ doDivides0(sK1(sK0(xk)),xk) ),
inference(resolve,[status(thm)],[c_113,c_3377]) ).
cnf(c_3681,negated_conjecture,
~ doDivides0(sK1(sK0(xk)),xk),
inference(resolve,[status(thm)],[c_4440,c_3379]) ).
cnf(c_4441,plain,
( doDivides0(sK1(sK0(xk)),B)
| ~ doDivides0(A,B)
| ~ doDivides0(sK1(sK0(xk)),A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_92,c_3377]) ).
cnf(c_4442,plain,
( doDivides0(sK1(sK0(xk)),A)
| ~ doDivides0(sK0(xk),A)
| ~ doDivides0(sK1(sK0(xk)),sK0(xk))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4441,c_322]) ).
cnf(c_4443,plain,
( doDivides0(sK1(sK0(xk)),xk)
| ~ doDivides0(sK0(xk),xk)
| ~ doDivides0(sK1(sK0(xk)),sK0(xk)) ),
inference(resolve,[status(thm)],[c_4442,c_106]) ).
cnf(c_4444,plain,
( doDivides0(sK1(sK0(xk)),xk)
| ~ doDivides0(sK1(sK0(xk)),sK0(xk)) ),
inference(resolve,[status(thm)],[c_4443,c_321]) ).
cnf(c_4445,plain,
~ doDivides0(sK1(sK0(xk)),sK0(xk)),
inference(resolve,[status(thm)],[c_4444,c_3681]) ).
cnf(c_4374,plain,
$false,
inference(resolve,[status(thm)],[c_3378,c_4445]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM483+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.37 % Computer : n020.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Sat Sep 26 02:57:04 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37 % Process 459957 was started by sandbox2 on n020,
% 0.08/0.37 % Sat Sep 26 02:57:04 2026
% 0.08/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.39
% 0.08/0.39 % From the command line: assign(max_seconds, 300).
% 21.60/3.28
% 21.60/3.28 % SZS status Theorem for theBenchmark
% 21.60/3.28
% 21.60/3.28 % Proof 1 at 2.71 (+ 0.13) seconds.
% 21.60/3.28 % Length of proof is 65.
% 21.60/3.28 % Level of proof is 10.
% 21.60/3.28 % Maximum clause weight is 19.000.
% 21.60/3.28 % Given clauses 262.
% 21.60/3.28
% 21.60/3.28 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------