%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM505+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 : n016.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:13 AM UTC 2026
% Result : Theorem 16.74s 25.03s
% Output : CNFRefutation 16.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 4
% Syntax : Number of formulae : 18 ( 8 unt; 0 def)
% Number of atoms : 46 ( 11 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 41 ( 13 ~; 13 |; 12 &)
% ( 0 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 9 ( 0 sgn 2 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(mLETotal,axiom,
! [W0,W1] :
( ( aNaturalNumber0(W1)
& aNaturalNumber0(W0) )
=> ( ( sdtlseqdt0(W1,W0)
& W1 != W0 )
| sdtlseqdt0(W0,W1) ) ),
file('theBenchmark.p',mLETotal) ).
fof(m__1837,axiom,
( aNaturalNumber0(xp)
& aNaturalNumber0(xm)
& aNaturalNumber0(xn) ),
file('theBenchmark.p',m__1837) ).
fof(m__2306,axiom,
( xk = sdtsldt0(sdtasdt0(xn,xm),xp)
& sdtasdt0(xn,xm) = sdtasdt0(xp,xk)
& aNaturalNumber0(xk) ),
file('theBenchmark.p',m__2306) ).
fof(m__,conjecture,
( ~ ( sdtlseqdt0(xp,xk)
| ? [W0] :
( sdtpldt0(xp,W0) = xk
& aNaturalNumber0(W0) ) )
=> ( ( sdtlseqdt0(xk,xp)
| ? [W0] :
( sdtpldt0(xk,W0) = xp
& aNaturalNumber0(W0) ) )
& xk != xp ) ),
file('theBenchmark.p',m__) ).
fof(m___neg,negated_conjecture,
~ ( ~ ( sdtlseqdt0(xp,xk)
| ? [W0] :
( sdtpldt0(xp,W0) = xk
& aNaturalNumber0(W0) ) )
=> ( ( sdtlseqdt0(xk,xp)
| ? [W0] :
( sdtpldt0(xk,W0) = xp
& aNaturalNumber0(W0) ) )
& xk != xp ) ),
inference(assume_negation,[status(cth)],[m__]) ).
cnf(c_300,negated_conjecture,
( ~ sdtlseqdt0(xk,xp)
| xk = xp ),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_302,negated_conjecture,
~ sdtlseqdt0(xp,xk),
inference(clausify,[status(thm)],[m___neg]) ).
cnf(c_325,plain,
aNaturalNumber0(xk),
inference(clausify,[status(thm)],[m__2306]) ).
cnf(c_568,plain,
aNaturalNumber0(xp),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_596,plain,
( sdtlseqdt0(B,A)
| sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLETotal]) ).
cnf(c_3087,plain,
( sdtlseqdt0(A,xp)
| sdtlseqdt0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_596,c_568]) ).
cnf(c_6472,plain,
( sdtlseqdt0(xp,xp)
| ~ aNaturalNumber0(xp) ),
inference(factor,[status(thm)],[c_3087]) ).
cnf(c_3098,plain,
sdtlseqdt0(xp,xp),
inference(resolve,[status(thm)],[c_568,c_6472]) ).
cnf(c_6473,plain,
( sdtlseqdt0(xk,xp)
| sdtlseqdt0(xp,xk) ),
inference(resolve,[status(thm)],[c_3087,c_325]) ).
cnf(c_6451,negated_conjecture,
sdtlseqdt0(xk,xp),
inference(resolve,[status(thm)],[c_302,c_6473]) ).
cnf(c_6456,negated_conjecture,
xk = xp,
inference(resolve,[status(thm)],[c_6451,c_300]) ).
cnf(c_6474,plain,
~ sdtlseqdt0(xp,xp),
inference(paramod,[status(thm)],[c_6456,c_302]) ).
cnf(c_6471,plain,
$false,
inference(resolve,[status(thm)],[c_3098,c_6474]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM505+3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n016.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.07/20.43 % CPULimit : 300
% 0.07/20.43 % WCLimit : 300
% 0.07/20.43 % DateTime : Sat Sep 26 03:02:22 UTC 2026
% 0.07/20.44 % CPUTime :
% 0.07/20.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/20.44 % Process 2335526 was started by sandbox on n010,
% 0.07/20.44 % Sat Sep 26 03:02:22 2026
% 0.07/20.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.34/20.53
% 0.34/20.53 % From the command line: assign(max_seconds, 300).
% 16.74/25.03
% 16.74/25.03 % given #500 (I,wt=54): 927 -aNaturalNumber0(A) | -aNaturalNumber0(B) | -aNaturalNumber0(C) | sdtasdt0(C,B) != sdtasdt0(A,B) | -iLess0(sdtpldt0(sdtpldt0(A,B),C),sdtpldt0(sdtpldt0(xn,xm),xp)) | doDivides0(C,A) | doDivides0(C,B) | sz00 = C | sz10 = C | aNaturalNumber0(f3(C)). [factor(206,b,d)].
% 16.74/25.03
% 16.74/25.03 % given #1000 (I,wt=66): 1557 -aNaturalNumber0(A) | -aNaturalNumber0(B) | -aNaturalNumber0(C) | sz00 = C | sz10 = C | aNaturalNumber0(f6(A,B,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 | sdtasdt0(C,f8(A,B,C)) = B. [factor(523,a,g),flip(g)].
% 16.74/25.03
% 16.74/25.03 % given #1500 (I,wt=57): 2205 -aNaturalNumber0(A) | -aNaturalNumber0(B) | sdtasdt0(B,B) != sdtasdt0(A,A) | -iLess0(sdtpldt0(sdtpldt0(A,A),B),sdtpldt0(sdtpldt0(xn,xm),xp)) | aNaturalNumber0(f7(A,A,B)) | aNaturalNumber0(f8(A,A,B)) | sz00 = B | sz10 = B | f3(B) != sz10. [factor(1173,b,c)].
% 16.74/25.03
% 16.74/25.03 % given #2000 (T,wt=13): 2952 -aNaturalNumber0(A) | -doDivides0(xk,A) | doDivides0(xr,A). [resolve(578,d,314,a),unit_del(a,318),unit_del(b,325)].
% 16.74/25.03
% 16.74/25.03 % SZS status Theorem for theBenchmark
% 16.74/25.03
% 16.74/25.03 % Proof 1 at 1.86 (+ 0.16) seconds.
% 16.74/25.03 % Length of proof is 14.
% 16.74/25.03 % Level of proof is 5.
% 16.74/25.03 % Maximum clause weight is 15.000.
% 16.74/25.03 % Given clauses 2055.
% 16.74/25.03
% 16.74/25.03 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------