%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP015^1 : 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 : n020.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:21 AM UTC 2026
% Result : Theorem 15.72s 4.64s
% Output : Refutation 16.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 69
% Syntax : Number of formulae : 140 ( 132 unt; 0 typ; 0 def)
% Number of atoms : 242 ( 165 equ; 0 cnn)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 2401 ( 10 ~; 2 |; 12 &;2367 @)
% ( 0 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 avg)
% Number of types : 6 ( 5 usr)
% Number of type conns : 60 ( 60 >; 0 *; 0 +; 0 <<)
% Number of symbols : 67 ( 65 usr; 19 con; 0-3 aty)
% Number of variables : 255 ( 0 ^; 253 !; 2 ?; 255 :)
% Comments :
%------------------------------------------------------------------------------
thf(u_type,type,
u: $tType ).
thf(d_type,type,
d: $tType ).
thf(du_type,type,
du: $tType ).
thf(mono_2Etyop_2Einteger_2Eint_type,type,
mono_2Etyop_2Einteger_2Eint: $tType ).
thf(mono_2Etyop_2Enum_2Enum_type,type,
mono_2Etyop_2Enum_2Enum: $tType ).
thf(tyop_2Ebool_2Eitself_decl,type,
tyop_2Ebool_2Eitself: d > d ).
thf(tyop_2Efcp_2Ecart_decl,type,
tyop_2Efcp_2Ecart: d > d > d ).
thf(tyop_2Einteger_2Eint_decl,type,
tyop_2Einteger_2Eint: d ).
thf(tyop_2Emin_2Ebool_decl,type,
tyop_2Emin_2Ebool: d ).
thf(tyop_2Emin_2Efun_decl,type,
tyop_2Emin_2Efun: d > d > d ).
thf(tyop_2Enum_2Enum_decl,type,
tyop_2Enum_2Enum: d ).
thf(s_decl,type,
s: d > u > du ).
thf(app_2E2_decl,type,
app_2E2: du > du > u ).
thf(combin_i_2E0_decl,type,
combin_i_2E0: u ).
thf(combin_k_2E0_decl,type,
combin_k_2E0: u ).
thf(combin_s_2E0_decl,type,
combin_s_2E0: u ).
thf(c_2Ebool_2E_21_2E0_decl,type,
c_2Ebool_2E_21_2E0: u ).
thf(c_2Ebool_2E_21_2E1_decl,type,
c_2Ebool_2E_21_2E1: du > u ).
thf(c_2Emin_2E_3D_2E0_decl,type,
c_2Emin_2E_3D_2E0: u ).
thf(c_2Emin_2E_3D_2E2_decl,type,
c_2Emin_2E_3D_2E2: du > du > u ).
thf(c_2Ebool_2E_3F_2E0_decl,type,
c_2Ebool_2E_3F_2E0: u ).
thf(c_2Ebool_2E_3F_2E1_decl,type,
c_2Ebool_2E_3F_2E1: du > u ).
thf(c_2Ebool_2ECOND_2E0_decl,type,
c_2Ebool_2ECOND_2E0: u ).
thf(c_2Ebool_2ECOND_2E3_decl,type,
c_2Ebool_2ECOND_2E3: du > du > du > u ).
thf(c_2Ewords_2Edimword_2E0_decl,type,
c_2Ewords_2Edimword_2E0: u ).
thf(c_2Ewords_2Edimword_2E1_decl,type,
c_2Ewords_2Edimword_2E1: du > u ).
thf(c_2Einteger__word_2Ei2w_2E0_decl,type,
c_2Einteger__word_2Ei2w_2E0: u ).
thf(c_2Einteger__word_2Ei2w_2E1_decl,type,
c_2Einteger__word_2Ei2w_2E1: du > u ).
thf(c_2Ewords_2En2w_2E0_decl,type,
c_2Ewords_2En2w_2E0: u ).
thf(c_2Ewords_2En2w_2E1_decl,type,
c_2Ewords_2En2w_2E1: du > u ).
thf(c_2Ebool_2Ethe__value_2E0_decl,type,
c_2Ebool_2Ethe__value_2E0: u ).
thf(c_2Ewords_2Eword__2comp_2E0_decl,type,
c_2Ewords_2Eword__2comp_2E0: u ).
thf(c_2Ewords_2Eword__2comp_2E1_decl,type,
c_2Ewords_2Eword__2comp_2E1: du > u ).
thf(mono_2Ec_2Enum_2E0_decl,type,
mono_2Ec_2Enum_2E0: mono_2Etyop_2Enum_2Enum ).
thf(mono_2Ec_2Eprim__rec_2E_3C_decl,type,
mono_2Ec_2Eprim__rec_2E_3C: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o ).
thf(mono_2Ec_2Ebool_2EF_decl,type,
mono_2Ec_2Ebool_2EF: $o ).
thf(mono_2Ec_2Earithmetic_2EMOD_decl,type,
mono_2Ec_2Earithmetic_2EMOD: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(mono_2Ec_2Einteger_2ENum_decl,type,
mono_2Ec_2Einteger_2ENum: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Enum_2Enum ).
thf(mono_2Ec_2Ebool_2ET_decl,type,
mono_2Ec_2Ebool_2ET: $o ).
thf(mono_2Ec_2Einteger_2Eint__lt_decl,type,
mono_2Ec_2Einteger_2Eint__lt: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o ).
thf(mono_2Ec_2Einteger_2Eint__neg_decl,type,
mono_2Ec_2Einteger_2Eint__neg: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint ).
thf(mono_2Ec_2Einteger_2Eint__of__num_decl,type,
mono_2Ec_2Einteger_2Eint__of__num: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint ).
thf(i_mono_2Etyop_2Emin_2Ebool_decl,type,
i_mono_2Etyop_2Emin_2Ebool: $o > u ).
thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_decl,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: ( $o > $o ) > u ).
thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29_decl,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: ( $o > $o > $o ) > u ).
thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_decl,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29: ( mono_2Etyop_2Einteger_2Eint > $o ) > u ).
thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29_decl,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29: ( mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o ) > u ).
thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29_decl,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29: ( mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint ) > u ).
thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29_decl,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29: ( mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Enum_2Enum ) > u ).
thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_decl,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29: ( mono_2Etyop_2Enum_2Enum > $o ) > u ).
thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_decl,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29: ( mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o ) > u ).
thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_decl,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29: ( mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ) > u ).
thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29_decl,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29: ( mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint ) > u ).
thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_decl,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29: ( mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ) > u ).
thf(i_mono_2Etyop_2Einteger_2Eint_decl,type,
i_mono_2Etyop_2Einteger_2Eint: mono_2Etyop_2Einteger_2Eint > u ).
thf(i_mono_2Etyop_2Enum_2Enum_decl,type,
i_mono_2Etyop_2Enum_2Enum: mono_2Etyop_2Enum_2Enum > u ).
thf(j_mono_2Etyop_2Emin_2Ebool_decl,type,
j_mono_2Etyop_2Emin_2Ebool: du > $o ).
thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_decl,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: du > $o > $o ).
thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29_decl,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: du > $o > $o > $o ).
thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_decl,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29: du > mono_2Etyop_2Einteger_2Eint > $o ).
thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29_decl,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29: du > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o ).
thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29_decl,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29: du > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint ).
thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29_decl,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29: du > mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Enum_2Enum ).
thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_decl,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29: du > mono_2Etyop_2Enum_2Enum > $o ).
thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29_decl,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29: du > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o ).
thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29_decl,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29: du > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29_decl,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29: du > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint ).
thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_decl,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29: du > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum ).
thf(j_mono_2Etyop_2Einteger_2Eint_decl,type,
j_mono_2Etyop_2Einteger_2Eint: du > mono_2Etyop_2Einteger_2Eint ).
thf(j_mono_2Etyop_2Enum_2Enum_decl,type,
j_mono_2Etyop_2Enum_2Enum: du > mono_2Etyop_2Enum_2Enum ).
thf(54,axiom,
! [A: d,B: mono_2Etyop_2Enum_2Enum,C: mono_2Etyop_2Enum_2Enum] :
( ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ C ) ) ) ) )
= ( ( mono_2Ec_2Earithmetic_2EMOD @ B @ ( j_mono_2Etyop_2Enum_2Enum @ ( s @ tyop_2Enum_2Enum @ ( c_2Ewords_2Edimword_2E1 @ ( s @ ( tyop_2Ebool_2Eitself @ A ) @ c_2Ebool_2Ethe__value_2E0 ) ) ) ) )
= ( mono_2Ec_2Earithmetic_2EMOD @ C @ ( j_mono_2Etyop_2Enum_2Enum @ ( s @ tyop_2Enum_2Enum @ ( c_2Ewords_2Edimword_2E1 @ ( s @ ( tyop_2Ebool_2Eitself @ A ) @ c_2Ebool_2Ethe__value_2E0 ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ewords_2En2w__11) ).
thf(385,plain,
! [A: d,B: mono_2Etyop_2Enum_2Enum,C: mono_2Etyop_2Enum_2Enum] :
( ( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ C ) ) ) ) )
= ( ( mono_2Ec_2Earithmetic_2EMOD @ B @ ( j_mono_2Etyop_2Enum_2Enum @ ( s @ tyop_2Enum_2Enum @ ( c_2Ewords_2Edimword_2E1 @ ( s @ ( tyop_2Ebool_2Eitself @ A ) @ c_2Ebool_2Ethe__value_2E0 ) ) ) ) )
= ( mono_2Ec_2Earithmetic_2EMOD @ C @ ( j_mono_2Etyop_2Enum_2Enum @ ( s @ tyop_2Enum_2Enum @ ( c_2Ewords_2Edimword_2E1 @ ( s @ ( tyop_2Ebool_2Eitself @ A ) @ c_2Ebool_2Ethe__value_2E0 ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(44,axiom,
! [A: d] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2Eword__2comp_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ewords_2EWORD__NEG__0) ).
thf(344,plain,
! [A: d] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2Eword__2comp_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(63,axiom,
! [A: d,B: u,C: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Emin_2E_3D_2E2 @ ( s @ A @ B ) @ ( s @ A @ C ) ) ) )
= ( ( s @ A @ B )
= ( s @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Elogic_2E_3D) ).
thf(416,plain,
! [A: d,B: u,C: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Emin_2E_3D_2E2 @ ( s @ A @ B ) @ ( s @ A @ C ) ) ) )
= ( ( s @ A @ B )
= ( s @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(59,axiom,
! [A: mono_2Etyop_2Enum_2Enum > $o,B: mono_2Etyop_2Enum_2Enum] :
( ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( A @ B ) ) )
= ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 @ A ) ) @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool) ).
thf(398,plain,
! [A: mono_2Etyop_2Enum_2Enum > $o,B: mono_2Etyop_2Enum_2Enum] :
( ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( A @ B ) ) )
= ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 @ A ) ) @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(19,axiom,
! [A: d,B: mono_2Etyop_2Enum_2Enum] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) ) @ c_2Ewords_2En2w_2E0 ) @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq1_2Ec_2Ewords_2En2w_2E1_2Emono_2EA_27a) ).
thf(213,plain,
! [A: d,B: mono_2Etyop_2Enum_2Enum] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) ) @ c_2Ewords_2En2w_2E0 ) @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(14,axiom,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29) ).
thf(112,plain,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(13,axiom,
! [A: d] :
( ! [B: u,C: u] :
( ( s @ A @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ mono_2Ec_2Ebool_2ET ) ) @ ( s @ A @ B ) @ ( s @ A @ C ) ) )
= ( s @ A @ B ) )
& ! [B: u,C: u] :
( ( s @ A @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ mono_2Ec_2Ebool_2EF ) ) @ ( s @ A @ B ) @ ( s @ A @ C ) ) )
= ( s @ A @ C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2Ebool__case__thm) ).
thf(104,plain,
! [A: d] :
( ! [B: u,C: u] :
( ( s @ A @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ mono_2Ec_2Ebool_2ET ) ) @ ( s @ A @ B ) @ ( s @ A @ C ) ) )
= ( s @ A @ B ) )
& ! [B: u,C: u] :
( ( s @ A @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ mono_2Ec_2Ebool_2EF ) ) @ ( s @ A @ B ) @ ( s @ A @ C ) ) )
= ( s @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(65,axiom,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum,B: mono_2Etyop_2Enum_2Enum] :
( ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( A @ B ) ) )
= ( s @ tyop_2Enum_2Enum @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 @ A ) ) @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum) ).
thf(422,plain,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum,B: mono_2Etyop_2Enum_2Enum] :
( ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( A @ B ) ) )
= ( s @ tyop_2Enum_2Enum @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 @ A ) ) @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(51,axiom,
! [A: d,B: $o,C: $o,D: u,E: u,F: u,G: u] :
( ( ( B = C )
& ( C
=> ( ( s @ A @ D )
= ( s @ A @ E ) ) )
& ( ~ C
=> ( ( s @ A @ F )
= ( s @ A @ G ) ) ) )
=> ( ( s @ A @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) @ ( s @ A @ D ) @ ( s @ A @ F ) ) )
= ( s @ A @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ C ) ) @ ( s @ A @ E ) @ ( s @ A @ G ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ECOND__CONG) ).
thf(365,plain,
! [A: d,B: $o,C: $o,D: u,E: u,F: u,G: u] :
( ( ( B = C )
& ( C
=> ( ( s @ A @ D )
= ( s @ A @ E ) ) )
& ( ~ C
=> ( ( s @ A @ F )
= ( s @ A @ G ) ) ) )
=> ( ( s @ A @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) @ ( s @ A @ D ) @ ( s @ A @ F ) ) )
= ( s @ A @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ C ) ) @ ( s @ A @ E ) @ ( s @ A @ G ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(12,axiom,
! [A: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Einteger_2ENum @ ( mono_2Ec_2Einteger_2Eint__of__num @ A ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger_2ENUM__OF__INT) ).
thf(101,plain,
! [A: mono_2Etyop_2Enum_2Enum] :
( ( mono_2Ec_2Einteger_2ENum @ ( mono_2Ec_2Einteger_2Eint__of__num @ A ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(45,axiom,
! [A: d,B: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_21_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) ) ) )
= ( ! [C: u] : ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) @ ( s @ A @ C ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Equant_2E_21) ).
thf(347,plain,
! [A: d,B: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_21_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) ) ) )
= ( ! [C: u] : ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) @ ( s @ A @ C ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(15,axiom,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29) ).
thf(115,plain,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(52,axiom,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29) ).
thf(379,plain,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(61,axiom,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint,B: mono_2Etyop_2Enum_2Enum] :
( ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( A @ B ) ) )
= ( s @ tyop_2Einteger_2Eint @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Einteger_2Eint ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29 @ A ) ) @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Einteger_2Eint) ).
thf(404,plain,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint,B: mono_2Etyop_2Enum_2Enum] :
( ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( A @ B ) ) )
= ( s @ tyop_2Einteger_2Eint @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Einteger_2Eint ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29 @ A ) ) @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(35,axiom,
! [A: d,B: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_3F_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) ) ) )
= ( ? [C: u] : ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) @ ( s @ A @ C ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Equant_2E_3F) ).
thf(301,plain,
! [A: d,B: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_3F_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) ) ) )
= ( ? [C: u] : ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) @ ( s @ A @ C ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(20,axiom,
! [A: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Einteger_2Eint ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29 @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29) ).
thf(216,plain,
! [A: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Einteger_2Eint ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29 @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(17,axiom,
! [A: $o] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Ebool) ).
thf(121,plain,
! [A: $o] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(47,axiom,
! [A: d,B: u] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2Eword__2comp_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ B ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) ) @ c_2Ewords_2Eword__2comp_2E0 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq1_2Ec_2Ewords_2Eword__2comp_2E1_2Emono_2EA_27a) ).
thf(353,plain,
! [A: d,B: u] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2Eword__2comp_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ B ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) ) @ c_2Ewords_2Eword__2comp_2E0 ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ B ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(22,axiom,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29) ).
thf(221,plain,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(8,axiom,
! [A: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Enum_2Enum] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29 @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29) ).
thf(89,plain,
! [A: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Enum_2Enum] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29 @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(67,axiom,
! [A: d,B: d,C: u,D: u] :
( ! [E: u] :
( ( s @ B @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ B ) @ C ) @ ( s @ A @ E ) ) )
= ( s @ B @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ B ) @ D ) @ ( s @ A @ E ) ) ) )
=> ( ( s @ ( tyop_2Emin_2Efun @ A @ B ) @ C )
= ( s @ ( tyop_2Emin_2Efun @ A @ B ) @ D ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Eeq__ext) ).
thf(428,plain,
! [A: d,B: d,C: u,D: u] :
( ! [E: u] :
( ( s @ B @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ B ) @ C ) @ ( s @ A @ E ) ) )
= ( s @ B @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ B ) @ D ) @ ( s @ A @ E ) ) ) )
=> ( ( s @ ( tyop_2Emin_2Efun @ A @ B ) @ C )
= ( s @ ( tyop_2Emin_2Efun @ A @ B ) @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(3,axiom,
! [A: $o] :
( mono_2Ec_2Ebool_2EF
=> A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EFALSITY) ).
thf(74,plain,
! [A: $o] :
( mono_2Ec_2Ebool_2EF
=> A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(37,axiom,
! [A: mono_2Etyop_2Einteger_2Eint > $o] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29 @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29) ).
thf(307,plain,
! [A: mono_2Etyop_2Einteger_2Eint > $o] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29 @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(32,axiom,
! [A: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint,B: mono_2Etyop_2Einteger_2Eint] :
( ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( A @ B ) ) )
= ( s @ tyop_2Einteger_2Eint @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Einteger_2Eint ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29 @ A ) ) @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Einteger_2Eint) ).
thf(292,plain,
! [A: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint,B: mono_2Etyop_2Einteger_2Eint] :
( ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( A @ B ) ) )
= ( s @ tyop_2Einteger_2Eint @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Einteger_2Eint ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29 @ A ) ) @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(26,axiom,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Einteger_2Eint ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Einteger_2Eint ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Einteger_2Eint ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29) ).
thf(233,plain,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Einteger_2Eint ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Einteger_2Eint ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Einteger_2Eint ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(57,axiom,
! [A: u] :
( ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ A ) ) ) )
= ( s @ tyop_2Einteger_2Eint @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Einteger_2Eint) ).
thf(392,plain,
! [A: u] :
( ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ A ) ) ) )
= ( s @ tyop_2Einteger_2Eint @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(62,axiom,
! [A: $o > $o] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29) ).
thf(407,plain,
! [A: $o > $o] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(9,axiom,
! [A: mono_2Etyop_2Einteger_2Eint > $o,B: mono_2Etyop_2Einteger_2Eint] :
( ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( A @ B ) ) )
= ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29 @ A ) ) @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Emin_2Ebool) ).
thf(92,plain,
! [A: mono_2Etyop_2Einteger_2Eint > $o,B: mono_2Etyop_2Einteger_2Eint] :
( ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( A @ B ) ) )
= ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29 @ A ) ) @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(39,axiom,
! [A: d,B: u,C: u] :
( ( ( s @ A @ B )
= ( s @ A @ C ) )
= ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) ) @ c_2Emin_2E_3D_2E0 ) @ ( s @ A @ B ) ) ) @ ( s @ A @ C ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a) ).
thf(329,plain,
! [A: d,B: u,C: u] :
( ( ( s @ A @ B )
= ( s @ A @ C ) )
= ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) ) @ c_2Emin_2E_3D_2E0 ) @ ( s @ A @ B ) ) ) @ ( s @ A @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(23,axiom,
! [A: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o,B: mono_2Etyop_2Einteger_2Eint] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29 @ ( A @ B ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29 @ A ) ) @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29) ).
thf(224,plain,
! [A: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o,B: mono_2Etyop_2Einteger_2Eint] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29 @ ( A @ B ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29 @ A ) ) @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(55,axiom,
! [A: d,B: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_21_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) ) ) )
= ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) @ c_2Ebool_2E_21_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a) ).
thf(388,plain,
! [A: d,B: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_21_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) ) ) )
= ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) @ c_2Ebool_2E_21_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(48,axiom,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29) ).
thf(356,plain,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(34,axiom,
! [A: d,B: u] :
( ( s @ A @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ A ) @ combin_i_2E0 ) @ ( s @ A @ B ) ) )
= ( s @ A @ B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Ei__thm) ).
thf(298,plain,
! [A: d,B: u] :
( ( s @ A @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ A ) @ combin_i_2E0 ) @ ( s @ A @ B ) ) )
= ( s @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(66,axiom,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Einteger_2Eint ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Einteger_2Eint ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Einteger_2Eint ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29) ).
thf(425,plain,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Einteger_2Eint ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Einteger_2Eint ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Einteger_2Eint ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(16,axiom,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29) ).
thf(118,plain,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(31,axiom,
! [A: $o > $o > $o] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29) ).
thf(259,plain,
! [A: $o > $o > $o] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(53,axiom,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o,B: mono_2Etyop_2Enum_2Enum] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 @ ( A @ B ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 @ A ) ) @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29) ).
thf(382,plain,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > $o,B: mono_2Etyop_2Enum_2Enum] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 @ ( A @ B ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 @ A ) ) @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(41,axiom,
! [A: u] :
( ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ A ) ) ) )
= ( s @ tyop_2Emin_2Ebool @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Ebool) ).
thf(335,plain,
! [A: u] :
( ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ A ) ) ) )
= ( s @ tyop_2Emin_2Ebool @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(27,axiom,
! [A: d,B: u,C: u] :
( ( ( s @ A @ B )
= ( s @ A @ C ) )
= ( ( s @ A @ C )
= ( s @ A @ B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EEQ__SYM__EQ) ).
thf(236,plain,
! [A: d,B: u,C: u] :
( ( ( s @ A @ B )
= ( s @ A @ C ) )
= ( ( s @ A @ C )
= ( s @ A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(46,axiom,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29) ).
thf(350,plain,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(7,axiom,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum,B: mono_2Etyop_2Enum_2Enum] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 @ ( A @ B ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 @ A ) ) @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29) ).
thf(86,plain,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum,B: mono_2Etyop_2Enum_2Enum] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29 @ ( A @ B ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 @ A ) ) @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(1,conjecture,
! [A: d] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger__word_2Ei2w__0) ).
thf(2,negated_conjecture,
~ ! [A: d] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(71,plain,
~ ! [A: d] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ mono_2Ec_2Enum_2E0 ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(56,axiom,
! [A: d,B: u] :
( ( ( s @ A @ B )
= ( s @ A @ B ) )
= mono_2Ec_2Ebool_2ET ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2EREFL__CLAUSE) ).
thf(391,plain,
mono_2Ec_2Ebool_2ET,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(21,axiom,
( ( mono_2Ec_2Einteger_2Eint__neg @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) )
= ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger_2EINT__NEG__0) ).
thf(219,plain,
( ( mono_2Ec_2Einteger_2Eint__neg @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) )
= ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(64,axiom,
! [A: mono_2Etyop_2Enum_2Enum] :
~ ( mono_2Ec_2Eprim__rec_2E_3C @ A @ mono_2Ec_2Enum_2E0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Eprim__rec_2ENOT__LESS__0) ).
thf(419,plain,
! [A: mono_2Etyop_2Enum_2Enum] :
~ ( mono_2Ec_2Eprim__rec_2E_3C @ A @ mono_2Ec_2Enum_2E0 ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(25,axiom,
! [A: mono_2Etyop_2Enum_2Enum] :
( ( j_mono_2Etyop_2Enum_2Enum @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Enum_2Enum) ).
thf(230,plain,
! [A: mono_2Etyop_2Enum_2Enum] :
( ( j_mono_2Etyop_2Enum_2Enum @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(50,axiom,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29) ).
thf(362,plain,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(30,axiom,
! [A: mono_2Etyop_2Enum_2Enum,B: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Einteger_2Eint__lt @ ( mono_2Ec_2Einteger_2Eint__of__num @ A ) @ ( mono_2Ec_2Einteger_2Eint__of__num @ B ) )
= ( mono_2Ec_2Eprim__rec_2E_3C @ A @ B ) )
& ( ( mono_2Ec_2Einteger_2Eint__lt @ ( mono_2Ec_2Einteger_2Eint__neg @ ( mono_2Ec_2Einteger_2Eint__of__num @ A ) ) @ ( mono_2Ec_2Einteger_2Eint__neg @ ( mono_2Ec_2Einteger_2Eint__of__num @ B ) ) )
= ( mono_2Ec_2Eprim__rec_2E_3C @ B @ A ) )
& ( ( mono_2Ec_2Einteger_2Eint__lt @ ( mono_2Ec_2Einteger_2Eint__neg @ ( mono_2Ec_2Einteger_2Eint__of__num @ A ) ) @ ( mono_2Ec_2Einteger_2Eint__of__num @ B ) )
= ( ( A != mono_2Ec_2Enum_2E0 )
| ( B != mono_2Ec_2Enum_2E0 ) ) )
& ( ( mono_2Ec_2Einteger_2Eint__lt @ ( mono_2Ec_2Einteger_2Eint__of__num @ A ) @ ( mono_2Ec_2Einteger_2Eint__neg @ ( mono_2Ec_2Einteger_2Eint__of__num @ B ) ) )
= mono_2Ec_2Ebool_2EF ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger_2EINT__LT__CALCULATE) ).
thf(245,plain,
! [A: mono_2Etyop_2Enum_2Enum,B: mono_2Etyop_2Enum_2Enum] :
( ( ( mono_2Ec_2Einteger_2Eint__lt @ ( mono_2Ec_2Einteger_2Eint__of__num @ A ) @ ( mono_2Ec_2Einteger_2Eint__of__num @ B ) )
= ( mono_2Ec_2Eprim__rec_2E_3C @ A @ B ) )
& ( ( mono_2Ec_2Einteger_2Eint__lt @ ( mono_2Ec_2Einteger_2Eint__neg @ ( mono_2Ec_2Einteger_2Eint__of__num @ A ) ) @ ( mono_2Ec_2Einteger_2Eint__neg @ ( mono_2Ec_2Einteger_2Eint__of__num @ B ) ) )
= ( mono_2Ec_2Eprim__rec_2E_3C @ B @ A ) )
& ( ( mono_2Ec_2Einteger_2Eint__lt @ ( mono_2Ec_2Einteger_2Eint__neg @ ( mono_2Ec_2Einteger_2Eint__of__num @ A ) ) @ ( mono_2Ec_2Einteger_2Eint__of__num @ B ) )
= ( ( A != mono_2Ec_2Enum_2E0 )
| ( B != mono_2Ec_2Enum_2E0 ) ) )
& ( ( mono_2Ec_2Einteger_2Eint__lt @ ( mono_2Ec_2Einteger_2Eint__of__num @ A ) @ ( mono_2Ec_2Einteger_2Eint__neg @ ( mono_2Ec_2Einteger_2Eint__of__num @ B ) ) )
= mono_2Ec_2Ebool_2EF ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(69,axiom,
! [A: u] :
( ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( j_mono_2Etyop_2Enum_2Enum @ ( s @ tyop_2Enum_2Enum @ A ) ) ) )
= ( s @ tyop_2Enum_2Enum @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Enum_2Enum) ).
thf(434,plain,
! [A: u] :
( ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( j_mono_2Etyop_2Enum_2Enum @ ( s @ tyop_2Enum_2Enum @ A ) ) ) )
= ( s @ tyop_2Enum_2Enum @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(11,axiom,
! [A: d,B: d,C: u,D: u] :
( ( s @ A @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ B @ A ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ B @ A ) ) @ combin_k_2E0 ) @ ( s @ A @ C ) ) ) @ ( s @ B @ D ) ) )
= ( s @ A @ C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Ek__thm) ).
thf(98,plain,
! [A: d,B: d,C: u,D: u] :
( ( s @ A @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ B @ A ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ B @ A ) ) @ combin_k_2E0 ) @ ( s @ A @ C ) ) ) @ ( s @ B @ D ) ) )
= ( s @ A @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(68,axiom,
! [A: mono_2Etyop_2Einteger_2Eint] :
( ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Einteger_2Eint) ).
thf(431,plain,
! [A: mono_2Etyop_2Einteger_2Eint] :
( ( j_mono_2Etyop_2Einteger_2Eint @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(5,axiom,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Enum_2Enum ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Enum_2Enum ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29) ).
thf(80,plain,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Enum_2Enum ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Enum_2Enum ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(33,axiom,
! [A: d,B: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_3F_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) ) ) )
= ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) @ c_2Ebool_2E_3F_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a) ).
thf(295,plain,
! [A: d,B: u] :
( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_3F_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) ) ) )
= ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) @ c_2Ebool_2E_3F_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A @ tyop_2Emin_2Ebool ) @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(10,axiom,
! [A: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Enum_2Enum,B: mono_2Etyop_2Einteger_2Eint] :
( ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( A @ B ) ) )
= ( s @ tyop_2Enum_2Enum @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29 @ A ) ) @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Enum_2Enum) ).
thf(95,plain,
! [A: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Enum_2Enum,B: mono_2Etyop_2Einteger_2Eint] :
( ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( A @ B ) ) )
= ( s @ tyop_2Enum_2Enum @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Enum_2Enum ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29 @ A ) ) @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(38,axiom,
! [A: $o > $o,B: $o] :
( ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( A @ B ) ) )
= ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ A ) ) @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool) ).
thf(310,plain,
! [A: $o > $o,B: $o] :
( ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( A @ B ) ) )
= ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ A ) ) @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(42,axiom,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29) ).
thf(338,plain,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(49,axiom,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) ) @ A ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29) ).
thf(359,plain,
! [A: u] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29 @ ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) ) @ A ) ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) ) @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(36,axiom,
! [A: d,B: d,C: d,D: u,E: u,F: u] :
( ( s @ C @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ C ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A @ B ) @ ( tyop_2Emin_2Efun @ A @ C ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ B @ C ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A @ B ) @ ( tyop_2Emin_2Efun @ A @ C ) ) ) @ combin_s_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ B @ C ) ) @ D ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ A @ B ) @ E ) ) ) @ ( s @ A @ F ) ) )
= ( s @ C @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ B @ C ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ B @ C ) ) @ D ) @ ( s @ A @ F ) ) ) @ ( s @ B @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ B ) @ E ) @ ( s @ A @ F ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reserved_2Eho_2Es__thm) ).
thf(304,plain,
! [A: d,B: d,C: d,D: u,E: u,F: u] :
( ( s @ C @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ C ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A @ B ) @ ( tyop_2Emin_2Efun @ A @ C ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ B @ C ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A @ B ) @ ( tyop_2Emin_2Efun @ A @ C ) ) ) @ combin_s_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ B @ C ) ) @ D ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ A @ B ) @ E ) ) ) @ ( s @ A @ F ) ) )
= ( s @ C @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ B @ C ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ B @ C ) ) @ D ) @ ( s @ A @ F ) ) ) @ ( s @ B @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ B ) @ E ) @ ( s @ A @ F ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(60,axiom,
! [A: d,B: $o,C: u,D: u] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ C ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ D ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( tyop_2Emin_2Efun @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( tyop_2Emin_2Efun @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) ) ) ) @ c_2Ebool_2ECOND_2E0 ) @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ C ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq3_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Efcp_2Ecart_28tyop_2Emin_2Ebool_2CA_27a_29) ).
thf(401,plain,
! [A: d,B: $o,C: u,D: u] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ C ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ D ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( tyop_2Emin_2Efun @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( tyop_2Emin_2Efun @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) ) ) ) @ c_2Ebool_2ECOND_2E0 ) @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ C ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(18,axiom,
! [A: $o > $o > $o,B: $o] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ ( A @ B ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @ A ) ) @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29) ).
thf(126,plain,
! [A: $o > $o > $o,B: $o] :
( ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ ( A @ B ) ) )
= ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @ A ) ) @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(43,axiom,
! [A: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29 @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29) ).
thf(341,plain,
! [A: mono_2Etyop_2Einteger_2Eint > mono_2Etyop_2Einteger_2Eint > $o] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ tyop_2Emin_2Ebool ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29 @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(4,axiom,
mono_2Ec_2Ebool_2ET,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Ebool_2ETRUTH) ).
thf(79,plain,
mono_2Ec_2Ebool_2ET,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(70,axiom,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29) ).
thf(437,plain,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Enum_2Enum] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Enum_2Enum ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29 @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(28,axiom,
! [A: d,B: mono_2Etyop_2Einteger_2Eint] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( mono_2Ec_2Einteger_2Eint__lt @ B @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2Eword__2comp_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Einteger_2ENum @ ( mono_2Ec_2Einteger_2Eint__neg @ B ) ) ) ) ) ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Einteger_2ENum @ B ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',thm_2Einteger__word_2Ei2w__def) ).
thf(239,plain,
! [A: d,B: mono_2Etyop_2Einteger_2Eint] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( mono_2Ec_2Einteger_2Eint__lt @ B @ ( mono_2Ec_2Einteger_2Eint__of__num @ mono_2Ec_2Enum_2E0 ) ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2Eword__2comp_2E1 @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Einteger_2ENum @ ( mono_2Ec_2Einteger_2Eint__neg @ B ) ) ) ) ) ) ) ) @ ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Ewords_2En2w_2E1 @ ( s @ tyop_2Enum_2Enum @ ( i_mono_2Etyop_2Enum_2Enum @ ( mono_2Ec_2Einteger_2ENum @ B ) ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(29,axiom,
! [A: mono_2Etyop_2Enum_2Enum > $o] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29) ).
thf(242,plain,
! [A: mono_2Etyop_2Enum_2Enum > $o] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29 @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(58,axiom,
! [A: d,B: mono_2Etyop_2Einteger_2Eint] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) ) @ c_2Einteger__word_2Ei2w_2E0 ) @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq1_2Ec_2Einteger__word_2Ei2w_2E1_2Emono_2EA_27a) ).
thf(395,plain,
! [A: d,B: mono_2Etyop_2Einteger_2Eint] :
( ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( c_2Einteger__word_2Ei2w_2E1 @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) )
= ( s @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Einteger_2Eint @ ( tyop_2Efcp_2Ecart @ tyop_2Emin_2Ebool @ A ) ) @ c_2Einteger__word_2Ei2w_2E0 ) @ ( s @ tyop_2Einteger_2Eint @ ( i_mono_2Etyop_2Einteger_2Eint @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(40,axiom,
! [A: d,B: $o,C: u,D: u] :
( ( s @ A @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) @ ( s @ A @ C ) @ ( s @ A @ D ) ) )
= ( s @ A @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ A ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ A @ A ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ A @ A ) ) ) @ c_2Ebool_2ECOND_2E0 ) @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) ) ) @ ( s @ A @ C ) ) ) @ ( s @ A @ D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq3_2Ec_2Ebool_2ECOND_2E3_2Emono_2EA_27a) ).
thf(332,plain,
! [A: d,B: $o,C: u,D: u] :
( ( s @ A @ ( c_2Ebool_2ECOND_2E3 @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) @ ( s @ A @ C ) @ ( s @ A @ D ) ) )
= ( s @ A @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ A ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ A @ A ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ A @ ( tyop_2Emin_2Efun @ A @ A ) ) ) @ c_2Ebool_2ECOND_2E0 ) @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ B ) ) ) ) @ ( s @ A @ C ) ) ) @ ( s @ A @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(24,axiom,
! [A: d,B: u] :
( ( j_mono_2Etyop_2Enum_2Enum @ ( s @ tyop_2Enum_2Enum @ ( c_2Ewords_2Edimword_2E1 @ ( s @ ( tyop_2Ebool_2Eitself @ A ) @ B ) ) ) )
= ( j_mono_2Etyop_2Enum_2Enum @ ( s @ tyop_2Enum_2Enum @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Ebool_2Eitself @ A ) @ tyop_2Enum_2Enum ) @ c_2Ewords_2Edimword_2E0 ) @ ( s @ ( tyop_2Ebool_2Eitself @ A ) @ B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',arityeq1_2Ec_2Ewords_2Edimword_2E1_2Emono_2EA_27a) ).
thf(227,plain,
! [A: d,B: u] :
( ( j_mono_2Etyop_2Enum_2Enum @ ( s @ tyop_2Enum_2Enum @ ( c_2Ewords_2Edimword_2E1 @ ( s @ ( tyop_2Ebool_2Eitself @ A ) @ B ) ) ) )
= ( j_mono_2Etyop_2Enum_2Enum @ ( s @ tyop_2Enum_2Enum @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Ebool_2Eitself @ A ) @ tyop_2Enum_2Enum ) @ c_2Ewords_2Edimword_2E0 ) @ ( s @ ( tyop_2Ebool_2Eitself @ A ) @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(6,axiom,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Einteger_2Eint ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29 @ A ) ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29) ).
thf(83,plain,
! [A: mono_2Etyop_2Enum_2Enum > mono_2Etyop_2Einteger_2Eint] :
( ( j_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29 @ ( s @ ( tyop_2Emin_2Efun @ tyop_2Enum_2Enum @ tyop_2Einteger_2Eint ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29 @ A ) ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(974,plain,
$false,
inference(e,[status(thm)],[385,344,416,398,213,112,104,422,365,101,347,115,379,404,301,216,121,353,221,89,428,74,307,292,233,392,407,92,329,224,388,356,298,425,118,259,382,335,236,350,86,71,391,219,419,230,362,245,434,98,431,80,295,95,310,338,359,304,401,126,341,79,437,239,242,395,332,227,83]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP015^1 : 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.08/0.19 % Computer : n020.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 19:30:10 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 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.76 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.62/1.12 % [INFO] Parsing done (363ms).
% 2.14/1.14 % [INFO] Running in sequential loop mode.
% 2.91/1.53 % [INFO] eprover registered as external prover.
% 2.91/1.54 % [INFO] Scanning for conjecture ...
% 3.29/1.70 % [INFO] Found a conjecture (or negated_conjecture) and 85 axioms. Running axiom selection ...
% 3.54/1.81 % [INFO] Axiom selection finished. Selected 68 axioms (removed 17 axioms).
% 3.79/1.94 % [INFO] Problem is higher-order (TPTP THF).
% 3.79/1.96 % [INFO] Type checking passed.
% 3.79/1.96 % [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 ...
% 15.72/4.63 % External prover 'e' found a proof!
% 15.72/4.63 % [INFO] Killing All external provers ...
% 15.72/4.63 % Time passed: 4305ms (effective reasoning time: 3487ms)
% 15.72/4.63 % 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)>
% 15.72/4.63 % Axioms used in derivation (68): ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29, ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29, ji_2Emono_2Etyop_2Emin_2Ebool, reserved_2Equant_2E_21, monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29, ij_2Emono_2Etyop_2Einteger_2Eint, arityeq1_2Ec_2Ewords_2Edimword_2E1_2Emono_2EA_27a, thm_2Eprim__rec_2ENOT__LESS__0, monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Emin_2Ebool, ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29, ij_2Emono_2Etyop_2Emin_2Ebool, thm_2Ewords_2EWORD__NEG__0, ji_2Emono_2Etyop_2Enum_2Enum, ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29, monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum, thm_2Ebool_2EREFL__CLAUSE, ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29, ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29, ji_2Emono_2Etyop_2Einteger_2Eint, monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Einteger_2Eint, ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_29, reserved_2Equant_2E_3F, ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29, reserved_2Eho_2Ei__thm, reserved_2Eho_2Es__thm, thm_2Ebool_2EFALSITY, reserved_2Elogic_2E_3D, arityeq1_2Ec_2Ewords_2Eword__2comp_2E1_2Emono_2EA_27a, monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Einteger_2Eint, ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29_29, ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29, thm_2Ebool_2ECOND__CONG, arityeq1_2Ec_2Ewords_2En2w_2E1_2Emono_2EA_27a, ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29, thm_2Einteger_2EINT__NEG__0, ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29_29, arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a, ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29, arityeq3_2Ec_2Ebool_2ECOND_2E3_2Emono_2Etyop_2Efcp_2Ecart_28tyop_2Emin_2Ebool_2CA_27a_29, thm_2Ebool_2ETRUTH, ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29, monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Ebool, arityeq1_2Ec_2Einteger__word_2Ei2w_2E1_2Emono_2EA_27a, reserved_2Eho_2Ek__thm, arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a, monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29, ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29, thm_2Einteger_2EINT__LT__CALCULATE, arityeq3_2Ec_2Ebool_2ECOND_2E3_2Emono_2EA_27a, ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29, ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Einteger_2Eint_29, monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Enum_2Enum, reserved_2Eho_2Eeq__ext, ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Einteger_2Eint_29, monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29, ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29, ij_2Emono_2Etyop_2Enum_2Enum, arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a, thm_2Einteger__word_2Ei2w__def, thm_2Ebool_2EEQ__SYM__EQ, ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29, monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool, thm_2Einteger_2ENUM__OF__INT, monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Einteger_2Eint_20mono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Emin_2Ebool_29, thm_2Ewords_2En2w__11, thm_2Ebool_2Ebool__case__thm, ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Enum_2Enum_2Ctyop_2Emin_2Ebool_29, ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Einteger_2Eint_2Ctyop_2Enum_2Enum_29
% 15.72/4.64 % No. of inferences in proof: 140
% 15.72/4.64 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 4305 ms resp. 3487 ms w/o parsing
% 16.17/4.75 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 16.17/4.76 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------