%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM496+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 : n003.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:11 AM UTC 2026
% Result : Theorem 20.49s 3.41s
% Output : CNFRefutation 20.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 8
% Syntax : Number of formulae : 68 ( 21 unt; 0 def)
% Number of atoms : 219 ( 97 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 224 ( 73 ~; 108 |; 36 &)
% ( 1 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 37 ( 0 sgn 12 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mDivSum,axiom,
! [W0,W1,W2] :
( ( aNaturalNumber0(W2)
& aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( doDivides0(W0,W2)
& doDivides0(W0,W1) )
=> doDivides0(W0,sdtpldt0(W1,W2)) ) ),
file('theBenchmark.p',mDivSum) ).
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))
& ? [W0] :
( sdtasdt0(xn,xm) = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
& isPrime0(xp)
& ! [W0] :
( ( ( doDivides0(W0,xp)
| ? [W1] :
( xp = sdtasdt0(W0,W1)
& aNaturalNumber0(W1) ) )
& aNaturalNumber0(W0) )
=> ( W0 = xp
| W0 = sz10 ) )
& xp != sz10
& xp != sz00 ),
file('theBenchmark.p',m__1860) ).
fof(m__1883,axiom,
( xr = sdtmndt0(xn,xp)
& sdtpldt0(xp,xr) = xn
& aNaturalNumber0(xr) ),
file('theBenchmark.p',m__1883) ).
fof(m__2027,axiom,
( ( doDivides0(xp,xm)
& ? [W0] :
( xm = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) )
| ( doDivides0(xp,xr)
& ? [W0] :
( xr = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ) ),
file('theBenchmark.p',m__2027) ).
fof(m__,conjecture,
( doDivides0(xp,xm)
| ? [W0] :
( xm = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
| doDivides0(xp,xn)
| ? [W0] :
( xn = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( doDivides0(xp,xm)
| ? [W0] :
( xm = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) )
| doDivides0(xp,xn)
| ? [W0] :
( xn = sdtasdt0(xp,W0)
& aNaturalNumber0(W0) ) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_49,plain,
( sz10 != A
| ~ isPrime0(A)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDefPrime]) ).
cnf(c_50,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_54,plain,
( isPrime0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimDiv]) ).
cnf(c_258,plain,
( sz00 != sK0(A)
| ~ aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_54,c_50]) ).
cnf(c_259,plain,
( sK0(A) != sz00
| ~ aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_258]) ).
cnf(c_260,plain,
( sz10 != sK0(A)
| ~ aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_54,c_49]) ).
cnf(c_261,plain,
( sK0(A) != sz10
| ~ aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(copy,[status(thm)],[c_260]) ).
cnf(c_272,negated_conjecture,
~ doDivides0(xp,xm),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_274,negated_conjecture,
~ doDivides0(xp,xn),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_276,plain,
( doDivides0(xp,xm)
| doDivides0(xp,xr) ),
inference(clausify,[status(thm)],[m__2027]) ).
cnf(c_277,negated_conjecture,
doDivides0(xp,xr),
inference(resolve,[status(thm)],[c_272,c_276]) ).
cnf(c_292,plain,
sdtpldt0(xp,xr) = xn,
inference(clausify,[status(thm)],[m__1883]) ).
cnf(c_293,plain,
aNaturalNumber0(xr),
inference(clausify,[status(thm)],[m__1883]) ).
cnf(c_301,plain,
( xp = A
| sz10 = A
| ~ doDivides0(A,xp)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[m__1860]) ).
cnf(c_303,plain,
xp != sz10,
inference(clausify,[status(thm)],[m__1860]) ).
cnf(c_304,plain,
sz10 != xp,
inference(copy,[status(thm)],[c_303]) ).
cnf(c_305,plain,
xp != sz00,
inference(clausify,[status(thm)],[m__1860]) ).
cnf(c_306,plain,
sz00 != xp,
inference(copy,[status(thm)],[c_305]) ).
cnf(c_523,plain,
aNaturalNumber0(xp),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_526,plain,
( doDivides0(sK0(A),A)
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimDiv]) ).
cnf(c_527,plain,
( aNaturalNumber0(sK0(A))
| sz10 = A
| sz00 = A
| ~ aNaturalNumber0(A) ),
inference(split_conjunct,[status(thm)],[sk_mPrimDiv]) ).
cnf(c_532,plain,
( doDivides0(A,sdtpldt0(B,C))
| ~ doDivides0(A,C)
| ~ doDivides0(A,B)
| ~ aNaturalNumber0(C)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mDivSum]) ).
cnf(c_1537,plain,
( doDivides0(A,sdtpldt0(A,B))
| ~ doDivides0(A,B)
| ~ doDivides0(A,A)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(factor,[status(thm)],[c_532]) ).
cnf(c_7188,plain,
( doDivides0(sK0(xp),xp)
| sz10 = xp
| sz00 = xp ),
inference(resolve,[status(thm)],[c_526,c_523]) ).
cnf(c_7189,plain,
( doDivides0(sK0(xp),xp)
| sz10 = xp ),
inference(resolve,[status(thm)],[c_306,c_7188]) ).
cnf(c_3532,plain,
doDivides0(sK0(xp),xp),
inference(resolve,[status(thm)],[c_304,c_7189]) ).
cnf(c_7190,plain,
( aNaturalNumber0(sK0(xp))
| sz10 = xp
| sz00 = xp ),
inference(resolve,[status(thm)],[c_527,c_523]) ).
cnf(c_7191,plain,
( aNaturalNumber0(sK0(xp))
| sz10 = xp ),
inference(resolve,[status(thm)],[c_306,c_7190]) ).
cnf(c_3541,plain,
aNaturalNumber0(sK0(xp)),
inference(resolve,[status(thm)],[c_304,c_7191]) ).
cnf(c_7192,plain,
( doDivides0(xp,sdtpldt0(xp,xr))
| ~ doDivides0(xp,xp)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_1537,c_277]) ).
cnf(c_7193,plain,
( doDivides0(xp,xn)
| ~ doDivides0(xp,xp)
| ~ aNaturalNumber0(xr)
| ~ aNaturalNumber0(xp) ),
inference(paramod,[status(thm)],[c_292,c_7192]) ).
cnf(c_7194,plain,
( doDivides0(xp,xn)
| ~ doDivides0(xp,xp)
| ~ aNaturalNumber0(xr) ),
inference(resolve,[status(thm)],[c_523,c_7193]) ).
cnf(c_7195,plain,
( doDivides0(xp,xn)
| ~ doDivides0(xp,xp) ),
inference(resolve,[status(thm)],[c_293,c_7194]) ).
cnf(c_5769,negated_conjecture,
~ doDivides0(xp,xp),
inference(resolve,[status(thm)],[c_274,c_7195]) ).
cnf(c_7196,plain,
( doDivides0(sK0(sK0(xp)),sK0(xp))
| sz10 = sK0(xp)
| sz00 = sK0(xp) ),
inference(resolve,[status(thm)],[c_3541,c_526]) ).
cnf(c_7197,plain,
( doDivides0(sK0(sK0(xp)),sK0(xp))
| sz10 = sK0(xp)
| sK0(xp) = sz00 ),
inference(copy,[status(thm)],[c_7196]) ).
cnf(c_7017,plain,
( doDivides0(sK0(sK0(xp)),sK0(xp))
| sK0(xp) = sz10
| sK0(xp) = sz00 ),
inference(copy,[status(thm)],[c_7197]) ).
cnf(c_7198,plain,
( sK0(xp) != sz10
| sz10 = xp
| sz00 = xp
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_3541,c_261]) ).
cnf(c_7199,plain,
( sK0(xp) != sz10
| sz10 = xp
| sz00 = xp ),
inference(resolve,[status(thm)],[c_523,c_7198]) ).
cnf(c_7200,plain,
( sK0(xp) != sz10
| sz10 = xp ),
inference(resolve,[status(thm)],[c_306,c_7199]) ).
cnf(c_7022,plain,
sK0(xp) != sz10,
inference(resolve,[status(thm)],[c_304,c_7200]) ).
cnf(c_7201,plain,
( sK0(xp) != sz00
| sz10 = xp
| sz00 = xp
| ~ aNaturalNumber0(xp) ),
inference(resolve,[status(thm)],[c_3541,c_259]) ).
cnf(c_7202,plain,
( sK0(xp) != sz00
| sz10 = xp
| sz00 = xp ),
inference(resolve,[status(thm)],[c_523,c_7201]) ).
cnf(c_7203,plain,
( sK0(xp) != sz00
| sz10 = xp ),
inference(resolve,[status(thm)],[c_306,c_7202]) ).
cnf(c_7023,plain,
sK0(xp) != sz00,
inference(resolve,[status(thm)],[c_304,c_7203]) ).
cnf(c_7204,plain,
( doDivides0(sK0(sK0(xp)),sK0(xp))
| sK0(xp) = sz10 ),
inference(resolve,[status(thm)],[c_7023,c_7017]) ).
cnf(c_7026,plain,
doDivides0(sK0(sK0(xp)),sK0(xp)),
inference(resolve,[status(thm)],[c_7022,c_7204]) ).
cnf(c_7205,plain,
( xp = sK0(xp)
| sz10 = sK0(xp)
| ~ aNaturalNumber0(sK0(xp)) ),
inference(resolve,[status(thm)],[c_3532,c_301]) ).
cnf(c_7206,plain,
( xp = sK0(xp)
| sK0(xp) = sz10
| ~ aNaturalNumber0(sK0(xp)) ),
inference(copy,[status(thm)],[c_7205]) ).
cnf(c_7207,plain,
( sK0(xp) = xp
| sK0(xp) = sz10
| ~ aNaturalNumber0(sK0(xp)) ),
inference(copy,[status(thm)],[c_7206]) ).
cnf(c_7208,plain,
( sK0(xp) = xp
| sK0(xp) = sz10 ),
inference(resolve,[status(thm)],[c_3541,c_7207]) ).
cnf(c_7177,plain,
sK0(xp) = xp,
inference(resolve,[status(thm)],[c_7022,c_7208]) ).
cnf(c_7209,plain,
doDivides0(sK0(xp),sK0(xp)),
inference(paramod,[status(thm)],[c_7177,c_7026]) ).
cnf(c_7210,plain,
doDivides0(xp,sK0(xp)),
inference(paramod,[status(thm)],[c_7177,c_7209]) ).
cnf(c_7211,plain,
doDivides0(xp,xp),
inference(paramod,[status(thm)],[c_7177,c_7210]) ).
cnf(c_7187,plain,
$false,
inference(resolve,[status(thm)],[c_5769,c_7211]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM496+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/0.35 % Computer : n003.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sat Sep 26 03:00:53 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 1879835 was started by sandbox2 on n003,
% 0.10/0.36 % Sat Sep 26 03:00:53 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/0.43
% 0.14/0.43 % From the command line: assign(max_seconds, 300).
% 20.49/3.41
% 20.49/3.41 % given #500 (I,wt=45): 888 -aNaturalNumber0(A) | -aNaturalNumber0(B) | -aNaturalNumber0(C) | sdtasdt0(A,B) != sdtasdt0(C,A) | -iLess0(sdtpldt0(sdtpldt0(A,B),C),sdtpldt0(sdtpldt0(xn,xm),xp)) | sdtasdt0(C,f7(A,B,C)) = A | doDivides0(C,B) | sz00 = C | sz10 = C | doDivides0(f3(C),C). [factor(207,a,d),flip(d)].
% 20.49/3.41
% 20.49/3.41 % given #1000 (I,wt=35): 1524 -aNaturalNumber0(A) | -aNaturalNumber0(B) | -aNaturalNumber0(C) | sdtasdt0(xp,C) != sdtasdt0(A,B) | -iLess0(sdtpldt0(sdtpldt0(A,B),xp),sdtpldt0(sdtpldt0(xn,xm),xp)) | doDivides0(xp,A) | sdtasdt0(xp,f8(A,B,xp)) = B. [back_unit_del(85),unit_del(c,523)].
% 20.49/3.41
% 20.49/3.41 % given #1500 (I,wt=40): 2208 -aNaturalNumber0(A) | -aNaturalNumber0(B) | sz00 = B | sz10 = B | doDivides0(f5(A,B,B),B) | sdtasdt0(B,A) != sdtasdt0(A,B) | -iLess0(sdtpldt0(sdtpldt0(A,B),B),sdtpldt0(sdtpldt0(xn,xm),xp)) | doDivides0(B,A) | doDivides0(B,B). [factor(1248,a,f)].
% 20.49/3.41
% 20.49/3.41 % SZS status Theorem for theBenchmark
% 20.49/3.41
% 20.49/3.41 % Proof 1 at 2.68 (+ 0.24) seconds.
% 20.49/3.41 % Length of proof is 40.
% 20.49/3.41 % Level of proof is 6.
% 20.49/3.41 % Maximum clause weight is 17.000.
% 20.49/3.41 % Given clauses 1833.
% 20.49/3.41
% 20.49/3.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------