%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP132^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:06:53 AM UTC 2026
% Result : Theorem 225.20s 125.10s
% Output : Refutation 226.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP132^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.11/0.22 % Computer : n001.cluster.edu
% 0.11/0.22 % Model : x86_64 x86_64
% 0.11/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.22 % Memory : 8046.5625MB
% 0.11/0.22 % OS : Linux 6.8.0-71-generic
% 0.11/0.22 % CPULimit : 300
% 0.11/0.22 % WCLimit : 300
% 0.11/0.22 % DateTime : Tue Sep 29 20:04:36 UTC 2026
% 0.11/0.22 % CPUTime :
% 0.11/0.22 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.89/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.40/1.22 % [INFO] Parsing done (423ms).
% 2.40/1.24 % [INFO] Running in sequential loop mode.
% 3.58/1.62 % [INFO] eprover registered as external prover.
% 3.58/1.63 % [INFO] Scanning for conjecture ...
% 3.78/1.79 % [INFO] Found a conjecture (or negated_conjecture) and 299 axioms. Running axiom selection ...
% 4.30/1.95 % [INFO] Axiom selection finished. Selected 295 axioms (removed 4 axioms).
% 5.33/2.26 % [INFO] Problem is higher-order (TPTP THF).
% 5.33/2.29 % [INFO] Type checking passed.
% 5.72/2.30 % [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 ...
% 225.20/125.09 % External prover 'e' found a proof!
% 225.20/125.09 % [INFO] Killing All external provers ...
% 225.20/125.09 % Time passed: 124728ms (effective reasoning time: 123850ms)
% 225.20/125.09 % 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)>
% 225.20/125.10 % Axioms used in derivation (295): fact_116_mult__nonpos__nonneg, fact_55_inf__period_I1_J, fact_180_fun__upd__def, fact_62_lambda__one, fact_40_sum__mono, tcon_fun___Groups_Ominus, fact_186_right__diff__distrib, fact_179_fun__upd__eqD, fact_61_order__refl, fact_242_order__less__subst2, fact_70_mult__cancel__left, fact_206_nat__0__less__mult__iff, tcon_Nat_Onat___Orderings_Oorder_2, fact_204_nat__mult__less__cancel__disj, fact_16_nat__mult__eq__1__iff, fact_189_comm__monoid__mult__class_Omult__1, tcon_Nat_Onat___Rings_Ocomm__semiring__1__cancel, fact_127_zero__le__square, tcon_Nat_Onat___Orderings_Ono__top, fact_132_zero__le__one, tcon_Nat_Onat___Groups_Ocomm__monoid__diff, fact_14_atMost__iff, tcon_Nat_Onat___Orderings_Olinorder, fact_217_less__imp__not__less, fact_58_fun__upd__upd, fact_213_not__less__iff__gr__or__eq, fact_125_mult__left__mono__neg, fact_210_linorder__neqE__linordered__idom, tcon_Nat_Onat___Rings_Odvd, tcon_Nat_Onat___Groups_Ocancel__comm__monoid__add, fact_64_partitionsI, fact_246_less__numeral__extra_I3_J, fact_25_partitions__bounds, fact_28_diff__le__self, fact_221_less__imp__triv, fact_57_mult_Oleft__neutral, fact_233_less__asym_H, fact_149_ord__eq__le__trans, fact_244_ord__less__eq__subst, tcon_Nat_Onat___Rings_Ozero__neq__one, fact_100_mult__right__cancel, fact_220_linorder__cases, fact_112_mult__0, tcon_fun___Orderings_Oord, fact_23_Nat_Oex__has__greatest__nat, fact_224_less__induct, fact_227_dual__order_Oasym, fact_216_exists__least__iff, fact_218_order_Ostrict__trans, fact_102_zero__neq__one, fact_103_lambda__zero, tcon_Nat_Onat___Rings_Osemiring__no__zero__divisors, fact_10_diff__mult__distrib, fact_75_diff__zero, fact_176_fun__upd__other, fact_208_nat__mult__le__cancel__disj, fact_197_le__numeral__extra_I3_J, fact_89_mult__cancel__left2, fact_191_diff__numeral__special_I9_J, fact_188_right__diff__distrib_H, fact_5_calculation, fact_158_eq__iff, tcon_Nat_Onat___Groups_Ocomm__monoid__mult, fact_3_minus__apply, fact_237_order_Oasym, fact_142_dual__order_Oeq__iff, fact_41_atMost__def, tcon_HOL_Obool___Groups_Ominus_13, tcon_Nat_Onat___Rings_Olinordered__nonzero__semiring, fact_137_mult__left__le__one__le, fact_241_lt__ex, fact_113_ordered__comm__semiring__class_Ocomm__mult__left__mono, tcon_Nat_Onat___Rings_Oordered__semiring, fact_130_le__iff__diff__le__0, fact_129_mult__mono, tcon_Nat_Onat___Groups_Ocomm__monoid__add, fact_161_order__subst2, fact_195_nat__mult__eq__cancel__disj, fact_81_mult__is__0, fact_231_less__linear, tcon_Nat_Onat___Groups_Oone, fact_173_one__reorient, fact_167_ab__semigroup__mult__class_Omult__ac_I1_J, fact_56_mult_Oright__neutral, fact_247_less__numeral__extra_I4_J, fact_131_not__one__le__zero, fact_11_diff__mult__distrib2, fact_13_atMost__subset__iff, fact_17_nat__1__eq__mult__iff, fact_12_inf__period_I2_J, tcon_Nat_Onat___Groups_Oab__semigroup__mult, fact_46_Collect__mem__eq, fact_166_le__funD, fact_141_dual__order_Oantisym, fact_177_fun__upd__same, fact_209_mult__le__cancel2, fact_63_partitions__def, fact_24_bounded__Max__nat, fact_120_mult__le__0__iff, tcon_HOL_Obool___Orderings_Oorder_11, fact_147_order__class_Oorder_Oantisym, tcon_HOL_Obool___Orderings_Olinorder_10, tcon_Nat_Onat___Groups_Ominus_4, fact_140_mult__eq__self__implies__10, fact_108_le__0__eq, fact_199_bot__nat__0_Onot__eq__extremum, fact_37_le__cube, fact_19_le__trans, fact_22_nat__le__linear, fact_182_diff__left__mono, fact_136_mult__right__le__one__le, fact_225_less__not__sym, fact_150_order__class_Oorder_Oeq__iff, fact_226_less__imp__not__eq, tcon_Nat_Onat___Rings_Osemiring__no__zero__divisors__cancel, fact_76_cancel__comm__monoid__add__class_Odiff__cancel, fact_164_le__funI, fact_15_diff__diff__cancel, fact_27_le__diff__iff_H, fact_155_eq__refl, fact_36_le__square, fact_172_cancel__ab__semigroup__add__class_Odiff__right__commute, fact_198_not__gr__zero, fact_53_diff__commute, fact_169_mult_Ocommute, fact_98_no__zero__divisors, fact_187_left__diff__distrib_H, fact_92_diff__is__0__eq, fact_79_diff__0__eq__0, fact_235_less__imp__neq, tcon_Set_Oset___Orderings_Oorder_6, fact_67_mult__zero__left, fact_110_diffs0__imp__equal, fact_2_atMost__eq__iff, tcon_Nat_Onat___Groups_Ozero, fact_230_less__irrefl, fact_107_bot__nat__0_Oextremum__unique, tcon_Nat_Onat___Orderings_Owellorder, fact_86_diff__ge__0__iff__ge, fact_65_partitionsE, fact_160_ord__eq__le__subst, fact_145_dual__order_Orefl, fact_215_linorder__less__wlog, fact_59_fun__upd__triv, fact_51_sum_Oeq__general, tcon_Nat_Onat___Groups_Omonoid__mult, fact_45_mem__Collect__eq, fact_123_mult__left__mono, fact_146_order__trans, tcon_Set_Oset___Orderings_Oord_7, fact_202_diff__gt__0__iff__gt, fact_60_fun__upd__apply, fact_72_diff__self, fact_135_mult__le__one, fact_29_diff__le__mono, fact_229_ord__eq__less__trans, fact_99_mult__left__cancel, fact_243_order__less__subst1, fact_30_Nat_Odiff__diff__eq, fact_0_partitions, fact_71_mult__cancel__right, fact_239_neqE, fact_168_mult_Oassoc, fact_96_mult__not__zero, fact_184_diff__eq__diff__less__eq, fact_91_diff__is__0__eq_H, fact_26_diff__le__mono2, fact_32_eq__diff__iff, tcon_Nat_Onat___Orderings_Oord_3, fact_49_sum_Oreindex__bij__witness, fact_104_sum_Oneutral, fact_232_less__trans, tcon_HOL_Obool___Orderings_Opreorder_9, fact_185_left__diff__distrib, fact_97_divisors__zero, fact_66_le__zero__eq, fact_174_fun__upd__idem__iff, fact_69_mult__eq__0__iff, fact_47_Collect__cong, fact_33_mult__le__mono2, fact_193_subset__antisym, fact_207_less__one, tcon_Nat_Onat___Groups_Ocancel__ab__semigroup__add, tcon_Nat_Onat___Rings_Omult__zero, tcon_Nat_Onat___Rings_Oordered__semiring__0, fact_133_partitions__zero, fact_156_linear, fact_152_le__cases3, fact_196_le__numeral__extra_I4_J, fact_119_split__mult__neg__le, fact_205_mult__less__cancel2, fact_95_zero__le, fact_38_nat__mult__1__right, fact_163_le__fun__def, fact_159_ord__le__eq__subst, fact_122_mult__right__mono__neg, fact_170_mult_Oleft__commute, fact_228_ord__less__eq__trans, fact_214_dual__order_Ostrict__trans, fact_73_diff__0__right, fact_138_sum__nonpos, fact_236_dense, fact_148_ord__le__eq__trans, fact_80_diff__self__eq__0, fact_128_mult__mono_H, fact_109_less__eq__nat_Osimps_I1_J, fact_54_sum_Oswap, fact_175_fun__upd__twist, fact_124_mult__nonpos__nonpos, fact_21_le__antisym, tcon_fun___Orderings_Opreorder, fact_200_less__nat__zero__code, fact_245_ord__eq__less__subst, fact_134_mult__left__le, fact_35_mult__le__mono, fact_83_mult__cancel1, fact_203_zero__less__diff, fact_157_antisym, tcon_Nat_Onat___Orderings_Opreorder_1, fact_126_split__mult__pos__le, fact_181_diff__mono, fact_201_neq0__conv, fact_252_nat__less__induct, fact_18_le__refl, fact_42_sum__subtractf__nat, fact_101_eq__iff__diff__eq__0, fact_248_infinite__descent__measure, fact_117_mult__nonneg__nonpos, fact_139_sum__nonneg, fact_219_dual__order_Oirrefl, fact_238_neq__iff, fact_106_bot__nat__0_Oextremum__uniqueI, fact_78_le0, fact_8_sum__distrib__left, tcon_Nat_Onat___Rings_Osemiring__0, fact_153_order_Otrans, fact_118_mult__nonneg__nonneg, fact_90_mult__cancel__left1, fact_77_bot__nat__0_Oextremum, fact_9_sum__distrib__right, fact_105_sum_Onot__neutral__contains__not__neutral, fact_20_eq__imp__le, tcon_Nat_Onat___Rings_Oordered__comm__semiring, tcon_fun___Orderings_Oorder, fact_74_zero__diff, fact_115_mult__nonneg__nonpos2, fact_4__092_060open_062_I_092_060Sum_062i_092_060le_062n_A_N_Ak_O_A_Ip_Ik_A_058_061_Ap_Ak_A_N_A1_J_J_Ai_A_K_Ai_J_A_061_A_I_092_060Sum_062i_092_060le_062n_O_A_Ip_Ik_A_058_061_Ap_Ak_A_N_A1_J_J_Ai_A_K_Ai_J_092_060close_062, fact_7_sum__product, fact_143_dual__order_Otrans, fact_111_minus__nat_Odiff__0, tcon_Nat_Onat___Groups_Osemigroup__mult, fact_165_le__funE, fact_43_partitions__parts__bounded, fact_194_partitions__remove1__bounds, fact_68_mult__zero__right, tcon_Nat_Onat___Groups_Ocanonically__ordered__monoid__add, fact_6_sum__subtractf, fact_1__092_060open_062k_A_092_060le_062_An_092_060close_062, fact_82_mult__0__right, fact_94_zero__reorient, fact_84_mult__cancel2, tcon_HOL_Obool___Orderings_Oord_12, fact_251_infinite__descent, tcon_Set_Oset___Orderings_Opreorder_5, fact_151_antisym__conv, fact_249_measure__induct__rule, fact_52_sum_Ocong, fact_212_order_Ostrict__implies__not__eq, fact_178_fun__upd__idem, fact_34_mult__le__mono1, fact_183_diff__right__mono, fact_223_antisym__conv3, fact_31_le__diff__iff, fact_44_fun__diff__def, fact_222_less__imp__not__eq2, fact_93_gr0, fact_88_mult__cancel__right1, fact_162_order__subst1, fact_87_mult__cancel__right2, fact_50_sum_Oeq__general__inverses, fact_250_linorder__neqE__nat, fact_171_diff__eq__diff__eq, fact_190_mult_Ocomm__neutral, fact_144_linorder__wlog, fact_240_gt__ex, fact_234_less__asym, fact_211_dual__order_Ostrict__implies__not__eq, tcon_Nat_Onat___Groups_Oordered__comm__monoid__add, fact_121_mult__right__mono, fact_114_zero__le__mult__iff, fact_154_le__cases, fact_39_nat__mult__1, fact_192_subsetI, fact_85_sum_Oneutral__const, tcon_Set_Oset___Groups_Ominus_8
% 225.20/125.10 % No. of inferences in proof: 599
% 225.20/125.10 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 124728 ms resp. 123850 ms w/o parsing
% 226.10/125.33 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 226.10/125.33 thf(nat_type, type, nat: $tType).
% 226.10/125.33 thf(dvd_decl, type, dvd: !> [TA: $tType]: $o).
% 226.10/125.33 thf(one_decl, type, one: !> [TA: $tType]: $o).
% 226.10/125.33 thf(ring_decl, type, ring: !> [TA: $tType]: $o).
% 226.10/125.33 thf(zero_decl, type, zero: !> [TA: $tType]: $o).
% 226.10/125.33 thf(minus_decl, type, minus: !> [TA: $tType]: $o).
% 226.10/125.33 thf(ord_decl, type, ord: !> [TA: $tType]: $o).
% 226.10/125.33 thf(neg_numeral_decl, type, neg_numeral: !> [TA: $tType]: $o).
% 226.10/125.33 thf(order_decl, type, order: !> [TA: $tType]: $o).
% 226.10/125.33 thf(comm_ring_decl, type, comm_ring: !> [TA: $tType]: $o).
% 226.10/125.33 thf(mult_zero_decl, type, mult_zero: !> [TA: $tType]: $o).
% 226.10/125.33 thf(group_add_decl, type, group_add: !> [TA: $tType]: $o).
% 226.10/125.33 thf(no_bot_decl, type, no_bot: !> [TA: $tType]: $o).
% 226.10/125.33 thf(no_top_decl, type, no_top: !> [TA: $tType]: $o).
% 226.10/125.33 thf(semiring_0_decl, type, semiring_0: !> [TA: $tType]: $o).
% 226.10/125.33 thf(monoid_mult_decl, type, monoid_mult: !> [TA: $tType]: $o).
% 226.10/125.33 thf(linorder_decl, type, linorder: !> [TA: $tType]: $o).
% 226.10/125.33 thf(preorder_decl, type, preorder: !> [TA: $tType]: $o).
% 226.10/125.33 thf(ordered_ring_decl, type, ordered_ring: !> [TA: $tType]: $o).
% 226.10/125.33 thf(zero_neq_one_decl, type, zero_neq_one: !> [TA: $tType]: $o).
% 226.10/125.33 thf(ab_group_add_decl, type, ab_group_add: !> [TA: $tType]: $o).
% 226.10/125.33 thf(wellorder_decl, type, wellorder: !> [TA: $tType]: $o).
% 226.10/125.33 thf(semigroup_mult_decl, type, semigroup_mult: !> [TA: $tType]: $o).
% 226.10/125.33 thf(dense_order_decl, type, dense_order: !> [TA: $tType]: $o).
% 226.10/125.33 thf(linordered_idom_decl, type, linordered_idom: !> [TA: $tType]: $o).
% 226.10/125.33 thf(linordered_ring_decl, type, linordered_ring: !> [TA: $tType]: $o).
% 226.10/125.33 thf(comm_monoid_add_decl, type, comm_monoid_add: !> [TA: $tType]: $o).
% 226.10/125.33 thf(ordered_semiring_decl, type, ordered_semiring: !> [TA: $tType]: $o).
% 226.10/125.33 thf(comm_monoid_diff_decl, type, comm_monoid_diff: !> [TA: $tType]: $o).
% 226.10/125.33 thf(comm_monoid_mult_decl, type, comm_monoid_mult: !> [TA: $tType]: $o).
% 226.10/125.33 thf(ab_semigroup_mult_decl, type, ab_semigroup_mult: !> [TA: $tType]: $o).
% 226.10/125.33 thf(ordered_semiring_0_decl, type, ordered_semiring_0: !> [TA: $tType]: $o).
% 226.10/125.33 thf(ordered_ab_group_add_decl, type, ordered_ab_group_add: !> [TA: $tType]: $o).
% 226.10/125.33 thf(ordere1490568538miring_decl, type, ordere1490568538miring: !> [TA: $tType]: $o).
% 226.10/125.33 thf(comm_s1003936772cancel_decl, type, comm_s1003936772cancel: !> [TA: $tType]: $o).
% 226.10/125.33 thf(linord581940658strict_decl, type, linord581940658strict: !> [TA: $tType]: $o).
% 226.10/125.33 thf(cancel1352612707id_add_decl, type, cancel1352612707id_add: !> [TA: $tType]: $o).
% 226.10/125.33 thf(ring_11004092258visors_decl, type, ring_11004092258visors: !> [TA: $tType]: $o).
% 226.10/125.33 thf(cancel146912293up_add_decl, type, cancel146912293up_add: !> [TA: $tType]: $o).
% 226.10/125.33 thf(ordere216010020id_add_decl, type, ordere216010020id_add: !> [TA: $tType]: $o).
% 226.10/125.33 thf(semiri1193490041visors_decl, type, semiri1193490041visors: !> [TA: $tType]: $o).
% 226.10/125.33 thf(linord1659791738miring_decl, type, linord1659791738miring: !> [TA: $tType]: $o).
% 226.10/125.33 thf(canoni770627133id_add_decl, type, canoni770627133id_add: !> [TA: $tType]: $o).
% 226.10/125.33 thf(semiri1923998003cancel_decl, type, semiri1923998003cancel: !> [TA: $tType]: $o).
% 226.10/125.33 thf(fun_upd_decl, type, fun_upd: !> [TA: $tType,TB: $tType]: ((TB > TA) > (TB > (TA > (TB > TA))))).
% 226.10/125.33 thf(minus_minus_decl, type, minus_minus: !> [TA: $tType]: (TA > (TA > TA))).
% 226.10/125.33 thf(one_one_decl, type, one_one: !> [TA: $tType]: TA).
% 226.10/125.33 thf(times_times_decl, type, times_times: !> [TA: $tType]: (TA > (TA > TA))).
% 226.10/125.33 thf(zero_zero_decl, type, zero_zero: !> [TA: $tType]: TA).
% 226.10/125.33 thf(groups1340683514dd_sum_decl, type, groups1340683514dd_sum: !> [TA: $tType,TB: $tType]: ((TB > TA) > ((set @ TB) > TA))).
% 226.10/125.33 thf(if_decl, type, if: !> [TA: $tType]: ($o > (TA > (TA > TA)))).
% 226.10/125.33 thf(number2016821345itions_decl, type, number2016821345itions: ((nat > nat) > (nat > $o))).
% 226.10/125.33 thf(ord_less_decl, type, ord_less: !> [TA: $tType]: (TA > (TA > $o))).
% 226.10/125.33 thf(ord_less_eq_decl, type, ord_less_eq: !> [TA: $tType]: (TA > (TA > $o))).
% 226.10/125.33 thf(collect_decl, type, collect: !> [TA: $tType]: ((TA > $o) > (set @ TA))).
% 226.10/125.33 thf(set_ord_atMost_decl, type, set_ord_atMost: !> [TA: $tType]: (TA > (set @ TA))).
% 226.10/125.33 thf(member_decl, type, member: !> [TA: $tType]: (TA > ((set @ TA) > $o))).
% 226.10/125.33 thf(k_decl, type, k: nat).
% 226.10/125.33 thf(n_decl, type, n: nat).
% 226.10/125.33 thf(p_decl, type, p: (nat > nat)).
% 226.10/125.33 thf(278,axiom,((! [TA: $tType]: ((ordered_ring @ TA) => (! [A:TA,B:TA]: ((((ord_less_eq @ TA @ (zero_zero @ TA) @ A) & (ord_less_eq @ TA @ (zero_zero @ TA) @ B)) | ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) & (ord_less_eq @ TA @ B @ (zero_zero @ TA)))) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_split__mult__pos__le)).
% 226.10/125.33 thf(1168,plain,((! [TA: $tType]: ((ordered_ring @ TA) => (! [A:TA,B:TA]: ((((ord_less_eq @ TA @ (zero_zero @ TA) @ A) & (ord_less_eq @ TA @ (zero_zero @ TA) @ B)) | ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) & (ord_less_eq @ TA @ B @ (zero_zero @ TA)))) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 226.10/125.33 thf(23,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_159_ord__le__eq__subst)).
% 226.10/125.33 thf(347,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)],[23])).
% 226.10/125.33 thf(170,axiom,((no_top @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Ono__top)).
% 226.10/125.33 thf(846,plain,((no_top @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 226.10/125.33 thf(17,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (one_one @ TA) @ (one_one @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_less__numeral__extra_I4_J)).
% 226.10/125.33 thf(333,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (one_one @ TA) @ (one_one @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 226.10/125.33 thf(184,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: (ord_less_eq @ TA @ (minus_minus @ TA @ A @ B) @ (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_le__iff__diff__le__0)).
% 226.10/125.33 thf(893,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: (ord_less_eq @ TA @ (minus_minus @ TA @ A @ B) @ (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 226.10/125.33 thf(78,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_229_ord__eq__less__trans)).
% 226.10/125.33 thf(555,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)],[78])).
% 226.10/125.33 thf(253,axiom,((! [TA: $tType]: ((ordered_semiring @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ C) => (ord_less_eq @ TA @ (times_times @ TA @ C @ A) @ (times_times @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_mult__left__mono)).
% 226.10/125.33 thf(1110,plain,((! [TA: $tType]: ((ordered_semiring @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ C) => (ord_less_eq @ TA @ (times_times @ TA @ C @ A) @ (times_times @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 226.10/125.33 thf(243,axiom,((! [A:nat,B:nat]: (((times_times @ nat @ A @ B) = (zero_zero @ nat)) = ((A = (zero_zero @ nat)) | (B = (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_mult__is__0)).
% 226.10/125.33 thf(1083,plain,((! [A:nat,B:nat]: (((times_times @ nat @ A @ B) = (zero_zero @ nat)) = ((A = (zero_zero @ nat)) | (B = (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 226.10/125.33 thf(207,axiom,((ord @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oord_3)).
% 226.10/125.33 thf(962,plain,((ord @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 226.10/125.33 thf(41,axiom,((! [TA: $tType]: (preorder @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Opreorder_5)).
% 226.10/125.33 thf(407,plain,((! [TA: $tType]: (preorder @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 226.10/125.33 thf(408,plain,(! [TA:$tType] : ((preorder @ (set @ TA)))),inference(cnf,[status(esa)],[407])).
% 226.10/125.33 thf(274,axiom,((! [TA: $tType]: ((ab_semigroup_mult @ TA) => ((times_times @ TA) = (^ [A:TA,B:TA]: (times_times @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_mult_Ocommute)).
% 226.10/125.33 thf(1158,plain,((! [TA: $tType]: ((ab_semigroup_mult @ TA) => ((times_times @ TA) = (^ [A:TA,B:TA]: (times_times @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 226.10/125.33 thf(115,axiom,((! [TA: $tType]: ((ordered_semiring_0 @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ A) => ((ord_less_eq @ TA @ B @ (zero_zero @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_mult__nonneg__nonpos)).
% 226.10/125.33 thf(683,plain,((! [TA: $tType]: ((ordered_semiring_0 @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ A) => ((ord_less_eq @ TA @ B @ (zero_zero @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 226.10/125.33 thf(291,axiom,((! [A:nat]: ((ord_less_eq @ nat @ A @ (zero_zero @ nat)) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_le__0__eq)).
% 226.10/125.33 thf(1205,plain,((! [A:nat]: ((ord_less_eq @ nat @ A @ (zero_zero @ nat)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[291])).
% 226.10/125.33 thf(176,axiom,((! [A:(nat > nat)]: ((number2016821345itions @ A @ (zero_zero @ nat)) = (A = (^ [B:nat]: (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_partitions__zero)).
% 226.10/125.33 thf(861,plain,((! [A:(nat > nat)]: ((number2016821345itions @ (A) @ (zero_zero @ nat)) = ((A) = (^ [B:nat]: (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 226.10/125.33 thf(280,axiom,((! [A:nat]: (ord_less_eq @ nat @ (zero_zero @ nat) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_less__eq__nat_Osimps_I1_J)).
% 226.10/125.33 thf(1173,plain,((! [A:nat]: (ord_less_eq @ nat @ (zero_zero @ nat) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[280])).
% 226.10/125.33 thf(52,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((~ (ord_less @ TA @ (zero_zero @ TA) @ A)) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_not__gr__zero)).
% 226.10/125.33 thf(440,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((~ (ord_less @ TA @ (zero_zero @ TA) @ A)) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 226.10/125.33 thf(110,axiom,((! [A:nat,B:nat,C:nat]: ((times_times @ nat @ (minus_minus @ nat @ A @ B) @ C) = (minus_minus @ nat @ (times_times @ nat @ A @ C) @ (times_times @ nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_diff__mult__distrib)).
% 226.10/125.33 thf(655,plain,((! [A:nat,B:nat,C:nat]: ((times_times @ nat @ (minus_minus @ nat @ A @ B) @ C) = (minus_minus @ nat @ (times_times @ nat @ A @ C) @ (times_times @ nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 226.10/125.33 thf(265,axiom,((! [TA: $tType]: ((ordered_semiring_0 @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ A) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ B) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_mult__nonneg__nonneg)).
% 226.10/125.33 thf(1137,plain,((! [TA: $tType]: ((ordered_semiring_0 @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ A) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ B) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[265])).
% 226.10/125.33 thf(76,axiom,((order @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder_11)).
% 226.10/125.33 thf(550,plain,((order @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 226.10/125.33 thf(62,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_162_order__subst1)).
% 226.10/125.33 thf(500,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)],[62])).
% 226.10/125.33 thf(276,axiom,((! [TA: $tType]: ((neg_numeral @ TA) => ((minus_minus @ TA @ (one_one @ TA) @ (one_one @ TA)) = (zero_zero @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_diff__numeral__special_I9_J)).
% 226.10/125.33 thf(1164,plain,((! [TA: $tType]: ((neg_numeral @ TA) => ((minus_minus @ TA @ (one_one @ TA) @ (one_one @ TA)) = (zero_zero @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[276])).
% 226.10/125.33 thf(158,axiom,((! [A:nat,B:nat]: ((A = (times_times @ nat @ A @ B)) => ((B = (one_one @ nat)) | (A = (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_mult__eq__self__implies__10)).
% 226.10/125.33 thf(814,plain,((! [A:nat,B:nat]: ((A = (times_times @ nat @ A @ B)) => ((B = (one_one @ nat)) | (A = (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 226.10/125.33 thf(191,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA]: ((member @ TA @ A @ (set_ord_atMost @ TA @ B)) = (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_atMost__iff)).
% 226.10/125.33 thf(913,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA]: ((member @ TA @ A @ (set_ord_atMost @ TA @ B)) = (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 226.10/125.33 thf(201,axiom,((! [TA: $tType]: ((ordered_semiring_0 @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ B) => (ord_less_eq @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_mult__nonpos__nonneg)).
% 226.10/125.33 thf(945,plain,((! [TA: $tType]: ((ordered_semiring_0 @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ B) => (ord_less_eq @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 226.10/125.33 thf(72,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_dual__order_Orefl)).
% 226.10/125.33 thf(538,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 226.10/125.33 thf(197,axiom,((linord1659791738miring @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Olinordered__nonzero__semiring)).
% 226.10/125.33 thf(930,plain,((linord1659791738miring @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 226.10/125.33 thf(288,axiom,((! [TA: $tType]: ((group_add @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((minus_minus @ TA @ A @ B) = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_eq__iff__diff__eq__0)).
% 226.10/125.33 thf(1196,plain,((! [TA: $tType]: ((group_add @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((minus_minus @ TA @ A @ B) = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[288])).
% 226.10/125.33 thf(260,axiom,((comm_s1003936772cancel @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Ocomm__semiring__1__cancel)).
% 226.10/125.33 thf(1127,plain,((comm_s1003936772cancel @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 226.10/125.33 thf(45,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_217_less__imp__not__less)).
% 226.10/125.33 thf(417,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)],[45])).
% 226.10/125.33 thf(164,axiom,((linorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Olinorder)).
% 226.10/125.33 thf(829,plain,((linorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 226.10/125.33 thf(247,axiom,((! [TA: $tType,TB: $tType]: ((ab_group_add @ TB) => (! [A:(TA > TB),B:(TA > TB),C:(set @ TA)]: ((groups1340683514dd_sum @ TA @ TB @ (^ [D:TA]: (minus_minus @ TB @ (A @ D) @ (B @ D))) @ C) = (minus_minus @ TB @ (groups1340683514dd_sum @ TA @ TB @ A @ C) @ (groups1340683514dd_sum @ TA @ TB @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_sum__subtractf)).
% 226.10/125.33 thf(1095,plain,((! [TA: $tType,TB: $tType]: ((ab_group_add @ TB) => (! [A:(TA > TB),B:(TA > TB),C:(set @ TA)]: ((groups1340683514dd_sum @ TA @ TB @ (^ [D:TA]: (minus_minus @ TB @ (A @ D) @ (B @ D))) @ C) = (minus_minus @ TB @ (groups1340683514dd_sum @ TA @ TB @ (A) @ C) @ (groups1340683514dd_sum @ TA @ TB @ (B) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 226.10/125.33 thf(35,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_less__imp__not__eq2)).
% 226.10/125.33 thf(389,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 226.10/125.33 thf(238,axiom,((! [TA: $tType]: ((semiri1193490041visors @ TA) => (! [A:TA,B:TA]: ((A != (zero_zero @ TA)) => ((B != (zero_zero @ TA)) => ((times_times @ TA @ A @ B) != (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_no__zero__divisors)).
% 226.10/125.33 thf(1055,plain,((! [TA: $tType]: ((semiri1193490041visors @ TA) => (! [A:TA,B:TA]: ((~ (A = (zero_zero @ TA))) => ((~ (B = (zero_zero @ TA))) => (~ ((times_times @ TA @ A @ B) = (zero_zero @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 226.10/125.33 thf(147,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((minus_minus @ nat @ A @ B) = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_diff__is__0__eq_H)).
% 226.10/125.33 thf(785,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((minus_minus @ nat @ A @ B) = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 226.10/125.33 thf(29,axiom,((! [TA: $tType]: ((one @ TA) => (! [A:TA]: (((one_one @ TA) = A) = (A = (one_one @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_one__reorient)).
% 226.10/125.33 thf(372,plain,((! [TA: $tType]: ((one @ TA) => (! [A:TA]: (((one_one @ TA) = A) = (A = (one_one @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 226.10/125.33 thf(63,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_158_eq__iff)).
% 226.10/125.33 thf(504,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)],[63])).
% 226.10/125.33 thf(90,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((collect @ TA @ A) = (collect @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_Collect__cong)).
% 226.10/125.33 thf(587,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((collect @ TA @ (A)) = (collect @ TA @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 226.10/125.33 thf(137,axiom,((! [TA: $tType]: ((semiri1193490041visors @ TA) => (! [A:TA,B:TA]: (((times_times @ TA @ A @ B) = (zero_zero @ TA)) => ((A = (zero_zero @ TA)) | (B = (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_divisors__zero)).
% 226.10/125.33 thf(751,plain,((! [TA: $tType]: ((semiri1193490041visors @ TA) => (! [A:TA,B:TA]: (((times_times @ TA @ A @ B) = (zero_zero @ TA)) => ((A = (zero_zero @ TA)) | (B = (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 226.10/125.33 thf(22,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_163_le__fun__def)).
% 226.10/125.33 thf(344,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)],[22])).
% 226.10/125.33 thf(199,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) = (ord_less @ nat @ (zero_zero @ nat) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_neq0__conv)).
% 226.10/125.33 thf(934,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) = (ord_less @ nat @ (zero_zero @ nat) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 226.10/125.33 thf(25,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_224_less__induct)).
% 226.10/125.33 thf(357,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)],[25])).
% 226.10/125.33 thf(159,axiom,((ordere1490568538miring @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Oordered__comm__semiring)).
% 226.10/125.33 thf(817,plain,((ordere1490568538miring @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 226.10/125.33 thf(79,axiom,((! [TA: $tType]: (order @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oorder_6)).
% 226.10/125.33 thf(559,plain,((! [TA: $tType]: (order @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 226.10/125.33 thf(108,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((~ (A @ C)) => (? [D:nat]: ((ord_less @ nat @ D @ C) & ~ (A @ D))))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_infinite__descent)).
% 226.10/125.33 thf(638,plain,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((~ (A @ C)) => (? [D:nat]: ((ord_less @ nat @ D @ C) & ~ (A @ D))))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 226.10/125.33 thf(211,axiom,((! [TA: $tType]: ((ordered_semiring @ 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 @ (zero_zero @ TA) @ B) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ C) => (ord_less_eq @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ D)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_mult__mono)).
% 226.10/125.33 thf(969,plain,((! [TA: $tType]: ((ordered_semiring @ 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 @ (zero_zero @ TA) @ B) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ C) => (ord_less_eq @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 226.10/125.33 thf(226,axiom,((! [TA: $tType]: ((comm_monoid_mult @ TA) => (! [A:TA]: ((times_times @ TA @ A @ (one_one @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_mult_Ocomm__neutral)).
% 226.10/125.33 thf(1013,plain,((! [TA: $tType]: ((comm_monoid_mult @ TA) => (! [A:TA]: ((times_times @ TA @ A @ (one_one @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 226.10/125.33 thf(13,axiom,((minus @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Groups_Ominus_13)).
% 226.10/125.33 thf(325,plain,((minus @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 226.10/125.33 thf(10,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA]: ((fun_upd @ TA @ TB @ A @ B @ (A @ B)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_fun__upd__triv)).
% 226.10/125.33 thf(316,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA]: ((fun_upd @ TA @ TB @ A @ B @ (A @ B)) = (A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 226.10/125.33 thf(195,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_172_cancel__ab__semigroup__add__class_Odiff__right__commute)).
% 226.10/125.33 thf(924,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)],[195])).
% 226.10/125.33 thf(53,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_161_order__subst2)).
% 226.10/125.33 thf(443,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)],[53])).
% 226.10/125.33 thf(252,axiom,((comm_monoid_diff @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocomm__monoid__diff)).
% 226.10/125.33 thf(1109,plain,((comm_monoid_diff @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 226.10/125.33 thf(61,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_152_le__cases3)).
% 226.10/125.33 thf(485,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)],[61])).
% 226.10/125.33 thf(154,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => ((ord_less_eq @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ C @ A)) = (ord_less_eq @ nat @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_le__diff__iff)).
% 226.10/125.33 thf(806,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => ((ord_less_eq @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ C @ A)) = (ord_less_eq @ nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 226.10/125.33 thf(271,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ B @ A) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_le__antisym)).
% 226.10/125.33 thf(1151,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 226.10/125.33 thf(200,axiom,((! [A:(nat > nat),B:nat]: ((number2016821345itions @ A @ B) => (~ ((! [C:nat]: (((A @ C) != (zero_zero @ nat)) => ((ord_less_eq @ nat @ (one_one @ nat) @ C) & (ord_less_eq @ nat @ C @ B)))) => ((groups1340683514dd_sum @ nat @ nat @ (^ [C:nat]: (times_times @ nat @ (A @ C) @ C)) @ (set_ord_atMost @ nat @ B)) != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_partitionsE)).
% 226.10/125.33 thf(937,plain,((! [A:(nat > nat),B:nat]: ((number2016821345itions @ (A) @ B) => (~ ((! [C:nat]: ((~ ((A @ C) = (zero_zero @ nat))) => ((ord_less_eq @ nat @ (one_one @ nat) @ C) & (ord_less_eq @ nat @ C @ B)))) => (~ ((groups1340683514dd_sum @ nat @ nat @ (^ [C:nat]: (times_times @ nat @ (A @ C) @ C)) @ (set_ord_atMost @ nat @ B)) = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 226.10/125.33 thf(180,axiom,((! [TA: $tType]: ((semiri1923998003cancel @ TA) => (! [A:TA,B:TA,C:TA]: (((times_times @ TA @ A @ B) = (times_times @ TA @ A @ C)) = ((A = (zero_zero @ TA)) | (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_mult__cancel__left)).
% 226.10/125.33 thf(877,plain,((! [TA: $tType]: ((semiri1923998003cancel @ TA) => (! [A:TA,B:TA,C:TA]: (((times_times @ TA @ A @ B) = (times_times @ TA @ A @ C)) = ((A = (zero_zero @ TA)) | (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 226.10/125.33 thf(205,axiom,((! [TA: $tType]: ((ring_11004092258visors @ TA) => (! [A:TA,B:TA]: (((times_times @ TA @ A @ B) = A) = ((A = (zero_zero @ TA)) | (B = (one_one @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_mult__cancel__left2)).
% 226.10/125.33 thf(956,plain,((! [TA: $tType]: ((ring_11004092258visors @ TA) => (! [A:TA,B:TA]: (((times_times @ TA @ A @ B) = A) = ((A = (zero_zero @ TA)) | (B = (one_one @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 226.10/125.33 thf(141,axiom,((cancel146912293up_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocancel__ab__semigroup__add)).
% 226.10/125.33 thf(774,plain,((cancel146912293up_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 226.10/125.33 thf(37,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_165_le__funE)).
% 226.10/125.33 thf(396,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)],[37])).
% 226.10/125.33 thf(43,axiom,((! [TA: $tType,TB: $tType]: (! [A:TB,B:TB,C:(TB > TA),D:TA,E:TA]: ((A != B) => ((fun_upd @ TB @ TA @ (fun_upd @ TB @ TA @ C @ A @ D) @ B @ E) = (fun_upd @ TB @ TA @ (fun_upd @ TB @ TA @ C @ B @ E) @ A @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_fun__upd__twist)).
% 226.10/125.33 thf(411,plain,((! [TA: $tType,TB: $tType]: (! [A:TB,B:TB,C:(TB > TA),D:TA,E:TA]: ((~ (A = B)) => ((fun_upd @ TB @ TA @ (fun_upd @ TB @ TA @ C @ A @ D) @ B @ E) = (fun_upd @ TB @ TA @ (fun_upd @ TB @ TA @ C @ B @ E) @ A @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 226.10/125.33 thf(250,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_3_minus__apply)).
% 226.10/125.33 thf(1104,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)],[250])).
% 226.10/125.33 thf(64,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (zero_zero @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_le__numeral__extra_I3_J)).
% 226.10/125.33 thf(507,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (zero_zero @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 226.10/125.33 thf(96,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_220_linorder__cases)).
% 226.10/125.33 thf(602,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)],[96])).
% 226.10/125.33 thf(216,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((semiring_0 @ TC) => (! [A:(TA > TC),B:(set @ TA),C:(TB > TC),D:(set @ TB)]: ((times_times @ TC @ (groups1340683514dd_sum @ TA @ TC @ A @ B) @ (groups1340683514dd_sum @ TB @ TC @ C @ D)) = (groups1340683514dd_sum @ TA @ TC @ (^ [E:TA]: (groups1340683514dd_sum @ TB @ TC @ (^ [F:TB]: (times_times @ TC @ (A @ E) @ (C @ F))) @ D)) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_sum__product)).
% 226.10/125.33 thf(981,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((semiring_0 @ TC) => (! [A:(TA > TC),B:(set @ TA),C:(TB > TC),D:(set @ TB)]: ((times_times @ TC @ (groups1340683514dd_sum @ TA @ TC @ (A) @ B) @ (groups1340683514dd_sum @ TB @ TC @ (C) @ D)) = (groups1340683514dd_sum @ TA @ TC @ (^ [E:TA]: (groups1340683514dd_sum @ TB @ TC @ (^ [F:TB]: (times_times @ TC @ (A @ E) @ (C @ F))) @ D)) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 226.10/125.33 thf(295,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: (((set_ord_atMost @ TA @ A) = (set_ord_atMost @ TA @ B)) = (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_atMost__eq__iff)).
% 226.10/125.33 thf(1215,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: (((set_ord_atMost @ TA @ A) = (set_ord_atMost @ TA @ B)) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[295])).
% 226.10/125.33 thf(106,axiom,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_lt__ex)).
% 226.10/125.33 thf(634,plain,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 226.10/125.33 thf(6,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_234_less__asym)).
% 226.10/125.33 thf(307,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)],[6])).
% 226.10/125.33 thf(32,axiom,((! [TA: $tType]: ((zero_neq_one @ TA) => ((zero_zero @ TA) != (one_one @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_zero__neq__one)).
% 226.10/125.33 thf(380,plain,((! [TA: $tType]: ((zero_neq_one @ TA) => (~ ((zero_zero @ TA) = (one_one @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 226.10/125.33 thf(289,axiom,((! [TA: $tType]: ((mult_zero @ TA) => (! [A:TA]: ((times_times @ TA @ A @ (zero_zero @ TA)) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_mult__zero__right)).
% 226.10/125.33 thf(1199,plain,((! [TA: $tType]: ((mult_zero @ TA) => (! [A:TA]: ((times_times @ TA @ A @ (zero_zero @ TA)) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[289])).
% 226.10/125.33 thf(155,axiom,((comm_monoid_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocomm__monoid__add)).
% 226.10/125.33 thf(810,plain,((comm_monoid_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 226.10/125.33 thf(124,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_182_diff__left__mono)).
% 226.10/125.33 thf(714,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)],[124])).
% 226.10/125.33 thf(152,axiom,((! [TA: $tType]: ((ordered_ring @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ (zero_zero @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ C @ B) @ (times_times @ TA @ C @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_mult__left__mono__neg)).
% 226.10/125.33 thf(798,plain,((! [TA: $tType]: ((ordered_ring @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ (zero_zero @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ C @ B) @ (times_times @ TA @ C @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 226.10/125.33 thf(74,axiom,((! [TA: $tType]: ((linordered_idom @ 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_210_linorder__neqE__linordered__idom)).
% 226.10/125.33 thf(546,plain,((! [TA: $tType]: ((linordered_idom @ 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)],[74])).
% 226.10/125.33 thf(150,axiom,((! [A:nat]: (ord_less_eq @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_le__refl)).
% 226.10/125.33 thf(793,plain,((! [A:nat]: (ord_less_eq @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 226.10/125.33 thf(334,plain,(! [TA:$tType] : ((~ (linord1659791738miring @ TA)) | (~ (ord_less @ TA @ (one_one @ TA) @ (one_one @ TA))))),inference(cnf,[status(esa)],[333])).
% 226.10/125.33 thf(135,axiom,((! [A:nat]: (ord_less_eq @ nat @ (zero_zero @ nat) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_le0)).
% 226.10/125.33 thf(746,plain,((! [A:nat]: (ord_less_eq @ nat @ (zero_zero @ nat) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 226.10/125.33 thf(162,axiom,((! [A:nat,B:nat]: ((A != B) => ((~ (ord_less @ nat @ A @ B)) => (ord_less @ nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_linorder__neqE__nat)).
% 226.10/125.33 thf(825,plain,((! [A:nat,B:nat]: ((~ (A = B)) => ((~ (ord_less @ nat @ A @ B)) => (ord_less @ nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 226.10/125.33 thf(144,axiom,((! [A:nat,B:nat]: (((minus_minus @ nat @ A @ B) = (zero_zero @ nat)) => (((minus_minus @ nat @ B @ A) = (zero_zero @ nat)) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_diffs0__imp__equal)).
% 226.10/125.33 thf(778,plain,((! [A:nat,B:nat]: (((minus_minus @ nat @ A @ B) = (zero_zero @ nat)) => (((minus_minus @ nat @ B @ A) = (zero_zero @ nat)) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 226.10/125.33 thf(233,axiom,((! [TA: $tType]: ((comm_monoid_mult @ TA) => (! [A:TA]: ((times_times @ TA @ (one_one @ TA) @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_comm__monoid__mult__class_Omult__1)).
% 226.10/125.33 thf(1042,plain,((! [TA: $tType]: ((comm_monoid_mult @ TA) => (! [A:TA]: ((times_times @ TA @ (one_one @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 226.10/125.33 thf(94,axiom,((ord @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oord_12)).
% 226.10/125.33 thf(598,plain,((ord @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 226.10/125.33 thf(80,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_142_dual__order_Oeq__iff)).
% 226.10/125.33 thf(561,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)],[80])).
% 226.10/125.33 thf(48,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_243_order__less__subst1)).
% 226.10/125.33 thf(429,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)],[48])).
% 226.10/125.33 thf(148,axiom,((! [TA: $tType]: ((ordered_semiring @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ C) => (ord_less_eq @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_mult__right__mono)).
% 226.10/125.33 thf(788,plain,((! [TA: $tType]: ((ordered_semiring @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ C) => (ord_less_eq @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 226.10/125.33 thf(129,axiom,((! [TA: $tType]: ((linord581940658strict @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)) = (((ord_less_eq @ TA @ (zero_zero @ TA) @ A) & (ord_less_eq @ TA @ (zero_zero @ TA) @ B)) | ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) & (ord_less_eq @ TA @ B @ (zero_zero @ TA))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_zero__le__mult__iff)).
% 226.10/125.33 thf(729,plain,((! [TA: $tType]: ((linord581940658strict @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)) = (((ord_less_eq @ TA @ (zero_zero @ TA) @ A) & (ord_less_eq @ TA @ (zero_zero @ TA) @ B)) | ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) & (ord_less_eq @ TA @ B @ (zero_zero @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 226.10/125.33 thf(105,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_less__imp__neq)).
% 226.10/125.33 thf(630,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 226.10/125.33 thf(192,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) = (ord_less @ nat @ (zero_zero @ nat) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_bot__nat__0_Onot__eq__extremum)).
% 226.10/125.33 thf(916,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) = (ord_less @ nat @ (zero_zero @ nat) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 226.10/125.33 thf(229,axiom,(((groups1340683514dd_sum @ nat @ nat @ (^ [A:nat]: (times_times @ nat @ (fun_upd @ nat @ nat @ p @ k @ (minus_minus @ nat @ (p @ k) @ (one_one @ nat)) @ A) @ A)) @ (set_ord_atMost @ nat @ (minus_minus @ nat @ n @ k))) = (minus_minus @ nat @ (groups1340683514dd_sum @ nat @ nat @ (^ [A:nat]: (times_times @ nat @ (p @ A) @ A)) @ (set_ord_atMost @ nat @ n)) @ k))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_calculation)).
% 226.10/125.33 thf(1032,plain,(((groups1340683514dd_sum @ nat @ nat @ (^ [A:nat]: (times_times @ nat @ (fun_upd @ nat @ nat @ p @ k @ (minus_minus @ nat @ (p @ k) @ (one_one @ nat)) @ A) @ A)) @ (set_ord_atMost @ nat @ (minus_minus @ nat @ n @ k))) = (minus_minus @ nat @ (groups1340683514dd_sum @ nat @ nat @ (^ [A:nat]: (times_times @ nat @ (p @ A) @ A)) @ (set_ord_atMost @ nat @ n)) @ k))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 226.10/125.33 thf(103,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_232_less__trans)).
% 226.10/125.33 thf(625,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)],[103])).
% 226.10/125.33 thf(282,axiom,((! [A:nat]: ((times_times @ nat @ A @ (one_one @ nat)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_nat__mult__1__right)).
% 226.10/125.33 thf(1178,plain,((! [A:nat]: ((times_times @ nat @ A @ (one_one @ nat)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 226.10/125.33 thf(182,axiom,((monoid_mult @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Omonoid__mult)).
% 226.10/125.33 thf(889,plain,((monoid_mult @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 226.10/125.33 thf(114,axiom,((ordere216010020id_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oordered__comm__monoid__add)).
% 226.10/125.33 thf(682,plain,((ordere216010020id_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 226.10/125.33 thf(213,axiom,((zero_neq_one @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Ozero__neq__one)).
% 226.10/125.33 thf(974,plain,((zero_neq_one @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 226.10/125.33 thf(171,axiom,((! [TA: $tType]: ((monoid_mult @ TA) => (! [A:TA]: ((times_times @ TA @ A @ (one_one @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_mult_Oright__neutral)).
% 226.10/125.33 thf(847,plain,((! [TA: $tType]: ((monoid_mult @ TA) => (! [A:TA]: ((times_times @ TA @ A @ (one_one @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 226.10/125.33 thf(82,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TB,C:TA,D:TA]: ((fun_upd @ TB @ TA @ (fun_upd @ TB @ TA @ A @ B @ C) @ B @ D) = (fun_upd @ TB @ TA @ A @ B @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_fun__upd__upd)).
% 226.10/125.33 thf(566,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TB,C:TA,D:TA]: ((fun_upd @ TB @ TA @ (fun_upd @ TB @ TA @ A @ B @ C) @ B @ D) = (fun_upd @ TB @ TA @ A @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 226.10/125.33 thf(173,axiom,((! [TA: $tType]: ((ring_11004092258visors @ TA) => (! [A:TA,B:TA]: ((A = (times_times @ TA @ B @ A)) = ((A = (zero_zero @ TA)) | (B = (one_one @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_mult__cancel__right1)).
% 226.10/125.33 thf(852,plain,((! [TA: $tType]: ((ring_11004092258visors @ TA) => (! [A:TA,B:TA]: ((A = (times_times @ TA @ B @ A)) = ((A = (zero_zero @ TA)) | (B = (one_one @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 226.10/125.33 thf(50,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_le__zero__eq)).
% 226.10/125.33 thf(435,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 226.10/125.33 thf(89,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:TB]: (((A @ B) = C) => ((fun_upd @ TA @ TB @ A @ B @ C) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_fun__upd__idem)).
% 226.10/125.33 thf(583,plain,((! [TA: $tType,TB: $tType]: (! [A:(TA > TB),B:TA,C:TB]: (((A @ B) = C) => ((fun_upd @ TA @ TB @ A @ B @ C) = (A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 226.10/125.33 thf(165,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (times_times @ nat @ A @ C) @ (times_times @ nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_mult__le__mono1)).
% 226.10/125.33 thf(830,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (times_times @ nat @ A @ C) @ (times_times @ nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 226.10/125.33 thf(77,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_148_ord__le__eq__trans)).
% 226.10/125.33 thf(551,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)],[77])).
% 226.10/125.33 thf(261,axiom,((! [TA: $tType]: ((linord581940658strict @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)) = (((ord_less_eq @ TA @ (zero_zero @ TA) @ A) & (ord_less_eq @ TA @ B @ (zero_zero @ TA))) | ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) & (ord_less_eq @ TA @ (zero_zero @ TA) @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_mult__le__0__iff)).
% 226.10/125.33 thf(1128,plain,((! [TA: $tType]: ((linord581940658strict @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)) = (((ord_less_eq @ TA @ (zero_zero @ TA) @ A) & (ord_less_eq @ TA @ B @ (zero_zero @ TA))) | ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) & (ord_less_eq @ TA @ (zero_zero @ TA) @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 226.10/125.33 thf(87,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_223_antisym__conv3)).
% 226.10/125.33 thf(578,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)],[87])).
% 226.10/125.33 thf(268,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (times_times @ nat @ A @ B) @ (times_times @ nat @ A @ C)) = ((ord_less @ nat @ (zero_zero @ nat) @ A) & (ord_less @ nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_nat__mult__less__cancel__disj)).
% 226.10/125.33 thf(1143,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (times_times @ nat @ A @ B) @ (times_times @ nat @ A @ C)) = ((ord_less @ nat @ (zero_zero @ nat) @ A) & (ord_less @ nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 226.10/125.33 thf(100,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ B)) = (B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_mem__Collect__eq)).
% 226.10/125.33 thf(615,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ (B))) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 226.10/125.33 thf(258,axiom,((! [TA: $tType]: ((ab_semigroup_mult @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ (times_times @ TA @ A @ B) @ C) = (times_times @ TA @ A @ (times_times @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_ab__semigroup__mult__class_Omult__ac_I1_J)).
% 226.10/125.33 thf(1121,plain,((! [TA: $tType]: ((ab_semigroup_mult @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ (times_times @ TA @ A @ B) @ C) = (times_times @ TA @ A @ (times_times @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 226.10/125.33 thf(40,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_149_ord__eq__le__trans)).
% 226.10/125.33 thf(403,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)],[40])).
% 226.10/125.33 thf(257,axiom,((! [A:nat]: ((minus_minus @ nat @ A @ A) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_diff__self__eq__0)).
% 226.10/125.33 thf(1118,plain,((! [A:nat]: ((minus_minus @ nat @ A @ A) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 226.10/125.33 thf(15,axiom,((! [TA: $tType,TB: $tType]: (! [A:TA,B:TA,C:(TA > TB),D:TB]: ((A != B) => ((fun_upd @ TA @ TB @ C @ B @ D @ A) = (C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_fun__upd__other)).
% 226.10/125.33 thf(328,plain,((! [TA: $tType,TB: $tType]: (! [A:TA,B:TA,C:(TA > TB),D:TB]: ((~ (A = B)) => ((fun_upd @ TA @ TB @ (C) @ B @ D @ A) = (C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 226.10/125.33 thf(20,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_151_antisym__conv)).
% 226.10/125.33 thf(339,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)],[20])).
% 226.10/125.33 thf(187,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (minus_minus @ nat @ C @ B) @ (minus_minus @ nat @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_diff__le__mono2)).
% 226.10/125.33 thf(901,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (minus_minus @ nat @ C @ B) @ (minus_minus @ nat @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 226.10/125.33 thf(113,axiom,((! [TA: $tType]: (((comm_ring @ TA) & (dvd @ TA)) => (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((! [D:TA,E:TA]: ((A @ D) = (A @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B))))) => ((! [D:TA,E:TA]: ((C @ D) = (C @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B))))) => (! [D:TA,E:TA]: (((A @ D) & (C @ D)) = ((A @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B))) & (C @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_inf__period_I1_J)).
% 226.10/125.33 thf(679,plain,((! [TA: $tType]: (((comm_ring @ TA) & (dvd @ TA)) => (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((! [D:TA,E:TA]: ((A @ D) = (A @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B))))) => ((! [D:TA,E:TA]: ((C @ D) = (C @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B))))) => (! [D:TA,E:TA]: (((A @ D) & (C @ D)) = ((A @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B))) & (C @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B)))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 226.10/125.33 thf(273,axiom,((! [A:nat,B:nat,C:nat]: (((times_times @ nat @ A @ B) = (times_times @ nat @ A @ C)) = ((B = C) | (A = (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_mult__cancel1)).
% 226.10/125.33 thf(1155,plain,((! [A:nat,B:nat,C:nat]: (((times_times @ nat @ A @ B) = (times_times @ nat @ A @ C)) = ((B = C) | (A = (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[273])).
% 226.10/125.33 thf(227,axiom,((! [TA: $tType]: ((ring @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_left__diff__distrib)).
% 226.10/125.33 thf(1016,plain,((! [TA: $tType]: ((ring @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 226.10/125.33 thf(91,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_228_ord__less__eq__trans)).
% 226.10/125.33 thf(590,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)],[91])).
% 226.10/125.33 thf(109,axiom,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TB) => (! [A:(set @ TA),B:(set @ TA),C:(TA > TB),D:(TA > TB)]: ((A = B) => ((! [E:TA]: ((member @ TA @ E @ B) => ((C @ E) = (D @ E)))) => ((groups1340683514dd_sum @ TA @ TB @ C @ A) = (groups1340683514dd_sum @ TA @ TB @ D @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_sum_Ocong)).
% 226.10/125.33 thf(647,plain,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TB) => (! [A:(set @ TA),B:(set @ TA),C:(TA > TB),D:(TA > TB)]: ((A = B) => ((! [E:TA]: ((member @ TA @ E @ B) => ((C @ E) = (D @ E)))) => ((groups1340683514dd_sum @ TA @ TB @ (C) @ A) = (groups1340683514dd_sum @ TA @ TB @ (D) @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 226.10/125.33 thf(132,axiom,((minus @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ominus_4)).
% 226.10/125.33 thf(738,plain,((minus @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 226.10/125.33 thf(262,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_183_diff__right__mono)).
% 226.10/125.33 thf(1131,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)],[262])).
% 226.10/125.33 thf(286,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ A) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ B) => ((ord_less_eq @ TA @ B @ (one_one @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ A @ B) @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_mult__right__le__one__le)).
% 226.10/125.33 thf(1192,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ A) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ B) => ((ord_less_eq @ TA @ B @ (one_one @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ A @ B) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[286])).
% 226.10/125.33 thf(217,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA]: ((minus_minus @ TA @ A @ (zero_zero @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_diff__0__right)).
% 226.10/125.33 thf(984,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA]: ((minus_minus @ TA @ A @ (zero_zero @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 226.10/125.33 thf(222,axiom,((! [A:(nat > nat),B:nat]: ((number2016821345itions @ A @ B) => (ord_less_eq @ nat @ (groups1340683514dd_sum @ nat @ nat @ A @ (set_ord_atMost @ nat @ B)) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_partitions__parts__bounded)).
% 226.10/125.33 thf(1002,plain,((! [A:(nat > nat),B:nat]: ((number2016821345itions @ (A) @ B) => (ord_less_eq @ nat @ (groups1340683514dd_sum @ nat @ nat @ (A) @ (set_ord_atMost @ nat @ B)) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 226.10/125.33 thf(83,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_233_less__asym_H)).
% 226.10/125.33 thf(569,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)],[83])).
% 226.10/125.33 thf(97,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_236_dense)).
% 226.10/125.33 thf(605,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)],[97])).
% 226.10/125.33 thf(36,axiom,((! [TA: $tType]: ((zero @ TA) => (! [A:TA]: (((zero_zero @ TA) = A) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_zero__reorient)).
% 226.10/125.33 thf(393,plain,((! [TA: $tType]: ((zero @ TA) => (! [A:TA]: (((zero_zero @ TA) = A) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 226.10/125.33 thf(256,axiom,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TA) => (! [A:(set @ TB),B:(TB > TA)]: ((! [C:TB]: ((member @ TB @ C @ A) => (ord_less_eq @ TA @ (B @ C) @ (zero_zero @ TA)))) => (ord_less_eq @ TA @ (groups1340683514dd_sum @ TB @ TA @ B @ A) @ (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_sum__nonpos)).
% 226.10/125.33 thf(1114,plain,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TA) => (! [A:(set @ TB),B:(TB > TA)]: ((! [C:TB]: ((member @ TB @ C @ A) => (ord_less_eq @ TA @ (B @ C) @ (zero_zero @ TA)))) => (ord_less_eq @ TA @ (groups1340683514dd_sum @ TB @ TA @ (B) @ A) @ (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 226.10/125.33 thf(290,axiom,((! [A:nat]: ((times_times @ nat @ (zero_zero @ nat) @ A) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_mult__0)).
% 226.10/125.33 thf(1202,plain,((! [A:nat]: ((times_times @ nat @ (zero_zero @ nat) @ A) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[290])).
% 226.10/125.33 thf(244,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => (((minus_minus @ nat @ B @ A) = (minus_minus @ nat @ C @ A)) = (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_eq__diff__iff)).
% 226.10/125.33 thf(1086,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => (((minus_minus @ nat @ B @ A) = (minus_minus @ nat @ C @ A)) = (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 226.10/125.33 thf(8,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_146_order__trans)).
% 226.10/125.33 thf(311,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)],[8])).
% 226.10/125.33 thf(38,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_214_dual__order_Ostrict__trans)).
% 226.10/125.33 thf(398,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)],[38])).
% 226.10/125.33 thf(277,axiom,((semiring_0 @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Osemiring__0)).
% 226.10/125.33 thf(1167,plain,((semiring_0 @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[277])).
% 226.10/125.33 thf(69,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oord)).
% 226.10/125.33 thf(530,plain,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 226.10/125.33 thf(204,axiom,((! [TA: $tType]: ((monoid_mult @ TA) => (! [A:TA]: ((times_times @ TA @ (one_one @ TA) @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_mult_Oleft__neutral)).
% 226.10/125.33 thf(953,plain,((! [TA: $tType]: ((monoid_mult @ TA) => (! [A:TA]: ((times_times @ TA @ (one_one @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 226.10/125.33 thf(189,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > nat),C:TA]: ((! [D:TA]: ((~ (A @ D)) => (? [E:TA]: ((ord_less @ nat @ (B @ E) @ (B @ D)) & ~ (A @ E))))) => (A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_infinite__descent__measure)).
% 226.10/125.33 thf(906,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > nat),C:TA]: ((! [D:TA]: ((~ (A @ D)) => (? [E:TA]: ((ord_less @ nat @ (B @ E) @ (B @ D)) & ~ (A @ E))))) => (A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 226.10/125.33 thf(1,conjecture,(((minus_minus @ nat @ (groups1340683514dd_sum @ nat @ nat @ (^ [A:nat]: (times_times @ nat @ (p @ A) @ A)) @ (set_ord_atMost @ nat @ n)) @ k) = (minus_minus @ nat @ n @ k))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 226.10/125.33 thf(2,negated_conjecture,((~ ((minus_minus @ nat @ (groups1340683514dd_sum @ nat @ nat @ (^ [A:nat]: (times_times @ nat @ (p @ A) @ A)) @ (set_ord_atMost @ nat @ n)) @ k) = (minus_minus @ nat @ n @ k)))),inference(neg_conjecture,[status(cth)],[1])).
% 226.10/125.33 thf(298,plain,((~ ((minus_minus @ nat @ (groups1340683514dd_sum @ nat @ nat @ (^ [A:nat]: (times_times @ nat @ (p @ A) @ A)) @ (set_ord_atMost @ nat @ n)) @ k) = (minus_minus @ nat @ n @ k)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 226.10/125.33 thf(209,axiom,((! [TA: $tType]: ((ring_11004092258visors @ TA) => (! [A:TA,B:TA]: ((A = (times_times @ TA @ A @ B)) = ((A = (zero_zero @ TA)) | (B = (one_one @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_mult__cancel__left1)).
% 226.10/125.33 thf(965,plain,((! [TA: $tType]: ((ring_11004092258visors @ TA) => (! [A:TA,B:TA]: ((A = (times_times @ TA @ A @ B)) = ((A = (zero_zero @ TA)) | (B = (one_one @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 226.10/125.33 thf(101,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_216_exists__least__iff)).
% 226.10/125.33 thf(618,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)],[101])).
% 226.10/125.33 thf(269,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ (minus_minus @ TA @ A @ B)) = (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_diff__ge__0__iff__ge)).
% 226.10/125.33 thf(1146,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ (minus_minus @ TA @ A @ B)) = (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 226.10/125.33 thf(161,axiom,((mult_zero @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Omult__zero)).
% 226.10/125.33 thf(824,plain,((mult_zero @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 226.10/125.33 thf(85,axiom,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Opreorder)).
% 226.10/125.33 thf(573,plain,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 226.10/125.33 thf(30,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ A) => (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_subset__antisym)).
% 226.10/125.33 thf(375,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((ord_less_eq @ (set @ TA) @ A @ B) => ((ord_less_eq @ (set @ TA) @ B @ A) => (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 226.10/125.33 thf(272,axiom,((semigroup_mult @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Osemigroup__mult)).
% 226.10/125.33 thf(1154,plain,((semigroup_mult @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[272])).
% 226.10/125.33 thf(130,axiom,((! [A:nat,B:nat,C:nat]: (((times_times @ nat @ A @ B) = (times_times @ nat @ C @ B)) = ((A = C) | (B = (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_mult__cancel2)).
% 226.10/125.33 thf(732,plain,((! [A:nat,B:nat,C:nat]: (((times_times @ nat @ A @ B) = (times_times @ nat @ C @ B)) = ((A = C) | (B = (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 226.10/125.33 thf(169,axiom,((! [TA: $tType]: (((comm_ring @ TA) & (dvd @ TA)) => (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((! [D:TA,E:TA]: ((A @ D) = (A @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B))))) => ((! [D:TA,E:TA]: ((C @ D) = (C @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B))))) => (! [D:TA,E:TA]: (((A @ D) | (C @ D)) = ((A @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B))) | (C @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B)))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_inf__period_I2_J)).
% 226.10/125.33 thf(843,plain,((! [TA: $tType]: (((comm_ring @ TA) & (dvd @ TA)) => (! [A:(TA > $o),B:TA,C:(TA > $o)]: ((! [D:TA,E:TA]: ((A @ D) = (A @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B))))) => ((! [D:TA,E:TA]: ((C @ D) = (C @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B))))) => (! [D:TA,E:TA]: (((A @ D) | (C @ D)) = ((A @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B))) | (C @ (minus_minus @ TA @ D @ (times_times @ TA @ E @ B)))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 226.10/125.33 thf(134,axiom,((! [A:nat]: ((ord_less @ nat @ A @ (one_one @ nat)) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_less__one)).
% 226.10/125.33 thf(743,plain,((! [A:nat]: ((ord_less @ nat @ A @ (one_one @ nat)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 226.10/125.33 thf(259,axiom,((! [A:nat]: ((ord_less_eq @ nat @ A @ (zero_zero @ nat)) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_bot__nat__0_Oextremum__unique)).
% 226.10/125.33 thf(1124,plain,((! [A:nat]: ((ord_less_eq @ nat @ A @ (zero_zero @ nat)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 226.10/125.33 thf(188,axiom,((! [TA: $tType]: ((ordere1490568538miring @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ C) => (ord_less_eq @ TA @ (times_times @ TA @ C @ A) @ (times_times @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_ordered__comm__semiring__class_Ocomm__mult__left__mono)).
% 226.10/125.33 thf(904,plain,((! [TA: $tType]: ((ordere1490568538miring @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ C) => (ord_less_eq @ TA @ (times_times @ TA @ C @ A) @ (times_times @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 226.10/125.33 thf(214,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ C @ D) => (ord_less_eq @ nat @ (times_times @ nat @ A @ C) @ (times_times @ nat @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_mult__le__mono)).
% 226.10/125.33 thf(975,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ C @ D) => (ord_less_eq @ nat @ (times_times @ nat @ A @ C) @ (times_times @ nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 226.10/125.33 thf(224,axiom,((! [TA: $tType]: ((cancel1352612707id_add @ TA) => (! [A:TA]: ((minus_minus @ TA @ A @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_cancel__comm__monoid__add__class_Odiff__cancel)).
% 226.10/125.33 thf(1007,plain,((! [TA: $tType]: ((cancel1352612707id_add @ TA) => (! [A:TA]: ((minus_minus @ TA @ A @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 226.10/125.33 thf(119,axiom,((! [A:nat]: (ord_less_eq @ nat @ A @ (times_times @ nat @ A @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_le__square)).
% 226.10/125.33 thf(694,plain,((! [A:nat]: (ord_less_eq @ nat @ A @ (times_times @ nat @ A @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 226.10/125.33 thf(179,axiom,((! [A:nat]: (ord_less_eq @ nat @ A @ (times_times @ nat @ A @ (times_times @ nat @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_le__cube)).
% 226.10/125.33 thf(875,plain,((! [A:nat]: (ord_less_eq @ nat @ A @ (times_times @ nat @ A @ (times_times @ nat @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 226.10/125.33 thf(123,axiom,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB)]: ((groups1340683514dd_sum @ TB @ TA @ (^ [B:TB]: (zero_zero @ TA)) @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_sum_Oneutral__const)).
% 226.10/125.33 thf(711,plain,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB)]: ((groups1340683514dd_sum @ TB @ TA @ (^ [B:TB]: (zero_zero @ TA)) @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 226.10/125.33 thf(266,axiom,((number2016821345itions @ p @ n)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_partitions)).
% 226.10/125.33 thf(1139,plain,((number2016821345itions @ (p) @ n)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 226.10/125.33 thf(381,plain,(! [TA:$tType] : ((~ (zero_neq_one @ TA)) | (~ ((zero_zero @ TA) = (one_one @ TA))))),inference(cnf,[status(esa)],[380])).
% 226.10/125.33 thf(382,plain,(! [TA:$tType] : (((zero_zero @ TA) != (one_one @ TA)) | (~ (zero_neq_one @ TA)))),inference(lifteq,[status(thm)],[381])).
% 226.10/125.33 thf(9,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_231_less__linear)).
% 226.10/125.33 thf(313,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)],[9])).
% 226.10/125.33 thf(99,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_155_eq__refl)).
% 226.10/125.33 thf(611,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)],[99])).
% 226.10/125.33 thf(18,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_153_order_Otrans)).
% 226.10/125.33 thf(335,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)],[18])).
% 226.10/125.33 thf(245,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_44_fun__diff__def)).
% 226.10/125.33 thf(1090,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)],[245])).
% 226.10/125.33 thf(193,axiom,((! [TA: $tType]: ((semigroup_mult @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ (times_times @ TA @ A @ B) @ C) = (times_times @ TA @ A @ (times_times @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_mult_Oassoc)).
% 226.10/125.33 thf(919,plain,((! [TA: $tType]: ((semigroup_mult @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ (times_times @ TA @ A @ B) @ C) = (times_times @ TA @ A @ (times_times @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 226.10/125.33 thf(202,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((comm_monoid_add @ TC) => (! [A:(TB > (TA > TC)),B:(set @ TA),C:(set @ TB)]: ((groups1340683514dd_sum @ TB @ TC @ (^ [D:TB]: (groups1340683514dd_sum @ TA @ TC @ (A @ D) @ B)) @ C) = (groups1340683514dd_sum @ TA @ TC @ (^ [D:TA]: (groups1340683514dd_sum @ TB @ TC @ (^ [E:TB]: (A @ E @ D)) @ C)) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_sum_Oswap)).
% 226.10/125.33 thf(947,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((comm_monoid_add @ TC) => (! [A:(TB > (TA > TC)),B:(set @ TA),C:(set @ TB)]: ((groups1340683514dd_sum @ TB @ TC @ (^ [D:TB]: (groups1340683514dd_sum @ TA @ TC @ (A @ D) @ B)) @ C) = (groups1340683514dd_sum @ TA @ TC @ (^ [D:TA]: (groups1340683514dd_sum @ TB @ TC @ (^ [E:TB]: (A @ E @ D)) @ C)) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 226.10/125.33 thf(73,axiom,((! [TA: $tType,TB: $tType]: ((wellorder @ TB) => (! [A:(TA > TB),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ TB @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_measure__induct__rule)).
% 226.10/125.33 thf(540,plain,((! [TA: $tType,TB: $tType]: ((wellorder @ TB) => (! [A:(TA > TB),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ TB @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 226.10/125.33 thf(239,axiom,((! [TA: $tType]: ((monoid_mult @ TA) => ((^ [A:TA]: (A)) = (times_times @ TA @ (one_one @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_lambda__one)).
% 226.10/125.33 thf(1058,plain,((! [TA: $tType]: ((monoid_mult @ TA) => ((^ [A:TA]: (A)) = (times_times @ TA @ (one_one @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 226.10/125.33 thf(251,axiom,((! [TA: $tType]: ((ordered_semiring_0 @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ A) => ((ord_less_eq @ TA @ B @ (zero_zero @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ B @ A) @ (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_mult__nonneg__nonpos2)).
% 226.10/125.33 thf(1107,plain,((! [TA: $tType]: ((ordered_semiring_0 @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ A) => ((ord_less_eq @ TA @ B @ (zero_zero @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ B @ A) @ (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 226.10/125.33 thf(287,axiom,((! [A:nat]: (ord_less_eq @ nat @ (zero_zero @ nat) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_bot__nat__0_Oextremum)).
% 226.10/125.33 thf(1194,plain,((! [A:nat]: (ord_less_eq @ nat @ (zero_zero @ nat) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[287])).
% 226.10/125.33 thf(293,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ (minus_minus @ nat @ A @ B)) = (ord_less @ nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_zero__less__diff)).
% 226.10/125.33 thf(1209,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ (minus_minus @ nat @ A @ B)) = (ord_less @ nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[293])).
% 226.10/125.33 thf(146,axiom,((ab_semigroup_mult @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oab__semigroup__mult)).
% 226.10/125.33 thf(784,plain,((ab_semigroup_mult @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 226.10/125.33 thf(46,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_244_ord__less__eq__subst)).
% 226.10/125.33 thf(419,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)],[46])).
% 226.10/125.33 thf(235,axiom,((comm_monoid_mult @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocomm__monoid__mult)).
% 226.10/125.33 thf(1048,plain,((comm_monoid_mult @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 226.10/125.33 thf(55,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_dual__order_Ostrict__implies__not__eq)).
% 226.10/125.33 thf(451,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 226.10/125.33 thf(4,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_164_le__funI)).
% 226.10/125.33 thf(303,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)],[4])).
% 226.10/125.33 thf(95,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_147_order__class_Oorder_Oantisym)).
% 226.10/125.33 thf(599,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)],[95])).
% 226.10/125.33 thf(281,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (minus_minus @ nat @ A @ C) @ (minus_minus @ nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_diff__le__mono)).
% 226.10/125.33 thf(1175,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (minus_minus @ nat @ A @ C) @ (minus_minus @ nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[281])).
% 226.10/125.33 thf(219,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ (one_one @ TA)) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ B) => ((ord_less_eq @ TA @ B @ (one_one @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ A @ B) @ (one_one @ TA))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_mult__le__one)).
% 226.10/125.33 thf(990,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ (one_one @ TA)) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ B) => ((ord_less_eq @ TA @ B @ (one_one @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ A @ B) @ (one_one @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 226.10/125.33 thf(221,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > nat),C:(TA > nat)]: ((! [D:TA]: ((member @ TA @ D @ A) => (ord_less_eq @ nat @ (B @ D) @ (C @ D)))) => ((groups1340683514dd_sum @ TA @ nat @ (^ [D:TA]: (minus_minus @ nat @ (C @ D) @ (B @ D))) @ A) = (minus_minus @ nat @ (groups1340683514dd_sum @ TA @ nat @ C @ A) @ (groups1340683514dd_sum @ TA @ nat @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_sum__subtractf__nat)).
% 226.10/125.33 thf(996,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(TA > nat),C:(TA > nat)]: ((! [D:TA]: ((member @ TA @ D @ A) => (ord_less_eq @ nat @ (B @ D) @ (C @ D)))) => ((groups1340683514dd_sum @ TA @ nat @ (^ [D:TA]: (minus_minus @ nat @ (C @ D) @ (B @ D))) @ A) = (minus_minus @ nat @ (groups1340683514dd_sum @ TA @ nat @ (C) @ A) @ (groups1340683514dd_sum @ TA @ nat @ (B) @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 226.10/125.33 thf(65,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_245_ord__eq__less__subst)).
% 226.10/125.33 thf(509,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)],[65])).
% 226.10/125.33 thf(181,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less @ nat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_nat__less__induct)).
% 226.10/125.33 thf(880,plain,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less @ nat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 226.10/125.33 thf(183,axiom,((! [TA: $tType]: ((ord @ TA) => ((set_ord_atMost @ TA) = (^ [A:TA]: (collect @ TA @ (^ [B:TA]: (ord_less_eq @ TA @ B @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_atMost__def)).
% 226.10/125.33 thf(890,plain,((! [TA: $tType]: ((ord @ TA) => ((set_ord_atMost @ TA) = (^ [A:TA]: (collect @ TA @ (^ [B:TA]: (ord_less_eq @ TA @ B @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 226.10/125.33 thf(156,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ (one_one @ TA)) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ B) => (ord_less_eq @ TA @ (times_times @ TA @ B @ A) @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_mult__left__le)).
% 226.10/125.33 thf(811,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ (one_one @ TA)) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ B) => (ord_less_eq @ TA @ (times_times @ TA @ B @ A) @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 226.10/125.33 thf(175,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ (set @ TA) @ (set_ord_atMost @ TA @ A) @ (set_ord_atMost @ TA @ B)) = (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_atMost__subset__iff)).
% 226.10/125.33 thf(858,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ (set @ TA) @ (set_ord_atMost @ TA @ A) @ (set_ord_atMost @ TA @ B)) = (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 226.10/125.33 thf(98,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_218_order_Ostrict__trans)).
% 226.10/125.33 thf(609,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)],[98])).
% 226.10/125.33 thf(92,axiom,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_gt__ex)).
% 226.10/125.33 thf(594,plain,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 226.10/125.33 thf(102,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_less__imp__not__eq)).
% 226.10/125.33 thf(621,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 226.10/125.33 thf(270,axiom,((! [TA: $tType]: ((ordered_ring @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) => ((ord_less_eq @ TA @ B @ (zero_zero @ TA)) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_mult__nonpos__nonpos)).
% 226.10/125.33 thf(1149,plain,((! [TA: $tType]: ((ordered_ring @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) => ((ord_less_eq @ TA @ B @ (zero_zero @ TA)) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 226.10/125.33 thf(254,axiom,((preorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Opreorder_1)).
% 226.10/125.33 thf(1112,plain,((preorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 226.10/125.33 thf(58,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (one_one @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_zero__le__one)).
% 226.10/125.33 thf(462,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (zero_zero @ TA) @ (one_one @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 226.10/125.33 thf(240,axiom,((wellorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Owellorder)).
% 226.10/125.33 thf(1061,plain,((wellorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 226.10/125.33 thf(206,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_184_diff__eq__diff__less__eq)).
% 226.10/125.33 thf(959,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)],[206])).
% 226.10/125.33 thf(107,axiom,((number2016821345itions = (^ [A:(nat > nat),B:nat]: (! [C:nat]: (((A @ C) != (zero_zero @ nat)) => ((ord_less_eq @ nat @ (one_one @ nat) @ C) & (ord_less_eq @ nat @ C @ B))) & ((groups1340683514dd_sum @ nat @ nat @ (^ [C:nat]: (times_times @ nat @ (A @ C) @ C)) @ (set_ord_atMost @ nat @ B)) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_partitions__def)).
% 226.10/125.33 thf(636,plain,(((number2016821345itions) = (^ [A:(nat > nat),B:nat]: (! [C:nat]: ((~ ((A @ C) = (zero_zero @ nat))) => ((ord_less_eq @ nat @ (one_one @ nat) @ C) & (ord_less_eq @ nat @ C @ B))) & ((groups1340683514dd_sum @ nat @ nat @ (^ [C:nat]: (times_times @ nat @ (A @ C) @ C)) @ (set_ord_atMost @ nat @ B)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 226.10/125.33 thf(56,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_Collect__mem__eq)).
% 226.10/125.33 thf(455,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 226.10/125.33 thf(255,axiom,((ord_less_eq @ nat @ k @ n)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__092_060open_062k_A_092_060le_062_An_092_060close_062)).
% 226.10/125.33 thf(1113,plain,((ord_less_eq @ nat @ k @ n)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 226.10/125.33 thf(51,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_less__irrefl)).
% 226.10/125.33 thf(438,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 226.10/125.33 thf(194,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ A) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ B) => ((ord_less_eq @ TA @ B @ (one_one @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ B @ A) @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_mult__left__le__one__le)).
% 226.10/125.33 thf(922,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (zero_zero @ TA) @ A) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ B) => ((ord_less_eq @ TA @ B @ (one_one @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ B @ A) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 226.10/125.33 thf(111,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((comm_monoid_add @ TB) => (! [A:(set @ TC),B:(TA > TC),C:(TC > TA),D:(set @ TA),E:(TA > TB),F:(TC > TB)]: ((! [G:TC]: ((member @ TC @ G @ A) => ((B @ (C @ G)) = G))) => ((! [G:TC]: ((member @ TC @ G @ A) => (member @ TA @ (C @ G) @ D))) => ((! [G:TA]: ((member @ TA @ G @ D) => ((C @ (B @ G)) = G))) => ((! [G:TA]: ((member @ TA @ G @ D) => (member @ TC @ (B @ G) @ A))) => ((! [G:TC]: ((member @ TC @ G @ A) => ((E @ (C @ G)) = (F @ G)))) => ((groups1340683514dd_sum @ TC @ TB @ F @ A) = (groups1340683514dd_sum @ TA @ TB @ E @ D))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_sum_Oreindex__bij__witness)).
% 226.10/125.33 thf(658,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((comm_monoid_add @ TB) => (! [A:(set @ TC),B:(TA > TC),C:(TC > TA),D:(set @ TA),E:(TA > TB),F:(TC > TB)]: ((! [G:TC]: ((member @ TC @ G @ A) => ((B @ (C @ G)) = G))) => ((! [G:TC]: ((member @ TC @ G @ A) => (member @ TA @ (C @ G) @ D))) => ((! [G:TA]: ((member @ TA @ G @ D) => ((C @ (B @ G)) = G))) => ((! [G:TA]: ((member @ TA @ G @ D) => (member @ TC @ (B @ G) @ A))) => ((! [G:TC]: ((member @ TC @ G @ A) => ((E @ (C @ G)) = (F @ G)))) => ((groups1340683514dd_sum @ TC @ TB @ (F) @ A) = (groups1340683514dd_sum @ TA @ TB @ (E) @ D))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 226.10/125.33 thf(190,axiom,((cancel1352612707id_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocancel__comm__monoid__add)).
% 226.10/125.33 thf(912,plain,((cancel1352612707id_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 226.10/125.33 thf(116,axiom,((! [A:nat,B:nat,C:nat]: ((times_times @ nat @ A @ (minus_minus @ nat @ B @ C)) = (minus_minus @ nat @ (times_times @ nat @ A @ B) @ (times_times @ nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_diff__mult__distrib2)).
% 226.10/125.33 thf(685,plain,((! [A:nat,B:nat,C:nat]: ((times_times @ nat @ A @ (minus_minus @ nat @ B @ C)) = (minus_minus @ nat @ (times_times @ nat @ A @ B) @ (times_times @ nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 226.10/125.33 thf(242,axiom,((! [A:(nat > nat),B:nat,C:nat,D:nat]: ((number2016821345itions @ A @ B) => ((ord_less @ nat @ (zero_zero @ nat) @ (A @ C)) => (((fun_upd @ nat @ nat @ A @ C @ (minus_minus @ nat @ (A @ C) @ (one_one @ nat)) @ D) != (zero_zero @ nat)) => ((ord_less_eq @ nat @ (one_one @ nat) @ D) & (ord_less_eq @ nat @ D @ (minus_minus @ nat @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_partitions__remove1__bounds)).
% 226.10/125.33 thf(1076,plain,((! [A:(nat > nat),B:nat,C:nat,D:nat]: ((number2016821345itions @ (A) @ B) => ((ord_less @ nat @ (zero_zero @ nat) @ (A @ C)) => ((~ ((fun_upd @ nat @ nat @ (A) @ C @ (minus_minus @ nat @ (A @ C) @ (one_one @ nat)) @ D) = (zero_zero @ nat))) => ((ord_less_eq @ nat @ (one_one @ nat) @ D) & (ord_less_eq @ nat @ D @ (minus_minus @ nat @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 226.10/125.33 thf(230,axiom,((! [TA: $tType]: ((ab_semigroup_mult @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ A @ (times_times @ TA @ B @ C)) = (times_times @ TA @ B @ (times_times @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_mult_Oleft__commute)).
% 226.10/125.33 thf(1034,plain,((! [TA: $tType]: ((ab_semigroup_mult @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ A @ (times_times @ TA @ B @ C)) = (times_times @ TA @ B @ (times_times @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 226.10/125.33 thf(292,axiom,((order @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oorder_2)).
% 226.10/125.33 thf(1208,plain,((order @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[292])).
% 226.10/125.33 thf(151,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (times_times @ nat @ A @ B) @ (times_times @ nat @ C @ B)) = ((ord_less @ nat @ (zero_zero @ nat) @ B) & (ord_less @ nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_mult__less__cancel2)).
% 226.10/125.33 thf(795,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (times_times @ nat @ A @ B) @ (times_times @ nat @ C @ B)) = ((ord_less @ nat @ (zero_zero @ nat) @ B) & (ord_less @ nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 226.10/125.33 thf(196,axiom,((! [A:nat]: ((times_times @ nat @ A @ (zero_zero @ nat)) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_mult__0__right)).
% 226.10/125.33 thf(927,plain,((! [A:nat]: ((times_times @ nat @ A @ (zero_zero @ nat)) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 226.10/125.33 thf(264,axiom,((! [TA: $tType]: ((mult_zero @ TA) => ((^ [A:TA]: (zero_zero @ TA)) = (times_times @ TA @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_lambda__zero)).
% 226.10/125.33 thf(1134,plain,((! [TA: $tType]: ((mult_zero @ TA) => ((^ [A:TA]: (zero_zero @ TA)) = (times_times @ TA @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 226.10/125.33 thf(21,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_less__numeral__extra_I3_J)).
% 226.10/125.33 thf(342,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 226.10/125.33 thf(24,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_225_less__not__sym)).
% 226.10/125.33 thf(355,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)],[24])).
% 226.10/125.33 thf(138,axiom,((zero @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ozero)).
% 226.10/125.33 thf(754,plain,((zero @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 226.10/125.33 thf(167,axiom,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TA),B:(TA > TB),C:(TA > TB)]: ((! [D:TA]: ((member @ TA @ D @ A) => (ord_less_eq @ TB @ (B @ D) @ (C @ D)))) => (ord_less_eq @ TB @ (groups1340683514dd_sum @ TA @ TB @ B @ A) @ (groups1340683514dd_sum @ TA @ TB @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_sum__mono)).
% 226.10/125.33 thf(836,plain,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TA),B:(TA > TB),C:(TA > TB)]: ((! [D:TA]: ((member @ TA @ D @ A) => (ord_less_eq @ TB @ (B @ D) @ (C @ D)))) => (ord_less_eq @ TB @ (groups1340683514dd_sum @ TA @ TB @ (B) @ A) @ (groups1340683514dd_sum @ TA @ TB @ (C) @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 226.10/125.33 thf(236,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_171_diff__eq__diff__eq)).
% 226.10/125.33 thf(1049,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)],[236])).
% 226.10/125.33 thf(210,axiom,((dvd @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Odvd)).
% 226.10/125.33 thf(968,plain,((dvd @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 226.10/125.33 thf(57,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_order__less__subst2)).
% 226.10/125.33 thf(458,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 226.10/125.33 thf(283,axiom,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (minus_minus @ nat @ A @ B) @ C) = (minus_minus @ nat @ (minus_minus @ nat @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_diff__commute)).
% 226.10/125.33 thf(1181,plain,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (minus_minus @ nat @ A @ B) @ C) = (minus_minus @ nat @ (minus_minus @ nat @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[283])).
% 226.10/125.33 thf(143,axiom,((! [TA: $tType]: ((ordered_ring @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ (zero_zero @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ B @ C) @ (times_times @ TA @ A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_mult__right__mono__neg)).
% 226.10/125.33 thf(776,plain,((! [TA: $tType]: ((ordered_ring @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ (zero_zero @ TA)) => (ord_less_eq @ TA @ (times_times @ TA @ B @ C) @ (times_times @ TA @ A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 226.10/125.33 thf(67,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_141_dual__order_Oantisym)).
% 226.10/125.33 thf(525,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)],[67])).
% 226.10/125.33 thf(174,axiom,((! [A:nat,B:nat]: (((one_one @ nat) = (times_times @ nat @ A @ B)) = ((A = (one_one @ nat)) & (B = (one_one @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_nat__1__eq__mult__iff)).
% 226.10/125.33 thf(855,plain,((! [A:nat,B:nat]: (((one_one @ nat) = (times_times @ nat @ A @ B)) = ((A = (one_one @ nat)) & (B = (one_one @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 226.10/125.33 thf(133,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => ((minus_minus @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ C @ A)) = (minus_minus @ nat @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_Nat_Odiff__diff__eq)).
% 226.10/125.33 thf(739,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => ((minus_minus @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ C @ A)) = (minus_minus @ nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 226.10/125.33 thf(42,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_227_dual__order_Oasym)).
% 226.10/125.33 thf(409,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)],[42])).
% 226.10/125.33 thf(248,axiom,((! [TA: $tType]: ((semiri1193490041visors @ TA) => (! [A:TA,B:TA]: (((times_times @ TA @ A @ B) = (zero_zero @ TA)) = ((A = (zero_zero @ TA)) | (B = (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_mult__eq__0__iff)).
% 226.10/125.33 thf(1098,plain,((! [TA: $tType]: ((semiri1193490041visors @ TA) => (! [A:TA,B:TA]: (((times_times @ TA @ A @ B) = (zero_zero @ TA)) = ((A = (zero_zero @ TA)) | (B = (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 226.10/125.33 thf(44,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_238_neq__iff)).
% 226.10/125.33 thf(414,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)],[44])).
% 226.10/125.33 thf(212,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ (times_times @ nat @ A @ B)) = ((ord_less @ nat @ (zero_zero @ nat) @ A) & (ord_less @ nat @ (zero_zero @ nat) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_nat__0__less__mult__iff)).
% 226.10/125.33 thf(971,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ (times_times @ nat @ A @ B)) = ((ord_less @ nat @ (zero_zero @ nat) @ A) & (ord_less @ nat @ (zero_zero @ nat) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 226.10/125.33 thf(168,axiom,((! [TA: $tType]: ((comm_monoid_diff @ TA) => (! [A:TA]: ((minus_minus @ TA @ (zero_zero @ TA) @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_zero__diff)).
% 226.10/125.33 thf(840,plain,((! [TA: $tType]: ((comm_monoid_diff @ TA) => (! [A:TA]: ((minus_minus @ TA @ (zero_zero @ TA) @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 226.10/125.33 thf(19,axiom,((! [TA: $tType]: (ord @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oord_7)).
% 226.10/125.33 thf(337,plain,((! [TA: $tType]: (ord @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 226.10/125.33 thf(338,plain,(! [TA:$tType] : ((ord @ (set @ TA)))),inference(cnf,[status(esa)],[337])).
% 226.10/125.33 thf(296,axiom,((! [TA: $tType,TB: $tType]: ((semiring_0 @ TB) => (! [A:TB,B:(TA > TB),C:(set @ TA)]: ((times_times @ TB @ A @ (groups1340683514dd_sum @ TA @ TB @ B @ C)) = (groups1340683514dd_sum @ TA @ TB @ (^ [D:TA]: (times_times @ TB @ A @ (B @ D))) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_sum__distrib__left)).
% 226.10/125.33 thf(1218,plain,((! [TA: $tType,TB: $tType]: ((semiring_0 @ TB) => (! [A:TB,B:(TA > TB),C:(set @ TA)]: ((times_times @ TB @ A @ (groups1340683514dd_sum @ TA @ TB @ (B) @ C)) = (groups1340683514dd_sum @ TA @ TB @ (^ [D:TA]: (times_times @ TB @ A @ (B @ D))) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[296])).
% 226.10/125.33 thf(16,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_237_order_Oasym)).
% 226.10/125.33 thf(331,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)],[16])).
% 226.10/125.33 thf(285,axiom,((! [A:(nat > nat),B:nat]: ((! [C:nat]: (((A @ C) != (zero_zero @ nat)) => ((ord_less_eq @ nat @ (one_one @ nat) @ C) & (ord_less_eq @ nat @ C @ B)))) => (((groups1340683514dd_sum @ nat @ nat @ (^ [C:nat]: (times_times @ nat @ (A @ C) @ C)) @ (set_ord_atMost @ nat @ B)) = B) => (number2016821345itions @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_partitionsI)).
% 226.10/125.33 thf(1186,plain,((! [A:(nat > nat),B:nat]: ((! [C:nat]: ((~ ((A @ C) = (zero_zero @ nat))) => ((ord_less_eq @ nat @ (one_one @ nat) @ C) & (ord_less_eq @ nat @ C @ B)))) => (((groups1340683514dd_sum @ nat @ nat @ (^ [C:nat]: (times_times @ nat @ (A @ C) @ C)) @ (set_ord_atMost @ nat @ B)) = B) => (number2016821345itions @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[285])).
% 226.10/125.33 thf(232,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_eq__imp__le)).
% 226.10/125.33 thf(1038,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 226.10/125.33 thf(28,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (zero_zero @ TA) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_zero__le)).
% 226.10/125.33 thf(370,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (zero_zero @ TA) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 226.10/125.33 thf(297,axiom,((canoni770627133id_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocanonically__ordered__monoid__add)).
% 226.10/125.33 thf(1221,plain,((canoni770627133id_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[297])).
% 226.10/125.33 thf(237,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA]: ((minus_minus @ TA @ A @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_diff__self)).
% 226.10/125.33 thf(1052,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA]: ((minus_minus @ TA @ A @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 226.10/125.33 thf(177,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (times_times @ nat @ C @ A) @ (times_times @ nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_mult__le__mono2)).
% 226.10/125.33 thf(864,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (times_times @ nat @ C @ A) @ (times_times @ nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 226.10/125.33 thf(128,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_181_diff__mono)).
% 226.10/125.33 thf(727,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)],[128])).
% 226.10/125.33 thf(84,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_156_linear)).
% 226.10/125.33 thf(571,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)],[84])).
% 226.10/125.33 thf(34,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_239_neqE)).
% 226.10/125.33 thf(386,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)],[34])).
% 226.10/125.33 thf(215,axiom,((! [TA: $tType]: ((semiri1923998003cancel @ TA) => (! [A:TA,B:TA,C:TA]: (((times_times @ TA @ A @ B) = (times_times @ TA @ C @ B)) = ((B = (zero_zero @ TA)) | (A = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_mult__cancel__right)).
% 226.10/125.33 thf(978,plain,((! [TA: $tType]: ((semiri1923998003cancel @ TA) => (! [A:TA,B:TA,C:TA]: (((times_times @ TA @ A @ B) = (times_times @ TA @ C @ B)) = ((B = (zero_zero @ TA)) | (A = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 226.10/125.33 thf(267,axiom,((! [TA: $tType]: ((comm_s1003936772cancel @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_left__diff__distrib_H)).
% 226.10/125.33 thf(1140,plain,((! [TA: $tType]: ((comm_s1003936772cancel @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 226.10/125.33 thf(104,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TB,C:TA]: ((fun_upd @ TB @ TA @ A @ B @ C @ B) = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_fun__upd__same)).
% 226.10/125.33 thf(627,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TB,C:TA]: ((fun_upd @ TB @ TA @ (A) @ B @ C @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 226.10/125.33 thf(26,axiom,((preorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Opreorder_9)).
% 226.10/125.33 thf(363,plain,((preorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 226.10/125.33 thf(198,axiom,((! [TA: $tType]: ((comm_s1003936772cancel @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ A @ (minus_minus @ TA @ B @ C)) = (minus_minus @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_right__diff__distrib_H)).
% 226.10/125.33 thf(931,plain,((! [TA: $tType]: ((comm_s1003936772cancel @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ A @ (minus_minus @ TA @ B @ C)) = (minus_minus @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 226.10/125.33 thf(60,axiom,((! [TA: $tType,TB: $tType]: ((fun_upd @ TA @ TB) = (^ [A:(TA > TB),B:TA,C:TB,D:TA]: (if @ TB @ (D = B) @ C @ (A @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_fun__upd__def)).
% 226.10/125.33 thf(482,plain,((! [TA: $tType,TB: $tType]: ((fun_upd @ TA @ TB) = (^ [A:(TA > TB),B:TA,C:TB,D:TA]: (if @ TB @ (D = B) @ C @ (A @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 226.10/125.33 thf(117,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (times_times @ nat @ A @ B) @ (times_times @ nat @ A @ C)) = ((ord_less @ nat @ (zero_zero @ nat) @ A) => (ord_less_eq @ nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_nat__mult__le__cancel__disj)).
% 226.10/125.33 thf(688,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (times_times @ nat @ A @ B) @ (times_times @ nat @ A @ C)) = ((ord_less @ nat @ (zero_zero @ nat) @ A) => (ord_less_eq @ nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 226.10/125.33 thf(88,axiom,((! [TA: $tType]: (minus @ (set @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Set_Oset___Groups_Ominus_8)).
% 226.10/125.33 thf(581,plain,((! [TA: $tType]: (minus @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 226.10/125.33 thf(225,axiom,((! [A:nat,B:nat]: (((minus_minus @ nat @ A @ B) = (zero_zero @ nat)) = (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_diff__is__0__eq)).
% 226.10/125.33 thf(1010,plain,((! [A:nat,B:nat]: (((minus_minus @ nat @ A @ B) = (zero_zero @ nat)) = (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 226.10/125.33 thf(140,axiom,((! [A:nat]: ((ord_less_eq @ nat @ A @ (zero_zero @ nat)) => (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_bot__nat__0_Oextremum__uniqueI)).
% 226.10/125.33 thf(771,plain,((! [A:nat]: ((ord_less_eq @ nat @ A @ (zero_zero @ nat)) => (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 226.10/125.33 thf(121,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((comm_monoid_add @ TB) => (! [A:(set @ TA),B:(TA > TC),C:(set @ TC),D:(TC > TA),E:(TA > TB),F:(TC > TB)]: ((! [G:TA]: ((member @ TA @ G @ A) => ((member @ TC @ (B @ G) @ C) & ((D @ (B @ G)) = G)))) => ((! [G:TC]: ((member @ TC @ G @ C) => ((member @ TA @ (D @ G) @ A) & ((B @ (D @ G)) = G) & ((E @ (D @ G)) = (F @ G))))) => ((groups1340683514dd_sum @ TC @ TB @ F @ C) = (groups1340683514dd_sum @ TA @ TB @ E @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_sum_Oeq__general__inverses)).
% 226.10/125.33 thf(699,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((comm_monoid_add @ TB) => (! [A:(set @ TA),B:(TA > TC),C:(set @ TC),D:(TC > TA),E:(TA > TB),F:(TC > TB)]: ((! [G:TA]: ((member @ TA @ G @ A) => ((member @ TC @ (B @ G) @ C) & ((D @ (B @ G)) = G)))) => ((! [G:TC]: ((member @ TC @ G @ C) => ((member @ TA @ (D @ G) @ A) & ((B @ (D @ G)) = G) & ((E @ (D @ G)) = (F @ G))))) => ((groups1340683514dd_sum @ TC @ TB @ (F) @ C) = (groups1340683514dd_sum @ TA @ TB @ (E) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 226.10/125.33 thf(157,axiom,((semiri1923998003cancel @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Osemiring__no__zero__divisors__cancel)).
% 226.10/125.33 thf(813,plain,((semiri1923998003cancel @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 226.10/125.33 thf(11,axiom,((! [TA: $tType,TB: $tType]: ((fun_upd @ TA @ TB) = (^ [A:(TA > TB),B:TA,C:TB,D:TA]: (if @ TB @ (D = B) @ C @ (A @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_fun__upd__apply)).
% 226.10/125.33 thf(319,plain,((! [TA: $tType,TB: $tType]: ((fun_upd @ TA @ TB) = (^ [A:(TA > TB),B:TA,C:TB,D:TA]: (if @ TB @ (D = B) @ C @ (A @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 226.10/125.33 thf(241,axiom,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ D) => (ord_less_eq @ nat @ D @ C))) => (~ (! [D:nat]: ((A @ D) => (~ (! [E:nat]: ((A @ E) => (ord_less_eq @ nat @ E @ D))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_bounded__Max__nat)).
% 226.10/125.33 thf(1062,plain,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ D) => (ord_less_eq @ nat @ D @ C))) => (~ (! [D:nat]: ((A @ D) => (~ (! [E:nat]: ((A @ E) => (ord_less_eq @ nat @ E @ D))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 226.10/125.33 thf(249,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_le__trans)).
% 226.10/125.33 thf(1101,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 226.10/125.33 thf(145,axiom,((! [TA: $tType]: ((cancel1352612707id_add @ TA) => (! [A:TA]: ((minus_minus @ TA @ A @ (zero_zero @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_diff__zero)).
% 226.10/125.33 thf(781,plain,((! [TA: $tType]: ((cancel1352612707id_add @ TA) => (! [A:TA]: ((minus_minus @ TA @ A @ (zero_zero @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 226.10/125.33 thf(208,axiom,((! [TA: $tType]: ((linordered_ring @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_zero__le__square)).
% 226.10/125.33 thf(963,plain,((! [TA: $tType]: ((linordered_ring @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 226.10/125.33 thf(66,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_160_ord__eq__le__subst)).
% 226.10/125.33 thf(517,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)],[66])).
% 226.10/125.33 thf(185,axiom,((! [TA: $tType]: ((ring @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ A @ (minus_minus @ TA @ B @ C)) = (minus_minus @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_right__diff__distrib)).
% 226.10/125.33 thf(896,plain,((! [TA: $tType]: ((ring @ TA) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ A @ (minus_minus @ TA @ B @ C)) = (minus_minus @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 226.10/125.33 thf(136,axiom,((! [A:nat,B:nat]: (((times_times @ nat @ A @ B) = (one_one @ nat)) = ((A = (one_one @ nat)) & (B = (one_one @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_nat__mult__eq__1__iff)).
% 226.10/125.33 thf(748,plain,((! [A:nat,B:nat]: (((times_times @ nat @ A @ B) = (one_one @ nat)) = ((A = (one_one @ nat)) & (B = (one_one @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 226.10/125.33 thf(31,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_dual__order_Oirrefl)).
% 226.10/125.33 thf(378,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 226.10/125.33 thf(49,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_154_le__cases)).
% 226.10/125.33 thf(433,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)],[49])).
% 226.10/125.33 thf(294,axiom,((! [TA: $tType]: ((semiri1923998003cancel @ TA) => (! [A:TA,B:TA,C:TA]: ((A != (zero_zero @ TA)) => (((times_times @ TA @ B @ A) = (times_times @ TA @ C @ A)) = (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_mult__right__cancel)).
% 226.10/125.33 thf(1212,plain,((! [TA: $tType]: ((semiri1923998003cancel @ TA) => (! [A:TA,B:TA,C:TA]: ((~ (A = (zero_zero @ TA))) => (((times_times @ TA @ B @ A) = (times_times @ TA @ C @ A)) = (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[294])).
% 226.10/125.33 thf(33,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TB,C:TA]: (((fun_upd @ TB @ TA @ A @ B @ C) = A) = ((A @ B) = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_fun__upd__idem__iff)).
% 226.10/125.33 thf(383,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TB,C:TA]: (((fun_upd @ TB @ TA @ A @ B @ C) = (A)) = ((A @ B) = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 226.10/125.33 thf(186,axiom,(((groups1340683514dd_sum @ nat @ nat @ (^ [A:nat]: (times_times @ nat @ (fun_upd @ nat @ nat @ p @ k @ (minus_minus @ nat @ (p @ k) @ (one_one @ nat)) @ A) @ A)) @ (set_ord_atMost @ nat @ (minus_minus @ nat @ n @ k))) = (groups1340683514dd_sum @ nat @ nat @ (^ [A:nat]: (times_times @ nat @ (fun_upd @ nat @ nat @ p @ k @ (minus_minus @ nat @ (p @ k) @ (one_one @ nat)) @ A) @ A)) @ (set_ord_atMost @ nat @ n)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4__092_060open_062_I_092_060Sum_062i_092_060le_062n_A_N_Ak_O_A_Ip_Ik_A_058_061_Ap_Ak_A_N_A1_J_J_Ai_A_K_Ai_J_A_061_A_I_092_060Sum_062i_092_060le_062n_O_A_Ip_Ik_A_058_061_Ap_Ak_A_N_A1_J_J_Ai_A_K_Ai_J_092_060close_062)).
% 226.10/125.33 thf(899,plain,(((groups1340683514dd_sum @ nat @ nat @ (^ [A:nat]: (times_times @ nat @ (fun_upd @ nat @ nat @ p @ k @ (minus_minus @ nat @ (p @ k) @ (one_one @ nat)) @ A) @ A)) @ (set_ord_atMost @ nat @ (minus_minus @ nat @ n @ k))) = (groups1340683514dd_sum @ nat @ nat @ (^ [A:nat]: (times_times @ nat @ (fun_upd @ nat @ nat @ p @ k @ (minus_minus @ nat @ (p @ k) @ (one_one @ nat)) @ A) @ A)) @ (set_ord_atMost @ nat @ n)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 226.10/125.33 thf(75,axiom,((linorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Olinorder_10)).
% 226.10/125.33 thf(549,plain,((linorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 226.10/125.33 thf(71,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_166_le__funD)).
% 226.10/125.33 thf(536,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)],[71])).
% 226.10/125.33 thf(234,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_less__nat__zero__code)).
% 226.10/125.33 thf(1045,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 226.10/125.33 thf(125,axiom,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TA),B:(TA > TB)]: ((! [C:TA]: ((member @ TA @ C @ A) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (B @ C)))) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (groups1340683514dd_sum @ TA @ TB @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_sum__nonneg)).
% 226.10/125.33 thf(716,plain,((! [TA: $tType,TB: $tType]: ((ordere216010020id_add @ TB) => (! [A:(set @ TA),B:(TA > TB)]: ((! [C:TA]: ((member @ TA @ C @ A) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (B @ C)))) => (ord_less_eq @ TB @ (zero_zero @ TB) @ (groups1340683514dd_sum @ TA @ TB @ (B) @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 226.10/125.33 thf(275,axiom,((! [TA: $tType,TB: $tType]: ((semiring_0 @ TB) => (! [A:(TA > TB),B:(set @ TA),C:TB]: ((times_times @ TB @ (groups1340683514dd_sum @ TA @ TB @ A @ B) @ C) = (groups1340683514dd_sum @ TA @ TB @ (^ [D:TA]: (times_times @ TB @ (A @ D) @ C)) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_sum__distrib__right)).
% 226.10/125.33 thf(1161,plain,((! [TA: $tType,TB: $tType]: ((semiring_0 @ TB) => (! [A:(TA > TB),B:(set @ TA),C:TB]: ((times_times @ TB @ (groups1340683514dd_sum @ TA @ TB @ (A) @ B) @ C) = (groups1340683514dd_sum @ TA @ TB @ (^ [D:TA]: (times_times @ TB @ (A @ D) @ C)) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[275])).
% 226.10/125.33 thf(153,axiom,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB),B:(TB > TA)]: ((! [C:TB]: ((member @ TB @ C @ A) => ((B @ C) = (zero_zero @ TA)))) => ((groups1340683514dd_sum @ TB @ TA @ B @ A) = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_sum_Oneutral)).
% 226.10/125.33 thf(800,plain,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(set @ TB),B:(TB > TA)]: ((! [C:TB]: ((member @ TB @ C @ A) => ((B @ C) = (zero_zero @ TA)))) => ((groups1340683514dd_sum @ TB @ TA @ (B) @ A) = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 226.10/125.33 thf(263,axiom,((semiri1193490041visors @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Osemiring__no__zero__divisors)).
% 226.10/125.33 thf(1133,plain,((semiri1193490041visors @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 226.10/125.33 thf(3,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_213_not__less__iff__gr__or__eq)).
% 226.10/125.33 thf(300,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)],[3])).
% 226.10/125.33 thf(54,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_order_Ostrict__implies__not__eq)).
% 226.10/125.33 thf(447,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 226.10/125.33 thf(166,axiom,((! [TA: $tType]: ((semiri1923998003cancel @ TA) => (! [A:TA,B:TA,C:TA]: ((A != (zero_zero @ TA)) => (((times_times @ TA @ A @ B) = (times_times @ TA @ A @ C)) = (B = C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_mult__left__cancel)).
% 226.10/125.33 thf(833,plain,((! [TA: $tType]: ((semiri1923998003cancel @ TA) => (! [A:TA,B:TA,C:TA]: ((~ (A = (zero_zero @ TA))) => (((times_times @ TA @ A @ B) = (times_times @ TA @ A @ C)) = (B = C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 226.10/125.33 thf(203,axiom,((! [A:nat,B:nat,C:nat]: (((times_times @ nat @ A @ B) = (times_times @ nat @ A @ C)) = ((A = (zero_zero @ nat)) | (B = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_nat__mult__eq__cancel__disj)).
% 226.10/125.33 thf(950,plain,((! [A:nat,B:nat,C:nat]: (((times_times @ nat @ A @ B) = (times_times @ nat @ A @ C)) = ((A = (zero_zero @ nat)) | (B = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 226.10/125.33 thf(160,axiom,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(TB > TA),B:(set @ TB)]: (((groups1340683514dd_sum @ TB @ TA @ A @ B) != (zero_zero @ TA)) => (~ (! [C:TB]: ((member @ TB @ C @ B) => ((A @ C) = (zero_zero @ TA)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_sum_Onot__neutral__contains__not__neutral)).
% 226.10/125.33 thf(818,plain,((! [TA: $tType,TB: $tType]: ((comm_monoid_add @ TA) => (! [A:(TB > TA),B:(set @ TB)]: ((~ ((groups1340683514dd_sum @ TB @ TA @ (A) @ B) = (zero_zero @ TA))) => (~ (! [C:TB]: ((member @ TB @ C @ B) => ((A @ C) = (zero_zero @ TA)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 226.10/125.33 thf(149,axiom,((! [A:nat]: ((minus_minus @ nat @ A @ (zero_zero @ nat)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_minus__nat_Odiff__0)).
% 226.10/125.33 thf(790,plain,((! [A:nat]: ((minus_minus @ nat @ A @ (zero_zero @ nat)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 226.10/125.33 thf(178,axiom,((! [TA: $tType]: ((mult_zero @ TA) => (! [A:TA,B:TA]: (((times_times @ TA @ A @ B) != (zero_zero @ TA)) => ((A != (zero_zero @ TA)) & (B != (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_mult__not__zero)).
% 226.10/125.33 thf(867,plain,((! [TA: $tType]: ((mult_zero @ TA) => (! [A:TA,B:TA]: ((~ ((times_times @ TA @ A @ B) = (zero_zero @ TA))) => (~ (A = (zero_zero @ TA)) & ~ (B = (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 226.10/125.33 thf(131,axiom,((! [TA: $tType]: ((mult_zero @ TA) => (! [A:TA]: ((times_times @ TA @ (zero_zero @ TA) @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_mult__zero__left)).
% 226.10/125.33 thf(735,plain,((! [TA: $tType]: ((mult_zero @ TA) => (! [A:TA]: ((times_times @ TA @ (zero_zero @ TA) @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 226.10/125.33 thf(81,axiom,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder)).
% 226.10/125.33 thf(564,plain,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 226.10/125.33 thf(5,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_221_less__imp__triv)).
% 226.10/125.33 thf(305,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)],[5])).
% 226.10/125.33 thf(14,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_143_dual__order_Otrans)).
% 226.10/125.33 thf(326,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)],[14])).
% 226.10/125.33 thf(279,axiom,((one @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oone)).
% 226.10/125.33 thf(1172,plain,((one @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[279])).
% 226.10/125.33 thf(39,axiom,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TB,C:TA,D:(TB > TA),E:TA]: (((fun_upd @ TB @ TA @ A @ B @ C) = (fun_upd @ TB @ TA @ D @ B @ E)) => (C = E))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_fun__upd__eqD)).
% 226.10/125.33 thf(400,plain,((! [TA: $tType,TB: $tType]: (! [A:(TB > TA),B:TB,C:TA,D:(TB > TA),E:TA]: (((fun_upd @ TB @ TA @ A @ B @ C) = (fun_upd @ TB @ TA @ D @ B @ E)) => (C = E))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 226.10/125.33 thf(163,axiom,((ordered_semiring_0 @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Oordered__semiring__0)).
% 226.10/125.33 thf(828,plain,((ordered_semiring_0 @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 226.10/125.33 thf(70,axiom,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B))) => (ord_less_eq @ (set @ TA) @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_subsetI)).
% 226.10/125.33 thf(532,plain,((! [TA: $tType]: (! [A:(set @ TA),B:(set @ TA)]: ((! [C:TA]: ((member @ TA @ C @ A) => (member @ TA @ C @ B))) => (ord_less_eq @ (set @ TA) @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 226.10/125.33 thf(120,axiom,((! [A:nat]: ((minus_minus @ nat @ (zero_zero @ nat) @ A) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_diff__0__eq__0)).
% 226.10/125.33 thf(696,plain,((! [A:nat]: ((minus_minus @ nat @ (zero_zero @ nat) @ A) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 226.10/125.33 thf(126,axiom,((! [TA: $tType]: ((ring_11004092258visors @ TA) => (! [A:TA,B:TA]: (((times_times @ TA @ A @ B) = B) = ((B = (zero_zero @ TA)) | (A = (one_one @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_mult__cancel__right2)).
% 226.10/125.33 thf(720,plain,((! [TA: $tType]: ((ring_11004092258visors @ TA) => (! [A:TA,B:TA]: (((times_times @ TA @ A @ B) = B) = ((B = (zero_zero @ TA)) | (A = (one_one @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 226.10/125.33 thf(246,axiom,((! [TA: $tType]: ((ordered_semiring @ 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 @ (zero_zero @ TA) @ A) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ C) => (ord_less_eq @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ D)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_mult__mono_H)).
% 226.10/125.33 thf(1093,plain,((! [TA: $tType]: ((ordered_semiring @ 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 @ (zero_zero @ TA) @ A) => ((ord_less_eq @ TA @ (zero_zero @ TA) @ C) => (ord_less_eq @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 226.10/125.33 thf(218,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((minus_minus @ nat @ B @ (minus_minus @ nat @ B @ A)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_diff__diff__cancel)).
% 226.10/125.33 thf(987,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((minus_minus @ nat @ B @ (minus_minus @ nat @ B @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 226.10/125.33 thf(59,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_215_linorder__less__wlog)).
% 226.10/125.33 thf(464,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)],[59])).
% 226.10/125.33 thf(86,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_157_antisym)).
% 226.10/125.33 thf(575,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)],[86])).
% 226.10/125.33 thf(47,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_order__refl)).
% 226.10/125.33 thf(427,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 226.10/125.33 thf(93,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less_eq @ TA @ (one_one @ TA) @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_not__one__le__zero)).
% 226.10/125.33 thf(596,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less_eq @ TA @ (one_one @ TA) @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 226.10/125.33 thf(228,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((comm_monoid_add @ TB) => (! [A:(set @ TA),B:(set @ TC),C:(TC > TA),D:(TA > TB),E:(TC > TB)]: ((! [F:TA]: ((member @ TA @ F @ A) => (? [G:TC]: ((member @ TC @ G @ B) & ((C @ G) = F) & ! [H:TC]: (((member @ TC @ H @ B) & ((C @ H) = F)) => (H = G)))))) => ((! [F:TC]: ((member @ TC @ F @ B) => ((member @ TA @ (C @ F) @ A) & ((D @ (C @ F)) = (E @ F))))) => ((groups1340683514dd_sum @ TC @ TB @ E @ B) = (groups1340683514dd_sum @ TA @ TB @ D @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_sum_Oeq__general)).
% 226.10/125.33 thf(1019,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((comm_monoid_add @ TB) => (! [A:(set @ TA),B:(set @ TC),C:(TC > TA),D:(TA > TB),E:(TC > TB)]: ((! [F:TA]: ((member @ TA @ F @ A) => (? [G:TC]: ((member @ TC @ G @ B) & ((C @ G) = F) & ! [H:TC]: (((member @ TC @ H @ B) & ((C @ H) = F)) => (H = G)))))) => ((! [F:TC]: ((member @ TC @ F @ B) => ((member @ TA @ (C @ F) @ A) & ((D @ (C @ F)) = (E @ F))))) => ((groups1340683514dd_sum @ TC @ TB @ (E) @ B) = (groups1340683514dd_sum @ TA @ TB @ (D) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 226.10/125.33 thf(68,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (one_one @ TA) @ (one_one @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_le__numeral__extra_I4_J)).
% 226.10/125.33 thf(528,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (one_one @ TA) @ (one_one @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 226.10/125.33 thf(220,axiom,((! [TA: $tType]: ((ordered_semiring_0 @ TA) => (! [A:TA,B:TA]: ((((ord_less_eq @ TA @ (zero_zero @ TA) @ A) & (ord_less_eq @ TA @ B @ (zero_zero @ TA))) | ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) & (ord_less_eq @ TA @ (zero_zero @ TA) @ B))) => (ord_less_eq @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_split__mult__neg__le)).
% 226.10/125.33 thf(992,plain,((! [TA: $tType]: ((ordered_semiring_0 @ TA) => (! [A:TA,B:TA]: ((((ord_less_eq @ TA @ (zero_zero @ TA) @ A) & (ord_less_eq @ TA @ B @ (zero_zero @ TA))) | ((ord_less_eq @ TA @ A @ (zero_zero @ TA)) & (ord_less_eq @ TA @ (zero_zero @ TA) @ B))) => (ord_less_eq @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 226.10/125.33 thf(127,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ C @ B) => ((ord_less_eq @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ B @ C)) = (ord_less_eq @ nat @ C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_le__diff__iff_H)).
% 226.10/125.33 thf(723,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ C @ B) => ((ord_less_eq @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ B @ C)) = (ord_less_eq @ nat @ C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 226.10/125.33 thf(172,axiom,((! [A:nat,B:nat]: (ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_diff__le__self)).
% 226.10/125.33 thf(850,plain,((! [A:nat,B:nat]: (ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 226.10/125.33 thf(223,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (minus_minus @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_diff__gt__0__iff__gt)).
% 226.10/125.33 thf(1004,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (minus_minus @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 226.10/125.33 thf(118,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (times_times @ nat @ A @ B) @ (times_times @ nat @ C @ B)) = ((ord_less @ nat @ (zero_zero @ nat) @ B) => (ord_less_eq @ nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_mult__le__cancel2)).
% 226.10/125.33 thf(691,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (times_times @ nat @ A @ B) @ (times_times @ nat @ C @ B)) = ((ord_less @ nat @ (zero_zero @ nat) @ B) => (ord_less_eq @ nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 226.10/125.33 thf(12,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_150_order__class_Oorder_Oeq__iff)).
% 226.10/125.33 thf(322,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)],[12])).
% 226.10/125.33 thf(284,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) | (ord_less_eq @ nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_nat__le__linear)).
% 226.10/125.33 thf(1184,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) | (ord_less_eq @ nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[284])).
% 226.10/125.33 thf(7,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TA) => (minus @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Groups_Ominus)).
% 226.10/125.33 thf(309,plain,((! [TA: $tType,TB: $tType]: ((minus @ TA) => (minus @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 226.10/125.33 thf(27,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_144_linorder__wlog)).
% 226.10/125.33 thf(364,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)],[27])).
% 226.10/125.33 thf(122,axiom,((! [A:nat]: ((times_times @ nat @ (one_one @ nat) @ A) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_nat__mult__1)).
% 226.10/125.33 thf(708,plain,((! [A:nat]: ((times_times @ nat @ (one_one @ nat) @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 226.10/125.33 thf(231,axiom,((ord_less @ nat @ (zero_zero @ nat) @ (p @ k))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_gr0)).
% 226.10/125.33 thf(1037,plain,((ord_less @ nat @ (zero_zero @ nat) @ (p @ k))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 226.10/125.33 thf(142,axiom,((ordered_semiring @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Oordered__semiring)).
% 226.10/125.33 thf(775,plain,((ordered_semiring @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 226.10/125.33 thf(139,axiom,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ D) => (ord_less_eq @ nat @ D @ C))) => (? [D:nat]: ((A @ D) & ! [E:nat]: ((A @ E) => (ord_less_eq @ nat @ E @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_Nat_Oex__has__greatest__nat)).
% 226.10/125.33 thf(755,plain,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ D) => (ord_less_eq @ nat @ D @ C))) => (? [D:nat]: ((A @ D) & ! [E:nat]: ((A @ E) => (ord_less_eq @ nat @ E @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 226.10/125.33 thf(112,axiom,((! [A:(nat > nat),B:nat,C:nat]: ((number2016821345itions @ A @ B) => (ord_less_eq @ nat @ (A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_partitions__bounds)).
% 226.10/125.33 thf(676,plain,((! [A:(nat > nat),B:nat,C:nat]: ((number2016821345itions @ (A) @ B) => (ord_less_eq @ nat @ (A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 226.10/125.33 thf(1224,plain,(($false)),inference(e,[status(thm)],[1168,347,846,333,893,555,1110,1083,962,408,1158,683,1205,861,1173,440,655,1137,550,500,1164,814,913,945,538,930,1196,1127,417,829,1095,389,1055,785,372,504,587,751,344,934,357,817,559,638,969,1013,325,316,924,443,1109,485,806,1151,937,877,956,774,396,411,1104,507,602,981,1215,634,307,380,1199,810,714,798,546,793,334,746,825,778,1042,598,561,429,788,729,407,630,916,1032,625,1178,889,682,974,847,566,852,435,583,830,551,1128,578,1143,615,1121,403,1118,328,339,901,679,1155,1016,590,647,738,1131,1192,984,1002,569,605,393,1114,1202,1086,311,398,1167,530,953,906,298,965,618,1146,824,573,375,1154,732,843,743,1124,904,975,1007,694,875,711,1139,382,313,611,335,1090,919,947,540,1058,1107,1194,1209,784,419,1048,451,303,599,1175,990,996,509,880,890,811,858,609,594,621,1149,1112,462,1061,959,636,455,1113,438,922,658,912,685,1076,1034,1208,795,927,1134,342,355,754,836,1049,968,458,1181,776,525,855,739,409,1098,414,971,840,338,1218,331,1186,1038,370,1221,1052,864,727,571,386,978,1140,627,363,931,482,688,581,1010,771,699,813,319,1062,1101,781,963,517,896,748,378,433,1212,383,899,549,536,1045,716,1161,800,1133,300,447,833,950,818,790,867,735,564,305,326,1172,400,828,532,696,720,1093,987,464,575,427,596,1019,528,992,723,850,1004,691,322,337,1184,309,364,708,1037,775,755,676])).
% 226.10/125.33 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 226.10/125.33 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------