%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP031^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 : n005.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:29 AM UTC 2026
% Result : Theorem 51.89s 28.82s
% Output : Refutation 53.05s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP031^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.10/0.20 % Computer : n005.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Tue Sep 29 19:38:31 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.86/0.77 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.36/1.21 % [INFO] Parsing done (440ms).
% 2.36/1.23 % [INFO] Running in sequential loop mode.
% 3.86/1.62 % [INFO] eprover registered as external prover.
% 3.86/1.63 % [INFO] Scanning for conjecture ...
% 4.29/1.81 % [INFO] Found a conjecture (or negated_conjecture) and 302 axioms. Running axiom selection ...
% 4.55/1.96 % [INFO] Axiom selection finished. Selected 285 axioms (removed 17 axioms).
% 5.55/2.28 % [INFO] Problem is higher-order (TPTP THF).
% 5.89/2.30 % [INFO] Type checking passed.
% 5.89/2.31 % [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 ...
% 51.89/28.81 % External prover 'e' found a proof!
% 51.89/28.81 % [INFO] Killing All external provers ...
% 51.89/28.82 % Time passed: 28481ms (effective reasoning time: 27583ms)
% 51.89/28.82 % 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)>
% 51.89/28.82 % Axioms used in derivation (285): fact_240_singleton__insert__inj__eq_H, tcon_fun___Groups_Ominus, fact_65_Set_Oset__insert, fact_107_sup__bot_Oright__neutral, fact_232_subsetI, fact_151_sup1I1, tcon_fun___Orderings_Obot, fact_99_insert__def, fact_56_ex__in__conv, tcon_HOL_Obool___Lattices_Osemilattice__sup_19, fact_42_insert__iff, fact_246_less__le, fact_70_Un__left__absorb, fact_200_diff__strict__right__mono, fact_163_exists__least__iff, fact_30_Un__Diff__cancel2, fact_61_insert__commute, fact_249_order__less__le__subst1, fact_131_boolean__algebra__cancel_Osup1, fact_5_s, fact_199_bot_Oextremum__strict, tcon_Set_Oset___Orderings_Oord_15, tcon_Set_Oset___Lattices_Olattice_13, fact_159_order_Ostrict__implies__not__eq, fact_4_s2, fact_87_set__diff__eq, fact_9_eqs__def, fact_31_Diff__insert0, tcon_Int_Oint___Groups_Ominus_8, fact_59_emptyE, fact_130_sup__fun__def, fact_212_Tree_Oset__intros_I3_J, fact_213_Tree_Oset__intros_I2_J, fact_241_singleton__insert__inj__eq, fact_113_sup__bot__right, tcon_HOL_Obool___Orderings_Olinorder_22, fact_49_UnCI, fact_203_sup__Un__eq, fact_67_insertI1, fact_3_s1, fact_120_sup_Oleft__idem, fact_78_UnE, fact_165_order_Ostrict__trans, fact_12__092_060open_062sortedTree_Ah_ATip_A_092_060longrightarrow_062_AsetOf_A_Ibinsert_Ah_Ae_ATip_J_A_061_AsetOf_ATip_A_N_Aeqs_Ah_Ae_A_092_060union_062_A_123e_125_092_060close_062, fact_41_insert__absorb2, fact_88_singleton__inject, fact_233_sup_Obounded__iff, fact_255_antisym__conv2, fact_15_setOf_Osimps_I1_J, fact_51_Diff__iff, tcon_Int_Oint___Groups_Oordered__ab__group__add, fact_14_setOf_Osimps_I2_J, fact_126_inf__sup__aci_I8_J, fact_54_Un__empty, fact_106_Diff__insert, tcon_HOL_Obool___Groups_Ominus_27, tcon_fun___Orderings_Oord, fact_237_insert__subset, fact_242_Diff__eq__empty__iff, fact_35_Diff__empty, fact_175_ord__less__eq__trans, fact_235_empty__subsetI, fact_153_not__psubset__empty, fact_184_order_Oasym, fact_231_subset__antisym, fact_223_theI_H, fact_189_order__less__subst2, tcon_Int_Oint___Orderings_Oord_7, fact_247_order__le__less__subst1, fact_62_insert__eq__iff, fact_2_res, fact_145_the__elem__eq, fact_127_inf__sup__aci_I7_J, fact_24_Tree_Oexhaust, fact_206_psubset__trans, fact_21_sortLemmaL, tcon_HOL_Obool___Orderings_Oorder_24, fact_58_equals0D, fact_101_Un__singleton__iff, tcon_HOL_Obool___Orderings_Obot_26, fact_224_theI2, tcon_fun___Lattices_Obounded__semilattice__sup__bot, fact_104_Diff__insert2, fact_229_pairwise__alt, fact_73_Un__assoc, fact_84_insert__compr, fact_108_sup__bot_Oneutr__eq__iff, fact_124_sup__set__def, fact_214_Tree_Oset__intros_I1_J, fact_202_diff__eq__diff__less, fact_166_dual__order_Oirrefl, fact_46_Collect__mem__eq, fact_234_le__sup__iff, fact_86_Un__def, fact_136_sup__commute, fact_239_psubsetI, tcon_Set_Oset___Lattices_Obounded__semilattice__sup__bot_9, fact_19_sortedTree_Osimps_I2_J, fact_193_bot__fun__def, fact_20_sortedTree_Osimps_I1_J, fact_114_sup__bot__left, fact_53_singletonI, fact_10_h1, fact_144_sup_Ostrict__coboundedI2, fact_205_Collect__empty__eq__bot, fact_64_insert__ident, fact_227_the1__equality, fact_18_binsert_Osimps_I1_J, fact_32_insert__Diff1, fact_76_UnI2, fact_245_le__less, tcon_fun___Lattices_Osemilattice__sup, fact_123_bot__set__def, tcon_fun___Lattices_Obounded__lattice_2, fact_115_memb__spec, fact_194_diff__right__commute, fact_222_theI, fact_158_dual__order_Ostrict__implies__not__eq, fact_248_order__le__less__subst2, fact_38_Collect__empty__eq, fact_217_Set_Ois__empty__def, fact_95_insert__Diff__if, fact_93_Un__empty__right, tcon_HOL_Obool___Orderings_Oord_25, fact_55_Diff__cancel, fact_219_the__sym__eq__trivial, fact_77_UnI1, fact_254_antisym__conv1, fact_44_Un__iff, fact_92_singletonD, fact_11_h2, fact_243_leD, fact_7_c1, tcon_Int_Oint___Orderings_Olinorder, fact_253_le__neq__trans, fact_210_Tree_Osimps_I15_J, fact_28_singleton__conv2, fact_36_empty__Diff, fact_97_Collect__conv__if2, fact_174_dual__order_Oasym, fact_91_singleton__iff, fact_116_minus__apply, tcon_Set_Oset___Lattices_Osemilattice__sup_10, fact_72_Un__absorb, fact_82_empty__def, fact_170_antisym__conv3, fact_209_remove__def, fact_45_mem__Collect__eq, fact_162_linorder__less__wlog, fact_150_sup1E, fact_105_insert__Diff, fact_129_inf__sup__aci_I5_J, fact_187_gt__ex, tcon_Set_Oset___Orderings_Oorder__bot_11, fact_102_insert__is__Un, fact_147_is__singletonI, fact_110_sup__bot_Oeq__neutr__iff, fact_143_sup_Ostrict__coboundedI1, fact_27_singleton__conv, fact_50_Diff__idemp, fact_201_diff__strict__left__mono, tcon_Int_Oint___Orderings_Oorder_6, fact_122_sup_Oright__idem, fact_160_not__less__iff__gr__or__eq, tcon_Int_Oint___Groups_Ocancel__ab__semigroup__add, fact_186_neqE, fact_216_Tree_Osimps_I14_J, tcon_Int_Oint___Lattices_Olattice_5, fact_226_the1I2, fact_188_lt__ex, fact_109_sup__bot_Oleft__neutral, fact_218_the__elem__def, fact_23_Tree_Oinduct, fact_171_less__induct, fact_57_equals0I, tcon_Int_Oint___Groups_Ogroup__add, fact_211_member__remove, fact_135_sup_Ocommute, fact_111_sup__eq__bot__iff, fact_191_ord__less__eq__subst, fact_16_Tree_Odistinct_I1_J, fact_47_Collect__cong, fact_251_not__le, fact_137_sup_Oleft__commute, fact_68_insertE, tcon_fun___Orderings_Oorder__bot, fact_138_sup__left__commute, fact_190_order__less__subst1, tcon_Set_Oset___Lattices_Obounded__lattice_1, fact_185_neq__iff, fact_63_insert__absorb, fact_39_all__not__in__conv, fact_146_bot__apply, fact_94_Un__empty__left, fact_238_Un__subset__iff, fact_133_sup_Oassoc, fact_1_eLess, fact_98_Collect__conv__if, fact_33_Un__insert__left, fact_169_less__imp__not__eq2, fact_220_the__eq__trivial, fact_17_binsert_Osimps_I2_J, fact_6_sorted__distinct, fact_173_less__imp__not__eq, fact_221_the__equality, fact_183_dense, fact_244_leI, fact_132_boolean__algebra__cancel_Osup2, fact_196_is__singleton__def, fact_90_doubleton__eq__iff, fact_29_Un__Diff__cancel, fact_13_Tree_Oinject, fact_25_sorted__distinct__pred__def, fact_197_is__singletonE, fact_178_less__linear, tcon_Set_Oset___Orderings_Obot_16, fact_157_is__singletonI_H, fact_66_insertI2, fact_149_sup1CI, fact_52_DiffI, fact_22_sortLemmaR, tcon_Int_Oint___Lattices_Osemilattice__sup_3, fact_118_sup_Oidem, fact_117_sup__apply, fact_121_sup__left__idem, fact_0_eqsLessX, fact_100_singleton__Un__iff, fact_250_order__less__le__subst2, fact_96_Un__Diff, fact_152_sup1I2, tcon_HOL_Obool___Orderings_Oorder__bot_20, fact_26_insert__Diff__single, fact_112_bot__eq__sup__iff, fact_142_sup_Ostrict__order__iff, fact_228_psubset__insert__iff, fact_154_psubset__imp__ex__mem, fact_215_Tree_Oset__cases, tcon_Int_Oint___Orderings_Ono__bot, fact_89_insert__not__empty, tcon_fun___Orderings_Oorder, fact_155_minus__set__def, fact_125_fun__diff__def, fact_204_bot__empty__eq, fact_167_linorder__cases, fact_103_Diff__insert__absorb, fact_140_less__supI2, tcon_Int_Oint___Orderings_Ono__top, fact_128_inf__sup__aci_I6_J, fact_208_psubsetD, fact_161_dual__order_Ostrict__trans, fact_141_sup_Ostrict__boundedE, tcon_HOL_Obool___Lattices_Obounded__lattice, fact_80_DiffD1, fact_74_ball__Un, fact_207_less__set__def, fact_85_Collect__disj__eq, fact_8_c2, fact_134_sup__assoc, fact_34_Un__insert__right, fact_75_bex__Un, fact_156_is__singleton__the__elem, fact_252_not__less, fact_195_diff__eq__diff__eq, fact_139_less__supI1, fact_192_ord__eq__less__subst, fact_119_sup__idem, fact_198_bot_Onot__eq__extremum, fact_236_subset__empty, fact_182_less__imp__neq, fact_79_DiffD2, fact_83_insert__Collect, fact_176_ord__eq__less__trans, fact_71_Un__commute, tcon_HOL_Obool___Lattices_Obounded__semilattice__sup__bot_18, fact_43_insertCI, fact_69_Un__left__commute, fact_40_empty__iff, tcon_Set_Oset___Groups_Ominus_17, tcon_Set_Oset___Orderings_Oorder_14, fact_37_empty__Collect__eq, fact_81_DiffE, tcon_fun___Lattices_Olattice, fact_60_mk__disjoint__insert, tcon_HOL_Obool___Lattices_Olattice_23, fact_148_diff__strict__mono
% 51.89/28.82 % No. of inferences in proof: 574
% 51.89/28.82 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 28481 ms resp. 27583 ms w/o parsing
% 53.05/29.09 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 53.05/29.09 thf(int_type, type, int: $tType).
% 53.05/29.09 thf(a_type, type, a: $tType).
% 53.05/29.09 thf(bounded_lattice_decl, type, bounded_lattice: !> [TA: $tType]: $o).
% 53.05/29.09 thf(minus_decl, type, minus: !> [TA: $tType]: $o).
% 53.05/29.09 thf(bot_decl, type, bot: !> [TA: $tType]: $o).
% 53.05/29.09 thf(ord_decl, type, ord: !> [TA: $tType]: $o).
% 53.05/29.09 thf(order_decl, type, order: !> [TA: $tType]: $o).
% 53.05/29.09 thf(group_add_decl, type, group_add: !> [TA: $tType]: $o).
% 53.05/29.09 thf(lattice_decl, type, lattice: !> [TA: $tType]: $o).
% 53.05/29.09 thf(no_bot_decl, type, no_bot: !> [TA: $tType]: $o).
% 53.05/29.09 thf(no_top_decl, type, no_top: !> [TA: $tType]: $o).
% 53.05/29.09 thf(linorder_decl, type, linorder: !> [TA: $tType]: $o).
% 53.05/29.09 thf(order_bot_decl, type, order_bot: !> [TA: $tType]: $o).
% 53.05/29.09 thf(wellorder_decl, type, wellorder: !> [TA: $tType]: $o).
% 53.05/29.09 thf(dense_order_decl, type, dense_order: !> [TA: $tType]: $o).
% 53.05/29.09 thf(semilattice_sup_decl, type, semilattice_sup: !> [TA: $tType]: $o).
% 53.05/29.09 thf(ordered_ab_group_add_decl, type, ordered_ab_group_add: !> [TA: $tType]: $o).
% 53.05/29.09 thf(cancel146912293up_add_decl, type, cancel146912293up_add: !> [TA: $tType]: $o).
% 53.05/29.09 thf(bounde1808546759up_bot_decl, type, bounde1808546759up_bot: !> [TA: $tType]: $o).
% 53.05/29.09 thf(binary210054475elle_T_decl, type, binary210054475elle_T: !> [TA: $tType]: ((binary1291135688e_Tree @ TA) > (TA > ((binary1291135688e_Tree @ TA) > (binary1291135688e_Tree @ TA))))).
% 53.05/29.09 thf(binary1746293266le_Tip_decl, type, binary1746293266le_Tip: !> [TA: $tType]: (binary1291135688e_Tree @ TA)).
% 53.05/29.09 thf(binary2130109271t_Tree_decl, type, binary2130109271t_Tree: !> [TA: $tType]: ((binary1291135688e_Tree @ TA) > (set @ TA))).
% 53.05/29.09 thf(binary1830089824insert_decl, type, binary1830089824insert: !> [TA: $tType]: ((TA > int) > (TA > ((binary1291135688e_Tree @ TA) > (binary1291135688e_Tree @ TA))))).
% 53.05/29.09 thf(binary64540844le_eqs_decl, type, binary64540844le_eqs: !> [TA: $tType]: ((TA > int) > (TA > (set @ TA)))).
% 53.05/29.09 thf(binary827270440e_memb_decl, type, binary827270440e_memb: !> [TA: $tType]: ((TA > int) > (TA > ((binary1291135688e_Tree @ TA) > $o)))).
% 53.05/29.09 thf(binary1653327646_setOf_decl, type, binary1653327646_setOf: !> [TA: $tType]: ((binary1291135688e_Tree @ TA) > (set @ TA))).
% 53.05/29.09 thf(binary1610619414edTree_decl, type, binary1610619414edTree: !> [TA: $tType]: ((TA > int) > ((binary1291135688e_Tree @ TA) > $o))).
% 53.05/29.09 thf(binary231205461t_pred_decl, type, binary231205461t_pred: !> [TA: $tType]: ((TA > int) > (TA > (TA > ((binary1291135688e_Tree @ TA) > $o))))).
% 53.05/29.09 thf(minus_minus_decl, type, minus_minus: !> [TA: $tType]: (TA > (TA > TA))).
% 53.05/29.09 thf(the_decl, type, the: !> [TA: $tType]: ((TA > $o) > TA)).
% 53.05/29.09 thf(sup_sup_decl, type, sup_sup: !> [TA: $tType]: (TA > (TA > TA))).
% 53.05/29.09 thf(bot_bot_decl, type, bot_bot: !> [TA: $tType]: TA).
% 53.05/29.09 thf(ord_less_decl, type, ord_less: !> [TA: $tType]: (TA > (TA > $o))).
% 53.05/29.09 thf(ord_less_eq_decl, type, ord_less_eq: !> [TA: $tType]: (TA > (TA > $o))).
% 53.05/29.09 thf(collect_decl, type, collect: !> [TA: $tType]: ((TA > $o) > (set @ TA))).
% 53.05/29.09 thf(insert_decl, type, insert: !> [TA: $tType]: (TA > ((set @ TA) > (set @ TA)))).
% 53.05/29.09 thf(is_empty_decl, type, is_empty: !> [TA: $tType]: ((set @ TA) > $o)).
% 53.05/29.09 thf(is_singleton_decl, type, is_singleton: !> [TA: $tType]: ((set @ TA) > $o)).
% 53.05/29.09 thf(pairwise_decl, type, pairwise: !> [TA: $tType]: ((TA > (TA > $o)) > ((set @ TA) > $o))).
% 53.05/29.09 thf(remove_decl, type, remove: !> [TA: $tType]: (TA > ((set @ TA) > (set @ TA)))).
% 53.05/29.09 thf(the_elem_decl, type, the_elem: !> [TA: $tType]: ((set @ TA) > TA)).
% 53.05/29.09 thf(member_decl, type, member: !> [TA: $tType]: (TA > ((set @ TA) > $o))).
% 53.05/29.09 thf(e_decl, type, e: a).
% 53.05/29.09 thf(h_decl, type, h: (a > int)).
% 53.05/29.09 thf(t1_decl, type, t1: (binary1291135688e_Tree @ a)).
% 53.05/29.09 thf(t2_decl, type, t2: (binary1291135688e_Tree @ a)).
% 53.05/29.09 thf(x_decl, type, x: a).
% 53.05/29.09 thf(160,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ (sup_sup @ TA @ A @ B) @ C) = ((ord_less_eq @ TA @ A @ C) & (ord_less_eq @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_sup_Obounded__iff)).
% 53.05/29.09 thf(809,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ (sup_sup @ TA @ A @ B) @ C) = ((ord_less_eq @ TA @ A @ C) & (ord_less_eq @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 53.05/29.09 thf(232,axiom,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((binary1610619414edTree @ TA @ A @ (binary210054475elle_T @ TA @ B @ C @ D)) = ((binary1610619414edTree @ TA @ A @ B) & ! [E:TA]: ((member @ TA @ E @ (binary1653327646_setOf @ TA @ B)) => (ord_less @ int @ (A @ E) @ (A @ C))) & ! [E:TA]: ((member @ TA @ E @ (binary1653327646_setOf @ TA @ D)) => (ord_less @ int @ (A @ C) @ (A @ E))) & (binary1610619414edTree @ TA @ A @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_sortedTree_Osimps_I2_J)).
% 53.05/29.09 thf(1024,plain,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((binary1610619414edTree @ TA @ (A) @ (binary210054475elle_T @ TA @ B @ C @ D)) = ((binary1610619414edTree @ TA @ (A) @ B) & ! [E:TA]: ((member @ TA @ E @ (binary1653327646_setOf @ TA @ B)) => (ord_less @ int @ (A @ E) @ (A @ C))) & ! [E:TA]: ((member @ TA @ E @ (binary1653327646_setOf @ TA @ D)) => (ord_less @ int @ (A @ C) @ (A @ E))) & (binary1610619414edTree @ TA @ (A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 53.05/29.09 thf(141,axiom,((cancel146912293up_add @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Ocancel__ab__semigroup__add)).
% 53.05/29.09 thf(760,plain,((cancel146912293up_add @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 53.05/29.09 thf(173,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_205_Collect__empty__eq__bot)).
% 53.05/29.09 thf(846,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)],[173])).
% 53.05/29.09 thf(22,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => ((! [C:TA]: ((A @ C) => (C = B))) => ((the @ TA @ A) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_the__equality)).
% 53.05/29.09 thf(352,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => ((! [C:TA]: ((A @ C) => (C = B))) => ((the @ TA @ (A)) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 53.05/29.09 thf(81,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (ord_less @ TA @ B @ A)) = (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_antisym__conv3)).
% 53.05/29.09 thf(582,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (ord_less @ TA @ B @ A)) = (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 53.05/29.09 thf(226,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_91_singleton__iff)).
% 53.05/29.09 thf(1005,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)],[226])).
% 53.05/29.09 thf(248,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)).
% 53.05/29.09 thf(1068,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 53.05/29.09 thf(136,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_61_insert__commute)).
% 53.05/29.09 thf(741,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)],[136])).
% 53.05/29.09 thf(182,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((ord_less @ TA @ A @ B) = (ord_less @ TA @ C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_diff__eq__diff__less)).
% 53.05/29.09 thf(873,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((ord_less @ TA @ A @ B) = (ord_less @ TA @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 53.05/29.09 thf(274,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_62_insert__eq__iff)).
% 53.05/29.09 thf(1142,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)],[274])).
% 53.05/29.09 thf(184,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((collect @ TA @ (^ [C:TA]: ((A @ C) | (B @ C)))) = (sup_sup @ (set @ TA) @ (collect @ TA @ A) @ (collect @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_Collect__disj__eq)).
% 53.05/29.09 thf(878,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((collect @ TA @ (^ [C:TA]: ((A @ C) | (B @ C)))) = (sup_sup @ (set @ TA) @ (collect @ TA @ (A)) @ (collect @ TA @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 53.05/29.09 thf(38,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_less__imp__not__eq2)).
% 53.05/29.09 thf(408,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 53.05/29.09 thf(218,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)) => ((~ (member @ TA @ A @ B)) => (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_UnE)).
% 53.05/29.09 thf(977,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)) => ((~ (member @ TA @ A @ B)) => (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 53.05/29.09 thf(91,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = (A = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_subset__empty)).
% 53.05/29.09 thf(614,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = (A = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 53.05/29.09 thf(115,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => (sup_sup @ (TA > $o) @ A @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_sup1I1)).
% 53.05/29.09 thf(677,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => (sup_sup @ (TA > $o) @ (A) @ (C) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 53.05/29.09 thf(239,axiom,((! [TA: $tType]: ((binary64540844le_eqs @ TA) = (^ [A:(TA > int),B:TA]: (collect @ TA @ (^ [C:TA]: ((A @ C) = (A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_eqs__def)).
% 53.05/29.09 thf(1041,plain,((! [TA: $tType]: ((binary64540844le_eqs @ TA) = (^ [A:(TA > int),B:TA]: (collect @ TA @ (^ [C:TA]: ((A @ C) = (A @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 53.05/29.09 thf(178,axiom,((! [TA: $tType]: ((binary2130109271t_Tree @ TA @ (binary1746293266le_Tip @ TA)) = (bot_bot @ (set @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_Tree_Osimps_I14_J)).
% 53.05/29.09 thf(861,plain,((! [TA: $tType]: ((binary2130109271t_Tree @ TA @ (binary1746293266le_Tip @ TA)) = (bot_bot @ (set @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 53.05/29.09 thf(272,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B))) => (ord_less_eq @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_subsetI)).
% 53.05/29.09 thf(1137,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B))) => (ord_less_eq @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[272])).
% 53.05/29.09 thf(71,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C)) = (sup_sup @ TA @ B @ (sup_sup @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_sup_Oleft__commute)).
% 53.05/29.09 thf(533,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C)) = (sup_sup @ TA @ B @ (sup_sup @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 53.05/29.09 thf(65,axiom,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TB) => ((sup_sup @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (sup_sup @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_sup__apply)).
% 53.05/29.09 thf(500,plain,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TB) => ((sup_sup @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (sup_sup @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 53.05/29.09 thf(126,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((~ (ord_less @ TA @ A @ B)) = (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_255_antisym__conv2)).
% 53.05/29.09 thf(715,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((~ (ord_less @ TA @ A @ B)) = (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 53.05/29.09 thf(120,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (minus_minus @ (set @ TA) @ B @ A)) = (sup_sup @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_Un__Diff__cancel)).
% 53.05/29.09 thf(698,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (minus_minus @ (set @ TA) @ B @ A)) = (sup_sup @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 53.05/29.09 thf(193,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_Diff__empty)).
% 53.05/29.09 thf(913,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 53.05/29.09 thf(246,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((! [D:TA]: ((member @ TA @ D @ (sup_sup @ (set @ TA) @ A @ B)) => (C @ D))) = (! [D:TA]: ((member @ TA @ D @ A) => (C @ D)) & ! [D:TA]: ((member @ TA @ D @ B) => (C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_ball__Un)).
% 53.05/29.09 thf(1063,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((! [D:TA]: ((member @ TA @ D @ (sup_sup @ (set @ TA) @ A @ B)) => (C @ D))) = (! [D:TA]: ((member @ TA @ D @ A) => (C @ D)) & ! [D:TA]: ((member @ TA @ D @ B) => (C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 53.05/29.09 thf(112,axiom,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (^ [A:TA]: (($false))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_empty__def)).
% 53.05/29.09 thf(670,plain,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (^ [A:TA]: (($false))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 53.05/29.09 thf(187,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_Un__absorb)).
% 53.05/29.09 thf(898,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 53.05/29.09 thf(1,conjecture,((! [A:a]: ((member @ a @ A @ (binary64540844le_eqs @ a @ h @ e)) => ((h @ A) != (h @ x))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 53.05/29.09 thf(2,negated_conjecture,((~ (! [A:a]: ((member @ a @ A @ (binary64540844le_eqs @ a @ h @ e)) => ((h @ A) != (h @ x)))))),inference(neg_conjecture,[status(cth)],[1])).
% 53.05/29.09 thf(288,plain,((~ (! [A:a]: ((member @ a @ A @ (binary64540844le_eqs @ a @ (h) @ e)) => (~ ((h @ A) = (h @ x))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 53.05/29.09 thf(15,axiom,((! [TA: $tType]: ((lattice @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C)) = (sup_sup @ TA @ B @ (sup_sup @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_inf__sup__aci_I7_J)).
% 53.05/29.09 thf(320,plain,((! [TA: $tType]: ((lattice @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C)) = (sup_sup @ TA @ B @ (sup_sup @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 53.05/29.09 thf(105,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => (sup_sup @ (TA > $o) @ C @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_sup1I2)).
% 53.05/29.09 thf(651,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => (sup_sup @ (TA > $o) @ (C) @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 53.05/29.09 thf(167,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_83_insert__Collect)).
% 53.05/29.09 thf(829,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)],[167])).
% 53.05/29.09 thf(36,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_dual__order_Oasym)).
% 53.05/29.09 thf(404,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 53.05/29.09 thf(29,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TB) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_fun__diff__def)).
% 53.05/29.09 thf(372,plain,((! [TA: $tType,TB: $tType]: ((minus @ TB) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 53.05/29.09 thf(200,axiom,((ord @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Oord_7)).
% 53.05/29.09 thf(934,plain,((ord @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 53.05/29.09 thf(270,axiom,(((binary1610619414edTree @ a @ h @ t1) => ((binary1653327646_setOf @ a @ (binary1830089824insert @ a @ h @ e @ t1)) = (sup_sup @ (set @ a) @ (minus_minus @ (set @ a) @ (binary1653327646_setOf @ a @ t1) @ (binary64540844le_eqs @ a @ h @ e)) @ (insert @ a @ e @ (bot_bot @ (set @ a))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_h1)).
% 53.05/29.09 thf(1132,plain,(((binary1610619414edTree @ a @ (h) @ t1) => ((binary1653327646_setOf @ a @ (binary1830089824insert @ a @ (h) @ e @ t1)) = (sup_sup @ (set @ a) @ (minus_minus @ (set @ a) @ (binary1653327646_setOf @ a @ t1) @ (binary64540844le_eqs @ a @ (h) @ e)) @ (insert @ a @ e @ (bot_bot @ (set @ a))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 53.05/29.09 thf(205,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_diff__strict__right__mono)).
% 53.05/29.09 thf(949,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 53.05/29.09 thf(244,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_65_Set_Oset__insert)).
% 53.05/29.09 thf(1055,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)],[244])).
% 53.05/29.09 thf(129,axiom,((bounded_lattice @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Obounded__lattice)).
% 53.05/29.09 thf(724,plain,((bounded_lattice @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 53.05/29.09 thf(78,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_order_Ostrict__trans)).
% 53.05/29.09 thf(559,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 53.05/29.09 thf(215,axiom,((! [TA: $tType]: (! [A:TA,B:(binary1291135688e_Tree @ TA),C:(binary1291135688e_Tree @ TA),D:TA]: ((member @ TA @ A @ (binary2130109271t_Tree @ TA @ B)) => (member @ TA @ A @ (binary2130109271t_Tree @ TA @ (binary210054475elle_T @ TA @ C @ D @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_Tree_Oset__intros_I3_J)).
% 53.05/29.09 thf(969,plain,((! [TA: $tType]: (! [A:TA,B:(binary1291135688e_Tree @ TA),C:(binary1291135688e_Tree @ TA),D:TA]: ((member @ TA @ A @ (binary2130109271t_Tree @ TA @ B)) => (member @ TA @ A @ (binary2130109271t_Tree @ TA @ (binary210054475elle_T @ TA @ C @ D @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 53.05/29.09 thf(185,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_Un__empty__right)).
% 53.05/29.09 thf(881,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (bot_bot @ (set @ TA))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 53.05/29.09 thf(13,axiom,((! [TA: $tType]: (! [A:TA]: ((the @ TA @ ((=) @ TA @ A)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_the__sym__eq__trivial)).
% 53.05/29.09 thf(316,plain,((! [TA: $tType]: (! [A:TA]: ((the @ TA @ ((=) @ TA @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 53.05/29.09 thf(152,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_leI)).
% 53.05/29.09 thf(789,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 53.05/29.09 thf(262,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_66_insertI2)).
% 53.05/29.09 thf(1109,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)],[262])).
% 53.05/29.09 thf(103,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_209_remove__def)).
% 53.05/29.09 thf(646,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)],[103])).
% 53.05/29.09 thf(169,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((sup_sup @ TA @ A @ B) = (bot_bot @ TA)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_sup__eq__bot__iff)).
% 53.05/29.09 thf(834,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((sup_sup @ TA @ A @ B) = (bot_bot @ TA)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 53.05/29.09 thf(159,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ((insert @ TA @ A @ B) != (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_insert__not__empty)).
% 53.05/29.09 thf(806,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: ~ ((insert @ TA @ A @ B) = (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 53.05/29.09 thf(213,axiom,((minus @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Ominus_8)).
% 53.05/29.09 thf(966,plain,((minus @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 53.05/29.09 thf(164,axiom,((no_bot @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Ono__bot)).
% 53.05/29.09 thf(821,plain,((no_bot @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 53.05/29.09 thf(278,axiom,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_singletonI)).
% 53.05/29.09 thf(1151,plain,((! [TA: $tType]: (! [A:TA]: (member @ TA @ A @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 53.05/29.09 thf(202,axiom,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (sup_sup @ (set @ TA) @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_Un__commute)).
% 53.05/29.09 thf(937,plain,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (sup_sup @ (set @ TA) @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 53.05/29.09 thf(231,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((~ (member @ TA @ A @ B)) => (member @ TA @ A @ C)) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_UnCI)).
% 53.05/29.09 thf(1020,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((~ (member @ TA @ A @ B)) => (member @ TA @ A @ C)) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 53.05/29.09 thf(20,axiom,((! [TA: $tType,TB: $tType]: ((bounded_lattice @ TA) => (bounded_lattice @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Obounded__lattice_2)).
% 53.05/29.09 thf(348,plain,((! [TA: $tType,TB: $tType]: ((bounded_lattice @ TA) => (bounded_lattice @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 53.05/29.09 thf(180,axiom,((! [TA: $tType]: ((binary1653327646_setOf @ TA @ (binary1746293266le_Tip @ TA)) = (bot_bot @ (set @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_setOf_Osimps_I1_J)).
% 53.05/29.09 thf(866,plain,((! [TA: $tType]: ((binary1653327646_setOf @ TA @ (binary1746293266le_Tip @ TA)) = (bot_bot @ (set @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 53.05/29.09 thf(266,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_57_equals0I)).
% 53.05/29.09 thf(1119,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)],[266])).
% 53.05/29.09 thf(223,axiom,((ord_less @ int @ (h @ e) @ (h @ x))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_eLess)).
% 53.05/29.09 thf(998,plain,((ord_less @ int @ (h @ e) @ (h @ x))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 53.05/29.09 thf(44,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((? [C:TA]: ((A @ C) & ! [D:TA]: ((A @ D) => (D = C)))) => ((! [C:TA]: ((A @ C) => (B @ C))) => (B @ (the @ TA @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_the1I2)).
% 53.05/29.09 thf(428,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((? [C:TA]: ((A @ C) & ! [D:TA]: ((A @ D) => (D = C)))) => ((! [C:TA]: ((A @ C) => (B @ C))) => (B @ (the @ TA @ (A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 53.05/29.09 thf(69,axiom,((! [TA: $tType,TB: $tType]: ((order_bot @ TA) => (order_bot @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder__bot)).
% 53.05/29.09 thf(527,plain,((! [TA: $tType,TB: $tType]: ((order_bot @ TA) => (order_bot @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 53.05/29.09 thf(220,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_95_insert__Diff__if)).
% 53.05/29.09 thf(981,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)],[220])).
% 53.05/29.09 thf(144,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ A @ B)) = (sup_sup @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_Un__left__absorb)).
% 53.05/29.09 thf(766,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ A @ B)) = (sup_sup @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 53.05/29.09 thf(3,axiom,((order @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Oorder_6)).
% 53.05/29.09 thf(293,plain,((order @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 53.05/29.09 thf(208,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: (((sup_sup @ (set @ TA) @ A @ B) = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) = (((A = (bot_bot @ (set @ TA))) & (B = (insert @ TA @ C @ (bot_bot @ (set @ TA))))) | ((A = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) & (B = (bot_bot @ (set @ TA)))) | ((A = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) & (B = (insert @ TA @ C @ (bot_bot @ (set @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_Un__singleton__iff)).
% 53.05/29.09 thf(956,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: (((sup_sup @ (set @ TA) @ A @ B) = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) = (((A = (bot_bot @ (set @ TA))) & (B = (insert @ TA @ C @ (bot_bot @ (set @ TA))))) | ((A = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) & (B = (bot_bot @ (set @ TA)))) | ((A = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) & (B = (insert @ TA @ C @ (bot_bot @ (set @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 53.05/29.09 thf(260,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_psubsetD)).
% 53.05/29.09 thf(1104,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:TA]: ((ord_less @ (set @ TA) @ A @ B) => ((member @ TA @ C @ A) => (member @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 53.05/29.09 thf(174,axiom,((! [TA: $tType]: ((insert @ TA) = (^ [A:TA]: (sup_sup @ (set @ TA) @ (collect @ TA @ (^ [B:TA]: (B = A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_insert__def)).
% 53.05/29.09 thf(849,plain,((! [TA: $tType]: ((insert @ TA) = (^ [A:TA]: (sup_sup @ (set @ TA) @ (collect @ TA @ (^ [B:TA]: (B = A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 53.05/29.09 thf(10,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_dual__order_Oirrefl)).
% 53.05/29.09 thf(307,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 53.05/29.09 thf(250,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ (insert @ TA @ A @ B) @ C) = ((member @ TA @ A @ C) & (ord_less_eq @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_insert__subset)).
% 53.05/29.09 thf(1074,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ (insert @ TA @ A @ B) @ C) = ((member @ TA @ A @ C) & (ord_less_eq @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 53.05/29.09 thf(47,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ C) = (sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_sup__assoc)).
% 53.05/29.09 thf(452,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ C) = (sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 53.05/29.09 thf(70,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_ord__eq__less__trans)).
% 53.05/29.09 thf(529,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 53.05/29.09 thf(197,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)).
% 53.05/29.09 thf(925,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)],[197])).
% 53.05/29.09 thf(25,axiom,((order @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder_24)).
% 53.05/29.09 thf(366,plain,((order @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 53.05/29.09 thf(279,axiom,((! [TA: $tType]: ((pairwise @ TA) = (^ [A:(TA > (TA > $o)),B:(set @ TA)]: ! [C:TA]: ((member @ TA @ C @ B) => (! [D:TA]: ((member @ TA @ D @ (minus_minus @ (set @ TA) @ B @ (insert @ TA @ C @ (bot_bot @ (set @ TA))))) => (A @ C @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_pairwise__alt)).
% 53.05/29.09 thf(1153,plain,((! [TA: $tType]: ((pairwise @ TA) = (^ [A:(TA > (TA > $o)),B:(set @ TA)]: ! [C:TA]: ((member @ TA @ C @ B) => (! [D:TA]: ((member @ TA @ D @ (minus_minus @ (set @ TA) @ B @ (insert @ TA @ C @ (bot_bot @ (set @ TA))))) => (A @ C @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[279])).
% 53.05/29.09 thf(142,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_sup_Ostrict__coboundedI2)).
% 53.05/29.09 thf(761,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 53.05/29.09 thf(241,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_92_singletonD)).
% 53.05/29.09 thf(1047,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)],[241])).
% 53.05/29.09 thf(156,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_104_Diff__insert2)).
% 53.05/29.09 thf(798,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)],[156])).
% 53.05/29.09 thf(138,axiom,((! [TA: $tType]: (! [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA),E:(binary1291135688e_Tree @ TA)]: (((ord_less @ int @ (A @ B) @ (A @ C)) => ((binary1830089824insert @ TA @ A @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ (binary1830089824insert @ TA @ A @ B @ D) @ C @ E))) & ((~ (ord_less @ int @ (A @ B) @ (A @ C))) => (((ord_less @ int @ (A @ C) @ (A @ B)) => ((binary1830089824insert @ TA @ A @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ D @ C @ (binary1830089824insert @ TA @ A @ B @ E)))) & ((~ (ord_less @ int @ (A @ C) @ (A @ B))) => ((binary1830089824insert @ TA @ A @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ D @ B @ E))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_binsert_Osimps_I2_J)).
% 53.05/29.09 thf(746,plain,((! [TA: $tType]: (! [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA),E:(binary1291135688e_Tree @ TA)]: (((ord_less @ int @ (A @ B) @ (A @ C)) => ((binary1830089824insert @ TA @ (A) @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ (binary1830089824insert @ TA @ (A) @ B @ D) @ C @ E))) & ((~ (ord_less @ int @ (A @ B) @ (A @ C))) => (((ord_less @ int @ (A @ C) @ (A @ B)) => ((binary1830089824insert @ TA @ (A) @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ D @ C @ (binary1830089824insert @ TA @ (A) @ B @ E)))) & ((~ (ord_less @ int @ (A @ C) @ (A @ B))) => ((binary1830089824insert @ TA @ (A) @ B @ (binary210054475elle_T @ TA @ D @ C @ E)) = (binary210054475elle_T @ TA @ D @ B @ E))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 53.05/29.09 thf(8,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A != B) => ((~ (ord_less @ TA @ A @ B)) => (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_neqE)).
% 53.05/29.09 thf(302,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) => ((~ (ord_less @ TA @ A @ B)) => (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 53.05/29.09 thf(86,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((bot_bot @ TA) = (sup_sup @ TA @ A @ B)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_bot__eq__sup__iff)).
% 53.05/29.09 thf(598,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((bot_bot @ TA) = (sup_sup @ TA @ A @ B)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 53.05/29.09 thf(79,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => ((! [D:TA]: ((A @ D) => (D = B))) => ((! [D:TA]: ((A @ D) => (C @ D))) => (C @ (the @ TA @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_theI2)).
% 53.05/29.09 thf(561,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => ((! [D:TA]: ((A @ D) => (D = B))) => ((! [D:TA]: ((A @ D) => (C @ D))) => (C @ (the @ TA @ (A))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 53.05/29.09 thf(6,axiom,((! [TA: $tType]: ((lattice @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ A @ B)) = (sup_sup @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_inf__sup__aci_I8_J)).
% 53.05/29.09 thf(297,plain,((! [TA: $tType]: ((lattice @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ A @ B)) = (sup_sup @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 53.05/29.09 thf(43,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_order__less__subst1)).
% 53.05/29.09 thf(424,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 53.05/29.09 thf(97,axiom,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ (bot_bot @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_bot_Oextremum__strict)).
% 53.05/29.09 thf(630,plain,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ (bot_bot @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 53.05/29.09 thf(162,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: (((insert @ TA @ A @ B) = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) = ((A = C) & (ord_less_eq @ (set @ TA) @ B @ (insert @ TA @ C @ (bot_bot @ (set @ TA))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_singleton__insert__inj__eq_H)).
% 53.05/29.09 thf(815,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:TA]: (((insert @ TA @ A @ B) = (insert @ TA @ C @ (bot_bot @ (set @ TA)))) = ((A = C) & (ord_less_eq @ (set @ TA) @ B @ (insert @ TA @ C @ (bot_bot @ (set @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 53.05/29.09 thf(194,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_not__less)).
% 53.05/29.09 thf(916,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 53.05/29.09 thf(59,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => ((sup_sup @ TA) = (^ [A:TA,B:TA]: (sup_sup @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_sup__commute)).
% 53.05/29.09 thf(484,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => ((sup_sup @ TA) = (^ [A:TA,B:TA]: (sup_sup @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 53.05/29.09 thf(236,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_52_DiffI)).
% 53.05/29.09 thf(1032,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)],[236])).
% 53.05/29.09 thf(23,axiom,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TB) => ((sup_sup @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (sup_sup @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_sup__fun__def)).
% 53.05/29.09 thf(361,plain,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TB) => ((sup_sup @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (sup_sup @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 53.05/29.09 thf(95,axiom,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((binary1610619414edTree @ TA @ A @ (binary210054475elle_T @ TA @ B @ C @ D)) => (binary1610619414edTree @ TA @ A @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_sortLemmaR)).
% 53.05/29.09 thf(625,plain,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((binary1610619414edTree @ TA @ (A) @ (binary210054475elle_T @ TA @ B @ C @ D)) => (binary1610619414edTree @ TA @ (A) @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 53.05/29.09 thf(175,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ (sup_sup @ (set @ TA) @ A @ B) @ C) = (sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_Un__assoc)).
% 53.05/29.09 thf(852,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ (sup_sup @ (set @ TA) @ A @ B) @ C) = (sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 53.05/29.09 thf(62,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((A = (sup_sup @ TA @ B @ C)) => ((sup_sup @ TA @ A @ D) = (sup_sup @ TA @ B @ (sup_sup @ TA @ C @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_boolean__algebra__cancel_Osup1)).
% 53.05/29.09 thf(493,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((A = (sup_sup @ TA @ B @ C)) => ((sup_sup @ TA @ A @ D) = (sup_sup @ TA @ B @ (sup_sup @ TA @ C @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 53.05/29.09 thf(140,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ B @ C)) = (sup_sup @ (set @ TA) @ B @ (sup_sup @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_Un__left__commute)).
% 53.05/29.09 thf(757,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (sup_sup @ (set @ TA) @ B @ C)) = (sup_sup @ (set @ TA) @ B @ (sup_sup @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 53.05/29.09 thf(117,axiom,((! [TA: $tType]: ((wellorder @ TA) => (! [A:(TA > $o),B:TA]: ((! [C:TA]: ((! [D:TA]: ((ord_less @ TA @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_less__induct)).
% 53.05/29.09 thf(682,plain,((! [TA: $tType]: ((wellorder @ TA) => (! [A:(TA > $o),B:TA]: ((! [C:TA]: ((! [D:TA]: ((ord_less @ TA @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 53.05/29.09 thf(75,axiom,((! [TA: $tType]: (! [A:TA]: ((the @ TA @ (^ [B:TA]: (B = A))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_the__eq__trivial)).
% 53.05/29.09 thf(551,plain,((! [TA: $tType]: (! [A:TA]: ((the @ TA @ (^ [B:TA]: (B = A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 53.05/29.09 thf(124,axiom,((! [TA: $tType]: (bounded_lattice @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Obounded__lattice_1)).
% 53.05/29.09 thf(710,plain,((! [TA: $tType]: (bounded_lattice @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 53.05/29.09 thf(217,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)).
% 53.05/29.09 thf(974,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ (B))) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 53.05/29.09 thf(261,axiom,((! [TA: $tType]: ((bot_bot @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_bot__empty__eq)).
% 53.05/29.09 thf(1106,plain,((! [TA: $tType]: ((bot_bot @ (TA > $o)) = (^ [A:TA]: (member @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 53.05/29.09 thf(18,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_ord__less__eq__subst)).
% 53.05/29.09 thf(329,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 53.05/29.09 thf(285,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)) = ((member @ TA @ A @ B) | (member @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_Un__iff)).
% 53.05/29.09 thf(1178,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)) = ((member @ TA @ A @ B) | (member @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[285])).
% 53.05/29.09 thf(281,axiom,(((binary1610619414edTree @ a @ h @ (binary1746293266le_Tip @ a)) => ((binary1653327646_setOf @ a @ (binary1830089824insert @ a @ h @ e @ (binary1746293266le_Tip @ a))) = (sup_sup @ (set @ a) @ (minus_minus @ (set @ a) @ (binary1653327646_setOf @ a @ (binary1746293266le_Tip @ a)) @ (binary64540844le_eqs @ a @ h @ e)) @ (insert @ a @ e @ (bot_bot @ (set @ a))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12__092_060open_062sortedTree_Ah_ATip_A_092_060longrightarrow_062_AsetOf_A_Ibinsert_Ah_Ae_ATip_J_A_061_AsetOf_ATip_A_N_Aeqs_Ah_Ae_A_092_060union_062_A_123e_125_092_060close_062)).
% 53.05/29.09 thf(1159,plain,(((binary1610619414edTree @ a @ (h) @ (binary1746293266le_Tip @ a)) => ((binary1653327646_setOf @ a @ (binary1830089824insert @ a @ (h) @ e @ (binary1746293266le_Tip @ a))) = (sup_sup @ (set @ a) @ (minus_minus @ (set @ a) @ (binary1653327646_setOf @ a @ (binary1746293266le_Tip @ a)) @ (binary64540844le_eqs @ a @ (h) @ e)) @ (insert @ a @ e @ (bot_bot @ (set @ a))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[281])).
% 53.05/29.09 thf(50,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oord)).
% 53.05/29.09 thf(461,plain,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 53.05/29.09 thf(252,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_UnI2)).
% 53.05/29.09 thf(1079,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 53.05/29.09 thf(233,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_79_DiffD2)).
% 53.05/29.09 thf(1027,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)],[233])).
% 53.05/29.09 thf(230,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_84_insert__compr)).
% 53.05/29.09 thf(1017,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)],[230])).
% 53.05/29.09 thf(263,axiom,(((binary1653327646_setOf @ a @ (binary1830089824insert @ a @ h @ e @ t2)) = (sup_sup @ (set @ a) @ (minus_minus @ (set @ a) @ (binary1653327646_setOf @ a @ t2) @ (binary64540844le_eqs @ a @ h @ e)) @ (insert @ a @ e @ (bot_bot @ (set @ a)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_c2)).
% 53.05/29.09 thf(1111,plain,(((binary1653327646_setOf @ a @ (binary1830089824insert @ a @ (h) @ e @ t2)) = (sup_sup @ (set @ a) @ (minus_minus @ (set @ a) @ (binary1653327646_setOf @ a @ t2) @ (binary64540844le_eqs @ a @ (h) @ e)) @ (insert @ a @ e @ (bot_bot @ (set @ a)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 53.05/29.09 thf(130,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ (insert @ TA @ A @ B) @ C) = (insert @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_Un__insert__left)).
% 53.05/29.09 thf(725,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((sup_sup @ (set @ TA) @ (insert @ TA @ A @ B) @ C) = (insert @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 53.05/29.09 thf(181,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: (((~ (A @ B)) => (C @ B)) => (sup_sup @ (TA > $o) @ C @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_sup1CI)).
% 53.05/29.09 thf(869,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > $o)]: (((~ (A @ B)) => (C @ B)) => (sup_sup @ (TA > $o) @ (C) @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 53.05/29.09 thf(150,axiom,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ((A != (bot_bot @ TA)) = (ord_less @ TA @ (bot_bot @ TA) @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_bot_Onot__eq__extremum)).
% 53.05/29.09 thf(783,plain,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ((~ (A = (bot_bot @ TA))) = (ord_less @ TA @ (bot_bot @ TA) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 53.05/29.09 thf(54,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B) | (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_less__linear)).
% 53.05/29.09 thf(471,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B) | (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 53.05/29.09 thf(186,axiom,((! [TA: $tType]: (! [A:((binary1291135688e_Tree @ TA) > $o),B:(binary1291135688e_Tree @ TA)]: ((A @ (binary1746293266le_Tip @ TA)) => ((! [C:(binary1291135688e_Tree @ TA),D:TA,E:(binary1291135688e_Tree @ TA)]: ((A @ C) => ((A @ E) => (A @ (binary210054475elle_T @ TA @ C @ D @ E))))) => (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_Tree_Oinduct)).
% 53.05/29.09 thf(884,plain,((! [TA: $tType]: (! [A:((binary1291135688e_Tree @ TA) > $o),B:(binary1291135688e_Tree @ TA)]: ((A @ (binary1746293266le_Tip @ TA)) => ((! [C:(binary1291135688e_Tree @ TA),D:TA,E:(binary1291135688e_Tree @ TA)]: ((A @ C) => ((A @ E) => (A @ (binary210054475elle_T @ TA @ C @ D @ E))))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 53.05/29.09 thf(76,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ A @ B)) = (sup_sup @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_sup_Oleft__idem)).
% 53.05/29.09 thf(554,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ A @ B)) = (sup_sup @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 53.05/29.09 thf(188,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:TA,C:(binary1291135688e_Tree @ TA)]: ((binary1746293266le_Tip @ TA) != (binary210054475elle_T @ TA @ A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_Tree_Odistinct_I1_J)).
% 53.05/29.09 thf(901,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:TA,C:(binary1291135688e_Tree @ TA)]: ~ ((binary1746293266le_Tip @ TA) = (binary210054475elle_T @ TA @ A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 53.05/29.09 thf(100,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_196_is__singleton__def)).
% 53.05/29.09 thf(637,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)],[100])).
% 53.05/29.09 thf(116,axiom,((! [TA: $tType]: ((insert @ TA) = (^ [A:TA]: (sup_sup @ (set @ TA) @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_insert__is__Un)).
% 53.05/29.09 thf(679,plain,((! [TA: $tType]: ((insert @ TA) = (^ [A:TA]: (sup_sup @ (set @ TA) @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 53.05/29.09 thf(170,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_90_doubleton__eq__iff)).
% 53.05/29.09 thf(837,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)],[170])).
% 53.05/29.09 thf(34,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_ord__eq__less__subst)).
% 53.05/29.09 thf(393,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 53.05/29.09 thf(258,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_31_Diff__insert0)).
% 53.05/29.09 thf(1099,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)],[258])).
% 53.05/29.09 thf(121,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_156_is__singleton__the__elem)).
% 53.05/29.09 thf(701,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)],[121])).
% 53.05/29.09 thf(192,axiom,((! [TA: $tType]: (! [A:TA]: (is_singleton @ TA @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_is__singletonI)).
% 53.05/29.09 thf(911,plain,((! [TA: $tType]: (! [A:TA]: (is_singleton @ TA @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 53.05/29.09 thf(128,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_50_Diff__idemp)).
% 53.05/29.09 thf(721,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)],[128])).
% 53.05/29.09 thf(225,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_64_insert__ident)).
% 53.05/29.09 thf(1002,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)],[225])).
% 53.05/29.09 thf(149,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_order__less__le__subst2)).
% 53.05/29.09 thf(779,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 53.05/29.09 thf(66,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA]: (A @ D @ D)) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_162_linorder__less__wlog)).
% 53.05/29.09 thf(503,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA]: (A @ D @ D)) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 53.05/29.09 thf(245,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:TA,C:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ (insert @ TA @ B @ C)) = (((member @ TA @ B @ C) => (ord_less @ (set @ TA) @ A @ C)) & ((~ (member @ TA @ B @ C)) => (((member @ TA @ B @ A) => (ord_less @ (set @ TA) @ (minus_minus @ (set @ TA) @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) @ C)) & ((~ (member @ TA @ B @ A)) => (ord_less_eq @ (set @ TA) @ A @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_psubset__insert__iff)).
% 53.05/29.09 thf(1060,plain,((! [TA: $tType]: (! [A:(set @ TA),B:TA,C:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ (insert @ TA @ B @ C)) = (((member @ TA @ B @ C) => (ord_less @ (set @ TA) @ A @ C)) & ((~ (member @ TA @ B @ C)) => (((member @ TA @ B @ A) => (ord_less @ (set @ TA) @ (minus_minus @ (set @ TA) @ A @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) @ C)) & ((~ (member @ TA @ B @ A)) => (ord_less_eq @ (set @ TA) @ A @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 53.05/29.09 thf(242,axiom,((! [TA: $tType]: ((binary231205461t_pred @ TA) = (^ [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA)]: (((binary1610619414edTree @ TA @ A @ D) & (member @ TA @ B @ (binary1653327646_setOf @ TA @ D)) & (member @ TA @ C @ (binary1653327646_setOf @ TA @ D)) & ((A @ B) = (A @ C))) => (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_sorted__distinct__pred__def)).
% 53.05/29.09 thf(1050,plain,((! [TA: $tType]: ((binary231205461t_pred @ TA) = (^ [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA)]: (((binary1610619414edTree @ TA @ A @ D) & (member @ TA @ B @ (binary1653327646_setOf @ TA @ D)) & (member @ TA @ C @ (binary1653327646_setOf @ TA @ D)) & ((A @ B) = (A @ C))) => (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 53.05/29.09 thf(154,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA)]: ((A != (binary1746293266le_Tip @ TA)) => (~ (! [B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: (A != (binary210054475elle_T @ TA @ B @ C @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_Tree_Oexhaust)).
% 53.05/29.09 thf(792,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA)]: ((~ (A = (binary1746293266le_Tip @ TA))) => (~ (! [B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ~ (A = (binary210054475elle_T @ TA @ B @ C @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 53.05/29.09 thf(249,axiom,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) | (member @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_Un__def)).
% 53.05/29.09 thf(1071,plain,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (collect @ TA @ (^ [C:TA]: ((member @ TA @ C @ A) | (member @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 53.05/29.09 thf(147,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_197_is__singletonE)).
% 53.05/29.09 thf(773,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)],[147])).
% 53.05/29.09 thf(109,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o),C:TA]: ((sup_sup @ (TA > $o) @ A @ B @ C) => ((~ (A @ C)) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_sup1E)).
% 53.05/29.09 thf(662,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o),C:TA]: ((sup_sup @ (TA > $o) @ (A) @ (B) @ C) => ((~ (A @ C)) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 53.05/29.09 thf(127,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_26_insert__Diff__single)).
% 53.05/29.09 thf(718,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)],[127])).
% 53.05/29.09 thf(190,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_less__supI1)).
% 53.05/29.09 thf(906,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 53.05/29.09 thf(93,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ A) = (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_Diff__cancel)).
% 53.05/29.09 thf(618,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((minus_minus @ (set @ TA) @ A @ A) = (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 53.05/29.09 thf(276,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))) = (^ [C:TA]: (member @ TA @ C @ (sup_sup @ (set @ TA) @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_sup__Un__eq)).
% 53.05/29.09 thf(1146,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))) = (^ [C:TA]: (member @ TA @ C @ (sup_sup @ (set @ TA) @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[276])).
% 53.05/29.09 thf(87,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((A != B) => (ord_less @ TA @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_le__neq__trans)).
% 53.05/29.09 thf(601,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((~ (A = B)) => (ord_less @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 53.05/29.09 thf(271,axiom,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_empty__iff)).
% 53.05/29.09 thf(1135,plain,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 53.05/29.09 thf(39,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ B) = (sup_sup @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_sup_Oright__idem)).
% 53.05/29.09 thf(412,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ B) = (sup_sup @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 53.05/29.09 thf(30,axiom,((! [TA: $tType]: (! [A:(TA > $o)]: ((? [B:TA]: ((A @ B) & ! [C:TA]: ((A @ C) => (C = B)))) => (A @ (the @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_theI_H)).
% 53.05/29.09 thf(375,plain,((! [TA: $tType]: (! [A:(TA > $o)]: ((? [B:TA]: ((A @ B) & ! [C:TA]: ((A @ C) => (C = B)))) => (A @ (the @ TA @ (A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 53.05/29.09 thf(133,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_41_insert__absorb2)).
% 53.05/29.09 thf(733,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)],[133])).
% 53.05/29.09 thf(189,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_less__supI2)).
% 53.05/29.09 thf(904,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 53.05/29.09 thf(119,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_order__le__less__subst2)).
% 53.05/29.09 thf(694,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 53.05/29.09 thf(132,axiom,((lattice @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Lattices_Olattice_5)).
% 53.05/29.09 thf(732,plain,((lattice @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 53.05/29.09 thf(172,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((minus_minus @ (set @ TA) @ (sup_sup @ (set @ TA) @ A @ B) @ C) = (sup_sup @ (set @ TA) @ (minus_minus @ (set @ TA) @ A @ C) @ (minus_minus @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_Un__Diff)).
% 53.05/29.09 thf(843,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((minus_minus @ (set @ TA) @ (sup_sup @ (set @ TA) @ A @ B) @ C) = (sup_sup @ (set @ TA) @ (minus_minus @ (set @ TA) @ A @ C) @ (minus_minus @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 53.05/29.09 thf(146,axiom,((minus @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Groups_Ominus_27)).
% 53.05/29.09 thf(772,plain,((minus @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 53.05/29.09 thf(166,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (A != B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_less__le)).
% 53.05/29.09 thf(826,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 53.05/29.09 thf(268,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_60_mk__disjoint__insert)).
% 53.05/29.09 thf(1124,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)],[268])).
% 53.05/29.09 thf(73,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_bot__fun__def)).
% 53.05/29.09 thf(545,plain,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 53.05/29.09 thf(12,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => ((sup_sup @ TA) = (^ [A:TA,B:TA]: (sup_sup @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_sup_Ocommute)).
% 53.05/29.09 thf(313,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => ((sup_sup @ TA) = (^ [A:TA,B:TA]: (sup_sup @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 53.05/29.09 thf(90,axiom,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (bot_bot @ (TA > $o)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_bot__set__def)).
% 53.05/29.09 thf(611,plain,((! [TA: $tType]: ((bot_bot @ (set @ TA)) = (collect @ TA @ (bot_bot @ (TA > $o)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 53.05/29.09 thf(64,axiom,((! [TA: $tType]: (minus @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Groups_Ominus_17)).
% 53.05/29.09 thf(498,plain,((! [TA: $tType]: (minus @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 53.05/29.09 thf(122,axiom,((! [TA: $tType]: (! [A:TA]: ((the_elem @ TA @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_the__elem__eq)).
% 53.05/29.09 thf(704,plain,((! [TA: $tType]: (! [A:TA]: ((the_elem @ TA @ (insert @ TA @ A @ (bot_bot @ (set @ TA)))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 53.05/29.09 thf(21,axiom,((! [TA: $tType]: (bot @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Obot_16)).
% 53.05/29.09 thf(350,plain,((! [TA: $tType]: (bot @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 53.05/29.09 thf(195,axiom,((! [TA: $tType]: (! [A:TA]: ((collect @ TA @ ((=) @ TA @ A)) = (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_singleton__conv2)).
% 53.05/29.09 thf(919,plain,((! [TA: $tType]: (! [A:TA]: ((collect @ TA @ ((=) @ TA @ A)) = (insert @ TA @ A @ (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 53.05/29.09 thf(158,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_diff__strict__left__mono)).
% 53.05/29.09 thf(804,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 53.05/29.09 thf(37,axiom,((! [TA: $tType]: (ord @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oord_15)).
% 53.05/29.09 thf(406,plain,((! [TA: $tType]: (ord @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 53.05/29.09 thf(134,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:TA,C:(binary1291135688e_Tree @ TA),D:(binary1291135688e_Tree @ TA),E:TA,F:(binary1291135688e_Tree @ TA)]: (((binary210054475elle_T @ TA @ A @ B @ C) = (binary210054475elle_T @ TA @ D @ E @ F)) = ((A = D) & (B = E) & (C = F)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_Tree_Oinject)).
% 53.05/29.09 thf(736,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:TA,C:(binary1291135688e_Tree @ TA),D:(binary1291135688e_Tree @ TA),E:TA,F:(binary1291135688e_Tree @ TA)]: (((binary210054475elle_T @ TA @ A @ B @ C) = (binary210054475elle_T @ TA @ D @ E @ F)) = ((A = D) & (B = E) & (C = F)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 53.05/29.09 thf(104,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_empty__subsetI)).
% 53.05/29.09 thf(649,plain,((! [TA: $tType]: (! [A:(set @ TA)]: (ord_less_eq @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 53.05/29.09 thf(267,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_UnI1)).
% 53.05/29.09 thf(1122,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: ((member @ TA @ A @ B) => (member @ TA @ A @ (sup_sup @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 53.05/29.09 thf(284,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_51_Diff__iff)).
% 53.05/29.09 thf(1175,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)],[284])).
% 53.05/29.09 thf(219,axiom,((! [TA: $tType]: (! [A:TA,B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((member @ TA @ A @ (binary2130109271t_Tree @ TA @ B)) => (member @ TA @ A @ (binary2130109271t_Tree @ TA @ (binary210054475elle_T @ TA @ B @ C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_Tree_Oset__intros_I1_J)).
% 53.05/29.09 thf(979,plain,((! [TA: $tType]: (! [A:TA,B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((member @ TA @ A @ (binary2130109271t_Tree @ TA @ B)) => (member @ TA @ A @ (binary2130109271t_Tree @ TA @ (binary210054475elle_T @ TA @ B @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 53.05/29.09 thf(88,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_order__le__less__subst1)).
% 53.05/29.09 thf(604,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 53.05/29.09 thf(228,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((? [D:TA]: ((member @ TA @ D @ (sup_sup @ (set @ TA) @ A @ B)) & (C @ D))) = (? [D:TA]: ((member @ TA @ D @ A) & (C @ D)) | ? [D:TA]: ((member @ TA @ D @ B) & (C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_bex__Un)).
% 53.05/29.09 thf(1011,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(TA > $o)]: ((? [D:TA]: ((member @ TA @ D @ (sup_sup @ (set @ TA) @ A @ B)) & (C @ D))) = (? [D:TA]: ((member @ TA @ D @ A) & (C @ D)) | ? [D:TA]: ((member @ TA @ D @ B) & (C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 53.05/29.09 thf(41,axiom,((! [TA: $tType]: ((lattice @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ C) = (sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_inf__sup__aci_I6_J)).
% 53.05/29.09 thf(419,plain,((! [TA: $tType]: ((lattice @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ C) = (sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 53.05/29.09 thf(56,axiom,((bounde1808546759up_bot @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Obounded__semilattice__sup__bot_18)).
% 53.05/29.09 thf(477,plain,((bounde1808546759up_bot @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 53.05/29.09 thf(32,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_sup__idem)).
% 53.05/29.09 thf(387,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 53.05/29.09 thf(16,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((B = C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_ord__less__eq__trans)).
% 53.05/29.09 thf(323,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((B = C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 53.05/29.09 thf(282,axiom,((! [TA: $tType]: ((ord_less @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (ord_less @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_less__set__def)).
% 53.05/29.09 thf(1162,plain,((! [TA: $tType]: ((ord_less @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (ord_less @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 53.05/29.09 thf(94,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_order__less__le__subst1)).
% 53.05/29.09 thf(621,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 53.05/29.09 thf(234,axiom,((binary1610619414edTree @ a @ h @ t1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_s1)).
% 53.05/29.09 thf(1029,plain,((binary1610619414edTree @ a @ (h) @ t1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 53.05/29.09 thf(277,axiom,((! [A:a]: ((member @ a @ A @ (binary64540844le_eqs @ a @ h @ e)) => (ord_less @ int @ (h @ A) @ (h @ x))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_eqsLessX)).
% 53.05/29.09 thf(1149,plain,((! [A:a]: ((member @ a @ A @ (binary64540844le_eqs @ a @ (h) @ e)) => (ord_less @ int @ (h @ A) @ (h @ x))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[277])).
% 53.05/29.09 thf(145,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((B = (sup_sup @ TA @ B @ A)) & (B != A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_sup_Ostrict__order__iff)).
% 53.05/29.09 thf(769,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((B = (sup_sup @ TA @ B @ A)) & ~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 53.05/29.09 thf(177,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((A != B) => (ord_less @ (set @ TA) @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_psubsetI)).
% 53.05/29.09 thf(858,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((~ (A = B)) => (ord_less @ (set @ TA) @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 53.05/29.09 thf(26,axiom,((semilattice_sup @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Lattices_Osemilattice__sup_3)).
% 53.05/29.09 thf(367,plain,((semilattice_sup @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 53.05/29.09 thf(67,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_order_Ostrict__implies__not__eq)).
% 53.05/29.09 thf(521,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 53.05/29.09 thf(209,axiom,((ordered_ab_group_add @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Oordered__ab__group__add)).
% 53.05/29.09 thf(959,plain,((ordered_ab_group_add @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 53.05/29.09 thf(240,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)).
% 53.05/29.09 thf(1044,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)],[240])).
% 53.05/29.09 thf(247,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: (member @ TA @ A @ (insert @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_insertI1)).
% 53.05/29.09 thf(1066,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA)]: (member @ TA @ A @ (insert @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 53.05/29.09 thf(48,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((A != B) => (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_linorder__cases)).
% 53.05/29.09 thf(455,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (A = B)) => (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 53.05/29.09 thf(89,axiom,((! [TA: $tType]: (! [A:(TA > int),B:TA]: ((binary1830089824insert @ TA @ A @ B @ (binary1746293266le_Tip @ TA)) = (binary210054475elle_T @ TA @ (binary1746293266le_Tip @ TA) @ B @ (binary1746293266le_Tip @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_binsert_Osimps_I1_J)).
% 53.05/29.09 thf(608,plain,((! [TA: $tType]: (! [A:(TA > int),B:TA]: ((binary1830089824insert @ TA @ (A) @ B @ (binary1746293266le_Tip @ TA)) = (binary210054475elle_T @ TA @ (binary1746293266le_Tip @ TA) @ B @ (binary1746293266le_Tip @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 53.05/29.09 thf(264,axiom,(((binary1610619414edTree @ a @ h @ t2) => ((binary1653327646_setOf @ a @ (binary1830089824insert @ a @ h @ e @ t2)) = (sup_sup @ (set @ a) @ (minus_minus @ (set @ a) @ (binary1653327646_setOf @ a @ t2) @ (binary64540844le_eqs @ a @ h @ e)) @ (insert @ a @ e @ (bot_bot @ (set @ a))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_h2)).
% 53.05/29.09 thf(1113,plain,(((binary1610619414edTree @ a @ (h) @ t2) => ((binary1653327646_setOf @ a @ (binary1830089824insert @ a @ (h) @ e @ t2)) = (sup_sup @ (set @ a) @ (minus_minus @ (set @ a) @ (binary1653327646_setOf @ a @ t2) @ (binary64540844le_eqs @ a @ (h) @ e)) @ (insert @ a @ e @ (bot_bot @ (set @ a))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 53.05/29.09 thf(259,axiom,(((binary1830089824insert @ a @ h @ e @ (binary210054475elle_T @ a @ t1 @ x @ t2)) = (binary210054475elle_T @ a @ (binary1830089824insert @ a @ h @ e @ t1) @ x @ t2))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_res)).
% 53.05/29.09 thf(1102,plain,(((binary1830089824insert @ a @ (h) @ e @ (binary210054475elle_T @ a @ t1 @ x @ t2)) = (binary210054475elle_T @ a @ (binary1830089824insert @ a @ (h) @ e @ t1) @ x @ t2))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 53.05/29.09 thf(106,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_Un__empty__left)).
% 53.05/29.09 thf(653,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((sup_sup @ (set @ TA) @ (bot_bot @ (set @ TA)) @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 53.05/29.09 thf(196,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((sup_sup @ TA @ A @ B) = (bot_bot @ TA)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_sup__bot_Oeq__neutr__iff)).
% 53.05/29.09 thf(922,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((sup_sup @ TA @ A @ B) = (bot_bot @ TA)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 53.05/29.09 thf(237,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (remove @ TA @ B @ C)) = ((member @ TA @ A @ C) & (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_member__remove)).
% 53.05/29.09 thf(1034,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: ((member @ TA @ A @ (remove @ TA @ B @ C)) = ((member @ TA @ A @ C) & ~ (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 53.05/29.09 thf(61,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TB) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_minus__apply)).
% 53.05/29.09 thf(490,plain,((! [TA: $tType,TB: $tType]: ((minus @ TB) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 53.05/29.09 thf(83,axiom,((! [TA: $tType]: ((the_elem @ TA) = (^ [A:(set @ TA)]: (the @ TA @ (^ [B:TA]: (A = (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_the__elem__def)).
% 53.05/29.09 thf(589,plain,((! [TA: $tType]: ((the_elem @ TA) = (^ [A:(set @ TA)]: (the @ TA @ (^ [B:TA]: (A = (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 53.05/29.09 thf(155,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ A) => (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_subset__antisym)).
% 53.05/29.09 thf(795,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ A) => (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 53.05/29.09 thf(74,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C)) = (sup_sup @ TA @ B @ (sup_sup @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_sup__left__commute)).
% 53.05/29.09 thf(548,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C)) = (sup_sup @ TA @ B @ (sup_sup @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 53.05/29.09 thf(60,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ A @ B)) = (sup_sup @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_sup__left__idem)).
% 53.05/29.09 thf(487,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA]: ((sup_sup @ TA @ A @ (sup_sup @ TA @ A @ B)) = (sup_sup @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 53.05/29.09 thf(161,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((ord_less_eq @ TA @ A @ B) = (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_254_antisym__conv1)).
% 53.05/29.09 thf(812,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((ord_less_eq @ TA @ A @ B) = (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 53.05/29.09 thf(253,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_58_equals0D)).
% 53.05/29.09 thf(1081,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)],[253])).
% 53.05/29.09 thf(92,axiom,((bot @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Obot_26)).
% 53.05/29.09 thf(617,plain,((bot @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 53.05/29.09 thf(275,axiom,((binary1610619414edTree @ a @ h @ (binary210054475elle_T @ a @ t1 @ x @ t2))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_s)).
% 53.05/29.09 thf(1145,plain,((binary1610619414edTree @ a @ (h) @ (binary210054475elle_T @ a @ t1 @ x @ t2))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[275])).
% 53.05/29.09 thf(139,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ (sup_sup @ TA @ A @ B) @ C) = ((ord_less_eq @ TA @ A @ C) & (ord_less_eq @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_le__sup__iff)).
% 53.05/29.09 thf(754,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ (sup_sup @ TA @ A @ B) @ C) = ((ord_less_eq @ TA @ A @ C) & (ord_less_eq @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 53.05/29.09 thf(49,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = ((ord_less @ TA @ B @ A) | (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_not__less__iff__gr__or__eq)).
% 53.05/29.09 thf(458,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = ((ord_less @ TA @ B @ A) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 53.05/29.09 thf(286,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_63_insert__absorb)).
% 53.05/29.09 thf(1181,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)],[286])).
% 53.05/29.09 thf(148,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)).
% 53.05/29.09 thf(776,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)],[148])).
% 53.05/29.09 thf(68,axiom,((! [TA: $tType]: (order_bot @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oorder__bot_11)).
% 53.05/29.09 thf(525,plain,((! [TA: $tType]: (order_bot @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 53.05/29.09 thf(101,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ (bot_bot @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_sup__bot__right)).
% 53.05/29.09 thf(640,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ (bot_bot @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 53.05/29.09 thf(5,axiom,((! [TA: $tType]: (order @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oorder_14)).
% 53.05/29.09 thf(295,plain,((! [TA: $tType]: (order @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 53.05/29.09 thf(280,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_105_insert__Diff)).
% 53.05/29.09 thf(1156,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)],[280])).
% 53.05/29.09 thf(123,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ (bot_bot @ TA) @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_sup__bot__left)).
% 53.05/29.09 thf(707,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ (bot_bot @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 53.05/29.09 thf(216,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_42_insert__iff)).
% 53.05/29.09 thf(971,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)],[216])).
% 53.05/29.09 thf(17,axiom,((! [TA: $tType]: (bounde1808546759up_bot @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Obounded__semilattice__sup__bot_9)).
% 53.05/29.09 thf(327,plain,((! [TA: $tType]: (bounde1808546759up_bot @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 53.05/29.09 thf(207,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ D) => (ord_less @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_diff__strict__mono)).
% 53.05/29.09 thf(954,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ D) => (ord_less @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 53.05/29.09 thf(135,axiom,((! [TA: $tType]: (! [A:(TA > int)]: (binary1610619414edTree @ TA @ A @ (binary1746293266le_Tip @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_sortedTree_Osimps_I1_J)).
% 53.05/29.09 thf(739,plain,((! [TA: $tType]: (! [A:(TA > int)]: (binary1610619414edTree @ TA @ (A) @ (binary1746293266le_Tip @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 53.05/29.09 thf(125,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:TA,C:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (insert @ TA @ B @ C)) = (insert @ TA @ B @ (sup_sup @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_Un__insert__right)).
% 53.05/29.09 thf(712,plain,((! [TA: $tType]: (! [A:(set @ TA),B:TA,C:(set @ TA)]: ((sup_sup @ (set @ TA) @ A @ (insert @ TA @ B @ C)) = (insert @ TA @ B @ (sup_sup @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 53.05/29.09 thf(77,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TA) => (bot @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Obot)).
% 53.05/29.09 thf(557,plain,((! [TA: $tType,TB: $tType]: ((bot @ TA) => (bot @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 53.05/29.09 thf(80,axiom,((! [TA: $tType]: (semilattice_sup @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Osemilattice__sup_10)).
% 53.05/29.09 thf(580,plain,((! [TA: $tType]: (semilattice_sup @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 53.05/29.09 thf(176,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((A = B) = (C = D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_diff__eq__diff__eq)).
% 53.05/29.09 thf(855,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((A = B) = (C = D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 53.05/29.09 thf(243,axiom,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_emptyE)).
% 53.05/29.09 thf(1053,plain,((! [TA: $tType]: (! [A:TA]: ~ (member @ TA @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 53.05/29.09 thf(113,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ (sup_sup @ (set @ TA) @ A @ B) @ C) = ((ord_less_eq @ (set @ TA) @ A @ C) & (ord_less_eq @ (set @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_Un__subset__iff)).
% 53.05/29.09 thf(673,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ (sup_sup @ (set @ TA) @ A @ B) @ C) = ((ord_less_eq @ (set @ TA) @ A @ C) & (ord_less_eq @ (set @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 53.05/29.09 thf(153,axiom,((group_add @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Ogroup__add)).
% 53.05/29.09 thf(791,plain,((group_add @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 53.05/29.09 thf(82,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_less__imp__not__eq)).
% 53.05/29.09 thf(585,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 53.05/29.09 thf(171,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:TA,C:(binary1291135688e_Tree @ TA)]: ((binary1653327646_setOf @ TA @ (binary210054475elle_T @ TA @ A @ B @ C)) = (sup_sup @ (set @ TA) @ (sup_sup @ (set @ TA) @ (binary1653327646_setOf @ TA @ A) @ (binary1653327646_setOf @ TA @ C)) @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_setOf_Osimps_I2_J)).
% 53.05/29.09 thf(840,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:TA,C:(binary1291135688e_Tree @ TA)]: ((binary1653327646_setOf @ TA @ (binary210054475elle_T @ TA @ A @ B @ C)) = (sup_sup @ (set @ TA) @ (sup_sup @ (set @ TA) @ (binary1653327646_setOf @ TA @ A) @ (binary1653327646_setOf @ TA @ C)) @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 53.05/29.09 thf(51,axiom,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TA) => (semilattice_sup @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Osemilattice__sup)).
% 53.05/29.09 thf(463,plain,((! [TA: $tType,TB: $tType]: ((semilattice_sup @ TA) => (semilattice_sup @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 53.05/29.09 thf(254,axiom,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (collect @ TA @ (sup_sup @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_sup__set__def)).
% 53.05/29.09 thf(1085,plain,((! [TA: $tType]: ((sup_sup @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (collect @ TA @ (sup_sup @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 53.05/29.09 thf(206,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_le__less)).
% 53.05/29.09 thf(951,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 53.05/29.09 thf(102,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)).
% 53.05/29.09 thf(643,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)],[102])).
% 53.05/29.09 thf(137,axiom,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_gt__ex)).
% 53.05/29.09 thf(744,plain,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 53.05/29.09 thf(273,axiom,((binary1610619414edTree @ a @ h @ t2)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_s2)).
% 53.05/29.09 thf(1141,plain,((binary1610619414edTree @ a @ (h) @ t2)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[273])).
% 53.05/29.09 thf(107,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: (((insert @ TA @ A @ (bot_bot @ (set @ TA))) = (insert @ TA @ B @ C)) = ((B = A) & (ord_less_eq @ (set @ TA) @ C @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_singleton__insert__inj__eq)).
% 53.05/29.09 thf(656,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(set @ TA)]: (((insert @ TA @ A @ (bot_bot @ (set @ TA))) = (insert @ TA @ B @ C)) = ((B = A) & (ord_less_eq @ (set @ TA) @ C @ (insert @ TA @ A @ (bot_bot @ (set @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 53.05/29.09 thf(179,axiom,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_lt__ex)).
% 53.05/29.09 thf(864,plain,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 53.05/29.09 thf(227,axiom,((! [TA: $tType]: ((minus_minus @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (collect @ TA @ (minus_minus @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_minus__set__def)).
% 53.05/29.09 thf(1008,plain,((! [TA: $tType]: ((minus_minus @ (set @ TA)) = (^ [A:(set @ TA),B:(set @ TA)]: (collect @ TA @ (minus_minus @ (TA > $o) @ (^ [C:TA]: (member @ TA @ C @ A)) @ (^ [C:TA]: (member @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 53.05/29.09 thf(85,axiom,((! [TA: $tType]: ((cancel146912293up_add @ TA) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (minus_minus @ TA @ A @ C) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_diff__right__commute)).
% 53.05/29.09 thf(595,plain,((! [TA: $tType]: ((cancel146912293up_add @ TA) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (minus_minus @ TA @ A @ C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 53.05/29.09 thf(256,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_87_set__diff__eq)).
% 53.05/29.09 thf(1094,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)],[256])).
% 53.05/29.09 thf(31,axiom,((lattice @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Olattice_23)).
% 53.05/29.09 thf(386,plain,((lattice @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 53.05/29.09 thf(63,axiom,((semilattice_sup @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Lattices_Osemilattice__sup_19)).
% 53.05/29.09 thf(497,plain,((semilattice_sup @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 53.05/29.09 thf(183,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => ((ord_less @ (set @ TA) @ B @ C) => (ord_less @ (set @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_psubset__trans)).
% 53.05/29.09 thf(876,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA),C:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => ((ord_less @ (set @ TA) @ B @ C) => (ord_less @ (set @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 53.05/29.09 thf(52,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((A = (sup_sup @ TA @ B @ C)) => ((sup_sup @ TA @ D @ A) = (sup_sup @ TA @ B @ (sup_sup @ TA @ D @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_boolean__algebra__cancel_Osup2)).
% 53.05/29.09 thf(465,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((A = (sup_sup @ TA @ B @ C)) => ((sup_sup @ TA @ D @ A) = (sup_sup @ TA @ B @ (sup_sup @ TA @ D @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 53.05/29.09 thf(96,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_36_empty__Diff)).
% 53.05/29.09 thf(627,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)],[96])).
% 53.05/29.09 thf(46,axiom,((! [TA: $tType]: (lattice @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Lattices_Olattice_13)).
% 53.05/29.09 thf(450,plain,((! [TA: $tType]: (lattice @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 53.05/29.09 thf(199,axiom,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((insert @ TA @ A @ (bot_bot @ (set @ TA))) = (sup_sup @ (set @ TA) @ B @ C)) = (((B = (bot_bot @ (set @ TA))) & (C = (insert @ TA @ A @ (bot_bot @ (set @ TA))))) | ((B = (insert @ TA @ A @ (bot_bot @ (set @ TA)))) & (C = (bot_bot @ (set @ TA)))) | ((B = (insert @ TA @ A @ (bot_bot @ (set @ TA)))) & (C = (insert @ TA @ A @ (bot_bot @ (set @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_singleton__Un__iff)).
% 53.05/29.09 thf(931,plain,((! [TA: $tType]: (! [A:TA,B:(set @ TA),C:(set @ TA)]: (((insert @ TA @ A @ (bot_bot @ (set @ TA))) = (sup_sup @ (set @ TA) @ B @ C)) = (((B = (bot_bot @ (set @ TA))) & (C = (insert @ TA @ A @ (bot_bot @ (set @ TA))))) | ((B = (insert @ TA @ A @ (bot_bot @ (set @ TA)))) & (C = (bot_bot @ (set @ TA)))) | ((B = (insert @ TA @ A @ (bot_bot @ (set @ TA)))) & (C = (insert @ TA @ A @ (bot_bot @ (set @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 53.05/29.09 thf(58,axiom,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder)).
% 53.05/29.09 thf(482,plain,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 53.05/29.09 thf(118,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_98_Collect__conv__if)).
% 53.05/29.09 thf(688,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)],[118])).
% 53.05/29.09 thf(27,axiom,((linorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Olinorder_22)).
% 53.05/29.09 thf(368,plain,((linorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 53.05/29.09 thf(211,axiom,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((binary1610619414edTree @ TA @ A @ (binary210054475elle_T @ TA @ B @ C @ D)) => (binary1610619414edTree @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_sortLemmaL)).
% 53.05/29.09 thf(961,plain,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA,D:(binary1291135688e_Tree @ TA)]: ((binary1610619414edTree @ TA @ (A) @ (binary210054475elle_T @ TA @ B @ C @ D)) => (binary1610619414edTree @ TA @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 53.05/29.09 thf(212,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((bot_bot @ TA) = (sup_sup @ TA @ A @ B)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_sup__bot_Oneutr__eq__iff)).
% 53.05/29.09 thf(963,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA,B:TA]: (((bot_bot @ TA) = (sup_sup @ TA @ A @ B)) = ((A = (bot_bot @ TA)) & (B = (bot_bot @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 53.05/29.09 thf(14,axiom,((ord @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oord_25)).
% 53.05/29.09 thf(319,plain,((ord @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 53.05/29.09 thf(204,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_not__le)).
% 53.05/29.09 thf(946,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 53.05/29.09 thf(33,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_bot__apply)).
% 53.05/29.09 thf(390,plain,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 53.05/29.09 thf(98,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_27_singleton__conv)).
% 53.05/29.09 thf(632,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)],[98])).
% 53.05/29.09 thf(35,axiom,((! [TA: $tType]: ((lattice @ TA) => ((sup_sup @ TA) = (^ [A:TA,B:TA]: (sup_sup @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_inf__sup__aci_I5_J)).
% 53.05/29.09 thf(401,plain,((! [TA: $tType]: ((lattice @ TA) => ((sup_sup @ TA) = (^ [A:TA,B:TA]: (sup_sup @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 53.05/29.09 thf(151,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (set @ TA) @ (minus_minus @ (set @ TA) @ A @ B) @ B) = (sup_sup @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_Un__Diff__cancel2)).
% 53.05/29.09 thf(786,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((sup_sup @ (set @ TA) @ (minus_minus @ (set @ TA) @ A @ B) @ B) = (sup_sup @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 53.05/29.09 thf(222,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_32_insert__Diff1)).
% 53.05/29.09 thf(995,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)],[222])).
% 53.05/29.09 thf(235,axiom,(((binary1653327646_setOf @ a @ (binary1830089824insert @ a @ h @ e @ t1)) = (sup_sup @ (set @ a) @ (minus_minus @ (set @ a) @ (binary1653327646_setOf @ a @ t1) @ (binary64540844le_eqs @ a @ h @ e)) @ (insert @ a @ e @ (bot_bot @ (set @ a)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_c1)).
% 53.05/29.09 thf(1030,plain,(((binary1653327646_setOf @ a @ (binary1830089824insert @ a @ (h) @ e @ t1)) = (sup_sup @ (set @ a) @ (minus_minus @ (set @ a) @ (binary1653327646_setOf @ a @ t1) @ (binary64540844le_eqs @ a @ (h) @ e)) @ (insert @ a @ e @ (bot_bot @ (set @ a)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 53.05/29.09 thf(111,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: (((minus_minus @ (set @ TA) @ A @ B) = (bot_bot @ (set @ TA))) = (ord_less_eq @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_Diff__eq__empty__iff)).
% 53.05/29.09 thf(667,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: (((minus_minus @ (set @ TA) @ A @ B) = (bot_bot @ (set @ TA))) = (ord_less_eq @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 53.05/29.09 thf(143,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_88_singleton__inject)).
% 53.05/29.09 thf(763,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)],[143])).
% 53.05/29.09 thf(168,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ~ (ord_less @ (set @ TA) @ A @ (bot_bot @ (set @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_not__psubset__empty)).
% 53.05/29.09 thf(832,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ~ (ord_less @ (set @ TA) @ A @ (bot_bot @ (set @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 53.05/29.09 thf(72,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((? [C:TA]: ((A @ C) & ! [D:TA]: ((A @ D) => (D = C)))) => ((A @ B) => ((the @ TA @ A) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_the1__equality)).
% 53.05/29.09 thf(536,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((? [C:TA]: ((A @ C) & ! [D:TA]: ((A @ D) => (D = C)))) => ((A @ B) => ((the @ TA @ (A)) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 53.05/29.09 thf(251,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => (? [C:TA]: (member @ TA @ C @ (minus_minus @ (set @ TA) @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_psubset__imp__ex__mem)).
% 53.05/29.09 thf(1077,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less @ (set @ TA) @ A @ B) => (? [C:TA]: (member @ TA @ C @ (minus_minus @ (set @ TA) @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 53.05/29.09 thf(57,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_order__less__subst2)).
% 53.05/29.09 thf(478,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 53.05/29.09 thf(265,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_68_insertE)).
% 53.05/29.09 thf(1116,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)],[265])).
% 53.05/29.09 thf(7,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TA) => (minus @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Groups_Ominus)).
% 53.05/29.09 thf(300,plain,((! [TA: $tType,TB: $tType]: ((minus @ TA) => (minus @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 53.05/29.09 thf(224,axiom,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA]: ((binary1610619414edTree @ TA @ A @ B) => ((binary827270440e_memb @ TA @ A @ C @ B) = (member @ TA @ C @ (binary1653327646_setOf @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_memb__spec)).
% 53.05/29.09 thf(999,plain,((! [TA: $tType]: (! [A:(TA > int),B:(binary1291135688e_Tree @ TA),C:TA]: ((binary1610619414edTree @ TA @ (A) @ B) => ((binary827270440e_memb @ TA @ (A) @ C @ B) = (member @ TA @ C @ (binary1653327646_setOf @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 53.05/29.09 thf(45,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A != B) = ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_neq__iff)).
% 53.05/29.09 thf(447,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) = ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 53.05/29.09 thf(214,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_leD)).
% 53.05/29.09 thf(967,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 53.05/29.09 thf(257,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_80_DiffD1)).
% 53.05/29.09 thf(1097,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)],[257])).
% 53.05/29.09 thf(163,axiom,((! [TA: $tType]: ((is_empty @ TA) = (^ [A:(set @ TA)]: (A = (bot_bot @ (set @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_Set_Ois__empty__def)).
% 53.05/29.09 thf(818,plain,((! [TA: $tType]: ((is_empty @ TA) = (^ [A:(set @ TA)]: (A = (bot_bot @ (set @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 53.05/29.09 thf(42,axiom,((! [TA: $tType,TB: $tType]: ((bounded_lattice @ TA) => (bounde1808546759up_bot @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Obounded__semilattice__sup__bot)).
% 53.05/29.09 thf(422,plain,((! [TA: $tType,TB: $tType]: ((bounded_lattice @ TA) => (bounde1808546759up_bot @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 53.05/29.09 thf(9,axiom,((! [TA: $tType,TB: $tType]: ((lattice @ TA) => (lattice @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Lattices_Olattice)).
% 53.05/29.09 thf(305,plain,((! [TA: $tType,TB: $tType]: ((lattice @ TA) => (lattice @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 53.05/29.09 thf(55,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ C) = (sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_sup_Oassoc)).
% 53.05/29.09 thf(474,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((sup_sup @ TA @ (sup_sup @ TA @ A @ B) @ C) = (sup_sup @ TA @ A @ (sup_sup @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 53.05/29.09 thf(110,axiom,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:TA,C:(binary1291135688e_Tree @ TA)]: ((binary2130109271t_Tree @ TA @ (binary210054475elle_T @ TA @ A @ B @ C)) = (sup_sup @ (set @ TA) @ (sup_sup @ (set @ TA) @ (binary2130109271t_Tree @ TA @ A) @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) @ (binary2130109271t_Tree @ TA @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_Tree_Osimps_I15_J)).
% 53.05/29.09 thf(664,plain,((! [TA: $tType]: (! [A:(binary1291135688e_Tree @ TA),B:TA,C:(binary1291135688e_Tree @ TA)]: ((binary2130109271t_Tree @ TA @ (binary210054475elle_T @ TA @ A @ B @ C)) = (sup_sup @ (set @ TA) @ (sup_sup @ (set @ TA) @ (binary2130109271t_Tree @ TA @ A) @ (insert @ TA @ B @ (bot_bot @ (set @ TA)))) @ (binary2130109271t_Tree @ TA @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 53.05/29.09 thf(283,axiom,((! [TA: $tType]: (! [A:TA,B:(binary1291135688e_Tree @ TA)]: ((member @ TA @ A @ (binary2130109271t_Tree @ TA @ B)) => ((! [C:(binary1291135688e_Tree @ TA)]: ((? [D:TA,E:(binary1291135688e_Tree @ TA)]: (B = (binary210054475elle_T @ TA @ C @ D @ E))) => (~ (member @ TA @ A @ (binary2130109271t_Tree @ TA @ C))))) => ((! [C:(binary1291135688e_Tree @ TA),D:(binary1291135688e_Tree @ TA)]: (B != (binary210054475elle_T @ TA @ C @ A @ D))) => (~ (! [C:(binary1291135688e_Tree @ TA),D:TA,E:(binary1291135688e_Tree @ TA)]: ((B = (binary210054475elle_T @ TA @ C @ D @ E)) => (~ (member @ TA @ A @ (binary2130109271t_Tree @ TA @ E)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_Tree_Oset__cases)).
% 53.05/29.09 thf(1165,plain,((! [TA: $tType]: (! [A:TA,B:(binary1291135688e_Tree @ TA)]: ((member @ TA @ A @ (binary2130109271t_Tree @ TA @ B)) => ((! [C:(binary1291135688e_Tree @ TA)]: ((? [D:TA,E:(binary1291135688e_Tree @ TA)]: (B = (binary210054475elle_T @ TA @ C @ D @ E))) => (~ (member @ TA @ A @ (binary2130109271t_Tree @ TA @ C))))) => ((! [C:(binary1291135688e_Tree @ TA),D:(binary1291135688e_Tree @ TA)]: ~ (B = (binary210054475elle_T @ TA @ C @ A @ D))) => (~ (! [C:(binary1291135688e_Tree @ TA),D:TA,E:(binary1291135688e_Tree @ TA)]: ((B = (binary210054475elle_T @ TA @ C @ D @ E)) => (~ (member @ TA @ A @ (binary2130109271t_Tree @ TA @ E)))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[283])).
% 53.05/29.09 thf(4,axiom,((linorder @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Olinorder)).
% 53.05/29.09 thf(294,plain,((linorder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 53.05/29.09 thf(157,axiom,((! [TA: $tType]: ((wellorder @ TA) => (((?) @ TA) = (^ [A:(TA > $o)]: ? [B:TA]: ((A @ B) & ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (A @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_exists__least__iff)).
% 53.05/29.09 thf(801,plain,((! [TA: $tType]: ((wellorder @ TA) => (((?) @ TA) = (^ [A:(TA > $o)]: ? [B:TA]: ((A @ B) & ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (A @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 53.05/29.09 thf(210,axiom,((no_top @ int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Ono__top)).
% 53.05/29.09 thf(960,plain,((no_top @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 53.05/29.09 thf(99,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_sup_Ostrict__coboundedI1)).
% 53.05/29.09 thf(635,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ A @ (sup_sup @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 53.05/29.09 thf(198,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ (bot_bot @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_sup__bot_Oright__neutral)).
% 53.05/29.09 thf(928,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ (bot_bot @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 53.05/29.09 thf(40,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_dual__order_Ostrict__implies__not__eq)).
% 53.05/29.09 thf(415,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 53.05/29.09 thf(131,axiom,((! [TA: $tType]: ((dense_order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (? [C:TA]: ((ord_less @ TA @ A @ C) & (ord_less @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_dense)).
% 53.05/29.09 thf(728,plain,((! [TA: $tType]: ((dense_order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (? [C:TA]: ((ord_less @ TA @ A @ C) & (ord_less @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 53.05/29.09 thf(221,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_157_is__singletonI_H)).
% 53.05/29.09 thf(987,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)],[221])).
% 53.05/29.09 thf(269,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_56_ex__in__conv)).
% 53.05/29.09 thf(1129,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)],[269])).
% 53.05/29.09 thf(191,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_106_Diff__insert)).
% 53.05/29.09 thf(908,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)],[191])).
% 53.05/29.09 thf(165,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (sup_sup @ TA @ A @ B) @ C) => (~ ((ord_less @ TA @ A @ C) => (~ (ord_less @ TA @ B @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_sup_Ostrict__boundedE)).
% 53.05/29.09 thf(822,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (sup_sup @ TA @ A @ B) @ C) => (~ ((ord_less @ TA @ A @ C) => (~ (ord_less @ TA @ B @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 53.05/29.09 thf(28,axiom,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_sup_Oidem)).
% 53.05/29.09 thf(369,plain,((! [TA: $tType]: ((semilattice_sup @ TA) => (! [A:TA]: ((sup_sup @ TA @ A @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 53.05/29.09 thf(19,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => ((! [C:TA]: ((A @ C) => (C = B))) => (A @ (the @ TA @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_theI)).
% 53.05/29.09 thf(337,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA]: ((A @ B) => ((! [C:TA]: ((A @ C) => (C = B))) => (A @ (the @ TA @ (A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 53.05/29.09 thf(201,axiom,((! [TA: $tType]: (! [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA)]: (binary231205461t_pred @ TA @ A @ B @ C @ D)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_sorted__distinct)).
% 53.05/29.09 thf(935,plain,((! [TA: $tType]: (! [A:(TA > int),B:TA,C:TA,D:(binary1291135688e_Tree @ TA)]: (binary231205461t_pred @ TA @ (A) @ B @ C @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 53.05/29.09 thf(287,axiom,((! [TA: $tType]: (! [A:TA,B:(binary1291135688e_Tree @ TA),C:(binary1291135688e_Tree @ TA)]: (member @ TA @ A @ (binary2130109271t_Tree @ TA @ (binary210054475elle_T @ TA @ B @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_Tree_Oset__intros_I2_J)).
% 53.05/29.09 thf(1184,plain,((! [TA: $tType]: (! [A:TA,B:(binary1291135688e_Tree @ TA),C:(binary1291135688e_Tree @ TA)]: (member @ TA @ A @ (binary2130109271t_Tree @ TA @ (binary210054475elle_T @ TA @ B @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[287])).
% 53.05/29.09 thf(238,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_81_DiffE)).
% 53.05/29.09 thf(1037,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)],[238])).
% 53.05/29.09 thf(114,axiom,((order_bot @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder__bot_20)).
% 53.05/29.09 thf(676,plain,((order_bot @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 53.05/29.09 thf(255,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_43_insertCI)).
% 53.05/29.09 thf(1088,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)],[255])).
% 53.05/29.09 thf(84,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: (((sup_sup @ (set @ TA) @ A @ B) = (bot_bot @ (set @ TA))) = ((A = (bot_bot @ (set @ TA))) & (B = (bot_bot @ (set @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_Un__empty)).
% 53.05/29.09 thf(592,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: (((sup_sup @ (set @ TA) @ A @ B) = (bot_bot @ (set @ TA))) = ((A = (bot_bot @ (set @ TA))) & (B = (bot_bot @ (set @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 53.05/29.09 thf(24,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_order_Oasym)).
% 53.05/29.09 thf(364,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 53.05/29.09 thf(229,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_103_Diff__insert__absorb)).
% 53.05/29.09 thf(1014,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)],[229])).
% 53.05/29.09 thf(53,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_dual__order_Ostrict__trans)).
% 53.05/29.09 thf(469,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 53.05/29.09 thf(203,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_97_Collect__conv__if2)).
% 53.05/29.09 thf(940,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)],[203])).
% 53.05/29.09 thf(11,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_less__imp__neq)).
% 53.05/29.09 thf(309,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 53.05/29.09 thf(108,axiom,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ (bot_bot @ TA) @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_sup__bot_Oleft__neutral)).
% 53.05/29.09 thf(659,plain,((! [TA: $tType]: ((bounde1808546759up_bot @ TA) => (! [A:TA]: ((sup_sup @ TA @ (bot_bot @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 53.05/29.09 thf(1186,plain,(($false)),inference(e,[status(thm)],[809,1024,760,846,352,582,1005,1068,741,873,1142,878,408,977,614,677,1041,861,1137,533,500,715,698,913,1063,670,898,288,320,651,829,404,372,934,1132,949,1055,724,559,969,881,316,789,1109,646,834,806,966,821,1151,937,1020,348,866,1119,998,428,527,981,766,293,956,1104,849,307,1074,452,529,925,366,1153,761,1047,798,746,302,598,561,297,424,630,815,916,484,1032,361,625,852,493,757,682,551,710,974,1106,329,1178,1159,461,1079,1027,1017,1111,725,869,783,471,884,554,901,637,679,837,393,1099,701,911,721,1002,779,503,1060,1050,792,1071,773,662,718,906,618,1146,601,1135,412,375,733,904,694,732,843,772,826,1124,545,313,611,498,704,350,919,804,406,736,649,1122,1175,979,604,1011,419,477,387,323,1162,621,1029,1149,769,858,367,521,959,1044,1066,455,608,1113,1102,653,922,1034,490,589,795,548,487,812,1081,617,1145,754,458,1181,776,525,640,295,1156,707,971,327,954,739,712,557,580,855,1053,673,791,585,840,463,1085,951,643,744,1141,656,864,1008,595,1094,386,497,876,465,627,450,931,482,688,368,961,963,319,946,390,632,401,786,995,1030,667,763,832,536,1077,478,1116,300,999,447,967,1097,818,422,305,474,664,1165,294,801,960,635,928,415,728,987,1129,908,822,369,337,935,1184,1037,676,1088,592,364,1014,469,940,309,659])).
% 53.05/29.09 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 53.05/29.09 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------