%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP021^7 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n005.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:26 AM UTC 2026
% Result : Theorem 20.41s 7.21s
% Output : Refutation 20.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 52
% Syntax : Number of formulae : 106 ( 84 unt; 0 typ; 0 def)
% Number of atoms : 255 ( 131 equ; 0 cnn)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 767 ( 10 ~; 14 |; 33 &; 640 @)
% ( 0 <=>; 70 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Number of types : 24 ( 23 usr)
% Number of type conns : 70 ( 70 >; 0 *; 0 +; 0 <<)
% Number of symbols : 10 ( 8 usr; 1 con; 0-5 aty)
% Number of variables : 367 ( 4 ^; 351 !; 12 ?; 367 :)
% Comments :
%------------------------------------------------------------------------------
thf(tyop_2Emin_2Ebool_type,type,
tyop_2Emin_2Ebool: $tType ).
thf(tyop_2Emin_2Eind_type,type,
tyop_2Emin_2Eind: $tType ).
thf(tyop_2Enum_2Enum_type,type,
tyop_2Enum_2Enum: $tType ).
thf(tyop_2Eone_2Eone_type,type,
tyop_2Eone_2Eone: $tType ).
thf(tyop_2Estring_2Echar_type,type,
tyop_2Estring_2Echar: $tType ).
thf(tyop_2EternaryComparisons_2Eordering_type,type,
tyop_2EternaryComparisons_2Eordering: $tType ).
thf(tyop_2Ehrat_2Ehrat_type,type,
tyop_2Ehrat_2Ehrat: $tType ).
thf(tyop_2Einteger_2Eint_type,type,
tyop_2Einteger_2Eint: $tType ).
thf(tyop_2Equote_2Eindex_type,type,
tyop_2Equote_2Eindex: $tType ).
thf(tyop_2Etoto_2Enum__dt_type,type,
tyop_2Etoto_2Enum__dt: $tType ).
thf(tyop_2Ehreal_2Ehreal_type,type,
tyop_2Ehreal_2Ehreal: $tType ).
thf(tyop_2EDeepSyntax_2Edeep__form_type,type,
tyop_2EDeepSyntax_2Edeep__form: $tType ).
thf(tyop_2Erealax_2Ereal_type,type,
tyop_2Erealax_2Ereal: $tType ).
thf(tyop_2Efrac_2Efrac_type,type,
tyop_2Efrac_2Efrac: $tType ).
thf(tyop_2Erat_2Erat_type,type,
tyop_2Erat_2Erat: $tType ).
thf(tyop_2Ebinary__ieee_2Eflags_type,type,
tyop_2Ebinary__ieee_2Eflags: $tType ).
thf(tyop_2Ebinary__ieee_2Efloat__compare_type,type,
tyop_2Ebinary__ieee_2Efloat__compare: $tType ).
thf(tyop_2Ebinary__ieee_2Efloat__value_type,type,
tyop_2Ebinary__ieee_2Efloat__value: $tType ).
thf(tyop_2Ebinary__ieee_2Erounding_type,type,
tyop_2Ebinary__ieee_2Erounding: $tType ).
thf(tyop_2Eieee_2Eccode_type,type,
tyop_2Eieee_2Eccode: $tType ).
thf(tyop_2Eieee_2Efloat_type,type,
tyop_2Eieee_2Efloat: $tType ).
thf(tyop_2Eieee_2Eroundmode_type,type,
tyop_2Eieee_2Eroundmode: $tType ).
thf(tyop_2Eextreal_2Eextreal_type,type,
tyop_2Eextreal_2Eextreal: $tType ).
thf(c_2Ebool_2ECOND_decl,type,
c_2Ebool_2ECOND:
!>[TA: $tType] : ( $o > TA > TA > TA ) ).
thf(c_2Epred__set_2EIMAGE_decl,type,
c_2Epred__set_2EIMAGE:
!>[TA: $tType,TB: $tType] : ( ( TB > TA ) > ( TB > $o ) > TA > $o ) ).
thf(c_2Eextreal_2Eextreal__ainv_decl,type,
c_2Eextreal_2Eextreal__ainv: tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal ).
thf(c_2Eextreal_2Eextreal__inf_decl,type,
c_2Eextreal_2Eextreal__inf: ( tyop_2Eextreal_2Eextreal > $o ) > tyop_2Eextreal_2Eextreal ).
thf(c_2Eextreal_2Eextreal__le_decl,type,
c_2Eextreal_2Eextreal__le: tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > $o ).
thf(c_2Eextreal_2Eextreal__max_decl,type,
c_2Eextreal_2Eextreal__max: tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal ).
thf(c_2Eextreal_2Eextreal__min_decl,type,
c_2Eextreal_2Eextreal__min: tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal > tyop_2Eextreal_2Eextreal ).
thf(c_2Eextreal_2Eextreal__sup_decl,type,
c_2Eextreal_2Eextreal__sup: ( tyop_2Eextreal_2Eextreal > $o ) > tyop_2Eextreal_2Eextreal ).
thf(7,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__ainv @ A )
= ( c_2Eextreal_2Eextreal__ainv @ B ) )
= ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Eeq__neg) ).
thf(69,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__ainv @ A )
= ( c_2Eextreal_2Eextreal__ainv @ B ) )
= ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(31,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__sup @ A )
= B )
= ( ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( c_2Eextreal_2Eextreal__le @ C @ B ) )
& ! [C: tyop_2Eextreal_2Eextreal] :
( ! [D: tyop_2Eextreal_2Eextreal] :
( ( A @ D )
=> ( c_2Eextreal_2Eextreal__le @ D @ C ) )
=> ( c_2Eextreal_2Eextreal__le @ B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Esup__eq) ).
thf(174,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__sup @ A )
= B )
= ( ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( c_2Eextreal_2Eextreal__le @ C @ B ) )
& ! [C: tyop_2Eextreal_2Eextreal] :
( ! [D: tyop_2Eextreal_2Eextreal] :
( ( A @ D )
=> ( c_2Eextreal_2Eextreal__le @ D @ C ) )
=> ( c_2Eextreal_2Eextreal__le @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(29,axiom,
! [A: tyop_2Eextreal_2Eextreal] : ( c_2Eextreal_2Eextreal__le @ A @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__refl) ).
thf(169,plain,
! [A: tyop_2Eextreal_2Eextreal] : ( c_2Eextreal_2Eextreal__le @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(1,conjecture,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ B @ C ) @ A )
= ( ( c_2Eextreal_2Eextreal__le @ B @ A )
& ( c_2Eextreal_2Eextreal__le @ C @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Emax__le) ).
thf(2,negated_conjecture,
~ ! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ B @ C ) @ A )
= ( ( c_2Eextreal_2Eextreal__le @ B @ A )
& ( c_2Eextreal_2Eextreal__le @ C @ A ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(54,plain,
~ ! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__max @ B @ C ) @ A )
= ( ( c_2Eextreal_2Eextreal__le @ B @ A )
& ( c_2Eextreal_2Eextreal__le @ C @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(6,axiom,
! [TA: $tType,TB: $tType,A: TB > $o,B: TB > $o,C: TB > TA] :
( ! [D: TB,E: TB] :
( ( ( C @ D )
= ( C @ E ) )
= ( D = E ) )
=> ( ( ( c_2Epred__set_2EIMAGE @ TB @ TA @ C @ B )
= ( c_2Epred__set_2EIMAGE @ TB @ TA @ C @ A ) )
= ( B = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Epred__set_2EIMAGE__11) ).
thf(66,plain,
! [TA: $tType,TB: $tType,A: TB > $o,B: TB > $o,C: TB > TA] :
( ! [D: TB,E: TB] :
( ( ( C @ D )
= ( C @ E ) )
= ( D = E ) )
=> ( ( ( c_2Epred__set_2EIMAGE @ TB @ TA @ C @ B )
= ( c_2Epred__set_2EIMAGE @ TB @ TA @ C @ A ) )
= ( B = A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(45,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ A @ B )
& ( c_2Eextreal_2Eextreal__le @ B @ C ) )
=> ( c_2Eextreal_2Eextreal__le @ A @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__trans) ).
thf(218,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ A @ B )
& ( c_2Eextreal_2Eextreal__le @ B @ C ) )
=> ( c_2Eextreal_2Eextreal__le @ A @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(25,axiom,
! [TA: $tType,A: TA,B: TA,C: $o] :
( C
| ( A
= ( c_2Ebool_2ECOND @ TA @ C @ B @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EHolSmt_2Ed017) ).
thf(151,plain,
! [TA: $tType,A: TA,B: TA,C: $o] :
( C
| ( A
= ( c_2Ebool_2ECOND @ TA @ C @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(15,axiom,
! [TA: $tType,A: TA,B: TA,C: $o] :
( ~ C
| ( B
= ( c_2Ebool_2ECOND @ TA @ C @ B @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EHolSmt_2Ed018) ).
thf(115,plain,
! [TA: $tType,A: TA,B: TA,C: $o] :
( ~ C
| ( B
= ( c_2Ebool_2ECOND @ TA @ C @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(39,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__sup @ A ) @ B )
= ( ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( c_2Eextreal_2Eextreal__le @ C @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Esup__le) ).
thf(202,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__sup @ A ) @ B )
= ( ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( c_2Eextreal_2Eextreal__le @ C @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(34,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( A @ B )
=> ( c_2Eextreal_2Eextreal__le @ B @ ( c_2Eextreal_2Eextreal__sup @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__sup__imp) ).
thf(189,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( A @ B )
=> ( c_2Eextreal_2Eextreal__le @ B @ ( c_2Eextreal_2Eextreal__sup @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(49,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( ( A @ B )
& ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( c_2Eextreal_2Eextreal__le @ B @ C ) ) )
=> ( ( c_2Eextreal_2Eextreal__inf @ A )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Einf__min) ).
thf(228,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( ( A @ B )
& ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( c_2Eextreal_2Eextreal__le @ B @ C ) ) )
=> ( ( c_2Eextreal_2Eextreal__inf @ A )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(3,axiom,
! [TA: $tType,TB: $tType,A: TB > TA] :
( ( ! [B: TB > $o,C: TB > $o] :
( ( ( c_2Epred__set_2EIMAGE @ TB @ TA @ A @ B )
= ( c_2Epred__set_2EIMAGE @ TB @ TA @ A @ C ) )
=> ( B = C ) ) )
= ( ! [B: TB,C: TB] :
( ( ( A @ B )
= ( A @ C ) )
=> ( B = C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ecardinal_2EINJECTIVE__IMAGE) ).
thf(57,plain,
! [TA: $tType,TB: $tType,A: TB > TA] :
( ( ! [B: TB > $o,C: TB > $o] :
( ( ( c_2Epred__set_2EIMAGE @ TB @ TA @ A @ B )
= ( c_2Epred__set_2EIMAGE @ TB @ TA @ A @ C ) )
=> ( B = C ) ) )
= ( ! [B: TB,C: TB] :
( ( ( A @ B )
= ( A @ C ) )
=> ( B = C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(44,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal,D: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ A @ C )
& ( c_2Eextreal_2Eextreal__le @ B @ D ) )
=> ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__min @ A @ B ) @ ( c_2Eextreal_2Eextreal__min @ C @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Emin__le2__imp) ).
thf(216,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal,D: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ A @ C )
& ( c_2Eextreal_2Eextreal__le @ B @ D ) )
=> ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__min @ A @ B ) @ ( c_2Eextreal_2Eextreal__min @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(17,axiom,
! [TA: $tType,TB: $tType,A: $o,B: TB > TA,C: TB > TA,D: TB] :
( ( c_2Ebool_2ECOND @ ( TB > TA ) @ A @ B @ C @ D )
= ( c_2Ebool_2ECOND @ TA @ A @ ( B @ D ) @ ( C @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ECOND__RATOR) ).
thf(121,plain,
! [TA: $tType,TB: $tType,A: $o,B: TB > TA,C: TB > TA,D: TB] :
( ( c_2Ebool_2ECOND @ ( TB > TA ) @ A @ B @ C @ D )
= ( c_2Ebool_2ECOND @ TA @ A @ ( B @ D ) @ ( C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(10,axiom,
! [TA: $tType,A: $o,B: TA] :
( ( c_2Ebool_2ECOND @ TA @ A @ B @ B )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2Ebool__case__ID) ).
thf(89,plain,
! [TA: $tType,A: $o,B: TA] :
( ( c_2Ebool_2ECOND @ TA @ A @ B @ B )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(21,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__min @ A @ B )
= ( c_2Eextreal_2Eextreal__min @ B @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Emin__comm) ).
thf(133,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__min @ A @ B )
= ( c_2Eextreal_2Eextreal__min @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(4,axiom,
! [TA: $tType,A: TA > $o] :
( ( c_2Epred__set_2EIMAGE @ TA @ TA
@ ^ [B: TA] : B
@ A )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Epred__set_2EIMAGE__ID) ).
thf(60,plain,
! [TA: $tType,A: TA > $o] :
( ( c_2Epred__set_2EIMAGE @ TA @ TA
@ ^ [B: TA] : B
@ A )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(46,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__inf @ A ) @ B )
= ( ! [C: tyop_2Eextreal_2Eextreal] :
( ! [D: tyop_2Eextreal_2Eextreal] :
( ( A @ D )
=> ( c_2Eextreal_2Eextreal__le @ C @ D ) )
=> ( c_2Eextreal_2Eextreal__le @ C @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Einf__le) ).
thf(220,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__inf @ A ) @ B )
= ( ! [C: tyop_2Eextreal_2Eextreal] :
( ! [D: tyop_2Eextreal_2Eextreal] :
( ( A @ D )
=> ( c_2Eextreal_2Eextreal__le @ C @ D ) )
=> ( c_2Eextreal_2Eextreal__le @ C @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(11,axiom,
! [TA: $tType,A: $o,B: TA] :
( ( c_2Ebool_2ECOND @ TA @ A @ B @ B )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EConseqConv_2ECOND__CLAUSES__ID) ).
thf(92,plain,
! [TA: $tType,A: $o,B: TA] :
( ( c_2Ebool_2ECOND @ TA @ A @ B @ B )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(37,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__ainv @ A ) @ ( c_2Eextreal_2Eextreal__ainv @ B ) )
= ( c_2Eextreal_2Eextreal__le @ B @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__neg) ).
thf(197,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__ainv @ A ) @ ( c_2Eextreal_2Eextreal__ainv @ B ) )
= ( c_2Eextreal_2Eextreal__le @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(18,axiom,
! [A: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__ainv @ ( c_2Eextreal_2Eextreal__ainv @ A ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Eneg__neg) ).
thf(124,plain,
! [A: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__ainv @ ( c_2Eextreal_2Eextreal__ainv @ A ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(43,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal > $o] :
( ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ? [D: tyop_2Eextreal_2Eextreal] :
( ( B @ D )
& ( c_2Eextreal_2Eextreal__le @ C @ D ) ) )
=> ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__sup @ A ) @ ( c_2Eextreal_2Eextreal__sup @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Esup__le__sup__imp) ).
thf(212,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal > $o] :
( ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ? [D: tyop_2Eextreal_2Eextreal] :
( ( B @ D )
& ( c_2Eextreal_2Eextreal__le @ C @ D ) ) )
=> ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__sup @ A ) @ ( c_2Eextreal_2Eextreal__sup @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(50,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] : ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__min @ A @ B ) @ B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Emin__le2) ).
thf(237,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] : ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__min @ A @ B ) @ B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(40,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] : ( c_2Eextreal_2Eextreal__le @ B @ ( c_2Eextreal_2Eextreal__max @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__max2) ).
thf(205,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] : ( c_2Eextreal_2Eextreal__le @ B @ ( c_2Eextreal_2Eextreal__max @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(28,axiom,
! [TA: $tType,A: $o,B: TA] :
( ( c_2Ebool_2ECOND @ TA @ A @ B @ B )
= B ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ECOND__ID) ).
thf(166,plain,
! [TA: $tType,A: $o,B: TA] :
( ( c_2Ebool_2ECOND @ TA @ A @ B @ B )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(24,axiom,
! [TA: $tType,TB: $tType,A: TB > TA,B: $o,C: TB,D: TB] :
( ( A @ ( c_2Ebool_2ECOND @ TB @ B @ C @ D ) )
= ( c_2Ebool_2ECOND @ TA @ B @ ( A @ C ) @ ( A @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ECOND__RAND) ).
thf(148,plain,
! [TA: $tType,TB: $tType,A: TB > TA,B: $o,C: TB,D: TB] :
( ( A @ ( c_2Ebool_2ECOND @ TB @ B @ C @ D ) )
= ( c_2Ebool_2ECOND @ TA @ B @ ( A @ C ) @ ( A @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(35,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__max @ A @ B )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ A @ B ) @ B @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Eextreal__max__def) ).
thf(191,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__max @ A @ B )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ A @ B ) @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(16,axiom,
! [TA: $tType,A: TA,B: TA,C: $o] :
( C
| ( ( c_2Ebool_2ECOND @ TA @ C @ B @ A )
= A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EHolSmt_2Ed019) ).
thf(118,plain,
! [TA: $tType,A: TA,B: TA,C: $o] :
( C
| ( ( c_2Ebool_2ECOND @ TA @ C @ B @ A )
= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(53,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ A @ B )
| ( c_2Eextreal_2Eextreal__le @ B @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__total) ).
thf(245,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ A @ B )
| ( c_2Eextreal_2Eextreal__le @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(13,axiom,
! [TA: $tType,A: $o,B: $o,C: TA,D: TA,E: TA,F: TA] :
( ( ( A = B )
& ( B
=> ( C = D ) )
& ( ~ B
=> ( E = F ) ) )
=> ( ( c_2Ebool_2ECOND @ TA @ A @ C @ E )
= ( c_2Ebool_2ECOND @ TA @ B @ D @ F ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ECOND__CONG) ).
thf(98,plain,
! [TA: $tType,A: $o,B: $o,C: TA,D: TA,E: TA,F: TA] :
( ( ( A = B )
& ( B
=> ( C = D ) )
& ( ~ B
=> ( E = F ) ) )
=> ( ( c_2Ebool_2ECOND @ TA @ A @ C @ E )
= ( c_2Ebool_2ECOND @ TA @ B @ D @ F ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(20,axiom,
! [TA: $tType,A: TA,B: TA,C: $o] :
( ~ C
| ( ( c_2Ebool_2ECOND @ TA @ C @ B @ A )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EHolSmt_2Ed020) ).
thf(130,plain,
! [TA: $tType,A: TA,B: TA,C: $o] :
( ~ C
| ( ( c_2Ebool_2ECOND @ TA @ C @ B @ A )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(47,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ A @ ( c_2Eextreal_2Eextreal__min @ B @ C ) )
= ( ( c_2Eextreal_2Eextreal__le @ A @ B )
& ( c_2Eextreal_2Eextreal__le @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__min) ).
thf(223,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ A @ ( c_2Eextreal_2Eextreal__min @ B @ C ) )
= ( ( c_2Eextreal_2Eextreal__le @ A @ B )
& ( c_2Eextreal_2Eextreal__le @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(48,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] : ( c_2Eextreal_2Eextreal__le @ A @ ( c_2Eextreal_2Eextreal__max @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__max1) ).
thf(226,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] : ( c_2Eextreal_2Eextreal__le @ A @ ( c_2Eextreal_2Eextreal__max @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(14,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__min @ A @ B )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ A @ B ) @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Eextreal__min__def) ).
thf(112,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__min @ A @ B )
= ( c_2Ebool_2ECOND @ tyop_2Eextreal_2Eextreal @ ( c_2Eextreal_2Eextreal__le @ A @ B ) @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(36,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ A @ ( c_2Eextreal_2Eextreal__max @ B @ C ) )
= ( ( c_2Eextreal_2Eextreal__le @ A @ B )
| ( c_2Eextreal_2Eextreal__le @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__max) ).
thf(194,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ A @ ( c_2Eextreal_2Eextreal__max @ B @ C ) )
= ( ( c_2Eextreal_2Eextreal__le @ A @ B )
| ( c_2Eextreal_2Eextreal__le @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(5,axiom,
! [TA: $tType,TB: $tType,A: TB > TA] :
( ( ! [B: TA > $o] :
? [C: TB > $o] :
( ( c_2Epred__set_2EIMAGE @ TB @ TA @ A @ C )
= B ) )
= ( ! [B: TA] :
? [C: TB] :
( ( A @ C )
= B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ecardinal_2ESURJECTIVE__IMAGE) ).
thf(63,plain,
! [TA: $tType,TB: $tType,A: TB > TA] :
( ( ! [B: TA > $o] :
? [C: TB > $o] :
( ( c_2Epred__set_2EIMAGE @ TB @ TA @ A @ C )
= B ) )
= ( ! [B: TA] :
? [C: TB] :
( ( A @ C )
= B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(12,axiom,
! [A: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__min @ A @ A )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Emin__refl) ).
thf(95,plain,
! [A: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__min @ A @ A )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(32,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( ( A @ B )
& ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( c_2Eextreal_2Eextreal__le @ C @ B ) ) )
=> ( ( c_2Eextreal_2Eextreal__sup @ A )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Esup__max) ).
thf(177,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( ( A @ B )
& ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( c_2Eextreal_2Eextreal__le @ C @ B ) ) )
=> ( ( c_2Eextreal_2Eextreal__sup @ A )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(19,axiom,
! [TA: $tType,A: TA > $o,B: TA > TA] :
? [C: TA > TA] :
! [D: TA] :
( ( C @ D )
= ( c_2Ebool_2ECOND @ TA @ ( A @ D ) @ D @ ( C @ ( B @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ewhile_2EITERATION) ).
thf(127,plain,
! [TA: $tType,A: TA > $o,B: TA > TA] :
? [C: TA > TA] :
! [D: TA] :
( ( C @ D )
= ( c_2Ebool_2ECOND @ TA @ ( A @ D ) @ D @ ( C @ ( B @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(26,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( ? [C: tyop_2Eextreal_2Eextreal] : ( A @ C )
& ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( C = B ) ) )
=> ( ( c_2Eextreal_2Eextreal__sup @ A )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Esup__const__alt) ).
thf(154,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( ? [C: tyop_2Eextreal_2Eextreal] : ( A @ C )
& ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( C = B ) ) )
=> ( ( c_2Eextreal_2Eextreal__sup @ A )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(8,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o] :
( ( c_2Eextreal_2Eextreal__inf @ A )
= ( c_2Eextreal_2Eextreal__ainv @ ( c_2Eextreal_2Eextreal__sup @ ( c_2Epred__set_2EIMAGE @ tyop_2Eextreal_2Eextreal @ tyop_2Eextreal_2Eextreal @ c_2Eextreal_2Eextreal__ainv @ A ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Eextreal__inf__def) ).
thf(72,plain,
! [A: tyop_2Eextreal_2Eextreal > $o] :
( ( c_2Eextreal_2Eextreal__inf @ A )
= ( c_2Eextreal_2Eextreal__ainv @ ( c_2Eextreal_2Eextreal__sup @ ( c_2Epred__set_2EIMAGE @ tyop_2Eextreal_2Eextreal @ tyop_2Eextreal_2Eextreal @ c_2Eextreal_2Eextreal__ainv @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(33,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ A @ B )
& ( c_2Eextreal_2Eextreal__le @ B @ A ) )
= ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__antisym) ).
thf(186,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__le @ A @ B )
& ( c_2Eextreal_2Eextreal__le @ B @ A ) )
= ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(30,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ B @ ( c_2Eextreal_2Eextreal__inf @ A ) )
= ( ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( c_2Eextreal_2Eextreal__le @ B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__inf) ).
thf(171,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ B @ ( c_2Eextreal_2Eextreal__inf @ A ) )
= ( ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( c_2Eextreal_2Eextreal__le @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(23,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( ? [C: tyop_2Eextreal_2Eextreal] : ( A @ C )
& ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( C = B ) ) )
=> ( ( c_2Eextreal_2Eextreal__inf @ A )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Einf__const__alt) ).
thf(139,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( ? [C: tyop_2Eextreal_2Eextreal] : ( A @ C )
& ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( C = B ) ) )
=> ( ( c_2Eextreal_2Eextreal__inf @ A )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(9,axiom,
! [TA: $tType,A: $o,B: $o,C: TA,D: TA,E: TA,F: TA] :
( ( ( A = B )
& ( B
=> ( C = D ) )
& ( ~ B
=> ( E = F ) ) )
=> ( ( c_2Ebool_2ECOND @ TA @ A @ C @ E )
= ( c_2Ebool_2ECOND @ TA @ B @ D @ F ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2Ebool__case__CONG) ).
thf(75,plain,
! [TA: $tType,A: $o,B: $o,C: TA,D: TA,E: TA,F: TA] :
( ( ( A = B )
& ( B
=> ( C = D ) )
& ( ~ B
=> ( E = F ) ) )
=> ( ( c_2Ebool_2ECOND @ TA @ A @ C @ E )
= ( c_2Ebool_2ECOND @ TA @ B @ D @ F ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(41,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__min @ B @ C ) @ A )
= ( ( c_2Eextreal_2Eextreal__le @ B @ A )
| ( c_2Eextreal_2Eextreal__le @ C @ A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Emin__le) ).
thf(207,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal,C: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__min @ B @ C ) @ A )
= ( ( c_2Eextreal_2Eextreal__le @ B @ A )
| ( c_2Eextreal_2Eextreal__le @ C @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(42,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( A @ B )
=> ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__inf @ A ) @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Einf__le__imp) ).
thf(210,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( A @ B )
=> ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__inf @ A ) @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(22,axiom,
! [TA: $tType,TB: $tType,A: $o,B: TB > TA,C: TB > TA] :
( ( ^ [D: TB] : ( c_2Ebool_2ECOND @ TA @ A @ ( B @ D ) @ ( C @ D ) ) )
= ( c_2Ebool_2ECOND @ ( TB > TA ) @ A @ B @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ECOND__ABS) ).
thf(136,plain,
! [TA: $tType,TB: $tType,A: $o,B: TB > TA,C: TB > TA] :
( ( ^ [D: TB] : ( c_2Ebool_2ECOND @ TA @ A @ ( B @ D ) @ ( C @ D ) ) )
= ( c_2Ebool_2ECOND @ ( TB > TA ) @ A @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(51,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__inf @ A )
= B )
= ( ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( c_2Eextreal_2Eextreal__le @ B @ C ) )
& ! [C: tyop_2Eextreal_2Eextreal] :
( ! [D: tyop_2Eextreal_2Eextreal] :
( ( A @ D )
=> ( c_2Eextreal_2Eextreal__le @ C @ D ) )
=> ( c_2Eextreal_2Eextreal__le @ C @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Einf__eq) ).
thf(239,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( ( c_2Eextreal_2Eextreal__inf @ A )
= B )
= ( ! [C: tyop_2Eextreal_2Eextreal] :
( ( A @ C )
=> ( c_2Eextreal_2Eextreal__le @ B @ C ) )
& ! [C: tyop_2Eextreal_2Eextreal] :
( ! [D: tyop_2Eextreal_2Eextreal] :
( ( A @ D )
=> ( c_2Eextreal_2Eextreal__le @ C @ D ) )
=> ( c_2Eextreal_2Eextreal__le @ C @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(52,axiom,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ B @ ( c_2Eextreal_2Eextreal__sup @ A ) )
= ( ! [C: tyop_2Eextreal_2Eextreal] :
( ! [D: tyop_2Eextreal_2Eextreal] :
( ( A @ D )
=> ( c_2Eextreal_2Eextreal__le @ D @ C ) )
=> ( c_2Eextreal_2Eextreal__le @ B @ C ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Ele__sup) ).
thf(242,plain,
! [A: tyop_2Eextreal_2Eextreal > $o,B: tyop_2Eextreal_2Eextreal] :
( ( c_2Eextreal_2Eextreal__le @ B @ ( c_2Eextreal_2Eextreal__sup @ A ) )
= ( ! [C: tyop_2Eextreal_2Eextreal] :
( ! [D: tyop_2Eextreal_2Eextreal] :
( ( A @ D )
=> ( c_2Eextreal_2Eextreal__le @ D @ C ) )
=> ( c_2Eextreal_2Eextreal__le @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(27,axiom,
! [TA: $tType,A: TA,B: TA,C: TA,D: $o] :
( ( c_2Ebool_2ECOND @ TA @ D @ C @ ( c_2Ebool_2ECOND @ TA @ D @ B @ A ) )
= ( c_2Ebool_2ECOND @ TA @ D @ C @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2EHolSmt_2Er023) ).
thf(163,plain,
! [TA: $tType,A: TA,B: TA,C: TA,D: $o] :
( ( c_2Ebool_2ECOND @ TA @ D @ C @ ( c_2Ebool_2ECOND @ TA @ D @ B @ A ) )
= ( c_2Ebool_2ECOND @ TA @ D @ C @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(38,axiom,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] : ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__min @ A @ B ) @ A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eextreal_2Emin__le1) ).
thf(200,plain,
! [A: tyop_2Eextreal_2Eextreal,B: tyop_2Eextreal_2Eextreal] : ( c_2Eextreal_2Eextreal__le @ ( c_2Eextreal_2Eextreal__min @ A @ B ) @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(413,plain,
$false,
inference(e,[status(thm)],[69,174,169,54,66,218,151,115,202,189,228,57,216,121,89,133,60,220,92,197,124,212,237,205,166,148,191,118,245,98,130,223,226,112,194,63,95,177,127,154,72,186,171,139,75,207,210,136,239,242,163,200]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP021^7 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.11/0.21 % Computer : n005.cluster.edu
% 0.11/0.21 % Model : x86_64 x86_64
% 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.21 % Memory : 8046.5625MB
% 0.11/0.21 % OS : Linux 6.8.0-71-generic
% 0.11/0.21 % CPULimit : 300
% 0.11/0.21 % WCLimit : 300
% 0.11/0.21 % DateTime : Tue Sep 29 19:34:18 UTC 2026
% 0.11/0.21 % CPUTime :
% 0.11/0.21 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.87/0.78 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 8.43/3.98 % [INFO] Parsing done (3195ms).
% 8.43/4.01 % [INFO] Running in sequential loop mode.
% 9.25/4.38 % [INFO] eprover registered as external prover.
% 9.25/4.39 % [INFO] Scanning for conjecture ...
% 12.30/5.26 % [INFO] Found a conjecture (or negated_conjecture) and 13876 axioms. Running axiom selection ...
% 13.42/5.53 % [INFO] Axiom selection finished. Selected 51 axioms (removed 13825 axioms).
% 13.76/5.62 % [INFO] Problem is higher-order (TPTP THF).
% 13.76/5.63 % [INFO] Type checking passed.
% 13.76/5.63 % [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 ...
% 20.41/7.20 % External prover 'e' found a proof!
% 20.41/7.20 % [INFO] Killing All external provers ...
% 20.41/7.20 % Time passed: 6854ms (effective reasoning time: 3191ms)
% 20.41/7.21 % 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)>
% 20.41/7.21 % Axioms used in derivation (51): thm_2EHolSmt_2Ed018, thm_2Eextreal_2Esup__const__alt, thm_2Eextreal_2Emin__refl, thm_2Eextreal_2Esup__le__sup__imp, thm_2Ewhile_2EITERATION, thm_2Eextreal_2Ele__total, thm_2Eextreal_2Einf__min, thm_2Eextreal_2Emin__comm, thm_2Ebool_2ECOND__ABS, thm_2Eextreal_2Eeq__neg, thm_2Ecardinal_2EINJECTIVE__IMAGE, thm_2Eextreal_2Einf__le, thm_2Epred__set_2EIMAGE__ID, thm_2Eextreal_2Ele__neg, thm_2EHolSmt_2Ed020, thm_2Eextreal_2Ele__min, thm_2Eextreal_2Emin__le2__imp, thm_2Ecardinal_2ESURJECTIVE__IMAGE, thm_2Eextreal_2Esup__eq, thm_2EHolSmt_2Er023, thm_2Eextreal_2Ele__max1, thm_2Ebool_2ECOND__RAND, thm_2Eextreal_2Eextreal__inf__def, thm_2Eextreal_2Einf__le__imp, thm_2Eextreal_2Esup__max, thm_2Eextreal_2Emin__le1, thm_2Eextreal_2Ele__max2, thm_2EHolSmt_2Ed017, thm_2Eextreal_2Ele__max, thm_2Eextreal_2Ele__refl, thm_2Eextreal_2Ele__trans, thm_2Eextreal_2Emin__le, thm_2Eextreal_2Ele__sup, thm_2Eextreal_2Emin__le2, thm_2Ebool_2Ebool__case__CONG, thm_2EConseqConv_2ECOND__CLAUSES__ID, thm_2Ebool_2ECOND__CONG, thm_2Eextreal_2Einf__const__alt, thm_2Eextreal_2Eneg__neg, thm_2Ebool_2ECOND__ID, thm_2Ebool_2ECOND__RATOR, thm_2Epred__set_2EIMAGE__11, thm_2Eextreal_2Ele__inf, thm_2Ebool_2Ebool__case__ID, thm_2Eextreal_2Ele__antisym, thm_2Eextreal_2Eextreal__max__def, thm_2Eextreal_2Esup__le, thm_2Eextreal_2Einf__eq, thm_2EHolSmt_2Ed019, thm_2Eextreal_2Eextreal__min__def, thm_2Eextreal_2Ele__sup__imp
% 20.41/7.21 % No. of inferences in proof: 106
% 20.41/7.21 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 6854 ms resp. 3191 ms w/o parsing
% 20.41/7.25 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 20.41/7.26 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------