%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP197^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:07:09 AM UTC 2026
% Result : Theorem 119.92s 95.17s
% Output : Refutation 121.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP197^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.11/0.20 % Computer : n001.cluster.edu
% 0.11/0.20 % Model : x86_64 x86_64
% 0.11/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.20 % Memory : 8046.5625MB
% 0.11/0.20 % OS : Linux 6.8.0-71-generic
% 0.11/0.20 % CPULimit : 300
% 0.11/0.20 % WCLimit : 300
% 0.11/0.20 % DateTime : Tue Sep 29 20:16:36 UTC 2026
% 0.11/0.20 % CPUTime :
% 0.11/0.20 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.90/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.08/1.19 % [INFO] Parsing done (396ms).
% 2.40/1.21 % [INFO] Running in sequential loop mode.
% 3.32/1.59 % [INFO] eprover registered as external prover.
% 3.51/1.60 % [INFO] Scanning for conjecture ...
% 3.69/1.76 % [INFO] Found a conjecture (or negated_conjecture) and 298 axioms. Running axiom selection ...
% 4.24/1.92 % [INFO] Axiom selection finished. Selected 297 axioms (removed 1 axioms).
% 5.27/2.22 % [INFO] Problem is higher-order (TPTP THF).
% 5.27/2.25 % [INFO] Type checking passed.
% 5.27/2.26 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 119.92/95.17 % External prover 'e' found a proof!
% 119.92/95.17 % [INFO] Killing All external provers ...
% 119.92/95.17 % Time passed: 94818ms (effective reasoning time: 93954ms)
% 119.92/95.17 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 119.92/95.17 % Axioms used in derivation (297): tcon_fun___Orderings_Obot, fact_24_type__scheme_Osimps_I12_J, fact_61_insert__absorb, fact_207_less__supI2, fact_143_dom__id__subst, fact_91_not__psubset__empty, fact_172_UnE, fact_66_insertE, fact_226_app__subst__Nil, fact_230_transpose_Ocases, fact_178_Un__assoc, fact_233_list_Oexhaust, fact_205_sup__set__def, fact_234_list_Oinducts, fact_126_linorder__less__wlog, fact_144_psubsetD, fact_57_not__Cons__self2, fact_221_lexordp__eq__refl, fact_193_bound__tv__type__scheme_Osimps_I3_J, fact_87_new__tv__TVar__subst, fact_246_successively_Oinduct, tcon_Nat_Onat___Orderings_Opreorder_5, tcon_Nat_Onat___Orderings_Ono__top, fact_36_type__scheme_Ocase__distrib, fact_39_singletonI, tcon_HOL_Obool___Orderings_Oorder_21, fact_95_is__singletonI_H, tcon_Nat_Onat___Orderings_Olinorder, tcon_Set_Oset___Orderings_Opreorder_12, fact_227_lexordp__eq__simps_I3_J, fact_117_less__induct, fact_25_type__scheme_Osimps_I11_J, fact_140_id__subst__def, fact_42_insert__absorb2, fact_37_singleton__conv, fact_177_ball__Un, fact_107_less__asym, fact_71_insert__not__empty, fact_195_free__tv__fun__def, fact_8_type__scheme_Odistinct_I1_J, tcon_HOL_Obool___Orderings_Opreorder_19, fact_173_UnI1, fact_218_lexordp__eq__antisym, fact_34_type__scheme_Oinduct, fact_121_linorder__cases, fact_179_Un__absorb, fact_243_sorted__wrt_Oinduct, fact_110_less__linear, fact_85_typ_Oinject_I1_J, fact_82_bot_Oextremum__strict, fact_4_type__scheme_Osimps_I13_J, tcon_fun___Orderings_Oord, fact_81_bot_Onot__eq__extremum, tcon_Nat_Onat___Orderings_Oord_7, fact_12_free__tv__type__scheme_Osimps_I1_J, fact_196_sup__bot__left, fact_30_typ__substitutions__only__on__free__variables, fact_133_is__singletonE, fact_75_Collect__conv__if2, fact_88_eq__free__eq__subst__scheme__list, fact_186_Un__empty__right, fact_70_singleton__inject, fact_239_min__list_Ocases, fact_65_insertI1, fact_21_new__tv__FVar, fact_44_empty__iff, fact_161_the1I2, fact_86_new__tv__TVar, fact_185_Un__empty__left, fact_0_type__scheme_Oinject_I1_J, tcon_fun___Lattices_Obounded__semilattice__sup__bot, fact_142_new__tv__Fun, fact_235_neq__Nil__conv, fact_159_theI2, fact_51_empty__Collect__eq, fact_135_free__tv__id__subst, fact_152_typ_Osimps_I6_J, fact_222_lexordp__eq_Ocases, tcon_HOL_Obool___Orderings_Oord_22, fact_209_sup_Ostrict__order__iff, fact_104_order_Oasym, fact_108_less__asym_H, tcon_Nat_Onat___Type__Mirabelle__sfxnzmapfi_Oof__nat, fact_43_list_Oinject, fact_249_strict__sorted_Ocases, fact_253_lexordp__eq_Oinducts, fact_38_singleton__conv2, fact_109_less__trans, fact_59_insert__commute, fact_189_insert__is__Un, fact_74_singletonD, fact_134_is__singleton__def, fact_7_app__subst__type__scheme_Osimps_I3_J, fact_90_bot__set__def, tcon_Type__Mirabelle__sfxnzmapfi_Otype__scheme___Type__Mirabelle__sfxnzmapfi_Otype__struct_26, fact_46_Collect__mem__eq, fact_69_insert__compr, tcon_Set_Oset___Lattices_Obounded__semilattice__sup__bot_9, tcon_HOL_Obool___Lattices_Obounded__semilattice__sup__bot_16, fact_223_lexordp__eq_Osimps, fact_180_Un__commute, fact_127_dual__order_Ostrict__trans, tcon_HOL_Obool___Orderings_Obot_23, fact_130_dual__order_Ostrict__implies__not__eq, fact_169_Un__insert__left, tcon_Nat_Onat___Orderings_Oorder__bot_4, fact_251_free__tv__list_Osimps_I1_J, fact_68_insert__Collect, tcon_fun___Lattices_Obounded__lattice_2, fact_132_mk__scheme_Osimps_I1_J, fact_27_mk__scheme__Fun, fact_182_Collect__disj__eq, fact_84_bound__tv__type__scheme_Osimps_I1_J, fact_111_less__irrefl, fact_138_mk__scheme_Osimps_I2_J, fact_100_lt__ex, help_If_1_1_T, fact_5_type__scheme_Osimps_I10_J, tcon_fun___Lattices_Osemilattice__sup, fact_28_eq__free__eq__subst__te, fact_124_less__imp__not__less, fact_2_scheme__substitutions__only__on__free__variables, fact_120_less__imp__triv, fact_101_gt__ex, fact_94_typ_Osimps_I5_J, fact_32_free__tv__type__scheme_Osimps_I2_J, tcon_fun___Type__Mirabelle__sfxnzmapfi_Otype__struct, fact_19_new__tv__Fun2, fact_160_If__def, fact_224_lexordp__eq__simps_I1_J, fact_116_less__not__sym, fact_137_the__elem__def, fact_220_lexordp__eq__trans, fact_231_list_Odistinct_I1_J, fact_250_strict__sorted_Oinduct, fact_208_sup_Ostrict__boundedE, fact_202_sup__eq__bot__iff, fact_240_min__list_Oinduct, fact_67_empty__def, fact_198_sup__bot_Oright__neutral, fact_33_type__scheme_Oexhaust, fact_252_bound__tv__list_Osimps_I1_J, fact_125_exists__least__iff, tcon_Set_Oset___Orderings_Obot_15, fact_73_singleton__iff, fact_77_the__elem__eq, fact_20_new__tv__BVar, fact_157_theI, fact_128_not__less__iff__gr__or__eq, fact_229_new__tv__Nil, fact_232_list_OdiscI, fact_210_sup_Ostrict__coboundedI1, fact_103_neq__iff, tcon_Nat_Onat___Orderings_Owellorder, fact_31_mk__scheme__injective, tcon_Set_Oset___Lattices_Osemilattice__sup_10, fact_131_bot__fun__def, tcon_Set_Oset___Orderings_Oorder__bot_11, fact_203_bot__eq__sup__iff, fact_45_mem__Collect__eq, fact_176_bex__Un, fact_114_dual__order_Oasym, fact_102_neqE, tcon_Nat_Onat___Orderings_Obot_8, fact_163_Collect__empty__eq__bot, fact_26_type__scheme_Odistinct_I5_J, fact_40_insertCI, fact_241_shuffles_Oinduct, fact_156_cod__id__subst, fact_201_sup__bot_Oeq__neutr__iff, fact_58_mk__disjoint__insert, fact_35_new__tv__def, fact_10_app__subst__Cons, fact_119_less__imp__not__eq2, tcon_HOL_Obool___Orderings_Olinorder_20, fact_248_map__tailrec__rev_Oinduct, fact_228_lexordp__eq_ONil, fact_148_app__subst__Fun, fact_92_app__subst__TVar, fact_204_sup__Un__eq, fact_151_typ_Odistinct_I1_J, fact_105_dense, fact_63_Set_Oset__insert, fact_183_Un__left__commute, tcon_HOL_Obool___Lattices_Osemilattice__sup_17, fact_113_ord__less__eq__trans, fact_171_weaken__asm__Un, fact_47_Collect__cong, fact_244_remdups__adj_Oinduct, fact_191_free__tv__Fun, help_If_2_1_T, tcon_Set_Oset___Lattices_Obounded__lattice_1, fact_247_list__nonempty__induct, fact_225_lexordp__eq__simps_I2_J, fact_3_app__subst__type__scheme_Osimps_I1_J, help_If_3_1_T, tcon_fun___Orderings_Oorder__bot, fact_197_sup__bot__right, fact_50_Collect__empty__eq, fact_199_sup__bot_Oneutr__eq__iff, fact_96_ord__eq__less__subst, tcon_List_Olist___Type__Mirabelle__sfxnzmapfi_Otype__struct_24, fact_83_free__tv__TVar, fact_245_arg__min__list_Oinduct, fact_190_bound__tv__list_Osimps_I2_J, fact_18_subst__mk__scheme, fact_9_type__scheme_Odistinct_I3_J, fact_158_theI_H, fact_211_sup_Ostrict__coboundedI2, fact_181_Un__left__absorb, fact_78_bot__apply, fact_219_lexordp__eq__linear, fact_155_the__equality, fact_145_less__set__def, fact_184_insert__def, fact_52_new__if__subst__type__scheme__list, fact_162_the1__equality, fact_236_list__induct2_H, fact_16_type__scheme_Oinject_I2_J, fact_216_lexordp__eq_OCons__eq, tcon_fun___Orderings_Opreorder, fact_215_lexordp__eq__simps_I4_J, fact_1_eq__free__eq__subst__type__scheme, fact_194_free__tv__list_Osimps_I2_J, fact_174_UnI2, fact_166_UnCI, fact_146_psubset__trans, fact_72_doubleton__eq__iff, fact_115_less__imp__not__eq, fact_164_bot__empty__eq, fact_213_theI__unique, fact_54_equals0I, fact_64_insertI2, fact_153_the__sym__eq__trivial, fact_17_new__tv__Cons, fact_60_insert__eq__iff, fact_15_type__scheme_Oinject_I3_J, fact_11_free__tv__mk__scheme, fact_49_all__not__in__conv, tcon_Set_Oset___Orderings_Oorder_13, fact_170_Un__insert__right, fact_76_Collect__conv__if, fact_187_singleton__Un__iff, fact_106_less__imp__neq, fact_29_eq__subst__te__eq__free, fact_98_order__less__subst1, fact_99_order__less__subst2, fact_22_type__scheme_Osimps_I15_J, fact_55_equals0D, fact_122_dual__order_Oirrefl, fact_154_the__eq__trivial, tcon_Set_Oset___Orderings_Oord_14, tcon_fun___Orderings_Oorder, fact_212_Nitpick_OThe__psimp, fact_147_new__tv__id__subst, fact_150_typ_Oinduct, fact_175_Un__def, fact_93_is__singleton__the__elem, fact_188_Un__singleton__iff, fact_139_Type__Mirabelle__sfxnzmapfi_Odom__def, fact_13_new__if__subst__type__scheme, fact_237_splice_Oinduct, fact_141_typ_Oinject_I2_J, tcon_HOL_Obool___Lattices_Obounded__lattice, fact_123_order_Ostrict__trans, fact_56_emptyE, fact_53_ex__in__conv, fact_136_Set_Ois__empty__def, tcon_Type__Mirabelle__sfxnzmapfi_Otyp___Type__Mirabelle__sfxnzmapfi_Otype__struct_25, fact_14_typ_Ocase__distrib, fact_217_lexordp__eq_OCons, fact_112_ord__eq__less__trans, fact_129_order_Ostrict__implies__not__eq, fact_168_Un__empty, fact_238_induct__list012, fact_41_insert__iff, fact_79_bound__tv__type__scheme_Osimps_I2_J, fact_214_sup__bot_Osemilattice__neutr__axioms, fact_62_insert__ident, tcon_Nat_Onat___Lattices_Osemilattice__sup_3, fact_254_insert__Nil, fact_206_less__supI1, fact_167_Un__iff, fact_192_free__tv__type__scheme_Osimps_I3_J, fact_89_scheme__list__substitutions__only__on__free__variables, fact_97_ord__less__eq__subst, tcon_HOL_Obool___Orderings_Oorder__bot_18, tcon_Type__Mirabelle__sfxnzmapfi_Otyp___Type__Mirabelle__sfxnzmapfi_Otyp__of, fact_149_typ_Oexhaust, fact_118_antisym__conv3, fact_165_free__tv__subst, fact_242_remdups__adj_Ocases, fact_6_app__subst__type__scheme_Osimps_I2_J, fact_23_type__scheme_Osimps_I14_J, fact_80_is__singletonI, fact_200_sup__bot_Oleft__neutral, tcon_Nat_Onat___Orderings_Oorder_6
% 119.92/95.17 % No. of inferences in proof: 598
% 119.92/95.17 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 94818 ms resp. 93954 ms w/o parsing
% 121.10/95.44 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 121.10/95.44 thf(type_M1610475166scheme_type, type, type_M1610475166scheme: $tType).
% 121.10/95.44 thf(type_Mirabelle_typ_type, type, type_Mirabelle_typ: $tType).
% 121.10/95.44 thf(nat_type, type, nat: $tType).
% 121.10/95.44 thf(bounded_lattice_decl, type, bounded_lattice: !> [TA: $tType]: $o).
% 121.10/95.44 thf(bot_decl, type, bot: !> [TA: $tType]: $o).
% 121.10/95.44 thf(ord_decl, type, ord: !> [TA: $tType]: $o).
% 121.10/95.44 thf(order_decl, type, order: !> [TA: $tType]: $o).
% 121.10/95.44 thf(no_bot_decl, type, no_bot: !> [TA: $tType]: $o).
% 121.10/95.44 thf(no_top_decl, type, no_top: !> [TA: $tType]: $o).
% 121.10/95.44 thf(linorder_decl, type, linorder: !> [TA: $tType]: $o).
% 121.10/95.44 thf(preorder_decl, type, preorder: !> [TA: $tType]: $o).
% 121.10/95.44 thf(order_bot_decl, type, order_bot: !> [TA: $tType]: $o).
% 121.10/95.44 thf(wellorder_decl, type, wellorder: !> [TA: $tType]: $o).
% 121.10/95.44 thf(dense_order_decl, type, dense_order: !> [TA: $tType]: $o).
% 121.10/95.44 thf(semilattice_sup_decl, type, semilattice_sup: !> [TA: $tType]: $o).
% 121.10/95.44 thf(type_M201404320of_nat_decl, type, type_M201404320of_nat: !> [TA: $tType]: $o).
% 121.10/95.44 thf(type_M1535146424typ_of_decl, type, type_M1535146424typ_of: !> [TA: $tType]: $o).
% 121.10/95.44 thf(bounde1808546759up_bot_decl, type, bounde1808546759up_bot: !> [TA: $tType]: $o).
% 121.10/95.44 thf(type_M1470978233struct_decl, type, type_M1470978233struct: !> [TA: $tType]: $o).
% 121.10/95.44 thf(the_decl, type, the: !> [TA: $tType]: ((TA > $o) > TA)).
% 121.10/95.44 thf(if_decl, type, if: !> [TA: $tType]: ($o > (TA > (TA > TA)))).
% 121.10/95.44 thf(semilattice_neutr_decl, type, semilattice_neutr: !> [TA: $tType]: ((TA > (TA > TA)) > (TA > $o))).
% 121.10/95.44 thf(sup_sup_decl, type, sup_sup: !> [TA: $tType]: (TA > (TA > TA))).
% 121.10/95.44 thf(insert_decl, type, insert: !> [TA: $tType]: (TA > ((list @ TA) > (list @ TA)))).
% 121.10/95.44 thf(cons_decl, type, cons: !> [TA: $tType]: (TA > ((list @ TA) > (list @ TA)))).
% 121.10/95.44 thf(nil_decl, type, nil: !> [TA: $tType]: (list @ TA)).
% 121.10/95.44 thf(ord_lexordp_eq_decl, type, ord_lexordp_eq: !> [TA: $tType]: ((list @ TA) > ((list @ TA) > $o))).
% 121.10/95.44 thf(bot_bot_decl, type, bot_bot: !> [TA: $tType]: TA).
% 121.10/95.44 thf(ord_less_decl, type, ord_less: !> [TA: $tType]: (TA > (TA > $o))).
% 121.10/95.44 thf(collect_decl, type, collect: !> [TA: $tType]: ((TA > $o) > (set @ TA))).
% 121.10/95.44 thf(insert2_decl, type, insert2: !> [TA: $tType]: (TA > ((set @ TA) > (set @ TA)))).
% 121.10/95.44 thf(is_empty_decl, type, is_empty: !> [TA: $tType]: ((set @ TA) > $o)).
% 121.10/95.44 thf(is_singleton_decl, type, is_singleton: !> [TA: $tType]: ((set @ TA) > $o)).
% 121.10/95.44 thf(the_elem_decl, type, the_elem: !> [TA: $tType]: ((set @ TA) > TA)).
% 121.10/95.44 thf(type_Mirabelle_cod_decl, type, type_Mirabelle_cod: ((nat > type_Mirabelle_typ) > (set @ nat))).
% 121.10/95.44 thf(type_Mirabelle_dom_decl, type, type_Mirabelle_dom: ((nat > type_Mirabelle_typ) > (set @ nat))).
% 121.10/95.44 thf(type_M17369686_subst_decl, type, type_M17369686_subst: (nat > type_Mirabelle_typ)).
% 121.10/95.44 thf(type_M540877363scheme_decl, type, type_M540877363scheme: (type_Mirabelle_typ > type_M1610475166scheme)).
% 121.10/95.44 thf(type_M1046766514new_tv_decl, type, type_M1046766514new_tv: !> [TA: $tType]: (nat > (TA > $o))).
% 121.10/95.44 thf(type_M167561660of_nat_decl, type, type_M167561660of_nat: !> [TA: $tType]: (nat > TA)).
% 121.10/95.44 thf(type_Mirabelle_Fun_decl, type, type_Mirabelle_Fun: (type_Mirabelle_typ > (type_Mirabelle_typ > type_Mirabelle_typ))).
% 121.10/95.44 thf(type_Mirabelle_TVar_decl, type, type_Mirabelle_TVar: (nat > type_Mirabelle_typ)).
% 121.10/95.44 thf(type_M1695911984se_typ_decl, type, type_M1695911984se_typ: !> [TA: $tType]: ((nat > TA) > ((type_Mirabelle_typ > (type_Mirabelle_typ > TA)) > (type_Mirabelle_typ > TA)))).
% 121.10/95.44 thf(type_M604437996typ_of_decl, type, type_M604437996typ_of: !> [TA: $tType]: (TA > type_Mirabelle_typ)).
% 121.10/95.44 thf(type_M1264524676e_BVar_decl, type, type_M1264524676e_BVar: (nat > type_M1610475166scheme)).
% 121.10/95.44 thf(type_M91906176e_FVar_decl, type, type_M91906176e_FVar: (nat > type_M1610475166scheme)).
% 121.10/95.44 thf(type_M1518733067e_SFun_decl, type, type_M1518733067e_SFun: (type_M1610475166scheme > (type_M1610475166scheme > type_M1610475166scheme))).
% 121.10/95.44 thf(type_M697345518scheme_decl, type, type_M697345518scheme: !> [TA: $tType]: ((nat > TA) > ((nat > TA) > ((type_M1610475166scheme > (type_M1610475166scheme > TA)) > (type_M1610475166scheme > TA))))).
% 121.10/95.44 thf(type_M1705333808scheme_decl, type, type_M1705333808scheme: !> [TA: $tType]: ((nat > TA) > ((nat > TA) > ((type_M1610475166scheme > (type_M1610475166scheme > (TA > (TA > TA)))) > (type_M1610475166scheme > TA))))).
% 121.10/95.44 thf(type_M353778473_subst_decl, type, type_M353778473_subst: !> [TA: $tType]: ((nat > type_Mirabelle_typ) > (TA > TA))).
% 121.10/95.44 thf(type_M779184887und_tv_decl, type, type_M779184887und_tv: !> [TA: $tType]: (TA > (set @ nat))).
% 121.10/95.44 thf(type_M950795831ree_tv_decl, type, type_M950795831ree_tv: !> [TA: $tType]: (TA > (set @ nat))).
% 121.10/95.44 thf(member_decl, type, member: !> [TA: $tType]: (TA > ((set @ TA) > $o))).
% 121.10/95.44 thf(s1_decl, type, s1: (nat > type_Mirabelle_typ)).
% 121.10/95.44 thf(s2_decl, type, s2: (nat > type_Mirabelle_typ)).
% 121.10/95.44 thf(n_decl, type, n: nat).
% 121.10/95.44 thf(x_decl, type, x: nat).
% 121.10/95.44 thf(135,axiom,((! [A:nat,B:nat]: (((type_Mirabelle_TVar @ A) = (type_Mirabelle_TVar @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_typ_Oinject_I1_J)).
% 121.10/95.44 thf(809,plain,((! [A:nat,B:nat]: (((type_Mirabelle_TVar @ A) = (type_Mirabelle_TVar @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 121.10/95.44 thf(246,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((? [D:TA]: ((member @ TA @ D @ (sup_sup @ (set @ TA) @ A @ B)) & (C @ D))) = (? [D:TA]: ((member @ TA @ D @ A) & (C @ D)) | ? [D:TA]: ((member @ TA @ D @ B) & (C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_bex__Un)).
% 121.10/95.44 thf(1190,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((? [D:TA]: ((member @ TA @ D @ (sup_sup @ (set @ TA) @ A @ B)) & (C @ D))) = (? [D:TA]: ((member @ TA @ D @ A) & (C @ D)) | ? [D:TA]: ((member @ TA @ D @ B) & (C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 121.10/95.44 thf(239,axiom,((preorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Opreorder_5)).
% 121.10/95.44 thf(1168,plain,((preorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 121.10/95.44 thf(258,axiom,((! [TA: $tType]: ((type_M1470978233struct @ TA) => ((type_M1046766514new_tv @ TA) = (^ [A:nat,B:TA]: ! [C:nat]: ((member @ nat @ C @ (type_M950795831ree_tv @ TA @ B)) => (ord_less @ nat @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_new__tv__def)).
% 121.10/95.44 thf(1237,plain,((! [TA: $tType]: ((type_M1470978233struct @ TA) => ((type_M1046766514new_tv @ TA) = (^ [A:nat,B:TA]: ! [C:nat]: ((member @ nat @ C @ (type_M950795831ree_tv @ TA @ B)) => (ord_less @ nat @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 121.10/95.44 thf(76,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (ord_less @ TA @ B @ A)) = (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_antisym__conv3)).
% 121.10/95.44 thf(628,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (ord_less @ TA @ B @ A)) = (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 121.10/95.44 thf(161,axiom,((! [TA: $tType,TB: $tType]: (! [A:((TB > TA) > ((list @ TB) > ((list @ TA) > $o))),B:(TB > TA),C:(list @ TB),D:(list @ TA)]: ((! [E:(TB > TA),F:(list @ TA)]: (A @ E @ (nil @ TB) @ F)) => ((! [E:(TB > TA),F:TB,G:(list @ TB),H:(list @ TA)]: ((A @ E @ G @ (cons @ TA @ (E @ F) @ H)) => (A @ E @ (cons @ TB @ F @ G) @ H))) => (A @ B @ C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_map__tailrec__rev_Oinduct)).
% 121.10/95.44 thf(893,plain,((! [TA: $tType,TB: $tType]: (! [A:((TB > TA) > ((list @ TB) > ((list @ TA) > $o))),B:(TB > TA),C:(list @ TB),D:(list @ TA)]: ((! [E:(TB > TA),F:(list @ TA)]: (A @ (E) @ (nil @ TB) @ F)) => ((! [E:(TB > TA),F:TB,G:(list @ TB),H:(list @ TA)]: ((A @ (E) @ G @ (cons @ TA @ (E @ F) @ H)) => (A @ (E) @ (cons @ TB @ F @ G) @ H))) => (A @ (B) @ C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 121.10/95.44 thf(50,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((A != B) => (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_linorder__cases)).
% 121.10/95.44 thf(518,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (A = B)) => (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 121.10/95.44 thf(128,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((insert2 @ TA @ A @ B) != (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_insert__not__empty)).
% 121.10/95.44 thf(777,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ~ ((insert2 @ TA @ A @ B) = (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 121.10/95.44 thf(38,axiom,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ,C:type_Mirabelle_typ,D:type_Mirabelle_typ]: (((type_Mirabelle_Fun @ A @ B) = (type_Mirabelle_Fun @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_typ_Oinject_I2_J)).
% 121.10/95.44 thf(481,plain,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ,C:type_Mirabelle_typ,D:type_Mirabelle_typ]: (((type_Mirabelle_Fun @ A @ B) = (type_Mirabelle_Fun @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 121.10/95.44 thf(193,axiom,((! [TA: $tType]: (! [A:(list @ TA)]: ((A != (nil @ TA)) = (? [B:TA,C:(list @ TA)]: (A = (cons @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_neq__Nil__conv)).
% 121.10/95.44 thf(1005,plain,((! [TA: $tType]: (! [A:(list @ TA)]: ((~ (A = (nil @ TA))) = (? [B:TA,C:(list @ TA)]: (A = (cons @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 121.10/95.44 thf(276,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o),C:$o,D:(set @ TA)]: (((! [E:TA]: ((member @ TA @ E @ A) => (B @ E))) => (C)) => ((! [E:TA]: ((member @ TA @ E @ (sup_sup @ (set @ TA) @ A @ D)) => (B @ E))) => (C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_weaken__asm__Un)).
% 121.10/95.44 thf(1290,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o),C:$o,D:(set @ TA)]: (((! [E:TA]: ((member @ TA @ E @ A) => (B @ E))) => (C)) => ((! [E:TA]: ((member @ TA @ E @ (sup_sup @ (set @ TA) @ A @ D)) => (B @ E))) => (C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[276])).
% 121.10/95.44 thf(189,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((B = C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_ord__less__eq__trans)).
% 121.10/95.44 thf(994,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((B = C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 121.10/95.44 thf(251,axiom,((! [A:nat]: ((type_M950795831ree_tv @ type_M1610475166scheme @ (type_M1264524676e_BVar @ A)) = (bot_bot @ (set @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_free__tv__type__scheme_Osimps_I2_J)).
% 121.10/95.44 thf(1205,plain,((! [A:nat]: ((type_M950795831ree_tv @ type_M1610475166scheme @ (type_M1264524676e_BVar @ A)) = (bot_bot @ (set @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 121.10/95.44 thf(52,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: (((A @ B) => ((collect @ TA @ (^ [C:TA]: ((B = C) & (A @ C)))) = (insert2 @ TA @ B @ (bot_bot @ (set @ TA))))) & ((~ (A @ B)) => ((collect @ TA @ (^ [C:TA]: ((B = C) & (A @ C)))) = (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_Collect__conv__if2)).
% 121.10/95.44 thf(523,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: (((A @ B) => ((collect @ TA @ (^ [C:TA]: ((B = C) & (A @ C)))) = (insert2 @ TA @ B @ (bot_bot @ (set @ TA))))) & ((~ (A @ B)) => ((collect @ TA @ (^ [C:TA]: ((B = C) & (A @ C)))) = (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 121.10/95.44 thf(61,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_2_1_T)).
% 121.10/95.44 thf(582,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 121.10/95.44 thf(122,axiom,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ((A != (bot_bot @ TA)) = (ord_less @ TA @ (bot_bot @ TA) @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_bot_Onot__eq__extremum)).
% 121.10/95.44 thf(762,plain,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ((~ (A = (bot_bot @ TA))) = (ord_less @ TA @ (bot_bot @ TA) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 121.10/95.44 thf(208,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:TA]: ((A = (bot_bot @ (set @ TA))) => (~ (member @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_equals0D)).
% 121.10/95.44 thf(1078,plain,((! [TA: $tType]: (! [A:(set @ TA),B:TA]: ((A = (bot_bot @ (set @ TA))) => (~ (member @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 121.10/95.44 thf(283,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((A != (bot_bot @ (set @ TA))) => ((! [B:TA,C:TA]: ((member @ TA @ B @ A) => ((member @ TA @ C @ A) => (B = C)))) => (is_singleton @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_is__singletonI_H)).
% 121.10/95.44 thf(1310,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((~ (A = (bot_bot @ (set @ TA)))) => ((! [B:TA,C:TA]: ((member @ TA @ B @ A) => ((member @ TA @ C @ A) => (B = C)))) => (is_singleton @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[283])).
% 121.10/95.44 thf(270,axiom,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (! [A:(nat > type_Mirabelle_typ)]: ((type_M353778473_subst @ (list @ TA) @ A @ (nil @ TA)) = (nil @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_app__subst__Nil)).
% 121.10/95.44 thf(1275,plain,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (! [A:(nat > type_Mirabelle_typ)]: ((type_M353778473_subst @ (list @ TA) @ (A) @ (nil @ TA)) = (nil @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 121.10/95.44 thf(36,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (semilattice_neutr @ TA @ (sup_sup @ TA) @ (bot_bot @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_sup__bot_Osemilattice__neutr__axioms)).
% 121.10/95.44 thf(472,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (semilattice_neutr @ TA @ (sup_sup @ TA) @ (bot_bot @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 121.10/95.44 thf(286,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_UnI1)).
% 121.10/95.44 thf(1327,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[286])).
% 121.10/95.44 thf(118,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_ord__eq__less__subst)).
% 121.10/95.44 thf(747,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 121.10/95.44 thf(7,axiom,((! [TA: $tType]: (! [A:TA]: ((the @ TA @ ((=) @ TA @ A)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_the__sym__eq__trivial)).
% 121.10/95.44 thf(340,plain,((! [TA: $tType]: (! [A:TA]: ((the @ TA @ ((=) @ TA @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 121.10/95.44 thf(256,axiom,((! [A:type_Mirabelle_typ]: ((type_M950795831ree_tv @ type_M1610475166scheme @ (type_M540877363scheme @ A)) = (type_M950795831ree_tv @ type_Mirabelle_typ @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_free__tv__mk__scheme)).
% 121.10/95.44 thf(1222,plain,((! [A:type_Mirabelle_typ]: ((type_M950795831ree_tv @ type_M1610475166scheme @ (type_M540877363scheme @ A)) = (type_M950795831ree_tv @ type_Mirabelle_typ @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 121.10/95.44 thf(248,axiom,((! [TA: $tType]: ((insert2 @ TA) = (^ [A:TA,B:(set @ TA)]: (collect @ TA @ (^ [C:TA]: ((C = A) | (member @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_insert__compr)).
% 121.10/95.44 thf(1196,plain,((! [TA: $tType]: ((insert2 @ TA) = (^ [A:TA,B:(set @ TA)]: (collect @ TA @ (^ [C:TA]: ((C = A) | (member @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 121.10/95.44 thf(260,axiom,((! [A:(nat > type_Mirabelle_typ),B:type_Mirabelle_typ,C:type_Mirabelle_typ]: ((type_M353778473_subst @ type_Mirabelle_typ @ A @ (type_Mirabelle_Fun @ B @ C)) = (type_Mirabelle_Fun @ (type_M353778473_subst @ type_Mirabelle_typ @ A @ B) @ (type_M353778473_subst @ type_Mirabelle_typ @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_app__subst__Fun)).
% 121.10/95.44 thf(1243,plain,((! [A:(nat > type_Mirabelle_typ),B:type_Mirabelle_typ,C:type_Mirabelle_typ]: ((type_M353778473_subst @ type_Mirabelle_typ @ (A) @ (type_Mirabelle_Fun @ B @ C)) = (type_Mirabelle_Fun @ (type_M353778473_subst @ type_Mirabelle_typ @ (A) @ B) @ (type_M353778473_subst @ type_Mirabelle_typ @ (A) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 121.10/95.44 thf(5,axiom,((bounde1808546759up_bot @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Obounded__semilattice__sup__bot_16)).
% 121.10/95.44 thf(320,plain,((bounde1808546759up_bot @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 121.10/95.44 thf(181,axiom,((! [TA: $tType]: (semilattice_sup @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Osemilattice__sup_10)).
% 121.10/95.44 thf(973,plain,((! [TA: $tType]: (semilattice_sup @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 121.10/95.44 thf(159,axiom,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: (((type_M540877363scheme @ A) = (type_M540877363scheme @ B)) => (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_mk__scheme__injective)).
% 121.10/95.44 thf(885,plain,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: (((type_M540877363scheme @ A) = (type_M540877363scheme @ B)) => (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 121.10/95.44 thf(109,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_dual__order_Ostrict__trans)).
% 121.10/95.44 thf(724,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 121.10/95.44 thf(107,axiom,((bounded_lattice @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Obounded__lattice)).
% 121.10/95.44 thf(719,plain,((bounded_lattice @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 121.10/95.44 thf(13,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => ((! [C:TA]: ((A @ C) => (C = B))) => ((the @ TA @ A) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_the__equality)).
% 121.10/95.44 thf(372,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => ((! [C:TA]: ((A @ C) => (C = B))) => ((the @ TA @ (A)) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 121.10/95.44 thf(47,axiom,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (type_M1470978233struct @ (list @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_List_Olist___Type__Mirabelle__sfxnzmapfi_Otype__struct_24)).
% 121.10/95.44 thf(504,plain,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (type_M1470978233struct @ (list @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 121.10/95.44 thf(267,axiom,((! [A:nat]: ((type_M950795831ree_tv @ type_M1610475166scheme @ (type_M91906176e_FVar @ A)) = (insert2 @ nat @ A @ (bot_bot @ (set @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_free__tv__type__scheme_Osimps_I1_J)).
% 121.10/95.44 thf(1264,plain,((! [A:nat]: ((type_M950795831ree_tv @ type_M1610475166scheme @ (type_M91906176e_FVar @ A)) = (insert2 @ nat @ A @ (bot_bot @ (set @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 121.10/95.44 thf(63,axiom,((! [TA: $tType,TB: $tType]: (((type_M201404320of_nat @ TB) & (type_M1535146424typ_of @ TA)) => (type_M1470978233struct @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Type__Mirabelle__sfxnzmapfi_Otype__struct)).
% 121.10/95.44 thf(587,plain,((! [TA: $tType,TB: $tType]: (((type_M201404320of_nat @ TB) & (type_M1535146424typ_of @ TA)) => (type_M1470978233struct @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 121.10/95.44 thf(177,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((bot_bot @ TA) = (sup_sup @ TA @ A @ B)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_sup__bot_Oneutr__eq__iff)).
% 121.10/95.44 thf(949,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((bot_bot @ TA) = (sup_sup @ TA @ A @ B)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 121.10/95.44 thf(201,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ B)) = (B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_mem__Collect__eq)).
% 121.10/95.44 thf(1059,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ (B))) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 121.10/95.44 thf(227,axiom,((! [A:nat,B:type_M1610475166scheme,C:type_M1610475166scheme]: ((type_M1046766514new_tv @ type_M1610475166scheme @ A @ (type_M1518733067e_SFun @ B @ C)) = ((type_M1046766514new_tv @ type_M1610475166scheme @ A @ B) & (type_M1046766514new_tv @ type_M1610475166scheme @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_new__tv__Fun2)).
% 121.10/95.44 thf(1132,plain,((! [A:nat,B:type_M1610475166scheme,C:type_M1610475166scheme]: ((type_M1046766514new_tv @ type_M1610475166scheme @ A @ (type_M1518733067e_SFun @ B @ C)) = ((type_M1046766514new_tv @ type_M1610475166scheme @ A @ B) & (type_M1046766514new_tv @ type_M1610475166scheme @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 121.10/95.44 thf(79,axiom,((! [TA: $tType]: (! [A:(list @ TA)]: ((A != (nil @ TA)) => ((! [B:TA]: (A != (cons @ TA @ B @ (nil @ TA)))) => (~ (! [B:TA,C:TA,D:(list @ TA)]: (A != (cons @ TA @ B @ (cons @ TA @ C @ D)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_remdups__adj_Ocases)).
% 121.10/95.44 thf(638,plain,((! [TA: $tType]: (! [A:(list @ TA)]: ((~ (A = (nil @ TA))) => ((! [B:TA]: ~ (A = (cons @ TA @ B @ (nil @ TA)))) => (~ (! [B:TA,C:TA,D:(list @ TA)]: ~ (A = (cons @ TA @ B @ (cons @ TA @ C @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 121.10/95.44 thf(70,axiom,((! [A:nat,B:type_Mirabelle_typ,C:type_Mirabelle_typ]: ((type_Mirabelle_TVar @ A) != (type_Mirabelle_Fun @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_typ_Odistinct_I1_J)).
% 121.10/95.44 thf(606,plain,((! [A:nat,B:type_Mirabelle_typ,C:type_Mirabelle_typ]: ~ ((type_Mirabelle_TVar @ A) = (type_Mirabelle_Fun @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 121.10/95.44 thf(196,axiom,((! [TA: $tType]: ((the_elem @ TA) = (^ [A:(set @ TA)]: (the @ TA @ (^ [B:TA]: (A = (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_the__elem__def)).
% 121.10/95.44 thf(1013,plain,((! [TA: $tType]: ((the_elem @ TA) = (^ [A:(set @ TA)]: (the @ TA @ (^ [B:TA]: (A = (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 121.10/95.44 thf(125,axiom,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TA) => (semilattice_sup @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Osemilattice__sup)).
% 121.10/95.44 thf(770,plain,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TA) => (semilattice_sup @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 121.10/95.44 thf(172,axiom,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (! [A:nat,B:TA,C:(list @ TA)]: ((type_M1046766514new_tv @ (list @ TA) @ A @ (cons @ TA @ B @ C)) = ((type_M1046766514new_tv @ TA @ A @ B) & (type_M1046766514new_tv @ (list @ TA) @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_new__tv__Cons)).
% 121.10/95.44 thf(924,plain,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (! [A:nat,B:TA,C:(list @ TA)]: ((type_M1046766514new_tv @ (list @ TA) @ A @ (cons @ TA @ B @ C)) = ((type_M1046766514new_tv @ TA @ A @ B) & (type_M1046766514new_tv @ (list @ TA) @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 121.10/95.44 thf(42,axiom,((! [TA: $tType]: (ord @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oord_14)).
% 121.10/95.44 thf(492,plain,((! [TA: $tType]: (ord @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 121.10/95.44 thf(280,axiom,((! [A:nat]: (type_M1046766514new_tv @ (nat > type_Mirabelle_typ) @ A @ type_M17369686_subst))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_new__tv__id__subst)).
% 121.10/95.44 thf(1302,plain,((! [A:nat]: (type_M1046766514new_tv @ (nat > type_Mirabelle_typ) @ A @ (type_M17369686_subst)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[280])).
% 121.10/95.44 thf(132,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ (bot_bot @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_sup__bot_Oright__neutral)).
% 121.10/95.44 thf(789,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ (bot_bot @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 121.10/95.44 thf(6,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => ((! [D:TA]: ((A @ D) => (D = B))) => ((! [D:TA]: ((A @ D) => (C @ D))) => (C @ (the @ TA @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_theI2)).
% 121.10/95.44 thf(321,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => ((! [D:TA]: ((A @ D) => (D = B))) => ((! [D:TA]: ((A @ D) => (C @ D))) => (C @ (the @ TA @ (A))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 121.10/95.44 thf(82,axiom,((! [TA: $tType]: ((is_empty @ TA) = (^ [A:(set @ TA)]: (A = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_Set_Ois__empty__def)).
% 121.10/95.44 thf(646,plain,((! [TA: $tType]: ((is_empty @ TA) = (^ [A:(set @ TA)]: (A = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 121.10/95.44 thf(10,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA)]: (ord_lexordp_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_lexordp__eq__refl)).
% 121.10/95.44 thf(348,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA)]: (ord_lexordp_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 121.10/95.44 thf(134,axiom,((! [TA: $tType]: (! [A:TA,B:(list @ TA)]: ((cons @ TA @ A @ B) != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_not__Cons__self2)).
% 121.10/95.44 thf(806,plain,((! [TA: $tType]: (! [A:TA,B:(list @ TA)]: ~ ((cons @ TA @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 121.10/95.44 thf(152,axiom,((! [TA: $tType]: (! [A:TA]: (is_singleton @ TA @ (insert2 @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_is__singletonI)).
% 121.10/95.44 thf(866,plain,((! [TA: $tType]: (! [A:TA]: (is_singleton @ TA @ (insert2 @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 121.10/95.44 thf(295,axiom,((! [A:nat,B:nat]: ((type_M91906176e_FVar @ A) != (type_M1264524676e_BVar @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_type__scheme_Odistinct_I1_J)).
% 121.10/95.44 thf(1351,plain,((! [A:nat,B:nat]: ~ ((type_M91906176e_FVar @ A) = (type_M1264524676e_BVar @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[295])).
% 121.10/95.44 thf(190,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA)]: (ord_lexordp_eq @ TA @ (nil @ TA) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_lexordp__eq__simps_I1_J)).
% 121.10/95.44 thf(998,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA)]: (ord_lexordp_eq @ TA @ (nil @ TA) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 121.10/95.44 thf(240,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((member @ TA @ A @ (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_singleton__iff)).
% 121.10/95.44 thf(1169,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((member @ TA @ A @ (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 121.10/95.44 thf(18,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA),B:(list @ TA)]: ((ord_lexordp_eq @ TA @ A @ B) => ((ord_lexordp_eq @ TA @ B @ A) => (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_lexordp__eq__antisym)).
% 121.10/95.44 thf(397,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA),B:(list @ TA)]: ((ord_lexordp_eq @ TA @ A @ B) => ((ord_lexordp_eq @ TA @ B @ A) => (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 121.10/95.44 thf(95,axiom,((! [A:type_M1610475166scheme,B:type_M1610475166scheme,C:type_M1610475166scheme,D:type_M1610475166scheme]: (((type_M1518733067e_SFun @ A @ B) = (type_M1518733067e_SFun @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_type__scheme_Oinject_I3_J)).
% 121.10/95.44 thf(687,plain,((! [A:type_M1610475166scheme,B:type_M1610475166scheme,C:type_M1610475166scheme,D:type_M1610475166scheme]: (((type_M1518733067e_SFun @ A @ B) = (type_M1518733067e_SFun @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 121.10/95.44 thf(254,axiom,((! [A:type_M1610475166scheme]: ((! [B:nat]: (A != (type_M91906176e_FVar @ B))) => ((! [B:nat]: (A != (type_M1264524676e_BVar @ B))) => (~ (! [B:type_M1610475166scheme,C:type_M1610475166scheme]: (A != (type_M1518733067e_SFun @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_type__scheme_Oexhaust)).
% 121.10/95.44 thf(1215,plain,((! [A:type_M1610475166scheme]: ((! [B:nat]: ~ (A = (type_M91906176e_FVar @ B))) => ((! [B:nat]: ~ (A = (type_M1264524676e_BVar @ B))) => (~ (! [B:type_M1610475166scheme,C:type_M1610475166scheme]: ~ (A = (type_M1518733067e_SFun @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 121.10/95.44 thf(78,axiom,((! [TA: $tType]: ((dense_order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (? [C:TA]: ((ord_less @ TA @ A @ C) & (ord_less @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_dense)).
% 121.10/95.44 thf(634,plain,((! [TA: $tType]: ((dense_order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (? [C:TA]: ((ord_less @ TA @ A @ C) & (ord_less @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 121.10/95.44 thf(156,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ B @ C)) = (sup_sup @ (set @ TA) @ B @ (sup_sup @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_Un__left__commute)).
% 121.10/95.44 thf(877,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ B @ C)) = (sup_sup @ (set @ TA) @ B @ (sup_sup @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 121.10/95.44 thf(97,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:(list @ TA),D:(list @ TA)]: ((~ (ord_less @ TA @ A @ B)) => ((~ (ord_less @ TA @ B @ A)) => ((ord_lexordp_eq @ TA @ C @ D) => (ord_lexordp_eq @ TA @ (cons @ TA @ A @ C) @ (cons @ TA @ B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_lexordp__eq_OCons__eq)).
% 121.10/95.44 thf(692,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:(list @ TA),D:(list @ TA)]: ((~ (ord_less @ TA @ A @ B)) => ((~ (ord_less @ TA @ B @ A)) => ((ord_lexordp_eq @ TA @ C @ D) => (ord_lexordp_eq @ TA @ (cons @ TA @ A @ C) @ (cons @ TA @ B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 121.10/95.44 thf(206,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((! [D:TA]: ((member @ TA @ D @ (sup_sup @ (set @ TA) @ A @ B)) => (C @ D))) = (! [D:TA]: ((member @ TA @ D @ A) => (C @ D)) & ! [D:TA]: ((member @ TA @ D @ B) => (C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_ball__Un)).
% 121.10/95.44 thf(1072,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((! [D:TA]: ((member @ TA @ D @ (sup_sup @ (set @ TA) @ A @ B)) => (C @ D))) = (! [D:TA]: ((member @ TA @ D @ A) => (C @ D)) & ! [D:TA]: ((member @ TA @ D @ B) => (C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 121.10/95.44 thf(33,axiom,((type_M17369686_subst = type_Mirabelle_TVar)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_id__subst__def)).
% 121.10/95.44 thf(453,plain,(((type_M17369686_subst) = (type_Mirabelle_TVar))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 121.10/95.44 thf(293,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (insert2 @ TA @ B @ C)) = ((A = B) | (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_insert__iff)).
% 121.10/95.44 thf(1345,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (insert2 @ TA @ B @ C)) = ((A = B) | (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[293])).
% 121.10/95.44 thf(187,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:TA,D:TA]: (((insert2 @ TA @ A @ (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))) = (insert2 @ TA @ C @ (insert2 @ TA @ D @ (bot_bot @ (set @ TA))))) = (((A = C) & (B = D)) | ((A = D) & (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_doubleton__eq__iff)).
% 121.10/95.44 thf(988,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:TA,D:TA]: (((insert2 @ TA @ A @ (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))) = (insert2 @ TA @ C @ (insert2 @ TA @ D @ (bot_bot @ (set @ TA))))) = (((A = C) & (B = D)) | ((A = D) & (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 121.10/95.44 thf(3,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A = ((=) @ TA @ B)) => ((the @ TA @ A) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_Nitpick_OThe__psimp)).
% 121.10/95.44 thf(307,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: (((A) = ((=) @ TA @ B)) => ((the @ TA @ (A)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 121.10/95.44 thf(170,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_less__irrefl)).
% 121.10/95.44 thf(920,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 121.10/95.44 thf(91,axiom,((! [TA: $tType]: ((is_singleton @ TA) = (^ [A:(set @ TA)]: (A = (insert2 @ TA @ (the_elem @ TA @ A) @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_is__singleton__the__elem)).
% 121.10/95.44 thf(678,plain,((! [TA: $tType]: ((is_singleton @ TA) = (^ [A:(set @ TA)]: (A = (insert2 @ TA @ (the_elem @ TA @ A) @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 121.10/95.44 thf(53,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_order_Oasym)).
% 121.10/95.44 thf(529,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 121.10/95.44 thf(56,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_ord__less__eq__subst)).
% 121.10/95.44 thf(546,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 121.10/95.44 thf(249,axiom,((! [A:(nat > type_Mirabelle_typ),B:type_Mirabelle_typ]: ((type_M353778473_subst @ type_M1610475166scheme @ A @ (type_M540877363scheme @ B)) = (type_M540877363scheme @ (type_M353778473_subst @ type_Mirabelle_typ @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_subst__mk__scheme)).
% 121.10/95.44 thf(1199,plain,((! [A:(nat > type_Mirabelle_typ),B:type_Mirabelle_typ]: ((type_M353778473_subst @ type_M1610475166scheme @ (A) @ (type_M540877363scheme @ B)) = (type_M540877363scheme @ (type_M353778473_subst @ type_Mirabelle_typ @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 121.10/95.44 thf(291,axiom,((order @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oorder_6)).
% 121.10/95.44 thf(1338,plain,((order @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[291])).
% 121.10/95.44 thf(14,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((? [C:TA]: ((A @ C) & ! [D:TA]: ((A @ D) => (D = C)))) => ((A @ B) = (B = (the @ TA @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_theI__unique)).
% 121.10/95.44 thf(381,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((? [C:TA]: ((A @ C) & ! [D:TA]: ((A @ D) => (D = C)))) => ((A @ B) = (B = (the @ TA @ (A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 121.10/95.44 thf(55,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA),B:(list @ TA),C:((list @ TA) > ((list @ TA) > $o))]: ((ord_lexordp_eq @ TA @ A @ B) => ((! [D:(list @ TA)]: (C @ (nil @ TA) @ D)) => ((! [D:TA,E:TA,F:(list @ TA),G:(list @ TA)]: ((ord_less @ TA @ D @ E) => (C @ (cons @ TA @ D @ F) @ (cons @ TA @ E @ G)))) => ((! [D:TA,E:TA,F:(list @ TA),G:(list @ TA)]: ((~ (ord_less @ TA @ D @ E)) => ((~ (ord_less @ TA @ E @ D)) => ((ord_lexordp_eq @ TA @ F @ G) => ((C @ F @ G) => (C @ (cons @ TA @ D @ F) @ (cons @ TA @ E @ G))))))) => (C @ A @ B))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_lexordp__eq_Oinducts)).
% 121.10/95.44 thf(534,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA),B:(list @ TA),C:((list @ TA) > ((list @ TA) > $o))]: ((ord_lexordp_eq @ TA @ A @ B) => ((! [D:(list @ TA)]: (C @ (nil @ TA) @ D)) => ((! [D:TA,E:TA,F:(list @ TA),G:(list @ TA)]: ((ord_less @ TA @ D @ E) => (C @ (cons @ TA @ D @ F) @ (cons @ TA @ E @ G)))) => ((! [D:TA,E:TA,F:(list @ TA),G:(list @ TA)]: ((~ (ord_less @ TA @ D @ E)) => ((~ (ord_less @ TA @ E @ D)) => ((ord_lexordp_eq @ TA @ F @ G) => ((C @ F @ G) => (C @ (cons @ TA @ D @ F) @ (cons @ TA @ E @ G))))))) => (C @ A @ B))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 121.10/95.44 thf(204,axiom,(((type_M950795831ree_tv @ (nat > type_Mirabelle_typ)) = (^ [A:(nat > type_Mirabelle_typ)]: (sup_sup @ (set @ nat) @ (type_Mirabelle_dom @ A) @ (type_Mirabelle_cod @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_free__tv__subst)).
% 121.10/95.44 thf(1067,plain,(((type_M950795831ree_tv @ (nat > type_Mirabelle_typ)) = (^ [A:(nat > type_Mirabelle_typ)]: (sup_sup @ (set @ nat) @ (type_Mirabelle_dom @ A) @ (type_Mirabelle_cod @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 121.10/95.44 thf(105,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_less__asym_H)).
% 121.10/95.44 thf(714,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 121.10/95.44 thf(213,axiom,((bot @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Obot_8)).
% 121.10/95.44 thf(1091,plain,((bot @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 121.10/95.44 thf(178,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_bot__fun__def)).
% 121.10/95.44 thf(952,plain,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 121.10/95.44 thf(296,axiom,((! [A:nat,B:nat]: ((type_M1046766514new_tv @ type_M1610475166scheme @ A @ (type_M91906176e_FVar @ B)) = (ord_less @ nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_new__tv__FVar)).
% 121.10/95.44 thf(1355,plain,((! [A:nat,B:nat]: ((type_M1046766514new_tv @ type_M1610475166scheme @ A @ (type_M91906176e_FVar @ B)) = (ord_less @ nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[296])).
% 121.10/95.44 thf(264,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:(nat > TA),C:(type_M1610475166scheme > (type_M1610475166scheme > (TA > (TA > TA)))),D:nat]: ((type_M1705333808scheme @ TA @ A @ B @ C @ (type_M91906176e_FVar @ D)) = (A @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_type__scheme_Osimps_I13_J)).
% 121.10/95.44 thf(1255,plain,((! [TA: $tType]: (! [A:(nat > TA),B:(nat > TA),C:(type_M1610475166scheme > (type_M1610475166scheme > (TA > (TA > TA)))),D:nat]: ((type_M1705333808scheme @ TA @ (A) @ (B) @ (C) @ (type_M91906176e_FVar @ D)) = (A @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 121.10/95.44 thf(151,axiom,((! [TA: $tType]: (! [A:((TA > (TA > $o)) > ((list @ TA) > $o)),B:(TA > (TA > $o)),C:(list @ TA)]: ((! [D:(TA > (TA > $o))]: (A @ D @ (nil @ TA))) => ((! [D:(TA > (TA > $o)),E:TA]: (A @ D @ (cons @ TA @ E @ (nil @ TA)))) => ((! [D:(TA > (TA > $o)),E:TA,F:TA,G:(list @ TA)]: ((A @ D @ (cons @ TA @ F @ G)) => (A @ D @ (cons @ TA @ E @ (cons @ TA @ F @ G))))) => (A @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_successively_Oinduct)).
% 121.10/95.44 thf(862,plain,((! [TA: $tType]: (! [A:((TA > (TA > $o)) > ((list @ TA) > $o)),B:(TA > (TA > $o)),C:(list @ TA)]: ((! [D:(TA > (TA > $o))]: (A @ (D) @ (nil @ TA))) => ((! [D:(TA > (TA > $o)),E:TA]: (A @ (D) @ (cons @ TA @ E @ (nil @ TA)))) => ((! [D:(TA > (TA > $o)),E:TA,F:TA,G:(list @ TA)]: ((A @ (D) @ (cons @ TA @ F @ G)) => (A @ (D) @ (cons @ TA @ E @ (cons @ TA @ F @ G))))) => (A @ (B) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 121.10/95.44 thf(242,axiom,((! [A:nat]: ((type_M779184887und_tv @ type_M1610475166scheme @ (type_M91906176e_FVar @ A)) = (bot_bot @ (set @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_bound__tv__type__scheme_Osimps_I1_J)).
% 121.10/95.44 thf(1174,plain,((! [A:nat]: ((type_M779184887und_tv @ type_M1610475166scheme @ (type_M91906176e_FVar @ A)) = (bot_bot @ (set @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 121.10/95.44 thf(67,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((collect @ TA @ A) = (collect @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_Collect__cong)).
% 121.10/95.44 thf(598,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((collect @ TA @ (A)) = (collect @ TA @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 121.10/95.44 thf(16,axiom,((! [TA: $tType,TB: $tType]: ((bounded_lattice @ TA) => (bounded_lattice @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Obounded__lattice_2)).
% 121.10/95.44 thf(392,plain,((! [TA: $tType,TB: $tType]: ((bounded_lattice @ TA) => (bounded_lattice @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 121.10/95.44 thf(23,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:(type_Mirabelle_typ > (type_Mirabelle_typ > TA)),C:nat]: ((type_M1695911984se_typ @ TA @ A @ B @ (type_Mirabelle_TVar @ C)) = (A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_typ_Osimps_I5_J)).
% 121.10/95.44 thf(424,plain,((! [TA: $tType]: (! [A:(nat > TA),B:(type_Mirabelle_typ > (type_Mirabelle_typ > TA)),C:nat]: ((type_M1695911984se_typ @ TA @ (A) @ (B) @ (type_Mirabelle_TVar @ C)) = (A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 121.10/95.44 thf(25,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_bot__apply)).
% 121.10/95.44 thf(429,plain,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 121.10/95.44 thf(137,axiom,((! [A:nat,B:type_M1610475166scheme,C:type_M1610475166scheme]: ((type_M1264524676e_BVar @ A) != (type_M1518733067e_SFun @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_type__scheme_Odistinct_I5_J)).
% 121.10/95.44 thf(815,plain,((! [A:nat,B:type_M1610475166scheme,C:type_M1610475166scheme]: ~ ((type_M1264524676e_BVar @ A) = (type_M1518733067e_SFun @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 121.10/95.44 thf(168,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_Un__absorb)).
% 121.10/95.44 thf(916,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 121.10/95.44 thf(200,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA),B:(list @ TA)]: ((ord_lexordp_eq @ TA @ A @ B) => ((A != (nil @ TA)) => ((! [C:TA]: ((? [D:(list @ TA)]: (A = (cons @ TA @ C @ D))) => (! [D:TA]: ((? [E:(list @ TA)]: (B = (cons @ TA @ D @ E))) => (~ (ord_less @ TA @ C @ D)))))) => (~ (! [C:TA,D:TA,E:(list @ TA)]: ((A = (cons @ TA @ C @ E)) => (! [F:(list @ TA)]: ((B = (cons @ TA @ D @ F)) => ((~ (ord_less @ TA @ C @ D)) => ((~ (ord_less @ TA @ D @ C)) => (~ (ord_lexordp_eq @ TA @ E @ F)))))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_lexordp__eq_Ocases)).
% 121.10/95.44 thf(1027,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA),B:(list @ TA)]: ((ord_lexordp_eq @ TA @ A @ B) => ((~ (A = (nil @ TA))) => ((! [C:TA]: ((? [D:(list @ TA)]: (A = (cons @ TA @ C @ D))) => (! [D:TA]: ((? [E:(list @ TA)]: (B = (cons @ TA @ D @ E))) => (~ (ord_less @ TA @ C @ D)))))) => (~ (! [C:TA,D:TA,E:(list @ TA)]: ((A = (cons @ TA @ C @ E)) => (! [F:(list @ TA)]: ((B = (cons @ TA @ D @ F)) => ((~ (ord_less @ TA @ C @ D)) => ((~ (ord_less @ TA @ D @ C)) => (~ (ord_lexordp_eq @ TA @ E @ F)))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 121.10/95.44 thf(225,axiom,((! [TA: $tType,TB: $tType]: (((type_M201404320of_nat @ TA) & (type_M1535146424typ_of @ TB)) => ((type_M950795831ree_tv @ (TA > TB)) = (^ [A:(TA > TB)]: (sup_sup @ (set @ nat) @ (type_Mirabelle_dom @ (^ [B:nat]: (type_M604437996typ_of @ TB @ (A @ (type_M167561660of_nat @ TA @ B))))) @ (type_Mirabelle_cod @ (^ [B:nat]: (type_M604437996typ_of @ TB @ (A @ (type_M167561660of_nat @ TA @ B))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_free__tv__fun__def)).
% 121.10/95.44 thf(1128,plain,((! [TA: $tType,TB: $tType]: (((type_M201404320of_nat @ TA) & (type_M1535146424typ_of @ TB)) => ((type_M950795831ree_tv @ (TA > TB)) = (^ [A:(TA > TB)]: (sup_sup @ (set @ nat) @ (type_Mirabelle_dom @ (^ [B:nat]: (type_M604437996typ_of @ TB @ (A @ (type_M167561660of_nat @ TA @ B))))) @ (type_Mirabelle_cod @ (^ [B:nat]: (type_M604437996typ_of @ TB @ (A @ (type_M167561660of_nat @ TA @ B))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 121.10/95.44 thf(272,axiom,((ord @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oord_7)).
% 121.10/95.44 thf(1281,plain,((ord @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[272])).
% 121.10/95.44 thf(144,axiom,((! [TA: $tType]: ((insert2 @ TA) = (^ [A:TA]: (sup_sup @ (set @ TA) @ (collect @ TA @ (^ [B:TA]: (B = A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_insert__def)).
% 121.10/95.44 thf(842,plain,((! [TA: $tType]: ((insert2 @ TA) = (^ [A:TA]: (sup_sup @ (set @ TA) @ (collect @ TA @ (^ [B:TA]: (B = A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 121.10/95.44 thf(146,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((insert2 @ TA @ A @ (insert2 @ TA @ B @ C)) = (insert2 @ TA @ B @ (insert2 @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_insert__commute)).
% 121.10/95.44 thf(847,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((insert2 @ TA @ A @ (insert2 @ TA @ B @ C)) = (insert2 @ TA @ B @ (insert2 @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 121.10/95.44 thf(39,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_less__imp__not__eq2)).
% 121.10/95.44 thf(484,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 121.10/95.44 thf(12,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => ((! [C:TA]: ((A @ C) => (C = B))) => (A @ (the @ TA @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_theI)).
% 121.10/95.44 thf(361,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => ((! [C:TA]: ((A @ C) => (C = B))) => (A @ (the @ TA @ (A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 121.10/95.44 thf(299,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_psubsetD)).
% 121.10/95.44 thf(1365,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[299])).
% 121.10/95.44 thf(148,axiom,((! [TA: $tType]: ((is_singleton @ TA) = (^ [A:(set @ TA)]: ? [B:TA]: (A = (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_is__singleton__def)).
% 121.10/95.44 thf(852,plain,((! [TA: $tType]: ((is_singleton @ TA) = (^ [A:(set @ TA)]: ? [B:TA]: (A = (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 121.10/95.44 thf(27,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: (((bot_bot @ (set @ TA)) = (collect @ TA @ A)) = (! [B:TA]: ~ (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_empty__Collect__eq)).
% 121.10/95.44 thf(435,plain,((! [TA: $tType]: (! [A:(TA > $o)]: (((bot_bot @ (set @ TA)) = (collect @ TA @ (A))) = (! [B:TA]: ~ (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 121.10/95.44 thf(277,axiom,((wellorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Owellorder)).
% 121.10/95.44 thf(1296,plain,((wellorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[277])).
% 121.10/95.44 thf(86,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ (bot_bot @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_sup__bot__right)).
% 121.10/95.44 thf(665,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ (bot_bot @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 121.10/95.44 thf(116,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((insert2 @ TA @ A @ (collect @ TA @ B)) = (collect @ TA @ (^ [C:TA]: ((C != A) => (B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_insert__Collect)).
% 121.10/95.44 thf(742,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((insert2 @ TA @ A @ (collect @ TA @ (B))) = (collect @ TA @ (^ [C:TA]: ((~ (C = A)) => (B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 121.10/95.44 thf(99,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:(type_Mirabelle_typ > (type_Mirabelle_typ > TA)),C:type_Mirabelle_typ,D:type_Mirabelle_typ]: ((type_M1695911984se_typ @ TA @ A @ B @ (type_Mirabelle_Fun @ C @ D)) = (B @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_typ_Osimps_I6_J)).
% 121.10/95.44 thf(697,plain,((! [TA: $tType]: (! [A:(nat > TA),B:(type_Mirabelle_typ > (type_Mirabelle_typ > TA)),C:type_Mirabelle_typ,D:type_Mirabelle_typ]: ((type_M1695911984se_typ @ TA @ (A) @ (B) @ (type_Mirabelle_Fun @ C @ D)) = (B @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 121.10/95.44 thf(155,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((B = (sup_sup @ TA @ B @ A)) & (B != A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_sup_Ostrict__order__iff)).
% 121.10/95.44 thf(874,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((B = (sup_sup @ TA @ B @ A)) & ~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 121.10/95.44 thf(216,axiom,((! [A:(nat > type_Mirabelle_typ),B:nat]: ((type_M353778473_subst @ type_M1610475166scheme @ A @ (type_M91906176e_FVar @ B)) = (type_M540877363scheme @ (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_app__subst__type__scheme_Osimps_I1_J)).
% 121.10/95.44 thf(1096,plain,((! [A:(nat > type_Mirabelle_typ),B:nat]: ((type_M353778473_subst @ type_M1610475166scheme @ (A) @ (type_M91906176e_FVar @ B)) = (type_M540877363scheme @ (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 121.10/95.44 thf(229,axiom,((! [A:(list @ type_M1610475166scheme),B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member @ nat @ D @ (type_M950795831ree_tv @ (list @ type_M1610475166scheme) @ A)) => ((B @ D) = (C @ D)))) => ((type_M353778473_subst @ (list @ type_M1610475166scheme) @ B @ A) = (type_M353778473_subst @ (list @ type_M1610475166scheme) @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_eq__free__eq__subst__scheme__list)).
% 121.10/95.44 thf(1138,plain,((! [A:(list @ type_M1610475166scheme),B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member @ nat @ D @ (type_M950795831ree_tv @ (list @ type_M1610475166scheme) @ A)) => ((B @ D) = (C @ D)))) => ((type_M353778473_subst @ (list @ type_M1610475166scheme) @ (B) @ A) = (type_M353778473_subst @ (list @ type_M1610475166scheme) @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 121.10/95.44 thf(71,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_Un__empty__right)).
% 121.10/95.44 thf(610,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 121.10/95.44 thf(130,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((sup_sup @ TA @ A @ B) = (bot_bot @ TA)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_sup__eq__bot__iff)).
% 121.10/95.44 thf(783,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((sup_sup @ TA @ A @ B) = (bot_bot @ TA)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 121.10/95.44 thf(184,axiom,((! [TA: $tType]: (preorder @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Opreorder_12)).
% 121.10/95.44 thf(980,plain,((! [TA: $tType]: (preorder @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 121.10/95.44 thf(21,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA),B:(list @ TA)]: ((ord_lexordp_eq @ TA @ A @ B) | (ord_lexordp_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_lexordp__eq__linear)).
% 121.10/95.44 thf(403,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA),B:(list @ TA)]: ((ord_lexordp_eq @ TA @ A @ B) | (ord_lexordp_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 121.10/95.44 thf(35,axiom,((ord @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oord_22)).
% 121.10/95.44 thf(471,plain,((ord @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 121.10/95.44 thf(287,axiom,((! [A:nat,B:nat]: (type_M1046766514new_tv @ type_M1610475166scheme @ A @ (type_M1264524676e_BVar @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_new__tv__BVar)).
% 121.10/95.44 thf(1329,plain,((! [A:nat,B:nat]: (type_M1046766514new_tv @ type_M1610475166scheme @ A @ (type_M1264524676e_BVar @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[287])).
% 121.10/95.44 thf(209,axiom,(((type_Mirabelle_dom @ type_M17369686_subst) = (bot_bot @ (set @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_dom__id__subst)).
% 121.10/95.44 thf(1082,plain,(((type_Mirabelle_dom @ (type_M17369686_subst)) = (bot_bot @ (set @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 121.10/95.44 thf(40,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_order_Ostrict__trans)).
% 121.10/95.44 thf(488,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 121.10/95.44 thf(174,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:((list @ TA) > $o),B:(list @ TA)]: ((! [C:TA,D:(list @ TA)]: ((! [E:TA,F:(list @ TA)]: ((D = (cons @ TA @ E @ F)) => (A @ D))) => (A @ (cons @ TA @ C @ D)))) => ((A @ (nil @ TA)) => (A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_min__list_Oinduct)).
% 121.10/95.44 thf(933,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:((list @ TA) > $o),B:(list @ TA)]: ((! [C:TA,D:(list @ TA)]: ((! [E:TA,F:(list @ TA)]: ((D = (cons @ TA @ E @ F)) => (A @ D))) => (A @ (cons @ TA @ C @ D)))) => ((A @ (nil @ TA)) => (A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 121.10/95.44 thf(57,axiom,((! [TA: $tType]: (! [A:TA,B:(list @ TA)]: ((nil @ TA) != (cons @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_list_Odistinct_I1_J)).
% 121.10/95.44 thf(554,plain,((! [TA: $tType]: (! [A:TA,B:(list @ TA)]: ~ ((nil @ TA) = (cons @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 121.10/95.44 thf(88,axiom,((! [TA: $tType]: (bounded_lattice @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Obounded__lattice_1)).
% 121.10/95.44 thf(669,plain,((! [TA: $tType]: (bounded_lattice @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 121.10/95.44 thf(197,axiom,((! [TA: $tType,TB: $tType]: ((order_bot @ TA) => (order_bot @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder__bot)).
% 121.10/95.44 thf(1016,plain,((! [TA: $tType,TB: $tType]: ((order_bot @ TA) => (order_bot @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 121.10/95.44 thf(234,axiom,((! [A:nat]: (type_M1046766514new_tv @ (nat > type_Mirabelle_typ) @ A @ type_Mirabelle_TVar))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_new__tv__TVar__subst)).
% 121.10/95.44 thf(1155,plain,((! [A:nat]: (type_M1046766514new_tv @ (nat > type_Mirabelle_typ) @ A @ (type_Mirabelle_TVar)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 121.10/95.44 thf(102,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => ((ord_less @ (set @ TA) @ B @ C) => (ord_less @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_psubset__trans)).
% 121.10/95.44 thf(706,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => ((ord_less @ (set @ TA) @ B @ C) => (ord_less @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 121.10/95.44 thf(94,axiom,((preorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Opreorder_19)).
% 121.10/95.44 thf(686,plain,((preorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 121.10/95.44 thf(207,axiom,((! [A:nat]: ((type_M950795831ree_tv @ type_Mirabelle_typ @ (type_Mirabelle_TVar @ A)) = (insert2 @ nat @ A @ (bot_bot @ (set @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_free__tv__TVar)).
% 121.10/95.44 thf(1075,plain,((! [A:nat]: ((type_M950795831ree_tv @ type_Mirabelle_typ @ (type_Mirabelle_TVar @ A)) = (insert2 @ nat @ A @ (bot_bot @ (set @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 121.10/95.44 thf(262,axiom,((! [TA: $tType]: ((ord_less @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (ord_less @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_less__set__def)).
% 121.10/95.44 thf(1249,plain,((! [TA: $tType]: ((ord_less @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (ord_less @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 121.10/95.44 thf(278,axiom,(((type_M950795831ree_tv @ (nat > type_Mirabelle_typ) @ type_M17369686_subst) = (bot_bot @ (set @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_free__tv__id__subst)).
% 121.10/95.44 thf(1297,plain,(((type_M950795831ree_tv @ (nat > type_Mirabelle_typ) @ (type_M17369686_subst)) = (bot_bot @ (set @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 121.10/95.44 thf(226,axiom,((order_bot @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oorder__bot_4)).
% 121.10/95.44 thf(1131,plain,((order_bot @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 121.10/95.44 thf(261,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)) = ((member @ TA @ A @ B) | (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_Un__iff)).
% 121.10/95.44 thf(1246,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)) = ((member @ TA @ A @ B) | (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 121.10/95.44 thf(217,axiom,((type_Mirabelle_dom = (^ [A:(nat > type_Mirabelle_typ)]: (collect @ nat @ (^ [B:nat]: ((A @ B) != (type_Mirabelle_TVar @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_Type__Mirabelle__sfxnzmapfi_Odom__def)).
% 121.10/95.44 thf(1099,plain,(((type_Mirabelle_dom) = (^ [A:(nat > type_Mirabelle_typ)]: (collect @ nat @ (^ [B:nat]: ~ ((A @ B) = (type_Mirabelle_TVar @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 121.10/95.44 thf(186,axiom,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (^ [A:TA]: (($false))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_empty__def)).
% 121.10/95.44 thf(985,plain,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (^ [A:TA]: (($false))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 121.10/95.44 thf(49,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:((list @ TA) > $o),B:(list @ TA)]: ((A @ (nil @ TA)) => ((! [C:TA,D:(list @ TA)]: ((A @ D) => (A @ (cons @ TA @ C @ D)))) => (A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_strict__sorted_Oinduct)).
% 121.10/95.44 thf(508,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:((list @ TA) > $o),B:(list @ TA)]: ((A @ (nil @ TA)) => ((! [C:TA,D:(list @ TA)]: ((A @ D) => (A @ (cons @ TA @ C @ D)))) => (A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 121.10/95.44 thf(4,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((? [C:TA]: ((A @ C) & ! [D:TA]: ((A @ D) => (D = C)))) => ((A @ B) => ((the @ TA @ A) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_162_the1__equality)).
% 121.10/95.44 thf(311,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((? [C:TA]: ((A @ C) & ! [D:TA]: ((A @ D) => (D = C)))) => ((A @ B) => ((the @ TA @ (A)) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 121.10/95.44 thf(123,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ (bot_bot @ TA) @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_sup__bot_Oleft__neutral)).
% 121.10/95.44 thf(765,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ (bot_bot @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 121.10/95.44 thf(8,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(nat > TB),C:(type_Mirabelle_typ > (type_Mirabelle_typ > TB)),D:type_Mirabelle_typ]: ((A @ (type_M1695911984se_typ @ TB @ B @ C @ D)) = (type_M1695911984se_typ @ TA @ (^ [E:nat]: (A @ (B @ E))) @ (^ [E:type_Mirabelle_typ,F:type_Mirabelle_typ]: (A @ (C @ E @ F))) @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_typ_Ocase__distrib)).
% 121.10/95.44 thf(343,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(nat > TB),C:(type_Mirabelle_typ > (type_Mirabelle_typ > TB)),D:type_Mirabelle_typ]: ((A @ (type_M1695911984se_typ @ TB @ (B) @ (C) @ D)) = (type_M1695911984se_typ @ TA @ (^ [E:nat]: (A @ (B @ E))) @ (^ [E:type_Mirabelle_typ,F:type_Mirabelle_typ]: (A @ (C @ E @ F))) @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 121.10/95.44 thf(284,axiom,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (collect @ TA @ (sup_sup @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_sup__set__def)).
% 121.10/95.44 thf(1318,plain,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (collect @ TA @ (sup_sup @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[284])).
% 121.10/95.44 thf(250,axiom,((! [A:(nat > type_Mirabelle_typ),B:nat]: ((type_M353778473_subst @ type_M1610475166scheme @ A @ (type_M1264524676e_BVar @ B)) = (type_M1264524676e_BVar @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_app__subst__type__scheme_Osimps_I2_J)).
% 121.10/95.44 thf(1202,plain,((! [A:(nat > type_Mirabelle_typ),B:nat]: ((type_M353778473_subst @ type_M1610475166scheme @ (A) @ (type_M1264524676e_BVar @ B)) = (type_M1264524676e_BVar @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 121.10/95.44 thf(133,axiom,((! [TA: $tType]: (! [A:((list @ TA) > $o),B:(list @ TA)]: ((A @ (nil @ TA)) => ((! [C:TA]: (A @ (cons @ TA @ C @ (nil @ TA)))) => ((! [C:TA,D:TA,E:(list @ TA)]: ((A @ E) => ((A @ (cons @ TA @ D @ E)) => (A @ (cons @ TA @ C @ (cons @ TA @ D @ E)))))) => (A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_induct__list012)).
% 121.10/95.44 thf(792,plain,((! [TA: $tType]: (! [A:((list @ TA) > $o),B:(list @ TA)]: ((A @ (nil @ TA)) => ((! [C:TA]: (A @ (cons @ TA @ C @ (nil @ TA)))) => ((! [C:TA,D:TA,E:(list @ TA)]: ((A @ E) => ((A @ (cons @ TA @ D @ E)) => (A @ (cons @ TA @ C @ (cons @ TA @ D @ E)))))) => (A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 121.10/95.44 thf(165,axiom,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ (bot_bot @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_bot_Oextremum__strict)).
% 121.10/95.44 thf(906,plain,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ (bot_bot @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 121.10/95.44 thf(271,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) => (A = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_equals0I)).
% 121.10/95.44 thf(1278,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) => (A = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 121.10/95.44 thf(228,axiom,((! [TA: $tType]: ((type_M1470978233struct @ TA) => ((type_M950795831ree_tv @ (list @ TA) @ (nil @ TA)) = (bot_bot @ (set @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_free__tv__list_Osimps_I1_J)).
% 121.10/95.44 thf(1135,plain,((! [TA: $tType]: ((type_M1470978233struct @ TA) => ((type_M950795831ree_tv @ (list @ TA) @ (nil @ TA)) = (bot_bot @ (set @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 121.10/95.44 thf(231,axiom,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (! [A:(nat > type_Mirabelle_typ),B:TA,C:(list @ TA)]: ((type_M353778473_subst @ (list @ TA) @ A @ (cons @ TA @ B @ C)) = (cons @ TA @ (type_M353778473_subst @ TA @ A @ B) @ (type_M353778473_subst @ (list @ TA) @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_app__subst__Cons)).
% 121.10/95.44 thf(1146,plain,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (! [A:(nat > type_Mirabelle_typ),B:TA,C:(list @ TA)]: ((type_M353778473_subst @ (list @ TA) @ (A) @ (cons @ TA @ B @ C)) = (cons @ TA @ (type_M353778473_subst @ TA @ (A) @ B) @ (type_M353778473_subst @ (list @ TA) @ (A) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 121.10/95.44 thf(255,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))) = (^ [C:TA]: (member @ TA @ C @ (sup_sup @ (set @ TA) @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_sup__Un__eq)).
% 121.10/95.44 thf(1219,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))) = (^ [C:TA]: (member @ TA @ C @ (sup_sup @ (set @ TA) @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 121.10/95.44 thf(117,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_dual__order_Oasym)).
% 121.10/95.44 thf(745,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 121.10/95.44 thf(30,axiom,((! [TA: $tType]: (! [A:TA]: ((insert @ TA @ A @ (nil @ TA)) = (cons @ TA @ A @ (nil @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_254_insert__Nil)).
% 121.10/95.44 thf(444,plain,((! [TA: $tType]: (! [A:TA]: ((insert @ TA @ A @ (nil @ TA)) = (cons @ TA @ A @ (nil @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 121.10/95.44 thf(68,axiom,((! [A:nat,B:type_Mirabelle_typ,C:type_Mirabelle_typ]: ((type_M1046766514new_tv @ type_Mirabelle_typ @ A @ (type_Mirabelle_Fun @ B @ C)) = ((type_M1046766514new_tv @ type_Mirabelle_typ @ A @ B) & (type_M1046766514new_tv @ type_Mirabelle_typ @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_new__tv__Fun)).
% 121.10/95.44 thf(601,plain,((! [A:nat,B:type_Mirabelle_typ,C:type_Mirabelle_typ]: ((type_M1046766514new_tv @ type_Mirabelle_typ @ A @ (type_Mirabelle_Fun @ B @ C)) = ((type_M1046766514new_tv @ type_Mirabelle_typ @ A @ B) & (type_M1046766514new_tv @ type_Mirabelle_typ @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 121.10/95.44 thf(138,axiom,((! [A:nat,B:nat]: (((type_M1264524676e_BVar @ A) = (type_M1264524676e_BVar @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_type__scheme_Oinject_I2_J)).
% 121.10/95.44 thf(819,plain,((! [A:nat,B:nat]: (((type_M1264524676e_BVar @ A) = (type_M1264524676e_BVar @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 121.10/95.44 thf(182,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((bot_bot @ TA) = (sup_sup @ TA @ A @ B)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_bot__eq__sup__iff)).
% 121.10/95.44 thf(975,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((bot_bot @ TA) = (sup_sup @ TA @ A @ B)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 121.10/95.44 thf(98,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(nat > TB),C:(nat > TB),D:(type_M1610475166scheme > (type_M1610475166scheme > TB)),E:type_M1610475166scheme]: ((A @ (type_M697345518scheme @ TB @ B @ C @ D @ E)) = (type_M697345518scheme @ TA @ (^ [F:nat]: (A @ (B @ F))) @ (^ [F:nat]: (A @ (C @ F))) @ (^ [F:type_M1610475166scheme,G:type_M1610475166scheme]: (A @ (D @ F @ G))) @ E))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_type__scheme_Ocase__distrib)).
% 121.10/95.44 thf(694,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(nat > TB),C:(nat > TB),D:(type_M1610475166scheme > (type_M1610475166scheme > TB)),E:type_M1610475166scheme]: ((A @ (type_M697345518scheme @ TB @ (B) @ (C) @ (D) @ E)) = (type_M697345518scheme @ TA @ (^ [F:nat]: (A @ (B @ F))) @ (^ [F:nat]: (A @ (C @ F))) @ (^ [F:type_M1610475166scheme,G:type_M1610475166scheme]: (A @ (D @ F @ G))) @ E))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 121.10/95.44 thf(20,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_T)).
% 121.10/95.44 thf(402,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 121.10/95.44 thf(112,axiom,((! [TA: $tType]: (! [A:TA]: ((the_elem @ TA @ (insert2 @ TA @ A @ (bot_bot @ (set @ TA)))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_the__elem__eq)).
% 121.10/95.44 thf(732,plain,((! [TA: $tType]: (! [A:TA]: ((the_elem @ TA @ (insert2 @ TA @ A @ (bot_bot @ (set @ TA)))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 121.10/95.44 thf(126,axiom,((! [TA: $tType,TB: $tType]: (! [A:((list @ TB) > ((list @ TA) > $o)),B:(list @ TB),C:(list @ TA)]: ((A @ (nil @ TB) @ (nil @ TA)) => ((! [D:TB,E:(list @ TB)]: (A @ (cons @ TB @ D @ E) @ (nil @ TA))) => ((! [D:TA,E:(list @ TA)]: (A @ (nil @ TB) @ (cons @ TA @ D @ E))) => ((! [D:TB,E:(list @ TB),F:TA,G:(list @ TA)]: ((A @ E @ G) => (A @ (cons @ TB @ D @ E) @ (cons @ TA @ F @ G)))) => (A @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_list__induct2_H)).
% 121.10/95.44 thf(772,plain,((! [TA: $tType,TB: $tType]: (! [A:((list @ TB) > ((list @ TA) > $o)),B:(list @ TB),C:(list @ TA)]: ((A @ (nil @ TB) @ (nil @ TA)) => ((! [D:TB,E:(list @ TB)]: (A @ (cons @ TB @ D @ E) @ (nil @ TA))) => ((! [D:TA,E:(list @ TA)]: (A @ (nil @ TB) @ (cons @ TA @ D @ E))) => ((! [D:TB,E:(list @ TB),F:TA,G:(list @ TA)]: ((A @ E @ G) => (A @ (cons @ TB @ D @ E) @ (cons @ TA @ F @ G)))) => (A @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 121.10/95.44 thf(104,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:(nat > TA),C:(type_M1610475166scheme > (type_M1610475166scheme > (TA > (TA > TA)))),D:type_M1610475166scheme,E:type_M1610475166scheme]: ((type_M1705333808scheme @ TA @ A @ B @ C @ (type_M1518733067e_SFun @ D @ E)) = (C @ D @ E @ (type_M1705333808scheme @ TA @ A @ B @ C @ D) @ (type_M1705333808scheme @ TA @ A @ B @ C @ E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_type__scheme_Osimps_I15_J)).
% 121.10/95.44 thf(711,plain,((! [TA: $tType]: (! [A:(nat > TA),B:(nat > TA),C:(type_M1610475166scheme > (type_M1610475166scheme > (TA > (TA > TA)))),D:type_M1610475166scheme,E:type_M1610475166scheme]: ((type_M1705333808scheme @ TA @ (A) @ (B) @ (C) @ (type_M1518733067e_SFun @ D @ E)) = (C @ D @ E @ (type_M1705333808scheme @ TA @ (A) @ (B) @ (C) @ D) @ (type_M1705333808scheme @ TA @ (A) @ (B) @ (C) @ E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 121.10/95.44 thf(60,axiom,((! [TA: $tType]: ((insert2 @ TA) = (^ [A:TA]: (sup_sup @ (set @ TA) @ (insert2 @ TA @ A @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_insert__is__Un)).
% 121.10/95.44 thf(579,plain,((! [TA: $tType]: ((insert2 @ TA) = (^ [A:TA]: (sup_sup @ (set @ TA) @ (insert2 @ TA @ A @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 121.10/95.44 thf(80,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((is_singleton @ TA @ A) => (~ (! [B:TA]: (A != (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_is__singletonE)).
% 121.10/95.44 thf(641,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((is_singleton @ TA @ A) => (~ (! [B:TA]: ~ (A = (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 121.10/95.44 thf(44,axiom,((! [TA: $tType]: (! [A:TA,B:(list @ TA),C:TA,D:(list @ TA)]: (((cons @ TA @ A @ B) = (cons @ TA @ C @ D)) = ((A = C) & (B = D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_list_Oinject)).
% 121.10/95.44 thf(498,plain,((! [TA: $tType]: (! [A:TA,B:(list @ TA),C:TA,D:(list @ TA)]: (((cons @ TA @ A @ B) = (cons @ TA @ C @ D)) = ((A = C) & (B = D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 121.10/95.44 thf(219,axiom,((! [A:type_M1610475166scheme,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member @ nat @ D @ (type_M950795831ree_tv @ type_M1610475166scheme @ A)) => ((B @ D) = (C @ D)))) => ((type_M353778473_subst @ type_M1610475166scheme @ B @ A) = (type_M353778473_subst @ type_M1610475166scheme @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_scheme__substitutions__only__on__free__variables)).
% 121.10/95.44 thf(1107,plain,((! [A:type_M1610475166scheme,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member @ nat @ D @ (type_M950795831ree_tv @ type_M1610475166scheme @ A)) => ((B @ D) = (C @ D)))) => ((type_M353778473_subst @ type_M1610475166scheme @ (B) @ A) = (type_M353778473_subst @ type_M1610475166scheme @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 121.10/95.44 thf(289,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (insert2 @ TA @ B @ C)) => ((A != B) => (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_insertE)).
% 121.10/95.44 thf(1332,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (insert2 @ TA @ B @ C)) => ((~ (A = B)) => (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[289])).
% 121.10/95.44 thf(214,axiom,((semilattice_sup @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Lattices_Osemilattice__sup_3)).
% 121.10/95.44 thf(1092,plain,((semilattice_sup @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 121.10/95.44 thf(212,axiom,((type_M1470978233struct @ type_M1610475166scheme)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Type__Mirabelle__sfxnzmapfi_Otype__scheme___Type__Mirabelle__sfxnzmapfi_Otype__struct_26)).
% 121.10/95.44 thf(1090,plain,((type_M1470978233struct @ type_M1610475166scheme)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 121.10/95.44 thf(169,axiom,((type_M1470978233struct @ type_Mirabelle_typ)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Type__Mirabelle__sfxnzmapfi_Otyp___Type__Mirabelle__sfxnzmapfi_Otype__struct_25)).
% 121.10/95.44 thf(919,plain,((type_M1470978233struct @ type_Mirabelle_typ)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 121.10/95.44 thf(265,axiom,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (! [A:TA,B:(list @ TA)]: ((type_M950795831ree_tv @ (list @ TA) @ (cons @ TA @ A @ B)) = (sup_sup @ (set @ nat) @ (type_M950795831ree_tv @ TA @ A) @ (type_M950795831ree_tv @ (list @ TA) @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_free__tv__list_Osimps_I2_J)).
% 121.10/95.44 thf(1258,plain,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (! [A:TA,B:(list @ TA)]: ((type_M950795831ree_tv @ (list @ TA) @ (cons @ TA @ A @ B)) = (sup_sup @ (set @ nat) @ (type_M950795831ree_tv @ TA @ A) @ (type_M950795831ree_tv @ (list @ TA) @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[265])).
% 121.10/95.44 thf(176,axiom,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Opreorder)).
% 121.10/95.44 thf(947,plain,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 121.10/95.44 thf(11,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: ((? [B:TA]: ((A @ B) & ! [C:TA]: ((A @ C) => (C = B)))) => (A @ (the @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_theI_H)).
% 121.10/95.44 thf(350,plain,((! [TA: $tType]: (! [A:(TA > $o)]: ((? [B:TA]: ((A @ B) & ! [C:TA]: ((A @ C) => (C = B)))) => (A @ (the @ TA @ (A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 121.10/95.44 thf(69,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:(list @ TA),D:(list @ TA)]: ((ord_less @ TA @ A @ B) => (ord_lexordp_eq @ TA @ (cons @ TA @ A @ C) @ (cons @ TA @ B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_lexordp__eq_OCons)).
% 121.10/95.44 thf(604,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:(list @ TA),D:(list @ TA)]: ((ord_less @ TA @ A @ B) => (ord_lexordp_eq @ TA @ (cons @ TA @ A @ C) @ (cons @ TA @ B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 121.10/95.44 thf(163,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B) | (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_less__linear)).
% 121.10/95.44 thf(900,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B) | (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 121.10/95.44 thf(92,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: (((sup_sup @ (set @ TA) @ A @ B) = (insert2 @ TA @ C @ (bot_bot @ (set @ TA)))) = (((A = (bot_bot @ (set @ TA))) & (B = (insert2 @ TA @ C @ (bot_bot @ (set @ TA))))) | ((A = (insert2 @ TA @ C @ (bot_bot @ (set @ TA)))) & (B = (bot_bot @ (set @ TA)))) | ((A = (insert2 @ TA @ C @ (bot_bot @ (set @ TA)))) & (B = (insert2 @ TA @ C @ (bot_bot @ (set @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_Un__singleton__iff)).
% 121.10/95.44 thf(681,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: (((sup_sup @ (set @ TA) @ A @ B) = (insert2 @ TA @ C @ (bot_bot @ (set @ TA)))) = (((A = (bot_bot @ (set @ TA))) & (B = (insert2 @ TA @ C @ (bot_bot @ (set @ TA))))) | ((A = (insert2 @ TA @ C @ (bot_bot @ (set @ TA)))) & (B = (bot_bot @ (set @ TA)))) | ((A = (insert2 @ TA @ C @ (bot_bot @ (set @ TA)))) & (B = (insert2 @ TA @ C @ (bot_bot @ (set @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 121.10/95.44 thf(273,axiom,((! [A:nat,B:nat]: (((type_M91906176e_FVar @ A) = (type_M91906176e_FVar @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_type__scheme_Oinject_I1_J)).
% 121.10/95.44 thf(1282,plain,((! [A:nat,B:nat]: (((type_M91906176e_FVar @ A) = (type_M91906176e_FVar @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[273])).
% 121.10/95.44 thf(221,axiom,((! [TA: $tType]: ((bot_bot @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_164_bot__empty__eq)).
% 121.10/95.44 thf(1117,plain,((! [TA: $tType]: ((bot_bot @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 121.10/95.44 thf(195,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_less__not__sym)).
% 121.10/95.44 thf(1011,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 121.10/95.44 thf(32,axiom,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (! [A:nat]: (type_M1046766514new_tv @ (list @ TA) @ A @ (nil @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_new__tv__Nil)).
% 121.10/95.44 thf(451,plain,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (! [A:nat]: (type_M1046766514new_tv @ (list @ TA) @ A @ (nil @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 121.10/95.44 thf(230,axiom,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_emptyE)).
% 121.10/95.44 thf(1144,plain,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 121.10/95.44 thf(114,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_sup_Ostrict__coboundedI1)).
% 121.10/95.44 thf(737,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 121.10/95.44 thf(223,axiom,((! [A:nat,B:type_M1610475166scheme,C:type_M1610475166scheme]: ((type_M91906176e_FVar @ A) != (type_M1518733067e_SFun @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_type__scheme_Odistinct_I3_J)).
% 121.10/95.44 thf(1122,plain,((! [A:nat,B:type_M1610475166scheme,C:type_M1610475166scheme]: ~ ((type_M91906176e_FVar @ A) = (type_M1518733067e_SFun @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 121.10/95.44 thf(282,axiom,((! [A:(nat > type_Mirabelle_typ),B:nat]: ((type_M353778473_subst @ type_Mirabelle_typ @ A @ (type_Mirabelle_TVar @ B)) = (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_app__subst__TVar)).
% 121.10/95.44 thf(1307,plain,((! [A:(nat > type_Mirabelle_typ),B:nat]: ((type_M353778473_subst @ type_Mirabelle_typ @ (A) @ (type_Mirabelle_TVar @ B)) = (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 121.10/95.44 thf(157,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:(list @ TA),C:TA,D:(list @ TA)]: ((ord_lexordp_eq @ TA @ (cons @ TA @ A @ B) @ (cons @ TA @ C @ D)) = ((ord_less @ TA @ A @ C) | (~ (ord_less @ TA @ C @ A) & (ord_lexordp_eq @ TA @ B @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_lexordp__eq__simps_I4_J)).
% 121.10/95.44 thf(880,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:(list @ TA),C:TA,D:(list @ TA)]: ((ord_lexordp_eq @ TA @ (cons @ TA @ A @ B) @ (cons @ TA @ C @ D)) = ((ord_less @ TA @ A @ C) | (~ (ord_less @ TA @ C @ A) & (ord_lexordp_eq @ TA @ B @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 121.10/95.44 thf(83,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((insert2 @ TA @ A @ (bot_bot @ (set @ TA))) = (sup_sup @ (set @ TA) @ B @ C)) = (((B = (bot_bot @ (set @ TA))) & (C = (insert2 @ TA @ A @ (bot_bot @ (set @ TA))))) | ((B = (insert2 @ TA @ A @ (bot_bot @ (set @ TA)))) & (C = (bot_bot @ (set @ TA)))) | ((B = (insert2 @ TA @ A @ (bot_bot @ (set @ TA)))) & (C = (insert2 @ TA @ A @ (bot_bot @ (set @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_singleton__Un__iff)).
% 121.10/95.44 thf(649,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((insert2 @ TA @ A @ (bot_bot @ (set @ TA))) = (sup_sup @ (set @ TA) @ B @ C)) = (((B = (bot_bot @ (set @ TA))) & (C = (insert2 @ TA @ A @ (bot_bot @ (set @ TA))))) | ((B = (insert2 @ TA @ A @ (bot_bot @ (set @ TA)))) & (C = (bot_bot @ (set @ TA)))) | ((B = (insert2 @ TA @ A @ (bot_bot @ (set @ TA)))) & (C = (insert2 @ TA @ A @ (bot_bot @ (set @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 121.10/95.44 thf(160,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:(nat > TA),C:(type_M1610475166scheme > (type_M1610475166scheme > (TA > (TA > TA)))),D:nat]: ((type_M1705333808scheme @ TA @ A @ B @ C @ (type_M1264524676e_BVar @ D)) = (B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_type__scheme_Osimps_I14_J)).
% 121.10/95.44 thf(890,plain,((! [TA: $tType]: (! [A:(nat > TA),B:(nat > TA),C:(type_M1610475166scheme > (type_M1610475166scheme > (TA > (TA > TA)))),D:nat]: ((type_M1705333808scheme @ TA @ (A) @ (B) @ (C) @ (type_M1264524676e_BVar @ D)) = (B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 121.10/95.44 thf(43,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_dual__order_Ostrict__implies__not__eq)).
% 121.10/95.44 thf(494,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 121.10/95.44 thf(77,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_Un__empty__left)).
% 121.10/95.44 thf(631,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 121.10/95.44 thf(150,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_order__less__subst2)).
% 121.10/95.44 thf(858,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 121.10/95.44 thf(100,axiom,((! [TA: $tType]: (! [A:(list @ TA)]: ((A != (nil @ TA)) => (~ (! [B:TA,C:(list @ TA)]: (A != (cons @ TA @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_list_Oexhaust)).
% 121.10/95.44 thf(700,plain,((! [TA: $tType]: (! [A:(list @ TA)]: ((~ (A = (nil @ TA))) => (~ (! [B:TA,C:(list @ TA)]: ~ (A = (cons @ TA @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 121.10/95.44 thf(232,axiom,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (! [A:TA,B:(list @ TA)]: ((type_M779184887und_tv @ (list @ TA) @ (cons @ TA @ A @ B)) = (sup_sup @ (set @ nat) @ (type_M779184887und_tv @ TA @ A) @ (type_M779184887und_tv @ (list @ TA) @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_bound__tv__list_Osimps_I2_J)).
% 121.10/95.44 thf(1149,plain,((! [TA: $tType]: ((type_M1470978233struct @ TA) => (! [A:TA,B:(list @ TA)]: ((type_M779184887und_tv @ (list @ TA) @ (cons @ TA @ A @ B)) = (sup_sup @ (set @ nat) @ (type_M779184887und_tv @ TA @ A) @ (type_M779184887und_tv @ (list @ TA) @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 121.10/95.44 thf(75,axiom,((! [TA: $tType]: (order @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oorder_13)).
% 121.10/95.44 thf(626,plain,((! [TA: $tType]: (order @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 121.10/95.44 thf(175,axiom,((! [TA: $tType]: (! [A:((TA > (TA > $o)) > ((list @ TA) > $o)),B:(TA > (TA > $o)),C:(list @ TA)]: ((! [D:(TA > (TA > $o))]: (A @ D @ (nil @ TA))) => ((! [D:(TA > (TA > $o)),E:TA,F:(list @ TA)]: ((A @ D @ F) => (A @ D @ (cons @ TA @ E @ F)))) => (A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_sorted__wrt_Oinduct)).
% 121.10/95.44 thf(943,plain,((! [TA: $tType]: (! [A:((TA > (TA > $o)) > ((list @ TA) > $o)),B:(TA > (TA > $o)),C:(list @ TA)]: ((! [D:(TA > (TA > $o))]: (A @ (D) @ (nil @ TA))) => ((! [D:(TA > (TA > $o)),E:TA,F:(list @ TA)]: ((A @ (D) @ F) => (A @ (D) @ (cons @ TA @ E @ F)))) => (A @ (B) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 121.10/95.44 thf(87,axiom,((order_bot @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder__bot_18)).
% 121.10/95.44 thf(668,plain,((order_bot @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 121.10/95.44 thf(243,axiom,((! [A:nat,B:(list @ type_M1610475166scheme),C:(nat > type_Mirabelle_typ),D:(nat > type_Mirabelle_typ)]: ((type_M1046766514new_tv @ (list @ type_M1610475166scheme) @ A @ B) => ((type_M353778473_subst @ (list @ type_M1610475166scheme) @ (^ [E:nat]: (if @ type_Mirabelle_typ @ (ord_less @ nat @ E @ A) @ (C @ E) @ (D @ E))) @ B) = (type_M353778473_subst @ (list @ type_M1610475166scheme) @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_new__if__subst__type__scheme__list)).
% 121.10/95.44 thf(1177,plain,((! [A:nat,B:(list @ type_M1610475166scheme),C:(nat > type_Mirabelle_typ),D:(nat > type_Mirabelle_typ)]: ((type_M1046766514new_tv @ (list @ type_M1610475166scheme) @ A @ B) => ((type_M353778473_subst @ (list @ type_M1610475166scheme) @ (^ [E:nat]: (if @ type_Mirabelle_typ @ (ord_less @ nat @ E @ A) @ (C @ E) @ (D @ E))) @ B) = (type_M353778473_subst @ (list @ type_M1610475166scheme) @ (C) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 121.10/95.44 thf(120,axiom,((type_M1535146424typ_of @ type_Mirabelle_typ)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Type__Mirabelle__sfxnzmapfi_Otyp___Type__Mirabelle__sfxnzmapfi_Otyp__of)).
% 121.10/95.44 thf(758,plain,((type_M1535146424typ_of @ type_Mirabelle_typ)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 121.10/95.44 thf(292,axiom,((! [A:(list @ type_M1610475166scheme),B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member @ nat @ D @ (type_M950795831ree_tv @ (list @ type_M1610475166scheme) @ A)) => ((B @ D) = (C @ D)))) => ((type_M353778473_subst @ (list @ type_M1610475166scheme) @ B @ A) = (type_M353778473_subst @ (list @ type_M1610475166scheme) @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_scheme__list__substitutions__only__on__free__variables)).
% 121.10/95.44 thf(1339,plain,((! [A:(list @ type_M1610475166scheme),B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member @ nat @ D @ (type_M950795831ree_tv @ (list @ type_M1610475166scheme) @ A)) => ((B @ D) = (C @ D)))) => ((type_M353778473_subst @ (list @ type_M1610475166scheme) @ (B) @ A) = (type_M353778473_subst @ (list @ type_M1610475166scheme) @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[292])).
% 121.10/95.44 thf(237,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:(nat > TA),C:(type_M1610475166scheme > (type_M1610475166scheme > TA)),D:nat]: ((type_M697345518scheme @ TA @ A @ B @ C @ (type_M91906176e_FVar @ D)) = (A @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_type__scheme_Osimps_I10_J)).
% 121.10/95.44 thf(1162,plain,((! [TA: $tType]: (! [A:(nat > TA),B:(nat > TA),C:(type_M1610475166scheme > (type_M1610475166scheme > TA)),D:nat]: ((type_M697345518scheme @ TA @ (A) @ (B) @ (C) @ (type_M91906176e_FVar @ D)) = (A @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 121.10/95.44 thf(110,axiom,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_lt__ex)).
% 121.10/95.44 thf(726,plain,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 121.10/95.44 thf(180,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:((list @ TA) > $o)]: ((A != (nil @ TA)) => ((! [C:TA]: (B @ (cons @ TA @ C @ (nil @ TA)))) => ((! [C:TA,D:(list @ TA)]: ((D != (nil @ TA)) => ((B @ D) => (B @ (cons @ TA @ C @ D))))) => (B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_list__nonempty__induct)).
% 121.10/95.44 thf(959,plain,((! [TA: $tType]: (! [A:(list @ TA),B:((list @ TA) > $o)]: ((~ (A = (nil @ TA))) => ((! [C:TA]: (B @ (cons @ TA @ C @ (nil @ TA)))) => ((! [C:TA,D:(list @ TA)]: ((~ (D = (nil @ TA))) => ((B @ D) => (B @ (cons @ TA @ C @ D))))) => (B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 121.10/95.44 thf(153,axiom,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (sup_sup @ (set @ TA) @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_Un__commute)).
% 121.10/95.44 thf(868,plain,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (sup_sup @ (set @ TA) @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 121.10/95.44 thf(129,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: (((sup_sup @ (set @ TA) @ A @ B) = (bot_bot @ (set @ TA))) = ((A = (bot_bot @ (set @ TA))) & (B = (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_Un__empty)).
% 121.10/95.44 thf(780,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: (((sup_sup @ (set @ TA) @ A @ B) = (bot_bot @ (set @ TA))) = ((A = (bot_bot @ (set @ TA))) & (B = (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 121.10/95.44 thf(17,axiom,((! [TA: $tType]: (! [A:TA]: ((the @ TA @ (^ [B:TA]: (B = A))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_the__eq__trivial)).
% 121.10/95.44 thf(394,plain,((! [TA: $tType]: (! [A:TA]: ((the @ TA @ (^ [B:TA]: (B = A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 121.10/95.44 thf(220,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((~ (member @ TA @ A @ B)) => (member @ TA @ A @ C)) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_UnCI)).
% 121.10/95.44 thf(1113,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((~ (member @ TA @ A @ B)) => (member @ TA @ A @ C)) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 121.10/95.44 thf(191,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ (insert2 @ TA @ A @ B) @ C) = (insert2 @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_Un__insert__left)).
% 121.10/95.44 thf(1000,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ (insert2 @ TA @ A @ B) @ C) = (insert2 @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 121.10/95.44 thf(298,axiom,((no_top @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Ono__top)).
% 121.10/95.44 thf(1364,plain,((no_top @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[298])).
% 121.10/95.44 thf(28,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:(nat > TA),C:(type_M1610475166scheme > (type_M1610475166scheme > TA)),D:type_M1610475166scheme,E:type_M1610475166scheme]: ((type_M697345518scheme @ TA @ A @ B @ C @ (type_M1518733067e_SFun @ D @ E)) = (C @ D @ E))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_type__scheme_Osimps_I12_J)).
% 121.10/95.44 thf(438,plain,((! [TA: $tType]: (! [A:(nat > TA),B:(nat > TA),C:(type_M1610475166scheme > (type_M1610475166scheme > TA)),D:type_M1610475166scheme,E:type_M1610475166scheme]: ((type_M697345518scheme @ TA @ (A) @ (B) @ (C) @ (type_M1518733067e_SFun @ D @ E)) = (C @ D @ E))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 121.10/95.44 thf(171,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:(list @ TA)]: ~ (ord_lexordp_eq @ TA @ (cons @ TA @ A @ B) @ (nil @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_lexordp__eq__simps_I3_J)).
% 121.10/95.44 thf(922,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:(list @ TA)]: ~ (ord_lexordp_eq @ TA @ (cons @ TA @ A @ B) @ (nil @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 121.10/95.44 thf(167,axiom,((! [TA: $tType,TB: $tType]: ((linorder @ TB) => (! [A:((TA > TB) > ((list @ TA) > $o)),B:(TA > TB),C:(list @ TA)]: ((! [D:(TA > TB),E:TA]: (A @ D @ (cons @ TA @ E @ (nil @ TA)))) => ((! [D:(TA > TB),E:TA,F:TA,G:(list @ TA)]: ((A @ D @ (cons @ TA @ F @ G)) => (A @ D @ (cons @ TA @ E @ (cons @ TA @ F @ G))))) => ((! [D:(TA > TB)]: (A @ D @ (nil @ TA))) => (A @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_arg__min__list_Oinduct)).
% 121.10/95.44 thf(912,plain,((! [TA: $tType,TB: $tType]: ((linorder @ TB) => (! [A:((TA > TB) > ((list @ TA) > $o)),B:(TA > TB),C:(list @ TA)]: ((! [D:(TA > TB),E:TA]: (A @ (D) @ (cons @ TA @ E @ (nil @ TA)))) => ((! [D:(TA > TB),E:TA,F:TA,G:(list @ TA)]: ((A @ (D) @ (cons @ TA @ F @ G)) => (A @ (D) @ (cons @ TA @ E @ (cons @ TA @ F @ G))))) => ((! [D:(TA > TB)]: (A @ (D) @ (nil @ TA))) => (A @ (B) @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 121.10/95.44 thf(51,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:$o]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ A) => (C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_less__imp__triv)).
% 121.10/95.44 thf(521,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:$o]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ A) => (C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 121.10/95.44 thf(253,axiom,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_empty__iff)).
% 121.10/95.44 thf(1213,plain,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 121.10/95.44 thf(124,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oord)).
% 121.10/95.44 thf(768,plain,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 121.10/95.44 thf(34,axiom,((! [TA: $tType]: (! [A:((list @ TA) > $o),B:(list @ TA)]: ((A @ (nil @ TA)) => ((! [C:TA]: (A @ (cons @ TA @ C @ (nil @ TA)))) => ((! [C:TA,D:TA,E:(list @ TA)]: (((C = D) => (A @ (cons @ TA @ C @ E))) => (((C != D) => (A @ (cons @ TA @ D @ E))) => (A @ (cons @ TA @ C @ (cons @ TA @ D @ E)))))) => (A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_remdups__adj_Oinduct)).
% 121.10/95.44 thf(455,plain,((! [TA: $tType]: (! [A:((list @ TA) > $o),B:(list @ TA)]: ((A @ (nil @ TA)) => ((! [C:TA]: (A @ (cons @ TA @ C @ (nil @ TA)))) => ((! [C:TA,D:TA,E:(list @ TA)]: (((C = D) => (A @ (cons @ TA @ C @ E))) => (((~ (C = D)) => (A @ (cons @ TA @ D @ E))) => (A @ (cons @ TA @ C @ (cons @ TA @ D @ E)))))) => (A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 121.10/95.44 thf(158,axiom,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder)).
% 121.10/95.44 thf(883,plain,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 121.10/95.44 thf(281,axiom,((! [A:nat]: ((type_M779184887und_tv @ type_M1610475166scheme @ (type_M1264524676e_BVar @ A)) = (insert2 @ nat @ A @ (bot_bot @ (set @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_bound__tv__type__scheme_Osimps_I2_J)).
% 121.10/95.44 thf(1304,plain,((! [A:nat]: ((type_M779184887und_tv @ type_M1610475166scheme @ (type_M1264524676e_BVar @ A)) = (insert2 @ nat @ A @ (bot_bot @ (set @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[281])).
% 121.10/95.44 thf(54,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ (sup_sup @ (set @ TA) @ A @ B) @ C) = (sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_Un__assoc)).
% 121.10/95.44 thf(531,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ (sup_sup @ (set @ TA) @ A @ B) @ C) = (sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 121.10/95.44 thf(173,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: (((A @ B) => ((collect @ TA @ (^ [C:TA]: ((C = B) & (A @ C)))) = (insert2 @ TA @ B @ (bot_bot @ (set @ TA))))) & ((~ (A @ B)) => ((collect @ TA @ (^ [C:TA]: ((C = B) & (A @ C)))) = (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_Collect__conv__if)).
% 121.10/95.44 thf(927,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: (((A @ B) => ((collect @ TA @ (^ [C:TA]: ((C = B) & (A @ C)))) = (insert2 @ TA @ B @ (bot_bot @ (set @ TA))))) & ((~ (A @ B)) => ((collect @ TA @ (^ [C:TA]: ((C = B) & (A @ C)))) = (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 121.10/95.44 thf(136,axiom,((! [TA: $tType]: ((if @ TA) = (^ [A:$o,B:TA,C:TA]: (the @ TA @ (^ [D:TA]: (((A) => (D = B)) & ((~ (A)) => (D = C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_If__def)).
% 121.10/95.44 thf(812,plain,((! [TA: $tType]: ((if @ TA) = (^ [A:$o,B:TA,C:TA]: (the @ TA @ (^ [D:TA]: (((A) => (D = B)) & ((~ (A)) => (D = C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 121.10/95.44 thf(73,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA)]: ((ord_lexordp_eq @ TA @ A @ (nil @ TA)) = (A = (nil @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_lexordp__eq__simps_I2_J)).
% 121.10/95.44 thf(617,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA)]: ((ord_lexordp_eq @ TA @ A @ (nil @ TA)) = (A = (nil @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 121.10/95.44 thf(198,axiom,((! [TA: $tType]: (! [A:((list @ TA) > ((list @ TA) > $o)),B:(list @ TA),C:(list @ TA)]: ((! [D:(list @ TA)]: (A @ (nil @ TA) @ D)) => ((! [D:(list @ TA)]: (A @ D @ (nil @ TA))) => ((! [D:TA,E:(list @ TA),F:TA,G:(list @ TA)]: ((A @ E @ (cons @ TA @ F @ G)) => ((A @ (cons @ TA @ D @ E) @ G) => (A @ (cons @ TA @ D @ E) @ (cons @ TA @ F @ G))))) => (A @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_shuffles_Oinduct)).
% 121.10/95.44 thf(1018,plain,((! [TA: $tType]: (! [A:((list @ TA) > ((list @ TA) > $o)),B:(list @ TA),C:(list @ TA)]: ((! [D:(list @ TA)]: (A @ (nil @ TA) @ D)) => ((! [D:(list @ TA)]: (A @ D @ (nil @ TA))) => ((! [D:TA,E:(list @ TA),F:TA,G:(list @ TA)]: ((A @ E @ (cons @ TA @ F @ G)) => ((A @ (cons @ TA @ D @ E) @ G) => (A @ (cons @ TA @ D @ E) @ (cons @ TA @ F @ G))))) => (A @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 121.10/95.44 thf(142,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A != B) => ((~ (ord_less @ TA @ A @ B)) => (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_neqE)).
% 121.10/95.44 thf(836,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) => ((~ (ord_less @ TA @ A @ B)) => (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 121.10/95.44 thf(41,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_less__supI1)).
% 121.10/95.44 thf(490,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 121.10/95.44 thf(90,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A != B) = ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_neq__iff)).
% 121.10/95.44 thf(675,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) = ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 121.10/95.44 thf(252,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => (? [C:(set @ TA)]: ((B = (insert2 @ TA @ A @ C)) & ~ (member @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_mk__disjoint__insert)).
% 121.10/95.44 thf(1208,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => (? [C:(set @ TA)]: ((B = (insert2 @ TA @ A @ C)) & ~ (member @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 121.10/95.44 thf(64,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA)]: ((! [B:TA,C:(list @ TA)]: (A != (cons @ TA @ B @ C))) => (A = (nil @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_min__list_Ocases)).
% 121.10/95.44 thf(589,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA)]: ((! [B:TA,C:(list @ TA)]: ~ (A = (cons @ TA @ B @ C))) => (A = (nil @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 121.10/95.44 thf(244,axiom,((! [A:nat,B:nat]: ((type_M1046766514new_tv @ type_Mirabelle_typ @ A @ (type_Mirabelle_TVar @ B)) = (ord_less @ nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_new__tv__TVar)).
% 121.10/95.44 thf(1181,plain,((! [A:nat,B:nat]: ((type_M1046766514new_tv @ type_Mirabelle_typ @ A @ (type_Mirabelle_TVar @ B)) = (ord_less @ nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 121.10/95.44 thf(140,axiom,((! [TA: $tType]: (! [A:((list @ TA) > $o),B:(list @ TA)]: ((A @ (nil @ TA)) => ((! [C:TA,D:(list @ TA)]: ((A @ D) => (A @ (cons @ TA @ C @ D)))) => (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_list_Oinducts)).
% 121.10/95.44 thf(823,plain,((! [TA: $tType]: (! [A:((list @ TA) > $o),B:(list @ TA)]: ((A @ (nil @ TA)) => ((! [C:TA,D:(list @ TA)]: ((A @ D) => (A @ (cons @ TA @ C @ D)))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 121.10/95.44 thf(127,axiom,((linorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Olinorder_20)).
% 121.10/95.44 thf(776,plain,((linorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 121.10/95.44 thf(149,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ (bot_bot @ TA) @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_sup__bot__left)).
% 121.10/95.44 thf(855,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ (bot_bot @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 121.10/95.44 thf(96,axiom,((! [TA: $tType]: (bot @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Obot_15)).
% 121.10/95.44 thf(690,plain,((! [TA: $tType]: (bot @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 121.10/95.44 thf(257,axiom,((! [A:(type_M1610475166scheme > $o),B:type_M1610475166scheme]: ((! [C:nat]: (A @ (type_M91906176e_FVar @ C))) => ((! [C:nat]: (A @ (type_M1264524676e_BVar @ C))) => ((! [C:type_M1610475166scheme,D:type_M1610475166scheme]: ((A @ C) => ((A @ D) => (A @ (type_M1518733067e_SFun @ C @ D))))) => (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_type__scheme_Oinduct)).
% 121.10/95.44 thf(1225,plain,((! [A:(type_M1610475166scheme > $o),B:type_M1610475166scheme]: ((! [C:nat]: (A @ (type_M91906176e_FVar @ C))) => ((! [C:nat]: (A @ (type_M1264524676e_BVar @ C))) => ((! [C:type_M1610475166scheme,D:type_M1610475166scheme]: ((A @ C) => ((A @ D) => (A @ (type_M1518733067e_SFun @ C @ D))))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 121.10/95.44 thf(263,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => ((insert2 @ TA @ A @ B) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_insert__absorb)).
% 121.10/95.44 thf(1252,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => ((insert2 @ TA @ A @ B) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 121.10/95.44 thf(115,axiom,((! [TA: $tType]: (! [A:TA]: ((collect @ TA @ (^ [B:TA]: (B = A))) = (insert2 @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_singleton__conv)).
% 121.10/95.44 thf(739,plain,((! [TA: $tType]: (! [A:TA]: ((collect @ TA @ (^ [B:TA]: (B = A))) = (insert2 @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 121.10/95.44 thf(268,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => (~ (! [C:(set @ TA)]: ((B = (insert2 @ TA @ A @ C)) => (member @ TA @ A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_Set_Oset__insert)).
% 121.10/95.44 thf(1267,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => (~ (! [C:(set @ TA)]: ((B = (insert2 @ TA @ A @ C)) => (member @ TA @ A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 121.10/95.44 thf(58,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA]: (A @ D @ D)) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_linorder__less__wlog)).
% 121.10/95.44 thf(557,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA]: (A @ D @ D)) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 121.10/95.44 thf(192,axiom,((! [TA: $tType]: (order_bot @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oorder__bot_11)).
% 121.10/95.44 thf(1003,plain,((! [TA: $tType]: (order_bot @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 121.10/95.44 thf(29,axiom,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (bot_bot @ (TA > $o)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_bot__set__def)).
% 121.10/95.44 thf(441,plain,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (bot_bot @ (TA > $o)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 121.10/95.44 thf(62,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ~ (ord_less @ (set @ TA) @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_not__psubset__empty)).
% 121.10/95.44 thf(585,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ~ (ord_less @ (set @ TA) @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 121.10/95.44 thf(46,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_less__trans)).
% 121.10/95.44 thf(502,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 121.10/95.44 thf(274,axiom,((! [A:nat]: ((type_M540877363scheme @ (type_Mirabelle_TVar @ A)) = (type_M91906176e_FVar @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_mk__scheme_Osimps_I1_J)).
% 121.10/95.44 thf(1285,plain,((! [A:nat]: ((type_M540877363scheme @ (type_Mirabelle_TVar @ A)) = (type_M91906176e_FVar @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 121.10/95.44 thf(297,axiom,((! [A:type_Mirabelle_typ,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member @ nat @ D @ (type_M950795831ree_tv @ type_Mirabelle_typ @ A)) => ((B @ D) = (C @ D)))) => ((type_M353778473_subst @ type_Mirabelle_typ @ B @ A) = (type_M353778473_subst @ type_Mirabelle_typ @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_typ__substitutions__only__on__free__variables)).
% 121.10/95.44 thf(1358,plain,((! [A:type_Mirabelle_typ,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member @ nat @ D @ (type_M950795831ree_tv @ type_Mirabelle_typ @ A)) => ((B @ D) = (C @ D)))) => ((type_M353778473_subst @ type_Mirabelle_typ @ (B) @ A) = (type_M353778473_subst @ type_Mirabelle_typ @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[297])).
% 121.10/95.44 thf(101,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: (((insert2 @ TA @ A @ (bot_bot @ (set @ TA))) = (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_singleton__inject)).
% 121.10/95.44 thf(703,plain,((! [TA: $tType]: (! [A:TA,B:TA]: (((insert2 @ TA @ A @ (bot_bot @ (set @ TA))) = (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 121.10/95.44 thf(199,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_less__imp__not__eq)).
% 121.10/95.44 thf(1023,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 121.10/95.44 thf(72,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_less__imp__neq)).
% 121.10/95.44 thf(613,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 121.10/95.44 thf(183,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA)]: (ord_lexordp_eq @ TA @ (nil @ TA) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_lexordp__eq_ONil)).
% 121.10/95.44 thf(978,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:(list @ TA)]: (ord_lexordp_eq @ TA @ (nil @ TA) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 121.10/95.44 thf(194,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_1_1_T)).
% 121.10/95.44 thf(1008,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 121.10/95.44 thf(66,axiom,((! [TA: $tType]: (! [A:TA]: ((collect @ TA @ ((=) @ TA @ A)) = (insert2 @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_singleton__conv2)).
% 121.10/95.44 thf(595,plain,((! [TA: $tType]: (! [A:TA]: ((collect @ TA @ ((=) @ TA @ A)) = (insert2 @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 121.10/95.44 thf(269,axiom,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) | (member @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_Un__def)).
% 121.10/95.44 thf(1272,plain,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) | (member @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 121.10/95.44 thf(259,axiom,((! [A:type_M1610475166scheme,B:type_M1610475166scheme]: ((type_M950795831ree_tv @ type_M1610475166scheme @ (type_M1518733067e_SFun @ A @ B)) = (sup_sup @ (set @ nat) @ (type_M950795831ree_tv @ type_M1610475166scheme @ A) @ (type_M950795831ree_tv @ type_M1610475166scheme @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_free__tv__type__scheme_Osimps_I3_J)).
% 121.10/95.44 thf(1240,plain,((! [A:type_M1610475166scheme,B:type_M1610475166scheme]: ((type_M950795831ree_tv @ type_M1610475166scheme @ (type_M1518733067e_SFun @ A @ B)) = (sup_sup @ (set @ nat) @ (type_M950795831ree_tv @ type_M1610475166scheme @ A) @ (type_M950795831ree_tv @ type_M1610475166scheme @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 121.10/95.44 thf(188,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((sup_sup @ TA @ A @ B) = (bot_bot @ TA)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_sup__bot_Oeq__neutr__iff)).
% 121.10/95.44 thf(991,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((sup_sup @ TA @ A @ B) = (bot_bot @ TA)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 121.10/95.44 thf(145,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TA) => (bot @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Obot)).
% 121.10/95.44 thf(845,plain,((! [TA: $tType,TB: $tType]: ((bot @ TA) => (bot @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 121.10/95.44 thf(210,axiom,((! [A:nat,B:type_M1610475166scheme,C:(nat > type_Mirabelle_typ),D:(nat > type_Mirabelle_typ)]: ((type_M1046766514new_tv @ type_M1610475166scheme @ A @ B) => ((type_M353778473_subst @ type_M1610475166scheme @ (^ [E:nat]: (if @ type_Mirabelle_typ @ (ord_less @ nat @ E @ A) @ (C @ E) @ (D @ E))) @ B) = (type_M353778473_subst @ type_M1610475166scheme @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_new__if__subst__type__scheme)).
% 121.10/95.44 thf(1084,plain,((! [A:nat,B:type_M1610475166scheme,C:(nat > type_Mirabelle_typ),D:(nat > type_Mirabelle_typ)]: ((type_M1046766514new_tv @ type_M1610475166scheme @ A @ B) => ((type_M353778473_subst @ type_M1610475166scheme @ (^ [E:nat]: (if @ type_Mirabelle_typ @ (ord_less @ nat @ E @ A) @ (C @ E) @ (D @ E))) @ B) = (type_M353778473_subst @ type_M1610475166scheme @ (C) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 121.10/95.44 thf(89,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_ord__eq__less__trans)).
% 121.10/95.44 thf(671,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 121.10/95.44 thf(164,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((collect @ TA @ (^ [C:TA]: ((A @ C) | (B @ C)))) = (sup_sup @ (set @ TA) @ (collect @ TA @ A) @ (collect @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_Collect__disj__eq)).
% 121.10/95.44 thf(903,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((collect @ TA @ (^ [C:TA]: ((A @ C) | (B @ C)))) = (sup_sup @ (set @ TA) @ (collect @ TA @ (A)) @ (collect @ TA @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 121.10/95.44 thf(121,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = ((ord_less @ TA @ B @ A) | (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_not__less__iff__gr__or__eq)).
% 121.10/95.44 thf(759,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = ((ord_less @ TA @ B @ A) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 121.10/95.44 thf(224,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)) => ((~ (member @ TA @ A @ B)) => (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_UnE)).
% 121.10/95.44 thf(1126,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)) => ((~ (member @ TA @ A @ B)) => (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 121.10/95.44 thf(235,axiom,((! [A:(nat > type_Mirabelle_typ),B:type_Mirabelle_typ,C:(nat > type_Mirabelle_typ),D:nat]: (((type_M353778473_subst @ type_Mirabelle_typ @ A @ B) = (type_M353778473_subst @ type_Mirabelle_typ @ C @ B)) => ((member @ nat @ D @ (type_M950795831ree_tv @ type_Mirabelle_typ @ B)) => ((A @ D) = (C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_eq__subst__te__eq__free)).
% 121.10/95.44 thf(1157,plain,((! [A:(nat > type_Mirabelle_typ),B:type_Mirabelle_typ,C:(nat > type_Mirabelle_typ),D:nat]: (((type_M353778473_subst @ type_Mirabelle_typ @ (A) @ B) = (type_M353778473_subst @ type_Mirabelle_typ @ (C) @ B)) => ((member @ nat @ D @ (type_M950795831ree_tv @ type_Mirabelle_typ @ B)) => ((A @ D) = (C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 121.10/95.44 thf(285,axiom,((! [A:type_M1610475166scheme,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member @ nat @ D @ (type_M950795831ree_tv @ type_M1610475166scheme @ A)) => ((B @ D) = (C @ D)))) => ((type_M353778473_subst @ type_M1610475166scheme @ B @ A) = (type_M353778473_subst @ type_M1610475166scheme @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_eq__free__eq__subst__type__scheme)).
% 121.10/95.44 thf(1321,plain,((! [A:type_M1610475166scheme,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member @ nat @ D @ (type_M950795831ree_tv @ type_M1610475166scheme @ A)) => ((B @ D) = (C @ D)))) => ((type_M353778473_subst @ type_M1610475166scheme @ (B) @ A) = (type_M353778473_subst @ type_M1610475166scheme @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[285])).
% 121.10/95.44 thf(202,axiom,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: ((type_M950795831ree_tv @ type_Mirabelle_typ @ (type_Mirabelle_Fun @ A @ B)) = (sup_sup @ (set @ nat) @ (type_M950795831ree_tv @ type_Mirabelle_typ @ A) @ (type_M950795831ree_tv @ type_Mirabelle_typ @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_free__tv__Fun)).
% 121.10/95.44 thf(1062,plain,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: ((type_M950795831ree_tv @ type_Mirabelle_typ @ (type_Mirabelle_Fun @ A @ B)) = (sup_sup @ (set @ nat) @ (type_M950795831ree_tv @ type_Mirabelle_typ @ A) @ (type_M950795831ree_tv @ type_Mirabelle_typ @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 121.10/95.44 thf(218,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: (((~ (member @ TA @ A @ B)) => (A = C)) => (member @ TA @ A @ (insert2 @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_insertCI)).
% 121.10/95.44 thf(1101,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: (((~ (member @ TA @ A @ B)) => (A = C)) => (member @ TA @ A @ (insert2 @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 121.10/95.44 thf(84,axiom,((! [A:(type_Mirabelle_typ > $o),B:type_Mirabelle_typ]: ((! [C:nat]: (A @ (type_Mirabelle_TVar @ C))) => ((! [C:type_Mirabelle_typ,D:type_Mirabelle_typ]: ((A @ C) => ((A @ D) => (A @ (type_Mirabelle_Fun @ C @ D))))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_typ_Oinduct)).
% 121.10/95.44 thf(652,plain,((! [A:(type_Mirabelle_typ > $o),B:type_Mirabelle_typ]: ((! [C:nat]: (A @ (type_Mirabelle_TVar @ C))) => ((! [C:type_Mirabelle_typ,D:type_Mirabelle_typ]: ((A @ C) => ((A @ D) => (A @ (type_Mirabelle_Fun @ C @ D))))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 121.10/95.44 thf(15,axiom,((! [TA: $tType]: (bounde1808546759up_bot @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Obounded__semilattice__sup__bot_9)).
% 121.10/95.44 thf(390,plain,((! [TA: $tType]: (bounde1808546759up_bot @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 121.10/95.44 thf(131,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ A @ B)) = (sup_sup @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_Un__left__absorb)).
% 121.10/95.44 thf(786,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ A @ B)) = (sup_sup @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 121.10/95.44 thf(247,axiom,((! [A:(nat > type_Mirabelle_typ),B:type_M1610475166scheme,C:type_M1610475166scheme]: ((type_M353778473_subst @ type_M1610475166scheme @ A @ (type_M1518733067e_SFun @ B @ C)) = (type_M1518733067e_SFun @ (type_M353778473_subst @ type_M1610475166scheme @ A @ B) @ (type_M353778473_subst @ type_M1610475166scheme @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_app__subst__type__scheme_Osimps_I3_J)).
% 121.10/95.44 thf(1193,plain,((! [A:(nat > type_Mirabelle_typ),B:type_M1610475166scheme,C:type_M1610475166scheme]: ((type_M353778473_subst @ type_M1610475166scheme @ (A) @ (type_M1518733067e_SFun @ B @ C)) = (type_M1518733067e_SFun @ (type_M353778473_subst @ type_M1610475166scheme @ (A) @ B) @ (type_M353778473_subst @ type_M1610475166scheme @ (A) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 121.10/95.44 thf(93,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_dual__order_Oirrefl)).
% 121.10/95.44 thf(684,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 121.10/95.44 thf(9,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA),B:(list @ TA),C:(list @ TA)]: ((ord_lexordp_eq @ TA @ A @ B) => ((ord_lexordp_eq @ TA @ B @ C) => (ord_lexordp_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_lexordp__eq__trans)).
% 121.10/95.44 thf(346,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA),B:(list @ TA),C:(list @ TA)]: ((ord_lexordp_eq @ TA @ A @ B) => ((ord_lexordp_eq @ TA @ B @ C) => (ord_lexordp_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 121.10/95.44 thf(106,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA)]: ((A != (nil @ TA)) => (~ (! [B:TA,C:(list @ TA)]: (A != (cons @ TA @ B @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_strict__sorted_Ocases)).
% 121.10/95.44 thf(716,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA)]: ((~ (A = (nil @ TA))) => (~ (! [B:TA,C:(list @ TA)]: ~ (A = (cons @ TA @ B @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 121.10/95.44 thf(236,axiom,((linorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Olinorder)).
% 121.10/95.44 thf(1161,plain,((linorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 121.10/95.44 thf(74,axiom,((! [TA: $tType]: ((wellorder @ TA) => (! [A:(TA > $o),B:TA]: ((! [C:TA]: ((! [D:TA]: ((ord_less @ TA @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_less__induct)).
% 121.10/95.44 thf(620,plain,((! [TA: $tType]: ((wellorder @ TA) => (! [A:(TA > $o),B:TA]: ((! [C:TA]: ((! [D:TA]: ((ord_less @ TA @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 121.10/95.44 thf(31,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_order__less__subst1)).
% 121.10/95.44 thf(447,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 121.10/95.44 thf(26,axiom,((! [TA: $tType]: (! [A:(list @ (list @ TA))]: ((A != (nil @ (list @ TA))) => ((! [B:(list @ (list @ TA))]: (A != (cons @ (list @ TA) @ (nil @ TA) @ B))) => (~ (! [B:TA,C:(list @ TA),D:(list @ (list @ TA))]: (A != (cons @ (list @ TA) @ (cons @ TA @ B @ C) @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_transpose_Ocases)).
% 121.10/95.44 thf(432,plain,((! [TA: $tType]: (! [A:(list @ (list @ TA))]: ((~ (A = (nil @ (list @ TA)))) => ((! [B:(list @ (list @ TA))]: ~ (A = (cons @ (list @ TA) @ (nil @ TA) @ B))) => (~ (! [B:TA,C:(list @ TA),D:(list @ (list @ TA))]: ~ (A = (cons @ (list @ TA) @ (cons @ TA @ B @ C) @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 121.10/95.44 thf(141,axiom,((! [TA: $tType]: ((wellorder @ TA) => (((?) @ TA) = (^ [A:(TA > $o)]: ? [B:TA]: ((A @ B) & ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (A @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_exists__least__iff)).
% 121.10/95.44 thf(833,plain,((! [TA: $tType]: ((wellorder @ TA) => (((?) @ TA) = (^ [A:(TA > $o)]: ? [B:TA]: ((A @ B) & ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (A @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 121.10/95.44 thf(22,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((? [C:TA]: ((A @ C) & ! [D:TA]: ((A @ D) => (D = C)))) => ((! [C:TA]: ((A @ C) => (B @ C))) => (B @ (the @ TA @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_the1I2)).
% 121.10/95.44 thf(405,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((? [C:TA]: ((A @ C) & ! [D:TA]: ((A @ D) => (D = C)))) => ((! [C:TA]: ((A @ C) => (B @ C))) => (B @ (the @ TA @ (A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 121.10/95.44 thf(113,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_less__imp__not__less)).
% 121.10/95.44 thf(735,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 121.10/95.44 thf(1,conjecture,((((type_M353778473_subst @ type_M1610475166scheme @ s1 @ (type_M91906176e_FVar @ x)) != (type_M353778473_subst @ type_M1610475166scheme @ s2 @ (type_M91906176e_FVar @ x))) | ~ (member @ nat @ n @ (type_M950795831ree_tv @ type_M1610475166scheme @ (type_M91906176e_FVar @ x))) | ((s1 @ n) = (s2 @ n)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 121.10/95.44 thf(2,negated_conjecture,((~ (((type_M353778473_subst @ type_M1610475166scheme @ s1 @ (type_M91906176e_FVar @ x)) != (type_M353778473_subst @ type_M1610475166scheme @ s2 @ (type_M91906176e_FVar @ x))) | ~ (member @ nat @ n @ (type_M950795831ree_tv @ type_M1610475166scheme @ (type_M91906176e_FVar @ x))) | ((s1 @ n) = (s2 @ n))))),inference(neg_conjecture,[status(cth)],[1])).
% 121.10/95.44 thf(300,plain,((~ (~ ((type_M353778473_subst @ type_M1610475166scheme @ (s1) @ (type_M91906176e_FVar @ x)) = (type_M353778473_subst @ type_M1610475166scheme @ (s2) @ (type_M91906176e_FVar @ x))) | ~ (member @ nat @ n @ (type_M950795831ree_tv @ type_M1610475166scheme @ (type_M91906176e_FVar @ x))) | ((s1 @ n) = (s2 @ n))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 121.10/95.44 thf(294,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) = (A = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_all__not__in__conv)).
% 121.10/95.44 thf(1348,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) = (A = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[294])).
% 121.10/95.44 thf(48,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_less__supI2)).
% 121.10/95.44 thf(506,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 121.10/95.44 thf(290,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA,D:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((~ (member @ TA @ C @ D)) => (((insert2 @ TA @ A @ B) = (insert2 @ TA @ C @ D)) = (((A = C) => (B = D)) & ((A != C) => (? [E:(set @ TA)]: ((B = (insert2 @ TA @ C @ E)) & ~ (member @ TA @ C @ E) & (D = (insert2 @ TA @ A @ E)) & ~ (member @ TA @ A @ E))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_insert__eq__iff)).
% 121.10/95.44 thf(1335,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA,D:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((~ (member @ TA @ C @ D)) => (((insert2 @ TA @ A @ B) = (insert2 @ TA @ C @ D)) = (((A = C) => (B = D)) & ((~ (A = C)) => (? [E:(set @ TA)]: ((B = (insert2 @ TA @ C @ E)) & ~ (member @ TA @ C @ E) & (D = (insert2 @ TA @ A @ E)) & ~ (member @ TA @ A @ E))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[290])).
% 121.10/95.44 thf(85,axiom,((bot @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Obot_23)).
% 121.10/95.44 thf(664,plain,((bot @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 121.10/95.44 thf(203,axiom,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (insert2 @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_singletonI)).
% 121.10/95.44 thf(1065,plain,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (insert2 @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 121.10/95.44 thf(179,axiom,((! [TA: $tType]: (! [A:((list @ TA) > ((list @ TA) > $o)),B:(list @ TA),C:(list @ TA)]: ((! [D:(list @ TA)]: (A @ (nil @ TA) @ D)) => ((! [D:TA,E:(list @ TA),F:(list @ TA)]: ((A @ F @ E) => (A @ (cons @ TA @ D @ E) @ F))) => (A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_splice_Oinduct)).
% 121.10/95.44 thf(955,plain,((! [TA: $tType]: (! [A:((list @ TA) > ((list @ TA) > $o)),B:(list @ TA),C:(list @ TA)]: ((! [D:(list @ TA)]: (A @ (nil @ TA) @ D)) => ((! [D:TA,E:(list @ TA),F:(list @ TA)]: ((A @ F @ E) => (A @ (cons @ TA @ D @ E) @ F))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 121.10/95.44 thf(241,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: ((member @ TA @ A @ B) => (member @ TA @ A @ (insert2 @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_insertI2)).
% 121.10/95.44 thf(1172,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: ((member @ TA @ A @ B) => (member @ TA @ A @ (insert2 @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 121.10/95.44 thf(162,axiom,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: ((type_M540877363scheme @ (type_Mirabelle_Fun @ A @ B)) = (type_M1518733067e_SFun @ (type_M540877363scheme @ A) @ (type_M540877363scheme @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_mk__scheme_Osimps_I2_J)).
% 121.10/95.44 thf(897,plain,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: ((type_M540877363scheme @ (type_Mirabelle_Fun @ A @ B)) = (type_M1518733067e_SFun @ (type_M540877363scheme @ A) @ (type_M540877363scheme @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 121.10/95.44 thf(37,axiom,((! [A:type_Mirabelle_typ,B:type_M1610475166scheme,C:type_M1610475166scheme]: (((type_M540877363scheme @ A) = (type_M1518733067e_SFun @ B @ C)) => (? [D:type_Mirabelle_typ,E:type_Mirabelle_typ]: ((B = (type_M540877363scheme @ D)) & (C = (type_M540877363scheme @ E))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_mk__scheme__Fun)).
% 121.10/95.44 thf(474,plain,((! [A:type_Mirabelle_typ,B:type_M1610475166scheme,C:type_M1610475166scheme]: (((type_M540877363scheme @ A) = (type_M1518733067e_SFun @ B @ C)) => (? [D:type_Mirabelle_typ,E:type_Mirabelle_typ]: ((B = (type_M540877363scheme @ D)) & (C = (type_M540877363scheme @ E))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 121.10/95.44 thf(275,axiom,(((type_Mirabelle_cod @ type_M17369686_subst) = (bot_bot @ (set @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_cod__id__subst)).
% 121.10/95.44 thf(1288,plain,(((type_Mirabelle_cod @ (type_M17369686_subst)) = (bot_bot @ (set @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[275])).
% 121.10/95.44 thf(19,axiom,((! [TA: $tType,TB: $tType]: ((bounded_lattice @ TA) => (bounde1808546759up_bot @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Obounded__semilattice__sup__bot)).
% 121.10/95.44 thf(400,plain,((! [TA: $tType,TB: $tType]: ((bounded_lattice @ TA) => (bounde1808546759up_bot @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 121.10/95.44 thf(108,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (sup_sup @ TA @ A @ B) @ C) => (~ ((ord_less @ TA @ A @ C) => (~ (ord_less @ TA @ B @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_sup_Ostrict__boundedE)).
% 121.10/95.44 thf(720,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (sup_sup @ TA @ A @ B) @ C) => (~ ((ord_less @ TA @ A @ C) => (~ (ord_less @ TA @ B @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 121.10/95.44 thf(238,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((member @ TA @ A @ (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_singletonD)).
% 121.10/95.44 thf(1165,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((member @ TA @ A @ (insert2 @ TA @ B @ (bot_bot @ (set @ TA)))) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 121.10/95.44 thf(111,axiom,((! [A:type_Mirabelle_typ]: ((! [B:nat]: (A != (type_Mirabelle_TVar @ B))) => (~ (! [B:type_Mirabelle_typ,C:type_Mirabelle_typ]: (A != (type_Mirabelle_Fun @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_typ_Oexhaust)).
% 121.10/95.44 thf(728,plain,((! [A:type_Mirabelle_typ]: ((! [B:nat]: ~ (A = (type_Mirabelle_TVar @ B))) => (~ (! [B:type_Mirabelle_typ,C:type_Mirabelle_typ]: ~ (A = (type_Mirabelle_Fun @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 121.10/95.44 thf(266,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_Collect__mem__eq)).
% 121.10/95.44 thf(1261,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 121.10/95.44 thf(59,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:TA,C:(list @ TA)]: ((A = (cons @ TA @ B @ C)) => (A != (nil @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_list_OdiscI)).
% 121.10/95.44 thf(575,plain,((! [TA: $tType]: (! [A:(list @ TA),B:TA,C:(list @ TA)]: ((A = (cons @ TA @ B @ C)) => (~ (A = (nil @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 121.10/95.44 thf(81,axiom,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_gt__ex)).
% 121.10/95.44 thf(644,plain,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 121.10/95.44 thf(166,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_order_Ostrict__implies__not__eq)).
% 121.10/95.44 thf(908,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 121.10/95.44 thf(139,axiom,((order @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder_21)).
% 121.10/95.44 thf(822,plain,((order @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 121.10/95.44 thf(147,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_less__asym)).
% 121.10/95.44 thf(850,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 121.10/95.44 thf(185,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: (((collect @ TA @ A) = (bot_bot @ (set @ TA))) = (! [B:TA]: ~ (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_Collect__empty__eq)).
% 121.10/95.44 thf(982,plain,((! [TA: $tType]: (! [A:(TA > $o)]: (((collect @ TA @ (A)) = (bot_bot @ (set @ TA))) = (! [B:TA]: ~ (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 121.10/95.44 thf(279,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((~ (member @ TA @ A @ C)) => (((insert2 @ TA @ A @ B) = (insert2 @ TA @ A @ C)) = (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_insert__ident)).
% 121.10/95.44 thf(1299,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((~ (member @ TA @ A @ C)) => (((insert2 @ TA @ A @ B) = (insert2 @ TA @ A @ C)) = (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[279])).
% 121.10/95.44 thf(154,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:TA,C:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (insert2 @ TA @ B @ C)) = (insert2 @ TA @ B @ (sup_sup @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_Un__insert__right)).
% 121.10/95.44 thf(871,plain,((! [TA: $tType]: (! [A:(set @ TA),B:TA,C:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (insert2 @ TA @ B @ C)) = (insert2 @ TA @ B @ (sup_sup @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 121.10/95.44 thf(222,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: (member @ TA @ A @ (insert2 @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_insertI1)).
% 121.10/95.44 thf(1120,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: (member @ TA @ A @ (insert2 @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 121.10/95.44 thf(45,axiom,((semilattice_sup @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Osemilattice__sup_17)).
% 121.10/95.44 thf(501,plain,((semilattice_sup @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 121.10/95.44 thf(215,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((? [B:TA]: (member @ TA @ B @ A)) = (A != (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_ex__in__conv)).
% 121.10/95.44 thf(1093,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((? [B:TA]: (member @ TA @ B @ A)) = (~ (A = (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 121.10/95.44 thf(143,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: (((collect @ TA @ A) = (bot_bot @ (set @ TA))) = (A = (bot_bot @ (TA > $o))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_Collect__empty__eq__bot)).
% 121.10/95.44 thf(839,plain,((! [TA: $tType]: (! [A:(TA > $o)]: (((collect @ TA @ (A)) = (bot_bot @ (set @ TA))) = ((A) = (bot_bot @ (TA > $o))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 121.10/95.44 thf(233,axiom,((! [TA: $tType]: ((type_M1470978233struct @ TA) => ((type_M779184887und_tv @ (list @ TA) @ (nil @ TA)) = (bot_bot @ (set @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_bound__tv__list_Osimps_I1_J)).
% 121.10/95.44 thf(1152,plain,((! [TA: $tType]: ((type_M1470978233struct @ TA) => ((type_M779184887und_tv @ (list @ TA) @ (nil @ TA)) = (bot_bot @ (set @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 121.10/95.44 thf(24,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_sup_Ostrict__coboundedI2)).
% 121.10/95.44 thf(427,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 121.10/95.44 thf(288,axiom,((type_M201404320of_nat @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Type__Mirabelle__sfxnzmapfi_Oof__nat)).
% 121.10/95.44 thf(1331,plain,((type_M201404320of_nat @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[288])).
% 121.10/95.44 thf(245,axiom,((! [A:type_Mirabelle_typ,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member @ nat @ D @ (type_M950795831ree_tv @ type_Mirabelle_typ @ A)) => ((B @ D) = (C @ D)))) => ((type_M353778473_subst @ type_Mirabelle_typ @ B @ A) = (type_M353778473_subst @ type_Mirabelle_typ @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_eq__free__eq__subst__te)).
% 121.10/95.44 thf(1184,plain,((! [A:type_Mirabelle_typ,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member @ nat @ D @ (type_M950795831ree_tv @ type_Mirabelle_typ @ A)) => ((B @ D) = (C @ D)))) => ((type_M353778473_subst @ type_Mirabelle_typ @ (B) @ A) = (type_M353778473_subst @ type_Mirabelle_typ @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 121.10/95.44 thf(119,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:(nat > TA),C:(type_M1610475166scheme > (type_M1610475166scheme > TA)),D:nat]: ((type_M697345518scheme @ TA @ A @ B @ C @ (type_M1264524676e_BVar @ D)) = (B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_type__scheme_Osimps_I11_J)).
% 121.10/95.44 thf(755,plain,((! [TA: $tType]: (! [A:(nat > TA),B:(nat > TA),C:(type_M1610475166scheme > (type_M1610475166scheme > TA)),D:nat]: ((type_M697345518scheme @ TA @ (A) @ (B) @ (C) @ (type_M1264524676e_BVar @ D)) = (B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 121.10/95.44 thf(211,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_UnI2)).
% 121.10/95.44 thf(1088,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 121.10/95.44 thf(65,axiom,((! [TA: $tType]: ((ord @ TA) => ((ord_lexordp_eq @ TA) = (^ [A:(list @ TA),B:(list @ TA)]: (? [C:(list @ TA)]: ((A = (nil @ TA)) & (B = C)) | ? [C:TA,D:TA,E:(list @ TA),F:(list @ TA)]: ((A = (cons @ TA @ C @ E)) & (B = (cons @ TA @ D @ F)) & (ord_less @ TA @ C @ D)) | ? [C:TA,D:TA,E:(list @ TA),F:(list @ TA)]: ((A = (cons @ TA @ C @ E)) & (B = (cons @ TA @ D @ F)) & ~ (ord_less @ TA @ C @ D) & ~ (ord_less @ TA @ D @ C) & (ord_lexordp_eq @ TA @ E @ F)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_lexordp__eq_Osimps)).
% 121.10/95.44 thf(592,plain,((! [TA: $tType]: ((ord @ TA) => ((ord_lexordp_eq @ TA) = (^ [A:(list @ TA),B:(list @ TA)]: (? [C:(list @ TA)]: ((A = (nil @ TA)) & (B = C)) | ? [C:TA,D:TA,E:(list @ TA),F:(list @ TA)]: ((A = (cons @ TA @ C @ E)) & (B = (cons @ TA @ D @ F)) & (ord_less @ TA @ C @ D)) | ? [C:TA,D:TA,E:(list @ TA),F:(list @ TA)]: ((A = (cons @ TA @ C @ E)) & (B = (cons @ TA @ D @ F)) & ~ (ord_less @ TA @ C @ D) & ~ (ord_less @ TA @ D @ C) & (ord_lexordp_eq @ TA @ E @ F)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 121.10/95.44 thf(205,axiom,((! [A:type_M1610475166scheme,B:type_M1610475166scheme]: ((type_M779184887und_tv @ type_M1610475166scheme @ (type_M1518733067e_SFun @ A @ B)) = (sup_sup @ (set @ nat) @ (type_M779184887und_tv @ type_M1610475166scheme @ A) @ (type_M779184887und_tv @ type_M1610475166scheme @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_bound__tv__type__scheme_Osimps_I3_J)).
% 121.10/95.44 thf(1069,plain,((! [A:type_M1610475166scheme,B:type_M1610475166scheme]: ((type_M779184887und_tv @ type_M1610475166scheme @ (type_M1518733067e_SFun @ A @ B)) = (sup_sup @ (set @ nat) @ (type_M779184887und_tv @ type_M1610475166scheme @ A) @ (type_M779184887und_tv @ type_M1610475166scheme @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 121.10/95.44 thf(103,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((insert2 @ TA @ A @ (insert2 @ TA @ A @ B)) = (insert2 @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_insert__absorb2)).
% 121.10/95.44 thf(708,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((insert2 @ TA @ A @ (insert2 @ TA @ A @ B)) = (insert2 @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 121.10/95.44 thf(1367,plain,(($false)),inference(e,[status(thm)],[809,1190,1168,1237,628,893,518,777,481,1005,1290,994,1205,523,582,762,1078,1310,1275,472,1327,747,340,1222,1196,1243,320,973,885,724,719,372,504,1264,587,949,1059,1132,638,606,1013,770,924,492,1302,789,321,646,348,806,866,1351,998,1169,397,687,1215,634,877,692,1072,453,1345,988,307,920,678,529,546,1199,1338,381,534,1067,714,1091,952,1355,1255,862,1174,598,392,424,429,815,916,1027,1128,1281,842,847,484,361,1365,852,435,1296,665,742,697,874,1096,1138,610,783,980,403,471,1329,1082,488,933,554,669,1016,1155,706,686,1075,1249,1297,1131,1246,1099,985,508,311,765,343,1318,1202,792,906,1278,1135,1146,1219,745,444,601,819,975,694,402,732,772,711,579,641,498,1107,1332,1092,1090,919,1258,947,350,604,900,681,1282,1117,1011,451,1144,737,1122,1307,880,649,890,494,631,858,700,1149,626,943,668,1177,758,1339,1162,726,959,868,780,394,1113,1000,1364,438,922,912,521,1213,768,455,883,1304,531,927,812,617,1018,836,490,675,1208,589,1181,823,776,855,690,1225,1252,739,1267,557,1003,441,585,502,1285,1358,703,1023,613,978,1008,595,1272,1240,991,845,1084,671,903,759,1126,1157,1321,1062,1101,652,390,786,1193,684,346,716,1161,620,447,432,833,405,735,300,1348,506,1335,664,1065,955,1172,897,474,1288,400,720,1165,728,1261,575,644,908,822,850,982,1299,871,1120,501,1093,839,1152,427,1331,1184,755,1088,592,1069,708])).
% 121.10/95.44 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 121.10/95.44 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------