%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : ANA004-4 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n024.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 : Wed Apr 9 05:37:31 PM UTC 2025
% Result : Unsatisfiable 6.26s 2.56s
% Output : CNFRefutation 6.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 13
% Syntax : Number of formulae : 47 ( 13 unt; 0 typ; 0 def)
% Number of atoms : 97 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 90 ( 40 ~; 50 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 3 con; 0-2 aty)
% Number of variables : 59 ( 59 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ less_or_equal > minimum > add > #nlpp > xs > negate > half > g > f > delta_2 > delta_1 > absolute > n0 > epsilon_0 > a_real_number
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(minimum,type,
minimum: ( $i * $i ) > $i ).
tff(less_or_equal,type,
less_or_equal: ( $i * $i ) > $o ).
tff(epsilon_0,type,
epsilon_0: $i ).
tff(half,type,
half: $i > $i ).
tff(xs,type,
xs: $i > $i ).
tff(f,type,
f: $i > $i ).
tff(delta_2,type,
delta_2: $i > $i ).
tff(g,type,
g: $i > $i ).
tff(absolute,type,
absolute: $i > $i ).
tff(delta_1,type,
delta_1: $i > $i ).
tff(add,type,
add: ( $i * $i ) > $i ).
tff(n0,type,
n0: $i ).
tff(negate,type,
negate: $i > $i ).
tff(a_real_number,type,
a_real_number: $i ).
tff(f_98,axiom,
~ less_or_equal(epsilon_0,n0),
file(unknown,unknown) ).
tff(f_95,axiom,
! [Epsilon,Z] :
( less_or_equal(Epsilon,n0)
| ~ less_or_equal(absolute(add(Z,negate(a_real_number))),delta_2(Epsilon))
| less_or_equal(absolute(add(g(Z),negate(g(a_real_number)))),Epsilon) ),
file(unknown,unknown) ).
tff(f_61,axiom,
! [X,Z,Y] :
( ~ less_or_equal(X,half(Z))
| ~ less_or_equal(Y,half(Z))
| less_or_equal(add(X,Y),Z) ),
file(unknown,unknown) ).
tff(f_32,axiom,
! [X,Y,Z] :
( ~ less_or_equal(add(absolute(X),absolute(Y)),Z)
| less_or_equal(absolute(add(X,Y)),Z) ),
file(unknown,unknown) ).
tff(f_109,axiom,
! [Delta] :
( less_or_equal(Delta,n0)
| ~ less_or_equal(absolute(add(add(f(xs(Delta)),negate(f(a_real_number))),add(g(xs(Delta)),negate(g(a_real_number))))),epsilon_0) ),
file(unknown,unknown) ).
tff(f_67,axiom,
! [X] :
( less_or_equal(X,n0)
| ~ less_or_equal(half(X),n0) ),
file(unknown,unknown) ).
tff(f_103,axiom,
! [Delta] :
( less_or_equal(Delta,n0)
| less_or_equal(absolute(add(xs(Delta),negate(a_real_number))),Delta) ),
file(unknown,unknown) ).
tff(f_44,axiom,
! [Z,X,Y] :
( ~ less_or_equal(Z,minimum(X,Y))
| less_or_equal(Z,Y) ),
file(unknown,unknown) ).
tff(f_38,axiom,
! [Z,X,Y] :
( ~ less_or_equal(Z,minimum(X,Y))
| less_or_equal(Z,X) ),
file(unknown,unknown) ).
tff(f_87,axiom,
! [Epsilon,Z] :
( less_or_equal(Epsilon,n0)
| ~ less_or_equal(absolute(add(Z,negate(a_real_number))),delta_1(Epsilon))
| less_or_equal(absolute(add(f(Z),negate(f(a_real_number)))),Epsilon) ),
file(unknown,unknown) ).
tff(f_52,axiom,
! [X,Y] :
( less_or_equal(X,n0)
| less_or_equal(Y,n0)
| ~ less_or_equal(minimum(X,Y),n0) ),
file(unknown,unknown) ).
tff(f_79,axiom,
! [Epsilon] :
( less_or_equal(Epsilon,n0)
| ~ less_or_equal(delta_2(Epsilon),n0) ),
file(unknown,unknown) ).
tff(f_73,axiom,
! [Epsilon] :
( less_or_equal(Epsilon,n0)
| ~ less_or_equal(delta_1(Epsilon),n0) ),
file(unknown,unknown) ).
tff(c_22,plain,
~ less_or_equal(epsilon_0,n0),
inference(cnfTransformation,[status(thm)],[f_98]) ).
tff(c_20,plain,
! [Z_21,Epsilon_20] :
( less_or_equal(absolute(add(g(Z_21),negate(g(a_real_number)))),Epsilon_20)
| ~ less_or_equal(absolute(add(Z_21,negate(a_real_number))),delta_2(Epsilon_20))
| less_or_equal(Epsilon_20,n0) ),
inference(cnfTransformation,[status(thm)],[f_95]) ).
tff(c_45,plain,
! [X_39,Y_40,Z_41] :
( less_or_equal(add(X_39,Y_40),Z_41)
| ~ less_or_equal(Y_40,half(Z_41))
| ~ less_or_equal(X_39,half(Z_41)) ),
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_2,plain,
! [X_1,Y_2,Z_3] :
( less_or_equal(absolute(add(X_1,Y_2)),Z_3)
| ~ less_or_equal(add(absolute(X_1),absolute(Y_2)),Z_3) ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_58,plain,
! [X_1,Y_2,Z_41] :
( less_or_equal(absolute(add(X_1,Y_2)),Z_41)
| ~ less_or_equal(absolute(Y_2),half(Z_41))
| ~ less_or_equal(absolute(X_1),half(Z_41)) ),
inference(resolution,[status(thm)],[c_45,c_2]) ).
tff(c_332,plain,
! [Delta_81] :
( ~ less_or_equal(absolute(add(add(f(xs(Delta_81)),negate(f(a_real_number))),add(g(xs(Delta_81)),negate(g(a_real_number))))),epsilon_0)
| less_or_equal(Delta_81,n0) ),
inference(cnfTransformation,[status(thm)],[f_109]) ).
tff(c_969,plain,
! [Delta_140] :
( less_or_equal(Delta_140,n0)
| ~ less_or_equal(absolute(add(g(xs(Delta_140)),negate(g(a_real_number)))),half(epsilon_0))
| ~ less_or_equal(absolute(add(f(xs(Delta_140)),negate(f(a_real_number)))),half(epsilon_0)) ),
inference(resolution,[status(thm)],[c_58,c_332]) ).
tff(c_986,plain,
! [Delta_140] :
( less_or_equal(Delta_140,n0)
| ~ less_or_equal(absolute(add(f(xs(Delta_140)),negate(f(a_real_number)))),half(epsilon_0))
| ~ less_or_equal(absolute(add(xs(Delta_140),negate(a_real_number))),delta_2(half(epsilon_0)))
| less_or_equal(half(epsilon_0),n0) ),
inference(resolution,[status(thm)],[c_20,c_969]) ).
tff(c_2216,plain,
less_or_equal(half(epsilon_0),n0),
inference(splitLeft,[status(thm)],[c_986]) ).
tff(c_12,plain,
! [X_15] :
( ~ less_or_equal(half(X_15),n0)
| less_or_equal(X_15,n0) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_2219,plain,
less_or_equal(epsilon_0,n0),
inference(resolution,[status(thm)],[c_2216,c_12]) ).
tff(c_2223,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_22,c_2219]) ).
tff(c_2225,plain,
~ less_or_equal(half(epsilon_0),n0),
inference(splitRight,[status(thm)],[c_986]) ).
tff(c_32,plain,
! [Delta_33] :
( less_or_equal(absolute(add(xs(Delta_33),negate(a_real_number))),Delta_33)
| less_or_equal(Delta_33,n0) ),
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_6,plain,
! [Z_7,Y_9,X_8] :
( less_or_equal(Z_7,Y_9)
| ~ less_or_equal(Z_7,minimum(X_8,Y_9)) ),
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_42,plain,
! [X_8,Y_9] :
( less_or_equal(absolute(add(xs(minimum(X_8,Y_9)),negate(a_real_number))),Y_9)
| less_or_equal(minimum(X_8,Y_9),n0) ),
inference(resolution,[status(thm)],[c_32,c_6]) ).
tff(c_4,plain,
! [Z_4,X_5,Y_6] :
( less_or_equal(Z_4,X_5)
| ~ less_or_equal(Z_4,minimum(X_5,Y_6)) ),
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_41,plain,
! [X_5,Y_6] :
( less_or_equal(absolute(add(xs(minimum(X_5,Y_6)),negate(a_real_number))),X_5)
| less_or_equal(minimum(X_5,Y_6),n0) ),
inference(resolution,[status(thm)],[c_32,c_4]) ).
tff(c_18,plain,
! [Z_19,Epsilon_18] :
( less_or_equal(absolute(add(f(Z_19),negate(f(a_real_number)))),Epsilon_18)
| ~ less_or_equal(absolute(add(Z_19,negate(a_real_number))),delta_1(Epsilon_18))
| less_or_equal(Epsilon_18,n0) ),
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_2226,plain,
! [Delta_249] :
( less_or_equal(Delta_249,n0)
| ~ less_or_equal(absolute(add(f(xs(Delta_249)),negate(f(a_real_number)))),half(epsilon_0))
| ~ less_or_equal(absolute(add(xs(Delta_249),negate(a_real_number))),delta_2(half(epsilon_0))) ),
inference(splitRight,[status(thm)],[c_986]) ).
tff(c_2253,plain,
! [Delta_249] :
( less_or_equal(Delta_249,n0)
| ~ less_or_equal(absolute(add(xs(Delta_249),negate(a_real_number))),delta_2(half(epsilon_0)))
| ~ less_or_equal(absolute(add(xs(Delta_249),negate(a_real_number))),delta_1(half(epsilon_0)))
| less_or_equal(half(epsilon_0),n0) ),
inference(resolution,[status(thm)],[c_18,c_2226]) ).
tff(c_2267,plain,
! [Delta_250] :
( less_or_equal(Delta_250,n0)
| ~ less_or_equal(absolute(add(xs(Delta_250),negate(a_real_number))),delta_2(half(epsilon_0)))
| ~ less_or_equal(absolute(add(xs(Delta_250),negate(a_real_number))),delta_1(half(epsilon_0))) ),
inference(negUnitSimplification,[status(thm)],[c_2225,c_2253]) ).
tff(c_2513,plain,
! [Y_257] :
( ~ less_or_equal(absolute(add(xs(minimum(delta_2(half(epsilon_0)),Y_257)),negate(a_real_number))),delta_1(half(epsilon_0)))
| less_or_equal(minimum(delta_2(half(epsilon_0)),Y_257),n0) ),
inference(resolution,[status(thm)],[c_41,c_2267]) ).
tff(c_2592,plain,
less_or_equal(minimum(delta_2(half(epsilon_0)),delta_1(half(epsilon_0))),n0),
inference(resolution,[status(thm)],[c_42,c_2513]) ).
tff(c_8,plain,
! [X_10,Y_11] :
( ~ less_or_equal(minimum(X_10,Y_11),n0)
| less_or_equal(Y_11,n0)
| less_or_equal(X_10,n0) ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_2596,plain,
( less_or_equal(delta_1(half(epsilon_0)),n0)
| less_or_equal(delta_2(half(epsilon_0)),n0) ),
inference(resolution,[status(thm)],[c_2592,c_8]) ).
tff(c_2597,plain,
less_or_equal(delta_2(half(epsilon_0)),n0),
inference(splitLeft,[status(thm)],[c_2596]) ).
tff(c_16,plain,
! [Epsilon_17] :
( ~ less_or_equal(delta_2(Epsilon_17),n0)
| less_or_equal(Epsilon_17,n0) ),
inference(cnfTransformation,[status(thm)],[f_79]) ).
tff(c_2600,plain,
less_or_equal(half(epsilon_0),n0),
inference(resolution,[status(thm)],[c_2597,c_16]) ).
tff(c_2604,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2225,c_2600]) ).
tff(c_2605,plain,
less_or_equal(delta_1(half(epsilon_0)),n0),
inference(splitRight,[status(thm)],[c_2596]) ).
tff(c_14,plain,
! [Epsilon_16] :
( ~ less_or_equal(delta_1(Epsilon_16),n0)
| less_or_equal(Epsilon_16,n0) ),
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_2609,plain,
less_or_equal(half(epsilon_0),n0),
inference(resolution,[status(thm)],[c_2605,c_14]) ).
tff(c_2613,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2225,c_2609]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ANA004-4 : TPTP v9.0.0. Released v1.0.0.
% 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n024.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Mon Apr 7 14:48:21 EDT 2025
% 0.12/0.34 % CPUTime :
% 6.26/2.56 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.26/2.57
% 6.26/2.57 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------