cvc5-SAT---1.3.4.CSA-Mod.s

%------------------------------------------------------------------------------
% File     : cvc5-SAT---1.3.4
% Problem  : ITP304_1 : TPTP v9.2.1. Released v8.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT

% Computer : n022.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Wed Jun  3 08:27:54 AM UTC 2026

% Result   : CounterSatisfiable 139.54s 139.76s
% Output   : Model 139.54s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : ITP304_1 : TPTP v9.2.1. Released v8.0.0.
% 0.12/0.13  % Command  : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.16/0.33  % Computer : n022.cluster.edu
% 0.16/0.33  % Model    : x86_64 x86_64
% 0.16/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33  % Memory   : 8042.1875MB
% 0.16/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34  % CPULimit : 300
% 0.16/0.34  % WCLimit  : 300
% 0.16/0.34  % DateTime : Tue Jun  2 04:58:39 EDT 2026
% 0.16/0.34  % CPUTime  : 
% 0.44/0.66  %----Disproving TF0_NAR
% 139.54/139.76  --- Run --finite-model-find --sort-inference --uf-ss-fair at 60...
% 139.54/139.76  --- Run --mbqi at 45...
% 139.54/139.76  --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45...
% 139.54/139.76  --- Run --full-saturate-quant at 45...
% 139.54/139.76  --- Run --finite-model-find --fmf-bound --macros-quant at 60...
% 139.54/139.76  % SZS status CounterSatisfiable
% 139.54/139.76  % SZS output start Model
% 139.54/139.76  (
% 139.54/139.76  ; cardinality of $$unsorted is 1
% 139.54/139.76  ; rep: (as @$$unsorted_0 $$unsorted)
% 139.54/139.76  ; cardinality of |tptp.'B_ZF_fun_set$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'B_ZF_fun_set$'__0| |tptp.'B_ZF_fun_set$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'Unit_set$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'Unit_set$'__0| |tptp.'Unit_set$'|)
% 139.54/139.76  ; cardinality of |tptp.'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$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'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$'__0| |tptp.'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$'|)
% 139.54/139.76  ; cardinality of |tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'__0| |tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_set$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_b_b_c_LSCategory_ext_Category_ext$'__0| |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_prod_set$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_set_set$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_set_ZF_set_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_set_ZF_set_fun$'__0| |tptp.'ZF_set_ZF_set_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$'__0| |tptp.'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_unit_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_unit_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_unit_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_set_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_prod_ZF_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_fun$'__0| |tptp.'ZF_ZF_prod_ZF_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_set$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_set$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_set$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_unit_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_unit_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_unit_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$'|)
% 139.54/139.76  ; cardinality of |tptp.'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$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'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$'__0| |tptp.'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$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'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_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'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_fun$'__0| |tptp.'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_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'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$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'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$'__0| |tptp.'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$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_prod$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_prod$'__0| |tptp.'ZF_ZF_prod$'|)
% 139.54/139.76  ; cardinality of |tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'__0| |tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'B$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'B$'__0| |tptp.'B$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_ZF_fun_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'Unit_unit_unit_Category_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'Unit_unit_unit_Category_ext$'__0| |tptp.'Unit_unit_unit_Category_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_prod_ZF_fun_set$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_fun_set$'__0| |tptp.'ZF_ZF_prod_ZF_fun_set$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_prod_bool_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_prod_bool_fun$'__0| |tptp.'ZF_ZF_prod_bool_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_fun_set$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_fun_set$'__0| |tptp.'ZF_ZF_fun_set$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_unit_b_unit_b_c_LSCategory_ext_unit_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_unit_b_unit_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_unit_b_unit_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'__0| |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_bool_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'A_set$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'B_set$'| is 2
% 139.54/139.76  ; rep: (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)
% 139.54/139.76  ; rep: (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|)
% 139.54/139.76  ; cardinality of |tptp.'A$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'A$'__0| |tptp.'A$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_unit_Category_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_fun_bool_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_fun_bool_fun$'__0| |tptp.'ZF_ZF_fun_bool_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'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$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'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$'__0| |tptp.'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$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_bool_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)
% 139.54/139.76  ; cardinality of |tptp.'Unit$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)
% 139.54/139.76  ; cardinality of |tptp.'B_ZF_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'B_ZF_fun$'__0| |tptp.'B_ZF_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'B_bool_fun$'| is 2
% 139.54/139.76  ; rep: (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)
% 139.54/139.76  ; rep: (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'B_ZF_fun_bool_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'B_ZF_fun_bool_fun$'__0| |tptp.'B_ZF_fun_bool_fun$'|)
% 139.54/139.76  ; cardinality of |tptp.'ZF_ZF_prod_ZF_fun_bool_fun$'| is 1
% 139.54/139.76  ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_fun_bool_fun$'__0| |tptp.'ZF_ZF_prod_ZF_fun_bool_fun$'|)
% 139.54/139.76  (define-fun |tptp.'catCod_update$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'uuh$'| (($x1 |tptp.'ZF$'|)) |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|))
% 139.54/139.76  (define-fun |tptp.'functorM$j'| (($x1 |tptp.'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$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'catDom$a'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'mapM$c'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|))
% 139.54/139.76  (define-fun |tptp.'functorComp$f'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'comp$b'| (($x1 |tptp.'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$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|) ($x3 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|))
% 139.54/139.76  (define-fun |tptp.'catDom$b'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'| (as |@_tptp.'A_b_b_c_LSCategory_ext_Category_ext$'__0| |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'c$'| () |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'| (as |@_tptp.'A_b_b_c_LSCategory_ext_Category_ext$'__0| |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'uum$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|))
% 139.54/139.76  (define-fun |tptp.'inverse$b'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|))
% 139.54/139.76  (define-fun |tptp.'collect$'| (($x1 |tptp.'ZF_ZF_prod_bool_fun$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|))
% 139.54/139.76  (define-fun |tptp.'catDom$e'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|)) |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'| (as |@_tptp.'A_b_b_c_LSCategory_ext_Category_ext$'__0| |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'preFunctor$c'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'nTDom$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'fun_app$b'| (($x1 |tptp.'ZF_bool_fun$'|) ($x2 |tptp.'ZF$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'constFunctor$k'| (($x1 |tptp.'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$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x3 |tptp.'ZF$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$j'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x3 |tptp.'A$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'mapsTo$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|) ($x3 |tptp.'A$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'unitFunctor$b'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_unit_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_unit_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_unit_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'fun_app$d'| (($x1 |tptp.'ZF_ZF_fun_bool_fun$'|) ($x2 |tptp.'ZF_ZF_fun$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'fun_app$e'| (($x1 |tptp.'B_ZF_fun_bool_fun$'|) ($x2 |tptp.'B_ZF_fun$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorExt$a'| (($x1 |tptp.'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$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'catCod$a'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functor_comp_def$g'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'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$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'obj$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|))
% 139.54/139.76  (define-fun |tptp.'mapO$c'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|))
% 139.54/139.76  (define-fun |tptp.'functor$j'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'case_prod$'| (($x1 |tptp.'ZF_ZF_ZF_fun_fun$'|)) |tptp.'ZF_ZF_prod_ZF_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_fun$'__0| |tptp.'ZF_ZF_prod_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'lSCategory$'| ((BOUND_VARIABLE_47904 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'catDom$'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'idNatTrans$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functor$i'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorM_axioms$b'| (($x1 |tptp.'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$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'obj_update$'| (($x1 |tptp.'ZF_set_ZF_set_fun$'|)) |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'| (as |@_tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'__0| |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'|))
% 139.54/139.76  (define-fun |tptp.'catCod$'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'equivalence$a'| ((BOUND_VARIABLE_47917 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'top$'| () |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|))
% 139.54/139.76  (define-fun |tptp.'makeFtor$b'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'preFunctor$e'| (($x1 |tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'inverse_rel$a'| (($x1 |tptp.'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$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|) ($x3 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'category_ext$'| (($x1 |tptp.'ZF_set$'|) ($x2 |tptp.'ZF_set$'|) ($x3 |tptp.'ZF_ZF_fun$'|) ($x4 |tptp.'ZF_ZF_fun$'|) ($x5 |tptp.'ZF_ZF_fun$'|) ($x6 |tptp.'ZF_ZF_ZF_fun_fun$'|) ($x7 |tptp.'Unit$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'obj$d'| (($x1 |tptp.'Unit_unit_unit_Category_ext$'|)) |tptp.'Unit_set$'| (as |@_tptp.'Unit_set$'__0| |tptp.'Unit_set$'|))
% 139.54/139.76  (define-fun |tptp.'uug$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$q'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x3 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'fun_app$n'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'| (as |@_tptp.'A_b_b_c_LSCategory_ext_Category_ext$'__0| |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functorComp$b'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'mapO$a'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'preFunctor$f'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'mapsTo$b'| (($x1 |tptp.'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$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|) ($x3 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) ($x4 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'equivalence_axioms$c'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorM$e'| (($x1 |tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'inverse$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|))
% 139.54/139.76  (define-fun |tptp.'functor$b'| ((BOUND_VARIABLE_47930 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functor_comp_def$a'| ((BOUND_VARIABLE_47952 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) (BOUND_VARIABLE_47954 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'natTransP$'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'category$b'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorComp$h'| (($x1 |tptp.'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$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functorM$m'| (($x1 |tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'preFunctor$k'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'more$b'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|))
% 139.54/139.76  (define-fun |tptp.'functorM_axioms$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorComp$c'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'collect$d'| (($x1 |tptp.'B_bool_fun$'|)) |tptp.'B_set$'| (ite (= (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) $x1) (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) (as |@_tptp.'B_set$'__1| |tptp.'B_set$'|)))
% 139.54/139.76  (define-fun |tptp.'mapM$a'| (($x1 |tptp.'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$'|)) |tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'| (as |@_tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'__0| |tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$f'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x3 |tptp.'A$'|)) |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'| (as |@_tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functorM$h'| (($x1 |tptp.'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$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'objIso$b'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$'| ((BOUND_VARIABLE_47974 |tptp.'ZF_ZF_unit_Category_ext$'|) (BOUND_VARIABLE_47976 |tptp.'ZF_ZF_unit_Category_ext$'|) (BOUND_VARIABLE_47978 |tptp.'ZF$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'mapO$'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) ($x2 |tptp.'A$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|))
% 139.54/139.76  (define-fun |tptp.'collect$b'| (($x1 |tptp.'ZF_ZF_fun_bool_fun$'|)) |tptp.'ZF_ZF_fun_set$'| (as |@_tptp.'ZF_ZF_fun_set$'__0| |tptp.'ZF_ZF_fun_set$'|))
% 139.54/139.76  (define-fun |tptp.'functorM$a'| ((BOUND_VARIABLE_47930 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'category$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorExt$b'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'member$a'| ((BOUND_VARIABLE_47996 |tptp.'ZF$'|) (BOUND_VARIABLE_47998 |tptp.'ZF_set$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorM$i'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'nTCompDefined$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'fun_app$l'| (($x1 |tptp.'B_ZF_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|))
% 139.54/139.76  (define-fun |tptp.'functor$o'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorM$k'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'catDom$c'| (($x1 |tptp.'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$'|)) |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'| (as |@_tptp.'A_b_b_c_LSCategory_ext_Category_ext$'__0| |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'inverse_rel$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|) ($x3 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'functor_comp_def$e'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'app$'| () |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|))
% 139.54/139.76  (define-fun |tptp.'set$'| () |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'identityFunctor$c'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functor_comp_def$b'| ((BOUND_VARIABLE_48023 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) (BOUND_VARIABLE_48025 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'extensional$a'| (($x1 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_fun_set$'| (as |@_tptp.'ZF_ZF_fun_set$'__0| |tptp.'ZF_ZF_fun_set$'|))
% 139.54/139.76  (define-fun |tptp.'preFunctor$j'| (($x1 |tptp.'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$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'mapO$g'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|))
% 139.54/139.76  (define-fun |tptp.'unity$'| () |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|))
% 139.54/139.76  (define-fun |tptp.'uul$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_prod_bool_fun$'| (as |@_tptp.'ZF_ZF_prod_bool_fun$'__0| |tptp.'ZF_ZF_prod_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'natTrans$a'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'fun_app$j'| (($x1 |tptp.'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_fun$'|) ($x2 |tptp.'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$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'compDefined$c'| (($x1 |tptp.'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$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|) ($x3 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'uuf$'| (($x1 |tptp.'ZF_set$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'preFunctor$i'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'catDom$h'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'uuj$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$u'| (($x1 |tptp.'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$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x3 |tptp.'ZF$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'natTransComp$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|))
% 139.54/139.76  (define-fun |tptp.'inverse$a'| (($x1 |tptp.'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$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|))
% 139.54/139.76  (define-fun |tptp.'inverse_rel$b'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$c'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'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$'|) ($x3 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'member$c'| ((BOUND_VARIABLE_48040 |tptp.'ZF_ZF_fun$'|) (BOUND_VARIABLE_48042 |tptp.'ZF_ZF_fun_set$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'mor2ZF$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_ZF_fun$'| (as |@_tptp.'B_ZF_fun$'__0| |tptp.'B_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'catDom$i'| (($x1 |tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'unitFunctor$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'A_unit_b_unit_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_unit_b_unit_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_unit_b_unit_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'dom$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$t'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x3 |tptp.'A$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'more$a'| (($x1 |tptp.'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$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|))
% 139.54/139.76  (define-fun |tptp.'identityFunctor$a'| (($x1 |tptp.'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$'|)) |tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'| (as |@_tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'__0| |tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'member$e'| ((BOUND_VARIABLE_6772 |tptp.'B$'|) (BOUND_VARIABLE_6773 |tptp.'B_set$'|)) Bool (and (= (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) (ite (= BOUND_VARIABLE_6773 (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|))) (= BOUND_VARIABLE_6772 (as |@_tptp.'B$'__0| |tptp.'B$'|))))
% 139.54/139.76  (define-fun |tptp.'zFfun$'| ((BOUND_VARIABLE_48080 |tptp.'ZF$'|) (BOUND_VARIABLE_48082 |tptp.'ZF$'|) (BOUND_VARIABLE_48084 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|))
% 139.54/139.76  (define-fun |tptp.'preFunctor$b'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functor$f'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_unit_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'mapO$h'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$i'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x3 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'catExp$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'member$h'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'functor_comp_def$'| ((BOUND_VARIABLE_48103 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) (BOUND_VARIABLE_48105 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'identityFunctor$f'| (($x1 |tptp.'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$'|)) |tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'| (as |@_tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'__0| |tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'lSCategory_axioms$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'mapO$f'| (($x1 |tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'zFfunCod$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'homFtor$'| ((BOUND_VARIABLE_48120 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) (BOUND_VARIABLE_48122 |tptp.'A$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'fun_app$m'| (($x1 |tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|))
% 139.54/139.76  (define-fun |tptp.'makeFtor$c'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functorComp$g'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'functor_abbrev$'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x3 |tptp.'Unit_unit_unit_Category_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorM$b'| ((BOUND_VARIABLE_48133 |tptp.'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$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'member$b'| ((BOUND_VARIABLE_48148 |tptp.'ZF_ZF_prod_ZF_fun$'|) (BOUND_VARIABLE_48150 |tptp.'ZF_ZF_prod_ZF_fun_set$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'comp$c'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|) ($x3 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|))
% 139.54/139.76  (define-fun |tptp.'member$k'| (($x1 |tptp.'ZF_set$'|) ($x2 |tptp.'ZF_set_set$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorComp$a'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'snd$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'functor$g'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'constFunctor$h'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x3 |tptp.'ZF$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functor$m'| (($x1 |tptp.'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$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'unitFunctor$a'| (($x1 |tptp.'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$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_unit_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_unit_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_unit_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'set$a'| () |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'collect$a'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun_bool_fun$'|)) |tptp.'ZF_ZF_prod_ZF_fun_set$'| (as |@_tptp.'ZF_ZF_prod_ZF_fun_set$'__0| |tptp.'ZF_ZF_prod_ZF_fun_set$'|))
% 139.54/139.76  (define-fun |tptp.'compDefined$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'uua$'| (($x1 |tptp.'ZF_ZF_fun_set$'|)) |tptp.'ZF_ZF_fun_bool_fun$'| (as |@_tptp.'ZF_ZF_fun_bool_fun$'__0| |tptp.'ZF_ZF_fun_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'mapO$b'| (($x1 |tptp.'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$'|) ($x2 |tptp.'A$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'uue$'| (($x1 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_ZF_prod_bool_fun$'| (as |@_tptp.'ZF_ZF_prod_bool_fun$'__0| |tptp.'ZF_ZF_prod_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'uui$'| () |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'preFunctor$h'| (($x1 |tptp.'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$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'uud$'| (($x1 |tptp.'A_set$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'mapM$'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'B_ZF_fun$'| (as |@_tptp.'B_ZF_fun$'__0| |tptp.'B_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'mor$b'| (($x1 |tptp.'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$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$'|))
% 139.54/139.76  (define-fun |tptp.'extCategory$'| ((BOUND_VARIABLE_48176 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functor_abbrev$b'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x3 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'mor$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$e'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x3 |tptp.'A$'|)) |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'| (as |@_tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'natTrans$'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'catDom_update$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'identityFunctor$e'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'| (as |@_tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$b'| ((BOUND_VARIABLE_48196 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) (BOUND_VARIABLE_48198 |tptp.'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$'|) (BOUND_VARIABLE_48200 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'functorM_axioms$a'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'equivalence_axioms$b'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'preFunctor$'| (($x1 |tptp.'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$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'functor_ext$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x3 |tptp.'B_ZF_fun$'|) ($x4 |tptp.'Unit$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'homFtorContra$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'id$c'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|))
% 139.54/139.76  (define-fun |tptp.'homFtorContra$'| ((BOUND_VARIABLE_48120 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) (BOUND_VARIABLE_48122 |tptp.'A$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'collect$e'| (($x1 |tptp.'A_bool_fun$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|))
% 139.54/139.76  (define-fun |tptp.'functorComp$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'nTCatDom$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functorM$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorM$'| ((BOUND_VARIABLE_48213 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'zFfunComp$'| () |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|))
% 139.54/139.76  (define-fun |tptp.'catCod$c'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) |tptp.'Unit_unit_unit_Category_ext$'| (as |@_tptp.'Unit_unit_unit_Category_ext$'__0| |tptp.'Unit_unit_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'more$c'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|))
% 139.54/139.76  (define-fun |tptp.'member$g'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_set$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'functor_ext$b'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'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$'|) ($x3 |tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'|) ($x4 |tptp.'Unit$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'fun_app$o'| (($x1 |tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'|) ($x2 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x3 |tptp.'ZF$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$n'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x3 |tptp.'ZF$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'fst$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'objIso$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'member$i'| (($x1 |tptp.'Unit$'|) ($x2 |tptp.'Unit_set$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'identityFunctor$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'| (as |@_tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functor_comp_def$c'| ((BOUND_VARIABLE_48233 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) (BOUND_VARIABLE_48235 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'uuc$'| (($x1 |tptp.'B_set$'|)) |tptp.'B_bool_fun$'| (ite (= (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) $x1) (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|)))
% 139.54/139.76  (define-fun |tptp.'isomorphism$a'| (($x1 |tptp.'Unit_unit_unit_Category_ext$'|) ($x2 |tptp.'Unit$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functor$c'| ((BOUND_VARIABLE_48133 |tptp.'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$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'constFunctor$m'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'Unit_unit_unit_Category_ext$'|) ($x3 |tptp.'Unit$'|)) |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functorM$c'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'mapsTo$c'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|) ($x3 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) ($x4 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'constFunctor$p'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x3 |tptp.'A$'|)) |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'| (as |@_tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'catDom_update$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$'|) ($x2 |tptp.'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$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'homSet$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|))
% 139.54/139.76  (define-fun |tptp.'mapsTo$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'ZF$'|) ($x3 |tptp.'ZF$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'functorExt$'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'extensional$'| (($x1 |tptp.'B_set$'|)) |tptp.'B_ZF_fun_set$'| (as |@_tptp.'B_ZF_fun_set$'__0| |tptp.'B_ZF_fun_set$'|))
% 139.54/139.76  (define-fun |tptp.'functor_ext$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x3 |tptp.'ZF_ZF_fun$'|) ($x4 |tptp.'Unit$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'homFtorMapContra$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|) ($x3 |tptp.'A$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|))
% 139.54/139.76  (define-fun |tptp.'catDom$g'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'extensional$b'| (($x1 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_ZF_prod_ZF_fun_set$'| (as |@_tptp.'ZF_ZF_prod_ZF_fun_set$'__0| |tptp.'ZF_ZF_prod_ZF_fun_set$'|))
% 139.54/139.76  (define-fun |tptp.'functorComp$e'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'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$'|)) |tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'fun_app$f'| (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) Bool (and (= (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|) $x1) (= (as |@_tptp.'B$'__0| |tptp.'B$'|) $x2)))
% 139.54/139.76  (define-fun |tptp.'functor$e'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_unit_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'fun_app$i'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|))
% 139.54/139.76  (define-fun |tptp.'category$d'| (($x1 |tptp.'Unit_unit_unit_Category_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'dom$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|))
% 139.54/139.76  (define-fun |tptp.'isOpair$'| () |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'homFtorMap$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A$'|)) |tptp.'B_ZF_fun$'| (as |@_tptp.'B_ZF_fun$'__0| |tptp.'B_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'collect$c'| (($x1 |tptp.'B_ZF_fun_bool_fun$'|)) |tptp.'B_ZF_fun_set$'| (as |@_tptp.'B_ZF_fun_set$'__0| |tptp.'B_ZF_fun_set$'|))
% 139.54/139.76  (define-fun |tptp.'comp$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|) ($x3 |tptp.'B$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|))
% 139.54/139.76  (define-fun |tptp.'functorComp$d'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'restrict$a'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'opair$'| () |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|))
% 139.54/139.76  (define-fun |tptp.'functor$k'| (($x1 |tptp.'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$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'isFun$'| () |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'isomorphism$c'| (($x1 |tptp.'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$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'compDefined$a'| (($x1 |tptp.'Unit_unit_unit_Category_ext$'|) ($x2 |tptp.'Unit$'|) ($x3 |tptp.'Unit$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'catDom$f'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'category$a'| (($x1 |tptp.'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$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'category_axioms$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'zF2mor$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|))
% 139.54/139.76  (define-fun |tptp.'makeFtor$a'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functor_abbrev$c'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x3 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'mapO$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'A$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|))
% 139.54/139.76  (define-fun |tptp.'restrict$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_ZF_prod_ZF_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_fun$'__0| |tptp.'ZF_ZF_prod_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'obj$b'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_set$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_set$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_set$'|))
% 139.54/139.76  (define-fun |tptp.'zFfunDom$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'more$'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|))
% 139.54/139.76  (define-fun |tptp.'zFfunApp$'| () |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$o'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x3 |tptp.'A$'|)) |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'| (as |@_tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'range$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'lambda$'| (($x1 |tptp.'ZF$'|) ($x2 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|))
% 139.54/139.76  (define-fun |tptp.'mor$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|))
% 139.54/139.76  (define-fun |tptp.'mapO$e'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|))
% 139.54/139.76  (define-fun |tptp.'hOMCollection$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A$'|) ($x3 |tptp.'A$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|))
% 139.54/139.76  (define-fun |tptp.'natTransMap$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'fun_app$k'| (($x1 |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functor_comp_def$j'| (($x1 |tptp.'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$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'comp$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|))
% 139.54/139.76  (define-fun |tptp.'isomorphism$d'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'fun_app$c'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun_bool_fun$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_fun$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'constFunctor$s'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x3 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'fun_app$a'| (($x1 |tptp.'ZF_ZF_prod_bool_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'mapM$b'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'functor$a'| ((BOUND_VARIABLE_48213 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'objIso$a'| (($x1 |tptp.'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$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) ($x3 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'preFunctor$a'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'natTransP$a'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'preFunctor$l'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'constFunctor$l'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'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$'|) ($x3 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'oppositeCategory$'| () |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'| (as |@_tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'__0| |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$r'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x3 |tptp.'ZF$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'constFunctor$d'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x3 |tptp.'ZF$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'member$j'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'identityFunctor$g'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'obj$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|))
% 139.54/139.76  (define-fun |tptp.'functor_comp_def$d'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'isomorphism$b'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'elem$'| (($x1 |tptp.'ZF$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'equivalence$b'| ((BOUND_VARIABLE_48213 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functor$'| ((BOUND_VARIABLE_48260 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'member$'| ((BOUND_VARIABLE_48275 |tptp.'ZF_ZF_prod$'|) (BOUND_VARIABLE_48277 |tptp.'ZF_ZF_prod_set$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'catExp$b'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'identityFunctor$d'| ((BOUND_VARIABLE_48286 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'identityFunctor$b'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'fun_app$'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|))
% 139.54/139.76  (define-fun |tptp.'functor_comp_def$i'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'comp$d'| (($x1 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'|))
% 139.54/139.76  (define-fun |tptp.'functor$l'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'catExp$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'member$f'| ((BOUND_VARIABLE_48301 |tptp.'A$'|) (BOUND_VARIABLE_48303 |tptp.'A_set$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'constFunctor$g'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x3 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'yFtorNT$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'| (as |@_tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'__0| |tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'|))
% 139.54/139.76  (define-fun |tptp.'catDom$d'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'makeCat$'| () |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'| (as |@_tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'__0| |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'|))
% 139.54/139.76  (define-fun |tptp.'fun_app$g'| (($x1 |tptp.'A_bool_fun$'|) ($x2 |tptp.'A$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorM$g'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'collect$f'| (($x1 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|))
% 139.54/139.76  (define-fun |tptp.'equivalence$c'| ((BOUND_VARIABLE_47930 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functorExt$c'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'compDefined$b'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__1| |tptp.'B_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'fun_app$h'| (($x1 |tptp.'ZF_ZF_ZF_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'isomorphism$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'id$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'domain$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'catCod_update$'| (($x1 |tptp.'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_fun$'|) ($x2 |tptp.'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$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'oppositeCategory$a'| () |tptp.'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$'| (as |@_tptp.'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$'__0| |tptp.'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$'|))
% 139.54/139.76  (define-fun |tptp.'category$c'| ((BOUND_VARIABLE_48176 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'obj$c'| (($x1 |tptp.'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$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$'|))
% 139.54/139.76  (define-fun |tptp.'image$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|))
% 139.54/139.76  (define-fun |tptp.'fun_app$p'| (($x1 |tptp.'ZF_set_ZF_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|))
% 139.54/139.76  (define-fun |tptp.'functorM$f'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'id_update$'| (($x1 |tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'|)) |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'| (as |@_tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'__0| |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'|))
% 139.54/139.76  (define-fun |tptp.'makeFtor$'| (($x1 |tptp.'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$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'nt_abbrev$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) ($x3 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'yFtor$'| ((BOUND_VARIABLE_48354 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'nTCatCod$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|))
% 139.54/139.76  (define-fun |tptp.'homFtor$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'unitFunctor$c'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'equivalence$'| ((BOUND_VARIABLE_48133 |tptp.'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$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'member$d'| ((BOUND_VARIABLE_48376 |tptp.'B_ZF_fun$'|) (BOUND_VARIABLE_48378 |tptp.'B_ZF_fun_set$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'cod$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'mapO$i'| (($x1 |tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'pair$'| (($x1 |tptp.'ZF$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_prod$'| (as |@_tptp.'ZF_ZF_prod$'__0| |tptp.'ZF_ZF_prod$'|))
% 139.54/139.76  (define-fun |tptp.'functor_comp_def$h'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_a_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functor$n'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_a_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'compDefined$d'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|) ($x3 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'yFtorNT$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'| (as |@_tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'__0| |tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'|))
% 139.54/139.76  (define-fun |tptp.'equivalence_axioms$a'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'category_axioms$a'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_Category_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'functor$h'| (($x1 |tptp.'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_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'catCod$b'| (($x1 |tptp.'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$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.76  (define-fun |tptp.'functor$d'| (($x1 |tptp.'A_unit_b_unit_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'preFunctor$m'| (($x1 |tptp.'ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_unit_unit_unit_Functor_ext$'|)) Bool false)
% 139.54/139.76  (define-fun |tptp.'inverse$c'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'uub$'| (($x1 |tptp.'B_ZF_fun_set$'|)) |tptp.'B_ZF_fun_bool_fun$'| (as |@_tptp.'B_ZF_fun_bool_fun$'__0| |tptp.'B_ZF_fun_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'preFunctor$g'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'id$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|))
% 139.54/139.76  (define-fun |tptp.'nTCod$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|))
% 139.54/139.76  (define-fun |tptp.'functorM$l'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'uu$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun_set$'|)) |tptp.'ZF_ZF_prod_ZF_fun_bool_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_fun_bool_fun$'__0| |tptp.'ZF_ZF_prod_ZF_fun_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'uuk$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|))
% 139.54/139.76  (define-fun |tptp.'id$b'| (($x1 |tptp.'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$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|))
% 139.54/139.76  (define-fun |tptp.'explode$'| () |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|))
% 139.54/139.76  (define-fun |tptp.'isZFfun$'| () |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|))
% 139.54/139.76  (define-fun |tptp.'functor_comp_def$k'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'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$'|)) Bool true)
% 139.54/139.76  (define-fun |tptp.'preFunctor$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true)
% 139.54/139.77  (define-fun |tptp.'cartProd$'| () |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|))
% 139.54/139.77  (define-fun |tptp.'equivalence_axioms$'| (($x1 |tptp.'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$'|)) Bool true)
% 139.54/139.77  (define-fun |tptp.'functorComp$i'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'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$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.77  (define-fun |tptp.'functor_comp_def$f'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_ZF_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_ZF_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true)
% 139.54/139.77  (define-fun |tptp.'yFtor$a'| ((BOUND_VARIABLE_48354 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'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$'| (as |@_tptp.'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$'__0| |tptp.'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$'|))
% 139.54/139.77  (define-fun |tptp.'cod$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|))
% 139.54/139.77  (define-fun |tptp.'functor_abbrev$a'| (($x1 |tptp.'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$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x3 |tptp.'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$'|)) Bool false)
% 139.54/139.77  (define-fun |tptp.'subset$'| (($x1 |tptp.'ZF$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|))
% 139.54/139.77  (define-fun |tptp.'inverse_rel$c'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|))
% 139.54/139.77  )
% 139.54/139.77  % SZS output end Model
% 139.54/139.77  % cvc5 exiting
%------------------------------------------------------------------------------