Vampire-SAT---5.0.1.SAT-FMo.s

%------------------------------------------------------------------------------
% File     : Vampire-SAT---5.0.1
% Problem  : ITP303_10 : TPTP v9.3.1. Released v8.2.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT

% Computer : n014.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Sep 29 11:39:18 AM UTC 2026

% Result   : Satisfiable 2.01s 0.92s
% Output   : FiniteModel 2.01s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
tff('declare_$i1',type,
    'fmb_$i_1': $i ).

tff('finite_domain_$i',axiom,
    ! [X: $i] : ( X = 'fmb_$i_1' ) ).

tff('declare_B_ZF_fun_set$',type,
    'B_ZF_fun_set$': $tType ).

tff('declare_B_ZF_fun_set$1',type,
    'fmb_B_ZF_fun_set$_1': 'B_ZF_fun_set$' ).

tff('finite_domain_B_ZF_fun_set$',axiom,
    ! [X: 'B_ZF_fun_set$'] : ( X = 'fmb_B_ZF_fun_set$_1' ) ).

tff('declare_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$',type,
    'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$': $tType ).

tff('declare_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$1',type,
    'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ).

tff('finite_domain_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$',axiom,
    ! [X: 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'] : ( X = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1' ) ).

tff('declare_Unit_set$',type,
    'Unit_set$': $tType ).

tff('declare_Unit_set$1',type,
    'fmb_Unit_set$_1': 'Unit_set$' ).

tff('finite_domain_Unit_set$',axiom,
    ! [X: 'Unit_set$'] : ( X = 'fmb_Unit_set$_1' ) ).

tff('declare_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$',type,
    'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$': $tType ).

tff('declare_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$1',type,
    'fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$_1': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' ).

tff('finite_domain_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$',axiom,
    ! [X: 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'] : ( X = 'fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$_1' ) ).

tff('declare_B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$',type,
    'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$': $tType ).

tff('declare_B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$1',type,
    'fmb_B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1': 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' ).

tff('finite_domain_B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$',axiom,
    ! [X: 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'] : ( X = 'fmb_B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1' ) ).

tff('declare_ZF_set$',type,
    'ZF_set$': $tType ).

tff('declare_ZF_set$1',type,
    'fmb_ZF_set$_1': 'ZF_set$' ).

tff('finite_domain_ZF_set$',axiom,
    ! [X: 'ZF_set$'] : ( X = 'fmb_ZF_set$_1' ) ).

tff('declare_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$',type,
    'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$': $tType ).

tff('declare_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$1',type,
    'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('finite_domain_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$',axiom,
    ! [X: 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'] : ( X = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ) ).

tff('declare_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$',type,
    'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$': $tType ).

tff('declare_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$1',type,
    'fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' ).

tff('finite_domain_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$',axiom,
    ! [X: 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'] : ( X = 'fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1' ) ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',type,
    'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$': $tType ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$1',type,
    'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('finite_domain_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$',axiom,
    ! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'] : ( X = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ) ).

tff('declare_Unit_unit_fun$',type,
    'Unit_unit_fun$': $tType ).

tff('declare_Unit_unit_fun$1',type,
    'fmb_Unit_unit_fun$_1': 'Unit_unit_fun$' ).

tff('finite_domain_Unit_unit_fun$',axiom,
    ! [X: 'Unit_unit_fun$'] : ( X = 'fmb_Unit_unit_fun$_1' ) ).

tff('declare_A_b_b_c_LSCategory_ext_Category_ext$',type,
    'A_b_b_c_LSCategory_ext_Category_ext$': $tType ).

tff('declare_A_b_b_c_LSCategory_ext_Category_ext$1',type,
    'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1': 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('finite_domain_A_b_b_c_LSCategory_ext_Category_ext$',axiom,
    ! [X: 'A_b_b_c_LSCategory_ext_Category_ext$'] : ( X = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ) ).

tff('declare_ZF_ZF_prod_set$',type,
    'ZF_ZF_prod_set$': $tType ).

tff('declare_ZF_ZF_prod_set$1',type,
    'fmb_ZF_ZF_prod_set$_1': 'ZF_ZF_prod_set$' ).

tff('finite_domain_ZF_ZF_prod_set$',axiom,
    ! [X: 'ZF_ZF_prod_set$'] : ( X = 'fmb_ZF_ZF_prod_set$_1' ) ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$',type,
    'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$': $tType ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$1',type,
    'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$_1': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$' ).

tff('finite_domain_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$',axiom,
    ! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$'] : ( X = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$_1' ) ).

tff('declare_ZF_set_set$',type,
    'ZF_set_set$': $tType ).

tff('declare_ZF_set_set$1',type,
    'fmb_ZF_set_set$_1': 'ZF_set_set$' ).

tff('finite_domain_ZF_set_set$',axiom,
    ! [X: 'ZF_set_set$'] : ( X = 'fmb_ZF_set_set$_1' ) ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$',type,
    'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$': $tType ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$1',type,
    'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' ).

tff('finite_domain_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$',axiom,
    ! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'] : ( X = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1' ) ).

tff('declare_ZF_set_ZF_set_fun$',type,
    'ZF_set_ZF_set_fun$': $tType ).

tff('declare_ZF_set_ZF_set_fun$1',type,
    'fmb_ZF_set_ZF_set_fun$_1': 'ZF_set_ZF_set_fun$' ).

tff('finite_domain_ZF_set_ZF_set_fun$',axiom,
    ! [X: 'ZF_set_ZF_set_fun$'] : ( X = 'fmb_ZF_set_ZF_set_fun$_1' ) ).

tff('declare_A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$',type,
    'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$': $tType ).

tff('declare_A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$1',type,
    'fmb_A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$_1': 'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$' ).

tff('finite_domain_A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$',axiom,
    ! [X: 'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$'] : ( X = 'fmb_A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$_1' ) ).

tff('declare_ZF_ZF_set_fun$',type,
    'ZF_ZF_set_fun$': $tType ).

tff('declare_ZF_ZF_set_fun$1',type,
    'fmb_ZF_ZF_set_fun$_1': 'ZF_ZF_set_fun$' ).

tff('finite_domain_ZF_ZF_set_fun$',axiom,
    ! [X: 'ZF_ZF_set_fun$'] : ( X = 'fmb_ZF_ZF_set_fun$_1' ) ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$',type,
    'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$': $tType ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$1',type,
    'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('finite_domain_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$',axiom,
    ! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'] : ( X = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ) ).

tff('declare_A_b_fun_set$',type,
    'A_b_fun_set$': $tType ).

tff('declare_A_b_fun_set$1',type,
    'fmb_A_b_fun_set$_1': 'A_b_fun_set$' ).

tff('finite_domain_A_b_fun_set$',axiom,
    ! [X: 'A_b_fun_set$'] : ( X = 'fmb_A_b_fun_set$_1' ) ).

tff('declare_ZF_ZF_prod_ZF_fun$',type,
    'ZF_ZF_prod_ZF_fun$': $tType ).

tff('declare_ZF_ZF_prod_ZF_fun$1',type,
    'fmb_ZF_ZF_prod_ZF_fun$_1': 'ZF_ZF_prod_ZF_fun$' ).

tff('finite_domain_ZF_ZF_prod_ZF_fun$',axiom,
    ! [X: 'ZF_ZF_prod_ZF_fun$'] : ( X = 'fmb_ZF_ZF_prod_ZF_fun$_1' ) ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$',type,
    'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$': $tType ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$1',type,
    'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$_1': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$' ).

tff('finite_domain_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$',axiom,
    ! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'] : ( X = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$_1' ) ).

tff('declare_B_c_LSCategory_ext$',type,
    'B_c_LSCategory_ext$': $tType ).

tff('declare_B_c_LSCategory_ext$1',type,
    'fmb_B_c_LSCategory_ext$_1': 'B_c_LSCategory_ext$' ).

tff('finite_domain_B_c_LSCategory_ext$',axiom,
    ! [X: 'B_c_LSCategory_ext$'] : ( X = 'fmb_B_c_LSCategory_ext$_1' ) ).

tff('declare_B_b_fun$',type,
    'B_b_fun$': $tType ).

tff('declare_B_b_fun$1',type,
    'fmb_B_b_fun$_1': 'B_b_fun$' ).

tff('finite_domain_B_b_fun$',axiom,
    ! [X: 'B_b_fun$'] : ( X = 'fmb_B_b_fun$_1' ) ).

tff('declare_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$',type,
    'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$': $tType ).

tff('declare_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$1',type,
    'fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' ).

tff('finite_domain_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$',axiom,
    ! [X: 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$'] : ( X = 'fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1' ) ).

tff('declare_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$',type,
    'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$': $tType ).

tff('declare_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$1',type,
    'fmb_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$_1': 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' ).

tff('finite_domain_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$',axiom,
    ! [X: 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'] : ( X = 'fmb_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$_1' ) ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$',type,
    'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$': $tType ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$1',type,
    'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$_1': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$' ).

tff('finite_domain_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$',axiom,
    ! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$'] : ( X = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$_1' ) ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$',type,
    'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$': $tType ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$1',type,
    'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('finite_domain_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$',axiom,
    ! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$'] : ( X = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1' ) ).

tff('declare_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$',type,
    'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$': $tType ).

tff('declare_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$1',type,
    'fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$_1': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' ).

tff('finite_domain_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$',axiom,
    ! [X: 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'] : ( X = 'fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$_1' ) ).

tff('declare_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$',type,
    'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$': $tType ).

tff('declare_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$1',type,
    'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('finite_domain_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$',axiom,
    ! [X: 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'] : ( X = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1' ) ).

tff('declare_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$',type,
    'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$': $tType ).

tff('declare_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$1',type,
    'fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('finite_domain_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$',axiom,
    ! [X: 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$'] : ( X = 'fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ) ).

tff('declare_ZF_ZF_prod$',type,
    'ZF_ZF_prod$': $tType ).

tff('declare_ZF_ZF_prod$1',type,
    'fmb_ZF_ZF_prod$_1': 'ZF_ZF_prod$' ).

tff('finite_domain_ZF_ZF_prod$',axiom,
    ! [X: 'ZF_ZF_prod$'] : ( X = 'fmb_ZF_ZF_prod$_1' ) ).

tff('declare_B_b_prod_set$',type,
    'B_b_prod_set$': $tType ).

tff('declare_B_b_prod_set$1',type,
    'fmb_B_b_prod_set$_1': 'B_b_prod_set$' ).

tff('finite_domain_B_b_prod_set$',axiom,
    ! [X: 'B_b_prod_set$'] : ( X = 'fmb_B_b_prod_set$_1' ) ).

tff('declare_B$',type,
    'B$': $tType ).

tff('declare_B$1',type,
    'fmb_B$_1': 'B$' ).

tff('finite_domain_B$',axiom,
    ! [X: 'B$'] : ( X = 'fmb_B$_1' ) ).

tff('declare_A_ZF_fun_set$',type,
    'A_ZF_fun_set$': $tType ).

tff('declare_A_ZF_fun_set$1',type,
    'fmb_A_ZF_fun_set$_1': 'A_ZF_fun_set$' ).

tff('finite_domain_A_ZF_fun_set$',axiom,
    ! [X: 'A_ZF_fun_set$'] : ( X = 'fmb_A_ZF_fun_set$_1' ) ).

tff('declare_ZF_ZF_ZF_fun_fun$',type,
    'ZF_ZF_ZF_fun_fun$': $tType ).

tff('declare_ZF_ZF_ZF_fun_fun$1',type,
    'fmb_ZF_ZF_ZF_fun_fun$_1': 'ZF_ZF_ZF_fun_fun$' ).

tff('finite_domain_ZF_ZF_ZF_fun_fun$',axiom,
    ! [X: 'ZF_ZF_ZF_fun_fun$'] : ( X = 'fmb_ZF_ZF_ZF_fun_fun$_1' ) ).

tff('declare_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$',type,
    'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$': $tType ).

tff('declare_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$1',type,
    'fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1': 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' ).

tff('finite_domain_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$',axiom,
    ! [X: 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'] : ( X = 'fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1' ) ).

tff('declare_Unit_unit_unit_Category_ext$',type,
    'Unit_unit_unit_Category_ext$': $tType ).

tff('declare_Unit_unit_unit_Category_ext$1',type,
    'fmb_Unit_unit_unit_Category_ext$_1': 'Unit_unit_unit_Category_ext$' ).

tff('finite_domain_Unit_unit_unit_Category_ext$',axiom,
    ! [X: 'Unit_unit_unit_Category_ext$'] : ( X = 'fmb_Unit_unit_unit_Category_ext$_1' ) ).

tff('declare_C$',type,
    'C$': $tType ).

tff('declare_C$1',type,
    'fmb_C$_1': 'C$' ).

tff('finite_domain_C$',axiom,
    ! [X: 'C$'] : ( X = 'fmb_C$_1' ) ).

tff('declare_A_ZF_fun_bool_fun$',type,
    'A_ZF_fun_bool_fun$': $tType ).

tff('declare_A_ZF_fun_bool_fun$1',type,
    'fmb_A_ZF_fun_bool_fun$_1': 'A_ZF_fun_bool_fun$' ).

tff('finite_domain_A_ZF_fun_bool_fun$',axiom,
    ! [X: 'A_ZF_fun_bool_fun$'] : ( X = 'fmb_A_ZF_fun_bool_fun$_1' ) ).

tff('declare_B_b_prod_bool_fun$',type,
    'B_b_prod_bool_fun$': $tType ).

tff('declare_B_b_prod_bool_fun$1',type,
    'fmb_B_b_prod_bool_fun$_1': 'B_b_prod_bool_fun$' ).

tff('finite_domain_B_b_prod_bool_fun$',axiom,
    ! [X: 'B_b_prod_bool_fun$'] : ( X = 'fmb_B_b_prod_bool_fun$_1' ) ).

tff('declare_ZF_ZF_prod_ZF_fun_set$',type,
    'ZF_ZF_prod_ZF_fun_set$': $tType ).

tff('declare_ZF_ZF_prod_ZF_fun_set$1',type,
    'fmb_ZF_ZF_prod_ZF_fun_set$_1': 'ZF_ZF_prod_ZF_fun_set$' ).

tff('finite_domain_ZF_ZF_prod_ZF_fun_set$',axiom,
    ! [X: 'ZF_ZF_prod_ZF_fun_set$'] : ( X = 'fmb_ZF_ZF_prod_ZF_fun_set$_1' ) ).

tff('declare_ZF_ZF_fun$',type,
    'ZF_ZF_fun$': $tType ).

tff('declare_ZF_ZF_fun$1',type,
    'fmb_ZF_ZF_fun$_1': 'ZF_ZF_fun$' ).

tff('finite_domain_ZF_ZF_fun$',axiom,
    ! [X: 'ZF_ZF_fun$'] : ( X = 'fmb_ZF_ZF_fun$_1' ) ).

tff('declare_ZF_ZF_prod_bool_fun$',type,
    'ZF_ZF_prod_bool_fun$': $tType ).

tff('declare_ZF_ZF_prod_bool_fun$1',type,
    'fmb_ZF_ZF_prod_bool_fun$_1': 'ZF_ZF_prod_bool_fun$' ).

tff('finite_domain_ZF_ZF_prod_bool_fun$',axiom,
    ! [X: 'ZF_ZF_prod_bool_fun$'] : ( X = 'fmb_ZF_ZF_prod_bool_fun$_1' ) ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$',type,
    'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$': $tType ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$1',type,
    'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' ).

tff('finite_domain_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$',axiom,
    ! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'] : ( X = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1' ) ).

tff('declare_ZF_ZF_fun_set$',type,
    'ZF_ZF_fun_set$': $tType ).

tff('declare_ZF_ZF_fun_set$1',type,
    'fmb_ZF_ZF_fun_set$_1': 'ZF_ZF_fun_set$' ).

tff('finite_domain_ZF_ZF_fun_set$',axiom,
    ! [X: 'ZF_ZF_fun_set$'] : ( X = 'fmb_ZF_ZF_fun_set$_1' ) ).

tff('declare_B_b_prod_b_fun_set$',type,
    'B_b_prod_b_fun_set$': $tType ).

tff('declare_B_b_prod_b_fun_set$1',type,
    'fmb_B_b_prod_b_fun_set$_1': 'B_b_prod_b_fun_set$' ).

tff('finite_domain_B_b_prod_b_fun_set$',axiom,
    ! [X: 'B_b_prod_b_fun_set$'] : ( X = 'fmb_B_b_prod_b_fun_set$_1' ) ).

tff('declare_B_a_fun$',type,
    'B_a_fun$': $tType ).

tff('declare_B_a_fun$1',type,
    'fmb_B_a_fun$_1': 'B_a_fun$' ).

tff('finite_domain_B_a_fun$',axiom,
    ! [X: 'B_a_fun$'] : ( X = 'fmb_B_a_fun$_1' ) ).

tff('declare_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$',type,
    'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$': $tType ).

tff('declare_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$1',type,
    'fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' ).

tff('finite_domain_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$',axiom,
    ! [X: 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'] : ( X = 'fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1' ) ).

tff('declare_B_b_prod$',type,
    'B_b_prod$': $tType ).

tff('declare_B_b_prod$1',type,
    'fmb_B_b_prod$_1': 'B_b_prod$' ).

tff('finite_domain_B_b_prod$',axiom,
    ! [X: 'B_b_prod$'] : ( X = 'fmb_B_b_prod$_1' ) ).

tff('declare_ZF_ZF_fun_ZF_ZF_fun_fun$',type,
    'ZF_ZF_fun_ZF_ZF_fun_fun$': $tType ).

tff('declare_ZF_ZF_fun_ZF_ZF_fun_fun$1',type,
    'fmb_ZF_ZF_fun_ZF_ZF_fun_fun$_1': 'ZF_ZF_fun_ZF_ZF_fun_fun$' ).

tff('finite_domain_ZF_ZF_fun_ZF_ZF_fun_fun$',axiom,
    ! [X: 'ZF_ZF_fun_ZF_ZF_fun_fun$'] : ( X = 'fmb_ZF_ZF_fun_ZF_ZF_fun_fun$_1' ) ).

tff('declare_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$',type,
    'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$': $tType ).

tff('declare_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$1',type,
    'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$_1': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$' ).

tff('finite_domain_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$',axiom,
    ! [X: 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$'] : ( X = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$_1' ) ).

tff('declare_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$',type,
    'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$': $tType ).

tff('declare_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$1',type,
    'fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1': 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' ).

tff('finite_domain_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$',axiom,
    ! [X: 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'] : ( X = 'fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1' ) ).

tff('declare_A_bool_fun$',type,
    'A_bool_fun$': $tType ).

tff('declare_A_bool_fun$1',type,
    'fmb_A_bool_fun$_1': 'A_bool_fun$' ).

tff('finite_domain_A_bool_fun$',axiom,
    ! [X: 'A_bool_fun$'] : ( X = 'fmb_A_bool_fun$_1' ) ).

tff('declare_A_set$',type,
    'A_set$': $tType ).

tff('declare_A_set$1',type,
    'fmb_A_set$_1': 'A_set$' ).

tff('finite_domain_A_set$',axiom,
    ! [X: 'A_set$'] : ( X = 'fmb_A_set$_1' ) ).

tff('declare_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$',type,
    'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$': $tType ).

tff('declare_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$1',type,
    'fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$_1': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' ).

tff('finite_domain_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$',axiom,
    ! [X: 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'] : ( X = 'fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$_1' ) ).

tff('declare_A_b_fun$',type,
    'A_b_fun$': $tType ).

tff('declare_A_b_fun$1',type,
    'fmb_A_b_fun$_1': 'A_b_fun$' ).

tff('finite_domain_A_b_fun$',axiom,
    ! [X: 'A_b_fun$'] : ( X = 'fmb_A_b_fun$_1' ) ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$',type,
    'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$': $tType ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$1',type,
    'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' ).

tff('finite_domain_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$',axiom,
    ! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'] : ( X = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1' ) ).

tff('declare_B_set$',type,
    'B_set$': $tType ).

tff('declare_B_set$1',type,
    'fmb_B_set$_1': 'B_set$' ).

tff('finite_domain_B_set$',axiom,
    ! [X: 'B_set$'] : ( X = 'fmb_B_set$_1' ) ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$',type,
    'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$': $tType ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$1',type,
    'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$_1': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$' ).

tff('finite_domain_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$',axiom,
    ! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$'] : ( X = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$_1' ) ).

tff('declare_A_b_fun_bool_fun$',type,
    'A_b_fun_bool_fun$': $tType ).

tff('declare_A_b_fun_bool_fun$1',type,
    'fmb_A_b_fun_bool_fun$_1': 'A_b_fun_bool_fun$' ).

tff('finite_domain_A_b_fun_bool_fun$',axiom,
    ! [X: 'A_b_fun_bool_fun$'] : ( X = 'fmb_A_b_fun_bool_fun$_1' ) ).

tff('declare_A$',type,
    'A$': $tType ).

tff('declare_A$1',type,
    'fmb_A$_1': 'A$' ).

tff('finite_domain_A$',axiom,
    ! [X: 'A$'] : ( X = 'fmb_A$_1' ) ).

tff('declare_ZF_ZF_unit_Category_ext$',type,
    'ZF_ZF_unit_Category_ext$': $tType ).

tff('declare_ZF_ZF_unit_Category_ext$1',type,
    'fmb_ZF_ZF_unit_Category_ext$_1': 'ZF_ZF_unit_Category_ext$' ).

tff('finite_domain_ZF_ZF_unit_Category_ext$',axiom,
    ! [X: 'ZF_ZF_unit_Category_ext$'] : ( X = 'fmb_ZF_ZF_unit_Category_ext$_1' ) ).

tff('declare_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$',type,
    'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$': $tType ).

tff('declare_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$1',type,
    'fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('finite_domain_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$',axiom,
    ! [X: 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'] : ( X = 'fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ) ).

tff('declare_B_b_prod_b_fun$',type,
    'B_b_prod_b_fun$': $tType ).

tff('declare_B_b_prod_b_fun$1',type,
    'fmb_B_b_prod_b_fun$_1': 'B_b_prod_b_fun$' ).

tff('finite_domain_B_b_prod_b_fun$',axiom,
    ! [X: 'B_b_prod_b_fun$'] : ( X = 'fmb_B_b_prod_b_fun$_1' ) ).

tff('declare_A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$',type,
    'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$': $tType ).

tff('declare_A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$1',type,
    'fmb_A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1': 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('finite_domain_A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$',axiom,
    ! [X: 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$'] : ( X = 'fmb_A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ) ).

tff('declare_B_set_b_set_fun$',type,
    'B_set_b_set_fun$': $tType ).

tff('declare_B_set_b_set_fun$1',type,
    'fmb_B_set_b_set_fun$_1': 'B_set_b_set_fun$' ).

tff('finite_domain_B_set_b_set_fun$',axiom,
    ! [X: 'B_set_b_set_fun$'] : ( X = 'fmb_B_set_b_set_fun$_1' ) ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$',type,
    'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$': $tType ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$1',type,
    'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' ).

tff('finite_domain_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$',axiom,
    ! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'] : ( X = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1' ) ).

tff('declare_ZF_bool_fun$',type,
    'ZF_bool_fun$': $tType ).

tff('declare_ZF_bool_fun$1',type,
    'fmb_ZF_bool_fun$_1': 'ZF_bool_fun$' ).

tff('finite_domain_ZF_bool_fun$',axiom,
    ! [X: 'ZF_bool_fun$'] : ( X = 'fmb_ZF_bool_fun$_1' ) ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$',type,
    'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$': $tType ).

tff('declare_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$1',type,
    'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' ).

tff('finite_domain_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$',axiom,
    ! [X: 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'] : ( X = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1' ) ).

tff('declare_B_b_b_fun_fun$',type,
    'B_b_b_fun_fun$': $tType ).

tff('declare_B_b_b_fun_fun$1',type,
    'fmb_B_b_b_fun_fun$_1': 'B_b_b_fun_fun$' ).

tff('finite_domain_B_b_b_fun_fun$',axiom,
    ! [X: 'B_b_b_fun_fun$'] : ( X = 'fmb_B_b_b_fun_fun$_1' ) ).

tff('declare_ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$',type,
    'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$': $tType ).

tff('declare_ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$1',type,
    'fmb_ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$_1': 'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$' ).

tff('finite_domain_ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$',axiom,
    ! [X: 'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$'] : ( X = 'fmb_ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$_1' ) ).

tff('declare_A_ZF_fun$',type,
    'A_ZF_fun$': $tType ).

tff('declare_A_ZF_fun$1',type,
    'fmb_A_ZF_fun$_1': 'A_ZF_fun$' ).

tff('finite_domain_A_ZF_fun$',axiom,
    ! [X: 'A_ZF_fun$'] : ( X = 'fmb_A_ZF_fun$_1' ) ).

tff('declare_Unit$',type,
    'Unit$': $tType ).

tff('declare_Unit$1',type,
    'fmb_Unit$_1': 'Unit$' ).

tff('finite_domain_Unit$',axiom,
    ! [X: 'Unit$'] : ( X = 'fmb_Unit$_1' ) ).

tff('declare_ZF$',type,
    'ZF$': $tType ).

tff('declare_ZF$1',type,
    'fmb_ZF$_1': 'ZF$' ).

tff('finite_domain_ZF$',axiom,
    ! [X: 'ZF$'] : ( X = 'fmb_ZF$_1' ) ).

tff('declare_B_ZF_fun$',type,
    'B_ZF_fun$': $tType ).

tff('declare_B_ZF_fun$1',type,
    'fmb_B_ZF_fun$_1': 'B_ZF_fun$' ).

tff('finite_domain_B_ZF_fun$',axiom,
    ! [X: 'B_ZF_fun$'] : ( X = 'fmb_B_ZF_fun$_1' ) ).

tff('declare_B_a_fun_set$',type,
    'B_a_fun_set$': $tType ).

tff('declare_B_a_fun_set$1',type,
    'fmb_B_a_fun_set$_1': 'B_a_fun_set$' ).

tff('finite_domain_B_a_fun_set$',axiom,
    ! [X: 'B_a_fun_set$'] : ( X = 'fmb_B_a_fun_set$_1' ) ).

tff('declare_B_a_fun_bool_fun$',type,
    'B_a_fun_bool_fun$': $tType ).

tff('declare_B_a_fun_bool_fun$1',type,
    'fmb_B_a_fun_bool_fun$_1': 'B_a_fun_bool_fun$' ).

tff('finite_domain_B_a_fun_bool_fun$',axiom,
    ! [X: 'B_a_fun_bool_fun$'] : ( X = 'fmb_B_a_fun_bool_fun$_1' ) ).

tff('declare_B_bool_fun$',type,
    'B_bool_fun$': $tType ).

tff('declare_B_bool_fun$1',type,
    'fmb_B_bool_fun$_1': 'B_bool_fun$' ).

tff('finite_domain_B_bool_fun$',axiom,
    ! [X: 'B_bool_fun$'] : ( X = 'fmb_B_bool_fun$_1' ) ).

tff('declare_B_ZF_fun_bool_fun$',type,
    'B_ZF_fun_bool_fun$': $tType ).

tff('declare_B_ZF_fun_bool_fun$1',type,
    'fmb_B_ZF_fun_bool_fun$_1': 'B_ZF_fun_bool_fun$' ).

tff('finite_domain_B_ZF_fun_bool_fun$',axiom,
    ! [X: 'B_ZF_fun_bool_fun$'] : ( X = 'fmb_B_ZF_fun_bool_fun$_1' ) ).

tff('declare_makeCat$a',type,
    'makeCat$a': 'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$' ).

tff('makeCat$a_definition',axiom,
    'makeCat$a' = 'fmb_A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$_1' ).

tff('declare_c$',type,
    'c$': 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('c$_definition',axiom,
    'c$' = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_natTrans$',type,
    'natTrans$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$' ).

tff('natTrans$_definition',axiom,
    'natTrans$' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$_1' ).

tff('declare_top$',type,
    'top$': 'ZF_set$' ).

tff('top$_definition',axiom,
    'top$' = 'fmb_ZF_set$_1' ).

tff('declare_oppositeCategory$',type,
    'oppositeCategory$': 'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$' ).

tff('oppositeCategory$_definition',axiom,
    'oppositeCategory$' = 'fmb_A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$_1' ).

tff('declare_f$',type,
    'f$': 'B$' ).

tff('f$_definition',axiom,
    'f$' = 'fmb_B$_1' ).

tff('declare_equivalence_axioms$',type,
    'equivalence_axioms$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' ).

tff('equivalence_axioms$_definition',axiom,
    'equivalence_axioms$' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1' ).

tff('declare_idNatTrans$d',type,
    'idNatTrans$d': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' ).

tff('idNatTrans$d_definition',axiom,
    'idNatTrans$d' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1' ).

tff('declare_uut$',type,
    'uut$': 'ZF_bool_fun$' ).

tff('uut$_definition',axiom,
    'uut$' = 'fmb_ZF_bool_fun$_1' ).

tff('declare_functorM$a',type,
    'functorM$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' ).

tff('functorM$a_definition',axiom,
    'functorM$a' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1' ).

tff('declare_set$',type,
    'set$': 'ZF_ZF_unit_Category_ext$' ).

tff('set$_definition',axiom,
    'set$' = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_unity$',type,
    'unity$': 'Unit$' ).

tff('unity$_definition',axiom,
    'unity$' = 'fmb_Unit$_1' ).

tff('declare_oppositeCategory$b',type,
    'oppositeCategory$b': 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' ).

tff('oppositeCategory$b_definition',axiom,
    'oppositeCategory$b' = 'fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1' ).

tff('declare_zFfunCod$',type,
    'zFfunCod$': 'ZF_ZF_fun$' ).

tff('zFfunCod$_definition',axiom,
    'zFfunCod$' = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_nTDom$',type,
    'nTDom$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' ).

tff('nTDom$_definition',axiom,
    'nTDom$' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1' ).

tff('declare_set$a',type,
    'set$a': 'ZF_ZF_unit_Category_ext$' ).

tff('set$a_definition',axiom,
    'set$a' = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_equivalence$a',type,
    'equivalence$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' ).

tff('equivalence$a_definition',axiom,
    'equivalence$a' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1' ).

tff('declare_zFfunComp$',type,
    'zFfunComp$': 'ZF_ZF_ZF_fun_fun$' ).

tff('zFfunComp$_definition',axiom,
    'zFfunComp$' = 'fmb_ZF_ZF_ZF_fun_fun$_1' ).

tff('declare_functor$',type,
    'functor$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' ).

tff('functor$_definition',axiom,
    'functor$' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1' ).

tff('declare_makeFtor$',type,
    'makeFtor$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' ).

tff('makeFtor$_definition',axiom,
    'makeFtor$' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1' ).

tff('declare_natTransExt$a',type,
    'natTransExt$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$' ).

tff('natTransExt$a_definition',axiom,
    'natTransExt$a' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$_1' ).

tff('declare_nTCod$',type,
    'nTCod$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' ).

tff('nTCod$_definition',axiom,
    'nTCod$' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1' ).

tff('declare_uuv$',type,
    'uuv$': 'ZF_ZF_fun$' ).

tff('uuv$_definition',axiom,
    'uuv$' = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_functorExt$a',type,
    'functorExt$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' ).

tff('functorExt$a_definition',axiom,
    'functorExt$a' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1' ).

tff('declare_zFfunDom$',type,
    'zFfunDom$': 'ZF_ZF_fun$' ).

tff('zFfunDom$_definition',axiom,
    'zFfunDom$' = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_natTransP$a',type,
    'natTransP$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$' ).

tff('natTransP$a_definition',axiom,
    'natTransP$a' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$_1' ).

tff('declare_zFfunApp$',type,
    'zFfunApp$': 'ZF_ZF_ZF_fun_fun$' ).

tff('zFfunApp$_definition',axiom,
    'zFfunApp$' = 'fmb_ZF_ZF_ZF_fun_fun$_1' ).

tff('declare_functorM_axioms$a',type,
    'functorM_axioms$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' ).

tff('functorM_axioms$a_definition',axiom,
    'functorM_axioms$a' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1' ).

tff('declare_makeCat$',type,
    'makeCat$': 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' ).

tff('makeCat$_definition',axiom,
    'makeCat$' = 'fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1' ).

tff('declare_uuu$',type,
    'uuu$': 'ZF_ZF_fun$' ).

tff('uuu$_definition',axiom,
    'uuu$' = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_preFunctor$',type,
    'preFunctor$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' ).

tff('preFunctor$_definition',axiom,
    'preFunctor$' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1' ).

tff('declare_explode$',type,
    'explode$': 'ZF_ZF_set_fun$' ).

tff('explode$_definition',axiom,
    'explode$' = 'fmb_ZF_ZF_set_fun$_1' ).

tff('declare_isZFfun$',type,
    'isZFfun$': 'ZF_bool_fun$' ).

tff('isZFfun$_definition',axiom,
    'isZFfun$' = 'fmb_ZF_bool_fun$_1' ).

tff('declare_natTransComp$c',type,
    'natTransComp$c': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$' ).

tff('natTransComp$c_definition',axiom,
    'natTransComp$c' = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$_1' ).

tff('declare_functorComp$a',type,
    'functorComp$a': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_functorComp$a',axiom,
    'functorComp$a'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_collect$e',type,
    'collect$e': 'B_ZF_fun_bool_fun$' > 'B_ZF_fun_set$' ).

tff('function_collect$e',axiom,
    'collect$e'('fmb_B_ZF_fun_bool_fun$_1') = 'fmb_B_ZF_fun_set$_1' ).

tff('declare_more_update$',type,
    'more_update$': ( 'Unit_unit_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('function_more_update$',axiom,
    'more_update$'('fmb_Unit_unit_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ).

tff('declare_id$',type,
    'id$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A_b_fun$' ).

tff('function_id$',axiom,
    'id$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_restrict$c',type,
    'restrict$c': ( 'A_ZF_fun$' * 'A_set$' ) > 'A_ZF_fun$' ).

tff('function_restrict$c',axiom,
    'restrict$c'('fmb_A_ZF_fun$_1','fmb_A_set$_1') = 'fmb_A_ZF_fun$_1' ).

tff('declare_functorComp$',type,
    'functorComp$': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_functorComp$',axiom,
    'functorComp$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_catDom$a',type,
    'catDom$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$' ).

tff('function_catDom$a',axiom,
    'catDom$a'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_extensional$c',type,
    'extensional$c': 'B_set$' > 'B_a_fun_set$' ).

tff('function_extensional$c',axiom,
    'extensional$c'('fmb_B_set$_1') = 'fmb_B_a_fun_set$_1' ).

tff('declare_uun$',type,
    'uun$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' ).

tff('function_uun$',axiom,
    'uun$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1' ).

tff('declare_collect$',type,
    'collect$': 'ZF_ZF_prod_bool_fun$' > 'ZF_ZF_prod_set$' ).

tff('function_collect$',axiom,
    'collect$'('fmb_ZF_ZF_prod_bool_fun$_1') = 'fmb_ZF_ZF_prod_set$_1' ).

tff('declare_mor_update$a',type,
    'mor_update$a': 'B_set_b_set_fun$' > 'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$' ).

tff('function_mor_update$a',axiom,
    'mor_update$a'('fmb_B_set_b_set_fun$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$_1' ).

tff('declare_uum$',type,
    'uum$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'B$' ) > 'A_ZF_fun$' ).

tff('function_uum$',axiom,
    'uum$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_B$_1') = 'fmb_A_ZF_fun$_1' ).

tff('declare_nTCod$c',type,
    'nTCod$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' ).

tff('function_nTCod$c',axiom,
    'nTCod$c'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1') = 'fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$_1' ).

tff('declare_uuq$',type,
    'uuq$': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A$' ) > 'ZF_bool_fun$' ).

tff('function_uuq$',axiom,
    'uuq$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1','fmb_A$_1') = 'fmb_ZF_bool_fun$_1' ).

tff('declare_nt_abbrev$a',type,
    'nt_abbrev$a': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' ).

tff('function_nt_abbrev$a',axiom,
    'nt_abbrev$a'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1' ).

tff('declare_fun_app$s',type,
    'fun_app$s': ( 'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$' * 'A_b_b_c_LSCategory_ext_Category_ext$' ) > 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('function_fun_app$s',axiom,
    'fun_app$s'('fmb_A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$_1','fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_more$b',type,
    'more$b': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'Unit$' ).

tff('function_more$b',axiom,
    'more$b'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') = 'fmb_Unit$_1' ).

tff('declare_unitFunctor$',type,
    'unitFunctor$': 'ZF_ZF_unit_Category_ext$' > 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' ).

tff('function_unitFunctor$',axiom,
    'unitFunctor$'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1' ).

tff('declare_natTransMap$d',type,
    'natTransMap$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_b_fun$' ).

tff('function_natTransMap$d',axiom,
    'natTransMap$d'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_natTrans_ext$a',type,
    'natTrans_ext$a': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_ZF_fun$' * 'Unit$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('function_natTrans_ext$a',axiom,
    'natTrans_ext$a'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1','fmb_A_ZF_fun$_1','fmb_Unit$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ).

tff('declare_catExp$c',type,
    'catExp$c': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_catExp$c',axiom,
    'catExp$c'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_the$a',type,
    'the$a': 'B_bool_fun$' > 'B$' ).

tff('function_the$a',axiom,
    'the$a'('fmb_B_bool_fun$_1') = 'fmb_B$_1' ).

tff('declare_mapsTo$',type,
    'mapsTo$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'B$' * 'A$' ) > 'A_bool_fun$' ).

tff('function_mapsTo$',axiom,
    'mapsTo$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_B$_1','fmb_A$_1') = 'fmb_A_bool_fun$_1' ).

tff('declare_obj$a',type,
    'obj$a': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A_set$' ).

tff('function_obj$a',axiom,
    'obj$a'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_A_set$_1' ).

tff('declare_uuz$',type,
    'uuz$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_fun_fun$' ).

tff('function_uuz$',axiom,
    'uuz$'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_ZF_fun_fun$_1' ).

tff('declare_case_prod$',type,
    'case_prod$': 'ZF_ZF_ZF_fun_fun$' > 'ZF_ZF_prod_ZF_fun$' ).

tff('function_case_prod$',axiom,
    'case_prod$'('fmb_ZF_ZF_ZF_fun_fun$_1') = 'fmb_ZF_ZF_prod_ZF_fun$_1' ).

tff('declare_catCod$d',type,
    'catCod$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('function_catCod$d',axiom,
    'catCod$d'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_catDom$c',type,
    'catDom$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$' ).

tff('function_catDom$c',axiom,
    'catDom$c'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_fun_app$n',type,
    'fun_app$n': ( 'A_ZF_fun$' * 'A$' ) > 'ZF$' ).

tff('function_fun_app$n',axiom,
    'fun_app$n'('fmb_A_ZF_fun$_1','fmb_A$_1') = 'fmb_ZF$_1' ).

tff('declare_uua$',type,
    'uua$': 'ZF_set$' > 'ZF_bool_fun$' ).

tff('function_uua$',axiom,
    'uua$'('fmb_ZF_set$_1') = 'fmb_ZF_bool_fun$_1' ).

tff('declare_uup$',type,
    'uup$': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > 'A_ZF_fun$' ).

tff('function_uup$',axiom,
    'uup$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_fun$_1' ).

tff('declare_extensional$d',type,
    'extensional$d': 'ZF_ZF_prod_set$' > 'ZF_ZF_prod_ZF_fun_set$' ).

tff('function_extensional$d',axiom,
    'extensional$d'('fmb_ZF_ZF_prod_set$_1') = 'fmb_ZF_ZF_prod_ZF_fun_set$_1' ).

tff('declare_obj_update$',type,
    'obj_update$': 'ZF_set_ZF_set_fun$' > 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' ).

tff('function_obj_update$',axiom,
    'obj_update$'('fmb_ZF_set_ZF_set_fun$_1') = 'fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1' ).

tff('declare_catDom_update$a',type,
    'catDom_update$a': 'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' ).

tff('function_catDom_update$a',axiom,
    'catDom_update$a'('fmb_A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1' ).

tff('declare_catCod$',type,
    'catCod$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$' ).

tff('function_catCod$',axiom,
    'catCod$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_nTCatDom$f',type,
    'nTCatDom$f': 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_unit_Category_ext$' ).

tff('function_nTCatDom$f',axiom,
    'nTCatDom$f'('fmb_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_restrict$a',type,
    'restrict$a': ( 'B_b_prod_b_fun$' * 'B_b_prod_set$' * 'B_b_prod$' ) > 'B$' ).

tff('function_restrict$a',axiom,
    'restrict$a'('fmb_B_b_prod_b_fun$_1','fmb_B_b_prod_set$_1','fmb_B_b_prod$_1') = 'fmb_B$_1' ).

tff('declare_mapM$a',type,
    'mapM$a': ( 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' * 'ZF$' ) > 'Unit$' ).

tff('function_mapM$a',axiom,
    'mapM$a'('fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1','fmb_ZF$_1') = 'fmb_Unit$_1' ).

tff('declare_catExp$',type,
    'catExp$': ( 'ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_catExp$',axiom,
    'catExp$'('fmb_ZF_ZF_unit_Category_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_more$c',type,
    'more$c': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'C$' ).

tff('function_more$c',axiom,
    'more$c'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_C$_1' ).

tff('declare_fun_app$r',type,
    'fun_app$r': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_fun_app$r',axiom,
    'fun_app$r'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_nTDom$a',type,
    'nTDom$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ).

tff('function_nTDom$a',axiom,
    'nTDom$a'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1' ).

tff('declare_mapO$b',type,
    'mapO$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_fun$' ).

tff('function_mapO$b',axiom,
    'mapO$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_natTransComp$g',type,
    'natTransComp$g': ( 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('function_natTransComp$g',axiom,
    'natTransComp$g'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1','fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ).

tff('declare_nTCompDefined$a',type,
    'nTCompDefined$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$' ).

tff('function_nTCompDefined$a',axiom,
    'nTCompDefined$a'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$_1' ).

tff('declare_uus$',type,
    'uus$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF$' ) > 'B_bool_fun$' ).

tff('function_uus$',axiom,
    'uus$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_ZF$_1') = 'fmb_B_bool_fun$_1' ).

tff('declare_uud$',type,
    'uud$': 'B_a_fun_set$' > 'B_a_fun_bool_fun$' ).

tff('function_uud$',axiom,
    'uud$'('fmb_B_a_fun_set$_1') = 'fmb_B_a_fun_bool_fun$_1' ).

tff('declare_natTransComp$d',type,
    'natTransComp$d': ( 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' ) > 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' ).

tff('function_natTransComp$d',axiom,
    'natTransComp$d'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1','fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1') = 'fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1' ).

tff('declare_fun_app$ab',type,
    'fun_app$ab': ( 'B_a_fun$' * 'B$' ) > 'A$' ).

tff('function_fun_app$ab',axiom,
    'fun_app$ab'('fmb_B_a_fun$_1','fmb_B$_1') = 'fmb_A$_1' ).

tff('declare_nTCatDom$d',type,
    'nTCatDom$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('function_nTCatDom$d',axiom,
    'nTCatDom$d'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_mapO$f',type,
    'mapO$f': ( 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ).

tff('function_mapO$f',axiom,
    'mapO$f'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1','fmb_A$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1' ).

tff('declare_collect$a',type,
    'collect$a': 'B_b_prod_bool_fun$' > 'B_b_prod_set$' ).

tff('function_collect$a',axiom,
    'collect$a'('fmb_B_b_prod_bool_fun$_1') = 'fmb_B_b_prod_set$_1' ).

tff('declare_nTCod$e',type,
    'nTCod$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' ).

tff('function_nTCod$e',axiom,
    'nTCod$e'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$_1' ).

tff('declare_mor$c',type,
    'mor$c': 'Unit_unit_unit_Category_ext$' > 'Unit_set$' ).

tff('function_mor$c',axiom,
    'mor$c'('fmb_Unit_unit_unit_Category_ext$_1') = 'fmb_Unit_set$_1' ).

tff('declare_pair$a',type,
    'pair$a': ( 'B$' * 'B$' ) > 'B_b_prod$' ).

tff('function_pair$a',axiom,
    'pair$a'('fmb_B$_1','fmb_B$_1') = 'fmb_B_b_prod$_1' ).

tff('declare_dom_update$',type,
    'dom_update$': 'ZF_ZF_fun_ZF_ZF_fun_fun$' > 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' ).

tff('function_dom_update$',axiom,
    'dom_update$'('fmb_ZF_ZF_fun_ZF_ZF_fun_fun$_1') = 'fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1' ).

tff('declare_fun_app$u',type,
    'fun_app$u': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ).

tff('function_fun_app$u',axiom,
    'fun_app$u'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1' ).

tff('declare_uuk$',type,
    'uuk$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_fun_fun$' ).

tff('function_uuk$',axiom,
    'uuk$'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_ZF_fun_fun$_1' ).

tff('declare_comp_update$',type,
    'comp_update$': 'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$' > 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' ).

tff('function_comp_update$',axiom,
    'comp_update$'('fmb_ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$_1') = 'fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1' ).

tff('declare_case_prod$a',type,
    'case_prod$a': 'B_b_b_fun_fun$' > 'B_b_prod_b_fun$' ).

tff('function_case_prod$a',axiom,
    'case_prod$a'('fmb_B_b_b_fun_fun$_1') = 'fmb_B_b_prod_b_fun$_1' ).

tff('declare_nTCatDom$b',type,
    'nTCatDom$b': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF_ZF_unit_Category_ext$' ).

tff('function_nTCatDom$b',axiom,
    'nTCatDom$b'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_natTransComp$f',type,
    'natTransComp$f': ( 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' ) > 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' ).

tff('function_natTransComp$f',axiom,
    'natTransComp$f'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1','fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_uu$',type,
    'uu$': 'B_set$' > 'B_bool_fun$' ).

tff('function_uu$',axiom,
    'uu$'('fmb_B_set$_1') = 'fmb_B_bool_fun$_1' ).

tff('declare_nTCatCod$d',type,
    'nTCatCod$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('function_nTCatCod$d',axiom,
    'nTCatCod$d'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_mapM$d',type,
    'mapM$d': ( 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' * 'B$' ) > 'B$' ).

tff('function_mapM$d',axiom,
    'mapM$d'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$_1','fmb_B$_1') = 'fmb_B$_1' ).

tff('declare_uuo$',type,
    'uuo$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$' ).

tff('function_uuo$',axiom,
    'uuo$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$_1' ).

tff('declare_uur$',type,
    'uur$': 'ZF$' > 'ZF_ZF_ZF_fun_fun$' ).

tff('function_uur$',axiom,
    'uur$'('fmb_ZF$_1') = 'fmb_ZF_ZF_ZF_fun_fun$_1' ).

tff('declare_fun_app$z',type,
    'fun_app$z': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' ).

tff('function_fun_app$z',axiom,
    'fun_app$z'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1' ).

tff('declare_nTDom$f',type,
    'nTDom$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_nTDom$f',axiom,
    'nTDom$f'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_uuy$',type,
    'uuy$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_prod_bool_fun$' ).

tff('function_uuy$',axiom,
    'uuy$'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_prod_bool_fun$_1' ).

tff('declare_natTransComp$',type,
    'natTransComp$': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('function_natTransComp$',axiom,
    'natTransComp$'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_fun_app$l',type,
    'fun_app$l': ( 'B_b_fun$' * 'B$' ) > 'B$' ).

tff('function_fun_app$l',axiom,
    'fun_app$l'('fmb_B_b_fun$_1','fmb_B$_1') = 'fmb_B$_1' ).

tff('declare_mor2ZF$',type,
    'mor2ZF$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_ZF_fun$' ).

tff('function_mor2ZF$',axiom,
    'mor2ZF$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_B_ZF_fun$_1' ).

tff('declare_idNatTrans$b',type,
    'idNatTrans$b': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('function_idNatTrans$b',axiom,
    'idNatTrans$b'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ).

tff('declare_natTransMap$c',type,
    'natTransMap$c': ( 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' * 'ZF$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('function_natTransMap$c',axiom,
    'natTransMap$c'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1','fmb_ZF$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_catDom$',type,
    'catDom$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('function_catDom$',axiom,
    'catDom$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_zFfun$',type,
    'zFfun$': ( 'ZF$' * 'ZF$' * 'ZF_ZF_fun$' ) > 'ZF$' ).

tff('function_zFfun$',axiom,
    'zFfun$'('fmb_ZF$_1','fmb_ZF$_1','fmb_ZF_ZF_fun$_1') = 'fmb_ZF$_1' ).

tff('declare_catDom_update$',type,
    'catDom_update$': 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$' ).

tff('function_catDom_update$',axiom,
    'catDom_update$'('fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$_1' ).

tff('declare_inverse_rel$',type,
    'inverse_rel$': ( 'ZF_ZF_unit_Category_ext$' * 'ZF$' ) > 'ZF_bool_fun$' ).

tff('function_inverse_rel$',axiom,
    'inverse_rel$'('fmb_ZF_ZF_unit_Category_ext$_1','fmb_ZF$_1') = 'fmb_ZF_bool_fun$_1' ).

tff('declare_extensional$b',type,
    'extensional$b': 'B_set$' > 'B_ZF_fun_set$' ).

tff('function_extensional$b',axiom,
    'extensional$b'('fmb_B_set$_1') = 'fmb_B_ZF_fun_set$_1' ).

tff('declare_fun_app$p',type,
    'fun_app$p': ( 'A_b_fun$' * 'A$' ) > 'B$' ).

tff('function_fun_app$p',axiom,
    'fun_app$p'('fmb_A_b_fun$_1','fmb_A$_1') = 'fmb_B$_1' ).

tff('declare_idNatTrans$',type,
    'idNatTrans$': 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' > 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' ).

tff('function_idNatTrans$',axiom,
    'idNatTrans$'('fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1') = 'fmb_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_idNatTrans$c',type,
    'idNatTrans$c': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('function_idNatTrans$c',axiom,
    'idNatTrans$c'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_more$a',type,
    'more$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'Unit$' ).

tff('function_more$a',axiom,
    'more$a'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_Unit$_1' ).

tff('declare_more$',type,
    'more$': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'Unit$' ).

tff('function_more$',axiom,
    'more$'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') = 'fmb_Unit$_1' ).

tff('declare_nTCatCod$',type,
    'nTCatCod$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'ZF_ZF_unit_Category_ext$' ).

tff('function_nTCatCod$',axiom,
    'nTCatCod$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_nTCod$f',type,
    'nTCod$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_nTCod$f',axiom,
    'nTCod$f'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_mapM$e',type,
    'mapM$e': ( 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' * 'ZF$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('function_mapM$e',axiom,
    'mapM$e'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$_1','fmb_ZF$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_nTCatCod$a',type,
    'nTCatCod$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_unit_Category_ext$' ).

tff('function_nTCatCod$a',axiom,
    'nTCatCod$a'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_fun_app$ac',type,
    'fun_app$ac': ( 'ZF_ZF_fun_ZF_ZF_fun_fun$' * 'ZF_ZF_fun$' ) > 'ZF_ZF_fun$' ).

tff('function_fun_app$ac',axiom,
    'fun_app$ac'('fmb_ZF_ZF_fun_ZF_ZF_fun_fun$_1','fmb_ZF_ZF_fun$_1') = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_natTransMap$e',type,
    'natTransMap$e': ( 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('function_natTransMap$e',axiom,
    'natTransMap$e'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1','fmb_A$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_natTransMap$b',type,
    'natTransMap$b': ( 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'ZF$' ) > 'B$' ).

tff('function_natTransMap$b',axiom,
    'natTransMap$b'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1','fmb_ZF$_1') = 'fmb_B$_1' ).

tff('declare_fun_app$k',type,
    'fun_app$k': ( 'ZF_ZF_ZF_fun_fun$' * 'ZF$' ) > 'ZF_ZF_fun$' ).

tff('function_fun_app$k',axiom,
    'fun_app$k'('fmb_ZF_ZF_ZF_fun_fun$_1','fmb_ZF$_1') = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_homFtor$',type,
    'homFtor$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_homFtor$',axiom,
    'homFtor$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_A$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_category_ext$',type,
    'category_ext$': ( 'A_set$' * 'B_set$' * 'B_a_fun$' * 'B_a_fun$' * 'A_b_fun$' * 'B_b_b_fun_fun$' * 'B_c_LSCategory_ext$' ) > 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('function_category_ext$',axiom,
    'category_ext$'('fmb_A_set$_1','fmb_B_set$_1','fmb_B_a_fun$_1','fmb_B_a_fun$_1','fmb_A_b_fun$_1','fmb_B_b_b_fun_fun$_1','fmb_B_c_LSCategory_ext$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_catDom$b',type,
    'catDom$b': 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$' ).

tff('function_catDom$b',axiom,
    'catDom$b'('fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_nTDom$e',type,
    'nTDom$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' ).

tff('function_nTDom$e',axiom,
    'nTDom$e'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$_1' ).

tff('declare_more$e',type,
    'more$e': 'ZF_ZF_unit_Category_ext$' > 'Unit$' ).

tff('function_more$e',axiom,
    'more$e'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_Unit$_1' ).

tff('declare_catDom$f',type,
    'catDom$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('function_catDom$f',axiom,
    'catDom$f'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_idNatTrans$e',type,
    'idNatTrans$e': 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' > 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' ).

tff('function_idNatTrans$e',axiom,
    'idNatTrans$e'('fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1') = 'fmb_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_nTDom$c',type,
    'nTDom$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' ).

tff('function_nTDom$c',axiom,
    'nTDom$c'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1') = 'fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$_1' ).

tff('declare_compDefined$',type,
    'compDefined$': ( 'ZF_ZF_unit_Category_ext$' * 'ZF$' ) > 'ZF_bool_fun$' ).

tff('function_compDefined$',axiom,
    'compDefined$'('fmb_ZF_ZF_unit_Category_ext$_1','fmb_ZF$_1') = 'fmb_ZF_bool_fun$_1' ).

tff('declare_makeCat$c',type,
    'makeCat$c': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_makeCat$c',axiom,
    'makeCat$c'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_extensional$f',type,
    'extensional$f': 'B_b_prod_set$' > 'B_b_prod_b_fun_set$' ).

tff('function_extensional$f',axiom,
    'extensional$f'('fmb_B_b_prod_set$_1') = 'fmb_B_b_prod_b_fun_set$_1' ).

tff('declare_restrict$d',type,
    'restrict$d': ( 'B_a_fun$' * 'B_set$' ) > 'B_a_fun$' ).

tff('function_restrict$d',axiom,
    'restrict$d'('fmb_B_a_fun$_1','fmb_B_set$_1') = 'fmb_B_a_fun$_1' ).

tff('declare_mapM$',type,
    'mapM$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'B_ZF_fun$' ).

tff('function_mapM$',axiom,
    'mapM$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') = 'fmb_B_ZF_fun$_1' ).

tff('declare_collect$d',type,
    'collect$d': 'A_bool_fun$' > 'A_set$' ).

tff('function_collect$d',axiom,
    'collect$d'('fmb_A_bool_fun$_1') = 'fmb_A_set$_1' ).

tff('declare_natTrans_ext$',type,
    'natTrans_ext$': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_fun$' * 'Unit$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('function_natTrans_ext$',axiom,
    'natTrans_ext$'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1','fmb_ZF_ZF_fun$_1','fmb_Unit$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_catExp$a',type,
    'catExp$a': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_catExp$a',axiom,
    'catExp$a'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_dom$b',type,
    'dom$b': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_dom$b',axiom,
    'dom$b'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_fun_app$m',type,
    'fun_app$m': ( 'B_b_b_fun_fun$' * 'B$' ) > 'B_b_fun$' ).

tff('function_fun_app$m',axiom,
    'fun_app$m'('fmb_B_b_b_fun_fun$_1','fmb_B$_1') = 'fmb_B_b_fun$_1' ).

tff('declare_nTCod_update$a',type,
    'nTCod_update$a': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('function_nTCod_update$a',axiom,
    'nTCod_update$a'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ).

tff('declare_catCod$c',type,
    'catCod$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('function_catCod$c',axiom,
    'catCod$c'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_restrict$f',type,
    'restrict$f': ( 'ZF_ZF_fun$' * 'ZF_set$' ) > 'ZF_ZF_fun$' ).

tff('function_restrict$f',axiom,
    'restrict$f'('fmb_ZF_ZF_fun$_1','fmb_ZF_set$_1') = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_natTransMap$',type,
    'natTransMap$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_ZF_fun$' ).

tff('function_natTransMap$',axiom,
    'natTransMap$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_fun$_1' ).

tff('declare_natTransMap$f',type,
    'natTransMap$f': ( 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' * 'ZF$' ) > 'Unit$' ).

tff('function_natTransMap$f',axiom,
    'natTransMap$f'('fmb_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$_1','fmb_ZF$_1') = 'fmb_Unit$_1' ).

tff('declare_oppositeCategory$a',type,
    'oppositeCategory$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_oppositeCategory$a',axiom,
    'oppositeCategory$a'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_functor_ext$',type,
    'functor_ext$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$' * 'B_ZF_fun$' * 'Unit$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_functor_ext$',axiom,
    'functor_ext$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1','fmb_B_ZF_fun$_1','fmb_Unit$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_homFtorContra$a',type,
    'homFtorContra$a': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_homFtorContra$a',axiom,
    'homFtorContra$a'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_A$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_homFtorContra$',type,
    'homFtorContra$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_homFtorContra$',axiom,
    'homFtorContra$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_A$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_nTCod$a',type,
    'nTCod$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ).

tff('function_nTCod$a',axiom,
    'nTCod$a'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1' ).

tff('declare_extensional$e',type,
    'extensional$e': 'A_set$' > 'A_b_fun_set$' ).

tff('function_extensional$e',axiom,
    'extensional$e'('fmb_A_set$_1') = 'fmb_A_b_fun_set$_1' ).

tff('declare_collect$b',type,
    'collect$b': 'B_bool_fun$' > 'B_set$' ).

tff('function_collect$b',axiom,
    'collect$b'('fmb_B_bool_fun$_1') = 'fmb_B_set$_1' ).

tff('declare_cod$b',type,
    'cod$b': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_cod$b',axiom,
    'cod$b'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_compDefined$a',type,
    'compDefined$a': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'B$' ) > 'B_bool_fun$' ).

tff('function_compDefined$a',axiom,
    'compDefined$a'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_B$_1') = 'fmb_B_bool_fun$_1' ).

tff('declare_inverse_rel$a',type,
    'inverse_rel$a': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'B$' ) > 'B_bool_fun$' ).

tff('function_inverse_rel$a',axiom,
    'inverse_rel$a'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_B$_1') = 'fmb_B_bool_fun$_1' ).

tff('declare_the$',type,
    'the$': 'ZF_bool_fun$' > 'ZF$' ).

tff('function_the$',axiom,
    'the$'('fmb_ZF_bool_fun$_1') = 'fmb_ZF$_1' ).

tff('declare_nTCatDom$c',type,
    'nTCatDom$c': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_unit_Category_ext$' ).

tff('function_nTCatDom$c',axiom,
    'nTCatDom$c'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_catCod$e',type,
    'catCod$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_catCod$e',axiom,
    'catCod$e'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_catCod$b',type,
    'catCod$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$' ).

tff('function_catCod$b',axiom,
    'catCod$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_constFunctor$a',type,
    'constFunctor$a': ( 'ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$' * 'ZF$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ).

tff('function_constFunctor$a',axiom,
    'constFunctor$a'('fmb_ZF_ZF_unit_Category_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1','fmb_ZF$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1' ).

tff('declare_uuf$',type,
    'uuf$': 'A_b_fun_set$' > 'A_b_fun_bool_fun$' ).

tff('function_uuf$',axiom,
    'uuf$'('fmb_A_b_fun_set$_1') = 'fmb_A_b_fun_bool_fun$_1' ).

tff('declare_nTDom_update$',type,
    'nTDom_update$': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('function_nTDom_update$',axiom,
    'nTDom_update$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ).

tff('declare_catCod$f',type,
    'catCod$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_catCod$f',axiom,
    'catCod$f'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_objIso$',type,
    'objIso$': ( 'ZF_ZF_unit_Category_ext$' * 'ZF$' ) > 'ZF_bool_fun$' ).

tff('function_objIso$',axiom,
    'objIso$'('fmb_ZF_ZF_unit_Category_ext$_1','fmb_ZF$_1') = 'fmb_ZF_bool_fun$_1' ).

tff('declare_oppositeCategory$c',type,
    'oppositeCategory$c': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_oppositeCategory$c',axiom,
    'oppositeCategory$c'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_cod_update$',type,
    'cod_update$': 'ZF_ZF_fun_ZF_ZF_fun_fun$' > 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' ).

tff('function_cod_update$',axiom,
    'cod_update$'('fmb_ZF_ZF_fun_ZF_ZF_fun_fun$_1') = 'fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1' ).

tff('declare_lSCategory_ext$',type,
    'lSCategory_ext$': ( 'B_ZF_fun$' * 'C$' ) > 'B_c_LSCategory_ext$' ).

tff('function_lSCategory_ext$',axiom,
    'lSCategory_ext$'('fmb_B_ZF_fun$_1','fmb_C$_1') = 'fmb_B_c_LSCategory_ext$_1' ).

tff('declare_identityFunctor$a',type,
    'identityFunctor$a': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ).

tff('function_identityFunctor$a',axiom,
    'identityFunctor$a'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1' ).

tff('declare_collect$h',type,
    'collect$h': 'A_b_fun_bool_fun$' > 'A_b_fun_set$' ).

tff('function_collect$h',axiom,
    'collect$h'('fmb_A_b_fun_bool_fun$_1') = 'fmb_A_b_fun_set$_1' ).

tff('declare_natTransComp$b',type,
    'natTransComp$b': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('function_natTransComp$b',axiom,
    'natTransComp$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_comp$b',type,
    'comp$b': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('function_comp$b',axiom,
    'comp$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_mor_update$',type,
    'mor_update$': 'ZF_set_ZF_set_fun$' > 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' ).

tff('function_mor_update$',axiom,
    'mor_update$'('fmb_ZF_set_ZF_set_fun$_1') = 'fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1' ).

tff('declare_catCod$a',type,
    'catCod$a': 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' > 'Unit_unit_unit_Category_ext$' ).

tff('function_catCod$a',axiom,
    'catCod$a'('fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1') = 'fmb_Unit_unit_unit_Category_ext$_1' ).

tff('declare_natTransMap$a',type,
    'natTransMap$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_fun$' ).

tff('function_natTransMap$a',axiom,
    'natTransMap$a'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_cod$a',type,
    'cod$a': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_a_fun$' ).

tff('function_cod$a',axiom,
    'cod$a'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_B_a_fun$_1' ).

tff('declare_functor_ext$a',type,
    'functor_ext$a': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' * 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'Unit$' ) > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_functor_ext$a',axiom,
    'functor_ext$a'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1','fmb_B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1','fmb_Unit$_1') = 'fmb_A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_nTCatCod$e',type,
    'nTCatCod$e': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_nTCatCod$e',axiom,
    'nTCatCod$e'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_fun_app$w',type,
    'fun_app$w': ( 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' * 'ZF_ZF_unit_Category_ext$' ) > 'ZF_ZF_unit_Category_ext$' ).

tff('function_fun_app$w',axiom,
    'fun_app$w'('fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1','fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_mapO$',type,
    'mapO$': ( 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'ZF$' ) > 'A$' ).

tff('function_mapO$',axiom,
    'mapO$'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$_1','fmb_ZF$_1') = 'fmb_A$_1' ).

tff('declare_nTDom$b',type,
    'nTDom$b': 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' > 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' ).

tff('function_nTDom$b',axiom,
    'nTDom$b'('fmb_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1' ).

tff('declare_uul$',type,
    'uul$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' ) > 'B_ZF_fun$' ).

tff('function_uul$',axiom,
    'uul$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_A$_1') = 'fmb_B_ZF_fun$_1' ).

tff('declare_identityFunctor$',type,
    'identityFunctor$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ).

tff('function_identityFunctor$',axiom,
    'identityFunctor$'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1' ).

tff('declare_restrict$e',type,
    'restrict$e': ( 'A_b_fun$' * 'A_set$' ) > 'A_b_fun$' ).

tff('function_restrict$e',axiom,
    'restrict$e'('fmb_A_b_fun$_1','fmb_A_set$_1') = 'fmb_A_b_fun$_1' ).

tff('declare_category_ext$a',type,
    'category_ext$a': ( 'ZF_set$' * 'ZF_set$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$' * 'ZF_ZF_fun$' * 'ZF_ZF_ZF_fun_fun$' * 'Unit$' ) > 'ZF_ZF_unit_Category_ext$' ).

tff('function_category_ext$a',axiom,
    'category_ext$a'('fmb_ZF_set$_1','fmb_ZF_set$_1','fmb_ZF_ZF_fun$_1','fmb_ZF_ZF_fun$_1','fmb_ZF_ZF_fun$_1','fmb_ZF_ZF_ZF_fun_fun$_1','fmb_Unit$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_constFunctor$',type,
    'constFunctor$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$' * 'ZF$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_constFunctor$',axiom,
    'constFunctor$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1','fmb_ZF$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_homFtorMap$',type,
    'homFtorMap$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' ) > 'B_ZF_fun$' ).

tff('function_homFtorMap$',axiom,
    'homFtorMap$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_A$_1') = 'fmb_B_ZF_fun$_1' ).

tff('declare_collect$f',type,
    'collect$f': 'B_a_fun_bool_fun$' > 'B_a_fun_set$' ).

tff('function_collect$f',axiom,
    'collect$f'('fmb_B_a_fun_bool_fun$_1') = 'fmb_B_a_fun_set$_1' ).

tff('declare_makeNT$a',type,
    'makeNT$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('function_makeNT$a',axiom,
    'makeNT$a'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_inverse$',type,
    'inverse$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$' ).

tff('function_inverse$',axiom,
    'inverse$'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_restrict$',type,
    'restrict$': ( 'ZF_ZF_prod_ZF_fun$' * 'ZF_ZF_prod_set$' * 'ZF_ZF_prod$' ) > 'ZF$' ).

tff('function_restrict$',axiom,
    'restrict$'('fmb_ZF_ZF_prod_ZF_fun$_1','fmb_ZF_ZF_prod_set$_1','fmb_ZF_ZF_prod$_1') = 'fmb_ZF$_1' ).

tff('declare_fun_app$t',type,
    'fun_app$t': ( 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'B$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('function_fun_app$t',axiom,
    'fun_app$t'('fmb_B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1','fmb_B$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ).

tff('declare_extensional$a',type,
    'extensional$a': 'A_set$' > 'A_ZF_fun_set$' ).

tff('function_extensional$a',axiom,
    'extensional$a'('fmb_A_set$_1') = 'fmb_A_ZF_fun_set$_1' ).

tff('declare_nTCatDom$a',type,
    'nTCatDom$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_unit_Category_ext$' ).

tff('function_nTCatDom$a',axiom,
    'nTCatDom$a'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_zF2mor$',type,
    'zF2mor$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF$' ) > 'B$' ).

tff('function_zF2mor$',axiom,
    'zF2mor$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_ZF$_1') = 'fmb_B$_1' ).

tff('declare_fun_app$x',type,
    'fun_app$x': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('function_fun_app$x',axiom,
    'fun_app$x'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ).

tff('declare_collect$j',type,
    'collect$j': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$' ).

tff('function_collect$j',axiom,
    'collect$j'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$_1' ).

tff('declare_uub$',type,
    'uub$': 'A_set$' > 'A_bool_fun$' ).

tff('function_uub$',axiom,
    'uub$'('fmb_A_set$_1') = 'fmb_A_bool_fun$_1' ).

tff('declare_fun_app$af',type,
    'fun_app$af': ( 'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$' * 'ZF_ZF_ZF_fun_fun$' ) > 'ZF_ZF_ZF_fun_fun$' ).

tff('function_fun_app$af',axiom,
    'fun_app$af'('fmb_ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$_1','fmb_ZF_ZF_ZF_fun_fun$_1') = 'fmb_ZF_ZF_ZF_fun_fun$_1' ).

tff('declare_uux$',type,
    'uux$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_b_b_fun_fun$' ).

tff('function_uux$',axiom,
    'uux$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_B_b_b_fun_fun$_1' ).

tff('declare_uui$',type,
    'uui$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' ).

tff('function_uui$',axiom,
    'uui$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1' ).

tff('declare_category_ext$b',type,
    'category_ext$b': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$' * 'Unit$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_category_ext$b',axiom,
    'category_ext$b'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$_1','fmb_Unit$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_dom$',type,
    'dom$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_a_fun$' ).

tff('function_dom$',axiom,
    'dom$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_B_a_fun$_1' ).

tff('declare_more$d',type,
    'more$d': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_c_LSCategory_ext$' ).

tff('function_more$d',axiom,
    'more$d'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_B_c_LSCategory_ext$_1' ).

tff('declare_collect$c',type,
    'collect$c': 'ZF_bool_fun$' > 'ZF_set$' ).

tff('function_collect$c',axiom,
    'collect$c'('fmb_ZF_bool_fun$_1') = 'fmb_ZF_set$_1' ).

tff('declare_fun_app$ae',type,
    'fun_app$ae': ( 'B_set_b_set_fun$' * 'B_set$' ) > 'B_set$' ).

tff('function_fun_app$ae',axiom,
    'fun_app$ae'('fmb_B_set_b_set_fun$_1','fmb_B_set$_1') = 'fmb_B_set$_1' ).

tff('declare_mapM$f',type,
    'mapM$f': ( 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'B$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('function_mapM$f',axiom,
    'mapM$f'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1','fmb_B$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_isomorphism$a',type,
    'isomorphism$a': 'ZF_ZF_unit_Category_ext$' > 'ZF_bool_fun$' ).

tff('function_isomorphism$a',axiom,
    'isomorphism$a'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_bool_fun$_1' ).

tff('declare_nTCod_update$',type,
    'nTCod_update$': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('function_nTCod_update$',axiom,
    'nTCod_update$'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_hOMCollection$',type,
    'hOMCollection$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' * 'A$' ) > 'ZF_set$' ).

tff('function_hOMCollection$',axiom,
    'hOMCollection$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_A$_1','fmb_A$_1') = 'fmb_ZF_set$_1' ).

tff('declare_uuw$',type,
    'uuw$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_b_prod_bool_fun$' ).

tff('function_uuw$',axiom,
    'uuw$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_B_b_prod_bool_fun$_1' ).

tff('declare_uuh$',type,
    'uuh$': 'B_b_prod_set$' > 'B_b_prod_bool_fun$' ).

tff('function_uuh$',axiom,
    'uuh$'('fmb_B_b_prod_set$_1') = 'fmb_B_b_prod_bool_fun$_1' ).

tff('declare_comp$',type,
    'comp$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_ZF_fun_fun$' ).

tff('function_comp$',axiom,
    'comp$'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_ZF_fun_fun$_1' ).

tff('declare_isomorphism$',type,
    'isomorphism$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_bool_fun$' ).

tff('function_isomorphism$',axiom,
    'isomorphism$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_B_bool_fun$_1' ).

tff('declare_makeNT$',type,
    'makeNT$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('function_makeNT$',axiom,
    'makeNT$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ).

tff('declare_fun_app$o',type,
    'fun_app$o': ( 'B_ZF_fun$' * 'B$' ) > 'ZF$' ).

tff('function_fun_app$o',axiom,
    'fun_app$o'('fmb_B_ZF_fun$_1','fmb_B$_1') = 'fmb_ZF$_1' ).

tff('declare_catDom$e',type,
    'catDom$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > 'ZF_ZF_unit_Category_ext$' ).

tff('function_catDom$e',axiom,
    'catDom$e'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$_1') = 'fmb_ZF_ZF_unit_Category_ext$_1' ).

tff('declare_inverse$a',type,
    'inverse$a': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'B$' ) > 'B$' ).

tff('function_inverse$a',axiom,
    'inverse$a'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_B$_1') = 'fmb_B$_1' ).

tff('declare_mapM$b',type,
    'mapM$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_fun$' ).

tff('function_mapM$b',axiom,
    'mapM$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_fun_app$ad',type,
    'fun_app$ad': ( 'ZF_set_ZF_set_fun$' * 'ZF_set$' ) > 'ZF_set$' ).

tff('function_fun_app$ad',axiom,
    'fun_app$ad'('fmb_ZF_set_ZF_set_fun$_1','fmb_ZF_set$_1') = 'fmb_ZF_set$_1' ).

tff('declare_fun_app$aa',type,
    'fun_app$aa': ( 'Unit_unit_fun$' * 'Unit$' ) > 'Unit$' ).

tff('function_fun_app$aa',axiom,
    'fun_app$aa'('fmb_Unit_unit_fun$_1','fmb_Unit$_1') = 'fmb_Unit$_1' ).

tff('declare_obj$',type,
    'obj$': 'ZF_ZF_unit_Category_ext$' > 'ZF_set$' ).

tff('function_obj$',axiom,
    'obj$'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_set$_1' ).

tff('declare_homFtorMapContra$',type,
    'homFtorMapContra$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'B$' ) > 'A_ZF_fun$' ).

tff('function_homFtorMapContra$',axiom,
    'homFtorMapContra$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_B$_1') = 'fmb_A_ZF_fun$_1' ).

tff('declare_elem$',type,
    'elem$': 'ZF$' > 'ZF_bool_fun$' ).

tff('function_elem$',axiom,
    'elem$'('fmb_ZF$_1') = 'fmb_ZF_bool_fun$_1' ).

tff('declare_comp$a',type,
    'comp$a': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_b_b_fun_fun$' ).

tff('function_comp$a',axiom,
    'comp$a'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_B_b_b_fun_fun$_1' ).

tff('declare_yFtorNT$',type,
    'yFtorNT$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'B$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('function_yFtorNT$',axiom,
    'yFtorNT$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_B$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ).

tff('declare_nTCatCod$f',type,
    'nTCatCod$f': 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' > 'Unit_unit_unit_Category_ext$' ).

tff('function_nTCatCod$f',axiom,
    'nTCatCod$f'('fmb_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$_1') = 'fmb_Unit_unit_unit_Category_ext$_1' ).

tff('declare_fun_app$v',type,
    'fun_app$v': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_fun_app$v',axiom,
    'fun_app$v'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_nTDom$d',type,
    'nTDom$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' ).

tff('function_nTDom$d',axiom,
    'nTDom$d'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1') = 'fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$_1' ).

tff('declare_catExp$b',type,
    'catExp$b': ( 'ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_catExp$b',axiom,
    'catExp$b'('fmb_ZF_ZF_unit_Category_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_more_update$a',type,
    'more_update$a': 'Unit_unit_fun$' > 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' ).

tff('function_more_update$a',axiom,
    'more_update$a'('fmb_Unit_unit_fun$_1') = 'fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1' ).

tff('declare_catDom$d',type,
    'catDom$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('function_catDom$d',axiom,
    'catDom$d'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_fun_app$',type,
    'fun_app$': ( 'ZF_ZF_fun$' * 'ZF$' ) > 'ZF$' ).

tff('function_fun_app$',axiom,
    'fun_app$'('fmb_ZF_ZF_fun$_1','fmb_ZF$_1') = 'fmb_ZF$_1' ).

tff('declare_comp$d',type,
    'comp$d': 'ZF_ZF_fun$' > 'ZF_ZF_fun_ZF_ZF_fun_fun$' ).

tff('function_comp$d',axiom,
    'comp$d'('fmb_ZF_ZF_fun$_1') = 'fmb_ZF_ZF_fun_ZF_ZF_fun_fun$_1' ).

tff('declare_mapO$c',type,
    'mapO$c': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' > 'A_ZF_fun$' ).

tff('function_mapO$c',axiom,
    'mapO$c'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') = 'fmb_A_ZF_fun$_1' ).

tff('declare_constFunctor$b',type,
    'constFunctor$b': ( 'ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$' * 'ZF$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ).

tff('function_constFunctor$b',axiom,
    'constFunctor$b'('fmb_ZF_ZF_unit_Category_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1','fmb_ZF$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1' ).

tff('declare_collect$i',type,
    'collect$i': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$' ).

tff('function_collect$i',axiom,
    'collect$i'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$_1' ).

tff('declare_yFtorNT$a',type,
    'yFtorNT$a': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' ).

tff('function_yFtorNT$a',axiom,
    'yFtorNT$a'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1' ).

tff('declare_mapsTo$a',type,
    'mapsTo$a': ( 'ZF_ZF_unit_Category_ext$' * 'ZF$' * 'ZF$' ) > 'ZF_bool_fun$' ).

tff('function_mapsTo$a',axiom,
    'mapsTo$a'('fmb_ZF_ZF_unit_Category_ext$_1','fmb_ZF$_1','fmb_ZF$_1') = 'fmb_ZF_bool_fun$_1' ).

tff('declare_mapM$c',type,
    'mapM$c': ( 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'ZF$' ) > 'B$' ).

tff('function_mapM$c',axiom,
    'mapM$c'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$_1','fmb_ZF$_1') = 'fmb_B$_1' ).

tff('declare_mor$a',type,
    'mor$a': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$' > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$' ).

tff('function_mor$a',axiom,
    'mor$a'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_Category_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$_1' ).

tff('declare_extensional$',type,
    'extensional$': 'ZF_set$' > 'ZF_ZF_fun_set$' ).

tff('function_extensional$',axiom,
    'extensional$'('fmb_ZF_set$_1') = 'fmb_ZF_ZF_fun_set$_1' ).

tff('declare_natTransComp$a',type,
    'natTransComp$a': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('function_natTransComp$a',axiom,
    'natTransComp$a'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ).

tff('declare_uug$',type,
    'uug$': 'ZF_ZF_prod_set$' > 'ZF_ZF_prod_bool_fun$' ).

tff('function_uug$',axiom,
    'uug$'('fmb_ZF_ZF_prod_set$_1') = 'fmb_ZF_ZF_prod_bool_fun$_1' ).

tff('declare_id$a',type,
    'id$a': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$' ).

tff('function_id$a',axiom,
    'id$a'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_image$',type,
    'image$': ( 'ZF_ZF_set_fun$' * 'ZF_set$' ) > 'ZF_set_set$' ).

tff('function_image$',axiom,
    'image$'('fmb_ZF_ZF_set_fun$_1','fmb_ZF_set$_1') = 'fmb_ZF_set_set$_1' ).

tff('declare_restrict$b',type,
    'restrict$b': ( 'B_ZF_fun$' * 'B_set$' ) > 'B_ZF_fun$' ).

tff('function_restrict$b',axiom,
    'restrict$b'('fmb_B_ZF_fun$_1','fmb_B_set$_1') = 'fmb_B_ZF_fun$_1' ).

tff('declare_uuj$',type,
    'uuj$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_b_b_fun_fun$' ).

tff('function_uuj$',axiom,
    'uuj$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_B_b_b_fun_fun$_1' ).

tff('declare_id_update$',type,
    'id_update$': 'ZF_ZF_fun_ZF_ZF_fun_fun$' > 'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$' ).

tff('function_id_update$',axiom,
    'id_update$'('fmb_ZF_ZF_fun_ZF_ZF_fun_fun$_1') = 'fmb_ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$_1' ).

tff('declare_yFtor$',type,
    'yFtor$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_yFtor$',axiom,
    'yFtor$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_A_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_b_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_homFtor$a',type,
    'homFtor$a': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ).

tff('function_homFtor$a',axiom,
    'homFtor$a'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_A$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1' ).

tff('declare_idNatTrans$a',type,
    'idNatTrans$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ).

tff('function_idNatTrans$a',axiom,
    'idNatTrans$a'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1' ).

tff('declare_cod$',type,
    'cod$': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$' ).

tff('function_cod$',axiom,
    'cod$'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_pair$',type,
    'pair$': ( 'ZF$' * 'ZF$' ) > 'ZF_ZF_prod$' ).

tff('function_pair$',axiom,
    'pair$'('fmb_ZF$_1','fmb_ZF$_1') = 'fmb_ZF_ZF_prod$_1' ).

tff('declare_nTCod$d',type,
    'nTCod$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' ).

tff('function_nTCod$d',axiom,
    'nTCod$d'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1') = 'fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$_1' ).

tff('declare_makeCat$b',type,
    'makeCat$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_makeCat$b',axiom,
    'makeCat$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_nTCod$b',type,
    'nTCod$b': 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' > 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' ).

tff('function_nTCod$b',axiom,
    'nTCod$b'('fmb_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1' ).

tff('declare_homSet$',type,
    'homSet$': ( 'A_b_b_c_LSCategory_ext_Category_ext$' * 'A$' ) > 'A_ZF_fun$' ).

tff('function_homSet$',axiom,
    'homSet$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_A$_1') = 'fmb_A_ZF_fun$_1' ).

tff('declare_uue$',type,
    'uue$': 'A_ZF_fun_set$' > 'A_ZF_fun_bool_fun$' ).

tff('function_uue$',axiom,
    'uue$'('fmb_A_ZF_fun_set$_1') = 'fmb_A_ZF_fun_bool_fun$_1' ).

tff('declare_collect$g',type,
    'collect$g': 'A_ZF_fun_bool_fun$' > 'A_ZF_fun_set$' ).

tff('function_collect$g',axiom,
    'collect$g'('fmb_A_ZF_fun_bool_fun$_1') = 'fmb_A_ZF_fun_set$_1' ).

tff('declare_nTCatDom$',type,
    'nTCatDom$': 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('function_nTCatDom$',axiom,
    'nTCatDom$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_fun_app$y',type,
    'fun_app$y': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ).

tff('function_fun_app$y',axiom,
    'fun_app$y'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1' ).

tff('declare_mapO$d',type,
    'mapO$d': ( 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' * 'ZF$' ) > 'Unit$' ).

tff('function_mapO$d',axiom,
    'mapO$d'('fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1','fmb_ZF$_1') = 'fmb_Unit$_1' ).

tff('declare_mor$b',type,
    'mor$b': 'ZF_ZF_unit_Category_ext$' > 'ZF_set$' ).

tff('function_mor$b',axiom,
    'mor$b'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_set$_1' ).

tff('declare_nTCatCod$c',type,
    'nTCatCod$c': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' ).

tff('function_nTCatCod$c',axiom,
    'nTCatCod$c'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1' ).

tff('declare_natTransComp$e',type,
    'natTransComp$e': ( 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' ) > 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' ).

tff('function_natTransComp$e',axiom,
    'natTransComp$e'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1','fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1') = 'fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1' ).

tff('declare_uuc$',type,
    'uuc$': 'B_ZF_fun_set$' > 'B_ZF_fun_bool_fun$' ).

tff('function_uuc$',axiom,
    'uuc$'('fmb_B_ZF_fun_set$_1') = 'fmb_B_ZF_fun_bool_fun$_1' ).

tff('declare_nTCatCod$b',type,
    'nTCatCod$b': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('function_nTCatCod$b',axiom,
    'nTCatCod$b'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_dom$a',type,
    'dom$a': 'ZF_ZF_unit_Category_ext$' > 'ZF_ZF_fun$' ).

tff('function_dom$a',axiom,
    'dom$a'('fmb_ZF_ZF_unit_Category_ext$_1') = 'fmb_ZF_ZF_fun$_1' ).

tff('declare_nTCatDom$e',type,
    'nTCatDom$e': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > 'A_b_b_c_LSCategory_ext_Category_ext$' ).

tff('function_nTCatDom$e',axiom,
    'nTCatDom$e'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') = 'fmb_A_b_b_c_LSCategory_ext_Category_ext$_1' ).

tff('declare_comp$c',type,
    'comp$c': ( 'Unit_unit_unit_Category_ext$' * 'Unit$' ) > 'Unit_unit_fun$' ).

tff('function_comp$c',axiom,
    'comp$c'('fmb_Unit_unit_unit_Category_ext$_1','fmb_Unit$_1') = 'fmb_Unit_unit_fun$_1' ).

tff('declare_mapO$a',type,
    'mapO$a': ( 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' * 'A$' ) > 'A$' ).

tff('function_mapO$a',axiom,
    'mapO$a'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$_1','fmb_A$_1') = 'fmb_A$_1' ).

tff('declare_mapO$e',type,
    'mapO$e': ( 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' * 'ZF$' ) > 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ).

tff('function_mapO$e',axiom,
    'mapO$e'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$_1','fmb_ZF$_1') = 'fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1' ).

tff('declare_mor$',type,
    'mor$': 'A_b_b_c_LSCategory_ext_Category_ext$' > 'B_set$' ).

tff('function_mor$',axiom,
    'mor$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') = 'fmb_B_set$_1' ).

tff('declare_member$j',type,
    'member$j': ( 'ZF_ZF_fun$' * 'ZF_ZF_fun_set$' ) > $o ).

tff('predicate_member$j',axiom,
    'member$j'('fmb_ZF_ZF_fun$_1','fmb_ZF_ZF_fun_set$_1') ).

tff('declare_member$n',type,
    'member$n': ( 'B_b_prod_b_fun$' * 'B_b_prod_b_fun_set$' ) > $o ).

tff('predicate_member$n',axiom,
    ~ 'member$n'('fmb_B_b_prod_b_fun$_1','fmb_B_b_prod_b_fun_set$_1') ).

tff('declare_fun_app$e',type,
    'fun_app$e': ( 'B_ZF_fun_bool_fun$' * 'B_ZF_fun$' ) > $o ).

tff('predicate_fun_app$e',axiom,
    'fun_app$e'('fmb_B_ZF_fun_bool_fun$_1','fmb_B_ZF_fun$_1') ).

tff('declare_extCategory$',type,
    'extCategory$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o ).

tff('predicate_extCategory$',axiom,
    ~ 'extCategory$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') ).

tff('declare_functor_comp_def$c',type,
    'functor_comp_def$c': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ) > $o ).

tff('predicate_functor_comp_def$c',axiom,
    'functor_comp_def$c'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') ).

tff('declare_lSCategory$',type,
    'lSCategory$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o ).

tff('predicate_lSCategory$',axiom,
    'lSCategory$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') ).

tff('declare_fun_app$a',type,
    'fun_app$a': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' ) > $o ).

tff('predicate_fun_app$a',axiom,
    'fun_app$a'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') ).

tff('declare_member$f',type,
    'member$f': ( 'A_ZF_fun$' * 'A_ZF_fun_set$' ) > $o ).

tff('predicate_member$f',axiom,
    'member$f'('fmb_A_ZF_fun$_1','fmb_A_ZF_fun_set$_1') ).

tff('declare_functor_comp_def$b',type,
    'functor_comp_def$b': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ) > $o ).

tff('predicate_functor_comp_def$b',axiom,
    'functor_comp_def$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') ).

tff('declare_natTransP$f',type,
    'natTransP$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > $o ).

tff('predicate_natTransP$f',axiom,
    ~ 'natTransP$f'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') ).

tff('declare_fun_app$q',type,
    'fun_app$q': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > $o ).

tff('predicate_fun_app$q',axiom,
    'fun_app$q'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') ).

tff('declare_fun_app$b',type,
    'fun_app$b': ( 'ZF_ZF_prod_bool_fun$' * 'ZF_ZF_prod$' ) > $o ).

tff('predicate_fun_app$b',axiom,
    'fun_app$b'('fmb_ZF_ZF_prod_bool_fun$_1','fmb_ZF_ZF_prod$_1') ).

tff('declare_category$a',type,
    'category$a': 'ZF_ZF_unit_Category_ext$' > $o ).

tff('predicate_category$a',axiom,
    'category$a'('fmb_ZF_ZF_unit_Category_ext$_1') ).

tff('declare_functor_comp_def$a',type,
    'functor_comp_def$a': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' ) > $o ).

tff('predicate_functor_comp_def$a',axiom,
    'functor_comp_def$a'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1','fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1') ).

tff('declare_category$b',type,
    'category$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > $o ).

tff('predicate_category$b',axiom,
    'category$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1') ).

tff('declare_functorM_axioms$',type,
    'functorM_axioms$': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o ).

tff('predicate_functorM_axioms$',axiom,
    'functorM_axioms$'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') ).

tff('declare_functorExt$',type,
    'functorExt$': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o ).

tff('predicate_functorExt$',axiom,
    'functorExt$'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') ).

tff('declare_category$',type,
    'category$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o ).

tff('predicate_category$',axiom,
    'category$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') ).

tff('declare_nTCompDefined$',type,
    'nTCompDefined$': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ) > $o ).

tff('predicate_nTCompDefined$',axiom,
    'nTCompDefined$'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') ).

tff('declare_equivalence$',type,
    'equivalence$': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o ).

tff('predicate_equivalence$',axiom,
    ~ 'equivalence$'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') ).

tff('declare_member$m',type,
    'member$m': ( 'ZF_ZF_prod_ZF_fun$' * 'ZF_ZF_prod_ZF_fun_set$' ) > $o ).

tff('predicate_member$m',axiom,
    'member$m'('fmb_ZF_ZF_prod_ZF_fun$_1','fmb_ZF_ZF_prod_ZF_fun_set$_1') ).

tff('declare_natTrans$a',type,
    'natTrans$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > $o ).

tff('predicate_natTrans$a',axiom,
    'natTrans$a'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') ).

tff('declare_fun_app$d',type,
    'fun_app$d': ( 'ZF_bool_fun$' * 'ZF$' ) > $o ).

tff('predicate_fun_app$d',axiom,
    'fun_app$d'('fmb_ZF_bool_fun$_1','fmb_ZF$_1') ).

tff('declare_natTransP$e',type,
    'natTransP$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' > $o ).

tff('predicate_natTransP$e',axiom,
    ~ 'natTransP$e'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1') ).

tff('declare_nTCompDefined$b',type,
    'nTCompDefined$b': ( 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' ) > $o ).

tff('predicate_nTCompDefined$b',axiom,
    ~ 'nTCompDefined$b'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1','fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1') ).

tff('declare_member$c',type,
    'member$c': ( 'ZF$' * 'ZF_set$' ) > $o ).

tff('predicate_member$c',axiom,
    'member$c'('fmb_ZF$_1','fmb_ZF_set$_1') ).

tff('declare_member$g',type,
    'member$g': ( 'A_b_fun$' * 'A_b_fun_set$' ) > $o ).

tff('predicate_member$g',axiom,
    ~ 'member$g'('fmb_A_b_fun$_1','fmb_A_b_fun_set$_1') ).

tff('declare_compDefined$c',type,
    'compDefined$c': ( 'Unit_unit_unit_Category_ext$' * 'Unit$' * 'Unit$' ) > $o ).

tff('predicate_compDefined$c',axiom,
    'compDefined$c'('fmb_Unit_unit_unit_Category_ext$_1','fmb_Unit$_1','fmb_Unit$_1') ).

tff('declare_natTransP$b',type,
    'natTransP$b': 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' > $o ).

tff('predicate_natTransP$b',axiom,
    'natTransP$b'('fmb_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$_1') ).

tff('declare_functor_comp_def$',type,
    'functor_comp_def$': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' ) > $o ).

tff('predicate_functor_comp_def$',axiom,
    'functor_comp_def$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1','fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1') ).

tff('declare_functor$d',type,
    'functor$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' > $o ).

tff('predicate_functor$d',axiom,
    ~ 'functor$d'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$_1') ).

tff('declare_functor$f',type,
    'functor$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$' > $o ).

tff('predicate_functor$f',axiom,
    ~ 'functor$f'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_Functor_ext$_1') ).

tff('declare_category_axioms$b',type,
    'category_axioms$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' > $o ).

tff('predicate_category_axioms$b',axiom,
    'category_axioms$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1') ).

tff('declare_lSCategory_axioms$',type,
    'lSCategory_axioms$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o ).

tff('predicate_lSCategory_axioms$',axiom,
    'lSCategory_axioms$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') ).

tff('declare_member$e',type,
    'member$e': ( 'B_a_fun$' * 'B_a_fun_set$' ) > $o ).

tff('predicate_member$e',axiom,
    ~ 'member$e'('fmb_B_a_fun$_1','fmb_B_a_fun_set$_1') ).

tff('declare_nTCompDefined$e',type,
    'nTCompDefined$e': ( 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' ) > $o ).

tff('predicate_nTCompDefined$e',axiom,
    ~ 'nTCompDefined$e'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1','fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') ).

tff('declare_fun_app$c',type,
    'fun_app$c': ( 'B_b_prod_bool_fun$' * 'B_b_prod$' ) > $o ).

tff('predicate_fun_app$c',axiom,
    'fun_app$c'('fmb_B_b_prod_bool_fun$_1','fmb_B_b_prod$_1') ).

tff('declare_natTrans$e',type,
    'natTrans$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' > $o ).

tff('predicate_natTrans$e',axiom,
    ~ 'natTrans$e'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1') ).

tff('declare_functor_abbrev$b',type,
    'functor_abbrev$b': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_unit_Category_ext$' * 'ZF_ZF_unit_Category_ext$' ) > $o ).

tff('predicate_functor_abbrev$b',axiom,
    'functor_abbrev$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1') ).

tff('declare_nt_abbrev$b',type,
    'nt_abbrev$b': ( 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' * 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' ) > $o ).

tff('predicate_nt_abbrev$b',axiom,
    ~ 'nt_abbrev$b'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1','fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$_1','fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$_1') ).

tff('declare_fun_app$g',type,
    'fun_app$g': ( 'A_ZF_fun_bool_fun$' * 'A_ZF_fun$' ) > $o ).

tff('predicate_fun_app$g',axiom,
    'fun_app$g'('fmb_A_ZF_fun_bool_fun$_1','fmb_A_ZF_fun$_1') ).

tff('declare_extCategory$a',type,
    'extCategory$a': 'ZF_ZF_unit_Category_ext$' > $o ).

tff('predicate_extCategory$a',axiom,
    'extCategory$a'('fmb_ZF_ZF_unit_Category_ext$_1') ).

tff('declare_category_axioms$',type,
    'category_axioms$': 'A_b_b_c_LSCategory_ext_Category_ext$' > $o ).

tff('predicate_category_axioms$',axiom,
    'category_axioms$'('fmb_A_b_b_c_LSCategory_ext_Category_ext$_1') ).

tff('declare_functor_abbrev$',type,
    'functor_abbrev$': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_b_b_c_LSCategory_ext_Category_ext$' * 'ZF_ZF_unit_Category_ext$' ) > $o ).

tff('predicate_functor_abbrev$',axiom,
    'functor_abbrev$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1','fmb_A_b_b_c_LSCategory_ext_Category_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1') ).

tff('declare_natTransExt$',type,
    'natTransExt$': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > $o ).

tff('predicate_natTransExt$',axiom,
    'natTransExt$'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') ).

tff('declare_functorM$',type,
    'functorM$': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o ).

tff('predicate_functorM$',axiom,
    'functorM$'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') ).

tff('declare_natTransP$d',type,
    'natTransP$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o ).

tff('predicate_natTransP$d',axiom,
    ~ 'natTransP$d'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1') ).

tff('declare_natTrans$b',type,
    'natTrans$b': 'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$' > $o ).

tff('predicate_natTrans$b',axiom,
    'natTrans$b'('fmb_ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$_1') ).

tff('declare_mapsTo$c',type,
    'mapsTo$c': ( 'Unit_unit_unit_Category_ext$' * 'Unit$' * 'Unit$' * 'Unit$' ) > $o ).

tff('predicate_mapsTo$c',axiom,
    'mapsTo$c'('fmb_Unit_unit_unit_Category_ext$_1','fmb_Unit$_1','fmb_Unit$_1','fmb_Unit$_1') ).

tff('declare_natTrans$c',type,
    'natTrans$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o ).

tff('predicate_natTrans$c',axiom,
    ~ 'natTrans$c'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1') ).

tff('declare_fun_app$j',type,
    'fun_app$j': ( 'A_bool_fun$' * 'A$' ) > $o ).

tff('predicate_fun_app$j',axiom,
    'fun_app$j'('fmb_A_bool_fun$_1','fmb_A$_1') ).

tff('declare_functor$b',type,
    'functor$b': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o ).

tff('predicate_functor$b',axiom,
    'functor$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') ).

tff('declare_compDefined$b',type,
    'compDefined$b': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' ) > $o ).

tff('predicate_compDefined$b',axiom,
    ~ 'compDefined$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') ).

tff('declare_functor_abbrev$a',type,
    'functor_abbrev$a': ( 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' * 'ZF_ZF_unit_Category_ext$' * 'Unit_unit_unit_Category_ext$' ) > $o ).

tff('predicate_functor_abbrev$a',axiom,
    'functor_abbrev$a'('fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1','fmb_ZF_ZF_unit_Category_ext$_1','fmb_Unit_unit_unit_Category_ext$_1') ).

tff('declare_functor$e',type,
    'functor$e': 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$' > $o ).

tff('predicate_functor$e',axiom,
    ~ 'functor$e'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$_1') ).

tff('declare_natTrans$d',type,
    'natTrans$d': 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o ).

tff('predicate_natTrans$d',axiom,
    ~ 'natTrans$d'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1') ).

tff('declare_member$h',type,
    'member$h': ( 'B$' * 'B_set$' ) > $o ).

tff('predicate_member$h',axiom,
    'member$h'('fmb_B$_1','fmb_B_set$_1') ).

tff('declare_member$a',type,
    'member$a': ( 'ZF_ZF_prod$' * 'ZF_ZF_prod_set$' ) > $o ).

tff('predicate_member$a',axiom,
    'member$a'('fmb_ZF_ZF_prod$_1','fmb_ZF_ZF_prod_set$_1') ).

tff('declare_member$i',type,
    'member$i': ( 'A$' * 'A_set$' ) > $o ).

tff('predicate_member$i',axiom,
    'member$i'('fmb_A$_1','fmb_A_set$_1') ).

tff('declare_natTrans$f',type,
    'natTrans$f': 'A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' > $o ).

tff('predicate_natTrans$f',axiom,
    ~ 'natTrans$f'('fmb_A_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_b_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1') ).

tff('declare_nTCompDefined$c',type,
    'nTCompDefined$c': ( 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$' ) > $o ).

tff('predicate_nTCompDefined$c',axiom,
    ~ 'nTCompDefined$c'('fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1','fmb_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$_1') ).

tff('declare_natTransP$c',type,
    'natTransP$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$' > $o ).

tff('predicate_natTransP$c',axiom,
    ~ 'natTransP$c'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$_1') ).

tff('declare_nTCompDefined$d',type,
    'nTCompDefined$d': ( 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' ) > $o ).

tff('predicate_nTCompDefined$d',axiom,
    ~ 'nTCompDefined$d'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1','fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1') ).

tff('declare_fun_app$f',type,
    'fun_app$f': ( 'B_a_fun_bool_fun$' * 'B_a_fun$' ) > $o ).

tff('predicate_fun_app$f',axiom,
    ~ 'fun_app$f'('fmb_B_a_fun_bool_fun$_1','fmb_B_a_fun$_1') ).

tff('declare_category_axioms$a',type,
    'category_axioms$a': 'ZF_ZF_unit_Category_ext$' > $o ).

tff('predicate_category_axioms$a',axiom,
    'category_axioms$a'('fmb_ZF_ZF_unit_Category_ext$_1') ).

tff('declare_nt_abbrev$c',type,
    'nt_abbrev$c': ( 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$' * 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' * 'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$' ) > $o ).

tff('predicate_nt_abbrev$c',axiom,
    ~ 'nt_abbrev$c'('fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$_1','fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$_1','fmb_A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$_1') ).

tff('declare_preFunctor$a',type,
    'preFunctor$a': 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' > $o ).

tff('predicate_preFunctor$a',axiom,
    'preFunctor$a'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') ).

tff('declare_member$b',type,
    'member$b': ( 'B_b_prod$' * 'B_b_prod_set$' ) > $o ).

tff('predicate_member$b',axiom,
    'member$b'('fmb_B_b_prod$_1','fmb_B_b_prod_set$_1') ).

tff('declare_fun_app$i',type,
    'fun_app$i': ( 'B_bool_fun$' * 'B$' ) > $o ).

tff('predicate_fun_app$i',axiom,
    'fun_app$i'('fmb_B_bool_fun$_1','fmb_B$_1') ).

tff('declare_member$',type,
    'member$': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$' ) > $o ).

tff('predicate_member$',axiom,
    'member$'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$_1') ).

tff('declare_mapsTo$b',type,
    'mapsTo$b': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ) > $o ).

tff('predicate_mapsTo$b',axiom,
    ~ 'mapsTo$b'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') ).

tff('declare_fun_app$h',type,
    'fun_app$h': ( 'A_b_fun_bool_fun$' * 'A_b_fun$' ) > $o ).

tff('predicate_fun_app$h',axiom,
    ~ 'fun_app$h'('fmb_A_b_fun_bool_fun$_1','fmb_A_b_fun$_1') ).

tff('declare_member$k',type,
    'member$k': ( 'Unit$' * 'Unit_set$' ) > $o ).

tff('predicate_member$k',axiom,
    'member$k'('fmb_Unit$_1','fmb_Unit_set$_1') ).

tff('declare_natTransP$',type,
    'natTransP$': 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' > $o ).

tff('predicate_natTransP$',axiom,
    'natTransP$'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1') ).

tff('declare_nt_abbrev$',type,
    'nt_abbrev$': ( 'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' * 'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$' ) > $o ).

tff('predicate_nt_abbrev$',axiom,
    'nt_abbrev$'('fmb_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1','fmb_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$_1') ).

tff('declare_member$d',type,
    'member$d': ( 'B_ZF_fun$' * 'B_ZF_fun_set$' ) > $o ).

tff('predicate_member$d',axiom,
    'member$d'('fmb_B_ZF_fun$_1','fmb_B_ZF_fun_set$_1') ).

tff('declare_functor$a',type,
    'functor$a': 'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$' > $o ).

tff('predicate_functor$a',axiom,
    'functor$a'('fmb_ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$_1') ).

tff('declare_functor$c',type,
    'functor$c': 'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$' > $o ).

tff('predicate_functor$c',axiom,
    ~ 'functor$c'('fmb_ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$_1') ).

tff('declare_member$l',type,
    'member$l': ( 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$' * 'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$' ) > $o ).

tff('predicate_member$l',axiom,
    ~ 'member$l'('fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$_1','fmb_A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$_1') ).

tff('declare_member$o',type,
    'member$o': ( 'ZF_set$' * 'ZF_set_set$' ) > $o ).

tff('predicate_member$o',axiom,
    'member$o'('fmb_ZF_set$_1','fmb_ZF_set_set$_1') ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP303_10 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.40  % Computer : n014.cluster.edu
% 0.13/0.40  % Model    : x86_64 x86_64
% 0.13/0.40  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40  % Memory   : 8046.5625MB
% 0.13/0.40  % OS       : Linux 6.8.0-71-generic
% 0.13/0.40  % CPULimit : 300
% 0.13/0.40  % WCLimit  : 300
% 0.13/0.40  % DateTime : Sun Sep 27 12:53:32 UTC 2026
% 0.13/0.40  % CPUTime  : 
% 0.13/0.40  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.13/0.44  Running first-order model finding
% 0.13/0.44  Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.01/0.92  % (787750)Will run a generic schedule for satisfiability detection.
% 2.01/0.92  % (787755)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3524403347_2999 on theBenchmark for (2999ds/0Mi)
% 2.01/0.92  % (787756)% WARNING: option uhcvi not known.
% 2.01/0.92  % (787758)dis+10_1_sil=32000:sp=arity:random_seed=1581890702:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.01/0.92  % (787756)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3334070320:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.01/0.92  % (787757)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3873456052:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.01/0.92  % (787760)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2793877353:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.01/0.92  % (787759)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3766528383:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.01/0.92  % (787761)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1766725047:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.01/0.92  % (787758)Instruction limit reached! 
% 2.01/0.92  % (787758)------------------------------
% 2.01/0.92  % (787758)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.01/0.92  % (787758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.01/0.92  % (787758)CaDiCaL version: 2.1.3
% 2.01/0.92  % (787758)Termination reason: Instruction limit
% 2.01/0.92  % (787758)Termination phase: Saturation
% 2.01/0.92  % (787758)Time elapsed: 0.055 s
% 2.01/0.92  % (787758)Peak memory usage: 14 MB
% 2.01/0.92  % (787758)Instructions burned: 103 (million)
% 2.01/0.92  % (787759)Instruction limit reached! 
% 2.01/0.92  % (787759)------------------------------
% 2.01/0.92  % (787759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.01/0.92  % (787759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.01/0.92  % (787759)CaDiCaL version: 2.1.3
% 2.01/0.92  % (787759)Termination reason: Instruction limit
% 2.01/0.92  % (787759)Termination phase: Saturation
% 2.01/0.92  % (787759)Time elapsed: 0.056 s
% 2.01/0.92  % (787759)Peak memory usage: 13 MB
% 2.01/0.92  % (787759)Instructions burned: 116 (million)
% 2.01/0.92  % (787796)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2186748563:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 2.01/0.92  % (787760)Instruction limit reached! 
% 2.01/0.92  % (787760)------------------------------
% 2.01/0.92  % (787760)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.01/0.92  % (787760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.01/0.92  % (787760)CaDiCaL version: 2.1.3
% 2.01/0.92  % (787760)Termination reason: Instruction limit
% 2.01/0.92  % (787760)Termination phase: Saturation
% 2.01/0.92  % (787760)Time elapsed: 0.076 s
% 2.01/0.92  % (787760)Peak memory usage: 15 MB
% 2.01/0.92  % (787760)Instructions burned: 131 (million)
% 2.01/0.92  % (787798)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3783186759:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 2.01/0.92  % (787761)Instruction limit reached! 
% 2.01/0.92  % (787761)------------------------------
% 2.01/0.92  % (787761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.01/0.92  % (787761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.01/0.92  % (787761)CaDiCaL version: 2.1.3
% 2.01/0.92  % (787761)Termination reason: Instruction limit
% 2.01/0.92  % (787761)Termination phase: Saturation
% 2.01/0.92  % (787761)Time elapsed: 0.091 s
% 2.01/0.92  % (787761)Peak memory usage: 15 MB
% 2.01/0.92  % (787761)Instructions burned: 160 (million)
% 2.01/0.92  % (787812)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2532614137:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.01/0.92  % (787813)ott-21_1_sil=16000:fs=off:random_seed=1235064853:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.01/0.92  % (787798)Instruction limit reached! 
% 2.01/0.92  % (787798)------------------------------
% 2.01/0.92  % (787798)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.01/0.92  % (787798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.01/0.92  % (787798)CaDiCaL version: 2.1.3
% 2.01/0.92  % (787798)Termination reason: Instruction limit
% 2.01/0.92  % (787798)Termination phase: Saturation
% 2.01/0.92  % (787798)Time elapsed: 0.067 s
% 2.01/0.92  % (787798)Peak memory usage: 14 MB
% 2.01/0.92  % (787798)Instructions burned: 132 (million)
% 2.01/0.92  % (787833)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=486100216:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 2.01/0.92  % (787813)Instruction limit reached! 
% 2.01/0.92  % (787813)------------------------------
% 2.01/0.92  % (787813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.01/0.92  % (787813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.01/0.92  % (787813)CaDiCaL version: 2.1.3
% 2.01/0.92  % (787813)Termination reason: Instruction limit
% 2.01/0.92  % (787813)Termination phase: Saturation
% 2.01/0.92  % (787813)Time elapsed: 0.092 s
% 2.01/0.92  % (787813)Peak memory usage: 14 MB
% 2.01/0.92  % (787813)Instructions burned: 181 (million)
% 2.01/0.92  % (787852)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3837659697:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 2.01/0.92  % TRYING [1]
% 2.01/0.92  % Finite Model Found!
% 2.01/0.92  % SZS status Satisfiable for theBenchmark
% 2.01/0.92  % (787796) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-787750-787796"...
% 2.01/0.92  % (787796)...printing done.
% 2.01/0.92  % SZS output start FiniteModel for theBenchmark
% See solution above
% 2.01/0.93  % (787796)------------------------------
% 2.01/0.93  % (787796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.01/0.93  % (787796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.01/0.93  % (787796)CaDiCaL version: 2.1.3
% 2.01/0.93  % (787796)Termination reason: Satisfiable
% 2.01/0.93  % (787796)Time elapsed: 0.334 s
% 2.01/0.93  % (787796)Peak memory usage: 23 MB
% 2.01/0.93  % (787796)Instructions burned: 715 (million)
% 2.01/0.93  % (787750)Success in time 0.477 s
% 2.01/0.93  % Vampire exiting
%------------------------------------------------------------------------------