%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP097^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 : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:06:45 AM UTC 2026
% Result : Theorem 15.22s 4.67s
% Output : Refutation 17.01s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP097^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.09/0.21 % Computer : n013.cluster.edu
% 0.09/0.21 % Model : x86_64 x86_64
% 0.09/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.21 % Memory : 8046.5625MB
% 0.09/0.21 % OS : Linux 6.8.0-71-generic
% 0.09/0.21 % CPULimit : 300
% 0.09/0.21 % WCLimit : 300
% 0.09/0.21 % DateTime : Tue Sep 29 19:52:36 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/0.21 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
% 1.24/0.91 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.85/1.43 % [INFO] Parsing done (512ms).
% 2.85/1.45 % [INFO] Running in sequential loop mode.
% 4.34/1.90 % [INFO] eprover registered as external prover.
% 4.34/1.91 % [INFO] Scanning for conjecture ...
% 4.68/2.07 % [INFO] Found a conjecture (or negated_conjecture) and 353 axioms. Running axiom selection ...
% 5.30/2.32 % [INFO] Axiom selection finished. Selected 348 axioms (removed 5 axioms).
% 6.17/2.69 % [INFO] Problem is higher-order (TPTP THF).
% 6.48/2.72 % [INFO] Type checking passed.
% 6.48/2.73 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 15.22/4.66 % External prover 'e' found a proof!
% 15.22/4.66 % [INFO] Killing All external provers ...
% 15.22/4.66 % Time passed: 4282ms (effective reasoning time: 3198ms)
% 15.22/4.66 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 15.22/4.67 % Axioms used in derivation (348): fact_257_nat__int, fact_222_order__refl, fact_294_zero__le__imp__eq__int, fact_125_of__nat__1__eq__iff, fact_309_int__ops_I2_J, fact_345_eq__nat__nat__iff, fact_179_le__antisym, fact_280_of__int__le__0__iff, fact_71_numeral__eq__one__iff, fact_288_zero__eq__power2, fact_37_nat__eq__numeral__power__cancel__iff, fact_123_of__nat__1__eq__iff, fact_156_real__of__nat__eq__numeral__power__cancel__iff, fact_271_nat__1, fact_246_of__int__0__eq__iff, fact_108_power2__nat__le__imp__le, fact_81_numeral__le__one__iff, fact_5_numeral__power__eq__of__int__cancel__iff, fact_83_complete__real, fact_342_int__ops_I3_J, fact_326_diff__induct, fact_27_of__int__le__iff, fact_180_eq__imp__le, fact_38_numeral__power__le__nat__cancel__iff, fact_146_of__nat__power, fact_320_nat_Odistinct_I1_J, fact_256_nat__power__eq__Suc__0__iff, fact_2_of__int__le__numeral__power__cancel__iff, fact_234_of__nat__0, fact_161_nat__ceiling__le__eq, fact_325_One__nat__def, fact_197_one__le__power, fact_316_power__not__zero, fact_287_zero__eq__power2, fact_99_verit__la__generic, fact_149_of__nat__power__le__of__nat__cancel__iff, fact_145_of__nat__power, fact_304_power__0__left, fact_214_one__power2, fact_135_of__nat__numeral, fact_279_of__int__le__0__iff, fact_42_le__of__int__ceiling, fact_259_dbl__simps_I2_J, fact_129_of__int__of__nat__eq, fact_130_of__int__of__nat__eq, fact_228_le0, fact_231_le__zero__eq, fact_340_nat__int__comparison_I3_J, fact_143_of__nat__eq__of__nat__power__cancel__iff, fact_46__092_060open_062log_A2_A1_A_092_060le_062_Alog_A2_A_Ireal__of__int_Ad_J_092_060close_062, fact_302_zero__le, fact_199_one__le__power, fact_236_of__nat__0__eq__iff, fact_333_not0__implies__Suc, fact_164_of__nat__le__numeral__power__cancel__iff, fact_232_of__nat__0, fact_190_not__less__eq__eq, fact_13_ceiling__le__numeral, fact_195_le__SucE, fact_202_lift__Suc__antimono__le, fact_339_le__nat__iff, fact_57_semiring__norm_I87_J, fact_111_power__one__right, fact_343_ex__nat, fact_155_real__of__nat__eq__numeral__power__cancel__iff, fact_281_ceiling__le__zero, fact_162_of__nat__le__numeral__power__cancel__iff, fact_258_dbl__simps_I2_J, fact_298_nat__eq__iff, fact_137_of__nat__numeral, fact_49_semiring__norm_I85_J, fact_299_zero__reorient, fact_260_of__nat__le__0__iff, fact_310_le__numeral__extra_I3_J, fact_244_of__int__0, fact_163_of__nat__le__numeral__power__cancel__iff, fact_0_numeral__power__le__of__int__cancel__iff, fact_181_le__trans, fact_332_old_Onat_Oinducts, fact_66_of__int__1, fact_213_one__power2, fact_262_of__nat__le__0__iff, fact_47_semiring__norm_I69_J, fact_40_nat__mono, fact_107_power2__nat__le__eq__le, fact_263_power__0__Suc, fact_82_numeral__le__one__iff, fact_17_of__int__numeral__le__iff, fact_219_power__numeral, fact_208_powr__mono, fact_154_real__of__nat__eq__numeral__power__cancel__iff, fact_84_le__numeral__extra_I4_J, fact_75_of__int__1__le__iff, fact_86_le__numeral__extra_I4_J, fact_184_powr__powr__swap, fact_170_of__nat__mono, fact_221_order__refl, fact_63_of__int__eq__1__iff, fact_255_power__Suc__0, fact_87_one__le__numeral, fact_275_dbl__simps_I5_J, fact_103__092_060open_0622_Apowr_Alog_A2_A_Ireal__of__int_Ad_J_A_092_060le_062_A2_Apowr_Areal_A_Inat_A_092_060lceil_062log_A2_A_Ireal__of__int_Ad_J_092_060rceil_062_J_092_060close_062, fact_92_numeral__One, fact_54_n__def, fact_25_ceiling__of__int, fact_53__092_060open_062real__of__int_Ad_A_061_A2_Apowr_Alog_A2_A_Ireal__of__int_Ad_J_092_060close_062, fact_311_le__numeral__extra_I3_J, fact_273_log__one, fact_11_of__int__power__le__of__int__cancel__iff, fact_330_Zero__not__Suc, fact_200_lift__Suc__antimono__le, fact_32_of__int__eq__numeral__iff, fact_113_nat_Oinject, fact_55_semiring__norm_I68_J, fact_201_lift__Suc__antimono__le, fact_73_one__eq__numeral__iff, fact_187_transitive__stepwise__le, fact_289_power2__less__eq__zero__iff, fact_238_of__nat__eq__0__iff, fact_141_of__nat__eq__of__nat__power__cancel__iff, fact_19_of__int__power, fact_192_le__Suc__eq, fact_115_of__nat__eq__iff, fact_301_zero__reorient, fact_319_exists__least__lemma, fact_152_of__nat__le__of__nat__power__cancel__iff, fact_20_of__int__eq__of__int__power__cancel__iff, fact_229_bot__nat__0_Oextremum, fact_203_lift__Suc__antimono__le, fact_78_of__int__le__1__iff, fact_85_le__numeral__extra_I4_J, fact_151_of__nat__le__of__nat__power__cancel__iff, fact_14_of__int__le__numeral__iff, fact_252_ceiling__zero, fact_296_int__int__eq, fact_100_verit__eq__simplify_I10_J, fact_76_of__int__1__le__iff, fact_205_lift__Suc__mono__le, fact_160_numeral__le__real__of__nat__iff, fact_158_numeral__power__eq__of__nat__cancel__iff, fact_28_of__int__le__iff, fact_277_of__int__0__le__iff, fact_303_nat__zero__as__int, fact_270_powr__nonneg__iff, fact_148_of__nat__power__le__of__nat__cancel__iff, fact_196_Suc__leD, fact_194_le__SucI, fact_126_of__nat__1, fact_274_int__nat__eq, fact_297_nat__eq__iff2, fact_134_of__nat__le__iff, fact_166_numeral__power__le__of__nat__cancel__iff, fact_313_zero__neq__numeral, fact_144_of__nat__power, fact_139_of__nat__power__eq__of__nat__cancel__iff, fact_218_power__numeral, fact_349_nat__le__iff, fact_282_powr__one, fact_245_of__int__0, fact_230_d_I2_J, fact_22_of__int__eq__iff, fact_307_nat__0__le, fact_171_of__nat__mono, fact_33_ceiling__numeral, fact_120_of__nat__eq__1__iff, fact_329_Zero__neq__Suc, fact_285_of__nat__nat, fact_48_semiring__norm_I83_J, fact_104_numeral__powr__numeral__real, fact_122_of__nat__eq__1__iff, fact_347_powr__ge__pzero, fact_131_ceiling__of__nat, fact_272_int__eq__iff__numeral, fact_110_power__one__right, fact_39_nat__le__numeral__power__cancel__iff, fact_305_power__0__left, fact_226_power2__eq__iff__nonneg, fact_306_power__0__left, fact_249_of__int__eq__0__iff, fact_317_power__not__zero, fact_167_numeral__power__le__of__nat__cancel__iff, fact_117_power__one, fact_215_dbl__simps_I3_J, fact_237_of__nat__0__eq__iff, fact_50_numeral__le__iff, fact_290_power2__less__eq__zero__iff, fact_7_of__int__eq__numeral__power__cancel__iff, fact_295_nonneg__int__cases, fact_106_self__le__ge2__pow, fact_276_dbl__simps_I5_J, fact_206_lift__Suc__mono__le, fact_250_powr__eq__0__iff, fact_109_Suc__le__mono, fact_136_of__nat__numeral, fact_116_of__nat__eq__iff, fact_1_numeral__power__le__of__int__cancel__iff, fact_334_bot__nat__0_Oextremum__uniqueI, fact_56_semiring__norm_I71_J, fact_186_le__log2__of__power, fact_124_of__nat__1__eq__iff, fact_300_zero__reorient, fact_225_power2__eq__iff__nonneg, fact_114_old_Onat_Oinject, fact_97_le__num__One__iff, fact_314_zero__neq__numeral, fact_210_power__increasing, fact_336_le__0__eq, fact_331_old_Onat_Oexhaust, fact_269_powr__zero__eq__one, fact_267_power__zero__numeral, fact_77_of__int__le__1__iff, fact_189_full__nat__induct, fact_29_of__int__numeral, fact_9_of__int__le__of__int__power__cancel__iff, fact_67_of__int__1, fact_62_of__int__eq__1__iff, fact_51_numeral__le__iff, fact_127_of__nat__1, fact_207_lift__Suc__mono__le, fact_24_nat__numeral, fact_293_int__ops_I1_J, fact_94_verit__la__disequality, fact_172_of__nat__mono, fact_35_of__int__power__eq__of__int__cancel__iff, fact_18_of__int__power, fact_212_one__power2, fact_72_one__eq__numeral__iff, fact_30_of__int__numeral, fact_248_of__int__eq__0__iff, fact_292_nat__int__comparison_I1_J, fact_90_numeral__One, fact_150_of__nat__power__le__of__nat__cancel__iff, fact_216_dbl__simps_I3_J, fact_185_log2__of__power__eq, fact_209_power__increasing, fact_335_bot__nat__0_Oextremum__unique, fact_264_power__0__Suc, fact_176_n__not__Suc__n, fact_183_real__nat__ceiling__ge, fact_165_numeral__power__le__of__nat__cancel__iff, fact_324_nat__induct, fact_140_of__nat__power__eq__of__nat__cancel__iff, fact_191_Suc__n__not__le__n, fact_61_numeral__eq__iff, fact_254_nat__0__iff, fact_211_power__increasing, fact_36_numeral__power__eq__nat__cancel__iff, fact_147_Suc__1, fact_344_all__nat, fact_204_lift__Suc__mono__le, fact_173_numerals_I1_J, fact_52_numeral__le__iff, fact_41_ex__le__of__int, fact_188_nat__induct__at__least, fact_247_of__int__0__eq__iff, fact_346_powr__mono2, fact_69_numeral__eq__one__iff, fact_118_power__one, fact_121_of__nat__eq__1__iff, fact_132_of__nat__le__iff, fact_174_of__nat__ceiling, fact_337_less__eq__nat_Osimps_I1_J, fact_10_of__int__le__of__int__power__cancel__iff, fact_15_of__int__le__numeral__iff, fact_138_of__nat__power__eq__of__nat__cancel__iff, fact_6_numeral__power__eq__of__int__cancel__iff, fact_182_le__refl, fact_227_power2__eq__iff__nonneg, fact_96_verit__la__disequality, fact_266_power__zero__numeral, fact_224_powr__numeral, fact_220_order__refl, fact_291_int__if, fact_45_ceiling__le, fact_59_numeral__eq__iff, fact_283_powr__one__gt__zero__iff, fact_3_of__int__le__numeral__power__cancel__iff, fact_268_power__zero__numeral, fact_79_ceiling__le__one, fact_261_of__nat__le__0__iff, fact_98_two__realpow__ge__one, fact_321_old_Onat_Odistinct_I2_J, fact_119_power__one, fact_8_of__int__eq__numeral__power__cancel__iff, fact_128_of__nat__1, fact_286_zero__eq__power2, fact_43_ceiling__mono, fact_265_power__0__Suc, fact_88_one__le__numeral, fact_168_nat__one__as__int, fact_239_of__nat__eq__0__iff, fact_23_of__int__eq__iff, fact_322_old_Onat_Odistinct_I1_J, fact_233_of__nat__0, fact_70_numeral__eq__one__iff, fact_217_power__numeral, fact_93_verit__la__disequality, fact_31_of__int__eq__numeral__iff, fact_89_one__le__numeral, fact_21_of__int__eq__of__int__power__cancel__iff, fact_169_real__arch__simple, fact_102__092_060open_0622_Apowr_Areal_A_Inat_A_092_060lceil_062log_A2_A_Ireal__of__int_Ad_J_092_060rceil_062_J_A_061_Areal__of__int_A_I2_A_094_Anat_A_092_060lceil_062log_A2_A_Ireal__of__int_Ad_J_092_060rceil_062_J_092_060close_062, fact_34_of__int__power__eq__of__int__cancel__iff, fact_91_numeral__One, fact_178_nat__le__linear, fact_308_int__eq__iff, fact_198_one__le__power, fact_327_zero__induct, fact_58_verit__eq__simplify_I8_J, fact_240_of__nat__eq__0__iff, fact_153_of__nat__le__of__nat__power__cancel__iff, fact_242_power__Suc0__right, fact_241_power__Suc0__right, fact_12_of__int__power__le__of__int__cancel__iff, fact_95_verit__la__disequality, fact_312_le__numeral__extra_I3_J, fact_101_nat__numeral__as__int, fact_159_numeral__power__eq__of__nat__cancel__iff, fact_348_pow_Osimps_I1_J, fact_157_numeral__power__eq__of__nat__cancel__iff, fact_105_powr__one__eq__one, fact_338_less__eq__int__code_I1_J, fact_315_zero__neq__numeral, fact_341_zle__int, fact_44_ceiling__le__iff, fact_323_nat_OdiscI, fact_4_ceiling__numeral__power, fact_318_power__not__zero, fact_16_of__int__numeral__le__iff, fact_235_of__nat__0__eq__iff, fact_26_of__int__ceiling__cancel, fact_328_Suc__neq__Zero, fact_284_of__nat__nat, fact_60_numeral__eq__iff, fact_68_ceiling__one, fact_142_of__nat__eq__of__nat__power__cancel__iff, fact_243_power__Suc0__right, fact_112_power__one__right, fact_223_order__refl, fact_251_powr__0, fact_253_nat__le__0, fact_80_numeral__le__one__iff, fact_278_of__int__0__le__iff, fact_74_one__eq__numeral__iff, fact_177_Nat_Oex__has__greatest__nat, fact_175_Suc__inject, fact_133_of__nat__le__iff, fact_193_Suc__le__D
% 15.22/4.67 % No. of inferences in proof: 700
% 15.22/4.67 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 4282 ms resp. 3198 ms w/o parsing
% 17.01/5.05 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.01/5.05 thf(set_real_type, type, set_real: $tType).
% 17.01/5.05 thf(real_type, type, real: $tType).
% 17.01/5.05 thf(num_type, type, num: $tType).
% 17.01/5.05 thf(nat_type, type, nat: $tType).
% 17.01/5.05 thf(int_type, type, int: $tType).
% 17.01/5.05 thf(archim1371465213g_real_decl, type, archim1371465213g_real: (real > int)).
% 17.01/5.05 thf(one_one_int_decl, type, one_one_int: int).
% 17.01/5.05 thf(one_one_nat_decl, type, one_one_nat: nat).
% 17.01/5.05 thf(one_one_real_decl, type, one_one_real: real).
% 17.01/5.05 thf(zero_zero_int_decl, type, zero_zero_int: int).
% 17.01/5.05 thf(zero_zero_nat_decl, type, zero_zero_nat: nat).
% 17.01/5.05 thf(zero_zero_real_decl, type, zero_zero_real: real).
% 17.01/5.05 thf(if_nat_decl, type, if_nat: ($o > (nat > (nat > nat)))).
% 17.01/5.05 thf(nat2_decl, type, nat2: (int > nat)).
% 17.01/5.05 thf(ring_1_of_int_int_decl, type, ring_1_of_int_int: (int > int)).
% 17.01/5.05 thf(ring_1_of_int_real_decl, type, ring_1_of_int_real: (int > real)).
% 17.01/5.05 thf(suc_decl, type, suc: (nat > nat)).
% 17.01/5.05 thf(semiri2019852685at_int_decl, type, semiri2019852685at_int: (nat > int)).
% 17.01/5.05 thf(semiri1382578993at_nat_decl, type, semiri1382578993at_nat: (nat > nat)).
% 17.01/5.05 thf(semiri2110766477t_real_decl, type, semiri2110766477t_real: (nat > real)).
% 17.01/5.05 thf(neg_numeral_dbl_int_decl, type, neg_numeral_dbl_int: (int > int)).
% 17.01/5.05 thf(neg_numeral_dbl_real_decl, type, neg_numeral_dbl_real: (real > real)).
% 17.01/5.05 thf(bit0_decl, type, bit0: (num > num)).
% 17.01/5.05 thf(one_decl, type, one: num).
% 17.01/5.05 thf(numeral_numeral_int_decl, type, numeral_numeral_int: (num > int)).
% 17.01/5.05 thf(numeral_numeral_nat_decl, type, numeral_numeral_nat: (num > nat)).
% 17.01/5.05 thf(numeral_numeral_real_decl, type, numeral_numeral_real: (num > real)).
% 17.01/5.05 thf(pow_decl, type, pow: (num > (num > num))).
% 17.01/5.05 thf(ord_less_int_decl, type, ord_less_int: (int > (int > $o))).
% 17.01/5.05 thf(ord_less_eq_int_decl, type, ord_less_eq_int: (int > (int > $o))).
% 17.01/5.05 thf(ord_less_eq_nat_decl, type, ord_less_eq_nat: (nat > (nat > $o))).
% 17.01/5.05 thf(ord_less_eq_num_decl, type, ord_less_eq_num: (num > (num > $o))).
% 17.01/5.05 thf(ord_less_eq_real_decl, type, ord_less_eq_real: (real > (real > $o))).
% 17.01/5.05 thf(power_power_int_decl, type, power_power_int: (int > (nat > int))).
% 17.01/5.05 thf(power_power_nat_decl, type, power_power_nat: (nat > (nat > nat))).
% 17.01/5.05 thf(power_power_real_decl, type, power_power_real: (real > (nat > real))).
% 17.01/5.05 thf(log_decl, type, log: (real > (real > real))).
% 17.01/5.05 thf(powr_real_decl, type, powr_real: (real > (real > real))).
% 17.01/5.05 thf(member_real_decl, type, member_real: (real > (set_real > $o))).
% 17.01/5.05 thf(d_decl, type, d: int).
% 17.01/5.05 thf(n_decl, type, n: nat).
% 17.01/5.05 thf(203,axiom,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) => (ord_less_eq_nat @ (nat2 @ A) @ (nat2 @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_40_nat__mono)).
% 17.01/5.05 thf(1036,plain,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) => (ord_less_eq_nat @ (nat2 @ A) @ (nat2 @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 17.01/5.05 thf(135,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ one_one_nat @ A) => (ord_less_eq_nat @ one_one_nat @ (power_power_nat @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_198_one__le__power)).
% 17.01/5.05 thf(809,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ one_one_nat @ A) => (ord_less_eq_nat @ one_one_nat @ (power_power_nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 17.01/5.05 thf(199,axiom,((! [A:int,B:nat]: ((ring_1_of_int_real @ (power_power_int @ A @ B)) = (power_power_real @ (ring_1_of_int_real @ A) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_19_of__int__power)).
% 17.01/5.05 thf(1024,plain,((! [A:int,B:nat]: ((ring_1_of_int_real @ (power_power_int @ A @ B)) = (power_power_real @ (ring_1_of_int_real @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 17.01/5.05 thf(119,axiom,((! [A:int]: (((ring_1_of_int_int @ A) = one_one_int) = (A = one_one_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_63_of__int__eq__1__iff)).
% 17.01/5.05 thf(760,plain,((! [A:int]: (((ring_1_of_int_int @ A) = one_one_int) = (A = one_one_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 17.01/5.05 thf(350,axiom,((ord_less_int @ zero_zero_int @ d)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_230_d_I2_J)).
% 17.01/5.05 thf(1454,plain,((ord_less_int @ zero_zero_int @ d)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[350])).
% 17.01/5.05 thf(83,axiom,((! [A:num,B:num]: (((numeral_numeral_nat @ A) = (numeral_numeral_nat @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_61_numeral__eq__iff)).
% 17.01/5.05 thf(628,plain,((! [A:num,B:num]: (((numeral_numeral_nat @ A) = (numeral_numeral_nat @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 17.01/5.05 thf(172,axiom,((! [A:nat,B:nat]: ((A = (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ B)) => ((semiri2110766477t_real @ B) = (log @ (numeral_numeral_real @ (bit0 @ one)) @ (semiri2110766477t_real @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_185_log2__of__power__eq)).
% 17.01/5.05 thf(941,plain,((! [A:nat,B:nat]: ((A = (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ B)) => ((semiri2110766477t_real @ B) = (log @ (numeral_numeral_real @ (bit0 @ one)) @ (semiri2110766477t_real @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 17.01/5.05 thf(256,axiom,((! [A:num,B:nat,C:nat]: ((ord_less_eq_real @ (power_power_real @ (numeral_numeral_real @ A) @ B) @ (semiri2110766477t_real @ C)) = (ord_less_eq_nat @ (power_power_nat @ (numeral_numeral_nat @ A) @ B) @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_167_numeral__power__le__of__nat__cancel__iff)).
% 17.01/5.05 thf(1179,plain,((! [A:num,B:nat,C:nat]: ((ord_less_eq_real @ (power_power_real @ (numeral_numeral_real @ A) @ B) @ (semiri2110766477t_real @ C)) = (ord_less_eq_nat @ (power_power_nat @ (numeral_numeral_nat @ A) @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 17.01/5.05 thf(125,axiom,((! [A:nat]: (((semiri2110766477t_real @ A) = zero_zero_real) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_239_of__nat__eq__0__iff)).
% 17.01/5.05 thf(777,plain,((! [A:nat]: (((semiri2110766477t_real @ A) = zero_zero_real) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 17.01/5.05 thf(3,axiom,(((semiri1382578993at_nat @ zero_zero_nat) = zero_zero_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_232_of__nat__0)).
% 17.01/5.05 thf(352,plain,(((semiri1382578993at_nat @ zero_zero_nat) = zero_zero_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 17.01/5.05 thf(320,axiom,((! [A:int]: ((ord_less_eq_real @ (ring_1_of_int_real @ A) @ one_one_real) = (ord_less_eq_int @ A @ one_one_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_78_of__int__le__1__iff)).
% 17.01/5.05 thf(1369,plain,((! [A:int]: ((ord_less_eq_real @ (ring_1_of_int_real @ A) @ one_one_real) = (ord_less_eq_int @ A @ one_one_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[320])).
% 17.01/5.05 thf(260,axiom,((! [A:num,B:nat,C:nat]: (((power_power_int @ (numeral_numeral_int @ A) @ B) = (semiri2019852685at_int @ C)) = ((power_power_nat @ (numeral_numeral_nat @ A) @ B) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_159_numeral__power__eq__of__nat__cancel__iff)).
% 17.01/5.05 thf(1190,plain,((! [A:num,B:nat,C:nat]: (((power_power_int @ (numeral_numeral_int @ A) @ B) = (semiri2019852685at_int @ C)) = ((power_power_nat @ (numeral_numeral_nat @ A) @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 17.01/5.05 thf(192,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (power_power_nat @ A @ (numeral_numeral_nat @ (bit0 @ one))) @ B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_108_power2__nat__le__imp__le)).
% 17.01/5.05 thf(1005,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (power_power_nat @ A @ (numeral_numeral_nat @ (bit0 @ one))) @ B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 17.01/5.05 thf(216,axiom,((ord_less_eq_nat = (^ [A:nat,B:nat]: (ord_less_eq_int @ (semiri2019852685at_int @ A) @ (semiri2019852685at_int @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_340_nat__int__comparison_I3_J)).
% 17.01/5.05 thf(1068,plain,(((ord_less_eq_nat) = (^ [A:nat,B:nat]: (ord_less_eq_int @ (semiri2019852685at_int @ A) @ (semiri2019852685at_int @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 17.01/5.05 thf(346,axiom,((! [A:int,B:int,C:nat]: (((ring_1_of_int_int @ A) = (power_power_int @ (ring_1_of_int_int @ B) @ C)) = (A = (power_power_int @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_34_of__int__power__eq__of__int__cancel__iff)).
% 17.01/5.05 thf(1443,plain,((! [A:int,B:int,C:nat]: (((ring_1_of_int_int @ A) = (power_power_int @ (ring_1_of_int_int @ B) @ C)) = (A = (power_power_int @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[346])).
% 17.01/5.05 thf(188,axiom,((! [A:num,B:num]: ((powr_real @ (numeral_numeral_real @ A) @ (numeral_numeral_real @ B)) = (power_power_real @ (numeral_numeral_real @ A) @ (numeral_numeral_nat @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_104_numeral__powr__numeral__real)).
% 17.01/5.05 thf(994,plain,((! [A:num,B:num]: ((powr_real @ (numeral_numeral_real @ A) @ (numeral_numeral_real @ B)) = (power_power_real @ (numeral_numeral_real @ A) @ (numeral_numeral_nat @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 17.01/5.05 thf(331,axiom,((! [A:real]: ((ord_less_eq_int @ (archim1371465213g_real @ A) @ one_one_int) = (ord_less_eq_real @ A @ one_one_real)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_79_ceiling__le__one)).
% 17.01/5.05 thf(1401,plain,((! [A:real]: ((ord_less_eq_int @ (archim1371465213g_real @ A) @ one_one_int) = (ord_less_eq_real @ A @ one_one_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[331])).
% 17.01/5.05 thf(218,axiom,((! [A:nat,B:nat,C:nat]: (((power_power_int @ (semiri2019852685at_int @ A) @ B) = (semiri2019852685at_int @ C)) = ((power_power_nat @ A @ B) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_143_of__nat__eq__of__nat__power__cancel__iff)).
% 17.01/5.05 thf(1073,plain,((! [A:nat,B:nat,C:nat]: (((power_power_int @ (semiri2019852685at_int @ A) @ B) = (semiri2019852685at_int @ C)) = ((power_power_nat @ A @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 17.01/5.05 thf(45,axiom,((! [A:nat]: (((semiri2019852685at_int @ A) = one_one_int) = (A = one_one_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_122_of__nat__eq__1__iff)).
% 17.01/5.05 thf(511,plain,((! [A:nat]: (((semiri2019852685at_int @ A) = one_one_int) = (A = one_one_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 17.01/5.05 thf(343,axiom,(((numeral_numeral_real @ one) = one_one_real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_91_numeral__One)).
% 17.01/5.05 thf(1437,plain,(((numeral_numeral_real @ one) = one_one_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[343])).
% 17.01/5.05 thf(205,axiom,((ord_less_eq_int @ zero_zero_int @ zero_zero_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_310_le__numeral__extra_I3_J)).
% 17.01/5.05 thf(1041,plain,((ord_less_eq_int @ zero_zero_int @ zero_zero_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 17.01/5.05 thf(254,axiom,((! [A:(nat > int),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_int @ (A @ (suc @ D)) @ (A @ D))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_int @ (A @ C) @ (A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_200_lift__Suc__antimono__le)).
% 17.01/5.05 thf(1173,plain,((! [A:(nat > int),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_int @ (A @ (suc @ D)) @ (A @ D))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_int @ (A @ C) @ (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 17.01/5.05 thf(21,axiom,((! [A:(nat > num),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_num @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_num @ (A @ B) @ (A @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_207_lift__Suc__mono__le)).
% 17.01/5.05 thf(408,plain,((! [A:(nat > num),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_num @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_num @ (A @ B) @ (A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 17.01/5.05 thf(182,axiom,((! [A:real]: ? [B:int]: (ord_less_eq_real @ A @ (ring_1_of_int_real @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_41_ex__le__of__int)).
% 17.01/5.05 thf(977,plain,((! [A:real]: ? [B:int]: (ord_less_eq_real @ A @ (ring_1_of_int_real @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 17.01/5.05 thf(47,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ A @ (suc @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_194_le__SucI)).
% 17.01/5.05 thf(523,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ A @ (suc @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 17.01/5.05 thf(67,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_real @ (power_power_real @ (semiri2110766477t_real @ A) @ B) @ (semiri2110766477t_real @ C)) = (ord_less_eq_nat @ (power_power_nat @ A @ B) @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_153_of__nat__le__of__nat__power__cancel__iff)).
% 17.01/5.05 thf(582,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_real @ (power_power_real @ (semiri2110766477t_real @ A) @ B) @ (semiri2110766477t_real @ C)) = (ord_less_eq_nat @ (power_power_nat @ A @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 17.01/5.05 thf(111,axiom,((! [A:real,B:real]: (ord_less_eq_real @ zero_zero_real @ (powr_real @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_347_powr__ge__pzero)).
% 17.01/5.05 thf(730,plain,((! [A:real,B:real]: (ord_less_eq_real @ zero_zero_real @ (powr_real @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 17.01/5.05 thf(294,axiom,(((archim1371465213g_real @ zero_zero_real) = zero_zero_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_252_ceiling__zero)).
% 17.01/5.05 thf(1290,plain,(((archim1371465213g_real @ zero_zero_real) = zero_zero_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[294])).
% 17.01/5.05 thf(152,axiom,((! [A:nat,B:nat]: ((semiri2110766477t_real @ (power_power_nat @ A @ B)) = (power_power_real @ (semiri2110766477t_real @ A) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_145_of__nat__power)).
% 17.01/5.05 thf(873,plain,((! [A:nat,B:nat]: ((semiri2110766477t_real @ (power_power_nat @ A @ B)) = (power_power_real @ (semiri2110766477t_real @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 17.01/5.05 thf(30,axiom,((! [A:nat]: ((A != zero_zero_nat) => (~ (! [B:nat]: (A != (suc @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_331_old_Onat_Oexhaust)).
% 17.01/5.05 thf(449,plain,((! [A:nat]: ((~ (A = zero_zero_nat)) => (~ (! [B:nat]: ~ (A = (suc @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 17.01/5.05 thf(220,axiom,((! [A:num]: ((bit0 @ A) != one))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_49_semiring__norm_I85_J)).
% 17.01/5.05 thf(1078,plain,((! [A:num]: ~ ((bit0 @ A) = one))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 17.01/5.05 thf(15,axiom,((! [A:int]: ((zero_zero_int = (ring_1_of_int_int @ A)) = (A = zero_zero_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_247_of__int__0__eq__iff)).
% 17.01/5.05 thf(385,plain,((! [A:int]: ((zero_zero_int = (ring_1_of_int_int @ A)) = (A = zero_zero_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 17.01/5.05 thf(51,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (suc @ A) @ B) => (? [C:nat]: (B = (suc @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_193_Suc__le__D)).
% 17.01/5.05 thf(533,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (suc @ A) @ B) => (? [C:nat]: (B = (suc @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 17.01/5.05 thf(56,axiom,((! [A:nat,B:num,C:nat]: (((semiri1382578993at_nat @ A) = (power_power_nat @ (numeral_numeral_nat @ B) @ C)) = (A = (power_power_nat @ (numeral_numeral_nat @ B) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_154_real__of__nat__eq__numeral__power__cancel__iff)).
% 17.01/5.05 thf(550,plain,((! [A:nat,B:num,C:nat]: (((semiri1382578993at_nat @ A) = (power_power_nat @ (numeral_numeral_nat @ B) @ C)) = (A = (power_power_nat @ (numeral_numeral_nat @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 17.01/5.05 thf(275,axiom,((! [A:num,B:num]: ((power_power_int @ (numeral_numeral_int @ A) @ (numeral_numeral_nat @ B)) = (numeral_numeral_int @ (pow @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_217_power__numeral)).
% 17.01/5.05 thf(1233,plain,((! [A:num,B:num]: ((power_power_int @ (numeral_numeral_int @ A) @ (numeral_numeral_nat @ B)) = (numeral_numeral_int @ (pow @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[275])).
% 17.01/5.05 thf(305,axiom,((! [A:num,B:num]: (((bit0 @ A) = (bit0 @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_58_verit__eq__simplify_I8_J)).
% 17.01/5.05 thf(1327,plain,((! [A:num,B:num]: (((bit0 @ A) = (bit0 @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[305])).
% 17.01/5.05 thf(173,axiom,((! [A:int]: ((power_power_int @ A @ one_one_nat) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_110_power__one__right)).
% 17.01/5.05 thf(945,plain,((! [A:int]: ((power_power_int @ A @ one_one_nat) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 17.01/5.05 thf(310,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ A) => (ord_less_eq_nat @ B @ (power_power_nat @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_106_self__le__ge2__pow)).
% 17.01/5.05 thf(1342,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ A) => (ord_less_eq_nat @ B @ (power_power_nat @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[310])).
% 17.01/5.05 thf(162,axiom,((! [A:num,B:nat]: ((archim1371465213g_real @ (power_power_real @ (numeral_numeral_real @ A) @ B)) = (power_power_int @ (numeral_numeral_int @ A) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_ceiling__numeral__power)).
% 17.01/5.05 thf(913,plain,((! [A:num,B:nat]: ((archim1371465213g_real @ (power_power_real @ (numeral_numeral_real @ A) @ B)) = (power_power_int @ (numeral_numeral_int @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 17.01/5.05 thf(226,axiom,((! [A:real]: (ord_less_eq_real @ A @ (semiri2110766477t_real @ (nat2 @ (archim1371465213g_real @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_174_of__nat__ceiling)).
% 17.01/5.05 thf(1095,plain,((! [A:real]: (ord_less_eq_real @ A @ (semiri2110766477t_real @ (nat2 @ (archim1371465213g_real @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 17.01/5.05 thf(262,axiom,((! [A:int]: (((ring_1_of_int_real @ A) = zero_zero_real) = (A = zero_zero_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_248_of__int__eq__0__iff)).
% 17.01/5.05 thf(1196,plain,((! [A:int]: (((ring_1_of_int_real @ A) = zero_zero_real) = (A = zero_zero_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 17.01/5.05 thf(105,axiom,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_336_le__0__eq)).
% 17.01/5.05 thf(709,plain,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 17.01/5.05 thf(24,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ (suc @ B)) => ((~ (ord_less_eq_nat @ A @ B)) => (A = (suc @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_195_le__SucE)).
% 17.01/5.06 thf(417,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ (suc @ B)) => ((~ (ord_less_eq_nat @ A @ B)) => (A = (suc @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 17.01/5.06 thf(208,axiom,((! [A:int]: ((ord_less_eq_int @ one_one_int @ (ring_1_of_int_int @ A)) = (ord_less_eq_int @ one_one_int @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_75_of__int__1__le__iff)).
% 17.01/5.06 thf(1046,plain,((! [A:int]: ((ord_less_eq_int @ one_one_int @ (ring_1_of_int_int @ A)) = (ord_less_eq_int @ one_one_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 17.01/5.06 thf(316,axiom,((! [A:(nat > int),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_int @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_int @ (A @ B) @ (A @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_204_lift__Suc__mono__le)).
% 17.01/5.06 thf(1359,plain,((! [A:(nat > int),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_int @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_int @ (A @ B) @ (A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[316])).
% 17.01/5.06 thf(28,axiom,((! [A:(nat > $o)]: ((~ (A @ zero_zero_nat)) => ((? [B:nat]: (A @ B)) => (? [B:nat]: (~ (A @ B) & (A @ (suc @ B)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_319_exists__least__lemma)).
% 17.01/5.06 thf(436,plain,((! [A:(nat > $o)]: ((~ (A @ zero_zero_nat)) => ((? [B:nat]: (A @ B)) => (? [B:nat]: (~ (A @ B) & (A @ (suc @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 17.01/5.06 thf(286,axiom,((! [A:int,B:num]: (((ring_1_of_int_real @ A) = (numeral_numeral_real @ B)) = (A = (numeral_numeral_int @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_32_of__int__eq__numeral__iff)).
% 17.01/5.06 thf(1265,plain,((! [A:int,B:num]: (((ring_1_of_int_real @ A) = (numeral_numeral_real @ B)) = (A = (numeral_numeral_int @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[286])).
% 17.01/5.06 thf(61,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_114_old_Onat_Oinject)).
% 17.01/5.06 thf(565,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 17.01/5.06 thf(319,axiom,((! [A:int,B:nat]: ((ring_1_of_int_int @ (power_power_int @ A @ B)) = (power_power_int @ (ring_1_of_int_int @ A) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_of__int__power)).
% 17.01/5.06 thf(1366,plain,((! [A:int,B:nat]: ((ring_1_of_int_int @ (power_power_int @ A @ B)) = (power_power_int @ (ring_1_of_int_int @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[319])).
% 17.01/5.06 thf(273,axiom,(((numeral_numeral_nat @ one) = one_one_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_173_numerals_I1_J)).
% 17.01/5.06 thf(1228,plain,(((numeral_numeral_nat @ one) = one_one_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[273])).
% 17.01/5.06 thf(282,axiom,(((ring_1_of_int_real @ zero_zero_int) = zero_zero_real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_244_of__int__0)).
% 17.01/5.06 thf(1254,plain,(((ring_1_of_int_real @ zero_zero_int) = zero_zero_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 17.01/5.06 thf(211,axiom,((! [A:num,B:nat,C:int]: (((power_power_real @ (numeral_numeral_real @ A) @ B) = (ring_1_of_int_real @ C)) = ((power_power_int @ (numeral_numeral_int @ A) @ B) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_numeral__power__eq__of__int__cancel__iff)).
% 17.01/5.06 thf(1055,plain,((! [A:num,B:nat,C:int]: (((power_power_real @ (numeral_numeral_real @ A) @ B) = (ring_1_of_int_real @ C)) = ((power_power_int @ (numeral_numeral_int @ A) @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 17.01/5.06 thf(293,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_int @ (semiri2019852685at_int @ A) @ (power_power_int @ (semiri2019852685at_int @ B) @ C)) = (ord_less_eq_nat @ A @ (power_power_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_148_of__nat__power__le__of__nat__cancel__iff)).
% 17.01/5.06 thf(1287,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_int @ (semiri2019852685at_int @ A) @ (power_power_int @ (semiri2019852685at_int @ B) @ C)) = (ord_less_eq_nat @ A @ (power_power_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[293])).
% 17.01/5.06 thf(341,axiom,((! [A:num]: (zero_zero_int != (numeral_numeral_int @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_313_zero__neq__numeral)).
% 17.01/5.06 thf(1430,plain,((! [A:num]: ~ (zero_zero_int = (numeral_numeral_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[341])).
% 17.01/5.06 thf(10,axiom,(((semiri1382578993at_nat @ one_one_nat) = one_one_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_126_of__nat__1)).
% 17.01/5.06 thf(372,plain,(((semiri1382578993at_nat @ one_one_nat) = one_one_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 17.01/5.06 thf(306,axiom,((! [A:int,B:num,C:nat]: ((ord_less_eq_real @ (ring_1_of_int_real @ A) @ (power_power_real @ (numeral_numeral_real @ B) @ C)) = (ord_less_eq_int @ A @ (power_power_int @ (numeral_numeral_int @ B) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_of__int__le__numeral__power__cancel__iff)).
% 17.01/5.06 thf(1330,plain,((! [A:int,B:num,C:nat]: ((ord_less_eq_real @ (ring_1_of_int_real @ A) @ (power_power_real @ (numeral_numeral_real @ B) @ C)) = (ord_less_eq_int @ A @ (power_power_int @ (numeral_numeral_int @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[306])).
% 17.01/5.06 thf(103,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ (powr_real @ A @ B) @ zero_zero_real) = (A = zero_zero_real)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_270_powr__nonneg__iff)).
% 17.01/5.06 thf(702,plain,((! [A:real,B:real]: ((ord_less_eq_real @ (powr_real @ A @ B) @ zero_zero_real) = (A = zero_zero_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 17.01/5.06 thf(5,axiom,((! [A:nat,B:nat]: ((semiri1382578993at_nat @ (power_power_nat @ A @ B)) = (power_power_nat @ (semiri1382578993at_nat @ A) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_144_of__nat__power)).
% 17.01/5.06 thf(357,plain,((! [A:nat,B:nat]: ((semiri1382578993at_nat @ (power_power_nat @ A @ B)) = (power_power_nat @ (semiri1382578993at_nat @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 17.01/5.06 thf(69,axiom,((! [A:nat,B:nat]: (((semiri2019852685at_int @ A) = (semiri2019852685at_int @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_116_of__nat__eq__iff)).
% 17.01/5.06 thf(587,plain,((! [A:nat,B:nat]: (((semiri2019852685at_int @ A) = (semiri2019852685at_int @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 17.01/5.06 thf(80,axiom,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) = (ord_less_eq_nat @ (suc @ B) @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_190_not__less__eq__eq)).
% 17.01/5.06 thf(619,plain,((! [A:nat,B:nat]: ((~ (ord_less_eq_nat @ A @ B)) = (ord_less_eq_nat @ (suc @ B) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 17.01/5.06 thf(158,axiom,((! [A:real]: ((powr_real @ one_one_real @ A) = one_one_real))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_105_powr__one__eq__one)).
% 17.01/5.06 thf(902,plain,((! [A:real]: ((powr_real @ one_one_real @ A) = one_one_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 17.01/5.06 thf(59,axiom,((! [A:nat,B:nat]: ((ord_less_eq_real @ (semiri2110766477t_real @ A) @ (semiri2110766477t_real @ B)) = (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_134_of__nat__le__iff)).
% 17.01/5.06 thf(559,plain,((! [A:nat,B:nat]: ((ord_less_eq_real @ (semiri2110766477t_real @ A) @ (semiri2110766477t_real @ B)) = (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 17.01/5.06 thf(245,axiom,((! [A:nat,B:nat,C:int]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_int @ one_one_int @ C) => (ord_less_eq_int @ (power_power_int @ C @ A) @ (power_power_int @ C @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_209_power__increasing)).
% 17.01/5.06 thf(1147,plain,((! [A:nat,B:nat,C:int]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_int @ one_one_int @ C) => (ord_less_eq_int @ (power_power_int @ C @ A) @ (power_power_int @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 17.01/5.06 thf(304,axiom,((! [A:int]: (((ord_less_eq_int @ zero_zero_int @ A) => ((semiri2019852685at_int @ (nat2 @ A)) = A)) & ((~ (ord_less_eq_int @ zero_zero_int @ A)) => ((semiri2019852685at_int @ (nat2 @ A)) = zero_zero_int))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_274_int__nat__eq)).
% 17.01/5.06 thf(1319,plain,((! [A:int]: (((ord_less_eq_int @ zero_zero_int @ A) => ((semiri2019852685at_int @ (nat2 @ A)) = A)) & ((~ (ord_less_eq_int @ zero_zero_int @ A)) => ((semiri2019852685at_int @ (nat2 @ A)) = zero_zero_int))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[304])).
% 17.01/5.06 thf(179,axiom,((! [A:num]: ((semiri2019852685at_int @ (numeral_numeral_nat @ A)) = (numeral_numeral_int @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_342_int__ops_I3_J)).
% 17.01/5.06 thf(969,plain,((! [A:num]: ((semiri2019852685at_int @ (numeral_numeral_nat @ A)) = (numeral_numeral_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 17.01/5.06 thf(195,axiom,((! [A:num,B:int]: ((ord_less_eq_int @ (numeral_numeral_int @ A) @ (ring_1_of_int_int @ B)) = (ord_less_eq_int @ (numeral_numeral_int @ A) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_16_of__int__numeral__le__iff)).
% 17.01/5.06 thf(1013,plain,((! [A:num,B:int]: ((ord_less_eq_int @ (numeral_numeral_int @ A) @ (ring_1_of_int_int @ B)) = (ord_less_eq_int @ (numeral_numeral_int @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 17.01/5.06 thf(317,axiom,(((ring_1_of_int_real @ one_one_int) = one_one_real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_66_of__int__1)).
% 17.01/5.06 thf(1362,plain,(((ring_1_of_int_real @ one_one_int) = one_one_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[317])).
% 17.01/5.06 thf(228,axiom,((! [A:nat,B:nat]: ((ord_less_eq_int @ (semiri2019852685at_int @ A) @ (semiri2019852685at_int @ B)) = (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_341_zle__int)).
% 17.01/5.06 thf(1100,plain,((! [A:nat,B:nat]: ((ord_less_eq_int @ (semiri2019852685at_int @ A) @ (semiri2019852685at_int @ B)) = (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 17.01/5.06 thf(330,axiom,((! [A:num]: ((ord_less_eq_nat @ (numeral_numeral_nat @ A) @ one_one_nat) = (ord_less_eq_num @ A @ one)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_81_numeral__le__one__iff)).
% 17.01/5.06 thf(1398,plain,((! [A:num]: ((ord_less_eq_nat @ (numeral_numeral_nat @ A) @ one_one_nat) = (ord_less_eq_num @ A @ one)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[330])).
% 17.01/5.06 thf(155,axiom,((! [A:nat,B:num,C:nat]: ((ord_less_eq_nat @ (semiri1382578993at_nat @ A) @ (power_power_nat @ (numeral_numeral_nat @ B) @ C)) = (ord_less_eq_nat @ A @ (power_power_nat @ (numeral_numeral_nat @ B) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_163_of__nat__le__numeral__power__cancel__iff)).
% 17.01/5.06 thf(881,plain,((! [A:nat,B:num,C:nat]: ((ord_less_eq_nat @ (semiri1382578993at_nat @ A) @ (power_power_nat @ (numeral_numeral_nat @ B) @ C)) = (ord_less_eq_nat @ A @ (power_power_nat @ (numeral_numeral_nat @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 17.01/5.06 thf(336,axiom,((! [A:int,B:int,C:nat]: (((ring_1_of_int_real @ A) = (power_power_real @ (ring_1_of_int_real @ B) @ C)) = (A = (power_power_int @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_35_of__int__power__eq__of__int__cancel__iff)).
% 17.01/5.06 thf(1415,plain,((! [A:int,B:int,C:nat]: (((ring_1_of_int_real @ A) = (power_power_real @ (ring_1_of_int_real @ B) @ C)) = (A = (power_power_int @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[336])).
% 17.01/5.06 thf(166,axiom,((! [A:int]: (((power_power_int @ A @ (numeral_numeral_nat @ (bit0 @ one))) = zero_zero_int) = (A = zero_zero_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_286_zero__eq__power2)).
% 17.01/5.06 thf(924,plain,((! [A:int]: (((power_power_int @ A @ (numeral_numeral_nat @ (bit0 @ one))) = zero_zero_int) = (A = zero_zero_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 17.01/5.06 thf(129,axiom,((! [A:nat]: (((A = zero_zero_nat) => ((power_power_real @ zero_zero_real @ A) = one_one_real)) & ((A != zero_zero_nat) => ((power_power_real @ zero_zero_real @ A) = zero_zero_real))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_306_power__0__left)).
% 17.01/5.06 thf(789,plain,((! [A:nat]: (((A = zero_zero_nat) => ((power_power_real @ zero_zero_real @ A) = one_one_real)) & ((~ (A = zero_zero_nat)) => ((power_power_real @ zero_zero_real @ A) = zero_zero_real))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 17.01/5.06 thf(231,axiom,((! [A:int]: ((ord_less_eq_int @ zero_zero_int @ A) => (? [B:nat]: (A = (semiri2019852685at_int @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_294_zero__le__imp__eq__int)).
% 17.01/5.06 thf(1109,plain,((! [A:int]: ((ord_less_eq_int @ zero_zero_int @ A) => (? [B:nat]: (A = (semiri2019852685at_int @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 17.01/5.06 thf(337,axiom,((! [A:real]: (((power_power_real @ A @ (numeral_numeral_nat @ (bit0 @ one))) = zero_zero_real) = (A = zero_zero_real)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_288_zero__eq__power2)).
% 17.01/5.06 thf(1418,plain,((! [A:real]: (((power_power_real @ A @ (numeral_numeral_nat @ (bit0 @ one))) = zero_zero_real) = (A = zero_zero_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[337])).
% 17.01/5.06 thf(242,axiom,((! [A:int,B:nat]: ((ord_less_eq_int @ zero_zero_int @ A) => ((ord_less_eq_nat @ B @ (nat2 @ A)) = (ord_less_eq_int @ (semiri2019852685at_int @ B) @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_339_le__nat__iff)).
% 17.01/5.06 thf(1136,plain,((! [A:int,B:nat]: ((ord_less_eq_int @ zero_zero_int @ A) => ((ord_less_eq_nat @ B @ (nat2 @ A)) = (ord_less_eq_int @ (semiri2019852685at_int @ B) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 17.01/5.06 thf(46,axiom,((! [A:nat]: (((A = zero_zero_nat) => ((power_power_nat @ zero_zero_nat @ A) = one_one_nat)) & ((A != zero_zero_nat) => ((power_power_nat @ zero_zero_nat @ A) = zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_305_power__0__left)).
% 17.01/5.06 thf(514,plain,((! [A:nat]: (((A = zero_zero_nat) => ((power_power_nat @ zero_zero_nat @ A) = one_one_nat)) & ((~ (A = zero_zero_nat)) => ((power_power_nat @ zero_zero_nat @ A) = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 17.01/5.06 thf(64,axiom,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_302_zero__le)).
% 17.01/5.06 thf(574,plain,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 17.01/5.06 thf(134,axiom,((! [A:nat]: ((zero_zero_int = (semiri2019852685at_int @ A)) = (zero_zero_nat = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_237_of__nat__0__eq__iff)).
% 17.01/5.06 thf(806,plain,((! [A:nat]: ((zero_zero_int = (semiri2019852685at_int @ A)) = (zero_zero_nat = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 17.01/5.06 thf(178,axiom,((! [A:num,B:nat,C:nat]: ((ord_less_eq_int @ (power_power_int @ (numeral_numeral_int @ A) @ B) @ (semiri2019852685at_int @ C)) = (ord_less_eq_nat @ (power_power_nat @ (numeral_numeral_nat @ A) @ B) @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_165_numeral__power__le__of__nat__cancel__iff)).
% 17.01/5.06 thf(966,plain,((! [A:num,B:nat,C:nat]: ((ord_less_eq_int @ (power_power_int @ (numeral_numeral_int @ A) @ B) @ (semiri2019852685at_int @ C)) = (ord_less_eq_nat @ (power_power_nat @ (numeral_numeral_nat @ A) @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 17.01/5.06 thf(139,axiom,((((=) @ nat) = (^ [A:nat,B:nat]: ((semiri2019852685at_int @ A) = (semiri2019852685at_int @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_292_nat__int__comparison_I1_J)).
% 17.01/5.06 thf(821,plain,((((=) @ nat) = (^ [A:nat,B:nat]: ((semiri2019852685at_int @ A) = (semiri2019852685at_int @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 17.01/5.06 thf(159,axiom,(((power_power_real @ one_one_real @ (numeral_numeral_nat @ (bit0 @ one))) = one_one_real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_214_one__power2)).
% 17.01/5.06 thf(905,plain,(((power_power_real @ one_one_real @ (numeral_numeral_nat @ (bit0 @ one))) = one_one_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 17.01/5.06 thf(298,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ zero_zero_nat @ A) => ((ord_less_eq_nat @ zero_zero_nat @ B) => (((power_power_nat @ A @ (numeral_numeral_nat @ (bit0 @ one))) = (power_power_nat @ B @ (numeral_numeral_nat @ (bit0 @ one)))) = (A = B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_226_power2__eq__iff__nonneg)).
% 17.01/5.06 thf(1302,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ zero_zero_nat @ A) => ((ord_less_eq_nat @ zero_zero_nat @ B) => (((power_power_nat @ A @ (numeral_numeral_nat @ (bit0 @ one))) = (power_power_nat @ B @ (numeral_numeral_nat @ (bit0 @ one)))) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[298])).
% 17.01/5.06 thf(118,axiom,((! [A:nat,B:nat]: ((A != zero_zero_nat) => ((power_power_nat @ A @ B) != zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_317_power__not__zero)).
% 17.01/5.06 thf(756,plain,((! [A:nat,B:nat]: ((~ (A = zero_zero_nat)) => (~ ((power_power_nat @ A @ B) = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 17.01/5.06 thf(121,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (suc @ A) @ B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_196_Suc__leD)).
% 17.01/5.06 thf(766,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (suc @ A) @ B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 17.01/5.06 thf(98,axiom,((! [A:num]: (zero_zero_nat != (numeral_numeral_nat @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_315_zero__neq__numeral)).
% 17.01/5.06 thf(687,plain,((! [A:num]: ~ (zero_zero_nat = (numeral_numeral_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 17.01/5.06 thf(85,axiom,((! [A:num,B:num]: ((ord_less_eq_nat @ (numeral_numeral_nat @ A) @ (numeral_numeral_nat @ B)) = (ord_less_eq_num @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_51_numeral__le__iff)).
% 17.01/5.06 thf(634,plain,((! [A:num,B:num]: ((ord_less_eq_nat @ (numeral_numeral_nat @ A) @ (numeral_numeral_nat @ B)) = (ord_less_eq_num @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 17.01/5.06 thf(149,axiom,((! [A:real]: ((power_power_real @ A @ (suc @ zero_zero_nat)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_243_power__Suc0__right)).
% 17.01/5.06 thf(866,plain,((! [A:real]: ((power_power_real @ A @ (suc @ zero_zero_nat)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 17.01/5.06 thf(31,axiom,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_231_le__zero__eq)).
% 17.01/5.06 thf(453,plain,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 17.01/5.06 thf(19,axiom,(((semiri2110766477t_real @ one_one_nat) = one_one_real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_127_of__nat__1)).
% 17.01/5.06 thf(396,plain,(((semiri2110766477t_real @ one_one_nat) = one_one_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 17.01/5.06 thf(264,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ A) @ B) => (ord_less_eq_real @ (semiri2110766477t_real @ A) @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (semiri2110766477t_real @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_186_le__log2__of__power)).
% 17.01/5.06 thf(1201,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (power_power_nat @ (numeral_numeral_nat @ (bit0 @ one)) @ A) @ B) => (ord_less_eq_real @ (semiri2110766477t_real @ A) @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (semiri2110766477t_real @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 17.01/5.06 thf(278,axiom,((! [A:num]: ((neg_numeral_dbl_real @ (numeral_numeral_real @ A)) = (numeral_numeral_real @ (bit0 @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_276_dbl__simps_I5_J)).
% 17.01/5.06 thf(1242,plain,((! [A:num]: ((neg_numeral_dbl_real @ (numeral_numeral_real @ A)) = (numeral_numeral_real @ (bit0 @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 17.01/5.06 thf(235,axiom,((zero_zero_nat = (nat2 @ zero_zero_int))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_303_nat__zero__as__int)).
% 17.01/5.06 thf(1119,plain,((zero_zero_nat = (nat2 @ zero_zero_int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 17.01/5.06 thf(124,axiom,((! [A:(nat > nat),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_nat @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ (A @ B) @ (A @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_205_lift__Suc__mono__le)).
% 17.01/5.06 thf(774,plain,((! [A:(nat > nat),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_nat @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ (A @ B) @ (A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 17.01/5.06 thf(22,axiom,((! [A:(nat > real),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_real @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_real @ (A @ B) @ (A @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_206_lift__Suc__mono__le)).
% 17.01/5.06 thf(411,plain,((! [A:(nat > real),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_real @ (A @ D) @ (A @ (suc @ D)))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_real @ (A @ B) @ (A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 17.01/5.06 thf(311,axiom,((! [A:num]: ((one_one_real = (numeral_numeral_real @ A)) = (one = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_73_one__eq__numeral__iff)).
% 17.01/5.06 thf(1345,plain,((! [A:num]: ((one_one_real = (numeral_numeral_real @ A)) = (one = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[311])).
% 17.01/5.06 thf(186,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_int @ (power_power_int @ (semiri2019852685at_int @ A) @ B) @ (semiri2019852685at_int @ C)) = (ord_less_eq_nat @ (power_power_nat @ A @ B) @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_151_of__nat__le__of__nat__power__cancel__iff)).
% 17.01/5.06 thf(988,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_int @ (power_power_int @ (semiri2019852685at_int @ A) @ B) @ (semiri2019852685at_int @ C)) = (ord_less_eq_nat @ (power_power_nat @ A @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 17.01/5.06 thf(13,axiom,((! [A:nat]: (((semiri1382578993at_nat @ A) = one_one_nat) = (A = one_one_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_120_of__nat__eq__1__iff)).
% 17.01/5.06 thf(380,plain,((! [A:nat]: (((semiri1382578993at_nat @ A) = one_one_nat) = (A = one_one_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 17.01/5.06 thf(91,axiom,((! [A:real]: ((power_power_real @ A @ one_one_nat) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_112_power__one__right)).
% 17.01/5.06 thf(661,plain,((! [A:real]: ((power_power_real @ A @ one_one_nat) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 17.01/5.06 thf(299,axiom,((! [A:num,B:num]: ((ord_less_eq_int @ (numeral_numeral_int @ A) @ (numeral_numeral_int @ B)) = (ord_less_eq_num @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_50_numeral__le__iff)).
% 17.01/5.06 thf(1306,plain,((! [A:num,B:num]: ((ord_less_eq_int @ (numeral_numeral_int @ A) @ (numeral_numeral_int @ B)) = (ord_less_eq_num @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[299])).
% 17.01/5.06 thf(263,axiom,((n = (suc @ (nat2 @ (archim1371465213g_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_54_n__def)).
% 17.01/5.06 thf(1199,plain,((n = (suc @ (nat2 @ (archim1371465213g_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 17.01/5.06 thf(247,axiom,((! [A:num]: ((ord_less_eq_num @ A @ one) = (A = one)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_97_le__num__One__iff)).
% 17.01/5.06 thf(1153,plain,((! [A:num]: ((ord_less_eq_num @ A @ one) = (A = one)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 17.01/5.06 thf(309,axiom,((! [A:num]: (zero_zero_real != (numeral_numeral_real @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_314_zero__neq__numeral)).
% 17.01/5.06 thf(1338,plain,((! [A:num]: ~ (zero_zero_real = (numeral_numeral_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[309])).
% 17.01/5.06 thf(8,axiom,((! [A:nat]: ((zero_zero_nat = (semiri1382578993at_nat @ A)) = (zero_zero_nat = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_235_of__nat__0__eq__iff)).
% 17.01/5.06 thf(366,plain,((! [A:nat]: ((zero_zero_nat = (semiri1382578993at_nat @ A)) = (zero_zero_nat = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 17.01/5.06 thf(301,axiom,((! [A:num]: ((pow @ A @ one) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_348_pow_Osimps_I1_J)).
% 17.01/5.06 thf(1311,plain,((! [A:num]: ((pow @ A @ one) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[301])).
% 17.01/5.06 thf(130,axiom,(((neg_numeral_dbl_real @ zero_zero_real) = zero_zero_real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_258_dbl__simps_I2_J)).
% 17.01/5.06 thf(798,plain,(((neg_numeral_dbl_real @ zero_zero_real) = zero_zero_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 17.01/5.06 thf(289,axiom,((! [A:nat,B:num,C:nat]: (((semiri2019852685at_int @ A) = (power_power_int @ (numeral_numeral_int @ B) @ C)) = (A = (power_power_nat @ (numeral_numeral_nat @ B) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_156_real__of__nat__eq__numeral__power__cancel__iff)).
% 17.01/5.06 thf(1274,plain,((! [A:nat,B:num,C:nat]: (((semiri2019852685at_int @ A) = (power_power_int @ (numeral_numeral_int @ B) @ C)) = (A = (power_power_nat @ (numeral_numeral_nat @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[289])).
% 17.01/5.06 thf(161,axiom,((! [A:num]: (((numeral_numeral_int @ A) = one_one_int) = (A = one)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_69_numeral__eq__one__iff)).
% 17.01/5.06 thf(910,plain,((! [A:num]: (((numeral_numeral_int @ A) = one_one_int) = (A = one)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 17.01/5.06 thf(271,axiom,(((ring_1_of_int_real @ d) = (powr_real @ (numeral_numeral_real @ (bit0 @ one)) @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_53__092_060open_062real__of__int_Ad_A_061_A2_Apowr_Alog_A2_A_Ireal__of__int_Ad_J_092_060close_062)).
% 17.01/5.06 thf(1223,plain,(((ring_1_of_int_real @ d) = (powr_real @ (numeral_numeral_real @ (bit0 @ one)) @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 17.01/5.06 thf(224,axiom,((! [A:num]: (ord_less_eq_int @ one_one_int @ (numeral_numeral_int @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_87_one__le__numeral)).
% 17.01/5.06 thf(1091,plain,((! [A:num]: (ord_less_eq_int @ one_one_int @ (numeral_numeral_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 17.01/5.06 thf(198,axiom,((! [A:nat]: ((ring_1_of_int_real @ (semiri2019852685at_int @ A)) = (semiri2110766477t_real @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_129_of__int__of__nat__eq)).
% 17.01/5.06 thf(1021,plain,((! [A:nat]: ((ring_1_of_int_real @ (semiri2019852685at_int @ A)) = (semiri2110766477t_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 17.01/5.06 thf(206,axiom,((! [A:real,B:nat]: ((ord_less_eq_nat @ (nat2 @ (archim1371465213g_real @ A)) @ B) = (ord_less_eq_real @ A @ (semiri2110766477t_real @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_161_nat__ceiling__le__eq)).
% 17.01/5.06 thf(1042,plain,((! [A:real,B:nat]: ((ord_less_eq_nat @ (nat2 @ (archim1371465213g_real @ A)) @ B) = (ord_less_eq_real @ A @ (semiri2110766477t_real @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 17.01/5.06 thf(137,axiom,((! [A:num,B:num]: ((A = B) | ~ (ord_less_eq_num @ A @ B) | ~ (ord_less_eq_num @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_verit__la__disequality)).
% 17.01/5.06 thf(815,plain,((! [A:num,B:num]: ((A = B) | ~ (ord_less_eq_num @ A @ B) | ~ (ord_less_eq_num @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 17.01/5.06 thf(269,axiom,((! [A:num]: ((archim1371465213g_real @ (numeral_numeral_real @ A)) = (numeral_numeral_int @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_33_ceiling__numeral)).
% 17.01/5.06 thf(1217,plain,((! [A:num]: ((archim1371465213g_real @ (numeral_numeral_real @ A)) = (numeral_numeral_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 17.01/5.06 thf(73,axiom,((! [A:int]: ((zero_zero_int = A) = (A = zero_zero_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_301_zero__reorient)).
% 17.01/5.06 thf(598,plain,((! [A:int]: ((zero_zero_int = A) = (A = zero_zero_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 17.01/5.06 thf(163,axiom,((! [A:num]: ((ord_less_eq_real @ (numeral_numeral_real @ A) @ one_one_real) = (ord_less_eq_num @ A @ one)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_82_numeral__le__one__iff)).
% 17.01/5.06 thf(916,plain,((! [A:num]: ((ord_less_eq_real @ (numeral_numeral_real @ A) @ one_one_real) = (ord_less_eq_num @ A @ one)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 17.01/5.06 thf(82,axiom,((! [A:num,B:nat,C:nat]: (((power_power_nat @ (numeral_numeral_nat @ A) @ B) = (semiri1382578993at_nat @ C)) = ((power_power_nat @ (numeral_numeral_nat @ A) @ B) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_157_numeral__power__eq__of__nat__cancel__iff)).
% 17.01/5.06 thf(625,plain,((! [A:num,B:nat,C:nat]: (((power_power_nat @ (numeral_numeral_nat @ A) @ B) = (semiri1382578993at_nat @ C)) = ((power_power_nat @ (numeral_numeral_nat @ A) @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 17.01/5.06 thf(154,axiom,((! [A:real]: (ord_less_eq_real @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_222_order__refl)).
% 17.01/5.06 thf(879,plain,((! [A:real]: (ord_less_eq_real @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 17.01/5.06 thf(249,axiom,((! [A:num]: (((numeral_numeral_real @ A) = one_one_real) = (A = one)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_70_numeral__eq__one__iff)).
% 17.01/5.06 thf(1159,plain,((! [A:num]: (((numeral_numeral_real @ A) = one_one_real) = (A = one)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 17.01/5.06 thf(200,axiom,((! [A:real]: ((ord_less_eq_int @ (archim1371465213g_real @ A) @ zero_zero_int) = (ord_less_eq_real @ A @ zero_zero_real)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_281_ceiling__le__zero)).
% 17.01/5.06 thf(1027,plain,((! [A:real]: ((ord_less_eq_int @ (archim1371465213g_real @ A) @ zero_zero_int) = (ord_less_eq_real @ A @ zero_zero_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 17.01/5.06 thf(238,axiom,((ord_less_eq_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ one_one_real) @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_46__092_060open_062log_A2_A1_A_092_060le_062_Alog_A2_A_Ireal__of__int_Ad_J_092_060close_062)).
% 17.01/5.06 thf(1128,plain,((ord_less_eq_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ one_one_real) @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 17.01/5.06 thf(291,axiom,((! [A:num]: ((semiri2019852685at_int @ (numeral_numeral_nat @ A)) = (numeral_numeral_int @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_137_of__nat__numeral)).
% 17.01/5.06 thf(1281,plain,((! [A:num]: ((semiri2019852685at_int @ (numeral_numeral_nat @ A)) = (numeral_numeral_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[291])).
% 17.01/5.06 thf(328,axiom,((! [A:num]: ((ord_less_eq_int @ (numeral_numeral_int @ A) @ one_one_int) = (ord_less_eq_num @ A @ one)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_80_numeral__le__one__iff)).
% 17.01/5.06 thf(1392,plain,((! [A:num]: ((ord_less_eq_int @ (numeral_numeral_int @ A) @ one_one_int) = (ord_less_eq_num @ A @ one)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[328])).
% 17.01/5.06 thf(32,axiom,((! [A:nat,B:nat,C:(nat > (nat > $o))]: ((ord_less_eq_nat @ A @ B) => ((! [D:nat]: (C @ D @ D)) => ((! [D:nat,E:nat,F:nat]: ((C @ D @ E) => ((C @ E @ F) => (C @ D @ F)))) => ((! [D:nat]: (C @ D @ (suc @ D))) => (C @ A @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_187_transitive__stepwise__le)).
% 17.01/5.06 thf(456,plain,((! [A:nat,B:nat,C:(nat > (nat > $o))]: ((ord_less_eq_nat @ A @ B) => ((! [D:nat]: (C @ D @ D)) => ((! [D:nat,E:nat,F:nat]: ((C @ D @ E) => ((C @ E @ F) => (C @ D @ F)))) => ((! [D:nat]: (C @ D @ (suc @ D))) => (C @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 17.01/5.06 thf(230,axiom,((! [A:int,B:nat,C:int]: ((ord_less_eq_real @ (power_power_real @ (ring_1_of_int_real @ A) @ B) @ (ring_1_of_int_real @ C)) = (ord_less_eq_int @ (power_power_int @ A @ B) @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_10_of__int__le__of__int__power__cancel__iff)).
% 17.01/5.06 thf(1106,plain,((! [A:int,B:nat,C:int]: ((ord_less_eq_real @ (power_power_real @ (ring_1_of_int_real @ A) @ B) @ (ring_1_of_int_real @ C)) = (ord_less_eq_int @ (power_power_int @ A @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 17.01/5.06 thf(296,axiom,((! [A:num,B:num]: ((ord_less_eq_num @ (bit0 @ A) @ (bit0 @ B)) = (ord_less_eq_num @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_56_semiring__norm_I71_J)).
% 17.01/5.06 thf(1296,plain,((! [A:num,B:num]: ((ord_less_eq_num @ (bit0 @ A) @ (bit0 @ B)) = (ord_less_eq_num @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[296])).
% 17.01/5.06 thf(93,axiom,((! [A:(nat > real),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_real @ (A @ (suc @ D)) @ (A @ D))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_real @ (A @ C) @ (A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_202_lift__Suc__antimono__le)).
% 17.01/5.06 thf(665,plain,((! [A:(nat > real),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_real @ (A @ (suc @ D)) @ (A @ D))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_real @ (A @ C) @ (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 17.01/5.06 thf(38,axiom,((! [A:nat]: ((power_power_real @ zero_zero_real @ (suc @ A)) = zero_zero_real))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_265_power__0__Suc)).
% 17.01/5.06 thf(493,plain,((! [A:nat]: ((power_power_real @ zero_zero_real @ (suc @ A)) = zero_zero_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 17.01/5.06 thf(267,axiom,((! [A:num]: (one != (bit0 @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_48_semiring__norm_I83_J)).
% 17.01/5.06 thf(1210,plain,((! [A:num]: ~ (one = (bit0 @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 17.01/5.06 thf(96,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_179_le__antisym)).
% 17.01/5.06 thf(682,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)],[96])).
% 17.01/5.06 thf(333,axiom,((! [A:int]: ((ord_less_eq_int @ zero_zero_int @ A) => ((semiri2019852685at_int @ (nat2 @ A)) = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_307_nat__0__le)).
% 17.01/5.06 thf(1407,plain,((! [A:int]: ((ord_less_eq_int @ zero_zero_int @ A) => ((semiri2019852685at_int @ (nat2 @ A)) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[333])).
% 17.01/5.06 thf(313,axiom,((! [A:nat,B:nat,C:nat]: (((semiri2019852685at_int @ A) = (power_power_int @ (semiri2019852685at_int @ B) @ C)) = (A = (power_power_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_140_of__nat__power__eq__of__nat__cancel__iff)).
% 17.01/5.06 thf(1350,plain,((! [A:nat,B:nat,C:nat]: (((semiri2019852685at_int @ A) = (power_power_int @ (semiri2019852685at_int @ B) @ C)) = (A = (power_power_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[313])).
% 17.01/5.06 thf(115,axiom,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_229_bot__nat__0_Oextremum)).
% 17.01/5.06 thf(742,plain,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 17.01/5.06 thf(101,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_real @ (semiri2110766477t_real @ A) @ (semiri2110766477t_real @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_172_of__nat__mono)).
% 17.01/5.06 thf(697,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_real @ (semiri2110766477t_real @ A) @ (semiri2110766477t_real @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 17.01/5.06 thf(284,axiom,((! [A:num,B:nat,C:int]: ((ord_less_eq_nat @ (power_power_nat @ (numeral_numeral_nat @ A) @ B) @ (nat2 @ C)) = (ord_less_eq_int @ (power_power_int @ (numeral_numeral_int @ A) @ B) @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_38_numeral__power__le__nat__cancel__iff)).
% 17.01/5.06 thf(1259,plain,((! [A:num,B:nat,C:int]: ((ord_less_eq_nat @ (power_power_nat @ (numeral_numeral_nat @ A) @ B) @ (nat2 @ C)) = (ord_less_eq_int @ (power_power_int @ (numeral_numeral_int @ A) @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[284])).
% 17.01/5.06 thf(174,axiom,((! [A:nat]: (((power_power_nat @ A @ (numeral_numeral_nat @ (bit0 @ one))) = zero_zero_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_287_zero__eq__power2)).
% 17.01/5.06 thf(948,plain,((! [A:nat]: (((power_power_nat @ A @ (numeral_numeral_nat @ (bit0 @ one))) = zero_zero_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 17.01/5.06 thf(214,axiom,((! [A:real]: (ord_less_eq_real @ A @ (semiri2110766477t_real @ (nat2 @ (archim1371465213g_real @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_183_real__nat__ceiling__ge)).
% 17.01/5.06 thf(1064,plain,((! [A:real]: (ord_less_eq_real @ A @ (semiri2110766477t_real @ (nat2 @ (archim1371465213g_real @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 17.01/5.06 thf(16,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_182_le__refl)).
% 17.01/5.06 thf(388,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 17.01/5.06 thf(71,axiom,((! [A:nat]: ((one_one_int = (semiri2019852685at_int @ A)) = (A = one_one_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_125_of__nat__1__eq__iff)).
% 17.01/5.06 thf(593,plain,((! [A:nat]: ((one_one_int = (semiri2019852685at_int @ A)) = (A = one_one_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 17.01/5.06 thf(150,axiom,((! [A:nat]: (ord_less_eq_nat @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_221_order__refl)).
% 17.01/5.06 thf(869,plain,((! [A:nat]: (ord_less_eq_nat @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 17.01/5.06 thf(41,axiom,((! [A:nat]: ((power_power_nat @ zero_zero_nat @ (suc @ A)) = zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_264_power__0__Suc)).
% 17.01/5.06 thf(499,plain,((! [A:nat]: ((power_power_nat @ zero_zero_nat @ (suc @ A)) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 17.01/5.06 thf(146,axiom,((! [A:real]: ((zero_zero_real = A) = (A = zero_zero_real)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_299_zero__reorient)).
% 17.01/5.06 thf(857,plain,((! [A:real]: ((zero_zero_real = A) = (A = zero_zero_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 17.01/5.06 thf(322,axiom,((! [A:int]: ((ord_less_eq_int @ A @ zero_zero_int) => ((nat2 @ A) = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_253_nat__le__0)).
% 17.01/5.06 thf(1375,plain,((! [A:int]: ((ord_less_eq_int @ A @ zero_zero_int) => ((nat2 @ A) = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[322])).
% 17.01/5.06 thf(236,axiom,((! [A:num,B:num]: ((ord_less_eq_real @ (numeral_numeral_real @ A) @ (numeral_numeral_real @ B)) = (ord_less_eq_num @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_52_numeral__le__iff)).
% 17.01/5.06 thf(1121,plain,((! [A:num,B:num]: ((ord_less_eq_real @ (numeral_numeral_real @ A) @ (numeral_numeral_real @ B)) = (ord_less_eq_num @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 17.01/5.06 thf(127,axiom,((! [A:nat,B:nat]: (((power_power_nat @ A @ B) = (suc @ zero_zero_nat)) = ((B = zero_zero_nat) | (A = (suc @ zero_zero_nat)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_256_nat__power__eq__Suc__0__iff)).
% 17.01/5.06 thf(783,plain,((! [A:nat,B:nat]: (((power_power_nat @ A @ B) = (suc @ zero_zero_nat)) = ((B = zero_zero_nat) | (A = (suc @ zero_zero_nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 17.01/5.06 thf(25,axiom,((! [A:(nat > $o),B:nat]: ((A @ zero_zero_nat) => ((! [C:nat]: ((A @ C) => (A @ (suc @ C)))) => (A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_332_old_Onat_Oinducts)).
% 17.01/5.06 thf(420,plain,((! [A:(nat > $o),B:nat]: ((A @ zero_zero_nat) => ((! [C:nat]: ((A @ C) => (A @ (suc @ C)))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 17.01/5.06 thf(33,axiom,((! [A:(nat > nat),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_nat @ (A @ (suc @ D)) @ (A @ D))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ (A @ C) @ (A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_201_lift__Suc__antimono__le)).
% 17.01/5.06 thf(471,plain,((! [A:(nat > nat),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_nat @ (A @ (suc @ D)) @ (A @ D))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_nat @ (A @ C) @ (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 17.01/5.06 thf(156,axiom,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less_eq_nat @ A @ B) => ((C @ A) => ((! [D:nat]: ((ord_less_eq_nat @ A @ D) => ((C @ D) => (C @ (suc @ D))))) => (C @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_188_nat__induct__at__least)).
% 17.01/5.06 thf(884,plain,((! [A:nat,B:nat,C:(nat > $o)]: ((ord_less_eq_nat @ A @ B) => ((C @ A) => ((! [D:nat]: ((ord_less_eq_nat @ A @ D) => ((C @ D) => (C @ (suc @ D))))) => (C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 17.01/5.06 thf(221,axiom,((! [A:int,B:int]: ((A = B) | ~ (ord_less_eq_int @ A @ B) | ~ (ord_less_eq_int @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_93_verit__la__disequality)).
% 17.01/5.06 thf(1082,plain,((! [A:int,B:int]: ((A = B) | ~ (ord_less_eq_int @ A @ B) | ~ (ord_less_eq_int @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 17.01/5.06 thf(295,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ zero_zero_real @ A) => ((ord_less_eq_real @ zero_zero_real @ B) => (((power_power_real @ A @ (numeral_numeral_nat @ (bit0 @ one))) = (power_power_real @ B @ (numeral_numeral_nat @ (bit0 @ one)))) = (A = B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_227_power2__eq__iff__nonneg)).
% 17.01/5.06 thf(1292,plain,((! [A:real,B:real]: ((ord_less_eq_real @ zero_zero_real @ A) => ((ord_less_eq_real @ zero_zero_real @ B) => (((power_power_real @ A @ (numeral_numeral_nat @ (bit0 @ one))) = (power_power_real @ B @ (numeral_numeral_nat @ (bit0 @ one)))) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[295])).
% 17.01/5.06 thf(117,axiom,((! [A:real]: (((powr_real @ A @ one_one_real) = A) = (ord_less_eq_real @ zero_zero_real @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_283_powr__one__gt__zero__iff)).
% 17.01/5.06 thf(753,plain,((! [A:real]: (((powr_real @ A @ one_one_real) = A) = (ord_less_eq_real @ zero_zero_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 17.01/5.06 thf(257,axiom,((((!) @ nat) = (^ [A:(nat > $o)]: ! [B:int]: ((ord_less_eq_int @ zero_zero_int @ B) => (A @ (nat2 @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_344_all__nat)).
% 17.01/5.06 thf(1182,plain,((((!) @ nat) = (^ [A:(nat > $o)]: ! [B:int]: ((ord_less_eq_int @ zero_zero_int @ B) => (A @ (nat2 @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 17.01/5.06 thf(339,axiom,((! [A:nat]: ((archim1371465213g_real @ (semiri2110766477t_real @ A)) = (semiri2019852685at_int @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_131_ceiling__of__nat)).
% 17.01/5.06 thf(1424,plain,((! [A:nat]: ((archim1371465213g_real @ (semiri2110766477t_real @ A)) = (semiri2019852685at_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[339])).
% 17.01/5.06 thf(88,axiom,((! [A:(nat > $o),B:nat]: ((A @ zero_zero_nat) => ((! [C:nat]: ((A @ C) => (A @ (suc @ C)))) => (A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_324_nat__induct)).
% 17.01/5.06 thf(642,plain,((! [A:(nat > $o),B:nat]: ((A @ zero_zero_nat) => ((! [C:nat]: ((A @ C) => (A @ (suc @ C)))) => (A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 17.01/5.06 thf(86,axiom,((! [A:nat,B:nat,C:nat]: (((power_power_real @ (semiri2110766477t_real @ A) @ B) = (semiri2110766477t_real @ C)) = ((power_power_nat @ A @ B) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_142_of__nat__eq__of__nat__power__cancel__iff)).
% 17.01/5.06 thf(637,plain,((! [A:nat,B:nat,C:nat]: (((power_power_real @ (semiri2110766477t_real @ A) @ B) = (semiri2110766477t_real @ C)) = ((power_power_nat @ A @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 17.01/5.06 thf(268,axiom,((! [A:int,B:nat]: ((ord_less_eq_int @ one_one_int @ A) => (ord_less_eq_int @ one_one_int @ (power_power_int @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_197_one__le__power)).
% 17.01/5.06 thf(1214,plain,((! [A:int,B:nat]: ((ord_less_eq_int @ one_one_int @ A) => (ord_less_eq_int @ one_one_int @ (power_power_int @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 17.01/5.06 thf(347,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_int @ (archim1371465213g_real @ A) @ (archim1371465213g_real @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_43_ceiling__mono)).
% 17.01/5.06 thf(1446,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_int @ (archim1371465213g_real @ A) @ (archim1371465213g_real @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[347])).
% 17.01/5.06 thf(95,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (semiri1382578993at_nat @ A) @ (power_power_nat @ (semiri1382578993at_nat @ B) @ C)) = (ord_less_eq_nat @ A @ (power_power_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_149_of__nat__power__le__of__nat__cancel__iff)).
% 17.01/5.06 thf(679,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (semiri1382578993at_nat @ A) @ (power_power_nat @ (semiri1382578993at_nat @ B) @ C)) = (ord_less_eq_nat @ A @ (power_power_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 17.01/5.06 thf(55,axiom,((! [A:nat]: ((power_power_nat @ (suc @ zero_zero_nat) @ A) = (suc @ zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_255_power__Suc__0)).
% 17.01/5.06 thf(547,plain,((! [A:nat]: ((power_power_nat @ (suc @ zero_zero_nat) @ A) = (suc @ zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 17.01/5.06 thf(196,axiom,((! [A:nat,B:nat]: ((semiri2019852685at_int @ (power_power_nat @ A @ B)) = (power_power_int @ (semiri2019852685at_int @ A) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_146_of__nat__power)).
% 17.01/5.06 thf(1016,plain,((! [A:nat,B:nat]: ((semiri2019852685at_int @ (power_power_nat @ A @ B)) = (power_power_int @ (semiri2019852685at_int @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 17.01/5.06 thf(266,axiom,((! [A:int]: (((ring_1_of_int_real @ A) = one_one_real) = (A = one_one_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_of__int__eq__1__iff)).
% 17.01/5.06 thf(1207,plain,((! [A:int]: (((ring_1_of_int_real @ A) = one_one_real) = (A = one_one_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 17.01/5.06 thf(70,axiom,((! [A:nat,B:nat,C:nat]: (((semiri2110766477t_real @ A) = (power_power_real @ (semiri2110766477t_real @ B) @ C)) = (A = (power_power_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_139_of__nat__power__eq__of__nat__cancel__iff)).
% 17.01/5.06 thf(590,plain,((! [A:nat,B:nat,C:nat]: (((semiri2110766477t_real @ A) = (power_power_real @ (semiri2110766477t_real @ B) @ C)) = (A = (power_power_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 17.01/5.06 thf(81,axiom,((! [A:nat]: (((semiri2019852685at_int @ A) = zero_zero_int) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_240_of__nat__eq__0__iff)).
% 17.01/5.06 thf(622,plain,((! [A:nat]: (((semiri2019852685at_int @ A) = zero_zero_int) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 17.01/5.06 thf(189,axiom,((numeral_numeral_nat = (^ [A:num]: (nat2 @ (numeral_numeral_int @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_101_nat__numeral__as__int)).
% 17.01/5.06 thf(997,plain,(((numeral_numeral_nat) = (^ [A:num]: (nat2 @ (numeral_numeral_int @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 17.01/5.06 thf(185,axiom,((! [A:nat,B:int]: ((A = (nat2 @ B)) = (((ord_less_eq_int @ zero_zero_int @ B) => (B = (semiri2019852685at_int @ A))) & ((~ (ord_less_eq_int @ zero_zero_int @ B)) => (A = zero_zero_nat)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_297_nat__eq__iff2)).
% 17.01/5.06 thf(985,plain,((! [A:nat,B:int]: ((A = (nat2 @ B)) = (((ord_less_eq_int @ zero_zero_int @ B) => (B = (semiri2019852685at_int @ A))) & ((~ (ord_less_eq_int @ zero_zero_int @ B)) => (A = zero_zero_nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 17.01/5.06 thf(246,axiom,((! [A:num,B:num]: (((bit0 @ A) = (bit0 @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_57_semiring__norm_I87_J)).
% 17.01/5.06 thf(1150,plain,((! [A:num,B:num]: (((bit0 @ A) = (bit0 @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 17.01/5.06 thf(349,axiom,((! [A:nat]: ((ord_less_eq_int @ (semiri2019852685at_int @ A) @ zero_zero_int) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_260_of__nat__le__0__iff)).
% 17.01/5.06 thf(1451,plain,((! [A:nat]: ((ord_less_eq_int @ (semiri2019852685at_int @ A) @ zero_zero_int) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[349])).
% 17.01/5.06 thf(325,axiom,((! [A:num]: ((ring_1_of_int_int @ (numeral_numeral_int @ A)) = (numeral_numeral_int @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_29_of__int__numeral)).
% 17.01/5.06 thf(1382,plain,((! [A:num]: ((ring_1_of_int_int @ (numeral_numeral_int @ A)) = (numeral_numeral_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[325])).
% 17.01/5.06 thf(240,axiom,((! [A:num,B:nat,C:int]: ((ord_less_eq_int @ (power_power_int @ (numeral_numeral_int @ A) @ B) @ (ring_1_of_int_int @ C)) = (ord_less_eq_int @ (power_power_int @ (numeral_numeral_int @ A) @ B) @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0_numeral__power__le__of__int__cancel__iff)).
% 17.01/5.06 thf(1131,plain,((! [A:num,B:nat,C:int]: ((ord_less_eq_int @ (power_power_int @ (numeral_numeral_int @ A) @ B) @ (ring_1_of_int_int @ C)) = (ord_less_eq_int @ (power_power_int @ (numeral_numeral_int @ A) @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 17.01/5.06 thf(109,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) => (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_175_Suc__inject)).
% 17.01/5.06 thf(721,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) => (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 17.01/5.06 thf(191,axiom,((! [A:real]: (((ring_1_of_int_real @ (archim1371465213g_real @ A)) = A) = (? [B:int]: (A = (ring_1_of_int_real @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_26_of__int__ceiling__cancel)).
% 17.01/5.06 thf(1002,plain,((! [A:real]: (((ring_1_of_int_real @ (archim1371465213g_real @ A)) = A) = (? [B:int]: (A = (ring_1_of_int_real @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 17.01/5.06 thf(75,axiom,((! [A:nat]: ~ (ord_less_eq_nat @ (suc @ A) @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_191_Suc__n__not__le__n)).
% 17.01/5.06 thf(605,plain,((! [A:nat]: ~ (ord_less_eq_nat @ (suc @ A) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 17.01/5.06 thf(18,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (power_power_nat @ (semiri1382578993at_nat @ A) @ B) @ (semiri1382578993at_nat @ C)) = (ord_less_eq_nat @ (power_power_nat @ A @ B) @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_152_of__nat__le__of__nat__power__cancel__iff)).
% 17.01/5.06 thf(393,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ (power_power_nat @ (semiri1382578993at_nat @ A) @ B) @ (semiri1382578993at_nat @ C)) = (ord_less_eq_nat @ (power_power_nat @ A @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 17.01/5.06 thf(233,axiom,((! [A:int]: ((ord_less_eq_real @ (ring_1_of_int_real @ A) @ zero_zero_real) = (ord_less_eq_int @ A @ zero_zero_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_280_of__int__le__0__iff)).
% 17.01/5.06 thf(1114,plain,((! [A:int]: ((ord_less_eq_real @ (ring_1_of_int_real @ A) @ zero_zero_real) = (ord_less_eq_int @ A @ zero_zero_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 17.01/5.06 thf(307,axiom,((! [A:int,B:nat,C:int]: (((power_power_real @ (ring_1_of_int_real @ A) @ B) = (ring_1_of_int_real @ C)) = ((power_power_int @ A @ B) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_21_of__int__eq__of__int__power__cancel__iff)).
% 17.01/5.06 thf(1333,plain,((! [A:int,B:nat,C:int]: (((power_power_real @ (ring_1_of_int_real @ A) @ B) = (ring_1_of_int_real @ C)) = ((power_power_int @ A @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[307])).
% 17.01/5.06 thf(342,axiom,((! [A:int,B:int,C:nat]: ((ord_less_eq_real @ (ring_1_of_int_real @ A) @ (power_power_real @ (ring_1_of_int_real @ B) @ C)) = (ord_less_eq_int @ A @ (power_power_int @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_12_of__int__power__le__of__int__cancel__iff)).
% 17.01/5.06 thf(1434,plain,((! [A:int,B:int,C:nat]: ((ord_less_eq_real @ (ring_1_of_int_real @ A) @ (power_power_real @ (ring_1_of_int_real @ B) @ C)) = (ord_less_eq_int @ A @ (power_power_int @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[342])).
% 17.01/5.06 thf(171,axiom,((! [A:num]: ((one_one_int = (numeral_numeral_int @ A)) = (one = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_72_one__eq__numeral__iff)).
% 17.01/5.06 thf(938,plain,((! [A:num]: ((one_one_int = (numeral_numeral_int @ A)) = (one = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 17.01/5.06 thf(6,axiom,((! [A:nat,B:nat,C:nat]: (((semiri1382578993at_nat @ A) = (power_power_nat @ (semiri1382578993at_nat @ B) @ C)) = (A = (power_power_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_138_of__nat__power__eq__of__nat__cancel__iff)).
% 17.01/5.06 thf(360,plain,((! [A:nat,B:nat,C:nat]: (((semiri1382578993at_nat @ A) = (power_power_nat @ (semiri1382578993at_nat @ B) @ C)) = (A = (power_power_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 17.01/5.06 thf(44,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ (suc @ B)) = ((ord_less_eq_nat @ A @ B) | (A = (suc @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_192_le__Suc__eq)).
% 17.01/5.06 thf(508,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ (suc @ B)) = ((ord_less_eq_nat @ A @ B) | (A = (suc @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 17.01/5.06 thf(165,axiom,((! [A:int,B:num,C:nat]: (((nat2 @ A) = (power_power_nat @ (numeral_numeral_nat @ B) @ C)) = (A = (power_power_int @ (numeral_numeral_int @ B) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_37_nat__eq__numeral__power__cancel__iff)).
% 17.01/5.06 thf(921,plain,((! [A:int,B:num,C:nat]: (((nat2 @ A) = (power_power_nat @ (numeral_numeral_nat @ B) @ C)) = (A = (power_power_int @ (numeral_numeral_int @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 17.01/5.06 thf(253,axiom,((! [A:int,B:num,C:nat]: ((ord_less_eq_int @ (ring_1_of_int_int @ A) @ (power_power_int @ (numeral_numeral_int @ B) @ C)) = (ord_less_eq_int @ A @ (power_power_int @ (numeral_numeral_int @ B) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_of__int__le__numeral__power__cancel__iff)).
% 17.01/5.06 thf(1170,plain,((! [A:int,B:num,C:nat]: ((ord_less_eq_int @ (ring_1_of_int_int @ A) @ (power_power_int @ (numeral_numeral_int @ B) @ C)) = (ord_less_eq_int @ A @ (power_power_int @ (numeral_numeral_int @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 17.01/5.06 thf(20,axiom,((! [A:set_real]: ((? [B:real]: (member_real @ B @ A)) => ((? [B:real]: ! [C:real]: ((member_real @ C @ A) => (ord_less_eq_real @ C @ B))) => (? [B:real]: (! [C:real]: ((member_real @ C @ A) => (ord_less_eq_real @ C @ B)) & ! [C:real]: ((! [D:real]: ((member_real @ D @ A) => (ord_less_eq_real @ D @ C))) => (ord_less_eq_real @ B @ C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_83_complete__real)).
% 17.01/5.06 thf(398,plain,((! [A:set_real]: ((? [B:real]: (member_real @ B @ A)) => ((? [B:real]: ! [C:real]: ((member_real @ C @ A) => (ord_less_eq_real @ C @ B))) => (? [B:real]: (! [C:real]: ((member_real @ C @ A) => (ord_less_eq_real @ C @ B)) & ! [C:real]: ((! [D:real]: ((member_real @ D @ A) => (ord_less_eq_real @ D @ C))) => (ord_less_eq_real @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 17.01/5.06 thf(259,axiom,((! [A:num]: ((nat2 @ (numeral_numeral_int @ A)) = (numeral_numeral_nat @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_24_nat__numeral)).
% 17.01/5.06 thf(1187,plain,((! [A:num]: ((nat2 @ (numeral_numeral_int @ A)) = (numeral_numeral_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 17.01/5.06 thf(252,axiom,((! [A:int,B:nat]: (((nat2 @ A) = B) = (((ord_less_eq_int @ zero_zero_int @ A) => (A = (semiri2019852685at_int @ B))) & ((~ (ord_less_eq_int @ zero_zero_int @ A)) => (B = zero_zero_nat)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_298_nat__eq__iff)).
% 17.01/5.06 thf(1167,plain,((! [A:int,B:nat]: (((nat2 @ A) = B) = (((ord_less_eq_int @ zero_zero_int @ A) => (A = (semiri2019852685at_int @ B))) & ((~ (ord_less_eq_int @ zero_zero_int @ A)) => (B = zero_zero_nat)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 17.01/5.06 thf(108,axiom,((! [A:nat]: ((power_power_real @ one_one_real @ A) = one_one_real))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_119_power__one)).
% 17.01/5.06 thf(718,plain,((! [A:nat]: ((power_power_real @ one_one_real @ A) = one_one_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 17.01/5.06 thf(281,axiom,((! [A:int]: ((power_power_int @ A @ (suc @ zero_zero_nat)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_241_power__Suc0__right)).
% 17.01/5.06 thf(1251,plain,((! [A:int]: ((power_power_int @ A @ (suc @ zero_zero_nat)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[281])).
% 17.01/5.06 thf(229,axiom,((! [A:num,B:num]: (((numeral_numeral_real @ A) = (numeral_numeral_real @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_60_numeral__eq__iff)).
% 17.01/5.06 thf(1103,plain,((! [A:num,B:num]: (((numeral_numeral_real @ A) = (numeral_numeral_real @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 17.01/5.06 thf(74,axiom,((! [A:nat]: ((suc @ A) != zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_328_Suc__neq__Zero)).
% 17.01/5.06 thf(601,plain,((! [A:nat]: ~ ((suc @ A) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 17.01/5.06 thf(193,axiom,((! [A:int,B:num,C:nat]: (((ring_1_of_int_real @ A) = (power_power_real @ (numeral_numeral_real @ B) @ C)) = (A = (power_power_int @ (numeral_numeral_int @ B) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_8_of__int__eq__numeral__power__cancel__iff)).
% 17.01/5.06 thf(1007,plain,((! [A:int,B:num,C:nat]: (((ring_1_of_int_real @ A) = (power_power_real @ (numeral_numeral_real @ B) @ C)) = (A = (power_power_int @ (numeral_numeral_int @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 17.01/5.06 thf(112,axiom,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat]: (A @ D @ zero_zero_nat)) => ((! [D:nat]: (A @ zero_zero_nat @ (suc @ D))) => ((! [D:nat,E:nat]: ((A @ D @ E) => (A @ (suc @ D) @ (suc @ E)))) => (A @ B @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_326_diff__induct)).
% 17.01/5.06 thf(732,plain,((! [A:(nat > (nat > $o)),B:nat,C:nat]: ((! [D:nat]: (A @ D @ zero_zero_nat)) => ((! [D:nat]: (A @ zero_zero_nat @ (suc @ D))) => ((! [D:nat,E:nat]: ((A @ D @ E) => (A @ (suc @ D) @ (suc @ E)))) => (A @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 17.01/5.06 thf(327,axiom,((! [A:int]: ((zero_zero_real = (ring_1_of_int_real @ A)) = (A = zero_zero_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_246_of__int__0__eq__iff)).
% 17.01/5.06 thf(1389,plain,((! [A:int]: ((zero_zero_real = (ring_1_of_int_real @ A)) = (A = zero_zero_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[327])).
% 17.01/5.06 thf(66,axiom,((! [A:nat,B:nat,C:real]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_real @ one_one_real @ C) => (ord_less_eq_real @ (power_power_real @ C @ A) @ (power_power_real @ C @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_211_power__increasing)).
% 17.01/5.06 thf(579,plain,((! [A:nat,B:nat,C:real]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_real @ one_one_real @ C) => (ord_less_eq_real @ (power_power_real @ C @ A) @ (power_power_real @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 17.01/5.06 thf(237,axiom,((! [A:int,B:nat]: ((A != zero_zero_int) => ((power_power_int @ A @ B) != zero_zero_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_316_power__not__zero)).
% 17.01/5.06 thf(1124,plain,((! [A:int,B:nat]: ((~ (A = zero_zero_int)) => (~ ((power_power_int @ A @ B) = zero_zero_int))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 17.01/5.06 thf(283,axiom,((! [A:int,B:num,C:nat]: (((ring_1_of_int_int @ A) = (power_power_int @ (numeral_numeral_int @ B) @ C)) = (A = (power_power_int @ (numeral_numeral_int @ B) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7_of__int__eq__numeral__power__cancel__iff)).
% 17.01/5.06 thf(1256,plain,((! [A:int,B:num,C:nat]: (((ring_1_of_int_int @ A) = (power_power_int @ (numeral_numeral_int @ B) @ C)) = (A = (power_power_int @ (numeral_numeral_int @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[283])).
% 17.01/5.06 thf(60,axiom,((! [A:real,B:nat]: ((ord_less_eq_real @ one_one_real @ A) => (ord_less_eq_real @ one_one_real @ (power_power_real @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_199_one__le__power)).
% 17.01/5.06 thf(562,plain,((! [A:real,B:nat]: ((ord_less_eq_real @ one_one_real @ A) => (ord_less_eq_real @ one_one_real @ (power_power_real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 17.01/5.06 thf(181,axiom,(((power_power_nat @ one_one_nat @ (numeral_numeral_nat @ (bit0 @ one))) = one_one_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_213_one__power2)).
% 17.01/5.06 thf(975,plain,(((power_power_nat @ one_one_nat @ (numeral_numeral_nat @ (bit0 @ one))) = one_one_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 17.01/5.06 thf(170,axiom,(((powr_real @ (numeral_numeral_real @ (bit0 @ one)) @ (semiri2110766477t_real @ (nat2 @ (archim1371465213g_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d)))))) = (ring_1_of_int_real @ (power_power_int @ (numeral_numeral_int @ (bit0 @ one)) @ (nat2 @ (archim1371465213g_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_102__092_060open_0622_Apowr_Areal_A_Inat_A_092_060lceil_062log_A2_A_Ireal__of__int_Ad_J_092_060rceil_062_J_A_061_Areal__of__int_A_I2_A_094_Anat_A_092_060lceil_062log_A2_A_Ireal__of__int_Ad_J_092_060rceil_062_J_092_060close_062)).
% 17.01/5.06 thf(936,plain,(((powr_real @ (numeral_numeral_real @ (bit0 @ one)) @ (semiri2110766477t_real @ (nat2 @ (archim1371465213g_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d)))))) = (ring_1_of_int_real @ (power_power_int @ (numeral_numeral_int @ (bit0 @ one)) @ (nat2 @ (archim1371465213g_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 17.01/5.06 thf(288,axiom,((! [A:num]: ((neg_numeral_dbl_int @ (numeral_numeral_int @ A)) = (numeral_numeral_int @ (bit0 @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_275_dbl__simps_I5_J)).
% 17.01/5.06 thf(1271,plain,((! [A:num]: ((neg_numeral_dbl_int @ (numeral_numeral_int @ A)) = (numeral_numeral_int @ (bit0 @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[288])).
% 17.01/5.06 thf(77,axiom,((! [A:num]: (ord_less_eq_num @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_223_order__refl)).
% 17.01/5.06 thf(611,plain,((! [A:num]: (ord_less_eq_num @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 17.01/5.06 thf(212,axiom,((! [A:int]: ((ord_less_eq_int @ (power_power_int @ A @ (numeral_numeral_nat @ (bit0 @ one))) @ zero_zero_int) = (A = zero_zero_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_289_power2__less__eq__zero__iff)).
% 17.01/5.06 thf(1058,plain,((! [A:int]: ((ord_less_eq_int @ (power_power_int @ A @ (numeral_numeral_nat @ (bit0 @ one))) @ zero_zero_int) = (A = zero_zero_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 17.01/5.06 thf(277,axiom,((! [A:real]: ((log @ A @ one_one_real) = zero_zero_real))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_273_log__one)).
% 17.01/5.06 thf(1239,plain,((! [A:real]: ((log @ A @ one_one_real) = zero_zero_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[277])).
% 17.01/5.06 thf(315,axiom,((! [A:num]: ((semiri2110766477t_real @ (numeral_numeral_nat @ A)) = (numeral_numeral_real @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_136_of__nat__numeral)).
% 17.01/5.06 thf(1356,plain,((! [A:num]: ((semiri2110766477t_real @ (numeral_numeral_nat @ A)) = (numeral_numeral_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[315])).
% 17.01/5.06 thf(53,axiom,((! [A:nat]: ((ord_less_eq_nat @ (semiri1382578993at_nat @ A) @ zero_zero_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_261_of__nat__le__0__iff)).
% 17.01/5.06 thf(540,plain,((! [A:nat]: ((ord_less_eq_nat @ (semiri1382578993at_nat @ A) @ zero_zero_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 17.01/5.06 thf(164,axiom,(((suc @ one_one_nat) = (numeral_numeral_nat @ (bit0 @ one)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_147_Suc__1)).
% 17.01/5.06 thf(919,plain,(((suc @ one_one_nat) = (numeral_numeral_nat @ (bit0 @ one)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 17.01/5.06 thf(133,axiom,(((semiri2019852685at_int @ zero_zero_nat) = zero_zero_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_293_int__ops_I1_J)).
% 17.01/5.06 thf(804,plain,(((semiri2019852685at_int @ zero_zero_nat) = zero_zero_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 17.01/5.06 thf(183,axiom,((! [A:int]: ((ord_less_eq_real @ zero_zero_real @ (ring_1_of_int_real @ A)) = (ord_less_eq_int @ zero_zero_int @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_278_of__int__0__le__iff)).
% 17.01/5.06 thf(979,plain,((! [A:int]: ((ord_less_eq_real @ zero_zero_real @ (ring_1_of_int_real @ A)) = (ord_less_eq_int @ zero_zero_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 17.01/5.06 thf(234,axiom,(((archim1371465213g_real @ one_one_real) = one_one_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_68_ceiling__one)).
% 17.01/5.06 thf(1117,plain,(((archim1371465213g_real @ one_one_real) = one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 17.01/5.06 thf(12,axiom,((! [A:num]: ((semiri1382578993at_nat @ (numeral_numeral_nat @ A)) = (numeral_numeral_nat @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_135_of__nat__numeral)).
% 17.01/5.06 thf(377,plain,((! [A:num]: ((semiri1382578993at_nat @ (numeral_numeral_nat @ A)) = (numeral_numeral_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 17.01/5.06 thf(244,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (power_power_nat @ A @ (numeral_numeral_nat @ (bit0 @ one))) @ (power_power_nat @ B @ (numeral_numeral_nat @ (bit0 @ one)))) = (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_107_power2__nat__le__eq__le)).
% 17.01/5.06 thf(1144,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (power_power_nat @ A @ (numeral_numeral_nat @ (bit0 @ one))) @ (power_power_nat @ B @ (numeral_numeral_nat @ (bit0 @ one)))) = (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 17.01/5.06 thf(113,axiom,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_335_bot__nat__0_Oextremum__unique)).
% 17.01/5.06 thf(737,plain,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 17.01/5.06 thf(27,axiom,(((semiri2019852685at_int @ one_one_nat) = one_one_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_128_of__nat__1)).
% 17.01/5.06 thf(434,plain,(((semiri2019852685at_int @ one_one_nat) = one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 17.01/5.06 thf(344,axiom,((! [A:real,B:int]: ((ord_less_eq_int @ (archim1371465213g_real @ A) @ B) = (ord_less_eq_real @ A @ (ring_1_of_int_real @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_44_ceiling__le__iff)).
% 17.01/5.06 thf(1439,plain,((! [A:real,B:int]: ((ord_less_eq_int @ (archim1371465213g_real @ A) @ B) = (ord_less_eq_real @ A @ (ring_1_of_int_real @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[344])).
% 17.01/5.06 thf(148,axiom,((! [A:nat,B:nat]: ((A = B) | ~ (ord_less_eq_nat @ A @ B) | ~ (ord_less_eq_nat @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_94_verit__la__disequality)).
% 17.01/5.06 thf(863,plain,((! [A:nat,B:nat]: ((A = B) | ~ (ord_less_eq_nat @ A @ B) | ~ (ord_less_eq_nat @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 17.01/5.06 thf(35,axiom,((! [A:$o,B:nat,C:nat]: (((A) => ((semiri2019852685at_int @ (if_nat @ A @ B @ C)) = (semiri2019852685at_int @ B))) & ((~ (A)) => ((semiri2019852685at_int @ (if_nat @ A @ B @ C)) = (semiri2019852685at_int @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_291_int__if)).
% 17.01/5.06 thf(477,plain,((! [A:$o,B:nat,C:nat]: (((A) => ((semiri2019852685at_int @ (if_nat @ A @ B @ C)) = (semiri2019852685at_int @ B))) & ((~ (A)) => ((semiri2019852685at_int @ (if_nat @ A @ B @ C)) = (semiri2019852685at_int @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 17.01/5.06 thf(84,axiom,((! [A:real,B:real,C:real]: ((powr_real @ (powr_real @ A @ B) @ C) = (powr_real @ (powr_real @ A @ C) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_184_powr__powr__swap)).
% 17.01/5.06 thf(631,plain,((! [A:real,B:real,C:real]: ((powr_real @ (powr_real @ A @ B) @ C) = (powr_real @ (powr_real @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 17.01/5.06 thf(142,axiom,((! [A:nat]: ((zero_zero_real = (semiri2110766477t_real @ A)) = (zero_zero_nat = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_236_of__nat__0__eq__iff)).
% 17.01/5.06 thf(848,plain,((! [A:nat]: ((zero_zero_real = (semiri2110766477t_real @ A)) = (zero_zero_nat = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 17.01/5.06 thf(94,axiom,((! [A:(nat > $o),B:nat]: ((A @ B) => ((! [C:nat]: ((A @ (suc @ C)) => (A @ C))) => (A @ zero_zero_nat))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_327_zero__induct)).
% 17.01/5.06 thf(668,plain,((! [A:(nat > $o),B:nat]: ((A @ B) => ((! [C:nat]: ((A @ (suc @ C)) => (A @ C))) => (A @ zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 17.01/5.06 thf(324,axiom,((ord_less_eq_int @ zero_zero_int @ zero_zero_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_338_less__eq__int__code_I1_J)).
% 17.01/5.06 thf(1381,plain,((ord_less_eq_int @ zero_zero_int @ zero_zero_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[324])).
% 17.01/5.06 thf(232,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_int @ (semiri2019852685at_int @ A) @ (semiri2019852685at_int @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_170_of__nat__mono)).
% 17.01/5.06 thf(1112,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_int @ (semiri2019852685at_int @ A) @ (semiri2019852685at_int @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 17.01/5.06 thf(250,axiom,((! [A:int]: ((ord_less_eq_int @ zero_zero_int @ A) => ((semiri2110766477t_real @ (nat2 @ A)) = (ring_1_of_int_real @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_284_of__nat__nat)).
% 17.01/5.06 thf(1162,plain,((! [A:int]: ((ord_less_eq_int @ zero_zero_int @ A) => ((semiri2110766477t_real @ (nat2 @ A)) = (ring_1_of_int_real @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 17.01/5.06 thf(110,axiom,((! [A:nat]: (zero_zero_nat != (suc @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_330_Zero__not__Suc)).
% 17.01/5.06 thf(726,plain,((! [A:nat]: ~ (zero_zero_nat = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 17.01/5.06 thf(169,axiom,((! [A:int,B:int]: ((ord_less_eq_int @ zero_zero_int @ A) => ((ord_less_eq_int @ zero_zero_int @ B) => (((nat2 @ A) = (nat2 @ B)) = (A = B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_345_eq__nat__nat__iff)).
% 17.01/5.06 thf(932,plain,((! [A:int,B:int]: ((ord_less_eq_int @ zero_zero_int @ A) => ((ord_less_eq_int @ zero_zero_int @ B) => (((nat2 @ A) = (nat2 @ B)) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 17.01/5.06 thf(213,axiom,((! [A:num]: ((ring_1_of_int_real @ (numeral_numeral_int @ A)) = (numeral_numeral_real @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_30_of__int__numeral)).
% 17.01/5.06 thf(1061,plain,((! [A:num]: ((ring_1_of_int_real @ (numeral_numeral_int @ A)) = (numeral_numeral_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 17.01/5.06 thf(97,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_178_nat__le__linear)).
% 17.01/5.06 thf(685,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)],[97])).
% 17.01/5.06 thf(122,axiom,((! [A:nat]: ((ring_1_of_int_int @ (semiri2019852685at_int @ A)) = (semiri2019852685at_int @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_130_of__int__of__nat__eq)).
% 17.01/5.06 thf(768,plain,((! [A:nat]: ((ring_1_of_int_int @ (semiri2019852685at_int @ A)) = (semiri2019852685at_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 17.01/5.06 thf(215,axiom,((! [A:num]: (ord_less_eq_real @ one_one_real @ (numeral_numeral_real @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_89_one__le__numeral)).
% 17.01/5.06 thf(1066,plain,((! [A:num]: (ord_less_eq_real @ one_one_real @ (numeral_numeral_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 17.01/5.06 thf(126,axiom,((! [A:int,B:int]: (((ring_1_of_int_int @ A) = (ring_1_of_int_int @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_23_of__int__eq__iff)).
% 17.01/5.06 thf(780,plain,((! [A:int,B:int]: (((ring_1_of_int_int @ A) = (ring_1_of_int_int @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 17.01/5.06 thf(318,axiom,((! [A:real,B:int]: ((ord_less_eq_real @ A @ (ring_1_of_int_real @ B)) => (ord_less_eq_int @ (archim1371465213g_real @ A) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_45_ceiling__le)).
% 17.01/5.06 thf(1364,plain,((! [A:real,B:int]: ((ord_less_eq_real @ A @ (ring_1_of_int_real @ B)) => (ord_less_eq_int @ (archim1371465213g_real @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[318])).
% 17.01/5.06 thf(143,axiom,((! [A:num,B:nat,C:nat]: ((ord_less_eq_nat @ (power_power_nat @ (numeral_numeral_nat @ A) @ B) @ (semiri1382578993at_nat @ C)) = (ord_less_eq_nat @ (power_power_nat @ (numeral_numeral_nat @ A) @ B) @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_166_numeral__power__le__of__nat__cancel__iff)).
% 17.01/5.06 thf(851,plain,((! [A:num,B:nat,C:nat]: ((ord_less_eq_nat @ (power_power_nat @ (numeral_numeral_nat @ A) @ B) @ (semiri1382578993at_nat @ C)) = (ord_less_eq_nat @ (power_power_nat @ (numeral_numeral_nat @ A) @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 17.01/5.06 thf(43,axiom,((! [A:nat]: ((one_one_real = (semiri2110766477t_real @ A)) = (A = one_one_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_124_of__nat__1__eq__iff)).
% 17.01/5.06 thf(505,plain,((! [A:nat]: ((one_one_real = (semiri2110766477t_real @ A)) = (A = one_one_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 17.01/5.06 thf(26,axiom,((! [A:num,B:num]: ((power_power_nat @ (numeral_numeral_nat @ A) @ (numeral_numeral_nat @ B)) = (numeral_numeral_nat @ (pow @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_219_power__numeral)).
% 17.01/5.06 thf(431,plain,((! [A:num,B:num]: ((power_power_nat @ (numeral_numeral_nat @ A) @ (numeral_numeral_nat @ B)) = (numeral_numeral_nat @ (pow @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 17.01/5.06 thf(89,axiom,((! [A:real,B:real]: ((A = B) | ~ (ord_less_eq_real @ A @ B) | ~ (ord_less_eq_real @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_95_verit__la__disequality)).
% 17.01/5.06 thf(653,plain,((! [A:real,B:real]: ((A = B) | ~ (ord_less_eq_real @ A @ B) | ~ (ord_less_eq_real @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 17.01/5.06 thf(100,axiom,(((semiri2110766477t_real @ zero_zero_nat) = zero_zero_real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_233_of__nat__0)).
% 17.01/5.06 thf(695,plain,(((semiri2110766477t_real @ zero_zero_nat) = zero_zero_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 17.01/5.06 thf(279,axiom,((! [A:int,B:int]: ((ord_less_eq_int @ (ring_1_of_int_int @ A) @ (ring_1_of_int_int @ B)) = (ord_less_eq_int @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_27_of__int__le__iff)).
% 17.01/5.06 thf(1245,plain,((! [A:int,B:int]: ((ord_less_eq_int @ (ring_1_of_int_int @ A) @ (ring_1_of_int_int @ B)) = (ord_less_eq_int @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[279])).
% 17.01/5.06 thf(255,axiom,((! [A:int,B:num]: ((ord_less_eq_real @ (ring_1_of_int_real @ A) @ (numeral_numeral_real @ B)) = (ord_less_eq_int @ A @ (numeral_numeral_int @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_15_of__int__le__numeral__iff)).
% 17.01/5.06 thf(1176,plain,((! [A:int,B:num]: ((ord_less_eq_real @ (ring_1_of_int_real @ A) @ (numeral_numeral_real @ B)) = (ord_less_eq_int @ A @ (numeral_numeral_int @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 17.01/5.06 thf(76,axiom,((! [A:num]: ((power_power_real @ zero_zero_real @ (numeral_numeral_nat @ A)) = zero_zero_real))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_268_power__zero__numeral)).
% 17.01/5.06 thf(608,plain,((! [A:num]: ((power_power_real @ zero_zero_real @ (numeral_numeral_nat @ A)) = zero_zero_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 17.01/5.06 thf(37,axiom,((! [A:nat]: ((zero_zero_nat = A) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_300_zero__reorient)).
% 17.01/5.06 thf(490,plain,((! [A:nat]: ((zero_zero_nat = A) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 17.01/5.06 thf(265,axiom,((! [A:int,B:int]: ((ord_less_eq_int @ zero_zero_int @ A) => ((ord_less_eq_int @ zero_zero_int @ B) => (((power_power_int @ A @ (numeral_numeral_nat @ (bit0 @ one))) = (power_power_int @ B @ (numeral_numeral_nat @ (bit0 @ one)))) = (A = B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_225_power2__eq__iff__nonneg)).
% 17.01/5.06 thf(1203,plain,((! [A:int,B:int]: ((ord_less_eq_int @ zero_zero_int @ A) => ((ord_less_eq_int @ zero_zero_int @ B) => (((power_power_int @ A @ (numeral_numeral_nat @ (bit0 @ one))) = (power_power_int @ B @ (numeral_numeral_nat @ (bit0 @ one)))) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[265])).
% 17.01/5.06 thf(50,axiom,((! [A:num]: (ord_less_eq_nat @ one_one_nat @ (numeral_numeral_nat @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_88_one__le__numeral)).
% 17.01/5.06 thf(531,plain,((! [A:num]: (ord_less_eq_nat @ one_one_nat @ (numeral_numeral_nat @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 17.01/5.06 thf(290,axiom,((! [A:real,B:num]: ((ord_less_eq_real @ zero_zero_real @ A) => ((powr_real @ A @ (numeral_numeral_real @ B)) = (power_power_real @ A @ (numeral_numeral_nat @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_224_powr__numeral)).
% 17.01/5.06 thf(1277,plain,((! [A:real,B:num]: ((ord_less_eq_real @ zero_zero_real @ A) => ((powr_real @ A @ (numeral_numeral_real @ B)) = (power_power_real @ A @ (numeral_numeral_nat @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[290])).
% 17.01/5.06 thf(241,axiom,((! [A:nat]: (ord_less_eq_real @ one_one_real @ (power_power_real @ (numeral_numeral_real @ (bit0 @ one)) @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_98_two__realpow__ge__one)).
% 17.01/5.06 thf(1134,plain,((! [A:nat]: (ord_less_eq_real @ one_one_real @ (power_power_real @ (numeral_numeral_real @ (bit0 @ one)) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 17.01/5.06 thf(136,axiom,((! [A:(nat > num),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_num @ (A @ (suc @ D)) @ (A @ D))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_num @ (A @ C) @ (A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_203_lift__Suc__antimono__le)).
% 17.01/5.06 thf(812,plain,((! [A:(nat > num),B:nat,C:nat]: ((! [D:nat]: (ord_less_eq_num @ (A @ (suc @ D)) @ (A @ D))) => ((ord_less_eq_nat @ B @ C) => (ord_less_eq_num @ (A @ C) @ (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 17.01/5.06 thf(79,axiom,(((semiri2019852685at_int @ one_one_nat) = one_one_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_309_int__ops_I2_J)).
% 17.01/5.06 thf(617,plain,(((semiri2019852685at_int @ one_one_nat) = one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 17.01/5.06 thf(57,axiom,((! [A:nat]: ((ord_less_eq_real @ (semiri2110766477t_real @ A) @ zero_zero_real) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_262_of__nat__le__0__iff)).
% 17.01/5.06 thf(553,plain,((! [A:nat]: ((ord_less_eq_real @ (semiri2110766477t_real @ A) @ zero_zero_real) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 17.01/5.06 thf(140,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_177_Nat_Oex__has__greatest__nat)).
% 17.01/5.06 thf(823,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)],[140])).
% 17.01/5.06 thf(209,axiom,((! [A:num]: ~ (ord_less_eq_num @ (bit0 @ A) @ one))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_47_semiring__norm_I69_J)).
% 17.01/5.06 thf(1049,plain,((! [A:num]: ~ (ord_less_eq_num @ (bit0 @ A) @ one))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 17.01/5.06 thf(335,axiom,(((neg_numeral_dbl_real @ one_one_real) = (numeral_numeral_real @ (bit0 @ one)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_216_dbl__simps_I3_J)).
% 17.01/5.06 thf(1413,plain,(((neg_numeral_dbl_real @ one_one_real) = (numeral_numeral_real @ (bit0 @ one)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[335])).
% 17.01/5.06 thf(219,axiom,((! [A:int]: (ord_less_eq_int @ A @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_220_order__refl)).
% 17.01/5.06 thf(1076,plain,((! [A:int]: (ord_less_eq_int @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 17.01/5.06 thf(167,axiom,(((neg_numeral_dbl_int @ one_one_int) = (numeral_numeral_int @ (bit0 @ one)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_215_dbl__simps_I3_J)).
% 17.01/5.06 thf(927,plain,(((neg_numeral_dbl_int @ one_one_int) = (numeral_numeral_int @ (bit0 @ one)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 17.01/5.06 thf(11,axiom,((! [A:nat,B:nat,C:nat]: (((power_power_nat @ (semiri1382578993at_nat @ A) @ B) = (semiri1382578993at_nat @ C)) = ((power_power_nat @ A @ B) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_141_of__nat__eq__of__nat__power__cancel__iff)).
% 17.01/5.06 thf(374,plain,((! [A:nat,B:nat,C:nat]: (((power_power_nat @ (semiri1382578993at_nat @ A) @ B) = (semiri1382578993at_nat @ C)) = ((power_power_nat @ A @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 17.01/5.06 thf(48,axiom,((! [A:nat,B:nat]: (((semiri2019852685at_int @ A) = (semiri2019852685at_int @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_296_int__int__eq)).
% 17.01/5.06 thf(525,plain,((! [A:nat,B:nat]: (((semiri2019852685at_int @ A) = (semiri2019852685at_int @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 17.01/5.06 thf(106,axiom,((! [A:nat]: (A != (suc @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_176_n__not__Suc__n)).
% 17.01/5.06 thf(712,plain,((! [A:nat]: ~ (A = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 17.01/5.06 thf(145,axiom,((! [A:real]: ? [B:nat]: (ord_less_eq_real @ A @ (semiri2110766477t_real @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_169_real__arch__simple)).
% 17.01/5.06 thf(855,plain,((! [A:real]: ? [B:nat]: (ord_less_eq_real @ A @ (semiri2110766477t_real @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 17.01/5.06 thf(87,axiom,(((semiri2019852685at_int @ zero_zero_nat) = zero_zero_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_234_of__nat__0)).
% 17.01/5.06 thf(640,plain,(((semiri2019852685at_int @ zero_zero_nat) = zero_zero_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 17.01/5.06 thf(217,axiom,((! [A:int,B:int]: ((ord_less_eq_real @ (ring_1_of_int_real @ A) @ (ring_1_of_int_real @ B)) = (ord_less_eq_int @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_28_of__int__le__iff)).
% 17.01/5.06 thf(1070,plain,((! [A:int,B:int]: ((ord_less_eq_real @ (ring_1_of_int_real @ A) @ (ring_1_of_int_real @ B)) = (ord_less_eq_int @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 17.01/5.06 thf(272,axiom,((! [A:num]: ((one_one_nat = (numeral_numeral_nat @ A)) = (one = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_74_one__eq__numeral__iff)).
% 17.01/5.06 thf(1225,plain,((! [A:num]: ((one_one_nat = (numeral_numeral_nat @ A)) = (one = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[272])).
% 17.01/5.06 thf(23,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ one_one_nat @ C) => (ord_less_eq_nat @ (power_power_nat @ C @ A) @ (power_power_nat @ C @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_210_power__increasing)).
% 17.01/5.06 thf(414,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_nat @ A @ B) => ((ord_less_eq_nat @ one_one_nat @ C) => (ord_less_eq_nat @ (power_power_nat @ C @ A) @ (power_power_nat @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 17.01/5.06 thf(274,axiom,((! [A:int,B:num,C:nat]: ((ord_less_eq_nat @ (nat2 @ A) @ (power_power_nat @ (numeral_numeral_nat @ B) @ C)) = (ord_less_eq_int @ A @ (power_power_int @ (numeral_numeral_int @ B) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_39_nat__le__numeral__power__cancel__iff)).
% 17.01/5.06 thf(1230,plain,((! [A:int,B:num,C:nat]: ((ord_less_eq_nat @ (nat2 @ A) @ (power_power_nat @ (numeral_numeral_nat @ B) @ C)) = (ord_less_eq_int @ A @ (power_power_int @ (numeral_numeral_int @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 17.01/5.06 thf(104,axiom,((! [A:nat]: (zero_zero_nat != (suc @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_320_nat_Odistinct_I1_J)).
% 17.01/5.06 thf(705,plain,((! [A:nat]: ~ (zero_zero_nat = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 17.01/5.06 thf(248,axiom,((! [A:nat]: ((power_power_int @ one_one_int @ A) = one_one_int))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_117_power__one)).
% 17.01/5.06 thf(1156,plain,((! [A:nat]: ((power_power_int @ one_one_int @ A) = one_one_int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 17.01/5.06 thf(42,axiom,((! [A:real,B:real]: (((powr_real @ A @ B) = zero_zero_real) = (A = zero_zero_real)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_250_powr__eq__0__iff)).
% 17.01/5.06 thf(502,plain,((! [A:real,B:real]: (((powr_real @ A @ B) = zero_zero_real) = (A = zero_zero_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 17.01/5.06 thf(285,axiom,((! [A:num,B:nat,C:int]: (((power_power_int @ (numeral_numeral_int @ A) @ B) = (ring_1_of_int_int @ C)) = ((power_power_int @ (numeral_numeral_int @ A) @ B) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_numeral__power__eq__of__int__cancel__iff)).
% 17.01/5.06 thf(1262,plain,((! [A:num,B:nat,C:int]: (((power_power_int @ (numeral_numeral_int @ A) @ B) = (ring_1_of_int_int @ C)) = ((power_power_int @ (numeral_numeral_int @ A) @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[285])).
% 17.01/5.06 thf(303,axiom,((((?) @ nat) = (^ [A:(nat > $o)]: ? [B:int]: ((ord_less_eq_int @ zero_zero_int @ B) & (A @ (nat2 @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_343_ex__nat)).
% 17.01/5.06 thf(1317,plain,((((?) @ nat) = (^ [A:(nat > $o)]: ? [B:int]: ((ord_less_eq_int @ zero_zero_int @ B) & (A @ (nat2 @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[303])).
% 17.01/5.06 thf(175,axiom,((! [A:nat]: (((A = zero_zero_nat) => ((power_power_int @ zero_zero_int @ A) = one_one_int)) & ((A != zero_zero_nat) => ((power_power_int @ zero_zero_int @ A) = zero_zero_int))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_304_power__0__left)).
% 17.01/5.06 thf(951,plain,((! [A:nat]: (((A = zero_zero_nat) => ((power_power_int @ zero_zero_int @ A) = one_one_int)) & ((~ (A = zero_zero_nat)) => ((power_power_int @ zero_zero_int @ A) = zero_zero_int))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 17.01/5.06 thf(308,axiom,(((numeral_numeral_int @ one) = one_one_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_90_numeral__One)).
% 17.01/5.06 thf(1336,plain,(((numeral_numeral_int @ one) = one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[308])).
% 17.01/5.06 thf(270,axiom,((! [A:int]: ((ord_less_eq_int @ (ring_1_of_int_int @ A) @ zero_zero_int) = (ord_less_eq_int @ A @ zero_zero_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_279_of__int__le__0__iff)).
% 17.01/5.06 thf(1220,plain,((! [A:int]: ((ord_less_eq_int @ (ring_1_of_int_int @ A) @ zero_zero_int) = (ord_less_eq_int @ A @ zero_zero_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 17.01/5.06 thf(160,axiom,((! [A:num,B:nat,C:nat]: (((power_power_real @ (numeral_numeral_real @ A) @ B) = (semiri2110766477t_real @ C)) = ((power_power_nat @ (numeral_numeral_nat @ A) @ B) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_158_numeral__power__eq__of__nat__cancel__iff)).
% 17.01/5.06 thf(907,plain,((! [A:num,B:nat,C:nat]: (((power_power_real @ (numeral_numeral_real @ A) @ B) = (semiri2110766477t_real @ C)) = ((power_power_nat @ (numeral_numeral_nat @ A) @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 17.01/5.06 thf(204,axiom,((! [A:nat,B:num,C:nat]: ((ord_less_eq_real @ (semiri2110766477t_real @ A) @ (power_power_real @ (numeral_numeral_real @ B) @ C)) = (ord_less_eq_nat @ A @ (power_power_nat @ (numeral_numeral_nat @ B) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_164_of__nat__le__numeral__power__cancel__iff)).
% 17.01/5.06 thf(1038,plain,((! [A:nat,B:num,C:nat]: ((ord_less_eq_real @ (semiri2110766477t_real @ A) @ (power_power_real @ (numeral_numeral_real @ B) @ C)) = (ord_less_eq_nat @ A @ (power_power_nat @ (numeral_numeral_nat @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 17.01/5.06 thf(68,axiom,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_228_le0)).
% 17.01/5.06 thf(585,plain,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 17.01/5.06 thf(222,axiom,((! [A:nat,B:int]: (((semiri2019852685at_int @ A) = B) = ((A = (nat2 @ B)) & (ord_less_eq_int @ zero_zero_int @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_308_int__eq__iff)).
% 17.01/5.06 thf(1085,plain,((! [A:nat,B:int]: (((semiri2019852685at_int @ A) = B) = ((A = (nat2 @ B)) & (ord_less_eq_int @ zero_zero_int @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 17.01/5.06 thf(65,axiom,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_real @ (semiri2110766477t_real @ A) @ (power_power_real @ (semiri2110766477t_real @ B) @ C)) = (ord_less_eq_nat @ A @ (power_power_nat @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_150_of__nat__power__le__of__nat__cancel__iff)).
% 17.01/5.06 thf(576,plain,((! [A:nat,B:nat,C:nat]: ((ord_less_eq_real @ (semiri2110766477t_real @ A) @ (power_power_real @ (semiri2110766477t_real @ B) @ C)) = (ord_less_eq_nat @ A @ (power_power_nat @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 17.01/5.06 thf(332,axiom,((! [A:int,B:num]: (((ring_1_of_int_int @ A) = (numeral_numeral_int @ B)) = (A = (numeral_numeral_int @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_31_of__int__eq__numeral__iff)).
% 17.01/5.06 thf(1404,plain,((! [A:int,B:num]: (((ring_1_of_int_int @ A) = (numeral_numeral_int @ B)) = (A = (numeral_numeral_int @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[332])).
% 17.01/5.06 thf(116,axiom,((! [A:real]: (((A = zero_zero_real) => ((powr_real @ A @ zero_zero_real) = zero_zero_real)) & ((A != zero_zero_real) => ((powr_real @ A @ zero_zero_real) = one_one_real))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_269_powr__zero__eq__one)).
% 17.01/5.06 thf(744,plain,((! [A:real]: (((A = zero_zero_real) => ((powr_real @ A @ zero_zero_real) = zero_zero_real)) & ((~ (A = zero_zero_real)) => ((powr_real @ A @ zero_zero_real) = one_one_real))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 17.01/5.06 thf(90,axiom,((! [A:nat,B:nat]: ((A = (suc @ B)) => (A != zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_323_nat_OdiscI)).
% 17.01/5.06 thf(656,plain,((! [A:nat,B:nat]: ((A = (suc @ B)) => (~ (A = zero_zero_nat))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 17.01/5.06 thf(78,axiom,((! [A:nat]: (zero_zero_nat != (suc @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_329_Zero__neq__Suc)).
% 17.01/5.06 thf(613,plain,((! [A:nat]: ~ (zero_zero_nat = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 17.01/5.06 thf(292,axiom,((! [A:real]: ((ord_less_eq_real @ (power_power_real @ A @ (numeral_numeral_nat @ (bit0 @ one))) @ zero_zero_real) = (A = zero_zero_real)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_290_power2__less__eq__zero__iff)).
% 17.01/5.06 thf(1284,plain,((! [A:real]: ((ord_less_eq_real @ (power_power_real @ A @ (numeral_numeral_nat @ (bit0 @ one))) @ zero_zero_real) = (A = zero_zero_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[292])).
% 17.01/5.06 thf(314,axiom,((! [A:int,B:num]: ((ord_less_eq_int @ (ring_1_of_int_int @ A) @ (numeral_numeral_int @ B)) = (ord_less_eq_int @ A @ (numeral_numeral_int @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_14_of__int__le__numeral__iff)).
% 17.01/5.06 thf(1353,plain,((! [A:int,B:num]: ((ord_less_eq_int @ (ring_1_of_int_int @ A) @ (numeral_numeral_int @ B)) = (ord_less_eq_int @ A @ (numeral_numeral_int @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[314])).
% 17.01/5.06 thf(210,axiom,((! [A:int,B:nat,C:int]: ((ord_less_eq_int @ (power_power_int @ (ring_1_of_int_int @ A) @ B) @ (ring_1_of_int_int @ C)) = (ord_less_eq_int @ (power_power_int @ A @ B) @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9_of__int__le__of__int__power__cancel__iff)).
% 17.01/5.06 thf(1052,plain,((! [A:int,B:nat,C:int]: ((ord_less_eq_int @ (power_power_int @ (ring_1_of_int_int @ A) @ B) @ (ring_1_of_int_int @ C)) = (ord_less_eq_int @ (power_power_int @ A @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 17.01/5.06 thf(340,axiom,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) | (A = B) | (ord_less_eq_int @ B @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_99_verit__la__generic)).
% 17.01/5.06 thf(1427,plain,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) | (A = B) | (ord_less_eq_int @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[340])).
% 17.01/5.06 thf(243,axiom,((! [A:int]: ((ord_less_eq_int @ zero_zero_int @ A) => (~ (! [B:nat]: (A != (semiri2019852685at_int @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_295_nonneg__int__cases)).
% 17.01/5.06 thf(1140,plain,((! [A:int]: ((ord_less_eq_int @ zero_zero_int @ A) => (~ (! [B:nat]: ~ (A = (semiri2019852685at_int @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 17.01/5.06 thf(321,axiom,((! [A:nat,B:num,C:nat]: ((ord_less_eq_int @ (semiri2019852685at_int @ A) @ (power_power_int @ (numeral_numeral_int @ B) @ C)) = (ord_less_eq_nat @ A @ (power_power_nat @ (numeral_numeral_nat @ B) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_162_of__nat__le__numeral__power__cancel__iff)).
% 17.01/5.06 thf(1372,plain,((! [A:nat,B:num,C:nat]: ((ord_less_eq_int @ (semiri2019852685at_int @ A) @ (power_power_int @ (numeral_numeral_int @ B) @ C)) = (ord_less_eq_nat @ A @ (power_power_nat @ (numeral_numeral_nat @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[321])).
% 17.01/5.06 thf(187,axiom,((! [A:nat,B:nat]: ((ord_less_eq_int @ (semiri2019852685at_int @ A) @ (semiri2019852685at_int @ B)) = (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_132_of__nat__le__iff)).
% 17.01/5.06 thf(991,plain,((! [A:nat,B:nat]: ((ord_less_eq_int @ (semiri2019852685at_int @ A) @ (semiri2019852685at_int @ B)) = (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 17.01/5.06 thf(29,axiom,((! [A:real]: ((ord_less_eq_real @ zero_zero_real @ A) => ((powr_real @ A @ one_one_real) = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_282_powr__one)).
% 17.01/5.06 thf(446,plain,((! [A:real]: ((ord_less_eq_real @ zero_zero_real @ A) => ((powr_real @ A @ one_one_real) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 17.01/5.06 thf(63,axiom,((! [A:num]: ((power_power_nat @ zero_zero_nat @ (numeral_numeral_nat @ A)) = zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_267_power__zero__numeral)).
% 17.01/5.06 thf(571,plain,((! [A:num]: ((power_power_nat @ zero_zero_nat @ (numeral_numeral_nat @ A)) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 17.01/5.06 thf(40,axiom,(((ring_1_of_int_int @ zero_zero_int) = zero_zero_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_245_of__int__0)).
% 17.01/5.06 thf(497,plain,(((ring_1_of_int_int @ zero_zero_int) = zero_zero_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 17.01/5.06 thf(153,axiom,((! [A:int]: (((ring_1_of_int_int @ A) = zero_zero_int) = (A = zero_zero_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_249_of__int__eq__0__iff)).
% 17.01/5.06 thf(876,plain,((! [A:int]: (((ring_1_of_int_int @ A) = zero_zero_int) = (A = zero_zero_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 17.01/5.06 thf(338,axiom,((! [A:num]: (((numeral_numeral_nat @ A) = one_one_nat) = (A = one)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_71_numeral__eq__one__iff)).
% 17.01/5.06 thf(1421,plain,((! [A:num]: (((numeral_numeral_nat @ A) = one_one_nat) = (A = one)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[338])).
% 17.01/5.06 thf(348,axiom,((! [A:num,B:num]: (((numeral_numeral_int @ A) = (numeral_numeral_int @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_59_numeral__eq__iff)).
% 17.01/5.06 thf(1448,plain,((! [A:num,B:num]: (((numeral_numeral_int @ A) = (numeral_numeral_int @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[348])).
% 17.01/5.06 thf(194,axiom,((! [A:int]: ((ord_less_eq_int @ zero_zero_int @ A) => ((semiri2019852685at_int @ (nat2 @ A)) = (ring_1_of_int_int @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_285_of__nat__nat)).
% 17.01/5.06 thf(1010,plain,((! [A:int]: ((ord_less_eq_int @ zero_zero_int @ A) => ((semiri2019852685at_int @ (nat2 @ A)) = (ring_1_of_int_int @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 17.01/5.06 thf(123,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ one_one_real @ C) => (ord_less_eq_real @ (powr_real @ C @ A) @ (powr_real @ C @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_208_powr__mono)).
% 17.01/5.06 thf(771,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ one_one_real @ C) => (ord_less_eq_real @ (powr_real @ C @ A) @ (powr_real @ C @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 17.01/5.06 thf(7,axiom,((! [A:nat]: ((one_one_nat = (semiri1382578993at_nat @ A)) = (A = one_one_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_123_of__nat__1__eq__iff)).
% 17.01/5.06 thf(363,plain,((! [A:nat]: ((one_one_nat = (semiri1382578993at_nat @ A)) = (A = one_one_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 17.01/5.06 thf(58,axiom,((! [A:nat]: ((power_power_nat @ A @ one_one_nat) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_111_power__one__right)).
% 17.01/5.06 thf(556,plain,((! [A:nat]: ((power_power_nat @ A @ one_one_nat) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 17.01/5.06 thf(102,axiom,((! [A:nat,B:nat]: (((semiri2110766477t_real @ A) = (semiri2110766477t_real @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_115_of__nat__eq__iff)).
% 17.01/5.06 thf(699,plain,((! [A:nat,B:nat]: (((semiri2110766477t_real @ A) = (semiri2110766477t_real @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 17.01/5.06 thf(326,axiom,((! [A:num]: (one != (bit0 @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_100_verit__eq__simplify_I10_J)).
% 17.01/5.06 thf(1385,plain,((! [A:num]: ~ (one = (bit0 @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[326])).
% 17.01/5.06 thf(177,axiom,((! [A:int]: ((ord_less_eq_int @ zero_zero_int @ (ring_1_of_int_int @ A)) = (ord_less_eq_int @ zero_zero_int @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_277_of__int__0__le__iff)).
% 17.01/5.06 thf(963,plain,((! [A:int]: ((ord_less_eq_int @ zero_zero_int @ (ring_1_of_int_int @ A)) = (ord_less_eq_int @ zero_zero_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 17.01/5.06 thf(1,conjecture,((ord_less_eq_int @ d @ (power_power_int @ (numeral_numeral_int @ (bit0 @ one)) @ (nat2 @ (archim1371465213g_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 17.01/5.06 thf(2,negated_conjecture,((~ (ord_less_eq_int @ d @ (power_power_int @ (numeral_numeral_int @ (bit0 @ one)) @ (nat2 @ (archim1371465213g_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d)))))))),inference(neg_conjecture,[status(cth)],[1])).
% 17.01/5.06 thf(351,plain,((~ (ord_less_eq_int @ d @ (power_power_int @ (numeral_numeral_int @ (bit0 @ one)) @ (nat2 @ (archim1371465213g_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 17.01/5.06 thf(17,axiom,((! [A:nat]: ((A != zero_zero_nat) => (? [B:nat]: (A = (suc @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_333_not0__implies__Suc)).
% 17.01/5.06 thf(390,plain,((! [A:nat]: ((~ (A = zero_zero_nat)) => (? [B:nat]: (A = (suc @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 17.01/5.06 thf(128,axiom,((! [A:nat]: ((power_power_nat @ A @ (suc @ zero_zero_nat)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_242_power__Suc0__right)).
% 17.01/5.06 thf(786,plain,((! [A:nat]: ((power_power_nat @ A @ (suc @ zero_zero_nat)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 17.01/5.06 thf(201,axiom,((! [A:int,B:int,C:nat]: ((ord_less_eq_int @ (ring_1_of_int_int @ A) @ (power_power_int @ (ring_1_of_int_int @ B) @ C)) = (ord_less_eq_int @ A @ (power_power_int @ B @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11_of__int__power__le__of__int__cancel__iff)).
% 17.01/5.06 thf(1030,plain,((! [A:int,B:int,C:nat]: ((ord_less_eq_int @ (ring_1_of_int_int @ A) @ (power_power_int @ (ring_1_of_int_int @ B) @ C)) = (ord_less_eq_int @ A @ (power_power_int @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 17.01/5.06 thf(62,axiom,((! [A:nat]: ((power_power_nat @ one_one_nat @ A) = one_one_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_118_power__one)).
% 17.01/5.06 thf(568,plain,((! [A:nat]: ((power_power_nat @ one_one_nat @ A) = one_one_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 17.01/5.06 thf(168,axiom,((! [A:num,B:nat,C:int]: (((power_power_nat @ (numeral_numeral_nat @ A) @ B) = (nat2 @ C)) = ((power_power_int @ (numeral_numeral_int @ A) @ B) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_36_numeral__power__eq__nat__cancel__iff)).
% 17.01/5.06 thf(929,plain,((! [A:num,B:nat,C:int]: (((power_power_nat @ (numeral_numeral_nat @ A) @ B) = (nat2 @ C)) = ((power_power_int @ (numeral_numeral_int @ A) @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 17.01/5.06 thf(261,axiom,((! [A:nat]: ((power_power_int @ zero_zero_int @ (suc @ A)) = zero_zero_int))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_263_power__0__Suc)).
% 17.01/5.06 thf(1193,plain,((! [A:nat]: ((power_power_int @ zero_zero_int @ (suc @ A)) = zero_zero_int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 17.01/5.06 thf(120,axiom,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_113_nat_Oinject)).
% 17.01/5.06 thf(763,plain,((! [A:nat,B:nat]: (((suc @ A) = (suc @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 17.01/5.06 thf(14,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (semiri1382578993at_nat @ A) @ (semiri1382578993at_nat @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_171_of__nat__mono)).
% 17.01/5.06 thf(383,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ A @ B) => (ord_less_eq_nat @ (semiri1382578993at_nat @ A) @ (semiri1382578993at_nat @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 17.01/5.06 thf(157,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ zero_zero_real @ A) => ((ord_less_eq_real @ zero_zero_real @ B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ (powr_real @ B @ A) @ (powr_real @ C @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_346_powr__mono2)).
% 17.01/5.06 thf(899,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ zero_zero_real @ A) => ((ord_less_eq_real @ zero_zero_real @ B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ (powr_real @ B @ A) @ (powr_real @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 17.01/5.06 thf(300,axiom,((! [A:real]: (ord_less_eq_real @ A @ (ring_1_of_int_real @ (archim1371465213g_real @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_42_le__of__int__ceiling)).
% 17.01/5.06 thf(1309,plain,((! [A:real]: (ord_less_eq_real @ A @ (ring_1_of_int_real @ (archim1371465213g_real @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[300])).
% 17.01/5.06 thf(345,axiom,((ord_less_eq_real @ (powr_real @ (numeral_numeral_real @ (bit0 @ one)) @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d))) @ (powr_real @ (numeral_numeral_real @ (bit0 @ one)) @ (semiri2110766477t_real @ (nat2 @ (archim1371465213g_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_103__092_060open_0622_Apowr_Alog_A2_A_Ireal__of__int_Ad_J_A_092_060le_062_A2_Apowr_Areal_A_Inat_A_092_060lceil_062log_A2_A_Ireal__of__int_Ad_J_092_060rceil_062_J_092_060close_062)).
% 17.01/5.06 thf(1442,plain,((ord_less_eq_real @ (powr_real @ (numeral_numeral_real @ (bit0 @ one)) @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d))) @ (powr_real @ (numeral_numeral_real @ (bit0 @ one)) @ (semiri2110766477t_real @ (nat2 @ (archim1371465213g_real @ (log @ (numeral_numeral_real @ (bit0 @ one)) @ (ring_1_of_int_real @ d)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[345])).
% 17.01/5.06 thf(52,axiom,((! [A:nat]: (zero_zero_nat != (suc @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_322_old_Onat_Odistinct_I1_J)).
% 17.01/5.06 thf(536,plain,((! [A:nat]: ~ (zero_zero_nat = (suc @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 17.01/5.06 thf(207,axiom,((ord_less_eq_int @ one_one_int @ one_one_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_84_le__numeral__extra_I4_J)).
% 17.01/5.06 thf(1045,plain,((ord_less_eq_int @ one_one_int @ one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 17.01/5.06 thf(107,axiom,((one_one_nat = (suc @ zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_325_One__nat__def)).
% 17.01/5.06 thf(716,plain,((one_one_nat = (suc @ zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 17.01/5.06 thf(131,axiom,((ord_less_eq_nat @ one_one_nat @ one_one_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_85_le__numeral__extra_I4_J)).
% 17.01/5.06 thf(800,plain,((ord_less_eq_nat @ one_one_nat @ one_one_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 17.01/5.06 thf(312,axiom,((one_one_nat = (nat2 @ one_one_int))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_168_nat__one__as__int)).
% 17.01/5.06 thf(1348,plain,((one_one_nat = (nat2 @ one_one_int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[312])).
% 17.01/5.06 thf(190,axiom,((! [A:num,B:num]: ((power_power_real @ (numeral_numeral_real @ A) @ (numeral_numeral_nat @ B)) = (numeral_numeral_real @ (pow @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_218_power__numeral)).
% 17.01/5.06 thf(999,plain,((! [A:num,B:num]: ((power_power_real @ (numeral_numeral_real @ A) @ (numeral_numeral_nat @ B)) = (numeral_numeral_real @ (pow @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 17.01/5.06 thf(227,axiom,((! [A:int]: ((ord_less_eq_int @ (ring_1_of_int_int @ A) @ one_one_int) = (ord_less_eq_int @ A @ one_one_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_77_of__int__le__1__iff)).
% 17.01/5.06 thf(1097,plain,((! [A:int]: ((ord_less_eq_int @ (ring_1_of_int_int @ A) @ one_one_int) = (ord_less_eq_int @ A @ one_one_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 17.01/5.06 thf(329,axiom,((! [A:nat,B:num,C:nat]: (((semiri2110766477t_real @ A) = (power_power_real @ (numeral_numeral_real @ B) @ C)) = (A = (power_power_nat @ (numeral_numeral_nat @ B) @ C))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_155_real__of__nat__eq__numeral__power__cancel__iff)).
% 17.01/5.06 thf(1395,plain,((! [A:nat,B:num,C:nat]: (((semiri2110766477t_real @ A) = (power_power_real @ (numeral_numeral_real @ B) @ C)) = (A = (power_power_nat @ (numeral_numeral_nat @ B) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[329])).
% 17.01/5.06 thf(138,axiom,((! [A:real]: ((powr_real @ zero_zero_real @ A) = zero_zero_real))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_251_powr__0)).
% 17.01/5.06 thf(818,plain,((! [A:real]: ((powr_real @ zero_zero_real @ A) = zero_zero_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 17.01/5.06 thf(144,axiom,((ord_less_eq_real @ zero_zero_real @ zero_zero_real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_312_le__numeral__extra_I3_J)).
% 17.01/5.06 thf(854,plain,((ord_less_eq_real @ zero_zero_real @ zero_zero_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 17.01/5.06 thf(280,axiom,((! [A:int,B:nat,C:int]: (((power_power_int @ (ring_1_of_int_int @ A) @ B) = (ring_1_of_int_int @ C)) = ((power_power_int @ A @ B) = C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_20_of__int__eq__of__int__power__cancel__iff)).
% 17.01/5.06 thf(1248,plain,((! [A:int,B:nat,C:int]: (((power_power_int @ (ring_1_of_int_int @ A) @ B) = (ring_1_of_int_int @ C)) = ((power_power_int @ A @ B) = C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[280])).
% 17.01/5.06 thf(132,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (suc @ A) @ (suc @ B)) = (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_109_Suc__le__mono)).
% 17.01/5.06 thf(801,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (suc @ A) @ (suc @ B)) = (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 17.01/5.06 thf(302,axiom,((! [A:num]: ((power_power_int @ zero_zero_int @ (numeral_numeral_nat @ A)) = zero_zero_int))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_266_power__zero__numeral)).
% 17.01/5.06 thf(1314,plain,((! [A:num]: ((power_power_int @ zero_zero_int @ (numeral_numeral_nat @ A)) = zero_zero_int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[302])).
% 17.01/5.06 thf(92,axiom,((ord_less_eq_real @ one_one_real @ one_one_real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_86_le__numeral__extra_I4_J)).
% 17.01/5.06 thf(664,plain,((ord_less_eq_real @ one_one_real @ one_one_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 17.01/5.06 thf(202,axiom,((! [A:int]: ((archim1371465213g_real @ (ring_1_of_int_real @ A)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_25_ceiling__of__int)).
% 17.01/5.06 thf(1033,plain,((! [A:int]: ((archim1371465213g_real @ (ring_1_of_int_real @ A)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 17.01/5.06 thf(176,axiom,((! [A:int]: (((nat2 @ A) = zero_zero_nat) = (ord_less_eq_int @ A @ zero_zero_int)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_254_nat__0__iff)).
% 17.01/5.06 thf(960,plain,((! [A:int]: (((nat2 @ A) = zero_zero_nat) = (ord_less_eq_int @ A @ zero_zero_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 17.01/5.06 thf(251,axiom,(((power_power_int @ one_one_int @ (numeral_numeral_nat @ (bit0 @ one))) = one_one_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_212_one__power2)).
% 17.01/5.06 thf(1165,plain,(((power_power_int @ one_one_int @ (numeral_numeral_nat @ (bit0 @ one))) = one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 17.01/5.06 thf(34,axiom,((! [A:nat]: (((semiri2110766477t_real @ A) = one_one_real) = (A = one_one_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_121_of__nat__eq__1__iff)).
% 17.01/5.06 thf(474,plain,((! [A:nat]: (((semiri2110766477t_real @ A) = one_one_real) = (A = one_one_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 17.01/5.06 thf(334,axiom,((! [A:num,B:int]: ((ord_less_eq_real @ (numeral_numeral_real @ A) @ (ring_1_of_int_real @ B)) = (ord_less_eq_int @ (numeral_numeral_int @ A) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_17_of__int__numeral__le__iff)).
% 17.01/5.06 thf(1410,plain,((! [A:num,B:int]: ((ord_less_eq_real @ (numeral_numeral_real @ A) @ (ring_1_of_int_real @ B)) = (ord_less_eq_int @ (numeral_numeral_int @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[334])).
% 17.01/5.06 thf(114,axiom,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_337_less__eq__nat_Osimps_I1_J)).
% 17.01/5.06 thf(740,plain,((! [A:nat]: (ord_less_eq_nat @ zero_zero_nat @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 17.01/5.06 thf(276,axiom,((! [A:real,B:num]: ((ord_less_eq_int @ (archim1371465213g_real @ A) @ (numeral_numeral_int @ B)) = (ord_less_eq_real @ A @ (numeral_numeral_real @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_13_ceiling__le__numeral)).
% 17.01/5.06 thf(1236,plain,((! [A:real,B:num]: ((ord_less_eq_int @ (archim1371465213g_real @ A) @ (numeral_numeral_int @ B)) = (ord_less_eq_real @ A @ (numeral_numeral_real @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[276])).
% 17.01/5.06 thf(239,axiom,(((numeral_numeral_nat @ one) = one_one_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_92_numeral__One)).
% 17.01/5.06 thf(1129,plain,(((numeral_numeral_nat @ one) = one_one_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 17.01/5.06 thf(287,axiom,((! [A:nat,B:num]: (((semiri2019852685at_int @ A) = (numeral_numeral_int @ B)) = (A = (numeral_numeral_nat @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_272_int__eq__iff__numeral)).
% 17.01/5.06 thf(1268,plain,((! [A:nat,B:num]: (((semiri2019852685at_int @ A) = (numeral_numeral_int @ B)) = (A = (numeral_numeral_nat @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[287])).
% 17.01/5.06 thf(147,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_181_le__trans)).
% 17.01/5.06 thf(860,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)],[147])).
% 17.01/5.06 thf(197,axiom,((! [A:num]: (ord_less_eq_num @ one @ A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_55_semiring__norm_I68_J)).
% 17.01/5.06 thf(1019,plain,((! [A:num]: (ord_less_eq_num @ one @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 17.01/5.06 thf(49,axiom,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) => (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_334_bot__nat__0_Oextremum__uniqueI)).
% 17.01/5.06 thf(528,plain,((! [A:nat]: ((ord_less_eq_nat @ A @ zero_zero_nat) => (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 17.01/5.06 thf(184,axiom,((! [A:int,B:int]: (((ring_1_of_int_real @ A) = (ring_1_of_int_real @ B)) = (A = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_22_of__int__eq__iff)).
% 17.01/5.06 thf(982,plain,((! [A:int,B:int]: (((ring_1_of_int_real @ A) = (ring_1_of_int_real @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 17.01/5.06 thf(297,axiom,((! [A:num,B:nat,C:int]: ((ord_less_eq_real @ (power_power_real @ (numeral_numeral_real @ A) @ B) @ (ring_1_of_int_real @ C)) = (ord_less_eq_int @ (power_power_int @ (numeral_numeral_int @ A) @ B) @ C)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1_numeral__power__le__of__int__cancel__iff)).
% 17.01/5.06 thf(1299,plain,((! [A:num,B:nat,C:int]: ((ord_less_eq_real @ (power_power_real @ (numeral_numeral_real @ A) @ B) @ (ring_1_of_int_real @ C)) = (ord_less_eq_int @ (power_power_int @ (numeral_numeral_int @ A) @ B) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[297])).
% 17.01/5.06 thf(99,axiom,((! [A:nat]: ((suc @ A) != zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_321_old_Onat_Odistinct_I2_J)).
% 17.01/5.06 thf(691,plain,((! [A:nat]: ~ ((suc @ A) = zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 17.01/5.06 thf(151,axiom,(((ring_1_of_int_int @ one_one_int) = one_one_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_67_of__int__1)).
% 17.01/5.06 thf(871,plain,(((ring_1_of_int_int @ one_one_int) = one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 17.01/5.06 thf(9,axiom,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (semiri1382578993at_nat @ A) @ (semiri1382578993at_nat @ B)) = (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_133_of__nat__le__iff)).
% 17.01/5.06 thf(369,plain,((! [A:nat,B:nat]: ((ord_less_eq_nat @ (semiri1382578993at_nat @ A) @ (semiri1382578993at_nat @ B)) = (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 17.01/5.06 thf(225,axiom,(((nat2 @ one_one_int) = (suc @ zero_zero_nat))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_271_nat__1)).
% 17.01/5.06 thf(1093,plain,(((nat2 @ one_one_int) = (suc @ zero_zero_nat))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 17.01/5.06 thf(141,axiom,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_eq_nat @ (suc @ D) @ C) => (A @ D))) => (A @ C))) => (A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_189_full__nat__induct)).
% 17.01/5.06 thf(839,plain,((! [A:(nat > $o),B:nat]: ((! [C:nat]: ((! [D:nat]: ((ord_less_eq_nat @ (suc @ D) @ C) => (A @ D))) => (A @ C))) => (A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 17.01/5.06 thf(72,axiom,(((neg_numeral_dbl_int @ zero_zero_int) = zero_zero_int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_259_dbl__simps_I2_J)).
% 17.01/5.06 thf(596,plain,(((neg_numeral_dbl_int @ zero_zero_int) = zero_zero_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 17.01/5.06 thf(323,axiom,((! [A:int,B:nat]: ((ord_less_eq_nat @ (nat2 @ A) @ B) = (ord_less_eq_int @ A @ (semiri2019852685at_int @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_349_nat__le__iff)).
% 17.01/5.06 thf(1378,plain,((! [A:int,B:nat]: ((ord_less_eq_nat @ (nat2 @ A) @ B) = (ord_less_eq_int @ A @ (semiri2019852685at_int @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[323])).
% 17.01/5.06 thf(36,axiom,((! [A:real,B:nat]: ((A != zero_zero_real) => ((power_power_real @ A @ B) != zero_zero_real)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_318_power__not__zero)).
% 17.01/5.06 thf(486,plain,((! [A:real,B:nat]: ((~ (A = zero_zero_real)) => (~ ((power_power_real @ A @ B) = zero_zero_real))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 17.01/5.06 thf(4,axiom,((! [A:nat]: (((semiri1382578993at_nat @ A) = zero_zero_nat) = (A = zero_zero_nat)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_238_of__nat__eq__0__iff)).
% 17.01/5.06 thf(354,plain,((! [A:nat]: (((semiri1382578993at_nat @ A) = zero_zero_nat) = (A = zero_zero_nat)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 17.01/5.06 thf(258,axiom,((! [A:int]: ((ord_less_eq_real @ one_one_real @ (ring_1_of_int_real @ A)) = (ord_less_eq_int @ one_one_int @ A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_76_of__int__1__le__iff)).
% 17.01/5.06 thf(1184,plain,((! [A:int]: ((ord_less_eq_real @ one_one_real @ (ring_1_of_int_real @ A)) = (ord_less_eq_int @ one_one_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 17.01/5.06 thf(54,axiom,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_180_eq__imp__le)).
% 17.01/5.06 thf(543,plain,((! [A:nat,B:nat]: ((A = B) => (ord_less_eq_nat @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 17.01/5.06 thf(223,axiom,((! [A:num,B:nat]: ((ord_less_eq_real @ (numeral_numeral_real @ A) @ (semiri2110766477t_real @ B)) = (ord_less_eq_nat @ (numeral_numeral_nat @ A) @ B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_160_numeral__le__real__of__nat__iff)).
% 17.01/5.06 thf(1088,plain,((! [A:num,B:nat]: ((ord_less_eq_real @ (numeral_numeral_real @ A) @ (semiri2110766477t_real @ B)) = (ord_less_eq_nat @ (numeral_numeral_nat @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 17.01/5.06 thf(39,axiom,((ord_less_eq_nat @ zero_zero_nat @ zero_zero_nat)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_311_le__numeral__extra_I3_J)).
% 17.01/5.06 thf(496,plain,((ord_less_eq_nat @ zero_zero_nat @ zero_zero_nat)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 17.01/5.06 thf(180,axiom,((! [A:nat]: ((nat2 @ (semiri2019852685at_int @ A)) = A))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_257_nat__int)).
% 17.01/5.06 thf(972,plain,((! [A:nat]: ((nat2 @ (semiri2019852685at_int @ A)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 17.01/5.06 thf(1459,plain,(($false)),inference(e,[status(thm)],[1036,809,1024,760,1454,628,941,1179,777,352,1369,1190,1005,1068,1443,994,1401,1073,511,1437,1041,1173,408,977,523,582,730,1290,873,449,1078,385,533,550,1233,1327,945,1342,913,1095,1196,709,417,1046,1359,436,1265,565,1366,1228,1254,1055,1287,1430,372,1330,702,357,587,619,902,559,1147,1319,969,1013,1362,1100,1398,881,1415,924,789,1109,1418,1136,514,574,806,966,821,905,1302,756,766,687,634,866,453,396,1201,1242,1119,774,411,1345,988,380,661,1306,1199,1153,1338,366,1311,798,1274,910,1223,1091,1021,1042,815,1217,598,916,625,879,1159,1027,1128,1281,1392,456,1106,1296,665,493,1210,682,1407,1350,742,697,1259,948,1064,388,593,869,499,857,1375,1121,783,420,471,884,1082,1292,753,1182,1424,642,637,1214,1446,679,547,1016,1207,590,622,997,985,1150,1451,1382,1131,721,1002,605,393,1114,1333,1434,938,360,508,921,1170,398,1187,1167,718,1251,1103,601,1007,732,1389,579,1124,1256,562,975,936,1271,611,1058,1239,1356,540,919,804,979,1117,377,1144,737,434,1439,863,477,631,848,668,1381,1112,1162,726,932,1061,685,768,1066,780,1364,851,505,431,653,695,1245,1176,608,490,1203,531,1277,1134,812,617,553,823,1049,1413,1076,927,374,525,712,855,640,1070,1225,414,1230,705,1156,502,1262,1317,951,1336,1220,907,1038,585,1085,576,1404,744,656,613,1284,1353,1052,1427,1140,1372,991,446,571,497,876,1421,1448,1010,771,363,556,699,1385,963,351,390,786,1030,568,929,1193,763,383,899,1309,1442,536,1045,716,800,1348,999,1097,1395,818,854,1248,801,1314,664,1033,960,1165,474,1410,740,1236,1129,1268,860,1019,528,982,1299,691,871,369,1093,839,596,1378,486,354,1184,543,1088,496,972])).
% 17.01/5.06 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.01/5.06 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------