%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : ITP302_10 : TPTP v9.2.1. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n024.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 141.61s 141.97s % Output : Model 141.61s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : ITP302_10 : TPTP v9.2.1. Released v8.2.0. % 0.00/0.07 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.07/0.25 % Computer : n024.cluster.edu % 0.07/0.25 % Model : x86_64 x86_64 % 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.25 % Memory : 8042.1875MB % 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.25 % CPULimit : 300 % 0.07/0.25 % WCLimit : 300 % 0.07/0.25 % DateTime : Mon Jun 1 23:58:00 EDT 2026 % 0.07/0.25 % CPUTime : % 0.31/0.58 %----Disproving TF0_NAR % 0.31/0.59 --- Run --finite-model-find --sort-inference --uf-ss-fair at 60... % 0.31/0.62 --- Run --mbqi at 45... % 45.43/45.76 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 45... % 45.51/90.91 --- Run --full-saturate-quant at 45... % 135.72/136.05 --- Run --finite-model-find --fmf-bound --macros-quant at 60... % 141.61/141.97 % SZS status Satisfiable % 141.61/141.97 % SZS output start Model % 141.61/141.98 ( % 141.61/141.98 ; cardinality of $$unsorted is 1 % 141.61/141.98 ; rep: (as @$$unsorted_0 $$unsorted) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_prod_fun$'__0| |tptp.'ZF_ZF_ZF_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_ZF_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_ZF_fun_set$'__0| |tptp.'B_ZF_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_fun_set$'__0| |tptp.'Nat_ZF_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_set_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_set_set$'__0| |tptp.'Nat_set_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_ZF_prod_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_ZF_prod_prod_set$'__0| |tptp.'Nat_ZF_ZF_prod_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_nat_ZF_set_ZF_set_prod_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_nat_ZF_set_ZF_set_prod_fun_fun$'__0| |tptp.'Nat_nat_ZF_set_ZF_set_prod_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_set_ZF_set_prod_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_set_ZF_set_prod_fun_fun$'__0| |tptp.'ZF_ZF_ZF_set_ZF_set_prod_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_nat_fun_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_nat_fun_ZF_set_fun$'__0| |tptp.'Nat_nat_fun_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| is 1 % 141.61/141.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$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_nat_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_nat_set_fun$'__0| |tptp.'ZF_nat_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Unit_unit_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Unit_unit_fun$'__0| |tptp.'Unit_unit_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_nat_bool_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_nat_bool_fun_fun$'__0| |tptp.'ZF_nat_bool_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_b_b_c_LSCategory_ext_Category_ext$'__0| |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_set_set_ZF_set_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_set_set_ZF_set_set_fun$'__0| |tptp.'Nat_set_set_ZF_set_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_b_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_b_set_fun$'__0| |tptp.'ZF_b_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_prod_set$'__0| |tptp.'Nat_ZF_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_set_set_ZF_ZF_prod_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_set_set_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_ZF_prod_set_set_ZF_ZF_prod_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_set_set_ZF_set_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_set_set_ZF_set_set_fun$'__0| |tptp.'ZF_ZF_prod_set_set_ZF_set_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'__0| |tptp.'ZF_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_bool_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_bool_fun_set$'__0| |tptp.'ZF_set_bool_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|) % 141.61/141.98 ; cardinality of |tptp.'A_bool_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_bool_fun_set$'__0| |tptp.'A_bool_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_ZF_set_fun$'__0| |tptp.'ZF_set_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_b_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_b_fun_set$'__0| |tptp.'A_b_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_ZF_set_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_ZF_set_prod_set$'__0| |tptp.'ZF_set_ZF_set_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_fun_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_fun_ZF_set_fun$'__0| |tptp.'ZF_ZF_fun_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_a_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_a_fun$'__0| |tptp.'Nat_a_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_set_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_set_set$'__0| |tptp.'A_set_set$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_nat_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_nat_fun_set$'__0| |tptp.'Nat_nat_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_fun$'__0| |tptp.'ZF_ZF_prod_ZF_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_nat_ZF_ZF_prod_set_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_nat_ZF_ZF_prod_set_fun_fun$'__0| |tptp.'ZF_nat_ZF_ZF_prod_set_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_c_LSCategory_ext$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_c_LSCategory_ext$'__0| |tptp.'B_c_LSCategory_ext$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_set_set_nat_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_set_set_nat_set_fun$'__0| |tptp.'Nat_set_set_nat_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_ZF_ZF_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_ZF_ZF_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_ZF_ZF_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'__0| |tptp.'ZF_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_b_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_b_fun$'__0| |tptp.'B_b_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_nat_ZF_set_ZF_set_prod_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_nat_ZF_set_ZF_set_prod_fun_fun$'__0| |tptp.'ZF_nat_ZF_set_ZF_set_prod_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_set_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_set_prod_set$'__0| |tptp.'ZF_ZF_set_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_bool_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_bool_fun_fun$'__0| |tptp.'Nat_ZF_bool_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_nat_prod_ZF_ZF_prod_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_nat_prod_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_nat_prod_ZF_ZF_prod_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_set_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_set_prod_fun$'__0| |tptp.'ZF_ZF_ZF_set_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_ZF_prod_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_prod_fun_fun$'__0| |tptp.'ZF_ZF_ZF_ZF_prod_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_prod_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_ZF_ZF_prod_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_set_fun$'__0| |tptp.'ZF_ZF_prod_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'| is 1 % 141.61/141.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$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_nat_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_nat_set_fun$'__0| |tptp.'ZF_ZF_prod_nat_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_nat_ZF_set_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_nat_ZF_set_fun_fun$'__0| |tptp.'ZF_nat_ZF_set_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod$'__0| |tptp.'ZF_ZF_prod$'|) % 141.61/141.98 ; cardinality of |tptp.'B_a_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_a_set_fun$'__0| |tptp.'B_a_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'__0| |tptp.'Nat_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_b_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_b_prod_set$'__0| |tptp.'B_b_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_set_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_set_set_fun$'__0| |tptp.'ZF_ZF_set_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_set_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_set_prod_set$'__0| |tptp.'Nat_ZF_set_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_set$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_nat_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_nat_prod_set$'__0| |tptp.'Nat_nat_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'B$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B$'__0| |tptp.'B$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_set_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_set_bool_fun$'__0| |tptp.'ZF_set_set_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_ZF_set_fun$'__0| |tptp.'A_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_bool_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_bool_fun_set$'__0| |tptp.'B_bool_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_a_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_a_fun$'__0| |tptp.'ZF_set_a_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_nat_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_nat_fun_set$'__0| |tptp.'ZF_nat_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'B_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_ZF_set_fun$'__0| |tptp.'B_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_nat_ZF_ZF_set_prod_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_nat_ZF_ZF_set_prod_fun_fun$'__0| |tptp.'ZF_ZF_prod_nat_ZF_ZF_set_prod_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_set_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_set_fun_fun$'__0| |tptp.'ZF_ZF_ZF_set_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_ZF_set_ZF_set_prod_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_ZF_set_ZF_set_prod_fun_fun$'__0| |tptp.'Nat_ZF_ZF_set_ZF_set_prod_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_set_ZF_set_bool_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_set_ZF_set_bool_fun_fun$'__0| |tptp.'ZF_set_set_ZF_set_bool_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_set_ZF_set_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_set_ZF_set_prod_fun$'__0| |tptp.'ZF_ZF_set_ZF_set_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'__0| |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_nat_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_nat_fun$'__0| |tptp.'Nat_nat_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'C$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'C$'__0| |tptp.'C$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_a_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_a_set_fun$'__0| |tptp.'ZF_a_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_b_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_b_fun$'__0| |tptp.'ZF_b_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_set_set_ZF_set_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_set_set_ZF_set_set_fun$'__0| |tptp.'ZF_set_set_set_ZF_set_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat$'__0| |tptp.'Nat$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_set_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_set_set_fun$'__0| |tptp.'Nat_ZF_set_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_set_ZF_set_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_set_ZF_set_set_fun$'__0| |tptp.'Nat_set_ZF_set_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_nat_prod_ZF_ZF_prod_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_nat_prod_ZF_ZF_prod_set_fun$'__0| |tptp.'Nat_nat_prod_ZF_ZF_prod_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_b_prod_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_b_prod_bool_fun$'__0| |tptp.'B_b_prod_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_ZF_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_ZF_prod_fun$'__0| |tptp.'Nat_ZF_ZF_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_fun_set$'__0| |tptp.'ZF_ZF_prod_ZF_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_bool_fun$'__0| |tptp.'ZF_ZF_prod_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_set_ZF_set_set_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_set_ZF_set_set_set_fun$'__0| |tptp.'ZF_set_set_ZF_set_set_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_set_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_set_ZF_set_fun$'__0| |tptp.'Nat_set_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_fun_set$'__0| |tptp.'ZF_ZF_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_nat_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_nat_prod_set$'__0| |tptp.'ZF_ZF_prod_nat_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'B_b_prod_b_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_b_prod_b_fun_set$'__0| |tptp.'B_b_prod_b_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_nat_prod_ZF_set_ZF_set_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_nat_prod_ZF_set_ZF_set_prod_fun$'__0| |tptp.'Nat_nat_prod_ZF_set_ZF_set_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_prod_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_prod_prod_set$'__0| |tptp.'ZF_ZF_ZF_prod_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_ZF_prod$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_ZF_prod$'__0| |tptp.'ZF_set_ZF_prod$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_set_ZF_set_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_set_ZF_set_prod_fun$'__0| |tptp.'Nat_ZF_set_ZF_set_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_set_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_set_set$'__0| |tptp.'ZF_ZF_prod_set_set$'|) % 141.61/141.98 ; cardinality of |tptp.'B_a_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_a_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_a_fun$'__0| |tptp.'ZF_a_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_set_prod$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_set_prod$'__0| |tptp.'ZF_ZF_set_prod$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of tptp.tlbool is 2 % 141.61/141.98 ; rep: (as @tptp.tlbool_0 tptp.tlbool) % 141.61/141.98 ; rep: (as @tptp.tlbool_1 tptp.tlbool) % 141.61/141.98 ; cardinality of |tptp.'ZF_nat_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_nat_prod_set$'__0| |tptp.'ZF_nat_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_set_ZF_set_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_set_ZF_set_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_set_ZF_set_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_b_prod$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_b_prod$'__0| |tptp.'B_b_prod$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_set_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_set_ZF_set_fun$'__0| |tptp.'ZF_set_set_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_fun_ZF_ZF_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_set_a_bool_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_set_a_bool_fun_fun$'__0| |tptp.'A_set_a_bool_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_prod_ZF_ZF_prod_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_prod_ZF_ZF_prod_set_fun$'__0| |tptp.'Nat_ZF_prod_ZF_ZF_prod_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_nat_fun_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_nat_fun_ZF_set_fun$'__0| |tptp.'ZF_nat_fun_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_ZF_prod_ZF_ZF_prod_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_ZF_ZF_prod_fun_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_ZF_ZF_prod_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_a_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_a_set_fun$'__0| |tptp.'A_a_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'| is 1 % 141.61/141.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$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_ZF_set_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_ZF_set_set_fun$'__0| |tptp.'ZF_set_ZF_set_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_nat_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_nat_set_fun$'__0| |tptp.'Nat_nat_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_b_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_nat_prod_ZF_set_ZF_set_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_nat_prod_ZF_set_ZF_set_prod_fun$'__0| |tptp.'ZF_nat_prod_ZF_set_ZF_set_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_ZF_prod_set_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_ZF_ZF_prod_set_fun_fun$'__0| |tptp.'ZF_ZF_ZF_ZF_prod_set_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_nat_ZF_ZF_prod_set_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_nat_ZF_ZF_prod_set_fun_fun$'__0| |tptp.'Nat_nat_ZF_ZF_prod_set_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_b_fun_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_b_fun_bool_fun$'__0| |tptp.'A_b_fun_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_ZF_prod_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_ZF_prod_set_fun$'__0| |tptp.'Nat_ZF_ZF_prod_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A$'__0| |tptp.'A$'|) % 141.61/141.98 ; cardinality of |tptp.'B_set_b_bool_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_set_b_bool_fun_fun$'__0| |tptp.'B_set_b_bool_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_unit_Category_ext$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_unit_Category_ext$'__0| |tptp.'ZF_ZF_unit_Category_ext$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_ZF_bool_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_ZF_bool_fun_fun$'__0| |tptp.'ZF_set_ZF_bool_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_fun_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_fun_bool_fun$'__0| |tptp.'ZF_ZF_fun_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_ZF_ZF_set_prod_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_ZF_ZF_set_prod_fun_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_ZF_set_prod_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_nat_ZF_set_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_nat_ZF_set_fun_fun$'__0| |tptp.'Nat_nat_ZF_set_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_set_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_set_ZF_set_fun$'__0| |tptp.'ZF_ZF_prod_set_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_set_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_set_bool_fun$'__0| |tptp.'B_set_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_b_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_b_set_fun$'__0| |tptp.'A_b_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_b_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_b_fun$'__0| |tptp.'Nat_b_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_ZF_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_ZF_prod_set$'__0| |tptp.'ZF_set_ZF_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'B_set_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_set_set$'__0| |tptp.'B_set_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_ZF_set_prod$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_ZF_set_prod$'__0| |tptp.'ZF_set_ZF_set_prod$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_ZF_set_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_ZF_set_prod_fun$'__0| |tptp.'Nat_ZF_ZF_set_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_b_prod_b_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_b_prod_b_fun$'__0| |tptp.'B_b_prod_b_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_ZF_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_ZF_fun$'__0| |tptp.'ZF_set_ZF_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_set_b_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_set_b_set_fun$'__0| |tptp.'B_set_b_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_set_set_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_set_set_ZF_set_fun$'__0| |tptp.'ZF_ZF_prod_set_set_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_a_fun_b_a_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_a_fun_b_a_fun_fun$'__0| |tptp.'B_a_fun_b_a_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_a_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_prod_ZF_set_ZF_set_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_prod_ZF_set_ZF_set_prod_fun$'__0| |tptp.'Nat_ZF_prod_ZF_set_ZF_set_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_b_b_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_b_b_fun_fun$'__0| |tptp.'B_b_b_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_set_ZF_set_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_set_ZF_set_set_fun$'__0| |tptp.'ZF_set_set_ZF_set_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_prod_ZF_ZF_set_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_prod_ZF_ZF_set_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_prod_ZF_ZF_set_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_set_set_ZF_set_set_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_set_set_ZF_set_set_set_fun$'__0| |tptp.'Nat_set_set_ZF_set_set_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$'| is 1 % 141.61/141.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$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_nat_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_nat_fun$'__0| |tptp.'ZF_nat_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_ZF_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_ZF_fun$'__0| |tptp.'A_ZF_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_set_a_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_set_a_set_fun$'__0| |tptp.'A_set_a_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_prod_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_ZF_prod_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_nat_prod_ZF_ZF_set_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_nat_prod_ZF_ZF_set_prod_fun$'__0| |tptp.'ZF_ZF_prod_nat_prod_ZF_ZF_set_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Unit$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_bool_fun$'__0| |tptp.'Nat_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Bool_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Bool_set$'__0| |tptp.'Bool_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|) % 141.61/141.98 ; cardinality of |tptp.'B_ZF_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_ZF_fun$'__0| |tptp.'B_ZF_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_set_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_set_set$'__0| |tptp.'ZF_set_set_set$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_set_ZF_ZF_prod_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_set_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_set_ZF_ZF_prod_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_a_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_a_fun_set$'__0| |tptp.'B_a_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_fun_ZF_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_fun_ZF_set_fun$'__0| |tptp.'Nat_ZF_fun_ZF_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_set$'__0| |tptp.'Nat_set$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'__0| |tptp.'Nat_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_bool_fun_set$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_bool_fun_set$'__0| |tptp.'ZF_bool_fun_set$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_fun$'__0| |tptp.'Nat_ZF_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_ZF_prod_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_a_fun_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_a_fun_bool_fun$'__0| |tptp.'B_a_fun_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_ZF_ZF_prod_set_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_ZF_ZF_prod_set_fun_fun$'__0| |tptp.'Nat_ZF_ZF_ZF_prod_set_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'Nat_ZF_ZF_set_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'Nat_ZF_ZF_set_fun_fun$'__0| |tptp.'Nat_ZF_ZF_set_fun_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_b_set_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_b_set_fun$'__0| |tptp.'B_b_set_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'A_set_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'A_set_bool_fun$'__0| |tptp.'A_set_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_prod_ZF_set_ZF_prod_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_prod_ZF_set_ZF_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_set_ZF_prod_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'B_ZF_fun_bool_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'B_ZF_fun_bool_fun$'__0| |tptp.'B_ZF_fun_bool_fun$'|) % 141.61/141.98 ; cardinality of |tptp.'ZF_ZF_bool_fun_fun$'| is 1 % 141.61/141.98 ; rep: (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|) % 141.61/141.98 (define-fun |tptp.'sup$'| () |tptp.'ZF_set_set_ZF_set_fun$'| (as |@_tptp.'ZF_set_set_ZF_set_fun$'__0| |tptp.'ZF_set_set_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$ai'| (($x1 |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_ZF_ZF_prod_fun$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_set$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'mor_update$a'| (($x1 |tptp.'B_set_b_set_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$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$e'| (($x1 |tptp.'ZF_ZF_prod_set$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'fun_app$ah'| (($x1 |tptp.'ZF_nat_bool_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'Nat_bool_fun$'| (as |@_tptp.'Nat_bool_fun$'__0| |tptp.'Nat_bool_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'oppositeCategory$'| ((BOUND_VARIABLE_69480 |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$'|)) % 141.61/141.98 (define-fun |tptp.'uxn$'| (($x1 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_ZF_ZF_prod_set_fun$'| (as |@_tptp.'ZF_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_ZF_ZF_prod_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sigma$b'| (($x1 |tptp.'ZF_set$'|) ($x2 |tptp.'ZF_nat_set_fun$'|)) |tptp.'ZF_nat_prod_set$'| (as |@_tptp.'ZF_nat_prod_set$'__0| |tptp.'ZF_nat_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bv'| (($x1 |tptp.'ZF_ZF_prod_nat_ZF_ZF_set_prod_fun_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) |tptp.'Nat_ZF_ZF_set_prod_fun$'| (as |@_tptp.'Nat_ZF_ZF_set_prod_fun$'__0| |tptp.'Nat_ZF_ZF_set_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sup$d'| () |tptp.'ZF_ZF_prod_set_set_ZF_ZF_prod_set_fun$'| (as |@_tptp.'ZF_ZF_prod_set_set_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_ZF_prod_set_set_ZF_ZF_prod_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uxj$'| () |tptp.'ZF_ZF_ZF_ZF_prod_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_ZF_prod_fun_fun$'__0| |tptp.'ZF_ZF_ZF_ZF_prod_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'relInvImage$b'| (($x1 |tptp.'ZF_ZF_prod_set$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|) ($x3 |tptp.'ZF_ZF_prod_ZF_fun$'|)) |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_set$'| (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_set$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_set$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'image$bg'| (($x1 |tptp.'ZF_ZF_prod_ZF_ZF_prod_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_ZF_prod_set_set$'| (as |@_tptp.'ZF_ZF_prod_set_set$'__0| |tptp.'ZF_ZF_prod_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'rec_set_unit$'| ((_arg_1 |tptp.'ZF$'|) (_arg_2 |tptp.'Unit$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uua$'| () |tptp.'B_set_b_bool_fun_fun$'| (as |@_tptp.'B_set_b_bool_fun_fun$'__0| |tptp.'B_set_b_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'functorM$'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'relcomp$'| (($x1 |tptp.'ZF_ZF_prod_set$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uwa$'| (($x1 |tptp.'B_ZF_fun$'|) ($x2 |tptp.'B_set$'|) ($x3 |tptp.'ZF_bool_fun$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'vah$'| () |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'mapO$a'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|)) |tptp.'A_a_fun$'| (as |@_tptp.'A_a_fun$'__0| |tptp.'A_a_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uwl$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'vas$'| (($x1 |tptp.'Nat_nat_ZF_set_fun_fun$'|) ($x2 |tptp.'Nat_nat_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$b'| (($x1 |tptp.'ZF_ZF_ZF_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uyt$'| (($x1 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_set_ZF_set_fun$'| (as |@_tptp.'Nat_set_ZF_set_fun$'__0| |tptp.'Nat_set_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ak'| (($x1 |tptp.'ZF_ZF_prod_bool_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'constFunctor$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x3 |tptp.'A$'|)) |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'| (as |@_tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|)) % 141.61/141.98 (define-fun |tptp.'vbb$'| (($x1 |tptp.'Nat_nat_ZF_set_fun_fun$'|)) |tptp.'Nat_nat_fun_ZF_set_fun$'| (as |@_tptp.'Nat_nat_fun_ZF_set_fun$'__0| |tptp.'Nat_nat_fun_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'the$a'| (($x1 |tptp.'B_bool_fun$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'compDefined$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'uyq$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'Nat_nat_set_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sigma$g'| (($x1 |tptp.'ZF_ZF_prod_set$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_set_fun$'|)) |tptp.'ZF_ZF_prod_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uwx$'| (($x1 |tptp.'Nat_ZF_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'constFunctor$d'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x3 |tptp.'A$'|)) |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'| (as |@_tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) % 141.61/141.98 (define-fun |tptp.'comp$f'| (($x1 |tptp.'ZF_set_ZF_set_set_fun$'|) ($x2 |tptp.'ZF_set_set_ZF_set_fun$'|)) |tptp.'ZF_set_set_ZF_set_set_fun$'| (as |@_tptp.'ZF_set_set_ZF_set_set_fun$'__0| |tptp.'ZF_set_set_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sup$c'| ((BOUND_VARIABLE_69494 |tptp.'B_set_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bk'| (($x1 |tptp.'B_a_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 141.61/141.98 (define-fun |tptp.'image$z'| (($x1 |tptp.'ZF_ZF_ZF_prod_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$f'| (($x1 |tptp.'ZF_ZF_set_prod_set$'|) ($x2 |tptp.'ZF_ZF_set_prod_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'extensional$e'| (($x1 |tptp.'B_set$'|)) |tptp.'B_ZF_fun_set$'| (as |@_tptp.'B_ZF_fun_set$'__0| |tptp.'B_ZF_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'rec_unit$'| ((BOUND_VARIABLE_69509 |tptp.'ZF$'|) (BOUND_VARIABLE_69511 |tptp.'Unit$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 141.61/141.98 (define-fun |tptp.'lSCategory$'| ((BOUND_VARIABLE_69522 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'uzv$'| (($x1 |tptp.'ZF_ZF_bool_fun_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'member$c'| (($x1 |tptp.'A$'|)) |tptp.'A_set_bool_fun$'| (as |@_tptp.'A_set_bool_fun$'__0| |tptp.'A_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'inf$'| (($x1 |tptp.'ZF_set_set$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'sup$h'| (($x1 |tptp.'B_bool_fun_set$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'cod_update$'| (($x1 |tptp.'ZF_ZF_fun_ZF_ZF_fun_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$'|)) % 141.61/141.98 (define-fun |tptp.'rec_bool$'| ((BOUND_VARIABLE_69546 |tptp.'ZF$'|) (BOUND_VARIABLE_69548 |tptp.'ZF$'|) (BOUND_VARIABLE_69550 tptp.tlbool)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 141.61/141.98 (define-fun |tptp.'member$a'| (($x1 |tptp.'ZF_set$'|)) |tptp.'ZF_set_set_bool_fun$'| (as |@_tptp.'ZF_set_set_bool_fun$'__0| |tptp.'ZF_set_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uyh$'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$av'| (($x1 |tptp.'ZF_ZF_ZF_prod_set_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$dd'| (($x1 |tptp.'ZF_set_set_ZF_set_set_set_fun$'|) ($x2 |tptp.'ZF_set_set$'|)) |tptp.'ZF_set_set_set$'| (as |@_tptp.'ZF_set_set_set$'__0| |tptp.'ZF_set_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'sigma$k'| (($x1 |tptp.'ZF_ZF_prod_set$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_ZF_prod_set_fun$'|)) |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_set$'| (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_set$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_set$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ai'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 141.61/141.98 (define-fun |tptp.'uwk$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cr'| (($x1 |tptp.'A_a_set_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.61/141.98 (define-fun |tptp.'obj_update$'| (($x1 |tptp.'A_set_a_set_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$'|)) % 141.61/141.98 (define-fun |tptp.'uux$'| (($x1 |tptp.'A_set$'|) ($x2 |tptp.'A_bool_fun$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'top$i'| () |tptp.'Nat_nat_fun_set$'| (as |@_tptp.'Nat_nat_fun_set$'__0| |tptp.'Nat_nat_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$bq'| (($x1 |tptp.'Nat_nat_fun_ZF_set_fun$'|) ($x2 |tptp.'Nat_nat_fun_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'uwd$'| (($x1 |tptp.'ZF_set_a_fun$'|) ($x2 |tptp.'ZF_set_set$'|) ($x3 |tptp.'A_bool_fun$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uyb$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_nat_ZF_set_ZF_set_prod_fun_fun$'| (as |@_tptp.'Nat_nat_ZF_set_ZF_set_prod_fun_fun$'__0| |tptp.'Nat_nat_ZF_set_ZF_set_prod_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uuw$'| () |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'id_update$'| (($x1 |tptp.'ZF_ZF_fun_ZF_ZF_fun_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$'|)) % 141.61/141.98 (define-fun |tptp.'image$e'| (($x1 |tptp.'A_set_bool_fun$'|) ($x2 |tptp.'A_set_set$'|)) |tptp.'Bool_set$'| (as |@_tptp.'Bool_set$'__0| |tptp.'Bool_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$o'| (($x1 |tptp.'A_set_a_bool_fun_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'inverse_rel$'| (($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$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$co'| (($x1 |tptp.'A_ZF_set_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'uwp$'| (($x1 |tptp.'ZF_set_ZF_fun$'|) ($x2 |tptp.'ZF_set_set$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$k'| (($x1 |tptp.'B_bool_fun$'|) ($x2 |tptp.'B_bool_fun$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'fun_app$bn'| (($x1 |tptp.'ZF_ZF_ZF_ZF_prod_set_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_ZF_prod_set_fun$'| (as |@_tptp.'ZF_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_ZF_ZF_prod_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'top$b'| () |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'f$'| () |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 141.61/141.98 (define-fun |tptp.'uye$'| (($x1 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_ZF_prod_ZF_ZF_prod_set_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'comp$g'| (($x1 |tptp.'ZF_set_set_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set_set_ZF_set_set_fun$'|)) |tptp.'ZF_ZF_prod_set_set_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_prod_set_set_ZF_set_fun$'__0| |tptp.'ZF_ZF_prod_set_set_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sup$j'| (($x1 |tptp.'ZF_bool_fun_set$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$f'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|)) |tptp.'ZF_ZF_prod_set_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_prod_set_ZF_set_fun$'__0| |tptp.'ZF_ZF_prod_set_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uww$'| (($x1 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'member$l'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_fun_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'image$'| (($x1 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_set_ZF_set_set_fun$'| (as |@_tptp.'Nat_set_ZF_set_set_fun$'__0| |tptp.'Nat_set_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$aa'| (($x1 |tptp.'Nat_nat_ZF_set_fun_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cg'| (($x1 |tptp.'ZF_ZF_prod_nat_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) |tptp.'Nat_set$'| (as |@_tptp.'Nat_set$'__0| |tptp.'Nat_set$'|)) % 141.61/141.98 (define-fun |tptp.'top$e'| () |tptp.'Nat_nat_prod_set$'| (as |@_tptp.'Nat_nat_prod_set$'__0| |tptp.'Nat_nat_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'top$d'| () |tptp.'Nat_ZF_prod_set$'| (as |@_tptp.'Nat_ZF_prod_set$'__0| |tptp.'Nat_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$ac'| (($x1 |tptp.'ZF_nat_prod_ZF_set_ZF_set_prod_fun$'|) ($x2 |tptp.'ZF_nat_prod_set$'|)) |tptp.'ZF_set_ZF_set_prod_set$'| (as |@_tptp.'ZF_set_ZF_set_prod_set$'__0| |tptp.'ZF_set_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'category$a'| ((BOUND_VARIABLE_69599 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'converse$'| (($x1 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uwv$'| (($x1 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uzb$'| (($x1 |tptp.'Nat_ZF_ZF_set_fun_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uxi$'| (($x1 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uxl$'| (($x1 |tptp.'ZF_ZF_bool_fun_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bf'| (($x1 |tptp.'A_ZF_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 141.61/141.98 (define-fun |tptp.'uur$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uxh$'| (($x1 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'comp$j'| (($x1 |tptp.'ZF_set_ZF_set_fun$'|) ($x2 |tptp.'ZF_set_set_ZF_set_fun$'|)) |tptp.'ZF_set_set_ZF_set_fun$'| (as |@_tptp.'ZF_set_set_ZF_set_fun$'__0| |tptp.'ZF_set_set_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'gr$'| (($x1 |tptp.'ZF_set$'|) ($x2 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_ZF_set_prod_set$'| (as |@_tptp.'ZF_ZF_set_prod_set$'__0| |tptp.'ZF_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'comp$e'| (($x1 |tptp.'ZF_set_set_set_ZF_set_set_fun$'|) ($x2 |tptp.'ZF_set_set_ZF_set_set_set_fun$'|)) |tptp.'ZF_set_set_ZF_set_set_fun$'| (as |@_tptp.'ZF_set_set_ZF_set_set_fun$'__0| |tptp.'ZF_set_set_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uuh$'| (($x1 tptp.tlbool) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sigma$f'| (($x1 |tptp.'ZF_set_set$'|) ($x2 |tptp.'ZF_set_ZF_set_fun$'|)) |tptp.'ZF_set_ZF_prod_set$'| (as |@_tptp.'ZF_set_ZF_prod_set$'__0| |tptp.'ZF_set_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'sigma$'| ((BOUND_VARIABLE_69614 |tptp.'ZF_set$'|) (BOUND_VARIABLE_69616 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'sup$i'| (($x1 |tptp.'ZF_set_bool_fun_set$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'uyp$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'ZF_nat_set_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'functorM$b'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'category$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'vao$'| (($x1 |tptp.'Nat_ZF_ZF_set_fun_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uzn$'| (($x1 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_ZF_ZF_set_fun_fun$'| (as |@_tptp.'Nat_ZF_ZF_set_fun_fun$'__0| |tptp.'Nat_ZF_ZF_set_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$m'| (($x1 |tptp.'B_a_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.61/141.98 (define-fun |tptp.'uzs$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'extensional$c'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'uut$'| () |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'uzp$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'collect$i'| (($x1 |tptp.'B_bool_fun$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 141.61/141.98 (define-fun |tptp.'uve$'| (($x1 |tptp.'ZF_set_ZF_set_fun$'|) ($x2 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'functorM$a'| (($x1 |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'uyc$'| (($x1 |tptp.'Nat_set$'|)) |tptp.'Nat_nat_set_fun$'| (as |@_tptp.'Nat_nat_set_fun$'__0| |tptp.'Nat_nat_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sum$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$a'| (($x1 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_set_ZF_set_set_fun$'| (as |@_tptp.'ZF_set_ZF_set_set_fun$'__0| |tptp.'ZF_set_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$bc'| (($x1 |tptp.'Nat_ZF_set_set_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_set_set_set$'| (as |@_tptp.'ZF_set_set_set$'__0| |tptp.'ZF_set_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'makeCat$'| ((BOUND_VARIABLE_69480 |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$'|)) % 141.61/141.98 (define-fun |tptp.'image$p'| (($x1 |tptp.'A_a_fun$'|)) |tptp.'A_set_a_set_fun$'| (as |@_tptp.'A_set_a_set_fun$'__0| |tptp.'A_set_a_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uub$'| () |tptp.'ZF_set_set_ZF_set_bool_fun_fun$'| (as |@_tptp.'ZF_set_set_ZF_set_bool_fun_fun$'__0| |tptp.'ZF_set_set_ZF_set_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$bh'| (($x1 |tptp.'A_set_a_bool_fun_fun$'|) ($x2 |tptp.'A_set_set$'|)) |tptp.'A_bool_fun_set$'| (as |@_tptp.'A_bool_fun_set$'__0| |tptp.'A_bool_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$aq'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'mor$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'uxa$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_set_ZF_set_set_fun$'| (as |@_tptp.'ZF_set_ZF_set_set_fun$'__0| |tptp.'ZF_set_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sigma$c'| (($x1 |tptp.'Nat_set$'|) ($x2 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_ZF_prod_set$'| (as |@_tptp.'Nat_ZF_prod_set$'__0| |tptp.'Nat_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ck'| ((BOUND_VARIABLE_69644 |tptp.'B_a_fun_bool_fun$'|) (BOUND_VARIABLE_69646 |tptp.'B_a_fun$'|)) Bool false) % 141.61/141.98 (define-fun |tptp.'app$'| () |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'catDom$'| (($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$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'uui$'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'uuz$'| (($x1 |tptp.'ZF_set_set$'|) ($x2 |tptp.'ZF_set_bool_fun$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uuj$'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$m'| (($x1 |tptp.'ZF_set_bool_fun$'|) ($x2 |tptp.'ZF_set_bool_fun$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'extensional$a'| (($x1 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_fun_set$'| (as |@_tptp.'ZF_ZF_fun_set$'__0| |tptp.'ZF_ZF_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ay'| (($x1 |tptp.'Nat_ZF_set_set_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'uzg$'| (($x1 |tptp.'Nat_nat_ZF_set_fun_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sigma$e'| (($x1 |tptp.'ZF_set$'|) ($x2 |tptp.'ZF_ZF_ZF_prod_set_fun$'|)) |tptp.'ZF_ZF_ZF_prod_prod_set$'| (as |@_tptp.'ZF_ZF_ZF_prod_prod_set$'__0| |tptp.'ZF_ZF_ZF_prod_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'unity$'| () |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$az'| (($x1 |tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) |tptp.'ZF_ZF_prod$'| (as |@_tptp.'ZF_ZF_prod$'__0| |tptp.'ZF_ZF_prod$'|)) % 141.61/141.98 (define-fun |tptp.'uwr$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'Nat_ZF_ZF_prod_fun$'|)) |tptp.'Nat_ZF_fun$'| (as |@_tptp.'Nat_ZF_fun$'__0| |tptp.'Nat_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$ah'| (($x1 |tptp.'Nat_nat_prod_ZF_set_ZF_set_prod_fun$'|) ($x2 |tptp.'Nat_nat_prod_set$'|)) |tptp.'ZF_set_ZF_set_prod_set$'| (as |@_tptp.'ZF_set_ZF_set_prod_set$'__0| |tptp.'ZF_set_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$h'| ((BOUND_VARIABLE_69671 |tptp.'ZF_set_bool_fun$'|) (BOUND_VARIABLE_69673 |tptp.'ZF_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'sup$f'| () |tptp.'Nat_set_set_nat_set_fun$'| (as |@_tptp.'Nat_set_set_nat_set_fun$'__0| |tptp.'Nat_set_set_nat_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$h'| (($x1 |tptp.'ZF_b_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 141.61/141.98 (define-fun |tptp.'uwt$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uyv$'| (($x1 |tptp.'ZF_ZF_ZF_set_fun_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'repl$'| (($x1 |tptp.'ZF$'|) ($x2 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 141.61/141.98 (define-fun |tptp.'inf$b'| (($x1 |tptp.'B_set_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$x'| (($x1 |tptp.'ZF_set_ZF_set_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'comp$d'| (($x1 |tptp.'Nat_set_ZF_set_set_fun$'|) ($x2 |tptp.'Nat_set_set_nat_set_fun$'|)) |tptp.'Nat_set_set_ZF_set_set_fun$'| (as |@_tptp.'Nat_set_set_ZF_set_set_fun$'__0| |tptp.'Nat_set_set_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'val$'| (($x1 |tptp.'ZF_nat_ZF_set_fun_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'obj_update$a'| (($x1 |tptp.'ZF_set_ZF_set_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$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'uva$'| (($x1 |tptp.'ZF_set$'|) ($x2 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'functor$b'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'comp_update$'| (($x1 |tptp.'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_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$'|)) % 141.61/141.98 (define-fun |tptp.'uxy$'| (($x1 |tptp.'ZF_set$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'functor$a'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'uvg$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'Nat_ZF_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uvi$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'|)) |tptp.'ZF_ZF_prod_ZF_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_fun$'__0| |tptp.'ZF_ZF_prod_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'extensional$b'| (($x1 |tptp.'A_set$'|)) |tptp.'A_b_fun_set$'| (as |@_tptp.'A_b_fun_set$'__0| |tptp.'A_b_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ca'| (($x1 |tptp.'Nat_ZF_set_ZF_set_prod_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF_set_ZF_set_prod$'| (as |@_tptp.'ZF_set_ZF_set_prod$'__0| |tptp.'ZF_set_ZF_set_prod$'|)) % 141.61/141.98 (define-fun |tptp.'uvb$'| (($x1 |tptp.'ZF_bool_fun$'|) ($x2 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$bj'| (($x1 |tptp.'ZF_set_set_ZF_set_bool_fun_fun$'|) ($x2 |tptp.'ZF_set_set_set$'|)) |tptp.'ZF_set_bool_fun_set$'| (as |@_tptp.'ZF_set_bool_fun_set$'__0| |tptp.'ZF_set_bool_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bw'| (($x1 |tptp.'ZF_ZF_prod_ZF_set_ZF_prod_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) |tptp.'ZF_set_ZF_prod$'| (as |@_tptp.'ZF_set_ZF_prod$'__0| |tptp.'ZF_set_ZF_prod$'|)) % 141.61/141.98 (define-fun |tptp.'uuk$'| (($x1 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$'| (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$'|)) % 141.61/141.98 (define-fun |tptp.'gr$a'| (($x1 |tptp.'ZF_ZF_prod_set$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_fun$'|)) |tptp.'ZF_ZF_prod_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uxb$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'dom_update$'| (($x1 |tptp.'B_a_fun_b_a_fun_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$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$f'| ((BOUND_VARIABLE_69690 |tptp.'ZF_bool_fun$'|) (BOUND_VARIABLE_69692 |tptp.'ZF$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'vaw$'| (($x1 |tptp.'ZF_nat_ZF_set_fun_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'zFfun$'| ((BOUND_VARIABLE_69720 |tptp.'ZF$'|) (BOUND_VARIABLE_69722 |tptp.'ZF$'|) (BOUND_VARIABLE_69724 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cx'| (($x1 |tptp.'B_ZF_set_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'member$j'| (($x1 |tptp.'B_b_prod$'|) ($x2 |tptp.'B_b_prod_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'image$az'| (($x1 |tptp.'ZF_ZF_ZF_prod_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_prod_set_set$'| (as |@_tptp.'ZF_ZF_prod_set_set$'__0| |tptp.'ZF_ZF_prod_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'vba$'| (($x1 |tptp.'Nat_nat_ZF_set_fun_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uvo$'| (($x1 |tptp.'B_a_fun$'|) ($x2 |tptp.'B_set$'|) ($x3 |tptp.'A_bool_fun$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'preFunctor$b'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) Bool false) % 141.61/141.98 (define-fun |tptp.'image$as'| (($x1 |tptp.'ZF_set_ZF_ZF_prod_set_fun$'|) ($x2 |tptp.'ZF_set_set$'|)) |tptp.'ZF_ZF_prod_set_set$'| (as |@_tptp.'ZF_ZF_prod_set_set$'__0| |tptp.'ZF_ZF_prod_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'comp$h'| (($x1 |tptp.'ZF_ZF_prod_set_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set_set_ZF_ZF_prod_set_fun$'|)) |tptp.'ZF_ZF_prod_set_set_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_prod_set_set_ZF_set_fun$'__0| |tptp.'ZF_ZF_prod_set_set_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'identityFunctor$b'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'member$k'| (($x1 |tptp.'B_b_prod_b_fun$'|) ($x2 |tptp.'B_b_prod_b_fun_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'pair$'| (($x1 |tptp.'ZF$'|)) |tptp.'ZF_ZF_ZF_prod_fun$'| (as |@_tptp.'ZF_ZF_ZF_prod_fun$'__0| |tptp.'ZF_ZF_ZF_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'case_prod$n'| (($x1 |tptp.'Nat_ZF_ZF_ZF_prod_set_fun_fun$'|)) |tptp.'Nat_ZF_prod_ZF_ZF_prod_set_fun$'| (as |@_tptp.'Nat_ZF_prod_ZF_ZF_prod_set_fun$'__0| |tptp.'Nat_ZF_prod_ZF_ZF_prod_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uvh$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_fun$'|)) |tptp.'ZF_ZF_prod_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_set_fun$'__0| |tptp.'ZF_ZF_prod_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'vac$'| (($x1 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_ZF_bool_fun_fun$'| (as |@_tptp.'Nat_ZF_bool_fun_fun$'__0| |tptp.'Nat_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$w'| (($x1 |tptp.'ZF_nat_fun_ZF_set_fun$'|) ($x2 |tptp.'ZF_nat_fun$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'vax$'| (($x1 |tptp.'ZF_nat_ZF_set_fun_fun$'|)) |tptp.'Nat_ZF_fun_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_fun_ZF_set_fun$'__0| |tptp.'Nat_ZF_fun_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$an'| (($x1 |tptp.'B_b_set_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_set_set$'| (as |@_tptp.'B_set_set$'__0| |tptp.'B_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'obj$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'uwf$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'Nat_bool_fun$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'top$g'| () |tptp.'Nat_ZF_fun_set$'| (as |@_tptp.'Nat_ZF_fun_set$'__0| |tptp.'Nat_ZF_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'uvr$'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B_set$'|) ($x3 |tptp.'B_bool_fun$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uwu$'| (($x1 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$aj'| (($x1 |tptp.'Nat_ZF_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 141.61/141.98 (define-fun |tptp.'lSCategory_axioms$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'uzm$'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ct'| (($x1 |tptp.'B_a_set_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.61/141.98 (define-fun |tptp.'uvu$'| (($x1 |tptp.'ZF_a_fun$'|) ($x2 |tptp.'ZF_set$'|) ($x3 |tptp.'A_bool_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uze$'| (($x1 |tptp.'Nat_nat_ZF_set_fun_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'zFfunCod$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$ax'| (($x1 |tptp.'Nat_nat_set_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'Nat_set_set$'| (as |@_tptp.'Nat_set_set$'__0| |tptp.'Nat_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'uyl$'| (($x1 |tptp.'ZF$'|)) |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'case_prod$l'| (($x1 |tptp.'ZF_ZF_ZF_set_ZF_set_prod_fun_fun$'|)) |tptp.'ZF_ZF_prod_ZF_set_ZF_set_prod_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_set_ZF_set_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_set_ZF_set_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uun$'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cn'| (($x1 |tptp.'ZF_set_set_ZF_set_set_fun$'|) ($x2 |tptp.'ZF_set_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$bb'| (($x1 |tptp.'ZF_ZF_set_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_set_set_set$'| (as |@_tptp.'ZF_set_set_set$'__0| |tptp.'ZF_set_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'uyg$'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF_ZF_ZF_ZF_prod_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_ZF_prod_fun_fun$'__0| |tptp.'ZF_ZF_ZF_ZF_prod_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uug$'| () |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uzd$'| (($x1 |tptp.'Nat_ZF_ZF_set_fun_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'var$'| (($x1 |tptp.'Nat_nat_ZF_set_fun_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'uxk$'| (($x1 |tptp.'ZF_bool_fun$'|) ($x2 |tptp.'ZF_ZF_bool_fun_fun$'|)) |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'vau$'| (($x1 |tptp.'ZF_ZF_ZF_set_fun_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bm'| (($x1 |tptp.'A_a_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 141.61/141.98 (define-fun |tptp.'uxm$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_fun$'|)) |tptp.'ZF_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'__0| |tptp.'ZF_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'extCategory$a'| ((BOUND_VARIABLE_69748 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool false) % 141.61/141.98 (define-fun |tptp.'vaf$'| (($x1 |tptp.'ZF_set_set_set$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'collect$b'| (($x1 |tptp.'B_b_prod_bool_fun$'|)) |tptp.'B_b_prod_set$'| (as |@_tptp.'B_b_prod_set$'__0| |tptp.'B_b_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uvz$'| (($x1 |tptp.'B_ZF_fun$'|) ($x2 |tptp.'B_set$'|) ($x3 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'cod$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_a_fun$'| (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|)) % 141.61/141.98 (define-fun |tptp.'collect$d'| ((_arg_1 |tptp.'B_ZF_fun_bool_fun$'|)) |tptp.'B_ZF_fun_set$'| (as |@_tptp.'B_ZF_fun_set$'__0| |tptp.'B_ZF_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cy'| (($x1 |tptp.'ZF_ZF_prod_set_set_ZF_ZF_prod_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set_set$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'case_prod$e'| (($x1 |tptp.'ZF_nat_ZF_set_ZF_set_prod_fun_fun$'|)) |tptp.'ZF_nat_prod_ZF_set_ZF_set_prod_fun$'| (as |@_tptp.'ZF_nat_prod_ZF_set_ZF_set_prod_fun$'__0| |tptp.'ZF_nat_prod_ZF_set_ZF_set_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ag'| ((BOUND_VARIABLE_69766 |tptp.'Nat_bool_fun$'|) (BOUND_VARIABLE_69768 |tptp.'Nat$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'sigma$a'| (($x1 |tptp.'ZF_set_set$'|) ($x2 |tptp.'ZF_set_ZF_set_set_fun$'|)) |tptp.'ZF_set_ZF_set_prod_set$'| (as |@_tptp.'ZF_set_ZF_set_prod_set$'__0| |tptp.'ZF_set_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uxg$'| (($x1 |tptp.'ZF_bool_fun$'|) ($x2 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'collect$c'| ((_arg_1 |tptp.'ZF_ZF_fun_bool_fun$'|)) |tptp.'ZF_ZF_fun_set$'| (as |@_tptp.'ZF_ZF_fun_set$'__0| |tptp.'ZF_ZF_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'uxp$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'ZF_nat_ZF_set_ZF_set_prod_fun_fun$'| (as |@_tptp.'ZF_nat_ZF_set_ZF_set_prod_fun_fun$'__0| |tptp.'ZF_nat_ZF_set_ZF_set_prod_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'relImage$a'| (($x1 |tptp.'Nat_nat_prod_set$'|) ($x2 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'ZF_set_ZF_set_prod_set$'| (as |@_tptp.'ZF_set_ZF_set_prod_set$'__0| |tptp.'ZF_set_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'sigma$h'| (($x1 |tptp.'ZF_set$'|) ($x2 |tptp.'ZF_ZF_set_set_fun$'|)) |tptp.'ZF_ZF_set_prod_set$'| (as |@_tptp.'ZF_ZF_set_prod_set$'__0| |tptp.'ZF_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'member$g'| (($x1 |tptp.'B_ZF_fun$'|) ($x2 |tptp.'B_ZF_fun_set$'|)) Bool true) % 141.61/141.98 (define-fun tptp.tltrue () tptp.tlbool (as @tptp.tlbool_1 tptp.tlbool)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'obj$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.61/141.98 (define-fun |tptp.'inverse$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_b_fun$'| (as |@_tptp.'B_b_fun$'__0| |tptp.'B_b_fun$'|)) % 141.61/141.98 (define-fun |tptp.'extCategory$'| ((BOUND_VARIABLE_69599 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'uxq$'| (($x1 |tptp.'Nat_set$'|)) |tptp.'ZF_nat_set_fun$'| (as |@_tptp.'ZF_nat_set_fun$'__0| |tptp.'ZF_nat_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uxo$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_set_ZF_set_fun$'| (as |@_tptp.'ZF_set_ZF_set_fun$'__0| |tptp.'ZF_set_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uvv$'| (($x1 |tptp.'ZF_b_fun$'|) ($x2 |tptp.'ZF_set$'|) ($x3 |tptp.'B_bool_fun$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bc'| (($x1 |tptp.'ZF_nat_set_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'Nat_set$'| (as |@_tptp.'Nat_set$'__0| |tptp.'Nat_set$'|)) % 141.61/141.98 (define-fun |tptp.'collect$j'| (($x1 |tptp.'ZF_set_bool_fun$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'uud$'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cd'| (($x1 |tptp.'Nat_ZF_ZF_set_ZF_set_prod_fun_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF_ZF_set_ZF_set_prod_fun$'| (as |@_tptp.'ZF_ZF_set_ZF_set_prod_fun$'__0| |tptp.'ZF_ZF_set_ZF_set_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$i'| (($x1 |tptp.'Nat_set$'|) ($x2 |tptp.'Nat_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'fun_app$cc'| (($x1 |tptp.'Nat_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF_ZF_prod_ZF_set_ZF_prod_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_set_ZF_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_set_ZF_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uzu$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_ZF_ZF_ZF_prod_set_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_ZF_prod_set_fun_fun$'__0| |tptp.'ZF_ZF_ZF_ZF_prod_set_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'vam$'| (($x1 |tptp.'ZF_nat_ZF_set_fun_fun$'|) ($x2 |tptp.'Nat_ZF_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uvc$'| (($x1 |tptp.'ZF_set_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'category_axioms$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'fun_app$ad'| (($x1 |tptp.'ZF_ZF_ZF_set_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'constFunctor$e'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$be'| (($x1 |tptp.'ZF_set_ZF_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 141.61/141.98 (define-fun |tptp.'uza$'| (($x1 |tptp.'ZF_nat_ZF_set_fun_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'mapsTo$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$aq'| (($x1 |tptp.'A_ZF_set_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'functor_abbrev$'| (($x1 |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x3 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'fun_app$bd'| (($x1 |tptp.'Nat_nat_set_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'Nat_set$'| (as |@_tptp.'Nat_set$'__0| |tptp.'Nat_set$'|)) % 141.61/141.98 (define-fun |tptp.'functorM$c'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'fun_app$bp'| (($x1 |tptp.'ZF_nat_ZF_ZF_prod_set_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'Nat_ZF_ZF_prod_set_fun$'| (as |@_tptp.'Nat_ZF_ZF_prod_set_fun$'__0| |tptp.'Nat_ZF_ZF_prod_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uvp$'| (($x1 |tptp.'A_b_fun$'|) ($x2 |tptp.'A_set$'|) ($x3 |tptp.'B_bool_fun$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bi'| (($x1 |tptp.'ZF_a_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 141.61/141.98 (define-fun |tptp.'image$al'| (($x1 |tptp.'A_b_set_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'B_set_set$'| (as |@_tptp.'B_set_set$'__0| |tptp.'B_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'case_prod$f'| (($x1 |tptp.'ZF_ZF_prod_ZF_ZF_ZF_set_prod_fun_fun$'|)) |tptp.'ZF_ZF_prod_ZF_prod_ZF_ZF_set_prod_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_prod_ZF_ZF_set_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_prod_ZF_ZF_set_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sup$g'| (($x1 |tptp.'A_bool_fun_set$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'homFtorContra$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A$'|)) |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'| (as |@_tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'__0| |tptp.'A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$'|)) % 141.61/141.98 (define-fun |tptp.'homFtorContra$'| ((BOUND_VARIABLE_69812 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) (BOUND_VARIABLE_69814 |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$'|)) % 141.61/141.98 (define-fun |tptp.'uyz$'| (($x1 |tptp.'ZF_nat_ZF_set_fun_fun$'|)) |tptp.'Nat_ZF_ZF_set_fun_fun$'| (as |@_tptp.'Nat_ZF_ZF_set_fun_fun$'__0| |tptp.'Nat_ZF_ZF_set_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$w'| ((BOUND_VARIABLE_69828 |tptp.'ZF_set_ZF_fun$'|) (BOUND_VARIABLE_69830 |tptp.'ZF_set_set$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'uxd$'| () |tptp.'ZF_nat_set_fun$'| (as |@_tptp.'ZF_nat_set_fun$'__0| |tptp.'ZF_nat_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$u'| (($x1 |tptp.'ZF_set_set_ZF_set_fun$'|) ($x2 |tptp.'ZF_set_set$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'inf$a'| (($x1 |tptp.'A_set_set$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$db'| (($x1 |tptp.'Nat_set_set_ZF_set_set_set_fun$'|) ($x2 |tptp.'Nat_set_set$'|)) |tptp.'ZF_set_set_set$'| (as |@_tptp.'ZF_set_set_set$'__0| |tptp.'ZF_set_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'uzw$'| (($x1 |tptp.'ZF_ZF_bool_fun_fun$'|)) |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$n'| ((BOUND_VARIABLE_69844 |tptp.'A_ZF_fun$'|) (BOUND_VARIABLE_69846 |tptp.'A_set$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$r'| (($x1 |tptp.'Nat_ZF_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$ak'| (($x1 |tptp.'A_a_set_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_set_set$'| (as |@_tptp.'A_set_set$'__0| |tptp.'A_set_set$'|)) % 141.61/141.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$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'oppositeCategory$a'| ((BOUND_VARIABLE_69861 |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$'|)) % 141.61/141.98 (define-fun |tptp.'the$'| (($x1 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 141.61/141.98 (define-fun |tptp.'constFunctor$a'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'image$ag'| (($x1 |tptp.'Nat_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'|) ($x2 |tptp.'Nat_ZF_ZF_prod_prod_set$'|)) |tptp.'ZF_set_ZF_prod_set$'| (as |@_tptp.'ZF_set_ZF_prod_set$'__0| |tptp.'ZF_set_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uwb$'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_set$'|) ($x3 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$a'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'uvw$'| (($x1 |tptp.'ZF_b_fun$'|) ($x2 |tptp.'ZF_set$'|) ($x3 |tptp.'B_bool_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'vap$'| (($x1 |tptp.'Nat_ZF_ZF_set_fun_fun$'|) ($x2 |tptp.'ZF_nat_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$as'| (($x1 |tptp.'ZF_b_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 141.61/141.98 (define-fun |tptp.'uzf$'| (($x1 |tptp.'Nat_nat_ZF_set_fun_fun$'|)) |tptp.'Nat_nat_ZF_set_fun_fun$'| (as |@_tptp.'Nat_nat_ZF_set_fun_fun$'__0| |tptp.'Nat_nat_ZF_set_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$ad'| (($x1 |tptp.'ZF_ZF_prod_ZF_prod_ZF_ZF_set_prod_fun$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_prod_set$'|)) |tptp.'ZF_ZF_set_prod_set$'| (as |@_tptp.'ZF_ZF_set_prod_set$'__0| |tptp.'ZF_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uxv$'| (($x1 |tptp.'Nat_set$'|)) |tptp.'ZF_ZF_prod_nat_set_fun$'| (as |@_tptp.'ZF_ZF_prod_nat_set_fun$'__0| |tptp.'ZF_ZF_prod_nat_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$af'| (($x1 |tptp.'Nat_set_ZF_set_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$g'| (($x1 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF_set_ZF_set_fun$'| (as |@_tptp.'ZF_set_ZF_set_fun$'__0| |tptp.'ZF_set_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'rec_set_bool$'| ((_arg_1 |tptp.'ZF$'|) (_arg_2 |tptp.'ZF$'|) (_arg_3 tptp.tlbool)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bh'| (($x1 |tptp.'A_set_a_set_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.61/141.98 (define-fun |tptp.'vag$'| (($x1 |tptp.'ZF_set_set$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'member$f'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_fun_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'uxr$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_ZF_prod_ZF_ZF_ZF_set_prod_fun_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_ZF_ZF_set_prod_fun_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_ZF_set_prod_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$br'| (($x1 |tptp.'ZF_ZF_prod_ZF_ZF_prod_ZF_ZF_prod_fun_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) |tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bx'| (($x1 |tptp.'ZF_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_prod_ZF_set_ZF_prod_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_set_ZF_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_set_ZF_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'case_prod$m'| (($x1 |tptp.'ZF_nat_ZF_ZF_prod_set_fun_fun$'|)) |tptp.'ZF_nat_prod_ZF_ZF_prod_set_fun$'| (as |@_tptp.'ZF_nat_prod_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_nat_prod_ZF_ZF_prod_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'case_prod$c'| (($x1 |tptp.'ZF_ZF_ZF_ZF_prod_fun_fun$'|)) |tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'gr$c'| (($x1 |tptp.'ZF_set$'|) ($x2 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uvm$'| (($x1 |tptp.'A_a_fun$'|) ($x2 |tptp.'A_set$'|) ($x3 |tptp.'A_bool_fun$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uvf$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'vaq$'| (($x1 |tptp.'Nat_ZF_ZF_set_fun_fun$'|)) |tptp.'ZF_nat_fun_ZF_set_fun$'| (as |@_tptp.'ZF_nat_fun_ZF_set_fun$'__0| |tptp.'ZF_nat_fun_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uwn$'| (($x1 |tptp.'B_ZF_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'identityFunctor$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'| (as |@_tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'A_a_b_b_b_c_LSCategory_ext_b_c_LSCategory_ext_unit_Functor_ext$'|)) % 141.61/141.98 (define-fun |tptp.'image$i'| (($x1 |tptp.'ZF_a_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.61/141.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$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'top$a'| () |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ar'| (($x1 |tptp.'B_ZF_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 141.61/141.98 (define-fun |tptp.'restrict$b'| (($x1 |tptp.'B_a_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_a_fun$'| (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$d'| (($x1 |tptp.'ZF_ZF_ZF_prod_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_prod$'| (as |@_tptp.'ZF_ZF_prod$'__0| |tptp.'ZF_ZF_prod$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cp'| (($x1 |tptp.'Nat_a_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 141.61/141.98 (define-fun |tptp.'uyw$'| (($x1 |tptp.'ZF_ZF_ZF_set_fun_fun$'|)) |tptp.'ZF_ZF_ZF_set_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_set_fun_fun$'__0| |tptp.'ZF_ZF_ZF_set_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$c'| (($x1 |tptp.'ZF_set_set_bool_fun$'|) ($x2 |tptp.'ZF_set_set_set$'|)) |tptp.'Bool_set$'| (as |@_tptp.'Bool_set$'__0| |tptp.'Bool_set$'|)) % 141.61/141.98 (define-fun |tptp.'inverse_rel$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$x'| (($x1 |tptp.'Nat_a_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$'| ((BOUND_VARIABLE_69877 |tptp.'A_set$'|) (BOUND_VARIABLE_69879 |tptp.'A_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'less_eq$j'| (($x1 |tptp.'A_bool_fun$'|) ($x2 |tptp.'A_bool_fun$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'case_prod$d'| (($x1 |tptp.'ZF_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'|)) |tptp.'ZF_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'| (as |@_tptp.'ZF_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'__0| |tptp.'ZF_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'case_prod$g'| (($x1 |tptp.'ZF_ZF_prod_nat_ZF_ZF_set_prod_fun_fun$'|)) |tptp.'ZF_ZF_prod_nat_prod_ZF_ZF_set_prod_fun$'| (as |@_tptp.'ZF_ZF_prod_nat_prod_ZF_ZF_set_prod_fun$'__0| |tptp.'ZF_ZF_prod_nat_prod_ZF_ZF_set_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$a'| ((BOUND_VARIABLE_69895 |tptp.'B_set$'|) (BOUND_VARIABLE_69897 |tptp.'B_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'uvy$'| (($x1 |tptp.'A_ZF_fun$'|) ($x2 |tptp.'A_set$'|) ($x3 |tptp.'ZF_bool_fun$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ab'| (($x1 |tptp.'ZF_nat_ZF_set_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'vai$'| (($x1 |tptp.'ZF_ZF_ZF_set_fun_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'van$'| (($x1 |tptp.'ZF_nat_ZF_set_fun_fun$'|)) |tptp.'Nat_ZF_fun_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_fun_ZF_set_fun$'__0| |tptp.'Nat_ZF_fun_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cl'| ((BOUND_VARIABLE_69915 |tptp.'A_b_fun_bool_fun$'|) (BOUND_VARIABLE_69917 |tptp.'A_b_fun$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'uvq$'| (($x1 |tptp.'A_b_fun$'|) ($x2 |tptp.'A_set$'|) ($x3 |tptp.'B_bool_fun$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uxu$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'ZF_ZF_prod_nat_ZF_ZF_set_prod_fun_fun$'| (as |@_tptp.'ZF_ZF_prod_nat_ZF_ZF_set_prod_fun_fun$'__0| |tptp.'ZF_ZF_prod_nat_ZF_ZF_set_prod_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sup$a'| (($x1 |tptp.'Bool_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'member$'| (($x1 |tptp.'ZF$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uyn$'| () |tptp.'ZF_set_ZF_set_fun$'| (as |@_tptp.'ZF_set_ZF_set_fun$'__0| |tptp.'ZF_set_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'vat$'| (($x1 |tptp.'Nat_nat_ZF_set_fun_fun$'|)) |tptp.'Nat_nat_fun_ZF_set_fun$'| (as |@_tptp.'Nat_nat_fun_ZF_set_fun$'__0| |tptp.'Nat_nat_fun_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cu'| (($x1 |tptp.'B_b_set_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 141.61/141.98 (define-fun |tptp.'uwe$'| (($x1 |tptp.'ZF_set_a_fun$'|) ($x2 |tptp.'ZF_set_set$'|) ($x3 |tptp.'A_bool_fun$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uum$'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'uyx$'| (($x1 |tptp.'ZF_ZF_ZF_set_fun_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$b'| (($x1 |tptp.'ZF_set_bool_fun$'|) ($x2 |tptp.'ZF_set_set$'|)) |tptp.'Bool_set$'| (as |@_tptp.'Bool_set$'__0| |tptp.'Bool_set$'|)) % 141.61/141.98 (define-fun |tptp.'uwo$'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$l'| (($x1 |tptp.'ZF_bool_fun$'|) ($x2 |tptp.'ZF_bool_fun$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'uya$'| (($x1 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'Nat_ZF_ZF_prod_set_fun$'| (as |@_tptp.'Nat_ZF_ZF_prod_set_fun$'__0| |tptp.'Nat_ZF_ZF_prod_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'collect$f'| ((_arg_1 |tptp.'A_b_fun_bool_fun$'|)) |tptp.'A_b_fun_set$'| (as |@_tptp.'A_b_fun_set$'__0| |tptp.'A_b_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$k'| ((BOUND_VARIABLE_69933 |tptp.'B_bool_fun$'|) (BOUND_VARIABLE_69935 |tptp.'B$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'relInvImage$a'| (($x1 |tptp.'Nat_set$'|) ($x2 |tptp.'ZF_set_ZF_set_prod_set$'|) ($x3 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_nat_prod_set$'| (as |@_tptp.'Nat_nat_prod_set$'__0| |tptp.'Nat_nat_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uxs$'| (($x1 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_prod_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_set_fun$'__0| |tptp.'ZF_ZF_prod_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'hOMCollection$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'A$'|)) |tptp.'A_ZF_set_fun$'| (as |@_tptp.'A_ZF_set_fun$'__0| |tptp.'A_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$y'| (($x1 |tptp.'Nat_b_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 141.61/141.98 (define-fun |tptp.'case_prod$h'| (($x1 |tptp.'Nat_ZF_ZF_set_ZF_set_prod_fun_fun$'|)) |tptp.'Nat_ZF_prod_ZF_set_ZF_set_prod_fun$'| (as |@_tptp.'Nat_ZF_prod_ZF_set_ZF_set_prod_fun$'__0| |tptp.'Nat_ZF_prod_ZF_set_ZF_set_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$ab'| (($x1 |tptp.'ZF_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'|) ($x2 |tptp.'ZF_ZF_ZF_prod_prod_set$'|)) |tptp.'ZF_set_ZF_prod_set$'| (as |@_tptp.'ZF_set_ZF_prod_set$'__0| |tptp.'ZF_set_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$s'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'vaa$'| (($x1 |tptp.'ZF_nat_bool_fun_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uyi$'| (($x1 |tptp.'ZF_set_set$'|)) |tptp.'ZF_ZF_set_set_fun$'| (as |@_tptp.'ZF_ZF_set_set_fun$'__0| |tptp.'ZF_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cq'| (($x1 |tptp.'Nat_b_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 141.61/141.98 (define-fun |tptp.'member$i'| (($x1 |tptp.'A_b_fun$'|) ($x2 |tptp.'A_b_fun_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'fun_app$ae'| (($x1 |tptp.'ZF_set_ZF_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'swap$'| () |tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'inverse$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'mapO$'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$y'| (($x1 |tptp.'Nat_ZF_fun_ZF_set_fun$'|) ($x2 |tptp.'Nat_ZF_fun$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$h'| (($x1 |tptp.'Nat_ZF_set_prod_set$'|) ($x2 |tptp.'Nat_ZF_set_prod_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'image$ap'| (($x1 |tptp.'ZF_b_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'B_set_set$'| (as |@_tptp.'B_set_set$'__0| |tptp.'B_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$al'| ((BOUND_VARIABLE_69950 |tptp.'B_b_prod_bool_fun$'|) (BOUND_VARIABLE_69952 |tptp.'B_b_prod$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'uxe$'| () |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'member$d'| (($x1 |tptp.'ZF_ZF_prod$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'fun_app$bu'| (($x1 |tptp.'Nat_ZF_ZF_set_prod_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF_ZF_set_prod$'| (as |@_tptp.'ZF_ZF_set_prod$'__0| |tptp.'ZF_ZF_set_prod$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bg'| (($x1 |tptp.'B_set_b_set_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bo'| (($x1 |tptp.'Nat_ZF_ZF_ZF_prod_set_fun_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF_ZF_ZF_prod_set_fun$'| (as |@_tptp.'ZF_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_ZF_ZF_prod_set_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'uyo$'| (($x1 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_set_ZF_ZF_prod_set_fun$'| (as |@_tptp.'ZF_set_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_set_ZF_ZF_prod_set_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'uzt$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_nat_ZF_ZF_prod_set_fun_fun$'| (as |@_tptp.'Nat_nat_ZF_ZF_prod_set_fun_fun$'__0| |tptp.'Nat_nat_ZF_ZF_prod_set_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uuq$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uxf$'| () |tptp.'Nat_nat_set_fun$'| (as |@_tptp.'Nat_nat_set_fun$'__0| |tptp.'Nat_nat_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bt'| (($x1 |tptp.'ZF_ZF_prod_ZF_ZF_ZF_set_prod_fun_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) |tptp.'ZF_ZF_ZF_set_prod_fun$'| (as |@_tptp.'ZF_ZF_ZF_set_prod_fun$'__0| |tptp.'ZF_ZF_ZF_set_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'extensional$'| (($x1 |tptp.'B_set$'|)) |tptp.'B_a_fun_set$'| (as |@_tptp.'B_a_fun_set$'__0| |tptp.'B_a_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$aj'| (($x1 |tptp.'ZF_ZF_prod_ZF_set_ZF_set_prod_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_set_ZF_set_prod_set$'| (as |@_tptp.'ZF_set_ZF_set_prod_set$'__0| |tptp.'ZF_set_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$d'| (($x1 |tptp.'ZF_set_ZF_set_prod_set$'|) ($x2 |tptp.'ZF_set_ZF_set_prod_set$'|)) Bool false) % 141.61/141.98 (define-fun |tptp.'image$d'| (($x1 |tptp.'B_set_bool_fun$'|) ($x2 |tptp.'B_set_set$'|)) |tptp.'Bool_set$'| (as |@_tptp.'Bool_set$'__0| |tptp.'Bool_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cw'| (($x1 |tptp.'ZF_b_set_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 141.61/141.98 (define-fun |tptp.'uuo$'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'opair$'| () |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uuy$'| (($x1 |tptp.'B_set$'|) ($x2 |tptp.'B_bool_fun$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uyy$'| (($x1 |tptp.'ZF_nat_ZF_set_fun_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'collect$'| (($x1 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ao'| (($x1 |tptp.'ZF_nat_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'Nat$'| (as |@_tptp.'Nat$'__0| |tptp.'Nat$'|)) % 141.61/141.98 (define-fun |tptp.'g$'| () |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 141.61/141.98 (define-fun |tptp.'vae$'| (($x1 |tptp.'B_set_set$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'member$b'| (($x1 |tptp.'B$'|)) |tptp.'B_set_bool_fun$'| (as |@_tptp.'B_set_bool_fun$'__0| |tptp.'B_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ac'| (($x1 |tptp.'Nat_ZF_ZF_set_fun_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'more_update$'| (($x1 |tptp.'Unit_unit_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$'|)) % 141.61/141.98 (define-fun |tptp.'image$aa'| (($x1 |tptp.'Nat_ZF_ZF_prod_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uzy$'| (($x1 |tptp.'ZF_nat_bool_fun_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uxw$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_ZF_set_set_fun$'| (as |@_tptp.'ZF_ZF_set_set_fun$'__0| |tptp.'ZF_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'comp$b'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'top$f'| () |tptp.'ZF_ZF_fun_set$'| (as |@_tptp.'ZF_ZF_fun_set$'__0| |tptp.'ZF_ZF_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'more$'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'uwh$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod_bool_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uyr$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'restrict$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_ZF_prod_ZF_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_fun$'__0| |tptp.'ZF_ZF_prod_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$bi'| (($x1 |tptp.'B_set_b_bool_fun_fun$'|) ($x2 |tptp.'B_set_set$'|)) |tptp.'B_bool_fun_set$'| (as |@_tptp.'B_bool_fun_set$'__0| |tptp.'B_bool_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'more$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)) % 141.61/141.98 (define-fun |tptp.'uvs$'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B_set$'|) ($x3 |tptp.'B_bool_fun$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'comp$i'| (($x1 |tptp.'ZF_set_set_ZF_set_fun$'|) ($x2 |tptp.'ZF_set_set_ZF_set_set_fun$'|)) |tptp.'ZF_set_set_ZF_set_fun$'| (as |@_tptp.'ZF_set_set_ZF_set_fun$'__0| |tptp.'ZF_set_set_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$bn'| (($x1 |tptp.'ZF_ZF_fun_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_fun_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cb'| (($x1 |tptp.'ZF_nat_ZF_set_ZF_set_prod_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'Nat_ZF_set_ZF_set_prod_fun$'| (as |@_tptp.'Nat_ZF_set_ZF_set_prod_fun$'__0| |tptp.'Nat_ZF_set_ZF_set_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bs'| (($x1 |tptp.'ZF_ZF_ZF_set_prod_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_set_prod$'| (as |@_tptp.'ZF_ZF_set_prod$'__0| |tptp.'ZF_ZF_set_prod$'|)) % 141.61/141.98 (define-fun |tptp.'vaj$'| (($x1 |tptp.'ZF_ZF_ZF_set_fun_fun$'|) ($x2 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'restrict$c'| (($x1 |tptp.'A_b_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'A_b_fun$'| (as |@_tptp.'A_b_fun$'__0| |tptp.'A_b_fun$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$g'| (($x1 |tptp.'ZF_ZF_prod_ZF_prod_set$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_prod_set$'|)) Bool true) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'elem$'| () |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'zFfunDom$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uzk$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_ZF_set_set_fun$'| (as |@_tptp.'Nat_ZF_set_set_fun$'__0| |tptp.'Nat_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'vak$'| (($x1 |tptp.'ZF_ZF_ZF_set_fun_fun$'|)) |tptp.'ZF_ZF_fun_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_fun_ZF_set_fun$'__0| |tptp.'ZF_ZF_fun_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$o'| (($x1 |tptp.'A_b_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 141.61/141.98 (define-fun |tptp.'uyk$'| () |tptp.'ZF_ZF_ZF_set_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_set_fun_fun$'__0| |tptp.'ZF_ZF_ZF_set_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bb'| (($x1 |tptp.'ZF_ZF_prod_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'uzr$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'Nat_ZF_ZF_ZF_prod_set_fun_fun$'| (as |@_tptp.'Nat_ZF_ZF_ZF_prod_set_fun_fun$'__0| |tptp.'Nat_ZF_ZF_ZF_prod_set_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'case_prod$p'| (($x1 |tptp.'ZF_ZF_ZF_ZF_prod_set_fun_fun$'|)) |tptp.'ZF_ZF_prod_ZF_ZF_prod_set_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_set_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uws$'| () |tptp.'Nat_bool_fun$'| (as |@_tptp.'Nat_bool_fun$'__0| |tptp.'Nat_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uwg$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'category_axioms$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'case_prod$b'| (($x1 |tptp.'ZF_ZF_bool_fun_fun$'|)) |tptp.'ZF_ZF_prod_bool_fun$'| (as |@_tptp.'ZF_ZF_prod_bool_fun$'__0| |tptp.'ZF_ZF_prod_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'lambda$'| ((BOUND_VARIABLE_69963 |tptp.'ZF$'|) (BOUND_VARIABLE_69965 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 141.61/141.98 (define-fun |tptp.'uzo$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'ZF_nat_ZF_ZF_prod_set_fun_fun$'| (as |@_tptp.'ZF_nat_ZF_ZF_prod_set_fun_fun$'__0| |tptp.'ZF_nat_ZF_ZF_prod_set_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uu$'| () |tptp.'A_set_a_bool_fun_fun$'| (as |@_tptp.'A_set_a_bool_fun_fun$'__0| |tptp.'A_set_a_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'cod$a'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uvn$'| (($x1 |tptp.'B_a_fun$'|) ($x2 |tptp.'B_set$'|) ($x3 |tptp.'A_bool_fun$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uwy$'| () |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'more$b'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'C$'| (as |@_tptp.'C$'__0| |tptp.'C$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$v'| (($x1 |tptp.'Nat_set_ZF_set_set_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'vad$'| (($x1 |tptp.'A_set_set$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cf'| (($x1 |tptp.'ZF_ZF_prod_ZF_ZF_prod_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'uuv$'| () |tptp.'ZF_ZF_ZF_fun_fun_ZF_ZF_ZF_fun_fun_fun$'| (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$'|)) % 141.61/141.98 (define-fun |tptp.'image$ar'| (($x1 |tptp.'B_ZF_set_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'preFunctor$a'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true) % 141.61/141.98 (define-fun tptp.tlfalse () tptp.tlbool (as @tptp.tlbool_0 tptp.tlbool)) % 141.61/141.98 (define-fun |tptp.'zF2mor$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'ZF_b_fun$'| (as |@_tptp.'ZF_b_fun$'__0| |tptp.'ZF_b_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uus$'| (($x1 |tptp.'ZF$'|)) |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$t'| (($x1 |tptp.'ZF_ZF_prod_ZF_ZF_prod_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uxz$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_fun$'|)) |tptp.'Nat_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'| (as |@_tptp.'Nat_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'__0| |tptp.'Nat_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'dom_update$a'| (($x1 |tptp.'ZF_ZF_fun_ZF_ZF_fun_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$'|)) % 141.61/141.98 (define-fun |tptp.'uwm$'| (($x1 |tptp.'A_ZF_fun$'|) ($x2 |tptp.'A_set$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ce'| (($x1 |tptp.'Nat_nat_ZF_set_ZF_set_prod_fun_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'Nat_ZF_set_ZF_set_prod_fun$'| (as |@_tptp.'Nat_ZF_set_ZF_set_prod_fun$'__0| |tptp.'Nat_ZF_set_ZF_set_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cm'| (($x1 |tptp.'Unit_unit_fun$'|) ($x2 |tptp.'Unit$'|)) |tptp.'Unit$'| (as |@_tptp.'Unit$'__0| |tptp.'Unit$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$at'| (($x1 |tptp.'Nat_ZF_bool_fun_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'uue$'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'uzj$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_ZF_set_set_fun$'| (as |@_tptp.'ZF_ZF_set_set_fun$'__0| |tptp.'ZF_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uzq$'| (($x1 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_ZF_ZF_set_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_set_fun_fun$'__0| |tptp.'ZF_ZF_ZF_set_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'collect$g'| (($x1 |tptp.'Nat_bool_fun$'|)) |tptp.'Nat_set$'| (as |@_tptp.'Nat_set$'__0| |tptp.'Nat_set$'|)) % 141.61/141.98 (define-fun |tptp.'constFunctor$c'| (($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$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$by'| (($x1 |tptp.'ZF_ZF_set_ZF_set_prod_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_set_ZF_set_prod$'| (as |@_tptp.'ZF_set_ZF_set_prod$'__0| |tptp.'ZF_set_ZF_set_prod$'|)) % 141.61/141.98 (define-fun |tptp.'functor$'| (($x1 |tptp.'ZF_ZF_ZF_ZF_unit_unit_unit_Functor_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'fun_app$am'| (($x1 |tptp.'B_b_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 141.61/141.98 (define-fun |tptp.'collect$h'| (($x1 |tptp.'A_bool_fun$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.61/141.98 (define-fun |tptp.'uzh$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_ZF_prod_set_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$b'| ((BOUND_VARIABLE_69981 |tptp.'ZF_set_set$'|) (BOUND_VARIABLE_69983 |tptp.'ZF_set_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'fun_app$n'| ((BOUND_VARIABLE_69999 |tptp.'A_bool_fun$'|) (BOUND_VARIABLE_70001 |tptp.'A$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'fun_app$au'| (($x1 |tptp.'ZF_ZF_prod_set_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'uyu$'| (($x1 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_set_ZF_set_fun$'| (as |@_tptp.'ZF_set_ZF_set_fun$'__0| |tptp.'ZF_set_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'relImage$b'| (($x1 |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_set$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_fun$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uxx$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'Nat_ZF_ZF_set_ZF_set_prod_fun_fun$'| (as |@_tptp.'Nat_ZF_ZF_set_ZF_set_prod_fun_fun$'__0| |tptp.'Nat_ZF_ZF_set_ZF_set_prod_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bq'| (($x1 |tptp.'Nat_nat_ZF_ZF_prod_set_fun_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'Nat_ZF_ZF_prod_set_fun$'| (as |@_tptp.'Nat_ZF_ZF_prod_set_fun$'__0| |tptp.'Nat_ZF_ZF_prod_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'product$'| ((BOUND_VARIABLE_70016 |tptp.'ZF_set$'|) (BOUND_VARIABLE_70018 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uyd$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_fun$'|)) |tptp.'ZF_ZF_prod_ZF_ZF_prod_ZF_ZF_prod_fun_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_ZF_ZF_prod_fun_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_ZF_ZF_prod_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uvj$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'ZF_nat_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uwq$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_ZF_prod_fun$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'pair$d'| (($x1 |tptp.'ZF_set$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_set_ZF_set_prod$'| (as |@_tptp.'ZF_set_ZF_set_prod$'__0| |tptp.'ZF_set_ZF_set_prod$'|)) % 141.61/141.98 (define-fun |tptp.'image$j'| (($x1 |tptp.'ZF_set_a_fun$'|) ($x2 |tptp.'ZF_set_set$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF$'| (as |@_tptp.'ZF$'__0| |tptp.'ZF$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$l'| (($x1 |tptp.'B_set_b_bool_fun_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'functor$c'| (($x1 |tptp.'ZF_unit_ZF_unit_unit_unit_unit_Functor_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'objIso$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ax'| (($x1 |tptp.'ZF_ZF_set_set_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'uuc$'| () |tptp.'ZF_set_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_set_ZF_bool_fun_fun$'__0| |tptp.'ZF_set_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cs'| (($x1 |tptp.'A_b_set_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B_set$'| (as |@_tptp.'B_set$'__0| |tptp.'B_set$'|)) % 141.61/141.98 (define-fun |tptp.'uzz$'| (($x1 |tptp.'ZF_nat_bool_fun_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$aw'| (($x1 |tptp.'Nat_ZF_ZF_prod_set_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'collect$e'| ((_arg_1 |tptp.'B_a_fun_bool_fun$'|)) |tptp.'B_a_fun_set$'| (as |@_tptp.'B_a_fun_set$'__0| |tptp.'B_a_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$g'| (($x1 |tptp.'ZF_set_ZF_bool_fun_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'restrict$d'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$af'| (($x1 |tptp.'Nat_ZF_prod_ZF_set_ZF_set_prod_fun$'|) ($x2 |tptp.'Nat_ZF_prod_set$'|)) |tptp.'ZF_set_ZF_set_prod_set$'| (as |@_tptp.'ZF_set_ZF_set_prod_set$'__0| |tptp.'ZF_set_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uvl$'| (($x1 |tptp.'A_a_fun$'|) ($x2 |tptp.'A_set$'|) ($x3 |tptp.'A_bool_fun$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'isomorphism$a'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|)) |tptp.'B_bool_fun$'| (as |@_tptp.'B_bool_fun$'__0| |tptp.'B_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$bd'| (($x1 |tptp.'ZF_nat_prod_ZF_ZF_prod_set_fun$'|) ($x2 |tptp.'ZF_nat_prod_set$'|)) |tptp.'ZF_ZF_prod_set_set$'| (as |@_tptp.'ZF_ZF_prod_set_set$'__0| |tptp.'ZF_ZF_prod_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$q'| (($x1 |tptp.'ZF_set_ZF_set_fun$'|)) |tptp.'ZF_set_set_ZF_set_set_fun$'| (as |@_tptp.'ZF_set_set_ZF_set_set_fun$'__0| |tptp.'ZF_set_set_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$an'| (($x1 |tptp.'B_b_b_fun_fun$'|) ($x2 |tptp.'B$'|)) |tptp.'B_b_fun$'| (as |@_tptp.'B_b_fun$'__0| |tptp.'B_b_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uwz$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_set_ZF_set_set_fun$'| (as |@_tptp.'ZF_set_ZF_set_set_fun$'__0| |tptp.'ZF_set_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uuu$'| () |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$av'| (($x1 |tptp.'ZF_ZF_prod_set_ZF_set_fun$'|)) |tptp.'ZF_ZF_prod_set_set_ZF_set_set_fun$'| (as |@_tptp.'ZF_ZF_prod_set_set_ZF_set_set_fun$'__0| |tptp.'ZF_ZF_prod_set_set_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$aw'| (($x1 |tptp.'ZF_nat_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'Nat_set_set$'| (as |@_tptp.'Nat_set_set$'__0| |tptp.'Nat_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$bp'| (($x1 |tptp.'ZF_nat_fun_ZF_set_fun$'|) ($x2 |tptp.'ZF_nat_fun_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ap'| (($x1 |tptp.'Nat_nat_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'Nat$'| (as |@_tptp.'Nat$'__0| |tptp.'Nat$'|)) % 141.61/141.98 (define-fun |tptp.'member$e'| (($x1 |tptp.'Nat$'|) ($x2 |tptp.'Nat_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'image$am'| (($x1 |tptp.'B_a_set_fun$'|) ($x2 |tptp.'B_set$'|)) |tptp.'A_set_set$'| (as |@_tptp.'A_set_set$'__0| |tptp.'A_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'top$c'| () |tptp.'ZF_nat_prod_set$'| (as |@_tptp.'ZF_nat_prod_set$'__0| |tptp.'ZF_nat_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'vab$'| (($x1 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sup$b'| ((BOUND_VARIABLE_70029 |tptp.'A_set_set$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$z'| (($x1 |tptp.'ZF_ZF_fun_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_fun$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'isomorphism$'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$ae'| (($x1 |tptp.'ZF_ZF_prod_nat_prod_ZF_ZF_set_prod_fun$'|) ($x2 |tptp.'ZF_ZF_prod_nat_prod_set$'|)) |tptp.'ZF_ZF_set_prod_set$'| (as |@_tptp.'ZF_ZF_set_prod_set$'__0| |tptp.'ZF_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uzi$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|) ($x2 |tptp.'Nat_ZF_ZF_prod_set_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$j'| (($x1 |tptp.'ZF_set_set_bool_fun$'|) ($x2 |tptp.'ZF_set_set$'|)) Bool true) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'case_prod$k'| (($x1 |tptp.'ZF_ZF_prod_ZF_ZF_prod_ZF_ZF_prod_fun_fun$'|)) |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_ZF_ZF_prod_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_ZF_ZF_prod_fun$'__0| |tptp.'ZF_ZF_prod_ZF_ZF_prod_prod_ZF_ZF_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sigma$j'| (($x1 |tptp.'Nat_set$'|) ($x2 |tptp.'Nat_ZF_ZF_prod_set_fun$'|)) |tptp.'Nat_ZF_ZF_prod_prod_set$'| (as |@_tptp.'Nat_ZF_ZF_prod_prod_set$'__0| |tptp.'Nat_ZF_ZF_prod_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uzc$'| (($x1 |tptp.'Nat_ZF_ZF_set_fun_fun$'|)) |tptp.'ZF_nat_ZF_set_fun_fun$'| (as |@_tptp.'ZF_nat_ZF_set_fun_fun$'__0| |tptp.'ZF_nat_ZF_set_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'comp$c'| (($x1 |tptp.'ZF_set_set_set_ZF_set_set_fun$'|) ($x2 |tptp.'Nat_set_set_ZF_set_set_set_fun$'|)) |tptp.'Nat_set_set_ZF_set_set_fun$'| (as |@_tptp.'Nat_set_set_ZF_set_set_fun$'__0| |tptp.'Nat_set_set_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uvd$'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_prod_ZF_fun$'|)) |tptp.'ZF_ZF_prod_ZF_fun$'| (as |@_tptp.'ZF_ZF_prod_ZF_fun$'__0| |tptp.'ZF_ZF_prod_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uvt$'| (($x1 |tptp.'ZF_a_fun$'|) ($x2 |tptp.'ZF_set$'|) ($x3 |tptp.'A_bool_fun$'|)) |tptp.'A_bool_fun$'| (as |@_tptp.'A_bool_fun$'__0| |tptp.'A_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'top$h'| () |tptp.'ZF_nat_fun_set$'| (as |@_tptp.'ZF_nat_fun_set$'__0| |tptp.'ZF_nat_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$dc'| (($x1 |tptp.'ZF_ZF_prod_set_set_ZF_set_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'constFunctor$b'| (($x1 |tptp.'ZF_ZF_unit_Category_ext$'|) ($x2 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x3 |tptp.'A$'|)) |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'| (as |@_tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'__0| |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cz'| (($x1 |tptp.'Nat_set_set_nat_set_fun$'|) ($x2 |tptp.'Nat_set_set$'|)) |tptp.'Nat_set$'| (as |@_tptp.'Nat_set$'__0| |tptp.'Nat_set$'|)) % 141.61/141.98 (define-fun |tptp.'uwi$'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uyf$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_ZF_ZF_set_ZF_set_prod_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_set_ZF_set_prod_fun_fun$'__0| |tptp.'ZF_ZF_ZF_set_ZF_set_prod_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$k'| ((BOUND_VARIABLE_70043 |tptp.'B_ZF_fun$'|) (BOUND_VARIABLE_70045 |tptp.'B_set$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'case_prod$j'| (($x1 |tptp.'Nat_nat_ZF_set_ZF_set_prod_fun_fun$'|)) |tptp.'Nat_nat_prod_ZF_set_ZF_set_prod_fun$'| (as |@_tptp.'Nat_nat_prod_ZF_set_ZF_set_prod_fun$'__0| |tptp.'Nat_nat_prod_ZF_set_ZF_set_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ba'| (($x1 |tptp.'Nat_ZF_ZF_prod_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF_ZF_prod$'| (as |@_tptp.'ZF_ZF_prod$'__0| |tptp.'ZF_ZF_prod$'|)) % 141.61/141.98 (define-fun |tptp.'relImage$'| (($x1 |tptp.'ZF_ZF_prod_set$'|) ($x2 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_set_ZF_set_prod_set$'| (as |@_tptp.'ZF_set_ZF_set_prod_set$'__0| |tptp.'ZF_set_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$be'| (($x1 |tptp.'Nat_ZF_prod_ZF_ZF_prod_set_fun$'|) ($x2 |tptp.'Nat_ZF_prod_set$'|)) |tptp.'ZF_ZF_prod_set_set$'| (as |@_tptp.'ZF_ZF_prod_set_set$'__0| |tptp.'ZF_ZF_prod_set_set$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'sigma$l'| (($x1 |tptp.'Nat_set$'|) ($x2 |tptp.'Nat_ZF_set_set_fun$'|)) |tptp.'Nat_ZF_set_prod_set$'| (as |@_tptp.'Nat_ZF_set_prod_set$'__0| |tptp.'Nat_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bj'| (($x1 |tptp.'ZF_set_a_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'A$'| (as |@_tptp.'A$'__0| |tptp.'A$'|)) % 141.61/141.98 (define-fun |tptp.'uzx$'| (($x1 |tptp.'ZF_ZF_bool_fun_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'relInvImage$'| (($x1 |tptp.'ZF_set$'|) ($x2 |tptp.'ZF_set_ZF_set_prod_set$'|) ($x3 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$m'| (($x1 |tptp.'B_set_bool_fun$'|) ($x2 |tptp.'B_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'case_prod$i'| (($x1 |tptp.'Nat_ZF_ZF_prod_ZF_set_ZF_prod_fun_fun$'|)) |tptp.'Nat_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'| (as |@_tptp.'Nat_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'__0| |tptp.'Nat_ZF_ZF_prod_prod_ZF_set_ZF_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'preFunctor$'| (($x1 |tptp.'ZF_a_ZF_b_unit_b_c_LSCategory_ext_unit_Functor_ext$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'vav$'| (($x1 |tptp.'ZF_ZF_ZF_set_fun_fun$'|)) |tptp.'ZF_ZF_fun_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_fun_ZF_set_fun$'__0| |tptp.'ZF_ZF_fun_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ch'| (($x1 |tptp.'B_a_fun_b_a_fun_fun$'|) ($x2 |tptp.'B_a_fun$'|)) |tptp.'B_a_fun$'| (as |@_tptp.'B_a_fun$'__0| |tptp.'B_a_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$bl'| (($x1 |tptp.'ZF_ZF_bool_fun_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_bool_fun_set$'| (as |@_tptp.'ZF_bool_fun_set$'__0| |tptp.'ZF_bool_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'case_prod$o'| (($x1 |tptp.'Nat_nat_ZF_ZF_prod_set_fun_fun$'|)) |tptp.'Nat_nat_prod_ZF_ZF_prod_set_fun$'| (as |@_tptp.'Nat_nat_prod_ZF_ZF_prod_set_fun$'__0| |tptp.'Nat_nat_prod_ZF_ZF_prod_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$da'| (($x1 |tptp.'ZF_set_set_set_ZF_set_set_fun$'|) ($x2 |tptp.'ZF_set_set_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'member$h'| (($x1 |tptp.'B_a_fun$'|) ($x2 |tptp.'B_a_fun_set$'|)) Bool false) % 141.61/141.98 (define-fun |tptp.'uul$'| (($x1 |tptp.'ZF_ZF_prod_ZF_fun$'|)) |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'sigma$d'| (($x1 |tptp.'Nat_set$'|) ($x2 |tptp.'Nat_nat_set_fun$'|)) |tptp.'Nat_nat_prod_set$'| (as |@_tptp.'Nat_nat_prod_set$'__0| |tptp.'Nat_nat_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$s'| (($x1 |tptp.'ZF_ZF_prod_ZF_set_fun$'|) ($x2 |tptp.'ZF_ZF_prod_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$v'| (($x1 |tptp.'Nat_nat_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'Nat_set$'| (as |@_tptp.'Nat_set$'__0| |tptp.'Nat_set$'|)) % 141.61/141.98 (define-fun |tptp.'uvx$'| (($x1 |tptp.'A_ZF_fun$'|) ($x2 |tptp.'A_set$'|) ($x3 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cj'| ((BOUND_VARIABLE_70060 |tptp.'B_ZF_fun_bool_fun$'|) (BOUND_VARIABLE_70062 |tptp.'B_ZF_fun$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'image$bm'| (($x1 |tptp.'Nat_ZF_bool_fun_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_bool_fun_set$'| (as |@_tptp.'ZF_bool_fun_set$'__0| |tptp.'ZF_bool_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$cv'| (($x1 |tptp.'ZF_a_set_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'A_set$'| (as |@_tptp.'A_set$'__0| |tptp.'A_set$'|)) % 141.61/141.98 (define-fun |tptp.'uzl$'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_ZF_set_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'pair$b'| (($x1 |tptp.'ZF$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_set_prod$'| (as |@_tptp.'ZF_ZF_set_prod$'__0| |tptp.'ZF_ZF_set_prod$'|)) % 141.61/141.98 (define-fun |tptp.'mor_update$'| (($x1 |tptp.'ZF_set_ZF_set_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$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$p'| (($x1 |tptp.'A_set_bool_fun$'|) ($x2 |tptp.'A_set$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'image$bo'| (($x1 |tptp.'Nat_ZF_fun_ZF_set_fun$'|) ($x2 |tptp.'Nat_ZF_fun_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$ay'| (($x1 |tptp.'Nat_set_ZF_set_fun$'|) ($x2 |tptp.'Nat_set_set$'|)) |tptp.'ZF_set_set$'| (as |@_tptp.'ZF_set_set$'__0| |tptp.'ZF_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'top$'| () |tptp.'Nat_set$'| (as |@_tptp.'Nat_set$'__0| |tptp.'Nat_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$bf'| (($x1 |tptp.'Nat_nat_prod_ZF_ZF_prod_set_fun$'|) ($x2 |tptp.'Nat_nat_prod_set$'|)) |tptp.'ZF_ZF_prod_set_set$'| (as |@_tptp.'ZF_ZF_prod_set_set$'__0| |tptp.'ZF_ZF_prod_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'sigma$i'| (($x1 |tptp.'ZF_ZF_prod_set$'|) ($x2 |tptp.'ZF_ZF_prod_nat_set_fun$'|)) |tptp.'ZF_ZF_prod_nat_prod_set$'| (as |@_tptp.'ZF_ZF_prod_nat_prod_set$'__0| |tptp.'ZF_ZF_prod_nat_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$l'| (($x1 |tptp.'B_b_fun$'|)) |tptp.'B_set_b_set_fun$'| (as |@_tptp.'B_set_b_set_fun$'__0| |tptp.'B_set_b_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uxt$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_set_set_fun$'| (as |@_tptp.'ZF_ZF_set_set_fun$'__0| |tptp.'ZF_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uxc$'| () |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$at'| (($x1 |tptp.'Nat_set_ZF_set_set_fun$'|)) |tptp.'Nat_set_set_ZF_set_set_set_fun$'| (as |@_tptp.'Nat_set_set_ZF_set_set_set_fun$'__0| |tptp.'Nat_set_set_ZF_set_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'vaz$'| (($x1 |tptp.'Nat_ZF_ZF_set_fun_fun$'|)) |tptp.'ZF_nat_fun_ZF_set_fun$'| (as |@_tptp.'ZF_nat_fun_ZF_set_fun$'__0| |tptp.'ZF_nat_fun_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uvk$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'Nat_nat_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$q'| (($x1 |tptp.'ZF_ZF_bool_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uwc$'| (($x1 |tptp.'ZF_ZF_fun$'|) ($x2 |tptp.'ZF_set$'|) ($x3 |tptp.'ZF_bool_fun$'|)) |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bl'| (($x1 |tptp.'A_b_fun$'|) ($x2 |tptp.'A$'|)) |tptp.'B$'| (as |@_tptp.'B$'__0| |tptp.'B$'|)) % 141.61/141.98 (define-fun |tptp.'uys$'| (($x1 |tptp.'ZF_ZF_set_fun$'|) ($x2 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_ZF_set_fun$'| (as |@_tptp.'Nat_ZF_set_fun$'__0| |tptp.'Nat_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'gr$b'| (($x1 |tptp.'Nat_set$'|) ($x2 |tptp.'Nat_ZF_set_fun$'|)) |tptp.'Nat_ZF_set_prod_set$'| (as |@_tptp.'Nat_ZF_set_prod_set$'__0| |tptp.'Nat_ZF_set_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'less_eq$c'| (($x1 |tptp.'ZF_set$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'explode$'| () |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'isZFfun$'| () |tptp.'ZF_bool_fun$'| (as |@_tptp.'ZF_bool_fun$'__0| |tptp.'ZF_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$c'| (($x1 |tptp.'ZF_set_ZF_ZF_prod_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.98 (define-fun |tptp.'uyj$'| (($x1 |tptp.'ZF_set_set$'|)) |tptp.'Nat_ZF_set_set_fun$'| (as |@_tptp.'Nat_ZF_set_set_fun$'__0| |tptp.'Nat_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'vay$'| (($x1 |tptp.'Nat_ZF_ZF_set_fun_fun$'|)) |tptp.'ZF_ZF_set_fun$'| (as |@_tptp.'ZF_ZF_set_fun$'__0| |tptp.'ZF_ZF_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'cartProd$'| () |tptp.'ZF_ZF_ZF_fun_fun$'| (as |@_tptp.'ZF_ZF_ZF_fun_fun$'__0| |tptp.'ZF_ZF_ZF_fun_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$au'| (($x1 |tptp.'ZF_set_ZF_set_set_fun$'|)) |tptp.'ZF_set_set_ZF_set_set_set_fun$'| (as |@_tptp.'ZF_set_set_ZF_set_set_set_fun$'__0| |tptp.'ZF_set_set_ZF_set_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'pair$c'| (($x1 |tptp.'ZF_set$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_set_ZF_prod$'| (as |@_tptp.'ZF_set_ZF_prod$'__0| |tptp.'ZF_set_ZF_prod$'|)) % 141.61/141.98 (define-fun |tptp.'sup$e'| () |tptp.'ZF_set_set_set_ZF_set_set_fun$'| (as |@_tptp.'ZF_set_set_set_ZF_set_set_fun$'__0| |tptp.'ZF_set_set_set_ZF_set_set_fun$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$ci'| ((BOUND_VARIABLE_70077 |tptp.'ZF_ZF_fun_bool_fun$'|) (BOUND_VARIABLE_70079 |tptp.'ZF_ZF_fun$'|)) Bool true) % 141.61/141.98 (define-fun |tptp.'fun_app$e'| (($x1 |tptp.'ZF_ZF_ZF_ZF_prod_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_ZF_prod_fun$'| (as |@_tptp.'ZF_ZF_ZF_prod_fun$'__0| |tptp.'ZF_ZF_ZF_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'makeCat$a'| ((BOUND_VARIABLE_69861 |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$'|)) % 141.61/141.98 (define-fun |tptp.'uym$'| () |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$'|)) % 141.61/141.98 (define-fun |tptp.'image$u'| (($x1 |tptp.'ZF_nat_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'Nat_set$'| (as |@_tptp.'Nat_set$'__0| |tptp.'Nat_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$bz'| (($x1 |tptp.'ZF_ZF_ZF_set_ZF_set_prod_fun_fun$'|) ($x2 |tptp.'ZF$'|)) |tptp.'ZF_ZF_set_ZF_set_prod_fun$'| (as |@_tptp.'ZF_ZF_set_ZF_set_prod_fun$'__0| |tptp.'ZF_ZF_set_ZF_set_prod_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uuf$'| () |tptp.'ZF_ZF_bool_fun_fun$'| (as |@_tptp.'ZF_ZF_bool_fun_fun$'__0| |tptp.'ZF_ZF_bool_fun_fun$'|)) % 141.61/141.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$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$r'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'Nat$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$t'| (($x1 |tptp.'Nat_nat_fun_ZF_set_fun$'|) ($x2 |tptp.'Nat_nat_fun$'|)) |tptp.'ZF_set$'| (as |@_tptp.'ZF_set$'__0| |tptp.'ZF_set$'|)) % 141.61/141.98 (define-fun |tptp.'fun_app$i'| (($x1 |tptp.'ZF_set_set_ZF_set_bool_fun_fun$'|) ($x2 |tptp.'ZF_set_set$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uup$'| (($x1 |tptp.'A_b_b_c_LSCategory_ext_Category_ext$'|) ($x2 |tptp.'B$'|)) |tptp.'ZF_ZF_fun$'| (as |@_tptp.'ZF_ZF_fun$'__0| |tptp.'ZF_ZF_fun$'|)) % 141.61/141.98 (define-fun |tptp.'uwj$'| (($x1 |tptp.'Nat_ZF_set_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_set_bool_fun$'| (as |@_tptp.'ZF_set_bool_fun$'__0| |tptp.'ZF_set_bool_fun$'|)) % 141.61/141.98 (define-fun |tptp.'image$ba'| (($x1 |tptp.'Nat_ZF_ZF_prod_set_fun$'|) ($x2 |tptp.'Nat_set$'|)) |tptp.'ZF_ZF_prod_set_set$'| (as |@_tptp.'ZF_ZF_prod_set_set$'__0| |tptp.'ZF_ZF_prod_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$bk'| (($x1 |tptp.'ZF_set_ZF_bool_fun_fun$'|) ($x2 |tptp.'ZF_set_set$'|)) |tptp.'ZF_bool_fun_set$'| (as |@_tptp.'ZF_bool_fun_set$'__0| |tptp.'ZF_bool_fun_set$'|)) % 141.61/141.98 (define-fun |tptp.'image$ao'| (($x1 |tptp.'ZF_a_set_fun$'|) ($x2 |tptp.'ZF_set$'|)) |tptp.'A_set_set$'| (as |@_tptp.'A_set_set$'__0| |tptp.'A_set_set$'|)) % 141.61/141.98 (define-fun |tptp.'collect$a'| (($x1 |tptp.'ZF_ZF_prod_bool_fun$'|)) |tptp.'ZF_ZF_prod_set$'| (as |@_tptp.'ZF_ZF_prod_set$'__0| |tptp.'ZF_ZF_prod_set$'|)) % 141.61/141.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$'|)) % 141.61/141.98 ) % 141.61/141.98 % SZS output end Model % 141.61/141.99 % cvc5 exiting %------------------------------------------------------------------------------