%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : ANA002-2 : TPTP v9.3.1. Bugfixed v1.0.1.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/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 : Thu Sep 24 08:12:51 AM UTC 2026
% Result : Unsatisfiable 120.12s 120.43s
% Output : Proof 120.12s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(in_interval,axiom,
( ~ less_than_or_equal(X,Upper)
| ~ less_than_or_equal(Lower,X)
| in_interval(Lower,X,Upper) ),
file('theBenchmark.p',in_interval) ).
cnf(reflexivity_of_less,axiom,
less_than_or_equal(X,X),
file('theBenchmark.p',reflexivity_of_less) ).
cnf(totality_of_less,axiom,
( less_than_or_equal(Y,X)
| less_than_or_equal(X,Y) ),
file('theBenchmark.p',totality_of_less) ).
cnf(transitivity_of_less,axiom,
( ~ less_than_or_equal(Y,Z)
| ~ less_than_or_equal(X,Y)
| less_than_or_equal(X,Z) ),
file('theBenchmark.p',transitivity_of_less) ).
cnf(interpolation1,axiom,
( less_than_or_equal(X,Y)
| ~ less_than_or_equal(X,q(Y,X)) ),
file('theBenchmark.p',interpolation1) ).
cnf(interpolation2,axiom,
( less_than_or_equal(Y,X)
| ~ less_than_or_equal(q(X,Y),X) ),
file('theBenchmark.p',interpolation2) ).
cnf(continuity1,axiom,
( ~ in_interval(lower_bound,X,upper_bound)
| ~ less_than_or_equal(X,h(X))
| less_than_or_equal(f(X),n0) ),
file('theBenchmark.p',continuity1) ).
cnf(continuity2,axiom,
( ~ in_interval(lower_bound,X,upper_bound)
| less_than_or_equal(Y,h(X))
| ~ less_than_or_equal(f(Y),n0)
| ~ less_than_or_equal(Y,X)
| less_than_or_equal(f(X),n0) ),
file('theBenchmark.p',continuity2) ).
cnf(continuity3,axiom,
( ~ in_interval(lower_bound,X,upper_bound)
| ~ less_than_or_equal(k(X),X)
| less_than_or_equal(n0,f(X)) ),
file('theBenchmark.p',continuity3) ).
cnf(continuity4,axiom,
( ~ in_interval(lower_bound,X,upper_bound)
| less_than_or_equal(k(X),Y)
| ~ less_than_or_equal(n0,f(Y))
| ~ less_than_or_equal(X,Y)
| less_than_or_equal(n0,f(X)) ),
file('theBenchmark.p',continuity4) ).
cnf(crossover1,axiom,
( ~ less_than_or_equal(f(X),n0)
| ~ less_than_or_equal(X,upper_bound)
| less_than_or_equal(X,l) ),
file('theBenchmark.p',crossover1) ).
cnf(crossover2_and_g_function1,axiom,
( less_than_or_equal(l,X)
| less_than_or_equal(g(X),upper_bound) ),
file('theBenchmark.p',crossover2_and_g_function1) ).
cnf(crossover3_and_g_function2,axiom,
( less_than_or_equal(l,X)
| less_than_or_equal(f(g(X)),n0) ),
file('theBenchmark.p',crossover3_and_g_function2) ).
cnf(crossover4_and_g_function3,axiom,
( less_than_or_equal(l,X)
| ~ less_than_or_equal(g(X),X) ),
file('theBenchmark.p',crossover4_and_g_function3) ).
cnf(the_interval,hypothesis,
less_than_or_equal(lower_bound,upper_bound),
file('theBenchmark.p',the_interval) ).
cnf(lower_mapping,hypothesis,
less_than_or_equal(f(lower_bound),n0),
file('theBenchmark.p',lower_mapping) ).
cnf(upper_mapping,hypothesis,
less_than_or_equal(n0,f(upper_bound)),
file('theBenchmark.p',upper_mapping) ).
cnf(prove_there_is_x_which_crosses,negated_conjecture,
~ in_interval(f(l),n0,f(l)),
file('theBenchmark.p',prove_there_is_x_which_crosses) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ANA002-2 : TPTP v9.3.1. Bugfixed v1.0.1.
% 0.00/0.05 This is a CNF_UNS_RFO_NEQ_NHN problem
% 0.00/0.06 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.41 % Computer : n006.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sun Sep 20 11:35:57 UTC 2026
% 0.14/0.42 % CPUTime :
% 120.12/120.43 % SZS status Unsatisfiable for theBenchmark
% 120.12/120.43 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------