%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP113^1 : 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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:06:48 AM UTC 2026
% Result : Theorem 10.65s 3.66s
% Output : Refutation 11.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 136
% Syntax : Number of formulae : 274 ( 112 unt; 0 typ; 0 def)
% Number of atoms : 752 ( 204 equ; 6 cnn)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 1866 ( 104 ~; 22 |; 30 &;1376 @)
% ( 0 <=>; 334 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 6 avg)
% Number of types : 26 ( 25 usr)
% Number of type conns : 40 ( 40 >; 0 *; 0 +; 0 <<)
% Number of symbols : 38 ( 35 usr; 17 con; 0-2 aty)
% Number of variables : 674 ( 50 ^; 608 !; 16 ?; 674 :)
% Comments :
%------------------------------------------------------------------------------
thf(produc2021989178_set_a_type,type,
produc2021989178_set_a: $tType ).
thf(produc211508562a_real_type,type,
produc211508562a_real: $tType ).
thf(produc1312517202t_real_type,type,
produc1312517202t_real: $tType ).
thf(produc304417648_set_a_type,type,
produc304417648_set_a: $tType ).
thf(produc509513372a_real_type,type,
produc509513372a_real: $tType ).
thf(produc25772804_set_a_type,type,
produc25772804_set_a: $tType ).
thf(set_Pr1158285382l_real_type,type,
set_Pr1158285382l_real: $tType ).
thf(produc792423270l_real_type,type,
produc792423270l_real: $tType ).
thf(produc1931999653t_real_type,type,
produc1931999653t_real: $tType ).
thf(produc232195311t_real_type,type,
produc232195311t_real: $tType ).
thf(produc1350454001_set_a_type,type,
produc1350454001_set_a: $tType ).
thf(set_Pr147102617l_real_type,type,
set_Pr147102617l_real: $tType ).
thf(produc1691597095_set_a_type,type,
produc1691597095_set_a: $tType ).
thf(set_Pr1928503567a_real_type,type,
set_Pr1928503567a_real: $tType ).
thf(produc957004601l_real_type,type,
produc957004601l_real: $tType ).
thf(produc581916509al_nat_type,type,
produc581916509al_nat: $tType ).
thf(produc845587165t_real_type,type,
produc845587165t_real: $tType ).
thf(product_prod_nat_nat_type,type,
product_prod_nat_nat: $tType ).
thf(product_prod_a_real_type,type,
product_prod_a_real: $tType ).
thf(set_real_type,type,
set_real: $tType ).
thf(extended_ereal_type,type,
extended_ereal: $tType ).
thf(set_a_type,type,
set_a: $tType ).
thf(real_type,type,
real: $tType ).
thf(nat_type,type,
nat: $tType ).
thf(a_type,type,
a: $tType ).
thf(elemen1695521870a_real_decl,type,
elemen1695521870a_real: set_Pr1928503567a_real > set_Pr1928503567a_real ).
thf(elementary_closure_a_decl,type,
elementary_closure_a: set_a > set_a ).
thf(zero_zero_real_decl,type,
zero_zero_real: real ).
thf(lower_930854854raph_a_decl,type,
lower_930854854raph_a: set_a > ( a > extended_ereal ) > set_Pr1928503567a_real ).
thf(ord_less_real_decl,type,
ord_less_real: real > real > $o ).
thf(ord_less_set_a_decl,type,
ord_less_set_a: set_a > set_a > $o ).
thf(ord_less_eq_real_decl,type,
ord_less_eq_real: real > real > $o ).
thf(ord_less_eq_set_a_decl,type,
ord_less_eq_set_a: set_a > set_a > $o ).
thf(top_to1567080838real_o_decl,type,
top_to1567080838real_o: product_prod_a_real > $o ).
thf(top_top_a_o_decl,type,
top_top_a_o: a > $o ).
thf(top_to345582004_set_a_decl,type,
top_to345582004_set_a: produc25772804_set_a ).
thf(top_to1153982881_set_a_decl,type,
top_to1153982881_set_a: produc1350454001_set_a ).
thf(top_to724687040_set_a_decl,type,
top_to724687040_set_a: produc304417648_set_a ).
thf(top_to829322572a_real_decl,type,
top_to829322572a_real: produc509513372a_real ).
thf(top_to35724191t_real_decl,type,
top_to35724191t_real: produc232195311t_real ).
thf(top_to1477940855_set_a_decl,type,
top_to1477940855_set_a: produc1691597095_set_a ).
thf(top_to2138011583a_real_decl,type,
top_to2138011583a_real: set_Pr1928503567a_real ).
thf(top_top_set_real_decl,type,
top_top_set_real: set_real ).
thf(top_top_set_a_decl,type,
top_top_set_a: set_a ).
thf(produc1220567734_set_a_decl,type,
produc1220567734_set_a: set_Pr1928503567a_real > set_a > produc25772804_set_a ).
thf(produc190993315_set_a_decl,type,
produc190993315_set_a: set_real > set_a > produc1350454001_set_a ).
thf(produc272677600_set_a_decl,type,
produc272677600_set_a: set_a > produc1691597095_set_a > produc304417648_set_a ).
thf(produc383769494a_real_decl,type,
produc383769494a_real: set_a > set_Pr1928503567a_real > produc509513372a_real ).
thf(produc1266579561t_real_decl,type,
produc1266579561t_real: set_a > set_real > produc232195311t_real ).
thf(product_Pair_a_real_decl,type,
product_Pair_a_real: a > real > product_prod_a_real ).
thf(real_V404783528a_real_decl,type,
real_V404783528a_real: product_prod_a_real > product_prod_a_real > real ).
thf(collec1714955950a_real_decl,type,
collec1714955950a_real: ( product_prod_a_real > $o ) > set_Pr1928503567a_real ).
thf(collect_a_decl,type,
collect_a: ( a > $o ) > set_a ).
thf(member1103263856a_real_decl,type,
member1103263856a_real: product_prod_a_real > set_Pr1928503567a_real > $o ).
thf(e_decl,type,
e: real ).
thf(f_decl,type,
f: a > extended_ereal ).
thf(thesis_decl,type,
thesis: $o ).
thf(x_decl,type,
x: a ).
thf(y_decl,type,
y: real ).
thf(z_decl,type,
z: real ).
thf(53,axiom,
! [A: real,B: real,C: real] :
( ( A = B )
=> ( ( ord_less_eq_real @ B @ C )
=> ( ord_less_eq_real @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_88_ord__eq__le__trans) ).
thf(307,plain,
! [A: real,B: real,C: real] :
( ( A = B )
=> ( ( ord_less_eq_real @ B @ C )
=> ( ord_less_eq_real @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(1,conjecture,
thesis,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
thf(2,negated_conjecture,
~ thesis,
inference(neg_conjecture,[status(cth)],[1]) ).
thf(138,plain,
~ thesis,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(64,axiom,
! [A: real,B: real,C: real > real,D: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_real @ ( C @ B ) @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_eq_real @ E @ F )
=> ( ord_less_eq_real @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_real @ ( C @ A ) @ D ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_174_order__le__less__subst2) ).
thf(347,plain,
! [A: real,B: real,C: real > real,D: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_real @ ( C @ B ) @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_eq_real @ E @ F )
=> ( ord_less_eq_real @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_real @ ( C @ A ) @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(96,axiom,
! [A: product_prod_a_real > $o,B: product_prod_a_real] :
( ! [C: a,D: real] : ( A @ ( product_Pair_a_real @ C @ D ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_278_old_Oprod_Oinducts) ).
thf(468,plain,
! [A: product_prod_a_real > $o,B: product_prod_a_real] :
( ! [C: a,D: real] : ( A @ ( product_Pair_a_real @ C @ D ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(120,axiom,
! [A: real] :
~ ( ord_less_real @ A @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_219_dual__order_Oirrefl) ).
thf(555,plain,
! [A: real] :
~ ( ord_less_real @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[120]) ).
thf(60,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ C )
=> ( ord_less_eq_real @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_94_order__trans) ).
thf(333,plain,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ C )
=> ( ord_less_eq_real @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(33,axiom,
( ord_less_eq_real
= ( ^ [A: real,B: real] :
( ( ord_less_real @ A @ B )
| ( A = B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_134_order_Oorder__iff__strict) ).
thf(249,plain,
( ord_less_eq_real
= ( ^ [A: real,B: real] :
( ( ord_less_real @ A @ B )
| ( A = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(99,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_253_order_Oasym) ).
thf(481,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(65,axiom,
! [A: real,B: real,C: real > real,D: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_eq_real @ ( C @ B ) @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_real @ E @ F )
=> ( ord_less_real @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_real @ ( C @ A ) @ D ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_166_order__less__le__subst2) ).
thf(352,plain,
! [A: real,B: real,C: real > real,D: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_eq_real @ ( C @ B ) @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_real @ E @ F )
=> ( ord_less_real @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_real @ ( C @ A ) @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(83,axiom,
( ( member1103263856a_real @ ( product_Pair_a_real @ x @ y ) @ ( elemen1695521870a_real @ ( lower_930854854raph_a @ top_top_set_a @ f ) ) )
& ( ord_less_eq_real @ y @ z ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_xy) ).
thf(408,plain,
( ( member1103263856a_real @ ( product_Pair_a_real @ x @ y ) @ ( elemen1695521870a_real @ ( lower_930854854raph_a @ top_top_set_a @ f ) ) )
& ( ord_less_eq_real @ y @ z ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(112,axiom,
! [A: product_prod_a_real,B: set_Pr1928503567a_real,C: product_prod_a_real] :
( ( member1103263856a_real @ A @ B )
=> ( ( member1103263856a_real @ C @ B )
=> ( ( A = C )
= ( ! [D: product_prod_a_real] :
( ( member1103263856a_real @ D @ B )
=> ( ( real_V404783528a_real @ A @ D )
= ( real_V404783528a_real @ C @ D ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_37_metric__eq__thm) ).
thf(523,plain,
! [A: product_prod_a_real,B: set_Pr1928503567a_real,C: product_prod_a_real] :
( ( member1103263856a_real @ A @ B )
=> ( ( member1103263856a_real @ C @ B )
=> ( ( A = C )
= ( ! [D: product_prod_a_real] :
( ( member1103263856a_real @ D @ B )
=> ( ( real_V404783528a_real @ A @ D )
= ( real_V404783528a_real @ C @ D ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(95,axiom,
! [A: real > real > $o,B: real,C: real] :
( ! [D: real,E: real] :
( ( ord_less_real @ D @ E )
=> ( A @ D @ E ) )
=> ( ! [D: real] : ( A @ D @ D )
=> ( ! [D: real,E: real] :
( ( A @ E @ D )
=> ( A @ D @ E ) )
=> ( A @ B @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_212_linorder__less__wlog) ).
thf(449,plain,
! [A: real > real > $o,B: real,C: real] :
( ! [D: real,E: real] :
( ( ord_less_real @ D @ E )
=> ( A @ D @ E ) )
=> ( ! [D: real] : ( A @ D @ D )
=> ( ! [D: real,E: real] :
( ( A @ E @ D )
=> ( A @ D @ E ) )
=> ( A @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(32,axiom,
( ord_less_eq_real
= ( ^ [A: real,B: real] :
( ( ord_less_real @ A @ B )
| ( A = B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_342_less__eq__real__def) ).
thf(247,plain,
( ord_less_eq_real
= ( ^ [A: real,B: real] :
( ( ord_less_real @ A @ B )
| ( A = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(75,axiom,
! [A: product_prod_a_real,B: product_prod_a_real] :
( ( A != B )
=> ( ord_less_real @ zero_zero_real @ ( real_V404783528a_real @ A @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_203_dist__pos__lt) ).
thf(379,plain,
! [A: product_prod_a_real,B: product_prod_a_real] :
( ( A != B )
=> ( ord_less_real @ zero_zero_real @ ( real_V404783528a_real @ A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(108,axiom,
! [A: product_prod_a_real,B: product_prod_a_real,C: real] :
( ( ord_less_real @ ( real_V404783528a_real @ A @ B ) @ C )
=> ( ord_less_real @ ( real_V404783528a_real @ B @ A ) @ C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_13_dist__commute__lessI) ).
thf(511,plain,
! [A: product_prod_a_real,B: product_prod_a_real,C: real] :
( ( ord_less_real @ ( real_V404783528a_real @ A @ B ) @ C )
=> ( ord_less_real @ ( real_V404783528a_real @ B @ A ) @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(39,axiom,
! [A: real,B: real] :
( ( ~ ( ord_less_real @ A @ B ) )
= ( ord_less_eq_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_162_not__less) ).
thf(269,plain,
! [A: real,B: real] :
( ( ~ ( ord_less_real @ A @ B ) )
= ( ord_less_eq_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(22,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( ord_less_eq_real @ A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_124_order_Ostrict__implies__order) ).
thf(202,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( ord_less_eq_real @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(77,axiom,
! [A: real] :
? [B: real] : ( ord_less_real @ B @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_261_lt__ex) ).
thf(385,plain,
! [A: real] :
? [B: real] : ( ord_less_real @ B @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(4,axiom,
( ord_less_real
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
& ( A != B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_132_order_Ostrict__iff__order) ).
thf(142,plain,
( ord_less_real
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
& ( A != B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(16,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ C @ A )
=> ( ord_less_eq_real @ C @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_100_dual__order_Otrans) ).
thf(185,plain,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ C @ A )
=> ( ord_less_eq_real @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(85,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_232_less__imp__not__eq) ).
thf(417,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(50,axiom,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
| ( ord_less_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_146_le__less__linear) ).
thf(301,plain,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
| ( ord_less_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(91,axiom,
( ( elementary_closure_a @ top_top_set_a )
= top_top_set_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_295_closure__UNIV) ).
thf(436,plain,
( ( elementary_closure_a @ top_top_set_a )
= top_top_set_a ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(72,axiom,
( ( (=) @ real )
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ B @ A )
& ( ord_less_eq_real @ A @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_108_dual__order_Oeq__iff) ).
thf(372,plain,
( ( (=) @ real )
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ B @ A )
& ( ord_less_eq_real @ A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(66,axiom,
! [A: real,B: real] :
( ~ ( ord_less_real @ A @ B )
=> ( ord_less_eq_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_186_leI) ).
thf(357,plain,
! [A: real,B: real] :
( ~ ( ord_less_real @ A @ B )
=> ( ord_less_eq_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(20,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_150_less__le__trans) ).
thf(196,plain,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(9,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_eq_real @ C @ A )
=> ( ord_less_real @ C @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_128_dual__order_Ostrict__trans2) ).
thf(157,plain,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_eq_real @ C @ A )
=> ( ord_less_real @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(86,axiom,
( top_to35724191t_real
= ( produc1266579561t_real @ top_top_set_a @ top_top_set_real ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_15_top__prod__def) ).
thf(421,plain,
( top_to35724191t_real
= ( produc1266579561t_real @ top_top_set_a @ top_top_set_real ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(28,axiom,
! [A: product_prod_a_real,B: set_Pr1928503567a_real] :
( ( member1103263856a_real @ A @ ( elemen1695521870a_real @ B ) )
= ( ! [C: real] :
( ( ord_less_real @ zero_zero_real @ C )
=> ? [D: product_prod_a_real] :
( ( member1103263856a_real @ D @ B )
& ( ord_less_eq_real @ ( real_V404783528a_real @ D @ A ) @ C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_300_closure__approachable__le) ).
thf(228,plain,
! [A: product_prod_a_real,B: set_Pr1928503567a_real] :
( ( member1103263856a_real @ A @ ( elemen1695521870a_real @ B ) )
= ( ! [C: real] :
( ( ord_less_real @ zero_zero_real @ C )
=> ? [D: product_prod_a_real] :
( ( member1103263856a_real @ D @ B )
& ( ord_less_eq_real @ ( real_V404783528a_real @ D @ A ) @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(46,axiom,
( ( elemen1695521870a_real @ top_to2138011583a_real )
= top_to2138011583a_real ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_297_closure__UNIV) ).
thf(289,plain,
( ( elemen1695521870a_real @ top_to2138011583a_real )
= top_to2138011583a_real ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(37,axiom,
! [A: real,B: real > real,C: real,D: real] :
( ( ord_less_eq_real @ A @ ( B @ C ) )
=> ( ( ord_less_real @ C @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_real @ E @ F )
=> ( ord_less_real @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_real @ A @ ( B @ D ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_178_order__le__less__subst1) ).
thf(261,plain,
! [A: real,B: real > real,C: real,D: real] :
( ( ord_less_eq_real @ A @ ( B @ C ) )
=> ( ( ord_less_real @ C @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_real @ E @ F )
=> ( ord_less_real @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_real @ A @ ( B @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(132,axiom,
ord_less_real @ zero_zero_real @ e,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__092_060open_0620_A_060_Ae_092_060close_062) ).
thf(591,plain,
ord_less_real @ zero_zero_real @ e,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[132]) ).
thf(56,axiom,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ A )
=> ( B = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_110_dual__order_Oantisym) ).
thf(321,plain,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ A )
=> ( B = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(26,axiom,
! [A: real,B: real,C: real] :
( ( ( ord_less_eq_real @ A @ B )
=> ~ ( ord_less_eq_real @ B @ C ) )
=> ( ( ( ord_less_eq_real @ B @ A )
=> ~ ( ord_less_eq_real @ A @ C ) )
=> ( ( ( ord_less_eq_real @ A @ C )
=> ~ ( ord_less_eq_real @ C @ B ) )
=> ( ( ( ord_less_eq_real @ C @ B )
=> ~ ( ord_less_eq_real @ B @ A ) )
=> ( ( ( ord_less_eq_real @ B @ C )
=> ~ ( ord_less_eq_real @ C @ A ) )
=> ~ ( ( ord_less_eq_real @ C @ A )
=> ~ ( ord_less_eq_real @ A @ B ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_82_le__cases3) ).
thf(211,plain,
! [A: real,B: real,C: real] :
( ( ( ord_less_eq_real @ A @ B )
=> ~ ( ord_less_eq_real @ B @ C ) )
=> ( ( ( ord_less_eq_real @ B @ A )
=> ~ ( ord_less_eq_real @ A @ C ) )
=> ( ( ( ord_less_eq_real @ A @ C )
=> ~ ( ord_less_eq_real @ C @ B ) )
=> ( ( ( ord_less_eq_real @ C @ B )
=> ~ ( ord_less_eq_real @ B @ A ) )
=> ( ( ( ord_less_eq_real @ B @ C )
=> ~ ( ord_less_eq_real @ C @ A ) )
=> ~ ( ( ord_less_eq_real @ C @ A )
=> ~ ( ord_less_eq_real @ A @ B ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(35,axiom,
! [A: real,B: real] :
( ( ~ ( ord_less_eq_real @ A @ B ) )
= ( ord_less_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_164_not__le) ).
thf(253,plain,
! [A: real,B: real] :
( ( ~ ( ord_less_eq_real @ A @ B ) )
= ( ord_less_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(137,axiom,
! [A: a,B: real] :
( ( ( member1103263856a_real @ ( product_Pair_a_real @ A @ B ) @ ( lower_930854854raph_a @ top_top_set_a @ f ) )
& ( ord_less_real @ ( real_V404783528a_real @ ( product_Pair_a_real @ A @ B ) @ ( product_Pair_a_real @ x @ y ) ) @ e ) )
=> thesis ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(602,plain,
! [A: a,B: real] :
( ( ( member1103263856a_real @ ( product_Pair_a_real @ A @ B ) @ ( lower_930854854raph_a @ top_top_set_a @ f ) )
& ( ord_less_real @ ( real_V404783528a_real @ ( product_Pair_a_real @ A @ B ) @ ( product_Pair_a_real @ x @ y ) ) @ e ) )
=> thesis ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[137]) ).
thf(81,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_215_less__imp__not__less) ).
thf(397,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(88,axiom,
! [A: real,B: real] :
( ~ ( ord_less_real @ A @ B )
=> ( ( ~ ( ord_less_real @ B @ A ) )
= ( B = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_227_antisym__conv3) ).
thf(428,plain,
! [A: real,B: real] :
( ~ ( ord_less_real @ A @ B )
=> ( ( ~ ( ord_less_real @ B @ A ) )
= ( B = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(107,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_250_less__imp__neq) ).
thf(507,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(24,axiom,
( ord_less_eq_real
= ( ^ [A: real,B: real] :
( ( ord_less_real @ A @ B )
| ( B = A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_122_dual__order_Oorder__iff__strict) ).
thf(206,plain,
( ord_less_eq_real
= ( ^ [A: real,B: real] :
( ( ord_less_real @ A @ B )
| ( B = A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(113,axiom,
! [A: real,B: real] :
( ( A != B )
=> ( ~ ( ord_less_real @ A @ B )
=> ( ord_less_real @ B @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_257_neqE) ).
thf(527,plain,
! [A: real,B: real] :
( ( A != B )
=> ( ~ ( ord_less_real @ A @ B )
=> ( ord_less_real @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[113]) ).
thf(54,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ! [D: real] :
( ( ord_less_real @ A @ D )
=> ( ( ord_less_real @ D @ B )
=> ( ord_less_eq_real @ C @ D ) ) )
=> ( ord_less_eq_real @ C @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_127_dense__ge__bounded) ).
thf(312,plain,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ! [D: real] :
( ( ord_less_real @ A @ D )
=> ( ( ord_less_real @ D @ B )
=> ( ord_less_eq_real @ C @ D ) ) )
=> ( ord_less_eq_real @ C @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(122,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_248_less__asym) ).
thf(561,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[122]) ).
thf(79,axiom,
! [A: real,B: real] :
( ~ ( ord_less_real @ A @ B )
=> ( ( A != B )
=> ( ord_less_real @ B @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_221_linorder__cases) ).
thf(392,plain,
! [A: real,B: real] :
( ~ ( ord_less_real @ A @ B )
=> ( ( A != B )
=> ( ord_less_real @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(49,axiom,
! [A: real,B: real] :
( ! [C: real] :
( ( ord_less_real @ A @ C )
=> ( ord_less_eq_real @ B @ C ) )
=> ( ord_less_eq_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_149_dense__ge) ).
thf(297,plain,
! [A: real,B: real] :
( ! [C: real] :
( ( ord_less_real @ A @ C )
=> ( ord_less_eq_real @ B @ C ) )
=> ( ord_less_eq_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(41,axiom,
! [A: real,B: real] :
( ~ ( ord_less_eq_real @ A @ B )
=> ( ord_less_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_140_not__le__imp__less) ).
thf(275,plain,
! [A: real,B: real] :
( ~ ( ord_less_eq_real @ A @ B )
=> ( ord_less_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(135,axiom,
( top_to724687040_set_a
= ( produc272677600_set_a @ top_top_set_a @ top_to1477940855_set_a ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_22_top__prod__def) ).
thf(598,plain,
( top_to724687040_set_a
= ( produc272677600_set_a @ top_top_set_a @ top_to1477940855_set_a ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[135]) ).
thf(10,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ C )
=> ( ord_less_eq_real @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_80_order_Otrans) ).
thf(160,plain,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ C )
=> ( ord_less_eq_real @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(119,axiom,
! [A: product_prod_a_real] :
~ ! [B: a,C: real] :
( A
!= ( product_Pair_a_real @ B @ C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_280_old_Oprod_Oexhaust) ).
thf(551,plain,
! [A: product_prod_a_real] :
~ ! [B: a,C: real] :
( A
!= ( product_Pair_a_real @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[119]) ).
thf(57,axiom,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( A != B )
=> ( ord_less_real @ A @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_160_le__neq__trans) ).
thf(324,plain,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( A != B )
=> ( ord_less_real @ A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(17,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( ord_less_eq_real @ A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_118_dual__order_Ostrict__implies__order) ).
thf(188,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( ord_less_eq_real @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(12,axiom,
! [A: real,B: real,C: real > real,D: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ( C @ B )
= D )
=> ( ! [E: real,F: real] :
( ( ord_less_eq_real @ E @ F )
=> ( ord_less_eq_real @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_eq_real @ ( C @ A ) @ D ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_66_ord__le__eq__subst) ).
thf(169,plain,
! [A: real,B: real,C: real > real,D: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ( C @ B )
= D )
=> ( ! [E: real,F: real] :
( ( ord_less_eq_real @ E @ F )
=> ( ord_less_eq_real @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_eq_real @ ( C @ A ) @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(103,axiom,
! [A: real] :
? [B: real] : ( ord_less_real @ A @ B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_259_gt__ex) ).
thf(499,plain,
! [A: real] :
? [B: real] : ( ord_less_real @ A @ B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(36,axiom,
! [A: real,B: real > real,C: real,D: real] :
( ( ord_less_real @ A @ ( B @ C ) )
=> ( ( ord_less_eq_real @ C @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_eq_real @ E @ F )
=> ( ord_less_eq_real @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_real @ A @ ( B @ D ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_170_order__less__le__subst1) ).
thf(256,plain,
! [A: real,B: real > real,C: real,D: real] :
( ( ord_less_real @ A @ ( B @ C ) )
=> ( ( ord_less_eq_real @ C @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_eq_real @ E @ F )
=> ( ord_less_eq_real @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_real @ A @ ( B @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(102,axiom,
! [A: a,B: real,C: a,D: real] :
( ( ( product_Pair_a_real @ A @ B )
= ( product_Pair_a_real @ C @ D ) )
=> ~ ( ( A = C )
=> ( B != D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_282_Pair__inject) ).
thf(489,plain,
! [A: a,B: real,C: a,D: real] :
( ( ( product_Pair_a_real @ A @ B )
= ( product_Pair_a_real @ C @ D ) )
=> ~ ( ( A = C )
=> ( B != D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).
thf(125,axiom,
! [A: real,B: real,C: $o] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_real @ B @ A )
=> C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_223_less__imp__triv) ).
thf(569,plain,
! [A: real,B: real,C: $o] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_real @ B @ A )
=> C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[125]) ).
thf(105,axiom,
! [A: set_a] : ( ord_less_eq_set_a @ A @ top_top_set_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_198_top__greatest) ).
thf(503,plain,
! [A: set_a] : ( ord_less_eq_set_a @ A @ top_top_set_a ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(38,axiom,
! [A: real,B: real] :
( ~ ( ord_less_real @ A @ B )
=> ( ( ord_less_eq_real @ A @ B )
= ( A = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_158_antisym__conv1) ).
thf(266,plain,
! [A: real,B: real] :
( ~ ( ord_less_real @ A @ B )
=> ( ( ord_less_eq_real @ A @ B )
= ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(121,axiom,
! [A: product_prod_a_real,B: product_prod_a_real] :
~ ( ord_less_real @ ( real_V404783528a_real @ A @ B ) @ zero_zero_real ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_202_dist__not__less__zero) ).
thf(558,plain,
! [A: product_prod_a_real,B: product_prod_a_real] :
~ ( ord_less_real @ ( real_V404783528a_real @ A @ B ) @ zero_zero_real ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[121]) ).
thf(114,axiom,
( real_V404783528a_real
= ( ^ [A: product_prod_a_real,B: product_prod_a_real] : ( real_V404783528a_real @ B @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_294_dist__commute) ).
thf(530,plain,
( real_V404783528a_real
= ( ^ [A: product_prod_a_real,B: product_prod_a_real] : ( real_V404783528a_real @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(84,axiom,
! [A: product_prod_a_real > $o,B: product_prod_a_real] :
( ! [C: a,D: real] : ( A @ ( product_Pair_a_real @ C @ D ) )
=> ( A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_284_prod__cases) ).
thf(412,plain,
! [A: product_prod_a_real > $o,B: product_prod_a_real] :
( ! [C: a,D: real] : ( A @ ( product_Pair_a_real @ C @ D ) )
=> ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(109,axiom,
! [A: set_a] :
( ( A != top_top_set_a )
= ( ord_less_set_a @ A @ top_top_set_a ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_28_top_Onot__eq__extremum) ).
thf(513,plain,
! [A: set_a] :
( ( A != top_top_set_a )
= ( ord_less_set_a @ A @ top_top_set_a ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
thf(43,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( ord_less_eq_real @ A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_154_less__imp__le) ).
thf(279,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( ord_less_eq_real @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(14,axiom,
! [A: product_prod_a_real] : ( member1103263856a_real @ A @ top_to2138011583a_real ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_iso__tuple__UNIV__I) ).
thf(180,plain,
! [A: product_prod_a_real] : ( member1103263856a_real @ A @ top_to2138011583a_real ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(94,axiom,
! [A: real,B: real > real,C: real,D: real] :
( ( ord_less_real @ A @ ( B @ C ) )
=> ( ( ord_less_real @ C @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_real @ E @ F )
=> ( ord_less_real @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_real @ A @ ( B @ D ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_266_order__less__subst1) ).
thf(444,plain,
! [A: real,B: real > real,C: real,D: real] :
( ( ord_less_real @ A @ ( B @ C ) )
=> ( ( ord_less_real @ C @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_real @ E @ F )
=> ( ord_less_real @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_real @ A @ ( B @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(6,axiom,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
| ( ord_less_eq_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_74_linear) ).
thf(149,plain,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
| ( ord_less_eq_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(87,axiom,
! [A: real,B: real,C: real] :
( ( A = B )
=> ( ( ord_less_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_238_ord__eq__less__trans) ).
thf(423,plain,
! [A: real,B: real,C: real] :
( ( A = B )
=> ( ( ord_less_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(45,axiom,
! [A: product_prod_a_real,B: product_prod_a_real] :
( ( ord_less_eq_real @ ( real_V404783528a_real @ A @ B ) @ zero_zero_real )
= ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_47_dist__le__zero__iff) ).
thf(286,plain,
! [A: product_prod_a_real,B: product_prod_a_real] :
( ( ord_less_eq_real @ ( real_V404783528a_real @ A @ B ) @ zero_zero_real )
= ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(128,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_246_less__asym_H) ).
thf(579,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[128]) ).
thf(47,axiom,
! [A: real,B: real] :
( ! [C: real] :
( ( ord_less_real @ C @ A )
=> ( ord_less_eq_real @ C @ B ) )
=> ( ord_less_eq_real @ A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_148_dense__le) ).
thf(291,plain,
! [A: real,B: real] :
( ! [C: real] :
( ( ord_less_real @ C @ A )
=> ( ord_less_eq_real @ C @ B ) )
=> ( ord_less_eq_real @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(44,axiom,
! [A: real,B: real,C: real > real,D: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ ( C @ B ) @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_eq_real @ E @ F )
=> ( ord_less_eq_real @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_eq_real @ ( C @ A ) @ D ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_53_order__subst2) ).
thf(281,plain,
! [A: real,B: real,C: real > real,D: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ ( C @ B ) @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_eq_real @ E @ F )
=> ( ord_less_eq_real @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_eq_real @ ( C @ A ) @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(23,axiom,
( ord_less_real
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
& ( A != B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_182_less__le) ).
thf(204,plain,
( ord_less_real
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
& ( A != B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(76,axiom,
! [A: set_a] :
~ ( ord_less_set_a @ top_top_set_a @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_24_top_Oextremum__strict) ).
thf(382,plain,
! [A: set_a] :
~ ( ord_less_set_a @ top_top_set_a @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(126,axiom,
! [A: a,B: real,C: a,D: real] :
( ( ( product_Pair_a_real @ A @ B )
= ( product_Pair_a_real @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_10_prod_Oinject) ).
thf(572,plain,
! [A: a,B: real,C: a,D: real] :
( ( ( product_Pair_a_real @ A @ B )
= ( product_Pair_a_real @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[126]) ).
thf(5,axiom,
! [A: real,B: real > real,C: real,D: real] :
( ( ord_less_eq_real @ A @ ( B @ C ) )
=> ( ( ord_less_eq_real @ C @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_eq_real @ E @ F )
=> ( ord_less_eq_real @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_eq_real @ A @ ( B @ D ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_49_order__subst1) ).
thf(144,plain,
! [A: real,B: real > real,C: real,D: real] :
( ( ord_less_eq_real @ A @ ( B @ C ) )
=> ( ( ord_less_eq_real @ C @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_eq_real @ E @ F )
=> ( ord_less_eq_real @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_eq_real @ A @ ( B @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(74,axiom,
( top_top_set_a
= ( collect_a @ top_top_a_o ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_113_top__set__def) ).
thf(377,plain,
( top_top_set_a
= ( collect_a @ top_top_a_o ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(55,axiom,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_real @ A @ B )
| ( A = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_144_le__imp__less__or__eq) ).
thf(318,plain,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_real @ A @ B )
| ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(51,axiom,
! [A: product_prod_a_real,B: product_prod_a_real] : ( ord_less_eq_real @ zero_zero_real @ ( real_V404783528a_real @ A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_112_zero__le__dist) ).
thf(303,plain,
! [A: product_prod_a_real,B: product_prod_a_real] : ( ord_less_eq_real @ zero_zero_real @ ( real_V404783528a_real @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(25,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_152_le__less__trans) ).
thf(208,plain,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(68,axiom,
( top_to2138011583a_real
= ( collec1714955950a_real @ top_to1567080838real_o ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_115_top__set__def) ).
thf(362,plain,
( top_to2138011583a_real
= ( collec1714955950a_real @ top_to1567080838real_o ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(124,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_230_less__not__sym) ).
thf(567,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[124]) ).
thf(78,axiom,
! [A: real,B: real,C: real > real,D: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_real @ ( C @ B ) @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_real @ E @ F )
=> ( ord_less_real @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_real @ ( C @ A ) @ D ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_262_order__less__subst2) ).
thf(387,plain,
! [A: real,B: real,C: real > real,D: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_real @ ( C @ B ) @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_real @ E @ F )
=> ( ord_less_real @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_real @ ( C @ A ) @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(116,axiom,
? [A: product_prod_a_real] :
( ( member1103263856a_real @ A @ ( lower_930854854raph_a @ top_top_set_a @ f ) )
& ( ord_less_real @ ( real_V404783528a_real @ A @ ( product_Pair_a_real @ x @ y ) ) @ e ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0__092_060open_062_092_060exists_062ya_092_060in_062Epigraph_AUNIV_Af_O_Adist_Aya_A_Ix_M_Ay_J_A_060_Ae_092_060close_062) ).
thf(535,plain,
? [A: product_prod_a_real] :
( ( member1103263856a_real @ A @ ( lower_930854854raph_a @ top_top_set_a @ f ) )
& ( ord_less_real @ ( real_V404783528a_real @ A @ ( product_Pair_a_real @ x @ y ) ) @ e ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(100,axiom,
! [A: product_prod_a_real] :
? [B: a,C: real] :
( A
= ( product_Pair_a_real @ B @ C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_286_surj__pair) ).
thf(483,plain,
! [A: product_prod_a_real] :
? [B: a,C: real] :
( A
= ( product_Pair_a_real @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(111,axiom,
! [A: a,B: real,C: a,D: real] :
( ( ( product_Pair_a_real @ A @ B )
= ( product_Pair_a_real @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_12_old_Oprod_Oinject) ).
thf(520,plain,
! [A: a,B: real,C: a,D: real] :
( ( ( product_Pair_a_real @ A @ B )
= ( product_Pair_a_real @ C @ D ) )
= ( ( A = C )
& ( B = D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).
thf(59,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_138_order_Ostrict__trans1) ).
thf(330,plain,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(63,axiom,
( ord_less_eq_real
= ( ^ [A: real,B: real] :
( ( ord_less_real @ A @ B )
| ( A = B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_184_le__less) ).
thf(345,plain,
( ord_less_eq_real
= ( ^ [A: real,B: real] :
( ( ord_less_real @ A @ B )
| ( A = B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(70,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_real @ C @ A )
=> ( ord_less_real @ C @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_130_dual__order_Ostrict__trans1) ).
thf(367,plain,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_real @ C @ A )
=> ( ord_less_real @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(30,axiom,
! [A: real] : ( ord_less_eq_real @ A @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_38_order__refl) ).
thf(240,plain,
! [A: real] : ( ord_less_eq_real @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(34,axiom,
! [A: real] : ( ord_less_eq_real @ A @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_dual__order_Orefl) ).
thf(251,plain,
! [A: real] : ( ord_less_eq_real @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(82,axiom,
! [A: real,B: real,C: real > real,D: real] :
( ( ord_less_real @ A @ B )
=> ( ( ( C @ B )
= D )
=> ( ! [E: real,F: real] :
( ( ord_less_real @ E @ F )
=> ( ord_less_real @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_real @ ( C @ A ) @ D ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_270_ord__less__eq__subst) ).
thf(399,plain,
! [A: real,B: real,C: real > real,D: real] :
( ( ord_less_real @ A @ B )
=> ( ( ( C @ B )
= D )
=> ( ! [E: real,F: real] :
( ( ord_less_real @ E @ F )
=> ( ord_less_real @ ( C @ E ) @ ( C @ F ) ) )
=> ( ord_less_real @ ( C @ A ) @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(123,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( B != A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_225_less__imp__not__eq2) ).
thf(563,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( B != A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[123]) ).
thf(27,axiom,
( ( (=) @ real )
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
& ( ord_less_eq_real @ B @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_86_order__class_Oorder_Oeq__iff) ).
thf(226,plain,
( ( (=) @ real )
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
& ( ord_less_eq_real @ B @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(89,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_234_dual__order_Oasym) ).
thf(431,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(106,axiom,
( top_to1153982881_set_a
= ( produc190993315_set_a @ top_top_set_real @ top_top_set_a ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_16_top__prod__def) ).
thf(505,plain,
( top_to1153982881_set_a
= ( produc190993315_set_a @ top_top_set_real @ top_top_set_a ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(92,axiom,
! [A: real,B: real] :
( ( ~ ( ord_less_real @ A @ B ) )
= ( ( ord_less_real @ B @ A )
| ( A = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_208_not__less__iff__gr__or__eq) ).
thf(438,plain,
! [A: real,B: real] :
( ( ~ ( ord_less_real @ A @ B ) )
= ( ( ord_less_real @ B @ A )
| ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(97,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( B = C )
=> ( ord_less_real @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_236_ord__less__eq__trans) ).
thf(473,plain,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( B = C )
=> ( ord_less_real @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(118,axiom,
! [A: real] :
~ ( ord_less_real @ A @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_240_less__irrefl) ).
thf(548,plain,
! [A: real] :
~ ( ord_less_real @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(73,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_real @ C @ A )
=> ( ord_less_real @ C @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_210_dual__order_Ostrict__trans) ).
thf(374,plain,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_real @ C @ A )
=> ( ord_less_real @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(110,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_206_order_Ostrict__implies__not__eq) ).
thf(516,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[110]) ).
thf(19,axiom,
! [A: real,B: real] :
( ~ ( ord_less_eq_real @ A @ B )
=> ( ord_less_eq_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_78_le__cases) ).
thf(194,plain,
! [A: real,B: real] :
( ~ ( ord_less_eq_real @ A @ B )
=> ( ord_less_eq_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(48,axiom,
( ord_less_real
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
& ~ ( ord_less_eq_real @ B @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_142_less__le__not__le) ).
thf(295,plain,
( ord_less_real
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
& ~ ( ord_less_eq_real @ B @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(58,axiom,
! [A: product_prod_a_real,B: product_prod_a_real] :
( ( ( real_V404783528a_real @ A @ B )
= zero_zero_real )
= ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_45_dist__eq__0__iff) ).
thf(327,plain,
! [A: product_prod_a_real,B: product_prod_a_real] :
( ( ( real_V404783528a_real @ A @ B )
= zero_zero_real )
= ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(21,axiom,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ A )
= ( B = A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_84_antisym__conv) ).
thf(199,plain,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ A )
= ( B = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(15,axiom,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ~ ( ord_less_real @ A @ B ) )
= ( A = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_156_antisym__conv2) ).
thf(182,plain,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ~ ( ord_less_real @ A @ B ) )
= ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(93,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_244_less__trans) ).
thf(441,plain,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(62,axiom,
! [A: real > real > $o,B: real,C: real] :
( ! [D: real,E: real] :
( ( ord_less_eq_real @ D @ E )
=> ( A @ D @ E ) )
=> ( ! [D: real,E: real] :
( ( A @ E @ D )
=> ( A @ D @ E ) )
=> ( A @ B @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_98_linorder__wlog) ).
thf(338,plain,
! [A: real > real > $o,B: real,C: real] :
( ! [D: real,E: real] :
( ( ord_less_eq_real @ D @ E )
=> ( A @ D @ E ) )
=> ( ! [D: real,E: real] :
( ( A @ E @ D )
=> ( A @ D @ E ) )
=> ( A @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(67,axiom,
! [A: product_prod_a_real] :
( ( real_V404783528a_real @ A @ A )
= zero_zero_real ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_46_dist__self) ).
thf(359,plain,
! [A: product_prod_a_real] :
( ( real_V404783528a_real @ A @ A )
= zero_zero_real ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(130,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_217_order_Ostrict__trans) ).
thf(585,plain,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[130]) ).
thf(71,axiom,
( ord_less_real
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
& ( B != A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_120_dual__order_Ostrict__iff__order) ).
thf(370,plain,
( ord_less_real
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
& ( B != A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(61,axiom,
? [A: product_prod_a_real] : ( member1103263856a_real @ A @ top_to2138011583a_real ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_290_UNIV__witness) ).
thf(336,plain,
? [A: product_prod_a_real] : ( member1103263856a_real @ A @ top_to2138011583a_real ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(8,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_136_order_Ostrict__trans2) ).
thf(154,plain,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ C )
=> ( ord_less_real @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(136,axiom,
( top_to345582004_set_a
= ( produc1220567734_set_a @ top_to2138011583a_real @ top_top_set_a ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_20_top__prod__def) ).
thf(600,plain,
( top_to345582004_set_a
= ( produc1220567734_set_a @ top_to2138011583a_real @ top_top_set_a ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[136]) ).
thf(134,axiom,
! [A: set_a] :
( ( ord_less_eq_set_a @ top_top_set_a @ A )
= ( A = top_top_set_a ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_194_top_Oextremum__unique) ).
thf(595,plain,
! [A: set_a] :
( ( ord_less_eq_set_a @ top_top_set_a @ A )
= ( A = top_top_set_a ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[134]) ).
thf(29,axiom,
! [A: real,B: real > real,C: real,D: real] :
( ( A
= ( B @ C ) )
=> ( ( ord_less_eq_real @ C @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_eq_real @ E @ F )
=> ( ord_less_eq_real @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_eq_real @ A @ ( B @ D ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_ord__eq__le__subst) ).
thf(231,plain,
! [A: real,B: real > real,C: real,D: real] :
( ( A
= ( B @ C ) )
=> ( ( ord_less_eq_real @ C @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_eq_real @ E @ F )
=> ( ord_less_eq_real @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_eq_real @ A @ ( B @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(117,axiom,
! [A: real,B: real > real,C: real,D: real] :
( ( A
= ( B @ C ) )
=> ( ( ord_less_real @ C @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_real @ E @ F )
=> ( ord_less_real @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_real @ A @ ( B @ D ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_274_ord__eq__less__subst) ).
thf(539,plain,
! [A: real,B: real > real,C: real,D: real] :
( ( A
= ( B @ C ) )
=> ( ( ord_less_real @ C @ D )
=> ( ! [E: real,F: real] :
( ( ord_less_real @ E @ F )
=> ( ord_less_real @ ( B @ E ) @ ( B @ F ) ) )
=> ( ord_less_real @ A @ ( B @ D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[117]) ).
thf(129,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( B != A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_204_dual__order_Ostrict__implies__not__eq) ).
thf(581,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ( B != A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(131,axiom,
! [A: real,B: real] :
( ( A != B )
= ( ( ord_less_real @ A @ B )
| ( ord_less_real @ B @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_255_neq__iff) ).
thf(588,plain,
! [A: real,B: real] :
( ( A != B )
= ( ( ord_less_real @ A @ B )
| ( ord_less_real @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(3,axiom,
! [A: set_Pr1928503567a_real] :
( ! [B: product_prod_a_real] : ( member1103263856a_real @ B @ A )
=> ( top_to2138011583a_real = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_293_UNIV__eq__I) ).
thf(139,plain,
! [A: set_Pr1928503567a_real] :
( ! [B: product_prod_a_real] : ( member1103263856a_real @ B @ A )
=> ( top_to2138011583a_real = A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(90,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
| ( A = B )
| ( ord_less_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_242_less__linear) ).
thf(433,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
| ( A = B )
| ( ord_less_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(98,axiom,
! [A: set_Pr1928503567a_real] :
( ( collec1714955950a_real
@ ^ [B: product_prod_a_real] : ( member1103263856a_real @ B @ A ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_105_Collect__mem__eq) ).
thf(478,plain,
! [A: set_Pr1928503567a_real] :
( ( collec1714955950a_real
@ ^ [B: product_prod_a_real] : ( member1103263856a_real @ B @ A ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(40,axiom,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ A )
=> ( A = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_92_order__class_Oorder_Oantisym) ).
thf(272,plain,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ A )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(7,axiom,
! [A: real,B: real] :
( ( A != B )
=> ( ( ord_less_eq_real @ A @ B )
=> ( ord_less_real @ A @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_116_order_Onot__eq__order__implies__strict) ).
thf(151,plain,
! [A: real,B: real] :
( ( A != B )
=> ( ( ord_less_eq_real @ A @ B )
=> ( ord_less_real @ A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(18,axiom,
! [A: real,B: real] :
( ( A = B )
=> ( ord_less_eq_real @ A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_76_eq__refl) ).
thf(190,plain,
! [A: real,B: real] :
( ( A = B )
=> ( ord_less_eq_real @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(52,axiom,
! [A: product_prod_a_real] : ( member1103263856a_real @ A @ top_to2138011583a_real ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_UNIV__I) ).
thf(305,plain,
! [A: product_prod_a_real] : ( member1103263856a_real @ A @ top_to2138011583a_real ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(31,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( B = C )
=> ( ord_less_eq_real @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_90_ord__le__eq__trans) ).
thf(242,plain,
! [A: real,B: real,C: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( B = C )
=> ( ord_less_eq_real @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(115,axiom,
! [A: product_prod_a_real,B: product_prod_a_real > $o] :
( ( member1103263856a_real @ A @ ( collec1714955950a_real @ B ) )
= ( B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_102_mem__Collect__eq) ).
thf(532,plain,
! [A: product_prod_a_real,B: product_prod_a_real > $o] :
( ( member1103263856a_real @ A @ ( collec1714955950a_real @ B ) )
= ( B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(80,axiom,
( top_to829322572a_real
= ( produc383769494a_real @ top_top_set_a @ top_to2138011583a_real ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_top__prod__def) ).
thf(395,plain,
( top_to829322572a_real
= ( produc383769494a_real @ top_top_set_a @ top_to2138011583a_real ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(127,axiom,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ? [C: real] :
( ( ord_less_real @ A @ C )
& ( ord_less_real @ C @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_252_dense) ).
thf(575,plain,
! [A: real,B: real] :
( ( ord_less_real @ A @ B )
=> ? [C: real] :
( ( ord_less_real @ A @ C )
& ( ord_less_real @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(11,axiom,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ! [D: real] :
( ( ord_less_real @ A @ D )
=> ( ( ord_less_real @ D @ B )
=> ( ord_less_eq_real @ D @ C ) ) )
=> ( ord_less_eq_real @ B @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_126_dense__le__bounded) ).
thf(163,plain,
! [A: real,B: real,C: real] :
( ( ord_less_real @ A @ B )
=> ( ! [D: real] :
( ( ord_less_real @ A @ D )
=> ( ( ord_less_real @ D @ B )
=> ( ord_less_eq_real @ D @ C ) ) )
=> ( ord_less_eq_real @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(13,axiom,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_188_leD) ).
thf(178,plain,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ~ ( ord_less_real @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(42,axiom,
( ( (=) @ real )
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
& ( ord_less_eq_real @ B @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_70_eq__iff) ).
thf(277,plain,
( ( (=) @ real )
= ( ^ [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
& ( ord_less_eq_real @ B @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(104,axiom,
! [A: a,B: real,C: a > extended_ereal,D: real] :
( ( ( member1103263856a_real @ ( product_Pair_a_real @ A @ B ) @ ( lower_930854854raph_a @ top_top_set_a @ C ) )
& ( ord_less_eq_real @ B @ D ) )
=> ( member1103263856a_real @ ( product_Pair_a_real @ A @ D ) @ ( lower_930854854raph_a @ top_top_set_a @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_34_epigraph__mono) ).
thf(501,plain,
! [A: a,B: real,C: a > extended_ereal,D: real] :
( ( ( member1103263856a_real @ ( product_Pair_a_real @ A @ B ) @ ( lower_930854854raph_a @ top_top_set_a @ C ) )
& ( ord_less_eq_real @ B @ D ) )
=> ( member1103263856a_real @ ( product_Pair_a_real @ A @ D ) @ ( lower_930854854raph_a @ top_top_set_a @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(101,axiom,
! [A: product_prod_a_real,B: product_prod_a_real] :
( ( ord_less_real @ zero_zero_real @ ( real_V404783528a_real @ A @ B ) )
= ( A != B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_48_zero__less__dist__iff) ).
thf(486,plain,
! [A: product_prod_a_real,B: product_prod_a_real] :
( ( ord_less_real @ zero_zero_real @ ( real_V404783528a_real @ A @ B ) )
= ( A != B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(133,axiom,
! [A: set_a] :
( ( ord_less_eq_set_a @ top_top_set_a @ A )
=> ( A = top_top_set_a ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_190_top_Oextremum__uniqueI) ).
thf(592,plain,
! [A: set_a] :
( ( ord_less_eq_set_a @ top_top_set_a @ A )
=> ( A = top_top_set_a ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[133]) ).
thf(69,axiom,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ A )
=> ( A = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_72_antisym) ).
thf(364,plain,
! [A: real,B: real] :
( ( ord_less_eq_real @ A @ B )
=> ( ( ord_less_eq_real @ B @ A )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(607,plain,
$false,
inference(e,[status(thm)],[307,138,347,468,555,333,249,481,352,408,523,449,247,379,511,269,202,385,142,185,417,301,436,372,357,196,157,421,228,289,261,591,321,211,253,602,397,428,507,206,527,312,561,392,297,275,598,160,551,324,188,169,499,256,489,569,503,266,558,530,412,513,279,180,444,149,423,286,579,291,281,204,382,572,144,377,318,303,208,362,567,387,535,483,520,330,345,367,240,251,399,563,226,431,505,438,473,548,374,516,194,295,327,199,182,441,338,359,585,370,336,154,600,595,231,539,581,588,139,433,478,272,151,190,305,242,532,395,575,163,178,277,501,486,592,364]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP113^1 : 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.09/0.20 % Computer : n004.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Tue Sep 29 19:55:22 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/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.99/0.81 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.00/1.16 % [INFO] Parsing done (352ms).
% 2.00/1.17 % [INFO] Running in sequential loop mode.
% 3.23/1.57 % [INFO] eprover registered as external prover.
% 3.23/1.58 % [INFO] Scanning for conjecture ...
% 3.65/1.71 % [INFO] Found a conjecture (or negated_conjecture) and 345 axioms. Running axiom selection ...
% 3.89/1.82 % [INFO] Axiom selection finished. Selected 135 axioms (removed 210 axioms).
% 4.28/1.96 % [INFO] Problem is higher-order (TPTP THF).
% 4.28/1.98 % [INFO] Type checking passed.
% 4.28/1.99 % [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 ...
% 10.65/3.65 % External prover 'e' found a proof!
% 10.65/3.65 % [INFO] Killing All external provers ...
% 10.65/3.65 % Time passed: 3303ms (effective reasoning time: 2473ms)
% 10.65/3.65 % 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)>
% 10.65/3.66 % Axioms used in derivation (135): fact_82_le__cases3, fact_112_zero__le__dist, fact_120_dual__order_Ostrict__iff__order, fact_261_lt__ex, fact_240_less__irrefl, fact_293_UNIV__eq__I, fact_225_less__imp__not__eq2, fact_284_prod__cases, fact_297_closure__UNIV, fact_136_order_Ostrict__trans2, fact_84_antisym__conv, fact_116_order_Onot__eq__order__implies__strict, fact_236_ord__less__eq__trans, fact_194_top_Oextremum__unique, fact_18_top__prod__def, fact_140_not__le__imp__less, fact_290_UNIV__witness, fact_262_order__less__subst2, fact_144_le__imp__less__or__eq, fact_2_xy, fact_170_order__less__le__subst1, fact_105_Collect__mem__eq, fact_115_top__set__def, fact_102_mem__Collect__eq, fact_78_le__cases, fact_37_metric__eq__thm, fact_210_dual__order_Ostrict__trans, fact_38_order__refl, fact_212_linorder__less__wlog, fact_70_eq__iff, fact_15_top__prod__def, fact_295_closure__UNIV, fact_248_less__asym, fact_270_ord__less__eq__subst, fact_76_eq__refl, fact_154_less__imp__le, fact_252_dense, fact_53_order__subst2, fact_253_order_Oasym, fact_0__092_060open_062_092_060exists_062ya_092_060in_062Epigraph_AUNIV_Af_O_Adist_Aya_A_Ix_M_Ay_J_A_060_Ae_092_060close_062, fact_86_order__class_Oorder_Oeq__iff, fact_108_dual__order_Oeq__iff, fact_286_surj__pair, fact_24_top_Oextremum__strict, fact_202_dist__not__less__zero, fact_215_less__imp__not__less, fact_227_antisym__conv3, fact_92_order__class_Oorder_Oantisym, fact_94_order__trans, fact_230_less__not__sym, fact_146_le__less__linear, fact_49_order__subst1, fact_96_dual__order_Orefl, fact_148_dense__le, fact_206_order_Ostrict__implies__not__eq, fact_282_Pair__inject, fact_255_neq__iff, fact_232_less__imp__not__eq, fact_158_antisym__conv1, fact_20_top__prod__def, fact_34_epigraph__mono, fact_149_dense__ge, fact_204_dual__order_Ostrict__implies__not__eq, fact_12_old_Oprod_Oinject, fact_100_dual__order_Otrans, fact_182_less__le, fact_190_top_Oextremum__uniqueI, fact_1__092_060open_0620_A_060_Ae_092_060close_062, fact_203_dist__pos__lt, fact_122_dual__order_Oorder__iff__strict, fact_186_leI, fact_152_le__less__trans, fact_178_order__le__less__subst1, fact_132_order_Ostrict__iff__order, fact_223_less__imp__triv, fact_162_not__less, fact_257_neqE, fact_238_ord__eq__less__trans, fact_250_less__imp__neq, fact_80_order_Otrans, fact_150_less__le__trans, fact_166_order__less__le__subst2, fact_280_old_Oprod_Oexhaust, fact_118_dual__order_Ostrict__implies__order, fact_134_order_Oorder__iff__strict, fact_16_top__prod__def, fact_124_order_Ostrict__implies__order, fact_188_leD, fact_13_dist__commute__lessI, fact_208_not__less__iff__gr__or__eq, fact_266_order__less__subst1, fact_48_zero__less__dist__iff, fact_22_top__prod__def, fact_62_ord__eq__le__subst, fact_6_iso__tuple__UNIV__I, fact_88_ord__eq__le__trans, fact_110_dual__order_Oantisym, fact_278_old_Oprod_Oinducts, fact_142_less__le__not__le, fact_184_le__less, fact_294_dist__commute, fact_221_linorder__cases, fact_45_dist__eq__0__iff, fact_259_gt__ex, fact_160_le__neq__trans, fact_138_order_Ostrict__trans1, fact_128_dual__order_Ostrict__trans2, fact_342_less__eq__real__def, fact_217_order_Ostrict__trans, fact_126_dense__le__bounded, fact_234_dual__order_Oasym, fact_198_top__greatest, fact_274_ord__eq__less__subst, fact_98_linorder__wlog, fact_3_UNIV__I, fact_174_order__le__less__subst2, fact_219_dual__order_Oirrefl, fact_300_closure__approachable__le, fact_164_not__le, fact_242_less__linear, fact_72_antisym, fact_244_less__trans, fact_66_ord__le__eq__subst, fact_47_dist__le__zero__iff, fact_10_prod_Oinject, conj_0, fact_46_dist__self, fact_74_linear, fact_130_dual__order_Ostrict__trans1, fact_246_less__asym_H, fact_156_antisym__conv2, fact_127_dense__ge__bounded, fact_28_top_Onot__eq__extremum, fact_113_top__set__def, fact_90_ord__le__eq__trans
% 10.65/3.66 % No. of inferences in proof: 274
% 10.65/3.66 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 3303 ms resp. 2473 ms w/o parsing
% 11.21/3.78 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 11.21/3.79 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------