%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP118^2 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n004.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 37.31s 15.54s
% Output : Refutation 38.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP118^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.11/0.20 % Computer : n004.cluster.edu
% 0.11/0.20 % Model : x86_64 x86_64
% 0.11/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.20 % Memory : 8046.5625MB
% 0.11/0.20 % OS : Linux 6.8.0-71-generic
% 0.11/0.20 % CPULimit : 300
% 0.11/0.20 % WCLimit : 300
% 0.11/0.20 % DateTime : Tue Sep 29 19:56:22 UTC 2026
% 0.11/0.20 % CPUTime :
% 0.11/0.20 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.85/0.77 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 2.04/1.14 % [INFO] Parsing done (368ms).
% 2.04/1.16 % [INFO] Running in sequential loop mode.
% 3.28/1.56 % [INFO] eprover registered as external prover.
% 3.28/1.56 % [INFO] Scanning for conjecture ...
% 3.72/1.72 % [INFO] Found a conjecture (or negated_conjecture) and 366 axioms. Running axiom selection ...
% 3.95/1.87 % [INFO] Axiom selection finished. Selected 365 axioms (removed 1 axioms).
% 5.18/2.14 % [INFO] Problem is higher-order (TPTP THF).
% 5.18/2.17 % [INFO] Type checking passed.
% 5.18/2.17 % [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 ...
% 37.31/15.53 % External prover 'e' found a proof!
% 37.31/15.53 % [INFO] Killing All external provers ...
% 37.31/15.54 % Time passed: 15198ms (effective reasoning time: 14370ms)
% 37.31/15.54 % 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)>
% 37.31/15.54 % Axioms used in derivation (365): fact_63_dist__diff_I2_J, fact_34_ceiling__diff__of__int, tcon_Real_Oreal___Orderings_Opreorder_26, fact_132_abs__triangle__ineq2, fact_246_dual__order_Ostrict__trans1, fact_88_abs__one, fact_7__092_060open_062x_A_E_Ai_A_N_Ay_A_E_Ai_A_092_060in_062_A_092_060int_062_092_060close_062, tcon_fun___Groups_Ominus, fact_140_dist__real, fact_224_order__le__less__subst1, fact_87_diff__strict__right__mono, fact_164_order__class_Oorder_Oantisym, tfree_0, tcon_Finite__Cartesian__Product_Ovec___Nat_Oring__char__0_65, fact_142_of__int__ceiling__diff__one__le, fact_136_of__int__floor__le, fact_36_vec_Oscale__left__diff__distrib, tcon_HOL_Obool___Orderings_Olinorder_14, tcon_Numeral__Type_Onum1___Cardinality_OCARD__1, tcon_Set_Oset___Groups_Omonoid__mult_6, tcon_fun___Finite__Set_Ofinite, fact_78_floor__less__cancel, fact_160_dual__order_Otrans, fact_251_dual__order_Oorder__iff__strict, tcon_Numeral__Type_Onum1___Groups_Oone_51, tcon_Finite__Cartesian__Product_Ovec___Real__Vector__Spaces_Oreal__normed__vector_53, fact_128_ceiling__diff__floor__le__1, fact_131_abs__triangle__ineq3, tcon_Int_Oint___Groups_Ozero, tcon_Finite__Cartesian__Product_Ovec___Groups_Ocancel__ab__semigroup__add_56, fact_139_component__le__norm__cart, fact_74_linorder__neqE__linordered__idom, fact_198_less__induct, fact_71_less__ceiling__iff, fact_166_ord__eq__le__trans, fact_59_vector__ssub__ldistrib, fact_16_assms, tcon_Int_Oint___Orderings_Oorder_2, fact_21_Ints__induct, fact_81_ex__less__of__int, fact_241_not__le__imp__less, fact_180_le__fun__def, tcon_Int_Oint___Nat_Oring__char__0, fact_124_norm__vector__1, fact_158_dual__order_Oantisym, fact_193_dual__order_Oirrefl, fact_157_complete__real, fact_189_linorder__less__wlog, fact_147_norm__triangle__ineq3, fact_55_vec__1, fact_0__C1_C_I2_J, tcon_Int_Oint___Rings_Oring__1, fact_15_vec__eq__iff, fact_159_dual__order_Oeq__iff, fact_119_diff__right__mono, fact_161_linorder__wlog, tcon_Int_Oint___Groups_Omonoid__mult, fact_209_less__imp__neq, fact_13_abs__minus__commute, fact_254_ex__1, tcon_Int_Oint___Groups_Oordered__ab__group__add, tcon_Int_Oint___Groups_Ominus_4, fact_121_diff__mono, fact_94_of__int__floor__cancel, fact_220_leD, fact_183_le__funD, fact_102_of__int__le__iff, tcon_fun___Orderings_Oord, fact_134_Finite__Cartesian__Product_Onorm__nth__le, tcon_Numeral__Type_Onum1___Groups_Ominus_48, tcon_Real_Oreal___Orderings_Ono__top_29, tcon_Real_Oreal___Groups_Ogroup__add_31, fact_75_dist__commute__lessI, fact_156_less__vec__def, fact_243_order_Ostrict__trans2, fact_237_dense__le, fact_73_dist__norm, tcon_Real_Oreal___Conditionally__Complete__Lattices_Oconditionally__complete__linorder_19, fact_58_vec__component, tcon_Numeral__Type_Onum1___Groups_Omonoid__mult_43, fact_41_vec_Oscale__one, fact_95_real__of__int__floor__gt__diff__one, fact_64_dist__diff_I1_J, fact_244_order_Oorder__iff__strict, fact_52_abs__norm__cancel, fact_199_less__not__sym, fact_114_int__le__induct, fact_99_le__ceiling__iff, fact_32__C1_C_I3_J, tcon_HOL_Obool___Finite__Set_Ofinite_15, fact_173_linear, fact_4_vector__minus__component, fact_11_abs__idempotent, fact_145_metric__eq__thm, tcon_Finite__Cartesian__Product_Ovec___Orderings_Oord_66, fact_14_lambda__skolem, fact_178_order__subst2, fact_91_vec_Oscale__right__diff__distrib, 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_219_ord__eq__less__subst, fact_31_vector__sub__rdistrib, fact_155_vector__one__nth, tcon_Real_Oreal___Groups_Oone_39, tcon_HOL_Obool___Orderings_Oord_17, fact_106_one__le__floor, fact_217_order__less__subst1, fact_61_of__int__less__1__iff, fact_76_dist__commute, fact_175_eq__iff, fact_27_cond__component, tcon_Numeral__Type_Onum1___Rings_Oring_50, fact_221_leI, fact_80_real__norm__def, tcon_Real_Oreal___Orderings_Oorder_32, fact_214_gt__ex, tcon_Int_Oint___Orderings_Opreorder_1, tcon_Real_Oreal___Rings_Oring__1_35, fact_67_floor__diff__one, fact_65_floor__less__one, tcon_Int_Oint___Rings_Oidom__abs__sgn, fact_211_order_Oasym, tcon_Numeral__Type_Onum1___Orderings_Owellorder, tcon_Real_Oreal___Groups_Oordered__ab__group__add__abs_21, fact_53_floor__one, fact_163_order__trans, fact_182_le__funE, fact_19_Ints__abs, fact_42_vector__smult__lid, tcon_Set_Oset___Finite__Set_Ofinite_7, fact_240_less__le__not__le, tcon_Finite__Cartesian__Product_Ovec___Groups_Ozero_69, fact_24_diff__eq__diff__eq, fact_234_le__less__trans, fact_38_norm__axis__1, fact_83_norm__bound__component__lt__cart, fact_68_ceiling__diff__one, fact_29_dist__of__int, fact_89_dist__real__def, fact_242_order_Ostrict__trans1, tcon_Real_Oreal___Rings_Oring_38, fact_9_of__int__eq__iff, fact_236_dense__ge, fact_141_floor__le__ceiling, fact_62_norm__one, fact_186_order_Ostrict__implies__not__eq, tcon_Real_Oreal___Real__Vector__Spaces_Ometric__space, tcon_Finite__Cartesian__Product_Ovec___Groups_Ogroup__add_63, tcon_Int_Oint___Conditionally__Complete__Lattices_Oconditionally__complete__linorder, help_If_1_1_T, tcon_Real_Oreal___Groups_Omonoid__mult_28, fact_216_order__less__subst2, tcon_Set_Oset___Orderings_Oord_9, fact_23_diff__right__commute, fact_154_dual__order_Ostrict__implies__order, fact_43_abs__1, fact_167_order__class_Oorder_Oeq__iff, fact_194_linorder__cases, fact_111_le__numeral__extra_I4_J, fact_144_abs__dist__diff__le, fact_174_antisym, fact_235_less__le__trans, tcon_Real_Oreal___Rings_Olinordered__idom_24, fact_72_vec_Oscale__left__commute, tcon_Real_Oreal___Groups_Ominus_36, fact_162_dual__order_Orefl, fact_118_diff__eq__diff__less__eq, fact_218_ord__less__eq__subst, fact_205_less__linear, fact_245_order_Ostrict__iff__order, fact_39_vec__eq, tcon_Int_Oint___Rings_Olinordered__idom, tcon_Int_Oint___Orderings_Olinorder, tcon_Real_Oreal___Real__Vector__Spaces_Oreal__normed__vector, fact_112_less__eq__vec__def, fact_116_le__floor__iff, fact_201_dual__order_Oasym, tcon_Numeral__Type_Onum1___Orderings_Oord_47, fact_126_dist__vector__1, fact_85_diff__eq__diff__less, fact_184_ex__gt__or__lt, fact_105_of__int__1__le__iff, fact_206_less__trans, fact_122_abs__ge__self, tcon_Real_Oreal___Groups_Ocancel__ab__semigroup__add_22, fact_230_le__neq__trans, fact_90_Ints__1, fact_223_less__le, fact_135_real__of__int__floor__ge__diff__one, fact_151_complete__interval, tcon_HOL_Obool___Orderings_Oorder_16, fact_69_one__reorient, fact_238_le__less__linear, fact_185_dual__order_Ostrict__implies__not__eq, fact_197_antisym__conv3, tcon_Real_Oreal___Orderings_Olinorder_27, fact_93_of__int__ceiling__cancel, fact_103_zle__diff1__eq, tcon_Set_Oset___Groups_Oone_12, tcon_Numeral__Type_Onum1___Groups_Ogroup__add_45, fact_228_not__le, fact_168_antisym__conv, fact_56_floor__of__int, tcon_Real_Oreal___Conditionally__Complete__Lattices_Olinear__continuum, fact_192_order_Ostrict__trans, fact_6_of__int__diff, fact_143_norm__triangle__ineq2, fact_10_abs__abs, fact_212_neq__iff, fact_100_ceiling__split, fact_200_less__imp__not__eq, tcon_Finite__Cartesian__Product_Ovec___Orderings_Opreorder_59, fact_138_norm__bound__component__le__cart, tcon_Real_Oreal___Orderings_Odense__linorder, fact_57_ceiling__of__int, fact_113_int__less__induct, tcon_Int_Oint___Groups_Ocancel__ab__semigroup__add, tcon_Real_Oreal___Orderings_Odense__order, fact_129_ceiling__less__iff, fact_225_order__le__less__subst2, fact_107_ceiling__le__one, tcon_Real_Oreal___Ordered__Euclidean__Space_Oordered__euclidean__space, fact_171_le__cases, fact_233_less__imp__le, tcon_Real_Oreal___Groups_Oordered__ab__group__add_23, tcon_Int_Oint___Groups_Ogroup__add, fact_213_neqE, fact_49_one__index, fact_66_one__less__ceiling, tcon_Real_Oreal___Archimedean__Field_Ofloor__ceiling, tcon_Finite__Cartesian__Product_Ovec___Real__Vector__Spaces_Ometric__space_54, fact_18_Ints__diff, fact_226_order__less__le__subst1, fact_109_floor__mono, fact_137_le__of__int__ceiling, help_If_3_1_T, fact_40_vec__inj, help_If_2_1_T, fact_5_of__int__abs, fact_79_norm__minus__commute, fact_50_of__int__eq__1__iff, fact_222_le__less, tcon_Finite__Cartesian__Product_Ovec___Orderings_Olinorder_60, fact_204_less__irrefl, fact_120_diff__left__mono, tcon_Numeral__Type_Onum1___Groups_Ocancel__ab__semigroup__add_40, fact_203_ord__eq__less__trans, fact_227_order__less__le__subst2, fact_117_ceiling__le__iff, fact_8_of__int__vec__nth, fact_86_diff__strict__left__mono, fact_110_less__eq__real__def, fact_248_dense__ge__bounded, tcon_Numeral__Type_Onum1___Finite__Set_Ofinite_44, fact_188_dual__order_Ostrict__trans, tcon_HOL_Obool___Groups_Ominus_18, fact_232_antisym__conv2, tcon_Real_Oreal___Orderings_Oord_34, fact_98_axis__index__axis, tcon_fun___Orderings_Opreorder, tcon_Finite__Cartesian__Product_Ovec___Groups_Oordered__ab__group__add_58, fact_104_of__int__le__1__iff, fact_45_Collect__mem__eq, fact_215_lt__ex, fact_190_exists__least__iff, fact_1__C1_C_I1_J, tcon_Finite__Cartesian__Product_Ovec___Groups_Oone_71, fact_108_ceiling__mono, fact_249_dense__le__bounded, fact_97_less__numeral__extra_I4_J, fact_229_not__less, fact_181_le__funI, tcon_Set_Oset___Orderings_Oorder_8, tcon_Int_Oint___Rings_Oring, fact_84_diff__strict__mono, fact_25_fun__diff__def, fact_115_ceiling__le, fact_20_Ints__of__int, fact_82_ex__of__int__less, subcl_Finite__Set_Ofinite___HOL_Otype, fact_191_less__imp__not__less, fact_210_dense, tcon_Int_Oint___Groups_Oordered__ab__group__add__abs, fact_208_less__asym, tcon_Real_Oreal___Real__Vector__Spaces_Odist__norm, fact_101_ceiling__eq__iff, tcon_Numeral__Type_Onum1___Groups_Ozero_49, fact_30_vec__sub, tcon_Finite__Cartesian__Product_Ovec___Ordered__Euclidean__Space_Oordered__euclidean__space_52, fact_22_Ints__cases, fact_252_dual__order_Ostrict__iff__order, tcon_Numeral__Type_Onum1___Orderings_Olinorder_42, fact_123_abs__le__D1, tcon_Finite__Cartesian__Product_Ovec___Finite__Set_Ofinite_62, fact_26_vec__nth__inject, fact_195_less__imp__triv, tcon_Set_Oset___Groups_Ominus_10, fact_247_dual__order_Ostrict__trans2, fact_37_floor__diff__of__int, tcon_fun___Orderings_Oorder, fact_33_norm__of__int, tcon_Real_Oreal___Rings_Olinordered__nonzero__semiring_20, tcon_Finite__Cartesian__Product_Ovec___Real__Vector__Spaces_Odist__norm_57, tcon_Int_Oint___Orderings_Ono__bot, fact_207_less__asym_H, fact_250_order_Ostrict__implies__order, tcon_Finite__Cartesian__Product_Ovec___Orderings_Oorder_64, tcon_Real_Oreal___Real__Vector__Spaces_Oreal__normed__algebra__1, fact_51_of__int__1, fact_96_real__abs__dist, tcon_Finite__Cartesian__Product_Ovec___Groups_Ominus_68, fact_172_eq__refl, fact_92_Ints__eq__abs__less1, tcon_Int_Oint___Orderings_Ono__top, fact_231_antisym__conv1, fact_149_ceiling__unique, tcon_Real_Oreal___Nat_Oring__char__0_33, fact_35_axis__nth, tcon_Numeral__Type_Onum1___Orderings_Oorder_46, tcon_Finite__Cartesian__Product_Ovec___Rings_Oring__1_67, fact_152_eucl__less__le__not__le, fact_239_le__imp__less__or__eq, fact_187_not__less__iff__gr__or__eq, fact_12_minus__apply, fact_176_ord__le__eq__subst, fact_48_of__int__less__iff, tcon_Real_Oreal___Archimedean__Field_Oarchimedean__field, tcon_Real_Oreal___Rings_Oidom__abs__sgn_25, tcon_Int_Oint___Orderings_Oord_3, fact_28_nth__map__matrix, fact_130_abs__triangle__ineq2__sym, fact_125_ex__le__of__int, fact_70_floor__less__iff, fact_196_less__imp__not__eq2, tcon_Set_Oset___Orderings_Opreorder_5, fact_170_order_Otrans, fact_146_dist__vec__nth__le, tcon_HOL_Obool___Orderings_Opreorder_13, fact_133_norm__le__componentwise__cart, tcon_Real_Oreal___Orderings_Ono__bot_30, tcon_Finite__Cartesian__Product_Ovec___Rings_Oring_70, tcon_Int_Oint___Rings_Olinordered__nonzero__semiring, tcon_Real_Oreal___Fields_Ofield, fact_54_ceiling__one, fact_77_ceiling__less__cancel, fact_148_ceiling__correct, tcon_Int_Oint___Groups_Oone, tcon_Finite__Cartesian__Product_Ovec___Groups_Omonoid__mult_61, fact_46_Collect__cong, fact_179_order__subst1, fact_153_order_Onot__eq__order__implies__strict, fact_253_forall__1, tcon_Set_Oset___Groups_Ozero_11, tcon_Finite__Cartesian__Product_Ovec___Groups_Oordered__ab__group__add__abs_55, fact_169_le__cases3, fact_60_of__int__1__less__iff, tcon_Real_Oreal___Groups_Ozero_37, fact_202_ord__less__eq__trans, fact_127_norm__real, tcon_Numeral__Type_Onum1___Orderings_Opreorder_41, fact_177_ord__eq__le__subst, fact_44_mem__Collect__eq, fact_165_ord__le__eq__trans, fact_2_m, fact_17_of__int__vec__eq__iff, fact_150_order__refl
% 37.31/15.54 % No. of inferences in proof: 734
% 37.31/15.54 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 15198 ms resp. 14370 ms w/o parsing
% 38.74/15.80 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 38.74/15.80 thf(numeral_num1_type, type, numeral_num1: $tType).
% 38.74/15.80 thf(real_type, type, real: $tType).
% 38.74/15.80 thf(int_type, type, int: $tType).
% 38.74/15.80 thf(n_type, type, n: $tType).
% 38.74/15.80 thf(cARD_1_decl, type, cARD_1: !> [TA: $tType]: $o).
% 38.74/15.80 thf(type_decl, type, type: !> [TA: $tType]: $o).
% 38.74/15.80 thf(one_decl, type, one: !> [TA: $tType]: $o).
% 38.74/15.80 thf(ring_decl, type, ring: !> [TA: $tType]: $o).
% 38.74/15.80 thf(zero_decl, type, zero: !> [TA: $tType]: $o).
% 38.74/15.80 thf(field_decl, type, field: !> [TA: $tType]: $o).
% 38.74/15.80 thf(minus_decl, type, minus: !> [TA: $tType]: $o).
% 38.74/15.80 thf(ring_1_decl, type, ring_1: !> [TA: $tType]: $o).
% 38.74/15.80 thf(ord_decl, type, ord: !> [TA: $tType]: $o).
% 38.74/15.80 thf(ring_char_0_decl, type, ring_char_0: !> [TA: $tType]: $o).
% 38.74/15.80 thf(order_decl, type, order: !> [TA: $tType]: $o).
% 38.74/15.80 thf(group_add_decl, type, group_add: !> [TA: $tType]: $o).
% 38.74/15.80 thf(no_bot_decl, type, no_bot: !> [TA: $tType]: $o).
% 38.74/15.80 thf(no_top_decl, type, no_top: !> [TA: $tType]: $o).
% 38.74/15.80 thf(finite_finite_decl, type, finite_finite: !> [TA: $tType]: $o).
% 38.74/15.80 thf(monoid_mult_decl, type, monoid_mult: !> [TA: $tType]: $o).
% 38.74/15.80 thf(linorder_decl, type, linorder: !> [TA: $tType]: $o).
% 38.74/15.80 thf(preorder_decl, type, preorder: !> [TA: $tType]: $o).
% 38.74/15.80 thf(idom_abs_sgn_decl, type, idom_abs_sgn: !> [TA: $tType]: $o).
% 38.74/15.80 thf(wellorder_decl, type, wellorder: !> [TA: $tType]: $o).
% 38.74/15.80 thf(dense_order_decl, type, dense_order: !> [TA: $tType]: $o).
% 38.74/15.80 thf(linordered_idom_decl, type, linordered_idom: !> [TA: $tType]: $o).
% 38.74/15.80 thf(dense_linorder_decl, type, dense_linorder: !> [TA: $tType]: $o).
% 38.74/15.80 thf(ordered_ab_group_add_decl, type, ordered_ab_group_add: !> [TA: $tType]: $o).
% 38.74/15.80 thf(real_V1639655670t_norm_decl, type, real_V1639655670t_norm: !> [TA: $tType]: $o).
% 38.74/15.80 thf(cancel146912293up_add_decl, type, cancel146912293up_add: !> [TA: $tType]: $o).
% 38.74/15.80 thf(archim1727834104eiling_decl, type, archim1727834104eiling: !> [TA: $tType]: $o).
% 38.74/15.80 thf(ordere142940540dd_abs_decl, type, ordere142940540dd_abs: !> [TA: $tType]: $o).
% 38.74/15.80 thf(real_V2090557954_space_decl, type, real_V2090557954_space: !> [TA: $tType]: $o).
% 38.74/15.80 thf(linord1659791738miring_decl, type, linord1659791738miring: !> [TA: $tType]: $o).
% 38.74/15.80 thf(archim1804426504_field_decl, type, archim1804426504_field: !> [TA: $tType]: $o).
% 38.74/15.80 thf(real_V55928688vector_decl, type, real_V55928688vector: !> [TA: $tType]: $o).
% 38.74/15.80 thf(real_V1229719638ebra_1_decl, type, real_V1229719638ebra_1: !> [TA: $tType]: $o).
% 38.74/15.80 thf(ordere890947078_space_decl, type, ordere890947078_space: !> [TA: $tType]: $o).
% 38.74/15.80 thf(condit1656338222tinuum_decl, type, condit1656338222tinuum: !> [TA: $tType]: $o).
% 38.74/15.80 thf(condit1037483654norder_decl, type, condit1037483654norder: !> [TA: $tType]: $o).
% 38.74/15.80 thf(archimedean_ceiling_decl, type, archimedean_ceiling: !> [TA: $tType]: (TA > int)).
% 38.74/15.80 thf(archim2085082626_floor_decl, type, archim2085082626_floor: !> [TA: $tType]: (TA > int)).
% 38.74/15.80 thf(finite1218308419n_axis_decl, type, finite1218308419n_axis: !> [TA: $tType,TB: $tType]: (TB > (TA > (finite_Cartesian_vec @ TA @ TB)))).
% 38.74/15.80 thf(finite1115014511_index_decl, type, finite1115014511_index: !> [TA: $tType,TB: $tType]: ((finite_Cartesian_vec @ TB @ TA) > TA)).
% 38.74/15.80 thf(finite1614961371matrix_decl, type, finite1614961371matrix: !> [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: ((TD > TC) > ((finite_Cartesian_vec @ (finite_Cartesian_vec @ TD @ TB) @ TA) > (finite_Cartesian_vec @ (finite_Cartesian_vec @ TC @ TB) @ TA)))).
% 38.74/15.80 thf(finite_Cartesian_vec2_decl, type, finite_Cartesian_vec2: !> [TA: $tType,TB: $tType]: (TB > (finite_Cartesian_vec @ TB @ TA))).
% 38.74/15.80 thf(finite1433825200ec_nth_decl, type, finite1433825200ec_nth: !> [TA: $tType,TB: $tType]: ((finite_Cartesian_vec @ TB @ TA) > (TA > TB))).
% 38.74/15.80 thf(finite431509953r_mult_decl, type, finite431509953r_mult: !> [TA: $tType,TB: $tType]: (TB > ((finite_Cartesian_vec @ TB @ TA) > (finite_Cartesian_vec @ TB @ TA)))).
% 38.74/15.80 thf(abs_abs_decl, type, abs_abs: !> [TA: $tType]: (TA > TA)).
% 38.74/15.80 thf(minus_minus_decl, type, minus_minus: !> [TA: $tType]: (TA > (TA > TA))).
% 38.74/15.80 thf(one_one_decl, type, one_one: !> [TA: $tType]: TA).
% 38.74/15.80 thf(if_decl, type, if: !> [TA: $tType]: ($o > (TA > (TA > TA)))).
% 38.74/15.80 thf(ring_1_Ints_decl, type, ring_1_Ints: !> [TA: $tType]: (set @ TA)).
% 38.74/15.80 thf(ring_1_of_int_decl, type, ring_1_of_int: !> [TA: $tType]: (int > TA)).
% 38.74/15.80 thf(minkow1937162798nt_vec_decl, type, minkow1937162798nt_vec: !> [TA: $tType,TB: $tType]: ((finite_Cartesian_vec @ int @ TB) > (finite_Cartesian_vec @ TA @ TB))).
% 38.74/15.80 thf(ord_less_decl, type, ord_less: !> [TA: $tType]: (TA > (TA > $o))).
% 38.74/15.80 thf(ord_less_eq_decl, type, ord_less_eq: !> [TA: $tType]: (TA > (TA > $o))).
% 38.74/15.80 thf(real_V2000881966t_dist_decl, type, real_V2000881966t_dist: !> [TA: $tType]: (TA > (TA > real))).
% 38.74/15.80 thf(real_V1127708846m_norm_decl, type, real_V1127708846m_norm: !> [TA: $tType]: (TA > real)).
% 38.74/15.80 thf(collect_decl, type, collect: !> [TA: $tType]: ((TA > $o) > (set @ TA))).
% 38.74/15.80 thf(member_decl, type, member: !> [TA: $tType]: (TA > ((set @ TA) > $o))).
% 38.74/15.80 thf(a_decl, type, a: (set @ (finite_Cartesian_vec @ real @ n))).
% 38.74/15.80 thf(i_decl, type, i: n).
% 38.74/15.80 thf(m_decl, type, m: int).
% 38.74/15.80 thf(x_decl, type, x: (finite_Cartesian_vec @ real @ n)).
% 38.74/15.80 thf(y_decl, type, y: (finite_Cartesian_vec @ real @ n)).
% 38.74/15.80 thf(364,axiom,((ordered_ab_group_add @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Oordered__ab__group__add)).
% 38.74/15.80 thf(1322,plain,((ordered_ab_group_add @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[364])).
% 38.74/15.80 thf(148,axiom,((zero @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Groups_Ozero_49)).
% 38.74/15.80 thf(809,plain,((zero @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[148])).
% 38.74/15.80 thf(37,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ D @ C)))) => (ord_less_eq @ TA @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_249_dense__le__bounded)).
% 38.74/15.80 thf(479,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ D @ C)))) => (ord_less_eq @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 38.74/15.80 thf(161,axiom,((! [TA: $tType]: ((real_V55928688vector @ TA) => (! [A:TA,B:TA]: ((real_V2000881966t_dist @ TA @ A @ (minus_minus @ TA @ A @ B)) = (real_V1127708846m_norm @ TA @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_64_dist__diff_I1_J)).
% 38.74/15.80 thf(846,plain,((! [TA: $tType]: ((real_V55928688vector @ TA) => (! [A:TA,B:TA]: ((real_V2000881966t_dist @ TA @ A @ (minus_minus @ TA @ A @ B)) = (real_V1127708846m_norm @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[161])).
% 38.74/15.80 thf(181,axiom,((monoid_mult @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Omonoid__mult)).
% 38.74/15.80 thf(893,plain,((monoid_mult @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[181])).
% 38.74/15.80 thf(51,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (A != B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_245_order_Ostrict__iff__order)).
% 38.74/15.80 thf(518,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[51])).
% 38.74/15.80 thf(354,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (finite_finite @ TB)) => ((ord_less_eq @ (finite_Cartesian_vec @ TA @ TB)) = (^ [A:(finite_Cartesian_vec @ TA @ TB),B:(finite_Cartesian_vec @ TA @ TB)]: ! [C:TB]: (ord_less_eq @ TA @ (finite1433825200ec_nth @ TA @ TB @ A @ C) @ (finite1433825200ec_nth @ TA @ TB @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_112_less__eq__vec__def)).
% 38.74/15.80 thf(1295,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (finite_finite @ TB)) => ((ord_less_eq @ (finite_Cartesian_vec @ TA @ TB)) = (^ [A:(finite_Cartesian_vec @ TA @ TB),B:(finite_Cartesian_vec @ TA @ TB)]: ! [C:TB]: (ord_less_eq @ TA @ (finite1433825200ec_nth @ TA @ TB @ A @ C) @ (finite1433825200ec_nth @ TA @ TB @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[354])).
% 38.74/15.80 thf(265,axiom,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA]: ((abs_abs @ TA @ (abs_abs @ TA @ A)) = (abs_abs @ TA @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_11_abs__idempotent)).
% 38.74/15.80 thf(1083,plain,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA]: ((abs_abs @ TA @ (abs_abs @ TA @ A)) = (abs_abs @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[265])).
% 38.74/15.80 thf(207,axiom,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA,B:TA]: ((abs_abs @ TA @ (minus_minus @ TA @ A @ B)) = (abs_abs @ TA @ (minus_minus @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_13_abs__minus__commute)).
% 38.74/15.80 thf(962,plain,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA,B:TA]: ((abs_abs @ TA @ (minus_minus @ TA @ A @ B)) = (abs_abs @ TA @ (minus_minus @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[207])).
% 38.74/15.80 thf(314,axiom,((preorder @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Opreorder_1)).
% 38.74/15.80 thf(1211,plain,((preorder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[314])).
% 38.74/15.80 thf(173,axiom,((linorder @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Olinorder)).
% 38.74/15.80 thf(873,plain,((linorder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[173])).
% 38.74/15.80 thf(99,axiom,((ord @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Orderings_Oord_47)).
% 38.74/15.80 thf(677,plain,((ord @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[99])).
% 38.74/15.80 thf(53,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less_eq @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_161_linorder__wlog)).
% 38.74/15.80 thf(523,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less_eq @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[53])).
% 38.74/15.80 thf(292,axiom,((! [TA: $tType]: ((real_V2090557954_space @ TA) => (! [A:TA,B:TA,C:real]: ((ord_less @ real @ (real_V2000881966t_dist @ TA @ A @ B) @ C) => (ord_less @ real @ (real_V2000881966t_dist @ TA @ B @ A) @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_75_dist__commute__lessI)).
% 38.74/15.80 thf(1158,plain,((! [TA: $tType]: ((real_V2090557954_space @ TA) => (! [A:TA,B:TA,C:real]: ((ord_less @ real @ (real_V2000881966t_dist @ TA @ A @ B) @ C) => (ord_less @ real @ (real_V2000881966t_dist @ TA @ B @ A) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[292])).
% 38.74/15.80 thf(76,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ A @ C) => (ord_less_eq @ TA @ B @ C))) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_236_dense__ge)).
% 38.74/15.80 thf(582,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ A @ C) => (ord_less_eq @ TA @ B @ C))) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[76])).
% 38.74/15.80 thf(132,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_221_leI)).
% 38.74/15.80 thf(762,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[132])).
% 38.74/15.80 thf(124,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_186_order_Ostrict__implies__not__eq)).
% 38.74/15.80 thf(741,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[124])).
% 38.74/15.80 thf(261,axiom,((! [TA: $tType,TB: $tType]: (((finite_finite @ TB) & (finite_finite @ TA)) => (finite_finite @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Finite__Set_Ofinite_62)).
% 38.74/15.80 thf(1073,plain,((! [TA: $tType,TB: $tType]: (((finite_finite @ TB) & (finite_finite @ TA)) => (finite_finite @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[261])).
% 38.74/15.80 thf(176,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((ord_less @ int @ (archim2085082626_floor @ TA @ A) @ (one_one @ int)) = (ord_less @ TA @ A @ (one_one @ TA))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_65_floor__less__one)).
% 38.74/15.80 thf(878,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((ord_less @ int @ (archim2085082626_floor @ TA @ A) @ (one_one @ int)) = (ord_less @ TA @ A @ (one_one @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[176])).
% 38.74/15.80 thf(48,axiom,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_175_eq__iff)).
% 38.74/15.80 thf(511,plain,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[48])).
% 38.74/15.80 thf(263,axiom,(((real_V2000881966t_dist @ (finite_Cartesian_vec @ real @ numeral_num1)) = (^ [A:(finite_Cartesian_vec @ real @ numeral_num1),B:(finite_Cartesian_vec @ real @ numeral_num1)]: (abs_abs @ real @ (minus_minus @ real @ (finite1433825200ec_nth @ real @ numeral_num1 @ A @ (one_one @ numeral_num1)) @ (finite1433825200ec_nth @ real @ numeral_num1 @ B @ (one_one @ numeral_num1))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_140_dist__real)).
% 38.74/15.80 thf(1078,plain,(((real_V2000881966t_dist @ (finite_Cartesian_vec @ real @ numeral_num1)) = (^ [A:(finite_Cartesian_vec @ real @ numeral_num1),B:(finite_Cartesian_vec @ real @ numeral_num1)]: (abs_abs @ real @ (minus_minus @ real @ (finite1433825200ec_nth @ real @ numeral_num1 @ A @ (one_one @ numeral_num1)) @ (finite1433825200ec_nth @ real @ numeral_num1 @ B @ (one_one @ numeral_num1))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[263])).
% 38.74/15.80 thf(11,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_218_ord__less__eq__subst)).
% 38.74/15.80 thf(384,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 38.74/15.80 thf(283,axiom,((! [TA: $tType]: ((real_V55928688vector @ TA) => (! [A:TA,B:TA]: ((real_V2000881966t_dist @ TA @ (minus_minus @ TA @ A @ B) @ A) = (real_V1127708846m_norm @ TA @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_63_dist__diff_I2_J)).
% 38.74/15.80 thf(1137,plain,((! [TA: $tType]: ((real_V55928688vector @ TA) => (! [A:TA,B:TA]: ((real_V2000881966t_dist @ TA @ (minus_minus @ TA @ A @ B) @ A) = (real_V1127708846m_norm @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[283])).
% 38.74/15.80 thf(62,axiom,((! [TA: $tType]: ((zero @ TA) => (zero @ (set @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Set_Oset___Groups_Ozero_11)).
% 38.74/15.80 thf(550,plain,((! [TA: $tType]: ((zero @ TA) => (zero @ (set @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[62])).
% 38.74/15.80 thf(44,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (one_one @ TA) @ (one_one @ TA)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_97_less__numeral__extra_I4_J)).
% 38.74/15.80 thf(500,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (~ (ord_less @ TA @ (one_one @ TA) @ (one_one @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[44])).
% 38.74/15.80 thf(111,axiom,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_214_gt__ex)).
% 38.74/15.80 thf(715,plain,((! [TA: $tType]: ((no_top @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[111])).
% 38.74/15.80 thf(345,axiom,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (abs_abs @ TA @ A) @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_123_abs__le__D1)).
% 38.74/15.80 thf(1275,plain,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ (abs_abs @ TA @ A) @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[345])).
% 38.74/15.80 thf(326,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: ((ord_less @ int @ (archim2085082626_floor @ TA @ A) @ B) = (ord_less @ TA @ A @ (ring_1_of_int @ TA @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_70_floor__less__iff)).
% 38.74/15.80 thf(1233,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: ((ord_less @ int @ (archim2085082626_floor @ TA @ A) @ B) = (ord_less @ TA @ A @ (ring_1_of_int @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[326])).
% 38.74/15.80 thf(191,axiom,((! [TA: $tType]: ((real_V55928688vector @ TA) => ((real_V2000881966t_dist @ (finite_Cartesian_vec @ TA @ numeral_num1)) = (^ [A:(finite_Cartesian_vec @ TA @ numeral_num1),B:(finite_Cartesian_vec @ TA @ numeral_num1)]: (real_V2000881966t_dist @ TA @ (finite1433825200ec_nth @ TA @ numeral_num1 @ A @ (one_one @ numeral_num1)) @ (finite1433825200ec_nth @ TA @ numeral_num1 @ B @ (one_one @ numeral_num1)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_126_dist__vector__1)).
% 38.74/15.80 thf(913,plain,((! [TA: $tType]: ((real_V55928688vector @ TA) => ((real_V2000881966t_dist @ (finite_Cartesian_vec @ TA @ numeral_num1)) = (^ [A:(finite_Cartesian_vec @ TA @ numeral_num1),B:(finite_Cartesian_vec @ TA @ numeral_num1)]: (real_V2000881966t_dist @ TA @ (finite1433825200ec_nth @ TA @ numeral_num1 @ A @ (one_one @ numeral_num1)) @ (finite1433825200ec_nth @ TA @ numeral_num1 @ B @ (one_one @ numeral_num1)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[191])).
% 38.74/15.80 thf(257,axiom,((! [TA: $tType]: ((real_V55928688vector @ TA) => (! [A:TA,B:TA]: (ord_less_eq @ real @ (abs_abs @ real @ (minus_minus @ real @ (real_V1127708846m_norm @ TA @ A) @ (real_V1127708846m_norm @ TA @ B))) @ (real_V1127708846m_norm @ TA @ (minus_minus @ TA @ A @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_147_norm__triangle__ineq3)).
% 38.74/15.80 thf(1063,plain,((! [TA: $tType]: ((real_V55928688vector @ TA) => (! [A:TA,B:TA]: (ord_less_eq @ real @ (abs_abs @ real @ (minus_minus @ real @ (real_V1127708846m_norm @ TA @ A) @ (real_V1127708846m_norm @ TA @ B))) @ (real_V1127708846m_norm @ TA @ (minus_minus @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[257])).
% 38.74/15.80 thf(321,axiom,((! [TA: $tType,TB: $tType]: (((real_V55928688vector @ TB) & (finite_finite @ TA)) => (real_V1639655670t_norm @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Real__Vector__Spaces_Odist__norm_57)).
% 38.74/15.80 thf(1222,plain,((! [TA: $tType,TB: $tType]: (((real_V55928688vector @ TB) & (finite_finite @ TA)) => (real_V1639655670t_norm @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[321])).
% 38.74/15.80 thf(295,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:TA]: ((member @ TA @ A @ (ring_1_Ints @ TA)) => (member @ TA @ (abs_abs @ TA @ A) @ (ring_1_Ints @ TA))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_19_Ints__abs)).
% 38.74/15.80 thf(1164,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:TA]: ((member @ TA @ A @ (ring_1_Ints @ TA)) => (member @ TA @ (abs_abs @ TA @ A) @ (ring_1_Ints @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[295])).
% 38.74/15.80 thf(144,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_217_order__less__subst1)).
% 38.74/15.80 thf(797,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[144])).
% 38.74/15.80 thf(224,axiom,((! [TA: $tType]: ((real_V1229719638ebra_1 @ TA) => (! [A:int,B:int]: ((real_V2000881966t_dist @ TA @ (ring_1_of_int @ TA @ A) @ (ring_1_of_int @ TA @ B)) = (ring_1_of_int @ real @ (abs_abs @ int @ (minus_minus @ int @ A @ B)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_29_dist__of__int)).
% 38.74/15.80 thf(1001,plain,((! [TA: $tType]: ((real_V1229719638ebra_1 @ TA) => (! [A:int,B:int]: ((real_V2000881966t_dist @ TA @ (ring_1_of_int @ TA @ A) @ (ring_1_of_int @ TA @ B)) = (ring_1_of_int @ real @ (abs_abs @ int @ (minus_minus @ int @ A @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[224])).
% 38.74/15.80 thf(108,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_211_order_Oasym)).
% 38.74/15.80 thf(709,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[108])).
% 38.74/15.80 thf(324,axiom,((! [TA: $tType]: ((real_V2090557954_space @ TA) => (! [A:TA,B:TA,C:TA]: (ord_less_eq @ real @ (abs_abs @ real @ (minus_minus @ real @ (real_V2000881966t_dist @ TA @ A @ B) @ (real_V2000881966t_dist @ TA @ B @ C))) @ (real_V2000881966t_dist @ TA @ A @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_144_abs__dist__diff__le)).
% 38.74/15.80 thf(1228,plain,((! [TA: $tType]: ((real_V2090557954_space @ TA) => (! [A:TA,B:TA,C:TA]: (ord_less_eq @ real @ (abs_abs @ real @ (minus_minus @ real @ (real_V2000881966t_dist @ TA @ A @ B) @ (real_V2000881966t_dist @ TA @ B @ C))) @ (real_V2000881966t_dist @ TA @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[324])).
% 38.74/15.80 thf(331,axiom,((! [TA: $tType]: ((finite_finite @ TA) => (! [A:(finite_Cartesian_vec @ real @ TA),B:real,C:TA]: ((ord_less_eq @ real @ (real_V1127708846m_norm @ (finite_Cartesian_vec @ real @ TA) @ A) @ B) => (ord_less_eq @ real @ (abs_abs @ real @ (finite1433825200ec_nth @ real @ TA @ A @ C)) @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_138_norm__bound__component__le__cart)).
% 38.74/15.80 thf(1243,plain,((! [TA: $tType]: ((finite_finite @ TA) => (! [A:(finite_Cartesian_vec @ real @ TA),B:real,C:TA]: ((ord_less_eq @ real @ (real_V1127708846m_norm @ (finite_Cartesian_vec @ real @ TA) @ A) @ B) => (ord_less_eq @ real @ (abs_abs @ real @ (finite1433825200ec_nth @ real @ TA @ A @ C)) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[331])).
% 38.74/15.80 thf(279,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: ((ord_less @ int @ (archimedean_ceiling @ TA @ A) @ B) = (ord_less_eq @ TA @ A @ (minus_minus @ TA @ (ring_1_of_int @ TA @ B) @ (one_one @ TA)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_129_ceiling__less__iff)).
% 38.74/15.80 thf(1127,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: ((ord_less @ int @ (archimedean_ceiling @ TA @ A) @ B) = (ord_less_eq @ TA @ A @ (minus_minus @ TA @ (ring_1_of_int @ TA @ B) @ (one_one @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[279])).
% 38.74/15.80 thf(350,axiom,(((real_V2000881966t_dist @ real) = (^ [A:real,B:real]: (abs_abs @ real @ (minus_minus @ real @ A @ B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_89_dist__real__def)).
% 38.74/15.80 thf(1287,plain,(((real_V2000881966t_dist @ real) = (^ [A:real,B:real]: (abs_abs @ real @ (minus_minus @ real @ A @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[350])).
% 38.74/15.80 thf(70,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_235_less__le__trans)).
% 38.74/15.80 thf(570,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[70])).
% 38.74/15.80 thf(355,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (ring_1_of_int @ TA @ (archim2085082626_floor @ TA @ A)) @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_136_of__int__floor__le)).
% 38.74/15.80 thf(1298,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (ring_1_of_int @ TA @ (archim2085082626_floor @ TA @ A)) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[355])).
% 38.74/15.80 thf(5,axiom,((! [TA: $tType]: ((finite_finite @ TA) => (finite_finite @ (set @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Set_Oset___Finite__Set_Ofinite_7)).
% 38.74/15.80 thf(372,plain,((! [TA: $tType]: ((finite_finite @ TA) => (finite_finite @ (set @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 38.74/15.80 thf(340,axiom,((! [A:real]: (ord_less @ real @ (minus_minus @ real @ A @ (one_one @ real)) @ (ring_1_of_int @ real @ (archim2085082626_floor @ real @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_95_real__of__int__floor__gt__diff__one)).
% 38.74/15.80 thf(1264,plain,((! [A:real]: (ord_less @ real @ (minus_minus @ real @ A @ (one_one @ real)) @ (ring_1_of_int @ real @ (archim2085082626_floor @ real @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[340])).
% 38.74/15.80 thf(127,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((ord_less_eq @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB)]: ! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_180_le__fun__def)).
% 38.74/15.80 thf(751,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => ((ord_less_eq @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB)]: ! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[127])).
% 38.74/15.80 thf(251,axiom,((ring @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Oring)).
% 38.74/15.80 thf(1055,plain,((ring @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[251])).
% 38.74/15.80 thf(116,axiom,((linorder @ $o)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Olinorder_14)).
% 38.74/15.80 thf(724,plain,((linorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[116])).
% 38.74/15.80 thf(365,axiom,((no_top @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Ono__top)).
% 38.74/15.80 thf(1323,plain,((no_top @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[365])).
% 38.74/15.80 thf(88,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_185_dual__order_Ostrict__implies__not__eq)).
% 38.74/15.80 thf(619,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[88])).
% 38.74/15.80 thf(254,axiom,((! [TA: $tType,TB: $tType]: (((one @ TB) & (finite_finite @ TA)) => (one @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Groups_Oone_71)).
% 38.74/15.80 thf(1059,plain,((! [TA: $tType,TB: $tType]: (((one @ TB) & (finite_finite @ TA)) => (one @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[254])).
% 38.74/15.80 thf(281,axiom,((! [TA: $tType,TB: $tType]: (((ring_char_0 @ TB) & (finite_finite @ TA)) => (ring_char_0 @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Nat_Oring__char__0_65)).
% 38.74/15.80 thf(1132,plain,((! [TA: $tType,TB: $tType]: (((ring_char_0 @ TB) & (finite_finite @ TA)) => (ring_char_0 @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[281])).
% 38.74/15.80 thf(65,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (A != B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_223_less__le)).
% 38.74/15.80 thf(559,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[65])).
% 38.74/15.80 thf(333,axiom,((member @ real @ (minus_minus @ real @ (finite1433825200ec_nth @ real @ n @ x @ i) @ (finite1433825200ec_nth @ real @ n @ y @ i)) @ (ring_1_Ints @ real))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_7__092_060open_062x_A_E_Ai_A_N_Ay_A_E_Ai_A_092_060in_062_A_092_060int_062_092_060close_062)).
% 38.74/15.80 thf(1247,plain,((member @ real @ (minus_minus @ real @ (finite1433825200ec_nth @ real @ n @ x @ i) @ (finite1433825200ec_nth @ real @ n @ y @ i)) @ (ring_1_Ints @ real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[333])).
% 38.74/15.80 thf(361,axiom,((real_V2090557954_space @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Real__Vector__Spaces_Ometric__space)).
% 38.74/15.80 thf(1319,plain,((real_V2090557954_space @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[361])).
% 38.74/15.80 thf(230,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((ord_less @ int @ (one_one @ int) @ (archimedean_ceiling @ TA @ A)) = (ord_less @ TA @ (one_one @ TA) @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_66_one__less__ceiling)).
% 38.74/15.80 thf(1013,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((ord_less @ int @ (one_one @ int) @ (archimedean_ceiling @ TA @ A)) = (ord_less @ TA @ (one_one @ TA) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[230])).
% 38.74/15.80 thf(28,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((A != B) => ((ord_less_eq @ TA @ A @ B) => (ord_less @ TA @ A @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_153_order_Onot__eq__order__implies__strict)).
% 38.74/15.80 thf(448,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) => ((ord_less_eq @ TA @ A @ B) => (ord_less @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 38.74/15.80 thf(177,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int,B:int]: ((ord_less_eq @ TA @ (ring_1_of_int @ TA @ A) @ (ring_1_of_int @ TA @ B)) = (ord_less_eq @ int @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_102_of__int__le__iff)).
% 38.74/15.80 thf(881,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int,B:int]: ((ord_less_eq @ TA @ (ring_1_of_int @ TA @ A) @ (ring_1_of_int @ TA @ B)) = (ord_less_eq @ int @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[177])).
% 38.74/15.80 thf(22,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_243_order_Ostrict__trans2)).
% 38.74/15.80 thf(416,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 38.74/15.80 thf(243,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (ord_less_eq @ int @ (archim2085082626_floor @ TA @ A) @ (archimedean_ceiling @ TA @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_141_floor__le__ceiling)).
% 38.74/15.80 thf(1040,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (ord_less_eq @ int @ (archim2085082626_floor @ TA @ A) @ (archimedean_ceiling @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[243])).
% 38.74/15.80 thf(7,axiom,((! [TA: $tType]: (ord @ (set @ TA)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oord_9)).
% 38.74/15.80 thf(376,plain,((! [TA: $tType]: (ord @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 38.74/15.80 thf(89,axiom,((! [TA: $tType]: (minus @ (set @ TA)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Set_Oset___Groups_Ominus_10)).
% 38.74/15.80 thf(623,plain,((! [TA: $tType]: (minus @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[89])).
% 38.74/15.80 thf(97,axiom,((! [TA: $tType]: ((condit1037483654norder @ TA) => (! [A:TA,B:TA,C:(TA > $o)]: ((ord_less @ TA @ A @ B) => ((C @ A) => ((~ (C @ B)) => (? [D:TA]: ((ord_less_eq @ TA @ A @ D) & (ord_less_eq @ TA @ D @ B) & ! [E:TA]: (((ord_less_eq @ TA @ A @ E) & (ord_less @ TA @ E @ D)) => (C @ E)) & ! [E:TA]: ((! [F:TA]: (((ord_less_eq @ TA @ A @ F) & (ord_less @ TA @ F @ E)) => (C @ F))) => (ord_less_eq @ TA @ E @ D))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_151_complete__interval)).
% 38.74/15.80 thf(646,plain,((! [TA: $tType]: ((condit1037483654norder @ TA) => (! [A:TA,B:TA,C:(TA > $o)]: ((ord_less @ TA @ A @ B) => ((C @ A) => ((~ (C @ B)) => (? [D:TA]: ((ord_less_eq @ TA @ A @ D) & (ord_less_eq @ TA @ D @ B) & ! [E:TA]: (((ord_less_eq @ TA @ A @ E) & (ord_less @ TA @ E @ D)) => (C @ E)) & ! [E:TA]: ((! [F:TA]: (((ord_less_eq @ TA @ A @ F) & (ord_less @ TA @ F @ E)) => (C @ F))) => (ord_less_eq @ TA @ E @ D))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[97])).
% 38.74/15.80 thf(156,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_If_2_1_T)).
% 38.74/15.80 thf(834,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($false) @ A @ B) = B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[156])).
% 38.74/15.80 thf(49,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TA) => (minus @ (TB > TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_fun___Groups_Ominus)).
% 38.74/15.80 thf(514,plain,((! [TA: $tType,TB: $tType]: ((minus @ TA) => (minus @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[49])).
% 38.74/15.80 thf(289,axiom,((! [TA: $tType,TB: $tType]: (((zero @ TA) & (finite_finite @ TB)) => (! [A:TB,B:TA]: ((finite1433825200ec_nth @ TA @ TB @ (finite1218308419n_axis @ TB @ TA @ A @ B) @ A) = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_35_axis__nth)).
% 38.74/15.80 thf(1151,plain,((! [TA: $tType,TB: $tType]: (((zero @ TA) & (finite_finite @ TB)) => (! [A:TB,B:TA]: ((finite1433825200ec_nth @ TA @ TB @ (finite1218308419n_axis @ TB @ TA @ A @ B) @ A) = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[289])).
% 38.74/15.80 thf(348,axiom,((linord1659791738miring @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Olinordered__nonzero__semiring)).
% 38.74/15.80 thf(1283,plain,((linord1659791738miring @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[348])).
% 38.74/15.80 thf(357,axiom,((! [TA: $tType,TB: $tType]: (((order @ TB) & (finite_finite @ TA)) => (preorder @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Orderings_Opreorder_59)).
% 38.74/15.80 thf(1302,plain,((! [TA: $tType,TB: $tType]: (((order @ TB) & (finite_finite @ TA)) => (preorder @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[357])).
% 38.74/15.80 thf(129,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_241_not__le__imp__less)).
% 38.74/15.80 thf(756,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[129])).
% 38.74/15.80 thf(233,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (ord_less_eq @ int @ (minus_minus @ int @ (archimedean_ceiling @ TA @ A) @ (archim2085082626_floor @ TA @ A)) @ (one_one @ int)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_128_ceiling__diff__floor__le__1)).
% 38.74/15.80 thf(1020,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (ord_less_eq @ int @ (minus_minus @ int @ (archimedean_ceiling @ TA @ A) @ (archim2085082626_floor @ TA @ A)) @ (one_one @ int)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[233])).
% 38.74/15.80 thf(73,axiom,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ B)) = (B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_44_mem__Collect__eq)).
% 38.74/15.80 thf(574,plain,((! [TA: $tType]: (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (collect @ TA @ (B))) = (B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[73])).
% 38.74/15.80 thf(248,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: ((ord_less_eq @ TA @ A @ (ring_1_of_int @ TA @ B)) => (ord_less_eq @ int @ (archimedean_ceiling @ TA @ A) @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_115_ceiling__le)).
% 38.74/15.80 thf(1051,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: ((ord_less_eq @ TA @ A @ (ring_1_of_int @ TA @ B)) => (ord_less_eq @ int @ (archimedean_ceiling @ TA @ A) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[248])).
% 38.74/15.80 thf(152,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_207_less__asym_H)).
% 38.74/15.80 thf(821,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[152])).
% 38.74/15.80 thf(297,axiom,((! [TA: $tType]: ((ring_1 @ TA) => (! [A:TA,B:TA]: ((member @ TA @ A @ (ring_1_Ints @ TA)) => ((member @ TA @ B @ (ring_1_Ints @ TA)) => (member @ TA @ (minus_minus @ TA @ A @ B) @ (ring_1_Ints @ TA)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_18_Ints__diff)).
% 38.74/15.80 thf(1169,plain,((! [TA: $tType]: ((ring_1 @ TA) => (! [A:TA,B:TA]: ((member @ TA @ A @ (ring_1_Ints @ TA)) => ((member @ TA @ B @ (ring_1_Ints @ TA)) => (member @ TA @ (minus_minus @ TA @ A @ B) @ (ring_1_Ints @ TA)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[297])).
% 38.74/15.80 thf(95,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_177_ord__eq__le__subst)).
% 38.74/15.80 thf(634,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[95])).
% 38.74/15.80 thf(175,axiom,((ring_char_0 @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Nat_Oring__char__0)).
% 38.74/15.80 thf(877,plain,((ring_char_0 @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[175])).
% 38.74/15.80 thf(204,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (((ring_1_of_int @ TA @ (archim2085082626_floor @ TA @ A)) = A) = (? [B:int]: (A = (ring_1_of_int @ TA @ B)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_94_of__int__floor__cancel)).
% 38.74/15.80 thf(956,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (((ring_1_of_int @ TA @ (archim2085082626_floor @ TA @ A)) = A) = (? [B:int]: (A = (ring_1_of_int @ TA @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[204])).
% 38.74/15.80 thf(170,axiom,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((A = B) = (C = D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_24_diff__eq__diff__eq)).
% 38.74/15.80 thf(866,plain,((! [TA: $tType]: ((group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((A = B) = (C = D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[170])).
% 38.74/15.80 thf(136,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_192_order_Ostrict__trans)).
% 38.74/15.80 thf(774,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[136])).
% 38.74/15.80 thf(309,axiom,((! [A:real]: (ord_less_eq @ real @ (minus_minus @ real @ A @ (one_one @ real)) @ (ring_1_of_int @ real @ (archim2085082626_floor @ real @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_135_real__of__int__floor__ge__diff__one)).
% 38.74/15.80 thf(1201,plain,((! [A:real]: (ord_less_eq @ real @ (minus_minus @ real @ A @ (one_one @ real)) @ (ring_1_of_int @ real @ (archim2085082626_floor @ real @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[309])).
% 38.74/15.80 thf(47,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_224_order__le__less__subst1)).
% 38.74/15.80 thf(507,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[47])).
% 38.74/15.80 thf(84,axiom,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_If_1_1_T)).
% 38.74/15.80 thf(602,plain,((! [TA: $tType]: (! [A:TA,B:TA]: ((if @ TA @ ($true) @ A @ B) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[84])).
% 38.74/15.80 thf(216,axiom,((! [TA: $tType,TB: $tType]: ((finite_finite @ TB) => (! [A:(finite_Cartesian_vec @ TA @ TB),B:(finite_Cartesian_vec @ TA @ TB)]: (((finite1433825200ec_nth @ TA @ TB @ A) = (finite1433825200ec_nth @ TA @ TB @ B)) = (A = B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_26_vec__nth__inject)).
% 38.74/15.80 thf(981,plain,((! [TA: $tType,TB: $tType]: ((finite_finite @ TB) => (! [A:(finite_Cartesian_vec @ TA @ TB),B:(finite_Cartesian_vec @ TA @ TB)]: (((finite1433825200ec_nth @ TA @ TB @ A) = (finite1433825200ec_nth @ TA @ TB @ B)) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[216])).
% 38.74/15.80 thf(20,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_250_order_Ostrict__implies__order)).
% 38.74/15.80 thf(411,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 38.74/15.80 thf(219,axiom,((ring_char_0 @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Nat_Oring__char__0_33)).
% 38.74/15.80 thf(988,plain,((ring_char_0 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[219])).
% 38.74/15.80 thf(330,axiom,((real_V1229719638ebra_1 @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Real__Vector__Spaces_Oreal__normed__algebra__1)).
% 38.74/15.80 thf(1242,plain,((real_V1229719638ebra_1 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[330])).
% 38.74/15.80 thf(162,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:TA]: ((ord_less @ int @ (archimedean_ceiling @ TA @ A) @ (archimedean_ceiling @ TA @ B)) => (ord_less @ TA @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_77_ceiling__less__cancel)).
% 38.74/15.80 thf(849,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:TA]: ((ord_less @ int @ (archimedean_ceiling @ TA @ A) @ (archimedean_ceiling @ TA @ B)) => (ord_less @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[162])).
% 38.74/15.80 thf(311,axiom,((! [TA: $tType,TB: $tType]: (((cancel146912293up_add @ TB) & (finite_finite @ TA)) => (cancel146912293up_add @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Groups_Ocancel__ab__semigroup__add_56)).
% 38.74/15.80 thf(1206,plain,((! [TA: $tType,TB: $tType]: (((cancel146912293up_add @ TB) & (finite_finite @ TA)) => (cancel146912293up_add @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[311])).
% 38.74/15.80 thf(9,axiom,((finite_finite @ $o)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_HOL_Obool___Finite__Set_Ofinite_15)).
% 38.74/15.80 thf(380,plain,((finite_finite @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 38.74/15.80 thf(197,axiom,((ordere890947078_space @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Ordered__Euclidean__Space_Oordered__euclidean__space)).
% 38.74/15.80 thf(942,plain,((ordere890947078_space @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[197])).
% 38.74/15.80 thf(100,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:$o]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ A) => (C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_195_less__imp__triv)).
% 38.74/15.80 thf(678,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:$o]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ A) => (C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[100])).
% 38.74/15.80 thf(54,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_150_order__refl)).
% 38.74/15.80 thf(529,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[54])).
% 38.74/15.80 thf(143,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_200_less__imp__not__eq)).
% 38.74/15.80 thf(793,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[143])).
% 38.74/15.80 thf(359,axiom,((! [TA: $tType,TB: $tType]: (((one @ TA) & (finite_finite @ TB)) => (! [A:TB]: ((finite1433825200ec_nth @ TA @ TB @ (one_one @ (finite_Cartesian_vec @ TA @ TB)) @ A) = (one_one @ TA)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_49_one__index)).
% 38.74/15.80 thf(1306,plain,((! [TA: $tType,TB: $tType]: (((one @ TA) & (finite_finite @ TB)) => (! [A:TB]: ((finite1433825200ec_nth @ TA @ TB @ (one_one @ (finite_Cartesian_vec @ TA @ TB)) @ A) = (one_one @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[359])).
% 38.74/15.80 thf(131,axiom,((cancel146912293up_add @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Groups_Ocancel__ab__semigroup__add_40)).
% 38.74/15.80 thf(761,plain,((cancel146912293up_add @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[131])).
% 38.74/15.80 thf(149,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (B = A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_158_dual__order_Oantisym)).
% 38.74/15.80 thf(810,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[149])).
% 38.74/15.80 thf(10,axiom,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((collect @ TA @ A) = (collect @ TA @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_46_Collect__cong)).
% 38.74/15.80 thf(381,plain,((! [TA: $tType]: (! [A:(TA > $o),B:(TA > $o)]: ((! [C:TA]: ((A @ C) = (B @ C))) => ((collect @ TA @ (A)) = (collect @ TA @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 38.74/15.80 thf(253,axiom,(((real_V1127708846m_norm @ (finite_Cartesian_vec @ real @ numeral_num1)) = (^ [A:(finite_Cartesian_vec @ real @ numeral_num1)]: (abs_abs @ real @ (finite1433825200ec_nth @ real @ numeral_num1 @ A @ (one_one @ numeral_num1)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_127_norm__real)).
% 38.74/15.80 thf(1057,plain,(((real_V1127708846m_norm @ (finite_Cartesian_vec @ real @ numeral_num1)) = (^ [A:(finite_Cartesian_vec @ real @ numeral_num1)]: (abs_abs @ real @ (finite1433825200ec_nth @ real @ numeral_num1 @ A @ (one_one @ numeral_num1)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[253])).
% 38.74/15.80 thf(294,axiom,((monoid_mult @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Omonoid__mult_28)).
% 38.74/15.80 thf(1163,plain,((monoid_mult @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[294])).
% 38.74/15.80 thf(344,axiom,((ring_1 @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Oring__1)).
% 38.74/15.80 thf(1274,plain,((ring_1 @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[344])).
% 38.74/15.80 thf(190,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int]: ((ring_1_of_int @ TA @ (abs_abs @ int @ A)) = (abs_abs @ TA @ (ring_1_of_int @ TA @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_of__int__abs)).
% 38.74/15.80 thf(910,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int]: ((ring_1_of_int @ TA @ (abs_abs @ int @ A)) = (abs_abs @ TA @ (ring_1_of_int @ TA @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[190])).
% 38.74/15.80 thf(182,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int]: ((ord_less @ TA @ (ring_1_of_int @ TA @ A) @ (one_one @ TA)) = (ord_less @ int @ A @ (one_one @ int))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_61_of__int__less__1__iff)).
% 38.74/15.80 thf(894,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int]: ((ord_less @ TA @ (ring_1_of_int @ TA @ A) @ (one_one @ TA)) = (ord_less @ int @ A @ (one_one @ int))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[182])).
% 38.74/15.80 thf(268,axiom,((! [TA: $tType,TB: $tType,TC: $tType]: (((real_V55928688vector @ TA) & (finite_finite @ TB) & (real_V55928688vector @ TC)) => (! [A:(finite_Cartesian_vec @ TC @ TB),B:(finite_Cartesian_vec @ TA @ TB)]: ((! [C:TB]: (ord_less_eq @ real @ (real_V1127708846m_norm @ TC @ (finite1433825200ec_nth @ TC @ TB @ A @ C)) @ (real_V1127708846m_norm @ TA @ (finite1433825200ec_nth @ TA @ TB @ B @ C)))) => (ord_less_eq @ real @ (real_V1127708846m_norm @ (finite_Cartesian_vec @ TC @ TB) @ A) @ (real_V1127708846m_norm @ (finite_Cartesian_vec @ TA @ TB) @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_133_norm__le__componentwise__cart)).
% 38.74/15.80 thf(1091,plain,((! [TA: $tType,TB: $tType,TC: $tType]: (((real_V55928688vector @ TA) & (finite_finite @ TB) & (real_V55928688vector @ TC)) => (! [A:(finite_Cartesian_vec @ TC @ TB),B:(finite_Cartesian_vec @ TA @ TB)]: ((! [C:TB]: (ord_less_eq @ real @ (real_V1127708846m_norm @ TC @ (finite1433825200ec_nth @ TC @ TB @ A @ C)) @ (real_V1127708846m_norm @ TA @ (finite1433825200ec_nth @ TA @ TB @ B @ C)))) => (ord_less_eq @ real @ (real_V1127708846m_norm @ (finite_Cartesian_vec @ TC @ TB) @ A) @ (real_V1127708846m_norm @ (finite_Cartesian_vec @ TA @ TB) @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[268])).
% 38.74/15.80 thf(277,axiom,((! [TA: $tType]: ((finite_finite @ TA) => (! [A:(finite_Cartesian_vec @ real @ TA),B:real,C:TA]: ((ord_less @ real @ (real_V1127708846m_norm @ (finite_Cartesian_vec @ real @ TA) @ A) @ B) => (ord_less @ real @ (abs_abs @ real @ (finite1433825200ec_nth @ real @ TA @ A @ C)) @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_83_norm__bound__component__lt__cart)).
% 38.74/15.80 thf(1123,plain,((! [TA: $tType]: ((finite_finite @ TA) => (! [A:(finite_Cartesian_vec @ real @ TA),B:real,C:TA]: ((ord_less @ real @ (real_V1127708846m_norm @ (finite_Cartesian_vec @ real @ TA) @ A) @ B) => (ord_less @ real @ (abs_abs @ real @ (finite1433825200ec_nth @ real @ TA @ A @ C)) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[277])).
% 38.74/15.80 thf(12,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:TA,B:TA]: ((A != B) => ((~ (ord_less @ TA @ A @ B)) => (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_74_linorder__neqE__linordered__idom)).
% 38.74/15.80 thf(392,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) => ((~ (ord_less @ TA @ A @ B)) => (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 38.74/15.80 thf(25,axiom,((! [TA: $tType,TB: $tType]: (((finite_finite @ TA) & (ring_char_0 @ TB)) => (! [A:(finite_Cartesian_vec @ int @ TA),B:(finite_Cartesian_vec @ int @ TA)]: (((minkow1937162798nt_vec @ TA @ TB @ A) = (minkow1937162798nt_vec @ TA @ TB @ B)) = (A = B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_17_of__int__vec__eq__iff)).
% 38.74/15.80 thf(424,plain,((! [TA: $tType,TB: $tType]: (((finite_finite @ TA) & (ring_char_0 @ TB)) => (! [A:(finite_Cartesian_vec @ int @ TA),B:(finite_Cartesian_vec @ int @ TA)]: (((minkow1937162798nt_vec @ TA @ TB @ A) = (minkow1937162798nt_vec @ TA @ TB @ B)) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 38.74/15.80 thf(119,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_233_less__imp__le)).
% 38.74/15.80 thf(729,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[119])).
% 38.74/15.80 thf(328,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => ((archim2085082626_floor @ TA @ (one_one @ TA)) = (one_one @ int))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_53_floor__one)).
% 38.74/15.80 thf(1238,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => ((archim2085082626_floor @ TA @ (one_one @ TA)) = (one_one @ int))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[328])).
% 38.74/15.80 thf(244,axiom,((one @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oone_39)).
% 38.74/15.80 thf(1042,plain,((one @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[244])).
% 38.74/15.80 thf(202,axiom,((order @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Oorder_32)).
% 38.74/15.80 thf(952,plain,((order @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[202])).
% 38.74/15.80 thf(319,axiom,((! [TA: $tType,TB: $tType]: (((linorder @ TB) & (cARD_1 @ TA)) => (linorder @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Orderings_Olinorder_60)).
% 38.74/15.80 thf(1217,plain,((! [TA: $tType,TB: $tType]: (((linorder @ TB) & (cARD_1 @ TA)) => (linorder @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[319])).
% 38.74/15.80 thf(82,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_199_less__not__sym)).
% 38.74/15.80 thf(598,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[82])).
% 38.74/15.80 thf(240,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((archim2085082626_floor @ TA @ (minus_minus @ TA @ A @ (one_one @ TA))) = (minus_minus @ int @ (archim2085082626_floor @ TA @ A) @ (one_one @ int))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_67_floor__diff__one)).
% 38.74/15.80 thf(1032,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((archim2085082626_floor @ TA @ (minus_minus @ TA @ A @ (one_one @ TA))) = (minus_minus @ int @ (archim2085082626_floor @ TA @ A) @ (one_one @ int))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[240])).
% 38.74/15.80 thf(90,axiom,((wellorder @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Orderings_Owellorder)).
% 38.74/15.80 thf(625,plain,((wellorder @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[90])).
% 38.74/15.80 thf(164,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:int,B:TA]: ((ord_less_eq @ int @ A @ (archim2085082626_floor @ TA @ B)) = (ord_less_eq @ TA @ (ring_1_of_int @ TA @ A) @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_116_le__floor__iff)).
% 38.74/15.80 thf(852,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:int,B:TA]: ((ord_less_eq @ int @ A @ (archim2085082626_floor @ TA @ B)) = (ord_less_eq @ TA @ (ring_1_of_int @ TA @ A) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[164])).
% 38.74/15.80 thf(300,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:int,B:TA]: ((ord_less_eq @ int @ A @ (archimedean_ceiling @ TA @ B)) = (ord_less @ TA @ (minus_minus @ TA @ (ring_1_of_int @ TA @ A) @ (one_one @ TA)) @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_99_le__ceiling__iff)).
% 38.74/15.80 thf(1178,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:int,B:TA]: ((ord_less_eq @ int @ A @ (archimedean_ceiling @ TA @ B)) = (ord_less @ TA @ (minus_minus @ TA @ (ring_1_of_int @ TA @ A) @ (one_one @ TA)) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[300])).
% 38.74/15.80 thf(32,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_208_less__asym)).
% 38.74/15.80 thf(461,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 38.74/15.80 thf(313,axiom,((ordered_ab_group_add @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oordered__ab__group__add_23)).
% 38.74/15.80 thf(1210,plain,((ordered_ab_group_add @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[313])).
% 38.74/15.80 thf(238,axiom,(((ring_1_of_int @ real @ m) = (minus_minus @ real @ (finite1433825200ec_nth @ real @ n @ x @ i) @ (finite1433825200ec_nth @ real @ n @ y @ i)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_m)).
% 38.74/15.80 thf(1027,plain,(((ring_1_of_int @ real @ m) = (minus_minus @ real @ (finite1433825200ec_nth @ real @ n @ x @ i) @ (finite1433825200ec_nth @ real @ n @ y @ i)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[238])).
% 38.74/15.80 thf(352,axiom,((! [TA: $tType,TB: $tType]: (((real_V2090557954_space @ TB) & (finite_finite @ TA)) => (real_V2090557954_space @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Real__Vector__Spaces_Ometric__space_54)).
% 38.74/15.80 thf(1291,plain,((! [TA: $tType,TB: $tType]: (((real_V2090557954_space @ TB) & (finite_finite @ TA)) => (real_V2090557954_space @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[352])).
% 38.74/15.80 thf(159,axiom,((! [TA: $tType]: ((idom_abs_sgn @ TA) => ((abs_abs @ TA @ (one_one @ TA)) = (one_one @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_43_abs__1)).
% 38.74/15.80 thf(842,plain,((! [TA: $tType]: ((idom_abs_sgn @ TA) => ((abs_abs @ TA @ (one_one @ TA)) = (one_one @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[159])).
% 38.74/15.80 thf(213,axiom,((ordere142940540dd_abs @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Oordered__ab__group__add__abs_21)).
% 38.74/15.80 thf(974,plain,((ordere142940540dd_abs @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[213])).
% 38.74/15.80 thf(229,axiom,((archim1727834104eiling @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Archimedean__Field_Ofloor__ceiling)).
% 38.74/15.80 thf(1012,plain,((archim1727834104eiling @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[229])).
% 38.74/15.80 thf(192,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/sandbox2/benchmark/theBenchmark.p',fact_113_int__less__induct)).
% 38.74/15.80 thf(916,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)],[192])).
% 38.74/15.80 thf(35,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_225_order__le__less__subst2)).
% 38.74/15.80 thf(467,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 38.74/15.80 thf(68,axiom,((! [TA: $tType]: ((ring_1 @ TA) => (member @ TA @ (one_one @ TA) @ (ring_1_Ints @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_90_Ints__1)).
% 38.74/15.80 thf(566,plain,((! [TA: $tType]: ((ring_1 @ TA) => (member @ TA @ (one_one @ TA) @ (ring_1_Ints @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[68])).
% 38.74/15.80 thf(38,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_204_less__irrefl)).
% 38.74/15.80 thf(484,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 38.74/15.80 thf(102,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B) | (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_205_less__linear)).
% 38.74/15.80 thf(682,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B) | (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[102])).
% 38.74/15.80 thf(307,axiom,((! [TA: $tType,TB: $tType]: ((finite_finite @ TB) => (! [A:(TB > (TA > $o))]: ((! [B:TB]: ? [C:TA]: (A @ B @ C)) = (? [B:(finite_Cartesian_vec @ TA @ TB)]: ! [C:TB]: (A @ C @ (finite1433825200ec_nth @ TA @ TB @ B @ C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_14_lambda__skolem)).
% 38.74/15.80 thf(1195,plain,((! [TA: $tType,TB: $tType]: ((finite_finite @ TB) => (! [A:(TB > (TA > $o))]: ((! [B:TB]: ? [C:TA]: (A @ B @ C)) = (? [B:(finite_Cartesian_vec @ TA @ TB)]: ! [C:TB]: (A @ C @ (finite1433825200ec_nth @ TA @ TB @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[307])).
% 38.74/15.80 thf(267,axiom,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA,B:TA]: (ord_less_eq @ TA @ (minus_minus @ TA @ (abs_abs @ TA @ A) @ (abs_abs @ TA @ B)) @ (abs_abs @ TA @ (minus_minus @ TA @ A @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_132_abs__triangle__ineq2)).
% 38.74/15.80 thf(1089,plain,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA,B:TA]: (ord_less_eq @ TA @ (minus_minus @ TA @ (abs_abs @ TA @ A) @ (abs_abs @ TA @ B)) @ (abs_abs @ TA @ (minus_minus @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[267])).
% 38.74/15.80 thf(174,axiom,((! [TA: $tType,TB: $tType]: ((finite_finite @ TB) => (! [A:TA,B:TB]: ((finite1433825200ec_nth @ TA @ TB @ (finite_Cartesian_vec2 @ TA @ TB @ A) @ B) = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_58_vec__component)).
% 38.74/15.80 thf(874,plain,((! [TA: $tType,TB: $tType]: ((finite_finite @ TB) => (! [A:TA,B:TB]: ((finite1433825200ec_nth @ TA @ TB @ (finite_Cartesian_vec2 @ TA @ TB @ A) @ B) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[174])).
% 38.74/15.80 thf(338,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/sandbox2/benchmark/theBenchmark.p',fact_103_zle__diff1__eq)).
% 38.74/15.80 thf(1259,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)],[338])).
% 38.74/15.80 thf(200,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int]: ((ord_less_eq @ TA @ (ring_1_of_int @ TA @ A) @ (one_one @ TA)) = (ord_less_eq @ int @ A @ (one_one @ int))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_104_of__int__le__1__iff)).
% 38.74/15.80 thf(948,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int]: ((ord_less_eq @ TA @ (ring_1_of_int @ TA @ A) @ (one_one @ TA)) = (ord_less_eq @ int @ A @ (one_one @ int))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[200])).
% 38.74/15.80 thf(232,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int]: ((ord_less_eq @ TA @ (one_one @ TA) @ (ring_1_of_int @ TA @ A)) = (ord_less_eq @ int @ (one_one @ int) @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_105_of__int__1__le__iff)).
% 38.74/15.80 thf(1017,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int]: ((ord_less_eq @ TA @ (one_one @ TA) @ (ring_1_of_int @ TA @ A)) = (ord_less_eq @ int @ (one_one @ int) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[232])).
% 38.74/15.80 thf(323,axiom,((preorder @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Opreorder_26)).
% 38.74/15.80 thf(1227,plain,((preorder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[323])).
% 38.74/15.80 thf(117,axiom,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_fun___Orderings_Oorder)).
% 38.74/15.80 thf(725,plain,((! [TA: $tType,TB: $tType]: ((order @ TA) => (order @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[117])).
% 38.74/15.80 thf(16,axiom,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_215_lt__ex)).
% 38.74/15.80 thf(403,plain,((! [TA: $tType]: ((no_bot @ TA) => (! [A:TA]: ? [B:TA]: (ord_less @ TA @ B @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 38.74/15.80 thf(271,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: ((archimedean_ceiling @ TA @ (minus_minus @ TA @ A @ (ring_1_of_int @ TA @ B))) = (minus_minus @ int @ (archimedean_ceiling @ TA @ A) @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_34_ceiling__diff__of__int)).
% 38.74/15.80 thf(1096,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: ((archimedean_ceiling @ TA @ (minus_minus @ TA @ A @ (ring_1_of_int @ TA @ B))) = (minus_minus @ int @ (archimedean_ceiling @ TA @ A) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[271])).
% 38.74/15.80 thf(171,axiom,((! [TA: $tType]: ((ring_1 @ TA) => (! [A:int]: (member @ TA @ (ring_1_of_int @ TA @ A) @ (ring_1_Ints @ TA)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_20_Ints__of__int)).
% 38.74/15.80 thf(869,plain,((! [TA: $tType]: ((ring_1 @ TA) => (! [A:int]: (member @ TA @ (ring_1_of_int @ TA @ A) @ (ring_1_Ints @ TA)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[171])).
% 38.74/15.80 thf(220,axiom,((idom_abs_sgn @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Oidom__abs__sgn_25)).
% 38.74/15.80 thf(989,plain,((idom_abs_sgn @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[220])).
% 38.74/15.80 thf(166,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((ord_less @ TA @ A @ B) = (ord_less @ TA @ C @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_85_diff__eq__diff__less)).
% 38.74/15.80 thf(857,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((ord_less @ TA @ A @ B) = (ord_less @ TA @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[166])).
% 38.74/15.80 thf(140,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (A != B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_209_less__imp__neq)).
% 38.74/15.80 thf(783,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[140])).
% 38.74/15.80 thf(24,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((A = B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_172_eq__refl)).
% 38.74/15.80 thf(420,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((A = B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 38.74/15.80 thf(275,axiom,((! [TA: $tType,TB: $tType]: (((real_V55928688vector @ TA) & (finite_finite @ TB)) => (! [A:(finite_Cartesian_vec @ TA @ TB),B:TB]: (ord_less_eq @ real @ (real_V1127708846m_norm @ TA @ (finite1433825200ec_nth @ TA @ TB @ A @ B)) @ (real_V1127708846m_norm @ (finite_Cartesian_vec @ TA @ TB) @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_134_Finite__Cartesian__Product_Onorm__nth__le)).
% 38.74/15.80 thf(1118,plain,((! [TA: $tType,TB: $tType]: (((real_V55928688vector @ TA) & (finite_finite @ TB)) => (! [A:(finite_Cartesian_vec @ TA @ TB),B:TB]: (ord_less_eq @ real @ (real_V1127708846m_norm @ TA @ (finite1433825200ec_nth @ TA @ TB @ A @ B)) @ (real_V1127708846m_norm @ (finite_Cartesian_vec @ TA @ TB) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[275])).
% 38.74/15.80 thf(36,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_176_ord__le__eq__subst)).
% 38.74/15.80 thf(471,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => (((C @ B) = D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 38.74/15.80 thf(178,axiom,((! [TA: $tType]: ((ring_1 @ TA) => (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (ring_1_Ints @ TA)) => ((! [C:int]: (B @ (ring_1_of_int @ TA @ C))) => (B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_21_Ints__induct)).
% 38.74/15.80 thf(884,plain,((! [TA: $tType]: ((ring_1 @ TA) => (! [A:TA,B:(TA > $o)]: ((member @ TA @ A @ (ring_1_Ints @ TA)) => ((! [C:int]: (B @ (ring_1_of_int @ TA @ C))) => (B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[178])).
% 38.74/15.80 thf(293,axiom,((! [TA: $tType,TB: $tType]: (((ring @ TA) & (finite_finite @ TB)) => (! [A:TA,B:TA,C:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ (finite431509953r_mult @ TA @ TB @ A @ C) @ (finite431509953r_mult @ TA @ TB @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_31_vector__sub__rdistrib)).
% 38.74/15.80 thf(1160,plain,((! [TA: $tType,TB: $tType]: (((ring @ TA) & (finite_finite @ TB)) => (! [A:TA,B:TA,C:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ (finite431509953r_mult @ TA @ TB @ A @ C) @ (finite431509953r_mult @ TA @ TB @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[293])).
% 38.74/15.80 thf(194,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TB) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_12_minus__apply)).
% 38.74/15.80 thf(933,plain,((! [TA: $tType,TB: $tType]: ((minus @ TB) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[194])).
% 38.74/15.80 thf(58,axiom,((! [TA: $tType]: ((wellorder @ TA) => (! [A:(TA > $o),B:TA]: ((! [C:TA]: ((! [D:TA]: ((ord_less @ TA @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_198_less__induct)).
% 38.74/15.80 thf(537,plain,((! [TA: $tType]: ((wellorder @ TA) => (! [A:(TA > $o),B:TA]: ((! [C:TA]: ((! [D:TA]: ((ord_less @ TA @ D @ C) => (A @ D))) => (A @ C))) => (A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[58])).
% 38.74/15.80 thf(96,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_226_order__less__le__subst1)).
% 38.74/15.80 thf(642,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[96])).
% 38.74/15.80 thf(40,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB)]: ((! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))) => (ord_less_eq @ (TA > TB) @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_181_le__funI)).
% 38.74/15.80 thf(489,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB)]: ((! [C:TA]: (ord_less_eq @ TB @ (A @ C) @ (B @ C))) => (ord_less_eq @ (TA > TB) @ (A) @ (B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 38.74/15.80 thf(317,axiom,((! [TA: $tType,TB: $tType]: (((ordere890947078_space @ TB) & (finite_finite @ TA)) => (ordere142940540dd_abs @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Groups_Oordered__ab__group__add__abs_55)).
% 38.74/15.80 thf(1214,plain,((! [TA: $tType,TB: $tType]: (((ordere890947078_space @ TB) & (finite_finite @ TA)) => (ordere142940540dd_abs @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[317])).
% 38.74/15.80 thf(185,axiom,((! [TA: $tType,TB: $tType]: (((ordere890947078_space @ TB) & (finite_finite @ TA)) => (ordered_ab_group_add @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Groups_Oordered__ab__group__add_58)).
% 38.74/15.80 thf(901,plain,((! [TA: $tType,TB: $tType]: (((ordere890947078_space @ TB) & (finite_finite @ TA)) => (ordered_ab_group_add @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[185])).
% 38.74/15.80 thf(104,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((B = C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_165_ord__le__eq__trans)).
% 38.74/15.80 thf(686,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((B = C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[104])).
% 38.74/15.80 thf(262,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: ((archim2085082626_floor @ TA @ (minus_minus @ TA @ A @ (ring_1_of_int @ TA @ B))) = (minus_minus @ int @ (archim2085082626_floor @ TA @ A) @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_37_floor__diff__of__int)).
% 38.74/15.80 thf(1075,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: ((archim2085082626_floor @ TA @ (minus_minus @ TA @ A @ (ring_1_of_int @ TA @ B))) = (minus_minus @ int @ (archim2085082626_floor @ TA @ A) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[262])).
% 38.74/15.80 thf(231,axiom,((condit1037483654norder @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Conditionally__Complete__Lattices_Oconditionally__complete__linorder_19)).
% 38.74/15.80 thf(1016,plain,((condit1037483654norder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[231])).
% 38.74/15.80 thf(79,axiom,((! [TA: $tType]: ((condit1656338222tinuum @ TA) => (! [A:TA]: ? [B:TA]: ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_184_ex__gt__or__lt)).
% 38.74/15.80 thf(590,plain,((! [TA: $tType]: ((condit1656338222tinuum @ TA) => (! [A:TA]: ? [B:TA]: ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[79])).
% 38.74/15.80 thf(291,axiom,((! [TA: $tType,TB: $tType]: (((ring @ TA) & (finite_finite @ TB)) => (! [A:TA,B:(finite_Cartesian_vec @ TA @ TB),C:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ A @ (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ B @ C)) = (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ (finite431509953r_mult @ TA @ TB @ A @ B) @ (finite431509953r_mult @ TA @ TB @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_59_vector__ssub__ldistrib)).
% 38.74/15.80 thf(1155,plain,((! [TA: $tType,TB: $tType]: (((ring @ TA) & (finite_finite @ TB)) => (! [A:TA,B:(finite_Cartesian_vec @ TA @ TB),C:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ A @ (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ B @ C)) = (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ (finite431509953r_mult @ TA @ TB @ A @ B) @ (finite431509953r_mult @ TA @ TB @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[291])).
% 38.74/15.80 thf(61,axiom,((! [TA: $tType]: ((ordere890947078_space @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_152_eucl__less__le__not__le)).
% 38.74/15.80 thf(547,plain,((! [TA: $tType]: ((ordere890947078_space @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[61])).
% 38.74/15.80 thf(157,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = ((ord_less @ TA @ B @ A) | (A = B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_187_not__less__iff__gr__or__eq)).
% 38.74/15.80 thf(837,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = ((ord_less @ TA @ B @ A) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[157])).
% 38.74/15.80 thf(366,axiom,((cancel146912293up_add @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ocancel__ab__semigroup__add_22)).
% 38.74/15.80 thf(1324,plain,((cancel146912293up_add @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[366])).
% 38.74/15.80 thf(272,axiom,((! [TA: $tType]: ((real_V2090557954_space @ TA) => (! [A:TA,B:TA]: ((abs_abs @ real @ (real_V2000881966t_dist @ TA @ A @ B)) = (real_V2000881966t_dist @ TA @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_96_real__abs__dist)).
% 38.74/15.80 thf(1099,plain,((! [TA: $tType]: ((real_V2090557954_space @ TA) => (! [A:TA,B:TA]: ((abs_abs @ real @ (real_V2000881966t_dist @ TA @ A @ B)) = (real_V2000881966t_dist @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[272])).
% 38.74/15.80 thf(341,axiom,((! [TA: $tType]: ((finite_finite @ TA) => (! [A:(finite_Cartesian_vec @ real @ TA),B:TA]: (ord_less_eq @ real @ (abs_abs @ real @ (finite1433825200ec_nth @ real @ TA @ A @ B)) @ (real_V1127708846m_norm @ (finite_Cartesian_vec @ real @ TA) @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_139_component__le__norm__cart)).
% 38.74/15.80 thf(1266,plain,((! [TA: $tType]: ((finite_finite @ TA) => (! [A:(finite_Cartesian_vec @ real @ TA),B:TA]: (ord_less_eq @ real @ (abs_abs @ real @ (finite1433825200ec_nth @ real @ TA @ A @ B)) @ (real_V1127708846m_norm @ (finite_Cartesian_vec @ real @ TA) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[341])).
% 38.74/15.80 thf(306,axiom,((! [TA: $tType]: ((cancel146912293up_add @ TA) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (minus_minus @ TA @ A @ C) @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_23_diff__right__commute)).
% 38.74/15.80 thf(1192,plain,((! [TA: $tType]: ((cancel146912293up_add @ TA) => (! [A:TA,B:TA,C:TA]: ((minus_minus @ TA @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ TA @ (minus_minus @ TA @ A @ C) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[306])).
% 38.74/15.80 thf(31,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_216_order__less__subst2)).
% 38.74/15.80 thf(457,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 38.74/15.80 thf(217,axiom,((! [A:(finite_Cartesian_vec @ real @ n),B:n]: ((member @ (finite_Cartesian_vec @ real @ n) @ A @ a) => (member @ real @ (finite1433825200ec_nth @ real @ n @ A @ B) @ (ring_1_Ints @ real))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_16_assms)).
% 38.74/15.80 thf(984,plain,((! [A:(finite_Cartesian_vec @ real @ n),B:n]: ((member @ (finite_Cartesian_vec @ real @ n) @ A @ a) => (member @ real @ (finite1433825200ec_nth @ real @ n @ A @ B) @ (ring_1_Ints @ real))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[217])).
% 38.74/15.80 thf(138,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ A @ B) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_182_le__funE)).
% 38.74/15.80 thf(779,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ (A) @ (B)) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[138])).
% 38.74/15.80 thf(4,axiom,((! [A:$o]: ((A = ($true)) | (A = ($false))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',help_If_3_1_T)).
% 38.74/15.80 thf(371,plain,(($true)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 38.74/15.80 thf(85,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_219_ord__eq__less__subst)).
% 38.74/15.80 thf(605,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (ord @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((A = (B @ C)) => ((ord_less @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less @ TA @ E @ F) => (ord_less @ TB @ (B @ E) @ (B @ F)))) => (ord_less @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[85])).
% 38.74/15.80 thf(266,axiom,((! [TA: $tType,TB: $tType]: (((field @ TA) & (finite_finite @ TB)) => (! [A:TA,B:TA,C:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ (finite431509953r_mult @ TA @ TB @ A @ C) @ (finite431509953r_mult @ TA @ TB @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_36_vec_Oscale__left__diff__distrib)).
% 38.74/15.80 thf(1086,plain,((! [TA: $tType,TB: $tType]: (((field @ TA) & (finite_finite @ TB)) => (! [A:TA,B:TA,C:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ (minus_minus @ TA @ A @ B) @ C) = (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ (finite431509953r_mult @ TA @ TB @ A @ C) @ (finite431509953r_mult @ TA @ TB @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[266])).
% 38.74/15.80 thf(329,axiom,((minus @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Ominus_4)).
% 38.74/15.80 thf(1241,plain,((minus @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[329])).
% 38.74/15.80 thf(250,axiom,((field @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Fields_Ofield)).
% 38.74/15.80 thf(1054,plain,((field @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[250])).
% 38.74/15.80 thf(241,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((archimedean_ceiling @ TA @ (minus_minus @ TA @ A @ (one_one @ TA))) = (minus_minus @ int @ (archimedean_ceiling @ TA @ A) @ (one_one @ int))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_68_ceiling__diff__one)).
% 38.74/15.80 thf(1035,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((archimedean_ceiling @ TA @ (minus_minus @ TA @ A @ (one_one @ TA))) = (minus_minus @ int @ (archimedean_ceiling @ TA @ A) @ (one_one @ int))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[241])).
% 38.74/15.80 thf(260,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (minus_minus @ TA @ (ring_1_of_int @ TA @ (archimedean_ceiling @ TA @ A)) @ (one_one @ TA)) @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_142_of__int__ceiling__diff__one__le)).
% 38.74/15.80 thf(1071,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (ord_less_eq @ TA @ (minus_minus @ TA @ (ring_1_of_int @ TA @ (archimedean_ceiling @ TA @ A)) @ (one_one @ TA)) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[260])).
% 38.74/15.80 thf(237,axiom,((ord_less @ real @ (real_V2000881966t_dist @ (finite_Cartesian_vec @ real @ n) @ y @ x) @ (one_one @ real))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_32__C1_C_I3_J)).
% 38.74/15.80 thf(1026,plain,((ord_less @ real @ (real_V2000881966t_dist @ (finite_Cartesian_vec @ real @ n) @ y @ x) @ (one_one @ real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[237])).
% 38.74/15.80 thf(203,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((ord_less_eq @ TA @ A @ B) = (ord_less_eq @ TA @ C @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_118_diff__eq__diff__less__eq)).
% 38.74/15.80 thf(953,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: (((minus_minus @ TA @ A @ B) = (minus_minus @ TA @ C @ D)) => ((ord_less_eq @ TA @ A @ B) = (ord_less_eq @ TA @ C @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[203])).
% 38.74/15.80 thf(77,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_201_dual__order_Oasym)).
% 38.74/15.80 thf(586,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[77])).
% 38.74/15.80 thf(179,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:TA]: ((ord_less @ int @ (archim2085082626_floor @ TA @ A) @ (archim2085082626_floor @ TA @ B)) => (ord_less @ TA @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_78_floor__less__cancel)).
% 38.74/15.80 thf(888,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:TA]: ((ord_less @ int @ (archim2085082626_floor @ TA @ A) @ (archim2085082626_floor @ TA @ B)) => (ord_less @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[179])).
% 38.74/15.80 thf(188,axiom,((member @ (finite_Cartesian_vec @ real @ n) @ y @ a)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0__C1_C_I2_J)).
% 38.74/15.80 thf(906,plain,((member @ (finite_Cartesian_vec @ real @ n) @ y @ a)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[188])).
% 38.74/15.80 thf(208,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_120_diff__left__mono)).
% 38.74/15.80 thf(965,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[208])).
% 38.74/15.80 thf(335,axiom,((! [TA: $tType,TB: $tType]: (((ring_1 @ TB) & (finite_finite @ TA)) => (ring_1 @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Rings_Oring__1_67)).
% 38.74/15.80 thf(1251,plain,((! [TA: $tType,TB: $tType]: (((ring_1 @ TB) & (finite_finite @ TA)) => (ring_1 @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[335])).
% 38.74/15.80 thf(320,axiom,((! [TA: $tType]: ((ring_1 @ TA) => ((ring_1_of_int @ TA @ (one_one @ int)) = (one_one @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_51_of__int__1)).
% 38.74/15.80 thf(1219,plain,((! [TA: $tType]: ((ring_1 @ TA) => ((ring_1_of_int @ TA @ (one_one @ int)) = (one_one @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[320])).
% 38.74/15.80 thf(125,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) = (B = A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_168_antisym__conv)).
% 38.74/15.80 thf(745,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) = (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[125])).
% 38.74/15.80 thf(72,axiom,((preorder @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Orderings_Opreorder_41)).
% 38.74/15.80 thf(573,plain,((preorder @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[72])).
% 38.74/15.80 thf(121,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_179_order__subst1)).
% 38.74/15.80 thf(733,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:(TA > TB),C:TA,D:TA]: ((ord_less_eq @ TB @ A @ (B @ C)) => ((ord_less_eq @ TA @ C @ D) => ((! [E:TA,F:TA]: ((ord_less_eq @ TA @ E @ F) => (ord_less_eq @ TB @ (B @ E) @ (B @ F)))) => (ord_less_eq @ TB @ A @ (B @ D))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[121])).
% 38.74/15.80 thf(290,axiom,((dense_linorder @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Odense__linorder)).
% 38.74/15.80 thf(1154,plain,((dense_linorder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[290])).
% 38.74/15.80 thf(15,axiom,((ring @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Rings_Oring_50)).
% 38.74/15.80 thf(402,plain,((ring @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 38.74/15.80 thf(278,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ int @ (archim2085082626_floor @ TA @ A) @ (archim2085082626_floor @ TA @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_109_floor__mono)).
% 38.74/15.80 thf(1125,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ int @ (archim2085082626_floor @ TA @ A) @ (archim2085082626_floor @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[278])).
% 38.74/15.80 thf(75,axiom,((! [TA: $tType,TB: $tType]: (((field @ TA) & (finite_finite @ TB)) => (! [A:TA,B:TA,C:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ A @ (finite431509953r_mult @ TA @ TB @ B @ C)) = (finite431509953r_mult @ TA @ TB @ B @ (finite431509953r_mult @ TA @ TB @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_72_vec_Oscale__left__commute)).
% 38.74/15.80 thf(579,plain,((! [TA: $tType,TB: $tType]: (((field @ TA) & (finite_finite @ TB)) => (! [A:TA,B:TA,C:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ A @ (finite431509953r_mult @ TA @ TB @ B @ C)) = (finite431509953r_mult @ TA @ TB @ B @ (finite431509953r_mult @ TA @ TB @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[75])).
% 38.74/15.80 thf(21,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((ord_less_eq @ TA @ A @ B) = (A = B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_231_antisym__conv1)).
% 38.74/15.80 thf(413,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((ord_less_eq @ TA @ A @ B) = (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 38.74/15.80 thf(66,axiom,((monoid_mult @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Groups_Omonoid__mult_43)).
% 38.74/15.80 thf(562,plain,((monoid_mult @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[66])).
% 38.74/15.80 thf(187,axiom,((! [TA: $tType,TB: $tType]: (((monoid_mult @ TB) & (finite_finite @ TA)) => (monoid_mult @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Groups_Omonoid__mult_61)).
% 38.74/15.80 thf(904,plain,((! [TA: $tType,TB: $tType]: (((monoid_mult @ TB) & (finite_finite @ TA)) => (monoid_mult @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[187])).
% 38.74/15.80 thf(214,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:int]: ((archim2085082626_floor @ TA @ (ring_1_of_int @ TA @ A)) = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_56_floor__of__int)).
% 38.74/15.80 thf(975,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:int]: ((archim2085082626_floor @ TA @ (ring_1_of_int @ TA @ A)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[214])).
% 38.74/15.80 thf(226,axiom,((zero @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ozero_37)).
% 38.74/15.80 thf(1007,plain,((zero @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[226])).
% 38.74/15.80 thf(107,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA,C:TA]: (((ord_less_eq @ TA @ A @ B) => (~ (ord_less_eq @ TA @ B @ C))) => (((ord_less_eq @ TA @ B @ A) => (~ (ord_less_eq @ TA @ A @ C))) => (((ord_less_eq @ TA @ A @ C) => (~ (ord_less_eq @ TA @ C @ B))) => (((ord_less_eq @ TA @ C @ B) => (~ (ord_less_eq @ TA @ B @ A))) => (((ord_less_eq @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))) => (~ ((ord_less_eq @ TA @ C @ A) => (~ (ord_less_eq @ TA @ A @ B))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_169_le__cases3)).
% 38.74/15.80 thf(694,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA,C:TA]: (((ord_less_eq @ TA @ A @ B) => (~ (ord_less_eq @ TA @ B @ C))) => (((ord_less_eq @ TA @ B @ A) => (~ (ord_less_eq @ TA @ A @ C))) => (((ord_less_eq @ TA @ A @ C) => (~ (ord_less_eq @ TA @ C @ B))) => (((ord_less_eq @ TA @ C @ B) => (~ (ord_less_eq @ TA @ B @ A))) => (((ord_less_eq @ TA @ B @ C) => (~ (ord_less_eq @ TA @ C @ A))) => (~ ((ord_less_eq @ TA @ C @ A) => (~ (ord_less_eq @ TA @ A @ B))))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[107])).
% 38.74/15.80 thf(74,axiom,((! [TA: $tType]: ((monoid_mult @ TA) => (monoid_mult @ (set @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Set_Oset___Groups_Omonoid__mult_6)).
% 38.74/15.80 thf(577,plain,((! [TA: $tType]: ((monoid_mult @ TA) => (monoid_mult @ (set @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[74])).
% 38.74/15.80 thf(109,axiom,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (one_one @ TA) @ (one_one @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_111_le__numeral__extra_I4_J)).
% 38.74/15.80 thf(711,plain,((! [TA: $tType]: ((linord1659791738miring @ TA) => (ord_less_eq @ TA @ (one_one @ TA) @ (one_one @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[109])).
% 38.74/15.80 thf(337,axiom,((! [TA: $tType,TB: $tType]: (((field @ TA) & (finite_finite @ TB)) => (! [A:TA,B:(finite_Cartesian_vec @ TA @ TB),C:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ A @ (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ B @ C)) = (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ (finite431509953r_mult @ TA @ TB @ A @ B) @ (finite431509953r_mult @ TA @ TB @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_91_vec_Oscale__right__diff__distrib)).
% 38.74/15.80 thf(1256,plain,((! [TA: $tType,TB: $tType]: (((field @ TA) & (finite_finite @ TB)) => (! [A:TA,B:(finite_Cartesian_vec @ TA @ TB),C:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ A @ (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ B @ C)) = (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ (finite431509953r_mult @ TA @ TB @ A @ B) @ (finite431509953r_mult @ TA @ TB @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[337])).
% 38.74/15.80 thf(60,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_170_order_Otrans)).
% 38.74/15.80 thf(545,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[60])).
% 38.74/15.80 thf(71,axiom,((cARD_1 @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Cardinality_OCARD__1)).
% 38.74/15.80 thf(572,plain,((cARD_1 @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[71])).
% 38.74/15.80 thf(343,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (((ring_1_of_int @ TA @ (archimedean_ceiling @ TA @ A)) = A) = (? [B:int]: (A = (ring_1_of_int @ TA @ B)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_93_of__int__ceiling__cancel)).
% 38.74/15.80 thf(1271,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (((ring_1_of_int @ TA @ (archimedean_ceiling @ TA @ A)) = A) = (? [B:int]: (A = (ring_1_of_int @ TA @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[343])).
% 38.74/15.80 thf(141,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_166_ord__eq__le__trans)).
% 38.74/15.80 thf(787,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[141])).
% 38.74/15.80 thf(110,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_188_dual__order_Ostrict__trans)).
% 38.74/15.80 thf(713,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[110])).
% 38.74/15.80 thf(146,axiom,((! [TA: $tType]: ((preorder @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_240_less__le__not__le)).
% 38.74/15.80 thf(804,plain,((! [TA: $tType]: ((preorder @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[146])).
% 38.74/15.80 thf(322,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:(int > $o),B:TA]: ((A @ (archimedean_ceiling @ TA @ B)) = (! [C:int]: (((ord_less @ TA @ (minus_minus @ TA @ (ring_1_of_int @ TA @ C) @ (one_one @ TA)) @ B) & (ord_less_eq @ TA @ B @ (ring_1_of_int @ TA @ C))) => (A @ C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_100_ceiling__split)).
% 38.74/15.80 thf(1224,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:(int > $o),B:TA]: ((A @ (archimedean_ceiling @ TA @ B)) = (! [C:int]: (((ord_less @ TA @ (minus_minus @ TA @ (ring_1_of_int @ TA @ C) @ (one_one @ TA)) @ B) & (ord_less_eq @ TA @ B @ (ring_1_of_int @ TA @ C))) => (A @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[322])).
% 38.74/15.80 thf(27,axiom,((! [TA: $tType,TB: $tType]: (((monoid_mult @ TA) & (finite_finite @ TB)) => (! [A:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ (one_one @ TA) @ A) = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_42_vector__smult__lid)).
% 38.74/15.80 thf(445,plain,((! [TA: $tType,TB: $tType]: (((monoid_mult @ TA) & (finite_finite @ TB)) => (! [A:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ (one_one @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 38.74/15.80 thf(195,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => ((abs_abs @ TA @ (one_one @ TA)) = (one_one @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_88_abs__one)).
% 38.74/15.80 thf(936,plain,((! [TA: $tType]: ((linordered_idom @ TA) => ((abs_abs @ TA @ (one_one @ TA)) = (one_one @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[195])).
% 38.74/15.80 thf(133,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_164_order__class_Oorder_Oantisym)).
% 38.74/15.80 thf(764,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[133])).
% 38.74/15.80 thf(155,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (B = A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_251_dual__order_Oorder__iff__strict)).
% 38.74/15.80 thf(831,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[155])).
% 38.74/15.80 thf(274,axiom,((linordered_idom @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Olinordered__idom_24)).
% 38.74/15.80 thf(1117,plain,((linordered_idom @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[274])).
% 38.74/15.80 thf(247,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:TA,B:TA]: ((member @ TA @ A @ (ring_1_Ints @ TA)) => ((member @ TA @ B @ (ring_1_Ints @ TA)) => ((A = B) = (ord_less @ TA @ (abs_abs @ TA @ (minus_minus @ TA @ A @ B)) @ (one_one @ TA))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_92_Ints__eq__abs__less1)).
% 38.74/15.80 thf(1048,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:TA,B:TA]: ((member @ TA @ A @ (ring_1_Ints @ TA)) => ((member @ TA @ B @ (ring_1_Ints @ TA)) => ((A = B) = (ord_less @ TA @ (abs_abs @ TA @ (minus_minus @ TA @ A @ B)) @ (one_one @ TA))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[247])).
% 38.74/15.80 thf(221,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_87_diff__strict__right__mono)).
% 38.74/15.80 thf(990,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[221])).
% 38.74/15.80 thf(29,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((~ (ord_less @ TA @ A @ B)) = (A = B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_232_antisym__conv2)).
% 38.74/15.80 thf(451,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((~ (ord_less @ TA @ A @ B)) = (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 38.74/15.80 thf(286,axiom,((real_V1639655670t_norm @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Real__Vector__Spaces_Odist__norm)).
% 38.74/15.80 thf(1144,plain,((real_V1639655670t_norm @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[286])).
% 38.74/15.80 thf(122,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_162_dual__order_Orefl)).
% 38.74/15.80 thf(737,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[122])).
% 38.74/15.80 thf(245,axiom,((! [TA: $tType,TB: $tType]: (((ring @ TB) & (finite_finite @ TA)) => (ring @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Rings_Oring_70)).
% 38.74/15.80 thf(1043,plain,((! [TA: $tType,TB: $tType]: (((ring @ TB) & (finite_finite @ TA)) => (ring @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[245])).
% 38.74/15.80 thf(87,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (ord_less @ TA @ B @ A)) = (B = A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_197_antisym__conv3)).
% 38.74/15.80 thf(616,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (ord_less @ TA @ B @ A)) = (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[87])).
% 38.74/15.80 thf(184,axiom,((linord1659791738miring @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Olinordered__nonzero__semiring_20)).
% 38.74/15.80 thf(900,plain,((linord1659791738miring @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[184])).
% 38.74/15.80 thf(18,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((A != B) => (ord_less @ TA @ A @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_230_le__neq__trans)).
% 38.74/15.80 thf(406,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((~ (A = B)) => (ord_less @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 38.74/15.80 thf(168,axiom,((! [TA: $tType]: ((archim1804426504_field @ TA) => (! [A:TA]: ? [B:int]: (ord_less @ TA @ A @ (ring_1_of_int @ TA @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_81_ex__less__of__int)).
% 38.74/15.80 thf(863,plain,((! [TA: $tType]: ((archim1804426504_field @ TA) => (! [A:TA]: ? [B:int]: (ord_less @ TA @ A @ (ring_1_of_int @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[168])).
% 38.74/15.80 thf(299,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (finite_finite @ TB)) => ((ord_less @ (finite_Cartesian_vec @ TA @ TB)) = (^ [A:(finite_Cartesian_vec @ TA @ TB),B:(finite_Cartesian_vec @ TA @ TB)]: ((ord_less_eq @ (finite_Cartesian_vec @ TA @ TB) @ A @ B) & ~ (ord_less_eq @ (finite_Cartesian_vec @ TA @ TB) @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_156_less__vec__def)).
% 38.74/15.80 thf(1175,plain,((! [TA: $tType,TB: $tType]: (((ord @ TA) & (finite_finite @ TB)) => ((ord_less @ (finite_Cartesian_vec @ TA @ TB)) = (^ [A:(finite_Cartesian_vec @ TA @ TB),B:(finite_Cartesian_vec @ TA @ TB)]: ((ord_less_eq @ (finite_Cartesian_vec @ TA @ TB) @ A @ B) & ~ (ord_less_eq @ (finite_Cartesian_vec @ TA @ TB) @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[299])).
% 38.74/15.80 thf(180,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int]: ((ord_less @ TA @ (one_one @ TA) @ (ring_1_of_int @ TA @ A)) = (ord_less @ int @ (one_one @ int) @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_60_of__int__1__less__iff)).
% 38.74/15.80 thf(890,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int]: ((ord_less @ TA @ (one_one @ TA) @ (ring_1_of_int @ TA @ A)) = (ord_less @ int @ (one_one @ int) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[180])).
% 38.74/15.80 thf(93,axiom,((linorder @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Orderings_Olinorder_42)).
% 38.74/15.80 thf(631,plain,((linorder @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[93])).
% 38.74/15.80 thf(130,axiom,((! [TA: $tType]: ((real_V2090557954_space @ TA) => (! [A:TA,B:(set @ TA),C:TA]: ((member @ TA @ A @ B) => ((member @ TA @ C @ B) => ((A = C) = (! [D:TA]: ((member @ TA @ D @ B) => ((real_V2000881966t_dist @ TA @ A @ D) = (real_V2000881966t_dist @ TA @ C @ D))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_145_metric__eq__thm)).
% 38.74/15.80 thf(758,plain,((! [TA: $tType]: ((real_V2090557954_space @ TA) => (! [A:TA,B:(set @ TA),C:TA]: ((member @ TA @ A @ B) => ((member @ TA @ C @ B) => ((A = C) = (! [D:TA]: ((member @ TA @ D @ B) => ((real_V2000881966t_dist @ TA @ A @ D) = (real_V2000881966t_dist @ TA @ C @ D))))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[130])).
% 38.74/15.80 thf(63,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_227_order__less__le__subst2)).
% 38.74/15.80 thf(552,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less @ TB @ E @ F) => (ord_less @ TA @ (C @ E) @ (C @ F)))) => (ord_less @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[63])).
% 38.74/15.80 thf(57,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_fun___Orderings_Oord)).
% 38.74/15.80 thf(535,plain,((! [TA: $tType,TB: $tType]: ((ord @ TA) => (ord @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[57])).
% 38.74/15.80 thf(367,axiom,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA,B:TA]: (ord_less_eq @ TA @ (minus_minus @ TA @ (abs_abs @ TA @ A) @ (abs_abs @ TA @ B)) @ (abs_abs @ TA @ (minus_minus @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_130_abs__triangle__ineq2__sym)).
% 38.74/15.80 thf(1325,plain,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA,B:TA]: (ord_less_eq @ TA @ (minus_minus @ TA @ (abs_abs @ TA @ A) @ (abs_abs @ TA @ B)) @ (abs_abs @ TA @ (minus_minus @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[367])).
% 38.74/15.80 thf(239,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((ord_less_eq @ int @ (one_one @ int) @ (archim2085082626_floor @ TA @ A)) = (ord_less_eq @ TA @ (one_one @ TA) @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_106_one__le__floor)).
% 38.74/15.80 thf(1029,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((ord_less_eq @ int @ (one_one @ int) @ (archim2085082626_floor @ TA @ A)) = (ord_less_eq @ TA @ (one_one @ TA) @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[239])).
% 38.74/15.80 thf(91,axiom,((preorder @ $o)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Opreorder_13)).
% 38.74/15.80 thf(626,plain,((preorder @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[91])).
% 38.74/15.80 thf(353,axiom,((! [TA: $tType,TB: $tType]: (((ordere890947078_space @ TB) & (finite_finite @ TA)) => (ordere890947078_space @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Ordered__Euclidean__Space_Oordered__euclidean__space_52)).
% 38.74/15.80 thf(1293,plain,((! [TA: $tType,TB: $tType]: (((ordere890947078_space @ TB) & (finite_finite @ TA)) => (ordere890947078_space @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[353])).
% 38.74/15.80 thf(255,axiom,((ring @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Oring_38)).
% 38.74/15.80 thf(1061,plain,((ring @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[255])).
% 38.74/15.80 thf(42,axiom,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_45_Collect__mem__eq)).
% 38.74/15.80 thf(494,plain,((! [TA: $tType]: (! [A:(set @ TA)]: ((collect @ TA @ (^ [B:TA]: (member @ TA @ B @ A))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[42])).
% 38.74/15.80 thf(264,axiom,((! [TA: $tType]: ((finite_finite @ TA) => (! [A:TA]: ((real_V1127708846m_norm @ (finite_Cartesian_vec @ real @ TA) @ (finite1218308419n_axis @ TA @ real @ A @ (one_one @ real))) = (one_one @ real)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_38_norm__axis__1)).
% 38.74/15.80 thf(1080,plain,((! [TA: $tType]: ((finite_finite @ TA) => (! [A:TA]: ((real_V1127708846m_norm @ (finite_Cartesian_vec @ real @ TA) @ (finite1218308419n_axis @ TA @ real @ A @ (one_one @ real))) = (one_one @ real)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[264])).
% 38.74/15.80 thf(198,axiom,((! [TA: $tType]: ((real_V1639655670t_norm @ TA) => ((real_V2000881966t_dist @ TA) = (^ [A:TA,B:TA]: (real_V1127708846m_norm @ TA @ (minus_minus @ TA @ A @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_73_dist__norm)).
% 38.74/15.80 thf(943,plain,((! [TA: $tType]: ((real_V1639655670t_norm @ TA) => ((real_V2000881966t_dist @ TA) = (^ [A:TA,B:TA]: (real_V1127708846m_norm @ TA @ (minus_minus @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[198])).
% 38.74/15.80 thf(234,axiom,((no_top @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Ono__top_29)).
% 38.74/15.80 thf(1022,plain,((no_top @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[234])).
% 38.74/15.80 thf(308,axiom,((! [TA: $tType]: ((ring_char_0 @ TA) => (! [A:int]: (((ring_1_of_int @ TA @ A) = (one_one @ TA)) = (A = (one_one @ int))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_50_of__int__eq__1__iff)).
% 38.74/15.80 thf(1198,plain,((! [TA: $tType]: ((ring_char_0 @ TA) => (! [A:int]: (((ring_1_of_int @ TA @ A) = (one_one @ TA)) = (A = (one_one @ int))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[308])).
% 38.74/15.80 thf(14,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_222_le__less)).
% 38.74/15.80 thf(399,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 38.74/15.80 thf(205,axiom,((idom_abs_sgn @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Oidom__abs__sgn)).
% 38.74/15.80 thf(959,plain,((idom_abs_sgn @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[205])).
% 38.74/15.80 thf(332,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ D) => (ord_less @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_84_diff__strict__mono)).
% 38.74/15.80 thf(1245,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ C @ D) => (ord_less @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[332])).
% 38.74/15.80 thf(67,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_174_antisym)).
% 38.74/15.80 thf(563,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ A) => (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[67])).
% 38.74/15.80 thf(103,axiom,((minus @ $o)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_HOL_Obool___Groups_Ominus_18)).
% 38.74/15.80 thf(685,plain,((minus @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[103])).
% 38.74/15.80 thf(52,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_173_linear)).
% 38.74/15.80 thf(521,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[52])).
% 38.74/15.80 thf(298,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((ord_less @ TA @ (minus_minus @ TA @ (ring_1_of_int @ TA @ (archimedean_ceiling @ TA @ A)) @ (one_one @ TA)) @ A) & (ord_less_eq @ TA @ A @ (ring_1_of_int @ TA @ (archimedean_ceiling @ TA @ A)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_148_ceiling__correct)).
% 38.74/15.80 thf(1171,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((ord_less @ TA @ (minus_minus @ TA @ (ring_1_of_int @ TA @ (archimedean_ceiling @ TA @ A)) @ (one_one @ TA)) @ A) & (ord_less_eq @ TA @ A @ (ring_1_of_int @ TA @ (archimedean_ceiling @ TA @ A)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[298])).
% 38.74/15.80 thf(316,axiom,((condit1656338222tinuum @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Conditionally__Complete__Lattices_Olinear__continuum)).
% 38.74/15.80 thf(1213,plain,((condit1656338222tinuum @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[316])).
% 38.74/15.80 thf(154,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (B != A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_196_less__imp__not__eq2)).
% 38.74/15.80 thf(827,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[154])).
% 38.74/15.80 thf(163,axiom,((member @ (finite_Cartesian_vec @ real @ n) @ x @ a)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__C1_C_I1_J)).
% 38.74/15.80 thf(851,plain,((member @ (finite_Cartesian_vec @ real @ n) @ x @ a)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[163])).
% 38.74/15.80 thf(273,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/sandbox2/benchmark/theBenchmark.p',fact_114_int__le__induct)).
% 38.74/15.80 thf(1102,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)],[273])).
% 38.74/15.80 thf(114,axiom,((ord @ $o)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oord_17)).
% 38.74/15.80 thf(722,plain,((ord @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[114])).
% 38.74/15.80 thf(98,axiom,((((?) @ numeral_num1) = (^ [A:(numeral_num1 > $o)]: (A @ (one_one @ numeral_num1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_254_ex__1)).
% 38.74/15.80 thf(675,plain,((((?) @ numeral_num1) = (^ [A:(numeral_num1 > $o)]: (A @ (one_one @ numeral_num1))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[98])).
% 38.74/15.80 thf(358,axiom,((! [TA: $tType,TB: $tType]: (((minus @ TB) & (finite_finite @ TA)) => (minus @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Groups_Ominus_68)).
% 38.74/15.80 thf(1304,plain,((! [TA: $tType,TB: $tType]: (((minus @ TB) & (finite_finite @ TA)) => (minus @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[358])).
% 38.74/15.80 thf(296,axiom,((! [TA: $tType]: ((real_V55928688vector @ TA) => ((real_V1127708846m_norm @ (finite_Cartesian_vec @ TA @ numeral_num1)) = (^ [A:(finite_Cartesian_vec @ TA @ numeral_num1)]: (real_V1127708846m_norm @ TA @ (finite1433825200ec_nth @ TA @ numeral_num1 @ A @ (one_one @ numeral_num1)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_124_norm__vector__1)).
% 38.74/15.80 thf(1166,plain,((! [TA: $tType]: ((real_V55928688vector @ TA) => ((real_V1127708846m_norm @ (finite_Cartesian_vec @ TA @ numeral_num1)) = (^ [A:(finite_Cartesian_vec @ TA @ numeral_num1)]: (real_V1127708846m_norm @ TA @ (finite1433825200ec_nth @ TA @ numeral_num1 @ A @ (one_one @ numeral_num1)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[296])).
% 38.74/15.80 thf(55,axiom,((one @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Groups_Oone_51)).
% 38.74/15.80 thf(531,plain,((one @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[55])).
% 38.74/15.80 thf(101,axiom,((! [TA: $tType]: ((one @ TA) => (one @ (set @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Set_Oset___Groups_Oone_12)).
% 38.74/15.80 thf(680,plain,((! [TA: $tType]: ((one @ TA) => (one @ (set @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[101])).
% 38.74/15.80 thf(6,axiom,((! [TA: $tType]: (order @ (set @ TA)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Oorder_8)).
% 38.74/15.80 thf(374,plain,((! [TA: $tType]: (order @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 38.74/15.80 thf(346,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: ((ord_less_eq @ int @ (archimedean_ceiling @ TA @ A) @ B) = (ord_less_eq @ TA @ A @ (ring_1_of_int @ TA @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_117_ceiling__le__iff)).
% 38.74/15.80 thf(1277,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: ((ord_less_eq @ int @ (archimedean_ceiling @ TA @ A) @ B) = (ord_less_eq @ TA @ A @ (ring_1_of_int @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[346])).
% 38.74/15.80 thf(282,axiom,((! [TA: $tType]: ((real_V1229719638ebra_1 @ TA) => ((real_V1127708846m_norm @ TA @ (one_one @ TA)) = (one_one @ real))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_62_norm__one)).
% 38.74/15.80 thf(1134,plain,((! [TA: $tType]: ((real_V1229719638ebra_1 @ TA) => ((real_V1127708846m_norm @ TA @ (one_one @ TA)) = (one_one @ real))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[282])).
% 38.74/15.80 thf(50,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_234_le__less__trans)).
% 38.74/15.80 thf(516,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[50])).
% 38.74/15.80 thf(196,axiom,((! [TA: $tType]: (! [A:(finite_Cartesian_vec @ TA @ numeral_num1)]: ((finite_Cartesian_vec2 @ TA @ numeral_num1 @ (finite1433825200ec_nth @ TA @ numeral_num1 @ A @ (one_one @ numeral_num1))) = A)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_155_vector__one__nth)).
% 38.74/15.80 thf(939,plain,((! [TA: $tType]: (! [A:(finite_Cartesian_vec @ TA @ numeral_num1)]: ((finite_Cartesian_vec2 @ TA @ numeral_num1 @ (finite1433825200ec_nth @ TA @ numeral_num1 @ A @ (one_one @ numeral_num1))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[196])).
% 38.74/15.80 thf(287,axiom,((! [TA: $tType]: ((ring_1 @ TA) => (! [A:int,B:int]: ((ring_1_of_int @ TA @ (minus_minus @ int @ A @ B)) = (minus_minus @ TA @ (ring_1_of_int @ TA @ A) @ (ring_1_of_int @ TA @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_6_of__int__diff)).
% 38.74/15.80 thf(1145,plain,((! [TA: $tType]: ((ring_1 @ TA) => (! [A:int,B:int]: ((ring_1_of_int @ TA @ (minus_minus @ int @ A @ B)) = (minus_minus @ TA @ (ring_1_of_int @ TA @ A) @ (ring_1_of_int @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[287])).
% 38.74/15.80 thf(128,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_220_leD)).
% 38.74/15.80 thf(754,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[128])).
% 38.74/15.80 thf(310,axiom,((! [TA: $tType]: ((real_V55928688vector @ TA) => (! [A:TA,B:TA]: ((real_V1127708846m_norm @ TA @ (minus_minus @ TA @ A @ B)) = (real_V1127708846m_norm @ TA @ (minus_minus @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_79_norm__minus__commute)).
% 38.74/15.80 thf(1203,plain,((! [TA: $tType]: ((real_V55928688vector @ TA) => (! [A:TA,B:TA]: ((real_V1127708846m_norm @ TA @ (minus_minus @ TA @ A @ B)) = (real_V1127708846m_norm @ TA @ (minus_minus @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[310])).
% 38.74/15.80 thf(312,axiom,((! [TA: $tType]: ((real_V55928688vector @ TA) => (! [A:TA,B:TA]: (ord_less_eq @ real @ (minus_minus @ real @ (real_V1127708846m_norm @ TA @ A) @ (real_V1127708846m_norm @ TA @ B)) @ (real_V1127708846m_norm @ TA @ (minus_minus @ TA @ A @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_143_norm__triangle__ineq2)).
% 38.74/15.80 thf(1208,plain,((! [TA: $tType]: ((real_V55928688vector @ TA) => (! [A:TA,B:TA]: (ord_less_eq @ real @ (minus_minus @ real @ (real_V1127708846m_norm @ TA @ A) @ (real_V1127708846m_norm @ TA @ B)) @ (real_V1127708846m_norm @ TA @ (minus_minus @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[312])).
% 38.74/15.80 thf(210,axiom,((! [TA: $tType]: ((finite_finite @ TA) => (! [A:TA]: ((finite1115014511_index @ real @ TA @ (finite1218308419n_axis @ TA @ real @ A @ (one_one @ real))) = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_98_axis__index__axis)).
% 38.74/15.80 thf(968,plain,((! [TA: $tType]: ((finite_finite @ TA) => (! [A:TA]: ((finite1115014511_index @ real @ TA @ (finite1218308419n_axis @ TA @ real @ A @ (one_one @ real))) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[210])).
% 38.74/15.80 thf(301,axiom,((! [TA: $tType]: ((real_V1229719638ebra_1 @ TA) => (! [A:int]: ((real_V1127708846m_norm @ TA @ (ring_1_of_int @ TA @ A)) = (abs_abs @ real @ (ring_1_of_int @ real @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_33_norm__of__int)).
% 38.74/15.80 thf(1181,plain,((! [TA: $tType]: ((real_V1229719638ebra_1 @ TA) => (! [A:int]: ((real_V1127708846m_norm @ TA @ (ring_1_of_int @ TA @ A)) = (abs_abs @ real @ (ring_1_of_int @ real @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[301])).
% 38.74/15.80 thf(153,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((B = C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_202_ord__less__eq__trans)).
% 38.74/15.80 thf(823,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((B = C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[153])).
% 38.74/15.80 thf(137,axiom,((! [TA: $tType,TB: $tType]: (((field @ TA) & (finite_finite @ TB)) => (! [A:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ (one_one @ TA) @ A) = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_41_vec_Oscale__one)).
% 38.74/15.80 thf(776,plain,((! [TA: $tType,TB: $tType]: (((field @ TA) & (finite_finite @ TB)) => (! [A:(finite_Cartesian_vec @ TA @ TB)]: ((finite431509953r_mult @ TA @ TB @ (one_one @ TA) @ A) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[137])).
% 38.74/15.80 thf(165,axiom,((! [TA: $tType,TB: $tType]: (((ord @ TB) & (finite_finite @ TA)) => (ord @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Orderings_Oord_66)).
% 38.74/15.80 thf(855,plain,((! [TA: $tType,TB: $tType]: (((ord @ TB) & (finite_finite @ TA)) => (ord @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[165])).
% 38.74/15.80 thf(105,axiom,((minus @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Groups_Ominus_48)).
% 38.74/15.80 thf(690,plain,((minus @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[105])).
% 38.74/15.80 thf(236,axiom,((finite_finite @ n)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tfree_0)).
% 38.74/15.80 thf(1025,plain,((finite_finite @ n)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[236])).
% 38.74/15.80 thf(259,axiom,((cancel146912293up_add @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Ocancel__ab__semigroup__add)).
% 38.74/15.80 thf(1070,plain,((cancel146912293up_add @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[259])).
% 38.74/15.80 thf(211,axiom,((group_add @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ogroup__add_31)).
% 38.74/15.80 thf(971,plain,((group_add @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[211])).
% 38.74/15.80 thf(123,axiom,((((!) @ numeral_num1) = (^ [A:(numeral_num1 > $o)]: (A @ (one_one @ numeral_num1))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_253_forall__1)).
% 38.74/15.80 thf(739,plain,((((!) @ numeral_num1) = (^ [A:(numeral_num1 > $o)]: (A @ (one_one @ numeral_num1))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[123])).
% 38.74/15.80 thf(19,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_154_dual__order_Ostrict__implies__order)).
% 38.74/15.80 thf(409,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 38.74/15.80 thf(325,axiom,((! [TA: $tType,TB: $tType]: (((finite_finite @ TA) & (minus @ TB)) => (! [A:(finite_Cartesian_vec @ TB @ TA),B:(finite_Cartesian_vec @ TB @ TA),C:TA]: ((finite1433825200ec_nth @ TB @ TA @ (minus_minus @ (finite_Cartesian_vec @ TB @ TA) @ A @ B) @ C) = (minus_minus @ TB @ (finite1433825200ec_nth @ TB @ TA @ A @ C) @ (finite1433825200ec_nth @ TB @ TA @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_vector__minus__component)).
% 38.74/15.80 thf(1230,plain,((! [TA: $tType,TB: $tType]: (((finite_finite @ TA) & (minus @ TB)) => (! [A:(finite_Cartesian_vec @ TB @ TA),B:(finite_Cartesian_vec @ TB @ TA),C:TA]: ((finite1433825200ec_nth @ TB @ TA @ (minus_minus @ (finite_Cartesian_vec @ TB @ TA) @ A @ B) @ C) = (minus_minus @ TB @ (finite1433825200ec_nth @ TB @ TA @ A @ C) @ (finite1433825200ec_nth @ TB @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[325])).
% 38.74/15.80 thf(249,axiom,((archim1804426504_field @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Archimedean__Field_Oarchimedean__field)).
% 38.74/15.80 thf(1053,plain,((archim1804426504_field @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[249])).
% 38.74/15.80 thf(356,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ D) => (ord_less_eq @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_121_diff__mono)).
% 38.74/15.80 thf(1300,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA,D:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ D) => (ord_less_eq @ TA @ (minus_minus @ TA @ A @ D) @ (minus_minus @ TA @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[356])).
% 38.74/15.80 thf(142,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_193_dual__order_Oirrefl)).
% 38.74/15.80 thf(791,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA]: ~ (ord_less @ TA @ A @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[142])).
% 38.74/15.80 thf(112,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ A @ B) | (A = B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_239_le__imp__less__or__eq)).
% 38.74/15.80 thf(717,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ A @ B) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[112])).
% 38.74/15.80 thf(45,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))) => (ord_less_eq @ TA @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_237_dense__le)).
% 38.74/15.80 thf(502,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA]: ((! [C:TA]: ((ord_less @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))) => (ord_less_eq @ TA @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[45])).
% 38.74/15.80 thf(158,axiom,((! [TA: $tType,TB: $tType]: (((real_V55928688vector @ TB) & (finite_finite @ TA)) => (real_V55928688vector @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Real__Vector__Spaces_Oreal__normed__vector_53)).
% 38.74/15.80 thf(840,plain,((! [TA: $tType,TB: $tType]: (((real_V55928688vector @ TB) & (finite_finite @ TA)) => (real_V55928688vector @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[158])).
% 38.74/15.80 thf(339,axiom,((! [TA: $tType,TB: $tType]: (((zero @ TB) & (finite_finite @ TA)) => (zero @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Groups_Ozero_69)).
% 38.74/15.80 thf(1262,plain,((! [TA: $tType,TB: $tType]: (((zero @ TB) & (finite_finite @ TA)) => (zero @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[339])).
% 38.74/15.80 thf(33,axiom,((! [TA: $tType,TB: $tType]: (((finite_finite @ TB) & (finite_finite @ TA)) => (finite_finite @ (TB > TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_fun___Finite__Set_Ofinite)).
% 38.74/15.80 thf(463,plain,((! [TA: $tType,TB: $tType]: (((finite_finite @ TB) & (finite_finite @ TA)) => (finite_finite @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 38.74/15.80 thf(201,axiom,((ordere142940540dd_abs @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Oordered__ab__group__add__abs)).
% 38.74/15.80 thf(951,plain,((ordere142940540dd_abs @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[201])).
% 38.74/15.80 thf(280,axiom,(((ord_less_eq @ real) = (^ [A:real,B:real]: ((ord_less @ real @ A @ B) | (A = B))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_110_less__eq__real__def)).
% 38.74/15.80 thf(1130,plain,(((ord_less_eq @ real) = (^ [A:real,B:real]: ((ord_less @ real @ A @ B) | (A = B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[280])).
% 38.74/15.80 thf(189,axiom,((! [TA: $tType,TB: $tType]: (((finite_finite @ TA) & (ring_1 @ TB)) => (! [A:(finite_Cartesian_vec @ int @ TA),B:TA]: ((finite1433825200ec_nth @ TB @ TA @ (minkow1937162798nt_vec @ TA @ TB @ A) @ B) = (ring_1_of_int @ TB @ (finite1433825200ec_nth @ int @ TA @ A @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_8_of__int__vec__nth)).
% 38.74/15.80 thf(907,plain,((! [TA: $tType,TB: $tType]: (((finite_finite @ TA) & (ring_1 @ TB)) => (! [A:(finite_Cartesian_vec @ int @ TA),B:TA]: ((finite1433825200ec_nth @ TB @ TA @ (minkow1937162798nt_vec @ TA @ TB @ A) @ B) = (ring_1_of_int @ TB @ (finite1433825200ec_nth @ int @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[189])).
% 38.74/15.80 thf(304,axiom,((no_bot @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Ono__bot)).
% 38.74/15.80 thf(1188,plain,((no_bot @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[304])).
% 38.74/15.80 thf(303,axiom,((! [TA: $tType,TB: $tType]: (((real_V2090557954_space @ TA) & (finite_finite @ TB)) => (! [A:(finite_Cartesian_vec @ TA @ TB),B:TB,C:(finite_Cartesian_vec @ TA @ TB)]: (ord_less_eq @ real @ (real_V2000881966t_dist @ TA @ (finite1433825200ec_nth @ TA @ TB @ A @ B) @ (finite1433825200ec_nth @ TA @ TB @ C @ B)) @ (real_V2000881966t_dist @ (finite_Cartesian_vec @ TA @ TB) @ A @ C)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_146_dist__vec__nth__le)).
% 38.74/15.80 thf(1186,plain,((! [TA: $tType,TB: $tType]: (((real_V2090557954_space @ TA) & (finite_finite @ TB)) => (! [A:(finite_Cartesian_vec @ TA @ TB),B:TB,C:(finite_Cartesian_vec @ TA @ TB)]: (ord_less_eq @ real @ (real_V2000881966t_dist @ TA @ (finite1433825200ec_nth @ TA @ TB @ A @ B) @ (finite1433825200ec_nth @ TA @ TB @ C @ B)) @ (real_V2000881966t_dist @ (finite_Cartesian_vec @ TA @ TB) @ A @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[303])).
% 38.74/15.80 thf(242,axiom,((! [TA: $tType,TB: $tType]: (((group_add @ TB) & (finite_finite @ TA)) => (group_add @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Groups_Ogroup__add_63)).
% 38.74/15.80 thf(1038,plain,((! [TA: $tType,TB: $tType]: (((group_add @ TB) & (finite_finite @ TA)) => (group_add @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[242])).
% 38.74/15.80 thf(3,axiom,((order @ $o)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_HOL_Obool___Orderings_Oorder_16)).
% 38.74/15.80 thf(370,plain,((order @ $o)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 38.74/15.80 thf(285,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:int,B:TA]: ((ord_less @ TA @ (minus_minus @ TA @ (ring_1_of_int @ TA @ A) @ (one_one @ TA)) @ B) => ((ord_less_eq @ TA @ B @ (ring_1_of_int @ TA @ A)) => ((archimedean_ceiling @ TA @ B) = A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_149_ceiling__unique)).
% 38.74/15.80 thf(1141,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:int,B:TA]: ((ord_less @ TA @ (minus_minus @ TA @ (ring_1_of_int @ TA @ A) @ (one_one @ TA)) @ B) => ((ord_less_eq @ TA @ B @ (ring_1_of_int @ TA @ A)) => ((archimedean_ceiling @ TA @ B) = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[285])).
% 38.74/15.80 thf(235,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ (ring_1_of_int @ TA @ (archimedean_ceiling @ TA @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_137_le__of__int__ceiling)).
% 38.74/15.80 thf(1023,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ (ring_1_of_int @ TA @ (archimedean_ceiling @ TA @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[235])).
% 38.74/15.80 thf(86,axiom,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_167_order__class_Oorder_Oeq__iff)).
% 38.74/15.80 thf(613,plain,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (ord_less_eq @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[86])).
% 38.74/15.80 thf(349,axiom,((! [TA: $tType]: ((ring_1 @ TA) => (! [A:TA]: ((member @ TA @ A @ (ring_1_Ints @ TA)) => (~ (! [B:int]: (A != (ring_1_of_int @ TA @ B))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_22_Ints__cases)).
% 38.74/15.80 thf(1284,plain,((! [TA: $tType]: ((ring_1 @ TA) => (! [A:TA]: ((member @ TA @ A @ (ring_1_Ints @ TA)) => (~ (! [B:int]: ~ (A = (ring_1_of_int @ TA @ B))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[349])).
% 38.74/15.80 thf(83,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_191_less__imp__not__less)).
% 38.74/15.80 thf(600,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (~ (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[83])).
% 38.74/15.80 thf(118,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_163_order__trans)).
% 38.74/15.80 thf(727,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ B @ C) => (ord_less_eq @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[118])).
% 38.74/15.80 thf(227,axiom,((linorder @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Olinorder_27)).
% 38.74/15.80 thf(1008,plain,((linorder @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[227])).
% 38.74/15.80 thf(81,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((A != B) => (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_194_linorder__cases)).
% 38.74/15.80 thf(595,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) => ((~ (A = B)) => (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[81])).
% 38.74/15.80 thf(43,axiom,((! [TA: $tType,TB: $tType]: ((finite_finite @ TB) => (! [A:TA,B:TA]: (((finite_Cartesian_vec2 @ TA @ TB @ A) = (finite_Cartesian_vec2 @ TA @ TB @ B)) = (A = B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_40_vec__inj)).
% 38.74/15.80 thf(497,plain,((! [TA: $tType,TB: $tType]: ((finite_finite @ TB) => (! [A:TA,B:TA]: (((finite_Cartesian_vec2 @ TA @ TB @ A) = (finite_Cartesian_vec2 @ TA @ TB @ B)) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[43])).
% 38.74/15.80 thf(270,axiom,((! [TA: $tType]: ((archim1804426504_field @ TA) => (! [A:TA]: ? [B:int]: (ord_less @ TA @ (ring_1_of_int @ TA @ B) @ A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_82_ex__of__int__less)).
% 38.74/15.80 thf(1094,plain,((! [TA: $tType]: ((archim1804426504_field @ TA) => (! [A:TA]: ? [B:int]: (ord_less @ TA @ (ring_1_of_int @ TA @ B) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[270])).
% 38.74/15.80 thf(215,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: (((archimedean_ceiling @ TA @ A) = B) = ((ord_less @ TA @ (minus_minus @ TA @ (ring_1_of_int @ TA @ B) @ (one_one @ TA)) @ A) & (ord_less_eq @ TA @ A @ (ring_1_of_int @ TA @ B)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_101_ceiling__eq__iff)).
% 38.74/15.80 thf(978,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:int]: (((archimedean_ceiling @ TA @ A) = B) = ((ord_less @ TA @ (minus_minus @ TA @ (ring_1_of_int @ TA @ B) @ (one_one @ TA)) @ A) & (ord_less_eq @ TA @ A @ (ring_1_of_int @ TA @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[215])).
% 38.74/15.80 thf(284,axiom,((group_add @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Ogroup__add)).
% 38.74/15.80 thf(1140,plain,((group_add @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[284])).
% 38.74/15.80 thf(160,axiom,((one @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Oone)).
% 38.74/15.80 thf(845,plain,((one @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[160])).
% 38.74/15.80 thf(34,axiom,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_206_less__trans)).
% 38.74/15.80 thf(465,plain,((! [TA: $tType]: ((preorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 38.74/15.80 thf(92,axiom,((! [TA: $tType]: ((dense_order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (? [C:TA]: ((ord_less @ TA @ A @ C) & (ord_less @ TA @ C @ B)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_210_dense)).
% 38.74/15.80 thf(627,plain,((! [TA: $tType]: ((dense_order @ TA) => (! [A:TA,B:TA]: ((ord_less @ TA @ A @ B) => (? [C:TA]: ((ord_less @ TA @ A @ C) & (ord_less @ TA @ C @ B)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[92])).
% 38.74/15.80 thf(64,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A != B) = ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_212_neq__iff)).
% 38.74/15.80 thf(556,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) = ((ord_less @ TA @ A @ B) | (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[64])).
% 38.74/15.80 thf(193,axiom,(((real_V1127708846m_norm @ real) = (abs_abs @ real))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_80_real__norm__def)).
% 38.74/15.80 thf(931,plain,(((real_V1127708846m_norm @ real) = (abs_abs @ real))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[193])).
% 38.74/15.80 thf(363,axiom,((condit1037483654norder @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Conditionally__Complete__Lattices_Oconditionally__complete__linorder)).
% 38.74/15.80 thf(1321,plain,((condit1037483654norder @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[363])).
% 38.74/15.80 thf(186,axiom,((linordered_idom @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Rings_Olinordered__idom)).
% 38.74/15.80 thf(903,plain,((linordered_idom @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[186])).
% 38.74/15.80 thf(318,axiom,((zero @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Groups_Ozero)).
% 38.74/15.80 thf(1216,plain,((zero @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[318])).
% 38.74/15.80 thf(305,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => ((archimedean_ceiling @ TA @ (one_one @ TA)) = (one_one @ int))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_54_ceiling__one)).
% 38.74/15.80 thf(1189,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => ((archimedean_ceiling @ TA @ (one_one @ TA)) = (one_one @ int))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[305])).
% 38.74/15.80 thf(135,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & (B != A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_252_dual__order_Ostrict__iff__order)).
% 38.74/15.80 thf(771,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) & ~ (B = A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[135])).
% 38.74/15.80 thf(351,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_119_diff__right__mono)).
% 38.74/15.80 thf(1289,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ TA @ (minus_minus @ TA @ A @ C) @ (minus_minus @ TA @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[351])).
% 38.74/15.80 thf(1,conjecture,(((ring_1_of_int @ real @ (abs_abs @ int @ m)) = (abs_abs @ real @ (finite1433825200ec_nth @ real @ n @ (minus_minus @ (finite_Cartesian_vec @ real @ n) @ x @ y) @ i)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0)).
% 38.74/15.80 thf(2,negated_conjecture,((~ ((ring_1_of_int @ real @ (abs_abs @ int @ m)) = (abs_abs @ real @ (finite1433825200ec_nth @ real @ n @ (minus_minus @ (finite_Cartesian_vec @ real @ n) @ x @ y) @ i))))),inference(neg_conjecture,[status(cth)],[1])).
% 38.74/15.80 thf(368,plain,((~ ((ring_1_of_int @ real @ (abs_abs @ int @ m)) = (abs_abs @ real @ (finite1433825200ec_nth @ real @ n @ (minus_minus @ (finite_Cartesian_vec @ real @ n) @ x @ y) @ i))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 38.74/15.80 thf(150,axiom,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ C @ D)))) => (ord_less_eq @ TA @ C @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_248_dense__ge__bounded)).
% 38.74/15.80 thf(813,plain,((! [TA: $tType]: ((dense_linorder @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((! [D:TA]: ((ord_less @ TA @ A @ D) => ((ord_less @ TA @ D @ B) => (ord_less_eq @ TA @ C @ D)))) => (ord_less_eq @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[150])).
% 38.74/15.80 thf(126,axiom,((! [TA: $tType]: ((wellorder @ TA) => (((?) @ TA) = (^ [A:(TA > $o)]: ? [B:TA]: ((A @ B) & ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (A @ C))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_190_exists__least__iff)).
% 38.74/15.80 thf(748,plain,((! [TA: $tType]: ((wellorder @ TA) => (((?) @ TA) = (^ [A:(TA > $o)]: ? [B:TA]: ((A @ B) & ! [C:TA]: ((ord_less @ TA @ C @ B) => (~ (A @ C))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[126])).
% 38.74/15.80 thf(256,axiom,((ring_1 @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Rings_Oring__1_35)).
% 38.74/15.80 thf(1062,plain,((ring_1 @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[256])).
% 38.74/15.80 thf(199,axiom,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_86_diff__strict__left__mono)).
% 38.74/15.80 thf(946,plain,((! [TA: $tType]: ((ordered_ab_group_add @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => (ord_less @ TA @ (minus_minus @ TA @ C @ B) @ (minus_minus @ TA @ C @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[199])).
% 38.74/15.80 thf(94,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_171_le__cases)).
% 38.74/15.80 thf(632,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) => (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[94])).
% 38.74/15.80 thf(139,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_246_dual__order_Ostrict__trans1)).
% 38.74/15.80 thf(781,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[139])).
% 38.74/15.80 thf(223,axiom,((! [TA: $tType,TB: $tType]: ((finite_finite @ TA) => (! [A:$o,B:(finite_Cartesian_vec @ TB @ TA),C:(finite_Cartesian_vec @ TB @ TA),D:TA]: (((A) => ((finite1433825200ec_nth @ TB @ TA @ (if @ (finite_Cartesian_vec @ TB @ TA) @ A @ B @ C) @ D) = (finite1433825200ec_nth @ TB @ TA @ B @ D))) & ((~ (A)) => ((finite1433825200ec_nth @ TB @ TA @ (if @ (finite_Cartesian_vec @ TB @ TA) @ A @ B @ C) @ D) = (finite1433825200ec_nth @ TB @ TA @ C @ D)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_27_cond__component)).
% 38.74/15.80 thf(995,plain,((! [TA: $tType,TB: $tType]: ((finite_finite @ TA) => (! [A:$o,B:(finite_Cartesian_vec @ TB @ TA),C:(finite_Cartesian_vec @ TB @ TA),D:TA]: (((A) => ((finite1433825200ec_nth @ TB @ TA @ (if @ (finite_Cartesian_vec @ TB @ TA) @ A @ B @ C) @ D) = (finite1433825200ec_nth @ TB @ TA @ B @ D))) & ((~ (A)) => ((finite1433825200ec_nth @ TB @ TA @ (if @ (finite_Cartesian_vec @ TB @ TA) @ A @ B @ C) @ D) = (finite1433825200ec_nth @ TB @ TA @ C @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[223])).
% 38.74/15.80 thf(78,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_160_dual__order_Otrans)).
% 38.74/15.80 thf(588,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less_eq @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[78])).
% 38.74/15.80 thf(336,axiom,((! [TA: $tType,TB: $tType]: ((minus @ TB) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_25_fun__diff__def)).
% 38.74/15.80 thf(1253,plain,((! [TA: $tType,TB: $tType]: ((minus @ TB) => ((minus_minus @ (TA > TB)) = (^ [A:(TA > TB),B:(TA > TB),C:TA]: (minus_minus @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[336])).
% 38.74/15.80 thf(120,axiom,((! [TA: $tType]: ((finite_finite @ TA) => (type @ TA)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subcl_Finite__Set_Ofinite___HOL_Otype)).
% 38.74/15.80 thf(731,plain,((! [TA: $tType]: ((finite_finite @ TA) => (type @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[120])).
% 38.74/15.80 thf(23,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_247_dual__order_Ostrict__trans2)).
% 38.74/15.80 thf(418,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less @ TA @ A @ B) => ((ord_less_eq @ TA @ C @ A) => (ord_less @ TA @ C @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 38.74/15.80 thf(69,axiom,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_242_order_Ostrict__trans1)).
% 38.74/15.80 thf(568,plain,((! [TA: $tType]: ((order @ TA) => (! [A:TA,B:TA,C:TA]: ((ord_less_eq @ TA @ A @ B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[69])).
% 38.74/15.80 thf(8,axiom,((! [TA: $tType]: (preorder @ (set @ TA)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Set_Oset___Orderings_Opreorder_5)).
% 38.74/15.80 thf(378,plain,((! [TA: $tType]: (preorder @ (set @ TA)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 38.74/15.80 thf(315,axiom,((no_bot @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Ono__bot_30)).
% 38.74/15.80 thf(1212,plain,((no_bot @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[315])).
% 38.74/15.80 thf(360,axiom,((! [A:(set @ real)]: ((? [B:real]: (member @ real @ B @ A)) => ((? [B:real]: ! [C:real]: ((member @ real @ C @ A) => (ord_less_eq @ real @ C @ B))) => (? [B:real]: (! [C:real]: ((member @ real @ C @ A) => (ord_less_eq @ real @ C @ B)) & ! [C:real]: ((! [D:real]: ((member @ real @ D @ A) => (ord_less_eq @ real @ D @ C))) => (ord_less_eq @ real @ B @ C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_157_complete__real)).
% 38.74/15.80 thf(1309,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)],[360])).
% 38.74/15.80 thf(246,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((ord_less_eq @ int @ (archimedean_ceiling @ TA @ A) @ (one_one @ int)) = (ord_less_eq @ TA @ A @ (one_one @ TA))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_107_ceiling__le__one)).
% 38.74/15.80 thf(1045,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA]: ((ord_less_eq @ int @ (archimedean_ceiling @ TA @ A) @ (one_one @ int)) = (ord_less_eq @ TA @ A @ (one_one @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[246])).
% 38.74/15.80 thf(347,axiom,((! [TA: $tType]: ((idom_abs_sgn @ TA) => (! [A:TA]: ((abs_abs @ TA @ (abs_abs @ TA @ A)) = (abs_abs @ TA @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_10_abs__abs)).
% 38.74/15.80 thf(1280,plain,((! [TA: $tType]: ((idom_abs_sgn @ TA) => (! [A:TA]: ((abs_abs @ TA @ (abs_abs @ TA @ A)) = (abs_abs @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[347])).
% 38.74/15.80 thf(209,axiom,((ord @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Oord_3)).
% 38.74/15.80 thf(967,plain,((ord @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[209])).
% 38.74/15.80 thf(151,axiom,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ B @ A) & (ord_less_eq @ TA @ A @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_159_dual__order_Oeq__iff)).
% 38.74/15.80 thf(818,plain,((! [TA: $tType]: ((order @ TA) => (((=) @ TA) = (^ [A:TA,B:TA]: ((ord_less_eq @ TA @ B @ A) & (ord_less_eq @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[151])).
% 38.74/15.80 thf(17,axiom,((finite_finite @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Finite__Set_Ofinite_44)).
% 38.74/15.80 thf(405,plain,((finite_finite @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 38.74/15.80 thf(288,axiom,((! [TA: $tType]: ((ring_char_0 @ TA) => (! [A:int,B:int]: (((ring_1_of_int @ TA @ A) = (ring_1_of_int @ TA @ B)) = (A = B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9_of__int__eq__iff)).
% 38.74/15.80 thf(1148,plain,((! [TA: $tType]: ((ring_char_0 @ TA) => (! [A:int,B:int]: (((ring_1_of_int @ TA @ A) = (ring_1_of_int @ TA @ B)) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[288])).
% 38.74/15.80 thf(334,axiom,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int,B:int]: ((ord_less @ TA @ (ring_1_of_int @ TA @ A) @ (ring_1_of_int @ TA @ B)) = (ord_less @ int @ A @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_48_of__int__less__iff)).
% 38.74/15.80 thf(1248,plain,((! [TA: $tType]: ((linordered_idom @ TA) => (! [A:int,B:int]: ((ord_less @ TA @ (ring_1_of_int @ TA @ A) @ (ring_1_of_int @ TA @ B)) = (ord_less @ int @ A @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[334])).
% 38.74/15.80 thf(169,axiom,((minus @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Groups_Ominus_36)).
% 38.74/15.80 thf(865,plain,((minus @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[169])).
% 38.74/15.80 thf(145,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((A != B) => ((~ (ord_less @ TA @ A @ B)) => (ord_less @ TA @ B @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_213_neqE)).
% 38.74/15.80 thf(801,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (A = B)) => ((~ (ord_less @ TA @ A @ B)) => (ord_less @ TA @ B @ A))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[145])).
% 38.74/15.80 thf(46,axiom,((order @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Orderings_Oorder_46)).
% 38.74/15.80 thf(506,plain,((order @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[46])).
% 38.74/15.80 thf(147,axiom,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ A @ B) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_183_le__funD)).
% 38.74/15.80 thf(807,plain,((! [TA: $tType,TB: $tType]: ((ord @ TB) => (! [A:(TA > TB),B:(TA > TB),C:TA]: ((ord_less_eq @ (TA > TB) @ (A) @ (B)) => (ord_less_eq @ TB @ (A @ C) @ (B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[147])).
% 38.74/15.80 thf(252,axiom,((ord @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Oord_34)).
% 38.74/15.80 thf(1056,plain,((ord @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[252])).
% 38.74/15.80 thf(206,axiom,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA,B:TA]: (ord_less_eq @ TA @ (abs_abs @ TA @ (minus_minus @ TA @ (abs_abs @ TA @ A) @ (abs_abs @ TA @ B))) @ (abs_abs @ TA @ (minus_minus @ TA @ A @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_131_abs__triangle__ineq3)).
% 38.74/15.80 thf(960,plain,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA,B:TA]: (ord_less_eq @ TA @ (abs_abs @ TA @ (minus_minus @ TA @ (abs_abs @ TA @ A) @ (abs_abs @ TA @ B))) @ (abs_abs @ TA @ (minus_minus @ TA @ A @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[206])).
% 38.74/15.80 thf(113,axiom,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_fun___Orderings_Opreorder)).
% 38.74/15.80 thf(720,plain,((! [TA: $tType,TB: $tType]: ((preorder @ TA) => (preorder @ (TB > TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[113])).
% 38.74/15.80 thf(183,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:int]: ((archimedean_ceiling @ TA @ (ring_1_of_int @ TA @ A)) = A))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_57_ceiling__of__int)).
% 38.74/15.80 thf(897,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:int]: ((archimedean_ceiling @ TA @ (ring_1_of_int @ TA @ A)) = A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[183])).
% 38.74/15.80 thf(134,axiom,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_178_order__subst2)).
% 38.74/15.80 thf(767,plain,((! [TA: $tType,TB: $tType]: (((order @ TA) & (order @ TB)) => (! [A:TB,B:TB,C:(TB > TA),D:TA]: ((ord_less_eq @ TB @ A @ B) => ((ord_less_eq @ TA @ (C @ B) @ D) => ((! [E:TB,F:TB]: ((ord_less_eq @ TB @ E @ F) => (ord_less_eq @ TA @ (C @ E) @ (C @ F)))) => (ord_less_eq @ TA @ (C @ A) @ D)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[134])).
% 38.74/15.80 thf(56,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = (ord_less_eq @ TA @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_229_not__less)).
% 38.74/15.80 thf(532,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less @ TA @ A @ B)) = (ord_less_eq @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[56])).
% 38.74/15.80 thf(258,axiom,((~ (! [A:int]: ((ring_1_of_int @ real @ A) != (minus_minus @ real @ (finite1433825200ec_nth @ real @ n @ x @ i) @ (finite1433825200ec_nth @ real @ n @ y @ i)))))),file('/export/starexec/sandbox2/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)).
% 38.74/15.80 thf(1065,plain,((~ (! [A:int]: ~ ((ring_1_of_int @ real @ A) = (minus_minus @ real @ (finite1433825200ec_nth @ real @ n @ x @ i) @ (finite1433825200ec_nth @ real @ n @ y @ i)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[258])).
% 38.74/15.80 thf(342,axiom,((! [TA: $tType,TB: $tType]: ((finite_finite @ TB) => (((=) @ (finite_Cartesian_vec @ TA @ TB)) = (^ [A:(finite_Cartesian_vec @ TA @ TB),B:(finite_Cartesian_vec @ TA @ TB)]: ! [C:TB]: ((finite1433825200ec_nth @ TA @ TB @ A @ C) = (finite1433825200ec_nth @ TA @ TB @ B @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_15_vec__eq__iff)).
% 38.74/15.80 thf(1268,plain,((! [TA: $tType,TB: $tType]: ((finite_finite @ TB) => (((=) @ (finite_Cartesian_vec @ TA @ TB)) = (^ [A:(finite_Cartesian_vec @ TA @ TB),B:(finite_Cartesian_vec @ TA @ TB)]: ! [C:TB]: ((finite1433825200ec_nth @ TA @ TB @ A @ C) = (finite1433825200ec_nth @ TA @ TB @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[342])).
% 38.74/15.80 thf(26,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA]: (A @ D @ D)) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_189_linorder__less__wlog)).
% 38.74/15.80 thf(427,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:(TA > (TA > $o)),B:TA,C:TA]: ((! [D:TA,E:TA]: ((ord_less @ TA @ D @ E) => (A @ D @ E))) => ((! [D:TA]: (A @ D @ D)) => ((! [D:TA,E:TA]: ((A @ E @ D) => (A @ D @ E))) => (A @ B @ C)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 38.74/15.80 thf(167,axiom,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (((finite_finite @ TA) & (finite_finite @ TC)) => (! [A:(TB > TD),B:(finite_Cartesian_vec @ (finite_Cartesian_vec @ TB @ TA) @ TC),C:TC,D:TA]: ((finite1433825200ec_nth @ TD @ TA @ (finite1433825200ec_nth @ (finite_Cartesian_vec @ TD @ TA) @ TC @ (finite1614961371matrix @ TB @ TD @ TA @ TC @ A @ B) @ C) @ D) = (A @ (finite1433825200ec_nth @ TB @ TA @ (finite1433825200ec_nth @ (finite_Cartesian_vec @ TB @ TA) @ TC @ B @ C) @ D))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_28_nth__map__matrix)).
% 38.74/15.80 thf(860,plain,((! [TA: $tType,TB: $tType,TC: $tType,TD: $tType]: (((finite_finite @ TA) & (finite_finite @ TC)) => (! [A:(TB > TD),B:(finite_Cartesian_vec @ (finite_Cartesian_vec @ TB @ TA) @ TC),C:TC,D:TA]: ((finite1433825200ec_nth @ TD @ TA @ (finite1433825200ec_nth @ (finite_Cartesian_vec @ TD @ TA) @ TC @ (finite1614961371matrix @ TB @ TD @ TA @ TC @ (A) @ B) @ C) @ D) = (A @ (finite1433825200ec_nth @ TB @ TA @ (finite1433825200ec_nth @ (finite_Cartesian_vec @ TB @ TA) @ TC @ B @ C) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[167])).
% 38.74/15.80 thf(222,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:int,B:TA]: ((ord_less @ int @ A @ (archimedean_ceiling @ TA @ B)) = (ord_less @ TA @ (ring_1_of_int @ TA @ A) @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_71_less__ceiling__iff)).
% 38.74/15.80 thf(992,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:int,B:TA]: ((ord_less @ int @ A @ (archimedean_ceiling @ TA @ B)) = (ord_less @ TA @ (ring_1_of_int @ TA @ A) @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[222])).
% 38.74/15.80 thf(115,axiom,((group_add @ numeral_num1)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Numeral__Type_Onum1___Groups_Ogroup__add_45)).
% 38.74/15.80 thf(723,plain,((group_add @ numeral_num1)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[115])).
% 38.74/15.80 thf(225,axiom,((! [TA: $tType,TB: $tType]: (((one @ TA) & (finite_finite @ TB)) => ((finite_Cartesian_vec2 @ TA @ TB @ (one_one @ TA)) = (one_one @ (finite_Cartesian_vec @ TA @ TB)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_55_vec__1)).
% 38.74/15.80 thf(1004,plain,((! [TA: $tType,TB: $tType]: (((one @ TA) & (finite_finite @ TB)) => ((finite_Cartesian_vec2 @ TA @ TB @ (one_one @ TA)) = (one_one @ (finite_Cartesian_vec @ TA @ TB)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[225])).
% 38.74/15.80 thf(106,axiom,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_244_order_Oorder__iff__strict)).
% 38.74/15.80 thf(691,plain,((! [TA: $tType]: ((order @ TA) => ((ord_less_eq @ TA) = (^ [A:TA,B:TA]: ((ord_less @ TA @ A @ B) | (A = B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[106])).
% 38.74/15.80 thf(172,axiom,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ int @ (archimedean_ceiling @ TA @ A) @ (archimedean_ceiling @ TA @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_108_ceiling__mono)).
% 38.74/15.80 thf(871,plain,((! [TA: $tType]: ((archim1727834104eiling @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) => (ord_less_eq @ int @ (archimedean_ceiling @ TA @ A) @ (archimedean_ceiling @ TA @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[172])).
% 38.74/15.80 thf(276,axiom,((! [TA: $tType]: ((real_V55928688vector @ TA) => (! [A:TA]: ((abs_abs @ real @ (real_V1127708846m_norm @ TA @ A)) = (real_V1127708846m_norm @ TA @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_52_abs__norm__cancel)).
% 38.74/15.80 thf(1120,plain,((! [TA: $tType]: ((real_V55928688vector @ TA) => (! [A:TA]: ((abs_abs @ real @ (real_V1127708846m_norm @ TA @ A)) = (real_V1127708846m_norm @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[276])).
% 38.74/15.80 thf(269,axiom,((real_V55928688vector @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Real__Vector__Spaces_Oreal__normed__vector)).
% 38.74/15.80 thf(1093,plain,((real_V55928688vector @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[269])).
% 38.74/15.80 thf(13,axiom,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_203_ord__eq__less__trans)).
% 38.74/15.80 thf(395,plain,((! [TA: $tType]: ((ord @ TA) => (! [A:TA,B:TA,C:TA]: ((A = B) => ((ord_less @ TA @ B @ C) => (ord_less @ TA @ A @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 38.74/15.80 thf(327,axiom,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ (abs_abs @ TA @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_122_abs__ge__self)).
% 38.74/15.80 thf(1236,plain,((! [TA: $tType]: ((ordere142940540dd_abs @ TA) => (! [A:TA]: (ord_less_eq @ TA @ A @ (abs_abs @ TA @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[327])).
% 38.74/15.80 thf(218,axiom,((dense_order @ real)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Real_Oreal___Orderings_Odense__order)).
% 38.74/15.80 thf(987,plain,((dense_order @ real)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[218])).
% 38.74/15.80 thf(39,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_228_not__le)).
% 38.74/15.80 thf(486,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((~ (ord_less_eq @ TA @ A @ B)) = (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 38.74/15.80 thf(362,axiom,((order @ int)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Int_Oint___Orderings_Oorder_2)).
% 38.74/15.80 thf(1320,plain,((order @ int)),inference(defexp_and_simp_and_etaexpand,[status(thm)],[362])).
% 38.74/15.80 thf(228,axiom,((! [TA: $tType,TB: $tType]: (((minus @ TA) & (finite_finite @ TB)) => (! [A:TA,B:TA]: ((finite_Cartesian_vec2 @ TA @ TB @ (minus_minus @ TA @ A @ B)) = (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ (finite_Cartesian_vec2 @ TA @ TB @ A) @ (finite_Cartesian_vec2 @ TA @ TB @ B))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_30_vec__sub)).
% 38.74/15.80 thf(1009,plain,((! [TA: $tType,TB: $tType]: (((minus @ TA) & (finite_finite @ TB)) => (! [A:TA,B:TA]: ((finite_Cartesian_vec2 @ TA @ TB @ (minus_minus @ TA @ A @ B)) = (minus_minus @ (finite_Cartesian_vec @ TA @ TB) @ (finite_Cartesian_vec2 @ TA @ TB @ A) @ (finite_Cartesian_vec2 @ TA @ TB @ B))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[228])).
% 38.74/15.80 thf(302,axiom,((! [TA: $tType,TB: $tType]: (((order @ TB) & (finite_finite @ TA)) => (order @ (finite_Cartesian_vec @ TB @ TA))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tcon_Finite__Cartesian__Product_Ovec___Orderings_Oorder_64)).
% 38.74/15.80 thf(1184,plain,((! [TA: $tType,TB: $tType]: (((order @ TB) & (finite_finite @ TA)) => (order @ (finite_Cartesian_vec @ TB @ TA))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[302])).
% 38.74/15.80 thf(59,axiom,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less @ TA @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_238_le__less__linear)).
% 38.74/15.80 thf(543,plain,((! [TA: $tType]: ((linorder @ TA) => (! [A:TA,B:TA]: ((ord_less_eq @ TA @ A @ B) | (ord_less @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[59])).
% 38.74/15.80 thf(41,axiom,((! [TA: $tType]: ((one @ TA) => (! [A:TA]: (((one_one @ TA) = A) = (A = (one_one @ TA))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_69_one__reorient)).
% 38.74/15.80 thf(491,plain,((! [TA: $tType]: ((one @ TA) => (! [A:TA]: (((one_one @ TA) = A) = (A = (one_one @ TA))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 38.74/15.80 thf(80,axiom,((! [TA: $tType]: ((real_V2090557954_space @ TA) => ((real_V2000881966t_dist @ TA) = (^ [A:TA,B:TA]: (real_V2000881966t_dist @ TA @ B @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_76_dist__commute)).
% 38.74/15.80 thf(592,plain,((! [TA: $tType]: ((real_V2090557954_space @ TA) => ((real_V2000881966t_dist @ TA) = (^ [A:TA,B:TA]: (real_V2000881966t_dist @ TA @ B @ A)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[80])).
% 38.74/15.80 thf(30,axiom,((! [TA: $tType,TB: $tType]: ((finite_finite @ TB) => (! [A:TA,B:TA]: (((finite_Cartesian_vec2 @ TA @ TB @ A) = (finite_Cartesian_vec2 @ TA @ TB @ B)) = (A = B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_39_vec__eq)).
% 38.74/15.80 thf(454,plain,((! [TA: $tType,TB: $tType]: ((finite_finite @ TB) => (! [A:TA,B:TA]: (((finite_Cartesian_vec2 @ TA @ TB @ A) = (finite_Cartesian_vec2 @ TA @ TB @ B)) = (A = B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 38.74/15.80 thf(212,axiom,((! [TA: $tType]: ((archim1804426504_field @ TA) => (! [A:TA]: ? [B:int]: (ord_less_eq @ TA @ A @ (ring_1_of_int @ TA @ B)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_125_ex__le__of__int)).
% 38.74/15.80 thf(972,plain,((! [TA: $tType]: ((archim1804426504_field @ TA) => (! [A:TA]: ? [B:int]: (ord_less_eq @ TA @ A @ (ring_1_of_int @ TA @ B)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[212])).
% 38.74/15.80 thf(1707,plain,(($false)),inference(e,[status(thm)],[1322,809,479,846,893,518,1295,1083,962,1211,873,677,523,1158,582,762,741,1073,878,511,1078,384,1137,550,500,715,1275,1233,913,1063,1222,1164,797,1001,709,1228,1243,1127,1287,570,1298,372,1264,751,1055,724,1323,619,1059,1132,559,1247,1319,1013,448,881,416,1040,376,623,646,834,514,1151,1283,1302,756,1020,574,1051,821,1169,634,877,956,866,774,1201,507,602,981,411,988,1242,849,1206,380,942,678,529,793,1306,761,810,381,1057,1163,1274,910,894,1091,1123,392,424,729,1238,1042,952,1217,598,1032,625,852,1178,461,1210,1027,1291,842,974,1012,916,467,566,484,682,1195,1089,874,1259,948,1017,1227,725,403,1096,869,989,857,783,420,1118,471,884,1160,933,537,642,489,1214,901,686,1075,1016,590,1155,547,837,1324,1099,1266,1192,457,984,779,371,605,1086,1241,1054,1035,1071,1026,953,586,888,906,965,1251,1219,745,573,733,1154,402,1125,579,413,562,904,975,1007,694,577,711,1256,545,572,1271,787,713,804,1224,445,936,764,831,1117,1048,990,451,1144,737,1043,616,900,406,863,1175,890,631,758,552,535,1325,1029,626,1293,1061,494,1080,943,1022,1198,399,959,1245,563,685,521,1171,1213,827,851,1102,722,675,1304,1166,531,680,374,1277,1134,516,939,1145,754,1203,1208,968,1181,823,776,855,690,1025,1070,971,739,409,1230,1053,1300,791,717,502,840,1262,463,951,1130,907,1188,1186,1038,370,1141,1023,613,1284,600,727,1008,595,497,1094,978,1140,845,465,627,556,931,1321,903,1216,1189,771,1289,368,813,748,1062,946,632,781,995,588,1253,731,418,568,378,1212,1309,1045,1280,967,818,405,1148,1248,865,801,506,807,1056,960,720,897,767,532,1065,1268,427,860,992,723,1004,691,871,1120,1093,395,1236,987,486,1320,1009,1184,543,491,592,454,972])).
% 38.74/15.80 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 38.74/15.80 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------