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

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : ITP099^1 : 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 : n003.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Wed Sep 30 08:06:45 AM UTC 2026

% Result   : Theorem 19.97s 5.82s
% Output   : Refutation 21.09s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : ITP099^1 : 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.09/0.22  % Computer : n003.cluster.edu
% 0.09/0.22  % Model    : x86_64 x86_64
% 0.09/0.22  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22  % Memory   : 8046.5625MB
% 0.09/0.22  % OS       : Linux 6.8.0-71-generic
% 0.09/0.22  % CPULimit : 300
% 0.09/0.22  % WCLimit  : 300
% 0.09/0.22  % DateTime : Tue Sep 29 19:55:13 UTC 2026
% 0.09/0.22  % CPUTime  : 
% 0.09/0.22  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.04/0.80  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 2.35/1.20  % [INFO] 	 Parsing done (394ms). 
% 2.35/1.21  % [INFO] 	 Running in sequential loop mode. 
% 3.74/1.60  % [INFO] 	 eprover registered as external prover. 
% 3.74/1.61  % [INFO] 	 Scanning for conjecture ... 
% 3.96/1.74  % [INFO] 	 Found a conjecture (or negated_conjecture) and 252 axioms. Running axiom selection ... 
% 4.15/1.87  % [INFO] 	 Axiom selection finished. Selected 252 axioms (removed 0 axioms). 
% 4.77/2.12  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 5.08/2.14  % [INFO] 	 Type checking passed. 
% 5.08/2.15  % [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 ... 
% 19.97/5.81  % External prover 'e' found a proof!
% 19.97/5.81  % [INFO] 	 Killing All external provers ... 
% 19.97/5.81  % Time passed: 5451ms (effective reasoning time: 4596ms)
% 19.97/5.82  % 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)>
% 19.97/5.82  % Axioms used in derivation (252): fact_195_antisym__conv1, fact_110_nth__append1, fact_129_order__class_Oorder_Oeq__iff, fact_69_le__greater__neq__conv, fact_96_Skolem__list__nth, fact_83_le__diff__swap, fact_42_i__append__def, fact_237_add__less__cancel__left, fact_170_ord__less__eq__subst, fact_52_append__eq__append__conv, fact_206_leD, fact_105_i__drop__nth__sub, fact_144_exists__least__iff, fact_86_eq__diff__left__iff, fact_70_nat__less__le, help_If_1_1_If_001tf__a_T, fact_40_i__append__nth, fact_143_linorder__less__wlog, fact_54_i__append__nth1, help_If_2_1_If_001t__Nat__Onat_T, fact_241_add__diff__cancel__right, fact_104_nat__diff__right__cancel__le1, fact_85_le__imp__diff__le, fact_157_ord__eq__less__trans, fact_65_i__append__eq__i__append__conv2__aux, fact_94_nth__equalityI, fact_224_pinf_I1_J, fact_15_length__induct, fact_49_same__append__eq, fact_209_verit__comp__simplify1_I3_J, fact_51_append__eq__append__conv, fact_95_nth__equalityI, fact_210_pinf_I6_J, fact_67_less__ge__neq__conv, fact_4_length__drop, fact_55_i__append__nth1, fact_246_drop__drop, fact_92_nth__append, fact_13_nat__diff__right__cancel__less, fact_219_pinf_I7_J, fact_97_Skolem__list__nth, fact_8_nat__diff__left__cancel__eq1, fact_239_add__diff__cancel__left, fact_12_nat__diff__right__cancel__eq2, fact_226_list__strict__desc__imp__list__desc, fact_217_minf_I2_J, fact_30_eq__imp__diff__eq, fact_90_i__append__eq__i__appendI, fact_123_linear, fact_141_not__less__iff__gr__or__eq, fact_165_neq__iff, fact_236_add__le__cancel__left, fact_36_last__drop, fact_66_ge__less__neq__conv, fact_101_diff__less__mono, fact_211_pinf_I8_J, fact_190_le__less__linear, fact_205_leI, fact_107_nth__append2, fact_197_not__less, fact_233_add__right__cancel, fact_113_nat__descend__induct, fact_138_dual__order_Oantisym, fact_82_diff__le__mono2, fact_16_linorder__neqE__nat, fact_118_order__subst2, fact_32_i__append__i__drop__eq1, fact_244_nat__add__left__cancel__le, fact_37_last__drop, fact_68_greater__le__neq__conv, fact_93_nth__append, fact_116_list__strict__asc__imp__list__asc, fact_220_pinf_I5_J, help_If_2_1_If_001tf__a_T, fact_34_i__append__i__drop__eq2, fact_119_ord__eq__le__subst, fact_58_eq__imp__le, fact_238_add__less__cancel__right, fact_218_minf_I1_J, fact_106_diff__right__commute, fact_174_list__strict__asc__trans, fact_130_ord__eq__le__trans, fact_25_size__neq__size__imp__neq, fact_18_nat__less__induct, fact_176_order_Onot__eq__order__implies__strict, fact_124_eq__refl, fact_212_verit__la__disequality, fact_150_less__imp__not__eq2, fact_225_verit__comp__simplify1_I1_J, fact_162_less__asym, fact_126_order_Otrans, fact_204_le__less, fact_196_le__neq__trans, fact_154_less__imp__not__eq, fact_80_diff__le__self, fact_155_dual__order_Oasym, fact_28_Ex__list__of__length, fact_173_list__asc__trans, fact_53_i__append__assoc, fact_191_less__le__trans, fact_87_le__diff__le__imp__le, fact_27_neq__if__length__neq, fact_84_le__diff__imp__le, fact_72_le__eq__less__or__eq, fact_188_less__le__not__le, help_If_3_1_If_001t__Nat__Onat_T, fact_152_less__induct, fact_231_nth__drop, fact_24_size__neq__size__imp__neq, fact_44_drop__append, fact_187_not__le__imp__less, fact_31_diff__commute, fact_19_less__irrefl__nat, fact_26_neq__if__length__neq, fact_142_dual__order_Ostrict__trans, fact_171_ord__eq__less__subst, fact_177_dual__order_Ostrict__implies__order, fact_234_add__left__cancel, fact_112_list__desc__trans__le, fact_182_dual__order_Ostrict__trans1, fact_175_list__desc__trans, fact_17_infinite__descent, fact_78_Nat_Odiff__diff__eq, help_If_1_1_If_001t__Nat__Onat_T, fact_115_list__strict__asc__trans__le, fact_229_i__append__i__take__eq2, fact_47_append__assoc, fact_200_order__less__le__subst1, fact_38_i__append__nth2, fact_221_pinf_I4_J, fact_168_order__less__subst2, fact_185_order_Ostrict__trans2, fact_169_order__less__subst1, fact_62_Nat_Oex__has__greatest__nat, fact_57_le__trans, fact_135_linorder__wlog, fact_77_le__diff__iff, fact_151_antisym__conv3, fact_146_order_Ostrict__trans, fact_178_dual__order_Ostrict__iff__order, fact_163_less__imp__neq, fact_64_i__append__eq__i__append__conv2__aux, fact_35_i__append__i__drop__eq2, fact_114_list__asc__trans__le, fact_111_order__refl, fact_120_ord__le__eq__subst, fact_199_order__less__le__subst2, fact_193_less__imp__le, fact_140_order_Ostrict__implies__not__eq, fact_121_eq__iff, fact_159_less__linear, fact_203_less__le, fact_56_le__refl, fact_20_less__not__refl3, fact_3_length__drop, fact_180_order_Ostrict__implies__order, fact_132_order__class_Oorder_Oantisym, fact_73_less__or__eq__imp__le, fact_91_i__append__eq__i__append__conv2, fact_161_less__asym_H, fact_117_order__subst1, fact_131_ord__le__eq__trans, fact_134_dual__order_Orefl, fact_223_pinf_I2_J, fact_1_i__append__eq__i__append__conv, fact_222_pinf_I3_J, fact_29_Ex__list__of__length, fact_183_order_Ostrict__iff__order, fact_61_append__eq__appendI, fact_242_add__diff__cancel__right_H, fact_207_list__strict__desc__trans, fact_186_order_Ostrict__trans1, fact_232_nth__drop, fact_108_nth__append2, fact_103_nat__diff__left__cancel__le1, fact_243_nat__add__left__cancel__less, fact_79_diff__le__mono, fact_202_order__le__less__subst1, fact_201_order__le__less__subst2, fact_166_neqE, fact_43_i__append__def, fact_88_nat__diff__left__cancel__le2, fact_145_less__imp__not__less, fact_0_same__i__append__eq, fact_41_i__append__nth, fact_184_order_Oorder__iff__strict, fact_48_append__same__eq, fact_198_not__le, fact_164_order_Oasym, fact_214_minf_I5_J, fact_10_nat__diff__left__cancel__less, fact_122_antisym, fact_46_append_Oassoc, fact_33_i__append__i__drop__eq1, fact_39_i__append__nth2, fact_139_dual__order_Ostrict__implies__not__eq, fact_22_less__not__refl, fact_215_minf_I4_J, fact_2_i__append__eq__i__append__conv, fact_21_less__not__refl2, fact_240_add__diff__cancel__left_H, fact_60_nat__le__linear, fact_160_less__trans, fact_149_less__imp__triv, fact_76_eq__diff__iff, fact_194_antisym__conv2, fact_6_less__imp__diff__less, fact_148_linorder__cases, fact_136_dual__order_Otrans, fact_81_le__diff__iff_H, fact_50_diff__diff__cancel, fact_153_less__not__sym, fact_109_nth__append1, fact_172_list__drop__eq__conv, fact_14_length__induct, fact_125_le__cases, fact_213_minf_I7_J, fact_7_less__diff__imp__less, fact_128_antisym__conv, fact_228_minf_I6_J, fact_158_less__irrefl, fact_230_i__append__i__take__eq2, fact_71_less__imp__le__nat, fact_245_diff__diff__left, fact_235_add__le__cancel__right, fact_23_nat__neq__iff, fact_75_less__mono__imp__le__mono, fact_11_nat__diff__right__cancel__eq1, fact_99_list__eq__iff__nth__eq, fact_181_dual__order_Ostrict__trans2, fact_5_diff__less__mono2, fact_147_dual__order_Oirrefl, fact_9_nat__diff__left__cancel__eq2, fact_100_less__diff__iff, fact_189_le__imp__less__or__eq, fact_179_dual__order_Oorder__iff__strict, fact_167_gt__ex, fact_63_append__eq__append__conv2, fact_127_le__cases3, fact_89_nat__diff__right__cancel__le2, fact_208_complete__interval, fact_74_le__neq__implies__less, fact_133_order__trans, fact_45_drop__append, fact_216_minf_I3_J, fact_102_less__diff__le__imp__less, fact_227_minf_I8_J, fact_98_list__eq__iff__nth__eq, fact_137_dual__order_Oeq__iff, fact_59_le__antisym, fact_192_le__less__trans, fact_156_ord__less__eq__trans
% 19.97/5.82  % No. of inferences in proof: 508
% 19.97/5.82  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 5451 ms resp. 4596 ms w/o parsing
% 20.42/6.04  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.42/6.04  thf(list_nat_type, type, list_nat: $tType).
% 20.42/6.04  thf(list_a_type, type, list_a: $tType).
% 20.42/6.04  thf(nat_type, type, nat: $tType).
% 20.42/6.04  thf(a_type, type, a: $tType).
% 20.42/6.04  thf(minus_minus_nat_decl, type, minus_minus_nat: (nat > (nat > nat))).
% 20.42/6.04  thf(plus_plus_nat_decl, type, plus_plus_nat: (nat > (nat > nat))).
% 20.42/6.04  thf(if_nat_decl, type, if_nat: ($o > (nat > (nat > nat)))).
% 20.42/6.04  thf(if_a_decl, type, if_a: ($o > (a > (a > a)))).
% 20.42/6.04  thf(list_asc_nat_decl, type, list_asc_nat: (list_nat > $o)).
% 20.42/6.04  thf(list_desc_nat_decl, type, list_desc_nat: (list_nat > $o)).
% 20.42/6.04  thf(list_strict_asc_nat_decl, type, list_strict_asc_nat: (list_nat > $o)).
% 20.42/6.04  thf(list_strict_desc_nat_decl, type, list_strict_desc_nat: (list_nat > $o)).
% 20.42/6.04  thf(listIn923761578nd_nat_decl, type, listIn923761578nd_nat: (list_nat > ((nat > nat) > (nat > nat)))).
% 20.42/6.04  thf(listIn1312259492pend_a_decl, type, listIn1312259492pend_a: (list_a > ((nat > a) > (nat > a)))).
% 20.42/6.04  thf(listIn870223551op_nat_decl, type, listIn870223551op_nat: (nat > ((nat > nat) > (nat > nat)))).
% 20.42/6.04  thf(listIn1417627087drop_a_decl, type, listIn1417627087drop_a: (nat > ((nat > a) > (nat > a)))).
% 20.42/6.04  thf(listIn1299132951ke_nat_decl, type, listIn1299132951ke_nat: (nat > ((nat > nat) > list_nat))).
% 20.42/6.04  thf(listIn84854903take_a_decl, type, listIn84854903take_a: (nat > ((nat > a) > list_a))).
% 20.42/6.04  thf(append_nat_decl, type, append_nat: (list_nat > (list_nat > list_nat))).
% 20.42/6.04  thf(append_a_decl, type, append_a: (list_a > (list_a > list_a))).
% 20.42/6.04  thf(drop_nat_decl, type, drop_nat: (nat > (list_nat > list_nat))).
% 20.42/6.04  thf(drop_a_decl, type, drop_a: (nat > (list_a > list_a))).
% 20.42/6.04  thf(last_nat_decl, type, last_nat: (list_nat > nat)).
% 20.42/6.04  thf(last_a_decl, type, last_a: (list_a > a)).
% 20.42/6.04  thf(nth_nat_decl, type, nth_nat: (list_nat > (nat > nat))).
% 20.42/6.04  thf(nth_a_decl, type, nth_a: (list_a > (nat > a))).
% 20.42/6.04  thf(size_size_list_nat_decl, type, size_size_list_nat: (list_nat > nat)).
% 20.42/6.04  thf(size_size_list_a_decl, type, size_size_list_a: (list_a > nat)).
% 20.42/6.04  thf(ord_less_nat_decl, type, ord_less_nat: (nat > (nat > $o))).
% 20.42/6.04  thf(ord_less_eq_nat_decl, type, ord_less_eq_nat: (nat > (nat > $o))).
% 20.42/6.04  thf(f_decl, type, f: (nat > a)).
% 20.42/6.04  thf(n_decl, type, n: nat).
% 20.42/6.04  thf(xs_decl, type, xs: list_a).
% 20.42/6.04  thf(156,axiom,((! [A:nat,B:list_a,C:(nat > a)]: ((ord_less_eq_nat @ A @ (size_size_list_a @ B)) => ((listIn1417627087drop_a @ A @ (listIn1312259492pend_a @ B @ C)) = (listIn1312259492pend_a @ (drop_a @ A @ B) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_i__append__i__drop__eq1)).
% 20.42/6.04  thf(892,plain,((! [A:nat,B:list_a,C:(nat > a)]: ((ord_less_eq_nat @ A @ (size_size_list_a @ B)) => ((listIn1417627087drop_a @ A @ (listIn1312259492pend_a @ B @ C)) = (listIn1312259492pend_a @ (drop_a @ A @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 20.42/6.04  thf(238,axiom,((listIn1312259492pend_a = (^ [A:list_a,B:(nat > a),C:nat]: (if_a @ (ord_less_nat @ C @ (size_size_list_a @ A)) @ (nth_a @ A @ C) @ (B @ (minus_minus_nat @ C @ (size_size_list_a @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_i__append__nth)).
% 20.42/6.04  thf(1168,plain,(((listIn1312259492pend_a) = (^ [A:list_a,B:(nat > a),C:nat]: (if_a @ (ord_less_nat @ C @ (size_size_list_a @ A)) @ (nth_a @ A @ C) @ (B @ (minus_minus_nat @ C @ (size_size_list_a @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 20.42/6.04  thf(21,axiom,((! [A:nat,B:list_nat,C:nat]: ((ord_less_eq_nat @ A @ (size_size_list_nat @ B)) => ((nth_nat @ (drop_nat @ A @ B) @ C) = (nth_nat @ B @ (plus_plus_nat @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_nth__drop)).
% 20.42/6.04  thf(347,plain,((! [A:nat,B:list_nat,C:nat]: ((ord_less_eq_nat @ A @ (size_size_list_nat @ B)) => ((nth_nat @ (drop_nat @ A @ B) @ C) = (nth_nat @ B @ (plus_plus_nat @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 20.42/6.04  thf(162,axiom,((! [A:nat,B:nat,C:$o]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ A) => (C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_less__imp__triv)).
% 20.42/6.04  thf(909,plain,((! [A:nat,B:nat,C:$o]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ A) => (C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 20.42/6.04  thf(242,axiom,((! [A:nat,B:nat]: (ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_diff__le__self)).
% 20.42/6.04  thf(1179,plain,((! [A:nat,B:nat]: (ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 20.42/6.04  thf(211,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ (minus_minus_nat @ B @ C)) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_le__diff__imp__le)).
% 20.42/6.04  thf(1083,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ (minus_minus_nat @ B @ C)) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 20.42/6.04  thf(177,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_196_le__neq__trans)).
% 20.42/6.04  thf(962,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)],[177])).
% 20.42/6.04  thf(73,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ! [C:nat]: ((ord_less_nat @ C @ A) => (B != C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_ge__less__neq__conv)).
% 20.42/6.04  thf(523,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ! [C:nat]: ((ord_less_nat @ C @ A) => (~ (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 20.42/6.04  thf(7,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_126_order_Otrans)).
% 20.42/6.04  thf(276,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)],[7])).
% 20.42/6.04  thf(208,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_152_less__induct)).
% 20.42/6.04  thf(1068,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)],[208])).
% 20.42/6.04  thf(50,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_eq__iff)).
% 20.42/6.04  thf(449,plain,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 20.42/6.04  thf(150,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = ((ord_less_nat @ B @ A) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_not__less__iff__gr__or__eq)).
% 20.42/6.04  thf(878,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = ((ord_less_nat @ B @ A) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 20.42/6.04  thf(109,axiom,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) = (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_198_not__le)).
% 20.42/6.04  thf(677,plain,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) = (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 20.42/6.04  thf(88,axiom,((! [A:list_a,B:list_a,C:(nat > a)]: ((listIn1312259492pend_a @ A @ (listIn1312259492pend_a @ B @ C)) = (listIn1312259492pend_a @ (append_a @ A @ B) @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_i__append__assoc)).
% 20.42/6.04  thf(597,plain,((! [A:list_a,B:list_a,C:(nat > a)]: ((listIn1312259492pend_a @ A @ (listIn1312259492pend_a @ B @ C)) = (listIn1312259492pend_a @ (append_a @ A @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 20.42/6.04  thf(78,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_16_linorder__neqE__nat)).
% 20.42/6.04  thf(550,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)],[78])).
% 20.42/6.04  thf(237,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (C != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_pinf_I4_J)).
% 20.42/6.04  thf(1164,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (C = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 20.42/6.04  thf(56,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ A) => (ord_less_eq_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_dual__order_Otrans)).
% 20.42/6.04  thf(472,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ A) => (ord_less_eq_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 20.42/6.04  thf(138,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (ord_less_eq_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_less__le__not__le)).
% 20.42/6.04  thf(814,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (ord_less_eq_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 20.42/6.04  thf(115,axiom,((! [A:list_a,B:(nat > a),C:(nat > a)]: (((listIn1312259492pend_a @ A @ B) = (listIn1312259492pend_a @ A @ C)) = (B = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_same__i__append__eq)).
% 20.42/6.04  thf(698,plain,((! [A:list_a,B:(nat > a),C:(nat > a)]: (((listIn1312259492pend_a @ A @ B) = (listIn1312259492pend_a @ A @ C)) = ((B) = (C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 20.42/6.04  thf(107,axiom,((! [A:nat,B:nat]: ((minus_minus_nat @ (plus_plus_nat @ A @ B) @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_add__diff__cancel__right_H)).
% 20.42/6.04  thf(670,plain,((! [A:nat,B:nat]: ((minus_minus_nat @ (plus_plus_nat @ A @ B) @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 20.42/6.04  thf(215,axiom,((! [A:nat,B:list_nat]: ((size_size_list_nat @ (drop_nat @ A @ B)) = (minus_minus_nat @ (size_size_list_nat @ B) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3_length__drop)).
% 20.42/6.04  thf(1095,plain,((! [A:nat,B:list_nat]: ((size_size_list_nat @ (drop_nat @ A @ B)) = (minus_minus_nat @ (size_size_list_nat @ B) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 20.42/6.04  thf(248,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_le__imp__less__or__eq)).
% 20.42/6.04  thf(1196,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 20.42/6.04  thf(158,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_eq_nat @ C @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_minf_I6_J)).
% 20.42/6.04  thf(898,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_eq_nat @ C @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 20.42/6.04  thf(227,axiom,((! [A:list_nat,B:nat,C:list_nat]: ((ord_less_eq_nat @ (size_size_list_nat @ A) @ B) => ((nth_nat @ (append_nat @ A @ C) @ B) = (nth_nat @ C @ (minus_minus_nat @ B @ (size_size_list_nat @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_nth__append2)).
% 20.42/6.04  thf(1127,plain,((! [A:list_nat,B:nat,C:list_nat]: ((ord_less_eq_nat @ (size_size_list_nat @ A) @ B) => ((nth_nat @ (append_nat @ A @ C) @ B) = (nth_nat @ C @ (minus_minus_nat @ B @ (size_size_list_nat @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 20.42/6.04  thf(118,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_order__less__subst2)).
% 20.42/6.04  thf(709,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 20.42/6.04  thf(147,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_less__imp__neq)).
% 20.42/6.04  thf(841,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 20.42/6.04  thf(11,axiom,((! [A:nat,B:nat,C:nat]: (((ord_less_eq_nat @ A @ B) => (~ (ord_less_eq_nat @ B @ C))) => (((ord_less_eq_nat @ B @ A) => (~ (ord_less_eq_nat @ A @ C))) => (((ord_less_eq_nat @ A @ C) => (~ (ord_less_eq_nat @ C @ B))) => (((ord_less_eq_nat @ C @ B) => (~ (ord_less_eq_nat @ B @ A))) => (((ord_less_eq_nat @ B @ C) => (~ (ord_less_eq_nat @ C @ A))) => (~ ((ord_less_eq_nat @ C @ A) => (~ (ord_less_eq_nat @ A @ B))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_le__cases3)).
% 20.42/6.04  thf(288,plain,((! [A:nat,B:nat,C:nat]: (((ord_less_eq_nat @ A @ B) => (~ (ord_less_eq_nat @ B @ C))) => (((ord_less_eq_nat @ B @ A) => (~ (ord_less_eq_nat @ A @ C))) => (((ord_less_eq_nat @ A @ C) => (~ (ord_less_eq_nat @ C @ B))) => (((ord_less_eq_nat @ C @ B) => (~ (ord_less_eq_nat @ B @ A))) => (((ord_less_eq_nat @ B @ C) => (~ (ord_less_eq_nat @ C @ A))) => (~ ((ord_less_eq_nat @ C @ A) => (~ (ord_less_eq_nat @ A @ B))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 20.42/6.04  thf(46,axiom,((! [A:list_a,B:list_a,C:list_a,D:list_a,E:list_a]: (((append_a @ A @ B) = C) => ((D = (append_a @ B @ E)) => ((append_a @ A @ D) = (append_a @ C @ E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_append__eq__appendI)).
% 20.42/6.04  thf(436,plain,((! [A:list_a,B:list_a,C:list_a,D:list_a,E:list_a]: (((append_a @ A @ B) = C) => ((D = (append_a @ B @ E)) => ((append_a @ A @ D) = (append_a @ C @ E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 20.42/6.04  thf(180,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_eq_nat @ C @ A) => (ord_less_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_dual__order_Ostrict__trans2)).
% 20.42/6.04  thf(973,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_eq_nat @ C @ A) => (ord_less_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 20.42/6.04  thf(153,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (A != C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_le__greater__neq__conv)).
% 20.42/6.04  thf(885,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (A = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 20.42/6.04  thf(32,axiom,((! [A:list_nat]: ((list_strict_desc_nat @ A) => (list_desc_nat @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_list__strict__desc__imp__list__desc)).
% 20.42/6.04  thf(389,plain,((! [A:list_nat]: ((list_strict_desc_nat @ A) => (list_desc_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 20.42/6.04  thf(122,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_pinf_I2_J)).
% 20.42/6.04  thf(724,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 20.42/6.04  thf(121,axiom,((! [A:list_a,B:list_a,C:list_a,D:(nat > a),E:(nat > a)]: (((append_a @ A @ B) = C) => ((D = (listIn1312259492pend_a @ B @ E)) => ((listIn1312259492pend_a @ A @ D) = (listIn1312259492pend_a @ C @ E)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_i__append__eq__i__appendI)).
% 20.42/6.04  thf(719,plain,((! [A:list_a,B:list_a,C:list_a,D:(nat > a),E:(nat > a)]: (((append_a @ A @ B) = C) => (((D) = (listIn1312259492pend_a @ B @ E)) => ((listIn1312259492pend_a @ A @ D) = (listIn1312259492pend_a @ C @ E)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 20.42/6.04  thf(29,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_ord__eq__le__subst)).
% 20.42/6.04  thf(372,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 20.42/6.04  thf(67,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_dual__order_Oorder__iff__strict)).
% 20.42/6.04  thf(504,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 20.42/6.04  thf(94,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_75_less__mono__imp__le__mono)).
% 20.42/6.04  thf(619,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)],[94])).
% 20.42/6.04  thf(165,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_less__not__refl)).
% 20.42/6.04  thf(917,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 20.42/6.04  thf(169,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ (minus_minus_nat @ C @ B)) => ((ord_less_nat @ B @ A) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_nat__diff__right__cancel__le1)).
% 20.42/6.04  thf(934,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ (minus_minus_nat @ C @ B)) => ((ord_less_nat @ B @ A) => (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 20.42/6.04  thf(98,axiom,((! [A:list_nat,B:nat,C:(nat > nat)]: ((ord_less_eq_nat @ (size_size_list_nat @ A) @ B) => ((listIn870223551op_nat @ B @ (listIn923761578nd_nat @ A @ C)) = (listIn870223551op_nat @ (minus_minus_nat @ B @ (size_size_list_nat @ A)) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_i__append__i__drop__eq2)).
% 20.42/6.04  thf(638,plain,((! [A:list_nat,B:nat,C:(nat > nat)]: ((ord_less_eq_nat @ (size_size_list_nat @ A) @ B) => ((listIn870223551op_nat @ B @ (listIn923761578nd_nat @ A @ C)) = (listIn870223551op_nat @ (minus_minus_nat @ B @ (size_size_list_nat @ A)) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 20.42/6.04  thf(234,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_nat__add__left__cancel__less)).
% 20.42/6.04  thf(1147,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 20.42/6.04  thf(42,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_123_linear)).
% 20.42/6.04  thf(421,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)],[42])).
% 20.42/6.04  thf(179,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_less__imp__not__eq2)).
% 20.42/6.04  thf(969,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 20.42/6.04  thf(217,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ (minus_minus_nat @ A @ C)) => ((ord_less_eq_nat @ C @ A) => (ord_less_eq_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_nat__diff__left__cancel__le2)).
% 20.42/6.04  thf(1100,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ (minus_minus_nat @ A @ C)) => ((ord_less_eq_nat @ C @ A) => (ord_less_eq_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 20.42/6.04  thf(151,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ (minus_minus_nat @ A @ C)) => ((ord_less_nat @ B @ A) => (ord_less_eq_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_nat__diff__left__cancel__le1)).
% 20.42/6.04  thf(881,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ (minus_minus_nat @ A @ C)) => ((ord_less_nat @ B @ A) => (ord_less_eq_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 20.42/6.04  thf(41,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_order__subst1)).
% 20.42/6.04  thf(416,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 20.42/6.04  thf(57,axiom,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_ord__eq__le__trans)).
% 20.42/6.04  thf(475,plain,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 20.42/6.04  thf(125,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_113_nat__descend__induct)).
% 20.42/6.04  thf(756,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)],[125])).
% 20.42/6.04  thf(86,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_74_le__neq__implies__less)).
% 20.42/6.04  thf(591,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)],[86])).
% 20.42/6.04  thf(23,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_order__refl)).
% 20.42/6.04  thf(353,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 20.42/6.04  thf(58,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_122_antisym)).
% 20.42/6.04  thf(480,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)],[58])).
% 20.42/6.04  thf(200,axiom,((! [A:nat,B:nat,C:nat]: ((minus_minus_nat @ (minus_minus_nat @ A @ B) @ C) = (minus_minus_nat @ A @ (plus_plus_nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_diff__diff__left)).
% 20.42/6.04  thf(1040,plain,((! [A:nat,B:nat,C:nat]: ((minus_minus_nat @ (minus_minus_nat @ A @ B) @ C) = (minus_minus_nat @ A @ (plus_plus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 20.42/6.04  thf(221,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_5_diff__less__mono2)).
% 20.42/6.04  thf(1109,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)],[221])).
% 20.42/6.04  thf(18,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_eq_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_add__le__cancel__left)).
% 20.42/6.04  thf(321,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_eq_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 20.42/6.04  thf(60,axiom,((((=) @ list_a) = (^ [A:list_a,B:list_a]: (((size_size_list_a @ A) = (size_size_list_a @ B)) & ! [C:nat]: ((ord_less_nat @ C @ (size_size_list_a @ A)) => ((nth_a @ A @ C) = (nth_a @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_list__eq__iff__nth__eq)).
% 20.42/6.04  thf(485,plain,((((=) @ list_a) = (^ [A:list_a,B:list_a]: (((size_size_list_a @ A) = (size_size_list_a @ B)) & ! [C:nat]: ((ord_less_nat @ C @ (size_size_list_a @ A)) => ((nth_a @ A @ C) = (nth_a @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 20.42/6.04  thf(230,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_204_le__less)).
% 20.42/6.04  thf(1136,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 20.42/6.04  thf(183,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_less__not__refl3)).
% 20.42/6.04  thf(981,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 20.42/6.04  thf(114,axiom,((! [A:list_a,B:(nat > a),C:list_a,D:(nat > a)]: (((listIn1312259492pend_a @ A @ B) = (listIn1312259492pend_a @ C @ D)) => ((ord_less_eq_nat @ (size_size_list_a @ A) @ (size_size_list_a @ C)) => (? [E:list_a]: (((append_a @ A @ E) = C) & (B = (listIn1312259492pend_a @ E @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_i__append__eq__i__append__conv2__aux)).
% 20.42/6.04  thf(692,plain,((! [A:list_a,B:(nat > a),C:list_a,D:(nat > a)]: (((listIn1312259492pend_a @ A @ B) = (listIn1312259492pend_a @ C @ D)) => ((ord_less_eq_nat @ (size_size_list_a @ A) @ (size_size_list_a @ C)) => (? [E:list_a]: (((append_a @ A @ E) = C) & ((B) = (listIn1312259492pend_a @ E @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 21.09/6.04  thf(224,axiom,((list_desc_nat = (^ [A:list_nat]: ! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_eq_nat @ C @ B) => (ord_less_eq_nat @ (nth_nat @ A @ B) @ (nth_nat @ A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_list__desc__trans__le)).
% 21.09/6.04  thf(1119,plain,(((list_desc_nat) = (^ [A:list_nat]: ! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_eq_nat @ C @ B) => (ord_less_eq_nat @ (nth_nat @ A @ B) @ (nth_nat @ A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 21.09/6.04  thf(185,axiom,((! [A:nat,B:list_nat]: ((ord_less_nat @ A @ (size_size_list_nat @ B)) => ((last_nat @ (drop_nat @ A @ B)) = (last_nat @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_last__drop)).
% 21.09/6.04  thf(988,plain,((! [A:nat,B:list_nat]: ((ord_less_nat @ A @ (size_size_list_nat @ B)) => ((last_nat @ (drop_nat @ A @ B)) = (last_nat @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 21.09/6.04  thf(15,axiom,((! [A:list_a,B:list_a,C:list_a]: (((append_a @ A @ B) = (append_a @ C @ B)) = (A = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_append__same__eq)).
% 21.09/6.04  thf(312,plain,((! [A:list_a,B:list_a,C:list_a]: (((append_a @ A @ B) = (append_a @ C @ B)) = (A = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 21.09/6.04  thf(219,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_50_diff__diff__cancel)).
% 21.09/6.04  thf(1104,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)],[219])).
% 21.09/6.04  thf(4,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) = (ord_less_eq_nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_add__le__cancel__right)).
% 21.09/6.04  thf(265,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) = (ord_less_eq_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 21.09/6.04  thf(166,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_11_nat__diff__right__cancel__eq1)).
% 21.09/6.04  thf(920,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)],[166])).
% 21.09/6.04  thf(70,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((ord_less_eq_nat @ A @ B) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_antisym__conv1)).
% 21.09/6.04  thf(512,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((ord_less_eq_nat @ A @ B) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 21.09/6.04  thf(77,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_78_Nat_Odiff__diff__eq)).
% 21.09/6.04  thf(546,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)],[77])).
% 21.09/6.04  thf(249,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_165_neq__iff)).
% 21.09/6.04  thf(1199,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)],[249])).
% 21.09/6.04  thf(236,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_minf_I2_J)).
% 21.09/6.04  thf(1153,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => (((A @ F) | (C @ F)) = ((B @ F) | (D @ F))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 21.09/6.04  thf(137,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ B) => (((minus_minus_nat @ B @ A) = (minus_minus_nat @ B @ C)) = (A = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_eq__diff__left__iff)).
% 21.09/6.04  thf(810,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ B) => (((minus_minus_nat @ B @ A) = (minus_minus_nat @ B @ C)) = (A = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 21.09/6.04  thf(30,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((B = C) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_ord__le__eq__trans)).
% 21.09/6.04  thf(381,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((B = C) => (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 21.09/6.04  thf(28,axiom,((! [A:list_nat,B:(nat > nat),C:list_nat,D:(nat > nat)]: (((listIn923761578nd_nat @ A @ B) = (listIn923761578nd_nat @ C @ D)) => ((ord_less_eq_nat @ (size_size_list_nat @ A) @ (size_size_list_nat @ C)) => (? [E:list_nat]: (((append_nat @ A @ E) = C) & (B = (listIn923761578nd_nat @ E @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_i__append__eq__i__append__conv2__aux)).
% 21.09/6.04  thf(366,plain,((! [A:list_nat,B:(nat > nat),C:list_nat,D:(nat > nat)]: (((listIn923761578nd_nat @ A @ B) = (listIn923761578nd_nat @ C @ D)) => ((ord_less_eq_nat @ (size_size_list_nat @ A) @ (size_size_list_nat @ C)) => (? [E:list_nat]: (((append_nat @ A @ E) = C) & ((B) = (listIn923761578nd_nat @ E @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 21.09/6.04  thf(119,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((A != B) => (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_linorder__cases)).
% 21.09/6.04  thf(714,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (A = B)) => (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 21.09/6.04  thf(203,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_166_neqE)).
% 21.09/6.04  thf(1047,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)],[203])).
% 21.09/6.04  thf(133,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((~ (ord_less_nat @ A @ B)) = (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_antisym__conv2)).
% 21.09/6.04  thf(798,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((~ (ord_less_nat @ A @ B)) = (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 21.09/6.04  thf(38,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_132_order__class_Oorder_Oantisym)).
% 21.09/6.04  thf(407,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)],[38])).
% 21.09/6.04  thf(131,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_dual__order_Ostrict__implies__not__eq)).
% 21.09/6.04  thf(788,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 21.09/6.04  thf(63,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_verit__comp__simplify1_I1_J)).
% 21.09/6.04  thf(493,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 21.09/6.04  thf(111,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_nat @ C @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_minf_I5_J)).
% 21.09/6.04  thf(682,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_nat @ C @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 21.09/6.04  thf(19,axiom,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_eq_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_linorder__wlog)).
% 21.09/6.04  thf(324,plain,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_eq_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 21.09/6.04  thf(72,axiom,((! [A:list_a,B:nat,C:(nat > a)]: ((ord_less_eq_nat @ (size_size_list_a @ A) @ B) => ((listIn1417627087drop_a @ B @ (listIn1312259492pend_a @ A @ C)) = (listIn1417627087drop_a @ (minus_minus_nat @ B @ (size_size_list_a @ A)) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_i__append__i__drop__eq2)).
% 21.09/6.04  thf(519,plain,((! [A:list_a,B:nat,C:(nat > a)]: ((ord_less_eq_nat @ (size_size_list_a @ A) @ B) => ((listIn1417627087drop_a @ B @ (listIn1312259492pend_a @ A @ C)) = (listIn1417627087drop_a @ (minus_minus_nat @ B @ (size_size_list_a @ A)) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 21.09/6.04  thf(233,axiom,((! [A:nat,B:list_a,C:nat]: ((ord_less_eq_nat @ A @ (size_size_list_a @ B)) => ((nth_a @ (drop_a @ A @ B) @ C) = (nth_a @ B @ (plus_plus_nat @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_nth__drop)).
% 21.09/6.04  thf(1143,plain,((! [A:nat,B:list_a,C:nat]: ((ord_less_eq_nat @ A @ (size_size_list_a @ B)) => ((nth_a @ (drop_a @ A @ B) @ C) = (nth_a @ B @ (plus_plus_nat @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 21.09/6.04  thf(225,axiom,((! [A:nat,B:(nat > (nat > $o))]: ((! [C:nat]: ((ord_less_nat @ C @ A) => (? [D:nat]: (B @ C @ D)))) = (? [C:list_nat]: (((size_size_list_nat @ C) = A) & ! [D:nat]: ((ord_less_nat @ D @ A) => (B @ D @ (nth_nat @ C @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_Skolem__list__nth)).
% 21.09/6.04  thf(1121,plain,((! [A:nat,B:(nat > (nat > $o))]: ((! [C:nat]: ((ord_less_nat @ C @ A) => (? [D:nat]: (B @ C @ D)))) = (? [C:list_nat]: (((size_size_list_nat @ C) = A) & ! [D:nat]: ((ord_less_nat @ D @ A) => (B @ D @ (nth_nat @ C @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 21.09/6.04  thf(190,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (B != A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_dual__order_Ostrict__iff__order)).
% 21.09/6.04  thf(1006,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 21.09/6.04  thf(231,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_less__le)).
% 21.09/6.04  thf(1138,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 21.09/6.04  thf(65,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_dual__order_Oirrefl)).
% 21.09/6.04  thf(499,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 21.09/6.04  thf(101,axiom,((! [A:nat,B:nat,C:(nat > a)]: ((ord_less_eq_nat @ A @ B) => ((listIn1417627087drop_a @ A @ C @ (minus_minus_nat @ B @ A)) = (C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_i__drop__nth__sub)).
% 21.09/6.04  thf(650,plain,((! [A:nat,B:nat,C:(nat > a)]: ((ord_less_eq_nat @ A @ B) => ((listIn1417627087drop_a @ A @ (C) @ (minus_minus_nat @ B @ A)) = (C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 21.09/6.04  thf(174,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_less__irrefl__nat)).
% 21.09/6.04  thf(948,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 21.09/6.04  thf(196,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_order_Oorder__iff__strict)).
% 21.09/6.04  thf(1028,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 21.09/6.04  thf(99,axiom,((! [A:list_a,B:list_a,C:list_a,D:list_a]: ((((size_size_list_a @ A) = (size_size_list_a @ B)) | ((size_size_list_a @ C) = (size_size_list_a @ D))) => (((append_a @ A @ C) = (append_a @ B @ D)) = ((A = B) & (C = D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_append__eq__append__conv)).
% 21.09/6.04  thf(642,plain,((! [A:list_a,B:list_a,C:list_a,D:list_a]: ((((size_size_list_a @ A) = (size_size_list_a @ B)) | ((size_size_list_a @ C) = (size_size_list_a @ D))) => (((append_a @ A @ C) = (append_a @ B @ D)) = ((A = B) & (C = D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 21.09/6.04  thf(254,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_18_nat__less__induct)).
% 21.09/6.04  thf(1214,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)],[254])).
% 21.09/6.04  thf(194,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_17_infinite__descent)).
% 21.09/6.04  thf(1016,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)],[194])).
% 21.09/6.04  thf(252,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_eq_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_199_order__less__le__subst2)).
% 21.09/6.04  thf(1207,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => ((ord_less_eq_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 21.09/6.04  thf(184,axiom,((! [A:nat,B:nat]: ((A != B) => ((ord_less_eq_nat @ A @ B) => (ord_less_nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_order_Onot__eq__order__implies__strict)).
% 21.09/6.04  thf(985,plain,((! [A:nat,B:nat]: ((~ (A = B)) => ((ord_less_eq_nat @ A @ B) => (ord_less_nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 21.09/6.04  thf(116,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ (minus_minus_nat @ B @ C)) => ((ord_less_eq_nat @ D @ C) => (ord_less_eq_nat @ A @ (minus_minus_nat @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_le__diff__le__imp__le)).
% 21.09/6.04  thf(701,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ (minus_minus_nat @ B @ C)) => ((ord_less_eq_nat @ D @ C) => (ord_less_eq_nat @ A @ (minus_minus_nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 21.09/6.04  thf(204,axiom,((! [A:nat,B:list_a,C:list_a]: (((ord_less_nat @ A @ (size_size_list_a @ B)) => ((nth_a @ (append_a @ B @ C) @ A) = (nth_a @ B @ A))) & ((~ (ord_less_nat @ A @ (size_size_list_a @ B))) => ((nth_a @ (append_a @ B @ C) @ A) = (nth_a @ C @ (minus_minus_nat @ A @ (size_size_list_a @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_nth__append)).
% 21.09/6.04  thf(1050,plain,((! [A:nat,B:list_a,C:list_a]: (((ord_less_nat @ A @ (size_size_list_a @ B)) => ((nth_a @ (append_a @ B @ C) @ A) = (nth_a @ B @ A))) & ((~ (ord_less_nat @ A @ (size_size_list_a @ B))) => ((nth_a @ (append_a @ B @ C) @ A) = (nth_a @ C @ (minus_minus_nat @ A @ (size_size_list_a @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 21.09/6.04  thf(188,axiom,((list_asc_nat = (^ [A:list_nat]: ! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_eq_nat @ (nth_nat @ A @ C) @ (nth_nat @ A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_list__asc__trans)).
% 21.09/6.04  thf(1002,plain,(((list_asc_nat) = (^ [A:list_nat]: ! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_eq_nat @ (nth_nat @ A @ C) @ (nth_nat @ A @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 21.09/6.04  thf(71,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_81_le__diff__iff_H)).
% 21.09/6.04  thf(515,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)],[71])).
% 21.09/6.04  thf(235,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_79_diff__le__mono)).
% 21.09/6.04  thf(1150,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)],[235])).
% 21.09/6.04  thf(228,axiom,((! [A:nat]: ? [B:nat]: (ord_less_nat @ A @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_gt__ex)).
% 21.09/6.04  thf(1131,plain,((! [A:nat]: ? [B:nat]: (ord_less_nat @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 21.09/6.04  thf(102,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_order_Ostrict__implies__order)).
% 21.09/6.04  thf(654,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 21.09/6.04  thf(239,axiom,((listIn923761578nd_nat = (^ [A:list_nat,B:(nat > nat),C:nat]: (if_nat @ (ord_less_nat @ C @ (size_size_list_nat @ A)) @ (nth_nat @ A @ C) @ (B @ (minus_minus_nat @ C @ (size_size_list_nat @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_i__append__nth)).
% 21.09/6.04  thf(1170,plain,(((listIn923761578nd_nat) = (^ [A:list_nat,B:(nat > nat),C:nat]: (if_nat @ (ord_less_nat @ C @ (size_size_list_nat @ A)) @ (nth_nat @ A @ C) @ (B @ (minus_minus_nat @ C @ (size_size_list_nat @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 21.09/6.04  thf(35,axiom,((! [A:nat,B:nat]: ((if_nat @ ($false) @ A @ B) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_2_1_If_001t__Nat__Onat_T)).
% 21.09/6.04  thf(398,plain,((! [A:nat,B:nat]: ((if_nat @ ($false) @ A @ B) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 21.09/6.04  thf(127,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_9_nat__diff__left__cancel__eq2)).
% 21.09/6.04  thf(773,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)],[127])).
% 21.09/6.04  thf(105,axiom,((! [A:nat,B:nat,C:nat]: ((A = B) => ((minus_minus_nat @ A @ C) = (minus_minus_nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_eq__imp__diff__eq)).
% 21.09/6.04  thf(662,plain,((! [A:nat,B:nat,C:nat]: ((A = B) => ((minus_minus_nat @ A @ C) = (minus_minus_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 21.09/6.04  thf(250,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (ord_less_eq_nat @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_pinf_I6_J)).
% 21.09/6.04  thf(1202,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (ord_less_eq_nat @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 21.09/6.04  thf(132,axiom,((! [A:list_nat,B:list_nat]: (((size_size_list_nat @ A) = (size_size_list_nat @ B)) => ((! [C:nat]: ((ord_less_nat @ C @ (size_size_list_nat @ A)) => ((nth_nat @ A @ C) = (nth_nat @ B @ C)))) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_nth__equalityI)).
% 21.09/6.04  thf(792,plain,((! [A:list_nat,B:list_nat]: (((size_size_list_nat @ A) = (size_size_list_nat @ B)) => ((! [C:nat]: ((ord_less_nat @ C @ (size_size_list_nat @ A)) => ((nth_nat @ A @ C) = (nth_nat @ B @ C)))) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 21.09/6.04  thf(212,axiom,((! [A:nat,B:list_a,C:(nat > a)]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((listIn1312259492pend_a @ B @ C @ A) = (nth_a @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_i__append__nth1)).
% 21.09/6.04  thf(1086,plain,((! [A:nat,B:list_a,C:(nat > a)]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((listIn1312259492pend_a @ B @ (C) @ A) = (nth_a @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 21.09/6.04  thf(171,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ! [C:nat]: ((ord_less_eq_nat @ C @ A) => (B != C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_greater__le__neq__conv)).
% 21.09/6.04  thf(938,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ! [C:nat]: ((ord_less_eq_nat @ C @ A) => (~ (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 21.09/6.04  thf(96,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_eq_nat @ C @ A) => (ord_less_nat @ (minus_minus_nat @ A @ C) @ (minus_minus_nat @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_diff__less__mono)).
% 21.09/6.04  thf(633,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_eq_nat @ C @ A) => (ord_less_nat @ (minus_minus_nat @ A @ C) @ (minus_minus_nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 21.09/6.04  thf(26,axiom,((! [A:list_a,B:list_a,C:list_a]: ((append_a @ (append_a @ A @ B) @ C) = (append_a @ A @ (append_a @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_append__assoc)).
% 21.09/6.04  thf(360,plain,((! [A:list_a,B:list_a,C:list_a]: ((append_a @ (append_a @ A @ B) @ C) = (append_a @ A @ (append_a @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 21.09/6.04  thf(161,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_106_diff__right__commute)).
% 21.09/6.04  thf(906,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)],[161])).
% 21.09/6.04  thf(178,axiom,((! [A:nat,B:list_nat,C:(nat > nat)]: ((ord_less_nat @ A @ (size_size_list_nat @ B)) => ((listIn923761578nd_nat @ B @ C @ A) = (nth_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_i__append__nth1)).
% 21.09/6.04  thf(965,plain,((! [A:nat,B:list_nat,C:(nat > nat)]: ((ord_less_nat @ A @ (size_size_list_nat @ B)) => ((listIn923761578nd_nat @ B @ (C) @ A) = (nth_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 21.09/6.04  thf(44,axiom,((! [A:list_nat,B:list_nat,C:list_nat,D:list_nat]: ((((size_size_list_nat @ A) = (size_size_list_nat @ B)) | ((size_size_list_nat @ C) = (size_size_list_nat @ D))) => (((append_nat @ A @ C) = (append_nat @ B @ D)) = ((A = B) & (C = D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_append__eq__append__conv)).
% 21.09/6.04  thf(425,plain,((! [A:list_nat,B:list_nat,C:list_nat,D:list_nat]: ((((size_size_list_nat @ A) = (size_size_list_nat @ B)) | ((size_size_list_nat @ C) = (size_size_list_nat @ D))) => (((append_nat @ A @ C) = (append_nat @ B @ D)) = ((A = B) & (C = D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 21.09/6.04  thf(3,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_If_001t__Nat__Onat_T)).
% 21.09/6.04  thf(264,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 21.09/6.04  thf(8,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_dual__order_Oantisym)).
% 21.09/6.04  thf(279,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 21.09/6.04  thf(48,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_133_order__trans)).
% 21.09/6.04  thf(444,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)],[48])).
% 21.09/6.04  thf(140,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ B) => ((ord_less_eq_nat @ (minus_minus_nat @ B @ C) @ A) = (ord_less_eq_nat @ (minus_minus_nat @ B @ A) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_le__diff__swap)).
% 21.09/6.04  thf(819,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ B) => ((ord_less_eq_nat @ (minus_minus_nat @ B @ C) @ A) = (ord_less_eq_nat @ (minus_minus_nat @ B @ A) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 21.09/6.04  thf(43,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_order__class_Oorder_Oeq__iff)).
% 21.09/6.04  thf(423,plain,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 21.09/6.04  thf(10,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_le__refl)).
% 21.09/6.04  thf(286,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 21.09/6.04  thf(226,axiom,((! [A:nat,B:nat]: ((minus_minus_nat @ (plus_plus_nat @ A @ B) @ A) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_add__diff__cancel__left_H)).
% 21.09/6.04  thf(1124,plain,((! [A:nat,B:nat]: ((minus_minus_nat @ (plus_plus_nat @ A @ B) @ A) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 21.09/6.04  thf(40,axiom,((! [A:nat,B:nat]: ((A = B) | ~ (ord_less_eq_nat @ A @ B) | ~ (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_verit__la__disequality)).
% 21.09/6.04  thf(413,plain,((! [A:nat,B:nat]: ((A = B) | ~ (ord_less_eq_nat @ A @ B) | ~ (ord_less_eq_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 21.09/6.04  thf(142,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_nat__less__le)).
% 21.09/6.04  thf(826,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 21.09/6.04  thf(84,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_218_minf_I1_J)).
% 21.09/6.04  thf(577,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ F @ E) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 21.09/6.04  thf(33,axiom,((! [A:a,B:a]: ((if_a @ ($true) @ A @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_1_1_If_001tf__a_T)).
% 21.09/6.04  thf(391,plain,((! [A:a,B:a]: ((if_a @ ($true) @ A @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 21.09/6.04  thf(170,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_less__imp__not__less)).
% 21.09/6.04  thf(936,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 21.09/6.04  thf(83,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_order__less__le__subst1)).
% 21.09/6.04  thf(572,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 21.09/6.04  thf(54,axiom,((! [A:a,B:a]: ((if_a @ ($false) @ A @ B) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_2_1_If_001tf__a_T)).
% 21.09/6.04  thf(466,plain,((! [A:a,B:a]: ((if_a @ ($false) @ A @ B) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 21.09/6.04  thf(213,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (minus_minus_nat @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_le__imp__diff__le)).
% 21.09/6.04  thf(1090,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (minus_minus_nat @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 21.09/6.04  thf(135,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) = (ord_less_nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_add__less__cancel__right)).
% 21.09/6.04  thf(804,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) = (ord_less_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 21.09/6.04  thf(117,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_order__le__less__subst1)).
% 21.09/6.04  thf(704,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 21.09/6.04  thf(205,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ A @ C) => (((minus_minus_nat @ B @ A) = (minus_minus_nat @ C @ A)) = (B = C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_eq__diff__iff)).
% 21.09/6.04  thf(1058,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ A @ C) => (((minus_minus_nat @ B @ A) = (minus_minus_nat @ C @ A)) = (B = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 21.09/6.04  thf(220,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ (minus_minus_nat @ C @ B)) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_nat__diff__right__cancel__le2)).
% 21.09/6.04  thf(1107,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ (minus_minus_nat @ C @ B)) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 21.09/6.04  thf(247,axiom,((((?) @ nat) = (^ [A:(nat > $o)]: ? [B:nat]: ((A @ B) & ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_exists__least__iff)).
% 21.09/6.04  thf(1194,plain,((((?) @ nat) = (^ [A:(nat > $o)]: ? [B:nat]: ((A @ B) & ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 21.09/6.04  thf(159,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_23_nat__neq__iff)).
% 21.09/6.04  thf(900,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)],[159])).
% 21.09/6.04  thf(144,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((B = C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_ord__less__eq__trans)).
% 21.09/6.04  thf(831,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((B = C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 21.09/6.04  thf(130,axiom,((! [A:list_a,B:nat,C:list_a]: ((ord_less_eq_nat @ (size_size_list_a @ A) @ B) => ((nth_a @ (append_a @ A @ C) @ B) = (nth_a @ C @ (minus_minus_nat @ B @ (size_size_list_a @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_nth__append2)).
% 21.09/6.04  thf(784,plain,((! [A:list_a,B:nat,C:list_a]: ((ord_less_eq_nat @ (size_size_list_a @ A) @ B) => ((nth_a @ (append_a @ A @ C) @ B) = (nth_a @ C @ (minus_minus_nat @ B @ (size_size_list_a @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 21.09/6.04  thf(201,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (ord_less_eq_nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_pinf_I8_J)).
% 21.09/6.04  thf(1043,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (ord_less_eq_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 21.09/6.04  thf(12,axiom,((! [A:nat,B:nat,C:nat]: (((plus_plus_nat @ A @ B) = (plus_plus_nat @ C @ B)) = (A = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_add__right__cancel)).
% 21.09/6.04  thf(303,plain,((! [A:nat,B:nat,C:nat]: (((plus_plus_nat @ A @ B) = (plus_plus_nat @ C @ B)) = (A = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 21.09/6.04  thf(182,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ! [C:nat]: ((ord_less_eq_nat @ B @ C) => (A != C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_less__ge__neq__conv)).
% 21.09/6.04  thf(979,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ! [C:nat]: ((ord_less_eq_nat @ B @ C) => (~ (A = C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 21.09/6.04  thf(90,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (C != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_pinf_I3_J)).
% 21.09/6.04  thf(604,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (C = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 21.09/6.04  thf(51,axiom,((! [A:list_a,B:list_a,C:list_a,D:list_a]: (((append_a @ A @ B) = (append_a @ C @ D)) = (? [E:list_a]: (((A = (append_a @ C @ E)) & ((append_a @ E @ B) = D)) | (((append_a @ A @ E) = C) & (B = (append_a @ E @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_append__eq__append__conv2)).
% 21.09/6.04  thf(451,plain,((! [A:list_a,B:list_a,C:list_a,D:list_a]: (((append_a @ A @ B) = (append_a @ C @ D)) = (? [E:list_a]: (((A = (append_a @ C @ E)) & ((append_a @ E @ B) = D)) | (((append_a @ A @ E) = C) & (B = (append_a @ E @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 21.09/6.04  thf(82,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_order__le__less__subst2)).
% 21.09/6.04  thf(567,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 21.09/6.04  thf(124,axiom,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat]: (A @ D @ D)) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_linorder__less__wlog)).
% 21.09/6.04  thf(737,plain,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat,E:nat]: ((ord_less_nat @ D @ E) => (A @ D @ E))) => ((! [D:nat]: (A @ D @ D)) => ((! [D:nat,E:nat]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 21.09/6.04  thf(17,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_eq_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_nat__add__left__cancel__le)).
% 21.09/6.04  thf(318,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_eq_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 21.09/6.04  thf(155,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_dual__order_Ostrict__implies__order)).
% 21.09/6.04  thf(890,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 21.09/6.04  thf(210,axiom,((! [A:nat,B:(nat > (a > $o))]: ((! [C:nat]: ((ord_less_nat @ C @ A) => (? [D:a]: (B @ C @ D)))) = (? [C:list_a]: (((size_size_list_a @ C) = A) & ! [D:nat]: ((ord_less_nat @ D @ A) => (B @ D @ (nth_a @ C @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_Skolem__list__nth)).
% 21.09/6.04  thf(1080,plain,((! [A:nat,B:(nat > (a > $o))]: ((! [C:nat]: ((ord_less_nat @ C @ A) => (? [D:a]: (B @ C @ D)))) = (? [C:list_a]: (((size_size_list_a @ C) = A) & ! [D:nat]: ((ord_less_nat @ D @ A) => (B @ D @ (nth_a @ C @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 21.09/6.04  thf(139,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_82_diff__le__mono2)).
% 21.09/6.04  thf(816,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)],[139])).
% 21.09/6.04  thf(87,axiom,((! [A:nat]: ? [B:list_a]: ((size_size_list_a @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_Ex__list__of__length)).
% 21.09/6.04  thf(594,plain,((! [A:nat]: ? [B:list_a]: ((size_size_list_a @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 21.09/6.04  thf(59,axiom,((list_asc_nat = (^ [A:list_nat]: ! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_eq_nat @ C @ B) => (ord_less_eq_nat @ (nth_nat @ A @ C) @ (nth_nat @ A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_list__asc__trans__le)).
% 21.09/6.04  thf(483,plain,(((list_asc_nat) = (^ [A:list_nat]: ! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_eq_nat @ C @ B) => (ord_less_eq_nat @ (nth_nat @ A @ C) @ (nth_nat @ A @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 21.09/6.04  thf(149,axiom,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less_nat @ A @ B) => ((C @ A) => ((~ (C @ B)) => (? [D:nat]: ((ord_less_eq_nat @ A @ D) & (ord_less_eq_nat @ D @ B) & ! [E:nat]: (((ord_less_eq_nat @ A @ E) & (ord_less_nat @ E @ D)) => (C @ E)) & ! [E:nat]: ((! [F:nat]: (((ord_less_eq_nat @ A @ F) & (ord_less_nat @ F @ E)) => (C @ F))) => (ord_less_eq_nat @ E @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_complete__interval)).
% 21.09/6.04  thf(848,plain,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less_nat @ A @ B) => ((C @ A) => ((~ (C @ B)) => (? [D:nat]: ((ord_less_eq_nat @ A @ D) & (ord_less_eq_nat @ D @ B) & ! [E:nat]: (((ord_less_eq_nat @ A @ E) & (ord_less_nat @ E @ D)) => (C @ E)) & ! [E:nat]: ((! [F:nat]: (((ord_less_eq_nat @ A @ F) & (ord_less_nat @ F @ E)) => (C @ F))) => (ord_less_eq_nat @ E @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 21.09/6.04  thf(164,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_dual__order_Oasym)).
% 21.09/6.04  thf(915,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 21.09/6.04  thf(126,axiom,((! [A:list_a,B:list_a,C:(nat > a),D:(nat > a)]: (((size_size_list_a @ A) = (size_size_list_a @ B)) => (((listIn1312259492pend_a @ A @ C) = (listIn1312259492pend_a @ B @ D)) = ((A = B) & (C = D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_i__append__eq__i__append__conv)).
% 21.09/6.04  thf(769,plain,((! [A:list_a,B:list_a,C:(nat > a),D:(nat > a)]: (((size_size_list_a @ A) = (size_size_list_a @ B)) => (((listIn1312259492pend_a @ A @ C) = (listIn1312259492pend_a @ B @ D)) = ((A = B) & ((C) = (D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 21.09/6.04  thf(168,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_leD)).
% 21.09/6.04  thf(932,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 21.09/6.04  thf(222,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_less__not__refl2)).
% 21.09/6.04  thf(1112,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 21.09/6.04  thf(163,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_add__less__cancel__left)).
% 21.09/6.04  thf(912,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (ord_less_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 21.09/6.04  thf(97,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_less__imp__le)).
% 21.09/6.04  thf(636,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 21.09/6.04  thf(207,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_leI)).
% 21.09/6.04  thf(1066,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => (ord_less_eq_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 21.09/6.04  thf(152,axiom,((list_desc_nat = (^ [A:list_nat]: ! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_eq_nat @ (nth_nat @ A @ B) @ (nth_nat @ A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_list__desc__trans)).
% 21.09/6.04  thf(883,plain,(((list_desc_nat) = (^ [A:list_nat]: ! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_eq_nat @ (nth_nat @ A @ B) @ (nth_nat @ A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 21.09/6.04  thf(81,axiom,((! [A:list_nat,B:nat,C:(nat > nat)]: ((ord_less_eq_nat @ (size_size_list_nat @ A) @ B) => ((listIn923761578nd_nat @ A @ C @ B) = (C @ (minus_minus_nat @ B @ (size_size_list_nat @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_i__append__nth2)).
% 21.09/6.04  thf(563,plain,((! [A:list_nat,B:nat,C:(nat > nat)]: ((ord_less_eq_nat @ (size_size_list_nat @ A) @ B) => ((listIn923761578nd_nat @ A @ (C) @ B) = (C @ (minus_minus_nat @ B @ (size_size_list_nat @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 21.09/6.04  thf(218,axiom,((((=) @ list_nat) = (^ [A:list_nat,B:list_nat]: (((size_size_list_nat @ A) = (size_size_list_nat @ B)) & ! [C:nat]: ((ord_less_nat @ C @ (size_size_list_nat @ A)) => ((nth_nat @ A @ C) = (nth_nat @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_list__eq__iff__nth__eq)).
% 21.09/6.04  thf(1102,plain,((((=) @ list_nat) = (^ [A:list_nat,B:list_nat]: (((size_size_list_nat @ A) = (size_size_list_nat @ B)) & ! [C:nat]: ((ord_less_nat @ C @ (size_size_list_nat @ A)) => ((nth_nat @ A @ C) = (nth_nat @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 21.09/6.04  thf(45,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_order__subst2)).
% 21.09/6.04  thf(431,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 21.09/6.04  thf(241,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_12_nat__diff__right__cancel__eq2)).
% 21.09/6.04  thf(1176,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)],[241])).
% 21.09/6.04  thf(91,axiom,((! [A:list_nat,B:nat,C:(nat > nat)]: ((ord_less_eq_nat @ (size_size_list_nat @ A) @ B) => ((listIn1299132951ke_nat @ B @ (listIn923761578nd_nat @ A @ C)) = (append_nat @ A @ (listIn1299132951ke_nat @ (minus_minus_nat @ B @ (size_size_list_nat @ A)) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_i__append__i__take__eq2)).
% 21.09/6.04  thf(608,plain,((! [A:list_nat,B:nat,C:(nat > nat)]: ((ord_less_eq_nat @ (size_size_list_nat @ A) @ B) => ((listIn1299132951ke_nat @ B @ (listIn923761578nd_nat @ A @ C)) = (append_nat @ A @ (listIn1299132951ke_nat @ (minus_minus_nat @ B @ (size_size_list_nat @ A)) @ (C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 21.09/6.04  thf(34,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_eq__refl)).
% 21.09/6.04  thf(394,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 21.09/6.04  thf(13,axiom,((! [A:list_nat,B:list_nat,C:(nat > nat),D:(nat > nat)]: (((size_size_list_nat @ A) = (size_size_list_nat @ B)) => (((listIn923761578nd_nat @ A @ C) = (listIn923761578nd_nat @ B @ D)) = ((A = B) & (C = D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_i__append__eq__i__append__conv)).
% 21.09/6.04  thf(306,plain,((! [A:list_nat,B:list_nat,C:(nat > nat),D:(nat > nat)]: (((size_size_list_nat @ A) = (size_size_list_nat @ B)) => (((listIn923761578nd_nat @ A @ C) = (listIn923761578nd_nat @ B @ D)) = ((A = B) & ((C) = (D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 21.09/6.04  thf(198,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_order_Ostrict__trans)).
% 21.09/6.04  thf(1034,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 21.09/6.04  thf(62,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ C @ A) => (ord_less_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_dual__order_Ostrict__trans1)).
% 21.09/6.04  thf(490,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ C @ A) => (ord_less_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 21.09/6.04  thf(173,axiom,((! [A:list_a,B:nat,C:(nat > a)]: ((ord_less_eq_nat @ (size_size_list_a @ A) @ B) => ((listIn84854903take_a @ B @ (listIn1312259492pend_a @ A @ C)) = (append_a @ A @ (listIn84854903take_a @ (minus_minus_nat @ B @ (size_size_list_a @ A)) @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_i__append__i__take__eq2)).
% 21.09/6.04  thf(944,plain,((! [A:list_a,B:nat,C:(nat > a)]: ((ord_less_eq_nat @ (size_size_list_a @ A) @ B) => ((listIn84854903take_a @ B @ (listIn1312259492pend_a @ A @ C)) = (append_a @ A @ (listIn84854903take_a @ (minus_minus_nat @ B @ (size_size_list_a @ A)) @ (C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 21.09/6.04  thf(110,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_less__imp__le__nat)).
% 21.09/6.04  thf(680,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 21.09/6.04  thf(1,conjecture,((((ord_less_nat @ n @ (size_size_list_a @ xs)) => ((listIn1417627087drop_a @ n @ (listIn1312259492pend_a @ xs @ f)) = (listIn1312259492pend_a @ (drop_a @ n @ xs) @ f))) & ((~ (ord_less_nat @ n @ (size_size_list_a @ xs))) => ((listIn1417627087drop_a @ n @ (listIn1312259492pend_a @ xs @ f)) = (listIn1417627087drop_a @ (minus_minus_nat @ n @ (size_size_list_a @ xs)) @ f))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 21.09/6.04  thf(2,negated_conjecture,((~ (((ord_less_nat @ n @ (size_size_list_a @ xs)) => ((listIn1417627087drop_a @ n @ (listIn1312259492pend_a @ xs @ f)) = (listIn1312259492pend_a @ (drop_a @ n @ xs) @ f))) & ((~ (ord_less_nat @ n @ (size_size_list_a @ xs))) => ((listIn1417627087drop_a @ n @ (listIn1312259492pend_a @ xs @ f)) = (listIn1417627087drop_a @ (minus_minus_nat @ n @ (size_size_list_a @ xs)) @ f)))))),inference(neg_conjecture,[status(cth)],[1])).
% 21.09/6.04  thf(255,plain,((~ (((ord_less_nat @ n @ (size_size_list_a @ xs)) => ((listIn1417627087drop_a @ n @ (listIn1312259492pend_a @ xs @ f)) = (listIn1312259492pend_a @ (drop_a @ n @ xs) @ f))) & ((~ (ord_less_nat @ n @ (size_size_list_a @ xs))) => ((listIn1417627087drop_a @ n @ (listIn1312259492pend_a @ xs @ f)) = (listIn1417627087drop_a @ (minus_minus_nat @ n @ (size_size_list_a @ xs)) @ f)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 21.09/6.04  thf(93,axiom,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) => (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_not__le__imp__less)).
% 21.09/6.04  thf(617,plain,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) => (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 21.09/6.04  thf(24,axiom,((! [A:nat,B:nat,C:nat]: (((plus_plus_nat @ A @ B) = (plus_plus_nat @ A @ C)) = (B = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_add__left__cancel)).
% 21.09/6.04  thf(355,plain,((! [A:nat,B:nat,C:nat]: (((plus_plus_nat @ A @ B) = (plus_plus_nat @ A @ C)) = (B = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 21.09/6.04  thf(79,axiom,((! [A:nat,B:list_nat,C:list_nat]: ((ord_less_nat @ A @ (size_size_list_nat @ B)) => ((nth_nat @ (append_nat @ B @ C) @ A) = (nth_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_nth__append1)).
% 21.09/6.04  thf(553,plain,((! [A:nat,B:list_nat,C:list_nat]: ((ord_less_nat @ A @ (size_size_list_nat @ B)) => ((nth_nat @ (append_nat @ B @ C) @ A) = (nth_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 21.09/6.04  thf(145,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (ord_less_nat @ B @ A)) = (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_antisym__conv3)).
% 21.09/6.04  thf(836,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (ord_less_nat @ B @ A)) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 21.09/6.04  thf(100,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_pinf_I7_J)).
% 21.09/6.04  thf(648,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 21.09/6.04  thf(61,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_order_Ostrict__trans1)).
% 21.09/6.04  thf(487,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 21.09/6.04  thf(243,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_31_diff__commute)).
% 21.09/6.04  thf(1181,plain,((! [A:nat,B:nat,C:nat]: ((minus_minus_nat @ (minus_minus_nat @ A @ B) @ C) = (minus_minus_nat @ (minus_minus_nat @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 21.09/6.04  thf(141,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_6_less__imp__diff__less)).
% 21.09/6.04  thf(823,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)],[141])).
% 21.09/6.04  thf(128,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_order__less__subst1)).
% 21.09/6.04  thf(776,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((ord_less_nat @ A @ (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 21.09/6.04  thf(74,axiom,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_pinf_I1_J)).
% 21.09/6.04  thf(525,plain,((! [A:(nat > $o),B:(nat > $o),C:(nat > $o),D:(nat > $o)]: ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((A @ F) = (B @ F)))) => ((? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => ((C @ F) = (D @ F)))) => (? [E:nat]: ! [F:nat]: ((ord_less_nat @ E @ F) => (((A @ F) & (C @ F)) = ((B @ F) & (D @ F))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 21.09/6.04  thf(80,axiom,((! [A:list_a,B:list_a]: (((size_size_list_a @ A) = (size_size_list_a @ B)) => ((! [C:nat]: ((ord_less_nat @ C @ (size_size_list_a @ A)) => ((nth_a @ A @ C) = (nth_a @ B @ C)))) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_nth__equalityI)).
% 21.09/6.04  thf(557,plain,((! [A:list_a,B:list_a]: (((size_size_list_a @ A) = (size_size_list_a @ B)) => ((! [C:nat]: ((ord_less_nat @ C @ (size_size_list_a @ A)) => ((nth_a @ A @ C) = (nth_a @ B @ C)))) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 21.09/6.04  thf(195,axiom,((! [A:nat,B:list_a]: ((size_size_list_a @ (drop_a @ A @ B)) = (minus_minus_nat @ (size_size_list_a @ B) @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_length__drop)).
% 21.09/6.04  thf(1025,plain,((! [A:nat,B:list_a]: ((size_size_list_a @ (drop_a @ A @ B)) = (minus_minus_nat @ (size_size_list_a @ B) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 21.09/6.04  thf(9,axiom,((! [A:nat,B:list_nat,C:(nat > nat)]: ((ord_less_eq_nat @ A @ (size_size_list_nat @ B)) => ((listIn870223551op_nat @ A @ (listIn923761578nd_nat @ B @ C)) = (listIn923761578nd_nat @ (drop_nat @ A @ B) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_i__append__i__drop__eq1)).
% 21.09/6.04  thf(282,plain,((! [A:nat,B:list_nat,C:(nat > nat)]: ((ord_less_eq_nat @ A @ (size_size_list_nat @ B)) => ((listIn870223551op_nat @ A @ (listIn923761578nd_nat @ B @ C)) = (listIn923761578nd_nat @ (drop_nat @ A @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 21.09/6.04  thf(154,axiom,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) = (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_verit__comp__simplify1_I3_J)).
% 21.09/6.04  thf(887,plain,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) = (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 21.09/6.04  thf(187,axiom,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_ord__eq__less__subst)).
% 21.09/6.04  thf(993,plain,((! [A:nat,B:(nat > nat),C:nat,D:nat]: ((A = (B @ C)) => ((ord_less_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (B @ E) @ (B @ F)))) => (ord_less_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 21.09/6.04  thf(216,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_le__eq__less__or__eq)).
% 21.09/6.04  thf(1098,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 21.09/6.04  thf(14,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_dual__order_Orefl)).
% 21.09/6.04  thf(310,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 21.09/6.04  thf(108,axiom,((! [A:list_a,B:nat,C:(nat > a)]: ((ord_less_eq_nat @ (size_size_list_a @ A) @ B) => ((listIn1312259492pend_a @ A @ C @ B) = (C @ (minus_minus_nat @ B @ (size_size_list_a @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_i__append__nth2)).
% 21.09/6.04  thf(673,plain,((! [A:list_a,B:nat,C:(nat > a)]: ((ord_less_eq_nat @ (size_size_list_a @ A) @ B) => ((listIn1312259492pend_a @ A @ (C) @ B) = (C @ (minus_minus_nat @ B @ (size_size_list_a @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 21.09/6.04  thf(47,axiom,((! [A:list_a,B:list_a,C:list_a]: (((append_a @ A @ B) = (append_a @ A @ C)) = (B = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_same__append__eq)).
% 21.09/6.04  thf(441,plain,((! [A:list_a,B:list_a,C:list_a]: (((append_a @ A @ B) = (append_a @ A @ C)) = (B = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 21.09/6.04  thf(120,axiom,((! [A:list_nat]: ((list_strict_asc_nat @ A) => (! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_eq_nat @ C @ B) => (ord_less_eq_nat @ (nth_nat @ A @ C) @ (nth_nat @ A @ B))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_list__strict__asc__trans__le)).
% 21.09/6.04  thf(717,plain,((! [A:list_nat]: ((list_strict_asc_nat @ A) => (! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_eq_nat @ C @ B) => (ord_less_eq_nat @ (nth_nat @ A @ C) @ (nth_nat @ A @ B))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 21.09/6.04  thf(66,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_162_less__asym)).
% 21.09/6.04  thf(502,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 21.09/6.04  thf(53,axiom,((! [A:nat,B:nat]: ((if_nat @ ($true) @ A @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_1_1_If_001t__Nat__Onat_T)).
% 21.09/6.04  thf(463,plain,((! [A:nat,B:nat]: ((if_nat @ ($true) @ A @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 21.09/6.04  thf(175,axiom,((! [A:(list_nat > $o),B:list_nat]: ((! [C:list_nat]: ((! [D:list_nat]: ((ord_less_nat @ (size_size_list_nat @ D) @ (size_size_list_nat @ C)) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14_length__induct)).
% 21.09/6.04  thf(951,plain,((! [A:(list_nat > $o),B:list_nat]: ((! [C:list_nat]: ((! [D:list_nat]: ((ord_less_nat @ (size_size_list_nat @ D) @ (size_size_list_nat @ C)) => (A @ D))) => (A @ C))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 21.09/6.04  thf(76,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_13_nat__diff__right__cancel__less)).
% 21.09/6.04  thf(544,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)],[76])).
% 21.09/6.04  thf(20,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_62_Nat_Oex__has__greatest__nat)).
% 21.09/6.04  thf(331,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)],[20])).
% 21.09/6.04  thf(246,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_73_less__or__eq__imp__le)).
% 21.09/6.04  thf(1188,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)],[246])).
% 21.09/6.04  thf(245,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_minf_I7_J)).
% 21.09/6.04  thf(1186,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 21.09/6.04  thf(103,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_8_nat__diff__left__cancel__eq1)).
% 21.09/6.04  thf(656,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)],[103])).
% 21.09/6.04  thf(89,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_order_Ostrict__implies__not__eq)).
% 21.09/6.04  thf(600,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 21.09/6.04  thf(191,axiom,((((=) @ list_a) = (^ [A:list_a,B:list_a]: ! [C:nat]: ((drop_a @ C @ A) = (drop_a @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_list__drop__eq__conv)).
% 21.09/6.04  thf(1008,plain,((((=) @ list_a) = (^ [A:list_a,B:list_a]: ! [C:nat]: ((drop_a @ C @ A) = (drop_a @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 21.09/6.04  thf(92,axiom,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_ord__eq__less__trans)).
% 21.09/6.04  thf(612,plain,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 21.09/6.04  thf(186,axiom,((listIn923761578nd_nat = (^ [A:list_nat,B:(nat > nat),C:nat]: (if_nat @ (ord_less_nat @ C @ (size_size_list_nat @ A)) @ (nth_nat @ A @ C) @ (B @ (minus_minus_nat @ C @ (size_size_list_nat @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_i__append__def)).
% 21.09/6.04  thf(991,plain,(((listIn923761578nd_nat) = (^ [A:list_nat,B:(nat > nat),C:nat]: (if_nat @ (ord_less_nat @ C @ (size_size_list_nat @ A)) @ (nth_nat @ A @ C) @ (B @ (minus_minus_nat @ C @ (size_size_list_nat @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 21.09/6.04  thf(232,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_eq_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_order_Ostrict__trans2)).
% 21.09/6.04  thf(1140,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_eq_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 21.09/6.04  thf(31,axiom,((! [A:nat]: ? [B:list_nat]: ((size_size_list_nat @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_Ex__list__of__length)).
% 21.09/6.04  thf(386,plain,((! [A:nat]: ? [B:list_nat]: ((size_size_list_nat @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 21.09/6.04  thf(148,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ A) => (ord_less_nat @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_dual__order_Ostrict__trans)).
% 21.09/6.04  thf(845,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ C @ A) => (ord_less_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 21.09/6.04  thf(27,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) = (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_antisym__conv)).
% 21.09/6.04  thf(363,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 21.09/6.04  thf(192,axiom,((! [A:list_a,B:list_a]: (((size_size_list_a @ A) != (size_size_list_a @ B)) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_neq__if__length__neq)).
% 21.09/6.04  thf(1010,plain,((! [A:list_a,B:list_a]: ((~ ((size_size_list_a @ A) = (size_size_list_a @ B))) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 21.09/6.04  thf(181,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_less__irrefl)).
% 21.09/6.04  thf(976,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 21.09/6.04  thf(113,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_less__imp__not__eq)).
% 21.09/6.04  thf(688,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 21.09/6.04  thf(160,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_not__less)).
% 21.09/6.04  thf(903,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = (ord_less_eq_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 21.09/6.04  thf(85,axiom,((! [A:nat,B:nat,C:nat]: ((minus_minus_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) = (minus_minus_nat @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_add__diff__cancel__right)).
% 21.09/6.04  thf(588,plain,((! [A:nat,B:nat,C:nat]: ((minus_minus_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ C @ B)) = (minus_minus_nat @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 21.09/6.04  thf(157,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) | (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_le__less__linear)).
% 21.09/6.04  thf(896,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) | (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 21.09/6.04  thf(206,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (C != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_minf_I3_J)).
% 21.09/6.04  thf(1062,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (C = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 21.09/6.04  thf(22,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_60_nat__le__linear)).
% 21.09/6.04  thf(351,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)],[22])).
% 21.09/6.04  thf(36,axiom,((! [A:list_nat,B:list_nat]: (((size_size_list_nat @ A) != (size_size_list_nat @ B)) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_size__neq__size__imp__neq)).
% 21.09/6.04  thf(401,plain,((! [A:list_nat,B:list_nat]: ((~ ((size_size_list_nat @ A) = (size_size_list_nat @ B))) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 21.09/6.04  thf(129,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_7_less__diff__imp__less)).
% 21.09/6.04  thf(781,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)],[129])).
% 21.09/6.04  thf(197,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (C != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_minf_I4_J)).
% 21.09/6.04  thf(1030,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (C = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 21.09/6.04  thf(69,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_less__not__sym)).
% 21.09/6.04  thf(510,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 21.09/6.04  thf(106,axiom,((! [A:nat,B:nat,C:nat]: ((minus_minus_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (minus_minus_nat @ B @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_add__diff__cancel__left)).
% 21.09/6.04  thf(667,plain,((! [A:nat,B:nat,C:nat]: ((minus_minus_nat @ (plus_plus_nat @ A @ B) @ (plus_plus_nat @ A @ C)) = (minus_minus_nat @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 21.09/6.04  thf(209,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B) | (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_less__linear)).
% 21.09/6.04  thf(1077,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B) | (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 21.09/6.04  thf(253,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_order_Ostrict__iff__order)).
% 21.09/6.04  thf(1212,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 21.09/6.04  thf(6,axiom,((! [A:list_nat,B:list_nat]: (((size_size_list_nat @ A) != (size_size_list_nat @ B)) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_neq__if__length__neq)).
% 21.09/6.04  thf(272,plain,((! [A:list_nat,B:list_nat]: ((~ ((size_size_list_nat @ A) = (size_size_list_nat @ B))) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 21.09/6.04  thf(112,axiom,((! [A:nat,B:list_a,C:list_a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((nth_a @ (append_a @ B @ C) @ A) = (nth_a @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_nth__append1)).
% 21.09/6.04  thf(684,plain,((! [A:nat,B:list_a,C:list_a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((nth_a @ (append_a @ B @ C) @ A) = (nth_a @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 21.09/6.04  thf(75,axiom,((! [A:nat,B:list_nat,C:list_nat]: (((ord_less_nat @ A @ (size_size_list_nat @ B)) => ((nth_nat @ (append_nat @ B @ C) @ A) = (nth_nat @ B @ A))) & ((~ (ord_less_nat @ A @ (size_size_list_nat @ B))) => ((nth_nat @ (append_nat @ B @ C) @ A) = (nth_nat @ C @ (minus_minus_nat @ A @ (size_size_list_nat @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_nth__append)).
% 21.09/6.04  thf(536,plain,((! [A:nat,B:list_nat,C:list_nat]: (((ord_less_nat @ A @ (size_size_list_nat @ B)) => ((nth_nat @ (append_nat @ B @ C) @ A) = (nth_nat @ B @ A))) & ((~ (ord_less_nat @ A @ (size_size_list_nat @ B))) => ((nth_nat @ (append_nat @ B @ C) @ A) = (nth_nat @ C @ (minus_minus_nat @ A @ (size_size_list_nat @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 21.09/6.04  thf(202,axiom,((list_strict_asc_nat = (^ [A:list_nat]: ! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_nat @ (nth_nat @ A @ C) @ (nth_nat @ A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_list__strict__asc__trans)).
% 21.09/6.04  thf(1045,plain,(((list_strict_asc_nat) = (^ [A:list_nat]: ! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_nat @ (nth_nat @ A @ C) @ (nth_nat @ A @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 21.09/6.04  thf(223,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_le__less__trans)).
% 21.09/6.04  thf(1116,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 21.09/6.04  thf(229,axiom,((! [A:nat,B:nat,C:list_a]: ((drop_a @ A @ (drop_a @ B @ C)) = (drop_a @ (plus_plus_nat @ A @ B) @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_drop__drop)).
% 21.09/6.04  thf(1133,plain,((! [A:nat,B:nat,C:list_a]: ((drop_a @ A @ (drop_a @ B @ C)) = (drop_a @ (plus_plus_nat @ A @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 21.09/6.04  thf(49,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ B @ A) & (ord_less_eq_nat @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_dual__order_Oeq__iff)).
% 21.09/6.04  thf(447,plain,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ B @ A) & (ord_less_eq_nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 21.09/6.04  thf(16,axiom,((! [A:list_a,B:list_a,C:list_a]: ((append_a @ (append_a @ A @ B) @ C) = (append_a @ A @ (append_a @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_append_Oassoc)).
% 21.09/6.04  thf(315,plain,((! [A:list_a,B:list_a,C:list_a]: ((append_a @ (append_a @ A @ B) @ C) = (append_a @ A @ (append_a @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 21.09/6.04  thf(39,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_59_le__antisym)).
% 21.09/6.04  thf(410,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)],[39])).
% 21.09/6.04  thf(37,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_125_le__cases)).
% 21.09/6.04  thf(405,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)],[37])).
% 21.09/6.04  thf(123,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_minf_I8_J)).
% 21.09/6.04  thf(735,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 21.09/6.04  thf(134,axiom,((! [A:list_a,B:(nat > a),C:list_a,D:(nat > a)]: (((listIn1312259492pend_a @ A @ B) = (listIn1312259492pend_a @ C @ D)) = (? [E:list_a]: (((A = (append_a @ C @ E)) & ((listIn1312259492pend_a @ E @ B) = D)) | (((append_a @ A @ E) = C) & (B = (listIn1312259492pend_a @ E @ D)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_i__append__eq__i__append__conv2)).
% 21.09/6.04  thf(801,plain,((! [A:list_a,B:(nat > a),C:list_a,D:(nat > a)]: (((listIn1312259492pend_a @ A @ B) = (listIn1312259492pend_a @ C @ D)) = (? [E:list_a]: (((A = (append_a @ C @ E)) & ((listIn1312259492pend_a @ E @ B) = (D))) | (((append_a @ A @ E) = C) & ((B) = (listIn1312259492pend_a @ E @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 21.09/6.04  thf(240,axiom,((! [A:list_a,B:list_a]: (((size_size_list_a @ A) != (size_size_list_a @ B)) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_size__neq__size__imp__neq)).
% 21.09/6.04  thf(1172,plain,((! [A:list_a,B:list_a]: ((~ ((size_size_list_a @ A) = (size_size_list_a @ B))) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 21.09/6.04  thf(143,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_eq_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_less__le__trans)).
% 21.09/6.04  thf(828,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_eq_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 21.09/6.04  thf(176,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_164_order_Oasym)).
% 21.09/6.04  thf(960,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 21.09/6.04  thf(68,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_77_le__diff__iff)).
% 21.09/6.04  thf(506,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)],[68])).
% 21.09/6.04  thf(5,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_eq__imp__le)).
% 21.09/6.04  thf(268,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 21.09/6.04  thf(25,axiom,((! [A:list_nat]: ((list_strict_asc_nat @ A) => (list_asc_nat @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_list__strict__asc__imp__list__asc)).
% 21.09/6.04  thf(358,plain,((! [A:list_nat]: ((list_strict_asc_nat @ A) => (list_asc_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 21.09/6.04  thf(136,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ (minus_minus_nat @ B @ C)) => ((ord_less_eq_nat @ D @ C) => (ord_less_nat @ A @ (minus_minus_nat @ B @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_less__diff__le__imp__less)).
% 21.09/6.04  thf(807,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_nat @ A @ (minus_minus_nat @ B @ C)) => ((ord_less_eq_nat @ D @ C) => (ord_less_nat @ A @ (minus_minus_nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 21.09/6.04  thf(189,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_less__asym_H)).
% 21.09/6.04  thf(1004,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 21.09/6.04  thf(214,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_10_nat__diff__left__cancel__less)).
% 21.09/6.04  thf(1093,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)],[214])).
% 21.09/6.04  thf(95,axiom,((! [A:(list_a > $o),B:list_a]: ((! [C:list_a]: ((! [D:list_a]: ((ord_less_nat @ (size_size_list_a @ D) @ (size_size_list_a @ C)) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_length__induct)).
% 21.09/6.04  thf(624,plain,((! [A:(list_a > $o),B:list_a]: ((! [C:list_a]: ((! [D:list_a]: ((ord_less_nat @ (size_size_list_a @ D) @ (size_size_list_a @ C)) => (A @ D))) => (A @ C))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 21.09/6.04  thf(146,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (ord_less_nat @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_pinf_I5_J)).
% 21.09/6.04  thf(839,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (ord_less_nat @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 21.09/6.04  thf(167,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_ord__less__eq__subst)).
% 21.09/6.04  thf(923,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_nat @ E @ F) => (ord_less_nat @ (C @ E) @ (C @ F)))) => (ord_less_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 21.09/6.04  thf(244,axiom,((list_strict_desc_nat = (^ [A:list_nat]: ! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_nat @ (nth_nat @ A @ B) @ (nth_nat @ A @ C)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_list__strict__desc__trans)).
% 21.09/6.04  thf(1184,plain,(((list_strict_desc_nat) = (^ [A:list_nat]: ! [B:nat]: ((ord_less_nat @ B @ (size_size_list_nat @ A)) => (! [C:nat]: ((ord_less_nat @ C @ B) => (ord_less_nat @ (nth_nat @ A @ B) @ (nth_nat @ A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 21.09/6.04  thf(104,axiom,((! [A:nat,B:list_nat,C:list_nat]: ((drop_nat @ A @ (append_nat @ B @ C)) = (append_nat @ (drop_nat @ A @ B) @ (drop_nat @ (minus_minus_nat @ A @ (size_size_list_nat @ B)) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_drop__append)).
% 21.09/6.04  thf(659,plain,((! [A:nat,B:list_nat,C:list_nat]: ((drop_nat @ A @ (append_nat @ B @ C)) = (append_nat @ (drop_nat @ A @ B) @ (drop_nat @ (minus_minus_nat @ A @ (size_size_list_nat @ B)) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 21.09/6.04  thf(199,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_less__trans)).
% 21.09/6.04  thf(1037,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 21.09/6.04  thf(251,axiom,((! [A:nat,B:list_a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((last_a @ (drop_a @ A @ B)) = (last_a @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_last__drop)).
% 21.09/6.04  thf(1204,plain,((! [A:nat,B:list_a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((last_a @ (drop_a @ A @ B)) = (last_a @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 21.09/6.04  thf(193,axiom,((listIn1312259492pend_a = (^ [A:list_a,B:(nat > a),C:nat]: (if_a @ (ord_less_nat @ C @ (size_size_list_a @ A)) @ (nth_a @ A @ C) @ (B @ (minus_minus_nat @ C @ (size_size_list_a @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_i__append__def)).
% 21.09/6.04  thf(1014,plain,(((listIn1312259492pend_a) = (^ [A:list_a,B:(nat > a),C:nat]: (if_a @ (ord_less_nat @ C @ (size_size_list_a @ A)) @ (nth_a @ A @ C) @ (B @ (minus_minus_nat @ C @ (size_size_list_a @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 21.09/6.04  thf(55,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_57_le__trans)).
% 21.09/6.04  thf(469,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)],[55])).
% 21.09/6.04  thf(172,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ A @ C) => ((ord_less_nat @ (minus_minus_nat @ B @ A) @ (minus_minus_nat @ C @ A)) = (ord_less_nat @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_less__diff__iff)).
% 21.09/6.04  thf(940,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ A @ C) => ((ord_less_nat @ (minus_minus_nat @ B @ A) @ (minus_minus_nat @ C @ A)) = (ord_less_nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 21.09/6.04  thf(64,axiom,((! [A:nat,B:list_a,C:list_a]: ((drop_a @ A @ (append_a @ B @ C)) = (append_a @ (drop_a @ A @ B) @ (drop_a @ (minus_minus_nat @ A @ (size_size_list_a @ B)) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_drop__append)).
% 21.09/6.04  thf(496,plain,((! [A:nat,B:list_a,C:list_a]: ((drop_a @ A @ (append_a @ B @ C)) = (append_a @ (drop_a @ A @ B) @ (drop_a @ (minus_minus_nat @ A @ (size_size_list_a @ B)) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 21.09/6.04  thf(52,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_ord__le__eq__subst)).
% 21.09/6.04  thf(454,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((ord_less_eq_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 21.09/6.04  thf(1409,plain,(($false)),inference(e,[status(thm)],[892,1168,347,909,1179,1083,962,523,276,1068,449,878,677,597,550,1164,472,814,698,670,1095,1196,898,1127,709,841,288,436,973,885,389,724,719,372,504,619,917,934,638,1147,421,969,1100,881,416,475,756,591,353,480,1040,1109,321,485,1136,981,692,1119,988,312,1104,265,920,512,546,1199,1153,810,381,366,714,1047,798,407,788,493,682,324,519,1143,1121,1006,1138,499,650,948,1028,642,1214,1016,1207,985,701,1050,1002,515,1150,1131,654,1170,398,773,662,1202,792,1086,938,633,360,906,965,425,264,279,444,819,423,286,1124,413,826,577,391,936,572,466,1090,804,704,1058,1107,1194,900,831,784,1043,303,979,604,451,567,737,318,890,1080,816,594,483,848,915,769,932,1112,912,636,1066,883,563,1102,431,1176,608,394,306,1034,490,944,680,255,617,355,553,836,648,487,1181,823,776,525,557,1025,282,887,993,1098,310,673,441,717,502,463,951,544,331,1188,1186,656,600,1008,612,991,1140,386,845,363,1010,976,688,903,588,896,1062,351,401,781,1030,510,667,1077,1212,272,684,536,1045,1116,1133,447,315,410,405,735,801,1172,828,960,506,268,358,807,1004,1093,624,839,923,1184,659,1037,1204,1014,469,940,496,454])).
% 21.09/6.04  % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.09/6.04  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------