%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM498+1 : 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 : n011.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:12 AM UTC 2026
% Result : Theorem 147.52s 20.11s
% Output : CNFRefutation 147.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 19
% Syntax : Number of formulae : 225 ( 83 unt; 0 def)
% Number of atoms : 593 ( 304 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 642 ( 274 ~; 307 |; 36 &)
% ( 3 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 123 ( 0 sgn 29 !; 3 ?)
% 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(mMulComm,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> sdtasdt0(W0,W1) = sdtasdt0(W1,W0) ),
file('theBenchmark.p',mMulComm) ).
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(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(mDivMin,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( doDivides0(W0,sdtpldt0(W1,W2))
& doDivides0(W0,W1) )
=> doDivides0(W0,W2) ) ),
file('theBenchmark.p',mDivMin) ).
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__1837,axiom,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('theBenchmark.p',m__1837) ).
fof(m__1860,axiom,
( doDivides0(xp,sdtasdt0(xn,xm))
& isPrime0(xp) ),
file('theBenchmark.p',m__1860) ).
fof(m__2287,axiom,
( sdtlseqdt0(xm,xp)
& xm != xp
& sdtlseqdt0(xn,xp)
& xn != xp ),
file('theBenchmark.p',m__2287) ).
fof(m__,conjecture,
( ( xk = sz10
| xk = sz00 )
=> ( doDivides0(xp,xm)
| doDivides0(xp,xn) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( ( xk = sz10
| xk = sz00 )
=> ( doDivides0(xp,xm)
| doDivides0(xp,xn) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_44,plain,
( B = A
| B = sz10
| ~ doDivides0(B,A)
| ~ aNaturalNumber0(B)
| ~ isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefPrime]) ).
cnf(c_45,plain,
( sz10 != A
| ~ isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefPrime]) ).
cnf(c_46,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_50,plain,
( isPrime0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimDiv]) ).
cnf(c_52,plain,
isPrime0(xp),
inference(clausify,[status(thm)],[m__1860]) ).
cnf(c_53,plain,
( sz00 != xp
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_52,c_46]) ).
cnf(c_54,plain,
( xp != sz00
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_53]) ).
cnf(c_55,plain,
( sz10 != xp
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_52,c_45]) ).
cnf(c_56,plain,
( xp != sz10
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_55]) ).
cnf(c_57,plain,
( A = xp
| A = sz10
| ~ doDivides0(A,xp)
| ~ aNaturalNumber0(A)
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_52,c_44]) ).
cnf(c_4712,plain,
( A = xp
| sz10 = A
| ~ doDivides0(A,xp)
| ~ aNaturalNumber0(A)
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_57]) ).
cnf(c_58,plain,
( xp = A
| sz10 = A
| ~ doDivides0(A,xp)
| ~ aNaturalNumber0(A)
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_4712]) ).
cnf(c_71,plain,
( sz10 != sK0(A)
| ~ aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_50,c_45]) ).
cnf(c_72,plain,
( sK0(A) != sz10
| ~ aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_71]) ).
cnf(c_83,negated_conjecture,
~ doDivides0(xp,xm),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_84,negated_conjecture,
~ doDivides0(xp,xn),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_85,negated_conjecture,
( xk = sz10
| xk = sz00 ),
inference(clausify,[status(thm)],[m___neg]) ).
fof(m__2306,axiom,
xk = sdtsldt0(sdtasdt0(xn,xm),xp),
file('theBenchmark.p',m__2306) ).
cnf(c_86,plain,
xk = sdtsldt0(sdtasdt0(xn,xm),xp),
inference(clausify,[status(thm)],[m__2306]) ).
cnf(c_87,plain,
sdtsldt0(sdtasdt0(xn,xm),xp) = xk,
inference(copy,[status(thm)],[c_86]) ).
cnf(c_89,plain,
xp != xm,
inference(clausify,[status(thm)],[m__2287]) ).
cnf(c_90,plain,
xm != xp,
inference(copy,[status(thm)],[c_89]) ).
cnf(c_92,plain,
xp != xn,
inference(clausify,[status(thm)],[m__2287]) ).
cnf(c_93,plain,
xn != xp,
inference(copy,[status(thm)],[c_92]) ).
cnf(c_96,plain,
doDivides0(xp,sdtasdt0(xn,xm)),
inference(clausify,[status(thm)],[m__1860]) ).
cnf(c_97,plain,
aNaturalNumber0(xp),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_98,plain,
aNaturalNumber0(xm),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_99,plain,
aNaturalNumber0(xn),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_100,plain,
( doDivides0(sK0(A),A)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimDiv]) ).
cnf(c_101,plain,
( aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimDiv]) ).
cnf(c_102,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_105,plain,
( doDivides0(A,C)
| ~ doDivides0(A,sdtpldt0(B,C))
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDivMin]) ).
cnf(c_108,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_109,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_110,plain,
( aNaturalNumber0(C)
| sdtsldt0(B,A) != C
| ~ doDivides0(A,B)
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefQuot]) ).
cnf(c_111,plain,
( sdtasdt0(A,C) != B
| ~ aNaturalNumber0(C)
| doDivides0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefDiv]) ).
cnf(c_142,plain,
( C = B
| sdtasdt0(A,C) != sdtasdt0(A,B)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mMulCanc]) ).
cnf(c_148,plain,
( sdtasdt0(A,sz00) = sz00
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_MulZero]) ).
cnf(c_149,plain,
( sdtasdt0(sz10,A) = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_MulUnit]) ).
cnf(c_150,plain,
( sdtasdt0(A,sz10) = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_MulUnit]) ).
cnf(c_152,plain,
( sdtasdt0(B,A) = sdtasdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mMulComm]) ).
cnf(c_154,plain,
( sdtpldt0(A,sz00) = A
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m_AddZero]) ).
cnf(c_157,plain,
( aNaturalNumber0(sdtasdt0(A,B))
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mSortsB_02]) ).
cnf(c_160,plain,
aNaturalNumber0(sz10),
inference(clausify,[status(thm)],[mSortsC_01]) ).
fof(mSortsC,axiom,
aNaturalNumber0(sz00),
file('theBenchmark.p',mSortsC) ).
cnf(c_161,plain,
aNaturalNumber0(sz00),
inference(clausify,[status(thm)],[mSortsC]) ).
cnf(c_186,plain,
( xp = A
| sz10 = A
| ~ doDivides0(A,xp)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_97,c_58]) ).
cnf(c_187,plain,
xp != sz10,
inference(resolve,[status(thm)],[c_97,c_56]) ).
cnf(c_188,plain,
xp != sz00,
inference(resolve,[status(thm)],[c_97,c_54]) ).
cnf(c_189,plain,
( sdtsldt0(sdtasdt0(B,A),A) = sdtasdt0(B,sdtsldt0(A,A))
| ~ aNaturalNumber0(B)
| ~ doDivides0(A,A)
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_102]) ).
cnf(c_200,plain,
( sdtasdt0(A,B) != B
| sdtsldt0(B,A) = B
| ~ doDivides0(A,B)
| sz00 = A
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_108]) ).
cnf(c_201,plain,
( sdtasdt0(A,B) = A
| sdtsldt0(A,A) != B
| ~ doDivides0(A,A)
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_109]) ).
cnf(c_4713,plain,
( sK0(xp) != sz10
| ~ aNaturalNumber0(sK0(xp))
| sz10 = xp
| sz00 = xp ),
inference(resolve,[status(thm)],[c_97,c_72]) ).
cnf(c_4714,plain,
( sK0(xp) != sz10
| ~ aNaturalNumber0(sK0(xp))
| sz10 = xp
| xp = sz00 ),
inference(copy,[status(thm)],[c_4713]) ).
cnf(c_4715,plain,
( sK0(xp) != sz10
| ~ aNaturalNumber0(sK0(xp))
| xp = sz10
| xp = sz00 ),
inference(copy,[status(thm)],[c_4714]) ).
cnf(c_4716,plain,
( sK0(xp) != sz10
| ~ aNaturalNumber0(sK0(xp))
| xp = sz10 ),
inference(resolve,[status(thm)],[c_188,c_4715]) ).
cnf(c_293,plain,
( sK0(xp) != sz10
| ~ aNaturalNumber0(sK0(xp)) ),
inference(resolve,[status(thm)],[c_187,c_4716]) ).
cnf(c_4717,plain,
( doDivides0(sK0(xp),xp)
| sz10 = xp
| sz00 = xp ),
inference(resolve,[status(thm)],[c_100,c_97]) ).
cnf(c_4718,plain,
( doDivides0(sK0(xp),xp)
| sz10 = xp
| xp = sz00 ),
inference(copy,[status(thm)],[c_4717]) ).
cnf(c_4719,plain,
( doDivides0(sK0(xp),xp)
| xp = sz10
| xp = sz00 ),
inference(copy,[status(thm)],[c_4718]) ).
cnf(c_4720,plain,
( doDivides0(sK0(xp),xp)
| xp = sz10 ),
inference(resolve,[status(thm)],[c_188,c_4719]) ).
cnf(c_443,plain,
doDivides0(sK0(xp),xp),
inference(resolve,[status(thm)],[c_187,c_4720]) ).
cnf(c_4721,plain,
( aNaturalNumber0(sK0(xp))
| sz10 = xp
| sz00 = xp ),
inference(resolve,[status(thm)],[c_101,c_97]) ).
cnf(c_4722,plain,
( aNaturalNumber0(sK0(xp))
| sz10 = xp
| xp = sz00 ),
inference(copy,[status(thm)],[c_4721]) ).
cnf(c_4723,plain,
( aNaturalNumber0(sK0(xp))
| xp = sz10
| xp = sz00 ),
inference(copy,[status(thm)],[c_4722]) ).
cnf(c_4724,plain,
( aNaturalNumber0(sK0(xp))
| xp = sz10 ),
inference(resolve,[status(thm)],[c_188,c_4723]) ).
cnf(c_446,plain,
aNaturalNumber0(sK0(xp)),
inference(resolve,[status(thm)],[c_187,c_4724]) ).
cnf(c_453,plain,
sK0(xp) != sz10,
inference(resolve,[status(thm)],[c_446,c_293]) ).
cnf(c_487,plain,
( doDivides0(A,B)
| ~ doDivides0(A,sdtpldt0(xp,B))
| ~ doDivides0(A,xp)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_105,c_97]) ).
cnf(c_4725,plain,
( sdtasdt0(xp,xk) = sdtasdt0(xn,xm)
| ~ doDivides0(xp,sdtasdt0(xn,xm))
| sz00 = xp
| ~ aNaturalNumber0(sdtasdt0(xn,xm))
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_109,c_87]) ).
cnf(c_4726,plain,
( sdtasdt0(xp,xk) = sdtasdt0(xn,xm)
| ~ doDivides0(xp,sdtasdt0(xn,xm))
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xm))
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_4725]) ).
cnf(c_4727,plain,
( sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
| ~ doDivides0(xp,sdtasdt0(xn,xm))
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xm))
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_4726]) ).
cnf(c_4728,plain,
( sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
| ~ doDivides0(xp,sdtasdt0(xn,xm))
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(resolve,[status(thm)],[c_97,c_4727]) ).
cnf(c_4729,plain,
( sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
| ~ doDivides0(xp,sdtasdt0(xn,xm))
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(resolve,[status(thm)],[c_188,c_4728]) ).
cnf(c_569,plain,
( sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(resolve,[status(thm)],[c_96,c_4729]) ).
cnf(c_4730,plain,
( aNaturalNumber0(xk)
| ~ doDivides0(xp,sdtasdt0(xn,xm))
| sz00 = xp
| ~ aNaturalNumber0(sdtasdt0(xn,xm))
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_110,c_87]) ).
cnf(c_4731,plain,
( aNaturalNumber0(xk)
| ~ doDivides0(xp,sdtasdt0(xn,xm))
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xm))
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_4730]) ).
cnf(c_4732,plain,
( aNaturalNumber0(xk)
| ~ doDivides0(xp,sdtasdt0(xn,xm))
| xp = sz00
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(resolve,[status(thm)],[c_97,c_4731]) ).
cnf(c_4733,plain,
( aNaturalNumber0(xk)
| ~ doDivides0(xp,sdtasdt0(xn,xm))
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(resolve,[status(thm)],[c_188,c_4732]) ).
cnf(c_579,plain,
( aNaturalNumber0(xk)
| ~ aNaturalNumber0(sdtasdt0(xn,xm)) ),
inference(resolve,[status(thm)],[c_96,c_4733]) ).
cnf(c_1026,plain,
sdtasdt0(xn,sz00) = sz00,
inference(resolve,[status(thm)],[c_148,c_99]) ).
cnf(c_1028,plain,
sdtasdt0(xp,sz00) = sz00,
inference(resolve,[status(thm)],[c_148,c_97]) ).
cnf(c_1031,plain,
sdtasdt0(sz10,xp) = xp,
inference(resolve,[status(thm)],[c_149,c_97]) ).
cnf(c_1034,plain,
sdtasdt0(xp,sz10) = xp,
inference(resolve,[status(thm)],[c_150,c_97]) ).
cnf(c_4734,plain,
( sdtasdt0(A,xn) = sdtasdt0(xn,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_152,c_99]) ).
cnf(c_4735,plain,
sdtasdt0(xm,xn) = sdtasdt0(xn,xm),
inference(resolve,[status(thm)],[c_4734,c_98]) ).
cnf(c_1083,plain,
sdtasdt0(xn,xm) = sdtasdt0(xm,xn),
inference(copy,[status(thm)],[c_4735]) ).
cnf(c_4736,plain,
( sdtasdt0(A,xm) = sdtasdt0(xm,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_152,c_98]) ).
cnf(c_4737,plain,
sdtasdt0(xp,xm) = sdtasdt0(xm,xp),
inference(resolve,[status(thm)],[c_4736,c_97]) ).
cnf(c_1085,plain,
sdtasdt0(xm,xp) = sdtasdt0(xp,xm),
inference(copy,[status(thm)],[c_4737]) ).
cnf(c_1106,plain,
( aNaturalNumber0(xk)
| ~ aNaturalNumber0(sdtasdt0(xm,xn)) ),
inference(paramod,[status(thm)],[c_1083,c_579]) ).
cnf(c_4738,plain,
( sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
| ~ aNaturalNumber0(sdtasdt0(xm,xn)) ),
inference(paramod,[status(thm)],[c_1083,c_569]) ).
cnf(c_1108,plain,
( sdtasdt0(xm,xn) = sdtasdt0(xp,xk)
| ~ aNaturalNumber0(sdtasdt0(xm,xn)) ),
inference(paramod,[status(thm)],[c_1083,c_4738]) ).
cnf(c_1127,plain,
sdtsldt0(sdtasdt0(xm,xn),xp) = xk,
inference(paramod,[status(thm)],[c_1083,c_87]) ).
cnf(c_1163,plain,
sdtpldt0(xp,sz00) = xp,
inference(resolve,[status(thm)],[c_154,c_97]) ).
cnf(c_4739,plain,
( aNaturalNumber0(sdtasdt0(xn,A))
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_157,c_99]) ).
cnf(c_4740,plain,
aNaturalNumber0(sdtasdt0(xn,xm)),
inference(resolve,[status(thm)],[c_4739,c_98]) ).
cnf(c_1547,plain,
aNaturalNumber0(sdtasdt0(xm,xn)),
inference(paramod,[status(thm)],[c_1083,c_4740]) ).
cnf(c_1569,plain,
sdtasdt0(xm,xn) = sdtasdt0(xp,xk),
inference(resolve,[status(thm)],[c_1547,c_1108]) ).
cnf(c_1571,plain,
( aNaturalNumber0(xk)
| ~ aNaturalNumber0(sdtasdt0(xp,xk)) ),
inference(paramod,[status(thm)],[c_1569,c_1106]) ).
cnf(c_1591,plain,
aNaturalNumber0(sdtasdt0(xp,xk)),
inference(paramod,[status(thm)],[c_1569,c_1547]) ).
cnf(c_1600,plain,
sdtsldt0(sdtasdt0(xp,xk),xp) = xk,
inference(paramod,[status(thm)],[c_1569,c_1127]) ).
cnf(c_1614,plain,
sdtasdt0(xn,xm) = sdtasdt0(xp,xk),
inference(paramod,[status(thm)],[c_1569,c_1083]) ).
cnf(c_1627,plain,
aNaturalNumber0(xk),
inference(resolve,[status(thm)],[c_1591,c_1571]) ).
cnf(c_4741,plain,
( sdtasdt0(xp,B) != A
| ~ aNaturalNumber0(B)
| doDivides0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_111,c_97]) ).
cnf(c_4742,plain,
( sdtasdt0(xp,A) != xn
| ~ aNaturalNumber0(A)
| doDivides0(xp,xn) ),
inference(resolve,[status(thm)],[c_4741,c_99]) ).
cnf(c_4743,negated_conjecture,
( sdtasdt0(xp,A) != xn
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4742,c_84]) ).
cnf(c_4744,negated_conjecture,
sdtasdt0(xp,sz00) != xn,
inference(resolve,[status(thm)],[c_4743,c_161]) ).
cnf(c_4745,negated_conjecture,
sz00 != xn,
inference(paramod,[status(thm)],[c_1028,c_4744]) ).
cnf(c_2100,negated_conjecture,
xn != sz00,
inference(copy,[status(thm)],[c_4745]) ).
cnf(c_4746,plain,
( sdtasdt0(xp,B) != A
| ~ aNaturalNumber0(B)
| doDivides0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_111,c_97]) ).
cnf(c_4747,plain,
( sdtasdt0(xp,A) != xm
| ~ aNaturalNumber0(A)
| doDivides0(xp,xm) ),
inference(resolve,[status(thm)],[c_4746,c_98]) ).
cnf(c_4748,negated_conjecture,
( sdtasdt0(xp,A) != xm
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4747,c_83]) ).
cnf(c_4749,negated_conjecture,
sdtasdt0(xp,sz00) != xm,
inference(resolve,[status(thm)],[c_4748,c_161]) ).
cnf(c_4750,negated_conjecture,
sz00 != xm,
inference(paramod,[status(thm)],[c_1028,c_4749]) ).
cnf(c_2101,negated_conjecture,
xm != sz00,
inference(copy,[status(thm)],[c_4750]) ).
cnf(c_4751,plain,
( xp = xm
| sz10 = xm
| ~ doDivides0(xm,xp) ),
inference(resolve,[status(thm)],[c_186,c_98]) ).
cnf(c_4752,plain,
( xp = xm
| xm = sz10
| ~ doDivides0(xm,xp) ),
inference(copy,[status(thm)],[c_4751]) ).
cnf(c_4753,plain,
( xm = xp
| xm = sz10
| ~ doDivides0(xm,xp) ),
inference(copy,[status(thm)],[c_4752]) ).
cnf(c_2256,plain,
( xm = sz10
| ~ doDivides0(xm,xp) ),
inference(resolve,[status(thm)],[c_90,c_4753]) ).
cnf(c_4754,plain,
( B = A
| sdtasdt0(xn,B) != sdtasdt0(xn,A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A)
| sz00 = xn ),
inference(resolve,[status(thm)],[c_142,c_99]) ).
cnf(c_4755,plain,
sz00 != xn,
inference(copy,[status(thm)],[c_2100]) ).
cnf(c_4756,plain,
( B = A
| sdtasdt0(xn,B) != sdtasdt0(xn,A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4754,c_4755]) ).
cnf(c_4757,plain,
( A = sz00
| sdtasdt0(xn,A) != sdtasdt0(xn,sz00)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4756,c_161]) ).
cnf(c_4758,plain,
( xm = sz00
| sdtasdt0(xn,xm) != sdtasdt0(xn,sz00) ),
inference(resolve,[status(thm)],[c_4757,c_98]) ).
cnf(c_4759,plain,
sdtasdt0(xn,xm) != sdtasdt0(xn,sz00),
inference(resolve,[status(thm)],[c_4758,c_2101]) ).
cnf(c_4760,plain,
sdtasdt0(xp,xk) != sdtasdt0(xn,sz00),
inference(paramod,[status(thm)],[c_1614,c_4759]) ).
cnf(c_2562,plain,
sdtasdt0(xp,xk) != sz00,
inference(paramod,[status(thm)],[c_1026,c_4760]) ).
cnf(c_4761,plain,
( B = A
| sdtasdt0(xm,B) != sdtasdt0(xm,A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A)
| sz00 = xm ),
inference(resolve,[status(thm)],[c_142,c_98]) ).
cnf(c_4762,plain,
sz00 != xm,
inference(copy,[status(thm)],[c_2101]) ).
cnf(c_4763,plain,
( B = A
| sdtasdt0(xm,B) != sdtasdt0(xm,A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4761,c_4762]) ).
cnf(c_4764,plain,
( A = xn
| sdtasdt0(xm,A) != sdtasdt0(xm,xn)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4763,c_99]) ).
cnf(c_4765,plain,
( xp = xn
| sdtasdt0(xm,xp) != sdtasdt0(xm,xn) ),
inference(resolve,[status(thm)],[c_4764,c_97]) ).
cnf(c_4766,plain,
xp != xn,
inference(copy,[status(thm)],[c_93]) ).
cnf(c_4767,plain,
sdtasdt0(xm,xp) != sdtasdt0(xm,xn),
inference(resolve,[status(thm)],[c_4765,c_4766]) ).
cnf(c_4768,plain,
sdtasdt0(xp,xm) != sdtasdt0(xm,xn),
inference(paramod,[status(thm)],[c_1085,c_4767]) ).
cnf(c_4769,plain,
sdtasdt0(xp,xm) != sdtasdt0(xp,xk),
inference(paramod,[status(thm)],[c_1569,c_4768]) ).
cnf(c_2565,plain,
sdtasdt0(xp,xk) != sdtasdt0(xp,xm),
inference(copy,[status(thm)],[c_4769]) ).
cnf(c_4770,plain,
( sdtasdt0(A,xp) = sdtasdt0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_152,c_97]) ).
cnf(c_2960,plain,
sdtasdt0(xk,xp) = sdtasdt0(xp,xk),
inference(resolve,[status(thm)],[c_4770,c_1627]) ).
cnf(c_4771,plain,
( xp = sK0(xp)
| sz10 = sK0(xp)
| ~ aNaturalNumber0(sK0(xp)) ),
inference(resolve,[status(thm)],[c_443,c_186]) ).
cnf(c_4772,plain,
( xp = sK0(xp)
| sK0(xp) = sz10
| ~ aNaturalNumber0(sK0(xp)) ),
inference(copy,[status(thm)],[c_4771]) ).
cnf(c_4773,plain,
( sK0(xp) = xp
| sK0(xp) = sz10
| ~ aNaturalNumber0(sK0(xp)) ),
inference(copy,[status(thm)],[c_4772]) ).
cnf(c_4774,plain,
( sK0(xp) = xp
| sK0(xp) = sz10 ),
inference(resolve,[status(thm)],[c_446,c_4773]) ).
cnf(c_3522,plain,
sK0(xp) = xp,
inference(resolve,[status(thm)],[c_453,c_4774]) ).
cnf(c_3535,plain,
doDivides0(xp,xp),
inference(paramod,[status(thm)],[c_3522,c_443]) ).
cnf(c_4775,plain,
( sdtsldt0(sdtasdt0(A,xp),xp) = sdtasdt0(A,sdtsldt0(xp,xp))
| ~ aNaturalNumber0(A)
| ~ doDivides0(xp,xp)
| sz00 = xp ),
inference(resolve,[status(thm)],[c_189,c_97]) ).
cnf(c_4776,plain,
( sdtsldt0(sdtasdt0(A,xp),xp) = sdtasdt0(A,sdtsldt0(xp,xp))
| ~ aNaturalNumber0(A)
| sz00 = xp ),
inference(resolve,[status(thm)],[c_4775,c_3535]) ).
cnf(c_4777,plain,
( sdtsldt0(sdtasdt0(xk,xp),xp) = sdtasdt0(xk,sdtsldt0(xp,xp))
| sz00 = xp ),
inference(resolve,[status(thm)],[c_4776,c_1627]) ).
cnf(c_4778,plain,
( sdtsldt0(sdtasdt0(xp,xk),xp) = sdtasdt0(xk,sdtsldt0(xp,xp))
| sz00 = xp ),
inference(paramod,[status(thm)],[c_2960,c_4777]) ).
cnf(c_4779,plain,
( xk = sdtasdt0(xk,sdtsldt0(xp,xp))
| sz00 = xp ),
inference(paramod,[status(thm)],[c_1600,c_4778]) ).
cnf(c_4780,plain,
( xk = sdtasdt0(xk,sdtsldt0(xp,xp))
| xp = sz00 ),
inference(copy,[status(thm)],[c_4779]) ).
cnf(c_4781,plain,
( sdtasdt0(xk,sdtsldt0(xp,xp)) = xk
| xp = sz00 ),
inference(copy,[status(thm)],[c_4780]) ).
cnf(c_3540,plain,
sdtasdt0(xk,sdtsldt0(xp,xp)) = xk,
inference(resolve,[status(thm)],[c_188,c_4781]) ).
cnf(c_4782,plain,
( sdtsldt0(sdtasdt0(A,xp),xp) = sdtasdt0(A,sdtsldt0(xp,xp))
| ~ aNaturalNumber0(A)
| ~ doDivides0(xp,xp)
| sz00 = xp ),
inference(resolve,[status(thm)],[c_189,c_97]) ).
cnf(c_4783,plain,
( sdtsldt0(sdtasdt0(A,xp),xp) = sdtasdt0(A,sdtsldt0(xp,xp))
| ~ aNaturalNumber0(A)
| sz00 = xp ),
inference(resolve,[status(thm)],[c_4782,c_3535]) ).
cnf(c_4784,plain,
( sdtsldt0(sdtasdt0(sz10,xp),xp) = sdtasdt0(sz10,sdtsldt0(xp,xp))
| sz00 = xp ),
inference(resolve,[status(thm)],[c_4783,c_160]) ).
cnf(c_4785,plain,
( sdtsldt0(xp,xp) = sdtasdt0(sz10,sdtsldt0(xp,xp))
| sz00 = xp ),
inference(paramod,[status(thm)],[c_1031,c_4784]) ).
cnf(c_4786,plain,
( sdtsldt0(xp,xp) = sdtasdt0(sz10,sdtsldt0(xp,xp))
| xp = sz00 ),
inference(copy,[status(thm)],[c_4785]) ).
cnf(c_4787,plain,
( sdtasdt0(sz10,sdtsldt0(xp,xp)) = sdtsldt0(xp,xp)
| xp = sz00 ),
inference(copy,[status(thm)],[c_4786]) ).
cnf(c_3542,plain,
sdtasdt0(sz10,sdtsldt0(xp,xp)) = sdtsldt0(xp,xp),
inference(resolve,[status(thm)],[c_188,c_4787]) ).
cnf(c_4788,plain,
( doDivides0(A,sz00)
| ~ doDivides0(A,sdtpldt0(xp,sz00))
| ~ doDivides0(A,xp)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_487,c_161]) ).
cnf(c_4789,plain,
( doDivides0(A,sz00)
| ~ doDivides0(A,xp)
| ~ doDivides0(A,xp)
| ~ aNaturalNumber0(A) ),
inference(paramod,[status(thm)],[c_1163,c_4788]) ).
cnf(c_4147,plain,
( doDivides0(A,sz00)
| ~ doDivides0(A,xp)
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_4789]) ).
cnf(c_4790,plain,
( doDivides0(xp,sz00)
| ~ doDivides0(xp,xp) ),
inference(resolve,[status(thm)],[c_4147,c_97]) ).
cnf(c_4340,plain,
doDivides0(xp,sz00),
inference(resolve,[status(thm)],[c_3535,c_4790]) ).
cnf(c_4791,plain,
( sdtasdt0(xp,sz00) != sz00
| sdtsldt0(sz00,xp) = sz00
| sz00 = xp
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_4340,c_200]) ).
cnf(c_4792,plain,
( sz00 != sz00
| sdtsldt0(sz00,xp) = sz00
| sz00 = xp
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(xp) ),
inference(paramod,[status(thm)],[c_1028,c_4791]) ).
cnf(c_4793,plain,
( sz00 != sz00
| sdtsldt0(sz00,xp) = sz00
| xp = sz00
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_4792]) ).
cnf(c_4794,plain,
( sdtsldt0(sz00,xp) = sz00
| xp = sz00
| ~ aNaturalNumber0(sz00)
| ~ aNaturalNumber0(xp) ),
inference(copy,[status(thm)],[c_4793]) ).
cnf(c_4795,plain,
( sdtsldt0(sz00,xp) = sz00
| xp = sz00
| ~ aNaturalNumber0(sz00) ),
inference(resolve,[status(thm)],[c_97,c_4794]) ).
cnf(c_4796,plain,
( sdtsldt0(sz00,xp) = sz00
| xp = sz00 ),
inference(resolve,[status(thm)],[c_161,c_4795]) ).
cnf(c_4349,plain,
sdtsldt0(sz00,xp) = sz00,
inference(resolve,[status(thm)],[c_188,c_4796]) ).
cnf(c_4797,plain,
( sdtasdt0(xp,B) = A
| sdtsldt0(A,xp) != B
| ~ doDivides0(xp,A)
| sz00 = xp
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_109,c_97]) ).
cnf(c_4798,plain,
( sdtasdt0(xp,A) = sz00
| sdtsldt0(sz00,xp) != A
| ~ doDivides0(xp,sz00)
| sz00 = xp ),
inference(resolve,[status(thm)],[c_4797,c_161]) ).
cnf(c_4799,plain,
sz00 != xp,
inference(copy,[status(thm)],[c_188]) ).
cnf(c_4800,plain,
( sdtasdt0(xp,A) = sz00
| sdtsldt0(sz00,xp) != A
| ~ doDivides0(xp,sz00) ),
inference(resolve,[status(thm)],[c_4798,c_4799]) ).
cnf(c_4801,plain,
( sdtasdt0(xp,A) = sz00
| sdtsldt0(sz00,xp) != A ),
inference(resolve,[status(thm)],[c_4800,c_4340]) ).
cnf(c_4802,plain,
sdtsldt0(sz00,xp) != xk,
inference(resolve,[status(thm)],[c_4801,c_2562]) ).
cnf(c_4803,plain,
sz00 != xk,
inference(paramod,[status(thm)],[c_4349,c_4802]) ).
cnf(c_4355,plain,
xk != sz00,
inference(copy,[status(thm)],[c_4803]) ).
cnf(c_4566,negated_conjecture,
xk = sz10,
inference(resolve,[status(thm)],[c_4355,c_85]) ).
cnf(c_4804,plain,
sdtasdt0(sz10,sdtsldt0(xp,xp)) = xk,
inference(paramod,[status(thm)],[c_4566,c_3540]) ).
cnf(c_4805,plain,
sdtsldt0(xp,xp) = xk,
inference(paramod,[status(thm)],[c_3542,c_4804]) ).
cnf(c_4575,plain,
sdtsldt0(xp,xp) = sz10,
inference(paramod,[status(thm)],[c_4566,c_4805]) ).
cnf(c_4806,plain,
sdtasdt0(xp,sz10) != sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_4566,c_2565]) ).
cnf(c_4807,plain,
xp != sdtasdt0(xp,xm),
inference(paramod,[status(thm)],[c_1034,c_4806]) ).
cnf(c_4581,plain,
sdtasdt0(xp,xm) != xp,
inference(copy,[status(thm)],[c_4807]) ).
cnf(c_4808,plain,
sdtasdt0(xm,xn) = sdtasdt0(xp,sz10),
inference(paramod,[status(thm)],[c_4566,c_1569]) ).
cnf(c_4609,plain,
sdtasdt0(xm,xn) = xp,
inference(paramod,[status(thm)],[c_1034,c_4808]) ).
cnf(c_4809,plain,
( sdtasdt0(xp,A) = xp
| sdtsldt0(xp,xp) != A
| ~ doDivides0(xp,xp)
| sz00 = xp ),
inference(resolve,[status(thm)],[c_201,c_97]) ).
cnf(c_4810,plain,
sz00 != xp,
inference(copy,[status(thm)],[c_188]) ).
cnf(c_4811,plain,
( sdtasdt0(xp,A) = xp
| sdtsldt0(xp,xp) != A
| ~ doDivides0(xp,xp) ),
inference(resolve,[status(thm)],[c_4809,c_4810]) ).
cnf(c_4812,plain,
( sdtasdt0(xp,A) = xp
| sdtsldt0(xp,xp) != A ),
inference(resolve,[status(thm)],[c_4811,c_3535]) ).
cnf(c_4813,plain,
sdtsldt0(xp,xp) != xm,
inference(resolve,[status(thm)],[c_4812,c_4581]) ).
cnf(c_4814,plain,
sz10 != xm,
inference(paramod,[status(thm)],[c_4575,c_4813]) ).
cnf(c_4629,plain,
xm != sz10,
inference(copy,[status(thm)],[c_4814]) ).
cnf(c_4651,plain,
~ doDivides0(xm,xp),
inference(resolve,[status(thm)],[c_4629,c_2256]) ).
cnf(c_4815,plain,
( sdtasdt0(xm,B) != A
| ~ aNaturalNumber0(B)
| doDivides0(xm,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_111,c_98]) ).
cnf(c_4816,plain,
( sdtasdt0(xm,A) != xp
| ~ aNaturalNumber0(A)
| doDivides0(xm,xp) ),
inference(resolve,[status(thm)],[c_4815,c_97]) ).
cnf(c_4817,plain,
( sdtasdt0(xm,A) != xp
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_4816,c_4651]) ).
cnf(c_4818,plain,
sdtasdt0(xm,xn) != xp,
inference(resolve,[status(thm)],[c_4817,c_99]) ).
cnf(c_4819,plain,
xp != xp,
inference(paramod,[status(thm)],[c_4609,c_4818]) ).
cnf(c_4711,plain,
$false,
inference(copy,[status(thm)],[c_4819]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NUM498+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n011.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Sat Sep 26 03:00:15 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.43 % Process 3648536 was started by sandbox on n011,
% 0.15/0.43 % Sat Sep 26 03:00:15 2026
% 0.15/0.43 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/0.44
% 0.15/0.44 % From the command line: assign(max_seconds, 300).
% 147.52/20.11
% 147.52/20.11 % given #500 (T,wt=13): 3137 -aNaturalNumber0(A) | -sdtlseqdt0(xp,A) | sdtlseqdt0(sz10,A). [resolve(647,a,127,d),unit_del(a,160),unit_del(b,97)].
% 147.52/20.11
% 147.52/20.11 % SZS status Theorem for theBenchmark
% 147.52/20.11
% 147.52/20.11 % Proof 1 at 3.22 (+ 0.36) seconds.
% 147.52/20.11 % Length of proof is 111.
% 147.52/20.11 % Level of proof is 16.
% 147.52/20.11 % Maximum clause weight is 38.000.
% 147.52/20.11 % Given clauses 562.
% 147.52/20.11
% 147.52/20.11 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------