%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : DAT153^1 : TPTP v9.3.1. Released v7.0.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 : n006.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 07:48:03 AM UTC 2026
% Result : Theorem 28.57s 8.03s
% Output : Refutation 29.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : DAT153^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.20 % Computer : n006.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Tue Sep 29 18:01:54 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 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.85/0.78 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.98/1.14 % [INFO] Parsing done (360ms).
% 1.98/1.15 % [INFO] Running in sequential loop mode.
% 3.15/1.53 % [INFO] eprover registered as external prover.
% 3.15/1.54 % [INFO] Scanning for conjecture ...
% 3.59/1.70 % [INFO] Found a conjecture (or negated_conjecture) and 293 axioms. Running axiom selection ...
% 3.88/1.86 % [INFO] Axiom selection finished. Selected 292 axioms (removed 1 axioms).
% 5.12/2.14 % [INFO] Problem is higher-order (TPTP THF).
% 5.12/2.17 % [INFO] Type checking passed.
% 5.12/2.17 % [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 ...
% 27.97/8.02 % External prover 'e' found a proof!
% 27.97/8.02 % [INFO] Killing All external provers ...
% 27.97/8.02 % Time passed: 7683ms (effective reasoning time: 6862ms)
% 27.97/8.02 % 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)>
% 27.97/8.03 % Axioms used in derivation (292): fact_54_not__less0, fact_238_nat__int, fact_27_neq0__conv, fact_152_enat__the__enat, fact_249_inverse__negative__imp__negative, fact_164_times__enat__simps_I1_J, fact_251_inverse__less__imp__less__neg, fact_22_zero__reorient, fact_239_inverse__positive__iff__positive, tcon_Nat_Onat___Nat_Osemiring__char__0_9, fact_130_imult__is__0, fact_176_no__zero__divisors, tcon_Int_Oint___Rings_Olinordered__semidom, fact_91_enat__ex__split, fact_221_semiring__normalization__rules_I17_J, fact_6_enat__iless, fact_125_less__int__code_I1_J, fact_39_measure__induct, fact_66_until__monoL, fact_203_nat__mult__eq__cancel__disj, fact_25_until__false, tcon_Int_Oint___Rings_Olinordered__semiring__strict, tcon_Nat_Onat___Rings_Osemiring__no__zero__divisors_4, fact_1_less__sfirstD, fact_72_enat_Osimps_I4_J, fact_228_transfer__morphism__int__nat, fact_172_zmult__zless__mono2__lemma, tcon_Extended__Nat_Oenat___Rings_Osemiring__no__zero__divisors_14, fact_219_semiring__normalization__rules_I15_J, fact_143_alw__ev__sdrop, fact_207_linordered__field__class_Osign__simps_I45_J, fact_122_ev_Obase, fact_194_mult__neg__pos, fact_170_zmult__zless__mono2, tcon_Int_Oint___Rings_Omult__zero, fact_105_zero__less__imp__eq__int, tcon_Int_Oint___Groups_Ozero, fact_220_semiring__normalization__rules_I16_J, fact_173_times__enat__def, fact_129_mult__of__nat__commute, fact_73_scount__eq__0__iff, fact_118_mult_Oassoc, fact_4_sdrop_Osimps_I1_J, fact_139_not__ev__iff, fact_210_linordered__field__no__lb, fact_84_of__nat__eq__0__iff, fact_230_ceiling__zero, fact_28_alw__iff__sdrop, fact_42_infinite__descent, fact_109_the__enat__0, fact_242_inverse__less__iff__less, fact_68_UNTIL_Obase, fact_92_enat_Oinducts, fact_80_enat__ord__simps_I4_J, fact_70_less__enat__def, tcon_Nat_Onat___Rings_Olinordered__semiring__strict_3, fact_31_enat_Osimps_I6_J, fact_74_scount__eq__0I, fact_2_not__gr__zero, fact_134_alw__alw__impl__ev, tcon_Nat_Onat___Rings_Olinordered__comm__semiring__strict_2, fact_171_linorder__neqE__linordered__idom, tcon_Extended__Nat_Oenat___Groups_Osemigroup__mult_17, fact_98_infinity__ne__i0, fact_112_of__nat__mult, fact_83_enat_Osimps_I7_J, fact_94_enat3__cases, fact_165_times__int__code_I1_J, fact_55_less__zeroE, fact_126_ev__alw__imp__alw__ev, fact_215_semiring__normalization__rules_I10_J, fact_236_inverse__nonzero__iff__nonzero, fact_132_ev__alw__alw__impl, fact_123_ev__mono, tcon_Int_Oint___Groups_Oab__semigroup__mult, fact_41_nat__less__induct, fact_209_linordered__field__no__ub, fact_38_less__not__refl3, fact_234_ex__inverse__of__nat__less, fact_107_times__enat__simps_I3_J, fact_52_gr0I, fact_103_less__infinityE, fact_99_of__nat__less__0__iff, fact_160_mult__0__right, tcon_Int_Oint___Rings_Olinordered__comm__semiring__strict, fact_62_alw__cong, fact_250_less__imp__inverse__less__neg, fact_101_less__imp__of__nat__less, fact_23_enat__less__induct, fact_235_inverse__zero, fact_13_i0__less, tcon_Int_Oint___Rings_Olinordered__ring, fact_223_semiring__normalization__rules_I19_J, fact_212_linordered__field__class_Osign__simps_I24_J, fact_151_imult__infinity, fact_227_sdrop__wait, fact_186_mult__less__cancel__left__pos, fact_202_int__if__cong, fact_166_times__int__code_I2_J, fact_61_alw__mono, fact_197_mult__neg__neg, fact_40_less__irrefl__nat, fact_200_transfer__int__nat__numerals_I1_J, fact_65_until__monoR, fact_198_nat__mult__less__cancel__disj, fact_71_case__enat__def, fact_100_of__nat__less__imp__less, fact_241_inverse__less__iff__less__neg, fact_232_ceiling__less__cancel, fact_252_less__imp__inverse__less, fact_33_alw__aand, fact_3_enat_Oinject, fact_153_mult__cancel__right, help_If_1_1_T, fact_187_mult__less__cancel__left__neg, fact_95_enat2__cases, fact_174_mult__not__zero, fact_154_mult__cancel__left, fact_168_mult__less__mono1, fact_182_mult__strict__right__mono__neg, fact_34_alw__mp, fact_77_of__nat__eq__iff, fact_110_scount__finite, fact_17_zero__enat__def, fact_222_semiring__normalization__rules_I18_J, tcon_Nat_Onat___Rings_Omult__zero_11, fact_8_gr__zeroI, tcon_Int_Oint___Groups_Osemigroup__mult, tcon_Int_Oint___Rings_Olinordered__idom, tcon_Int_Oint___Rings_Ocomm__semiring__1, fact_206_nat__mult__eq__cancel1, fact_43_linorder__neqE__nat, fact_208_linordered__field__class_Osign__simps_I44_J, fact_119_mult_Ocommute, fact_97_enat_Odistinct_I2_J, fact_82_enat_Osimps_I5_J, fact_14_sfirst__0, fact_231_ceiling__of__nat, fact_11_zero__less__iff__neq__zero, fact_162_mult__less__cancel2, fact_53_not__gr0, fact_213_linordered__field__class_Osign__simps_I23_J, fact_78_not__infinity__eq, fact_36_less__not__refl, fact_245_zless__nat__eq__int__zless, fact_75_scount__eq__0D, fact_150_imult__infinity__right, fact_196_not__square__less__zero, fact_135_ev__alw__impl__ev, fact_15_enat__ord__simps_I2_J, fact_64_alwD, fact_211_linordered__field__class_Osign__simps_I25_J, fact_191_mult__pos__neg2, fact_141_not__ev, fact_51_size__enat__def, fact_19_enat__0__iff_I2_J, tcon_Int_Oint___Rings_Osemiring__1, fact_224_scount__eq__card, fact_138_ev__alw__aand, fact_159_mult__cancel1, fact_147_scount__infinite__iff, fact_201_transfer__int__nat__relations_I1_J, fact_199_transfer__int__nat__relations_I2_J, fact_161_mult__is__0, fact_185_mult__strict__left__mono__neg, fact_37_less__not__refl2, tcon_Nat_Onat___Groups_Oab__semigroup__mult_6, fact_16_not__iless0, fact_195_mult__less__0__iff, fact_104_enat__ord__code_I4_J, fact_216_semiring__normalization__rules_I7_J, fact_90_of__nat__eq__enat, fact_179_linordered__comm__semiring__strict__class_Ocomm__mult__strict__left__mono, fact_93_enat_Oexhaust, fact_12_fun__cong__unused__0, fact_237_inverse__mult__distrib, fact_59_infinite__descent0__measure, help_If_3_1_T, fact_69_of__nat__0__less__iff, tcon_Extended__Nat_Oenat___Rings_Ocomm__semiring__1_16, help_If_2_1_T, fact_177_mult__left__cancel, fact_115_not__ev__not, tcon_Extended__Nat_Oenat___Groups_Ocanonically__ordered__monoid__add_13, tcon_Nat_Onat___Groups_Ozero_12, fact_79_not__enat__eq, fact_193_mult__pos__neg, fact_192_mult__pos__pos, fact_205_nat__mult__less__cancel1, fact_9_not__less__zero, fact_180_mult__less__cancel__right__disj, fact_35_nat__neq__iff, fact_63_alw__alwD, fact_29_alw__sdrop, fact_158_mult__cancel2, fact_116_int__int__eq, tcon_Int_Oint___Rings_Osemiring__no__zero__divisors, fact_137_ev__alw__impl, fact_136_not__alw__iff, fact_124_ev__False, fact_49_infinite__descent__measure, fact_246_positive__imp__inverse__positive, fact_240_inverse__negative__iff__negative, tcon_Extended__Nat_Oenat___Rings_Osemiring__1_19, fact_20_less__enatE, fact_145_imult__is__infinity, fact_247_negative__imp__inverse__negative, fact_45_Collect__mem__eq, fact_121_ev__or, tcon_Nat_Onat___Groups_Osemigroup__mult_8, fact_85_of__nat__0__eq__iff, fact_248_inverse__positive__imp__positive, fact_225_semiring__normalization__rules_I9_J, fact_76_enat_Osize_I4_J, fact_217_semiring__normalization__rules_I13_J, fact_21_sfirst__eq__0, fact_144_ex__less__of__nat__mult, fact_155_mult__eq__0__iff, fact_146_enat__0__less__mult__iff, fact_26_alw__alw, fact_149_sfirst__finite, fact_229_zero__less__ceiling, fact_163_nat__0__less__mult__iff, tcon_Nat_Onat___Rings_Osemiring__no__zero__divisors__cancel_1, fact_120_mult_Oleft__commute, fact_243_nat__0, tcon_Int_Oint___Nat_Osemiring__char__0, fact_190_zero__less__mult__iff, fact_127_ev__cong, fact_18_enat__0__iff_I1_J, fact_117_ab__semigroup__mult__class_Omult__ac_I1_J, fact_188_zero__less__mult__pos2, fact_131_alw__ev__imp__ev__alw, fact_142_the__enat_Osimps, tcon_Extended__Nat_Oenat___Nat_Osemiring__char__0_18, fact_175_divisors__zero, fact_48_measure__induct__rule, tcon_Extended__Nat_Oenat___Groups_Ozero_21, tcon_Int_Oint___Rings_Olinordered__ring__strict, fact_167_mult__0, tcon_Nat_Onat___Rings_Osemiring__1_10, fact_189_zero__less__mult__pos, fact_7_less__numeral__extra_I3_J, fact_181_mult__strict__right__mono, tcon_Extended__Nat_Oenat___Rings_Omult__zero_20, fact_156_mult__zero__right, tcon_Nat_Onat___Rings_Ocomm__semiring__1_7, fact_86_of__nat__0, fact_24_enat_Osize_I1_J, fact_60_all__imp__alw, fact_0__C0_Oprems_C, tcon_Nat_Onat___Groups_Ocanonically__ordered__monoid__add, fact_148_scount__infinite, fact_226_card__Collect__less__nat, tcon_Nat_Onat___Rings_Olinordered__semidom_5, fact_32_alw__False, fact_57_infinite__descent0, fact_89_enat_Osize_I2_J, fact_214_scount__eq, fact_106_reals__Archimedean2, fact_108_times__enat__simps_I4_J, fact_204_Nat__Transfer_Otransfer__int__nat__functions_I2_J, fact_10_gr__implies__not__zero, fact_5_chain__incr, fact_183_mult__less__cancel__left__disj, fact_56_gr__implies__not0, fact_88_case__enat__0, fact_114_not__alw__not, fact_133_alw__impl__ev__alw, fact_169_mult__less__mono2, tcon_Int_Oint___Rings_Osemiring__no__zero__divisors__cancel, fact_81_enat__ord__simps_I6_J, fact_178_mult__right__cancel, fact_140_not__alw, fact_157_mult__zero__left, tcon_Extended__Nat_Oenat___Groups_Oab__semigroup__mult_15, fact_58_less__nat__zero__code, fact_113_times__enat__simps_I2_J, fact_96_enat_Odistinct_I1_J, fact_46_Collect__cong, fact_184_mult__strict__left__mono, fact_111_ev__ev, fact_87_of__nat__less__iff, fact_44_mem__Collect__eq, fact_50_size__enat__overloaded__def, fact_218_semiring__normalization__rules_I14_J, fact_128_ev__iff__sdrop, fact_244_zless__nat__conj, fact_67_until__mono, fact_30_enat_Osize_I3_J, fact_102_infinity__ilessE, fact_233_zero__less__nat__eq
% 27.97/8.03 % No. of inferences in proof: 588
% 28.57/8.03 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 7683 ms resp. 6862 ms w/o parsing
% 29.81/8.31 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.81/8.31 thf(extended_enat_type, type, extended_enat: $tType).
% 29.81/8.31 thf(nat_type, type, nat: $tType).
% 29.81/8.31 thf(int_type, type, int: $tType).
% 29.81/8.31 thf(a_type, type, a: $tType).
% 29.81/8.31 thf(zero_decl, type, zero: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(field_decl, type, field: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(mult_zero_decl, type, mult_zero: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(semiring_1_decl, type, semiring_1: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(semiring_char_0_decl, type, semiring_char_0: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(division_ring_decl, type, division_ring: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(semigroup_mult_decl, type, semigroup_mult: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(comm_semiring_1_decl, type, comm_semiring_1: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(linordered_idom_decl, type, linordered_idom: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(linordered_ring_decl, type, linordered_ring: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(linordered_field_decl, type, linordered_field: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(ab_semigroup_mult_decl, type, ab_semigroup_mult: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(linordered_semidom_decl, type, linordered_semidom: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(linord581940658strict_decl, type, linord581940658strict: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(archim1727834104eiling_decl, type, archim1727834104eiling: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(semiri1193490041visors_decl, type, semiri1193490041visors: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(linord20386208strict_decl, type, linord20386208strict: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(archim1804426504_field_decl, type, archim1804426504_field: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(canoni770627133id_add_decl, type, canoni770627133id_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(linord893533164strict_decl, type, linord893533164strict: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(semiri1923998003cancel_decl, type, semiri1923998003cancel: !> [TA: $tType]: ((itself @ TA) > $o)).
% 29.81/8.31 thf(archimedean_ceiling_decl, type, archimedean_ceiling: !> [TA: $tType]: (TA > int)).
% 29.81/8.31 thf(coindu1365464361scount_decl, type, coindu1365464361scount: !> [TA: $tType]: (((stream @ TA) > $o) > ((stream @ TA) > extended_enat))).
% 29.81/8.31 thf(coindu76177514sfirst_decl, type, coindu76177514sfirst: !> [TA: $tType]: (((stream @ TA) > $o) > ((stream @ TA) > extended_enat))).
% 29.81/8.31 thf(extended_enat2_decl, type, extended_enat2: (nat > extended_enat)).
% 29.81/8.31 thf(extended_case_enat_decl, type, extended_case_enat: !> [TA: $tType]: ((nat > TA) > (TA > (extended_enat > TA)))).
% 29.81/8.31 thf(extended_rec_enat_decl, type, extended_rec_enat: !> [TA: $tType]: ((nat > TA) > (TA > (extended_enat > TA)))).
% 29.81/8.31 thf(extended_size_enat_decl, type, extended_size_enat: (extended_enat > nat)).
% 29.81/8.31 thf(extend1396239628finity_decl, type, extend1396239628finity: !> [TA: $tType]: TA).
% 29.81/8.31 thf(extended_the_enat_decl, type, extended_the_enat: (extended_enat > nat)).
% 29.81/8.31 thf(inverse_inverse_decl, type, inverse_inverse: !> [TA: $tType]: (TA > TA)).
% 29.81/8.31 thf(finite_card_decl, type, finite_card: !> [TA: $tType]: ((set @ TA) > nat)).
% 29.81/8.31 thf(times_times_decl, type, times_times: !> [TA: $tType]: (TA > (TA > TA))).
% 29.81/8.31 thf(zero_zero_decl, type, zero_zero: !> [TA: $tType]: TA).
% 29.81/8.31 thf(if_decl, type, if: !> [TA: $tType]: ($o > (TA > (TA > TA)))).
% 29.81/8.31 thf(nat2_decl, type, nat2: (int > nat)).
% 29.81/8.31 thf(linear1341015445_UNTIL_decl, type, linear1341015445_UNTIL: !> [TA: $tType]: (((stream @ TA) > $o) > (((stream @ TA) > $o) > ((stream @ TA) > $o)))).
% 29.81/8.31 thf(linear1386806755on_alw_decl, type, linear1386806755on_alw: !> [TA: $tType]: (((stream @ TA) > $o) > ((stream @ TA) > $o))).
% 29.81/8.31 thf(linear505997466_on_ev_decl, type, linear505997466_on_ev: !> [TA: $tType]: (((stream @ TA) > $o) > ((stream @ TA) > $o))).
% 29.81/8.31 thf(linear1335279038n_wait_decl, type, linear1335279038n_wait: !> [TA: $tType]: (((stream @ TA) > $o) > ((stream @ TA) > nat))).
% 29.81/8.31 thf(semiring_1_of_nat_decl, type, semiring_1_of_nat: !> [TA: $tType]: (nat > TA)).
% 29.81/8.31 thf(size_size_decl, type, size_size: !> [TA: $tType]: (TA > nat)).
% 29.81/8.31 thf(nat_tr1645093318rphism_decl, type, nat_tr1645093318rphism: !> [TA: $tType,TB: $tType]: ((TB > TA) > ((TB > $o) > $o))).
% 29.81/8.31 thf(ord_less_decl, type, ord_less: !> [TA: $tType]: (TA > (TA > $o))).
% 29.81/8.31 thf(type_decl, type, type: !> [TA: $tType]: (itself @ TA)).
% 29.81/8.31 thf(collect_decl, type, collect: !> [TA: $tType]: ((TA > $o) > (set @ TA))).
% 29.81/8.31 thf(sdrop_decl, type, sdrop: !> [TA: $tType]: (nat > ((stream @ TA) > (stream @ TA)))).
% 29.81/8.31 thf(member_decl, type, member: !> [TA: $tType]: (TA > ((set @ TA) > $o))).
% 29.81/8.31 thf(p_decl, type, p: ((stream @ a) > $o)).
% 29.81/8.31 thf(omega_decl, type, omega: (stream @ a)).
% 29.81/8.31 thf(234,axiom,((semiring_char_0 @ extended_enat @ (type @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Nat_Osemiring__char__0_18)).
% 29.81/8.31 thf(1036,plain,((semiring_char_0 @ extended_enat @ (type @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 29.81/8.31 thf(124,axiom,((! [TA: $tType]: ((archim1804426504_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => (? [B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ B) & (ord_less @ TA @ (inverse_inverse @ TA @ (semiring_1_of_nat @ TA @ B)) @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_ex__inverse__of__nat__less)).
% 29.81/8.31 thf(629,plain,((! [TA: $tType]: ((archim1804426504_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => (? [B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ B) & (ord_less @ TA @ (inverse_inverse @ TA @ (semiring_1_of_nat @ TA @ B)) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 29.81/8.31 thf(281,axiom,((! [A:nat]: ((times_times @ nat @ A @ (zero_zero @ nat)) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_mult__0__right)).
% 29.81/8.31 thf(1168,plain,((! [A:nat]: ((times_times @ nat @ A @ (zero_zero @ nat)) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[281])).
% 29.81/8.31 thf(259,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ A @ (zero_zero @ TA)) => (ord_less @ TA @ (inverse_inverse @ TA @ A) @ (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_negative__imp__inverse__negative)).
% 29.81/8.31 thf(1105,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ A @ (zero_zero @ TA)) => (ord_less @ TA @ (inverse_inverse @ TA @ A) @ (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 29.81/8.31 thf(205,axiom,(((extended_size_enat @ (extend1396239628finity @ extended_enat)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_enat_Osize_I2_J)).
% 29.81/8.31 thf(893,plain,(((extended_size_enat @ (extend1396239628finity @ extended_enat)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 29.81/8.31 thf(88,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:TA,C:nat]: ((extended_rec_enat @ TA @ A @ B @ (extended_enat2 @ C)) = (A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_enat_Osimps_I6_J)).
% 29.81/8.31 thf(518,plain,((! [TA: $tType]: (! [A:(nat > TA),B:TA,C:nat]: ((extended_rec_enat @ TA @ (A) @ B @ (extended_enat2 @ C)) = (A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 29.81/8.31 thf(103,axiom,((! [TA: $tType]: (! [A:(TA > nat),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ nat @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_measure__induct__rule)).
% 29.81/8.31 thf(555,plain,((! [TA: $tType]: (! [A:(TA > nat),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ nat @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 29.81/8.31 thf(261,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B) => ((coindu1365464361scount @ TA @ A @ B) = (zero_zero @ extended_enat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_scount__eq__0I)).
% 29.81/8.31 thf(1110,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B) => ((coindu1365464361scount @ TA @ (A) @ B) = (zero_zero @ extended_enat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 29.81/8.31 thf(24,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o),C:(stream @ TA)]: ((linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((A @ D) => (linear505997466_on_ev @ TA @ B @ D))) @ C) => (linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((linear505997466_on_ev @ TA @ A @ D) => (linear505997466_on_ev @ TA @ B @ D))) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_alw__impl__ev__alw)).
% 29.81/8.31 thf(352,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o),C:(stream @ TA)]: ((linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((A @ D) => (linear505997466_on_ev @ TA @ B @ D))) @ C) => (linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((linear505997466_on_ev @ TA @ A @ D) => (linear505997466_on_ev @ TA @ B @ D))) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 29.81/8.31 thf(18,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((^ [B:(stream @ TA)]: ~ (linear1386806755on_alw @ TA @ A @ B)) = (linear505997466_on_ev @ TA @ (^ [B:(stream @ TA)]: ~ (A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_not__alw)).
% 29.81/8.31 thf(333,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((^ [B:(stream @ TA)]: ~ (linear1386806755on_alw @ TA @ A @ B)) = (linear505997466_on_ev @ TA @ (^ [B:(stream @ TA)]: ~ (A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 29.81/8.31 thf(232,axiom,((! [A:int,B:int]: ((ord_less @ nat @ (nat2 @ A) @ (nat2 @ B)) = ((ord_less @ int @ (zero_zero @ int) @ B) & (ord_less @ int @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_zless__nat__conj)).
% 29.81/8.31 thf(1031,plain,((! [A:int,B:int]: ((ord_less @ nat @ (nat2 @ A) @ (nat2 @ B)) = ((ord_less @ int @ (zero_zero @ int) @ B) & (ord_less @ int @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 29.81/8.31 thf(214,axiom,((! [TA: $tType]: ((division_ring @ TA @ (type @ TA)) => (! [A:TA]: (((inverse_inverse @ TA @ A) = (zero_zero @ TA)) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_inverse__nonzero__iff__nonzero)).
% 29.81/8.31 thf(977,plain,((! [TA: $tType]: ((division_ring @ TA @ (type @ TA)) => (! [A:TA]: (((inverse_inverse @ TA @ A) = (zero_zero @ TA)) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 29.81/8.31 thf(163,axiom,((! [TA: $tType]: ((linordered_idom @ TA @ (type @ 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_171_linorder__neqE__linordered__idom)).
% 29.81/8.31 thf(762,plain,((! [TA: $tType]: ((linordered_idom @ TA @ (type @ 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)],[163])).
% 29.81/8.31 thf(64,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA @ (type @ TA)) => (! [A:nat]: ((archimedean_ceiling @ TA @ (semiring_1_of_nat @ TA @ A)) = (semiring_1_of_nat @ int @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_ceiling__of__nat)).
% 29.81/8.31 thf(449,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA @ (type @ TA)) => (! [A:nat]: ((archimedean_ceiling @ TA @ (semiring_1_of_nat @ TA @ A)) = (semiring_1_of_nat @ int @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 29.81/8.31 thf(118,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_43_linorder__neqE__nat)).
% 29.81/8.31 thf(614,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)],[118])).
% 29.81/8.31 thf(195,axiom,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)) => ((ord_less @ TA @ (zero_zero @ TA) @ B) => (ord_less @ TA @ (zero_zero @ TA) @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_zero__less__mult__pos2)).
% 29.81/8.31 thf(861,plain,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)) => ((ord_less @ TA @ (zero_zero @ TA) @ B) => (ord_less @ TA @ (zero_zero @ TA) @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 29.81/8.31 thf(275,axiom,((linordered_semidom @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Olinordered__semidom_5)).
% 29.81/8.31 thf(1142,plain,((linordered_semidom @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[275])).
% 29.81/8.31 thf(34,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((linear1341015445_UNTIL @ TA @ A @ (^ [B:(stream @ TA)]: (($false)))) = (linear1386806755on_alw @ TA @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_until__false)).
% 29.81/8.31 thf(379,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((linear1341015445_UNTIL @ TA @ A @ (^ [B:(stream @ TA)]: (($false)))) = (linear1386806755on_alw @ TA @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 29.81/8.31 thf(61,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ A @ B) => ((linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((A @ D) => (C @ D))) @ B) => (linear1386806755on_alw @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_alw__mp)).
% 29.81/8.31 thf(440,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ (A) @ B) => ((linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((A @ D) => (C @ D))) @ B) => (linear1386806755on_alw @ TA @ (C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 29.81/8.31 thf(128,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: (((coindu76177514sfirst @ TA @ A @ B) = (zero_zero @ extended_enat)) = (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_sfirst__eq__0)).
% 29.81/8.31 thf(655,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: (((coindu76177514sfirst @ TA @ (A) @ B) = (zero_zero @ extended_enat)) = (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 29.81/8.31 thf(86,axiom,((! [A:nat,B:nat]: ((ord_less @ extended_enat @ (extended_enat2 @ A) @ (extended_enat2 @ B)) = (ord_less @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_enat__ord__simps_I2_J)).
% 29.81/8.31 thf(511,plain,((! [A:nat,B:nat]: ((ord_less @ extended_enat @ (extended_enat2 @ A) @ (extended_enat2 @ B)) = (ord_less @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 29.81/8.31 thf(36,axiom,((linordered_idom @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Olinordered__idom)).
% 29.81/8.31 thf(385,plain,((linordered_idom @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 29.81/8.31 thf(273,axiom,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => ((ord_less @ TA @ B @ (zero_zero @ TA)) => (ord_less @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_mult__pos__neg)).
% 29.81/8.31 thf(1137,plain,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => ((ord_less @ TA @ B @ (zero_zero @ TA)) => (ord_less @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[273])).
% 29.81/8.31 thf(147,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type @ TA)) => (! [A:TA]: ((A != (zero_zero @ TA)) => (ord_less @ TA @ (zero_zero @ TA) @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_gr__zeroI)).
% 29.81/8.31 thf(715,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type @ TA)) => (! [A:TA]: ((~ (A = (zero_zero @ TA))) => (ord_less @ TA @ (zero_zero @ TA) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 29.81/8.31 thf(72,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((! [C:(stream @ TA)]: (A @ C)) => (linear1386806755on_alw @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_all__imp__alw)).
% 29.81/8.31 thf(472,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((! [C:(stream @ TA)]: (A @ C)) => (linear1386806755on_alw @ TA @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 29.81/8.31 thf(179,axiom,((semiring_1 @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Osemiring__1_10)).
% 29.81/8.31 thf(814,plain,((semiring_1 @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 29.81/8.31 thf(140,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ (zero_zero @ TA) @ A) => (ord_less @ TA @ (inverse_inverse @ TA @ B) @ (inverse_inverse @ TA @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_less__imp__inverse__less)).
% 29.81/8.31 thf(698,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ (zero_zero @ TA) @ A) => (ord_less @ TA @ (inverse_inverse @ TA @ B) @ (inverse_inverse @ TA @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 29.81/8.31 thf(158,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ int @ (archimedean_ceiling @ TA @ A) @ (archimedean_ceiling @ TA @ B)) => (ord_less @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_ceiling__less__cancel)).
% 29.81/8.31 thf(747,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ int @ (archimedean_ceiling @ TA @ A) @ (archimedean_ceiling @ TA @ B)) => (ord_less @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 29.81/8.31 thf(21,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o),D:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ A @ B) => ((! [E:(stream @ TA)]: ((A @ E) => ((C @ E) = (D @ E)))) => ((linear1386806755on_alw @ TA @ C @ B) = (linear1386806755on_alw @ TA @ D @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_alw__cong)).
% 29.81/8.31 thf(340,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o),D:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ (A) @ B) => ((! [E:(stream @ TA)]: ((A @ E) => ((C @ E) = (D @ E)))) => ((linear1386806755on_alw @ TA @ (C) @ B) = (linear1386806755on_alw @ TA @ (D) @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 29.81/8.31 thf(96,axiom,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ (zero_zero @ TA)) => ((ord_less @ TA @ B @ (zero_zero @ TA)) => (ord_less @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_mult__neg__neg)).
% 29.81/8.31 thf(538,plain,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ (zero_zero @ TA)) => ((ord_less @ TA @ B @ (zero_zero @ TA)) => (ord_less @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 29.81/8.31 thf(185,axiom,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ (zero_zero @ TA)) => ((ord_less @ TA @ (zero_zero @ TA) @ B) => (ord_less @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_mult__neg__pos)).
% 29.81/8.31 thf(829,plain,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ (zero_zero @ TA)) => ((ord_less @ TA @ (zero_zero @ TA) @ B) => (ord_less @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 29.81/8.31 thf(207,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_less__irrefl__nat)).
% 29.81/8.31 thf(898,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 29.81/8.31 thf(170,axiom,((! [A:extended_enat]: ((A != (extend1396239628finity @ extended_enat)) = (? [B:nat]: (A = (extended_enat2 @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_not__infinity__eq)).
% 29.81/8.31 thf(782,plain,((! [A:extended_enat]: ((~ (A = (extend1396239628finity @ extended_enat))) = (? [B:nat]: (A = (extended_enat2 @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 29.81/8.31 thf(13,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((^ [B:(stream @ TA)]: ~ (linear505997466_on_ev @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B)) = (linear1386806755on_alw @ TA @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_not__ev__not)).
% 29.81/8.31 thf(320,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((^ [B:(stream @ TA)]: ~ (linear505997466_on_ev @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B)) = (linear1386806755on_alw @ TA @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 29.81/8.31 thf(58,axiom,((semiring_char_0 @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Nat_Osemiring__char__0)).
% 29.81/8.31 thf(436,plain,((semiring_char_0 @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 29.81/8.31 thf(127,axiom,((! [A:extended_enat,B:nat]: ((ord_less @ extended_enat @ A @ (extended_enat2 @ B)) => (? [C:nat]: (A = (extended_enat2 @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_enat__iless)).
% 29.81/8.31 thf(651,plain,((! [A:extended_enat,B:nat]: ((ord_less @ extended_enat @ A @ (extended_enat2 @ B)) => (? [C:nat]: (A = (extended_enat2 @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 29.81/8.31 thf(190,axiom,((! [A:extended_enat]: ((! [B:nat]: (A != (extended_enat2 @ B))) => (A = (extend1396239628finity @ extended_enat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_enat_Oexhaust)).
% 29.81/8.31 thf(841,plain,((! [A:extended_enat]: ((! [B:nat]: ~ (A = (extended_enat2 @ B))) => (A = (extend1396239628finity @ extended_enat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 29.81/8.31 thf(51,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_2_1_T)).
% 29.81/8.31 thf(417,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 29.81/8.31 thf(213,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_less__not__refl3)).
% 29.81/8.31 thf(973,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 29.81/8.31 thf(238,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) = (A != (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_zero__less__iff__neq__zero)).
% 29.81/8.31 thf(1046,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) = (~ (A = (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 29.81/8.31 thf(40,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ B)) = (B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_mem__Collect__eq)).
% 29.81/8.31 thf(389,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ (B))) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 29.81/8.31 thf(150,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) => (((times_times @ nat @ A @ B) = (times_times @ nat @ A @ C)) = (B = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_nat__mult__eq__cancel1)).
% 29.81/8.31 thf(724,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) => (((times_times @ nat @ A @ B) = (times_times @ nat @ A @ C)) = (B = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 29.81/8.31 thf(171,axiom,((! [A:(extended_enat > $o),B:extended_enat]: ((! [C:extended_enat]: ((! [D:extended_enat]: ((ord_less @ extended_enat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_enat__less__induct)).
% 29.81/8.31 thf(785,plain,((! [A:(extended_enat > $o),B:extended_enat]: ((! [C:extended_enat]: ((! [D:extended_enat]: ((ord_less @ extended_enat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 29.81/8.31 thf(32,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o),C:(stream @ TA),D:((stream @ TA) > $o)]: ((linear1341015445_UNTIL @ TA @ A @ B @ C) => ((! [E:(stream @ TA)]: ((A @ E) => (D @ E))) => (linear1341015445_UNTIL @ TA @ D @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_until__monoL)).
% 29.81/8.31 thf(372,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o),C:(stream @ TA),D:((stream @ TA) > $o)]: ((linear1341015445_UNTIL @ TA @ (A) @ (B) @ C) => ((! [E:(stream @ TA)]: ((A @ E) => (D @ E))) => (linear1341015445_UNTIL @ TA @ (D) @ (B) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 29.81/8.31 thf(189,axiom,((! [TA: $tType]: ((mult_zero @ TA @ (type @ TA)) => (! [A:TA]: ((times_times @ TA @ A @ (zero_zero @ TA)) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_mult__zero__right)).
% 29.81/8.31 thf(838,plain,((! [TA: $tType]: ((mult_zero @ TA @ (type @ TA)) => (! [A:TA]: ((times_times @ TA @ A @ (zero_zero @ TA)) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 29.81/8.31 thf(174,axiom,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ (zero_zero @ TA) @ C) => (ord_less @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_mult__strict__right__mono)).
% 29.81/8.31 thf(802,plain,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ (zero_zero @ TA) @ C) => (ord_less @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 29.81/8.31 thf(243,axiom,((! [TA: $tType]: ((semiri1923998003cancel @ TA @ (type @ 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_153_mult__cancel__right)).
% 29.81/8.31 thf(1059,plain,((! [TA: $tType]: ((semiri1923998003cancel @ TA @ (type @ 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)],[243])).
% 29.81/8.31 thf(68,axiom,((mult_zero @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Omult__zero)).
% 29.81/8.31 thf(460,plain,((mult_zero @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 29.81/8.31 thf(253,axiom,(((extended_the_enat @ (zero_zero @ extended_enat)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_the__enat__0)).
% 29.81/8.31 thf(1087,plain,(((extended_the_enat @ (zero_zero @ extended_enat)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 29.81/8.31 thf(199,axiom,(((nat2 @ (zero_zero @ int)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_nat__0)).
% 29.81/8.31 thf(870,plain,(((nat2 @ (zero_zero @ int)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 29.81/8.31 thf(201,axiom,((! [A:extended_enat,B:extended_enat]: (((times_times @ extended_enat @ A @ B) = (extend1396239628finity @ extended_enat)) = (((A = (extend1396239628finity @ extended_enat)) & (B != (zero_zero @ extended_enat))) | ((B = (extend1396239628finity @ extended_enat)) & (A != (zero_zero @ extended_enat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_imult__is__infinity)).
% 29.81/8.31 thf(881,plain,((! [A:extended_enat,B:extended_enat]: (((times_times @ extended_enat @ A @ B) = (extend1396239628finity @ extended_enat)) = (((A = (extend1396239628finity @ extended_enat)) & ~ (B = (zero_zero @ extended_enat))) | ((B = (extend1396239628finity @ extended_enat)) & ~ (A = (zero_zero @ extended_enat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 29.81/8.31 thf(256,axiom,((! [TA: $tType]: ((semiri1193490041visors @ TA @ (type @ 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_155_mult__eq__0__iff)).
% 29.81/8.31 thf(1100,plain,((! [TA: $tType]: ((semiri1193490041visors @ TA @ (type @ 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)],[256])).
% 29.81/8.31 thf(236,axiom,((! [TA: $tType]: ((linear505997466_on_ev @ TA) = (^ [A:((stream @ TA) > $o),B:(stream @ TA)]: ? [C:nat]: (A @ (sdrop @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_ev__iff__sdrop)).
% 29.81/8.31 thf(1040,plain,((! [TA: $tType]: ((linear505997466_on_ev @ TA) = (^ [A:((stream @ TA) > $o),B:(stream @ TA)]: ? [C:nat]: (A @ (sdrop @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 29.81/8.31 thf(33,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ 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_223_semiring__normalization__rules_I19_J)).
% 29.81/8.31 thf(376,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ 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)],[33])).
% 29.81/8.31 thf(121,axiom,((semiring_1 @ extended_enat @ (type @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Rings_Osemiring__1_19)).
% 29.81/8.31 thf(623,plain,((semiring_1 @ extended_enat @ (type @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 29.81/8.31 thf(87,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) => ((ord_less @ nat @ (times_times @ nat @ A @ B) @ (times_times @ nat @ A @ C)) = (ord_less @ nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_nat__mult__less__cancel1)).
% 29.81/8.31 thf(514,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) => ((ord_less @ nat @ (times_times @ nat @ A @ B) @ (times_times @ nat @ A @ C)) = (ord_less @ nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 29.81/8.31 thf(287,axiom,((! [A:nat]: (ord_less @ extended_enat @ (extended_enat2 @ A) @ (extend1396239628finity @ extended_enat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_enat__ord__code_I4_J)).
% 29.81/8.31 thf(1183,plain,((! [A:nat]: (ord_less @ extended_enat @ (extended_enat2 @ A) @ (extend1396239628finity @ extended_enat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[287])).
% 29.81/8.31 thf(74,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ((linear1386806755on_alw @ TA @ A @ C) => (linear505997466_on_ev @ TA @ B @ C)))) = (^ [C:(stream @ TA)]: ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ A) @ C) => (linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ B) @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_alw__alw__impl__ev)).
% 29.81/8.31 thf(480,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ((linear1386806755on_alw @ TA @ A @ C) => (linear505997466_on_ev @ TA @ B @ C)))) = (^ [C:(stream @ TA)]: ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ A) @ C) => (linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ B) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 29.81/8.31 thf(240,axiom,((((?) @ extended_enat) = (^ [A:(extended_enat > $o)]: ((A @ (extend1396239628finity @ extended_enat)) | ? [B:nat]: (A @ (extended_enat2 @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_enat__ex__split)).
% 29.81/8.31 thf(1051,plain,((((?) @ extended_enat) = (^ [A:(extended_enat > $o)]: ((A @ (extend1396239628finity @ extended_enat)) | ? [B:nat]: (A @ (extended_enat2 @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 29.81/8.31 thf(181,axiom,((semiring_char_0 @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Nat_Osemiring__char__0_9)).
% 29.81/8.31 thf(821,plain,((semiring_char_0 @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 29.81/8.31 thf(153,axiom,((! [A:nat,B:nat]: (((extended_enat2 @ A) = (extended_enat2 @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_enat_Oinject)).
% 29.81/8.31 thf(734,plain,((! [A:nat,B:nat]: (((extended_enat2 @ A) = (extended_enat2 @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 29.81/8.31 thf(265,axiom,((zero @ extended_enat @ (type @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Groups_Ozero_21)).
% 29.81/8.31 thf(1119,plain,((zero @ extended_enat @ (type @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[265])).
% 29.81/8.31 thf(219,axiom,(((times_times @ extended_enat @ (extend1396239628finity @ extended_enat) @ (extend1396239628finity @ extended_enat)) = (extend1396239628finity @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_times__enat__simps_I2_J)).
% 29.81/8.31 thf(998,plain,(((times_times @ extended_enat @ (extend1396239628finity @ extended_enat) @ (extend1396239628finity @ extended_enat)) = (extend1396239628finity @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 29.81/8.31 thf(294,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:TA,C:nat]: ((extended_case_enat @ TA @ A @ B @ (extended_enat2 @ C)) = (A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_enat_Osimps_I4_J)).
% 29.81/8.31 thf(1201,plain,((! [TA: $tType]: (! [A:(nat > TA),B:TA,C:nat]: ((extended_case_enat @ TA @ (A) @ B @ (extended_enat2 @ C)) = (A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[294])).
% 29.81/8.31 thf(258,axiom,((semigroup_mult @ extended_enat @ (type @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Groups_Osemigroup__mult_17)).
% 29.81/8.31 thf(1104,plain,((semigroup_mult @ extended_enat @ (type @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 29.81/8.31 thf(92,axiom,((! [TA: $tType]: (! [A:nat,B:((stream @ TA) > $o),C:(stream @ TA)]: ((ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu76177514sfirst @ TA @ B @ C)) => (~ (B @ (sdrop @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_less__sfirstD)).
% 29.81/8.31 thf(527,plain,((! [TA: $tType]: (! [A:nat,B:((stream @ TA) > $o),C:(stream @ TA)]: ((ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu76177514sfirst @ TA @ (B) @ C)) => (~ (B @ (sdrop @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 29.81/8.31 thf(43,axiom,((! [TA: $tType]: ((ab_semigroup_mult @ TA @ (type @ TA)) => ((times_times @ TA) = (^ [A:TA,B:TA]: (times_times @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_mult_Ocommute)).
% 29.81/8.31 thf(397,plain,((! [TA: $tType]: ((ab_semigroup_mult @ TA @ (type @ TA)) => ((times_times @ TA) = (^ [A:TA,B:TA]: (times_times @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 29.81/8.31 thf(138,axiom,(((size_size @ extended_enat @ (extend1396239628finity @ extended_enat)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_enat_Osize_I4_J)).
% 29.81/8.31 thf(687,plain,(((size_size @ extended_enat @ (extend1396239628finity @ extended_enat)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 29.81/8.31 thf(8,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((A @ B) => (linear1341015445_UNTIL @ TA @ C @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_UNTIL_Obase)).
% 29.81/8.31 thf(307,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((A @ B) => (linear1341015445_UNTIL @ TA @ (C) @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 29.81/8.31 thf(247,axiom,((! [A:extended_enat]: ((! [B:nat]: (A != (extended_enat2 @ B))) = (A = (extend1396239628finity @ extended_enat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_not__enat__eq)).
% 29.81/8.31 thf(1074,plain,((! [A:extended_enat]: ((! [B:nat]: ~ (A = (extended_enat2 @ B))) = (A = (extend1396239628finity @ extended_enat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 29.81/8.31 thf(65,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ A @ (times_times @ TA @ B @ C)) = (times_times @ TA @ (times_times @ TA @ A @ B) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_semiring__normalization__rules_I18_J)).
% 29.81/8.31 thf(452,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ A @ (times_times @ TA @ B @ C)) = (times_times @ TA @ (times_times @ TA @ A @ B) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 29.81/8.31 thf(60,axiom,((semiri1923998003cancel @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Osemiring__no__zero__divisors__cancel)).
% 29.81/8.31 thf(439,plain,((semiri1923998003cancel @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 29.81/8.31 thf(93,axiom,((! [A:nat]: ((finite_card @ nat @ (collect @ nat @ (^ [B:nat]: (ord_less @ nat @ B @ A)))) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_card__Collect__less__nat)).
% 29.81/8.31 thf(529,plain,((! [A:nat]: ((finite_card @ nat @ (collect @ nat @ (^ [B:nat]: (ord_less @ nat @ B @ A)))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 29.81/8.31 thf(130,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_less__not__refl)).
% 29.81/8.31 thf(661,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 29.81/8.31 thf(177,axiom,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ (zero_zero @ TA)) => (ord_less @ TA @ (times_times @ TA @ B @ C) @ (times_times @ TA @ A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_mult__strict__right__mono__neg)).
% 29.81/8.31 thf(810,plain,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ (zero_zero @ TA)) => (ord_less @ TA @ (times_times @ TA @ B @ C) @ (times_times @ TA @ A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 29.81/8.31 thf(30,axiom,((! [TA: $tType]: ((extended_case_enat @ TA) = (extended_rec_enat @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_case__enat__def)).
% 29.81/8.31 thf(366,plain,((! [TA: $tType]: ((extended_case_enat @ TA) = (extended_rec_enat @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 29.81/8.31 thf(245,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_gr__implies__not__zero)).
% 29.81/8.31 thf(1067,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 29.81/8.31 thf(210,axiom,((! [A:extended_enat,B:extended_enat,C:extended_enat]: (((? [D:nat]: (A = (extended_enat2 @ D))) => ((? [D:nat]: (B = (extended_enat2 @ D))) => (! [D:nat]: (C != (extended_enat2 @ D))))) => (((? [D:nat]: (A = (extended_enat2 @ D))) => ((? [D:nat]: (B = (extended_enat2 @ D))) => (C != (extend1396239628finity @ extended_enat)))) => (((? [D:nat]: (A = (extended_enat2 @ D))) => ((B = (extend1396239628finity @ extended_enat)) => (! [D:nat]: (C != (extended_enat2 @ D))))) => (((? [D:nat]: (A = (extended_enat2 @ D))) => ((B = (extend1396239628finity @ extended_enat)) => (C != (extend1396239628finity @ extended_enat)))) => (((A = (extend1396239628finity @ extended_enat)) => ((? [D:nat]: (B = (extended_enat2 @ D))) => (! [D:nat]: (C != (extended_enat2 @ D))))) => (((A = (extend1396239628finity @ extended_enat)) => ((? [D:nat]: (B = (extended_enat2 @ D))) => (C != (extend1396239628finity @ extended_enat)))) => (((A = (extend1396239628finity @ extended_enat)) => ((B = (extend1396239628finity @ extended_enat)) => (! [D:nat]: (C != (extended_enat2 @ D))))) => (~ ((A = (extend1396239628finity @ extended_enat)) => ((B = (extend1396239628finity @ extended_enat)) => (C != (extend1396239628finity @ extended_enat)))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_enat3__cases)).
% 29.81/8.31 thf(910,plain,((! [A:extended_enat,B:extended_enat,C:extended_enat]: (((? [D:nat]: (A = (extended_enat2 @ D))) => ((? [D:nat]: (B = (extended_enat2 @ D))) => (! [D:nat]: ~ (C = (extended_enat2 @ D))))) => (((? [D:nat]: (A = (extended_enat2 @ D))) => ((? [D:nat]: (B = (extended_enat2 @ D))) => (~ (C = (extend1396239628finity @ extended_enat))))) => (((? [D:nat]: (A = (extended_enat2 @ D))) => ((B = (extend1396239628finity @ extended_enat)) => (! [D:nat]: ~ (C = (extended_enat2 @ D))))) => (((? [D:nat]: (A = (extended_enat2 @ D))) => ((B = (extend1396239628finity @ extended_enat)) => (~ (C = (extend1396239628finity @ extended_enat))))) => (((A = (extend1396239628finity @ extended_enat)) => ((? [D:nat]: (B = (extended_enat2 @ D))) => (! [D:nat]: ~ (C = (extended_enat2 @ D))))) => (((A = (extend1396239628finity @ extended_enat)) => ((? [D:nat]: (B = (extended_enat2 @ D))) => (~ (C = (extend1396239628finity @ extended_enat))))) => (((A = (extend1396239628finity @ extended_enat)) => ((B = (extend1396239628finity @ extended_enat)) => (! [D:nat]: ~ (C = (extended_enat2 @ D))))) => (~ ((A = (extend1396239628finity @ extended_enat)) => ((B = (extend1396239628finity @ extended_enat)) => (~ (C = (extend1396239628finity @ extended_enat))))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 29.81/8.31 thf(183,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:TA]: ((extended_case_enat @ TA @ A @ B @ (zero_zero @ extended_enat)) = (A @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_case__enat__0)).
% 29.81/8.31 thf(825,plain,((! [TA: $tType]: (! [A:(nat > TA),B:TA]: ((extended_case_enat @ TA @ (A) @ B @ (zero_zero @ extended_enat)) = (A @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 29.81/8.31 thf(5,axiom,((linordered_semidom @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Olinordered__semidom)).
% 29.81/8.31 thf(302,plain,((linordered_semidom @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 29.81/8.31 thf(23,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_46_Collect__cong)).
% 29.81/8.31 thf(349,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)],[23])).
% 29.81/8.31 thf(283,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ (zero_zero @ TA)) => (ord_less @ TA @ (inverse_inverse @ TA @ B) @ (inverse_inverse @ TA @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_less__imp__inverse__less__neg)).
% 29.81/8.31 thf(1174,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ (zero_zero @ TA)) => (ord_less @ TA @ (inverse_inverse @ TA @ B) @ (inverse_inverse @ TA @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[283])).
% 29.81/8.31 thf(104,axiom,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)) => ((ord_less @ TA @ (zero_zero @ TA) @ A) => (ord_less @ TA @ (zero_zero @ TA) @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_zero__less__mult__pos)).
% 29.81/8.31 thf(561,plain,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)) => ((ord_less @ TA @ (zero_zero @ TA) @ A) => (ord_less @ TA @ (zero_zero @ TA) @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 29.81/8.31 thf(41,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ A @ B) => ((linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((A @ D) => (linear505997466_on_ev @ TA @ C @ D))) @ B) => (linear505997466_on_ev @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_ev__alw__impl__ev)).
% 29.81/8.31 thf(392,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ (A) @ B) => ((linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((A @ D) => (linear505997466_on_ev @ TA @ C @ D))) @ B) => (linear505997466_on_ev @ TA @ (C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 29.81/8.31 thf(3,axiom,((! [TA: $tType]: (! [A:(stream @ TA)]: ~ (linear1386806755on_alw @ TA @ (^ [B:(stream @ TA)]: (($false))) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_alw__False)).
% 29.81/8.31 thf(297,plain,((! [TA: $tType]: (! [A:(stream @ TA)]: ~ (linear1386806755on_alw @ TA @ (^ [B:(stream @ TA)]: (($false))) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 29.81/8.31 thf(53,axiom,((! [TA: $tType]: ((semiring_1 @ TA @ (type @ TA)) => (! [A:nat,B:TA]: ((times_times @ TA @ (semiring_1_of_nat @ TA @ A) @ B) = (times_times @ TA @ B @ (semiring_1_of_nat @ TA @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_mult__of__nat__commute)).
% 29.81/8.31 thf(424,plain,((! [TA: $tType]: ((semiring_1 @ TA @ (type @ TA)) => (! [A:nat,B:TA]: ((times_times @ TA @ (semiring_1_of_nat @ TA @ A) @ B) = (times_times @ TA @ B @ (semiring_1_of_nat @ TA @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 29.81/8.31 thf(47,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ A) @ B) => ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ C) @ B) => (linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((A @ D) & (C @ D)))) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_ev__alw__aand)).
% 29.81/8.31 thf(407,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ A) @ B) => ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ C) @ B) => (linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((A @ D) & (C @ D)))) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 29.81/8.31 thf(180,axiom,((! [A:(extended_enat > $o),B:extended_enat]: ((! [C:nat]: (A @ (extended_enat2 @ C))) => ((A @ (extend1396239628finity @ extended_enat)) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_enat_Oinducts)).
% 29.81/8.31 thf(815,plain,((! [A:(extended_enat > $o),B:extended_enat]: ((! [C:nat]: (A @ (extended_enat2 @ C))) => ((A @ (extend1396239628finity @ extended_enat)) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 29.81/8.31 thf(157,axiom,((linord20386208strict @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Olinordered__semiring__strict_3)).
% 29.81/8.31 thf(746,plain,((linord20386208strict @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 29.81/8.31 thf(255,axiom,((! [A:nat]: (((A = (zero_zero @ nat)) => ((times_times @ extended_enat @ (extended_enat2 @ A) @ (extend1396239628finity @ extended_enat)) = (zero_zero @ extended_enat))) & ((A != (zero_zero @ nat)) => ((times_times @ extended_enat @ (extended_enat2 @ A) @ (extend1396239628finity @ extended_enat)) = (extend1396239628finity @ extended_enat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_times__enat__simps_I4_J)).
% 29.81/8.31 thf(1091,plain,((! [A:nat]: (((A = (zero_zero @ nat)) => ((times_times @ extended_enat @ (extended_enat2 @ A) @ (extend1396239628finity @ extended_enat)) = (zero_zero @ extended_enat))) & ((~ (A = (zero_zero @ nat))) => ((times_times @ extended_enat @ (extended_enat2 @ A) @ (extend1396239628finity @ extended_enat)) = (extend1396239628finity @ extended_enat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 29.81/8.31 thf(106,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => ((ord_less @ nat @ (zero_zero @ nat) @ C) => (ord_less @ nat @ (times_times @ nat @ A @ C) @ (times_times @ nat @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_mult__less__mono1)).
% 29.81/8.31 thf(566,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => ((ord_less @ nat @ (zero_zero @ nat) @ C) => (ord_less @ nat @ (times_times @ nat @ A @ C) @ (times_times @ nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 29.81/8.31 thf(16,axiom,((! [A:nat]: ((nat2 @ (semiring_1_of_nat @ int @ A)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_nat__int)).
% 29.81/8.31 thf(329,plain,((! [A:nat]: ((nat2 @ (semiring_1_of_nat @ int @ A)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 29.81/8.31 thf(69,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: ((times_times @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ C @ D)) = (times_times @ TA @ C @ (times_times @ TA @ (times_times @ TA @ A @ B) @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_semiring__normalization__rules_I15_J)).
% 29.81/8.31 thf(461,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: ((times_times @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ C @ D)) = (times_times @ TA @ C @ (times_times @ TA @ (times_times @ TA @ A @ B) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 29.81/8.31 thf(249,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type @ TA)) => (! [A:TA]: ~ (ord_less @ TA @ A @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_not__less__zero)).
% 29.81/8.31 thf(1079,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type @ TA)) => (! [A:TA]: ~ (ord_less @ TA @ A @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 29.81/8.31 thf(225,axiom,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ C @ B)) = (((ord_less @ TA @ (zero_zero @ TA) @ B) & (ord_less @ TA @ A @ C)) | ((ord_less @ TA @ B @ (zero_zero @ TA)) & (ord_less @ TA @ C @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_mult__less__cancel__right__disj)).
% 29.81/8.31 thf(1012,plain,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ C @ B)) = (((ord_less @ TA @ (zero_zero @ TA) @ B) & (ord_less @ TA @ A @ C)) | ((ord_less @ TA @ B @ (zero_zero @ TA)) & (ord_less @ TA @ C @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 29.81/8.31 thf(136,axiom,((! [TA: $tType]: (! [A:(TA > extended_enat),B:nat]: ((! [C:TA]: ? [D:TA]: (ord_less @ extended_enat @ (A @ C) @ (A @ D))) => (? [C:TA]: (ord_less @ extended_enat @ (extended_enat2 @ B) @ (A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_chain__incr)).
% 29.81/8.31 thf(682,plain,((! [TA: $tType]: (! [A:(TA > extended_enat),B:nat]: ((! [C:TA]: ? [D:TA]: (ord_less @ extended_enat @ (A @ C) @ (A @ D))) => (? [C:TA]: (ord_less @ extended_enat @ (extended_enat2 @ B) @ (A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 29.81/8.31 thf(292,axiom,((! [A:int]: ((times_times @ int @ A @ (zero_zero @ int)) = (zero_zero @ int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_times__int__code_I1_J)).
% 29.81/8.31 thf(1195,plain,((! [A:int]: ((times_times @ int @ A @ (zero_zero @ int)) = (zero_zero @ int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[292])).
% 29.81/8.31 thf(101,axiom,(((times_times @ extended_enat) = (^ [A:extended_enat,B:extended_enat]: (extended_case_enat @ extended_enat @ (^ [C:nat]: (extended_case_enat @ extended_enat @ (^ [D:nat]: (extended_enat2 @ (times_times @ nat @ C @ D))) @ (if @ extended_enat @ (C = (zero_zero @ nat)) @ (zero_zero @ extended_enat) @ (extend1396239628finity @ extended_enat)) @ B)) @ (if @ extended_enat @ (B = (zero_zero @ extended_enat)) @ (zero_zero @ extended_enat) @ (extend1396239628finity @ extended_enat)) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_times__enat__def)).
% 29.81/8.31 thf(551,plain,(((times_times @ extended_enat) = (^ [A:extended_enat,B:extended_enat]: (extended_case_enat @ extended_enat @ (^ [C:nat]: (extended_case_enat @ extended_enat @ (^ [D:nat]: (extended_enat2 @ (times_times @ nat @ C @ D))) @ (if @ extended_enat @ (C = (zero_zero @ nat)) @ (zero_zero @ extended_enat) @ (extend1396239628finity @ extended_enat)) @ B)) @ (if @ extended_enat @ (B = (zero_zero @ extended_enat)) @ (zero_zero @ extended_enat) @ (extend1396239628finity @ extended_enat)) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 29.81/8.31 thf(269,axiom,(((ord_less @ extended_enat) = (^ [A:extended_enat,B:extended_enat]: (extended_case_enat @ $o @ (^ [C:nat]: (extended_case_enat @ $o @ (ord_less @ nat @ C) @ ($true) @ B)) @ ($false) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_less__enat__def)).
% 29.81/8.31 thf(1128,plain,(((ord_less @ extended_enat) = (^ [A:extended_enat,B:extended_enat]: (extended_case_enat @ $o @ (^ [C:nat]: (extended_case_enat @ $o @ (ord_less @ nat @ C) @ ($true) @ B)) @ ($false) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 29.81/8.31 thf(254,axiom,(((semiring_1_of_nat @ extended_enat) = extended_enat2)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_of__nat__eq__enat)).
% 29.81/8.31 thf(1089,plain,(((semiring_1_of_nat @ extended_enat) = (extended_enat2))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 29.81/8.31 thf(276,axiom,((! [A:nat]: (((A = (zero_zero @ nat)) => ((times_times @ extended_enat @ (extend1396239628finity @ extended_enat) @ (extended_enat2 @ A)) = (zero_zero @ extended_enat))) & ((A != (zero_zero @ nat)) => ((times_times @ extended_enat @ (extend1396239628finity @ extended_enat) @ (extended_enat2 @ A)) = (extend1396239628finity @ extended_enat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_times__enat__simps_I3_J)).
% 29.81/8.31 thf(1143,plain,((! [A:nat]: (((A = (zero_zero @ nat)) => ((times_times @ extended_enat @ (extend1396239628finity @ extended_enat) @ (extended_enat2 @ A)) = (zero_zero @ extended_enat))) & ((~ (A = (zero_zero @ nat))) => ((times_times @ extended_enat @ (extend1396239628finity @ extended_enat) @ (extended_enat2 @ A)) = (extend1396239628finity @ extended_enat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[276])).
% 29.81/8.31 thf(12,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => ((times_times @ TA) = (^ [A:TA,B:TA]: (times_times @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_semiring__normalization__rules_I7_J)).
% 29.81/8.31 thf(317,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => ((times_times @ TA) = (^ [A:TA,B:TA]: (times_times @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 29.81/8.31 thf(126,axiom,((mult_zero @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Omult__zero_11)).
% 29.81/8.31 thf(650,plain,((mult_zero @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 29.81/8.31 thf(222,axiom,((! [A:int,B:int,C:int]: ((ord_less @ int @ A @ B) => ((ord_less @ int @ (zero_zero @ int) @ C) => (ord_less @ int @ (times_times @ int @ C @ A) @ (times_times @ int @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_zmult__zless__mono2)).
% 29.81/8.31 thf(1006,plain,((! [A:int,B:int,C:int]: ((ord_less @ int @ A @ B) => ((ord_less @ int @ (zero_zero @ int) @ C) => (ord_less @ int @ (times_times @ int @ C @ A) @ (times_times @ int @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 29.81/8.31 thf(39,axiom,((comm_semiring_1 @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Ocomm__semiring__1)).
% 29.81/8.31 thf(388,plain,((comm_semiring_1 @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 29.81/8.31 thf(52,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ A @ B) => ((! [D:(stream @ TA)]: ((A @ D) => (C @ D))) => (linear1386806755on_alw @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_alw__mono)).
% 29.81/8.31 thf(420,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ (A) @ B) => ((! [D:(stream @ TA)]: ((A @ D) => (C @ D))) => (linear1386806755on_alw @ TA @ (C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 29.81/8.31 thf(82,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA]: ((times_times @ TA @ A @ (zero_zero @ TA)) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_semiring__normalization__rules_I10_J)).
% 29.81/8.31 thf(499,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA]: ((times_times @ TA @ A @ (zero_zero @ TA)) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 29.81/8.31 thf(215,axiom,((! [TA: $tType]: ((coindu1365464361scount @ TA) = (^ [A:((stream @ TA) > $o),B:(stream @ TA)]: (if @ extended_enat @ (linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ B) @ (extend1396239628finity @ extended_enat) @ (extended_enat2 @ (finite_card @ nat @ (collect @ nat @ (^ [C:nat]: (A @ (sdrop @ TA @ C @ B))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_scount__eq)).
% 29.81/8.31 thf(980,plain,((! [TA: $tType]: ((coindu1365464361scount @ TA) = (^ [A:((stream @ TA) > $o),B:(stream @ TA)]: (if @ extended_enat @ (linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ B) @ (extend1396239628finity @ extended_enat) @ (extended_enat2 @ (finite_card @ nat @ (collect @ nat @ (^ [C:nat]: (A @ (sdrop @ TA @ C @ B))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 29.81/8.31 thf(45,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: ((times_times @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ C @ D)) = (times_times @ TA @ A @ (times_times @ TA @ B @ (times_times @ TA @ C @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_semiring__normalization__rules_I14_J)).
% 29.81/8.31 thf(403,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: ((times_times @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ C @ D)) = (times_times @ TA @ A @ (times_times @ TA @ B @ (times_times @ TA @ C @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 29.81/8.31 thf(202,axiom,((! [TA: $tType]: ((semiring_char_0 @ TA @ (type @ TA)) => (! [A:nat]: (((zero_zero @ TA) = (semiring_1_of_nat @ TA @ A)) = ((zero_zero @ nat) = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_of__nat__0__eq__iff)).
% 29.81/8.31 thf(884,plain,((! [TA: $tType]: ((semiring_char_0 @ TA @ (type @ TA)) => (! [A:nat]: (((zero_zero @ TA) = (semiring_1_of_nat @ TA @ A)) = ((zero_zero @ nat) = A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 29.81/8.31 thf(278,axiom,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ (zero_zero @ TA) @ C) => (ord_less @ TA @ (times_times @ TA @ C @ A) @ (times_times @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_mult__strict__left__mono)).
% 29.81/8.31 thf(1160,plain,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ (zero_zero @ TA) @ C) => (ord_less @ TA @ (times_times @ TA @ C @ A) @ (times_times @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 29.81/8.31 thf(231,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)) = (((ord_less @ TA @ (zero_zero @ TA) @ A) & (ord_less @ TA @ (zero_zero @ TA) @ B)) | ((ord_less @ TA @ A @ (zero_zero @ TA)) & (ord_less @ TA @ B @ (zero_zero @ TA))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_linordered__field__class_Osign__simps_I44_J)).
% 29.81/8.31 thf(1028,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)) = (((ord_less @ TA @ (zero_zero @ TA) @ A) & (ord_less @ TA @ (zero_zero @ TA) @ B)) | ((ord_less @ TA @ A @ (zero_zero @ TA)) & (ord_less @ TA @ B @ (zero_zero @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 29.81/8.31 thf(208,axiom,((! [A:int]: ((ord_less @ nat @ (zero_zero @ nat) @ (nat2 @ A)) = (ord_less @ int @ (zero_zero @ int) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_zero__less__nat__eq)).
% 29.81/8.31 thf(901,plain,((! [A:int]: ((ord_less @ nat @ (zero_zero @ nat) @ (nat2 @ A)) = (ord_less @ int @ (zero_zero @ int) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 29.81/8.31 thf(91,axiom,((canoni770627133id_add @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocanonically__ordered__monoid__add)).
% 29.81/8.31 thf(526,plain,((canoni770627133id_add @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 29.81/8.31 thf(77,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((A @ B) => (linear505997466_on_ev @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_ev_Obase)).
% 29.81/8.31 thf(489,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((A @ B) => (linear505997466_on_ev @ TA @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 29.81/8.31 thf(227,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ int @ (zero_zero @ int) @ (archimedean_ceiling @ TA @ A)) = (ord_less @ TA @ (zero_zero @ TA) @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_zero__less__ceiling)).
% 29.81/8.31 thf(1016,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ int @ (zero_zero @ int) @ (archimedean_ceiling @ TA @ A)) = (ord_less @ TA @ (zero_zero @ TA) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 29.81/8.31 thf(100,axiom,((! [A:nat]: ((extend1396239628finity @ extended_enat) != (extended_enat2 @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_enat_Odistinct_I2_J)).
% 29.81/8.31 thf(547,plain,((! [A:nat]: ~ ((extend1396239628finity @ extended_enat) = (extended_enat2 @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 29.81/8.31 thf(143,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (inverse_inverse @ TA @ A) @ (inverse_inverse @ TA @ B)) => ((ord_less @ TA @ B @ (zero_zero @ TA)) => (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_inverse__less__imp__less__neg)).
% 29.81/8.31 thf(706,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (inverse_inverse @ TA @ A) @ (inverse_inverse @ TA @ B)) => ((ord_less @ TA @ B @ (zero_zero @ TA)) => (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 29.81/8.31 thf(135,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_35_nat__neq__iff)).
% 29.81/8.31 thf(679,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)],[135])).
% 29.81/8.31 thf(212,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_not__less0)).
% 29.81/8.31 thf(970,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 29.81/8.31 thf(263,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_linordered__field__no__ub)).
% 29.81/8.31 thf(1114,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 29.81/8.31 thf(271,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: (((coindu1365464361scount @ TA @ A @ B) = (zero_zero @ extended_enat)) = (linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_scount__eq__0__iff)).
% 29.81/8.31 thf(1131,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: (((coindu1365464361scount @ TA @ (A) @ B) = (zero_zero @ extended_enat)) = (linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 29.81/8.31 thf(291,axiom,((! [TA: $tType]: ((semiri1193490041visors @ TA @ (type @ 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_176_no__zero__divisors)).
% 29.81/8.31 thf(1192,plain,((! [TA: $tType]: ((semiri1193490041visors @ TA @ (type @ 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)],[291])).
% 29.81/8.31 thf(67,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_Collect__mem__eq)).
% 29.81/8.31 thf(457,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 29.81/8.31 thf(149,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) = (ord_less @ nat @ (zero_zero @ nat) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_neq0__conv)).
% 29.81/8.31 thf(721,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) = (ord_less @ nat @ (zero_zero @ nat) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 29.81/8.31 thf(107,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (inverse_inverse @ TA @ A)) = (ord_less @ TA @ (zero_zero @ TA) @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_inverse__positive__iff__positive)).
% 29.81/8.31 thf(569,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (inverse_inverse @ TA @ A)) = (ord_less @ TA @ (zero_zero @ TA) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 29.81/8.31 thf(169,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)) = (((ord_less @ TA @ (zero_zero @ TA) @ A) & (ord_less @ TA @ B @ (zero_zero @ TA))) | ((ord_less @ TA @ A @ (zero_zero @ TA)) & (ord_less @ TA @ (zero_zero @ TA) @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_linordered__field__class_Osign__simps_I45_J)).
% 29.81/8.31 thf(779,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)) = (((ord_less @ TA @ (zero_zero @ TA) @ A) & (ord_less @ TA @ B @ (zero_zero @ TA))) | ((ord_less @ TA @ A @ (zero_zero @ TA)) & (ord_less @ TA @ (zero_zero @ TA) @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 29.81/8.31 thf(114,axiom,((! [A:extended_enat]: ~ (ord_less @ extended_enat @ A @ (zero_zero @ extended_enat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_not__iless0)).
% 29.81/8.31 thf(605,plain,((! [A:extended_enat]: ~ (ord_less @ extended_enat @ A @ (zero_zero @ extended_enat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 29.81/8.31 thf(252,axiom,((ab_semigroup_mult @ extended_enat @ (type @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Groups_Oab__semigroup__mult_15)).
% 29.81/8.31 thf(1086,plain,((ab_semigroup_mult @ extended_enat @ (type @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 29.81/8.31 thf(85,axiom,((! [A:nat,B:int]: ((ord_less @ nat @ A @ (nat2 @ B)) = (ord_less @ int @ (semiring_1_of_nat @ int @ A) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_zless__nat__eq__int__zless)).
% 29.81/8.31 thf(508,plain,((! [A:nat,B:int]: ((ord_less @ nat @ A @ (nat2 @ B)) = (ord_less @ int @ (semiring_1_of_nat @ int @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 29.81/8.31 thf(10,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_1_1_T)).
% 29.81/8.31 thf(311,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 29.81/8.31 thf(164,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (B != (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_gr__implies__not0)).
% 29.81/8.31 thf(765,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (B = (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 29.81/8.31 thf(246,axiom,((! [A:nat]: (((zero_zero @ extended_enat) = (extended_enat2 @ A)) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_enat__0__iff_I2_J)).
% 29.81/8.31 thf(1071,plain,((! [A:nat]: (((zero_zero @ extended_enat) = (extended_enat2 @ A)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 29.81/8.31 thf(133,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C))) @ B) => (ord_less @ extended_enat @ (coindu1365464361scount @ TA @ A @ B) @ (extend1396239628finity @ extended_enat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_scount__finite)).
% 29.81/8.31 thf(674,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C))) @ B) => (ord_less @ extended_enat @ (coindu1365464361scount @ TA @ (A) @ B) @ (extend1396239628finity @ extended_enat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 29.81/8.31 thf(288,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((A @ B) => ((coindu76177514sfirst @ TA @ A @ B) = (zero_zero @ extended_enat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_sfirst__0)).
% 29.81/8.31 thf(1185,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((A @ B) => ((coindu76177514sfirst @ TA @ (A) @ B) = (zero_zero @ extended_enat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[288])).
% 29.81/8.31 thf(148,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_162_mult__less__cancel2)).
% 29.81/8.31 thf(718,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)],[148])).
% 29.81/8.31 thf(125,axiom,((! [A:(nat > $o),B:nat]: ((A @ (zero_zero @ nat)) => ((! [C:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ C) => ((~ (A @ C)) => (? [D:nat]: ((ord_less @ nat @ D @ C) & ~ (A @ D)))))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_infinite__descent0)).
% 29.81/8.31 thf(633,plain,((! [A:(nat > $o),B:nat]: ((A @ (zero_zero @ nat)) => ((! [C:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ C) => ((~ (A @ C)) => (? [D:nat]: ((ord_less @ nat @ D @ C) & ~ (A @ D)))))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 29.81/8.31 thf(28,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ (linear505997466_on_ev @ TA @ A)) = (linear505997466_on_ev @ TA @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_ev__ev)).
% 29.81/8.31 thf(360,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ (linear505997466_on_ev @ TA @ A)) = (linear505997466_on_ev @ TA @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 29.81/8.31 thf(167,axiom,((! [TA: $tType]: ((linordered_semidom @ TA @ (type @ TA)) => (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_less__numeral__extra_I3_J)).
% 29.81/8.31 thf(773,plain,((! [TA: $tType]: ((linordered_semidom @ TA @ (type @ TA)) => (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 29.81/8.31 thf(172,axiom,((! [A:int]: ((ord_less @ int @ (zero_zero @ int) @ A) => (? [B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ B) & (A = (semiring_1_of_nat @ int @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_zero__less__imp__eq__int)).
% 29.81/8.31 thf(794,plain,((! [A:int]: ((ord_less @ int @ (zero_zero @ int) @ A) => (? [B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ B) & (A = (semiring_1_of_nat @ int @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 29.81/8.31 thf(49,axiom,((linord20386208strict @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Olinordered__semiring__strict)).
% 29.81/8.31 thf(412,plain,((linord20386208strict @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 29.81/8.31 thf(55,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_T)).
% 29.81/8.31 thf(430,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 29.81/8.31 thf(257,axiom,((linord893533164strict @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Olinordered__comm__semiring__strict_2)).
% 29.81/8.31 thf(1103,plain,((linord893533164strict @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 29.81/8.31 thf(139,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_42_infinite__descent)).
% 29.81/8.31 thf(689,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)],[139])).
% 29.81/8.31 thf(209,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_49_infinite__descent__measure)).
% 29.81/8.31 thf(904,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)],[209])).
% 29.81/8.31 thf(268,axiom,((! [A:nat]: (((extended_enat2 @ A) = (zero_zero @ extended_enat)) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_enat__0__iff_I1_J)).
% 29.81/8.31 thf(1125,plain,((! [A:nat]: (((extended_enat2 @ A) = (zero_zero @ extended_enat)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 29.81/8.31 thf(156,axiom,((! [A:extended_enat,B:extended_enat]: (((times_times @ extended_enat @ A @ B) = (zero_zero @ extended_enat)) = ((A = (zero_zero @ extended_enat)) | (B = (zero_zero @ extended_enat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_imult__is__0)).
% 29.81/8.31 thf(743,plain,((! [A:extended_enat,B:extended_enat]: (((times_times @ extended_enat @ A @ B) = (zero_zero @ extended_enat)) = ((A = (zero_zero @ extended_enat)) | (B = (zero_zero @ extended_enat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 29.81/8.31 thf(145,axiom,((! [TA: $tType]: ((linord893533164strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ (zero_zero @ TA) @ C) => (ord_less @ TA @ (times_times @ TA @ C @ A) @ (times_times @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_linordered__comm__semiring__strict__class_Ocomm__mult__strict__left__mono)).
% 29.81/8.31 thf(711,plain,((! [TA: $tType]: ((linord893533164strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ (zero_zero @ TA) @ C) => (ord_less @ TA @ (times_times @ TA @ C @ A) @ (times_times @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 29.81/8.31 thf(50,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ A @ B) => ((! [D:(stream @ TA)]: ((A @ D) => (C @ D))) => (linear505997466_on_ev @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_ev__mono)).
% 29.81/8.31 thf(413,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ (A) @ B) => ((! [D:(stream @ TA)]: ((A @ D) => (C @ D))) => (linear505997466_on_ev @ TA @ (C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 29.81/8.31 thf(274,axiom,((! [TA: $tType]: ((linear1386806755on_alw @ TA) = (^ [A:((stream @ TA) > $o),B:(stream @ TA)]: ! [C:nat]: (A @ (sdrop @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_alw__iff__sdrop)).
% 29.81/8.31 thf(1139,plain,((! [TA: $tType]: ((linear1386806755on_alw @ TA) = (^ [A:((stream @ TA) > $o),B:(stream @ TA)]: ! [C:nat]: (A @ (sdrop @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 29.81/8.31 thf(63,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o),C:(stream @ TA),D:((stream @ TA) > $o)]: ((linear1341015445_UNTIL @ TA @ A @ B @ C) => ((! [E:(stream @ TA)]: ((B @ E) => (D @ E))) => (linear1341015445_UNTIL @ TA @ A @ D @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_until__monoR)).
% 29.81/8.31 thf(445,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o),C:(stream @ TA),D:((stream @ TA) > $o)]: ((linear1341015445_UNTIL @ TA @ (A) @ (B) @ C) => ((! [E:(stream @ TA)]: ((B @ E) => (D @ E))) => (linear1341015445_UNTIL @ TA @ (A) @ (D) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 29.81/8.31 thf(35,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((~ (linear1386806755on_alw @ TA @ A @ B)) = (linear505997466_on_ev @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_not__alw__iff)).
% 29.81/8.31 thf(382,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((~ (linear1386806755on_alw @ TA @ (A) @ B)) = (linear505997466_on_ev @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 29.81/8.31 thf(108,axiom,((! [A:extended_enat,B:extended_enat]: (((? [C:nat]: (A = (extended_enat2 @ C))) => (! [C:nat]: (B != (extended_enat2 @ C)))) => (((? [C:nat]: (A = (extended_enat2 @ C))) => (B != (extend1396239628finity @ extended_enat))) => (((A = (extend1396239628finity @ extended_enat)) => (! [C:nat]: (B != (extended_enat2 @ C)))) => (~ ((A = (extend1396239628finity @ extended_enat)) => (B != (extend1396239628finity @ extended_enat))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_enat2__cases)).
% 29.81/8.31 thf(572,plain,((! [A:extended_enat,B:extended_enat]: (((? [C:nat]: (A = (extended_enat2 @ C))) => (! [C:nat]: ~ (B = (extended_enat2 @ C)))) => (((? [C:nat]: (A = (extended_enat2 @ C))) => (~ (B = (extend1396239628finity @ extended_enat)))) => (((A = (extend1396239628finity @ extended_enat)) => (! [C:nat]: ~ (B = (extended_enat2 @ C)))) => (~ ((A = (extend1396239628finity @ extended_enat)) => (~ (B = (extend1396239628finity @ extended_enat)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 29.81/8.31 thf(146,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:nat,C:(stream @ TA)]: ((linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ (sdrop @ TA @ B @ C)) => (linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_alw__ev__sdrop)).
% 29.81/8.31 thf(713,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:nat,C:(stream @ TA)]: ((linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ (sdrop @ TA @ B @ C)) => (linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 29.81/8.31 thf(260,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: (((coindu1365464361scount @ TA @ A @ B) = (zero_zero @ extended_enat)) => (linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_scount__eq__0D)).
% 29.81/8.31 thf(1107,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: (((coindu1365464361scount @ TA @ (A) @ B) = (zero_zero @ extended_enat)) => (linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 29.81/8.31 thf(175,axiom,((! [A:extended_enat]: ((ord_less @ extended_enat @ A @ (extend1396239628finity @ extended_enat)) = (A != (extend1396239628finity @ extended_enat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_enat__ord__simps_I4_J)).
% 29.81/8.31 thf(804,plain,((! [A:extended_enat]: ((ord_less @ extended_enat @ A @ (extend1396239628finity @ extended_enat)) = (~ (A = (extend1396239628finity @ extended_enat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 29.81/8.31 thf(97,axiom,((! [TA: $tType]: ((semiri1193490041visors @ TA @ (type @ 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_175_divisors__zero)).
% 29.81/8.31 thf(540,plain,((! [TA: $tType]: ((semiri1193490041visors @ TA @ (type @ 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)],[97])).
% 29.81/8.31 thf(46,axiom,((linord581940658strict @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Olinordered__ring__strict)).
% 29.81/8.31 thf(406,plain,((linord581940658strict @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 29.81/8.31 thf(186,axiom,((semiri1193490041visors @ extended_enat @ (type @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Rings_Osemiring__no__zero__divisors_14)).
% 29.81/8.31 thf(831,plain,((semiri1193490041visors @ extended_enat @ (type @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 29.81/8.31 thf(224,axiom,((semiri1193490041visors @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Osemiring__no__zero__divisors_4)).
% 29.81/8.31 thf(1011,plain,((semiri1193490041visors @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 29.81/8.31 thf(154,axiom,((! [TA: $tType]: ((linordered_semidom @ TA @ (type @ TA)) => (! [A:nat]: ((ord_less @ TA @ (zero_zero @ TA) @ (semiring_1_of_nat @ TA @ A)) = (ord_less @ nat @ (zero_zero @ nat) @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_of__nat__0__less__iff)).
% 29.81/8.31 thf(737,plain,((! [TA: $tType]: ((linordered_semidom @ TA @ (type @ TA)) => (! [A:nat]: ((ord_less @ TA @ (zero_zero @ TA) @ (semiring_1_of_nat @ TA @ A)) = (ord_less @ nat @ (zero_zero @ nat) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 29.81/8.31 thf(111,axiom,((canoni770627133id_add @ extended_enat @ (type @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Groups_Ocanonically__ordered__monoid__add_13)).
% 29.81/8.31 thf(599,plain,((canoni770627133id_add @ extended_enat @ (type @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 29.81/8.31 thf(196,axiom,(((zero_zero @ extended_enat) = (extended_enat2 @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_zero__enat__def)).
% 29.81/8.31 thf(863,plain,(((zero_zero @ extended_enat) = (extended_enat2 @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 29.81/8.31 thf(237,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ (zero_zero @ TA)) => ((ord_less @ TA @ B @ (zero_zero @ TA)) => ((ord_less @ TA @ (inverse_inverse @ TA @ A) @ (inverse_inverse @ TA @ B)) = (ord_less @ TA @ B @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_inverse__less__iff__less__neg)).
% 29.81/8.31 thf(1043,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ (zero_zero @ TA)) => ((ord_less @ TA @ B @ (zero_zero @ TA)) => ((ord_less @ TA @ (inverse_inverse @ TA @ A) @ (inverse_inverse @ TA @ B)) = (ord_less @ TA @ B @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 29.81/8.31 thf(57,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear1386806755on_alw @ TA @ A @ B) => (linear1386806755on_alw @ TA @ (linear1386806755on_alw @ TA @ A) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_alw__alwD)).
% 29.81/8.31 thf(434,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear1386806755on_alw @ TA @ (A) @ B) => (linear1386806755on_alw @ TA @ (linear1386806755on_alw @ TA @ A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 29.81/8.31 thf(6,axiom,((! [TA: $tType]: ((ab_semigroup_mult @ TA @ (type @ 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_117_ab__semigroup__mult__class_Omult__ac_I1_J)).
% 29.81/8.31 thf(303,plain,((! [TA: $tType]: ((ab_semigroup_mult @ TA @ (type @ 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)],[6])).
% 29.81/8.31 thf(267,axiom,((! [A:extended_enat]: ((A != (extend1396239628finity @ extended_enat)) => ((extended_enat2 @ (extended_the_enat @ A)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_enat__the__enat)).
% 29.81/8.31 thf(1122,plain,((! [A:extended_enat]: ((~ (A = (extend1396239628finity @ extended_enat))) => ((extended_enat2 @ (extended_the_enat @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 29.81/8.31 thf(204,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA]: ((times_times @ TA @ (zero_zero @ TA) @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_semiring__normalization__rules_I9_J)).
% 29.81/8.31 thf(890,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA]: ((times_times @ TA @ (zero_zero @ TA) @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 29.81/8.31 thf(38,axiom,((semigroup_mult @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Osemigroup__mult)).
% 29.81/8.31 thf(387,plain,((semigroup_mult @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 29.81/8.31 thf(79,axiom,((semiri1193490041visors @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Osemiring__no__zero__divisors)).
% 29.81/8.31 thf(494,plain,((semiri1193490041visors @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 29.81/8.31 thf(194,axiom,((! [TA: $tType]: ((semiri1923998003cancel @ TA @ (type @ 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_177_mult__left__cancel)).
% 29.81/8.31 thf(858,plain,((! [TA: $tType]: ((semiri1923998003cancel @ TA @ (type @ 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)],[194])).
% 29.81/8.31 thf(95,axiom,((! [A:extended_enat]: ((ord_less @ extended_enat @ (zero_zero @ extended_enat) @ A) => ((times_times @ extended_enat @ A @ (extend1396239628finity @ extended_enat)) = (extend1396239628finity @ extended_enat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_imult__infinity__right)).
% 29.81/8.31 thf(535,plain,((! [A:extended_enat]: ((ord_less @ extended_enat @ (zero_zero @ extended_enat) @ A) => ((times_times @ extended_enat @ A @ (extend1396239628finity @ extended_enat)) = (extend1396239628finity @ extended_enat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 29.81/8.31 thf(116,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_less__zeroE)).
% 29.81/8.31 thf(609,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 29.81/8.31 thf(14,axiom,((! [A:nat,B:nat]: (((semiring_1_of_nat @ int @ A) = (semiring_1_of_nat @ int @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_transfer__int__nat__relations_I1_J)).
% 29.81/8.31 thf(323,plain,((! [A:nat,B:nat]: (((semiring_1_of_nat @ int @ A) = (semiring_1_of_nat @ int @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 29.81/8.31 thf(75,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((^ [B:(stream @ TA)]: ~ (linear505997466_on_ev @ TA @ A @ B)) = (linear1386806755on_alw @ TA @ (^ [B:(stream @ TA)]: ~ (A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_not__ev)).
% 29.81/8.31 thf(483,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((^ [B:(stream @ TA)]: ~ (linear505997466_on_ev @ TA @ A @ B)) = (linear1386806755on_alw @ TA @ (^ [B:(stream @ TA)]: ~ (A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 29.81/8.31 thf(141,axiom,((! [A:nat]: ((extended_the_enat @ (extended_enat2 @ A)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_the__enat_Osimps)).
% 29.81/8.31 thf(700,plain,((! [A:nat]: ((extended_the_enat @ (extended_enat2 @ A)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 29.81/8.31 thf(206,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((ord_less @ extended_enat @ (coindu76177514sfirst @ TA @ A @ B) @ (extend1396239628finity @ extended_enat)) = (linear505997466_on_ev @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_sfirst__finite)).
% 29.81/8.31 thf(895,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((ord_less @ extended_enat @ (coindu76177514sfirst @ TA @ (A) @ B) @ (extend1396239628finity @ extended_enat)) = (linear505997466_on_ev @ TA @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 29.81/8.31 thf(165,axiom,((~ (ord_less @ int @ (zero_zero @ int) @ (zero_zero @ int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_less__int__code_I1_J)).
% 29.81/8.31 thf(769,plain,((~ (ord_less @ int @ (zero_zero @ int) @ (zero_zero @ int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 29.81/8.31 thf(229,axiom,((! [TA: $tType]: ((semiring_1 @ TA @ (type @ TA)) => ((semiring_1_of_nat @ TA @ (zero_zero @ nat)) = (zero_zero @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_of__nat__0)).
% 29.81/8.31 thf(1022,plain,((! [TA: $tType]: ((semiring_1 @ TA @ (type @ TA)) => ((semiring_1_of_nat @ TA @ (zero_zero @ nat)) = (zero_zero @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 29.81/8.31 thf(132,axiom,((! [TA: $tType]: (! [A:(TA > nat),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ nat @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_measure__induct)).
% 29.81/8.31 thf(668,plain,((! [TA: $tType]: (! [A:(TA > nat),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ nat @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 29.81/8.31 thf(285,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ B) => ((coindu1365464361scount @ TA @ A @ B) = (extend1396239628finity @ extended_enat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_scount__infinite)).
% 29.81/8.31 thf(1177,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ B) => ((coindu1365464361scount @ TA @ (A) @ B) = (extend1396239628finity @ extended_enat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[285])).
% 29.81/8.31 thf(173,axiom,((! [TA: $tType]: (! [A:(stream @ TA)]: ((sdrop @ TA @ (zero_zero @ nat) @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_sdrop_Osimps_I1_J)).
% 29.81/8.31 thf(799,plain,((! [TA: $tType]: (! [A:(stream @ TA)]: ((sdrop @ TA @ (zero_zero @ nat) @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 29.81/8.31 thf(279,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_203_nat__mult__eq__cancel__disj)).
% 29.81/8.31 thf(1162,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)],[279])).
% 29.81/8.31 thf(216,axiom,((! [TA: $tType]: (! [A:(TA > nat),B:(TA > $o),C:TA]: ((! [D:TA]: (((A @ D) = (zero_zero @ nat)) => (B @ D))) => ((! [D:TA]: ((ord_less @ nat @ (zero_zero @ nat) @ (A @ D)) => ((~ (B @ D)) => (? [E:TA]: ((ord_less @ nat @ (A @ E) @ (A @ D)) & ~ (B @ E)))))) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_infinite__descent0__measure)).
% 29.81/8.31 thf(983,plain,((! [TA: $tType]: (! [A:(TA > nat),B:(TA > $o),C:TA]: ((! [D:TA]: (((A @ D) = (zero_zero @ nat)) => (B @ D))) => ((! [D:TA]: ((ord_less @ nat @ (zero_zero @ nat) @ (A @ D)) => ((~ (B @ D)) => (? [E:TA]: ((ord_less @ nat @ (A @ E) @ (A @ D)) & ~ (B @ E)))))) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 29.81/8.31 thf(293,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (inverse_inverse @ TA @ A) @ (zero_zero @ TA)) = (ord_less @ TA @ A @ (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_inverse__negative__iff__negative)).
% 29.81/8.31 thf(1198,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (inverse_inverse @ TA @ A) @ (zero_zero @ TA)) = (ord_less @ TA @ A @ (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[293])).
% 29.81/8.31 thf(198,axiom,((! [TA: $tType]: ((linordered_semidom @ TA @ (type @ TA)) => (! [A:nat,B:nat]: ((ord_less @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B)) => (ord_less @ nat @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_of__nat__less__imp__less)).
% 29.81/8.31 thf(868,plain,((! [TA: $tType]: ((linordered_semidom @ TA @ (type @ TA)) => (! [A:nat,B:nat]: ((ord_less @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B)) => (ord_less @ nat @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 29.81/8.31 thf(66,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear1386806755on_alw @ TA @ A @ B) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_alwD)).
% 29.81/8.31 thf(455,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear1386806755on_alw @ TA @ (A) @ B) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 29.81/8.31 thf(226,axiom,((comm_semiring_1 @ extended_enat @ (type @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Rings_Ocomm__semiring__1_16)).
% 29.81/8.31 thf(1015,plain,((comm_semiring_1 @ extended_enat @ (type @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 29.81/8.31 thf(220,axiom,((! [TA: $tType]: ((mult_zero @ TA @ (type @ TA)) => (! [A:TA]: ((times_times @ TA @ (zero_zero @ TA) @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_mult__zero__left)).
% 29.81/8.31 thf(1000,plain,((! [TA: $tType]: ((mult_zero @ TA @ (type @ TA)) => (! [A:TA]: ((times_times @ TA @ (zero_zero @ TA) @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 29.81/8.31 thf(4,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => ((times_times @ TA) = (^ [A:TA,B:TA]: (times_times @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_linordered__field__class_Osign__simps_I24_J)).
% 29.81/8.31 thf(299,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => ((times_times @ TA) = (^ [A:TA,B:TA]: (times_times @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 29.81/8.31 thf(84,axiom,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)) = (((ord_less @ TA @ (zero_zero @ TA) @ A) & (ord_less @ TA @ (zero_zero @ TA) @ B)) | ((ord_less @ TA @ A @ (zero_zero @ TA)) & (ord_less @ TA @ B @ (zero_zero @ TA))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_zero__less__mult__iff)).
% 29.81/8.31 thf(505,plain,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)) = (((ord_less @ TA @ (zero_zero @ TA) @ A) & (ord_less @ TA @ (zero_zero @ TA) @ B)) | ((ord_less @ TA @ A @ (zero_zero @ TA)) & (ord_less @ TA @ B @ (zero_zero @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 29.81/8.31 thf(56,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ (^ [C:(stream @ TA)]: ((A @ C) | (B @ C)))) = (^ [C:(stream @ TA)]: ((linear505997466_on_ev @ TA @ A @ C) | (linear505997466_on_ev @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_ev__or)).
% 29.81/8.31 thf(431,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ (^ [C:(stream @ TA)]: ((A @ C) | (B @ C)))) = (^ [C:(stream @ TA)]: ((linear505997466_on_ev @ TA @ A @ C) | (linear505997466_on_ev @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 29.81/8.31 thf(129,axiom,((! [A:nat]: ~ (ord_less @ extended_enat @ (extend1396239628finity @ extended_enat) @ (extended_enat2 @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_infinity__ilessE)).
% 29.81/8.31 thf(658,plain,((! [A:nat]: ~ (ord_less @ extended_enat @ (extend1396239628finity @ extended_enat) @ (extended_enat2 @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 29.81/8.31 thf(89,axiom,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ (zero_zero @ TA)) => ((ord_less @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ A @ C)) = (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_mult__less__cancel__left__neg)).
% 29.81/8.31 thf(521,plain,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ (zero_zero @ TA)) => ((ord_less @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ A @ C)) = (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 29.81/8.31 thf(282,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) => (ord_less @ nat @ (zero_zero @ nat) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_gr0I)).
% 29.81/8.31 thf(1171,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) => (ord_less @ nat @ (zero_zero @ nat) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 29.81/8.31 thf(284,axiom,((ab_semigroup_mult @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oab__semigroup__mult_6)).
% 29.81/8.31 thf(1176,plain,((ab_semigroup_mult @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[284])).
% 29.81/8.31 thf(115,axiom,((nat_tr1645093318rphism @ nat @ int @ (semiring_1_of_nat @ int) @ (^ [A:nat]: (($true))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_transfer__morphism__int__nat)).
% 29.81/8.31 thf(608,plain,((nat_tr1645093318rphism @ nat @ int @ (semiring_1_of_nat @ int) @ (^ [A:nat]: (($true))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 29.81/8.31 thf(42,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ 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_211_linordered__field__class_Osign__simps_I25_J)).
% 29.81/8.31 thf(394,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ 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)],[42])).
% 29.81/8.31 thf(7,axiom,((linordered_ring @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Olinordered__ring)).
% 29.81/8.31 thf(306,plain,((linordered_ring @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 29.81/8.31 thf(262,axiom,((comm_semiring_1 @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Ocomm__semiring__1_7)).
% 29.81/8.31 thf(1113,plain,((comm_semiring_1 @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 29.81/8.31 thf(105,axiom,((! [TA: $tType]: ((linordered_semidom @ TA @ (type @ TA)) => (! [A:nat,B:nat]: ((ord_less @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B)) = (ord_less @ nat @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_of__nat__less__iff)).
% 29.81/8.31 thf(563,plain,((! [TA: $tType]: ((linordered_semidom @ TA @ (type @ TA)) => (! [A:nat,B:nat]: ((ord_less @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B)) = (ord_less @ nat @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 29.81/8.31 thf(233,axiom,((! [TA: $tType]: ((archim1804426504_field @ TA @ (type @ TA)) => (! [A:TA]: ? [B:nat]: (ord_less @ TA @ A @ (semiring_1_of_nat @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_reals__Archimedean2)).
% 29.81/8.31 thf(1034,plain,((! [TA: $tType]: ((archim1804426504_field @ TA @ (type @ TA)) => (! [A:TA]: ? [B:nat]: (ord_less @ TA @ A @ (semiring_1_of_nat @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 29.81/8.31 thf(272,axiom,((! [A:extended_enat]: ((ord_less @ extended_enat @ (zero_zero @ extended_enat) @ A) = (A != (zero_zero @ extended_enat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_i0__less)).
% 29.81/8.31 thf(1134,plain,((! [A:extended_enat]: ((ord_less @ extended_enat @ (zero_zero @ extended_enat) @ A) = (~ (A = (zero_zero @ extended_enat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[272])).
% 29.81/8.31 thf(178,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear505997466_on_ev @ TA @ A @ B) => (A @ (sdrop @ TA @ (linear1335279038n_wait @ TA @ A @ B) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_sdrop__wait)).
% 29.81/8.31 thf(812,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear505997466_on_ev @ TA @ (A) @ B) => (A @ (sdrop @ TA @ (linear1335279038n_wait @ TA @ (A) @ B) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 29.81/8.31 thf(119,axiom,((! [TA: $tType]: ((division_ring @ TA @ (type @ TA)) => ((inverse_inverse @ TA @ (zero_zero @ TA)) = (zero_zero @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_inverse__zero)).
% 29.81/8.31 thf(617,plain,((! [TA: $tType]: ((division_ring @ TA @ (type @ TA)) => ((inverse_inverse @ TA @ (zero_zero @ TA)) = (zero_zero @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 29.81/8.31 thf(26,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ 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_213_linordered__field__class_Osign__simps_I23_J)).
% 29.81/8.31 thf(355,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ 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)],[26])).
% 29.81/8.31 thf(102,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => (ord_less @ TA @ (zero_zero @ TA) @ (inverse_inverse @ TA @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_positive__imp__inverse__positive)).
% 29.81/8.31 thf(553,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => (ord_less @ TA @ (zero_zero @ TA) @ (inverse_inverse @ TA @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 29.81/8.31 thf(239,axiom,((! [TA: $tType]: ((linordered_semidom @ TA @ (type @ TA)) => (! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_less__imp__of__nat__less)).
% 29.81/8.31 thf(1049,plain,((! [TA: $tType]: ((linordered_semidom @ TA @ (type @ TA)) => (! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 29.81/8.31 thf(250,axiom,((! [A:nat,B:nat]: ((times_times @ extended_enat @ (extended_enat2 @ A) @ (extended_enat2 @ B)) = (extended_enat2 @ (times_times @ nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_164_times__enat__simps_I1_J)).
% 29.81/8.31 thf(1081,plain,((! [A:nat,B:nat]: ((times_times @ extended_enat @ (extended_enat2 @ A) @ (extended_enat2 @ B)) = (extended_enat2 @ (times_times @ nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 29.81/8.31 thf(159,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C))) @ B) => ((coindu1365464361scount @ TA @ A @ B) = (extended_enat2 @ (finite_card @ nat @ (collect @ nat @ (^ [C:nat]: (A @ (sdrop @ TA @ C @ B))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_scount__eq__card)).
% 29.81/8.31 thf(749,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C))) @ B) => ((coindu1365464361scount @ TA @ (A) @ B) = (extended_enat2 @ (finite_card @ nat @ (collect @ nat @ (^ [C:nat]: (A @ (sdrop @ TA @ C @ B))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 29.81/8.31 thf(221,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:TA]: ((extended_case_enat @ TA @ A @ B @ (extend1396239628finity @ extended_enat)) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_enat_Osimps_I5_J)).
% 29.81/8.31 thf(1003,plain,((! [TA: $tType]: (! [A:(nat > TA),B:TA]: ((extended_case_enat @ TA @ (A) @ B @ (extend1396239628finity @ extended_enat)) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 29.81/8.31 thf(193,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => ((ord_less @ TA @ (zero_zero @ TA) @ B) => ((ord_less @ TA @ (inverse_inverse @ TA @ A) @ (inverse_inverse @ TA @ B)) = (ord_less @ TA @ B @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_inverse__less__iff__less)).
% 29.81/8.31 thf(855,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => ((ord_less @ TA @ (zero_zero @ TA) @ B) => ((ord_less @ TA @ (inverse_inverse @ TA @ A) @ (inverse_inverse @ TA @ B)) = (ord_less @ TA @ B @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 29.81/8.31 thf(200,axiom,((! [A:$o,B:nat,C:nat]: (((A) => ((semiring_1_of_nat @ int @ B) = (semiring_1_of_nat @ int @ (if @ nat @ A @ B @ C)))) & ((~ (A)) => ((semiring_1_of_nat @ int @ C) = (semiring_1_of_nat @ int @ (if @ nat @ A @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_int__if__cong)).
% 29.81/8.31 thf(872,plain,((! [A:$o,B:nat,C:nat]: (((A) => ((semiring_1_of_nat @ int @ B) = (semiring_1_of_nat @ int @ (if @ nat @ A @ B @ C)))) & ((~ (A)) => ((semiring_1_of_nat @ int @ C) = (semiring_1_of_nat @ int @ (if @ nat @ A @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 29.81/8.31 thf(203,axiom,((! [A:nat]: ((size_size @ extended_enat @ (extended_enat2 @ A)) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_enat_Osize_I3_J)).
% 29.81/8.31 thf(887,plain,((! [A:nat]: ((size_size @ extended_enat @ (extended_enat2 @ A)) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 29.81/8.31 thf(48,axiom,((! [TA: $tType]: ((field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((inverse_inverse @ TA @ (times_times @ TA @ A @ B)) = (times_times @ TA @ (inverse_inverse @ TA @ A) @ (inverse_inverse @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_inverse__mult__distrib)).
% 29.81/8.31 thf(409,plain,((! [TA: $tType]: ((field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((inverse_inverse @ TA @ (times_times @ TA @ A @ B)) = (times_times @ TA @ (inverse_inverse @ TA @ A) @ (inverse_inverse @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 29.81/8.31 thf(217,axiom,(((zero_zero @ int) = (semiring_1_of_nat @ int @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_transfer__int__nat__numerals_I1_J)).
% 29.81/8.31 thf(993,plain,(((zero_zero @ int) = (semiring_1_of_nat @ int @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 29.81/8.31 thf(230,axiom,((! [A:int]: ((times_times @ int @ (zero_zero @ int) @ A) = (zero_zero @ int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_times__int__code_I2_J)).
% 29.81/8.31 thf(1025,plain,((! [A:int]: ((times_times @ int @ (zero_zero @ int) @ A) = (zero_zero @ int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 29.81/8.31 thf(1,conjecture,(((ord_less @ extended_enat @ (extended_enat2 @ (zero_zero @ nat)) @ (coindu76177514sfirst @ a @ p @ omega)) = (~ (p @ (sdrop @ a @ (zero_zero @ nat) @ omega))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 29.81/8.31 thf(2,negated_conjecture,((~ ((ord_less @ extended_enat @ (extended_enat2 @ (zero_zero @ nat)) @ (coindu76177514sfirst @ a @ p @ omega)) = (~ (p @ (sdrop @ a @ (zero_zero @ nat) @ omega)))))),inference(neg_conjecture,[status(cth)],[1])).
% 29.81/8.31 thf(295,plain,((~ ((ord_less @ extended_enat @ (extended_enat2 @ (zero_zero @ nat)) @ (coindu76177514sfirst @ a @ (p) @ omega)) = (~ (p @ (sdrop @ a @ (zero_zero @ nat) @ omega)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 29.81/8.31 thf(241,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: (((coindu1365464361scount @ TA @ A @ B) = (extend1396239628finity @ extended_enat)) = (linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_scount__infinite__iff)).
% 29.81/8.31 thf(1053,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: (((coindu1365464361scount @ TA @ (A) @ B) = (extend1396239628finity @ extended_enat)) = (linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 29.81/8.31 thf(289,axiom,((linear1341015445_UNTIL @ a @ (^ [A:(stream @ a)]: ~ (p @ A)) @ (linear1386806755on_alw @ a @ p) @ omega)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__C0_Oprems_C)).
% 29.81/8.31 thf(1188,plain,((linear1341015445_UNTIL @ a @ (^ [A:(stream @ a)]: ~ (p @ A)) @ (linear1386806755on_alw @ a @ p) @ omega)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[289])).
% 29.81/8.31 thf(83,axiom,((! [A:nat]: ((times_times @ nat @ (zero_zero @ nat) @ A) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_mult__0)).
% 29.81/8.31 thf(502,plain,((! [A:nat]: ((times_times @ nat @ (zero_zero @ nat) @ A) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 29.81/8.31 thf(71,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ A @ B) => ((linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((A @ D) => (C @ D))) @ B) => (linear505997466_on_ev @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_ev__alw__impl)).
% 29.81/8.31 thf(470,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ (A) @ B) => ((linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((A @ D) => (C @ D))) @ B) => (linear505997466_on_ev @ TA @ (C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 29.81/8.31 thf(270,axiom,((semiri1923998003cancel @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Osemiring__no__zero__divisors__cancel_1)).
% 29.81/8.31 thf(1130,plain,((semiri1923998003cancel @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 29.81/8.31 thf(99,axiom,((! [A:nat]: ((extended_size_enat @ (extended_enat2 @ A)) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_enat_Osize_I1_J)).
% 29.81/8.31 thf(544,plain,((! [A:nat]: ((extended_size_enat @ (extended_enat2 @ A)) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 29.81/8.31 thf(19,axiom,((linord893533164strict @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Olinordered__comm__semiring__strict)).
% 29.81/8.31 thf(336,plain,((linord893533164strict @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 29.81/8.31 thf(142,axiom,((! [TA: $tType]: ((semiring_1 @ TA @ (type @ TA)) => (! [A:nat,B:nat]: ((semiring_1_of_nat @ TA @ (times_times @ nat @ A @ B)) = (times_times @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_of__nat__mult)).
% 29.81/8.31 thf(703,plain,((! [TA: $tType]: ((semiring_1 @ TA @ (type @ TA)) => (! [A:nat,B:nat]: ((semiring_1_of_nat @ TA @ (times_times @ nat @ A @ B)) = (times_times @ TA @ (semiring_1_of_nat @ TA @ A) @ (semiring_1_of_nat @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 29.81/8.31 thf(112,axiom,((! [A:nat]: ((~ (ord_less @ nat @ (zero_zero @ nat) @ A)) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_not__gr0)).
% 29.81/8.31 thf(600,plain,((! [A:nat]: ((~ (ord_less @ nat @ (zero_zero @ nat) @ A)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 29.81/8.31 thf(37,axiom,((zero @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Ozero)).
% 29.81/8.31 thf(386,plain,((zero @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 29.81/8.31 thf(11,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ 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_221_semiring__normalization__rules_I17_J)).
% 29.81/8.31 thf(314,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ 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)],[11])).
% 29.81/8.31 thf(110,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: ((zero @ TB @ (type @ TB)) => (! [A:((TC > TB) > TA),B:TA]: ((A = (^ [C:(TC > TB)]: (B))) => ((A @ (^ [C:TC]: (zero_zero @ TB))) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_fun__cong__unused__0)).
% 29.81/8.31 thf(595,plain,((! [TA: $tType,TB: $tType,TC: $tType]: ((zero @ TB @ (type @ TB)) => (! [A:((TC > TB) > TA),B:TA]: (((A) = (^ [C:(TC > TB)]: (B))) => ((A @ (^ [C:TC]: (zero_zero @ TB))) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 29.81/8.31 thf(117,axiom,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ (zero_zero @ TA)) => (ord_less @ TA @ (times_times @ TA @ C @ B) @ (times_times @ TA @ C @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_mult__strict__left__mono__neg)).
% 29.81/8.31 thf(612,plain,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ (zero_zero @ TA)) => (ord_less @ TA @ (times_times @ TA @ C @ B) @ (times_times @ TA @ C @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 29.81/8.31 thf(81,axiom,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => ((ord_less @ TA @ (zero_zero @ TA) @ B) => (ord_less @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_mult__pos__pos)).
% 29.81/8.31 thf(497,plain,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => ((ord_less @ TA @ (zero_zero @ TA) @ B) => (ord_less @ TA @ (zero_zero @ TA) @ (times_times @ TA @ A @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 29.81/8.31 thf(191,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_41_nat__less__induct)).
% 29.81/8.31 thf(845,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)],[191])).
% 29.81/8.31 thf(123,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_linordered__field__no__lb)).
% 29.81/8.31 thf(627,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 29.81/8.31 thf(251,axiom,((! [TA: $tType]: ((archim1804426504_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => (? [C:nat]: (ord_less @ TA @ B @ (times_times @ TA @ (semiring_1_of_nat @ TA @ C) @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_ex__less__of__nat__mult)).
% 29.81/8.31 thf(1084,plain,((! [TA: $tType]: ((archim1804426504_field @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => (? [C:nat]: (ord_less @ TA @ B @ (times_times @ TA @ (semiring_1_of_nat @ TA @ C) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 29.81/8.31 thf(286,axiom,((! [TA: $tType]: ((semiri1923998003cancel @ TA @ (type @ 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_154_mult__cancel__left)).
% 29.81/8.31 thf(1180,plain,((! [TA: $tType]: ((semiri1923998003cancel @ TA @ (type @ 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)],[286])).
% 29.81/8.31 thf(29,axiom,((! [TA: $tType]: ((semigroup_mult @ TA @ (type @ 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_118_mult_Oassoc)).
% 29.81/8.31 thf(363,plain,((! [TA: $tType]: ((semigroup_mult @ TA @ (type @ 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)],[29])).
% 29.81/8.31 thf(90,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:nat]: ((linear1386806755on_alw @ TA @ A @ B) => (linear1386806755on_alw @ TA @ A @ (sdrop @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_alw__sdrop)).
% 29.81/8.31 thf(524,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:nat]: ((linear1386806755on_alw @ TA @ (A) @ B) => (linear1386806755on_alw @ TA @ (A) @ (sdrop @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 29.81/8.31 thf(80,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ A) @ B) => (linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_ev__alw__imp__alw__ev)).
% 29.81/8.31 thf(495,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ A) @ B) => (linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 29.81/8.31 thf(162,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => ((ord_less @ nat @ (zero_zero @ nat) @ C) => (ord_less @ nat @ (times_times @ nat @ C @ A) @ (times_times @ nat @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_mult__less__mono2)).
% 29.81/8.31 thf(759,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => ((ord_less @ nat @ (zero_zero @ nat) @ C) => (ord_less @ nat @ (times_times @ nat @ C @ A) @ (times_times @ nat @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 29.81/8.31 thf(290,axiom,((! [A:extended_enat,B:extended_enat]: ((ord_less @ extended_enat @ (zero_zero @ extended_enat) @ (times_times @ extended_enat @ A @ B)) = ((ord_less @ extended_enat @ (zero_zero @ extended_enat) @ A) & (ord_less @ extended_enat @ (zero_zero @ extended_enat) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_enat__0__less__mult__iff)).
% 29.81/8.31 thf(1189,plain,((! [A:extended_enat,B:extended_enat]: ((ord_less @ extended_enat @ (zero_zero @ extended_enat) @ (times_times @ extended_enat @ A @ B)) = ((ord_less @ extended_enat @ (zero_zero @ extended_enat) @ A) & (ord_less @ extended_enat @ (zero_zero @ extended_enat) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[290])).
% 29.81/8.31 thf(166,axiom,((extended_size_enat = (extended_rec_enat @ nat @ (^ [A:nat]: (zero_zero @ nat)) @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_size__enat__def)).
% 29.81/8.31 thf(771,plain,(((extended_size_enat) = (extended_rec_enat @ nat @ (^ [A:nat]: (zero_zero @ nat)) @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 29.81/8.31 thf(244,axiom,((! [A:extended_enat,B:nat]: ((ord_less @ extended_enat @ A @ (extended_enat2 @ B)) => (~ (! [C:nat]: ((A = (extended_enat2 @ C)) => (~ (ord_less @ nat @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_less__enatE)).
% 29.81/8.31 thf(1062,plain,((! [A:extended_enat,B:nat]: ((ord_less @ extended_enat @ A @ (extended_enat2 @ B)) => (~ (! [C:nat]: ((A = (extended_enat2 @ C)) => (~ (ord_less @ nat @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 29.81/8.31 thf(152,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_less__nat__zero__code)).
% 29.81/8.31 thf(731,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 29.81/8.31 thf(218,axiom,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)) = (((ord_less @ TA @ (zero_zero @ TA) @ A) & (ord_less @ TA @ B @ (zero_zero @ TA))) | ((ord_less @ TA @ A @ (zero_zero @ TA)) & (ord_less @ TA @ (zero_zero @ TA) @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_mult__less__0__iff)).
% 29.81/8.31 thf(995,plain,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (times_times @ TA @ A @ B) @ (zero_zero @ TA)) = (((ord_less @ TA @ (zero_zero @ TA) @ A) & (ord_less @ TA @ B @ (zero_zero @ TA))) | ((ord_less @ TA @ A @ (zero_zero @ TA)) & (ord_less @ TA @ (zero_zero @ TA) @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 29.81/8.31 thf(248,axiom,(((size_size @ extended_enat) = (extended_rec_enat @ nat @ (^ [A:nat]: (zero_zero @ nat)) @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_size__enat__overloaded__def)).
% 29.81/8.31 thf(1077,plain,(((size_size @ extended_enat) = (extended_rec_enat @ nat @ (^ [A:nat]: (zero_zero @ nat)) @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 29.81/8.31 thf(22,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ((A @ C) & (B @ C)))) = (^ [C:(stream @ TA)]: ((linear1386806755on_alw @ TA @ A @ C) & (linear1386806755on_alw @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_alw__aand)).
% 29.81/8.31 thf(346,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ((A @ C) & (B @ C)))) = (^ [C:(stream @ TA)]: ((linear1386806755on_alw @ TA @ A @ C) & (linear1386806755on_alw @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 29.81/8.31 thf(187,axiom,((! [TA: $tType]: (! [A:(nat > TA),B:TA]: ((extended_rec_enat @ TA @ A @ B @ (extend1396239628finity @ extended_enat)) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_enat_Osimps_I7_J)).
% 29.81/8.31 thf(832,plain,((! [TA: $tType]: (! [A:(nat > TA),B:TA]: ((extended_rec_enat @ TA @ (A) @ B @ (extend1396239628finity @ extended_enat)) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 29.81/8.31 thf(137,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_163_nat__0__less__mult__iff)).
% 29.81/8.31 thf(684,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)],[137])).
% 29.81/8.31 thf(264,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_161_mult__is__0)).
% 29.81/8.31 thf(1116,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)],[264])).
% 29.81/8.31 thf(120,axiom,((! [TA: $tType]: ((semiri1923998003cancel @ TA @ (type @ 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_178_mult__right__cancel)).
% 29.81/8.31 thf(620,plain,((! [TA: $tType]: ((semiri1923998003cancel @ TA @ (type @ 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)],[120])).
% 29.81/8.31 thf(160,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_159_mult__cancel1)).
% 29.81/8.31 thf(752,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)],[160])).
% 29.81/8.31 thf(211,axiom,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ A @ C)) = (((ord_less @ TA @ (zero_zero @ TA) @ A) & (ord_less @ TA @ B @ C)) | ((ord_less @ TA @ A @ (zero_zero @ TA)) & (ord_less @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_mult__less__cancel__left__disj)).
% 29.81/8.31 thf(967,plain,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ A @ C)) = (((ord_less @ TA @ (zero_zero @ TA) @ A) & (ord_less @ TA @ B @ C)) | ((ord_less @ TA @ A @ (zero_zero @ TA)) & (ord_less @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 29.81/8.31 thf(188,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type @ TA)) => (! [A:TA]: ((~ (ord_less @ TA @ (zero_zero @ TA) @ A)) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_not__gr__zero)).
% 29.81/8.31 thf(835,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type @ TA)) => (! [A:TA]: ((~ (ord_less @ TA @ (zero_zero @ TA) @ A)) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 29.81/8.31 thf(192,axiom,((semigroup_mult @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Osemigroup__mult_8)).
% 29.81/8.31 thf(854,plain,((semigroup_mult @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 29.81/8.31 thf(197,axiom,((! [A:nat,B:nat]: ((times_times @ int @ (semiring_1_of_nat @ int @ A) @ (semiring_1_of_nat @ int @ B)) = (semiring_1_of_nat @ int @ (times_times @ nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_Nat__Transfer_Otransfer__int__nat__functions_I2_J)).
% 29.81/8.31 thf(865,plain,((! [A:nat,B:nat]: ((times_times @ int @ (semiring_1_of_nat @ int @ A) @ (semiring_1_of_nat @ int @ B)) = (semiring_1_of_nat @ int @ (times_times @ nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 29.81/8.31 thf(113,axiom,((! [TA: $tType]: ((linordered_ring @ TA @ (type @ TA)) => (! [A:TA]: ~ (ord_less @ TA @ (times_times @ TA @ A @ A) @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_not__square__less__zero)).
% 29.81/8.31 thf(603,plain,((! [TA: $tType]: ((linordered_ring @ TA @ (type @ TA)) => (! [A:TA]: ~ (ord_less @ TA @ (times_times @ TA @ A @ A) @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 29.81/8.31 thf(15,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ (linear1386806755on_alw @ TA @ A)) = (linear1386806755on_alw @ TA @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_alw__alw)).
% 29.81/8.31 thf(326,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ (linear1386806755on_alw @ TA @ A)) = (linear1386806755on_alw @ TA @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 29.81/8.31 thf(59,axiom,((! [TA: $tType]: (! [A:(stream @ TA)]: ~ (linear505997466_on_ev @ TA @ (^ [B:(stream @ TA)]: (($false))) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_ev__False)).
% 29.81/8.31 thf(437,plain,((! [TA: $tType]: (! [A:(stream @ TA)]: ~ (linear505997466_on_ev @ TA @ (^ [B:(stream @ TA)]: (($false))) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 29.81/8.31 thf(73,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o),D:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ A @ B) => ((! [E:(stream @ TA)]: ((A @ E) => ((C @ E) = (D @ E)))) => ((linear505997466_on_ev @ TA @ C @ B) = (linear505997466_on_ev @ TA @ D @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_ev__cong)).
% 29.81/8.31 thf(474,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o),D:((stream @ TA) > $o)]: ((linear1386806755on_alw @ TA @ (A) @ B) => ((! [E:(stream @ TA)]: ((A @ E) => ((C @ E) = (D @ E)))) => ((linear505997466_on_ev @ TA @ (C) @ B) = (linear505997466_on_ev @ TA @ (D) @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 29.81/8.31 thf(44,axiom,((! [TA: $tType]: ((semiring_char_0 @ TA @ (type @ TA)) => (! [A:nat,B:nat]: (((semiring_1_of_nat @ TA @ A) = (semiring_1_of_nat @ TA @ B)) = (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_of__nat__eq__iff)).
% 29.81/8.31 thf(400,plain,((! [TA: $tType]: ((semiring_char_0 @ TA @ (type @ TA)) => (! [A:nat,B:nat]: (((semiring_1_of_nat @ TA @ A) = (semiring_1_of_nat @ TA @ B)) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 29.81/8.31 thf(184,axiom,((mult_zero @ extended_enat @ (type @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Rings_Omult__zero_20)).
% 29.81/8.31 thf(828,plain,((mult_zero @ extended_enat @ (type @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 29.81/8.31 thf(94,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_158_mult__cancel2)).
% 29.81/8.31 thf(532,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)],[94])).
% 29.81/8.31 thf(280,axiom,((! [TA: $tType]: ((semiring_char_0 @ TA @ (type @ TA)) => (! [A:nat]: (((semiring_1_of_nat @ TA @ A) = (zero_zero @ TA)) = (A = (zero_zero @ nat))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_of__nat__eq__0__iff)).
% 29.81/8.31 thf(1165,plain,((! [TA: $tType]: ((semiring_char_0 @ TA @ (type @ TA)) => (! [A:nat]: (((semiring_1_of_nat @ TA @ A) = (zero_zero @ TA)) = (A = (zero_zero @ nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[280])).
% 29.81/8.31 thf(27,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ B) => (linear505997466_on_ev @ TA @ (^ [C:(stream @ TA)]: ((A @ C) & (linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ C))) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_alw__ev__imp__ev__alw)).
% 29.81/8.31 thf(358,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ B) => (linear505997466_on_ev @ TA @ (^ [C:(stream @ TA)]: ((A @ C) & (linear1386806755on_alw @ TA @ (linear505997466_on_ev @ TA @ A) @ C))) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 29.81/8.31 thf(176,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (inverse_inverse @ TA @ A) @ (zero_zero @ TA)) => ((A != (zero_zero @ TA)) => (ord_less @ TA @ A @ (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_inverse__negative__imp__negative)).
% 29.81/8.31 thf(807,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (inverse_inverse @ TA @ A) @ (zero_zero @ TA)) => ((~ (A = (zero_zero @ TA))) => (ord_less @ TA @ A @ (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 29.81/8.31 thf(242,axiom,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => ((ord_less @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ A @ C)) = (ord_less @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_mult__less__cancel__left__pos)).
% 29.81/8.31 thf(1056,plain,((! [TA: $tType]: ((linord581940658strict @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => ((ord_less @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ A @ C)) = (ord_less @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 29.81/8.31 thf(131,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_less__not__refl2)).
% 29.81/8.31 thf(664,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 29.81/8.31 thf(122,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA @ (type @ TA)) => ((archimedean_ceiling @ TA @ (zero_zero @ TA)) = (zero_zero @ int))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_ceiling__zero)).
% 29.81/8.31 thf(624,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA @ (type @ TA)) => ((archimedean_ceiling @ TA @ (zero_zero @ TA)) = (zero_zero @ int))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 29.81/8.31 thf(70,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o),C:(stream @ TA),D:((stream @ TA) > $o),E:((stream @ TA) > $o)]: ((linear1341015445_UNTIL @ TA @ A @ B @ C) => ((! [F:(stream @ TA)]: ((A @ F) => (D @ F))) => ((! [F:(stream @ TA)]: ((B @ F) => (E @ F))) => (linear1341015445_UNTIL @ TA @ D @ E @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_until__mono)).
% 29.81/8.31 thf(464,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:((stream @ TA) > $o),C:(stream @ TA),D:((stream @ TA) > $o),E:((stream @ TA) > $o)]: ((linear1341015445_UNTIL @ TA @ (A) @ (B) @ C) => ((! [F:(stream @ TA)]: ((A @ F) => (D @ F))) => ((! [F:(stream @ TA)]: ((B @ F) => (E @ F))) => (linear1341015445_UNTIL @ TA @ (D) @ (E) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 29.81/8.31 thf(17,axiom,((semiring_1 @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Osemiring__1)).
% 29.81/8.31 thf(332,plain,((semiring_1 @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 29.81/8.31 thf(228,axiom,((! [A:extended_enat]: ((ord_less @ extended_enat @ (zero_zero @ extended_enat) @ A) => ((times_times @ extended_enat @ (extend1396239628finity @ extended_enat) @ A) = (extend1396239628finity @ extended_enat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_imult__infinity)).
% 29.81/8.31 thf(1019,plain,((! [A:extended_enat]: ((ord_less @ extended_enat @ (zero_zero @ extended_enat) @ A) => ((times_times @ extended_enat @ (extend1396239628finity @ extended_enat) @ A) = (extend1396239628finity @ extended_enat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 29.81/8.31 thf(182,axiom,((! [TA: $tType]: ((zero @ TA @ (type @ TA)) => (! [A:TA]: (((zero_zero @ TA) = A) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_zero__reorient)).
% 29.81/8.31 thf(822,plain,((! [TA: $tType]: ((zero @ TA @ (type @ TA)) => (! [A:TA]: (((zero_zero @ TA) = A) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 29.81/8.31 thf(62,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ (times_times @ TA @ A @ B) @ C) = (times_times @ TA @ (times_times @ TA @ A @ C) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_semiring__normalization__rules_I16_J)).
% 29.81/8.31 thf(442,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA]: ((times_times @ TA @ (times_times @ TA @ A @ B) @ C) = (times_times @ TA @ (times_times @ TA @ A @ C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 29.81/8.31 thf(266,axiom,((! [TA: $tType]: ((linordered_semidom @ TA @ (type @ TA)) => (! [A:nat]: ~ (ord_less @ TA @ (semiring_1_of_nat @ TA @ A) @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_of__nat__less__0__iff)).
% 29.81/8.31 thf(1120,plain,((! [TA: $tType]: ((linordered_semidom @ TA @ (type @ TA)) => (! [A:nat]: ~ (ord_less @ TA @ (semiring_1_of_nat @ TA @ A) @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 29.81/8.31 thf(31,axiom,((! [A:nat,B:nat]: (((semiring_1_of_nat @ int @ A) = (semiring_1_of_nat @ int @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_int__int__eq)).
% 29.81/8.31 thf(369,plain,((! [A:nat,B:nat]: (((semiring_1_of_nat @ int @ A) = (semiring_1_of_nat @ int @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 29.81/8.31 thf(151,axiom,(((extend1396239628finity @ extended_enat) != (zero_zero @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_infinity__ne__i0)).
% 29.81/8.31 thf(728,plain,((~ ((extend1396239628finity @ extended_enat) = (zero_zero @ extended_enat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 29.81/8.31 thf(155,axiom,((! [A:int,B:int,C:nat]: ((ord_less @ int @ A @ B) => ((ord_less @ nat @ (zero_zero @ nat) @ C) => (ord_less @ int @ (times_times @ int @ (semiring_1_of_nat @ int @ C) @ A) @ (times_times @ int @ (semiring_1_of_nat @ int @ C) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_zmult__zless__mono2__lemma)).
% 29.81/8.31 thf(740,plain,((! [A:int,B:int,C:nat]: ((ord_less @ int @ A @ B) => ((ord_less @ nat @ (zero_zero @ nat) @ C) => (ord_less @ int @ (times_times @ int @ (semiring_1_of_nat @ int @ C) @ A) @ (times_times @ int @ (semiring_1_of_nat @ int @ C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 29.81/8.31 thf(277,axiom,((! [TA: $tType]: ((mult_zero @ TA @ (type @ 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_174_mult__not__zero)).
% 29.81/8.31 thf(1152,plain,((! [TA: $tType]: ((mult_zero @ TA @ (type @ 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)],[277])).
% 29.81/8.31 thf(54,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((~ (linear505997466_on_ev @ TA @ A @ B)) = (linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_not__ev__iff)).
% 29.81/8.31 thf(427,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA)]: ((~ (linear505997466_on_ev @ TA @ (A) @ B)) = (linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 29.81/8.31 thf(76,axiom,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: ((times_times @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ C @ D)) = (times_times @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_semiring__normalization__rules_I13_J)).
% 29.81/8.31 thf(486,plain,((! [TA: $tType]: ((comm_semiring_1 @ TA @ (type @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: ((times_times @ TA @ (times_times @ TA @ A @ B) @ (times_times @ TA @ C @ D)) = (times_times @ TA @ (times_times @ TA @ A @ C) @ (times_times @ TA @ B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 29.81/8.31 thf(20,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((^ [B:(stream @ TA)]: ~ (linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B)) = (linear505997466_on_ev @ TA @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_not__alw__not)).
% 29.81/8.31 thf(337,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o)]: ((^ [B:(stream @ TA)]: ~ (linear1386806755on_alw @ TA @ (^ [C:(stream @ TA)]: ~ (A @ C)) @ B)) = (linear505997466_on_ev @ TA @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 29.81/8.31 thf(25,axiom,((ab_semigroup_mult @ int @ (type @ int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Oab__semigroup__mult)).
% 29.81/8.31 thf(354,plain,((ab_semigroup_mult @ int @ (type @ int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 29.81/8.31 thf(223,axiom,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => ((ord_less @ TA @ B @ (zero_zero @ TA)) => (ord_less @ TA @ (times_times @ TA @ B @ A) @ (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_mult__pos__neg2)).
% 29.81/8.31 thf(1009,plain,((! [TA: $tType]: ((linord20386208strict @ TA @ (type @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) => ((ord_less @ TA @ B @ (zero_zero @ TA)) => (ord_less @ TA @ (times_times @ TA @ B @ A) @ (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 29.81/8.31 thf(9,axiom,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ A) @ B) => ((linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((linear1386806755on_alw @ TA @ A @ D) => (linear505997466_on_ev @ TA @ C @ D))) @ B) => (linear505997466_on_ev @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_ev__alw__alw__impl)).
% 29.81/8.31 thf(309,plain,((! [TA: $tType]: (! [A:((stream @ TA) > $o),B:(stream @ TA),C:((stream @ TA) > $o)]: ((linear505997466_on_ev @ TA @ (linear1386806755on_alw @ TA @ A) @ B) => ((linear1386806755on_alw @ TA @ (^ [D:(stream @ TA)]: ((linear1386806755on_alw @ TA @ A @ D) => (linear505997466_on_ev @ TA @ C @ D))) @ B) => (linear505997466_on_ev @ TA @ (C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 29.81/8.31 thf(98,axiom,((zero @ nat @ (type @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ozero_12)).
% 29.81/8.31 thf(543,plain,((zero @ nat @ (type @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 29.81/8.31 thf(78,axiom,((! [TA: $tType]: ((ab_semigroup_mult @ TA @ (type @ 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_120_mult_Oleft__commute)).
% 29.81/8.31 thf(491,plain,((! [TA: $tType]: ((ab_semigroup_mult @ TA @ (type @ 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)],[78])).
% 29.81/8.31 thf(109,axiom,((! [A:nat,B:nat]: ((ord_less @ int @ (semiring_1_of_nat @ int @ A) @ (semiring_1_of_nat @ int @ B)) = (ord_less @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_transfer__int__nat__relations_I2_J)).
% 29.81/8.31 thf(592,plain,((! [A:nat,B:nat]: ((ord_less @ int @ (semiring_1_of_nat @ int @ A) @ (semiring_1_of_nat @ int @ B)) = (ord_less @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 29.81/8.31 thf(144,axiom,((! [A:extended_enat]: ~ (ord_less @ extended_enat @ (extend1396239628finity @ extended_enat) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_enat__ord__simps_I6_J)).
% 29.81/8.31 thf(708,plain,((! [A:extended_enat]: ~ (ord_less @ extended_enat @ (extend1396239628finity @ extended_enat) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 29.81/8.31 thf(235,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_198_nat__mult__less__cancel__disj)).
% 29.81/8.31 thf(1037,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)],[235])).
% 29.81/8.31 thf(168,axiom,((! [A:nat]: ((extended_enat2 @ A) != (extend1396239628finity @ extended_enat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_enat_Odistinct_I1_J)).
% 29.81/8.31 thf(775,plain,((! [A:nat]: ~ ((extended_enat2 @ A) = (extend1396239628finity @ extended_enat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 29.81/8.31 thf(161,axiom,((! [A:extended_enat]: ((ord_less @ extended_enat @ A @ (extend1396239628finity @ extended_enat)) => (~ (! [B:nat]: (A != (extended_enat2 @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_less__infinityE)).
% 29.81/8.31 thf(755,plain,((! [A:extended_enat]: ((ord_less @ extended_enat @ A @ (extend1396239628finity @ extended_enat)) => (~ (! [B:nat]: ~ (A = (extended_enat2 @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 29.81/8.31 thf(134,axiom,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (inverse_inverse @ TA @ A)) => ((A != (zero_zero @ TA)) => (ord_less @ TA @ (zero_zero @ TA) @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_inverse__positive__imp__positive)).
% 29.81/8.31 thf(676,plain,((! [TA: $tType]: ((linordered_field @ TA @ (type @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (inverse_inverse @ TA @ A)) => ((~ (A = (zero_zero @ TA))) => (ord_less @ TA @ (zero_zero @ TA) @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 29.81/8.31 thf(1261,plain,(($false)),inference(e,[status(thm)],[1036,629,1168,1105,893,518,555,1110,352,333,1031,977,762,449,614,861,1142,379,440,655,511,385,1137,715,472,814,698,747,340,538,829,898,782,320,436,651,841,417,973,1046,389,724,785,372,838,802,1059,460,1087,870,881,1100,1040,376,623,514,1183,480,1051,821,734,1119,998,1201,1104,527,397,687,307,1074,452,439,529,661,810,366,1067,910,825,302,349,1174,561,392,297,424,407,815,746,1091,566,329,461,1079,1012,682,1195,551,1128,1089,1143,317,650,1006,388,420,499,980,403,884,1160,1028,901,526,489,1016,547,706,679,970,1114,1131,1192,457,721,569,779,605,1086,508,311,765,1071,674,1185,718,633,360,773,794,412,430,1103,689,904,1125,743,711,413,1139,445,382,572,713,1107,804,540,406,831,1011,737,599,863,1043,434,303,1122,890,387,494,858,535,609,323,483,700,895,769,1022,668,1177,799,1162,983,1198,868,455,1015,1000,299,505,431,658,521,1171,1176,608,394,306,1113,563,1034,1134,812,617,355,553,1049,1081,749,1003,855,872,887,409,993,1025,295,1053,1188,502,470,1130,544,336,703,600,386,314,595,612,497,845,627,1084,1180,363,524,495,759,1189,771,1062,731,995,1077,346,832,684,1116,620,752,967,835,854,865,603,326,437,474,400,828,532,1165,358,807,1056,664,624,464,332,1019,822,442,1120,369,728,740,1152,427,486,337,354,1009,309,543,491,592,708,1037,775,755,676])).
% 29.81/8.31 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.81/8.31 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------