%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : DAT129^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 : n017.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:01 AM UTC 2026
% Result : Theorem 20.44s 5.69s
% Output : Refutation 21.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : DAT129^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.11/0.21 % Computer : n017.cluster.edu
% 0.11/0.21 % Model : x86_64 x86_64
% 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.21 % Memory : 8046.5625MB
% 0.11/0.21 % OS : Linux 6.8.0-71-generic
% 0.11/0.21 % CPULimit : 300
% 0.11/0.21 % WCLimit : 300
% 0.11/0.21 % DateTime : Tue Sep 29 17:54:07 UTC 2026
% 0.11/0.21 % CPUTime :
% 0.11/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.89/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.44/1.20 % [INFO] Parsing done (408ms).
% 2.44/1.22 % [INFO] Running in sequential loop mode.
% 3.13/1.59 % [INFO] eprover registered as external prover.
% 3.32/1.60 % [INFO] Scanning for conjecture ...
% 3.52/1.75 % [INFO] Found a conjecture (or negated_conjecture) and 282 axioms. Running axiom selection ...
% 4.08/1.90 % [INFO] Axiom selection finished. Selected 281 axioms (removed 1 axioms).
% 4.70/2.18 % [INFO] Problem is higher-order (TPTP THF).
% 4.96/2.21 % [INFO] Type checking passed.
% 4.96/2.21 % [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 ...
% 20.44/5.68 % External prover 'e' found a proof!
% 20.44/5.68 % [INFO] Killing All external provers ...
% 20.44/5.69 % Time passed: 5333ms (effective reasoning time: 4465ms)
% 20.44/5.69 % 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)>
% 20.44/5.69 % Axioms used in derivation (281): fact_218_add_Ocomm__neutral, tcon_Extended__Nat_Oenat___Groups_Ominus_12, fact_54_not__less0, fact_239_less__add__eq__less, tcon_fun___Groups_Ominus, fact_227_add__less__imp__less__left, fact_226_add__strict__right__mono, fact_37_diff__self, fact_8_Suc__inject, fact_15_i0__less, fact_183_add__cancel__right__right, fact_229_diff__eq__eq, fact_75_gr0__conv__Suc, fact_64_infinite__descent, fact_144_enat_Osize_I4_J, fact_151_enat__ex__split, fact_182_add__cancel__right__left, fact_22_less__numeral__extra_I3_J, fact_110_less__enatE, fact_201_less__add__same__cancel1, tcon_Nat_Onat___Groups_Ocomm__monoid__diff, fact_159_less__imp__diff__less, fact_214_diff__add__inverse, fact_117_minus__apply, fact_219_add_Ogroup__left__neutral, fact_204_diff__add__zero, fact_107_old_Onat_Oexhaust, fact_179_double__zero__sym, fact_210_diff__commute, fact_99_old_Onat_Odistinct_I1_J, fact_21_not__gr__zero, tcon_Nat_Onat___Groups_Ocancel__comm__monoid__add, fact_100_nat_OdiscI, fact_130_lappend__code_I2_J, fact_58_less__not__refl2, fact_233_diff__add__eq, fact_131_not__infinity__eq, fact_40_lessI, fact_82_Suc__lessD, fact_139_enat_Osimps_I7_J, fact_73_less__Suc__eq__0__disj, fact_113_enat__0__iff_I2_J, fact_162_lnth__lappend1, tcon_Extended__Nat_Oenat___Groups_Ocanonically__ordered__monoid__add_6, tcon_Nat_Onat___Groups_Oordered__ab__semigroup__monoid__add__imp__le, fact_184_add__less__cancel__left, fact_122_ldrop__lappend, fact_88_not__less__eq, fact_207_diff__add__0, fact_106_Zero__not__Suc, fact_235_diff__diff__add, fact_202_add__less__same__cancel2, fact_7_assms, fact_39_less__Suc0, fact_174_add__left__cancel, fact_18_lift__Suc__mono__less__iff, fact_191_add__diff__cancel__right_H, fact_91_Suc__less__SucD, fact_248_nat__add__right__cancel, fact_209_diff__cancel2, fact_87_less__Suc__eq, fact_147_minus__nat_Odiff__0, fact_221_add__mono__thms__linordered__field_I5_J, fact_114_zero__reorient, fact_55_less__zeroE, fact_124_lstrict__prefix__llength__less, fact_194_add__Suc__right, tcon_Nat_Onat___Groups_Oordered__ab__semigroup__add, tcon_Extended__Nat_Oenat___Groups_Omonoid__add_10, fact_134_enat__ord__simps_I4_J, fact_83_Suc__lessE, tcon_Nat_Onat___Groups_Ocomm__monoid__add, fact_52_gr0I, fact_94_strict__inc__induct, fact_213_add__eq__self__zero, fact_241_trans__less__add1, fact_80_diff__strict__mono, fact_246_add__lessD1, tcon_Nat_Onat___Groups_Ocancel__semigroup__add, fact_11_enat_Osimps_I6_J, fact_19_lift__Suc__mono__less, tcon_HOL_Obool___Groups_Ominus_4, fact_79_diff__eq__diff__less, fact_211_less__diff__conv, fact_47_idiff__0, fact_236_add__implies__diff, fact_243_not__add__less2, fact_240_trans__less__add2, fact_35_zero__diff, fact_105_Zero__neq__Suc, fact_86_less__SucI, fact_234_diff__add__eq__diff__diff__swap, tcon_Nat_Onat___Rings_Olinordered__semidom, fact_245_add__less__mono, tcon_Nat_Onat___Groups_Omonoid__add, fact_217_comm__monoid__add__class_Oadd__0, fact_156_enat_Odistinct_I1_J, fact_200_less__add__same__cancel2, fact_66_linorder__neqE__nat, fact_132_not__enat__eq, fact_127_Suc__diff__diff, fact_116_case__enat__0, fact_28_enat_Osimps_I4_J, fact_69_infinite__descent__measure, fact_208_Nat_Odiff__cancel, fact_193_Nat_Oadd__0__right, fact_166_infinity__ilessE, fact_140_Suc__pred, fact_61_gr__implies__not0, fact_121_llength__ldrop, fact_4_enat_Oinject, fact_192_add__is__0, fact_185_add__less__cancel__right, fact_62_less__irrefl__nat, fact_96_less__iff__diff__less__0, fact_164_diff__less__Suc, tcon_Nat_Onat___Groups_Oordered__ab__semigroup__add__imp__le, fact_196_diff__diff__left, fact_154_enat3__cases, fact_228_add__less__imp__less__right, fact_72_diff__eq__diff__eq, fact_230_eq__diff__eq, fact_203_add__less__same__cancel1, fact_118_enat_Osize_I1_J, tcon_Extended__Nat_Oenat___Groups_Oordered__ab__semigroup__add_7, fact_46_idiff__0__right, fact_36_diff__0__right, tcon_Nat_Onat___Groups_Ozero, fact_102_diff__induct, fact_53_not__gr0, fact_180_add__cancel__left__left, fact_216_add__diff__inverse__nat, fact_68_measure__induct__rule, fact_71_diff__right__commute, fact_152_enat_Oinducts, fact_26_zero__less__iff__neq__zero, fact_187_diff__add__cancel, fact_108_old_Onat_Oinducts, fact_6_old_Onat_Oinject, fact_29_llength__ldropn, fact_237_add__Suc, fact_186_add__diff__cancel, tcon_Extended__Nat_Oenat___Groups_Oab__semigroup__add_8, fact_57_less__not__refl, fact_244_not__add__less1, fact_212_plus__nat_Oadd__0, fact_199_double__add__less__zero__iff__single__add__less__zero, fact_177_add_Oright__neutral, fact_149_llist__less__induct, fact_198_zero__less__double__add__iff__zero__less__single__add, fact_126_diff__self__eq__0, fact_30_neq0__conv, fact_24_not__less__zero, fact_197_ldropn__ldropn, fact_148_lappend__assoc, fact_34_diff__zero, fact_178_double__zero, fact_137_enat_Osimps_I5_J, fact_168_enat__ord__code_I4_J, fact_16_not__iless0, fact_119_ldropn__Suc__conv__ldropn, fact_206_the__enat__0, fact_143_idiff__self, fact_25_gr__implies__not__zero, fact_150_zero__induct__lemma, fact_9_n__not__Suc__n, tcon_Nat_Onat___Groups_Ocancel__ab__semigroup__add, fact_173_exists__least__lemma, fact_59_less__not__refl3, fact_63_nat__less__induct, fact_125_diff__0__eq__0, fact_163_Suc__diff__Suc, fact_103_zero__induct, fact_84_Suc__lessI, fact_123_idiff__infinity__right, fact_13_enat__iless, fact_231_add__diff__eq, fact_14_ldrop__0, fact_167_less__infinityE, fact_93_less__Suc__induct, fact_120_enat_Osize_I3_J, fact_189_add__diff__cancel__left_H, fact_115_ldrop__eq__LConsD, tcon_Extended__Nat_Oenat___Orderings_Oorder_11, tcon_Extended__Nat_Oenat___Groups_Ocomm__monoid__add_9, fact_215_diff__add__inverse2, fact_90_less__antisym, fact_49_diff__gt__0__iff__gt, fact_181_add__cancel__left__right, fact_48_llast__LCons2, fact_76_eq__iff__diff__eq__0, fact_51_ldropn__Suc__LCons, fact_161_diff__less, fact_145_enat_Osize_I2_J, tcon_Nat_Onat___Groups_Oordered__cancel__ab__semigroup__add, fact_112_enat__0__iff_I1_J, fact_44_idiff__enat__0__right, fact_31_llist_Oinject, tcon_HOL_Obool___Orderings_Oorder_3, fact_27_ldropn__eq__LConsD, fact_89_Suc__less__eq2, fact_81_lessE, fact_67_less__nat__zero__code, tcon_Nat_Onat___Groups_Ominus_2, fact_41_Suc__mono, fact_5_nat_Oinject, fact_250_is__num__normalize_I1_J, fact_17_enat__less__induct, fact_232_diff__diff__eq2, fact_10_ldrop__enat, fact_109_not0__implies__Suc, fact_225_add__strict__left__mono, fact_247_nat__add__left__cancel, fact_176_add_Oleft__neutral, fact_238_add__Suc__shift, fact_190_add__diff__cancel__right, fact_45_idiff__enat__0, fact_175_add__right__cancel, fact_92_less__trans__Suc, fact_50_enat__ord__simps_I2_J, fact_155_enat2__cases, tcon_fun___Orderings_Oorder, fact_129_zero__less__diff, fact_33_cancel__comm__monoid__add__class_Odiff__cancel, fact_172_lnth__ldropn, tcon_Extended__Nat_Oenat___Groups_Ostrict__ordered__ab__semigroup__add_5, fact_242_add__less__mono1, fact_223_add__mono__thms__linordered__field_I1_J, fact_136_idiff__infinity, tcon_Nat_Onat___Groups_Ostrict__ordered__ab__semigroup__add, fact_169_fun__diff__def, fact_95_not__less__less__Suc__eq, tcon_Nat_Onat___Orderings_Oorder_1, fact_104_Suc__neq__Zero, fact_205_add__gr__0, fact_142_lnth__Suc__LCons, fact_85_less__SucE, fact_97_nat_Odistinct_I1_J, tcon_Extended__Nat_Oenat___Groups_Ozero_13, tcon_Nat_Onat___Groups_Ocanonically__ordered__monoid__add, fact_77_diff__strict__right__mono, fact_98_old_Onat_Odistinct_I2_J, fact_170_ldropn__lappend, fact_111_zero__enat__def, fact_157_enat_Odistinct_I2_J, fact_65_infinite__descent0, fact_133_enat__ord__simps_I6_J, fact_220_add__eq__0__iff__both__eq__0, fact_60_measure__induct, fact_42_Suc__less__eq, fact_188_add__diff__cancel__left, fact_56_nat__neq__iff, fact_224_add__strict__mono, fact_146_diffs0__imp__equal, fact_171_lnth__lappend, fact_78_diff__strict__left__mono, fact_0_n, fact_153_enat_Oexhaust, fact_249_ab__semigroup__add__class_Oadd__ac_I1_J, fact_23_gr__zeroI, tcon_Nat_Onat___Groups_Oab__semigroup__add, fact_74_gr0__implies__Suc, fact_222_add__mono__thms__linordered__field_I2_J, fact_3__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062n_H_O_An_A_061_Aenat_An_H_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062, fact_158_infinity__ne__i0, fact_128_diff__Suc__Suc, fact_135_idiff__enat__enat, fact_141_lnth__0, fact_38_zero__less__Suc, fact_32_ldropn__0, fact_160_diff__less__mono2, fact_195_nat__add__left__cancel__less, fact_2_Suc_Oprems, fact_138_lstrict__prefix__code_I4_J, fact_165_diff__Suc__less, fact_101_nat__induct, fact_70_infinite__descent0__measure, fact_251_add__mono__thms__linordered__semiring_I4_J, fact_20_llast__ldropn, fact_1_Suc_Ohyps, fact_12_chain__incr
% 20.44/5.69 % No. of inferences in proof: 566
% 20.44/5.69 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 5333 ms resp. 4465 ms w/o parsing
% 21.68/5.92 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.68/5.92 thf(extended_enat_type, type, extended_enat: $tType).
% 21.68/5.92 thf(nat_type, type, nat: $tType).
% 21.68/5.92 thf(a_type, type, a: $tType).
% 21.68/5.92 thf(zero_decl, type, zero: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(minus_decl, type, minus: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(neg_numeral_decl, type, neg_numeral: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(order_decl, type, order: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(group_add_decl, type, group_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(monoid_add_decl, type, monoid_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(ab_group_add_decl, type, ab_group_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(comm_monoid_add_decl, type, comm_monoid_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(ab_semigroup_add_decl, type, ab_semigroup_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(comm_monoid_diff_decl, type, comm_monoid_diff: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(linordered_semidom_decl, type, linordered_semidom: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(cancel_semigroup_add_decl, type, cancel_semigroup_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(ordered_ab_group_add_decl, type, ordered_ab_group_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(cancel1352612707id_add_decl, type, cancel1352612707id_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(cancel146912293up_add_decl, type, cancel146912293up_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(linord219039673up_add_decl, type, linord219039673up_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(ordere779506340up_add_decl, type, ordere779506340up_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(canoni770627133id_add_decl, type, canoni770627133id_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(ordere236663937imp_le_decl, type, ordere236663937imp_le: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(ordere223160158up_add_decl, type, ordere223160158up_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(strict2144017051up_add_decl, type, strict2144017051up_add: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(ordere516151231imp_le_decl, type, ordere516151231imp_le: !> [TA: $tType]: ((itself @ TA) > $o)).
% 21.68/5.92 thf(coindu268472904append_decl, type, coindu268472904append: !> [TA: $tType]: ((coindu1593790203_llist @ TA) > ((coindu1593790203_llist @ TA) > (coindu1593790203_llist @ TA)))).
% 21.68/5.92 thf(coindu191418589_ldrop_decl, type, coindu191418589_ldrop: !> [TA: $tType]: (extended_enat > ((coindu1593790203_llist @ TA) > (coindu1593790203_llist @ TA)))).
% 21.68/5.92 thf(coindu531130065ldropn_decl, type, coindu531130065ldropn: !> [TA: $tType]: (nat > ((coindu1593790203_llist @ TA) > (coindu1593790203_llist @ TA)))).
% 21.68/5.92 thf(coindu2000965700_llast_decl, type, coindu2000965700_llast: !> [TA: $tType]: ((coindu1593790203_llist @ TA) > TA)).
% 21.68/5.92 thf(coindu1018505716length_decl, type, coindu1018505716length: !> [TA: $tType]: ((coindu1593790203_llist @ TA) > extended_enat)).
% 21.68/5.92 thf(coindu1121789889_LCons_decl, type, coindu1121789889_LCons: !> [TA: $tType]: (TA > ((coindu1593790203_llist @ TA) > (coindu1593790203_llist @ TA)))).
% 21.68/5.92 thf(coindu749330388e_lnth_decl, type, coindu749330388e_lnth: !> [TA: $tType]: ((coindu1593790203_llist @ TA) > (nat > TA))).
% 21.68/5.92 thf(coindu574146665prefix_decl, type, coindu574146665prefix: !> [TA: $tType]: ((coindu1593790203_llist @ TA) > ((coindu1593790203_llist @ TA) > $o))).
% 21.68/5.92 thf(extended_enat2_decl, type, extended_enat2: (nat > extended_enat)).
% 21.68/5.92 thf(extended_case_enat_decl, type, extended_case_enat: !> [TA: $tType]: ((nat > TA) > (TA > (extended_enat > TA)))).
% 21.68/5.92 thf(extended_rec_enat_decl, type, extended_rec_enat: !> [TA: $tType]: ((nat > TA) > (TA > (extended_enat > TA)))).
% 21.68/5.92 thf(extended_size_enat_decl, type, extended_size_enat: (extended_enat > nat)).
% 21.68/5.92 thf(extend1396239628finity_decl, type, extend1396239628finity: !> [TA: $tType]: TA).
% 21.68/5.92 thf(extended_the_enat_decl, type, extended_the_enat: (extended_enat > nat)).
% 21.68/5.92 thf(minus_minus_decl, type, minus_minus: !> [TA: $tType]: (TA > (TA > TA))).
% 21.68/5.92 thf(plus_plus_decl, type, plus_plus: !> [TA: $tType]: (TA > (TA > TA))).
% 21.68/5.92 thf(zero_zero_decl, type, zero_zero: !> [TA: $tType]: TA).
% 21.68/5.92 thf(suc_decl, type, suc: (nat > nat)).
% 21.68/5.92 thf(size_size_decl, type, size_size: !> [TA: $tType]: (TA > nat)).
% 21.68/5.92 thf(ord_less_decl, type, ord_less: !> [TA: $tType]: (TA > (TA > $o))).
% 21.68/5.92 thf(type2_decl, type, type2: !> [TA: $tType]: (itself @ TA)).
% 21.68/5.92 thf(n_decl, type, n: extended_enat).
% 21.68/5.92 thf(n2_decl, type, n2: nat).
% 21.68/5.92 thf(n_a_decl, type, n_a: nat).
% 21.68/5.92 thf(xs_decl, type, xs: (coindu1593790203_llist @ a)).
% 21.68/5.92 thf(xsa_decl, type, xsa: (coindu1593790203_llist @ a)).
% 21.68/5.92 thf(182,axiom,((! [TA: $tType]: (! [A:(coindu1593790203_llist @ TA)]: ((coindu191418589_ldrop @ TA @ (zero_zero @ extended_enat) @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_ldrop__0)).
% 21.68/5.92 thf(809,plain,((! [TA: $tType]: (! [A:(coindu1593790203_llist @ TA)]: ((coindu191418589_ldrop @ TA @ (zero_zero @ extended_enat) @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 21.68/5.92 thf(119,axiom,((! [TA: $tType]: ((monoid_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((plus_plus @ TA @ A @ (zero_zero @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_add_Oright__neutral)).
% 21.68/5.92 thf(629,plain,((! [TA: $tType]: ((monoid_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((plus_plus @ TA @ A @ (zero_zero @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 21.68/5.92 thf(163,axiom,((! [TA: $tType]: (! [A:TA,B:(coindu1593790203_llist @ TA)]: ((coindu749330388e_lnth @ TA @ (coindu1121789889_LCons @ TA @ A @ B) @ (zero_zero @ nat)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_lnth__0)).
% 21.68/5.92 thf(760,plain,((! [TA: $tType]: (! [A:TA,B:(coindu1593790203_llist @ TA)]: ((coindu749330388e_lnth @ TA @ (coindu1121789889_LCons @ TA @ A @ B) @ (zero_zero @ nat)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 21.68/5.92 thf(169,axiom,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((plus_plus @ TA @ A @ (minus_minus @ TA @ B @ C)) = (minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_add__diff__eq)).
% 21.68/5.92 thf(777,plain,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((plus_plus @ TA @ A @ (minus_minus @ TA @ B @ C)) = (minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 21.68/5.92 thf(130,axiom,((! [A:extended_enat]: ((ord_less @ extended_enat @ A @ (extend1396239628finity @ extended_enat)) = (A != (extend1396239628finity @ extended_enat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_enat__ord__simps_I4_J)).
% 21.68/5.92 thf(666,plain,((! [A:extended_enat]: ((ord_less @ extended_enat @ A @ (extend1396239628finity @ extended_enat)) = (~ (A = (extend1396239628finity @ extended_enat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 21.68/5.92 thf(29,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_less__not__refl)).
% 21.68/5.92 thf(352,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 21.68/5.92 thf(77,axiom,((! [TA: $tType]: ((ordere223160158up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: (((ord_less @ TA @ A @ B) & (C = D)) => (ord_less @ TA @ (plus_plus @ TA @ A @ C) @ (plus_plus @ TA @ B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_add__mono__thms__linordered__field_I1_J)).
% 21.68/5.92 thf(479,plain,((! [TA: $tType]: ((ordere223160158up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: (((ord_less @ TA @ A @ B) & (C = D)) => (ord_less @ TA @ (plus_plus @ TA @ A @ C) @ (plus_plus @ TA @ B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 21.68/5.92 thf(256,axiom,((! [A:nat,B:nat]: ((minus_minus @ nat @ (suc @ A) @ (suc @ B)) = (minus_minus @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_diff__Suc__Suc)).
% 21.68/5.92 thf(1105,plain,((! [A:nat,B:nat]: ((minus_minus @ nat @ (suc @ A) @ (suc @ B)) = (minus_minus @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 21.68/5.92 thf(22,axiom,(((extend1396239628finity @ extended_enat) != (zero_zero @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_infinity__ne__i0)).
% 21.68/5.92 thf(333,plain,((~ ((extend1396239628finity @ extended_enat) = (zero_zero @ extended_enat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 21.68/5.92 thf(118,axiom,((cancel146912293up_add @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocancel__ab__semigroup__add)).
% 21.68/5.92 thf(628,plain,((cancel146912293up_add @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 21.68/5.92 thf(223,axiom,((! [A:nat,B:nat,C:(nat > (nat > $o))]: ((ord_less @ nat @ A @ B) => ((! [D:nat]: (C @ D @ (suc @ D))) => ((! [D:nat,E:nat,F:nat]: ((ord_less @ nat @ D @ E) => ((ord_less @ nat @ E @ F) => ((C @ D @ E) => ((C @ E @ F) => (C @ D @ F)))))) => (C @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_less__Suc__induct)).
% 21.68/5.92 thf(977,plain,((! [A:nat,B:nat,C:(nat > (nat > $o))]: ((ord_less @ nat @ A @ B) => ((! [D:nat]: (C @ D @ (suc @ D))) => ((! [D:nat,E:nat,F:nat]: ((ord_less @ nat @ D @ E) => ((ord_less @ nat @ E @ F) => ((C @ D @ E) => ((C @ E @ F) => (C @ D @ F)))))) => (C @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 21.68/5.92 thf(267,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ B) => (~ (! [C:nat]: ((ord_less @ nat @ A @ C) => (B != (suc @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_Suc__lessE)).
% 21.68/5.92 thf(1158,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ B) => (~ (! [C:nat]: ((ord_less @ nat @ A @ C) => (~ (B = (suc @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 21.68/5.92 thf(154,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_64_infinite__descent)).
% 21.68/5.92 thf(730,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)],[154])).
% 21.68/5.92 thf(11,axiom,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((plus_plus @ TA @ (minus_minus @ TA @ A @ B) @ B) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_diff__add__cancel)).
% 21.68/5.92 thf(308,plain,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((plus_plus @ TA @ (minus_minus @ TA @ A @ B) @ B) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 21.68/5.92 thf(66,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type2 @ TA)) => (! [A:TA]: ~ (ord_less @ TA @ A @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_not__less__zero)).
% 21.68/5.92 thf(449,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type2 @ TA)) => (! [A:TA]: ~ (ord_less @ TA @ A @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 21.68/5.92 thf(39,axiom,((! [A:extended_enat]: ((minus_minus @ extended_enat @ (zero_zero @ extended_enat) @ A) = (zero_zero @ extended_enat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_idiff__0)).
% 21.68/5.92 thf(379,plain,((! [A:extended_enat]: ((minus_minus @ extended_enat @ (zero_zero @ extended_enat) @ A) = (zero_zero @ extended_enat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 21.68/5.92 thf(41,axiom,((! [A:nat,B:nat]: (((plus_plus @ nat @ A @ B) = (zero_zero @ nat)) = ((A = (zero_zero @ nat)) & (B = (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_add__is__0)).
% 21.68/5.92 thf(385,plain,((! [A:nat,B:nat]: (((plus_plus @ nat @ A @ B) = (zero_zero @ nat)) = ((A = (zero_zero @ nat)) & (B = (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 21.68/5.92 thf(84,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_not__less0)).
% 21.68/5.92 thf(500,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 21.68/5.92 thf(177,axiom,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((A = (plus_plus @ TA @ B @ A)) = (B = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_add__cancel__right__left)).
% 21.68/5.92 thf(797,plain,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((A = (plus_plus @ TA @ B @ A)) = (B = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 21.68/5.92 thf(143,axiom,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: (((plus_plus @ TA @ A @ B) = A) = (B = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_add__cancel__left__right)).
% 21.68/5.92 thf(698,plain,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: (((plus_plus @ TA @ A @ B) = A) = (B = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 21.68/5.92 thf(214,axiom,((~ (! [A:nat]: (n != (extended_enat2 @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062n_H_O_An_A_061_Aenat_An_H_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062)).
% 21.68/5.92 thf(945,plain,((~ (! [A:nat]: ~ (n = (extended_enat2 @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 21.68/5.92 thf(25,axiom,(((size_size @ extended_enat @ (extend1396239628finity @ extended_enat)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_enat_Osize_I4_J)).
% 21.68/5.92 thf(340,plain,(((size_size @ extended_enat @ (extend1396239628finity @ extended_enat)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 21.68/5.92 thf(132,axiom,((! [TA: $tType]: ((linord219039673up_add @ TA @ (type2 @ TA)) => (! [A:TA]: (((plus_plus @ TA @ A @ A) = (zero_zero @ TA)) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_double__zero)).
% 21.68/5.92 thf(670,plain,((! [TA: $tType]: ((linord219039673up_add @ TA @ (type2 @ TA)) => (! [A:TA]: (((plus_plus @ TA @ A @ A) = (zero_zero @ TA)) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 21.68/5.92 thf(146,axiom,((! [TA: $tType]: ((ordere223160158up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (plus_plus @ TA @ C @ A) @ (plus_plus @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_add__strict__left__mono)).
% 21.68/5.92 thf(709,plain,((! [TA: $tType]: ((ordere223160158up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (plus_plus @ TA @ C @ A) @ (plus_plus @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 21.68/5.92 thf(239,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ B) = (? [C:nat]: ((B = (suc @ C)) & (ord_less @ nat @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_Suc__less__eq2)).
% 21.68/5.92 thf(1046,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ B) = (? [C:nat]: ((B = (suc @ C)) & (ord_less @ nat @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 21.68/5.92 thf(60,axiom,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ B) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_add__diff__cancel)).
% 21.68/5.92 thf(436,plain,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ B) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 21.68/5.92 thf(126,axiom,((! [TA: $tType]: ((ordere236663937imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ A @ C)) = (ord_less @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_add__less__cancel__left)).
% 21.68/5.92 thf(651,plain,((! [TA: $tType]: ((ordere236663937imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ A @ C)) = (ord_less @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 21.68/5.92 thf(186,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_152_enat_Oinducts)).
% 21.68/5.92 thf(829,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)],[186])).
% 21.68/5.92 thf(48,axiom,((! [TA: $tType]: ((cancel146912293up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ A) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_add__diff__cancel__left_H)).
% 21.68/5.92 thf(404,plain,((! [TA: $tType]: ((cancel146912293up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ A) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 21.68/5.92 thf(242,axiom,((ord_less @ extended_enat @ (extended_enat2 @ (suc @ n_a)) @ (coindu1018505716length @ a @ xsa))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_Suc_Oprems)).
% 21.68/5.92 thf(1055,plain,((ord_less @ extended_enat @ (extended_enat2 @ (suc @ n_a)) @ (coindu1018505716length @ a @ xsa))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 21.68/5.92 thf(206,axiom,((! [A:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) = (? [B:nat]: (A = (suc @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_gr0__conv__Suc)).
% 21.68/5.92 thf(917,plain,((! [A:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) = (? [B:nat]: (A = (suc @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 21.68/5.92 thf(104,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less @ nat @ A @ B) => (((plus_plus @ nat @ C @ B) = (plus_plus @ nat @ A @ D)) => (ord_less @ nat @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_less__add__eq__less)).
% 21.68/5.92 thf(587,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less @ nat @ A @ B) => (((plus_plus @ nat @ C @ B) = (plus_plus @ nat @ A @ D)) => (ord_less @ nat @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 21.68/5.92 thf(116,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_69_infinite__descent__measure)).
% 21.68/5.92 thf(619,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)],[116])).
% 21.68/5.92 thf(188,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_155_enat2__cases)).
% 21.68/5.92 thf(838,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)],[188])).
% 21.68/5.92 thf(91,axiom,((! [TA: $tType]: (! [A:(coindu1593790203_llist @ TA)]: ((coindu531130065ldropn @ TA @ (zero_zero @ nat) @ A) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_ldropn__0)).
% 21.68/5.92 thf(542,plain,((! [TA: $tType]: (! [A:(coindu1593790203_llist @ TA)]: ((coindu531130065ldropn @ TA @ (zero_zero @ nat) @ A) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 21.68/5.92 thf(70,axiom,((! [A:nat,B:nat]: ((minus_minus @ nat @ (plus_plus @ nat @ A @ B) @ A) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_diff__add__inverse)).
% 21.68/5.92 thf(460,plain,((! [A:nat,B:nat]: ((minus_minus @ nat @ (plus_plus @ nat @ A @ B) @ A) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 21.68/5.92 thf(201,axiom,((! [A:nat]: ((ord_less @ nat @ A @ (suc @ (zero_zero @ nat))) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_less__Suc0)).
% 21.68/5.92 thf(902,plain,((! [A:nat]: ((ord_less @ nat @ A @ (suc @ (zero_zero @ nat))) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 21.68/5.92 thf(122,axiom,((! [TA: $tType]: ((linord219039673up_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (plus_plus @ TA @ A @ A)) = (ord_less @ TA @ (zero_zero @ TA) @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_zero__less__double__add__iff__zero__less__single__add)).
% 21.68/5.92 thf(638,plain,((! [TA: $tType]: ((linord219039673up_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (plus_plus @ TA @ A @ A)) = (ord_less @ TA @ (zero_zero @ TA) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 21.68/5.92 thf(263,axiom,((! [A:extended_enat]: ((minus_minus @ extended_enat @ (extended_enat2 @ (zero_zero @ nat)) @ A) = (extended_enat2 @ (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_idiff__enat__0)).
% 21.68/5.92 thf(1147,plain,((! [A:extended_enat]: ((minus_minus @ extended_enat @ (extended_enat2 @ (zero_zero @ nat)) @ A) = (extended_enat2 @ (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 21.68/5.92 thf(279,axiom,((! [A:(nat > $o),B:nat]: ((A @ B) => ((! [C:nat]: ((A @ (suc @ C)) => (A @ C))) => (A @ (zero_zero @ nat)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_zero__induct)).
% 21.68/5.92 thf(1247,plain,((! [A:(nat > $o),B:nat]: ((A @ B) => ((! [C:nat]: ((A @ (suc @ C)) => (A @ C))) => (A @ (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[279])).
% 21.68/5.92 thf(193,axiom,((! [A:(nat > $o),B:nat]: ((A @ (zero_zero @ nat)) => ((! [C:nat]: ((A @ C) => (A @ (suc @ C)))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_old_Onat_Oinducts)).
% 21.68/5.92 thf(870,plain,((! [A:(nat > $o),B:nat]: ((A @ (zero_zero @ nat)) => ((! [C:nat]: ((A @ C) => (A @ (suc @ C)))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 21.68/5.92 thf(111,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_56_nat__neq__iff)).
% 21.68/5.92 thf(606,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)],[111])).
% 21.68/5.92 thf(1,conjecture,(((coindu2000965700_llast @ a @ (coindu191418589_ldrop @ a @ (extended_enat2 @ (suc @ n_a)) @ xsa)) = (coindu2000965700_llast @ a @ xsa))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 21.68/5.92 thf(2,negated_conjecture,((~ ((coindu2000965700_llast @ a @ (coindu191418589_ldrop @ a @ (extended_enat2 @ (suc @ n_a)) @ xsa)) = (coindu2000965700_llast @ a @ xsa)))),inference(neg_conjecture,[status(cth)],[1])).
% 21.68/5.92 thf(284,plain,((~ ((coindu2000965700_llast @ a @ (coindu191418589_ldrop @ a @ (extended_enat2 @ (suc @ n_a)) @ xsa)) = (coindu2000965700_llast @ a @ xsa)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 21.68/5.92 thf(19,axiom,((! [A:nat]: ((minus_minus @ nat @ A @ A) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_diff__self__eq__0)).
% 21.68/5.92 thf(325,plain,((! [A:nat]: ((minus_minus @ nat @ A @ A) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 21.68/5.92 thf(5,axiom,((! [TA: $tType]: (! [A:((coindu1593790203_llist @ TA) > $o),B:(coindu1593790203_llist @ TA)]: ((! [C:(coindu1593790203_llist @ TA)]: ((! [D:(coindu1593790203_llist @ TA)]: ((coindu574146665prefix @ TA @ D @ C) => (A @ D))) => (A @ C))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_llist__less__induct)).
% 21.68/5.92 thf(289,plain,((! [TA: $tType]: (! [A:((coindu1593790203_llist @ TA) > $o),B:(coindu1593790203_llist @ TA)]: ((! [C:(coindu1593790203_llist @ TA)]: ((! [D:(coindu1593790203_llist @ TA)]: ((coindu574146665prefix @ TA @ D @ C) => (A @ D))) => (A @ C))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 21.68/5.92 thf(65,axiom,((zero @ extended_enat @ (type2 @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Groups_Ozero_13)).
% 21.68/5.92 thf(448,plain,((zero @ extended_enat @ (type2 @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 21.68/5.92 thf(15,axiom,((! [TA: $tType,TB: $tType]: ((order @ TA @ (type2 @ TA)) => (order @ (TB > TA) @ (type2 @ (TB > TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder)).
% 21.68/5.92 thf(316,plain,((! [TA: $tType,TB: $tType]: ((order @ TA @ (type2 @ TA)) => (order @ (TB > TA) @ (type2 @ (TB > TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 21.68/5.92 thf(255,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) => (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_Suc__inject)).
% 21.68/5.92 thf(1100,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) => (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 21.68/5.92 thf(194,axiom,((! [A:nat]: ((size_size @ extended_enat @ (extended_enat2 @ A)) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_enat_Osize_I3_J)).
% 21.68/5.92 thf(881,plain,((! [A:nat]: ((size_size @ extended_enat @ (extended_enat2 @ A)) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 21.68/5.92 thf(52,axiom,((! [TA: $tType]: ((ordere236663937imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ C @ B)) => (ord_less @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_add__less__imp__less__right)).
% 21.68/5.92 thf(416,plain,((! [TA: $tType]: ((ordere236663937imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ C @ B)) => (ord_less @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 21.68/5.92 thf(174,axiom,((! [A:nat,B:nat]: (((minus_minus @ nat @ A @ B) = (zero_zero @ nat)) => (((minus_minus @ nat @ B @ A) = (zero_zero @ nat)) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_diffs0__imp__equal)).
% 21.68/5.92 thf(789,plain,((! [A:nat,B:nat]: (((minus_minus @ nat @ A @ B) = (zero_zero @ nat)) => (((minus_minus @ nat @ B @ A) = (zero_zero @ nat)) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 21.68/5.92 thf(105,axiom,((comm_monoid_add @ extended_enat @ (type2 @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Groups_Ocomm__monoid__add_9)).
% 21.68/5.92 thf(591,plain,((comm_monoid_add @ extended_enat @ (type2 @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 21.68/5.92 thf(63,axiom,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((A = B) = (C = D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_diff__eq__diff__eq)).
% 21.68/5.92 thf(443,plain,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((A = B) = (C = D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 21.68/5.92 thf(17,axiom,((canoni770627133id_add @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocanonically__ordered__monoid__add)).
% 21.68/5.92 thf(321,plain,((canoni770627133id_add @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 21.68/5.92 thf(38,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) => ((ord_less @ nat @ (zero_zero @ nat) @ B) => (ord_less @ nat @ (minus_minus @ nat @ B @ A) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_diff__less)).
% 21.68/5.92 thf(376,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) => ((ord_less @ nat @ (zero_zero @ nat) @ B) => (ord_less @ nat @ (minus_minus @ nat @ B @ A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 21.68/5.92 thf(180,axiom,(((extended_size_enat @ (extend1396239628finity @ extended_enat)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_enat_Osize_I2_J)).
% 21.68/5.92 thf(806,plain,(((extended_size_enat @ (extend1396239628finity @ extended_enat)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 21.68/5.92 thf(202,axiom,((! [A:nat,B:nat]: ((plus_plus @ nat @ (suc @ A) @ B) = (suc @ (plus_plus @ nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_add__Suc)).
% 21.68/5.92 thf(905,plain,((! [A:nat,B:nat]: ((plus_plus @ nat @ (suc @ A) @ B) = (suc @ (plus_plus @ nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 21.68/5.92 thf(165,axiom,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((A = (minus_minus @ TA @ B @ C)) = ((plus_plus @ TA @ A @ C) = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_eq__diff__eq)).
% 21.68/5.92 thf(766,plain,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((A = (minus_minus @ TA @ B @ C)) = ((plus_plus @ TA @ A @ C) = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 21.68/5.92 thf(248,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_151_enat__ex__split)).
% 21.68/5.92 thf(1072,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)],[248])).
% 21.68/5.92 thf(57,axiom,((! [TA: $tType]: ((ordere516151231imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ B) @ A) = (ord_less @ TA @ B @ (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_add__less__same__cancel1)).
% 21.68/5.92 thf(428,plain,((! [TA: $tType]: ((ordere516151231imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ B) @ A) = (ord_less @ TA @ B @ (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 21.68/5.92 thf(277,axiom,((! [TA: $tType]: (! [A:TA,B:TA,C:(coindu1593790203_llist @ TA)]: ((coindu2000965700_llast @ TA @ (coindu1121789889_LCons @ TA @ A @ (coindu1121789889_LCons @ TA @ B @ C))) = (coindu2000965700_llast @ TA @ (coindu1121789889_LCons @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_llast__LCons2)).
% 21.68/5.92 thf(1242,plain,((! [TA: $tType]: (! [A:TA,B:TA,C:(coindu1593790203_llist @ TA)]: ((coindu2000965700_llast @ TA @ (coindu1121789889_LCons @ TA @ A @ (coindu1121789889_LCons @ TA @ B @ C))) = (coindu2000965700_llast @ TA @ (coindu1121789889_LCons @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[277])).
% 21.68/5.92 thf(13,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ A @ (plus_plus @ nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_trans__less__add1)).
% 21.68/5.92 thf(312,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ A @ (plus_plus @ nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 21.68/5.92 thf(270,axiom,((! [A:nat,B:nat]: (((extended_enat2 @ A) = (extended_enat2 @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_enat_Oinject)).
% 21.68/5.92 thf(1169,plain,((! [A:nat,B:nat]: (((extended_enat2 @ A) = (extended_enat2 @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 21.68/5.92 thf(45,axiom,((comm_monoid_diff @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocomm__monoid__diff)).
% 21.68/5.92 thf(397,plain,((comm_monoid_diff @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 21.68/5.92 thf(249,axiom,((! [TA: $tType]: (! [A:nat,B:nat,C:(coindu1593790203_llist @ TA)]: ((ord_less @ extended_enat @ (extended_enat2 @ (plus_plus @ nat @ A @ B)) @ (coindu1018505716length @ TA @ C)) => ((coindu749330388e_lnth @ TA @ (coindu531130065ldropn @ TA @ A @ C) @ B) = (coindu749330388e_lnth @ TA @ C @ (plus_plus @ nat @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_lnth__ldropn)).
% 21.68/5.92 thf(1074,plain,((! [TA: $tType]: (! [A:nat,B:nat,C:(coindu1593790203_llist @ TA)]: ((ord_less @ extended_enat @ (extended_enat2 @ (plus_plus @ nat @ A @ B)) @ (coindu1018505716length @ TA @ C)) => ((coindu749330388e_lnth @ TA @ (coindu531130065ldropn @ TA @ A @ C) @ B) = (coindu749330388e_lnth @ TA @ C @ (plus_plus @ nat @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 21.68/5.92 thf(207,axiom,(((zero_zero @ extended_enat) = (extended_enat2 @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_zero__enat__def)).
% 21.68/5.92 thf(920,plain,(((zero_zero @ extended_enat) = (extended_enat2 @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 21.68/5.92 thf(209,axiom,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA),C:(coindu1593790203_llist @ TA)]: (((ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B)) => ((coindu749330388e_lnth @ TA @ (coindu268472904append @ TA @ B @ C) @ A) = (coindu749330388e_lnth @ TA @ B @ A))) & ((~ (ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B))) => ((coindu749330388e_lnth @ TA @ (coindu268472904append @ TA @ B @ C) @ A) = (coindu749330388e_lnth @ TA @ C @ (minus_minus @ nat @ A @ (extended_the_enat @ (coindu1018505716length @ TA @ B)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_lnth__lappend)).
% 21.68/5.92 thf(925,plain,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA),C:(coindu1593790203_llist @ TA)]: (((ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B)) => ((coindu749330388e_lnth @ TA @ (coindu268472904append @ TA @ B @ C) @ A) = (coindu749330388e_lnth @ TA @ B @ A))) & ((~ (ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B))) => ((coindu749330388e_lnth @ TA @ (coindu268472904append @ TA @ B @ C) @ A) = (coindu749330388e_lnth @ TA @ C @ (minus_minus @ nat @ A @ (extended_the_enat @ (coindu1018505716length @ TA @ B)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 21.68/5.92 thf(265,axiom,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA)]: ((ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B)) => ((coindu2000965700_llast @ TA @ (coindu531130065ldropn @ TA @ A @ B)) = (coindu2000965700_llast @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_llast__ldropn)).
% 21.68/5.92 thf(1153,plain,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA)]: ((ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B)) => ((coindu2000965700_llast @ TA @ (coindu531130065ldropn @ TA @ A @ B)) = (coindu2000965700_llast @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[265])).
% 21.68/5.92 thf(148,axiom,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: (((plus_plus @ TA @ A @ B) = C) => (A = (minus_minus @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_add__implies__diff)).
% 21.68/5.92 thf(714,plain,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: (((plus_plus @ TA @ A @ B) = C) => (A = (minus_minus @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 21.68/5.92 thf(268,axiom,((! [TA: $tType]: (! [A:TA,B:(coindu1593790203_llist @ TA),C:nat]: ((coindu749330388e_lnth @ TA @ (coindu1121789889_LCons @ TA @ A @ B) @ (suc @ C)) = (coindu749330388e_lnth @ TA @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_lnth__Suc__LCons)).
% 21.68/5.92 thf(1163,plain,((! [TA: $tType]: (! [A:TA,B:(coindu1593790203_llist @ TA),C:nat]: ((coindu749330388e_lnth @ TA @ (coindu1121789889_LCons @ TA @ A @ B) @ (suc @ C)) = (coindu749330388e_lnth @ TA @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 21.68/5.92 thf(88,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_70_infinite__descent0__measure)).
% 21.68/5.92 thf(512,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)],[88])).
% 21.68/5.92 thf(61,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less @ nat @ A @ B) => ((ord_less @ nat @ C @ D) => (ord_less @ nat @ (plus_plus @ nat @ A @ C) @ (plus_plus @ nat @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_add__less__mono)).
% 21.68/5.92 thf(439,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less @ nat @ A @ B) => ((ord_less @ nat @ C @ D) => (ord_less @ nat @ (plus_plus @ nat @ A @ C) @ (plus_plus @ nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 21.68/5.92 thf(198,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ (suc @ B)) = ((A = (zero_zero @ nat)) | ? [C:nat]: ((A = (suc @ C)) & (ord_less @ nat @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_less__Suc__eq__0__disj)).
% 21.68/5.92 thf(894,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ (suc @ B)) = ((A = (zero_zero @ nat)) | ? [C:nat]: ((A = (suc @ C)) & (ord_less @ nat @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 21.68/5.92 thf(252,axiom,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA),C:(coindu1593790203_llist @ TA)]: ((ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B)) => ((coindu749330388e_lnth @ TA @ (coindu268472904append @ TA @ B @ C) @ A) = (coindu749330388e_lnth @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_162_lnth__lappend1)).
% 21.68/5.92 thf(1091,plain,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA),C:(coindu1593790203_llist @ TA)]: ((ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B)) => ((coindu749330388e_lnth @ TA @ (coindu268472904append @ TA @ B @ C) @ A) = (coindu749330388e_lnth @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 21.68/5.92 thf(9,axiom,((! [TA: $tType]: ((cancel146912293up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ A @ (plus_plus @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_diff__diff__add)).
% 21.68/5.92 thf(302,plain,((! [TA: $tType]: ((cancel146912293up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ A @ (plus_plus @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 21.68/5.92 thf(28,axiom,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (((=) @ TA) = (^ [A:TA,B:TA]: ((minus_minus @ TA @ A @ B) = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_eq__iff__diff__eq__0)).
% 21.68/5.92 thf(349,plain,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (((=) @ TA) = (^ [A:TA,B:TA]: ((minus_minus @ TA @ A @ B) = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 21.68/5.92 thf(49,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_less__nat__zero__code)).
% 21.68/5.92 thf(407,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 21.68/5.92 thf(275,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) => (ord_less @ nat @ (minus_minus @ nat @ A @ (suc @ B)) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_diff__Suc__less)).
% 21.68/5.92 thf(1238,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) => (ord_less @ nat @ (minus_minus @ nat @ A @ (suc @ B)) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[275])).
% 21.68/5.92 thf(238,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) => (~ (! [B:nat]: (A != (suc @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_old_Onat_Oexhaust)).
% 21.68/5.92 thf(1042,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) => (~ (! [B:nat]: ~ (A = (suc @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 21.68/5.92 thf(216,axiom,((! [TA: $tType]: (! [A:extended_enat,B:(coindu1593790203_llist @ TA),C:(coindu1593790203_llist @ TA)]: (((ord_less @ extended_enat @ A @ (coindu1018505716length @ TA @ B)) => ((coindu191418589_ldrop @ TA @ A @ (coindu268472904append @ TA @ B @ C)) = (coindu268472904append @ TA @ (coindu191418589_ldrop @ TA @ A @ B) @ C))) & ((~ (ord_less @ extended_enat @ A @ (coindu1018505716length @ TA @ B))) => ((coindu191418589_ldrop @ TA @ A @ (coindu268472904append @ TA @ B @ C)) = (coindu191418589_ldrop @ TA @ (minus_minus @ extended_enat @ A @ (coindu1018505716length @ TA @ B)) @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_ldrop__lappend)).
% 21.68/5.92 thf(952,plain,((! [TA: $tType]: (! [A:extended_enat,B:(coindu1593790203_llist @ TA),C:(coindu1593790203_llist @ TA)]: (((ord_less @ extended_enat @ A @ (coindu1018505716length @ TA @ B)) => ((coindu191418589_ldrop @ TA @ A @ (coindu268472904append @ TA @ B @ C)) = (coindu268472904append @ TA @ (coindu191418589_ldrop @ TA @ A @ B) @ C))) & ((~ (ord_less @ extended_enat @ A @ (coindu1018505716length @ TA @ B))) => ((coindu191418589_ldrop @ TA @ A @ (coindu268472904append @ TA @ B @ C)) = (coindu191418589_ldrop @ TA @ (minus_minus @ extended_enat @ A @ (coindu1018505716length @ TA @ B)) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 21.68/5.92 thf(73,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_116_case__enat__0)).
% 21.68/5.92 thf(467,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)],[73])).
% 21.68/5.92 thf(79,axiom,((! [TA: $tType]: ((linord219039673up_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ A) @ (zero_zero @ TA)) = (ord_less @ TA @ A @ (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_double__add__less__zero__iff__single__add__less__zero)).
% 21.68/5.92 thf(484,plain,((! [TA: $tType]: ((linord219039673up_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ A) @ (zero_zero @ TA)) = (ord_less @ TA @ A @ (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 21.68/5.92 thf(32,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) = (ord_less @ nat @ (zero_zero @ nat) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_neq0__conv)).
% 21.68/5.92 thf(361,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) = (ord_less @ nat @ (zero_zero @ nat) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 21.68/5.92 thf(117,axiom,((! [TA: $tType]: ((ab_semigroup_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((plus_plus @ TA @ (plus_plus @ TA @ A @ B) @ C) = (plus_plus @ TA @ A @ (plus_plus @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_ab__semigroup__add__class_Oadd__ac_I1_J)).
% 21.68/5.92 thf(625,plain,((! [TA: $tType]: ((ab_semigroup_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((plus_plus @ TA @ (plus_plus @ TA @ A @ B) @ C) = (plus_plus @ TA @ A @ (plus_plus @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 21.68/5.92 thf(129,axiom,((ordere516151231imp_le @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oordered__ab__semigroup__monoid__add__imp__le)).
% 21.68/5.92 thf(665,plain,((ordere516151231imp_le @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 21.68/5.92 thf(82,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_less__not__refl2)).
% 21.68/5.92 thf(493,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 21.68/5.92 thf(233,axiom,((! [A:nat,B:nat]: ((minus_minus @ extended_enat @ (extended_enat2 @ A) @ (extended_enat2 @ B)) = (extended_enat2 @ (minus_minus @ nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_idiff__enat__enat)).
% 21.68/5.92 thf(1027,plain,((! [A:nat,B:nat]: ((minus_minus @ extended_enat @ (extended_enat2 @ A) @ (extended_enat2 @ B)) = (extended_enat2 @ (minus_minus @ nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 21.68/5.92 thf(162,axiom,((! [TA: $tType]: ((comm_monoid_diff @ TA @ (type2 @ TA)) => (! [A:TA]: ((minus_minus @ TA @ (zero_zero @ TA) @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_zero__diff)).
% 21.68/5.92 thf(757,plain,((! [TA: $tType]: ((comm_monoid_diff @ TA @ (type2 @ TA)) => (! [A:TA]: ((minus_minus @ TA @ (zero_zero @ TA) @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 21.68/5.92 thf(137,axiom,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (plus_plus @ nat @ A @ B) @ (plus_plus @ nat @ C @ B)) = (minus_minus @ nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_diff__cancel2)).
% 21.68/5.92 thf(682,plain,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (plus_plus @ nat @ A @ B) @ (plus_plus @ nat @ C @ B)) = (minus_minus @ nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 21.68/5.92 thf(222,axiom,((! [A:extended_enat]: ((A != (extend1396239628finity @ extended_enat)) = (? [B:nat]: (A = (extended_enat2 @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_not__infinity__eq)).
% 21.68/5.92 thf(974,plain,((! [A:extended_enat]: ((~ (A = (extend1396239628finity @ extended_enat))) = (? [B:nat]: (A = (extended_enat2 @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 21.68/5.92 thf(231,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_110_less__enatE)).
% 21.68/5.92 thf(1012,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)],[231])).
% 21.68/5.92 thf(21,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_less__not__refl3)).
% 21.68/5.92 thf(329,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 21.68/5.92 thf(273,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_154_enat3__cases)).
% 21.68/5.92 thf(1178,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)],[273])).
% 21.68/5.92 thf(102,axiom,((comm_monoid_add @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocomm__monoid__add)).
% 21.68/5.92 thf(583,plain,((comm_monoid_add @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 21.68/5.92 thf(89,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_65_infinite__descent0)).
% 21.68/5.92 thf(522,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)],[89])).
% 21.68/5.92 thf(94,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_68_measure__induct__rule)).
% 21.68/5.92 thf(551,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)],[94])).
% 21.68/5.92 thf(258,axiom,((! [A:nat]: ((extended_size_enat @ (extended_enat2 @ A)) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_enat_Osize_I1_J)).
% 21.68/5.92 thf(1128,plain,((! [A:nat]: ((extended_size_enat @ (extended_enat2 @ A)) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 21.68/5.92 thf(283,axiom,((! [A:nat]: ((suc @ A) != (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_Suc__neq__Zero)).
% 21.68/5.92 thf(1270,plain,((! [A:nat]: ~ ((suc @ A) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[283])).
% 21.68/5.92 thf(232,axiom,((! [A:(nat > $o)]: ((~ (A @ (zero_zero @ nat))) => ((? [B:nat]: (A @ B)) => (? [B:nat]: (~ (A @ B) & (A @ (suc @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_exists__least__lemma)).
% 21.68/5.92 thf(1017,plain,((! [A:(nat > $o)]: ((~ (A @ (zero_zero @ nat))) => ((? [B:nat]: (A @ B)) => (? [B:nat]: (~ (A @ B) & (A @ (suc @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 21.68/5.92 thf(152,axiom,((! [A:nat]: ((plus_plus @ nat @ (zero_zero @ nat) @ A) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_plus__nat_Oadd__0)).
% 21.68/5.92 thf(725,plain,((! [A:nat]: ((plus_plus @ nat @ (zero_zero @ nat) @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 21.68/5.92 thf(42,axiom,((! [TA: $tType]: ((comm_monoid_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((plus_plus @ TA @ (zero_zero @ TA) @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_comm__monoid__add__class_Oadd__0)).
% 21.68/5.92 thf(388,plain,((! [TA: $tType]: ((comm_monoid_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((plus_plus @ TA @ (zero_zero @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 21.68/5.92 thf(113,axiom,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ A @ (plus_plus @ TA @ B @ C)) = (minus_minus @ TA @ (minus_minus @ TA @ A @ C) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_diff__add__eq__diff__diff__swap)).
% 21.68/5.92 thf(610,plain,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ A @ (plus_plus @ TA @ B @ C)) = (minus_minus @ TA @ (minus_minus @ TA @ A @ C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 21.68/5.92 thf(172,axiom,((! [TA: $tType]: ((ordere516151231imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ B) @ B) = (ord_less @ TA @ A @ (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_add__less__same__cancel2)).
% 21.68/5.92 thf(783,plain,((! [TA: $tType]: ((ordere516151231imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ B) @ B) = (ord_less @ TA @ A @ (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 21.68/5.92 thf(225,axiom,((! [A:nat]: ((zero_zero @ nat) != (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_Zero__neq__Suc)).
% 21.68/5.92 thf(989,plain,((! [A:nat]: ~ ((zero_zero @ nat) = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 21.68/5.92 thf(156,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)).
% 21.68/5.92 thf(742,plain,((! [A:nat]: ((~ (ord_less @ nat @ (zero_zero @ nat) @ A)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 21.68/5.92 thf(100,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (plus_plus @ nat @ A @ B) @ C) => (ord_less @ nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_add__lessD1)).
% 21.68/5.92 thf(578,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (plus_plus @ nat @ A @ B) @ C) => (ord_less @ nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 21.68/5.92 thf(20,axiom,((ab_semigroup_add @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oab__semigroup__add)).
% 21.68/5.92 thf(328,plain,((ab_semigroup_add @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 21.68/5.92 thf(195,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_nat_Oinject)).
% 21.68/5.92 thf(884,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 21.68/5.92 thf(24,axiom,((order @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oorder_1)).
% 21.68/5.92 thf(339,plain,((order @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 21.68/5.92 thf(211,axiom,((! [A:nat,B:nat]: ((plus_plus @ nat @ A @ (suc @ B)) = (suc @ (plus_plus @ nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_add__Suc__right)).
% 21.68/5.92 thf(933,plain,((! [A:nat,B:nat]: ((plus_plus @ nat @ A @ (suc @ B)) = (suc @ (plus_plus @ nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 21.68/5.92 thf(131,axiom,((minus @ extended_enat @ (type2 @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Groups_Ominus_12)).
% 21.68/5.92 thf(669,plain,((minus @ extended_enat @ (type2 @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 21.68/5.92 thf(76,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ (minus_minus @ nat @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_less__imp__diff__less)).
% 21.68/5.92 thf(476,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ (minus_minus @ nat @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 21.68/5.92 thf(136,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_less__irrefl__nat)).
% 21.68/5.92 thf(679,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 21.68/5.92 thf(125,axiom,((! [TA: $tType]: ((ordere779506340up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: (((A = B) & (C = D)) => ((plus_plus @ TA @ A @ C) = (plus_plus @ TA @ B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_add__mono__thms__linordered__semiring_I4_J)).
% 21.68/5.92 thf(647,plain,((! [TA: $tType]: ((ordere779506340up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: (((A = B) & (C = D)) => ((plus_plus @ TA @ A @ C) = (plus_plus @ TA @ B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 21.68/5.92 thf(224,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_13_enat__iless)).
% 21.68/5.92 thf(985,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)],[224])).
% 21.68/5.92 thf(144,axiom,((! [TA: $tType]: ((strict2144017051up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ D) => (ord_less @ TA @ (plus_plus @ TA @ A @ C) @ (plus_plus @ TA @ B @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_add__strict__mono)).
% 21.68/5.92 thf(701,plain,((! [TA: $tType]: ((strict2144017051up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ D) => (ord_less @ TA @ (plus_plus @ TA @ A @ C) @ (plus_plus @ TA @ B @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 21.68/5.92 thf(264,axiom,((! [A:(coindu1593790203_llist @ a)]: ((ord_less @ extended_enat @ (extended_enat2 @ n_a) @ (coindu1018505716length @ a @ A)) => ((coindu2000965700_llast @ a @ (coindu191418589_ldrop @ a @ (extended_enat2 @ n_a) @ A)) = (coindu2000965700_llast @ a @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_Suc_Ohyps)).
% 21.68/5.92 thf(1150,plain,((! [A:(coindu1593790203_llist @ a)]: ((ord_less @ extended_enat @ (extended_enat2 @ n_a) @ (coindu1018505716length @ a @ A)) => ((coindu2000965700_llast @ a @ (coindu191418589_ldrop @ a @ (extended_enat2 @ n_a) @ A)) = (coindu2000965700_llast @ a @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 21.68/5.92 thf(204,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (((suc @ A) != B) => (ord_less @ nat @ (suc @ A) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_Suc__lessI)).
% 21.68/5.92 thf(911,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => ((~ ((suc @ A) = B)) => (ord_less @ nat @ (suc @ A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 21.68/5.92 thf(150,axiom,((monoid_add @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Omonoid__add)).
% 21.68/5.92 thf(721,plain,((monoid_add @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 21.68/5.92 thf(229,axiom,((! [TA: $tType]: (! [A:extended_enat,B:(coindu1593790203_llist @ TA)]: (((A = (extend1396239628finity @ extended_enat)) => ((coindu1018505716length @ TA @ (coindu191418589_ldrop @ TA @ A @ B)) = (zero_zero @ extended_enat))) & ((A != (extend1396239628finity @ extended_enat)) => ((coindu1018505716length @ TA @ (coindu191418589_ldrop @ TA @ A @ B)) = (minus_minus @ extended_enat @ (coindu1018505716length @ TA @ B) @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_llength__ldrop)).
% 21.68/5.92 thf(1002,plain,((! [TA: $tType]: (! [A:extended_enat,B:(coindu1593790203_llist @ TA)]: (((A = (extend1396239628finity @ extended_enat)) => ((coindu1018505716length @ TA @ (coindu191418589_ldrop @ TA @ A @ B)) = (zero_zero @ extended_enat))) & ((~ (A = (extend1396239628finity @ extended_enat))) => ((coindu1018505716length @ TA @ (coindu191418589_ldrop @ TA @ A @ B)) = (minus_minus @ extended_enat @ (coindu1018505716length @ TA @ B) @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 21.68/5.92 thf(36,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_gr__implies__not__zero)).
% 21.68/5.92 thf(371,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 21.68/5.92 thf(85,axiom,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((minus_minus @ TA @ A @ (zero_zero @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_diff__0__right)).
% 21.68/5.92 thf(503,plain,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((minus_minus @ TA @ A @ (zero_zero @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 21.68/5.92 thf(259,axiom,((! [A:nat]: ((suc @ A) != (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_old_Onat_Odistinct_I2_J)).
% 21.68/5.92 thf(1131,plain,((! [A:nat]: ~ ((suc @ A) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 21.68/5.92 thf(127,axiom,((! [TA: $tType]: ((ordere236663937imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ A @ C)) => (ord_less @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_add__less__imp__less__left)).
% 21.68/5.92 thf(654,plain,((! [TA: $tType]: ((ordere236663937imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ A @ C)) => (ord_less @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 21.68/5.92 thf(244,axiom,((! [A:nat,B:nat]: (ord_less @ nat @ (minus_minus @ nat @ A @ B) @ (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_164_diff__less__Suc)).
% 21.68/5.92 thf(1060,plain,((! [A:nat,B:nat]: (ord_less @ nat @ (minus_minus @ nat @ A @ B) @ (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 21.68/5.92 thf(69,axiom,((! [A:extended_enat]: ((A != (extend1396239628finity @ extended_enat)) => ((minus_minus @ extended_enat @ A @ A) = (zero_zero @ extended_enat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_idiff__self)).
% 21.68/5.92 thf(457,plain,((! [A:extended_enat]: ((~ (A = (extend1396239628finity @ extended_enat))) => ((minus_minus @ extended_enat @ A @ A) = (zero_zero @ extended_enat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 21.68/5.92 thf(175,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ D) => (ord_less @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_diff__strict__mono)).
% 21.68/5.92 thf(792,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ D) => (ord_less @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 21.68/5.92 thf(276,axiom,((ord_less @ extended_enat @ n @ (coindu1018505716length @ a @ xs))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_assms)).
% 21.68/5.93 thf(1241,plain,((ord_less @ extended_enat @ n @ (coindu1018505716length @ a @ xs))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[276])).
% 21.68/5.93 thf(12,axiom,((order @ $o @ (type2 @ $o))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder_3)).
% 21.68/5.93 thf(311,plain,((order @ $o @ (type2 @ $o))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 21.68/5.93 thf(134,axiom,((! [TA: $tType]: ((ordere223160158up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: (((ord_less @ TA @ A @ B) & (ord_less @ TA @ C @ D)) => (ord_less @ TA @ (plus_plus @ TA @ A @ C) @ (plus_plus @ TA @ B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_add__mono__thms__linordered__field_I5_J)).
% 21.68/5.93 thf(674,plain,((! [TA: $tType]: ((ordere223160158up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: (((ord_less @ TA @ A @ B) & (ord_less @ TA @ C @ D)) => (ord_less @ TA @ (plus_plus @ TA @ A @ C) @ (plus_plus @ TA @ B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 21.68/5.93 thf(176,axiom,((! [A:nat,B:nat,C:nat]: (((plus_plus @ nat @ A @ B) = (plus_plus @ nat @ A @ C)) = (B = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_nat__add__left__cancel)).
% 21.68/5.93 thf(794,plain,((! [A:nat,B:nat,C:nat]: (((plus_plus @ nat @ A @ B) = (plus_plus @ nat @ A @ C)) = (B = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 21.68/5.93 thf(149,axiom,((! [TA: $tType]: ((ordere516151231imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ (plus_plus @ TA @ B @ A)) = (ord_less @ TA @ (zero_zero @ TA) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_less__add__same__cancel2)).
% 21.68/5.93 thf(718,plain,((! [TA: $tType]: ((ordere516151231imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ (plus_plus @ TA @ B @ A)) = (ord_less @ TA @ (zero_zero @ TA) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 21.68/5.93 thf(46,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_139_enat_Osimps_I7_J)).
% 21.68/5.93 thf(398,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)],[46])).
% 21.68/5.93 thf(236,axiom,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (minus_minus @ nat @ (suc @ A) @ B) @ (suc @ C)) = (minus_minus @ nat @ (minus_minus @ nat @ A @ B) @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_Suc__diff__diff)).
% 21.68/5.93 thf(1035,plain,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (minus_minus @ nat @ (suc @ A) @ B) @ (suc @ C)) = (minus_minus @ nat @ (minus_minus @ nat @ A @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 21.68/5.93 thf(260,axiom,((! [A:nat]: ((extend1396239628finity @ extended_enat) != (extended_enat2 @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_enat_Odistinct_I2_J)).
% 21.68/5.93 thf(1135,plain,((! [A:nat]: ~ ((extend1396239628finity @ extended_enat) = (extended_enat2 @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 21.68/5.93 thf(56,axiom,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ A @ (minus_minus @ TA @ B @ C)) = (minus_minus @ TA @ (plus_plus @ TA @ A @ C) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_diff__diff__eq2)).
% 21.68/5.93 thf(425,plain,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ A @ (minus_minus @ TA @ B @ C)) = (minus_minus @ TA @ (plus_plus @ TA @ A @ C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 21.68/5.93 thf(157,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_66_linorder__neqE__nat)).
% 21.68/5.93 thf(745,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)],[157])).
% 21.68/5.93 thf(7,axiom,((! [A:nat]: ((minus_minus @ nat @ (zero_zero @ nat) @ A) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_diff__0__eq__0)).
% 21.68/5.93 thf(296,plain,((! [A:nat]: ((minus_minus @ nat @ (zero_zero @ nat) @ A) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 21.68/5.93 thf(37,axiom,((minus @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ominus_2)).
% 21.68/5.93 thf(375,plain,((minus @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 21.68/5.93 thf(103,axiom,((! [A:extended_enat]: ~ (ord_less @ extended_enat @ (extend1396239628finity @ extended_enat) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_enat__ord__simps_I6_J)).
% 21.68/5.93 thf(584,plain,((! [A:extended_enat]: ~ (ord_less @ extended_enat @ (extend1396239628finity @ extended_enat) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 21.68/5.93 thf(141,axiom,((ordere236663937imp_le @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oordered__ab__semigroup__add__imp__le)).
% 21.68/5.93 thf(694,plain,((ordere236663937imp_le @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 21.68/5.93 thf(167,axiom,((! [A:nat]: ((plus_plus @ nat @ A @ (zero_zero @ nat)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_Nat_Oadd__0__right)).
% 21.68/5.93 thf(772,plain,((! [A:nat]: ((plus_plus @ nat @ A @ (zero_zero @ nat)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 21.68/5.93 thf(3,axiom,((minus @ $o @ (type2 @ $o))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Groups_Ominus_4)).
% 21.68/5.93 thf(286,plain,((minus @ $o @ (type2 @ $o))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 21.68/5.93 thf(217,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_12_chain__incr)).
% 21.68/5.93 thf(958,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)],[217])).
% 21.68/5.93 thf(92,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_less__zeroE)).
% 21.68/5.93 thf(545,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 21.68/5.93 thf(51,axiom,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (minus_minus @ nat @ A @ B) @ C) = (minus_minus @ nat @ A @ (plus_plus @ nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_diff__diff__left)).
% 21.68/5.93 thf(413,plain,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (minus_minus @ nat @ A @ B) @ C) = (minus_minus @ nat @ A @ (plus_plus @ nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 21.68/5.93 thf(185,axiom,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA)]: ((coindu1018505716length @ TA @ (coindu531130065ldropn @ TA @ A @ B)) = (minus_minus @ extended_enat @ (coindu1018505716length @ TA @ B) @ (extended_enat2 @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_llength__ldropn)).
% 21.68/5.93 thf(826,plain,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA)]: ((coindu1018505716length @ TA @ (coindu531130065ldropn @ TA @ A @ B)) = (minus_minus @ extended_enat @ (coindu1018505716length @ TA @ B) @ (extended_enat2 @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 21.68/5.93 thf(147,axiom,((! [A:nat,B:nat]: ~ (ord_less @ nat @ (plus_plus @ nat @ A @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_not__add__less1)).
% 21.68/5.93 thf(711,plain,((! [A:nat,B:nat]: ~ (ord_less @ nat @ (plus_plus @ nat @ A @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 21.68/5.93 thf(123,axiom,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (plus_plus @ nat @ A @ B) @ (plus_plus @ nat @ A @ C)) = (minus_minus @ nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_Nat_Odiff__cancel)).
% 21.68/5.93 thf(641,plain,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (plus_plus @ nat @ A @ B) @ (plus_plus @ nat @ A @ C)) = (minus_minus @ nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 21.68/5.93 thf(212,axiom,((! [A:nat]: ((zero_zero @ nat) != (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_nat_Odistinct_I1_J)).
% 21.68/5.93 thf(936,plain,((! [A:nat]: ~ ((zero_zero @ nat) = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 21.68/5.93 thf(40,axiom,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((A = (plus_plus @ TA @ A @ B)) = (B = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_add__cancel__right__right)).
% 21.68/5.93 thf(382,plain,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((A = (plus_plus @ TA @ A @ B)) = (B = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 21.68/5.93 thf(98,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_137_enat_Osimps_I5_J)).
% 21.68/5.93 thf(572,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)],[98])).
% 21.68/5.93 thf(280,axiom,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA)]: ((coindu191418589_ldrop @ TA @ (extended_enat2 @ A) @ B) = (coindu531130065ldropn @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_ldrop__enat)).
% 21.68/5.93 thf(1258,plain,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA)]: ((coindu191418589_ldrop @ TA @ (extended_enat2 @ A) @ B) = (coindu531130065ldropn @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[280])).
% 21.68/5.93 thf(43,axiom,((! [A:extended_enat]: ((minus_minus @ extended_enat @ (extend1396239628finity @ extended_enat) @ A) = (extend1396239628finity @ extended_enat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_idiff__infinity)).
% 21.68/5.93 thf(391,plain,((! [A:extended_enat]: ((minus_minus @ extended_enat @ (extend1396239628finity @ extended_enat) @ A) = (extend1396239628finity @ extended_enat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 21.68/5.93 thf(261,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => ((B != (suc @ A)) => (~ (! [C:nat]: ((ord_less @ nat @ A @ C) => (B != (suc @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_lessE)).
% 21.68/5.93 thf(1139,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => ((~ (B = (suc @ A))) => (~ (! [C:nat]: ((ord_less @ nat @ A @ C) => (~ (B = (suc @ C)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 21.68/5.93 thf(200,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ B) => (ord_less @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_Suc__lessD)).
% 21.68/5.93 thf(900,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ B) => (ord_less @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 21.68/5.93 thf(54,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ A @ (plus_plus @ nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_trans__less__add2)).
% 21.68/5.93 thf(419,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ A @ (plus_plus @ nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 21.68/5.93 thf(227,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => ((suc @ (minus_minus @ nat @ B @ (suc @ A))) = (minus_minus @ nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_Suc__diff__Suc)).
% 21.68/5.93 thf(996,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => ((suc @ (minus_minus @ nat @ B @ (suc @ A))) = (minus_minus @ nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 21.68/5.93 thf(67,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: (((plus_plus @ TA @ A @ B) = (zero_zero @ TA)) = ((A = (zero_zero @ TA)) & (B = (zero_zero @ TA)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_add__eq__0__iff__both__eq__0)).
% 21.68/5.93 thf(451,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: (((plus_plus @ TA @ A @ B) = (zero_zero @ TA)) = ((A = (zero_zero @ TA)) & (B = (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 21.68/5.93 thf(16,axiom,((! [TA: $tType]: ((ab_group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((plus_plus @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (plus_plus @ TA @ A @ C) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_diff__add__eq)).
% 21.68/5.93 thf(318,plain,((! [TA: $tType]: ((ab_group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((plus_plus @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (plus_plus @ TA @ A @ C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 21.68/5.93 thf(87,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) = (A != (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_zero__less__iff__neq__zero)).
% 21.68/5.93 thf(509,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ A) = (~ (A = (zero_zero @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 21.68/5.93 thf(115,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) => (ord_less @ nat @ (zero_zero @ nat) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_gr0I)).
% 21.68/5.93 thf(616,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) => (ord_less @ nat @ (zero_zero @ nat) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 21.68/5.93 thf(108,axiom,((ordere223160158up_add @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oordered__cancel__ab__semigroup__add)).
% 21.68/5.93 thf(599,plain,((ordere223160158up_add @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 21.68/5.93 thf(190,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ (suc @ B)) => (ord_less @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_Suc__less__SucD)).
% 21.68/5.93 thf(863,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ (suc @ B)) => (ord_less @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 21.68/5.93 thf(272,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_11_enat_Osimps_I6_J)).
% 21.68/5.93 thf(1175,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)],[272])).
% 21.68/5.93 thf(197,axiom,((! [A:nat]: (A != (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_n__not__Suc__n)).
% 21.68/5.93 thf(890,plain,((! [A:nat]: ~ (A = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 21.68/5.93 thf(251,axiom,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ (suc @ D)) => (A @ D))) => (A @ (minus_minus @ nat @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_zero__induct__lemma)).
% 21.68/5.93 thf(1080,plain,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ (suc @ D)) => (A @ D))) => (A @ (minus_minus @ nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 21.68/5.93 thf(112,axiom,((strict2144017051up_add @ extended_enat @ (type2 @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Groups_Ostrict__ordered__ab__semigroup__add_5)).
% 21.68/5.93 thf(609,plain,((strict2144017051up_add @ extended_enat @ (type2 @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 21.68/5.93 thf(78,axiom,((strict2144017051up_add @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ostrict__ordered__ab__semigroup__add)).
% 21.68/5.93 thf(483,plain,((strict2144017051up_add @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 21.68/5.93 thf(166,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TB @ (type2 @ TB)) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_minus__apply)).
% 21.68/5.93 thf(769,plain,((! [TA: $tType,TB: $tType]: ((minus @ TB @ (type2 @ TB)) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 21.68/5.93 thf(27,axiom,((! [TA: $tType]: ((ordere223160158up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: (((A = B) & (ord_less @ TA @ C @ D)) => (ord_less @ TA @ (plus_plus @ TA @ A @ C) @ (plus_plus @ TA @ B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_add__mono__thms__linordered__field_I2_J)).
% 21.68/5.93 thf(345,plain,((! [TA: $tType]: ((ordere223160158up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: (((A = B) & (ord_less @ TA @ C @ D)) => (ord_less @ TA @ (plus_plus @ TA @ A @ C) @ (plus_plus @ TA @ B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 21.68/5.93 thf(189,axiom,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat]: (A @ D @ (zero_zero @ nat))) => ((! [D:nat]: (A @ (zero_zero @ nat) @ (suc @ D))) => ((! [D:nat,E:nat]: ((A @ D @ E) => (A @ (suc @ D) @ (suc @ E)))) => (A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_diff__induct)).
% 21.68/5.93 thf(858,plain,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat]: (A @ D @ (zero_zero @ nat))) => ((! [D:nat]: (A @ (zero_zero @ nat) @ (suc @ D))) => ((! [D:nat,E:nat]: ((A @ D @ E) => (A @ (suc @ D) @ (suc @ E)))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 21.68/5.93 thf(34,axiom,((ab_semigroup_add @ extended_enat @ (type2 @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Groups_Oab__semigroup__add_8)).
% 21.68/5.93 thf(367,plain,((ab_semigroup_add @ extended_enat @ (type2 @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 21.68/5.93 thf(138,axiom,((! [TA: $tType]: ((ordere236663937imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ C @ B)) = (ord_less @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_add__less__cancel__right)).
% 21.68/5.93 thf(685,plain,((! [TA: $tType]: ((ordere236663937imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ C @ B)) = (ord_less @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 21.68/5.93 thf(246,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_50_enat__ord__simps_I2_J)).
% 21.68/5.93 thf(1066,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)],[246])).
% 21.68/5.93 thf(170,axiom,((linordered_semidom @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Rings_Olinordered__semidom)).
% 21.68/5.93 thf(780,plain,((linordered_semidom @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 21.68/5.93 thf(44,axiom,((! [TA: $tType]: ((monoid_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((plus_plus @ TA @ (zero_zero @ TA) @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_add_Oleft__neutral)).
% 21.68/5.93 thf(394,plain,((! [TA: $tType]: ((monoid_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((plus_plus @ TA @ (zero_zero @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 21.68/5.93 thf(97,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_17_enat__less__induct)).
% 21.68/5.93 thf(563,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)],[97])).
% 21.68/5.93 thf(8,axiom,((! [TA: $tType]: ((neg_numeral @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((plus_plus @ TA @ (plus_plus @ TA @ A @ B) @ C) = (plus_plus @ TA @ A @ (plus_plus @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_is__num__normalize_I1_J)).
% 21.68/5.93 thf(299,plain,((! [TA: $tType]: ((neg_numeral @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((plus_plus @ TA @ (plus_plus @ TA @ A @ B) @ C) = (plus_plus @ TA @ A @ (plus_plus @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 21.68/5.93 thf(58,axiom,((! [TA: $tType]: ((ordere223160158up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (plus_plus @ TA @ A @ C) @ (plus_plus @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_add__strict__right__mono)).
% 21.68/5.93 thf(431,plain,((! [TA: $tType]: ((ordere223160158up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (plus_plus @ TA @ A @ C) @ (plus_plus @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 21.68/5.93 thf(208,axiom,((! [A:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) => (? [B:nat]: (A = (suc @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_gr0__implies__Suc)).
% 21.68/5.93 thf(922,plain,((! [A:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) => (? [B:nat]: (A = (suc @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 21.68/5.93 thf(142,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => ((ord_less @ nat @ A @ C) => (ord_less @ nat @ (minus_minus @ nat @ C @ B) @ (minus_minus @ nat @ C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_diff__less__mono2)).
% 21.68/5.93 thf(695,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => ((ord_less @ nat @ A @ C) => (ord_less @ nat @ (minus_minus @ nat @ C @ B) @ (minus_minus @ nat @ C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 21.68/5.93 thf(278,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ A @ (suc @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_less__SucI)).
% 21.68/5.93 thf(1245,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ A @ (suc @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 21.68/5.93 thf(75,axiom,((! [TA: $tType]: ((cancel146912293up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (minus_minus @ TA @ A @ C) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_diff__right__commute)).
% 21.68/5.93 thf(473,plain,((! [TA: $tType]: ((cancel146912293up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (minus_minus @ TA @ A @ C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 21.68/5.93 thf(151,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ (plus_plus @ 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_205_add__gr__0)).
% 21.68/5.93 thf(722,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ (plus_plus @ 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)],[151])).
% 21.68/5.93 thf(81,axiom,((! [TA: $tType]: ((linord219039673up_add @ TA @ (type2 @ TA)) => (! [A:TA]: (((zero_zero @ TA) = (plus_plus @ TA @ A @ A)) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_double__zero__sym)).
% 21.68/5.93 thf(490,plain,((! [TA: $tType]: ((linord219039673up_add @ TA @ (type2 @ TA)) => (! [A:TA]: (((zero_zero @ TA) = (plus_plus @ TA @ A @ A)) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 21.68/5.93 thf(269,axiom,((! [A:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) => ((suc @ (minus_minus @ nat @ A @ (suc @ (zero_zero @ nat)))) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_Suc__pred)).
% 21.68/5.93 thf(1166,plain,((! [A:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ A) => ((suc @ (minus_minus @ nat @ A @ (suc @ (zero_zero @ nat)))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 21.68/5.93 thf(93,axiom,((! [TA: $tType]: (! [A:TA,B:(coindu1593790203_llist @ TA),C:TA,D:(coindu1593790203_llist @ TA)]: (((coindu1121789889_LCons @ TA @ A @ B) = (coindu1121789889_LCons @ TA @ C @ D)) = ((A = C) & (B = D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_llist_Oinject)).
% 21.68/5.93 thf(548,plain,((! [TA: $tType]: (! [A:TA,B:(coindu1593790203_llist @ TA),C:TA,D:(coindu1593790203_llist @ TA)]: (((coindu1121789889_LCons @ TA @ A @ B) = (coindu1121789889_LCons @ TA @ C @ D)) = ((A = C) & (B = D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 21.68/5.93 thf(80,axiom,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: (((minus_minus @ TA @ A @ B) = C) = (A = (plus_plus @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_diff__eq__eq)).
% 21.68/5.93 thf(487,plain,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: (((minus_minus @ TA @ A @ B) = C) = (A = (plus_plus @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 21.68/5.93 thf(183,axiom,((! [A:(nat > $o),B:nat]: ((A @ (zero_zero @ nat)) => ((! [C:nat]: ((A @ C) => (A @ (suc @ C)))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_nat__induct)).
% 21.68/5.93 thf(812,plain,((! [A:(nat > $o),B:nat]: ((A @ (zero_zero @ nat)) => ((! [C:nat]: ((A @ C) => (A @ (suc @ C)))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 21.68/5.93 thf(159,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ (minus_minus @ nat @ B @ C)) = (ord_less @ nat @ (plus_plus @ nat @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_less__diff__conv)).
% 21.68/5.93 thf(749,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ (minus_minus @ nat @ B @ C)) = (ord_less @ nat @ (plus_plus @ nat @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 21.68/5.93 thf(26,axiom,((! [TA: $tType]: (! [A:(coindu1593790203_llist @ TA),B:(coindu1593790203_llist @ TA),C:(coindu1593790203_llist @ TA)]: ((coindu268472904append @ TA @ (coindu268472904append @ TA @ A @ B) @ C) = (coindu268472904append @ TA @ A @ (coindu268472904append @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_lappend__assoc)).
% 21.68/5.93 thf(342,plain,((! [TA: $tType]: (! [A:(coindu1593790203_llist @ TA),B:(coindu1593790203_llist @ TA),C:(coindu1593790203_llist @ TA)]: ((coindu268472904append @ TA @ (coindu268472904append @ TA @ A @ B) @ C) = (coindu268472904append @ TA @ A @ (coindu268472904append @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 21.68/5.93 thf(262,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ (suc @ A) @ (suc @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_Suc__mono)).
% 21.68/5.93 thf(1145,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ (suc @ A) @ (suc @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 21.68/5.93 thf(30,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((A != (zero_zero @ TA)) => (ord_less @ TA @ (zero_zero @ TA) @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_gr__zeroI)).
% 21.68/5.93 thf(355,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((~ (A = (zero_zero @ TA))) => (ord_less @ TA @ (zero_zero @ TA) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 21.68/5.93 thf(161,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((ord_less @ TA @ A @ B) = (ord_less @ TA @ C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_diff__eq__diff__less)).
% 21.68/5.93 thf(754,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((ord_less @ TA @ A @ B) = (ord_less @ TA @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 21.68/5.93 thf(184,axiom,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA),C:TA,D:(coindu1593790203_llist @ TA)]: (((coindu531130065ldropn @ TA @ A @ B) = (coindu1121789889_LCons @ TA @ C @ D)) => (ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_ldropn__eq__LConsD)).
% 21.68/5.93 thf(823,plain,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA),C:TA,D:(coindu1593790203_llist @ TA)]: (((coindu531130065ldropn @ TA @ A @ B) = (coindu1121789889_LCons @ TA @ C @ D)) => (ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 21.68/5.93 thf(240,axiom,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA)]: ((ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B)) => ((coindu1121789889_LCons @ TA @ (coindu749330388e_lnth @ TA @ B @ A) @ (coindu531130065ldropn @ TA @ (suc @ A) @ B)) = (coindu531130065ldropn @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_ldropn__Suc__conv__ldropn)).
% 21.68/5.93 thf(1049,plain,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA)]: ((ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B)) => ((coindu1121789889_LCons @ TA @ (coindu749330388e_lnth @ TA @ B @ A) @ (coindu531130065ldropn @ TA @ (suc @ A) @ B)) = (coindu531130065ldropn @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 21.68/5.93 thf(95,axiom,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((plus_plus @ TA @ (zero_zero @ TA) @ A) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_add_Ogroup__left__neutral)).
% 21.68/5.93 thf(557,plain,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((plus_plus @ TA @ (zero_zero @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 21.68/5.93 thf(101,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TB @ (type2 @ TB)) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_fun__diff__def)).
% 21.68/5.93 thf(580,plain,((! [TA: $tType,TB: $tType]: ((minus @ TB @ (type2 @ TB)) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 21.68/5.93 thf(6,axiom,((monoid_add @ extended_enat @ (type2 @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Groups_Omonoid__add_10)).
% 21.68/5.93 thf(295,plain,((monoid_add @ extended_enat @ (type2 @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 21.68/5.93 thf(266,axiom,((! [A:nat]: (ord_less @ nat @ (zero_zero @ nat) @ (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_zero__less__Suc)).
% 21.68/5.93 thf(1156,plain,((! [A:nat]: (ord_less @ nat @ (zero_zero @ nat) @ (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 21.68/5.93 thf(196,axiom,((! [TA: $tType]: ((order @ TA @ (type2 @ TA)) => (! [A:(nat > TA),B:nat,C:nat]: ((! [D:nat]: (ord_less @ TA @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less @ TA @ (A @ B) @ (A @ C)) = (ord_less @ nat @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_lift__Suc__mono__less__iff)).
% 21.68/5.93 thf(887,plain,((! [TA: $tType]: ((order @ TA @ (type2 @ TA)) => (! [A:(nat > TA),B:nat,C:nat]: ((! [D:nat]: (ord_less @ TA @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less @ TA @ (A @ B) @ (A @ C)) = (ord_less @ nat @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 21.68/5.93 thf(221,axiom,((! [A:nat]: ~ (ord_less @ extended_enat @ (extend1396239628finity @ extended_enat) @ (extended_enat2 @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_infinity__ilessE)).
% 21.68/5.93 thf(971,plain,((! [A:nat]: ~ (ord_less @ extended_enat @ (extend1396239628finity @ extended_enat) @ (extended_enat2 @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 21.68/5.93 thf(155,axiom,((! [TA: $tType]: ((cancel_semigroup_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: (((plus_plus @ TA @ A @ B) = (plus_plus @ TA @ A @ C)) = (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_add__left__cancel)).
% 21.68/5.93 thf(739,plain,((! [TA: $tType]: ((cancel_semigroup_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: (((plus_plus @ TA @ A @ B) = (plus_plus @ TA @ A @ C)) = (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 21.68/5.93 thf(282,axiom,((! [A:extended_enat]: ((minus_minus @ extended_enat @ A @ (extended_enat2 @ (zero_zero @ nat))) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_idiff__enat__0__right)).
% 21.68/5.93 thf(1267,plain,((! [A:extended_enat]: ((minus_minus @ extended_enat @ A @ (extended_enat2 @ (zero_zero @ nat))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 21.68/5.93 thf(226,axiom,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) => ((ord_less @ nat @ A @ (suc @ B)) => (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_less__antisym)).
% 21.68/5.93 thf(993,plain,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) => ((ord_less @ nat @ A @ (suc @ B)) => (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 21.68/5.93 thf(133,axiom,((ordere779506340up_add @ extended_enat @ (type2 @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Groups_Oordered__ab__semigroup__add_7)).
% 21.68/5.93 thf(673,plain,((ordere779506340up_add @ extended_enat @ (type2 @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 21.68/5.93 thf(237,axiom,((! [A:nat]: ((zero_zero @ nat) != (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_Zero__not__Suc)).
% 21.68/5.93 thf(1038,plain,((! [A:nat]: ~ ((zero_zero @ nat) = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 21.68/5.93 thf(274,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ (suc @ B)) = ((ord_less @ nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_less__Suc__eq)).
% 21.68/5.93 thf(1235,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ (suc @ B)) = ((ord_less @ nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 21.68/5.93 thf(71,axiom,((zero @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ozero)).
% 21.68/5.93 thf(463,plain,((zero @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 21.68/5.93 thf(74,axiom,((! [TA: $tType]: (! [A:nat,B:nat,C:(coindu1593790203_llist @ TA)]: ((coindu531130065ldropn @ TA @ A @ (coindu531130065ldropn @ TA @ B @ C)) = (coindu531130065ldropn @ TA @ (plus_plus @ nat @ A @ B) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_ldropn__ldropn)).
% 21.68/5.93 thf(470,plain,((! [TA: $tType]: (! [A:nat,B:nat,C:(coindu1593790203_llist @ TA)]: ((coindu531130065ldropn @ TA @ A @ (coindu531130065ldropn @ TA @ B @ C)) = (coindu531130065ldropn @ TA @ (plus_plus @ nat @ A @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 21.68/5.93 thf(181,axiom,((canoni770627133id_add @ extended_enat @ (type2 @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Groups_Ocanonically__ordered__monoid__add_6)).
% 21.68/5.93 thf(808,plain,((canoni770627133id_add @ extended_enat @ (type2 @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 21.68/5.93 thf(23,axiom,((! [TA: $tType]: ((cancel146912293up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ B) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_add__diff__cancel__right_H)).
% 21.68/5.93 thf(336,plain,((! [TA: $tType]: ((cancel146912293up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ B) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 21.68/5.93 thf(145,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_60_measure__induct)).
% 21.68/5.93 thf(703,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)],[145])).
% 21.68/5.93 thf(128,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_63_nat__less__induct)).
% 21.68/5.93 thf(656,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)],[128])).
% 21.68/5.93 thf(114,axiom,((! [A:extended_enat]: ((minus_minus @ extended_enat @ A @ (zero_zero @ extended_enat)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_idiff__0__right)).
% 21.68/5.93 thf(613,plain,((! [A:extended_enat]: ((minus_minus @ extended_enat @ A @ (zero_zero @ extended_enat)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 21.68/5.93 thf(109,axiom,((! [TA: $tType]: ((ordere516151231imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ (plus_plus @ TA @ A @ B)) = (ord_less @ TA @ (zero_zero @ TA) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_less__add__same__cancel1)).
% 21.68/5.93 thf(600,plain,((! [TA: $tType]: ((ordere516151231imp_le @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ (plus_plus @ TA @ A @ B)) = (ord_less @ TA @ (zero_zero @ TA) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 21.68/5.93 thf(241,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => ((ord_less @ nat @ B @ C) => (ord_less @ nat @ (suc @ A) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_less__trans__Suc)).
% 21.68/5.93 thf(1052,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => ((ord_less @ nat @ B @ C) => (ord_less @ nat @ (suc @ A) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 21.68/5.93 thf(253,axiom,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) = (ord_less @ nat @ B @ (suc @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_not__less__eq)).
% 21.68/5.93 thf(1094,plain,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) = (ord_less @ nat @ B @ (suc @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 21.68/5.93 thf(64,axiom,((! [TA: $tType]: (! [A:(coindu1593790203_llist @ TA),B:(coindu1593790203_llist @ TA)]: ((coindu574146665prefix @ TA @ A @ B) => (ord_less @ extended_enat @ (coindu1018505716length @ TA @ A) @ (coindu1018505716length @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_lstrict__prefix__llength__less)).
% 21.68/5.93 thf(446,plain,((! [TA: $tType]: (! [A:(coindu1593790203_llist @ TA),B:(coindu1593790203_llist @ TA)]: ((coindu574146665prefix @ TA @ A @ B) => (ord_less @ extended_enat @ (coindu1018505716length @ TA @ A) @ (coindu1018505716length @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 21.68/5.93 thf(83,axiom,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (minus_minus @ nat @ A @ B) @ C) = (minus_minus @ nat @ (minus_minus @ nat @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_diff__commute)).
% 21.68/5.93 thf(497,plain,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (minus_minus @ nat @ A @ B) @ C) = (minus_minus @ nat @ (minus_minus @ nat @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 21.68/5.93 thf(139,axiom,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((~ (ord_less @ TA @ (zero_zero @ TA) @ A)) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_not__gr__zero)).
% 21.68/5.93 thf(688,plain,((! [TA: $tType]: ((canoni770627133id_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((~ (ord_less @ TA @ (zero_zero @ TA) @ A)) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 21.68/5.93 thf(35,axiom,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((minus_minus @ TA @ A @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_cancel__comm__monoid__add__class_Odiff__cancel)).
% 21.68/5.93 thf(368,plain,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((minus_minus @ TA @ A @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 21.68/5.93 thf(257,axiom,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less @ nat @ A @ B) => ((! [D:nat]: ((B = (suc @ D)) => (C @ D))) => ((! [D:nat]: ((ord_less @ nat @ D @ B) => ((C @ (suc @ D)) => (C @ D)))) => (C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_strict__inc__induct)).
% 21.68/5.93 thf(1108,plain,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less @ nat @ A @ B) => ((! [D:nat]: ((B = (suc @ D)) => (C @ D))) => ((! [D:nat]: ((ord_less @ nat @ D @ B) => ((C @ (suc @ D)) => (C @ D)))) => (C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 21.68/5.93 thf(210,axiom,((n = (extended_enat2 @ n2))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_n)).
% 21.68/5.93 thf(931,plain,((n = (extended_enat2 @ n2))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 21.68/5.93 thf(90,axiom,((! [TA: $tType]: (! [A:TA,B:(coindu1593790203_llist @ TA),C:(coindu1593790203_llist @ TA)]: ((coindu268472904append @ TA @ (coindu1121789889_LCons @ TA @ A @ B) @ C) = (coindu1121789889_LCons @ TA @ A @ (coindu268472904append @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_lappend__code_I2_J)).
% 21.68/5.93 thf(539,plain,((! [TA: $tType]: (! [A:TA,B:(coindu1593790203_llist @ TA),C:(coindu1593790203_llist @ TA)]: ((coindu268472904append @ TA @ (coindu1121789889_LCons @ TA @ A @ B) @ C) = (coindu1121789889_LCons @ TA @ A @ (coindu268472904append @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 21.68/5.93 thf(219,axiom,((! [A:nat]: ((extended_enat2 @ A) != (extend1396239628finity @ extended_enat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_enat_Odistinct_I1_J)).
% 21.68/5.93 thf(963,plain,((! [A:nat]: ~ ((extended_enat2 @ A) = (extend1396239628finity @ extended_enat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 21.68/5.93 thf(158,axiom,((order @ extended_enat @ (type2 @ extended_enat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Extended__Nat_Oenat___Orderings_Oorder_11)).
% 21.68/5.93 thf(748,plain,((order @ extended_enat @ (type2 @ extended_enat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 21.68/5.93 thf(245,axiom,((! [A:extended_enat]: ((! [B:nat]: (A != (extended_enat2 @ B))) => (A = (extend1396239628finity @ extended_enat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_enat_Oexhaust)).
% 21.68/5.93 thf(1062,plain,((! [A:extended_enat]: ((! [B:nat]: ~ (A = (extended_enat2 @ B))) => (A = (extend1396239628finity @ extended_enat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 21.68/5.93 thf(120,axiom,((! [A:nat]: ((minus_minus @ nat @ A @ (zero_zero @ nat)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_minus__nat_Odiff__0)).
% 21.68/5.93 thf(632,plain,((! [A:nat]: ((minus_minus @ nat @ A @ (zero_zero @ nat)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 21.68/5.93 thf(47,axiom,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: (((plus_plus @ TA @ A @ B) = B) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_add__cancel__left__left)).
% 21.68/5.93 thf(401,plain,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: (((plus_plus @ TA @ A @ B) = B) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 21.68/5.93 thf(171,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_diff__strict__right__mono)).
% 21.68/5.93 thf(781,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 21.68/5.93 thf(53,axiom,((cancel_semigroup_add @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocancel__semigroup__add)).
% 21.68/5.93 thf(418,plain,((cancel_semigroup_add @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 21.68/5.93 thf(173,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (minus_minus @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_diff__gt__0__iff__gt)).
% 21.68/5.93 thf(786,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((ord_less @ TA @ (zero_zero @ TA) @ (minus_minus @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 21.68/5.93 thf(234,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_28_enat_Osimps_I4_J)).
% 21.68/5.93 thf(1030,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)],[234])).
% 21.68/5.93 thf(205,axiom,((! [A:nat]: ((A != (zero_zero @ nat)) => (? [B:nat]: (A = (suc @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_not0__implies__Suc)).
% 21.68/5.93 thf(914,plain,((! [A:nat]: ((~ (A = (zero_zero @ nat))) => (? [B:nat]: (A = (suc @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 21.68/5.93 thf(59,axiom,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) => ((plus_plus @ nat @ B @ (minus_minus @ nat @ A @ B)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_add__diff__inverse__nat)).
% 21.68/5.93 thf(433,plain,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) => ((plus_plus @ nat @ B @ (minus_minus @ nat @ A @ B)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 21.68/5.93 thf(250,axiom,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) => ((ord_less @ nat @ A @ (suc @ B)) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_not__less__less__Suc__eq)).
% 21.68/5.93 thf(1077,plain,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) => ((ord_less @ nat @ A @ (suc @ B)) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 21.68/5.93 thf(164,axiom,((! [TA: $tType]: ((cancel146912293up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ A @ C)) = (minus_minus @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_add__diff__cancel__left)).
% 21.68/5.93 thf(763,plain,((! [TA: $tType]: ((cancel146912293up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ A @ C)) = (minus_minus @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 21.68/5.93 thf(178,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA @ (type2 @ TA)) => ((ord_less @ TA) = (^ [A:TA,B:TA]: (ord_less @ TA @ (minus_minus @ TA @ A @ B) @ (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_less__iff__diff__less__0)).
% 21.68/5.93 thf(800,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA @ (type2 @ TA)) => ((ord_less @ TA) = (^ [A:TA,B:TA]: (ord_less @ TA @ (minus_minus @ TA @ A @ B) @ (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 21.68/5.93 thf(4,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TA @ (type2 @ TA)) => (minus @ (TB > TA) @ (type2 @ (TB > TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Groups_Ominus)).
% 21.68/5.93 thf(287,plain,((! [TA: $tType,TB: $tType]: ((minus @ TA @ (type2 @ TA)) => (minus @ (TB > TA) @ (type2 @ (TB > TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 21.68/5.93 thf(228,axiom,((! [A:extended_enat]: ((! [B:nat]: (A != (extended_enat2 @ B))) = (A = (extend1396239628finity @ extended_enat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_not__enat__eq)).
% 21.68/5.93 thf(999,plain,((! [A:extended_enat]: ((! [B:nat]: ~ (A = (extended_enat2 @ B))) = (A = (extend1396239628finity @ extended_enat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 21.68/5.93 thf(160,axiom,((! [TA: $tType]: ((linordered_semidom @ TA @ (type2 @ TA)) => (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_less__numeral__extra_I3_J)).
% 21.68/5.93 thf(752,plain,((! [TA: $tType]: ((linordered_semidom @ TA @ (type2 @ TA)) => (~ (ord_less @ TA @ (zero_zero @ TA) @ (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 21.68/5.93 thf(14,axiom,((ordere779506340up_add @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oordered__ab__semigroup__add)).
% 21.68/5.93 thf(315,plain,((ordere779506340up_add @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 21.68/5.93 thf(55,axiom,((! [TA: $tType]: ((comm_monoid_diff @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((minus_minus @ TA @ A @ (plus_plus @ TA @ A @ B)) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_diff__add__zero)).
% 21.68/5.93 thf(422,plain,((! [TA: $tType]: ((comm_monoid_diff @ TA @ (type2 @ TA)) => (! [A:TA,B:TA]: ((minus_minus @ TA @ A @ (plus_plus @ TA @ A @ B)) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 21.68/5.93 thf(192,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ (suc @ B)) => ((~ (ord_less @ nat @ A @ B)) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_less__SucE)).
% 21.68/5.93 thf(867,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ (suc @ B)) => ((~ (ord_less @ nat @ A @ B)) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 21.68/5.93 thf(191,axiom,((! [A:nat]: (ord_less @ nat @ A @ (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_lessI)).
% 21.68/5.93 thf(865,plain,((! [A:nat]: (ord_less @ nat @ A @ (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 21.68/5.93 thf(110,axiom,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((minus_minus @ TA @ A @ A) = (zero_zero @ TA)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_diff__self)).
% 21.68/5.93 thf(603,plain,((! [TA: $tType]: ((group_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((minus_minus @ TA @ A @ A) = (zero_zero @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 21.68/5.93 thf(50,axiom,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((minus_minus @ TA @ A @ (zero_zero @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_diff__zero)).
% 21.68/5.93 thf(410,plain,((! [TA: $tType]: ((cancel1352612707id_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((minus_minus @ TA @ A @ (zero_zero @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 21.68/5.93 thf(220,axiom,((! [A:nat]: ((zero_zero @ nat) != (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_old_Onat_Odistinct_I1_J)).
% 21.68/5.93 thf(967,plain,((! [A:nat]: ~ ((zero_zero @ nat) = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 21.68/5.93 thf(215,axiom,((! [A:nat]: (ord_less @ extended_enat @ (extended_enat2 @ A) @ (extend1396239628finity @ extended_enat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_enat__ord__code_I4_J)).
% 21.68/5.93 thf(950,plain,((! [A:nat]: (ord_less @ extended_enat @ (extended_enat2 @ A) @ (extend1396239628finity @ extended_enat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 21.68/5.93 thf(254,axiom,((! [A:nat]: (((extended_enat2 @ A) = (zero_zero @ extended_enat)) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_enat__0__iff_I1_J)).
% 21.68/5.93 thf(1097,plain,((! [A:nat]: (((extended_enat2 @ A) = (zero_zero @ extended_enat)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 21.68/5.93 thf(187,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ (suc @ B)) = (ord_less @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_Suc__less__eq)).
% 21.68/5.93 thf(835,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ (suc @ B)) = (ord_less @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 21.68/5.93 thf(10,axiom,((! [A:nat,B:nat,C:nat]: (((plus_plus @ nat @ A @ B) = (plus_plus @ nat @ C @ B)) = (A = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_nat__add__right__cancel)).
% 21.68/5.93 thf(305,plain,((! [A:nat,B:nat,C:nat]: (((plus_plus @ nat @ A @ B) = (plus_plus @ nat @ C @ B)) = (A = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 21.68/5.93 thf(86,axiom,((! [TA: $tType]: ((comm_monoid_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((plus_plus @ TA @ A @ (zero_zero @ TA)) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_add_Ocomm__neutral)).
% 21.68/5.93 thf(506,plain,((! [TA: $tType]: ((comm_monoid_add @ TA @ (type2 @ TA)) => (! [A:TA]: ((plus_plus @ TA @ A @ (zero_zero @ TA)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 21.68/5.93 thf(31,axiom,((! [TA: $tType]: ((cancel_semigroup_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: (((plus_plus @ TA @ A @ B) = (plus_plus @ TA @ C @ B)) = (A = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_add__right__cancel)).
% 21.68/5.93 thf(358,plain,((! [TA: $tType]: ((cancel_semigroup_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: (((plus_plus @ TA @ A @ B) = (plus_plus @ TA @ C @ B)) = (A = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 21.68/5.93 thf(243,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_167_less__infinityE)).
% 21.68/5.93 thf(1056,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)],[243])).
% 21.68/5.93 thf(235,axiom,((! [TA: $tType]: ((order @ TA @ (type2 @ TA)) => (! [A:(nat > TA),B:nat,C:nat]: ((! [D:nat]: (ord_less @ TA @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less @ nat @ B @ C) => (ord_less @ TA @ (A @ B) @ (A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_lift__Suc__mono__less)).
% 21.68/5.93 thf(1033,plain,((! [TA: $tType]: ((order @ TA @ (type2 @ TA)) => (! [A:(nat > TA),B:nat,C:nat]: ((! [D:nat]: (ord_less @ TA @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less @ nat @ B @ C) => (ord_less @ TA @ (A @ B) @ (A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 21.68/5.93 thf(271,axiom,((! [TA: $tType]: (! [A:extended_enat,B:(coindu1593790203_llist @ TA),C:TA,D:(coindu1593790203_llist @ TA)]: (((coindu191418589_ldrop @ TA @ A @ B) = (coindu1121789889_LCons @ TA @ C @ D)) => (ord_less @ extended_enat @ A @ (coindu1018505716length @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_ldrop__eq__LConsD)).
% 21.68/5.93 thf(1172,plain,((! [TA: $tType]: (! [A:extended_enat,B:(coindu1593790203_llist @ TA),C:TA,D:(coindu1593790203_llist @ TA)]: (((coindu191418589_ldrop @ TA @ A @ B) = (coindu1121789889_LCons @ TA @ C @ D)) => (ord_less @ extended_enat @ A @ (coindu1018505716length @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 21.68/5.93 thf(199,axiom,((! [A:nat,B:nat]: ((plus_plus @ nat @ (suc @ A) @ B) = (plus_plus @ nat @ A @ (suc @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_add__Suc__shift)).
% 21.68/5.93 thf(897,plain,((! [A:nat,B:nat]: ((plus_plus @ nat @ (suc @ A) @ B) = (plus_plus @ nat @ A @ (suc @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 21.68/5.93 thf(218,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_old_Onat_Oinject)).
% 21.68/5.93 thf(960,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 21.68/5.93 thf(121,axiom,((! [A:nat,B:nat]: ((minus_minus @ nat @ (plus_plus @ nat @ A @ B) @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_diff__add__inverse2)).
% 21.68/5.93 thf(635,plain,((! [A:nat,B:nat]: ((minus_minus @ nat @ (plus_plus @ nat @ A @ B) @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 21.68/5.93 thf(153,axiom,(((extended_the_enat @ (zero_zero @ extended_enat)) = (zero_zero @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_the__enat__0)).
% 21.68/5.93 thf(728,plain,(((extended_the_enat @ (zero_zero @ extended_enat)) = (zero_zero @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 21.68/5.93 thf(72,axiom,((! [TA: $tType]: ((cancel146912293up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ C @ B)) = (minus_minus @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_add__diff__cancel__right)).
% 21.68/5.93 thf(464,plain,((! [TA: $tType]: ((cancel146912293up_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ C @ B)) = (minus_minus @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 21.68/5.93 thf(281,axiom,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA),C:(coindu1593790203_llist @ TA)]: (((ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B)) => ((coindu531130065ldropn @ TA @ A @ (coindu268472904append @ TA @ B @ C)) = (coindu268472904append @ TA @ (coindu531130065ldropn @ TA @ A @ B) @ C))) & ((~ (ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B))) => ((coindu531130065ldropn @ TA @ A @ (coindu268472904append @ TA @ B @ C)) = (coindu531130065ldropn @ TA @ (minus_minus @ nat @ A @ (extended_the_enat @ (coindu1018505716length @ TA @ B))) @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_ldropn__lappend)).
% 21.68/5.93 thf(1261,plain,((! [TA: $tType]: (! [A:nat,B:(coindu1593790203_llist @ TA),C:(coindu1593790203_llist @ TA)]: (((ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B)) => ((coindu531130065ldropn @ TA @ A @ (coindu268472904append @ TA @ B @ C)) = (coindu268472904append @ TA @ (coindu531130065ldropn @ TA @ A @ B) @ C))) & ((~ (ord_less @ extended_enat @ (extended_enat2 @ A) @ (coindu1018505716length @ TA @ B))) => ((coindu531130065ldropn @ TA @ A @ (coindu268472904append @ TA @ B @ C)) = (coindu531130065ldropn @ TA @ (minus_minus @ nat @ A @ (extended_the_enat @ (coindu1018505716length @ TA @ B))) @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[281])).
% 21.68/5.93 thf(99,axiom,((! [A:nat,B:nat]: (((plus_plus @ nat @ A @ B) = A) => (B = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_add__eq__self__zero)).
% 21.68/5.93 thf(575,plain,((! [A:nat,B:nat]: (((plus_plus @ nat @ A @ B) = A) => (B = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 21.68/5.93 thf(107,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ (plus_plus @ nat @ A @ C) @ (plus_plus @ nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_add__less__mono1)).
% 21.68/5.93 thf(596,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ (plus_plus @ nat @ A @ C) @ (plus_plus @ nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 21.68/5.93 thf(124,axiom,((! [TA: $tType]: (! [A:TA,B:(coindu1593790203_llist @ TA),C:TA,D:(coindu1593790203_llist @ TA)]: ((coindu574146665prefix @ TA @ (coindu1121789889_LCons @ TA @ A @ B) @ (coindu1121789889_LCons @ TA @ C @ D)) = ((A = C) & (coindu574146665prefix @ TA @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_lstrict__prefix__code_I4_J)).
% 21.68/5.93 thf(644,plain,((! [TA: $tType]: (! [A:TA,B:(coindu1593790203_llist @ TA),C:TA,D:(coindu1593790203_llist @ TA)]: ((coindu574146665prefix @ TA @ (coindu1121789889_LCons @ TA @ A @ B) @ (coindu1121789889_LCons @ TA @ C @ D)) = ((A = C) & (coindu574146665prefix @ TA @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 21.68/5.93 thf(203,axiom,((! [TA: $tType]: (! [A:nat,B:TA,C:(coindu1593790203_llist @ TA)]: ((coindu531130065ldropn @ TA @ (suc @ A) @ (coindu1121789889_LCons @ TA @ B @ C)) = (coindu531130065ldropn @ TA @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_ldropn__Suc__LCons)).
% 21.68/5.93 thf(908,plain,((! [TA: $tType]: (! [A:nat,B:TA,C:(coindu1593790203_llist @ TA)]: ((coindu531130065ldropn @ TA @ (suc @ A) @ (coindu1121789889_LCons @ TA @ B @ C)) = (coindu531130065ldropn @ TA @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 21.68/5.93 thf(140,axiom,((! [A:nat,B:nat]: ~ (ord_less @ nat @ (plus_plus @ nat @ A @ B) @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_not__add__less2)).
% 21.68/5.93 thf(691,plain,((! [A:nat,B:nat]: ~ (ord_less @ nat @ (plus_plus @ nat @ A @ B) @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 21.68/5.93 thf(62,axiom,((cancel1352612707id_add @ nat @ (type2 @ nat))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocancel__comm__monoid__add)).
% 21.68/5.93 thf(442,plain,((cancel1352612707id_add @ nat @ (type2 @ nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 21.68/5.93 thf(18,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ (minus_minus @ nat @ A @ B)) = (ord_less @ nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_zero__less__diff)).
% 21.68/5.93 thf(322,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (zero_zero @ nat) @ (minus_minus @ nat @ A @ B)) = (ord_less @ nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 21.68/5.93 thf(179,axiom,((! [A:extended_enat]: ~ (ord_less @ extended_enat @ A @ (zero_zero @ extended_enat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_not__iless0)).
% 21.68/5.93 thf(803,plain,((! [A:extended_enat]: ~ (ord_less @ extended_enat @ A @ (zero_zero @ extended_enat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 21.68/5.93 thf(213,axiom,((! [A:nat,B:nat]: ((A = (suc @ B)) => (A != (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_nat_OdiscI)).
% 21.68/5.93 thf(940,plain,((! [A:nat,B:nat]: ((A = (suc @ B)) => (~ (A = (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 21.68/5.93 thf(230,axiom,((! [A:nat]: (((zero_zero @ extended_enat) = (extended_enat2 @ A)) = (A = (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_enat__0__iff_I2_J)).
% 21.68/5.93 thf(1009,plain,((! [A:nat]: (((zero_zero @ extended_enat) = (extended_enat2 @ A)) = (A = (zero_zero @ nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 21.68/5.93 thf(135,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (plus_plus @ nat @ A @ B) @ (plus_plus @ nat @ A @ C)) = (ord_less @ nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_nat__add__left__cancel__less)).
% 21.68/5.93 thf(676,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (plus_plus @ nat @ A @ B) @ (plus_plus @ nat @ A @ C)) = (ord_less @ nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 21.68/5.93 thf(106,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (B != (zero_zero @ nat))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_gr__implies__not0)).
% 21.68/5.93 thf(592,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (B = (zero_zero @ nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 21.68/5.93 thf(33,axiom,((! [TA: $tType]: ((zero @ TA @ (type2 @ TA)) => (! [A:TA]: (((zero_zero @ TA) = A) = (A = (zero_zero @ TA))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_zero__reorient)).
% 21.68/5.93 thf(364,plain,((! [TA: $tType]: ((zero @ TA @ (type2 @ TA)) => (! [A:TA]: (((zero_zero @ TA) = A) = (A = (zero_zero @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 21.68/5.93 thf(168,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_diff__strict__left__mono)).
% 21.68/5.93 thf(775,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA @ (type2 @ TA)) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 21.68/5.93 thf(96,axiom,((! [A:nat,B:nat]: ((minus_minus @ nat @ A @ (plus_plus @ nat @ A @ B)) = (zero_zero @ nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_diff__add__0)).
% 21.68/5.93 thf(560,plain,((! [A:nat,B:nat]: ((minus_minus @ nat @ A @ (plus_plus @ nat @ A @ B)) = (zero_zero @ nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 21.68/5.93 thf(68,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_15_i0__less)).
% 21.68/5.93 thf(454,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)],[68])).
% 21.68/5.93 thf(247,axiom,((! [A:nat]: ((minus_minus @ extended_enat @ (extended_enat2 @ A) @ (extend1396239628finity @ extended_enat)) = (zero_zero @ extended_enat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_idiff__infinity__right)).
% 21.68/5.93 thf(1069,plain,((! [A:nat]: ((minus_minus @ extended_enat @ (extended_enat2 @ A) @ (extend1396239628finity @ extended_enat)) = (zero_zero @ extended_enat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 21.68/5.93 thf(1513,plain,(($false)),inference(e,[status(thm)],[809,629,760,777,666,352,479,1105,333,628,977,1158,730,308,449,379,385,500,797,698,945,340,670,709,1046,436,651,829,404,1055,917,587,619,838,542,460,902,638,1147,1247,870,606,284,325,289,448,316,1100,881,416,789,591,443,321,376,806,905,766,1072,428,1242,312,1169,397,1074,920,925,1153,714,1163,512,439,894,1091,302,349,407,1238,1042,952,467,484,361,625,665,493,1027,757,682,974,1012,329,1178,583,522,551,1128,1270,1017,725,388,610,783,989,742,578,328,884,339,933,669,476,679,647,985,701,1150,911,721,1002,371,503,1131,654,1060,457,792,1241,311,674,794,718,398,1035,1135,425,745,296,375,584,694,772,286,958,545,413,826,711,641,936,382,572,1258,391,1139,900,419,996,451,318,509,616,599,863,1175,890,1080,609,483,769,345,858,367,685,1066,780,394,563,299,431,922,695,1245,473,722,490,1166,548,487,812,749,342,1145,355,754,823,1049,557,580,295,1156,887,971,739,1267,993,673,1038,1235,463,470,808,336,703,656,613,600,1052,1094,446,497,688,368,1108,931,539,963,748,1062,632,401,781,418,786,1030,914,433,1077,763,800,287,999,752,315,422,867,865,603,410,967,950,1097,835,305,506,358,1056,1033,1172,897,960,635,728,464,1261,575,596,644,908,691,442,322,803,940,1009,676,592,364,775,560,454,1069])).
% 21.68/5.93 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.68/5.93 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------