%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : NUM521+1 : 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 : n002.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:16 AM UTC 2026
% Result : Theorem 0.19s 5.51s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 5
% Syntax : Number of formulae : 31 ( 13 unt; 0 def)
% Number of atoms : 70 ( 21 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 69 ( 30 ~; 31 |; 7 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 10 ( 0 sgn 2 !; 0 ?)
% 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__2287,axiom,
~ ( sdtlseqdt0(xm,xp)
& xm != xp
& sdtlseqdt0(xn,xp)
& xn != xp ),
file('theBenchmark.p',m__2287) ).
cnf(c_85,plain,
( ~ sdtlseqdt0(xm,xp)
| xp = xm
| ~ sdtlseqdt0(xn,xp)
| xp = xn ),
inference(clausify,[status(thm)],[m__2287]) ).
cnf(c_360,plain,
( ~ sdtlseqdt0(xm,xp)
| xp = xm
| ~ sdtlseqdt0(xn,xp)
| xn = xp ),
inference(copy,[status(thm)],[c_85]) ).
cnf(c_86,plain,
( ~ sdtlseqdt0(xm,xp)
| xm = xp
| ~ sdtlseqdt0(xn,xp)
| xn = xp ),
inference(copy,[status(thm)],[c_360]) ).
fof(m__2075,axiom,
~ sdtlseqdt0(xp,xm),
file('theBenchmark.p',m__2075) ).
cnf(c_87,plain,
~ sdtlseqdt0(xp,xm),
inference(clausify,[status(thm)],[m__2075]) ).
fof(m__1870,axiom,
~ sdtlseqdt0(xp,xn),
file('theBenchmark.p',m__1870) ).
cnf(c_88,plain,
~ sdtlseqdt0(xp,xn),
inference(clausify,[status(thm)],[m__1870]) ).
cnf(c_90,plain,
aNaturalNumber0(xp),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_91,plain,
aNaturalNumber0(xm),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_92,plain,
aNaturalNumber0(xn),
inference(clausify,[status(thm)],[m__1837]) ).
cnf(c_118,plain,
( sdtlseqdt0(B,A)
| sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLETotal]) ).
cnf(c_119,plain,
( B != A
| sdtlseqdt0(A,B)
| ~ aNaturalNumber0(B)
| ~ aNaturalNumber0(A) ),
inference(clausify,[status(thm)],[mLETotal]) ).
cnf(c_361,plain,
( sdtlseqdt0(A,xn)
| sdtlseqdt0(xn,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_118,c_92]) ).
cnf(c_362,plain,
( sdtlseqdt0(xp,xn)
| sdtlseqdt0(xn,xp) ),
inference(resolve,[status(thm)],[c_361,c_90]) ).
cnf(c_346,plain,
sdtlseqdt0(xn,xp),
inference(resolve,[status(thm)],[c_88,c_362]) ).
cnf(c_363,plain,
( sdtlseqdt0(A,xm)
| sdtlseqdt0(xm,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_118,c_91]) ).
cnf(c_364,plain,
( sdtlseqdt0(xp,xm)
| sdtlseqdt0(xm,xp) ),
inference(resolve,[status(thm)],[c_363,c_90]) ).
cnf(c_348,plain,
sdtlseqdt0(xm,xp),
inference(resolve,[status(thm)],[c_87,c_364]) ).
cnf(c_365,plain,
( ~ sdtlseqdt0(xm,xp)
| xm = xp
| xn = xp ),
inference(resolve,[status(thm)],[c_346,c_86]) ).
cnf(c_350,plain,
( xm = xp
| xn = xp ),
inference(resolve,[status(thm)],[c_348,c_365]) ).
cnf(c_366,plain,
( A != xp
| sdtlseqdt0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_119,c_90]) ).
cnf(c_367,plain,
( xn != xp
| sdtlseqdt0(xp,xn) ),
inference(resolve,[status(thm)],[c_366,c_92]) ).
cnf(c_357,plain,
xn != xp,
inference(resolve,[status(thm)],[c_367,c_88]) ).
cnf(c_368,plain,
( A != xp
| sdtlseqdt0(xp,A)
| ~ aNaturalNumber0(A) ),
inference(resolve,[status(thm)],[c_119,c_90]) ).
cnf(c_369,plain,
( xm != xp
| sdtlseqdt0(xp,xm) ),
inference(resolve,[status(thm)],[c_368,c_91]) ).
cnf(c_358,plain,
xm != xp,
inference(resolve,[status(thm)],[c_369,c_87]) ).
cnf(c_370,plain,
xm = xp,
inference(resolve,[status(thm)],[c_357,c_350]) ).
cnf(c_359,plain,
$false,
inference(resolve,[status(thm)],[c_358,c_370]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM521+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/5.40 % Computer : n002.cluster.edu
% 0.14/5.40 % Model : x86_64 x86_64
% 0.14/5.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/5.40 % Memory : 8046.5625MB
% 0.14/5.40 % OS : Linux 6.8.0-71-generic
% 0.14/5.40 % CPULimit : 300
% 0.14/5.40 % WCLimit : 300
% 0.14/5.40 % DateTime : Sat Sep 26 03:08:26 UTC 2026
% 0.14/5.41 % CPUTime :
% 0.14/5.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.14/5.41 % Process 699358 was started by sandbox2 on n002,
% 0.14/5.41 % Sat Sep 26 03:08:26 2026
% 0.14/5.41 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.14/5.43
% 0.14/5.43 % From the command line: assign(max_seconds, 300).
% 0.19/5.51
% 0.19/5.51 % SZS status Theorem for theBenchmark
% 0.19/5.51
% 0.19/5.51 % Proof 1 at 0.05 (+ 0.01) seconds.
% 0.19/5.51 % Length of proof is 18.
% 0.19/5.51 % Level of proof is 4.
% 0.19/5.51 % Maximum clause weight is 17.000.
% 0.19/5.51 % Given clauses 43.
% 0.19/5.51
% 0.19/5.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------