%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM481+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 : n014.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:08 AM UTC 2026
% Result : Theorem 39.55s 10.69s
% Output : CNFRefutation 39.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 14
% Syntax : Number of formulae : 160 ( 35 unt; 0 def)
% Number of atoms : 630 ( 238 equ)
% Maximal formula atoms : 32 ( 3 avg)
% Number of connectives : 771 ( 301 ~; 368 |; 72 &)
% ( 2 <=>; 28 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 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 : 122 ( 0 sgn 46 !; 8 ?)
% 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__,conjecture,
! [W0] :
( ( W0 != sz10
& W0 != sz00
& aNaturalNumber0(W0) )
=> ( ! [W1] :
( ( W1 != sz10
& W1 != sz00
& aNaturalNumber0(W1) )
=> ( iLess0(W1,W0)
=> ? [W2] :
( isPrime0(W2)
& doDivides0(W2,W1)
& aNaturalNumber0(W2) ) ) )
=> ? [W1] :
( isPrime0(W1)
& doDivides0(W1,W0)
& aNaturalNumber0(W1) ) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ! [W0] :
( ( W0 != sz10
& W0 != sz00
& aNaturalNumber0(W0) )
=> ( ! [W1] :
( ( W1 != sz10
& W1 != sz00
& aNaturalNumber0(W1) )
=> ( iLess0(W1,W0)
=> ? [W2] :
( isPrime0(W2)
& doDivides0(W2,W1)
& aNaturalNumber0(W2) ) ) )
=> ? [W1] :
( isPrime0(W1)
& doDivides0(W1,W0)
& aNaturalNumber0(W1) ) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
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_38,plain,
( aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefPrime]) ).
cnf(c_42,plain,
( doDivides0(sK0(A),A)
| sz10 = A
| sz00 = A
| isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefPrime]) ).
cnf(c_43,plain,
( sK0(A) != sz10
| sz10 = A
| sz00 = A
| isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefPrime]) ).
cnf(c_44,plain,
( sK0(A) != A
| sz10 = A
| sz00 = A
| isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mDefPrime]) ).
fof(nnf_37,plain,
? [W0] :
( ! [W1] :
( ~ isPrime0(W1)
| ~ doDivides0(W1,W0)
| ~ aNaturalNumber0(W1) )
& ! [X0] :
( ? [W2] :
( isPrime0(W2)
& doDivides0(W2,X0)
& aNaturalNumber0(W2) )
| ~ iLess0(X0,W0)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) )
& sz10 != W0
& sz00 != W0
& aNaturalNumber0(W0) ),
inference(fof_nnf,[status(thm)],[m___neg]) ).
fof(sk_m___neg_sk,plain,
( ! [W1] :
( ~ isPrime0(W1)
| ~ doDivides0(W1,sK1)
| ~ aNaturalNumber0(W1) )
& ! [X0] :
( ( isPrime0(sK2(X0))
& doDivides0(sK2(X0),X0)
& aNaturalNumber0(sK2(X0)) )
| ~ iLess0(X0,sK1)
| X0 = sz10
| X0 = sz00
| ~ aNaturalNumber0(X0) )
& sz10 != sK1
& sz00 != sK1
& aNaturalNumber0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(W0,sK1),skolemize(W2,sK2(X0))],[nnf_37]) ).
fof(sk_m___neg,plain,
( ! [VAR_0] :
( ~ isPrime0(VAR_0)
| ~ doDivides0(VAR_0,sK1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( isPrime0(sK2(VAR_0))
| ~ iLess0(VAR_0,sK1)
| VAR_0 = sz10
| VAR_0 = sz00
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( doDivides0(sK2(VAR_0),VAR_0)
| ~ iLess0(VAR_0,sK1)
| VAR_0 = sz10
| VAR_0 = sz00
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( aNaturalNumber0(sK2(VAR_0))
| ~ iLess0(VAR_0,sK1)
| VAR_0 = sz10
| VAR_0 = sz00
| ~ aNaturalNumber0(VAR_0) )
& sz10 != sK1
& sz00 != sK1
& aNaturalNumber0(sK1) ),
inference(cnf_transformation,[status(thm)],[sk_m___neg_sk]) ).
cnf(c_45,negated_conjecture,
( isPrime0(sK2(A))
| ~ iLess0(A,sK1)
| A = sz10
| A = sz00
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_46,negated_conjecture,
( ~ isPrime0(A)
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_47,negated_conjecture,
( aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A)
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_46,c_38]) ).
cnf(c_48,negated_conjecture,
( aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_47]) ).
cnf(c_49,negated_conjecture,
( doDivides0(sK0(A),A)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A)
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_46,c_42]) ).
cnf(c_50,negated_conjecture,
( doDivides0(sK0(A),A)
| sz10 = A
| sz00 = A
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_49]) ).
cnf(c_51,negated_conjecture,
( sK0(A) != sz10
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A)
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_46,c_43]) ).
cnf(c_52,negated_conjecture,
( sK0(A) != sz10
| sz10 = A
| sz00 = A
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_51]) ).
cnf(c_53,negated_conjecture,
( sK0(A) != A
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A)
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_46,c_44]) ).
cnf(c_54,negated_conjecture,
( sK0(A) != A
| sz10 = A
| sz00 = A
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_53]) ).
cnf(c_55,negated_conjecture,
( ~ iLess0(A,sK1)
| A = sz10
| A = sz00
| ~ aNaturalNumber0(A)
| ~ doDivides0(sK2(A),sK1)
| ~ aNaturalNumber0(sK2(A)) ),
inference(resolve,[status(thm)],[c_46,c_45]) ).
cnf(c_14656,negated_conjecture,
( ~ iLess0(A,sK1)
| A = sz10
| sz00 = A
| ~ aNaturalNumber0(A)
| ~ doDivides0(sK2(A),sK1)
| ~ aNaturalNumber0(sK2(A)) ),
inference(copy,[status(thm)],[c_55]) ).
cnf(c_56,negated_conjecture,
( ~ iLess0(A,sK1)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A)
| ~ doDivides0(sK2(A),sK1)
| ~ aNaturalNumber0(sK2(A)) ),
inference(copy,[status(thm)],[c_14656]) ).
cnf(c_71,negated_conjecture,
( doDivides0(sK2(A),A)
| ~ iLess0(A,sK1)
| A = sz10
| A = sz00
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_14657,negated_conjecture,
( doDivides0(sK2(A),A)
| ~ iLess0(A,sK1)
| A = sz10
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_71]) ).
cnf(c_72,negated_conjecture,
( doDivides0(sK2(A),A)
| ~ iLess0(A,sK1)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_14657]) ).
cnf(c_73,negated_conjecture,
( aNaturalNumber0(sK2(A))
| ~ iLess0(A,sK1)
| A = sz10
| A = sz00
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_14658,negated_conjecture,
( aNaturalNumber0(sK2(A))
| ~ iLess0(A,sK1)
| A = sz10
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_73]) ).
cnf(c_74,negated_conjecture,
( aNaturalNumber0(sK2(A))
| ~ iLess0(A,sK1)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_14658]) ).
cnf(c_75,negated_conjecture,
sz10 != sK1,
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_76,negated_conjecture,
sK1 != sz10,
inference(copy,[status(thm)],[c_75]) ).
cnf(c_77,negated_conjecture,
sz00 != sK1,
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_78,negated_conjecture,
sK1 != sz00,
inference(copy,[status(thm)],[c_77]) ).
cnf(c_79,negated_conjecture,
aNaturalNumber0(sK1),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_81,plain,
( sdtlseqdt0(A,B)
| B = sz00
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDivLE]) ).
cnf(c_82,plain,
( sdtlseqdt0(A,B)
| sz00 = B
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_81]) ).
cnf(c_85,plain,
( doDivides0(A,C)
| ~ doDivides0(B,C)
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDivTrans]) ).
cnf(c_89,plain,
( sdtasdt0(A,C) != B
| ~ aNaturalNumber0(C)
| doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefDiv]) ).
cnf(c_92,plain,
( iLess0(A,B)
| ~ sdtlseqdt0(A,B)
| B = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mIH_03]) ).
cnf(c_93,plain,
( sdtlseqdt0(B,sdtasdt0(B,A))
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mMonMul2]) ).
cnf(c_106,plain,
( B = A
| ~ sdtlseqdt0(B,A)
| ~ sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLEAsym]) ).
cnf(c_120,plain,
( C = B
| sdtasdt0(A,C) != sdtasdt0(A,B)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mMulCanc]) ).
cnf(c_128,plain,
( sdtasdt0(A,sz00) = sz00
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_MulZero]) ).
cnf(c_130,plain,
( sdtasdt0(A,sz10) = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_MulUnit]) ).
cnf(c_137,plain,
( aNaturalNumber0(sdtasdt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mSortsB_02]) ).
cnf(c_140,plain,
aNaturalNumber0(sz10),
inference(clausify,[status(thm)],[mSortsC_01]) ).
fof(mSortsC,axiom,
aNaturalNumber0(sz00),
file('theBenchmark.p',mSortsC) ).
cnf(c_141,plain,
aNaturalNumber0(sz00),
inference(clausify,[status(thm)],[mSortsC]) ).
cnf(c_161,plain,
( sdtasdt0(A,B) != A
| ~ aNaturalNumber0(B)
| doDivides0(A,A)
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_89]) ).
cnf(c_166,plain,
( sdtlseqdt0(A,sdtasdt0(A,A))
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_93]) ).
cnf(c_220,plain,
( aNaturalNumber0(sdtasdt0(A,A))
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_137]) ).
cnf(c_14659,negated_conjecture,
( sK0(sK1) != sK1
| sz10 = sK1
| sz00 = sK1
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_79,c_54]) ).
cnf(c_14660,negated_conjecture,
( sK0(sK1) != sK1
| sz10 = sK1
| sK1 = sz00
| ~ doDivides0(sK1,sK1) ),
inference(copy,[status(thm)],[c_14659]) ).
cnf(c_14661,negated_conjecture,
( sK0(sK1) != sK1
| sK1 = sz10
| sK1 = sz00
| ~ doDivides0(sK1,sK1) ),
inference(copy,[status(thm)],[c_14660]) ).
cnf(c_14662,negated_conjecture,
( sK0(sK1) != sK1
| sK1 = sz10
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_78,c_14661]) ).
cnf(c_246,negated_conjecture,
( sK0(sK1) != sK1
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_76,c_14662]) ).
cnf(c_14663,negated_conjecture,
( sK0(sK1) != sz10
| sz10 = sK1
| sz00 = sK1
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_79,c_52]) ).
cnf(c_14664,negated_conjecture,
( sK0(sK1) != sz10
| sz10 = sK1
| sK1 = sz00
| ~ doDivides0(sK1,sK1) ),
inference(copy,[status(thm)],[c_14663]) ).
cnf(c_14665,negated_conjecture,
( sK0(sK1) != sz10
| sK1 = sz10
| sK1 = sz00
| ~ doDivides0(sK1,sK1) ),
inference(copy,[status(thm)],[c_14664]) ).
cnf(c_14666,negated_conjecture,
( sK0(sK1) != sz10
| sK1 = sz10
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_78,c_14665]) ).
cnf(c_247,negated_conjecture,
( sK0(sK1) != sz10
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_76,c_14666]) ).
cnf(c_14667,negated_conjecture,
( doDivides0(sK0(sK1),sK1)
| sz10 = sK1
| sz00 = sK1
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_79,c_50]) ).
cnf(c_14668,negated_conjecture,
( doDivides0(sK0(sK1),sK1)
| sz10 = sK1
| sK1 = sz00
| ~ doDivides0(sK1,sK1) ),
inference(copy,[status(thm)],[c_14667]) ).
cnf(c_14669,negated_conjecture,
( doDivides0(sK0(sK1),sK1)
| sK1 = sz10
| sK1 = sz00
| ~ doDivides0(sK1,sK1) ),
inference(copy,[status(thm)],[c_14668]) ).
cnf(c_14670,negated_conjecture,
( doDivides0(sK0(sK1),sK1)
| sK1 = sz10
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_78,c_14669]) ).
cnf(c_248,negated_conjecture,
( doDivides0(sK0(sK1),sK1)
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_76,c_14670]) ).
cnf(c_14671,negated_conjecture,
( aNaturalNumber0(sK0(sK1))
| sz10 = sK1
| sz00 = sK1
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_79,c_48]) ).
cnf(c_14672,negated_conjecture,
( aNaturalNumber0(sK0(sK1))
| sz10 = sK1
| sK1 = sz00
| ~ doDivides0(sK1,sK1) ),
inference(copy,[status(thm)],[c_14671]) ).
cnf(c_14673,negated_conjecture,
( aNaturalNumber0(sK0(sK1))
| sK1 = sz10
| sK1 = sz00
| ~ doDivides0(sK1,sK1) ),
inference(copy,[status(thm)],[c_14672]) ).
cnf(c_14674,negated_conjecture,
( aNaturalNumber0(sK0(sK1))
| sK1 = sz10
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_78,c_14673]) ).
cnf(c_249,negated_conjecture,
( aNaturalNumber0(sK0(sK1))
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_76,c_14674]) ).
cnf(c_14675,negated_conjecture,
( sdtlseqdt0(A,sK1)
| sz00 = sK1
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_82,c_79]) ).
cnf(c_14676,negated_conjecture,
( sdtlseqdt0(A,sK1)
| sK1 = sz00
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_14675]) ).
cnf(c_257,negated_conjecture,
( sdtlseqdt0(A,sK1)
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_78,c_14676]) ).
cnf(c_273,plain,
( doDivides0(A,sK1)
| ~ doDivides0(B,sK1)
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_85,c_79]) ).
cnf(c_397,plain,
sdtasdt0(sK1,sz10) = sK1,
inference(resolve,[status(thm)],[c_130,c_79]) ).
cnf(c_14677,negated_conjecture,
( B = A
| sdtasdt0(sK1,B) != sdtasdt0(sK1,A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A)
| sz00 = sK1 ),
inference(resolve,[status(thm)],[c_120,c_79]) ).
cnf(c_14678,negated_conjecture,
sz00 != sK1,
inference(copy,[status(thm)],[c_78]) ).
cnf(c_14679,negated_conjecture,
( B = A
| sdtasdt0(sK1,B) != sdtasdt0(sK1,A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_14677,c_14678]) ).
cnf(c_14680,negated_conjecture,
( A = sK1
| sdtasdt0(sK1,A) != sdtasdt0(sK1,sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_14679,c_79]) ).
cnf(c_14681,negated_conjecture,
( sz10 = sK1
| sdtasdt0(sK1,sz10) != sdtasdt0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_14680,c_140]) ).
cnf(c_14682,negated_conjecture,
sz10 != sK1,
inference(copy,[status(thm)],[c_76]) ).
cnf(c_14683,negated_conjecture,
sdtasdt0(sK1,sz10) != sdtasdt0(sK1,sK1),
inference(resolve,[status(thm)],[c_14681,c_14682]) ).
cnf(c_14684,negated_conjecture,
sK1 != sdtasdt0(sK1,sK1),
inference(paramod,[status(thm)],[c_397,c_14683]) ).
cnf(c_524,negated_conjecture,
sdtasdt0(sK1,sK1) != sK1,
inference(copy,[status(thm)],[c_14684]) ).
cnf(c_14685,negated_conjecture,
( sdtlseqdt0(sK1,sdtasdt0(sK1,sK1))
| sz00 = sK1 ),
inference(resolve,[status(thm)],[c_166,c_79]) ).
cnf(c_14686,negated_conjecture,
( sdtlseqdt0(sK1,sdtasdt0(sK1,sK1))
| sK1 = sz00 ),
inference(copy,[status(thm)],[c_14685]) ).
cnf(c_757,negated_conjecture,
sdtlseqdt0(sK1,sdtasdt0(sK1,sK1)),
inference(resolve,[status(thm)],[c_78,c_14686]) ).
cnf(c_849,plain,
aNaturalNumber0(sdtasdt0(sK1,sK1)),
inference(resolve,[status(thm)],[c_220,c_79]) ).
cnf(c_1757,plain,
( sdtlseqdt0(sdtasdt0(sK1,sK1),sK1)
| ~ doDivides0(sdtasdt0(sK1,sK1),sK1) ),
inference(resolve,[status(thm)],[c_849,c_257]) ).
cnf(c_1907,plain,
sdtasdt0(sdtasdt0(sK1,sK1),sz00) = sz00,
inference(resolve,[status(thm)],[c_849,c_128]) ).
cnf(c_14687,plain,
( ~ aNaturalNumber0(sz10)
| doDivides0(sK1,sK1)
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_397,c_161]) ).
cnf(c_14688,negated_conjecture,
( ~ aNaturalNumber0(sz10)
| doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_79,c_14687]) ).
cnf(c_4601,negated_conjecture,
doDivides0(sK1,sK1),
inference(resolve,[status(thm)],[c_140,c_14688]) ).
cnf(c_4617,negated_conjecture,
aNaturalNumber0(sK0(sK1)),
inference(resolve,[status(thm)],[c_4601,c_249]) ).
cnf(c_4618,negated_conjecture,
doDivides0(sK0(sK1),sK1),
inference(resolve,[status(thm)],[c_4601,c_248]) ).
cnf(c_4619,negated_conjecture,
sK0(sK1) != sz10,
inference(resolve,[status(thm)],[c_4601,c_247]) ).
cnf(c_4620,negated_conjecture,
sK0(sK1) != sK1,
inference(resolve,[status(thm)],[c_4601,c_246]) ).
cnf(c_14689,plain,
( sdtlseqdt0(sK0(sK1),sK1)
| ~ doDivides0(sK0(sK1),sK1) ),
inference(resolve,[status(thm)],[c_4617,c_257]) ).
cnf(c_4697,plain,
sdtlseqdt0(sK0(sK1),sK1),
inference(resolve,[status(thm)],[c_4618,c_14689]) ).
cnf(c_14690,negated_conjecture,
( aNaturalNumber0(sK2(sK0(sK1)))
| ~ iLess0(sK0(sK1),sK1)
| sz10 = sK0(sK1)
| sz00 = sK0(sK1) ),
inference(resolve,[status(thm)],[c_4617,c_74]) ).
cnf(c_14691,negated_conjecture,
( aNaturalNumber0(sK2(sK0(sK1)))
| ~ iLess0(sK0(sK1),sK1)
| sz10 = sK0(sK1)
| sK0(sK1) = sz00 ),
inference(copy,[status(thm)],[c_14690]) ).
cnf(c_14692,negated_conjecture,
( aNaturalNumber0(sK2(sK0(sK1)))
| ~ iLess0(sK0(sK1),sK1)
| sK0(sK1) = sz10
| sK0(sK1) = sz00 ),
inference(copy,[status(thm)],[c_14691]) ).
cnf(c_4938,negated_conjecture,
( aNaturalNumber0(sK2(sK0(sK1)))
| ~ iLess0(sK0(sK1),sK1)
| sK0(sK1) = sz00 ),
inference(resolve,[status(thm)],[c_4619,c_14692]) ).
cnf(c_14693,negated_conjecture,
( doDivides0(sK2(sK0(sK1)),sK0(sK1))
| ~ iLess0(sK0(sK1),sK1)
| sz10 = sK0(sK1)
| sz00 = sK0(sK1) ),
inference(resolve,[status(thm)],[c_4617,c_72]) ).
cnf(c_14694,negated_conjecture,
( doDivides0(sK2(sK0(sK1)),sK0(sK1))
| ~ iLess0(sK0(sK1),sK1)
| sz10 = sK0(sK1)
| sK0(sK1) = sz00 ),
inference(copy,[status(thm)],[c_14693]) ).
cnf(c_14695,negated_conjecture,
( doDivides0(sK2(sK0(sK1)),sK0(sK1))
| ~ iLess0(sK0(sK1),sK1)
| sK0(sK1) = sz10
| sK0(sK1) = sz00 ),
inference(copy,[status(thm)],[c_14694]) ).
cnf(c_4939,negated_conjecture,
( doDivides0(sK2(sK0(sK1)),sK0(sK1))
| ~ iLess0(sK0(sK1),sK1)
| sK0(sK1) = sz00 ),
inference(resolve,[status(thm)],[c_4619,c_14695]) ).
cnf(c_14696,negated_conjecture,
( ~ iLess0(sK0(sK1),sK1)
| sz10 = sK0(sK1)
| sz00 = sK0(sK1)
| ~ doDivides0(sK2(sK0(sK1)),sK1)
| ~ aNaturalNumber0(sK2(sK0(sK1))) ),
inference(resolve,[status(thm)],[c_4617,c_56]) ).
cnf(c_14697,negated_conjecture,
( ~ iLess0(sK0(sK1),sK1)
| sz10 = sK0(sK1)
| sK0(sK1) = sz00
| ~ doDivides0(sK2(sK0(sK1)),sK1)
| ~ aNaturalNumber0(sK2(sK0(sK1))) ),
inference(copy,[status(thm)],[c_14696]) ).
cnf(c_14698,negated_conjecture,
( ~ iLess0(sK0(sK1),sK1)
| sK0(sK1) = sz10
| sK0(sK1) = sz00
| ~ doDivides0(sK2(sK0(sK1)),sK1)
| ~ aNaturalNumber0(sK2(sK0(sK1))) ),
inference(copy,[status(thm)],[c_14697]) ).
cnf(c_4952,negated_conjecture,
( ~ iLess0(sK0(sK1),sK1)
| sK0(sK1) = sz00
| ~ doDivides0(sK2(sK0(sK1)),sK1)
| ~ aNaturalNumber0(sK2(sK0(sK1))) ),
inference(resolve,[status(thm)],[c_4619,c_14698]) ).
cnf(c_14699,plain,
( doDivides0(A,sK1)
| ~ doDivides0(A,sK0(sK1))
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sK0(sK1))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4618,c_85]) ).
cnf(c_14700,plain,
( doDivides0(A,sK1)
| ~ doDivides0(A,sK0(sK1))
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4617,c_14699]) ).
cnf(c_5423,negated_conjecture,
( doDivides0(A,sK1)
| ~ doDivides0(A,sK0(sK1))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_79,c_14700]) ).
cnf(c_14701,plain,
( iLess0(sK0(sK1),sK1)
| sK1 = sK0(sK1)
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sK0(sK1)) ),
inference(resolve,[status(thm)],[c_4697,c_92]) ).
cnf(c_14702,plain,
( iLess0(sK0(sK1),sK1)
| sK0(sK1) = sK1
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sK0(sK1)) ),
inference(copy,[status(thm)],[c_14701]) ).
cnf(c_14703,plain,
( iLess0(sK0(sK1),sK1)
| sK0(sK1) = sK1
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_4617,c_14702]) ).
cnf(c_14704,negated_conjecture,
( iLess0(sK0(sK1),sK1)
| sK0(sK1) = sK1 ),
inference(resolve,[status(thm)],[c_79,c_14703]) ).
cnf(c_5463,negated_conjecture,
iLess0(sK0(sK1),sK1),
inference(resolve,[status(thm)],[c_4620,c_14704]) ).
cnf(c_5465,negated_conjecture,
( sK0(sK1) = sz00
| ~ doDivides0(sK2(sK0(sK1)),sK1)
| ~ aNaturalNumber0(sK2(sK0(sK1))) ),
inference(resolve,[status(thm)],[c_5463,c_4952]) ).
cnf(c_5469,negated_conjecture,
( doDivides0(sK2(sK0(sK1)),sK0(sK1))
| sK0(sK1) = sz00 ),
inference(resolve,[status(thm)],[c_5463,c_4939]) ).
cnf(c_5470,negated_conjecture,
( aNaturalNumber0(sK2(sK0(sK1)))
| sK0(sK1) = sz00 ),
inference(resolve,[status(thm)],[c_5463,c_4938]) ).
cnf(c_14705,plain,
( sK1 = sdtasdt0(sK1,sK1)
| ~ sdtlseqdt0(sdtasdt0(sK1,sK1),sK1)
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sdtasdt0(sK1,sK1)) ),
inference(resolve,[status(thm)],[c_757,c_106]) ).
cnf(c_14706,plain,
( sdtasdt0(sK1,sK1) = sK1
| ~ sdtlseqdt0(sdtasdt0(sK1,sK1),sK1)
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sdtasdt0(sK1,sK1)) ),
inference(copy,[status(thm)],[c_14705]) ).
cnf(c_14707,plain,
( sdtasdt0(sK1,sK1) = sK1
| ~ sdtlseqdt0(sdtasdt0(sK1,sK1),sK1)
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_849,c_14706]) ).
cnf(c_14708,negated_conjecture,
( sdtasdt0(sK1,sK1) = sK1
| ~ sdtlseqdt0(sdtasdt0(sK1,sK1),sK1) ),
inference(resolve,[status(thm)],[c_79,c_14707]) ).
cnf(c_6269,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(sK1,sK1),sK1),
inference(resolve,[status(thm)],[c_524,c_14708]) ).
cnf(c_6280,plain,
~ doDivides0(sdtasdt0(sK1,sK1),sK1),
inference(resolve,[status(thm)],[c_6269,c_1757]) ).
cnf(c_14709,plain,
( doDivides0(sdtasdt0(sK1,sK1),sK1)
| ~ doDivides0(A,sK1)
| ~ doDivides0(sdtasdt0(sK1,sK1),A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_273,c_849]) ).
cnf(c_14710,plain,
( doDivides0(sdtasdt0(sK1,sK1),sK1)
| ~ doDivides0(sK0(sK1),sK1)
| ~ doDivides0(sdtasdt0(sK1,sK1),sK0(sK1)) ),
inference(resolve,[status(thm)],[c_14709,c_4617]) ).
cnf(c_14711,plain,
( doDivides0(sdtasdt0(sK1,sK1),sK1)
| ~ doDivides0(sdtasdt0(sK1,sK1),sK0(sK1)) ),
inference(resolve,[status(thm)],[c_14710,c_4618]) ).
cnf(c_6366,plain,
~ doDivides0(sdtasdt0(sK1,sK1),sK0(sK1)),
inference(resolve,[status(thm)],[c_14711,c_6280]) ).
cnf(c_14712,plain,
( sdtasdt0(sdtasdt0(sK1,sK1),B) != A
| ~ aNaturalNumber0(B)
| doDivides0(sdtasdt0(sK1,sK1),A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_89,c_849]) ).
cnf(c_14713,plain,
( sdtasdt0(sdtasdt0(sK1,sK1),A) != sK0(sK1)
| ~ aNaturalNumber0(A)
| doDivides0(sdtasdt0(sK1,sK1),sK0(sK1)) ),
inference(resolve,[status(thm)],[c_14712,c_4617]) ).
cnf(c_14714,plain,
( sdtasdt0(sdtasdt0(sK1,sK1),A) != sK0(sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_14713,c_6366]) ).
cnf(c_14715,plain,
sdtasdt0(sdtasdt0(sK1,sK1),sz00) != sK0(sK1),
inference(resolve,[status(thm)],[c_14714,c_141]) ).
cnf(c_14716,plain,
sz00 != sK0(sK1),
inference(paramod,[status(thm)],[c_1907,c_14715]) ).
cnf(c_6656,plain,
sK0(sK1) != sz00,
inference(copy,[status(thm)],[c_14716]) ).
cnf(c_6673,negated_conjecture,
aNaturalNumber0(sK2(sK0(sK1))),
inference(resolve,[status(thm)],[c_6656,c_5470]) ).
cnf(c_6674,negated_conjecture,
doDivides0(sK2(sK0(sK1)),sK0(sK1)),
inference(resolve,[status(thm)],[c_6656,c_5469]) ).
cnf(c_14717,negated_conjecture,
( sK0(sK1) = sz00
| ~ doDivides0(sK2(sK0(sK1)),sK1) ),
inference(resolve,[status(thm)],[c_6673,c_5465]) ).
cnf(c_6678,negated_conjecture,
~ doDivides0(sK2(sK0(sK1)),sK1),
inference(resolve,[status(thm)],[c_6656,c_14717]) ).
cnf(c_14718,plain,
( doDivides0(sK2(sK0(sK1)),sK1)
| ~ doDivides0(sK2(sK0(sK1)),sK0(sK1)) ),
inference(resolve,[status(thm)],[c_6673,c_5423]) ).
cnf(c_14719,plain,
doDivides0(sK2(sK0(sK1)),sK1),
inference(resolve,[status(thm)],[c_6674,c_14718]) ).
cnf(c_14655,plain,
$false,
inference(resolve,[status(thm)],[c_6678,c_14719]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM481+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/5.58 % Computer : n014.cluster.edu
% 0.08/5.58 % Model : x86_64 x86_64
% 0.08/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.58 % Memory : 8046.5625MB
% 0.08/5.58 % OS : Linux 6.8.0-71-generic
% 0.08/5.58 % CPULimit : 300
% 0.08/5.58 % WCLimit : 300
% 0.08/5.58 % DateTime : Sat Sep 26 02:55:23 UTC 2026
% 0.08/5.58 % CPUTime :
% 0.08/5.58 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/5.58 % Process 1979028 was started by sandbox2 on n014,
% 0.08/5.58 % Sat Sep 26 02:55:23 2026
% 0.08/5.58 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/5.60
% 0.08/5.60 % From the command line: assign(max_seconds, 300).
% 39.55/10.69
% 39.55/10.69 % given #500 (W,wt=16): 420 -aNaturalNumber0(A) | aNaturalNumber0(sdtasdt0(A,sz10)). [resolve(140,a,137,b)].
% 39.55/10.69
% 39.55/10.69 % SZS status Theorem for theBenchmark
% 39.55/10.69
% 39.55/10.69 % Proof 1 at 4.75 (+ 0.32) seconds.
% 39.55/10.69 % Length of proof is 88.
% 39.55/10.69 % Level of proof is 11.
% 39.55/10.69 % Maximum clause weight is 32.000.
% 39.55/10.69 % Given clauses 796.
% 39.55/10.69
% 39.55/10.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------