%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ANA003-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n004.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 : Sun Sep 27 06:50:13 AM UTC 2026
% Result : Unsatisfiable 225.24s 57.43s
% Output : Refutation 218.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 21
% Syntax : Number of formulae : 451 ( 163 unt; 0 typ; 0 def)
% Number of atoms : 1303 ( 478 equ; 0 cnn)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 4150 ( 651 ~; 400 |; 0 &;3099 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 5 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 19 ( 16 usr; 7 con; 0-2 aty)
% Number of variables : 378 ( 0 ^; 378 !; 0 ?; 378 :)
% Comments :
%------------------------------------------------------------------------------
thf(less_than_decl,type,
less_than: $i > $i > $o ).
thf(n0_decl,type,
n0: $i ).
thf(fp31_decl,type,
fp31: $i > $i ).
thf(absolute_decl,type,
absolute: $i > $i ).
thf(add_decl,type,
add: $i > $i > $i ).
thf(minus_decl,type,
minus: $i > $i ).
thf(a_decl,type,
a: $i ).
thf(f_decl,type,
f: $i > $i ).
thf(l1_decl,type,
l1: $i ).
thf(fp32_decl,type,
fp32: $i > $i ).
thf(g_decl,type,
g: $i > $i ).
thf(l2_decl,type,
l2: $i ).
thf(b_decl,type,
b: $i ).
thf(fp33_decl,type,
fp33: $i > $i ).
thf(minimum_decl,type,
minimum: $i > $i > $i ).
thf(half_decl,type,
half: $i > $i ).
thf(5,negated_conjecture,
b @ ( n0 @ less_than ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_14) ).
thf(22,plain,
b @ ( n0 @ less_than ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(3,negated_conjecture,
! [A: $i] :
( ( A @ fp32 @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_12) ).
thf(27,plain,
! [A: $i] :
( ( A @ fp32 @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(32,plain,
! [A: $i] :
( ( A @ fp32 @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(cnf,[status(esa)],[27]) ).
thf(127,plain,
! [A: $i] :
( ( ( b @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,32]) ).
thf(128,plain,
! [A: $i] :
( ( ( b @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[127]) ).
thf(129,plain,
b @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[128:[bind(A,$thf( b ))]]) ).
thf(145,plain,
! [A: $i] :
( ( ( b @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[129,32]) ).
thf(146,plain,
! [A: $i] :
( ( ( b @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[145]) ).
thf(147,plain,
b @ fp32 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[146:[bind(A,$thf( b @ fp32 ))]]) ).
thf(227,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[147,32]) ).
thf(228,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[227]) ).
thf(229,plain,
b @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[228:[bind(A,$thf( b @ fp32 @ fp32 ))]]) ).
thf(1,negated_conjecture,
! [A: $i] :
( ( A @ fp31 @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_10) ).
thf(23,plain,
! [A: $i] :
( ( A @ fp31 @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(34,plain,
! [A: $i] :
( ( A @ fp31 @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(cnf,[status(esa)],[23]) ).
thf(821,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[229,34]) ).
thf(822,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[821]) ).
thf(823,plain,
b @ fp32 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[822:[bind(A,$thf( b @ fp32 @ fp32 @ fp32 ))]]) ).
thf(19,axiom,
! [A: $i] :
( ( A @ half @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6_2) ).
thf(57,plain,
! [A: $i] :
( ( A @ half @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(58,plain,
! [A: $i] :
( ( A @ half @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(cnf,[status(esa)],[57]) ).
thf(7,negated_conjecture,
! [A: $i] :
( ~ ( b @ ( l2 @ minus @ ( A @ fp33 @ g @ add ) @ absolute @ ( l1 @ minus @ ( A @ fp33 @ f @ add ) @ absolute @ add ) @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_16) ).
thf(26,plain,
! [A: $i] :
( ~ ( b @ ( l2 @ minus @ ( A @ fp33 @ g @ add ) @ absolute @ ( l1 @ minus @ ( A @ fp33 @ f @ add ) @ absolute @ add ) @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(33,plain,
! [A: $i] :
( ~ ( b @ ( l2 @ minus @ ( A @ fp33 @ g @ add ) @ absolute @ ( l1 @ minus @ ( A @ fp33 @ f @ add ) @ absolute @ add ) @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(cnf,[status(esa)],[26]) ).
thf(67,plain,
! [A: $i] :
( ( ( b @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ~ ( b @ ( l2 @ minus @ ( A @ fp33 @ g @ add ) @ absolute @ ( l1 @ minus @ ( A @ fp33 @ f @ add ) @ absolute @ add ) @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,33]) ).
thf(68,plain,
! [A: $i] :
( ( ( b @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ~ ( b @ ( l2 @ minus @ ( A @ fp33 @ g @ add ) @ absolute @ ( l1 @ minus @ ( A @ fp33 @ f @ add ) @ absolute @ add ) @ less_than ) ) ),
inference(simp,[status(thm)],[67]) ).
thf(69,plain,
~ ( b @ ( l2 @ minus @ ( b @ fp33 @ g @ add ) @ absolute @ ( l1 @ minus @ ( b @ fp33 @ f @ add ) @ absolute @ add ) @ less_than ) ),
inference(pattern_uni,[status(thm)],[68:[bind(A,$thf( b ))]]) ).
thf(813,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[147,34]) ).
thf(814,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[813]) ).
thf(815,plain,
b @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[814:[bind(A,$thf( b @ fp32 @ fp32 ))]]) ).
thf(1503,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[815,34]) ).
thf(1504,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1503]) ).
thf(1505,plain,
b @ fp32 @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1504:[bind(A,$thf( b @ fp32 @ fp32 @ fp31 ))]]) ).
thf(10,axiom,
! [A: $i] :
~ ( A @ ( A @ less_than ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_of_less_than) ).
thf(39,plain,
! [A: $i] :
~ ( A @ ( A @ less_than ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(40,plain,
! [A: $i] :
~ ( A @ ( A @ less_than ) ),
inference(polarity_switch,[status(thm)],[39]) ).
thf(130,plain,
! [B: $i,A: $i] :
( ( ( A @ fp32 @ ( n0 @ less_than ) )
!= ( B @ ( B @ less_than ) ) )
| ~ $true
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(paramod_ordered,[status(thm)],[32,40]) ).
thf(131,plain,
! [B: $i,A: $i] :
( ( ( A @ fp32 @ ( n0 @ less_than ) )
!= ( B @ ( B @ less_than ) ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[130]) ).
thf(138,plain,
! [B: $i,A: $i] :
( ( ( A @ fp32 )
!= B )
| ( n0 != B )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[131]) ).
thf(141,plain,
! [A: $i] :
( ( ( A @ fp32 )
!= n0 )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[138]) ).
thf(2610,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1505,141]) ).
thf(2611,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[2610]) ).
thf(2612,plain,
( ( b @ fp32 @ fp32 @ fp31 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[2611:[bind(A,$thf( b @ fp32 @ fp32 @ fp31 @ fp31 ))]]) ).
thf(797,plain,
! [A: $i] :
( ( ( b @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,34]) ).
thf(798,plain,
! [A: $i] :
( ( ( b @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[797]) ).
thf(799,plain,
b @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[798:[bind(A,$thf( b ))]]) ).
thf(1095,plain,
! [A: $i] :
( ( ( b @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[799,34]) ).
thf(1096,plain,
! [A: $i] :
( ( ( b @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1095]) ).
thf(1097,plain,
b @ fp31 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1096:[bind(A,$thf( b @ fp31 ))]]) ).
thf(1233,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1097,34]) ).
thf(1234,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1233]) ).
thf(1235,plain,
b @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1234:[bind(A,$thf( b @ fp31 @ fp31 ))]]) ).
thf(2107,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1235,141]) ).
thf(2108,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[2107]) ).
thf(2109,plain,
( ( b @ fp31 @ fp31 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[2108:[bind(A,$thf( b @ fp31 @ fp31 @ fp31 ))]]) ).
thf(794,plain,
! [A: $i] :
( ( ( b @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[129,34]) ).
thf(795,plain,
! [A: $i] :
( ( ( b @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[794]) ).
thf(796,plain,
b @ fp32 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[795:[bind(A,$thf( b @ fp32 ))]]) ).
thf(1141,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[796,34]) ).
thf(1142,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1141]) ).
thf(1143,plain,
b @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1142:[bind(A,$thf( b @ fp32 @ fp31 ))]]) ).
thf(1623,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1143,40]) ).
thf(1624,plain,
! [A: $i] :
( ( b @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[1623]) ).
thf(1632,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[1624]) ).
thf(1633,plain,
( ( b @ fp32 @ fp31 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[1632]) ).
thf(1092,plain,
! [A: $i] :
( ( ( b @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[799,32]) ).
thf(1093,plain,
! [A: $i] :
( ( ( b @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1092]) ).
thf(1094,plain,
b @ fp31 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1093:[bind(A,$thf( b @ fp31 ))]]) ).
thf(1187,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1094,34]) ).
thf(1188,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1187]) ).
thf(1189,plain,
b @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1188:[bind(A,$thf( b @ fp31 @ fp32 ))]]) ).
thf(1993,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1189,34]) ).
thf(1994,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1993]) ).
thf(1995,plain,
b @ fp31 @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1994:[bind(A,$thf( b @ fp31 @ fp32 @ fp31 ))]]) ).
thf(6,negated_conjecture,
! [A: $i] :
( ( A @ ( a @ minus @ ( A @ fp33 @ add ) @ absolute @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_15) ).
thf(24,plain,
! [A: $i] :
( ( A @ ( a @ minus @ ( A @ fp33 @ add ) @ absolute @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(30,plain,
! [A: $i] :
( ( A @ ( a @ minus @ ( A @ fp33 @ add ) @ absolute @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(cnf,[status(esa)],[24]) ).
thf(331,plain,
! [A: $i] :
( ( ( b @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ ( a @ minus @ ( A @ fp33 @ add ) @ absolute @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,30]) ).
thf(332,plain,
! [A: $i] :
( ( ( b @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ ( a @ minus @ ( A @ fp33 @ add ) @ absolute @ less_than ) ) ),
inference(simp,[status(thm)],[331]) ).
thf(333,plain,
b @ ( a @ minus @ ( b @ fp33 @ add ) @ absolute @ less_than ),
inference(pattern_uni,[status(thm)],[332:[bind(A,$thf( b ))]]) ).
thf(4615,plain,
! [A: $i] :
( ( ( b @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[799,58]) ).
thf(4616,plain,
! [A: $i] :
( ( ( b @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[4615]) ).
thf(4617,plain,
b @ fp31 @ half @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[4616:[bind(A,$thf( b @ fp31 ))]]) ).
thf(4929,plain,
! [A: $i] :
( ( ( b @ fp31 @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4617,141]) ).
thf(4930,plain,
! [A: $i] :
( ( ( b @ fp31 @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[4929]) ).
thf(4931,plain,
( ( b @ fp31 @ half @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[4930:[bind(A,$thf( b @ fp31 @ half ))]]) ).
thf(1209,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1097,141]) ).
thf(1210,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[1209]) ).
thf(1211,plain,
( ( b @ fp31 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[1210:[bind(A,$thf( b @ fp31 @ fp31 ))]]) ).
thf(1071,plain,
! [A: $i] :
( ( ( b @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[799,141]) ).
thf(1072,plain,
! [A: $i] :
( ( ( b @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[1071]) ).
thf(1073,plain,
( ( b @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[1072:[bind(A,$thf( b @ fp31 ))]]) ).
thf(9,axiom,
! [A: $i] :
( ( A @ ( n0 @ add ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_identity) ).
thf(37,plain,
! [A: $i] :
( ( A @ ( n0 @ add ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(38,plain,
! [A: $i] :
( ( A @ ( n0 @ add ) )
= A ),
inference(lifteq,[status(thm)],[37]) ).
thf(414,plain,
! [A: $i] :
( ( ( A @ ( n0 @ add ) )
!= ( a @ minus @ ( b @ fp33 @ add ) ) )
| ( b @ ( A @ absolute @ less_than ) ) ),
inference(paramod_ordered,[status(thm)],[38,333]) ).
thf(435,plain,
! [A: $i] :
( ( A
!= ( a @ minus ) )
| ( ( b @ fp33 )
!= n0 )
| ( b @ ( A @ absolute @ less_than ) ) ),
inference(simp,[status(thm)],[414]) ).
thf(440,plain,
( ( ( b @ fp33 )
!= n0 )
| ( b @ ( a @ minus @ absolute @ less_than ) ) ),
inference(simp,[status(thm)],[435]) ).
thf(1606,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1143,32]) ).
thf(1607,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1606]) ).
thf(1608,plain,
b @ fp32 @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1607:[bind(A,$thf( b @ fp32 @ fp31 @ fp31 ))]]) ).
thf(18,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ add ) )
= ( A @ ( B @ add ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_6_1) ).
thf(55,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ add ) )
= ( A @ ( B @ add ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(56,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ add ) )
= ( A @ ( B @ add ) ) ),
inference(lifteq,[status(thm)],[55]) ).
thf(1138,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[796,32]) ).
thf(1139,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1138]) ).
thf(1140,plain,
b @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1139:[bind(A,$thf( b @ fp32 @ fp31 ))]]) ).
thf(1556,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1140,34]) ).
thf(1557,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1556]) ).
thf(1558,plain,
b @ fp32 @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1557:[bind(A,$thf( b @ fp32 @ fp31 @ fp32 ))]]) ).
thf(3155,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1558,40]) ).
thf(3156,plain,
! [A: $i] :
( ( b @ fp32 @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[3155]) ).
thf(3166,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp32 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[3156]) ).
thf(3175,plain,
( ( b @ fp32 @ fp31 @ fp32 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[3166]) ).
thf(1230,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1097,32]) ).
thf(1231,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1230]) ).
thf(1232,plain,
b @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1231:[bind(A,$thf( b @ fp31 @ fp31 ))]]) ).
thf(2050,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1232,32]) ).
thf(2051,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[2050]) ).
thf(2052,plain,
b @ fp31 @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[2051:[bind(A,$thf( b @ fp31 @ fp31 @ fp32 ))]]) ).
thf(3834,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2052,141]) ).
thf(3835,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[3834]) ).
thf(3836,plain,
( ( b @ fp31 @ fp31 @ fp32 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[3835:[bind(A,$thf( b @ fp31 @ fp31 @ fp32 @ fp32 ))]]) ).
thf(2053,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1232,34]) ).
thf(2054,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[2053]) ).
thf(2055,plain,
b @ fp31 @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[2054:[bind(A,$thf( b @ fp31 @ fp31 @ fp32 ))]]) ).
thf(3913,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2055,141]) ).
thf(3914,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[3913]) ).
thf(3915,plain,
( ( b @ fp31 @ fp31 @ fp32 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[3914:[bind(A,$thf( b @ fp31 @ fp31 @ fp32 @ fp31 ))]]) ).
thf(11,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less_than ) )
| ~ ( C @ ( B @ less_than ) )
| ~ ( B @ ( A @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_less_than) ).
thf(41,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less_than ) )
| ~ ( C @ ( B @ less_than ) )
| ~ ( B @ ( A @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(42,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( A @ less_than ) )
| ~ ( C @ ( B @ less_than ) )
| ~ ( B @ ( A @ less_than ) ) ),
inference(cnf,[status(esa)],[41]) ).
thf(323,plain,
! [A: $i] :
( ( ( b @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ ( a @ minus @ ( A @ fp33 @ add ) @ absolute @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[129,30]) ).
thf(324,plain,
! [A: $i] :
( ( ( b @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ ( a @ minus @ ( A @ fp33 @ add ) @ absolute @ less_than ) ) ),
inference(simp,[status(thm)],[323]) ).
thf(325,plain,
b @ fp32 @ ( a @ minus @ ( b @ fp32 @ fp33 @ add ) @ absolute @ less_than ),
inference(pattern_uni,[status(thm)],[324:[bind(A,$thf( b @ fp32 ))]]) ).
thf(679,plain,
! [A: $i] :
( ( ( b @ fp32 @ ( a @ minus @ ( b @ fp32 @ fp33 @ add ) @ absolute @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[325,40]) ).
thf(680,plain,
! [A: $i] :
( ( b @ fp32 @ ( a @ minus @ ( b @ fp32 @ fp33 @ add ) @ absolute @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[679]) ).
thf(691,plain,
! [A: $i] :
( ( ( b @ fp32 )
!= A )
| ( ( a @ minus @ ( b @ fp32 @ fp33 @ add ) @ absolute )
!= A ) ),
inference(simp,[status(thm)],[680]) ).
thf(702,plain,
( ( a @ minus @ ( b @ fp32 @ fp33 @ add ) @ absolute )
!= ( b @ fp32 ) ),
inference(simp,[status(thm)],[691]) ).
thf(705,plain,
! [A: $i] :
( ( ( A @ ( n0 @ add ) )
!= ( a @ minus @ ( b @ fp32 @ fp33 @ add ) ) )
| ( ( A @ absolute )
!= ( b @ fp32 ) ) ),
inference(paramod_ordered,[status(thm)],[38,702]) ).
thf(707,plain,
! [A: $i] :
( ( A
!= ( a @ minus ) )
| ( ( b @ fp32 @ fp33 )
!= n0 )
| ( ( A @ absolute )
!= ( b @ fp32 ) ) ),
inference(simp,[status(thm)],[705]) ).
thf(709,plain,
( ( ( b @ fp32 @ fp33 )
!= n0 )
| ( ( b @ fp32 )
!= ( a @ minus @ absolute ) ) ),
inference(simp,[status(thm)],[707]) ).
thf(1184,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1094,32]) ).
thf(1185,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1184]) ).
thf(1186,plain,
b @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1185:[bind(A,$thf( b @ fp31 @ fp32 ))]]) ).
thf(1933,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1186,34]) ).
thf(1934,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1933]) ).
thf(1935,plain,
b @ fp31 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1934:[bind(A,$thf( b @ fp31 @ fp32 @ fp32 ))]]) ).
thf(4597,plain,
! [A: $i] :
( ( ( b @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,58]) ).
thf(4598,plain,
! [A: $i] :
( ( ( b @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[4597]) ).
thf(4599,plain,
b @ half @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[4598:[bind(A,$thf( b ))]]) ).
thf(4773,plain,
! [A: $i] :
( ( ( b @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4599,34]) ).
thf(4774,plain,
! [A: $i] :
( ( ( b @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[4773]) ).
thf(4775,plain,
b @ half @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[4774:[bind(A,$thf( b @ half ))]]) ).
thf(2,negated_conjecture,
! [B: $i,A: $i] :
( ( A @ ( l1 @ minus @ ( B @ f @ add ) @ absolute @ less_than ) )
| ~ ( A @ fp31 @ ( a @ minus @ ( B @ add ) @ absolute @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_11) ).
thf(25,plain,
! [B: $i,A: $i] :
( ( A @ ( l1 @ minus @ ( B @ f @ add ) @ absolute @ less_than ) )
| ~ ( A @ fp31 @ ( a @ minus @ ( B @ add ) @ absolute @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(1241,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1097,40]) ).
thf(1242,plain,
! [A: $i] :
( ( b @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[1241]) ).
thf(1246,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[1242]) ).
thf(1254,plain,
( ( b @ fp31 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[1246]) ).
thf(16,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ add ) @ absolute @ less_than ) )
| ~ ( C @ ( B @ absolute @ ( A @ absolute @ add ) @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_17) ).
thf(51,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ add ) @ absolute @ less_than ) )
| ~ ( C @ ( B @ absolute @ ( A @ absolute @ add ) @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(52,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ add ) @ absolute @ less_than ) )
| ~ ( C @ ( B @ absolute @ ( A @ absolute @ add ) @ less_than ) ) ),
inference(cnf,[status(esa)],[51]) ).
thf(1990,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1189,32]) ).
thf(1991,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1990]) ).
thf(1992,plain,
b @ fp31 @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1991:[bind(A,$thf( b @ fp31 @ fp32 @ fp31 ))]]) ).
thf(250,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[229,32]) ).
thf(251,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[250]) ).
thf(252,plain,
b @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[251:[bind(A,$thf( b @ fp32 @ fp32 @ fp32 ))]]) ).
thf(296,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[252,32]) ).
thf(297,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[296]) ).
thf(298,plain,
b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[297:[bind(A,$thf( b @ fp32 @ fp32 @ fp32 @ fp32 ))]]) ).
thf(392,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[298,32]) ).
thf(393,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[392]) ).
thf(394,plain,
b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[393:[bind(A,$thf( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 ))]]) ).
thf(458,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[394,141]) ).
thf(459,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[458]) ).
thf(460,plain,
( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[459:[bind(A,$thf( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 ))]]) ).
thf(2047,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1232,141]) ).
thf(2048,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[2047]) ).
thf(2049,plain,
( ( b @ fp31 @ fp31 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[2048:[bind(A,$thf( b @ fp31 @ fp31 @ fp32 ))]]) ).
thf(13,axiom,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ minimum ) @ less_than ) )
| ~ ( B @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2_2) ).
thf(45,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ minimum ) @ less_than ) )
| ~ ( B @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(46,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ ( A @ minimum ) @ less_than ) )
| ~ ( B @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(cnf,[status(esa)],[45]) ).
thf(824,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[252,34]) ).
thf(825,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[824]) ).
thf(826,plain,
b @ fp32 @ fp32 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[825:[bind(A,$thf( b @ fp32 @ fp32 @ fp32 @ fp32 ))]]) ).
thf(4252,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[826,40]) ).
thf(4253,plain,
! [A: $i] :
( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[4252]) ).
thf(4257,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[4253]) ).
thf(4265,plain,
( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[4257]) ).
thf(4,negated_conjecture,
! [B: $i,A: $i] :
( ( A @ ( l2 @ minus @ ( B @ g @ add ) @ absolute @ less_than ) )
| ~ ( A @ fp32 @ ( a @ minus @ ( B @ add ) @ absolute @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c_13) ).
thf(28,plain,
! [B: $i,A: $i] :
( ( A @ ( l2 @ minus @ ( B @ g @ add ) @ absolute @ less_than ) )
| ~ ( A @ fp32 @ ( a @ minus @ ( B @ add ) @ absolute @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(29,plain,
! [B: $i,A: $i] :
( ( A @ ( l2 @ minus @ ( B @ g @ add ) @ absolute @ less_than ) )
| ~ ( A @ fp32 @ ( a @ minus @ ( B @ add ) @ absolute @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(cnf,[status(esa)],[28]) ).
thf(4576,plain,
! [A: $i] :
( ( ( b @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[129,58]) ).
thf(4577,plain,
! [A: $i] :
( ( ( b @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[4576]) ).
thf(4578,plain,
b @ fp32 @ half @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[4577:[bind(A,$thf( b @ fp32 ))]]) ).
thf(2636,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1505,40]) ).
thf(2637,plain,
! [A: $i] :
( ( b @ fp32 @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[2636]) ).
thf(2643,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[2637]) ).
thf(2650,plain,
( ( b @ fp32 @ fp32 @ fp31 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[2643]) ).
thf(4738,plain,
! [A: $i] :
( ( ( b @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4599,58]) ).
thf(4739,plain,
! [A: $i] :
( ( ( b @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[4738]) ).
thf(4740,plain,
b @ half @ half @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[4739:[bind(A,$thf( b @ half ))]]) ).
thf(5042,plain,
! [A: $i] :
( ( ( b @ half @ half @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4740,40]) ).
thf(5043,plain,
! [A: $i] :
( ( b @ half @ half @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[5042]) ).
thf(5047,plain,
! [A: $i] :
( ( ( b @ half @ half )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[5043]) ).
thf(5059,plain,
( ( b @ half @ half )
!= n0 ),
inference(simp,[status(thm)],[5047]) ).
thf(21,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ add ) @ minus )
= ( B @ minus @ ( A @ minus @ add ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_8) ).
thf(61,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ add ) @ minus )
= ( B @ minus @ ( A @ minus @ add ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(258,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[229,40]) ).
thf(259,plain,
! [A: $i] :
( ( b @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[258]) ).
thf(263,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[259]) ).
thf(265,plain,
( ( b @ fp32 @ fp32 @ fp32 )
!= n0 ),
inference(simp,[status(thm)],[263]) ).
thf(421,plain,
! [A: $i] :
( ( ( b @ ( a @ minus @ ( b @ fp33 @ add ) @ absolute @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[333,40]) ).
thf(422,plain,
! [A: $i] :
( ( b @ ( a @ minus @ ( b @ fp33 @ add ) @ absolute @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[421]) ).
thf(432,plain,
! [A: $i] :
( ( b != A )
| ( ( a @ minus @ ( b @ fp33 @ add ) @ absolute )
!= A ) ),
inference(simp,[status(thm)],[422]) ).
thf(437,plain,
( ( a @ minus @ ( b @ fp33 @ add ) @ absolute )
!= b ),
inference(simp,[status(thm)],[432]) ).
thf(4363,plain,
! [B: $i,A: $i] :
( ( ( B @ ( A @ add ) )
!= ( a @ minus @ ( b @ fp33 @ add ) ) )
| ( ( A @ ( B @ add ) @ absolute )
!= b ) ),
inference(paramod_ordered,[status(thm)],[56,437]) ).
thf(4364,plain,
( ( b @ fp33 @ ( a @ minus @ add ) @ absolute )
!= b ),
inference(pattern_uni,[status(thm)],[4363:[bind(A,$thf( b @ fp33 )),bind(B,$thf( a @ minus ))]]) ).
thf(1117,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[796,141]) ).
thf(1118,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[1117]) ).
thf(1119,plain,
( ( b @ fp32 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[1118:[bind(A,$thf( b @ fp32 @ fp31 ))]]) ).
thf(8,axiom,
! [A: $i] :
( ( n0 @ ( A @ add ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_identity) ).
thf(35,plain,
! [A: $i] :
( ( n0 @ ( A @ add ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(36,plain,
! [A: $i] :
( ( n0 @ ( A @ add ) )
= A ),
inference(lifteq,[status(thm)],[35]) ).
thf(448,plain,
! [A: $i] :
( ( ( n0 @ ( A @ add ) )
!= ( a @ minus @ ( b @ fp33 @ add ) ) )
| ( ( A @ absolute )
!= b ) ),
inference(paramod_ordered,[status(thm)],[36,437]) ).
thf(450,plain,
! [A: $i] :
( ( ( a @ minus )
!= n0 )
| ( A
!= ( b @ fp33 ) )
| ( ( A @ absolute )
!= b ) ),
inference(simp,[status(thm)],[448]) ).
thf(452,plain,
( ( ( a @ minus )
!= n0 )
| ( ( b @ fp33 @ absolute )
!= b ) ),
inference(simp,[status(thm)],[450]) ).
thf(5010,plain,
! [A: $i] :
( ( ( b @ half @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4740,141]) ).
thf(5011,plain,
! [A: $i] :
( ( ( b @ half @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[5010]) ).
thf(5012,plain,
( ( b @ half @ half @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[5011:[bind(A,$thf( b @ half @ half ))]]) ).
thf(268,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[229,141]) ).
thf(269,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[268]) ).
thf(270,plain,
( ( b @ fp32 @ fp32 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[269:[bind(A,$thf( b @ fp32 @ fp32 @ fp32 ))]]) ).
thf(1500,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[815,32]) ).
thf(1501,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1500]) ).
thf(1502,plain,
b @ fp32 @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1501:[bind(A,$thf( b @ fp32 @ fp32 @ fp31 ))]]) ).
thf(1553,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1140,32]) ).
thf(1554,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1553]) ).
thf(1555,plain,
b @ fp32 @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1554:[bind(A,$thf( b @ fp32 @ fp31 @ fp32 ))]]) ).
thf(4538,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[147,58]) ).
thf(4539,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[4538]) ).
thf(4540,plain,
b @ fp32 @ fp32 @ half @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[4539:[bind(A,$thf( b @ fp32 @ fp32 ))]]) ).
thf(5287,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ half @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4540,40]) ).
thf(5288,plain,
! [A: $i] :
( ( b @ fp32 @ fp32 @ half @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[5287]) ).
thf(5295,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ half )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[5288]) ).
thf(5302,plain,
( ( b @ fp32 @ fp32 @ half )
!= n0 ),
inference(simp,[status(thm)],[5295]) ).
thf(2110,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1235,32]) ).
thf(2111,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[2110]) ).
thf(2112,plain,
b @ fp31 @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[2111:[bind(A,$thf( b @ fp31 @ fp31 @ fp31 ))]]) ).
thf(706,plain,
! [A: $i] :
( ( ( n0 @ ( A @ add ) )
!= ( a @ minus @ ( b @ fp32 @ fp33 @ add ) ) )
| ( ( A @ absolute )
!= ( b @ fp32 ) ) ),
inference(paramod_ordered,[status(thm)],[36,702]) ).
thf(708,plain,
! [A: $i] :
( ( ( a @ minus )
!= n0 )
| ( A
!= ( b @ fp32 @ fp33 ) )
| ( ( A @ absolute )
!= ( b @ fp32 ) ) ),
inference(simp,[status(thm)],[706]) ).
thf(710,plain,
( ( ( a @ minus )
!= n0 )
| ( ( b @ fp32 @ fp33 @ absolute )
!= ( b @ fp32 ) ) ),
inference(simp,[status(thm)],[708]) ).
thf(1532,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1140,141]) ).
thf(1533,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[1532]) ).
thf(1534,plain,
( ( b @ fp32 @ fp31 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[1533:[bind(A,$thf( b @ fp32 @ fp31 @ fp32 ))]]) ).
thf(17,axiom,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ add ) @ add ) )
= ( C @ ( B @ add ) @ ( A @ add ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5) ).
thf(53,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ add ) @ add ) )
= ( C @ ( B @ add ) @ ( A @ add ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(2113,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1235,34]) ).
thf(2114,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[2113]) ).
thf(2115,plain,
b @ fp31 @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[2114:[bind(A,$thf( b @ fp31 @ fp31 @ fp31 ))]]) ).
thf(1149,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[796,40]) ).
thf(1150,plain,
! [A: $i] :
( ( b @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[1149]) ).
thf(1156,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[1150]) ).
thf(1160,plain,
( ( b @ fp32 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[1156]) ).
thf(4770,plain,
! [A: $i] :
( ( ( b @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4599,32]) ).
thf(4771,plain,
! [A: $i] :
( ( ( b @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[4770]) ).
thf(4772,plain,
b @ half @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[4771:[bind(A,$thf( b @ half ))]]) ).
thf(4173,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2115,40]) ).
thf(4174,plain,
! [A: $i] :
( ( b @ fp31 @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[4173]) ).
thf(4180,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[4174]) ).
thf(4191,plain,
( ( b @ fp31 @ fp31 @ fp31 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[4180]) ).
thf(3627,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1935,40]) ).
thf(3628,plain,
! [A: $i] :
( ( b @ fp31 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[3627]) ).
thf(3635,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp32 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[3628]) ).
thf(3643,plain,
( ( b @ fp31 @ fp32 @ fp32 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[3635]) ).
thf(1103,plain,
! [A: $i] :
( ( ( b @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[799,40]) ).
thf(1104,plain,
! [A: $i] :
( ( b @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[1103]) ).
thf(1108,plain,
! [A: $i] :
( ( ( b @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[1104]) ).
thf(1114,plain,
( ( b @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[1108]) ).
thf(1517,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[815,40]) ).
thf(1518,plain,
! [A: $i] :
( ( b @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[1517]) ).
thf(1522,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[1518]) ).
thf(1530,plain,
( ( b @ fp32 @ fp32 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[1522]) ).
thf(1930,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1186,32]) ).
thf(1931,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1930]) ).
thf(1932,plain,
b @ fp31 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1931:[bind(A,$thf( b @ fp31 @ fp32 @ fp32 ))]]) ).
thf(1609,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1143,34]) ).
thf(1610,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp31 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[1609]) ).
thf(1611,plain,
b @ fp32 @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[1610:[bind(A,$thf( b @ fp32 @ fp31 @ fp31 ))]]) ).
thf(3305,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1611,40]) ).
thf(3306,plain,
! [A: $i] :
( ( b @ fp32 @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[3305]) ).
thf(3310,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[3306]) ).
thf(3319,plain,
( ( b @ fp32 @ fp31 @ fp31 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[3310]) ).
thf(12,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ minimum ) @ ( n0 @ less_than ) )
| ~ ( B @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2_1) ).
thf(43,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ minimum ) @ ( n0 @ less_than ) )
| ~ ( B @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(44,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ minimum ) @ ( n0 @ less_than ) )
| ~ ( B @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(cnf,[status(esa)],[43]) ).
thf(1927,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1186,141]) ).
thf(1928,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[1927]) ).
thf(1929,plain,
( ( b @ fp31 @ fp32 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[1928:[bind(A,$thf( b @ fp31 @ fp32 @ fp32 ))]]) ).
thf(20,axiom,
! [A: $i] :
( ( A @ half @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_7) ).
thf(59,plain,
! [A: $i] :
( ( A @ half @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(4767,plain,
! [A: $i] :
( ( ( b @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4599,141]) ).
thf(4768,plain,
! [A: $i] :
( ( ( b @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[4767]) ).
thf(4769,plain,
( ( b @ half @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[4768:[bind(A,$thf( b @ half ))]]) ).
thf(4675,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1097,58]) ).
thf(4676,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[4675]) ).
thf(4677,plain,
b @ fp31 @ fp31 @ half @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[4676:[bind(A,$thf( b @ fp31 @ fp31 ))]]) ).
thf(2502,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[823,40]) ).
thf(2503,plain,
! [A: $i] :
( ( b @ fp32 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[2502]) ).
thf(2508,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[2503]) ).
thf(2514,plain,
( ( b @ fp32 @ fp32 @ fp32 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[2508]) ).
thf(3597,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1935,141]) ).
thf(3598,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[3597]) ).
thf(3599,plain,
( ( b @ fp31 @ fp32 @ fp32 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[3598:[bind(A,$thf( b @ fp31 @ fp32 @ fp32 @ fp31 ))]]) ).
thf(54,plain,
! [C: $i,B: $i,A: $i] :
( ( C @ ( B @ ( A @ add ) @ add ) )
= ( C @ ( B @ add ) @ ( A @ add ) ) ),
inference(lifteq,[status(thm)],[53]) ).
thf(15,axiom,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ add ) @ less_than ) )
| ~ ( B @ half @ ( C @ less_than ) )
| ~ ( B @ half @ ( A @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
thf(49,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ add ) @ less_than ) )
| ~ ( B @ half @ ( C @ less_than ) )
| ~ ( B @ half @ ( A @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(3676,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1992,141]) ).
thf(3677,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[3676]) ).
thf(3678,plain,
( ( b @ fp31 @ fp32 @ fp31 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[3677:[bind(A,$thf( b @ fp31 @ fp32 @ fp31 @ fp32 ))]]) ).
thf(3350,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1932,141]) ).
thf(3351,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[3350]) ).
thf(3352,plain,
( ( b @ fp31 @ fp32 @ fp32 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[3351:[bind(A,$thf( b @ fp31 @ fp32 @ fp32 @ fp32 ))]]) ).
thf(2476,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[823,141]) ).
thf(2477,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[2476]) ).
thf(2478,plain,
( ( b @ fp32 @ fp32 @ fp32 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[2477:[bind(A,$thf( b @ fp32 @ fp32 @ fp32 @ fp31 ))]]) ).
thf(447,plain,
! [A: $i] :
( ( ( A @ ( n0 @ add ) )
!= ( a @ minus @ ( b @ fp33 @ add ) ) )
| ( ( A @ absolute )
!= b ) ),
inference(paramod_ordered,[status(thm)],[38,437]) ).
thf(449,plain,
! [A: $i] :
( ( A
!= ( a @ minus ) )
| ( ( b @ fp33 )
!= n0 )
| ( ( A @ absolute )
!= b ) ),
inference(simp,[status(thm)],[447]) ).
thf(451,plain,
( ( ( b @ fp33 )
!= n0 )
| ( ( a @ minus @ absolute )
!= b ) ),
inference(simp,[status(thm)],[449]) ).
thf(5091,plain,
! [A: $i] :
( ( ( b @ half @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4772,141]) ).
thf(5092,plain,
! [A: $i] :
( ( ( b @ half @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[5091]) ).
thf(5093,plain,
( ( b @ half @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[5092:[bind(A,$thf( b @ half @ fp32 ))]]) ).
thf(5173,plain,
! [A: $i] :
( ( ( b @ half @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4775,141]) ).
thf(5174,plain,
! [A: $i] :
( ( ( b @ half @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[5173]) ).
thf(5175,plain,
( ( b @ half @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[5174:[bind(A,$thf( b @ half @ fp31 ))]]) ).
thf(63,plain,
! [A: $i] :
( ( ( b @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[22,40]) ).
thf(64,plain,
! [A: $i] :
( ( b @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[63]) ).
thf(65,plain,
! [A: $i] :
( ( b != A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[64]) ).
thf(66,plain,
b != n0,
inference(simp,[status(thm)],[65]) ).
thf(4848,plain,
! [A: $i] :
( ( ( b @ fp32 @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4578,141]) ).
thf(4849,plain,
! [A: $i] :
( ( ( b @ fp32 @ half @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[4848]) ).
thf(4850,plain,
( ( b @ fp32 @ half @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[4849:[bind(A,$thf( b @ fp32 @ half ))]]) ).
thf(2479,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[823,32]) ).
thf(2480,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[2479]) ).
thf(2481,plain,
b @ fp32 @ fp32 @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[2480:[bind(A,$thf( b @ fp32 @ fp32 @ fp32 @ fp31 ))]]) ).
thf(2007,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1189,40]) ).
thf(2008,plain,
! [A: $i] :
( ( b @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[2007]) ).
thf(2015,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[2008]) ).
thf(2022,plain,
( ( b @ fp31 @ fp32 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[2015]) ).
thf(423,plain,
! [A: $i] :
( ( ( n0 @ ( A @ add ) )
!= ( a @ minus @ ( b @ fp33 @ add ) ) )
| ( b @ ( A @ absolute @ less_than ) ) ),
inference(paramod_ordered,[status(thm)],[36,333]) ).
thf(433,plain,
! [A: $i] :
( ( ( a @ minus )
!= n0 )
| ( A
!= ( b @ fp33 ) )
| ( b @ ( A @ absolute @ less_than ) ) ),
inference(simp,[status(thm)],[423]) ).
thf(438,plain,
( ( ( a @ minus )
!= n0 )
| ( b @ ( b @ fp33 @ absolute @ less_than ) ) ),
inference(simp,[status(thm)],[433]) ).
thf(14,axiom,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ minimum ) @ less_than ) )
| ~ ( B @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2_3) ).
thf(47,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ minimum ) @ less_than ) )
| ~ ( B @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(48,plain,
! [B: $i,A: $i] :
( ( B @ ( B @ ( A @ minimum ) @ less_than ) )
| ~ ( B @ ( n0 @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(cnf,[status(esa)],[47]) ).
thf(293,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[252,141]) ).
thf(294,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[293]) ).
thf(295,plain,
( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[294:[bind(A,$thf( b @ fp32 @ fp32 @ fp32 @ fp32 ))]]) ).
thf(1603,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1143,141]) ).
thf(1604,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[1603]) ).
thf(1605,plain,
( ( b @ fp32 @ fp31 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[1604:[bind(A,$thf( b @ fp32 @ fp31 @ fp31 ))]]) ).
thf(50,plain,
! [C: $i,B: $i,A: $i] :
( ( B @ ( C @ ( A @ add ) @ less_than ) )
| ~ ( B @ half @ ( C @ less_than ) )
| ~ ( B @ half @ ( A @ less_than ) ) ),
inference(cnf,[status(esa)],[49]) ).
thf(3200,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1608,141]) ).
thf(3201,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[3200]) ).
thf(3202,plain,
( ( b @ fp32 @ fp31 @ fp31 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[3201:[bind(A,$thf( b @ fp32 @ fp31 @ fp31 @ fp32 ))]]) ).
thf(4143,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2115,141]) ).
thf(4144,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[4143]) ).
thf(4145,plain,
( ( b @ fp31 @ fp31 @ fp31 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[4144:[bind(A,$thf( b @ fp31 @ fp31 @ fp31 @ fp31 ))]]) ).
thf(3125,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1558,141]) ).
thf(3126,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[3125]) ).
thf(3127,plain,
( ( b @ fp32 @ fp31 @ fp32 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[3126:[bind(A,$thf( b @ fp32 @ fp31 @ fp32 @ fp31 ))]]) ).
thf(468,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[394,32]) ).
thf(469,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ fp32 @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[468]) ).
thf(470,plain,
b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[469:[bind(A,$thf( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 ))]]) ).
thf(2543,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1502,141]) ).
thf(2544,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[2543]) ).
thf(2545,plain,
( ( b @ fp32 @ fp32 @ fp31 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[2544:[bind(A,$thf( b @ fp32 @ fp32 @ fp31 @ fp32 ))]]) ).
thf(31,plain,
! [B: $i,A: $i] :
( ( A @ ( l1 @ minus @ ( B @ f @ add ) @ absolute @ less_than ) )
| ~ ( A @ fp31 @ ( a @ minus @ ( B @ add ) @ absolute @ less_than ) )
| ~ ( A @ ( n0 @ less_than ) ) ),
inference(cnf,[status(esa)],[25]) ).
thf(5203,plain,
! [A: $i] :
( ( ( b @ half @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4775,40]) ).
thf(5204,plain,
! [A: $i] :
( ( b @ half @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[5203]) ).
thf(5215,plain,
! [A: $i] :
( ( ( b @ half @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[5204]) ).
thf(5223,plain,
( ( b @ half @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[5215]) ).
thf(4661,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1094,58]) ).
thf(4662,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( A @ half @ ( n0 @ less_than ) ) ),
inference(simp,[status(thm)],[4661]) ).
thf(4663,plain,
b @ fp31 @ fp32 @ half @ ( n0 @ less_than ),
inference(pattern_uni,[status(thm)],[4662:[bind(A,$thf( b @ fp31 @ fp32 ))]]) ).
thf(5440,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ half @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4663,40]) ).
thf(5441,plain,
! [A: $i] :
( ( b @ fp31 @ fp32 @ half @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[5440]) ).
thf(5450,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ half )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[5441]) ).
thf(5453,plain,
( ( b @ fp31 @ fp32 @ half )
!= n0 ),
inference(simp,[status(thm)],[5450]) ).
thf(3943,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2055,40]) ).
thf(3944,plain,
! [A: $i] :
( ( b @ fp31 @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[3943]) ).
thf(3954,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp32 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[3944]) ).
thf(3961,plain,
( ( b @ fp31 @ fp31 @ fp32 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[3954]) ).
thf(384,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[298,141]) ).
thf(385,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[384]) ).
thf(386,plain,
( ( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[385:[bind(A,$thf( b @ fp32 @ fp32 @ fp32 @ fp32 @ fp32 ))]]) ).
thf(3755,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1995,141]) ).
thf(3756,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[3755]) ).
thf(3757,plain,
( ( b @ fp31 @ fp32 @ fp31 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[3756:[bind(A,$thf( b @ fp31 @ fp32 @ fp31 @ fp31 ))]]) ).
thf(1479,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[815,141]) ).
thf(1480,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[1479]) ).
thf(1481,plain,
( ( b @ fp32 @ fp32 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[1480:[bind(A,$thf( b @ fp32 @ fp32 @ fp31 ))]]) ).
thf(148,plain,
! [A: $i] :
( ( ( b @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[129,40]) ).
thf(149,plain,
! [A: $i] :
( ( b @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[148]) ).
thf(155,plain,
! [A: $i] :
( ( ( b @ fp32 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[149]) ).
thf(158,plain,
( ( b @ fp32 )
!= n0 ),
inference(simp,[status(thm)],[155]) ).
thf(2127,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1235,40]) ).
thf(2128,plain,
! [A: $i] :
( ( b @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[2127]) ).
thf(2135,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[2128]) ).
thf(2142,plain,
( ( b @ fp31 @ fp31 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[2135]) ).
thf(4799,plain,
! [A: $i] :
( ( ( b @ half @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4599,40]) ).
thf(4800,plain,
! [A: $i] :
( ( b @ half @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[4799]) ).
thf(4808,plain,
! [A: $i] :
( ( ( b @ half )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[4800]) ).
thf(4811,plain,
( ( b @ half )
!= n0 ),
inference(simp,[status(thm)],[4808]) ).
thf(235,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[147,40]) ).
thf(236,plain,
! [A: $i] :
( ( b @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[235]) ).
thf(239,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp32 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[236]) ).
thf(242,plain,
( ( b @ fp32 @ fp32 )
!= n0 ),
inference(simp,[status(thm)],[239]) ).
thf(1987,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1189,141]) ).
thf(1988,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[1987]) ).
thf(1989,plain,
( ( b @ fp31 @ fp32 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[1988:[bind(A,$thf( b @ fp31 @ fp32 @ fp31 ))]]) ).
thf(3785,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1995,40]) ).
thf(3786,plain,
! [A: $i] :
( ( b @ fp31 @ fp32 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[3785]) ).
thf(3797,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ fp31 @ fp31 )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[3786]) ).
thf(3804,plain,
( ( b @ fp31 @ fp32 @ fp31 @ fp31 )
!= n0 ),
inference(simp,[status(thm)],[3797]) ).
thf(1163,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1094,141]) ).
thf(1164,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[1163]) ).
thf(1165,plain,
( ( b @ fp31 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[1164:[bind(A,$thf( b @ fp31 @ fp32 ))]]) ).
thf(4880,plain,
! [A: $i] :
( ( ( b @ fp32 @ half @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4578,40]) ).
thf(4881,plain,
! [A: $i] :
( ( b @ fp32 @ half @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[4880]) ).
thf(4889,plain,
! [A: $i] :
( ( ( b @ fp32 @ half )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[4881]) ).
thf(4895,plain,
( ( b @ fp32 @ half )
!= n0 ),
inference(simp,[status(thm)],[4889]) ).
thf(3275,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1611,141]) ).
thf(3276,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp31 @ fp31 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[3275]) ).
thf(3277,plain,
( ( b @ fp32 @ fp31 @ fp31 @ fp31 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[3276:[bind(A,$thf( b @ fp32 @ fp31 @ fp31 @ fp31 ))]]) ).
thf(4064,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[2112,141]) ).
thf(4065,plain,
! [A: $i] :
( ( ( b @ fp31 @ fp31 @ fp31 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[4064]) ).
thf(4066,plain,
( ( b @ fp31 @ fp31 @ fp31 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[4065:[bind(A,$thf( b @ fp31 @ fp31 @ fp31 @ fp32 ))]]) ).
thf(62,plain,
! [B: $i,A: $i] :
( ( B @ minus @ ( A @ minus @ add ) )
= ( B @ ( A @ add ) @ minus ) ),
inference(lifteq,[status(thm)],[61]) ).
thf(4961,plain,
! [A: $i] :
( ( ( b @ fp31 @ half @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[4617,40]) ).
thf(4962,plain,
! [A: $i] :
( ( b @ fp31 @ half @ ( n0 @ less_than ) )
!= ( A @ ( A @ less_than ) ) ),
inference(simp,[status(thm)],[4961]) ).
thf(4970,plain,
! [A: $i] :
( ( ( b @ fp31 @ half )
!= A )
| ( n0 != A ) ),
inference(simp,[status(thm)],[4962]) ).
thf(4977,plain,
( ( b @ fp31 @ half )
!= n0 ),
inference(simp,[status(thm)],[4970]) ).
thf(3050,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 )
| ~ $true ),
inference(paramod_ordered,[status(thm)],[1555,141]) ).
thf(3051,plain,
! [A: $i] :
( ( ( b @ fp32 @ fp31 @ fp32 @ fp32 @ ( n0 @ less_than ) )
!= ( A @ ( n0 @ less_than ) ) )
| ( ( A @ fp32 )
!= n0 ) ),
inference(simp,[status(thm)],[3050]) ).
thf(3052,plain,
( ( b @ fp32 @ fp31 @ fp32 @ fp32 @ fp32 )
!= n0 ),
inference(pattern_uni,[status(thm)],[3051:[bind(A,$thf( b @ fp32 @ fp31 @ fp32 @ fp32 ))]]) ).
thf(64869,plain,
$false,
inference(e,[status(thm)],[823,58,69,2612,2109,1633,1995,333,4931,1211,1073,440,1608,56,3175,3836,3915,42,709,24,1935,37,4775,25,1254,52,702,1992,460,4617,2049,46,325,4265,57,1232,29,4578,2650,5059,147,61,265,4364,1119,452,5012,270,1502,815,33,28,38,229,1555,4740,252,5302,2112,710,1534,53,141,1143,2115,1160,4772,4191,3643,1114,1530,1932,4540,129,2052,41,298,45,4599,32,34,3319,22,44,1929,826,59,4769,4677,2514,27,3599,54,49,2055,3678,3352,2478,451,39,5093,5175,799,66,4850,2481,394,2022,438,35,48,295,1611,1605,50,1186,3202,1235,4145,3127,470,2545,31,5223,5453,3961,43,386,1094,1140,3757,1189,40,26,1481,158,55,23,1558,2142,36,30,51,4663,1097,4811,242,1989,3804,437,1165,796,4895,3277,4066,47,62,1505,4977,3052]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ANA003-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.12 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.25/0.50 % Computer : n004.cluster.edu
% 0.25/0.50 % Model : x86_64 x86_64
% 0.25/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.25/0.50 % Memory : 8046.5625MB
% 0.25/0.50 % OS : Linux 6.8.0-71-generic
% 0.25/0.50 % CPULimit : 300
% 0.25/0.50 % WCLimit : 300
% 0.25/0.50 % DateTime : Sat Sep 26 22:01:51 UTC 2026
% 0.25/0.51 % CPUTime :
% 0.25/0.51 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.34/1.37 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.83/1.67 % [INFO] Parsing done (296ms).
% 1.83/1.69 % [INFO] Running in sequential loop mode.
% 2.93/2.24 % [INFO] eprover registered as external prover.
% 2.93/2.26 % [INFO] Scanning for conjecture ...
% 3.28/2.43 % [INFO] Found a conjecture (or negated_conjecture) and 14 axioms. Running axiom selection ...
% 3.46/2.51 % [INFO] Axiom selection finished. Selected 14 axioms (removed 0 axioms).
% 3.46/2.54 % [INFO] Problem is propositional (TPTP CNF).
% 3.46/2.55 % [INFO] Type checking passed.
% 3.46/2.55 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 225.24/57.42 % External prover 'e' found a proof!
% 225.24/57.42 % [INFO] Killing All external provers ...
% 225.24/57.42 % Time passed: 56702ms (effective reasoning time: 55718ms)
% 225.24/57.43 % Axioms used in derivation (14): axiom_7, axiom_2_2, left_identity, axiom_3, right_identity, axiom_6_2, axiom_5, axiom_2_1, c_17, axiom_6_1, axiom_8, transitivity_of_less_than, reflexivity_of_less_than, axiom_2_3
% 225.24/57.43 % No. of inferences in proof: 451
% 225.24/57.43 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p : 56702 ms resp. 55718 ms w/o parsing
% 218.44/57.64 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 218.44/57.65 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------