%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ANA003-4 : 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 : n006.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 06:51:04 AM UTC 2026
% Result : Unsatisfiable 37.00s 5.39s
% Output : CNFRefutation 37.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 12
% Syntax : Number of formulae : 41 ( 8 unt; 0 def)
% Number of atoms : 94 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 83 ( 30 ~; 53 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-2 aty)
% Number of variables : 58 ( 2 sgn 20 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(minimum3,axiom,
! [VAR_0,VAR_1,VAR_2] :
( less_or_equal(VAR_0,VAR_1)
| ~ less_or_equal(VAR_0,minimum(VAR_1,VAR_2)) ),
file('theBenchmark.p',minimum3) ).
cnf(c_1,plain,
( less_or_equal(A,B)
| ~ less_or_equal(A,minimum(B,C)) ),
inference(clausify,[status(thm)],[minimum3]) ).
fof(minimum7,axiom,
! [VAR_0,VAR_1,VAR_2] :
( less_or_equal(VAR_0,VAR_2)
| ~ less_or_equal(VAR_0,minimum(VAR_1,VAR_2)) ),
file('theBenchmark.p',minimum7) ).
cnf(c_2,plain,
( less_or_equal(A,C)
| ~ less_or_equal(A,minimum(B,C)) ),
inference(clausify,[status(thm)],[minimum7]) ).
fof(minimum9,axiom,
! [VAR_0,VAR_1] :
( ~ less_or_equal(minimum(VAR_0,VAR_1),n0)
| less_or_equal(VAR_1,n0)
| less_or_equal(VAR_0,n0) ),
file('theBenchmark.p',minimum9) ).
cnf(c_3,plain,
( ~ less_or_equal(minimum(A,B),n0)
| less_or_equal(B,n0)
| less_or_equal(A,n0) ),
inference(clausify,[status(thm)],[minimum9]) ).
fof(less_or_equal_sum_of_halves,axiom,
! [VAR_0,VAR_1,VAR_2] :
( less_or_equal(add(VAR_0,VAR_2),VAR_1)
| ~ less_or_equal(VAR_2,half(VAR_1))
| ~ less_or_equal(VAR_0,half(VAR_1)) ),
file('theBenchmark.p',less_or_equal_sum_of_halves) ).
cnf(c_4,plain,
( less_or_equal(add(A,C),B)
| ~ less_or_equal(C,half(B))
| ~ less_or_equal(A,half(B)) ),
inference(clausify,[status(thm)],[less_or_equal_sum_of_halves]) ).
fof(zero_and_half,axiom,
! [VAR_0] :
( ~ less_or_equal(half(VAR_0),n0)
| less_or_equal(VAR_0,n0) ),
file('theBenchmark.p',zero_and_half) ).
cnf(c_5,plain,
( ~ less_or_equal(half(A),n0)
| less_or_equal(A,n0) ),
inference(clausify,[status(thm)],[zero_and_half]) ).
fof(clause_1,axiom,
! [VAR_0] :
( ~ less_or_equal(delta_1(VAR_0),n0)
| less_or_equal(VAR_0,n0) ),
file('theBenchmark.p',clause_1) ).
cnf(c_6,plain,
( ~ less_or_equal(delta_1(A),n0)
| less_or_equal(A,n0) ),
inference(clausify,[status(thm)],[clause_1]) ).
fof(clause_2,axiom,
! [VAR_0] :
( ~ less_or_equal(delta_2(VAR_0),n0)
| less_or_equal(VAR_0,n0) ),
file('theBenchmark.p',clause_2) ).
cnf(c_7,plain,
( ~ less_or_equal(delta_2(A),n0)
| less_or_equal(A,n0) ),
inference(clausify,[status(thm)],[clause_2]) ).
fof(clause_3,axiom,
! [VAR_0,VAR_1] :
( less_or_equal(absolute(add(f(VAR_1),negate(f(a_real_number)))),VAR_0)
| ~ less_or_equal(absolute(add(VAR_1,negate(a_real_number))),delta_1(VAR_0))
| less_or_equal(VAR_0,n0) ),
file('theBenchmark.p',clause_3) ).
cnf(c_8,plain,
( less_or_equal(absolute(add(f(B),negate(f(a_real_number)))),A)
| ~ less_or_equal(absolute(add(B,negate(a_real_number))),delta_1(A))
| less_or_equal(A,n0) ),
inference(clausify,[status(thm)],[clause_3]) ).
fof(clause_4,axiom,
! [VAR_0,VAR_1] :
( less_or_equal(absolute(add(g(VAR_1),negate(g(a_real_number)))),VAR_0)
| ~ less_or_equal(absolute(add(VAR_1,negate(a_real_number))),delta_2(VAR_0))
| less_or_equal(VAR_0,n0) ),
file('theBenchmark.p',clause_4) ).
cnf(c_9,plain,
( less_or_equal(absolute(add(g(B),negate(g(a_real_number)))),A)
| ~ less_or_equal(absolute(add(B,negate(a_real_number))),delta_2(A))
| less_or_equal(A,n0) ),
inference(clausify,[status(thm)],[clause_4]) ).
fof(clause_5,axiom,
~ less_or_equal(epsilon_0,n0),
file('theBenchmark.p',clause_5) ).
cnf(c_10,plain,
~ less_or_equal(epsilon_0,n0),
inference(clausify,[status(thm)],[clause_5]) ).
fof(clause_6,axiom,
! [VAR_0] :
( less_or_equal(absolute(add(xs(VAR_0),negate(a_real_number))),VAR_0)
| less_or_equal(VAR_0,n0) ),
file('theBenchmark.p',clause_6) ).
cnf(c_11,plain,
( less_or_equal(absolute(add(xs(A),negate(a_real_number))),A)
| less_or_equal(A,n0) ),
inference(clausify,[status(thm)],[clause_6]) ).
fof(clause_7_2,axiom,
! [VAR_0] :
( ~ less_or_equal(add(absolute(add(f(xs(VAR_0)),negate(f(a_real_number)))),absolute(add(g(xs(VAR_0)),negate(g(a_real_number))))),epsilon_0)
| less_or_equal(VAR_0,n0) ),
file('theBenchmark.p',clause_7_2) ).
cnf(c_12,plain,
( ~ less_or_equal(add(absolute(add(f(xs(A)),negate(f(a_real_number)))),absolute(add(g(xs(A)),negate(g(a_real_number))))),epsilon_0)
| less_or_equal(A,n0) ),
inference(clausify,[status(thm)],[clause_7_2]) ).
cnf(c_17,plain,
~ less_or_equal(half(epsilon_0),n0),
inference(resolve,[status(thm)],[c_5,c_10]) ).
cnf(c_25,plain,
( less_or_equal(absolute(add(xs(minimum(A,B)),negate(a_real_number))),B)
| less_or_equal(minimum(A,B),n0) ),
inference(resolve,[status(thm)],[c_11,c_2]) ).
cnf(c_26,plain,
( less_or_equal(absolute(add(xs(minimum(A,B)),negate(a_real_number))),A)
| less_or_equal(minimum(A,B),n0) ),
inference(resolve,[status(thm)],[c_11,c_1]) ).
cnf(c_51,plain,
~ less_or_equal(delta_2(half(epsilon_0)),n0),
inference(resolve,[status(thm)],[c_7,c_17]) ).
cnf(c_52,plain,
~ less_or_equal(delta_1(half(epsilon_0)),n0),
inference(resolve,[status(thm)],[c_6,c_17]) ).
cnf(c_81,plain,
( less_or_equal(absolute(add(f(xs(minimum(A,delta_1(B)))),negate(f(a_real_number)))),B)
| less_or_equal(B,n0)
| less_or_equal(minimum(A,delta_1(B)),n0) ),
inference(resolve,[status(thm)],[c_25,c_8]) ).
cnf(c_90,plain,
( less_or_equal(absolute(add(g(xs(minimum(delta_2(A),B))),negate(g(a_real_number)))),A)
| less_or_equal(A,n0)
| less_or_equal(minimum(delta_2(A),B),n0) ),
inference(resolve,[status(thm)],[c_26,c_9]) ).
cnf(c_15452,plain,
( less_or_equal(half(B),n0)
| less_or_equal(minimum(C,delta_1(half(B))),n0)
| less_or_equal(add(absolute(add(f(xs(minimum(C,delta_1(half(B))))),negate(f(a_real_number)))),A),B)
| ~ less_or_equal(A,half(B)) ),
inference(resolve,[status(thm)],[c_4,c_81]) ).
cnf(c_15453,plain,
( less_or_equal(half(B),n0)
| less_or_equal(minimum(delta_2(half(B)),C),n0)
| less_or_equal(half(B),n0)
| less_or_equal(minimum(A,delta_1(half(B))),n0)
| less_or_equal(add(absolute(add(f(xs(minimum(A,delta_1(half(B))))),negate(f(a_real_number)))),absolute(add(g(xs(minimum(delta_2(half(B)),C))),negate(g(a_real_number))))),B) ),
inference(resolve,[status(thm)],[c_15452,c_90]) ).
cnf(c_258,plain,
( less_or_equal(minimum(delta_2(half(B)),C),n0)
| less_or_equal(half(B),n0)
| less_or_equal(minimum(A,delta_1(half(B))),n0)
| less_or_equal(add(absolute(add(f(xs(minimum(A,delta_1(half(B))))),negate(f(a_real_number)))),absolute(add(g(xs(minimum(delta_2(half(B)),C))),negate(g(a_real_number))))),B) ),
inference(copy,[status(thm)],[c_15453]) ).
cnf(c_15454,plain,
( ~ less_or_equal(minimum(delta_2(half(epsilon_0)),A),n0)
| less_or_equal(A,n0) ),
inference(resolve,[status(thm)],[c_3,c_51]) ).
cnf(c_380,plain,
~ less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0),
inference(resolve,[status(thm)],[c_15454,c_52]) ).
cnf(c_15455,plain,
( less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0)
| less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0)
| less_or_equal(half(epsilon_0),n0)
| less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0) ),
inference(resolve,[status(thm)],[c_258,c_12]) ).
cnf(c_15456,plain,
( less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0)
| less_or_equal(half(epsilon_0),n0)
| less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0) ),
inference(copy,[status(thm)],[c_15455]) ).
cnf(c_15457,plain,
( less_or_equal(half(epsilon_0),n0)
| less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0) ),
inference(copy,[status(thm)],[c_15456]) ).
cnf(c_15458,plain,
less_or_equal(half(epsilon_0),n0),
inference(resolve,[status(thm)],[c_380,c_15457]) ).
cnf(c_15451,plain,
$false,
inference(resolve,[status(thm)],[c_17,c_15458]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ANA003-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.60 % Computer : n006.cluster.edu
% 0.14/0.60 % Model : x86_64 x86_64
% 0.14/0.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.60 % Memory : 8046.5625MB
% 0.14/0.60 % OS : Linux 6.8.0-71-generic
% 0.14/0.60 % CPULimit : 300
% 0.14/0.60 % WCLimit : 300
% 0.14/0.60 % DateTime : Sat Sep 26 22:02:10 UTC 2026
% 0.14/0.60 % CPUTime :
% 0.14/0.60 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.14/0.60 % Process 2215515 was started by sandbox on n006,
% 0.14/0.60 % Sat Sep 26 22:02:10 2026
% 0.14/0.60 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/0.61
% 0.14/0.61 % From the command line: assign(max_seconds, 300).
% 37.00/5.39
% 37.00/5.39 % given #500 (F,wt=29): 323 -less_or_equal(minimum(delta_2(half(epsilon_0)),delta_2(half(epsilon_0))),n0). [ur(13,a,51,a)].
% 37.00/5.39
% 37.00/5.39 % SZS status Unsatisfiable for theBenchmark
% 37.00/5.39
% 37.00/5.39 % Proof 1 at 3.17 (+ 1.56) seconds.
% 37.00/5.39 % Length of proof is 22.
% 37.00/5.39 % Level of proof is 4.
% 37.00/5.39 % Maximum clause weight is 90.000.
% 37.00/5.39 % Given clauses 719.
% 37.00/5.39
% 37.00/5.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------