%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ANA002-2 : TPTP v9.3.1. Bugfixed v1.0.1.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 43.02s 12.68s
% Output : CNFRefutation 43.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 17
% Syntax : Number of formulae : 120 ( 28 unt; 0 def)
% Number of atoms : 329 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 370 ( 161 ~; 209 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 74 ( 0 sgn 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(continuity1,axiom,
! [VAR_0] :
( ~ in_interval(lower_bound,VAR_0,upper_bound)
| ~ less_than_or_equal(VAR_0,h(VAR_0))
| less_than_or_equal(f(VAR_0),n0) ),
file('theBenchmark.p',continuity1) ).
cnf(c_1,plain,
( ~ in_interval(lower_bound,A,upper_bound)
| ~ less_than_or_equal(A,h(A))
| less_than_or_equal(f(A),n0) ),
inference(clausify,[status(thm)],[continuity1]) ).
fof(in_interval,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ less_than_or_equal(VAR_1,VAR_2)
| ~ less_than_or_equal(VAR_0,VAR_1)
| in_interval(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',in_interval) ).
cnf(c_2,plain,
( ~ less_than_or_equal(B,C)
| ~ less_than_or_equal(A,B)
| in_interval(A,B,C) ),
inference(clausify,[status(thm)],[in_interval]) ).
fof(continuity2,axiom,
! [VAR_0,VAR_1] :
( ~ in_interval(lower_bound,VAR_0,upper_bound)
| less_than_or_equal(VAR_1,h(VAR_0))
| ~ less_than_or_equal(f(VAR_1),n0)
| ~ less_than_or_equal(VAR_1,VAR_0)
| less_than_or_equal(f(VAR_0),n0) ),
file('theBenchmark.p',continuity2) ).
cnf(c_3,plain,
( ~ in_interval(lower_bound,A,upper_bound)
| less_than_or_equal(B,h(A))
| ~ less_than_or_equal(f(B),n0)
| ~ less_than_or_equal(B,A)
| less_than_or_equal(f(A),n0) ),
inference(clausify,[status(thm)],[continuity2]) ).
fof(continuity3,axiom,
! [VAR_0] :
( ~ in_interval(lower_bound,VAR_0,upper_bound)
| ~ less_than_or_equal(k(VAR_0),VAR_0)
| less_than_or_equal(n0,f(VAR_0)) ),
file('theBenchmark.p',continuity3) ).
cnf(c_4,plain,
( ~ in_interval(lower_bound,A,upper_bound)
| ~ less_than_or_equal(k(A),A)
| less_than_or_equal(n0,f(A)) ),
inference(clausify,[status(thm)],[continuity3]) ).
fof(continuity4,axiom,
! [VAR_0,VAR_1] :
( ~ in_interval(lower_bound,VAR_0,upper_bound)
| less_than_or_equal(k(VAR_0),VAR_1)
| ~ less_than_or_equal(n0,f(VAR_1))
| ~ less_than_or_equal(VAR_0,VAR_1)
| less_than_or_equal(n0,f(VAR_0)) ),
file('theBenchmark.p',continuity4) ).
cnf(c_5,plain,
( ~ in_interval(lower_bound,A,upper_bound)
| less_than_or_equal(k(A),B)
| ~ less_than_or_equal(n0,f(B))
| ~ less_than_or_equal(A,B)
| less_than_or_equal(n0,f(A)) ),
inference(clausify,[status(thm)],[continuity4]) ).
fof(prove_there_is_x_which_crosses,axiom,
~ in_interval(f(l),n0,f(l)),
file('theBenchmark.p',prove_there_is_x_which_crosses) ).
cnf(c_6,plain,
~ in_interval(f(l),n0,f(l)),
inference(clausify,[status(thm)],[prove_there_is_x_which_crosses]) ).
cnf(c_7,plain,
( ~ less_than_or_equal(n0,f(l))
| ~ less_than_or_equal(f(l),n0) ),
inference(resolve,[status(thm)],[c_6,c_2]) ).
cnf(c_8,plain,
( ~ less_than_or_equal(A,upper_bound)
| ~ less_than_or_equal(lower_bound,A)
| less_than_or_equal(k(A),B)
| ~ less_than_or_equal(n0,f(B))
| ~ less_than_or_equal(A,B)
| less_than_or_equal(n0,f(A)) ),
inference(resolve,[status(thm)],[c_5,c_2]) ).
cnf(c_9,plain,
( ~ less_than_or_equal(A,upper_bound)
| ~ less_than_or_equal(lower_bound,A)
| ~ less_than_or_equal(k(A),A)
| less_than_or_equal(n0,f(A)) ),
inference(resolve,[status(thm)],[c_4,c_2]) ).
cnf(c_10,plain,
( ~ less_than_or_equal(A,upper_bound)
| ~ less_than_or_equal(lower_bound,A)
| less_than_or_equal(B,h(A))
| ~ less_than_or_equal(f(B),n0)
| ~ less_than_or_equal(B,A)
| less_than_or_equal(f(A),n0) ),
inference(resolve,[status(thm)],[c_3,c_2]) ).
cnf(c_11,plain,
( ~ less_than_or_equal(A,upper_bound)
| ~ less_than_or_equal(lower_bound,A)
| ~ less_than_or_equal(A,h(A))
| less_than_or_equal(f(A),n0) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
fof(upper_mapping,axiom,
less_than_or_equal(n0,f(upper_bound)),
file('theBenchmark.p',upper_mapping) ).
cnf(c_12,plain,
less_than_or_equal(n0,f(upper_bound)),
inference(clausify,[status(thm)],[upper_mapping]) ).
fof(lower_mapping,axiom,
less_than_or_equal(f(lower_bound),n0),
file('theBenchmark.p',lower_mapping) ).
cnf(c_13,plain,
less_than_or_equal(f(lower_bound),n0),
inference(clausify,[status(thm)],[lower_mapping]) ).
fof(the_interval,axiom,
less_than_or_equal(lower_bound,upper_bound),
file('theBenchmark.p',the_interval) ).
cnf(c_14,plain,
less_than_or_equal(lower_bound,upper_bound),
inference(clausify,[status(thm)],[the_interval]) ).
fof(crossover4_and_g_function3,axiom,
! [VAR_0] :
( less_than_or_equal(l,VAR_0)
| ~ less_than_or_equal(g(VAR_0),VAR_0) ),
file('theBenchmark.p',crossover4_and_g_function3) ).
cnf(c_15,plain,
( less_than_or_equal(l,A)
| ~ less_than_or_equal(g(A),A) ),
inference(clausify,[status(thm)],[crossover4_and_g_function3]) ).
fof(crossover3_and_g_function2,axiom,
! [VAR_0] :
( less_than_or_equal(l,VAR_0)
| less_than_or_equal(f(g(VAR_0)),n0) ),
file('theBenchmark.p',crossover3_and_g_function2) ).
cnf(c_16,plain,
( less_than_or_equal(l,A)
| less_than_or_equal(f(g(A)),n0) ),
inference(clausify,[status(thm)],[crossover3_and_g_function2]) ).
fof(crossover2_and_g_function1,axiom,
! [VAR_0] :
( less_than_or_equal(l,VAR_0)
| less_than_or_equal(g(VAR_0),upper_bound) ),
file('theBenchmark.p',crossover2_and_g_function1) ).
cnf(c_17,plain,
( less_than_or_equal(l,A)
| less_than_or_equal(g(A),upper_bound) ),
inference(clausify,[status(thm)],[crossover2_and_g_function1]) ).
fof(crossover1,axiom,
! [VAR_0] :
( ~ less_than_or_equal(f(VAR_0),n0)
| ~ less_than_or_equal(VAR_0,upper_bound)
| less_than_or_equal(VAR_0,l) ),
file('theBenchmark.p',crossover1) ).
cnf(c_18,plain,
( ~ less_than_or_equal(f(A),n0)
| ~ less_than_or_equal(A,upper_bound)
| less_than_or_equal(A,l) ),
inference(clausify,[status(thm)],[crossover1]) ).
fof(interpolation2,axiom,
! [VAR_0,VAR_1] :
( less_than_or_equal(VAR_1,VAR_0)
| ~ less_than_or_equal(q(VAR_0,VAR_1),VAR_0) ),
file('theBenchmark.p',interpolation2) ).
cnf(c_19,plain,
( less_than_or_equal(B,A)
| ~ less_than_or_equal(q(A,B),A) ),
inference(clausify,[status(thm)],[interpolation2]) ).
fof(interpolation1,axiom,
! [VAR_0,VAR_1] :
( less_than_or_equal(VAR_0,VAR_1)
| ~ less_than_or_equal(VAR_0,q(VAR_1,VAR_0)) ),
file('theBenchmark.p',interpolation1) ).
cnf(c_20,plain,
( less_than_or_equal(A,B)
| ~ less_than_or_equal(A,q(B,A)) ),
inference(clausify,[status(thm)],[interpolation1]) ).
fof(transitivity_of_less,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ less_than_or_equal(VAR_2,VAR_1)
| ~ less_than_or_equal(VAR_0,VAR_2)
| less_than_or_equal(VAR_0,VAR_1) ),
file('theBenchmark.p',transitivity_of_less) ).
cnf(c_21,plain,
( ~ less_than_or_equal(C,B)
| ~ less_than_or_equal(A,C)
| less_than_or_equal(A,B) ),
inference(clausify,[status(thm)],[transitivity_of_less]) ).
fof(totality_of_less,axiom,
! [VAR_0,VAR_1] :
( less_than_or_equal(VAR_1,VAR_0)
| less_than_or_equal(VAR_0,VAR_1) ),
file('theBenchmark.p',totality_of_less) ).
cnf(c_22,plain,
( less_than_or_equal(B,A)
| less_than_or_equal(A,B) ),
inference(clausify,[status(thm)],[totality_of_less]) ).
cnf(c_33,plain,
( ~ less_than_or_equal(B,upper_bound)
| ~ less_than_or_equal(lower_bound,B)
| less_than_or_equal(g(A),h(B))
| ~ less_than_or_equal(g(A),B)
| less_than_or_equal(f(B),n0)
| less_than_or_equal(l,A) ),
inference(resolve,[status(thm)],[c_16,c_10]) ).
cnf(c_4821,plain,
( less_than_or_equal(l,upper_bound)
| less_than_or_equal(l,upper_bound) ),
inference(resolve,[status(thm)],[c_17,c_15]) ).
cnf(c_34,plain,
less_than_or_equal(l,upper_bound),
inference(copy,[status(thm)],[c_4821]) ).
cnf(c_36,plain,
( less_than_or_equal(l,A)
| ~ less_than_or_equal(g(A),upper_bound)
| less_than_or_equal(g(A),l) ),
inference(resolve,[status(thm)],[c_18,c_16]) ).
cnf(c_4822,plain,
( ~ less_than_or_equal(lower_bound,upper_bound)
| less_than_or_equal(lower_bound,l) ),
inference(resolve,[status(thm)],[c_18,c_13]) ).
cnf(c_37,plain,
less_than_or_equal(lower_bound,l),
inference(resolve,[status(thm)],[c_14,c_4822]) ).
cnf(c_49,plain,
( ~ less_than_or_equal(C,B)
| less_than_or_equal(C,A)
| less_than_or_equal(A,B) ),
inference(resolve,[status(thm)],[c_22,c_21]) ).
cnf(c_52,plain,
( ~ less_than_or_equal(A,upper_bound)
| less_than_or_equal(A,l)
| less_than_or_equal(n0,f(A)) ),
inference(resolve,[status(thm)],[c_22,c_18]) ).
cnf(c_56,plain,
( ~ less_than_or_equal(B,upper_bound)
| ~ less_than_or_equal(lower_bound,B)
| less_than_or_equal(A,h(B))
| ~ less_than_or_equal(A,B)
| less_than_or_equal(f(B),n0)
| less_than_or_equal(n0,f(A)) ),
inference(resolve,[status(thm)],[c_22,c_10]) ).
cnf(c_57,plain,
( ~ less_than_or_equal(A,upper_bound)
| ~ less_than_or_equal(lower_bound,A)
| less_than_or_equal(B,h(A))
| ~ less_than_or_equal(f(B),n0)
| less_than_or_equal(f(A),n0)
| less_than_or_equal(A,B) ),
inference(resolve,[status(thm)],[c_22,c_10]) ).
cnf(c_58,plain,
( ~ less_than_or_equal(A,upper_bound)
| ~ less_than_or_equal(lower_bound,A)
| less_than_or_equal(n0,f(A))
| less_than_or_equal(A,k(A)) ),
inference(resolve,[status(thm)],[c_22,c_9]) ).
cnf(c_60,plain,
( ~ less_than_or_equal(B,upper_bound)
| ~ less_than_or_equal(lower_bound,B)
| less_than_or_equal(k(B),A)
| ~ less_than_or_equal(B,A)
| less_than_or_equal(n0,f(B))
| less_than_or_equal(f(A),n0) ),
inference(resolve,[status(thm)],[c_22,c_8]) ).
cnf(c_4823,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(k(l),upper_bound)
| ~ less_than_or_equal(n0,f(upper_bound))
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_34,c_8]) ).
cnf(c_4824,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(k(l),upper_bound)
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_12,c_4823]) ).
cnf(c_4825,plain,
( ~ less_than_or_equal(l,upper_bound)
| less_than_or_equal(k(l),upper_bound)
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_37,c_4824]) ).
cnf(c_70,plain,
( less_than_or_equal(k(l),upper_bound)
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_34,c_4825]) ).
cnf(c_72,plain,
( ~ less_than_or_equal(A,lower_bound)
| less_than_or_equal(A,l) ),
inference(resolve,[status(thm)],[c_37,c_21]) ).
cnf(c_81,plain,
( less_than_or_equal(lower_bound,A)
| less_than_or_equal(A,l) ),
inference(resolve,[status(thm)],[c_72,c_22]) ).
cnf(c_4826,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(n0,f(l))
| less_than_or_equal(lower_bound,k(l)) ),
inference(resolve,[status(thm)],[c_81,c_9]) ).
cnf(c_4827,plain,
( ~ less_than_or_equal(l,upper_bound)
| less_than_or_equal(n0,f(l))
| less_than_or_equal(lower_bound,k(l)) ),
inference(resolve,[status(thm)],[c_37,c_4826]) ).
cnf(c_95,plain,
( less_than_or_equal(n0,f(l))
| less_than_or_equal(lower_bound,k(l)) ),
inference(resolve,[status(thm)],[c_34,c_4827]) ).
cnf(c_4828,plain,
( less_than_or_equal(l,A)
| less_than_or_equal(l,A)
| less_than_or_equal(g(A),l) ),
inference(resolve,[status(thm)],[c_36,c_17]) ).
cnf(c_148,plain,
( less_than_or_equal(l,A)
| less_than_or_equal(g(A),l) ),
inference(copy,[status(thm)],[c_4828]) ).
cnf(c_4829,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(g(A),h(l))
| less_than_or_equal(f(l),n0)
| less_than_or_equal(l,A)
| less_than_or_equal(l,A) ),
inference(resolve,[status(thm)],[c_148,c_33]) ).
cnf(c_4830,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(g(A),h(l))
| less_than_or_equal(f(l),n0)
| less_than_or_equal(l,A) ),
inference(copy,[status(thm)],[c_4829]) ).
cnf(c_4831,plain,
( ~ less_than_or_equal(l,upper_bound)
| less_than_or_equal(g(A),h(l))
| less_than_or_equal(f(l),n0)
| less_than_or_equal(l,A) ),
inference(resolve,[status(thm)],[c_37,c_4830]) ).
cnf(c_310,plain,
( less_than_or_equal(g(A),h(l))
| less_than_or_equal(f(l),n0)
| less_than_or_equal(l,A) ),
inference(resolve,[status(thm)],[c_34,c_4831]) ).
cnf(c_329,plain,
( less_than_or_equal(k(l),A)
| less_than_or_equal(A,upper_bound)
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_70,c_49]) ).
cnf(c_4832,plain,
( ~ less_than_or_equal(l,upper_bound)
| less_than_or_equal(n0,f(l))
| less_than_or_equal(l,k(l)) ),
inference(resolve,[status(thm)],[c_58,c_37]) ).
cnf(c_489,plain,
( less_than_or_equal(n0,f(l))
| less_than_or_equal(l,k(l)) ),
inference(resolve,[status(thm)],[c_34,c_4832]) ).
cnf(c_4833,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| ~ less_than_or_equal(lower_bound,k(l))
| less_than_or_equal(l,h(k(l)))
| less_than_or_equal(f(k(l)),n0)
| less_than_or_equal(n0,f(l))
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_489,c_56]) ).
cnf(c_510,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| ~ less_than_or_equal(lower_bound,k(l))
| less_than_or_equal(l,h(k(l)))
| less_than_or_equal(f(k(l)),n0)
| less_than_or_equal(n0,f(l)) ),
inference(copy,[status(thm)],[c_4833]) ).
cnf(c_1870,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| ~ less_than_or_equal(lower_bound,k(l))
| less_than_or_equal(f(k(l)),n0)
| less_than_or_equal(h(k(l)),upper_bound)
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_329,c_11]) ).
cnf(c_4834,plain,
( less_than_or_equal(l,h(l))
| less_than_or_equal(f(l),n0)
| less_than_or_equal(l,h(l)) ),
inference(resolve,[status(thm)],[c_310,c_15]) ).
cnf(c_2353,plain,
( less_than_or_equal(f(l),n0)
| less_than_or_equal(l,h(l)) ),
inference(copy,[status(thm)],[c_4834]) ).
cnf(c_4835,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(f(l),n0)
| less_than_or_equal(f(l),n0) ),
inference(resolve,[status(thm)],[c_2353,c_11]) ).
cnf(c_4836,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(f(l),n0) ),
inference(copy,[status(thm)],[c_4835]) ).
cnf(c_4837,plain,
( ~ less_than_or_equal(l,upper_bound)
| less_than_or_equal(f(l),n0) ),
inference(resolve,[status(thm)],[c_37,c_4836]) ).
cnf(c_2362,plain,
less_than_or_equal(f(l),n0),
inference(resolve,[status(thm)],[c_34,c_4837]) ).
cnf(c_2364,plain,
~ less_than_or_equal(n0,f(l)),
inference(resolve,[status(thm)],[c_2362,c_7]) ).
cnf(c_2403,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| ~ less_than_or_equal(lower_bound,k(l))
| less_than_or_equal(f(k(l)),n0)
| less_than_or_equal(h(k(l)),upper_bound) ),
inference(resolve,[status(thm)],[c_2364,c_1870]) ).
cnf(c_2481,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| ~ less_than_or_equal(lower_bound,k(l))
| less_than_or_equal(l,h(k(l)))
| less_than_or_equal(f(k(l)),n0) ),
inference(resolve,[status(thm)],[c_2364,c_510]) ).
cnf(c_2497,plain,
less_than_or_equal(lower_bound,k(l)),
inference(resolve,[status(thm)],[c_2364,c_95]) ).
cnf(c_2499,plain,
less_than_or_equal(k(l),upper_bound),
inference(resolve,[status(thm)],[c_2364,c_70]) ).
cnf(c_4838,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| less_than_or_equal(l,h(k(l)))
| less_than_or_equal(f(k(l)),n0) ),
inference(resolve,[status(thm)],[c_2497,c_2481]) ).
cnf(c_2500,plain,
( less_than_or_equal(l,h(k(l)))
| less_than_or_equal(f(k(l)),n0) ),
inference(resolve,[status(thm)],[c_2499,c_4838]) ).
cnf(c_4839,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| less_than_or_equal(f(k(l)),n0)
| less_than_or_equal(h(k(l)),upper_bound) ),
inference(resolve,[status(thm)],[c_2497,c_2403]) ).
cnf(c_2502,plain,
( less_than_or_equal(f(k(l)),n0)
| less_than_or_equal(h(k(l)),upper_bound) ),
inference(resolve,[status(thm)],[c_2499,c_4839]) ).
cnf(c_4840,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| ~ less_than_or_equal(k(l),l) ),
inference(resolve,[status(thm)],[c_9,c_2364]) ).
cnf(c_4841,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(k(l),l) ),
inference(resolve,[status(thm)],[c_4840,c_37]) ).
cnf(c_2544,plain,
~ less_than_or_equal(k(l),l),
inference(resolve,[status(thm)],[c_4841,c_34]) ).
cnf(c_2549,plain,
~ less_than_or_equal(k(l),q(l,k(l))),
inference(resolve,[status(thm)],[c_20,c_2544]) ).
cnf(c_2550,plain,
~ less_than_or_equal(q(l,k(l)),l),
inference(resolve,[status(thm)],[c_19,c_2544]) ).
cnf(c_4842,plain,
( ~ less_than_or_equal(f(k(l)),n0)
| ~ less_than_or_equal(k(l),upper_bound) ),
inference(resolve,[status(thm)],[c_18,c_2544]) ).
cnf(c_2574,plain,
~ less_than_or_equal(f(k(l)),n0),
inference(resolve,[status(thm)],[c_4842,c_2499]) ).
cnf(c_2584,plain,
less_than_or_equal(h(k(l)),upper_bound),
inference(resolve,[status(thm)],[c_2574,c_2502]) ).
cnf(c_2585,plain,
less_than_or_equal(l,h(k(l))),
inference(resolve,[status(thm)],[c_2574,c_2500]) ).
cnf(c_4843,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| ~ less_than_or_equal(lower_bound,k(l))
| ~ less_than_or_equal(k(l),h(k(l))) ),
inference(resolve,[status(thm)],[c_11,c_2574]) ).
cnf(c_4844,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| ~ less_than_or_equal(k(l),h(k(l))) ),
inference(resolve,[status(thm)],[c_4843,c_2497]) ).
cnf(c_2954,plain,
~ less_than_or_equal(k(l),h(k(l))),
inference(resolve,[status(thm)],[c_4844,c_2499]) ).
cnf(c_3095,plain,
less_than_or_equal(l,q(l,k(l))),
inference(resolve,[status(thm)],[c_2550,c_22]) ).
cnf(c_3354,plain,
( less_than_or_equal(h(k(l)),l)
| less_than_or_equal(n0,f(h(k(l)))) ),
inference(resolve,[status(thm)],[c_2584,c_52]) ).
cnf(c_4845,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(k(l),h(k(l)))
| ~ less_than_or_equal(n0,f(h(k(l))))
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_2585,c_8]) ).
cnf(c_4846,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(k(l),h(k(l)))
| ~ less_than_or_equal(n0,f(h(k(l)))) ),
inference(resolve,[status(thm)],[c_2364,c_4845]) ).
cnf(c_4847,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| ~ less_than_or_equal(n0,f(h(k(l)))) ),
inference(resolve,[status(thm)],[c_2954,c_4846]) ).
cnf(c_4848,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(n0,f(h(k(l)))) ),
inference(resolve,[status(thm)],[c_37,c_4847]) ).
cnf(c_3436,plain,
~ less_than_or_equal(n0,f(h(k(l)))),
inference(resolve,[status(thm)],[c_34,c_4848]) ).
cnf(c_3438,plain,
less_than_or_equal(h(k(l)),l),
inference(resolve,[status(thm)],[c_3436,c_3354]) ).
cnf(c_4849,plain,
( ~ less_than_or_equal(A,l)
| ~ less_than_or_equal(q(l,k(l)),A) ),
inference(resolve,[status(thm)],[c_21,c_2550]) ).
cnf(c_3550,plain,
~ less_than_or_equal(q(l,k(l)),h(k(l))),
inference(resolve,[status(thm)],[c_4849,c_3438]) ).
cnf(c_4850,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| ~ less_than_or_equal(lower_bound,k(l))
| less_than_or_equal(q(l,k(l)),h(k(l)))
| ~ less_than_or_equal(f(q(l,k(l))),n0)
| less_than_or_equal(f(k(l)),n0) ),
inference(resolve,[status(thm)],[c_57,c_2549]) ).
cnf(c_4851,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| ~ less_than_or_equal(lower_bound,k(l))
| less_than_or_equal(q(l,k(l)),h(k(l)))
| ~ less_than_or_equal(f(q(l,k(l))),n0) ),
inference(resolve,[status(thm)],[c_4850,c_2574]) ).
cnf(c_4852,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| ~ less_than_or_equal(lower_bound,k(l))
| ~ less_than_or_equal(f(q(l,k(l))),n0) ),
inference(resolve,[status(thm)],[c_4851,c_3550]) ).
cnf(c_4853,plain,
( ~ less_than_or_equal(k(l),upper_bound)
| ~ less_than_or_equal(f(q(l,k(l))),n0) ),
inference(resolve,[status(thm)],[c_4852,c_2497]) ).
cnf(c_4734,plain,
~ less_than_or_equal(f(q(l,k(l))),n0),
inference(resolve,[status(thm)],[c_4853,c_2499]) ).
cnf(c_4854,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(k(l),q(l,k(l)))
| less_than_or_equal(n0,f(l))
| less_than_or_equal(f(q(l,k(l))),n0) ),
inference(resolve,[status(thm)],[c_3095,c_60]) ).
cnf(c_4855,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(k(l),q(l,k(l)))
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_4734,c_4854]) ).
cnf(c_4856,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(k(l),q(l,k(l))) ),
inference(resolve,[status(thm)],[c_2364,c_4855]) ).
cnf(c_4857,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l) ),
inference(resolve,[status(thm)],[c_2549,c_4856]) ).
cnf(c_4858,plain,
~ less_than_or_equal(l,upper_bound),
inference(resolve,[status(thm)],[c_37,c_4857]) ).
cnf(c_4820,plain,
$false,
inference(resolve,[status(thm)],[c_34,c_4858]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ANA002-2 : TPTP v9.3.1. Bugfixed v1.0.1.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n014.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 22:01:33 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 4189248 was started by sandbox on n014,
% 0.08/0.35 % Sat Sep 26 22:01:33 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.36
% 0.08/0.36 % From the command line: assign(max_seconds, 300).
% 43.02/12.68
% 43.02/12.68 % given #500 (A,wt=17): 288 less_than_or_equal(A,f(B)) | less_than_or_equal(n0,A) | less_than_or_equal(B,l) | -less_than_or_equal(B,upper_bound). [resolve(122,a,18,c)].
% 43.02/12.68
% 43.02/12.68 % SZS status Unsatisfiable for theBenchmark
% 43.02/12.68
% 43.02/12.68 % Proof 1 at 1.69 (+ 0.32) seconds.
% 43.02/12.68 % Length of proof is 65.
% 43.02/12.68 % Level of proof is 14.
% 43.02/12.68 % Maximum clause weight is 28.000.
% 43.02/12.68 % Given clauses 508.
% 43.02/12.68
% 43.02/12.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------