%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : ITP110^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n014.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 Oct 7 10:24:09 AM UTC 2026
% Result : Theorem 1.29s 0.46s
% Output : CNFRefutation 1.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 17
% Syntax : Number of formulae : 180 ( 90 unt; 0 typ; 0 def)
% Number of atoms : 910 ( 337 equ; 0 cnn)
% Maximal formula atoms : 3 ( 5 avg)
% Number of connectives : 1090 ( 152 ~; 159 |; 0 &; 758 @)
% ( 0 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Number of types : 17 ( 16 usr)
% Number of type conns : 106 ( 106 >; 0 *; 0 +; 0 <<)
% Number of symbols : 77 ( 74 usr; 20 con; 0-2 aty)
% Number of variables : 239 ( 0 ^; 236 !; 3 ?; 239 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_a,type,
a: $tType ).
thf(tp_extended_ereal,type,
extended_ereal: $tType ).
thf(tp_product_prod_a_real,type,
product_prod_a_real: $tType ).
thf(tp_real,type,
real: $tType ).
thf(tp_set_Extended_ereal,type,
set_Extended_ereal: $tType ).
thf(tp_set_Extended_ereal_o,type,
set_Extended_ereal_o: $tType ).
thf(tp_set_Pr1158285382l_real,type,
set_Pr1158285382l_real: $tType ).
thf(tp_set_Pr1928503567a_real,type,
set_Pr1928503567a_real: $tType ).
thf(tp_set_Pr597221087l_real,type,
set_Pr597221087l_real: $tType ).
thf(tp_set_a,type,
set_a: $tType ).
thf(tp_set_a_o,type,
set_a_o: $tType ).
thf(tp_set_real,type,
set_real: $tType ).
thf(tp_set_se1849684334_ereal,type,
set_se1849684334_ereal: $tType ).
thf(tp_set_se767749006_ereal,type,
set_se767749006_ereal: $tType ).
thf(tp_set_set_a,type,
set_set_a: $tType ).
thf(tp_set_set_set_a,type,
set_set_set_a: $tType ).
thf(tp_collec1714955950a_real,type,
collec1714955950a_real: ( product_prod_a_real > $o ) > set_Pr1928503567a_real ).
thf(tp_collec247695033_ereal,type,
collec247695033_ereal: ( extended_ereal > $o ) > set_Extended_ereal ).
thf(tp_collect_a,type,
collect_a: ( a > $o ) > set_a ).
thf(tp_comple1161760187_ereal,type,
comple1161760187_ereal: set_Extended_ereal > extended_ereal ).
thf(tp_comple1517911419_ereal,type,
comple1517911419_ereal: set_se1849684334_ereal > set_se767749006_ereal ).
thf(tp_comple1766734283_set_a,type,
comple1766734283_set_a: set_set_a > set_a ).
thf(tp_comple179807490real_o,type,
comple179807490real_o: set_Extended_ereal_o > extended_ereal > $o ).
thf(tp_comple2129349247p_real,type,
comple2129349247p_real: set_real > real ).
thf(tp_comple767846299_ereal,type,
comple767846299_ereal: set_se767749006_ereal > set_Extended_ereal ).
thf(tp_comple968993579_set_a,type,
comple968993579_set_a: set_set_set_a > set_set_a ).
thf(tp_complete_Sup_Sup_a_o,type,
complete_Sup_Sup_a_o: set_a_o > a > $o ).
thf(tp_convex291263275l_real,type,
convex291263275l_real: set_Pr1158285382l_real > $o ).
thf(tp_convex78185044a_real,type,
convex78185044a_real: set_Pr1928503567a_real > $o ).
thf(tp_convex_a,type,
convex_a: set_a > $o ).
thf(tp_divide595620860_ereal,type,
divide595620860_ereal: extended_ereal > extended_ereal > extended_ereal ).
thf(tp_divide_divide_real,type,
divide_divide_real: real > real > real ).
thf(tp_extend1289208545_ereal,type,
extend1289208545_ereal: extended_ereal ).
thf(tp_extend1716541707_ereal,type,
extend1716541707_ereal: extended_ereal > real ).
thf(tp_extended_MInfty,type,
extended_MInfty: extended_ereal ).
thf(tp_extended_PInfty,type,
extended_PInfty: extended_ereal ).
thf(tp_extended_ereal2,type,
extended_ereal2: real > extended_ereal ).
thf(tp_f,type,
f: a > extended_ereal ).
thf(tp_lower_1023700310e_on_a,type,
lower_1023700310e_on_a: set_a > ( a > extended_ereal ) > $o ).
thf(tp_lower_128423320e_on_a,type,
lower_128423320e_on_a: set_a > ( a > extended_ereal ) > $o ).
thf(tp_lower_1359521925a_real,type,
lower_1359521925a_real: ( product_prod_a_real > extended_ereal ) > set_Pr1928503567a_real ).
thf(tp_lower_1391529426main_a,type,
lower_1391529426main_a: ( a > extended_ereal ) > set_a ).
thf(tp_lower_1486931688e_on_a,type,
lower_1486931688e_on_a: set_a > ( a > extended_ereal ) > $o ).
thf(tp_lower_311861424x_on_a,type,
lower_311861424x_on_a: set_a > ( a > extended_ereal ) > $o ).
thf(tp_lower_331963542_ereal,type,
lower_331963542_ereal: set_Extended_ereal > ( extended_ereal > extended_ereal ) > set_Pr597221087l_real ).
thf(tp_lower_591730471a_real,type,
lower_591730471a_real: set_Pr1928503567a_real > ( product_prod_a_real > extended_ereal ) > $o ).
thf(tp_lower_870348689a_real,type,
lower_870348689a_real: set_Pr1928503567a_real > ( product_prod_a_real > extended_ereal ) > set_Pr1158285382l_real ).
thf(tp_lower_930854854raph_a,type,
lower_930854854raph_a: set_a > ( a > extended_ereal ) > set_Pr1928503567a_real ).
thf(tp_member1103263856a_real,type,
member1103263856a_real: product_prod_a_real > set_Pr1928503567a_real > $o ).
thf(tp_member1900190071_ereal,type,
member1900190071_ereal: extended_ereal > set_Extended_ereal > $o ).
thf(tp_member450560855_ereal,type,
member450560855_ereal: set_Extended_ereal > set_se767749006_ereal > $o ).
thf(tp_member_a,type,
member_a: a > set_a > $o ).
thf(tp_member_real,type,
member_real: real > set_real > $o ).
thf(tp_member_set_a,type,
member_set_a: set_a > set_set_a > $o ).
thf(tp_ord_le1153389358_ereal,type,
ord_le1153389358_ereal: set_se767749006_ereal > set_se767749006_ereal > $o ).
thf(tp_ord_le1586073967a_real,type,
ord_le1586073967a_real: set_Pr1928503567a_real > set_Pr1928503567a_real > $o ).
thf(tp_ord_le318720350_set_a,type,
ord_le318720350_set_a: set_set_a > set_set_a > $o ).
thf(tp_ord_le824540014_ereal,type,
ord_le824540014_ereal: extended_ereal > extended_ereal > $o ).
thf(tp_ord_le88246606_ereal,type,
ord_le88246606_ereal: set_Extended_ereal > set_Extended_ereal > $o ).
thf(tp_ord_less_eq_real,type,
ord_less_eq_real: real > real > $o ).
thf(tp_ord_less_eq_set_a,type,
ord_less_eq_set_a: set_a > set_a > $o ).
thf(tp_ord_less_eq_set_real,type,
ord_less_eq_set_real: set_real > set_real > $o ).
thf(tp_order_1158471719_ereal,type,
order_1158471719_ereal: ( extended_ereal > $o ) > extended_ereal ).
thf(tp_order_Greatest_real,type,
order_Greatest_real: ( real > $o ) > real ).
thf(tp_sK1_SX0,type,
sK1_SX0: a ).
thf(tp_sK2_SY22,type,
sK2_SY22: set_a > a ).
thf(tp_sK3_SY20,type,
sK3_SY20: ( a > extended_ereal ) > set_a ).
thf(tp_sK4_SY21,type,
sK4_SY21: ( a > extended_ereal ) > set_a ).
thf(tp_times_1966848393_ereal,type,
times_1966848393_ereal: extended_ereal > extended_ereal > extended_ereal ).
thf(tp_times_times_real,type,
times_times_real: real > real > real ).
thf(tp_top_to1486684270_set_a,type,
top_to1486684270_set_a: set_set_set_a ).
thf(tp_top_to1767659262_ereal,type,
top_to1767659262_ereal: set_Extended_ereal ).
thf(tp_top_to1791633086_ereal,type,
top_to1791633086_ereal: set_se1849684334_ereal ).
thf(tp_top_to2138011583a_real,type,
top_to2138011583a_real: set_Pr1928503567a_real ).
thf(tp_top_to398855007real_o,type,
top_to398855007real_o: extended_ereal > $o ).
thf(tp_top_to692740318_ereal,type,
top_to692740318_ereal: set_se767749006_ereal ).
thf(tp_top_to772344469real_o,type,
top_to772344469real_o: set_Extended_ereal_o ).
thf(tp_top_to802031902_ereal,type,
top_to802031902_ereal: extended_ereal ).
thf(tp_top_top_a_o,type,
top_top_a_o: a > $o ).
thf(tp_top_top_o,type,
top_top_o: $o ).
thf(tp_top_top_set_a,type,
top_top_set_a: set_a ).
thf(tp_top_top_set_a_o,type,
top_top_set_a_o: set_a_o ).
thf(tp_top_top_set_real,type,
top_top_set_real: set_real ).
thf(tp_top_top_set_set_a,type,
top_top_set_set_a: set_set_a ).
thf(tp_uminus1208298309_ereal,type,
uminus1208298309_ereal: extended_ereal > extended_ereal ).
thf(tp_uminus360668453_ereal,type,
uminus360668453_ereal: set_Extended_ereal > set_Extended_ereal ).
thf(tp_uminus_uminus_real,type,
uminus_uminus_real: real > real ).
thf(tp_uminus_uminus_set_a,type,
uminus_uminus_set_a: set_a > set_a ).
thf(tp_zero_z163181189_ereal,type,
zero_z163181189_ereal: extended_ereal ).
thf(tp_zero_zero_real,type,
zero_zero_real: real ).
thf(160,axiom,
! [F: a > extended_ereal,G: a > extended_ereal] :
( ( ( lower_930854854raph_a @ top_top_set_a @ F )
= ( lower_930854854raph_a @ top_top_set_a @ G ) )
=> ( F = G ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_194_epigraph__invertible) ).
thf(162,axiom,
! [A: set_a] : ( ord_less_eq_set_a @ A @ top_top_set_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_192_subset__UNIV) ).
thf(165,axiom,
! [A3: set_a] : ( ord_less_eq_set_a @ A3 @ top_top_set_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_189_top__greatest) ).
thf(168,axiom,
! [A3: set_a] :
( ( ord_less_eq_set_a @ top_top_set_a @ A3 )
= ( A3 = top_top_set_a ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_186_top_Oextremum__unique) ).
thf(171,axiom,
! [A3: set_a] :
( ( ord_less_eq_set_a @ top_top_set_a @ A3 )
=> ( A3 = top_top_set_a ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_183_top_Oextremum__uniqueI) ).
thf(310,axiom,
! [T: set_a,F: a > extended_ereal,S3: set_a] :
( ( lower_311861424x_on_a @ T @ F )
=> ( ( ord_less_eq_set_a @ S3 @ T )
=> ( lower_311861424x_on_a @ S3 @ F ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_44_convex__on__ereal__subset) ).
thf(325,axiom,
? [X4: a] : ( member_a @ X4 @ top_top_set_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_29_UNIV__witness) ).
thf(330,axiom,
! [A: set_a] :
( ! [X4: a] : ( member_a @ X4 @ A )
=> ( top_top_set_a = A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_24_UNIV__eq__I) ).
thf(337,axiom,
! [X: a] : ( member_a @ X @ top_top_set_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_17_iso__tuple__UNIV__I) ).
thf(342,axiom,
! [X: a] : ( member_a @ X @ top_top_set_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_12_UNIV__I) ).
thf(347,axiom,
convex_a @ top_top_set_a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_convex__UNIV) ).
thf(349,axiom,
! [F: a > extended_ereal] :
( ( lower_311861424x_on_a @ top_top_set_a @ F )
= ( ! [S: set_a] : ( lower_311861424x_on_a @ S @ F ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_convex__on__ereal__univ) ).
thf(350,axiom,
! [F: a > extended_ereal] :
( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ F ) @ F )
= ( ! [S: set_a] : ( lower_311861424x_on_a @ S @ F ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_convex__on__domain2) ).
thf(351,axiom,
! [F: a > extended_ereal] :
( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ F ) @ F )
= ( lower_311861424x_on_a @ top_top_set_a @ F ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_convex__on__domain) ).
thf(352,axiom,
! [F: a > extended_ereal] :
( ( lower_311861424x_on_a @ top_top_set_a @ F )
=> ( convex_a @ ( lower_1391529426main_a @ F ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_convex__domain) ).
thf(354,axiom,
( ( convex_a @ ( lower_1391529426main_a @ f ) )
=> ( lower_311861424x_on_a @ top_top_set_a @ f ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0__092_060open_062convex_A_Idomain_Af_J_A_092_060Longrightarrow_062_ALower__Semicontinuous__Mirabelle__mxyexokbxt_Oconvex__on_AUNIV_Af_092_060close_062) ).
thf(355,conjecture,
( ( lower_311861424x_on_a @ top_top_set_a @ f )
= ( convex_a @ ( lower_1391529426main_a @ f ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(356,negated_conjecture,
( ( ( lower_311861424x_on_a @ top_top_set_a @ f )
= ( convex_a @ ( lower_1391529426main_a @ f ) ) )
= $false ),
inference(negate_conjecture,[status(cth)],[355]) ).
thf(357,plain,
( ( ( lower_311861424x_on_a @ top_top_set_a @ f )
= ( convex_a @ ( lower_1391529426main_a @ f ) ) )
= $false ),
inference(unfold_def,[status(thm)],[356]) ).
thf(358,plain,
( ( ! [F: a > extended_ereal,G: a > extended_ereal] :
( ( ( lower_930854854raph_a @ top_top_set_a @ F )
= ( lower_930854854raph_a @ top_top_set_a @ G ) )
=> ( F = G ) ) )
= $true ),
inference(unfold_def,[status(thm)],[160]) ).
thf(359,plain,
( ( ! [A: set_a] : ( ord_less_eq_set_a @ A @ top_top_set_a ) )
= $true ),
inference(unfold_def,[status(thm)],[162]) ).
thf(360,plain,
( ( ! [A3: set_a] : ( ord_less_eq_set_a @ A3 @ top_top_set_a ) )
= $true ),
inference(unfold_def,[status(thm)],[165]) ).
thf(361,plain,
( ( ! [A3: set_a] :
( ( ord_less_eq_set_a @ top_top_set_a @ A3 )
= ( A3 = top_top_set_a ) ) )
= $true ),
inference(unfold_def,[status(thm)],[168]) ).
thf(362,plain,
( ( ! [A3: set_a] :
( ( ord_less_eq_set_a @ top_top_set_a @ A3 )
=> ( A3 = top_top_set_a ) ) )
= $true ),
inference(unfold_def,[status(thm)],[171]) ).
thf(363,plain,
( ( ! [T: set_a,F: a > extended_ereal,S3: set_a] :
( ( lower_311861424x_on_a @ T @ F )
=> ( ( ord_less_eq_set_a @ S3 @ T )
=> ( lower_311861424x_on_a @ S3 @ F ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[310]) ).
thf(364,plain,
( ( ? [X4: a] : ( member_a @ X4 @ top_top_set_a ) )
= $true ),
inference(unfold_def,[status(thm)],[325]) ).
thf(365,plain,
( ( ! [A: set_a] :
( ! [X4: a] : ( member_a @ X4 @ A )
=> ( top_top_set_a = A ) ) )
= $true ),
inference(unfold_def,[status(thm)],[330]) ).
thf(366,plain,
( ( ! [X: a] : ( member_a @ X @ top_top_set_a ) )
= $true ),
inference(unfold_def,[status(thm)],[337]) ).
thf(367,plain,
( ( ! [X: a] : ( member_a @ X @ top_top_set_a ) )
= $true ),
inference(unfold_def,[status(thm)],[342]) ).
thf(368,plain,
( ( convex_a @ top_top_set_a )
= $true ),
inference(unfold_def,[status(thm)],[347]) ).
thf(369,plain,
( ( ! [F: a > extended_ereal] :
( ( lower_311861424x_on_a @ top_top_set_a @ F )
= ( ! [S: set_a] : ( lower_311861424x_on_a @ S @ F ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[349]) ).
thf(370,plain,
( ( ! [F: a > extended_ereal] :
( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ F ) @ F )
= ( ! [S: set_a] : ( lower_311861424x_on_a @ S @ F ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[350]) ).
thf(371,plain,
( ( ! [F: a > extended_ereal] :
( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ F ) @ F )
= ( lower_311861424x_on_a @ top_top_set_a @ F ) ) )
= $true ),
inference(unfold_def,[status(thm)],[351]) ).
thf(372,plain,
( ( ! [F: a > extended_ereal] :
( ( lower_311861424x_on_a @ top_top_set_a @ F )
=> ( convex_a @ ( lower_1391529426main_a @ F ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[352]) ).
thf(373,plain,
( ( ( convex_a @ ( lower_1391529426main_a @ f ) )
=> ( lower_311861424x_on_a @ top_top_set_a @ f ) )
= $true ),
inference(unfold_def,[status(thm)],[354]) ).
thf(374,plain,
( ( ( lower_311861424x_on_a @ top_top_set_a @ f )
!= ( convex_a @ ( lower_1391529426main_a @ f ) ) )
= $true ),
inference(polarity_switch,[status(thm)],[357]) ).
thf(375,plain,
( ( ( convex_a @ ( lower_1391529426main_a @ f ) )
=> ( lower_311861424x_on_a @ top_top_set_a @ f ) )
= $true ),
inference(copy,[status(thm)],[373]) ).
thf(376,plain,
( ( ! [F: a > extended_ereal] :
( ( lower_311861424x_on_a @ top_top_set_a @ F )
=> ( convex_a @ ( lower_1391529426main_a @ F ) ) ) )
= $true ),
inference(copy,[status(thm)],[372]) ).
thf(377,plain,
( ( ! [F: a > extended_ereal] :
( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ F ) @ F )
= ( lower_311861424x_on_a @ top_top_set_a @ F ) ) )
= $true ),
inference(copy,[status(thm)],[371]) ).
thf(378,plain,
( ( ! [F: a > extended_ereal] :
( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ F ) @ F )
= ( ! [S: set_a] : ( lower_311861424x_on_a @ S @ F ) ) ) )
= $true ),
inference(copy,[status(thm)],[370]) ).
thf(379,plain,
( ( ! [F: a > extended_ereal] :
( ( lower_311861424x_on_a @ top_top_set_a @ F )
= ( ! [S: set_a] : ( lower_311861424x_on_a @ S @ F ) ) ) )
= $true ),
inference(copy,[status(thm)],[369]) ).
thf(380,plain,
( ( convex_a @ top_top_set_a )
= $true ),
inference(copy,[status(thm)],[368]) ).
thf(381,plain,
( ( ! [X: a] : ( member_a @ X @ top_top_set_a ) )
= $true ),
inference(copy,[status(thm)],[367]) ).
thf(382,plain,
( ( ! [X: a] : ( member_a @ X @ top_top_set_a ) )
= $true ),
inference(copy,[status(thm)],[366]) ).
thf(383,plain,
( ( ! [A: set_a] :
( ! [X4: a] : ( member_a @ X4 @ A )
=> ( top_top_set_a = A ) ) )
= $true ),
inference(copy,[status(thm)],[365]) ).
thf(384,plain,
( ( ? [X4: a] : ( member_a @ X4 @ top_top_set_a ) )
= $true ),
inference(copy,[status(thm)],[364]) ).
thf(385,plain,
( ( ! [T: set_a,F: a > extended_ereal,S3: set_a] :
( ( lower_311861424x_on_a @ T @ F )
=> ( ( ord_less_eq_set_a @ S3 @ T )
=> ( lower_311861424x_on_a @ S3 @ F ) ) ) )
= $true ),
inference(copy,[status(thm)],[363]) ).
thf(386,plain,
( ( ! [A3: set_a] :
( ( ord_less_eq_set_a @ top_top_set_a @ A3 )
=> ( A3 = top_top_set_a ) ) )
= $true ),
inference(copy,[status(thm)],[362]) ).
thf(387,plain,
( ( ! [A3: set_a] :
( ( ord_less_eq_set_a @ top_top_set_a @ A3 )
= ( A3 = top_top_set_a ) ) )
= $true ),
inference(copy,[status(thm)],[361]) ).
thf(388,plain,
( ( ! [A3: set_a] : ( ord_less_eq_set_a @ A3 @ top_top_set_a ) )
= $true ),
inference(copy,[status(thm)],[360]) ).
thf(389,plain,
( ( ! [A: set_a] : ( ord_less_eq_set_a @ A @ top_top_set_a ) )
= $true ),
inference(copy,[status(thm)],[359]) ).
thf(390,plain,
( ( ! [F: a > extended_ereal,G: a > extended_ereal] :
( ( ( lower_930854854raph_a @ top_top_set_a @ F )
= ( lower_930854854raph_a @ top_top_set_a @ G ) )
=> ( F = G ) ) )
= $true ),
inference(copy,[status(thm)],[358]) ).
thf(391,plain,
( ( ( lower_311861424x_on_a @ top_top_set_a @ f )
!= ( convex_a @ ( lower_1391529426main_a @ f ) ) )
= $true ),
inference(copy,[status(thm)],[374]) ).
thf(392,plain,
( ( ! [SX0: set_a] :
( ~ ! [SX1: a] : ( member_a @ SX1 @ SX0 )
| ( top_top_set_a = SX0 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[383]) ).
thf(393,plain,
( ( ! [SX0: a > extended_ereal] :
( ~ ( lower_311861424x_on_a @ top_top_set_a @ SX0 )
| ( convex_a @ ( lower_1391529426main_a @ SX0 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[376]) ).
thf(394,plain,
( ( ~ ! [SX0: a] :
~ ( member_a @ SX0 @ top_top_set_a ) )
= $true ),
inference(unfold_def,[status(thm)],[384]) ).
thf(395,plain,
( ( ! [SX0: a > extended_ereal,SX1: a > extended_ereal] :
( ( ( lower_930854854raph_a @ top_top_set_a @ SX0 )
!= ( lower_930854854raph_a @ top_top_set_a @ SX1 ) )
| ( SX0 = SX1 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[390]) ).
thf(396,plain,
( ( ~ ( convex_a @ ( lower_1391529426main_a @ f ) )
| ( lower_311861424x_on_a @ top_top_set_a @ f ) )
= $true ),
inference(unfold_def,[status(thm)],[375]) ).
thf(397,plain,
( ( ! [SX0: set_a,SX1: a > extended_ereal,SX2: set_a] :
( ~ ( lower_311861424x_on_a @ SX0 @ SX1 )
| ~ ( ord_less_eq_set_a @ SX2 @ SX0 )
| ( lower_311861424x_on_a @ SX2 @ SX1 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[385]) ).
thf(398,plain,
( ( ! [SX0: set_a] :
( ~ ( ord_less_eq_set_a @ top_top_set_a @ SX0 )
| ( SX0 = top_top_set_a ) ) )
= $true ),
inference(unfold_def,[status(thm)],[386]) ).
thf(399,plain,
! [SV1: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
= ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[377]) ).
thf(400,plain,
! [SV2: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
= ( ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[378]) ).
thf(401,plain,
! [SV3: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
= ( ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[379]) ).
thf(402,plain,
! [SV4: a] :
( ( member_a @ SV4 @ top_top_set_a )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[381]) ).
thf(403,plain,
! [SV5: a] :
( ( member_a @ SV5 @ top_top_set_a )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[382]) ).
thf(404,plain,
! [SV6: set_a] :
( ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
= ( SV6 = top_top_set_a ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[387]) ).
thf(405,plain,
! [SV7: set_a] :
( ( ord_less_eq_set_a @ SV7 @ top_top_set_a )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[388]) ).
thf(406,plain,
! [SV8: set_a] :
( ( ord_less_eq_set_a @ SV8 @ top_top_set_a )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[389]) ).
thf(407,plain,
( ( ( lower_311861424x_on_a @ top_top_set_a @ f )
= ( convex_a @ ( lower_1391529426main_a @ f ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[391]) ).
thf(408,plain,
! [SV9: set_a] :
( ( ~ ! [SY22: a] : ( member_a @ SY22 @ SV9 )
| ( top_top_set_a = SV9 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[392]) ).
thf(409,plain,
! [SV10: a > extended_ereal] :
( ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV10 )
| ( convex_a @ ( lower_1391529426main_a @ SV10 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[393]) ).
thf(410,plain,
( ( ! [SX0: a] :
~ ( member_a @ SX0 @ top_top_set_a ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[394]) ).
thf(411,plain,
! [SV11: a > extended_ereal] :
( ( ! [SY23: a > extended_ereal] :
( ( ( lower_930854854raph_a @ top_top_set_a @ SV11 )
!= ( lower_930854854raph_a @ top_top_set_a @ SY23 ) )
| ( SV11 = SY23 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[395]) ).
thf(412,plain,
( ( ( ~ ( convex_a @ ( lower_1391529426main_a @ f ) ) )
= $true )
| ( ( lower_311861424x_on_a @ top_top_set_a @ f )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[396]) ).
thf(413,plain,
! [SV12: set_a] :
( ( ! [SY24: a > extended_ereal,SY25: set_a] :
( ~ ( lower_311861424x_on_a @ SV12 @ SY24 )
| ~ ( ord_less_eq_set_a @ SY25 @ SV12 )
| ( lower_311861424x_on_a @ SY25 @ SY24 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[397]) ).
thf(414,plain,
! [SV13: set_a] :
( ( ~ ( ord_less_eq_set_a @ top_top_set_a @ SV13 )
| ( SV13 = top_top_set_a ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[398]) ).
thf(415,plain,
! [SV1: a > extended_ereal] :
( ( ~ ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
| ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) )
| ~ ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
| ~ ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[399]) ).
thf(416,plain,
! [SV1: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
= ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[399]) ).
thf(417,plain,
! [SV2: a > extended_ereal] :
( ( ~ ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
| ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) )
| ~ ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
| ~ ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[400]) ).
thf(418,plain,
! [SV2: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
= ( ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[400]) ).
thf(419,plain,
! [SV3: a > extended_ereal] :
( ( ~ ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
| ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) )
| ~ ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
| ~ ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[401]) ).
thf(420,plain,
! [SV3: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
= ( ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[401]) ).
thf(421,plain,
! [SV6: set_a] :
( ( ~ ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
| ( SV6 = top_top_set_a ) )
| ~ ( ~ ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
| ( SV6 != top_top_set_a ) ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[404]) ).
thf(422,plain,
! [SV6: set_a] :
( ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
= ( SV6 = top_top_set_a ) )
= $true ),
inference(extcnf_equal_pos,[status(thm)],[404]) ).
thf(423,plain,
( ( ~ ( ( lower_311861424x_on_a @ top_top_set_a @ f )
| ( convex_a @ ( lower_1391529426main_a @ f ) ) )
| ~ ( ~ ( lower_311861424x_on_a @ top_top_set_a @ f )
| ~ ( convex_a @ ( lower_1391529426main_a @ f ) ) ) )
= $false ),
inference(extcnf_equal_neg,[status(thm)],[407]) ).
thf(424,plain,
( ( ( lower_311861424x_on_a @ top_top_set_a @ f )
= ( convex_a @ ( lower_1391529426main_a @ f ) ) )
= $false ),
inference(extcnf_equal_neg,[status(thm)],[407]) ).
thf(425,plain,
! [SV9: set_a] :
( ( ( ~ ! [SY22: a] : ( member_a @ SY22 @ SV9 ) )
= $true )
| ( ( top_top_set_a = SV9 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[408]) ).
thf(426,plain,
! [SV10: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV10 ) )
= $true )
| ( ( convex_a @ ( lower_1391529426main_a @ SV10 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[409]) ).
thf(427,plain,
( ( ~ ( member_a @ sK1_SX0 @ top_top_set_a ) )
= $false ),
inference(extcnf_forall_neg,[status(esa)],[410]) ).
thf(428,plain,
! [SV14: a > extended_ereal,SV11: a > extended_ereal] :
( ( ( ( lower_930854854raph_a @ top_top_set_a @ SV11 )
!= ( lower_930854854raph_a @ top_top_set_a @ SV14 ) )
| ( SV11 = SV14 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[411]) ).
thf(429,plain,
( ( ( convex_a @ ( lower_1391529426main_a @ f ) )
= $false )
| ( ( lower_311861424x_on_a @ top_top_set_a @ f )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[412]) ).
thf(430,plain,
! [SV15: a > extended_ereal,SV12: set_a] :
( ( ! [SY26: set_a] :
( ~ ( lower_311861424x_on_a @ SV12 @ SV15 )
| ~ ( ord_less_eq_set_a @ SY26 @ SV12 )
| ( lower_311861424x_on_a @ SY26 @ SV15 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[413]) ).
thf(431,plain,
! [SV13: set_a] :
( ( ( ~ ( ord_less_eq_set_a @ top_top_set_a @ SV13 ) )
= $true )
| ( ( SV13 = top_top_set_a )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[414]) ).
thf(432,plain,
! [SV1: a > extended_ereal] :
( ( ( ~ ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
| ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) ) )
= $true )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
| ~ ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[415]) ).
thf(433,plain,
! [SV2: a > extended_ereal] :
( ( ( ~ ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
| ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) ) )
= $true )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
| ~ ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[417]) ).
thf(434,plain,
! [SV3: a > extended_ereal] :
( ( ( ~ ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
| ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) ) )
= $true )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
| ~ ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[419]) ).
thf(435,plain,
! [SV6: set_a] :
( ( ( ~ ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
| ( SV6 = top_top_set_a ) ) )
= $true )
| ( ( ~ ( ~ ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
| ( SV6 != top_top_set_a ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[421]) ).
thf(436,plain,
( ( ~ ( ( lower_311861424x_on_a @ top_top_set_a @ f )
| ( convex_a @ ( lower_1391529426main_a @ f ) ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[423]) ).
thf(437,plain,
( ( ~ ( ~ ( lower_311861424x_on_a @ top_top_set_a @ f )
| ~ ( convex_a @ ( lower_1391529426main_a @ f ) ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[423]) ).
thf(438,plain,
! [SV9: set_a] :
( ( ( ! [SY22: a] : ( member_a @ SY22 @ SV9 ) )
= $false )
| ( ( top_top_set_a = SV9 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[425]) ).
thf(439,plain,
! [SV10: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ top_top_set_a @ SV10 )
= $false )
| ( ( convex_a @ ( lower_1391529426main_a @ SV10 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[426]) ).
thf(440,plain,
( ( member_a @ sK1_SX0 @ top_top_set_a )
= $true ),
inference(extcnf_not_neg,[status(thm)],[427]) ).
thf(441,plain,
! [SV14: a > extended_ereal,SV11: a > extended_ereal] :
( ( ( ( lower_930854854raph_a @ top_top_set_a @ SV11 )
!= ( lower_930854854raph_a @ top_top_set_a @ SV14 ) )
= $true )
| ( ( SV11 = SV14 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[428]) ).
thf(442,plain,
! [SV16: set_a,SV15: a > extended_ereal,SV12: set_a] :
( ( ~ ( lower_311861424x_on_a @ SV12 @ SV15 )
| ~ ( ord_less_eq_set_a @ SV16 @ SV12 )
| ( lower_311861424x_on_a @ SV16 @ SV15 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[430]) ).
thf(443,plain,
! [SV13: set_a] :
( ( ( ord_less_eq_set_a @ top_top_set_a @ SV13 )
= $false )
| ( ( SV13 = top_top_set_a )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[431]) ).
thf(444,plain,
! [SV1: a > extended_ereal] :
( ( ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
| ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) )
= $false )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
| ~ ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[432]) ).
thf(445,plain,
! [SV2: a > extended_ereal] :
( ( ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
| ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) )
= $false )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
| ~ ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[433]) ).
thf(446,plain,
! [SV3: a > extended_ereal] :
( ( ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
| ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) )
= $false )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
| ~ ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[434]) ).
thf(447,plain,
! [SV6: set_a] :
( ( ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
| ( SV6 = top_top_set_a ) )
= $false )
| ( ( ~ ( ~ ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
| ( SV6 != top_top_set_a ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[435]) ).
thf(448,plain,
( ( ( lower_311861424x_on_a @ top_top_set_a @ f )
| ( convex_a @ ( lower_1391529426main_a @ f ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[436]) ).
thf(449,plain,
( ( ~ ( lower_311861424x_on_a @ top_top_set_a @ f )
| ~ ( convex_a @ ( lower_1391529426main_a @ f ) ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[437]) ).
thf(450,plain,
! [SV9: set_a] :
( ( ( member_a @ ( sK2_SY22 @ SV9 ) @ SV9 )
= $false )
| ( ( top_top_set_a = SV9 )
= $true ) ),
inference(extcnf_forall_neg,[status(esa)],[438]) ).
thf(451,plain,
! [SV14: a > extended_ereal,SV11: a > extended_ereal] :
( ( ( ( lower_930854854raph_a @ top_top_set_a @ SV11 )
= ( lower_930854854raph_a @ top_top_set_a @ SV14 ) )
= $false )
| ( ( SV11 = SV14 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[441]) ).
thf(452,plain,
! [SV16: set_a,SV15: a > extended_ereal,SV12: set_a] :
( ( ( ~ ( lower_311861424x_on_a @ SV12 @ SV15 ) )
= $true )
| ( ( ~ ( ord_less_eq_set_a @ SV16 @ SV12 )
| ( lower_311861424x_on_a @ SV16 @ SV15 ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[442]) ).
thf(453,plain,
! [SV1: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
= $false )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
| ~ ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[444]) ).
thf(454,plain,
! [SV1: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ top_top_set_a @ SV1 )
= $false )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
| ~ ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[444]) ).
thf(455,plain,
! [SV2: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
= $false )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
| ~ ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[445]) ).
thf(456,plain,
! [SV2: a > extended_ereal] :
( ( ( ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) )
= $false )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
| ~ ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[445]) ).
thf(457,plain,
! [SV3: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
= $false )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
| ~ ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[446]) ).
thf(458,plain,
! [SV3: a > extended_ereal] :
( ( ( ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) )
= $false )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
| ~ ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[446]) ).
thf(459,plain,
! [SV6: set_a] :
( ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
= $false )
| ( ( ~ ( ~ ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
| ( SV6 != top_top_set_a ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[447]) ).
thf(460,plain,
! [SV6: set_a] :
( ( ( SV6 = top_top_set_a )
= $false )
| ( ( ~ ( ~ ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
| ( SV6 != top_top_set_a ) ) )
= $true ) ),
inference(extcnf_or_neg,[status(thm)],[447]) ).
thf(461,plain,
( ( ( lower_311861424x_on_a @ top_top_set_a @ f )
= $true )
| ( ( convex_a @ ( lower_1391529426main_a @ f ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[448]) ).
thf(462,plain,
( ( ( ~ ( lower_311861424x_on_a @ top_top_set_a @ f ) )
= $true )
| ( ( ~ ( convex_a @ ( lower_1391529426main_a @ f ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[449]) ).
thf(463,plain,
! [SV14: a > extended_ereal,SV11: a > extended_ereal] :
( ( ( ! [SV17: a] :
( ( SV11 @ SV17 )
= ( SV14 @ SV17 ) ) )
= $true )
| ( ( ( lower_930854854raph_a @ top_top_set_a @ SV11 )
= ( lower_930854854raph_a @ top_top_set_a @ SV14 ) )
= $false ) ),
inference(extcnf_equal_pos,[status(thm)],[451]) ).
thf(464,plain,
! [SV14: a > extended_ereal,SV11: a > extended_ereal] :
( ( ( SV11 = SV14 )
= $true )
| ( ( ( lower_930854854raph_a @ top_top_set_a @ SV11 )
= ( lower_930854854raph_a @ top_top_set_a @ SV14 ) )
= $false ) ),
inference(extcnf_equal_pos,[status(thm)],[451]) ).
thf(465,plain,
! [SV16: set_a,SV15: a > extended_ereal,SV12: set_a] :
( ( ( lower_311861424x_on_a @ SV12 @ SV15 )
= $false )
| ( ( ~ ( ord_less_eq_set_a @ SV16 @ SV12 )
| ( lower_311861424x_on_a @ SV16 @ SV15 ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[452]) ).
thf(466,plain,
! [SV1: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
| ~ ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) )
= $false )
| ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[453]) ).
thf(467,plain,
! [SV1: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
| ~ ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) )
= $false )
| ( ( lower_311861424x_on_a @ top_top_set_a @ SV1 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[454]) ).
thf(468,plain,
! [SV2: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
| ~ ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) )
= $false )
| ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[455]) ).
thf(469,plain,
! [SV2: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ ( sK3_SY20 @ SV2 ) @ SV2 )
= $false )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
| ~ ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) ) )
= $true ) ),
inference(extcnf_forall_neg,[status(esa)],[456]) ).
thf(470,plain,
! [SV3: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
| ~ ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) )
= $false )
| ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[457]) ).
thf(471,plain,
! [SV3: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ ( sK4_SY21 @ SV3 ) @ SV3 )
= $false )
| ( ( ~ ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
| ~ ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) ) )
= $true ) ),
inference(extcnf_forall_neg,[status(esa)],[458]) ).
thf(472,plain,
! [SV6: set_a] :
( ( ( ~ ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
| ( SV6 != top_top_set_a ) )
= $false )
| ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[459]) ).
thf(473,plain,
! [SV6: set_a] :
( ( ( ~ ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
| ( SV6 != top_top_set_a ) )
= $false )
| ( ( SV6 = top_top_set_a )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[460]) ).
thf(474,plain,
( ( ( lower_311861424x_on_a @ top_top_set_a @ f )
= $false )
| ( ( ~ ( convex_a @ ( lower_1391529426main_a @ f ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[462]) ).
thf(475,plain,
! [SV14: a > extended_ereal,SV18: a,SV11: a > extended_ereal] :
( ( ( ( SV11 @ SV18 )
= ( SV14 @ SV18 ) )
= $true )
| ( ( ( lower_930854854raph_a @ top_top_set_a @ SV11 )
= ( lower_930854854raph_a @ top_top_set_a @ SV14 ) )
= $false ) ),
inference(extcnf_forall_pos,[status(thm)],[463]) ).
thf(476,plain,
! [SV15: a > extended_ereal,SV12: set_a,SV16: set_a] :
( ( ( ~ ( ord_less_eq_set_a @ SV16 @ SV12 ) )
= $true )
| ( ( lower_311861424x_on_a @ SV16 @ SV15 )
= $true )
| ( ( lower_311861424x_on_a @ SV12 @ SV15 )
= $false ) ),
inference(extcnf_or_pos,[status(thm)],[465]) ).
thf(477,plain,
! [SV1: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 ) )
= $false )
| ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[466]) ).
thf(478,plain,
! [SV1: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) )
= $false )
| ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[466]) ).
thf(479,plain,
! [SV1: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 ) )
= $false )
| ( ( lower_311861424x_on_a @ top_top_set_a @ SV1 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[467]) ).
thf(480,plain,
! [SV1: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV1 ) )
= $false )
| ( ( lower_311861424x_on_a @ top_top_set_a @ SV1 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[467]) ).
thf(481,plain,
! [SV2: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 ) )
= $false )
| ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[468]) ).
thf(482,plain,
! [SV2: a > extended_ereal] :
( ( ( ~ ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) )
= $false )
| ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[468]) ).
thf(483,plain,
! [SV2: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
| ~ ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) )
= $false )
| ( ( lower_311861424x_on_a @ ( sK3_SY20 @ SV2 ) @ SV2 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[469]) ).
thf(484,plain,
! [SV3: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV3 ) )
= $false )
| ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[470]) ).
thf(485,plain,
! [SV3: a > extended_ereal] :
( ( ( ~ ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) )
= $false )
| ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[470]) ).
thf(486,plain,
! [SV3: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
| ~ ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) )
= $false )
| ( ( lower_311861424x_on_a @ ( sK4_SY21 @ SV3 ) @ SV3 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[471]) ).
thf(487,plain,
! [SV6: set_a] :
( ( ( ~ ( ord_less_eq_set_a @ top_top_set_a @ SV6 ) )
= $false )
| ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[472]) ).
thf(488,plain,
! [SV6: set_a] :
( ( ( SV6 != top_top_set_a )
= $false )
| ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[472]) ).
thf(489,plain,
! [SV6: set_a] :
( ( ( ~ ( ord_less_eq_set_a @ top_top_set_a @ SV6 ) )
= $false )
| ( ( SV6 = top_top_set_a )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[473]) ).
thf(490,plain,
! [SV6: set_a] :
( ( ( SV6 != top_top_set_a )
= $false )
| ( ( SV6 = top_top_set_a )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[473]) ).
thf(491,plain,
( ( ( convex_a @ ( lower_1391529426main_a @ f ) )
= $false )
| ( ( lower_311861424x_on_a @ top_top_set_a @ f )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[474]) ).
thf(492,plain,
! [SV15: a > extended_ereal,SV12: set_a,SV16: set_a] :
( ( ( ord_less_eq_set_a @ SV16 @ SV12 )
= $false )
| ( ( lower_311861424x_on_a @ SV16 @ SV15 )
= $true )
| ( ( lower_311861424x_on_a @ SV12 @ SV15 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[476]) ).
thf(493,plain,
! [SV1: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
= $true )
| ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[477]) ).
thf(494,plain,
! [SV1: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ top_top_set_a @ SV1 )
= $true )
| ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[478]) ).
thf(495,plain,
! [SV1: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV1 ) @ SV1 )
= $true )
| ( ( lower_311861424x_on_a @ top_top_set_a @ SV1 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[479]) ).
thf(496,plain,
! [SV1: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ top_top_set_a @ SV1 )
= $true )
| ( ( lower_311861424x_on_a @ top_top_set_a @ SV1 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[480]) ).
thf(497,plain,
! [SV2: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
= $true )
| ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[481]) ).
thf(498,plain,
! [SV2: a > extended_ereal] :
( ( ( ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) )
= $true )
| ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[482]) ).
thf(499,plain,
! [SV2: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 ) )
= $false )
| ( ( lower_311861424x_on_a @ ( sK3_SY20 @ SV2 ) @ SV2 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[483]) ).
thf(500,plain,
! [SV2: a > extended_ereal] :
( ( ( ~ ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) )
= $false )
| ( ( lower_311861424x_on_a @ ( sK3_SY20 @ SV2 ) @ SV2 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[483]) ).
thf(501,plain,
! [SV3: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
= $true )
| ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[484]) ).
thf(502,plain,
! [SV3: a > extended_ereal] :
( ( ( ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) )
= $true )
| ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[485]) ).
thf(503,plain,
! [SV3: a > extended_ereal] :
( ( ( ~ ( lower_311861424x_on_a @ top_top_set_a @ SV3 ) )
= $false )
| ( ( lower_311861424x_on_a @ ( sK4_SY21 @ SV3 ) @ SV3 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[486]) ).
thf(504,plain,
! [SV3: a > extended_ereal] :
( ( ( ~ ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) )
= $false )
| ( ( lower_311861424x_on_a @ ( sK4_SY21 @ SV3 ) @ SV3 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[486]) ).
thf(505,plain,
! [SV6: set_a] :
( ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
= $true )
| ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[487]) ).
thf(506,plain,
! [SV6: set_a] :
( ( ( SV6 = top_top_set_a )
= $true )
| ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[488]) ).
thf(507,plain,
! [SV6: set_a] :
( ( ( ord_less_eq_set_a @ top_top_set_a @ SV6 )
= $true )
| ( ( SV6 = top_top_set_a )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[489]) ).
thf(508,plain,
! [SV6: set_a] :
( ( ( SV6 = top_top_set_a )
= $true )
| ( ( SV6 = top_top_set_a )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[490]) ).
thf(509,plain,
! [SV2: a > extended_ereal,SV19: set_a] :
( ( ( lower_311861424x_on_a @ SV19 @ SV2 )
= $true )
| ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
= $false ) ),
inference(extcnf_forall_pos,[status(thm)],[498]) ).
thf(510,plain,
! [SV2: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ ( lower_1391529426main_a @ SV2 ) @ SV2 )
= $true )
| ( ( lower_311861424x_on_a @ ( sK3_SY20 @ SV2 ) @ SV2 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[499]) ).
thf(511,plain,
! [SV2: a > extended_ereal] :
( ( ( ! [SY20: set_a] : ( lower_311861424x_on_a @ SY20 @ SV2 ) )
= $true )
| ( ( lower_311861424x_on_a @ ( sK3_SY20 @ SV2 ) @ SV2 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[500]) ).
thf(512,plain,
! [SV3: a > extended_ereal,SV20: set_a] :
( ( ( lower_311861424x_on_a @ SV20 @ SV3 )
= $true )
| ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
= $false ) ),
inference(extcnf_forall_pos,[status(thm)],[502]) ).
thf(513,plain,
! [SV3: a > extended_ereal] :
( ( ( lower_311861424x_on_a @ top_top_set_a @ SV3 )
= $true )
| ( ( lower_311861424x_on_a @ ( sK4_SY21 @ SV3 ) @ SV3 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[503]) ).
thf(514,plain,
! [SV3: a > extended_ereal] :
( ( ( ! [SY21: set_a] : ( lower_311861424x_on_a @ SY21 @ SV3 ) )
= $true )
| ( ( lower_311861424x_on_a @ ( sK4_SY21 @ SV3 ) @ SV3 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[504]) ).
thf(515,plain,
! [SV2: a > extended_ereal,SV21: set_a] :
( ( ( lower_311861424x_on_a @ SV21 @ SV2 )
= $true )
| ( ( lower_311861424x_on_a @ ( sK3_SY20 @ SV2 ) @ SV2 )
= $false ) ),
inference(extcnf_forall_pos,[status(thm)],[511]) ).
thf(516,plain,
! [SV3: a > extended_ereal,SV22: set_a] :
( ( ( lower_311861424x_on_a @ SV22 @ SV3 )
= $true )
| ( ( lower_311861424x_on_a @ ( sK4_SY21 @ SV3 ) @ SV3 )
= $false ) ),
inference(extcnf_forall_pos,[status(thm)],[514]) ).
thf(517,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[380,516,515,513,512,510,509,508,507,506,505,501,497,496,495,494,493,492,491,475,464,461,450,443,440,439,429,424,422,420,418,416,406,405,403,402]) ).
thf(518,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[517]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP110^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.19 % Computer : n014.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Oct 6 11:17:26 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.29/0.46 ..
% 1.29/0.46
% 1.29/0.46 No.of.Axioms: 16
% 1.29/0.46
% 1.29/0.46 Length.of.Defs: 0
% 1.29/0.46
% 1.29/0.46 Contains.Choice.Funs: true
% 1.29/0.46 ......
% 1.29/0.46
% 1.29/0.46 ********************************
% 1.29/0.46 * All subproblems solved! *
% 1.29/0.46 ********************************
% 1.29/0.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:16,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:517,loop_count:0,foatp_calls:1,translation:fof_full)
% 1.29/0.46
% 1.29/0.46 %**** Beginning of derivation protocol ****
% 1.29/0.46 % SZS output start CNFRefutation
% See solution above
% 1.29/0.46
% 1.29/0.46 %**** End of derivation protocol ****
% 1.29/0.46 %**** no. of clauses in derivation: 180 ****
% 1.29/0.46 %**** clause counter: 517 ****
% 1.29/0.46
% 1.29/0.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:16,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:25,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:517,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------