%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP127^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 : n009.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:52 AM UTC 2026
% Result : Theorem 48.65s 29.06s
% Output : Refutation 49.54s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP127^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08 % 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 : n009.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:57:30 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.88/0.77 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.43/1.20 % [INFO] Parsing done (423ms).
% 2.43/1.21 % [INFO] Running in sequential loop mode.
% 3.53/1.60 % [INFO] eprover registered as external prover.
% 3.53/1.61 % [INFO] Scanning for conjecture ...
% 3.71/1.76 % [INFO] Found a conjecture (or negated_conjecture) and 278 axioms. Running axiom selection ...
% 3.91/1.89 % [INFO] Axiom selection finished. Selected 270 axioms (removed 8 axioms).
% 5.00/2.16 % [INFO] Problem is higher-order (TPTP THF).
% 5.00/2.19 % [INFO] Type checking passed.
% 5.00/2.20 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 48.65/29.05 % External prover 'e' found a proof!
% 48.65/29.05 % [INFO] Killing All external provers ...
% 48.65/29.05 % Time passed: 28708ms (effective reasoning time: 27831ms)
% 48.65/29.05 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 48.65/29.06 % Axioms used in derivation (270): tcon_fun___Orderings_Obot, tcon_Countable__Set__Type_Ocset___Orderings_Obot_11, fact_134_set__cinsert, fact_174_less__imp__neq, fact_55_cDiff__idemp, fact_203_leI, tcon_fun___Groups_Ominus, fact_175_less__asym, fact_123_le__fun__def, fact_137_cinsertE, fact_132_cinsert__absorb, fact_191_order_Ostrict__trans, fact_105_if__split__cin1, fact_173_dense, fact_197_order_Ostrict__implies__not__eq, fact_209_order__less__le__subst2, fact_115_eq__iff, fact_189_linorder__cases, fact_16_altc__nondet__def, fact_142_cDiffD1, fact_151_csingleton__iff, fact_50_monad__altc_Oaxioms_I2_J, fact_56_cDiff__cancel, fact_95_order__class_Oorder_Oeq__iff, fact_70_all__not__cin__conv, fact_103_eq__refl, fact_32_nondetT_Osel, fact_130_cemptyE, tcon_HOL_Obool___Orderings_Oord_4, fact_240_diff__eq__diff__less, fact_3_bot__apply, fact_155_cpsubset__finsert__iff, fact_205_less__le, fact_66_fun__diff__def, fact_74_csubsetI, fact_131_mk__disjoint__cinsert, fact_255_minf_I6_J, fact_35_nondetT_Osplit__sel__asm, fact_227_order_Ostrict__iff__order, fact_102_eqcset__imp__iff, fact_180_ord__eq__less__trans, fact_109_csubset__refl, fact_65_diff__eq__diff__eq, tcon_HOL_Obool___Groups_Ominus_6, tcon_HOL_Obool___Orderings_Oorder__bot_1, fact_239_diff__strict__mono, fact_214_antisym__conv2, fact_72_cinsert__iff, fact_250_csubset__not__fsubset__eq, fact_152_cinsert__cDiff__if, tcon_fun___Orderings_Oord, fact_36_nondetT_Osplit__sel, fact_125_le__funE, fact_153_csubset__csingletonD, fact_114_cequalityE, fact_163_ord__eq__less__subst, fact_69_csubset__antisym, fact_170_neq__iff, fact_124_le__funI, tcon_HOL_Obool___Orderings_Olinorder, fact_177_less__trans, fact_67_cinsert__cDiff, fact_14_nondetT_Oexpand, fact_128_equals__cemptyD, fact_83_diff__left__mono, fact_111_cequalityD1, fact_8_cset__nondetM_Omerge__single, fact_206_order__le__less__subst1, fact_6_cinsert__not__cempty, fact_58_cempty__cDiff, fact_112_cequalityCE, fact_138_bot_Oextremum__uniqueI, fact_33_put__nondet__def, fact_181_ord__less__eq__trans, fact_87_dual__order_Oeq__iff, fact_158_Greatest__equality, fact_38_rewriteL__comp__comp2, fact_78_cDiffI, fact_75_cempty__fsubsetI, fact_121_order__subst2, fact_182_dual__order_Oasym, fact_241_diff__strict__left__mono, fact_171_order_Oasym, fact_253_cpsubset__imp__ex__fmem, fact_190_dual__order_Oirrefl, fact_64_cancel__ab__semigroup__add__class_Odiff__right__commute, fact_26_comp__apply__eq, fact_101_le__cases, fact_23_comp__eq__elim, fact_71_cempty__iff, fact_86_dual__order_Oantisym, fact_92_order__class_Oorder_Oantisym, fact_207_order__le__less__subst2, fact_247_cpsubset__imp__fsubset, fact_88_dual__order_Otrans, fact_99_cset__eq__csubset, fact_42_run__put__nondet, fact_126_le__funD, fact_204_le__less, tcon_Countable__Set__Type_Ocset___Orderings_Oord_10, fact_216_le__less__trans, help_If_1_1_T, fact_243_cpsubsetD, fact_21_comp__assoc, fact_225_order_Ostrict__trans2, fact_127_equals__cemptyI, fact_28_nondetT_Ocollapse, fact_25_comp__eq__dest__lhs, fact_2_cinsert__absorb2, fact_141_cDiffD2, fact_244_not__cpsubset__cempty, fact_94_ord__eq__le__trans, fact_118_cin__mono, fact_165_order__less__subst1, fact_249_csubset__cpsubset__trans, fact_242_diff__strict__right__mono, fact_217_less__le__trans, fact_104_if__split__cin2, fact_192_less__imp__not__less, fact_161_le__rel__bool__arg__iff, fact_234_dual__order_Ostrict__iff__order, fact_49_function__factors__right, fact_169_neqE, fact_146_cinsert__mono, fact_0_mergec__single, fact_18_cset__nondetM__base_Oaltc__nondet__def, fact_19_cset__nondetM_Oaxioms_I3_J, fact_238_bot_Onot__eq__extremum, fact_160_verit__la__disequality, tcon_Countable__Set__Type_Ocset___Orderings_Opreorder_8, fact_139_bot_Oextremum__unique, fact_168_gt__ex, fact_251_csubset__iff__pfsubset__eq, fact_254_minf_I8_J, fact_196_not__less__iff__gr__or__eq, fact_122_order__subst1, fact_186_antisym__conv3, fact_60_cDiff__cinsert2, fact_82_diff__right__mono, fact_222_less__le__not__le, fact_48_function__factors__left, fact_149_cminus__mono, fact_62_cDiff__single__cinsert, fact_215_less__imp__le, fact_185_less__induct, fact_212_le__neq__trans, fact_39_rewriteR__comp__comp, fact_120_ord__eq__le__subst, fact_184_less__not__sym, fact_46_nondetM__base_Orun__put__nondet, fact_57_cDiff__cempty, fact_228_dual__order_Ostrict__trans1, fact_150_csubset__cinsert__iff, fact_54_monad__state__altc_Oaxioms_I2_J, fact_148_double__cDiff, fact_219_dense__le, fact_113_antisym, fact_220_le__less__linear, fact_167_lt__ex, fact_97_le__cases3, fact_236_order_Onot__eq__order__implies__strict, help_If_3_1_T, fact_237_bot_Oextremum__strict, tcon_fun___Orderings_Oorder__bot, fact_129_ex__cin__conv, fact_80_cinsert__cDiff1, fact_176_less__asym_H, fact_47_fun_Omap__comp, help_If_2_1_T, fact_89_linorder__wlog, fact_117_cset__eqI, fact_41_type__copy__map__cong0, fact_202_leD, fact_12_run__altc__nondet, fact_24_comp__cong, fact_31_nondetT_Oexhaust__sel, fact_231_dense__le__bounded, fact_30_nondetT_Oinduct, tcon_HOL_Obool___Orderings_Obot_5, fact_96_antisym__conv, fact_5_csingleton__inject, fact_221_le__imp__less__or__eq, fact_79_cinsert__csubset, fact_213_antisym__conv1, fact_147_cDiff__csubset, fact_27_nondetT_Oinject, fact_145_csubset__cinsertI, tcon_HOL_Obool___Orderings_Opreorder_2, fact_119_ord__le__eq__subst, fact_81_diff__eq__diff__less__eq, fact_11_monad__altc_Oaltc__single, tcon_HOL_Obool___Orderings_Oorder_3, tcon_fun___Orderings_Opreorder, fact_90_dual__order_Orefl, fact_15_cset__nondetM__base_Orun__altc__nondet, tcon_Countable__Set__Type_Ocset___Orderings_Oorder_9, fact_10_bot__fun__def, fact_100_order_Otrans, fact_154_cDiff__cinsert__absorb, fact_178_less__linear, fact_135_cinsertI2, fact_218_dense__ge, fact_208_order__less__le__subst1, fact_108_linear, fact_162_verit__comp__simplify1_I3_J, fact_159_GreatestI2__order, fact_29_nondetT_Oexhaust, fact_230_dense__ge__bounded, fact_110_cequalityD2, fact_85_csubset__cinsert, fact_59_cDiff__cinsert, fact_195_dual__order_Ostrict__trans, fact_133_cinsert__ident, fact_143_cDiffE, fact_164_ord__less__eq__subst, fact_226_order_Oorder__iff__strict, fact_198_dual__order_Ostrict__implies__not__eq, fact_233_dual__order_Oorder__iff__strict, fact_43_nondetT_Ocase__eq__if, fact_116_csubsetD, fact_248_cpsubset__csubset__trans, fact_53_nondetT_Orec, fact_1_cset__nondetM__base_Oaltc__nondet_Ocong, tcon_fun___Orderings_Oorder, fact_232_order_Ostrict__implies__order, fact_40_rewriteL__comp__comp, fact_84_diff__mono, fact_179_less__irrefl, fact_246_less__cset__def, fact_188_less__imp__triv, fact_91_order__trans, fact_172_cpsubset__trans, fact_37_rewriteR__comp__comp2, fact_210_not__le, fact_68_order__refl, fact_73_cinsertCI, fact_106_eq__cmem__trans, fact_183_less__imp__not__eq, fact_44_nondetT_Ocase, fact_166_order__less__subst2, fact_193_exists__least__iff, fact_4_cdoubleton__eq__iff, fact_17_comp__apply, fact_194_linorder__less__wlog, fact_9_cset__nondetM_Omergec__single, fact_61_minus__apply, fact_76_csubset__cempty, fact_211_not__less, fact_52_monad__altc3_Oaxioms_I1_J, fact_144_csubset__cinsertI2, tcon_Countable__Set__Type_Ocset___Orderings_Oorder__bot_7, fact_98_eqcelem__imp__iff, fact_224_order_Ostrict__trans1, fact_77_cDiff__iff, fact_140_bot_Oextremum, fact_235_dual__order_Ostrict__implies__order, fact_107_csubset__trans, fact_245_cpsubset__eq, fact_136_cinsertI1, fact_187_less__imp__not__eq2, fact_34_nondetM__base_Oput__nondet__def, fact_13_cset__nondetM_Omerge__empty, tcon_Countable__Set__Type_Ocset___Groups_Ominus_12, fact_22_comp__eq__dest, fact_223_not__le__imp__less, fact_93_ord__le__eq__trans, fact_229_dual__order_Ostrict__trans2, fact_51_cinsert__cDiff__single, fact_20_comp__def, fact_7_cinsert__commute
% 48.65/29.06 % No. of inferences in proof: 544
% 48.65/29.06 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 28708 ms resp. 27831 ms w/o parsing
% 49.54/29.20 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 49.54/29.20 thf(m_type, type, m: $tType).
% 49.54/29.20 thf(c_type, type, c: $tType).
% 49.54/29.20 thf(a_type, type, a: $tType).
% 49.54/29.20 thf(minus_decl, type, minus: !> [TA: $tType]: $o).
% 49.54/29.20 thf(bot_decl, type, bot: !> [TA: $tType]: $o).
% 49.54/29.20 thf(ord_decl, type, ord: !> [TA: $tType]: $o).
% 49.54/29.20 thf(order_decl, type, order: !> [TA: $tType]: $o).
% 49.54/29.20 thf(group_add_decl, type, group_add: !> [TA: $tType]: $o).
% 49.54/29.20 thf(no_bot_decl, type, no_bot: !> [TA: $tType]: $o).
% 49.54/29.20 thf(no_top_decl, type, no_top: !> [TA: $tType]: $o).
% 49.54/29.20 thf(linorder_decl, type, linorder: !> [TA: $tType]: $o).
% 49.54/29.20 thf(preorder_decl, type, preorder: !> [TA: $tType]: $o).
% 49.54/29.20 thf(order_bot_decl, type, order_bot: !> [TA: $tType]: $o).
% 49.54/29.20 thf(wellorder_decl, type, wellorder: !> [TA: $tType]: $o).
% 49.54/29.20 thf(dense_order_decl, type, dense_order: !> [TA: $tType]: $o).
% 49.54/29.20 thf(dense_linorder_decl, type, dense_linorder: !> [TA: $tType]: $o).
% 49.54/29.20 thf(ordered_ab_group_add_decl, type, ordered_ab_group_add: !> [TA: $tType]: $o).
% 49.54/29.20 thf(cancel146912293up_add_decl, type, cancel146912293up_add: !> [TA: $tType]: $o).
% 49.54/29.20 thf(countable_Set_cin_decl, type, countable_Set_cin: !> [TA: $tType]: (TA > ((countable_Set_cset @ TA) > $o))).
% 49.54/29.20 thf(counta2111716221insert_decl, type, counta2111716221insert: !> [TA: $tType]: (TA > ((countable_Set_cset @ TA) > (countable_Set_cset @ TA)))).
% 49.54/29.20 thf(comp_decl, type, comp: !> [TA: $tType,TB: $tType,TC: $tType]: ((TC > TB) > ((TA > TC) > (TA > TB)))).
% 49.54/29.20 thf(minus_minus_decl, type, minus_minus: !> [TA: $tType]: (TA > (TA > TA))).
% 49.54/29.20 thf(if_decl, type, if: !> [TA: $tType]: ($o > (TA > (TA > TA)))).
% 49.54/29.20 thf(monomo2011693592ondetM_decl, type, monomo2011693592ondetM: !> [TA: $tType,TB: $tType,TC: $tType]: (((countable_Set_cset @ TC) > TB) > ((TB > (((countable_Set_cset @ TC) > TB) > TB)) > (((countable_Set_cset @ TC) > ((TC > TB) > TB)) > (((countable_Set_cset @ TA) > ((TA > TB) > TB)) > $o))))).
% 49.54/29.20 thf(monomo759963067axioms_decl, type, monomo759963067axioms: !> [TA: $tType,TB: $tType,TC: $tType]: (((countable_Set_cset @ TC) > TB) > ((TB > (((countable_Set_cset @ TC) > TB) > TB)) > (((countable_Set_cset @ TC) > ((TC > TB) > TB)) > (((countable_Set_cset @ TA) > ((TA > TB) > TB)) > $o))))).
% 49.54/29.20 thf(monomo955616121nondet_decl, type, monomo955616121nondet: !> [TA: $tType,TB: $tType,TC: $tType]: (((countable_Set_cset @ TC) > ((TC > TB) > TB)) > ((countable_Set_cset @ TC) > ((TC > (monomo1453983439ondetT @ TA @ TB)) > (monomo1453983439ondetT @ TA @ TB))))).
% 49.54/29.20 thf(monomo439771545d_altc_decl, type, monomo439771545d_altc: !> [TA: $tType,TB: $tType,TC: $tType]: ((TC > TB) > ((TB > ((TC > TB) > TB)) > (((countable_Set_cset @ TA) > ((TA > TB) > TB)) > $o)))).
% 49.54/29.20 thf(monomo1425736922_altc3_decl, type, monomo1425736922_altc3: !> [TA: $tType,TB: $tType,TC: $tType]: ((TC > TB) > ((TB > ((TC > TB) > TB)) > (((countable_Set_cset @ TA) > ((TA > TB) > TB)) > $o)))).
% 49.54/29.20 thf(monomo555039548axioms_decl, type, monomo555039548axioms: !> [TA: $tType,TB: $tType,TC: $tType]: ((TC > ((TB > TC) > TC)) > (((countable_Set_cset @ TA) > ((TA > TC) > TC)) > $o))).
% 49.54/29.20 thf(monomo1036387116e_altc_decl, type, monomo1036387116e_altc: !> [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: ((TD > TC) > ((TC > ((TD > TC) > TC)) > (((TB > TC) > TC) > ((TB > (TC > TC)) > (((countable_Set_cset @ TA) > ((TA > TC) > TC)) > $o)))))).
% 49.54/29.20 thf(monomo410456285nondet_decl, type, monomo410456285nondet: !> [TA: $tType,TB: $tType,TC: $tType]: ((TC > (TB > TB)) > (TC > ((monomo1453983439ondetT @ TA @ TB) > (monomo1453983439ondetT @ TA @ TB))))).
% 49.54/29.20 thf(monomo1975189248ondetT_decl, type, monomo1975189248ondetT: !> [TA: $tType,TB: $tType]: (TB > (monomo1453983439ondetT @ TA @ TB))).
% 49.54/29.20 thf(monomo1564381680ondetT_decl, type, monomo1564381680ondetT: !> [TA: $tType,TB: $tType,TC: $tType]: ((TC > TB) > ((monomo1453983439ondetT @ TA @ TC) > TB))).
% 49.54/29.20 thf(monomo1291740684ondetT_decl, type, monomo1291740684ondetT: !> [TA: $tType,TB: $tType,TC: $tType]: ((TC > TB) > ((monomo1453983439ondetT @ TA @ TC) > TB))).
% 49.54/29.20 thf(monomo603716163nondet_decl, type, monomo603716163nondet: !> [TA: $tType,TB: $tType]: ((monomo1453983439ondetT @ TB @ TA) > TA)).
% 49.54/29.20 thf(bot_bot_decl, type, bot_bot: !> [TA: $tType]: TA).
% 49.54/29.20 thf(ord_less_decl, type, ord_less: !> [TA: $tType]: (TA > (TA > $o))).
% 49.54/29.20 thf(ord_less_eq_decl, type, ord_less_eq: !> [TA: $tType]: (TA > (TA > $o))).
% 49.54/29.20 thf(order_Greatest_decl, type, order_Greatest: !> [TA: $tType]: ((TA > $o) > TA)).
% 49.54/29.20 thf(f_decl, type, f: (c > (monomo1453983439ondetT @ a @ m))).
% 49.54/29.20 thf(mergec_decl, type, mergec: ((countable_Set_cset @ c) > ((c > m) > m))).
% 49.54/29.20 thf(x_decl, type, x: c).
% 49.54/29.20 thf(113,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => ((! [D:TA]: ((A @ D) => (ord_less_eq @ TA @ D @ B))) => ((! [D:TA]: ((A @ D) => ((! [E:TA]: ((A @ E) => (ord_less_eq @ TA @ E @ D))) => (C @ D)))) => (C @ (order_Greatest @ TA @ A))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_GreatestI2__order)).
% 49.54/29.20 thf(629,plain,((! [TA: $tType]: ((order @ TA) => (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((A @ B) => ((! [D:TA]: ((A @ D) => (ord_less_eq @ TA @ D @ B))) => ((! [D:TA]: ((A @ D) => ((! [E:TA]: ((A @ E) => (ord_less_eq @ TA @ E @ D))) => (C @ D)))) => (C @ (order_Greatest @ TA @ (A)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 49.54/29.20 thf(241,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:((countable_Set_cset @ TA) > TB),B:(TB > (((countable_Set_cset @ TA) > TB) > TB)),C:((countable_Set_cset @ TA) > ((TA > TB) > TB)),D:((countable_Set_cset @ TC) > ((TC > TB) > TB)),E:TA,F:(TA > TB)]: ((monomo2011693592ondetM @ TA @ TB @ TC @ A @ B @ C @ D) => ((C @ (counta2111716221insert @ TA @ E @ (bot_bot @ (countable_Set_cset @ TA))) @ F) = (F @ E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_cset__nondetM_Omerge__single)).
% 49.54/29.20 thf(1024,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:((countable_Set_cset @ TA) > TB),B:(TB > (((countable_Set_cset @ TA) > TB) > TB)),C:((countable_Set_cset @ TA) > ((TA > TB) > TB)),D:((countable_Set_cset @ TC) > ((TC > TB) > TB)),E:TA,F:(TA > TB)]: ((monomo2011693592ondetM @ TA @ TB @ TC @ (A) @ (B) @ (C) @ (D)) => ((C @ (counta2111716221insert @ TA @ E @ (bot_bot @ (countable_Set_cset @ TA))) @ (F)) = (F @ E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 49.54/29.20 thf(26,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_dual__order_Oantisym)).
% 49.54/29.20 thf(365,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 49.54/29.20 thf(243,axiom,((! [TA: $tType]: ((ord_less @ (countable_Set_cset @ TA)) = (^ [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) & ~ (ord_less_eq @ (countable_Set_cset @ TA) @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_csubset__not__fsubset__eq)).
% 49.54/29.20 thf(1031,plain,((! [TA: $tType]: ((ord_less @ (countable_Set_cset @ TA)) = (^ [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) & ~ (ord_less_eq @ (countable_Set_cset @ TA) @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 49.54/29.20 thf(211,axiom,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ A @ (bot_bot @ TA)) = (A = (bot_bot @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_bot_Oextremum__unique)).
% 49.54/29.20 thf(941,plain,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ A @ (bot_bot @ TA)) = (A = (bot_bot @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 49.54/29.20 thf(121,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_dual__order_Ostrict__implies__not__eq)).
% 49.54/29.20 thf(666,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 49.54/29.20 thf(271,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ C)) = ((countable_Set_cin @ TA @ A @ B) & ~ (countable_Set_cin @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_cDiff__iff)).
% 49.54/29.20 thf(1110,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ C)) = ((countable_Set_cin @ TA @ A @ B) & ~ (countable_Set_cin @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 49.54/29.20 thf(218,axiom,((! [TA: $tType]: ((ord_less_eq @ (countable_Set_cset @ TA)) = (^ [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less @ (countable_Set_cset @ TA) @ A @ B) | (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_csubset__iff__pfsubset__eq)).
% 49.54/29.20 thf(962,plain,((! [TA: $tType]: ((ord_less_eq @ (countable_Set_cset @ TA)) = (^ [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less @ (countable_Set_cset @ TA) @ A @ B) | (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 49.54/29.20 thf(57,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_less__imp__le)).
% 49.54/29.20 thf(468,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 49.54/29.20 thf(224,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: (ord_less_eq @ (countable_Set_cset @ TA) @ (bot_bot @ (countable_Set_cset @ TA)) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_cempty__fsubsetI)).
% 49.54/29.20 thf(977,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: (ord_less_eq @ (countable_Set_cset @ TA) @ (bot_bot @ (countable_Set_cset @ TA)) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 49.54/29.20 thf(125,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_203_leI)).
% 49.54/29.20 thf(683,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)],[125])).
% 49.54/29.20 thf(4,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_194_linorder__less__wlog)).
% 49.54/29.20 thf(276,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)],[4])).
% 49.54/29.20 thf(254,axiom,((! [A:(countable_Set_cset @ c),B:(c > (monomo1453983439ondetT @ a @ m))]: ((monomo603716163nondet @ a @ m @ (monomo955616121nondet @ c @ m @ a @ mergec @ A @ B)) = (mergec @ A @ (comp @ (monomo1453983439ondetT @ a @ m) @ m @ c @ (monomo603716163nondet @ a @ m) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_run__altc__nondet)).
% 49.54/29.20 thf(1068,plain,((! [A:(countable_Set_cset @ c),B:(c > (monomo1453983439ondetT @ a @ m))]: ((monomo603716163nondet @ a @ m @ (monomo955616121nondet @ c @ m @ a @ (mergec) @ A @ (B))) = (mergec @ A @ (comp @ (monomo1453983439ondetT @ a @ m) @ m @ c @ (monomo603716163nondet @ a @ m) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 49.54/29.20 thf(230,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((counta2111716221insert @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ (counta2111716221insert @ TA @ A @ (bot_bot @ (countable_Set_cset @ TA))))) = (counta2111716221insert @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_cinsert__cDiff__single)).
% 49.54/29.20 thf(994,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((counta2111716221insert @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ (counta2111716221insert @ TA @ A @ (bot_bot @ (countable_Set_cset @ TA))))) = (counta2111716221insert @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 49.54/29.20 thf(143,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_185_less__induct)).
% 49.54/29.20 thf(741,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)],[143])).
% 49.54/29.20 thf(32,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((A = B) => (((countable_Set_cin @ TA @ C @ A) => (~ (countable_Set_cin @ TA @ C @ B))) => (~ ((~ (countable_Set_cin @ TA @ C @ A)) => (countable_Set_cin @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_cequalityCE)).
% 49.54/29.20 thf(379,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((A = B) => (((countable_Set_cin @ TA @ C @ A) => (~ (countable_Set_cin @ TA @ C @ B))) => (~ ((~ (countable_Set_cin @ TA @ C @ A)) => (countable_Set_cin @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 49.54/29.20 thf(190,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less_eq @ (countable_Set_cset @ TA) @ B @ C) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_csubset__trans)).
% 49.54/29.20 thf(878,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less_eq @ (countable_Set_cset @ TA) @ B @ C) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 49.54/29.20 thf(100,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_dual__order_Ostrict__trans1)).
% 49.54/29.20 thf(597,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 49.54/29.20 thf(184,axiom,((! [TA: $tType]: ((ord_less @ (countable_Set_cset @ TA)) = (^ [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) & (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_cpsubset__eq)).
% 49.54/29.20 thf(861,plain,((! [TA: $tType]: ((ord_less @ (countable_Set_cset @ TA)) = (^ [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) & ~ (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 49.54/29.20 thf(188,axiom,((! [TA: $tType]: (bot @ (countable_Set_cset @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Countable__Set__Type_Ocset___Orderings_Obot_11)).
% 49.54/29.20 thf(873,plain,((! [TA: $tType]: (bot @ (countable_Set_cset @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 49.54/29.20 thf(51,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_dual__order_Ostrict__trans2)).
% 49.54/29.20 thf(449,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 49.54/29.20 thf(258,axiom,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ (bot_bot @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_bot_Oextremum__strict)).
% 49.54/29.20 thf(1078,plain,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ (bot_bot @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 49.54/29.20 thf(85,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_207_order__le__less__subst2)).
% 49.54/29.20 thf(550,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)],[85])).
% 49.54/29.20 thf(161,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_180_ord__eq__less__trans)).
% 49.54/29.20 thf(797,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)],[161])).
% 49.54/29.20 thf(59,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA]: ((monomo603716163nondet @ TB @ TA @ (monomo1975189248ondetT @ TA @ TB @ A)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_nondetT_Osel)).
% 49.54/29.20 thf(472,plain,((! [TA: $tType,TB: $tType]: (! [A:TA]: ((monomo603716163nondet @ TB @ TA @ (monomo1975189248ondetT @ TA @ TB @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 49.54/29.20 thf(167,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_le__less__trans)).
% 49.54/29.20 thf(814,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 49.54/29.20 thf(144,axiom,((ord @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oord_4)).
% 49.54/29.20 thf(747,plain,((ord @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 49.54/29.20 thf(122,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_163_ord__eq__less__subst)).
% 49.54/29.20 thf(670,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)],[122])).
% 49.54/29.20 thf(36,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (B != A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_dual__order_Ostrict__iff__order)).
% 49.54/29.20 thf(404,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 49.54/29.20 thf(177,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA,C:(countable_Set_cset @ TA)]: ((ord_less @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ C)) = (((countable_Set_cin @ TA @ B @ C) => (ord_less @ (countable_Set_cset @ TA) @ A @ C)) & ((~ (countable_Set_cin @ TA @ B @ C)) => (((countable_Set_cin @ TA @ B @ A) => (ord_less @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) @ C)) & ((~ (countable_Set_cin @ TA @ B @ A)) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_cpsubset__finsert__iff)).
% 49.54/29.20 thf(841,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA,C:(countable_Set_cset @ TA)]: ((ord_less @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ C)) = (((countable_Set_cin @ TA @ B @ C) => (ord_less @ (countable_Set_cset @ TA) @ A @ C)) & ((~ (countable_Set_cin @ TA @ B @ C)) => (((countable_Set_cin @ TA @ B @ A) => (ord_less @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) @ C)) & ((~ (countable_Set_cin @ TA @ B @ A)) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 49.54/29.20 thf(8,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA,C:TA]: (((ord_less_eq @ TA @ A @ B) => (~ (ord_less_eq @ TA @ B @ C))) => (((ord_less_eq @ TA @ B @ A) => (~ (ord_less_eq @ TA @ A @ C))) => (((ord_less_eq @ TA @ A @ C) => (~ (ord_less_eq @ TA @ C @ B))) => (((ord_less_eq @ TA @ C @ B) => (~ (ord_less_eq @ TA @ B @ A))) => (((ord_less_eq @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))) => (~ ((ord_less_eq @ TA @ C @ A) => (~ (ord_less_eq @ TA @ A @ B))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_le__cases3)).
% 49.54/29.20 thf(301,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA,C:TA]: (((ord_less_eq @ TA @ A @ B) => (~ (ord_less_eq @ TA @ B @ C))) => (((ord_less_eq @ TA @ B @ A) => (~ (ord_less_eq @ TA @ A @ C))) => (((ord_less_eq @ TA @ A @ C) => (~ (ord_less_eq @ TA @ C @ B))) => (((ord_less_eq @ TA @ C @ B) => (~ (ord_less_eq @ TA @ B @ A))) => (((ord_less_eq @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))) => (~ ((ord_less_eq @ TA @ C @ A) => (~ (ord_less_eq @ TA @ A @ B))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 49.54/29.20 thf(90,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TC),B:(TB > TD),C:(TB > TC),D:(TA > TB)]: (((comp @ TD @ TC @ TB @ A @ B) = C) => ((comp @ TD @ TC @ TA @ A @ (comp @ TB @ TD @ TA @ B @ D)) = (comp @ TB @ TC @ TA @ C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_rewriteL__comp__comp)).
% 49.54/29.20 thf(565,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TC),B:(TB > TD),C:(TB > TC),D:(TA > TB)]: (((comp @ TD @ TC @ TB @ A @ B) = (C)) => ((comp @ TD @ TC @ TA @ A @ (comp @ TB @ TD @ TA @ B @ D)) = (comp @ TB @ TC @ TA @ C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 49.54/29.20 thf(48,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_order__class_Oorder_Oantisym)).
% 49.54/29.20 thf(436,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 49.54/29.20 thf(116,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_171_order_Oasym)).
% 49.54/29.20 thf(651,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)],[116])).
% 49.54/29.20 thf(137,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(countable_Set_cset @ TA)]: ((A = B) => ((countable_Set_cin @ TA @ A @ C) = (countable_Set_cin @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_eqcelem__imp__iff)).
% 49.54/29.20 thf(719,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(countable_Set_cset @ TA)]: ((A = B) => ((countable_Set_cin @ TA @ A @ C) = (countable_Set_cin @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 49.54/29.20 thf(157,axiom,((preorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Opreorder_2)).
% 49.54/29.20 thf(785,plain,((preorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 49.54/29.20 thf(29,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_order_Ostrict__trans1)).
% 49.54/29.20 thf(372,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 49.54/29.20 thf(176,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((minus_minus @ (countable_Set_cset @ TA) @ A @ (bot_bot @ (countable_Set_cset @ TA))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_cDiff__cempty)).
% 49.54/29.20 thf(838,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((minus_minus @ (countable_Set_cset @ TA) @ A @ (bot_bot @ (countable_Set_cset @ TA))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 49.54/29.20 thf(205,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((A = B) => (~ ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => (~ (ord_less_eq @ (countable_Set_cset @ TA) @ B @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_cequalityE)).
% 49.54/29.20 thf(917,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((A = B) => (~ ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => (~ (ord_less_eq @ (countable_Set_cset @ TA) @ B @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 49.54/29.20 thf(18,axiom,((linorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Olinorder)).
% 49.54/29.20 thf(344,plain,((linorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 49.54/29.20 thf(208,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ~ (ord_less @ (countable_Set_cset @ TA) @ A @ (bot_bot @ (countable_Set_cset @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_not__cpsubset__cempty)).
% 49.54/29.20 thf(934,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ~ (ord_less @ (countable_Set_cset @ TA) @ A @ (bot_bot @ (countable_Set_cset @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 49.54/29.20 thf(252,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:TA]: (((~ (countable_Set_cin @ TA @ A @ B)) => (A = C)) => (countable_Set_cin @ TA @ A @ (counta2111716221insert @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_cinsertCI)).
% 49.54/29.20 thf(1059,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:TA]: (((~ (countable_Set_cin @ TA @ A @ B)) => (A = C)) => (countable_Set_cin @ TA @ A @ (counta2111716221insert @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 49.54/29.20 thf(213,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA,C:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ C)) = (((countable_Set_cin @ TA @ B @ A) => (ord_less_eq @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) @ C)) & ((~ (countable_Set_cin @ TA @ B @ A)) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_csubset__cinsert__iff)).
% 49.54/29.20 thf(949,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA,C:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ C)) = (((countable_Set_cin @ TA @ B @ A) => (ord_less_eq @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) @ C)) & ((~ (countable_Set_cin @ TA @ B @ A)) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 49.54/29.20 thf(82,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TC > TB),B:(TB > ((TC > TB) > TB)),C:((TD > TB) > TB),D:(TD > (TB > TB)),E:((countable_Set_cset @ TA) > ((TA > TB) > TB))]: ((monomo1036387116e_altc @ TC @ TB @ TD @ TA @ A @ B @ C @ D @ E) => (monomo439771545d_altc @ TC @ TB @ TA @ A @ B @ E))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_monad__state__altc_Oaxioms_I2_J)).
% 49.54/29.20 thf(542,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TC > TB),B:(TB > ((TC > TB) > TB)),C:((TD > TB) > TB),D:(TD > (TB > TB)),E:((countable_Set_cset @ TA) > ((TA > TB) > TB))]: ((monomo1036387116e_altc @ TC @ TB @ TD @ TA @ (A) @ (B) @ (C) @ (D) @ (E)) => (monomo439771545d_altc @ TC @ TB @ TA @ (A) @ (B) @ (E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 49.54/29.20 thf(55,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_173_dense)).
% 49.54/29.20 thf(460,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)],[55])).
% 49.54/29.20 thf(181,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less_eq @ (countable_Set_cset @ TA) @ B @ A) => (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_csubset__antisym)).
% 49.54/29.20 thf(853,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less_eq @ (countable_Set_cset @ TA) @ B @ A) => (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 49.54/29.20 thf(221,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:TA,D:TA]: (((counta2111716221insert @ TA @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) = (counta2111716221insert @ TA @ C @ (counta2111716221insert @ TA @ D @ (bot_bot @ (countable_Set_cset @ TA))))) = (((A = C) & (B = D)) | ((A = D) & (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_cdoubleton__eq__iff)).
% 49.54/29.20 thf(969,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:TA,D:TA]: (((counta2111716221insert @ TA @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) = (counta2111716221insert @ TA @ C @ (counta2111716221insert @ TA @ D @ (bot_bot @ (countable_Set_cset @ TA))))) = (((A = C) & (B = D)) | ((A = D) & (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 49.54/29.20 thf(41,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oord)).
% 49.54/29.20 thf(416,plain,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 49.54/29.20 thf(9,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_le__cases)).
% 49.54/29.20 thf(316,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 49.54/29.20 thf(43,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_less__asym)).
% 49.54/29.20 thf(421,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 49.54/29.20 thf(187,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA,C:(countable_Set_cset @ TA)]: ((minus_minus @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ C)) = (minus_minus @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_cDiff__cinsert2)).
% 49.54/29.20 thf(870,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA,C:(countable_Set_cset @ TA)]: ((minus_minus @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ C)) = (minus_minus @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 49.54/29.20 thf(60,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ A @ B) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_le__funE)).
% 49.54/29.20 thf(475,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ (A) @ (B)) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 49.54/29.20 thf(67,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_212_le__neq__trans)).
% 49.54/29.20 thf(492,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)],[67])).
% 49.54/29.20 thf(148,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > TC),B:(TA > TC)]: ((! [C:TA]: ? [D:TB]: ((A @ D) = (B @ C))) = (? [C:(TA > TB)]: (B = (comp @ TB @ TC @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_function__factors__right)).
% 49.54/29.20 thf(756,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TB > TC),B:(TA > TC)]: ((! [C:TA]: ? [D:TB]: ((A @ D) = (B @ C))) = (? [C:(TA > TB)]: ((B) = (comp @ TB @ TC @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 49.54/29.20 thf(159,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_166_order__less__subst2)).
% 49.54/29.20 thf(789,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)],[159])).
% 49.54/29.20 thf(31,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_226_order_Oorder__iff__strict)).
% 49.54/29.20 thf(376,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)],[31])).
% 49.54/29.20 thf(110,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_204_le__less)).
% 49.54/29.20 thf(623,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)],[110])).
% 49.54/29.20 thf(64,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TA) => (minus @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Groups_Ominus)).
% 49.54/29.20 thf(485,plain,((! [TA: $tType,TB: $tType]: ((minus @ TA) => (minus @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 49.54/29.20 thf(20,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_order__refl)).
% 49.54/29.20 thf(348,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 49.54/29.20 thf(22,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_213_antisym__conv1)).
% 49.54/29.20 thf(353,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)],[22])).
% 49.54/29.20 thf(249,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((minus_minus @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ B) @ B) = (minus_minus @ (countable_Set_cset @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_cDiff__idemp)).
% 49.54/29.20 thf(1051,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((minus_minus @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ B) @ B) = (minus_minus @ (countable_Set_cset @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 49.54/29.20 thf(245,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((minus_minus @ (countable_Set_cset @ TA) @ (bot_bot @ (countable_Set_cset @ TA)) @ A) = (bot_bot @ (countable_Set_cset @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_cempty__cDiff)).
% 49.54/29.20 thf(1040,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((minus_minus @ (countable_Set_cset @ TA) @ (bot_bot @ (countable_Set_cset @ TA)) @ A) = (bot_bot @ (countable_Set_cset @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 49.54/29.20 thf(11,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_189_linorder__cases)).
% 49.54/29.20 thf(321,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)],[11])).
% 49.54/29.20 thf(200,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((! [B:TA]: ~ (countable_Set_cin @ TA @ B @ A)) => (A = (bot_bot @ (countable_Set_cset @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_equals__cemptyI)).
% 49.54/29.20 thf(905,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((! [B:TA]: ~ (countable_Set_cin @ TA @ B @ A)) => (A = (bot_bot @ (countable_Set_cset @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 49.54/29.20 thf(62,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_dual__order_Oirrefl)).
% 49.54/29.20 thf(480,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 49.54/29.20 thf(102,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((comp @ TA @ TB @ TC) = (^ [A:(TA > TB),B:(TC > TA),C:TC]: (A @ (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_comp__apply)).
% 49.54/29.20 thf(602,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((comp @ TA @ TB @ TC) = (^ [A:(TA > TB),B:(TC > TA),C:TC]: (A @ (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 49.54/29.20 thf(141,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((B = C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_ord__le__eq__trans)).
% 49.54/29.20 thf(734,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((B = C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 49.54/29.20 thf(53,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_165_order__less__subst1)).
% 49.54/29.20 thf(453,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)],[53])).
% 49.54/29.20 thf(153,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_191_order_Ostrict__trans)).
% 49.54/29.20 thf(774,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)],[153])).
% 49.54/29.20 thf(269,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) => ((A = (bot_bot @ (countable_Set_cset @ TA))) | (A = (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_csubset__csingletonD)).
% 49.54/29.20 thf(1104,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) => ((A = (bot_bot @ (countable_Set_cset @ TA))) | (A = (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 49.54/29.20 thf(72,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:((countable_Set_cset @ TC) > TB),B:(TB > (((countable_Set_cset @ TC) > TB) > TB)),C:((countable_Set_cset @ TC) > ((TC > TB) > TB)),D:((countable_Set_cset @ TA) > ((TA > TB) > TB))]: ((monomo2011693592ondetM @ TC @ TB @ TA @ A @ B @ C @ D) => (monomo759963067axioms @ TC @ TB @ TA @ A @ B @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_cset__nondetM_Oaxioms_I3_J)).
% 49.54/29.20 thf(507,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:((countable_Set_cset @ TC) > TB),B:(TB > (((countable_Set_cset @ TC) > TB) > TB)),C:((countable_Set_cset @ TC) > ((TC > TB) > TB)),D:((countable_Set_cset @ TA) > ((TA > TB) > TB))]: ((monomo2011693592ondetM @ TC @ TB @ TA @ (A) @ (B) @ (C) @ (D)) => (monomo759963067axioms @ TC @ TB @ TA @ (A) @ (B) @ (C) @ (D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 49.54/29.20 thf(79,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_206_order__le__less__subst1)).
% 49.54/29.20 thf(527,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)],[79])).
% 49.54/29.20 thf(34,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TB),B:(TA > TD),C:TA,D:(TC > TB),E:(TA > TC)]: (((A @ (B @ C)) = (D @ (E @ C))) => ((comp @ TD @ TB @ TA @ A @ B @ C) = (comp @ TC @ TB @ TA @ D @ E @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_comp__apply__eq)).
% 49.54/29.20 thf(397,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TB),B:(TA > TD),C:TA,D:(TC > TB),E:(TA > TC)]: (((A @ (B @ C)) = (D @ (E @ C))) => ((comp @ TD @ TB @ TA @ (A) @ (B) @ C) = (comp @ TC @ TB @ TA @ (D) @ (E) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 49.54/29.20 thf(127,axiom,((order_bot @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder__bot_1)).
% 49.54/29.20 thf(687,plain,((order_bot @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 49.54/29.20 thf(39,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_195_dual__order_Ostrict__trans)).
% 49.54/29.20 thf(411,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)],[39])).
% 49.54/29.20 thf(228,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((countable_Set_cin @ TA @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_csingleton__iff)).
% 49.54/29.20 thf(988,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((countable_Set_cin @ TA @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 49.54/29.20 thf(256,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: (countable_Set_cin @ TA @ A @ (counta2111716221insert @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_cinsertI1)).
% 49.54/29.20 thf(1074,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: (countable_Set_cin @ TA @ A @ (counta2111716221insert @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 49.54/29.20 thf(49,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_less__le__trans)).
% 49.54/29.20 thf(439,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 49.54/29.20 thf(123,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > TB),B:(TB > ((TC > TB) > TB)),C:((countable_Set_cset @ TA) > ((TA > TB) > TB))]: ((monomo1425736922_altc3 @ TC @ TB @ TA @ A @ B @ C) => (monomo439771545d_altc @ TC @ TB @ TA @ A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_monad__altc3_Oaxioms_I1_J)).
% 49.54/29.20 thf(678,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > TB),B:(TB > ((TC > TB) > TB)),C:((countable_Set_cset @ TA) > ((TA > TB) > TB))]: ((monomo1425736922_altc3 @ TC @ TB @ TA @ (A) @ (B) @ (C)) => (monomo439771545d_altc @ TC @ TB @ TA @ (A) @ (B) @ (C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 49.54/29.20 thf(206,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((A = B) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_cequalityD1)).
% 49.54/29.20 thf(925,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((A = B) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 49.54/29.20 thf(150,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_less__trans)).
% 49.54/29.20 thf(761,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 49.54/29.20 thf(135,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > $o),B:(TB > TC),C:(monomo1453983439ondetT @ TA @ TB)]: ((A @ (monomo1564381680ondetT @ TB @ TC @ TA @ B @ C)) = (~ ((C = (monomo1975189248ondetT @ TB @ TA @ (monomo603716163nondet @ TA @ TB @ C))) & ~ (A @ (B @ (monomo603716163nondet @ TA @ TB @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_nondetT_Osplit__sel__asm)).
% 49.54/29.20 thf(714,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > $o),B:(TB > TC),C:(monomo1453983439ondetT @ TA @ TB)]: ((A @ (monomo1564381680ondetT @ TB @ TC @ TA @ (B) @ C)) = (~ ((C = (monomo1975189248ondetT @ TB @ TA @ (monomo603716163nondet @ TA @ TB @ C))) & ~ (A @ (B @ (monomo603716163nondet @ TA @ TB @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 49.54/29.20 thf(251,axiom,((! [TA: $tType]: (ord @ (countable_Set_cset @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Countable__Set__Type_Ocset___Orderings_Oord_10)).
% 49.54/29.20 thf(1057,plain,((! [TA: $tType]: (ord @ (countable_Set_cset @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 49.54/29.20 thf(84,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType]: (! [A:(TE > TD),B:(TA > TE),C:(TB > TD),D:(TA > TB),E:(TD > TC),F:(TB > TC)]: (((comp @ TE @ TD @ TA @ A @ B) = (comp @ TB @ TD @ TA @ C @ D)) => (((comp @ TD @ TC @ TB @ E @ C) = F) => ((comp @ TE @ TC @ TA @ (comp @ TD @ TC @ TE @ E @ A) @ B) = (comp @ TB @ TC @ TA @ F @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_rewriteR__comp__comp2)).
% 49.54/29.20 thf(546,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType]: (! [A:(TE > TD),B:(TA > TE),C:(TB > TD),D:(TA > TB),E:(TD > TC),F:(TB > TC)]: (((comp @ TE @ TD @ TA @ A @ B) = (comp @ TB @ TD @ TA @ C @ D)) => (((comp @ TD @ TC @ TB @ E @ C) = (F)) => ((comp @ TE @ TC @ TA @ (comp @ TD @ TC @ TE @ E @ A) @ B) = (comp @ TB @ TC @ TA @ F @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 49.54/29.20 thf(160,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_208_order__less__le__subst1)).
% 49.54/29.20 thf(793,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)],[160])).
% 49.54/29.20 thf(202,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((ord_less @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less_eq @ (countable_Set_cset @ TA) @ B @ C) => (ord_less @ (countable_Set_cset @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_cpsubset__csubset__trans)).
% 49.54/29.20 thf(910,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((ord_less @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less_eq @ (countable_Set_cset @ TA) @ B @ C) => (ord_less @ (countable_Set_cset @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 49.54/29.20 thf(196,axiom,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ A @ (bot_bot @ TA)) => (A = (bot_bot @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_bot_Oextremum__uniqueI)).
% 49.54/29.20 thf(894,plain,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ A @ (bot_bot @ TA)) => (A = (bot_bot @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 49.54/29.20 thf(264,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:((countable_Set_cset @ TA) > ((TA > TC) > TC)),B:(countable_Set_cset @ TA),C:(TA > (monomo1453983439ondetT @ TB @ TC))]: ((monomo603716163nondet @ TB @ TC @ (monomo955616121nondet @ TA @ TC @ TB @ A @ B @ C)) = (A @ B @ (comp @ (monomo1453983439ondetT @ TB @ TC) @ TC @ TA @ (monomo603716163nondet @ TB @ TC) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_cset__nondetM__base_Orun__altc__nondet)).
% 49.54/29.20 thf(1091,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:((countable_Set_cset @ TA) > ((TA > TC) > TC)),B:(countable_Set_cset @ TA),C:(TA > (monomo1453983439ondetT @ TB @ TC))]: ((monomo603716163nondet @ TB @ TC @ (monomo955616121nondet @ TA @ TC @ TB @ (A) @ B @ (C))) = (A @ B @ (comp @ (monomo1453983439ondetT @ TB @ TC) @ TC @ TA @ (monomo603716163nondet @ TB @ TC) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 49.54/29.20 thf(171,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_dual__order_Otrans)).
% 49.54/29.20 thf(825,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 49.54/29.20 thf(240,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (counta2111716221insert @ TA @ B @ C)) => ((A != B) => (countable_Set_cin @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_cinsertE)).
% 49.54/29.20 thf(1021,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (counta2111716221insert @ TA @ B @ C)) => ((~ (A = B)) => (countable_Set_cin @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 49.54/29.20 thf(214,axiom,((! [TA: $tType]: (! [A:TA,B:$o,C:(countable_Set_cset @ TA),D:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (if @ (countable_Set_cset @ TA) @ B @ C @ D)) = (((B) => (countable_Set_cin @ TA @ A @ C)) & ((~ (B)) => (countable_Set_cin @ TA @ A @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_if__split__cin2)).
% 49.54/29.20 thf(952,plain,((! [TA: $tType]: (! [A:TA,B:$o,C:(countable_Set_cset @ TA),D:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (if @ (countable_Set_cset @ TA) @ B @ C @ D)) = (((B) => (countable_Set_cin @ TA @ A @ C)) & ((~ (B)) => (countable_Set_cin @ TA @ A @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 49.54/29.20 thf(37,axiom,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Opreorder)).
% 49.54/29.20 thf(407,plain,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 49.54/29.20 thf(46,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType]: (! [A:(TD > TB),B:(TE > TD),C:TE,D:(TC > TB),E:(TA > TC),F:TA]: (((A @ (B @ C)) = (D @ (E @ F))) => ((comp @ TD @ TB @ TE @ A @ B @ C) = (comp @ TC @ TB @ TA @ D @ E @ F)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_comp__cong)).
% 49.54/29.20 thf(429,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType]: (! [A:(TD > TB),B:(TE > TD),C:TE,D:(TC > TB),E:(TA > TC),F:TA]: (((A @ (B @ C)) = (D @ (E @ F))) => ((comp @ TD @ TB @ TE @ (A) @ (B) @ C) = (comp @ TC @ TB @ TA @ (D) @ (E) @ F)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 49.54/29.20 thf(3,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_T)).
% 49.54/29.20 thf(275,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 49.54/29.20 thf(242,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA]: ((A = (bot_bot @ (countable_Set_cset @ TA))) => (~ (countable_Set_cin @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_equals__cemptyD)).
% 49.54/29.20 thf(1027,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA]: ((A = (bot_bot @ (countable_Set_cset @ TA))) => (~ (countable_Set_cin @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 49.54/29.20 thf(134,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ A @ C) => (ord_less_eq @ TA @ B @ C))) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_dense__ge)).
% 49.54/29.20 thf(710,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ A @ C) => (ord_less_eq @ TA @ B @ C))) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 49.54/29.20 thf(12,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_169_neqE)).
% 49.54/29.20 thf(324,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)],[12])).
% 49.54/29.20 thf(237,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ C)) => (countable_Set_cin @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_cDiffD1)).
% 49.54/29.20 thf(1012,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ C)) => (countable_Set_cin @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 49.54/29.20 thf(95,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > $o),B:(TB > TC),C:(monomo1453983439ondetT @ TA @ TB)]: ((A @ (monomo1564381680ondetT @ TB @ TC @ TA @ B @ C)) = ((C = (monomo1975189248ondetT @ TB @ TA @ (monomo603716163nondet @ TA @ TB @ C))) => (A @ (B @ (monomo603716163nondet @ TA @ TB @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_nondetT_Osplit__sel)).
% 49.54/29.20 thf(583,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > $o),B:(TB > TC),C:(monomo1453983439ondetT @ TA @ TB)]: ((A @ (monomo1564381680ondetT @ TB @ TC @ TA @ (B) @ C)) = ((C = (monomo1975189248ondetT @ TB @ TA @ (monomo603716163nondet @ TA @ TB @ C))) => (A @ (B @ (monomo603716163nondet @ TA @ TB @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 49.54/29.20 thf(173,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_210_not__le)).
% 49.54/29.20 thf(830,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)],[173])).
% 49.54/29.20 thf(76,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_241_diff__strict__left__mono)).
% 49.54/29.20 thf(519,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)],[76])).
% 49.54/29.20 thf(263,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA]: (ord_less_eq @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_csubset__cinsertI)).
% 49.54/29.20 thf(1089,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA]: (ord_less_eq @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 49.54/29.20 thf(239,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((! [C:TA]: ((countable_Set_cin @ TA @ C @ A) => (countable_Set_cin @ TA @ C @ B))) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_csubsetI)).
% 49.54/29.20 thf(1017,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((! [C:TA]: ((countable_Set_cin @ TA @ C @ A) => (countable_Set_cin @ TA @ C @ B))) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 49.54/29.20 thf(106,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > TA),B:(TC > TB)]: ((! [C:TC,D:TC]: (((A @ C) = (A @ D)) => ((B @ C) = (B @ D)))) = (? [C:(TA > TB)]: (B = (comp @ TA @ TB @ TC @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_function__factors__left)).
% 49.54/29.20 thf(615,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > TA),B:(TC > TB)]: ((! [C:TC,D:TC]: (((A @ C) = (A @ D)) => ((B @ C) = (B @ D)))) = (? [C:(TA > TB)]: ((B) = (comp @ TA @ TB @ TC @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 49.54/29.20 thf(23,axiom,((! [TA: $tType]: (! [A:$o,B:TA,C:TA,D:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ (if @ TA @ A @ B @ C) @ D) = (((A) => (countable_Set_cin @ TA @ B @ D)) & ((~ (A)) => (countable_Set_cin @ TA @ C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_if__split__cin1)).
% 49.54/29.20 thf(356,plain,((! [TA: $tType]: (! [A:$o,B:TA,C:TA,D:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ (if @ TA @ A @ B @ C) @ D) = (((A) => (countable_Set_cin @ TA @ B @ D)) & ((~ (A)) => (countable_Set_cin @ TA @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 49.54/29.20 thf(98,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_order_Ostrict__trans2)).
% 49.54/29.20 thf(593,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 49.54/29.20 thf(156,axiom,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_gt__ex)).
% 49.54/29.20 thf(783,plain,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 49.54/29.20 thf(260,axiom,((! [TA: $tType]: (preorder @ (countable_Set_cset @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Countable__Set__Type_Ocset___Orderings_Opreorder_8)).
% 49.54/29.20 thf(1082,plain,((! [TA: $tType]: (preorder @ (countable_Set_cset @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 49.54/29.20 thf(66,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((A != B) => ((ord_less_eq @ TA @ A @ B) => (ord_less @ TA @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_order_Onot__eq__order__implies__strict)).
% 49.54/29.20 thf(489,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) => ((ord_less_eq @ TA @ A @ B) => (ord_less @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 49.54/29.20 thf(86,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ A @ B) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_le__funD)).
% 49.54/29.20 thf(554,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ (A) @ (B)) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 49.54/29.20 thf(147,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_162_verit__comp__simplify1_I3_J)).
% 49.54/29.20 thf(753,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)],[147])).
% 49.54/29.20 thf(109,axiom,((minus @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Groups_Ominus_6)).
% 49.54/29.20 thf(622,plain,((minus @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 49.54/29.20 thf(33,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_less__imp__not__eq)).
% 49.54/29.20 thf(393,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 49.54/29.20 thf(75,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_209_order__less__le__subst2)).
% 49.54/29.20 thf(515,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)],[75])).
% 49.54/29.20 thf(142,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_antisym)).
% 49.54/29.20 thf(738,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 49.54/29.20 thf(54,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_205_less__le)).
% 49.54/29.20 thf(457,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)],[54])).
% 49.54/29.20 thf(233,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((countable_Set_cin @ TA @ C @ A) => (countable_Set_cin @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_cin__mono)).
% 49.54/29.20 thf(1002,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((countable_Set_cin @ TA @ C @ A) => (countable_Set_cin @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 49.54/29.20 thf(91,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_less__imp__not__eq2)).
% 49.54/29.20 thf(569,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 49.54/29.20 thf(155,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((A = B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_eq__refl)).
% 49.54/29.20 thf(779,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((A = B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 49.54/29.20 thf(115,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(countable_Set_cset @ TA)]: ((A = B) => ((countable_Set_cin @ TA @ B @ C) => (countable_Set_cin @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_eq__cmem__trans)).
% 49.54/29.20 thf(647,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(countable_Set_cset @ TA)]: ((A = B) => ((countable_Set_cin @ TA @ B @ C) => (countable_Set_cin @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 49.54/29.20 thf(231,axiom,((! [TA: $tType]: (! [A:TA]: ~ (countable_Set_cin @ TA @ A @ (bot_bot @ (countable_Set_cset @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_cemptyE)).
% 49.54/29.20 thf(997,plain,((! [TA: $tType]: (! [A:TA]: ~ (countable_Set_cin @ TA @ A @ (bot_bot @ (countable_Set_cset @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 49.54/29.20 thf(267,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((~ (countable_Set_cin @ TA @ A @ B)) => ((ord_less_eq @ (countable_Set_cset @ TA) @ B @ (counta2111716221insert @ TA @ A @ C)) = (ord_less_eq @ (countable_Set_cset @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_csubset__cinsert)).
% 49.54/29.20 thf(1099,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((~ (countable_Set_cin @ TA @ A @ B)) => ((ord_less_eq @ (countable_Set_cset @ TA) @ B @ (counta2111716221insert @ TA @ A @ C)) = (ord_less_eq @ (countable_Set_cset @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 49.54/29.20 thf(227,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_238_bot_Onot__eq__extremum)).
% 49.54/29.20 thf(985,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)],[227])).
% 49.54/29.20 thf(71,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType]: (! [A:(TD > TC),B:(TE > TD),C:(TB > TC),D:(TE > TB),E:(TA > TE),F:(TA > TB)]: (((comp @ TD @ TC @ TE @ A @ B) = (comp @ TB @ TC @ TE @ C @ D)) => (((comp @ TE @ TB @ TA @ D @ E) = F) => ((comp @ TD @ TC @ TA @ A @ (comp @ TE @ TD @ TA @ B @ E)) = (comp @ TB @ TC @ TA @ C @ F))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_rewriteL__comp__comp2)).
% 49.54/29.20 thf(503,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType]: (! [A:(TD > TC),B:(TE > TD),C:(TB > TC),D:(TE > TB),E:(TA > TE),F:(TA > TB)]: (((comp @ TD @ TC @ TE @ A @ B) = (comp @ TB @ TC @ TE @ C @ D)) => (((comp @ TE @ TB @ TA @ D @ E) = (F)) => ((comp @ TD @ TC @ TA @ A @ (comp @ TE @ TD @ TA @ B @ E)) = (comp @ TB @ TC @ TA @ C @ F))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 49.54/29.20 thf(103,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:TA]: (((monomo1975189248ondetT @ TA @ TB @ A) = (monomo1975189248ondetT @ TA @ TB @ B)) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_nondetT_Oinject)).
% 49.54/29.20 thf(605,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:TA]: (((monomo1975189248ondetT @ TA @ TB @ A) = (monomo1975189248ondetT @ TA @ TB @ B)) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 49.54/29.20 thf(262,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ (counta2111716221insert @ TA @ A @ B) @ C) = ((countable_Set_cin @ TA @ A @ C) & (ord_less_eq @ (countable_Set_cset @ TA) @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_cinsert__csubset)).
% 49.54/29.20 thf(1086,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ (counta2111716221insert @ TA @ A @ B) @ C) = ((countable_Set_cin @ TA @ A @ C) & (ord_less_eq @ (countable_Set_cset @ TA) @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 49.54/29.20 thf(164,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TA > TB),B:TA]: ((monomo1291740684ondetT @ TA @ TB @ TC @ A @ (monomo1975189248ondetT @ TA @ TC @ B)) = (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_nondetT_Orec)).
% 49.54/29.20 thf(805,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TA > TB),B:TA]: ((monomo1291740684ondetT @ TA @ TB @ TC @ (A) @ (monomo1975189248ondetT @ TA @ TC @ B)) = (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 49.54/29.20 thf(255,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((~ (countable_Set_cin @ TA @ A @ B)) => ((~ (countable_Set_cin @ TA @ A @ C)) => (((counta2111716221insert @ TA @ A @ B) = (counta2111716221insert @ TA @ A @ C)) = (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_cinsert__ident)).
% 49.54/29.20 thf(1071,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((~ (countable_Set_cin @ TA @ A @ B)) => ((~ (countable_Set_cin @ TA @ A @ C)) => (((counta2111716221insert @ TA @ A @ B) = (counta2111716221insert @ TA @ A @ C)) = (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 49.54/29.20 thf(96,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_64_cancel__ab__semigroup__add__class_Odiff__right__commute)).
% 49.54/29.20 thf(586,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)],[96])).
% 49.54/29.20 thf(194,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: (((counta2111716221insert @ TA @ A @ (bot_bot @ (countable_Set_cset @ TA))) = (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_csingleton__inject)).
% 49.54/29.20 thf(888,plain,((! [TA: $tType]: (! [A:TA,B:TA]: (((counta2111716221insert @ TA @ A @ (bot_bot @ (countable_Set_cset @ TA))) = (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 49.54/29.20 thf(152,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:(TA > $o),B:TA]: ((A @ B) => ((! [C:TA]: ((A @ C) => (ord_less_eq @ TA @ C @ B))) => ((order_Greatest @ TA @ A) = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_Greatest__equality)).
% 49.54/29.20 thf(765,plain,((! [TA: $tType]: ((order @ TA) => (! [A:(TA > $o),B:TA]: ((A @ B) => ((! [C:TA]: ((A @ C) => (ord_less_eq @ TA @ C @ B))) => ((order_Greatest @ TA @ (A)) = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 49.54/29.20 thf(250,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_bot__fun__def)).
% 49.54/29.20 thf(1054,plain,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 49.54/29.20 thf(7,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_196_not__less__iff__gr__or__eq)).
% 49.54/29.20 thf(298,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)],[7])).
% 49.54/29.20 thf(107,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_182_dual__order_Oasym)).
% 49.54/29.20 thf(618,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)],[107])).
% 49.54/29.20 thf(74,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (ord_less_eq @ TA @ C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_255_minf_I6_J)).
% 49.54/29.20 thf(513,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (ord_less_eq @ TA @ C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 49.54/29.20 thf(182,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:((countable_Set_cset @ TC) > TB),B:(TB > (((countable_Set_cset @ TC) > TB) > TB)),C:((countable_Set_cset @ TC) > ((TC > TB) > TB)),D:((countable_Set_cset @ TA) > ((TA > TB) > TB)),E:TA,F:(TA > TB)]: ((monomo2011693592ondetM @ TC @ TB @ TA @ A @ B @ C @ D) => ((D @ (counta2111716221insert @ TA @ E @ (bot_bot @ (countable_Set_cset @ TA))) @ F) = (F @ E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_cset__nondetM_Omergec__single)).
% 49.54/29.20 thf(856,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:((countable_Set_cset @ TC) > TB),B:(TB > (((countable_Set_cset @ TC) > TB) > TB)),C:((countable_Set_cset @ TC) > ((TC > TB) > TB)),D:((countable_Set_cset @ TA) > ((TA > TB) > TB)),E:TA,F:(TA > TB)]: ((monomo2011693592ondetM @ TC @ TB @ TA @ (A) @ (B) @ (C) @ (D)) => ((D @ (counta2111716221insert @ TA @ E @ (bot_bot @ (countable_Set_cset @ TA))) @ (F)) = (F @ E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 49.54/29.20 thf(92,axiom,((! [TA: $tType]: ((preorder @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_less__le__not__le)).
% 49.54/29.20 thf(573,plain,((! [TA: $tType]: ((preorder @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 49.54/29.20 thf(219,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA,C:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) @ C) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_cDiff__single__cinsert)).
% 49.54/29.20 thf(965,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA,C:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))) @ C) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 49.54/29.20 thf(146,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType]: (! [A:(TE > TB),B:(TA > TE),C:TA,D:(TD > TB),E:(TA > TD),F:(TB > TC)]: (((A @ (B @ C)) = (D @ (E @ C))) => ((comp @ TE @ TC @ TA @ (comp @ TB @ TC @ TE @ F @ A) @ B @ C) = (comp @ TD @ TC @ TA @ (comp @ TB @ TC @ TD @ F @ D) @ E @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_type__copy__map__cong0)).
% 49.54/29.20 thf(750,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType,TE: $tType]: (! [A:(TE > TB),B:(TA > TE),C:TA,D:(TD > TB),E:(TA > TD),F:(TB > TC)]: (((A @ (B @ C)) = (D @ (E @ C))) => ((comp @ TE @ TC @ TA @ (comp @ TB @ TC @ TE @ F @ A) @ (B) @ C) = (comp @ TD @ TC @ TA @ (comp @ TB @ TC @ TD @ F @ D) @ (E) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 49.54/29.20 thf(169,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((comp @ TA @ TB @ TC) = (^ [A:(TA > TB),B:(TC > TA),C:TC]: (A @ (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_comp__def)).
% 49.54/29.20 thf(819,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((comp @ TA @ TB @ TC) = (^ [A:(TA > TB),B:(TC > TA),C:TC]: (A @ (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 49.54/29.20 thf(44,axiom,((! [TA: $tType,TB: $tType]: (! [A:(monomo1453983439ondetT @ TA @ TB)]: (A = (monomo1975189248ondetT @ TB @ TA @ (monomo603716163nondet @ TA @ TB @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_nondetT_Oexhaust__sel)).
% 49.54/29.20 thf(423,plain,((! [TA: $tType,TB: $tType]: (! [A:(monomo1453983439ondetT @ TA @ TB)]: (A = (monomo1975189248ondetT @ TB @ TA @ (monomo603716163nondet @ TA @ TB @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 49.54/29.20 thf(189,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_bot__apply)).
% 49.54/29.20 thf(875,plain,((! [TA: $tType,TB: $tType]: ((bot @ TB) => ((bot_bot @ (TA > TB)) = (^ [A:TA]: (bot_bot @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 49.54/29.20 thf(216,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((monomo955616121nondet @ TA @ TB @ TC) = (monomo955616121nondet @ TA @ TB @ TC)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_cset__nondetM__base_Oaltc__nondet_Ocong)).
% 49.54/29.20 thf(958,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 49.54/29.20 thf(40,axiom,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ B @ A) & (ord_less_eq @ TA @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_dual__order_Oeq__iff)).
% 49.54/29.20 thf(413,plain,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ B @ A) & (ord_less_eq @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 49.54/29.20 thf(89,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TC),B:(TB > TD),C:(TA > TB)]: ((comp @ TD @ TC @ TA @ A @ (comp @ TB @ TD @ TA @ B @ C)) = (comp @ TB @ TC @ TA @ (comp @ TD @ TC @ TB @ A @ B) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_fun_Omap__comp)).
% 49.54/29.20 thf(562,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TC),B:(TB > TD),C:(TA > TB)]: ((comp @ TD @ TC @ TA @ A @ (comp @ TB @ TD @ TA @ B @ C)) = (comp @ TB @ TC @ TA @ (comp @ TD @ TC @ TB @ A @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 49.54/29.20 thf(223,axiom,((! [TA: $tType]: (order @ (countable_Set_cset @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Countable__Set__Type_Ocset___Orderings_Oorder_9)).
% 49.54/29.20 thf(975,plain,((! [TA: $tType]: (order @ (countable_Set_cset @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 49.54/29.20 thf(235,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((counta2111716221insert @ TA @ A @ B) != (bot_bot @ (countable_Set_cset @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_cinsert__not__cempty)).
% 49.54/29.20 thf(1007,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ~ ((counta2111716221insert @ TA @ A @ B) = (bot_bot @ (countable_Set_cset @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 49.54/29.20 thf(130,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_239_diff__strict__mono)).
% 49.54/29.20 thf(694,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)],[130])).
% 49.54/29.20 thf(209,axiom,((! [TA: $tType]: ((monomo410456285nondet @ TA @ m @ a) = (^ [A:(TA > (m > m)),B:TA,C:(monomo1453983439ondetT @ a @ m)]: (monomo1975189248ondetT @ m @ a @ (A @ B @ (monomo603716163nondet @ a @ m @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_put__nondet__def)).
% 49.54/29.20 thf(936,plain,((! [TA: $tType]: ((monomo410456285nondet @ TA @ m @ a) = (^ [A:(TA > (m > m)),B:TA,C:(monomo1453983439ondetT @ a @ m)]: (monomo1975189248ondetT @ m @ a @ (A @ B @ (monomo603716163nondet @ a @ m @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 49.54/29.20 thf(105,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > TB),B:(TA > TC),C:(TA > TB),D:TA]: (((comp @ TC @ TB @ TA @ A @ B) = C) => ((A @ (B @ D)) = (C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_comp__eq__dest__lhs)).
% 49.54/29.20 thf(611,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > TB),B:(TA > TC),C:(TA > TB),D:TA]: (((comp @ TC @ TB @ TA @ A @ B) = (C)) => ((A @ (B @ D)) = (C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 49.54/29.20 thf(69,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_dual__order_Oorder__iff__strict)).
% 49.54/29.20 thf(498,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 49.54/29.20 thf(270,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(countable_Set_cset @ TA)]: ((counta2111716221insert @ TA @ A @ (counta2111716221insert @ TA @ B @ C)) = (counta2111716221insert @ TA @ B @ (counta2111716221insert @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_cinsert__commute)).
% 49.54/29.20 thf(1107,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(countable_Set_cset @ TA)]: ((counta2111716221insert @ TA @ A @ (counta2111716221insert @ TA @ B @ C)) = (counta2111716221insert @ TA @ B @ (counta2111716221insert @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 49.54/29.20 thf(16,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_170_neq__iff)).
% 49.54/29.20 thf(335,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)],[16])).
% 49.54/29.20 thf(21,axiom,((! [TA: $tType,TB: $tType]: (! [A:(monomo1453983439ondetT @ TB @ TA)]: ~ (! [B:TA]: (A != (monomo1975189248ondetT @ TA @ TB @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_nondetT_Oexhaust)).
% 49.54/29.20 thf(350,plain,((! [TA: $tType,TB: $tType]: (! [A:(monomo1453983439ondetT @ TB @ TA)]: ~ (! [B:TA]: ~ (A = (monomo1975189248ondetT @ TA @ TB @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 49.54/29.20 thf(225,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ C)) => (~ ((countable_Set_cin @ TA @ A @ B) => (countable_Set_cin @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_cDiffE)).
% 49.54/29.20 thf(979,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ C)) => (~ ((countable_Set_cin @ TA @ A @ B) => (countable_Set_cin @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 49.54/29.20 thf(198,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > TB),B:(TB > ((TC > TB) > TB)),C:((countable_Set_cset @ TA) > ((TA > TB) > TB)),D:TA,E:(TA > TB)]: ((monomo439771545d_altc @ TC @ TB @ TA @ A @ B @ C) => ((C @ (counta2111716221insert @ TA @ D @ (bot_bot @ (countable_Set_cset @ TA))) @ E) = (E @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_monad__altc_Oaltc__single)).
% 49.54/29.20 thf(900,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > TB),B:(TB > ((TC > TB) > TB)),C:((countable_Set_cset @ TA) > ((TA > TB) > TB)),D:TA,E:(TA > TB)]: ((monomo439771545d_altc @ TC @ TB @ TA @ (A) @ (B) @ (C)) => ((C @ (counta2111716221insert @ TA @ D @ (bot_bot @ (countable_Set_cset @ TA))) @ (E)) = (E @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 49.54/29.20 thf(248,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((~ (countable_Set_cin @ TA @ A @ B)) => ((minus_minus @ (countable_Set_cset @ TA) @ (counta2111716221insert @ TA @ A @ B) @ (counta2111716221insert @ TA @ A @ (bot_bot @ (countable_Set_cset @ TA)))) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_cDiff__cinsert__absorb)).
% 49.54/29.20 thf(1048,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((~ (countable_Set_cin @ TA @ A @ B)) => ((minus_minus @ (countable_Set_cset @ TA) @ (counta2111716221insert @ TA @ A @ B) @ (counta2111716221insert @ TA @ A @ (bot_bot @ (countable_Set_cset @ TA)))) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 49.54/29.20 thf(10,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_186_antisym__conv3)).
% 49.54/29.20 thf(318,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)],[10])).
% 49.54/29.20 thf(101,axiom,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_eq__iff)).
% 49.54/29.20 thf(599,plain,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 49.54/29.20 thf(25,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_240_diff__eq__diff__less)).
% 49.54/29.20 thf(362,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)],[25])).
% 49.54/29.20 thf(52,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_order_Ostrict__implies__order)).
% 49.54/29.20 thf(451,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 49.54/29.20 thf(73,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TB),B:(TA > TD),C:(TA > TB),D:(TB > TC)]: (((comp @ TD @ TB @ TA @ A @ B) = C) => ((comp @ TD @ TC @ TA @ (comp @ TB @ TC @ TD @ D @ A) @ B) = (comp @ TB @ TC @ TA @ D @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_rewriteR__comp__comp)).
% 49.54/29.20 thf(509,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TB),B:(TA > TD),C:(TA > TB),D:(TB > TC)]: (((comp @ TD @ TB @ TA @ A @ B) = (C)) => ((comp @ TD @ TC @ TA @ (comp @ TB @ TC @ TD @ D @ A) @ B) = (comp @ TB @ TC @ TA @ D @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 49.54/29.20 thf(191,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((monomo955616121nondet @ TA @ TB @ TC) = (^ [A:((countable_Set_cset @ TA) > ((TA > TB) > TB)),B:(countable_Set_cset @ TA),C:(TA > (monomo1453983439ondetT @ TC @ TB))]: (monomo1975189248ondetT @ TB @ TC @ (A @ B @ (comp @ (monomo1453983439ondetT @ TC @ TB) @ TB @ TA @ (monomo603716163nondet @ TC @ TB) @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_cset__nondetM__base_Oaltc__nondet__def)).
% 49.54/29.20 thf(880,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((monomo955616121nondet @ TA @ TB @ TC) = (^ [A:((countable_Set_cset @ TA) > ((TA > TB) > TB)),B:(countable_Set_cset @ TA),C:(TA > (monomo1453983439ondetT @ TC @ TB))]: (monomo1975189248ondetT @ TB @ TC @ (A @ B @ (comp @ (monomo1453983439ondetT @ TC @ TB) @ TB @ TA @ (monomo603716163nondet @ TC @ TB) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 49.54/29.20 thf(246,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:TA]: ((countable_Set_cin @ TA @ A @ B) => (countable_Set_cin @ TA @ A @ (counta2111716221insert @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_cinsertI2)).
% 49.54/29.20 thf(1043,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:TA]: ((countable_Set_cin @ TA @ A @ B) => (countable_Set_cin @ TA @ A @ (counta2111716221insert @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 49.54/29.20 thf(61,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((ord_less_eq @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB)]: ! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_le__fun__def)).
% 49.54/29.20 thf(477,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((ord_less_eq @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB)]: ! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 49.54/29.20 thf(259,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((countable_Set_cin @ TA @ C @ A) => (countable_Set_cin @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_csubsetD)).
% 49.54/29.20 thf(1080,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((countable_Set_cin @ TA @ C @ A) => (countable_Set_cin @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 49.54/29.20 thf(19,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((! [C:TA]: ((countable_Set_cin @ TA @ C @ A) = (countable_Set_cin @ TA @ C @ B))) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_cset__eqI)).
% 49.54/29.20 thf(345,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((! [C:TA]: ((countable_Set_cin @ TA @ C @ A) = (countable_Set_cin @ TA @ C @ B))) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 49.54/29.20 thf(168,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_61_minus__apply)).
% 49.54/29.20 thf(816,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)],[168])).
% 49.54/29.20 thf(111,axiom,((bot @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Obot_5)).
% 49.54/29.20 thf(626,plain,((bot @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 49.54/29.20 thf(14,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_linear)).
% 49.54/29.20 thf(330,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 49.54/29.20 thf(179,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ C)) => (~ (countable_Set_cin @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_cDiffD2)).
% 49.54/29.20 thf(848,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ C)) => (~ (countable_Set_cin @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 49.54/29.20 thf(132,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_ord__le__eq__subst)).
% 49.54/29.20 thf(700,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 49.54/29.20 thf(226,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: (ord_less_eq @ (countable_Set_cset @ TA) @ A @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_csubset__refl)).
% 49.54/29.20 thf(983,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: (ord_less_eq @ (countable_Set_cset @ TA) @ A @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 49.54/29.20 thf(217,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((? [B:TA]: (countable_Set_cin @ TA @ B @ A)) = (A != (bot_bot @ (countable_Set_cset @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_ex__cin__conv)).
% 49.54/29.20 thf(959,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((? [B:TA]: (countable_Set_cin @ TA @ B @ A)) = (~ (A = (bot_bot @ (countable_Set_cset @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 49.54/29.20 thf(172,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) = (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_antisym__conv)).
% 49.54/29.20 thf(827,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) = (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 49.54/29.20 thf(192,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA,C:(countable_Set_cset @ TA)]: ((minus_minus @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ C)) = (minus_minus @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ C) @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_cDiff__cinsert)).
% 49.54/29.20 thf(883,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:TA,C:(countable_Set_cset @ TA)]: ((minus_minus @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ B @ C)) = (minus_minus @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ C) @ (counta2111716221insert @ TA @ B @ (bot_bot @ (countable_Set_cset @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 49.54/29.20 thf(104,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_65_diff__eq__diff__eq)).
% 49.54/29.20 thf(608,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)],[104])).
% 49.54/29.20 thf(272,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA),D:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less_eq @ (countable_Set_cset @ TA) @ C @ D) => (ord_less_eq @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ D) @ (minus_minus @ (countable_Set_cset @ TA) @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_cminus__mono)).
% 49.54/29.20 thf(1113,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA),D:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less_eq @ (countable_Set_cset @ TA) @ C @ D) => (ord_less_eq @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ D) @ (minus_minus @ (countable_Set_cset @ TA) @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[272])).
% 49.54/29.20 thf(268,axiom,((! [TA: $tType]: (minus @ (countable_Set_cset @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Countable__Set__Type_Ocset___Groups_Ominus_12)).
% 49.54/29.20 thf(1102,plain,((! [TA: $tType]: (minus @ (countable_Set_cset @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 49.54/29.20 thf(117,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_1_1_T)).
% 49.54/29.20 thf(653,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 49.54/29.20 thf(119,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ C @ D)))) => (ord_less_eq @ TA @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_dense__ge__bounded)).
% 49.54/29.20 thf(658,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ C @ D)))) => (ord_less_eq @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 49.54/29.20 thf(203,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((ord_less @ (countable_Set_cset @ TA) @ A @ B) => ((countable_Set_cin @ TA @ C @ A) => (countable_Set_cin @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_cpsubsetD)).
% 49.54/29.20 thf(912,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((ord_less @ (countable_Set_cset @ TA) @ A @ B) => ((countable_Set_cin @ TA @ C @ A) => (countable_Set_cin @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 49.54/29.20 thf(126,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_less__asym_H)).
% 49.54/29.20 thf(685,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 49.54/29.20 thf(77,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((A = B) => ((countable_Set_cin @ TA @ C @ A) = (countable_Set_cin @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_eqcset__imp__iff)).
% 49.54/29.20 thf(521,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((A = B) => ((countable_Set_cin @ TA @ C @ A) = (countable_Set_cin @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 49.54/29.20 thf(257,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => (ord_less_eq @ (countable_Set_cset @ TA) @ (counta2111716221insert @ TA @ C @ A) @ (counta2111716221insert @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_cinsert__mono)).
% 49.54/29.20 thf(1076,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => (ord_less_eq @ (countable_Set_cset @ TA) @ (counta2111716221insert @ TA @ C @ A) @ (counta2111716221insert @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 49.54/29.20 thf(244,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: (((countable_Set_cin @ TA @ A @ B) => ((minus_minus @ (countable_Set_cset @ TA) @ (counta2111716221insert @ TA @ A @ C) @ B) = (minus_minus @ (countable_Set_cset @ TA) @ C @ B))) & ((~ (countable_Set_cin @ TA @ A @ B)) => ((minus_minus @ (countable_Set_cset @ TA) @ (counta2111716221insert @ TA @ A @ C) @ B) = (counta2111716221insert @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_cinsert__cDiff__if)).
% 49.54/29.20 thf(1034,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: (((countable_Set_cin @ TA @ A @ B) => ((minus_minus @ (countable_Set_cset @ TA) @ (counta2111716221insert @ TA @ A @ C) @ B) = (minus_minus @ (countable_Set_cset @ TA) @ C @ B))) & ((~ (countable_Set_cin @ TA @ A @ B)) => ((minus_minus @ (countable_Set_cset @ TA) @ (counta2111716221insert @ TA @ A @ C) @ B) = (counta2111716221insert @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 49.54/29.20 thf(45,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((monomo410456285nondet @ TA @ TB @ TC) = (^ [A:(TA > (TB > TB)),B:TA,C:(monomo1453983439ondetT @ TC @ TB)]: (monomo1975189248ondetT @ TB @ TC @ (A @ B @ (monomo603716163nondet @ TC @ TB @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_nondetM__base_Oput__nondet__def)).
% 49.54/29.20 thf(426,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((monomo410456285nondet @ TA @ TB @ TC) = (^ [A:(TA > (TB > TB)),B:TA,C:(monomo1453983439ondetT @ TC @ TB)]: (monomo1975189248ondetT @ TB @ TC @ (A @ B @ (monomo603716163nondet @ TC @ TB @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 49.54/29.20 thf(97,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_181_ord__less__eq__trans)).
% 49.54/29.20 thf(589,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)],[97])).
% 49.54/29.20 thf(124,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_66_fun__diff__def)).
% 49.54/29.20 thf(680,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)],[124])).
% 49.54/29.20 thf(120,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_eq @ TA @ A @ B) = (ord_less_eq @ TA @ C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_diff__eq__diff__less__eq)).
% 49.54/29.20 thf(663,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_eq @ TA @ A @ B) = (ord_less_eq @ TA @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 49.54/29.20 thf(30,axiom,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_lt__ex)).
% 49.54/29.20 thf(374,plain,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 49.54/29.20 thf(65,axiom,((! [TA: $tType,TB: $tType]: ((bot @ TA) => (bot @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Obot)).
% 49.54/29.20 thf(487,plain,((! [TA: $tType,TB: $tType]: ((bot @ TA) => (bot @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 49.54/29.20 thf(166,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_202_leD)).
% 49.54/29.20 thf(812,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)],[166])).
% 49.54/29.20 thf(210,axiom,((! [TA: $tType]: (order_bot @ (countable_Set_cset @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Countable__Set__Type_Ocset___Orderings_Oorder__bot_7)).
% 49.54/29.20 thf(939,plain,((! [TA: $tType]: (order_bot @ (countable_Set_cset @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 49.54/29.20 thf(175,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: (ord_less_eq @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ B) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_cDiff__csubset)).
% 49.54/29.20 thf(836,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: (ord_less_eq @ (countable_Set_cset @ TA) @ (minus_minus @ (countable_Set_cset @ TA) @ A @ B) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 49.54/29.20 thf(80,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_164_ord__less__eq__subst)).
% 49.54/29.20 thf(531,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)],[80])).
% 49.54/29.20 thf(212,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ B) => (? [C:(countable_Set_cset @ TA)]: ((B = (counta2111716221insert @ TA @ A @ C)) & ~ (countable_Set_cin @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_mk__disjoint__cinsert)).
% 49.54/29.20 thf(944,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ B) => (? [C:(countable_Set_cset @ TA)]: ((B = (counta2111716221insert @ TA @ A @ C)) & ~ (countable_Set_cin @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 49.54/29.20 thf(154,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TC > TD),B:(TB > TC),C:(TA > TB)]: ((comp @ TB @ TD @ TA @ (comp @ TC @ TD @ TB @ A @ B) @ C) = (comp @ TC @ TD @ TA @ A @ (comp @ TB @ TC @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_comp__assoc)).
% 49.54/29.20 thf(776,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TC > TD),B:(TB > TC),C:(TA > TB)]: ((comp @ TB @ TD @ TA @ (comp @ TC @ TD @ TB @ A @ B) @ C) = (comp @ TC @ TD @ TA @ A @ (comp @ TB @ TC @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 49.54/29.20 thf(78,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_order__trans)).
% 49.54/29.20 thf(525,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 49.54/29.20 thf(94,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_221_le__imp__less__or__eq)).
% 49.54/29.20 thf(580,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)],[94])).
% 49.54/29.20 thf(6,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A = B) | ~ (ord_less_eq @ TA @ A @ B) | ~ (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_verit__la__disequality)).
% 49.54/29.20 thf(295,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A = B) | ~ (ord_less_eq @ TA @ A @ B) | ~ (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 49.54/29.20 thf(13,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)).
% 49.54/29.20 thf(327,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)],[13])).
% 49.54/29.20 thf(38,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_dual__order_Orefl)).
% 49.54/29.20 thf(409,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 49.54/29.20 thf(50,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((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_eq @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_ord__eq__le__subst)).
% 49.54/29.20 thf(441,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((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_eq @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 49.54/29.20 thf(28,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:$o]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ A) => (C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_less__imp__triv)).
% 49.54/29.20 thf(370,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:$o]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ A) => (C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 49.54/29.20 thf(136,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_less__not__sym)).
% 49.54/29.20 thf(717,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 49.54/29.20 thf(17,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less_eq @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_linorder__wlog)).
% 49.54/29.20 thf(338,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less_eq @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 49.54/29.20 thf(165,axiom,((! [TA: $tType,TB: $tType]: (! [A:((monomo1453983439ondetT @ TA @ TB) > $o),B:(monomo1453983439ondetT @ TA @ TB)]: ((! [C:TB]: (A @ (monomo1975189248ondetT @ TB @ TA @ C))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_nondetT_Oinduct)).
% 49.54/29.20 thf(808,plain,((! [TA: $tType,TB: $tType]: (! [A:((monomo1453983439ondetT @ TA @ TB) > $o),B:(monomo1453983439ondetT @ TA @ TB)]: ((! [C:TB]: (A @ (monomo1975189248ondetT @ TB @ TA @ C))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 49.54/29.20 thf(24,axiom,((! [TA: $tType,TB: $tType]: (! [A:(monomo1453983439ondetT @ TA @ TB),B:(monomo1453983439ondetT @ TA @ TB)]: (((monomo603716163nondet @ TA @ TB @ A) = (monomo603716163nondet @ TA @ TB @ B)) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_nondetT_Oexpand)).
% 49.54/29.20 thf(359,plain,((! [TA: $tType,TB: $tType]: (! [A:(monomo1453983439ondetT @ TA @ TB),B:(monomo1453983439ondetT @ TA @ TB)]: (((monomo603716163nondet @ TA @ TB @ A) = (monomo603716163nondet @ TA @ TB @ B)) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 49.54/29.20 thf(83,axiom,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder)).
% 49.54/29.20 thf(544,plain,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 49.54/29.20 thf(58,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_220_le__less__linear)).
% 49.54/29.20 thf(470,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)],[58])).
% 49.54/29.20 thf(93,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_ord__eq__le__trans)).
% 49.54/29.20 thf(576,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 49.54/29.20 thf(118,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ D) => (ord_less_eq @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_diff__mono)).
% 49.54/29.20 thf(656,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ D) => (ord_less_eq @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 49.54/29.20 thf(185,axiom,((! [A:(countable_Set_cset @ c),B:(c > (monomo1453983439ondetT @ a @ m))]: ((monomo955616121nondet @ c @ m @ a @ mergec @ A @ B) = (monomo1975189248ondetT @ m @ a @ (mergec @ A @ (comp @ (monomo1453983439ondetT @ a @ m) @ m @ c @ (monomo603716163nondet @ a @ m) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_altc__nondet__def)).
% 49.54/29.20 thf(864,plain,((! [A:(countable_Set_cset @ c),B:(c > (monomo1453983439ondetT @ a @ m))]: ((monomo955616121nondet @ c @ m @ a @ (mergec) @ A @ (B)) = (monomo1975189248ondetT @ m @ a @ (mergec @ A @ (comp @ (monomo1453983439ondetT @ a @ m) @ m @ c @ (monomo603716163nondet @ a @ m) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 49.54/29.20 thf(265,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ B) => ((minus_minus @ (countable_Set_cset @ TA) @ (counta2111716221insert @ TA @ A @ C) @ B) = (minus_minus @ (countable_Set_cset @ TA) @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_cinsert__cDiff1)).
% 49.54/29.20 thf(1094,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ B) => ((minus_minus @ (countable_Set_cset @ TA) @ (counta2111716221insert @ TA @ A @ C) @ B) = (minus_minus @ (countable_Set_cset @ TA) @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[265])).
% 49.54/29.20 thf(99,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > TB),B:(TB > ((TC > TB) > TB)),C:((countable_Set_cset @ TA) > ((TA > TB) > TB))]: ((monomo439771545d_altc @ TC @ TB @ TA @ A @ B @ C) => (monomo555039548axioms @ TB @ TC @ TA @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_monad__altc_Oaxioms_I2_J)).
% 49.54/29.20 thf(595,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > TB),B:(TB > ((TC > TB) > TB)),C:((countable_Set_cset @ TA) > ((TA > TB) > TB))]: ((monomo439771545d_altc @ TC @ TB @ TA @ (A) @ (B) @ (C)) => (monomo555039548axioms @ TB @ TC @ TA @ (B) @ (C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 49.54/29.20 thf(183,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((ord_less @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less @ (countable_Set_cset @ TA) @ B @ C) => (ord_less @ (countable_Set_cset @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_cpsubset__trans)).
% 49.54/29.20 thf(859,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((ord_less @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less @ (countable_Set_cset @ TA) @ B @ C) => (ord_less @ (countable_Set_cset @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 49.54/29.20 thf(229,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ B) => ((counta2111716221insert @ TA @ A @ B) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_cinsert__absorb)).
% 49.54/29.20 thf(991,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ B) => ((counta2111716221insert @ TA @ A @ B) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 49.54/29.20 thf(112,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_242_diff__strict__right__mono)).
% 49.54/29.20 thf(627,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)],[112])).
% 49.54/29.20 thf(261,axiom,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (bot_bot @ TA) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_bot_Oextremum)).
% 49.54/29.20 thf(1084,plain,((! [TA: $tType]: ((order_bot @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (bot_bot @ TA) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 49.54/29.20 thf(87,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_less__imp__neq)).
% 49.54/29.20 thf(556,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 49.54/29.20 thf(81,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_211_not__less)).
% 49.54/29.20 thf(539,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)],[81])).
% 49.54/29.20 thf(63,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((monomo1564381680ondetT @ TA @ TB @ TC) = (^ [A:(TA > TB),B:(monomo1453983439ondetT @ TC @ TA)]: (A @ (monomo603716163nondet @ TC @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_nondetT_Ocase__eq__if)).
% 49.54/29.20 thf(482,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((monomo1564381680ondetT @ TA @ TB @ TC) = (^ [A:(TA > TB),B:(monomo1453983439ondetT @ TC @ TA)]: (A @ (monomo603716163nondet @ TC @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 49.54/29.20 thf(68,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TA > TB),B:TA]: ((monomo1564381680ondetT @ TA @ TB @ TC @ A @ (monomo1975189248ondetT @ TA @ TC @ B)) = (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_nondetT_Ocase)).
% 49.54/29.20 thf(495,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TA > TB),B:TA]: ((monomo1564381680ondetT @ TA @ TB @ TC @ (A) @ (monomo1975189248ondetT @ TA @ TC @ B)) = (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 49.54/29.20 thf(149,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_dual__order_Ostrict__implies__order)).
% 49.54/29.20 thf(759,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 49.54/29.20 thf(195,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (counta2111716221insert @ TA @ B @ C)) = ((A = B) | (countable_Set_cin @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_cinsert__iff)).
% 49.54/29.20 thf(891,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ (counta2111716221insert @ TA @ B @ C)) = ((A = B) | (countable_Set_cin @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 49.54/29.20 thf(236,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_csubset__cinsertI2)).
% 49.54/29.20 thf(1010,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:TA]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ (counta2111716221insert @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 49.54/29.20 thf(128,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TC),B:(TA > TD),C:(TB > TC),D:(TA > TB),E:TA]: (((comp @ TD @ TC @ TA @ A @ B) = (comp @ TB @ TC @ TA @ C @ D)) => ((A @ (B @ E)) = (C @ (D @ E))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_comp__eq__dest)).
% 49.54/29.20 thf(688,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TC),B:(TA > TD),C:(TB > TC),D:(TA > TB),E:TA]: (((comp @ TD @ TC @ TA @ A @ B) = (comp @ TB @ TC @ TA @ C @ D)) => ((A @ (B @ E)) = (C @ (D @ E))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 49.54/29.20 thf(199,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less @ (countable_Set_cset @ TA) @ B @ C) => (ord_less @ (countable_Set_cset @ TA) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_csubset__cpsubset__trans)).
% 49.54/29.20 thf(903,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less @ (countable_Set_cset @ TA) @ B @ C) => (ord_less @ (countable_Set_cset @ TA) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 49.54/29.20 thf(27,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_less__irrefl)).
% 49.54/29.20 thf(368,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 49.54/29.20 thf(178,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((A = B) => (ord_less_eq @ (countable_Set_cset @ TA) @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_cequalityD2)).
% 49.54/29.20 thf(844,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((A = B) => (ord_less_eq @ (countable_Set_cset @ TA) @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 49.54/29.20 thf(145,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_223_not__le__imp__less)).
% 49.54/29.20 thf(748,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)],[145])).
% 49.54/29.20 thf(140,axiom,((! [TA: $tType,TB: $tType]: (! [A:(monomo1453983439ondetT @ TA @ TB)]: ((monomo1975189248ondetT @ TB @ TA @ (monomo603716163nondet @ TA @ TB @ A)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_nondetT_Ocollapse)).
% 49.54/29.20 thf(731,plain,((! [TA: $tType,TB: $tType]: (! [A:(monomo1453983439ondetT @ TA @ TB)]: ((monomo1975189248ondetT @ TB @ TA @ (monomo603716163nondet @ TA @ TB @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 49.54/29.20 thf(42,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_2_1_T)).
% 49.54/29.20 thf(418,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 49.54/29.20 thf(158,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TC),B:(TA > TD),C:(TB > TC),D:(TA > TB)]: (((comp @ TD @ TC @ TA @ A @ B) = (comp @ TB @ TC @ TA @ C @ D)) => (! [E:TA]: ((A @ (B @ E)) = (C @ (D @ E)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_comp__eq__elim)).
% 49.54/29.20 thf(786,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (! [A:(TD > TC),B:(TA > TD),C:(TB > TC),D:(TA > TB)]: (((comp @ TD @ TC @ TA @ A @ B) = (comp @ TB @ TC @ TA @ C @ D)) => (! [E:TA]: ((A @ (B @ E)) = (C @ (D @ E)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 49.54/29.20 thf(204,axiom,((! [TA: $tType]: (((=) @ (countable_Set_cset @ TA)) = (^ [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) & (ord_less_eq @ (countable_Set_cset @ TA) @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_cset__eq__csubset)).
% 49.54/29.20 thf(914,plain,((! [TA: $tType]: (((=) @ (countable_Set_cset @ TA)) = (^ [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) & (ord_less_eq @ (countable_Set_cset @ TA) @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 49.54/29.20 thf(207,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ B) => (~ (! [C:(countable_Set_cset @ TA)]: ((B = (counta2111716221insert @ TA @ A @ C)) => (countable_Set_cin @ TA @ A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_set__cinsert)).
% 49.54/29.20 thf(929,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ B) => (~ (! [C:(countable_Set_cset @ TA)]: ((B = (counta2111716221insert @ TA @ A @ C)) => (countable_Set_cin @ TA @ A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 49.54/29.20 thf(151,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_order_Otrans)).
% 49.54/29.20 thf(763,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 49.54/29.20 thf(247,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less_eq @ (countable_Set_cset @ TA) @ B @ C) => ((minus_minus @ (countable_Set_cset @ TA) @ B @ (minus_minus @ (countable_Set_cset @ TA) @ C @ A)) = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_double__cDiff)).
% 49.54/29.20 thf(1045,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) => ((ord_less_eq @ (countable_Set_cset @ TA) @ B @ C) => ((minus_minus @ (countable_Set_cset @ TA) @ B @ (minus_minus @ (countable_Set_cset @ TA) @ C @ A)) = A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 49.54/29.20 thf(47,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_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_order__subst2)).
% 49.54/29.20 thf(432,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_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 49.54/29.20 thf(266,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ B) => ((~ (countable_Set_cin @ TA @ A @ C)) => (countable_Set_cin @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_cDiffI)).
% 49.54/29.20 thf(1097,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA),C:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ B) => ((~ (countable_Set_cin @ TA @ A @ C)) => (countable_Set_cin @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 49.54/29.20 thf(232,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:((countable_Set_cset @ TA) > TB),B:(TB > (((countable_Set_cset @ TA) > TB) > TB)),C:((countable_Set_cset @ TA) > ((TA > TB) > TB)),D:((countable_Set_cset @ TC) > ((TC > TB) > TB)),E:(TA > TB)]: ((monomo2011693592ondetM @ TA @ TB @ TC @ A @ B @ C @ D) => ((C @ (bot_bot @ (countable_Set_cset @ TA)) @ E) = (A @ (bot_bot @ (countable_Set_cset @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_cset__nondetM_Omerge__empty)).
% 49.54/29.20 thf(999,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:((countable_Set_cset @ TA) > TB),B:(TB > (((countable_Set_cset @ TA) > TB) > TB)),C:((countable_Set_cset @ TA) > ((TA > TB) > TB)),D:((countable_Set_cset @ TC) > ((TC > TB) > TB)),E:(TA > TB)]: ((monomo2011693592ondetM @ TA @ TB @ TC @ (A) @ (B) @ (C) @ (D)) => ((C @ (bot_bot @ (countable_Set_cset @ TA)) @ (E)) = (A @ (bot_bot @ (countable_Set_cset @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 49.54/29.20 thf(108,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_diff__left__mono)).
% 49.54/29.20 thf(620,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 49.54/29.20 thf(174,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_193_exists__least__iff)).
% 49.54/29.20 thf(833,plain,((! [TA: $tType]: ((wellorder @ TA) => (((?) @ TA) = (^ [A:(TA > $o)]: ? [B:TA]: ((A @ B) & ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (A @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 49.54/29.20 thf(220,axiom,((! [TA: $tType]: (! [A:TA]: ~ (countable_Set_cin @ TA @ A @ (bot_bot @ (countable_Set_cset @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_cempty__iff)).
% 49.54/29.20 thf(967,plain,((! [TA: $tType]: (! [A:TA]: ~ (countable_Set_cin @ TA @ A @ (bot_bot @ (countable_Set_cset @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 49.54/29.20 thf(186,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ B) => ((counta2111716221insert @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ (counta2111716221insert @ TA @ A @ (bot_bot @ (countable_Set_cset @ TA))))) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_cinsert__cDiff)).
% 49.54/29.20 thf(867,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((countable_Set_cin @ TA @ A @ B) => ((counta2111716221insert @ TA @ A @ (minus_minus @ (countable_Set_cset @ TA) @ B @ (counta2111716221insert @ TA @ A @ (bot_bot @ (countable_Set_cset @ TA))))) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 49.54/29.20 thf(1,conjecture,(((monomo955616121nondet @ c @ m @ a @ mergec @ (counta2111716221insert @ c @ x @ (bot_bot @ (countable_Set_cset @ c))) @ f) = (f @ x))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 49.54/29.20 thf(2,negated_conjecture,((~ ((monomo955616121nondet @ c @ m @ a @ mergec @ (counta2111716221insert @ c @ x @ (bot_bot @ (countable_Set_cset @ c))) @ f) = (f @ x)))),inference(neg_conjecture,[status(cth)],[1])).
% 49.54/29.20 thf(273,plain,((~ ((monomo955616121nondet @ c @ m @ a @ (mergec) @ (counta2111716221insert @ c @ x @ (bot_bot @ (countable_Set_cset @ c))) @ (f)) = (f @ x)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 49.54/29.20 thf(197,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ (bot_bot @ (countable_Set_cset @ TA))) = (A = (bot_bot @ (countable_Set_cset @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_csubset__cempty)).
% 49.54/29.20 thf(897,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ (bot_bot @ (countable_Set_cset @ TA))) = (A = (bot_bot @ (countable_Set_cset @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 49.54/29.20 thf(35,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_dense__le)).
% 49.54/29.20 thf(400,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 49.54/29.20 thf(253,axiom,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((counta2111716221insert @ TA @ A @ (counta2111716221insert @ TA @ A @ B)) = (counta2111716221insert @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_cinsert__absorb2)).
% 49.54/29.20 thf(1065,plain,((! [TA: $tType]: (! [A:TA,B:(countable_Set_cset @ TA)]: ((counta2111716221insert @ TA @ A @ (counta2111716221insert @ TA @ A @ B)) = (counta2111716221insert @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 49.54/29.20 thf(131,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_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_order__subst1)).
% 49.54/29.20 thf(696,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_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 49.54/29.20 thf(215,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((minus_minus @ (countable_Set_cset @ TA) @ A @ A) = (bot_bot @ (countable_Set_cset @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_cDiff__cancel)).
% 49.54/29.20 thf(955,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((minus_minus @ (countable_Set_cset @ TA) @ A @ A) = (bot_bot @ (countable_Set_cset @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 49.54/29.20 thf(193,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less @ (countable_Set_cset @ TA) @ A @ B) => (? [C:TA]: (countable_Set_cin @ TA @ C @ (minus_minus @ (countable_Set_cset @ TA) @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_cpsubset__imp__ex__fmem)).
% 49.54/29.20 thf(886,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less @ (countable_Set_cset @ TA) @ A @ B) => (? [C:TA]: (countable_Set_cin @ TA @ C @ (minus_minus @ (countable_Set_cset @ TA) @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 49.54/29.20 thf(5,axiom,((order @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder_3)).
% 49.54/29.20 thf(294,plain,((order @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 49.54/29.20 thf(162,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB)]: ((! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))) => (ord_less_eq @ (TA > TB) @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_le__funI)).
% 49.54/29.20 thf(801,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB)]: ((! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))) => (ord_less_eq @ (TA > TB) @ (A) @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 49.54/29.20 thf(139,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > (TB > TB)),B:TC,C:(monomo1453983439ondetT @ TA @ TB)]: ((monomo603716163nondet @ TA @ TB @ (monomo410456285nondet @ TC @ TB @ TA @ A @ B @ C)) = (A @ B @ (monomo603716163nondet @ TA @ TB @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_nondetM__base_Orun__put__nondet)).
% 49.54/29.20 thf(728,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (! [A:(TC > (TB > TB)),B:TC,C:(monomo1453983439ondetT @ TA @ TB)]: ((monomo603716163nondet @ TA @ TB @ (monomo410456285nondet @ TC @ TB @ TA @ (A) @ B @ C)) = (A @ B @ (monomo603716163nondet @ TA @ TB @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 49.54/29.20 thf(56,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_order_Ostrict__implies__not__eq)).
% 49.54/29.20 thf(464,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 49.54/29.20 thf(15,axiom,((! [TA: $tType]: ((ord @ TA) => ((ord_less_eq @ ($o > TA)) = (^ [A:($o > TA),B:($o > TA)]: ((ord_less_eq @ TA @ (A @ ($false)) @ (B @ ($false))) & (ord_less_eq @ TA @ (A @ ($true)) @ (B @ ($true))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_le__rel__bool__arg__iff)).
% 49.54/29.20 thf(332,plain,((! [TA: $tType]: ((ord @ TA) => ((ord_less_eq @ ($o > TA)) = (^ [A:($o > TA),B:($o > TA)]: ((ord_less_eq @ TA @ (A @ ($false)) @ (B @ ($false))) & (ord_less_eq @ TA @ (A @ ($true)) @ (B @ ($true))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 49.54/29.20 thf(114,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_227_order_Ostrict__iff__order)).
% 49.54/29.20 thf(644,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)],[114])).
% 49.54/29.20 thf(201,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less @ (countable_Set_cset @ TA) @ A @ B) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_cpsubset__imp__fsubset)).
% 49.54/29.20 thf(908,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less @ (countable_Set_cset @ TA) @ A @ B) => (ord_less_eq @ (countable_Set_cset @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 49.54/29.20 thf(138,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ D @ C)))) => (ord_less_eq @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_dense__le__bounded)).
% 49.54/29.20 thf(723,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ D @ C)))) => (ord_less_eq @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 49.54/29.20 thf(170,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_214_antisym__conv2)).
% 49.54/29.20 thf(822,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)],[170])).
% 49.54/29.20 thf(180,axiom,((! [TA: $tType]: ((ord_less @ (countable_Set_cset @ TA)) = (^ [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) & (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_less__cset__def)).
% 49.54/29.20 thf(850,plain,((! [TA: $tType]: ((ord_less @ (countable_Set_cset @ TA)) = (^ [A:(countable_Set_cset @ TA),B:(countable_Set_cset @ TA)]: ((ord_less_eq @ (countable_Set_cset @ TA) @ A @ B) & ~ (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 49.54/29.20 thf(234,axiom,((! [A:c,B:(c > m)]: ((mergec @ (counta2111716221insert @ c @ A @ (bot_bot @ (countable_Set_cset @ c))) @ B) = (B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_mergec__single)).
% 49.54/29.20 thf(1004,plain,((! [A:c,B:(c > m)]: ((mergec @ (counta2111716221insert @ c @ A @ (bot_bot @ (countable_Set_cset @ c))) @ (B)) = (B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 49.54/29.20 thf(129,axiom,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_order__class_Oorder_Oeq__iff)).
% 49.54/29.20 thf(691,plain,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 49.54/29.20 thf(70,axiom,((! [TA: $tType,TB: $tType]: ((order_bot @ TA) => (order_bot @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder__bot)).
% 49.54/29.20 thf(501,plain,((! [TA: $tType,TB: $tType]: ((order_bot @ TA) => (order_bot @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 49.54/29.20 thf(163,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_diff__right__mono)).
% 49.54/29.20 thf(803,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 49.54/29.20 thf(88,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_less__imp__not__less)).
% 49.54/29.20 thf(560,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 49.54/29.20 thf(133,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_254_minf_I8_J)).
% 49.54/29.20 thf(708,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 49.54/29.20 thf(238,axiom,((! [TA: $tType]: (! [A:(TA > (m > m)),B:TA,C:(monomo1453983439ondetT @ a @ m)]: ((monomo603716163nondet @ a @ m @ (monomo410456285nondet @ TA @ m @ a @ A @ B @ C)) = (A @ B @ (monomo603716163nondet @ a @ m @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_run__put__nondet)).
% 49.54/29.20 thf(1014,plain,((! [TA: $tType]: (! [A:(TA > (m > m)),B:TA,C:(monomo1453983439ondetT @ a @ m)]: ((monomo603716163nondet @ a @ m @ (monomo410456285nondet @ TA @ m @ a @ (A) @ B @ C)) = (A @ B @ (monomo603716163nondet @ a @ m @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 49.54/29.20 thf(222,axiom,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((! [B:TA]: ~ (countable_Set_cin @ TA @ B @ A)) = (A = (bot_bot @ (countable_Set_cset @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_all__not__cin__conv)).
% 49.54/29.20 thf(972,plain,((! [TA: $tType]: (! [A:(countable_Set_cset @ TA)]: ((! [B:TA]: ~ (countable_Set_cin @ TA @ B @ A)) = (A = (bot_bot @ (countable_Set_cset @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 49.54/29.20 thf(1118,plain,(($false)),inference(e,[status(thm)],[629,1024,365,1031,941,666,1110,962,468,977,683,276,1068,994,741,379,878,597,861,873,449,1078,550,797,472,814,747,670,404,841,301,565,436,651,719,785,372,838,917,344,934,1059,949,542,460,853,969,416,316,421,870,475,492,756,789,376,623,485,348,353,1051,1040,321,905,480,602,734,453,774,1104,507,527,397,687,411,988,1074,439,678,925,761,714,1057,546,793,910,894,1091,825,1021,952,407,429,275,1027,710,324,1012,583,830,519,1089,1017,615,356,593,783,1082,489,554,753,622,393,515,738,457,1002,569,779,647,997,1099,985,503,605,1086,805,1071,586,888,765,1054,298,618,513,856,573,965,750,819,423,875,958,413,562,975,1007,694,936,611,498,1107,335,350,979,900,1048,318,599,362,451,509,880,1043,477,1080,345,816,626,330,848,700,983,959,827,883,608,1113,1102,653,658,912,685,521,1076,1034,426,589,680,663,374,487,812,939,836,531,944,776,525,580,295,327,409,441,370,717,338,808,359,544,470,576,656,864,1094,595,859,991,627,1084,556,539,482,495,759,891,1010,688,903,368,844,748,731,418,786,914,929,763,1045,432,1097,999,620,833,967,867,273,897,400,1065,696,955,886,294,801,728,464,332,644,908,723,822,850,1004,691,501,803,560,708,1014,972])).
% 49.54/29.20 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 49.54/29.20 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------