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

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : ITP132^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39

% Computer : n014.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:53 AM UTC 2026

% Result   : Theorem 12.58s 3.27s
% Output   : Refutation 13.71s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : ITP132^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.19  % Computer : n014.cluster.edu
% 0.10/0.19  % Model    : x86_64 x86_64
% 0.10/0.19  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.19  % Memory   : 8046.5625MB
% 0.10/0.19  % OS       : Linux 6.8.0-71-generic
% 0.10/0.19  % CPULimit : 300
% 0.10/0.19  % WCLimit  : 300
% 0.10/0.19  % DateTime : Tue Sep 29 19:58:29 UTC 2026
% 0.10/0.19  % CPUTime  : 
% 0.10/0.19  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.65/0.49  % [INFO] 	 Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ... 
% 1.48/0.73  % [INFO] 	 Parsing done (238ms). 
% 1.48/0.74  % [INFO] 	 Running in sequential loop mode. 
% 2.29/0.94  % [INFO] 	 eprover registered as external prover. 
% 2.29/0.95  % [INFO] 	 Scanning for conjecture ... 
% 2.29/1.02  % [INFO] 	 Found a conjecture (or negated_conjecture) and 244 axioms. Running axiom selection ... 
% 2.76/1.09  % [INFO] 	 Axiom selection finished. Selected 241 axioms (removed 3 axioms). 
% 3.51/1.26  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 3.51/1.28  % [INFO] 	 Type checking passed. 
% 3.51/1.28  % [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 ... 
% 12.58/3.26  % External prover 'e' found a proof!
% 12.58/3.26  % [INFO] 	 Killing All external provers ... 
% 12.58/3.26  % Time passed: 2977ms (effective reasoning time: 2517ms)
% 12.58/3.26  % 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)>
% 12.58/3.27  % Axioms used in derivation (241): fact_64_le__zero__eq, fact_39_sum__mono, fact_99_less__eq__nat_Osimps_I1_J, fact_224_less__trans, fact_108_split__mult__neg__le, fact_218_less__imp__not__eq, fact_157_ord__eq__le__subst, fact_188_partitions__remove1__bounds, fact_71_diff__zero, fact_189_nat__mult__eq__cancel__disj, fact_190_le__numeral__extra_I4_J, fact_175_fun__upd__idem__iff, fact_120_mult__eq__self__implies__10, fact_25_diff__le__mono2, fact_213_less__imp__triv, fact_60_lambda__one, fact_97_bot__nat__0_Oextremum__unique, fact_156_ord__le__eq__subst, fact_14_diff__diff__cancel, fact_115_partitions__zero, fact_3__092_060open_062_I_092_060Sum_062i_092_060le_062n_A_N_Ak_O_A_Ip_Ik_A_058_061_Ap_Ak_A_N_A1_J_J_Ai_A_K_Ai_J_A_061_A_I_092_060Sum_062i_092_060le_062n_O_A_Ip_Ik_A_058_061_Ap_Ak_A_N_A1_J_J_Ai_A_K_Ai_J_092_060close_062, fact_18_le__trans, fact_227_less__imp__neq, fact_102_mult__0, fact_40_atMost__def, fact_234_ord__less__eq__subst, fact_197_nat__mult__less__cancel__disj, fact_10_atMost__subset__iff, fact_9_diff__mult__distrib2, fact_56_fun__upd__triv, fact_215_antisym__conv3, fact_128_dual__order_Orefl, fact_85_zero__reorient, fact_26_le__diff__iff_H, fact_22_Nat_Oex__has__greatest__nat, fact_112_mult__mono, fact_237_less__numeral__extra_I4_J, fact_217_less__not__sym, fact_233_order__less__subst1, fact_232_order__less__subst2, fact_8_diff__mult__distrib, fact_162_order__subst2, fact_196_zero__less__diff, fact_178_fun__upd__same, fact_59_order__refl, fact_63_partitionsE, fact_41_atMost__def, fact_89_no__zero__divisors, fact_147_eq__refl, fact_163_order__subst2, fact_131_order__trans, fact_123_dual__order_Oeq__iff, fact_16_nat__1__eq__mult__iff, fact_50_sum_Ocong, fact_214_less__imp__not__eq2, fact_146_eq__refl, fact_38_nat__mult__1, fact_161_order__subst2, fact_171_mult_Ocommute, fact_202_mult__le__cancel2, fact_116_mult__left__le, fact_17_le__refl, fact_210_order_Ostrict__trans, fact_168_order__subst1, fact_138_order__class_Oorder_Oeq__iff, fact_69_mult__cancel__right, fact_113_not__one__le__zero, fact_19_eq__imp__le, fact_240_nat__less__induct, fact_32_mult__le__mono2, fact_226_less__asym, fact_118_sum__nonpos, fact_148_linear, fact_126_dual__order_Otrans, fact_106_mult__nonneg__nonpos, fact_220_ord__less__eq__trans, fact_33_mult__le__mono1, fact_238_linorder__neqE__nat, fact_98_le__0__eq, fact_208_exists__least__iff, fact_127_linorder__wlog, fact_117_mult__le__one, fact_37_nat__mult__1__right, fact_181_fun__upd__def, fact_62_partitionsI, fact_211_dual__order_Oirrefl, fact_72_cancel__comm__monoid__add__class_Odiff__cancel, fact_90_mult__left__cancel, fact_216_less__induct, fact_130_order__trans, fact_221_ord__eq__less__trans, fact_4_calculation, fact_122_dual__order_Oantisym, fact_119_sum__nonneg, fact_223_less__linear, fact_140_antisym__conv, fact_121_dual__order_Oantisym, fact_129_dual__order_Orefl, fact_24_partitions__bounds, fact_207_linorder__less__wlog, fact_109_mult__right__mono, fact_111_mult__mono_H, fact_87_mult__not__zero, fact_15_nat__mult__eq__1__iff, fact_2_atMost__eq__iff, fact_95_sum_Onot__neutral__contains__not__neutral, fact_49_sum_Oeq__general, fact_160_ord__eq__le__subst, fact_166_order__subst1, fact_209_less__imp__not__less, fact_135_ord__le__eq__trans, fact_31_eq__diff__iff, fact_67_mult__eq__0__iff, fact_27_diff__le__self, fact_145_le__cases, fact_192_not__gr__zero, fact_55_fun__upd__upd, fact_79_mult__cancel1, fact_155_ord__le__eq__subst, fact_225_less__asym_H, fact_200_less__one, fact_165_order__subst1, fact_0_partitions, fact_231_gt__ex, fact_150_antisym, fact_170_mult_Oassoc, fact_228_order_Oasym, fact_20_le__antisym, fact_103_ordered__comm__semiring__class_Ocomm__mult__left__mono, fact_104_mult__nonneg__nonpos2, fact_93_lambda__zero, fact_70_zero__diff, fact_12_atMost__iff, fact_94_sum_Oneutral, fact_6_sum__distrib__left, fact_66_mult__zero__right, fact_201_nat__mult__le__cancel__disj, fact_68_mult__cancel__left, fact_177_fun__upd__other, fact_184_comm__monoid__mult__class_Omult__1, fact_110_mult__left__mono, fact_74_le0, fact_53_mult_Oright__neutral, fact_125_dual__order_Otrans, fact_75_diff__0__eq__0, fact_107_mult__nonneg__nonneg, fact_154_ord__le__eq__subst, fact_47_sum_Oreindex__bij__witness, fact_205_not__less__iff__gr__or__eq, fact_182_left__diff__distrib_H, fact_132_order__class_Oorder_Oantisym, fact_91_mult__right__cancel, fact_204_order_Ostrict__implies__not__eq, fact_212_linorder__cases, fact_77_mult__is__0, fact_28_diff__le__mono, fact_35_le__square, fact_139_order__class_Oorder_Oeq__iff, fact_84_gr0, fact_57_fun__upd__apply, fact_186_subsetI, fact_124_dual__order_Oeq__iff, fact_61_partitions__def, fact_54_mult_Oleft__neutral, fact_83_diff__is__0__eq, fact_137_ord__eq__le__trans, fact_180_fun__upd__eqD, fact_100_diffs0__imp__equal, fact_101_minus__nat_Odiff__0, fact_194_less__nat__zero__code, fact_230_neqE, fact_172_mult_Oleft__commute, fact_30_le__diff__iff, fact_176_fun__upd__twist, fact_229_neq__iff, fact_45_Collect__mem__eq, fact_78_mult__0__right, fact_152_eq__iff, fact_29_Nat_Odiff__diff__eq, fact_151_eq__iff, fact_82_diff__is__0__eq_H, fact_48_sum_Oeq__general__inverses, fact_36_le__cube, fact_159_ord__eq__le__subst, fact_143_order_Otrans, fact_185_mult_Ocomm__neutral, fact_51_diff__commute, fact_183_right__diff__distrib_H, fact_80_mult__cancel2, fact_81_sum_Oneutral__const, fact_21_nat__le__linear, fact_42_sum__subtractf__nat, fact_198_mult__less__cancel2, fact_23_bounded__Max__nat, fact_76_diff__self__eq__0, fact_114_zero__le__one, fact_219_dual__order_Oasym, fact_136_ord__eq__le__trans, fact_43_partitions__parts__bounded, fact_222_less__irrefl, fact_195_neq0__conv, fact_239_infinite__descent, fact_96_bot__nat__0_Oextremum__uniqueI, fact_13_atMost__iff, fact_164_order__subst2, fact_144_order_Otrans, fact_203_dual__order_Ostrict__implies__not__eq, fact_34_mult__le__mono, fact_187_subset__antisym, fact_1__092_060open_062k_A_092_060le_062_An_092_060close_062, fact_158_ord__eq__le__subst, fact_141_antisym__conv, fact_142_le__cases3, fact_206_dual__order_Ostrict__trans, fact_88_divisors__zero, fact_173_cancel__ab__semigroup__add__class_Odiff__right__commute, fact_65_mult__zero__left, fact_153_ord__le__eq__subst, fact_52_sum_Oswap, fact_92_zero__neq__one, fact_73_bot__nat__0_Oextremum, fact_191_le__numeral__extra_I3_J, fact_5_sum__product, fact_133_order__class_Oorder_Oantisym, fact_86_zero__le, fact_174_one__reorient, fact_167_order__subst1, fact_236_less__numeral__extra_I3_J, fact_11_atMost__subset__iff, fact_169_ab__semigroup__mult__class_Omult__ac_I1_J, fact_134_ord__le__eq__trans, fact_44_mem__Collect__eq, fact_58_order__refl, fact_235_ord__eq__less__subst, fact_179_fun__upd__idem, fact_193_bot__nat__0_Onot__eq__extremum, fact_46_Collect__cong, fact_149_antisym, fact_7_sum__distrib__right, fact_199_nat__0__less__mult__iff, fact_105_mult__nonpos__nonneg
% 12.58/3.27  % No. of inferences in proof: 486
% 12.58/3.27  % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 2977 ms resp. 2517 ms w/o parsing
% 13.71/3.47  % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.71/3.47  thf(set_set_nat_type, type, set_set_nat: $tType).
% 13.71/3.47  thf(set_nat_type, type, set_nat: $tType).
% 13.71/3.47  thf(nat_type, type, nat: $tType).
% 13.71/3.47  thf(fun_upd_nat_nat_decl, type, fun_upd_nat_nat: ((nat > nat) > (nat > (nat > (nat > nat))))).
% 13.71/3.47  thf(minus_minus_nat_decl, type, minus_minus_nat: (nat > (nat > nat))).
% 13.71/3.47  thf(one_one_nat_decl, type, one_one_nat: nat).
% 13.71/3.47  thf(times_times_nat_decl, type, times_times_nat: (nat > (nat > nat))).
% 13.71/3.47  thf(zero_zero_nat_decl, type, zero_zero_nat: nat).
% 13.71/3.47  thf(groups1842438620at_nat_decl, type, groups1842438620at_nat: ((nat > nat) > (set_nat > nat))).
% 13.71/3.47  thf(if_nat_decl, type, if_nat: ($o > (nat > (nat > nat)))).
% 13.71/3.47  thf(number1551313001itions_decl, type, number1551313001itions: ((nat > nat) > (nat > $o))).
% 13.71/3.47  thf(ord_less_nat_decl, type, ord_less_nat: (nat > (nat > $o))).
% 13.71/3.47  thf(ord_less_eq_nat_decl, type, ord_less_eq_nat: (nat > (nat > $o))).
% 13.71/3.47  thf(ord_less_eq_set_nat_decl, type, ord_less_eq_set_nat: (set_nat > (set_nat > $o))).
% 13.71/3.47  thf(ord_le1613022364et_nat_decl, type, ord_le1613022364et_nat: (set_set_nat > (set_set_nat > $o))).
% 13.71/3.47  thf(collect_nat_decl, type, collect_nat: ((nat > $o) > set_nat)).
% 13.71/3.47  thf(collect_set_nat_decl, type, collect_set_nat: ((set_nat > $o) > set_set_nat)).
% 13.71/3.47  thf(set_ord_atMost_nat_decl, type, set_ord_atMost_nat: (nat > set_nat)).
% 13.71/3.47  thf(set_or1086813439et_nat_decl, type, set_or1086813439et_nat: (set_nat > set_set_nat)).
% 13.71/3.47  thf(member_nat_decl, type, member_nat: (nat > (set_nat > $o))).
% 13.71/3.47  thf(member_set_nat_decl, type, member_set_nat: (set_nat > (set_set_nat > $o))).
% 13.71/3.47  thf(k_decl, type, k: nat).
% 13.71/3.47  thf(n_decl, type, n: nat).
% 13.71/3.47  thf(p_decl, type, p: (nat > nat)).
% 13.71/3.47  thf(110,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_20_le__antisym)).
% 13.71/3.47  thf(645,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)],[110])).
% 13.71/3.47  thf(145,axiom,((! [A:nat,B:nat,C:nat]: (((times_times_nat @ A @ B) = (times_times_nat @ C @ B)) = ((B = zero_zero_nat) | (A = C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_69_mult__cancel__right)).
% 13.71/3.47  thf(809,plain,((! [A:nat,B:nat,C:nat]: (((times_times_nat @ A @ B) = (times_times_nat @ C @ B)) = ((B = zero_zero_nat) | (A = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 13.71/3.47  thf(105,axiom,((~ (ord_less_nat @ one_one_nat @ one_one_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_237_less__numeral__extra_I4_J)).
% 13.71/3.47  thf(629,plain,((~ (ord_less_nat @ one_one_nat @ one_one_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 13.71/3.47  thf(243,axiom,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ (minus_minus_nat @ A @ B) @ C) = (minus_minus_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_182_left__diff__distrib_H)).
% 13.71/3.47  thf(1168,plain,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ (minus_minus_nat @ A @ B) @ C) = (minus_minus_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 13.71/3.47  thf(224,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/sandbox2/benchmark/theBenchmark.p',fact_30_le__diff__iff)).
% 13.71/3.47  thf(1105,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)],[224])).
% 13.71/3.47  thf(156,axiom,((! [A:nat]: ((times_times_nat @ A @ one_one_nat) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_185_mult_Ocomm__neutral)).
% 13.71/3.47  thf(846,plain,((! [A:nat]: ((times_times_nat @ A @ one_one_nat) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 13.71/3.47  thf(169,axiom,((! [A:nat,B:nat,C:nat]: (((times_times_nat @ A @ B) = (times_times_nat @ C @ B)) = ((A = C) | (B = zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_80_mult__cancel2)).
% 13.71/3.47  thf(893,plain,((! [A:nat,B:nat,C:nat]: (((times_times_nat @ A @ B) = (times_times_nat @ C @ B)) = ((A = C) | (B = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 13.71/3.47  thf(60,axiom,((((=) @ set_nat) = (^ [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) & (ord_less_eq_set_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_138_order__class_Oorder_Oeq__iff)).
% 13.71/3.47  thf(481,plain,((((=) @ set_nat) = (^ [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) & (ord_less_eq_set_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 13.71/3.47  thf(174,axiom,((! [A:nat]: ((times_times_nat @ zero_zero_nat @ A) = zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_102_mult__0)).
% 13.71/3.47  thf(909,plain,((! [A:nat]: ((times_times_nat @ zero_zero_nat @ A) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 13.71/3.47  thf(4,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_204_order_Ostrict__implies__not__eq)).
% 13.71/3.47  thf(249,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 13.71/3.47  thf(193,axiom,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ (minus_minus_nat @ A @ B) @ C) = (minus_minus_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_8_diff__mult__distrib)).
% 13.71/3.47  thf(977,plain,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ (minus_minus_nat @ A @ B) @ C) = (minus_minus_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 13.71/3.47  thf(199,axiom,((! [A:nat]: ((minus_minus_nat @ A @ zero_zero_nat) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_71_diff__zero)).
% 13.71/3.47  thf(994,plain,((! [A:nat]: ((minus_minus_nat @ A @ zero_zero_nat) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 13.71/3.47  thf(32,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_139_order__class_Oorder_Oeq__iff)).
% 13.71/3.47  thf(379,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)],[32])).
% 13.71/3.47  thf(70,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((~ (ord_less_nat @ B @ A)) = (B = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_215_antisym__conv3)).
% 13.71/3.47  thf(511,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)],[70])).
% 13.71/3.47  thf(98,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ A) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_149_antisym)).
% 13.71/3.47  thf(597,plain,((! [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 13.71/3.47  thf(209,axiom,((! [A:set_nat,B:(nat > nat),C:(nat > nat),D:set_nat,E:(nat > nat),F:(nat > nat)]: ((! [G:nat]: ((member_nat @ G @ A) => ((B @ (C @ G)) = G))) => ((! [G:nat]: ((member_nat @ G @ A) => (member_nat @ (C @ G) @ D))) => ((! [G:nat]: ((member_nat @ G @ D) => ((C @ (B @ G)) = G))) => ((! [G:nat]: ((member_nat @ G @ D) => (member_nat @ (B @ G) @ A))) => ((! [G:nat]: ((member_nat @ G @ A) => ((E @ (C @ G)) = (F @ G)))) => ((groups1842438620at_nat @ F @ A) = (groups1842438620at_nat @ E @ D))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_47_sum_Oreindex__bij__witness)).
% 13.71/3.47  thf(1041,plain,((! [A:set_nat,B:(nat > nat),C:(nat > nat),D:set_nat,E:(nat > nat),F:(nat > nat)]: ((! [G:nat]: ((member_nat @ G @ A) => ((B @ (C @ G)) = G))) => ((! [G:nat]: ((member_nat @ G @ A) => (member_nat @ (C @ G) @ D))) => ((! [G:nat]: ((member_nat @ G @ D) => ((C @ (B @ G)) = G))) => ((! [G:nat]: ((member_nat @ G @ D) => (member_nat @ (B @ G) @ A))) => ((! [G:nat]: ((member_nat @ G @ A) => ((E @ (C @ G)) = (F @ G)))) => ((groups1842438620at_nat @ (F) @ A) = (groups1842438620at_nat @ (E) @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 13.71/3.47  thf(75,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) & (ord_less_eq_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_152_eq__iff)).
% 13.71/3.47  thf(523,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)],[75])).
% 13.71/3.47  thf(240,axiom,((! [A:nat,B:nat,C:nat]: ((A != zero_zero_nat) => (((times_times_nat @ B @ A) = (times_times_nat @ C @ A)) = (B = C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_91_mult__right__cancel)).
% 13.71/3.47  thf(1158,plain,((! [A:nat,B:nat,C:nat]: ((~ (A = zero_zero_nat)) => (((times_times_nat @ B @ A) = (times_times_nat @ C @ A)) = (B = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 13.71/3.47  thf(12,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) | (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_148_linear)).
% 13.71/3.47  thf(269,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)],[12])).
% 13.71/3.47  thf(118,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/sandbox2/benchmark/theBenchmark.p',fact_142_le__cases3)).
% 13.71/3.47  thf(677,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)],[118])).
% 13.71/3.47  thf(217,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/sandbox2/benchmark/theBenchmark.p',fact_26_le__diff__iff_H)).
% 13.71/3.47  thf(1078,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)],[217])).
% 13.71/3.47  thf(83,axiom,((((=) @ set_nat) = (^ [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) & (ord_less_eq_set_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_151_eq__iff)).
% 13.71/3.47  thf(550,plain,((((=) @ set_nat) = (^ [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) & (ord_less_eq_set_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 13.71/3.47  thf(57,axiom,((! [A:nat]: ((zero_zero_nat = A) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_85_zero__reorient)).
% 13.71/3.47  thf(472,plain,((! [A:nat]: ((zero_zero_nat = A) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 13.71/3.47  thf(121,axiom,((! [A:nat,B:(set_nat > nat),C:set_nat,D:set_nat]: ((A = (B @ C)) => ((ord_less_eq_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_158_ord__eq__le__subst)).
% 13.71/3.47  thf(698,plain,((! [A:nat,B:(set_nat > nat),C:set_nat,D:set_nat]: ((A = (B @ C)) => ((ord_less_eq_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_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)],[121])).
% 13.71/3.47  thf(184,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (times_times_nat @ A @ B) @ (times_times_nat @ C @ B)) = ((ord_less_nat @ zero_zero_nat @ B) & (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_198_mult__less__cancel2)).
% 13.71/3.47  thf(945,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (times_times_nat @ A @ B) @ (times_times_nat @ C @ B)) = ((ord_less_nat @ zero_zero_nat @ B) & (ord_less_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 13.71/3.47  thf(211,axiom,((! [A:nat]: ((minus_minus_nat @ A @ A) = zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_72_cancel__comm__monoid__add__class_Odiff__cancel)).
% 13.71/3.47  thf(1063,plain,((! [A:nat]: ((minus_minus_nat @ A @ A) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 13.71/3.47  thf(179,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ one_one_nat) => ((ord_less_eq_nat @ zero_zero_nat @ B) => (ord_less_eq_nat @ (times_times_nat @ B @ A) @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_116_mult__left__le)).
% 13.71/3.47  thf(930,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ one_one_nat) => ((ord_less_eq_nat @ zero_zero_nat @ B) => (ord_less_eq_nat @ (times_times_nat @ B @ A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 13.71/3.47  thf(36,axiom,((! [A:(nat > nat),B:nat,C:nat,D:nat]: ((fun_upd_nat_nat @ (fun_upd_nat_nat @ A @ B @ C) @ B @ D) = (fun_upd_nat_nat @ A @ B @ D)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_55_fun__upd__upd)).
% 13.71/3.47  thf(404,plain,((! [A:(nat > nat),B:nat,C:nat,D:nat]: ((fun_upd_nat_nat @ (fun_upd_nat_nat @ A @ B @ C) @ B @ D) = (fun_upd_nat_nat @ A @ B @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 13.71/3.47  thf(231,axiom,((! [A:nat,B:nat]: ((A = (times_times_nat @ A @ B)) => ((B = one_one_nat) | (A = zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_120_mult__eq__self__implies__10)).
% 13.71/3.47  thf(1127,plain,((! [A:nat,B:nat]: ((A = (times_times_nat @ A @ B)) => ((B = one_one_nat) | (A = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 13.71/3.47  thf(135,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/sandbox2/benchmark/theBenchmark.p',fact_144_order_Otrans)).
% 13.71/3.47  thf(782,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)],[135])).
% 13.71/3.47  thf(88,axiom,((~ (ord_less_nat @ zero_zero_nat @ zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_236_less__numeral__extra_I3_J)).
% 13.71/3.47  thf(565,plain,((~ (ord_less_nat @ zero_zero_nat @ zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 13.71/3.47  thf(46,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_226_less__asym)).
% 13.71/3.47  thf(436,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 13.71/3.47  thf(112,axiom,((! [A:nat]: ((ord_less_nat @ A @ one_one_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_200_less__one)).
% 13.71/3.47  thf(651,plain,((! [A:nat]: ((ord_less_nat @ A @ one_one_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 13.71/3.47  thf(7,axiom,((! [A:set_nat,B:set_nat]: ((! [C:nat]: ((member_nat @ C @ A) => (member_nat @ C @ B))) => (ord_less_eq_set_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_186_subsetI)).
% 13.71/3.47  thf(257,plain,((! [A:set_nat,B:set_nat]: ((! [C:nat]: ((member_nat @ C @ A) => (member_nat @ C @ B))) => (ord_less_eq_set_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 13.71/3.47  thf(136,axiom,((! [A:nat,B:nat,C:$o]: ((ord_less_nat @ A @ B) => ((ord_less_nat @ B @ A) => (C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_213_less__imp__triv)).
% 13.71/3.47  thf(785,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)],[136])).
% 13.71/3.47  thf(142,axiom,((! [A:(nat > nat),B:set_nat,C:(nat > nat),D:set_nat]: ((times_times_nat @ (groups1842438620at_nat @ A @ B) @ (groups1842438620at_nat @ C @ D)) = (groups1842438620at_nat @ (^ [E:nat]: (groups1842438620at_nat @ (^ [F:nat]: (times_times_nat @ (A @ E) @ (C @ F))) @ D)) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_sum__product)).
% 13.71/3.47  thf(802,plain,((! [A:(nat > nat),B:set_nat,C:(nat > nat),D:set_nat]: ((times_times_nat @ (groups1842438620at_nat @ (A) @ B) @ (groups1842438620at_nat @ (C) @ D)) = (groups1842438620at_nat @ (^ [E:nat]: (groups1842438620at_nat @ (^ [F:nat]: (times_times_nat @ (A @ E) @ (C @ F))) @ D)) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 13.71/3.47  thf(30,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/sandbox2/benchmark/theBenchmark.p',fact_207_linorder__less__wlog)).
% 13.71/3.47  thf(357,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)],[30])).
% 13.71/3.47  thf(158,axiom,((! [A:nat,B:nat,C:nat]: (((times_times_nat @ A @ B) = (times_times_nat @ A @ C)) = ((B = C) | (A = zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_79_mult__cancel1)).
% 13.71/3.47  thf(853,plain,((! [A:nat,B:nat,C:nat]: (((times_times_nat @ A @ B) = (times_times_nat @ A @ C)) = ((B = C) | (A = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 13.71/3.47  thf(42,axiom,((fun_upd_nat_nat = (^ [A:(nat > nat),B:nat,C:nat,D:nat]: (if_nat @ (D = B) @ C @ (A @ D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_181_fun__upd__def)).
% 13.71/3.47  thf(421,plain,(((fun_upd_nat_nat) = (^ [A:(nat > nat),B:nat,C:nat,D:nat]: (if_nat @ (D = B) @ C @ (A @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 13.71/3.47  thf(227,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (times_times_nat @ C @ A) @ (times_times_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_32_mult__le__mono2)).
% 13.71/3.47  thf(1115,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (times_times_nat @ C @ A) @ (times_times_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 13.71/3.47  thf(8,axiom,((! [A:nat]: ((one_one_nat = A) = (A = one_one_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_174_one__reorient)).
% 13.71/3.47  thf(261,plain,((! [A:nat]: ((one_one_nat = A) = (A = one_one_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 13.71/3.47  thf(58,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_225_less__asym_H)).
% 13.71/3.47  thf(475,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 13.71/3.47  thf(225,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ zero_zero_nat @ C) => (ord_less_eq_nat @ (times_times_nat @ C @ A) @ (times_times_nat @ C @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_103_ordered__comm__semiring__class_Ocomm__mult__left__mono)).
% 13.71/3.47  thf(1109,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ zero_zero_nat @ C) => (ord_less_eq_nat @ (times_times_nat @ C @ A) @ (times_times_nat @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 13.71/3.47  thf(31,axiom,((! [A:nat]: ((A != zero_zero_nat) = (ord_less_nat @ zero_zero_nat @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_195_neq0__conv)).
% 13.71/3.47  thf(376,plain,((! [A:nat]: ((~ (A = zero_zero_nat)) = (ord_less_nat @ zero_zero_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 13.71/3.47  thf(103,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) = (B = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_141_antisym__conv)).
% 13.71/3.47  thf(623,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)],[103])).
% 13.71/3.47  thf(5,axiom,((! [A:set_nat]: (ord_less_eq_set_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_128_dual__order_Orefl)).
% 13.71/3.47  thf(253,plain,((! [A:set_nat]: (ord_less_eq_set_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 13.71/3.47  thf(71,axiom,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) => (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_145_le__cases)).
% 13.71/3.47  thf(514,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)],[71])).
% 13.71/3.47  thf(234,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) => ((ord_less_eq_nat @ zero_zero_nat @ B) => (ord_less_eq_nat @ (times_times_nat @ A @ B) @ zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_105_mult__nonpos__nonneg)).
% 13.71/3.47  thf(1136,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) => ((ord_less_eq_nat @ zero_zero_nat @ B) => (ord_less_eq_nat @ (times_times_nat @ A @ B) @ zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 13.71/3.47  thf(152,axiom,(((^ [A:nat]: (A)) = (times_times_nat @ one_one_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_60_lambda__one)).
% 13.71/3.47  thf(834,plain,(((^ [A:nat]: (A)) = (times_times_nat @ one_one_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 13.71/3.47  thf(107,axiom,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_97_bot__nat__0_Oextremum__unique)).
% 13.71/3.47  thf(634,plain,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 13.71/3.47  thf(215,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/sandbox2/benchmark/theBenchmark.p',fact_29_Nat_Odiff__diff__eq)).
% 13.71/3.47  thf(1072,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)],[215])).
% 13.71/3.47  thf(133,axiom,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_137_ord__eq__le__trans)).
% 13.71/3.47  thf(774,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)],[133])).
% 13.71/3.47  thf(197,axiom,((! [A:nat]: ((minus_minus_nat @ A @ zero_zero_nat) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_101_minus__nat_Odiff__0)).
% 13.71/3.47  thf(988,plain,((! [A:nat]: ((minus_minus_nat @ A @ zero_zero_nat) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 13.71/3.47  thf(44,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/sandbox2/benchmark/theBenchmark.p',fact_232_order__less__subst2)).
% 13.71/3.47  thf(428,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)],[44])).
% 13.71/3.47  thf(157,axiom,((! [A:nat,B:nat]: ((((ord_less_eq_nat @ zero_zero_nat @ A) & (ord_less_eq_nat @ B @ zero_zero_nat)) | ((ord_less_eq_nat @ A @ zero_zero_nat) & (ord_less_eq_nat @ zero_zero_nat @ B))) => (ord_less_eq_nat @ (times_times_nat @ A @ B) @ zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_108_split__mult__neg__le)).
% 13.71/3.47  thf(849,plain,((! [A:nat,B:nat]: ((((ord_less_eq_nat @ zero_zero_nat @ A) & (ord_less_eq_nat @ B @ zero_zero_nat)) | ((ord_less_eq_nat @ A @ zero_zero_nat) & (ord_less_eq_nat @ zero_zero_nat @ B))) => (ord_less_eq_nat @ (times_times_nat @ A @ B) @ zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 13.71/3.47  thf(77,axiom,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_74_le0)).
% 13.71/3.47  thf(527,plain,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 13.71/3.47  thf(165,axiom,((! [A:set_nat,B:set_nat,C:(nat > nat),D:(nat > nat)]: ((A = B) => ((! [E:nat]: ((member_nat @ E @ B) => ((C @ E) = (D @ E)))) => ((groups1842438620at_nat @ C @ A) = (groups1842438620at_nat @ D @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_50_sum_Ocong)).
% 13.71/3.47  thf(877,plain,((! [A:set_nat,B:set_nat,C:(nat > nat),D:(nat > nat)]: ((A = B) => ((! [E:nat]: ((member_nat @ E @ B) => ((C @ E) = (D @ E)))) => ((groups1842438620at_nat @ (C) @ A) = (groups1842438620at_nat @ (D) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 13.71/3.47  thf(119,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat,E:nat]: ((A != B) => ((fun_upd_nat_nat @ (fun_upd_nat_nat @ C @ A @ D) @ B @ E) = (fun_upd_nat_nat @ (fun_upd_nat_nat @ C @ B @ E) @ A @ D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_176_fun__upd__twist)).
% 13.71/3.47  thf(692,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat,E:nat]: ((~ (A = B)) => ((fun_upd_nat_nat @ (fun_upd_nat_nat @ C @ A @ D) @ B @ E) = (fun_upd_nat_nat @ (fun_upd_nat_nat @ C @ B @ E) @ A @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 13.71/3.47  thf(52,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/sandbox2/benchmark/theBenchmark.p',fact_234_ord__less__eq__subst)).
% 13.71/3.47  thf(452,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)],[52])).
% 13.71/3.47  thf(183,axiom,((! [A:nat]: ((minus_minus_nat @ zero_zero_nat @ A) = zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_70_zero__diff)).
% 13.71/3.47  thf(942,plain,((! [A:nat]: ((minus_minus_nat @ zero_zero_nat @ A) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 13.71/3.47  thf(78,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ C @ A) => (ord_less_eq_set_nat @ C @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_125_dual__order_Otrans)).
% 13.71/3.47  thf(529,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ C @ A) => (ord_less_eq_set_nat @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 13.71/3.47  thf(82,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_227_less__imp__neq)).
% 13.71/3.47  thf(546,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 13.71/3.47  thf(177,axiom,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ (times_times_nat @ A @ B) @ C) = (times_times_nat @ A @ (times_times_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_170_mult_Oassoc)).
% 13.71/3.47  thf(925,plain,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ (times_times_nat @ A @ B) @ C) = (times_times_nat @ A @ (times_times_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 13.71/3.47  thf(130,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (B = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_122_dual__order_Oantisym)).
% 13.71/3.47  thf(761,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)],[130])).
% 13.71/3.47  thf(33,axiom,((! [A:set_nat,B:(nat > set_nat),C:nat,D:nat]: ((ord_less_eq_set_nat @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_set_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_166_order__subst1)).
% 13.71/3.47  thf(381,plain,((! [A:set_nat,B:(nat > set_nat),C:nat,D:nat]: ((ord_less_eq_set_nat @ A @ (B @ C)) => ((ord_less_eq_nat @ C @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_set_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 13.71/3.47  thf(25,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((B = C) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_135_ord__le__eq__trans)).
% 13.71/3.47  thf(334,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)],[25])).
% 13.71/3.47  thf(188,axiom,((! [A:(nat > nat),B:nat]: ((! [C:nat]: (((A @ C) != zero_zero_nat) => ((ord_less_eq_nat @ one_one_nat @ C) & (ord_less_eq_nat @ C @ B)))) => (((groups1842438620at_nat @ (^ [C:nat]: (times_times_nat @ (A @ C) @ C)) @ (set_ord_atMost_nat @ B)) = B) => (number1551313001itions @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_partitionsI)).
% 13.71/3.47  thf(957,plain,((! [A:(nat > nat),B:nat]: ((! [C:nat]: ((~ ((A @ C) = zero_zero_nat)) => ((ord_less_eq_nat @ one_one_nat @ C) & (ord_less_eq_nat @ C @ B)))) => (((groups1842438620at_nat @ (^ [C:nat]: (times_times_nat @ (A @ C) @ C)) @ (set_ord_atMost_nat @ B)) = B) => (number1551313001itions @ (A) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 13.71/3.47  thf(221,axiom,((! [A:(nat > nat),B:nat]: ((number1551313001itions @ A @ B) => (~ ((! [C:nat]: (((A @ C) != zero_zero_nat) => ((ord_less_eq_nat @ one_one_nat @ C) & (ord_less_eq_nat @ C @ B)))) => ((groups1842438620at_nat @ (^ [C:nat]: (times_times_nat @ (A @ C) @ C)) @ (set_ord_atMost_nat @ B)) != B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_63_partitionsE)).
% 13.71/3.47  thf(1091,plain,((! [A:(nat > nat),B:nat]: ((number1551313001itions @ (A) @ B) => (~ ((! [C:nat]: ((~ ((A @ C) = zero_zero_nat)) => ((ord_less_eq_nat @ one_one_nat @ C) & (ord_less_eq_nat @ C @ B)))) => (~ ((groups1842438620at_nat @ (^ [C:nat]: (times_times_nat @ (A @ C) @ C)) @ (set_ord_atMost_nat @ B)) = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 13.71/3.47  thf(161,axiom,((! [A:nat,B:nat,C:nat]: (((times_times_nat @ A @ B) = (times_times_nat @ A @ C)) = ((A = zero_zero_nat) | (B = C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_68_mult__cancel__left)).
% 13.71/3.47  thf(862,plain,((! [A:nat,B:nat,C:nat]: (((times_times_nat @ A @ B) = (times_times_nat @ A @ C)) = ((A = zero_zero_nat) | (B = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 13.71/3.47  thf(37,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/sandbox2/benchmark/theBenchmark.p',fact_131_order__trans)).
% 13.71/3.47  thf(407,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)],[37])).
% 13.71/3.47  thf(147,axiom,((! [A:nat,B:nat]: ((A != zero_zero_nat) => ((B != zero_zero_nat) => ((times_times_nat @ A @ B) != zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_89_no__zero__divisors)).
% 13.71/3.47  thf(815,plain,((! [A:nat,B:nat]: ((~ (A = zero_zero_nat)) => ((~ (B = zero_zero_nat)) => (~ ((times_times_nat @ A @ B) = zero_zero_nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 13.71/3.47  thf(127,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/sandbox2/benchmark/theBenchmark.p',fact_23_bounded__Max__nat)).
% 13.71/3.47  thf(729,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)],[127])).
% 13.71/3.47  thf(14,axiom,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_86_zero__le)).
% 13.71/3.47  thf(275,plain,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 13.71/3.47  thf(137,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/sandbox2/benchmark/theBenchmark.p',fact_210_order_Ostrict__trans)).
% 13.71/3.47  thf(788,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)],[137])).
% 13.71/3.47  thf(207,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ one_one_nat) => ((ord_less_eq_nat @ zero_zero_nat @ B) => ((ord_less_eq_nat @ B @ one_one_nat) => (ord_less_eq_nat @ (times_times_nat @ A @ B) @ one_one_nat)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_117_mult__le__one)).
% 13.71/3.47  thf(1032,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ one_one_nat) => ((ord_less_eq_nat @ zero_zero_nat @ B) => ((ord_less_eq_nat @ B @ one_one_nat) => (ord_less_eq_nat @ (times_times_nat @ A @ B) @ one_one_nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 13.71/3.47  thf(23,axiom,((! [A:set_nat]: (ord_less_eq_set_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_58_order__refl)).
% 13.71/3.47  thf(329,plain,((! [A:set_nat]: (ord_less_eq_set_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 13.71/3.47  thf(167,axiom,((times_times_nat = (^ [A:nat,B:nat]: (times_times_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_171_mult_Ocommute)).
% 13.71/3.47  thf(889,plain,(((times_times_nat) = (^ [A:nat,B:nat]: (times_times_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 13.71/3.47  thf(53,axiom,((fun_upd_nat_nat = (^ [A:(nat > nat),B:nat,C:nat,D:nat]: (if_nat @ (D = B) @ C @ (A @ D))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_57_fun__upd__apply)).
% 13.71/3.47  thf(461,plain,(((fun_upd_nat_nat) = (^ [A:(nat > nat),B:nat,C:nat,D:nat]: (if_nat @ (D = B) @ C @ (A @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 13.71/3.47  thf(64,axiom,((! [A:set_nat,B:set_nat]: ((A = B) => (ord_less_eq_set_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_146_eq__refl)).
% 13.71/3.47  thf(493,plain,((! [A:set_nat,B:set_nat]: ((A = B) => (ord_less_eq_set_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 13.71/3.47  thf(155,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/sandbox2/benchmark/theBenchmark.p',fact_31_eq__diff__iff)).
% 13.71/3.47  thf(842,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)],[155])).
% 13.71/3.47  thf(74,axiom,((ord_less_eq_nat @ one_one_nat @ one_one_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_190_le__numeral__extra_I4_J)).
% 13.71/3.47  thf(522,plain,((ord_less_eq_nat @ one_one_nat @ one_one_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 13.71/3.47  thf(150,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ (times_times_nat @ A @ (times_times_nat @ A @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_36_le__cube)).
% 13.71/3.47  thf(830,plain,((! [A:nat]: (ord_less_eq_nat @ A @ (times_times_nat @ A @ (times_times_nat @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 13.71/3.47  thf(22,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/sandbox2/benchmark/theBenchmark.p',fact_164_order__subst2)).
% 13.71/3.47  thf(324,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)],[22])).
% 13.71/3.47  thf(192,axiom,((! [A:nat]: ((minus_minus_nat @ A @ A) = zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_76_diff__self__eq__0)).
% 13.71/3.47  thf(974,plain,((! [A:nat]: ((minus_minus_nat @ A @ A) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 13.71/3.47  thf(73,axiom,((zero_zero_nat != one_one_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_92_zero__neq__one)).
% 13.71/3.47  thf(519,plain,((~ (zero_zero_nat = one_one_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 13.71/3.47  thf(164,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/sandbox2/benchmark/theBenchmark.p',fact_28_diff__le__mono)).
% 13.71/3.47  thf(874,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)],[164])).
% 13.71/3.47  thf(185,axiom,((! [A:nat,B:(nat > nat),C:set_nat]: ((times_times_nat @ A @ (groups1842438620at_nat @ B @ C)) = (groups1842438620at_nat @ (^ [D:nat]: (times_times_nat @ A @ (B @ D))) @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_sum__distrib__left)).
% 13.71/3.47  thf(948,plain,((! [A:nat,B:(nat > nat),C:set_nat]: ((times_times_nat @ A @ (groups1842438620at_nat @ (B) @ C)) = (groups1842438620at_nat @ (^ [D:nat]: (times_times_nat @ A @ (B @ D))) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 13.71/3.47  thf(229,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((minus_minus_nat @ B @ (minus_minus_nat @ B @ A)) = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_14_diff__diff__cancel)).
% 13.71/3.47  thf(1121,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)],[229])).
% 13.71/3.47  thf(126,axiom,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((A != B) => ((fun_upd_nat_nat @ C @ B @ D @ A) = (C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_177_fun__upd__other)).
% 13.71/3.47  thf(725,plain,((! [A:nat,B:nat,C:(nat > nat),D:nat]: ((~ (A = B)) => ((fun_upd_nat_nat @ (C) @ B @ D @ A) = (C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 13.71/3.47  thf(194,axiom,(((^ [A:nat]: (zero_zero_nat)) = (times_times_nat @ zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_93_lambda__zero)).
% 13.71/3.47  thf(980,plain,(((^ [A:nat]: (zero_zero_nat)) = (times_times_nat @ zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 13.71/3.47  thf(203,axiom,((! [A:nat,B:nat]: ((member_nat @ A @ (set_ord_atMost_nat @ B)) = (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_13_atMost__iff)).
% 13.71/3.47  thf(1006,plain,((! [A:nat,B:nat]: ((member_nat @ A @ (set_ord_atMost_nat @ B)) = (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 13.71/3.47  thf(228,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_33_mult__le__mono1)).
% 13.71/3.47  thf(1118,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 13.71/3.47  thf(66,axiom,((! [A:(nat > nat)]: ((number1551313001itions @ A @ zero_zero_nat) = (A = (^ [B:nat]: (zero_zero_nat)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_115_partitions__zero)).
% 13.71/3.47  thf(499,plain,((! [A:(nat > nat)]: ((number1551313001itions @ (A) @ zero_zero_nat) = ((A) = (^ [B:nat]: (zero_zero_nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 13.71/3.47  thf(218,axiom,((! [A:nat]: ((times_times_nat @ A @ one_one_nat) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_37_nat__mult__1__right)).
% 13.71/3.47  thf(1082,plain,((! [A:nat]: ((times_times_nat @ A @ one_one_nat) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 13.71/3.47  thf(26,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_133_order__class_Oorder_Oantisym)).
% 13.71/3.47  thf(339,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)],[26])).
% 13.71/3.47  thf(180,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/sandbox2/benchmark/theBenchmark.p',fact_51_diff__commute)).
% 13.71/3.47  thf(933,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)],[180])).
% 13.71/3.47  thf(81,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/sandbox2/benchmark/theBenchmark.p',fact_235_ord__eq__less__subst)).
% 13.71/3.47  thf(537,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)],[81])).
% 13.71/3.47  thf(116,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((A = B) => ((ord_less_eq_set_nat @ B @ C) => (ord_less_eq_set_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_136_ord__eq__le__trans)).
% 13.71/3.47  thf(669,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((A = B) => ((ord_less_eq_set_nat @ B @ C) => (ord_less_eq_set_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 13.71/3.47  thf(109,axiom,((! [A:nat,B:nat]: ((A != B) => ((~ (ord_less_nat @ A @ B)) => (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_238_linorder__neqE__nat)).
% 13.71/3.47  thf(642,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)],[109])).
% 13.71/3.47  thf(108,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ A @ B) => ((B = C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_220_ord__less__eq__trans)).
% 13.71/3.47  thf(637,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)],[108])).
% 13.71/3.47  thf(63,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (A != B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_218_less__imp__not__eq)).
% 13.71/3.47  thf(489,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 13.71/3.47  thf(191,axiom,((! [A:set_nat,B:(nat > nat)]: ((! [C:nat]: ((member_nat @ C @ A) => (ord_less_eq_nat @ (B @ C) @ zero_zero_nat))) => (ord_less_eq_nat @ (groups1842438620at_nat @ B @ A) @ zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_118_sum__nonpos)).
% 13.71/3.47  thf(970,plain,((! [A:set_nat,B:(nat > nat)]: ((! [C:nat]: ((member_nat @ C @ A) => (ord_less_eq_nat @ (B @ C) @ zero_zero_nat))) => (ord_less_eq_nat @ (groups1842438620at_nat @ (B) @ A) @ zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 13.71/3.47  thf(239,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ D) => ((ord_less_eq_nat @ zero_zero_nat @ A) => ((ord_less_eq_nat @ zero_zero_nat @ C) => (ord_less_eq_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ D)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_111_mult__mono_H)).
% 13.71/3.47  thf(1155,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ D) => ((ord_less_eq_nat @ zero_zero_nat @ A) => ((ord_less_eq_nat @ zero_zero_nat @ C) => (ord_less_eq_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 13.71/3.47  thf(200,axiom,((! [A:nat]: ((times_times_nat @ A @ zero_zero_nat) = zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_78_mult__0__right)).
% 13.71/3.47  thf(997,plain,((! [A:nat]: ((times_times_nat @ A @ zero_zero_nat) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 13.71/3.47  thf(113,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) | (A = B) | (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_223_less__linear)).
% 13.71/3.47  thf(654,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)],[113])).
% 13.71/3.47  thf(210,axiom,((! [A:nat]: ((times_times_nat @ one_one_nat @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_54_mult_Oleft__neutral)).
% 13.71/3.47  thf(1060,plain,((! [A:nat]: ((times_times_nat @ one_one_nat @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 13.71/3.47  thf(124,axiom,((~ (ord_less_eq_nat @ one_one_nat @ zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_113_not__one__le__zero)).
% 13.71/3.47  thf(721,plain,((~ (ord_less_eq_nat @ one_one_nat @ zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 13.71/3.47  thf(90,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_19_eq__imp__le)).
% 13.71/3.47  thf(569,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 13.71/3.47  thf(134,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_194_less__nat__zero__code)).
% 13.71/3.47  thf(779,plain,((! [A:nat]: ~ (ord_less_nat @ A @ zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 13.71/3.47  thf(222,axiom,((! [A:nat,B:nat]: (((times_times_nat @ A @ B) = zero_zero_nat) = ((A = zero_zero_nat) | (B = zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_67_mult__eq__0__iff)).
% 13.71/3.47  thf(1099,plain,((! [A:nat,B:nat]: (((times_times_nat @ A @ B) = zero_zero_nat) = ((A = zero_zero_nat) | (B = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 13.71/3.47  thf(196,axiom,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ A @ (minus_minus_nat @ B @ C)) = (minus_minus_nat @ (times_times_nat @ A @ B) @ (times_times_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_183_right__diff__distrib_H)).
% 13.71/3.47  thf(985,plain,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ A @ (minus_minus_nat @ B @ C)) = (minus_minus_nat @ (times_times_nat @ A @ B) @ (times_times_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 13.71/3.47  thf(1,conjecture,(((minus_minus_nat @ (groups1842438620at_nat @ (^ [A:nat]: (times_times_nat @ (p @ A) @ A)) @ (set_ord_atMost_nat @ n)) @ k) = (minus_minus_nat @ n @ k))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 13.71/3.47  thf(2,negated_conjecture,((~ ((minus_minus_nat @ (groups1842438620at_nat @ (^ [A:nat]: (times_times_nat @ (p @ A) @ A)) @ (set_ord_atMost_nat @ n)) @ k) = (minus_minus_nat @ n @ k)))),inference(neg_conjecture,[status(cth)],[1])).
% 13.71/3.47  thf(244,plain,((~ ((minus_minus_nat @ (groups1842438620at_nat @ (^ [A:nat]: (times_times_nat @ (p @ A) @ A)) @ (set_ord_atMost_nat @ n)) @ k) = (minus_minus_nat @ n @ k)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 13.71/3.47  thf(10,axiom,((ord_less_eq_nat @ zero_zero_nat @ one_one_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_114_zero__le__one)).
% 13.71/3.47  thf(266,plain,((ord_less_eq_nat @ zero_zero_nat @ one_one_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 13.71/3.47  thf(143,axiom,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ A @ (times_times_nat @ B @ C)) = (times_times_nat @ B @ (times_times_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_172_mult_Oleft__commute)).
% 13.71/3.47  thf(805,plain,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ A @ (times_times_nat @ B @ C)) = (times_times_nat @ B @ (times_times_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 13.71/3.47  thf(69,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_222_less__irrefl)).
% 13.71/3.47  thf(508,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 13.71/3.47  thf(114,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/sandbox2/benchmark/theBenchmark.p',fact_127_linorder__wlog)).
% 13.71/3.47  thf(657,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)],[114])).
% 13.71/3.47  thf(208,axiom,((! [A:(nat > nat),B:set_nat]: (((groups1842438620at_nat @ A @ B) != zero_zero_nat) => (~ (! [C:nat]: ((member_nat @ C @ B) => ((A @ C) = zero_zero_nat))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_95_sum_Onot__neutral__contains__not__neutral)).
% 13.71/3.47  thf(1035,plain,((! [A:(nat > nat),B:set_nat]: ((~ ((groups1842438620at_nat @ (A) @ B) = zero_zero_nat)) => (~ (! [C:nat]: ((member_nat @ C @ B) => ((A @ C) = zero_zero_nat))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 13.71/3.47  thf(117,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ A) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_187_subset__antisym)).
% 13.71/3.47  thf(674,plain,((! [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 13.71/3.47  thf(132,axiom,((ord_less_eq_nat @ zero_zero_nat @ zero_zero_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_191_le__numeral__extra_I3_J)).
% 13.71/3.47  thf(773,plain,((ord_less_eq_nat @ zero_zero_nat @ zero_zero_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 13.71/3.47  thf(139,axiom,((! [A:(nat > nat),B:nat]: ((number1551313001itions @ A @ B) => (ord_less_eq_nat @ (groups1842438620at_nat @ A @ (set_ord_atMost_nat @ B)) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_43_partitions__parts__bounded)).
% 13.71/3.47  thf(794,plain,((! [A:(nat > nat),B:nat]: ((number1551313001itions @ (A) @ B) => (ord_less_eq_nat @ (groups1842438620at_nat @ (A) @ (set_ord_atMost_nat @ B)) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 13.71/3.47  thf(95,axiom,((! [A:nat]: ((~ (ord_less_nat @ zero_zero_nat @ A)) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_192_not__gr__zero)).
% 13.71/3.47  thf(586,plain,((! [A:nat]: ((~ (ord_less_nat @ zero_zero_nat @ A)) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 13.71/3.47  thf(173,axiom,((! [A:nat]: ((times_times_nat @ zero_zero_nat @ A) = zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_65_mult__zero__left)).
% 13.71/3.47  thf(906,plain,((! [A:nat]: ((times_times_nat @ zero_zero_nat @ A) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 13.71/3.47  thf(39,axiom,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_64_le__zero__eq)).
% 13.71/3.47  thf(412,plain,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 13.71/3.47  thf(101,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) | (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_21_nat__le__linear)).
% 13.71/3.47  thf(618,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)],[101])).
% 13.71/3.47  thf(9,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_209_less__imp__not__less)).
% 13.71/3.47  thf(264,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 13.71/3.47  thf(159,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ D) => ((ord_less_eq_nat @ zero_zero_nat @ B) => ((ord_less_eq_nat @ zero_zero_nat @ C) => (ord_less_eq_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ D)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_112_mult__mono)).
% 13.71/3.47  thf(856,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ D) => ((ord_less_eq_nat @ zero_zero_nat @ B) => ((ord_less_eq_nat @ zero_zero_nat @ C) => (ord_less_eq_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 13.71/3.47  thf(91,axiom,((! [A:(nat > nat),B:nat]: ((fun_upd_nat_nat @ A @ B @ (A @ B)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_56_fun__upd__triv)).
% 13.71/3.47  thf(573,plain,((! [A:(nat > nat),B:nat]: ((fun_upd_nat_nat @ A @ B @ (A @ B)) = (A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 13.71/3.47  thf(148,axiom,((! [A:nat,B:nat]: ((ord_less_eq_set_nat @ (set_ord_atMost_nat @ A) @ (set_ord_atMost_nat @ B)) = (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11_atMost__subset__iff)).
% 13.71/3.47  thf(819,plain,((! [A:nat,B:nat]: ((ord_less_eq_set_nat @ (set_ord_atMost_nat @ A) @ (set_ord_atMost_nat @ B)) = (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 13.71/3.47  thf(43,axiom,((! [A:set_nat,B:set_nat,C:(set_nat > set_nat),D:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ (C @ B) @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_nat @ E @ F) => (ord_less_eq_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_set_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_163_order__subst2)).
% 13.71/3.47  thf(423,plain,((! [A:set_nat,B:set_nat,C:(set_nat > set_nat),D:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ (C @ B) @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_nat @ E @ F) => (ord_less_eq_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_set_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 13.71/3.47  thf(128,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/sandbox2/benchmark/theBenchmark.p',fact_160_ord__eq__le__subst)).
% 13.71/3.47  thf(743,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)],[128])).
% 13.71/3.47  thf(230,axiom,((! [A:set_nat]: ((groups1842438620at_nat @ (^ [B:nat]: (zero_zero_nat)) @ A) = zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_81_sum_Oneutral__const)).
% 13.71/3.47  thf(1124,plain,((! [A:set_nat]: ((groups1842438620at_nat @ (^ [B:nat]: (zero_zero_nat)) @ A) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 13.71/3.47  thf(87,axiom,((! [A:nat,B:nat]: ((A != B) = ((ord_less_nat @ A @ B) | (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_229_neq__iff)).
% 13.71/3.47  thf(562,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)],[87])).
% 13.71/3.47  thf(172,axiom,((set_ord_atMost_nat = (^ [A:nat]: (collect_nat @ (^ [B:nat]: (ord_less_eq_nat @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_41_atMost__def)).
% 13.71/3.47  thf(904,plain,(((set_ord_atMost_nat) = (^ [A:nat]: (collect_nat @ (^ [B:nat]: (ord_less_eq_nat @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 13.71/3.47  thf(93,axiom,((! [A:nat]: ? [B:nat]: (ord_less_nat @ A @ B))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_231_gt__ex)).
% 13.71/3.47  thf(579,plain,((! [A:nat]: ? [B:nat]: (ord_less_nat @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 13.71/3.47  thf(18,axiom,((! [A:(nat > nat),B:nat,C:nat]: (((fun_upd_nat_nat @ A @ B @ C) = A) = ((A @ B) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_175_fun__upd__idem__iff)).
% 13.71/3.47  thf(291,plain,((! [A:(nat > nat),B:nat,C:nat]: (((fun_upd_nat_nat @ A @ B @ C) = (A)) = ((A @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 13.71/3.47  thf(235,axiom,((! [A:set_nat,B:(nat > nat),C:(nat > nat)]: ((! [D:nat]: ((member_nat @ D @ A) => (ord_less_eq_nat @ (B @ D) @ (C @ D)))) => ((groups1842438620at_nat @ (^ [D:nat]: (minus_minus_nat @ (C @ D) @ (B @ D))) @ A) = (minus_minus_nat @ (groups1842438620at_nat @ C @ A) @ (groups1842438620at_nat @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_42_sum__subtractf__nat)).
% 13.71/3.47  thf(1139,plain,((! [A:set_nat,B:(nat > nat),C:(nat > nat)]: ((! [D:nat]: ((member_nat @ D @ A) => (ord_less_eq_nat @ (B @ D) @ (C @ D)))) => ((groups1842438620at_nat @ (^ [D:nat]: (minus_minus_nat @ (C @ D) @ (B @ D))) @ A) = (minus_minus_nat @ (groups1842438620at_nat @ (C) @ A) @ (groups1842438620at_nat @ (B) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 13.71/3.47  thf(55,axiom,((! [A:nat,B:(nat > $o)]: ((member_nat @ A @ (collect_nat @ B)) = (B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_44_mem__Collect__eq)).
% 13.71/3.47  thf(466,plain,((! [A:nat,B:(nat > $o)]: ((member_nat @ A @ (collect_nat @ (B))) = (B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 13.71/3.47  thf(49,axiom,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_99_less__eq__nat_Osimps_I1_J)).
% 13.71/3.47  thf(445,plain,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 13.71/3.47  thf(181,axiom,((! [A:nat,B:nat]: (((set_ord_atMost_nat @ A) = (set_ord_atMost_nat @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_atMost__eq__iff)).
% 13.71/3.47  thf(936,plain,((! [A:nat,B:nat]: (((set_ord_atMost_nat @ A) = (set_ord_atMost_nat @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 13.71/3.47  thf(131,axiom,((! [A:set_nat,B:set_nat,C:(set_nat > set_nat),D:set_nat]: ((ord_less_eq_set_nat @ A @ B) => (((C @ B) = D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_nat @ E @ F) => (ord_less_eq_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_set_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_155_ord__le__eq__subst)).
% 13.71/3.47  thf(764,plain,((! [A:set_nat,B:set_nat,C:(set_nat > set_nat),D:set_nat]: ((ord_less_eq_set_nat @ A @ B) => (((C @ B) = D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_nat @ E @ F) => (ord_less_eq_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_set_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 13.71/3.47  thf(89,axiom,((set_or1086813439et_nat = (^ [A:set_nat]: (collect_set_nat @ (^ [B:set_nat]: (ord_less_eq_set_nat @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_40_atMost__def)).
% 13.71/3.47  thf(567,plain,(((set_or1086813439et_nat) = (^ [A:set_nat]: (collect_set_nat @ (^ [B:set_nat]: (ord_less_eq_set_nat @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 13.71/3.47  thf(13,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_203_dual__order_Ostrict__implies__not__eq)).
% 13.71/3.47  thf(271,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 13.71/3.47  thf(59,axiom,((! [A:(nat > nat),B:nat,C:nat]: (((A @ B) = C) => ((fun_upd_nat_nat @ A @ B @ C) = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_179_fun__upd__idem)).
% 13.71/3.47  thf(477,plain,((! [A:(nat > nat),B:nat,C:nat]: (((A @ B) = C) => ((fun_upd_nat_nat @ A @ B @ C) = (A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 13.71/3.47  thf(106,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ A) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_132_order__class_Oorder_Oantisym)).
% 13.71/3.47  thf(631,plain,((! [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 13.71/3.47  thf(80,axiom,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_73_bot__nat__0_Oextremum)).
% 13.71/3.47  thf(535,plain,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 13.71/3.47  thf(100,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((~ (A @ C)) => (? [D:nat]: ((ord_less_nat @ D @ C) & ~ (A @ D))))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_239_infinite__descent)).
% 13.71/3.47  thf(609,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)],[100])).
% 13.71/3.47  thf(97,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/sandbox2/benchmark/theBenchmark.p',fact_206_dual__order_Ostrict__trans)).
% 13.71/3.47  thf(594,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)],[97])).
% 13.71/3.47  thf(61,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/sandbox2/benchmark/theBenchmark.p',fact_224_less__trans)).
% 13.71/3.47  thf(483,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)],[61])).
% 13.71/3.47  thf(206,axiom,((! [A:nat,B:nat]: (((times_times_nat @ A @ B) = one_one_nat) = ((A = one_one_nat) & (B = one_one_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_15_nat__mult__eq__1__iff)).
% 13.71/3.48  thf(1029,plain,((! [A:nat,B:nat]: (((times_times_nat @ A @ B) = one_one_nat) = ((A = one_one_nat) & (B = one_one_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 13.71/3.48  thf(237,axiom,((! [A:nat,B:nat]: (((minus_minus_nat @ A @ B) = zero_zero_nat) => (((minus_minus_nat @ B @ A) = zero_zero_nat) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_100_diffs0__imp__equal)).
% 13.71/3.48  thf(1149,plain,((! [A:nat,B:nat]: (((minus_minus_nat @ A @ B) = zero_zero_nat) => (((minus_minus_nat @ B @ A) = zero_zero_nat) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 13.71/3.48  thf(104,axiom,((! [A:set_nat]: ((collect_nat @ (^ [B:nat]: (member_nat @ B @ A))) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_45_Collect__mem__eq)).
% 13.71/3.48  thf(626,plain,((! [A:set_nat]: ((collect_nat @ (^ [B:nat]: (member_nat @ B @ A))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 13.71/3.48  thf(226,axiom,((! [A:nat,B:nat,C:nat]: (((times_times_nat @ A @ B) = (times_times_nat @ A @ C)) = ((A = zero_zero_nat) | (B = C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_189_nat__mult__eq__cancel__disj)).
% 13.71/3.48  thf(1112,plain,((! [A:nat,B:nat,C:nat]: (((times_times_nat @ A @ B) = (times_times_nat @ A @ C)) = ((A = zero_zero_nat) | (B = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 13.71/3.48  thf(28,axiom,((! [A:nat,B:nat,C:(nat > set_nat),D:set_nat]: ((ord_less_eq_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_set_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_153_ord__le__eq__subst)).
% 13.71/3.48  thf(345,plain,((! [A:nat,B:nat,C:(nat > set_nat),D:set_nat]: ((ord_less_eq_nat @ A @ B) => (((C @ B) = D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_set_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 13.71/3.48  thf(84,axiom,((! [A:nat,B:nat,C:nat]: ((A = B) => ((ord_less_nat @ B @ C) => (ord_less_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_221_ord__eq__less__trans)).
% 13.71/3.48  thf(552,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)],[84])).
% 13.71/3.48  thf(141,axiom,((! [A:nat]: ((times_times_nat @ one_one_nat @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_184_comm__monoid__mult__class_Omult__1)).
% 13.71/3.48  thf(799,plain,((! [A:nat]: ((times_times_nat @ one_one_nat @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 13.71/3.48  thf(241,axiom,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ D) => (ord_less_eq_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_34_mult__le__mono)).
% 13.71/3.48  thf(1162,plain,((! [A:nat,B:nat,C:nat,D:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ C @ D) => (ord_less_eq_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 13.71/3.48  thf(175,axiom,((! [A:set_nat,B:(nat > nat),C:set_nat,D:(nat > nat),E:(nat > nat),F:(nat > nat)]: ((! [G:nat]: ((member_nat @ G @ A) => ((member_nat @ (B @ G) @ C) & ((D @ (B @ G)) = G)))) => ((! [G:nat]: ((member_nat @ G @ C) => ((member_nat @ (D @ G) @ A) & ((B @ (D @ G)) = G) & ((E @ (D @ G)) = (F @ G))))) => ((groups1842438620at_nat @ F @ C) = (groups1842438620at_nat @ E @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_48_sum_Oeq__general__inverses)).
% 13.71/3.48  thf(912,plain,((! [A:set_nat,B:(nat > nat),C:set_nat,D:(nat > nat),E:(nat > nat),F:(nat > nat)]: ((! [G:nat]: ((member_nat @ G @ A) => ((member_nat @ (B @ G) @ C) & ((D @ (B @ G)) = G)))) => ((! [G:nat]: ((member_nat @ G @ C) => ((member_nat @ (D @ G) @ A) & ((B @ (D @ G)) = G) & ((E @ (D @ G)) = (F @ G))))) => ((groups1842438620at_nat @ (F) @ C) = (groups1842438620at_nat @ (E) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 13.71/3.48  thf(201,axiom,((! [A:nat,B:nat]: (((times_times_nat @ A @ B) = zero_zero_nat) => ((A = zero_zero_nat) | (B = zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_88_divisors__zero)).
% 13.71/3.48  thf(1000,plain,((! [A:nat,B:nat]: (((times_times_nat @ A @ B) = zero_zero_nat) => ((A = zero_zero_nat) | (B = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 13.71/3.48  thf(176,axiom,((! [A:nat]: ((times_times_nat @ A @ zero_zero_nat) = zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_66_mult__zero__right)).
% 13.71/3.48  thf(922,plain,((! [A:nat]: ((times_times_nat @ A @ zero_zero_nat) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 13.71/3.48  thf(212,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/sandbox2/benchmark/theBenchmark.p',fact_173_cancel__ab__semigroup__add__class_Odiff__right__commute)).
% 13.71/3.48  thf(1066,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)],[212])).
% 13.71/3.48  thf(163,axiom,((! [A:set_nat,B:(nat > nat)]: ((! [C:nat]: ((member_nat @ C @ A) => ((B @ C) = zero_zero_nat))) => ((groups1842438620at_nat @ B @ A) = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_94_sum_Oneutral)).
% 13.71/3.48  thf(868,plain,((! [A:set_nat,B:(nat > nat)]: ((! [C:nat]: ((member_nat @ C @ A) => ((B @ C) = zero_zero_nat))) => ((groups1842438620at_nat @ (B) @ A) = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 13.71/3.48  thf(11,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_17_le__refl)).
% 13.71/3.48  thf(267,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 13.71/3.48  thf(223,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ zero_zero_nat @ C) => (ord_less_eq_nat @ (times_times_nat @ C @ A) @ (times_times_nat @ C @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_110_mult__left__mono)).
% 13.71/3.48  thf(1102,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ zero_zero_nat @ C) => (ord_less_eq_nat @ (times_times_nat @ C @ A) @ (times_times_nat @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 13.71/3.48  thf(68,axiom,((! [A:(nat > nat),B:nat,C:nat]: ((fun_upd_nat_nat @ A @ B @ C @ B) = C))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_178_fun__upd__same)).
% 13.71/3.48  thf(505,plain,((! [A:(nat > nat),B:nat,C:nat]: ((fun_upd_nat_nat @ (A) @ B @ C @ B) = C))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 13.71/3.48  thf(47,axiom,((! [A:nat,B:nat]: ((A != B) => ((~ (ord_less_nat @ A @ B)) => (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_230_neqE)).
% 13.71/3.48  thf(438,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)],[47])).
% 13.71/3.48  thf(216,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ (times_times_nat @ A @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_35_le__square)).
% 13.71/3.48  thf(1076,plain,((! [A:nat]: (ord_less_eq_nat @ A @ (times_times_nat @ A @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 13.71/3.48  thf(96,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/sandbox2/benchmark/theBenchmark.p',fact_233_order__less__subst1)).
% 13.71/3.48  thf(589,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)],[96])).
% 13.71/3.48  thf(6,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_228_order_Oasym)).
% 13.71/3.48  thf(255,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 13.71/3.48  thf(111,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ A) = (B = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_140_antisym__conv)).
% 13.71/3.48  thf(648,plain,((! [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ A) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 13.71/3.48  thf(146,axiom,((! [A:nat,B:nat]: (((times_times_nat @ A @ B) = zero_zero_nat) = ((A = zero_zero_nat) | (B = zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_77_mult__is__0)).
% 13.71/3.48  thf(812,plain,((! [A:nat,B:nat]: (((times_times_nat @ A @ B) = zero_zero_nat) = ((A = zero_zero_nat) | (B = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 13.71/3.48  thf(72,axiom,((! [A:(nat > $o),B:(nat > $o)]: ((! [C:nat]: ((A @ C) = (B @ C))) => ((collect_nat @ A) = (collect_nat @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_46_Collect__cong)).
% 13.71/3.48  thf(516,plain,((! [A:(nat > $o),B:(nat > $o)]: ((! [C:nat]: ((A @ C) = (B @ C))) => ((collect_nat @ (A)) = (collect_nat @ (B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 13.71/3.48  thf(182,axiom,((! [A:nat,B:nat]: (((minus_minus_nat @ A @ B) = zero_zero_nat) = (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_83_diff__is__0__eq)).
% 13.71/3.48  thf(939,plain,((! [A:nat,B:nat]: (((minus_minus_nat @ A @ B) = zero_zero_nat) = (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 13.71/3.48  thf(27,axiom,((! [A:set_nat,B:set_nat]: ((ord_le1613022364et_nat @ (set_or1086813439et_nat @ A) @ (set_or1086813439et_nat @ B)) = (ord_less_eq_set_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_10_atMost__subset__iff)).
% 13.71/3.48  thf(342,plain,((! [A:set_nat,B:set_nat]: ((ord_le1613022364et_nat @ (set_or1086813439et_nat @ A) @ (set_or1086813439et_nat @ B)) = (ord_less_eq_set_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 13.71/3.48  thf(236,axiom,((! [A:set_nat,B:(nat > nat)]: ((! [C:nat]: ((member_nat @ C @ A) => (ord_less_eq_nat @ zero_zero_nat @ (B @ C)))) => (ord_less_eq_nat @ zero_zero_nat @ (groups1842438620at_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_119_sum__nonneg)).
% 13.71/3.48  thf(1145,plain,((! [A:set_nat,B:(nat > nat)]: ((! [C:nat]: ((member_nat @ C @ A) => (ord_less_eq_nat @ zero_zero_nat @ (B @ C)))) => (ord_less_eq_nat @ zero_zero_nat @ (groups1842438620at_nat @ (B) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 13.71/3.48  thf(153,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ zero_zero_nat @ A) => ((ord_less_eq_nat @ B @ zero_zero_nat) => (ord_less_eq_nat @ (times_times_nat @ B @ A) @ zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_104_mult__nonneg__nonpos2)).
% 13.71/3.48  thf(836,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ zero_zero_nat @ A) => ((ord_less_eq_nat @ B @ zero_zero_nat) => (ord_less_eq_nat @ (times_times_nat @ B @ A) @ zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 13.71/3.48  thf(76,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_217_less__not__sym)).
% 13.71/3.48  thf(525,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 13.71/3.48  thf(205,axiom,((! [A:nat,B:nat,C:nat]: ((A != zero_zero_nat) => (((times_times_nat @ A @ B) = (times_times_nat @ A @ C)) = (B = C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_90_mult__left__cancel)).
% 13.71/3.48  thf(1025,plain,((! [A:nat,B:nat,C:nat]: ((~ (A = zero_zero_nat)) => (((times_times_nat @ A @ B) = (times_times_nat @ A @ C)) = (B = C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 13.71/3.48  thf(214,axiom,((! [A:nat,B:nat]: (ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_27_diff__le__self)).
% 13.71/3.48  thf(1070,plain,((! [A:nat,B:nat]: (ord_less_eq_nat @ (minus_minus_nat @ A @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 13.71/3.48  thf(16,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/sandbox2/benchmark/theBenchmark.p',fact_168_order__subst1)).
% 13.71/3.48  thf(282,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)],[16])).
% 13.71/3.48  thf(122,axiom,((! [A:nat,B:nat,C:(nat > set_nat),D:set_nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_set_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_set_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_161_order__subst2)).
% 13.71/3.48  thf(707,plain,((! [A:nat,B:nat,C:(nat > set_nat),D:set_nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_set_nat @ (C @ B) @ D) => ((! [E:nat,F:nat]: ((ord_less_eq_nat @ E @ F) => (ord_less_eq_set_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_set_nat @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 13.71/3.48  thf(187,axiom,((! [A:nat]: ((minus_minus_nat @ zero_zero_nat @ A) = zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_75_diff__0__eq__0)).
% 13.71/3.48  thf(954,plain,((! [A:nat]: ((minus_minus_nat @ zero_zero_nat @ A) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 13.71/3.48  thf(20,axiom,((! [A:set_nat,B:(nat > set_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_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_set_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_157_ord__eq__le__subst)).
% 13.71/3.48  thf(310,plain,((! [A:set_nat,B:(nat > set_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_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_set_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 13.71/3.48  thf(123,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/sandbox2/benchmark/theBenchmark.p',fact_156_ord__le__eq__subst)).
% 13.71/3.48  thf(712,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)],[123])).
% 13.71/3.48  thf(85,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/sandbox2/benchmark/theBenchmark.p',fact_18_le__trans)).
% 13.71/3.48  thf(557,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)],[85])).
% 13.71/3.48  thf(202,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (times_times_nat @ A @ B) @ (times_times_nat @ A @ C)) = ((ord_less_nat @ zero_zero_nat @ A) & (ord_less_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_197_nat__mult__less__cancel__disj)).
% 13.71/3.48  thf(1003,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_nat @ (times_times_nat @ A @ B) @ (times_times_nat @ A @ C)) = ((ord_less_nat @ zero_zero_nat @ A) & (ord_less_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 13.71/3.48  thf(138,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (times_times_nat @ A @ B) @ (times_times_nat @ C @ B)) = ((ord_less_nat @ zero_zero_nat @ B) => (ord_less_eq_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_202_mult__le__cancel2)).
% 13.71/3.48  thf(791,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (times_times_nat @ A @ B) @ (times_times_nat @ C @ B)) = ((ord_less_nat @ zero_zero_nat @ B) => (ord_less_eq_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 13.71/3.48  thf(24,axiom,((! [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ A) => (B = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_121_dual__order_Oantisym)).
% 13.71/3.48  thf(331,plain,((! [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ A) => (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 13.71/3.48  thf(48,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_147_eq__refl)).
% 13.71/3.48  thf(441,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 13.71/3.48  thf(67,axiom,((! [A:(nat > nat),B:nat,C:nat]: ((number1551313001itions @ A @ B) => (ord_less_eq_nat @ (A @ C) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_24_partitions__bounds)).
% 13.71/3.48  thf(502,plain,((! [A:(nat > nat),B:nat,C:nat]: ((number1551313001itions @ (A) @ B) => (ord_less_eq_nat @ (A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 13.71/3.48  thf(54,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/sandbox2/benchmark/theBenchmark.p',fact_126_dual__order_Otrans)).
% 13.71/3.48  thf(463,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)],[54])).
% 13.71/3.48  thf(232,axiom,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ (times_times_nat @ A @ B) @ C) = (times_times_nat @ A @ (times_times_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_169_ab__semigroup__mult__class_Omult__ac_I1_J)).
% 13.71/3.48  thf(1130,plain,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ (times_times_nat @ A @ B) @ C) = (times_times_nat @ A @ (times_times_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 13.71/3.48  thf(219,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ zero_zero_nat @ C) => (ord_less_eq_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_109_mult__right__mono)).
% 13.71/3.48  thf(1085,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ zero_zero_nat @ C) => (ord_less_eq_nat @ (times_times_nat @ A @ C) @ (times_times_nat @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 13.71/3.48  thf(92,axiom,((! [A:nat]: ~ (ord_less_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_211_dual__order_Oirrefl)).
% 13.71/3.48  thf(576,plain,((! [A:nat]: ~ (ord_less_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 13.71/3.48  thf(186,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ zero_zero_nat @ A) => ((ord_less_eq_nat @ zero_zero_nat @ B) => (ord_less_eq_nat @ zero_zero_nat @ (times_times_nat @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_107_mult__nonneg__nonneg)).
% 13.71/3.48  thf(951,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ zero_zero_nat @ A) => ((ord_less_eq_nat @ zero_zero_nat @ B) => (ord_less_eq_nat @ zero_zero_nat @ (times_times_nat @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 13.71/3.48  thf(144,axiom,((ord_less_nat @ zero_zero_nat @ (p @ k))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_84_gr0)).
% 13.71/3.48  thf(808,plain,((ord_less_nat @ zero_zero_nat @ (p @ k))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 13.71/3.48  thf(99,axiom,((! [A:set_nat,B:(set_nat > set_nat),C:set_nat,D:set_nat]: ((A = (B @ C)) => ((ord_less_eq_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_nat @ E @ F) => (ord_less_eq_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_set_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_159_ord__eq__le__subst)).
% 13.71/3.48  thf(600,plain,((! [A:set_nat,B:(set_nat > set_nat),C:set_nat,D:set_nat]: ((A = (B @ C)) => ((ord_less_eq_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_nat @ E @ F) => (ord_less_eq_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_set_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 13.71/3.48  thf(34,axiom,((! [A:set_nat,B:set_nat,C:(set_nat > nat),D:nat]: ((ord_less_eq_set_nat @ A @ B) => (((C @ B) = D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_154_ord__le__eq__subst)).
% 13.71/3.48  thf(386,plain,((! [A:set_nat,B:set_nat,C:(set_nat > nat),D:nat]: ((ord_less_eq_set_nat @ A @ B) => (((C @ B) = D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_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])).
% 13.71/3.48  thf(65,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_59_order__refl)).
% 13.71/3.48  thf(497,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 13.71/3.48  thf(160,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/sandbox2/benchmark/theBenchmark.p',fact_25_diff__le__mono2)).
% 13.71/3.48  thf(859,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)],[160])).
% 13.71/3.48  thf(198,axiom,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ A @ (minus_minus_nat @ B @ C)) = (minus_minus_nat @ (times_times_nat @ A @ B) @ (times_times_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9_diff__mult__distrib2)).
% 13.71/3.48  thf(991,plain,((! [A:nat,B:nat,C:nat]: ((times_times_nat @ A @ (minus_minus_nat @ B @ C)) = (minus_minus_nat @ (times_times_nat @ A @ B) @ (times_times_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 13.71/3.48  thf(51,axiom,((((=) @ set_nat) = (^ [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ B @ A) & (ord_less_eq_set_nat @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_123_dual__order_Oeq__iff)).
% 13.71/3.48  thf(450,plain,((((=) @ set_nat) = (^ [A:set_nat,B:set_nat]: ((ord_less_eq_set_nat @ B @ A) & (ord_less_eq_set_nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 13.71/3.48  thf(171,axiom,((ord_less_eq_nat @ k @ n)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__092_060open_062k_A_092_060le_062_An_092_060close_062)).
% 13.71/3.48  thf(903,plain,((ord_less_eq_nat @ k @ n)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 13.71/3.48  thf(94,axiom,((! [A:set_nat,B:(set_nat > set_nat),C:set_nat,D:set_nat]: ((ord_less_eq_set_nat @ A @ (B @ C)) => ((ord_less_eq_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_nat @ E @ F) => (ord_less_eq_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_set_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_167_order__subst1)).
% 13.71/3.48  thf(581,plain,((! [A:set_nat,B:(set_nat > set_nat),C:set_nat,D:set_nat]: ((ord_less_eq_set_nat @ A @ (B @ C)) => ((ord_less_eq_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_nat @ E @ F) => (ord_less_eq_set_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_set_nat @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 13.71/3.48  thf(168,axiom,(((groups1842438620at_nat @ (^ [A:nat]: (times_times_nat @ (fun_upd_nat_nat @ p @ k @ (minus_minus_nat @ (p @ k) @ one_one_nat) @ A) @ A)) @ (set_ord_atMost_nat @ (minus_minus_nat @ n @ k))) = (groups1842438620at_nat @ (^ [A:nat]: (times_times_nat @ (fun_upd_nat_nat @ p @ k @ (minus_minus_nat @ (p @ k) @ one_one_nat) @ A) @ A)) @ (set_ord_atMost_nat @ n)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3__092_060open_062_I_092_060Sum_062i_092_060le_062n_A_N_Ak_O_A_Ip_Ik_A_058_061_Ap_Ak_A_N_A1_J_J_Ai_A_K_Ai_J_A_061_A_I_092_060Sum_062i_092_060le_062n_O_A_Ip_Ik_A_058_061_Ap_Ak_A_N_A1_J_J_Ai_A_K_Ai_J_092_060close_062)).
% 13.71/3.48  thf(891,plain,(((groups1842438620at_nat @ (^ [A:nat]: (times_times_nat @ (fun_upd_nat_nat @ p @ k @ (minus_minus_nat @ (p @ k) @ one_one_nat) @ A) @ A)) @ (set_ord_atMost_nat @ (minus_minus_nat @ n @ k))) = (groups1842438620at_nat @ (^ [A:nat]: (times_times_nat @ (fun_upd_nat_nat @ p @ k @ (minus_minus_nat @ (p @ k) @ one_one_nat) @ A) @ A)) @ (set_ord_atMost_nat @ n)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 13.71/3.48  thf(189,axiom,((! [A:set_nat,B:(nat > nat),C:(nat > nat)]: ((! [D:nat]: ((member_nat @ D @ A) => (ord_less_eq_nat @ (B @ D) @ (C @ D)))) => (ord_less_eq_nat @ (groups1842438620at_nat @ B @ A) @ (groups1842438620at_nat @ C @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_39_sum__mono)).
% 13.71/3.48  thf(963,plain,((! [A:set_nat,B:(nat > nat),C:(nat > nat)]: ((! [D:nat]: ((member_nat @ D @ A) => (ord_less_eq_nat @ (B @ D) @ (C @ D)))) => (ord_less_eq_nat @ (groups1842438620at_nat @ (B) @ A) @ (groups1842438620at_nat @ (C) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 13.71/3.48  thf(21,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((B = C) => (ord_less_eq_set_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_134_ord__le__eq__trans)).
% 13.71/3.48  thf(319,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((B = C) => (ord_less_eq_set_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 13.71/3.48  thf(170,axiom,((! [A:(nat > nat),B:nat,C:nat,D:nat]: ((number1551313001itions @ A @ B) => ((ord_less_nat @ zero_zero_nat @ (A @ C)) => (((fun_upd_nat_nat @ A @ C @ (minus_minus_nat @ (A @ C) @ one_one_nat) @ D) != zero_zero_nat) => ((ord_less_eq_nat @ one_one_nat @ D) & (ord_less_eq_nat @ D @ (minus_minus_nat @ B @ C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_188_partitions__remove1__bounds)).
% 13.71/3.48  thf(896,plain,((! [A:(nat > nat),B:nat,C:nat,D:nat]: ((number1551313001itions @ (A) @ B) => ((ord_less_nat @ zero_zero_nat @ (A @ C)) => ((~ ((fun_upd_nat_nat @ (A) @ C @ (minus_minus_nat @ (A @ C) @ one_one_nat) @ D) = zero_zero_nat)) => ((ord_less_eq_nat @ one_one_nat @ D) & (ord_less_eq_nat @ D @ (minus_minus_nat @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 13.71/3.48  thf(41,axiom,((! [A:(nat > nat),B:nat,C:nat,D:(nat > nat),E:nat]: (((fun_upd_nat_nat @ A @ B @ C) = (fun_upd_nat_nat @ D @ B @ E)) => (C = E)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_180_fun__upd__eqD)).
% 13.71/3.48  thf(418,plain,((! [A:(nat > nat),B:nat,C:nat,D:(nat > nat),E:nat]: (((fun_upd_nat_nat @ A @ B @ C) = (fun_upd_nat_nat @ D @ B @ E)) => (C = E)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 13.71/3.48  thf(3,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ C) => (ord_less_eq_set_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_143_order_Otrans)).
% 13.71/3.48  thf(246,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ C) => (ord_less_eq_set_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 13.71/3.48  thf(45,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ B @ A) => (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_150_antisym)).
% 13.71/3.48  thf(433,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)],[45])).
% 13.71/3.48  thf(151,axiom,(((groups1842438620at_nat @ (^ [A:nat]: (times_times_nat @ (fun_upd_nat_nat @ p @ k @ (minus_minus_nat @ (p @ k) @ one_one_nat) @ A) @ A)) @ (set_ord_atMost_nat @ (minus_minus_nat @ n @ k))) = (minus_minus_nat @ (groups1842438620at_nat @ (^ [A:nat]: (times_times_nat @ (p @ A) @ A)) @ (set_ord_atMost_nat @ n)) @ k))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_calculation)).
% 13.71/3.48  thf(832,plain,(((groups1842438620at_nat @ (^ [A:nat]: (times_times_nat @ (fun_upd_nat_nat @ p @ k @ (minus_minus_nat @ (p @ k) @ one_one_nat) @ A) @ A)) @ (set_ord_atMost_nat @ (minus_minus_nat @ n @ k))) = (minus_minus_nat @ (groups1842438620at_nat @ (^ [A:nat]: (times_times_nat @ (p @ A) @ A)) @ (set_ord_atMost_nat @ n)) @ k))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 13.71/3.48  thf(17,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (B != A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_214_less__imp__not__eq2)).
% 13.71/3.48  thf(287,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 13.71/3.48  thf(233,axiom,((! [A:nat]: ((times_times_nat @ A @ one_one_nat) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_53_mult_Oright__neutral)).
% 13.71/3.48  thf(1133,plain,((! [A:nat]: ((times_times_nat @ A @ one_one_nat) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 13.71/3.48  thf(102,axiom,((! [A:nat]: ((A != zero_zero_nat) = (ord_less_nat @ zero_zero_nat @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_193_bot__nat__0_Onot__eq__extremum)).
% 13.71/3.48  thf(620,plain,((! [A:nat]: ((~ (A = zero_zero_nat)) = (ord_less_nat @ zero_zero_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 13.71/3.48  thf(129,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_nat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_240_nat__less__induct)).
% 13.71/3.48  thf(752,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)],[129])).
% 13.71/3.48  thf(50,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) => ((A != B) => (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_212_linorder__cases)).
% 13.71/3.48  thf(447,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)],[50])).
% 13.71/3.48  thf(162,axiom,((! [A:nat]: ((times_times_nat @ one_one_nat @ A) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_38_nat__mult__1)).
% 13.71/3.48  thf(865,plain,((! [A:nat]: ((times_times_nat @ one_one_nat @ A) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 13.71/3.48  thf(38,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_219_dual__order_Oasym)).
% 13.71/3.48  thf(410,plain,((! [A:nat,B:nat]: ((ord_less_nat @ A @ B) => (~ (ord_less_nat @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 13.71/3.48  thf(190,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ zero_zero_nat @ A) => ((ord_less_eq_nat @ B @ zero_zero_nat) => (ord_less_eq_nat @ (times_times_nat @ A @ B) @ zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_106_mult__nonneg__nonpos)).
% 13.71/3.48  thf(967,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ zero_zero_nat @ A) => ((ord_less_eq_nat @ B @ zero_zero_nat) => (ord_less_eq_nat @ (times_times_nat @ A @ B) @ zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 13.71/3.48  thf(19,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/sandbox2/benchmark/theBenchmark.p',fact_22_Nat_Oex__has__greatest__nat)).
% 13.71/3.48  thf(294,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)],[19])).
% 13.71/3.48  thf(115,axiom,((! [A:nat,B:(set_nat > nat),C:set_nat,D:set_nat]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_eq_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_nat @ E @ F) => (ord_less_eq_nat @ (B @ E) @ (B @ F)))) => (ord_less_eq_nat @ A @ (B @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_165_order__subst1)).
% 13.71/3.48  thf(664,plain,((! [A:nat,B:(set_nat > nat),C:set_nat,D:set_nat]: ((ord_less_eq_nat @ A @ (B @ C)) => ((ord_less_eq_set_nat @ C @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_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)],[115])).
% 13.71/3.48  thf(79,axiom,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_98_le__0__eq)).
% 13.71/3.48  thf(532,plain,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 13.71/3.48  thf(120,axiom,((((?) @ nat) = (^ [A:(nat > $o)]: ? [B:nat]: ((A @ B) & ! [C:nat]: ((ord_less_nat @ C @ B) => (~ (A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_208_exists__least__iff)).
% 13.71/3.48  thf(696,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)],[120])).
% 13.71/3.48  thf(242,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ zero_zero_nat @ (minus_minus_nat @ A @ B)) = (ord_less_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_196_zero__less__diff)).
% 13.71/3.48  thf(1165,plain,((! [A:nat,B:nat]: ((ord_less_nat @ zero_zero_nat @ (minus_minus_nat @ A @ B)) = (ord_less_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 13.71/3.48  thf(140,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((minus_minus_nat @ A @ B) = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_82_diff__is__0__eq_H)).
% 13.71/3.48  thf(796,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => ((minus_minus_nat @ A @ B) = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 13.71/3.48  thf(166,axiom,((! [A:nat,B:nat]: ((one_one_nat = (times_times_nat @ A @ B)) = ((A = one_one_nat) & (B = one_one_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_16_nat__1__eq__mult__iff)).
% 13.71/3.48  thf(886,plain,((! [A:nat,B:nat]: ((one_one_nat = (times_times_nat @ A @ B)) = ((A = one_one_nat) & (B = one_one_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 13.71/3.48  thf(178,axiom,((number1551313001itions = (^ [A:(nat > nat),B:nat]: (! [C:nat]: (((A @ C) != zero_zero_nat) => ((ord_less_eq_nat @ one_one_nat @ C) & (ord_less_eq_nat @ C @ B))) & ((groups1842438620at_nat @ (^ [C:nat]: (times_times_nat @ (A @ C) @ C)) @ (set_ord_atMost_nat @ B)) = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_61_partitions__def)).
% 13.71/3.48  thf(928,plain,(((number1551313001itions) = (^ [A:(nat > nat),B:nat]: (! [C:nat]: ((~ ((A @ C) = zero_zero_nat)) => ((ord_less_eq_nat @ one_one_nat @ C) & (ord_less_eq_nat @ C @ B))) & ((groups1842438620at_nat @ (^ [C:nat]: (times_times_nat @ (A @ C) @ C)) @ (set_ord_atMost_nat @ B)) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 13.71/3.48  thf(40,axiom,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ C) => (ord_less_eq_set_nat @ A @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_130_order__trans)).
% 13.71/3.48  thf(415,plain,((! [A:set_nat,B:set_nat,C:set_nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_set_nat @ B @ C) => (ord_less_eq_set_nat @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 13.71/3.48  thf(238,axiom,((! [A:nat,B:nat]: ((ord_less_nat @ zero_zero_nat @ (times_times_nat @ A @ B)) = ((ord_less_nat @ zero_zero_nat @ A) & (ord_less_nat @ zero_zero_nat @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_199_nat__0__less__mult__iff)).
% 13.71/3.48  thf(1152,plain,((! [A:nat,B:nat]: ((ord_less_nat @ zero_zero_nat @ (times_times_nat @ A @ B)) = ((ord_less_nat @ zero_zero_nat @ A) & (ord_less_nat @ zero_zero_nat @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 13.71/3.48  thf(125,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_129_dual__order_Orefl)).
% 13.71/3.48  thf(723,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 13.71/3.48  thf(149,axiom,((! [A:nat,B:nat]: (((times_times_nat @ A @ B) != zero_zero_nat) => ((A != zero_zero_nat) & (B != zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_87_mult__not__zero)).
% 13.71/3.48  thf(822,plain,((! [A:nat,B:nat]: ((~ ((times_times_nat @ A @ B) = zero_zero_nat)) => (~ (A = zero_zero_nat) & ~ (B = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 13.71/3.48  thf(195,axiom,((! [A:(nat > (nat > nat)),B:set_nat,C:set_nat]: ((groups1842438620at_nat @ (^ [D:nat]: (groups1842438620at_nat @ (A @ D) @ B)) @ C) = (groups1842438620at_nat @ (^ [D:nat]: (groups1842438620at_nat @ (^ [E:nat]: (A @ E @ D)) @ C)) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_52_sum_Oswap)).
% 13.71/3.48  thf(982,plain,((! [A:(nat > (nat > nat)),B:set_nat,C:set_nat]: ((groups1842438620at_nat @ (^ [D:nat]: (groups1842438620at_nat @ (A @ D) @ B)) @ C) = (groups1842438620at_nat @ (^ [D:nat]: (groups1842438620at_nat @ (^ [E:nat]: (A @ E @ D)) @ C)) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 13.71/3.48  thf(15,axiom,((! [A:set_nat,B:set_nat,C:(set_nat > nat),D:nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_nat @ (C @ B) @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_nat @ E @ F) => (ord_less_eq_nat @ (C @ E) @ (C @ F)))) => (ord_less_eq_nat @ (C @ A) @ D)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_162_order__subst2)).
% 13.71/3.48  thf(277,plain,((! [A:set_nat,B:set_nat,C:(set_nat > nat),D:nat]: ((ord_less_eq_set_nat @ A @ B) => ((ord_less_eq_nat @ (C @ B) @ D) => ((! [E:set_nat,F:set_nat]: ((ord_less_eq_set_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)],[15])).
% 13.71/3.48  thf(35,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_nat @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_216_less__induct)).
% 13.71/3.48  thf(395,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)],[35])).
% 13.71/3.48  thf(154,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (times_times_nat @ A @ B) @ (times_times_nat @ A @ C)) = ((ord_less_nat @ zero_zero_nat @ A) => (ord_less_eq_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_201_nat__mult__le__cancel__disj)).
% 13.71/3.48  thf(839,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (times_times_nat @ A @ B) @ (times_times_nat @ A @ C)) = ((ord_less_nat @ zero_zero_nat @ A) => (ord_less_eq_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 13.71/3.48  thf(62,axiom,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) => (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_bot__nat__0_Oextremum__uniqueI)).
% 13.71/3.48  thf(486,plain,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) => (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 13.71/3.48  thf(56,axiom,((! [A:nat,B:nat]: ((~ (ord_less_nat @ A @ B)) = ((ord_less_nat @ B @ A) | (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_205_not__less__iff__gr__or__eq)).
% 13.71/3.48  thf(469,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)],[56])).
% 13.71/3.48  thf(29,axiom,((! [A:set_nat,B:set_nat]: ((member_set_nat @ A @ (set_or1086813439et_nat @ B)) = (ord_less_eq_set_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_12_atMost__iff)).
% 13.71/3.48  thf(354,plain,((! [A:set_nat,B:set_nat]: ((member_set_nat @ A @ (set_or1086813439et_nat @ B)) = (ord_less_eq_set_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 13.71/3.48  thf(204,axiom,((! [A:set_nat,B:set_nat,C:(nat > nat),D:(nat > nat),E:(nat > nat)]: ((! [F:nat]: ((member_nat @ F @ A) => (? [G:nat]: ((member_nat @ G @ B) & ((C @ G) = F) & ! [H:nat]: (((member_nat @ H @ B) & ((C @ H) = F)) => (H = G)))))) => ((! [F:nat]: ((member_nat @ F @ B) => ((member_nat @ (C @ F) @ A) & ((D @ (C @ F)) = (E @ F))))) => ((groups1842438620at_nat @ E @ B) = (groups1842438620at_nat @ D @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_49_sum_Oeq__general)).
% 13.71/3.48  thf(1009,plain,((! [A:set_nat,B:set_nat,C:(nat > nat),D:(nat > nat),E:(nat > nat)]: ((! [F:nat]: ((member_nat @ F @ A) => (? [G:nat]: ((member_nat @ G @ B) & ((C @ G) = F) & ! [H:nat]: (((member_nat @ H @ B) & ((C @ H) = F)) => (H = G)))))) => ((! [F:nat]: ((member_nat @ F @ B) => ((member_nat @ (C @ F) @ A) & ((D @ (C @ F)) = (E @ F))))) => ((groups1842438620at_nat @ (E) @ B) = (groups1842438620at_nat @ (D) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 13.71/3.48  thf(86,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((ord_less_eq_nat @ B @ A) & (ord_less_eq_nat @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_124_dual__order_Oeq__iff)).
% 13.71/3.48  thf(560,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)],[86])).
% 13.71/3.48  thf(220,axiom,((! [A:(nat > nat),B:set_nat,C:nat]: ((times_times_nat @ (groups1842438620at_nat @ A @ B) @ C) = (groups1842438620at_nat @ (^ [D:nat]: (times_times_nat @ (A @ D) @ C)) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_sum__distrib__right)).
% 13.71/3.48  thf(1088,plain,((! [A:(nat > nat),B:set_nat,C:nat]: ((times_times_nat @ (groups1842438620at_nat @ (A) @ B) @ C) = (groups1842438620at_nat @ (^ [D:nat]: (times_times_nat @ (A @ D) @ C)) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 13.71/3.48  thf(213,axiom,((number1551313001itions @ p @ n)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_partitions)).
% 13.71/3.48  thf(1069,plain,((number1551313001itions @ (p) @ n)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 13.71/3.48  thf(1201,plain,(($false)),inference(e,[status(thm)],[645,809,629,1168,1105,846,893,481,909,249,977,994,379,511,597,1041,523,1158,269,677,1078,550,472,698,945,1063,930,404,1127,782,565,436,651,257,785,802,357,853,421,1115,261,475,1109,376,623,253,514,1136,834,634,1072,774,988,428,849,527,877,692,452,942,529,546,925,761,381,334,957,1091,862,407,815,729,275,788,1032,329,889,461,493,842,522,830,324,974,519,874,948,1121,725,980,1006,1118,499,1082,339,933,537,669,642,637,489,970,1155,997,654,1060,721,569,779,1099,985,244,266,805,508,657,1035,674,773,794,586,906,412,618,264,856,573,819,423,743,1124,562,904,579,291,1139,466,445,936,764,567,271,477,631,535,609,594,483,1029,1149,626,1112,345,552,799,1162,912,1000,922,1066,868,267,1102,505,438,1076,589,255,648,812,516,939,342,1145,836,525,1025,1070,282,707,954,310,712,557,1003,791,331,441,502,463,1130,1085,576,951,808,600,386,497,859,991,450,903,581,891,963,319,896,418,246,433,832,287,1133,620,752,447,865,410,967,294,664,532,696,1165,796,886,928,415,1152,723,822,982,277,395,839,486,469,354,1009,560,1088,1069])).
% 13.71/3.48  % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.71/3.48  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------