%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP147^2 : TPTP v9.3.1. Released v7.5.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 : n009.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 : Wed Sep 30 08:06:56 AM UTC 2026
% Result : Theorem 47.15s 11.81s
% Output : Refutation 48.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 194
% Syntax : Number of formulae : 431 ( 88 unt; 0 typ; 2 def)
% Number of atoms : 1424 ( 403 equ; 0 cnn)
% Maximal formula atoms : 11 ( 3 avg)
% Number of connectives : 6410 ( 176 ~; 56 |; 43 &;5561 @)
% ( 0 <=>; 574 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 7 avg)
% Number of types : 3 ( 2 usr)
% Number of type conns : 239 ( 239 >; 0 *; 0 +; 0 <<)
% Number of symbols : 53 ( 50 usr; 10 con; 0-5 aty)
% Number of variables : 804 ( 8 ^; 788 !; 6 ?; 804 :)
% ( 0 !>; 0 ?*; 0 @-; 2 @+)
% Comments :
%------------------------------------------------------------------------------
thf(real_type,type,
real: $tType ).
thf(a_type,type,
a: $tType ).
thf(one_decl,type,
one:
!>[TA: $tType] : $o ).
thf(zero_decl,type,
zero:
!>[TA: $tType] : $o ).
thf(abs_if_decl,type,
abs_if:
!>[TA: $tType] : $o ).
thf(neg_numeral_decl,type,
neg_numeral:
!>[TA: $tType] : $o ).
thf(idom_abs_sgn_decl,type,
idom_abs_sgn:
!>[TA: $tType] : $o ).
thf(zero_neq_one_decl,type,
zero_neq_one:
!>[TA: $tType] : $o ).
thf(ab_group_add_decl,type,
ab_group_add:
!>[TA: $tType] : $o ).
thf(zero_less_one_decl,type,
zero_less_one:
!>[TA: $tType] : $o ).
thf(linordered_idom_decl,type,
linordered_idom:
!>[TA: $tType] : $o ).
thf(linordered_ring_decl,type,
linordered_ring:
!>[TA: $tType] : $o ).
thf(ordere216010020id_add_decl,type,
ordere216010020id_add:
!>[TA: $tType] : $o ).
thf(ordere142940540dd_abs_decl,type,
ordere142940540dd_abs:
!>[TA: $tType] : $o ).
thf(real_V2090557954_space_decl,type,
real_V2090557954_space:
!>[TA: $tType] : $o ).
thf(linord1659791738miring_decl,type,
linord1659791738miring:
!>[TA: $tType] : $o ).
thf(canoni770627133id_add_decl,type,
canoni770627133id_add:
!>[TA: $tType] : $o ).
thf(ordere1818651114id_add_decl,type,
ordere1818651114id_add:
!>[TA: $tType] : $o ).
thf(elemen1815086676c_ball_decl,type,
elemen1815086676c_ball:
!>[TA: $tType] : ( TA > real > ( set @ TA ) ) ).
thf(auto_l1112008849e_ivl0_decl,type,
auto_l1112008849e_ivl0:
!>[TA: $tType] : ( ( TA > TA ) > ( set @ TA ) > TA > ( set @ real ) ) ).
thf(auto_ll_on_flow0_decl,type,
auto_ll_on_flow0:
!>[TA: $tType] : ( ( TA > TA ) > ( set @ TA ) > TA > real > TA ) ).
thf(abs_abs_decl,type,
abs_abs:
!>[TA: $tType] : ( TA > TA ) ).
thf(one_one_decl,type,
one_one:
!>[TA: $tType] : TA ).
thf(plus_plus_decl,type,
plus_plus:
!>[TA: $tType] : ( TA > TA > TA ) ).
thf(uminus_uminus_decl,type,
uminus_uminus:
!>[TA: $tType] : ( TA > TA ) ).
thf(zero_zero_decl,type,
zero_zero:
!>[TA: $tType] : TA ).
thf(if_decl,type,
if:
!>[TA: $tType] : ( $o > TA > TA > TA ) ).
thf(initia826609931terval_decl,type,
initia826609931terval: ( set @ real ) > $o ).
thf(limit_1335059408_point_decl,type,
limit_1335059408_point:
!>[TA: $tType] : ( ( TA > TA ) > ( set @ TA ) > TA > TA > $o ) ).
thf(limit_1052139091_point_decl,type,
limit_1052139091_point:
!>[TA: $tType] : ( ( TA > TA ) > ( set @ TA ) > TA > TA > $o ) ).
thf(line_open_segment_decl,type,
line_open_segment:
!>[TA: $tType] : ( TA > TA > ( set @ TA ) ) ).
thf(bot_bot_decl,type,
bot_bot:
!>[TA: $tType] : TA ).
thf(ord_less_decl,type,
ord_less:
!>[TA: $tType] : ( TA > TA > $o ) ).
thf(ord_less_eq_decl,type,
ord_less_eq:
!>[TA: $tType] : ( TA > TA > $o ) ).
thf(top_top_decl,type,
top_top:
!>[TA: $tType] : TA ).
thf(period385816147_orbit_decl,type,
period385816147_orbit:
!>[TA: $tType] : ( ( TA > TA ) > ( set @ TA ) > TA > $o ) ).
thf(period1153813292period_decl,type,
period1153813292period:
!>[TA: $tType] : ( ( TA > TA ) > ( set @ TA ) > TA > real ) ).
thf(period862636932_orbit_decl,type,
period862636932_orbit:
!>[TA: $tType] : ( ( TA > TA ) > ( set @ TA ) > TA > $o ) ).
thf(poinca272511729egment_decl,type,
poinca272511729egment:
!>[TA: $tType] : ( ( TA > TA ) > ( set @ TA ) > TA > TA > $o ) ).
thf(collect_decl,type,
collect:
!>[TA: $tType] : ( ( TA > $o ) > ( set @ TA ) ) ).
thf(topolo2071040574ous_on_decl,type,
topolo2071040574ous_on:
!>[TA: $tType,TB: $tType] : ( ( set @ TB ) > ( TB > TA ) > $o ) ).
thf(member_decl,type,
member:
!>[TA: $tType] : ( TA > ( set @ TA ) > $o ) ).
thf(x_decl,type,
x: set @ a ).
thf(a2_decl,type,
a2: a ).
thf(b_decl,type,
b: a ).
thf(f_decl,type,
f: a > a ).
thf(p_decl,type,
p: a ).
thf(thesisa_decl,type,
thesisa: $o ).
thf(x2_decl,type,
x2: a ).
thf(sk3_decl,type,
sk3: real ).
thf(sk4_decl,type,
sk4: a > real ).
thf(sk3_def,definition,
( sk3
= ( @+[A: real] :
~ ( ( ord_less @ real @ ( zero_zero @ real ) @ A )
=> ! [B: a > real] :
( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ A ) @ B )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ C @ ( B @ C ) ) @ ( line_open_segment @ a @ a2 @ b ) ) )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( ord_less @ real @ ( abs_abs @ real @ ( B @ C ) ) @ ( one_one @ real ) ) )
=> ( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ A ) @ B )
=> ( ( B @ p )
!= ( zero_zero @ real ) ) ) ) ) ) ) ) ) ).
thf(sk4_def,definition,
( sk4
= ( @+[A: a > real] :
~ ( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ sk3 ) @ A )
=> ( ! [B: a] :
( ( member @ a @ B @ ( elemen1815086676c_ball @ a @ p @ sk3 ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ B @ ( A @ B ) ) @ ( line_open_segment @ a @ a2 @ b ) ) )
=> ( ! [B: a] :
( ( member @ a @ B @ ( elemen1815086676c_ball @ a @ p @ sk3 ) )
=> ( ord_less @ real @ ( abs_abs @ real @ ( A @ B ) ) @ ( one_one @ real ) ) )
=> ( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ sk3 ) @ A )
=> ( ( A @ p )
!= ( zero_zero @ real ) ) ) ) ) ) ) ) ).
thf(152,axiom,
! [A: real,B: a] :
( ~ ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A )
= ( zero_zero @ a ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_76_local_Orev_Oflow__undefined0) ).
thf(645,plain,
! [A: real,B: a] :
( ~ ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A )
= ( zero_zero @ a ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[152]) ).
thf(64,axiom,
ordere1818651114id_add @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oordered__cancel__comm__monoid__add) ).
thf(347,plain,
ordere1818651114id_add @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(102,axiom,
one @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oone_11) ).
thf(500,plain,
one @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).
thf(21,axiom,
! [TA: $tType] :
( ( one @ TA )
=> ( one @ ( set @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Set_Oset___Groups_Oone) ).
thf(235,plain,
! [TA: $tType] :
( ( one @ TA )
=> ( one @ ( set @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(236,plain,
! [TA: $tType] :
( ~ ( one @ TA )
| ( one @ ( set @ TA ) ) ),
inference(cnf,[status(esa)],[235]) ).
thf(828,plain,
! [TA: $tType] :
( ~ $true
| ( one @ ( set @ TA ) )
| ( ( one @ real )
!= ( one @ TA ) ) ),
inference(paramod_ordered,[status(thm)],[500,236]) ).
thf(829,plain,
! [TA: $tType] :
( ( one @ ( set @ TA ) )
| ( ( one @ real )
!= ( one @ TA ) ) ),
inference(simp,[status(thm)],[828]) ).
thf(830,plain,
one @ ( set @ real ),
inference(pattern_uni,[status(thm)],[829:[bind_type(TA,$thf( real ))]]) ).
thf(831,plain,
! [TA: $tType] :
( ~ $true
| ( one @ ( set @ TA ) )
| ( ( one @ ( set @ real ) )
!= ( one @ TA ) ) ),
inference(paramod_ordered,[status(thm)],[830,236]) ).
thf(832,plain,
! [TA: $tType] :
( ( one @ ( set @ TA ) )
| ( ( one @ ( set @ real ) )
!= ( one @ TA ) ) ),
inference(simp,[status(thm)],[831]) ).
thf(833,plain,
one @ ( set @ ( set @ real ) ),
inference(pattern_uni,[status(thm)],[832:[bind_type(TA,$thf( set @ real ))]]) ).
thf(841,plain,
! [TA: $tType] :
( ~ $true
| ( one @ ( set @ TA ) )
| ( ( one @ ( set @ ( set @ real ) ) )
!= ( one @ TA ) ) ),
inference(paramod_ordered,[status(thm)],[833,236]) ).
thf(842,plain,
! [TA: $tType] :
( ( one @ ( set @ TA ) )
| ( ( one @ ( set @ ( set @ real ) ) )
!= ( one @ TA ) ) ),
inference(simp,[status(thm)],[841]) ).
thf(843,plain,
one @ ( set @ ( set @ ( set @ real ) ) ),
inference(pattern_uni,[status(thm)],[842:[bind_type(TA,$thf( set @ ( set @ real ) ))]]) ).
thf(844,plain,
! [TA: $tType] :
( ~ $true
| ( one @ ( set @ TA ) )
| ( ( one @ ( set @ ( set @ ( set @ real ) ) ) )
!= ( one @ TA ) ) ),
inference(paramod_ordered,[status(thm)],[843,236]) ).
thf(845,plain,
! [TA: $tType] :
( ( one @ ( set @ TA ) )
| ( ( one @ ( set @ ( set @ ( set @ real ) ) ) )
!= ( one @ TA ) ) ),
inference(simp,[status(thm)],[844]) ).
thf(846,plain,
one @ ( set @ ( set @ ( set @ ( set @ real ) ) ) ),
inference(pattern_uni,[status(thm)],[845:[bind_type(TA,$thf( set @ ( set @ ( set @ real ) ) ))]]) ).
thf(27,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ A )
!= ( zero_zero @ a ) )
=> ( period862636932_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_86_rev_Oclosed__orbit__periodic) ).
thf(249,plain,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ A )
!= ( zero_zero @ a ) )
=> ( period862636932_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(160,axiom,
! [A: a,B: real] :
( ( auto_ll_on_flow0 @ a @ f @ x @ A @ B )
= ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ ( uminus_uminus @ real @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_141_rev_Orev__eq__flow) ).
thf(666,plain,
! [A: a,B: real] :
( ( auto_ll_on_flow0 @ a @ f @ x @ A @ B )
= ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ ( uminus_uminus @ real @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[160]) ).
thf(165,axiom,
! [A: a] :
( ( ( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
& ( member @ a @ A @ x ) )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ ( zero_zero @ real ) )
= A ) )
& ( ~ ( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
& ( member @ a @ A @ x ) )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ ( zero_zero @ real ) )
= ( zero_zero @ a ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_92_local_Orev_Oflow__initial__time__if) ).
thf(683,plain,
! [A: a] :
( ( ( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
& ( member @ a @ A @ x ) )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ ( zero_zero @ real ) )
= A ) )
& ( ~ ( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
& ( member @ a @ A @ x ) )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ ( zero_zero @ real ) )
= ( zero_zero @ a ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[165]) ).
thf(36,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( abs_abs @ TA @ ( uminus_uminus @ TA @ A ) )
= ( abs_abs @ TA @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_abs__minus__cancel) ).
thf(276,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( abs_abs @ TA @ ( uminus_uminus @ TA @ A ) )
= ( abs_abs @ TA @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(48,axiom,
initia826609931terval @ ( top_top @ ( set @ real ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_137_interval__axioms) ).
thf(308,plain,
initia826609931terval @ ( top_top @ ( set @ real ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(26,axiom,
! [TA: $tType] :
( ( ordere1818651114id_add @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less @ TA @ B @ C )
=> ( ord_less @ TA @ B @ ( plus_plus @ TA @ A @ C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_245_add__strict__increasing2) ).
thf(247,plain,
! [TA: $tType] :
( ( ordere1818651114id_add @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less @ TA @ B @ C )
=> ( ord_less @ TA @ B @ ( plus_plus @ TA @ A @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(5,axiom,
! [TA: $tType] :
( ( neg_numeral @ TA )
=> ! [A: TA,B: TA] :
( ( uminus_uminus @ TA @ ( plus_plus @ TA @ A @ B ) )
= ( plus_plus @ TA @ ( uminus_uminus @ TA @ B ) @ ( uminus_uminus @ TA @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_207_is__num__normalize_I8_J) ).
thf(200,plain,
! [TA: $tType] :
( ( neg_numeral @ TA )
=> ! [A: TA,B: TA] :
( ( uminus_uminus @ TA @ ( plus_plus @ TA @ A @ B ) )
= ( plus_plus @ TA @ ( uminus_uminus @ TA @ B ) @ ( uminus_uminus @ TA @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(201,plain,
! [TA: $tType,B: TA,A: TA] :
( ~ ( neg_numeral @ TA )
| ( ( uminus_uminus @ TA @ ( plus_plus @ TA @ A @ B ) )
= ( plus_plus @ TA @ ( uminus_uminus @ TA @ B ) @ ( uminus_uminus @ TA @ A ) ) ) ),
inference(cnf,[status(esa)],[200]) ).
thf(202,plain,
! [TA: $tType,B: TA,A: TA] :
( ( ( uminus_uminus @ TA @ ( plus_plus @ TA @ A @ B ) )
= ( plus_plus @ TA @ ( uminus_uminus @ TA @ B ) @ ( uminus_uminus @ TA @ A ) ) )
| ~ ( neg_numeral @ TA ) ),
inference(lifteq,[status(thm)],[201]) ).
thf(110,axiom,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( member @ a @ A @ x )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ ( zero_zero @ real ) )
= A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_117_local_Orev_Oflow__initial__time) ).
thf(523,plain,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( member @ a @ A @ x )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ ( zero_zero @ real ) )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[110]) ).
thf(132,axiom,
linord1659791738miring @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Olinordered__nonzero__semiring) ).
thf(582,plain,
linord1659791738miring @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[132]) ).
thf(192,axiom,
! [A: real,B: a > real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ A )
=> ( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ A ) @ B )
=> ( ( ( B @ p )
= ( zero_zero @ real ) )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( ord_less @ real @ ( abs_abs @ real @ ( B @ C ) ) @ ( one_one @ real ) ) )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ C @ ( B @ C ) ) @ ( line_open_segment @ a @ a2 @ b ) ) )
=> thesisa ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_that) ).
thf(762,plain,
! [A: real,B: a > real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ A )
=> ( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ A ) @ B )
=> ( ( ( B @ p )
= ( zero_zero @ real ) )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( ord_less @ real @ ( abs_abs @ real @ ( B @ C ) ) @ ( one_one @ real ) ) )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ C @ ( B @ C ) ) @ ( line_open_segment @ a @ a2 @ b ) ) )
=> thesisa ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[192]) ).
thf(113,axiom,
! [A: real,B: a,C: real] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( ( member @ real @ C @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) ) )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ ( plus_plus @ real @ A @ C ) )
= ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_149_local_Orev_Oflow__trans) ).
thf(533,plain,
! [A: real,B: a,C: real] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( ( member @ real @ C @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) ) )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ ( plus_plus @ real @ A @ C ) )
= ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[113]) ).
thf(119,axiom,
member @ a @ p @ x,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__092_060open_062p_A_092_060in_062_AX_092_060close_062) ).
thf(550,plain,
member @ a @ p @ x,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[119]) ).
thf(97,axiom,
! [A: a,B: a] :
( ( limit_1335059408_point @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
= ( limit_1052139091_point @ a @ f @ x @ A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_127_rev_O_092_060alpha_062__limit__point__eq__rev) ).
thf(472,plain,
! [A: a,B: a] :
( ( limit_1335059408_point @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
= ( limit_1052139091_point @ a @ f @ x @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(168,axiom,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( member @ a @ A @ x )
=> ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ A )
!= ( bot_bot @ ( set @ real ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_152_local_Oexistence__ivl__notempty) ).
thf(698,plain,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( member @ a @ A @ x )
=> ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ A )
!= ( bot_bot @ ( set @ real ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[168]) ).
thf(61,axiom,
ordere142940540dd_abs @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oordered__ab__group__add__abs) ).
thf(340,plain,
ordere142940540dd_abs @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(172,axiom,
zero_less_one @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Ozero__less__one) ).
thf(709,plain,
zero_less_one @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[172]) ).
thf(81,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ( ( abs_abs @ TA @ ( zero_zero @ TA ) )
= ( zero_zero @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_14_abs__zero) ).
thf(417,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ( ( abs_abs @ TA @ ( zero_zero @ TA ) )
= ( zero_zero @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(40,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( abs_abs @ TA @ A )
= A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_195_abs__of__nonneg) ).
thf(288,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( abs_abs @ TA @ A )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(53,axiom,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( ord_less_eq @ TA @ B @ ( zero_zero @ TA ) )
=> ( ord_less @ TA @ ( plus_plus @ TA @ A @ B ) @ ( zero_zero @ TA ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_250_add__neg__nonpos) ).
thf(320,plain,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( ord_less_eq @ TA @ B @ ( zero_zero @ TA ) )
=> ( ord_less @ TA @ ( plus_plus @ TA @ A @ B ) @ ( zero_zero @ TA ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(87,axiom,
! [A: a] :
( ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ A )
= ( bot_bot @ ( set @ real ) ) )
= ( ~ ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
| ~ ( member @ a @ A @ x ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_203_local_Oexistence__ivl__empty__iff) ).
thf(436,plain,
! [A: a] :
( ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ A )
= ( bot_bot @ ( set @ real ) ) )
= ( ~ ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
| ~ ( member @ a @ A @ x ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(177,axiom,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) )
= ( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
& ( member @ a @ A @ x ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_116_local_Orev_Oexistence__ivl__initial__time__iff) ).
thf(724,plain,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) )
= ( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
& ( member @ a @ A @ x ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[177]) ).
thf(127,axiom,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA] :
~ ( ord_less @ TA @ A @ ( zero_zero @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_29_not__less__zero) ).
thf(570,plain,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA] :
~ ( ord_less @ TA @ A @ ( zero_zero @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(70,axiom,
! [TA: $tType] :
( ( zero @ TA )
=> ! [A: TA] :
( ( ( zero_zero @ TA )
= A )
= ( A
= ( zero_zero @ TA ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_24_zero__reorient) ).
thf(372,plain,
! [TA: $tType] :
( ( zero @ TA )
=> ! [A: TA] :
( ( ( zero_zero @ TA )
= A )
= ( A
= ( zero_zero @ TA ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(104,axiom,
! [A: a] :
( ( period862636932_orbit @ a @ f @ x @ A )
=> ( ord_less @ real @ ( zero_zero @ real ) @ ( period1153813292period @ a @ f @ x @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_83_periodic__orbit__period_I1_J) ).
thf(504,plain,
! [A: a] :
( ( period862636932_orbit @ a @ f @ x @ A )
=> ( ord_less @ real @ ( zero_zero @ real ) @ ( period1153813292period @ a @ f @ x @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(135,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ( ( ( period1153813292period @ a @ f @ x @ A )
= ( zero_zero @ real ) )
=> ( ( f @ A )
= ( zero_zero @ a ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_84_closed__orbit__period__zero__fixed__point) ).
thf(587,plain,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ( ( ( period1153813292period @ a @ f @ x @ A )
= ( zero_zero @ real ) )
=> ( ( f @ A )
= ( zero_zero @ a ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[135]) ).
thf(169,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A )
= B )
=> ( member @ real @ ( uminus_uminus @ real @ A ) @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_144_rev_Orecurrence__time__flip__sign_I1_J) ).
thf(702,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A )
= B )
=> ( member @ real @ ( uminus_uminus @ real @ A ) @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[169]) ).
thf(63,axiom,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ( zero_zero @ TA )
= ( plus_plus @ TA @ A @ B ) )
= ( ( A
= ( zero_zero @ TA ) )
& ( B
= ( zero_zero @ TA ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_156_zero__eq__add__iff__both__eq__0) ).
thf(344,plain,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ( zero_zero @ TA )
= ( plus_plus @ TA @ A @ B ) )
= ( ( A
= ( zero_zero @ TA ) )
& ( B
= ( zero_zero @ TA ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(123,axiom,
! [TA: $tType] :
( ( idom_abs_sgn @ TA )
=> ! [A: TA] :
( ( abs_abs @ TA @ ( abs_abs @ TA @ A ) )
= ( abs_abs @ TA @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_21_abs__abs) ).
thf(559,plain,
! [TA: $tType] :
( ( idom_abs_sgn @ TA )
=> ! [A: TA] :
( ( abs_abs @ TA @ ( abs_abs @ TA @ A ) )
= ( abs_abs @ TA @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[123]) ).
thf(141,axiom,
! [A: a,B: real] :
( ( period862636932_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ( uminus_uminus @ ( a > a ) @ f @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B ) )
!= ( zero_zero @ a ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_81_rev_Operiodic__orbit__imp__flow0__regular) ).
thf(606,plain,
! [A: a,B: real] :
( ( period862636932_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ( uminus_uminus @ ( a > a ) @ f @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B ) )
!= ( zero_zero @ a ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[141]) ).
thf(18,axiom,
real_V2090557954_space @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Real__Vector__Spaces_Ometric__space_5) ).
thf(228,plain,
real_V2090557954_space @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(91,axiom,
! [A: a] :
( ~ ( member @ a @ A @ x )
=> ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ A )
= ( bot_bot @ ( set @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_201_local_Oexistence__ivl__undefined) ).
thf(448,plain,
! [A: a] :
( ~ ( member @ a @ A @ x )
=> ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ A )
= ( bot_bot @ ( set @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(31,axiom,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less @ TA @ ( zero_zero @ TA ) @ B )
=> ( ord_less @ TA @ ( zero_zero @ TA ) @ ( plus_plus @ TA @ A @ B ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_249_add__nonneg__pos) ).
thf(261,plain,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less @ TA @ ( zero_zero @ TA ) @ B )
=> ( ord_less @ TA @ ( zero_zero @ TA ) @ ( plus_plus @ TA @ A @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(12,axiom,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ B )
=> ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ ( plus_plus @ TA @ A @ B ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_219_add__nonneg__nonneg) ).
thf(216,plain,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ B )
=> ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ ( plus_plus @ TA @ A @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(98,axiom,
! [A: a] :
( ( ( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
& ( member @ a @ A @ x ) )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( zero_zero @ real ) )
= A ) )
& ( ~ ( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
& ( member @ a @ A @ x ) )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( zero_zero @ real ) )
= ( zero_zero @ a ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_40_local_Oflow__initial__time__if) ).
thf(475,plain,
! [A: a] :
( ( ( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
& ( member @ a @ A @ x ) )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( zero_zero @ real ) )
= A ) )
& ( ~ ( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
& ( member @ a @ A @ x ) )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( zero_zero @ real ) )
= ( zero_zero @ a ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(189,axiom,
abs_if @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Oabs__if) ).
thf(756,plain,
abs_if @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[189]) ).
thf(65,axiom,
! [A: a] :
( ( period862636932_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
& ( ord_less @ real @ ( zero_zero @ real ) @ ( period1153813292period @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_101_rev_Operiodic__orbit__def) ).
thf(348,plain,
! [A: a] :
( ( period862636932_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
& ( ord_less @ real @ ( zero_zero @ real ) @ ( period1153813292period @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(67,axiom,
! [TA: $tType] :
( ( idom_abs_sgn @ TA )
=> ! [A: TA] :
( ( ( abs_abs @ TA @ A )
= ( zero_zero @ TA ) )
= ( A
= ( zero_zero @ TA ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_32_abs__eq__0__iff) ).
thf(353,plain,
! [TA: $tType] :
( ( idom_abs_sgn @ TA )
=> ! [A: TA] :
( ( ( abs_abs @ TA @ A )
= ( zero_zero @ TA ) )
= ( A
= ( zero_zero @ TA ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(139,axiom,
! [A: a,B: a] :
( ( poinca272511729egment @ a @ f @ x @ A @ B )
=> ( poinca272511729egment @ a @ f @ x @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_transversal__segment__reverse) ).
thf(602,plain,
! [A: a,B: a] :
( ( poinca272511729egment @ a @ f @ x @ A @ B )
=> ( poinca272511729egment @ a @ f @ x @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[139]) ).
thf(24,axiom,
idom_abs_sgn @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Oidom__abs__sgn) ).
thf(243,plain,
idom_abs_sgn @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(847,plain,
! [TA: $tType] :
( ~ $true
| ( one @ ( set @ TA ) )
| ( ( one @ ( set @ ( set @ ( set @ ( set @ real ) ) ) ) )
!= ( one @ TA ) ) ),
inference(paramod_ordered,[status(thm)],[846,236]) ).
thf(848,plain,
! [TA: $tType] :
( ( one @ ( set @ TA ) )
| ( ( one @ ( set @ ( set @ ( set @ ( set @ real ) ) ) ) )
!= ( one @ TA ) ) ),
inference(simp,[status(thm)],[847]) ).
thf(849,plain,
one @ ( set @ ( set @ ( set @ ( set @ ( set @ real ) ) ) ) ),
inference(pattern_uni,[status(thm)],[848:[bind_type(TA,$thf( set @ ( set @ ( set @ ( set @ real ) ) ) ))]]) ).
thf(111,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ( ord_less_eq @ real @ ( zero_zero @ real ) @ ( period1153813292period @ a @ f @ x @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_153_closed__orbit__period__nonneg) ).
thf(527,plain,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ( ord_less_eq @ real @ ( zero_zero @ real ) @ ( period1153813292period @ a @ f @ x @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).
thf(7,axiom,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( ord_less_eq @ TA @ B @ C )
=> ( ord_less_eq @ TA @ ( plus_plus @ TA @ B @ A ) @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_222_add__decreasing2) ).
thf(206,plain,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( ord_less_eq @ TA @ B @ C )
=> ( ord_less_eq @ TA @ ( plus_plus @ TA @ B @ A ) @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(180,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
~ ( ord_less @ TA @ ( abs_abs @ TA @ A ) @ ( zero_zero @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_36_abs__not__less__zero) ).
thf(733,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
~ ( ord_less @ TA @ ( abs_abs @ TA @ A ) @ ( zero_zero @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[180]) ).
thf(734,plain,
! [TA: $tType,A: TA] :
( ~ ( ordere142940540dd_abs @ TA )
| ~ ( ord_less @ TA @ ( abs_abs @ TA @ A ) @ ( zero_zero @ TA ) ) ),
inference(cnf,[status(esa)],[733]) ).
thf(15,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( abs_abs @ TA @ A )
= ( uminus_uminus @ TA @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_199_abs__of__nonpos) ).
thf(221,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( abs_abs @ TA @ A )
= ( uminus_uminus @ TA @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(72,axiom,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( member @ a @ A @ x )
=> ( member @ real @ ( zero_zero @ real ) @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_74_local_Orev_Oexistence__ivl__initial__time) ).
thf(380,plain,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( member @ a @ A @ x )
=> ( member @ real @ ( zero_zero @ real ) @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(112,axiom,
! [A: real,B: real,C: a] :
( ( A != B )
=> ( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) )
=> ( ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) )
=> ( ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C @ A )
= ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C @ B ) )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ C )
!= ( zero_zero @ a ) )
=> ( period862636932_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_97_rev_Operiodic__orbitI) ).
thf(529,plain,
! [A: real,B: real,C: a] :
( ( A != B )
=> ( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) )
=> ( ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) )
=> ( ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C @ A )
= ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C @ B ) )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ C )
!= ( zero_zero @ a ) )
=> ( period862636932_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(158,axiom,
! [A: real,B: a,C: real] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( ( member @ real @ C @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ ( auto_ll_on_flow0 @ a @ f @ x @ B @ A ) ) )
=> ( member @ real @ ( plus_plus @ real @ A @ C ) @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_148_local_Oexistence__ivl__trans) ).
thf(661,plain,
! [A: real,B: a,C: real] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( ( member @ real @ C @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ ( auto_ll_on_flow0 @ a @ f @ x @ B @ A ) ) )
=> ( member @ real @ ( plus_plus @ real @ A @ C ) @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[158]) ).
thf(140,axiom,
! [TA: $tType] :
( ( linord1659791738miring @ TA )
=> ~ ( ord_less @ TA @ ( one_one @ TA ) @ ( zero_zero @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_34_not__one__less__zero) ).
thf(604,plain,
! [TA: $tType] :
( ( linord1659791738miring @ TA )
=> ~ ( ord_less @ TA @ ( one_one @ TA ) @ ( zero_zero @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[140]) ).
thf(605,plain,
! [TA: $tType] :
( ~ ( linord1659791738miring @ TA )
| ~ ( ord_less @ TA @ ( one_one @ TA ) @ ( zero_zero @ TA ) ) ),
inference(cnf,[status(esa)],[604]) ).
thf(791,plain,
! [TA: $tType] :
( ~ $true
| ~ ( ord_less @ TA @ ( one_one @ TA ) @ ( zero_zero @ TA ) )
| ( ( linord1659791738miring @ real )
!= ( linord1659791738miring @ TA ) ) ),
inference(paramod_ordered,[status(thm)],[582,605]) ).
thf(792,plain,
! [TA: $tType] :
( ~ ( ord_less @ TA @ ( one_one @ TA ) @ ( zero_zero @ TA ) )
| ( ( linord1659791738miring @ real )
!= ( linord1659791738miring @ TA ) ) ),
inference(simp,[status(thm)],[791]) ).
thf(793,plain,
~ ( ord_less @ real @ ( one_one @ real ) @ ( zero_zero @ real ) ),
inference(pattern_uni,[status(thm)],[792:[bind_type(TA,$thf( real ))]]) ).
thf(69,axiom,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ A )
!= ( zero_zero @ a ) )
=> ~ ! [B: a,C: a] :
( ( member @ a @ A @ ( line_open_segment @ a @ B @ C ) )
=> ~ ( poinca272511729egment @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_41_rev_Otransversal__segment__exists) ).
thf(366,plain,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ A )
!= ( zero_zero @ a ) )
=> ~ ! [B: a,C: a] :
( ( member @ a @ A @ ( line_open_segment @ a @ B @ C ) )
=> ~ ( poinca272511729egment @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(107,axiom,
! [A: a,B: real] :
( ( member @ a @ A @ x )
=> ( ( ( f @ A )
= ( zero_zero @ a ) )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ A @ B )
= A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_16_fixpoint__sol_I2_J) ).
thf(512,plain,
! [A: a,B: real] :
( ( member @ a @ A @ x )
=> ( ( ( f @ A )
= ( zero_zero @ a ) )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ A @ B )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(88,axiom,
! [TA: $tType] :
( ( idom_abs_sgn @ TA )
=> ( ( abs_abs @ TA @ ( one_one @ TA ) )
= ( one_one @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_10_abs__1) ).
thf(439,plain,
! [TA: $tType] :
( ( idom_abs_sgn @ TA )
=> ( ( abs_abs @ TA @ ( one_one @ TA ) )
= ( one_one @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(59,axiom,
! [A: a] :
( ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( bot_bot @ ( set @ real ) ) )
= ( ~ ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
| ~ ( member @ a @ A @ x ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_205_local_Orev_Oexistence__ivl__empty__iff) ).
thf(334,plain,
! [A: a] :
( ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( bot_bot @ ( set @ real ) ) )
= ( ~ ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
| ~ ( member @ a @ A @ x ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(185,axiom,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ A )
= ( zero_zero @ a ) )
=> ( ( period1153813292period @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( zero_zero @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_80_rev_Ofixed__point__imp__closed__orbit__period__zero_I2_J) ).
thf(746,plain,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ A )
= ( zero_zero @ a ) )
=> ( ( period1153813292period @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( zero_zero @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[185]) ).
thf(45,axiom,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ B )
=> ( ord_less @ TA @ ( zero_zero @ TA ) @ ( plus_plus @ TA @ A @ B ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_247_add__pos__nonneg) ).
thf(302,plain,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ B )
=> ( ord_less @ TA @ ( zero_zero @ TA ) @ ( plus_plus @ TA @ A @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(74,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_115_local_Orev_Omem__existence__ivl__iv__defined_I1_J) ).
thf(392,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(85,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( ? [B: real] :
( ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) )
& ( B
!= ( zero_zero @ real ) )
& ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
= A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_94_rev_Oclosed__orbit__def) ).
thf(429,plain,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( ? [B: real] :
( ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) )
& ( B
!= ( zero_zero @ real ) )
& ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
= A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(813,plain,
! [TA: $tType,A: TA] :
( ~ $true
| ~ ( ord_less @ TA @ ( abs_abs @ TA @ A ) @ ( zero_zero @ TA ) )
| ( ( ordere142940540dd_abs @ real )
!= ( ordere142940540dd_abs @ TA ) ) ),
inference(paramod_ordered,[status(thm)],[340,734]) ).
thf(814,plain,
! [TA: $tType,A: TA] :
( ~ ( ord_less @ TA @ ( abs_abs @ TA @ A ) @ ( zero_zero @ TA ) )
| ( ( ordere142940540dd_abs @ real )
!= ( ordere142940540dd_abs @ TA ) ) ),
inference(simp,[status(thm)],[813]) ).
thf(815,plain,
! [A: real] :
~ ( ord_less @ real @ ( abs_abs @ real @ A ) @ ( zero_zero @ real ) ),
inference(pattern_uni,[status(thm)],[814:[bind_type(TA,$thf( real ))]]) ).
thf(19,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less_eq @ TA @ ( abs_abs @ TA @ A ) @ ( zero_zero @ TA ) )
= ( A
= ( zero_zero @ TA ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_193_abs__le__zero__iff) ).
thf(229,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less_eq @ TA @ ( abs_abs @ TA @ A ) @ ( zero_zero @ TA ) )
= ( A
= ( zero_zero @ TA ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(28,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ A )
= ( top_top @ ( set @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_69_closed__orbit__global__existence) ).
thf(252,plain,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ A )
= ( top_top @ ( set @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(3,axiom,
! [TA: $tType] :
( ( neg_numeral @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( plus_plus @ TA @ ( plus_plus @ TA @ A @ B ) @ C )
= ( plus_plus @ TA @ A @ ( plus_plus @ TA @ B @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_211_is__num__normalize_I1_J) ).
thf(195,plain,
! [TA: $tType] :
( ( neg_numeral @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( plus_plus @ TA @ ( plus_plus @ TA @ A @ B ) @ C )
= ( plus_plus @ TA @ A @ ( plus_plus @ TA @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(196,plain,
! [TA: $tType,C: TA,B: TA,A: TA] :
( ~ ( neg_numeral @ TA )
| ( ( plus_plus @ TA @ ( plus_plus @ TA @ A @ B ) @ C )
= ( plus_plus @ TA @ A @ ( plus_plus @ TA @ B @ C ) ) ) ),
inference(cnf,[status(esa)],[195]) ).
thf(197,plain,
! [TA: $tType,C: TA,B: TA,A: TA] :
( ( ( plus_plus @ TA @ ( plus_plus @ TA @ A @ B ) @ C )
= ( plus_plus @ TA @ A @ ( plus_plus @ TA @ B @ C ) ) )
| ~ ( neg_numeral @ TA ) ),
inference(lifteq,[status(thm)],[196]) ).
thf(57,axiom,
! [TA: $tType] :
( ( real_V2090557954_space @ TA )
=> ! [A: TA,B: real] :
( ( ( elemen1815086676c_ball @ TA @ A @ B )
= ( bot_bot @ ( set @ TA ) ) )
= ( ord_less_eq @ real @ B @ ( zero_zero @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_200_ball__eq__empty) ).
thf(329,plain,
! [TA: $tType] :
( ( real_V2090557954_space @ TA )
=> ! [A: TA,B: real] :
( ( ( elemen1815086676c_ball @ TA @ A @ B )
= ( bot_bot @ ( set @ TA ) ) )
= ( ord_less_eq @ real @ B @ ( zero_zero @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(190,axiom,
! [A: a] :
( ( period862636932_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ord_less @ real @ ( zero_zero @ real ) @ ( period1153813292period @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_98_rev_Operiodic__orbit__period_I1_J) ).
thf(757,plain,
! [A: a] :
( ( period862636932_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ord_less @ real @ ( zero_zero @ real ) @ ( period1153813292period @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[190]) ).
thf(120,axiom,
! [TA: $tType] :
( ( real_V2090557954_space @ TA )
=> ! [A: TA,B: real] :
( ( member @ TA @ A @ ( elemen1815086676c_ball @ TA @ A @ B ) )
= ( ord_less @ real @ ( zero_zero @ real ) @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_centre__in__ball) ).
thf(551,plain,
! [TA: $tType] :
( ( real_V2090557954_space @ TA )
=> ! [A: TA,B: real] :
( ( member @ TA @ A @ ( elemen1815086676c_ball @ TA @ A @ B ) )
= ( ord_less @ real @ ( zero_zero @ real ) @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[120]) ).
thf(173,axiom,
! [A: a,B: a] :
( ( poinca272511729egment @ a @ f @ x @ A @ B )
= ( poinca272511729egment @ a @ f @ x @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_19_transversal__segment__commute) ).
thf(710,plain,
! [A: a,B: a] :
( ( poinca272511729egment @ a @ f @ x @ A @ B )
= ( poinca272511729egment @ a @ f @ x @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[173]) ).
thf(55,axiom,
! [TA: $tType] :
( ( idom_abs_sgn @ TA )
=> ! [A: TA] :
( ( abs_abs @ TA @ ( uminus_uminus @ TA @ A ) )
= ( abs_abs @ TA @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_95_abs__minus) ).
thf(324,plain,
! [TA: $tType] :
( ( idom_abs_sgn @ TA )
=> ! [A: TA] :
( ( abs_abs @ TA @ ( uminus_uminus @ TA @ A ) )
= ( abs_abs @ TA @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(850,plain,
! [TA: $tType] :
( ~ $true
| ( one @ ( set @ TA ) )
| ( ( one @ ( set @ ( set @ ( set @ ( set @ ( set @ real ) ) ) ) ) )
!= ( one @ TA ) ) ),
inference(paramod_ordered,[status(thm)],[849,236]) ).
thf(851,plain,
! [TA: $tType] :
( ( one @ ( set @ TA ) )
| ( ( one @ ( set @ ( set @ ( set @ ( set @ ( set @ real ) ) ) ) ) )
!= ( one @ TA ) ) ),
inference(simp,[status(thm)],[850]) ).
thf(852,plain,
one @ ( set @ ( set @ ( set @ ( set @ ( set @ ( set @ real ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[851:[bind_type(TA,$thf( set @ ( set @ ( set @ ( set @ ( set @ real ) ) ) ) ))]]) ).
thf(86,axiom,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less @ TA @ A @ B )
=> ( B
!= ( zero_zero @ TA ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_28_gr__implies__not__zero) ).
thf(432,plain,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less @ TA @ A @ B )
=> ( B
!= ( zero_zero @ TA ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(433,plain,
! [TA: $tType,B: TA,A: TA] :
( ~ ( canoni770627133id_add @ TA )
| ~ ( ord_less @ TA @ A @ B )
| ( B
!= ( zero_zero @ TA ) ) ),
inference(cnf,[status(esa)],[432]) ).
thf(434,plain,
! [TA: $tType,B: TA,A: TA] :
( ( B
!= ( zero_zero @ TA ) )
| ~ ( canoni770627133id_add @ TA )
| ~ ( ord_less @ TA @ A @ B ) ),
inference(lifteq,[status(thm)],[433]) ).
thf(435,plain,
! [TA: $tType,A: TA] :
( ~ ( canoni770627133id_add @ TA )
| ~ ( ord_less @ TA @ A @ ( zero_zero @ TA ) ) ),
inference(simp,[status(thm)],[434]) ).
thf(133,axiom,
! [A: a,B: a] :
( ( poinca272511729egment @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
= ( poinca272511729egment @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_50_rev_Otransversal__segment__commute) ).
thf(583,plain,
! [A: a,B: a] :
( ( poinca272511729egment @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
= ( poinca272511729egment @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[133]) ).
thf(39,axiom,
! [TA: $tType] :
( ( linordered_ring @ TA )
=> ! [A: TA,B: TA] :
( ( ( abs_abs @ TA @ A )
= ( abs_abs @ TA @ B ) )
= ( ( A = B )
| ( A
= ( uminus_uminus @ TA @ B ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_122_abs__eq__iff) ).
thf(285,plain,
! [TA: $tType] :
( ( linordered_ring @ TA )
=> ! [A: TA,B: TA] :
( ( ( abs_abs @ TA @ A )
= ( abs_abs @ TA @ B ) )
= ( ( A = B )
| ( A
= ( uminus_uminus @ TA @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(16,axiom,
linordered_idom @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Olinordered__idom) ).
thf(224,plain,
linordered_idom @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(52,axiom,
! [TA: $tType] :
( ( neg_numeral @ TA )
=> ( ( plus_plus @ TA @ ( uminus_uminus @ TA @ ( one_one @ TA ) ) @ ( one_one @ TA ) )
= ( zero_zero @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_198_add__neg__numeral__special_I8_J) ).
thf(317,plain,
! [TA: $tType] :
( ( neg_numeral @ TA )
=> ( ( plus_plus @ TA @ ( uminus_uminus @ TA @ ( one_one @ TA ) ) @ ( one_one @ TA ) )
= ( zero_zero @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(154,axiom,
! [A: a] :
( ( period862636932_orbit @ a @ f @ x @ A )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( period1153813292period @ a @ f @ x @ A ) )
= A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_72_periodic__orbit__period_I2_J) ).
thf(650,plain,
! [A: a] :
( ( period862636932_orbit @ a @ f @ x @ A )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( period1153813292period @ a @ f @ x @ A ) )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[154]) ).
thf(78,axiom,
! [A: a,B: real] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_68_rev_Oclosed__orbit__flow0) ).
thf(403,plain,
! [A: a,B: real] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(68,axiom,
~ ! [A: real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ A )
=> ! [B: a > real] :
( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ A ) @ B )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ C @ ( B @ C ) ) @ ( line_open_segment @ a @ a2 @ b ) ) )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( ord_less @ real @ ( abs_abs @ real @ ( B @ C ) ) @ ( one_one @ real ) ) )
=> ( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ A ) @ B )
=> ( ( B @ p )
!= ( zero_zero @ real ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062d_At_O_A_092_060lbrakk_0620_A_060_Ad_059_Acontinuous__on_A_Iball_Ap_Ad_J_At_059_A_092_060And_062y_O_Ay_A_092_060in_062_Aball_Ap_Ad_A_092_060Longrightarrow_062_Aflow0_Ay_A_It_Ay_J_A_092_060in_062_A_123a_060_N_N_060b_125_059_A_092_060And_062y_O_Ay_A_092_060in_062_Aball_Ap_Ad_A_092_060Longrightarrow_062_A_092_060bar_062t_Ay_092_060bar_062_A_060_A1_059_Acontinuous__on_A_Iball_Ap_Ad_J_At_059_At_Ap_A_061_A0_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062) ).
thf(356,plain,
~ ! [A: real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ A )
=> ! [B: a > real] :
( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ A ) @ B )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ C @ ( B @ C ) ) @ ( line_open_segment @ a @ a2 @ b ) ) )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( ord_less @ real @ ( abs_abs @ real @ ( B @ C ) ) @ ( one_one @ real ) ) )
=> ( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ A ) @ B )
=> ( ( B @ p )
!= ( zero_zero @ real ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(142,axiom,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ A ) )
= ( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
& ( member @ a @ A @ x ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_111_local_Oexistence__ivl__initial__time__iff) ).
thf(610,plain,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ A ) )
= ( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
& ( member @ a @ A @ x ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[142]) ).
thf(82,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( ( ( auto_ll_on_flow0 @ a @ f @ x @ B @ A )
= B )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ B @ ( uminus_uminus @ real @ A ) )
= B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_143_recurrence__time__flip__sign_I2_J) ).
thf(420,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( ( ( auto_ll_on_flow0 @ a @ f @ x @ B @ A )
= B )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ B @ ( uminus_uminus @ real @ A ) )
= B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(109,axiom,
! [A: a] :
( ~ ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ A )
= ( bot_bot @ ( set @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_204_local_Oexistence__ivl__empty1) ).
thf(519,plain,
! [A: a] :
( ~ ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ A )
= ( bot_bot @ ( set @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
thf(183,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ B @ A ) @ x ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_108_flow0__defined) ).
thf(742,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ B @ A ) @ x ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[183]) ).
thf(17,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( abs_abs @ TA @ ( abs_abs @ TA @ A ) )
= ( abs_abs @ TA @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_20_abs__idempotent) ).
thf(225,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( abs_abs @ TA @ ( abs_abs @ TA @ A ) )
= ( abs_abs @ TA @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(114,axiom,
! [A: a,B: a] :
( ( limit_1335059408_point @ a @ f @ x @ A @ B )
= ( limit_1052139091_point @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_126__092_060alpha_062__limit__point__eq__rev) ).
thf(537,plain,
! [A: a,B: a] :
( ( limit_1335059408_point @ a @ f @ x @ A @ B )
= ( limit_1052139091_point @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(161,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
= ( ? [B: real] :
( ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ A ) )
& ( B
!= ( zero_zero @ real ) )
& ( ( auto_ll_on_flow0 @ a @ f @ x @ A @ B )
= A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_77_closed__orbit__def) ).
thf(669,plain,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
= ( ? [B: real] :
( ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ A ) )
& ( B
!= ( zero_zero @ real ) )
& ( ( auto_ll_on_flow0 @ a @ f @ x @ A @ B )
= A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[161]) ).
thf(151,axiom,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA] :
( ( ord_less @ TA @ ( zero_zero @ TA ) @ A )
= ( A
!= ( zero_zero @ TA ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_27_zero__less__iff__neq__zero) ).
thf(642,plain,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA] :
( ( ord_less @ TA @ ( zero_zero @ TA ) @ A )
= ( A
!= ( zero_zero @ TA ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[151]) ).
thf(100,axiom,
poinca272511729egment @ a @ f @ x @ a2 @ b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_assms_I1_J) ).
thf(489,plain,
poinca272511729egment @ a @ f @ x @ a2 @ b,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(136,axiom,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( f @ A )
!= ( zero_zero @ a ) )
=> ~ ! [B: a,C: a] :
( ( member @ a @ A @ ( line_open_segment @ a @ B @ C ) )
=> ~ ( poinca272511729egment @ a @ f @ x @ B @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_22_transversal__segment__exists) ).
thf(590,plain,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( f @ A )
!= ( zero_zero @ a ) )
=> ~ ! [B: a,C: a] :
( ( member @ a @ A @ ( line_open_segment @ a @ B @ C ) )
=> ~ ( poinca272511729egment @ a @ f @ x @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[136]) ).
thf(171,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ( ( period1153813292period @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( zero_zero @ real ) )
=> ( ( uminus_uminus @ ( a > a ) @ f @ A )
= ( zero_zero @ a ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_99_rev_Oclosed__orbit__period__zero__fixed__point) ).
thf(706,plain,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ( ( period1153813292period @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( zero_zero @ real ) )
=> ( ( uminus_uminus @ ( a > a ) @ f @ A )
= ( zero_zero @ a ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[171]) ).
thf(121,axiom,
! [A: a] :
( ( member @ a @ A @ x )
=> ( member @ real @ ( zero_zero @ real ) @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_56_existence__ivl__zero) ).
thf(554,plain,
! [A: a] :
( ( member @ a @ A @ x )
=> ( member @ real @ ( zero_zero @ real ) @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[121]) ).
thf(187,axiom,
linordered_ring @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Olinordered__ring) ).
thf(753,plain,
linordered_ring @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[187]) ).
thf(94,axiom,
! [TA: $tType,A: set @ a,B: a > a,C: real,D: a] :
( ( x = A )
=> ( ! [E: a,F: TA] :
( ( member @ a @ E @ A )
=> ( ( uminus_uminus @ ( a > a ) @ f @ E )
= ( B @ E ) ) )
=> ( ( member @ real @ C @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ D ) )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ D @ C )
= ( auto_ll_on_flow0 @ a @ B @ A @ D @ C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_66_rev_Oflow0__cong) ).
thf(457,plain,
! [A: set @ a,B: a > a,C: real,D: a] :
( ( x = A )
=> ( ! [E: a] :
( ( member @ a @ E @ A )
=> ( ( uminus_uminus @ ( a > a ) @ f @ E )
= ( B @ E ) ) )
=> ( ( member @ real @ C @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ D ) )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ D @ C )
= ( auto_ll_on_flow0 @ a @ B @ A @ D @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(176,axiom,
! [A: a] :
( ( period862636932_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ ( period1153813292period @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) )
= A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_85_rev_Operiodic__orbit__period_I2_J) ).
thf(721,plain,
! [A: a] :
( ( period862636932_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ ( period1153813292period @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[176]) ).
thf(22,axiom,
! [TA: $tType] :
( ( real_V2090557954_space @ TA )
=> ! [A: TA] :
( ( elemen1815086676c_ball @ TA @ A @ ( zero_zero @ real ) )
= ( bot_bot @ ( set @ TA ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_196_ball__trivial) ).
thf(237,plain,
! [TA: $tType] :
( ( real_V2090557954_space @ TA )
=> ! [A: TA] :
( ( elemen1815086676c_ball @ TA @ A @ ( zero_zero @ real ) )
= ( bot_bot @ ( set @ TA ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(25,axiom,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ( ( ord_less_eq @ TA )
= ( ^ [A: TA,B: TA] :
? [C: TA] :
( B
= ( plus_plus @ TA @ A @ C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_220_le__iff__add) ).
thf(244,plain,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ( ( ord_less_eq @ TA )
= ( ^ [A: TA,B: TA] :
? [C: TA] :
( B
= ( plus_plus @ TA @ A @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(50,axiom,
! [TA: $tType] :
( ( linordered_idom @ TA )
=> ( ( abs_abs @ TA @ ( uminus_uminus @ TA @ ( one_one @ TA ) ) )
= ( one_one @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_130_abs__neg__one) ).
thf(311,plain,
! [TA: $tType] :
( ( linordered_idom @ TA )
=> ( ( abs_abs @ TA @ ( uminus_uminus @ TA @ ( one_one @ TA ) ) )
= ( one_one @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(116,axiom,
! [A: a,B: a,C: a,D: a] :
( ( member @ a @ A @ ( line_open_segment @ a @ B @ C ) )
=> ( ( member @ a @ D @ ( line_open_segment @ a @ B @ C ) )
=> ( ( A = D )
| ( member @ a @ D @ ( line_open_segment @ a @ A @ C ) )
| ( member @ a @ D @ ( line_open_segment @ a @ B @ A ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_rev_Oopen__segment__trichotomy) ).
thf(541,plain,
! [A: a,B: a,C: a,D: a] :
( ( member @ a @ A @ ( line_open_segment @ a @ B @ C ) )
=> ( ( member @ a @ D @ ( line_open_segment @ a @ B @ C ) )
=> ( ( A = D )
| ( member @ a @ D @ ( line_open_segment @ a @ A @ C ) )
| ( member @ a @ D @ ( line_open_segment @ a @ B @ A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(76,axiom,
! [A: real,B: real,C: a] :
( ( member @ real @ ( plus_plus @ real @ A @ B ) @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) )
=> ( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) )
=> ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C @ A ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_150_local_Orev_Oexistence__ivl__trans_H) ).
thf(398,plain,
! [A: real,B: real,C: a] :
( ( member @ real @ ( plus_plus @ real @ A @ B ) @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) )
=> ( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) )
=> ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C @ A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(175,axiom,
! [TA: $tType] :
( ( abs_if @ TA )
=> ( ( abs_abs @ TA )
= ( ^ [A: TA] : ( if @ TA @ ( ord_less @ TA @ A @ ( zero_zero @ TA ) ) @ ( uminus_uminus @ TA @ A ) @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_124_abs__if) ).
thf(718,plain,
! [TA: $tType] :
( ( abs_if @ TA )
=> ( ( abs_abs @ TA )
= ( ^ [A: TA] : ( if @ TA @ ( ord_less @ TA @ A @ ( zero_zero @ TA ) ) @ ( uminus_uminus @ TA @ A ) @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[175]) ).
thf(193,axiom,
! [A: real,B: a > real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ A )
=> ( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ A ) @ B )
=> ( ( ( B @ p )
= ( zero_zero @ real ) )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( ord_less @ real @ ( abs_abs @ real @ ( B @ C ) ) @ ( one_one @ real ) ) )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ C @ ( B @ C ) ) @ ( line_open_segment @ a @ a2 @ b ) ) )
=> thesisa ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(773,plain,
! [A: real,B: a > real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ A )
=> ( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ A ) @ B )
=> ( ( ( B @ p )
= ( zero_zero @ real ) )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( ord_less @ real @ ( abs_abs @ real @ ( B @ C ) ) @ ( one_one @ real ) ) )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ C @ ( B @ C ) ) @ ( line_open_segment @ a @ a2 @ b ) ) )
=> thesisa ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[193]) ).
thf(134,axiom,
zero @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ozero_10) ).
thf(586,plain,
zero @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[134]) ).
thf(145,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ( zero_zero @ TA )
= ( abs_abs @ TA @ A ) )
= ( A
= ( zero_zero @ TA ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_12_abs__0__eq) ).
thf(618,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ( zero_zero @ TA )
= ( abs_abs @ TA @ A ) )
= ( A
= ( zero_zero @ TA ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[145]) ).
thf(84,axiom,
! [A: real,B: real,C: a] :
( ( A != B )
=> ( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) )
=> ( ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) )
=> ( ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C @ A )
= ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C @ B ) )
=> ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_79_rev_Oclosed__orbitI) ).
thf(425,plain,
! [A: real,B: real,C: a] :
( ( A != B )
=> ( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) )
=> ( ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) )
=> ( ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C @ A )
= ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C @ B ) )
=> ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(37,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( top_top @ ( set @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_78_rev_Oclosed__orbit__global__existence) ).
thf(279,plain,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( top_top @ ( set @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(43,axiom,
! [TA: $tType] :
( ( ab_group_add @ TA )
=> ! [A: TA,B: TA] :
( ( uminus_uminus @ TA @ ( plus_plus @ TA @ A @ B ) )
= ( plus_plus @ TA @ ( uminus_uminus @ TA @ A ) @ ( uminus_uminus @ TA @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_171_minus__add__distrib) ).
thf(296,plain,
! [TA: $tType] :
( ( ab_group_add @ TA )
=> ! [A: TA,B: TA] :
( ( uminus_uminus @ TA @ ( plus_plus @ TA @ A @ B ) )
= ( plus_plus @ TA @ ( uminus_uminus @ TA @ A ) @ ( uminus_uminus @ TA @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(71,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ~ ! [B: real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ B )
=> ~ ! [C: real] :
( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ ( plus_plus @ real @ C @ B ) )
= ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_131_rev_Oclosed__orbitE) ).
thf(375,plain,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ~ ! [B: real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ B )
=> ~ ! [C: real] :
( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ ( plus_plus @ real @ C @ B ) )
= ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(124,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ( member @ a @ A @ x ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_53_closed__orbit__in__domain) ).
thf(562,plain,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ( member @ a @ A @ x ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[124]) ).
thf(83,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) @ x ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_113_rev_Oflow0__defined) ).
thf(423,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) @ x ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(166,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ B @ A ) @ x ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_109_local_Oflow__in__domain) ).
thf(694,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ B @ A ) @ x ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[166]) ).
thf(117,axiom,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( f @ A )
= ( zero_zero @ a ) )
=> ( ( period1153813292period @ a @ f @ x @ A )
= ( zero_zero @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_39_fixed__point__imp__closed__orbit__period__zero_I2_J) ).
thf(545,plain,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( f @ A )
= ( zero_zero @ a ) )
=> ( ( period1153813292period @ a @ f @ x @ A )
= ( zero_zero @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[117]) ).
thf(131,axiom,
! [TA: $tType] :
( ( linordered_idom @ TA )
=> ! [A: TA,B: TA] :
( ( A != B )
=> ( ~ ( ord_less @ TA @ A @ B )
=> ( ord_less @ TA @ B @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_25_linorder__neqE__linordered__idom) ).
thf(579,plain,
! [TA: $tType] :
( ( linordered_idom @ TA )
=> ! [A: TA,B: TA] :
( ( A != B )
=> ( ~ ( ord_less @ TA @ A @ B )
=> ( ord_less @ TA @ B @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(41,axiom,
! [TA: $tType] :
( ( linordered_idom @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less @ TA @ ( abs_abs @ TA @ A ) @ B )
= ( ( ord_less @ TA @ A @ B )
& ( ord_less @ TA @ ( uminus_uminus @ TA @ A ) @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_123_abs__less__iff) ).
thf(291,plain,
! [TA: $tType] :
( ( linordered_idom @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less @ TA @ ( abs_abs @ TA @ A ) @ B )
= ( ( ord_less @ TA @ A @ B )
& ( ord_less @ TA @ ( uminus_uminus @ TA @ A ) @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(90,axiom,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( f @ A )
= ( zero_zero @ a ) )
=> ( period385816147_orbit @ a @ f @ x @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_51_fixed__point__imp__closed__orbit__period__zero_I1_J) ).
thf(445,plain,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( f @ A )
= ( zero_zero @ a ) )
=> ( period385816147_orbit @ a @ f @ x @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(128,axiom,
! [TA: $tType,A: TA,B: TA > $o] :
( ( member @ TA @ A @ ( collect @ TA @ B ) )
= ( B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_43_mem__Collect__eq) ).
thf(572,plain,
! [TA: $tType,A: TA,B: TA > $o] :
( ( member @ TA @ A @ ( collect @ TA @ B ) )
= ( B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[128]) ).
thf(174,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ~ ! [B: real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ B )
=> ~ ! [C: real] :
( ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( plus_plus @ real @ C @ B ) )
= ( auto_ll_on_flow0 @ a @ f @ x @ A @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_170_closed__orbitE) ).
thf(713,plain,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ~ ! [B: real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ B )
=> ~ ! [C: real] :
( ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( plus_plus @ real @ C @ B ) )
= ( auto_ll_on_flow0 @ a @ f @ x @ A @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[174]) ).
thf(95,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A )
= B )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ ( uminus_uminus @ real @ A ) )
= B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_145_rev_Orecurrence__time__flip__sign_I2_J) ).
thf(466,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A )
= B )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ ( uminus_uminus @ real @ A ) )
= B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(115,axiom,
limit_1052139091_point @ a @ f @ x @ x2 @ p,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_assms_I3_J) ).
thf(540,plain,
limit_1052139091_point @ a @ f @ x @ x2 @ p,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(162,axiom,
! [A: real,B: a,C: real] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( ( member @ real @ C @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ ( auto_ll_on_flow0 @ a @ f @ x @ B @ A ) ) )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ B @ ( plus_plus @ real @ A @ C ) )
= ( auto_ll_on_flow0 @ a @ f @ x @ ( auto_ll_on_flow0 @ a @ f @ x @ B @ A ) @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_146_local_Oflow__trans) ).
thf(672,plain,
! [A: real,B: a,C: real] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( ( member @ real @ C @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ ( auto_ll_on_flow0 @ a @ f @ x @ B @ A ) ) )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ B @ ( plus_plus @ real @ A @ C ) )
= ( auto_ll_on_flow0 @ a @ f @ x @ ( auto_ll_on_flow0 @ a @ f @ x @ B @ A ) @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[162]) ).
thf(79,axiom,
! [TA: $tType,A: set @ a,B: a > a,C: real,D: a] :
( ( x = A )
=> ( ! [E: a,F: TA] :
( ( member @ a @ E @ A )
=> ( ( f @ E )
= ( B @ E ) ) )
=> ( ( member @ real @ C @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ D ) )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ D @ C )
= ( auto_ll_on_flow0 @ a @ B @ A @ D @ C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_59_flow0__cong) ).
thf(406,plain,
! [A: set @ a,B: a > a,C: real,D: a] :
( ( x = A )
=> ( ! [E: a] :
( ( member @ a @ E @ A )
=> ( ( f @ E )
= ( B @ E ) ) )
=> ( ( member @ real @ C @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ D ) )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ D @ C )
= ( auto_ll_on_flow0 @ a @ B @ A @ D @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(14,axiom,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less_eq @ TA @ B @ C )
=> ( ord_less_eq @ TA @ B @ ( plus_plus @ TA @ C @ A ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_221_add__increasing2) ).
thf(219,plain,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less_eq @ TA @ B @ C )
=> ( ord_less_eq @ TA @ B @ ( plus_plus @ TA @ C @ A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(106,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( abs_abs @ TA @ A )
= A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_37_abs__of__pos) ).
thf(509,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( abs_abs @ TA @ A )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(138,axiom,
! [TA: $tType,A: set @ TA] :
( ( collect @ TA
@ ^ [B: TA] : ( member @ TA @ B @ A ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_44_Collect__mem__eq) ).
thf(599,plain,
! [TA: $tType,A: set @ TA] :
( ( collect @ TA
@ ^ [B: TA] : ( member @ TA @ B @ A ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[138]) ).
thf(92,axiom,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ A )
= ( zero_zero @ a ) )
=> ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_71_rev_Ofixed__point__imp__closed__orbit__period__zero_I1_J) ).
thf(451,plain,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ A )
= ( zero_zero @ a ) )
=> ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(126,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( abs_abs @ TA @ A )
= ( uminus_uminus @ TA @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_125_abs__of__neg) ).
thf(567,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( abs_abs @ TA @ A )
= ( uminus_uminus @ TA @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[126]) ).
thf(34,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ord_less_eq @ real @ ( zero_zero @ real ) @ ( period1153813292period @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_133_rev_Oclosed__orbit__period__nonneg) ).
thf(271,plain,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( ord_less_eq @ real @ ( zero_zero @ real ) @ ( period1153813292period @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(8,axiom,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( ord_less_eq @ TA @ B @ ( zero_zero @ TA ) )
=> ( ord_less_eq @ TA @ ( plus_plus @ TA @ A @ B ) @ ( zero_zero @ TA ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_218_add__nonpos__nonpos) ).
thf(208,plain,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( ord_less_eq @ TA @ B @ ( zero_zero @ TA ) )
=> ( ord_less_eq @ TA @ ( plus_plus @ TA @ A @ B ) @ ( zero_zero @ TA ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(10,axiom,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( ord_less_eq @ TA @ B @ C )
=> ( ord_less_eq @ TA @ ( plus_plus @ TA @ A @ B ) @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_226_add__decreasing) ).
thf(213,plain,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( ord_less_eq @ TA @ B @ C )
=> ( ord_less_eq @ TA @ ( plus_plus @ TA @ A @ B ) @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(146,axiom,
! [A: real,B: a] :
( ~ ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ B @ A )
= ( zero_zero @ a ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_47_local_Oflow__undefined0) ).
thf(621,plain,
! [A: real,B: a] :
( ~ ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ B @ A )
= ( zero_zero @ a ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[146]) ).
thf(23,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less_eq @ TA @ ( abs_abs @ TA @ A ) @ A )
= ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_194_abs__le__self__iff) ).
thf(240,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less_eq @ TA @ ( abs_abs @ TA @ A ) @ A )
= ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(4,axiom,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less_eq @ TA @ B @ C )
=> ( ord_less_eq @ TA @ B @ ( plus_plus @ TA @ A @ C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_225_add__increasing) ).
thf(198,plain,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less_eq @ TA @ B @ C )
=> ( ord_less_eq @ TA @ B @ ( plus_plus @ TA @ A @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(149,axiom,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA] :
( ( A
!= ( zero_zero @ TA ) )
=> ( ord_less @ TA @ ( zero_zero @ TA ) @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_30_gr__zeroI) ).
thf(636,plain,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA] :
( ( A
!= ( zero_zero @ TA ) )
=> ( ord_less @ TA @ ( zero_zero @ TA ) @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[149]) ).
thf(47,axiom,
! [TA: $tType] :
( ( linord1659791738miring @ TA )
=> ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ ( zero_zero @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_209_le__numeral__extra_I3_J) ).
thf(306,plain,
! [TA: $tType] :
( ( linord1659791738miring @ TA )
=> ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ ( zero_zero @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(44,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( member @ real @ A @ ( top_top @ ( set @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_65_local_Orev_Omem__existence__ivl__subset) ).
thf(299,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( member @ real @ A @ ( top_top @ ( set @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(33,axiom,
! [A: a] :
( ~ ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( bot_bot @ ( set @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_206_local_Orev_Oexistence__ivl__empty1) ).
thf(267,plain,
! [A: a] :
( ~ ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( bot_bot @ ( set @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(155,axiom,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA] :
( ( ~ ( ord_less @ TA @ ( zero_zero @ TA ) @ A ) )
= ( A
= ( zero_zero @ TA ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_15_not__gr__zero) ).
thf(653,plain,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA] :
( ( ~ ( ord_less @ TA @ ( zero_zero @ TA ) @ A ) )
= ( A
= ( zero_zero @ TA ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[155]) ).
thf(156,axiom,
! [TA: $tType] :
( ( zero_neq_one @ TA )
=> ( ( zero_zero @ TA )
!= ( one_one @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_31_zero__neq__one) ).
thf(656,plain,
! [TA: $tType] :
( ( zero_neq_one @ TA )
=> ( ( zero_zero @ TA )
!= ( one_one @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[156]) ).
thf(657,plain,
! [TA: $tType] :
( ~ ( zero_neq_one @ TA )
| ( ( zero_zero @ TA )
!= ( one_one @ TA ) ) ),
inference(cnf,[status(esa)],[656]) ).
thf(658,plain,
! [TA: $tType] :
( ( ( zero_zero @ TA )
!= ( one_one @ TA ) )
| ~ ( zero_neq_one @ TA ) ),
inference(lifteq,[status(thm)],[657]) ).
thf(101,axiom,
! [A: a,B: a,C: a,D: real] :
( ( poinca272511729egment @ a @ f @ x @ A @ B )
=> ( ( member @ a @ C @ ( line_open_segment @ a @ A @ B ) )
=> ( ( ord_less @ real @ ( zero_zero @ real ) @ D )
=> ~ ! [E: real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ E )
=> ! [F: a > real] :
( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ C @ E ) @ F )
=> ( ! [G: a] :
( ( member @ a @ G @ ( elemen1815086676c_ball @ a @ C @ E ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ G @ ( F @ G ) ) @ ( line_open_segment @ a @ A @ B ) ) )
=> ( ! [G: a] :
( ( member @ a @ G @ ( elemen1815086676c_ball @ a @ C @ E ) )
=> ( ord_less @ real @ ( abs_abs @ real @ ( F @ G ) ) @ D ) )
=> ( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ C @ E ) @ F )
=> ( ( F @ C )
!= ( zero_zero @ real ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9_cross__time__continuous) ).
thf(490,plain,
! [A: a,B: a,C: a,D: real] :
( ( poinca272511729egment @ a @ f @ x @ A @ B )
=> ( ( member @ a @ C @ ( line_open_segment @ a @ A @ B ) )
=> ( ( ord_less @ real @ ( zero_zero @ real ) @ D )
=> ~ ! [E: real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ E )
=> ! [F: a > real] :
( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ C @ E ) @ F )
=> ( ! [G: a] :
( ( member @ a @ G @ ( elemen1815086676c_ball @ a @ C @ E ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ G @ ( F @ G ) ) @ ( line_open_segment @ a @ A @ B ) ) )
=> ( ! [G: a] :
( ( member @ a @ G @ ( elemen1815086676c_ball @ a @ C @ E ) )
=> ( ord_less @ real @ ( abs_abs @ real @ ( F @ G ) ) @ D ) )
=> ( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ C @ E ) @ F )
=> ( ( F @ C )
!= ( zero_zero @ real ) ) ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(164,axiom,
! [TA: $tType] :
( ( idom_abs_sgn @ TA )
=> ( ( abs_abs @ TA @ ( zero_zero @ TA ) )
= ( zero_zero @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11_abs__0) ).
thf(680,plain,
! [TA: $tType] :
( ( idom_abs_sgn @ TA )
=> ( ( abs_abs @ TA @ ( zero_zero @ TA ) )
= ( zero_zero @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[164]) ).
thf(118,axiom,
! [A: a] : ( initia826609931terval @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_129_mvar_Ointerval__axioms) ).
thf(548,plain,
! [A: a] : ( initia826609931terval @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(29,axiom,
! [TA: $tType,A: TA > $o,B: TA > $o] :
( ! [C: TA] :
( ( A @ C )
= ( B @ C ) )
=> ( ( collect @ TA @ A )
= ( collect @ TA @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_45_Collect__cong) ).
thf(255,plain,
! [TA: $tType,A: TA > $o,B: TA > $o] :
( ! [C: TA] :
( ( A @ C )
= ( B @ C ) )
=> ( ( collect @ TA @ A )
= ( collect @ TA @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(153,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( member @ a @ B @ x ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_107_local_Orev_Omem__existence__ivl__iv__defined_I2_J) ).
thf(648,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( member @ a @ B @ x ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[153]) ).
thf(186,axiom,
! [A: a,B: real] :
( ( member @ a @ A @ x )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ A )
= ( zero_zero @ a ) )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
= A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_42_rev_Ofixpoint__sol_I2_J) ).
thf(749,plain,
! [A: a,B: real] :
( ( member @ a @ A @ x )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ A )
= ( zero_zero @ a ) )
=> ( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[186]) ).
thf(188,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( member @ a @ A @ x ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_61_rev_Oclosed__orbit__in__domain) ).
thf(754,plain,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
=> ( member @ a @ A @ x ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[188]) ).
thf(1,conjecture,
thesisa,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
thf(2,negated_conjecture,
~ thesisa,
inference(neg_conjecture,[status(cth)],[1]) ).
thf(194,plain,
~ thesisa,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(144,axiom,
zero_neq_one @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Ozero__neq__one) ).
thf(617,plain,
zero_neq_one @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[144]) ).
thf(108,axiom,
! [A: a,B: real] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ( period385816147_orbit @ a @ f @ x @ ( auto_ll_on_flow0 @ a @ f @ x @ A @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_closed__orbit__flow0) ).
thf(516,plain,
! [A: a,B: real] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ( period385816147_orbit @ a @ f @ x @ ( auto_ll_on_flow0 @ a @ f @ x @ A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(56,axiom,
! [TA: $tType] :
( ( linord1659791738miring @ TA )
=> ( ord_less_eq @ TA @ ( one_one @ TA ) @ ( one_one @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_210_le__numeral__extra_I4_J) ).
thf(327,plain,
! [TA: $tType] :
( ( linord1659791738miring @ TA )
=> ( ord_less_eq @ TA @ ( one_one @ TA ) @ ( one_one @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(182,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less @ TA @ ( zero_zero @ TA ) @ ( abs_abs @ TA @ A ) )
= ( A
!= ( zero_zero @ TA ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_8_zero__less__abs__iff) ).
thf(739,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ord_less @ TA @ ( zero_zero @ TA ) @ ( abs_abs @ TA @ A ) )
= ( A
!= ( zero_zero @ TA ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[182]) ).
thf(32,axiom,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( member @ a @ A @ x )
=> ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
!= ( bot_bot @ ( set @ real ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_132_local_Orev_Oexistence__ivl__notempty) ).
thf(263,plain,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( member @ a @ A @ x )
=> ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
!= ( bot_bot @ ( set @ real ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(170,axiom,
ab_group_add @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oab__group__add) ).
thf(705,plain,
ab_group_add @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[170]) ).
thf(38,axiom,
! [TA: $tType] :
( ( neg_numeral @ TA )
=> ( ( plus_plus @ TA @ ( one_one @ TA ) @ ( uminus_uminus @ TA @ ( one_one @ TA ) ) )
= ( zero_zero @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_197_add__neg__numeral__special_I7_J) ).
thf(282,plain,
! [TA: $tType] :
( ( neg_numeral @ TA )
=> ( ( plus_plus @ TA @ ( one_one @ TA ) @ ( uminus_uminus @ TA @ ( one_one @ TA ) ) )
= ( zero_zero @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(199,plain,
! [TA: $tType,C: TA,B: TA,A: TA] :
( ~ ( ordere216010020id_add @ TA )
| ~ ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
| ~ ( ord_less_eq @ TA @ B @ C )
| ( ord_less_eq @ TA @ B @ ( plus_plus @ TA @ A @ C ) ) ),
inference(cnf,[status(esa)],[198]) ).
thf(130,axiom,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( member @ a @ A @ x )
=> ( member @ real @ ( zero_zero @ real ) @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_64_local_Oexistence__ivl__initial__time) ).
thf(576,plain,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( member @ a @ A @ x )
=> ( member @ real @ ( zero_zero @ real ) @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[130]) ).
thf(184,axiom,
! [A: a,B: a] :
( ( poinca272511729egment @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
=> ( poinca272511729egment @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_49_rev_Otransversal__segment__reverse) ).
thf(744,plain,
! [A: a,B: a] :
( ( poinca272511729egment @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
=> ( poinca272511729egment @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[184]) ).
thf(143,axiom,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( member @ a @ A @ x )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( zero_zero @ real ) )
= A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_112_local_Oflow__initial__time) ).
thf(613,plain,
! [A: a] :
( ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) )
=> ( ( member @ a @ A @ x )
=> ( ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( zero_zero @ real ) )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[143]) ).
thf(178,axiom,
! [A: real,B: real,C: a] :
( ( A != B )
=> ( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ C ) )
=> ( ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ C ) )
=> ( ( ( auto_ll_on_flow0 @ a @ f @ x @ C @ A )
= ( auto_ll_on_flow0 @ a @ f @ x @ C @ B ) )
=> ( period385816147_orbit @ a @ f @ x @ C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_70_closed__orbitI) ).
thf(727,plain,
! [A: real,B: real,C: a] :
( ( A != B )
=> ( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ C ) )
=> ( ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ C ) )
=> ( ( ( auto_ll_on_flow0 @ a @ f @ x @ C @ A )
= ( auto_ll_on_flow0 @ a @ f @ x @ C @ B ) )
=> ( period385816147_orbit @ a @ f @ x @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[178]) ).
thf(51,axiom,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
= ( A
= ( zero_zero @ TA ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_154_le__zero__eq) ).
thf(314,plain,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
= ( A
= ( zero_zero @ TA ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(148,axiom,
! [TA: $tType,A: set @ a,B: a > a,C: a] :
( ( x = A )
=> ( ! [D: a,E: TA] :
( ( member @ a @ D @ A )
=> ( ( uminus_uminus @ ( a > a ) @ f @ D )
= ( B @ D ) ) )
=> ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C )
= ( auto_l1112008849e_ivl0 @ a @ B @ A @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_57_rev_Oexistence__ivl0__cong) ).
thf(627,plain,
! [A: set @ a,B: a > a,C: a] :
( ( x = A )
=> ( ! [D: a] :
( ( member @ a @ D @ A )
=> ( ( uminus_uminus @ ( a > a ) @ f @ D )
= ( B @ D ) ) )
=> ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ C )
= ( auto_l1112008849e_ivl0 @ a @ B @ A @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[148]) ).
thf(6,axiom,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( ord_less_eq @ TA @ B @ ( zero_zero @ TA ) )
=> ( ( ( plus_plus @ TA @ A @ B )
= ( zero_zero @ TA ) )
= ( ( A
= ( zero_zero @ TA ) )
& ( B
= ( zero_zero @ TA ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_216_add__nonpos__eq__0__iff) ).
thf(203,plain,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( ord_less_eq @ TA @ B @ ( zero_zero @ TA ) )
=> ( ( ( plus_plus @ TA @ A @ B )
= ( zero_zero @ TA ) )
= ( ( A
= ( zero_zero @ TA ) )
& ( B
= ( zero_zero @ TA ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(191,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( ( ( auto_ll_on_flow0 @ a @ f @ x @ B @ A )
= B )
=> ( member @ real @ ( uminus_uminus @ real @ A ) @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_142_recurrence__time__flip__sign_I1_J) ).
thf(759,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( ( ( auto_ll_on_flow0 @ a @ f @ x @ B @ A )
= B )
=> ( member @ real @ ( uminus_uminus @ real @ A ) @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[191]) ).
thf(13,axiom,
ordere216010020id_add @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oordered__comm__monoid__add) ).
thf(218,plain,
ordere216010020id_add @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(357,plain,
~ ! [A: real] :
( ( ord_less @ real @ ( zero_zero @ real ) @ A )
=> ! [B: a > real] :
( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ A ) @ B )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ C @ ( B @ C ) ) @ ( line_open_segment @ a @ a2 @ b ) ) )
=> ( ! [C: a] :
( ( member @ a @ C @ ( elemen1815086676c_ball @ a @ p @ A ) )
=> ( ord_less @ real @ ( abs_abs @ real @ ( B @ C ) ) @ ( one_one @ real ) ) )
=> ( ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ A ) @ B )
=> ( ( B @ p )
!= ( zero_zero @ real ) ) ) ) ) ) ),
inference(polarity_switch,[status(thm)],[356]) ).
thf(358,plain,
! [B: a,A: a] :
( ( ord_less @ real @ ( zero_zero @ real ) @ sk3 )
& ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ sk3 ) @ sk4 )
& ( ~ ( member @ a @ A @ ( elemen1815086676c_ball @ a @ p @ sk3 ) )
| ( member @ a @ ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( sk4 @ A ) ) @ ( line_open_segment @ a @ a2 @ b ) ) )
& ( ~ ( member @ a @ B @ ( elemen1815086676c_ball @ a @ p @ sk3 ) )
| ( ord_less @ real @ ( abs_abs @ real @ ( sk4 @ B ) ) @ ( one_one @ real ) ) )
& ( topolo2071040574ous_on @ a @ real @ ( elemen1815086676c_ball @ a @ p @ sk3 ) @ sk4 )
& ( ( sk4 @ p )
= ( zero_zero @ real ) ) ),
inference(cnf,[status(esa)],[357]) ).
thf(363,plain,
ord_less @ real @ ( zero_zero @ real ) @ sk3,
inference(cnfConj,[status(thm)],[358]) ).
thf(122,axiom,
! [A: a] :
( ( period862636932_orbit @ a @ f @ x @ A )
= ( ( period385816147_orbit @ a @ f @ x @ A )
& ( ord_less @ real @ ( zero_zero @ real ) @ ( period1153813292period @ a @ f @ x @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_100_periodic__orbit__def) ).
thf(556,plain,
! [A: a] :
( ( period862636932_orbit @ a @ f @ x @ A )
= ( ( period385816147_orbit @ a @ f @ x @ A )
& ( ord_less @ real @ ( zero_zero @ real ) @ ( period1153813292period @ a @ f @ x @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[122]) ).
thf(46,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA,B: TA] : ( ord_less_eq @ TA @ ( abs_abs @ TA @ ( plus_plus @ TA @ A @ B ) ) @ ( plus_plus @ TA @ ( abs_abs @ TA @ A ) @ ( abs_abs @ TA @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_208_abs__triangle__ineq) ).
thf(304,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA,B: TA] : ( ord_less_eq @ TA @ ( abs_abs @ TA @ ( plus_plus @ TA @ A @ B ) ) @ ( plus_plus @ TA @ ( abs_abs @ TA @ A ) @ ( abs_abs @ TA @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(30,axiom,
! [A: a] :
( ~ ( member @ a @ A @ x )
=> ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( bot_bot @ ( set @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_202_local_Orev_Oexistence__ivl__undefined) ).
thf(258,plain,
! [A: a] :
( ~ ( member @ a @ A @ x )
=> ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( bot_bot @ ( set @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(66,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) @ x ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_114_local_Orev_Oflow__in__domain) ).
thf(351,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( member @ a @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) @ x ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(179,axiom,
! [A: real,B: real,C: a] :
( ( member @ real @ ( plus_plus @ real @ A @ B ) @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ C ) )
=> ( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ C ) )
=> ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ ( auto_ll_on_flow0 @ a @ f @ x @ C @ A ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_147_local_Oexistence__ivl__trans_H) ).
thf(731,plain,
! [A: real,B: real,C: a] :
( ( member @ real @ ( plus_plus @ real @ A @ B ) @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ C ) )
=> ( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ C ) )
=> ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ ( auto_ll_on_flow0 @ a @ f @ x @ C @ A ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[179]) ).
thf(73,axiom,
! [TA: $tType,A: set @ a,B: a > a,C: a] :
( ( x = A )
=> ( ! [D: a,E: TA] :
( ( member @ a @ D @ A )
=> ( ( f @ D )
= ( B @ D ) ) )
=> ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ C )
= ( auto_l1112008849e_ivl0 @ a @ B @ A @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_52_existence__ivl0__cong) ).
thf(383,plain,
! [A: set @ a,B: a > a,C: a] :
( ( x = A )
=> ( ! [D: a] :
( ( member @ a @ D @ A )
=> ( ( f @ D )
= ( B @ D ) ) )
=> ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ C )
= ( auto_l1112008849e_ivl0 @ a @ B @ A @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(35,axiom,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ( plus_plus @ TA @ A @ B )
= ( zero_zero @ TA ) )
= ( ( A
= ( zero_zero @ TA ) )
& ( B
= ( zero_zero @ TA ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_157_add__eq__0__iff__both__eq__0) ).
thf(273,plain,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ( plus_plus @ TA @ A @ B )
= ( zero_zero @ TA ) )
= ( ( A
= ( zero_zero @ TA ) )
& ( B
= ( zero_zero @ TA ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(181,axiom,
! [A: real,B: real,C: a] :
( ( A != B )
=> ( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ C ) )
=> ( ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ C ) )
=> ( ( ( auto_ll_on_flow0 @ a @ f @ x @ C @ A )
= ( auto_ll_on_flow0 @ a @ f @ x @ C @ B ) )
=> ( ( ( f @ C )
!= ( zero_zero @ a ) )
=> ( period862636932_orbit @ a @ f @ x @ C ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_82_periodic__orbitI) ).
thf(735,plain,
! [A: real,B: real,C: a] :
( ( A != B )
=> ( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ C ) )
=> ( ( member @ real @ B @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ C ) )
=> ( ( ( auto_ll_on_flow0 @ a @ f @ x @ C @ A )
= ( auto_ll_on_flow0 @ a @ f @ x @ C @ B ) )
=> ( ( ( f @ C )
!= ( zero_zero @ a ) )
=> ( period862636932_orbit @ a @ f @ x @ C ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[181]) ).
thf(125,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ( ( ( f @ A )
!= ( zero_zero @ a ) )
=> ( period862636932_orbit @ a @ f @ x @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_73_closed__orbit__periodic) ).
thf(564,plain,
! [A: a] :
( ( period385816147_orbit @ a @ f @ x @ A )
=> ( ( ( f @ A )
!= ( zero_zero @ a ) )
=> ( period862636932_orbit @ a @ f @ x @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[125]) ).
thf(9,axiom,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ B )
=> ( ( ( plus_plus @ TA @ A @ B )
= ( zero_zero @ TA ) )
= ( ( A
= ( zero_zero @ TA ) )
& ( B
= ( zero_zero @ TA ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_217_add__nonneg__eq__0__iff) ).
thf(210,plain,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less_eq @ TA @ ( zero_zero @ TA ) @ B )
=> ( ( ( plus_plus @ TA @ A @ B )
= ( zero_zero @ TA ) )
= ( ( A
= ( zero_zero @ TA ) )
& ( B
= ( zero_zero @ TA ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(42,axiom,
! [TA: $tType] :
( ( ordere1818651114id_add @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( ord_less @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less_eq @ TA @ B @ C )
=> ( ord_less @ TA @ B @ ( plus_plus @ TA @ A @ C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_246_add__strict__increasing) ).
thf(294,plain,
! [TA: $tType] :
( ( ordere1818651114id_add @ TA )
=> ! [A: TA,B: TA,C: TA] :
( ( ord_less @ TA @ ( zero_zero @ TA ) @ A )
=> ( ( ord_less_eq @ TA @ B @ C )
=> ( ord_less @ TA @ B @ ( plus_plus @ TA @ A @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(62,axiom,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ A @ B )
=> ~ ! [C: TA] :
( B
!= ( plus_plus @ TA @ A @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_224_less__eqE) ).
thf(341,plain,
! [TA: $tType] :
( ( canoni770627133id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ A @ B )
=> ~ ! [C: TA] :
( B
!= ( plus_plus @ TA @ A @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(105,axiom,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ A )
= ( zero_zero @ a ) )
=> ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( top_top @ ( set @ real ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_75_rev_Ofixpoint__sol_I1_J) ).
thf(506,plain,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( uminus_uminus @ ( a > a ) @ f @ A )
= ( zero_zero @ a ) )
=> ( ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( top_top @ ( set @ real ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(159,axiom,
! [A: a] :
( ( member @ a @ A @ x )
=> ( member @ real @ ( zero_zero @ real ) @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_63_rev_Oexistence__ivl__zero) ).
thf(664,plain,
! [A: a] :
( ( member @ a @ A @ x )
=> ( member @ real @ ( zero_zero @ real ) @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[159]) ).
thf(77,axiom,
! [TA: $tType] :
( ( one @ TA )
=> ! [A: TA] :
( ( ( one_one @ TA )
= A )
= ( A
= ( one_one @ TA ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_26_one__reorient) ).
thf(400,plain,
! [TA: $tType] :
( ( one @ TA )
=> ! [A: TA] :
( ( ( one_one @ TA )
= A )
= ( A
= ( one_one @ TA ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(167,axiom,
! [TA: $tType] :
( ( zero_less_one @ TA )
=> ( ord_less @ TA @ ( zero_zero @ TA ) @ ( one_one @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_35_zero__less__one) ).
thf(696,plain,
! [TA: $tType] :
( ( zero_less_one @ TA )
=> ( ord_less @ TA @ ( zero_zero @ TA ) @ ( one_one @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[167]) ).
thf(794,plain,
! [TA: $tType] :
( ( ( zero_zero @ TA )
!= ( one_one @ TA ) )
| ~ $true
| ( ( zero_neq_one @ real )
!= ( zero_neq_one @ TA ) ) ),
inference(paramod_ordered,[status(thm)],[617,658]) ).
thf(795,plain,
! [TA: $tType] :
( ( ( zero_zero @ TA )
!= ( one_one @ TA ) )
| ( ( zero_neq_one @ real )
!= ( zero_neq_one @ TA ) ) ),
inference(simp,[status(thm)],[794]) ).
thf(796,plain,
( ( zero_zero @ real )
!= ( one_one @ real ) ),
inference(pattern_uni,[status(thm)],[795:[bind_type(TA,$thf( real ))]]) ).
thf(80,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( member @ a @ B @ x ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_106_local_Omem__existence__ivl__iv__defined_I2_J) ).
thf(415,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( member @ a @ B @ x ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(58,axiom,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( ord_less @ TA @ B @ ( zero_zero @ TA ) )
=> ( ord_less @ TA @ ( plus_plus @ TA @ A @ B ) @ ( zero_zero @ TA ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_248_add__nonpos__neg) ).
thf(332,plain,
! [TA: $tType] :
( ( ordere216010020id_add @ TA )
=> ! [A: TA,B: TA] :
( ( ord_less_eq @ TA @ A @ ( zero_zero @ TA ) )
=> ( ( ord_less @ TA @ B @ ( zero_zero @ TA ) )
=> ( ord_less @ TA @ ( plus_plus @ TA @ A @ B ) @ ( zero_zero @ TA ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(129,axiom,
member @ a @ p @ ( line_open_segment @ a @ a2 @ b ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_assms_I4_J) ).
thf(575,plain,
member @ a @ p @ ( line_open_segment @ a @ a2 @ b ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(137,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( member @ real @ A @ ( top_top @ ( set @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_58_local_Omem__existence__ivl__subset) ).
thf(596,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( member @ real @ A @ ( top_top @ ( set @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[137]) ).
thf(89,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ( abs_abs @ TA @ A )
= ( zero_zero @ TA ) )
= ( A
= ( zero_zero @ TA ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_13_abs__eq__0) ).
thf(442,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA] :
( ( ( abs_abs @ TA @ A )
= ( zero_zero @ TA ) )
= ( A
= ( zero_zero @ TA ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(103,axiom,
! [A: a,B: a] :
( ( poinca272511729egment @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
= ( poinca272511729egment @ a @ f @ x @ A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_48_rev__transversal__segment) ).
thf(501,plain,
! [A: a,B: a] :
( ( poinca272511729egment @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
= ( poinca272511729egment @ a @ f @ x @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(75,axiom,
! [A: real,B: a,C: real] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( ( member @ real @ C @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) ) )
=> ( member @ real @ ( plus_plus @ real @ A @ C ) @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_151_local_Orev_Oexistence__ivl__trans) ).
thf(395,plain,
! [A: real,B: a,C: real] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) )
=> ( ( member @ real @ C @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B @ A ) ) )
=> ( member @ real @ ( plus_plus @ real @ A @ C ) @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(147,axiom,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_110_local_Omem__existence__ivl__iv__defined_I1_J) ).
thf(624,plain,
! [A: real,B: a] :
( ( member @ real @ A @ ( auto_l1112008849e_ivl0 @ a @ f @ x @ B ) )
=> ( member @ real @ ( zero_zero @ real ) @ ( top_top @ ( set @ real ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[147]) ).
thf(54,axiom,
! [TA: $tType] :
( ( zero @ TA )
=> ( zero @ ( set @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Set_Oset___Groups_Ozero) ).
thf(322,plain,
! [TA: $tType] :
( ( zero @ TA )
=> ( zero @ ( set @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(99,axiom,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( period385816147_orbit @ a @ f @ x @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_60_rev_Oclosed__orbit__eq__rev) ).
thf(486,plain,
! [A: a] :
( ( period385816147_orbit @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A )
= ( period385816147_orbit @ a @ f @ x @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(60,axiom,
! [TA: $tType] :
( ( real_V2090557954_space @ TA )
=> ! [A: real,B: TA] :
( ( ord_less_eq @ real @ A @ ( zero_zero @ real ) )
=> ( ( elemen1815086676c_ball @ TA @ B @ A )
= ( bot_bot @ ( set @ TA ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_251_Elementary__Metric__Spaces_Oball__empty) ).
thf(337,plain,
! [TA: $tType] :
( ( real_V2090557954_space @ TA )
=> ! [A: real,B: TA] :
( ( ord_less_eq @ real @ A @ ( zero_zero @ real ) )
=> ( ( elemen1815086676c_ball @ TA @ B @ A )
= ( bot_bot @ ( set @ TA ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(96,axiom,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( f @ A )
= ( zero_zero @ a ) )
=> ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ A )
= ( top_top @ ( set @ real ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_67_fixpoint__sol_I1_J) ).
thf(469,plain,
! [A: a] :
( ( member @ a @ A @ x )
=> ( ( ( f @ A )
= ( zero_zero @ a ) )
=> ( ( auto_l1112008849e_ivl0 @ a @ f @ x @ A )
= ( top_top @ ( set @ real ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(11,axiom,
neg_numeral @ real,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Num_Oneg__numeral) ).
thf(215,plain,
neg_numeral @ real,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(150,axiom,
! [A: a,B: real] :
( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
= ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( uminus_uminus @ real @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_140_rev__eq__flow) ).
thf(639,plain,
! [A: a,B: real] :
( ( auto_ll_on_flow0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A @ B )
= ( auto_ll_on_flow0 @ a @ f @ x @ A @ ( uminus_uminus @ real @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[150]) ).
thf(163,axiom,
! [A: a,B: real] :
( ( period862636932_orbit @ a @ f @ x @ A )
=> ( ( f @ ( auto_ll_on_flow0 @ a @ f @ x @ A @ B ) )
!= ( zero_zero @ a ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_38_periodic__orbit__imp__flow0__regular) ).
thf(676,plain,
! [A: a,B: real] :
( ( period862636932_orbit @ a @ f @ x @ A )
=> ( ( f @ ( auto_ll_on_flow0 @ a @ f @ x @ A @ B ) )
!= ( zero_zero @ a ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[163]) ).
thf(93,axiom,
! [TA: $tType] :
( ( linordered_idom @ TA )
=> ( ( abs_abs @ TA @ ( one_one @ TA ) )
= ( one_one @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_33_abs__one) ).
thf(454,plain,
! [TA: $tType] :
( ( linordered_idom @ TA )
=> ( ( abs_abs @ TA @ ( one_one @ TA ) )
= ( one_one @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(20,axiom,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA,B: TA] :
( ( abs_abs @ TA @ ( plus_plus @ TA @ ( abs_abs @ TA @ A ) @ ( abs_abs @ TA @ B ) ) )
= ( plus_plus @ TA @ ( abs_abs @ TA @ A ) @ ( abs_abs @ TA @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_174_abs__add__abs) ).
thf(232,plain,
! [TA: $tType] :
( ( ordere142940540dd_abs @ TA )
=> ! [A: TA,B: TA] :
( ( abs_abs @ TA @ ( plus_plus @ TA @ ( abs_abs @ TA @ A ) @ ( abs_abs @ TA @ B ) ) )
= ( plus_plus @ TA @ ( abs_abs @ TA @ A ) @ ( abs_abs @ TA @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(49,axiom,
! [A: a] : ( initia826609931terval @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_128_rev_Omvar_Ointerval__axioms) ).
thf(309,plain,
! [A: a] : ( initia826609931terval @ ( auto_l1112008849e_ivl0 @ a @ ( uminus_uminus @ ( a > a ) @ f ) @ x @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(157,axiom,
! [A: real] :
( ( ord_less @ real @ ( abs_abs @ real @ A ) @ ( one_one @ real ) )
=> ( ord_less @ real @ A @ ( one_one @ real ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_17_gt__one__absI) ).
thf(659,plain,
! [A: real] :
( ( ord_less @ real @ ( abs_abs @ real @ A ) @ ( one_one @ real ) )
=> ( ord_less @ real @ A @ ( one_one @ real ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[157]) ).
thf(2078,plain,
$false,
inference(e,[status(thm)],[645,347,846,249,666,683,276,308,247,202,523,582,762,533,550,500,472,698,340,709,417,288,320,436,724,570,372,504,587,702,344,559,606,228,448,261,216,475,756,348,353,602,243,849,527,206,734,221,380,529,661,793,366,512,439,334,746,302,392,429,815,229,252,197,329,757,551,710,324,852,435,583,830,285,224,317,650,403,356,610,420,519,742,225,537,669,642,489,590,706,554,753,457,721,605,237,244,311,541,398,718,773,586,618,425,279,296,375,733,562,423,694,843,545,579,291,445,572,713,466,236,540,672,604,406,219,509,599,451,567,271,208,213,621,240,198,636,306,299,267,653,658,490,680,548,255,648,749,754,194,617,516,327,739,263,705,282,199,576,744,656,613,727,314,627,203,759,218,363,556,304,258,351,731,235,383,432,833,273,735,564,210,294,341,506,195,664,400,696,796,415,332,575,596,200,442,501,395,624,322,486,337,469,215,639,676,454,232,309,659]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP147^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % 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.10/0.20 % Computer : n009.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 20:01:05 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 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
% 0.86/0.80 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.34/1.21 % [INFO] Parsing done (406ms).
% 2.34/1.22 % [INFO] Running in sequential loop mode.
% 3.40/1.60 % [INFO] eprover registered as external prover.
% 3.40/1.61 % [INFO] Scanning for conjecture ...
% 3.59/1.78 % [INFO] Found a conjecture (or negated_conjecture) and 319 axioms. Running axiom selection ...
% 4.09/1.96 % [INFO] Axiom selection finished. Selected 191 axioms (removed 128 axioms).
% 5.07/2.23 % [INFO] Problem is higher-order (TPTP THF).
% 5.07/2.26 % [INFO] Type checking passed.
% 5.07/2.26 % [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 ...
% 47.15/11.80 % External prover 'e' found a proof!
% 47.15/11.80 % [INFO] Killing All external provers ...
% 47.15/11.80 % Time passed: 11454ms (effective reasoning time: 10578ms)
% 47.15/11.81 % Solved by 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)>
% 47.15/11.81 % Axioms used in derivation (191): fact_74_local_Orev_Oexistence__ivl__initial__time, fact_41_rev_Otransversal__segment__exists, fact_12_abs__0__eq, fact_216_add__nonpos__eq__0__iff, fact_36_abs__not__less__zero, fact_63_rev_Oexistence__ivl__zero, tcon_Real_Oreal___Rings_Ozero__less__one, fact_85_rev_Operiodic__orbit__period_I2_J, fact_110_local_Omem__existence__ivl__iv__defined_I1_J, fact_157_add__eq__0__iff__both__eq__0, fact_6_assms_I3_J, fact_108_flow0__defined, fact_143_recurrence__time__flip__sign_I2_J, fact_128_rev_Omvar_Ointerval__axioms, fact_51_fixed__point__imp__closed__orbit__period__zero_I1_J, fact_16_fixpoint__sol_I2_J, fact_109_local_Oflow__in__domain, fact_246_add__strict__increasing, fact_141_rev_Orev__eq__flow, fact_2_assms_I4_J, fact_210_le__numeral__extra_I4_J, fact_28_gr__implies__not__zero, tcon_Real_Oreal___Groups_Ozero_10, tcon_Real_Oreal___Real__Vector__Spaces_Ometric__space_5, fact_154_le__zero__eq, tcon_Real_Oreal___Groups_Oordered__ab__group__add__abs, fact_69_closed__orbit__global__existence, fact_174_abs__add__abs, fact_80_rev_Ofixed__point__imp__closed__orbit__period__zero_I2_J, fact_19_transversal__segment__commute, fact_86_rev_Oclosed__orbit__periodic, fact_56_existence__ivl__zero, fact_44_Collect__mem__eq, fact_31_zero__neq__one, fact_25_linorder__neqE__linordered__idom, fact_199_abs__of__nonpos, tcon_Set_Oset___Groups_Oone, fact_39_fixed__point__imp__closed__orbit__period__zero_I2_J, fact_38_periodic__orbit__imp__flow0__regular, fact_50_rev_Otransversal__segment__commute, fact_245_add__strict__increasing2, fact_129_mvar_Ointerval__axioms, fact_21_abs__abs, fact_123_abs__less__iff, fact_208_abs__triangle__ineq, fact_60_rev_Oclosed__orbit__eq__rev, fact_197_add__neg__numeral__special_I7_J, tcon_Real_Oreal___Rings_Ozero__neq__one, fact_70_closed__orbitI, tcon_Real_Oreal___Groups_Oordered__comm__monoid__add, fact_220_le__iff__add, fact_226_add__decreasing, fact_1__092_060open_062p_A_092_060in_062_AX_092_060close_062, fact_8_zero__less__abs__iff, fact_49_rev_Otransversal__segment__reverse, fact_42_rev_Ofixpoint__sol_I2_J, fact_95_abs__minus, fact_82_periodic__orbitI, fact_71_rev_Ofixed__point__imp__closed__orbit__period__zero_I1_J, fact_7_centre__in__ball, fact_247_add__pos__nonneg, fact_250_add__neg__nonpos, fact_22_transversal__segment__exists, tcon_Real_Oreal___Groups_Oordered__cancel__comm__monoid__add, fact_202_local_Orev_Oexistence__ivl__undefined, fact_43_mem__Collect__eq, fact_251_Elementary__Metric__Spaces_Oball__empty, fact_140_rev__eq__flow, fact_156_zero__eq__add__iff__both__eq__0, fact_133_rev_Oclosed__orbit__period__nonneg, fact_30_gr__zeroI, fact_76_local_Orev_Oflow__undefined0, fact_72_periodic__orbit__period_I2_J, fact_130_abs__neg__one, fact_17_gt__one__absI, fact_125_abs__of__neg, fact_29_not__less__zero, fact_195_abs__of__nonneg, fact_194_abs__le__self__iff, fact_24_zero__reorient, fact_124_abs__if, fact_96_abs__minus__cancel, fact_79_rev_Oclosed__orbitI, fact_78_rev_Oclosed__orbit__global__existence, fact_149_local_Orev_Oflow__trans, fact_11_abs__0, fact_5_assms_I1_J, fact_122_abs__eq__iff, fact_107_local_Orev_Omem__existence__ivl__iv__defined_I2_J, fact_81_rev_Operiodic__orbit__imp__flow0__regular, fact_217_add__nonneg__eq__0__iff, tcon_Real_Oreal___Rings_Olinordered__nonzero__semiring, fact_170_closed__orbitE, fact_4_that, fact_73_closed__orbit__periodic, fact_206_local_Orev_Oexistence__ivl__empty1, tcon_Real_Oreal___Groups_Oab__group__add, fact_152_local_Oexistence__ivl__notempty, fact_145_rev_Orecurrence__time__flip__sign_I2_J, fact_114_local_Orev_Oflow__in__domain, fact_200_ball__eq__empty, fact_94_rev_Oclosed__orbit__def, fact_127_rev_O_092_060alpha_062__limit__point__eq__rev, fact_53_closed__orbit__in__domain, fact_153_closed__orbit__period__nonneg, fact_58_local_Omem__existence__ivl__subset, fact_59_flow0__cong, fact_15_not__gr__zero, fact_35_zero__less__one, fact_222_add__decreasing2, fact_64_local_Oexistence__ivl__initial__time, tcon_Real_Oreal___Rings_Oidom__abs__sgn, fact_201_local_Oexistence__ivl__undefined, fact_148_local_Oexistence__ivl__trans, fact_113_rev_Oflow0__defined, fact_219_add__nonneg__nonneg, fact_3__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062d_At_O_A_092_060lbrakk_0620_A_060_Ad_059_Acontinuous__on_A_Iball_Ap_Ad_J_At_059_A_092_060And_062y_O_Ay_A_092_060in_062_Aball_Ap_Ad_A_092_060Longrightarrow_062_Aflow0_Ay_A_It_Ay_J_A_092_060in_062_A_123a_060_N_N_060b_125_059_A_092_060And_062y_O_Ay_A_092_060in_062_Aball_Ap_Ad_A_092_060Longrightarrow_062_A_092_060bar_062t_Ay_092_060bar_062_A_060_A1_059_Acontinuous__on_A_Iball_Ap_Ad_J_At_059_At_Ap_A_061_A0_092_060rbrakk_062_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062, fact_99_rev_Oclosed__orbit__period__zero__fixed__point, fact_111_local_Oexistence__ivl__initial__time__iff, fact_13_abs__eq__0, fact_68_rev_Oclosed__orbit__flow0, fact_203_local_Oexistence__ivl__empty__iff, fact_147_local_Oexistence__ivl__trans_H, fact_112_local_Oflow__initial__time, fact_218_add__nonpos__nonpos, fact_207_is__num__normalize_I8_J, fact_66_rev_Oflow0__cong, fact_61_rev_Oclosed__orbit__in__domain, fact_62_closed__orbit__flow0, fact_151_local_Orev_Oexistence__ivl__trans, fact_67_fixpoint__sol_I1_J, fact_18_transversal__segment__reverse, fact_65_local_Orev_Omem__existence__ivl__subset, fact_27_zero__less__iff__neq__zero, fact_98_rev_Operiodic__orbit__period_I1_J, fact_77_closed__orbit__def, fact_146_local_Oflow__trans, fact_97_rev_Operiodic__orbitI, fact_137_interval__axioms, fact_57_rev_Oexistence__ivl0__cong, fact_225_add__increasing, fact_20_abs__idempotent, tcon_Real_Oreal___Rings_Olinordered__idom, fact_221_add__increasing2, fact_248_add__nonpos__neg, fact_198_add__neg__numeral__special_I8_J, fact_142_recurrence__time__flip__sign_I1_J, tcon_Real_Oreal___Rings_Oabs__if, fact_33_abs__one, fact_48_rev__transversal__segment, fact_45_Collect__cong, fact_10_abs__1, fact_150_local_Orev_Oexistence__ivl__trans_H, tcon_Real_Oreal___Num_Oneg__numeral, fact_37_abs__of__pos, fact_9_cross__time__continuous, fact_116_local_Orev_Oexistence__ivl__initial__time__iff, fact_101_rev_Operiodic__orbit__def, fact_47_local_Oflow__undefined0, tcon_Real_Oreal___Groups_Oone_11, fact_52_existence__ivl0__cong, fact_34_not__one__less__zero, fact_0_rev_Oopen__segment__trichotomy, fact_115_local_Orev_Omem__existence__ivl__iv__defined_I1_J, fact_209_le__numeral__extra_I3_J, fact_193_abs__le__zero__iff, fact_249_add__nonneg__pos, fact_92_local_Orev_Oflow__initial__time__if, fact_32_abs__eq__0__iff, fact_132_local_Orev_Oexistence__ivl__notempty, fact_205_local_Orev_Oexistence__ivl__empty__iff, fact_224_less__eqE, tcon_Real_Oreal___Rings_Olinordered__ring, fact_204_local_Oexistence__ivl__empty1, fact_100_periodic__orbit__def, fact_126__092_060alpha_062__limit__point__eq__rev, fact_211_is__num__normalize_I1_J, fact_83_periodic__orbit__period_I1_J, conj_0, fact_84_closed__orbit__period__zero__fixed__point, fact_14_abs__zero, fact_117_local_Orev_Oflow__initial__time, fact_131_rev_Oclosed__orbitE, fact_40_local_Oflow__initial__time__if, fact_26_one__reorient, tcon_Set_Oset___Groups_Ozero, fact_171_minus__add__distrib, fact_196_ball__trivial, fact_106_local_Omem__existence__ivl__iv__defined_I2_J, fact_75_rev_Ofixpoint__sol_I1_J, fact_144_rev_Orecurrence__time__flip__sign_I1_J
% 47.15/11.81 % No. of inferences in proof: 429
% 47.15/11.81 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 11454 ms resp. 10578 ms w/o parsing
% 48.71/12.04 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 48.71/12.04 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------