%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP144^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n011.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:06:56 AM UTC 2026
% Result : Theorem 48.98s 34.00s
% Output : Refutation 50.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP144^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.09/0.17 % Computer : n011.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Tue Sep 29 20:00:31 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.68/0.48 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.94/0.81 % [INFO] Parsing done (326ms).
% 1.94/0.83 % [INFO] Running in sequential loop mode.
% 3.20/1.21 % [INFO] eprover registered as external prover.
% 3.20/1.21 % [INFO] Scanning for conjecture ...
% 3.37/1.36 % [INFO] Found a conjecture (or negated_conjecture) and 269 axioms. Running axiom selection ...
% 3.93/1.50 % [INFO] Axiom selection finished. Selected 252 axioms (removed 17 axioms).
% 4.81/1.80 % [INFO] Problem is higher-order (TPTP THF).
% 4.81/1.83 % [INFO] Type checking passed.
% 4.81/1.84 % [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 ...
% 48.98/33.99 % External prover 'e' found a proof!
% 48.98/34.00 % [INFO] Killing All external provers ...
% 48.98/34.00 % Time passed: 33725ms (effective reasoning time: 33163ms)
% 48.98/34.00 % 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)>
% 48.98/34.00 % Axioms used in derivation (252): fact_178_inv__into__into, fact_213_injI, fact_11_some__eq__ex, tcon_fun___Orderings_Obot, fact_244_insert__Diff, fact_43_toCard__def, fact_76_UNIV__witness, fact_7_verit__sko__forall_H_H, fact_19_verit__sko__ex__indirect2, fact_129_insert__UNIV, fact_82_iso__tuple__UNIV__I, fact_3_verit__sko__ex_H, fact_117_insert__compr, fact_222_range__ex1__eq, fact_201_full__SetCompr__eq, fact_52_emptyE, fact_145_image__ident, fact_227_inj__on__insert, fact_182_rangeE, fact_208_surjD, fact_224_inj__image__mem__iff, fact_253_top__conj_I1_J, fact_98_Quotient3__rel__abs, fact_4_verit__sko__forall, fact_240_inj__diff__right, fact_163_image__cong, fact_86_bijection_Oinv__right__eq__iff, fact_230_Diff__iff, fact_53_equals0D, fact_245_Diff__insert, fact_216_bij__betw__empty2, fact_101_Quotient3__refl2, fact_136_bijection_Oinv__left, fact_153_inj__imp__bij__betw__inv, fact_228_top__conj_I2_J, fact_31_exE__some, fact_248_DiffD1, fact_66_bot__empty__eq, fact_206_bij__is__inj, fact_15_someI, tcon_fun___Orderings_Oord, fact_181_Setcompr__eq__image, tcon_HOL_Obool___Orderings_Oord_5, fact_127_singleton__iff, fact_157_surj__imp__inj__inv, fact_191_bijection__def, fact_24_some__in__eq, fact_116_insert__ident, fact_186_inv__inv__eq, fact_146_top1I, fact_149_image__empty, fact_137_bijection_Oinv__right, fact_166_rev__image__eqI, fact_215_inj__def, fact_158_bijI_H, fact_193_surj__imp__inv__eq, fact_154_inj__transfer, fact_160_imageI, fact_139_the__elem__eq, fact_119_insertI2, fact_233_empty__Diff, fact_115_insert__absorb, fact_135_bijection_Oeq__invI, fact_92_singletonI, fact_74_UNIV__def, fact_254_remove__def, fact_184_bij__imp__bij__inv, fact_94_singleton__conv2, fact_198_bijection_Osurj, fact_99_Quotient3__abs__rep, fact_220_inj__fun, fact_65_Collect__empty__eq__bot, fact_83_quot__type_OQuotient, fact_229_DiffI, fact_210_surjI, fact_235_insert__Diff1, fact_46_Collect__mem__eq, fact_112_insert__commute, fact_8_someI__ex, tcon_Set_Oset___Orderings_Oord_2, fact_217_bij__betw__empty1, fact_106_equals__rsp, fact_41_bot__apply, fact_111_mk__disjoint__insert, fact_42_quot__type_Orep__def, fact_0_some__equality, fact_171_bij__image__Collect__eq, fact_90_insert__iff, tcon_HOL_Obool___Orderings_Obot_6, fact_238_Diff__UNIV, fact_38_Collect__empty__eq, fact_133_is__singleton__def, fact_138_is__singleton__the__elem, fact_79_quot__type_Oabs_Ocong, fact_130_Collect__conv__if, fact_169_rangeI, fact_110_bijection_OeqI, fact_21_Nitpick_OEps__psimp, fact_32_quot__type_Orep__inverse, fact_113_insert__Collect, tcon_HOL_Obool___Orderings_Otop_4, fact_247_DiffE, fact_174_bij__betw__inv__into__left, fact_85_is__singletonI, fact_33_quot__type_Oabs__inverse, fact_62_Set_Ois__empty__def, fact_199_image__constant, fact_200_image__constant__conv, fact_140_range__constant, fact_234_Diff__cancel, fact_89_insert__absorb2, fact_239_surj__diff__right, fact_192_bijection_Obij, fact_231_Diff__idemp, fact_205_bijI, fact_45_mem__Collect__eq, fact_189_inv__f__f, fact_70_top__apply, fact_13_tfl__some, fact_126_doubleton__eq__iff, fact_179_inv__into__injective, fact_203_inj__on__empty, fact_237_insert__Diff__single, fact_195_surj__iff__all, fact_2_some__sym__eq__trivial, fact_18_some1__equality, fact_6_verit__sko__forall_H, fact_9_someI2__ex, fact_197_bijection_Oinj, fact_26_inv__into__def, fact_177_f__inv__into__f, fact_255_fun__upd__image, fact_100_rep__abs__rsp__left, fact_29_arg__max__def, fact_131_Collect__conv__if2, tcon_Set_Oset___Orderings_Otop_1, fact_164_ball__imageD, fact_176_inv__into__f__eq, fact_223_inj__image__eq__iff, fact_104_Quotient3__def, fact_35_quot__type_Orep__prop, fact_134_is__singletonE, fact_17_verit__sko__forall__indirect, fact_185_bij__inv__eq__iff, fact_159_imageE, fact_236_Diff__insert0, fact_63_quot__type_Oabs__def, fact_47_Collect__cong, fact_155_image__inv__f__f, fact_20_verit__sko__ex__indirect, fact_93_singleton__conv, fact_102_Quotient3__refl1, fact_95_Quotient3__rep__reflp, fact_148_empty__is__image, fact_168_the__elem__image__unique, help_If_3_1_T, fact_39_all__not__in__conv, fact_14_Eps__cong, fact_232_Diff__empty, fact_226_bij__betw__imp__surj, tcon_fun___Orderings_Otop, fact_165_image__image, fact_156_inj__imp__surj__inv, fact_190_bijection_Ointro, fact_23_pick__middlep__def, fact_221_inj__img__insertE, fact_144_image__eqI, fact_122_top__empty__eq, fact_75_UNIV__eq__I, fact_91_insertCI, fact_71_UNIV__I, fact_81_inv__equality, fact_10_someI2__bex, fact_211_surj__def, fact_51_bot__fun__def, fact_242_Diff__insert__absorb, fact_16_verit__sko__forall__indirect2, fact_50_quot__type_Orep_Ocong, fact_175_bij__betw__inv__into__right, fact_170_range__eqI, fact_54_equals0I, fact_202_range__eq__singletonD, fact_22_univ__def, fact_196_surj__f__inv__f, fact_87_bijection_Oinv__left__eq__iff, fact_246_in__image__insert__iff, fact_212_injD, fact_56_empty__def, fact_69_is__singletonI_H, fact_218_bij__pointE, fact_107_Quotient3I, fact_1_some__eq__trivial, fact_225_bij__is__surj, fact_204_bij__def, fact_252_image__set__diff, fact_27_quot__type_Osome__collect, fact_5_someI2, fact_173_inv__into__inv__into__eq, fact_67_inv__def, fact_105_rep__abs__rsp, fact_209_surjE, fact_128_singletonD, fact_143_bijection_Obij__inv, fact_214_inj__eq, fact_187_inj__imp__inv__eq, fact_109_bijection_Oeq__iff, fact_25_inv__into__def2, fact_152_inv__into__f__f, fact_183_range__composition, fact_34_quot__type_Orep__inject, fact_80_empty__not__UNIV, fact_124_singleton__inject, fact_249_DiffD2, fact_141_bijection_Osurj__inv, fact_241_translation__subtract__diff, fact_97_Quotient3__rel__rep, fact_161_image__iff, fact_114_insert__eq__iff, fact_167_Compr__image__eq, fact_251_insert__Diff__if, fact_188_inv__f__eq, fact_121_insertE, fact_250_set__diff__eq, fact_147_image__is__empty, fact_243_Diff__insert2, fact_123_top__set__def, fact_28_fromCard__def, fact_36_arg__max__on__def, fact_180_setcompr__eq__image, fact_125_insert__not__empty, tcon_Set_Oset___Orderings_Obot_3, fact_219_inj__singleton, conj_0, fact_103_Quotient3__rel, fact_120_insertI1, fact_207_inj__on__id2, fact_118_Set_Oset__insert, fact_194_image__f__inv__f, fact_72_Collect__const, fact_142_bijection_Oinj__inv, fact_73_inv__identity, fact_162_bex__imageD, fact_96_Quotient3__rep__abs, fact_12_some__eq__imp, fact_88_bijection_Oeq__inv__iff, fact_40_empty__iff, fact_37_empty__Collect__eq, fact_172_bij__betw__inv__into, fact_49_bot__set__def, fact_55_ex__in__conv, fact_150_image__insert, fact_151_insert__image
% 48.98/34.00 % No. of inferences in proof: 508
% 48.98/34.00 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 33725 ms resp. 33163 ms w/o parsing
% 50.45/34.27 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 50.45/34.27 thf(b_type, type, b: $tType).
% 50.45/34.27 thf(a_type, type, a: $tType).
% 50.45/34.27 thf(bot_decl, type, bot: !> [TA: $tType]: $o).
% 50.45/34.27 thf(ord_decl, type, ord: !> [TA: $tType]: $o).
% 50.45/34.27 thf(top_decl, type, top: !> [TA: $tType]: $o).
% 50.45/34.27 thf(ab_group_add_decl, type, ab_group_add: !> [TA: $tType]: $o).
% 50.45/34.27 thf(bNF_pick_middlep_decl, type, bNF_pick_middlep: !> [TA: $tType,TB: $tType,TC: $tType]: ((TC > (TB > $o)) > ((TB > (TA > $o)) > (TC > (TA > TB))))).
% 50.45/34.27 thf(bNF_Gr932048252omCard_decl, type, bNF_Gr932048252omCard: !> [TA: $tType,TB: $tType]: ((set @ TB) > ((set @ (product_prod @ TA @ TA)) > (TA > TB)))).
% 50.45/34.27 thf(bNF_Greatest_toCard_decl, type, bNF_Greatest_toCard: !> [TA: $tType,TB: $tType]: ((set @ TB) > ((set @ (product_prod @ TA @ TA)) > (TB > TA)))).
% 50.45/34.27 thf(bNF_Gr1978856366d_pred_decl, type, bNF_Gr1978856366d_pred: !> [TA: $tType,TB: $tType]: ((set @ TB) > ((set @ (product_prod @ TA @ TA)) > ((TB > TA) > $o)))).
% 50.45/34.27 thf(bNF_Greatest_univ_decl, type, bNF_Greatest_univ: !> [TA: $tType,TB: $tType]: ((TB > TA) > ((set @ TB) > TA))).
% 50.45/34.27 thf(bij_betw_decl, type, bij_betw: !> [TA: $tType,TB: $tType]: ((TB > TA) > ((set @ TB) > ((set @ TA) > $o)))).
% 50.45/34.27 thf(fun_upd_decl, type, fun_upd: !> [TA: $tType,TB: $tType]: ((TB > TA) > (TB > (TA > (TB > TA))))).
% 50.45/34.27 thf(inj_on_decl, type, inj_on: !> [TA: $tType,TB: $tType]: ((TB > TA) > ((set @ TB) > $o))).
% 50.45/34.27 thf(minus_minus_decl, type, minus_minus: !> [TA: $tType]: (TA > (TA > TA))).
% 50.45/34.27 thf(hilbert_Eps_decl, type, hilbert_Eps: !> [TA: $tType]: ((TA > $o) > TA)).
% 50.45/34.27 thf(hilbert_bijection_decl, type, hilbert_bijection: !> [TA: $tType]: ((TA > TA) > $o)).
% 50.45/34.27 thf(hilbert_inv_into_decl, type, hilbert_inv_into: !> [TA: $tType,TB: $tType]: ((set @ TB) > ((TB > TA) > (TA > TB)))).
% 50.45/34.27 thf(lattices_ord_arg_max_decl, type, lattices_ord_arg_max: !> [TA: $tType,TB: $tType]: ((TB > TA) > ((TB > $o) > TB))).
% 50.45/34.27 thf(lattic1534546155max_on_decl, type, lattic1534546155max_on: !> [TA: $tType,TB: $tType]: ((TB > TA) > ((set @ TB) > TB))).
% 50.45/34.27 thf(lattic2130478198rg_max_decl, type, lattic2130478198rg_max: !> [TA: $tType,TB: $tType]: ((TB > TA) > ((TB > $o) > (TB > $o)))).
% 50.45/34.27 thf(bot_bot_decl, type, bot_bot: !> [TA: $tType]: TA).
% 50.45/34.27 thf(top_top_decl, type, top_top: !> [TA: $tType]: TA).
% 50.45/34.27 thf(quotient3_decl, type, quotient3: !> [TA: $tType,TB: $tType]: ((TB > (TB > $o)) > ((TB > TA) > ((TA > TB) > $o)))).
% 50.45/34.27 thf(quot_type_decl, type, quot_type: !> [TA: $tType,TB: $tType]: ((TB > (TB > $o)) > (((set @ TB) > TA) > ((TA > (set @ TB)) > $o)))).
% 50.45/34.27 thf(quot_abs_decl, type, quot_abs: !> [TA: $tType,TB: $tType]: ((TB > (TB > $o)) > (((set @ TB) > TA) > (TB > TA)))).
% 50.45/34.27 thf(quot_rep_decl, type, quot_rep: !> [TA: $tType,TB: $tType]: ((TB > (set @ TA)) > (TB > TA))).
% 50.45/34.27 thf(collect_decl, type, collect: !> [TA: $tType]: ((TA > $o) > (set @ TA))).
% 50.45/34.27 thf(image_decl, type, image: !> [TA: $tType,TB: $tType]: ((TB > TA) > ((set @ TB) > (set @ TA)))).
% 50.45/34.27 thf(insert_decl, type, insert: !> [TA: $tType]: (TA > ((set @ TA) > (set @ TA)))).
% 50.45/34.27 thf(is_empty_decl, type, is_empty: !> [TA: $tType]: ((set @ TA) > $o)).
% 50.45/34.27 thf(is_singleton_decl, type, is_singleton: !> [TA: $tType]: ((set @ TA) > $o)).
% 50.45/34.27 thf(remove_decl, type, remove: !> [TA: $tType]: (TA > ((set @ TA) > (set @ TA)))).
% 50.45/34.27 thf(the_elem_decl, type, the_elem: !> [TA: $tType]: ((set @ TA) > TA)).
% 50.45/34.27 thf(member_decl, type, member: !> [TA: $tType]: (TA > ((set @ TA) > $o))).
% 50.45/34.27 thf(p_decl, type, p: (a > $o)).
% 50.45/34.27 thf(q_decl, type, q: (a > (b > $o))).
% 50.45/34.27 thf(74,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA)]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) => (bij_betw @ TB @ TA @ (hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A) @ (image @ TA @ TB @ A @ B) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_inj__imp__bij__betw__inv)).
% 50.45/34.27 thf(479,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA)]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) => (bij_betw @ TB @ TA @ (hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A) @ (image @ TA @ TB @ (A) @ B) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 50.45/34.27 thf(32,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:TA,C:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ (insert @ TA @ B @ C)) = (minus_minus @ (set @ TA) @ (minus_minus @ (set @ TA) @ A @ C) @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_Diff__insert)).
% 50.45/34.27 thf(347,plain,((! [TA: $tType]: (! [A:(set @ TA),B:TA,C:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ (insert @ TA @ B @ C)) = (minus_minus @ (set @ TA) @ (minus_minus @ (set @ TA) @ A @ C) @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 50.45/34.27 thf(210,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oord)).
% 50.45/34.27 thf(909,plain,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 50.45/34.27 thf(205,axiom,((! [TA: $tType]: (! [A:TA]: ((insert @ TA @ A @ (top_top @ (set @ TA))) = (top_top @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_insert__UNIV)).
% 50.45/34.27 thf(893,plain,((! [TA: $tType]: (! [A:TA]: ((insert @ TA @ A @ (top_top @ (set @ TA))) = (top_top @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 50.45/34.27 thf(86,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: ((inj_on @ TB @ TA @ A @ (top_top @ (set @ TB))) => (((image @ TB @ TA @ A @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) => (bij_betw @ TB @ TA @ A @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_bijI)).
% 50.45/34.27 thf(518,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: ((inj_on @ TB @ TA @ (A) @ (top_top @ (set @ TB))) => (((image @ TB @ TA @ (A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) => (bij_betw @ TB @ TA @ (A) @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 50.45/34.27 thf(71,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA]: ((quotient3 @ TA @ TB @ A @ B @ C) => (((A @ D @ D) & (A @ E @ E) & ((B @ D) = (B @ E))) = (A @ D @ E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_Quotient3__rel)).
% 50.45/34.27 thf(468,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA]: ((quotient3 @ TA @ TB @ (A) @ (B) @ (C)) => (((A @ D @ D) & (A @ E @ E) & ((B @ D) = (B @ E))) = (A @ D @ E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 50.45/34.27 thf(75,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => (? [C:(set @ TA)]: ((B = (insert @ TA @ A @ C)) & ~ (member @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_mk__disjoint__insert)).
% 50.45/34.27 thf(481,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => (? [C:(set @ TA)]: ((B = (insert @ TA @ A @ C)) & ~ (member @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 50.45/34.27 thf(226,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((member @ TA @ (hilbert_Eps @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) @ A) = (A != (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_some__in__eq)).
% 50.45/34.27 thf(977,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((member @ TA @ (hilbert_Eps @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) @ A) = (~ (A = (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 50.45/34.27 thf(165,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ (top_top @ (set @ TA))) = (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_Diff__UNIV)).
% 50.45/34.27 thf(762,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ (top_top @ (set @ TA))) = (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 50.45/34.27 thf(9,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA]: ((quotient3 @ TA @ TB @ A @ B @ C) => ((A @ D @ E) => ((B @ D) = (B @ E))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_Quotient3__rel__abs)).
% 50.45/34.27 thf(276,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA]: ((quotient3 @ TA @ TB @ (A) @ (B) @ (C)) => ((A @ D @ E) => ((B @ D) = (B @ E))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 50.45/34.27 thf(17,axiom,((! [TA: $tType]: (! [A:(TA > TA)]: ((bij_betw @ TA @ TA @ A @ (top_top @ (set @ TA)) @ (top_top @ (set @ TA))) => (hilbert_bijection @ TA @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_bijection_Ointro)).
% 50.45/34.27 thf(308,plain,((! [TA: $tType]: (! [A:(TA > TA)]: ((bij_betw @ TA @ TA @ (A) @ (top_top @ (set @ TA)) @ (top_top @ (set @ TA))) => (hilbert_bijection @ TA @ (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 50.45/34.27 thf(158,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(TB > TA)]: ((! [C:TB]: ((A @ (B @ C)) = C)) => ((! [C:TA]: ((B @ (A @ C)) = C)) => ((hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ B) = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_inv__equality)).
% 50.45/34.27 thf(741,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(TB > TA)]: ((! [C:TB]: ((A @ (B @ C)) = C)) => ((! [C:TA]: ((B @ (A @ C)) = C)) => ((hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ B) = (A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 50.45/34.27 thf(64,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA,F:TA,G:TA]: ((quotient3 @ TA @ TB @ A @ B @ C) => ((A @ D @ E) => ((A @ F @ G) => ((A @ D @ F) = (A @ E @ G)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_equals__rsp)).
% 50.45/34.27 thf(449,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA,F:TA,G:TA]: ((quotient3 @ TA @ TB @ (A) @ (B) @ (C)) => ((A @ D @ E) => ((A @ F @ G) => ((A @ D @ F) = (A @ E @ G)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 50.45/34.27 thf(126,axiom,((! [TA: $tType]: ((top_top @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_top__empty__eq)).
% 50.45/34.27 thf(655,plain,((! [TA: $tType]: ((top_top @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 50.45/34.27 thf(250,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => ((! [C:TA]: ((A @ C) => (C = B))) => ((hilbert_Eps @ TA @ A) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_some__equality)).
% 50.45/34.27 thf(1078,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => ((! [C:TA]: ((A @ C) => (C = B))) => ((hilbert_Eps @ TA @ (A)) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 50.45/34.27 thf(93,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ B)) = (B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_mem__Collect__eq)).
% 50.45/34.27 thf(550,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ (B))) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 50.45/34.27 thf(160,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) = (A = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_all__not__in__conv)).
% 50.45/34.27 thf(747,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) = (A = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 50.45/34.27 thf(29,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((bij_betw @ TA @ TB @ A @ (top_top @ (set @ TA)) @ (top_top @ (set @ TB))) => (inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_bij__is__inj)).
% 50.45/34.27 thf(340,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((bij_betw @ TA @ TB @ (A) @ (top_top @ (set @ TA)) @ (top_top @ (set @ TB))) => (inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 50.45/34.27 thf(90,axiom,((! [TA: $tType]: (! [A:(TA > TA),B:TA,C:TA]: ((hilbert_bijection @ TA @ A) => (((A @ B) = (A @ C)) => (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_bijection_OeqI)).
% 50.45/34.27 thf(538,plain,((! [TA: $tType]: (! [A:(TA > TA),B:TA,C:TA]: ((hilbert_bijection @ TA @ (A)) => (((A @ B) = (A @ C)) => (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 50.45/34.27 thf(216,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:TA]: ((A = (B @ C)) => (member @ TB @ A @ (image @ TA @ TB @ B @ (top_top @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_range__eqI)).
% 50.45/34.27 thf(930,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:TA]: ((A = (B @ C)) => (member @ TB @ A @ (image @ TA @ TB @ (B) @ (top_top @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 50.45/34.27 thf(131,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: (inj_on @ TA @ TB @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_inj__on__empty)).
% 50.45/34.27 thf(670,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: (inj_on @ TA @ TB @ (A) @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 50.45/34.27 thf(50,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ TB),B:TA]: (((A = (bot_bot @ (set @ TB))) => ((image @ TB @ TA @ (^ [C:TB]: (B)) @ A) = (bot_bot @ (set @ TA)))) & ((A != (bot_bot @ (set @ TB))) => ((image @ TB @ TA @ (^ [C:TB]: (B)) @ A) = (insert @ TA @ B @ (bot_bot @ (set @ TA))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_image__constant__conv)).
% 50.45/34.27 thf(404,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ TB),B:TA]: (((A = (bot_bot @ (set @ TB))) => ((image @ TB @ TA @ (^ [C:TB]: (B)) @ A) = (bot_bot @ (set @ TA)))) & ((~ (A = (bot_bot @ (set @ TB)))) => ((image @ TB @ TA @ (^ [C:TB]: (B)) @ A) = (insert @ TA @ B @ (bot_bot @ (set @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 50.45/34.27 thf(146,axiom,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_emptyE)).
% 50.45/34.27 thf(709,plain,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 50.45/34.27 thf(202,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_Diff__empty)).
% 50.45/34.27 thf(885,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 50.45/34.27 thf(22,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(set @ TA),C:TB,D:(TA > TB)]: ((member @ TA @ A @ B) => ((C = (D @ A)) => (member @ TB @ C @ (image @ TA @ TB @ D @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_rev__image__eqI)).
% 50.45/34.27 thf(320,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(set @ TA),C:TB,D:(TA > TB)]: ((member @ TA @ A @ B) => ((C = (D @ A)) => (member @ TB @ C @ (image @ TA @ TB @ (D) @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 50.45/34.27 thf(98,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((A != (bot_bot @ (set @ TA))) => ((! [B:TA,C:TA]: ((member @ TA @ B @ A) => ((member @ TA @ C @ A) => (B = C)))) => (is_singleton @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_is__singletonI_H)).
% 50.45/34.27 thf(565,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((~ (A = (bot_bot @ (set @ TA)))) => ((! [B:TA,C:TA]: ((member @ TA @ B @ A) => ((member @ TA @ C @ A) => (B = C)))) => (is_singleton @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 50.45/34.27 thf(245,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:((set @ TA) > TB),C:(TB > (set @ TA)),D:TB]: ((quot_type @ TA @ TB @ A @ B @ C) => ((quot_rep @ TB @ TA @ C @ D) = (hilbert_Eps @ TA @ (^ [E:TA]: (member @ TA @ E @ (C @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_quot__type_Orep__def)).
% 50.45/34.27 thf(1055,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:((set @ TA) > TB),C:(TB > (set @ TA)),D:TB]: ((quot_type @ TA @ TB @ (A) @ (B) @ (C)) => ((quot_rep @ TB @ TA @ (C) @ D) = (hilbert_Eps @ TA @ (^ [E:TA]: (member @ TA @ E @ (C @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 50.45/34.27 thf(104,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((bij_betw @ TA @ TB @ A @ (top_top @ (set @ TA)) @ (top_top @ (set @ TB))) => ((hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ (hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_inv__inv__eq)).
% 50.45/34.27 thf(587,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((bij_betw @ TA @ TB @ (A) @ (top_top @ (set @ TA)) @ (top_top @ (set @ TB))) => ((hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ (hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A)) = (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 50.45/34.27 thf(213,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ TB),B:(TB > TA),C:TA,D:TA]: (((hilbert_inv_into @ TB @ TA @ A @ B @ C) = (hilbert_inv_into @ TB @ TA @ A @ B @ D)) => ((member @ TA @ C @ (image @ TB @ TA @ B @ A)) => ((member @ TA @ D @ (image @ TB @ TA @ B @ A)) => (C = D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_inv__into__injective)).
% 50.45/34.27 thf(917,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ TB),B:(TB > TA),C:TA,D:TA]: (((hilbert_inv_into @ TB @ TA @ A @ (B) @ C) = (hilbert_inv_into @ TB @ TA @ A @ (B) @ D)) => ((member @ TA @ C @ (image @ TB @ TA @ (B) @ A)) => ((member @ TA @ D @ (image @ TB @ TA @ (B) @ A)) => (C = D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 50.45/34.27 thf(176,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TA]: (((image @ TB @ TA @ A @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) => ((A @ (hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A @ B)) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_surj__f__inv__f)).
% 50.45/34.27 thf(802,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TA]: (((image @ TB @ TA @ (A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) => ((A @ (hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ (A) @ B)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 50.45/34.27 thf(31,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(set @ TA)]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) => (((image @ TA @ TB @ A @ B) = (image @ TA @ TB @ A @ C)) = (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_inj__image__eq__iff)).
% 50.45/34.27 thf(344,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(set @ TA)]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) => (((image @ TA @ TB @ (A) @ B) = (image @ TA @ TB @ (A) @ C)) = (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 50.45/34.27 thf(217,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TB > $o)),B:((set @ TB) > TA),C:(TA > (set @ TB)),D:TA,E:TA]: ((quot_type @ TB @ TA @ A @ B @ C) => (((C @ D) = (C @ E)) = (D = E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_quot__type_Orep__inject)).
% 50.45/34.27 thf(934,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TB > $o)),B:((set @ TB) > TA),C:(TA > (set @ TB)),D:TA,E:TA]: ((quot_type @ TB @ TA @ (A) @ (B) @ (C)) => (((C @ D) = (C @ E)) = (D = E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 50.45/34.27 thf(34,axiom,((! [TA: $tType]: (! [A:TA]: (is_singleton @ TA @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_is__singletonI)).
% 50.45/34.27 thf(357,plain,((! [TA: $tType]: (! [A:TA]: (is_singleton @ TA @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 50.45/34.27 thf(208,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: (((bot_bot @ (set @ TA)) = (collect @ TA @ A)) = (! [B:TA]: ~ (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_empty__Collect__eq)).
% 50.45/34.27 thf(902,plain,((! [TA: $tType]: (! [A:(TA > $o)]: (((bot_bot @ (set @ TA)) = (collect @ TA @ (A))) = (! [B:TA]: ~ (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 50.45/34.27 thf(96,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA)]: ((bij_betw @ TA @ TB @ A @ B @ (bot_bot @ (set @ TB))) => (B = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_bij__betw__empty2)).
% 50.45/34.27 thf(559,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA)]: ((bij_betw @ TA @ TB @ (A) @ B @ (bot_bot @ (set @ TB))) => (B = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 50.45/34.27 thf(251,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:$o]: (((A @ (hilbert_Eps @ TA @ (^ [C:TA]: ~ (A @ C)))) = B) => ((! [C:TA]: (A @ C)) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_verit__sko__forall_H)).
% 50.45/34.27 thf(1087,plain,((! [TA: $tType]: (! [A:(TA > $o),B:$o]: (((A @ (hilbert_Eps @ TA @ (^ [C:TA]: ~ (A @ C)))) = B) => ((! [C:TA]: (A @ C)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 50.45/34.27 thf(12,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:TB,D:(set @ TB)]: ((inj_on @ TA @ TB @ A @ B) => ((~ (member @ TB @ C @ D)) => (((insert @ TB @ C @ D) = (image @ TA @ TB @ A @ B)) => (~ (! [E:TA,F:(set @ TA)]: ((~ (member @ TA @ E @ F)) => ((B = (insert @ TA @ E @ F)) => ((C = (A @ E)) => (D != (image @ TA @ TB @ A @ F))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_inj__img__insertE)).
% 50.45/34.27 thf(284,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:TB,D:(set @ TB)]: ((inj_on @ TA @ TB @ (A) @ B) => ((~ (member @ TB @ C @ D)) => (((insert @ TB @ C @ D) = (image @ TA @ TB @ (A) @ B)) => (~ (! [E:TA,F:(set @ TA)]: ((~ (member @ TA @ E @ F)) => ((B = (insert @ TA @ E @ F)) => ((C = (A @ E)) => (~ (D = (image @ TA @ TB @ (A) @ F)))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 50.45/34.27 thf(54,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:TA,D:(set @ TA)]: ((A = (B @ C)) => ((member @ TA @ C @ D) => (member @ TB @ A @ (image @ TA @ TB @ B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_image__eqI)).
% 50.45/34.27 thf(416,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:TA,D:(set @ TA)]: ((A = (B @ C)) => ((member @ TA @ C @ D) => (member @ TB @ A @ (image @ TA @ TB @ (B) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 50.45/34.27 thf(78,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > TC),B:(TA > TB),C:(set @ TA)]: ((image @ TB @ TC @ A @ (image @ TA @ TB @ B @ C)) = (image @ TA @ TC @ (^ [D:TA]: (A @ (B @ D))) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_image__image)).
% 50.45/34.27 thf(492,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > TC),B:(TA > TB),C:(set @ TA)]: ((image @ TB @ TC @ (A) @ (image @ TA @ TB @ (B) @ C)) = (image @ TA @ TC @ (^ [D:TA]: (A @ (B @ D))) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 50.45/34.27 thf(163,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(TB > TA),C:(set @ TB)]: ((member @ TA @ A @ (image @ TB @ TA @ B @ C)) => ((B @ (hilbert_inv_into @ TB @ TA @ C @ B @ A)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_f__inv__into__f)).
% 50.45/34.27 thf(756,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(TB > TA),C:(set @ TB)]: ((member @ TA @ A @ (image @ TB @ TA @ (B) @ C)) => ((B @ (hilbert_inv_into @ TB @ TA @ C @ (B) @ A)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 50.45/34.27 thf(173,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:TA]: ((A = (bot_bot @ (set @ TA))) => (~ (member @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_equals0D)).
% 50.45/34.27 thf(789,plain,((! [TA: $tType]: (! [A:(set @ TA),B:TA]: ((A = (bot_bot @ (set @ TA))) => (~ (member @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 50.45/34.27 thf(123,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:TA,D:TA]: (((insert @ TA @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) = (insert @ TA @ C @ (insert @ TA @ D @ (bot_bot @ (set @ TA))))) = (((A = C) & (B = D)) | ((A = D) & (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_doubleton__eq__iff)).
% 50.45/34.27 thf(646,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:TA,D:TA]: (((insert @ TA @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) = (insert @ TA @ C @ (insert @ TA @ D @ (bot_bot @ (set @ TA))))) = (((A = C) & (B = D)) | ((A = D) & (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 50.45/34.27 thf(218,axiom,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_singletonI)).
% 50.45/34.27 thf(937,plain,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 50.45/34.27 thf(209,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:TA,D:TB]: ((inj_on @ TA @ TB @ A @ B) => ((member @ TA @ C @ B) => (((A @ C) = D) => ((hilbert_inv_into @ TA @ TB @ B @ A @ D) = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_inv__into__f__eq)).
% 50.45/34.27 thf(905,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:TA,D:TB]: ((inj_on @ TA @ TB @ (A) @ B) => ((member @ TA @ C @ B) => (((A @ C) = D) => ((hilbert_inv_into @ TA @ TB @ B @ (A) @ D) = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 50.45/34.27 thf(138,axiom,((! [TA: $tType]: ((bot_bot @ (set @ TA)) != (top_top @ (set @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_empty__not__UNIV)).
% 50.45/34.27 thf(687,plain,((! [TA: $tType]: (~ ((bot_bot @ (set @ TA)) = (top_top @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 50.45/34.27 thf(200,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:((set @ TA) > TB),C:(TB > (set @ TA)),D:TB]: ((quot_type @ TA @ TB @ A @ B @ C) => (? [E:TA]: ((A @ E @ E) & ((C @ D) = (collect @ TA @ (A @ E))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_quot__type_Orep__prop)).
% 50.45/34.27 thf(877,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:((set @ TA) > TB),C:(TB > (set @ TA)),D:TB]: ((quot_type @ TA @ TB @ (A) @ (B) @ (C)) => (? [E:TA]: ((A @ E @ E) & ((C @ D) = (collect @ TA @ (A @ E))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 50.45/34.27 thf(222,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((A = (hilbert_Eps @ TA @ (^ [C:TA]: ~ (B @ C)))) => ((! [C:TA]: (B @ C)) = (B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_verit__sko__forall__indirect)).
% 50.45/34.27 thf(956,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((A = (hilbert_Eps @ TA @ (^ [C:TA]: ~ (B @ C)))) => ((! [C:TA]: (B @ C)) = (B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 50.45/34.27 thf(197,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) => (A = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_equals0I)).
% 50.45/34.27 thf(866,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: ~ (member @ TA @ B @ A)) => (A = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 50.45/34.27 thf(47,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(set @ TA),C:(TA > TB)]: ((member @ TA @ A @ B) => (member @ TB @ (C @ A) @ (image @ TA @ TB @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_imageI)).
% 50.45/34.27 thf(396,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(set @ TA),C:(TA > TB)]: ((member @ TA @ A @ B) => (member @ TB @ (C @ A) @ (image @ TA @ TB @ (C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 50.45/34.27 thf(51,axiom,((! [TA: $tType,TB: $tType]: ((quot_abs @ TA @ TB) = (quot_abs @ TA @ TB)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_quot__type_Oabs_Ocong)).
% 50.45/34.27 thf(411,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 50.45/34.27 thf(58,axiom,((! [TA: $tType]: (! [A:(TA > TA)]: ((hilbert_bijection @ TA @ A) => (inj_on @ TA @ TA @ A @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_bijection_Oinj)).
% 50.45/34.27 thf(428,plain,((! [TA: $tType]: (! [A:(TA > TA)]: ((hilbert_bijection @ TA @ (A)) => (inj_on @ TA @ TA @ (A) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 50.45/34.27 thf(5,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((insert @ TA @ A @ (insert @ TA @ B @ C)) = (insert @ TA @ B @ (insert @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_insert__commute)).
% 50.45/34.27 thf(265,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((insert @ TA @ A @ (insert @ TA @ B @ C)) = (insert @ TA @ B @ (insert @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 50.45/34.27 thf(88,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > TB),D:(TA > TB)]: ((A = B) => ((! [E:TA]: ((member @ TA @ E @ B) => ((C @ E) = (D @ E)))) => ((image @ TA @ TB @ C @ A) = (image @ TA @ TB @ D @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_image__cong)).
% 50.45/34.27 thf(527,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > TB),D:(TA > TB)]: ((A = B) => ((! [E:TA]: ((member @ TA @ E @ B) => ((C @ E) = (D @ E)))) => ((image @ TA @ TB @ (C) @ A) = (image @ TA @ TB @ (D) @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 50.45/34.27 thf(19,axiom,((! [TA: $tType]: (! [A:(TA > TA)]: ((hilbert_bijection @ TA @ A) => (bij_betw @ TA @ TA @ A @ (top_top @ (set @ TA)) @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_bijection_Obij)).
% 50.45/34.27 thf(312,plain,((! [TA: $tType]: (! [A:(TA > TA)]: ((hilbert_bijection @ TA @ (A)) => (bij_betw @ TA @ TA @ (A) @ (top_top @ (set @ TA)) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 50.45/34.27 thf(65,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:(set @ TA)]: ((inj_on @ TA @ TB @ A @ (insert @ TA @ B @ C)) = ((inj_on @ TA @ TB @ A @ C) & ~ (member @ TB @ (A @ B) @ (image @ TA @ TB @ A @ (minus_minus @ (set @ TA) @ C @ (insert @ TA @ B @ (bot_bot @ (set @ TA))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_inj__on__insert)).
% 50.45/34.27 thf(452,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:(set @ TA)]: ((inj_on @ TA @ TB @ (A) @ (insert @ TA @ B @ C)) = ((inj_on @ TA @ TB @ (A) @ C) & ~ (member @ TB @ (A @ B) @ (image @ TA @ TB @ (A) @ (minus_minus @ (set @ TA) @ C @ (insert @ TA @ B @ (bot_bot @ (set @ TA))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 50.45/34.27 thf(214,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:((set @ TA) > TB),C:(TB > (set @ TA)),D:(set @ TA)]: ((quot_type @ TA @ TB @ A @ B @ C) => ((? [E:TA]: ((A @ E @ E) & (D = (collect @ TA @ (A @ E))))) => ((C @ (B @ D)) = D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_quot__type_Oabs__inverse)).
% 50.45/34.27 thf(920,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:((set @ TA) > TB),C:(TB > (set @ TA)),D:(set @ TA)]: ((quot_type @ TA @ TB @ (A) @ (B) @ (C)) => ((? [E:TA]: ((A @ E @ E) & (D = (collect @ TA @ (A @ E))))) => ((C @ (B @ D)) = D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 50.45/34.27 thf(128,axiom,((! [TA: $tType]: ((insert @ TA) = (^ [A:TA,B:(set @ TA)]: (collect @ TA @ (^ [C:TA]: ((C = A) | (member @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_insert__compr)).
% 50.45/34.27 thf(661,plain,((! [TA: $tType]: ((insert @ TA) = (^ [A:TA,B:(set @ TA)]: (collect @ TA @ (^ [C:TA]: ((C = A) | (member @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 50.45/34.27 thf(174,axiom,((! [TA: $tType]: (! [A:$o]: (((A) => ((collect @ TA @ (^ [B:TA]: (A))) = (top_top @ (set @ TA)))) & ((~ (A)) => ((collect @ TA @ (^ [B:TA]: (A))) = (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_Collect__const)).
% 50.45/34.27 thf(793,plain,((! [TA: $tType]: (! [A:$o]: (((A) => ((collect @ TA @ (^ [B:TA]: (A))) = (top_top @ (set @ TA)))) & ((~ (A)) => ((collect @ TA @ (^ [B:TA]: (A))) = (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 50.45/34.27 thf(38,axiom,((! [TA: $tType]: ((ab_group_add @ TA) => (! [A:TA]: (inj_on @ TA @ TA @ (^ [B:TA]: (minus_minus @ TA @ B @ A)) @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_inj__diff__right)).
% 50.45/34.27 thf(366,plain,((! [TA: $tType]: ((ab_group_add @ TA) => (! [A:TA]: (inj_on @ TA @ TA @ (^ [B:TA]: (minus_minus @ TA @ B @ A)) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 50.45/34.27 thf(148,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:TA]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) => (((A @ B) = (A @ C)) = (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_inj__eq)).
% 50.45/34.27 thf(714,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:TA]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) => (((A @ B) = (A @ C)) = (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 50.45/34.27 thf(84,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (insert @ TA @ B @ C)) => ((A != B) => (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_insertE)).
% 50.45/34.27 thf(512,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (insert @ TA @ B @ C)) => ((~ (A = B)) => (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 50.45/34.27 thf(220,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((? [C:TA]: (A @ C)) => ((! [C:TA]: ((A @ C) => (B @ C))) => (B @ (hilbert_Eps @ TA @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_someI2__ex)).
% 50.45/34.27 thf(942,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((? [C:TA]: (A @ C)) => ((! [C:TA]: ((A @ C) => (B @ C))) => (B @ (hilbert_Eps @ TA @ (A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 50.45/34.27 thf(252,axiom,((! [TA: $tType,TB: $tType]: ((bNF_Greatest_univ @ TA @ TB) = (^ [A:(TA > TB),B:(set @ TA)]: (A @ (hilbert_Eps @ TA @ (^ [C:TA]: (member @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_univ__def)).
% 50.45/34.27 thf(1091,plain,((! [TA: $tType,TB: $tType]: ((bNF_Greatest_univ @ TA @ TB) = (^ [A:(TA > TB),B:(set @ TA)]: (A @ (hilbert_Eps @ TA @ (^ [C:TA]: (member @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 50.45/34.27 thf(183,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (minus_minus @ (set @ TA) @ B @ C)) => (~ (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_DiffD2)).
% 50.45/34.27 thf(825,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (minus_minus @ (set @ TA) @ B @ C)) => (~ (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 50.45/34.27 thf(241,axiom,((! [TA: $tType,TB: $tType]: ((bNF_Gr932048252omCard @ TA @ TB) = (^ [A:(set @ TA),B:(set @ (product_prod @ TB @ TB)),C:TB]: (hilbert_Eps @ TA @ (^ [D:TA]: ((member @ TA @ D @ A) & ((bNF_Greatest_toCard @ TA @ TB @ A @ B @ D) = C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_fromCard__def)).
% 50.45/34.27 thf(1042,plain,((! [TA: $tType,TB: $tType]: ((bNF_Gr932048252omCard @ TA @ TB) = (^ [A:(set @ TA),B:(set @ (product_prod @ TB @ TB)),C:TB]: (hilbert_Eps @ TA @ (^ [D:TA]: ((member @ TA @ D @ A) & ((bNF_Greatest_toCard @ TA @ TB @ A @ B @ D) = C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 50.45/34.27 thf(108,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((! [B:TA,C:TA]: (((A @ B) = (A @ C)) => (B = C))) => (inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_injI)).
% 50.45/34.27 thf(598,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((! [B:TA,C:TA]: (((A @ B) = (A @ C)) => (B = C))) => (inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 50.45/34.27 thf(181,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((insert @ TA @ A @ B) != (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_insert__not__empty)).
% 50.45/34.27 thf(820,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ~ ((insert @ TA @ A @ B) = (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 50.45/34.27 thf(45,axiom,((bot @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Obot_6)).
% 50.45/34.27 thf(392,plain,((bot @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 50.45/34.27 thf(14,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: ((bij_betw @ TB @ TA @ A @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA))) => ((image @ TB @ TA @ A @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_bij__is__surj)).
% 50.45/34.27 thf(297,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: ((bij_betw @ TB @ TA @ (A) @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA))) => ((image @ TB @ TA @ (A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 50.45/34.27 thf(179,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: (member @ TA @ B @ A)) => ((top_top @ (set @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_UNIV__eq__I)).
% 50.45/34.27 thf(815,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((! [B:TA]: (member @ TA @ B @ A)) => ((top_top @ (set @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 50.45/34.27 thf(154,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((lattic1534546155max_on @ TA @ TB) = (^ [A:(TA > TB),B:(set @ TA)]: (lattices_ord_arg_max @ TA @ TB @ A @ (^ [C:TA]: (member @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_arg__max__on__def)).
% 50.45/34.27 thf(729,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((lattic1534546155max_on @ TA @ TB) = (^ [A:(TA > TB),B:(set @ TA)]: (lattices_ord_arg_max @ TA @ TB @ A @ (^ [C:TA]: (member @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 50.45/34.27 thf(236,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => (A @ (hilbert_Eps @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_someI)).
% 50.45/34.27 thf(1021,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => (A @ (hilbert_Eps @ TA @ (A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 50.45/34.27 thf(169,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((member @ TA @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_singleton__iff)).
% 50.45/34.27 thf(778,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((member @ TA @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 50.45/34.27 thf(140,axiom,((ord @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oord_5)).
% 50.45/34.27 thf(693,plain,((ord @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 50.45/34.27 thf(117,axiom,((! [TA: $tType]: (! [A:(TA > TA),B:TA]: ((hilbert_bijection @ TA @ A) => ((A @ (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A @ B)) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_bijection_Oinv__right)).
% 50.45/34.27 thf(630,plain,((! [TA: $tType]: (! [A:(TA > TA),B:TA]: ((hilbert_bijection @ TA @ (A)) => ((A @ (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ (A) @ B)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 50.45/34.27 thf(239,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((? [C:TA]: (A @ C)) => ((B = (hilbert_Eps @ TA @ A)) => (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_exE__some)).
% 50.45/34.27 thf(1032,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((? [C:TA]: (A @ C)) => ((B = (hilbert_Eps @ TA @ (A))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 50.45/34.27 thf(60,axiom,((! [TA: $tType]: ((remove @ TA) = (^ [A:TA,B:(set @ TA)]: (minus_minus @ (set @ TA) @ B @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_254_remove__def)).
% 50.45/34.27 thf(435,plain,((! [TA: $tType]: ((remove @ TA) = (^ [A:TA,B:(set @ TA)]: (minus_minus @ (set @ TA) @ B @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 50.45/34.27 thf(185,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((minus_minus @ (set @ TA) @ (insert @ TA @ A @ B) @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_Diff__insert__absorb)).
% 50.45/34.27 thf(830,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((minus_minus @ (set @ TA) @ (insert @ TA @ A @ B) @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 50.45/34.27 thf(68,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (insert @ TA @ B @ C)) = ((A = B) | (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_insert__iff)).
% 50.45/34.27 thf(461,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (insert @ TA @ B @ C)) = ((A = B) | (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 50.45/34.27 thf(189,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(TA > TB)]: ((! [C:TA]: ((A @ (B @ C)) = C)) => ((image @ TB @ TA @ A @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_surjI)).
% 50.45/34.27 thf(842,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(TA > TB)]: ((! [C:TA]: ((A @ (B @ C)) = C)) => ((image @ TB @ TA @ (A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 50.45/34.27 thf(235,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((? [C:TA]: ((A @ C) & ! [D:TA]: ((A @ D) => (D = C)))) => ((A @ B) => ((hilbert_Eps @ TA @ A) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_some1__equality)).
% 50.45/34.27 thf(1012,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((? [C:TA]: ((A @ C) & ! [D:TA]: ((A @ D) => (D = C)))) => ((A @ B) => ((hilbert_Eps @ TA @ (A)) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 50.45/34.27 thf(23,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(TB > $o)]: ((! [D:TB]: ((member @ TB @ D @ (image @ TA @ TB @ A @ B)) => (C @ D))) => (! [D:TA]: ((member @ TA @ D @ B) => (C @ (A @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_164_ball__imageD)).
% 50.45/34.27 thf(324,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(TB > $o)]: ((! [D:TB]: ((member @ TB @ D @ (image @ TA @ TB @ (A) @ B)) => (C @ D))) => (! [D:TA]: ((member @ TA @ D @ B) => (C @ (A @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 50.45/34.27 thf(225,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: ((hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A) = (^ [B:TA]: (hilbert_Eps @ TB @ (^ [C:TB]: ((A @ C) = B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_inv__def)).
% 50.45/34.27 thf(974,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: ((hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A) = (^ [B:TA]: (hilbert_Eps @ TB @ (^ [C:TB]: ((A @ C) = B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 50.45/34.27 thf(142,axiom,((! [TA: $tType]: (! [A:(TA > TA),B:TA]: ((hilbert_bijection @ TA @ A) => ((hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A @ (A @ B)) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_bijection_Oinv__left)).
% 50.45/34.27 thf(697,plain,((! [TA: $tType]: (! [A:(TA > TA),B:TA]: ((hilbert_bijection @ TA @ (A)) => ((hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ (A) @ (A @ B)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 50.45/34.27 thf(21,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TB > $o)),B:(TB > TA),C:(TA > TB),D:TA,E:TA]: ((quotient3 @ TB @ TA @ A @ B @ C) => ((A @ (C @ D) @ (C @ E)) = (D = E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_Quotient3__rel__rep)).
% 50.45/34.27 thf(317,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TB > $o)),B:(TB > TA),C:(TA > TB),D:TA,E:TA]: ((quotient3 @ TB @ TA @ (A) @ (B) @ (C)) => ((A @ (C @ D) @ (C @ E)) = (D = E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 50.45/34.27 thf(227,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:TA]: (((hilbert_Eps @ TA @ A) = B) => ((A @ C) => (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_some__eq__imp)).
% 50.45/34.27 thf(980,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:TA]: (((hilbert_Eps @ TA @ (A)) = B) => ((A @ C) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 50.45/34.27 thf(233,axiom,((! [TA: $tType,TB: $tType]: ((hilbert_inv_into @ TA @ TB) = (^ [A:(set @ TA),B:(TA > TB),C:TB]: (hilbert_Eps @ TA @ (^ [D:TA]: ((member @ TA @ D @ A) & ((B @ D) = C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_inv__into__def)).
% 50.45/34.27 thf(1006,plain,((! [TA: $tType,TB: $tType]: ((hilbert_inv_into @ TA @ TB) = (^ [A:(set @ TA),B:(TA > TB),C:TB]: (hilbert_Eps @ TA @ (^ [D:TA]: ((member @ TA @ D @ A) & ((B @ D) = C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 50.45/34.27 thf(198,axiom,((! [TA: $tType]: (? [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_UNIV__witness)).
% 50.45/34.27 thf(869,plain,((! [TA: $tType]: (? [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 50.45/34.27 thf(111,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: (((A @ B) => ((collect @ TA @ (^ [C:TA]: ((C = B) & (A @ C)))) = (insert @ TA @ B @ (bot_bot @ (set @ TA))))) & ((~ (A @ B)) => ((collect @ TA @ (^ [C:TA]: ((C = B) & (A @ C)))) = (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_Collect__conv__if)).
% 50.45/34.27 thf(610,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: (((A @ B) => ((collect @ TA @ (^ [C:TA]: ((C = B) & (A @ C)))) = (insert @ TA @ B @ (bot_bot @ (set @ TA))))) & ((~ (A @ B)) => ((collect @ TA @ (^ [C:TA]: ((C = B) & (A @ C)))) = (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 50.45/34.27 thf(55,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((insert @ TA @ A @ (insert @ TA @ A @ B)) = (insert @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_insert__absorb2)).
% 50.45/34.27 thf(420,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((insert @ TA @ A @ (insert @ TA @ A @ B)) = (insert @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 50.45/34.27 thf(194,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((collect @ TB @ (^ [B:TB]: ? [C:TA]: (B = (A @ C)))) = (image @ TA @ TB @ A @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_full__SetCompr__eq)).
% 50.45/34.27 thf(857,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((collect @ TB @ (^ [B:TB]: ? [C:TA]: (B = (A @ C)))) = (image @ TA @ TB @ (A) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 50.45/34.27 thf(72,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(TA > TB),C:(TB > (TB > $o))]: ((! [D:TA]: ((A @ (B @ D)) = D)) => ((! [D:TA]: (C @ (B @ D) @ (B @ D))) => ((! [D:TB,E:TB]: ((C @ D @ E) = ((C @ D @ D) & (C @ E @ E) & ((A @ D) = (A @ E))))) => (quotient3 @ TB @ TA @ C @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_Quotient3I)).
% 50.45/34.27 thf(471,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(TA > TB),C:(TB > (TB > $o))]: ((! [D:TA]: ((A @ (B @ D)) = D)) => ((! [D:TA]: (C @ (B @ D) @ (B @ D))) => ((! [D:TB,E:TB]: ((C @ D @ E) = ((C @ D @ D) & (C @ E @ E) & ((A @ D) = (A @ E))))) => (quotient3 @ TB @ TA @ (C) @ (A) @ (B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 50.45/34.27 thf(162,axiom,((! [TA: $tType]: (! [A:(TA > TA)]: ((hilbert_bijection @ TA @ A) => ((image @ TA @ TA @ (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A) @ (top_top @ (set @ TA))) = (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_bijection_Osurj__inv)).
% 50.45/34.27 thf(753,plain,((! [TA: $tType]: (! [A:(TA > TA)]: ((hilbert_bijection @ TA @ (A)) => ((image @ TA @ TA @ (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A) @ (top_top @ (set @ TA))) = (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 50.45/34.27 thf(249,axiom,((! [TA: $tType,TB: $tType]: ((bNF_Greatest_toCard @ TA @ TB) = (^ [A:(set @ TA),B:(set @ (product_prod @ TB @ TB))]: (hilbert_Eps @ (TA > TB) @ (bNF_Gr1978856366d_pred @ TA @ TB @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_toCard__def)).
% 50.45/34.27 thf(1075,plain,((! [TA: $tType,TB: $tType]: ((bNF_Greatest_toCard @ TA @ TB) = (^ [A:(set @ TA),B:(set @ (product_prod @ TB @ TB))]: (hilbert_Eps @ (TA > TB) @ (bNF_Gr1978856366d_pred @ TA @ TB @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 50.45/34.27 thf(121,axiom,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_empty__iff)).
% 50.45/34.27 thf(642,plain,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 50.45/34.27 thf(77,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((insert @ TA @ A @ (collect @ TA @ B)) = (collect @ TA @ (^ [C:TA]: ((C != A) => (B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_insert__Collect)).
% 50.45/34.27 thf(489,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((insert @ TA @ A @ (collect @ TA @ (B))) = (collect @ TA @ (^ [C:TA]: ((~ (C = A)) => (B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 50.45/34.27 thf(105,axiom,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_iso__tuple__UNIV__I)).
% 50.45/34.27 thf(590,plain,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 50.45/34.27 thf(145,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: (((image @ TB @ TA @ A @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) => (inj_on @ TA @ TB @ (hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A) @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_surj__imp__inj__inv)).
% 50.45/34.27 thf(706,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: (((image @ TB @ TA @ (A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) => (inj_on @ TA @ TB @ (hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 50.45/34.27 thf(135,axiom,((! [TA: $tType]: (! [A:(TA > TA)]: ((hilbert_bijection @ TA @ A) => (inj_on @ TA @ TA @ (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A) @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_bijection_Oinj__inv)).
% 50.45/34.27 thf(679,plain,((! [TA: $tType]: (! [A:(TA > TA)]: ((hilbert_bijection @ TA @ (A)) => (inj_on @ TA @ TA @ (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 50.45/34.27 thf(240,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((lattices_ord_arg_max @ TA @ TB) = (^ [A:(TA > TB),B:(TA > $o)]: (hilbert_Eps @ TA @ (lattic2130478198rg_max @ TA @ TB @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_arg__max__def)).
% 50.45/34.27 thf(1039,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((lattices_ord_arg_max @ TA @ TB) = (^ [A:(TA > TB),B:(TA > $o)]: (hilbert_Eps @ TA @ (lattic2130478198rg_max @ TA @ TB @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 50.45/34.27 thf(224,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((A = (hilbert_Eps @ TA @ B)) => ((? [C:TA]: (B @ C)) = (B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_verit__sko__ex__indirect)).
% 50.45/34.27 thf(970,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((A = (hilbert_Eps @ TA @ (B))) => ((? [C:TA]: (B @ C)) = (B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 50.45/34.27 thf(46,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(TA > $o)]: ((collect @ TB @ (^ [C:TB]: ? [D:TA]: ((C = (A @ D)) & (B @ D)))) = (image @ TA @ TB @ A @ (collect @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_setcompr__eq__image)).
% 50.45/34.27 thf(393,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(TA > $o)]: ((collect @ TB @ (^ [C:TB]: ? [D:TA]: ((C = (A @ D)) & (B @ D)))) = (image @ TA @ TB @ (A) @ (collect @ TA @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 50.45/34.27 thf(85,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:(set @ TA)]: ((member @ TB @ A @ (image @ TA @ TB @ B @ C)) = (? [D:TA]: ((member @ TA @ D @ C) & (A = (B @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_image__iff)).
% 50.45/34.27 thf(515,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:(set @ TA)]: ((member @ TB @ A @ (image @ TA @ TB @ (B) @ C)) = (? [D:TA]: ((member @ TA @ D @ C) & (A = (B @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 50.45/34.27 thf(157,axiom,((! [TA: $tType]: (! [A:TA]: ((collect @ TA @ ((=) @ TA @ A)) = (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_singleton__conv2)).
% 50.45/34.27 thf(738,plain,((! [TA: $tType]: (! [A:TA]: ((collect @ TA @ ((=) @ TA @ A)) = (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 50.45/34.27 thf(243,axiom,((! [A:a]: ((p @ A) => (? [B:b]: (q @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 50.45/34.27 thf(1050,plain,((! [A:a]: ((p @ A) => (? [B:b]: (q @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 50.45/34.27 thf(211,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: (((collect @ TA @ A) = (bot_bot @ (set @ TA))) = (A = (bot_bot @ (TA > $o))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_Collect__empty__eq__bot)).
% 50.45/34.27 thf(911,plain,((! [TA: $tType]: (! [A:(TA > $o)]: (((collect @ TA @ (A)) = (bot_bot @ (set @ TA))) = ((A) = (bot_bot @ (TA > $o))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 50.45/34.27 thf(151,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TA > TC)]: ((inj_on @ TA @ TC @ A @ (top_top @ (set @ TA))) => (inj_on @ TA @ (TB > TC) @ (^ [B:TA,C:TB]: (A @ B)) @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_inj__fun)).
% 50.45/34.27 thf(721,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TA > TC)]: ((inj_on @ TA @ TC @ (A) @ (top_top @ (set @ TA))) => (inj_on @ TA @ (TB > TC) @ (^ [B:TA,C:TB]: (A @ B)) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 50.45/34.27 thf(40,axiom,((! [TA: $tType]: (! [A:(TA > TA)]: ((hilbert_bijection @ TA @ A) => ((image @ TA @ TA @ A @ (top_top @ (set @ TA))) = (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_bijection_Osurj)).
% 50.45/34.27 thf(371,plain,((! [TA: $tType]: (! [A:(TA > TA)]: ((hilbert_bijection @ TA @ (A)) => ((image @ TA @ TA @ (A) @ (top_top @ (set @ TA))) = (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 50.45/34.27 thf(118,axiom,((! [TA: $tType]: (! [A:TA]: ((collect @ TA @ (^ [B:TA]: (B = A))) = (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_singleton__conv)).
% 50.45/34.27 thf(633,plain,((! [TA: $tType]: (! [A:TA]: ((collect @ TA @ (^ [B:TA]: (B = A))) = (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 50.45/34.27 thf(177,axiom,((! [TA: $tType,TB: $tType]: (! [A:(set @ TA),B:(TA > TB),C:TA]: ((A != (bot_bot @ (set @ TA))) => ((! [D:TA]: ((member @ TA @ D @ A) => ((B @ D) = (B @ C)))) => ((the_elem @ TB @ (image @ TA @ TB @ B @ A)) = (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_the__elem__image__unique)).
% 50.45/34.27 thf(805,plain,((! [TA: $tType,TB: $tType]: (! [A:(set @ TA),B:(TA > TB),C:TA]: ((~ (A = (bot_bot @ (set @ TA)))) => ((! [D:TA]: ((member @ TA @ D @ A) => ((B @ D) = (B @ C)))) => ((the_elem @ TB @ (image @ TA @ TB @ (B) @ A)) = (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 50.45/34.27 thf(91,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) => ((hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A @ (A @ B)) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_inv__f__f)).
% 50.45/34.27 thf(541,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) => ((hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ (A) @ (A @ B)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 50.45/34.27 thf(166,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TB]: ((bij_betw @ TA @ TB @ A @ (top_top @ (set @ TA)) @ (top_top @ (set @ TB))) => (~ (! [C:TA]: ((B = (A @ C)) => (~ (! [D:TA]: ((B = (A @ D)) => (D = C))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_bij__pointE)).
% 50.45/34.27 thf(765,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TB]: ((bij_betw @ TA @ TB @ (A) @ (top_top @ (set @ TA)) @ (top_top @ (set @ TB))) => (~ (! [C:TA]: ((B = (A @ C)) => (~ (! [D:TA]: ((B = (A @ D)) => (D = C))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 50.45/34.27 thf(48,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((minus_minus @ (set @ TA) @ B @ (insert @ TA @ A @ C)) = (minus_minus @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_Diff__insert0)).
% 50.45/34.27 thf(398,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((minus_minus @ (set @ TA) @ B @ (insert @ TA @ A @ C)) = (minus_minus @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 50.45/34.27 thf(248,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o),C:(TA > $o)]: ((A = (hilbert_Eps @ TA @ (^ [D:TA]: ~ (B @ D)))) => ((! [D:TA]: ((B @ D) = (C @ D))) => ((! [D:TA]: (C @ D)) = (B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_verit__sko__forall__indirect2)).
% 50.45/34.27 thf(1071,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o),C:(TA > $o)]: ((A = (hilbert_Eps @ TA @ (^ [D:TA]: ~ (B @ D)))) => ((! [D:TA]: ((B @ D) = (C @ D))) => ((! [D:TA]: (C @ D)) = (B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 50.45/34.27 thf(133,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA]: (member @ TB @ (A @ B) @ (image @ TA @ TB @ A @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_rangeI)).
% 50.45/34.27 thf(674,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA]: (member @ TB @ (A @ B) @ (image @ TA @ TB @ (A) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 50.45/34.27 thf(237,axiom,((! [TA: $tType]: (((!) @ TA) = (^ [A:(TA > $o)]: (A @ (hilbert_Eps @ TA @ (^ [B:TA]: ~ (A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_verit__sko__forall)).
% 50.45/34.27 thf(1026,plain,((! [TA: $tType]: (((!) @ TA) = (^ [A:(TA > $o)]: (A @ (hilbert_Eps @ TA @ (^ [B:TA]: ~ (A @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 50.45/34.27 thf(203,axiom,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (bot_bot @ (TA > $o)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_bot__set__def)).
% 50.45/34.27 thf(888,plain,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (bot_bot @ (TA > $o)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 50.45/34.27 thf(52,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: ((member @ TA @ A @ B) => (member @ TA @ A @ (insert @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_insertI2)).
% 50.45/34.27 thf(412,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: ((member @ TA @ A @ B) => (member @ TA @ A @ (insert @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 50.45/34.27 thf(161,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_bot__fun__def)).
% 50.45/34.27 thf(750,plain,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 50.45/34.27 thf(113,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:TA]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) => (((A @ B) = (A @ C)) => (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_injD)).
% 50.45/34.27 thf(618,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:TA]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) => (((A @ B) = (A @ C)) => (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 50.45/34.27 thf(57,axiom,((! [TA: $tType]: ((ab_group_add @ TA) => (! [A:TA]: ((image @ TA @ TA @ (^ [B:TA]: (minus_minus @ TA @ B @ A)) @ (top_top @ (set @ TA))) = (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_surj__diff__right)).
% 50.45/34.27 thf(425,plain,((! [TA: $tType]: ((ab_group_add @ TA) => (! [A:TA]: ((image @ TA @ TA @ (^ [B:TA]: (minus_minus @ TA @ B @ A)) @ (top_top @ (set @ TA))) = (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 50.45/34.27 thf(59,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => (~ (! [C:(set @ TA)]: ((B = (insert @ TA @ A @ C)) => (member @ TA @ A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_Set_Oset__insert)).
% 50.45/34.27 thf(430,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => (~ (! [C:(set @ TA)]: ((B = (insert @ TA @ A @ C)) => (member @ TA @ A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 50.45/34.27 thf(10,axiom,((! [TA: $tType,TB: $tType]: ((top @ TA) => (top @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Otop)).
% 50.45/34.27 thf(279,plain,((! [TA: $tType,TB: $tType]: ((top @ TA) => (top @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 50.45/34.27 thf(99,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) = (! [B:TA,C:TA]: (((A @ B) = (A @ C)) => (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_inj__def)).
% 50.45/34.27 thf(573,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) = (! [B:TA,C:TA]: (((A @ B) = (A @ C)) => (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 50.45/34.27 thf(103,axiom,((! [TA: $tType]: (! [A:(TA > TA),B:TA,C:TA]: ((hilbert_bijection @ TA @ A) => (((hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A @ B) = (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A @ C)) = (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_bijection_Oeq__inv__iff)).
% 50.45/34.27 thf(584,plain,((! [TA: $tType]: (! [A:(TA > TA),B:TA,C:TA]: ((hilbert_bijection @ TA @ (A)) => (((hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ (A) @ B) = (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ (A) @ C)) = (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 50.45/34.27 thf(97,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((? [B:TA]: (member @ TA @ B @ A)) = (A != (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_ex__in__conv)).
% 50.45/34.27 thf(562,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((? [B:TA]: (member @ TA @ B @ A)) = (~ (A = (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 50.45/34.27 thf(56,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: (inj_on @ TA @ TA @ (^ [B:TA]: (B)) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_inj__on__id2)).
% 50.45/34.27 thf(423,plain,((! [TA: $tType]: (! [A:(set @ TA)]: (inj_on @ TA @ TA @ (^ [B:TA]: (B)) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 50.45/34.27 thf(141,axiom,((! [TA: $tType]: ((top_top @ (set @ TA)) = (collect @ TA @ (^ [A:TA]: (($true))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_UNIV__def)).
% 50.45/34.27 thf(694,plain,((! [TA: $tType]: ((top_top @ (set @ TA)) = (collect @ TA @ (^ [A:TA]: (($true))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 50.45/34.27 thf(155,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA]: ((image @ TB @ TA @ (^ [B:TB]: (A)) @ (top_top @ (set @ TB))) = (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_range__constant)).
% 50.45/34.27 thf(732,plain,((! [TA: $tType,TB: $tType]: (! [A:TA]: ((image @ TB @ TA @ (^ [B:TB]: (A)) @ (top_top @ (set @ TB))) = (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 50.45/34.27 thf(167,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(TA > TB)]: (((image @ TB @ TA @ A @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) => ((! [C:TB]: ((B @ (A @ C)) = C)) => ((hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_surj__imp__inv__eq)).
% 50.45/34.27 thf(772,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(TA > TB)]: (((image @ TB @ TA @ (A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) => ((! [C:TB]: ((B @ (A @ C)) = C)) => ((hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A) = (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 50.45/34.27 thf(147,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(set @ TB),D:TA]: ((bij_betw @ TA @ TB @ A @ B @ C) => ((member @ TA @ D @ B) => ((hilbert_inv_into @ TA @ TB @ B @ A @ (A @ D)) = D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_bij__betw__inv__into__left)).
% 50.45/34.27 thf(711,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(set @ TB),D:TA]: ((bij_betw @ TA @ TB @ (A) @ B @ C) => ((member @ TA @ D @ B) => ((hilbert_inv_into @ TA @ TB @ B @ (A) @ (A @ D)) = D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 50.45/34.27 thf(101,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((bij_betw @ TA @ TB @ A @ (top_top @ (set @ TA)) @ (top_top @ (set @ TB))) => (bij_betw @ TB @ TA @ (hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A) @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_bij__imp__bij__inv)).
% 50.45/34.27 thf(579,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((bij_betw @ TA @ TB @ (A) @ (top_top @ (set @ TA)) @ (top_top @ (set @ TB))) => (bij_betw @ TB @ TA @ (hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A) @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 50.45/34.27 thf(11,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((minus_minus @ (set @ TA) @ (minus_minus @ (set @ TA) @ A @ B) @ B) = (minus_minus @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_Diff__idemp)).
% 50.45/34.27 thf(281,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((minus_minus @ (set @ TA) @ (minus_minus @ (set @ TA) @ A @ B) @ B) = (minus_minus @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 50.45/34.27 thf(3,axiom,((! [TA: $tType]: ((ab_group_add @ TA) => (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((image @ TA @ TA @ (^ [D:TA]: (minus_minus @ TA @ D @ A)) @ (minus_minus @ (set @ TA) @ B @ C)) = (minus_minus @ (set @ TA) @ (image @ TA @ TA @ (^ [D:TA]: (minus_minus @ TA @ D @ A)) @ B) @ (image @ TA @ TA @ (^ [D:TA]: (minus_minus @ TA @ D @ A)) @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_translation__subtract__diff)).
% 50.45/34.27 thf(259,plain,((! [TA: $tType]: ((ab_group_add @ TA) => (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((image @ TA @ TA @ (^ [D:TA]: (minus_minus @ TA @ D @ A)) @ (minus_minus @ (set @ TA) @ B @ C)) = (minus_minus @ (set @ TA) @ (image @ TA @ TA @ (^ [D:TA]: (minus_minus @ TA @ D @ A)) @ B) @ (image @ TA @ TA @ (^ [D:TA]: (minus_minus @ TA @ D @ A)) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 50.45/34.27 thf(80,axiom,((! [TA: $tType]: ((hilbert_bijection @ TA) = (^ [A:(TA > TA)]: (bij_betw @ TA @ TA @ A @ (top_top @ (set @ TA)) @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_bijection__def)).
% 50.45/34.27 thf(498,plain,((! [TA: $tType]: ((hilbert_bijection @ TA) = (^ [A:(TA > TA)]: (bij_betw @ TA @ TA @ A @ (top_top @ (set @ TA)) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 50.45/34.27 thf(246,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o),C:(TA > $o)]: ((A = (hilbert_Eps @ TA @ B)) => ((! [D:TA]: ((B @ D) = (C @ D))) => ((? [D:TA]: (C @ D)) = (B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_verit__sko__ex__indirect2)).
% 50.45/34.27 thf(1058,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o),C:(TA > $o)]: ((A = (hilbert_Eps @ TA @ (B))) => ((! [D:TA]: ((B @ D) = (C @ D))) => ((? [D:TA]: (C @ D)) = (B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 50.45/34.27 thf(26,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA]: ((quotient3 @ TA @ TB @ A @ B @ C) => ((A @ D @ E) => (A @ D @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_Quotient3__refl1)).
% 50.45/34.27 thf(335,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA]: ((quotient3 @ TA @ TB @ (A) @ (B) @ (C)) => ((A @ D @ E) => (A @ D @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 50.45/34.27 thf(33,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(TB > $o)]: ((? [D:TB]: ((member @ TB @ D @ (image @ TA @ TB @ A @ B)) & (C @ D))) => (? [D:TA]: ((member @ TA @ D @ B) & (C @ (A @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_162_bex__imageD)).
% 50.45/34.27 thf(350,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(TB > $o)]: ((? [D:TB]: ((member @ TB @ D @ (image @ TA @ TB @ (A) @ B)) & (C @ D))) => (? [D:TA]: ((member @ TA @ D @ B) & (C @ (A @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 50.45/34.27 thf(132,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (minus_minus @ (set @ TA) @ B @ C)) => (member @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_DiffD1)).
% 50.45/34.27 thf(672,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (minus_minus @ (set @ TA) @ B @ C)) => (member @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 50.45/34.27 thf(109,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(TB > $o)]: ((bij_betw @ TB @ TA @ A @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA))) => ((image @ TB @ TA @ A @ (collect @ TB @ B)) = (collect @ TA @ (^ [C:TA]: (B @ (hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_bij__image__Collect__eq)).
% 50.45/34.27 thf(604,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(TB > $o)]: ((bij_betw @ TB @ TA @ (A) @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA))) => ((image @ TB @ TA @ (A) @ (collect @ TB @ (B))) = (collect @ TA @ (^ [C:TA]: (B @ (hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 50.45/34.27 thf(136,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: ((! [B:TB,C:TB]: (((A @ B) = (A @ C)) = (B = C))) => ((! [B:TA]: ? [C:TB]: (B = (A @ C))) => (bij_betw @ TB @ TA @ A @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_bijI_H)).
% 50.45/34.27 thf(681,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: ((! [B:TB,C:TB]: (((A @ B) = (A @ C)) = (B = C))) => ((! [B:TA]: ? [C:TB]: (B = (A @ C))) => (bij_betw @ TB @ TA @ (A) @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 50.45/34.27 thf(8,axiom,((! [TA: $tType]: (bot @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Obot_3)).
% 50.45/34.27 thf(274,plain,((! [TA: $tType]: (bot @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 50.45/34.27 thf(171,axiom,((! [TA: $tType]: (! [A:(TA > TA)]: ((hilbert_bijection @ TA @ A) => (bij_betw @ TA @ TA @ (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A) @ (top_top @ (set @ TA)) @ (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_bijection_Obij__inv)).
% 50.45/34.27 thf(784,plain,((! [TA: $tType]: (! [A:(TA > TA)]: ((hilbert_bijection @ TA @ (A)) => (bij_betw @ TA @ TA @ (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A) @ (top_top @ (set @ TA)) @ (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 50.45/34.27 thf(36,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA]: ((quotient3 @ TA @ TB @ A @ B @ C) => ((A @ D @ E) => (A @ E @ E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_Quotient3__refl2)).
% 50.45/34.27 thf(362,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA]: ((quotient3 @ TA @ TB @ (A) @ (B) @ (C)) => ((A @ D @ E) => (A @ E @ E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 50.45/34.27 thf(112,axiom,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_UNIV__I)).
% 50.45/34.27 thf(616,plain,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (top_top @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 50.45/34.27 thf(7,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((is_singleton @ TA @ A) => (~ (! [B:TA]: (A != (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_is__singletonE)).
% 50.45/34.27 thf(271,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((is_singleton @ TA @ A) => (~ (! [B:TA]: ~ (A = (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 50.45/34.27 thf(196,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => ((insert @ TA @ A @ (minus_minus @ (set @ TA) @ B @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_insert__Diff)).
% 50.45/34.27 thf(863,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => ((insert @ TA @ A @ (minus_minus @ (set @ TA) @ B @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 50.45/34.27 thf(42,axiom,((! [TA: $tType]: (! [A:(set @ (set @ TA)),B:TA,C:(set @ TA)]: ((! [D:(set @ TA)]: ((member @ (set @ TA) @ D @ A) => (~ (member @ TA @ B @ D)))) => ((member @ (set @ TA) @ C @ (image @ (set @ TA) @ (set @ TA) @ (insert @ TA @ B) @ A)) = ((member @ TA @ B @ C) & (member @ (set @ TA) @ (minus_minus @ (set @ TA) @ C @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_in__image__insert__iff)).
% 50.45/34.27 thf(377,plain,((! [TA: $tType]: (! [A:(set @ (set @ TA)),B:TA,C:(set @ TA)]: ((! [D:(set @ TA)]: ((member @ (set @ TA) @ D @ A) => (~ (member @ TA @ B @ D)))) => ((member @ (set @ TA) @ C @ (image @ (set @ TA) @ (set @ TA) @ (insert @ TA @ B) @ A)) = ((member @ TA @ B @ C) & (member @ (set @ TA) @ (minus_minus @ (set @ TA) @ C @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 50.45/34.27 thf(230,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(TA > $o)]: ((A = B) => (((hilbert_Eps @ TA @ C) = B) = ((hilbert_Eps @ TA @ C) = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_verit__sko__forall_H_H)).
% 50.45/34.27 thf(996,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(TA > $o)]: ((A = B) => (((hilbert_Eps @ TA @ (C)) = B) = ((hilbert_Eps @ TA @ (C)) = A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 50.45/34.27 thf(83,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((image @ TA @ TA @ (^ [B:TA]: (B)) @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_image__ident)).
% 50.45/34.27 thf(509,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((image @ TA @ TA @ (^ [B:TA]: (B)) @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 50.45/34.27 thf(124,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TB]: (((image @ TA @ TB @ A @ (top_top @ (set @ TA))) = (top_top @ (set @ TB))) => (~ (! [C:TA]: (B != (A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_surjE)).
% 50.45/34.27 thf(649,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TB]: (((image @ TA @ TB @ (A) @ (top_top @ (set @ TA))) = (top_top @ (set @ TB))) => (~ (! [C:TA]: ~ (B = (A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 50.45/34.27 thf(73,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TA) => (bot @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Obot)).
% 50.45/34.27 thf(477,plain,((! [TA: $tType,TB: $tType]: ((bot @ TA) => (bot @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 50.45/34.27 thf(178,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (minus_minus @ (set @ TA) @ B @ C)) => (~ ((member @ TA @ A @ B) => (member @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_DiffE)).
% 50.45/34.27 thf(811,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (minus_minus @ (set @ TA) @ B @ C)) => (~ ((member @ TA @ A @ B) => (member @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 50.45/34.27 thf(89,axiom,((! [TA: $tType]: ((is_singleton @ TA) = (^ [A:(set @ TA)]: ? [B:TA]: (A = (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_is__singleton__def)).
% 50.45/34.27 thf(535,plain,((! [TA: $tType]: ((is_singleton @ TA) = (^ [A:(set @ TA)]: ? [B:TA]: (A = (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 50.45/34.27 thf(114,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((minus_minus @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A) = (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_empty__Diff)).
% 50.45/34.27 thf(621,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((minus_minus @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A) = (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 50.45/34.27 thf(238,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((hilbert_Eps @ TA @ A) = (hilbert_Eps @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_Eps__cong)).
% 50.45/34.27 thf(1029,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((hilbert_Eps @ TA @ (A)) = (hilbert_Eps @ TA @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 50.45/34.27 thf(24,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(set @ TB)]: ((bij_betw @ TA @ TB @ A @ B @ C) => (bij_betw @ TB @ TA @ (hilbert_inv_into @ TA @ TB @ B @ A) @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_bij__betw__inv__into)).
% 50.45/34.27 thf(330,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(set @ TB)]: ((bij_betw @ TA @ TB @ (A) @ B @ C) => (bij_betw @ TB @ TA @ (hilbert_inv_into @ TA @ TB @ B @ A) @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 50.45/34.27 thf(175,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(set @ TA)]: ((bij_betw @ TB @ TA @ A @ (bot_bot @ (set @ TB)) @ B) => (B = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_bij__betw__empty1)).
% 50.45/34.27 thf(799,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(set @ TA)]: ((bij_betw @ TB @ TA @ (A) @ (bot_bot @ (set @ TB)) @ B) => (B = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 50.45/34.27 thf(153,axiom,((! [TA: $tType]: ((hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ (^ [A:TA]: (A))) = (^ [A:TA]: (A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_inv__identity)).
% 50.45/34.27 thf(726,plain,((! [TA: $tType]: ((hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ (^ [A:TA]: (A))) = (^ [A:TA]: (A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 50.45/34.27 thf(191,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:(set @ TA)]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) => ((member @ TB @ (A @ B) @ (image @ TA @ TB @ A @ C)) = (member @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_inj__image__mem__iff)).
% 50.45/34.27 thf(848,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:(set @ TA)]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) => ((member @ TB @ (A @ B) @ (image @ TA @ TB @ (A) @ C)) = (member @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 50.45/34.27 thf(143,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:((set @ TA) > TB),C:(TB > (set @ TA)),D:TA]: ((quot_type @ TA @ TB @ A @ B @ C) => ((quot_abs @ TA @ TB @ A @ B @ D) = (B @ (collect @ TA @ (A @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_quot__type_Oabs__def)).
% 50.45/34.27 thf(700,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:((set @ TA) > TB),C:(TB > (set @ TA)),D:TA]: ((quot_type @ TA @ TB @ (A) @ (B) @ (C)) => ((quot_abs @ TA @ TB @ (A) @ (B) @ D) = (B @ (collect @ TA @ (A @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 50.45/34.27 thf(87,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(set @ TA),C:(TA > TB),D:TB]: (((member @ TA @ A @ B) => ((image @ TA @ TB @ (fun_upd @ TA @ TB @ C @ A @ D) @ B) = (insert @ TB @ D @ (image @ TA @ TB @ C @ (minus_minus @ (set @ TA) @ B @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))))))) & ((~ (member @ TA @ A @ B)) => ((image @ TA @ TB @ (fun_upd @ TA @ TB @ C @ A @ D) @ B) = (image @ TA @ TB @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_255_fun__upd__image)).
% 50.45/34.27 thf(521,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(set @ TA),C:(TA > TB),D:TB]: (((member @ TA @ A @ B) => ((image @ TA @ TB @ (fun_upd @ TA @ TB @ C @ A @ D) @ B) = (insert @ TB @ D @ (image @ TA @ TB @ (C) @ (minus_minus @ (set @ TA) @ B @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))))))) & ((~ (member @ TA @ A @ B)) => ((image @ TA @ TB @ (fun_upd @ TA @ TB @ C @ A @ D) @ B) = (image @ TA @ TB @ (C) @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 50.45/34.27 thf(184,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA)]: ((collect @ TB @ (^ [C:TB]: ? [D:TA]: ((C = (A @ D)) & (member @ TA @ D @ B)))) = (image @ TA @ TB @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_Setcompr__eq__image)).
% 50.45/34.27 thf(827,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA)]: ((collect @ TB @ (^ [C:TB]: ? [D:TA]: ((C = (A @ D)) & (member @ TA @ D @ B)))) = (image @ TA @ TB @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 50.45/34.27 thf(119,axiom,((! [TA: $tType]: (! [A:(TA > TA),B:TA,C:TA]: ((hilbert_bijection @ TA @ A) => (((hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A @ B) = (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A @ C)) => (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_bijection_Oeq__invI)).
% 50.45/34.27 thf(636,plain,((! [TA: $tType]: (! [A:(TA > TA),B:TA,C:TA]: ((hilbert_bijection @ TA @ (A)) => (((hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ (A) @ B) = (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ (A) @ C)) => (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 50.45/34.27 thf(66,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => ((minus_minus @ (set @ TA) @ (insert @ TA @ A @ C) @ B) = (minus_minus @ (set @ TA) @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_insert__Diff1)).
% 50.45/34.27 thf(455,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => ((minus_minus @ (set @ TA) @ (insert @ TA @ A @ C) @ B) = (minus_minus @ (set @ TA) @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 50.45/34.27 thf(16,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: (inj_on @ TA @ (set @ TA) @ (^ [B:TA]: (insert @ TA @ B @ (bot_bot @ (set @ TA)))) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_inj__singleton)).
% 50.45/34.27 thf(306,plain,((! [TA: $tType]: (! [A:(set @ TA)]: (inj_on @ TA @ (set @ TA) @ (^ [B:TA]: (insert @ TA @ B @ (bot_bot @ (set @ TA)))) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 50.45/34.27 thf(231,axiom,((! [TA: $tType]: (! [A:TA]: ((hilbert_Eps @ TA @ (^ [B:TA]: (B = A))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_some__eq__trivial)).
% 50.45/34.27 thf(1000,plain,((! [TA: $tType]: (! [A:TA]: ((hilbert_Eps @ TA @ (^ [B:TA]: (B = A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 50.45/34.27 thf(192,axiom,((! [TA: $tType]: ((minus_minus @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) & ~ (member @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_set__diff__eq)).
% 50.45/34.27 thf(851,plain,((! [TA: $tType]: ((minus_minus @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) & ~ (member @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 50.45/34.27 thf(61,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((~ (member @ TA @ A @ C)) => (((insert @ TA @ A @ B) = (insert @ TA @ A @ C)) = (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_insert__ident)).
% 50.45/34.27 thf(438,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((~ (member @ TA @ A @ C)) => (((insert @ TA @ A @ B) = (insert @ TA @ A @ C)) = (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 50.45/34.27 thf(127,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(set @ TB),D:TA]: ((bij_betw @ TA @ TB @ A @ B @ C) => ((member @ TA @ D @ B) => ((hilbert_inv_into @ TB @ TA @ C @ (hilbert_inv_into @ TA @ TB @ B @ A) @ D) = (A @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_inv__into__inv__into__eq)).
% 50.45/34.27 thf(658,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(set @ TB),D:TA]: ((bij_betw @ TA @ TB @ (A) @ B @ C) => ((member @ TA @ D @ B) => ((hilbert_inv_into @ TB @ TA @ C @ (hilbert_inv_into @ TA @ TB @ B @ A) @ D) = (A @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 50.45/34.27 thf(1,conjecture,((! [A:a]: (~ (p @ A) | (q @ A @ (hilbert_Eps @ b @ (q @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1)).
% 50.45/34.27 thf(2,negated_conjecture,((~ (! [A:a]: (~ (p @ A) | (q @ A @ (hilbert_Eps @ b @ (q @ A))))))),inference(neg_conjecture,[status(cth)],[1])).
% 50.45/34.27 thf(255,plain,((~ (! [A:a]: (~ (p @ A) | (q @ A @ (hilbert_Eps @ b @ (q @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 50.45/34.27 thf(219,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: (((image @ TB @ TA @ A @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) = (! [B:TA]: ((A @ (hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A @ B)) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_surj__iff__all)).
% 50.45/34.27 thf(939,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: (((image @ TB @ TA @ (A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) = (! [B:TA]: ((A @ (hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ (A) @ B)) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 50.45/34.27 thf(30,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA]: ((quotient3 @ TA @ TB @ A @ B @ C) => ((A @ D @ E) => (A @ D @ (C @ (B @ E)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_rep__abs__rsp)).
% 50.45/34.27 thf(342,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA]: ((quotient3 @ TA @ TB @ (A) @ (B) @ (C)) => ((A @ D @ E) => (A @ D @ (C @ (B @ E)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 50.45/34.27 thf(94,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) => ((image @ TB @ TA @ (hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_inj__imp__surj__inv)).
% 50.45/34.27 thf(553,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB)]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) => ((image @ TB @ TA @ (hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 50.45/34.27 thf(187,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:TB]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) => (((A @ B) = C) => ((hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A @ C) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_inv__f__eq)).
% 50.45/34.27 thf(836,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:TB]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) => (((A @ B) = C) => ((hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ (A) @ C) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 50.45/34.27 thf(215,axiom,((! [TA: $tType]: ((top_top @ (set @ TA)) = (collect @ TA @ (top_top @ (TA > $o)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_top__set__def)).
% 50.45/34.27 thf(927,plain,((! [TA: $tType]: ((top_top @ (set @ TA)) = (collect @ TA @ (top_top @ (TA > $o)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 50.45/34.27 thf(41,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:(set @ TA)]: ((image @ TA @ TB @ A @ (insert @ TA @ B @ C)) = (insert @ TB @ (A @ B) @ (image @ TA @ TB @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_image__insert)).
% 50.45/34.27 thf(374,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:(set @ TA)]: ((image @ TA @ TB @ (A) @ (insert @ TA @ B @ C)) = (insert @ TB @ (A @ B) @ (image @ TA @ TB @ (A) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 50.45/34.27 thf(67,axiom,((! [TA: $tType,TB: $tType]: ((quotient3 @ TA @ TB) = (^ [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA)]: (! [D:TB]: ((B @ (C @ D)) = D) & ! [D:TB]: (A @ (C @ D) @ (C @ D)) & ! [D:TA,E:TA]: ((A @ D @ E) = ((A @ D @ D) & (A @ E @ E) & ((B @ D) = (B @ E))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_Quotient3__def)).
% 50.45/34.27 thf(458,plain,((! [TA: $tType,TB: $tType]: ((quotient3 @ TA @ TB) = (^ [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA)]: (! [D:TB]: ((B @ (C @ D)) = D) & ! [D:TB]: (A @ (C @ D) @ (C @ D)) & ! [D:TA,E:TA]: ((A @ D @ E) = ((A @ D @ D) & (A @ E @ E) & ((B @ D) = (B @ E))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 50.45/34.27 thf(182,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => ((~ (member @ TA @ A @ C)) => (member @ TA @ A @ (minus_minus @ (set @ TA) @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_DiffI)).
% 50.45/34.27 thf(823,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => ((~ (member @ TA @ A @ C)) => (member @ TA @ A @ (minus_minus @ (set @ TA) @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 50.45/34.27 thf(232,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((bNF_pick_middlep @ TA @ TB @ TC) = (^ [A:(TA > (TB > $o)),B:(TB > (TC > $o)),C:TA,D:TC]: (hilbert_Eps @ TB @ (^ [E:TB]: ((A @ C @ E) & (B @ E @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_pick__middlep__def)).
% 50.45/34.27 thf(1003,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((bNF_pick_middlep @ TA @ TB @ TC) = (^ [A:(TA > (TB > $o)),B:(TB > (TC > $o)),C:TA,D:TC]: (hilbert_Eps @ TB @ (^ [E:TB]: ((A @ C @ E) & (B @ E @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 50.45/34.27 thf(139,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA)]: (((image @ TA @ TB @ A @ B) = (bot_bot @ (set @ TB))) = (B = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_image__is__empty)).
% 50.45/34.27 thf(690,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA)]: (((image @ TA @ TB @ (A) @ B) = (bot_bot @ (set @ TB))) = (B = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 50.45/34.27 thf(53,axiom,((! [TA: $tType]: (! [A:TA]: (top_top @ (TA > $o) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_top1I)).
% 50.45/34.27 thf(414,plain,((! [TA: $tType]: (! [A:TA]: (top_top @ (TA > $o) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 50.45/34.27 thf(229,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: ((A @ (hilbert_Eps @ TA @ A)) = (? [B:TA]: (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_some__eq__ex)).
% 50.45/34.27 thf(993,plain,((! [TA: $tType]: (! [A:(TA > $o)]: ((A @ (hilbert_Eps @ TA @ (A))) = (? [B:TA]: (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 50.45/34.27 thf(254,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:TA]: ((A @ B) => ((~ (A @ C)) => (((hilbert_Eps @ TA @ A) = C) => ((hilbert_Eps @ TA @ A) = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_Nitpick_OEps__psimp)).
% 50.45/34.27 thf(1098,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:TA]: ((A @ B) => ((~ (A @ C)) => (((hilbert_Eps @ TA @ (A)) = C) => ((hilbert_Eps @ TA @ (A)) = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 50.45/34.27 thf(18,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TB > $o)),B:(TB > TA),C:(TA > TB),D:TA]: ((quotient3 @ TB @ TA @ A @ B @ C) => (A @ (C @ D) @ (C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_Quotient3__rep__reflp)).
% 50.45/34.27 thf(310,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TB > $o)),B:(TB > TA),C:(TA > TB),D:TA]: ((quotient3 @ TB @ TA @ (A) @ (B) @ (C)) => (A @ (C @ D) @ (C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 50.45/34.27 thf(62,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA]: ((quotient3 @ TA @ TB @ A @ B @ C) => ((A @ D @ D) => (A @ (C @ (B @ D)) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_Quotient3__rep__abs)).
% 50.45/34.27 thf(441,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA]: ((quotient3 @ TA @ TB @ (A) @ (B) @ (C)) => ((A @ D @ D) => (A @ (C @ (B @ D)) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 50.45/34.27 thf(149,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(TA > TB)]: ((inj_on @ TB @ TA @ A @ (top_top @ (set @ TB))) => ((! [C:TA]: ((A @ (B @ C)) = C)) => ((hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_inj__imp__inv__eq)).
% 50.45/34.27 thf(717,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(TA > TB)]: ((inj_on @ TB @ TA @ (A) @ (top_top @ (set @ TB))) => ((! [C:TA]: ((A @ (B @ C)) = C)) => ((hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A) = (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 50.45/34.27 thf(188,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:(set @ TA)]: ((member @ TB @ A @ (image @ TA @ TB @ B @ C)) => (member @ TA @ (hilbert_inv_into @ TA @ TB @ C @ B @ A) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_inv__into__into)).
% 50.45/34.27 thf(840,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:(set @ TA)]: ((member @ TB @ A @ (image @ TA @ TB @ (B) @ C)) => (member @ TA @ (hilbert_inv_into @ TA @ TB @ C @ (B) @ A) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 50.45/34.27 thf(28,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: (member @ TA @ A @ (insert @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_insertI1)).
% 50.45/34.27 thf(338,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: (member @ TA @ A @ (insert @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 50.45/34.27 thf(100,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(set @ TB),C:TA]: ((member @ TB @ A @ B) => ((image @ TB @ TA @ (^ [D:TB]: (C)) @ B) = (insert @ TA @ C @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_image__constant)).
% 50.45/34.27 thf(576,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(set @ TB),C:TA]: ((member @ TB @ A @ B) => ((image @ TB @ TA @ (^ [D:TB]: (C)) @ B) = (insert @ TA @ C @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 50.45/34.27 thf(221,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: ((? [B:TA]: (A @ B)) => (A @ (hilbert_Eps @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_someI__ex)).
% 50.45/34.27 thf(951,plain,((! [TA: $tType]: (! [A:(TA > $o)]: ((? [B:TA]: (A @ B)) => (A @ (hilbert_Eps @ TA @ (A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 50.45/34.27 thf(35,axiom,((! [TA: $tType]: (! [A:(TA > TA),B:TA,C:TA]: ((hilbert_bijection @ TA @ A) => (((A @ B) = (A @ C)) = (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_bijection_Oeq__iff)).
% 50.45/34.27 thf(359,plain,((! [TA: $tType]: (! [A:(TA > TA),B:TA,C:TA]: ((hilbert_bijection @ TA @ (A)) => (((A @ B) = (A @ C)) = (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 50.45/34.27 thf(92,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(TA > $o),C:TA]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) => ((! [D:TB]: ((member @ TB @ D @ (image @ TA @ TB @ A @ (top_top @ (set @ TA)))) => (B @ (hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A @ D)))) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_inj__transfer)).
% 50.45/34.27 thf(544,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(TA > $o),C:TA]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) => ((! [D:TB]: ((member @ TB @ D @ (image @ TA @ TB @ (A) @ (top_top @ (set @ TA)))) => (B @ (hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ (A) @ D)))) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 50.45/34.27 thf(159,axiom,((! [TA: $tType,TB: $tType]: ((top @ TB) => ((top_top @ (TA > TB)) = (^ [A:TA]: (top_top @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_top__apply)).
% 50.45/34.27 thf(744,plain,((! [TA: $tType,TB: $tType]: ((top @ TB) => ((top_top @ (TA > TB)) = (^ [A:TA]: (top_top @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 50.45/34.27 thf(144,axiom,((! [TA: $tType]: (! [A:(TA > TA),B:TA,C:TA]: ((hilbert_bijection @ TA @ A) => (((hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A @ B) = C) = ((A @ C) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_bijection_Oinv__left__eq__iff)).
% 50.45/34.27 thf(703,plain,((! [TA: $tType]: (! [A:(TA > TA),B:TA,C:TA]: ((hilbert_bijection @ TA @ (A)) => (((hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ (A) @ B) = C) = ((A @ C) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 50.45/34.27 thf(244,axiom,((! [TA: $tType,TB: $tType]: ((hilbert_inv_into @ TA @ TB) = (^ [A:(set @ TA),B:(TA > TB),C:TB]: (hilbert_Eps @ TA @ (^ [D:TA]: ((member @ TA @ D @ A) & ((B @ D) = C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_inv__into__def2)).
% 50.45/34.27 thf(1052,plain,((! [TA: $tType,TB: $tType]: ((hilbert_inv_into @ TA @ TB) = (^ [A:(set @ TA),B:(TA > TB),C:TB]: (hilbert_Eps @ TA @ (^ [D:TA]: ((member @ TA @ D @ A) & ((B @ D) = C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 50.45/34.27 thf(20,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA,D:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((~ (member @ TA @ C @ D)) => (((insert @ TA @ A @ B) = (insert @ TA @ C @ D)) = (((A = C) => (B = D)) & ((A != C) => (? [E:(set @ TA)]: ((B = (insert @ TA @ C @ E)) & ~ (member @ TA @ C @ E) & (D = (insert @ TA @ A @ E)) & ~ (member @ TA @ A @ E))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_insert__eq__iff)).
% 50.45/34.27 thf(314,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA,D:(set @ TA)]: ((~ (member @ TA @ A @ B)) => ((~ (member @ TA @ C @ D)) => (((insert @ TA @ A @ B) = (insert @ TA @ C @ D)) = (((A = C) => (B = D)) & ((~ (A = C)) => (? [E:(set @ TA)]: ((B = (insert @ TA @ C @ E)) & ~ (member @ TA @ C @ E) & (D = (insert @ TA @ A @ E)) & ~ (member @ TA @ A @ E))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 50.45/34.27 thf(63,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(set @ TA)]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) => ((image @ TA @ TB @ A @ (minus_minus @ (set @ TA) @ B @ C)) = (minus_minus @ (set @ TB) @ (image @ TA @ TB @ A @ B) @ (image @ TA @ TB @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_image__set__diff)).
% 50.45/34.27 thf(446,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(set @ TA)]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) => ((image @ TA @ TB @ (A) @ (minus_minus @ (set @ TA) @ B @ C)) = (minus_minus @ (set @ TB) @ (image @ TA @ TB @ (A) @ B) @ (image @ TA @ TB @ (A) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 50.45/34.27 thf(107,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TB > $o)),B:((set @ TB) > TA),C:(TA > (set @ TB)),D:TA]: ((quot_type @ TB @ TA @ A @ B @ C) => ((B @ (C @ D)) = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_quot__type_Orep__inverse)).
% 50.45/34.27 thf(595,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TB > $o)),B:((set @ TB) > TA),C:(TA > (set @ TB)),D:TA]: ((quot_type @ TB @ TA @ (A) @ (B) @ (C)) => ((B @ (C @ D)) = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 50.45/34.27 thf(253,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:$o]: (((A @ (hilbert_Eps @ TA @ A)) = B) => ((? [C:TA]: (A @ C)) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_verit__sko__ex_H)).
% 50.45/34.27 thf(1094,plain,((! [TA: $tType]: (! [A:(TA > $o),B:$o]: (((A @ (hilbert_Eps @ TA @ (A))) = B) => ((? [C:TA]: (A @ C)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 50.45/34.27 thf(44,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: (((~ (member @ TA @ A @ B)) => (A = C)) => (member @ TA @ A @ (insert @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_insertCI)).
% 50.45/34.27 thf(386,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: (((~ (member @ TA @ A @ B)) => (A = C)) => (member @ TA @ A @ (insert @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 50.45/34.27 thf(190,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(set @ TA)]: (((image @ TB @ TA @ A @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) => ((image @ TB @ TA @ A @ (image @ TA @ TB @ (hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A) @ B)) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_image__f__inv__f)).
% 50.45/34.27 thf(845,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(set @ TA)]: (((image @ TB @ TA @ (A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) => ((image @ TB @ TA @ (A) @ (image @ TA @ TB @ (hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A) @ B)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 50.45/34.27 thf(70,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(set @ TA),C:(TA > TB)]: ((member @ TA @ A @ B) => ((insert @ TB @ (C @ A) @ (image @ TA @ TB @ C @ B)) = (image @ TA @ TB @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_insert__image)).
% 50.45/34.27 thf(465,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:(set @ TA),C:(TA > TB)]: ((member @ TA @ A @ B) => ((insert @ TB @ (C @ A) @ (image @ TA @ TB @ (C) @ B)) = (image @ TA @ TB @ (C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 50.45/34.27 thf(116,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_bot__apply)).
% 50.45/34.27 thf(627,plain,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 50.45/34.27 thf(95,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TB]: (((image @ TA @ TB @ A @ (top_top @ (set @ TA))) = (top_top @ (set @ TB))) => (? [C:TA]: (B = (A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_surjD)).
% 50.45/34.27 thf(556,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TB]: (((image @ TA @ TB @ (A) @ (top_top @ (set @ TA))) = (top_top @ (set @ TB))) => (? [C:TA]: (B = (A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 50.45/34.27 thf(102,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TB]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) => ((member @ TB @ B @ (image @ TA @ TB @ A @ (top_top @ (set @ TA)))) = (? [C:TA]: ((B = (A @ C)) & ! [D:TA]: ((B = (A @ D)) => (D = C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_range__ex1__eq)).
% 50.45/34.27 thf(581,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TB]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) => ((member @ TB @ B @ (image @ TA @ TB @ (A) @ (top_top @ (set @ TA)))) = (? [C:TA]: ((B = (A @ C)) & ! [D:TA]: ((B = (A @ D)) => (D = C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 50.45/34.27 thf(79,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((insert @ TA @ A @ (minus_minus @ (set @ TA) @ B @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))) = (insert @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_insert__Diff__single)).
% 50.45/34.27 thf(495,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((insert @ TA @ A @ (minus_minus @ (set @ TA) @ B @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))) = (insert @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 50.45/34.27 thf(164,axiom,((! [TA: $tType]: ((is_empty @ TA) = (^ [A:(set @ TA)]: (A = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_Set_Ois__empty__def)).
% 50.45/34.27 thf(759,plain,((! [TA: $tType]: ((is_empty @ TA) = (^ [A:(set @ TA)]: (A = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 50.45/34.27 thf(204,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TB > $o)),B:((set @ TB) > TA),C:(TA > (set @ TB))]: ((quot_type @ TB @ TA @ A @ B @ C) => (quotient3 @ TB @ TA @ A @ (quot_abs @ TB @ TA @ A @ B) @ (quot_rep @ TA @ TB @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_quot__type_OQuotient)).
% 50.45/34.27 thf(891,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TB > $o)),B:((set @ TB) > TA),C:(TA > (set @ TB))]: ((quot_type @ TB @ TA @ (A) @ (B) @ (C)) => (quotient3 @ TB @ TA @ (A) @ (quot_abs @ TB @ TA @ A @ B) @ (quot_rep @ TA @ TB @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 50.45/34.27 thf(39,axiom,((! [TA: $tType]: (! [A:TA,B:$o]: (((top_top @ (TA > $o) @ A) & (B)) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_top__conj_I1_J)).
% 50.45/34.27 thf(368,plain,((! [TA: $tType]: (! [A:TA,B:$o]: (((top_top @ (TA > $o) @ A) & (B)) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 50.45/34.27 thf(206,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TB,C:TA]: ((bij_betw @ TB @ TA @ A @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA))) => ((B = (hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ A @ C)) = ((A @ B) = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_bij__inv__eq__iff)).
% 50.45/34.27 thf(896,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TB,C:TA]: ((bij_betw @ TB @ TA @ (A) @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA))) => ((B = (hilbert_inv_into @ TB @ TA @ (top_top @ (set @ TB)) @ (A) @ C)) = ((A @ B) = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 50.45/34.27 thf(247,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => ((! [D:TA]: ((A @ D) => (C @ D))) => (C @ (hilbert_Eps @ TA @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_someI2)).
% 50.45/34.27 thf(1062,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => ((! [D:TA]: ((A @ D) => (C @ D))) => (C @ (hilbert_Eps @ TA @ (A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 50.45/34.27 thf(125,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: (((insert @ TA @ A @ (bot_bot @ (set @ TA))) = (insert @ TA @ B @ (bot_bot @ (set @ TA)))) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_singleton__inject)).
% 50.45/34.27 thf(652,plain,((! [TA: $tType]: (! [A:TA,B:TA]: (((insert @ TA @ A @ (bot_bot @ (set @ TA))) = (insert @ TA @ B @ (bot_bot @ (set @ TA)))) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 50.45/34.27 thf(49,axiom,((! [TA: $tType]: ((is_singleton @ TA) = (^ [A:(set @ TA)]: (A = (insert @ TA @ (the_elem @ TA @ A) @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_is__singleton__the__elem)).
% 50.45/34.27 thf(401,plain,((! [TA: $tType]: ((is_singleton @ TA) = (^ [A:(set @ TA)]: (A = (insert @ TA @ (the_elem @ TA @ A) @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 50.45/34.27 thf(172,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_Collect__mem__eq)).
% 50.45/34.27 thf(786,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 50.45/34.27 thf(170,axiom,((! [TA: $tType]: ((bot_bot @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_bot__empty__eq)).
% 50.45/34.27 thf(781,plain,((! [TA: $tType]: ((bot_bot @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 50.45/34.27 thf(212,axiom,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (^ [A:TA]: (($false))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_empty__def)).
% 50.45/34.27 thf(914,plain,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (^ [A:TA]: (($false))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 50.45/34.27 thf(130,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: ((image @ TB @ TA @ A @ (bot_bot @ (set @ TB))) = (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_image__empty)).
% 50.45/34.27 thf(667,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: ((image @ TB @ TA @ (A) @ (bot_bot @ (set @ TB))) = (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 50.45/34.27 thf(43,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: ((bij_betw @ TB @ TA @ A @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA))) = ((inj_on @ TB @ TA @ A @ (top_top @ (set @ TB))) & ((image @ TB @ TA @ A @ (top_top @ (set @ TB))) = (top_top @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_bij__def)).
% 50.45/34.27 thf(383,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: ((bij_betw @ TB @ TA @ (A) @ (top_top @ (set @ TB)) @ (top_top @ (set @ TA))) = ((inj_on @ TB @ TA @ (A) @ (top_top @ (set @ TB))) & ((image @ TB @ TA @ (A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 50.45/34.27 thf(207,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA)]: (((bot_bot @ (set @ TB)) = (image @ TA @ TB @ A @ B)) = (B = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_empty__is__image)).
% 50.45/34.27 thf(899,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA)]: (((bot_bot @ (set @ TB)) = (image @ TA @ TB @ (A) @ B)) = (B = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 50.45/34.27 thf(137,axiom,((! [TA: $tType]: (! [A:(TA > TA),B:TA,C:TA]: ((hilbert_bijection @ TA @ A) => ((B = (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ A @ C)) = ((A @ B) = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_bijection_Oinv__right__eq__iff)).
% 50.45/34.27 thf(684,plain,((! [TA: $tType]: (! [A:(TA > TA),B:TA,C:TA]: ((hilbert_bijection @ TA @ (A)) => ((B = (hilbert_inv_into @ TA @ TA @ (top_top @ (set @ TA)) @ (A) @ C)) = ((A @ B) = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 50.45/34.27 thf(242,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => (A @ (hilbert_Eps @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_tfl__some)).
% 50.45/34.27 thf(1045,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => (A @ (hilbert_Eps @ TA @ (A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 50.45/34.27 thf(15,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((member @ TA @ A @ B) => ((minus_minus @ (set @ TA) @ (insert @ TA @ A @ C) @ B) = (minus_minus @ (set @ TA) @ C @ B))) & ((~ (member @ TA @ A @ B)) => ((minus_minus @ (set @ TA) @ (insert @ TA @ A @ C) @ B) = (insert @ TA @ A @ (minus_minus @ (set @ TA) @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_insert__Diff__if)).
% 50.45/34.27 thf(300,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((member @ TA @ A @ B) => ((minus_minus @ (set @ TA) @ (insert @ TA @ A @ C) @ B) = (minus_minus @ (set @ TA) @ C @ B))) & ((~ (member @ TA @ A @ B)) => ((minus_minus @ (set @ TA) @ (insert @ TA @ A @ C) @ B) = (insert @ TA @ A @ (minus_minus @ (set @ TA) @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 50.45/34.27 thf(186,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ A) = (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_Diff__cancel)).
% 50.45/34.27 thf(833,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ A) = (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 50.45/34.27 thf(4,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TB > $o)),B:(TB > TA),C:(TA > TB),D:TA]: ((quotient3 @ TB @ TA @ A @ B @ C) => ((B @ (C @ D)) = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_Quotient3__abs__rep)).
% 50.45/34.27 thf(262,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > (TB > $o)),B:(TB > TA),C:(TA > TB),D:TA]: ((quotient3 @ TB @ TA @ (A) @ (B) @ (C)) => ((B @ (C @ D)) = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 50.45/34.27 thf(180,axiom,((! [TA: $tType]: (top @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Otop_1)).
% 50.45/34.27 thf(818,plain,((! [TA: $tType]: (top @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 50.45/34.27 thf(193,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: (((image @ TB @ TA @ A @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) = (! [B:TA]: ? [C:TB]: (B = (A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_surj__def)).
% 50.45/34.27 thf(854,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA)]: (((image @ TB @ TA @ (A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))) = (! [B:TA]: ? [C:TB]: (B = (A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 50.45/34.27 thf(156,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((member @ TA @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_singletonD)).
% 50.45/34.27 thf(735,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((member @ TA @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 50.45/34.27 thf(13,axiom,((! [TA: $tType]: (! [A:$o,B:TA]: (((A) & (top_top @ (TA > $o) @ B)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_top__conj_I2_J)).
% 50.45/34.27 thf(294,plain,((! [TA: $tType]: (! [A:$o,B:TA]: (((A) & (top_top @ (TA > $o) @ B)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 50.45/34.27 thf(129,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA)]: ((inj_on @ TA @ TB @ A @ (top_top @ (set @ TA))) => ((image @ TB @ TA @ (hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A) @ (image @ TA @ TB @ A @ B)) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_image__inv__f__f)).
% 50.45/34.27 thf(664,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA)]: ((inj_on @ TA @ TB @ (A) @ (top_top @ (set @ TA))) => ((image @ TB @ TA @ (hilbert_inv_into @ TA @ TB @ (top_top @ (set @ TA)) @ A) @ (image @ TA @ TB @ (A) @ B)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 50.45/34.27 thf(223,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o),C:(TA > $o)]: ((? [D:TA]: ((member @ TA @ D @ A) & (B @ D))) => ((! [D:TA]: (((member @ TA @ D @ A) & (B @ D)) => (C @ D))) => (C @ (hilbert_Eps @ TA @ (^ [D:TA]: ((member @ TA @ D @ A) & (B @ D)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_someI2__bex)).
% 50.45/34.27 thf(960,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > $o),C:(TA > $o)]: ((? [D:TA]: ((member @ TA @ D @ A) & (B @ D))) => ((! [D:TA]: (((member @ TA @ D @ A) & (B @ D)) => (C @ D))) => (C @ (hilbert_Eps @ TA @ (^ [D:TA]: ((member @ TA @ D @ A) & (B @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 50.45/34.27 thf(150,axiom,((! [TA: $tType,TB: $tType]: ((quot_rep @ TA @ TB) = (quot_rep @ TA @ TB)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_quot__type_Orep_Ocong)).
% 50.45/34.27 thf(720,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 50.45/34.27 thf(82,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:TA,C:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ (insert @ TA @ B @ C)) = (minus_minus @ (set @ TA) @ (minus_minus @ (set @ TA) @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_Diff__insert2)).
% 50.45/34.27 thf(506,plain,((! [TA: $tType]: (! [A:(set @ TA),B:TA,C:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ (insert @ TA @ B @ C)) = (minus_minus @ (set @ TA) @ (minus_minus @ (set @ TA) @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 50.45/34.27 thf(6,axiom,((! [TA: $tType]: (! [A:TA]: ((the_elem @ TA @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_the__elem__eq)).
% 50.45/34.27 thf(268,plain,((! [TA: $tType]: (! [A:TA]: ((the_elem @ TA @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 50.45/34.27 thf(115,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(TB > $o)]: ((collect @ TB @ (^ [D:TB]: ((member @ TB @ D @ (image @ TA @ TB @ A @ B)) & (C @ D)))) = (image @ TA @ TB @ A @ (collect @ TA @ (^ [D:TA]: ((member @ TA @ D @ B) & (C @ (A @ D)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_Compr__image__eq)).
% 50.45/34.27 thf(624,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:(TB > $o)]: ((collect @ TB @ (^ [D:TB]: ((member @ TB @ D @ (image @ TA @ TB @ A @ B)) & (C @ D)))) = (image @ TA @ TB @ (A) @ (collect @ TA @ (^ [D:TA]: ((member @ TA @ D @ B) & (C @ (A @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 50.45/34.27 thf(228,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:((set @ TA) > TB),C:(TB > (set @ TA)),D:TA]: ((quot_type @ TA @ TB @ A @ B @ C) => ((A @ D @ D) => ((A @ (hilbert_Eps @ TA @ (^ [E:TA]: (member @ TA @ E @ (collect @ TA @ (A @ D)))))) = (A @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_quot__type_Osome__collect)).
% 50.45/34.27 thf(987,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:((set @ TA) > TB),C:(TB > (set @ TA)),D:TA]: ((quot_type @ TA @ TB @ (A) @ (B) @ (C)) => ((A @ D @ D) => ((A @ (hilbert_Eps @ TA @ (^ [E:TA]: (member @ TA @ E @ (collect @ TA @ (A @ D)))))) = (A @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 50.45/34.27 thf(69,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_T)).
% 50.45/34.27 thf(464,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 50.45/34.27 thf(25,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(set @ TB)]: ((bij_betw @ TB @ TA @ A @ B @ (top_top @ (set @ TA))) => ((image @ TB @ TA @ A @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_bij__betw__imp__surj)).
% 50.45/34.27 thf(332,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(set @ TB)]: ((bij_betw @ TB @ TA @ (A) @ B @ (top_top @ (set @ TA))) => ((image @ TB @ TA @ (A) @ (top_top @ (set @ TB))) = (top_top @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 50.45/34.27 thf(195,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB)]: ((member @ TB @ A @ (image @ TA @ TB @ B @ (top_top @ (set @ TA)))) => (~ (! [C:TA]: (A != (B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_rangeE)).
% 50.45/34.27 thf(860,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB)]: ((member @ TB @ A @ (image @ TA @ TB @ (B) @ (top_top @ (set @ TA)))) => (~ (! [C:TA]: ~ (A = (B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 50.45/34.27 thf(122,axiom,((! [TA: $tType]: (ord @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oord_2)).
% 50.45/34.27 thf(644,plain,((! [TA: $tType]: (ord @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 50.45/34.27 thf(152,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > TC),B:(TA > TB)]: ((image @ TA @ TC @ (^ [C:TA]: (A @ (B @ C))) @ (top_top @ (set @ TA))) = (image @ TB @ TC @ A @ (image @ TA @ TB @ B @ (top_top @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_range__composition)).
% 50.45/34.27 thf(723,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > TC),B:(TA > TB)]: ((image @ TA @ TC @ (^ [C:TA]: (A @ (B @ C))) @ (top_top @ (set @ TA))) = (image @ TB @ TC @ (A) @ (image @ TA @ TB @ (B) @ (top_top @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 50.45/34.27 thf(199,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: (((A @ B) => ((collect @ TA @ (^ [C:TA]: ((B = C) & (A @ C)))) = (insert @ TA @ B @ (bot_bot @ (set @ TA))))) & ((~ (A @ B)) => ((collect @ TA @ (^ [C:TA]: ((B = C) & (A @ C)))) = (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_Collect__conv__if2)).
% 50.45/34.27 thf(871,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: (((A @ B) => ((collect @ TA @ (^ [C:TA]: ((B = C) & (A @ C)))) = (insert @ TA @ B @ (bot_bot @ (set @ TA))))) & ((~ (A @ B)) => ((collect @ TA @ (^ [C:TA]: ((B = C) & (A @ C)))) = (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 50.45/34.27 thf(81,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:(set @ TA)]: ((member @ TB @ A @ (image @ TA @ TB @ B @ C)) => (~ (! [D:TA]: ((A = (B @ D)) => (~ (member @ TA @ D @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_imageE)).
% 50.45/34.27 thf(501,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:(TA > TB),C:(set @ TA)]: ((member @ TB @ A @ (image @ TA @ TB @ (B) @ C)) => (~ (! [D:TA]: ((A = (B @ D)) => (~ (member @ TA @ D @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 50.45/34.27 thf(110,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TA,C:TB]: (((image @ TB @ TA @ A @ (top_top @ (set @ TB))) = (insert @ TA @ B @ (bot_bot @ (set @ TA)))) => ((A @ C) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_range__eq__singletonD)).
% 50.45/34.27 thf(607,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TA,C:TB]: (((image @ TB @ TA @ (A) @ (top_top @ (set @ TB))) = (insert @ TA @ B @ (bot_bot @ (set @ TA)))) => ((A @ C) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 50.45/34.27 thf(76,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => ((insert @ TA @ A @ B) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_insert__absorb)).
% 50.45/34.27 thf(486,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((member @ TA @ A @ B) => ((insert @ TA @ A @ B) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 50.45/34.27 thf(27,axiom,((top @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Otop_4)).
% 50.45/34.27 thf(337,plain,((top @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 50.45/34.27 thf(234,axiom,((! [TA: $tType]: (! [A:TA]: ((hilbert_Eps @ TA @ ((=) @ TA @ A)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_some__sym__eq__trivial)).
% 50.45/34.27 thf(1009,plain,((! [TA: $tType]: (! [A:TA]: ((hilbert_Eps @ TA @ ((=) @ TA @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 50.45/34.27 thf(168,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:TA]: ((inj_on @ TA @ TB @ A @ B) => ((member @ TA @ C @ B) => ((hilbert_inv_into @ TA @ TB @ B @ A @ (A @ C)) = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_inv__into__f__f)).
% 50.45/34.27 thf(775,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:(set @ TA),C:TA]: ((inj_on @ TA @ TB @ (A) @ B) => ((member @ TA @ C @ B) => ((hilbert_inv_into @ TA @ TB @ B @ (A) @ (A @ C)) = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 50.45/34.27 thf(120,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((collect @ TA @ A) = (collect @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_Collect__cong)).
% 50.45/34.27 thf(639,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((collect @ TA @ (A)) = (collect @ TA @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 50.45/34.27 thf(134,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: (((collect @ TA @ A) = (bot_bot @ (set @ TA))) = (! [B:TA]: ~ (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_Collect__empty__eq)).
% 50.45/34.27 thf(676,plain,((! [TA: $tType]: (! [A:(TA > $o)]: (((collect @ TA @ (A)) = (bot_bot @ (set @ TA))) = (! [B:TA]: ~ (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 50.45/34.27 thf(106,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (minus_minus @ (set @ TA) @ B @ C)) = ((member @ TA @ A @ B) & ~ (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_Diff__iff)).
% 50.45/34.27 thf(592,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (minus_minus @ (set @ TA) @ B @ C)) = ((member @ TA @ A @ B) & ~ (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 50.45/34.27 thf(37,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA]: ((quotient3 @ TA @ TB @ A @ B @ C) => ((A @ D @ E) => (A @ (C @ (B @ D)) @ E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_rep__abs__rsp__left)).
% 50.45/34.27 thf(364,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > (TA > $o)),B:(TA > TB),C:(TB > TA),D:TA,E:TA]: ((quotient3 @ TA @ TB @ (A) @ (B) @ (C)) => ((A @ D @ E) => (A @ (C @ (B @ D)) @ E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 50.45/34.27 thf(201,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(set @ TB),C:(set @ TA),D:TA]: ((bij_betw @ TB @ TA @ A @ B @ C) => ((member @ TA @ D @ C) => ((A @ (hilbert_inv_into @ TB @ TA @ B @ A @ D)) = D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_bij__betw__inv__into__right)).
% 50.45/34.27 thf(882,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:(set @ TB),C:(set @ TA),D:TA]: ((bij_betw @ TB @ TA @ (A) @ B @ C) => ((member @ TA @ D @ C) => ((A @ (hilbert_inv_into @ TB @ TA @ B @ (A) @ D)) = D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 50.45/34.27 thf(1105,plain,(($false)),inference(e,[status(thm)],[479,347,909,893,518,468,481,977,762,276,308,741,449,655,1078,550,747,340,538,930,670,404,709,885,320,565,1055,587,917,802,344,934,357,902,559,1087,284,416,492,756,789,646,937,905,687,877,956,866,396,411,428,265,527,312,452,920,661,793,366,714,512,942,1091,825,1042,598,820,392,297,815,729,1021,778,693,630,1032,435,830,461,842,1012,324,974,697,317,980,1006,869,610,420,857,471,753,1075,642,489,590,706,679,1039,970,393,515,738,1050,911,721,371,633,805,541,765,398,1071,674,1026,888,412,750,618,425,430,279,573,584,562,423,694,732,772,711,579,281,259,498,1058,335,350,672,604,681,274,784,362,616,271,863,377,996,509,649,477,811,535,621,1029,330,799,726,848,700,521,827,636,455,306,1000,851,438,658,255,939,342,553,836,927,374,458,823,1003,690,414,993,1098,310,441,717,840,338,576,951,359,544,744,703,1052,314,446,595,1094,386,845,465,627,556,581,495,759,891,368,896,1062,652,401,786,781,914,667,383,899,684,1045,300,833,262,818,854,735,294,664,960,720,506,268,624,987,464,332,860,644,723,871,501,607,486,337,1009,775,639,676,592,364,882])).
% 50.45/34.27 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 50.45/34.27 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------