Leo-III---1.8.0.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : ITP102^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 : n026.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:46 AM UTC 2026

% Result   : Theorem 210.34s 123.66s
% Output   : Refutation 197.98s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP102^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21  % Computer : n026.cluster.edu
% 0.10/0.21  % Model    : x86_64 x86_64
% 0.10/0.21  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21  % Memory   : 8046.5625MB
% 0.10/0.21  % OS       : Linux 6.8.0-71-generic
% 0.10/0.21  % CPULimit : 300
% 0.10/0.21  % WCLimit  : 300
% 0.10/0.21  % DateTime : Tue Sep 29 19:56:27 UTC 2026
% 0.10/0.21  % CPUTime  : 
% 0.10/0.21  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.64/0.53  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 2.02/0.99  % [INFO] 	 Parsing done (451ms). 
% 2.02/1.01  % [INFO] 	 Running in sequential loop mode. 
% 3.91/1.59  % [INFO] 	 eprover registered as external prover. 
% 3.91/1.60  % [INFO] 	 Scanning for conjecture ... 
% 4.35/1.76  % [INFO] 	 Found a conjecture (or negated_conjecture) and 273 axioms. Running axiom selection ... 
% 4.93/1.93  % [INFO] 	 Axiom selection finished. Selected 272 axioms (removed 1 axioms). 
% 5.86/2.28  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 6.22/2.32  % [INFO] 	 Type checking passed. 
% 6.22/2.32  % [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 ... 
% 210.34/123.65  % External prover 'e' found a proof!
% 210.34/123.65  % [INFO] 	 Killing All external provers ... 
% 210.34/123.65  % Time passed: 123352ms (effective reasoning time: 122634ms)
% 210.34/123.65  % 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)>
% 210.34/123.65  % Axioms used in derivation (272): fact_209_Ex__less__Suc, fact_160_minf_I2_J, fact_50_linorder__cases, fact_241_nat__diff__left__cancel__eq2, fact_109_order_Ostrict__trans1, fact_98_dual__order_Ostrict__implies__order, fact_20_order__class_Oorder_Oantisym, fact_119_antisym__conv2, tcon_HOL_Obool___Orderings_Opreorder_4, fact_133_list__asc__trans__le, fact_7_length__induct, fact_104_dual__order_Ostrict__trans2, fact_199_not__less__less__Suc__eq, fact_53_antisym__conv3, fact_124_order__less__le__subst2, fact_6_list__desc__trans__le, fact_85_less__not__refl, fact_32_ord__le__eq__subst, fact_59_ord__eq__less__trans, tcon_Nat_Onat___Orderings_Oorder_2, tcon_Nat_Onat___Orderings_Ono__top, fact_148_ge__less__neq__conv, fact_234_diff__Suc__Suc, fact_100_dual__order_Oorder__iff__strict, fact_28_eq__refl, fact_228_Suc__leI, fact_111_less__le__not__le, tcon_Nat_Onat___Nat_Osize, fact_153_pinf_I2_J, fact_131_leD, fact_121_le__neq__trans, tcon_Nat_Onat___Orderings_Olinorder, fact_247_less__imp__diff__less, fact_125_order__less__le__subst1, fact_185_length__rev, fact_60_less__irrefl, tcon_Nat_Onat___Conditionally__Complete__Lattices_Oconditionally__complete__linorder, fact_252_diff__le__mono, fact_230_nat__induct_H, fact_163_minf_I5_J, fact_106_order_Ostrict__iff__order, fact_144_list__strict__asc__imp__list__asc, tcon_HOL_Obool___Orderings_Olinorder_5, fact_1_i__append__nth1, fact_205_Suc__less__eq2, tcon_List_Olist___Nat_Osize_8, fact_41_order_Ostrict__implies__not__eq, fact_164_minf_I7_J, fact_83_less__not__refl3, fact_4_list__eq__iff__nth__eq, fact_168_sorted__iff__nth__mono, fact_216_lift__Suc__mono__less__iff, fact_197_Suc__inject, fact_123_not__le, tcon_fun___Orderings_Oord, fact_250_le__diff__iff_H, fact_233_Suc__diff__diff, fact_225_inc__induct, fact_208_less__Suc__eq, fact_236_list__ex__rev, fact_3_Skolem__list__nth, fact_128_less__le, fact_137_Lattices__Big_Oex__has__greatest__nat, fact_68_neq__iff, fact_39_le__funD, fact_139_complete__interval, fact_54_less__induct, fact_248_diff__commute, fact_76_measure__induct__rule, fact_237_i__append__nth2, fact_145_ex__gt__or__lt, fact_186_Suc__leD, fact_218_lift__Suc__antimono__le, fact_235_diff__diff__cancel, fact_81_nat__less__induct, fact_2_nth__equalityI, fact_65_less__imp__neq, fact_17_linorder__wlog, fact_146_ex__has__least__nat, fact_207_not__less__eq, fact_11_less__or__eq__imp__le, fact_112_le__imp__less__or__eq, fact_194_nat__induct__at__least, fact_173_sorted__iff__nth__mono__less, fact_31_eq__iff, fact_170_list__ord__le__sorted__eq, fact_69_neqE, fact_202_less__trans__Suc, fact_138_nat__descend__induct, fact_212_Suc__lessI, fact_238_zero__induct__lemma, fact_198_rev__swap, fact_201_less__Suc__induct, fact_88_nat__le__linear, fact_22_ord__eq__le__trans, fact_71_lt__ex, fact_117_le__less__trans, fact_183_lessI, fact_55_less__not__sym, fact_147_list__strict__desc__imp__list__desc, fact_34_order__subst2, fact_58_ord__less__eq__trans, fact_246_diff__less__mono2, fact_25_le__cases3, fact_113_le__less__linear, fact_27_le__cases, fact_167_verit__comp__simplify1_I3_J, fact_210_less__SucI, fact_44_linorder__less__wlog, fact_26_order_Otrans, fact_47_less__imp__not__less, fact_136_list__asc__trans, fact_66_dense, fact_80_infinite__descent, fact_51_less__imp__triv, fact_254_le__diff__iff, fact_227_Suc__le__eq, fact_61_less__linear, fact_52_less__imp__not__eq2, fact_244_nat__diff__right__cancel__eq2, fact_10_le__eq__less__or__eq, fact_149_minf_I8_J, fact_35_order__subst1, fact_239_less__diff__imp__less, fact_118_less__imp__le, fact_157_pinf_I7_J, tcon_HOL_Obool___Orderings_Oorder_6, fact_93_size__neq__size__imp__neq, fact_48_order_Ostrict__trans, fact_154_pinf_I3_J, fact_115_dense__ge, fact_180_rev__rev__ident, fact_221_less__eq__Suc__le, fact_9_less__imp__le__nat, fact_219_lift__Suc__mono__le, fact_14_dual__order_Oantisym, fact_90_eq__imp__le, fact_141_greater__le__neq__conv, fact_92_le__refl, fact_56_less__imp__not__eq, fact_96_list__desc__trans, tcon_Nat_Onat___Orderings_Owellorder, fact_82_less__irrefl__nat, fact_162_minf_I4_J, fact_33_ord__eq__le__subst, fact_77_measure__induct, fact_190_le__Suc__eq, fact_15_dual__order_Oeq__iff, fact_114_dense__le, fact_204_less__antisym, fact_127_order__le__less__subst1, fact_49_dual__order_Oirrefl, fact_63_less__asym_H, fact_91_le__trans, fact_193_full__nat__induct, fact_23_order__class_Oorder_Oeq__iff, fact_13_less__mono__imp__le__mono, fact_184_Suc__le__mono, fact_107_order_Oorder__iff__strict, fact_223_le__less__Suc__eq, fact_72_order__less__subst2, fact_169_sorted__nth__mono, fact_110_not__le__imp__less, fact_150_minf_I6_J, tcon_Nat_Onat___Orderings_Oord_3, fact_57_dual__order_Oasym, fact_5_order__refl, fact_86_nat__neq__iff, fact_62_less__trans, fact_222_less__Suc__eq__le, fact_226_dec__induct, fact_12_le__neq__implies__less, fact_213_Suc__lessE, fact_42_not__less__iff__gr__or__eq, fact_101_order_Ostrict__implies__order, fact_142_less__ge__neq__conv, fact_43_dual__order_Ostrict__trans, fact_79_linorder__neqE__nat, fact_174_sorted__rev__nth__mono, fact_192_not__less__eq__eq, fact_158_pinf_I11_J, fact_177_old_Onat_Oinject, fact_195_transitive__stepwise__le, fact_203_Suc__less__SucD, fact_29_linear, fact_36_le__fun__def, fact_132_list__strict__asc__trans__le, fact_103_dense__ge__bounded, fact_161_minf_I3_J, fact_232_list__ex__length, tcon_HOL_Obool___Orderings_Oord_7, fact_84_less__not__refl2, fact_19_order__trans, fact_245_nat__diff__right__cancel__less, fact_191_Suc__n__not__le__n, fact_181_Suc__less__eq, fact_214_Suc__lessD, fact_196_n__not__Suc__n, fact_21_ord__le__eq__trans, fact_224_Suc__le__lessD, fact_220_le__imp__less__Suc, fact_143_less__fun__def, fact_30_antisym, fact_187_le__SucE, fact_73_order__less__subst1, fact_151_pinf_I8_J, conj_1, fact_116_less__le__trans, fact_8_nat__less__le, tcon_fun___Orderings_Opreorder, fact_40_dual__order_Ostrict__implies__not__eq, fact_242_nat__diff__left__cancel__less, fact_178_nat_Oinject, fact_24_antisym__conv, fact_140_le__greater__neq__conv, fact_249_diff__le__mono2, fact_189_Suc__le__D, fact_182_Suc__mono, fact_74_ord__less__eq__subst, fact_165_minf_I11_J, fact_229_sorted__rev__iff__nth__Suc, fact_129_le__less, fact_179_rev__is__rev__conv, fact_105_dual__order_Ostrict__trans1, fact_166_pinf_I6_J, fact_64_less__asym, tcon_Nat_Onat___Orderings_Opreorder_1, fact_155_pinf_I4_J, fact_102_dense__le__bounded, fact_70_gt__ex, fact_159_minf_I1_J, fact_108_order_Ostrict__trans2, fact_206_All__less__Suc, fact_97_order_Onot__eq__order__implies__strict, fact_231_rev__nth, fact_67_order_Oasym, tcon_fun___Orderings_Oorder, fact_16_dual__order_Otrans, fact_37_le__funI, fact_156_pinf_I5_J, fact_240_nat__diff__left__cancel__eq1, fact_134_list__strict__desc__trans, fact_188_le__SucI, fact_126_order__le__less__subst2, fact_211_less__SucE, fact_18_dual__order_Orefl, fact_200_strict__inc__induct, fact_176_sorted__iff__nth__Suc, fact_46_exists__least__iff, fact_215_Nat_OlessE, fact_135_list__strict__asc__trans, fact_120_antisym__conv1, fact_75_ord__eq__less__subst, fact_78_infinite__descent__measure, fact_38_le__funE, fact_243_nat__diff__right__cancel__eq1, conj_0, fact_171_verit__la__disequality, fact_0_i__append__eq__i__append__conv, fact_253_Nat_Odiff__diff__eq, fact_87_Nat_Oex__has__greatest__nat, fact_89_le__antisym, fact_251_diff__le__self, fact_175_sorted__rev__iff__nth__mono, fact_99_dual__order_Ostrict__iff__order, fact_172_verit__comp__simplify1_I1_J, fact_122_not__less, fact_95_Ex__list__of__length, fact_94_neq__if__length__neq, fact_152_pinf_I1_J, fact_217_lift__Suc__mono__less, fact_130_leI
% 210.34/123.65  % No. of inferences in proof: 612
% 210.34/123.66  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 123352 ms resp. 122634 ms w/o parsing
% 197.98/123.90  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 197.98/123.90  thf(nat_type, type, nat: $tType).
% 197.98/123.90  thf(a_type, type, a: $tType).
% 197.98/123.90  thf(size_decl, type, size: !> [TA: $tType]: $o).
% 197.98/123.90  thf(ord_decl, type, ord: !> [TA: $tType]: $o).
% 197.98/123.90  thf(order_decl, type, order: !> [TA: $tType]: $o).
% 197.98/123.90  thf(no_bot_decl, type, no_bot: !> [TA: $tType]: $o).
% 197.98/123.90  thf(no_top_decl, type, no_top: !> [TA: $tType]: $o).
% 197.98/123.90  thf(linorder_decl, type, linorder: !> [TA: $tType]: $o).
% 197.98/123.90  thf(preorder_decl, type, preorder: !> [TA: $tType]: $o).
% 197.98/123.90  thf(wellorder_decl, type, wellorder: !> [TA: $tType]: $o).
% 197.98/123.90  thf(dense_order_decl, type, dense_order: !> [TA: $tType]: $o).
% 197.98/123.90  thf(dense_linorder_decl, type, dense_linorder: !> [TA: $tType]: $o).
% 197.98/123.90  thf(condit1656338222tinuum_decl, type, condit1656338222tinuum: !> [TA: $tType]: $o).
% 197.98/123.90  thf(condit1037483654norder_decl, type, condit1037483654norder: !> [TA: $tType]: $o).
% 197.98/123.90  thf(minus_minus_decl, type, minus_minus: !> [TA: $tType]: (TA > (TA > TA))).
% 197.98/123.90  thf(list_asc_decl, type, list_asc: !> [TA: $tType]: ((list @ TA) > $o)).
% 197.98/123.90  thf(list_desc_decl, type, list_desc: !> [TA: $tType]: ((list @ TA) > $o)).
% 197.98/123.90  thf(list_strict_asc_decl, type, list_strict_asc: !> [TA: $tType]: ((list @ TA) > $o)).
% 197.98/123.90  thf(list_strict_desc_decl, type, list_strict_desc: !> [TA: $tType]: ((list @ TA) > $o)).
% 197.98/123.90  thf(listIn521021761append_decl, type, listIn521021761append: !> [TA: $tType]: ((list @ TA) > ((nat > TA) > (nat > TA)))).
% 197.98/123.90  thf(linorder_sorted_decl, type, linorder_sorted: !> [TA: $tType]: ((list @ TA) > $o)).
% 197.98/123.90  thf(list_ex_decl, type, list_ex: !> [TA: $tType]: ((TA > $o) > ((list @ TA) > $o))).
% 197.98/123.90  thf(nth_decl, type, nth: !> [TA: $tType]: ((list @ TA) > (nat > TA))).
% 197.98/123.90  thf(rev_decl, type, rev: !> [TA: $tType]: ((list @ TA) > (list @ TA))).
% 197.98/123.90  thf(suc_decl, type, suc: (nat > nat)).
% 197.98/123.90  thf(size_size_decl, type, size_size: !> [TA: $tType]: (TA > nat)).
% 197.98/123.90  thf(ord_less_decl, type, ord_less: !> [TA: $tType]: (TA > (TA > $o))).
% 197.98/123.90  thf(ord_less_eq_decl, type, ord_less_eq: !> [TA: $tType]: (TA > (TA > $o))).
% 197.98/123.90  thf(f_decl, type, f: (nat > a)).
% 197.98/123.90  thf(g_decl, type, g: (nat > a)).
% 197.98/123.90  thf(xs_decl, type, xs: (list @ a)).
% 197.98/123.90  thf(ys_decl, type, ys: (list @ a)).
% 197.98/123.90  thf(sk1_decl, type, sk1: nat).
% 197.98/123.90  thf(sk2_decl, type, sk2: !> [TA: $tType,TB: $tType]: (TB > ((TA > TB) > (TA > (TA > TA))))).
% 197.98/123.90  thf(sk3_decl, type, sk3: !> [TA: $tType,TB: $tType]: (TB > ((TA > TB) > (TA > (TA > TA))))).
% 197.98/123.90  thf(sk1_def, definition, sk1 = (@+ [A:nat]: ~ (~ (ord_less @ nat @ A @ (size_size @ (list @ a) @ xs)) | ((nth @ a @ xs @ A) = (nth @ a @ ys @ A)))) ).
% 197.98/123.90  thf(sk2_def, definition, sk2 = (^ [TA: $tType,TB: $tType]: (^ [A:TB,B:(TA > TB),C:TA,D:TA]: (@+ [E:TA]: ~ (! [F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F))))))) ).
% 197.98/123.90  thf(sk3_def, definition, sk3 = (^ [TA: $tType,TB: $tType]: (^ [A:TB,B:(TA > TB),C:TA,D:TA]: (@+ [E:TA]: ~ ((ord_less_eq @ TA @ (sk2 @ TB @ TA @ A @ B @ C @ D) @ E) => (ord_less_eq @ TB @ (B @ (sk2 @ TB @ TA @ A @ B @ C @ D)) @ (B @ E)))))) ).
% 197.98/123.90  thf(105,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_159_minf_I1_J)).
% 197.98/123.90  thf(645,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)],[105])).
% 197.98/123.90  thf(100,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_50_linorder__cases)).
% 197.98/123.90  thf(629,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)],[100])).
% 197.98/123.90  thf(27,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_171_verit__la__disequality)).
% 197.98/123.90  thf(365,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)],[27])).
% 197.98/123.90  thf(159,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_42_not__less__iff__gr__or__eq)).
% 197.98/123.90  thf(846,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)],[159])).
% 197.98/123.90  thf(188,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_94_neq__if__length__neq)).
% 197.98/123.90  thf(962,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)],[188])).
% 197.98/123.90  thf(246,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_155_pinf_I4_J)).
% 197.98/123.90  thf(1179,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)],[246])).
% 197.98/123.90  thf(230,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_73_order__less__subst1)).
% 197.98/123.90  thf(1110,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)],[230])).
% 197.98/123.90  thf(243,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_93_size__neq__size__imp__neq)).
% 197.98/123.90  thf(1168,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)],[243])).
% 197.98/123.90  thf(134,axiom,((! [TA: $tType]: (! [A:nat]: ? [B:(list @ TA)]: ((size_size @ (list @ TA) @ B) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_Ex__list__of__length)).
% 197.98/123.90  thf(760,plain,((! [TA: $tType]: (! [A:nat]: ? [B:(list @ TA)]: ((size_size @ (list @ TA) @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 197.98/123.90  thf(59,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_134_list__strict__desc__trans)).
% 197.98/123.90  thf(479,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)],[59])).
% 197.98/123.90  thf(228,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:(nat > TA),B:nat,C:nat]: ((! [D:nat]: (ord_less @ TA @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less @ nat @ B @ C) => (ord_less @ TA @ (A @ B) @ (A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_lift__Suc__mono__less)).
% 197.98/123.90  thf(1105,plain,((! [TA: $tType]: ((order @ TA) => (! [A:(nat > TA),B:nat,C:nat]: ((! [D:nat]: (ord_less @ TA @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less @ nat @ B @ C) => (ord_less @ TA @ (A @ B) @ (A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 197.98/123.90  thf(250,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ (suc @ B)) => ((~ (ord_less @ nat @ A @ B)) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_less__SucE)).
% 197.98/123.90  thf(1211,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ (suc @ B)) => ((~ (ord_less @ nat @ A @ B)) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 197.98/123.90  thf(242,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_152_pinf_I1_J)).
% 197.98/123.90  thf(1158,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)],[242])).
% 197.98/123.90  thf(201,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_103_dense__ge__bounded)).
% 197.98/123.90  thf(1005,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)],[201])).
% 197.98/123.90  thf(96,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_131_leD)).
% 197.98/123.90  thf(614,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)],[96])).
% 197.98/123.90  thf(122,axiom,((linorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Olinorder)).
% 197.98/123.90  thf(730,plain,((linorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 197.98/123.90  thf(270,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_118_less__imp__le)).
% 197.98/123.90  thf(1290,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)],[270])).
% 197.98/123.90  thf(165,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_86_nat__neq__iff)).
% 197.98/123.90  thf(878,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)],[165])).
% 197.98/123.90  thf(106,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_47_less__imp__not__less)).
% 197.98/123.90  thf(655,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)],[106])).
% 197.98/123.90  thf(218,axiom,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (minus_minus @ nat @ (suc @ A) @ B) @ (suc @ C)) = (minus_minus @ nat @ (minus_minus @ nat @ A @ B) @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_Suc__diff__diff)).
% 197.98/123.90  thf(1078,plain,((! [A:nat,B:nat,C:nat]: ((minus_minus @ nat @ (minus_minus @ nat @ (suc @ A) @ B) @ (suc @ C)) = (minus_minus @ nat @ (minus_minus @ nat @ A @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 197.98/123.90  thf(34,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) => (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_Suc__inject)).
% 197.98/123.90  thf(384,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) => (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 197.98/123.90  thf(240,axiom,((! [TA: $tType]: (! [A:(list @ TA)]: ((size_size @ (list @ TA) @ (rev @ TA @ A)) = (size_size @ (list @ TA) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_length__rev)).
% 197.98/123.90  thf(1137,plain,((! [TA: $tType]: (! [A:(list @ TA)]: ((size_size @ (list @ TA) @ (rev @ TA @ A)) = (size_size @ (list @ TA) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 197.98/123.90  thf(76,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_12_le__neq__implies__less)).
% 197.98/123.90  thf(533,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)],[76])).
% 197.98/123.90  thf(66,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_250_le__diff__iff_H)).
% 197.98/123.90  thf(500,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)],[66])).
% 197.98/123.90  thf(174,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_156_pinf_I5_J)).
% 197.98/123.90  thf(913,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)],[174])).
% 197.98/123.90  thf(254,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ B) => (ord_less @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_Suc__le__lessD)).
% 197.98/123.90  thf(1222,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ B) => (ord_less @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 197.98/123.90  thf(153,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_148_ge__less__neq__conv)).
% 197.98/123.90  thf(829,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)],[153])).
% 197.98/123.90  thf(192,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_13_less__mono__imp__le__mono)).
% 197.98/123.90  thf(973,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)],[192])).
% 197.98/123.90  thf(6,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_32_ord__le__eq__subst)).
% 197.98/123.90  thf(288,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)],[6])).
% 197.98/123.90  thf(83,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_dual__order_Oirrefl)).
% 197.98/123.90  thf(564,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 197.98/123.90  thf(565,plain,(! [TA:$tType,A:TA] : ((~ (order @ TA)) | (~ (ord_less @ TA @ A @ A)))),inference(cnf,[status(esa)],[564])).
% 197.98/123.90  thf(262,axiom,((condit1037483654norder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Conditionally__Complete__Lattices_Oconditionally__complete__linorder)).
% 197.98/123.90  thf(1254,plain,((condit1037483654norder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 197.98/123.90  thf(260,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_146_ex__has__least__nat)).
% 197.98/123.90  thf(1243,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)],[260])).
% 197.98/123.90  thf(236,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_43_dual__order_Ostrict__trans)).
% 197.98/123.90  thf(1127,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)],[236])).
% 197.98/123.90  thf(35,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_14_dual__order_Oantisym)).
% 197.98/123.90  thf(389,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)],[35])).
% 197.98/123.90  thf(269,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_133_list__asc__trans__le)).
% 197.98/123.90  thf(1287,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)],[269])).
% 197.98/123.90  thf(67,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_113_le__less__linear)).
% 197.98/123.90  thf(504,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)],[67])).
% 197.98/123.90  thf(113,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_129_le__less)).
% 197.98/123.90  thf(702,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)],[113])).
% 197.98/123.90  thf(147,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_145_ex__gt__or__lt)).
% 197.98/123.90  thf(802,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)],[147])).
% 197.98/123.90  thf(78,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_244_nat__diff__right__cancel__eq2)).
% 197.98/123.90  thf(542,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)],[78])).
% 197.98/123.90  thf(87,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_119_antisym__conv2)).
% 197.98/123.90  thf(587,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)],[87])).
% 197.98/123.90  thf(1,conjecture,((! [A:nat]: (~ (ord_less @ nat @ A @ (size_size @ (list @ a) @ xs)) | ((nth @ a @ xs @ A) = (nth @ a @ ys @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_2)).
% 197.98/123.90  thf(2,negated_conjecture,((~ (! [A:nat]: (~ (ord_less @ nat @ A @ (size_size @ (list @ a) @ xs)) | ((nth @ a @ xs @ A) = (nth @ a @ ys @ A)))))),inference(neg_conjecture,[status(cth)],[1])).
% 197.98/123.90  thf(275,plain,((~ (! [A:nat]: (~ (ord_less @ nat @ A @ (size_size @ (list @ a) @ xs)) | ((nth @ a @ xs @ A) = (nth @ a @ ys @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 197.98/123.90  thf(276,plain,(((ord_less @ nat @ sk1 @ (size_size @ (list @ a) @ xs)) & ~ ((nth @ a @ xs @ sk1) = (nth @ a @ ys @ sk1)))),inference(cnf,[status(esa)],[275])).
% 197.98/123.90  thf(277,plain,((ord_less @ nat @ sk1 @ (size_size @ (list @ a) @ xs))),inference(cnfConj,[status(thm)],[276])).
% 197.98/123.90  thf(63,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_less__not__refl2)).
% 197.98/123.90  thf(488,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 197.98/123.90  thf(489,plain,(! [B:nat,A:nat] : ((~ (ord_less @ nat @ A @ B)) | (~ (B = A)))),inference(cnf,[status(esa)],[488])).
% 197.98/123.90  thf(490,plain,(! [B:nat,A:nat] : ((B != A) | (~ (ord_less @ nat @ A @ B)))),inference(lifteq,[status(thm)],[489])).
% 197.98/123.90  thf(491,plain,(! [A:nat] : ((~ (ord_less @ nat @ A @ A)))),inference(simp,[status(thm)],[490])).
% 197.98/123.90  thf(1320,plain,(! [A:nat] : (~ (($true)) | ((ord_less @ nat @ sk1 @ (size_size @ (list @ a) @ xs)) != (ord_less @ nat @ A @ A)))),inference(paramod_ordered,[status(thm)],[277,491])).
% 197.98/123.90  thf(1321,plain,(! [A:nat] : (((ord_less @ nat @ sk1 @ (size_size @ (list @ a) @ xs)) != (ord_less @ nat @ A @ A)))),inference(simp,[status(thm)],[1320])).
% 197.98/123.90  thf(1322,plain,(! [A:nat] : ((sk1 != A) | ((size_size @ (list @ a) @ xs) != A))),inference(simp,[status(thm)],[1321])).
% 197.98/123.90  thf(1323,plain,((sk1 != (size_size @ (list @ a) @ xs))),inference(simp,[status(thm)],[1322])).
% 197.98/123.90  thf(179,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_126_order__le__less__subst2)).
% 197.98/123.90  thf(934,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)],[179])).
% 197.98/123.90  thf(25,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_17_linorder__wlog)).
% 197.98/123.90  thf(357,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)],[25])).
% 197.98/123.90  thf(102,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ B) => (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_Suc__leD)).
% 197.98/123.90  thf(638,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ B) => (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 197.98/123.90  thf(221,axiom,(((ord_less @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_nat__less__le)).
% 197.98/123.90  thf(1087,plain,(((ord_less @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 197.98/123.90  thf(46,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oord)).
% 197.98/123.90  thf(421,plain,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 197.98/123.90  thf(5,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_21_ord__le__eq__trans)).
% 197.98/123.90  thf(284,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)],[5])).
% 197.98/123.90  thf(93,axiom,(((ord_less @ nat) = (^ [A:nat]: (ord_less_eq @ nat @ (suc @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_less__eq__Suc__le)).
% 197.98/123.90  thf(606,plain,(((ord_less @ nat) = (^ [A:nat]: (ord_less_eq @ nat @ (suc @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 197.98/123.90  thf(266,axiom,((order @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oorder_2)).
% 197.98/123.90  thf(1280,plain,((order @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 197.98/123.90  thf(4,axiom,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder)).
% 197.98/123.90  thf(282,plain,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 197.98/123.90  thf(283,plain,(! [TA:$tType,TB:$tType] : ((~ (order @ TB)) | (order @ (TA > TB)))),inference(cnf,[status(esa)],[282])).
% 197.98/123.90  thf(1333,plain,(! [TA:$tType,TB:$tType] : (~ (($true)) | (order @ (TA > TB)) | ((order @ nat) != (order @ TB)))),inference(paramod_ordered,[status(thm)],[1280,283])).
% 197.98/123.90  thf(1334,plain,(! [TA:$tType,TB:$tType] : ((order @ (TA > TB)) | ((order @ nat) != (order @ TB)))),inference(simp,[status(thm)],[1333])).
% 197.98/123.90  thf(1335,plain,(! [TA:$tType] : ((order @ (TA > nat)))),inference(pattern_uni,[status(thm)],[1334:[bind_type(TA,$thf(TA)),bind_type(TB,$thf(nat))]])).
% 197.98/123.90  thf(1339,plain,(! [TA:$tType,TB:$tType,TC:$tType] : (~ (($true)) | (order @ (TB > TC)) | ((order @ (TA > nat)) != (order @ TC)))),inference(paramod_ordered,[status(thm)],[1335,283])).
% 197.98/123.90  thf(1340,plain,(! [TA:$tType,TB:$tType,TC:$tType] : ((order @ (TB > TC)) | ((order @ (TA > nat)) != (order @ TC)))),inference(simp,[status(thm)],[1339])).
% 197.98/123.90  thf(1341,plain,(! [TA:$tType,TB:$tType] : ((order @ (TB > (TA > nat))))),inference(pattern_uni,[status(thm)],[1340:[bind_type(TA,$thf(TA)),bind_type(TB,$thf(TB)),bind_type(TC,$thf((TA > nat)))]])).
% 197.98/123.90  thf(1345,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType] : (~ (($true)) | (order @ (TC > TD)) | ((order @ (TB > (TA > nat))) != (order @ TD)))),inference(paramod_ordered,[status(thm)],[1341,283])).
% 197.98/123.90  thf(1346,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType] : ((order @ (TC > TD)) | ((order @ (TB > (TA > nat))) != (order @ TD)))),inference(simp,[status(thm)],[1345])).
% 197.98/123.90  thf(1347,plain,(! [TA:$tType,TB:$tType,TC:$tType] : ((order @ (TC > (TB > (TA > nat)))))),inference(pattern_uni,[status(thm)],[1346:[bind_type(TA,$thf(TA)),bind_type(TB,$thf(TB)),bind_type(TC,$thf(TC)),bind_type(TD,$thf((TB > (TA > nat))))]])).
% 197.98/123.90  thf(166,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ B) = (ord_less @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_Suc__le__eq)).
% 197.98/123.90  thf(881,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ B) = (ord_less @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 197.98/123.90  thf(43,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_24_antisym__conv)).
% 197.98/123.90  thf(416,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)],[43])).
% 197.98/123.90  thf(64,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_76_measure__induct__rule)).
% 197.98/123.90  thf(492,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)],[64])).
% 197.98/123.90  thf(132,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_110_not__le__imp__less)).
% 197.98/123.90  thf(756,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)],[132])).
% 197.98/123.90  thf(143,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA)]: ((linorder_sorted @ TA @ (rev @ TA @ A)) = (! [B:nat]: ((ord_less @ nat @ (suc @ B) @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ (suc @ B)) @ (nth @ TA @ A @ B))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_sorted__rev__iff__nth__Suc)).
% 197.98/123.90  thf(789,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA)]: ((linorder_sorted @ TA @ (rev @ TA @ A)) = (! [B:nat]: ((ord_less @ nat @ (suc @ B) @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ (suc @ B)) @ (nth @ TA @ A @ B))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 197.98/123.90  thf(16,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_29_linear)).
% 197.98/123.90  thf(321,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)],[16])).
% 197.98/123.90  thf(247,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_246_diff__less__mono2)).
% 197.98/123.90  thf(1183,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)],[247])).
% 197.98/123.90  thf(23,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_order__refl)).
% 197.98/123.90  thf(353,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 197.98/123.90  thf(189,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_132_list__strict__asc__trans__le)).
% 197.98/123.90  thf(966,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)],[189])).
% 197.98/123.90  thf(194,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_53_antisym__conv3)).
% 197.98/123.90  thf(981,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)],[194])).
% 197.98/123.90  thf(38,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_38_le__funE)).
% 197.98/123.90  thf(397,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)],[38])).
% 197.98/123.90  thf(3,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_147_list__strict__desc__imp__list__desc)).
% 197.98/123.90  thf(280,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)],[3])).
% 197.98/123.90  thf(110,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_less__imp__not__eq2)).
% 197.98/123.90  thf(692,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 197.98/123.90  thf(124,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_97_order_Onot__eq__order__implies__strict)).
% 197.98/123.90  thf(734,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)],[124])).
% 197.98/123.90  thf(198,axiom,((! [A:nat]: (ord_less @ nat @ A @ (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_lessI)).
% 197.98/123.90  thf(998,plain,((! [A:nat]: (ord_less @ nat @ A @ (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 197.98/123.90  thf(41,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_20_order__class_Oorder_Oantisym)).
% 197.98/123.90  thf(411,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)],[41])).
% 197.98/123.90  thf(49,axiom,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_gt__ex)).
% 197.98/123.90  thf(428,plain,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 197.98/123.90  thf(160,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => ((B != (suc @ A)) => (~ (! [C:nat]: ((ord_less @ nat @ A @ C) => (B != (suc @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_Nat_OlessE)).
% 197.98/123.90  thf(849,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => ((~ (B = (suc @ A))) => (~ (! [C:nat]: ((ord_less @ nat @ A @ C) => (~ (B = (suc @ C)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 197.98/123.90  thf(12,axiom,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_fun___Orderings_Opreorder)).
% 197.98/123.90  thf(312,plain,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 197.98/123.90  thf(289,plain,(! [TA:$tType,TB:$tType,D:TB,C:(TA > TB),B:TA,A:TA] : (((~ (ord @ TB) | ~ (ord @ TA) | ~ (ord_less_eq @ TA @ A @ B) | ~ ((C @ B) = D) | (ord_less_eq @ TA @ (sk2 @ TB @ TA @ D @ (C) @ B @ A) @ (sk3 @ TB @ TA @ D @ (C) @ B @ A)) | (ord_less_eq @ TB @ (C @ A) @ D)) & (~ (ord @ TB) | ~ (ord @ TA) | ~ (ord_less_eq @ TA @ A @ B) | ~ ((C @ B) = D) | ~ (ord_less_eq @ TB @ (C @ (sk2 @ TB @ TA @ D @ (C) @ B @ A)) @ (C @ (sk3 @ TB @ TA @ D @ (C) @ B @ A))) | (ord_less_eq @ TB @ (C @ A) @ D))))),inference(cnf,[status(esa)],[288])).
% 197.98/123.90  thf(290,plain,(! [TA:$tType,TB:$tType,D:TB,C:(TA > TB),B:TA,A:TA] : ((~ (ord @ TB)) | (~ (ord @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (~ ((C @ B) = D)) | (ord_less_eq @ TA @ (sk2 @ TB @ TA @ D @ (C) @ B @ A) @ (sk3 @ TB @ TA @ D @ (C) @ B @ A)) | (ord_less_eq @ TB @ (C @ A) @ D))),inference(cnfConj,[status(thm)],[289])).
% 197.98/123.90  thf(292,plain,(! [TA:$tType,TB:$tType,D:TB,C:(TA > TB),B:TA,A:TA] : (((C @ B) != D) | (~ (ord @ TB)) | (~ (ord @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (ord_less_eq @ TA @ (sk2 @ TB @ TA @ D @ (C) @ B @ A) @ (sk3 @ TB @ TA @ D @ (C) @ B @ A)) | (ord_less_eq @ TB @ (C @ A) @ D))),inference(lifteq,[status(thm)],[290])).
% 197.98/123.90  thf(293,plain,(! [TA:$tType,TB:$tType,C:(TA > TB),B:TA,A:TA] : ((~ (ord @ TB)) | (~ (ord @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (ord_less_eq @ TA @ (sk2 @ TB @ TA @ (C @ B) @ (C) @ B @ A) @ (sk3 @ TB @ TA @ (C @ B) @ (C) @ B @ A)) | (ord_less_eq @ TB @ (C @ A) @ (C @ B)))),inference(simp,[status(thm)],[292])).
% 197.98/123.90  thf(186,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ (suc @ B)) = (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_less__Suc__eq__le)).
% 197.98/123.90  thf(956,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ (suc @ B)) = (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 197.98/123.90  thf(45,axiom,((order @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder_6)).
% 197.98/123.90  thf(420,plain,((order @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 197.98/123.90  thf(1327,plain,(! [TA:$tType,TB:$tType] : (~ (($true)) | (order @ (TA > TB)) | ((order @ $o) != (order @ TB)))),inference(paramod_ordered,[status(thm)],[420,283])).
% 197.98/123.90  thf(1328,plain,(! [TA:$tType,TB:$tType] : ((order @ (TA > TB)) | ((order @ $o) != (order @ TB)))),inference(simp,[status(thm)],[1327])).
% 197.98/123.90  thf(1329,plain,(! [TA:$tType] : ((order @ (TA > $o)))),inference(pattern_uni,[status(thm)],[1328:[bind_type(TA,$thf(TA)),bind_type(TB,$thf($o))]])).
% 197.98/123.90  thf(1336,plain,(! [TA:$tType,TB:$tType,TC:$tType] : (~ (($true)) | (order @ (TB > TC)) | ((order @ (TA > $o)) != (order @ TC)))),inference(paramod_ordered,[status(thm)],[1329,283])).
% 197.98/123.90  thf(1337,plain,(! [TA:$tType,TB:$tType,TC:$tType] : ((order @ (TB > TC)) | ((order @ (TA > $o)) != (order @ TC)))),inference(simp,[status(thm)],[1336])).
% 197.98/123.90  thf(1338,plain,(! [TA:$tType,TB:$tType] : ((order @ (TB > (TA > $o))))),inference(pattern_uni,[status(thm)],[1337:[bind_type(TA,$thf(TA)),bind_type(TB,$thf(TB)),bind_type(TC,$thf((TA > $o)))]])).
% 197.98/123.90  thf(33,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_30_antisym)).
% 197.98/123.90  thf(381,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)],[33])).
% 197.98/123.90  thf(215,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_140_le__greater__neq__conv)).
% 197.98/123.90  thf(1067,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)],[215])).
% 197.98/123.90  thf(117,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_108_order_Ostrict__trans2)).
% 197.98/123.90  thf(714,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)],[117])).
% 197.98/123.90  thf(210,axiom,((wellorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Owellorder)).
% 197.98/123.90  thf(1047,plain,((wellorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 197.98/123.90  thf(70,axiom,((ord_less_eq @ nat @ (size_size @ (list @ a) @ xs) @ (size_size @ (list @ a) @ ys))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1)).
% 197.98/123.90  thf(512,plain,((ord_less_eq @ nat @ (size_size @ (list @ a) @ xs) @ (size_size @ (list @ a) @ ys))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 197.98/123.90  thf(181,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_162_minf_I4_J)).
% 197.98/123.90  thf(942,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)],[181])).
% 197.98/123.90  thf(53,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ (suc @ B)) => (ord_less @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_Suc__less__SucD)).
% 197.98/123.90  thf(439,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ (suc @ B)) => (ord_less @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 197.98/123.90  thf(264,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_115_dense__ge)).
% 197.98/123.90  thf(1274,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)],[264])).
% 197.98/123.90  thf(21,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_25_le__cases3)).
% 197.98/123.90  thf(334,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)],[21])).
% 197.98/123.90  thf(173,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_141_greater__le__neq__conv)).
% 197.98/123.90  thf(910,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)],[173])).
% 197.98/123.90  thf(170,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:(nat > TA),B:nat,C:nat]: ((! [D:nat]: (ord_less @ TA @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less @ TA @ (A @ B) @ (A @ C)) = (ord_less @ nat @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_lift__Suc__mono__less__iff)).
% 197.98/123.90  thf(894,plain,((! [TA: $tType]: ((order @ TA) => (! [A:(nat > TA),B:nat,C:nat]: ((! [D:nat]: (ord_less @ TA @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less @ TA @ (A @ B) @ (A @ C)) = (ord_less @ nat @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 197.98/123.90  thf(223,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ B) => (? [C:nat]: (B = (suc @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_Suc__le__D)).
% 197.98/123.90  thf(1091,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ B) => (? [C:nat]: (B = (suc @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 197.98/123.90  thf(139,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_239_less__diff__imp__less)).
% 197.98/123.90  thf(778,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)],[139])).
% 197.98/123.90  thf(184,axiom,((! [TA: $tType]: (size @ (list @ TA)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_List_Olist___Nat_Osize_8)).
% 197.98/123.90  thf(951,plain,((! [TA: $tType]: (size @ (list @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 197.98/123.90  thf(952,plain,(! [TA:$tType] : ((size @ (list @ TA)))),inference(cnf,[status(esa)],[951])).
% 197.98/123.90  thf(263,axiom,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less_eq @ nat @ A @ B) => ((C @ A) => ((! [D:nat]: ((ord_less_eq @ nat @ A @ D) => ((ord_less @ nat @ D @ B) => ((C @ D) => (C @ (suc @ D)))))) => (C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_dec__induct)).
% 197.98/123.90  thf(1255,plain,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less_eq @ nat @ A @ B) => ((C @ A) => ((! [D:nat]: ((ord_less_eq @ nat @ A @ D) => ((ord_less @ nat @ D @ B) => ((C @ D) => (C @ (suc @ D)))))) => (C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 197.98/123.90  thf(252,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_6_list__desc__trans__le)).
% 197.98/123.90  thf(1217,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)],[252])).
% 197.98/123.90  thf(82,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (((suc @ A) != B) => (ord_less @ nat @ (suc @ A) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_Suc__lessI)).
% 197.98/123.90  thf(561,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => ((~ ((suc @ A) = B)) => (ord_less @ nat @ (suc @ A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 197.98/123.90  thf(36,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_23_order__class_Oorder_Oeq__iff)).
% 197.98/123.90  thf(392,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)],[36])).
% 197.98/123.90  thf(258,axiom,((! [A:nat,B:(nat > $o)]: ((! [C:nat]: ((ord_less @ nat @ C @ (suc @ A)) => (B @ C))) = ((B @ A) & ! [C:nat]: ((ord_less @ nat @ C @ A) => (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_All__less__Suc)).
% 197.98/123.90  thf(1238,plain,((! [A:nat,B:(nat > $o)]: ((! [C:nat]: ((ord_less @ nat @ C @ (suc @ A)) => (B @ C))) = ((B @ A) & ! [C:nat]: ((ord_less @ nat @ C @ A) => (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 197.98/123.90  thf(164,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_87_Nat_Oex__has__greatest__nat)).
% 197.98/123.90  thf(862,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)],[164])).
% 197.98/123.90  thf(22,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_34_order__subst2)).
% 197.98/123.90  thf(349,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)],[22])).
% 197.98/123.90  thf(176,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_164_minf_I7_J)).
% 197.98/123.90  thf(916,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)],[176])).
% 197.98/123.90  thf(206,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_99_dual__order_Ostrict__iff__order)).
% 197.98/123.90  thf(1032,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)],[206])).
% 197.98/123.90  thf(75,axiom,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ (suc @ D)) => (A @ D))) => (A @ (minus_minus @ nat @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_zero__induct__lemma)).
% 197.98/123.90  thf(522,plain,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((A @ (suc @ D)) => (A @ D))) => (A @ (minus_minus @ nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 197.98/123.90  thf(169,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ B) => (~ (! [C:nat]: ((ord_less @ nat @ A @ C) => (B != (suc @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_Suc__lessE)).
% 197.98/123.90  thf(889,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ B) => (~ (! [C:nat]: ((ord_less @ nat @ A @ C) => (~ (B = (suc @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 197.98/123.90  thf(267,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_89_le__antisym)).
% 197.98/123.90  thf(1281,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)],[267])).
% 197.98/123.90  thf(116,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_less__imp__neq)).
% 197.98/123.90  thf(710,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 197.98/123.90  thf(157,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_166_pinf_I6_J)).
% 197.98/123.90  thf(842,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)],[157])).
% 197.98/123.90  thf(203,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_248_diff__commute)).
% 197.98/123.90  thf(1012,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)],[203])).
% 197.98/123.90  thf(84,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_68_neq__iff)).
% 197.98/123.90  thf(566,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)],[84])).
% 197.98/123.90  thf(61,axiom,((! [TA: $tType]: ((linorder @ TA) => ((linorder_sorted @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ (suc @ B) @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ (suc @ B))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_sorted__iff__nth__Suc)).
% 197.98/123.90  thf(484,plain,((! [TA: $tType]: ((linorder @ TA) => ((linorder_sorted @ TA) = (^ [A:(list @ TA)]: ! [B:nat]: ((ord_less @ nat @ (suc @ B) @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ (suc @ B))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 197.98/123.90  thf(1342,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType] : (~ (($true)) | (order @ (TC > TD)) | ((order @ (TB > (TA > $o))) != (order @ TD)))),inference(paramod_ordered,[status(thm)],[1338,283])).
% 197.98/123.90  thf(1343,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType] : ((order @ (TC > TD)) | ((order @ (TB > (TA > $o))) != (order @ TD)))),inference(simp,[status(thm)],[1342])).
% 197.98/123.90  thf(1344,plain,(! [TA:$tType,TB:$tType,TC:$tType] : ((order @ (TC > (TB > (TA > $o)))))),inference(pattern_uni,[status(thm)],[1343:[bind_type(TA,$thf(TA)),bind_type(TB,$thf(TB)),bind_type(TC,$thf(TC)),bind_type(TD,$thf((TB > (TA > $o))))]])).
% 197.98/123.90  thf(1348,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType] : (~ (($true)) | (order @ (TD > TE)) | ((order @ (TC > (TB > (TA > $o)))) != (order @ TE)))),inference(paramod_ordered,[status(thm)],[1344,283])).
% 197.98/123.90  thf(1349,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType] : ((order @ (TD > TE)) | ((order @ (TC > (TB > (TA > $o)))) != (order @ TE)))),inference(simp,[status(thm)],[1348])).
% 197.98/123.90  thf(1350,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType] : ((order @ (TD > (TC > (TB > (TA > $o))))))),inference(pattern_uni,[status(thm)],[1349:[bind_type(TA,$thf(TA)),bind_type(TB,$thf(TB)),bind_type(TC,$thf(TC)),bind_type(TD,$thf(TD)),bind_type(TE,$thf((TC > (TB > (TA > $o)))))]])).
% 197.98/123.90  thf(74,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ (suc @ B)) = ((ord_less @ nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_less__Suc__eq)).
% 197.98/123.90  thf(519,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ (suc @ B)) = ((ord_less @ nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 197.98/123.90  thf(222,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_67_order_Oasym)).
% 197.98/123.90  thf(1089,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)],[222])).
% 197.98/123.90  thf(14,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_dual__order_Otrans)).
% 197.98/123.90  thf(317,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 197.98/123.90  thf(183,axiom,((! [TA: $tType]: ((linorder @ TA) => ((linorder_sorted @ TA) = (^ [A:(list @ TA)]: ! [B:nat,C:nat]: ((ord_less @ nat @ B @ C) => ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_sorted__iff__nth__mono__less)).
% 197.98/123.90  thf(948,plain,((! [TA: $tType]: ((linorder @ TA) => ((linorder_sorted @ TA) = (^ [A:(list @ TA)]: ! [B:nat,C:nat]: ((ord_less @ nat @ B @ C) => ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 197.98/123.90  thf(205,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_137_Lattices__Big_Oex__has__greatest__nat)).
% 197.98/123.90  thf(1017,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)],[205])).
% 197.98/123.90  thf(234,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_125_order__less__le__subst1)).
% 197.98/123.90  thf(1121,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)],[234])).
% 197.98/123.90  thf(214,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_79_linorder__neqE__nat)).
% 197.98/123.90  thf(1064,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)],[214])).
% 197.98/123.90  thf(40,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_33_ord__eq__le__subst)).
% 197.98/123.90  thf(403,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)],[40])).
% 197.98/123.90  thf(225,axiom,((! [TA: $tType]: ((list_ex @ TA) = (^ [A:(TA > $o),B:(list @ TA)]: ? [C:nat]: ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ B)) & (A @ (nth @ TA @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_list__ex__length)).
% 197.98/123.90  thf(1096,plain,((! [TA: $tType]: ((list_ex @ TA) = (^ [A:(TA > $o),B:(list @ TA)]: ? [C:nat]: ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ B)) & (A @ (nth @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 197.98/123.90  thf(89,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA),B:nat,C:nat]: ((linorder_sorted @ TA @ A) => ((ord_less_eq @ nat @ B @ C) => ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_sorted__nth__mono)).
% 197.98/123.90  thf(593,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA),B:nat,C:nat]: ((linorder_sorted @ TA @ A) => ((ord_less_eq @ nat @ B @ C) => ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 197.98/123.90  thf(162,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_149_minf_I8_J)).
% 197.98/123.90  thf(857,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)],[162])).
% 197.98/123.90  thf(19,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_31_eq__iff)).
% 197.98/123.90  thf(328,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)],[19])).
% 197.98/123.90  thf(271,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:(nat > TA),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq @ TA @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ TA @ (A @ B) @ (A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_lift__Suc__mono__le)).
% 197.98/123.90  thf(1292,plain,((! [TA: $tType]: ((order @ TA) => (! [A:(nat > TA),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq @ TA @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ TA @ (A @ B) @ (A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 197.98/123.90  thf(58,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ (suc @ B)) = (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_Suc__le__mono)).
% 197.98/123.90  thf(476,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ (suc @ A) @ (suc @ B)) = (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 197.98/123.90  thf(1582,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType,TF:$tType] : (~ (($true)) | (order @ (TE > TF)) | ((order @ (TD > (TC > (TB > (TA > $o))))) != (order @ TF)))),inference(paramod_ordered,[status(thm)],[1350,283])).
% 197.98/123.90  thf(1583,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType,TF:$tType] : ((order @ (TE > TF)) | ((order @ (TD > (TC > (TB > (TA > $o))))) != (order @ TF)))),inference(simp,[status(thm)],[1582])).
% 197.98/123.90  thf(1584,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType] : ((order @ (TE > (TD > (TC > (TB > (TA > $o)))))))),inference(pattern_uni,[status(thm)],[1583:[bind_type(TA,$thf(TA)),bind_type(TB,$thf(TB)),bind_type(TC,$thf(TC)),bind_type(TD,$thf(TD)),bind_type(TE,$thf(TE)),bind_type(TF,$thf((TD > (TC > (TB > (TA > $o))))))]])).
% 197.98/123.90  thf(251,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_96_list__desc__trans)).
% 197.98/123.90  thf(1214,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)],[251])).
% 197.98/123.90  thf(88,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_112_le__imp__less__or__eq)).
% 197.98/123.90  thf(590,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)],[88])).
% 197.98/123.90  thf(167,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less @ nat @ A @ (suc @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_le__imp__less__Suc)).
% 197.98/123.90  thf(884,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less @ nat @ A @ (suc @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 197.98/123.90  thf(80,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_69_neqE)).
% 197.98/123.90  thf(554,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)],[80])).
% 197.98/123.90  thf(130,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_57_dual__order_Oasym)).
% 197.98/123.90  thf(753,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)],[130])).
% 197.98/123.90  thf(209,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_74_ord__less__eq__subst)).
% 197.98/123.90  thf(1039,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)],[209])).
% 197.98/123.90  thf(191,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA)]: ((linorder_sorted @ TA @ (rev @ TA @ A)) = (! [B:nat,C:nat]: ((ord_less_eq @ nat @ B @ C) => ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ C) @ (nth @ TA @ A @ B)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_sorted__rev__iff__nth__mono)).
% 197.98/123.90  thf(970,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA)]: ((linorder_sorted @ TA @ (rev @ TA @ A)) = (! [B:nat,C:nat]: ((ord_less_eq @ nat @ B @ C) => ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ C) @ (nth @ TA @ A @ B)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 197.98/123.90  thf(231,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_123_not__le)).
% 197.98/123.90  thf(1114,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)],[231])).
% 197.98/123.90  thf(226,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_111_less__le__not__le)).
% 197.98/123.90  thf(1099,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)],[226])).
% 197.98/123.90  thf(72,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_63_less__asym_H)).
% 197.98/123.90  thf(515,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)],[72])).
% 197.98/123.90  thf(273,axiom,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((ord_less_eq @ nat @ B @ D) => ((A @ D) => (A @ (suc @ D))))) => ((ord_less_eq @ nat @ B @ C) => (A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_nat__induct_H)).
% 197.98/123.90  thf(1297,plain,((! [A:(nat > $o),B:nat,C:nat]: ((A @ B) => ((! [D:nat]: ((ord_less_eq @ nat @ B @ D) => ((A @ D) => (A @ (suc @ D))))) => ((ord_less_eq @ nat @ B @ C) => (A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[273])).
% 197.98/123.90  thf(238,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_235_diff__diff__cancel)).
% 197.98/123.90  thf(1131,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)],[238])).
% 197.98/123.90  thf(249,axiom,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less_eq @ nat @ A @ B) => ((C @ B) => ((! [D:nat]: ((ord_less_eq @ nat @ A @ D) => ((ord_less @ nat @ D @ B) => ((C @ (suc @ D)) => (C @ D))))) => (C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_inc__induct)).
% 197.98/123.90  thf(1192,plain,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less_eq @ nat @ A @ B) => ((C @ B) => ((! [D:nat]: ((ord_less_eq @ nat @ A @ D) => ((ord_less @ nat @ D @ B) => ((C @ (suc @ D)) => (C @ D))))) => (C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 197.98/123.90  thf(195,axiom,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) = (ord_less @ nat @ B @ (suc @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_not__less__eq)).
% 197.98/123.90  thf(984,plain,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) = (ord_less @ nat @ B @ (suc @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 197.98/123.90  thf(200,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_135_list__strict__asc__trans)).
% 197.98/123.90  thf(1002,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)],[200])).
% 197.98/123.90  thf(85,axiom,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less_eq @ nat @ A @ B) => ((C @ A) => ((! [D:nat]: ((ord_less_eq @ nat @ A @ D) => ((C @ D) => (C @ (suc @ D))))) => (C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_nat__induct__at__least)).
% 197.98/123.90  thf(569,plain,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less_eq @ nat @ A @ B) => ((C @ A) => ((! [D:nat]: ((ord_less_eq @ nat @ A @ D) => ((C @ D) => (C @ (suc @ D))))) => (C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 197.98/123.90  thf(144,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_253_Nat_Odiff__diff__eq)).
% 197.98/123.90  thf(792,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)],[144])).
% 197.98/123.90  thf(180,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_order_Ostrict__implies__not__eq)).
% 197.98/123.90  thf(938,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 197.98/123.90  thf(259,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ B) => (ord_less @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_Suc__lessD)).
% 197.98/123.90  thf(1241,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ B) => (ord_less @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 197.98/123.90  thf(178,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_138_nat__descend__induct)).
% 197.98/123.90  thf(921,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)],[178])).
% 197.98/123.90  thf(107,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_109_order_Ostrict__trans1)).
% 197.98/123.90  thf(657,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)],[107])).
% 197.98/123.90  thf(213,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_153_pinf_I2_J)).
% 197.98/123.90  thf(1054,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)],[213])).
% 197.98/123.90  thf(207,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_107_order_Oorder__iff__strict)).
% 197.98/123.90  thf(1035,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)],[207])).
% 197.98/123.90  thf(185,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_91_le__trans)).
% 197.98/123.90  thf(953,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)],[185])).
% 197.98/123.90  thf(119,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_less__imp__not__eq)).
% 197.98/123.90  thf(718,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 197.98/123.90  thf(265,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_88_nat__le__linear)).
% 197.98/123.90  thf(1278,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)],[265])).
% 197.98/123.90  thf(129,axiom,((! [A:nat]: ~ (ord_less_eq @ nat @ (suc @ A) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_Suc__n__not__le__n)).
% 197.98/123.90  thf(750,plain,((! [A:nat]: ~ (ord_less_eq @ nat @ (suc @ A) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 197.98/123.90  thf(151,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ (suc @ B)) = ((ord_less_eq @ nat @ A @ B) | (A = (suc @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_le__Suc__eq)).
% 197.98/123.90  thf(824,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ (suc @ B)) = ((ord_less_eq @ nat @ A @ B) | (A = (suc @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 197.98/123.90  thf(278,plain,((~ ((nth @ a @ xs @ sk1) = (nth @ a @ ys @ sk1)))),inference(cnfConj,[status(thm)],[276])).
% 197.98/123.90  thf(279,plain,(((nth @ a @ ys @ sk1) != (nth @ a @ xs @ sk1))),inference(lifteq,[status(thm)],[278])).
% 197.98/123.90  thf(1351,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType] : (~ (($true)) | (order @ (TD > TE)) | ((order @ (TC > (TB > (TA > nat)))) != (order @ TE)))),inference(paramod_ordered,[status(thm)],[1347,283])).
% 197.98/123.90  thf(1352,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType] : ((order @ (TD > TE)) | ((order @ (TC > (TB > (TA > nat)))) != (order @ TE)))),inference(simp,[status(thm)],[1351])).
% 197.98/123.90  thf(1353,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType] : ((order @ (TD > (TC > (TB > (TA > nat))))))),inference(pattern_uni,[status(thm)],[1352:[bind_type(TA,$thf(TA)),bind_type(TB,$thf(TB)),bind_type(TC,$thf(TC)),bind_type(TD,$thf(TD)),bind_type(TE,$thf((TC > (TB > (TA > nat)))))]])).
% 197.98/123.90  thf(1593,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType,TF:$tType] : (~ (($true)) | (order @ (TE > TF)) | ((order @ (TD > (TC > (TB > (TA > nat))))) != (order @ TF)))),inference(paramod_ordered,[status(thm)],[1353,283])).
% 197.98/123.90  thf(1594,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType,TF:$tType] : ((order @ (TE > TF)) | ((order @ (TD > (TC > (TB > (TA > nat))))) != (order @ TF)))),inference(simp,[status(thm)],[1593])).
% 197.98/123.90  thf(1595,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType] : ((order @ (TE > (TD > (TC > (TB > (TA > nat)))))))),inference(pattern_uni,[status(thm)],[1594:[bind_type(TA,$thf(TA)),bind_type(TB,$thf(TB)),bind_type(TC,$thf(TC)),bind_type(TD,$thf(TD)),bind_type(TE,$thf(TE)),bind_type(TF,$thf((TD > (TC > (TB > (TA > nat))))))]])).
% 197.98/123.90  thf(7,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_nat_Oinject)).
% 197.98/123.90  thf(296,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 197.98/123.90  thf(55,axiom,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less @ nat @ A @ B) => ((! [D:nat]: ((B = (suc @ D)) => (C @ D))) => ((! [D:nat]: ((ord_less @ nat @ D @ B) => ((C @ (suc @ D)) => (C @ D)))) => (C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_strict__inc__induct)).
% 197.98/123.90  thf(444,plain,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less @ nat @ A @ B) => ((! [D:nat]: ((B = (suc @ D)) => (C @ D))) => ((! [D:nat]: ((ord_less @ nat @ D @ B) => ((C @ (suc @ D)) => (C @ D)))) => (C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 197.98/123.90  thf(71,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_101_order_Ostrict__implies__order)).
% 197.98/123.90  thf(513,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)],[71])).
% 197.98/123.90  thf(50,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_136_list__asc__trans)).
% 197.98/123.90  thf(430,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)],[50])).
% 197.98/123.90  thf(86,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ B) = (? [C:nat]: ((B = (suc @ C)) & (ord_less @ nat @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_Suc__less__eq2)).
% 197.98/123.90  thf(584,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ B) = (? [C:nat]: ((B = (suc @ C)) & (ord_less @ nat @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 197.98/123.90  thf(149,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_237_i__append__nth2)).
% 197.98/123.90  thf(819,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)],[149])).
% 197.98/123.90  thf(47,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA)]: (((rev @ TA @ A) = B) = (A = (rev @ TA @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_rev__swap)).
% 197.98/123.90  thf(423,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA)]: (((rev @ TA @ A) = B) = (A = (rev @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 197.98/123.90  thf(235,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA),B:nat,C:nat]: ((linorder_sorted @ TA @ (rev @ TA @ A)) => ((ord_less_eq @ nat @ B @ C) => ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ C) @ (nth @ TA @ A @ B))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_sorted__rev__nth__mono)).
% 197.98/123.90  thf(1125,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(list @ TA),B:nat,C:nat]: ((linorder_sorted @ TA @ (rev @ TA @ A)) => ((ord_less_eq @ nat @ B @ C) => ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ C) @ (nth @ TA @ A @ B))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 197.98/123.90  thf(137,axiom,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) => ((ord_less @ nat @ A @ (suc @ B)) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_not__less__less__Suc__eq)).
% 197.98/123.90  thf(772,plain,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) => ((ord_less @ nat @ A @ (suc @ B)) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 197.98/123.90  thf(281,plain,(! [TA:$tType,A:(list @ TA)] : ((~ (preorder @ TA)) | (~ (list_strict_desc @ TA @ A)) | (list_desc @ TA @ A))),inference(cnf,[status(esa)],[280])).
% 197.98/123.90  thf(256,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_46_exists__least__iff)).
% 197.98/123.90  thf(1226,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)],[256])).
% 197.98/123.90  thf(79,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_eq @ nat @ (suc @ D) @ C) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_full__nat__induct)).
% 197.98/123.90  thf(545,plain,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_eq @ nat @ (suc @ D) @ C) => (A @ D))) => (A @ C))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 197.98/123.90  thf(104,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_254_le__diff__iff)).
% 197.98/123.90  thf(641,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)],[104])).
% 197.98/123.90  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_61_less__linear)).
% 197.98/123.90  thf(1312,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])).
% 197.98/123.90  thf(65,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_48_order_Ostrict__trans)).
% 197.98/123.90  thf(498,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)],[65])).
% 197.98/123.90  thf(229,axiom,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) => ((ord_less @ nat @ A @ (suc @ B)) => (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_less__antisym)).
% 197.98/123.90  thf(1107,plain,((! [A:nat,B:nat]: ((~ (ord_less @ nat @ A @ B)) => ((ord_less @ nat @ A @ (suc @ B)) => (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 197.98/123.90  thf(148,axiom,((! [A:nat,B:nat,C:(nat > (nat > $o))]: ((ord_less_eq @ nat @ A @ B) => ((! [D:nat]: (C @ D @ D)) => ((! [D:nat,E:nat,F:nat]: ((C @ D @ E) => ((C @ E @ F) => (C @ D @ F)))) => ((! [D:nat]: (C @ D @ (suc @ D))) => (C @ A @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_transitive__stepwise__le)).
% 197.98/123.90  thf(804,plain,((! [A:nat,B:nat,C:(nat > (nat > $o))]: ((ord_less_eq @ nat @ A @ B) => ((! [D:nat]: (C @ D @ D)) => ((! [D:nat,E:nat,F:nat]: ((C @ D @ E) => ((C @ E @ F) => (C @ D @ F)))) => ((! [D:nat]: (C @ D @ (suc @ D))) => (C @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 197.98/123.90  thf(255,axiom,(((ord_less_eq @ nat) = (^ [A:nat,B:nat]: ((ord_less @ nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_le__eq__less__or__eq)).
% 197.98/123.90  thf(1224,plain,(((ord_less_eq @ nat) = (^ [A:nat,B:nat]: ((ord_less @ nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 197.98/123.90  thf(172,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_160_minf_I2_J)).
% 197.98/123.90  thf(900,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)],[172])).
% 197.98/123.90  thf(44,axiom,((preorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Opreorder_4)).
% 197.98/123.90  thf(419,plain,((preorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 197.98/123.90  thf(211,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_less__not__refl3)).
% 197.98/123.90  thf(1048,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 197.98/123.90  thf(125,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_4_list__eq__iff__nth__eq)).
% 197.98/123.90  thf(737,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)],[125])).
% 197.98/123.90  thf(69,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_247_less__imp__diff__less)).
% 197.98/123.90  thf(509,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)],[69])).
% 197.98/123.90  thf(141,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less_eq @ nat @ (suc @ A) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_Suc__leI)).
% 197.98/123.90  thf(784,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less_eq @ nat @ (suc @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 197.98/123.90  thf(232,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_less__not__refl)).
% 197.98/123.90  thf(1117,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 197.98/123.90  thf(32,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_35_order__subst1)).
% 197.98/123.90  thf(377,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)],[32])).
% 197.98/123.90  thf(197,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_75_ord__eq__less__subst)).
% 197.98/123.90  thf(990,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)],[197])).
% 197.98/123.90  thf(97,axiom,((! [A:nat,B:nat,C:(nat > (nat > $o))]: ((ord_less @ nat @ A @ B) => ((! [D:nat]: (C @ D @ (suc @ D))) => ((! [D:nat,E:nat,F:nat]: ((ord_less @ nat @ D @ E) => ((ord_less @ nat @ E @ F) => ((C @ D @ E) => ((C @ E @ F) => (C @ D @ F)))))) => (C @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_less__Suc__induct)).
% 197.98/123.90  thf(616,plain,((! [A:nat,B:nat,C:(nat > (nat > $o))]: ((ord_less @ nat @ A @ B) => ((! [D:nat]: (C @ D @ (suc @ D))) => ((! [D:nat,E:nat,F:nat]: ((ord_less @ nat @ D @ E) => ((ord_less @ nat @ E @ F) => ((C @ D @ E) => ((C @ E @ F) => (C @ D @ F)))))) => (C @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 197.98/123.90  thf(9,axiom,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA)]: (((rev @ TA @ A) = (rev @ TA @ B)) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_rev__is__rev__conv)).
% 197.98/123.90  thf(303,plain,((! [TA: $tType]: (! [A:(list @ TA),B:(list @ TA)]: (((rev @ TA @ A) = (rev @ TA @ B)) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 197.98/123.90  thf(133,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_151_pinf_I8_J)).
% 197.98/123.90  thf(758,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)],[133])).
% 197.98/123.90  thf(17,axiom,((! [A:nat]: (A != (suc @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_n__not__Suc__n)).
% 197.98/123.90  thf(323,plain,((! [A:nat]: ~ (A = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 197.98/123.90  thf(146,axiom,((! [TA: $tType]: (! [A:nat,B:(list @ TA)]: ((ord_less @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((nth @ TA @ (rev @ TA @ B) @ A) = (nth @ TA @ B @ (minus_minus @ nat @ (size_size @ (list @ TA) @ B) @ (suc @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_rev__nth)).
% 197.98/123.90  thf(799,plain,((! [TA: $tType]: (! [A:nat,B:(list @ TA)]: ((ord_less @ nat @ A @ (size_size @ (list @ TA) @ B)) => ((nth @ TA @ (rev @ TA @ B) @ A) = (nth @ TA @ B @ (minus_minus @ nat @ (size_size @ (list @ TA) @ B) @ (suc @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 197.98/123.90  thf(175,axiom,((ord @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Oord_3)).
% 197.98/123.90  thf(915,plain,((ord @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 197.98/123.90  thf(136,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_120_antisym__conv1)).
% 197.98/123.90  thf(769,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)],[136])).
% 197.98/123.90  thf(39,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_28_eq__refl)).
% 197.98/123.90  thf(399,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)],[39])).
% 197.98/123.90  thf(1452,plain,(! [TA:$tType,C:(TA > $o),B:TA,A:TA] : ((~ (ord @ $o)) | (~ (ord @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (ord_less_eq @ TA @ (sk2 @ $o @ TA @ (C @ B) @ (C) @ B @ A) @ (sk3 @ $o @ TA @ (C @ B) @ (C) @ B @ A)) | (ord_less_eq @ $o @ (C @ A) @ ($true)) | ((ord_less @ nat @ sk1 @ (size_size @ (list @ a) @ xs)) != (C @ B)))),inference(paramod_ordered,[status(thm)],[277,293])).
% 197.98/123.90  thf(1466,plain,(! [TA:$tType,B:TA,A:TA] : ((~ (ord @ $o)) | (~ (ord @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (ord_less_eq @ TA @ (sk2 @ $o @ TA @ (ord_less @ nat @ sk1 @ (size_size @ (list @ a) @ xs)) @ (^ [C:TA]: (ord_less @ nat @ sk1 @ (size_size @ (list @ a) @ xs))) @ B @ A) @ (sk3 @ $o @ TA @ (ord_less @ nat @ sk1 @ (size_size @ (list @ a) @ xs)) @ (^ [C:TA]: (ord_less @ nat @ sk1 @ (size_size @ (list @ a) @ xs))) @ B @ A)) | (ord_less_eq @ $o @ (ord_less @ nat @ sk1 @ (size_size @ (list @ a) @ xs)) @ ($true)))),inference(pre_uni,[status(thm)],[1452:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(^ [D:TA]: (ord_less @ nat @ sk1 @ (size_size @ (list @ a) @ xs))))]])).
% 197.98/123.90  thf(30,axiom,((ord @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oord_7)).
% 197.98/123.90  thf(373,plain,((ord @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 197.98/123.90  thf(1677,plain,(! [TA:$tType,B:TA,A:TA] : (~ (($true)) | (~ (ord @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (ord_less_eq @ TA @ (sk2 @ $o @ TA @ ($true) @ (^ [C:TA]: (($true))) @ B @ A) @ (sk3 @ $o @ TA @ ($true) @ (^ [C:TA]: (($true))) @ B @ A)) | (ord_less_eq @ $o @ ($true) @ ($true)))),inference(rewrite,[status(thm)],[1466,277,373])).
% 197.98/123.90  thf(1678,plain,(! [TA:$tType,B:TA,A:TA] : ((~ (ord @ TA)) | (~ (ord_less_eq @ TA @ A @ B)) | (ord_less_eq @ TA @ (sk2 @ $o @ TA @ ($true) @ (^ [C:TA]: (($true))) @ B @ A) @ (sk3 @ $o @ TA @ ($true) @ (^ [C:TA]: (($true))) @ B @ A)) | (ord_less_eq @ $o @ ($true) @ ($true)))),inference(simp,[status(thm)],[1677])).
% 197.98/123.90  thf(1697,plain,(! [TA:$tType,B:TA,A:TA] : (~ (($true)) | (~ (ord_less_eq @ TA @ A @ B)) | (ord_less_eq @ TA @ (sk2 @ $o @ TA @ ($true) @ (^ [C:TA]: (($true))) @ B @ A) @ (sk3 @ $o @ TA @ ($true) @ (^ [C:TA]: (($true))) @ B @ A)) | (ord_less_eq @ $o @ ($true) @ ($true)) | ((ord @ nat) != (ord @ TA)))),inference(paramod_ordered,[status(thm)],[915,1678])).
% 197.98/123.90  thf(1698,plain,(! [TA:$tType,B:TA,A:TA] : ((~ (ord_less_eq @ TA @ A @ B)) | (ord_less_eq @ TA @ (sk2 @ $o @ TA @ ($true) @ (^ [C:TA]: (($true))) @ B @ A) @ (sk3 @ $o @ TA @ ($true) @ (^ [C:TA]: (($true))) @ B @ A)) | (ord_less_eq @ $o @ ($true) @ ($true)) | ((ord @ nat) != (ord @ TA)))),inference(simp,[status(thm)],[1697])).
% 197.98/123.90  thf(1699,plain,(! [B:nat,A:nat] : ((~ (ord_less_eq @ nat @ A @ B)) | (ord_less_eq @ nat @ (sk2 @ $o @ nat @ ($true) @ (^ [C:nat]: (($true))) @ B @ A) @ (sk3 @ $o @ nat @ ($true) @ (^ [C:nat]: (($true))) @ B @ A)) | (ord_less_eq @ $o @ ($true) @ ($true)))),inference(pattern_uni,[status(thm)],[1698:[bind_type(TA,$thf(nat))]])).
% 197.98/123.90  thf(187,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_252_diff__le__mono)).
% 197.98/123.90  thf(959,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)],[187])).
% 197.98/123.90  thf(152,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ A @ (suc @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_le__SucI)).
% 197.98/123.90  thf(827,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => (ord_less_eq @ nat @ A @ (suc @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 197.98/123.90  thf(204,axiom,((! [A:nat,B:nat]: (ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_diff__le__self)).
% 197.98/123.90  thf(1015,plain,((! [A:nat,B:nat]: (ord_less_eq @ nat @ (minus_minus @ nat @ A @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 197.98/123.90  thf(10,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(list @ TA)]: ((list_ex @ TA @ A @ (rev @ TA @ B)) = (list_ex @ TA @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_list__ex__rev)).
% 197.98/123.90  thf(306,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(list @ TA)]: ((list_ex @ TA @ (A) @ (rev @ TA @ B)) = (list_ex @ TA @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 197.98/123.90  thf(199,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_51_less__imp__triv)).
% 197.98/123.90  thf(1000,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)],[199])).
% 197.98/123.90  thf(8,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_22_ord__eq__le__trans)).
% 197.98/123.90  thf(299,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)],[8])).
% 197.98/123.90  thf(261,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_dual__order_Ostrict__implies__not__eq)).
% 197.98/123.90  thf(1250,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 197.98/123.90  thf(227,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_0_i__append__eq__i__append__conv)).
% 197.98/123.90  thf(1102,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)],[227])).
% 197.98/123.90  thf(245,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_241_nat__diff__left__cancel__eq2)).
% 197.98/123.90  thf(1176,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)],[245])).
% 197.98/123.90  thf(94,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_161_minf_I3_J)).
% 197.98/123.90  thf(608,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)],[94])).
% 197.98/123.90  thf(120,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_7_length__induct)).
% 197.98/123.90  thf(722,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)],[120])).
% 197.98/123.90  thf(48,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_37_le__funI)).
% 197.98/123.90  thf(426,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)],[48])).
% 197.98/123.90  thf(31,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_15_dual__order_Oeq__iff)).
% 197.98/123.90  thf(374,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)],[31])).
% 197.98/123.90  thf(219,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_154_pinf_I3_J)).
% 197.98/123.90  thf(1081,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)],[219])).
% 197.98/123.90  thf(24,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_dual__order_Orefl)).
% 197.98/123.90  thf(355,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 197.98/123.90  thf(190,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_55_less__not__sym)).
% 197.98/123.90  thf(968,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)],[190])).
% 197.98/123.90  thf(155,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_58_ord__less__eq__trans)).
% 197.98/123.90  thf(836,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)],[155])).
% 197.98/123.90  thf(57,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_142_less__ge__neq__conv)).
% 197.98/123.90  thf(473,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)],[57])).
% 197.98/123.90  thf(217,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_62_less__trans)).
% 197.98/123.90  thf(1076,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)],[217])).
% 197.98/123.90  thf(239,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ (suc @ B)) => ((~ (ord_less_eq @ nat @ A @ B)) => (A = (suc @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_le__SucE)).
% 197.98/123.90  thf(1134,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ (suc @ B)) => ((~ (ord_less_eq @ nat @ A @ B)) => (A = (suc @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 197.98/123.90  thf(62,axiom,((size @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Nat_Osize)).
% 197.98/123.90  thf(487,plain,((size @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 197.98/123.90  thf(81,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_124_order__less__le__subst2)).
% 197.98/123.90  thf(557,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)],[81])).
% 197.98/123.90  thf(161,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_163_minf_I5_J)).
% 197.98/123.90  thf(855,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)],[161])).
% 197.98/123.90  thf(103,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_165_minf_I11_J)).
% 197.98/123.90  thf(640,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 197.98/123.90  thf(216,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_77_measure__induct)).
% 197.98/123.90  thf(1070,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)],[216])).
% 197.98/123.90  thf(42,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_27_le__cases)).
% 197.98/123.90  thf(414,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)],[42])).
% 197.98/123.90  thf(18,axiom,((linorder @ $o)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Olinorder_5)).
% 197.98/123.90  thf(327,plain,((linorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 197.98/123.90  thf(114,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_122_not__less)).
% 197.98/123.90  thf(705,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)],[114])).
% 197.98/123.90  thf(54,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ (suc @ B)) = (ord_less @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_Suc__less__eq)).
% 197.98/123.90  thf(441,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ (suc @ A) @ (suc @ B)) = (ord_less @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 197.98/123.90  thf(156,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_242_nat__diff__left__cancel__less)).
% 197.98/123.90  thf(840,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)],[156])).
% 197.98/123.90  thf(220,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_64_less__asym)).
% 197.98/123.90  thf(1085,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)],[220])).
% 197.98/123.90  thf(253,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_105_dual__order_Ostrict__trans1)).
% 197.98/123.90  thf(1220,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)],[253])).
% 197.98/123.90  thf(20,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_old_Onat_Oinject)).
% 197.98/123.90  thf(331,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 197.98/123.90  thf(248,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_2_nth__equalityI)).
% 197.98/123.90  thf(1186,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)],[248])).
% 197.98/123.90  thf(208,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_158_pinf_I11_J)).
% 197.98/123.90  thf(1038,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 197.98/123.90  thf(29,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_36_le__fun__def)).
% 197.98/123.90  thf(370,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)],[29])).
% 197.98/123.90  thf(127,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_59_ord__eq__less__trans)).
% 197.98/123.90  thf(744,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)],[127])).
% 197.98/123.90  thf(268,axiom,((! [A:nat]: ((listIn521021761append @ a @ xs @ f @ A) = (listIn521021761append @ a @ ys @ g @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 197.98/123.90  thf(1284,plain,((! [A:nat]: ((listIn521021761append @ a @ xs @ (f) @ A) = (listIn521021761append @ a @ ys @ (g) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 197.98/123.90  thf(212,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:(nat > TA),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq @ TA @ (A @ (suc @ D)) @ (A @ D))) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ TA @ (A @ C) @ (A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_lift__Suc__antimono__le)).
% 197.98/123.90  thf(1052,plain,((! [TA: $tType]: ((order @ TA) => (! [A:(nat > TA),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq @ TA @ (A @ (suc @ D)) @ (A @ D))) => ((ord_less_eq @ nat @ B @ C) => (ord_less_eq @ TA @ (A @ C) @ (A @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 197.98/123.90  thf(13,axiom,((! [TA: $tType]: (! [A:(list @ TA)]: ((rev @ TA @ (rev @ TA @ A)) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_rev__rev__ident)).
% 197.98/123.90  thf(314,plain,((! [TA: $tType]: (! [A:(list @ TA)]: ((rev @ TA @ (rev @ TA @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 197.98/123.90  thf(90,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_102_dense__le__bounded)).
% 197.98/123.90  thf(595,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)],[90])).
% 197.98/123.90  thf(95,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_117_le__less__trans)).
% 197.98/123.90  thf(612,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)],[95])).
% 197.98/123.90  thf(163,axiom,((! [A:nat,B:(nat > $o)]: ((? [C:nat]: ((ord_less @ nat @ C @ (suc @ A)) & (B @ C))) = ((B @ A) | ? [C:nat]: ((ord_less @ nat @ C @ A) & (B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_Ex__less__Suc)).
% 197.98/123.90  thf(859,plain,((! [A:nat,B:(nat > $o)]: ((? [C:nat]: ((ord_less @ nat @ C @ (suc @ A)) & (B @ C))) = ((B @ A) | ? [C:nat]: ((ord_less @ nat @ C @ A) & (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 197.98/123.90  thf(91,axiom,((! [A:nat,B:nat]: ((minus_minus @ nat @ (suc @ A) @ (suc @ B)) = (minus_minus @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_diff__Suc__Suc)).
% 197.98/123.90  thf(600,plain,((! [A:nat,B:nat]: ((minus_minus @ nat @ (suc @ A) @ (suc @ B)) = (minus_minus @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 197.98/123.90  thf(224,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_less__irrefl)).
% 197.98/123.90  thf(1094,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 197.98/123.90  thf(193,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_167_verit__comp__simplify1_I3_J)).
% 197.98/123.90  thf(978,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)],[193])).
% 197.98/123.90  thf(241,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_44_linorder__less__wlog)).
% 197.98/123.90  thf(1140,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)],[241])).
% 197.98/123.90  thf(99,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ (suc @ A) @ (suc @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_Suc__mono)).
% 197.98/123.90  thf(627,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ (suc @ A) @ (suc @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 197.98/123.90  thf(1315,plain,((ys != xs) | (sk1 != sk1)),inference(simp,[status(thm)],[279])).
% 197.98/123.90  thf(1316,plain,((ys != xs)),inference(simp,[status(thm)],[1315])).
% 197.98/123.90  thf(26,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_144_list__strict__asc__imp__list__asc)).
% 197.98/123.90  thf(363,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)],[26])).
% 197.98/123.90  thf(60,axiom,((! [A:nat]: (ord_less_eq @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_le__refl)).
% 197.98/123.90  thf(482,plain,((! [A:nat]: (ord_less_eq @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 197.98/123.90  thf(109,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_66_dense)).
% 197.98/123.90  thf(688,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)],[109])).
% 197.98/123.90  thf(202,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_verit__comp__simplify1_I1_J)).
% 197.98/123.90  thf(1010,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 197.98/123.90  thf(28,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_39_le__funD)).
% 197.98/123.90  thf(368,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)],[28])).
% 197.98/123.90  thf(158,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_150_minf_I6_J)).
% 197.98/123.90  thf(844,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)],[158])).
% 197.98/123.90  thf(112,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => ((ord_less @ nat @ B @ C) => (ord_less @ nat @ (suc @ A) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_less__trans__Suc)).
% 197.98/123.90  thf(699,plain,((! [A:nat,B:nat,C:nat]: ((ord_less @ nat @ A @ B) => ((ord_less @ nat @ B @ C) => (ord_less @ nat @ (suc @ A) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 197.98/123.90  thf(73,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_116_less__le__trans)).
% 197.98/123.90  thf(517,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)],[73])).
% 197.98/123.90  thf(15,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_26_order_Otrans)).
% 197.98/123.90  thf(319,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)],[15])).
% 197.98/123.90  thf(182,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ A @ (suc @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_less__SucI)).
% 197.98/123.90  thf(946,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less @ nat @ A @ (suc @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 197.98/123.90  thf(101,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_11_less__or__eq__imp__le)).
% 197.98/123.90  thf(632,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)],[101])).
% 197.98/123.90  thf(140,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_243_nat__diff__right__cancel__eq1)).
% 197.98/123.90  thf(781,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)],[140])).
% 197.98/123.90  thf(128,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_245_nat__diff__right__cancel__less)).
% 197.98/123.90  thf(748,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)],[128])).
% 197.98/123.90  thf(123,axiom,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_less__irrefl__nat)).
% 197.98/123.90  thf(731,plain,((! [A:nat]: ~ (ord_less @ nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 197.98/123.90  thf(142,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_1_i__append__nth1)).
% 197.98/123.90  thf(786,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)],[142])).
% 197.98/123.90  thf(51,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_72_order__less__subst2)).
% 197.98/123.90  thf(433,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)],[51])).
% 197.98/123.90  thf(272,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_121_le__neq__trans)).
% 197.98/123.90  thf(1294,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)],[272])).
% 197.98/123.90  thf(135,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_78_infinite__descent__measure)).
% 197.98/123.90  thf(763,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)],[135])).
% 197.98/123.90  thf(154,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_114_dense__le)).
% 197.98/123.90  thf(832,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)],[154])).
% 197.98/123.90  thf(77,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_54_less__induct)).
% 197.98/123.90  thf(536,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)],[77])).
% 197.98/123.90  thf(118,axiom,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_lt__ex)).
% 197.98/123.90  thf(716,plain,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 197.98/123.90  thf(257,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_81_nat__less__induct)).
% 197.98/123.90  thf(1229,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)],[257])).
% 197.98/123.90  thf(92,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_128_less__le)).
% 197.98/123.90  thf(603,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)],[92])).
% 197.98/123.90  thf(324,plain,((~ (? [A:nat]: (A = (suc @ A))))),inference(miniscope,[status(thm)],[323])).
% 197.98/123.90  thf(325,plain,(! [A:nat] : ((~ (A = (suc @ A))))),inference(cnf,[status(esa)],[324])).
% 197.98/123.90  thf(326,plain,(! [A:nat] : (((suc @ A) != A))),inference(lifteq,[status(thm)],[325])).
% 197.98/123.90  thf(177,axiom,((! [TA: $tType]: ((linorder @ TA) => ((linorder_sorted @ TA) = (^ [A:(list @ TA)]: ! [B:nat,C:nat]: ((ord_less_eq @ nat @ B @ C) => ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ C))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_sorted__iff__nth__mono)).
% 197.98/123.90  thf(918,plain,((! [TA: $tType]: ((linorder @ TA) => ((linorder_sorted @ TA) = (^ [A:(list @ TA)]: ! [B:nat,C:nat]: ((ord_less_eq @ nat @ B @ C) => ((ord_less @ nat @ C @ (size_size @ (list @ TA) @ A)) => (ord_less_eq @ TA @ (nth @ TA @ A @ B) @ (nth @ TA @ A @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 197.98/123.90  thf(68,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_143_less__fun__def)).
% 197.98/123.90  thf(506,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)],[68])).
% 197.98/123.90  thf(111,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_100_dual__order_Oorder__iff__strict)).
% 197.98/123.90  thf(696,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)],[111])).
% 197.98/123.90  thf(168,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_240_nat__diff__left__cancel__eq1)).
% 197.98/123.90  thf(886,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)],[168])).
% 197.98/123.90  thf(52,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_104_dual__order_Ostrict__trans2)).
% 197.98/123.90  thf(437,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)],[52])).
% 197.98/123.91  thf(244,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_eq__imp__le)).
% 197.98/123.91  thf(1172,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 197.98/123.91  thf(171,axiom,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less @ nat @ B @ (suc @ A)) = (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_le__less__Suc__eq)).
% 197.98/123.91  thf(897,plain,((! [A:nat,B:nat]: ((ord_less_eq @ nat @ A @ B) => ((ord_less @ nat @ B @ (suc @ A)) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 197.98/123.91  thf(145,axiom,((! [A:nat,B:nat]: ((~ (ord_less_eq @ nat @ A @ B)) = (ord_less_eq @ nat @ (suc @ B) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_not__less__eq__eq)).
% 197.98/123.91  thf(796,plain,((! [A:nat,B:nat]: ((~ (ord_less_eq @ nat @ A @ B)) = (ord_less_eq @ nat @ (suc @ B) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 197.98/123.91  thf(196,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_3_Skolem__list__nth)).
% 197.98/123.91  thf(987,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)],[196])).
% 197.98/123.91  thf(56,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_80_infinite__descent)).
% 197.98/123.91  thf(464,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)],[56])).
% 197.98/123.91  thf(237,axiom,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less_eq @ nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_less__imp__le__nat)).
% 197.98/123.91  thf(1129,plain,((! [A:nat,B:nat]: ((ord_less @ nat @ A @ B) => (ord_less_eq @ nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 197.98/123.91  thf(150,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_130_leI)).
% 197.98/123.91  thf(822,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)],[150])).
% 197.98/123.91  thf(233,axiom,((preorder @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Opreorder_1)).
% 197.98/123.91  thf(1120,plain,((preorder @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 197.98/123.91  thf(37,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_19_order__trans)).
% 197.98/123.91  thf(395,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)],[37])).
% 197.98/123.91  thf(98,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_106_order_Ostrict__iff__order)).
% 197.98/123.91  thf(624,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)],[98])).
% 197.98/123.91  thf(121,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_98_dual__order_Ostrict__implies__order)).
% 197.98/123.91  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)],[121])).
% 197.98/123.91  thf(126,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_127_order__le__less__subst1)).
% 197.98/123.91  thf(740,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)],[126])).
% 197.98/123.91  thf(1604,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType,TF:$tType,TG:$tType] : (~ (($true)) | (order @ (TF > TG)) | ((order @ (TE > (TD > (TC > (TB > (TA > $o)))))) != (order @ TG)))),inference(paramod_ordered,[status(thm)],[1584,283])).
% 197.98/123.91  thf(1605,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType,TF:$tType,TG:$tType] : ((order @ (TF > TG)) | ((order @ (TE > (TD > (TC > (TB > (TA > $o)))))) != (order @ TG)))),inference(simp,[status(thm)],[1604])).
% 197.98/123.91  thf(1606,plain,(! [TA:$tType,TB:$tType,TC:$tType,TD:$tType,TE:$tType,TF:$tType] : ((order @ (TF > (TE > (TD > (TC > (TB > (TA > $o))))))))),inference(pattern_uni,[status(thm)],[1605:[bind_type(TA,$thf(TA)),bind_type(TB,$thf(TB)),bind_type(TC,$thf(TC)),bind_type(TD,$thf(TD)),bind_type(TE,$thf(TE)),bind_type(TF,$thf(TF)),bind_type(TG,$thf((TE > (TD > (TC > (TB > (TA > $o)))))))]])).
% 197.98/123.91  thf(138,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_249_diff__le__mono2)).
% 197.98/123.91  thf(775,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)],[138])).
% 197.98/123.91  thf(131,axiom,((no_top @ nat)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',tcon_Nat_Onat___Orderings_Ono__top)).
% 197.98/123.91  thf(755,plain,((no_top @ nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 197.98/123.91  thf(115,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_157_pinf_I7_J)).
% 197.98/123.91  thf(708,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)],[115])).
% 197.98/123.91  thf(11,axiom,((! [TA: $tType]: ((linorder @ TA) => ((list_asc @ TA) = (linorder_sorted @ TA))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_list__ord__le__sorted__eq)).
% 197.98/123.91  thf(309,plain,((! [TA: $tType]: ((linorder @ TA) => ((list_asc @ TA) = (linorder_sorted @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 197.98/123.91  thf(108,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_139_complete__interval)).
% 197.98/123.91  thf(659,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)],[108])).
% 197.98/123.91  thf(5342,plain,(($false)),inference(e,[status(thm)],[645,629,365,846,962,1179,1110,1168,760,479,1105,1211,1158,1005,614,730,1290,878,655,1078,384,1137,533,500,913,1222,829,973,288,565,1254,1243,1127,389,1287,504,702,802,542,587,1323,934,357,638,1087,421,284,606,1347,881,416,492,756,789,321,1183,353,966,981,397,280,692,734,998,411,428,849,312,293,956,1338,381,1067,714,1047,512,942,439,1274,334,910,894,1091,778,952,1255,1217,561,392,275,1238,862,349,916,1032,522,889,1281,710,842,1012,566,484,1350,519,1089,317,948,1017,1121,1064,403,1096,593,420,857,328,488,1292,476,1584,1214,590,884,1329,554,753,1039,970,1114,1099,515,1297,1131,1192,984,1002,569,792,938,1241,921,657,1054,1035,953,718,1278,750,824,279,1595,296,444,513,430,584,819,423,1125,772,281,1226,545,641,1312,498,1107,804,1224,900,419,1048,737,509,784,1117,377,990,616,303,758,323,799,915,1344,769,399,1699,959,827,1015,306,1000,299,1250,1102,1176,608,722,426,374,1081,355,968,836,473,1076,1134,487,557,855,640,1070,414,327,705,282,441,840,1085,951,1220,331,1186,1038,370,744,1284,1052,314,595,612,859,1353,600,1094,978,1140,627,1316,363,482,688,1010,368,844,699,517,319,946,632,781,1341,748,731,786,433,1294,763,832,536,716,1280,1678,1229,373,603,564,326,918,506,696,886,437,1335,1172,897,796,283,987,464,1129,822,277,1120,395,624,728,740,1606,775,755,491,708,309,659])).
% 197.98/123.91  % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 197.98/123.91  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------