%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM528+3 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:17 AM UTC 2026
% Result : Theorem 33.58s 5.33s
% Output : CNFRefutation 33.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 23
% Syntax : Number of formulae : 232 ( 58 unt; 0 def)
% Number of atoms : 716 ( 306 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 796 ( 312 ~; 392 |; 66 &)
% ( 3 <=>; 23 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% Number of variables : 111 ( 0 sgn 32 !; 12 ?)
% 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_AddZero,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtpldt0(sz00,W0)
& sdtpldt0(W0,sz00) = W0 ) ),
file('theBenchmark.p',m_AddZero) ).
fof(m_MulUnit,axiom,
! [W0] :
( aNaturalNumber0(W0)
=> ( W0 = sdtasdt0(sz10,W0)
& sdtasdt0(W0,sz10) = W0 ) ),
file('theBenchmark.p',m_MulUnit) ).
fof(mZeroMul,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( sdtasdt0(W0,W1) = sz00
=> ( W1 = sz00
| W0 = sz00 ) ) ),
file('theBenchmark.p',mZeroMul) ).
fof(mLEAsym,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& sdtlseqdt0(W0,W1) )
=> W0 = W1 ) ),
file('theBenchmark.p',mLEAsym) ).
fof(mLETotal,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1) ) ),
file('theBenchmark.p',mLETotal) ).
fof(mMonMul2,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( W0 != sz00
=> sdtlseqdt0(W1,sdtasdt0(W1,W0)) ) ),
file('theBenchmark.p',mMonMul2) ).
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(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(mDivAsso,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( doDivides0(W0,W1)
& W0 != sz00 )
=> ! [W2] :
( aNaturalNumber0(W2)
=> sdtasdt0(W2,sdtsldt0(W1,W0)) = sdtsldt0(sdtasdt0(W2,W1),W0) ) ) ),
file('theBenchmark.p',mDivAsso) ).
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(mPrimDiv,axiom,
! [W0] :
( ( W0 != sz10
& W0 != sz00
& aNaturalNumber0(W0) )
=> ? [W1] :
( isPrime0(W1)
& doDivides0(W1,W0)
& aNaturalNumber0(W1) ) ),
file('theBenchmark.p',mPrimDiv) ).
fof(m__2987,axiom,
( xp != sz00
& xm != sz00
& xn != sz00
& aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('theBenchmark.p',m__2987) ).
fof(m__3025,axiom,
( isPrime0(xp)
& ! [W0] :
( ( ( doDivides0(W0,xp)
| ? [W1] :
( xp = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) ) )
& aNaturalNumber0(W0) )
=> ( W0 = xp
| W0 = sz10 ) )
& xp != sz10 ),
file('theBenchmark.p',m__3025) ).
fof(m__3046,axiom,
( doDivides0(xp,xn)
& ? [W0] :
( xn = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& doDivides0(xp,sdtasdt0(xn,xn))
& ? [W0] :
( sdtasdt0(xn,xn) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ),
file('theBenchmark.p',m__3046) ).
fof(m__3059,axiom,
( xq = sdtsldt0(xn,xp)
& xn = sdtasdt0(xp,xq)
& aNaturalNumber0(xq) ),
file('theBenchmark.p',m__3059) ).
fof(m__3152,axiom,
( ( sdtlseqdt0(xn,xm)
| ? [W0] :
( sdtpldt0(xn,W0) = xm
& aNaturalNumber0(W0) ) )
=> ( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
& ? [W0] :
( sdtpldt0(sdtasdt0(xn,xn),W0) = sdtasdt0(xm,xm)
& aNaturalNumber0(W0) ) ) ),
file('theBenchmark.p',m__3152) ).
fof(m__,conjecture,
( ( sdtlseqdt0(xm,xn)
| ? [W0] :
( sdtpldt0(xm,W0) = xn
& aNaturalNumber0(W0) ) )
& xm != xn ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( ( sdtlseqdt0(xm,xn)
| ? [W0] :
( sdtpldt0(xm,W0) = xn
& aNaturalNumber0(W0) ) )
& xm != xn ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_48,plain,
( sz10 != A
| ~ isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefPrime]) ).
cnf(c_49,plain,
( sz00 != A
| ~ isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefPrime]) ).
fof(nnf_37,plain,
! [W0] :
( ? [W1] :
( isPrime0(W1)
& doDivides0(W1,W0)
& aNaturalNumber0(W1) )
| sz10 = W0
| sz00 = W0
| ~ aNaturalNumber0(W0) ),
inference(fof_nnf,[status(thm)],[mPrimDiv]) ).
fof(sk_mPrimDiv_sk,plain,
! [W0] :
( ( isPrime0(sK0(W0))
& doDivides0(sK0(W0),W0)
& aNaturalNumber0(sK0(W0)) )
| sz10 = W0
| sz00 = W0
| ~ aNaturalNumber0(W0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(W1,sK0(W0))],[nnf_37]) ).
fof(sk_mPrimDiv,plain,
( ! [VAR_0] :
( isPrime0(sK0(VAR_0))
| sz10 = VAR_0
| sz00 = VAR_0
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( doDivides0(sK0(VAR_0),VAR_0)
| sz10 = VAR_0
| sz00 = VAR_0
| ~ aNaturalNumber0(VAR_0) )
& ! [VAR_0] :
( aNaturalNumber0(sK0(VAR_0))
| sz10 = VAR_0
| sz00 = VAR_0
| ~ aNaturalNumber0(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_mPrimDiv_sk]) ).
cnf(c_53,plain,
( isPrime0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimDiv]) ).
cnf(c_85,plain,
( sz00 != sK0(A)
| ~ aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_53,c_49]) ).
cnf(c_86,plain,
( sK0(A) != sz00
| ~ aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_85]) ).
cnf(c_87,plain,
( sz10 != sK0(A)
| ~ aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_53,c_48]) ).
cnf(c_88,plain,
( sK0(A) != sz10
| ~ aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_87]) ).
cnf(c_99,negated_conjecture,
( ~ sdtlseqdt0(xm,xn)
| xm = xn ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_101,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
| ~ sdtlseqdt0(xn,xm) ),
inference(clausify,[status(thm)],[m__3152]) ).
cnf(c_105,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
| sdtpldt0(xn,A) != xm
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m__3152]) ).
fof(m__3082,axiom,
sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(xq,xq)),
file('theBenchmark.p',m__3082) ).
cnf(c_109,plain,
sdtasdt0(xm,xm) = sdtasdt0(xp,sdtasdt0(xq,xq)),
inference(clausify,[status(thm)],[m__3082]) ).
cnf(c_110,plain,
sdtasdt0(xp,sdtasdt0(xq,xq)) = sdtasdt0(xm,xm),
inference(copy,[status(thm)],[c_109]) ).
cnf(c_111,plain,
sdtsldt0(xn,xp) = xq,
inference(clausify,[status(thm)],[m__3059]) ).
cnf(c_113,plain,
aNaturalNumber0(xq),
inference(clausify,[status(thm)],[m__3059]) ).
fof(nnf_42,plain,
( doDivides0(xp,xn)
& ? [W0] :
( sdtasdt0(xp,W0) = xn
& aNaturalNumber0(W0) )
& doDivides0(xp,sdtasdt0(xn,xn))
& ? [X0] :
( sdtasdt0(xp,X0) = sdtasdt0(xn,xn)
& aNaturalNumber0(X0) ) ),
inference(fof_nnf,[status(thm)],[m__3046]) ).
fof(sk_m__3046,plain,
( doDivides0(xp,xn)
& sdtasdt0(xp,sK4) = xn
& aNaturalNumber0(sK4)
& doDivides0(xp,sdtasdt0(xn,xn))
& sdtasdt0(xp,sK1) = sdtasdt0(xn,xn)
& aNaturalNumber0(sK1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK4]),skolemize(X0,sK1),skolemize(W0,sK4)],[nnf_42]) ).
cnf(c_114,plain,
doDivides0(xp,xn),
inference(split_conjunct,[status(thm)],[sk_m__3046]) ).
cnf(c_117,plain,
doDivides0(xp,sdtasdt0(xn,xn)),
inference(split_conjunct,[status(thm)],[sk_m__3046]) ).
cnf(c_118,plain,
sdtasdt0(xp,sK1) = sdtasdt0(xn,xn),
inference(split_conjunct,[status(thm)],[sk_m__3046]) ).
cnf(c_119,plain,
aNaturalNumber0(sK1),
inference(split_conjunct,[status(thm)],[sk_m__3046]) ).
cnf(c_120,plain,
( xp = A
| sz10 = A
| ~ doDivides0(A,xp)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m__3025]) ).
cnf(c_122,plain,
xp != sz10,
inference(clausify,[status(thm)],[m__3025]) ).
fof(m__3014,axiom,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
file('theBenchmark.p',m__3014) ).
cnf(c_123,plain,
sdtasdt0(xp,sdtasdt0(xm,xm)) = sdtasdt0(xn,xn),
inference(clausify,[status(thm)],[m__3014]) ).
cnf(c_136,plain,
xp != sz00,
inference(clausify,[status(thm)],[m__2987]) ).
cnf(c_137,plain,
xm != sz00,
inference(clausify,[status(thm)],[m__2987]) ).
cnf(c_139,plain,
aNaturalNumber0(xp),
inference(clausify,[status(thm)],[m__2987]) ).
cnf(c_140,plain,
aNaturalNumber0(xm),
inference(clausify,[status(thm)],[m__2987]) ).
cnf(c_141,plain,
aNaturalNumber0(xn),
inference(clausify,[status(thm)],[m__2987]) ).
cnf(c_142,plain,
( doDivides0(sK0(A),A)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimDiv]) ).
cnf(c_143,plain,
( aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimDiv]) ).
cnf(c_144,plain,
( sdtsldt0(sdtasdt0(C,B),A) = sdtasdt0(C,sdtsldt0(B,A))
| ~ aNaturalNumber0(C)
| ~ doDivides0(A,B)
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDivAsso]) ).
cnf(c_149,plain,
( doDivides0(A,C)
| ~ doDivides0(B,C)
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDivTrans]) ).
cnf(c_150,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]) ).
cnf(c_151,plain,
( sdtasdt0(A,C) = B
| sdtsldt0(B,A) != C
| ~ doDivides0(A,B)
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefQuot]) ).
cnf(c_153,plain,
( sdtasdt0(A,C) != B
| ~ aNaturalNumber0(C)
| doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefDiv]) ).
cnf(c_157,plain,
( sdtlseqdt0(B,sdtasdt0(B,A))
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mMonMul2]) ).
cnf(c_167,plain,
( sdtlseqdt0(B,A)
| sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLETotal]) ).
cnf(c_170,plain,
( B = A
| ~ sdtlseqdt0(B,A)
| ~ sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLEAsym]) ).
cnf(c_178,plain,
( B = sz00
| sz00 = A
| sdtasdt0(A,B) != sz00
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mZeroMul]) ).
cnf(c_179,plain,
( sz00 = B
| sz00 = A
| sdtasdt0(A,B) != sz00
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_178]) ).
cnf(c_194,plain,
( sdtasdt0(A,sz10) = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_MulUnit]) ).
cnf(c_198,plain,
( sdtpldt0(A,sz00) = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_AddZero]) ).
cnf(c_201,plain,
( aNaturalNumber0(sdtasdt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mSortsB_02]) ).
cnf(c_204,plain,
aNaturalNumber0(sz10),
inference(clausify,[status(thm)],[mSortsC_01]) ).
fof(mSortsC,axiom,
aNaturalNumber0(sz00),
file('theBenchmark.p',mSortsC) ).
cnf(c_205,plain,
aNaturalNumber0(sz00),
inference(clausify,[status(thm)],[mSortsC]) ).
cnf(c_272,plain,
( sdtsldt0(sdtasdt0(B,B),A) = sdtasdt0(B,sdtsldt0(B,A))
| ~ doDivides0(A,B)
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_144]) ).
cnf(c_279,plain,
( sdtasdt0(A,B) != A
| ~ aNaturalNumber0(B)
| sdtsldt0(A,A) = B
| ~ doDivides0(A,A)
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_150]) ).
cnf(c_284,plain,
( sdtasdt0(A,B) != A
| ~ aNaturalNumber0(B)
| doDivides0(A,A)
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_153]) ).
cnf(c_26702,plain,
( sz00 = A
| sz00 = A
| sdtasdt0(A,A) != sz00
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_179]) ).
cnf(c_319,plain,
( sz00 = A
| sdtasdt0(A,A) != sz00
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_26702]) ).
cnf(c_343,plain,
( aNaturalNumber0(sdtasdt0(A,A))
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_201]) ).
cnf(c_26703,plain,
( sK0(xp) != sz10
| ~ aNaturalNumber0(sK0(xp))
| sz10 = xp
| sz00 = xp ),
inference(resolve,[status(thm)],[c_139,c_88]) ).
cnf(c_26704,plain,
( sK0(xp) != sz10
| ~ aNaturalNumber0(sK0(xp))
| sz10 = xp
| xp = sz00 ),
inference(copy,[status(thm)],[c_26703]) ).
cnf(c_26705,plain,
( sK0(xp) != sz10
| ~ aNaturalNumber0(sK0(xp))
| xp = sz10
| xp = sz00 ),
inference(copy,[status(thm)],[c_26704]) ).
cnf(c_26706,plain,
( sK0(xp) != sz10
| ~ aNaturalNumber0(sK0(xp))
| xp = sz10 ),
inference(resolve,[status(thm)],[c_136,c_26705]) ).
cnf(c_898,plain,
( sK0(xp) != sz10
| ~ aNaturalNumber0(sK0(xp)) ),
inference(resolve,[status(thm)],[c_122,c_26706]) ).
cnf(c_26707,plain,
( sK0(xp) != sz00
| ~ aNaturalNumber0(sK0(xp))
| sz10 = xp
| sz00 = xp ),
inference(resolve,[status(thm)],[c_139,c_86]) ).
cnf(c_26708,plain,
( sK0(xp) != sz00
| ~ aNaturalNumber0(sK0(xp))
| sz10 = xp
| xp = sz00 ),
inference(copy,[status(thm)],[c_26707]) ).
cnf(c_26709,plain,
( sK0(xp) != sz00
| ~ aNaturalNumber0(sK0(xp))
| xp = sz10
| xp = sz00 ),
inference(copy,[status(thm)],[c_26708]) ).
cnf(c_26710,plain,
( sK0(xp) != sz00
| ~ aNaturalNumber0(sK0(xp))
| xp = sz10 ),
inference(resolve,[status(thm)],[c_136,c_26709]) ).
cnf(c_899,plain,
( sK0(xp) != sz00
| ~ aNaturalNumber0(sK0(xp)) ),
inference(resolve,[status(thm)],[c_122,c_26710]) ).
cnf(c_26711,plain,
( doDivides0(sK0(xp),xp)
| sz10 = xp
| sz00 = xp ),
inference(resolve,[status(thm)],[c_142,c_139]) ).
cnf(c_26712,plain,
( doDivides0(sK0(xp),xp)
| sz10 = xp
| xp = sz00 ),
inference(copy,[status(thm)],[c_26711]) ).
cnf(c_26713,plain,
( doDivides0(sK0(xp),xp)
| xp = sz10
| xp = sz00 ),
inference(copy,[status(thm)],[c_26712]) ).
cnf(c_26714,plain,
( doDivides0(sK0(xp),xp)
| xp = sz10 ),
inference(resolve,[status(thm)],[c_136,c_26713]) ).
cnf(c_1235,plain,
doDivides0(sK0(xp),xp),
inference(resolve,[status(thm)],[c_122,c_26714]) ).
cnf(c_26715,plain,
( aNaturalNumber0(sK0(xp))
| sz10 = xp
| sz00 = xp ),
inference(resolve,[status(thm)],[c_143,c_139]) ).
cnf(c_26716,plain,
( aNaturalNumber0(sK0(xp))
| sz10 = xp
| xp = sz00 ),
inference(copy,[status(thm)],[c_26715]) ).
cnf(c_26717,plain,
( aNaturalNumber0(sK0(xp))
| xp = sz10
| xp = sz00 ),
inference(copy,[status(thm)],[c_26716]) ).
cnf(c_26718,plain,
( aNaturalNumber0(sK0(xp))
| xp = sz10 ),
inference(resolve,[status(thm)],[c_136,c_26717]) ).
cnf(c_1241,plain,
aNaturalNumber0(sK0(xp)),
inference(resolve,[status(thm)],[c_122,c_26718]) ).
cnf(c_1255,plain,
sK0(xp) != sz00,
inference(resolve,[status(thm)],[c_1241,c_899]) ).
cnf(c_1256,plain,
sK0(xp) != sz10,
inference(resolve,[status(thm)],[c_1241,c_898]) ).
cnf(c_1280,plain,
( sdtsldt0(sdtasdt0(sK1,B),A) = sdtasdt0(sK1,sdtsldt0(B,A))
| ~ doDivides0(A,B)
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_144,c_119]) ).
cnf(c_1446,plain,
( sdtasdt0(A,xp) != B
| sdtsldt0(B,A) = xp
| ~ doDivides0(A,B)
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_150,c_139]) ).
cnf(c_26719,plain,
( ~ aNaturalNumber0(sdtasdt0(xm,xm))
| sdtsldt0(sdtasdt0(xn,xn),xp) = sdtasdt0(xm,xm)
| ~ doDivides0(xp,sdtasdt0(xn,xn))
| sz00 = xp
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_150,c_123]) ).
cnf(c_26720,plain,
( ~ aNaturalNumber0(sdtasdt0(xm,xm))
| sdtsldt0(sdtasdt0(xn,xn),xp) = sdtasdt0(xm,xm)
| ~ doDivides0(xp,sdtasdt0(xn,xn))
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_26719]) ).
cnf(c_26721,plain,
( ~ aNaturalNumber0(sdtasdt0(xm,xm))
| sdtsldt0(sdtasdt0(xn,xn),xp) = sdtasdt0(xm,xm)
| ~ doDivides0(xp,sdtasdt0(xn,xn))
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(resolve,[status(thm)],[c_139,c_26720]) ).
cnf(c_26722,plain,
( ~ aNaturalNumber0(sdtasdt0(xm,xm))
| sdtsldt0(sdtasdt0(xn,xn),xp) = sdtasdt0(xm,xm)
| ~ doDivides0(xp,sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(resolve,[status(thm)],[c_136,c_26721]) ).
cnf(c_1450,plain,
( ~ aNaturalNumber0(sdtasdt0(xm,xm))
| sdtsldt0(sdtasdt0(xn,xn),xp) = sdtasdt0(xm,xm)
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(resolve,[status(thm)],[c_117,c_26722]) ).
cnf(c_26723,plain,
( ~ aNaturalNumber0(sK1)
| sdtsldt0(sdtasdt0(xn,xn),xp) = sK1
| ~ doDivides0(xp,sdtasdt0(xn,xn))
| sz00 = xp
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_150,c_118]) ).
cnf(c_26724,plain,
( ~ aNaturalNumber0(sK1)
| sdtsldt0(sdtasdt0(xn,xn),xp) = sK1
| ~ doDivides0(xp,sdtasdt0(xn,xn))
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xn))
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_26723]) ).
cnf(c_26725,plain,
( ~ aNaturalNumber0(sK1)
| sdtsldt0(sdtasdt0(xn,xn),xp) = sK1
| ~ doDivides0(xp,sdtasdt0(xn,xn))
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(resolve,[status(thm)],[c_139,c_26724]) ).
cnf(c_26726,plain,
( ~ aNaturalNumber0(sK1)
| sdtsldt0(sdtasdt0(xn,xn),xp) = sK1
| ~ doDivides0(xp,sdtasdt0(xn,xn))
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(resolve,[status(thm)],[c_136,c_26725]) ).
cnf(c_26727,plain,
( ~ aNaturalNumber0(sK1)
| sdtsldt0(sdtasdt0(xn,xn),xp) = sK1
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(resolve,[status(thm)],[c_117,c_26726]) ).
cnf(c_1451,plain,
( sdtsldt0(sdtasdt0(xn,xn),xp) = sK1
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(resolve,[status(thm)],[c_119,c_26727]) ).
cnf(c_1492,plain,
( sdtasdt0(A,sdtsldt0(B,A)) = B
| ~ doDivides0(A,B)
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(xxres,[status(thm)],[c_151]) ).
cnf(c_26728,plain,
( ~ aNaturalNumber0(sdtasdt0(xq,xq))
| doDivides0(xp,sdtasdt0(xm,xm))
| ~ aNaturalNumber0(sdtasdt0(xm,xm))
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_153,c_110]) ).
cnf(c_1523,plain,
( ~ aNaturalNumber0(sdtasdt0(xq,xq))
| doDivides0(xp,sdtasdt0(xm,xm))
| ~ aNaturalNumber0(sdtasdt0(xm,xm)) ),
inference(resolve,[status(thm)],[c_139,c_26728]) ).
cnf(c_1526,plain,
( ~ aNaturalNumber0(B)
| doDivides0(A,sdtasdt0(A,B))
| ~ aNaturalNumber0(sdtasdt0(A,B))
| ~ aNaturalNumber0(A) ),
inference(xxres,[status(thm)],[c_153]) ).
cnf(c_26729,plain,
( sdtlseqdt0(A,sdtasdt0(A,xp))
| sz00 = xp
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_157,c_139]) ).
cnf(c_26730,plain,
( sdtlseqdt0(A,sdtasdt0(A,xp))
| xp = sz00
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_26729]) ).
cnf(c_1583,plain,
( sdtlseqdt0(A,sdtasdt0(A,xp))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_136,c_26730]) ).
cnf(c_1700,plain,
( sdtlseqdt0(A,xn)
| sdtlseqdt0(xn,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_167,c_141]) ).
cnf(c_26731,plain,
( A = sK1
| ~ sdtlseqdt0(A,sK1)
| ~ sdtlseqdt0(sK1,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_170,c_119]) ).
cnf(c_1738,plain,
( sK1 = A
| ~ sdtlseqdt0(A,sK1)
| ~ sdtlseqdt0(sK1,A)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_26731]) ).
cnf(c_2027,plain,
sdtasdt0(xp,sz10) = xp,
inference(resolve,[status(thm)],[c_194,c_139]) ).
cnf(c_2028,plain,
sdtasdt0(sK1,sz10) = sK1,
inference(resolve,[status(thm)],[c_194,c_119]) ).
cnf(c_2070,plain,
sdtpldt0(xn,sz00) = xn,
inference(resolve,[status(thm)],[c_198,c_141]) ).
cnf(c_2113,plain,
( aNaturalNumber0(sdtasdt0(sK1,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_201,c_119]) ).
cnf(c_26732,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
| sdtpldt0(xn,sz00) != xm ),
inference(resolve,[status(thm)],[c_205,c_105]) ).
cnf(c_26733,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
| xn != xm ),
inference(paramod,[status(thm)],[c_2070,c_26732]) ).
cnf(c_2430,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xm,xm))
| xm != xn ),
inference(copy,[status(thm)],[c_26733]) ).
cnf(c_26734,plain,
( sdtsldt0(sdtasdt0(xn,xn),xp) = sdtasdt0(xn,sdtsldt0(xn,xp))
| sz00 = xp
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_272,c_114]) ).
cnf(c_26735,plain,
( sdtsldt0(sdtasdt0(xn,xn),xp) = sdtasdt0(xn,xq)
| sz00 = xp
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp) ),
inference(paramod,[status(thm)],[c_111,c_26734]) ).
cnf(c_26736,plain,
( sdtsldt0(sdtasdt0(xn,xn),xp) = sdtasdt0(xn,xq)
| xp = sz00
| ~ aNaturalNumber0(xn)
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_26735]) ).
cnf(c_26737,plain,
( sdtsldt0(sdtasdt0(xn,xn),xp) = sdtasdt0(xn,xq)
| xp = sz00
| ~ aNaturalNumber0(xn) ),
inference(resolve,[status(thm)],[c_139,c_26736]) ).
cnf(c_26738,plain,
( sdtsldt0(sdtasdt0(xn,xn),xp) = sdtasdt0(xn,xq)
| xp = sz00 ),
inference(resolve,[status(thm)],[c_141,c_26737]) ).
cnf(c_2777,plain,
sdtsldt0(sdtasdt0(xn,xn),xp) = sdtasdt0(xn,xq),
inference(resolve,[status(thm)],[c_136,c_26738]) ).
cnf(c_2782,plain,
( sdtasdt0(xn,xq) = sK1
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(paramod,[status(thm)],[c_2777,c_1451]) ).
cnf(c_26739,plain,
( ~ aNaturalNumber0(sdtasdt0(xm,xm))
| sdtasdt0(xn,xq) = sdtasdt0(xm,xm)
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(paramod,[status(thm)],[c_2777,c_1450]) ).
cnf(c_2783,plain,
( ~ aNaturalNumber0(sdtasdt0(xm,xm))
| sdtasdt0(xm,xm) = sdtasdt0(xn,xq)
| ~ aNaturalNumber0(sdtasdt0(xn,xn)) ),
inference(copy,[status(thm)],[c_26739]) ).
cnf(c_26740,plain,
( sz00 = xm
| sdtasdt0(xm,xm) != sz00 ),
inference(resolve,[status(thm)],[c_319,c_140]) ).
cnf(c_26741,plain,
( xm = sz00
| sdtasdt0(xm,xm) != sz00 ),
inference(copy,[status(thm)],[c_26740]) ).
cnf(c_3038,plain,
sdtasdt0(xm,xm) != sz00,
inference(resolve,[status(thm)],[c_137,c_26741]) ).
cnf(c_3171,plain,
aNaturalNumber0(sdtasdt0(xn,xn)),
inference(resolve,[status(thm)],[c_343,c_141]) ).
cnf(c_3172,plain,
aNaturalNumber0(sdtasdt0(xm,xm)),
inference(resolve,[status(thm)],[c_343,c_140]) ).
cnf(c_3175,plain,
aNaturalNumber0(sdtasdt0(xq,xq)),
inference(resolve,[status(thm)],[c_343,c_113]) ).
cnf(c_26742,plain,
( ~ aNaturalNumber0(sdtasdt0(xm,xm))
| sdtasdt0(xm,xm) = sdtasdt0(xn,xq) ),
inference(resolve,[status(thm)],[c_3171,c_2783]) ).
cnf(c_3189,plain,
sdtasdt0(xm,xm) = sdtasdt0(xn,xq),
inference(resolve,[status(thm)],[c_3172,c_26742]) ).
cnf(c_3190,plain,
sdtasdt0(xn,xq) = sK1,
inference(resolve,[status(thm)],[c_3171,c_2782]) ).
cnf(c_26743,plain,
( ~ aNaturalNumber0(sdtasdt0(xq,xq))
| doDivides0(xp,sdtasdt0(xm,xm))
| ~ aNaturalNumber0(sdtasdt0(xn,xq)) ),
inference(paramod,[status(thm)],[c_3189,c_1523]) ).
cnf(c_26744,plain,
( ~ aNaturalNumber0(sdtasdt0(xq,xq))
| doDivides0(xp,sdtasdt0(xm,xm))
| ~ aNaturalNumber0(sK1) ),
inference(paramod,[status(thm)],[c_3190,c_26743]) ).
cnf(c_26745,plain,
( ~ aNaturalNumber0(sdtasdt0(xq,xq))
| doDivides0(xp,sdtasdt0(xn,xq))
| ~ aNaturalNumber0(sK1) ),
inference(paramod,[status(thm)],[c_3189,c_26744]) ).
cnf(c_26746,plain,
( ~ aNaturalNumber0(sdtasdt0(xq,xq))
| doDivides0(xp,sK1)
| ~ aNaturalNumber0(sK1) ),
inference(paramod,[status(thm)],[c_3190,c_26745]) ).
cnf(c_26747,plain,
( ~ aNaturalNumber0(sdtasdt0(xq,xq))
| doDivides0(xp,sK1) ),
inference(resolve,[status(thm)],[c_119,c_26746]) ).
cnf(c_3214,plain,
doDivides0(xp,sK1),
inference(resolve,[status(thm)],[c_3175,c_26747]) ).
cnf(c_26748,plain,
sdtasdt0(xn,xq) != sz00,
inference(paramod,[status(thm)],[c_3189,c_3038]) ).
cnf(c_3247,plain,
sK1 != sz00,
inference(paramod,[status(thm)],[c_3190,c_26748]) ).
cnf(c_26749,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xn,xq))
| xm != xn ),
inference(paramod,[status(thm)],[c_3189,c_2430]) ).
cnf(c_3300,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sK1)
| xm != xn ),
inference(paramod,[status(thm)],[c_3190,c_26749]) ).
cnf(c_26750,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sdtasdt0(xn,xq))
| ~ sdtlseqdt0(xn,xm) ),
inference(paramod,[status(thm)],[c_3189,c_101]) ).
cnf(c_3373,plain,
( sdtlseqdt0(sdtasdt0(xn,xn),sK1)
| ~ sdtlseqdt0(xn,xm) ),
inference(paramod,[status(thm)],[c_3190,c_26750]) ).
cnf(c_26751,plain,
( doDivides0(xp,A)
| ~ doDivides0(sK1,A)
| ~ aNaturalNumber0(A)
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_3214,c_149]) ).
cnf(c_26752,plain,
( doDivides0(xp,A)
| ~ doDivides0(sK1,A)
| ~ aNaturalNumber0(A)
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_139,c_26751]) ).
cnf(c_3819,plain,
( doDivides0(xp,A)
| ~ doDivides0(sK1,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_119,c_26752]) ).
cnf(c_26753,plain,
( doDivides0(sK0(sK0(xp)),sK0(xp))
| sz10 = sK0(xp)
| sz00 = sK0(xp) ),
inference(resolve,[status(thm)],[c_1241,c_142]) ).
cnf(c_26754,plain,
( doDivides0(sK0(sK0(xp)),sK0(xp))
| sz10 = sK0(xp)
| sK0(xp) = sz00 ),
inference(copy,[status(thm)],[c_26753]) ).
cnf(c_26755,plain,
( doDivides0(sK0(sK0(xp)),sK0(xp))
| sK0(xp) = sz10
| sK0(xp) = sz00 ),
inference(copy,[status(thm)],[c_26754]) ).
cnf(c_26756,plain,
( doDivides0(sK0(sK0(xp)),sK0(xp))
| sK0(xp) = sz10 ),
inference(resolve,[status(thm)],[c_1255,c_26755]) ).
cnf(c_4578,plain,
doDivides0(sK0(sK0(xp)),sK0(xp)),
inference(resolve,[status(thm)],[c_1256,c_26756]) ).
cnf(c_26757,plain,
( xp = sK0(xp)
| sz10 = sK0(xp)
| ~ doDivides0(sK0(xp),xp) ),
inference(resolve,[status(thm)],[c_1241,c_120]) ).
cnf(c_26758,plain,
( xp = sK0(xp)
| sK0(xp) = sz10
| ~ doDivides0(sK0(xp),xp) ),
inference(copy,[status(thm)],[c_26757]) ).
cnf(c_26759,plain,
( sK0(xp) = xp
| sK0(xp) = sz10
| ~ doDivides0(sK0(xp),xp) ),
inference(copy,[status(thm)],[c_26758]) ).
cnf(c_26760,plain,
( sK0(xp) = xp
| sK0(xp) = sz10 ),
inference(resolve,[status(thm)],[c_1235,c_26759]) ).
cnf(c_4593,plain,
sK0(xp) = xp,
inference(resolve,[status(thm)],[c_1256,c_26760]) ).
cnf(c_26761,plain,
doDivides0(sK0(xp),sK0(xp)),
inference(paramod,[status(thm)],[c_4593,c_4578]) ).
cnf(c_26762,plain,
doDivides0(xp,sK0(xp)),
inference(paramod,[status(thm)],[c_4593,c_26761]) ).
cnf(c_4594,plain,
doDivides0(xp,xp),
inference(paramod,[status(thm)],[c_4593,c_26762]) ).
cnf(c_4810,plain,
( sdtlseqdt0(xm,xn)
| sdtlseqdt0(xn,xm) ),
inference(resolve,[status(thm)],[c_1700,c_140]) ).
cnf(c_4885,plain,
( xm = xn
| sdtlseqdt0(xn,xm) ),
inference(resolve,[status(thm)],[c_4810,c_99]) ).
cnf(c_26763,plain,
( ~ aNaturalNumber0(sz10)
| sdtsldt0(xp,xp) = sz10
| ~ doDivides0(xp,xp)
| sz00 = xp
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_2027,c_279]) ).
cnf(c_26764,plain,
( ~ aNaturalNumber0(sz10)
| sdtsldt0(xp,xp) = sz10
| ~ doDivides0(xp,xp)
| xp = sz00
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_26763]) ).
cnf(c_26765,plain,
( ~ aNaturalNumber0(sz10)
| sdtsldt0(xp,xp) = sz10
| ~ doDivides0(xp,xp)
| xp = sz00 ),
inference(resolve,[status(thm)],[c_139,c_26764]) ).
cnf(c_26766,plain,
( ~ aNaturalNumber0(sz10)
| sdtsldt0(xp,xp) = sz10
| ~ doDivides0(xp,xp) ),
inference(resolve,[status(thm)],[c_136,c_26765]) ).
cnf(c_26767,plain,
( ~ aNaturalNumber0(sz10)
| sdtsldt0(xp,xp) = sz10 ),
inference(resolve,[status(thm)],[c_4594,c_26766]) ).
cnf(c_20022,plain,
sdtsldt0(xp,xp) = sz10,
inference(resolve,[status(thm)],[c_204,c_26767]) ).
cnf(c_26768,plain,
( ~ aNaturalNumber0(sz10)
| doDivides0(sK1,sK1)
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_2028,c_284]) ).
cnf(c_26769,plain,
( ~ aNaturalNumber0(sz10)
| doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_119,c_26768]) ).
cnf(c_20074,plain,
doDivides0(sK1,sK1),
inference(resolve,[status(thm)],[c_204,c_26769]) ).
cnf(c_26770,plain,
( ~ aNaturalNumber0(sz10)
| sdtsldt0(sK1,sK1) = sz10
| ~ doDivides0(sK1,sK1)
| sz00 = sK1
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_2028,c_279]) ).
cnf(c_26771,plain,
( ~ aNaturalNumber0(sz10)
| sdtsldt0(sK1,sK1) = sz10
| ~ doDivides0(sK1,sK1)
| sK1 = sz00
| ~ aNaturalNumber0(sK1) ),
inference(copy,[status(thm)],[c_26770]) ).
cnf(c_26772,plain,
( ~ aNaturalNumber0(sz10)
| sdtsldt0(sK1,sK1) = sz10
| ~ doDivides0(sK1,sK1)
| sK1 = sz00 ),
inference(resolve,[status(thm)],[c_119,c_26771]) ).
cnf(c_26773,plain,
( ~ aNaturalNumber0(sz10)
| sdtsldt0(sK1,sK1) = sz10
| ~ doDivides0(sK1,sK1) ),
inference(resolve,[status(thm)],[c_3247,c_26772]) ).
cnf(c_26774,plain,
( ~ aNaturalNumber0(sz10)
| sdtsldt0(sK1,sK1) = sz10 ),
inference(resolve,[status(thm)],[c_20074,c_26773]) ).
cnf(c_20075,plain,
sdtsldt0(sK1,sK1) = sz10,
inference(resolve,[status(thm)],[c_204,c_26774]) ).
cnf(c_26775,plain,
( sdtsldt0(sdtasdt0(sK1,xp),xp) = sdtasdt0(sK1,sdtsldt0(xp,xp))
| sz00 = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_1280,c_4594]) ).
cnf(c_26776,plain,
( sdtsldt0(sdtasdt0(sK1,xp),xp) = sdtasdt0(sK1,sz10)
| sz00 = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xp) ),
inference(paramod,[status(thm)],[c_20022,c_26775]) ).
cnf(c_26777,plain,
( sdtsldt0(sdtasdt0(sK1,xp),xp) = sK1
| sz00 = xp
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xp) ),
inference(paramod,[status(thm)],[c_2028,c_26776]) ).
cnf(c_26778,plain,
( sdtsldt0(sdtasdt0(sK1,xp),xp) = sK1
| xp = sz00
| ~ aNaturalNumber0(xp)
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_26777]) ).
cnf(c_26779,plain,
( sdtsldt0(sdtasdt0(sK1,xp),xp) = sK1
| xp = sz00
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_26778]) ).
cnf(c_26780,plain,
( sdtsldt0(sdtasdt0(sK1,xp),xp) = sK1
| xp = sz00 ),
inference(resolve,[status(thm)],[c_139,c_26779]) ).
cnf(c_20670,plain,
sdtsldt0(sdtasdt0(sK1,xp),xp) = sK1,
inference(resolve,[status(thm)],[c_136,c_26780]) ).
cnf(c_26781,plain,
( sdtasdt0(sK1,xp) != sK1
| sdtsldt0(sK1,sK1) = xp
| sz00 = sK1
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_1446,c_20074]) ).
cnf(c_26782,plain,
( sdtasdt0(sK1,xp) != sK1
| sz10 = xp
| sz00 = sK1
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sK1) ),
inference(paramod,[status(thm)],[c_20075,c_26781]) ).
cnf(c_26783,plain,
( sdtasdt0(sK1,xp) != sK1
| sz10 = xp
| sK1 = sz00
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sK1) ),
inference(copy,[status(thm)],[c_26782]) ).
cnf(c_26784,plain,
( sdtasdt0(sK1,xp) != sK1
| xp = sz10
| sK1 = sz00
| ~ aNaturalNumber0(sK1)
| ~ aNaturalNumber0(sK1) ),
inference(copy,[status(thm)],[c_26783]) ).
cnf(c_26785,plain,
( sdtasdt0(sK1,xp) != sK1
| xp = sz10
| sK1 = sz00
| ~ aNaturalNumber0(sK1) ),
inference(copy,[status(thm)],[c_26784]) ).
cnf(c_26786,plain,
( sdtasdt0(sK1,xp) != sK1
| xp = sz10
| sK1 = sz00 ),
inference(resolve,[status(thm)],[c_119,c_26785]) ).
cnf(c_26787,plain,
( sdtasdt0(sK1,xp) != sK1
| xp = sz10 ),
inference(resolve,[status(thm)],[c_3247,c_26786]) ).
cnf(c_24145,plain,
sdtasdt0(sK1,xp) != sK1,
inference(resolve,[status(thm)],[c_122,c_26787]) ).
cnf(c_25478,plain,
sdtlseqdt0(sK1,sdtasdt0(sK1,xp)),
inference(resolve,[status(thm)],[c_1583,c_119]) ).
cnf(c_26788,plain,
( sK1 = sdtasdt0(sK1,xp)
| ~ sdtlseqdt0(sdtasdt0(sK1,xp),sK1)
| ~ aNaturalNumber0(sdtasdt0(sK1,xp)) ),
inference(resolve,[status(thm)],[c_25478,c_1738]) ).
cnf(c_26789,plain,
( sdtasdt0(sK1,xp) = sK1
| ~ sdtlseqdt0(sdtasdt0(sK1,xp),sK1)
| ~ aNaturalNumber0(sdtasdt0(sK1,xp)) ),
inference(copy,[status(thm)],[c_26788]) ).
cnf(c_25554,plain,
( ~ sdtlseqdt0(sdtasdt0(sK1,xp),sK1)
| ~ aNaturalNumber0(sdtasdt0(sK1,xp)) ),
inference(resolve,[status(thm)],[c_24145,c_26789]) ).
cnf(c_26283,plain,
aNaturalNumber0(sdtasdt0(sK1,xp)),
inference(resolve,[status(thm)],[c_2113,c_139]) ).
cnf(c_26297,plain,
~ sdtlseqdt0(sdtasdt0(sK1,xp),sK1),
inference(resolve,[status(thm)],[c_26283,c_25554]) ).
cnf(c_26790,plain,
( ~ aNaturalNumber0(xp)
| doDivides0(sK1,sdtasdt0(sK1,xp))
| ~ aNaturalNumber0(sK1) ),
inference(resolve,[status(thm)],[c_26283,c_1526]) ).
cnf(c_26791,plain,
( ~ aNaturalNumber0(xp)
| doDivides0(sK1,sdtasdt0(sK1,xp)) ),
inference(resolve,[status(thm)],[c_119,c_26790]) ).
cnf(c_26452,plain,
doDivides0(sK1,sdtasdt0(sK1,xp)),
inference(resolve,[status(thm)],[c_139,c_26791]) ).
cnf(c_26792,plain,
( doDivides0(xp,sdtasdt0(sK1,xp))
| ~ aNaturalNumber0(sdtasdt0(sK1,xp)) ),
inference(resolve,[status(thm)],[c_26452,c_3819]) ).
cnf(c_26582,plain,
doDivides0(xp,sdtasdt0(sK1,xp)),
inference(resolve,[status(thm)],[c_26283,c_26792]) ).
cnf(c_26793,plain,
( sdtasdt0(xp,sdtsldt0(sdtasdt0(sK1,xp),xp)) = sdtasdt0(sK1,xp)
| sz00 = xp
| ~ aNaturalNumber0(sdtasdt0(sK1,xp))
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_26582,c_1492]) ).
cnf(c_26794,plain,
( sdtasdt0(xp,sK1) = sdtasdt0(sK1,xp)
| sz00 = xp
| ~ aNaturalNumber0(sdtasdt0(sK1,xp))
| ~ aNaturalNumber0(xp) ),
inference(paramod,[status(thm)],[c_20670,c_26793]) ).
cnf(c_26795,plain,
( sdtasdt0(xn,xn) = sdtasdt0(sK1,xp)
| sz00 = xp
| ~ aNaturalNumber0(sdtasdt0(sK1,xp))
| ~ aNaturalNumber0(xp) ),
inference(paramod,[status(thm)],[c_118,c_26794]) ).
cnf(c_26796,plain,
( sdtasdt0(xn,xn) = sdtasdt0(sK1,xp)
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(sK1,xp))
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_26795]) ).
cnf(c_26797,plain,
( sdtasdt0(sK1,xp) = sdtasdt0(xn,xn)
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(sK1,xp))
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_26796]) ).
cnf(c_26798,plain,
( sdtasdt0(sK1,xp) = sdtasdt0(xn,xn)
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(sK1,xp)) ),
inference(resolve,[status(thm)],[c_139,c_26797]) ).
cnf(c_26799,plain,
( sdtasdt0(sK1,xp) = sdtasdt0(xn,xn)
| xp = sz00 ),
inference(resolve,[status(thm)],[c_26283,c_26798]) ).
cnf(c_26646,plain,
sdtasdt0(sK1,xp) = sdtasdt0(xn,xn),
inference(resolve,[status(thm)],[c_136,c_26799]) ).
cnf(c_26677,plain,
~ sdtlseqdt0(sdtasdt0(xn,xn),sK1),
inference(paramod,[status(thm)],[c_26646,c_26297]) ).
cnf(c_26690,plain,
~ sdtlseqdt0(xn,xm),
inference(resolve,[status(thm)],[c_26677,c_3373]) ).
cnf(c_26698,plain,
xm != xn,
inference(resolve,[status(thm)],[c_26677,c_3300]) ).
cnf(c_26800,plain,
xm = xn,
inference(resolve,[status(thm)],[c_26690,c_4885]) ).
cnf(c_26701,plain,
$false,
inference(resolve,[status(thm)],[c_26698,c_26800]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM528+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n004.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Sat Sep 26 03:07:23 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 684325 was started by sandbox on n004,
% 0.09/0.36 % Sat Sep 26 03:07:23 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.37
% 0.12/0.37 % From the command line: assign(max_seconds, 300).
% 33.58/5.33
% 33.58/5.33 % given #500 (W,wt=11): 5641 sdtlseqdt0(c1,sz10) | sdtlseqdt0(sz10,c1). [resolve(1703,a,204,a)].
% 33.58/5.33
% 33.58/5.33 % given #1000 (T,wt=14): 6102 aNaturalNumber0(f1(sz10,c1)). [back_unit_del(4033),unit_del(a,6045)].
% 33.58/5.33
% 33.58/5.33 % given #1500 (A,wt=46): 1178 -aNaturalNumber0(A) | sz00 = A | sdtasdt0(A,sdtasdt0(xn,xn)) != sdtasdt0(A,A) | -iLess0(A,xn) | sz10 = A | doDivides0(f5(A,xn,A),A). [factor(1111,a,b),merge(c)].
% 33.58/5.33
% 33.58/5.33 % given #2000 (T,wt=11): 23228 -sdtlseqdt0(c1,xq) | sdtlseqdt0(xn,xq). [resolve(22987,a,113,a)].
% 33.58/5.33
% 33.58/5.33 % given #2500 (A,wt=20): 1544 -aNaturalNumber0(A) | doDivides0(A,A) | sdtasdt0(A,xq) != A. [factor(1522,a,b)].
% 33.58/5.33
% 33.58/5.33 % SZS status Theorem for theBenchmark
% 33.58/5.33
% 33.58/5.33 % Proof 1 at 3.73 (+ 1.18) seconds.
% 33.58/5.33 % Length of proof is 124.
% 33.58/5.33 % Level of proof is 13.
% 33.58/5.33 % Maximum clause weight is 38.000.
% 33.58/5.33 % Given clauses 2871.
% 33.58/5.33
% 33.58/5.33 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------