%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP018^7 : TPTP v9.3.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:06:24 AM UTC 2026
% Result : Theorem 22.15s 7.26s
% Output : Refutation 21.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 32
% Syntax : Number of formulae : 165 ( 145 unt; 0 typ; 1 def)
% Number of atoms : 718 ( 288 equ; 0 cnn)
% Maximal formula atoms : 35 ( 4 avg)
% Number of connectives : 3332 ( 206 ~; 12 |; 107 &;2998 @)
% ( 0 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 49 ( 5 avg)
% Number of types : 22 ( 21 usr)
% Number of type conns : 45 ( 45 >; 0 *; 0 +; 0 <<)
% Number of symbols : 33 ( 30 usr; 8 con; 0-9 aty)
% Number of variables : 416 ( 17 ^; 394 !; 4 ?; 416 :)
% ( 0 !>; 0 ?*; 0 @-; 1 @+)
% 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(skt1_type,type,
skt1: $tType ).
thf(skt2_type,type,
skt2: $tType ).
thf(c_2Ebool_2Eitself__case_decl,type,
c_2Ebool_2Eitself__case:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebool_2Eitself @ TB ) > TA > TA ) ).
thf(c_2Ebool_2Ethe__value_decl,type,
c_2Ebool_2Ethe__value:
!>[TA: $tType] : ( tyop_2Ebool_2Eitself @ TA ) ).
thf(c_2EerrorStateMonad_2EMCOMP_decl,type,
c_2EerrorStateMonad_2EMCOMP:
!>[TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType] : ( ( TB > TA > ( tyop_2Eoption_2Eoption @ TC ) ) > ( TE > TD > ( tyop_2Eoption_2Eoption @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) > TE > TD > ( tyop_2Eoption_2Eoption @ TC ) ) ).
thf(c_2Efcp_2Edimindex_decl,type,
c_2Efcp_2Edimindex:
!>[TA: $tType] : ( ( tyop_2Ebool_2Eitself @ TA ) > tyop_2Enum_2Enum ) ).
thf(c_2Ewords_2Eword__len_decl,type,
c_2Ewords_2Eword__len:
!>[TA: $tType] : ( ( tyop_2Efcp_2Ecart @ $o @ TA ) > tyop_2Enum_2Enum ) ).
thf(c_2Erealax_2Ereal__neg_decl,type,
c_2Erealax_2Ereal__neg: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal ).
thf(c_2Eseq_2Econvergent_decl,type,
c_2Eseq_2Econvergent: ( tyop_2Enum_2Enum > tyop_2Erealax_2Ereal ) > $o ).
thf(c_2Elim_2Etends__real__real_decl,type,
c_2Elim_2Etends__real__real: ( tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal ) > tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal > $o ).
thf(c_2Epowser_2Ediffs_decl,type,
c_2Epowser_2Ediffs: ( tyop_2Enum_2Enum > tyop_2Erealax_2Ereal ) > tyop_2Enum_2Enum > tyop_2Erealax_2Ereal ).
thf(c_2Etransc_2Etan_decl,type,
c_2Etransc_2Etan: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal ).
thf(c_2Ebinary__ieee_2Efloat__bottom_decl,type,
c_2Ebinary__ieee_2Efloat__bottom:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebool_2Eitself @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) > ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) ) ).
thf(c_2Ebinary__ieee_2Efloat__is__infinite_decl,type,
c_2Ebinary__ieee_2Efloat__is__infinite:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) > $o ) ).
thf(c_2Ebinary__ieee_2Efloat__minus__infinity_decl,type,
c_2Ebinary__ieee_2Efloat__minus__infinity:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebool_2Eitself @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) > ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) ) ).
thf(c_2Ebinary__ieee_2Efloat__minus__min_decl,type,
c_2Ebinary__ieee_2Efloat__minus__min:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebool_2Eitself @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) > ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) ) ).
thf(c_2Ebinary__ieee_2Efloat__minus__zero_decl,type,
c_2Ebinary__ieee_2Efloat__minus__zero:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebool_2Eitself @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) > ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) ) ).
thf(c_2Ebinary__ieee_2Efloat__negate_decl,type,
c_2Ebinary__ieee_2Efloat__negate:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) > ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) ) ).
thf(c_2Ebinary__ieee_2Efloat__plus__infinity_decl,type,
c_2Ebinary__ieee_2Efloat__plus__infinity:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebool_2Eitself @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) > ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) ) ).
thf(c_2Ebinary__ieee_2Efloat__plus__min_decl,type,
c_2Ebinary__ieee_2Efloat__plus__min:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebool_2Eitself @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) > ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) ) ).
thf(c_2Ebinary__ieee_2Efloat__plus__zero_decl,type,
c_2Ebinary__ieee_2Efloat__plus__zero:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebool_2Eitself @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) > ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) ) ).
thf(c_2Ebinary__ieee_2Efloat__some__qnan_decl,type,
c_2Ebinary__ieee_2Efloat__some__qnan:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebinary__ieee_2Efp__op @ TB @ TA ) > ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) ) ).
thf(c_2Ebinary__ieee_2Efloat__to__real_decl,type,
c_2Ebinary__ieee_2Efloat__to__real:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) > tyop_2Erealax_2Ereal ) ).
thf(c_2Ebinary__ieee_2Efloat__top_decl,type,
c_2Ebinary__ieee_2Efloat__top:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebool_2Eitself @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) > ( tyop_2Ebinary__ieee_2Efloat @ TB @ TA ) ) ).
thf(c_2Ebinary__ieee_2Eulp_decl,type,
c_2Ebinary__ieee_2Eulp:
!>[TA: $tType,TB: $tType] : ( ( tyop_2Ebool_2Eitself @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) > tyop_2Erealax_2Ereal ) ).
thf(sk1_decl,type,
sk1: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal > ( tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal ) > ( tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal ) > tyop_2Erealax_2Ereal ).
thf(sk1_def,definition,
( sk1
= ( ^ [A: tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal,C: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,D: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal] :
@+[E: tyop_2Erealax_2Ereal] :
~ ( ( E != A )
=> ( ( D @ E )
= ( C @ E ) ) ) ) ) ).
thf(8,axiom,
! [TA: $tType,TB: $tType,TC: $tType,TD: $tType] :
( ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ! [A: tyop_2Ebinary__ieee_2Efloat @ TD @ TC] :
( ( c_2Ebinary__ieee_2Efloat__negate @ TD @ TC @ A )
!= A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebinary__ieee_2Efloat__distinct) ).
thf(53,plain,
! [TA: $tType,TB: $tType,TC: $tType,TD: $tType] :
( ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ! [A: tyop_2Ebinary__ieee_2Efp__op @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TB @ TA @ A ) )
& ! [A: tyop_2Ebinary__ieee_2Efloat @ TD @ TC] :
( ( c_2Ebinary__ieee_2Efloat__negate @ TD @ TC @ A )
!= A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(54,plain,
! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,I: tyop_2Ebinary__ieee_2Efloat @ TA @ TB,H: tyop_2Ebinary__ieee_2Efp__op @ TC @ TD,G: tyop_2Ebinary__ieee_2Efp__op @ TC @ TD,F: tyop_2Ebinary__ieee_2Efp__op @ TC @ TD,E: tyop_2Ebinary__ieee_2Efp__op @ TC @ TD,D: tyop_2Ebinary__ieee_2Efp__op @ TC @ TD,C: tyop_2Ebinary__ieee_2Efp__op @ TC @ TD,B: tyop_2Ebinary__ieee_2Efp__op @ TC @ TD,A: tyop_2Ebinary__ieee_2Efp__op @ TC @ TD] :
( ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TC @ TD @ A ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TC @ TD @ B ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TC @ TD @ C ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TC @ TD @ D ) )
& ( ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TC @ TD @ E ) )
& ( ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TC @ TD @ F ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TC @ TD @ G ) )
& ( ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) )
& ( ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__some__qnan @ TC @ TD @ H ) )
& ( ( c_2Ebinary__ieee_2Efloat__negate @ TA @ TB @ I )
!= I ) ),
inference(cnf,[status(esa)],[53]) ).
thf(73,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(100,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[73]) ).
thf(101,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[100]) ).
thf(58,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(152,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[58]) ).
thf(153,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[152]) ).
thf(84,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(92,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[84]) ).
thf(93,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[92]) ).
thf(28,axiom,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
= ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebinary__ieee_2Efloat__minus__min__def) ).
thf(220,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
= ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(57,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(128,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[57]) ).
thf(129,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[128]) ).
thf(62,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(158,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[62]) ).
thf(159,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[158]) ).
thf(70,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(94,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[70]) ).
thf(95,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[94]) ).
thf(77,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(98,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[77]) ).
thf(99,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[98]) ).
thf(32,axiom,
! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType,TF: $tType,TG: $tType,A: TG > TF > ( tyop_2Eoption_2Eoption @ ( tyop_2Epair_2Eprod @ TB @ TA ) ),B: TB > TA > ( tyop_2Eoption_2Eoption @ ( tyop_2Epair_2Eprod @ TD @ TC ) ),C: TD > TC > ( tyop_2Eoption_2Eoption @ TE )] :
( ( c_2EerrorStateMonad_2EMCOMP @ TG @ TF @ TE @ TD @ TC @ C @ ( c_2EerrorStateMonad_2EMCOMP @ TG @ TF @ ( tyop_2Epair_2Eprod @ TD @ TC ) @ TB @ TA @ B @ A ) )
= ( c_2EerrorStateMonad_2EMCOMP @ TG @ TF @ TE @ TB @ TA @ ( c_2EerrorStateMonad_2EMCOMP @ TB @ TA @ TE @ TD @ TC @ C @ B ) @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2EerrorStateMonad_2EMCOMP__ASSOC) ).
thf(232,plain,
! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType,TF: $tType,TG: $tType,A: TG > TF > ( tyop_2Eoption_2Eoption @ ( tyop_2Epair_2Eprod @ TB @ TA ) ),B: TB > TA > ( tyop_2Eoption_2Eoption @ ( tyop_2Epair_2Eprod @ TD @ TC ) ),C: TD > TC > ( tyop_2Eoption_2Eoption @ TE )] :
( ( c_2EerrorStateMonad_2EMCOMP @ TG @ TF @ TE @ TD @ TC @ C @ ( c_2EerrorStateMonad_2EMCOMP @ TG @ TF @ ( tyop_2Epair_2Eprod @ TD @ TC ) @ TB @ TA @ B @ A ) )
= ( c_2EerrorStateMonad_2EMCOMP @ TG @ TF @ TE @ TB @ TA @ ( c_2EerrorStateMonad_2EMCOMP @ TB @ TA @ TE @ TD @ TC @ C @ B ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(27,axiom,
! [TA: $tType,A: ( tyop_2Ebool_2Eitself @ TA ) > $o] :
( ( ! [B: tyop_2Ebool_2Eitself @ TA] : ( A @ B ) )
= ( A @ ( c_2Ebool_2Ethe__value @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EFORALL__itself) ).
thf(217,plain,
! [TA: $tType,A: ( tyop_2Ebool_2Eitself @ TA ) > $o] :
( ( ! [B: tyop_2Ebool_2Eitself @ TA] : ( A @ B ) )
= ( A @ ( c_2Ebool_2Ethe__value @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(22,axiom,
! [TA: $tType,A: tyop_2Ebool_2Eitself @ TA] :
( A
= ( c_2Ebool_2Ethe__value @ TA ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EITSELF__UNIQUE) ).
thf(202,plain,
! [TA: $tType,A: tyop_2Ebool_2Eitself @ TA] :
( A
= ( c_2Ebool_2Ethe__value @ TA ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(4,axiom,
! [A: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,C: tyop_2Erealax_2Ereal,D: tyop_2Erealax_2Ereal] :
( ! [E: tyop_2Erealax_2Ereal] :
( ( E != D )
=> ( ( A @ E )
= ( B @ E ) ) )
=> ( ( c_2Elim_2Etends__real__real @ A @ C @ D )
= ( c_2Elim_2Etends__real__real @ B @ C @ D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Elim_2ELIM__EQUAL) ).
thf(38,plain,
! [A: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,C: tyop_2Erealax_2Ereal,D: tyop_2Erealax_2Ereal] :
( ! [E: tyop_2Erealax_2Ereal] :
( ( E != D )
=> ( ( A @ E )
= ( B @ E ) ) )
=> ( ( c_2Elim_2Etends__real__real @ A @ C @ D )
= ( c_2Elim_2Etends__real__real @ B @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(39,plain,
! [D: tyop_2Erealax_2Ereal,C: tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,A: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal] :
( ( ( ( sk1 @ D @ C @ B @ A )
!= D )
| ( ( c_2Elim_2Etends__real__real @ A @ C @ D )
= ( c_2Elim_2Etends__real__real @ B @ C @ D ) ) )
& ( ( ( A @ ( sk1 @ D @ C @ B @ A ) )
!= ( B @ ( sk1 @ D @ C @ B @ A ) ) )
| ( ( c_2Elim_2Etends__real__real @ A @ C @ D )
= ( c_2Elim_2Etends__real__real @ B @ C @ D ) ) ) ),
inference(cnf,[status(esa)],[38]) ).
thf(40,plain,
! [D: tyop_2Erealax_2Ereal,C: tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,A: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal] :
( ( ( sk1 @ D @ C @ B @ A )
!= D )
| ( ( c_2Elim_2Etends__real__real @ A @ C @ D )
= ( c_2Elim_2Etends__real__real @ B @ C @ D ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(42,plain,
! [D: tyop_2Erealax_2Ereal,C: tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,A: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal] :
( ( ( sk1 @ D @ C @ B @ A )
!= D )
| ( ( c_2Elim_2Etends__real__real @ A @ C @ D )
= ( c_2Elim_2Etends__real__real @ B @ C @ D ) ) ),
inference(lifteq,[status(thm)],[40]) ).
thf(3,axiom,
! [A: tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal] :
( c_2Elim_2Etends__real__real
@ ^ [C: tyop_2Erealax_2Ereal] : A
@ A
@ B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Elim_2ELIM__CONST) ).
thf(36,plain,
! [A: tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal] :
( c_2Elim_2Etends__real__real
@ ^ [C: tyop_2Erealax_2Ereal] : A
@ A
@ B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(37,plain,
! [B: tyop_2Erealax_2Ereal,A: tyop_2Erealax_2Ereal] :
( c_2Elim_2Etends__real__real
@ ^ [C: tyop_2Erealax_2Ereal] : A
@ A
@ B ),
inference(cnf,[status(esa)],[36]) ).
thf(69,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(124,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[69]) ).
thf(125,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[124]) ).
thf(20,axiom,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
= ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebinary__ieee_2Efloat__minus__infinity__def) ).
thf(196,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
= ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(25,axiom,
! [TA: $tType,TB: $tType,A: TA] :
? [B: ( tyop_2Ebool_2Eitself @ TB ) > TA] :
( ( B @ ( c_2Ebool_2Ethe__value @ TB ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2Eitself__Axiom) ).
thf(211,plain,
! [TA: $tType,TB: $tType,A: TA] :
? [B: ( tyop_2Ebool_2Eitself @ TB ) > TA] :
( ( B @ ( c_2Ebool_2Ethe__value @ TB ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(79,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(120,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[79]) ).
thf(121,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[120]) ).
thf(61,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(132,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[61]) ).
thf(133,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[132]) ).
thf(13,axiom,
! [TA: $tType,A: ( tyop_2Ebool_2Eitself @ TA ) > $o] :
( ( A @ ( c_2Ebool_2Ethe__value @ TA ) )
=> ! [B: tyop_2Ebool_2Eitself @ TA] : ( A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2Eitself__induction) ).
thf(172,plain,
! [TA: $tType,A: ( tyop_2Ebool_2Eitself @ TA ) > $o] :
( ( A @ ( c_2Ebool_2Ethe__value @ TA ) )
=> ! [B: tyop_2Ebool_2Eitself @ TA] : ( A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(173,plain,
! [TA: $tType,B: tyop_2Ebool_2Eitself @ TA,A: ( tyop_2Ebool_2Eitself @ TA ) > $o] :
( ~ ( A @ ( c_2Ebool_2Ethe__value @ TA ) )
| ( A @ B ) ),
inference(cnf,[status(esa)],[172]) ).
thf(174,plain,
! [TA: $tType,A: tyop_2Ebool_2Eitself @ TA] :
( ( ( c_2Ebool_2Ethe__value @ TA )
!= ( c_2Ebool_2Ethe__value @ TA ) )
| ( ( c_2Ebool_2Ethe__value @ TA )
= A ) ),
inference(replace_leibeq,[status(thm)],[173:[bind(A,$thf( (=) @ ( tyop_2Ebool_2Eitself @ TA ) @ ( c_2Ebool_2Ethe__value @ TA ) ))]]) ).
thf(175,plain,
! [TA: $tType,A: tyop_2Ebool_2Eitself @ TA] :
( ( ( c_2Ebool_2Ethe__value @ TA )
!= ( c_2Ebool_2Ethe__value @ TA ) )
| ( ( c_2Ebool_2Ethe__value @ TA )
= A ) ),
inference(lifteq,[status(thm)],[174]) ).
thf(176,plain,
! [TA: $tType,A: tyop_2Ebool_2Eitself @ TA] :
( ( c_2Ebool_2Ethe__value @ TA )
= A ),
inference(simp,[status(thm)],[175]) ).
thf(1,conjecture,
! [TA: $tType,TB: $tType] :
( ( c_2Erealax_2Ereal__neg @ ( c_2Ebinary__ieee_2Eulp @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
= ( c_2Ebinary__ieee_2Efloat__to__real @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebinary__ieee_2Eneg__ulp) ).
thf(2,negated_conjecture,
~ ! [TA: $tType,TB: $tType] :
( ( c_2Erealax_2Ereal__neg @ ( c_2Ebinary__ieee_2Eulp @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
= ( c_2Ebinary__ieee_2Efloat__to__real @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(33,plain,
~ ! [TA: $tType,TB: $tType] :
( ( c_2Erealax_2Ereal__neg @ ( c_2Ebinary__ieee_2Eulp @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
= ( c_2Ebinary__ieee_2Efloat__to__real @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(34,plain,
( ( c_2Erealax_2Ereal__neg @ ( c_2Ebinary__ieee_2Eulp @ skt1 @ skt2 @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ skt1 @ skt2 ) ) ) )
!= ( c_2Ebinary__ieee_2Efloat__to__real @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__negate @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__plus__min @ skt1 @ skt2 @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ skt1 @ skt2 ) ) ) ) ) ),
inference(cnf,[status(esa)],[33]) ).
thf(35,plain,
( ( c_2Erealax_2Ereal__neg @ ( c_2Ebinary__ieee_2Eulp @ skt1 @ skt2 @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ skt1 @ skt2 ) ) ) )
!= ( c_2Ebinary__ieee_2Efloat__to__real @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__negate @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__plus__min @ skt1 @ skt2 @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ skt1 @ skt2 ) ) ) ) ) ),
inference(lifteq,[status(thm)],[34]) ).
thf(10,axiom,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Eulp @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
= ( c_2Ebinary__ieee_2Efloat__to__real @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebinary__ieee_2Eulp) ).
thf(163,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Eulp @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
= ( c_2Ebinary__ieee_2Efloat__to__real @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__plus__min @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(164,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Eulp @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
= ( c_2Ebinary__ieee_2Efloat__to__real @ TA @ TB @ ( c_2Ebinary__ieee_2Efloat__plus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ) ),
inference(cnf,[status(esa)],[163]) ).
thf(165,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Eulp @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
= ( c_2Ebinary__ieee_2Efloat__to__real @ TA @ TB @ ( c_2Ebinary__ieee_2Efloat__plus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ) ),
inference(lifteq,[status(thm)],[164]) ).
thf(235,plain,
( ( c_2Erealax_2Ereal__neg @ ( c_2Ebinary__ieee_2Efloat__to__real @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__plus__min @ skt1 @ skt2 @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ skt1 @ skt2 ) ) ) ) )
!= ( c_2Ebinary__ieee_2Efloat__to__real @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__negate @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__plus__min @ skt1 @ skt2 @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ skt1 @ skt2 ) ) ) ) ) ),
inference(rewrite,[status(thm)],[35,165]) ).
thf(264,plain,
! [A: tyop_2Ebool_2Eitself @ ( tyop_2Epair_2Eprod @ skt1 @ skt2 )] :
( ( ( c_2Erealax_2Ereal__neg @ ( c_2Ebinary__ieee_2Efloat__to__real @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__plus__min @ skt1 @ skt2 @ A ) ) )
!= ( c_2Ebinary__ieee_2Efloat__to__real @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__negate @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__plus__min @ skt1 @ skt2 @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ skt1 @ skt2 ) ) ) ) ) )
| ( ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ skt1 @ skt2 ) )
!= ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ skt1 @ skt2 ) ) ) ),
inference(paramod_ordered,[status(thm)],[176,235]) ).
thf(265,plain,
! [A: tyop_2Ebool_2Eitself @ ( tyop_2Epair_2Eprod @ skt1 @ skt2 )] :
( ( c_2Erealax_2Ereal__neg @ ( c_2Ebinary__ieee_2Efloat__to__real @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__plus__min @ skt1 @ skt2 @ A ) ) )
!= ( c_2Ebinary__ieee_2Efloat__to__real @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__negate @ skt1 @ skt2 @ ( c_2Ebinary__ieee_2Efloat__plus__min @ skt1 @ skt2 @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ skt1 @ skt2 ) ) ) ) ) ),
inference(pattern_uni,[status(thm)],[264:[]]) ).
thf(9,axiom,
! [TA: $tType,A: ( tyop_2Ebool_2Eitself @ TA ) > $o] :
( ( ? [B: tyop_2Ebool_2Eitself @ TA] : ( A @ B ) )
= ( A @ ( c_2Ebool_2Ethe__value @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2EEXISTS__itself) ).
thf(160,plain,
! [TA: $tType,A: ( tyop_2Ebool_2Eitself @ TA ) > $o] :
( ( ? [B: tyop_2Ebool_2Eitself @ TA] : ( A @ B ) )
= ( A @ ( c_2Ebool_2Ethe__value @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(18,axiom,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
= ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebinary__ieee_2Efloat__minus__zero__def) ).
thf(190,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
= ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__plus__zero @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(191,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
= ( c_2Ebinary__ieee_2Efloat__negate @ TA @ TB @ ( c_2Ebinary__ieee_2Efloat__plus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ) ),
inference(cnf,[status(esa)],[190]) ).
thf(192,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__negate @ TA @ TB @ ( c_2Ebinary__ieee_2Efloat__plus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) )
= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(lifteq,[status(thm)],[191]) ).
thf(74,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(136,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[74]) ).
thf(137,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[136]) ).
thf(31,axiom,
! [A: tyop_2Erealax_2Ereal] :
( ( c_2Etransc_2Etan @ ( c_2Erealax_2Ereal__neg @ A ) )
= ( c_2Erealax_2Ereal__neg @ ( c_2Etransc_2Etan @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Etransc_2ETAN__NEG) ).
thf(229,plain,
! [A: tyop_2Erealax_2Ereal] :
( ( c_2Etransc_2Etan @ ( c_2Erealax_2Ereal__neg @ A ) )
= ( c_2Erealax_2Ereal__neg @ ( c_2Etransc_2Etan @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(65,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(96,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[65]) ).
thf(97,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[96]) ).
thf(12,axiom,
! [TA: $tType,TB: $tType,A: tyop_2Ebinary__ieee_2Efloat @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ A ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebinary__ieee_2Efloat__negate__negate) ).
thf(169,plain,
! [TA: $tType,TB: $tType,A: tyop_2Ebinary__ieee_2Efloat @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ A ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(85,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(140,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[85]) ).
thf(141,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[140]) ).
thf(80,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(108,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[80]) ).
thf(109,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[108]) ).
thf(19,axiom,
! [TA: $tType,A: tyop_2Efcp_2Ecart @ $o @ TA] :
( ( c_2Ewords_2Eword__len @ TA @ A )
= ( c_2Efcp_2Edimindex @ TA @ ( c_2Ebool_2Ethe__value @ TA ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ewords_2Eword__len__def) ).
thf(193,plain,
! [TA: $tType,A: tyop_2Efcp_2Ecart @ $o @ TA] :
( ( c_2Ewords_2Eword__len @ TA @ A )
= ( c_2Efcp_2Edimindex @ TA @ ( c_2Ebool_2Ethe__value @ TA ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(59,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(104,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[59]) ).
thf(105,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[104]) ).
thf(23,axiom,
! [A: tyop_2Erealax_2Ereal] :
( ( c_2Erealax_2Ereal__neg @ ( c_2Erealax_2Ereal__neg @ A ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ereal_2EREAL__NEG__NEG) ).
thf(205,plain,
! [A: tyop_2Erealax_2Ereal] :
( ( c_2Erealax_2Ereal__neg @ ( c_2Erealax_2Ereal__neg @ A ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(11,axiom,
! [A: tyop_2Enum_2Enum > tyop_2Erealax_2Ereal] :
( ( c_2Epowser_2Ediffs
@ ^ [B: tyop_2Enum_2Enum] : ( c_2Erealax_2Ereal__neg @ ( A @ B ) ) )
= ( ^ [B: tyop_2Enum_2Enum] : ( c_2Erealax_2Ereal__neg @ ( c_2Epowser_2Ediffs @ A @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Epowser_2EDIFFS__NEG) ).
thf(166,plain,
! [A: tyop_2Enum_2Enum > tyop_2Erealax_2Ereal] :
( ( c_2Epowser_2Ediffs
@ ^ [B: tyop_2Enum_2Enum] : ( c_2Erealax_2Ereal__neg @ ( A @ B ) ) )
= ( ^ [B: tyop_2Enum_2Enum] : ( c_2Erealax_2Ereal__neg @ ( c_2Epowser_2Ediffs @ A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(15,axiom,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
= ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebinary__ieee_2Efloat__bottom__def) ).
thf(180,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__bottom @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) )
= ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__top @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(76,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(148,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[76]) ).
thf(149,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[148]) ).
thf(5,axiom,
! [TA: $tType,TB: $tType,A: tyop_2Ebinary__ieee_2Efloat @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__is__infinite @ TB @ TA @ A )
= ( ( A
= ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
| ( A
= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebinary__ieee_2Efloat__infinities) ).
thf(44,plain,
! [TA: $tType,TB: $tType,A: tyop_2Ebinary__ieee_2Efloat @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__is__infinite @ TB @ TA @ A )
= ( ( A
= ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
| ( A
= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(17,axiom,
! [A: tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal] :
( ( ( c_2Erealax_2Ereal__neg @ A )
= B )
= ( A
= ( c_2Erealax_2Ereal__neg @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ereal_2EREAL__NEG__EQ) ).
thf(187,plain,
! [A: tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal] :
( ( ( c_2Erealax_2Ereal__neg @ A )
= B )
= ( A
= ( c_2Erealax_2Ereal__neg @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(67,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(112,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[67]) ).
thf(113,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[112]) ).
thf(24,axiom,
! [A: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal,C: tyop_2Erealax_2Ereal] :
( ( c_2Elim_2Etends__real__real @ A @ B @ C )
= ( c_2Elim_2Etends__real__real
@ ^ [D: tyop_2Erealax_2Ereal] : ( c_2Erealax_2Ereal__neg @ ( A @ D ) )
@ ( c_2Erealax_2Ereal__neg @ B )
@ C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Elim_2ELIM__NEG) ).
thf(208,plain,
! [A: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal,C: tyop_2Erealax_2Ereal] :
( ( c_2Elim_2Etends__real__real @ A @ B @ C )
= ( c_2Elim_2Etends__real__real
@ ^ [D: tyop_2Erealax_2Ereal] : ( c_2Erealax_2Ereal__neg @ ( A @ D ) )
@ ( c_2Erealax_2Ereal__neg @ B )
@ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(64,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(102,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[64]) ).
thf(103,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[102]) ).
thf(56,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(90,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[56]) ).
thf(91,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[90]) ).
thf(29,axiom,
! [TA: $tType,TB: $tType,A: TA] :
( ( c_2Ebool_2Eitself__case @ TB @ TA @ ( c_2Ebool_2Ethe__value @ TB ) @ A )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebool_2Eitself__case__thm) ).
thf(223,plain,
! [TA: $tType,TB: $tType,A: TA] :
( ( c_2Ebool_2Eitself__case @ TB @ TA @ ( c_2Ebool_2Ethe__value @ TB ) @ A )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(89,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(134,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[89]) ).
thf(135,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[134]) ).
thf(30,axiom,
! [A: tyop_2Erealax_2Ereal] :
( ( c_2Erealax_2Ereal__neg @ ( c_2Erealax_2Ereal__neg @ A ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ereal_2EREAL__NEGNEG) ).
thf(226,plain,
! [A: tyop_2Erealax_2Ereal] :
( ( c_2Erealax_2Ereal__neg @ ( c_2Erealax_2Ereal__neg @ A ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(83,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(122,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[83]) ).
thf(123,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__top @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[122]) ).
thf(86,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(144,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[86]) ).
thf(145,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__bottom @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[144]) ).
thf(21,axiom,
! [TA: $tType,TB: $tType,A: tyop_2Ebinary__ieee_2Efloat @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__to__real @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ A ) )
= ( c_2Erealax_2Ereal__neg @ ( c_2Ebinary__ieee_2Efloat__to__real @ TB @ TA @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebinary__ieee_2Efloat__to__real__negate) ).
thf(199,plain,
! [TA: $tType,TB: $tType,A: tyop_2Ebinary__ieee_2Efloat @ TB @ TA] :
( ( c_2Ebinary__ieee_2Efloat__to__real @ TB @ TA @ ( c_2Ebinary__ieee_2Efloat__negate @ TB @ TA @ A ) )
= ( c_2Erealax_2Ereal__neg @ ( c_2Ebinary__ieee_2Efloat__to__real @ TB @ TA @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(14,axiom,
! [A: tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal] :
( ( ( c_2Erealax_2Ereal__neg @ A )
= ( c_2Erealax_2Ereal__neg @ B ) )
= ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ereal_2EREAL__EQ__NEG) ).
thf(177,plain,
! [A: tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal] :
( ( ( c_2Erealax_2Ereal__neg @ A )
= ( c_2Erealax_2Ereal__neg @ B ) )
= ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(181,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__bottom @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
= ( c_2Ebinary__ieee_2Efloat__negate @ TA @ TB @ ( c_2Ebinary__ieee_2Efloat__top @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ) ),
inference(cnf,[status(esa)],[180]) ).
thf(182,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__negate @ TA @ TB @ ( c_2Ebinary__ieee_2Efloat__top @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) )
= ( c_2Ebinary__ieee_2Efloat__bottom @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(lifteq,[status(thm)],[181]) ).
thf(71,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(142,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[71]) ).
thf(143,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__zero @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[142]) ).
thf(41,plain,
! [D: tyop_2Erealax_2Ereal,C: tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,A: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal] :
( ( ( A @ ( sk1 @ D @ C @ B @ A ) )
!= ( B @ ( sk1 @ D @ C @ B @ A ) ) )
| ( ( c_2Elim_2Etends__real__real @ A @ C @ D )
= ( c_2Elim_2Etends__real__real @ B @ C @ D ) ) ),
inference(cnfConj,[status(thm)],[39]) ).
thf(43,plain,
! [D: tyop_2Erealax_2Ereal,C: tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,A: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal] :
( ( ( A @ ( sk1 @ D @ C @ B @ A ) )
!= ( B @ ( sk1 @ D @ C @ B @ A ) ) )
| ( ( c_2Elim_2Etends__real__real @ A @ C @ D )
= ( c_2Elim_2Etends__real__real @ B @ C @ D ) ) ),
inference(lifteq,[status(thm)],[41]) ).
thf(55,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(118,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[55]) ).
thf(119,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[118]) ).
thf(26,axiom,
! [A: tyop_2Enum_2Enum > tyop_2Erealax_2Ereal] :
( ( c_2Eseq_2Econvergent @ A )
= ( c_2Eseq_2Econvergent
@ ^ [B: tyop_2Enum_2Enum] : ( c_2Erealax_2Ereal__neg @ ( A @ B ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Eseq_2ESEQ__NEG__CONV) ).
thf(214,plain,
! [A: tyop_2Enum_2Enum > tyop_2Erealax_2Ereal] :
( ( c_2Eseq_2Econvergent @ A )
= ( c_2Eseq_2Econvergent
@ ^ [B: tyop_2Enum_2Enum] : ( c_2Erealax_2Ereal__neg @ ( A @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(75,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(150,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[75]) ).
thf(151,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[150]) ).
thf(7,axiom,
! [A: tyop_2Erealax_2Ereal] :
( c_2Elim_2Etends__real__real
@ ^ [B: tyop_2Erealax_2Ereal] : B
@ A
@ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Elim_2ELIM__X) ).
thf(51,plain,
! [A: tyop_2Erealax_2Ereal] :
( c_2Elim_2Etends__real__real
@ ^ [B: tyop_2Erealax_2Ereal] : B
@ A
@ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(16,axiom,
! [TA: $tType,TB: $tType,A: tyop_2Ebinary__ieee_2Efloat @ TB @ TA] :
~ ( ( A
= ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( A
= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Ebinary__ieee_2Efloat__infinities__distinct) ).
thf(183,plain,
! [TA: $tType,TB: $tType,A: tyop_2Ebinary__ieee_2Efloat @ TB @ TA] :
~ ( ( A
= ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) )
& ( A
= ( c_2Ebinary__ieee_2Efloat__minus__infinity @ TB @ TA @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TB @ TA ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(78,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(cnfConj,[status(thm)],[54]) ).
thf(130,plain,
! [TC: $tType,TD: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TC @ TD @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TC @ TD ) ) ) ),
inference(lifteq,[status(thm)],[78]) ).
thf(131,plain,
! [TA: $tType,TB: $tType] :
( ( c_2Ebinary__ieee_2Efloat__plus__min @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) )
!= ( c_2Ebinary__ieee_2Efloat__plus__infinity @ TA @ TB @ ( c_2Ebool_2Ethe__value @ ( tyop_2Epair_2Eprod @ TA @ TB ) ) ) ),
inference(simp,[status(thm)],[130]) ).
thf(6,axiom,
! [A: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal,C: tyop_2Erealax_2Ereal,D: tyop_2Erealax_2Ereal] :
( ( ( c_2Elim_2Etends__real__real @ A @ B @ D )
& ( c_2Elim_2Etends__real__real @ A @ C @ D ) )
=> ( B = C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',thm_2Elim_2ELIM__UNIQ) ).
thf(47,plain,
! [A: tyop_2Erealax_2Ereal > tyop_2Erealax_2Ereal,B: tyop_2Erealax_2Ereal,C: tyop_2Erealax_2Ereal,D: tyop_2Erealax_2Ereal] :
( ( ( c_2Elim_2Etends__real__real @ A @ B @ D )
& ( c_2Elim_2Etends__real__real @ A @ C @ D ) )
=> ( B = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(466,plain,
$false,
inference(e,[status(thm)],[101,153,93,220,129,159,95,99,232,217,202,42,37,125,196,211,121,133,265,38,160,192,137,165,33,229,97,53,169,141,109,193,105,205,166,180,149,176,44,187,172,113,208,103,91,223,135,226,123,145,199,177,182,143,43,119,235,214,151,36,51,190,183,163,131,47]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP018^7 : TPTP v9.3.1. Bugfixed v7.5.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n009.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 19:33:19 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.86/0.79 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 9.79/3.72 % [INFO] Parsing done (2922ms).
% 9.79/3.74 % [INFO] Running in sequential loop mode.
% 10.29/4.12 % [INFO] eprover registered as external prover.
% 10.29/4.12 % [INFO] Scanning for conjecture ...
% 13.26/4.95 % [INFO] Found a conjecture (or negated_conjecture) and 12436 axioms. Running axiom selection ...
% 14.73/5.31 % [INFO] Axiom selection finished. Selected 30 axioms (removed 12406 axioms).
% 15.09/5.41 % [INFO] Problem is higher-order (TPTP THF).
% 15.09/5.42 % [INFO] Type checking passed.
% 15.09/5.43 % [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 ...
% 17.16/6.11 % [INFO] [Domain constraints] Detected constraint on tyop_2Ebool_2Eitself(1)
% 17.16/6.11 % [INFO] [Domain constraints] dom(tyop_2Ebool_2Eitself(1)) ⊆ {c_2Ebool_2Ethe__value ⋅ (1;⊥)}
% 17.68/6.15 % [INFO] [Domain constraints] Detected constraint on tyop_2Ebool_2Eitself(1)
% 17.68/6.15 % [INFO] [Domain constraints] dom(tyop_2Ebool_2Eitself(1)) ⊆ {c_2Ebool_2Ethe__value ⋅ (1;⊥)}
% 22.15/7.26 % External prover 'e' found a proof!
% 22.15/7.26 % [INFO] Killing All external provers ...
% 22.15/7.26 % Time passed: 6908ms (effective reasoning time: 3514ms)
% 22.15/7.26 % 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)>
% 22.15/7.26 % Axioms used in derivation (30): thm_2Ebinary__ieee_2Efloat__infinities, thm_2Ebinary__ieee_2Efloat__distinct, thm_2Elim_2ELIM__CONST, thm_2Ebool_2EFORALL__itself, thm_2Ebinary__ieee_2Efloat__to__real__negate, thm_2Elim_2ELIM__X, thm_2Ebool_2Eitself__case__thm, thm_2Ebool_2EITSELF__UNIQUE, thm_2Elim_2ELIM__EQUAL, thm_2Ebool_2Eitself__induction, thm_2Ebinary__ieee_2Efloat__minus__zero__def, thm_2Ereal_2EREAL__NEGNEG, thm_2Ebool_2Eitself__Axiom, thm_2Ereal_2EREAL__NEG__NEG, thm_2Ebinary__ieee_2Efloat__negate__negate, thm_2Ebinary__ieee_2Efloat__minus__infinity__def, thm_2Ebool_2EEXISTS__itself, thm_2Ebinary__ieee_2Efloat__minus__min__def, thm_2Ewords_2Eword__len__def, thm_2EerrorStateMonad_2EMCOMP__ASSOC, thm_2Elim_2ELIM__NEG, thm_2Ebinary__ieee_2Efloat__bottom__def, thm_2Ereal_2EREAL__NEG__EQ, thm_2Epowser_2EDIFFS__NEG, thm_2Ereal_2EREAL__EQ__NEG, thm_2Elim_2ELIM__UNIQ, thm_2Eseq_2ESEQ__NEG__CONV, thm_2Ebinary__ieee_2Eulp, thm_2Ebinary__ieee_2Efloat__infinities__distinct, thm_2Etransc_2ETAN__NEG
% 22.15/7.26 % No. of inferences in proof: 164
% 22.15/7.26 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 6908 ms resp. 3514 ms w/o parsing
% 21.93/7.38 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 21.93/7.39 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------