%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : ITP303_10 : TPTP v9.2.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n021.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 : Satisfiable 137.64s 137.97s % Output : Model 137.64s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ITP303_10 : TPTP v9.2.1. Released v8.2.0. % 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.18/0.34 % Computer : n021.cluster.edu % 0.18/0.34 % Model : x86_64 x86_64 % 0.18/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.18/0.34 % Memory : 8042.1875MB % 0.18/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.18/0.34 % CPULimit : 300 % 0.18/0.34 % WCLimit : 300 % 0.18/0.34 % DateTime : Tue Jun 2 04:59:20 EDT 2026 % 0.18/0.34 % CPUTime : % 0.37/0.61 %----Disproving TF0_NAR % 0.37/0.62 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 0.45/0.68 --- Run --mbqi at 45... % 45.58/45.84 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45... % 90.69/90.96 --- Run --full-saturate-quant at 45... % 135.77/136.12 --- Run --finite-model-find --fmf-bound --macros-quant at 60... % 137.64/137.97 % SZS status Satisfiable % 137.64/137.97 % SZS output start Model % 137.64/137.98 ( % 137.64/137.98 ; cardinality of $$unsorted is 1 % 137.64/137.98 ; rep: (as @$$unsorted_0 $$unsorted) % 137.64/137.98 ; cardinality of |tptp.'B_ZF_fun_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_ZF_fun_set$'__0| |tptp.'B_ZF_fun_set$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) % 137.64/137.98 ; cardinality of |tptp.'Unit_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'Unit_set$'__0| |tptp.'Unit_set$'|) % 137.64/137.98 ; 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 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; cardinality of |tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'| is 1 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|) % 137.64/137.98 ; cardinality of |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'__0| |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'|) % 137.64/137.98 ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| is 1 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; cardinality of |tptp.'Unit_unit_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'Unit_unit_fun$'__0| |tptp.'Unit_unit_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_b_b_c_LSCategory_ext_Category_ext$'__0| |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_prod_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|) % 137.64/137.98 ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$'| is 1 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_set_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|) % 137.64/137.98 ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_set_ZF_set_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_set_ZF_set_fun$'__0| |tptp.'ZF_set_ZF_set_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$'| is 1 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_set_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'| is 1 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; cardinality of |tptp.'A_b_fun_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_b_fun_set$'__0| |tptp.'A_b_fun_set$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_fun$'__0| |tptp.'ZF_ZF_prod_ZF_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'B_c_LSCategory_ext$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_c_LSCategory_ext$'__0| |tptp.'B_c_LSCategory_ext$'|) % 137.64/137.98 ; cardinality of |tptp.'B_b_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_b_fun$'__0| |tptp.'B_b_fun$'|) % 137.64/137.98 ; 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_NatTrans_ext$'| is 1 % 137.64/137.98 ; 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_NatTrans_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_NatTrans_ext$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'__0| |tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'|) % 137.64/137.98 ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$'| is 1 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; 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 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; cardinality of |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'| is 1 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; 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 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; 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 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_prod$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_prod$'__0| |tptp.'ZF_ZF_prod$'|) % 137.64/137.98 ; cardinality of |tptp.'B_b_prod_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_b_prod_set$'__0| |tptp.'B_b_prod_set$'|) % 137.64/137.98 ; cardinality of |tptp.'B$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B$'__0| |tptp.'B$'|) % 137.64/137.98 ; cardinality of |tptp.'A_ZF_fun_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_ZF_fun_set$'__0| |tptp.'A_ZF_fun_set$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_ZF_fun_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|) % 137.64/137.98 ; cardinality of |tptp.'Unit_unit_unit_Category_ext$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'Unit_unit_unit_Category_ext$'__0| |tptp.'Unit_unit_unit_Category_ext$'|) % 137.64/137.98 ; cardinality of |tptp.'C$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'C$'__0| |tptp.'C$'|) % 137.64/137.98 ; cardinality of |tptp.'A_ZF_fun_bool_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_ZF_fun_bool_fun$'__0| |tptp.'A_ZF_fun_bool_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'B_b_prod_bool_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_b_prod_bool_fun$'__0| |tptp.'B_b_prod_bool_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_fun_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_fun_set$'__0| |tptp.'ZF_ZF_prod_ZF_fun_set$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_prod_bool_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_prod_bool_fun$'__0| |tptp.'ZF_ZF_prod_bool_fun$'|) % 137.64/137.98 ; 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_fun$'| is 1 % 137.64/137.98 ; 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_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_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_fun_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_fun_set$'__0| |tptp.'ZF_ZF_fun_set$'|) % 137.64/137.98 ; cardinality of |tptp.'B_b_prod_b_fun_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_b_prod_b_fun_set$'__0| |tptp.'B_b_prod_b_fun_set$'|) % 137.64/137.98 ; cardinality of |tptp.'B_a_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'__0| |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|) % 137.64/137.98 ; cardinality of |tptp.'B_b_prod$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_b_prod$'__0| |tptp.'B_b_prod$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'| is 1 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; cardinality of |tptp.'A_bool_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'A_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'| is 1 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; cardinality of |tptp.'A_b_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|) % 137.64/137.98 ; 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_fun$'| is 1 % 137.64/137.98 ; 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_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_Functor_ext_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'B_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) % 137.64/137.98 ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'A_b_fun_bool_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_b_fun_bool_fun$'__0| |tptp.'A_b_fun_bool_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'A$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A$'__0| |tptp.'A$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_unit_Category_ext$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|) % 137.64/137.98 ; 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_NatTrans_ext$'| is 1 % 137.64/137.98 ; 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_NatTrans_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_NatTrans_ext$'|) % 137.64/137.98 ; cardinality of |tptp.'B_b_prod_b_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_b_prod_b_fun$'__0| |tptp.'B_b_prod_b_fun$'|) % 137.64/137.98 ; 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 % 137.64/137.98 ; 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$'|) % 137.64/137.98 ; cardinality of |tptp.'B_set_b_set_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_set_b_set_fun$'__0| |tptp.'B_set_b_set_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_bool_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'B_b_b_fun_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_b_b_fun_fun$'__0| |tptp.'B_b_b_fun_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'A_ZF_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'A_ZF_fun$'__0| |tptp.'A_ZF_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'Unit$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|) % 137.64/137.98 ; cardinality of |tptp.'ZF$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|) % 137.64/137.98 ; cardinality of |tptp.'B_ZF_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_ZF_fun$'__0| |tptp.'B_ZF_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'B_a_fun_set$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_a_fun_set$'__0| |tptp.'B_a_fun_set$'|) % 137.64/137.98 ; cardinality of |tptp.'B_a_fun_bool_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_a_fun_bool_fun$'__0| |tptp.'B_a_fun_bool_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'B_bool_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) % 137.64/137.98 ; cardinality of |tptp.'B_ZF_fun_bool_fun$'| is 1 % 137.64/137.98 ; rep: (as |@_tptp.'B_ZF_fun_bool_fun$'__0| |tptp.'B_ZF_fun_bool_fun$'|) % 137.64/137.98 (define-fun |tptp.'functorComp$a'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'collect$e'| (($x1 |tptp.'B_ZF_fun_bool_fun$'|)) |tptp.'B_ZF_fun_set$'| (as |@_tptp.'B_ZF_fun_set$'__0| |tptp.'B_ZF_fun_set$'|)) % 137.64/137.98 (define-fun |tptp.'more_update$'| (($x1 |tptp.'Unit_unit_fun$'|) ($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$'|)) % 137.64/137.98 (define-fun |tptp.'id$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 137.64/137.98 (define-fun |tptp.'makeCat$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$'|)) % 137.64/137.98 (define-fun |tptp.'restrict$c'| (($x1 |tptp.'A_ZF_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_ZF_fun$'| (as |@_tptp.'A_ZF_fun$'__0| |tptp.'A_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'functorComp$'| (($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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'extensional$c'| (($x1 |tptp.'B_set$'|)) |tptp.'B_a_fun_set$'| (as |@_tptp.'B_a_fun_set$'__0| |tptp.'B_a_fun_set$'|)) % 137.64/137.98 (define-fun |tptp.'uun$'| (($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_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'member$j'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_fun_set$'|)) Bool true) % 137.64/137.98 (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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'mor_update$a'| (($x1 |tptp.'B_set_b_set_fun$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'uum$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'A_ZF_fun$'| (as |@_tptp.'A_ZF_fun$'__0| |tptp.'A_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'nTCod$c'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'uuq$'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) ($x2 |tptp.'A$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'nt_abbrev$a'| (($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_Functor_ext$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$s'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'more$b'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)) % 137.64/137.98 (define-fun |tptp.'unitFunctor$'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'natTransMap$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTrans_ext$a'| (($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$'|) ($x3 |tptp.'A_ZF_fun$'|) ($x4 |tptp.'Unit$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'member$n'| (($x1 |tptp.'B_b_prod_b_fun$'|) ($x2 |tptp.'B_b_prod_b_fun_set$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'fun_app$e'| (($x1 |tptp.'B_ZF_fun_bool_fun$'|) ($x2 |tptp.'B_ZF_fun$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'catExp$c'| ((BOUND_VARIABLE_44629 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) (BOUND_VARIABLE_44631 |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$'|)) % 137.64/137.98 (define-fun |tptp.'extCategory$'| ((BOUND_VARIABLE_44658 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'the$a'| (($x1 |tptp.'B_bool_fun$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.64/137.98 (define-fun |tptp.'mapsTo$'| (($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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'uuz$'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'functor_comp_def$c'| ((BOUND_VARIABLE_44677 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) (BOUND_VARIABLE_44679 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'catCod$d'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'lSCategory$'| ((BOUND_VARIABLE_44689 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'catDom$c'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$a'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'natTrans$'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$n'| (($x1 |tptp.'A_ZF_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 137.64/137.98 (define-fun |tptp.'uua$'| (($x1 |tptp.'ZF_set$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'uup$'| (($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$'|)) |tptp.'A_ZF_fun$'| (as |@_tptp.'A_ZF_fun$'__0| |tptp.'A_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'member$f'| ((BOUND_VARIABLE_44704 |tptp.'A_ZF_fun$'|) (BOUND_VARIABLE_44706 |tptp.'A_ZF_fun_set$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'extensional$d'| (($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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'catDom_update$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext_a_b_b_c_LSCategory_ext_Category_ext_fun$'|)) |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_fun$'| (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_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_Functor_ext_fun$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'functor_comp_def$b'| ((BOUND_VARIABLE_44721 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) (BOUND_VARIABLE_44723 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'nTCatDom$f'| (($x1 |tptp.'ZF_unit_ZF_unit_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$'|)) % 137.64/137.98 (define-fun |tptp.'top$'| () |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 137.64/137.98 (define-fun |tptp.'restrict$a'| (($x1 |tptp.'B_b_prod_b_fun$'|) ($x2 |tptp.'B_b_prod_set$'|) ($x3 |tptp.'B_b_prod$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.64/137.98 (define-fun |tptp.'mapM$a'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)) % 137.64/137.98 (define-fun |tptp.'natTransP$f'| (($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_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'catExp$'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'more$c'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'C$'| (as |@_tptp.'C$'__0| |tptp.'C$'|)) % 137.64/137.98 (define-fun |tptp.'oppositeCategory$'| () |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$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$r'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'|) ($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_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$'|)) % 137.64/137.98 (define-fun |tptp.'nTDom$a'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'mapO$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$'|)) % 137.64/137.98 (define-fun |tptp.'f$'| () |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.64/137.98 (define-fun |tptp.'natTransComp$g'| (($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_NatTrans_ext$'|) ($x2 |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_NatTrans_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_NatTrans_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_NatTrans_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_NatTrans_ext$'|)) % 137.64/137.98 (define-fun |tptp.'nTCompDefined$a'| (($x1 |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_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'uus$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'uud$'| (($x1 |tptp.'B_a_fun_set$'|)) |tptp.'B_a_fun_bool_fun$'| (as |@_tptp.'B_a_fun_bool_fun$'__0| |tptp.'B_a_fun_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTransComp$d'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|) ($x2 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'| (as |@_tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'__0| |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$q'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'|) ($x2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'fun_app$b'| (($x1 |tptp.'ZF_ZF_prod_bool_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'fun_app$ab'| (($x1 |tptp.'B_a_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 137.64/137.98 (define-fun |tptp.'category$a'| ((BOUND_VARIABLE_44766 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'functor_comp_def$a'| ((BOUND_VARIABLE_44783 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) (BOUND_VARIABLE_44785 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'nTCatDom$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'mapO$f'| (($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$'|) ($x2 |tptp.'A$'|)) |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$'|)) % 137.64/137.98 (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) % 137.64/137.98 (define-fun |tptp.'collect$a'| (($x1 |tptp.'B_b_prod_bool_fun$'|)) |tptp.'B_b_prod_set$'| (as |@_tptp.'B_b_prod_set$'__0| |tptp.'B_b_prod_set$'|)) % 137.64/137.98 (define-fun |tptp.'nTCod$e'| (($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_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'functorM_axioms$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'mor$c'| (($x1 |tptp.'Unit_unit_unit_Category_ext$'|)) |tptp.'Unit_set$'| (as |@_tptp.'Unit_set$'__0| |tptp.'Unit_set$'|)) % 137.64/137.98 (define-fun |tptp.'pair$a'| (($x1 |tptp.'B$'|) ($x2 |tptp.'B$'|)) |tptp.'B_b_prod$'| (as |@_tptp.'B_b_prod$'__0| |tptp.'B_b_prod$'|)) % 137.64/137.98 (define-fun |tptp.'equivalence_axioms$'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'dom_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$'|)) % 137.64/137.98 (define-fun |tptp.'functorExt$'| ((BOUND_VARIABLE_44794 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'category$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'fun_app$u'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_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$'|)) % 137.64/137.98 (define-fun |tptp.'idNatTrans$d'| () |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_fun$'| (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_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_fun$'|)) % 137.64/137.98 (define-fun |tptp.'uuk$'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'uut$'| () |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'comp_update$'| (($x1 |tptp.'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_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$'|)) % 137.64/137.98 (define-fun |tptp.'nTCompDefined$'| ((BOUND_VARIABLE_44837 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|) (BOUND_VARIABLE_44839 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'case_prod$a'| (($x1 |tptp.'B_b_b_fun_fun$'|)) |tptp.'B_b_prod_b_fun$'| (as |@_tptp.'B_b_prod_b_fun$'__0| |tptp.'B_b_prod_b_fun$'|)) % 137.64/137.98 (define-fun |tptp.'equivalence$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'member$m'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_fun_set$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'functorM$a'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'nTCatDom$b'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|)) % 137.64/137.98 (define-fun |tptp.'natTransComp$f'| (($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_NatTrans_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$'|)) |tptp.'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$'| (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_NatTrans_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_NatTrans_ext$'|)) % 137.64/137.98 (define-fun |tptp.'uu$'| (($x1 |tptp.'B_set$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'set$'| () |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|)) % 137.64/137.98 (define-fun |tptp.'nTCatCod$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'mapM$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.64/137.98 (define-fun |tptp.'unity$'| () |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)) % 137.64/137.98 (define-fun |tptp.'uuo$'| (($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_NatTrans_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTrans$a'| ((BOUND_VARIABLE_44851 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'uur$'| (($x1 |tptp.'ZF$'|)) |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$d'| (($x1 |tptp.'ZF_bool_fun$'|) ($x2 |tptp.'ZF$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'fun_app$z'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$'|) ($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_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'|)) % 137.64/137.98 (define-fun |tptp.'oppositeCategory$b'| () |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$'|)) % 137.64/137.98 (define-fun |tptp.'nTDom$f'| (($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_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'natTransP$e'| (($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_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'uuy$'| (($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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$l'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.64/137.98 (define-fun |tptp.'nTCompDefined$b'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|) ($x2 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'idNatTrans$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_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$'|)) % 137.64/137.98 (define-fun |tptp.'natTransMap$c'| (($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_NatTrans_ext$'|) ($x2 |tptp.'ZF$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'catDom$'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'zFfun$'| (($x1 |tptp.'ZF$'|) ($x2 |tptp.'ZF$'|) ($x3 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 137.64/137.98 (define-fun |tptp.'catDom_update$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext_ZF_ZF_unit_Category_ext_fun$'|)) |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$'| (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$'|)) % 137.64/137.98 (define-fun |tptp.'inverse_rel$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'member$c'| ((BOUND_VARIABLE_44866 |tptp.'ZF$'|) (BOUND_VARIABLE_44868 |tptp.'ZF_set$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'extensional$b'| (($x1 |tptp.'B_set$'|)) |tptp.'B_ZF_fun_set$'| (as |@_tptp.'B_ZF_fun_set$'__0| |tptp.'B_ZF_fun_set$'|)) % 137.64/137.98 (define-fun |tptp.'member$g'| ((BOUND_VARIABLE_44883 |tptp.'A_b_fun$'|) (BOUND_VARIABLE_44885 |tptp.'A_b_fun_set$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'fun_app$p'| (($x1 |tptp.'A_b_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.64/137.98 (define-fun |tptp.'idNatTrans$'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'| (as |@_tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'__0| |tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'|)) % 137.64/137.98 (define-fun |tptp.'idNatTrans$c'| ((BOUND_VARIABLE_44895 |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$'|)) % 137.64/137.98 (define-fun |tptp.'compDefined$c'| (($x1 |tptp.'Unit_unit_unit_Category_ext$'|) ($x2 |tptp.'Unit$'|) ($x3 |tptp.'Unit$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'more$a'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)) % 137.64/137.98 (define-fun |tptp.'natTransP$b'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'more$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)) % 137.64/137.98 (define-fun |tptp.'functor_comp_def$'| ((BOUND_VARIABLE_44910 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) (BOUND_VARIABLE_44912 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'functor$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'functor$f'| (($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 false) % 137.64/137.98 (define-fun |tptp.'nTCatCod$'| ((BOUND_VARIABLE_44922 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|)) % 137.64/137.98 (define-fun |tptp.'nTCod$f'| (($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_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'category_axioms$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) % 137.64/137.98 (define-fun |tptp.'mapM$e'| (($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$'|) ($x2 |tptp.'ZF$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'nTCatCod$a'| ((BOUND_VARIABLE_44931 |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$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$ac'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'lSCategory_axioms$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'member$e'| ((BOUND_VARIABLE_44946 |tptp.'B_a_fun$'|) (BOUND_VARIABLE_44948 |tptp.'B_a_fun_set$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'natTransMap$e'| (($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_NatTrans_ext$'|) ($x2 |tptp.'A$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'zFfunCod$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTransMap$b'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$k'| (($x1 |tptp.'ZF_ZF_ZF_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'homFtor$'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'category_ext$'| (($x1 |tptp.'A_set$'|) ($x2 |tptp.'B_set$'|) ($x3 |tptp.'B_a_fun$'|) ($x4 |tptp.'B_a_fun$'|) ($x5 |tptp.'A_b_fun$'|) ($x6 |tptp.'B_b_b_fun_fun$'|) ($x7 |tptp.'B_c_LSCategory_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$'|)) % 137.64/137.98 (define-fun |tptp.'nTCompDefined$e'| (($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_NatTrans_ext$'|) ($x2 |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_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'catDom$b'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'nTDom$e'| (($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_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'nTDom$'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$c'| (($x1 |tptp.'B_b_prod_bool_fun$'|) ($x2 |tptp.'B_b_prod$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'more$e'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)) % 137.64/137.98 (define-fun |tptp.'catDom$f'| (($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$'|)) |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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'idNatTrans$e'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) |tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'| (as |@_tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'__0| |tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'|)) % 137.64/137.98 (define-fun |tptp.'nTDom$c'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) |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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'makeCat$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_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$'|)) % 137.64/137.98 (define-fun |tptp.'extensional$f'| (($x1 |tptp.'B_b_prod_set$'|)) |tptp.'B_b_prod_b_fun_set$'| (as |@_tptp.'B_b_prod_b_fun_set$'__0| |tptp.'B_b_prod_b_fun_set$'|)) % 137.64/137.98 (define-fun |tptp.'restrict$d'| (($x1 |tptp.'B_a_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_a_fun$'| (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTrans$e'| (($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_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (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$'|)) % 137.64/137.98 (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) % 137.64/137.98 (define-fun |tptp.'nt_abbrev$b'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|) ($x2 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x3 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'collect$d'| (($x1 |tptp.'A_bool_fun$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 137.64/137.98 (define-fun |tptp.'equivalence$a'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTrans_ext$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) ($x3 |tptp.'ZF_ZF_fun$'|) ($x4 |tptp.'Unit$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$g'| (($x1 |tptp.'A_ZF_fun_bool_fun$'|) ($x2 |tptp.'A_ZF_fun$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'extCategory$a'| ((BOUND_VARIABLE_44766 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'catExp$a'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'category_axioms$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'dom$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$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'functor_abbrev$'| ((BOUND_VARIABLE_44976 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) (BOUND_VARIABLE_44978 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) (BOUND_VARIABLE_44980 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'fun_app$m'| (($x1 |tptp.'B_b_b_fun_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B_b_fun$'| (as |@_tptp.'B_b_fun$'__0| |tptp.'B_b_fun$'|)) % 137.64/137.98 (define-fun |tptp.'nTCod_update$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_Functor_ext_fun$'|) ($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$'|)) % 137.64/137.98 (define-fun |tptp.'catCod$c'| (($x1 |tptp.'ZF_a_ZF_b_unit_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$'|)) % 137.64/137.98 (define-fun |tptp.'restrict$f'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTransMap$'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|)) |tptp.'A_ZF_fun$'| (as |@_tptp.'A_ZF_fun$'__0| |tptp.'A_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTransMap$f'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)) % 137.64/137.98 (define-fun |tptp.'oppositeCategory$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_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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'homFtorContra$a'| ((BOUND_VARIABLE_44995 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) (BOUND_VARIABLE_44997 |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$'|)) % 137.64/137.98 (define-fun |tptp.'homFtorContra$'| ((BOUND_VARIABLE_44995 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) (BOUND_VARIABLE_44997 |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$'|)) % 137.64/137.98 (define-fun |tptp.'natTransExt$'| ((BOUND_VARIABLE_44851 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'nTCod$a'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'extensional$e'| (($x1 |tptp.'A_set$'|)) |tptp.'A_b_fun_set$'| (as |@_tptp.'A_b_fun_set$'__0| |tptp.'A_b_fun_set$'|)) % 137.64/137.98 (define-fun |tptp.'collect$b'| (($x1 |tptp.'B_bool_fun$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 137.64/137.98 (define-fun |tptp.'functorM$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'cod$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$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'zFfunComp$'| () |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|)) % 137.64/137.98 (define-fun |tptp.'compDefined$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'inverse_rel$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'the$'| (($x1 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 137.64/137.98 (define-fun |tptp.'nTCatDom$c'| (($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_NatTrans_ext$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|)) % 137.64/137.98 (define-fun |tptp.'catCod$e'| (($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$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'natTransP$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'catCod$b'| (($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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'uuf$'| (($x1 |tptp.'A_b_fun_set$'|)) |tptp.'A_b_fun_bool_fun$'| (as |@_tptp.'A_b_fun_bool_fun$'__0| |tptp.'A_b_fun_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'nTDom_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_Functor_ext_fun$'|) ($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$'|)) % 137.64/137.98 (define-fun |tptp.'catCod$f'| (($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$'|)) |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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'natTrans$b'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'oppositeCategory$c'| (($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_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$'|)) % 137.64/137.98 (define-fun |tptp.'mapsTo$c'| (($x1 |tptp.'Unit_unit_unit_Category_ext$'|) ($x2 |tptp.'Unit$'|) ($x3 |tptp.'Unit$'|) ($x4 |tptp.'Unit$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'cod_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$'|)) % 137.64/137.98 (define-fun |tptp.'natTrans$c'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'lSCategory_ext$'| (($x1 |tptp.'B_ZF_fun$'|) ($x2 |tptp.'C$'|)) |tptp.'B_c_LSCategory_ext$'| (as |@_tptp.'B_c_LSCategory_ext$'__0| |tptp.'B_c_LSCategory_ext$'|)) % 137.64/137.98 (define-fun |tptp.'identityFunctor$a'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'collect$h'| (($x1 |tptp.'A_b_fun_bool_fun$'|)) |tptp.'A_b_fun_set$'| (as |@_tptp.'A_b_fun_set$'__0| |tptp.'A_b_fun_set$'|)) % 137.64/137.98 (define-fun |tptp.'natTransComp$b'| ((BOUND_VARIABLE_45020 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|) (BOUND_VARIABLE_45022 |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$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$j'| (($x1 |tptp.'A_bool_fun$'|) ($x2 |tptp.'A$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'comp$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$'|) ($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$'|)) % 137.64/137.98 (define-fun |tptp.'functor$b'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'compDefined$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$'|) ($x3 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'functor$'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'mor_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$'|)) % 137.64/137.98 (define-fun |tptp.'catCod$a'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'functor_abbrev$a'| (($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) % 137.64/137.98 (define-fun |tptp.'natTransMap$a'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'functor$e'| (($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 false) % 137.64/137.98 (define-fun |tptp.'cod$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_a_fun$'| (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|)) % 137.64/137.98 (define-fun |tptp.'makeFtor$'| () |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_fun$'| (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_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_Functor_ext_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTrans$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'functor_ext$a'| ((_arg_1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) (_arg_2 |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$'|) (_arg_3 |tptp.'B_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'|) (_arg_4 |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$'|)) % 137.64/137.98 (define-fun |tptp.'natTransExt$a'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'nTCatCod$e'| (($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_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'member$h'| ((BOUND_VARIABLE_45043 |tptp.'B$'|) (BOUND_VARIABLE_45045 |tptp.'B_set$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'fun_app$w'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'mapO$'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'nTDom$b'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'nTCod$'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'|)) % 137.64/137.98 (define-fun |tptp.'member$a'| ((BOUND_VARIABLE_45060 |tptp.'ZF_ZF_prod$'|) (BOUND_VARIABLE_45062 |tptp.'ZF_ZF_prod_set$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'member$i'| ((BOUND_VARIABLE_45077 |tptp.'A$'|) (BOUND_VARIABLE_45079 |tptp.'A_set$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'uul$'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'identityFunctor$'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'restrict$e'| (($x1 |tptp.'A_b_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 137.64/137.98 (define-fun |tptp.'category_ext$a'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'constFunctor$'| (($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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'natTrans$f'| (($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_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'collect$f'| (($x1 |tptp.'B_a_fun_bool_fun$'|)) |tptp.'B_a_fun_set$'| (as |@_tptp.'B_a_fun_set$'__0| |tptp.'B_a_fun_set$'|)) % 137.64/137.98 (define-fun |tptp.'makeNT$a'| (($x1 |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$'|)) % 137.64/137.98 (define-fun |tptp.'nTCompDefined$c'| (($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_NatTrans_ext$'|) ($x2 |tptp.'ZF_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext_unit_unit_unit_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'inverse$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'uuv$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'restrict$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|) ($x3 |tptp.'ZF_ZF_prod$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$t'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'extensional$a'| (($x1 |tptp.'A_set$'|)) |tptp.'A_ZF_fun_set$'| (as |@_tptp.'A_ZF_fun_set$'__0| |tptp.'A_ZF_fun_set$'|)) % 137.64/137.98 (define-fun |tptp.'functorExt$a'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTransP$c'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'nTCompDefined$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'|) ($x2 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'nTCatDom$a'| ((BOUND_VARIABLE_44931 |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$'|)) % 137.64/137.98 (define-fun |tptp.'zF2mor$'| ((BOUND_VARIABLE_45096 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) (BOUND_VARIABLE_45098 |tptp.'ZF$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$x'| (($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_fun$'|) ($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$'|)) % 137.64/137.98 (define-fun |tptp.'collect$j'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$f'| (($x1 |tptp.'B_a_fun_bool_fun$'|) ($x2 |tptp.'B_a_fun$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'uub$'| (($x1 |tptp.'A_set$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$af'| (($x1 |tptp.'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$'|) ($x2 |tptp.'ZF_ZF_ZF_fun_fun$'|)) |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|)) % 137.64/137.98 (define-fun |tptp.'uux$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_b_b_fun_fun$'| (as |@_tptp.'B_b_b_fun_fun$'__0| |tptp.'B_b_b_fun_fun$'|)) % 137.64/137.98 (define-fun |tptp.'uui$'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'category_ext$b'| ((_arg_1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$'|) (_arg_2 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_set$'|) (_arg_3 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'|) (_arg_4 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_fun$'|) (_arg_5 |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_fun$'|) (_arg_6 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$'|) (_arg_7 |tptp.'Unit$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'dom$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_a_fun$'| (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|)) % 137.64/137.98 (define-fun |tptp.'more$d'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_c_LSCategory_ext$'| (as |@_tptp.'B_c_LSCategory_ext$'__0| |tptp.'B_c_LSCategory_ext$'|)) % 137.64/137.98 (define-fun |tptp.'zFfunDom$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTransP$a'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'zFfunApp$'| () |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|)) % 137.64/137.98 (define-fun |tptp.'collect$c'| (($x1 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$ae'| (($x1 |tptp.'B_set_b_set_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 137.64/137.98 (define-fun |tptp.'mapM$f'| (($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$'|) ($x2 |tptp.'B$'|)) |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$'|)) % 137.64/137.98 (define-fun |tptp.'category_axioms$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'isomorphism$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'nt_abbrev$c'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'|) ($x2 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x3 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'nTCod_update$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext_fun$'|) ($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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'uuw$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_b_prod_bool_fun$'| (as |@_tptp.'B_b_prod_bool_fun$'__0| |tptp.'B_b_prod_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'uuh$'| (($x1 |tptp.'B_b_prod_set$'|)) |tptp.'B_b_prod_bool_fun$'| (as |@_tptp.'B_b_prod_bool_fun$'__0| |tptp.'B_b_prod_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'functorM_axioms$a'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'isomorphism$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'makeNT$'| ((BOUND_VARIABLE_45112 |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$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$o'| (($x1 |tptp.'B_ZF_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 137.64/137.98 (define-fun |tptp.'catDom$e'| (($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$'|)) |tptp.'ZF_ZF_unit_Category_ext$'| (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|)) % 137.64/137.98 (define-fun |tptp.'inverse$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'preFunctor$a'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'fun_app$ad'| (($x1 |tptp.'ZF_set_ZF_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$aa'| (($x1 |tptp.'Unit_unit_fun$'|) ($x2 |tptp.'Unit$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)) % 137.64/137.98 (define-fun |tptp.'member$b'| ((BOUND_VARIABLE_45127 |tptp.'B_b_prod$'|) (BOUND_VARIABLE_45129 |tptp.'B_b_prod_set$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'obj$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 137.64/137.98 (define-fun |tptp.'homFtorMapContra$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'A_ZF_fun$'| (as |@_tptp.'A_ZF_fun$'__0| |tptp.'A_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$i'| (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'elem$'| (($x1 |tptp.'ZF$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'comp$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_b_b_fun_fun$'| (as |@_tptp.'B_b_b_fun_fun$'__0| |tptp.'B_b_b_fun_fun$'|)) % 137.64/137.98 (define-fun |tptp.'yFtorNT$'| ((BOUND_VARIABLE_45148 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) (BOUND_VARIABLE_45150 |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$'|)) % 137.64/137.98 (define-fun |tptp.'nTCatCod$f'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_ext$'|)) |tptp.'Unit_unit_unit_Category_ext$'| (as |@_tptp.'Unit_unit_unit_Category_ext$'__0| |tptp.'Unit_unit_unit_Category_ext$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$v'| (($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_fun$'|) ($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$'|)) % 137.64/137.98 (define-fun |tptp.'nTDom$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'more_update$a'| (($x1 |tptp.'Unit_unit_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$'|)) % 137.64/137.98 (define-fun |tptp.'catDom$d'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'member$'| ((BOUND_VARIABLE_45165 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) (BOUND_VARIABLE_45167 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_set$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'fun_app$'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'mapsTo$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$'|) ($x3 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) ($x4 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'mapO$c'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) |tptp.'A_ZF_fun$'| (as |@_tptp.'A_ZF_fun$'__0| |tptp.'A_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'constFunctor$b'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$h'| (($x1 |tptp.'A_b_fun_bool_fun$'|) ($x2 |tptp.'A_b_fun$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'collect$i'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|)) |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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'member$k'| (($x1 |tptp.'Unit$'|) ($x2 |tptp.'Unit_set$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'mapsTo$a'| (($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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'natTransP$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_NatTrans_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'mapM$c'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 137.64/137.98 (define-fun |tptp.'mor$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_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$'|)) % 137.64/137.98 (define-fun |tptp.'extensional$'| (($x1 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_fun_set$'| (as |@_tptp.'ZF_ZF_fun_set$'__0| |tptp.'ZF_ZF_fun_set$'|)) % 137.64/137.98 (define-fun |tptp.'uuu$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTransComp$a'| ((BOUND_VARIABLE_45181 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$'|) (BOUND_VARIABLE_45183 |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$'|)) % 137.64/137.98 (define-fun |tptp.'uug$'| (($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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'restrict$b'| (($x1 |tptp.'B_ZF_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_ZF_fun$'| (as |@_tptp.'B_ZF_fun$'__0| |tptp.'B_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'uuj$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_b_b_fun_fun$'| (as |@_tptp.'B_b_b_fun_fun$'__0| |tptp.'B_b_b_fun_fun$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (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) % 137.64/137.98 (define-fun |tptp.'yFtor$'| ((BOUND_VARIABLE_45195 |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$'|)) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'preFunctor$'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'idNatTrans$a'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'member$d'| ((BOUND_VARIABLE_45210 |tptp.'B_ZF_fun$'|) (BOUND_VARIABLE_45212 |tptp.'B_ZF_fun_set$'|)) Bool true) % 137.64/137.98 (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$'|)) % 137.64/137.98 (define-fun |tptp.'pair$'| (($x1 |tptp.'ZF$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_prod$'| (as |@_tptp.'ZF_ZF_prod$'__0| |tptp.'ZF_ZF_prod$'|)) % 137.64/137.98 (define-fun |tptp.'nTCod$d'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'makeCat$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_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$'|)) % 137.64/137.98 (define-fun |tptp.'functor$a'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'nTCod$b'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'homSet$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A$'|)) |tptp.'A_ZF_fun$'| (as |@_tptp.'A_ZF_fun$'__0| |tptp.'A_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'functor$c'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool false) % 137.64/137.98 (define-fun |tptp.'uue$'| (($x1 |tptp.'A_ZF_fun_set$'|)) |tptp.'A_ZF_fun_bool_fun$'| (as |@_tptp.'A_ZF_fun_bool_fun$'__0| |tptp.'A_ZF_fun_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'member$l'| (($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 false) % 137.64/137.98 (define-fun |tptp.'collect$g'| (($x1 |tptp.'A_ZF_fun_bool_fun$'|)) |tptp.'A_ZF_fun_set$'| (as |@_tptp.'A_ZF_fun_set$'__0| |tptp.'A_ZF_fun_set$'|)) % 137.64/137.98 (define-fun |tptp.'nTCatDom$'| ((BOUND_VARIABLE_45221 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'explode$'| () |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 137.64/137.98 (define-fun |tptp.'isZFfun$'| () |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 137.64/137.98 (define-fun |tptp.'fun_app$y'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun$'|) ($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$'|)) % 137.64/137.98 (define-fun |tptp.'mapO$d'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)) % 137.64/137.98 (define-fun |tptp.'mor$b'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 137.64/137.98 (define-fun |tptp.'nTCatCod$c'| (($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_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'natTransComp$e'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'|) ($x2 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'| (as |@_tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'__0| |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_NatTrans_ext$'|)) % 137.64/137.98 (define-fun |tptp.'uuc$'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'nTCatCod$b'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'dom$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 137.64/137.98 (define-fun |tptp.'member$o'| (($x1 |tptp.'ZF_set$'|) ($x2 |tptp.'ZF_set_set$'|)) Bool true) % 137.64/137.98 (define-fun |tptp.'nTCatDom$e'| (($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_NatTrans_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$'|)) % 137.64/137.98 (define-fun |tptp.'comp$c'| (($x1 |tptp.'Unit_unit_unit_Category_ext$'|) ($x2 |tptp.'Unit$'|)) |tptp.'Unit_unit_fun$'| (as |@_tptp.'Unit_unit_fun$'__0| |tptp.'Unit_unit_fun$'|)) % 137.64/137.98 (define-fun |tptp.'natTransComp$c'| () |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_a_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext_fun_fun$'|)) % 137.64/137.98 (define-fun |tptp.'mapO$a'| (($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$'|)) % 137.64/137.98 (define-fun |tptp.'mapO$e'| (($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$'|) ($x2 |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$'|)) % 137.64/137.98 (define-fun |tptp.'mor$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 137.64/137.98 ) % 137.64/137.98 % SZS output end Model % 137.64/137.98 % cvc5 exiting %------------------------------------------------------------------------------