%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : ANA003-4 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:09:15 PM UTC 2026
% Result : Unsatisfiable 95.91s 79.23s
% Output : CNFRefutation 98.02s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_66)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_7_2,negated_conjecture,
( less_or_equal(X1,n0)
| ~ less_or_equal(add(absolute(add(f(xs(X1)),negate(f(a_real_number)))),absolute(add(g(xs(X1)),negate(g(a_real_number))))),epsilon_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_7_2) ).
cnf(clause_4,hypothesis,
( less_or_equal(X1,n0)
| less_or_equal(absolute(add(g(X2),negate(g(a_real_number)))),X1)
| ~ less_or_equal(absolute(add(X2,negate(a_real_number))),delta_2(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_4) ).
cnf(clause_3,hypothesis,
( less_or_equal(X1,n0)
| less_or_equal(absolute(add(f(X2),negate(f(a_real_number)))),X1)
| ~ less_or_equal(absolute(add(X2,negate(a_real_number))),delta_1(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_3) ).
cnf(clause_6,hypothesis,
( less_or_equal(X1,n0)
| less_or_equal(absolute(add(xs(X1),negate(a_real_number))),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_6) ).
cnf(less_or_equal_sum_of_halves,axiom,
( less_or_equal(add(X1,X3),X2)
| ~ less_or_equal(X1,half(X2))
| ~ less_or_equal(X3,half(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less_or_equal_sum_of_halves) ).
cnf(minimum9,axiom,
( less_or_equal(X1,n0)
| less_or_equal(X2,n0)
| ~ less_or_equal(minimum(X1,X2),n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minimum9) ).
cnf(minimum3,axiom,
( less_or_equal(X1,X2)
| ~ less_or_equal(X1,minimum(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minimum3) ).
cnf(minimum7,axiom,
( less_or_equal(X1,X3)
| ~ less_or_equal(X1,minimum(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',minimum7) ).
cnf(clause_2,hypothesis,
( less_or_equal(X1,n0)
| ~ less_or_equal(delta_2(X1),n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_2) ).
cnf(clause_1,hypothesis,
( less_or_equal(X1,n0)
| ~ less_or_equal(delta_1(X1),n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_1) ).
cnf(zero_and_half,axiom,
( less_or_equal(X1,n0)
| ~ less_or_equal(half(X1),n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',zero_and_half) ).
cnf(clause_5,hypothesis,
~ less_or_equal(epsilon_0,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_5) ).
cnf(i_0_12,negated_conjecture,
( less_or_equal(X1,n0)
| ~ less_or_equal(add(absolute(add(f(xs(X1)),negate(f(a_real_number)))),absolute(add(g(xs(X1)),negate(g(a_real_number))))),epsilon_0) ),
clause_7_2,
[final] ).
cnf(i_0_13,hypothesis,
( less_or_equal(X1,n0)
| less_or_equal(absolute(add(g(X2),negate(g(a_real_number)))),X1)
| ~ less_or_equal(absolute(add(X2,negate(a_real_number))),delta_2(X1)) ),
clause_4,
[final] ).
cnf(i_0_14,hypothesis,
( less_or_equal(X1,n0)
| less_or_equal(absolute(add(f(X2),negate(f(a_real_number)))),X1)
| ~ less_or_equal(absolute(add(X2,negate(a_real_number))),delta_1(X1)) ),
clause_3,
[final] ).
cnf(i_0_15,hypothesis,
( less_or_equal(X1,n0)
| less_or_equal(absolute(add(xs(X1),negate(a_real_number))),X1) ),
clause_6,
[final] ).
cnf(i_0_16,axiom,
( less_or_equal(add(X1,X3),X2)
| ~ less_or_equal(X1,half(X2))
| ~ less_or_equal(X3,half(X2)) ),
less_or_equal_sum_of_halves,
[final] ).
cnf(i_0_17,axiom,
( less_or_equal(X1,n0)
| less_or_equal(X2,n0)
| ~ less_or_equal(minimum(X1,X2),n0) ),
minimum9,
[final] ).
cnf(i_0_18,axiom,
( less_or_equal(X1,X2)
| ~ less_or_equal(X1,minimum(X2,X3)) ),
minimum3,
[final] ).
cnf(i_0_19,axiom,
( less_or_equal(X1,X3)
| ~ less_or_equal(X1,minimum(X2,X3)) ),
minimum7,
[final] ).
cnf(i_0_20,hypothesis,
( less_or_equal(X1,n0)
| ~ less_or_equal(delta_2(X1),n0) ),
clause_2,
[final] ).
cnf(i_0_21,hypothesis,
( less_or_equal(X1,n0)
| ~ less_or_equal(delta_1(X1),n0) ),
clause_1,
[final] ).
cnf(i_0_22,axiom,
( less_or_equal(X1,n0)
| ~ less_or_equal(half(X1),n0) ),
zero_and_half,
[final] ).
cnf(i_0_23,hypothesis,
~ less_or_equal(epsilon_0,n0),
clause_5,
[final] ).
cnf(i_0_136,plain,
~ less_or_equal(delta_2(minimum(delta_1(epsilon_0),delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_66,i_0_92,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_138,plain,
~ less_or_equal(delta_1(minimum(delta_1(epsilon_0),delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_66,i_0_92,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_140,plain,
~ less_or_equal(half(minimum(delta_1(epsilon_0),delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_66,i_0_92,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_146,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(minimum(n0,X1),X2)),
inference(scs_inference,[],[i_0_23,i_0_80,i_0_15,i_0_18]) ).
cnf(i_0_148,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(X1,minimum(n0,X2))),
inference(scs_inference,[],[i_0_23,i_0_80,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_150,plain,
~ less_or_equal(delta_2(delta_2(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_80,i_0_68,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_152,plain,
~ less_or_equal(delta_1(delta_2(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_80,i_0_68,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_154,plain,
~ less_or_equal(half(delta_2(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_80,i_0_68,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_160,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(minimum(X1,n0),X2)),
inference(scs_inference,[],[i_0_23,i_0_82,i_0_15,i_0_18]) ).
cnf(i_0_162,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(X1,minimum(X2,n0))),
inference(scs_inference,[],[i_0_23,i_0_82,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_164,plain,
~ less_or_equal(delta_2(delta_1(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_82,i_0_70,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_166,plain,
~ less_or_equal(delta_1(delta_1(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_82,i_0_70,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_168,plain,
~ less_or_equal(half(delta_1(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_82,i_0_70,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_178,plain,
~ less_or_equal(half(epsilon_0),minimum(minimum(n0,X1),X2)),
inference(scs_inference,[],[i_0_23,i_0_96,i_0_15,i_0_18]) ).
cnf(i_0_180,plain,
~ less_or_equal(half(epsilon_0),minimum(X1,minimum(n0,X2))),
inference(scs_inference,[],[i_0_23,i_0_96,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_182,plain,
~ less_or_equal(delta_2(half(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_96,i_0_72,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_184,plain,
~ less_or_equal(delta_1(half(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_96,i_0_72,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_186,plain,
~ less_or_equal(half(half(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_96,i_0_72,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_188,plain,
~ less_or_equal(minimum(half(minimum(epsilon_0,epsilon_0)),half(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_96,i_0_72,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22,i_0_17]) ).
cnf(i_0_194,plain,
~ less_or_equal(half(epsilon_0),minimum(minimum(X1,n0),X2)),
inference(scs_inference,[],[i_0_23,i_0_98,i_0_15,i_0_18]) ).
cnf(i_0_196,plain,
~ less_or_equal(half(epsilon_0),minimum(X1,minimum(X2,n0))),
inference(scs_inference,[],[i_0_23,i_0_98,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_198,plain,
~ less_or_equal(delta_2(delta_2(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_98,i_0_48,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_200,plain,
~ less_or_equal(delta_1(delta_2(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_98,i_0_48,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_202,plain,
~ less_or_equal(half(delta_2(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_98,i_0_48,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_204,plain,
~ less_or_equal(minimum(delta_2(delta_2(epsilon_0)),delta_2(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_98,i_0_48,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22,i_0_17]) ).
cnf(i_0_212,plain,
~ less_or_equal(delta_2(delta_1(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_26,i_0_50,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_214,plain,
~ less_or_equal(delta_1(delta_1(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_26,i_0_50,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_216,plain,
~ less_or_equal(half(delta_1(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_26,i_0_50,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_218,plain,
~ less_or_equal(minimum(delta_1(delta_2(epsilon_0)),delta_1(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_26,i_0_50,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22,i_0_17]) ).
cnf(i_0_406,plain,
~ less_or_equal(epsilon_0,minimum(minimum(minimum(n0,X1),X2),X3)),
inference(scs_inference,[],[i_0_23,i_0_44,i_0_15,i_0_18]) ).
cnf(i_0_408,plain,
~ less_or_equal(epsilon_0,minimum(X1,minimum(minimum(n0,X2),X3))),
inference(scs_inference,[],[i_0_23,i_0_44,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_422,plain,
~ less_or_equal(epsilon_0,minimum(minimum(X1,minimum(n0,X2)),X3)),
inference(scs_inference,[],[i_0_23,i_0_46,i_0_15,i_0_18]) ).
cnf(i_0_424,plain,
~ less_or_equal(epsilon_0,minimum(X1,minimum(X2,minimum(n0,X3)))),
inference(scs_inference,[],[i_0_23,i_0_46,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_438,plain,
~ less_or_equal(epsilon_0,minimum(minimum(minimum(X1,n0),X2),X3)),
inference(scs_inference,[],[i_0_23,i_0_208,i_0_15,i_0_18]) ).
cnf(i_0_440,plain,
~ less_or_equal(epsilon_0,minimum(X1,minimum(minimum(X2,n0),X3))),
inference(scs_inference,[],[i_0_23,i_0_208,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_452,plain,
~ less_or_equal(epsilon_0,minimum(minimum(X1,minimum(X2,n0)),X3)),
inference(scs_inference,[],[i_0_23,i_0_210,i_0_15,i_0_18]) ).
cnf(i_0_454,plain,
~ less_or_equal(epsilon_0,minimum(X1,minimum(X2,minimum(X3,n0)))),
inference(scs_inference,[],[i_0_23,i_0_210,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_2104,plain,
~ less_or_equal(delta_2(delta_2(epsilon_0)),minimum(n0,X1)),
inference(scs_inference,[],[i_0_48,i_0_15,i_0_18]) ).
cnf(i_0_2106,plain,
~ less_or_equal(delta_2(delta_2(epsilon_0)),minimum(X1,n0)),
inference(scs_inference,[],[i_0_48,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_2237,plain,
~ less_or_equal(delta_1(delta_2(epsilon_0)),minimum(n0,X1)),
inference(scs_inference,[],[i_0_50,i_0_15,i_0_18]) ).
cnf(i_0_2239,plain,
~ less_or_equal(delta_1(delta_2(epsilon_0)),minimum(X1,n0)),
inference(scs_inference,[],[i_0_50,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_222,plain,
~ less_or_equal(minimum(epsilon_0,epsilon_0),minimum(minimum(minimum(X1,n0),X2),X3)),
inference(scs_inference,[],[i_0_23,i_0_132,i_0_15,i_0_18]) ).
cnf(i_0_224,plain,
~ less_or_equal(minimum(epsilon_0,epsilon_0),minimum(X1,minimum(minimum(X2,n0),X3))),
inference(scs_inference,[],[i_0_23,i_0_132,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_226,plain,
~ less_or_equal(delta_2(half(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_132,i_0_52,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_228,plain,
~ less_or_equal(delta_1(half(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_132,i_0_52,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_230,plain,
~ less_or_equal(half(half(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_132,i_0_52,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_232,plain,
~ less_or_equal(minimum(half(delta_2(epsilon_0)),half(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_132,i_0_52,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22,i_0_17]) ).
cnf(i_0_240,plain,
~ less_or_equal(minimum(epsilon_0,epsilon_0),minimum(minimum(X1,minimum(X2,n0)),X3)),
inference(scs_inference,[],[i_0_23,i_0_134,i_0_15,i_0_18]) ).
cnf(i_0_242,plain,
~ less_or_equal(minimum(epsilon_0,epsilon_0),minimum(X1,minimum(X2,minimum(X3,n0)))),
inference(scs_inference,[],[i_0_23,i_0_134,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_244,plain,
~ less_or_equal(delta_2(minimum(delta_2(epsilon_0),delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_134,i_0_58,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_246,plain,
~ less_or_equal(delta_1(minimum(delta_2(epsilon_0),delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_134,i_0_58,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_248,plain,
~ less_or_equal(half(minimum(delta_2(epsilon_0),delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_134,i_0_58,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_256,plain,
~ less_or_equal(minimum(epsilon_0,epsilon_0),minimum(minimum(minimum(n0,X1),X2),X3)),
inference(scs_inference,[],[i_0_23,i_0_116,i_0_15,i_0_18]) ).
cnf(i_0_258,plain,
~ less_or_equal(minimum(epsilon_0,epsilon_0),minimum(X1,minimum(minimum(n0,X2),X3))),
inference(scs_inference,[],[i_0_23,i_0_116,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_260,plain,
~ less_or_equal(delta_2(delta_2(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_116,i_0_84,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_262,plain,
~ less_or_equal(delta_1(delta_2(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_116,i_0_84,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_264,plain,
~ less_or_equal(half(delta_2(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_116,i_0_84,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_266,plain,
~ less_or_equal(minimum(delta_2(delta_1(epsilon_0)),delta_2(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_116,i_0_84,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22,i_0_17]) ).
cnf(i_0_270,plain,
~ less_or_equal(minimum(epsilon_0,epsilon_0),minimum(minimum(X1,minimum(n0,X2)),X3)),
inference(scs_inference,[],[i_0_23,i_0_118,i_0_15,i_0_18]) ).
cnf(i_0_272,plain,
~ less_or_equal(minimum(epsilon_0,epsilon_0),minimum(X1,minimum(X2,minimum(n0,X3)))),
inference(scs_inference,[],[i_0_23,i_0_118,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_274,plain,
~ less_or_equal(delta_2(delta_1(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_118,i_0_86,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_276,plain,
~ less_or_equal(delta_1(delta_1(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_118,i_0_86,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_278,plain,
~ less_or_equal(half(delta_1(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_118,i_0_86,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_280,plain,
~ less_or_equal(minimum(delta_1(delta_1(epsilon_0)),delta_1(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_118,i_0_86,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22,i_0_17]) ).
cnf(i_0_284,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(minimum(minimum(n0,X1),X2),X3)),
inference(scs_inference,[],[i_0_23,i_0_146,i_0_15,i_0_18]) ).
cnf(i_0_286,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(X1,minimum(minimum(n0,X2),X3))),
inference(scs_inference,[],[i_0_23,i_0_146,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_288,plain,
~ less_or_equal(delta_2(half(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_146,i_0_88,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_290,plain,
~ less_or_equal(delta_1(half(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_146,i_0_88,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_292,plain,
~ less_or_equal(half(half(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_146,i_0_88,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_294,plain,
~ less_or_equal(minimum(half(delta_1(epsilon_0)),half(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_146,i_0_88,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22,i_0_17]) ).
cnf(i_0_302,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(minimum(X1,minimum(n0,X2)),X3)),
inference(scs_inference,[],[i_0_23,i_0_148,i_0_15,i_0_18]) ).
cnf(i_0_304,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(X1,minimum(X2,minimum(n0,X3)))),
inference(scs_inference,[],[i_0_23,i_0_148,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_306,plain,
~ less_or_equal(delta_2(delta_2(half(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_148,i_0_100,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_308,plain,
~ less_or_equal(delta_1(delta_2(half(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_148,i_0_100,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_310,plain,
~ less_or_equal(half(delta_2(half(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_148,i_0_100,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_312,plain,
~ less_or_equal(minimum(delta_2(half(epsilon_0)),delta_2(half(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_148,i_0_100,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22,i_0_17]) ).
cnf(i_0_318,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(minimum(minimum(X1,n0),X2),X3)),
inference(scs_inference,[],[i_0_23,i_0_160,i_0_15,i_0_18]) ).
cnf(i_0_320,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(X1,minimum(minimum(X2,n0),X3))),
inference(scs_inference,[],[i_0_23,i_0_160,i_0_15,i_0_18,i_0_19]) ).
cnf(i_0_322,plain,
~ less_or_equal(delta_2(delta_1(half(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_160,i_0_102,i_0_15,i_0_18,i_0_19,i_0_20]) ).
cnf(i_0_324,plain,
~ less_or_equal(delta_1(delta_1(half(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_160,i_0_102,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21]) ).
cnf(i_0_326,plain,
~ less_or_equal(half(delta_1(half(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_160,i_0_102,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_328,plain,
~ less_or_equal(minimum(delta_1(half(epsilon_0)),delta_1(half(epsilon_0))),n0),
inference(scs_inference,[],[i_0_23,i_0_160,i_0_102,i_0_15,i_0_18,i_0_19,i_0_20,i_0_21,i_0_22,i_0_17]) ).
cnf(c_0_36,axiom,
( less_or_equal(X1,X2)
| ~ less_or_equal(X1,minimum(X2,X3)) ),
i_0_18 ).
cnf(c_0_37,hypothesis,
( less_or_equal(X1,n0)
| less_or_equal(absolute(add(xs(X1),negate(a_real_number))),X1) ),
i_0_15 ).
cnf(c_0_38,negated_conjecture,
( less_or_equal(X1,n0)
| ~ less_or_equal(add(absolute(add(f(xs(X1)),negate(f(a_real_number)))),absolute(add(g(xs(X1)),negate(g(a_real_number))))),epsilon_0) ),
i_0_12 ).
cnf(c_0_39,axiom,
( less_or_equal(add(X1,X2),X3)
| ~ less_or_equal(X1,half(X3))
| ~ less_or_equal(X2,half(X3)) ),
i_0_16 ).
cnf(c_0_40,hypothesis,
( less_or_equal(X1,n0)
| less_or_equal(absolute(add(g(X2),negate(g(a_real_number)))),X1)
| ~ less_or_equal(absolute(add(X2,negate(a_real_number))),delta_2(X1)) ),
i_0_13 ).
cnf(c_0_41,hypothesis,
( less_or_equal(absolute(add(xs(minimum(X1,X2)),negate(a_real_number))),X1)
| less_or_equal(minimum(X1,X2),n0) ),
inference(spm,[status(thm)],[c_0_36,c_0_37]) ).
cnf(c_0_42,axiom,
( less_or_equal(X1,X2)
| ~ less_or_equal(X1,minimum(X3,X2)) ),
i_0_19 ).
cnf(c_0_43,negated_conjecture,
( less_or_equal(X1,n0)
| ~ less_or_equal(absolute(add(g(xs(X1)),negate(g(a_real_number)))),half(epsilon_0))
| ~ less_or_equal(absolute(add(f(xs(X1)),negate(f(a_real_number)))),half(epsilon_0)) ),
inference(spm,[status(thm)],[c_0_38,c_0_39]) ).
cnf(c_0_44,hypothesis,
( less_or_equal(absolute(add(g(xs(minimum(delta_2(X1),X2))),negate(g(a_real_number)))),X1)
| less_or_equal(minimum(delta_2(X1),X2),n0)
| less_or_equal(X1,n0) ),
inference(spm,[status(thm)],[c_0_40,c_0_41]) ).
cnf(c_0_45,hypothesis,
( less_or_equal(X1,n0)
| less_or_equal(absolute(add(f(X2),negate(f(a_real_number)))),X1)
| ~ less_or_equal(absolute(add(X2,negate(a_real_number))),delta_1(X1)) ),
i_0_14 ).
cnf(c_0_46,hypothesis,
( less_or_equal(absolute(add(xs(minimum(X1,X2)),negate(a_real_number))),X2)
| less_or_equal(minimum(X1,X2),n0) ),
inference(spm,[status(thm)],[c_0_42,c_0_37]) ).
cnf(c_0_47,negated_conjecture,
( less_or_equal(minimum(delta_2(half(epsilon_0)),X1),n0)
| less_or_equal(half(epsilon_0),n0)
| ~ less_or_equal(absolute(add(f(xs(minimum(delta_2(half(epsilon_0)),X1))),negate(f(a_real_number)))),half(epsilon_0)) ),
inference(spm,[status(thm)],[c_0_43,c_0_44]) ).
cnf(c_0_48,hypothesis,
( less_or_equal(absolute(add(f(xs(minimum(X1,delta_1(X2)))),negate(f(a_real_number)))),X2)
| less_or_equal(minimum(X1,delta_1(X2)),n0)
| less_or_equal(X2,n0) ),
inference(spm,[status(thm)],[c_0_45,c_0_46]) ).
cnf(c_0_49,axiom,
( less_or_equal(X1,n0)
| less_or_equal(X2,n0)
| ~ less_or_equal(minimum(X1,X2),n0) ),
i_0_17 ).
cnf(c_0_50,negated_conjecture,
( less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0)
| less_or_equal(half(epsilon_0),n0) ),
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
cnf(c_0_51,hypothesis,
( less_or_equal(X1,n0)
| ~ less_or_equal(delta_2(X1),n0) ),
i_0_20 ).
cnf(c_0_52,hypothesis,
( less_or_equal(X1,n0)
| ~ less_or_equal(delta_1(X1),n0) ),
i_0_21 ).
cnf(c_0_53,axiom,
( less_or_equal(X1,n0)
| ~ less_or_equal(half(X1),n0) ),
i_0_22 ).
cnf(c_0_54,negated_conjecture,
less_or_equal(half(epsilon_0),n0),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_49,c_0_50]),c_0_51]),c_0_52]) ).
cnf(c_0_55,hypothesis,
~ less_or_equal(epsilon_0,n0),
i_0_23 ).
cnf(c_0_56,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_53,c_0_54]),c_0_55]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ANA003-4 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.32 % Computer : n023.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue May 5 10:35:08 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 95.91/79.23 % Version : CSE_E---1.7
% 95.91/79.23 % Problem : theBenchmark.p
% 95.91/79.23 % SZS status Unsatisfiable for theBenchmark.p
% 95.91/79.23 % SZS output start CNFRefutation
% See solution above
% 98.02/81.39 % Total time : 78.885s
%------------------------------------------------------------------------------