%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ANA002-1 : TPTP v9.3.1. Bugfixed v1.0.1.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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 106.86s 14.17s
% Output : CNFRefutation 106.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 18
% Syntax : Number of formulae : 107 ( 33 unt; 0 def)
% Number of atoms : 269 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 294 ( 132 ~; 162 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 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 : 82 ( 0 sgn 24 !; 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,
! [VAR_0] : ~ in_interval(f(VAR_0),n0,f(VAR_0)),
file('theBenchmark.p',prove_there_is_x_which_crosses) ).
cnf(c_6,plain,
~ in_interval(f(A),n0,f(A)),
inference(clausify,[status(thm)],[prove_there_is_x_which_crosses]) ).
cnf(c_7,plain,
( ~ less_than_or_equal(n0,f(A))
| ~ less_than_or_equal(f(A),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]) ).
fof(reflexivity_of_less,axiom,
! [VAR_0] : less_than_or_equal(VAR_0,VAR_0),
file('theBenchmark.p',reflexivity_of_less) ).
cnf(c_23,plain,
less_than_or_equal(A,A),
inference(clausify,[status(thm)],[reflexivity_of_less]) ).
cnf(c_28,plain,
~ less_than_or_equal(f(upper_bound),n0),
inference(resolve,[status(thm)],[c_12,c_7]) ).
cnf(c_35,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_9753,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_37,plain,
less_than_or_equal(l,upper_bound),
inference(copy,[status(thm)],[c_9753]) ).
cnf(c_39,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_9754,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_40,plain,
less_than_or_equal(lower_bound,l),
inference(resolve,[status(thm)],[c_14,c_9754]) ).
cnf(c_53,plain,
( less_than_or_equal(B,A)
| less_than_or_equal(q(A,B),B) ),
inference(resolve,[status(thm)],[c_22,c_20]) ).
cnf(c_55,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_63,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_64,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(n0,f(A))
| less_than_or_equal(n0,f(B))
| less_than_or_equal(A,B) ),
inference(resolve,[status(thm)],[c_22,c_8]) ).
cnf(c_9755,plain,
( ~ less_than_or_equal(upper_bound,upper_bound)
| ~ less_than_or_equal(lower_bound,upper_bound)
| ~ less_than_or_equal(upper_bound,h(upper_bound)) ),
inference(resolve,[status(thm)],[c_11,c_28]) ).
cnf(c_9756,plain,
( ~ less_than_or_equal(upper_bound,upper_bound)
| ~ less_than_or_equal(upper_bound,h(upper_bound)) ),
inference(resolve,[status(thm)],[c_9755,c_14]) ).
cnf(c_73,plain,
~ less_than_or_equal(upper_bound,h(upper_bound)),
inference(resolve,[status(thm)],[c_9756,c_23]) ).
cnf(c_9757,plain,
( less_than_or_equal(l,A)
| ~ less_than_or_equal(upper_bound,upper_bound)
| ~ less_than_or_equal(lower_bound,upper_bound)
| less_than_or_equal(g(A),h(upper_bound))
| less_than_or_equal(f(upper_bound),n0)
| less_than_or_equal(l,A) ),
inference(resolve,[status(thm)],[c_35,c_17]) ).
cnf(c_9758,plain,
( ~ less_than_or_equal(upper_bound,upper_bound)
| ~ less_than_or_equal(lower_bound,upper_bound)
| less_than_or_equal(g(A),h(upper_bound))
| less_than_or_equal(f(upper_bound),n0)
| less_than_or_equal(l,A) ),
inference(copy,[status(thm)],[c_9757]) ).
cnf(c_9759,plain,
( ~ less_than_or_equal(upper_bound,upper_bound)
| ~ less_than_or_equal(lower_bound,upper_bound)
| less_than_or_equal(g(A),h(upper_bound))
| less_than_or_equal(l,A) ),
inference(resolve,[status(thm)],[c_28,c_9758]) ).
cnf(c_9760,plain,
( ~ less_than_or_equal(upper_bound,upper_bound)
| less_than_or_equal(g(A),h(upper_bound))
| less_than_or_equal(l,A) ),
inference(resolve,[status(thm)],[c_14,c_9759]) ).
cnf(c_135,plain,
( less_than_or_equal(g(A),h(upper_bound))
| less_than_or_equal(l,A) ),
inference(resolve,[status(thm)],[c_23,c_9760]) ).
cnf(c_9761,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_39,c_17]) ).
cnf(c_173,plain,
( less_than_or_equal(l,A)
| less_than_or_equal(g(A),l) ),
inference(copy,[status(thm)],[c_9761]) ).
cnf(c_271,plain,
( ~ less_than_or_equal(C,q(B,A))
| less_than_or_equal(C,A)
| less_than_or_equal(A,B) ),
inference(resolve,[status(thm)],[c_53,c_21]) ).
cnf(c_9762,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_173,c_35]) ).
cnf(c_9763,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_9762]) ).
cnf(c_9764,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_40,c_9763]) ).
cnf(c_292,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_37,c_9764]) ).
cnf(c_9765,plain,
( less_than_or_equal(l,h(upper_bound))
| less_than_or_equal(l,h(upper_bound)) ),
inference(resolve,[status(thm)],[c_135,c_15]) ).
cnf(c_777,plain,
less_than_or_equal(l,h(upper_bound)),
inference(copy,[status(thm)],[c_9765]) ).
cnf(c_9766,plain,
( ~ less_than_or_equal(A,h(upper_bound))
| ~ less_than_or_equal(upper_bound,A) ),
inference(resolve,[status(thm)],[c_21,c_73]) ).
cnf(c_787,plain,
~ less_than_or_equal(upper_bound,l),
inference(resolve,[status(thm)],[c_9766,c_777]) ).
cnf(c_803,plain,
~ less_than_or_equal(upper_bound,q(l,upper_bound)),
inference(resolve,[status(thm)],[c_20,c_787]) ).
cnf(c_804,plain,
~ less_than_or_equal(q(l,upper_bound),l),
inference(resolve,[status(thm)],[c_19,c_787]) ).
cnf(c_806,plain,
less_than_or_equal(q(l,upper_bound),upper_bound),
inference(resolve,[status(thm)],[c_803,c_22]) ).
cnf(c_860,plain,
less_than_or_equal(l,q(l,upper_bound)),
inference(resolve,[status(thm)],[c_804,c_22]) ).
cnf(c_9767,plain,
( ~ less_than_or_equal(f(q(l,upper_bound)),n0)
| ~ less_than_or_equal(q(l,upper_bound),upper_bound) ),
inference(resolve,[status(thm)],[c_18,c_804]) ).
cnf(c_881,plain,
~ less_than_or_equal(f(q(l,upper_bound)),n0),
inference(resolve,[status(thm)],[c_9767,c_806]) ).
cnf(c_9768,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(k(l),q(l,upper_bound))
| less_than_or_equal(n0,f(l))
| less_than_or_equal(f(q(l,upper_bound)),n0) ),
inference(resolve,[status(thm)],[c_860,c_63]) ).
cnf(c_9769,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| less_than_or_equal(k(l),q(l,upper_bound))
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_881,c_9768]) ).
cnf(c_9770,plain,
( ~ less_than_or_equal(l,upper_bound)
| less_than_or_equal(k(l),q(l,upper_bound))
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_40,c_9769]) ).
cnf(c_890,plain,
( less_than_or_equal(k(l),q(l,upper_bound))
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_37,c_9770]) ).
cnf(c_9771,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_292,c_15]) ).
cnf(c_7250,plain,
( less_than_or_equal(f(l),n0)
| less_than_or_equal(l,h(l)) ),
inference(copy,[status(thm)],[c_9771]) ).
cnf(c_9772,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_7250,c_11]) ).
cnf(c_9773,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_9772]) ).
cnf(c_9774,plain,
( ~ less_than_or_equal(l,upper_bound)
| less_than_or_equal(f(l),n0) ),
inference(resolve,[status(thm)],[c_40,c_9773]) ).
cnf(c_7332,plain,
less_than_or_equal(f(l),n0),
inference(resolve,[status(thm)],[c_37,c_9774]) ).
cnf(c_7373,plain,
~ less_than_or_equal(n0,f(l)),
inference(resolve,[status(thm)],[c_7332,c_7]) ).
cnf(c_7484,plain,
less_than_or_equal(k(l),q(l,upper_bound)),
inference(resolve,[status(thm)],[c_7373,c_890]) ).
cnf(c_9775,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_7373]) ).
cnf(c_9776,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(k(l),l) ),
inference(resolve,[status(thm)],[c_9775,c_40]) ).
cnf(c_7536,plain,
~ less_than_or_equal(k(l),l),
inference(resolve,[status(thm)],[c_9776,c_37]) ).
cnf(c_7561,plain,
~ less_than_or_equal(k(l),q(l,k(l))),
inference(resolve,[status(thm)],[c_20,c_7536]) ).
cnf(c_7562,plain,
~ less_than_or_equal(q(l,k(l)),l),
inference(resolve,[status(thm)],[c_19,c_7536]) ).
cnf(c_9777,plain,
( ~ less_than_or_equal(A,q(l,upper_bound))
| ~ less_than_or_equal(upper_bound,A) ),
inference(resolve,[status(thm)],[c_21,c_803]) ).
cnf(c_7624,plain,
~ less_than_or_equal(upper_bound,k(l)),
inference(resolve,[status(thm)],[c_9777,c_7484]) ).
cnf(c_9778,plain,
( ~ less_than_or_equal(A,q(l,k(l)))
| less_than_or_equal(A,k(l)) ),
inference(resolve,[status(thm)],[c_271,c_7536]) ).
cnf(c_7626,plain,
~ less_than_or_equal(upper_bound,q(l,k(l))),
inference(resolve,[status(thm)],[c_9778,c_7624]) ).
cnf(c_7873,plain,
less_than_or_equal(q(l,k(l)),upper_bound),
inference(resolve,[status(thm)],[c_7626,c_22]) ).
cnf(c_9779,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(q(l,k(l))))
| less_than_or_equal(n0,f(l)) ),
inference(resolve,[status(thm)],[c_64,c_7562]) ).
cnf(c_9780,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(q(l,k(l)))) ),
inference(resolve,[status(thm)],[c_9779,c_7373]) ).
cnf(c_9781,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(lower_bound,l)
| ~ less_than_or_equal(n0,f(q(l,k(l)))) ),
inference(resolve,[status(thm)],[c_9780,c_7561]) ).
cnf(c_9782,plain,
( ~ less_than_or_equal(l,upper_bound)
| ~ less_than_or_equal(n0,f(q(l,k(l)))) ),
inference(resolve,[status(thm)],[c_9781,c_40]) ).
cnf(c_8432,plain,
~ less_than_or_equal(n0,f(q(l,k(l)))),
inference(resolve,[status(thm)],[c_9782,c_37]) ).
cnf(c_9783,plain,
( less_than_or_equal(q(l,k(l)),l)
| less_than_or_equal(n0,f(q(l,k(l)))) ),
inference(resolve,[status(thm)],[c_7873,c_55]) ).
cnf(c_9784,plain,
less_than_or_equal(q(l,k(l)),l),
inference(resolve,[status(thm)],[c_8432,c_9783]) ).
cnf(c_9752,plain,
$false,
inference(resolve,[status(thm)],[c_7562,c_9784]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ANA002-1 : TPTP v9.3.1. Bugfixed v1.0.1.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.60 % Computer : n019.cluster.edu
% 0.13/0.60 % Model : x86_64 x86_64
% 0.13/0.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.60 % Memory : 8046.5625MB
% 0.13/0.60 % OS : Linux 6.8.0-71-generic
% 0.13/0.60 % CPULimit : 300
% 0.13/0.60 % WCLimit : 300
% 0.13/0.60 % DateTime : Sat Sep 26 22:01:52 UTC 2026
% 0.13/0.60 % CPUTime :
% 0.13/0.60 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.60 % Process 2281054 was started by sandbox2 on n019,
% 0.13/0.60 % Sat Sep 26 22:01:52 2026
% 0.13/0.60 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.61
% 0.13/0.61 % From the command line: assign(max_seconds, 300).
% 106.86/14.17
% 106.86/14.17 % given #500 (A,wt=14): 236 less_than_or_equal(l,A) | less_than_or_equal(B,g(A)) | -less_than_or_equal(B,A). [resolve(56,a,21,c)].
% 106.86/14.17
% 106.86/14.17 % SZS status Unsatisfiable for theBenchmark
% 106.86/14.17
% 106.86/14.17 % Proof 1 at 4.59 (+ 0.90) seconds.
% 106.86/14.17 % Length of proof is 57.
% 106.86/14.17 % Level of proof is 14.
% 106.86/14.17 % Maximum clause weight is 26.000.
% 106.86/14.17 % Given clauses 871.
% 106.86/14.17
% 106.86/14.17 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------