%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV007-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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 09:06:38 AM UTC 2026
% Result : Unsatisfiable 0.13s 10.42s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 9
% Syntax : Number of formulae : 30 ( 17 unt; 0 def)
% Number of atoms : 49 ( 5 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 41 ( 22 ~; 19 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-1 aty)
% Number of variables : 20 ( 0 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(less_than_successor,axiom,
! [VAR_0] : less_than(VAR_0,successor(VAR_0)),
file('theBenchmark.p',less_than_successor) ).
cnf(c_6,plain,
less_than(A,successor(A)),
inference(clausify,[status(thm)],[less_than_successor]) ).
fof(transitivity_of_less_than,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ less_than(VAR_2,VAR_1)
| ~ less_than(VAR_0,VAR_2)
| less_than(VAR_0,VAR_1) ),
file('theBenchmark.p',transitivity_of_less_than) ).
cnf(c_7,plain,
( ~ less_than(C,B)
| ~ less_than(A,C)
| less_than(A,B) ),
inference(clausify,[status(thm)],[transitivity_of_less_than]) ).
fof(all_related,axiom,
! [VAR_0,VAR_1] :
( VAR_0 = VAR_1
| less_than(VAR_1,VAR_0)
| less_than(VAR_0,VAR_1) ),
file('theBenchmark.p',all_related) ).
cnf(c_8,plain,
( A = B
| less_than(B,A)
| less_than(A,B) ),
inference(clausify,[status(thm)],[all_related]) ).
fof(anti_symmetry_of_less_than,axiom,
! [VAR_0,VAR_1] :
( ~ less_than(VAR_1,VAR_0)
| ~ less_than(VAR_0,VAR_1) ),
file('theBenchmark.p',anti_symmetry_of_less_than) ).
cnf(c_10,plain,
( ~ less_than(B,A)
| ~ less_than(A,B) ),
inference(clausify,[status(thm)],[anti_symmetry_of_less_than]) ).
fof(clause_3,axiom,
less_than(i,n),
file('theBenchmark.p',clause_3) ).
cnf(c_15,plain,
less_than(i,n),
inference(clausify,[status(thm)],[clause_3]) ).
fof(clause_4,axiom,
~ less_than(n,m),
file('theBenchmark.p',clause_4) ).
cnf(c_16,plain,
~ less_than(n,m),
inference(clausify,[status(thm)],[clause_4]) ).
fof(clause_5,axiom,
less_than(i,m),
file('theBenchmark.p',clause_5) ).
cnf(c_17,plain,
less_than(i,m),
inference(clausify,[status(thm)],[clause_5]) ).
fof(clause_8,axiom,
less_than(a(m),a(k)),
file('theBenchmark.p',clause_8) ).
cnf(c_21,plain,
less_than(a(m),a(k)),
inference(clausify,[status(thm)],[clause_8]) ).
fof(clause_11,axiom,
! [VAR_0] :
( ~ less_than(a(VAR_0),a(k))
| ~ less_than(VAR_0,successor(n))
| less_than(VAR_0,i) ),
file('theBenchmark.p',clause_11) ).
cnf(c_24,plain,
( ~ less_than(a(A),a(k))
| ~ less_than(A,successor(n))
| less_than(A,i) ),
inference(clausify,[status(thm)],[clause_11]) ).
cnf(c_29,plain,
( ~ less_than(A,B)
| less_than(A,successor(B)) ),
inference(resolve,[status(thm)],[c_7,c_6]) ).
cnf(c_71,plain,
~ less_than(n,i),
inference(resolve,[status(thm)],[c_15,c_10]) ).
cnf(c_75,plain,
( m = n
| less_than(m,n) ),
inference(resolve,[status(thm)],[c_16,c_8]) ).
cnf(c_86,plain,
~ less_than(m,i),
inference(resolve,[status(thm)],[c_17,c_10]) ).
cnf(c_237,plain,
( ~ less_than(m,successor(n))
| less_than(m,i) ),
inference(resolve,[status(thm)],[c_24,c_21]) ).
cnf(c_114,plain,
~ less_than(m,successor(n)),
inference(resolve,[status(thm)],[c_86,c_237]) ).
cnf(c_238,plain,
( ~ less_than(a(n),a(k))
| ~ less_than(n,successor(n)) ),
inference(resolve,[status(thm)],[c_24,c_71]) ).
cnf(c_125,plain,
~ less_than(a(n),a(k)),
inference(resolve,[status(thm)],[c_238,c_6]) ).
cnf(c_239,plain,
( less_than(m,successor(n))
| m = n ),
inference(resolve,[status(thm)],[c_75,c_29]) ).
cnf(c_230,plain,
m = n,
inference(resolve,[status(thm)],[c_114,c_239]) ).
cnf(c_240,plain,
less_than(a(n),a(k)),
inference(paramod,[status(thm)],[c_230,c_21]) ).
cnf(c_236,plain,
$false,
inference(resolve,[status(thm)],[c_125,c_240]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV007-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/10.38 % Computer : n013.cluster.edu
% 0.09/10.38 % Model : x86_64 x86_64
% 0.09/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.38 % Memory : 8046.5625MB
% 0.09/10.38 % OS : Linux 6.8.0-71-generic
% 0.09/10.38 % CPULimit : 300
% 0.09/10.38 % WCLimit : 300
% 0.09/10.38 % DateTime : Sat Sep 26 13:04:19 UTC 2026
% 0.09/10.38 % CPUTime :
% 0.09/10.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/10.39 % Process 2808763 was started by sandbox on n013,
% 0.09/10.39 % Sat Sep 26 13:04:19 2026
% 0.09/10.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/10.39
% 0.09/10.39 % From the command line: assign(max_seconds, 300).
% 0.13/10.42
% 0.13/10.42 % SZS status Unsatisfiable for theBenchmark
% 0.13/10.42
% 0.13/10.42 % Proof 1 at 0.01 (+ 0.01) seconds.
% 0.13/10.42 % Length of proof is 17.
% 0.13/10.42 % Level of proof is 4.
% 0.13/10.42 % Maximum clause weight is 22.000.
% 0.13/10.42 % Given clauses 49.
% 0.13/10.42
% 0.13/10.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------