[-16, t29_pasch, [d5_analoaf, t5_diraf], [d3_diraf, d5_analoaf, t11_diraf, t12_diraf, t13_diraf, t17_diraf, t26_pasch, t27_pasch, t28_pasch, t34_diraf, t35_diraf, t36_diraf, t37_diraf, t38_diraf, t5_diraf, t6_diraf, t7_diraf, t9_diraf], []]
[-15, t34_connsp_3, [t24_connsp_1, t39_pre_topc], [d10_pre_topc, d10_xboole_0, d1_xboole_0, d3_connsp_1, d3_tarski, d3_xboole_0, d5_pre_topc, d7_xboole_0, d9_pre_topc, t10_subset_1, t12_connsp_1, t19_xboole_1, t1_jordan1, t1_xboole_1, t23_xboole_1, t29_connsp_3, t3_xboole_1], [dt_k3_pre_topc]]
[-11, t15_bvfunc_9, [t1_bvfunc_9], [d15_bvfunc_1, d5_valuat_1, d6_valuat_1, d7_bvfunc_1, t19_binarith, t22_binarith, t39_margrel1, t43_margrel1, t46_margrel1, t49_margrel1, t7_binarith, t8_bvfunc_4], []]
[-11, t30_bvfunc_6, [t16_bvfunc_1, t29_bvfunc_6], [d11_bvfunc_1, d14_bvfunc_1, d5_valuat_1, d6_valuat_1, d7_bvfunc_1, t10_binarith, t18_binarith, t19_binarith, t20_binarith, t23_binarith, t40_margrel1, t45_margrel1, t9_binarith], []]
[-11, t38_bvfunc_6, [t17_bvfunc_1, t37_bvfunc_6], [d11_bvfunc_1, d14_bvfunc_1, d5_valuat_1, d6_valuat_1, d7_bvfunc_1, t10_binarith, t18_binarith, t19_binarith, t20_binarith, t23_binarith, t40_margrel1, t45_margrel1, t9_binarith], []]
[-11, t7_waybel32, [], [d1_waybel11, d39_waybel_0, d3_tarski, d4_waybel11, d4_yellow_9, d5_pre_topc, t15_yellow_0, t25_waybel_0, t26_yellow_0, t3_waybel_0, t47_yellow_9], [rc1_waybel29, rc2_waybel29]]
[-10, t17_bvfunc_5, [t8_bvfunc_5, t15_bvfunc_5, t16_bvfunc_5], [d11_bvfunc_1, d14_bvfunc_1, d2_funct_2, t10_binarith, t19_binarith, t20_binarith, t22_binarith, t23_binarith, t39_margrel1, t40_margrel1, t41_margrel1, t50_margrel1, t9_funct_1], [redefinition_m2_fraenkel, dt_k14_bvfunc_1, dt_k1_fraenkel, fc3_margrel1]]
[-10, t20_arytm_0, [d5_arytm_0], [d1_numbers, d2_xboole_0, d3_arytm_0, d4_xboole_0, t21_arytm_2, t33_zfmisc_1, t3_arytm_0, t3_xboole_0, t4_arytm_2, t5_arytm_0, t8_arytm_0], [redefinition_k13_arytm_3]]
[-10, t27_waybel32, [t41_waybel21], [d1_yellow_9, d2_yellow_0, d7_waybel_9, d9_yellow_6, t13_waybel_9, t14_waybel_9, t35_funct_1, t36_waybel21, t38_waybel21, t40_waybel21, t61_yellow_0], [cc12_waybel_0, cc1_lattice3, cc11_waybel_0, cc3_yellow14]]
[-10, t44_oposet_1, [d24_oposet_1, d25_oposet_1], [d15_oposet_1, d19_oposet_1, d24_oposet_1, d25_oposet_1, d4_orders_2, d5_orders_2, d6_orders_2, t10_oposet_1, t12_oposet_1, t28_oposet_1, t32_oposet_1, t7_oposet_1], [cc3_oposet_1, cc5_oposet_1, cc7_oposet_1, cc8_oposet_1, dt_l1_oposet_1]]
[-9, t16_bvfunc_4, [t20_bvfunc_1], [t10_bvfunc_4, t11_bvfunc_1, t13_bvfunc_1, t14_bvfunc_1, t16_bvfunc_1, t17_bvfunc_1, t4_bvfunc_1, t7_bvfunc_4, t8_bvfunc_4, t9_bvfunc_1], [redefinition_m2_fraenkel, dt_k15_bvfunc_1, dt_k1_fraenkel, fc3_margrel1]]
[-9, t65_rmod_2, [t64_rmod_2, t29_rmod_2], [d10_xboole_0, d1_rlvect_1, d2_rmod_2, d3_tarski, d6_rlvect_1, t28_rmod_2, t29_rmod_2, t31_rmod_2, t3_rlvect_1, t66_vectsp_1, t7_vectsp_1], [dt_l2_struct_0, dt_l2_vectsp_1, dt_k6_vectsp_2, dt_l3_vectsp_1]]
[-9, t65_vectsp_4, [t64_vectsp_4, t29_vectsp_4], [d10_xboole_0, d1_rlvect_1, d2_vectsp_4, d3_tarski, d6_rlvect_1, t10_rlvect_1, t28_vectsp_4, t29_vectsp_4, t31_vectsp_4, t3_rlvect_1, t66_vectsp_1], [dt_l2_struct_0, dt_k6_vectsp_1, dt_l1_rlvect_1, dt_l3_vectsp_1]]
[-9, t9_instalg1, [t29_pua2mss1, t6_msalimit], [d11_finseq_1, d13_pua2mss1, d1_funct_2, d1_instalg1, d4_finseq_1, t12_relset_1, t34_funct_1, t42_funct_1, t71_relat_1, t79_relat_1, t7_funct_2], [cc4_instalg1, redefinition_k6_partfun1]]
[-8, t10_bvfunc_3, [t9_bvfunc_3], [d10_bvfunc_2, d15_bvfunc_1, d19_bvfunc_1, d20_bvfunc_1, d7_bvfunc_1, d9_bvfunc_2, t19_binarith, t43_margrel1, t7_binarith], [commutativity_k8_bvfunc_1, redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k6_bvfunc_2, dt_k7_bvfunc_2, fc3_margrel1]]
[-8, t14_bvfunc_4, [t20_bvfunc_1], [t10_bvfunc_4, t11_bvfunc_1, t13_bvfunc_1, t14_bvfunc_1, t16_bvfunc_1, t4_bvfunc_1, t7_bvfunc_4, t8_bvfunc_4, t9_bvfunc_1], [redefinition_m2_fraenkel, dt_k14_bvfunc_1, dt_k1_fraenkel, fc3_margrel1]]
[-8, t24_tex_2, [], [d10_xboole_0, d1_pre_topc, d1_tdlat_3, d1_tex_1, d2_tdlat_3, t30_zfmisc_1, t38_zfmisc_1, t5_pre_topc], [cc1_tex_1, dt_k1_tex_2, dt_m1_pre_topc, fc2_tex_2]]
[-8, t44_bvfunc_6, [t43_bvfunc_6], [d11_bvfunc_1, d12_bvfunc_1, d14_bvfunc_1, d2_binarith, t18_binarith, t19_binarith, t20_binarith, t40_margrel1, t9_binarith], [commutativity_k15_bvfunc_1, redefinition_m2_fraenkel, dt_k1_fraenkel, fc3_margrel1]]
[-8, t82_tops_1, [t81_tops_1, d3_tops_1], [d10_xboole_0, d1_struct_0, d3_tarski, d3_tops_1, d7_xboole_0, t16_xboole_1, t38_tops_1, t39_tops_1, t51_pre_topc, t80_tops_1], [commutativity_k5_subset_1, dt_k5_subset_1]]
[-7, t11_bvfunc_4, [t20_bvfunc_1], [d11_bvfunc_1, d14_bvfunc_1, t10_bvfunc_4, t19_binarith, t39_margrel1, t41_margrel1, t43_margrel1, t7_binarith], []]
[-7, t12_bvfunc_4, [t20_bvfunc_1], [d11_bvfunc_1, d14_bvfunc_1, d5_valuat_1, t10_bvfunc_4, t19_binarith, t39_margrel1, t40_margrel1, t7_binarith], [redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k5_valuat_1, fc3_margrel1]]
[-7, t13_bvfunc_3, [t12_bvfunc_3], [d10_bvfunc_2, d15_bvfunc_1, d19_bvfunc_1, d20_bvfunc_1, d6_valuat_1, d9_bvfunc_2, t43_margrel1, t45_margrel1], [commutativity_k6_valuat_1, redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k6_bvfunc_2, dt_k7_bvfunc_2, fc3_margrel1]]
[-7, t13_bvfunc_4, [t20_bvfunc_1], [t10_bvfunc_4, t11_bvfunc_1, t13_bvfunc_1, t14_bvfunc_1, t17_bvfunc_1, t7_bvfunc_4, t8_bvfunc_4, t9_bvfunc_1], [redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k6_valuat_1, fc3_margrel1]]
[-7, t3_bvfunc_8, [t6_bvfunc_7], [d11_bvfunc_1, d2_funct_2, d6_valuat_1, d7_bvfunc_1, t20_binarith, t21_binarith, t9_binarith, t9_funct_1], [redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k6_valuat_1, fc3_margrel1]]
[-7, t3_pardepap, [t6_translac, d1_aff_1, t13_aff_1], [d11_aff_2, d3_aff_1, t12_aff_1, t26_aff_1, t37_aff_1, t46_aff_1, t50_aff_1, t57_aff_1, t63_aff_1, t65_aff_1], []]
[-7, t56_filter_0, [t52_lattices, t49_lattices], [d3_lattices, d7_lattices, t21_lattices, t31_lattices, t39_lattices, t40_lattices, t43_lattices, t47_lattices, t48_lattices], [dt_k7_lattices]]
[-7, t59_yellow_5, [t53_yellow_5, t48_yellow_5, t55_yellow_5, t17_lattice3], [d3_waybel_1, d3_yellow_0, t23_yellow_0, t2_yellow_5, t37_yellow_5, t39_yellow_5, t44_yellow_0, t4_waybel_1, t6_yellow_5, t85_waybel_1, t90_waybel_1], [reflexivity_r3_orders_2, dt_k1_yellow_5, dt_k3_yellow_0, cc8_waybel_1]]
[-7, t81_tmap_1, [d3_tmap_1, d4_tmap_1, t64_tmap_1], [d3_xboole_0, d4_tmap_1, t154_relat_1, t161_relat_1, t17_xboole_1, t1_tsep_1, t1_xboole_1, t32_tops_2, t48_tmap_1, t72_tmap_1], [dt_m1_pre_topc, cc1_pre_topc]]
[-7, t83_waybel_1, [d22_waybel_1, t73_waybel_1, t77_waybel_1], [d19_waybel_1, t15_lattice3, t23_yellow_0, t24_orders_2, t25_orders_2, t25_yellow_0, t44_yellow_0, t45_yellow_0, t70_waybel_1, t71_waybel_1], [cc2_lattice3, cc5_waybel_1, cc5_yellow_0, cc6_waybel_1, cc7_waybel_1, dt_k3_yellow_0, dt_k4_yellow_0, dt_l1_orders_2]]
[-7, t86_arytm_3, [t54_arytm_3, t62_arytm_3], [d7_arytm_3, d8_arytm_3, t19_ordinal2, t34_ordinal3, t41_arytm_3, t43_arytm_3, t45_arytm_3, t51_arytm_3, t52_ordinal2], [dt_k12_arytm_3]]
[-6, t29_classes2, [t28_classes2], [d3_tarski, t10_classes2, t22_classes2, t26_classes2, t35_classes1, t37_classes1, t8_classes2], [fc1_classes2]]
[-6, t38_waybel23, [t31_waybel23], [d15_yellow_0, d16_yellow_0, d1_waybel23, t18_waybel_0, t2_yellow_3, t2_yellow_5, t40_yellow_0], [dt_k7_waybel_0, cc2_lattice3, fc10_waybel_0, fc14_waybel_0]]
[-6, t39_fintopo2, [t38_fintopo2], [d3_tarski, t21_fin_topo, t21_fintopo2, t22_fintopo2, t2_tarski, t3_xboole_0, t54_subset_1], [involutiveness_k3_subset_1, dt_k3_subset_1, dt_k9_fintopo2]]
[-6, t4_bvfunc_8, [t5_bvfunc_7], [d11_bvfunc_1, d2_funct_2, d6_valuat_1, d7_bvfunc_1, t10_binarith, t23_binarith, t9_funct_1], [redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k8_bvfunc_1, fc3_margrel1]]
[-6, t53_xboole_1, [t41_xboole_1, t49_xboole_1], [d10_xboole_0, d2_xboole_0, d3_tarski, d3_xboole_0, d4_xboole_0, t19_xboole_1, t34_xboole_1, t7_xboole_1], [commutativity_k2_xboole_0, commutativity_k3_xboole_0, idempotence_k3_xboole_0]]
[-6, t61_tex_3, [], [t13_tex_2, t16_tsep_1, t1_tsep_1, t38_tex_1, t5_tex_2, t9_tex_3], [cc26_tex_3, cc8_tex_3]]
[-6, t69_rmod_2, [t68_rmod_2], [d10_xboole_0, d3_tarski, d6_rlvect_1, t28_rmod_2, t31_rmod_2, t66_vectsp_1, t7_vectsp_1], []]
[-5, t16_quantal1, [d18_quantal1, t13_quantal1, t11_quantal1, t12_quantal1], [d3_tarski, t11_quantal1, t12_quantal1, t13_quantal1, t15_quantal1, t25_lattices, t45_lattice3, t46_lattice3, t8_quantal1], [reflexivity_r3_lattices, dt_k1_quantal1, dt_l1_quantal1, cc1_lattices]]
[-5, t18_waybel21, [t32_yellow_2], [d18_yellow_0, t17_xboole_1, t17_yellow_0, t27_yellow_2, t50_yellow_0, t64_yellow_0], [cc2_waybel10]]
[-5, t19_waybel21, [t33_yellow_2], [d19_yellow_0, t17_xboole_1, t17_yellow_0, t26_yellow_2, t50_yellow_0, t65_yellow_0], [cc3_waybel10]]
[-5, t35_funct_4, [t31_funct_4, t28_funct_4], [d1_funct_4, d2_xboole_0, d3_xboole_0, d6_partfun1, t12_funct_4, t14_funct_4, t9_funct_1], [commutativity_k2_xboole_0, symmetry_r1_partfun1, reflexivity_r1_partfun1, dt_k1_funct_4]]
[-5, t35_waybel23, [t32_waybel23], [d15_yellow_0, d17_yellow_0, d2_waybel23, t17_waybel_0, t41_yellow_0, t9_yellow_5], [dt_k6_waybel_0, cc1_lattice3, fc9_waybel_0, fc13_waybel_0]]
[-5, t40_tops_3, [t39_tops_3], [d4_tops_3, d5_tops_1, t2_tdlat_3, t2_tops_3, t4_tdlat_3, t84_tops_1], [involutiveness_k3_subset_1, dt_k3_subset_1]]
[-5, t50_tex_3, [], [t13_tex_2, t1_tsep_1, t35_tex_1, t5_tex_2, t9_tex_3], [cc1_tdlat_3, cc23_tex_3, cc24_tex_3]]
[-5, t55_binari_5, [t25_binari_5, t37_binari_5, t43_binari_5, t49_binari_5], [d1_bvfunc_1, t10_binarith, t19_binarith, t20_binarith, t23_binarith, t39_margrel1, t40_margrel1, t41_margrel1, t50_margrel1], [cc1_bvfunc_1, cc1_margrel1, dt_k8_margrel1, fc1_bvfunc_1]]
[-5, t60_tex_3, [], [t13_tex_2, t16_tex_3, t1_tsep_1, t36_tex_1, t5_tex_2], [cc26_tex_3]]
[-5, t7_closure3, [d3_closure3, t6_closure3], [d16_pboole, d3_closure3, d3_pboole, d3_xboole_0, t70_funct_1, t90_relat_1, t9_funct_1], [reflexivity_r6_pboole]]
[-5, t82_pzfmisc1, [t74_pzfmisc1], [d21_pboole, d7_xboole_0, d8_pboole, t127_zfmisc_1, t3_pboole, t5_pboole], []]
[-4, t17_altcat_3, [t16_altcat_3, t15_altcat_3, t5_altcat_3], [d19_altcat_1, d7_altcat_3, d8_altcat_3, t24_altcat_1, t25_altcat_1, t2_altcat_3, t6_altcat_3], []]
[-4, t18_connsp_3, [t3_subset, t36_connsp_1, t67_xboole_1, t2_connsp_1, t9_connsp_3, t1_connsp_3], [d3_xboole_0, d5_connsp_1, d7_xboole_0, t10_subset_1, t11_connsp_3, t15_connsp_3, t1_connsp_3, t28_xboole_1, t5_connsp_3, t7_connsp_3], [reflexivity_r1_tarski, symmetry_r1_xboole_0, dt_k1_connsp_3]]
[-4, t20_bvfunc26, [t14_bvfunc26, t6_bvfunc_4, t13_bvfunc_1], [t11_bvfunc_1, t13_bvfunc_1, t17_bvfunc_1, t1_bvfunc26, t2_bvfunc26, t4_bvfunc_1, t6_bvfunc_4], [commutativity_k8_bvfunc_1, redefinition_m2_fraenkel, dt_k19_bvfunc_1, dt_k1_fraenkel, dt_k5_valuat_1, fc3_margrel1]]
[-4, t25_rmod_3, [t47_rmod_2, t21_rmod_3, t48_rmod_2, t18_rmod_3], [d1_rlvect_1, d2_rmod_3, d3_rmod_2, t18_rmod_3, t25_rmod_2, t28_xboole_1, t37_rmod_2, t37_zfmisc_1], [dt_k1_rmod_2, dt_m1_rmod_2]]
[-4, t25_vectsp_5, [t47_vectsp_4, t21_vectsp_5, t48_vectsp_4], [d1_rlvect_1, d2_vectsp_5, d3_vectsp_4, t25_vectsp_4, t28_xboole_1, t37_vectsp_4, t37_zfmisc_1], [commutativity_k2_vectsp_5, dt_k1_vectsp_4, dt_m1_vectsp_4]]
[-4, t29_bvfunc_5, [t22_bvfunc_5, t26_bvfunc_5], [d11_bvfunc_1, d14_bvfunc_1, t19_binarith, t39_margrel1, t41_margrel1, t7_binarith], [redefinition_m2_fraenkel, dt_k14_bvfunc_1, dt_k19_bvfunc_1, dt_k1_fraenkel, fc3_margrel1]]
[-4, t34_funct_4, [t24_funct_4, t32_funct_4], [d1_funct_4, t21_xboole_1, t25_funct_4, t83_xboole_1, t90_relat_1, t9_grfunc_1], [commutativity_k2_xboole_0, symmetry_r1_xboole_0]]
[-4, t37_ordinal1, [t36_ordinal1, t7_ordinal1], [d2_ordinal1, d3_ordinal1, d3_tarski, d4_ordinal1, t23_ordinal1, t24_ordinal1], [rc3_ordinal1]]
[-4, t46_classes2, [t27_classes1, t32_classes2], [d10_xboole_0, d4_classes1, t29_classes2, t43_classes2, t45_classes2, t5_classes1], [fc1_classes2]]
[-4, t59_tex_3, [], [t11_tsep_1, t1_tsep_1, t29_tex_3, t37_tex_1], [cc11_tdlat_3, cc11_tex_3]]
[-4, t65_tex_4, [t64_tex_4], [d10_xboole_0, t1_xboole_1, t31_tops_1, t37_tex_4, t61_tex_4], []]
[-4, t6_functor0, [t12_funct_6], [d2_funct_4, d2_zfmisc_1, t106_zfmisc_1, t13_funcop_1, t19_funcop_1], [redefinition_k10_pboole]]
[-4, t6_isocat_2, [t46_cat_1], [d13_cat_1, t19_cat_1, t22_cat_1, t56_cat_1, t57_cat_1], [redefinition_k10_cat_1, dt_k3_cat_1]]
[-4, t71_vectsp_4, [d5_vectsp_4, t4_subset, t70_vectsp_4], [d10_xboole_0, d3_tarski, d6_rlvect_1, t10_rlvect_1, t28_vectsp_4, t31_vectsp_4, t66_vectsp_1], [dt_k3_vectsp_4, dt_l2_struct_0, dt_l2_vectsp_1, dt_l3_vectsp_1, dt_l4_vectsp_1]]
[-4, t73_waybel_1, [t24_orders_2, t72_waybel_1], [d19_waybel_1, t23_yellow_0, t25_orders_2, t45_yellow_0, t70_waybel_1, t71_waybel_1], [cc2_lattice3, cc5_waybel_1, cc6_waybel_1, cc7_waybel_1, dt_l1_orders_2]]
[-4, t7_isocat_2, [t47_cat_1], [d13_cat_1, t19_cat_1, t22_cat_1, t56_cat_1, t58_cat_1], [redefinition_k10_cat_1, dt_k2_cat_1]]
[-3, t10_yellow_5, [t25_yellow_0], [d3_yellow_0, t23_yellow_0, t2_yellow_5, t6_yellow_5], [commutativity_k12_lattice3]]
[-3, t11_altcat_1, [d1_cat_1, t42_cqc_lang], [d1_funct_2, d5_funct_2, t11_relset_1, t35_zfmisc_1, t5_cqc_lang], []]
[-3, t12_pzfmisc1, [t11_pzfmisc1], [d1_pzfmisc1, d2_pzfmisc1, t3_pboole, t69_enumset1], [dt_k1_pzfmisc1, dt_k2_pzfmisc1, idempotence_k2_pboole, symmetry_r6_pboole]]
[-3, t131_funct_2, [], [d4_partfun1, t12_relset_1, t4_funct_2], [cc1_funct_2, redefinition_m2_relset_1]]
[-3, t13_relset_1, [t11_relset_1, t12_relset_1], [d1_relset_1, t119_zfmisc_1, t12_relset_1, t1_xboole_1, t21_relat_1], [cc1_relset_1, dt_m2_relset_1]]
[-3, t14_relset_1, [t11_relset_1, t12_relset_1], [d1_relset_1, t119_zfmisc_1, t12_relset_1, t1_xboole_1, t21_relat_1], [cc1_relset_1, dt_m2_relset_1]]
[-3, t17_equation, [t11_equation], [t13_extens_1, t15_equation, t17_mssubfam, t24_autalg_1], [dt_k2_msualg_3, reflexivity_r1_pzfmisc1]]
[-3, t187_relat_1, [t95_relat_1], [d7_xboole_0, t100_relat_1, t110_relat_1, t97_relat_1], [symmetry_r1_xboole_0]]
[-3, t18_bvfunc26, [t15_bvfunc26, t6_boole], [t12_bvfunc25, t17_bvfunc_1, t1_bvfunc26, t4_bvfunc_1, t8_bvfunc_4], [fc1_margrel1]]
[-3, t20_symsp_1, [t13_symsp_1, t14_symsp_1], [d2_symsp_1, d6_rlvect_1, t10_rlvect_1, t16_rlvect_1, t59_vectsp_1], [cc1_vectsp_1, cc4_vectsp_1, cc5_vectsp_1, dt_l2_vectsp_1, dt_l3_vectsp_1]]
[-3, t20_yellow_5, [t6_waybel_1], [d3_waybel_1, t14_lattice3, t17_lattice3, t18_lattice3], []]
[-3, t22_classes2, [t19_card_2, t20_classes2, t21_card_1, t46_card_1, t47_card_1], [d2_ordinal2, t10_classes2, t14_classes2, t21_card_1, t41_ordinal1, t46_card_1, t47_card_1, t6_classes2], [fc1_classes2, spc0_boole]]
[-3, t25_tdlat_1, [t107_tops_1, t111_tops_1], [d10_xboole_0, d6_tops_1, d8_tops_1, t111_tops_1, t48_tops_1], [dt_k1_tops_1, fc6_tops_1]]
[-3, t26_autgroup, [t23_autgroup, d6_group_1], [d6_autgroup, t113_funct_2, t21_funct_2, t25_autgroup, t30_group_3], [dt_k3_group_1]]
[-3, t27_bvfunc_5, [t19_bvfunc_5, t21_bvfunc_5, t24_bvfunc_5, t25_bvfunc_5], [d11_bvfunc_1, d14_bvfunc_1, t19_binarith, t20_binarith, t21_binarith, t39_margrel1, t7_binarith], [redefinition_m2_fraenkel, dt_k14_bvfunc_1, dt_k19_bvfunc_1, dt_k1_fraenkel, fc3_margrel1]]
[-3, t28_margrel1, [t15_finseq_2, t27_margrel1], [d11_finseq_1, d1_tarski, d8_margrel1, d9_finseq_1, t37_zfmisc_1], []]
[-3, t2_yellow_3, [t23_yellow_0, t26_orders_2], [d11_lattice3, d14_lattice3, t19_yellow_0, t21_yellow_0, t26_orders_2], [dt_k12_lattice3]]
[-3, t32_yellow_5, [t27_yellow_5], [d3_yellow_0, d3_yellow_5, t44_yellow_0, t6_yellow_5], [redefinition_r2_yellow_5]]
[-3, t34_waybel16, [t17_yellow_0, t24_waybel16], [d10_orders_2, d8_lattice3, t20_waybel16, t26_orders_2, t33_yellow_0], []]
[-3, t34_yellow_5, [d3_yellow_5, t23_yellow_5], [d3_yellow_0, d3_yellow_5, t10_yellow_5, t44_yellow_0, t6_yellow_5], [redefinition_k12_lattice3, cc1_lattice3]]
[-3, t43_conlat_1, [t40_conlat_1, t42_conlat_1], [d13_conlat_1, d22_conlat_1, t12_xboole_1, t16_conlat_1, t24_conlat_1], [dt_k5_conlat_1]]
[-3, t49_tex_3, [], [d6_tex_1, t1_tsep_1, t29_tex_3], [cc1_tdlat_3, cc22_tex_3]]
[-3, t49_vectsp_2, [t43_vectsp_2, t45_vectsp_2], [d13_vectsp_1, d19_vectsp_1, d4_group_1, t43_vectsp_2, t48_vectsp_2], [dt_k1_vectsp_2, dt_l2_vectsp_1, dt_l3_vectsp_1, cc4_vectsp_1]]
[-3, t50_binari_5, [d1_bvfunc_1, t37_binari_5, t39_binari_5, t39_margrel1, t41_margrel1], [d1_bvfunc_1, t10_binarith, t19_binarith, t23_binarith, t39_margrel1, t40_margrel1, t41_margrel1, t50_margrel1], [dt_k9_margrel1, involutiveness_k9_margrel1]]
[-3, t51_pzfmisc1, [t12_pboole], [d1_pzfmisc1, d4_pboole, d9_pboole, t64_zfmisc_1], [dt_k1_pzfmisc1]]
[-3, t53_lattices, [t52_lattices, t49_lattices], [t26_lattices, t27_lattices, t41_lattices, t47_lattices, t52_lattices], [commutativity_k4_lattices, dt_k7_lattices, dt_l3_lattices, cc1_lattices]]
[-3, t58_tex_3, [], [d7_tex_1, t1_tsep_1, t35_tex_3], [cc25_tex_3]]
[-3, t5_bvfunc_2, [d9_bvfunc_2, t33_bvfunc_1], [d18_bvfunc_1, d19_bvfunc_1, d1_t_1topsp, d6_eqrel_1, t3_xboole_0], [redefinition_k1_bvfunc_2, dt_k5_bvfunc_2]]
[-3, t5_hessenbe, [t14_collsp], [d7_anproj_2, d8_anproj_2, t3_hessenbe, t4_hessenbe], []]
[-3, t65_yellow_5, [t83_waybel_1], [d23_waybel_1, t11_yellow_5, t4_waybel_1, t5_waybel_1], [cc10_waybel_1, cc2_lattice3, cc8_waybel_1]]
[-3, t66_yellow_5, [t83_waybel_1], [d23_waybel_1, t11_yellow_5, t4_waybel_1, t5_waybel_1], [cc10_waybel_1, cc2_lattice3, cc8_waybel_1]]
[-3, t6_bvfunc_2, [d10_bvfunc_2, t34_bvfunc_1], [d18_bvfunc_1, d1_t_1topsp, d20_bvfunc_1, d6_eqrel_1, t3_xboole_0], [redefinition_k1_bvfunc_2, dt_k5_bvfunc_2]]
[-3, t73_cat_1, [t63_cat_1, t68_cat_1, t70_cat_1], [t54_cat_1, t57_cat_1, t58_cat_1, t60_cat_1, t65_cat_1, t70_cat_1], []]
[-3, t7_bvfunc13, [t6_bvfunc13, t21_bvfunc_2], [t11_partit_2, t13_partit_2, t17_partit_2, t20_bvfunc_2, t8_bvfunc11], [redefinition_k1_bvfunc_2]]
[-3, t8_pzfmisc1, [t4_pzfmisc1], [d1_pzfmisc1, d1_tarski, d4_pboole, t3_pboole], [reflexivity_r6_pboole, existence_m1_pboole, dt_k1_pzfmisc1]]
[-2, t100_semi_af1, [d1_semi_af1, d6_semi_af1], [d5_semi_af1, t81_semi_af1, t82_semi_af1, t89_semi_af1], [dt_k2_semi_af1, dt_l1_analoaf, existence_m1_subset_1]]
[-2, t109_pboole, [t108_pboole], [t10_pboole, t11_pboole, t9_pboole], [symmetry_r4_pboole]]
[-2, t10_pzfmisc1, [t6_pzfmisc1], [d2_pzfmisc1, d2_tarski, d4_pboole], [reflexivity_r6_pboole, existence_m1_pboole, dt_k2_pzfmisc1]]
[-2, t11_connsp_3, [t9_connsp_3, t7_connsp_3], [t10_connsp_3, t34_connsp_1, t5_connsp_3, t8_connsp_3], [dt_k1_connsp_3]]
[-2, t13_mod_1, [d13_vectsp_1, t40_vectsp_1], [d13_vectsp_1, t27_rlvect_1, t36_vectsp_1, t43_vectsp_1], [dt_k2_group_1, dt_l1_vectsp_1, dt_l2_vectsp_1, dt_l3_vectsp_1, existence_m1_subset_1]]
[-2, t149_pboole, [d9_relat_1], [d16_pboole, d3_pboole, d5_funct_1], [dt_m1_pboole]]
[-2, t14_mod_1, [d19_vectsp_1, t41_vectsp_1], [d19_vectsp_1, t27_rlvect_1, t39_vectsp_1, t45_vectsp_1], [dt_k2_group_1, dt_l1_vectsp_1, dt_l2_vectsp_1, dt_l3_vectsp_1, existence_m1_subset_1]]
[-2, t15_arytm_1, [t12_arytm_1], [d1_arytm_1, t12_arytm_2, t7_arytm_2], [commutativity_k7_arytm_2, dt_k1_arytm_1]]
[-2, t15_finset_1, [], [t13_finset_1, t17_xboole_1], [fc11_finset_1]]
[-2, t164_orders_1, [d7_relat_1, t163_orders_1], [d11_orders_1, d12_orders_1, d7_relat_1, t38_relat_1], [dt_k4_relat_1, involutiveness_k4_relat_1]]
[-2, t166_orders_1, [d7_relat_1, t165_orders_1], [d13_orders_1, d14_orders_1, d7_relat_1, t38_relat_1], [dt_k4_relat_1, involutiveness_k4_relat_1]]
[-2, t16_coh_sp, [d4_tarski, t38_zfmisc_1], [d1_classes1, d1_tarski, d4_tarski, t12_zfmisc_1], [reflexivity_r1_tarski]]
[-2, t16_finset_1, [], [t13_finset_1, t36_xboole_1], [fc12_finset_1]]
[-2, t16_pzfmisc1, [t6_pzfmisc1, t8_pzfmisc1], [d1_pzfmisc1, d2_pzfmisc1, t3_pboole, t8_zfmisc_1], [dt_k1_pzfmisc1, redefinition_r6_pboole, reflexivity_r6_pboole, symmetry_r6_pboole]]
[-2, t18_bvfunc13, [t20_bvfunc_2, t15_bvfunc13], [t20_bvfunc_2, t21_bvfunc11, t21_bvfunc_2, t7_bvfunc13], [redefinition_k1_bvfunc_2, redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k6_bvfunc_2, fc3_margrel1]]
[-2, t19_mboolean, [t1_mboolean], [d1_mboolean, d4_pboole, d5_pboole], [reflexivity_r6_pboole, existence_m1_pboole, dt_k1_mboolean]]
[-2, t1_pboole, [], [d9_relat_1, d9_setfam_1], [fc6_funct_1]]
[-2, t20_tops_1, [t44_subset_1], [d7_xboole_0, t32_subset_1, t37_xboole_1], []]
[-2, t21_tex_2, [], [t20_tex_2, t8_tex_2], [cc12_tex_2, dt_k1_tex_2]]
[-2, t21_xboole_1, [t10_xboole_1, t20_xboole_1], [d10_xboole_0, d2_xboole_0, d3_tarski, d3_xboole_0], [commutativity_k2_xboole_0, reflexivity_r1_tarski]]
[-2, t22_ordinal1, [d8_xboole_0, t19_ordinal1, t21_ordinal1], [d2_ordinal1, d8_xboole_0, t1_xboole_1, t21_ordinal1, t7_ordinal1], []]
[-2, t22_xboole_1, [t14_xboole_1, t17_xboole_1], [d10_xboole_0, d2_xboole_0, d3_tarski, d3_xboole_0], [commutativity_k3_xboole_0, reflexivity_r1_tarski]]
[-2, t24_conlat_1, [d14_conlat_1, d15_conlat_1], [d16_conlat_1, d17_conlat_1, t18_conlat_1, t19_conlat_1], [dt_k5_conlat_1, dt_k6_conlat_1, dt_l2_conlat_1]]
[-2, t25_bvfunc_5, [t24_bvfunc_5, t2_bvfunc_5], [d11_bvfunc_1, d14_bvfunc_1, t41_margrel1, t7_binarith], [redefinition_m2_fraenkel, dt_k14_bvfunc_1, dt_k1_fraenkel, fc3_margrel1]]
[-2, t26_conlat_1, [d13_conlat_1, d14_conlat_1, d15_conlat_1, t24_conlat_1, t25_conlat_1], [d13_conlat_1, d14_conlat_1, d15_conlat_1, d16_conlat_1, d17_conlat_1, t18_conlat_1, t19_conlat_1], [abstractness_v6_conlat_1, dt_k5_conlat_1, dt_k6_conlat_1, dt_l2_conlat_1]]
[-2, t27_autgroup, [t19_group_1, t23_autgroup, t26_autgroup], [d6_autgroup, t113_funct_2, t21_funct_2, t25_autgroup, t30_group_3], [cc1_group_1, dt_k3_group_1, dt_l1_group_1]]
[-2, t28_yellow_5, [t4_waybel_1], [d3_yellow_0, t23_yellow_0, t44_yellow_0], [cc2_lattice3, commutativity_k12_lattice3, dt_k3_yellow_0, redefinition_k12_lattice3]]
[-2, t29_yellow18, [d6_yellow18, t4_yellow18], [d4_yellow18, d6_yellow18, t26_yellow18, t4_yellow18], [symmetry_r1_yellow18, symmetry_r3_yellow18, dt_k1_yellow18, fc2_yellow18, fc3_yellow18]]
[-2, t30_xboole_1, [t12_xboole_1, t24_xboole_1], [d10_xboole_0, d2_xboole_0, d3_tarski, d3_xboole_0], [commutativity_k3_xboole_0]]
[-2, t32_e_siec, [d10_e_siec, t16_e_siec, t21_e_siec], [d3_e_siec, t20_e_siec, t36_xboole_1, t3_xboole_1, t49_relat_1], []]
[-2, t33_mod_4, [t32_mod_4], [d16_group_1, t11_grcat_1, t28_mod_4], [cc1_vectsp_1, cc4_vectsp_1, dt_l2_vectsp_1, dt_l3_vectsp_1]]
[-2, t34_ordinal1, [d10_xboole_0, t10_ordinal1, t13_ordinal1, t24_ordinal1, t26_ordinal1], [d10_xboole_0, d1_tarski, d2_ordinal1, d2_xboole_0, t10_ordinal1, t14_ordinal1, t24_ordinal1], [antisymmetry_r2_hidden, redefinition_r1_ordinal1, reflexivity_r1_ordinal1]]
[-2, t36_pboole, [t16_pboole, t25_pboole], [d13_pboole, t16_pboole, t17_pboole, t19_pboole], [commutativity_k2_pboole, commutativity_k3_pboole, dt_k2_pboole]]
[-2, t37_pboole, [t17_pboole, t24_pboole], [d13_pboole, t16_pboole, t17_pboole, t18_pboole], [commutativity_k2_pboole, commutativity_k3_pboole, dt_k3_pboole]]
[-2, t38_vectsp_2, [t78_rlsub_2], [d6_rlvect_1, t10_rlvect_1, t16_rlvect_1], [commutativity_k4_rlvect_1, redefinition_k4_rlvect_1, dt_k6_rlvect_1]]
[-2, t3_bvfunc_5, [t13_bvfunc_1], [d14_bvfunc_1, d7_bvfunc_1, t19_binarith], [commutativity_k8_bvfunc_1, redefinition_m2_fraenkel, dt_k1_fraenkel, fc3_margrel1]]
[-2, t41_cat_3, [d12_cat_3], [d15_cat_1, t23_cat_1, t40_cat_3], []]
[-2, t43_fintopo2, [t32_subset_1, t41_fintopo2], [t2_tarski, t32_subset_1, t38_fintopo2, t40_fintopo2], [dt_k10_fintopo2, dt_k9_fintopo2]]
[-2, t44_cat_3, [d13_cat_3], [d16_cat_1, t23_cat_1, t43_cat_3], []]
[-2, t45_binari_5, [d1_bvfunc_1, t21_binarith, t36_binari_5, t37_binari_5, t39_binari_5, t39_margrel1, t41_margrel1], [d1_bvfunc_1, t10_binarith, t19_binarith, t20_binarith, t23_binarith, t39_margrel1, t40_margrel1, t41_margrel1, t50_margrel1], [cc1_margrel1, dt_k7_margrel1, dt_k8_margrel1, dt_k9_margrel1, involutiveness_k9_margrel1]]
[-2, t45_connsp_1, [t43_connsp_1, t44_connsp_1, t4_subset], [d3_xboole_0, d7_xboole_0, t37_connsp_1, t40_connsp_1, t43_connsp_1], [existence_m1_subset_1]]
[-2, t45_oposet_1, [d27_oposet_1, d28_oposet_1], [d27_oposet_1, d28_oposet_1, t30_oposet_1, t32_oposet_1], [cc4_oposet_1, cc5_oposet_1]]
[-2, t45_xboole_1, [t12_xboole_1, t39_xboole_1], [d2_xboole_0, d3_tarski, d4_xboole_0, t2_tarski], []]
[-2, t4_bvfunc13, [t8_bvfunc11, t19_bvfunc11], [t11_bvfunc11, t11_partit_2, t20_bvfunc_2, t21_bvfunc_2], [reflexivity_r1_bvfunc_1, redefinition_k5_valuat_1, redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k5_valuat_1, dt_k7_bvfunc_2, fc3_margrel1]]
[-2, t4_fintopo2, [t30_fin_topo], [d15_fin_topo, d16_fin_topo, t23_fin_topo], [involutiveness_k3_subset_1, dt_k3_subset_1]]
[-2, t4_tsep_1, [t35_borsuk_1, t4_topmetr], [d9_pre_topc, t16_xboole_1, t17_xboole_1, t28_xboole_1], [dt_m1_pre_topc]]
[-2, t50_rmod_2, [t47_rmod_2], [d3_rmod_2, t19_rmod_2, t35_rmod_2], [dt_k1_rmod_2, dt_l1_group_1, dt_l1_vectsp_1, dt_l1_vectsp_2, dt_l2_vectsp_1, dt_l3_vectsp_1, dt_m1_rmod_2]]
[-2, t50_vectsp_4, [t47_vectsp_4], [d3_vectsp_4, t19_vectsp_4, t35_vectsp_4], [dt_k1_vectsp_4, dt_l2_struct_0, dt_l2_vectsp_1, dt_l3_vectsp_1, dt_l4_vectsp_1, dt_m1_vectsp_4]]
[-2, t51_xboole_1, [t22_xboole_1, t39_xboole_1, t47_xboole_1], [d10_xboole_0, d2_xboole_0, d3_tarski, d3_xboole_0, d4_xboole_0], [commutativity_k2_xboole_0, commutativity_k3_xboole_0]]
[-2, t51_yellow_5, [t22_yellow_0, t48_yellow_5], [t16_lattice3, t37_yellow_5, t39_yellow_5, t4_waybel_1], [redefinition_r3_orders_2, dt_k13_lattice3, cc8_waybel_1]]
[-2, t53_setfam_1, [], [d10_xboole_0, t51_setfam_1], [involutiveness_k7_setfam_1]]
[-2, t54_binari_5, [d17_margrel1, t35_binari_5, t37_binari_5, t50_margrel1], [d1_bvfunc_1, t19_binarith, t20_binarith, t21_binarith, t39_margrel1, t7_binarith], [cc1_bvfunc_1, cc1_margrel1, commutativity_k10_margrel1, dt_k7_margrel1, dt_k8_margrel1, fc1_bvfunc_1]]
[-2, t54_yellow_5, [t50_yellow_5], [t20_yellow_5, t37_yellow_5, t5_waybel_1], [commutativity_k13_lattice3, dt_k1_yellow_5, cc8_waybel_1]]
[-2, t55_boolealg, [d1_boolealg, t50_boolealg, t49_lattices], [d11_lattices, t39_lattices, t47_lattices, t49_lattices, t50_lattices], [dt_k7_lattices]]
[-2, t55_yellow_5, [t23_yellow_0, t47_yellow_5, t52_yellow_5], [t17_lattice3, t18_lattice3, t20_yellow_5, t37_yellow_5, t5_waybel_1], [redefinition_r3_orders_2, dt_k12_lattice3, cc8_waybel_1]]
[-2, t55_zfmisc_1, [t38_zfmisc_1, t3_xboole_0], [d1_xboole_0, d2_tarski, d3_xboole_0, d7_xboole_0], [reflexivity_r1_tarski]]
[-2, t57_yellow_5, [d1_yellow_5, t52_yellow_5, t90_waybel_1], [d3_waybel_1, t37_yellow_5, t39_yellow_5, t4_waybel_1, t90_waybel_1], [redefinition_k12_lattice3, dt_k7_waybel_1, cc2_lattice3, cc8_waybel_1]]
[-2, t5_fintopo2, [t31_fin_topo], [d15_fin_topo, d16_fin_topo, t22_fin_topo], [involutiveness_k3_subset_1, dt_k3_subset_1]]
[-2, t5_mboolean, [t49_pboole], [d5_pboole, t2_xboole_1, t5_pboole], []]
[-2, t5_waybel28, [d5_yellow_6], [d1_waybel_0, d6_waybel_0, t12_pre_topc], []]
[-2, t61_bvfunc26, [t43_bvfunc26, t6_boole], [t13_bvfunc_1, t55_bvfunc26, t5_bvfunc_1, t6_bvfunc_4], [fc1_margrel1]]
[-2, t61_funct_2, [t37_zfmisc_1, t7_funct_2], [d1_funct_2, t12_relset_1, t14_funct_1, t37_zfmisc_1], [reflexivity_r1_tarski]]
[-2, t67_bvfunc26, [t14_bvfunc26, t6_boole, t8_bvfunc_4], [t11_bvfunc_1, t17_bvfunc_1, t1_bvfunc26, t2_bvfunc26, t4_bvfunc_1], [dt_k1_fraenkel, fc1_margrel1, fc3_margrel1, redefinition_k5_valuat_1, redefinition_m2_fraenkel]]
[-2, t67_partfun2, [t37_zfmisc_1, t65_partfun2], [d1_tarski, d4_finseq_4, t16_grfunc_1, t8_funct_1], [reflexivity_r1_tarski]]
[-2, t69_enumset1, [t41_enumset1], [d1_tarski, d2_tarski, t2_tarski], [idempotence_k2_xboole_0]]
[-2, t6_tex_2, [t7_rpr_1], [d1_tex_2, t24_zfmisc_1, t5_tex_2], [cc3_tex_2, dt_k6_domain_1]]
[-2, t6_tsep_2, [t5_tsep_2], [t18_pre_topc, t26_subset_1, t2_tsep_2], [dt_k3_subset_1]]
[-2, t70_rmod_2, [t29_rmod_2, d1_rlvect_1, t64_rmod_2], [d23_vectsp_2, t26_rlvect_1, t28_rlvect_1, t29_rmod_2, t43_rlvect_1], [dt_l2_struct_0, dt_l2_vectsp_1, dt_l1_rlvect_1, dt_l1_vectsp_2, dt_l3_vectsp_1, dt_m1_rmod_2]]
[-2, t71_yellow_5, [d3_yellow_5, t53_yellow_5], [d3_yellow_5, t16_lattice3, t37_yellow_5, t4_waybel_1], [redefinition_k12_lattice3, dt_k1_yellow_5, cc8_waybel_1]]
[-2, t76_waybel_1, [t45_yellow_0, t72_waybel_1], [d19_waybel_1, t45_yellow_0, t71_waybel_1, t72_waybel_1], [cc2_lattice3, cc5_waybel_1, cc6_waybel_1, cc7_waybel_1, dt_k4_yellow_0, dt_l1_orders_2]]
[-2, t81_pzfmisc1, [t66_pzfmisc1], [d21_pboole, d5_pboole, t119_zfmisc_1], []]
[-2, t81_zfmisc_1, [t79_zfmisc_1, t7_xboole_1, t8_xboole_1], [d1_zfmisc_1, d2_xboole_0, d3_tarski, t1_xboole_1, t7_xboole_1], [commutativity_k2_xboole_0]]
[-2, t86_waybel_1, [t85_waybel_1, t84_waybel_1, t24_orders_2, t15_lattice3, t26_orders_2], [d19_waybel_1, t15_lattice3, t16_lattice3, t24_orders_2, t25_yellow_0, t4_waybel_1, t85_waybel_1], [dt_k7_waybel_1, cc5_waybel_1]]
[-2, t86_xboole_1, [t33_xboole_1, t83_xboole_1], [d3_tarski, d3_xboole_0, d4_xboole_0, d7_xboole_0], []]
[-2, t8_lattice2, [t79_funct_4], [d1_funct_4, t12_xboole_1, t8_grfunc_1], []]
[-2, t95_relat_1, [d7_xboole_0, t90_relat_1, t64_relat_1, t60_relat_1], [d11_relat_1, d2_relat_1, d3_xboole_0, d4_relat_1, d7_xboole_0, t2_tarski], [commutativity_k3_xboole_0, dt_k7_relat_1]]
[-2, t9_partit_2, [t98_orders_1], [d10_xboole_0, t19_relset_1, t8_partit_2], []]
[-2, t9_pzfmisc1, [t4_pzfmisc1], [d1_pzfmisc1, d1_tarski, d4_pboole], [dt_k1_pboole, dt_k1_pzfmisc1, reflexivity_r6_pboole]]
[-2, t9_robbins1, [d9_robbins1, t5_robbins1, t7_robbins1], [d5_lattices, d7_robbins1, d9_robbins1, t3_robbins1, t4_robbins1], [cc1_robbins1, dt_l2_robbins1, existence_m1_subset_1, redefinition_k6_robbins1]]
[-1, t103_enumset1, [t45_enumset1], [t44_enumset1, t98_enumset1], [commutativity_k2_tarski]]
[-1, t10_bvfunc_4, [t7_bvfunc_4, t20_bvfunc_1, t19_bvfunc_1], [d14_bvfunc_1, d6_valuat_1, t45_margrel1, t7_bvfunc_4], [reflexivity_r1_bvfunc_1, redefinition_m2_fraenkel, dt_k1_fraenkel, fc3_margrel1]]
[-1, t10_nattra_1, [d4_cat_2, d8_cat_1, t8_nattra_1], [d1_funct_2, t12_relset_1, t8_nattra_1, t97_relat_1], [abstractness_v1_cat_1, dt_m3_cat_2, existence_m1_subset_1, reflexivity_r1_tarski]]
[-1, t10_tops_3, [d3_pre_topc], [d1_tops_3, t43_tops_1], [cc5_tops_1, cc6_tops_1, dt_l1_pre_topc, fc2_pre_topc, fc5_pre_topc, fc8_tops_1]]
[-1, t10_xboole_1, [t1_xboole_1, t7_xboole_1], [t1_xboole_1, t7_xboole_1, t9_xboole_1], [commutativity_k2_xboole_0]]
[-1, t114_pboole, [t111_pboole], [t110_pboole, t17_pboole], [symmetry_r4_pboole, dt_k3_pboole]]
[-1, t11_algspec1, [d3_pboole, t10_algspec1], [d3_pboole, t3_pboole, t9_algspec1], [dt_k1_algspec1, dt_m1_pboole, reflexivity_r6_pboole]]
[-1, t11_projpl_1, [t5_projpl_1], [d5_projpl_1, t1_projpl_1], []]
[-1, t11_yellow_0, [t4_yellow_0], [d9_lattice3, t26_orders_2], []]
[-1, t120_funct_1, [t117_relat_1, t157_relat_1], [d12_funct_1, d3_tarski, t85_funct_1], [dt_k8_relat_1]]
[-1, t128_partfun1, [t125_partfun1, t127_partfun1, t1_xboole_1], [d3_tarski, t119_partfun1, t120_partfun1, t32_partfun1], []]
[-1, t12_altcat_1, [t43_cqc_lang], [t11_altcat_1, t6_cqc_lang], []]
[-1, t12_yellow_0, [t4_yellow_0], [d8_lattice3, t26_orders_2], []]
[-1, t13_grcat_1, [d17_vectsp_2, d4_algstr_1, t5_grcat_1, t8_grcat_1], [d1_tarski, d25_vectsp_1, d4_algstr_1, t18_funct_2, t5_grcat_1], [abstractness_v1_rlvect_1, cc1_relset_1, dt_k1_algstr_1, dt_k2_algstr_1, dt_k2_midsp_1, dt_k7_vectsp_1, dt_l1_rlvect_1, dt_m2_relset_1, dt_u2_struct_0, fc1_grcat_1, free_g1_rlvect_1, redefinition_m2_relset_1]]
[-1, t13_realset2, [t12_realset2, t7_realset2], [d14_realset2, t4_realset2, t6_realset2], []]
[-1, t14_hessenbe, [t3_hessenbe, d7_anproj_2, t8_hessenbe], [d7_anproj_2, d8_anproj_2, t3_hessenbe, t4_hessenbe], []]
[-1, t14_robbins1, [t12_robbins1, t5_robbins1, t9_robbins1], [d6_robbins1, d7_robbins1, t3_robbins1, t9_robbins1], [cc2_robbins1, existence_m1_subset_1]]
[-1, t152_sheffer2, [t83_sheffer2], [t136_sheffer2, t151_sheffer2], [dt_l1_sheffer1]]
[-1, t153_sheffer2, [t83_sheffer2], [t152_sheffer2, t83_sheffer2], [dt_k5_sheffer1, dt_l1_sheffer1]]
[-1, t15_bvfunc13, [t20_bvfunc_2, t7_bvfunc13], [t21_bvfunc11, t21_bvfunc_2, t7_bvfunc13], [redefinition_k1_bvfunc_2, redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k7_bvfunc_2, fc3_margrel1]]
[-1, t15_hessenbe, [t3_hessenbe, t8_hessenbe], [d8_anproj_2, t3_hessenbe, t4_hessenbe], []]
[-1, t15_mboolean, [t21_pboole, t44_pboole], [d5_pboole, d8_pboole, t108_xboole_1], [dt_k3_pboole]]
[-1, t15_pzfmisc1, [d13_pboole, t14_pzfmisc1], [d1_pzfmisc1, t3_pboole, t6_zfmisc_1], [dt_k1_pzfmisc1]]
[-1, t161_funct_1, [t147_funct_1], [d10_xboole_0, t158_funct_1], []]
[-1, t16_classes2, [t14_classes2], [d2_ordinal2, t10_classes2], []]
[-1, t16_latsum_1, [t40_waybel_0, t4_subset], [d19_waybel_0, d1_waybel_0, t22_yellow_0], [dt_l1_orders_2, existence_m1_subset_1, redefinition_k13_lattice3]]
[-1, t17_bvfunc13, [t20_bvfunc_2, t14_bvfunc13], [t1_bvfunc13, t20_bvfunc_2, t21_bvfunc_2], [redefinition_k1_bvfunc_2, redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k6_bvfunc_2, fc3_margrel1]]
[-1, t17_classes2, [t15_classes2], [d2_ordinal2, t10_classes2], []]
[-1, t17_mcart_1, [t13_mcart_1, t15_mcart_1], [d1_tarski, d2_tarski, t10_mcart_1], []]
[-1, t17_projpl_1, [t5_projpl_1], [d7_incproj, t5_projpl_1], [existence_m1_subset_1]]
[-1, t17_relset_1, [t15_relset_1, t16_relset_1], [d1_relset_1, t119_zfmisc_1, t1_xboole_1], []]
[-1, t18_binop_1, [t11_binop_1], [d7_binop_1, t17_binop_1], []]
[-1, t18_bvfunc11, [t15_bvfunc11, t21_bvfunc_2], [t18_partit_2, t20_bvfunc_2, t8_bvfunc11], [redefinition_k1_bvfunc_2, redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k6_bvfunc_2, fc3_margrel1]]
[-1, t18_mcart_1, [t12_mcart_1, t16_mcart_1], [d1_tarski, d2_tarski, t10_mcart_1], []]
[-1, t190_relat_1, [t94_relat_1, t96_relat_1], [d15_relat_1, t1_xboole_1, t99_relat_1], [fc13_relat_1]]
[-1, t19_toler_1, [d15_relat_2, d7_relat_2, t15_toler_1, t97_orders_1], [d15_relat_2, d1_eqrel_1, d7_relat_2, t106_zfmisc_1, t97_orders_1], [dt_k1_eqrel_1, fc1_eqrel_1, fc2_eqrel_1]]
[-1, t19_tsep_2, [t51_tsep_1, t16_tsep_2], [d7_xboole_0, t16_tsep_2, t51_tsep_1], [symmetry_r2_tsep_1]]
[-1, t1_latsubgr, [t97_group_2], [d10_group_2, d9_group_2], [dt_k8_group_2, dt_l1_group_1, redefinition_k9_group_2]]
[-1, t1_oposet_1, [t97_orders_1], [d6_relat_1, t71_relat_1], [dt_k6_partfun1]]
[-1, t20_finset_1, [d3_zfmisc_1], [d3_zfmisc_1, t19_finset_1], [fc14_finset_1]]
[-1, t21_finset_1, [t13_finset_1, t54_mcart_1], [d4_zfmisc_1, t19_finset_1, t20_finset_1], [fc14_finset_1, fc15_finset_1, reflexivity_r1_tarski]]
[-1, t21_yellow19, [t9_waybel_0, t27_yellow_6], [d11_waybel_0, d12_yellow_6, t21_funct_2], [dt_m2_yellow_6]]
[-1, t22_arytm_1, [t21_arytm_1, t20_arytm_1], [d2_arytm_1, t11_arytm_1, t3_arytm_1], [commutativity_k7_arytm_2, dt_k1_arytm_1]]
[-1, t22_bvfunc13, [t20_bvfunc_2, t11_bvfunc13], [t11_bvfunc13, t21_bvfunc11, t21_bvfunc_2], [redefinition_k1_bvfunc_2, redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k7_bvfunc_2, fc3_margrel1]]
[-1, t22_bvfunc26, [t1_bvfunc26, t6_bvfunc_1, t7_bvfunc26], [t10_bvfunc_1, t17_bvfunc_1, t1_bvfunc26, t4_bvfunc_1], [commutativity_k6_valuat_1, redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k3_bvfunc26, fc3_margrel1]]
[-1, t22_net_1, [d9_net_1], [d9_net_1, t6_net_1], []]
[-1, t22_pre_topc, [t17_pre_topc], [t15_pre_topc, t48_xboole_1], [involutiveness_k3_subset_1, dt_k3_subset_1]]
[-1, t23_supinf_1, [t21_supinf_1, t22_supinf_1], [d7_supinf_1, t22_supinf_1, t6_supinf_1], [dt_k5_supinf_1]]
[-1, t24_lmod_6, [t18_lmod_6], [d7_lmod_6, t50_vectsp_4], [reflexivity_r1_lmod_6]]
[-1, t24_robbins3, [t24_yellow_0, t25_yellow_0], [t13_lattice3, t24_yellow_0, t25_yellow_0], [cc14_oposet_1, commutativity_k13_lattice3, dt_l1_oposet_1, redefinition_k12_lattice3, redefinition_k13_lattice3, redefinition_r3_orders_2]]
[-1, t24_xboole_1, [t22_xboole_1, t23_xboole_1, t4_xboole_1], [d10_xboole_0, d2_xboole_0, d3_tarski, d3_xboole_0], [commutativity_k2_xboole_0, commutativity_k3_xboole_0, idempotence_k3_xboole_0]]
[-1, t25_arytm_1, [t24_arytm_1], [d2_arytm_1, t4_arytm_1], [commutativity_k7_arytm_2]]
[-1, t25_lukasi_1, [t15_lukasi_1, t3_lukasi_1, t78_cqc_the1, t79_cqc_the1], [t15_lukasi_1, t24_lukasi_1, t3_lukasi_1, t77_cqc_the1, t82_cqc_the1], [dt_k10_cqc_lang, dt_k12_cqc_lang, dt_k7_cqc_lang, dt_k8_qc_lang1, fc2_cqc_lang, redefinition_m2_subset_1]]
[-1, t25_net_1, [d10_net_1], [d10_net_1, t6_net_1], []]
[-1, t26_finset_1, [t146_relat_1], [t146_relat_1, t17_finset_1], [fc13_finset_1]]
[-1, t26_ordinal3, [t49_ordinal2, t26_ordinal1, t23_ordinal1, t7_ordinal1], [d2_ordinal1, d8_xboole_0, t21_ordinal1, t24_ordinal3, t25_ordinal3], [redefinition_r1_ordinal1, dt_k14_ordinal2]]
[-1, t26_yellow_2, [t53_yellow_0], [d12_lattice3, d9_yellow_0], [existence_m1_subset_1]]
[-1, t27_finset_1, [t147_funct_1], [t147_funct_1, t17_finset_1], [fc13_finset_1]]
[-1, t28_waybel_8, [t3_subset, t4_waybel_7], [d1_lattice3, d2_lattice3, d2_yellow_1], [reflexivity_r1_tarski]]
[-1, t28_wellord1, [t26_wellord1], [d2_relat_1, t16_wellord1], [idempotence_k3_xboole_0]]
[-1, t29_arytm_3, [t28_arytm_3, t6_arytm_3], [t25_arytm_3, t6_arytm_3, t84_ordinal3], [cc1_ordinal1, dt_k4_ordinal2, fc1_arytm_3, symmetry_r1_arytm_3]]
[-1, t29_lukasi_1, [t25_lukasi_1, t13_lukasi_1, t27_lukasi_1, t19_lukasi_1], [t11_lukasi_1, t13_lukasi_1, t25_lukasi_1, t27_lukasi_1, t82_cqc_the1], [redefinition_m2_subset_1, dt_k10_cqc_lang, dt_k12_cqc_lang, dt_k7_cqc_lang, dt_k8_qc_lang1, fc2_cqc_lang]]
[-1, t29_sysrel, [t43_funct_1], [t71_relat_1, t77_relat_1], [idempotence_k3_xboole_0]]
[-1, t29_xboole_1, [t10_xboole_1, t17_xboole_1], [t17_xboole_1, t1_xboole_1, t7_xboole_1], [commutativity_k2_xboole_0, commutativity_k3_xboole_0]]
[-1, t2_alg_1, [t3_subset, d7_unialg_2, t7_unialg_2], [d7_unialg_2, t17_finseq_1, t6_unialg_2, t7_unialg_2], [fc1_struct_0, reflexivity_r1_tarski, redefinition_m2_unialg_2, dt_k1_unialg_2, dt_l1_unialg_1, dt_u1_unialg_1]]
[-1, t2_rcomp_2, [d2_square_1, t6_wsierp_1], [t2_xreal_1, t46_square_1, t49_square_1], [cc2_xreal_0]]
[-1, t2_yellow_5, [t25_yellow_0], [d3_yellow_0, t23_yellow_0], [cc2_lattice3, dt_l1_orders_2, redefinition_k12_lattice3, reflexivity_r3_orders_2]]
[-1, t30_bvfunc_5, [t8_bvfunc_5, t26_bvfunc_5, t22_bvfunc_5], [d11_bvfunc_1, d14_bvfunc_1, t41_margrel1, t7_binarith], [redefinition_m2_fraenkel, dt_k14_bvfunc_1, dt_k1_fraenkel, fc3_margrel1]]
[-1, t30_projpl_1, [t16_projpl_1, t24_projpl_1], [d2_projpl_1, d9_projpl_1, t16_projpl_1], [dt_k1_projpl_1]]
[-1, t31_projpl_1, [t24_projpl_1, t16_projpl_1], [d7_incproj, d8_projpl_1, t24_projpl_1], [dt_k2_projpl_1]]
[-1, t31_xboole_1, [t13_xboole_1, t17_xboole_1], [d2_xboole_0, d3_tarski, d3_xboole_0], [commutativity_k2_xboole_0, commutativity_k3_xboole_0]]
[-1, t32_boolealg, [d1_boolealg, t31_boolealg], [d4_boolealg, d7_lattices, t40_lattices], [dt_k7_lattices]]
[-1, t32_coh_sp, [t27_coh_sp], [d19_coh_sp, d4_tarski], [dt_k6_partfun1, fc2_partfun1, redefinition_k6_partfun1, reflexivity_r1_tarski]]
[-1, t32_projpl_1, [t16_projpl_1], [d9_incproj, t16_projpl_1], [existence_m1_subset_1, dt_k1_projpl_1]]
[-1, t33_lukasi_1, [t15_lukasi_1, t79_cqc_the1], [t28_lukasi_1, t3_lukasi_1, t79_cqc_the1], [dt_k10_cqc_lang, dt_k7_cqc_lang, dt_k8_qc_lang1, fc2_cqc_lang, redefinition_m2_subset_1]]
[-1, t33_sheffer2, [t20_sheffer2], [t28_sheffer2, t30_sheffer2], [dt_l1_sheffer1]]
[-1, t34_finsub_1, [t27_finsub_1], [d5_finsub_1, t13_finset_1], []]
[-1, t34_relat_1, [t31_relat_1, t17_xboole_1, t3_relat_1, t19_xboole_1], [d2_xboole_0, d3_tarski, d3_xboole_0, t14_relat_1, t27_relat_1], [commutativity_k3_xboole_0]]
[-1, t35_oposet_1, [d13_oposet_1, d19_oposet_1, d9_oposet_1], [d13_oposet_1, d19_oposet_1, d9_oposet_1, t22_relat_2], [cc1_partfun1, cc1_relset_1, dt_m2_relset_1, dt_u1_orders_2]]
[-1, t35_tops_3, [d3_tops_1, d4_tops_3, t30_tdlat_3], [d3_tops_1, d4_tops_3, t32_tops_3, t33_tops_3], [dt_k1_tops_1, dt_l1_pre_topc, existence_m1_subset_1]]
[-1, t36_funct_4, [t32_funct_4], [t138_partfun1, t35_funct_4], [commutativity_k2_xboole_0, symmetry_r1_xboole_0]]
[-1, t36_supinf_1, [d10_supinf_1, t21_supinf_1], [d10_supinf_1, d7_supinf_1, t6_supinf_1], [dt_k5_supinf_1]]
[-1, t37_boolealg, [t35_boolealg, d4_boolealg], [d4_boolealg, d7_lattices, t40_lattices], [commutativity_k4_lattices, dt_k4_lattices, dt_l3_lattices, cc1_lattices]]
[-1, t37_lattice4, [t39_lattices, t48_lattices], [t47_lattices, t48_lattices, t50_lattices], [cc1_lattices, cc5_lattices, cc7_lattices, commutativity_k3_lattices, dt_k5_lattices, dt_k7_lattices, dt_l3_lattices]]
[-1, t37_sheffer2, [t20_sheffer2], [t20_sheffer2, t33_sheffer2], [dt_k5_sheffer1]]
[-1, t38_filter_2, [d11_filter_2], [d10_xboole_0, d11_filter_2], [dt_l1_lattices, fc1_struct_0, reflexivity_r1_filter_2, reflexivity_r1_tarski, existence_m1_subset_1, dt_l3_lattices, dt_m2_filter_2, dt_m2_lattice4]]
[-1, t38_tops_1, [d1_pre_topc, d5_pre_topc], [t30_subset_1, t30_tops_1, t36_tops_1], [dt_k5_subset_1]]
[-1, t3_fintopo2, [t2_fintopo2, t32_subset_1], [t2_fintopo2, t2_tarski, t32_subset_1], [dt_k7_fin_topo, dt_k8_fin_topo]]
[-1, t3_funct_2, [d4_partfun1, t24_partfun1], [d1_funct_2, t65_relat_1, t9_relset_1], [cc1_funct_2, redefinition_k4_relset_1, redefinition_m2_relset_1]]
[-1, t40_parsp_1, [t36_parsp_1, t38_parsp_1], [t36_parsp_1, t38_parsp_1, t39_parsp_1], [dt_l1_parsp_1]]
[-1, t42_bvfunc13, [t20_bvfunc_2, t36_bvfunc13], [t21_bvfunc11, t21_bvfunc_2, t24_bvfunc13], [redefinition_k1_bvfunc_2]]
[-1, t42_filter_1, [t41_filter_1, t40_filter_1], [d15_lattices, t40_filter_1, t41_filter_1], [dt_k8_filter_1, fc2_filter_1, cc3_lattices, cc4_lattices]]
[-1, t44_bvfunc13, [t19_partit_2, t21_bvfunc_2], [t21_bvfunc11, t21_bvfunc_2, t26_bvfunc13], [dt_k1_fraenkel, dt_k5_valuat_1, fc3_margrel1, redefinition_k1_bvfunc_2, redefinition_k5_valuat_1, redefinition_m2_fraenkel]]
[-1, t46_grfunc_1, [], [t25_grfunc_1], [cc1_funct_1, cc2_funct_1, fc1_xboole_0]]
[-1, t48_vectsp_2, [t39_vectsp_2, t43_vectsp_2], [d21_vectsp_1, t36_vectsp_1, t43_vectsp_2], [cc1_vectsp_1, cc4_vectsp_1, dt_k1_vectsp_2, dt_l2_vectsp_1, dt_l3_vectsp_1]]
[-1, t49_oposet_1, [d22_oposet_1, d24_oposet_1], [d22_oposet_1, d25_oposet_1, t39_oposet_1], [cc12_oposet_1, cc5_oposet_1, dt_l1_oposet_1]]
[-1, t4_boolealg, [t22_lattices, t2_filter_0], [t22_lattices, t23_lattices, t25_lattices], [cc1_lattices, dt_k1_lattices, dt_l3_lattices, redefinition_k3_lattices, redefinition_r3_lattices]]
[-1, t4_hessenbe, [t11_collsp], [d7_anproj_2, d8_anproj_2], []]
[-1, t51_classes2, [t27_classes1], [d1_classes2, t27_classes1], [cc3_classes2, fc1_classes2]]
[-1, t51_ens_1, [t42_ens_1], [t19_cat_1, t52_cat_1], [dt_k2_cat_1]]
[-1, t51_tex_3, [t30_tex_3], [t10_tsep_1, t29_tex_3], [cc1_pre_topc, dt_l1_pre_topc, dt_m1_pre_topc, rc11_tex_1]]
[-1, t52_binari_6, [d2_binari_5, t22_binari_6], [t20_binarith, t23_binari_5, t23_binarith], [fc2_bvfunc_1]]
[-1, t53_classes2, [t51_classes2], [d1_classes2, t27_classes1], [cc1_ordinal1]]
[-1, t53_funct_1, [d8_funct_1, t23_funct_1, t34_funct_1], [t27_funct_1, t47_funct_1, t52_funct_1, t71_relat_1], [dt_k6_relat_1, fc2_funct_1]]
[-1, t55_procal_1, [t82_cqc_the1, t54_procal_1, t8_procal_1], [t3_lukasi_1, t5_procal_1, t82_cqc_the1, t8_procal_1], [redefinition_m2_subset_1, dt_k13_cqc_lang, dt_k7_cqc_lang, dt_k8_qc_lang1, fc2_cqc_lang]]
[-1, t55_transgeo, [t44_transgeo, t52_transgeo], [t24_diraf, t35_funct_1, t51_transgeo], [cc1_funct_2, cc4_funct_2, dt_k6_partfun1, dt_k6_relat_1, fc2_partfun1, redefinition_k6_partfun1, redefinition_m2_relset_1]]
[-1, t57_classes2, [d10_xboole_0, d2_ordinal1, t56_classes2], [t26_ordinal1, t42_classes1, t43_classes1, t54_classes2], [cc2_classes2]]
[-1, t58_rmod_3, [t57_rmod_3, t46_rmod_3], [d5_rmod_3, t46_rmod_3, t51_rmod_3], []]
[-1, t59_bvfunc13, [t47_bvfunc13], [t17_partit_2, t21_bvfunc_2], []]
[-1, t59_midsp_1, [t57_midsp_1, t18_midsp_1], [t27_midsp_1, t32_midsp_1, t43_midsp_1], []]
[-1, t5_boole, [d6_xboole_0, t1_boole, t3_boole, t4_boole], [d10_xboole_0, d1_xboole_0, d2_xboole_0, d3_tarski, d4_xboole_0], []]
[-1, t5_bvfunc_5, [t8_bvfunc_4, t13_bvfunc_1], [d11_bvfunc_1, d14_bvfunc_1, t19_binarith], [redefinition_m2_fraenkel, dt_k1_fraenkel, dt_k5_valuat_1, fc3_margrel1]]
[-1, t5_conmetr, [t4_subset, t76_analmetr], [t30_aff_1, t57_analmetr, t58_analmetr], [cc1_analmetr]]
[-1, t5_ordinal2, [t26_ordinal1, d4_tarski], [d2_ordinal1, d3_tarski, d4_tarski], [antisymmetry_r2_hidden, fc4_ordinal1]]
[-1, t60_xboole_1, [d8_xboole_0], [d10_xboole_0, d8_xboole_0], [antisymmetry_r2_xboole_0]]
[-1, t63_xboole_1, [d3_tarski, t3_xboole_0], [d7_xboole_0, t26_xboole_1, t3_xboole_1], []]
[-1, t66_pzfmisc1, [t65_pzfmisc1, t15_pboole], [d21_pboole, d5_pboole, t119_zfmisc_1], [dt_k11_pboole]]
[-1, t68_binari_6, [t4_binari_6, t16_binarith, t52_margrel1], [t10_binarith, t16_binarith, t40_margrel1, t52_margrel1], [dt_k9_margrel1]]
[-1, t68_xboole_1, [d5_xboole_0, t67_xboole_1], [d1_xboole_0, d3_tarski, t3_xboole_0], [symmetry_r1_xboole_0]]
[-1, t69_tops_1, [t52_pre_topc, t63_tops_1], [d3_tarski, d3_xboole_0, t52_pre_topc], []]
[-1, t6_altcat_3, [t2_altcat_3, d5_altcat_3, t5_altcat_3], [d1_altcat_3, d4_altcat_3, d5_altcat_3, t5_altcat_3], []]
[-1, t6_boolealg, [d1_boolealg, t2_filter_0], [t23_lattices, t25_lattices, t27_lattices], [dt_k7_lattices]]
[-1, t6_closure2, [t109_xboole_1, t3_subset], [t1_xboole_1, t33_xboole_1, t36_xboole_1], []]
[-1, t6_hessenbe, [t19_collsp], [d6_collsp, d8_anproj_2], [existence_m1_subset_1]]
[-1, t6_lukasi_1, [t2_lukasi_1, t5_lukasi_1], [t1_lukasi_1, t5_lukasi_1, t82_cqc_the1], [dt_k12_cqc_lang, dt_k7_cqc_lang, dt_k8_qc_lang1, fc2_cqc_lang, redefinition_m2_subset_1]]
[-1, t6_yellow14, [d3_pre_topc, t5_yellow14], [d1_struct_0, d1_xboole_0, d5_funct_1], [fc1_waybel12, fc2_pre_topc]]
[-1, t6_yellow_5, [t2_waybel_1], [d2_yellow_0, t23_yellow_0], []]
[-1, t72_yellow_5, [d3_yellow_5, t17_lattice3, t18_lattice3, t51_yellow_5, t55_yellow_5, t58_yellow_5, t63_yellow_5, t90_waybel_1], [d3_waybel_1, d3_yellow_0, d3_yellow_5, t10_yellow_5, t20_yellow_5, t22_yellow_0, t37_yellow_5, t4_waybel_1, t5_waybel_1], [cc10_waybel_1, cc2_lattice3, cc8_waybel_1, commutativity_k13_lattice3, dt_k10_lattice3, dt_l1_orders_2, existence_m1_subset_1, redefinition_k12_lattice3, redefinition_k13_lattice3]]
[-1, t73_bvfunc26, [t20_bvfunc26, t6_boole], [t13_bvfunc_1, t67_bvfunc26, t6_bvfunc_4], [fc1_margrel1]]
[-1, t73_filter_0, [t66_filter_0, t70_filter_0], [d15_lattices, t66_filter_0, t70_filter_0], [dt_k2_filter_0, dt_k8_filter_0, cc3_lattices]]
[-1, t73_supinf_1, [t69_supinf_1, t71_supinf_1], [t36_supinf_1, t69_supinf_1, t71_supinf_1], [dt_k5_supinf_1, dt_m2_supinf_1, existence_m2_supinf_1, reflexivity_r1_supinf_1]]
[-1, t74_waybel_1, [t72_waybel_1, t25_orders_2], [d19_waybel_1, t25_orders_2, t72_waybel_1], [cc5_waybel_1]]
[-1, t75_waybel_1, [t70_waybel_1, t23_yellow_0], [d19_waybel_1, t23_yellow_0, t70_waybel_1], [redefinition_k12_lattice3, dt_k12_lattice3, cc5_waybel_1]]
[-1, t76_binari_6, [t11_binari_6], [t23_binari_5, t52_margrel1], [dt_k9_margrel1]]
[-1, t76_lukasi_1, [t92_cqc_the1, t75_lukasi_1], [t41_lukasi_1, t92_cqc_the1, t98_cqc_the1], [redefinition_m2_subset_1, dt_k12_cqc_lang, dt_k7_cqc_lang, dt_k8_qc_lang1, fc2_cqc_lang]]
[-1, t7_mcart_4, [t5_mcart_2, t5_mcart_4], [d3_mcart_1, t3_mcart_2, t3_mcart_4], []]
[-1, t7_projdes1, [t6_projdes1, t9_collsp], [d7_anproj_2, d8_anproj_2, t1_projdes1], []]
[-1, t7_yellow_5, [t3_waybel_1], [d2_yellow_0, t22_yellow_0], []]
[-1, t82_binari_6, [t23_binari_6, t21_binarith], [t20_binarith, t21_binarith, t9_binarith], [dt_k9_margrel1]]
[-1, t83_xboole_1, [t2_boole, t3_boole, d7_xboole_0, t48_xboole_1, t47_xboole_1], [d10_xboole_0, d3_tarski, d3_xboole_0, d4_xboole_0, d7_xboole_0, t4_xboole_0], [commutativity_k3_xboole_0, symmetry_r1_xboole_0]]
[-1, t86_binari_6, [d2_bvfunc_1, d2_binarith], [t23_binari_5, t85_binari_6, t9_binarith], [commutativity_k10_margrel1, commutativity_k2_binarith, involutiveness_k9_margrel1, dt_k9_margrel1, fc2_binarith]]
[-1, t87_sheffer2, [t83_sheffer2], [d13_sheffer1, t86_sheffer2], [dt_l1_sheffer1]]
[-1, t88_lukasi_1, [t64_lukasi_1, t65_lukasi_1, t76_lukasi_1, t98_cqc_the1], [t64_lukasi_1, t69_lukasi_1, t76_lukasi_1, t92_cqc_the1, t98_cqc_the1], [dt_k10_cqc_lang, dt_k12_cqc_lang, dt_k7_cqc_lang, dt_k8_qc_lang1, fc2_cqc_lang, redefinition_m2_subset_1]]
[-1, t89_lukasi_1, [t64_lukasi_1, t65_lukasi_1, t76_lukasi_1, t98_cqc_the1], [t65_lukasi_1, t67_lukasi_1, t76_lukasi_1, t92_cqc_the1, t98_cqc_the1], [dt_k10_cqc_lang, dt_k12_cqc_lang, dt_k7_cqc_lang, dt_k8_qc_lang1, fc2_cqc_lang, redefinition_m2_subset_1]]
[-1, t8_mcart_1, [t7_mcart_1], [d1_mcart_1, d2_mcart_1], []]
[-1, t8_yellow_5, [t24_yellow_0], [d3_yellow_0, t22_yellow_0], [commutativity_k13_lattice3, redefinition_r3_orders_2, cc1_lattice3]]
[-1, t90_lukasi_1, [t86_lukasi_1, t89_lukasi_1], [t71_lukasi_1, t92_cqc_the1, t98_cqc_the1], [dt_k10_cqc_lang, dt_k7_cqc_lang, dt_k8_qc_lang1, fc2_cqc_lang, redefinition_m2_subset_1]]
[-1, t91_tmap_1, [t11_grcat_1], [d11_grcat_1, t35_funct_1], []]
[-1, t9_hessenbe, [t3_hessenbe, t8_hessenbe], [d7_anproj_2, d8_anproj_2, t3_hessenbe], []]
[-1, t9_projpl_1, [d10_incproj, d9_incproj, d12_incproj], [d5_incproj, d7_incproj, d9_incproj, t8_projpl_1], []]