%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SWW216+1 : TPTP v9.2.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue May 12 07:16:37 PM UTC 2026 % Result : Theorem 2.96s 3.44s % Output : Proof 2.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW216+1 : TPTP v9.2.1. Released v5.2.0. % 0.00/0.12 % Command : g4plus.sh /export/starexec/sandbox2/benchmark/theBenchmark.p 300 % 0.15/0.33 % Computer : n015.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Mon May 11 14:27:32 EDT 2026 % 0.15/0.33 % CPUTime : % 2.96/3.44 % SZS status Theorem % 2.96/3.44 % SZS output start Proof % 2.96/3.45 % 2.96/3.45 =============================================================== % 2.96/3.45 TPTP Problem: conj_0 (conjecture with 1249 axiom(s)) % 2.96/3.45 Axioms: [fact_ext,fact_m_I1_J,fact_H_I3_J,fact_assms,fact_H_I1_J,fact_H_I2_J,fact_dm_I2_J,fact_d_I3_J,fact_dm_I1_J,fact_em0,fact_real__mult__commute,fact_real__mult__assoc,fact_d_I1_J,fact_times_Oidem,fact_mult__idem,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,fact_mult__left__idem,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,fact_d_I2_J,fact_one0,fact_real__zero__not__eq__one,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I12_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I11_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J,fact_real__mult__1,fact_real__mult__left__cancel,fact_real__mult__right__cancel,fact_real__mult__less__mono2,fact_real__mult__order,fact_real__mult__less__iff1,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I13_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I15_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I14_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I16_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I17_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I18_J,fact__096_B_Bthesis_O_A_I_B_Bd_O_A_091_124_A0_A_060_Ad_059_Ad_A_060_A1_059_Ad_A_060_Ae_A_P_Am_A_124_093_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096,fact__096EX_Aea_0620_O_Aea_A_060_A1_A_G_Aea_A_060_Ae_A_P_Am_096,fact_divide__strict__left__mono__neg,fact_divide__strict__left__mono,fact_neg__divide__less__eq,fact_neg__less__divide__eq,fact_mult__imp__less__div__pos,fact_mult__imp__div__pos__less,fact_pos__divide__less__eq,fact_pos__less__divide__eq,fact_divide__less__eq,fact_less__divide__eq,fact_times__divide__times__eq,fact_divide__strict__right__mono__neg,fact_divide__strict__right__mono,fact_divide__neg__neg,fact_divide__neg__pos,fact_divide__pos__neg,fact_divide__pos__pos,fact_divide__less__0__iff,fact_zero__less__divide__iff,fact_frac__eq__eq,fact_mult__divide__mult__cancel__left,fact_mult__divide__mult__cancel__right,fact_divide__eq__eq,fact_eq__divide__eq,fact_not__real__square__gt__zero,fact_right__inverse__eq,fact_divide__self,fact_divide__self__if,fact_eq__divide__imp,fact_divide__eq__imp,fact_nonzero__divide__eq__eq,fact_nonzero__eq__divide__eq,fact_less__1__mult,fact_zero__less__one,fact_not__one__less__zero,fact_linorder__neqE__linordered__idom,fact_divisors__zero,fact_no__zero__divisors,fact_mult__eq__0__iff,fact_mult__zero__right,fact_mult__zero__left,fact_one__neq__zero,fact_zero__neq__one,fact_divide__zero__left,fact_divide__zero,fact_times__divide__eq__right,fact_divide__1,fact_real__divide__square__eq,fact_mult__strict__left__mono__neg,fact_mult__strict__right__mono__neg,fact_comm__mult__strict__left__mono,fact_mult__strict__left__mono,fact_mult__strict__right__mono,fact_mult__neg__neg,fact_mult__neg__pos,fact_mult__less__cancel__left__neg,fact_zero__less__mult__pos2,fact_zero__less__mult__pos,fact_mult__pos__neg2,fact_mult__pos__neg,fact_mult__pos__pos,fact_mult__less__cancel__left__pos,fact_mult__less__cancel__left__disj,fact_mult__less__cancel__right__disj,fact_not__square__less__zero,fact_d1_I2_J,fact_divide_Ozero,fact_mult_Ocomm__neutral,fact_mult__1__right,fact_mult__1,fact_mult__1__left,fact_mult__right_Ozero,fact_mult_Ozero__right,fact_mult__left_Ozero,fact_mult_Ozero__left,fact_real__le__refl,fact_real__le__linear,fact_real__le__trans,fact_real__le__antisym,fact_real__less__def,fact_less__eq__real__def,fact_split__mult__neg__le,fact_split__mult__pos__le,fact_mult__mono,fact_mult__mono_H,fact_mult__left__mono__neg,fact_mult__right__mono__neg,fact_comm__mult__left__mono,fact_mult__left__mono,fact_mult__right__mono,fact_mult__nonpos__nonpos,fact_mult__nonpos__nonneg,fact_mult__nonneg__nonpos2,fact_mult__nonneg__nonpos,fact_mult__nonneg__nonneg,fact_mult__le__0__iff,fact_zero__le__mult__iff,fact_zero__le__square,fact_zero__le__one,fact_not__one__le__zero,fact_divide__right__mono__neg,fact_divide__right__mono,fact_divide__le__0__iff,fact_zero__le__divide__iff,fact_real__0__le__divide__iff,fact_mult__le__cancel__left__pos,fact_mult__le__cancel__left__neg,fact_mult__strict__mono,fact_mult__strict__mono_H,fact_mult__less__le__imp__less,fact_mult__le__less__imp__less,fact_mult__right__less__imp__less,fact_mult__less__imp__less__right,fact_mult__left__less__imp__less,fact_mult__less__imp__less__left,fact_mult__right__le__imp__le,fact_mult__left__le__imp__le,fact_mult__left__le__one__le,fact_mult__right__le__one__le,fact_divide__nonpos__neg,fact_divide__nonpos__pos,fact_frac__le,fact_frac__less,fact_frac__less2,fact_divide__nonneg__neg,fact_divide__nonneg__pos,fact_zero__reorient,fact_real__mult__le__cancel__iff1,fact_real__mult__le__cancel__iff2,fact_ab__semigroup__mult__class_Omult__ac_I1_J,fact_one__reorient,fact_le__divide__eq,fact_divide__le__eq,fact_pos__le__divide__eq,fact_pos__divide__le__eq,fact_mult__imp__div__pos__le,fact_mult__imp__le__div__pos,fact_neg__le__divide__eq,fact_neg__divide__le__eq,fact_divide__left__mono,fact_divide__left__mono__neg,fact_order__refl,fact_linorder__not__less,fact_linorder__not__le,fact_linorder__le__less__linear,fact_order__less__le,fact_less__le__not__le,fact_order__le__less,fact_leI,fact_not__leE,fact_le__fun__def,fact_linorder__linear,fact_order__eq__iff,fact_order__eq__refl,fact_le__funD,fact_order__antisym__conv,fact_ord__eq__le__trans,fact_xt1_I3_J,fact_ord__le__eq__trans,fact_xt1_I4_J,fact_order__antisym,fact_order__trans,fact_xt1_I5_J,fact_xt1_I6_J,fact_le__funE,fact_linorder__le__cases,fact_linorder__cases,fact_order__less__asym,fact_xt1_I10_J,fact_order__less__trans,fact_xt1_I2_J,fact_ord__less__eq__trans,fact_xt1_I1_J,fact_ord__eq__less__trans,fact_xt1_I9_J,fact_order__less__asym_H,fact_order__less__imp__not__eq2,fact_order__less__imp__not__eq,fact_order__less__imp__not__less,fact_order__less__not__sym,fact_less__imp__neq,fact_linorder__neqE,fact_linorder__antisym__conv3,fact_linorder__less__linear,fact_not__less__iff__gr__or__eq,fact_linorder__neq__iff,fact_order__less__irrefl,fact_xt1_I8_J,fact_order__le__less__trans,fact_xt1_I7_J,fact_order__less__le__trans,fact_xt1_I11_J,fact_order__le__neq__trans,fact_order__le__imp__less__or__eq,fact_linorder__antisym__conv2,fact_order__less__imp__le,fact_leD,fact_xt1_I12_J,fact_order__neq__le__trans,fact_linorder__antisym__conv1,fact_field__le__mult__one__interval,fact_convex__bound__lt,fact_convex__bound__le,fact_one__le__inverse__iff,fact_inverse__less__1__iff,fact_one__le__inverse,fact_sgn__1__pos,fact_sgn__pos,fact_less__fun__def,fact_inverse__inverse__eq,fact_sgn__sgn,fact_inverse__eq__iff__eq,fact_inverse__eq__imp__eq,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I24_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I22_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I25_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I21_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I23_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I20_J,fact_ab__semigroup__add__class_Oadd__ac_I1_J,fact_add__left__cancel,fact_add__right__cancel,fact_add__left__imp__eq,fact_add__imp__eq,fact_add__right__imp__eq,fact_inverse__add,fact_division__ring__inverse__add,fact_field__inverse__zero,fact_nonzero__inverse__eq__imp__eq,fact_inverse__zero__imp__zero,fact_nonzero__inverse__inverse__eq,fact_nonzero__imp__inverse__nonzero,fact_inverse__nonzero__iff__nonzero,fact_inverse__zero,fact_inverse__mult__distrib,fact_inverse__eq__1__iff,fact_inverse__1,fact_inverse__divide,fact_INVERSE__ZERO,fact_add_Ocomm__neutral,fact_add__0__right,fact_double__zero__sym,fact_add__0,fact_add__0__left,fact_add__0__iff,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I6_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I5_J,fact_add__le__imp__le__left,fact_add__le__imp__le__right,fact_add__mono,fact_add__left__mono,fact_add__right__mono,fact_add__le__cancel__left,fact_add__le__cancel__right,fact_add__less__cancel__right,fact_add__less__cancel__left,fact_add__strict__right__mono,fact_add__strict__left__mono,fact_add__strict__mono,fact_add__less__imp__less__right,fact_add__less__imp__less__left,fact_mult_Oadd__right,fact_mult__right_Oadd,fact_mult_Oadd__left,fact_mult__left_Oadd,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I34_J,fact_crossproduct__noteq,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I8_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I1_J,fact_crossproduct__eq,fact_comm__semiring__class_Odistrib,fact_combine__common__factor,fact_divide_Oadd,fact_add__divide__distrib,fact_real__add__left__mono,fact_real__add__mult__distrib,fact_sgn__zero__iff,fact_sgn__zero,fact_sgn0,fact_sgn__0__0,fact_sgn__mult,fact_sgn__times,fact_sgn__one,fact_inverse__nonpositive__iff__nonpositive,fact_inverse__nonnegative__iff__nonnegative,fact_inverse__less__imp__less__neg,fact_inverse__less__imp__less,fact_inverse__negative__imp__negative,fact_less__imp__inverse__less__neg,fact_less__imp__inverse__less,fact_negative__imp__inverse__negative,fact_inverse__positive__imp__positive,fact_positive__imp__inverse__positive,fact_inverse__negative__iff__negative,fact_inverse__positive__iff__positive,fact_nonzero__inverse__mult__distrib,fact_inverse__unique,fact_field__divide__inverse,fact_divide__inverse,fact_field__class_Onormalizing__field__rules_I2_J,fact_inverse__eq__divide,fact_add__nonpos__nonpos,fact_add__increasing2,fact_add__increasing,fact_add__nonneg__eq__0__iff,fact_add__nonneg__nonneg,fact_double__add__le__zero__iff__single__add__le__zero,fact_zero__le__double__add__iff__zero__le__single__add,fact_add__neg__neg,fact_add__pos__pos,fact_double__add__less__zero__iff__single__add__less__zero,fact_zero__less__double__add__iff__zero__less__single__add,fact_pos__add__strict,fact_add__less__le__mono,fact_add__le__less__mono,fact_add__scale__eq__noteq,fact_less__add__one,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I2_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I3_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J,fact_divide__real__def,fact_real__divide__def,fact_real__two__squares__add__zero__iff,fact_sgn__less,fact_sgn__greater,fact_inverse__le__imp__le__neg,fact_inverse__le__imp__le,fact_le__imp__inverse__le__neg,fact_le__imp__inverse__le,fact_inverse__le__1__iff,fact_one__less__inverse,fact_one__less__inverse__iff,fact_field__inverse,fact_left__inverse,fact_right__inverse,fact_nonzero__inverse__eq__divide,fact_add__nonpos__neg,fact_add__neg__nonpos,fact_add__strict__increasing2,fact_add__strict__increasing,fact_add__nonneg__pos,fact_add__pos__nonneg,fact_zero__less__two,fact_add__frac__eq,fact_divide__add__eq__iff,fact_add__frac__num,fact_add__divide__eq__iff,fact_add__num__frac,fact_real__mult__inverse__left,fact_gt__half__sum,fact_less__half__sum,fact_real__sgn__pos,fact_not__sum__squares__lt__zero,fact_sum__squares__gt__zero__iff,fact_sum__squares__le__zero__iff,fact_sum__squares__ge__zero,fact_real__mult__inverse__cancel2,fact_real__mult__inverse__cancel,fact_sum__squares__eq__zero__iff,fact_even__less__0__iff,fact_double__eq__0__iff,fact_field__le__epsilon,fact_ln__add__one__self__le__self,fact_ln__mult,fact_ln__less__cancel__iff,fact_ln__inj__iff,fact_ln__less__self,fact_ln__one,fact_ln__le__cancel__iff,fact_ln__ge__zero,fact_ln__gt__zero__imp__gt__one,fact_ln__less__zero,fact_ln__less__zero__iff,fact_ln__eq__zero__iff,fact_ln__gt__zero__iff,fact_ln__gt__zero,fact_ln__ge__zero__imp__ge__one,fact_ln__ge__zero__iff,fact_divide__le__eq__number__of1,fact_divide__le__eq__number__of,fact_le__divide__eq__number__of,fact_le__divide__eq__number__of1,fact_DERIV__ln__divide,fact_add__number__of__left,fact_add__number__of__eq,fact_number__of__add,fact_less__number__of,fact_eq__number__of,fact_number__of__reorient,fact_mult__number__of__left,fact_arith__simps_I32_J,fact_number__of__mult,fact_le__number__of,fact_le__number__of__eq__not__less,fact_left__distrib__number__of,fact_right__distrib__number__of,fact_eq__divide__eq__number__of1,fact_eq__divide__eq__number__of,fact_divide__eq__eq__number__of,fact_divide__eq__eq__number__of1,fact_inverse__eq__divide__number__of,fact_divide__less__eq__number__of1,fact_divide__less__eq__number__of,fact_less__divide__eq__number__of,fact_less__divide__eq__number__of1,fact_DERIV__ln,fact_DERIV__cmult__Id,fact_number__of__succ,fact_sgn__real__def,fact_real__sgn__def,fact_exp__ge__add__one__self__aux,fact_exp__less__mono,fact_plus__numeral__code_I9_J,fact_less__number__of__int__code,fact_times__numeral__code_I5_J,fact_minus__number__of__mult,fact_number__of__minus,fact_arith__simps_I30_J,fact_less__eq__number__of__int__code,fact_sgn__minus,fact_exp__le__cancel__iff,fact_exp__minus,fact_exp__inj__iff,fact_minus__zero,fact_neg__0__equal__iff__equal,fact_equal__neg__zero,fact_neg__equal__0__iff__equal,fact_neg__equal__zero,fact_le__minus__iff,fact_minus__le__iff,fact_neg__le__iff__le,fact_le__imp__neg__le,fact_compl__mono,fact_compl__le__compl__iff,fact_neg__less__iff__less,fact_minus__less__iff,fact_less__minus__iff,fact_square__eq__iff,fact_minus__mult__minus,fact_minus__mult__commute,fact_minus__mult__left,fact_minus__mult__right,fact_mult__left_Ominus,fact_mult_Ominus__left,fact_mult__right_Ominus,fact_mult_Ominus__right,fact_minus__add__cancel,fact_add__minus__cancel,fact_minus__add,fact_minus__add__distrib,fact_minus__divide__left,fact_minus__divide__right,fact_minus__divide__divide,fact_divide_Ominus,fact_inverse__minus__eq,fact_double__compl,fact_uminus__apply,fact_compl__eq__compl__iff,fact_minus__minus,fact_equation__minus__iff,fact_minus__equation__iff,fact_neg__equal__iff__equal,fact_exp__less__cancel__iff,fact_exp__less__cancel,fact_zle__antisym,fact_zle__trans,fact_zle__linear,fact_zle__refl,fact_zmult__1,fact_zmult__1__right,fact_zmult__assoc,fact_zmult__commute,fact_zless__linear,fact_zmult__zless__mono2,fact_pos__zmult__eq__1__iff,fact_int__0__less__1,fact_odd__nonzero,fact_succ__def,fact_zadd__0,fact_zadd__0__right,fact_zless__add1__eq,fact_odd__less__0,fact_zadd__strict__right__mono,fact_zadd__commute,fact_zadd__left__commute,fact_zadd__assoc,fact_zadd__zmult__distrib,fact_zadd__zmult__distrib2,fact_int__one__le__iff__zero__less,fact_zle__add1__eq__le,fact_add1__zle__eq,fact_le__imp__0__less,fact_zless__imp__add1__zle,fact_zadd__zless__mono,fact_zless__le,fact_zadd__left__mono,fact_ln__exp,fact_exp__ln__eq,fact_ln__unique,fact_exp__not__eq__zero,fact_DERIV__exp,fact_minus__le__self__iff,fact_neg__le__0__iff__le,fact_le__minus__self__iff,fact_neg__0__le__iff__le,fact_neg__less__nonneg,fact_neg__less__0__iff__less,fact_neg__0__less__iff__less,fact_less__minus__self__iff,fact_add__eq__0__iff,fact_right__minus,fact_eq__neg__iff__add__eq__0,fact_left__minus,fact_ab__left__minus,fact_minus__unique,fact_comm__ring__1__class_Onormalizing__ring__rules_I1_J,fact_square__eq__1__iff,fact_nonzero__minus__divide__divide,fact_nonzero__minus__divide__right,fact_nonzero__inverse__minus__eq,fact_real__minus__mult__self__le,fact_real__add__eq__0__iff,fact_real__add__minus__iff,fact_exp__ge__zero,fact_not__exp__le__zero,fact_exp__gt__zero,fact_not__exp__less__zero,fact_exp__eq__one__iff,fact_exp__zero,fact_exp__add,fact_mult__exp__exp,fact_real__add__le__0__iff,fact_real__0__le__add__iff,fact_real__add__less__0__iff,fact_real__0__less__add__iff,fact_exp__le__one__iff,fact_one__le__exp__iff,fact_exp__gt__one,fact_exp__less__one__iff,fact_one__less__exp__iff,fact_exp__ln,fact_exp__ln__iff,fact_DERIV__unique,fact_DERIV__cong,fact_Deriv_Olemma__DERIV__subst,fact_sgn__if,fact_sgn__neg,fact_sgn__1__neg,fact_ln__inverse,fact_zdiv__mono2__neg__lemma,fact_unique__quotient__lemma__neg,fact_zdiv__mono2__lemma,fact_unique__quotient__lemma,fact_minus__numeral__code_I5_J,fact_zminus__0,fact_zminus__zminus,fact_zmult__zminus,fact_zsgn__def,fact_zadd__zminus__inverse2,fact_zminus__zadd__distrib,fact_int__0__neq__1,fact_number__of__is__id,fact_self__quotient__aux2,fact_self__quotient__aux1,fact_q__pos__lemma,fact_q__neg__lemma,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I2_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I1_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I6_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I5_J,fact_eq__number__of__eq,fact_DERIV__pos__inc__right,fact_DERIV__neg__dec__right,fact_iszero__def,fact_iszero__0,fact_not__iszero__1,fact_eq__special_I3_J,fact_eq__special_I1_J,fact_number__of__pred,fact_less__nat__number__of,fact_less__0__number__of,fact_eq__0__number__of,fact_eq__number__of__0,fact_le__nat__number__of,fact_minus__Pls,fact_Pls__def,fact_semiring__norm_I113_J,fact_nat__number__of__Pls,fact_add__Pls__right,fact_add__Pls,fact_rel__simps_I2_J,fact_mult__Pls,fact_rel__simps_I19_J,fact_succ__pred,fact_semiring__norm_I112_J,fact_number__of__Pls,fact_add__numeral__0__right,fact_add__numeral__0,fact_bin__less__0__simps_I1_J,fact_zero__is__num__zero,fact_add__nat__number__of,fact_nat__number__of__mult__left,fact_mult__nat__number__of,fact_iszero__Numeral0,fact_nat__1__add__number__of,fact_nat__number__of__add__1,fact_le__iff__pred__less,fact_divide__Numeral0,fact_le__special_I1_J,fact_le__special_I3_J,fact_less__special_I1_J,fact_less__special_I3_J,fact_number__of2,fact_eq__special_I4_J,fact_eq__special_I2_J,fact_Numeral1__eq1__nat,fact_nat__numeral__1__eq__1,fact_rel__simps_I39_J,fact_rel__simps_I46_J,fact_less__eq__int__code_I16_J,fact_rel__simps_I34_J,fact_rel__simps_I17_J,fact_less__int__code_I16_J,fact_rel__simps_I51_J,fact_rel__simps_I22_J,fact_bin__less__0__simps_I4_J,fact_rel__simps_I12_J,fact_Bit1__def,fact_minus__Bit1,fact_iszero__number__of__Bit1,fact_succ__Pls,fact_number__of__Bit1,fact_mult__numeral__1,fact_mult__numeral__1__right,fact_numeral__1__eq__1,fact_semiring__norm_I110_J,fact_divide__Numeral1,fact_divide__numeral__1,fact_inverse__numeral__1,fact_rel__simps_I29_J,fact_rel__simps_I5_J,fact_one__is__num__one,fact_not__iszero__Numeral1,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I8_J,fact_le__special_I2_J,fact_le__special_I4_J,fact_less__special_I2_J,fact_less__special_I4_J,fact_add__special_I3_J,fact_add__special_I2_J,fact_le0,fact_less__zeroE,fact_mult__le__cancel1,fact_less__not__refl,fact_nat__neq__iff,fact_linorder__neqE__nat,fact_less__irrefl__nat,fact_less__not__refl2,fact_less__not__refl3,fact_nat__less__cases,fact_nat__add__commute,fact_nat__add__left__commute,fact_nat__add__assoc,fact_nat__add__left__cancel,fact_nat__add__right__cancel,fact_le__antisym,fact_le__trans,fact_eq__imp__le,fact_nat__le__linear,fact_le__refl,fact_nat__mult__assoc,fact_nat__mult__commute,fact_not__less0,fact_neq0__conv,fact_less__nat__zero__code,fact_gr__implies__not0,fact_gr0I,fact_add__eq__self__zero,fact_add__is__0,fact_Nat_Oadd__0__right,fact_plus__nat_Oadd__0,fact_less__eq__nat_Osimps_I1_J,fact_le__0__eq,fact_mult__cancel2,fact_mult__cancel1,fact_mult__is__0,fact_mult__0__right,fact_mult__0,fact_add__lessD1,fact_less__add__eq__less,fact_add__less__mono,fact_add__less__mono1,fact_trans__less__add2,fact_trans__less__add1,fact_nat__add__left__cancel__less,fact_not__add__less2,fact_not__add__less1,fact_less__or__eq__imp__le,fact_le__neq__implies__less,fact_less__imp__le__nat,fact_le__eq__less__or__eq,fact_nat__less__le,fact_le__add2,fact_le__add1,fact_le__iff__add,fact_nat__add__left__cancel__le,fact_trans__le__add1,fact_trans__le__add2,fact_add__le__mono1,fact_add__le__mono,fact_add__leD2,fact_add__leD1,fact_add__leE,fact_add__mult__distrib,fact_add__mult__distrib2,fact_le__square,fact_le__cube,fact_mult__le__mono1,fact_mult__le__mono2,fact_mult__le__mono,fact_nat__mult__eq__1__iff,fact_nat__mult__1__right,fact_nat__1__eq__mult__iff,fact_nat__mult__1,fact_add__gr__0,fact_nat__0__less__mult__iff,fact_mult__less__cancel1,fact_mult__less__cancel2,fact_mult__less__mono1,fact_mult__less__mono2,fact_mult__eq__self__implies__10,fact_mult__le__cancel2,fact_nat__mult__le__cancel1,fact_nat__mult__eq__cancel1,fact_nat__mult__less__cancel1,fact_nat__mult__eq__cancel__disj,fact_left__add__mult__distrib,fact_termination__basic__simps_I4_J,fact_termination__basic__simps_I3_J,fact_termination__basic__simps_I2_J,fact_termination__basic__simps_I1_J,fact_termination__basic__simps_I5_J,fact_le__Suc__ex__iff,fact_one__code__numeral__code,fact_zero__code__numeral__code,fact_half,fact_incr__mult__lemma,fact_iszero__number__of__Bit0,fact_pred__Bit1,fact_pred__Bit0,fact_succ__Bit0,fact_succ__Bit1,fact_less__eq__int__code_I13_J,fact_rel__simps_I31_J,fact_mult__Bit0,fact_rel__simps_I14_J,fact_less__int__code_I13_J,fact_Bit0__def,fact_add__Bit0__Bit0,fact_rel__simps_I50_J,fact_rel__simps_I49_J,fact_minus__Bit0,fact_rel__simps_I48_J,fact_rel__simps_I44_J,fact_rel__simps_I38_J,fact_Bit0__Pls,fact_add__Bit0__Bit1,fact_add__Bit1__Bit0,fact_rel__simps_I4_J,fact_rel__simps_I10_J,fact_bin__less__0__simps_I3_J,fact_rel__simps_I16_J,fact_less__int__code_I15_J,fact_rel__simps_I27_J,fact_rel__simps_I21_J,fact_less__eq__int__code_I14_J,fact_rel__simps_I32_J,fact_number__of__Bit0,fact_rel__simps_I15_J,fact_less__int__code_I14_J,fact_rel__simps_I33_J,fact_less__eq__int__code_I15_J,fact_mult__Bit1,fact_add__Bit1__Bit1,fact_double__number__of__Bit0,fact_number__of1,fact_eq__divide__2__times__iff,fact_mult__2__right,fact_mult__2,fact_one__add__one__is__two,fact_pos2,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I7_J,fact_nat__mult__2__right,fact_nat__mult__2,fact_nat__1__add__1,fact_real__less__half__sum,fact_real__gt__half__sum,fact_half__gt__zero,fact_half__gt__zero__iff,fact_int__pos__lt__two__imp__zero__or__one,fact_real__sum__of__halves,fact_DERIV__real__sqrt__generic,fact_DERIV__const__average,fact_real__sqrt__lt__1__iff,fact_real__sqrt__gt__1__iff,fact_real__sqrt__ge__1__iff,fact_real__sqrt__le__1__iff,fact_real__sqrt__ge__one,fact_real__sqrt__eq__1__iff,fact_real__sqrt__one,fact_real__sqrt__le__mono,fact_real__sqrt__le__iff,fact_real__sqrt__less__mono,fact_real__sqrt__less__iff,fact_real__sqrt__mult,fact_real__sqrt__minus,fact_real__sqrt__inverse,fact_real__sqrt__divide,fact_real__sqrt__eq__iff,fact_real__sqrt__gt__zero,fact_real__sqrt__not__eq__zero,fact_real__sqrt__lt__0__iff,fact_real__sqrt__gt__0__iff,fact_real__sqrt__ge__0__iff,fact_real__sqrt__le__0__iff,fact_real__sqrt__ge__zero,fact_real__sqrt__eq__zero__cancel,fact_real__sqrt__eq__0__iff,fact_real__sqrt__zero,fact_le__real__sqrt__sumsq,fact_real__sqrt__mult__self__sum__ge__zero,fact_sqrt__divide__self__eq,fact_real__sqrt__two__ge__zero,fact_real__sqrt__two__gt__zero,fact_real__sqrt__two__gt__one,fact_lemma__real__divide__sqrt__less,fact_DERIV__real__sqrt,fact_lemma__sqrt__hcomplex__capprox,fact_real__sqrt__sum__squares__mult__ge__zero,fact_real__sqrt__power,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I32_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I30_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,fact_power__eq__0__iff__number__of,fact_power__0__left__number__of,fact_power3__eq__cube,fact_zero__power2,fact_zero__eq__power2,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,fact_power2__eq__square,fact_one__power2,fact_power2__minus,fact_power__even__eq,fact_zero__le__power2,fact_power2__le__imp__le,fact_power2__eq__imp__eq,fact_zero__less__power2,fact_power2__less__0,fact_sum__power2__eq__zero__iff,fact_power2__eq__square__number__of,fact_power2__eq__1__iff,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,fact_ring__1__class_Opower__minus__even,fact_realpow__two__sum__zero__iff,fact_four__x__squared,fact_two__realpow__ge__one,fact_realpow__square__minus__le,fact_power2__less__imp__less,fact_sum__power2__ge__zero,fact_sum__power2__le__zero__iff,fact_not__sum__power2__lt__zero,fact_sum__power2__gt__zero__iff,fact_power2__sum,fact_even__power__le__0__imp__0,fact_zero__le__even__power_H,fact_power__minus1__even,fact_real__sqrt__unique,fact_real__sqrt__pow2,fact_real__sqrt__pow2__iff,fact_real__sqrt__pow2__gt__zero,fact_real__sqrt__sum__squares__ge1,fact_real__sqrt__sum__squares__ge2,fact_real__sqrt__sum__squares__triangle__ineq,fact_real__sqrt__sum__squares__eq__cancel,fact_real__sqrt__sum__squares__eq__cancel2,fact_real__sqrt__sum__squares__mult__squared__eq,fact_real__sqrt__sum__squares__ge__zero,fact_real__inv__sqrt__pow2,fact_real__sum__squared__expand,fact_power__strict__mono,fact_nat__power__less__imp__less,fact_nat__zero__less__power__iff,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I4_J,fact_zpower__zadd__distrib,fact_zpower__zpower,fact_zero__less__power__nat__eq,fact_zero__less__power__nat__eq__number__of,fact_field__power__not__zero,fact_power__mult__distrib,fact_power__commutes,fact_power__one,fact_power__divide,fact_power__mult,fact_power__inverse,fact_power__one__right,fact_zero__le__power,fact_power__mono,fact_zero__less__power,fact_one__le__power,fact_power__eq__0__iff,fact_power__inject__exp,fact_nonzero__power__divide,fact_power__0,fact_power__add,fact_power__one__over,fact_nonzero__power__inverse,fact_power__less__imp__less__base,fact_power__gt1__lemma,fact_power__less__power__Suc,fact_power__0__left,fact_power__minus,fact_power__strict__increasing__iff,fact_power__less__imp__less__exp,fact_power__strict__increasing,fact_power__increasing,fact_power__Suc__less,fact_power__strict__decreasing,fact_power__eq__imp__eq__base,fact_power__decreasing,fact_power__increasing__iff,fact_power__le__imp__le__exp,fact_one__less__power,fact_csqrt,fact_arctan__half,fact_arctan__zero__zero,fact_arctan__minus,fact_arctan__monotone_H,fact_arctan__monotone,fact_DERIV__arctan,fact_cos__x__y__le__one,fact_real__sqrt__sum__squares__less,fact_zero__le__power__abs,fact_power__abs,fact_abs__power__minus,fact_rabs__ratiotest__lemma,fact_abs__mult__pos,fact_abs__eq__mult,fact_abs__of__nonpos,fact_abs__minus__le__zero,fact_abs__of__neg,fact_abs__if,fact_abs__div__pos,fact_abs__one,fact_real__sgn__eq,fact_abs__mult__less,arity_fun__Lattices_Oboolean__algebra,arity_fun__Orderings_Opreorder,arity_fun__Orderings_Oorder,arity_fun__Orderings_Oord,arity_fun__Groups_Ouminus,arity_Int__Oint__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct,arity_Int__Oint__Groups_Oordered__cancel__ab__semigroup__add,arity_Int__Oint__Groups_Oordered__ab__semigroup__add__imp__le,arity_Int__Oint__Rings_Olinordered__comm__semiring__strict,arity_Int__Oint__Rings_Olinordered__semiring__1__strict,arity_Int__Oint__Rings_Olinordered__semiring__strict,arity_Int__Oint__Groups_Oordered__ab__semigroup__add,arity_Int__Oint__Groups_Oordered__ab__group__add__abs,arity_Int__Oint__Groups_Oordered__comm__monoid__add,arity_Int__Oint__Groups_Olinordered__ab__group__add,arity_Int__Oint__Groups_Ocancel__ab__semigroup__add,arity_Int__Oint__Rings_Oring__1__no__zero__divisors,arity_Int__Oint__Rings_Oordered__cancel__semiring,arity_Int__Oint__Rings_Olinordered__ring__strict,arity_Int__Oint__Rings_Oring__no__zero__divisors,arity_Int__Oint__Rings_Oordered__comm__semiring,arity_Int__Oint__Rings_Olinordered__semiring__1,arity_Int__Oint__Groups_Oordered__ab__group__add,arity_Int__Oint__Groups_Ocancel__semigroup__add,arity_Int__Oint__Rings_Olinordered__semiring,arity_Int__Oint__Rings_Olinordered__semidom,arity_Int__Oint__Groups_Oab__semigroup__mult,arity_Int__Oint__Groups_Ocomm__monoid__mult,arity_Int__Oint__Groups_Oab__semigroup__add,arity_Int__Oint__Rings_Oordered__semiring,arity_Int__Oint__Rings_Oordered__ring__abs,arity_Int__Oint__Rings_Ono__zero__divisors,arity_Int__Oint__Groups_Ocomm__monoid__add,arity_Int__Oint__Rings_Olinordered__ring,arity_Int__Oint__Rings_Olinordered__idom,arity_Int__Oint__Rings_Ocomm__semiring__1,arity_Int__Oint__Rings_Ocomm__semiring,arity_Int__Oint__Groups_Oab__group__add,arity_Int__Oint__Rings_Ozero__neq__one,arity_Int__Oint__Rings_Oordered__ring,arity_Int__Oint__Orderings_Opreorder,arity_Int__Oint__Orderings_Olinorder,arity_Int__Oint__Groups_Omonoid__mult,arity_Int__Oint__Rings_Ocomm__ring__1,arity_Int__Oint__Groups_Omonoid__add,arity_Int__Oint__Rings_Osemiring__1,arity_Int__Oint__Rings_Osemiring__0,arity_Int__Oint__Groups_Ogroup__add,arity_Int__Oint__Rings_Omult__zero,arity_Int__Oint__Orderings_Oorder,arity_Int__Oint__Int_Oring__char__0,arity_Int__Oint__Int_Onumber__ring,arity_Int__Oint__Rings_Osemiring,arity_Int__Oint__Orderings_Oord,arity_Int__Oint__Groups_Ouminus,arity_Int__Oint__Groups_Osgn__if,arity_Int__Oint__Groups_Oabs__if,arity_Int__Oint__Rings_Oring__1,arity_Int__Oint__Power_Opower,arity_Int__Oint__Groups_Ozero,arity_Int__Oint__Rings_Oring,arity_Int__Oint__Rings_Oidom,arity_Int__Oint__Int_Onumber,arity_Int__Oint__Groups_Oone,arity_Nat__Onat__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct,arity_Nat__Onat__Groups_Oordered__cancel__ab__semigroup__add,arity_Nat__Onat__Groups_Oordered__ab__semigroup__add__imp__le,arity_Nat__Onat__Rings_Olinordered__comm__semiring__strict,arity_Nat__Onat__Rings_Olinordered__semiring__strict,arity_Nat__Onat__Groups_Oordered__ab__semigroup__add,arity_Nat__Onat__Groups_Oordered__comm__monoid__add,arity_Nat__Onat__Groups_Ocancel__ab__semigroup__add,arity_Nat__Onat__Rings_Oordered__cancel__semiring,arity_Nat__Onat__Rings_Oordered__comm__semiring,arity_Nat__Onat__Groups_Ocancel__semigroup__add,arity_Nat__Onat__Rings_Olinordered__semiring,arity_Nat__Onat__Rings_Olinordered__semidom,arity_Nat__Onat__Groups_Oab__semigroup__mult,arity_Nat__Onat__Groups_Ocomm__monoid__mult,arity_Nat__Onat__Groups_Oab__semigroup__add,arity_Nat__Onat__Rings_Oordered__semiring,arity_Nat__Onat__Rings_Ono__zero__divisors,arity_Nat__Onat__Groups_Ocomm__monoid__add,arity_Nat__Onat__Rings_Ocomm__semiring__1,arity_Nat__Onat__Rings_Ocomm__semiring,arity_Nat__Onat__Rings_Ozero__neq__one,arity_Nat__Onat__Orderings_Opreorder,arity_Nat__Onat__Orderings_Olinorder,arity_Nat__Onat__Groups_Omonoid__mult,arity_Nat__Onat__Groups_Omonoid__add,arity_Nat__Onat__Rings_Osemiring__1,arity_Nat__Onat__Rings_Osemiring__0,arity_Nat__Onat__Rings_Omult__zero,arity_Nat__Onat__Orderings_Oorder,arity_Nat__Onat__Rings_Osemiring,arity_Nat__Onat__Orderings_Oord,arity_Nat__Onat__Power_Opower,arity_Nat__Onat__Groups_Ozero,arity_Nat__Onat__Int_Onumber,arity_Nat__Onat__Groups_Oone,arity_HOL__Obool__Lattices_Oboolean__algebra,arity_HOL__Obool__Orderings_Opreorder,arity_HOL__Obool__Orderings_Oorder,arity_HOL__Obool__Orderings_Oord,arity_HOL__Obool__Groups_Ouminus,arity_RealDef__Oreal__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct,arity_RealDef__Oreal__Groups_Oordered__cancel__ab__semigroup__add,arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add__imp__le,arity_RealDef__Oreal__Rings_Olinordered__comm__semiring__strict,arity_RealDef__Oreal__Fields_Olinordered__field__inverse__zero,arity_RealDef__Oreal__Rings_Olinordered__semiring__1__strict,arity_RealDef__Oreal__RealVector_Oreal__normed__div__algebra,arity_RealDef__Oreal__Rings_Olinordered__semiring__strict,arity_RealDef__Oreal__Rings_Odivision__ring__inverse__zero,arity_RealDef__Oreal__RealVector_Oreal__normed__algebra__1,arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add,arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs,arity_RealDef__Oreal__RealVector_Oreal__normed__algebra,arity_RealDef__Oreal__Groups_Oordered__comm__monoid__add,arity_RealDef__Oreal__Groups_Olinordered__ab__group__add,arity_RealDef__Oreal__Groups_Ocancel__ab__semigroup__add,arity_RealDef__Oreal__Rings_Oring__1__no__zero__divisors,arity_RealDef__Oreal__Rings_Oordered__cancel__semiring,arity_RealDef__Oreal__RealVector_Oreal__normed__vector,arity_RealDef__Oreal__Rings_Olinordered__ring__strict,arity_RealDef__Oreal__RealVector_Oreal__normed__field,arity_RealDef__Oreal__Rings_Oring__no__zero__divisors,arity_RealDef__Oreal__Rings_Oordered__comm__semiring,arity_RealDef__Oreal__Rings_Olinordered__semiring__1,arity_RealDef__Oreal__Groups_Oordered__ab__group__add,arity_RealDef__Oreal__Groups_Ocancel__semigroup__add,arity_RealDef__Oreal__Rings_Olinordered__semiring,arity_RealDef__Oreal__Fields_Ofield__inverse__zero,arity_RealDef__Oreal__Rings_Olinordered__semidom,arity_RealDef__Oreal__Groups_Oab__semigroup__mult,arity_RealDef__Oreal__Groups_Ocomm__monoid__mult,arity_RealDef__Oreal__Groups_Oab__semigroup__add,arity_RealDef__Oreal__Fields_Olinordered__field,arity_RealDef__Oreal__Rings_Oordered__semiring,arity_RealDef__Oreal__Rings_Oordered__ring__abs,arity_RealDef__Oreal__Rings_Ono__zero__divisors,arity_RealDef__Oreal__Groups_Ocomm__monoid__add,arity_RealDef__Oreal__Rings_Olinordered__ring,arity_RealDef__Oreal__Rings_Olinordered__idom,arity_RealDef__Oreal__Rings_Ocomm__semiring__1,arity_RealDef__Oreal__Rings_Odivision__ring,arity_RealDef__Oreal__Rings_Ocomm__semiring,arity_RealDef__Oreal__Groups_Oab__group__add,arity_RealDef__Oreal__Rings_Ozero__neq__one,arity_RealDef__Oreal__Rings_Oordered__ring,arity_RealDef__Oreal__Orderings_Opreorder,arity_RealDef__Oreal__Orderings_Olinorder,arity_RealDef__Oreal__Groups_Omonoid__mult,arity_RealDef__Oreal__Rings_Ocomm__ring__1,arity_RealDef__Oreal__Groups_Omonoid__add,arity_RealDef__Oreal__Rings_Osemiring__1,arity_RealDef__Oreal__Rings_Osemiring__0,arity_RealDef__Oreal__Groups_Ogroup__add,arity_RealDef__Oreal__Rings_Omult__zero,arity_RealDef__Oreal__Orderings_Oorder,arity_RealDef__Oreal__Int_Oring__char__0,arity_RealDef__Oreal__Int_Onumber__ring,arity_RealDef__Oreal__Rings_Osemiring,arity_RealDef__Oreal__Orderings_Oord,arity_RealDef__Oreal__Groups_Ouminus,arity_RealDef__Oreal__Groups_Osgn__if,arity_RealDef__Oreal__Groups_Oabs__if,arity_RealDef__Oreal__Rings_Oring__1,arity_RealDef__Oreal__Fields_Ofield,arity_RealDef__Oreal__Power_Opower,arity_RealDef__Oreal__Groups_Ozero,arity_RealDef__Oreal__SEQ_Obanach,arity_RealDef__Oreal__Rings_Oring,arity_RealDef__Oreal__Rings_Oidom,arity_RealDef__Oreal__Int_Onumber,arity_RealDef__Oreal__Groups_Oone,arity_Complex__Ocomplex__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct,arity_Complex__Ocomplex__RealVector_Oreal__normed__div__algebra,arity_Complex__Ocomplex__Rings_Odivision__ring__inverse__zero,arity_Complex__Ocomplex__RealVector_Oreal__normed__algebra__1,arity_Complex__Ocomplex__RealVector_Oreal__normed__algebra,arity_Complex__Ocomplex__Groups_Ocancel__ab__semigroup__add,arity_Complex__Ocomplex__Rings_Oring__1__no__zero__divisors,arity_Complex__Ocomplex__RealVector_Oreal__normed__vector,arity_Complex__Ocomplex__RealVector_Oreal__normed__field,arity_Complex__Ocomplex__Rings_Oring__no__zero__divisors,arity_Complex__Ocomplex__Groups_Ocancel__semigroup__add,arity_Complex__Ocomplex__Fields_Ofield__inverse__zero,arity_Complex__Ocomplex__Groups_Oab__semigroup__mult,arity_Complex__Ocomplex__Groups_Ocomm__monoid__mult,arity_Complex__Ocomplex__Groups_Oab__semigroup__add,arity_Complex__Ocomplex__Rings_Ono__zero__divisors,arity_Complex__Ocomplex__Groups_Ocomm__monoid__add,arity_Complex__Ocomplex__Rings_Ocomm__semiring__1,arity_Complex__Ocomplex__Rings_Odivision__ring,arity_Complex__Ocomplex__Rings_Ocomm__semiring,arity_Complex__Ocomplex__Groups_Oab__group__add,arity_Complex__Ocomplex__Rings_Ozero__neq__one,arity_Complex__Ocomplex__Groups_Omonoid__mult,arity_Complex__Ocomplex__Rings_Ocomm__ring__1,arity_Complex__Ocomplex__Groups_Omonoid__add,arity_Complex__Ocomplex__Rings_Osemiring__1,arity_Complex__Ocomplex__Rings_Osemiring__0,arity_Complex__Ocomplex__Groups_Ogroup__add,arity_Complex__Ocomplex__Rings_Omult__zero,arity_Complex__Ocomplex__Int_Oring__char__0,arity_Complex__Ocomplex__Int_Onumber__ring,arity_Complex__Ocomplex__Rings_Osemiring,arity_Complex__Ocomplex__Groups_Ouminus,arity_Complex__Ocomplex__Rings_Oring__1,arity_Complex__Ocomplex__Fields_Ofield,arity_Complex__Ocomplex__Power_Opower,arity_Complex__Ocomplex__Groups_Ozero,arity_Complex__Ocomplex__SEQ_Obanach,arity_Complex__Ocomplex__Rings_Oring,arity_Complex__Ocomplex__Rings_Oidom,arity_Complex__Ocomplex__Int_Onumber,arity_Complex__Ocomplex__Groups_Oone,arity_Code____Numeral__Ocode____numeral__Groups_Oordered__cancel__ab__semigroup__add,arity_Code____Numeral__Ocode____numeral__Groups_Oordered__ab__semigroup__add__imp__le,arity_Code____Numeral__Ocode____numeral__Rings_Olinordered__comm__semiring__strict,arity_Code____Numeral__Ocode____numeral__Rings_Olinordered__semiring__strict,arity_Code____Numeral__Ocode____numeral__Groups_Oordered__ab__semigroup__add,arity_Code____Numeral__Ocode____numeral__Groups_Oordered__comm__monoid__add,arity_Code____Numeral__Ocode____numeral__Groups_Ocancel__ab__semigroup__add,arity_Code____Numeral__Ocode____numeral__Rings_Oordered__cancel__semiring,arity_Code____Numeral__Ocode____numeral__Rings_Oordered__comm__semiring,arity_Code____Numeral__Ocode____numeral__Groups_Ocancel__semigroup__add,arity_Code____Numeral__Ocode____numeral__Rings_Olinordered__semiring,arity_Code____Numeral__Ocode____numeral__Rings_Olinordered__semidom,arity_Code____Numeral__Ocode____numeral__Groups_Oab__semigroup__mult,arity_Code____Numeral__Ocode____numeral__Groups_Ocomm__monoid__mult,arity_Code____Numeral__Ocode____numeral__Groups_Oab__semigroup__add,arity_Code____Numeral__Ocode____numeral__Rings_Oordered__semiring,arity_Code____Numeral__Ocode____numeral__Rings_Ono__zero__divisors,arity_Code____Numeral__Ocode____numeral__Groups_Ocomm__monoid__add,arity_Code____Numeral__Ocode____numeral__Rings_Ocomm__semiring__1,arity_Code____Numeral__Ocode____numeral__Rings_Ocomm__semiring,arity_Code____Numeral__Ocode____numeral__Rings_Ozero__neq__one,arity_Code____Numeral__Ocode____numeral__Orderings_Opreorder,arity_Code____Numeral__Ocode____numeral__Orderings_Olinorder,arity_Code____Numeral__Ocode____numeral__Groups_Omonoid__mult,arity_Code____Numeral__Ocode____numeral__Groups_Omonoid__add,arity_Code____Numeral__Ocode____numeral__Rings_Osemiring__1,arity_Code____Numeral__Ocode____numeral__Rings_Osemiring__0,arity_Code____Numeral__Ocode____numeral__Rings_Omult__zero,arity_Code____Numeral__Ocode____numeral__Orderings_Oorder,arity_Code____Numeral__Ocode____numeral__Rings_Osemiring,arity_Code____Numeral__Ocode____numeral__Orderings_Oord,arity_Code____Numeral__Ocode____numeral__Power_Opower,arity_Code____Numeral__Ocode____numeral__Groups_Ozero,arity_Code____Numeral__Ocode____numeral__Int_Onumber,arity_Code____Numeral__Ocode____numeral__Groups_Oone] % 2.96/3.45 =============================================================== % 2.96/3.45 % 2.96/3.45 Combined formula: 1249 axiom(s) => conjecture % 2.96/3.45 % 2.96/3.45 % Equality/functions detected -> nanoCoP oracle mode % 2.96/3.45 nanoCoP : % 2.96/3.45 % 1,434,921 inferences, 1.683 CPU in 1.683 seconds (100% CPU, 852675 Lips) % 2.96/3.45 % 2.96/3.45 % nanoCoP proof (equality/functions) % 2.96/3.45 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 2.96/3.45 % 2.96/3.45 % SZS output end Proof %------------------------------------------------------------------------------