Leo-III---1.8.0.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : ITP197^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39

% Computer : n010.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 21.93s 6.26s
% Output   : Refutation 23.31s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP197^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.20  % Computer : n010.cluster.edu
% 0.10/0.20  % Model    : x86_64 x86_64
% 0.10/0.20  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20  % Memory   : 8046.5625MB
% 0.10/0.20  % OS       : Linux 6.8.0-71-generic
% 0.10/0.20  % CPULimit : 300
% 0.10/0.20  % WCLimit  : 300
% 0.10/0.20  % DateTime : Tue Sep 29 20:10:48 UTC 2026
% 0.10/0.20  % CPUTime  : 
% 0.10/0.20  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.88/0.77  % [INFO] 	 Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ... 
% 2.20/1.18  % [INFO] 	 Parsing done (408ms). 
% 2.20/1.19  % [INFO] 	 Running in sequential loop mode. 
% 3.55/1.57  % [INFO] 	 eprover registered as external prover. 
% 3.55/1.58  % [INFO] 	 Scanning for conjecture ... 
% 3.99/1.73  % [INFO] 	 Found a conjecture (or negated_conjecture) and 359 axioms. Running axiom selection ... 
% 4.20/1.89  % [INFO] 	 Axiom selection finished. Selected 323 axioms (removed 36 axioms). 
% 5.31/2.17  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 5.58/2.20  % [INFO] 	 Type checking passed. 
% 5.58/2.20  % [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 ... 
% 21.93/6.26  % External prover 'e' found a proof!
% 21.93/6.26  % [INFO] 	 Killing All external provers ... 
% 21.93/6.26  % Time passed: 5925ms (effective reasoning time: 5059ms)
% 21.93/6.26  % 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)>
% 21.93/6.26  % Axioms used in derivation (323): fact_252_UnCI, fact_169_less__linear, fact_330_sup__bot_Osemilattice__neutr__axioms, fact_15_free__tv__type__scheme_Osimps_I1_J, fact_115_ord__eq__less__subst, fact_40_new__tv__def, fact_256_Un__insert__right, fact_321_sup_Ostrict__coboundedI1, fact_271_Un__empty__left, fact_298_sup__bot_Oneutr__eq__iff, fact_86_singleton__inject, fact_233_psubset__trans, fact_192_less__imp__not__eq2, fact_206_exists__least__iff, fact_67_equals0D, fact_189_antisym__conv3, fact_198_dual__order_Oirrefl, fact_296_sup__bot_Oright__neutral, fact_54_list_Oinject, help_If_3_1_If_001t__Type____Mirabelle____lczmhmumaa__Otyp_T, fact_351_new__tv__Nil, fact_41_new__tv__def, fact_268_Collect__disj__eq, fact_165_less__asym_H, fact_144_order__less__subst2, fact_29_new__tv__FVar, fact_46_singleton__conv, fact_202_order_Ostrict__trans, fact_139_order__less__subst1, fact_230_dom__id__subst, fact_152_neqE, fact_161_less__asym, fact_119_ord__eq__less__subst, fact_26_subst__mk__scheme, fact_201_order_Ostrict__trans, fact_123_ord__eq__less__subst, fact_164_less__asym_H, fact_27_new__tv__Fun2, fact_125_ord__less__eq__subst, fact_130_ord__less__eq__subst, fact_153_neq__iff, fact_94_bot__apply, fact_247_the1I2, fact_155_order_Oasym, fact_299_sup__bot_Oleft__neutral, fact_190_less__imp__not__eq2, fact_75_insert__commute, fact_278_bound__tv__list_Osimps_I2_J, fact_193_less__imp__triv, fact_269_Un__left__commute, fact_13_app__subst__Cons, fact_232_less__set__def, fact_319_sup_Ostrict__order__iff, fact_157_less__imp__neq, fact_50_insert__iff, fact_187_less__not__sym, fact_220_is__singletonE, fact_251_free__tv__subst, fact_126_ord__less__eq__subst, fact_172_less__irrefl, fact_285_free__tv__list_Osimps_I2_J, fact_111_not__psubset__empty, fact_135_order__less__subst1, fact_306_bot__eq__sup__iff, fact_167_less__trans, fact_185_less__not__sym, fact_294_sup__bot__right, fact_245_theI2, fact_225_mk__scheme_Osimps_I2_J, fact_77_insert__absorb, fact_25_new__tv__Cons, fact_237_typ_Oinduct, fact_282_bound__tv__type__scheme_Osimps_I3_J, fact_255_Un__insert__left, fact_181_dual__order_Oasym, fact_36_free__tv__type__scheme_Osimps_I2_J, fact_243_theI, fact_222_free__tv__id__subst, fact_210_dual__order_Ostrict__trans, fact_88_doubleton__eq__iff, fact_82_insertE, fact_234_new__tv__id__subst, fact_128_ord__less__eq__subst, fact_158_less__imp__neq, fact_18_type__scheme_Oinject_I2_J, fact_98_bot_Onot__eq__extremum, fact_145_order__less__subst2, fact_276_bound__tv__list_Osimps_I2_J, fact_170_less__irrefl, fact_293_sup__bot__right, fact_69_not__Cons__self2, fact_173_ord__eq__less__trans, fact_325_sup_Ostrict__coboundedI2, fact_113_is__singleton__the__elem, fact_44_new__tv__def, fact_250_bot__empty__eq, fact_223_Set_Ois__empty__def, fact_0_type__scheme_Oinject_I1_J, fact_39_new__tv__def, fact_240_the__eq__trivial, fact_290_free__tv__fun__def, fact_104_bound__tv__type__scheme_Osimps_I1_J, fact_30_type__scheme_Odistinct_I5_J, fact_174_ord__eq__less__trans, fact_138_order__less__subst1, fact_168_less__trans, fact_37_type__scheme_Oexhaust, fact_7_type__scheme_Odistinct_I3_J, fact_279_bound__tv__list_Osimps_I2_J, fact_136_order__less__subst1, fact_76_insert__eq__iff, fact_150_order__less__subst2, fact_231_psubsetD, fact_315_sup_Ostrict__boundedE, fact_175_ord__eq__less__trans, fact_219_mk__scheme_Osimps_I1_J, fact_4_app__subst__type__scheme_Osimps_I2_J, fact_203_less__imp__not__less, fact_209_dual__order_Ostrict__trans, fact_47_singleton__conv2, fact_316_sup_Ostrict__boundedE, fact_71_not__Cons__self2, fact_199_dual__order_Oirrefl, fact_160_less__asym, fact_214_order_Ostrict__implies__not__eq, fact_216_dual__order_Ostrict__implies__not__eq, fact_162_less__asym, fact_132_ord__less__eq__subst, fact_261_Un__def, fact_120_ord__eq__less__subst, fact_23_new__tv__Cons, fact_20_new__tv__Cons, fact_273_singleton__Un__iff, fact_151_gt__ex, fact_352_free__tv__list_Osimps_I1_J, fact_97_bot_Onot__eq__extremum, fact_302_sup__bot_Oeq__neutr__iff, fact_81_insertI1, fact_260_UnI2, fact_131_ord__less__eq__subst, fact_31_mk__scheme__Fun, help_If_1_1_If_001t__Type____Mirabelle____lczmhmumaa__Otyp_T, fact_127_ord__less__eq__subst, fact_228_typ_Oinject_I2_J, fact_244_theI_H, fact_101_bot_Oextremum__strict, fact_64_new__if__subst__type__scheme__list, fact_22_new__tv__Cons, fact_6_type__scheme_Odistinct_I1_J, fact_154_order_Oasym, fact_177_ord__less__eq__trans, fact_239_the__sym__eq__trivial, fact_241_the__equality, fact_35_mk__scheme__injective, fact_124_ord__less__eq__subst, fact_65_ex__in__conv, fact_303_sup__eq__bot__iff, fact_227_id__subst__def, fact_2_scheme__substitutions__only__on__free__variables, fact_308_sup__set__def, fact_141_order__less__subst1, fact_207_linorder__less__wlog, fact_275_insert__is__Un, fact_5_app__subst__type__scheme_Osimps_I3_J, fact_191_less__imp__not__eq2, fact_105_typ_Oinject_I1_J, fact_85_insert__compr, fact_52_list_Oinject, fact_100_bot_Oextremum__strict, fact_180_dual__order_Oasym, fact_258_UnE, fact_329_sup__bot_Osemilattice__neutr__axioms, fact_300_sup__bot_Oleft__neutral, fact_277_bound__tv__list_Osimps_I2_J, fact_117_ord__eq__less__subst, fact_142_order__less__subst2, fact_280_free__tv__Fun, fact_95_bound__tv__type__scheme_Osimps_I2_J, fact_79_Set_Oset__insert, fact_307_sup__Un__eq, fact_116_ord__eq__less__subst, fact_66_equals0I, fact_262_bex__Un, fact_109_scheme__list__substitutions__only__on__free__variables, fact_218_bot__fun__def, fact_292_sup__bot__left, fact_92_Collect__conv__if, fact_249_Collect__empty__eq__bot, fact_48_singletonI, fact_110_bot__set__def, fact_108_eq__free__eq__subst__scheme__list, fact_147_order__less__subst2, fact_61_all__not__in__conv, fact_91_Collect__conv__if2, fact_204_less__imp__not__less, fact_134_order__less__subst1, fact_28_new__tv__BVar, fact_313_less__supI2, fact_322_sup_Ostrict__coboundedI1, fact_148_order__less__subst2, fact_248_the1__equality, fact_121_ord__eq__less__subst, fact_289_free__tv__list_Osimps_I2_J, fact_19_new__tv__Cons, fact_55_list_Oinject, fact_90_singletonD, fact_49_insertCI, fact_176_ord__less__eq__trans, fact_33_eq__subst__te__eq__free, fact_68_emptyE, fact_133_order__less__subst1, fact_224_the__elem__def, fact_159_less__imp__neq, fact_129_ord__less__eq__subst, fact_194_less__imp__triv, fact_146_order__less__subst2, fact_286_free__tv__list_Osimps_I2_J, fact_259_UnI1, fact_257_weaken__asm__Un, fact_21_new__tv__Cons, fact_266_Un__commute, fact_211_not__less__iff__gr__or__eq, fact_287_free__tv__list_Osimps_I2_J, fact_274_Un__singleton__iff, fact_38_type__scheme_Oinduct, fact_263_ball__Un, fact_213_order_Ostrict__implies__not__eq, fact_221_is__singleton__def, fact_3_app__subst__type__scheme_Osimps_I1_J, fact_182_less__imp__not__eq, fact_288_free__tv__list_Osimps_I2_J, fact_297_sup__bot_Oneutr__eq__iff, fact_143_order__less__subst2, fact_284_free__tv__list_Osimps_I2_J, fact_178_ord__less__eq__trans, fact_281_free__tv__type__scheme_Osimps_I3_J, fact_304_sup__eq__bot__iff, fact_140_order__less__subst1, fact_17_type__scheme_Oinject_I3_J, fact_179_dual__order_Oasym, fact_87_insert__not__empty, fact_34_typ__substitutions__only__on__free__variables, fact_114_is__singletonI_H, fact_171_less__irrefl, fact_215_dual__order_Ostrict__implies__not__eq, fact_57_empty__iff, fact_99_bot_Onot__eq__extremum, fact_112_app__subst__TVar, fact_264_Un__assoc, fact_200_order_Ostrict__trans, fact_16_new__if__subst__type__scheme, fact_59_Collect__mem__eq, fact_74_mk__disjoint__insert, fact_267_Un__left__absorb, fact_32_eq__free__eq__subst__te, fact_107_new__tv__TVar__subst, fact_43_new__tv__def, fact_78_insert__ident, fact_310_less__supI1, fact_1_eq__free__eq__subst__type__scheme, help_If_2_1_If_001t__Type____Mirabelle____lczmhmumaa__Otyp_T, fact_72_not__Cons__self2, fact_156_order_Oasym, fact_238_typ_Odistinct_I1_J, fact_163_less__asym_H, fact_226_Type__Mirabelle__lczmhmumaa_Odom__def, fact_137_order__less__subst1, fact_188_less__induct, fact_122_ord__eq__less__subst, fact_186_less__not__sym, fact_318_sup_Ostrict__order__iff, fact_89_singleton__iff, fact_312_less__supI2, fact_80_insertI2, fact_184_less__imp__not__eq, fact_83_empty__def, fact_291_sup__bot__left, fact_195_less__imp__triv, fact_196_linorder__cases, fact_283_free__tv__list_Osimps_I2_J, fact_24_new__tv__Cons, fact_327_Nitpick_OThe__psimp, fact_236_typ_Oexhaust, fact_42_new__tv__def, fact_295_sup__bot_Oright__neutral, fact_63_empty__Collect__eq, fact_350_app__subst__Nil, fact_270_insert__def, fact_217_dual__order_Ostrict__implies__not__eq, fact_309_less__supI1, fact_166_less__trans, fact_60_Collect__cong, fact_84_insert__Collect, fact_149_order__less__subst2, fact_51_insert__absorb2, fact_183_less__imp__not__eq, fact_324_sup_Ostrict__coboundedI2, fact_253_Un__iff, fact_254_Un__empty, fact_197_dual__order_Oirrefl, fact_205_less__imp__not__less, fact_103_free__tv__TVar, fact_106_new__tv__TVar, fact_96_is__singletonI, fact_328_theI__unique, fact_212_order_Ostrict__implies__not__eq, fact_102_bot_Oextremum__strict, fact_265_Un__absorb, fact_272_Un__empty__right, fact_208_dual__order_Ostrict__trans, fact_229_new__tv__Fun, fact_118_ord__eq__less__subst, fact_14_free__tv__mk__scheme, fact_70_not__Cons__self2, fact_62_Collect__empty__eq, fact_242_cod__id__subst, fact_53_list_Oinject, fact_301_sup__bot_Oeq__neutr__iff, fact_58_mem__Collect__eq, fact_235_app__subst__Fun, fact_305_bot__eq__sup__iff, fact_93_the__elem__eq, fact_45_new__tv__def
% 21.93/6.26  % No. of inferences in proof: 650
% 21.93/6.26  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 5925 ms resp. 5059 ms w/o parsing
% 23.31/6.55  % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.31/6.55  thf(list_l1704431731scheme_type, type, list_l1704431731scheme: $tType).
% 23.31/6.55  thf(list_l865305402le_typ_type, type, list_l865305402le_typ: $tType).
% 23.31/6.55  thf(list_l1334080099scheme_type, type, list_l1334080099scheme: $tType).
% 23.31/6.55  thf(list_n396811828le_typ_type, type, list_n396811828le_typ: $tType).
% 23.31/6.55  thf(list_l1790670291le_typ_type, type, list_l1790670291le_typ: $tType).
% 23.31/6.55  thf(list_T247403987scheme_type, type, list_T247403987scheme: $tType).
% 23.31/6.55  thf(list_T1103309005le_typ_type, type, list_T1103309005le_typ: $tType).
% 23.31/6.55  thf(type_M1694694083scheme_type, type, type_M1694694083scheme: $tType).
% 23.31/6.55  thf(list_set_nat_type, type, list_set_nat: $tType).
% 23.31/6.55  thf(list_nat_o_type, type, list_nat_o: $tType).
% 23.31/6.55  thf(type_Mirabelle_typ_type, type, type_Mirabelle_typ: $tType).
% 23.31/6.55  thf(list_nat_type, type, list_nat: $tType).
% 23.31/6.55  thf(set_nat_type, type, set_nat: $tType).
% 23.31/6.55  thf(nat_type, type, nat: $tType).
% 23.31/6.55  thf(the_nat_decl, type, the_nat: ((nat > $o) > nat)).
% 23.31/6.55  thf(if_Typ1169047309le_typ_decl, type, if_Typ1169047309le_typ: ($o > (type_Mirabelle_typ > (type_Mirabelle_typ > type_Mirabelle_typ)))).
% 23.31/6.55  thf(semila1414375521_nat_o_decl, type, semila1414375521_nat_o: (((nat > $o) > ((nat > $o) > (nat > $o))) > ((nat > $o) > $o))).
% 23.31/6.55  thf(semila1369944356et_nat_decl, type, semila1369944356et_nat: ((set_nat > (set_nat > set_nat)) > (set_nat > $o))).
% 23.31/6.55  thf(sup_sup_nat_o_decl, type, sup_sup_nat_o: ((nat > $o) > ((nat > $o) > (nat > $o)))).
% 23.31/6.55  thf(sup_sup_set_nat_decl, type, sup_sup_set_nat: (set_nat > (set_nat > set_nat))).
% 23.31/6.55  thf(cons_n499085924le_typ_decl, type, cons_n499085924le_typ: ((nat > type_Mirabelle_typ) > (list_n396811828le_typ > list_n396811828le_typ))).
% 23.31/6.55  thf(cons_l1800589546le_typ_decl, type, cons_l1800589546le_typ: (list_n396811828le_typ > (list_l865305402le_typ > list_l865305402le_typ))).
% 23.31/6.55  thf(cons_l531914285scheme_decl, type, cons_l531914285scheme: (list_l1334080099scheme > (list_l1704431731scheme > list_l1704431731scheme))).
% 23.31/6.55  thf(cons_l392684675le_typ_decl, type, cons_l392684675le_typ: (list_T1103309005le_typ > (list_l1790670291le_typ > list_l1790670291le_typ))).
% 23.31/6.55  thf(cons_l1910959773scheme_decl, type, cons_l1910959773scheme: (list_T247403987scheme > (list_l1334080099scheme > list_l1334080099scheme))).
% 23.31/6.55  thf(cons_T363929085le_typ_decl, type, cons_T363929085le_typ: (type_Mirabelle_typ > (list_T1103309005le_typ > list_T1103309005le_typ))).
% 23.31/6.55  thf(cons_T633159821scheme_decl, type, cons_T633159821scheme: (type_M1694694083scheme > (list_T247403987scheme > list_T247403987scheme))).
% 23.31/6.55  thf(nil_Ty61485117scheme_decl, type, nil_Ty61485117scheme: list_T247403987scheme).
% 23.31/6.55  thf(bot_bot_nat_o_decl, type, bot_bot_nat_o: (nat > $o)).
% 23.31/6.55  thf(bot_bot_o_decl, type, bot_bot_o: $o).
% 23.31/6.55  thf(bot_bot_nat_decl, type, bot_bot_nat: nat).
% 23.31/6.55  thf(bot_bot_set_nat_decl, type, bot_bot_set_nat: set_nat).
% 23.31/6.55  thf(ord_less_nat_o_decl, type, ord_less_nat_o: ((nat > $o) > ((nat > $o) > $o))).
% 23.31/6.55  thf(ord_less_nat_decl, type, ord_less_nat: (nat > (nat > $o))).
% 23.31/6.55  thf(ord_less_set_nat_decl, type, ord_less_set_nat: (set_nat > (set_nat > $o))).
% 23.31/6.55  thf(collect_nat_decl, type, collect_nat: ((nat > $o) > set_nat)).
% 23.31/6.55  thf(insert_nat_decl, type, insert_nat: (nat > (set_nat > set_nat))).
% 23.31/6.55  thf(is_empty_nat_decl, type, is_empty_nat: (set_nat > $o)).
% 23.31/6.55  thf(is_singleton_nat_decl, type, is_singleton_nat: (set_nat > $o)).
% 23.31/6.55  thf(the_elem_nat_decl, type, the_elem_nat: (set_nat > nat)).
% 23.31/6.55  thf(type_Mirabelle_cod_decl, type, type_Mirabelle_cod: ((nat > type_Mirabelle_typ) > set_nat)).
% 23.31/6.55  thf(type_Mirabelle_dom_decl, type, type_Mirabelle_dom: ((nat > type_Mirabelle_typ) > set_nat)).
% 23.31/6.55  thf(type_M405566558_subst_decl, type, type_M405566558_subst: (nat > type_Mirabelle_typ)).
% 23.31/6.55  thf(type_M1006385707scheme_decl, type, type_M1006385707scheme: (type_Mirabelle_typ > type_M1694694083scheme)).
% 23.31/6.55  thf(type_M1734147655le_typ_decl, type, type_M1734147655le_typ: (nat > ((nat > type_Mirabelle_typ) > $o))).
% 23.31/6.55  thf(type_M244876119le_typ_decl, type, type_M244876119le_typ: (nat > (list_n396811828le_typ > $o))).
% 23.31/6.55  thf(type_M2086816231le_typ_decl, type, type_M2086816231le_typ: (nat > (list_l865305402le_typ > $o))).
% 23.31/6.55  thf(type_M1172169604scheme_decl, type, type_M1172169604scheme: (nat > (list_l1704431731scheme > $o))).
% 23.31/6.55  thf(type_M1826376056le_typ_decl, type, type_M1826376056le_typ: (nat > (list_l1790670291le_typ > $o))).
% 23.31/6.55  thf(type_M1377662078scheme_decl, type, type_M1377662078scheme: (nat > (list_l1334080099scheme > $o))).
% 23.31/6.55  thf(type_M263553000le_typ_decl, type, type_M263553000le_typ: (nat > (list_T1103309005le_typ > $o))).
% 23.31/6.55  thf(type_M2064939256scheme_decl, type, type_M2064939256scheme: (nat > (list_T247403987scheme > $o))).
% 23.31/6.55  thf(type_M1211611096le_typ_decl, type, type_M1211611096le_typ: (nat > (type_Mirabelle_typ > $o))).
% 23.31/6.55  thf(type_M1963061490scheme_decl, type, type_M1963061490scheme: (nat > (type_M1694694083scheme > $o))).
% 23.31/6.55  thf(type_M1898948661at_nat_decl, type, type_M1898948661at_nat: (nat > nat)).
% 23.31/6.55  thf(type_Mirabelle_Fun_decl, type, type_Mirabelle_Fun: (type_Mirabelle_typ > (type_Mirabelle_typ > type_Mirabelle_typ))).
% 23.31/6.55  thf(type_Mirabelle_TVar_decl, type, type_Mirabelle_TVar: (nat > type_Mirabelle_typ)).
% 23.31/6.55  thf(type_M1743451154le_typ_decl, type, type_M1743451154le_typ: (type_Mirabelle_typ > type_Mirabelle_typ)).
% 23.31/6.55  thf(type_M2048935292e_BVar_decl, type, type_M2048935292e_BVar: (nat > type_M1694694083scheme)).
% 23.31/6.55  thf(type_M876316792e_FVar_decl, type, type_M876316792e_FVar: (nat > type_M1694694083scheme)).
% 23.31/6.55  thf(type_M155660035e_SFun_decl, type, type_M155660035e_SFun: (type_M1694694083scheme > (type_M1694694083scheme > type_M1694694083scheme))).
% 23.31/6.55  thf(type_M1944210753scheme_decl, type, type_M1944210753scheme: ((nat > type_Mirabelle_typ) > (list_T247403987scheme > list_T247403987scheme))).
% 23.31/6.55  thf(type_M784671311le_typ_decl, type, type_M784671311le_typ: ((nat > type_Mirabelle_typ) > (type_Mirabelle_typ > type_Mirabelle_typ))).
% 23.31/6.55  thf(type_M1690910139scheme_decl, type, type_M1690910139scheme: ((nat > type_Mirabelle_typ) > (type_M1694694083scheme > type_M1694694083scheme))).
% 23.31/6.55  thf(type_M772783356le_typ_decl, type, type_M772783356le_typ: ((nat > type_Mirabelle_typ) > set_nat)).
% 23.31/6.55  thf(type_M513401740le_typ_decl, type, type_M513401740le_typ: (list_n396811828le_typ > set_nat)).
% 23.31/6.55  thf(type_M1496178953scheme_decl, type, type_M1496178953scheme: (list_l1334080099scheme > set_nat)).
% 23.31/6.55  thf(type_M1539052445le_typ_decl, type, type_M1539052445le_typ: (list_T1103309005le_typ > set_nat)).
% 23.31/6.55  thf(type_M961603331scheme_decl, type, type_M961603331scheme: (list_T247403987scheme > set_nat)).
% 23.31/6.55  thf(type_M801073677le_typ_decl, type, type_M801073677le_typ: (type_Mirabelle_typ > set_nat)).
% 23.31/6.55  thf(type_M326705277scheme_decl, type, type_M326705277scheme: (type_M1694694083scheme > set_nat)).
% 23.31/6.55  thf(type_M1715972684le_typ_decl, type, type_M1715972684le_typ: ((nat > type_Mirabelle_typ) > set_nat)).
% 23.31/6.55  thf(type_M1691543772le_typ_decl, type, type_M1691543772le_typ: (list_n396811828le_typ > set_nat)).
% 23.31/6.55  thf(type_M906078444le_typ_decl, type, type_M906078444le_typ: (list_l865305402le_typ > set_nat)).
% 23.31/6.55  thf(type_M1926053183scheme_decl, type, type_M1926053183scheme: (list_l1704431731scheme > set_nat)).
% 23.31/6.55  thf(type_M1418941437le_typ_decl, type, type_M1418941437le_typ: (list_l1790670291le_typ > set_nat)).
% 23.31/6.55  thf(type_M1958029241scheme_decl, type, type_M1958029241scheme: (list_l1334080099scheme > set_nat)).
% 23.31/6.55  thf(type_M510873837le_typ_decl, type, type_M510873837le_typ: (list_T1103309005le_typ > set_nat)).
% 23.31/6.55  thf(type_M141510067scheme_decl, type, type_M141510067scheme: (list_T247403987scheme > set_nat)).
% 23.31/6.55  thf(type_M49385309le_typ_decl, type, type_M49385309le_typ: (type_Mirabelle_typ > set_nat)).
% 23.31/6.55  thf(type_M1050318637scheme_decl, type, type_M1050318637scheme: (type_M1694694083scheme > set_nat)).
% 23.31/6.55  thf(member_nat_decl, type, member_nat: (nat > (set_nat > $o))).
% 23.31/6.55  thf(s1_decl, type, s1: (nat > type_Mirabelle_typ)).
% 23.31/6.55  thf(s2_decl, type, s2: (nat > type_Mirabelle_typ)).
% 23.31/6.55  thf(n_decl, type, n: nat).
% 23.31/6.55  thf(x_decl, type, x: nat).
% 23.31/6.55  thf(179,axiom,((! [A:(nat > type_Mirabelle_typ),B:nat]: ((type_M784671311le_typ @ A @ (type_Mirabelle_TVar @ B)) = (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_112_app__subst__TVar)).
% 23.31/6.55  thf(1036,plain,((! [A:(nat > type_Mirabelle_typ),B:nat]: ((type_M784671311le_typ @ (A) @ (type_Mirabelle_TVar @ B)) = (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 23.31/6.55  thf(176,axiom,((bot_bot_nat_o = (^ [A:nat]: (bot_bot_o)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_218_bot__fun__def)).
% 23.31/6.55  thf(1024,plain,(((bot_bot_nat_o) = (^ [A:nat]: (bot_bot_o)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 23.31/6.55  thf(264,axiom,((! [A:set_nat]: ((A != bot_bot_set_nat) => ((! [B:nat,C:nat]: ((member_nat @ B @ A) => ((member_nat @ C @ A) => (B = C)))) => (is_singleton_nat @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_114_is__singletonI_H)).
% 23.31/6.55  thf(1369,plain,((! [A:set_nat]: ((~ (A = bot_bot_set_nat)) => ((! [B:nat,C:nat]: ((member_nat @ B @ A) => ((member_nat @ C @ A) => (B = C)))) => (is_singleton_nat @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 23.31/6.55  thf(317,axiom,((! [A:nat,B:nat]: ((type_M1963061490scheme @ A @ (type_M876316792e_FVar @ B)) = (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_29_new__tv__FVar)).
% 23.31/6.55  thf(1559,plain,((! [A:nat,B:nat]: ((type_M1963061490scheme @ A @ (type_M876316792e_FVar @ B)) = (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[317])).
% 23.31/6.55  thf(250,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_212_order_Ostrict__implies__not__eq)).
% 23.31/6.55  thf(1315,plain,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 23.31/6.55  thf(153,axiom,((! [A:nat,B:list_T247403987scheme,C:(nat > type_Mirabelle_typ),D:(nat > type_Mirabelle_typ)]: ((type_M2064939256scheme @ A @ B) => ((type_M1944210753scheme @ (^ [E:nat]: (if_Typ1169047309le_typ @ (ord_less_nat @ E @ A) @ (C @ E) @ (D @ E))) @ B) = (type_M1944210753scheme @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_64_new__if__subst__type__scheme__list)).
% 23.31/6.55  thf(941,plain,((! [A:nat,B:list_T247403987scheme,C:(nat > type_Mirabelle_typ),D:(nat > type_Mirabelle_typ)]: ((type_M2064939256scheme @ A @ B) => ((type_M1944210753scheme @ (^ [E:nat]: (if_Typ1169047309le_typ @ (ord_less_nat @ E @ A) @ (C @ E) @ (D @ E))) @ B) = (type_M1944210753scheme @ (C) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 23.31/6.55  thf(314,axiom,((! [A:nat,B:nat]: ((type_M876316792e_FVar @ A) != (type_M2048935292e_BVar @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_type__scheme_Odistinct_I1_J)).
% 23.31/6.55  thf(1549,plain,((! [A:nat,B:nat]: ~ ((type_M876316792e_FVar @ A) = (type_M2048935292e_BVar @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[314])).
% 23.31/6.55  thf(227,axiom,((! [A:nat,B:type_M1694694083scheme,C:type_M1694694083scheme]: ((type_M1963061490scheme @ A @ (type_M155660035e_SFun @ B @ C)) = ((type_M1963061490scheme @ A @ B) & (type_M1963061490scheme @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_27_new__tv__Fun2)).
% 23.31/6.55  thf(1237,plain,((! [A:nat,B:type_M1694694083scheme,C:type_M1694694083scheme]: ((type_M1963061490scheme @ A @ (type_M155660035e_SFun @ B @ C)) = ((type_M1963061490scheme @ A @ B) & (type_M1963061490scheme @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 23.31/6.55  thf(128,axiom,((! [A:set_nat,B:nat,C:set_nat]: ((sup_sup_set_nat @ A @ (insert_nat @ B @ C)) = (insert_nat @ B @ (sup_sup_set_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_256_Un__insert__right)).
% 23.31/6.55  thf(846,plain,((! [A:set_nat,B:nat,C:set_nat]: ((sup_sup_set_nat @ A @ (insert_nat @ B @ C)) = (insert_nat @ B @ (sup_sup_set_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 23.31/6.55  thf(178,axiom,((! [A:nat,B:nat,C:(nat > set_nat),D:set_nat]: ((ord_less_nat @ A @ B) => ((ord_less_set_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_set_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_142_order__less__subst2)).
% 23.31/6.55  thf(1031,plain,((! [A:nat,B:nat,C:(nat > set_nat),D:set_nat]: ((ord_less_nat @ A @ B) => ((ord_less_set_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_set_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 23.31/6.55  thf(3,axiom,((! [A:(nat > $o),B:nat,C:(nat > $o)]: ((A @ B) => ((! [D:nat]: ((A @ D) => (D = B))) => ((! [D:nat]: ((A @ D) => (C @ D))) => (C @ (the_nat @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_245_theI2)).
% 23.31/6.55  thf(333,plain,((! [A:(nat > $o),B:nat,C:(nat > $o)]: ((A @ B) => ((! [D:nat]: ((A @ D) => (D = B))) => ((! [D:nat]: ((A @ D) => (C @ D))) => (C @ (the_nat @ (A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 23.31/6.55  thf(67,axiom,((! [A:nat]: (is_singleton_nat @ (insert_nat @ A @ bot_bot_set_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_is__singletonI)).
% 23.31/6.55  thf(628,plain,((! [A:nat]: (is_singleton_nat @ (insert_nat @ A @ bot_bot_set_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 23.31/6.55  thf(162,axiom,((! [A:(nat > $o),B:(nat > (nat > $o)),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat_o @ (B @ E) @ (B @ F)))) => (ord_less_nat_o @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_116_ord__eq__less__subst)).
% 23.31/6.55  thf(977,plain,((! [A:(nat > $o),B:(nat > (nat > $o)),C:nat,D:nat]: (((A) = (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat_o @ (B @ E) @ (B @ F)))) => (ord_less_nat_o @ (A) @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 23.31/6.55  thf(101,axiom,((! [A:nat,B:set_nat]: ((insert_nat @ A @ (insert_nat @ A @ B)) = (insert_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_51_insert__absorb2)).
% 23.31/6.55  thf(762,plain,((! [A:nat,B:set_nat]: ((insert_nat @ A @ (insert_nat @ A @ B)) = (insert_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 23.31/6.55  thf(171,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => (ord_less_set_nat @ A @ (sup_sup_set_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_313_less__supI2)).
% 23.31/6.55  thf(1005,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => (ord_less_set_nat @ A @ (sup_sup_set_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 23.31/6.55  thf(84,axiom,((! [A:nat,B:type_M1694694083scheme,C:list_T247403987scheme]: ((type_M2064939256scheme @ A @ (cons_T633159821scheme @ B @ C)) = ((type_M1963061490scheme @ A @ B) & (type_M2064939256scheme @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_25_new__tv__Cons)).
% 23.31/6.55  thf(683,plain,((! [A:nat,B:type_M1694694083scheme,C:list_T247403987scheme]: ((type_M2064939256scheme @ A @ (cons_T633159821scheme @ B @ C)) = ((type_M1963061490scheme @ A @ B) & (type_M2064939256scheme @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 23.31/6.55  thf(307,axiom,((! [A:(nat > type_Mirabelle_typ),B:type_M1694694083scheme,C:list_T247403987scheme]: ((type_M1944210753scheme @ A @ (cons_T633159821scheme @ B @ C)) = (cons_T633159821scheme @ (type_M1690910139scheme @ A @ B) @ (type_M1944210753scheme @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_13_app__subst__Cons)).
% 23.31/6.55  thf(1522,plain,((! [A:(nat > type_Mirabelle_typ),B:type_M1694694083scheme,C:list_T247403987scheme]: ((type_M1944210753scheme @ (A) @ (cons_T633159821scheme @ B @ C)) = (cons_T633159821scheme @ (type_M1690910139scheme @ (A) @ B) @ (type_M1944210753scheme @ (A) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[307])).
% 23.31/6.55  thf(166,axiom,((semila1369944356et_nat @ sup_sup_set_nat @ bot_bot_set_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_330_sup__bot_Osemilattice__neutr__axioms)).
% 23.31/6.55  thf(994,plain,((semila1369944356et_nat @ (sup_sup_set_nat) @ bot_bot_set_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 23.31/6.55  thf(273,axiom,((! [A:nat,B:set_nat,C:nat]: (((~ (member_nat @ A @ B)) => (A = C)) => (member_nat @ A @ (insert_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_49_insertCI)).
% 23.31/6.55  thf(1401,plain,((! [A:nat,B:set_nat,C:nat]: (((~ (member_nat @ A @ B)) => (A = C)) => (member_nat @ A @ (insert_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[273])).
% 23.31/6.55  thf(311,axiom,((! [A:list_T247403987scheme,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member_nat @ D @ (type_M141510067scheme @ A)) => ((B @ D) = (C @ D)))) => ((type_M1944210753scheme @ B @ A) = (type_M1944210753scheme @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_108_eq__free__eq__subst__scheme__list)).
% 23.31/6.55  thf(1533,plain,((! [A:list_T247403987scheme,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member_nat @ D @ (type_M141510067scheme @ A)) => ((B @ D) = (C @ D)))) => ((type_M1944210753scheme @ (B) @ A) = (type_M1944210753scheme @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[311])).
% 23.31/6.55  thf(82,axiom,((! [A:(nat > $o)]: ((sup_sup_nat_o @ A @ bot_bot_nat_o) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_293_sup__bot__right)).
% 23.31/6.55  thf(677,plain,((! [A:(nat > $o)]: ((sup_sup_nat_o @ A @ bot_bot_nat_o) = (A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 23.31/6.55  thf(248,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((B = C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_178_ord__less__eq__trans)).
% 23.31/6.55  thf(1305,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((B = C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 23.31/6.55  thf(59,axiom,((! [A:nat,B:list_T247403987scheme,C:list_l1334080099scheme]: ((type_M1377662078scheme @ A @ (cons_l1910959773scheme @ B @ C)) = ((type_M2064939256scheme @ A @ B) & (type_M1377662078scheme @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_22_new__tv__Cons)).
% 23.31/6.55  thf(597,plain,((! [A:nat,B:list_T247403987scheme,C:list_l1334080099scheme]: ((type_M1377662078scheme @ A @ (cons_l1910959773scheme @ B @ C)) = ((type_M2064939256scheme @ A @ B) & (type_M1377662078scheme @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 23.31/6.55  thf(299,axiom,((insert_nat = (^ [A:nat,B:set_nat]: (collect_nat @ (^ [C:nat]: ((C = A) | (member_nat @ C @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_85_insert__compr)).
% 23.31/6.55  thf(1497,plain,(((insert_nat) = (^ [A:nat,B:set_nat]: (collect_nat @ (^ [C:nat]: ((C = A) | (member_nat @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[299])).
% 23.31/6.55  thf(9,axiom,((! [A:(nat > $o),B:nat]: ((A @ B) => ((! [C:nat]: ((A @ C) => (C = B))) => ((the_nat @ A) = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_241_the__equality)).
% 23.31/6.55  thf(385,plain,((! [A:(nat > $o),B:nat]: ((A @ B) => ((! [C:nat]: ((A @ C) => (C = B))) => ((the_nat @ (A)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 23.31/6.55  thf(249,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ A @ B) => ((B = C) => (ord_less_nat_o @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_177_ord__less__eq__trans)).
% 23.31/6.55  thf(1310,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (((B) = (C)) => (ord_less_nat_o @ (A) @ (C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 23.31/6.55  thf(211,axiom,((! [A:nat,B:nat]: (((type_Mirabelle_TVar @ A) = (type_Mirabelle_TVar @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_105_typ_Oinject_I1_J)).
% 23.31/6.55  thf(1164,plain,((! [A:nat,B:nat]: (((type_Mirabelle_TVar @ A) = (type_Mirabelle_TVar @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 23.31/6.55  thf(239,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((! [C:nat]: ((A @ C) = (B @ C))) => ((collect_nat @ A) = (collect_nat @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_60_Collect__cong)).
% 23.31/6.55  thf(1275,plain,((! [A:(nat > $o),B:(nat > $o)]: ((! [C:nat]: ((A @ C) = (B @ C))) => ((collect_nat @ (A)) = (collect_nat @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 23.31/6.55  thf(26,axiom,((is_singleton_nat = (^ [A:set_nat]: (A = (insert_nat @ (the_elem_nat @ A) @ bot_bot_set_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_113_is__singleton__the__elem)).
% 23.31/6.55  thf(472,plain,(((is_singleton_nat) = (^ [A:set_nat]: (A = (insert_nat @ (the_elem_nat @ A) @ bot_bot_set_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 23.31/6.55  thf(235,axiom,((! [A:type_Mirabelle_typ,B:type_M1694694083scheme,C:type_M1694694083scheme]: (((type_M1006385707scheme @ A) = (type_M155660035e_SFun @ B @ C)) => (? [D:type_Mirabelle_typ,E:type_Mirabelle_typ]: ((B = (type_M1006385707scheme @ D)) & (C = (type_M1006385707scheme @ E))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_31_mk__scheme__Fun)).
% 23.31/6.55  thf(1260,plain,((! [A:type_Mirabelle_typ,B:type_M1694694083scheme,C:type_M1694694083scheme]: (((type_M1006385707scheme @ A) = (type_M155660035e_SFun @ B @ C)) => (? [D:type_Mirabelle_typ,E:type_Mirabelle_typ]: ((B = (type_M1006385707scheme @ D)) & (C = (type_M1006385707scheme @ E))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 23.31/6.55  thf(154,axiom,((! [A:set_nat,B:set_nat,C:(set_nat > (nat > $o)),D:(nat > $o)]: ((ord_less_set_nat @ A @ B) => ((ord_less_nat_o @ (C @ B) @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat_o @ (C @ E) @ (C @ F)))) => (ord_less_nat_o @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_146_order__less__subst2)).
% 23.31/6.55  thf(945,plain,((! [A:set_nat,B:set_nat,C:(set_nat > (nat > $o)),D:(nat > $o)]: ((ord_less_set_nat @ A @ B) => ((ord_less_nat_o @ (C @ B) @ (D)) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat_o @ (C @ E) @ (C @ F)))) => (ord_less_nat_o @ (C @ A) @ (D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 23.31/6.55  thf(185,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (B != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_191_less__imp__not__eq2)).
% 23.31/6.55  thf(1063,plain,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (~ ((B) = (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 23.31/6.55  thf(260,axiom,((! [A:set_nat]: ((? [B:nat]: (member_nat @ B @ A)) = (A != bot_bot_set_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_65_ex__in__conv)).
% 23.31/6.55  thf(1354,plain,((! [A:set_nat]: ((? [B:nat]: (member_nat @ B @ A)) = (~ (A = bot_bot_set_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 23.31/6.55  thf(151,axiom,((! [A:set_nat]: ~ (ord_less_set_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_170_less__irrefl)).
% 23.31/6.55  thf(930,plain,((! [A:set_nat]: ~ (ord_less_set_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 23.31/6.55  thf(79,axiom,((! [A:nat]: (type_M1734147655le_typ @ A @ type_Mirabelle_TVar))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_107_new__tv__TVar__subst)).
% 23.31/6.55  thf(670,plain,((! [A:nat]: (type_M1734147655le_typ @ A @ (type_Mirabelle_TVar)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 23.31/6.56  thf(205,axiom,((! [A:set_nat]: ((sup_sup_set_nat @ A @ bot_bot_set_nat) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_272_Un__empty__right)).
% 23.31/6.56  thf(1127,plain,((! [A:set_nat]: ((sup_sup_set_nat @ A @ bot_bot_set_nat) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 23.31/6.56  thf(12,axiom,(((type_Mirabelle_dom @ type_M405566558_subst) = bot_bot_set_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_230_dom__id__subst)).
% 23.31/6.56  thf(417,plain,(((type_Mirabelle_dom @ (type_M405566558_subst)) = bot_bot_set_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 23.31/6.56  thf(263,axiom,((! [A:nat,B:set_nat]: ((member_nat @ A @ B) => ((insert_nat @ A @ B) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_77_insert__absorb)).
% 23.31/6.56  thf(1366,plain,((! [A:nat,B:set_nat]: ((member_nat @ A @ B) => ((insert_nat @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 23.31/6.56  thf(161,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_182_less__imp__not__eq)).
% 23.31/6.56  thf(973,plain,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 23.31/6.56  thf(182,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_141_order__less__subst1)).
% 23.31/6.56  thf(1046,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 23.31/6.56  thf(281,axiom,((! [A:type_M1694694083scheme,B:type_M1694694083scheme]: ((type_M1050318637scheme @ (type_M155660035e_SFun @ A @ B)) = (sup_sup_set_nat @ (type_M1050318637scheme @ A) @ (type_M1050318637scheme @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_281_free__tv__type__scheme_Osimps_I3_J)).
% 23.31/6.56  thf(1430,plain,((! [A:type_M1694694083scheme,B:type_M1694694083scheme]: ((type_M1050318637scheme @ (type_M155660035e_SFun @ A @ B)) = (sup_sup_set_nat @ (type_M1050318637scheme @ A) @ (type_M1050318637scheme @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[281])).
% 23.31/6.56  thf(114,axiom,((! [A:set_nat]: ~ (ord_less_set_nat @ A @ bot_bot_set_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_101_bot_Oextremum__strict)).
% 23.31/6.56  thf(802,plain,((! [A:set_nat]: ~ (ord_less_set_nat @ A @ bot_bot_set_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 23.31/6.56  thf(288,axiom,((! [A:nat,B:type_M1694694083scheme,C:type_M1694694083scheme]: ((type_M876316792e_FVar @ A) != (type_M155660035e_SFun @ B @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_type__scheme_Odistinct_I3_J)).
% 23.31/6.56  thf(1462,plain,((! [A:nat,B:type_M1694694083scheme,C:type_M1694694083scheme]: ~ ((type_M876316792e_FVar @ A) = (type_M155660035e_SFun @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[288])).
% 23.31/6.56  thf(56,axiom,((! [A:set_nat]: ((is_singleton_nat @ A) => (~ (! [B:nat]: (A != (insert_nat @ B @ bot_bot_set_nat))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_220_is__singletonE)).
% 23.31/6.56  thf(587,plain,((! [A:set_nat]: ((is_singleton_nat @ A) => (~ (! [B:nat]: ~ (A = (insert_nat @ B @ bot_bot_set_nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 23.31/6.56  thf(252,axiom,((! [A:type_M1694694083scheme,B:type_M1694694083scheme,C:type_M1694694083scheme,D:type_M1694694083scheme]: (((type_M155660035e_SFun @ A @ B) = (type_M155660035e_SFun @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_17_type__scheme_Oinject_I3_J)).
% 23.31/6.56  thf(1323,plain,((! [A:type_M1694694083scheme,B:type_M1694694083scheme,C:type_M1694694083scheme,D:type_M1694694083scheme]: (((type_M155660035e_SFun @ A @ B) = (type_M155660035e_SFun @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 23.31/6.56  thf(303,axiom,((! [A:type_Mirabelle_typ]: ((type_M1050318637scheme @ (type_M1006385707scheme @ A)) = (type_M49385309le_typ @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_14_free__tv__mk__scheme)).
% 23.31/6.56  thf(1511,plain,((! [A:type_Mirabelle_typ]: ((type_M1050318637scheme @ (type_M1006385707scheme @ A)) = (type_M49385309le_typ @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[303])).
% 23.31/6.56  thf(91,axiom,((! [A:set_nat,B:set_nat]: ((sup_sup_set_nat @ A @ (sup_sup_set_nat @ A @ B)) = (sup_sup_set_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_267_Un__left__absorb)).
% 23.31/6.56  thf(702,plain,((! [A:set_nat,B:set_nat]: ((sup_sup_set_nat @ A @ (sup_sup_set_nat @ A @ B)) = (sup_sup_set_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 23.31/6.56  thf(145,axiom,((! [A:(nat > type_Mirabelle_typ),B:list_n396811828le_typ]: ((type_M1691543772le_typ @ (cons_n499085924le_typ @ A @ B)) = (sup_sup_set_nat @ (type_M1715972684le_typ @ A) @ (type_M1691543772le_typ @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_288_free__tv__list_Osimps_I2_J)).
% 23.31/6.56  thf(902,plain,((! [A:(nat > type_Mirabelle_typ),B:list_n396811828le_typ]: ((type_M1691543772le_typ @ (cons_n499085924le_typ @ (A) @ B)) = (sup_sup_set_nat @ (type_M1715972684le_typ @ (A)) @ (type_M1691543772le_typ @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 23.31/6.56  thf(48,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (B != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_216_dual__order_Ostrict__implies__not__eq)).
% 23.31/6.56  thf(559,plain,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (~ ((B) = (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 23.31/6.56  thf(304,axiom,((! [A:type_M1694694083scheme,B:list_T247403987scheme]: ((type_M141510067scheme @ (cons_T633159821scheme @ A @ B)) = (sup_sup_set_nat @ (type_M1050318637scheme @ A) @ (type_M141510067scheme @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_289_free__tv__list_Osimps_I2_J)).
% 23.31/6.56  thf(1514,plain,((! [A:type_M1694694083scheme,B:list_T247403987scheme]: ((type_M141510067scheme @ (cons_T633159821scheme @ A @ B)) = (sup_sup_set_nat @ (type_M1050318637scheme @ A) @ (type_M141510067scheme @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[304])).
% 23.31/6.56  thf(230,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (ord_less_set_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_160_less__asym)).
% 23.31/6.56  thf(1247,plain,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (ord_less_set_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 23.31/6.56  thf(251,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/sandbox2/benchmark/theBenchmark.p',fact_236_typ_Oexhaust)).
% 23.31/6.56  thf(1319,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)],[251])).
% 23.31/6.56  thf(257,axiom,((type_M244876119le_typ = (^ [A:nat,B:list_n396811828le_typ]: ! [C:nat]: ((member_nat @ C @ (type_M1691543772le_typ @ B)) => (ord_less_nat @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_39_new__tv__def)).
% 23.31/6.56  thf(1347,plain,(((type_M244876119le_typ) = (^ [A:nat,B:list_n396811828le_typ]: ! [C:nat]: ((member_nat @ C @ (type_M1691543772le_typ @ B)) => (ord_less_nat @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 23.31/6.56  thf(138,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_156_order_Oasym)).
% 23.31/6.56  thf(881,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 23.31/6.56  thf(200,axiom,((! [A:set_nat,B:set_nat,C:nat]: (((sup_sup_set_nat @ A @ B) = (insert_nat @ C @ bot_bot_set_nat)) = (((A = bot_bot_set_nat) & (B = (insert_nat @ C @ bot_bot_set_nat))) | ((A = (insert_nat @ C @ bot_bot_set_nat)) & (B = bot_bot_set_nat)) | ((A = (insert_nat @ C @ bot_bot_set_nat)) & (B = (insert_nat @ C @ bot_bot_set_nat))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_274_Un__singleton__iff)).
% 23.31/6.56  thf(1115,plain,((! [A:set_nat,B:set_nat,C:nat]: (((sup_sup_set_nat @ A @ B) = (insert_nat @ C @ bot_bot_set_nat)) = (((A = bot_bot_set_nat) & (B = (insert_nat @ C @ bot_bot_set_nat))) | ((A = (insert_nat @ C @ bot_bot_set_nat)) & (B = bot_bot_set_nat)) | ((A = (insert_nat @ C @ bot_bot_set_nat)) & (B = (insert_nat @ C @ bot_bot_set_nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 23.31/6.56  thf(320,axiom,((! [A:set_nat,B:set_nat,C:(nat > $o)]: ((? [D:nat]: ((member_nat @ D @ (sup_sup_set_nat @ A @ B)) & (C @ D))) = (? [D:nat]: ((member_nat @ D @ A) & (C @ D)) | ? [D:nat]: ((member_nat @ D @ B) & (C @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_262_bex__Un)).
% 23.31/6.56  thf(1568,plain,((! [A:set_nat,B:set_nat,C:(nat > $o)]: ((? [D:nat]: ((member_nat @ D @ (sup_sup_set_nat @ A @ B)) & (C @ D))) = (? [D:nat]: ((member_nat @ D @ A) & (C @ D)) | ? [D:nat]: ((member_nat @ D @ B) & (C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[320])).
% 23.31/6.56  thf(226,axiom,((! [A:nat,B:nat,C:(nat > (nat > $o)),D:(nat > $o)]: ((ord_less_nat @ A @ B) => ((ord_less_nat_o @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat_o @ (C @ E) @ (C @ F)))) => (ord_less_nat_o @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_143_order__less__subst2)).
% 23.31/6.56  thf(1232,plain,((! [A:nat,B:nat,C:(nat > (nat > $o)),D:(nat > $o)]: ((ord_less_nat @ A @ B) => ((ord_less_nat_o @ (C @ B) @ (D)) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat_o @ (C @ E) @ (C @ F)))) => (ord_less_nat_o @ (C @ A) @ (D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 23.31/6.56  thf(174,axiom,((! [A:set_nat,B:(nat > set_nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_set_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_115_ord__eq__less__subst)).
% 23.31/6.56  thf(1013,plain,((! [A:set_nat,B:(nat > set_nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_set_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 23.31/6.56  thf(104,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_168_less__trans)).
% 23.31/6.56  thf(770,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 23.31/6.56  thf(18,axiom,((! [A:(nat > type_Mirabelle_typ),B:list_n396811828le_typ,C:(nat > type_Mirabelle_typ),D:list_n396811828le_typ]: (((cons_n499085924le_typ @ A @ B) = (cons_n499085924le_typ @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_55_list_Oinject)).
% 23.31/6.56  thf(448,plain,((! [A:(nat > type_Mirabelle_typ),B:list_n396811828le_typ,C:(nat > type_Mirabelle_typ),D:list_n396811828le_typ]: (((cons_n499085924le_typ @ (A) @ B) = (cons_n499085924le_typ @ (C) @ D)) = (((A) = (C)) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 23.31/6.56  thf(298,axiom,((! [A:(nat > type_Mirabelle_typ),B:type_Mirabelle_typ]: ((type_M1690910139scheme @ A @ (type_M1006385707scheme @ B)) = (type_M1006385707scheme @ (type_M784671311le_typ @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_26_subst__mk__scheme)).
% 23.31/6.56  thf(1494,plain,((! [A:(nat > type_Mirabelle_typ),B:type_Mirabelle_typ]: ((type_M1690910139scheme @ (A) @ (type_M1006385707scheme @ B)) = (type_M1006385707scheme @ (type_M784671311le_typ @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[298])).
% 23.31/6.56  thf(149,axiom,((! [A:list_n396811828le_typ,B:list_l865305402le_typ]: ((type_M906078444le_typ @ (cons_l1800589546le_typ @ A @ B)) = (sup_sup_set_nat @ (type_M1691543772le_typ @ A) @ (type_M906078444le_typ @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_283_free__tv__list_Osimps_I2_J)).
% 23.31/6.56  thf(924,plain,((! [A:list_n396811828le_typ,B:list_l865305402le_typ]: ((type_M906078444le_typ @ (cons_l1800589546le_typ @ A @ B)) = (sup_sup_set_nat @ (type_M1691543772le_typ @ A) @ (type_M906078444le_typ @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 23.31/6.56  thf(110,axiom,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: ((type_M49385309le_typ @ (type_Mirabelle_Fun @ A @ B)) = (sup_sup_set_nat @ (type_M49385309le_typ @ A) @ (type_M49385309le_typ @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_280_free__tv__Fun)).
% 23.31/6.56  thf(789,plain,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: ((type_M49385309le_typ @ (type_Mirabelle_Fun @ A @ B)) = (sup_sup_set_nat @ (type_M49385309le_typ @ A) @ (type_M49385309le_typ @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 23.31/6.56  thf(284,axiom,((! [A:nat,B:nat]: ((member_nat @ A @ (insert_nat @ B @ bot_bot_set_nat)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_89_singleton__iff)).
% 23.31/6.56  thf(1450,plain,((! [A:nat,B:nat]: ((member_nat @ A @ (insert_nat @ B @ bot_bot_set_nat)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[284])).
% 23.31/6.56  thf(57,axiom,((! [A:type_M1694694083scheme,B:list_T247403987scheme,C:type_M1694694083scheme,D:list_T247403987scheme]: (((cons_T633159821scheme @ A @ B) = (cons_T633159821scheme @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_52_list_Oinject)).
% 23.31/6.56  thf(591,plain,((! [A:type_M1694694083scheme,B:list_T247403987scheme,C:type_M1694694083scheme,D:list_T247403987scheme]: (((cons_T633159821scheme @ A @ B) = (cons_T633159821scheme @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 23.31/6.56  thf(198,axiom,((! [A:(nat > $o)]: ~ (ord_less_nat_o @ A @ bot_bot_nat_o))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_100_bot_Oextremum__strict)).
% 23.31/6.56  thf(1109,plain,((! [A:(nat > $o)]: ~ (ord_less_nat_o @ (A) @ (bot_bot_nat_o)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 23.31/6.56  thf(277,axiom,((! [A:nat]: ((type_M1050318637scheme @ (type_M2048935292e_BVar @ A)) = bot_bot_set_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_36_free__tv__type__scheme_Osimps_I2_J)).
% 23.31/6.56  thf(1418,plain,((! [A:nat]: ((type_M1050318637scheme @ (type_M2048935292e_BVar @ A)) = bot_bot_set_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[277])).
% 23.31/6.56  thf(29,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (~ (ord_less_nat_o @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_164_less__asym_H)).
% 23.31/6.56  thf(485,plain,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (~ (ord_less_nat_o @ (B) @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 23.31/6.56  thf(52,axiom,((! [A:set_nat,B:set_nat]: ((bot_bot_set_nat = (sup_sup_set_nat @ A @ B)) = ((A = bot_bot_set_nat) & (B = bot_bot_set_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_306_bot__eq__sup__iff)).
% 23.31/6.56  thf(574,plain,((! [A:set_nat,B:set_nat]: ((bot_bot_set_nat = (sup_sup_set_nat @ A @ B)) = ((A = bot_bot_set_nat) & (B = bot_bot_set_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 23.31/6.56  thf(4,axiom,((! [A:type_Mirabelle_typ,B:list_T1103309005le_typ,C:type_Mirabelle_typ,D:list_T1103309005le_typ]: (((cons_T363929085le_typ @ A @ B) = (cons_T363929085le_typ @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_54_list_Oinject)).
% 23.31/6.56  thf(353,plain,((! [A:type_Mirabelle_typ,B:list_T1103309005le_typ,C:type_Mirabelle_typ,D:list_T1103309005le_typ]: (((cons_T363929085le_typ @ A @ B) = (cons_T363929085le_typ @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 23.31/6.56  thf(241,axiom,((! [A:set_nat,B:((nat > $o) > set_nat),C:(nat > $o),D:(nat > $o)]: ((ord_less_set_nat @ A @ (B @ C)) => ((ord_less_nat_o @ C @ D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ E @ F) => (ord_less_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_set_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_137_order__less__subst1)).
% 23.31/6.56  thf(1283,plain,((! [A:set_nat,B:((nat > $o) > set_nat),C:(nat > $o),D:(nat > $o)]: ((ord_less_set_nat @ A @ (B @ (C))) => ((ord_less_nat_o @ (C) @ (D)) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ (E) @ (F)) => (ord_less_set_nat @ (B @ (E)) @ (B @ (F))))) => (ord_less_set_nat @ A @ (B @ (D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 23.31/6.56  thf(183,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => ((ord_less_set_nat @ C @ A) => (ord_less_set_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_208_dual__order_Ostrict__trans)).
% 23.31/6.56  thf(1051,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => ((ord_less_set_nat @ C @ A) => (ord_less_set_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 23.31/6.56  thf(146,axiom,((! [A:nat,B:nat,C:(nat > set_nat),D:set_nat]: ((ord_less_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_set_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_124_ord__less__eq__subst)).
% 23.31/6.56  thf(905,plain,((! [A:nat,B:nat,C:(nat > set_nat),D:set_nat]: ((ord_less_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_set_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 23.31/6.56  thf(69,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => ((ord_less_set_nat @ B @ C) => (ord_less_set_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_200_order_Ostrict__trans)).
% 23.31/6.56  thf(634,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => ((ord_less_set_nat @ B @ C) => (ord_less_set_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 23.31/6.56  thf(96,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_132_ord__less__eq__subst)).
% 23.31/6.56  thf(734,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 23.31/6.56  thf(133,axiom,((! [A:set_nat,B:(nat > set_nat),C:nat,D:nat]: ((ord_less_set_nat @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_set_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_135_order__less__subst1)).
% 23.31/6.56  thf(866,plain,((! [A:set_nat,B:(nat > set_nat),C:nat,D:nat]: ((ord_less_set_nat @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_set_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 23.31/6.56  thf(259,axiom,((! [A:set_nat]: ((collect_nat @ (^ [B:nat]: (member_nat @ B @ A))) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_59_Collect__mem__eq)).
% 23.31/6.56  thf(1351,plain,((! [A:set_nat]: ((collect_nat @ (^ [B:nat]: (member_nat @ B @ A))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 23.31/6.56  thf(164,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_172_less__irrefl)).
% 23.31/6.56  thf(988,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 23.31/6.56  thf(282,axiom,((! [A:nat,B:set_nat]: ((member_nat @ A @ B) => (? [C:set_nat]: ((B = (insert_nat @ A @ C)) & ~ (member_nat @ A @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_74_mk__disjoint__insert)).
% 23.31/6.56  thf(1433,plain,((! [A:nat,B:set_nat]: ((member_nat @ A @ B) => (? [C:set_nat]: ((B = (insert_nat @ A @ C)) & ~ (member_nat @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 23.31/6.56  thf(136,axiom,((ord_less_nat_o = (^ [A:(nat > $o),B:(nat > $o)]: ((B = (sup_sup_nat_o @ B @ A)) & (B != A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_318_sup_Ostrict__order__iff)).
% 23.31/6.56  thf(877,plain,(((ord_less_nat_o) = (^ [A:(nat > $o),B:(nat > $o)]: ((B = (sup_sup_nat_o @ B @ A)) & ~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 23.31/6.56  thf(87,axiom,((type_Mirabelle_dom = (^ [A:(nat > type_Mirabelle_typ)]: (collect_nat @ (^ [B:nat]: ((A @ B) != (type_Mirabelle_TVar @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_226_Type__Mirabelle__lczmhmumaa_Odom__def)).
% 23.31/6.56  thf(692,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)],[87])).
% 23.31/6.56  thf(196,axiom,((! [A:set_nat]: ~ (ord_less_set_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_197_dual__order_Oirrefl)).
% 23.31/6.56  thf(1104,plain,((! [A:set_nat]: ~ (ord_less_set_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 23.31/6.56  thf(129,axiom,((! [A:nat,B:(nat > type_Mirabelle_typ),C:list_n396811828le_typ]: ((type_M244876119le_typ @ A @ (cons_n499085924le_typ @ B @ C)) = ((type_M1734147655le_typ @ A @ B) & (type_M244876119le_typ @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_24_new__tv__Cons)).
% 23.31/6.56  thf(849,plain,((! [A:nat,B:(nat > type_Mirabelle_typ),C:list_n396811828le_typ]: ((type_M244876119le_typ @ A @ (cons_n499085924le_typ @ (B) @ C)) = ((type_M1734147655le_typ @ A @ (B)) & (type_M244876119le_typ @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 23.31/6.56  thf(188,axiom,((! [A:nat,B:nat]: ((type_M1211611096le_typ @ A @ (type_Mirabelle_TVar @ B)) = (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_106_new__tv__TVar)).
% 23.31/6.56  thf(1074,plain,((! [A:nat,B:nat]: ((type_M1211611096le_typ @ A @ (type_Mirabelle_TVar @ B)) = (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 23.31/6.56  thf(283,axiom,((! [A:(type_M1694694083scheme > $o),B:type_M1694694083scheme]: ((! [C:nat]: (A @ (type_M876316792e_FVar @ C))) => ((! [C:nat]: (A @ (type_M2048935292e_BVar @ C))) => ((! [C:type_M1694694083scheme,D:type_M1694694083scheme]: ((A @ C) => ((A @ D) => (A @ (type_M155660035e_SFun @ C @ D))))) => (A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_38_type__scheme_Oinduct)).
% 23.31/6.56  thf(1438,plain,((! [A:(type_M1694694083scheme > $o),B:type_M1694694083scheme]: ((! [C:nat]: (A @ (type_M876316792e_FVar @ C))) => ((! [C:nat]: (A @ (type_M2048935292e_BVar @ C))) => ((! [C:type_M1694694083scheme,D:type_M1694694083scheme]: ((A @ C) => ((A @ D) => (A @ (type_M155660035e_SFun @ C @ D))))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[283])).
% 23.31/6.56  thf(44,axiom,((! [A:set_nat,B:(set_nat > set_nat),C:set_nat,D:set_nat]: ((ord_less_set_nat @ A @ (B @ C)) => ((ord_less_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_set_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_136_order__less__subst1)).
% 23.31/6.56  thf(546,plain,((! [A:set_nat,B:(set_nat > set_nat),C:set_nat,D:set_nat]: ((ord_less_set_nat @ A @ (B @ C)) => ((ord_less_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_set_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 23.31/6.56  thf(220,axiom,((! [A:nat,B:(set_nat > nat),C:set_nat,D:set_nat]: ((A = (B @ C)) => ((ord_less_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_117_ord__eq__less__subst)).
% 23.31/6.56  thf(1199,plain,((! [A:nat,B:(set_nat > nat),C:set_nat,D:set_nat]: ((A = (B @ C)) => ((ord_less_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 23.31/6.56  thf(117,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((bot_bot_nat_o = (sup_sup_nat_o @ A @ B)) = ((A = bot_bot_nat_o) & (B = bot_bot_nat_o))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_305_bot__eq__sup__iff)).
% 23.31/6.56  thf(810,plain,((! [A:(nat > $o),B:(nat > $o)]: (((bot_bot_nat_o) = (sup_sup_nat_o @ A @ B)) = (((A) = (bot_bot_nat_o)) & ((B) = (bot_bot_nat_o)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 23.31/6.56  thf(290,axiom,((! [A:type_M1694694083scheme]: ((! [B:nat]: (A != (type_M876316792e_FVar @ B))) => ((! [B:nat]: (A != (type_M2048935292e_BVar @ B))) => (~ (! [B:type_M1694694083scheme,C:type_M1694694083scheme]: (A != (type_M155660035e_SFun @ B @ C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_37_type__scheme_Oexhaust)).
% 23.31/6.56  thf(1470,plain,((! [A:type_M1694694083scheme]: ((! [B:nat]: ~ (A = (type_M876316792e_FVar @ B))) => ((! [B:nat]: ~ (A = (type_M2048935292e_BVar @ B))) => (~ (! [B:type_M1694694083scheme,C:type_M1694694083scheme]: ~ (A = (type_M155660035e_SFun @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[290])).
% 23.31/6.56  thf(41,axiom,((! [A:(nat > $o),B:(nat > $o),C:$o]: ((ord_less_nat_o @ A @ B) => ((ord_less_nat_o @ B @ A) => (C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_194_less__imp__triv)).
% 23.31/6.56  thf(534,plain,((! [A:(nat > $o),B:(nat > $o),C:$o]: ((ord_less_nat_o @ (A) @ (B)) => ((ord_less_nat_o @ (B) @ (A)) => (C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 23.31/6.56  thf(186,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_184_less__imp__not__eq)).
% 23.31/6.56  thf(1067,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 23.31/6.56  thf(113,axiom,((! [A:nat,B:type_M1694694083scheme,C:type_M1694694083scheme]: ((type_M2048935292e_BVar @ A) != (type_M155660035e_SFun @ B @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_30_type__scheme_Odistinct_I5_J)).
% 23.31/6.56  thf(798,plain,((! [A:nat,B:type_M1694694083scheme,C:type_M1694694083scheme]: ~ ((type_M2048935292e_BVar @ A) = (type_M155660035e_SFun @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 23.31/6.56  thf(269,axiom,((! [A:nat,B:set_nat,C:nat]: ((member_nat @ A @ B) => (member_nat @ A @ (insert_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_80_insertI2)).
% 23.31/6.56  thf(1387,plain,((! [A:nat,B:set_nat,C:nat]: ((member_nat @ A @ B) => (member_nat @ A @ (insert_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 23.31/6.56  thf(322,axiom,((! [A:nat,B:set_nat,C:set_nat]: ((member_nat @ A @ (sup_sup_set_nat @ B @ C)) => ((~ (member_nat @ A @ B)) => (member_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_258_UnE)).
% 23.31/6.56  thf(1580,plain,((! [A:nat,B:set_nat,C:set_nat]: ((member_nat @ A @ (sup_sup_set_nat @ B @ C)) => ((~ (member_nat @ A @ B)) => (member_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[322])).
% 23.31/6.56  thf(233,axiom,((bot_bot_nat_o = (^ [A:nat]: (bot_bot_o)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_94_bot__apply)).
% 23.31/6.56  thf(1255,plain,(((bot_bot_nat_o) = (^ [A:nat]: (bot_bot_o)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 23.31/6.56  thf(203,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (ord_less_set_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_185_less__not__sym)).
% 23.31/6.56  thf(1123,plain,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (ord_less_set_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 23.31/6.56  thf(222,axiom,((! [A:nat]: ? [B:nat]: (ord_less_nat @ A @ B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_151_gt__ex)).
% 23.31/6.56  thf(1217,plain,((! [A:nat]: ? [B:nat]: (ord_less_nat @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 23.31/6.56  thf(301,axiom,((! [A:nat]: ((type_M1006385707scheme @ (type_Mirabelle_TVar @ A)) = (type_M876316792e_FVar @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_219_mk__scheme_Osimps_I1_J)).
% 23.31/6.56  thf(1502,plain,((! [A:nat]: ((type_M1006385707scheme @ (type_Mirabelle_TVar @ A)) = (type_M876316792e_FVar @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[301])).
% 23.31/6.56  thf(68,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_183_less__imp__not__eq)).
% 23.31/6.56  thf(630,plain,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (~ ((A) = (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 23.31/6.56  thf(95,axiom,((! [A:set_nat,B:set_nat,C:(set_nat > set_nat),D:set_nat]: ((ord_less_set_nat @ A @ B) => ((ord_less_set_nat @ (C @ B) @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_set_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_145_order__less__subst2)).
% 23.31/6.56  thf(729,plain,((! [A:set_nat,B:set_nat,C:(set_nat > set_nat),D:set_nat]: ((ord_less_set_nat @ A @ B) => ((ord_less_set_nat @ (C @ B) @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_set_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 23.31/6.56  thf(225,axiom,((! [A:nat,B:((nat > $o) > nat),C:(nat > $o),D:(nat > $o)]: ((A = (B @ C)) => ((ord_less_nat_o @ C @ D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_120_ord__eq__less__subst)).
% 23.31/6.56  thf(1223,plain,((! [A:nat,B:((nat > $o) > nat),C:(nat > $o),D:(nat > $o)]: ((A = (B @ (C))) => ((ord_less_nat_o @ (C) @ (D)) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ (E) @ (F)) => (ord_less_nat @ (B @ (E)) @ (B @ (F))))) => (ord_less_nat @ A @ (B @ (D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 23.31/6.56  thf(142,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((collect_nat @ (^ [C:nat]: ((A @ C) | (B @ C)))) = (sup_sup_set_nat @ (collect_nat @ A) @ (collect_nat @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_268_Collect__disj__eq)).
% 23.31/6.56  thf(894,plain,((! [A:(nat > $o),B:(nat > $o)]: ((collect_nat @ (^ [C:nat]: ((A @ C) | (B @ C)))) = (sup_sup_set_nat @ (collect_nat @ (A)) @ (collect_nat @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 23.31/6.56  thf(98,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_192_less__imp__not__eq2)).
% 23.31/6.56  thf(746,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 23.31/6.56  thf(192,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (~ (ord_less_nat_o @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_155_order_Oasym)).
% 23.31/6.56  thf(1091,plain,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (~ (ord_less_nat_o @ (B) @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 23.31/6.56  thf(181,axiom,((! [A:nat,B:set_nat]: ((insert_nat @ A @ B) != bot_bot_set_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_87_insert__not__empty)).
% 23.31/6.56  thf(1042,plain,((! [A:nat,B:set_nat]: ~ ((insert_nat @ A @ B) = bot_bot_set_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 23.31/6.56  thf(156,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (ord_less_nat_o @ A @ (sup_sup_nat_o @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_312_less__supI2)).
% 23.31/6.56  thf(952,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (ord_less_nat_o @ (A) @ (sup_sup_nat_o @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 23.31/6.56  thf(279,axiom,((type_M2064939256scheme = (^ [A:nat,B:list_T247403987scheme]: ! [C:nat]: ((member_nat @ C @ (type_M141510067scheme @ B)) => (ord_less_nat @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_44_new__tv__def)).
% 23.31/6.56  thf(1423,plain,(((type_M2064939256scheme) = (^ [A:nat,B:list_T247403987scheme]: ! [C:nat]: ((member_nat @ C @ (type_M141510067scheme @ B)) => (ord_less_nat @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[279])).
% 23.31/6.56  thf(148,axiom,((! [A:(nat > $o),B:nat]: (((A @ B) => ((collect_nat @ (^ [C:nat]: ((B = C) & (A @ C)))) = (insert_nat @ B @ bot_bot_set_nat))) & ((~ (A @ B)) => ((collect_nat @ (^ [C:nat]: ((B = C) & (A @ C)))) = bot_bot_set_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_91_Collect__conv__if2)).
% 23.31/6.56  thf(916,plain,((! [A:(nat > $o),B:nat]: (((A @ B) => ((collect_nat @ (^ [C:nat]: ((B = C) & (A @ C)))) = (insert_nat @ B @ bot_bot_set_nat))) & ((~ (A @ B)) => ((collect_nat @ (^ [C:nat]: ((B = C) & (A @ C)))) = bot_bot_set_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 23.31/6.56  thf(50,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ bot_bot_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_102_bot_Oextremum__strict)).
% 23.31/6.56  thf(566,plain,((! [A:nat]: ~ (ord_less_nat @ A @ bot_bot_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 23.31/6.56  thf(66,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (ord_less_nat_o @ A @ (sup_sup_nat_o @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_324_sup_Ostrict__coboundedI2)).
% 23.31/6.56  thf(625,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (ord_less_nat_o @ (A) @ (sup_sup_nat_o @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 23.31/6.56  thf(137,axiom,((is_empty_nat = (^ [A:set_nat]: (A = bot_bot_set_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_223_Set_Ois__empty__def)).
% 23.31/6.56  thf(879,plain,(((is_empty_nat) = (^ [A:set_nat]: (A = bot_bot_set_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 23.31/6.56  thf(130,axiom,((! [A:nat]: (type_M1734147655le_typ @ A @ type_M405566558_subst))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_234_new__tv__id__subst)).
% 23.31/6.56  thf(852,plain,((! [A:nat]: (type_M1734147655le_typ @ A @ (type_M405566558_subst)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 23.31/6.56  thf(141,axiom,((! [A:nat,B:(set_nat > nat),C:set_nat,D:set_nat]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_133_order__less__subst1)).
% 23.31/6.56  thf(889,plain,((! [A:nat,B:(set_nat > nat),C:set_nat,D:set_nat]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 23.31/6.56  thf(22,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_If_3_1_If_001t__Type____Mirabelle____lczmhmumaa__Otyp_T)).
% 23.31/6.56  thf(461,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 23.31/6.56  thf(32,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => ((ord_less_set_nat @ B @ C) => (ord_less_set_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_233_psubset__trans)).
% 23.31/6.56  thf(493,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => ((ord_less_set_nat @ B @ C) => (ord_less_set_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 23.31/6.56  thf(274,axiom,((! [A:nat,B:nat,C:set_nat]: ((member_nat @ A @ (insert_nat @ B @ C)) = ((A = B) | (member_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_50_insert__iff)).
% 23.31/6.56  thf(1407,plain,((! [A:nat,B:nat,C:set_nat]: ((member_nat @ A @ (insert_nat @ B @ C)) = ((A = B) | (member_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 23.31/6.56  thf(45,axiom,((the_elem_nat = (^ [A:set_nat]: (the_nat @ (^ [B:nat]: (A = (insert_nat @ B @ bot_bot_set_nat))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_224_the__elem__def)).
% 23.31/6.56  thf(551,plain,(((the_elem_nat) = (^ [A:set_nat]: (the_nat @ (^ [B:nat]: (A = (insert_nat @ B @ bot_bot_set_nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 23.31/6.56  thf(243,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_181_dual__order_Oasym)).
% 23.31/6.56  thf(1291,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 23.31/6.56  thf(39,axiom,((! [A:nat,B:(nat > $o)]: ((insert_nat @ A @ (collect_nat @ B)) = (collect_nat @ (^ [C:nat]: ((C != A) => (B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_84_insert__Collect)).
% 23.31/6.56  thf(522,plain,((! [A:nat,B:(nat > $o)]: ((insert_nat @ A @ (collect_nat @ (B))) = (collect_nat @ (^ [C:nat]: ((~ (C = A)) => (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 23.31/6.56  thf(123,axiom,((! [A:nat]: ((type_M326705277scheme @ (type_M2048935292e_BVar @ A)) = (insert_nat @ A @ bot_bot_set_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_95_bound__tv__type__scheme_Osimps_I2_J)).
% 23.31/6.56  thf(830,plain,((! [A:nat]: ((type_M326705277scheme @ (type_M2048935292e_BVar @ A)) = (insert_nat @ A @ bot_bot_set_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 23.31/6.56  thf(89,axiom,((! [A:nat]: ((the_elem_nat @ (insert_nat @ A @ bot_bot_set_nat)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_93_the__elem__eq)).
% 23.31/6.56  thf(697,plain,((! [A:nat]: ((the_elem_nat @ (insert_nat @ A @ bot_bot_set_nat)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 23.31/6.56  thf(135,axiom,((! [A:set_nat,B:set_nat,C:$o]: ((ord_less_set_nat @ A @ B) => ((ord_less_set_nat @ B @ A) => (C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_193_less__imp__triv)).
% 23.31/6.56  thf(874,plain,((! [A:set_nat,B:set_nat,C:$o]: ((ord_less_set_nat @ A @ B) => ((ord_less_set_nat @ B @ A) => (C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 23.31/6.56  thf(237,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (ord_less_set_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_203_less__imp__not__less)).
% 23.31/6.56  thf(1270,plain,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (ord_less_set_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 23.31/6.56  thf(74,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (~ (ord_less_nat_o @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_186_less__not__sym)).
% 23.31/6.56  thf(650,plain,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (~ (ord_less_nat_o @ (B) @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 23.31/6.56  thf(64,axiom,((! [A:(nat > $o),B:(nat > $o),C:((nat > $o) > (nat > $o)),D:(nat > $o)]: ((ord_less_nat_o @ A @ B) => ((ord_less_nat_o @ (C @ B) @ D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ E @ F) => (ord_less_nat_o @ (C @ E) @ (C @ F)))) => (ord_less_nat_o @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_149_order__less__subst2)).
% 23.31/6.56  thf(615,plain,((! [A:(nat > $o),B:(nat > $o),C:((nat > $o) > (nat > $o)),D:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => ((ord_less_nat_o @ (C @ B) @ (D)) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ (E) @ (F)) => (ord_less_nat_o @ (C @ E) @ (C @ F)))) => (ord_less_nat_o @ (C @ A) @ (D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 23.31/6.56  thf(202,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (ord_less_set_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_163_less__asym_H)).
% 23.31/6.56  thf(1121,plain,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (ord_less_set_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 23.31/6.56  thf(280,axiom,((! [A:set_nat,B:nat]: ((A = bot_bot_set_nat) => (~ (member_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_67_equals0D)).
% 23.31/6.56  thf(1425,plain,((! [A:set_nat,B:nat]: ((A = bot_bot_set_nat) => (~ (member_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[280])).
% 23.31/6.56  thf(5,axiom,((! [A:type_Mirabelle_typ,B:list_T1103309005le_typ]: ((cons_T363929085le_typ @ A @ B) != B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_71_not__Cons__self2)).
% 23.31/6.56  thf(356,plain,((! [A:type_Mirabelle_typ,B:list_T1103309005le_typ]: ~ ((cons_T363929085le_typ @ A @ B) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 23.31/6.56  thf(272,axiom,((! [A:nat,B:set_nat,C:set_nat]: (((~ (member_nat @ A @ B)) => (member_nat @ A @ C)) => (member_nat @ A @ (sup_sup_set_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_252_UnCI)).
% 23.31/6.56  thf(1397,plain,((! [A:nat,B:set_nat,C:set_nat]: (((~ (member_nat @ A @ B)) => (member_nat @ A @ C)) => (member_nat @ A @ (sup_sup_set_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[272])).
% 23.31/6.56  thf(108,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ A @ B) => ((ord_less_nat_o @ B @ C) => (ord_less_nat_o @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_167_less__trans)).
% 23.31/6.56  thf(783,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => ((ord_less_nat_o @ (B) @ (C)) => (ord_less_nat_o @ (A) @ (C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 23.31/6.56  thf(201,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (ord_less_nat_o @ A @ (sup_sup_nat_o @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_309_less__supI1)).
% 23.31/6.56  thf(1118,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (ord_less_nat_o @ (A) @ (sup_sup_nat_o @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 23.31/6.56  thf(254,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((bot_bot_nat_o = (sup_sup_nat_o @ A @ B)) = ((A = bot_bot_nat_o) & (B = bot_bot_nat_o))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_297_sup__bot_Oneutr__eq__iff)).
% 23.31/6.56  thf(1329,plain,((! [A:(nat > $o),B:(nat > $o)]: (((bot_bot_nat_o) = (sup_sup_nat_o @ A @ B)) = (((A) = (bot_bot_nat_o)) & ((B) = (bot_bot_nat_o)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 23.31/6.56  thf(210,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_215_dual__order_Ostrict__implies__not__eq)).
% 23.31/6.56  thf(1160,plain,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 23.31/6.56  thf(191,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_123_ord__eq__less__subst)).
% 23.31/6.56  thf(1082,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 23.31/6.56  thf(152,axiom,((! [A:(nat > $o),B:nat]: (((A @ B) => ((collect_nat @ (^ [C:nat]: ((C = B) & (A @ C)))) = (insert_nat @ B @ bot_bot_set_nat))) & ((~ (A @ B)) => ((collect_nat @ (^ [C:nat]: ((C = B) & (A @ C)))) = bot_bot_set_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_92_Collect__conv__if)).
% 23.31/6.56  thf(933,plain,((! [A:(nat > $o),B:nat]: (((A @ B) => ((collect_nat @ (^ [C:nat]: ((C = B) & (A @ C)))) = (insert_nat @ B @ bot_bot_set_nat))) & ((~ (A @ B)) => ((collect_nat @ (^ [C:nat]: ((C = B) & (A @ C)))) = bot_bot_set_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 23.31/6.56  thf(100,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_nat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_188_less__induct)).
% 23.31/6.56  thf(753,plain,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_nat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 23.31/6.56  thf(42,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_214_order_Ostrict__implies__not__eq)).
% 23.31/6.56  thf(537,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 23.31/6.56  thf(72,axiom,((! [A:(nat > $o),B:((nat > $o) > (nat > $o)),C:(nat > $o),D:(nat > $o)]: ((ord_less_nat_o @ A @ (B @ C)) => ((ord_less_nat_o @ C @ D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ E @ F) => (ord_less_nat_o @ (B @ E) @ (B @ F)))) => (ord_less_nat_o @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_140_order__less__subst1)).
% 23.31/6.56  thf(642,plain,((! [A:(nat > $o),B:((nat > $o) > (nat > $o)),C:(nat > $o),D:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B @ C)) => ((ord_less_nat_o @ (C) @ (D)) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ (E) @ (F)) => (ord_less_nat_o @ (B @ E) @ (B @ F)))) => (ord_less_nat_o @ (A) @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 23.31/6.56  thf(70,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (ord_less_set_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_154_order_Oasym)).
% 23.31/6.56  thf(637,plain,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (ord_less_set_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 23.31/6.56  thf(209,axiom,((! [A:(nat > $o),B:(nat > $o),C:((nat > $o) > nat),D:nat]: ((ord_less_nat_o @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_147_order__less__subst2)).
% 23.31/6.56  thf(1155,plain,((! [A:(nat > $o),B:(nat > $o),C:((nat > $o) > nat),D:nat]: ((ord_less_nat_o @ (A) @ (B)) => ((ord_less_nat @ (C @ (B)) @ D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ (E) @ (F)) => (ord_less_nat @ (C @ (E)) @ (C @ (F))))) => (ord_less_nat @ (C @ (A)) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 23.31/6.56  thf(85,axiom,((! [A:type_Mirabelle_typ,B:list_T1103309005le_typ]: ((type_M510873837le_typ @ (cons_T363929085le_typ @ A @ B)) = (sup_sup_set_nat @ (type_M49385309le_typ @ A) @ (type_M510873837le_typ @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_286_free__tv__list_Osimps_I2_J)).
% 23.31/6.56  thf(686,plain,((! [A:type_Mirabelle_typ,B:list_T1103309005le_typ]: ((type_M510873837le_typ @ (cons_T363929085le_typ @ A @ B)) = (sup_sup_set_nat @ (type_M49385309le_typ @ A) @ (type_M510873837le_typ @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 23.31/6.56  thf(28,axiom,((! [A:set_nat,B:(set_nat > set_nat),C:set_nat,D:set_nat]: ((A = (B @ C)) => ((ord_less_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_set_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_118_ord__eq__less__subst)).
% 23.31/6.56  thf(476,plain,((! [A:set_nat,B:(set_nat > set_nat),C:set_nat,D:set_nat]: ((A = (B @ C)) => ((ord_less_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_set_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 23.31/6.56  thf(180,axiom,((! [A:(nat > $o)]: ((sup_sup_nat_o @ bot_bot_nat_o @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_299_sup__bot_Oleft__neutral)).
% 23.31/6.56  thf(1039,plain,((! [A:(nat > $o)]: ((sup_sup_nat_o @ bot_bot_nat_o @ A) = (A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 23.31/6.56  thf(160,axiom,((! [A:(nat > type_Mirabelle_typ),B:list_n396811828le_typ]: ((type_M513401740le_typ @ (cons_n499085924le_typ @ A @ B)) = (sup_sup_set_nat @ (type_M772783356le_typ @ A) @ (type_M513401740le_typ @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_277_bound__tv__list_Osimps_I2_J)).
% 23.31/6.56  thf(970,plain,((! [A:(nat > type_Mirabelle_typ),B:list_n396811828le_typ]: ((type_M513401740le_typ @ (cons_n499085924le_typ @ (A) @ B)) = (sup_sup_set_nat @ (type_M772783356le_typ @ (A)) @ (type_M513401740le_typ @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 23.31/6.56  thf(125,axiom,((! [A:nat]: ((collect_nat @ (^ [B:nat]: (B = A))) = (insert_nat @ A @ bot_bot_set_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_46_singleton__conv)).
% 23.31/6.56  thf(837,plain,((! [A:nat]: ((collect_nat @ (^ [B:nat]: (B = A))) = (insert_nat @ A @ bot_bot_set_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 23.31/6.56  thf(231,axiom,((! [A:(nat > $o),B:(nat > $o)]: (((sup_sup_nat_o @ A @ B) = bot_bot_nat_o) = ((A = bot_bot_nat_o) & (B = bot_bot_nat_o))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_301_sup__bot_Oeq__neutr__iff)).
% 23.31/6.56  thf(1249,plain,((! [A:(nat > $o),B:(nat > $o)]: (((sup_sup_nat_o @ A @ B) = (bot_bot_nat_o)) = (((A) = (bot_bot_nat_o)) & ((B) = (bot_bot_nat_o)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 23.31/6.56  thf(245,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_199_dual__order_Oirrefl)).
% 23.31/6.56  thf(1297,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 23.31/6.56  thf(76,axiom,((! [A:set_nat,B:((nat > $o) > set_nat),C:(nat > $o),D:(nat > $o)]: ((A = (B @ C)) => ((ord_less_nat_o @ C @ D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ E @ F) => (ord_less_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_set_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_121_ord__eq__less__subst)).
% 23.31/6.56  thf(654,plain,((! [A:set_nat,B:((nat > $o) > set_nat),C:(nat > $o),D:(nat > $o)]: ((A = (B @ (C))) => ((ord_less_nat_o @ (C) @ (D)) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ (E) @ (F)) => (ord_less_set_nat @ (B @ (E)) @ (B @ (F))))) => (ord_less_set_nat @ A @ (B @ (D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 23.31/6.56  thf(218,axiom,((! [A:(nat > $o),B:(set_nat > (nat > $o)),C:set_nat,D:set_nat]: ((ord_less_nat_o @ A @ (B @ C)) => ((ord_less_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat_o @ (B @ E) @ (B @ F)))) => (ord_less_nat_o @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_139_order__less__subst1)).
% 23.31/6.56  thf(1192,plain,((! [A:(nat > $o),B:(set_nat > (nat > $o)),C:set_nat,D:set_nat]: ((ord_less_nat_o @ (A) @ (B @ C)) => ((ord_less_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat_o @ (B @ E) @ (B @ F)))) => (ord_less_nat_o @ (A) @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 23.31/6.56  thf(170,axiom,((! [A:nat,B:nat]: (((insert_nat @ A @ bot_bot_set_nat) = (insert_nat @ B @ bot_bot_set_nat)) => (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_86_singleton__inject)).
% 23.31/6.56  thf(1002,plain,((! [A:nat,B:nat]: (((insert_nat @ A @ bot_bot_set_nat) = (insert_nat @ B @ bot_bot_set_nat)) => (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 23.31/6.56  thf(51,axiom,((! [A:(nat > $o),B:(nat > $o),C:((nat > $o) > set_nat),D:set_nat]: ((ord_less_nat_o @ A @ B) => ((ord_less_set_nat @ (C @ B) @ D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ E @ F) => (ord_less_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_set_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_148_order__less__subst2)).
% 23.31/6.56  thf(569,plain,((! [A:(nat > $o),B:(nat > $o),C:((nat > $o) > set_nat),D:set_nat]: ((ord_less_nat_o @ (A) @ (B)) => ((ord_less_set_nat @ (C @ (B)) @ D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ (E) @ (F)) => (ord_less_set_nat @ (C @ (E)) @ (C @ (F))))) => (ord_less_set_nat @ (C @ (A)) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 23.31/6.56  thf(107,axiom,((! [A:nat,B:type_Mirabelle_typ,C:type_Mirabelle_typ]: ((type_Mirabelle_TVar @ A) != (type_Mirabelle_Fun @ B @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_238_typ_Odistinct_I1_J)).
% 23.31/6.56  thf(779,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)],[107])).
% 23.31/6.56  thf(7,axiom,((! [A:nat]: ((the_nat @ (^ [B:nat]: (B = A))) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_240_the__eq__trivial)).
% 23.31/6.56  thf(371,plain,((! [A:nat]: ((the_nat @ (^ [B:nat]: (B = A))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 23.31/6.56  thf(271,axiom,((! [A:(nat > type_Mirabelle_typ),B:type_Mirabelle_typ,C:(nat > type_Mirabelle_typ),D:nat]: (((type_M784671311le_typ @ A @ B) = (type_M784671311le_typ @ C @ B)) => ((member_nat @ D @ (type_M49385309le_typ @ B)) => ((A @ D) = (C @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_33_eq__subst__te__eq__free)).
% 23.31/6.56  thf(1393,plain,((! [A:(nat > type_Mirabelle_typ),B:type_Mirabelle_typ,C:(nat > type_Mirabelle_typ),D:nat]: (((type_M784671311le_typ @ (A) @ B) = (type_M784671311le_typ @ (C) @ B)) => ((member_nat @ D @ (type_M49385309le_typ @ B)) => ((A @ D) = (C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 23.31/6.56  thf(308,axiom,((ord_less_set_nat = (^ [A:set_nat,B:set_nat]: (ord_less_nat_o @ (^ [C:nat]: (member_nat @ C @ A)) @ (^ [C:nat]: (member_nat @ C @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_232_less__set__def)).
% 23.31/6.56  thf(1525,plain,(((ord_less_set_nat) = (^ [A:set_nat,B:set_nat]: (ord_less_nat_o @ (^ [C:nat]: (member_nat @ C @ A)) @ (^ [C:nat]: (member_nat @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[308])).
% 23.31/6.56  thf(73,axiom,((! [A:nat,B:list_n396811828le_typ,C:list_l865305402le_typ]: ((type_M2086816231le_typ @ A @ (cons_l1800589546le_typ @ B @ C)) = ((type_M244876119le_typ @ A @ B) & (type_M2086816231le_typ @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_19_new__tv__Cons)).
% 23.31/6.56  thf(647,plain,((! [A:nat,B:list_n396811828le_typ,C:list_l865305402le_typ]: ((type_M2086816231le_typ @ A @ (cons_l1800589546le_typ @ B @ C)) = ((type_M244876119le_typ @ A @ B) & (type_M2086816231le_typ @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 23.31/6.56  thf(168,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_187_less__not__sym)).
% 23.31/6.56  thf(997,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 23.31/6.56  thf(310,axiom,((! [A:nat,B:(nat > $o)]: ((member_nat @ A @ (collect_nat @ B)) = (B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_58_mem__Collect__eq)).
% 23.31/6.56  thf(1530,plain,((! [A:nat,B:(nat > $o)]: ((member_nat @ A @ (collect_nat @ (B))) = (B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[310])).
% 23.31/6.56  thf(312,axiom,((! [A:nat,B:type_M1694694083scheme,C:(nat > type_Mirabelle_typ),D:(nat > type_Mirabelle_typ)]: ((type_M1963061490scheme @ A @ B) => ((type_M1690910139scheme @ (^ [E:nat]: (if_Typ1169047309le_typ @ (ord_less_nat @ E @ A) @ (C @ E) @ (D @ E))) @ B) = (type_M1690910139scheme @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_16_new__if__subst__type__scheme)).
% 23.31/6.56  thf(1539,plain,((! [A:nat,B:type_M1694694083scheme,C:(nat > type_Mirabelle_typ),D:(nat > type_Mirabelle_typ)]: ((type_M1963061490scheme @ A @ B) => ((type_M1690910139scheme @ (^ [E:nat]: (if_Typ1169047309le_typ @ (ord_less_nat @ E @ A) @ (C @ E) @ (D @ E))) @ B) = (type_M1690910139scheme @ (C) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[312])).
% 23.31/6.56  thf(286,axiom,((! [A:(nat > type_Mirabelle_typ),B:nat]: ((type_M1690910139scheme @ A @ (type_M2048935292e_BVar @ B)) = (type_M2048935292e_BVar @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_app__subst__type__scheme_Osimps_I2_J)).
% 23.31/6.56  thf(1456,plain,((! [A:(nat > type_Mirabelle_typ),B:nat]: ((type_M1690910139scheme @ (A) @ (type_M2048935292e_BVar @ B)) = (type_M2048935292e_BVar @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[286])).
% 23.31/6.56  thf(267,axiom,((! [A:nat,B:set_nat,C:set_nat]: ((member_nat @ A @ B) => (member_nat @ A @ (sup_sup_set_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_260_UnI2)).
% 23.31/6.56  thf(1382,plain,((! [A:nat,B:set_nat,C:set_nat]: ((member_nat @ A @ B) => (member_nat @ A @ (sup_sup_set_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 23.31/6.56  thf(111,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_162_less__asym)).
% 23.31/6.56  thf(792,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 23.31/6.56  thf(6,axiom,((! [A:(nat > $o),B:nat]: ((A @ B) => ((! [C:nat]: ((A @ C) => (C = B))) => (A @ (the_nat @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_243_theI)).
% 23.31/6.56  thf(360,plain,((! [A:(nat > $o),B:nat]: ((A @ B) => ((! [C:nat]: ((A @ C) => (C = B))) => (A @ (the_nat @ (A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 23.31/6.56  thf(115,axiom,((! [A:set_nat]: ((A != bot_bot_set_nat) = (ord_less_set_nat @ bot_bot_set_nat @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_98_bot_Onot__eq__extremum)).
% 23.31/6.56  thf(805,plain,((! [A:set_nat]: ((~ (A = bot_bot_set_nat)) = (ord_less_set_nat @ bot_bot_set_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 23.31/6.56  thf(37,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => ((B = C) => (ord_less_set_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_176_ord__less__eq__trans)).
% 23.31/6.56  thf(508,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => ((B = C) => (ord_less_set_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 23.31/6.56  thf(43,axiom,((! [A:(nat > $o),B:(nat > (nat > $o)),C:nat,D:nat]: ((ord_less_nat_o @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat_o @ (B @ E) @ (B @ F)))) => (ord_less_nat_o @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_138_order__less__subst1)).
% 23.31/6.56  thf(541,plain,((! [A:(nat > $o),B:(nat > (nat > $o)),C:nat,D:nat]: ((ord_less_nat_o @ (A) @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat_o @ (B @ E) @ (B @ F)))) => (ord_less_nat_o @ (A) @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 23.31/6.56  thf(216,axiom,((! [A:nat,B:nat]: (type_M1963061490scheme @ A @ (type_M2048935292e_BVar @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_28_new__tv__BVar)).
% 23.31/6.56  thf(1187,plain,((! [A:nat,B:nat]: (type_M1963061490scheme @ A @ (type_M2048935292e_BVar @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 23.31/6.56  thf(102,axiom,((sup_sup_set_nat = (^ [A:set_nat,B:set_nat]: (sup_sup_set_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_266_Un__commute)).
% 23.31/6.56  thf(765,plain,(((sup_sup_set_nat) = (^ [A:set_nat,B:set_nat]: (sup_sup_set_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 23.31/6.56  thf(184,axiom,((! [A:(nat > $o),B:(nat > $o),C:((nat > $o) > nat),D:nat]: ((ord_less_nat_o @ A @ B) => (((C @ B) = D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_129_ord__less__eq__subst)).
% 23.31/6.56  thf(1054,plain,((! [A:(nat > $o),B:(nat > $o),C:((nat > $o) > nat),D:nat]: ((ord_less_nat_o @ (A) @ (B)) => (((C @ (B)) = D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ (E) @ (F)) => (ord_less_nat @ (C @ (E)) @ (C @ (F))))) => (ord_less_nat @ (C @ (A)) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 23.31/6.56  thf(289,axiom,((! [A:nat,B:set_nat,C:nat,D:set_nat]: ((~ (member_nat @ A @ B)) => ((~ (member_nat @ C @ D)) => (((insert_nat @ A @ B) = (insert_nat @ C @ D)) = (((A = C) => (B = D)) & ((A != C) => (? [E:set_nat]: ((B = (insert_nat @ C @ E)) & ~ (member_nat @ C @ E) & (D = (insert_nat @ A @ E)) & ~ (member_nat @ A @ E)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_76_insert__eq__iff)).
% 23.31/6.56  thf(1466,plain,((! [A:nat,B:set_nat,C:nat,D:set_nat]: ((~ (member_nat @ A @ B)) => ((~ (member_nat @ C @ D)) => (((insert_nat @ A @ B) = (insert_nat @ C @ D)) = (((A = C) => (B = D)) & ((~ (A = C)) => (? [E:set_nat]: ((B = (insert_nat @ C @ E)) & ~ (member_nat @ C @ E) & (D = (insert_nat @ A @ E)) & ~ (member_nat @ A @ E)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[289])).
% 23.31/6.56  thf(187,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (ord_less_nat_o @ A @ (sup_sup_nat_o @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_321_sup_Ostrict__coboundedI1)).
% 23.31/6.56  thf(1071,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (ord_less_nat_o @ (A) @ (sup_sup_nat_o @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 23.31/6.56  thf(177,axiom,((! [A:set_nat,B:set_nat,C:(set_nat > nat),D:nat]: ((ord_less_set_nat @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_144_order__less__subst2)).
% 23.31/6.56  thf(1026,plain,((! [A:set_nat,B:set_nat,C:(set_nat > nat),D:nat]: ((ord_less_set_nat @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 23.31/6.56  thf(212,axiom,((! [A:(nat > $o),B:((nat > $o) > (nat > $o)),C:(nat > $o),D:(nat > $o)]: ((A = (B @ C)) => ((ord_less_nat_o @ C @ D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ E @ F) => (ord_less_nat_o @ (B @ E) @ (B @ F)))) => (ord_less_nat_o @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_122_ord__eq__less__subst)).
% 23.31/6.56  thf(1167,plain,((! [A:(nat > $o),B:((nat > $o) > (nat > $o)),C:(nat > $o),D:(nat > $o)]: (((A) = (B @ C)) => ((ord_less_nat_o @ (C) @ (D)) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ (E) @ (F)) => (ord_less_nat_o @ (B @ E) @ (B @ F)))) => (ord_less_nat_o @ (A) @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 23.31/6.56  thf(105,axiom,((! [A:nat,B:set_nat,C:set_nat]: ((sup_sup_set_nat @ (insert_nat @ A @ B) @ C) = (insert_nat @ A @ (sup_sup_set_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_255_Un__insert__left)).
% 23.31/6.56  thf(773,plain,((! [A:nat,B:set_nat,C:set_nat]: ((sup_sup_set_nat @ (insert_nat @ A @ B) @ C) = (insert_nat @ A @ (sup_sup_set_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 23.31/6.56  thf(112,axiom,((! [A:type_M1694694083scheme,B:list_T247403987scheme]: ((cons_T633159821scheme @ A @ B) != B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_69_not__Cons__self2)).
% 23.31/6.56  thf(794,plain,((! [A:type_M1694694083scheme,B:list_T247403987scheme]: ~ ((cons_T633159821scheme @ A @ B) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 23.31/6.56  thf(240,axiom,((! [A:nat,B:((nat > $o) > nat),C:(nat > $o),D:(nat > $o)]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_nat_o @ C @ D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_134_order__less__subst1)).
% 23.31/6.56  thf(1278,plain,((! [A:nat,B:((nat > $o) > nat),C:(nat > $o),D:(nat > $o)]: ((ord_less_nat @ A @ (B @ (C))) => ((ord_less_nat_o @ (C) @ (D)) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ (E) @ (F)) => (ord_less_nat @ (B @ (E)) @ (B @ (F))))) => (ord_less_nat @ A @ (B @ (D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 23.31/6.56  thf(99,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => (ord_less_set_nat @ A @ (sup_sup_set_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_322_sup_Ostrict__coboundedI1)).
% 23.31/6.56  thf(750,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => (ord_less_set_nat @ A @ (sup_sup_set_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 23.31/6.56  thf(38,axiom,((! [A:set_nat,B:set_nat,C:(set_nat > nat),D:nat]: ((ord_less_set_nat @ A @ B) => (((C @ B) = D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_126_ord__less__eq__subst)).
% 23.31/6.56  thf(513,plain,((! [A:set_nat,B:set_nat,C:(set_nat > nat),D:nat]: ((ord_less_set_nat @ A @ B) => (((C @ B) = D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 23.31/6.56  thf(294,axiom,((! [A:nat,B:set_nat]: (member_nat @ A @ (insert_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_81_insertI1)).
% 23.31/6.56  thf(1483,plain,((! [A:nat,B:set_nat]: (member_nat @ A @ (insert_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[294])).
% 23.31/6.56  thf(86,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((sup_sup_set_nat @ (sup_sup_set_nat @ A @ B) @ C) = (sup_sup_set_nat @ A @ (sup_sup_set_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_264_Un__assoc)).
% 23.31/6.56  thf(689,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((sup_sup_set_nat @ (sup_sup_set_nat @ A @ B) @ C) = (sup_sup_set_nat @ A @ (sup_sup_set_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 23.31/6.56  thf(17,axiom,((! [A:(nat > $o),B:nat]: ((A = ((=) @ nat @ B)) => ((the_nat @ A) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_327_Nitpick_OThe__psimp)).
% 23.31/6.56  thf(444,plain,((! [A:(nat > $o),B:nat]: (((A) = ((=) @ nat @ B)) => ((the_nat @ (A)) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 23.31/6.56  thf(223,axiom,((semila1414375521_nat_o @ sup_sup_nat_o @ bot_bot_nat_o)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_329_sup__bot_Osemilattice__neutr__axioms)).
% 23.31/6.56  thf(1219,plain,((semila1414375521_nat_o @ (sup_sup_nat_o) @ (bot_bot_nat_o))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 23.31/6.56  thf(121,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = ((ord_less_nat @ B @ A) | (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_211_not__less__iff__gr__or__eq)).
% 23.31/6.56  thf(824,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = ((ord_less_nat @ B @ A) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 23.31/6.56  thf(55,axiom,((! [A:(nat > $o)]: ((bot_bot_set_nat = (collect_nat @ A)) = (! [B:nat]: ~ (A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_63_empty__Collect__eq)).
% 23.31/6.56  thf(584,plain,((! [A:(nat > $o)]: ((bot_bot_set_nat = (collect_nat @ (A))) = (! [B:nat]: ~ (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 23.31/6.56  thf(120,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_150_order__less__subst2)).
% 23.31/6.56  thf(819,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 23.31/6.56  thf(88,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => (ord_less_set_nat @ A @ (sup_sup_set_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_310_less__supI1)).
% 23.31/6.56  thf(694,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => (ord_less_set_nat @ A @ (sup_sup_set_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 23.31/6.56  thf(97,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B) | (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_169_less__linear)).
% 23.31/6.56  thf(743,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B) | (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 23.31/6.56  thf(53,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_157_less__imp__neq)).
% 23.31/6.56  thf(577,plain,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 23.31/6.56  thf(158,axiom,((! [A:type_Mirabelle_typ,B:list_T1103309005le_typ]: ((type_M1539052445le_typ @ (cons_T363929085le_typ @ A @ B)) = (sup_sup_set_nat @ (type_M801073677le_typ @ A) @ (type_M1539052445le_typ @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_276_bound__tv__list_Osimps_I2_J)).
% 23.31/6.56  thf(958,plain,((! [A:type_Mirabelle_typ,B:list_T1103309005le_typ]: ((type_M1539052445le_typ @ (cons_T363929085le_typ @ A @ B)) = (sup_sup_set_nat @ (type_M801073677le_typ @ A) @ (type_M1539052445le_typ @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 23.31/6.56  thf(306,axiom,((type_M1734147655le_typ = (^ [A:nat,B:(nat > type_Mirabelle_typ)]: ! [C:nat]: ((member_nat @ C @ (type_M1715972684le_typ @ B)) => (ord_less_nat @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_45_new__tv__def)).
% 23.31/6.56  thf(1520,plain,(((type_M1734147655le_typ) = (^ [A:nat,B:(nat > type_Mirabelle_typ)]: ! [C:nat]: ((member_nat @ C @ (type_M1715972684le_typ @ B)) => (ord_less_nat @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[306])).
% 23.31/6.56  thf(296,axiom,((! [A:set_nat]: ((! [B:nat]: ~ (member_nat @ B @ A)) => (A = bot_bot_set_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_66_equals0I)).
% 23.31/6.56  thf(1488,plain,((! [A:set_nat]: ((! [B:nat]: ~ (member_nat @ B @ A)) => (A = bot_bot_set_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[296])).
% 23.31/6.56  thf(127,axiom,((! [A:nat,B:type_Mirabelle_typ,C:type_Mirabelle_typ]: ((type_M1211611096le_typ @ A @ (type_Mirabelle_Fun @ B @ C)) = ((type_M1211611096le_typ @ A @ B) & (type_M1211611096le_typ @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_229_new__tv__Fun)).
% 23.31/6.56  thf(843,plain,((! [A:nat,B:type_Mirabelle_typ,C:type_Mirabelle_typ]: ((type_M1211611096le_typ @ A @ (type_Mirabelle_Fun @ B @ C)) = ((type_M1211611096le_typ @ A @ B) & (type_M1211611096le_typ @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 23.31/6.56  thf(204,axiom,((((?) @ nat) = (^ [A:(nat > $o)]: ? [B:nat]: ((A @ B) & ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_206_exists__least__iff)).
% 23.31/6.56  thf(1125,plain,((((?) @ nat) = (^ [A:(nat > $o)]: ? [B:nat]: ((A @ B) & ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 23.31/6.56  thf(34,axiom,((! [A:set_nat]: ((sup_sup_set_nat @ bot_bot_set_nat @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_271_Un__empty__left)).
% 23.31/6.56  thf(498,plain,((! [A:set_nat]: ((sup_sup_set_nat @ bot_bot_set_nat @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 23.31/6.56  thf(197,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (~ (ord_less_nat_o @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_161_less__asym)).
% 23.31/6.56  thf(1107,plain,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (~ (ord_less_nat_o @ (B) @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 23.31/6.56  thf(255,axiom,((! [A:(nat > $o),B:(nat > $o),C:((nat > $o) > set_nat),D:set_nat]: ((ord_less_nat_o @ A @ B) => (((C @ B) = D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ E @ F) => (ord_less_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_set_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_130_ord__less__eq__subst)).
% 23.31/6.56  thf(1332,plain,((! [A:(nat > $o),B:(nat > $o),C:((nat > $o) > set_nat),D:set_nat]: ((ord_less_nat_o @ (A) @ (B)) => (((C @ (B)) = D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ (E) @ (F)) => (ord_less_set_nat @ (C @ (E)) @ (C @ (F))))) => (ord_less_set_nat @ (C @ (A)) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 23.31/6.56  thf(24,axiom,((! [A:set_nat]: ((sup_sup_set_nat @ A @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_265_Un__absorb)).
% 23.31/6.56  thf(466,plain,((! [A:set_nat]: ((sup_sup_set_nat @ A @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 23.31/6.56  thf(80,axiom,((! [A:set_nat]: ((sup_sup_set_nat @ bot_bot_set_nat @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_292_sup__bot__left)).
% 23.31/6.56  thf(672,plain,((! [A:set_nat]: ((sup_sup_set_nat @ bot_bot_set_nat @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 23.31/6.56  thf(61,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((A = B) => ((ord_less_nat_o @ B @ C) => (ord_less_nat_o @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_174_ord__eq__less__trans)).
% 23.31/6.56  thf(604,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: (((A) = (B)) => ((ord_less_nat_o @ (B) @ (C)) => (ord_less_nat_o @ (A) @ (C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 23.31/6.56  thf(144,axiom,((bot_bot_set_nat = (collect_nat @ bot_bot_nat_o))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_110_bot__set__def)).
% 23.31/6.56  thf(900,plain,((bot_bot_set_nat = (collect_nat @ (bot_bot_nat_o)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 23.31/6.56  thf(258,axiom,((! [A:nat]: (member_nat @ A @ (insert_nat @ A @ bot_bot_set_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_48_singletonI)).
% 23.31/6.56  thf(1349,plain,((! [A:nat]: (member_nat @ A @ (insert_nat @ A @ bot_bot_set_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 23.31/6.56  thf(297,axiom,((type_M263553000le_typ = (^ [A:nat,B:list_T1103309005le_typ]: ! [C:nat]: ((member_nat @ C @ (type_M510873837le_typ @ B)) => (ord_less_nat @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_41_new__tv__def)).
% 23.31/6.56  thf(1492,plain,(((type_M263553000le_typ) = (^ [A:nat,B:list_T1103309005le_typ]: ! [C:nat]: ((member_nat @ C @ (type_M510873837le_typ @ B)) => (ord_less_nat @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[297])).
% 23.31/6.56  thf(19,axiom,((! [A:(nat > type_Mirabelle_typ),B:list_n396811828le_typ]: ((cons_n499085924le_typ @ A @ B) != B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_72_not__Cons__self2)).
% 23.31/6.56  thf(451,plain,((! [A:(nat > type_Mirabelle_typ),B:list_n396811828le_typ]: ~ ((cons_n499085924le_typ @ (A) @ B) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 23.31/6.56  thf(321,axiom,((! [A:set_nat,B:(nat > $o),C:$o,D:set_nat]: (((! [E:nat]: ((member_nat @ E @ A) => (B @ E))) => (C)) => ((! [E:nat]: ((member_nat @ E @ (sup_sup_set_nat @ A @ D)) => (B @ E))) => (C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_257_weaken__asm__Un)).
% 23.31/6.56  thf(1571,plain,((! [A:set_nat,B:(nat > $o),C:$o,D:set_nat]: (((! [E:nat]: ((member_nat @ E @ A) => (B @ E))) => (C)) => ((! [E:nat]: ((member_nat @ E @ (sup_sup_set_nat @ A @ D)) => (B @ E))) => (C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[321])).
% 23.31/6.56  thf(132,axiom,((! [A:list_T247403987scheme,B:list_l1334080099scheme]: ((type_M1958029241scheme @ (cons_l1910959773scheme @ A @ B)) = (sup_sup_set_nat @ (type_M141510067scheme @ A) @ (type_M1958029241scheme @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_287_free__tv__list_Osimps_I2_J)).
% 23.31/6.56  thf(863,plain,((! [A:list_T247403987scheme,B:list_l1334080099scheme]: ((type_M1958029241scheme @ (cons_l1910959773scheme @ A @ B)) = (sup_sup_set_nat @ (type_M141510067scheme @ A) @ (type_M1958029241scheme @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 23.31/6.56  thf(173,axiom,((is_singleton_nat = (^ [A:set_nat]: ? [B:nat]: (A = (insert_nat @ B @ bot_bot_set_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_221_is__singleton__def)).
% 23.31/6.56  thf(1011,plain,(((is_singleton_nat) = (^ [A:set_nat]: ? [B:nat]: (A = (insert_nat @ B @ bot_bot_set_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 23.31/6.56  thf(13,axiom,((! [A:list_T247403987scheme,B:list_l1334080099scheme]: ((type_M1496178953scheme @ (cons_l1910959773scheme @ A @ B)) = (sup_sup_set_nat @ (type_M961603331scheme @ A) @ (type_M1496178953scheme @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_278_bound__tv__list_Osimps_I2_J)).
% 23.31/6.56  thf(419,plain,((! [A:list_T247403987scheme,B:list_l1334080099scheme]: ((type_M1496178953scheme @ (cons_l1910959773scheme @ A @ B)) = (sup_sup_set_nat @ (type_M961603331scheme @ A) @ (type_M1496178953scheme @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 23.31/6.56  thf(190,axiom,((bot_bot_set_nat = (collect_nat @ (^ [A:nat]: (($false)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_83_empty__def)).
% 23.31/6.56  thf(1080,plain,((bot_bot_set_nat = (collect_nat @ (^ [A:nat]: (($false)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 23.31/6.56  thf(119,axiom,((! [A:(nat > $o),B:(nat > $o)]: (((sup_sup_nat_o @ A @ B) = bot_bot_nat_o) = ((A = bot_bot_nat_o) & (B = bot_bot_nat_o))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_303_sup__eq__bot__iff)).
% 23.31/6.56  thf(816,plain,((! [A:(nat > $o),B:(nat > $o)]: (((sup_sup_nat_o @ A @ B) = (bot_bot_nat_o)) = (((A) = (bot_bot_nat_o)) & ((B) = (bot_bot_nat_o)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 23.31/6.56  thf(62,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => ((ord_less_set_nat @ B @ C) => (ord_less_set_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_166_less__trans)).
% 23.31/6.56  thf(609,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => ((ord_less_set_nat @ B @ C) => (ord_less_set_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 23.31/6.56  thf(58,axiom,((! [A:nat,B:nat,C:set_nat]: ((insert_nat @ A @ (insert_nat @ B @ C)) = (insert_nat @ B @ (insert_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_75_insert__commute)).
% 23.31/6.56  thf(594,plain,((! [A:nat,B:nat,C:set_nat]: ((insert_nat @ A @ (insert_nat @ B @ C)) = (insert_nat @ B @ (insert_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 23.31/6.56  thf(90,axiom,((ord_less_set_nat = (^ [A:set_nat,B:set_nat]: ((B = (sup_sup_set_nat @ B @ A)) & (B != A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_319_sup_Ostrict__order__iff)).
% 23.31/6.56  thf(700,plain,(((ord_less_set_nat) = (^ [A:set_nat,B:set_nat]: ((B = (sup_sup_set_nat @ B @ A)) & ~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 23.31/6.56  thf(316,axiom,((! [A:nat,B:nat,C:set_nat]: ((member_nat @ A @ (insert_nat @ B @ C)) => ((A != B) => (member_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_82_insertE)).
% 23.31/6.56  thf(1556,plain,((! [A:nat,B:nat,C:set_nat]: ((member_nat @ A @ (insert_nat @ B @ C)) => ((~ (A = B)) => (member_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[316])).
% 23.31/6.56  thf(175,axiom,((insert_nat = (^ [A:nat]: (sup_sup_set_nat @ (collect_nat @ (^ [B:nat]: (B = A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_270_insert__def)).
% 23.31/6.56  thf(1022,plain,(((insert_nat) = (^ [A:nat]: (sup_sup_set_nat @ (collect_nat @ (^ [B:nat]: (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 23.31/6.56  thf(244,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_190_less__imp__not__eq2)).
% 23.31/6.56  thf(1293,plain,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 23.31/6.56  thf(23,axiom,((! [A:list_T247403987scheme,B:list_l1334080099scheme]: ((cons_l1910959773scheme @ A @ B) != B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_70_not__Cons__self2)).
% 23.31/6.56  thf(462,plain,((! [A:list_T247403987scheme,B:list_l1334080099scheme]: ~ ((cons_l1910959773scheme @ A @ B) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 23.31/6.56  thf(199,axiom,((! [A:nat]: ((A != bot_bot_nat) = (ord_less_nat @ bot_bot_nat @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_99_bot_Onot__eq__extremum)).
% 23.31/6.56  thf(1112,plain,((! [A:nat]: ((~ (A = bot_bot_nat)) = (ord_less_nat @ bot_bot_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 23.31/6.56  thf(291,axiom,((! [A:nat]: ((type_M1050318637scheme @ (type_M876316792e_FVar @ A)) = (insert_nat @ A @ bot_bot_set_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_15_free__tv__type__scheme_Osimps_I1_J)).
% 23.31/6.56  thf(1474,plain,((! [A:nat]: ((type_M1050318637scheme @ (type_M876316792e_FVar @ A)) = (insert_nat @ A @ bot_bot_set_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[291])).
% 23.31/6.56  thf(122,axiom,((! [A:nat,B:list_T1103309005le_typ,C:list_l1790670291le_typ]: ((type_M1826376056le_typ @ A @ (cons_l392684675le_typ @ B @ C)) = ((type_M263553000le_typ @ A @ B) & (type_M1826376056le_typ @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_20_new__tv__Cons)).
% 23.31/6.56  thf(827,plain,((! [A:nat,B:list_T1103309005le_typ,C:list_l1790670291le_typ]: ((type_M1826376056le_typ @ A @ (cons_l392684675le_typ @ B @ C)) = ((type_M263553000le_typ @ A @ B) & (type_M1826376056le_typ @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 23.31/6.56  thf(213,axiom,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: (((type_M1006385707scheme @ A) = (type_M1006385707scheme @ B)) => (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_35_mk__scheme__injective)).
% 23.31/6.56  thf(1176,plain,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: (((type_M1006385707scheme @ A) = (type_M1006385707scheme @ B)) => (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 23.31/6.56  thf(49,axiom,((! [A:(nat > $o)]: ((A != bot_bot_nat_o) = (ord_less_nat_o @ bot_bot_nat_o @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_97_bot_Onot__eq__extremum)).
% 23.31/6.56  thf(563,plain,((! [A:(nat > $o)]: ((~ ((A) = (bot_bot_nat_o))) = (ord_less_nat_o @ (bot_bot_nat_o) @ (A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 23.31/6.56  thf(292,axiom,((! [A:nat,B:set_nat,C:set_nat]: ((~ (member_nat @ A @ B)) => ((~ (member_nat @ A @ C)) => (((insert_nat @ A @ B) = (insert_nat @ A @ C)) = (B = C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_78_insert__ident)).
% 23.31/6.56  thf(1477,plain,((! [A:nat,B:set_nat,C:set_nat]: ((~ (member_nat @ A @ B)) => ((~ (member_nat @ A @ C)) => (((insert_nat @ A @ B) = (insert_nat @ A @ C)) = (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[292])).
% 23.31/6.56  thf(195,axiom,((type_M405566558_subst = type_Mirabelle_TVar)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_227_id__subst__def)).
% 23.31/6.56  thf(1102,plain,(((type_M405566558_subst) = (type_Mirabelle_TVar))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 23.31/6.56  thf(36,axiom,((! [A:nat,B:nat,C:$o]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ A) => (C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_195_less__imp__triv)).
% 23.31/6.56  thf(505,plain,((! [A:nat,B:nat,C:$o]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ A) => (C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 23.31/6.56  thf(318,axiom,((! [A:set_nat,B:set_nat]: ((sup_sup_nat_o @ (^ [C:nat]: (member_nat @ C @ A)) @ (^ [C:nat]: (member_nat @ C @ B))) = (^ [C:nat]: (member_nat @ C @ (sup_sup_set_nat @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_307_sup__Un__eq)).
% 23.31/6.56  thf(1562,plain,((! [A:set_nat,B:set_nat]: ((sup_sup_nat_o @ (^ [C:nat]: (member_nat @ C @ A)) @ (^ [C:nat]: (member_nat @ C @ B))) = (^ [C:nat]: (member_nat @ C @ (sup_sup_set_nat @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[318])).
% 23.31/6.56  thf(20,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/sandbox2/benchmark/theBenchmark.p',fact_228_typ_Oinject_I2_J)).
% 23.31/6.56  thf(455,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)],[20])).
% 23.31/6.56  thf(139,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => (ord_less_set_nat @ A @ (sup_sup_set_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_325_sup_Ostrict__coboundedI2)).
% 23.31/6.56  thf(883,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ A @ B) => (ord_less_set_nat @ A @ (sup_sup_set_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 23.31/6.56  thf(10,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((? [C:nat]: ((A @ C) & ! [D:nat]: ((A @ D) => (D = C)))) => ((! [C:nat]: ((A @ C) => (B @ C))) => (B @ (the_nat @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_247_the1I2)).
% 23.31/6.56  thf(394,plain,((! [A:(nat > $o),B:(nat > $o)]: ((? [C:nat]: ((A @ C) & ! [D:nat]: ((A @ D) => (D = C)))) => ((! [C:nat]: ((A @ C) => (B @ C))) => (B @ (the_nat @ (A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 23.31/6.56  thf(163,axiom,((insert_nat = (^ [A:nat]: (sup_sup_set_nat @ (insert_nat @ A @ bot_bot_set_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_275_insert__is__Un)).
% 23.31/6.56  thf(986,plain,(((insert_nat) = (^ [A:nat]: (sup_sup_set_nat @ (insert_nat @ A @ bot_bot_set_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 23.31/6.56  thf(221,axiom,((! [A:(nat > $o),B:(set_nat > (nat > $o)),C:set_nat,D:set_nat]: ((A = (B @ C)) => ((ord_less_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat_o @ (B @ E) @ (B @ F)))) => (ord_less_nat_o @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_119_ord__eq__less__subst)).
% 23.31/6.56  thf(1208,plain,((! [A:(nat > $o),B:(set_nat > (nat > $o)),C:set_nat,D:set_nat]: (((A) = (B @ C)) => ((ord_less_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat_o @ (B @ E) @ (B @ F)))) => (ord_less_nat_o @ (A) @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 23.31/6.56  thf(83,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((sup_sup_set_nat @ A @ (sup_sup_set_nat @ B @ C)) = (sup_sup_set_nat @ B @ (sup_sup_set_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_269_Un__left__commute)).
% 23.31/6.56  thf(680,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((sup_sup_set_nat @ A @ (sup_sup_set_nat @ B @ C)) = (sup_sup_set_nat @ B @ (sup_sup_set_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 23.31/6.56  thf(77,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ (sup_sup_nat_o @ A @ B) @ C) => (~ ((ord_less_nat_o @ A @ C) => (~ (ord_less_nat_o @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_315_sup_Ostrict__boundedE)).
% 23.31/6.56  thf(663,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ (sup_sup_nat_o @ A @ B) @ (C)) => (~ ((ord_less_nat_o @ (A) @ (C)) => (~ (ord_less_nat_o @ (B) @ (C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 23.31/6.56  thf(30,axiom,((! [A:(nat > $o)]: ~ (ord_less_nat_o @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_171_less__irrefl)).
% 23.31/6.56  thf(487,plain,((! [A:(nat > $o)]: ~ (ord_less_nat_o @ (A) @ (A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 23.31/6.56  thf(46,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((A != B) => (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_196_linorder__cases)).
% 23.31/6.56  thf(553,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (A = B)) => (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 23.31/6.56  thf(31,axiom,((! [A:set_nat,B:set_nat]: (((sup_sup_set_nat @ A @ B) = bot_bot_set_nat) = ((A = bot_bot_set_nat) & (B = bot_bot_set_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_304_sup__eq__bot__iff)).
% 23.31/6.56  thf(490,plain,((! [A:set_nat,B:set_nat]: (((sup_sup_set_nat @ A @ B) = bot_bot_set_nat) = ((A = bot_bot_set_nat) & (B = bot_bot_set_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 23.31/6.56  thf(81,axiom,((! [A:nat]: (type_M2064939256scheme @ A @ nil_Ty61485117scheme))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_351_new__tv__Nil)).
% 23.31/6.56  thf(675,plain,((! [A:nat]: (type_M2064939256scheme @ A @ nil_Ty61485117scheme))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 23.31/6.56  thf(150,axiom,((! [A:nat,B:set_nat,C:set_nat]: (((insert_nat @ A @ bot_bot_set_nat) = (sup_sup_set_nat @ B @ C)) = (((B = bot_bot_set_nat) & (C = (insert_nat @ A @ bot_bot_set_nat))) | ((B = (insert_nat @ A @ bot_bot_set_nat)) & (C = bot_bot_set_nat)) | ((B = (insert_nat @ A @ bot_bot_set_nat)) & (C = (insert_nat @ A @ bot_bot_set_nat))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_273_singleton__Un__iff)).
% 23.31/6.56  thf(927,plain,((! [A:nat,B:set_nat,C:set_nat]: (((insert_nat @ A @ bot_bot_set_nat) = (sup_sup_set_nat @ B @ C)) = (((B = bot_bot_set_nat) & (C = (insert_nat @ A @ bot_bot_set_nat))) | ((B = (insert_nat @ A @ bot_bot_set_nat)) & (C = bot_bot_set_nat)) | ((B = (insert_nat @ A @ bot_bot_set_nat)) & (C = (insert_nat @ A @ bot_bot_set_nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 23.31/6.56  thf(8,axiom,((! [A:(nat > $o)]: ((? [B:nat]: ((A @ B) & ! [C:nat]: ((A @ C) => (C = B)))) => (A @ (the_nat @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_244_theI_H)).
% 23.31/6.56  thf(374,plain,((! [A:(nat > $o)]: ((? [B:nat]: ((A @ B) & ! [C:nat]: ((A @ C) => (C = B)))) => (A @ (the_nat @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 23.31/6.56  thf(21,axiom,((! [A:list_T247403987scheme,B:list_l1334080099scheme,C:list_T247403987scheme,D:list_l1334080099scheme]: (((cons_l1910959773scheme @ A @ B) = (cons_l1910959773scheme @ C @ D)) = ((A = C) & (B = D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_53_list_Oinject)).
% 23.31/6.56  thf(458,plain,((! [A:list_T247403987scheme,B:list_l1334080099scheme,C:list_T247403987scheme,D:list_l1334080099scheme]: (((cons_l1910959773scheme @ A @ B) = (cons_l1910959773scheme @ C @ D)) = ((A = C) & (B = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 23.31/6.56  thf(214,axiom,((! [A:(nat > type_Mirabelle_typ),B:type_Mirabelle_typ,C:type_Mirabelle_typ]: ((type_M784671311le_typ @ A @ (type_Mirabelle_Fun @ B @ C)) = (type_Mirabelle_Fun @ (type_M784671311le_typ @ A @ B) @ (type_M784671311le_typ @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_235_app__subst__Fun)).
% 23.31/6.56  thf(1181,plain,((! [A:(nat > type_Mirabelle_typ),B:type_Mirabelle_typ,C:type_Mirabelle_typ]: ((type_M784671311le_typ @ (A) @ (type_Mirabelle_Fun @ B @ C)) = (type_Mirabelle_Fun @ (type_M784671311le_typ @ (A) @ B) @ (type_M784671311le_typ @ (A) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 23.31/6.56  thf(106,axiom,((! [A:nat,B:nat,C:nat,D:nat]: (((insert_nat @ A @ (insert_nat @ B @ bot_bot_set_nat)) = (insert_nat @ C @ (insert_nat @ D @ bot_bot_set_nat))) = (((A = C) & (B = D)) | ((A = D) & (B = C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_88_doubleton__eq__iff)).
% 23.31/6.56  thf(776,plain,((! [A:nat,B:nat,C:nat,D:nat]: (((insert_nat @ A @ (insert_nat @ B @ bot_bot_set_nat)) = (insert_nat @ C @ (insert_nat @ D @ bot_bot_set_nat))) = (((A = C) & (B = D)) | ((A = D) & (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 23.31/6.56  thf(40,axiom,((! [A:set_nat,B:set_nat,C:(set_nat > (nat > $o)),D:(nat > $o)]: ((ord_less_set_nat @ A @ B) => (((C @ B) = D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat_o @ (C @ E) @ (C @ F)))) => (ord_less_nat_o @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_128_ord__less__eq__subst)).
% 23.31/6.56  thf(525,plain,((! [A:set_nat,B:set_nat,C:(set_nat > (nat > $o)),D:(nat > $o)]: ((ord_less_set_nat @ A @ B) => (((C @ B) = (D)) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_nat_o @ (C @ E) @ (C @ F)))) => (ord_less_nat_o @ (C @ A) @ (D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 23.31/6.56  thf(92,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/sandbox2/benchmark/theBenchmark.p',fact_237_typ_Oinduct)).
% 23.31/6.56  thf(705,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)],[92])).
% 23.31/6.56  thf(11,axiom,((! [A:nat]: ((the_nat @ ((=) @ nat @ A)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_239_the__sym__eq__trivial)).
% 23.31/6.56  thf(414,plain,((! [A:nat]: ((the_nat @ ((=) @ nat @ A)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 23.31/6.56  thf(232,axiom,((! [A:nat,B:nat]: (((type_M2048935292e_BVar @ A) = (type_M2048935292e_BVar @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_type__scheme_Oinject_I2_J)).
% 23.31/6.56  thf(1252,plain,((! [A:nat,B:nat]: (((type_M2048935292e_BVar @ A) = (type_M2048935292e_BVar @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 23.31/6.56  thf(236,axiom,((! [A:list_T1103309005le_typ,B:list_l1790670291le_typ]: ((type_M1418941437le_typ @ (cons_l392684675le_typ @ A @ B)) = (sup_sup_set_nat @ (type_M510873837le_typ @ A) @ (type_M1418941437le_typ @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_285_free__tv__list_Osimps_I2_J)).
% 23.31/6.56  thf(1267,plain,((! [A:list_T1103309005le_typ,B:list_l1790670291le_typ]: ((type_M1418941437le_typ @ (cons_l392684675le_typ @ A @ B)) = (sup_sup_set_nat @ (type_M510873837le_typ @ A) @ (type_M1418941437le_typ @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 23.31/6.56  thf(194,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_213_order_Ostrict__implies__not__eq)).
% 23.31/6.56  thf(1098,plain,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (~ ((A) = (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 23.31/6.56  thf(300,axiom,((! [A:nat]: ~ (member_nat @ A @ bot_bot_set_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_57_empty__iff)).
% 23.31/6.56  thf(1499,plain,((! [A:nat]: ~ (member_nat @ A @ bot_bot_set_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[300])).
% 23.31/6.56  thf(246,axiom,((! [A:(nat > $o)]: ((sup_sup_nat_o @ A @ bot_bot_nat_o) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_295_sup__bot_Oright__neutral)).
% 23.31/6.56  thf(1300,plain,((! [A:(nat > $o)]: ((sup_sup_nat_o @ A @ bot_bot_nat_o) = (A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 23.31/6.56  thf(93,axiom,((! [A:set_nat]: ~ (ord_less_set_nat @ A @ bot_bot_set_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_111_not__psubset__empty)).
% 23.31/6.56  thf(717,plain,((! [A:set_nat]: ~ (ord_less_set_nat @ A @ bot_bot_set_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 23.31/6.56  thf(126,axiom,((! [A:type_M1694694083scheme,B:type_M1694694083scheme]: ((type_M326705277scheme @ (type_M155660035e_SFun @ A @ B)) = (sup_sup_set_nat @ (type_M326705277scheme @ A) @ (type_M326705277scheme @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_282_bound__tv__type__scheme_Osimps_I3_J)).
% 23.31/6.56  thf(840,plain,((! [A:type_M1694694083scheme,B:type_M1694694083scheme]: ((type_M326705277scheme @ (type_M155660035e_SFun @ A @ B)) = (sup_sup_set_nat @ (type_M326705277scheme @ A) @ (type_M326705277scheme @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 23.31/6.56  thf(116,axiom,((type_M1715972684le_typ = (^ [A:(nat > type_Mirabelle_typ)]: (sup_sup_set_nat @ (type_Mirabelle_dom @ (^ [B:nat]: (type_M1743451154le_typ @ (A @ (type_M1898948661at_nat @ B))))) @ (type_Mirabelle_cod @ (^ [B:nat]: (type_M1743451154le_typ @ (A @ (type_M1898948661at_nat @ B))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_290_free__tv__fun__def)).
% 23.31/6.56  thf(808,plain,(((type_M1715972684le_typ) = (^ [A:(nat > type_Mirabelle_typ)]: (sup_sup_set_nat @ (type_Mirabelle_dom @ (^ [B:nat]: (type_M1743451154le_typ @ (A @ (type_M1898948661at_nat @ B))))) @ (type_Mirabelle_cod @ (^ [B:nat]: (type_M1743451154le_typ @ (A @ (type_M1898948661at_nat @ B))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 23.31/6.56  thf(206,axiom,((! [A:nat]: ((collect_nat @ ((=) @ nat @ A)) = (insert_nat @ A @ bot_bot_set_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_47_singleton__conv2)).
% 23.31/6.56  thf(1130,plain,((! [A:nat]: ((collect_nat @ ((=) @ nat @ A)) = (insert_nat @ A @ bot_bot_set_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 23.31/6.56  thf(224,axiom,((! [A:(nat > $o)]: (((collect_nat @ A) = bot_bot_set_nat) = (A = bot_bot_nat_o)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_249_Collect__empty__eq__bot)).
% 23.31/6.56  thf(1220,plain,((! [A:(nat > $o)]: (((collect_nat @ (A)) = bot_bot_set_nat) = ((A) = (bot_bot_nat_o))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 23.31/6.56  thf(313,axiom,((! [A:list_T247403987scheme,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member_nat @ D @ (type_M141510067scheme @ A)) => ((B @ D) = (C @ D)))) => ((type_M1944210753scheme @ B @ A) = (type_M1944210753scheme @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_109_scheme__list__substitutions__only__on__free__variables)).
% 23.31/6.56  thf(1543,plain,((! [A:list_T247403987scheme,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member_nat @ D @ (type_M141510067scheme @ A)) => ((B @ D) = (C @ D)))) => ((type_M1944210753scheme @ (B) @ A) = (type_M1944210753scheme @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[313])).
% 23.31/6.56  thf(234,axiom,((! [A:nat,B:list_l1334080099scheme,C:list_l1704431731scheme]: ((type_M1172169604scheme @ A @ (cons_l531914285scheme @ B @ C)) = ((type_M1377662078scheme @ A @ B) & (type_M1172169604scheme @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_21_new__tv__Cons)).
% 23.31/6.56  thf(1257,plain,((! [A:nat,B:list_l1334080099scheme,C:list_l1704431731scheme]: ((type_M1172169604scheme @ A @ (cons_l531914285scheme @ B @ C)) = ((type_M1377662078scheme @ A @ B) & (type_M1172169604scheme @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 23.31/6.56  thf(60,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_217_dual__order_Ostrict__implies__not__eq)).
% 23.31/6.56  thf(600,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 23.31/6.56  thf(295,axiom,((! [A:(nat > type_Mirabelle_typ),B:nat]: ((type_M1690910139scheme @ A @ (type_M876316792e_FVar @ B)) = (type_M1006385707scheme @ (A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_app__subst__type__scheme_Osimps_I1_J)).
% 23.31/6.56  thf(1485,plain,((! [A:(nat > type_Mirabelle_typ),B:nat]: ((type_M1690910139scheme @ (A) @ (type_M876316792e_FVar @ B)) = (type_M1006385707scheme @ (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[295])).
% 23.31/6.56  thf(324,axiom,((! [A:nat,B:set_nat]: ((member_nat @ A @ B) => (~ (! [C:set_nat]: ((B = (insert_nat @ A @ C)) => (member_nat @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_79_Set_Oset__insert)).
% 23.31/6.56  thf(1585,plain,((! [A:nat,B:set_nat]: ((member_nat @ A @ B) => (~ (! [C:set_nat]: ((B = (insert_nat @ A @ C)) => (member_nat @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[324])).
% 23.31/6.56  thf(172,axiom,((! [A:(nat > type_Mirabelle_typ)]: ((type_M1944210753scheme @ A @ nil_Ty61485117scheme) = nil_Ty61485117scheme))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_350_app__subst__Nil)).
% 23.31/6.56  thf(1008,plain,((! [A:(nat > type_Mirabelle_typ)]: ((type_M1944210753scheme @ (A) @ nil_Ty61485117scheme) = nil_Ty61485117scheme))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 23.31/6.56  thf(238,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (ord_less_nat @ B @ A)) = (B = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_189_antisym__conv3)).
% 23.31/6.56  thf(1272,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (ord_less_nat @ B @ A)) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 23.31/6.56  thf(63,axiom,((! [A:nat,B:nat]: ((A != B) = ((ord_less_nat @ A @ B) | (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_153_neq__iff)).
% 23.31/6.56  thf(612,plain,((! [A:nat,B:nat]: ((~ (A = B)) = ((ord_less_nat @ A @ B) | (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 23.31/6.56  thf(228,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_158_less__imp__neq)).
% 23.31/6.56  thf(1240,plain,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (~ ((A) = (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 23.31/6.56  thf(165,axiom,((! [A:nat]: ((type_M49385309le_typ @ (type_Mirabelle_TVar @ A)) = (insert_nat @ A @ bot_bot_set_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_103_free__tv__TVar)).
% 23.31/6.56  thf(991,plain,((! [A:nat]: ((type_M49385309le_typ @ (type_Mirabelle_TVar @ A)) = (insert_nat @ A @ bot_bot_set_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 23.31/6.56  thf(278,axiom,((sup_sup_set_nat = (^ [A:set_nat,B:set_nat]: (collect_nat @ (sup_sup_nat_o @ (^ [C:nat]: (member_nat @ C @ A)) @ (^ [C:nat]: (member_nat @ C @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_308_sup__set__def)).
% 23.31/6.56  thf(1421,plain,(((sup_sup_set_nat) = (^ [A:set_nat,B:set_nat]: (collect_nat @ (sup_sup_nat_o @ (^ [C:nat]: (member_nat @ C @ A)) @ (^ [C:nat]: (member_nat @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 23.31/6.56  thf(287,axiom,((! [A:set_nat,B:set_nat,C:(nat > $o)]: ((! [D:nat]: ((member_nat @ D @ (sup_sup_set_nat @ A @ B)) => (C @ D))) = (! [D:nat]: ((member_nat @ D @ A) => (C @ D)) & ! [D:nat]: ((member_nat @ D @ B) => (C @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_263_ball__Un)).
% 23.31/6.56  thf(1459,plain,((! [A:set_nat,B:set_nat,C:(nat > $o)]: ((! [D:nat]: ((member_nat @ D @ (sup_sup_set_nat @ A @ B)) => (C @ D))) = (! [D:nat]: ((member_nat @ D @ A) => (C @ D)) & ! [D:nat]: ((member_nat @ D @ B) => (C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[287])).
% 23.31/6.56  thf(47,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ A @ B) => ((ord_less_nat_o @ C @ A) => (ord_less_nat_o @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_209_dual__order_Ostrict__trans)).
% 23.31/6.56  thf(556,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => ((ord_less_nat_o @ (C) @ (A)) => (ord_less_nat_o @ (C) @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 23.31/6.56  thf(315,axiom,((! [A:nat,B:nat]: (((type_M876316792e_FVar @ A) = (type_M876316792e_FVar @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_type__scheme_Oinject_I1_J)).
% 23.31/6.56  thf(1553,plain,((! [A:nat,B:nat]: (((type_M876316792e_FVar @ A) = (type_M876316792e_FVar @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[315])).
% 23.31/6.56  thf(54,axiom,((! [A:set_nat,B:set_nat]: ((bot_bot_set_nat = (sup_sup_set_nat @ A @ B)) = ((A = bot_bot_set_nat) & (B = bot_bot_set_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_298_sup__bot_Oneutr__eq__iff)).
% 23.31/6.56  thf(581,plain,((! [A:set_nat,B:set_nat]: ((bot_bot_set_nat = (sup_sup_set_nat @ A @ B)) = ((A = bot_bot_set_nat) & (B = bot_bot_set_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 23.31/6.56  thf(276,axiom,((! [A:type_Mirabelle_typ,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member_nat @ D @ (type_M49385309le_typ @ A)) => ((B @ D) = (C @ D)))) => ((type_M784671311le_typ @ B @ A) = (type_M784671311le_typ @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_34_typ__substitutions__only__on__free__variables)).
% 23.31/6.56  thf(1412,plain,((! [A:type_Mirabelle_typ,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member_nat @ D @ (type_M49385309le_typ @ A)) => ((B @ D) = (C @ D)))) => ((type_M784671311le_typ @ (B) @ A) = (type_M784671311le_typ @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[276])).
% 23.31/6.56  thf(305,axiom,((! [A:nat,B:set_nat,C:set_nat]: ((member_nat @ A @ (sup_sup_set_nat @ B @ C)) = ((member_nat @ A @ B) | (member_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_253_Un__iff)).
% 23.31/6.56  thf(1517,plain,((! [A:nat,B:set_nat,C:set_nat]: ((member_nat @ A @ (sup_sup_set_nat @ B @ C)) = ((member_nat @ A @ B) | (member_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[305])).
% 23.31/6.56  thf(217,axiom,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: ((if_Typ1169047309le_typ @ ($true) @ A @ B) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_If_1_1_If_001t__Type____Mirabelle____lczmhmumaa__Otyp_T)).
% 23.31/6.56  thf(1189,plain,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: ((if_Typ1169047309le_typ @ ($true) @ A @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 23.31/6.56  thf(270,axiom,((! [A:nat,B:nat]: ((member_nat @ A @ (insert_nat @ B @ bot_bot_set_nat)) => (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_90_singletonD)).
% 23.31/6.56  thf(1390,plain,((! [A:nat,B:nat]: ((member_nat @ A @ (insert_nat @ B @ bot_bot_set_nat)) => (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 23.31/6.56  thf(285,axiom,((! [A:nat]: ((type_M326705277scheme @ (type_M876316792e_FVar @ A)) = bot_bot_set_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_104_bound__tv__type__scheme_Osimps_I1_J)).
% 23.31/6.56  thf(1453,plain,((! [A:nat]: ((type_M326705277scheme @ (type_M876316792e_FVar @ A)) = bot_bot_set_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[285])).
% 23.31/6.56  thf(325,axiom,((! [A:nat,B:set_nat,C:set_nat]: ((member_nat @ A @ B) => (member_nat @ A @ (sup_sup_set_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_259_UnI1)).
% 23.31/6.56  thf(1590,plain,((! [A:nat,B:set_nat,C:set_nat]: ((member_nat @ A @ B) => (member_nat @ A @ (sup_sup_set_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[325])).
% 23.31/6.56  thf(253,axiom,((! [A:set_nat]: ((sup_sup_set_nat @ A @ bot_bot_set_nat) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_294_sup__bot__right)).
% 23.31/6.56  thf(1326,plain,((! [A:set_nat]: ((sup_sup_set_nat @ A @ bot_bot_set_nat) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 23.31/6.56  thf(256,axiom,((! [A:type_Mirabelle_typ,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member_nat @ D @ (type_M49385309le_typ @ A)) => ((B @ D) = (C @ D)))) => ((type_M784671311le_typ @ B @ A) = (type_M784671311le_typ @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_32_eq__free__eq__subst__te)).
% 23.31/6.56  thf(1341,plain,((! [A:type_Mirabelle_typ,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member_nat @ D @ (type_M49385309le_typ @ A)) => ((B @ D) = (C @ D)))) => ((type_M784671311le_typ @ (B) @ A) = (type_M784671311le_typ @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 23.31/6.56  thf(293,axiom,((type_M1377662078scheme = (^ [A:nat,B:list_l1334080099scheme]: ! [C:nat]: ((member_nat @ C @ (type_M1958029241scheme @ B)) => (ord_less_nat @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_40_new__tv__def)).
% 23.31/6.56  thf(1481,plain,(((type_M1377662078scheme) = (^ [A:nat,B:list_l1334080099scheme]: ! [C:nat]: ((member_nat @ C @ (type_M1958029241scheme @ B)) => (ord_less_nat @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[293])).
% 23.31/6.56  thf(75,axiom,((type_M1715972684le_typ = (^ [A:(nat > type_Mirabelle_typ)]: (sup_sup_set_nat @ (type_Mirabelle_dom @ A) @ (type_Mirabelle_cod @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_251_free__tv__subst)).
% 23.31/6.56  thf(652,plain,(((type_M1715972684le_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)],[75])).
% 23.31/6.56  thf(229,axiom,((! [A:set_nat,B:set_nat]: (((sup_sup_set_nat @ A @ B) = bot_bot_set_nat) = ((A = bot_bot_set_nat) & (B = bot_bot_set_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_254_Un__empty)).
% 23.31/6.56  thf(1244,plain,((! [A:set_nat,B:set_nat]: (((sup_sup_set_nat @ A @ B) = bot_bot_set_nat) = ((A = bot_bot_set_nat) & (B = bot_bot_set_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 23.31/6.56  thf(109,axiom,((! [A:type_M1694694083scheme,B:list_T247403987scheme]: ((type_M961603331scheme @ (cons_T633159821scheme @ A @ B)) = (sup_sup_set_nat @ (type_M326705277scheme @ A) @ (type_M961603331scheme @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_279_bound__tv__list_Osimps_I2_J)).
% 23.31/6.56  thf(786,plain,((! [A:type_M1694694083scheme,B:list_T247403987scheme]: ((type_M961603331scheme @ (cons_T633159821scheme @ A @ B)) = (sup_sup_set_nat @ (type_M326705277scheme @ A) @ (type_M961603331scheme @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 23.31/6.56  thf(167,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (~ (ord_less_nat_o @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_180_dual__order_Oasym)).
% 23.31/6.56  thf(995,plain,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (~ (ord_less_nat_o @ (B) @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 23.31/6.56  thf(159,axiom,((! [A:set_nat,B:set_nat,C:(set_nat > set_nat),D:set_nat]: ((ord_less_set_nat @ A @ B) => (((C @ B) = D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_set_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_127_ord__less__eq__subst)).
% 23.31/6.56  thf(961,plain,((! [A:set_nat,B:set_nat,C:(set_nat > set_nat),D:set_nat]: ((ord_less_set_nat @ A @ B) => (((C @ B) = D) => ((! [E:set_nat,F:set_nat]: ((ord_less_set_nat @ E @ F) => (ord_less_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_set_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 23.31/6.56  thf(118,axiom,((! [A:set_nat,B:set_nat]: (((sup_sup_set_nat @ A @ B) = bot_bot_set_nat) = ((A = bot_bot_set_nat) & (B = bot_bot_set_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_302_sup__bot_Oeq__neutr__iff)).
% 23.31/6.56  thf(813,plain,((! [A:set_nat,B:set_nat]: (((sup_sup_set_nat @ A @ B) = bot_bot_set_nat) = ((A = bot_bot_set_nat) & (B = bot_bot_set_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 23.31/6.56  thf(268,axiom,((type_M1963061490scheme = (^ [A:nat,B:type_M1694694083scheme]: ! [C:nat]: ((member_nat @ C @ (type_M1050318637scheme @ B)) => (ord_less_nat @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_42_new__tv__def)).
% 23.31/6.56  thf(1385,plain,(((type_M1963061490scheme) = (^ [A:nat,B:type_M1694694083scheme]: ! [C:nat]: ((member_nat @ C @ (type_M1050318637scheme @ B)) => (ord_less_nat @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 23.31/6.56  thf(147,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (ord_less_set_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_179_dual__order_Oasym)).
% 23.31/6.56  thf(914,plain,((! [A:set_nat,B:set_nat]: ((ord_less_set_nat @ A @ B) => (~ (ord_less_set_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 23.31/6.56  thf(78,axiom,((! [A:(nat > $o)]: ((sup_sup_nat_o @ bot_bot_nat_o @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_291_sup__bot__left)).
% 23.31/6.56  thf(667,plain,((! [A:(nat > $o)]: ((sup_sup_nat_o @ bot_bot_nat_o @ A) = (A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 23.31/6.56  thf(189,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ A) => (ord_less_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_210_dual__order_Ostrict__trans)).
% 23.31/6.56  thf(1077,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ A) => (ord_less_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 23.31/6.56  thf(207,axiom,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat]: (A @ D @ D)) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_207_linorder__less__wlog)).
% 23.31/6.56  thf(1133,plain,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat]: (A @ D @ D)) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 23.31/6.56  thf(15,axiom,((! [A:(nat > $o),B:nat]: ((? [C:nat]: ((A @ C) & ! [D:nat]: ((A @ D) => (D = C)))) => ((A @ B) = (B = (the_nat @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_328_theI__unique)).
% 23.31/6.56  thf(432,plain,((! [A:(nat > $o),B:nat]: ((? [C:nat]: ((A @ C) & ! [D:nat]: ((A @ D) => (D = C)))) => ((A @ B) = (B = (the_nat @ (A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 23.31/6.56  thf(124,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ (sup_sup_set_nat @ A @ B) @ C) => (~ ((ord_less_set_nat @ A @ C) => (~ (ord_less_set_nat @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_316_sup_Ostrict__boundedE)).
% 23.31/6.56  thf(833,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_set_nat @ (sup_sup_set_nat @ A @ B) @ C) => (~ ((ord_less_set_nat @ A @ C) => (~ (ord_less_set_nat @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 23.31/6.56  thf(155,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (~ (ord_less_nat_o @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_204_less__imp__not__less)).
% 23.31/6.56  thf(950,plain,((! [A:(nat > $o),B:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (~ (ord_less_nat_o @ (B) @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 23.31/6.56  thf(266,axiom,((bot_bot_nat_o = (^ [A:nat]: (member_nat @ A @ bot_bot_set_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_250_bot__empty__eq)).
% 23.31/6.56  thf(1380,plain,(((bot_bot_nat_o) = (^ [A:nat]: (member_nat @ A @ bot_bot_set_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 23.31/6.56  thf(309,axiom,((! [A:nat]: ~ (member_nat @ A @ bot_bot_set_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_68_emptyE)).
% 23.31/6.56  thf(1527,plain,((! [A:nat]: ~ (member_nat @ A @ bot_bot_set_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[309])).
% 23.31/6.56  thf(14,axiom,((! [A:(nat > $o),B:nat]: ((? [C:nat]: ((A @ C) & ! [D:nat]: ((A @ D) => (D = C)))) => ((A @ B) => ((the_nat @ A) = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_248_the1__equality)).
% 23.31/6.56  thf(422,plain,((! [A:(nat > $o),B:nat]: ((? [C:nat]: ((A @ C) & ! [D:nat]: ((A @ D) => (D = C)))) => ((A @ B) => ((the_nat @ (A)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 23.31/6.56  thf(169,axiom,((! [A:nat,B:type_Mirabelle_typ,C:list_T1103309005le_typ]: ((type_M263553000le_typ @ A @ (cons_T363929085le_typ @ B @ C)) = ((type_M1211611096le_typ @ A @ B) & (type_M263553000le_typ @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_23_new__tv__Cons)).
% 23.31/6.56  thf(999,plain,((! [A:nat,B:type_Mirabelle_typ,C:list_T1103309005le_typ]: ((type_M263553000le_typ @ A @ (cons_T363929085le_typ @ B @ C)) = ((type_M1211611096le_typ @ A @ B) & (type_M263553000le_typ @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 23.31/6.56  thf(65,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((A = B) => ((ord_less_set_nat @ B @ C) => (ord_less_set_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_173_ord__eq__less__trans)).
% 23.31/6.56  thf(620,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((A = B) => ((ord_less_set_nat @ B @ C) => (ord_less_set_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 23.31/6.56  thf(131,axiom,((! [A:(nat > $o),B:(nat > $o),C:((nat > $o) > (nat > $o)),D:(nat > $o)]: ((ord_less_nat_o @ A @ B) => (((C @ B) = D) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ E @ F) => (ord_less_nat_o @ (C @ E) @ (C @ F)))) => (ord_less_nat_o @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_131_ord__less__eq__subst)).
% 23.31/6.56  thf(854,plain,((! [A:(nat > $o),B:(nat > $o),C:((nat > $o) > (nat > $o)),D:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => (((C @ B) = (D)) => ((! [E:(nat > $o),F:(nat > $o)]: ((ord_less_nat_o @ (E) @ (F)) => (ord_less_nat_o @ (C @ E) @ (C @ F)))) => (ord_less_nat_o @ (C @ A) @ (D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 23.31/6.56  thf(247,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_205_less__imp__not__less)).
% 23.31/6.56  thf(1303,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 23.31/6.56  thf(1,conjecture,((((type_M1690910139scheme @ s1 @ (type_M876316792e_FVar @ x)) != (type_M1690910139scheme @ s2 @ (type_M876316792e_FVar @ x))) | ~ (member_nat @ n @ (type_M1050318637scheme @ (type_M876316792e_FVar @ x))) | ((s1 @ n) = (s2 @ n)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 23.31/6.56  thf(2,negated_conjecture,((~ (((type_M1690910139scheme @ s1 @ (type_M876316792e_FVar @ x)) != (type_M1690910139scheme @ s2 @ (type_M876316792e_FVar @ x))) | ~ (member_nat @ n @ (type_M1050318637scheme @ (type_M876316792e_FVar @ x))) | ((s1 @ n) = (s2 @ n))))),inference(neg_conjecture,[status(cth)],[1])).
% 23.31/6.56  thf(326,plain,((~ (~ ((type_M1690910139scheme @ (s1) @ (type_M876316792e_FVar @ x)) = (type_M1690910139scheme @ (s2) @ (type_M876316792e_FVar @ x))) | ~ (member_nat @ n @ (type_M1050318637scheme @ (type_M876316792e_FVar @ x))) | ((s1 @ n) = (s2 @ n))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 23.31/6.56  thf(262,axiom,((! [A:(nat > type_Mirabelle_typ),B:type_M1694694083scheme,C:type_M1694694083scheme]: ((type_M1690910139scheme @ A @ (type_M155660035e_SFun @ B @ C)) = (type_M155660035e_SFun @ (type_M1690910139scheme @ A @ B) @ (type_M1690910139scheme @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_app__subst__type__scheme_Osimps_I3_J)).
% 23.31/6.56  thf(1363,plain,((! [A:(nat > type_Mirabelle_typ),B:type_M1694694083scheme,C:type_M1694694083scheme]: ((type_M1690910139scheme @ (A) @ (type_M155660035e_SFun @ B @ C)) = (type_M155660035e_SFun @ (type_M1690910139scheme @ (A) @ B) @ (type_M1690910139scheme @ (A) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 23.31/6.56  thf(94,axiom,((! [A:nat,B:nat,C:(nat > (nat > $o)),D:(nat > $o)]: ((ord_less_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat_o @ (C @ E) @ (C @ F)))) => (ord_less_nat_o @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_125_ord__less__eq__subst)).
% 23.31/6.56  thf(720,plain,((! [A:nat,B:nat,C:(nat > (nat > $o)),D:(nat > $o)]: ((ord_less_nat @ A @ B) => (((C @ B) = (D)) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat_o @ (C @ E) @ (C @ F)))) => (ord_less_nat_o @ (C @ A) @ (D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 23.31/6.56  thf(157,axiom,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: ((type_M1006385707scheme @ (type_Mirabelle_Fun @ A @ B)) = (type_M155660035e_SFun @ (type_M1006385707scheme @ A) @ (type_M1006385707scheme @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_225_mk__scheme_Osimps_I2_J)).
% 23.31/6.56  thf(955,plain,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: ((type_M1006385707scheme @ (type_Mirabelle_Fun @ A @ B)) = (type_M155660035e_SFun @ (type_M1006385707scheme @ A) @ (type_M1006385707scheme @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 23.31/6.56  thf(140,axiom,((! [A:(nat > $o)]: ~ (ord_less_nat_o @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_198_dual__order_Oirrefl)).
% 23.31/6.56  thf(886,plain,((! [A:(nat > $o)]: ~ (ord_less_nat_o @ (A) @ (A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 23.31/6.56  thf(143,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_202_order_Ostrict__trans)).
% 23.31/6.56  thf(897,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 23.31/6.56  thf(27,axiom,(((type_M1715972684le_typ @ type_M405566558_subst) = bot_bot_set_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_222_free__tv__id__subst)).
% 23.31/6.56  thf(474,plain,(((type_M1715972684le_typ @ (type_M405566558_subst)) = bot_bot_set_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 23.31/6.56  thf(275,axiom,((type_M1211611096le_typ = (^ [A:nat,B:type_Mirabelle_typ]: ! [C:nat]: ((member_nat @ C @ (type_M49385309le_typ @ B)) => (ord_less_nat @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_43_new__tv__def)).
% 23.31/6.56  thf(1410,plain,(((type_M1211611096le_typ) = (^ [A:nat,B:type_Mirabelle_typ]: ! [C:nat]: ((member_nat @ C @ (type_M49385309le_typ @ B)) => (ord_less_nat @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[275])).
% 23.31/6.56  thf(103,axiom,((! [A:set_nat]: ((sup_sup_set_nat @ A @ bot_bot_set_nat) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_296_sup__bot_Oright__neutral)).
% 23.31/6.56  thf(767,plain,((! [A:set_nat]: ((sup_sup_set_nat @ A @ bot_bot_set_nat) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 23.31/6.56  thf(242,axiom,((! [A:set_nat]: ((sup_sup_set_nat @ bot_bot_set_nat @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_300_sup__bot_Oleft__neutral)).
% 23.31/6.56  thf(1288,plain,((! [A:set_nat]: ((sup_sup_set_nat @ bot_bot_set_nat @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 23.31/6.56  thf(219,axiom,(((type_M141510067scheme @ nil_Ty61485117scheme) = bot_bot_set_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_352_free__tv__list_Osimps_I1_J)).
% 23.31/6.56  thf(1197,plain,(((type_M141510067scheme @ nil_Ty61485117scheme) = bot_bot_set_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 23.31/6.56  thf(193,axiom,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_175_ord__eq__less__trans)).
% 23.31/6.56  thf(1093,plain,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 23.31/6.56  thf(208,axiom,((! [A:(nat > $o)]: (((collect_nat @ A) = bot_bot_set_nat) = (! [B:nat]: ~ (A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_Collect__empty__eq)).
% 23.31/6.56  thf(1152,plain,((! [A:(nat > $o)]: (((collect_nat @ (A)) = bot_bot_set_nat) = (! [B:nat]: ~ (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 23.31/6.56  thf(265,axiom,((sup_sup_set_nat = (^ [A:set_nat,B:set_nat]: (collect_nat @ (^ [C:nat]: ((member_nat @ C @ A) | (member_nat @ C @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_261_Un__def)).
% 23.31/6.56  thf(1378,plain,(((sup_sup_set_nat) = (^ [A:set_nat,B:set_nat]: (collect_nat @ (^ [C:nat]: ((member_nat @ C @ A) | (member_nat @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[265])).
% 23.31/6.56  thf(323,axiom,((! [A:set_nat]: ((! [B:nat]: ~ (member_nat @ B @ A)) = (A = bot_bot_set_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_61_all__not__in__conv)).
% 23.31/6.56  thf(1582,plain,((! [A:set_nat]: ((! [B:nat]: ~ (member_nat @ B @ A)) = (A = bot_bot_set_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[323])).
% 23.31/6.56  thf(261,axiom,((! [A:type_M1694694083scheme,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member_nat @ D @ (type_M1050318637scheme @ A)) => ((B @ D) = (C @ D)))) => ((type_M1690910139scheme @ B @ A) = (type_M1690910139scheme @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_scheme__substitutions__only__on__free__variables)).
% 23.31/6.56  thf(1357,plain,((! [A:type_M1694694083scheme,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member_nat @ D @ (type_M1050318637scheme @ A)) => ((B @ D) = (C @ D)))) => ((type_M1690910139scheme @ (B) @ A) = (type_M1690910139scheme @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 23.31/6.56  thf(16,axiom,(((type_Mirabelle_cod @ type_M405566558_subst) = bot_bot_set_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_242_cod__id__subst)).
% 23.31/6.56  thf(442,plain,(((type_Mirabelle_cod @ (type_M405566558_subst)) = bot_bot_set_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 23.31/6.56  thf(134,axiom,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: ((if_Typ1169047309le_typ @ ($false) @ A @ B) = B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_If_2_1_If_001t__Type____Mirabelle____lczmhmumaa__Otyp_T)).
% 23.31/6.56  thf(871,plain,((! [A:type_Mirabelle_typ,B:type_Mirabelle_typ]: ((if_Typ1169047309le_typ @ ($false) @ A @ B) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 23.31/6.56  thf(302,axiom,((! [A:type_M1694694083scheme,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member_nat @ D @ (type_M1050318637scheme @ A)) => ((B @ D) = (C @ D)))) => ((type_M1690910139scheme @ B @ A) = (type_M1690910139scheme @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_eq__free__eq__subst__type__scheme)).
% 23.31/6.56  thf(1505,plain,((! [A:type_M1694694083scheme,B:(nat > type_Mirabelle_typ),C:(nat > type_Mirabelle_typ)]: ((! [D:nat]: ((member_nat @ D @ (type_M1050318637scheme @ A)) => ((B @ D) = (C @ D)))) => ((type_M1690910139scheme @ (B) @ A) = (type_M1690910139scheme @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[302])).
% 23.31/6.56  thf(35,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_159_less__imp__neq)).
% 23.31/6.56  thf(501,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 23.31/6.56  thf(25,axiom,((! [A:list_l1334080099scheme,B:list_l1704431731scheme]: ((type_M1926053183scheme @ (cons_l531914285scheme @ A @ B)) = (sup_sup_set_nat @ (type_M1958029241scheme @ A) @ (type_M1926053183scheme @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_284_free__tv__list_Osimps_I2_J)).
% 23.31/6.56  thf(469,plain,((! [A:list_l1334080099scheme,B:list_l1704431731scheme]: ((type_M1926053183scheme @ (cons_l531914285scheme @ A @ B)) = (sup_sup_set_nat @ (type_M1958029241scheme @ A) @ (type_M1926053183scheme @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 23.31/6.56  thf(215,axiom,((! [A:nat,B:nat]: ((A != B) => ((~ (ord_less_nat @ A @ B)) => (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_152_neqE)).
% 23.31/6.56  thf(1184,plain,((! [A:nat,B:nat]: ((~ (A = B)) => ((~ (ord_less_nat @ A @ B)) => (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 23.31/6.56  thf(319,axiom,((! [A:set_nat,B:set_nat,C:nat]: ((ord_less_set_nat @ A @ B) => ((member_nat @ C @ A) => (member_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_231_psubsetD)).
% 23.31/6.56  thf(1565,plain,((! [A:set_nat,B:set_nat,C:nat]: ((ord_less_set_nat @ A @ B) => ((member_nat @ C @ A) => (member_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[319])).
% 23.31/6.56  thf(71,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ A @ B) => ((ord_less_nat_o @ B @ C) => (ord_less_nat_o @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_201_order_Ostrict__trans)).
% 23.31/6.56  thf(639,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o)]: ((ord_less_nat_o @ (A) @ (B)) => ((ord_less_nat_o @ (B) @ (C)) => (ord_less_nat_o @ (A) @ (C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 23.31/6.56  thf(33,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_165_less__asym_H)).
% 23.31/6.56  thf(496,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 23.31/6.56  thf(1924,plain,(($false)),inference(e,[status(thm)],[1036,1024,1369,1559,1315,941,1549,1237,846,1031,333,628,977,762,1005,683,1522,994,1401,1533,677,1305,597,1497,385,1310,1164,1275,472,1260,945,1063,1354,930,670,1127,417,1366,973,1046,1430,802,1462,587,1323,1511,702,902,559,1514,1247,1319,1347,881,1115,1568,1232,1013,770,448,1494,924,789,1450,591,1109,1418,485,574,353,1283,1051,905,634,734,866,1351,988,1433,877,692,1104,849,1074,1438,546,1199,810,1470,534,1067,798,1387,1580,1255,1123,1217,1502,630,729,1223,894,746,1091,1042,952,1423,916,566,625,879,852,889,461,493,1407,551,1291,522,830,697,874,1270,650,615,1121,1425,356,1397,783,1118,1329,1160,1082,933,753,537,642,637,1155,686,476,1039,970,837,1249,1297,654,1192,1002,569,779,371,1393,1525,647,997,1530,1539,1456,1382,792,360,805,508,541,1187,765,1054,1466,1071,1026,1167,773,794,1278,750,513,1483,689,444,1219,824,584,819,694,743,577,958,1520,1488,843,1125,498,1107,1332,466,672,604,900,1349,1492,451,1571,863,1011,419,1080,816,609,594,700,1556,1022,1293,462,1112,1474,827,1176,563,1477,1102,505,1562,455,883,394,986,1208,680,663,487,553,490,675,927,374,458,1181,776,525,705,414,1252,1267,1098,1499,1300,717,840,808,1130,1220,1543,1257,600,1485,1585,1008,1272,612,1240,991,1421,1459,556,1553,581,1412,1517,1189,1390,1453,1590,1326,1341,1481,652,1244,786,995,961,813,1385,914,667,1077,1133,432,833,950,1380,1527,422,999,620,854,1303,326,1363,720,955,886,897,474,1410,767,1288,1197,1093,1152,1378,1582,1357,442,871,1505,501,469,1184,1565,639,496])).
% 23.31/6.56  % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.31/6.56  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------