%------------------------------------------------------------------------------
% File : DT2H2X---1.9.5
% Problem : ITP010^1 : TPTP v9.2.1. Bugfixed v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Feb 25 08:53:20 AM UTC 2026
% Result : Theorem 1.89s 1.31s
% Output : Refutation 1.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 2
% Syntax : Number of formulae : 10 ( 6 unt; 0 typ; 0 def)
% Number of atoms : 28 ( 7 equ; 0 cnn)
% Maximal formula atoms : 2 ( 2 avg)
% Number of connectives : 293 ( 29 ~; 0 |; 0 &; 260 @)
% ( 3 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 8 avg)
% Number of types : 4 ( 3 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 50 ( 48 usr; 19 con; 0-4 aty)
% Number of variables : 28 ( 0 ^; 16 !; 12 ?; 28 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
d: $tType ).
thf(type_def_7,type,
u: $tType ).
thf(type_def_8,type,
du: $tType ).
thf(func_def_0,type,
u: $tType ).
thf(func_def_1,type,
d: $tType ).
thf(func_def_2,type,
du: $tType ).
thf(func_def_3,type,
tyop_2Emin_2Ebool: d ).
thf(func_def_4,type,
tyop_2Emin_2Efun: d > d > d ).
thf(func_def_5,type,
s: d > u > du ).
thf(func_def_6,type,
app_2E2: du > du > u ).
thf(func_def_7,type,
combin_i_2E0: u ).
thf(func_def_8,type,
combin_k_2E0: u ).
thf(func_def_9,type,
combin_s_2E0: u ).
thf(func_def_10,type,
c_2Ebool_2E_21_2E0: u ).
thf(func_def_11,type,
c_2Ebool_2E_21_2E1: du > u ).
thf(func_def_12,type,
c_2Ebool_2E_2F_5C_2E0: u ).
thf(func_def_13,type,
c_2Ebool_2E_2F_5C_2E2: du > du > u ).
thf(func_def_14,type,
c_2Emin_2E_3D_2E0: u ).
thf(func_def_15,type,
c_2Emin_2E_3D_2E2: du > du > u ).
thf(func_def_16,type,
c_2Emin_2E_3D_3D_3E_2E0: u ).
thf(func_def_17,type,
c_2Emin_2E_3D_3D_3E_2E2: du > du > u ).
thf(func_def_18,type,
c_2Ebool_2E_3F_2E0: u ).
thf(func_def_19,type,
c_2Ebool_2E_3F_2E1: du > u ).
thf(func_def_20,type,
c_2Ebool_2EF_2E0: u ).
thf(func_def_21,type,
c_2Ebool_2ET_2E0: u ).
thf(func_def_22,type,
c_2Ebool_2E_5C_2F_2E0: u ).
thf(func_def_23,type,
c_2Ebool_2E_5C_2F_2E2: du > du > u ).
thf(func_def_24,type,
c_2Ecardinal_2Ecardleq_2E0: u ).
thf(func_def_25,type,
c_2Ecardinal_2Ecardleq_2E2: du > du > u ).
thf(func_def_26,type,
c_2Ebool_2E_7E_2E0: u ).
thf(func_def_27,type,
c_2Ebool_2E_7E_2E1: du > u ).
thf(func_def_28,type,
mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool: ( $o > $o ) > $o > $o ).
thf(func_def_29,type,
mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: ( $o > $o > $o ) > $o > $o > $o ).
thf(func_def_30,type,
mono_2Ec_2Ebool_2E_2F_5C: $o > $o > $o ).
thf(func_def_31,type,
mono_2Ec_2Emin_2E_3D_3D_3E: $o > $o > $o ).
thf(func_def_34,type,
mono_2Ec_2Ebool_2E_5C_2F: $o > $o > $o ).
thf(func_def_35,type,
mono_2Ec_2Ebool_2E_7E: $o > $o ).
thf(func_def_36,type,
i_mono_2Etyop_2Emin_2Ebool: $o > u ).
thf(func_def_37,type,
i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: ( $o > $o ) > u ).
thf(func_def_38,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(func_def_39,type,
j_mono_2Etyop_2Emin_2Ebool: du > $o ).
thf(func_def_40,type,
j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: du > $o > $o ).
thf(func_def_41,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(func_def_47,type,
sP0: $o > $o > $o > $o ).
thf(func_def_48,type,
sP1: $o > $o > $o > $o ).
thf(func_def_49,type,
sP2: $o > $o > $o > $o ).
thf(func_def_50,type,
sP3: $o > $o > $o > $o ).
thf(func_def_51,type,
sK4: u > d > u ).
thf(func_def_52,type,
sK5: d ).
thf(func_def_53,type,
sK6: d ).
thf(func_def_54,type,
sK7: u ).
thf(func_def_55,type,
sK8: u ).
thf(func_def_56,type,
sK9: u > u > d > d > u ).
thf(func_def_57,type,
sK10: d > u > u ).
thf(f464,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[f208]) ).
thf(f208,plain,
( ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ sK6 @ tyop_2Emin_2Ebool ) @ sK8 ) @ ( s @ ( tyop_2Emin_2Efun @ sK5 @ tyop_2Emin_2Ebool ) @ sK7 ) ) ) ) )
!= ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ sK6 @ tyop_2Emin_2Ebool ) @ sK8 ) @ ( s @ ( tyop_2Emin_2Efun @ sK5 @ tyop_2Emin_2Ebool ) @ sK7 ) ) ) ) ) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
thf(f143,plain,
( ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ sK6 @ tyop_2Emin_2Ebool ) @ sK8 ) @ ( s @ ( tyop_2Emin_2Efun @ sK5 @ tyop_2Emin_2Ebool ) @ sK7 ) ) ) ) )
!= ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ sK6 @ tyop_2Emin_2Ebool ) @ sK8 ) @ ( s @ ( tyop_2Emin_2Efun @ sK5 @ tyop_2Emin_2Ebool ) @ sK7 ) ) ) ) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK5,sK6,sK7,sK8])],[f141,f142]) ).
thf(f142,plain,
( ? [X0: d,X1: d,X2: u,X3: u] :
( ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool ) @ X2 ) ) ) ) )
!= ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool ) @ X2 ) ) ) ) ) )
=> ( ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ sK6 @ tyop_2Emin_2Ebool ) @ sK8 ) @ ( s @ ( tyop_2Emin_2Efun @ sK5 @ tyop_2Emin_2Ebool ) @ sK7 ) ) ) ) )
!= ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ sK6 @ tyop_2Emin_2Ebool ) @ sK8 ) @ ( s @ ( tyop_2Emin_2Efun @ sK5 @ tyop_2Emin_2Ebool ) @ sK7 ) ) ) ) ) ) ),
introduced(definition,[],[choice_axiom]) ).
thf(f141,plain,
? [X0: d,X1: d,X2: u,X3: u] :
( ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool ) @ X2 ) ) ) ) )
!= ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X3 ) @ ( s @ ( tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool ) @ X2 ) ) ) ) ) ),
inference(rectify,[status(thm)],[f119]) ).
thf(f119,plain,
? [X3: d,X1: d,X0: u,X2: u] :
( ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X2 ) @ ( s @ ( tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool ) @ X0 ) ) ) ) )
!= ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X2 ) @ ( s @ ( tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool ) @ X0 ) ) ) ) ) ),
inference(ennf_transformation,[status(thm)],[f84]) ).
thf(f84,plain,
~ ! [X1: d,X2: u,X0: u,X3: d] :
( ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X2 ) @ ( s @ ( tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool ) @ X0 ) ) ) ) )
= ( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X2 ) @ ( s @ ( tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool ) @ X0 ) ) ) ) ) ),
inference(fool_elimination,[status(thm)],[f83]) ).
thf(f83,plain,
~ ! [X0: u,X1: d,X2: u,X3: d] :
( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X2 ) @ ( s @ ( tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool ) @ X0 ) ) ) )
<=> ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X2 ) @ ( s @ ( tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool ) @ X0 ) ) ) ) ),
inference(rectify,[status(thm)],[f43]) ).
thf(f43,negated_conjecture,
~ ! [X17: u,X0: d,X16: u,X1: d] :
( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool ) @ X16 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X17 ) ) ) )
<=> ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool ) @ X16 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X17 ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f42]) ).
thf(f42,conjecture,
! [X17: u,X0: d,X16: u,X1: d] :
( ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool ) @ X16 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X17 ) ) ) )
<=> ~ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool ) @ X16 ) @ ( s @ ( tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool ) @ X17 ) ) ) ) ),
file('/export/starexec/sandbox/tmp/tmp.TLjRvridFZ/DTF2THF_3089.p',thm_2Ecardinal_2ECARD__NOT__LE) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : ITP010^1 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.13/0.32 % Computer : n020.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 300
% 0.13/0.32 % DateTime : Tue Feb 24 08:19:27 EST 2026
% 0.13/0.32 % CPUTime :
% 0.13/0.32 Running /export/starexec/sandbox/solver/bin/run_DT2H2X /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.24/0.45 ---- Original DTF file ---
% 0.24/0.45 thf(spec,logic,$$dhol).
% 0.24/0.45 %------------------------------------------------------------------------------
% 0.24/0.45 % File : ITP010^1 : TPTP v9.2.1. Bugfixed v7.5.0.
% 0.24/0.45 % Domain : Interactive Theorem Proving
% 0.24/0.45 % Problem : HOL4 syntactic export of thm_2Ecardinal_2ECARD__NOT__LE.p, bushy mode
% 0.24/0.45 % Version : [BG+19] axioms.
% 0.24/0.45 % English :
% 0.24/0.45
% 0.24/0.45 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall
% 0.24/0.45 % : [Gau19] Gauthier (2019), Email to Geoff Sutcliffe
% 0.24/0.45 % Source : [BG+19]
% 0.24/0.45 % Names : thm_2Ecardinal_2ECARD__NOT__LE.p [Gau19]
% 0.24/0.45 % : HL404501^1.p [TPAP]
% 0.24/0.45
% 0.24/0.45 % Status : Theorem
% 0.24/0.45 % Rating : 0.11 v9.1.0, 0.12 v9.0.0, 0.10 v8.2.0, 0.08 v8.1.0, 0.09 v7.5.0
% 0.24/0.45 % Syntax : Number of formulae : 84 ( 22 unt; 42 typ; 0 def)
% 0.24/0.45 % Number of atoms : 110 ( 27 equ; 28 cnn)
% 0.24/0.45 % Maximal formula atoms : 8 ( 2 avg)
% 0.24/0.45 % Number of connectives : 646 ( 28 ~; 14 |; 14 &; 539 @)
% 0.24/0.45 % ( 30 <=>; 21 =>; 0 <=; 0 <~>)
% 0.24/0.45 % Maximal formula depth : 17 ( 6 avg)
% 0.24/0.45 % Number of types : 4 ( 3 usr)
% 0.24/0.45 % Number of type conns : 55 ( 55 >; 0 *; 0 +; 0 <<)
% 0.24/0.45 % Number of symbols : 41 ( 39 usr; 17 con; 0-3 aty)
% 0.24/0.45 % Number of variables : 91 ( 0 ^; 90 !; 1 ?; 91 :)
% 0.24/0.45 % SPC : TH0_THM_EQU_NAR
% 0.24/0.45
% 0.24/0.45 % Comments :
% 0.24/0.45 % Bugfixes : v7.5.0 - Bugfixes in axioms and export.
% 0.24/0.45 %------------------------------------------------------------------------------
% 0.24/0.45 thf(u,type,
% 0.24/0.45 u: $tType ).
% 0.24/0.45
% 0.24/0.45 thf(d,type,
% 0.24/0.45 d: $tType ).
% 0.24/0.45
% 0.24/0.45 thf(du,type,
% 0.24/0.45 du: $tType ).
% 0.24/0.45
% 0.24/0.45 thf(tyop_2Emin_2Ebool,type,
% 0.24/0.45 tyop_2Emin_2Ebool: d ).
% 0.24/0.45
% 0.24/0.45 thf(tyop_2Emin_2Efun,type,
% 0.24/0.45 tyop_2Emin_2Efun: d > d > d ).
% 0.24/0.45
% 0.24/0.45 thf(s,type,
% 0.24/0.45 s: d > u > du ).
% 0.24/0.45
% 0.24/0.45 thf(app_2E2,type,
% 0.24/0.45 app_2E2: du > du > u ).
% 0.24/0.45
% 0.24/0.45 thf(combin_i_2E0,type,
% 0.24/0.45 combin_i_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(combin_k_2E0,type,
% 0.24/0.45 combin_k_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(combin_s_2E0,type,
% 0.24/0.45 combin_s_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ebool_2E_21_2E0,type,
% 0.24/0.45 c_2Ebool_2E_21_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ebool_2E_21_2E1,type,
% 0.24/0.45 c_2Ebool_2E_21_2E1: du > u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ebool_2E_2F_5C_2E0,type,
% 0.24/0.45 c_2Ebool_2E_2F_5C_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ebool_2E_2F_5C_2E2,type,
% 0.24/0.45 c_2Ebool_2E_2F_5C_2E2: du > du > u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Emin_2E_3D_2E0,type,
% 0.24/0.45 c_2Emin_2E_3D_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Emin_2E_3D_2E2,type,
% 0.24/0.45 c_2Emin_2E_3D_2E2: du > du > u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Emin_2E_3D_3D_3E_2E0,type,
% 0.24/0.45 c_2Emin_2E_3D_3D_3E_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Emin_2E_3D_3D_3E_2E2,type,
% 0.24/0.45 c_2Emin_2E_3D_3D_3E_2E2: du > du > u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ebool_2E_3F_2E0,type,
% 0.24/0.45 c_2Ebool_2E_3F_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ebool_2E_3F_2E1,type,
% 0.24/0.45 c_2Ebool_2E_3F_2E1: du > u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ebool_2EF_2E0,type,
% 0.24/0.45 c_2Ebool_2EF_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ebool_2ET_2E0,type,
% 0.24/0.45 c_2Ebool_2ET_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ebool_2E_5C_2F_2E0,type,
% 0.24/0.45 c_2Ebool_2E_5C_2F_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ebool_2E_5C_2F_2E2,type,
% 0.24/0.45 c_2Ebool_2E_5C_2F_2E2: du > du > u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ecardinal_2Ecardleq_2E0,type,
% 0.24/0.45 c_2Ecardinal_2Ecardleq_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ecardinal_2Ecardleq_2E2,type,
% 0.24/0.45 c_2Ecardinal_2Ecardleq_2E2: du > du > u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ebool_2E_7E_2E0,type,
% 0.24/0.45 c_2Ebool_2E_7E_2E0: u ).
% 0.24/0.45
% 0.24/0.45 thf(c_2Ebool_2E_7E_2E1,type,
% 0.24/0.45 c_2Ebool_2E_7E_2E1: du > u ).
% 0.24/0.45
% 0.24/0.45 thf(mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool,type,
% 0.24/0.45 mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool: ( $o > $o ) > $o > $o ).
% 0.24/0.45
% 0.24/0.45 thf(mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,type,
% 0.24/0.45 mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: ( $o > $o > $o ) > $o > $o > $o ).
% 0.24/0.45
% 0.24/0.45 thf(mono_2Ec_2Ebool_2E_2F_5C,type,
% 0.24/0.45 mono_2Ec_2Ebool_2E_2F_5C: $o > $o > $o ).
% 0.24/0.45
% 0.24/0.45 thf(mono_2Ec_2Emin_2E_3D_3D_3E,type,
% 0.24/0.45 mono_2Ec_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 0.24/0.45
% 0.24/0.45 thf(mono_2Ec_2Ebool_2EF,type,
% 0.24/0.45 mono_2Ec_2Ebool_2EF: $o ).
% 0.24/0.45
% 0.24/0.45 thf(mono_2Ec_2Ebool_2ET,type,
% 0.24/0.45 mono_2Ec_2Ebool_2ET: $o ).
% 0.24/0.45
% 0.24/0.45 thf(mono_2Ec_2Ebool_2E_5C_2F,type,
% 0.24/0.45 mono_2Ec_2Ebool_2E_5C_2F: $o > $o > $o ).
% 0.24/0.45
% 0.24/0.45 thf(mono_2Ec_2Ebool_2E_7E,type,
% 0.24/0.45 mono_2Ec_2Ebool_2E_7E: $o > $o ).
% 0.24/0.45
% 0.24/0.45 thf(i_mono_2Etyop_2Emin_2Ebool,type,
% 0.24/0.45 i_mono_2Etyop_2Emin_2Ebool: $o > u ).
% 0.24/0.45
% 0.24/0.45 thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,type,
% 0.24/0.45 i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: ( $o > $o ) > u ).
% 0.24/0.45
% 0.24/0.45 thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29,type,
% 0.24/0.45 i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: ( $o > $o > $o ) > u ).
% 0.24/0.45
% 0.24/0.45 thf(j_mono_2Etyop_2Emin_2Ebool,type,
% 0.24/0.45 j_mono_2Etyop_2Emin_2Ebool: du > $o ).
% 0.24/0.45
% 0.24/0.45 thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,type,
% 0.24/0.45 j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: du > $o > $o ).
% 0.24/0.45
% 0.24/0.45 thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29,type,
% 0.24/0.45 j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: du > $o > $o > $o ).
% 0.24/0.45
% 0.24/0.45 thf(reserved_2Eho_2Eeq__ext,axiom,
% 0.24/0.45 ! [A_27a: d,A_27b: d,V0f_2E0: u,V1g_2E0: u] :
% 0.24/0.45 ( ! [V2x_2E0: u] :
% 0.24/0.45 ( ( s @ A_27b @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V0f_2E0 ) @ ( s @ A_27a @ V2x_2E0 ) ) )
% 0.24/0.45 = ( s @ A_27b @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V1g_2E0 ) @ ( s @ A_27a @ V2x_2E0 ) ) ) )
% 0.24/0.45 => ( ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V0f_2E0 )
% 0.24/0.45 = ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V1g_2E0 ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(reserved_2Eho_2Ei__thm,axiom,
% 0.24/0.45 ! [A_27a: d,V0x_2E0: u] :
% 0.24/0.45 ( ( s @ A_27a @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27a ) @ combin_i_2E0 ) @ ( s @ A_27a @ V0x_2E0 ) ) )
% 0.24/0.45 = ( s @ A_27a @ V0x_2E0 ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(reserved_2Eho_2Ek__thm,axiom,
% 0.24/0.45 ! [A_27a: d,A_27b: d,V0x_2E0: u,V1y_2E0: u] :
% 0.24/0.45 ( ( s @ A_27a @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ A_27a ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ ( tyop_2Emin_2Efun @ A_27b @ A_27a ) ) @ combin_k_2E0 ) @ ( s @ A_27a @ V0x_2E0 ) ) ) @ ( s @ A_27b @ V1y_2E0 ) ) )
% 0.24/0.45 = ( s @ A_27a @ V0x_2E0 ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(reserved_2Eho_2Es__thm,axiom,
% 0.24/0.45 ! [A_27a: d,A_27b: d,A_27c: d,V0f_2E0: u,V1g_2E0: u,V2x_2E0: u] :
% 0.24/0.45 ( ( s @ A_27c @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27c ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ ( tyop_2Emin_2Efun @ A_27a @ A_27c ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ ( tyop_2Emin_2Efun @ A_27b @ A_27c ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ ( tyop_2Emin_2Efun @ A_27a @ A_27c ) ) ) @ combin_s_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ ( tyop_2Emin_2Efun @ A_27b @ A_27c ) ) @ V0f_2E0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V1g_2E0 ) ) ) @ ( s @ A_27a @ V2x_2E0 ) ) )
% 0.24/0.45 = ( s @ A_27c @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ A_27c ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ ( tyop_2Emin_2Efun @ A_27b @ A_27c ) ) @ V0f_2E0 ) @ ( s @ A_27a @ V2x_2E0 ) ) ) @ ( s @ A_27b @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V1g_2E0 ) @ ( s @ A_27a @ V2x_2E0 ) ) ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(reserved_2Elogic_2E_2F_5C,axiom,
% 0.24/0.45 ! [V0: $o,V1: $o] :
% 0.24/0.45 ( ( mono_2Ec_2Ebool_2E_2F_5C @ V0 @ V1 )
% 0.24/0.45 <=> ( V0
% 0.24/0.45 & V1 ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(reserved_2Elogic_2E_5C_2F,axiom,
% 0.24/0.45 ! [V0: $o,V1: $o] :
% 0.24/0.45 ( ( mono_2Ec_2Ebool_2E_5C_2F @ V0 @ V1 )
% 0.24/0.45 <=> ( V0
% 0.24/0.45 | V1 ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(reserved_2Elogic_2E_7E,axiom,
% 0.24/0.45 ! [V0: $o] :
% 0.24/0.45 ( ( mono_2Ec_2Ebool_2E_7E @ V0 )
% 0.24/0.45 <=> ( (~) @ V0 ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(reserved_2Elogic_2E_3D_3D_3E,axiom,
% 0.24/0.45 ! [V0: $o,V1: $o] :
% 0.24/0.45 ( ( mono_2Ec_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 0.24/0.45 <=> ( V0
% 0.24/0.45 => V1 ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(reserved_2Elogic_2E_3D,axiom,
% 0.24/0.45 ! [A_27a: d,V0_2E0: u,V1_2E0: u] :
% 0.24/0.45 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Emin_2E_3D_2E2 @ ( s @ A_27a @ V0_2E0 ) @ ( s @ A_27a @ V1_2E0 ) ) ) )
% 0.24/0.45 <=> ( ( s @ A_27a @ V0_2E0 )
% 0.24/0.45 = ( s @ A_27a @ V1_2E0 ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(reserved_2Equant_2E_21,axiom,
% 0.24/0.45 ! [A_27a: d,V0f_2E0: u] :
% 0.24/0.45 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_21_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0f_2E0 ) ) ) )
% 0.24/0.45 <=> ! [V1x_2E0: u] : ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0f_2E0 ) @ ( s @ A_27a @ V1x_2E0 ) ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(reserved_2Equant_2E_3F,axiom,
% 0.24/0.45 ! [A_27a: d,V0f_2E0: u] :
% 0.24/0.45 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_3F_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0f_2E0 ) ) ) )
% 0.24/0.45 <=> ? [V1x_2E0: u] : ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0f_2E0 ) @ ( s @ A_27a @ V1x_2E0 ) ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(ij_2Emono_2Etyop_2Emin_2Ebool,axiom,
% 0.24/0.45 ! [V0_2E0: u] :
% 0.24/0.45 ( ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ V0_2E0 ) ) ) )
% 0.24/0.45 = ( s @ tyop_2Emin_2Ebool @ V0_2E0 ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,axiom,
% 0.24/0.45 ! [V0_2E0: u] :
% 0.24/0.45 ( ( 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 ) @ V0_2E0 ) ) ) )
% 0.24/0.45 = ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ V0_2E0 ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29,axiom,
% 0.24/0.45 ! [V0_2E0: u] :
% 0.24/0.45 ( ( 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 ) ) @ V0_2E0 ) ) ) )
% 0.24/0.45 = ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) ) @ V0_2E0 ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(ji_2Emono_2Etyop_2Emin_2Ebool,axiom,
% 0.24/0.45 ! [V0: $o] :
% 0.24/0.45 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ V0 ) ) )
% 0.24/0.45 = V0 ) ).
% 0.24/0.45
% 0.24/0.45 thf(ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,axiom,
% 0.24/0.45 ! [V0: $o > $o] :
% 0.24/0.45 ( ( 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 @ V0 ) ) )
% 0.24/0.45 = V0 ) ).
% 0.24/0.45
% 0.24/0.45 thf(ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29,axiom,
% 0.24/0.45 ! [V0: $o > $o > $o] :
% 0.24/0.45 ( ( 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 @ V0 ) ) )
% 0.24/0.45 = V0 ) ).
% 0.24/0.45
% 0.24/0.45 thf(arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a,axiom,
% 0.24/0.45 ! [A_27a: d,X0_2E0: u] :
% 0.24/0.45 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_21_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X0_2E0 ) ) ) )
% 0.24/0.45 = ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) @ c_2Ebool_2E_21_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X0_2E0 ) ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a,axiom,
% 0.24/0.45 ! [A_27a: d,X0_2E0: u,X1_2E0: u] :
% 0.24/0.45 ( ( ( s @ A_27a @ X0_2E0 )
% 0.24/0.45 = ( s @ A_27a @ X1_2E0 ) )
% 0.24/0.45 <=> ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) ) @ c_2Emin_2E_3D_2E0 ) @ ( s @ A_27a @ X0_2E0 ) ) ) @ ( s @ A_27a @ X1_2E0 ) ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a,axiom,
% 0.24/0.45 ! [A_27a: d,X0_2E0: u] :
% 0.24/0.45 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_3F_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X0_2E0 ) ) ) )
% 0.24/0.45 = ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) @ c_2Ebool_2E_3F_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X0_2E0 ) ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(arityeq2_2Ec_2Ecardinal_2Ecardleq_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom,
% 0.24/0.45 ! [A_27a: d,A_27b: d,X0_2E0: u,X1_2E0: u] :
% 0.24/0.45 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X0_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ X1_2E0 ) ) ) )
% 0.24/0.45 = ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) ) @ c_2Ecardinal_2Ecardleq_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X0_2E0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ X1_2E0 ) ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(arityeq2_2Ec_2Ecardinal_2Ecardleq_2E2_2Emono_2EA_27b_20mono_2EA_27a,axiom,
% 0.24/0.45 ! [A_27a: d,A_27b: d,X0_2E0: u,X1_2E0: u] :
% 0.24/0.45 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ X0_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X1_2E0 ) ) ) )
% 0.24/0.45 = ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) ) @ c_2Ecardinal_2Ecardleq_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ X0_2E0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X1_2E0 ) ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool,axiom,
% 0.24/0.45 ! [V0: $o > $o,V1: $o] :
% 0.24/0.45 ( ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( V0 @ V1 ) ) )
% 0.24/0.45 = ( 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 @ V0 ) ) @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ V1 ) ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,axiom,
% 0.24/0.45 ! [V0: $o > $o > $o,V1: $o] :
% 0.24/0.45 ( ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ ( V0 @ V1 ) ) )
% 0.24/0.45 = ( 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 @ V0 ) ) @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ V1 ) ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool,axiom,
% 0.24/0.45 ! [V0: $o > $o,V1: $o] :
% 0.24/0.45 ( ( V0 @ V1 )
% 0.24/0.45 = ( V0 @ V1 ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,axiom,
% 0.24/0.45 ! [V0: $o > $o > $o,V1: $o] :
% 0.24/0.45 ( ( V0 @ V1 )
% 0.24/0.45 = ( V0 @ V1 ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Ebool_2ETRUTH,axiom,
% 0.24/0.45 mono_2Ec_2Ebool_2ET ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Ebool_2EFALSITY,axiom,
% 0.24/0.45 ! [V0t: $o] :
% 0.24/0.45 ( mono_2Ec_2Ebool_2EF
% 0.24/0.45 => V0t ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Ebool_2EFORALL__SIMP,axiom,
% 0.24/0.45 ! [A_27a: d,V0t: $o] :
% 0.24/0.45 ( ! [V1x_2E0: u] : V0t
% 0.24/0.45 <=> V0t ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Ebool_2EIMP__CLAUSES,axiom,
% 0.24/0.45 ! [V0t: $o] :
% 0.24/0.45 ( ( ( mono_2Ec_2Ebool_2ET
% 0.24/0.45 => V0t )
% 0.24/0.45 <=> V0t )
% 0.24/0.45 & ( ( V0t
% 0.24/0.45 => mono_2Ec_2Ebool_2ET )
% 0.24/0.45 <=> mono_2Ec_2Ebool_2ET )
% 0.24/0.45 & ( ( mono_2Ec_2Ebool_2EF
% 0.24/0.45 => V0t )
% 0.24/0.45 <=> mono_2Ec_2Ebool_2ET )
% 0.24/0.45 & ( ( V0t
% 0.24/0.45 => V0t )
% 0.24/0.45 <=> mono_2Ec_2Ebool_2ET )
% 0.24/0.45 & ( ( V0t
% 0.24/0.45 => mono_2Ec_2Ebool_2EF )
% 0.24/0.45 <=> ( (~) @ V0t ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Ebool_2ENOT__CLAUSES,axiom,
% 0.24/0.45 ( ! [V0t: $o] :
% 0.24/0.45 ( ( (~) @ ( (~) @ V0t ) )
% 0.24/0.45 <=> V0t )
% 0.24/0.45 & ( ( (~) @ mono_2Ec_2Ebool_2ET )
% 0.24/0.45 <=> mono_2Ec_2Ebool_2EF )
% 0.24/0.45 & ( ( (~) @ mono_2Ec_2Ebool_2EF )
% 0.24/0.45 <=> mono_2Ec_2Ebool_2ET ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Ebool_2EREFL__CLAUSE,axiom,
% 0.24/0.45 ! [A_27a: d,V0x_2E0: u] :
% 0.24/0.45 ( ( ( s @ A_27a @ V0x_2E0 )
% 0.24/0.45 = ( s @ A_27a @ V0x_2E0 ) )
% 0.24/0.45 <=> mono_2Ec_2Ebool_2ET ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Ebool_2EEQ__CLAUSES,axiom,
% 0.24/0.45 ! [V0t: $o] :
% 0.24/0.45 ( ( ( mono_2Ec_2Ebool_2ET = V0t )
% 0.24/0.45 <=> V0t )
% 0.24/0.45 & ( ( V0t = mono_2Ec_2Ebool_2ET )
% 0.24/0.45 <=> V0t )
% 0.24/0.45 & ( ( mono_2Ec_2Ebool_2EF = V0t )
% 0.24/0.45 <=> ( (~) @ V0t ) )
% 0.24/0.45 & ( ( V0t = mono_2Ec_2Ebool_2EF )
% 0.24/0.45 <=> ( (~) @ V0t ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Ecardinal_2ECARD__LE__TOTAL,axiom,
% 0.24/0.45 ! [A_27a: d,A_27b: d,V0s_2E0: u,V1t_2E0: u] :
% 0.24/0.45 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0s_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ V1t_2E0 ) ) ) )
% 0.24/0.45 | ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ V1t_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0s_2E0 ) ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Esat_2ENOT__NOT,axiom,
% 0.24/0.45 ! [V0t: $o] :
% 0.24/0.45 ( ( (~) @ ( (~) @ V0t ) )
% 0.24/0.45 <=> V0t ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Esat_2EAND__INV__IMP,axiom,
% 0.24/0.45 ! [V0A: $o] :
% 0.24/0.45 ( V0A
% 0.24/0.45 => ( ( (~) @ V0A )
% 0.24/0.45 => mono_2Ec_2Ebool_2EF ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Esat_2EOR__DUAL2,axiom,
% 0.24/0.45 ! [V0B: $o,V1A: $o] :
% 0.24/0.45 ( ( ( (~)
% 0.24/0.45 @ ( V1A
% 0.24/0.45 | V0B ) )
% 0.24/0.45 => mono_2Ec_2Ebool_2EF )
% 0.24/0.45 <=> ( ( V1A
% 0.24/0.45 => mono_2Ec_2Ebool_2EF )
% 0.24/0.45 => ( ( (~) @ V0B )
% 0.24/0.45 => mono_2Ec_2Ebool_2EF ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Esat_2EOR__DUAL3,axiom,
% 0.24/0.45 ! [V0B: $o,V1A: $o] :
% 0.24/0.45 ( ( ( (~)
% 0.24/0.45 @ ( ( (~) @ V1A )
% 0.24/0.45 | V0B ) )
% 0.24/0.45 => mono_2Ec_2Ebool_2EF )
% 0.24/0.45 <=> ( V1A
% 0.24/0.45 => ( ( (~) @ V0B )
% 0.24/0.45 => mono_2Ec_2Ebool_2EF ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Esat_2EAND__INV2,axiom,
% 0.24/0.45 ! [V0A: $o] :
% 0.24/0.45 ( ( ( (~) @ V0A )
% 0.24/0.45 => mono_2Ec_2Ebool_2EF )
% 0.24/0.45 => ( ( V0A
% 0.24/0.45 => mono_2Ec_2Ebool_2EF )
% 0.24/0.45 => mono_2Ec_2Ebool_2EF ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Esat_2Edc__eq,axiom,
% 0.24/0.45 ! [V0r: $o,V1q: $o,V2p: $o] :
% 0.24/0.45 ( ( V2p
% 0.24/0.45 <=> ( V1q = V0r ) )
% 0.24/0.45 <=> ( ( V2p
% 0.24/0.45 | V1q
% 0.24/0.45 | V0r )
% 0.24/0.45 & ( V2p
% 0.24/0.45 | ( (~) @ V0r )
% 0.24/0.45 | ( (~) @ V1q ) )
% 0.24/0.45 & ( V1q
% 0.24/0.45 | ( (~) @ V0r )
% 0.24/0.45 | ( (~) @ V2p ) )
% 0.24/0.45 & ( V0r
% 0.24/0.45 | ( (~) @ V1q )
% 0.24/0.45 | ( (~) @ V2p ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Esat_2Edc__neg,axiom,
% 0.24/0.45 ! [V0q: $o,V1p: $o] :
% 0.24/0.45 ( ( V1p
% 0.24/0.45 <=> ( (~) @ V0q ) )
% 0.24/0.45 <=> ( ( V1p
% 0.24/0.45 | V0q )
% 0.24/0.45 & ( ( (~) @ V0q )
% 0.24/0.45 | ( (~) @ V1p ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 thf(thm_2Ecardinal_2ECARD__NOT__LE,conjecture,
% 0.24/0.45 ! [A_27a: d,A_27b: d,V0s_2E0: u,V1t_2E0: u] :
% 0.24/0.45 ( ( (~) @ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0s_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ V1t_2E0 ) ) ) ) )
% 0.24/0.45 <=> ( (~) @ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0s_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ V1t_2E0 ) ) ) ) ) ) ).
% 0.24/0.45
% 0.24/0.45 %------------------------------------------------------------------------------
% 0.24/0.45 ------------------------
% 1.66/1.27 ---- Embedded in THF ---
% 1.66/1.27 %%% This output was generated by embedproblem, version 1.9.5 (library version 1.9).
% 1.66/1.27 %%% Generated on Tue Feb 24 08:19:28 EST 2026
% 1.66/1.27 %%% using '$$dhol' embedding, version 1.3.0.
% 1.66/1.27 %%% Logic specification used:
% 1.66/1.27 %%% thf(spec, logic, $$dhol).
% 1.66/1.27
% 1.66/1.27 % SZS output start ListOfTHF for /export/starexec/sandbox/tmp/tmp.TLjRvridFZ/DTF2DTF3089.p
% See solution above
% 1.66/1.27 ------------------------
% 1.66/1.29 ---- Cleaned THF ---
% 1.66/1.29 thf(u,type,
% 1.66/1.29 u: $tType ).
% 1.66/1.29
% 1.66/1.29 thf(d,type,
% 1.66/1.29 d: $tType ).
% 1.66/1.29
% 1.66/1.29 thf(du,type,
% 1.66/1.29 du: $tType ).
% 1.66/1.29
% 1.66/1.29 thf(tyop_2Emin_2Ebool,type,
% 1.66/1.29 tyop_2Emin_2Ebool: d ).
% 1.66/1.29
% 1.66/1.29 thf(tyop_2Emin_2Efun,type,
% 1.66/1.29 tyop_2Emin_2Efun: d > d > d ).
% 1.66/1.29
% 1.66/1.29 thf(s,type,
% 1.66/1.29 s: d > u > du ).
% 1.66/1.29
% 1.66/1.29 thf(app_2E2,type,
% 1.66/1.29 app_2E2: du > du > u ).
% 1.66/1.29
% 1.66/1.29 thf(combin_i_2E0,type,
% 1.66/1.29 combin_i_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(combin_k_2E0,type,
% 1.66/1.29 combin_k_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(combin_s_2E0,type,
% 1.66/1.29 combin_s_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ebool_2E_21_2E0,type,
% 1.66/1.29 c_2Ebool_2E_21_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ebool_2E_21_2E1,type,
% 1.66/1.29 c_2Ebool_2E_21_2E1: du > u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ebool_2E_2F_5C_2E0,type,
% 1.66/1.29 c_2Ebool_2E_2F_5C_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ebool_2E_2F_5C_2E2,type,
% 1.66/1.29 c_2Ebool_2E_2F_5C_2E2: du > du > u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Emin_2E_3D_2E0,type,
% 1.66/1.29 c_2Emin_2E_3D_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Emin_2E_3D_2E2,type,
% 1.66/1.29 c_2Emin_2E_3D_2E2: du > du > u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Emin_2E_3D_3D_3E_2E0,type,
% 1.66/1.29 c_2Emin_2E_3D_3D_3E_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Emin_2E_3D_3D_3E_2E2,type,
% 1.66/1.29 c_2Emin_2E_3D_3D_3E_2E2: du > du > u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ebool_2E_3F_2E0,type,
% 1.66/1.29 c_2Ebool_2E_3F_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ebool_2E_3F_2E1,type,
% 1.66/1.29 c_2Ebool_2E_3F_2E1: du > u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ebool_2EF_2E0,type,
% 1.66/1.29 c_2Ebool_2EF_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ebool_2ET_2E0,type,
% 1.66/1.29 c_2Ebool_2ET_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ebool_2E_5C_2F_2E0,type,
% 1.66/1.29 c_2Ebool_2E_5C_2F_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ebool_2E_5C_2F_2E2,type,
% 1.66/1.29 c_2Ebool_2E_5C_2F_2E2: du > du > u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ecardinal_2Ecardleq_2E0,type,
% 1.66/1.29 c_2Ecardinal_2Ecardleq_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ecardinal_2Ecardleq_2E2,type,
% 1.66/1.29 c_2Ecardinal_2Ecardleq_2E2: du > du > u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ebool_2E_7E_2E0,type,
% 1.66/1.29 c_2Ebool_2E_7E_2E0: u ).
% 1.66/1.29
% 1.66/1.29 thf(c_2Ebool_2E_7E_2E1,type,
% 1.66/1.29 c_2Ebool_2E_7E_2E1: du > u ).
% 1.66/1.29
% 1.66/1.29 thf(mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool,type,
% 1.66/1.29 mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool: ( $o > $o ) > $o > $o ).
% 1.66/1.29
% 1.66/1.29 thf(mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,type,
% 1.66/1.29 mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: ( $o > $o > $o ) > $o > $o > $o ).
% 1.66/1.29
% 1.66/1.29 thf(mono_2Ec_2Ebool_2E_2F_5C,type,
% 1.66/1.29 mono_2Ec_2Ebool_2E_2F_5C: $o > $o > $o ).
% 1.66/1.29
% 1.66/1.29 thf(mono_2Ec_2Emin_2E_3D_3D_3E,type,
% 1.66/1.29 mono_2Ec_2Emin_2E_3D_3D_3E: $o > $o > $o ).
% 1.66/1.29
% 1.66/1.29 thf(mono_2Ec_2Ebool_2EF,type,
% 1.66/1.29 mono_2Ec_2Ebool_2EF: $o ).
% 1.66/1.29
% 1.66/1.29 thf(mono_2Ec_2Ebool_2ET,type,
% 1.66/1.29 mono_2Ec_2Ebool_2ET: $o ).
% 1.66/1.29
% 1.66/1.29 thf(mono_2Ec_2Ebool_2E_5C_2F,type,
% 1.66/1.29 mono_2Ec_2Ebool_2E_5C_2F: $o > $o > $o ).
% 1.66/1.29
% 1.66/1.29 thf(mono_2Ec_2Ebool_2E_7E,type,
% 1.66/1.29 mono_2Ec_2Ebool_2E_7E: $o > $o ).
% 1.66/1.29
% 1.66/1.29 thf(i_mono_2Etyop_2Emin_2Ebool,type,
% 1.66/1.29 i_mono_2Etyop_2Emin_2Ebool: $o > u ).
% 1.66/1.29
% 1.66/1.29 thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,type,
% 1.66/1.29 i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: ( $o > $o ) > u ).
% 1.66/1.29
% 1.66/1.29 thf(i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29,type,
% 1.66/1.29 i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: ( $o > $o > $o ) > u ).
% 1.66/1.29
% 1.66/1.29 thf(j_mono_2Etyop_2Emin_2Ebool,type,
% 1.66/1.29 j_mono_2Etyop_2Emin_2Ebool: du > $o ).
% 1.66/1.29
% 1.66/1.29 thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,type,
% 1.66/1.29 j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: du > $o > $o ).
% 1.66/1.29
% 1.66/1.29 thf(j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29,type,
% 1.66/1.29 j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: du > $o > $o > $o ).
% 1.66/1.29
% 1.66/1.29 thf(reserved_2Eho_2Eeq__ext,axiom,
% 1.66/1.29 ! [A_27a: d,A_27b: d,V0f_2E0: u,V1g_2E0: u] :
% 1.66/1.29 ( ! [V2x_2E0: u] :
% 1.66/1.29 ( ( s @ A_27b @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V0f_2E0 ) @ ( s @ A_27a @ V2x_2E0 ) ) )
% 1.66/1.29 = ( s @ A_27b @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V1g_2E0 ) @ ( s @ A_27a @ V2x_2E0 ) ) ) )
% 1.66/1.29 => ( ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V0f_2E0 )
% 1.66/1.29 = ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V1g_2E0 ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(reserved_2Eho_2Ei__thm,axiom,
% 1.66/1.29 ! [A_27a: d,V0x_2E0: u] :
% 1.66/1.29 ( ( s @ A_27a @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27a ) @ combin_i_2E0 ) @ ( s @ A_27a @ V0x_2E0 ) ) )
% 1.66/1.29 = ( s @ A_27a @ V0x_2E0 ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(reserved_2Eho_2Ek__thm,axiom,
% 1.66/1.29 ! [A_27a: d,A_27b: d,V0x_2E0: u,V1y_2E0: u] :
% 1.66/1.29 ( ( s @ A_27a @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ A_27a ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ ( tyop_2Emin_2Efun @ A_27b @ A_27a ) ) @ combin_k_2E0 ) @ ( s @ A_27a @ V0x_2E0 ) ) ) @ ( s @ A_27b @ V1y_2E0 ) ) )
% 1.66/1.29 = ( s @ A_27a @ V0x_2E0 ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(reserved_2Eho_2Es__thm,axiom,
% 1.66/1.29 ! [A_27a: d,A_27b: d,A_27c: d,V0f_2E0: u,V1g_2E0: u,V2x_2E0: u] :
% 1.66/1.29 ( ( s @ A_27c @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27c ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ ( tyop_2Emin_2Efun @ A_27a @ A_27c ) ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ ( tyop_2Emin_2Efun @ A_27b @ A_27c ) ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ ( tyop_2Emin_2Efun @ A_27a @ A_27c ) ) ) @ combin_s_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ ( tyop_2Emin_2Efun @ A_27b @ A_27c ) ) @ V0f_2E0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V1g_2E0 ) ) ) @ ( s @ A_27a @ V2x_2E0 ) ) )
% 1.66/1.29 = ( s @ A_27c @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ A_27c ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ ( tyop_2Emin_2Efun @ A_27b @ A_27c ) ) @ V0f_2E0 ) @ ( s @ A_27a @ V2x_2E0 ) ) ) @ ( s @ A_27b @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ A_27b ) @ V1g_2E0 ) @ ( s @ A_27a @ V2x_2E0 ) ) ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(reserved_2Elogic_2E_2F_5C,axiom,
% 1.66/1.29 ! [V0: $o,V1: $o] :
% 1.66/1.29 ( ( mono_2Ec_2Ebool_2E_2F_5C @ V0 @ V1 )
% 1.66/1.29 <=> ( V0
% 1.66/1.29 & V1 ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(reserved_2Elogic_2E_5C_2F,axiom,
% 1.66/1.29 ! [V0: $o,V1: $o] :
% 1.66/1.29 ( ( mono_2Ec_2Ebool_2E_5C_2F @ V0 @ V1 )
% 1.66/1.29 <=> ( V0
% 1.66/1.29 | V1 ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(reserved_2Elogic_2E_7E,axiom,
% 1.66/1.29 ! [V0: $o] :
% 1.66/1.29 ( ( mono_2Ec_2Ebool_2E_7E @ V0 )
% 1.66/1.29 <=> ( (~) @ V0 ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(reserved_2Elogic_2E_3D_3D_3E,axiom,
% 1.66/1.29 ! [V0: $o,V1: $o] :
% 1.66/1.29 ( ( mono_2Ec_2Emin_2E_3D_3D_3E @ V0 @ V1 )
% 1.66/1.29 <=> ( V0
% 1.66/1.29 => V1 ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(reserved_2Elogic_2E_3D,axiom,
% 1.66/1.29 ! [A_27a: d,V0_2E0: u,V1_2E0: u] :
% 1.66/1.29 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Emin_2E_3D_2E2 @ ( s @ A_27a @ V0_2E0 ) @ ( s @ A_27a @ V1_2E0 ) ) ) )
% 1.66/1.29 <=> ( ( s @ A_27a @ V0_2E0 )
% 1.66/1.29 = ( s @ A_27a @ V1_2E0 ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(reserved_2Equant_2E_21,axiom,
% 1.66/1.29 ! [A_27a: d,V0f_2E0: u] :
% 1.66/1.29 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_21_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0f_2E0 ) ) ) )
% 1.66/1.29 <=> ! [V1x_2E0: u] : ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0f_2E0 ) @ ( s @ A_27a @ V1x_2E0 ) ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(reserved_2Equant_2E_3F,axiom,
% 1.66/1.29 ! [A_27a: d,V0f_2E0: u] :
% 1.66/1.29 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_3F_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0f_2E0 ) ) ) )
% 1.66/1.29 <=> ? [V1x_2E0: u] : ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0f_2E0 ) @ ( s @ A_27a @ V1x_2E0 ) ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(ij_2Emono_2Etyop_2Emin_2Ebool,axiom,
% 1.66/1.29 ! [V0_2E0: u] :
% 1.66/1.29 ( ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ V0_2E0 ) ) ) )
% 1.66/1.29 = ( s @ tyop_2Emin_2Ebool @ V0_2E0 ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,axiom,
% 1.66/1.29 ! [V0_2E0: u] :
% 1.66/1.29 ( ( 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 ) @ V0_2E0 ) ) ) )
% 1.66/1.29 = ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ V0_2E0 ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(ij_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29,axiom,
% 1.66/1.29 ! [V0_2E0: u] :
% 1.66/1.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 @ ( 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 ) ) @ V0_2E0 ) ) ) )
% 1.66/1.29 = ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) ) @ V0_2E0 ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(ji_2Emono_2Etyop_2Emin_2Ebool,axiom,
% 1.66/1.29 ! [V0: $o] :
% 1.66/1.29 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ V0 ) ) )
% 1.66/1.29 = V0 ) ).
% 1.66/1.29
% 1.66/1.29 thf(ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,axiom,
% 1.66/1.29 ! [V0: $o > $o] :
% 1.66/1.29 ( ( 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 @ V0 ) ) )
% 1.66/1.29 = V0 ) ).
% 1.66/1.29
% 1.66/1.29 thf(ji_2Emono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29,axiom,
% 1.66/1.29 ! [V0: $o > $o > $o] :
% 1.66/1.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 ) ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29 @ V0 ) ) )
% 1.66/1.29 = V0 ) ).
% 1.66/1.29
% 1.66/1.29 thf(arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a,axiom,
% 1.66/1.29 ! [A_27a: d,X0_2E0: u] :
% 1.66/1.29 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_21_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X0_2E0 ) ) ) )
% 1.66/1.29 = ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) @ c_2Ebool_2E_21_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X0_2E0 ) ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a,axiom,
% 1.66/1.29 ! [A_27a: d,X0_2E0: u,X1_2E0: u] :
% 1.66/1.29 ( ( ( s @ A_27a @ X0_2E0 )
% 1.66/1.29 = ( s @ A_27a @ X1_2E0 ) )
% 1.66/1.29 <=> ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) ) @ c_2Emin_2E_3D_2E0 ) @ ( s @ A_27a @ X0_2E0 ) ) ) @ ( s @ A_27a @ X1_2E0 ) ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a,axiom,
% 1.66/1.29 ! [A_27a: d,X0_2E0: u] :
% 1.66/1.29 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ebool_2E_3F_2E1 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X0_2E0 ) ) ) )
% 1.66/1.29 = ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) @ c_2Ebool_2E_3F_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X0_2E0 ) ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(arityeq2_2Ec_2Ecardinal_2Ecardleq_2E2_2Emono_2EA_27a_20mono_2EA_27b,axiom,
% 1.66/1.29 ! [A_27a: d,A_27b: d,X0_2E0: u,X1_2E0: u] :
% 1.66/1.29 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X0_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ X1_2E0 ) ) ) )
% 1.66/1.29 = ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) ) @ c_2Ecardinal_2Ecardleq_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X0_2E0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ X1_2E0 ) ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(arityeq2_2Ec_2Ecardinal_2Ecardleq_2E2_2Emono_2EA_27b_20mono_2EA_27a,axiom,
% 1.66/1.29 ! [A_27a: d,A_27b: d,X0_2E0: u,X1_2E0: u] :
% 1.66/1.29 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ X0_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X1_2E0 ) ) ) )
% 1.66/1.29 = ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) @ ( app_2E2 @ ( s @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ ( tyop_2Emin_2Efun @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ tyop_2Emin_2Ebool ) ) @ c_2Ecardinal_2Ecardleq_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ X0_2E0 ) ) ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ X1_2E0 ) ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool,axiom,
% 1.66/1.29 ! [V0: $o > $o,V1: $o] :
% 1.66/1.29 ( ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ ( V0 @ V1 ) ) )
% 1.66/1.29 = ( 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 @ V0 ) ) @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ V1 ) ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(monoeq_2Emono_2Eapp_2E2_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,axiom,
% 1.66/1.29 ! [V0: $o > $o > $o,V1: $o] :
% 1.66/1.29 ( ( s @ ( tyop_2Emin_2Efun @ tyop_2Emin_2Ebool @ tyop_2Emin_2Ebool ) @ ( i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29 @ ( V0 @ V1 ) ) )
% 1.66/1.29 = ( 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 @ V0 ) ) @ ( s @ tyop_2Emin_2Ebool @ ( i_mono_2Etyop_2Emin_2Ebool @ V1 ) ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool,axiom,
% 1.66/1.29 ! [V0: $o > $o,V1: $o] :
% 1.66/1.29 ( ( V0 @ V1 )
% 1.66/1.29 = ( V0 @ V1 ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(monoapp_2Emono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29,axiom,
% 1.66/1.29 ! [V0: $o > $o > $o,V1: $o] :
% 1.66/1.29 ( ( V0 @ V1 )
% 1.66/1.29 = ( V0 @ V1 ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Ebool_2ETRUTH,axiom,
% 1.66/1.29 mono_2Ec_2Ebool_2ET ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Ebool_2EFALSITY,axiom,
% 1.66/1.29 ! [V0t: $o] :
% 1.66/1.29 ( mono_2Ec_2Ebool_2EF
% 1.66/1.29 => V0t ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Ebool_2EFORALL__SIMP,axiom,
% 1.66/1.29 ! [A_27a: d,V0t: $o] :
% 1.66/1.29 ( ! [V1x_2E0: u] : V0t
% 1.66/1.29 <=> V0t ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Ebool_2EIMP__CLAUSES,axiom,
% 1.66/1.29 ! [V0t: $o] :
% 1.66/1.29 ( ( ( mono_2Ec_2Ebool_2ET
% 1.66/1.29 => V0t )
% 1.66/1.29 <=> V0t )
% 1.66/1.29 & ( ( V0t
% 1.66/1.29 => mono_2Ec_2Ebool_2ET )
% 1.66/1.29 <=> mono_2Ec_2Ebool_2ET )
% 1.66/1.29 & ( ( mono_2Ec_2Ebool_2EF
% 1.66/1.29 => V0t )
% 1.66/1.29 <=> mono_2Ec_2Ebool_2ET )
% 1.66/1.29 & ( ( V0t
% 1.66/1.29 => V0t )
% 1.66/1.29 <=> mono_2Ec_2Ebool_2ET )
% 1.66/1.29 & ( ( V0t
% 1.66/1.29 => mono_2Ec_2Ebool_2EF )
% 1.66/1.29 <=> ( (~) @ V0t ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Ebool_2ENOT__CLAUSES,axiom,
% 1.66/1.29 ( ! [V0t: $o] :
% 1.66/1.29 ( ( (~) @ ( (~) @ V0t ) )
% 1.66/1.29 <=> V0t )
% 1.66/1.29 & ( ( (~) @ mono_2Ec_2Ebool_2ET )
% 1.66/1.29 <=> mono_2Ec_2Ebool_2EF )
% 1.66/1.29 & ( ( (~) @ mono_2Ec_2Ebool_2EF )
% 1.66/1.29 <=> mono_2Ec_2Ebool_2ET ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Ebool_2EREFL__CLAUSE,axiom,
% 1.66/1.29 ! [A_27a: d,V0x_2E0: u] :
% 1.66/1.29 ( ( ( s @ A_27a @ V0x_2E0 )
% 1.66/1.29 = ( s @ A_27a @ V0x_2E0 ) )
% 1.66/1.29 <=> mono_2Ec_2Ebool_2ET ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Ebool_2EEQ__CLAUSES,axiom,
% 1.66/1.29 ! [V0t: $o] :
% 1.66/1.29 ( ( ( mono_2Ec_2Ebool_2ET = V0t )
% 1.66/1.29 <=> V0t )
% 1.66/1.29 & ( ( V0t = mono_2Ec_2Ebool_2ET )
% 1.66/1.29 <=> V0t )
% 1.66/1.29 & ( ( mono_2Ec_2Ebool_2EF = V0t )
% 1.66/1.29 <=> ( (~) @ V0t ) )
% 1.66/1.29 & ( ( V0t = mono_2Ec_2Ebool_2EF )
% 1.66/1.29 <=> ( (~) @ V0t ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Ecardinal_2ECARD__LE__TOTAL,axiom,
% 1.66/1.29 ! [A_27a: d,A_27b: d,V0s_2E0: u,V1t_2E0: u] :
% 1.66/1.29 ( ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0s_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ V1t_2E0 ) ) ) )
% 1.66/1.29 | ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ V1t_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0s_2E0 ) ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Esat_2ENOT__NOT,axiom,
% 1.66/1.29 ! [V0t: $o] :
% 1.66/1.29 ( ( (~) @ ( (~) @ V0t ) )
% 1.66/1.29 <=> V0t ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Esat_2EAND__INV__IMP,axiom,
% 1.66/1.29 ! [V0A: $o] :
% 1.66/1.29 ( V0A
% 1.66/1.29 => ( ( (~) @ V0A )
% 1.66/1.29 => mono_2Ec_2Ebool_2EF ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Esat_2EOR__DUAL2,axiom,
% 1.66/1.29 ! [V0B: $o,V1A: $o] :
% 1.66/1.29 ( ( ( (~)
% 1.66/1.29 @ ( V1A
% 1.66/1.29 | V0B ) )
% 1.66/1.29 => mono_2Ec_2Ebool_2EF )
% 1.66/1.29 <=> ( ( V1A
% 1.66/1.29 => mono_2Ec_2Ebool_2EF )
% 1.66/1.29 => ( ( (~) @ V0B )
% 1.66/1.29 => mono_2Ec_2Ebool_2EF ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Esat_2EOR__DUAL3,axiom,
% 1.66/1.29 ! [V0B: $o,V1A: $o] :
% 1.66/1.29 ( ( ( (~)
% 1.66/1.29 @ ( ( (~) @ V1A )
% 1.66/1.29 | V0B ) )
% 1.66/1.29 => mono_2Ec_2Ebool_2EF )
% 1.66/1.29 <=> ( V1A
% 1.66/1.29 => ( ( (~) @ V0B )
% 1.66/1.29 => mono_2Ec_2Ebool_2EF ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Esat_2EAND__INV2,axiom,
% 1.66/1.29 ! [V0A: $o] :
% 1.66/1.29 ( ( ( (~) @ V0A )
% 1.66/1.29 => mono_2Ec_2Ebool_2EF )
% 1.66/1.29 => ( ( V0A
% 1.66/1.29 => mono_2Ec_2Ebool_2EF )
% 1.66/1.29 => mono_2Ec_2Ebool_2EF ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Esat_2Edc__eq,axiom,
% 1.66/1.29 ! [V0r: $o,V1q: $o,V2p: $o] :
% 1.66/1.29 ( ( V2p
% 1.66/1.29 <=> ( V1q = V0r ) )
% 1.66/1.29 <=> ( ( V2p
% 1.66/1.29 | V1q
% 1.66/1.29 | V0r )
% 1.66/1.29 & ( V2p
% 1.66/1.29 | ( (~) @ V0r )
% 1.66/1.29 | ( (~) @ V1q ) )
% 1.66/1.29 & ( V1q
% 1.66/1.29 | ( (~) @ V0r )
% 1.66/1.29 | ( (~) @ V2p ) )
% 1.66/1.29 & ( V0r
% 1.66/1.29 | ( (~) @ V1q )
% 1.66/1.29 | ( (~) @ V2p ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Esat_2Edc__neg,axiom,
% 1.66/1.29 ! [V0q: $o,V1p: $o] :
% 1.66/1.29 ( ( V1p
% 1.66/1.29 <=> ( (~) @ V0q ) )
% 1.66/1.29 <=> ( ( V1p
% 1.66/1.29 | V0q )
% 1.66/1.29 & ( ( (~) @ V0q )
% 1.66/1.29 | ( (~) @ V1p ) ) ) ) ).
% 1.66/1.29
% 1.66/1.29 thf(thm_2Ecardinal_2ECARD__NOT__LE,conjecture,
% 1.66/1.29 ! [A_27a: d,A_27b: d,V0s_2E0: u,V1t_2E0: u] :
% 1.66/1.29 ( ( (~) @ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0s_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ V1t_2E0 ) ) ) ) )
% 1.66/1.29 <=> ( (~) @ ( j_mono_2Etyop_2Emin_2Ebool @ ( s @ tyop_2Emin_2Ebool @ ( c_2Ecardinal_2Ecardleq_2E2 @ ( s @ ( tyop_2Emin_2Efun @ A_27a @ tyop_2Emin_2Ebool ) @ V0s_2E0 ) @ ( s @ ( tyop_2Emin_2Efun @ A_27b @ tyop_2Emin_2Ebool ) @ V1t_2E0 ) ) ) ) ) ) ).
% 1.66/1.29 ------------------------
% 1.89/1.30 % (3188)lrs+1002_1:8_bd=off:fd=off:hud=10:tnu=1:i=183:si=on:rtra=on_0 on DTF2THF_3089 for (2999ds/183Mi)
% 1.89/1.31 % (3188)First to succeed.
% 1.89/1.31 % (3188)Refutation found. Thanks to Tanya!
% 1.89/1.31 % SZS status Theorem for DTF2THF_3089
% 1.89/1.31 % SZS output start Proof for DTF2THF_3089
% 1.89/1.31 thf(type_def_5, type, d: $tType).
% 1.89/1.31 thf(type_def_7, type, u: $tType).
% 1.89/1.31 thf(type_def_8, type, du: $tType).
% 1.89/1.31 thf(func_def_0, type, u: $tType).
% 1.89/1.31 thf(func_def_1, type, d: $tType).
% 1.89/1.31 thf(func_def_2, type, du: $tType).
% 1.89/1.31 thf(func_def_3, type, tyop_2Emin_2Ebool: d).
% 1.89/1.31 thf(func_def_4, type, tyop_2Emin_2Efun: d > d > d).
% 1.89/1.31 thf(func_def_5, type, s: d > u > du).
% 1.89/1.31 thf(func_def_6, type, app_2E2: du > du > u).
% 1.89/1.31 thf(func_def_7, type, combin_i_2E0: u).
% 1.89/1.31 thf(func_def_8, type, combin_k_2E0: u).
% 1.89/1.31 thf(func_def_9, type, combin_s_2E0: u).
% 1.89/1.31 thf(func_def_10, type, c_2Ebool_2E_21_2E0: u).
% 1.89/1.31 thf(func_def_11, type, c_2Ebool_2E_21_2E1: du > u).
% 1.89/1.31 thf(func_def_12, type, c_2Ebool_2E_2F_5C_2E0: u).
% 1.89/1.31 thf(func_def_13, type, c_2Ebool_2E_2F_5C_2E2: du > du > u).
% 1.89/1.31 thf(func_def_14, type, c_2Emin_2E_3D_2E0: u).
% 1.89/1.31 thf(func_def_15, type, c_2Emin_2E_3D_2E2: du > du > u).
% 1.89/1.31 thf(func_def_16, type, c_2Emin_2E_3D_3D_3E_2E0: u).
% 1.89/1.31 thf(func_def_17, type, c_2Emin_2E_3D_3D_3E_2E2: du > du > u).
% 1.89/1.31 thf(func_def_18, type, c_2Ebool_2E_3F_2E0: u).
% 1.89/1.31 thf(func_def_19, type, c_2Ebool_2E_3F_2E1: du > u).
% 1.89/1.31 thf(func_def_20, type, c_2Ebool_2EF_2E0: u).
% 1.89/1.31 thf(func_def_21, type, c_2Ebool_2ET_2E0: u).
% 1.89/1.31 thf(func_def_22, type, c_2Ebool_2E_5C_2F_2E0: u).
% 1.89/1.31 thf(func_def_23, type, c_2Ebool_2E_5C_2F_2E2: du > du > u).
% 1.89/1.31 thf(func_def_24, type, c_2Ecardinal_2Ecardleq_2E0: u).
% 1.89/1.31 thf(func_def_25, type, c_2Ecardinal_2Ecardleq_2E2: du > du > u).
% 1.89/1.31 thf(func_def_26, type, c_2Ebool_2E_7E_2E0: u).
% 1.89/1.31 thf(func_def_27, type, c_2Ebool_2E_7E_2E1: du > u).
% 1.89/1.31 thf(func_def_28, type, mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Ebool: ($o > $o) > $o > $o).
% 1.89/1.31 thf(func_def_29, type, mono_2Eapp_2Emono_2Etyop_2Emin_2Ebool_20mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: ($o > $o > $o) > $o > $o > $o).
% 1.89/1.31 thf(func_def_30, type, mono_2Ec_2Ebool_2E_2F_5C: $o > $o > $o).
% 1.89/1.31 thf(func_def_31, type, mono_2Ec_2Emin_2E_3D_3D_3E: $o > $o > $o).
% 1.89/1.31 thf(func_def_34, type, mono_2Ec_2Ebool_2E_5C_2F: $o > $o > $o).
% 1.89/1.31 thf(func_def_35, type, mono_2Ec_2Ebool_2E_7E: $o > $o).
% 1.89/1.31 thf(func_def_36, type, i_mono_2Etyop_2Emin_2Ebool: $o > u).
% 1.89/1.31 thf(func_def_37, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: ($o > $o) > u).
% 1.89/1.31 thf(func_def_38, type, i_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: ($o > $o > $o) > u).
% 1.89/1.31 thf(func_def_39, type, j_mono_2Etyop_2Emin_2Ebool: du > $o).
% 1.89/1.31 thf(func_def_40, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29: du > $o > $o).
% 1.89/1.31 thf(func_def_41, type, j_mono_2Etyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Efun_28tyop_2Emin_2Ebool_2Ctyop_2Emin_2Ebool_29_29: du > $o > $o > $o).
% 1.89/1.31 thf(func_def_47, type, sP0: $o > $o > $o > $o).
% 1.89/1.31 thf(func_def_48, type, sP1: $o > $o > $o > $o).
% 1.89/1.31 thf(func_def_49, type, sP2: $o > $o > $o > $o).
% 1.89/1.31 thf(func_def_50, type, sP3: $o > $o > $o > $o).
% 1.89/1.31 thf(func_def_51, type, sK4: u > d > u).
% 1.89/1.31 thf(func_def_52, type, sK5: d).
% 1.89/1.31 thf(func_def_53, type, sK6: d).
% 1.89/1.31 thf(func_def_54, type, sK7: u).
% 1.89/1.31 thf(func_def_55, type, sK8: u).
% 1.89/1.31 thf(func_def_56, type, sK9: u > u > d > d > u).
% 1.89/1.31 thf(func_def_57, type, sK10: d > u > u).
% 1.89/1.31 thf(f464,plain,(
% 1.89/1.31 $false),
% 1.89/1.31 inference(trivial_inequality_removal,[status(thm)],[f208])).
% 1.89/1.31 thf(f208,plain,(
% 1.89/1.31 ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ sK6 @ tyop_2Emin_2Ebool) @ sK8) @ (s @ (tyop_2Emin_2Efun @ sK5 @ tyop_2Emin_2Ebool) @ sK7))))) != (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ sK6 @ tyop_2Emin_2Ebool) @ sK8) @ (s @ (tyop_2Emin_2Efun @ sK5 @ tyop_2Emin_2Ebool) @ sK7))))))),
% 1.89/1.31 inference(cnf_transformation,[status(thm)],[f143])).
% 1.89/1.31 thf(f143,plain,(
% 1.89/1.31 ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ sK6 @ tyop_2Emin_2Ebool) @ sK8) @ (s @ (tyop_2Emin_2Efun @ sK5 @ tyop_2Emin_2Ebool) @ sK7))))) != (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ sK6 @ tyop_2Emin_2Ebool) @ sK8) @ (s @ (tyop_2Emin_2Efun @ sK5 @ tyop_2Emin_2Ebool) @ sK7))))))),
% 1.89/1.31 inference(skolemisation,[status(esa),new_symbols(skolem,[sK5,sK6,sK7,sK8])],[f141,f142])).
% 1.89/1.31 thf(f142,plain,(
% 1.89/1.31 ? [X0 : d,X1 : d,X2 : u,X3 : u] : ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X2))))) != (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X2)))))) => ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ sK6 @ tyop_2Emin_2Ebool) @ sK8) @ (s @ (tyop_2Emin_2Efun @ sK5 @ tyop_2Emin_2Ebool) @ sK7))))) != (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ sK6 @ tyop_2Emin_2Ebool) @ sK8) @ (s @ (tyop_2Emin_2Efun @ sK5 @ tyop_2Emin_2Ebool) @ sK7))))))),
% 1.89/1.31 introduced(definition,[],[choice_axiom])).
% 1.89/1.31 thf(f141,plain,(
% 1.89/1.31 ? [X0 : d,X1 : d,X2 : u,X3 : u] : ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X2))))) != (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X3) @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X2))))))),
% 1.89/1.31 inference(rectify,[status(thm)],[f119])).
% 1.89/1.31 thf(f119,plain,(
% 1.89/1.31 ? [X3 : d,X1 : d,X0 : u,X2 : u] : ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X2) @ (s @ (tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool) @ X0))))) != (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X2) @ (s @ (tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool) @ X0))))))),
% 1.89/1.31 inference(ennf_transformation,[status(thm)],[f84])).
% 1.89/1.31 thf(f84,plain,(
% 1.89/1.31 ~! [X1 : d,X2 : u,X0 : u,X3 : d] : ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X2) @ (s @ (tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool) @ X0))))) = (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X2) @ (s @ (tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool) @ X0))))))),
% 1.89/1.31 inference(fool_elimination,[status(thm)],[f83])).
% 1.89/1.31 thf(f83,plain,(
% 1.89/1.31 ~! [X0 : u,X1 : d,X2 : u,X3 : d] : ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X2) @ (s @ (tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool) @ X0))))) <=> (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X2) @ (s @ (tyop_2Emin_2Efun @ X3 @ tyop_2Emin_2Ebool) @ X0))))))),
% 1.89/1.31 inference(rectify,[status(thm)],[f43])).
% 1.89/1.31 thf(f43,negated_conjecture,(
% 1.89/1.31 ~! [X17 : u,X0 : d,X16 : u,X1 : d] : ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X16) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X17))))) <=> (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X16) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X17))))))),
% 1.89/1.31 inference(negated_conjecture,[status(cth)],[f42])).
% 1.89/1.31 thf(f42,conjecture,(
% 1.89/1.31 ! [X17 : u,X0 : d,X16 : u,X1 : d] : ((~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X16) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X17))))) <=> (~ (j_mono_2Etyop_2Emin_2Ebool @ (s @ tyop_2Emin_2Ebool @ (c_2Ecardinal_2Ecardleq_2E2 @ (s @ (tyop_2Emin_2Efun @ X0 @ tyop_2Emin_2Ebool) @ X16) @ (s @ (tyop_2Emin_2Efun @ X1 @ tyop_2Emin_2Ebool) @ X17))))))),
% 1.89/1.31 file('/export/starexec/sandbox/tmp/tmp.TLjRvridFZ/DTF2THF_3089.p',thm_2Ecardinal_2ECARD__NOT__LE)).
% 1.89/1.31 % SZS output end Proof for DTF2THF_3089
% 1.89/1.31 % (3188)------------------------------
% 1.89/1.31 % (3188)Version: Vampire 4.8 (commit 7b44b1c2f on 2025-07-15 09:50:17 +0100)
% 1.89/1.31 % (3188)Termination reason: Refutation
% 1.89/1.31
% 1.89/1.31 % (3188)Memory used [KB]: 5756
% 1.89/1.31 % (3188)Time elapsed: 0.008 s
% 1.89/1.31 % (3188)Instructions burned: 20 (million)
% 1.89/1.31 % (3188)------------------------------
% 1.89/1.31 % (3188)------------------------------
% 1.89/1.31 % (3187)Success in time 0.02 s
%------------------------------------------------------------------------------