%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM481+3 : 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:08 AM UTC 2026
% Result : Theorem 48.29s 11.77s
% Output : CNFRefutation 48.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 14
% Syntax : Number of formulae : 162 ( 34 unt; 0 def)
% Number of atoms : 849 ( 373 equ)
% Maximal formula atoms : 128 ( 5 avg)
% Number of connectives : 1095 ( 408 ~; 510 |; 143 &)
% ( 2 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 32 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 185 ( 0 sgn 85 !; 19 ?)
% 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)
& ! [W3] :
( ( ( doDivides0(W3,W2)
| ? [W4] :
( W2 = sdtasdt0(W3,W4)
& aNaturalNumber0(W4) ) )
& aNaturalNumber0(W3) )
=> ( W3 = W2
| W3 = sz10 ) )
& W2 != sz10
& W2 != sz00
& doDivides0(W2,W1)
& ? [W3] :
( W1 = sdtasdt0(W2,W3)
& aNaturalNumber0(W3) )
& aNaturalNumber0(W2) ) ) )
=> ? [W1] :
( ( isPrime0(W1)
| ( ! [W2] :
( ( doDivides0(W2,W1)
& ? [W3] :
( W1 = sdtasdt0(W2,W3)
& aNaturalNumber0(W3) )
& aNaturalNumber0(W2) )
=> ( W2 = W1
| W2 = sz10 ) )
& W1 != sz10
& W1 != sz00 ) )
& ( doDivides0(W1,W0)
| ? [W2] :
( W0 = sdtasdt0(W1,W2)
& aNaturalNumber0(W2) ) )
& 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)
& ! [W3] :
( ( ( doDivides0(W3,W2)
| ? [W4] :
( W2 = sdtasdt0(W3,W4)
& aNaturalNumber0(W4) ) )
& aNaturalNumber0(W3) )
=> ( W3 = W2
| W3 = sz10 ) )
& W2 != sz10
& W2 != sz00
& doDivides0(W2,W1)
& ? [W3] :
( W1 = sdtasdt0(W2,W3)
& aNaturalNumber0(W3) )
& aNaturalNumber0(W2) ) ) )
=> ? [W1] :
( ( isPrime0(W1)
| ( ! [W2] :
( ( doDivides0(W2,W1)
& ? [W3] :
( W1 = sdtasdt0(W2,W3)
& aNaturalNumber0(W3) )
& aNaturalNumber0(W2) )
=> ( W2 = W1
| W2 = sz10 ) )
& W1 != sz10
& W1 != sz00 ) )
& ( doDivides0(W1,W0)
| ? [W2] :
( W0 = sdtasdt0(W1,W2)
& aNaturalNumber0(W2) ) )
& 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)
& ( ? [W2] :
( W2 != W1
& W2 != sz10
& doDivides0(W2,W1)
& ? [W3] :
( sdtasdt0(W2,W3) = W1
& aNaturalNumber0(W3) )
& aNaturalNumber0(W2) )
| W1 = sz10
| W1 = sz00 ) )
| ( ~ doDivides0(W1,W0)
& ! [X0] :
( sdtasdt0(W1,X0) != W0
| ~ aNaturalNumber0(X0) ) )
| ~ aNaturalNumber0(W1) )
& ! [X1] :
( ? [X2] :
( isPrime0(X2)
& ! [X4] :
( X4 = X2
| X4 = sz10
| ( ~ doDivides0(X4,X2)
& ! [W4] :
( sdtasdt0(X4,W4) != X2
| ~ aNaturalNumber0(W4) ) )
| ~ aNaturalNumber0(X4) )
& X2 != sz10
& X2 != sz00
& doDivides0(X2,X1)
& ? [X3] :
( sdtasdt0(X2,X3) = X1
& aNaturalNumber0(X3) )
& aNaturalNumber0(X2) )
| ~ iLess0(X1,W0)
| X1 = sz10
| X1 = sz00
| ~ aNaturalNumber0(X1) )
& sz10 != W0
& sz00 != W0
& aNaturalNumber0(W0) ),
inference(fof_nnf,[status(thm)],[m___neg]) ).
fof(sk_m___neg_sk,plain,
( ! [W1] :
( ( ~ isPrime0(W1)
& ( ( sK4(W1) != W1
& sK4(W1) != sz10
& doDivides0(sK4(W1),W1)
& sdtasdt0(sK4(W1),sK5(W1)) = W1
& aNaturalNumber0(sK5(W1))
& aNaturalNumber0(sK4(W1)) )
| W1 = sz10
| W1 = sz00 ) )
| ( ~ doDivides0(W1,sK1)
& ! [X0] :
( sdtasdt0(W1,X0) != sK1
| ~ aNaturalNumber0(X0) ) )
| ~ aNaturalNumber0(W1) )
& ! [X1] :
( ( isPrime0(sK2(X1))
& ! [X4] :
( X4 = sK2(X1)
| X4 = sz10
| ( ~ doDivides0(X4,sK2(X1))
& ! [W4] :
( sdtasdt0(X4,W4) != sK2(X1)
| ~ aNaturalNumber0(W4) ) )
| ~ aNaturalNumber0(X4) )
& sK2(X1) != sz10
& sK2(X1) != sz00
& doDivides0(sK2(X1),X1)
& sdtasdt0(sK2(X1),sK3(X1)) = X1
& aNaturalNumber0(sK3(X1))
& aNaturalNumber0(sK2(X1)) )
| ~ iLess0(X1,sK1)
| X1 = sz10
| X1 = sz00
| ~ aNaturalNumber0(X1) )
& sz10 != sK1
& sz00 != sK1
& aNaturalNumber0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3,sK4,sK5]),skolemize(W0,sK1),skolemize(X2,sK2(X1)),skolemize(X3,sK3(X1)),skolemize(W2,sK4(W1)),skolemize(W3,sK5(W1))],[nnf_37]) ).
fof(sk_m___neg,plain,
( ! [VAR_0] :
( ~ isPrime0(VAR_0)
| ~ doDivides0(VAR_0,sK1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( sK4(VAR_0) != VAR_0
| VAR_0 = sz10
| VAR_0 = sz00
| ~ doDivides0(VAR_0,sK1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( sK4(VAR_0) != sz10
| VAR_0 = sz10
| VAR_0 = sz00
| ~ doDivides0(VAR_0,sK1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( doDivides0(sK4(VAR_0),VAR_0)
| VAR_0 = sz10
| VAR_0 = sz00
| ~ doDivides0(VAR_0,sK1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( sdtasdt0(sK4(VAR_0),sK5(VAR_0)) = VAR_0
| VAR_0 = sz10
| VAR_0 = sz00
| ~ doDivides0(VAR_0,sK1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( aNaturalNumber0(sK5(VAR_0))
| VAR_0 = sz10
| VAR_0 = sz00
| ~ doDivides0(VAR_0,sK1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( aNaturalNumber0(sK4(VAR_0))
| VAR_0 = sz10
| VAR_0 = sz00
| ~ doDivides0(VAR_0,sK1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ isPrime0(VAR_0)
| sdtasdt0(VAR_0,VAR_1) != sK1
| ~ aNaturalNumber0(VAR_1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sK4(VAR_0) != VAR_0
| VAR_0 = sz10
| VAR_0 = sz00
| sdtasdt0(VAR_0,VAR_1) != sK1
| ~ aNaturalNumber0(VAR_1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sK4(VAR_0) != sz10
| VAR_0 = sz10
| VAR_0 = sz00
| sdtasdt0(VAR_0,VAR_1) != sK1
| ~ aNaturalNumber0(VAR_1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1] :
( doDivides0(sK4(VAR_0),VAR_0)
| VAR_0 = sz10
| VAR_0 = sz00
| sdtasdt0(VAR_0,VAR_1) != sK1
| ~ aNaturalNumber0(VAR_1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1] :
( sdtasdt0(sK4(VAR_0),sK5(VAR_0)) = VAR_0
| VAR_0 = sz10
| VAR_0 = sz00
| sdtasdt0(VAR_0,VAR_1) != sK1
| ~ aNaturalNumber0(VAR_1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aNaturalNumber0(sK5(VAR_0))
| VAR_0 = sz10
| VAR_0 = sz00
| sdtasdt0(VAR_0,VAR_1) != sK1
| ~ aNaturalNumber0(VAR_1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1] :
( aNaturalNumber0(sK4(VAR_0))
| VAR_0 = sz10
| VAR_0 = sz00
| sdtasdt0(VAR_0,VAR_1) != sK1
| ~ aNaturalNumber0(VAR_1)
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( isPrime0(sK2(VAR_0))
| ~ iLess0(VAR_0,sK1)
| VAR_0 = sz10
| VAR_0 = sz00
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1] :
( VAR_1 = sK2(VAR_0)
| VAR_1 = sz10
| ~ doDivides0(VAR_1,sK2(VAR_0))
| ~ aNaturalNumber0(VAR_1)
| ~ iLess0(VAR_0,sK1)
| VAR_0 = sz10
| VAR_0 = sz00
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( VAR_1 = sK2(VAR_0)
| VAR_1 = sz10
| sdtasdt0(VAR_1,VAR_2) != sK2(VAR_0)
| ~ aNaturalNumber0(VAR_2)
| ~ aNaturalNumber0(VAR_1)
| ~ iLess0(VAR_0,sK1)
| VAR_0 = sz10
| VAR_0 = sz00
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( sK2(VAR_0) != sz10
| ~ iLess0(VAR_0,sK1)
| VAR_0 = sz10
| VAR_0 = sz00
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( sK2(VAR_0) != sz00
| ~ 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] :
( sdtasdt0(sK2(VAR_0),sK3(VAR_0)) = VAR_0
| ~ iLess0(VAR_0,sK1)
| VAR_0 = sz10
| VAR_0 = sz00
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( aNaturalNumber0(sK3(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)
| sdtasdt0(A,B) != sK1
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_47,negated_conjecture,
( ~ isPrime0(A)
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_56,negated_conjecture,
( ~ iLess0(A,sK1)
| A = sz10
| A = sz00
| ~ aNaturalNumber0(A)
| ~ doDivides0(sK2(A),sK1)
| ~ aNaturalNumber0(sK2(A)) ),
inference(resolve,[status(thm)],[c_47,c_45]) ).
cnf(c_14713,negated_conjecture,
( ~ iLess0(A,sK1)
| A = sz10
| sz00 = A
| ~ aNaturalNumber0(A)
| ~ doDivides0(sK2(A),sK1)
| ~ aNaturalNumber0(sK2(A)) ),
inference(copy,[status(thm)],[c_56]) ).
cnf(c_57,negated_conjecture,
( ~ iLess0(A,sK1)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A)
| ~ doDivides0(sK2(A),sK1)
| ~ aNaturalNumber0(sK2(A)) ),
inference(copy,[status(thm)],[c_14713]) ).
cnf(c_58,negated_conjecture,
( aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A)
| sdtasdt0(A,B) != sK1
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_46,c_38]) ).
cnf(c_59,negated_conjecture,
( aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| sdtasdt0(A,B) != sK1
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_58]) ).
cnf(c_60,negated_conjecture,
( doDivides0(sK0(A),A)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A)
| sdtasdt0(A,B) != sK1
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_46,c_42]) ).
cnf(c_61,negated_conjecture,
( doDivides0(sK0(A),A)
| sz10 = A
| sz00 = A
| sdtasdt0(A,B) != sK1
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_60]) ).
cnf(c_62,negated_conjecture,
( sK0(A) != sz10
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A)
| sdtasdt0(A,B) != sK1
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_46,c_43]) ).
cnf(c_63,negated_conjecture,
( sK0(A) != sz10
| sz10 = A
| sz00 = A
| sdtasdt0(A,B) != sK1
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_62]) ).
cnf(c_64,negated_conjecture,
( sK0(A) != A
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A)
| sdtasdt0(A,B) != sK1
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_46,c_44]) ).
cnf(c_65,negated_conjecture,
( sK0(A) != A
| sz10 = A
| sz00 = A
| sdtasdt0(A,B) != sK1
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_64]) ).
cnf(c_114,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_14714,negated_conjecture,
( doDivides0(sK2(A),A)
| ~ iLess0(A,sK1)
| A = sz10
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_114]) ).
cnf(c_115,negated_conjecture,
( doDivides0(sK2(A),A)
| ~ iLess0(A,sK1)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_14714]) ).
cnf(c_120,negated_conjecture,
( aNaturalNumber0(sK2(A))
| ~ iLess0(A,sK1)
| A = sz10
| A = sz00
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_14715,negated_conjecture,
( aNaturalNumber0(sK2(A))
| ~ iLess0(A,sK1)
| A = sz10
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_120]) ).
cnf(c_121,negated_conjecture,
( aNaturalNumber0(sK2(A))
| ~ iLess0(A,sK1)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_14715]) ).
cnf(c_122,negated_conjecture,
sz10 != sK1,
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_123,negated_conjecture,
sK1 != sz10,
inference(copy,[status(thm)],[c_122]) ).
cnf(c_124,negated_conjecture,
sz00 != sK1,
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_125,negated_conjecture,
sK1 != sz00,
inference(copy,[status(thm)],[c_124]) ).
cnf(c_126,negated_conjecture,
aNaturalNumber0(sK1),
inference(split_conjunct,[status(thm)],[sk_m___neg]) ).
cnf(c_128,plain,
( sdtlseqdt0(A,B)
| B = sz00
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDivLE]) ).
cnf(c_129,plain,
( sdtlseqdt0(A,B)
| sz00 = B
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_128]) ).
cnf(c_132,plain,
( doDivides0(A,C)
| ~ doDivides0(B,C)
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDivTrans]) ).
cnf(c_136,plain,
( sdtasdt0(A,C) != B
| ~ aNaturalNumber0(C)
| doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefDiv]) ).
cnf(c_139,plain,
( iLess0(A,B)
| ~ sdtlseqdt0(A,B)
| B = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mIH_03]) ).
cnf(c_140,plain,
( sdtlseqdt0(B,sdtasdt0(B,A))
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mMonMul2]) ).
cnf(c_153,plain,
( B = A
| ~ sdtlseqdt0(B,A)
| ~ sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLEAsym]) ).
cnf(c_167,plain,
( C = B
| sdtasdt0(A,C) != sdtasdt0(A,B)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mMulCanc]) ).
cnf(c_175,plain,
( sdtasdt0(A,sz00) = sz00
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_MulZero]) ).
cnf(c_177,plain,
( sdtasdt0(A,sz10) = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_MulUnit]) ).
cnf(c_184,plain,
( aNaturalNumber0(sdtasdt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mSortsB_02]) ).
cnf(c_187,plain,
aNaturalNumber0(sz10),
inference(clausify,[status(thm)],[mSortsC_01]) ).
fof(mSortsC,axiom,
aNaturalNumber0(sz00),
file('theBenchmark.p',mSortsC) ).
cnf(c_188,plain,
aNaturalNumber0(sz00),
inference(clausify,[status(thm)],[mSortsC]) ).
cnf(c_229,plain,
( sdtlseqdt0(A,sdtasdt0(A,A))
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_140]) ).
cnf(c_283,plain,
( aNaturalNumber0(sdtasdt0(A,A))
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_184]) ).
cnf(c_14716,negated_conjecture,
( sK0(sK1) != sK1
| sz10 = sK1
| sz00 = sK1
| sdtasdt0(sK1,A) != sK1
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_126,c_65]) ).
cnf(c_14717,negated_conjecture,
( sK0(sK1) != sK1
| sz10 = sK1
| sK1 = sz00
| sdtasdt0(sK1,A) != sK1
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_14716]) ).
cnf(c_14718,negated_conjecture,
( sK0(sK1) != sK1
| sK1 = sz10
| sK1 = sz00
| sdtasdt0(sK1,A) != sK1
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_14717]) ).
cnf(c_14719,negated_conjecture,
( sK0(sK1) != sK1
| sK1 = sz10
| sdtasdt0(sK1,A) != sK1
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_125,c_14718]) ).
cnf(c_335,negated_conjecture,
( sK0(sK1) != sK1
| sdtasdt0(sK1,A) != sK1
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_123,c_14719]) ).
cnf(c_14720,negated_conjecture,
( sdtlseqdt0(A,sK1)
| sz00 = sK1
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_129,c_126]) ).
cnf(c_14721,negated_conjecture,
( sdtlseqdt0(A,sK1)
| sK1 = sz00
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_14720]) ).
cnf(c_358,negated_conjecture,
( sdtlseqdt0(A,sK1)
| ~ doDivides0(A,sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_125,c_14721]) ).
cnf(c_498,plain,
sdtasdt0(sK1,sz10) = sK1,
inference(resolve,[status(thm)],[c_177,c_126]) ).
cnf(c_14722,negated_conjecture,
( B = A
| sdtasdt0(sK1,B) != sdtasdt0(sK1,A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A)
| sz00 = sK1 ),
inference(resolve,[status(thm)],[c_167,c_126]) ).
cnf(c_14723,negated_conjecture,
sz00 != sK1,
inference(copy,[status(thm)],[c_125]) ).
cnf(c_14724,negated_conjecture,
( B = A
| sdtasdt0(sK1,B) != sdtasdt0(sK1,A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_14722,c_14723]) ).
cnf(c_14725,negated_conjecture,
( A = sK1
| sdtasdt0(sK1,A) != sdtasdt0(sK1,sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_14724,c_126]) ).
cnf(c_14726,negated_conjecture,
( sz10 = sK1
| sdtasdt0(sK1,sz10) != sdtasdt0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_14725,c_187]) ).
cnf(c_14727,negated_conjecture,
sz10 != sK1,
inference(copy,[status(thm)],[c_123]) ).
cnf(c_14728,negated_conjecture,
sdtasdt0(sK1,sz10) != sdtasdt0(sK1,sK1),
inference(resolve,[status(thm)],[c_14726,c_14727]) ).
cnf(c_14729,negated_conjecture,
sK1 != sdtasdt0(sK1,sK1),
inference(paramod,[status(thm)],[c_498,c_14728]) ).
cnf(c_637,negated_conjecture,
sdtasdt0(sK1,sK1) != sK1,
inference(copy,[status(thm)],[c_14729]) ).
cnf(c_14730,negated_conjecture,
( sdtlseqdt0(sK1,sdtasdt0(sK1,sK1))
| sz00 = sK1 ),
inference(resolve,[status(thm)],[c_229,c_126]) ).
cnf(c_14731,negated_conjecture,
( sdtlseqdt0(sK1,sdtasdt0(sK1,sK1))
| sK1 = sz00 ),
inference(copy,[status(thm)],[c_14730]) ).
cnf(c_890,negated_conjecture,
sdtlseqdt0(sK1,sdtasdt0(sK1,sK1)),
inference(resolve,[status(thm)],[c_125,c_14731]) ).
cnf(c_982,plain,
aNaturalNumber0(sdtasdt0(sK1,sK1)),
inference(resolve,[status(thm)],[c_283,c_126]) ).
cnf(c_1989,plain,
( sdtlseqdt0(sdtasdt0(sK1,sK1),sK1)
| ~ doDivides0(sdtasdt0(sK1,sK1),sK1) ),
inference(resolve,[status(thm)],[c_982,c_358]) ).
cnf(c_2146,plain,
sdtasdt0(sdtasdt0(sK1,sK1),sz00) = sz00,
inference(resolve,[status(thm)],[c_982,c_175]) ).
cnf(c_14732,plain,
( sK0(sK1) != sK1
| sdtasdt0(sK1,sz10) != sK1 ),
inference(resolve,[status(thm)],[c_335,c_187]) ).
cnf(c_14733,plain,
( sK0(sK1) != sK1
| sK1 != sK1 ),
inference(paramod,[status(thm)],[c_498,c_14732]) ).
cnf(c_4550,plain,
sK0(sK1) != sK1,
inference(copy,[status(thm)],[c_14733]) ).
cnf(c_14734,negated_conjecture,
( sK0(sK1) != sz10
| sz10 = sK1
| sz00 = sK1
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_498,c_63]) ).
cnf(c_14735,negated_conjecture,
( sK0(sK1) != sz10
| sz10 = sK1
| sK1 = sz00
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK1) ),
inference(copy,[status(thm)],[c_14734]) ).
cnf(c_14736,negated_conjecture,
( sK0(sK1) != sz10
| sK1 = sz10
| sK1 = sz00
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK1) ),
inference(copy,[status(thm)],[c_14735]) ).
cnf(c_14737,negated_conjecture,
( sK0(sK1) != sz10
| sK1 = sz10
| sK1 = sz00
| ~ aNaturalNumber0(sz10) ),
inference(resolve,[status(thm)],[c_126,c_14736]) ).
cnf(c_14738,negated_conjecture,
( sK0(sK1) != sz10
| sK1 = sz10
| sK1 = sz00 ),
inference(resolve,[status(thm)],[c_187,c_14737]) ).
cnf(c_14739,negated_conjecture,
( sK0(sK1) != sz10
| sK1 = sz10 ),
inference(resolve,[status(thm)],[c_125,c_14738]) ).
cnf(c_4932,negated_conjecture,
sK0(sK1) != sz10,
inference(resolve,[status(thm)],[c_123,c_14739]) ).
cnf(c_14740,negated_conjecture,
( doDivides0(sK0(sK1),sK1)
| sz10 = sK1
| sz00 = sK1
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_498,c_61]) ).
cnf(c_14741,negated_conjecture,
( doDivides0(sK0(sK1),sK1)
| sz10 = sK1
| sK1 = sz00
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK1) ),
inference(copy,[status(thm)],[c_14740]) ).
cnf(c_14742,negated_conjecture,
( doDivides0(sK0(sK1),sK1)
| sK1 = sz10
| sK1 = sz00
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK1) ),
inference(copy,[status(thm)],[c_14741]) ).
cnf(c_14743,negated_conjecture,
( doDivides0(sK0(sK1),sK1)
| sK1 = sz10
| sK1 = sz00
| ~ aNaturalNumber0(sz10) ),
inference(resolve,[status(thm)],[c_126,c_14742]) ).
cnf(c_14744,negated_conjecture,
( doDivides0(sK0(sK1),sK1)
| sK1 = sz10
| sK1 = sz00 ),
inference(resolve,[status(thm)],[c_187,c_14743]) ).
cnf(c_14745,negated_conjecture,
( doDivides0(sK0(sK1),sK1)
| sK1 = sz10 ),
inference(resolve,[status(thm)],[c_125,c_14744]) ).
cnf(c_4933,negated_conjecture,
doDivides0(sK0(sK1),sK1),
inference(resolve,[status(thm)],[c_123,c_14745]) ).
cnf(c_14746,negated_conjecture,
( aNaturalNumber0(sK0(sK1))
| sz10 = sK1
| sz00 = sK1
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_498,c_59]) ).
cnf(c_14747,negated_conjecture,
( aNaturalNumber0(sK0(sK1))
| sz10 = sK1
| sK1 = sz00
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK1) ),
inference(copy,[status(thm)],[c_14746]) ).
cnf(c_14748,negated_conjecture,
( aNaturalNumber0(sK0(sK1))
| sK1 = sz10
| sK1 = sz00
| ~ aNaturalNumber0(sz10)
| ~ aNaturalNumber0(sK1) ),
inference(copy,[status(thm)],[c_14747]) ).
cnf(c_14749,negated_conjecture,
( aNaturalNumber0(sK0(sK1))
| sK1 = sz10
| sK1 = sz00
| ~ aNaturalNumber0(sz10) ),
inference(resolve,[status(thm)],[c_126,c_14748]) ).
cnf(c_14750,negated_conjecture,
( aNaturalNumber0(sK0(sK1))
| sK1 = sz10
| sK1 = sz00 ),
inference(resolve,[status(thm)],[c_187,c_14749]) ).
cnf(c_14751,negated_conjecture,
( aNaturalNumber0(sK0(sK1))
| sK1 = sz10 ),
inference(resolve,[status(thm)],[c_125,c_14750]) ).
cnf(c_4934,negated_conjecture,
aNaturalNumber0(sK0(sK1)),
inference(resolve,[status(thm)],[c_123,c_14751]) ).
cnf(c_14752,plain,
( sdtlseqdt0(sK0(sK1),sK1)
| ~ doDivides0(sK0(sK1),sK1) ),
inference(resolve,[status(thm)],[c_4934,c_358]) ).
cnf(c_5771,plain,
sdtlseqdt0(sK0(sK1),sK1),
inference(resolve,[status(thm)],[c_4933,c_14752]) ).
cnf(c_14753,negated_conjecture,
( aNaturalNumber0(sK2(sK0(sK1)))
| ~ iLess0(sK0(sK1),sK1)
| sz10 = sK0(sK1)
| sz00 = sK0(sK1) ),
inference(resolve,[status(thm)],[c_4934,c_121]) ).
cnf(c_14754,negated_conjecture,
( aNaturalNumber0(sK2(sK0(sK1)))
| ~ iLess0(sK0(sK1),sK1)
| sz10 = sK0(sK1)
| sK0(sK1) = sz00 ),
inference(copy,[status(thm)],[c_14753]) ).
cnf(c_14755,negated_conjecture,
( aNaturalNumber0(sK2(sK0(sK1)))
| ~ iLess0(sK0(sK1),sK1)
| sK0(sK1) = sz10
| sK0(sK1) = sz00 ),
inference(copy,[status(thm)],[c_14754]) ).
cnf(c_6024,negated_conjecture,
( aNaturalNumber0(sK2(sK0(sK1)))
| ~ iLess0(sK0(sK1),sK1)
| sK0(sK1) = sz00 ),
inference(resolve,[status(thm)],[c_4932,c_14755]) ).
cnf(c_14756,negated_conjecture,
( doDivides0(sK2(sK0(sK1)),sK0(sK1))
| ~ iLess0(sK0(sK1),sK1)
| sz10 = sK0(sK1)
| sz00 = sK0(sK1) ),
inference(resolve,[status(thm)],[c_4934,c_115]) ).
cnf(c_14757,negated_conjecture,
( doDivides0(sK2(sK0(sK1)),sK0(sK1))
| ~ iLess0(sK0(sK1),sK1)
| sz10 = sK0(sK1)
| sK0(sK1) = sz00 ),
inference(copy,[status(thm)],[c_14756]) ).
cnf(c_14758,negated_conjecture,
( doDivides0(sK2(sK0(sK1)),sK0(sK1))
| ~ iLess0(sK0(sK1),sK1)
| sK0(sK1) = sz10
| sK0(sK1) = sz00 ),
inference(copy,[status(thm)],[c_14757]) ).
cnf(c_6027,negated_conjecture,
( doDivides0(sK2(sK0(sK1)),sK0(sK1))
| ~ iLess0(sK0(sK1),sK1)
| sK0(sK1) = sz00 ),
inference(resolve,[status(thm)],[c_4932,c_14758]) ).
cnf(c_14759,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_4934,c_57]) ).
cnf(c_14760,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_14759]) ).
cnf(c_14761,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_14760]) ).
cnf(c_6071,negated_conjecture,
( ~ iLess0(sK0(sK1),sK1)
| sK0(sK1) = sz00
| ~ doDivides0(sK2(sK0(sK1)),sK1)
| ~ aNaturalNumber0(sK2(sK0(sK1))) ),
inference(resolve,[status(thm)],[c_4932,c_14761]) ).
cnf(c_14762,plain,
( doDivides0(A,sK1)
| ~ doDivides0(A,sK0(sK1))
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sK0(sK1))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4933,c_132]) ).
cnf(c_14763,plain,
( doDivides0(A,sK1)
| ~ doDivides0(A,sK0(sK1))
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4934,c_14762]) ).
cnf(c_6224,negated_conjecture,
( doDivides0(A,sK1)
| ~ doDivides0(A,sK0(sK1))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_126,c_14763]) ).
cnf(c_14764,plain,
( iLess0(sK0(sK1),sK1)
| sK1 = sK0(sK1)
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sK0(sK1)) ),
inference(resolve,[status(thm)],[c_5771,c_139]) ).
cnf(c_14765,plain,
( iLess0(sK0(sK1),sK1)
| sK0(sK1) = sK1
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sK0(sK1)) ),
inference(copy,[status(thm)],[c_14764]) ).
cnf(c_14766,plain,
( iLess0(sK0(sK1),sK1)
| sK0(sK1) = sK1
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_4934,c_14765]) ).
cnf(c_14767,negated_conjecture,
( iLess0(sK0(sK1),sK1)
| sK0(sK1) = sK1 ),
inference(resolve,[status(thm)],[c_126,c_14766]) ).
cnf(c_6758,negated_conjecture,
iLess0(sK0(sK1),sK1),
inference(resolve,[status(thm)],[c_4550,c_14767]) ).
cnf(c_6759,negated_conjecture,
( sK0(sK1) = sz00
| ~ doDivides0(sK2(sK0(sK1)),sK1)
| ~ aNaturalNumber0(sK2(sK0(sK1))) ),
inference(resolve,[status(thm)],[c_6758,c_6071]) ).
cnf(c_6765,negated_conjecture,
( doDivides0(sK2(sK0(sK1)),sK0(sK1))
| sK0(sK1) = sz00 ),
inference(resolve,[status(thm)],[c_6758,c_6027]) ).
cnf(c_6768,negated_conjecture,
( aNaturalNumber0(sK2(sK0(sK1)))
| sK0(sK1) = sz00 ),
inference(resolve,[status(thm)],[c_6758,c_6024]) ).
cnf(c_14768,plain,
( sK1 = sdtasdt0(sK1,sK1)
| ~ sdtlseqdt0(sdtasdt0(sK1,sK1),sK1)
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sdtasdt0(sK1,sK1)) ),
inference(resolve,[status(thm)],[c_890,c_153]) ).
cnf(c_14769,plain,
( sdtasdt0(sK1,sK1) = sK1
| ~ sdtlseqdt0(sdtasdt0(sK1,sK1),sK1)
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sdtasdt0(sK1,sK1)) ),
inference(copy,[status(thm)],[c_14768]) ).
cnf(c_14770,plain,
( sdtasdt0(sK1,sK1) = sK1
| ~ sdtlseqdt0(sdtasdt0(sK1,sK1),sK1)
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_982,c_14769]) ).
cnf(c_14771,negated_conjecture,
( sdtasdt0(sK1,sK1) = sK1
| ~ sdtlseqdt0(sdtasdt0(sK1,sK1),sK1) ),
inference(resolve,[status(thm)],[c_126,c_14770]) ).
cnf(c_7316,negated_conjecture,
~ sdtlseqdt0(sdtasdt0(sK1,sK1),sK1),
inference(resolve,[status(thm)],[c_637,c_14771]) ).
cnf(c_7328,plain,
~ doDivides0(sdtasdt0(sK1,sK1),sK1),
inference(resolve,[status(thm)],[c_7316,c_1989]) ).
cnf(c_14772,plain,
( doDivides0(sdtasdt0(sK1,sK1),B)
| ~ doDivides0(A,B)
| ~ doDivides0(sdtasdt0(sK1,sK1),A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_132,c_982]) ).
cnf(c_14773,plain,
( doDivides0(sdtasdt0(sK1,sK1),A)
| ~ doDivides0(sK0(sK1),A)
| ~ doDivides0(sdtasdt0(sK1,sK1),sK0(sK1))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_14772,c_4934]) ).
cnf(c_14774,negated_conjecture,
( doDivides0(sdtasdt0(sK1,sK1),sK1)
| ~ doDivides0(sK0(sK1),sK1)
| ~ doDivides0(sdtasdt0(sK1,sK1),sK0(sK1)) ),
inference(resolve,[status(thm)],[c_14773,c_126]) ).
cnf(c_14775,negated_conjecture,
( doDivides0(sdtasdt0(sK1,sK1),sK1)
| ~ doDivides0(sdtasdt0(sK1,sK1),sK0(sK1)) ),
inference(resolve,[status(thm)],[c_14774,c_4933]) ).
cnf(c_7388,negated_conjecture,
~ doDivides0(sdtasdt0(sK1,sK1),sK0(sK1)),
inference(resolve,[status(thm)],[c_14775,c_7328]) ).
cnf(c_14776,plain,
( sdtasdt0(sdtasdt0(sK1,sK1),B) != A
| ~ aNaturalNumber0(B)
| doDivides0(sdtasdt0(sK1,sK1),A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_136,c_982]) ).
cnf(c_14777,plain,
( sdtasdt0(sdtasdt0(sK1,sK1),A) != sK0(sK1)
| ~ aNaturalNumber0(A)
| doDivides0(sdtasdt0(sK1,sK1),sK0(sK1)) ),
inference(resolve,[status(thm)],[c_14776,c_4934]) ).
cnf(c_14778,plain,
( sdtasdt0(sdtasdt0(sK1,sK1),A) != sK0(sK1)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_14777,c_7388]) ).
cnf(c_14779,plain,
sdtasdt0(sdtasdt0(sK1,sK1),sz00) != sK0(sK1),
inference(resolve,[status(thm)],[c_14778,c_188]) ).
cnf(c_14780,plain,
sz00 != sK0(sK1),
inference(paramod,[status(thm)],[c_2146,c_14779]) ).
cnf(c_7645,plain,
sK0(sK1) != sz00,
inference(copy,[status(thm)],[c_14780]) ).
cnf(c_7657,negated_conjecture,
aNaturalNumber0(sK2(sK0(sK1))),
inference(resolve,[status(thm)],[c_7645,c_6768]) ).
cnf(c_7660,negated_conjecture,
doDivides0(sK2(sK0(sK1)),sK0(sK1)),
inference(resolve,[status(thm)],[c_7645,c_6765]) ).
cnf(c_14781,negated_conjecture,
( sK0(sK1) = sz00
| ~ doDivides0(sK2(sK0(sK1)),sK1) ),
inference(resolve,[status(thm)],[c_7657,c_6759]) ).
cnf(c_7666,negated_conjecture,
~ doDivides0(sK2(sK0(sK1)),sK1),
inference(resolve,[status(thm)],[c_7645,c_14781]) ).
cnf(c_14782,plain,
( doDivides0(sK2(sK0(sK1)),sK1)
| ~ doDivides0(sK2(sK0(sK1)),sK0(sK1)) ),
inference(resolve,[status(thm)],[c_7657,c_6224]) ).
cnf(c_14783,plain,
doDivides0(sK2(sK0(sK1)),sK1),
inference(resolve,[status(thm)],[c_7660,c_14782]) ).
cnf(c_14712,plain,
$false,
inference(resolve,[status(thm)],[c_7666,c_14783]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM481+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.58 % Computer : n019.cluster.edu
% 0.10/5.58 % Model : x86_64 x86_64
% 0.10/5.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.58 % Memory : 8046.5625MB
% 0.10/5.58 % OS : Linux 6.8.0-71-generic
% 0.10/5.59 % CPULimit : 300
% 0.10/5.59 % WCLimit : 300
% 0.10/5.59 % DateTime : Sat Sep 26 02:55:40 UTC 2026
% 0.10/5.59 % CPUTime :
% 0.10/5.59 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.59 % Process 246564 was started by sandbox2 on n019,
% 0.10/5.59 % Sat Sep 26 02:55:40 2026
% 0.10/5.59 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/5.60
% 0.14/5.60 % From the command line: assign(max_seconds, 300).
% 48.29/11.77
% 48.29/11.77 % given #500 (T,wt=15): 10253 iLess0(sz00,sdtpldt0(sz10,c1)). [resolve(9461,a,139,d),unit_del(a,188),unit_del(b,9441),unit_del(c,640)].
% 48.29/11.77
% 48.29/11.77 % SZS status Theorem for theBenchmark
% 48.29/11.77
% 48.29/11.77 % Proof 1 at 5.83 (+ 0.31) seconds.
% 48.29/11.77 % Length of proof is 83.
% 48.29/11.77 % Level of proof is 10.
% 48.29/11.77 % Maximum clause weight is 32.000.
% 48.29/11.77 % Given clauses 842.
% 48.29/11.77
% 48.29/11.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------