%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP101^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:46 AM UTC 2026
% Result : Theorem 15.44s 4.86s
% Output : Refutation 16.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP101^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.11/0.21 % Computer : n003.cluster.edu
% 0.11/0.21 % Model : x86_64 x86_64
% 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.21 % Memory : 8046.5625MB
% 0.11/0.21 % OS : Linux 6.8.0-71-generic
% 0.11/0.21 % CPULimit : 300
% 0.11/0.21 % WCLimit : 300
% 0.11/0.21 % DateTime : Tue Sep 29 19:55:29 UTC 2026
% 0.11/0.21 % CPUTime :
% 0.11/0.21 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.05/0.81 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.01/1.20 % [INFO] Parsing done (384ms).
% 2.37/1.21 % [INFO] Running in sequential loop mode.
% 3.54/1.61 % [INFO] eprover registered as external prover.
% 3.54/1.62 % [INFO] Scanning for conjecture ...
% 3.71/1.75 % [INFO] Found a conjecture (or negated_conjecture) and 266 axioms. Running axiom selection ...
% 3.89/1.88 % [INFO] Axiom selection finished. Selected 221 axioms (removed 45 axioms).
% 4.59/2.11 % [INFO] Problem is higher-order (TPTP THF).
% 4.90/2.14 % [INFO] Type checking passed.
% 4.90/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 ...
% 15.44/4.85 % External prover 'e' found a proof!
% 15.44/4.85 % [INFO] Killing All external provers ...
% 15.44/4.85 % Time passed: 4495ms (effective reasoning time: 3634ms)
% 15.44/4.85 % 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)>
% 15.44/4.86 % Axioms used in derivation (221): fact_121_list__update__same__conv, fact_241_subset__code_I1_J, fact_175_less__asym, fact_219_le__neq__trans, fact_75_nat__le__linear, fact_177_order_Oasym, fact_154_not__less__iff__gr__or__eq, fact_136_linear, fact_91_le__eq__less__or__eq, fact_16_infinite__descent, fact_90_less__imp__le__nat, fact_153_order_Ostrict__implies__not__eq, fact_97_Nat_Odiff__diff__eq, fact_15_linorder__neqE__nat, fact_218_antisym__conv1, fact_13_nat__diff__left__cancel__less, fact_246_in__set__butlast__appendI, fact_162_less__imp__triv, help_If_1_1_If_001tf__a_T, fact_190_pinf_I7_J, fact_187_pinf_I3_J, fact_103_le__diff__imp__le, fact_92_less__or__eq__imp__le, fact_127_order__refl, fact_186_pinf_I2_J, fact_156_linorder__less__wlog, fact_104_le__imp__diff__le, fact_32_i__append__nth, fact_220_not__less, fact_21_less__not__refl, fact_185_pinf_I1_J, fact_98_diff__le__mono, fact_206_order_Ostrict__iff__order, fact_173_less__trans, fact_217_antisym__conv2, fact_133_ord__le__eq__subst, fact_130_order__subst1, fact_36_length__induct, fact_234_verit__comp__simplify1_I3_J, fact_245_list__ex__cong, fact_214_less__le__trans, fact_107_nat__diff__left__cancel__le2, fact_30_diff__commute, fact_240_length__butlast, fact_145_order__class_Oorder_Oantisym, fact_3_Skolem__list__nth, fact_131_order__subst2, fact_62_length__list__update, fact_54_append__assoc, fact_56_same__append__eq, fact_52_Collect__mem__eq, fact_71_le__refl, fact_191_minf_I1_J, fact_119_nth__list__update, fact_5_list__eq__iff__nth__eq, fact_1_nth__equalityI, fact_232_minf_I6_J, fact_165_less__induct, fact_29_eq__imp__diff__eq, fact_135_antisym, fact_201_dual__order_Ostrict__iff__order, fact_57_list__update__overwrite, fact_213_le__less__linear, fact_149_dual__order_Otrans, fact_221_not__le, fact_18_less__irrefl__nat, help_If_2_1_If_001tf__a_T, fact_70_list__update__beyond, fact_147_dual__order_Orefl, fact_254_all__nth__imp__all__set, fact_231_pinf_I8_J, fact_256_all__set__conv__all__nth, fact_85_ge__less__neq__conv, fact_105_eq__diff__left__iff, fact_148_linorder__wlog, fact_44_i__append__nth2, fact_8_diff__less__mono2, fact_74_le__antisym, fact_77_append__eq__appendI, fact_193_minf_I3_J, fact_161_linorder__cases, fact_116_nat__diff__left__cancel__le1, fact_192_minf_I2_J, fact_225_order__le__less__subst1, fact_168_dual__order_Oasym, fact_73_eq__imp__le, fact_195_minf_I5_J, conj_2, fact_178_neq__iff, fact_223_order__less__le__subst1, fact_28_Ex__list__of__length, fact_84_nth__append2, fact_19_less__not__refl3, fact_89_nat__less__le, fact_159_order_Ostrict__trans, fact_37_nat__diff__right__cancel__less, fact_67_list__ex__append, fact_224_order__le__less__subst2, help_If_3_1_If_001t__Nat__Onat_T, fact_24_size__neq__size__imp__neq, fact_230_pinf_I6_J, fact_20_less__not__refl2, fact_78_Nat_Oex__has__greatest__nat, fact_179_neqE, fact_100_le__diff__iff_H, fact_26_neq__if__length__neq, fact_22_nat__neq__iff, fact_86_less__ge__neq__conv, fact_93_le__neq__implies__less, fact_257_verit__la__disequality, fact_250_list__ball__nth, fact_229_leD, fact_72_le__trans, fact_10_less__diff__imp__less, fact_94_less__mono__imp__le__mono, fact_242_set__update__subsetI, fact_152_dual__order_Ostrict__implies__not__eq, fact_158_less__imp__not__less, fact_236_set__swap, fact_88_le__greater__neq__conv, fact_146_order__trans, fact_55_append__same__eq, fact_243_in__set__butlastD, fact_172_less__linear, fact_226_less__le, fact_17_nat__less__induct, fact_42_list__ex__length, fact_51_mem__Collect__eq, fact_106_le__diff__le__imp__le, fact_200_dual__order_Ostrict__implies__order, fact_113_less__diff__iff, fact_139_order_Otrans, fact_167_less__imp__not__eq, fact_58_diff__diff__cancel, fact_64_list__update__id, fact_155_dual__order_Ostrict__trans, fact_138_le__cases, fact_181_order__less__subst2, fact_244_one__reorient, fact_150_dual__order_Oeq__iff, fact_101_diff__le__mono2, fact_34_i__append__def, fact_129_minf_I8_J, fact_48_nth__list__update__eq, fact_53_append_Oassoc, fact_182_order__less__subst1, fact_176_less__imp__neq, fact_122_diff__right__commute, fact_151_dual__order_Oantisym, fact_171_less__irrefl, fact_204_dual__order_Ostrict__trans2, fact_110_list__update__append, fact_199_order_Onot__eq__order__implies__strict, fact_208_order_Ostrict__trans2, fact_14_nat__diff__right__cancel__eq1, fact_68_i__append__assoc, fact_248_nth__mem, conj_1, fact_76_list__update__swap, fact_205_dual__order_Ostrict__trans1, fact_132_ord__eq__le__subst, fact_144_ord__le__eq__trans, fact_140_le__cases3, fact_183_ord__less__eq__subst, fact_238_butlast__list__update, fact_174_less__asym_H, fact_66_nth__list__update__neq, fact_189_pinf_I5_J, fact_114_diff__less__mono, fact_170_ord__eq__less__trans, fact_222_order__less__le__subst2, fact_115_less__diff__le__imp__less, fact_112_nth__append1, fact_216_less__imp__le, fact_143_ord__eq__le__trans, fact_202_dual__order_Oorder__iff__strict, fact_46_nth__append, fact_95_eq__diff__iff, fact_233_complete__interval, fact_169_ord__less__eq__trans, fact_7_i__append__nth1, fact_207_order_Oorder__iff__strict, fact_211_less__le__not__le, fact_79_append__eq__append__conv2, fact_99_diff__le__self, fact_82_list__update__append1, fact_128_nat__descend__induct, fact_209_order_Ostrict__trans1, fact_38_nat__diff__right__cancel__eq2, fact_87_greater__le__neq__conv, fact_180_gt__ex, fact_9_less__imp__diff__less, fact_227_le__less, fact_210_not__le__imp__less, fact_60_append__eq__append__conv, fact_141_antisym__conv, fact_194_minf_I4_J, fact_11_nat__diff__left__cancel__eq1, fact_163_less__imp__not__eq2, fact_196_minf_I7_J, conj_0, fact_160_dual__order_Oirrefl, fact_166_less__not__sym, fact_108_nat__diff__right__cancel__le2, fact_50_nth__butlast, fact_184_ord__eq__less__subst, fact_142_order__class_Oorder_Oeq__iff, fact_96_le__diff__iff, fact_157_exists__least__iff, fact_215_le__less__trans, fact_12_nat__diff__left__cancel__eq2, fact_188_pinf_I4_J, fact_212_le__imp__less__or__eq, fact_102_le__diff__swap, fact_203_order_Ostrict__implies__order, fact_252_in__set__conv__nth, fact_164_antisym__conv3, fact_117_nat__diff__right__cancel__le1, fact_134_eq__iff, fact_228_leI, fact_137_eq__refl
% 15.44/4.86 % No. of inferences in proof: 446
% 15.44/4.86 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 4495 ms resp. 3634 ms w/o parsing
% 16.79/5.05 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.79/5.05 thf(list_nat_type, type, list_nat: $tType).
% 16.79/5.05 thf(set_nat_type, type, set_nat: $tType).
% 16.79/5.05 thf(list_a_type, type, list_a: $tType).
% 16.79/5.05 thf(set_a_type, type, set_a: $tType).
% 16.79/5.05 thf(nat_type, type, nat: $tType).
% 16.79/5.05 thf(a_type, type, a: $tType).
% 16.79/5.05 thf(minus_minus_nat_decl, type, minus_minus_nat: (nat > (nat > nat))).
% 16.79/5.05 thf(one_one_nat_decl, type, one_one_nat: nat).
% 16.79/5.05 thf(if_a_decl, type, if_a: ($o > (a > (a > a)))).
% 16.79/5.05 thf(listIn1312259492pend_a_decl, type, listIn1312259492pend_a: (list_a > ((nat > a) > (nat > a)))).
% 16.79/5.05 thf(append_a_decl, type, append_a: (list_a > (list_a > list_a))).
% 16.79/5.05 thf(butlast_a_decl, type, butlast_a: (list_a > list_a)).
% 16.79/5.05 thf(set_a2_decl, type, set_a2: (list_a > set_a)).
% 16.79/5.05 thf(list_ex_a_decl, type, list_ex_a: ((a > $o) > (list_a > $o))).
% 16.79/5.05 thf(list_update_a_decl, type, list_update_a: (list_a > (nat > (a > list_a)))).
% 16.79/5.05 thf(nth_a_decl, type, nth_a: (list_a > (nat > a))).
% 16.79/5.05 thf(size_size_list_a_decl, type, size_size_list_a: (list_a > nat)).
% 16.79/5.05 thf(ord_less_nat_decl, type, ord_less_nat: (nat > (nat > $o))).
% 16.79/5.05 thf(ord_less_eq_nat_decl, type, ord_less_eq_nat: (nat > (nat > $o))).
% 16.79/5.05 thf(ord_less_eq_set_a_decl, type, ord_less_eq_set_a: (set_a > (set_a > $o))).
% 16.79/5.05 thf(collect_a_decl, type, collect_a: ((a > $o) > set_a)).
% 16.79/5.05 thf(member_a_decl, type, member_a: (a > (set_a > $o))).
% 16.79/5.05 thf(f_decl, type, f: (nat > a)).
% 16.79/5.05 thf(g_decl, type, g: (nat > a)).
% 16.79/5.05 thf(x_decl, type, x: nat).
% 16.79/5.05 thf(xs_decl, type, xs: list_a).
% 16.79/5.05 thf(ys_decl, type, ys: list_a).
% 16.79/5.05 thf(84,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_15_linorder__neqE__nat)).
% 16.79/5.05 thf(518,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)],[84])).
% 16.79/5.05 thf(11,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_131_order__subst2)).
% 16.79/5.05 thf(249,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)],[11])).
% 16.79/5.05 thf(34,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_133_ord__le__eq__subst)).
% 16.79/5.05 thf(333,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)],[34])).
% 16.79/5.05 thf(112,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_130_order__subst1)).
% 16.79/5.05 thf(628,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)],[112])).
% 16.79/5.05 thf(194,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_97_Nat_Odiff__diff__eq)).
% 16.79/5.05 thf(977,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)],[194])).
% 16.79/5.05 thf(216,axiom,((! [A:nat,B:list_a,C:a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((nth_a @ (list_update_a @ B @ A @ C) @ A) = C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_nth__list__update__eq)).
% 16.79/5.05 thf(1073,plain,((! [A:nat,B:list_a,C:a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((nth_a @ (list_update_a @ B @ A @ C) @ A) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 16.79/5.05 thf(120,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_122_diff__right__commute)).
% 16.79/5.05 thf(655,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)],[120])).
% 16.79/5.05 thf(163,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_113_less__diff__iff)).
% 16.79/5.05 thf(861,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)],[163])).
% 16.79/5.05 thf(167,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_dual__order_Ostrict__implies__not__eq)).
% 16.79/5.05 thf(873,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 16.79/5.05 thf(62,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_93_le__neq__implies__less)).
% 16.79/5.05 thf(449,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)],[62])).
% 16.79/5.05 thf(134,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_146_order__trans)).
% 16.79/5.05 thf(715,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)],[134])).
% 16.79/5.05 thf(145,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_less__not__refl2)).
% 16.79/5.05 thf(747,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 16.79/5.05 thf(186,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_108_nat__diff__right__cancel__le2)).
% 16.79/5.05 thf(945,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)],[186])).
% 16.79/5.05 thf(214,axiom,((! [A:list_a,B:(a > $o),C:a]: ((! [D:nat]: ((ord_less_nat @ D @ (size_size_list_a @ A)) => (B @ (nth_a @ A @ D)))) => ((member_a @ C @ (set_a2 @ A)) => (B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_254_all__nth__imp__all__set)).
% 16.79/5.05 thf(1063,plain,((! [A:list_a,B:(a > $o),C:a]: ((! [D:nat]: ((ord_less_nat @ D @ (size_size_list_a @ A)) => (B @ (nth_a @ A @ D)))) => ((member_a @ C @ (set_a2 @ A)) => (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 16.79/5.05 thf(155,axiom,((! [A:nat,B:nat,C:nat]: ((minus_minus_nat @ (minus_minus_nat @ A @ B) @ C) = (minus_minus_nat @ (minus_minus_nat @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_diff__commute)).
% 16.79/5.05 thf(829,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)],[155])).
% 16.79/5.05 thf(131,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_less__asym)).
% 16.79/5.05 thf(709,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 16.79/5.05 thf(158,axiom,((! [A:nat,B:list_a,C:a]: (((A = (minus_minus_nat @ (size_size_list_a @ B) @ one_one_nat)) => ((butlast_a @ (list_update_a @ B @ A @ C)) = (butlast_a @ B))) & ((A != (minus_minus_nat @ (size_size_list_a @ B) @ one_one_nat)) => ((butlast_a @ (list_update_a @ B @ A @ C)) = (list_update_a @ (butlast_a @ B) @ A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_butlast__list__update)).
% 16.79/5.05 thf(841,plain,((! [A:nat,B:list_a,C:a]: (((A = (minus_minus_nat @ (size_size_list_a @ B) @ one_one_nat)) => ((butlast_a @ (list_update_a @ B @ A @ C)) = (butlast_a @ B))) & ((~ (A = (minus_minus_nat @ (size_size_list_a @ B) @ one_one_nat))) => ((butlast_a @ (list_update_a @ B @ A @ C)) = (list_update_a @ (butlast_a @ B) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 16.79/5.05 thf(29,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_order_Ostrict__iff__order)).
% 16.79/5.05 thf(320,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 16.79/5.05 thf(58,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_179_neqE)).
% 16.79/5.05 thf(436,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)],[58])).
% 16.79/5.05 thf(118,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_157_exists__least__iff)).
% 16.79/5.05 thf(651,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)],[118])).
% 16.79/5.05 thf(13,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_211_less__le__not__le)).
% 16.79/5.05 thf(257,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)],[13])).
% 16.79/5.05 thf(137,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_149_dual__order_Otrans)).
% 16.79/5.05 thf(724,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)],[137])).
% 16.79/5.05 thf(79,axiom,((! [A:list_a,B:nat,C:a,D:a]: ((list_update_a @ (list_update_a @ A @ B @ C) @ B @ D) = (list_update_a @ A @ B @ D)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_list__update__overwrite)).
% 16.79/5.05 thf(504,plain,((! [A:list_a,B:nat,C:a,D:a]: ((list_update_a @ (list_update_a @ A @ B @ C) @ B @ D) = (list_update_a @ A @ B @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 16.79/5.05 thf(157,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_54_append__assoc)).
% 16.79/5.05 thf(838,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)],[157])).
% 16.79/5.05 thf(146,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_nat__less__le)).
% 16.79/5.05 thf(751,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 16.79/5.05 thf(213,axiom,((! [A:nat,B:nat,C:list_a,D:a]: ((A != B) => ((nth_a @ (list_update_a @ C @ A @ D) @ B) = (nth_a @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_nth__list__update__neq)).
% 16.79/5.05 thf(1059,plain,((! [A:nat,B:nat,C:list_a,D:a]: ((~ (A = B)) => ((nth_a @ (list_update_a @ C @ A @ D) @ B) = (nth_a @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 16.79/5.05 thf(66,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_208_order_Ostrict__trans2)).
% 16.79/5.05 thf(460,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)],[66])).
% 16.79/5.05 thf(166,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_22_nat__neq__iff)).
% 16.79/5.05 thf(870,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)],[166])).
% 16.79/5.05 thf(31,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_214_less__le__trans)).
% 16.79/5.05 thf(325,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)],[31])).
% 16.79/5.05 thf(21,axiom,((! [A:nat,B:nat,C:nat]: ((A = B) => ((minus_minus_nat @ A @ C) = (minus_minus_nat @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_eq__imp__diff__eq)).
% 16.79/5.05 thf(289,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)],[21])).
% 16.79/5.05 thf(223,axiom,((! [A:nat,B:list_a,C:(a > $o)]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((! [D:a]: ((member_a @ D @ (set_a2 @ B)) => (C @ D))) => (C @ (nth_a @ B @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_list__ball__nth)).
% 16.79/5.05 thf(1100,plain,((! [A:nat,B:list_a,C:(a > $o)]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((! [D:a]: ((member_a @ D @ (set_a2 @ B)) => (C @ D))) => (C @ (nth_a @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 16.79/5.05 thf(115,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_order__refl)).
% 16.79/5.05 thf(638,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 16.79/5.05 thf(160,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_56_same__append__eq)).
% 16.79/5.05 thf(853,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)],[160])).
% 16.79/5.05 thf(75,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_102_le__diff__swap)).
% 16.79/5.05 thf(492,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)],[75])).
% 16.79/5.05 thf(207,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_84_nth__append2)).
% 16.79/5.05 thf(1040,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)],[207])).
% 16.79/5.05 thf(183,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_98_diff__le__mono)).
% 16.79/5.05 thf(937,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)],[183])).
% 16.79/5.05 thf(192,axiom,((! [A:nat,B:list_a,C:list_a,D:a]: (((ord_less_nat @ A @ (size_size_list_a @ B)) => ((list_update_a @ (append_a @ B @ C) @ A @ D) = (append_a @ (list_update_a @ B @ A @ D) @ C))) & ((~ (ord_less_nat @ A @ (size_size_list_a @ B))) => ((list_update_a @ (append_a @ B @ C) @ A @ D) = (append_a @ B @ (list_update_a @ C @ (minus_minus_nat @ A @ (size_size_list_a @ B)) @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_list__update__append)).
% 16.79/5.05 thf(966,plain,((! [A:nat,B:list_a,C:list_a,D:a]: (((ord_less_nat @ A @ (size_size_list_a @ B)) => ((list_update_a @ (append_a @ B @ C) @ A @ D) = (append_a @ (list_update_a @ B @ A @ D) @ C))) & ((~ (ord_less_nat @ A @ (size_size_list_a @ B))) => ((list_update_a @ (append_a @ B @ C) @ A @ D) = (append_a @ B @ (list_update_a @ C @ (minus_minus_nat @ A @ (size_size_list_a @ B)) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 16.79/5.05 thf(72,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_less__imp__not__eq2)).
% 16.79/5.05 thf(480,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 16.79/5.05 thf(97,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_164_antisym__conv3)).
% 16.79/5.05 thf(574,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)],[97])).
% 16.79/5.05 thf(202,axiom,((! [A:nat,B:list_a,C:nat,D:a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => (((A = C) => ((nth_a @ (list_update_a @ B @ A @ D) @ C) = D)) & ((A != C) => ((nth_a @ (list_update_a @ B @ A @ D) @ C) = (nth_a @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_nth__list__update)).
% 16.79/5.05 thf(1020,plain,((! [A:nat,B:list_a,C:nat,D:a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => (((A = C) => ((nth_a @ (list_update_a @ B @ A @ D) @ C) = D)) & ((~ (A = C)) => ((nth_a @ (list_update_a @ B @ A @ D) @ C) = (nth_a @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 16.79/5.05 thf(37,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_151_dual__order_Oantisym)).
% 16.79/5.05 thf(348,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)],[37])).
% 16.79/5.05 thf(195,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_170_ord__eq__less__trans)).
% 16.79/5.05 thf(981,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)],[195])).
% 16.79/5.05 thf(20,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_36_length__induct)).
% 16.79/5.05 thf(280,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)],[20])).
% 16.79/5.05 thf(168,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_185_pinf_I1_J)).
% 16.79/5.05 thf(877,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)],[168])).
% 16.79/5.05 thf(140,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_101_diff__le__mono2)).
% 16.79/5.05 thf(734,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)],[140])).
% 16.79/5.05 thf(122,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_156_linorder__less__wlog)).
% 16.79/5.05 thf(660,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)],[122])).
% 16.79/5.05 thf(54,axiom,((! [A:nat]: ? [B:nat]: (ord_less_nat @ A @ B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_gt__ex)).
% 16.79/5.05 thf(411,plain,((! [A:nat]: ? [B:nat]: (ord_less_nat @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 16.79/5.05 thf(56,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (C != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_minf_I4_J)).
% 16.79/5.05 thf(428,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (C = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 16.79/5.05 thf(80,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_129_minf_I8_J)).
% 16.79/5.05 thf(507,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)],[80])).
% 16.79/5.05 thf(63,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_44_i__append__nth2)).
% 16.79/5.05 thf(452,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)],[63])).
% 16.79/5.05 thf(45,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_189_pinf_I5_J)).
% 16.79/5.05 thf(380,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)],[45])).
% 16.79/5.05 thf(59,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_217_antisym__conv2)).
% 16.79/5.05 thf(439,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)],[59])).
% 16.79/5.05 thf(40,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_139_order_Otrans)).
% 16.79/5.05 thf(366,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)],[40])).
% 16.79/5.05 thf(88,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_173_less__trans)).
% 16.79/5.05 thf(534,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)],[88])).
% 16.79/5.05 thf(209,axiom,(((size_size_list_a @ xs) = (size_size_list_a @ ys))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 16.79/5.05 thf(1047,plain,(((size_size_list_a @ xs) = (size_size_list_a @ ys))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 16.79/5.05 thf(212,axiom,((! [A:nat,B:list_a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => (member_a @ (nth_a @ B @ A) @ (set_a2 @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_nth__mem)).
% 16.79/5.05 thf(1057,plain,((! [A:nat,B:list_a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => (member_a @ (nth_a @ B @ A) @ (set_a2 @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 16.79/5.05 thf(189,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_104_le__imp__diff__le)).
% 16.79/5.05 thf(952,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)],[189])).
% 16.79/5.05 thf(25,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_205_dual__order_Ostrict__trans1)).
% 16.79/5.05 thf(302,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)],[25])).
% 16.79/5.05 thf(104,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_148_linorder__wlog)).
% 16.79/5.05 thf(598,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)],[104])).
% 16.79/5.05 thf(154,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_183_ord__less__eq__subst)).
% 16.79/5.05 thf(820,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)],[154])).
% 16.79/5.05 thf(53,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_less__imp__not__eq)).
% 16.79/5.05 thf(407,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 16.79/5.05 thf(150,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_204_dual__order_Ostrict__trans2)).
% 16.79/5.05 thf(788,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)],[150])).
% 16.79/5.05 thf(204,axiom,((! [A:list_a,B:(a > $o)]: ((! [C:a]: ((member_a @ C @ (set_a2 @ A)) => (B @ C))) = (! [C:nat]: ((ord_less_nat @ C @ (size_size_list_a @ A)) => (B @ (nth_a @ A @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_256_all__set__conv__all__nth)).
% 16.79/5.05 thf(1032,plain,((! [A:list_a,B:(a > $o)]: ((! [C:a]: ((member_a @ C @ (set_a2 @ A)) => (B @ C))) = (! [C:nat]: ((ord_less_nat @ C @ (size_size_list_a @ A)) => (B @ (nth_a @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 16.79/5.05 thf(111,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_154_not__less__iff__gr__or__eq)).
% 16.79/5.05 thf(625,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)],[111])).
% 16.79/5.05 thf(100,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)).
% 16.79/5.05 thf(583,plain,((! [A:a,B:a]: ((if_a @ ($false) @ A @ B) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 16.79/5.05 thf(218,axiom,((ord_less_nat @ x @ (size_size_list_a @ ys))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_2)).
% 16.79/5.05 thf(1079,plain,((ord_less_nat @ x @ (size_size_list_a @ ys))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 16.79/5.05 thf(64,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_136_linear)).
% 16.79/5.05 thf(456,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)],[64])).
% 16.79/5.05 thf(193,axiom,((! [A:list_a,B:set_a]: ((ord_less_eq_set_a @ (set_a2 @ A) @ B) = (! [C:a]: ((member_a @ C @ (set_a2 @ A)) => (member_a @ C @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_subset__code_I1_J)).
% 16.79/5.05 thf(974,plain,((! [A:list_a,B:set_a]: ((ord_less_eq_set_a @ (set_a2 @ A) @ B) = (! [C:a]: ((member_a @ C @ (set_a2 @ A)) => (member_a @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 16.79/5.05 thf(1,conjecture,(((nth_a @ xs @ x) = (nth_a @ ys @ x))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_3)).
% 16.79/5.05 thf(2,negated_conjecture,((~ ((nth_a @ xs @ x) = (nth_a @ ys @ x)))),inference(neg_conjecture,[status(cth)],[1])).
% 16.79/5.05 thf(224,plain,((~ ((nth_a @ xs @ x) = (nth_a @ ys @ x)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 16.79/5.05 thf(4,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_If_001t__Nat__Onat_T)).
% 16.79/5.05 thf(229,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 16.79/5.05 thf(73,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_224_order__le__less__subst2)).
% 16.79/5.05 thf(484,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)],[73])).
% 16.79/5.05 thf(143,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) | (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_le__less__linear)).
% 16.79/5.05 thf(742,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) | (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 16.79/5.05 thf(51,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_230_pinf_I6_J)).
% 16.79/5.05 thf(403,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)],[51])).
% 16.79/5.05 thf(201,axiom,((! [A:nat]: (((ord_less_nat @ A @ (size_size_list_a @ ys)) => (((ord_less_nat @ A @ (size_size_list_a @ ys)) => ((nth_a @ xs @ A) = (nth_a @ ys @ A))) & ((~ (ord_less_nat @ A @ (size_size_list_a @ ys))) => ((f @ (minus_minus_nat @ A @ (size_size_list_a @ xs))) = (nth_a @ ys @ A))))) & ((~ (ord_less_nat @ A @ (size_size_list_a @ ys))) => (((ord_less_nat @ A @ (size_size_list_a @ ys)) => ((nth_a @ xs @ A) = (g @ (minus_minus_nat @ A @ (size_size_list_a @ ys))))) & ((~ (ord_less_nat @ A @ (size_size_list_a @ ys))) => ((f @ (minus_minus_nat @ A @ (size_size_list_a @ xs))) = (g @ (minus_minus_nat @ A @ (size_size_list_a @ ys)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1)).
% 16.79/5.05 thf(1006,plain,((! [A:nat]: (((ord_less_nat @ A @ (size_size_list_a @ ys)) => (((ord_less_nat @ A @ (size_size_list_a @ ys)) => ((nth_a @ xs @ A) = (nth_a @ ys @ A))) & ((~ (ord_less_nat @ A @ (size_size_list_a @ ys))) => ((f @ (minus_minus_nat @ A @ (size_size_list_a @ xs))) = (nth_a @ ys @ A))))) & ((~ (ord_less_nat @ A @ (size_size_list_a @ ys))) => (((ord_less_nat @ A @ (size_size_list_a @ ys)) => ((nth_a @ xs @ A) = (g @ (minus_minus_nat @ A @ (size_size_list_a @ ys))))) & ((~ (ord_less_nat @ A @ (size_size_list_a @ ys))) => ((f @ (minus_minus_nat @ A @ (size_size_list_a @ xs))) = (g @ (minus_minus_nat @ A @ (size_size_list_a @ ys)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 16.79/5.05 thf(103,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_144_ord__le__eq__trans)).
% 16.79/5.05 thf(593,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)],[103])).
% 16.79/5.05 thf(107,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_161_linorder__cases)).
% 16.79/5.05 thf(610,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)],[107])).
% 16.79/5.05 thf(148,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_212_le__imp__less__or__eq)).
% 16.79/5.05 thf(783,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)],[148])).
% 16.79/5.05 thf(197,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_leI)).
% 16.79/5.05 thf(989,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => (ord_less_eq_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 16.79/5.05 thf(32,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_53_append_Oassoc)).
% 16.79/5.05 thf(328,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)],[32])).
% 16.79/5.05 thf(220,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_1_nth__equalityI)).
% 16.79/5.05 thf(1082,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)],[220])).
% 16.79/5.05 thf(147,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_233_complete__interval)).
% 16.79/5.05 thf(753,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)],[147])).
% 16.79/5.05 thf(89,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_dual__order_Oirrefl)).
% 16.79/5.05 thf(537,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 16.79/5.05 thf(117,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_17_nat__less__induct)).
% 16.79/5.05 thf(642,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)],[117])).
% 16.79/5.05 thf(86,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_143_ord__eq__le__trans)).
% 16.79/5.05 thf(526,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)],[86])).
% 16.79/5.05 thf(74,axiom,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) = (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_verit__comp__simplify1_I3_J)).
% 16.79/5.05 thf(489,plain,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) = (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 16.79/5.05 thf(123,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_less__imp__not__less)).
% 16.79/5.05 thf(679,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 16.79/5.05 thf(126,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_less__asym_H)).
% 16.79/5.05 thf(686,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 16.79/5.05 thf(71,axiom,((! [A:a,B:list_a,C:list_a]: (((member_a @ A @ (set_a2 @ (butlast_a @ B))) | (member_a @ A @ (set_a2 @ (butlast_a @ C)))) => (member_a @ A @ (set_a2 @ (butlast_a @ (append_a @ B @ C))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_in__set__butlast__appendI)).
% 16.79/5.05 thf(476,plain,((! [A:a,B:list_a,C:list_a]: (((member_a @ A @ (set_a2 @ (butlast_a @ B))) | (member_a @ A @ (set_a2 @ (butlast_a @ C)))) => (member_a @ A @ (set_a2 @ (butlast_a @ (append_a @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 16.79/5.05 thf(129,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_107_nat__diff__left__cancel__le2)).
% 16.79/5.05 thf(701,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)],[129])).
% 16.79/5.05 thf(83,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)).
% 16.79/5.05 thf(515,plain,((! [A:a,B:a]: ((if_a @ ($true) @ A @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 16.79/5.05 thf(175,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_96_le__diff__iff)).
% 16.79/5.05 thf(911,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)],[175])).
% 16.79/5.05 thf(200,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_112_nth__append1)).
% 16.79/5.05 thf(1002,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)],[200])).
% 16.79/5.05 thf(105,axiom,((! [A:list_a]: ((size_size_list_a @ (butlast_a @ A)) = (minus_minus_nat @ (size_size_list_a @ A) @ one_one_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_length__butlast)).
% 16.79/5.05 thf(605,plain,((! [A:list_a]: ((size_size_list_a @ (butlast_a @ A)) = (minus_minus_nat @ (size_size_list_a @ A) @ one_one_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 16.79/5.05 thf(10,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_182_order__less__subst1)).
% 16.79/5.05 thf(244,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)],[10])).
% 16.79/5.05 thf(17,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_75_nat__le__linear)).
% 16.79/5.05 thf(266,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)],[17])).
% 16.79/5.05 thf(113,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_order_Oorder__iff__strict)).
% 16.79/5.05 thf(633,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 16.79/5.05 thf(178,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_less__imp__le)).
% 16.79/5.05 thf(921,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 16.79/5.05 thf(101,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_8_diff__less__mono2)).
% 16.79/5.05 thf(586,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)],[101])).
% 16.79/5.05 thf(180,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_less__irrefl)).
% 16.79/5.05 thf(926,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 16.79/5.05 thf(49,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_86_less__ge__neq__conv)).
% 16.79/5.05 thf(398,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)],[49])).
% 16.79/5.05 thf(205,axiom,((! [A:a,B:list_a]: ((member_a @ A @ (set_a2 @ B)) = (? [C:nat]: ((ord_less_nat @ C @ (size_size_list_a @ B)) & ((nth_a @ B @ C) = A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_in__set__conv__nth)).
% 16.79/5.05 thf(1035,plain,((! [A:a,B:list_a]: ((member_a @ A @ (set_a2 @ B)) = (? [C:nat]: ((ord_less_nat @ C @ (size_size_list_a @ B)) & ((nth_a @ B @ C) = A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 16.79/5.05 thf(135,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_196_minf_I7_J)).
% 16.79/5.05 thf(718,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)],[135])).
% 16.79/5.05 thf(169,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_219_le__neq__trans)).
% 16.79/5.05 thf(888,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)],[169])).
% 16.79/5.05 thf(109,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_141_antisym__conv)).
% 16.79/5.05 thf(618,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)],[109])).
% 16.79/5.05 thf(82,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_134_eq__iff)).
% 16.79/5.05 thf(513,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)],[82])).
% 16.79/5.05 thf(16,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_dual__order_Orefl)).
% 16.79/5.05 thf(264,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 16.79/5.05 thf(161,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_142_order__class_Oorder_Oeq__iff)).
% 16.79/5.05 thf(856,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)],[161])).
% 16.79/5.05 thf(23,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_162_less__imp__triv)).
% 16.79/5.05 thf(296,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)],[23])).
% 16.79/5.05 thf(43,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_le__less)).
% 16.79/5.05 thf(375,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 16.79/5.05 thf(139,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_117_nat__diff__right__cancel__le1)).
% 16.79/5.05 thf(732,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)],[139])).
% 16.79/5.05 thf(92,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_less__not__refl3)).
% 16.79/5.05 thf(545,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 16.79/5.05 thf(14,axiom,((! [A:nat]: ? [B:list_a]: ((size_size_list_a @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_Ex__list__of__length)).
% 16.79/5.05 thf(259,plain,((! [A:nat]: ? [B:list_a]: ((size_size_list_a @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 16.79/5.05 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 @ 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_140_le__cases3)).
% 16.79/5.05 thf(413,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)],[55])).
% 16.79/5.05 thf(98,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_9_less__imp__diff__less)).
% 16.79/5.05 thf(577,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)],[98])).
% 16.79/5.05 thf(132,axiom,((! [A:a,B:list_a]: ((member_a @ A @ (set_a2 @ (butlast_a @ B))) => (member_a @ A @ (set_a2 @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_in__set__butlastD)).
% 16.79/5.05 thf(711,plain,((! [A:a,B:list_a]: ((member_a @ A @ (set_a2 @ (butlast_a @ B))) => (member_a @ A @ (set_a2 @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 16.79/5.05 thf(47,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_215_le__less__trans)).
% 16.79/5.05 thf(391,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)],[47])).
% 16.79/5.05 thf(61,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_105_eq__diff__left__iff)).
% 16.79/5.05 thf(445,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)],[61])).
% 16.79/5.05 thf(46,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_132_ord__eq__le__subst)).
% 16.79/5.05 thf(382,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)],[46])).
% 16.79/5.05 thf(96,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_88_le__greater__neq__conv)).
% 16.79/5.05 thf(572,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)],[96])).
% 16.79/5.05 thf(7,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_10_less__diff__imp__less)).
% 16.79/5.05 thf(236,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)],[7])).
% 16.79/5.05 thf(187,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_less__irrefl__nat)).
% 16.79/5.05 thf(947,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 16.79/5.05 thf(90,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_114_diff__less__mono)).
% 16.79/5.05 thf(540,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)],[90])).
% 16.79/5.05 thf(133,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_order_Oasym)).
% 16.79/5.05 thf(713,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 16.79/5.05 thf(77,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_115_less__diff__le__imp__less)).
% 16.79/5.05 thf(498,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)],[77])).
% 16.79/5.05 thf(68,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_58_diff__diff__cancel)).
% 16.79/5.05 thf(466,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)],[68])).
% 16.79/5.05 thf(222,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_46_nth__append)).
% 16.79/5.05 thf(1092,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)],[222])).
% 16.79/5.05 thf(172,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_12_nat__diff__left__cancel__eq2)).
% 16.79/5.05 thf(900,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)],[172])).
% 16.79/5.05 thf(124,axiom,((! [A:set_a]: ((collect_a @ (^ [B:a]: (member_a @ B @ A))) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_Collect__mem__eq)).
% 16.79/5.05 thf(681,plain,((! [A:set_a]: ((collect_a @ (^ [B:a]: (member_a @ B @ A))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 16.79/5.05 thf(44,axiom,((! [A:list_a,B:set_a,C:a,D:nat]: ((ord_less_eq_set_a @ (set_a2 @ A) @ B) => ((member_a @ C @ B) => (ord_less_eq_set_a @ (set_a2 @ (list_update_a @ A @ D @ C)) @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_set__update__subsetI)).
% 16.79/5.05 thf(377,plain,((! [A:list_a,B:set_a,C:a,D:nat]: ((ord_less_eq_set_a @ (set_a2 @ A) @ B) => ((member_a @ C @ B) => (ord_less_eq_set_a @ (set_a2 @ (list_update_a @ A @ D @ C)) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 16.79/5.05 thf(5,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_116_nat__diff__left__cancel__le1)).
% 16.79/5.05 thf(230,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)],[5])).
% 16.79/5.05 thf(81,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (C != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_pinf_I4_J)).
% 16.79/5.05 thf(509,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (C = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 16.79/5.05 thf(141,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_85_ge__less__neq__conv)).
% 16.79/5.05 thf(737,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)],[141])).
% 16.79/5.05 thf(28,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_leD)).
% 16.79/5.05 thf(318,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 16.79/5.05 thf(219,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_34_i__append__def)).
% 16.79/5.05 thf(1080,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)],[219])).
% 16.79/5.05 thf(110,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_order_Ostrict__implies__not__eq)).
% 16.79/5.05 thf(621,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 16.79/5.05 thf(191,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_202_dual__order_Oorder__iff__strict)).
% 16.79/5.05 thf(964,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 16.79/5.05 thf(176,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_209_order_Ostrict__trans1)).
% 16.79/5.05 thf(915,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)],[176])).
% 16.79/5.05 thf(185,axiom,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) => (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_not__le__imp__less)).
% 16.79/5.05 thf(943,plain,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) => (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 16.79/5.05 thf(182,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_181_order__less__subst2)).
% 16.79/5.05 thf(932,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)],[182])).
% 16.79/5.05 thf(36,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_155_dual__order_Ostrict__trans)).
% 16.79/5.05 thf(345,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)],[36])).
% 16.79/5.05 thf(162,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_72_le__trans)).
% 16.79/5.05 thf(858,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)],[162])).
% 16.79/5.05 thf(203,axiom,((! [A:list_a,B:nat]: ((list_update_a @ A @ B @ (nth_a @ A @ B)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_list__update__id)).
% 16.79/5.05 thf(1029,plain,((! [A:list_a,B:nat]: ((list_update_a @ A @ B @ (nth_a @ A @ B)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 16.79/5.05 thf(171,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_169_ord__less__eq__trans)).
% 16.79/5.05 thf(895,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)],[171])).
% 16.79/5.05 thf(85,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_225_order__le__less__subst1)).
% 16.79/5.05 thf(521,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)],[85])).
% 16.79/5.05 thf(208,axiom,((! [A:nat,B:list_a]: ((ord_less_nat @ A @ (size_size_list_a @ (butlast_a @ B))) => ((nth_a @ (butlast_a @ B) @ A) = (nth_a @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_nth__butlast)).
% 16.79/5.05 thf(1044,plain,((! [A:nat,B:list_a]: ((ord_less_nat @ A @ (size_size_list_a @ (butlast_a @ B))) => ((nth_a @ (butlast_a @ B) @ A) = (nth_a @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 16.79/5.05 thf(165,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_87_greater__le__neq__conv)).
% 16.79/5.05 thf(868,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)],[165])).
% 16.79/5.05 thf(106,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_195_minf_I5_J)).
% 16.79/5.05 thf(608,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)],[106])).
% 16.79/5.05 thf(199,axiom,((list_ex_a = (^ [A:(a > $o),B:list_a]: ? [C:nat]: ((ord_less_nat @ C @ (size_size_list_a @ B)) & (A @ (nth_a @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_list__ex__length)).
% 16.79/5.05 thf(1000,plain,(((list_ex_a) = (^ [A:(a > $o),B:list_a]: ? [C:nat]: ((ord_less_nat @ C @ (size_size_list_a @ B)) & (A @ (nth_a @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 16.79/5.05 thf(24,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_38_nat__diff__right__cancel__eq2)).
% 16.79/5.05 thf(299,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)],[24])).
% 16.79/5.05 thf(3,axiom,((! [A:nat]: ((one_one_nat = A) = (A = one_one_nat)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_one__reorient)).
% 16.79/5.05 thf(226,plain,((! [A:nat]: ((one_one_nat = A) = (A = one_one_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 16.79/5.05 thf(119,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_dual__order_Ostrict__implies__order)).
% 16.79/5.05 thf(653,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 16.79/5.05 thf(121,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_13_nat__diff__left__cancel__less)).
% 16.79/5.05 thf(658,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)],[121])).
% 16.79/5.05 thf(48,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_26_neq__if__length__neq)).
% 16.79/5.05 thf(394,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)],[48])).
% 16.79/5.05 thf(196,axiom,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) = (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_not__le)).
% 16.79/5.05 thf(986,plain,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) = (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 16.79/5.05 thf(102,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (C != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_pinf_I3_J)).
% 16.79/5.05 thf(589,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ B @ C) => (~ (C = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 16.79/5.05 thf(87,axiom,((! [A:(a > $o),B:list_a,C:list_a]: ((list_ex_a @ A @ (append_a @ B @ C)) = ((list_ex_a @ A @ B) | (list_ex_a @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_list__ex__append)).
% 16.79/5.05 thf(531,plain,((! [A:(a > $o),B:list_a,C:list_a]: ((list_ex_a @ (A) @ (append_a @ B @ C)) = ((list_ex_a @ (A) @ B) | (list_ex_a @ (A) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 16.79/5.05 thf(35,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_257_verit__la__disequality)).
% 16.79/5.05 thf(342,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)],[35])).
% 16.79/5.05 thf(39,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_186_pinf_I2_J)).
% 16.79/5.05 thf(355,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)],[39])).
% 16.79/5.05 thf(94,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_79_append__eq__append__conv2)).
% 16.79/5.05 thf(553,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)],[94])).
% 16.79/5.05 thf(65,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_le__refl)).
% 16.79/5.05 thf(458,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 16.79/5.05 thf(210,axiom,((! [A:nat,B:list_a,C:a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => (((list_update_a @ B @ A @ C) = B) = ((nth_a @ B @ A) = C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_list__update__same__conv)).
% 16.79/5.05 thf(1049,plain,((! [A:nat,B:list_a,C:a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => (((list_update_a @ B @ A @ C) = B) = ((nth_a @ B @ A) = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 16.79/5.05 thf(99,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_106_le__diff__le__imp__le)).
% 16.79/5.05 thf(580,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)],[99])).
% 16.79/5.05 thf(128,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_191_minf_I1_J)).
% 16.79/5.05 thf(690,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)],[128])).
% 16.79/5.05 thf(116,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_231_pinf_I8_J)).
% 16.79/5.05 thf(640,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)],[116])).
% 16.79/5.05 thf(215,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_3_Skolem__list__nth)).
% 16.79/5.05 thf(1070,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)],[215])).
% 16.79/5.05 thf(142,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_less__not__refl)).
% 16.79/5.05 thf(739,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 16.79/5.05 thf(211,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_7_i__append__nth1)).
% 16.79/5.05 thf(1053,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)],[211])).
% 16.79/5.05 thf(151,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_77_append__eq__appendI)).
% 16.79/5.05 thf(791,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)],[151])).
% 16.79/5.05 thf(33,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_37_nat__diff__right__cancel__less)).
% 16.79/5.05 thf(331,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)],[33])).
% 16.79/5.05 thf(206,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_32_i__append__nth)).
% 16.79/5.05 thf(1038,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)],[206])).
% 16.79/5.05 thf(67,axiom,((! [A:a,B:(a > $o)]: ((member_a @ A @ (collect_a @ B)) = (B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_mem__Collect__eq)).
% 16.79/5.05 thf(463,plain,((! [A:a,B:(a > $o)]: ((member_a @ A @ (collect_a @ (B))) = (B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 16.79/5.05 thf(174,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_95_eq__diff__iff)).
% 16.79/5.05 thf(907,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)],[174])).
% 16.79/5.05 thf(144,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_74_le__antisym)).
% 16.79/5.05 thf(744,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)],[144])).
% 16.79/5.05 thf(130,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_60_append__eq__append__conv)).
% 16.79/5.05 thf(703,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)],[130])).
% 16.79/5.05 thf(108,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_94_less__mono__imp__le__mono)).
% 16.79/5.05 thf(613,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)],[108])).
% 16.79/5.05 thf(138,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_223_order__less__le__subst1)).
% 16.79/5.05 thf(727,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)],[138])).
% 16.79/5.05 thf(27,axiom,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (C != A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_minf_I3_J)).
% 16.79/5.05 thf(314,plain,((! [A:nat]: ? [B:nat]: ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (C = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 16.79/5.05 thf(198,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_165_less__induct)).
% 16.79/5.05 thf(991,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)],[198])).
% 16.79/5.05 thf(95,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_78_Nat_Oex__has__greatest__nat)).
% 16.79/5.05 thf(556,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)],[95])).
% 16.79/5.05 thf(170,axiom,((! [A:nat,B:nat,C:list_a,D:a,E:a]: ((A != B) => ((list_update_a @ (list_update_a @ C @ A @ D) @ B @ E) = (list_update_a @ (list_update_a @ C @ B @ E) @ A @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_list__update__swap)).
% 16.79/5.05 thf(891,plain,((! [A:nat,B:nat,C:list_a,D:a,E:a]: ((~ (A = B)) => ((list_update_a @ (list_update_a @ C @ A @ D) @ B @ E) = (list_update_a @ (list_update_a @ C @ B @ E) @ A @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 16.79/5.05 thf(127,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_190_pinf_I7_J)).
% 16.79/5.05 thf(688,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)],[127])).
% 16.79/5.05 thf(173,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_100_le__diff__iff_H)).
% 16.79/5.05 thf(903,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)],[173])).
% 16.79/5.05 thf(38,axiom,((! [A:nat,B:list_a,C:list_a,D:a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((list_update_a @ (append_a @ B @ C) @ A @ D) = (append_a @ (list_update_a @ B @ A @ D) @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_list__update__append1)).
% 16.79/5.05 thf(351,plain,((! [A:nat,B:list_a,C:list_a,D:a]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((list_update_a @ (append_a @ B @ C) @ A @ D) = (append_a @ (list_update_a @ B @ A @ D) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 16.79/5.05 thf(149,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_dual__order_Oasym)).
% 16.79/5.05 thf(786,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 16.79/5.05 thf(181,axiom,((! [A:list_a,B:nat,C:a]: ((size_size_list_a @ (list_update_a @ A @ B @ C)) = (size_size_list_a @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_length__list__update)).
% 16.79/5.05 thf(929,plain,((! [A:list_a,B:nat,C:a]: ((size_size_list_a @ (list_update_a @ A @ B @ C)) = (size_size_list_a @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 16.79/5.05 thf(217,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_5_list__eq__iff__nth__eq)).
% 16.79/5.05 thf(1077,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)],[217])).
% 16.79/5.05 thf(93,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_less__imp__neq)).
% 16.79/5.05 thf(549,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 16.79/5.05 thf(156,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_92_less__or__eq__imp__le)).
% 16.79/5.05 thf(832,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)],[156])).
% 16.79/5.05 thf(125,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_232_minf_I6_J)).
% 16.79/5.05 thf(684,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)],[125])).
% 16.79/5.05 thf(57,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_eq__imp__le)).
% 16.79/5.05 thf(432,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 16.79/5.05 thf(52,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_150_dual__order_Oeq__iff)).
% 16.79/5.05 thf(405,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)],[52])).
% 16.79/5.05 thf(164,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_103_le__diff__imp__le)).
% 16.79/5.05 thf(865,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)],[164])).
% 16.79/5.05 thf(42,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_le__eq__less__or__eq)).
% 16.79/5.05 thf(373,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 16.79/5.05 thf(188,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (B != A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_201_dual__order_Ostrict__iff__order)).
% 16.79/5.05 thf(950,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 16.79/5.05 thf(15,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_203_order_Ostrict__implies__order)).
% 16.79/5.05 thf(262,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 16.79/5.05 thf(26,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_16_infinite__descent)).
% 16.79/5.05 thf(305,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)],[26])).
% 16.79/5.05 thf(18,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_184_ord__eq__less__subst)).
% 16.79/5.05 thf(268,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)],[18])).
% 16.79/5.05 thf(153,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_128_nat__descend__induct)).
% 16.79/5.05 thf(807,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)],[153])).
% 16.79/5.05 thf(70,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_less__imp__le__nat)).
% 16.79/5.05 thf(474,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 16.79/5.05 thf(50,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_220_not__less)).
% 16.79/5.05 thf(400,plain,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = (ord_less_eq_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 16.79/5.05 thf(114,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_199_order_Onot__eq__order__implies__strict)).
% 16.79/5.05 thf(635,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)],[114])).
% 16.79/5.05 thf(136,axiom,((! [A:list_a,B:nat,C:a]: ((ord_less_eq_nat @ (size_size_list_a @ A) @ B) => ((list_update_a @ A @ B @ C) = A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_list__update__beyond)).
% 16.79/5.05 thf(720,plain,((! [A:list_a,B:nat,C:a]: ((ord_less_eq_nat @ (size_size_list_a @ A) @ B) => ((list_update_a @ A @ B @ C) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 16.79/5.05 thf(190,axiom,((! [A:list_a,B:list_a,C:(a > $o),D:(a > $o)]: ((A = B) => ((! [E:a]: ((member_a @ E @ (set_a2 @ B)) => ((C @ E) = (D @ E)))) => ((list_ex_a @ C @ A) = (list_ex_a @ D @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_list__ex__cong)).
% 16.79/5.05 thf(955,plain,((! [A:list_a,B:list_a,C:(a > $o),D:(a > $o)]: ((A = B) => ((! [E:a]: ((member_a @ E @ (set_a2 @ B)) => ((C @ E) = (D @ E)))) => ((list_ex_a @ (C) @ A) = (list_ex_a @ (D) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 16.79/5.05 thf(152,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_192_minf_I2_J)).
% 16.79/5.05 thf(796,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)],[152])).
% 16.79/5.05 thf(8,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_68_i__append__assoc)).
% 16.79/5.05 thf(239,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)],[8])).
% 16.79/5.05 thf(9,axiom,((! [A:nat,B:nat]: (ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_diff__le__self)).
% 16.79/5.05 thf(242,plain,((! [A:nat,B:nat]: (ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 16.79/5.05 thf(22,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_less__not__sym)).
% 16.79/5.05 thf(294,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 16.79/5.05 thf(177,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_145_order__class_Oorder_Oantisym)).
% 16.79/5.05 thf(918,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)],[177])).
% 16.79/5.05 thf(159,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_135_antisym)).
% 16.79/5.05 thf(850,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)],[159])).
% 16.79/5.05 thf(19,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_14_nat__diff__right__cancel__eq1)).
% 16.79/5.05 thf(277,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)],[19])).
% 16.79/5.05 thf(60,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_218_antisym__conv1)).
% 16.79/5.05 thf(442,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)],[60])).
% 16.79/5.05 thf(78,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_55_append__same__eq)).
% 16.79/5.05 thf(501,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)],[78])).
% 16.79/5.05 thf(41,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_eq__refl)).
% 16.79/5.05 thf(369,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 16.79/5.05 thf(12,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_172_less__linear)).
% 16.79/5.05 thf(254,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)],[12])).
% 16.79/5.05 thf(30,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_159_order_Ostrict__trans)).
% 16.79/5.05 thf(322,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)],[30])).
% 16.79/5.05 thf(179,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_11_nat__diff__left__cancel__eq1)).
% 16.79/5.05 thf(923,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)],[179])).
% 16.79/5.05 thf(91,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_138_le__cases)).
% 16.79/5.05 thf(543,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)],[91])).
% 16.79/5.05 thf(221,axiom,((! [A:nat,B:list_a,C:nat]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((ord_less_nat @ C @ (size_size_list_a @ B)) => ((set_a2 @ (list_update_a @ (list_update_a @ B @ A @ (nth_a @ B @ C)) @ C @ (nth_a @ B @ A))) = (set_a2 @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_set__swap)).
% 16.79/5.05 thf(1088,plain,((! [A:nat,B:list_a,C:nat]: ((ord_less_nat @ A @ (size_size_list_a @ B)) => ((ord_less_nat @ C @ (size_size_list_a @ B)) => ((set_a2 @ (list_update_a @ (list_update_a @ B @ A @ (nth_a @ B @ C)) @ C @ (nth_a @ B @ A))) = (set_a2 @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 16.79/5.05 thf(76,axiom,((ord_less_nat = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (A != B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_less__le)).
% 16.79/5.05 thf(496,plain,(((ord_less_nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & ~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 16.79/5.05 thf(6,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_24_size__neq__size__imp__neq)).
% 16.79/5.05 thf(232,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)],[6])).
% 16.79/5.05 thf(69,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_222_order__less__le__subst2)).
% 16.79/5.05 thf(469,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)],[69])).
% 16.79/5.05 thf(184,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_178_neq__iff)).
% 16.79/5.05 thf(940,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)],[184])).
% 16.79/5.05 thf(1173,plain,(($false)),inference(e,[status(thm)],[518,249,333,628,977,1073,655,861,873,449,715,747,945,1063,829,709,841,320,436,651,257,724,504,838,751,1059,460,870,325,289,1100,638,853,492,1040,937,966,480,574,1020,348,981,280,877,734,660,411,428,507,452,380,439,366,534,1047,1057,952,302,598,820,407,788,1032,625,583,1079,456,974,224,229,484,742,403,1006,593,610,783,989,328,1082,753,537,642,526,489,679,686,476,701,515,911,1002,605,244,266,633,921,586,926,398,1035,718,888,618,513,264,856,296,375,732,545,259,413,577,711,391,445,382,572,236,947,540,713,498,466,1092,900,681,377,230,509,737,318,1080,621,964,915,943,932,345,858,1029,895,521,1044,868,608,1000,299,226,653,658,394,986,589,531,342,355,553,458,1049,580,690,640,1070,739,1053,791,331,1038,463,907,744,703,613,727,314,991,556,891,688,903,351,786,929,1077,549,832,684,432,405,865,373,950,262,305,268,807,474,400,635,720,955,796,239,242,294,918,850,277,442,501,369,254,322,923,543,1088,496,232,469,940])).
% 16.79/5.05 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.79/5.05 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------