%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : ANA004-4 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n012.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 : 600s
% DateTime : Thu Jul 14 19:28:35 EDT 2022
% Result : Unsatisfiable 0.55s 0.72s
% Output : Refutation 0.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 13
% Syntax : Number of clauses : 45 ( 13 unt; 17 nHn; 45 RR)
% Number of literals : 94 ( 0 equ; 34 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( ~ less_or_equal(add(absolute(u),absolute(v)),w)
| less_or_equal(absolute(add(u,v)),w) ),
file('ANA004-4.p',unknown),
[] ).
cnf(2,axiom,
( ~ less_or_equal(u,minimum(v,w))
| less_or_equal(u,v) ),
file('ANA004-4.p',unknown),
[] ).
cnf(3,axiom,
( ~ less_or_equal(u,minimum(v,w))
| less_or_equal(u,w) ),
file('ANA004-4.p',unknown),
[] ).
cnf(4,axiom,
( ~ less_or_equal(minimum(u,v),n0)
| less_or_equal(v,n0)
| less_or_equal(u,n0) ),
file('ANA004-4.p',unknown),
[] ).
cnf(5,axiom,
( ~ less_or_equal(u,half(v))
| ~ less_or_equal(w,half(v))
| less_or_equal(add(w,u),v) ),
file('ANA004-4.p',unknown),
[] ).
cnf(6,axiom,
( ~ less_or_equal(half(u),n0)
| less_or_equal(u,n0) ),
file('ANA004-4.p',unknown),
[] ).
cnf(7,axiom,
( ~ less_or_equal(delta_1(u),n0)
| less_or_equal(u,n0) ),
file('ANA004-4.p',unknown),
[] ).
cnf(8,axiom,
( ~ less_or_equal(delta_2(u),n0)
| less_or_equal(u,n0) ),
file('ANA004-4.p',unknown),
[] ).
cnf(9,axiom,
( ~ less_or_equal(absolute(add(u,negate(a_real_number))),delta_1(v))
| less_or_equal(v,n0)
| less_or_equal(absolute(add(f(u),negate(f(a_real_number)))),v) ),
file('ANA004-4.p',unknown),
[] ).
cnf(10,axiom,
( ~ less_or_equal(absolute(add(u,negate(a_real_number))),delta_2(v))
| less_or_equal(v,n0)
| less_or_equal(absolute(add(g(u),negate(g(a_real_number)))),v) ),
file('ANA004-4.p',unknown),
[] ).
cnf(11,axiom,
~ less_or_equal(epsilon_0,n0),
file('ANA004-4.p',unknown),
[] ).
cnf(12,axiom,
( less_or_equal(u,n0)
| less_or_equal(absolute(add(xs(u),negate(a_real_number))),u) ),
file('ANA004-4.p',unknown),
[] ).
cnf(13,axiom,
( ~ less_or_equal(absolute(add(add(f(xs(u)),negate(f(a_real_number))),add(g(xs(u)),negate(g(a_real_number))))),epsilon_0)
| less_or_equal(u,n0) ),
file('ANA004-4.p',unknown),
[] ).
cnf(15,plain,
( less_or_equal(minimum(u,v),n0)
| less_or_equal(absolute(add(xs(minimum(u,v)),negate(a_real_number))),u) ),
inference(res,[status(thm),theory(equality)],[12,2]),
[iquote('0:Res:12.1,2.0')] ).
cnf(16,plain,
( less_or_equal(minimum(u,v),n0)
| less_or_equal(absolute(add(xs(minimum(u,v)),negate(a_real_number))),v) ),
inference(res,[status(thm),theory(equality)],[12,3]),
[iquote('0:Res:12.1,3.0')] ).
cnf(19,plain,
( ~ less_or_equal(absolute(u),half(v))
| ~ less_or_equal(absolute(w),half(v))
| less_or_equal(absolute(add(w,u)),v) ),
inference(res,[status(thm),theory(equality)],[5,1]),
[iquote('0:Res:5.2,1.0')] ).
cnf(37,plain,
( ~ less_or_equal(absolute(add(u,negate(a_real_number))),delta_1(minimum(v,w)))
| less_or_equal(minimum(v,w),n0)
| less_or_equal(absolute(add(f(u),negate(f(a_real_number)))),v) ),
inference(res,[status(thm),theory(equality)],[9,2]),
[iquote('0:Res:9.2,2.0')] ).
cnf(61,plain,
( ~ less_or_equal(absolute(add(g(xs(u)),negate(g(a_real_number)))),half(epsilon_0))
| ~ less_or_equal(absolute(add(f(xs(u)),negate(f(a_real_number)))),half(epsilon_0))
| less_or_equal(u,n0) ),
inference(res,[status(thm),theory(equality)],[19,13]),
[iquote('0:Res:19.2,13.0')] ).
cnf(181,plain,
( less_or_equal(delta_1(minimum(u,v)),n0)
| less_or_equal(minimum(u,v),n0)
| less_or_equal(absolute(add(f(xs(delta_1(minimum(u,v)))),negate(f(a_real_number)))),u) ),
inference(res,[status(thm),theory(equality)],[12,37]),
[iquote('0:Res:12.1,37.0')] ).
cnf(191,plain,
( less_or_equal(minimum(u,v),n0)
| less_or_equal(absolute(add(f(xs(delta_1(minimum(u,v)))),negate(f(a_real_number)))),u) ),
inference(mrr,[status(thm)],[181,7]),
[iquote('0:MRR:181.0,7.0')] ).
cnf(193,plain,
( less_or_equal(minimum(minimum(u,v),w),n0)
| less_or_equal(absolute(add(f(xs(delta_1(minimum(minimum(u,v),w)))),negate(f(a_real_number)))),v) ),
inference(res,[status(thm),theory(equality)],[191,3]),
[iquote('0:Res:191.1,3.0')] ).
cnf(297,plain,
( ~ less_or_equal(absolute(add(xs(u),negate(a_real_number))),delta_1(half(epsilon_0)))
| ~ less_or_equal(absolute(add(g(xs(u)),negate(g(a_real_number)))),half(epsilon_0))
| less_or_equal(half(epsilon_0),n0)
| less_or_equal(u,n0) ),
inference(res,[status(thm),theory(equality)],[9,61]),
[iquote('0:Res:9.2,61.1')] ).
cnf(300,plain,
( ~ less_or_equal(absolute(add(g(xs(delta_1(minimum(minimum(u,half(epsilon_0)),v)))),negate(g(a_real_number)))),half(epsilon_0))
| less_or_equal(minimum(minimum(u,half(epsilon_0)),v),n0)
| less_or_equal(delta_1(minimum(minimum(u,half(epsilon_0)),v)),n0) ),
inference(res,[status(thm),theory(equality)],[193,61]),
[iquote('0:Res:193.1,61.1')] ).
cnf(304,plain,
( ~ less_or_equal(absolute(add(g(xs(delta_1(minimum(minimum(u,half(epsilon_0)),v)))),negate(g(a_real_number)))),half(epsilon_0))
| less_or_equal(minimum(minimum(u,half(epsilon_0)),v),n0) ),
inference(mrr,[status(thm)],[300,7]),
[iquote('0:MRR:300.2,7.0')] ).
cnf(322,plain,
( ~ less_or_equal(absolute(add(xs(delta_1(minimum(minimum(u,half(epsilon_0)),v))),negate(a_real_number))),delta_2(half(epsilon_0)))
| less_or_equal(half(epsilon_0),n0)
| less_or_equal(minimum(minimum(u,half(epsilon_0)),v),n0) ),
inference(res,[status(thm),theory(equality)],[10,304]),
[iquote('0:Res:10.2,304.0')] ).
cnf(671,plain,
less_or_equal(half(epsilon_0),n0),
inference(spt,[spt(split,[position(s1)])],[322]),
[iquote('1:Spt:322.1')] ).
cnf(672,plain,
less_or_equal(epsilon_0,n0),
inference(res,[status(thm),theory(equality)],[671,6]),
[iquote('1:Res:671.0,6.0')] ).
cnf(673,plain,
$false,
inference(mrr,[status(thm)],[672,11]),
[iquote('1:MRR:672.0,11.0')] ).
cnf(674,plain,
~ less_or_equal(half(epsilon_0),n0),
inference(spt,[spt(split,[position(sa)])],[673,671]),
[iquote('1:Spt:673.0,322.1,671.0')] ).
cnf(675,plain,
( ~ less_or_equal(absolute(add(xs(delta_1(minimum(minimum(u,half(epsilon_0)),v))),negate(a_real_number))),delta_2(half(epsilon_0)))
| less_or_equal(minimum(minimum(u,half(epsilon_0)),v),n0) ),
inference(spt,[spt(split,[position(s2)])],[322]),
[iquote('1:Spt:673.0,322.0,322.2')] ).
cnf(681,plain,
( ~ less_or_equal(absolute(add(xs(u),negate(a_real_number))),delta_1(half(epsilon_0)))
| ~ less_or_equal(absolute(add(g(xs(u)),negate(g(a_real_number)))),half(epsilon_0))
| less_or_equal(u,n0) ),
inference(mrr,[status(thm)],[297,674]),
[iquote('1:MRR:297.2,674.0')] ).
cnf(785,plain,
( ~ less_or_equal(absolute(add(xs(u),negate(a_real_number))),delta_2(half(epsilon_0)))
| ~ less_or_equal(absolute(add(xs(u),negate(a_real_number))),delta_1(half(epsilon_0)))
| less_or_equal(half(epsilon_0),n0)
| less_or_equal(u,n0) ),
inference(res,[status(thm),theory(equality)],[10,681]),
[iquote('1:Res:10.2,681.1')] ).
cnf(797,plain,
( ~ less_or_equal(absolute(add(xs(u),negate(a_real_number))),delta_2(half(epsilon_0)))
| ~ less_or_equal(absolute(add(xs(u),negate(a_real_number))),delta_1(half(epsilon_0)))
| less_or_equal(u,n0) ),
inference(mrr,[status(thm)],[785,674]),
[iquote('1:MRR:785.2,674.0')] ).
cnf(916,plain,
( ~ less_or_equal(absolute(add(xs(minimum(u,delta_1(half(epsilon_0)))),negate(a_real_number))),delta_2(half(epsilon_0)))
| less_or_equal(minimum(u,delta_1(half(epsilon_0))),n0)
| less_or_equal(minimum(u,delta_1(half(epsilon_0))),n0) ),
inference(res,[status(thm),theory(equality)],[16,797]),
[iquote('1:Res:16.1,797.1')] ).
cnf(928,plain,
( ~ less_or_equal(absolute(add(xs(minimum(u,delta_1(half(epsilon_0)))),negate(a_real_number))),delta_2(half(epsilon_0)))
| less_or_equal(minimum(u,delta_1(half(epsilon_0))),n0) ),
inference(obv,[status(thm),theory(equality)],[916]),
[iquote('1:Obv:916.1')] ).
cnf(959,plain,
( less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0)
| less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0) ),
inference(res,[status(thm),theory(equality)],[15,928]),
[iquote('1:Res:15.1,928.0')] ).
cnf(975,plain,
less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0),
inference(obv,[status(thm),theory(equality)],[959]),
[iquote('1:Obv:959.0')] ).
cnf(990,plain,
( less_or_equal(delta_1(half(epsilon_0)),n0)
| less_or_equal(delta_2(half(epsilon_0)),n0) ),
inference(res,[status(thm),theory(equality)],[975,4]),
[iquote('1:Res:975.0,4.0')] ).
cnf(991,plain,
less_or_equal(delta_1(half(epsilon_0)),n0),
inference(spt,[spt(split,[position(s2s1)])],[990]),
[iquote('2:Spt:990.0')] ).
cnf(992,plain,
less_or_equal(half(epsilon_0),n0),
inference(res,[status(thm),theory(equality)],[991,7]),
[iquote('2:Res:991.0,7.0')] ).
cnf(993,plain,
$false,
inference(mrr,[status(thm)],[992,674]),
[iquote('2:MRR:992.0,674.0')] ).
cnf(994,plain,
~ less_or_equal(delta_1(half(epsilon_0)),n0),
inference(spt,[spt(split,[position(s2sa)])],[993,991]),
[iquote('2:Spt:993.0,990.0,991.0')] ).
cnf(995,plain,
less_or_equal(delta_2(half(epsilon_0)),n0),
inference(spt,[spt(split,[position(s2s2)])],[990]),
[iquote('2:Spt:993.0,990.1')] ).
cnf(998,plain,
less_or_equal(half(epsilon_0),n0),
inference(res,[status(thm),theory(equality)],[995,8]),
[iquote('2:Res:995.0,8.0')] ).
cnf(999,plain,
$false,
inference(mrr,[status(thm)],[998,674]),
[iquote('2:MRR:998.0,674.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : ANA004-4 : TPTP v8.1.0. Released v1.0.0.
% 0.12/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n012.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Fri Jul 8 06:57:44 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.55/0.72
% 0.55/0.72 SPASS V 3.9
% 0.55/0.72 SPASS beiseite: Proof found.
% 0.55/0.72 % SZS status Theorem
% 0.55/0.72 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.55/0.72 SPASS derived 881 clauses, backtracked 14 clauses, performed 4 splits and kept 899 clauses.
% 0.55/0.72 SPASS allocated 65828 KBytes.
% 0.55/0.72 SPASS spent 0:00:00.35 on the problem.
% 0.55/0.72 0:00:00.03 for the input.
% 0.55/0.72 0:00:00.00 for the FLOTTER CNF translation.
% 0.55/0.72 0:00:00.03 for inferences.
% 0.55/0.72 0:00:00.00 for the backtracking.
% 0.55/0.72 0:00:00.25 for the reduction.
% 0.55/0.72
% 0.55/0.72
% 0.55/0.72 Here is a proof with depth 9, length 45 :
% 0.55/0.72 % SZS output start Refutation
% See solution above
% 0.55/0.72 Formulae used in the proof : absolute_sum_less_or_equal_sum_of_absolutes2 minimum3 minimum7 minimum9 less_or_equal_sum_of_halves zero_and_half clause_1 clause_2 clause_3 clause_4 clause_5 clause_6 clause_7_1
% 0.55/0.72
%------------------------------------------------------------------------------