%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP099^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:06:45 AM UTC 2026
% Result : Theorem 182.37s 78.34s
% Output : Refutation 177.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP099^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.11/0.23 % Computer : n018.cluster.edu
% 0.11/0.23 % Model : x86_64 x86_64
% 0.11/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.23 % Memory : 8046.5625MB
% 0.11/0.23 % OS : Linux 6.8.0-71-generic
% 0.11/0.23 % CPULimit : 300
% 0.11/0.23 % WCLimit : 300
% 0.11/0.23 % DateTime : Tue Sep 29 19:55:41 UTC 2026
% 0.11/0.23 % CPUTime :
% 0.11/0.23 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
% 1.05/0.80 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.29/1.24 % [INFO] Parsing done (432ms).
% 2.29/1.25 % [INFO] Running in sequential loop mode.
% 3.63/1.65 % [INFO] eprover registered as external prover.
% 3.63/1.66 % [INFO] Scanning for conjecture ...
% 4.13/1.81 % [INFO] Found a conjecture (or negated_conjecture) and 281 axioms. Running axiom selection ...
% 4.41/1.94 % [INFO] Axiom selection finished. Selected 280 axioms (removed 1 axioms).
% 5.44/2.24 % [INFO] Problem is higher-order (TPTP THF).
% 5.44/2.27 % [INFO] Type checking passed.
% 5.44/2.27 % [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 ...
% 182.37/78.33 % External prover 'e' found a proof!
% 182.37/78.33 % [INFO] Killing All external provers ...
% 182.37/78.33 % Time passed: 77961ms (effective reasoning time: 77071ms)
% 182.37/78.33 % 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)>
% 182.37/78.34 % Axioms used in derivation (280): fact_77_diff__le__mono, fact_231_pinf_I2_J, fact_174_list__asc__trans, tcon_fun___Groups_Ominus, fact_149_antisym__conv3, fact_146_linorder__cases, fact_87_nat__diff__right__cancel__le2, fact_99_i__drop__nth__sub, fact_238_i__append__i__take__eq2, fact_176_list__desc__trans, fact_15_measure__induct, fact_125_le__cases3, fact_32_diff__strict__left__mono, fact_246_add__diff__cancel, fact_145_dual__order_Oirrefl, fact_170_ord__less__eq__subst, fact_34_diff__strict__mono, tcon_Nat_Onat___Orderings_Oorder_2, fact_219_minf_I11_J, tcon_Nat_Onat___Orderings_Ono__top, fact_178_dual__order_Ostrict__implies__order, fact_214_verit__comp__simplify1_I3_J, tcon_Nat_Onat___Orderings_Olinorder, tcon_Nat_Onat___Nat_Osize, fact_236_minf_I8_J, fact_206_order__le__less__subst2, fact_105_list__desc__trans__le, fact_211_leD, fact_78_diff__le__self, fact_5_less__imp__diff__less, fact_44_append__same__eq, tcon_List_Olist___Nat_Osize_10, fact_156_less__irrefl, tcon_Nat_Onat___Conditionally__Complete__Lattices_Oconditionally__complete__linorder, fact_122_eq__refl, fact_222_minf_I4_J, fact_123_le__cases, fact_98_nat__diff__right__cancel__le1, fact_97_nat__diff__left__cancel__le1, fact_133_linorder__wlog, fact_223_minf_I3_J, fact_64_ge__less__neq__conv, fact_153_dual__order_Oasym, fact_248_add__diff__cancel__left, fact_193_le__less__linear, fact_6_less__diff__imp__less, fact_9_nat__diff__left__cancel__less, fact_233_verit__comp__simplify1_I1_J, fact_197_le__less__trans, fact_229_pinf_I4_J, fact_135_dual__order_Oeq__iff, fact_101_diff__right__commute, fact_140_dual__order_Ostrict__trans, fact_96_less__diff__le__imp__less, fact_30_diff__commute, fact_79_le__diff__iff_H, tcon_fun___Orderings_Oord, fact_11_nat__diff__right__cancel__eq2, fact_199_antisym__conv2, fact_39_i__append__nth, fact_228_pinf_I5_J, fact_110_list__strict__asc__imp__list__asc, tcon_HOL_Obool___Groups_Ominus_9, fact_80_diff__le__mono2, fact_59_diff__mono, fact_152_less__imp__not__eq, fact_209_le__less, fact_177_order_Onot__eq__order__implies__strict, fact_3_minus__apply, fact_150_less__induct, fact_63_i__append__eq__i__append__conv2__aux, fact_217_less__fun__def, fact_212_list__strict__desc__trans, fact_126_antisym__conv, fact_194_dense__le, fact_65_less__ge__neq__conv, fact_131_order__trans, fact_148_less__imp__not__eq2, fact_35_i__append__i__drop__eq1, fact_166_gt__ex, fact_29_eq__imp__diff__eq, fact_37_last__drop, fact_147_less__imp__triv, fact_60_diff__left__mono, fact_75_le__diff__iff, fact_200_antisym__conv1, fact_56_append__eq__appendI, tcon_Nat_Onat___Groups_Ocancel__semigroup__add, fact_175_list__strict__asc__trans, tcon_HOL_Obool___Orderings_Olinorder_6, fact_50_i__append__nth1, fact_160_less__asym, fact_134_dual__order_Otrans, fact_242_add__le__cancel__right, fact_109_list__strict__asc__trans__le, fact_255_drop__drop, fact_57_Nat_Oex__has__greatest__nat, fact_26_size__neq__size__imp__neq, fact_14_measure__induct__rule, tcon_Nat_Onat___Groups_Ominus_4, fact_70_le__eq__less__or__eq, fact_186_order_Ostrict__iff__order, fact_85_le__diff__le__imp__le, fact_161_less__imp__neq, fact_202_not__less, help_If_1_1_T, fact_40_i__append__def, fact_22_less__not__refl3, fact_143_less__imp__not__less, fact_83_le__imp__diff__le, fact_136_dual__order_Oantisym, fact_27_neq__if__length__neq, fact_155_ord__eq__less__trans, fact_61_diff__right__mono, fact_28_Ex__list__of__length, fact_187_order_Oorder__iff__strict, fact_67_le__greater__neq__conv, fact_218_verit__la__disequality, fact_213_complete__interval, tcon_HOL_Obool___Orderings_Oord_8, fact_243_add__le__cancel__left, fact_207_order__le__less__subst1, fact_58_append__eq__append__conv2, tcon_HOL_Obool___Orderings_Opreorder_5, fact_189_order_Ostrict__trans1, fact_47_diff__diff__cancel, fact_12_nat__diff__right__cancel__less, fact_13_length__induct, fact_250_add__diff__cancel__right, fact_216_pinf_I8_J, fact_171_ord__eq__less__subst, fact_215_pinf_I6_J, fact_237_minf_I6_J, fact_91_nth__equalityI, fact_230_pinf_I3_J, fact_33_diff__eq__diff__less, fact_55_nat__le__linear, tcon_Nat_Onat___Orderings_Owellorder, tcon_Nat_Onat___Groups_Oordered__ab__semigroup__add__imp__le, fact_210_leI, fact_253_nat__add__left__cancel__le, fact_76_Nat_Odiff__diff__eq, fact_74_eq__diff__iff, fact_204_order__less__le__subst2, fact_241_add__left__cancel, fact_208_less__le, fact_168_order__less__subst2, fact_17_infinite__descent__measure, fact_73_less__mono__imp__le__mono, fact_38_i__append__nth2, fact_89_i__append__eq__i__append__conv2, fact_127_order__class_Oorder_Oeq__iff, fact_68_nat__less__le, fact_93_list__eq__iff__nth__eq, fact_53_eq__imp__le, fact_46_same__append__eq, fact_169_order__less__subst1, fact_41_drop__append, fact_108_list__asc__trans__le, fact_72_le__neq__implies__less, fact_8_nat__diff__left__cancel__eq2, fact_49_i__append__assoc, fact_31_diff__strict__right__mono, fact_42_append_Oassoc, fact_179_dual__order_Ostrict__iff__order, fact_128_ord__eq__le__trans, tcon_Nat_Onat___Orderings_Oord_3, fact_36_i__append__i__drop__eq2, fact_84_eq__diff__left__iff, fact_129_ord__le__eq__trans, fact_159_less__asym_H, fact_185_dual__order_Ostrict__trans1, fact_195_dense__ge, fact_252_nat__add__left__cancel__less, fact_167_lt__ex, fact_115_order__subst1, fact_184_dual__order_Ostrict__trans2, tcon_Nat_Onat___Groups_Ocancel__ab__semigroup__add, fact_71_less__or__eq__imp__le, fact_224_minf_I2_J, help_If_3_1_T, fact_137_dual__order_Ostrict__implies__not__eq, fact_234_ex__gt__or__lt, help_If_2_1_T, fact_151_less__not__sym, fact_180_dual__order_Oorder__iff__strict, fact_232_pinf_I1_J, fact_121_linear, fact_69_less__imp__le__nat, fact_10_nat__diff__right__cancel__eq1, fact_132_dual__order_Orefl, tcon_HOL_Obool___Orderings_Oorder_7, fact_16_fun__diff__def, fact_227_pinf_I7_J, fact_120_antisym, fact_1_i__append__eq__i__append__conv, fact_20_nat__less__induct, fact_116_order__subst2, fact_112_le__funE, fact_158_less__trans, fact_254_diff__diff__left, fact_165_neqE, fact_66_greater__le__neq__conv, fact_183_dense__ge__bounded, fact_19_infinite__descent, fact_106_nat__descend__induct, fact_48_append__eq__append__conv, fact_118_ord__le__eq__subst, fact_226_pinf_I11_J, fact_191_less__le__not__le, fact_220_minf_I7_J, fact_82_le__diff__imp__le, fact_94_less__diff__iff, fact_240_add__right__cancel, fact_102_nth__append2, tcon_fun___Orderings_Opreorder, fact_0_same__i__append__eq, fact_163_order_Oasym, fact_157_less__linear, fact_154_ord__less__eq__trans, fact_164_neq__iff, fact_245_add__less__cancel__right, fact_90_nth__append, tcon_Nat_Onat___Orderings_Opreorder_1, fact_201_le__neq__trans, fact_100_diff__eq__diff__eq, fact_54_le__antisym, fact_172_ex__has__least__nat, fact_88_i__append__eq__i__appendI, fact_86_nat__diff__left__cancel__le2, fact_25_nat__neq__iff, fact_4_diff__less__mono2, fact_196_less__le__trans, fact_95_diff__less__mono, fact_2_length__drop, fact_111_le__funD, fact_142_exists__least__iff, fact_203_not__le, fact_225_minf_I1_J, fact_247_diff__add__cancel, fact_173_list__drop__eq__conv, tcon_fun___Orderings_Oorder, fact_192_le__imp__less__or__eq, fact_198_less__imp__le, fact_249_add__diff__cancel__left_H, fact_221_minf_I5_J, fact_139_not__less__iff__gr__or__eq, fact_81_le__diff__swap, fact_117_ord__eq__le__subst, fact_205_order__less__le__subst1, fact_7_nat__diff__left__cancel__eq1, fact_181_order_Ostrict__implies__order, fact_24_less__not__refl, fact_130_order__class_Oorder_Oantisym, fact_92_Skolem__list__nth, fact_114_le__fun__def, fact_18_linorder__neqE__nat, fact_188_order_Ostrict__trans2, fact_113_le__funI, fact_124_order_Otrans, fact_182_dense__le__bounded, fact_51_le__refl, fact_239_nth__drop, fact_244_add__less__cancel__left, fact_251_add__diff__cancel__right_H, fact_104_order__refl, fact_23_less__not__refl2, fact_144_order_Ostrict__trans, fact_235_list__strict__desc__imp__list__desc, fact_190_not__le__imp__less, fact_119_eq__iff, fact_107_Lattices__Big_Oex__has__greatest__nat, fact_103_nth__append1, fact_62_diff__eq__diff__less__eq, fact_141_linorder__less__wlog, fact_21_less__irrefl__nat, fact_43_append__assoc, fact_138_order_Ostrict__implies__not__eq, fact_162_dense, fact_52_le__trans
% 182.37/78.34 % No. of inferences in proof: 701
% 182.37/78.34 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 77961 ms resp. 77071 ms w/o parsing
% 177.75/78.64 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 177.75/78.64 thf(nat_type, type, nat: $tType).
% 177.75/78.64 thf(a_type, type, a: $tType).
% 177.75/78.64 thf(size_decl, type, size: !> [TA: $tType]: $o).
% 177.75/78.64 thf(minus_decl, type, minus: !> [TA: $tType]: $o).
% 177.75/78.64 thf(ord_decl, type, ord: !> [TA: $tType]: $o).
% 177.75/78.64 thf(order_decl, type, order: !> [TA: $tType]: $o).
% 177.75/78.64 thf(group_add_decl, type, group_add: !> [TA: $tType]: $o).
% 177.75/78.64 thf(no_bot_decl, type, no_bot: !> [TA: $tType]: $o).
% 177.75/78.64 thf(no_top_decl, type, no_top: !> [TA: $tType]: $o).
% 177.75/78.64 thf(linorder_decl, type, linorder: !> [TA: $tType]: $o).
% 177.75/78.64 thf(preorder_decl, type, preorder: !> [TA: $tType]: $o).
% 177.75/78.64 thf(wellorder_decl, type, wellorder: !> [TA: $tType]: $o).
% 177.75/78.64 thf(dense_order_decl, type, dense_order: !> [TA: $tType]: $o).
% 177.75/78.64 thf(dense_linorder_decl, type, dense_linorder: !> [TA: $tType]: $o).
% 177.75/78.64 thf(cancel_semigroup_add_decl, type, cancel_semigroup_add: !> [TA: $tType]: $o).
% 177.75/78.64 thf(ordered_ab_group_add_decl, type, ordered_ab_group_add: !> [TA: $tType]: $o).
% 177.75/78.64 thf(cancel146912293up_add_decl, type, cancel146912293up_add: !> [TA: $tType]: $o).
% 177.75/78.64 thf(ordere236663937imp_le_decl, type, ordere236663937imp_le: !> [TA: $tType]: $o).
% 177.75/78.64 thf(condit1656338222tinuum_decl, type, condit1656338222tinuum: !> [TA: $tType]: $o).
% 177.75/78.64 thf(condit1037483654norder_decl, type, condit1037483654norder: !> [TA: $tType]: $o).
% 177.75/78.64 thf(minus_minus_decl, type, minus_minus: !> [TA: $tType]: (TA > (TA > TA))).
% 177.75/78.64 thf(plus_plus_decl, type, plus_plus: !> [TA: $tType]: (TA > (TA > TA))).
% 177.75/78.64 thf(if_decl, type, if: !> [TA: $tType]: ($o > (TA > (TA > TA)))).
% 177.75/78.64 thf(list_asc_decl, type, list_asc: !> [TA: $tType]: ((list @ TA) > $o)).
% 177.75/78.64 thf(list_desc_decl, type, list_desc: !> [TA: $tType]: ((list @ TA) > $o)).
% 177.75/78.64 thf(list_strict_asc_decl, type, list_strict_asc: !> [TA: $tType]: ((list @ TA) > $o)).
% 177.75/78.64 thf(list_strict_desc_decl, type, list_strict_desc: !> [TA: $tType]: ((list @ TA) > $o)).
% 177.75/78.64 thf(listIn521021761append_decl, type, listIn521021761append: !> [TA: $tType]: ((list @ TA) > ((nat > TA) > (nat > TA)))).
% 177.75/78.64 thf(listIn1569887318i_drop_decl, type, listIn1569887318i_drop: !> [TA: $tType]: (nat > ((nat > TA) > (nat > TA)))).
% 177.75/78.64 thf(listIn1033672622i_take_decl, type, listIn1033672622i_take: !> [TA: $tType]: (nat > ((nat > TA) > (list @ TA)))).
% 177.75/78.64 thf(append_decl, type, append: !> [TA: $tType]: ((list @ TA) > ((list @ TA) > (list @ TA)))).
% 177.75/78.64 thf(drop_decl, type, drop: !> [TA: $tType]: (nat > ((list @ TA) > (list @ TA)))).
% 177.75/78.64 thf(last_decl, type, last: !> [TA: $tType]: ((list @ TA) > TA)).
% 177.75/78.64 thf(nth_decl, type, nth: !> [TA: $tType]: ((list @ TA) > (nat > TA))).
% 177.75/78.64 thf(size_size_decl, type, size_size: !> [TA: $tType]: (TA > nat)).
% 177.75/78.64 thf(ord_less_decl, type, ord_less: !> [TA: $tType]: (TA > (TA > $o))).
% 177.75/78.64 thf(ord_less_eq_decl, type, ord_less_eq: !> [TA: $tType]: (TA > (TA > $o))).
% 177.75/78.64 thf(f_decl, type, f: (nat > a)).
% 177.75/78.64 thf(n_decl, type, n: nat).
% 177.75/78.64 thf(xs_decl, type, xs: (list @ a)).
% 177.75/78.64 thf(sk1_decl, type, sk1: !> [TA: $tType]: (TA > (TA > ((TA > (TA > $o)) > TA)))).
% 177.75/78.64 thf(sk2_decl, type, sk2: !> [TA: $tType]: (TA > (TA > ((TA > (TA > $o)) > TA)))).
% 177.75/78.64 thf(sk3_decl, type, sk3: !> [TA: $tType]: (TA > (TA > ((TA > (TA > $o)) > TA)))).
% 177.75/78.64 thf(sk4_decl, type, sk4: !> [TA: $tType]: (TA > (TA > ((TA > (TA > $o)) > TA)))).
% 177.75/78.64 thf(sk25_decl, type, sk25: !> [TA: $tType]: (TA > TA)).
% 177.75/78.64 thf(sk46_decl, type, sk46: !> [TA: $tType]: (nat > (list @ TA))).
% 177.75/78.64 thf(sk50_decl, type, sk50: !> [TA: $tType]: (TA > TA)).
% 177.75/78.64 thf(sk51_decl, type, sk51: !> [TA: $tType]: (TA > TA)).
% 177.75/78.64 thf(sk55_decl, type, sk55: !> [TA: $tType]: (TA > TA)).
% 177.75/78.64 thf(sk91_decl, type, sk91: !> [TA: $tType]: ((TA > nat) > (TA > ((TA > $o) > TA)))).
% 177.75/78.64 thf(sk93_decl, type, sk93: nat).
% 177.75/78.64 thf(sk99_decl, type, sk99: nat).
% 177.75/78.64 thf(sk102_decl, type, sk102: nat).
% 177.75/78.64 thf(sk103_decl, type, sk103: nat).
% 177.75/78.64 thf(sk1_def, definition, sk1 = (^ [TA: $tType]: (^ [A:TA,B:TA,C:(TA > (TA > $o))]: (@+ [D:TA]: ~ (! [E:TA]: ((ord_less_eq @ TA @ D @ E) => (C @ D @ E)))))) ).
% 177.75/78.64 thf(sk2_def, definition, sk2 = (^ [TA: $tType]: (^ [A:TA,B:TA,C:(TA > (TA > $o))]: (@+ [D:TA]: ~ ((ord_less_eq @ TA @ (sk1 @ TA @ A @ B @ C) @ D) => (C @ (sk1 @ TA @ A @ B @ C) @ D))))) ).
% 177.75/78.64 thf(sk3_def, definition, sk3 = (^ [TA: $tType]: (^ [A:TA,B:TA,C:(TA > (TA > $o))]: (@+ [D:TA]: ~ (! [E:TA]: ((C @ E @ D) => (C @ D @ E)))))) ).
% 177.75/78.64 thf(sk4_def, definition, sk4 = (^ [TA: $tType]: (^ [A:TA,B:TA,C:(TA > (TA > $o))]: (@+ [D:TA]: ~ ((C @ D @ (sk3 @ TA @ A @ B @ C)) => (C @ (sk3 @ TA @ A @ B @ C) @ D))))) ).
% 177.75/78.64 thf(sk25_def, definition, sk25 = (^ [TA: $tType]: (^ [A:TA]: (@+ [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (C = A)))))) ).
% 177.75/78.64 thf(sk46_def, definition, sk46 = (^ [TA: $tType]: (^ [A:nat]: (@+ [B:(list @ TA)]: ((size_size @ (list @ TA) @ B) = A)))) ).
% 177.75/78.64 thf(sk50_def, definition, sk50 = (^ [TA: $tType]: (^ [A:TA]: (@+ [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (C = A)))))) ).
% 177.75/78.64 thf(sk51_def, definition, sk51 = (^ [TA: $tType]: (^ [A:TA]: (@+ [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (C = A)))))) ).
% 177.75/78.64 thf(sk55_def, definition, sk55 = (^ [TA: $tType]: (^ [A:TA]: (@+ [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (C = A)))))) ).
% 177.75/78.64 thf(sk91_def, definition, sk91 = (^ [TA: $tType]: (^ [A:(TA > nat),B:TA,C:(TA > $o)]: (@+ [D:TA]: ((C @ D) & ! [E:TA]: ((C @ E) => (ord_less_eq @ nat @ (A @ D) @ (A @ E))))))) ).
% 177.75/78.64 thf(221,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_minf_I8_J)).
% 177.75/78.64 thf(1036,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 177.75/78.64 thf(107,axiom,((! [TA: $tType]: ((listIn521021761append @ TA) = (^ [A:(list @ TA),B:(nat > TA),C:nat]: (if @ TA @ (ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) @ (nth @ TA @ A @ C) @ (B @ (minus_minus @ nat @ C @ (size_size @ (list @ TA) @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_i__append__nth)).
% 177.75/78.64 thf(629,plain,((! [TA: $tType]: ((listIn521021761append @ TA) = (^ [A:(list @ TA),B:(nat > TA),C:nat]: (if @ TA @ (ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) @ (nth @ TA @ A @ C) @ (B @ (minus_minus @ nat @ C @ (size_size @ (list @ TA) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 177.75/78.64 thf(217,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((B = C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_ord__less__eq__trans)).
% 177.75/78.64 thf(1024,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((B = C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 177.75/78.64 thf(150,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:TA]: ? [B:TB]: ! [C:TB]: ((ord_less @ TB @ C @ B) => (A = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_minf_I11_J)).
% 177.75/78.64 thf(760,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 177.75/78.64 thf(22,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((B = C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_ord__le__eq__trans)).
% 177.75/78.64 thf(347,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((B = C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 177.75/78.64 thf(278,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A != B) => ((~ (ord_less @ TA @ A @ B)) => (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_neqE)).
% 177.75/78.64 thf(1237,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) => ((~ (ord_less @ TA @ A @ B)) => (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 177.75/78.64 thf(24,axiom,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_order__class_Oorder_Oeq__iff)).
% 177.75/78.64 thf(352,plain,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 177.75/78.64 thf(192,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_order_Oasym)).
% 177.75/78.64 thf(909,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 177.75/78.64 thf(219,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(nat > TA),D:(nat > TA)]: (((size_size @ (list @ TA) @ A) = (size_size @ (list @ TA) @ B)) => (((listIn521021761append @ TA @ A @ C) = (listIn521021761append @ TA @ B @ D)) = ((A = B) & (C = D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_i__append__eq__i__append__conv)).
% 177.75/78.64 thf(1031,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(nat > TA),D:(nat > TA)]: (((size_size @ (list @ TA) @ A) = (size_size @ (list @ TA) @ B)) => (((listIn521021761append @ TA @ A @ C) = (listIn521021761append @ TA @ B @ D)) = ((A = B) & ((C) = (D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 177.75/78.64 thf(157,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:nat,C:(nat > TA)]: ((ord_less_eq @ nat @ (size_size @ (list @ TA) @ A) @ B) => ((listIn521021761append @ TA @ A @ C @ B) = (C @ (minus_minus @ nat @ B @ (size_size @ (list @ TA) @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_i__append__nth2)).
% 177.75/78.64 thf(777,plain,((! [TA: $tType]: (! [A:(list @ TA),B:nat,C:(nat > TA)]: ((ord_less_eq @ nat @ (size_size @ (list @ TA) @ A) @ B) => ((listIn521021761append @ TA @ A @ (C) @ B) = (C @ (minus_minus @ nat @ B @ (size_size @ (list @ TA) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 177.75/78.64 thf(85,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_order__less__le__subst1)).
% 177.75/78.64 thf(555,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 177.75/78.64 thf(256,axiom,((! [TA: $tType]: (! [A:((list @ TA) > $o),B:(list @ TA)]: ((! [C:(list @ TA)]: ((! [D:(list @ TA)]: ((ord_less @ nat @ (size_size @ (list @ TA) @ D) @ (size_size @ (list @ TA) @ C)) => (A @ D))) => (A @ C))) => (A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_length__induct)).
% 177.75/78.64 thf(1158,plain,((! [TA: $tType]: (! [A:((list @ TA) > $o),B:(list @ TA)]: ((! [C:(list @ TA)]: ((! [D:(list @ TA)]: ((ord_less @ nat @ (size_size @ (list @ TA) @ D) @ (size_size @ (list @ TA) @ C)) => (A @ D))) => (A @ C))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 177.75/78.64 thf(141,axiom,((! [TA: $tType]: (! [A:nat,B:(list @ TA),C:(list @ TA)]: (((ord_less @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((nth @ TA @ (append @ TA @ B @ C) @ A) = (nth @ TA @ B @ A))) & ((~ (ord_less @ nat @ A @ (size_size @ (list @ TA) @ B))) => ((nth @ TA @ (append @ TA @ B @ C) @ A) = (nth @ TA @ C @ (minus_minus @ nat @ A @ (size_size @ (list @ TA) @ B))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_nth__append)).
% 177.75/78.64 thf(730,plain,((! [TA: $tType]: (! [A:nat,B:(list @ TA),C:(list @ TA)]: (((ord_less @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((nth @ TA @ (append @ TA @ B @ C) @ A) = (nth @ TA @ B @ A))) & ((~ (ord_less @ nat @ A @ (size_size @ (list @ TA) @ B))) => ((nth @ TA @ (append @ TA @ B @ C) @ A) = (nth @ TA @ C @ (minus_minus @ nat @ A @ (size_size @ (list @ TA) @ B))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 177.75/78.64 thf(12,axiom,((linorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Olinorder_6)).
% 177.75/78.64 thf(318,plain,((linorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 177.75/78.64 thf(67,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (C != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_pinf_I4_J)).
% 177.75/78.64 thf(502,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (C = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 177.75/78.64 thf(503,plain,(! [TA:$tType,B:TA,A:TA] : ((~ (linorder @ TA)) | (~ (ord_less @ TA @ (sk25 @ TA @ A) @ B)) | (~ (B = A)))),inference(cnf,[status(esa)],[502])).
% 177.75/78.64 thf(504,plain,(! [TA:$tType,B:TA,A:TA] : ((B != A) | (~ (linorder @ TA)) | (~ (ord_less @ TA @ (sk25 @ TA @ A) @ B)))),inference(lifteq,[status(thm)],[503])).
% 177.75/78.64 thf(505,plain,(! [TA:$tType,A:TA] : ((~ (linorder @ TA)) | (~ (ord_less @ TA @ (sk25 @ TA @ A) @ A)))),inference(simp,[status(thm)],[504])).
% 177.75/78.64 thf(1441,plain,(! [TA:$tType,A:TA] : (~ (($true)) | (~ (ord_less @ TA @ (sk25 @ TA @ A) @ A)) | ((linorder @ $o) != (linorder @ TA)))),inference(paramod_ordered,[status(thm)],[318,505])).
% 177.75/78.64 thf(1442,plain,(! [TA:$tType,A:TA] : ((~ (ord_less @ TA @ (sk25 @ TA @ A) @ A)) | ((linorder @ $o) != (linorder @ TA)))),inference(simp,[status(thm)],[1441])).
% 177.75/78.64 thf(1443,plain,(! [A:$o] : ((~ (ord_less @ $o @ (sk25 @ $o @ A) @ A)))),inference(pattern_uni,[status(thm)],[1442:[bind_type(TA,$thf($o))]])).
% 177.75/78.64 thf(210,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(nat > TA)]: ((listIn521021761append @ TA @ A @ (listIn521021761append @ TA @ B @ C)) = (listIn521021761append @ TA @ (append @ TA @ A @ B) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_i__append__assoc)).
% 177.75/78.64 thf(994,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(nat > TA)]: ((listIn521021761append @ TA @ A @ (listIn521021761append @ TA @ B @ C)) = (listIn521021761append @ TA @ (append @ TA @ A @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 177.75/78.64 thf(9,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((A = B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_eq__refl)).
% 177.75/78.64 thf(305,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((A = B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 177.75/78.64 thf(306,plain,(! [TA:$tType,B:TA,A:TA] : ((~ (preorder @ TA)) | (~ (A = B)) | (ord_less_eq @ TA @ A @ B))),inference(cnf,[status(esa)],[305])).
% 177.75/78.64 thf(307,plain,(! [TA:$tType,B:TA,A:TA] : ((A != B) | (~ (preorder @ TA)) | (ord_less_eq @ TA @ A @ B))),inference(lifteq,[status(thm)],[306])).
% 177.75/78.64 thf(308,plain,(! [TA:$tType,A:TA] : ((~ (preorder @ TA)) | (ord_less_eq @ TA @ A @ A))),inference(simp,[status(thm)],[307])).
% 177.75/78.64 thf(230,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_less__le__trans)).
% 177.75/78.65 thf(1073,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 177.75/78.65 thf(54,axiom,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Opreorder)).
% 177.75/78.65 thf(449,plain,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 177.75/78.65 thf(123,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA),D:(nat > TA),E:(nat > TA)]: (((append @ TA @ A @ B) = C) => ((D = (listIn521021761append @ TA @ B @ E)) => ((listIn521021761append @ TA @ A @ D) = (listIn521021761append @ TA @ C @ E))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_i__append__eq__i__appendI)).
% 177.75/78.65 thf(677,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA),D:(nat > TA),E:(nat > TA)]: (((append @ TA @ A @ B) = C) => (((D) = (listIn521021761append @ TA @ B @ E)) => ((listIn521021761append @ TA @ A @ D) = (listIn521021761append @ TA @ C @ E))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 177.75/78.65 thf(98,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_diff__strict__right__mono)).
% 177.75/78.65 thf(597,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 177.75/78.65 thf(223,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_diff__right__mono)).
% 177.75/78.65 thf(1041,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 177.75/78.65 thf(260,axiom,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ D) => (ord_less_eq @ nat @ D @ C))) => (? [D:nat]: ((A @ D) & ! [E:nat]: ((A @ E) => (ord_less_eq @ nat @ E @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_Nat_Oex__has__greatest__nat)).
% 177.75/78.65 thf(1173,plain,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ D) => (ord_less_eq @ nat @ D @ C))) => (? [D:nat]: ((A @ D) & ! [E:nat]: ((A @ E) => (ord_less_eq @ nat @ E @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 177.75/78.65 thf(250,axiom,((! [TA: $tType]: (! [A:nat,B:(list @ TA)]: ((ord_less @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((last @ TA @ (drop @ TA @ A @ B)) = (last @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_last__drop)).
% 177.75/78.65 thf(1142,plain,((! [TA: $tType]: (! [A:nat,B:(list @ TA)]: ((ord_less @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((last @ TA @ (drop @ TA @ A @ B)) = (last @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 177.75/78.65 thf(30,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_ord__le__eq__subst)).
% 177.75/78.65 thf(379,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 177.75/78.65 thf(1,conjecture,((((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) => ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn521021761append @ a @ (drop @ a @ n @ xs) @ f))) & ((~ (ord_less @ nat @ n @ (size_size @ (list @ a) @ xs))) => ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 177.75/78.65 thf(2,negated_conjecture,((~ (((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) => ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn521021761append @ a @ (drop @ a @ n @ xs) @ f))) & ((~ (ord_less @ nat @ n @ (size_size @ (list @ a) @ xs))) => ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f)))))),inference(neg_conjecture,[status(cth)],[1])).
% 177.75/78.65 thf(283,plain,((~ (((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) => ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn521021761append @ a @ (drop @ a @ n @ xs) @ f))) & ((~ (ord_less @ nat @ n @ (size_size @ (list @ a) @ xs))) => ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 177.75/78.65 thf(284,plain,((((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) | ~ (ord_less @ nat @ n @ (size_size @ (list @ a) @ xs))) & ((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) | ~ ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f))) & (~ ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn521021761append @ a @ (drop @ a @ n @ xs) @ f)) | ~ (ord_less @ nat @ n @ (size_size @ (list @ a) @ xs))) & (~ ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn521021761append @ a @ (drop @ a @ n @ xs) @ f)) | ~ ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f))))),inference(cnf,[status(esa)],[283])).
% 177.75/78.65 thf(286,plain,((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) | (~ ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f)))),inference(cnfConj,[status(thm)],[284])).
% 177.75/78.65 thf(289,plain,(((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | (ord_less @ nat @ n @ (size_size @ (list @ a) @ xs))),inference(lifteq,[status(thm)],[286])).
% 177.75/78.65 thf(76,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_less__not__refl)).
% 177.75/78.65 thf(531,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 177.75/78.65 thf(532,plain,((~ (? [A:nat]: (ord_less @ nat @ A @ A)))),inference(miniscope,[status(thm)],[531])).
% 177.75/78.65 thf(533,plain,(! [A:nat] : ((~ (ord_less @ nat @ A @ A)))),inference(cnf,[status(esa)],[532])).
% 177.75/78.65 thf(1254,plain,(! [A:nat] : (((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | ~ (($true)) | ((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) != (ord_less @ nat @ A @ A)))),inference(paramod_ordered,[status(thm)],[289,533])).
% 177.75/78.65 thf(1255,plain,(! [A:nat] : (((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | ((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) != (ord_less @ nat @ A @ A)))),inference(simp,[status(thm)],[1254])).
% 177.75/78.65 thf(1261,plain,(! [A:nat] : (((^ [B:nat]: (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs))) != (^ [B:nat]: (n))) | ((^ [B:nat]: (listIn521021761append @ a @ xs @ f)) != (^ [B:nat]: (f))) | ((^ [B:nat]: (B)) != (^ [B:nat]: (B))) | (n != A) | ((size_size @ (list @ a) @ xs) != A))),inference(simp,[status(thm)],[1255])).
% 177.75/78.65 thf(1265,plain,(((^ [A:nat]: (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs))) != (^ [A:nat]: (n))) | ((^ [A:nat]: (listIn521021761append @ a @ xs @ f)) != (^ [A:nat]: (f))) | ((size_size @ (list @ a) @ xs) != n)),inference(simp,[status(thm)],[1261])).
% 177.75/78.65 thf(1269,plain,(((minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) != n) | ((listIn521021761append @ a @ xs @ (f) @ sk99) != (f @ sk99)) | ((size_size @ (list @ a) @ xs) != n)),inference(func_ext,[status(esa)],[1265])).
% 177.75/78.65 thf(50,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TA) => (minus @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Groups_Ominus)).
% 177.75/78.65 thf(440,plain,((! [TA: $tType,TB: $tType]: ((minus @ TA) => (minus @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 177.75/78.65 thf(70,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_leI)).
% 177.75/78.65 thf(511,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 177.75/78.65 thf(232,axiom,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_gt__ex)).
% 177.75/78.65 thf(1078,plain,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 177.75/78.65 thf(83,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA]: ((plus_plus @ TA @ (minus_minus @ TA @ A @ B) @ B) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_diff__add__cancel)).
% 177.75/78.65 thf(550,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA]: ((plus_plus @ TA @ (minus_minus @ TA @ A @ B) @ B) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 177.75/78.65 thf(257,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:nat,C:(nat > TA)]: ((ord_less_eq @ nat @ (size_size @ (list @ TA) @ A) @ B) => ((listIn1033672622i_take @ TA @ B @ (listIn521021761append @ TA @ A @ C)) = (append @ TA @ A @ (listIn1033672622i_take @ TA @ (minus_minus @ nat @ B @ (size_size @ (list @ TA) @ A)) @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_i__append__i__take__eq2)).
% 177.75/78.65 thf(1164,plain,((! [TA: $tType]: (! [A:(list @ TA),B:nat,C:(nat > TA)]: ((ord_less_eq @ nat @ (size_size @ (list @ TA) @ A) @ B) => ((listIn1033672622i_take @ TA @ B @ (listIn521021761append @ TA @ A @ C)) = (append @ TA @ A @ (listIn1033672622i_take @ TA @ (minus_minus @ nat @ B @ (size_size @ (list @ TA) @ A)) @ (C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 177.75/78.65 thf(135,axiom,(((ord_less @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_nat__less__le)).
% 177.75/78.65 thf(711,plain,(((ord_less @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 177.75/78.65 thf(712,plain,(((^ [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) & ~ (A = B))) = (ord_less @ nat))),inference(lifteq,[status(thm)],[711])).
% 177.75/78.65 thf(1327,plain,(! [A:nat] : (((^ [B:nat]: ((ord_less_eq @ nat @ A @ B) & ~ (A = B))) = (ord_less @ nat @ A)))),inference(func_ext,[status(esa)],[712])).
% 177.75/78.65 thf(130,axiom,((! [TA: $tType]: (((=) @ (list @ TA)) = (^ [A:(list @ TA),B:(list @ TA)]: (((size_size @ (list @ TA) @ A) = (size_size @ (list @ TA) @ B)) & ! [C:nat]: ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => ((nth @ TA @ A @ C) = (nth @ TA @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_list__eq__iff__nth__eq)).
% 177.75/78.65 thf(698,plain,((! [TA: $tType]: (((=) @ (list @ TA)) = (^ [A:(list @ TA),B:(list @ TA)]: (((size_size @ (list @ TA) @ A) = (size_size @ (list @ TA) @ B)) & ! [C:nat]: ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => ((nth @ TA @ A @ C) = (nth @ TA @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 177.75/78.65 thf(146,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:nat,C:(list @ TA)]: ((ord_less_eq @ nat @ (size_size @ (list @ TA) @ A) @ B) => ((nth @ TA @ (append @ TA @ A @ C) @ B) = (nth @ TA @ C @ (minus_minus @ nat @ B @ (size_size @ (list @ TA) @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_nth__append2)).
% 177.75/78.65 thf(747,plain,((! [TA: $tType]: (! [A:(list @ TA),B:nat,C:(list @ TA)]: ((ord_less_eq @ nat @ (size_size @ (list @ TA) @ A) @ B) => ((nth @ TA @ (append @ TA @ A @ C) @ B) = (nth @ TA @ C @ (minus_minus @ nat @ B @ (size_size @ (list @ TA) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 177.75/78.65 thf(203,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (A != B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_less__le)).
% 177.75/78.65 thf(945,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 177.75/78.65 thf(20,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((ord_less_eq @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB)]: ! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_le__fun__def)).
% 177.75/78.65 thf(340,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((ord_less_eq @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB)]: ! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 177.75/78.65 thf(120,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((~ (ord_less @ TA @ A @ B)) = (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_antisym__conv2)).
% 177.75/78.65 thf(670,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((~ (ord_less @ TA @ A @ B)) = (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 177.75/78.65 thf(263,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((ord_less_eq @ TA @ A @ B) = (ord_less_eq @ TA @ C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_diff__eq__diff__less__eq)).
% 177.75/78.65 thf(1196,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((ord_less_eq @ TA @ A @ B) = (ord_less_eq @ TA @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 177.75/78.65 thf(158,axiom,((! [TA: $tType]: (! [A:nat,B:(list @ TA)]: ((size_size @ (list @ TA) @ (drop @ TA @ A @ B)) = (minus_minus @ nat @ (size_size @ (list @ TA) @ B) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_length__drop)).
% 177.75/78.65 thf(780,plain,((! [TA: $tType]: (! [A:nat,B:(list @ TA)]: ((size_size @ (list @ TA) @ (drop @ TA @ A @ B)) = (minus_minus @ nat @ (size_size @ (list @ TA) @ B) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 177.75/78.65 thf(781,plain,(! [TA:$tType,B:(list @ TA),A:nat] : (((size_size @ (list @ TA) @ (drop @ TA @ A @ B)) = (minus_minus @ nat @ (size_size @ (list @ TA) @ B) @ A)))),inference(cnf,[status(esa)],[780])).
% 177.75/78.65 thf(782,plain,(! [TA:$tType,B:(list @ TA),A:nat] : (((size_size @ (list @ TA) @ (drop @ TA @ A @ B)) = (minus_minus @ nat @ (size_size @ (list @ TA) @ B) @ A)))),inference(lifteq,[status(thm)],[781])).
% 177.75/78.65 thf(225,axiom,((! [TA: $tType]: ((cancel146912293up_add @ 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_248_add__diff__cancel__left)).
% 177.75/78.65 thf(1046,plain,((! [TA: $tType]: ((cancel146912293up_add @ 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)],[225])).
% 177.75/78.65 thf(7,axiom,((preorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Opreorder_5)).
% 177.75/78.65 thf(301,plain,((preorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 177.75/78.65 thf(113,axiom,((! [A:nat]: (ord_less_eq @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_le__refl)).
% 177.75/78.65 thf(651,plain,((! [A:nat]: (ord_less_eq @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 177.75/78.65 thf(139,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_order__less__subst1)).
% 177.75/78.65 thf(724,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 177.75/78.65 thf(1260,plain,(! [A:nat] : (((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | (n != A) | ((size_size @ (list @ a) @ xs) != A))),inference(simp,[status(thm)],[1255])).
% 177.75/78.65 thf(1264,plain,(((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | ((size_size @ (list @ a) @ xs) != n)),inference(simp,[status(thm)],[1260])).
% 177.75/78.65 thf(195,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA),D:(list @ TA)]: ((((size_size @ (list @ TA) @ A) = (size_size @ (list @ TA) @ B)) | ((size_size @ (list @ TA) @ C) = (size_size @ (list @ TA) @ D))) => (((append @ TA @ A @ C) = (append @ TA @ B @ D)) = ((A = B) & (C = D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_append__eq__append__conv)).
% 177.75/78.65 thf(917,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA),D:(list @ TA)]: ((((size_size @ (list @ TA) @ A) = (size_size @ (list @ TA) @ B)) | ((size_size @ (list @ TA) @ C) = (size_size @ (list @ TA) @ D))) => (((append @ TA @ A @ C) = (append @ TA @ B @ D)) = ((A = B) & (C = D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 177.75/78.65 thf(165,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (C != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_minf_I3_J)).
% 177.75/78.65 thf(802,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (C = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 177.75/78.65 thf(26,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA),D:(list @ TA),E:(list @ TA)]: (((append @ TA @ A @ B) = C) => ((D = (append @ TA @ B @ E)) => ((append @ TA @ A @ D) = (append @ TA @ C @ E))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_append__eq__appendI)).
% 177.75/78.65 thf(357,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA),D:(list @ TA),E:(list @ TA)]: (((append @ TA @ A @ B) = C) => ((D = (append @ TA @ B @ E)) => ((append @ TA @ A @ D) = (append @ TA @ C @ E))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 177.75/78.65 thf(247,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_30_diff__commute)).
% 177.75/78.65 thf(1132,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)],[247])).
% 177.75/78.65 thf(94,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_le__less__linear)).
% 177.75/78.65 thf(587,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 177.75/78.65 thf(174,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_less__imp__not__eq)).
% 177.75/78.65 thf(838,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 177.75/78.65 thf(190,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_less__imp__not__eq2)).
% 177.75/78.65 thf(902,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 177.75/78.65 thf(86,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_pinf_I8_J)).
% 177.75/78.65 thf(559,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 177.75/78.65 thf(109,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_order_Ostrict__implies__not__eq)).
% 177.75/78.65 thf(635,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 177.75/78.65 thf(636,plain,(! [TA:$tType,B:TA,A:TA] : ((~ (order @ TA)) | (~ (ord_less @ TA @ A @ B)) | (~ (A = B)))),inference(cnf,[status(esa)],[635])).
% 177.75/78.65 thf(637,plain,(! [TA:$tType,B:TA,A:TA] : ((A != B) | (~ (order @ TA)) | (~ (ord_less @ TA @ A @ B)))),inference(lifteq,[status(thm)],[636])).
% 177.75/78.65 thf(638,plain,(! [TA:$tType,A:TA] : ((~ (order @ TA)) | (~ (ord_less @ TA @ A @ A)))),inference(simp,[status(thm)],[637])).
% 177.75/78.65 thf(276,axiom,(((ord_less_eq @ nat) = (^ [A:nat,B:nat]: ((ord_less @ nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_le__eq__less__or__eq)).
% 177.75/78.65 thf(1232,plain,(((ord_less_eq @ nat) = (^ [A:nat,B:nat]: ((ord_less @ nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[276])).
% 177.75/78.65 thf(28,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_order__trans)).
% 177.75/78.65 thf(376,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 177.75/78.65 thf(72,axiom,((ordere236663937imp_le @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Oordered__ab__semigroup__add__imp__le)).
% 177.75/78.65 thf(514,plain,((ordere236663937imp_le @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 177.75/78.65 thf(253,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_less__imp__le)).
% 177.75/78.65 thf(1151,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 177.75/78.65 thf(166,axiom,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_lt__ex)).
% 177.75/78.65 thf(806,plain,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 177.75/78.65 thf(153,axiom,((! [TA: $tType]: (! [A:nat]: ? [B:(list @ TA)]: ((size_size @ (list @ TA) @ B) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_Ex__list__of__length)).
% 177.75/78.65 thf(766,plain,((! [TA: $tType]: (! [A:nat]: ? [B:(list @ TA)]: ((size_size @ (list @ TA) @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 177.75/78.65 thf(128,axiom,((linorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Olinorder)).
% 177.75/78.65 thf(693,plain,((linorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 177.75/78.65 thf(803,plain,(! [TA:$tType,B:TA,A:TA] : ((~ (linorder @ TA)) | (~ (ord_less @ TA @ B @ (sk51 @ TA @ A))) | (~ (B = A)))),inference(cnf,[status(esa)],[802])).
% 177.75/78.65 thf(804,plain,(! [TA:$tType,B:TA,A:TA] : ((B != A) | (~ (linorder @ TA)) | (~ (ord_less @ TA @ B @ (sk51 @ TA @ A))))),inference(lifteq,[status(thm)],[803])).
% 177.75/78.65 thf(805,plain,(! [TA:$tType,A:TA] : ((~ (linorder @ TA)) | (~ (ord_less @ TA @ A @ (sk51 @ TA @ A))))),inference(simp,[status(thm)],[804])).
% 177.75/78.65 thf(2027,plain,(! [TA:$tType,A:TA] : (~ (($true)) | (~ (ord_less @ TA @ A @ (sk51 @ TA @ A))) | ((linorder @ nat) != (linorder @ TA)))),inference(paramod_ordered,[status(thm)],[693,805])).
% 177.75/78.65 thf(2028,plain,(! [TA:$tType,A:TA] : ((~ (ord_less @ TA @ A @ (sk51 @ TA @ A))) | ((linorder @ nat) != (linorder @ TA)))),inference(simp,[status(thm)],[2027])).
% 177.75/78.65 thf(2029,plain,(! [A:nat] : ((~ (ord_less @ nat @ A @ (sk51 @ nat @ A))))),inference(pattern_uni,[status(thm)],[2028:[bind_type(TA,$thf(nat))]])).
% 177.75/78.65 thf(2047,plain,(! [A:nat] : (((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | ~ (($true)) | ((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) != (ord_less @ nat @ A @ (sk51 @ nat @ A))))),inference(paramod_ordered,[status(thm)],[289,2029])).
% 177.75/78.65 thf(2048,plain,(! [A:nat] : (((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | ((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) != (ord_less @ nat @ A @ (sk51 @ nat @ A))))),inference(simp,[status(thm)],[2047])).
% 177.75/78.65 thf(2053,plain,(! [A:nat] : (((^ [B:nat]: (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs))) != (^ [B:nat]: (n))) | ((^ [B:nat]: (listIn521021761append @ a @ xs @ f)) != (^ [B:nat]: (f))) | ((^ [B:nat]: (B)) != (^ [B:nat]: (B))) | (n != A) | ((sk51 @ nat @ A) != (size_size @ (list @ a) @ xs)))),inference(simp,[status(thm)],[2048])).
% 177.75/78.65 thf(2058,plain,(((^ [A:nat]: (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs))) != (^ [A:nat]: (n))) | ((^ [A:nat]: (listIn521021761append @ a @ xs @ f)) != (^ [A:nat]: (f))) | ((sk51 @ nat @ n) != (size_size @ (list @ a) @ xs))),inference(simp,[status(thm)],[2053])).
% 177.75/78.65 thf(269,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_dual__order_Oasym)).
% 177.75/78.65 thf(1215,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 177.75/78.65 thf(4,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA)]: (((append @ TA @ A @ B) = (append @ TA @ C @ B)) = (A = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_append__same__eq)).
% 177.75/78.65 thf(293,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA)]: (((append @ TA @ A @ B) = (append @ TA @ C @ B)) = (A = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 177.75/78.65 thf(41,axiom,((ord @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oord_8)).
% 177.75/78.65 thf(411,plain,((ord @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 177.75/78.65 thf(10,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less_eq @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_linorder__wlog)).
% 177.75/78.65 thf(309,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less_eq @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 177.75/78.65 thf(310,plain,(! [TA:$tType,C:TA,B:TA,A:(TA > (TA > $o))] : (((~ (linorder @ TA) | (ord_less_eq @ TA @ (sk1 @ TA @ C @ B @ (A)) @ (sk2 @ TA @ C @ B @ (A))) | (A @ (sk4 @ TA @ C @ B @ (A)) @ (sk3 @ TA @ C @ B @ (A))) | (A @ B @ C)) & (~ (linorder @ TA) | (ord_less_eq @ TA @ (sk1 @ TA @ C @ B @ (A)) @ (sk2 @ TA @ C @ B @ (A))) | ~ (A @ (sk3 @ TA @ C @ B @ (A)) @ (sk4 @ TA @ C @ B @ (A))) | (A @ B @ C)) & (~ (linorder @ TA) | ~ (A @ (sk1 @ TA @ C @ B @ (A)) @ (sk2 @ TA @ C @ B @ (A))) | (A @ (sk4 @ TA @ C @ B @ (A)) @ (sk3 @ TA @ C @ B @ (A))) | (A @ B @ C)) & (~ (linorder @ TA) | ~ (A @ (sk1 @ TA @ C @ B @ (A)) @ (sk2 @ TA @ C @ B @ (A))) | ~ (A @ (sk3 @ TA @ C @ B @ (A)) @ (sk4 @ TA @ C @ B @ (A))) | (A @ B @ C))))),inference(cnf,[status(esa)],[309])).
% 177.75/78.65 thf(312,plain,(! [TA:$tType,C:TA,B:TA,A:(TA > (TA > $o))] : ((~ (linorder @ TA)) | (ord_less_eq @ TA @ (sk1 @ TA @ C @ B @ (A)) @ (sk2 @ TA @ C @ B @ (A))) | (~ (A @ (sk3 @ TA @ C @ B @ (A)) @ (sk4 @ TA @ C @ B @ (A)))) | (A @ B @ C))),inference(cnfConj,[status(thm)],[310])).
% 177.75/78.65 thf(35,axiom,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder)).
% 177.75/78.65 thf(397,plain,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 177.75/78.65 thf(126,axiom,((! [TA: $tType]: ((preorder @ TA) => ((list_strict_desc @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less @ nat @ C @ B) => (ord_less @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ C)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_list__strict__desc__trans)).
% 177.75/78.65 thf(687,plain,((! [TA: $tType]: ((preorder @ TA) => ((list_strict_desc @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less @ nat @ C @ B) => (ord_less @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ C)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 177.75/78.65 thf(243,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_ord__eq__less__trans)).
% 177.75/78.65 thf(1104,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 177.75/78.65 thf(178,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((A != B) => (ord_less @ TA @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_le__neq__trans)).
% 177.75/78.65 thf(849,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((~ (A = B)) => (ord_less @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 177.75/78.65 thf(3,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_T)).
% 177.75/78.65 thf(292,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 177.75/78.65 thf(202,axiom,((! [TA: $tType]: (! [A:nat,B:(list @ TA),C:(nat > TA)]: ((ord_less_eq @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((listIn1569887318i_drop @ TA @ A @ (listIn521021761append @ TA @ B @ C)) = (listIn521021761append @ TA @ (drop @ TA @ A @ B) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_i__append__i__drop__eq1)).
% 177.75/78.65 thf(942,plain,((! [TA: $tType]: (! [A:nat,B:(list @ TA),C:(nat > TA)]: ((ord_less_eq @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((listIn1569887318i_drop @ TA @ A @ (listIn521021761append @ TA @ B @ C)) = (listIn521021761append @ TA @ (drop @ TA @ A @ B) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 177.75/78.65 thf(264,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_eq__imp__le)).
% 177.75/78.65 thf(1199,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 177.75/78.65 thf(168,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_19_infinite__descent)).
% 177.75/78.65 thf(810,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)],[168])).
% 177.75/78.65 thf(77,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_le__trans)).
% 177.75/78.65 thf(534,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 177.75/78.65 thf(254,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:TA]: ? [B:TB]: ! [C:TB]: ((ord_less @ TB @ B @ C) => (A = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_pinf_I11_J)).
% 177.75/78.65 thf(1153,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 177.75/78.65 thf(151,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ (minus_minus @ nat @ A @ C)) => ((ord_less_eq @ nat @ C @ A) => (ord_less_eq @ nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_nat__diff__left__cancel__le2)).
% 177.75/78.65 thf(761,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ (minus_minus @ nat @ A @ C)) => ((ord_less_eq @ nat @ C @ A) => (ord_less_eq @ nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 177.75/78.65 thf(18,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_1_1_T)).
% 177.75/78.65 thf(334,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 177.75/78.65 thf(237,axiom,((preorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Opreorder_1)).
% 177.75/78.65 thf(1091,plain,((preorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 177.75/78.65 thf(171,axiom,((! [TA: $tType]: ((preorder @ TA) => ((list_desc @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less_eq @ nat @ C @ B) => (ord_less_eq @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ C)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_list__desc__trans__le)).
% 177.75/78.65 thf(825,plain,((! [TA: $tType]: ((preorder @ TA) => ((list_desc @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less_eq @ nat @ C @ B) => (ord_less_eq @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ C)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 177.75/78.65 thf(8,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) = (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_antisym__conv)).
% 177.75/78.65 thf(302,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) = (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 177.75/78.65 thf(180,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_minf_I7_J)).
% 177.75/78.65 thf(862,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 177.75/78.65 thf(270,axiom,((! [TA: $tType]: (! [A:nat,B:(list @ TA),C:nat]: ((ord_less_eq @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((nth @ TA @ (drop @ TA @ A @ B) @ C) = (nth @ TA @ B @ (plus_plus @ nat @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_nth__drop)).
% 177.75/78.65 thf(1217,plain,((! [TA: $tType]: (! [A:nat,B:(list @ TA),C:nat]: ((ord_less_eq @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((nth @ TA @ (drop @ TA @ A @ B) @ C) = (nth @ TA @ B @ (plus_plus @ nat @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 177.75/78.65 thf(33,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB)]: ((! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))) => (ord_less_eq @ (TA > TB) @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_le__funI)).
% 177.75/78.65 thf(392,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB)]: ((! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))) => (ord_less_eq @ (TA > TB) @ (A) @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 177.75/78.65 thf(44,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_2_1_T)).
% 177.75/78.65 thf(422,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 177.75/78.65 thf(423,plain,(! [TA:$tType,B:TA,A:TA] : (((if @ TA @ ($false) @ A @ B) = B))),inference(cnf,[status(esa)],[422])).
% 177.75/78.65 thf(424,plain,(! [TA:$tType,B:TA,A:TA] : (((if @ TA @ ($false) @ A @ B) = B))),inference(lifteq,[status(thm)],[423])).
% 177.75/78.65 thf(46,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_dual__order_Oantisym)).
% 177.75/78.65 thf(429,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 177.75/78.65 thf(206,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:nat,C:(nat > TA)]: ((ord_less_eq @ nat @ (size_size @ (list @ TA) @ A) @ B) => ((listIn1569887318i_drop @ TA @ B @ (listIn521021761append @ TA @ A @ C)) = (listIn1569887318i_drop @ TA @ (minus_minus @ nat @ B @ (size_size @ (list @ TA) @ A)) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_i__append__i__drop__eq2)).
% 177.75/78.65 thf(957,plain,((! [TA: $tType]: (! [A:(list @ TA),B:nat,C:(nat > TA)]: ((ord_less_eq @ nat @ (size_size @ (list @ TA) @ A) @ B) => ((listIn1569887318i_drop @ TA @ B @ (listIn521021761append @ TA @ A @ C)) = (listIn1569887318i_drop @ TA @ (minus_minus @ nat @ B @ (size_size @ (list @ TA) @ A)) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 177.75/78.65 thf(273,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_25_nat__neq__iff)).
% 177.75/78.65 thf(1223,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)],[273])).
% 177.75/78.65 thf(87,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (ord_less @ TA @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_pinf_I5_J)).
% 177.75/78.65 thf(561,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (ord_less @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 177.75/78.65 thf(160,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (C != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_pinf_I3_J)).
% 177.75/78.65 thf(787,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (C = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 177.75/78.65 thf(788,plain,(! [TA:$tType,B:TA,A:TA] : ((~ (linorder @ TA)) | (~ (ord_less @ TA @ (sk50 @ TA @ A) @ B)) | (~ (B = A)))),inference(cnf,[status(esa)],[787])).
% 177.75/78.65 thf(789,plain,(! [TA:$tType,B:TA,A:TA] : ((B != A) | (~ (linorder @ TA)) | (~ (ord_less @ TA @ (sk50 @ TA @ A) @ B)))),inference(lifteq,[status(thm)],[788])).
% 177.75/78.65 thf(790,plain,(! [TA:$tType,A:TA] : ((~ (linorder @ TA)) | (~ (ord_less @ TA @ (sk50 @ TA @ A) @ A)))),inference(simp,[status(thm)],[789])).
% 177.75/78.65 thf(1664,plain,(! [TA:$tType,A:TA] : (~ (($true)) | (~ (ord_less @ TA @ (sk50 @ TA @ A) @ A)) | ((linorder @ $o) != (linorder @ TA)))),inference(paramod_ordered,[status(thm)],[318,790])).
% 177.75/78.65 thf(1665,plain,(! [TA:$tType,A:TA] : ((~ (ord_less @ TA @ (sk50 @ TA @ A) @ A)) | ((linorder @ $o) != (linorder @ TA)))),inference(simp,[status(thm)],[1664])).
% 177.75/78.65 thf(1666,plain,(! [A:$o] : ((~ (ord_less @ $o @ (sk50 @ $o @ A) @ A)))),inference(pattern_uni,[status(thm)],[1665:[bind_type(TA,$thf($o))]])).
% 177.75/78.65 thf(39,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_order_Otrans)).
% 177.75/78.65 thf(407,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 177.75/78.65 thf(57,axiom,((! [TA: $tType,TB: $tType]: ((wellorder @ TB) => (! [A:(TA > TB),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ TB @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_measure__induct__rule)).
% 177.75/78.65 thf(467,plain,((! [TA: $tType,TB: $tType]: ((wellorder @ TB) => (! [A:(TA > TB),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ TB @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 177.75/78.65 thf(61,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_order__le__less__subst1)).
% 177.75/78.65 thf(484,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 177.75/78.65 thf(27,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA,C:TA]: (((ord_less_eq @ TA @ A @ B) => (~ (ord_less_eq @ TA @ B @ C))) => (((ord_less_eq @ TA @ B @ A) => (~ (ord_less_eq @ TA @ A @ C))) => (((ord_less_eq @ TA @ A @ C) => (~ (ord_less_eq @ TA @ C @ B))) => (((ord_less_eq @ TA @ C @ B) => (~ (ord_less_eq @ TA @ B @ A))) => (((ord_less_eq @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))) => (~ ((ord_less_eq @ TA @ C @ A) => (~ (ord_less_eq @ TA @ A @ B))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_le__cases3)).
% 177.75/78.65 thf(361,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA,C:TA]: (((ord_less_eq @ TA @ A @ B) => (~ (ord_less_eq @ TA @ B @ C))) => (((ord_less_eq @ TA @ B @ A) => (~ (ord_less_eq @ TA @ A @ C))) => (((ord_less_eq @ TA @ A @ C) => (~ (ord_less_eq @ TA @ C @ B))) => (((ord_less_eq @ TA @ C @ B) => (~ (ord_less_eq @ TA @ B @ A))) => (((ord_less_eq @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))) => (~ ((ord_less_eq @ TA @ C @ A) => (~ (ord_less_eq @ TA @ A @ B))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 177.75/78.65 thf(184,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_not__le)).
% 177.75/78.65 thf(879,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 177.75/78.65 thf(1656,plain,(! [TA:$tType,A:TA] : (~ (($true)) | (~ (ord_less @ TA @ (sk50 @ TA @ A) @ A)) | ((linorder @ nat) != (linorder @ TA)))),inference(paramod_ordered,[status(thm)],[693,790])).
% 177.75/78.65 thf(1657,plain,(! [TA:$tType,A:TA] : ((~ (ord_less @ TA @ (sk50 @ TA @ A) @ A)) | ((linorder @ nat) != (linorder @ TA)))),inference(simp,[status(thm)],[1656])).
% 177.75/78.65 thf(1658,plain,(! [A:nat] : ((~ (ord_less @ nat @ (sk50 @ nat @ A) @ A)))),inference(pattern_uni,[status(thm)],[1657:[bind_type(TA,$thf(nat))]])).
% 177.75/78.65 thf(1676,plain,(! [A:nat] : (((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | ~ (($true)) | ((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) != (ord_less @ nat @ (sk50 @ nat @ A) @ A)))),inference(paramod_ordered,[status(thm)],[289,1658])).
% 177.75/78.65 thf(1677,plain,(! [A:nat] : (((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | ((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) != (ord_less @ nat @ (sk50 @ nat @ A) @ A)))),inference(simp,[status(thm)],[1676])).
% 177.75/78.65 thf(1682,plain,(! [A:nat] : (((^ [B:nat]: (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs))) != (^ [B:nat]: (n))) | ((^ [B:nat]: (listIn521021761append @ a @ xs @ f)) != (^ [B:nat]: (f))) | ((^ [B:nat]: (B)) != (^ [B:nat]: (B))) | ((sk50 @ nat @ A) != n) | ((size_size @ (list @ a) @ xs) != A))),inference(simp,[status(thm)],[1677])).
% 177.75/78.65 thf(1687,plain,(((^ [A:nat]: (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs))) != (^ [A:nat]: (n))) | ((^ [A:nat]: (listIn521021761append @ a @ xs @ f)) != (^ [A:nat]: (f))) | ((sk50 @ nat @ (size_size @ (list @ a) @ xs)) != n)),inference(simp,[status(thm)],[1682])).
% 177.75/78.65 thf(75,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_20_nat__less__induct)).
% 177.75/78.65 thf(522,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)],[75])).
% 177.75/78.65 thf(266,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (minus_minus @ nat @ A @ B) @ (minus_minus @ nat @ C @ B)) => (ord_less @ nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_nat__diff__right__cancel__less)).
% 177.75/78.65 thf(1210,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (minus_minus @ nat @ A @ B) @ (minus_minus @ nat @ C @ B)) => (ord_less @ nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 177.75/78.65 thf(149,axiom,((! [TA: $tType]: (! [A:nat,B:nat,C:(nat > TA)]: ((ord_less_eq @ nat @ A @ B) => ((listIn1569887318i_drop @ TA @ A @ C @ (minus_minus @ nat @ B @ A)) = (C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_i__drop__nth__sub)).
% 177.75/78.65 thf(757,plain,((! [TA: $tType]: (! [A:nat,B:nat,C:(nat > TA)]: ((ord_less_eq @ nat @ A @ B) => ((listIn1569887318i_drop @ TA @ A @ (C) @ (minus_minus @ nat @ B @ A)) = (C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 177.75/78.65 thf(15,axiom,((! [TA: $tType]: ((ordere236663937imp_le @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ C @ B)) = (ord_less_eq @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_add__le__cancel__right)).
% 177.75/78.65 thf(324,plain,((! [TA: $tType]: ((ordere236663937imp_le @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ C @ B)) = (ord_less_eq @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 177.75/78.65 thf(179,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_pinf_I1_J)).
% 177.75/78.65 thf(852,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 177.75/78.65 thf(48,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ A @ B) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_le__funD)).
% 177.75/78.65 thf(435,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ (A) @ (B)) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 177.75/78.65 thf(1291,plain,(((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ (f) @ sk103) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f) @ sk103)) | ((size_size @ (list @ a) @ xs) != n)),inference(func_ext,[status(esa)],[1264])).
% 177.75/78.65 thf(134,axiom,((no_top @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Ono__top)).
% 177.75/78.65 thf(710,plain,((no_top @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 177.75/78.65 thf(55,axiom,((! [A:nat,B:nat]: (((ord_less @ nat @ A @ B) | (A = B)) => (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_less__or__eq__imp__le)).
% 177.75/78.65 thf(451,plain,((! [A:nat,B:nat]: (((ord_less @ nat @ A @ B) | (A = B)) => (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 177.75/78.65 thf(452,plain,(! [B:nat,A:nat] : (((~ (ord_less @ nat @ A @ B) | (ord_less_eq @ nat @ A @ B)) & (~ (A = B) | (ord_less_eq @ nat @ A @ B))))),inference(cnf,[status(esa)],[451])).
% 177.75/78.65 thf(454,plain,(! [B:nat,A:nat] : ((~ (A = B)) | (ord_less_eq @ nat @ A @ B))),inference(cnfConj,[status(thm)],[452])).
% 177.75/78.65 thf(455,plain,(! [B:nat,A:nat] : ((A != B) | (ord_less_eq @ nat @ A @ B))),inference(lifteq,[status(thm)],[454])).
% 177.75/78.65 thf(456,plain,(! [A:nat] : ((ord_less_eq @ nat @ A @ A))),inference(simp,[status(thm)],[455])).
% 177.75/78.65 thf(175,axiom,((ord @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oord_3)).
% 177.75/78.65 thf(842,plain,((ord @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 177.75/78.65 thf(74,axiom,((! [TA: $tType]: ((linorder @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ! [C:TA]: ((ord_less_eq @ TA @ B @ C) => (A != C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_less__ge__neq__conv)).
% 177.75/78.65 thf(519,plain,((! [TA: $tType]: ((linorder @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ! [C:TA]: ((ord_less_eq @ TA @ B @ C) => (~ (A = C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 177.75/78.65 thf(1252,plain,((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) | ((^ [A:nat]: (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs))) != (^ [A:nat]: (n))) | ((^ [A:nat]: (listIn521021761append @ a @ xs @ f)) != (^ [A:nat]: (f))) | ((^ [A:nat]: (A)) != (^ [A:nat]: (A)))),inference(simp,[status(thm)],[289])).
% 177.75/78.65 thf(1262,plain,((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) | ((^ [A:nat]: (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs))) != (^ [A:nat]: (n))) | ((^ [A:nat]: (listIn521021761append @ a @ xs @ f)) != (^ [A:nat]: (f)))),inference(simp,[status(thm)],[1252])).
% 177.75/78.65 thf(1270,plain,(((minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) != n) | ((listIn521021761append @ a @ xs @ (f) @ sk102) != (f @ sk102)) | (ord_less @ nat @ n @ (size_size @ (list @ a) @ xs))),inference(func_ext,[status(esa)],[1262])).
% 177.75/78.65 thf(204,axiom,((! [TA: $tType,TB: $tType]: ((wellorder @ TB) => (! [A:(TA > TB),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ TB @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_measure__induct)).
% 177.75/78.65 thf(948,plain,((! [TA: $tType,TB: $tType]: ((wellorder @ TB) => (! [A:(TA > TB),B:(TA > $o),C:TA]: ((! [D:TA]: ((! [E:TA]: ((ord_less @ TB @ (A @ E) @ (A @ D)) => (B @ E))) => (B @ D))) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 177.75/78.65 thf(227,axiom,((! [TA: $tType]: (size @ (list @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_List_Olist___Nat_Osize_10)).
% 177.75/78.65 thf(1064,plain,((! [TA: $tType]: (size @ (list @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 177.75/78.65 thf(245,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_dual__order_Oorder__iff__strict)).
% 177.75/78.65 thf(1111,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 177.75/78.65 thf(240,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ A @ B) | (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_le__imp__less__or__eq)).
% 177.75/78.65 thf(1096,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ A @ B) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 177.75/78.65 thf(249,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_less__not__refl2)).
% 177.75/78.65 thf(1138,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 177.75/78.65 thf(183,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_pinf_I2_J)).
% 177.75/78.65 thf(869,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ E @ F) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 177.75/78.65 thf(159,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_order__less__subst2)).
% 177.75/78.65 thf(783,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 177.75/78.65 thf(66,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_not__less)).
% 177.75/78.65 thf(499,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 177.75/78.65 thf(236,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_le__less__trans)).
% 177.75/78.65 thf(1089,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 177.75/78.65 thf(277,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((A = B) = (C = D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_diff__eq__diff__eq)).
% 177.75/78.65 thf(1234,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((A = B) = (C = D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[277])).
% 177.75/78.65 thf(630,plain,(! [TA:$tType] : (((listIn521021761append @ TA) = (^ [A:(list @ TA),B:(nat > TA),C:nat]: (if @ TA @ (ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) @ (nth @ TA @ A @ C) @ (B @ (minus_minus @ nat @ C @ (size_size @ (list @ TA) @ A)))))))),inference(cnf,[status(esa)],[629])).
% 177.75/78.65 thf(631,plain,(! [TA:$tType] : (((listIn521021761append @ TA) = (^ [A:(list @ TA),B:(nat > TA),C:nat]: (if @ TA @ (ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) @ (nth @ TA @ A @ C) @ (B @ (minus_minus @ nat @ C @ (size_size @ (list @ TA) @ A)))))))),inference(lifteq,[status(thm)],[630])).
% 177.75/78.65 thf(1329,plain,(! [TA:$tType,A:(list @ TA)] : (((listIn521021761append @ TA @ A) = (^ [B:(nat > TA),C:nat]: (if @ TA @ (ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) @ (nth @ TA @ A @ C) @ (B @ (minus_minus @ nat @ C @ (size_size @ (list @ TA) @ A)))))))),inference(func_ext,[status(esa)],[631])).
% 177.75/78.65 thf(62,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (plus_plus @ nat @ A @ B) @ (plus_plus @ nat @ A @ C)) = (ord_less_eq @ nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_nat__add__left__cancel__le)).
% 177.75/78.65 thf(488,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (plus_plus @ nat @ A @ B) @ (plus_plus @ nat @ A @ C)) = (ord_less_eq @ nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 177.75/78.65 thf(199,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_dual__order_Ostrict__implies__order)).
% 177.75/78.65 thf(933,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 177.75/78.65 thf(78,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_5_less__imp__diff__less)).
% 177.75/78.65 thf(537,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)],[78])).
% 177.75/78.65 thf(214,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TB) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_minus__apply)).
% 177.75/78.65 thf(1016,plain,((! [TA: $tType,TB: $tType]: ((minus @ TB) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 177.75/78.65 thf(82,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((ord_less @ TA @ A @ B) = (ord_less @ TA @ C @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_diff__eq__diff__less)).
% 177.75/78.65 thf(547,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((ord_less @ TA @ A @ B) = (ord_less @ TA @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 177.75/78.65 thf(218,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (ord_less @ TA @ B @ A)) = (B = A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_antisym__conv3)).
% 177.75/78.65 thf(1028,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (ord_less @ TA @ B @ A)) = (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 177.75/78.65 thf(234,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_order__less__le__subst2)).
% 177.75/78.65 thf(1082,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 177.75/78.65 thf(125,axiom,((! [TA: $tType]: (((=) @ (list @ TA)) = (^ [A:(list @ TA),B:(list @ TA)]: ! [C:nat]: ((drop @ TA @ C @ A) = (drop @ TA @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_list__drop__eq__conv)).
% 177.75/78.65 thf(684,plain,((! [TA: $tType]: (((=) @ (list @ TA)) = (^ [A:(list @ TA),B:(list @ TA)]: ! [C:nat]: ((drop @ TA @ C @ A) = (drop @ TA @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 177.75/78.65 thf(685,plain,(! [TA:$tType] : ((((=) @ (list @ TA)) = (^ [A:(list @ TA),B:(list @ TA)]: ! [C:nat]: ((drop @ TA @ C @ A) = (drop @ TA @ C @ B)))))),inference(cnf,[status(esa)],[684])).
% 177.75/78.65 thf(686,plain,(! [TA:$tType] : ((((=) @ (list @ TA)) = (^ [A:(list @ TA),B:(list @ TA)]: ! [C:nat]: ((drop @ TA @ C @ A) = (drop @ TA @ C @ B)))))),inference(lifteq,[status(thm)],[685])).
% 177.75/78.65 thf(231,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_252_nat__add__left__cancel__less)).
% 177.75/78.65 thf(1075,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)],[231])).
% 177.75/78.65 thf(59,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_17_infinite__descent__measure)).
% 177.75/78.65 thf(476,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)],[59])).
% 177.75/78.65 thf(105,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ C @ B) => ((ord_less_eq @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ B @ C)) = (ord_less_eq @ nat @ C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79_le__diff__iff_H)).
% 177.75/78.65 thf(622,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ C @ B) => ((ord_less_eq @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ B @ C)) = (ord_less_eq @ nat @ C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 177.75/78.65 thf(246,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA]: (A @ D @ D)) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_linorder__less__wlog)).
% 177.75/78.65 thf(1114,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA]: (A @ D @ D)) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 177.75/78.65 thf(211,axiom,((! [A:nat,B:nat,C:nat]: (((minus_minus @ nat @ A @ B) = (minus_minus @ nat @ C @ B)) => ((ord_less @ nat @ B @ A) => (A = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_nat__diff__right__cancel__eq1)).
% 177.75/78.65 thf(997,plain,((! [A:nat,B:nat,C:nat]: (((minus_minus @ nat @ A @ B) = (minus_minus @ nat @ C @ B)) => ((ord_less @ nat @ B @ A) => (A = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 177.75/78.65 thf(241,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (minus_minus @ nat @ A @ B) @ (minus_minus @ nat @ A @ C)) => (ord_less @ nat @ C @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_nat__diff__left__cancel__less)).
% 177.75/78.65 thf(1099,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ (minus_minus @ nat @ A @ B) @ (minus_minus @ nat @ A @ C)) => (ord_less @ nat @ C @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 177.75/78.65 thf(131,axiom,((! [TA: $tType]: ((ordere236663937imp_le @ 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_245_add__less__cancel__right)).
% 177.75/78.65 thf(701,plain,((! [TA: $tType]: ((ordere236663937imp_le @ 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)],[131])).
% 177.75/78.65 thf(73,axiom,((! [TA: $tType]: ((dense_order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (? [C:TA]: ((ord_less @ TA @ A @ C) & (ord_less @ TA @ C @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_162_dense)).
% 177.75/78.65 thf(515,plain,((! [TA: $tType]: ((dense_order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (? [C:TA]: ((ord_less @ TA @ A @ C) & (ord_less @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 177.75/78.65 thf(143,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_not__le__imp__less)).
% 177.75/78.65 thf(738,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 177.75/78.65 thf(262,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => ((ord_less @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ C @ A)) = (ord_less @ nat @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_less__diff__iff)).
% 177.75/78.65 thf(1192,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => ((ord_less @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ C @ A)) = (ord_less @ nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 177.75/78.65 thf(56,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_minf_I1_J)).
% 177.75/78.65 thf(457,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 177.75/78.65 thf(193,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((minus_minus @ nat @ B @ (minus_minus @ nat @ B @ A)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_diff__diff__cancel)).
% 177.75/78.65 thf(911,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((minus_minus @ nat @ B @ (minus_minus @ nat @ B @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 177.75/78.65 thf(138,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((ord_less_eq @ TA @ A @ B) = (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_antisym__conv1)).
% 177.75/78.65 thf(721,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((ord_less_eq @ TA @ A @ B) = (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 177.75/78.65 thf(281,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_dense__le)).
% 177.75/78.65 thf(1246,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[281])).
% 177.75/78.65 thf(1332,plain,(((minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) != n) | ((listIn521021761append @ a @ xs @ f) != (f)) | (sk103 != sk103) | ((size_size @ (list @ a) @ xs) != n)),inference(simp,[status(thm)],[1291])).
% 177.75/78.65 thf(1333,plain,(((minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) != n) | ((listIn521021761append @ a @ xs @ f) != (f)) | ((size_size @ (list @ a) @ xs) != n)),inference(simp,[status(thm)],[1332])).
% 177.75/78.65 thf(21,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_order__subst2)).
% 177.75/78.65 thf(343,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 177.75/78.65 thf(235,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A != B) = ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_164_neq__iff)).
% 177.75/78.65 thf(1086,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) = ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 177.75/78.65 thf(311,plain,(! [TA:$tType,C:TA,B:TA,A:(TA > (TA > $o))] : ((~ (linorder @ TA)) | (ord_less_eq @ TA @ (sk1 @ TA @ C @ B @ (A)) @ (sk2 @ TA @ C @ B @ (A))) | (A @ (sk4 @ TA @ C @ B @ (A)) @ (sk3 @ TA @ C @ B @ (A))) | (A @ B @ C))),inference(cnfConj,[status(thm)],[310])).
% 177.75/78.65 thf(80,axiom,((! [TA: $tType]: ((preorder @ TA) => ((list_desc @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less @ nat @ C @ B) => (ord_less_eq @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ C)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_list__desc__trans)).
% 177.75/78.65 thf(541,plain,((! [TA: $tType]: ((preorder @ TA) => ((list_desc @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less @ nat @ C @ B) => (ord_less_eq @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ C)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 177.75/78.65 thf(259,axiom,((! [A:nat,B:nat,C:nat]: (((minus_minus @ nat @ A @ B) = (minus_minus @ nat @ C @ B)) => ((ord_less @ nat @ B @ C) => (A = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_nat__diff__right__cancel__eq2)).
% 177.75/78.65 thf(1170,plain,((! [A:nat,B:nat,C:nat]: (((minus_minus @ nat @ A @ B) = (minus_minus @ nat @ C @ B)) => ((ord_less @ nat @ B @ C) => (A = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 177.75/78.65 thf(229,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:$o]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ A) => (C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_less__imp__triv)).
% 177.75/78.65 thf(1071,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:$o]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ A) => (C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 177.75/78.65 thf(258,axiom,((! [TA: $tType]: ((preorder @ TA) => ((list_asc @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less @ nat @ C @ B) => (ord_less_eq @ TA @ (nth @ TA @ A @ C) @ (nth @ TA @ A @ B)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_list__asc__trans)).
% 177.75/78.65 thf(1167,plain,((! [TA: $tType]: ((preorder @ TA) => ((list_asc @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less @ nat @ C @ B) => (ord_less_eq @ TA @ (nth @ TA @ A @ C) @ (nth @ TA @ A @ B)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 177.75/78.65 thf(162,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_diff__left__mono)).
% 177.75/78.65 thf(794,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 177.75/78.65 thf(93,axiom,((minus @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ominus_4)).
% 177.75/78.65 thf(586,plain,((minus @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 177.75/78.65 thf(117,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_pinf_I6_J)).
% 177.75/78.65 thf(662,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 177.75/78.65 thf(137,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ (minus_minus @ nat @ B @ C)) => (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_le__diff__imp__le)).
% 177.75/78.65 thf(718,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ (minus_minus @ nat @ B @ C)) => (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 177.75/78.65 thf(186,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (A != B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_order_Ostrict__iff__order)).
% 177.75/78.65 thf(888,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 177.75/78.65 thf(191,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_order_Oorder__iff__strict)).
% 177.75/78.65 thf(906,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 177.75/78.65 thf(5,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA)]: (((append @ TA @ A @ B) = (append @ TA @ A @ C)) = (B = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_same__append__eq)).
% 177.75/78.65 thf(296,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA)]: (((append @ TA @ A @ B) = (append @ TA @ A @ C)) = (B = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 177.75/78.65 thf(297,plain,(! [TA:$tType,C:(list @ TA),B:(list @ TA),A:(list @ TA)] : ((((append @ TA @ A @ B) = (append @ TA @ A @ C)) = (B = C)))),inference(cnf,[status(esa)],[296])).
% 177.75/78.65 thf(298,plain,(! [TA:$tType,C:(list @ TA),B:(list @ TA),A:(list @ TA)] : ((((append @ TA @ A @ B) = (append @ TA @ A @ C)) = (B = C)))),inference(lifteq,[status(thm)],[297])).
% 177.75/78.65 thf(147,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => (((minus_minus @ nat @ B @ A) = (minus_minus @ nat @ C @ A)) = (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_eq__diff__iff)).
% 177.75/78.65 thf(750,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => (((minus_minus @ nat @ B @ A) = (minus_minus @ nat @ C @ A)) = (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 177.75/78.65 thf(287,plain,((~ ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn521021761append @ a @ (drop @ a @ n @ xs) @ f))) | (~ (ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)))),inference(cnfConj,[status(thm)],[284])).
% 177.75/78.65 thf(290,plain,(((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) != (listIn521021761append @ a @ (drop @ a @ n @ xs) @ f)) | (~ (ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)))),inference(lifteq,[status(thm)],[287])).
% 177.75/78.65 thf(1251,plain,(((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f) @ sk93) != (listIn521021761append @ a @ (drop @ a @ n @ xs) @ (f) @ sk93)) | (~ (ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)))),inference(func_ext,[status(esa)],[290])).
% 177.75/78.65 thf(45,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_order__subst1)).
% 177.75/78.65 thf(425,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 177.75/78.65 thf(71,axiom,((size @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Nat_Osize)).
% 177.75/78.65 thf(513,plain,((size @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 177.75/78.65 thf(90,axiom,((! [TA: $tType]: ((wellorder @ TA) => (! [A:(TA > $o),B:TA]: ((! [C:TA]: ((! [D:TA]: ((ord_less @ TA @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_less__induct)).
% 177.75/78.65 thf(573,plain,((! [TA: $tType]: ((wellorder @ TA) => (! [A:(TA > $o),B:TA]: ((! [C:TA]: ((! [D:TA]: ((ord_less @ TA @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 177.75/78.65 thf(100,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (B != A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_dual__order_Ostrict__iff__order)).
% 177.75/78.65 thf(601,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 177.75/78.65 thf(248,axiom,((! [TA: $tType]: ((linorder @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ! [C:TA]: ((ord_less_eq @ TA @ C @ A) => (B != C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_greater__le__neq__conv)).
% 177.75/78.65 thf(1135,plain,((! [TA: $tType]: ((linorder @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ! [C:TA]: ((ord_less_eq @ TA @ C @ A) => (~ (B = C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 177.75/78.65 thf(42,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_order__refl)).
% 177.75/78.65 thf(412,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 177.75/78.65 thf(169,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (minus_minus @ nat @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_le__imp__diff__le)).
% 177.75/78.65 thf(819,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (minus_minus @ nat @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 177.75/78.65 thf(129,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_dual__order_Ostrict__implies__not__eq)).
% 177.75/78.65 thf(694,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 177.75/78.65 thf(37,axiom,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_eq__iff)).
% 177.75/78.65 thf(402,plain,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 177.75/78.65 thf(176,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_order_Ostrict__trans1)).
% 177.75/78.65 thf(843,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 177.75/78.65 thf(155,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less @ nat @ A @ (minus_minus @ nat @ B @ C)) => ((ord_less_eq @ nat @ D @ C) => (ord_less @ nat @ A @ (minus_minus @ nat @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_less__diff__le__imp__less)).
% 177.75/78.65 thf(772,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less @ nat @ A @ (minus_minus @ nat @ B @ C)) => ((ord_less_eq @ nat @ D @ C) => (ord_less @ nat @ A @ (minus_minus @ nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 177.75/78.65 thf(145,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => ((ord_less_eq @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ C @ A)) = (ord_less_eq @ nat @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_le__diff__iff)).
% 177.75/78.65 thf(743,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => ((ord_less_eq @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ C @ A)) = (ord_less_eq @ nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 177.75/78.65 thf(274,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B) | (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_less__linear)).
% 177.75/78.65 thf(1226,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B) | (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 177.75/78.65 thf(92,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_leD)).
% 177.75/78.65 thf(584,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 177.75/78.65 thf(255,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ C @ B) => (((minus_minus @ nat @ B @ A) = (minus_minus @ nat @ B @ C)) = (A = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_eq__diff__left__iff)).
% 177.75/78.65 thf(1154,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ C @ B) => (((minus_minus @ nat @ B @ A) = (minus_minus @ nat @ B @ C)) = (A = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 177.75/78.65 thf(91,axiom,((! [A:nat,B:nat,C:nat]: ((A = B) => ((minus_minus @ nat @ A @ C) = (minus_minus @ nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_eq__imp__diff__eq)).
% 177.75/78.65 thf(579,plain,((! [A:nat,B:nat,C:nat]: ((A = B) => ((minus_minus @ nat @ A @ C) = (minus_minus @ nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 177.75/78.65 thf(288,plain,((~ ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn521021761append @ a @ (drop @ a @ n @ xs) @ f))) | (~ ((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) = (listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f)))),inference(cnfConj,[status(thm)],[284])).
% 177.75/78.65 thf(291,plain,(((listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)) != (listIn521021761append @ a @ (drop @ a @ n @ xs) @ f)) | ((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f)))),inference(lifteq,[status(thm)],[288])).
% 177.75/78.65 thf(111,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_ord__eq__less__subst)).
% 177.75/78.65 thf(641,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 177.75/78.65 thf(52,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ A @ B) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_le__funE)).
% 177.75/78.65 thf(445,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ (A) @ (B)) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 177.75/78.65 thf(313,plain,(! [TA:$tType,C:TA,B:TA,A:(TA > (TA > $o))] : ((~ (linorder @ TA)) | (~ (A @ (sk1 @ TA @ C @ B @ (A)) @ (sk2 @ TA @ C @ B @ (A)))) | (A @ (sk4 @ TA @ C @ B @ (A)) @ (sk3 @ TA @ C @ B @ (A))) | (A @ B @ C))),inference(cnfConj,[status(thm)],[310])).
% 177.75/78.65 thf(136,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ C @ D)))) => (ord_less_eq @ TA @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_dense__ge__bounded)).
% 177.75/78.65 thf(713,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ C @ D)))) => (ord_less_eq @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 177.75/78.65 thf(238,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_order_Ostrict__trans2)).
% 177.75/78.65 thf(1092,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 177.75/78.65 thf(132,axiom,((! [TA: $tType]: ((linorder @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ A) => (B != C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_ge__less__neq__conv)).
% 177.75/78.65 thf(704,plain,((! [TA: $tType]: ((linorder @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ A) => (~ (B = C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 177.75/78.65 thf(1446,plain,(! [TA:$tType,A:TA] : (~ (($true)) | (~ (ord_less @ TA @ (sk25 @ TA @ A) @ A)) | ((linorder @ nat) != (linorder @ TA)))),inference(paramod_ordered,[status(thm)],[693,505])).
% 177.75/78.65 thf(1447,plain,(! [TA:$tType,A:TA] : ((~ (ord_less @ TA @ (sk25 @ TA @ A) @ A)) | ((linorder @ nat) != (linorder @ TA)))),inference(simp,[status(thm)],[1446])).
% 177.75/78.65 thf(1448,plain,(! [A:nat] : ((~ (ord_less @ nat @ (sk25 @ nat @ A) @ A)))),inference(pattern_uni,[status(thm)],[1447:[bind_type(TA,$thf(nat))]])).
% 177.75/78.65 thf(1628,plain,(! [A:nat] : (((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | ~ (($true)) | ((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) != (ord_less @ nat @ (sk25 @ nat @ A) @ A)))),inference(paramod_ordered,[status(thm)],[289,1448])).
% 177.75/78.65 thf(1629,plain,(! [A:nat] : (((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | ((ord_less @ nat @ n @ (size_size @ (list @ a) @ xs)) != (ord_less @ nat @ (sk25 @ nat @ A) @ A)))),inference(simp,[status(thm)],[1628])).
% 177.75/78.65 thf(1633,plain,(! [A:nat] : (((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | ((sk25 @ nat @ A) != n) | ((size_size @ (list @ a) @ xs) != A))),inference(simp,[status(thm)],[1629])).
% 177.75/78.65 thf(1638,plain,(((listIn1569887318i_drop @ a @ (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs)) @ f) != (listIn1569887318i_drop @ a @ n @ (listIn521021761append @ a @ xs @ f))) | ((sk25 @ nat @ (size_size @ (list @ a) @ xs)) != n)),inference(simp,[status(thm)],[1633])).
% 177.75/78.65 thf(79,axiom,((cancel_semigroup_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocancel__semigroup__add)).
% 177.75/78.65 thf(540,plain,((cancel_semigroup_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 177.75/78.65 thf(101,axiom,((! [TA: $tType]: ((preorder @ TA) => ((list_strict_asc @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less @ nat @ C @ B) => (ord_less @ TA @ (nth @ TA @ A @ C) @ (nth @ TA @ A @ B)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_list__strict__asc__trans)).
% 177.75/78.65 thf(604,plain,((! [TA: $tType]: ((preorder @ TA) => ((list_strict_asc @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less @ nat @ C @ B) => (ord_less @ TA @ (nth @ TA @ A @ C) @ (nth @ TA @ A @ B)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 177.75/78.65 thf(265,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > nat)]: ((A @ B) => (? [D:TA]: ((A @ D) & ! [E:TA]: ((A @ E) => (ord_less_eq @ nat @ (C @ D) @ (C @ E))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_ex__has__least__nat)).
% 177.75/78.65 thf(1203,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > nat)]: ((A @ B) => (? [D:TA]: ((A @ D) & ! [E:TA]: ((A @ E) => (ord_less_eq @ nat @ (C @ D) @ (C @ E))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[265])).
% 177.75/78.65 thf(1204,plain,(! [TA:$tType,D:TA,C:(TA > nat),B:TA,A:(TA > $o)] : (((~ (A @ B) | (A @ (sk91 @ TA @ (C) @ B @ (A)))) & (~ (A @ B) | ~ (A @ D) | (ord_less_eq @ nat @ (C @ (sk91 @ TA @ (C) @ B @ (A))) @ (C @ D)))))),inference(cnf,[status(esa)],[1203])).
% 177.75/78.65 thf(1205,plain,(! [TA:$tType,C:(TA > nat),B:TA,A:(TA > $o)] : ((~ (A @ B)) | (A @ (sk91 @ TA @ (C) @ B @ (A))))),inference(cnfConj,[status(thm)],[1204])).
% 177.75/78.65 thf(1207,plain,(! [TA:$tType,B:(TA > nat),A:TA] : ((~ (A = A)) | (A = (sk91 @ TA @ (B) @ A @ ((=) @ TA @ A))))),inference(replace_leibeq,[status(thm)],[1205:[bind(A, $thf((=) @ TA @ B))]])).
% 177.75/78.65 thf(1208,plain,(! [TA:$tType,B:(TA > nat),A:TA] : ((A != A) | ((sk91 @ TA @ (B) @ A @ ((=) @ TA @ A)) = A))),inference(lifteq,[status(thm)],[1207])).
% 177.75/78.65 thf(1209,plain,(! [TA:$tType,B:(TA > nat),A:TA] : (((sk91 @ TA @ (B) @ A @ ((=) @ TA @ A)) = A))),inference(simp,[status(thm)],[1208])).
% 177.75/78.65 thf(124,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq @ nat @ A @ (minus_minus @ nat @ B @ C)) => ((ord_less_eq @ nat @ D @ C) => (ord_less_eq @ nat @ A @ (minus_minus @ nat @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_le__diff__le__imp__le)).
% 177.75/78.65 thf(681,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq @ nat @ A @ (minus_minus @ nat @ B @ C)) => ((ord_less_eq @ nat @ D @ C) => (ord_less_eq @ nat @ A @ (minus_minus @ nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 177.75/78.65 thf(142,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ (minus_minus @ nat @ C @ B)) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_nat__diff__right__cancel__le2)).
% 177.75/78.65 thf(736,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ (minus_minus @ nat @ C @ B)) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 177.75/78.65 thf(99,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (ord_less @ TA @ C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_minf_I5_J)).
% 177.75/78.65 thf(599,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (ord_less @ TA @ C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 177.75/78.65 thf(69,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_pinf_I7_J)).
% 177.75/78.65 thf(509,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 177.75/78.65 thf(112,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_less__asym)).
% 177.75/78.65 thf(649,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 177.75/78.65 thf(224,axiom,((! [TA: $tType]: (! [A:nat,B:nat,C:(list @ TA)]: ((drop @ TA @ A @ (drop @ TA @ B @ C)) = (drop @ TA @ (plus_plus @ nat @ A @ B) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_255_drop__drop)).
% 177.75/78.65 thf(1043,plain,((! [TA: $tType]: (! [A:nat,B:nat,C:(list @ TA)]: ((drop @ TA @ A @ (drop @ TA @ B @ C)) = (drop @ TA @ (plus_plus @ nat @ A @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 177.75/78.65 thf(31,axiom,((! [TA: $tType]: ((ordere236663937imp_le @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ A @ C)) = (ord_less_eq @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_add__le__cancel__left)).
% 177.75/78.65 thf(387,plain,((! [TA: $tType]: ((ordere236663937imp_le @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ (plus_plus @ TA @ A @ B) @ (plus_plus @ TA @ A @ C)) = (ord_less_eq @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 177.75/78.65 thf(97,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((A != B) => ((ord_less_eq @ TA @ A @ B) => (ord_less @ TA @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_order_Onot__eq__order__implies__strict)).
% 177.75/78.65 thf(594,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) => ((ord_less_eq @ TA @ A @ B) => (ord_less @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 177.75/78.65 thf(60,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_less__irrefl)).
% 177.75/78.65 thf(482,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 177.75/78.65 thf(483,plain,(! [TA:$tType,A:TA] : ((~ (preorder @ TA)) | (~ (ord_less @ TA @ A @ A)))),inference(cnf,[status(esa)],[482])).
% 177.75/78.65 thf(106,axiom,((! [A:nat,B:nat,C:nat]: (((minus_minus @ nat @ A @ B) = (minus_minus @ nat @ A @ C)) => ((ord_less @ nat @ B @ A) => (B = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_nat__diff__left__cancel__eq1)).
% 177.75/78.65 thf(626,plain,((! [A:nat,B:nat,C:nat]: (((minus_minus @ nat @ A @ B) = (minus_minus @ nat @ A @ C)) => ((ord_less @ nat @ B @ A) => (B = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 177.75/78.65 thf(154,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (minus_minus @ nat @ C @ B) @ (minus_minus @ nat @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_diff__le__mono2)).
% 177.75/78.65 thf(769,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (minus_minus @ nat @ C @ B) @ (minus_minus @ nat @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 177.75/78.65 thf(216,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) | (ord_less_eq @ nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_nat__le__linear)).
% 177.75/78.65 thf(1022,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) | (ord_less_eq @ nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 177.75/78.65 thf(64,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:(list @ TA)]: ((list_strict_asc @ TA @ A) => (! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less_eq @ nat @ C @ B) => (ord_less_eq @ TA @ (nth @ TA @ A @ C) @ (nth @ TA @ A @ B))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_list__strict__asc__trans__le)).
% 177.75/78.65 thf(494,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:(list @ TA)]: ((list_strict_asc @ TA @ A) => (! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less_eq @ nat @ C @ B) => (ord_less_eq @ TA @ (nth @ TA @ A @ C) @ (nth @ TA @ A @ B))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 177.75/78.65 thf(233,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_verit__comp__simplify1_I1_J)).
% 177.75/78.65 thf(1080,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 177.75/78.65 thf(177,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (C != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_minf_I4_J)).
% 177.75/78.65 thf(845,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (C = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 177.75/78.65 thf(846,plain,(! [TA:$tType,B:TA,A:TA] : ((~ (linorder @ TA)) | (~ (ord_less @ TA @ B @ (sk55 @ TA @ A))) | (~ (B = A)))),inference(cnf,[status(esa)],[845])).
% 177.75/78.65 thf(847,plain,(! [TA:$tType,B:TA,A:TA] : ((B != A) | (~ (linorder @ TA)) | (~ (ord_less @ TA @ B @ (sk55 @ TA @ A))))),inference(lifteq,[status(thm)],[846])).
% 177.75/78.65 thf(848,plain,(! [TA:$tType,A:TA] : ((~ (linorder @ TA)) | (~ (ord_less @ TA @ A @ (sk55 @ TA @ A))))),inference(simp,[status(thm)],[847])).
% 177.75/78.65 thf(699,plain,(! [TA:$tType] : ((((=) @ (list @ TA)) = (^ [A:(list @ TA),B:(list @ TA)]: (((size_size @ (list @ TA) @ A) = (size_size @ (list @ TA) @ B)) & ! [C:nat]: ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => ((nth @ TA @ A @ C) = (nth @ TA @ B @ C)))))))),inference(cnf,[status(esa)],[698])).
% 177.75/78.65 thf(700,plain,(! [TA:$tType] : (((^ [A:(list @ TA),B:(list @ TA)]: (((size_size @ (list @ TA) @ A) = (size_size @ (list @ TA) @ B)) & ! [C:nat]: ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => ((nth @ TA @ A @ C) = (nth @ TA @ B @ C))))) = ((=) @ (list @ TA))))),inference(lifteq,[status(thm)],[699])).
% 177.75/78.65 thf(36,axiom,((! [TA: $tType]: ((cancel_semigroup_add @ 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_240_add__right__cancel)).
% 177.75/78.65 thf(399,plain,((! [TA: $tType]: ((cancel_semigroup_add @ 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)],[36])).
% 177.75/78.65 thf(280,axiom,((! [A:nat,B:nat]: (ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_diff__le__self)).
% 177.75/78.65 thf(1244,plain,((! [A:nat,B:nat]: (ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[280])).
% 177.75/78.65 thf(1245,plain,(! [B:nat,A:nat] : ((ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ A))),inference(cnf,[status(esa)],[1244])).
% 177.75/78.65 thf(228,axiom,((! [A:(nat > nat),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less @ nat @ D @ E) => (ord_less @ nat @ (A @ D) @ (A @ E)))) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ nat @ (A @ B) @ (A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_less__mono__imp__le__mono)).
% 177.75/78.65 thf(1066,plain,((! [A:(nat > nat),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less @ nat @ D @ E) => (ord_less @ nat @ (A @ D) @ (A @ E)))) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ nat @ (A @ B) @ (A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 177.75/78.65 thf(103,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_less__not__refl3)).
% 177.75/78.65 thf(608,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 177.75/78.65 thf(34,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_order__class_Oorder_Oantisym)).
% 177.75/78.65 thf(394,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 177.75/78.65 thf(88,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_ord__less__eq__subst)).
% 177.75/78.65 thf(563,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 177.75/78.65 thf(212,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_18_linorder__neqE__nat)).
% 177.75/78.65 thf(1000,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)],[212])).
% 177.75/78.65 thf(282,axiom,((wellorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Owellorder)).
% 177.75/78.65 thf(1250,plain,((wellorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 177.75/78.65 thf(114,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ B) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_add__diff__cancel)).
% 177.75/78.65 thf(653,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ B) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 177.75/78.65 thf(116,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA)]: (((size_size @ (list @ TA) @ A) != (size_size @ (list @ TA) @ B)) => (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_neq__if__length__neq)).
% 177.75/78.65 thf(658,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA)]: ((~ ((size_size @ (list @ TA) @ A) = (size_size @ (list @ TA) @ B))) => (~ (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 177.75/78.65 thf(268,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_order_Ostrict__trans)).
% 177.75/78.65 thf(1213,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 177.75/78.65 thf(767,plain,(! [TA:$tType,A:nat] : (((size_size @ (list @ TA) @ (sk46 @ TA @ A)) = A))),inference(cnf,[status(esa)],[766])).
% 177.75/78.65 thf(768,plain,(! [TA:$tType,A:nat] : (((size_size @ (list @ TA) @ (sk46 @ TA @ A)) = A))),inference(lifteq,[status(thm)],[767])).
% 177.75/78.65 thf(1316,plain,(! [TA:$tType,A:(list @ TA)] : ((((=) @ (list @ TA) @ A) = (^ [B:(list @ TA)]: ! [C:nat]: ((drop @ TA @ C @ A) = (drop @ TA @ C @ B)))))),inference(func_ext,[status(esa)],[686])).
% 177.75/78.65 thf(1645,plain,(! [TA:$tType,C:((list @ TA) > nat),B:(list @ TA),A:(list @ TA)] : (((sk91 @ (list @ TA) @ (C) @ B @ (^ [D:(list @ TA)]: ! [E:nat]: ((drop @ TA @ E @ A) = (drop @ TA @ E @ D)))) = B) | (((=) @ (list @ TA) @ A) != ((=) @ (list @ TA) @ B)))),inference(paramod_ordered,[status(thm)],[1316,1209])).
% 177.75/78.65 thf(1646,plain,(! [TA:$tType,B:((list @ TA) > nat),A:(list @ TA)] : (((sk91 @ (list @ TA) @ (B) @ A @ (^ [C:(list @ TA)]: ! [D:nat]: ((drop @ TA @ D @ A) = (drop @ TA @ D @ C)))) = A))),inference(pattern_uni,[status(thm)],[1645:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 177.75/78.65 thf(1653,plain,(! [TA:$tType,B:((list @ TA) > nat),A:(list @ TA)] : (((sk91 @ (list @ TA) @ (B) @ A @ (^ [C:(list @ TA)]: ! [D:nat]: ((drop @ TA @ D @ A) = (drop @ TA @ D @ C)))) = A))),inference(simp,[status(thm)],[1646])).
% 177.75/78.65 thf(2018,plain,(! [TB:$tType,C:((list @ TB) > nat),B:(list @ TB),A:(list @ TB)] : (((sk91 @ (list @ TB) @ (C) @ B @ ((=) @ (list @ TB) @ A)) = B) | ((^ [D:(list @ TB)]: ! [E:nat]: ((drop @ TB @ E @ A) = (drop @ TB @ E @ D))) != (^ [D:(list @ TB)]: ! [E:nat]: ((drop @ TB @ E @ B) = (drop @ TB @ E @ D)))))),inference(paramod_ordered,[status(thm)],[1316,1653])).
% 177.75/78.65 thf(2019,plain,(! [TB:$tType,B:((list @ TB) > nat),A:(list @ TB)] : (((sk91 @ (list @ TB) @ (B) @ A @ ((=) @ (list @ TB) @ A)) = A))),inference(pattern_uni,[status(thm)],[2018:[bind(A, $thf(A)),bind(B, $thf(A))]])).
% 177.75/78.65 thf(2022,plain,(! [TA:$tType,B:((list @ TA) > nat),A:(list @ TA)] : (((sk91 @ (list @ TA) @ (B) @ A @ ((=) @ (list @ TA) @ A)) = A))),inference(simp,[status(thm)],[2019])).
% 177.75/78.65 thf(6,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_dual__order_Orefl)).
% 177.75/78.65 thf(299,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 177.75/78.65 thf(58,axiom,((! [TA: $tType]: (! [A:nat,B:(list @ TA),C:(list @ TA)]: ((ord_less @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((nth @ TA @ (append @ TA @ B @ C) @ A) = (nth @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_nth__append1)).
% 177.75/78.65 thf(473,plain,((! [TA: $tType]: (! [A:nat,B:(list @ TA),C:(list @ TA)]: ((ord_less @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((nth @ TA @ (append @ TA @ B @ C) @ A) = (nth @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 177.75/78.65 thf(220,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_dual__order_Ostrict__trans2)).
% 177.75/78.65 thf(1034,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 177.75/78.65 thf(122,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_dual__order_Ostrict__trans1)).
% 177.75/78.65 thf(675,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 177.75/78.65 thf(1233,plain,(((^ [A:nat,B:nat]: ((ord_less @ nat @ A @ B) | (A = B))) = (ord_less_eq @ nat))),inference(lifteq,[status(thm)],[1232])).
% 177.75/78.65 thf(1304,plain,(! [A:nat] : (((^ [B:nat]: ((ord_less @ nat @ A @ B) | (A = B))) = (ord_less_eq @ nat @ A)))),inference(func_ext,[status(esa)],[1233])).
% 177.75/78.65 thf(201,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TB) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_fun__diff__def)).
% 177.75/78.65 thf(939,plain,((! [TA: $tType,TB: $tType]: ((minus @ TB) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 177.75/78.65 thf(251,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((A != B) => (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_linorder__cases)).
% 177.75/78.65 thf(1145,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (A = B)) => (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 177.75/78.65 thf(25,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_dual__order_Otrans)).
% 177.75/78.65 thf(355,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 177.75/78.65 thf(148,axiom,((! [TA: $tType]: ((wellorder @ TA) => (((?) @ TA) = (^ [A:(TA > $o)]: ? [B:TA]: ((A @ B) & ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (A @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_exists__least__iff)).
% 177.75/78.65 thf(754,plain,((! [TA: $tType]: ((wellorder @ TA) => (((?) @ TA) = (^ [A:(TA > $o)]: ? [B:TA]: ((A @ B) & ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (A @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 177.75/78.65 thf(84,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_diff__strict__left__mono)).
% 177.75/78.65 thf(553,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 177.75/78.65 thf(226,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > nat),D:nat]: ((A @ B) => ((! [E:TA]: ((A @ E) => (ord_less @ nat @ (C @ E) @ D))) => (? [E:TA]: ((A @ E) & ! [F:TA]: ((A @ F) => (ord_less_eq @ nat @ (C @ F) @ (C @ E)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_Lattices__Big_Oex__has__greatest__nat)).
% 177.75/78.65 thf(1049,plain,((! [TA: $tType]: (! [A:(TA > $o),B:TA,C:(TA > nat),D:nat]: ((A @ B) => ((! [E:TA]: ((A @ E) => (ord_less @ nat @ (C @ E) @ D))) => (? [E:TA]: ((A @ E) & ! [F:TA]: ((A @ F) => (ord_less_eq @ nat @ (C @ F) @ (C @ E)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 177.75/78.65 thf(95,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_254_diff__diff__left)).
% 177.75/78.65 thf(589,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)],[95])).
% 177.75/78.65 thf(197,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ (minus_minus @ nat @ C @ B)) => ((ord_less @ nat @ B @ A) => (ord_less_eq @ nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_nat__diff__right__cancel__le1)).
% 177.75/78.65 thf(927,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ (minus_minus @ nat @ C @ B)) => ((ord_less @ nat @ B @ A) => (ord_less_eq @ nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 177.75/78.65 thf(2035,plain,(! [TA:$tType,A:TA] : (~ (($true)) | (~ (ord_less @ TA @ A @ (sk51 @ TA @ A))) | ((linorder @ $o) != (linorder @ TA)))),inference(paramod_ordered,[status(thm)],[318,805])).
% 177.75/78.65 thf(2036,plain,(! [TA:$tType,A:TA] : ((~ (ord_less @ TA @ A @ (sk51 @ TA @ A))) | ((linorder @ $o) != (linorder @ TA)))),inference(simp,[status(thm)],[2035])).
% 177.75/78.65 thf(2037,plain,(! [A:$o] : ((~ (ord_less @ $o @ A @ (sk51 @ $o @ A))))),inference(pattern_uni,[status(thm)],[2036:[bind_type(TA,$thf($o))]])).
% 177.75/78.65 thf(213,axiom,((! [A:nat,B:(nat > $o),C:nat]: ((! [D:nat]: ((ord_less @ nat @ A @ D) => (B @ D))) => ((! [D:nat]: ((ord_less_eq @ nat @ D @ A) => ((! [E:nat]: ((ord_less @ nat @ D @ E) => (B @ E))) => (B @ D)))) => (B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_nat__descend__induct)).
% 177.75/78.65 thf(1003,plain,((! [A:nat,B:(nat > $o),C:nat]: ((! [D:nat]: ((ord_less @ nat @ A @ D) => (B @ D))) => ((! [D:nat]: ((ord_less_eq @ nat @ D @ A) => ((! [E:nat]: ((ord_less @ nat @ D @ E) => (B @ E))) => (B @ D)))) => (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 177.75/78.65 thf(127,axiom,((! [TA: $tType]: ((listIn521021761append @ TA) = (^ [A:(list @ TA),B:(nat > TA),C:nat]: (if @ TA @ (ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) @ (nth @ TA @ A @ C) @ (B @ (minus_minus @ nat @ C @ (size_size @ (list @ TA) @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_i__append__def)).
% 177.75/78.65 thf(690,plain,((! [TA: $tType]: ((listIn521021761append @ TA) = (^ [A:(list @ TA),B:(nat > TA),C:nat]: (if @ TA @ (ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) @ (nth @ TA @ A @ C) @ (B @ (minus_minus @ nat @ C @ (size_size @ (list @ TA) @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 177.75/78.65 thf(294,plain,(! [TA:$tType,C:(list @ TA),B:(list @ TA),A:(list @ TA)] : ((((append @ TA @ A @ B) = (append @ TA @ C @ B)) = (A = C)))),inference(cnf,[status(esa)],[293])).
% 177.75/78.65 thf(295,plain,(! [TA:$tType,C:(list @ TA),B:(list @ TA),A:(list @ TA)] : ((((append @ TA @ A @ B) = (append @ TA @ C @ B)) = (A = C)))),inference(lifteq,[status(thm)],[294])).
% 177.75/78.65 thf(133,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(nat > TA),C:(nat > TA)]: (((listIn521021761append @ TA @ A @ B) = (listIn521021761append @ TA @ A @ C)) = (B = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_same__i__append__eq)).
% 177.75/78.65 thf(707,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(nat > TA),C:(nat > TA)]: (((listIn521021761append @ TA @ A @ B) = (listIn521021761append @ TA @ A @ C)) = ((B) = (C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 177.75/78.65 thf(43,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_ord__eq__le__subst)).
% 177.75/78.65 thf(414,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 177.75/78.65 thf(16,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_ord__eq__le__trans)).
% 177.75/78.65 thf(327,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 177.75/78.65 thf(205,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((ord_less @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB)]: ((ord_less_eq @ (TA > TB) @ A @ B) & ~ (ord_less_eq @ (TA > TB) @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_less__fun__def)).
% 177.75/78.65 thf(954,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((ord_less @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB)]: ((ord_less_eq @ (TA > TB) @ A @ B) & ~ (ord_less_eq @ (TA > TB) @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 177.75/78.65 thf(40,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_le__cases)).
% 177.75/78.65 thf(409,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 177.75/78.65 thf(121,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ D) => (ord_less @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_diff__strict__mono)).
% 177.75/78.65 thf(673,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ D) => (ord_less @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 177.75/78.65 thf(161,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_verit__comp__simplify1_I3_J)).
% 177.75/78.65 thf(791,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 177.75/78.65 thf(17,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A = B) | ~ (ord_less_eq @ TA @ A @ B) | ~ (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_verit__la__disequality)).
% 177.75/78.65 thf(331,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A = B) | ~ (ord_less_eq @ TA @ A @ B) | ~ (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 177.75/78.65 thf(222,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_4_diff__less__mono2)).
% 177.75/78.65 thf(1038,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)],[222])).
% 177.75/78.65 thf(1317,plain,(! [TA:$tType,B:(list @ TA),A:(list @ TA)] : (((A = B) = (! [C:nat]: ((drop @ TA @ C @ A) = (drop @ TA @ C @ B)))))),inference(func_ext,[status(esa)],[686])).
% 177.75/78.65 thf(167,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_less__not__sym)).
% 177.75/78.65 thf(808,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 177.75/78.65 thf(271,axiom,((order @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oorder_2)).
% 177.75/78.65 thf(1220,plain,((order @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 177.75/78.65 thf(81,axiom,((! [TA: $tType]: ((cancel146912293up_add @ TA) => (! [A:TA,B:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ A) = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_add__diff__cancel__left_H)).
% 177.75/78.65 thf(544,plain,((! [TA: $tType]: ((cancel146912293up_add @ TA) => (! [A:TA,B:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ A) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 177.75/78.65 thf(335,plain,(! [TA:$tType,B:TA,A:TA] : (((if @ TA @ ($true) @ A @ B) = A))),inference(cnf,[status(esa)],[334])).
% 177.75/78.65 thf(336,plain,(! [TA:$tType,B:TA,A:TA] : (((if @ TA @ ($true) @ A @ B) = A))),inference(lifteq,[status(thm)],[335])).
% 177.75/78.65 thf(272,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_less__imp__not__less)).
% 177.75/78.65 thf(1221,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[272])).
% 177.75/78.65 thf(181,axiom,((! [TA: $tType]: ((ordere236663937imp_le @ 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_244_add__less__cancel__left)).
% 177.75/78.65 thf(864,plain,((! [TA: $tType]: ((ordere236663937imp_le @ 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)],[181])).
% 177.75/78.65 thf(239,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_dual__order_Oirrefl)).
% 177.75/78.65 thf(1094,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 177.75/78.65 thf(89,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ D) => (ord_less_eq @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_diff__mono)).
% 177.75/78.65 thf(571,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ D) => (ord_less_eq @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 177.75/78.65 thf(104,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_minf_I2_J)).
% 177.75/78.65 thf(612,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > $o),B:(TA > $o),C:(TA > $o),D:(TA > $o)]: ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:TA]: ! [F:TA]: ((ord_less @ TA @ F @ E) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 177.75/78.65 thf(2576,plain,(! [TA:$tType,TB:$tType,B:(list @ TB),A:nat] : (((^ [C:(nat > TB),D:nat]: (if @ TB @ (ord_less @ nat @ D @ (size_size @ (list @ TB) @ B)) @ (nth @ TB @ B @ D) @ (C @ (minus_minus @ nat @ D @ A)))) = (listIn521021761append @ TB @ B)) | ((size_size @ (list @ TA) @ (sk46 @ TA @ A)) != (size_size @ (list @ TB) @ B)))),inference(paramod_ordered,[status(thm)],[768,1329])).
% 177.75/78.65 thf(2577,plain,(! [TB:$tType,A:nat] : (((^ [B:(nat > TB),C:nat]: (if @ TB @ (ord_less @ nat @ C @ (size_size @ (list @ TB) @ (sk46 @ TB @ A))) @ (nth @ TB @ (sk46 @ TB @ A) @ C) @ (B @ (minus_minus @ nat @ C @ A)))) = (listIn521021761append @ TB @ (sk46 @ TB @ A))))),inference(pattern_uni,[status(thm)],[2576:[bind(A, $thf(C)),bind(B, $thf(sk46 @ TB @ C)),bind_type(TA,$thf(TB))]])).
% 177.75/78.65 thf(2580,plain,(! [TA:$tType,A:nat] : (((^ [B:(nat > TA),C:nat]: (if @ TA @ (ord_less @ nat @ C @ (size_size @ (list @ TA) @ (sk46 @ TA @ A))) @ (nth @ TA @ (sk46 @ TA @ A) @ C) @ (B @ (minus_minus @ nat @ C @ A)))) = (listIn521021761append @ TA @ (sk46 @ TA @ A))))),inference(simp,[status(thm)],[2577])).
% 177.75/78.65 thf(2584,plain,(! [TA:$tType,A:nat] : (((^ [B:(nat > TA),C:nat]: (if @ TA @ (ord_less @ nat @ C @ A) @ (nth @ TA @ (sk46 @ TA @ A) @ C) @ (B @ (minus_minus @ nat @ C @ A)))) = (listIn521021761append @ TA @ (sk46 @ TA @ A))))),inference(rewrite,[status(thm)],[2580,768])).
% 177.75/78.65 thf(279,axiom,((! [TA: $tType]: ((size @ TA) => (! [A:TA,B:TA]: (((size_size @ TA @ A) != (size_size @ TA @ B)) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_size__neq__size__imp__neq)).
% 177.75/78.65 thf(1240,plain,((! [TA: $tType]: ((size @ TA) => (! [A:TA,B:TA]: ((~ ((size_size @ TA @ A) = (size_size @ TA @ B))) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[279])).
% 177.75/78.65 thf(115,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ (minus_minus @ nat @ A @ C)) => ((ord_less @ nat @ B @ A) => (ord_less_eq @ nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_nat__diff__left__cancel__le1)).
% 177.75/78.65 thf(656,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ (minus_minus @ nat @ A @ C)) => ((ord_less @ nat @ B @ A) => (ord_less_eq @ nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 177.75/78.65 thf(1023,plain,(! [B:nat,A:nat] : ((ord_less_eq @ nat @ A @ B) | (ord_less_eq @ nat @ B @ A))),inference(cnf,[status(esa)],[1022])).
% 177.75/78.65 thf(187,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ D @ C)))) => (ord_less_eq @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_dense__le__bounded)).
% 177.75/78.65 thf(891,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ D @ C)))) => (ord_less_eq @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 177.75/78.65 thf(244,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ (minus_minus @ nat @ B @ C)) => (ord_less @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_less__diff__imp__less)).
% 177.75/78.65 thf(1108,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ (minus_minus @ nat @ B @ C)) => (ord_less @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 177.75/78.65 thf(261,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_less__irrefl__nat)).
% 177.75/78.65 thf(1189,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 177.75/78.65 thf(29,axiom,((order @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder_7)).
% 177.75/78.65 thf(378,plain,((order @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 177.75/78.65 thf(300,plain,(! [TA:$tType,A:TA] : ((~ (order @ TA)) | (ord_less_eq @ TA @ A @ A))),inference(cnf,[status(esa)],[299])).
% 177.75/78.65 thf(1324,plain,(! [TA:$tType,A:TA] : (~ (($true)) | (ord_less_eq @ TA @ A @ A) | ((order @ $o) != (order @ TA)))),inference(paramod_ordered,[status(thm)],[378,300])).
% 177.75/78.65 thf(1325,plain,(! [TA:$tType,A:TA] : ((ord_less_eq @ TA @ A @ A) | ((order @ $o) != (order @ TA)))),inference(simp,[status(thm)],[1324])).
% 177.75/78.65 thf(1326,plain,(! [A:$o] : ((ord_less_eq @ $o @ A @ A))),inference(pattern_uni,[status(thm)],[1325:[bind_type(TA,$thf($o))]])).
% 177.75/78.65 thf(208,axiom,((! [TA: $tType]: ((condit1037483654norder @ TA) => (! [A:TA,B:TA,C:(TA > $o)]: ((ord_less @ TA @ A @ B) => ((C @ A) => ((~ (C @ B)) => (? [D:TA]: ((ord_less_eq @ TA @ A @ D) & (ord_less_eq @ TA @ D @ B) & ! [E:TA]: (((ord_less_eq @ TA @ A @ E) & (ord_less @ TA @ E @ D)) => (C @ E)) & ! [E:TA]: ((! [F:TA]: (((ord_less_eq @ TA @ A @ F) & (ord_less @ TA @ F @ E)) => (C @ F))) => (ord_less_eq @ TA @ E @ D))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_complete__interval)).
% 177.75/78.65 thf(963,plain,((! [TA: $tType]: ((condit1037483654norder @ TA) => (! [A:TA,B:TA,C:(TA > $o)]: ((ord_less @ TA @ A @ B) => ((C @ A) => ((~ (C @ B)) => (? [D:TA]: ((ord_less_eq @ TA @ A @ D) & (ord_less_eq @ TA @ D @ B) & ! [E:TA]: (((ord_less_eq @ TA @ A @ E) & (ord_less @ TA @ E @ D)) => (C @ E)) & ! [E:TA]: ((! [F:TA]: (((ord_less_eq @ TA @ A @ F) & (ord_less @ TA @ F @ E)) => (C @ F))) => (ord_less_eq @ TA @ E @ D))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 177.75/78.65 thf(13,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA)]: ((append @ TA @ (append @ TA @ A @ B) @ C) = (append @ TA @ A @ (append @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_append__assoc)).
% 177.75/78.65 thf(319,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA)]: ((append @ TA @ (append @ TA @ A @ B) @ C) = (append @ TA @ A @ (append @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 177.75/78.65 thf(188,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = ((ord_less @ TA @ B @ A) | (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_not__less__iff__gr__or__eq)).
% 177.75/78.65 thf(896,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = ((ord_less @ TA @ B @ A) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 177.75/78.65 thf(1634,plain,(! [A:nat] : (((^ [B:nat]: (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs))) != (^ [B:nat]: (n))) | ((^ [B:nat]: (listIn521021761append @ a @ xs @ f)) != (^ [B:nat]: (f))) | ((^ [B:nat]: (B)) != (^ [B:nat]: (B))) | ((sk25 @ nat @ A) != n) | ((size_size @ (list @ a) @ xs) != A))),inference(simp,[status(thm)],[1629])).
% 177.75/78.65 thf(1639,plain,(((^ [A:nat]: (minus_minus @ nat @ n @ (size_size @ (list @ a) @ xs))) != (^ [A:nat]: (n))) | ((^ [A:nat]: (listIn521021761append @ a @ xs @ f)) != (^ [A:nat]: (f))) | ((sk25 @ nat @ (size_size @ (list @ a) @ xs)) != n)),inference(simp,[status(thm)],[1634])).
% 177.75/78.65 thf(303,plain,(! [TA:$tType,B:TA,A:TA] : ((~ (order @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | ((ord_less_eq @ TA @ B @ A) = (B = A)))),inference(cnf,[status(esa)],[302])).
% 177.75/78.65 thf(304,plain,(! [TA:$tType,B:TA,A:TA] : (((ord_less_eq @ TA @ B @ A) = (B = A)) | (~ (order @ TA)) | (~ (ord_less_eq @ TA @ A @ B)))),inference(lifteq,[status(thm)],[303])).
% 177.75/78.65 thf(242,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_le__less)).
% 177.75/78.65 thf(1101,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 177.75/78.65 thf(23,axiom,((minus @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Groups_Ominus_9)).
% 177.75/78.65 thf(351,plain,((minus @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 177.75/78.65 thf(32,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:(list @ TA)]: ((list_strict_desc @ TA @ A) => (list_desc @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_list__strict__desc__imp__list__desc)).
% 177.75/78.65 thf(390,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:(list @ TA)]: ((list_strict_desc @ TA @ A) => (list_desc @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 177.75/78.65 thf(108,axiom,((! [TA: $tType]: (! [A:nat,B:(list @ TA),C:(list @ TA)]: ((drop @ TA @ A @ (append @ TA @ B @ C)) = (append @ TA @ (drop @ TA @ A @ B) @ (drop @ TA @ (minus_minus @ nat @ A @ (size_size @ (list @ TA) @ B)) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_drop__append)).
% 177.75/78.65 thf(632,plain,((! [TA: $tType]: (! [A:nat,B:(list @ TA),C:(list @ TA)]: ((drop @ TA @ A @ (append @ TA @ B @ C)) = (append @ TA @ (drop @ TA @ A @ B) @ (drop @ TA @ (minus_minus @ nat @ A @ (size_size @ (list @ TA) @ B)) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 177.75/78.65 thf(2606,plain,(! [TA:$tType,A:TA] : (~ (($true)) | (~ (ord_less @ TA @ A @ (sk55 @ TA @ A))) | ((linorder @ nat) != (linorder @ TA)))),inference(paramod_ordered,[status(thm)],[693,848])).
% 177.75/78.65 thf(2607,plain,(! [TA:$tType,A:TA] : ((~ (ord_less @ TA @ A @ (sk55 @ TA @ A))) | ((linorder @ nat) != (linorder @ TA)))),inference(simp,[status(thm)],[2606])).
% 177.75/78.65 thf(2608,plain,(! [A:nat] : ((~ (ord_less @ nat @ A @ (sk55 @ nat @ A))))),inference(pattern_uni,[status(thm)],[2607:[bind_type(TA,$thf(nat))]])).
% 177.75/78.65 thf(119,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (minus_minus @ nat @ A @ C) @ (minus_minus @ nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_diff__le__mono)).
% 177.75/78.65 thf(667,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ (minus_minus @ nat @ A @ C) @ (minus_minus @ nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 177.75/78.65 thf(198,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_order__le__less__subst2)).
% 177.75/78.65 thf(929,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 177.75/78.65 thf(267,axiom,((condit1037483654norder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Conditionally__Complete__Lattices_Oconditionally__complete__linorder)).
% 177.75/78.65 thf(1212,plain,((condit1037483654norder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 177.75/78.65 thf(152,axiom,((! [TA: $tType]: (! [A:nat,B:(nat > (TA > $o))]: ((! [C:nat]: ((ord_less @ nat @ C @ A) => (? [D:TA]: (B @ C @ D)))) = (? [C:(list @ TA)]: (((size_size @ (list @ TA) @ C) = A) & ! [D:nat]: ((ord_less @ nat @ D @ A) => (B @ D @ (nth @ TA @ C @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_Skolem__list__nth)).
% 177.75/78.65 thf(763,plain,((! [TA: $tType]: (! [A:nat,B:(nat > (TA > $o))]: ((! [C:nat]: ((ord_less @ nat @ C @ A) => (? [D:TA]: (B @ C @ D)))) = (? [C:(list @ TA)]: (((size_size @ (list @ TA) @ C) = A) & ! [D:nat]: ((ord_less @ nat @ D @ A) => (B @ D @ (nth @ TA @ C @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 177.75/78.65 thf(189,axiom,((! [TA: $tType]: ((linorder @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (A != C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_le__greater__neq__conv)).
% 177.75/78.65 thf(899,plain,((! [TA: $tType]: ((linorder @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ! [C:TA]: ((ord_less @ TA @ B @ C) => (~ (A = C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 177.75/78.65 thf(164,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_dual__order_Ostrict__trans)).
% 177.75/78.65 thf(800,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 177.75/78.65 thf(194,axiom,((! [A:nat,B:nat,C:nat]: (((minus_minus @ nat @ A @ B) = (minus_minus @ nat @ A @ C)) => ((ord_less @ nat @ C @ A) => (B = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_nat__diff__left__cancel__eq2)).
% 177.75/78.65 thf(914,plain,((! [A:nat,B:nat,C:nat]: (((minus_minus @ nat @ A @ B) = (minus_minus @ nat @ A @ C)) => ((ord_less @ nat @ C @ A) => (B = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 177.75/78.65 thf(173,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA)]: (((size_size @ (list @ TA) @ A) = (size_size @ (list @ TA) @ B)) => ((! [C:nat]: ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => ((nth @ TA @ A @ C) = (nth @ TA @ B @ C)))) => (A = B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_nth__equalityI)).
% 177.75/78.65 thf(832,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA)]: (((size_size @ (list @ TA) @ A) = (size_size @ (list @ TA) @ B)) => ((! [C:nat]: ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => ((nth @ TA @ A @ C) = (nth @ TA @ B @ C)))) => (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 177.75/78.65 thf(53,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oord)).
% 177.75/78.65 thf(447,plain,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 177.75/78.65 thf(47,axiom,((! [TA: $tType]: ((cancel_semigroup_add @ 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_241_add__left__cancel)).
% 177.75/78.65 thf(432,plain,((! [TA: $tType]: ((cancel_semigroup_add @ 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)],[47])).
% 177.75/78.65 thf(275,axiom,((! [TA: $tType]: (! [A:nat,B:(list @ TA),C:(nat > TA)]: ((ord_less @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((listIn521021761append @ TA @ B @ C @ A) = (nth @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_i__append__nth1)).
% 177.75/78.65 thf(1229,plain,((! [TA: $tType]: (! [A:nat,B:(list @ TA),C:(nat > TA)]: ((ord_less @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((listIn521021761append @ TA @ B @ (C) @ A) = (nth @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[275])).
% 177.75/78.65 thf(38,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_linear)).
% 177.75/78.65 thf(405,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 177.75/78.65 thf(252,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(nat > TA),C:(list @ TA),D:(nat > TA)]: (((listIn521021761append @ TA @ A @ B) = (listIn521021761append @ TA @ C @ D)) = (? [E:(list @ TA)]: (((A = (append @ TA @ C @ E)) & ((listIn521021761append @ TA @ E @ B) = D)) | (((append @ TA @ A @ E) = C) & (B = (listIn521021761append @ TA @ E @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_i__append__eq__i__append__conv2)).
% 177.75/78.65 thf(1148,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(nat > TA),C:(list @ TA),D:(nat > TA)]: (((listIn521021761append @ TA @ A @ B) = (listIn521021761append @ TA @ C @ D)) = (? [E:(list @ TA)]: (((A = (append @ TA @ C @ E)) & ((listIn521021761append @ TA @ E @ B) = (D))) | (((append @ TA @ A @ E) = C) & ((B) = (listIn521021761append @ TA @ E @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 177.75/78.65 thf(182,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_less__asym_H)).
% 177.75/78.65 thf(867,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 177.75/78.65 thf(11,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_antisym)).
% 177.75/78.65 thf(315,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 177.75/78.65 thf(1278,plain,(! [TA:$tType,A:TA] : (~ (($true)) | (~ (ord_less @ TA @ A @ A)) | ((preorder @ $o) != (preorder @ TA)))),inference(paramod_ordered,[status(thm)],[301,483])).
% 177.75/78.65 thf(1279,plain,(! [TA:$tType,A:TA] : ((~ (ord_less @ TA @ A @ A)) | ((preorder @ $o) != (preorder @ TA)))),inference(simp,[status(thm)],[1278])).
% 177.75/78.65 thf(1280,plain,(! [A:$o] : ((~ (ord_less @ $o @ A @ A)))),inference(pattern_uni,[status(thm)],[1279:[bind_type(TA,$thf($o))]])).
% 177.75/78.65 thf(68,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ B @ A) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_le__antisym)).
% 177.75/78.65 thf(506,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 177.75/78.65 thf(49,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA)]: ((append @ TA @ (append @ TA @ A @ B) @ C) = (append @ TA @ A @ (append @ TA @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_append_Oassoc)).
% 177.75/78.65 thf(437,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA)]: ((append @ TA @ (append @ TA @ A @ B) @ C) = (append @ TA @ A @ (append @ TA @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 177.75/78.65 thf(118,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => ((ord_less_eq @ nat @ C @ A) => (ord_less @ nat @ (minus_minus @ nat @ A @ C) @ (minus_minus @ nat @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_diff__less__mono)).
% 177.75/78.65 thf(664,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => ((ord_less_eq @ nat @ C @ A) => (ord_less @ nat @ (minus_minus @ nat @ A @ C) @ (minus_minus @ nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 177.75/78.65 thf(172,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_less__imp__neq)).
% 177.75/78.65 thf(828,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 177.75/78.65 thf(1065,plain,(! [TA:$tType] : ((size @ (list @ TA)))),inference(cnf,[status(esa)],[1064])).
% 177.75/78.65 thf(207,axiom,((! [TA: $tType]: ((preorder @ TA) => ((list_asc @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less_eq @ nat @ C @ B) => (ord_less_eq @ TA @ (nth @ TA @ A @ C) @ (nth @ TA @ A @ B)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_list__asc__trans__le)).
% 177.75/78.65 thf(960,plain,((! [TA: $tType]: ((preorder @ TA) => ((list_asc @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ B @ (size_size @ (list @ TA) @ A)) => (! [C:nat]: ((ord_less_eq @ nat @ C @ B) => (ord_less_eq @ TA @ (nth @ TA @ A @ C) @ (nth @ TA @ A @ B)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 177.75/78.65 thf(163,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => ((minus_minus @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ C @ A)) = (minus_minus @ nat @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_Nat_Odiff__diff__eq)).
% 177.75/78.65 thf(796,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ A @ C) => ((minus_minus @ nat @ (minus_minus @ nat @ B @ A) @ (minus_minus @ nat @ C @ A)) = (minus_minus @ nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 177.75/78.65 thf(215,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((A != B) => (ord_less @ nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_le__neq__implies__less)).
% 177.75/78.65 thf(1019,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((~ (A = B)) => (ord_less @ nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 177.75/78.65 thf(209,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (ord_less_eq @ TA @ C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_minf_I6_J)).
% 177.75/78.65 thf(992,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA]: ? [B:TA]: ! [C:TA]: ((ord_less @ TA @ C @ B) => (ord_less_eq @ TA @ C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 177.75/78.65 thf(170,axiom,((! [TA: $tType]: ((preorder @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_less__le__not__le)).
% 177.75/78.65 thf(822,plain,((! [TA: $tType]: ((preorder @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 177.75/78.65 thf(51,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA),D:(list @ TA)]: (((append @ TA @ A @ B) = (append @ TA @ C @ D)) = (? [E:(list @ TA)]: (((A = (append @ TA @ C @ E)) & ((append @ TA @ E @ B) = D)) | (((append @ TA @ A @ E) = C) & (B = (append @ TA @ E @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_append__eq__append__conv2)).
% 177.75/78.65 thf(442,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA),C:(list @ TA),D:(list @ TA)]: (((append @ TA @ A @ B) = (append @ TA @ C @ D)) = (? [E:(list @ TA)]: (((A = (append @ TA @ C @ E)) & ((append @ TA @ E @ B) = D)) | (((append @ TA @ A @ E) = C) & (B = (append @ TA @ E @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 177.75/78.65 thf(102,axiom,((cancel146912293up_add @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Groups_Ocancel__ab__semigroup__add)).
% 177.75/78.65 thf(607,plain,((cancel146912293up_add @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 177.75/78.65 thf(140,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_order_Ostrict__implies__order)).
% 177.75/78.65 thf(728,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 177.75/78.65 thf(144,axiom,((! [TA: $tType]: ((cancel146912293up_add @ TA) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (minus_minus @ TA @ A @ C) @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_diff__right__commute)).
% 177.75/78.65 thf(740,plain,((! [TA: $tType]: ((cancel146912293up_add @ TA) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (minus_minus @ TA @ A @ C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 177.75/78.65 thf(14,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:(list @ TA)]: ((list_strict_asc @ TA @ A) => (list_asc @ TA @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_list__strict__asc__imp__list__asc)).
% 177.75/78.65 thf(322,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:(list @ TA)]: ((list_strict_asc @ TA @ A) => (list_asc @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 177.75/78.65 thf(19,axiom,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ B @ A) & (ord_less_eq @ TA @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_dual__order_Oeq__iff)).
% 177.75/78.65 thf(337,plain,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ B @ A) & (ord_less_eq @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 177.75/78.65 thf(200,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ A @ C) => (ord_less_eq @ TA @ B @ C))) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_dense__ge)).
% 177.75/78.65 thf(935,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ A @ C) => (ord_less_eq @ TA @ B @ C))) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 177.75/78.65 thf(196,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ C @ B) => ((ord_less_eq @ nat @ (minus_minus @ nat @ B @ C) @ A) = (ord_less_eq @ nat @ (minus_minus @ nat @ B @ A) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_le__diff__swap)).
% 177.75/78.65 thf(923,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less_eq @ nat @ C @ B) => ((ord_less_eq @ nat @ (minus_minus @ nat @ B @ C) @ A) = (ord_less_eq @ nat @ (minus_minus @ nat @ B @ A) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 177.75/78.65 thf(156,axiom,((! [TA: $tType]: ((condit1656338222tinuum @ TA) => (! [A:TA]: ? [B:TA]: ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_ex__gt__or__lt)).
% 177.75/78.65 thf(775,plain,((! [TA: $tType]: ((condit1656338222tinuum @ TA) => (! [A:TA]: ? [B:TA]: ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 177.75/78.65 thf(110,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_less__imp__le__nat)).
% 177.75/78.65 thf(639,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 177.75/78.65 thf(63,axiom,((! [TA: $tType]: ((cancel146912293up_add @ TA) => (! [A:TA,B:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ B) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_add__diff__cancel__right_H)).
% 177.75/78.65 thf(491,plain,((! [TA: $tType]: ((cancel146912293up_add @ TA) => (! [A:TA,B:TA]: ((minus_minus @ TA @ (plus_plus @ TA @ A @ B) @ B) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 177.75/78.65 thf(96,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_less__trans)).
% 177.75/78.65 thf(592,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 177.75/78.65 thf(65,axiom,((! [TA: $tType]: ((cancel146912293up_add @ 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_250_add__diff__cancel__right)).
% 177.75/78.65 thf(496,plain,((! [TA: $tType]: ((cancel146912293up_add @ 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)],[65])).
% 177.75/78.65 thf(185,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(nat > TA),C:(list @ TA),D:(nat > TA)]: (((listIn521021761append @ TA @ A @ B) = (listIn521021761append @ TA @ C @ D)) => ((ord_less_eq @ nat @ (size_size @ (list @ TA) @ A) @ (size_size @ (list @ TA) @ C)) => (? [E:(list @ TA)]: (((append @ TA @ A @ E) = C) & (B = (listIn521021761append @ TA @ E @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_i__append__eq__i__append__conv2__aux)).
% 177.75/78.65 thf(882,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(nat > TA),C:(list @ TA),D:(nat > TA)]: (((listIn521021761append @ TA @ A @ B) = (listIn521021761append @ TA @ C @ D)) => ((ord_less_eq @ nat @ (size_size @ (list @ TA) @ A) @ (size_size @ (list @ TA) @ C)) => (? [E:(list @ TA)]: (((append @ TA @ A @ E) = C) & ((B) = (listIn521021761append @ TA @ E @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 177.75/78.65 thf(5615,plain,(($false)),inference(e,[status(thm)],[1036,629,1024,760,347,1237,352,909,1031,777,555,1158,730,1443,994,308,1073,449,677,597,1041,1173,1142,379,1269,440,511,1078,533,550,1164,1327,698,747,945,340,670,1196,782,1046,301,1265,651,724,1264,917,802,357,1132,587,838,902,559,638,289,1232,376,514,1151,806,766,2058,1215,293,411,312,397,687,1104,849,292,942,1199,810,534,1153,761,334,1091,825,302,862,1217,392,424,429,957,1223,561,1666,407,693,467,484,361,879,1687,522,1210,757,324,852,435,1291,710,456,842,519,1270,948,1064,1111,1096,1138,869,783,499,1089,1234,1329,488,933,537,1016,547,1028,1082,686,1075,476,622,1114,997,1099,701,515,738,1192,457,911,721,1246,1333,343,1086,805,311,541,1170,1071,1167,794,586,662,718,888,906,298,750,1251,425,513,573,296,601,1135,412,819,694,402,843,772,743,711,1226,584,1154,579,291,641,445,2029,313,787,713,1092,704,1638,540,604,1209,681,736,451,318,599,509,649,1043,387,631,594,483,626,769,1022,494,1080,848,700,399,1245,1066,780,608,394,563,1000,1250,505,653,658,1213,768,2022,299,473,1034,675,1304,531,939,1145,355,754,553,1049,1203,589,927,2037,1003,690,295,707,414,327,954,409,673,791,331,1038,502,1262,1317,1658,808,1220,544,336,1221,864,1094,571,612,2584,1240,656,1023,845,1316,482,891,1108,1448,1189,1326,963,319,896,1639,304,1101,351,390,632,2608,1244,667,929,1212,763,899,800,290,914,378,832,684,300,447,432,1229,405,1148,867,315,1280,422,790,305,506,437,664,828,1065,960,635,796,283,1019,992,822,442,607,728,740,322,337,1653,935,923,309,775,639,491,592,496,882])).
% 177.75/78.65 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 177.75/78.65 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------