%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP118^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:06:50 AM UTC 2026
% Result : Theorem 16.17s 4.82s
% Output : Refutation 17.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP118^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.20 % Computer : n026.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Tue Sep 29 19:58:57 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.88/0.78 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.28/1.17 % [INFO] Parsing done (388ms).
% 2.28/1.19 % [INFO] Running in sequential loop mode.
% 3.08/1.56 % [INFO] eprover registered as external prover.
% 3.08/1.57 % [INFO] Scanning for conjecture ...
% 3.48/1.72 % [INFO] Found a conjecture (or negated_conjecture) and 363 axioms. Running axiom selection ...
% 3.67/1.87 % [INFO] Axiom selection finished. Selected 363 axioms (removed 0 axioms).
% 4.44/2.08 % [INFO] Problem is higher-order (TPTP THF).
% 4.44/2.10 % [INFO] Type checking passed.
% 4.44/2.10 % [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 ...
% 16.17/4.82 % External prover 'e' found a proof!
% 16.17/4.82 % [INFO] Killing All external provers ...
% 16.17/4.82 % Time passed: 4477ms (effective reasoning time: 3623ms)
% 16.17/4.82 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 16.17/4.82 % Axioms used in derivation (363): fact_145_dist__commute__lessI, fact_272_le__of__int__ceiling, fact_47_Ints__abs, fact_333_order_Otrans, fact_240_abs__le__D1, fact_323_ord__le__eq__trans, fact_178_abs__one, fact_273_norm__bound__component__le__cart, fact_92_mem__Collect__eq, fact_102_of__int__eq__1__iff, fact_282_norm__triangle__ineq2, fact_260_abs__triangle__ineq2, fact_8_of__int__abs, fact_211_le__numeral__extra_I4_J, fact_85_axis__nth, fact_56_Ints__cases, fact_156_real__norm__def, fact_349_ord__eq__le__subst, fact_275_component__le__norm__cart, fact_299_complete__interval, fact_67_vec__nth__inject, fact_10_of__int__diff, fact_314_linorder__wlog, fact_305_vector__one__nth, fact_48_Ints__abs, fact_209_less__eq__real__def, fact_97_of__int__less__iff, fact_210_le__numeral__extra_I4_J, fact_228_diff__right__mono, fact_58_diff__right__commute, fact_232_diff__left__mono, fact_332_order_Otrans, fact_99_one__index, fact_37_vec__eq__iff, fact_264_norm__le__componentwise__cart, fact_277_dist__real, fact_217_int__le__induct, fact_161_diff__strict__mono, fact_160_norm__bound__component__lt__cart, fact_229_diff__left__mono, fact_345_ord__le__eq__subst, fact_52_Ints__induct, fact_251_abs__triangle__ineq2__sym, help_If_1_1_If_001t__Finite____Cartesian____Product__Ovec_It__Int__Oint_Mtf__n_J_T, fact_281_norm__triangle__ineq2, fact_105_of__int__1, fact_318_order__trans, fact_79__C1_C_I3_J, fact_133_floor__diff__one, fact_286_metric__eq__thm, fact_173_diff__strict__right__mono, fact_84_axis__nth, fact_180_Ints__1, fact_130_dist__diff_I1_J, fact_162_diff__strict__mono, fact_65_diff__eq__diff__eq, fact_0__C1_C_I2_J, fact_150_dist__commute, fact_40_assms, fact_335_le__cases, fact_111_ceiling__one, fact_45_Ints__diff, fact_203_of__int__1__le__iff, fact_307_complete__real, fact_331_le__cases3, fact_13_of__int__diff, fact_250_abs__triangle__ineq2__sym, fact_98_one__index, fact_107_of__int__1, fact_32_lambda__skolem, fact_290_dist__vec__nth__le, fact_301_order_Onot__eq__order__implies__strict, fact_248_ceiling__diff__floor__le__1, fact_20_of__int__vec__nth, fact_195_le__ceiling__iff, fact_59_diff__right__commute, fact_257_abs__triangle__ineq3, fact_112_floor__of__int, fact_327_order__class_Oorder_Oeq__iff, fact_46_Ints__diff, fact_51_Ints__of__int, fact_75_vec__sub, fact_18_of__int__vec__nth, fact_219_le__floor__iff, fact_4_vector__minus__component, fact_340_antisym, fact_205_one__le__floor, fact_179_dist__real__def, fact_188_of__int__floor__cancel, fact_234_diff__mono, fact_223_diff__eq__diff__less__eq, fact_213_less__eq__vec__def, fact_76_vec__sub, fact_55_Ints__cases, fact_27_abs__idempotent, fact_3__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062m_O_Areal__of__int_Am_A_061_Ax_A_E_Ai_A_N_Ay_A_E_Ai_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062, fact_329_antisym__conv, fact_36_vec__eq__iff, fact_159_norm__bound__component__lt__cart, fact_294_ceiling__correct, fact_143_linorder__neqE__linordered__idom, fact_252_abs__triangle__ineq2__sym, fact_176_diff__strict__right__mono, fact_146_dist__commute__lessI, fact_280_norm__triangle__ineq2, fact_54_Ints__induct, fact_192_real__abs__dist, fact_254_abs__triangle__ineq3, fact_350_ord__eq__le__subst, fact_86_vec_Oscale__left__diff__distrib, fact_283_abs__dist__diff__le, fact_78_vector__sub__rdistrib, fact_225_diff__right__mono, fact_325_ord__eq__le__trans, fact_90_abs__1, fact_292_norm__triangle__ineq3, fact_338_linear, fact_70_cond__component, fact_131_floor__less__one, fact_142_dist__norm, fact_221_diff__eq__diff__less__eq, fact_208_floor__mono, fact_230_diff__left__mono, fact_100_one__index, fact_300_eucl__less__le__not__le, fact_60_diff__right__commute, fact_136_one__reorient, fact_216_int__less__induct, fact_298_complete__interval, fact_181_Ints__1, fact_104_of__int__eq__1__iff, fact_220_ceiling__le__iff, fact_50_Ints__of__int, fact_271_of__int__floor__le, fact_165_diff__eq__diff__less, fact_236_diff__mono, fact_89_norm__axis__1, fact_343_eq__iff, help_If_2_1_If_001t__Finite____Cartesian____Product__Ovec_It__Int__Oint_Mtf__n_J_T, fact_118_vector__ssub__ldistrib, help_If_1_1_If_001t__Finite____Cartesian____Product__Ovec_It__Int__Oint_Mt__Numeral____Type__Onum1_J_T, fact_141_dist__norm, fact_22_of__int__eq__iff, fact_119_vector__ssub__ldistrib, fact_117_vec__component, help_If_3_1_If_001t__Finite____Cartesian____Product__Ovec_It__Real__Oreal_Mt__Numeral____Type__Onum1_J_T, fact_81_ceiling__diff__of__int, fact_134_ceiling__diff__one, fact_25_abs__abs, fact_306_vector__one__nth, fact_166_diff__eq__diff__less, fact_348_ord__eq__le__subst, fact_245_dist__vector__1, fact_140_dist__norm, fact_196_ceiling__split, fact_19_of__int__vec__nth, fact_14__092_060open_062x_A_E_Ai_A_N_Ay_A_E_Ai_A_092_060in_062_A_092_060int_062_092_060close_062, fact_110_floor__one, fact_115_vec__component, fact_139_less__ceiling__iff, fact_261_abs__triangle__ineq2, fact_116_vec__component, fact_43_Ints__diff, fact_316_dual__order_Orefl, help_If_2_1_If_001t__Finite____Cartesian____Product__Ovec_It__Real__Oreal_Mtf__n_J_T, fact_246_dist__vector__1, fact_96_of__int__less__iff, fact_120_of__int__1__less__iff, fact_128_dist__diff_I1_J, fact_326_order__class_Oorder_Oeq__iff, fact_137_one__reorient, fact_152_floor__less__cancel, fact_26_abs__idempotent, fact_319_order__trans, fact_287_metric__eq__thm, fact_31_abs__minus__commute, fact_302_order_Onot__eq__order__implies__strict, fact_149_dist__commute, fact_34_lambda__skolem, fact_344_ord__le__eq__subst, fact_174_diff__strict__right__mono, fact_352_forall__1, fact_153_norm__minus__commute, fact_17_of__int__vec__nth, fact_308_dual__order_Oantisym, fact_163_diff__strict__mono, fact_171_diff__strict__left__mono, fact_138_floor__less__iff, fact_262_norm__le__componentwise__cart, fact_24_abs__abs, fact_39_vec__eq__iff, fact_12_of__int__diff, fact_263_norm__le__componentwise__cart, fact_11_of__int__diff, help_If_2_1_If_001t__Finite____Cartesian____Product__Ovec_It__Real__Oreal_Mt__Numeral____Type__Onum1_J_T, fact_182_Ints__1, fact_6_vector__minus__component, fact_87_vec_Oscale__left__diff__distrib, fact_125_dist__diff_I2_J, fact_235_diff__mono, fact_334_le__cases, fact_83_axis__nth, fact_66_vec__nth__inject, fact_285_abs__dist__diff__le, fact_311_dual__order_Oeq__iff, fact_5_vector__minus__component, fact_53_Ints__induct, fact_346_ord__le__eq__subst, fact_72_cond__component, fact_49_Ints__of__int, fact_322_ord__le__eq__trans, fact_249_ceiling__less__iff, fact_189_real__of__int__floor__gt__diff__one, fact_201_of__int__le__1__iff, fact_122_of__int__less__1__iff, fact_193_less__numeral__extra_I4_J, fact_158_ex__of__int__less, help_If_1_1_If_001t__Finite____Cartesian____Product__Ovec_It__Real__Oreal_Mt__Numeral____Type__Onum1_J_T, fact_16_of__int__vec__nth, fact_304_dual__order_Ostrict__implies__order, fact_202_of__int__le__1__iff, fact_68_vec__nth__inject, fact_7_vector__minus__component, fact_259_abs__triangle__ineq2, fact_342_eq__iff, fact_243_ex__le__of__int, fact_258_abs__triangle__ineq2, fact_336_eq__refl, fact_73_cond__component, fact_151_ceiling__less__cancel, fact_309_dual__order_Oantisym, fact_265_norm__le__componentwise__cart, fact_114_vec__component, fact_9_of__int__abs, fact_274_norm__bound__component__le__cart, fact_337_eq__refl, fact_215_less__eq__vec__def, fact_303_dual__order_Ostrict__implies__order, fact_320_order__class_Oorder_Oantisym, fact_95_Collect__mem__eq, fact_93_mem__Collect__eq, fact_255_abs__triangle__ineq3, fact_88_floor__diff__of__int, fact_77_vector__sub__rdistrib, fact_155_norm__minus__commute, fact_1__C1_C_I1_J, fact_15_of__int__vec__nth, fact_231_diff__left__mono, help_If_2_1_If_001t__Finite____Cartesian____Product__Ovec_It__Int__Oint_Mt__Numeral____Type__Onum1_J_T, fact_339_linear, fact_186_Ints__eq__abs__less1, fact_288_metric__eq__thm, fact_164_diff__strict__mono, help_If_1_1_If_001t__Finite____Cartesian____Product__Ovec_It__Real__Oreal_Mtf__n_J_T, fact_206_ceiling__le__one, fact_69_vec__nth__inject, fact_347_ord__le__eq__subst, fact_313_dual__order_Otrans, fact_194_less__numeral__extra_I4_J, fact_212_less__eq__vec__def, fact_123_of__int__less__1__iff, fact_237_abs__ge__self, fact_94_Collect__mem__eq, fact_296_order__refl, fact_157_ex__less__of__int, fact_177_abs__one, fact_266_norm__le__componentwise__cart, fact_330_le__cases3, fact_293_norm__triangle__ineq3, fact_154_norm__minus__commute, fact_351_ord__eq__le__subst, fact_291_norm__triangle__ineq3, fact_80_norm__of__int, fact_324_ord__eq__le__trans, fact_103_of__int__eq__1__iff, fact_191_real__abs__dist, fact_207_ceiling__mono, fact_279_of__int__ceiling__diff__one__le, fact_233_diff__mono, fact_268_Finite__Cartesian__Product_Onorm__nth__le, fact_63_diff__eq__diff__eq, fact_23_of__int__eq__iff, fact_218_ceiling__le, fact_35_lambda__skolem, fact_241_norm__vector__1, fact_91_abs__1, fact_185_Ints__eq__abs__less1, fact_109_abs__norm__cancel, fact_38_vec__eq__iff, fact_190_real__abs__dist, fact_198_of__int__le__iff, fact_144_linorder__neqE__linordered__idom, fact_29_abs__minus__commute, fact_204_of__int__1__le__iff, fact_297_order__refl, fact_167_diff__eq__diff__less, fact_244_dist__vector__1, fact_183_vec_Oscale__right__diff__distrib, fact_187_of__int__ceiling__cancel, fact_284_abs__dist__diff__le, fact_270_real__of__int__floor__ge__diff__one, fact_41_of__int__vec__eq__iff, fact_267_norm__le__componentwise__cart, fact_199_of__int__le__iff, fact_242_norm__vector__1, fact_135_one__reorient, fact_253_abs__triangle__ineq2__sym, fact_172_diff__strict__left__mono, fact_353_ex__1, fact_71_cond__component, fact_44_Ints__diff, fact_74_dist__of__int, fact_108_abs__norm__cancel, fact_321_order__class_Oorder_Oantisym, fact_57_Ints__cases, fact_312_dual__order_Otrans, fact_278_floor__le__ceiling, fact_269_Finite__Cartesian__Product_Onorm__nth__le, fact_82_axis__nth, fact_132_one__less__ceiling, fact_197_ceiling__eq__iff, fact_124_norm__one, fact_28_abs__minus__commute, fact_113_ceiling__of__int, fact_276_component__le__norm__cart, fact_64_diff__eq__diff__eq, fact_317_dual__order_Orefl, fact_247_norm__real, fact_341_antisym, fact_175_diff__strict__right__mono, fact_101_one__index, fact_21_of__int__eq__iff, fact_214_less__eq__vec__def, fact_169_diff__strict__left__mono, fact_127_dist__diff_I2_J, fact_106_of__int__1, fact_170_diff__strict__left__mono, fact_328_antisym__conv, fact_238_abs__ge__self, fact_147_dist__commute__lessI, fact_184_vec_Oscale__right__diff__distrib, fact_256_abs__triangle__ineq3, fact_168_diff__eq__diff__less, fact_310_dual__order_Oeq__iff, fact_222_diff__eq__diff__less__eq, fact_61_diff__right__commute, fact_315_linorder__wlog, fact_295_ceiling__unique, fact_289_dist__vec__nth__le, fact_33_lambda__skolem, fact_227_diff__right__mono, fact_226_diff__right__mono, fact_148_dist__commute, fact_42_of__int__vec__eq__iff, fact_129_dist__diff_I1_J, fact_2_m, fact_200_zle__diff1__eq, fact_62_diff__eq__diff__eq, fact_121_of__int__1__less__iff, fact_224_diff__eq__diff__less__eq, fact_239_abs__le__D1, fact_30_abs__minus__commute, fact_126_dist__diff_I2_J
% 16.17/4.82 % No. of inferences in proof: 730
% 16.17/4.82 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 4477 ms resp. 3623 ms w/o parsing
% 17.33/5.10 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.33/5.10 thf(finite463740460l_num1_type, type, finite463740460l_num1: $tType).
% 17.33/5.10 thf(finite121157254l_num1_type, type, finite121157254l_num1: $tType).
% 17.33/5.10 thf(finite337957458num1_n_type, type, finite337957458num1_n: $tType).
% 17.33/5.10 thf(finite318270636al_n_n_type, type, finite318270636al_n_n: $tType).
% 17.33/5.10 thf(set_Fi1257234438l_num1_type, type, set_Fi1257234438l_num1: $tType).
% 17.33/5.10 thf(finite1183840848l_num1_type, type, finite1183840848l_num1: $tType).
% 17.33/5.10 thf(finite2063899472l_num1_type, type, finite2063899472l_num1: $tType).
% 17.33/5.10 thf(set_Fi1058188332real_n_type, type, set_Fi1058188332real_n: $tType).
% 17.33/5.10 thf(finite1489363574real_n_type, type, finite1489363574real_n: $tType).
% 17.33/5.10 thf(finite964658038_int_n_type, type, finite964658038_int_n: $tType).
% 17.33/5.10 thf(set_real_type, type, set_real: $tType).
% 17.33/5.10 thf(set_int_type, type, set_int: $tType).
% 17.33/5.10 thf(numeral_num1_type, type, numeral_num1: $tType).
% 17.33/5.10 thf(real_type, type, real: $tType).
% 17.33/5.10 thf(int_type, type, int: $tType).
% 17.33/5.10 thf(n_type, type, n: $tType).
% 17.33/5.10 thf(archim1371465213g_real_decl, type, archim1371465213g_real: (real > int)).
% 17.33/5.10 thf(archim1031974863r_real_decl, type, archim1031974863r_real: (real > int)).
% 17.33/5.10 thf(finite627713486m1_int_decl, type, finite627713486m1_int: (numeral_num1 > (int > finite2063899472l_num1))).
% 17.33/5.10 thf(finite15144922381_real_decl, type, finite15144922381_real: (numeral_num1 > (real > finite1183840848l_num1))).
% 17.33/5.10 thf(finite1888777460_n_int_decl, type, finite1888777460_n_int: (n > (int > finite964658038_int_n))).
% 17.33/5.10 thf(finite703491444n_real_decl, type, finite703491444n_real: (n > (real > finite1489363574real_n))).
% 17.33/5.10 thf(finite1470207077l_num1_decl, type, finite1470207077l_num1: (int > finite2063899472l_num1)).
% 17.33/5.10 thf(finite55766923_int_n_decl, type, finite55766923_int_n: (int > finite964658038_int_n)).
% 17.33/5.10 thf(finite1329045861l_num1_decl, type, finite1329045861l_num1: (real > finite1183840848l_num1)).
% 17.33/5.10 thf(finite667548811real_n_decl, type, finite667548811real_n: (real > finite1489363574real_n)).
% 17.33/5.10 thf(finite1449546019l_num1_decl, type, finite1449546019l_num1: (finite463740460l_num1 > (numeral_num1 > finite1183840848l_num1))).
% 17.33/5.10 thf(finite1639785033num1_n_decl, type, finite1639785033num1_n: (finite337957458num1_n > (n > finite1183840848l_num1))).
% 17.33/5.10 thf(finite1503577981l_num1_decl, type, finite1503577981l_num1: (finite121157254l_num1 > (numeral_num1 > finite1489363574real_n))).
% 17.33/5.10 thf(finite625646243al_n_n_decl, type, finite625646243al_n_n: (finite318270636al_n_n > (n > finite1489363574real_n))).
% 17.33/5.10 thf(finite1800583751l_num1_decl, type, finite1800583751l_num1: (finite2063899472l_num1 > (numeral_num1 > int))).
% 17.33/5.10 thf(finite566214509_int_n_decl, type, finite566214509_int_n: (finite964658038_int_n > (n > int))).
% 17.33/5.10 thf(finite1106245191l_num1_decl, type, finite1106245191l_num1: (finite1183840848l_num1 > (numeral_num1 > real))).
% 17.33/5.10 thf(finite772340589real_n_decl, type, finite772340589real_n: (finite1489363574real_n > (n > real))).
% 17.33/5.10 thf(finite1961675766l_num1_decl, type, finite1961675766l_num1: (real > (finite1183840848l_num1 > finite1183840848l_num1))).
% 17.33/5.10 thf(finite2053577756real_n_decl, type, finite2053577756real_n: (real > (finite1489363574real_n > finite1489363574real_n))).
% 17.33/5.10 thf(abs_ab948591917l_num1_decl, type, abs_ab948591917l_num1: (finite1183840848l_num1 > finite1183840848l_num1)).
% 17.33/5.10 thf(abs_ab1599551059real_n_decl, type, abs_ab1599551059real_n: (finite1489363574real_n > finite1489363574real_n)).
% 17.33/5.10 thf(abs_abs_int_decl, type, abs_abs_int: (int > int)).
% 17.33/5.10 thf(abs_abs_real_decl, type, abs_abs_real: (real > real)).
% 17.33/5.10 thf(minus_779068585l_num1_decl, type, minus_779068585l_num1: (finite2063899472l_num1 > (finite2063899472l_num1 > finite2063899472l_num1))).
% 17.33/5.10 thf(minus_1196255695_int_n_decl, type, minus_1196255695_int_n: (finite964658038_int_n > (finite964658038_int_n > finite964658038_int_n))).
% 17.33/5.10 thf(minus_249161513l_num1_decl, type, minus_249161513l_num1: (finite1183840848l_num1 > (finite1183840848l_num1 > finite1183840848l_num1))).
% 17.33/5.10 thf(minus_1037315151real_n_decl, type, minus_1037315151real_n: (finite1489363574real_n > (finite1489363574real_n > finite1489363574real_n))).
% 17.33/5.10 thf(minus_minus_int_decl, type, minus_minus_int: (int > (int > int))).
% 17.33/5.10 thf(minus_minus_real_decl, type, minus_minus_real: (real > (real > real))).
% 17.33/5.10 thf(one_on601734293l_num1_decl, type, one_on601734293l_num1: finite2063899472l_num1).
% 17.33/5.10 thf(one_on1516019131_int_n_decl, type, one_on1516019131_int_n: finite964658038_int_n).
% 17.33/5.10 thf(one_on1961019669l_num1_decl, type, one_on1961019669l_num1: finite1183840848l_num1).
% 17.33/5.10 thf(one_on1253059131real_n_decl, type, one_on1253059131real_n: finite1489363574real_n).
% 17.33/5.10 thf(one_one_int_decl, type, one_one_int: int).
% 17.33/5.10 thf(one_one_Numeral_num1_decl, type, one_one_Numeral_num1: numeral_num1).
% 17.33/5.10 thf(one_one_real_decl, type, one_one_real: real).
% 17.33/5.10 thf(if_Fin1570437642l_num1_decl, type, if_Fin1570437642l_num1: ($o > (finite2063899472l_num1 > (finite2063899472l_num1 > finite2063899472l_num1)))).
% 17.33/5.10 thf(if_Fin1767949360_int_n_decl, type, if_Fin1767949360_int_n: ($o > (finite964658038_int_n > (finite964658038_int_n > finite964658038_int_n)))).
% 17.33/5.10 thf(if_Fin1668193290l_num1_decl, type, if_Fin1668193290l_num1: ($o > (finite1183840848l_num1 > (finite1183840848l_num1 > finite1183840848l_num1)))).
% 17.33/5.10 thf(if_Fin127821360real_n_decl, type, if_Fin127821360real_n: ($o > (finite1489363574real_n > (finite1489363574real_n > finite1489363574real_n)))).
% 17.33/5.10 thf(ring_11529266783l_num1_decl, type, ring_11529266783l_num1: set_Fi1257234438l_num1).
% 17.33/5.10 thf(ring_1723899781real_n_decl, type, ring_1723899781real_n: set_Fi1058188332real_n).
% 17.33/5.10 thf(ring_1_Ints_int_decl, type, ring_1_Ints_int: set_int).
% 17.33/5.10 thf(ring_1_Ints_real_decl, type, ring_1_Ints_real: set_real).
% 17.33/5.10 thf(ring_1154201247l_num1_decl, type, ring_1154201247l_num1: (int > finite1183840848l_num1)).
% 17.33/5.10 thf(ring_11737179077real_n_decl, type, ring_11737179077real_n: (int > finite1489363574real_n)).
% 17.33/5.10 thf(ring_1_of_int_int_decl, type, ring_1_of_int_int: (int > int)).
% 17.33/5.10 thf(ring_1_of_int_real_decl, type, ring_1_of_int_real: (int > real)).
% 17.33/5.10 thf(minkow781993583real_n_decl, type, minkow781993583real_n: (finite2063899472l_num1 > finite121157254l_num1)).
% 17.33/5.10 thf(minkow2063319845m1_int_decl, type, minkow2063319845m1_int: (finite2063899472l_num1 > finite2063899472l_num1)).
% 17.33/5.10 thf(minkow19073400691_real_decl, type, minkow19073400691_real: (finite2063899472l_num1 > finite1183840848l_num1)).
% 17.33/5.10 thf(minkow371489429real_n_decl, type, minkow371489429real_n: (finite964658038_int_n > finite318270636al_n_n)).
% 17.33/5.10 thf(minkow1468704075_n_int_decl, type, minkow1468704075_n_int: (finite964658038_int_n > finite964658038_int_n)).
% 17.33/5.10 thf(minkow1134813771n_real_decl, type, minkow1134813771n_real: (finite964658038_int_n > finite1489363574real_n)).
% 17.33/5.10 thf(ord_le2035778724l_num1_decl, type, ord_le2035778724l_num1: (finite1183840848l_num1 > (finite1183840848l_num1 > $o))).
% 17.33/5.10 thf(ord_le1017090250real_n_decl, type, ord_le1017090250real_n: (finite1489363574real_n > (finite1489363574real_n > $o))).
% 17.33/5.10 thf(ord_less_int_decl, type, ord_less_int: (int > (int > $o))).
% 17.33/5.10 thf(ord_less_real_decl, type, ord_less_real: (real > (real > $o))).
% 17.33/5.10 thf(ord_le1202326448l_num1_decl, type, ord_le1202326448l_num1: (finite2063899472l_num1 > (finite2063899472l_num1 > $o))).
% 17.33/5.10 thf(ord_le1908593622_int_n_decl, type, ord_le1908593622_int_n: (finite964658038_int_n > (finite964658038_int_n > $o))).
% 17.33/5.10 thf(ord_le1724070576l_num1_decl, type, ord_le1724070576l_num1: (finite1183840848l_num1 > (finite1183840848l_num1 > $o))).
% 17.33/5.10 thf(ord_le866583254real_n_decl, type, ord_le866583254real_n: (finite1489363574real_n > (finite1489363574real_n > $o))).
% 17.33/5.10 thf(ord_less_eq_int_decl, type, ord_less_eq_int: (int > (int > $o))).
% 17.33/5.10 thf(ord_less_eq_real_decl, type, ord_less_eq_real: (real > (real > $o))).
% 17.33/5.10 thf(real_V1974343547l_num1_decl, type, real_V1974343547l_num1: (finite463740460l_num1 > (finite463740460l_num1 > real))).
% 17.33/5.10 thf(real_V845814485l_num1_decl, type, real_V845814485l_num1: (finite121157254l_num1 > (finite121157254l_num1 > real))).
% 17.33/5.10 thf(real_V488409631l_num1_decl, type, real_V488409631l_num1: (finite1183840848l_num1 > (finite1183840848l_num1 > real))).
% 17.33/5.10 thf(real_V783965509real_n_decl, type, real_V783965509real_n: (finite1489363574real_n > (finite1489363574real_n > real))).
% 17.33/5.10 thf(real_V1934908667t_real_decl, type, real_V1934908667t_real: (real > (real > real))).
% 17.33/5.10 thf(real_V316032763l_num1_decl, type, real_V316032763l_num1: (finite463740460l_num1 > real)).
% 17.33/5.10 thf(real_V1121707553num1_n_decl, type, real_V1121707553num1_n: (finite337957458num1_n > real)).
% 17.33/5.10 thf(real_V400292255l_num1_decl, type, real_V400292255l_num1: (finite1183840848l_num1 > real)).
% 17.33/5.10 thf(real_V739724485real_n_decl, type, real_V739724485real_n: (finite1489363574real_n > real)).
% 17.33/5.10 thf(real_V646646907m_real_decl, type, real_V646646907m_real: (real > real)).
% 17.33/5.10 thf(collec321817931real_n_decl, type, collec321817931real_n: ((finite1489363574real_n > $o) > set_Fi1058188332real_n)).
% 17.33/5.10 thf(collect_real_decl, type, collect_real: ((real > $o) > set_real)).
% 17.33/5.10 thf(member1413569767l_num1_decl, type, member1413569767l_num1: (finite1183840848l_num1 > (set_Fi1257234438l_num1 > $o))).
% 17.33/5.10 thf(member1352538125real_n_decl, type, member1352538125real_n: (finite1489363574real_n > (set_Fi1058188332real_n > $o))).
% 17.33/5.10 thf(member_int_decl, type, member_int: (int > (set_int > $o))).
% 17.33/5.10 thf(member_real_decl, type, member_real: (real > (set_real > $o))).
% 17.33/5.10 thf(a_decl, type, a: set_Fi1058188332real_n).
% 17.33/5.10 thf(i_decl, type, i: n).
% 17.33/5.10 thf(m_decl, type, m: int).
% 17.33/5.10 thf(x_decl, type, x: finite1489363574real_n).
% 17.33/5.10 thf(y_decl, type, y: finite1489363574real_n).
% 17.33/5.10 thf(122,axiom,((! [A:real,B:real,C:(real > int),D:int]: ((ord_less_eq_real @ A @ B) => (((C @ B) = D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_int @ (C @ E) @ (C @ F)))) => (ord_less_eq_int @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_346_ord__le__eq__subst)).
% 17.33/5.10 thf(809,plain,((! [A:real,B:real,C:(real > int),D:int]: ((ord_less_eq_real @ A @ B) => (((C @ B) = D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_int @ (C @ E) @ (C @ F)))) => (ord_less_eq_int @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 17.33/5.10 thf(317,axiom,((! [A:int]: (ord_less_eq_int @ A @ (abs_abs_int @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_237_abs__ge__self)).
% 17.33/5.10 thf(1411,plain,((! [A:int]: (ord_less_eq_int @ A @ (abs_abs_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[317])).
% 17.33/5.10 thf(254,axiom,((! [A:finite1489363574real_n,B:n]: (ord_less_eq_real @ (abs_abs_real @ (finite772340589real_n @ A @ B)) @ (real_V739724485real_n @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_275_component__le__norm__cart)).
% 17.33/5.10 thf(1237,plain,((! [A:finite1489363574real_n,B:n]: (ord_less_eq_real @ (abs_abs_real @ (finite772340589real_n @ A @ B)) @ (real_V739724485real_n @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 17.33/5.10 thf(76,axiom,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ B @ A) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_320_order__class_Oorder_Oantisym)).
% 17.33/5.10 thf(628,plain,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 17.33/5.10 thf(144,axiom,((! [A:real,B:real,C:real,D:real]: (((minus_minus_real @ A @ B) = (minus_minus_real @ C @ D)) => ((ord_less_real @ A @ B) = (ord_less_real @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_167_diff__eq__diff__less)).
% 17.33/5.10 thf(893,plain,((! [A:real,B:real,C:real,D:real]: (((minus_minus_real @ A @ B) = (minus_minus_real @ C @ D)) => ((ord_less_real @ A @ B) = (ord_less_real @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 17.33/5.10 thf(164,axiom,((((=) @ int) = (^ [A:int,B:int]: ((ord_less_eq_int @ A @ B) & (ord_less_eq_int @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_326_order__class_Oorder_Oeq__iff)).
% 17.33/5.10 thf(962,plain,((((=) @ int) = (^ [A:int,B:int]: ((ord_less_eq_int @ A @ B) & (ord_less_eq_int @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 17.33/5.10 thf(40,axiom,((! [A:(numeral_num1 > (real > $o))]: ((! [B:numeral_num1]: ? [C:real]: (A @ B @ C)) = (? [B:finite1183840848l_num1]: ! [C:numeral_num1]: (A @ C @ (finite1106245191l_num1 @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_33_lambda__skolem)).
% 17.33/5.10 thf(481,plain,((! [A:(numeral_num1 > (real > $o))]: ((! [B:numeral_num1]: ? [C:real]: (A @ B @ C)) = (? [B:finite1183840848l_num1]: ! [C:numeral_num1]: (A @ C @ (finite1106245191l_num1 @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 17.33/5.10 thf(315,axiom,((! [A:int,B:int]: ((ring_1_of_int_real @ (minus_minus_int @ A @ B)) = (minus_minus_real @ (ring_1_of_int_real @ A) @ (ring_1_of_int_real @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_of__int__diff)).
% 17.33/5.10 thf(1406,plain,((! [A:int,B:int]: ((ring_1_of_int_real @ (minus_minus_int @ A @ B)) = (minus_minus_real @ (ring_1_of_int_real @ A) @ (ring_1_of_int_real @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[315])).
% 17.33/5.10 thf(275,axiom,((! [A:int,B:real]: ((ord_less_int @ A @ (archim1371465213g_real @ B)) = (ord_less_real @ (ring_1_of_int_real @ A) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_139_less__ceiling__iff)).
% 17.33/5.10 thf(1290,plain,((! [A:int,B:real]: ((ord_less_int @ A @ (archim1371465213g_real @ B)) = (ord_less_real @ (ring_1_of_int_real @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[275])).
% 17.33/5.10 thf(359,axiom,((! [A:real,B:int]: (((archim1371465213g_real @ A) = B) = ((ord_less_real @ (minus_minus_real @ (ring_1_of_int_real @ B) @ one_one_real) @ A) & (ord_less_eq_real @ A @ (ring_1_of_int_real @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_197_ceiling__eq__iff)).
% 17.33/5.10 thf(1522,plain,((! [A:real,B:int]: (((archim1371465213g_real @ A) = B) = ((ord_less_real @ (minus_minus_real @ (ring_1_of_int_real @ B) @ one_one_real) @ A) & (ord_less_eq_real @ A @ (ring_1_of_int_real @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[359])).
% 17.33/5.10 thf(198,axiom,((! [A:finite1183840848l_num1,B:numeral_num1,C:finite1183840848l_num1]: (ord_less_eq_real @ (real_V1934908667t_real @ (finite1106245191l_num1 @ A @ B) @ (finite1106245191l_num1 @ C @ B)) @ (real_V488409631l_num1 @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_290_dist__vec__nth__le)).
% 17.33/5.10 thf(1073,plain,((! [A:finite1183840848l_num1,B:numeral_num1,C:finite1183840848l_num1]: (ord_less_eq_real @ (real_V1934908667t_real @ (finite1106245191l_num1 @ A @ B) @ (finite1106245191l_num1 @ C @ B)) @ (real_V488409631l_num1 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 17.33/5.10 thf(7,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1,D:finite1183840848l_num1]: (((minus_249161513l_num1 @ A @ B) = (minus_249161513l_num1 @ C @ D)) => ((ord_le1724070576l_num1 @ A @ B) = (ord_le1724070576l_num1 @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_222_diff__eq__diff__less__eq)).
% 17.33/5.10 thf(379,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1,D:finite1183840848l_num1]: (((minus_249161513l_num1 @ A @ B) = (minus_249161513l_num1 @ C @ D)) => ((ord_le1724070576l_num1 @ A @ B) = (ord_le1724070576l_num1 @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 17.33/5.10 thf(280,axiom,((! [A:real]: (ord_less_eq_real @ A @ (ring_1_of_int_real @ (archim1371465213g_real @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_272_le__of__int__ceiling)).
% 17.33/5.10 thf(1305,plain,((! [A:real]: (ord_less_eq_real @ A @ (ring_1_of_int_real @ (archim1371465213g_real @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[280])).
% 17.33/5.10 thf(226,axiom,((! [A:int,B:(int > int),C:int,D:int]: ((A = (B @ C)) => ((ord_less_eq_int @ C @ D) => ((! [E:int,F:int]: ((ord_less_eq_int @ E @ F) => (ord_less_eq_int @ (B @ E) @ (B @ F)))) => (ord_less_eq_int @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_348_ord__eq__le__subst)).
% 17.33/5.10 thf(1158,plain,((! [A:int,B:(int > int),C:int,D:int]: ((A = (B @ C)) => ((ord_less_eq_int @ C @ D) => ((! [E:int,F:int]: ((ord_less_eq_int @ E @ F) => (ord_less_eq_int @ (B @ E) @ (B @ F)))) => (ord_less_eq_int @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 17.33/5.10 thf(63,axiom,((! [A:real,B:real]: (ord_less_eq_real @ (minus_minus_real @ (real_V646646907m_real @ A) @ (real_V646646907m_real @ B)) @ (real_V646646907m_real @ (minus_minus_real @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_281_norm__triangle__ineq2)).
% 17.33/5.10 thf(582,plain,((! [A:real,B:real]: (ord_less_eq_real @ (minus_minus_real @ (real_V646646907m_real @ A) @ (real_V646646907m_real @ B)) @ (real_V646646907m_real @ (minus_minus_real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 17.33/5.10 thf(229,axiom,((real_V783965509real_n = (^ [A:finite1489363574real_n,B:finite1489363574real_n]: (real_V783965509real_n @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_148_dist__commute)).
% 17.33/5.10 thf(1173,plain,(((real_V783965509real_n) = (^ [A:finite1489363574real_n,B:finite1489363574real_n]: (real_V783965509real_n @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 17.33/5.10 thf(345,axiom,((! [A:int]: ((ord_less_real @ (ring_1_of_int_real @ A) @ one_one_real) = (ord_less_int @ A @ one_one_int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_122_of__int__less__1__iff)).
% 17.33/5.10 thf(1486,plain,((! [A:int]: ((ord_less_real @ (ring_1_of_int_real @ A) @ one_one_real) = (ord_less_int @ A @ one_one_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[345])).
% 17.33/5.10 thf(349,axiom,((! [A:finite1183840848l_num1,B:numeral_num1]: (ord_less_eq_real @ (abs_abs_real @ (finite1106245191l_num1 @ A @ B)) @ (real_V400292255l_num1 @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_276_component__le__norm__cart)).
% 17.33/5.10 thf(1497,plain,((! [A:finite1183840848l_num1,B:numeral_num1]: (ord_less_eq_real @ (abs_abs_real @ (finite1106245191l_num1 @ A @ B)) @ (real_V400292255l_num1 @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[349])).
% 17.33/5.10 thf(9,axiom,((! [A:finite2063899472l_num1,B:finite2063899472l_num1]: ((if_Fin1570437642l_num1 @ ($true) @ A @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_1_1_If_001t__Finite____Cartesian____Product__Ovec_It__Int__Oint_Mt__Numeral____Type__Onum1_J_T)).
% 17.33/5.10 thf(384,plain,((! [A:finite2063899472l_num1,B:finite2063899472l_num1]: ((if_Fin1570437642l_num1 @ ($true) @ A @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 17.33/5.10 thf(282,axiom,((! [A:finite1183840848l_num1,B:real,C:numeral_num1]: ((ord_less_eq_real @ (real_V400292255l_num1 @ A) @ B) => (ord_less_eq_real @ (abs_abs_real @ (finite1106245191l_num1 @ A @ C)) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_274_norm__bound__component__le__cart)).
% 17.33/5.10 thf(1310,plain,((! [A:finite1183840848l_num1,B:real,C:numeral_num1]: ((ord_less_eq_real @ (real_V400292255l_num1 @ A) @ B) => (ord_less_eq_real @ (abs_abs_real @ (finite1106245191l_num1 @ A @ C)) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 17.33/5.10 thf(56,axiom,((! [A:real,B:(real > $o)]: ((member_real @ A @ (collect_real @ B)) = (B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_93_mem__Collect__eq)).
% 17.33/5.10 thf(550,plain,((! [A:real,B:(real > $o)]: ((member_real @ A @ (collect_real @ (B))) = (B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 17.33/5.10 thf(47,axiom,(((archim1371465213g_real @ one_one_real) = one_one_int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_111_ceiling__one)).
% 17.33/5.10 thf(500,plain,(((archim1371465213g_real @ one_one_real) = one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 17.33/5.10 thf(98,axiom,((! [A:real,B:real]: ((real_V646646907m_real @ (minus_minus_real @ A @ B)) = (real_V646646907m_real @ (minus_minus_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_154_norm__minus__commute)).
% 17.33/5.10 thf(715,plain,((! [A:real,B:real]: ((real_V646646907m_real @ (minus_minus_real @ A @ B)) = (real_V646646907m_real @ (minus_minus_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 17.33/5.10 thf(150,axiom,((! [A:finite1489363574real_n,B:(finite1489363574real_n > $o)]: ((member1352538125real_n @ A @ ring_1723899781real_n) => ((! [C:int]: (B @ (ring_11737179077real_n @ C))) => (B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_54_Ints__induct)).
% 17.33/5.10 thf(913,plain,((! [A:finite1489363574real_n,B:(finite1489363574real_n > $o)]: ((member1352538125real_n @ A @ ring_1723899781real_n) => ((! [C:int]: (B @ (ring_11737179077real_n @ C))) => (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 17.33/5.10 thf(83,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_real @ (minus_minus_real @ A @ C) @ (minus_minus_real @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_228_diff__right__mono)).
% 17.33/5.10 thf(670,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_real @ (minus_minus_real @ A @ C) @ (minus_minus_real @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 17.33/5.10 thf(177,axiom,((! [A:(int > (int > $o)),B:int,C:int]: ((! [D:int,E:int]: ((ord_less_eq_int @ D @ E) => (A @ D @ E))) => ((! [D:int,E:int]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_314_linorder__wlog)).
% 17.33/5.10 thf(1001,plain,((! [A:(int > (int > $o)),B:int,C:int]: ((! [D:int,E:int]: ((ord_less_eq_int @ D @ E) => (A @ D @ E))) => ((! [D:int,E:int]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 17.33/5.10 thf(257,axiom,((! [A:real,B:int]: ((archim1031974863r_real @ (minus_minus_real @ A @ (ring_1_of_int_real @ B))) = (minus_minus_int @ (archim1031974863r_real @ A) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_88_floor__diff__of__int)).
% 17.33/5.10 thf(1243,plain,((! [A:real,B:int]: ((archim1031974863r_real @ (minus_minus_real @ A @ (ring_1_of_int_real @ B))) = (minus_minus_int @ (archim1031974863r_real @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 17.33/5.10 thf(312,axiom,((! [A:$o,B:finite1489363574real_n,C:finite1489363574real_n,D:n]: (((A) => ((finite772340589real_n @ (if_Fin127821360real_n @ A @ B @ C) @ D) = (finite772340589real_n @ B @ D))) & ((~ (A)) => ((finite772340589real_n @ (if_Fin127821360real_n @ A @ B @ C) @ D) = (finite772340589real_n @ C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_70_cond__component)).
% 17.33/5.10 thf(1391,plain,((! [A:$o,B:finite1489363574real_n,C:finite1489363574real_n,D:n]: (((A) => ((finite772340589real_n @ (if_Fin127821360real_n @ A @ B @ C) @ D) = (finite772340589real_n @ B @ D))) & ((~ (A)) => ((finite772340589real_n @ (if_Fin127821360real_n @ A @ B @ C) @ D) = (finite772340589real_n @ C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[312])).
% 17.33/5.10 thf(327,axiom,((! [A:int,B:int]: ((real_V1934908667t_real @ (ring_1_of_int_real @ A) @ (ring_1_of_int_real @ B)) = (ring_1_of_int_real @ (abs_abs_int @ (minus_minus_int @ A @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_dist__of__int)).
% 17.33/5.10 thf(1441,plain,((! [A:int,B:int]: ((real_V1934908667t_real @ (ring_1_of_int_real @ A) @ (ring_1_of_int_real @ B)) = (ring_1_of_int_real @ (abs_abs_int @ (minus_minus_int @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[327])).
% 17.33/5.10 thf(141,axiom,((! [A:int,B:int,C:int,D:int]: (((minus_minus_int @ A @ B) = (minus_minus_int @ C @ D)) => ((ord_less_int @ A @ B) = (ord_less_int @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_168_diff__eq__diff__less)).
% 17.33/5.10 thf(885,plain,((! [A:int,B:int,C:int,D:int]: (((minus_minus_int @ A @ B) = (minus_minus_int @ C @ D)) => ((ord_less_int @ A @ B) = (ord_less_int @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 17.33/5.10 thf(28,axiom,((! [A:real]: ((ord_less_int @ one_one_int @ (archim1371465213g_real @ A)) = (ord_less_real @ one_one_real @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_132_one__less__ceiling)).
% 17.33/5.10 thf(436,plain,((! [A:real]: ((ord_less_int @ one_one_int @ (archim1371465213g_real @ A)) = (ord_less_real @ one_one_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 17.33/5.10 thf(357,axiom,(((abs_abs_real @ one_one_real) = one_one_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_90_abs__1)).
% 17.33/5.10 thf(1518,plain,(((abs_abs_real @ one_one_real) = one_one_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[357])).
% 17.33/5.10 thf(251,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((abs_ab1599551059real_n @ (minus_1037315151real_n @ A @ B)) = (abs_ab1599551059real_n @ (minus_1037315151real_n @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_28_abs__minus__commute)).
% 17.33/5.10 thf(1228,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((abs_ab1599551059real_n @ (minus_1037315151real_n @ A @ B)) = (abs_ab1599551059real_n @ (minus_1037315151real_n @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 17.33/5.10 thf(316,axiom,((! [A:int,B:int]: (ord_less_eq_int @ (minus_minus_int @ (abs_abs_int @ A) @ (abs_abs_int @ B)) @ (abs_abs_int @ (minus_minus_int @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_252_abs__triangle__ineq2__sym)).
% 17.33/5.10 thf(1409,plain,((! [A:int,B:int]: (ord_less_eq_int @ (minus_minus_int @ (abs_abs_int @ A) @ (abs_abs_int @ B)) @ (abs_abs_int @ (minus_minus_int @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[316])).
% 17.33/5.10 thf(274,axiom,((! [A:int]: ((ord_less_real @ one_one_real @ (ring_1_of_int_real @ A)) = (ord_less_int @ one_one_int @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_120_of__int__1__less__iff)).
% 17.33/5.10 thf(1287,plain,((! [A:int]: ((ord_less_real @ one_one_real @ (ring_1_of_int_real @ A)) = (ord_less_int @ one_one_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 17.33/5.10 thf(59,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((real_V400292255l_num1 @ (minus_249161513l_num1 @ A @ B)) = (real_V400292255l_num1 @ (minus_249161513l_num1 @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_155_norm__minus__commute)).
% 17.33/5.10 thf(570,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((real_V400292255l_num1 @ (minus_249161513l_num1 @ A @ B)) = (real_V400292255l_num1 @ (minus_249161513l_num1 @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 17.33/5.10 thf(323,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n]: ((ord_le1017090250real_n @ A @ B) => (ord_le1017090250real_n @ (minus_1037315151real_n @ C @ B) @ (minus_1037315151real_n @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_169_diff__strict__left__mono)).
% 17.33/5.10 thf(1430,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n]: ((ord_le1017090250real_n @ A @ B) => (ord_le1017090250real_n @ (minus_1037315151real_n @ C @ B) @ (minus_1037315151real_n @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[323])).
% 17.33/5.10 thf(49,axiom,((! [A:finite1183840848l_num1]: ((finite1329045861l_num1 @ (finite1106245191l_num1 @ A @ one_one_Numeral_num1)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_305_vector__one__nth)).
% 17.33/5.10 thf(504,plain,((! [A:finite1183840848l_num1]: ((finite1329045861l_num1 @ (finite1106245191l_num1 @ A @ one_one_Numeral_num1)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 17.33/5.10 thf(264,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/sandbox/benchmark/theBenchmark.p',fact_204_of__int__1__le__iff)).
% 17.33/5.10 thf(1264,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)],[264])).
% 17.33/5.10 thf(354,axiom,((! [A:real,B:real]: (ord_less_eq_real @ (minus_minus_real @ (abs_abs_real @ A) @ (abs_abs_real @ B)) @ (abs_abs_real @ (minus_minus_real @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_261_abs__triangle__ineq2)).
% 17.33/5.10 thf(1511,plain,((! [A:real,B:real]: (ord_less_eq_real @ (minus_minus_real @ (abs_abs_real @ A) @ (abs_abs_real @ B)) @ (abs_abs_real @ (minus_minus_real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[354])).
% 17.33/5.10 thf(119,axiom,((((=) @ finite964658038_int_n) = (^ [A:finite964658038_int_n,B:finite964658038_int_n]: ! [C:n]: ((finite566214509_int_n @ A @ C) = (finite566214509_int_n @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_39_vec__eq__iff)).
% 17.33/5.10 thf(802,plain,((((=) @ finite964658038_int_n) = (^ [A:finite964658038_int_n,B:finite964658038_int_n]: ! [C:n]: ((finite566214509_int_n @ A @ C) = (finite566214509_int_n @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 17.33/5.10 thf(237,axiom,((! [A:real]: (ord_less_eq_real @ (minus_minus_real @ A @ one_one_real) @ (ring_1_of_int_real @ (archim1031974863r_real @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_270_real__of__int__floor__ge__diff__one)).
% 17.33/5.10 thf(1191,plain,((! [A:real]: (ord_less_eq_real @ (minus_minus_real @ A @ one_one_real) @ (ring_1_of_int_real @ (archim1031974863r_real @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 17.33/5.10 thf(218,axiom,((! [A:$o,B:finite1183840848l_num1,C:finite1183840848l_num1,D:numeral_num1]: (((A) => ((finite1106245191l_num1 @ (if_Fin1668193290l_num1 @ A @ B @ C) @ D) = (finite1106245191l_num1 @ B @ D))) & ((~ (A)) => ((finite1106245191l_num1 @ (if_Fin1668193290l_num1 @ A @ B @ C) @ D) = (finite1106245191l_num1 @ C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_cond__component)).
% 17.33/5.10 thf(1132,plain,((! [A:$o,B:finite1183840848l_num1,C:finite1183840848l_num1,D:numeral_num1]: (((A) => ((finite1106245191l_num1 @ (if_Fin1668193290l_num1 @ A @ B @ C) @ D) = (finite1106245191l_num1 @ B @ D))) & ((~ (A)) => ((finite1106245191l_num1 @ (if_Fin1668193290l_num1 @ A @ B @ C) @ D) = (finite1106245191l_num1 @ C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 17.33/5.10 thf(65,axiom,((! [A:int,B:int,C:(int > $o)]: ((ord_less_int @ A @ B) => ((C @ (minus_minus_int @ B @ one_one_int)) => ((! [D:int]: ((ord_less_int @ D @ B) => ((C @ D) => (C @ (minus_minus_int @ D @ one_one_int))))) => (C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_216_int__less__induct)).
% 17.33/5.10 thf(587,plain,((! [A:int,B:int,C:(int > $o)]: ((ord_less_int @ A @ B) => ((C @ (minus_minus_int @ B @ one_one_int)) => ((! [D:int]: ((ord_less_int @ D @ B) => ((C @ D) => (C @ (minus_minus_int @ D @ one_one_int))))) => (C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 17.33/5.10 thf(287,axiom,((! [A:int]: (member_real @ (ring_1_of_int_real @ A) @ ring_1_Ints_real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_49_Ints__of__int)).
% 17.33/5.10 thf(1323,plain,((! [A:int]: (member_real @ (ring_1_of_int_real @ A) @ ring_1_Ints_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[287])).
% 17.33/5.10 thf(72,axiom,((! [A:real]: ((archim1371465213g_real @ (minus_minus_real @ A @ one_one_real)) = (minus_minus_int @ (archim1371465213g_real @ A) @ one_one_int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_134_ceiling__diff__one)).
% 17.33/5.10 thf(619,plain,((! [A:real]: ((archim1371465213g_real @ (minus_minus_real @ A @ one_one_real)) = (minus_minus_int @ (archim1371465213g_real @ A) @ one_one_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 17.33/5.10 thf(128,axiom,((! [A:int,B:(real > int),C:real,D:real]: ((A = (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_int @ (B @ E) @ (B @ F)))) => (ord_less_eq_int @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_350_ord__eq__le__subst)).
% 17.33/5.10 thf(838,plain,((! [A:int,B:(real > int),C:real,D:real]: ((A = (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_int @ (B @ E) @ (B @ F)))) => (ord_less_eq_int @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 17.33/5.10 thf(283,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n,D:finite1489363574real_n]: (((minus_1037315151real_n @ A @ B) = (minus_1037315151real_n @ C @ D)) => ((ord_le1017090250real_n @ A @ B) = (ord_le1017090250real_n @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_165_diff__eq__diff__less)).
% 17.33/5.10 thf(1313,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n,D:finite1489363574real_n]: (((minus_1037315151real_n @ A @ B) = (minus_1037315151real_n @ C @ D)) => ((ord_le1017090250real_n @ A @ B) = (ord_le1017090250real_n @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[283])).
% 17.33/5.10 thf(271,axiom,((! [A:real,B:finite1489363574real_n,C:finite1489363574real_n]: ((finite2053577756real_n @ A @ (minus_1037315151real_n @ B @ C)) = (minus_1037315151real_n @ (finite2053577756real_n @ A @ B) @ (finite2053577756real_n @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_vec_Oscale__right__diff__distrib)).
% 17.33/5.10 thf(1279,plain,((! [A:real,B:finite1489363574real_n,C:finite1489363574real_n]: ((finite2053577756real_n @ A @ (minus_1037315151real_n @ B @ C)) = (minus_1037315151real_n @ (finite2053577756real_n @ A @ B) @ (finite2053577756real_n @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 17.33/5.10 thf(53,axiom,((! [A:real,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((finite1961675766l_num1 @ A @ (minus_249161513l_num1 @ B @ C)) = (minus_249161513l_num1 @ (finite1961675766l_num1 @ A @ B) @ (finite1961675766l_num1 @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_vec_Oscale__right__diff__distrib)).
% 17.33/5.10 thf(542,plain,((! [A:real,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((finite1961675766l_num1 @ A @ (minus_249161513l_num1 @ B @ C)) = (minus_249161513l_num1 @ (finite1961675766l_num1 @ A @ B) @ (finite1961675766l_num1 @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 17.33/5.10 thf(33,axiom,((! [A:numeral_num1]: ((finite1800583751l_num1 @ one_on601734293l_num1 @ A) = one_one_int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_100_one__index)).
% 17.33/5.10 thf(460,plain,((! [A:numeral_num1]: ((finite1800583751l_num1 @ one_on601734293l_num1 @ A) = one_one_int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 17.33/5.10 thf(132,axiom,((! [A:int,B:int,C:(int > real),D:real]: ((ord_less_eq_int @ A @ B) => (((C @ B) = D) => ((! [E:int,F:int]: ((ord_less_eq_int @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_eq_real @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_345_ord__le__eq__subst)).
% 17.33/5.10 thf(853,plain,((! [A:int,B:int,C:(int > real),D:real]: ((ord_less_eq_int @ A @ B) => (((C @ B) = D) => ((! [E:int,F:int]: ((ord_less_eq_int @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_eq_real @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 17.33/5.10 thf(308,axiom,((! [A:int]: ((archim1031974863r_real @ (ring_1_of_int_real @ A)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_112_floor__of__int)).
% 17.33/5.10 thf(1379,plain,((! [A:int]: ((archim1031974863r_real @ (ring_1_of_int_real @ A)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[308])).
% 17.33/5.10 thf(23,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ C @ A) => (ord_less_eq_real @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_313_dual__order_Otrans)).
% 17.33/5.10 thf(421,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ C @ A) => (ord_less_eq_real @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 17.33/5.10 thf(342,axiom,((! [A:real]: ? [B:int]: (ord_less_real @ (ring_1_of_int_real @ B) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_158_ex__of__int__less)).
% 17.33/5.10 thf(1479,plain,((! [A:real]: ? [B:int]: (ord_less_real @ (ring_1_of_int_real @ B) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[342])).
% 17.33/5.10 thf(296,axiom,((member1352538125real_n @ x @ a)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__C1_C_I1_J)).
% 17.33/5.10 thf(1347,plain,((member1352538125real_n @ x @ a)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[296])).
% 17.33/5.10 thf(109,axiom,((! [A:int,B:int,C:int]: ((A = B) => ((ord_less_eq_int @ B @ C) => (ord_less_eq_int @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_324_ord__eq__le__trans)).
% 17.33/5.10 thf(770,plain,((! [A:int,B:int,C:int]: ((A = B) => ((ord_less_eq_int @ B @ C) => (ord_less_eq_int @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 17.33/5.10 thf(21,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((real_V488409631l_num1 @ (minus_249161513l_num1 @ A @ B) @ A) = (real_V400292255l_num1 @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_127_dist__diff_I2_J)).
% 17.33/5.10 thf(416,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((real_V488409631l_num1 @ (minus_249161513l_num1 @ A @ B) @ A) = (real_V400292255l_num1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 17.33/5.10 thf(206,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((if_Fin127821360real_n @ ($false) @ A @ B) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_2_1_If_001t__Finite____Cartesian____Product__Ovec_It__Real__Oreal_Mtf__n_J_T)).
% 17.33/5.10 thf(1100,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((if_Fin127821360real_n @ ($false) @ A @ B) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 17.33/5.10 thf(30,axiom,((! [A:set_real]: ((collect_real @ (^ [B:real]: (member_real @ B @ A))) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_95_Collect__mem__eq)).
% 17.33/5.10 thf(448,plain,((! [A:set_real]: ((collect_real @ (^ [B:real]: (member_real @ B @ A))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 17.33/5.10 thf(348,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n]: ((ord_le866583254real_n @ A @ B) => (ord_le866583254real_n @ (minus_1037315151real_n @ A @ C) @ (minus_1037315151real_n @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_225_diff__right__mono)).
% 17.33/5.10 thf(1494,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n]: ((ord_le866583254real_n @ A @ B) => (ord_le866583254real_n @ (minus_1037315151real_n @ A @ C) @ (minus_1037315151real_n @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[348])).
% 17.33/5.10 thf(346,axiom,((ord_le866583254real_n = (^ [A:finite1489363574real_n,B:finite1489363574real_n]: ! [C:n]: (ord_less_eq_real @ (finite772340589real_n @ A @ C) @ (finite772340589real_n @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_212_less__eq__vec__def)).
% 17.33/5.10 thf(1489,plain,(((ord_le866583254real_n) = (^ [A:finite1489363574real_n,B:finite1489363574real_n]: ! [C:n]: (ord_less_eq_real @ (finite772340589real_n @ A @ C) @ (finite772340589real_n @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[346])).
% 17.33/5.10 thf(153,axiom,((! [A:$o,B:finite2063899472l_num1,C:finite2063899472l_num1,D:numeral_num1]: (((A) => ((finite1800583751l_num1 @ (if_Fin1570437642l_num1 @ A @ B @ C) @ D) = (finite1800583751l_num1 @ B @ D))) & ((~ (A)) => ((finite1800583751l_num1 @ (if_Fin1570437642l_num1 @ A @ B @ C) @ D) = (finite1800583751l_num1 @ C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_cond__component)).
% 17.33/5.10 thf(924,plain,((! [A:$o,B:finite2063899472l_num1,C:finite2063899472l_num1,D:numeral_num1]: (((A) => ((finite1800583751l_num1 @ (if_Fin1570437642l_num1 @ A @ B @ C) @ D) = (finite1800583751l_num1 @ B @ D))) & ((~ (A)) => ((finite1800583751l_num1 @ (if_Fin1570437642l_num1 @ A @ B @ C) @ D) = (finite1800583751l_num1 @ C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 17.33/5.10 thf(337,axiom,((! [A:real]: (ord_less_real @ (minus_minus_real @ A @ one_one_real) @ (ring_1_of_int_real @ (archim1031974863r_real @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_189_real__of__int__floor__gt__diff__one)).
% 17.33/5.10 thf(1465,plain,((! [A:real]: (ord_less_real @ (minus_minus_real @ A @ one_one_real) @ (ring_1_of_int_real @ (archim1031974863r_real @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[337])).
% 17.33/5.10 thf(306,axiom,((! [A:finite1183840848l_num1,B:real,C:numeral_num1]: ((ord_less_real @ (real_V400292255l_num1 @ A) @ B) => (ord_less_real @ (abs_abs_real @ (finite1106245191l_num1 @ A @ C)) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_160_norm__bound__component__lt__cart)).
% 17.33/5.10 thf(1373,plain,((! [A:finite1183840848l_num1,B:real,C:numeral_num1]: ((ord_less_real @ (real_V400292255l_num1 @ A) @ B) => (ord_less_real @ (abs_abs_real @ (finite1106245191l_num1 @ A @ C)) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[306])).
% 17.33/5.10 thf(188,axiom,((((=) @ int) = (^ [A:int,B:int]: ((ord_less_eq_int @ A @ B) & (ord_less_eq_int @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_342_eq__iff)).
% 17.33/5.10 thf(1040,plain,((((=) @ int) = (^ [A:int,B:int]: ((ord_less_eq_int @ A @ B) & (ord_less_eq_int @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 17.33/5.10 thf(6,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((if_Fin1668193290l_num1 @ ($false) @ A @ B) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_2_1_If_001t__Finite____Cartesian____Product__Ovec_It__Real__Oreal_Mt__Numeral____Type__Onum1_J_T)).
% 17.33/5.10 thf(376,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((if_Fin1668193290l_num1 @ ($false) @ A @ B) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 17.33/5.10 thf(320,axiom,((! [A:finite2063899472l_num1,B:numeral_num1]: ((finite1106245191l_num1 @ (minkow19073400691_real @ A) @ B) = (ring_1_of_int_real @ (finite1800583751l_num1 @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_20_of__int__vec__nth)).
% 17.33/5.10 thf(1418,plain,((! [A:finite2063899472l_num1,B:numeral_num1]: ((finite1106245191l_num1 @ (minkow19073400691_real @ A) @ B) = (ring_1_of_int_real @ (finite1800583751l_num1 @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[320])).
% 17.33/5.10 thf(78,axiom,((member1352538125real_n @ one_on1253059131real_n @ ring_1723899781real_n)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_180_Ints__1)).
% 17.33/5.10 thf(646,plain,((member1352538125real_n @ one_on1253059131real_n @ ring_1723899781real_n)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 17.33/5.10 thf(223,axiom,((! [A:real]: ((archim1031974863r_real @ (minus_minus_real @ A @ one_one_real)) = (minus_minus_int @ (archim1031974863r_real @ A) @ one_one_int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_133_floor__diff__one)).
% 17.33/5.10 thf(1151,plain,((! [A:real]: ((archim1031974863r_real @ (minus_minus_real @ A @ one_one_real)) = (minus_minus_int @ (archim1031974863r_real @ A) @ one_one_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 17.33/5.10 thf(183,axiom,((! [A:$o,B:finite964658038_int_n,C:finite964658038_int_n,D:n]: (((A) => ((finite566214509_int_n @ (if_Fin1767949360_int_n @ A @ B @ C) @ D) = (finite566214509_int_n @ B @ D))) & ((~ (A)) => ((finite566214509_int_n @ (if_Fin1767949360_int_n @ A @ B @ C) @ D) = (finite566214509_int_n @ C @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_73_cond__component)).
% 17.33/5.10 thf(1020,plain,((! [A:$o,B:finite964658038_int_n,C:finite964658038_int_n,D:n]: (((A) => ((finite566214509_int_n @ (if_Fin1767949360_int_n @ A @ B @ C) @ D) = (finite566214509_int_n @ B @ D))) & ((~ (A)) => ((finite566214509_int_n @ (if_Fin1767949360_int_n @ A @ B @ C) @ D) = (finite566214509_int_n @ C @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 17.33/5.10 thf(124,axiom,((! [A:real,B:real,C:real]: ((minus_minus_real @ (minus_minus_real @ A @ B) @ C) = (minus_minus_real @ (minus_minus_real @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_59_diff__right__commute)).
% 17.33/5.10 thf(821,plain,((! [A:real,B:real,C:real]: ((minus_minus_real @ (minus_minus_real @ A @ B) @ C) = (minus_minus_real @ (minus_minus_real @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 17.33/5.10 thf(147,axiom,((((=) @ real) = (^ [A:real,B:real]: ((ord_less_eq_real @ B @ A) & (ord_less_eq_real @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_311_dual__order_Oeq__iff)).
% 17.33/5.10 thf(905,plain,((((=) @ real) = (^ [A:real,B:real]: ((ord_less_eq_real @ B @ A) & (ord_less_eq_real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 17.33/5.10 thf(66,axiom,((! [A:real,B:real]: ((ord_less_int @ (archim1371465213g_real @ A) @ (archim1371465213g_real @ B)) => (ord_less_real @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_151_ceiling__less__cancel)).
% 17.33/5.10 thf(602,plain,((! [A:real,B:real]: ((ord_less_int @ (archim1371465213g_real @ A) @ (archim1371465213g_real @ B)) => (ord_less_real @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 17.33/5.10 thf(138,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: (((finite1106245191l_num1 @ A) = (finite1106245191l_num1 @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_67_vec__nth__inject)).
% 17.33/5.10 thf(877,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: (((finite1106245191l_num1 @ A) = (finite1106245191l_num1 @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 17.33/5.10 thf(329,axiom,((real_V488409631l_num1 = (^ [A:finite1183840848l_num1,B:finite1183840848l_num1]: (abs_abs_real @ (minus_minus_real @ (finite1106245191l_num1 @ A @ one_one_Numeral_num1) @ (finite1106245191l_num1 @ B @ one_one_Numeral_num1)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_277_dist__real)).
% 17.33/5.10 thf(1447,plain,(((real_V488409631l_num1) = (^ [A:finite1183840848l_num1,B:finite1183840848l_num1]: (abs_abs_real @ (minus_minus_real @ (finite1106245191l_num1 @ A @ one_one_Numeral_num1) @ (finite1106245191l_num1 @ B @ one_one_Numeral_num1)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[329])).
% 17.33/5.10 thf(212,axiom,((ord_less_eq_real @ one_one_real @ one_one_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_211_le__numeral__extra_I4_J)).
% 17.33/5.10 thf(1119,plain,((ord_less_eq_real @ one_one_real @ one_one_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 17.33/5.10 thf(14,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1,D:finite1183840848l_num1]: ((ord_le1724070576l_num1 @ A @ B) => ((ord_le1724070576l_num1 @ C @ D) => (ord_le1724070576l_num1 @ (minus_249161513l_num1 @ A @ D) @ (minus_249161513l_num1 @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_234_diff__mono)).
% 17.33/5.10 thf(396,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1,D:finite1183840848l_num1]: ((ord_le1724070576l_num1 @ A @ B) => ((ord_le1724070576l_num1 @ C @ D) => (ord_le1724070576l_num1 @ (minus_249161513l_num1 @ A @ D) @ (minus_249161513l_num1 @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 17.33/5.10 thf(176,axiom,((! [A:int,B:int,C:int]: ((ord_less_eq_int @ A @ B) => (ord_less_eq_int @ (minus_minus_int @ A @ C) @ (minus_minus_int @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_227_diff__right__mono)).
% 17.33/5.10 thf(998,plain,((! [A:int,B:int,C:int]: ((ord_less_eq_int @ A @ B) => (ord_less_eq_int @ (minus_minus_int @ A @ C) @ (minus_minus_int @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 17.33/5.10 thf(173,axiom,((! [A:real,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((finite1961675766l_num1 @ A @ (minus_249161513l_num1 @ B @ C)) = (minus_249161513l_num1 @ (finite1961675766l_num1 @ A @ B) @ (finite1961675766l_num1 @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_119_vector__ssub__ldistrib)).
% 17.33/5.10 thf(988,plain,((! [A:real,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((finite1961675766l_num1 @ A @ (minus_249161513l_num1 @ B @ C)) = (minus_249161513l_num1 @ (finite1961675766l_num1 @ A @ B) @ (finite1961675766l_num1 @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 17.33/5.10 thf(324,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/sandbox/benchmark/theBenchmark.p',fact_218_ceiling__le)).
% 17.33/5.10 thf(1433,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)],[324])).
% 17.33/5.10 thf(241,axiom,((! [A:int]: ((ring_1_of_int_int @ (abs_abs_int @ A)) = (abs_abs_int @ (ring_1_of_int_int @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_8_of__int__abs)).
% 17.33/5.10 thf(1201,plain,((! [A:int]: ((ring_1_of_int_int @ (abs_abs_int @ A)) = (abs_abs_int @ (ring_1_of_int_int @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 17.33/5.10 thf(50,axiom,((! [A:numeral_num1,B:real]: ((finite1106245191l_num1 @ (finite15144922381_real @ A @ B) @ A) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_83_axis__nth)).
% 17.33/5.10 thf(507,plain,((! [A:numeral_num1,B:real]: ((finite1106245191l_num1 @ (finite15144922381_real @ A @ B) @ A) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 17.33/5.10 thf(86,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((ord_le2035778724l_num1 @ A @ B) => (ord_le2035778724l_num1 @ (minus_249161513l_num1 @ A @ C) @ (minus_249161513l_num1 @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_174_diff__strict__right__mono)).
% 17.33/5.10 thf(678,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((ord_le2035778724l_num1 @ A @ B) => (ord_le2035778724l_num1 @ (minus_249161513l_num1 @ A @ C) @ (minus_249161513l_num1 @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 17.33/5.10 thf(326,axiom,((! [A:int]: ((abs_abs_int @ (abs_abs_int @ A)) = (abs_abs_int @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_24_abs__abs)).
% 17.33/5.10 thf(1438,plain,((! [A:int]: ((abs_abs_int @ (abs_abs_int @ A)) = (abs_abs_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[326])).
% 17.33/5.10 thf(105,axiom,((((?) @ numeral_num1) = (^ [A:(numeral_num1 > $o)]: (A @ one_one_Numeral_num1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_353_ex__1)).
% 17.33/5.10 thf(761,plain,((((?) @ numeral_num1) = (^ [A:(numeral_num1 > $o)]: (A @ one_one_Numeral_num1)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 17.33/5.10 thf(293,axiom,((! [A:finite964658038_int_n,B:n]: ((finite772340589real_n @ (minkow1134813771n_real @ A) @ B) = (ring_1_of_int_real @ (finite566214509_int_n @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_19_of__int__vec__nth)).
% 17.33/5.10 thf(1338,plain,((! [A:finite964658038_int_n,B:n]: ((finite772340589real_n @ (minkow1134813771n_real @ A) @ B) = (ring_1_of_int_real @ (finite566214509_int_n @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[293])).
% 17.33/5.10 thf(1,conjecture,(((ring_1_of_int_real @ (abs_abs_int @ m)) = (abs_abs_real @ (finite772340589real_n @ (minus_1037315151real_n @ x @ y) @ i)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 17.33/5.10 thf(2,negated_conjecture,((~ ((ring_1_of_int_real @ (abs_abs_int @ m)) = (abs_abs_real @ (finite772340589real_n @ (minus_1037315151real_n @ x @ y) @ i))))),inference(neg_conjecture,[status(cth)],[1])).
% 17.33/5.10 thf(366,plain,((~ ((ring_1_of_int_real @ (abs_abs_int @ m)) = (abs_abs_real @ (finite772340589real_n @ (minus_1037315151real_n @ x @ y) @ i))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 17.33/5.10 thf(157,axiom,((~ (ord_less_real @ one_one_real @ one_one_real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_193_less__numeral__extra_I4_J)).
% 17.33/5.10 thf(942,plain,((~ (ord_less_real @ one_one_real @ one_one_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 17.33/5.10 thf(29,axiom,((! [A:real,B:(real > real),C:real,D:real]: ((A = (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_eq_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_351_ord__eq__le__subst)).
% 17.33/5.10 thf(439,plain,((! [A:real,B:(real > real),C:real,D:real]: ((A = (B @ C)) => ((ord_less_eq_real @ C @ D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_eq_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 17.33/5.10 thf(191,axiom,(((ring_1_of_int_int @ one_one_int) = one_one_int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_106_of__int__1)).
% 17.33/5.10 thf(1047,plain,(((ring_1_of_int_int @ one_one_int) = one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 17.33/5.10 thf(117,axiom,((! [A:int,B:int]: ((ord_less_int @ (ring_1_of_int_int @ A) @ (ring_1_of_int_int @ B)) = (ord_less_int @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_97_of__int__less__iff)).
% 17.33/5.10 thf(798,plain,((! [A:int,B:int]: ((ord_less_int @ (ring_1_of_int_int @ A) @ (ring_1_of_int_int @ B)) = (ord_less_int @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 17.33/5.10 thf(195,axiom,((! [A:real]: ((ord_less_int @ (archim1031974863r_real @ A) @ one_one_int) = (ord_less_real @ A @ one_one_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_131_floor__less__one)).
% 17.33/5.10 thf(1057,plain,((! [A:real]: ((ord_less_int @ (archim1031974863r_real @ A) @ one_one_int) = (ord_less_real @ A @ one_one_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 17.33/5.10 thf(269,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: (ord_le866583254real_n @ (minus_1037315151real_n @ (abs_ab1599551059real_n @ A) @ (abs_ab1599551059real_n @ B)) @ (abs_ab1599551059real_n @ (minus_1037315151real_n @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_250_abs__triangle__ineq2__sym)).
% 17.33/5.10 thf(1274,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: (ord_le866583254real_n @ (minus_1037315151real_n @ (abs_ab1599551059real_n @ A) @ (abs_ab1599551059real_n @ B)) @ (abs_ab1599551059real_n @ (minus_1037315151real_n @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 17.33/5.10 thf(149,axiom,((! [A:int,B:int,C:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ B @ C) => (ord_less_eq_int @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_332_order_Otrans)).
% 17.33/5.10 thf(910,plain,((! [A:int,B:int,C:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ B @ C) => (ord_less_eq_int @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 17.33/5.10 thf(162,axiom,((! [A:real,B:real,C:finite1183840848l_num1]: ((finite1961675766l_num1 @ (minus_minus_real @ A @ B) @ C) = (minus_249161513l_num1 @ (finite1961675766l_num1 @ A @ C) @ (finite1961675766l_num1 @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_87_vec_Oscale__left__diff__distrib)).
% 17.33/5.10 thf(957,plain,((! [A:real,B:real,C:finite1183840848l_num1]: ((finite1961675766l_num1 @ (minus_minus_real @ A @ B) @ C) = (minus_249161513l_num1 @ (finite1961675766l_num1 @ A @ C) @ (finite1961675766l_num1 @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 17.33/5.10 thf(111,axiom,((! [A:set_Fi1058188332real_n]: ((collec321817931real_n @ (^ [B:finite1489363574real_n]: (member1352538125real_n @ B @ A))) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_94_Collect__mem__eq)).
% 17.33/5.10 thf(778,plain,((! [A:set_Fi1058188332real_n]: ((collec321817931real_n @ (^ [B:finite1489363574real_n]: (member1352538125real_n @ B @ A))) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 17.33/5.10 thf(189,axiom,((! [A:int,B:int]: ((~ (ord_less_eq_int @ A @ B)) => (ord_less_eq_int @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_334_le__cases)).
% 17.33/5.10 thf(1042,plain,((! [A:int,B:int]: ((~ (ord_less_eq_int @ A @ B)) => (ord_less_eq_int @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 17.33/5.10 thf(299,axiom,((! [A:finite1183840848l_num1]: ((abs_abs_real @ (real_V400292255l_num1 @ A)) = (real_V400292255l_num1 @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_109_abs__norm__cancel)).
% 17.33/5.10 thf(1355,plain,((! [A:finite1183840848l_num1]: ((abs_abs_real @ (real_V400292255l_num1 @ A)) = (real_V400292255l_num1 @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[299])).
% 17.33/5.10 thf(351,axiom,((! [A:real,B:real]: ((finite667548811real_n @ (minus_minus_real @ A @ B)) = (minus_1037315151real_n @ (finite667548811real_n @ A) @ (finite667548811real_n @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_75_vec__sub)).
% 17.33/5.10 thf(1502,plain,((! [A:real,B:real]: ((finite667548811real_n @ (minus_minus_real @ A @ B)) = (minus_1037315151real_n @ (finite667548811real_n @ A) @ (finite667548811real_n @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[351])).
% 17.33/5.10 thf(24,axiom,((! [A:int]: (ord_less_eq_int @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_316_dual__order_Orefl)).
% 17.33/5.10 thf(424,plain,((! [A:int]: (ord_less_eq_int @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 17.33/5.10 thf(26,axiom,((! [A:real,B:real,C:finite1183840848l_num1]: ((finite1961675766l_num1 @ (minus_minus_real @ A @ B) @ C) = (minus_249161513l_num1 @ (finite1961675766l_num1 @ A @ C) @ (finite1961675766l_num1 @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_78_vector__sub__rdistrib)).
% 17.33/5.10 thf(429,plain,((! [A:real,B:real,C:finite1183840848l_num1]: ((finite1961675766l_num1 @ (minus_minus_real @ A @ B) @ C) = (minus_249161513l_num1 @ (finite1961675766l_num1 @ A @ C) @ (finite1961675766l_num1 @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 17.33/5.10 thf(214,axiom,((! [A:real,B:real,C:real]: ((ord_less_real @ (real_V1934908667t_real @ A @ B) @ C) => (ord_less_real @ (real_V1934908667t_real @ B @ A) @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_146_dist__commute__lessI)).
% 17.33/5.10 thf(1123,plain,((! [A:real,B:real,C:real]: ((ord_less_real @ (real_V1934908667t_real @ A @ B) @ C) => (ord_less_real @ (real_V1934908667t_real @ B @ A) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 17.33/5.10 thf(133,axiom,((! [A:int,B:numeral_num1]: ((finite1800583751l_num1 @ (finite1470207077l_num1 @ A) @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_116_vec__component)).
% 17.33/5.10 thf(862,plain,((! [A:int,B:numeral_num1]: ((finite1800583751l_num1 @ (finite1470207077l_num1 @ A) @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 17.33/5.10 thf(18,axiom,((! [A:finite964658038_int_n,B:finite964658038_int_n]: (((finite566214509_int_n @ A) = (finite566214509_int_n @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_69_vec__nth__inject)).
% 17.33/5.10 thf(407,plain,((! [A:finite964658038_int_n,B:finite964658038_int_n]: (((finite566214509_int_n @ A) = (finite566214509_int_n @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 17.33/5.10 thf(92,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_319_order__trans)).
% 17.33/5.10 thf(693,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 17.33/5.10 thf(114,axiom,((! [A:int,B:int]: ((member_int @ A @ ring_1_Ints_int) => ((member_int @ B @ ring_1_Ints_int) => (member_int @ (minus_minus_int @ A @ B) @ ring_1_Ints_int))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_45_Ints__diff)).
% 17.33/5.10 thf(788,plain,((! [A:int,B:int]: ((member_int @ A @ ring_1_Ints_int) => ((member_int @ B @ ring_1_Ints_int) => (member_int @ (minus_minus_int @ A @ B) @ ring_1_Ints_int))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 17.33/5.10 thf(305,axiom,((! [A:int,B:int]: ((ring_11737179077real_n @ (minus_minus_int @ A @ B)) = (minus_1037315151real_n @ (ring_11737179077real_n @ A) @ (ring_11737179077real_n @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_11_of__int__diff)).
% 17.33/5.10 thf(1370,plain,((! [A:int,B:int]: ((ring_11737179077real_n @ (minus_minus_int @ A @ B)) = (minus_1037315151real_n @ (ring_11737179077real_n @ A) @ (ring_11737179077real_n @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[305])).
% 17.33/5.10 thf(36,axiom,((! [A:int,B:int]: ((ring_1154201247l_num1 @ (minus_minus_int @ A @ B)) = (minus_249161513l_num1 @ (ring_1154201247l_num1 @ A) @ (ring_1154201247l_num1 @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_of__int__diff)).
% 17.33/5.10 thf(467,plain,((! [A:int,B:int]: ((ring_1154201247l_num1 @ (minus_minus_int @ A @ B)) = (minus_249161513l_num1 @ (ring_1154201247l_num1 @ A) @ (ring_1154201247l_num1 @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 17.33/5.10 thf(185,axiom,((! [A:numeral_num1,B:int]: ((finite1800583751l_num1 @ (finite627713486m1_int @ A @ B) @ A) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_84_axis__nth)).
% 17.33/5.10 thf(1032,plain,((! [A:numeral_num1,B:int]: ((finite1800583751l_num1 @ (finite627713486m1_int @ A @ B) @ A) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 17.33/5.10 thf(303,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n]: ((ord_le1017090250real_n @ A @ B) => (ord_le1017090250real_n @ (minus_1037315151real_n @ A @ C) @ (minus_1037315151real_n @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_173_diff__strict__right__mono)).
% 17.33/5.10 thf(1365,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n]: ((ord_le1017090250real_n @ A @ B) => (ord_le1017090250real_n @ (minus_1037315151real_n @ A @ C) @ (minus_1037315151real_n @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[303])).
% 17.33/5.10 thf(239,axiom,((! [A:int]: ((real_V646646907m_real @ (ring_1_of_int_real @ A)) = (abs_abs_real @ (ring_1_of_int_real @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_80_norm__of__int)).
% 17.33/5.10 thf(1195,plain,((! [A:int]: ((real_V646646907m_real @ (ring_1_of_int_real @ A)) = (abs_abs_real @ (ring_1_of_int_real @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 17.33/5.10 thf(216,axiom,((! [A:finite1183840848l_num1,B:finite463740460l_num1]: ((! [C:numeral_num1]: (ord_less_eq_real @ (real_V646646907m_real @ (finite1106245191l_num1 @ A @ C)) @ (real_V400292255l_num1 @ (finite1449546019l_num1 @ B @ C)))) => (ord_less_eq_real @ (real_V400292255l_num1 @ A) @ (real_V316032763l_num1 @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_266_norm__le__componentwise__cart)).
% 17.33/5.10 thf(1128,plain,((! [A:finite1183840848l_num1,B:finite463740460l_num1]: ((! [C:numeral_num1]: (ord_less_eq_real @ (real_V646646907m_real @ (finite1106245191l_num1 @ A @ C)) @ (real_V400292255l_num1 @ (finite1449546019l_num1 @ B @ C)))) => (ord_less_eq_real @ (real_V400292255l_num1 @ A) @ (real_V316032763l_num1 @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 17.33/5.10 thf(32,axiom,((! [A:real,B:real]: ((A = B) => (ord_less_eq_real @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_337_eq__refl)).
% 17.33/5.10 thf(456,plain,((! [A:real,B:real]: ((A = B) => (ord_less_eq_real @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 17.33/5.10 thf(168,axiom,((! [A:finite463740460l_num1,B:finite1183840848l_num1]: ((! [C:numeral_num1]: (ord_less_eq_real @ (real_V400292255l_num1 @ (finite1449546019l_num1 @ A @ C)) @ (real_V646646907m_real @ (finite1106245191l_num1 @ B @ C)))) => (ord_less_eq_real @ (real_V316032763l_num1 @ A) @ (real_V400292255l_num1 @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_263_norm__le__componentwise__cart)).
% 17.33/5.10 thf(974,plain,((! [A:finite463740460l_num1,B:finite1183840848l_num1]: ((! [C:numeral_num1]: (ord_less_eq_real @ (real_V400292255l_num1 @ (finite1449546019l_num1 @ A @ C)) @ (real_V646646907m_real @ (finite1106245191l_num1 @ B @ C)))) => (ord_less_eq_real @ (real_V316032763l_num1 @ A) @ (real_V400292255l_num1 @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 17.33/5.10 thf(129,axiom,((member_real @ one_one_real @ ring_1_Ints_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_182_Ints__1)).
% 17.33/5.10 thf(847,plain,((member_real @ one_one_real @ ring_1_Ints_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 17.33/5.10 thf(41,axiom,((! [A:int,B:int,C:int,D:int]: (((minus_minus_int @ A @ B) = (minus_minus_int @ C @ D)) => ((ord_less_eq_int @ A @ B) = (ord_less_eq_int @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_223_diff__eq__diff__less__eq)).
% 17.33/5.10 thf(484,plain,((! [A:int,B:int,C:int,D:int]: (((minus_minus_int @ A @ B) = (minus_minus_int @ C @ D)) => ((ord_less_eq_int @ A @ B) = (ord_less_eq_int @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 17.33/5.10 thf(277,axiom,((! [A:n,B:real]: ((finite772340589real_n @ (finite703491444n_real @ A @ B) @ A) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_82_axis__nth)).
% 17.33/5.10 thf(1296,plain,((! [A:n,B:real]: ((finite772340589real_n @ (finite703491444n_real @ A @ B) @ A) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[277])).
% 17.33/5.10 thf(81,axiom,((((=) @ real) = (^ [A:real,B:real]: ((ord_less_eq_real @ A @ B) & (ord_less_eq_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_343_eq__iff)).
% 17.33/5.10 thf(665,plain,((((=) @ real) = (^ [A:real,B:real]: ((ord_less_eq_real @ A @ B) & (ord_less_eq_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 17.33/5.10 thf(44,axiom,((((!) @ numeral_num1) = (^ [A:(numeral_num1 > $o)]: (A @ one_one_Numeral_num1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_352_forall__1)).
% 17.33/5.10 thf(493,plain,((((!) @ numeral_num1) = (^ [A:(numeral_num1 > $o)]: (A @ one_one_Numeral_num1)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 17.33/5.10 thf(244,axiom,((! [A:real,B:real]: ((abs_abs_real @ (real_V1934908667t_real @ A @ B)) = (real_V1934908667t_real @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_191_real__abs__dist)).
% 17.33/5.10 thf(1210,plain,((! [A:real,B:real]: ((abs_abs_real @ (real_V1934908667t_real @ A @ B)) = (real_V1934908667t_real @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 17.33/5.10 thf(301,axiom,((! [A:finite1489363574real_n,B:n]: ((member1352538125real_n @ A @ a) => (member_real @ (finite772340589real_n @ A @ B) @ ring_1_Ints_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_40_assms)).
% 17.33/5.10 thf(1360,plain,((! [A:finite1489363574real_n,B:n]: ((member1352538125real_n @ A @ a) => (member_real @ (finite772340589real_n @ A @ B) @ ring_1_Ints_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[301])).
% 17.33/5.10 thf(137,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1,D:finite1183840848l_num1]: ((ord_le2035778724l_num1 @ A @ B) => ((ord_le2035778724l_num1 @ C @ D) => (ord_le2035778724l_num1 @ (minus_249161513l_num1 @ A @ D) @ (minus_249161513l_num1 @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_162_diff__strict__mono)).
% 17.33/5.10 thf(874,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1,D:finite1183840848l_num1]: ((ord_le2035778724l_num1 @ A @ B) => ((ord_le2035778724l_num1 @ C @ D) => (ord_le2035778724l_num1 @ (minus_249161513l_num1 @ A @ D) @ (minus_249161513l_num1 @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 17.33/5.10 thf(80,axiom,((! [A:real,B:real,C:real]: (((ord_less_eq_real @ A @ B) => (~ (ord_less_eq_real @ B @ C))) => (((ord_less_eq_real @ B @ A) => (~ (ord_less_eq_real @ A @ C))) => (((ord_less_eq_real @ A @ C) => (~ (ord_less_eq_real @ C @ B))) => (((ord_less_eq_real @ C @ B) => (~ (ord_less_eq_real @ B @ A))) => (((ord_less_eq_real @ B @ C) => (~ (ord_less_eq_real @ C @ A))) => (~ ((ord_less_eq_real @ C @ A) => (~ (ord_less_eq_real @ A @ B))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_331_le__cases3)).
% 17.33/5.10 thf(650,plain,((! [A:real,B:real,C:real]: (((ord_less_eq_real @ A @ B) => (~ (ord_less_eq_real @ B @ C))) => (((ord_less_eq_real @ B @ A) => (~ (ord_less_eq_real @ A @ C))) => (((ord_less_eq_real @ A @ C) => (~ (ord_less_eq_real @ C @ B))) => (((ord_less_eq_real @ C @ B) => (~ (ord_less_eq_real @ B @ A))) => (((ord_less_eq_real @ B @ C) => (~ (ord_less_eq_real @ C @ A))) => (~ ((ord_less_eq_real @ C @ A) => (~ (ord_less_eq_real @ A @ B))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 17.33/5.10 thf(364,axiom,((! [A:int,B:int]: ((ord_less_real @ (ring_1_of_int_real @ A) @ (ring_1_of_int_real @ B)) = (ord_less_int @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_96_of__int__less__iff)).
% 17.33/5.10 thf(1534,plain,((! [A:int,B:int]: ((ord_less_real @ (ring_1_of_int_real @ A) @ (ring_1_of_int_real @ B)) = (ord_less_int @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[364])).
% 17.33/5.10 thf(289,axiom,((! [A:finite1489363574real_n,B:real,C:n]: ((ord_less_eq_real @ (real_V739724485real_n @ A) @ B) => (ord_less_eq_real @ (abs_abs_real @ (finite772340589real_n @ A @ C)) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_273_norm__bound__component__le__cart)).
% 17.33/5.10 thf(1328,plain,((! [A:finite1489363574real_n,B:real,C:n]: ((ord_less_eq_real @ (real_V739724485real_n @ A) @ B) => (ord_less_eq_real @ (abs_abs_real @ (finite772340589real_n @ A @ C)) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[289])).
% 17.33/5.10 thf(209,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((ord_le2035778724l_num1 @ A @ B) => (ord_le2035778724l_num1 @ (minus_249161513l_num1 @ C @ B) @ (minus_249161513l_num1 @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_170_diff__strict__left__mono)).
% 17.33/5.10 thf(1111,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((ord_le2035778724l_num1 @ A @ B) => (ord_le2035778724l_num1 @ (minus_249161513l_num1 @ C @ B) @ (minus_249161513l_num1 @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 17.33/5.10 thf(102,axiom,((! [A:real,B:real,C:(real > $o)]: ((ord_less_real @ A @ B) => ((C @ A) => ((~ (C @ B)) => (? [D:real]: ((ord_less_eq_real @ A @ D) & (ord_less_eq_real @ D @ B) & ! [E:real]: (((ord_less_eq_real @ A @ E) & (ord_less_real @ E @ D)) => (C @ E)) & ! [E:real]: ((! [F:real]: (((ord_less_eq_real @ A @ F) & (ord_less_real @ F @ E)) => (C @ F))) => (ord_less_eq_real @ E @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_299_complete__interval)).
% 17.33/5.10 thf(725,plain,((! [A:real,B:real,C:(real > $o)]: ((ord_less_real @ A @ B) => ((C @ A) => ((~ (C @ B)) => (? [D:real]: ((ord_less_eq_real @ A @ D) & (ord_less_eq_real @ D @ B) & ! [E:real]: (((ord_less_eq_real @ A @ E) & (ord_less_real @ E @ D)) => (C @ E)) & ! [E:real]: ((! [F:real]: (((ord_less_eq_real @ A @ F) & (ord_less_real @ F @ E)) => (C @ F))) => (ord_less_eq_real @ E @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 17.33/5.10 thf(11,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((ord_le1724070576l_num1 @ A @ B) => (ord_le1724070576l_num1 @ (minus_249161513l_num1 @ C @ B) @ (minus_249161513l_num1 @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_230_diff__left__mono)).
% 17.33/5.10 thf(388,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((ord_le1724070576l_num1 @ A @ B) => (ord_le1724070576l_num1 @ (minus_249161513l_num1 @ C @ B) @ (minus_249161513l_num1 @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 17.33/5.10 thf(69,axiom,((! [A:int]: ((ord_less_int @ one_one_int @ (ring_1_of_int_int @ A)) = (ord_less_int @ one_one_int @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_121_of__int__1__less__iff)).
% 17.33/5.10 thf(610,plain,((! [A:int]: ((ord_less_int @ one_one_int @ (ring_1_of_int_int @ A)) = (ord_less_int @ one_one_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 17.33/5.10 thf(113,axiom,((! [A:real,B:real,C:real]: ((A = B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_325_ord__eq__le__trans)).
% 17.33/5.10 thf(783,plain,((! [A:real,B:real,C:real]: ((A = B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 17.33/5.10 thf(202,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((abs_ab948591917l_num1 @ (minus_249161513l_num1 @ A @ B)) = (abs_ab948591917l_num1 @ (minus_249161513l_num1 @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_31_abs__minus__commute)).
% 17.33/5.10 thf(1089,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((abs_ab948591917l_num1 @ (minus_249161513l_num1 @ A @ B)) = (abs_ab948591917l_num1 @ (minus_249161513l_num1 @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 17.33/5.10 thf(253,axiom,((! [A:real,B:real,C:finite1489363574real_n]: ((finite2053577756real_n @ (minus_minus_real @ A @ B) @ C) = (minus_1037315151real_n @ (finite2053577756real_n @ A @ C) @ (finite2053577756real_n @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_vec_Oscale__left__diff__distrib)).
% 17.33/5.10 thf(1234,plain,((! [A:real,B:real,C:finite1489363574real_n]: ((finite2053577756real_n @ (minus_minus_real @ A @ B) @ C) = (minus_1037315151real_n @ (finite2053577756real_n @ A @ C) @ (finite2053577756real_n @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 17.33/5.10 thf(266,axiom,((ord_less_real @ (real_V783965509real_n @ y @ x) @ one_one_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_79__C1_C_I3_J)).
% 17.33/5.10 thf(1270,plain,((ord_less_real @ (real_V783965509real_n @ y @ x) @ one_one_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 17.33/5.10 thf(262,axiom,((! [A:real,B:real]: ((abs_abs_real @ (minus_minus_real @ A @ B)) = (abs_abs_real @ (minus_minus_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_abs__minus__commute)).
% 17.33/5.10 thf(1259,plain,((! [A:real,B:real]: ((abs_abs_real @ (minus_minus_real @ A @ B)) = (abs_abs_real @ (minus_minus_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 17.33/5.10 thf(154,axiom,((! [A:int,B:int,C:int]: ((ord_less_eq_int @ A @ B) => (ord_less_eq_int @ (minus_minus_int @ C @ B) @ (minus_minus_int @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_231_diff__left__mono)).
% 17.33/5.10 thf(933,plain,((! [A:int,B:int,C:int]: ((ord_less_eq_int @ A @ B) => (ord_less_eq_int @ (minus_minus_int @ C @ B) @ (minus_minus_int @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 17.33/5.10 thf(233,axiom,(((ring_1_of_int_real @ one_one_int) = one_one_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_105_of__int__1)).
% 17.33/5.10 thf(1182,plain,(((ring_1_of_int_real @ one_one_int) = one_one_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 17.33/5.10 thf(335,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: (ord_less_eq_real @ (minus_minus_real @ (real_V739724485real_n @ A) @ (real_V739724485real_n @ B)) @ (real_V739724485real_n @ (minus_1037315151real_n @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_280_norm__triangle__ineq2)).
% 17.33/5.10 thf(1461,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: (ord_less_eq_real @ (minus_minus_real @ (real_V739724485real_n @ A) @ (real_V739724485real_n @ B)) @ (real_V739724485real_n @ (minus_1037315151real_n @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[335])).
% 17.33/5.10 thf(97,axiom,((! [A:real,B:real,C:(real > real),D:real]: ((ord_less_eq_real @ A @ B) => (((C @ B) = D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_eq_real @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_347_ord__le__eq__subst)).
% 17.33/5.10 thf(706,plain,((! [A:real,B:real,C:(real > real),D:real]: ((ord_less_eq_real @ A @ B) => (((C @ B) = D) => ((! [E:real,F:real]: ((ord_less_eq_real @ E @ F) => (ord_less_eq_real @ (C @ E) @ (C @ F)))) => (ord_less_eq_real @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 17.33/5.10 thf(89,axiom,((! [A:real]: ((one_one_real = A) = (A = one_one_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_135_one__reorient)).
% 17.33/5.10 thf(686,plain,((! [A:real]: ((one_one_real = A) = (A = one_one_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 17.33/5.10 thf(199,axiom,((real_V1934908667t_real = (^ [A:real,B:real]: (real_V1934908667t_real @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_dist__commute)).
% 17.33/5.10 thf(1075,plain,(((real_V1934908667t_real) = (^ [A:real,B:real]: (real_V1934908667t_real @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 17.33/5.10 thf(181,axiom,((! [A:real,B:real]: ((finite1329045861l_num1 @ (minus_minus_real @ A @ B)) = (minus_249161513l_num1 @ (finite1329045861l_num1 @ A) @ (finite1329045861l_num1 @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_76_vec__sub)).
% 17.33/5.10 thf(1016,plain,((! [A:real,B:real]: ((finite1329045861l_num1 @ (minus_minus_real @ A @ B)) = (minus_249161513l_num1 @ (finite1329045861l_num1 @ A) @ (finite1329045861l_num1 @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 17.33/5.10 thf(243,axiom,((! [A:finite1489363574real_n,B:real,C:n]: ((ord_less_real @ (real_V739724485real_n @ A) @ B) => (ord_less_real @ (abs_abs_real @ (finite772340589real_n @ A @ C)) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_159_norm__bound__component__lt__cart)).
% 17.33/5.10 thf(1207,plain,((! [A:finite1489363574real_n,B:real,C:n]: ((ord_less_real @ (real_V739724485real_n @ A) @ B) => (ord_less_real @ (abs_abs_real @ (finite772340589real_n @ A @ C)) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 17.33/5.10 thf(73,axiom,((ord_le1908593622_int_n = (^ [A:finite964658038_int_n,B:finite964658038_int_n]: ! [C:n]: (ord_less_eq_int @ (finite566214509_int_n @ A @ C) @ (finite566214509_int_n @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_215_less__eq__vec__def)).
% 17.33/5.10 thf(622,plain,(((ord_le1908593622_int_n) = (^ [A:finite964658038_int_n,B:finite964658038_int_n]: ! [C:n]: (ord_less_eq_int @ (finite566214509_int_n @ A @ C) @ (finite566214509_int_n @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 17.33/5.10 thf(79,axiom,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ B @ A) = (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_328_antisym__conv)).
% 17.33/5.10 thf(647,plain,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ B @ A) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 17.33/5.10 thf(172,axiom,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => (ord_less_real @ (minus_minus_real @ C @ B) @ (minus_minus_real @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_171_diff__strict__left__mono)).
% 17.33/5.10 thf(985,plain,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => (ord_less_real @ (minus_minus_real @ C @ B) @ (minus_minus_real @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 17.33/5.10 thf(95,axiom,((! [A:finite964658038_int_n,B:n]: ((finite566214509_int_n @ (minkow1468704075_n_int @ A) @ B) = (ring_1_of_int_int @ (finite566214509_int_n @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_18_of__int__vec__nth)).
% 17.33/5.10 thf(701,plain,((! [A:finite964658038_int_n,B:n]: ((finite566214509_int_n @ (minkow1468704075_n_int @ A) @ B) = (ring_1_of_int_int @ (finite566214509_int_n @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 17.33/5.10 thf(259,axiom,((! [A:real,B:n]: ((finite772340589real_n @ (finite667548811real_n @ A) @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_114_vec__component)).
% 17.33/5.10 thf(1249,plain,((! [A:real,B:n]: ((finite772340589real_n @ (finite667548811real_n @ A) @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 17.33/5.10 thf(331,axiom,((real_V400292255l_num1 = (^ [A:finite1183840848l_num1]: (abs_abs_real @ (finite1106245191l_num1 @ A @ one_one_Numeral_num1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_247_norm__real)).
% 17.33/5.10 thf(1451,plain,(((real_V400292255l_num1) = (^ [A:finite1183840848l_num1]: (abs_abs_real @ (finite1106245191l_num1 @ A @ one_one_Numeral_num1))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[331])).
% 17.33/5.10 thf(252,axiom,((! [A:real,B:int]: ((ord_less_int @ (archim1371465213g_real @ A) @ B) = (ord_less_eq_real @ A @ (minus_minus_real @ (ring_1_of_int_real @ B) @ one_one_real))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_249_ceiling__less__iff)).
% 17.33/5.10 thf(1231,plain,((! [A:real,B:int]: ((ord_less_int @ (archim1371465213g_real @ A) @ B) = (ord_less_eq_real @ A @ (minus_minus_real @ (ring_1_of_int_real @ B) @ one_one_real))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 17.33/5.10 thf(196,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/sandbox/benchmark/theBenchmark.p',fact_307_complete__real)).
% 17.33/5.10 thf(1060,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)],[196])).
% 17.33/5.10 thf(258,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n,D:finite1489363574real_n]: ((ord_le866583254real_n @ A @ B) => ((ord_le866583254real_n @ C @ D) => (ord_le866583254real_n @ (minus_1037315151real_n @ A @ D) @ (minus_1037315151real_n @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_233_diff__mono)).
% 17.33/5.10 thf(1246,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n,D:finite1489363574real_n]: ((ord_le866583254real_n @ A @ B) => ((ord_le866583254real_n @ C @ D) => (ord_le866583254real_n @ (minus_1037315151real_n @ A @ D) @ (minus_1037315151real_n @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 17.33/5.10 thf(360,axiom,((! [A:n]: ((finite772340589real_n @ one_on1253059131real_n @ A) = one_one_real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_98_one__index)).
% 17.33/5.10 thf(1525,plain,((! [A:n]: ((finite772340589real_n @ one_on1253059131real_n @ A) = one_one_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[360])).
% 17.33/5.10 thf(13,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((ord_le1724070576l_num1 @ A @ B) => (ord_le1724070576l_num1 @ (minus_249161513l_num1 @ A @ C) @ (minus_249161513l_num1 @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_226_diff__right__mono)).
% 17.33/5.10 thf(393,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((ord_le1724070576l_num1 @ A @ B) => (ord_le1724070576l_num1 @ (minus_249161513l_num1 @ A @ C) @ (minus_249161513l_num1 @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 17.33/5.10 thf(210,axiom,((! [A:real]: (ord_less_eq_int @ (minus_minus_int @ (archim1371465213g_real @ A) @ (archim1031974863r_real @ A)) @ one_one_int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_248_ceiling__diff__floor__le__1)).
% 17.33/5.10 thf(1114,plain,((! [A:real]: (ord_less_eq_int @ (minus_minus_int @ (archim1371465213g_real @ A) @ (archim1031974863r_real @ A)) @ one_one_int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 17.33/5.10 thf(333,axiom,((! [A:real]: (((ring_1_of_int_real @ (archim1031974863r_real @ A)) = A) = (? [B:int]: (A = (ring_1_of_int_real @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_188_of__int__floor__cancel)).
% 17.33/5.10 thf(1456,plain,((! [A:real]: (((ring_1_of_int_real @ (archim1031974863r_real @ A)) = A) = (? [B:int]: (A = (ring_1_of_int_real @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[333])).
% 17.33/5.10 thf(309,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: (((finite772340589real_n @ A) = (finite772340589real_n @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_66_vec__nth__inject)).
% 17.33/5.10 thf(1382,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: (((finite772340589real_n @ A) = (finite772340589real_n @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[309])).
% 17.33/5.10 thf(291,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((real_V739724485real_n @ (minus_1037315151real_n @ A @ B)) = (real_V739724485real_n @ (minus_1037315151real_n @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_153_norm__minus__commute)).
% 17.33/5.10 thf(1333,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((real_V739724485real_n @ (minus_1037315151real_n @ A @ B)) = (real_V739724485real_n @ (minus_1037315151real_n @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[291])).
% 17.33/5.10 thf(285,axiom,((! [A:real]: ((abs_abs_real @ (real_V646646907m_real @ A)) = (real_V646646907m_real @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_108_abs__norm__cancel)).
% 17.33/5.10 thf(1318,plain,((! [A:real]: ((abs_abs_real @ (real_V646646907m_real @ A)) = (real_V646646907m_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[285])).
% 17.33/5.10 thf(256,axiom,((! [A:real,B:real]: (ord_less_eq_real @ (minus_minus_real @ (abs_abs_real @ A) @ (abs_abs_real @ B)) @ (abs_abs_real @ (minus_minus_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_253_abs__triangle__ineq2__sym)).
% 17.33/5.10 thf(1241,plain,((! [A:real,B:real]: (ord_less_eq_real @ (minus_minus_real @ (abs_abs_real @ A) @ (abs_abs_real @ B)) @ (abs_abs_real @ (minus_minus_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 17.33/5.10 thf(152,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1,D:finite1183840848l_num1]: (((minus_249161513l_num1 @ A @ B) = (minus_249161513l_num1 @ C @ D)) => ((A = B) = (C = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_65_diff__eq__diff__eq)).
% 17.33/5.10 thf(921,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1,D:finite1183840848l_num1]: (((minus_249161513l_num1 @ A @ B) = (minus_249161513l_num1 @ C @ D)) => ((A = B) = (C = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 17.33/5.10 thf(228,axiom,((! [A:numeral_num1]: ((finite1106245191l_num1 @ one_on1961019669l_num1 @ A) = one_one_real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_99_one__index)).
% 17.33/5.10 thf(1170,plain,((! [A:numeral_num1]: ((finite1106245191l_num1 @ one_on1961019669l_num1 @ A) = one_one_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 17.33/5.10 thf(186,axiom,((! [A:n,B:int]: ((finite566214509_int_n @ (finite1888777460_n_int @ A @ B) @ A) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_85_axis__nth)).
% 17.33/5.10 thf(1035,plain,((! [A:n,B:int]: ((finite566214509_int_n @ (finite1888777460_n_int @ A @ B) @ A) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 17.33/5.10 thf(235,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ (abs_abs_real @ A) @ B) => (ord_less_eq_real @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_240_abs__le__D1)).
% 17.33/5.10 thf(1187,plain,((! [A:real,B:real]: ((ord_less_eq_real @ (abs_abs_real @ A) @ B) => (ord_less_eq_real @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 17.33/5.10 thf(227,axiom,((! [A:real,B:numeral_num1]: ((finite1106245191l_num1 @ (finite1329045861l_num1 @ A) @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_115_vec__component)).
% 17.33/5.10 thf(1167,plain,((! [A:real,B:numeral_num1]: ((finite1106245191l_num1 @ (finite1329045861l_num1 @ A) @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 17.33/5.10 thf(161,axiom,((! [A:finite1183840848l_num1,B:set_Fi1257234438l_num1,C:finite1183840848l_num1]: ((member1413569767l_num1 @ A @ B) => ((member1413569767l_num1 @ C @ B) => ((A = C) = (! [D:finite1183840848l_num1]: ((member1413569767l_num1 @ D @ B) => ((real_V488409631l_num1 @ A @ D) = (real_V488409631l_num1 @ C @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_288_metric__eq__thm)).
% 17.33/5.10 thf(953,plain,((! [A:finite1183840848l_num1,B:set_Fi1257234438l_num1,C:finite1183840848l_num1]: ((member1413569767l_num1 @ A @ B) => ((member1413569767l_num1 @ C @ B) => ((A = C) = (! [D:finite1183840848l_num1]: ((member1413569767l_num1 @ D @ B) => ((real_V488409631l_num1 @ A @ D) = (real_V488409631l_num1 @ C @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 17.33/5.10 thf(116,axiom,((! [A:finite1489363574real_n,B:set_Fi1058188332real_n,C:finite1489363574real_n]: ((member1352538125real_n @ A @ B) => ((member1352538125real_n @ C @ B) => ((A = C) = (! [D:finite1489363574real_n]: ((member1352538125real_n @ D @ B) => ((real_V783965509real_n @ A @ D) = (real_V783965509real_n @ C @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_286_metric__eq__thm)).
% 17.33/5.10 thf(794,plain,((! [A:finite1489363574real_n,B:set_Fi1058188332real_n,C:finite1489363574real_n]: ((member1352538125real_n @ A @ B) => ((member1352538125real_n @ C @ B) => ((A = C) = (! [D:finite1489363574real_n]: ((member1352538125real_n @ D @ B) => ((real_V783965509real_n @ A @ D) = (real_V783965509real_n @ C @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 17.33/5.10 thf(107,axiom,((real_V845814485l_num1 = (^ [A:finite121157254l_num1,B:finite121157254l_num1]: (real_V783965509real_n @ (finite1503577981l_num1 @ A @ one_one_Numeral_num1) @ (finite1503577981l_num1 @ B @ one_one_Numeral_num1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_244_dist__vector__1)).
% 17.33/5.10 thf(765,plain,(((real_V845814485l_num1) = (^ [A:finite121157254l_num1,B:finite121157254l_num1]: (real_V783965509real_n @ (finite1503577981l_num1 @ A @ one_one_Numeral_num1) @ (finite1503577981l_num1 @ B @ one_one_Numeral_num1))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 17.33/5.10 thf(194,axiom,((! [A:finite964658038_int_n,B:finite964658038_int_n]: (((minkow1134813771n_real @ A) = (minkow1134813771n_real @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_42_of__int__vec__eq__iff)).
% 17.33/5.10 thf(1054,plain,((! [A:finite964658038_int_n,B:finite964658038_int_n]: (((minkow1134813771n_real @ A) = (minkow1134813771n_real @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 17.33/5.10 thf(99,axiom,((ord_less_eq_real = (^ [A:real,B:real]: ((ord_less_real @ A @ B) | (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_209_less__eq__real__def)).
% 17.33/5.10 thf(718,plain,(((ord_less_eq_real) = (^ [A:real,B:real]: ((ord_less_real @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 17.33/5.10 thf(142,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((member1413569767l_num1 @ A @ ring_11529266783l_num1) => ((member1413569767l_num1 @ B @ ring_11529266783l_num1) => (member1413569767l_num1 @ (minus_249161513l_num1 @ A @ B) @ ring_11529266783l_num1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_46_Ints__diff)).
% 17.33/5.10 thf(888,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((member1413569767l_num1 @ A @ ring_11529266783l_num1) => ((member1413569767l_num1 @ B @ ring_11529266783l_num1) => (member1413569767l_num1 @ (minus_249161513l_num1 @ A @ B) @ ring_11529266783l_num1))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 17.33/5.10 thf(221,axiom,((! [A:real,B:real]: ((A != B) => ((~ (ord_less_real @ A @ B)) => (ord_less_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_143_linorder__neqE__linordered__idom)).
% 17.33/5.10 thf(1146,plain,((! [A:real,B:real]: ((~ (A = B)) => ((~ (ord_less_real @ A @ B)) => (ord_less_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 17.33/5.10 thf(207,axiom,((! [A:int,B:(int > $o)]: ((member_int @ A @ ring_1_Ints_int) => ((! [C:int]: (B @ (ring_1_of_int_int @ C))) => (B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_53_Ints__induct)).
% 17.33/5.10 thf(1103,plain,((! [A:int,B:(int > $o)]: ((member_int @ A @ ring_1_Ints_int) => ((! [C:int]: (B @ (ring_1_of_int_int @ C))) => (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 17.33/5.10 thf(268,axiom,((member1352538125real_n @ y @ a)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__C1_C_I2_J)).
% 17.33/5.10 thf(1273,plain,((member1352538125real_n @ y @ a)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 17.33/5.10 thf(279,axiom,((! [A:real]: ((member_real @ A @ ring_1_Ints_real) => (~ (! [B:int]: (A != (ring_1_of_int_real @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_55_Ints__cases)).
% 17.33/5.10 thf(1301,plain,((! [A:real]: ((member_real @ A @ ring_1_Ints_real) => (~ (! [B:int]: ~ (A = (ring_1_of_int_real @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[279])).
% 17.33/5.10 thf(60,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_333_order_Otrans)).
% 17.33/5.10 thf(573,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ C) => (ord_less_eq_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 17.33/5.10 thf(90,axiom,((! [A:int]: (member1352538125real_n @ (ring_11737179077real_n @ A) @ ring_1723899781real_n))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_51_Ints__of__int)).
% 17.33/5.10 thf(689,plain,((! [A:int]: (member1352538125real_n @ (ring_11737179077real_n @ A) @ ring_1723899781real_n))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 17.33/5.10 thf(247,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (real_V400292255l_num1 @ A) @ (real_V400292255l_num1 @ B))) @ (real_V400292255l_num1 @ (minus_249161513l_num1 @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_293_norm__triangle__ineq3)).
% 17.33/5.10 thf(1219,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (real_V400292255l_num1 @ A) @ (real_V400292255l_num1 @ B))) @ (real_V400292255l_num1 @ (minus_249161513l_num1 @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 17.33/5.10 thf(125,axiom,((! [A:int,B:int,C:(int > int),D:int]: ((ord_less_eq_int @ A @ B) => (((C @ B) = D) => ((! [E:int,F:int]: ((ord_less_eq_int @ E @ F) => (ord_less_eq_int @ (C @ E) @ (C @ F)))) => (ord_less_eq_int @ (C @ A) @ D)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_344_ord__le__eq__subst)).
% 17.33/5.10 thf(824,plain,((! [A:int,B:int,C:(int > int),D:int]: ((ord_less_eq_int @ A @ B) => (((C @ B) = D) => ((! [E:int,F:int]: ((ord_less_eq_int @ E @ F) => (ord_less_eq_int @ (C @ E) @ (C @ F)))) => (ord_less_eq_int @ (C @ A) @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 17.33/5.10 thf(16,axiom,((! [A:finite2063899472l_num1,B:finite2063899472l_num1]: ((if_Fin1570437642l_num1 @ ($false) @ A @ B) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_2_1_If_001t__Finite____Cartesian____Product__Ovec_It__Int__Oint_Mt__Numeral____Type__Onum1_J_T)).
% 17.33/5.10 thf(402,plain,((! [A:finite2063899472l_num1,B:finite2063899472l_num1]: ((if_Fin1570437642l_num1 @ ($false) @ A @ B) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 17.33/5.10 thf(311,axiom,(((abs_abs_real @ one_one_real) = one_one_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_177_abs__one)).
% 17.33/5.10 thf(1389,plain,(((abs_abs_real @ one_one_real) = one_one_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[311])).
% 17.33/5.10 thf(215,axiom,((! [A:int,B:int]: ((ring_1_of_int_int @ (minus_minus_int @ A @ B)) = (minus_minus_int @ (ring_1_of_int_int @ A) @ (ring_1_of_int_int @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_13_of__int__diff)).
% 17.33/5.10 thf(1125,plain,((! [A:int,B:int]: ((ring_1_of_int_int @ (minus_minus_int @ A @ B)) = (minus_minus_int @ (ring_1_of_int_int @ A) @ (ring_1_of_int_int @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 17.33/5.10 thf(62,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1,D:finite1183840848l_num1]: (((minus_249161513l_num1 @ A @ B) = (minus_249161513l_num1 @ C @ D)) => ((ord_le2035778724l_num1 @ A @ B) = (ord_le2035778724l_num1 @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_166_diff__eq__diff__less)).
% 17.33/5.10 thf(579,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1,D:finite1183840848l_num1]: (((minus_249161513l_num1 @ A @ B) = (minus_249161513l_num1 @ C @ D)) => ((ord_le2035778724l_num1 @ A @ B) = (ord_le2035778724l_num1 @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 17.33/5.10 thf(314,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((real_V783965509real_n @ (minus_1037315151real_n @ A @ B) @ A) = (real_V739724485real_n @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_125_dist__diff_I2_J)).
% 17.33/5.10 thf(1403,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((real_V783965509real_n @ (minus_1037315151real_n @ A @ B) @ A) = (real_V739724485real_n @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[314])).
% 17.33/5.10 thf(358,axiom,((! [A:int,B:int]: ((ord_less_eq_int @ (abs_abs_int @ A) @ B) => (ord_less_eq_int @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_239_abs__le__D1)).
% 17.33/5.10 thf(1520,plain,((! [A:int,B:int]: ((ord_less_eq_int @ (abs_abs_int @ A) @ B) => (ord_less_eq_int @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[358])).
% 17.33/5.10 thf(20,axiom,((! [A:int,B:int,C:int,D:int]: (((minus_minus_int @ A @ B) = (minus_minus_int @ C @ D)) => ((A = B) = (C = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_64_diff__eq__diff__eq)).
% 17.33/5.10 thf(413,plain,((! [A:int,B:int,C:int,D:int]: (((minus_minus_int @ A @ B) = (minus_minus_int @ C @ D)) => ((A = B) = (C = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 17.33/5.10 thf(64,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/sandbox/benchmark/theBenchmark.p',fact_198_of__int__le__iff)).
% 17.33/5.10 thf(584,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)],[64])).
% 17.33/5.10 thf(224,axiom,((real_V400292255l_num1 = (^ [A:finite1183840848l_num1]: (real_V646646907m_real @ (finite1106245191l_num1 @ A @ one_one_Numeral_num1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_242_norm__vector__1)).
% 17.33/5.10 thf(1154,plain,(((real_V400292255l_num1) = (^ [A:finite1183840848l_num1]: (real_V646646907m_real @ (finite1106245191l_num1 @ A @ one_one_Numeral_num1))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 17.33/5.10 thf(250,axiom,(((abs_abs_int @ one_one_int) = one_one_int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_178_abs__one)).
% 17.33/5.10 thf(1226,plain,(((abs_abs_int @ one_one_int) = one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 17.33/5.10 thf(54,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((real_V488409631l_num1 @ A @ (minus_249161513l_num1 @ A @ B)) = (real_V400292255l_num1 @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_130_dist__diff_I1_J)).
% 17.33/5.10 thf(545,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((real_V488409631l_num1 @ A @ (minus_249161513l_num1 @ A @ B)) = (real_V400292255l_num1 @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 17.33/5.10 thf(12,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: (ord_le1724070576l_num1 @ (minus_249161513l_num1 @ (abs_ab948591917l_num1 @ A) @ (abs_ab948591917l_num1 @ B)) @ (abs_ab948591917l_num1 @ (minus_249161513l_num1 @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_251_abs__triangle__ineq2__sym)).
% 17.33/5.10 thf(391,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: (ord_le1724070576l_num1 @ (minus_249161513l_num1 @ (abs_ab948591917l_num1 @ A) @ (abs_ab948591917l_num1 @ B)) @ (abs_ab948591917l_num1 @ (minus_249161513l_num1 @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 17.33/5.10 thf(155,axiom,((! [A:finite964658038_int_n,B:finite964658038_int_n,C:n]: ((finite566214509_int_n @ (minus_1196255695_int_n @ A @ B) @ C) = (minus_minus_int @ (finite566214509_int_n @ A @ C) @ (finite566214509_int_n @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_vector__minus__component)).
% 17.33/5.10 thf(936,plain,((! [A:finite964658038_int_n,B:finite964658038_int_n,C:n]: ((finite566214509_int_n @ (minus_1196255695_int_n @ A @ B) @ C) = (minus_minus_int @ (finite566214509_int_n @ A @ C) @ (finite566214509_int_n @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 17.33/5.10 thf(8,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: (ord_le1724070576l_num1 @ (minus_249161513l_num1 @ (abs_ab948591917l_num1 @ A) @ (abs_ab948591917l_num1 @ B)) @ (abs_ab948591917l_num1 @ (minus_249161513l_num1 @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_259_abs__triangle__ineq2)).
% 17.33/5.10 thf(382,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: (ord_le1724070576l_num1 @ (minus_249161513l_num1 @ (abs_ab948591917l_num1 @ A) @ (abs_ab948591917l_num1 @ B)) @ (abs_ab948591917l_num1 @ (minus_249161513l_num1 @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 17.33/5.10 thf(267,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: (ord_le866583254real_n @ (minus_1037315151real_n @ (abs_ab1599551059real_n @ A) @ (abs_ab1599551059real_n @ B)) @ (abs_ab1599551059real_n @ (minus_1037315151real_n @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_258_abs__triangle__ineq2)).
% 17.33/5.10 thf(1271,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: (ord_le866583254real_n @ (minus_1037315151real_n @ (abs_ab1599551059real_n @ A) @ (abs_ab1599551059real_n @ B)) @ (abs_ab1599551059real_n @ (minus_1037315151real_n @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 17.33/5.10 thf(255,axiom,((! [A:finite1489363574real_n,B:n,C:finite1489363574real_n]: (ord_less_eq_real @ (real_V1934908667t_real @ (finite772340589real_n @ A @ B) @ (finite772340589real_n @ C @ B)) @ (real_V783965509real_n @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_289_dist__vec__nth__le)).
% 17.33/5.10 thf(1239,plain,((! [A:finite1489363574real_n,B:n,C:finite1489363574real_n]: (ord_less_eq_real @ (real_V1934908667t_real @ (finite772340589real_n @ A @ B) @ (finite772340589real_n @ C @ B)) @ (real_V783965509real_n @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 17.33/5.10 thf(203,axiom,(((ring_11737179077real_n @ one_one_int) = one_on1253059131real_n)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_107_of__int__1)).
% 17.33/5.10 thf(1092,plain,(((ring_11737179077real_n @ one_one_int) = one_on1253059131real_n)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 17.33/5.10 thf(120,axiom,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => (ord_less_real @ (minus_minus_real @ A @ C) @ (minus_minus_real @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_175_diff__strict__right__mono)).
% 17.33/5.10 thf(804,plain,((! [A:real,B:real,C:real]: ((ord_less_real @ A @ B) => (ord_less_real @ (minus_minus_real @ A @ C) @ (minus_minus_real @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 17.33/5.10 thf(96,axiom,((ord_less_real = (^ [A:real,B:real]: ((ord_less_eq_real @ A @ B) & ~ (ord_less_eq_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_300_eucl__less__le__not__le)).
% 17.33/5.10 thf(704,plain,(((ord_less_real) = (^ [A:real,B:real]: ((ord_less_eq_real @ A @ B) & ~ (ord_less_eq_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 17.33/5.10 thf(159,axiom,((! [A:real,B:real]: ((A != B) => ((ord_less_eq_real @ A @ B) => (ord_less_real @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_302_order_Onot__eq__order__implies__strict)).
% 17.33/5.10 thf(947,plain,((! [A:real,B:real]: ((~ (A = B)) => ((ord_less_eq_real @ A @ B) => (ord_less_real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 17.33/5.10 thf(249,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (real_V488409631l_num1 @ A @ B) @ (real_V488409631l_num1 @ B @ C))) @ (real_V488409631l_num1 @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_285_abs__dist__diff__le)).
% 17.33/5.10 thf(1224,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (real_V488409631l_num1 @ A @ B) @ (real_V488409631l_num1 @ B @ C))) @ (real_V488409631l_num1 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 17.33/5.10 thf(52,axiom,((! [A:int]: (ord_less_eq_int @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_296_order__refl)).
% 17.33/5.10 thf(540,plain,((! [A:int]: (ord_less_eq_int @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 17.33/5.10 thf(87,axiom,((! [A:int]: ((ord_less_int @ (ring_1_of_int_int @ A) @ one_one_int) = (ord_less_int @ A @ one_one_int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_123_of__int__less__1__iff)).
% 17.33/5.10 thf(681,plain,((! [A:int]: ((ord_less_int @ (ring_1_of_int_int @ A) @ one_one_int) = (ord_less_int @ A @ one_one_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 17.33/5.10 thf(272,axiom,((! [A:int]: ((abs_abs_int @ (abs_abs_int @ A)) = (abs_abs_int @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_26_abs__idempotent)).
% 17.33/5.10 thf(1282,plain,((! [A:int]: ((abs_abs_int @ (abs_abs_int @ A)) = (abs_abs_int @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[272])).
% 17.33/5.10 thf(175,axiom,((((=) @ int) = (^ [A:int,B:int]: ((ord_less_eq_int @ B @ A) & (ord_less_eq_int @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_310_dual__order_Oeq__iff)).
% 17.33/5.10 thf(996,plain,((((=) @ int) = (^ [A:int,B:int]: ((ord_less_eq_int @ B @ A) & (ord_less_eq_int @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 17.33/5.10 thf(31,axiom,((! [A:int,B:int,C:int]: ((ord_less_eq_int @ A @ B) => ((B = C) => (ord_less_eq_int @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_322_ord__le__eq__trans)).
% 17.33/5.10 thf(451,plain,((! [A:int,B:int,C:int]: ((ord_less_eq_int @ A @ B) => ((B = C) => (ord_less_eq_int @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 17.33/5.10 thf(220,axiom,((real_V488409631l_num1 = (^ [A:finite1183840848l_num1,B:finite1183840848l_num1]: (real_V488409631l_num1 @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_150_dist__commute)).
% 17.33/5.10 thf(1144,plain,(((real_V488409631l_num1) = (^ [A:finite1183840848l_num1,B:finite1183840848l_num1]: (real_V488409631l_num1 @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 17.33/5.10 thf(139,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) = (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_329_antisym__conv)).
% 17.33/5.10 thf(880,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) = (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 17.33/5.10 thf(71,axiom,((! [A:real,B:real,C:real,D:real]: (((minus_minus_real @ A @ B) = (minus_minus_real @ C @ D)) => ((A = B) = (C = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_63_diff__eq__diff__eq)).
% 17.33/5.10 thf(616,plain,((! [A:real,B:real,C:real,D:real]: (((minus_minus_real @ A @ B) = (minus_minus_real @ C @ D)) => ((A = B) = (C = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 17.33/5.10 thf(307,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/sandbox/benchmark/theBenchmark.p',fact_220_ceiling__le__iff)).
% 17.33/5.10 thf(1376,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)],[307])).
% 17.33/5.10 thf(281,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/sandbox/benchmark/theBenchmark.p',fact_199_of__int__le__iff)).
% 17.33/5.10 thf(1307,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)],[281])).
% 17.33/5.10 thf(230,axiom,((real_V646646907m_real = abs_abs_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_156_real__norm__def)).
% 17.33/5.10 thf(1175,plain,(((real_V646646907m_real) = (abs_abs_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 17.33/5.10 thf(170,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/sandbox/benchmark/theBenchmark.p',fact_203_of__int__1__le__iff)).
% 17.33/5.10 thf(979,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)],[170])).
% 17.33/5.10 thf(67,axiom,((! [A:int]: (((ring_1_of_int_int @ A) = one_one_int) = (A = one_one_int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_103_of__int__eq__1__iff)).
% 17.33/5.10 thf(604,plain,((! [A:int]: (((ring_1_of_int_int @ A) = one_one_int) = (A = one_one_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 17.33/5.10 thf(179,axiom,((! [A:real]: ((ord_less_eq_int @ (archim1371465213g_real @ A) @ one_one_int) = (ord_less_eq_real @ A @ one_one_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_206_ceiling__le__one)).
% 17.33/5.10 thf(1011,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)],[179])).
% 17.33/5.10 thf(22,axiom,((((=) @ finite1183840848l_num1) = (^ [A:finite1183840848l_num1,B:finite1183840848l_num1]: ! [C:numeral_num1]: ((finite1106245191l_num1 @ A @ C) = (finite1106245191l_num1 @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_37_vec__eq__iff)).
% 17.33/5.10 thf(419,plain,((((=) @ finite1183840848l_num1) = (^ [A:finite1183840848l_num1,B:finite1183840848l_num1]: ! [C:numeral_num1]: ((finite1106245191l_num1 @ A @ C) = (finite1106245191l_num1 @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 17.33/5.10 thf(39,axiom,((! [A:int]: ((member_int @ A @ ring_1_Ints_int) => (~ (! [B:int]: (A != (ring_1_of_int_int @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_Ints__cases)).
% 17.33/5.10 thf(477,plain,((! [A:int]: ((member_int @ A @ ring_1_Ints_int) => (~ (! [B:int]: ~ (A = (ring_1_of_int_int @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 17.33/5.10 thf(10,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_3_1_If_001t__Finite____Cartesian____Product__Ovec_It__Real__Oreal_Mt__Numeral____Type__Onum1_J_T)).
% 17.33/5.10 thf(387,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 17.33/5.10 thf(339,axiom,((! [A:real]: (ord_less_eq_real @ (ring_1_of_int_real @ (archim1031974863r_real @ A)) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_271_of__int__floor__le)).
% 17.33/5.10 thf(1471,plain,((! [A:real]: (ord_less_eq_real @ (ring_1_of_int_real @ (archim1031974863r_real @ A)) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[339])).
% 17.33/5.10 thf(201,axiom,((! [A:real,B:(int > real),C:int,D:int]: ((A = (B @ C)) => ((ord_less_eq_int @ C @ D) => ((! [E:int,F:int]: ((ord_less_eq_int @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_eq_real @ A @ (B @ D))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_349_ord__eq__le__subst)).
% 17.33/5.10 thf(1080,plain,((! [A:real,B:(int > real),C:int,D:int]: ((A = (B @ C)) => ((ord_less_eq_int @ C @ D) => ((! [E:int,F:int]: ((ord_less_eq_int @ E @ F) => (ord_less_eq_real @ (B @ E) @ (B @ F)))) => (ord_less_eq_real @ A @ (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 17.33/5.10 thf(77,axiom,((! [A:int,B:int,C:(int > $o)]: ((ord_less_eq_int @ A @ B) => ((C @ B) => ((! [D:int]: ((ord_less_eq_int @ D @ B) => ((C @ D) => (C @ (minus_minus_int @ D @ one_one_int))))) => (C @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_217_int__le__induct)).
% 17.33/5.10 thf(631,plain,((! [A:int,B:int,C:(int > $o)]: ((ord_less_eq_int @ A @ B) => ((C @ B) => ((! [D:int]: ((ord_less_eq_int @ D @ B) => ((C @ D) => (C @ (minus_minus_int @ D @ one_one_int))))) => (C @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 17.33/5.10 thf(104,axiom,((! [A:finite2063899472l_num1,B:finite2063899472l_num1]: (((finite1800583751l_num1 @ A) = (finite1800583751l_num1 @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_68_vec__nth__inject)).
% 17.33/5.10 thf(758,plain,((! [A:finite2063899472l_num1,B:finite2063899472l_num1]: (((finite1800583751l_num1 @ A) = (finite1800583751l_num1 @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 17.33/5.10 thf(130,axiom,((((=) @ real) = (^ [A:real,B:real]: ((ord_less_eq_real @ A @ B) & (ord_less_eq_real @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_327_order__class_Oorder_Oeq__iff)).
% 17.33/5.10 thf(848,plain,((((=) @ real) = (^ [A:real,B:real]: ((ord_less_eq_real @ A @ B) & (ord_less_eq_real @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 17.33/5.10 thf(288,axiom,((! [A:int,B:real]: ((ord_less_real @ (minus_minus_real @ (ring_1_of_int_real @ A) @ one_one_real) @ B) => ((ord_less_eq_real @ B @ (ring_1_of_int_real @ A)) => ((archim1371465213g_real @ B) = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_295_ceiling__unique)).
% 17.33/5.10 thf(1325,plain,((! [A:int,B:real]: ((ord_less_real @ (minus_minus_real @ (ring_1_of_int_real @ A) @ one_one_real) @ B) => ((ord_less_eq_real @ B @ (ring_1_of_int_real @ A)) => ((archim1371465213g_real @ B) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[288])).
% 17.33/5.10 thf(184,axiom,((! [A:finite2063899472l_num1,B:finite2063899472l_num1,C:numeral_num1]: ((finite1800583751l_num1 @ (minus_779068585l_num1 @ A @ B) @ C) = (minus_minus_int @ (finite1800583751l_num1 @ A @ C) @ (finite1800583751l_num1 @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_vector__minus__component)).
% 17.33/5.10 thf(1029,plain,((! [A:finite2063899472l_num1,B:finite2063899472l_num1,C:numeral_num1]: ((finite1800583751l_num1 @ (minus_779068585l_num1 @ A @ B) @ C) = (minus_minus_int @ (finite1800583751l_num1 @ A @ C) @ (finite1800583751l_num1 @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 17.33/5.10 thf(75,axiom,((! [A:real]: (ord_less_eq_real @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_317_dual__order_Orefl)).
% 17.33/5.10 thf(626,plain,((! [A:real]: (ord_less_eq_real @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 17.33/5.10 thf(295,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:n]: ((finite772340589real_n @ (minus_1037315151real_n @ A @ B) @ C) = (minus_minus_real @ (finite772340589real_n @ A @ C) @ (finite772340589real_n @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_6_vector__minus__component)).
% 17.33/5.10 thf(1344,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:n]: ((finite772340589real_n @ (minus_1037315151real_n @ A @ B) @ C) = (minus_minus_real @ (finite772340589real_n @ A @ C) @ (finite772340589real_n @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[295])).
% 17.33/5.10 thf(276,axiom,((! [A:(n > (real > $o))]: ((! [B:n]: ? [C:real]: (A @ B @ C)) = (? [B:finite1489363574real_n]: ! [C:n]: (A @ C @ (finite772340589real_n @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_32_lambda__skolem)).
% 17.33/5.10 thf(1293,plain,((! [A:(n > (real > $o))]: ((! [B:n]: ? [C:real]: (A @ B @ C)) = (? [B:finite1489363574real_n]: ! [C:n]: (A @ C @ (finite772340589real_n @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[276])).
% 17.33/5.10 thf(231,axiom,((! [A:real,B:int]: ((archim1371465213g_real @ (minus_minus_real @ A @ (ring_1_of_int_real @ B))) = (minus_minus_int @ (archim1371465213g_real @ A) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_81_ceiling__diff__of__int)).
% 17.33/5.10 thf(1177,plain,((! [A:real,B:int]: ((archim1371465213g_real @ (minus_minus_real @ A @ (ring_1_of_int_real @ B))) = (minus_minus_int @ (archim1371465213g_real @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 17.33/5.10 thf(222,axiom,((ord_le1202326448l_num1 = (^ [A:finite2063899472l_num1,B:finite2063899472l_num1]: ! [C:numeral_num1]: (ord_less_eq_int @ (finite1800583751l_num1 @ A @ C) @ (finite1800583751l_num1 @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_214_less__eq__vec__def)).
% 17.33/5.10 thf(1149,plain,(((ord_le1202326448l_num1) = (^ [A:finite2063899472l_num1,B:finite2063899472l_num1]: ! [C:numeral_num1]: (ord_less_eq_int @ (finite1800583751l_num1 @ A @ C) @ (finite1800583751l_num1 @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 17.33/5.10 thf(165,axiom,((! [A:int,B:int]: ((A != B) => ((~ (ord_less_int @ A @ B)) => (ord_less_int @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_144_linorder__neqE__linordered__idom)).
% 17.33/5.10 thf(964,plain,((! [A:int,B:int]: ((~ (A = B)) => ((~ (ord_less_int @ A @ B)) => (ord_less_int @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 17.33/5.10 thf(240,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n,D:finite1489363574real_n]: (((minus_1037315151real_n @ A @ B) = (minus_1037315151real_n @ C @ D)) => ((ord_le866583254real_n @ A @ B) = (ord_le866583254real_n @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_221_diff__eq__diff__less__eq)).
% 17.33/5.10 thf(1198,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n,D:finite1489363574real_n]: (((minus_1037315151real_n @ A @ B) = (minus_1037315151real_n @ C @ D)) => ((ord_le866583254real_n @ A @ B) = (ord_le866583254real_n @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 17.33/5.10 thf(15,axiom,((! [A:finite964658038_int_n,B:finite964658038_int_n]: ((if_Fin1767949360_int_n @ ($false) @ A @ B) = B))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_2_1_If_001t__Finite____Cartesian____Product__Ovec_It__Int__Oint_Mtf__n_J_T)).
% 17.33/5.10 thf(399,plain,((! [A:finite964658038_int_n,B:finite964658038_int_n]: ((if_Fin1767949360_int_n @ ($false) @ A @ B) = B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 17.33/5.10 thf(245,axiom,((! [A:real,B:real,C:finite1489363574real_n]: ((finite2053577756real_n @ (minus_minus_real @ A @ B) @ C) = (minus_1037315151real_n @ (finite2053577756real_n @ A @ C) @ (finite2053577756real_n @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_77_vector__sub__rdistrib)).
% 17.33/5.10 thf(1213,plain,((! [A:real,B:real,C:finite1489363574real_n]: ((finite2053577756real_n @ (minus_minus_real @ A @ B) @ C) = (minus_1037315151real_n @ (finite2053577756real_n @ A @ C) @ (finite2053577756real_n @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 17.33/5.10 thf(190,axiom,((! [A:int,B:int,C:int]: ((minus_minus_int @ (minus_minus_int @ A @ B) @ C) = (minus_minus_int @ (minus_minus_int @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_60_diff__right__commute)).
% 17.33/5.10 thf(1044,plain,((! [A:int,B:int,C:int]: ((minus_minus_int @ (minus_minus_int @ A @ B) @ C) = (minus_minus_int @ (minus_minus_int @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 17.33/5.10 thf(140,axiom,((! [A:int,B:int]: ((ord_less_int @ A @ B) => (ord_less_eq_int @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_303_dual__order_Ostrict__implies__order)).
% 17.33/5.10 thf(883,plain,((! [A:int,B:int]: ((ord_less_int @ A @ B) => (ord_less_eq_int @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 17.33/5.10 thf(325,axiom,((! [A:int,B:int]: ((abs_abs_int @ (minus_minus_int @ A @ B)) = (abs_abs_int @ (minus_minus_int @ B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_30_abs__minus__commute)).
% 17.33/5.10 thf(1435,plain,((! [A:int,B:int]: ((abs_abs_int @ (minus_minus_int @ A @ B)) = (abs_abs_int @ (minus_minus_int @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[325])).
% 17.33/5.10 thf(361,axiom,((! [A:int]: ((archim1371465213g_real @ (ring_1_of_int_real @ A)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_113_ceiling__of__int)).
% 17.33/5.10 thf(1528,plain,((! [A:int]: ((archim1371465213g_real @ (ring_1_of_int_real @ A)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[361])).
% 17.33/5.10 thf(135,axiom,((! [A:finite2063899472l_num1,B:numeral_num1]: ((finite1800583751l_num1 @ (minkow2063319845m1_int @ A) @ B) = (ring_1_of_int_int @ (finite1800583751l_num1 @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_17_of__int__vec__nth)).
% 17.33/5.10 thf(868,plain,((! [A:finite2063899472l_num1,B:numeral_num1]: ((finite1800583751l_num1 @ (minkow2063319845m1_int @ A) @ B) = (ring_1_of_int_int @ (finite1800583751l_num1 @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 17.33/5.10 thf(318,axiom,((! [A:real,B:finite1489363574real_n,C:finite1489363574real_n]: ((finite2053577756real_n @ A @ (minus_1037315151real_n @ B @ C)) = (minus_1037315151real_n @ (finite2053577756real_n @ A @ B) @ (finite2053577756real_n @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_118_vector__ssub__ldistrib)).
% 17.33/5.10 thf(1413,plain,((! [A:real,B:finite1489363574real_n,C:finite1489363574real_n]: ((finite2053577756real_n @ A @ (minus_1037315151real_n @ B @ C)) = (minus_1037315151real_n @ (finite2053577756real_n @ A @ B) @ (finite2053577756real_n @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[318])).
% 17.33/5.10 thf(25,axiom,((! [A:int,B:int]: ((ord_less_eq_int @ A @ (minus_minus_int @ B @ one_one_int)) = (ord_less_int @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_200_zle__diff1__eq)).
% 17.33/5.10 thf(426,plain,((! [A:int,B:int]: ((ord_less_eq_int @ A @ (minus_minus_int @ B @ one_one_int)) = (ord_less_int @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 17.33/5.10 thf(158,axiom,((! [A:real,B:real]: ((member_real @ A @ ring_1_Ints_real) => ((member_real @ B @ ring_1_Ints_real) => (member_real @ (minus_minus_real @ A @ B) @ ring_1_Ints_real))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_44_Ints__diff)).
% 17.33/5.10 thf(944,plain,((! [A:real,B:real]: ((member_real @ A @ ring_1_Ints_real) => ((member_real @ B @ ring_1_Ints_real) => (member_real @ (minus_minus_real @ A @ B) @ ring_1_Ints_real))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 17.33/5.10 thf(338,axiom,((! [A:real,B:real]: ((member_real @ A @ ring_1_Ints_real) => ((member_real @ B @ ring_1_Ints_real) => ((A = B) = (ord_less_real @ (abs_abs_real @ (minus_minus_real @ A @ B)) @ one_one_real)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_185_Ints__eq__abs__less1)).
% 17.33/5.10 thf(1467,plain,((! [A:real,B:real]: ((member_real @ A @ ring_1_Ints_real) => ((member_real @ B @ ring_1_Ints_real) => ((A = B) = (ord_less_real @ (abs_abs_real @ (minus_minus_real @ A @ B)) @ one_one_real)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[338])).
% 17.33/5.10 thf(55,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((! [C:numeral_num1]: (ord_less_eq_real @ (real_V646646907m_real @ (finite1106245191l_num1 @ A @ C)) @ (real_V646646907m_real @ (finite1106245191l_num1 @ B @ C)))) => (ord_less_eq_real @ (real_V400292255l_num1 @ A) @ (real_V400292255l_num1 @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_267_norm__le__componentwise__cart)).
% 17.33/5.10 thf(548,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((! [C:numeral_num1]: (ord_less_eq_real @ (real_V646646907m_real @ (finite1106245191l_num1 @ A @ C)) @ (real_V646646907m_real @ (finite1106245191l_num1 @ B @ C)))) => (ord_less_eq_real @ (real_V400292255l_num1 @ A) @ (real_V400292255l_num1 @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 17.33/5.10 thf(42,axiom,((! [A:int,B:int,C:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ C @ A) => (ord_less_eq_int @ C @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_312_dual__order_Otrans)).
% 17.33/5.10 thf(487,plain,((! [A:int,B:int,C:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ C @ A) => (ord_less_eq_int @ C @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 17.33/5.10 thf(156,axiom,((! [A:int,B:int]: (((ring_11737179077real_n @ A) = (ring_11737179077real_n @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_of__int__eq__iff)).
% 17.33/5.10 thf(939,plain,((! [A:int,B:int]: (((ring_11737179077real_n @ A) = (ring_11737179077real_n @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 17.33/5.10 thf(57,axiom,((! [A:int,B:int,C:int]: (((ord_less_eq_int @ A @ B) => (~ (ord_less_eq_int @ B @ C))) => (((ord_less_eq_int @ B @ A) => (~ (ord_less_eq_int @ A @ C))) => (((ord_less_eq_int @ A @ C) => (~ (ord_less_eq_int @ C @ B))) => (((ord_less_eq_int @ C @ B) => (~ (ord_less_eq_int @ B @ A))) => (((ord_less_eq_int @ B @ C) => (~ (ord_less_eq_int @ C @ A))) => (~ ((ord_less_eq_int @ C @ A) => (~ (ord_less_eq_int @ A @ B))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_330_le__cases3)).
% 17.33/5.10 thf(553,plain,((! [A:int,B:int,C:int]: (((ord_less_eq_int @ A @ B) => (~ (ord_less_eq_int @ B @ C))) => (((ord_less_eq_int @ B @ A) => (~ (ord_less_eq_int @ A @ C))) => (((ord_less_eq_int @ A @ C) => (~ (ord_less_eq_int @ C @ B))) => (((ord_less_eq_int @ C @ B) => (~ (ord_less_eq_int @ B @ A))) => (((ord_less_eq_int @ B @ C) => (~ (ord_less_eq_int @ C @ A))) => (~ ((ord_less_eq_int @ C @ A) => (~ (ord_less_eq_int @ A @ B))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 17.33/5.10 thf(127,axiom,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) | (ord_less_eq_int @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_338_linear)).
% 17.33/5.10 thf(836,plain,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) | (ord_less_eq_int @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 17.33/5.10 thf(192,axiom,((! [A:(n > (int > $o))]: ((! [B:n]: ? [C:int]: (A @ B @ C)) = (? [B:finite964658038_int_n]: ! [C:n]: (A @ C @ (finite566214509_int_n @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_35_lambda__skolem)).
% 17.33/5.10 thf(1049,plain,((! [A:(n > (int > $o))]: ((! [B:n]: ? [C:int]: (A @ B @ C)) = (? [B:finite964658038_int_n]: ! [C:n]: (A @ C @ (finite566214509_int_n @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[192])).
% 17.33/5.10 thf(43,axiom,((! [A:real,B:real,C:real,D:real]: ((ord_less_real @ A @ B) => ((ord_less_real @ C @ D) => (ord_less_real @ (minus_minus_real @ A @ D) @ (minus_minus_real @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_163_diff__strict__mono)).
% 17.33/5.10 thf(490,plain,((! [A:real,B:real,C:real,D:real]: ((ord_less_real @ A @ B) => ((ord_less_real @ C @ D) => (ord_less_real @ (minus_minus_real @ A @ D) @ (minus_minus_real @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 17.33/5.10 thf(85,axiom,((! [A:real]: ((ord_less_eq_int @ one_one_int @ (archim1031974863r_real @ A)) = (ord_less_eq_real @ one_one_real @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_205_one__le__floor)).
% 17.33/5.10 thf(675,plain,((! [A:real]: ((ord_less_eq_int @ one_one_int @ (archim1031974863r_real @ A)) = (ord_less_eq_real @ one_one_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 17.33/5.10 thf(356,axiom,((! [A:finite1489363574real_n,B:n]: (ord_less_eq_real @ (real_V646646907m_real @ (finite772340589real_n @ A @ B)) @ (real_V739724485real_n @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_268_Finite__Cartesian__Product_Onorm__nth__le)).
% 17.33/5.10 thf(1516,plain,((! [A:finite1489363574real_n,B:n]: (ord_less_eq_real @ (real_V646646907m_real @ (finite772340589real_n @ A @ B)) @ (real_V739724485real_n @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[356])).
% 17.33/5.10 thf(197,axiom,((! [A:finite1489363574real_n,B:(finite1489363574real_n > $o)]: ((member1352538125real_n @ A @ (collec321817931real_n @ B)) = (B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_92_mem__Collect__eq)).
% 17.33/5.10 thf(1070,plain,((! [A:finite1489363574real_n,B:(finite1489363574real_n > $o)]: ((member1352538125real_n @ A @ (collec321817931real_n @ (B))) = (B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 17.33/5.10 thf(225,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_int @ (archim1371465213g_real @ A) @ (archim1371465213g_real @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_207_ceiling__mono)).
% 17.33/5.10 thf(1156,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)],[225])).
% 17.33/5.10 thf(313,axiom,((! [A:(int > $o),B:real]: ((A @ (archim1371465213g_real @ B)) = (! [C:int]: (((ord_less_real @ (minus_minus_real @ (ring_1_of_int_real @ C) @ one_one_real) @ B) & (ord_less_eq_real @ B @ (ring_1_of_int_real @ C))) => (A @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_196_ceiling__split)).
% 17.33/5.10 thf(1400,plain,((! [A:(int > $o),B:real]: ((A @ (archim1371465213g_real @ B)) = (! [C:int]: (((ord_less_real @ (minus_minus_real @ (ring_1_of_int_real @ C) @ one_one_real) @ B) & (ord_less_eq_real @ B @ (ring_1_of_int_real @ C))) => (A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[313])).
% 17.33/5.10 thf(167,axiom,((! [A:finite2063899472l_num1]: ((finite1470207077l_num1 @ (finite1800583751l_num1 @ A @ one_one_Numeral_num1)) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_306_vector__one__nth)).
% 17.33/5.10 thf(971,plain,((! [A:finite2063899472l_num1]: ((finite1470207077l_num1 @ (finite1800583751l_num1 @ A @ one_one_Numeral_num1)) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 17.33/5.10 thf(260,axiom,((! [A:real,B:(real > $o)]: ((member_real @ A @ ring_1_Ints_real) => ((! [C:int]: (B @ (ring_1_of_int_real @ C))) => (B @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_52_Ints__induct)).
% 17.33/5.10 thf(1252,plain,((! [A:real,B:(real > $o)]: ((member_real @ A @ ring_1_Ints_real) => ((! [C:int]: (B @ (ring_1_of_int_real @ C))) => (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 17.33/5.10 thf(304,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((! [C:n]: (ord_less_eq_real @ (real_V646646907m_real @ (finite772340589real_n @ A @ C)) @ (real_V646646907m_real @ (finite772340589real_n @ B @ C)))) => (ord_less_eq_real @ (real_V739724485real_n @ A) @ (real_V739724485real_n @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_265_norm__le__componentwise__cart)).
% 17.33/5.10 thf(1368,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((! [C:n]: (ord_less_eq_real @ (real_V646646907m_real @ (finite772340589real_n @ A @ C)) @ (real_V646646907m_real @ (finite772340589real_n @ B @ C)))) => (ord_less_eq_real @ (real_V739724485real_n @ A) @ (real_V739724485real_n @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[304])).
% 17.33/5.10 thf(265,axiom,((! [A:real]: (((ring_1_of_int_real @ (archim1371465213g_real @ A)) = A) = (? [B:int]: (A = (ring_1_of_int_real @ B)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_187_of__int__ceiling__cancel)).
% 17.33/5.10 thf(1267,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)],[265])).
% 17.33/5.10 thf(362,axiom,((member_real @ (minus_minus_real @ (finite772340589real_n @ x @ i) @ (finite772340589real_n @ y @ i)) @ ring_1_Ints_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_14__092_060open_062x_A_E_Ai_A_N_Ay_A_E_Ai_A_092_060in_062_A_092_060int_062_092_060close_062)).
% 17.33/5.10 thf(1531,plain,((member_real @ (minus_minus_real @ (finite772340589real_n @ x @ i) @ (finite772340589real_n @ y @ i)) @ ring_1_Ints_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[362])).
% 17.33/5.10 thf(344,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (real_V783965509real_n @ A @ B) @ (real_V783965509real_n @ B @ C))) @ (real_V783965509real_n @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_283_abs__dist__diff__le)).
% 17.33/5.10 thf(1484,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (real_V783965509real_n @ A @ B) @ (real_V783965509real_n @ B @ C))) @ (real_V783965509real_n @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[344])).
% 17.33/5.10 thf(350,axiom,((! [A:int,B:int]: (((ring_1_of_int_real @ A) = (ring_1_of_int_real @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_of__int__eq__iff)).
% 17.33/5.10 thf(1499,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)],[350])).
% 17.33/5.10 thf(84,axiom,((ord_le1724070576l_num1 = (^ [A:finite1183840848l_num1,B:finite1183840848l_num1]: ! [C:numeral_num1]: (ord_less_eq_real @ (finite1106245191l_num1 @ A @ C) @ (finite1106245191l_num1 @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_213_less__eq__vec__def)).
% 17.33/5.10 thf(673,plain,(((ord_le1724070576l_num1) = (^ [A:finite1183840848l_num1,B:finite1183840848l_num1]: ! [C:numeral_num1]: (ord_less_eq_real @ (finite1106245191l_num1 @ A @ C) @ (finite1106245191l_num1 @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 17.33/5.10 thf(115,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) => (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_309_dual__order_Oantisym)).
% 17.33/5.10 thf(791,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) => (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 17.33/5.10 thf(48,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:real]: ((ord_less_real @ (real_V783965509real_n @ A @ B) @ C) => (ord_less_real @ (real_V783965509real_n @ B @ A) @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_145_dist__commute__lessI)).
% 17.33/5.10 thf(502,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:real]: ((ord_less_real @ (real_V783965509real_n @ A @ B) @ C) => (ord_less_real @ (real_V783965509real_n @ B @ A) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 17.33/5.10 thf(263,axiom,(((abs_abs_int @ one_one_int) = one_one_int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_91_abs__1)).
% 17.33/5.10 thf(1262,plain,(((abs_abs_int @ one_one_int) = one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 17.33/5.10 thf(34,axiom,((! [A:real,B:real]: ((ord_less_int @ (archim1031974863r_real @ A) @ (archim1031974863r_real @ B)) => (ord_less_real @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_152_floor__less__cancel)).
% 17.33/5.10 thf(463,plain,((! [A:real,B:real]: ((ord_less_int @ (archim1031974863r_real @ A) @ (archim1031974863r_real @ B)) => (ord_less_real @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 17.33/5.10 thf(217,axiom,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (ord_less_eq_real @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_304_dual__order_Ostrict__implies__order)).
% 17.33/5.10 thf(1130,plain,((! [A:real,B:real]: ((ord_less_real @ A @ B) => (ord_less_eq_real @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 17.33/5.10 thf(273,axiom,((! [A:int,B:int]: (ord_less_eq_int @ (abs_abs_int @ (minus_minus_int @ (abs_abs_int @ A) @ (abs_abs_int @ B))) @ (abs_abs_int @ (minus_minus_int @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_256_abs__triangle__ineq3)).
% 17.33/5.10 thf(1285,plain,((! [A:int,B:int]: (ord_less_eq_int @ (abs_abs_int @ (minus_minus_int @ (abs_abs_int @ A) @ (abs_abs_int @ B))) @ (abs_abs_int @ (minus_minus_int @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[273])).
% 17.33/5.10 thf(292,axiom,((! [A:finite1489363574real_n,B:finite337957458num1_n]: ((! [C:n]: (ord_less_eq_real @ (real_V646646907m_real @ (finite772340589real_n @ A @ C)) @ (real_V400292255l_num1 @ (finite1639785033num1_n @ B @ C)))) => (ord_less_eq_real @ (real_V739724485real_n @ A) @ (real_V1121707553num1_n @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_264_norm__le__componentwise__cart)).
% 17.33/5.10 thf(1336,plain,((! [A:finite1489363574real_n,B:finite337957458num1_n]: ((! [C:n]: (ord_less_eq_real @ (real_V646646907m_real @ (finite772340589real_n @ A @ C)) @ (real_V400292255l_num1 @ (finite1639785033num1_n @ B @ C)))) => (ord_less_eq_real @ (real_V739724485real_n @ A) @ (real_V1121707553num1_n @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[292])).
% 17.33/5.10 thf(148,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((minus_249161513l_num1 @ (minus_249161513l_num1 @ A @ B) @ C) = (minus_249161513l_num1 @ (minus_249161513l_num1 @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_61_diff__right__commute)).
% 17.33/5.10 thf(907,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:finite1183840848l_num1]: ((minus_249161513l_num1 @ (minus_249161513l_num1 @ A @ B) @ C) = (minus_249161513l_num1 @ (minus_249161513l_num1 @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 17.33/5.10 thf(187,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) | (ord_less_eq_real @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_339_linear)).
% 17.33/5.10 thf(1038,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) | (ord_less_eq_real @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 17.33/5.10 thf(4,axiom,((! [A:finite964658038_int_n,B:finite964658038_int_n]: ((if_Fin1767949360_int_n @ ($true) @ A @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_1_1_If_001t__Finite____Cartesian____Product__Ovec_It__Int__Oint_Mtf__n_J_T)).
% 17.33/5.10 thf(370,plain,((! [A:finite964658038_int_n,B:finite964658038_int_n]: ((if_Fin1767949360_int_n @ ($true) @ A @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 17.33/5.10 thf(37,axiom,((! [A:real,B:set_real,C:real]: ((member_real @ A @ B) => ((member_real @ C @ B) => ((A = C) = (! [D:real]: ((member_real @ D @ B) => ((real_V1934908667t_real @ A @ D) = (real_V1934908667t_real @ C @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_287_metric__eq__thm)).
% 17.33/5.10 thf(470,plain,((! [A:real,B:set_real,C:real]: ((member_real @ A @ B) => ((member_real @ C @ B) => ((A = C) = (! [D:real]: ((member_real @ D @ B) => ((real_V1934908667t_real @ A @ D) = (real_V1934908667t_real @ C @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 17.33/5.10 thf(61,axiom,((! [A:finite2063899472l_num1,B:numeral_num1]: ((finite1503577981l_num1 @ (minkow781993583real_n @ A) @ B) = (ring_11737179077real_n @ (finite1800583751l_num1 @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_15_of__int__vec__nth)).
% 17.33/5.10 thf(576,plain,((! [A:finite2063899472l_num1,B:numeral_num1]: ((finite1503577981l_num1 @ (minkow781993583real_n @ A) @ B) = (ring_11737179077real_n @ (finite1800583751l_num1 @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 17.33/5.10 thf(300,axiom,((! [A:int,B:int]: (ord_less_eq_int @ (minus_minus_int @ (abs_abs_int @ A) @ (abs_abs_int @ B)) @ (abs_abs_int @ (minus_minus_int @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_260_abs__triangle__ineq2)).
% 17.33/5.10 thf(1358,plain,((! [A:int,B:int]: (ord_less_eq_int @ (minus_minus_int @ (abs_abs_int @ A) @ (abs_abs_int @ B)) @ (abs_abs_int @ (minus_minus_int @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[300])).
% 17.33/5.10 thf(261,axiom,((! [A:real]: (ord_less_eq_real @ A @ (abs_abs_real @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_238_abs__ge__self)).
% 17.33/5.10 thf(1257,plain,((! [A:real]: (ord_less_eq_real @ A @ (abs_abs_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 17.33/5.10 thf(219,axiom,((! [A:finite2063899472l_num1,B:finite2063899472l_num1]: (((minkow19073400691_real @ A) = (minkow19073400691_real @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_of__int__vec__eq__iff)).
% 17.33/5.10 thf(1141,plain,((! [A:finite2063899472l_num1,B:finite2063899472l_num1]: (((minkow19073400691_real @ A) = (minkow19073400691_real @ B)) = (A = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 17.33/5.10 thf(70,axiom,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ B @ A) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_340_antisym)).
% 17.33/5.10 thf(613,plain,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 17.33/5.10 thf(248,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n]: ((minus_1037315151real_n @ (minus_1037315151real_n @ A @ B) @ C) = (minus_1037315151real_n @ (minus_1037315151real_n @ A @ C) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_58_diff__right__commute)).
% 17.33/5.10 thf(1221,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n]: ((minus_1037315151real_n @ (minus_1037315151real_n @ A @ B) @ C) = (minus_1037315151real_n @ (minus_1037315151real_n @ A @ C) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 17.33/5.10 thf(298,axiom,((real_V1934908667t_real = (^ [A:real,B:real]: (abs_abs_real @ (minus_minus_real @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_179_dist__real__def)).
% 17.33/5.10 thf(1353,plain,(((real_V1934908667t_real) = (^ [A:real,B:real]: (abs_abs_real @ (minus_minus_real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[298])).
% 17.33/5.10 thf(193,axiom,((real_V488409631l_num1 = (^ [A:finite1183840848l_num1,B:finite1183840848l_num1]: (real_V1934908667t_real @ (finite1106245191l_num1 @ A @ one_one_Numeral_num1) @ (finite1106245191l_num1 @ B @ one_one_Numeral_num1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_246_dist__vector__1)).
% 17.33/5.10 thf(1052,plain,(((real_V488409631l_num1) = (^ [A:finite1183840848l_num1,B:finite1183840848l_num1]: (real_V1934908667t_real @ (finite1106245191l_num1 @ A @ one_one_Numeral_num1) @ (finite1106245191l_num1 @ B @ one_one_Numeral_num1))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 17.33/5.10 thf(322,axiom,((! [A:real,B:int]: ((ord_less_int @ (archim1031974863r_real @ A) @ B) = (ord_less_real @ A @ (ring_1_of_int_real @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_138_floor__less__iff)).
% 17.33/5.11 thf(1427,plain,((! [A:real,B:int]: ((ord_less_int @ (archim1031974863r_real @ A) @ B) = (ord_less_real @ A @ (ring_1_of_int_real @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[322])).
% 17.33/5.11 thf(204,axiom,((! [A:int,B:n]: ((finite566214509_int_n @ (finite55766923_int_n @ A) @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_117_vec__component)).
% 17.33/5.11 thf(1094,plain,((! [A:int,B:n]: ((finite566214509_int_n @ (finite55766923_int_n @ A) @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 17.33/5.11 thf(178,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_321_order__class_Oorder_Oantisym)).
% 17.33/5.11 thf(1008,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 17.33/5.11 thf(46,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((if_Fin127821360real_n @ ($true) @ A @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_1_1_If_001t__Finite____Cartesian____Product__Ovec_It__Real__Oreal_Mtf__n_J_T)).
% 17.33/5.11 thf(497,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((if_Fin127821360real_n @ ($true) @ A @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 17.33/5.11 thf(174,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((B = C) => (ord_less_eq_real @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_323_ord__le__eq__trans)).
% 17.33/5.11 thf(991,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => ((B = C) => (ord_less_eq_real @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 17.33/5.11 thf(284,axiom,((real_V783965509real_n = (^ [A:finite1489363574real_n,B:finite1489363574real_n]: (real_V739724485real_n @ (minus_1037315151real_n @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_140_dist__norm)).
% 17.33/5.11 thf(1316,plain,(((real_V783965509real_n) = (^ [A:finite1489363574real_n,B:finite1489363574real_n]: (real_V739724485real_n @ (minus_1037315151real_n @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[284])).
% 17.33/5.11 thf(334,axiom,((! [A:finite337957458num1_n,B:finite1489363574real_n]: ((! [C:n]: (ord_less_eq_real @ (real_V400292255l_num1 @ (finite1639785033num1_n @ A @ C)) @ (real_V646646907m_real @ (finite772340589real_n @ B @ C)))) => (ord_less_eq_real @ (real_V1121707553num1_n @ A) @ (real_V739724485real_n @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_262_norm__le__componentwise__cart)).
% 17.33/5.11 thf(1459,plain,((! [A:finite337957458num1_n,B:finite1489363574real_n]: ((! [C:n]: (ord_less_eq_real @ (real_V400292255l_num1 @ (finite1639785033num1_n @ A @ C)) @ (real_V646646907m_real @ (finite772340589real_n @ B @ C)))) => (ord_less_eq_real @ (real_V1121707553num1_n @ A) @ (real_V739724485real_n @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[334])).
% 17.33/5.11 thf(232,axiom,((! [A:real,B:real]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (abs_abs_real @ A) @ (abs_abs_real @ B))) @ (abs_abs_real @ (minus_minus_real @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_257_abs__triangle__ineq3)).
% 17.33/5.11 thf(1180,plain,((! [A:real,B:real]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (abs_abs_real @ A) @ (abs_abs_real @ B))) @ (abs_abs_real @ (minus_minus_real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 17.33/5.11 thf(286,axiom,((! [A:real]: ? [B:int]: (ord_less_eq_real @ A @ (ring_1_of_int_real @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_243_ex__le__of__int)).
% 17.33/5.11 thf(1321,plain,((! [A:real]: ? [B:int]: (ord_less_eq_real @ A @ (ring_1_of_int_real @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[286])).
% 17.33/5.11 thf(45,axiom,(((archim1031974863r_real @ one_one_real) = one_one_int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_110_floor__one)).
% 17.33/5.11 thf(495,plain,(((archim1031974863r_real @ one_one_real) = one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 17.33/5.11 thf(236,axiom,(((ring_1_of_int_real @ m) = (minus_minus_real @ (finite772340589real_n @ x @ i) @ (finite772340589real_n @ y @ i)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_m)).
% 17.33/5.11 thf(1189,plain,(((ring_1_of_int_real @ m) = (minus_minus_real @ (finite772340589real_n @ x @ i) @ (finite772340589real_n @ y @ i)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 17.33/5.11 thf(208,axiom,((! [A:int]: ((one_one_int = A) = (A = one_one_int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_136_one__reorient)).
% 17.33/5.11 thf(1108,plain,((! [A:int]: ((one_one_int = A) = (A = one_one_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 17.33/5.11 thf(321,axiom,((! [A:real]: ((ord_less_real @ (minus_minus_real @ (ring_1_of_int_real @ (archim1371465213g_real @ A)) @ one_one_real) @ A) & (ord_less_eq_real @ A @ (ring_1_of_int_real @ (archim1371465213g_real @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_294_ceiling__correct)).
% 17.33/5.11 thf(1421,plain,((! [A:real]: ((ord_less_real @ (minus_minus_real @ (ring_1_of_int_real @ (archim1371465213g_real @ A)) @ one_one_real) @ A) & (ord_less_eq_real @ A @ (ring_1_of_int_real @ (archim1371465213g_real @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[321])).
% 17.33/5.11 thf(35,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:real]: ((ord_less_real @ (real_V488409631l_num1 @ A @ B) @ C) => (ord_less_real @ (real_V488409631l_num1 @ B @ A) @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_147_dist__commute__lessI)).
% 17.33/5.11 thf(465,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:real]: ((ord_less_real @ (real_V488409631l_num1 @ A @ B) @ C) => (ord_less_real @ (real_V488409631l_num1 @ B @ A) @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 17.33/5.11 thf(169,axiom,((! [A:real,B:real]: ((real_V1934908667t_real @ (minus_minus_real @ A @ B) @ A) = (real_V646646907m_real @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_126_dist__diff_I2_J)).
% 17.33/5.11 thf(976,plain,((! [A:real,B:real]: ((real_V1934908667t_real @ (minus_minus_real @ A @ B) @ A) = (real_V646646907m_real @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 17.33/5.11 thf(146,axiom,((! [A:real]: (ord_less_eq_real @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_297_order__refl)).
% 17.33/5.11 thf(903,plain,((! [A:real]: (ord_less_eq_real @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 17.33/5.11 thf(246,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((abs_abs_real @ (real_V783965509real_n @ A @ B)) = (real_V783965509real_n @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_190_real__abs__dist)).
% 17.33/5.11 thf(1216,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((abs_abs_real @ (real_V783965509real_n @ A @ B)) = (real_V783965509real_n @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 17.33/5.11 thf(143,axiom,((real_V1974343547l_num1 = (^ [A:finite463740460l_num1,B:finite463740460l_num1]: (real_V488409631l_num1 @ (finite1449546019l_num1 @ A @ one_one_Numeral_num1) @ (finite1449546019l_num1 @ B @ one_one_Numeral_num1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_245_dist__vector__1)).
% 17.33/5.11 thf(891,plain,(((real_V1974343547l_num1) = (^ [A:finite463740460l_num1,B:finite463740460l_num1]: (real_V488409631l_num1 @ (finite1449546019l_num1 @ A @ one_one_Numeral_num1) @ (finite1449546019l_num1 @ B @ one_one_Numeral_num1))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 17.33/5.11 thf(3,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: (ord_le1724070576l_num1 @ (abs_ab948591917l_num1 @ (minus_249161513l_num1 @ (abs_ab948591917l_num1 @ A) @ (abs_ab948591917l_num1 @ B))) @ (abs_ab948591917l_num1 @ (minus_249161513l_num1 @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_255_abs__triangle__ineq3)).
% 17.33/5.11 thf(368,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: (ord_le1724070576l_num1 @ (abs_ab948591917l_num1 @ (minus_249161513l_num1 @ (abs_ab948591917l_num1 @ A) @ (abs_ab948591917l_num1 @ B))) @ (abs_ab948591917l_num1 @ (minus_249161513l_num1 @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 17.33/5.11 thf(332,axiom,((! [A:int,B:real]: ((ord_less_eq_int @ A @ (archim1031974863r_real @ B)) = (ord_less_eq_real @ (ring_1_of_int_real @ A) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_219_le__floor__iff)).
% 17.33/5.11 thf(1453,plain,((! [A:int,B:real]: ((ord_less_eq_int @ A @ (archim1031974863r_real @ B)) = (ord_less_eq_real @ (ring_1_of_int_real @ A) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[332])).
% 17.33/5.11 thf(270,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n,D:finite1489363574real_n]: (((minus_1037315151real_n @ A @ B) = (minus_1037315151real_n @ C @ D)) => ((A = B) = (C = D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_62_diff__eq__diff__eq)).
% 17.33/5.11 thf(1276,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n,D:finite1489363574real_n]: (((minus_1037315151real_n @ A @ B) = (minus_1037315151real_n @ C @ D)) => ((A = B) = (C = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 17.33/5.11 thf(94,axiom,((! [A:int]: (member_int @ (ring_1_of_int_int @ A) @ ring_1_Ints_int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_50_Ints__of__int)).
% 17.33/5.11 thf(699,plain,((! [A:int]: (member_int @ (ring_1_of_int_int @ A) @ ring_1_Ints_int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 17.33/5.11 thf(310,axiom,((! [A:int,B:int]: ((member_int @ A @ ring_1_Ints_int) => ((member_int @ B @ ring_1_Ints_int) => ((A = B) = (ord_less_int @ (abs_abs_int @ (minus_minus_int @ A @ B)) @ one_one_int)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_186_Ints__eq__abs__less1)).
% 17.33/5.11 thf(1385,plain,((! [A:int,B:int]: ((member_int @ A @ ring_1_Ints_int) => ((member_int @ B @ ring_1_Ints_int) => ((A = B) = (ord_less_int @ (abs_abs_int @ (minus_minus_int @ A @ B)) @ one_one_int)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[310])).
% 17.33/5.11 thf(341,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n,D:finite1489363574real_n]: ((ord_le1017090250real_n @ A @ B) => ((ord_le1017090250real_n @ C @ D) => (ord_le1017090250real_n @ (minus_1037315151real_n @ A @ D) @ (minus_1037315151real_n @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_161_diff__strict__mono)).
% 17.33/5.11 thf(1476,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n,D:finite1489363574real_n]: ((ord_le1017090250real_n @ A @ B) => ((ord_le1017090250real_n @ C @ D) => (ord_le1017090250real_n @ (minus_1037315151real_n @ A @ D) @ (minus_1037315151real_n @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[341])).
% 17.33/5.11 thf(353,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((member1352538125real_n @ A @ ring_1723899781real_n) => ((member1352538125real_n @ B @ ring_1723899781real_n) => (member1352538125real_n @ (minus_1037315151real_n @ A @ B) @ ring_1723899781real_n))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_43_Ints__diff)).
% 17.33/5.11 thf(1508,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((member1352538125real_n @ A @ ring_1723899781real_n) => ((member1352538125real_n @ B @ ring_1723899781real_n) => (member1352538125real_n @ (minus_1037315151real_n @ A @ B) @ ring_1723899781real_n))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[353])).
% 17.33/5.11 thf(343,axiom,((! [A:int]: ((ring_1_of_int_real @ (abs_abs_int @ A)) = (abs_abs_real @ (ring_1_of_int_real @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_9_of__int__abs)).
% 17.33/5.11 thf(1481,plain,((! [A:int]: ((ring_1_of_int_real @ (abs_abs_int @ A)) = (abs_abs_real @ (ring_1_of_int_real @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[343])).
% 17.33/5.11 thf(112,axiom,((! [A:finite1183840848l_num1,B:numeral_num1]: (ord_less_eq_real @ (real_V646646907m_real @ (finite1106245191l_num1 @ A @ B)) @ (real_V400292255l_num1 @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_269_Finite__Cartesian__Product_Onorm__nth__le)).
% 17.33/5.11 thf(781,plain,((! [A:finite1183840848l_num1,B:numeral_num1]: (ord_less_eq_real @ (real_V646646907m_real @ (finite1106245191l_num1 @ A @ B)) @ (real_V400292255l_num1 @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 17.33/5.11 thf(294,axiom,((! [A:int]: (((ring_1_of_int_real @ A) = one_one_real) = (A = one_one_int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_102_of__int__eq__1__iff)).
% 17.33/5.11 thf(1341,plain,((! [A:int]: (((ring_1_of_int_real @ A) = one_one_real) = (A = one_one_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[294])).
% 17.33/5.11 thf(145,axiom,((! [A:(real > (real > $o)),B:real,C:real]: ((! [D:real,E:real]: ((ord_less_eq_real @ D @ E) => (A @ D @ E))) => ((! [D:real,E:real]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_315_linorder__wlog)).
% 17.33/5.11 thf(896,plain,((! [A:(real > (real > $o)),B:real,C:real]: ((! [D:real,E:real]: ((ord_less_eq_real @ D @ E) => (A @ D @ E))) => ((! [D:real,E:real]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 17.33/5.11 thf(347,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((abs_abs_real @ (real_V488409631l_num1 @ A @ B)) = (real_V488409631l_num1 @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_192_real__abs__dist)).
% 17.33/5.11 thf(1491,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((abs_abs_real @ (real_V488409631l_num1 @ A @ B)) = (real_V488409631l_num1 @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[347])).
% 17.33/5.11 thf(58,axiom,((~ (ord_less_int @ one_one_int @ one_one_int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_194_less__numeral__extra_I4_J)).
% 17.33/5.11 thf(568,plain,((~ (ord_less_int @ one_one_int @ one_one_int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 17.33/5.11 thf(51,axiom,((! [A:int,B:int,C:(int > $o)]: ((ord_less_int @ A @ B) => ((C @ A) => ((~ (C @ B)) => (? [D:int]: ((ord_less_eq_int @ A @ D) & (ord_less_eq_int @ D @ B) & ! [E:int]: (((ord_less_eq_int @ A @ E) & (ord_less_int @ E @ D)) => (C @ E)) & ! [E:int]: ((! [F:int]: (((ord_less_eq_int @ A @ F) & (ord_less_int @ F @ E)) => (C @ F))) => (ord_less_eq_int @ E @ D))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_298_complete__interval)).
% 17.33/5.11 thf(510,plain,((! [A:int,B:int,C:(int > $o)]: ((ord_less_int @ A @ B) => ((C @ A) => ((~ (C @ B)) => (? [D:int]: ((ord_less_eq_int @ A @ D) & (ord_less_eq_int @ D @ B) & ! [E:int]: (((ord_less_eq_int @ A @ E) & (ord_less_int @ E @ D)) => (C @ E)) & ! [E:int]: ((! [F:int]: (((ord_less_eq_int @ A @ F) & (ord_less_int @ F @ E)) => (C @ F))) => (ord_less_eq_int @ E @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 17.33/5.11 thf(82,axiom,((! [A:int,B:int]: ((A != B) => ((ord_less_eq_int @ A @ B) => (ord_less_int @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_301_order_Onot__eq__order__implies__strict)).
% 17.33/5.11 thf(667,plain,((! [A:int,B:int]: ((~ (A = B)) => ((ord_less_eq_int @ A @ B) => (ord_less_int @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 17.33/5.11 thf(238,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: (ord_le866583254real_n @ (abs_ab1599551059real_n @ (minus_1037315151real_n @ (abs_ab1599551059real_n @ A) @ (abs_ab1599551059real_n @ B))) @ (abs_ab1599551059real_n @ (minus_1037315151real_n @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_254_abs__triangle__ineq3)).
% 17.33/5.11 thf(1193,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: (ord_le866583254real_n @ (abs_ab1599551059real_n @ (minus_1037315151real_n @ (abs_ab1599551059real_n @ A) @ (abs_ab1599551059real_n @ B))) @ (abs_ab1599551059real_n @ (minus_1037315151real_n @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 17.33/5.11 thf(200,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) => (A = B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_341_antisym)).
% 17.33/5.11 thf(1077,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ B @ A) => (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 17.33/5.11 thf(106,axiom,((real_V1934908667t_real = (^ [A:real,B:real]: (real_V646646907m_real @ (minus_minus_real @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_141_dist__norm)).
% 17.33/5.11 thf(763,plain,(((real_V1934908667t_real) = (^ [A:real,B:real]: (real_V646646907m_real @ (minus_minus_real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 17.33/5.11 thf(355,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((real_V783965509real_n @ A @ (minus_1037315151real_n @ A @ B)) = (real_V739724485real_n @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_128_dist__diff_I1_J)).
% 17.33/5.11 thf(1513,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: ((real_V783965509real_n @ A @ (minus_1037315151real_n @ A @ B)) = (real_V739724485real_n @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[355])).
% 17.33/5.11 thf(88,axiom,((((=) @ finite2063899472l_num1) = (^ [A:finite2063899472l_num1,B:finite2063899472l_num1]: ! [C:numeral_num1]: ((finite1800583751l_num1 @ A @ C) = (finite1800583751l_num1 @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_38_vec__eq__iff)).
% 17.33/5.11 thf(684,plain,((((=) @ finite2063899472l_num1) = (^ [A:finite2063899472l_num1,B:finite2063899472l_num1]: ! [C:numeral_num1]: ((finite1800583751l_num1 @ A @ C) = (finite1800583751l_num1 @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 17.33/5.11 thf(328,axiom,((! [A:int,B:real]: ((ord_less_eq_int @ A @ (archim1371465213g_real @ B)) = (ord_less_real @ (minus_minus_real @ (ring_1_of_int_real @ A) @ one_one_real) @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_195_le__ceiling__iff)).
% 17.33/5.11 thf(1444,plain,((! [A:int,B:real]: ((ord_less_eq_int @ A @ (archim1371465213g_real @ B)) = (ord_less_real @ (minus_minus_real @ (ring_1_of_int_real @ A) @ one_one_real) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[328])).
% 17.33/5.11 thf(211,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:numeral_num1]: ((finite1106245191l_num1 @ (minus_249161513l_num1 @ A @ B) @ C) = (minus_minus_real @ (finite1106245191l_num1 @ A @ C) @ (finite1106245191l_num1 @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_7_vector__minus__component)).
% 17.33/5.11 thf(1116,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1,C:numeral_num1]: ((finite1106245191l_num1 @ (minus_249161513l_num1 @ A @ B) @ C) = (minus_minus_real @ (finite1106245191l_num1 @ A @ C) @ (finite1106245191l_num1 @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 17.33/5.11 thf(297,axiom,((~ (! [A:int]: ((ring_1_of_int_real @ A) != (minus_minus_real @ (finite772340589real_n @ x @ i) @ (finite772340589real_n @ y @ i)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_3__092_060open_062_092_060And_062thesis_O_A_I_092_060And_062m_O_Areal__of__int_Am_A_061_Ax_A_E_Ai_A_N_Ay_A_E_Ai_A_092_060Longrightarrow_062_Athesis_J_A_092_060Longrightarrow_062_Athesis_092_060close_062)).
% 17.33/5.11 thf(1348,plain,((~ (! [A:int]: ~ ((ring_1_of_int_real @ A) = (minus_minus_real @ (finite772340589real_n @ x @ i) @ (finite772340589real_n @ y @ i)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[297])).
% 17.33/5.11 thf(27,axiom,((! [A:int,B:int]: ((A = B) => (ord_less_eq_int @ A @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_336_eq__refl)).
% 17.33/5.11 thf(432,plain,((! [A:int,B:int]: ((A = B) => (ord_less_eq_int @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 17.33/5.11 thf(123,axiom,((! [A:int,B:int]: (((ring_1_of_int_int @ A) = (ring_1_of_int_int @ B)) = (A = B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_21_of__int__eq__iff)).
% 17.33/5.11 thf(818,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)],[123])).
% 17.33/5.11 thf(17,axiom,((! [A:real]: (ord_less_eq_int @ (archim1031974863r_real @ A) @ (archim1371465213g_real @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_278_floor__le__ceiling)).
% 17.33/5.11 thf(405,plain,((! [A:real]: (ord_less_eq_int @ (archim1031974863r_real @ A) @ (archim1371465213g_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 17.33/5.11 thf(134,axiom,((! [A:numeral_num1]: ((one_one_Numeral_num1 = A) = (A = one_one_Numeral_num1)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_137_one__reorient)).
% 17.33/5.11 thf(865,plain,((! [A:numeral_num1]: ((one_one_Numeral_num1 = A) = (A = one_one_Numeral_num1)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 17.33/5.11 thf(5,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((if_Fin1668193290l_num1 @ ($true) @ A @ B) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_If_1_1_If_001t__Finite____Cartesian____Product__Ovec_It__Real__Oreal_Mt__Numeral____Type__Onum1_J_T)).
% 17.33/5.11 thf(373,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: ((if_Fin1668193290l_num1 @ ($true) @ A @ B) = A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 17.33/5.11 thf(126,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/sandbox/benchmark/theBenchmark.p',fact_201_of__int__le__1__iff)).
% 17.33/5.11 thf(833,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)],[126])).
% 17.33/5.11 thf(19,axiom,((! [A:real,B:real]: ((real_V1934908667t_real @ A @ (minus_minus_real @ A @ B)) = (real_V646646907m_real @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_129_dist__diff_I1_J)).
% 17.33/5.11 thf(410,plain,((! [A:real,B:real]: ((real_V1934908667t_real @ A @ (minus_minus_real @ A @ B)) = (real_V646646907m_real @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 17.33/5.11 thf(166,axiom,((! [A:finite1489363574real_n]: ((member1352538125real_n @ A @ ring_1723899781real_n) => (~ (! [B:int]: (A != (ring_11737179077real_n @ B))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_57_Ints__cases)).
% 17.33/5.11 thf(967,plain,((! [A:finite1489363574real_n]: ((member1352538125real_n @ A @ ring_1723899781real_n) => (~ (! [B:int]: ~ (A = (ring_11737179077real_n @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 17.33/5.11 thf(160,axiom,((! [A:int,B:int,C:int,D:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ C @ D) => (ord_less_eq_int @ (minus_minus_int @ A @ D) @ (minus_minus_int @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_235_diff__mono)).
% 17.33/5.11 thf(950,plain,((! [A:int,B:int,C:int,D:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ C @ D) => (ord_less_eq_int @ (minus_minus_int @ A @ D) @ (minus_minus_int @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 17.33/5.11 thf(205,axiom,((! [A:real,B:real,C:real,D:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ C @ D) => (ord_less_eq_real @ (minus_minus_real @ A @ D) @ (minus_minus_real @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_236_diff__mono)).
% 17.33/5.11 thf(1097,plain,((! [A:real,B:real,C:real,D:real]: ((ord_less_eq_real @ A @ B) => ((ord_less_eq_real @ C @ D) => (ord_less_eq_real @ (minus_minus_real @ A @ D) @ (minus_minus_real @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 17.33/5.11 thf(302,axiom,((((=) @ finite1489363574real_n) = (^ [A:finite1489363574real_n,B:finite1489363574real_n]: ! [C:n]: ((finite772340589real_n @ A @ C) = (finite772340589real_n @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_36_vec__eq__iff)).
% 17.33/5.11 thf(1363,plain,((((=) @ finite1489363574real_n) = (^ [A:finite1489363574real_n,B:finite1489363574real_n]: ! [C:n]: ((finite772340589real_n @ A @ C) = (finite772340589real_n @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[302])).
% 17.33/5.11 thf(121,axiom,(((real_V646646907m_real @ one_one_real) = one_one_real)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_norm__one)).
% 17.33/5.11 thf(807,plain,(((real_V646646907m_real @ one_one_real) = one_one_real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 17.33/5.11 thf(93,axiom,((! [A:int]: (((ring_11737179077real_n @ A) = one_on1253059131real_n) = (A = one_one_int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_104_of__int__eq__1__iff)).
% 17.33/5.11 thf(696,plain,((! [A:int]: (((ring_11737179077real_n @ A) = one_on1253059131real_n) = (A = one_one_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 17.33/5.11 thf(100,axiom,((! [A:finite964658038_int_n,B:n]: ((finite625646243al_n_n @ (minkow371489429real_n @ A) @ B) = (ring_11737179077real_n @ (finite566214509_int_n @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_16_of__int__vec__nth)).
% 17.33/5.11 thf(720,plain,((! [A:finite964658038_int_n,B:n]: ((finite625646243al_n_n @ (minkow371489429real_n @ A) @ B) = (ring_11737179077real_n @ (finite566214509_int_n @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 17.33/5.11 thf(151,axiom,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ B @ A) => (B = A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_308_dual__order_Oantisym)).
% 17.33/5.11 thf(918,plain,((! [A:int,B:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ B @ A) => (B = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 17.33/5.11 thf(118,axiom,((ord_less_eq_int @ one_one_int @ one_one_int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_210_le__numeral__extra_I4_J)).
% 17.33/5.11 thf(801,plain,((ord_less_eq_int @ one_one_int @ one_one_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 17.33/5.11 thf(38,axiom,((! [A:int,B:int,C:int,D:int]: ((ord_less_int @ A @ B) => ((ord_less_int @ C @ D) => (ord_less_int @ (minus_minus_int @ A @ D) @ (minus_minus_int @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_164_diff__strict__mono)).
% 17.33/5.11 thf(474,plain,((! [A:int,B:int,C:int,D:int]: ((ord_less_int @ A @ B) => ((ord_less_int @ C @ D) => (ord_less_int @ (minus_minus_int @ A @ D) @ (minus_minus_int @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 17.33/5.11 thf(108,axiom,((! [A:n]: ((finite566214509_int_n @ one_on1516019131_int_n @ A) = one_one_int))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_101_one__index)).
% 17.33/5.11 thf(767,plain,((! [A:n]: ((finite566214509_int_n @ one_on1516019131_int_n @ A) = one_one_int))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 17.33/5.11 thf(163,axiom,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_int @ (archim1031974863r_real @ A) @ (archim1031974863r_real @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_208_floor__mono)).
% 17.33/5.11 thf(960,plain,((! [A:real,B:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_int @ (archim1031974863r_real @ A) @ (archim1031974863r_real @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 17.33/5.11 thf(340,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n]: ((ord_le866583254real_n @ A @ B) => (ord_le866583254real_n @ (minus_1037315151real_n @ C @ B) @ (minus_1037315151real_n @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_229_diff__left__mono)).
% 17.33/5.11 thf(1473,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n,C:finite1489363574real_n]: ((ord_le866583254real_n @ A @ B) => (ord_le866583254real_n @ (minus_1037315151real_n @ C @ B) @ (minus_1037315151real_n @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[340])).
% 17.33/5.11 thf(74,axiom,((! [A:real,B:real]: ((~ (ord_less_eq_real @ A @ B)) => (ord_less_eq_real @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_335_le__cases)).
% 17.33/5.11 thf(624,plain,((! [A:real,B:real]: ((~ (ord_less_eq_real @ A @ B)) => (ord_less_eq_real @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 17.33/5.11 thf(363,axiom,((! [A:real]: ((member_real @ A @ ring_1_Ints_real) => (member_real @ (abs_abs_real @ A) @ ring_1_Ints_real)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_48_Ints__abs)).
% 17.33/5.11 thf(1532,plain,((! [A:real]: ((member_real @ A @ ring_1_Ints_real) => (member_real @ (abs_abs_real @ A) @ ring_1_Ints_real)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[363])).
% 17.33/5.11 thf(365,axiom,((! [A:finite1489363574real_n,B:finite1489363574real_n]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (real_V739724485real_n @ A) @ (real_V739724485real_n @ B))) @ (real_V739724485real_n @ (minus_1037315151real_n @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_291_norm__triangle__ineq3)).
% 17.33/5.11 thf(1537,plain,((! [A:finite1489363574real_n,B:finite1489363574real_n]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (real_V739724485real_n @ A) @ (real_V739724485real_n @ B))) @ (real_V739724485real_n @ (minus_1037315151real_n @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[365])).
% 17.33/5.11 thf(182,axiom,((member_int @ one_one_int @ ring_1_Ints_int)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_181_Ints__1)).
% 17.33/5.11 thf(1019,plain,((member_int @ one_one_int @ ring_1_Ints_int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 17.33/5.11 thf(101,axiom,((real_V488409631l_num1 = (^ [A:finite1183840848l_num1,B:finite1183840848l_num1]: (real_V400292255l_num1 @ (minus_249161513l_num1 @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_142_dist__norm)).
% 17.33/5.11 thf(723,plain,(((real_V488409631l_num1) = (^ [A:finite1183840848l_num1,B:finite1183840848l_num1]: (real_V400292255l_num1 @ (minus_249161513l_num1 @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 17.33/5.11 thf(131,axiom,((! [A:real,B:real,C:real,D:real]: (((minus_minus_real @ A @ B) = (minus_minus_real @ C @ D)) => ((ord_less_eq_real @ A @ B) = (ord_less_eq_real @ C @ D))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_224_diff__eq__diff__less__eq)).
% 17.33/5.11 thf(850,plain,((! [A:real,B:real,C:real,D:real]: (((minus_minus_real @ A @ B) = (minus_minus_real @ C @ D)) => ((ord_less_eq_real @ A @ B) = (ord_less_eq_real @ C @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 17.33/5.11 thf(171,axiom,((! [A:numeral_num1]: ((real_V400292255l_num1 @ (finite15144922381_real @ A @ one_one_real)) = one_one_real))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_89_norm__axis__1)).
% 17.33/5.11 thf(982,plain,((! [A:numeral_num1]: ((real_V400292255l_num1 @ (finite15144922381_real @ A @ one_one_real)) = one_one_real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 17.33/5.11 thf(278,axiom,((! [A:int]: ((member_int @ A @ ring_1_Ints_int) => (member_int @ (abs_abs_int @ A) @ ring_1_Ints_int)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_Ints__abs)).
% 17.33/5.11 thf(1299,plain,((! [A:int]: ((member_int @ A @ ring_1_Ints_int) => (member_int @ (abs_abs_int @ A) @ ring_1_Ints_int)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 17.33/5.11 thf(91,axiom,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: (ord_less_eq_real @ (minus_minus_real @ (real_V400292255l_num1 @ A) @ (real_V400292255l_num1 @ B)) @ (real_V400292255l_num1 @ (minus_249161513l_num1 @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_282_norm__triangle__ineq2)).
% 17.33/5.11 thf(691,plain,((! [A:finite1183840848l_num1,B:finite1183840848l_num1]: (ord_less_eq_real @ (minus_minus_real @ (real_V400292255l_num1 @ A) @ (real_V400292255l_num1 @ B)) @ (real_V400292255l_num1 @ (minus_249161513l_num1 @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 17.33/5.11 thf(136,axiom,((! [A:(numeral_num1 > (int > $o))]: ((! [B:numeral_num1]: ? [C:int]: (A @ B @ C)) = (? [B:finite2063899472l_num1]: ! [C:numeral_num1]: (A @ C @ (finite1800583751l_num1 @ B @ C)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_34_lambda__skolem)).
% 17.33/5.11 thf(871,plain,((! [A:(numeral_num1 > (int > $o))]: ((! [B:numeral_num1]: ? [C:int]: (A @ B @ C)) = (? [B:finite2063899472l_num1]: ! [C:numeral_num1]: (A @ C @ (finite1800583751l_num1 @ B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 17.33/5.11 thf(352,axiom,((! [A:real]: ((abs_abs_real @ (abs_abs_real @ A)) = (abs_abs_real @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_abs__idempotent)).
% 17.33/5.11 thf(1505,plain,((! [A:real]: ((abs_abs_real @ (abs_abs_real @ A)) = (abs_abs_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[352])).
% 17.33/5.11 thf(213,axiom,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_real @ (minus_minus_real @ C @ B) @ (minus_minus_real @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_diff__left__mono)).
% 17.33/5.11 thf(1120,plain,((! [A:real,B:real,C:real]: ((ord_less_eq_real @ A @ B) => (ord_less_eq_real @ (minus_minus_real @ C @ B) @ (minus_minus_real @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 17.33/5.11 thf(68,axiom,((! [A:int,B:int,C:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ B @ C) => (ord_less_eq_int @ A @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_318_order__trans)).
% 17.33/5.11 thf(607,plain,((! [A:int,B:int,C:int]: ((ord_less_eq_int @ A @ B) => ((ord_less_eq_int @ B @ C) => (ord_less_eq_int @ A @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 17.33/5.11 thf(290,axiom,((! [A:real]: (ord_less_eq_real @ (minus_minus_real @ (ring_1_of_int_real @ (archim1371465213g_real @ A)) @ one_one_real) @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_279_of__int__ceiling__diff__one__le)).
% 17.33/5.11 thf(1331,plain,((! [A:real]: (ord_less_eq_real @ (minus_minus_real @ (ring_1_of_int_real @ (archim1371465213g_real @ A)) @ one_one_real) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[290])).
% 17.33/5.11 thf(234,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/sandbox/benchmark/theBenchmark.p',fact_202_of__int__le__1__iff)).
% 17.33/5.11 thf(1184,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)],[234])).
% 17.33/5.11 thf(336,axiom,((! [A:real,B:real]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (real_V646646907m_real @ A) @ (real_V646646907m_real @ B))) @ (real_V646646907m_real @ (minus_minus_real @ A @ B))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_292_norm__triangle__ineq3)).
% 17.33/5.11 thf(1463,plain,((! [A:real,B:real]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (real_V646646907m_real @ A) @ (real_V646646907m_real @ B))) @ (real_V646646907m_real @ (minus_minus_real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[336])).
% 17.33/5.11 thf(110,axiom,((! [A:int,B:int,C:int]: ((ord_less_int @ A @ B) => (ord_less_int @ (minus_minus_int @ C @ B) @ (minus_minus_int @ C @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_172_diff__strict__left__mono)).
% 17.33/5.11 thf(775,plain,((! [A:int,B:int,C:int]: ((ord_less_int @ A @ B) => (ord_less_int @ (minus_minus_int @ C @ B) @ (minus_minus_int @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 17.33/5.11 thf(319,axiom,((! [A:real]: ? [B:int]: (ord_less_real @ A @ (ring_1_of_int_real @ B)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_157_ex__less__of__int)).
% 17.33/5.11 thf(1416,plain,((! [A:real]: ? [B:int]: (ord_less_real @ A @ (ring_1_of_int_real @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[319])).
% 17.33/5.11 thf(103,axiom,((! [A:int,B:int,C:int]: ((ord_less_int @ A @ B) => (ord_less_int @ (minus_minus_int @ A @ C) @ (minus_minus_int @ B @ C))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_176_diff__strict__right__mono)).
% 17.33/5.11 thf(755,plain,((! [A:int,B:int,C:int]: ((ord_less_int @ A @ B) => (ord_less_int @ (minus_minus_int @ A @ C) @ (minus_minus_int @ B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 17.33/5.11 thf(180,axiom,((real_V316032763l_num1 = (^ [A:finite463740460l_num1]: (real_V400292255l_num1 @ (finite1449546019l_num1 @ A @ one_one_Numeral_num1))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_241_norm__vector__1)).
% 17.33/5.11 thf(1014,plain,(((real_V316032763l_num1) = (^ [A:finite463740460l_num1]: (real_V400292255l_num1 @ (finite1449546019l_num1 @ A @ one_one_Numeral_num1))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 17.33/5.11 thf(242,axiom,((! [A:real]: ((abs_abs_real @ (abs_abs_real @ A)) = (abs_abs_real @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_25_abs__abs)).
% 17.33/5.11 thf(1204,plain,((! [A:real]: ((abs_abs_real @ (abs_abs_real @ A)) = (abs_abs_real @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 17.33/5.11 thf(330,axiom,((! [A:real,B:real,C:real]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (real_V1934908667t_real @ A @ B) @ (real_V1934908667t_real @ B @ C))) @ (real_V1934908667t_real @ A @ C)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_284_abs__dist__diff__le)).
% 17.33/5.11 thf(1449,plain,((! [A:real,B:real,C:real]: (ord_less_eq_real @ (abs_abs_real @ (minus_minus_real @ (real_V1934908667t_real @ A @ B) @ (real_V1934908667t_real @ B @ C))) @ (real_V1934908667t_real @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[330])).
% 17.33/5.11 thf(1556,plain,(($false)),inference(e,[status(thm)],[809,1411,1237,628,893,962,481,1406,1290,1522,1073,379,1305,1158,582,1173,1486,1497,384,1310,550,500,715,913,670,1001,1243,1391,1441,885,436,1518,1228,1409,1287,570,1430,504,1264,1511,802,1191,1132,587,1323,619,838,1313,1279,542,460,853,1379,421,1479,1347,770,416,1100,448,1494,1489,924,1465,1373,1040,376,1418,646,1151,1020,821,905,602,877,1447,1119,396,998,988,1433,1201,507,678,1438,761,1338,366,942,439,1047,798,1057,1274,910,957,778,1042,1355,1502,424,429,1123,862,407,693,788,1370,467,1032,1365,1195,1128,456,974,847,484,1296,665,493,1210,1360,874,650,1534,1328,1111,725,388,610,783,1089,1234,1270,1259,933,1182,1461,706,686,1075,1016,1207,622,647,985,701,1249,1451,1231,1060,1246,1525,393,1114,1456,1382,1333,1318,1241,921,1170,1035,1187,1167,953,794,765,1054,718,888,1146,1103,1273,1301,573,689,1219,824,402,1389,1125,579,1403,1520,413,584,1154,1226,545,391,936,382,1271,1239,1092,804,704,947,1224,540,681,1282,996,451,1144,880,616,1376,1307,1175,979,604,1011,419,477,387,1471,1080,631,758,848,1325,1029,626,1344,1293,1177,1149,964,1198,399,1213,1044,883,1435,1528,868,1413,426,944,1467,548,487,939,553,836,1049,490,675,1516,1070,1156,1400,971,1252,1368,1267,1531,1484,1499,673,791,502,1262,463,1130,1285,1336,907,1038,370,470,576,1358,1257,1141,613,1221,1353,1052,1427,1094,1008,497,991,1316,1459,1180,1321,495,1189,1108,1421,465,976,903,1216,891,368,1453,1276,699,1385,1476,1508,1481,781,1341,896,1491,568,510,667,1193,1077,763,1513,684,1444,1116,1348,432,818,405,865,373,833,410,967,950,1097,1363,807,696,720,918,801,474,767,960,1473,624,1532,1537,1019,723,850,982,1299,691,871,1505,1120,607,1331,1184,1463,775,1416,755,1014,1204,1449])).
% 17.33/5.11 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.33/5.11 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------