%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : ANA004-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 : n020.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 154.66s 121.83s
% Output : CNFRefutation 156.46s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_88)
% Comments :
%------------------------------------------------------------------------------
cnf(clause_7_1,negated_conjecture,
( less_or_equal(X1,n0)
| ~ less_or_equal(absolute(add(add(f(xs(X1)),negate(f(a_real_number))),add(g(xs(X1)),negate(g(a_real_number))))),epsilon_0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_7_1) ).
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(absolute_sum_less_or_equal_sum_of_absolutes2,axiom,
( less_or_equal(absolute(add(X1,X2)),X3)
| ~ less_or_equal(add(absolute(X1),absolute(X2)),X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absolute_sum_less_or_equal_sum_of_absolutes2) ).
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_13,negated_conjecture,
( less_or_equal(X1,n0)
| ~ less_or_equal(absolute(add(add(f(xs(X1)),negate(f(a_real_number))),add(g(xs(X1)),negate(g(a_real_number))))),epsilon_0) ),
clause_7_1,
[final] ).
cnf(i_0_14,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_15,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_16,axiom,
( less_or_equal(absolute(add(X1,X2)),X3)
| ~ less_or_equal(add(absolute(X1),absolute(X2)),X3) ),
absolute_sum_less_or_equal_sum_of_absolutes2,
[final] ).
cnf(i_0_17,hypothesis,
( less_or_equal(X1,n0)
| less_or_equal(absolute(add(xs(X1),negate(a_real_number))),X1) ),
clause_6,
[final] ).
cnf(i_0_18,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_19,axiom,
( less_or_equal(X1,n0)
| less_or_equal(X2,n0)
| ~ less_or_equal(minimum(X1,X2),n0) ),
minimum9,
[final] ).
cnf(i_0_20,axiom,
( less_or_equal(X1,X2)
| ~ less_or_equal(X1,minimum(X2,X3)) ),
minimum3,
[final] ).
cnf(i_0_21,axiom,
( less_or_equal(X1,X3)
| ~ less_or_equal(X1,minimum(X2,X3)) ),
minimum7,
[final] ).
cnf(i_0_22,hypothesis,
( less_or_equal(X1,n0)
| ~ less_or_equal(delta_2(X1),n0) ),
clause_2,
[final] ).
cnf(i_0_23,hypothesis,
( less_or_equal(X1,n0)
| ~ less_or_equal(delta_1(X1),n0) ),
clause_1,
[final] ).
cnf(i_0_24,axiom,
( less_or_equal(X1,n0)
| ~ less_or_equal(half(X1),n0) ),
zero_and_half,
[final] ).
cnf(i_0_25,hypothesis,
~ less_or_equal(epsilon_0,n0),
clause_5,
[final] ).
cnf(i_0_160,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(minimum(n0,X1),X2)),
inference(scs_inference,[],[i_0_25,i_0_88,i_0_17,i_0_20]) ).
cnf(i_0_162,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(X1,minimum(n0,X2))),
inference(scs_inference,[],[i_0_25,i_0_88,i_0_17,i_0_20,i_0_21]) ).
cnf(i_0_164,plain,
~ less_or_equal(delta_2(delta_2(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_88,i_0_74,i_0_17,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_166,plain,
~ less_or_equal(delta_1(delta_2(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_88,i_0_74,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23]) ).
cnf(i_0_168,plain,
~ less_or_equal(half(delta_2(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_88,i_0_74,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23,i_0_24]) ).
cnf(i_0_174,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(minimum(X1,n0),X2)),
inference(scs_inference,[],[i_0_25,i_0_90,i_0_17,i_0_20]) ).
cnf(i_0_176,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(X1,minimum(X2,n0))),
inference(scs_inference,[],[i_0_25,i_0_90,i_0_17,i_0_20,i_0_21]) ).
cnf(i_0_178,plain,
~ less_or_equal(delta_2(delta_1(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_90,i_0_76,i_0_17,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_180,plain,
~ less_or_equal(delta_1(delta_1(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_90,i_0_76,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23]) ).
cnf(i_0_182,plain,
~ less_or_equal(half(delta_1(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_90,i_0_76,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23,i_0_24]) ).
cnf(i_0_194,plain,
~ less_or_equal(half(epsilon_0),minimum(minimum(n0,X1),X2)),
inference(scs_inference,[],[i_0_25,i_0_106,i_0_17,i_0_20]) ).
cnf(i_0_196,plain,
~ less_or_equal(half(epsilon_0),minimum(X1,minimum(n0,X2))),
inference(scs_inference,[],[i_0_25,i_0_106,i_0_17,i_0_20,i_0_21]) ).
cnf(i_0_198,plain,
~ less_or_equal(delta_2(half(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_106,i_0_78,i_0_17,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_200,plain,
~ less_or_equal(delta_1(half(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_106,i_0_78,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23]) ).
cnf(i_0_202,plain,
~ less_or_equal(half(half(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_106,i_0_78,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23,i_0_24]) ).
cnf(i_0_204,plain,
~ less_or_equal(minimum(half(minimum(epsilon_0,epsilon_0)),half(minimum(epsilon_0,epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_106,i_0_78,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23,i_0_24,i_0_19]) ).
cnf(i_0_212,plain,
~ less_or_equal(half(epsilon_0),minimum(minimum(X1,n0),X2)),
inference(scs_inference,[],[i_0_25,i_0_108,i_0_17,i_0_20]) ).
cnf(i_0_214,plain,
~ less_or_equal(half(epsilon_0),minimum(X1,minimum(X2,n0))),
inference(scs_inference,[],[i_0_25,i_0_108,i_0_17,i_0_20,i_0_21]) ).
cnf(i_0_216,plain,
~ less_or_equal(delta_2(delta_2(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_108,i_0_52,i_0_17,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_218,plain,
~ less_or_equal(delta_1(delta_2(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_108,i_0_52,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23]) ).
cnf(i_0_220,plain,
~ less_or_equal(half(delta_2(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_108,i_0_52,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23,i_0_24]) ).
cnf(i_0_222,plain,
~ less_or_equal(minimum(delta_2(delta_2(epsilon_0)),delta_2(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_108,i_0_52,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23,i_0_24,i_0_19]) ).
cnf(i_0_230,plain,
~ less_or_equal(delta_2(delta_1(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_28,i_0_54,i_0_17,i_0_20,i_0_21,i_0_22]) ).
cnf(i_0_232,plain,
~ less_or_equal(delta_1(delta_1(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_28,i_0_54,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23]) ).
cnf(i_0_234,plain,
~ less_or_equal(half(delta_1(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_28,i_0_54,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23,i_0_24]) ).
cnf(i_0_236,plain,
~ less_or_equal(minimum(delta_1(delta_2(epsilon_0)),delta_1(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_25,i_0_28,i_0_54,i_0_17,i_0_20,i_0_21,i_0_22,i_0_23,i_0_24,i_0_19]) ).
cnf(i_0_238,plain,
~ less_or_equal(minimum(half(delta_2(epsilon_0)),half(delta_2(epsilon_0))),n0),
inference(scs_inference,[],[i_0_56,i_0_19]) ).
cnf(i_0_281,plain,
~ less_or_equal(delta_1(half(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_96,i_0_17,i_0_23]) ).
cnf(i_0_436,plain,
~ less_or_equal(epsilon_0,minimum(minimum(X1,minimum(n0,X2)),X3)),
inference(scs_inference,[],[i_0_50,i_0_20]) ).
cnf(i_0_452,plain,
~ less_or_equal(epsilon_0,minimum(minimum(X1,minimum(X2,n0)),X3)),
inference(scs_inference,[],[i_0_228,i_0_20]) ).
cnf(i_0_542,plain,
~ less_or_equal(delta_2(epsilon_0),minimum(minimum(n0,X1),X2)),
inference(scs_inference,[],[i_0_520,i_0_20]) ).
cnf(i_0_1159,plain,
~ less_or_equal(epsilon_0,minimum(minimum(minimum(n0,X1),X2),X3)),
inference(scs_inference,[],[i_0_48,i_0_20]) ).
cnf(i_0_1369,plain,
~ less_or_equal(delta_2(delta_2(epsilon_0)),minimum(n0,X1)),
inference(scs_inference,[],[i_0_52,i_0_20]) ).
cnf(i_0_1477,plain,
~ less_or_equal(delta_1(delta_2(epsilon_0)),minimum(n0,X1)),
inference(scs_inference,[],[i_0_54,i_0_20]) ).
cnf(i_0_1571,plain,
~ less_or_equal(half(delta_2(epsilon_0)),minimum(n0,X1)),
inference(scs_inference,[],[i_0_56,i_0_20]) ).
cnf(i_0_1793,plain,
~ less_or_equal(minimum(delta_2(epsilon_0),delta_2(epsilon_0)),minimum(n0,X1)),
inference(scs_inference,[],[i_0_62,i_0_20]) ).
cnf(i_0_2193,plain,
~ less_or_equal(delta_2(minimum(epsilon_0,epsilon_0)),minimum(n0,X1)),
inference(scs_inference,[],[i_0_74,i_0_20]) ).
cnf(i_0_259,plain,
~ less_or_equal(delta_1(delta_2(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_92,i_0_254,i_0_20,i_0_17,i_0_23]) ).
cnf(i_0_263,plain,
~ less_or_equal(minimum(delta_2(delta_1(epsilon_0)),delta_2(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_92,i_0_254,i_0_32,i_0_20,i_0_17,i_0_23,i_0_14,i_0_19]) ).
cnf(i_0_265,plain,
~ less_or_equal(minimum(epsilon_0,epsilon_0),minimum(X1,minimum(minimum(X2,n0),X3))),
inference(scs_inference,[],[i_0_146,i_0_92,i_0_254,i_0_32,i_0_20,i_0_17,i_0_23,i_0_14,i_0_19,i_0_21]) ).
cnf(i_0_267,plain,
~ less_or_equal(delta_2(delta_2(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_146,i_0_92,i_0_254,i_0_32,i_0_20,i_0_17,i_0_23,i_0_14,i_0_19,i_0_21,i_0_22]) ).
cnf(i_0_269,plain,
~ less_or_equal(half(delta_2(delta_1(epsilon_0))),n0),
inference(scs_inference,[],[i_0_146,i_0_92,i_0_254,i_0_32,i_0_20,i_0_17,i_0_23,i_0_14,i_0_19,i_0_21,i_0_22,i_0_24]) ).
cnf(i_0_271,plain,
~ less_or_equal(minimum(epsilon_0,epsilon_0),minimum(minimum(X1,minimum(X2,n0)),X3)),
inference(scs_inference,[],[i_0_148,i_0_20]) ).
cnf(i_0_285,plain,
~ less_or_equal(minimum(epsilon_0,epsilon_0),minimum(X1,minimum(minimum(n0,X2),X3))),
inference(scs_inference,[],[i_0_128,i_0_96,i_0_254,i_0_17,i_0_23,i_0_20,i_0_21]) ).
cnf(i_0_295,plain,
~ less_or_equal(minimum(epsilon_0,epsilon_0),minimum(minimum(X1,minimum(n0,X2)),X3)),
inference(scs_inference,[],[i_0_130,i_0_20]) ).
cnf(i_0_332,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(minimum(X1,minimum(n0,X2)),X3)),
inference(scs_inference,[],[i_0_162,i_0_20]) ).
cnf(i_0_355,plain,
~ less_or_equal(delta_1(epsilon_0),minimum(minimum(X1,minimum(X2,n0)),X3)),
inference(scs_inference,[],[i_0_176,i_0_20]) ).
cnf(i_0_371,plain,
~ less_or_equal(half(epsilon_0),minimum(X1,minimum(minimum(n0,X2),X3))),
inference(scs_inference,[],[i_0_194,i_0_254,i_0_20,i_0_21]) ).
cnf(i_0_383,plain,
~ less_or_equal(half(epsilon_0),minimum(minimum(X1,minimum(n0,X2)),X3)),
inference(scs_inference,[],[i_0_196,i_0_20]) ).
cnf(i_0_412,plain,
~ less_or_equal(half(epsilon_0),minimum(minimum(X1,minimum(X2,n0)),X3)),
inference(scs_inference,[],[i_0_214,i_0_20]) ).
cnf(i_0_560,plain,
~ less_or_equal(delta_2(epsilon_0),minimum(minimum(minimum(n0,X1),X2),X3)),
inference(scs_inference,[],[i_0_542,i_0_20]) ).
cnf(i_0_672,plain,
~ less_or_equal(epsilon_0,minimum(minimum(minimum(X1,minimum(n0,X2)),X3),X4)),
inference(scs_inference,[],[i_0_436,i_0_20]) ).
cnf(i_0_692,plain,
~ less_or_equal(epsilon_0,minimum(minimum(minimum(X1,minimum(X2,n0)),X3),X4)),
inference(scs_inference,[],[i_0_452,i_0_20]) ).
cnf(i_0_1383,plain,
~ less_or_equal(delta_2(delta_2(epsilon_0)),minimum(minimum(n0,X1),X2)),
inference(scs_inference,[],[i_0_1369,i_0_20]) ).
cnf(i_0_1497,plain,
~ less_or_equal(delta_1(delta_2(epsilon_0)),minimum(minimum(n0,X1),X2)),
inference(scs_inference,[],[i_0_1477,i_0_20]) ).
cnf(c_0_39,axiom,
( less_or_equal(absolute(add(X1,X2)),X3)
| ~ less_or_equal(add(absolute(X1),absolute(X2)),X3) ),
i_0_16 ).
cnf(c_0_40,axiom,
( less_or_equal(add(X1,X2),X3)
| ~ less_or_equal(X1,half(X3))
| ~ less_or_equal(X2,half(X3)) ),
i_0_18 ).
cnf(c_0_41,axiom,
( less_or_equal(X1,X2)
| ~ less_or_equal(X1,minimum(X2,X3)) ),
i_0_20 ).
cnf(c_0_42,hypothesis,
( less_or_equal(X1,n0)
| less_or_equal(absolute(add(xs(X1),negate(a_real_number))),X1) ),
i_0_17 ).
cnf(c_0_43,negated_conjecture,
( less_or_equal(X1,n0)
| ~ less_or_equal(absolute(add(add(f(xs(X1)),negate(f(a_real_number))),add(g(xs(X1)),negate(g(a_real_number))))),epsilon_0) ),
i_0_13 ).
cnf(c_0_44,plain,
( less_or_equal(absolute(add(X1,X2)),X3)
| ~ less_or_equal(absolute(X2),half(X3))
| ~ less_or_equal(absolute(X1),half(X3)) ),
inference(spm,[status(thm)],[c_0_39,c_0_40]) ).
cnf(c_0_45,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_14 ).
cnf(c_0_46,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_41,c_0_42]) ).
cnf(c_0_47,axiom,
( less_or_equal(X1,X2)
| ~ less_or_equal(X1,minimum(X3,X2)) ),
i_0_21 ).
cnf(c_0_48,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_43,c_0_44]) ).
cnf(c_0_49,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_45,c_0_46]) ).
cnf(c_0_50,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_15 ).
cnf(c_0_51,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_47,c_0_42]) ).
cnf(c_0_52,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_48,c_0_49]) ).
cnf(c_0_53,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_50,c_0_51]) ).
cnf(c_0_54,axiom,
( less_or_equal(X1,n0)
| less_or_equal(X2,n0)
| ~ less_or_equal(minimum(X1,X2),n0) ),
i_0_19 ).
cnf(c_0_55,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_52,c_0_53]) ).
cnf(c_0_56,hypothesis,
( less_or_equal(X1,n0)
| ~ less_or_equal(delta_2(X1),n0) ),
i_0_22 ).
cnf(c_0_57,hypothesis,
( less_or_equal(X1,n0)
| ~ less_or_equal(delta_1(X1),n0) ),
i_0_23 ).
cnf(c_0_58,axiom,
( less_or_equal(X1,n0)
| ~ less_or_equal(half(X1),n0) ),
i_0_24 ).
cnf(c_0_59,negated_conjecture,
less_or_equal(half(epsilon_0),n0),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_55]),c_0_56]),c_0_57]) ).
cnf(c_0_60,hypothesis,
~ less_or_equal(epsilon_0,n0),
i_0_25 ).
cnf(c_0_61,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_58,c_0_59]),c_0_60]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ANA004-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 : n020.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.33 % DateTime : Tue May 5 10:36:34 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 154.66/121.83 % Version : CSE_E---1.7
% 154.66/121.83 % Problem : theBenchmark.p
% 154.66/121.83 % SZS status Unsatisfiable for theBenchmark.p
% 154.66/121.83 % SZS output start CNFRefutation
% See solution above
% 156.46/123.62 % Total time : 121.483s
%------------------------------------------------------------------------------