%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SWW198+1 : TPTP v9.2.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % Computer : n010.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:36 PM UTC 2026 % Result : Theorem 2.98s 3.43s % Output : Proof 2.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWW198+1 : TPTP v9.2.1. Released v5.2.0. % 0.00/0.11 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.14/0.32 % Computer : n010.cluster.edu % 0.14/0.32 % Model : x86_64 x86_64 % 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.32 % Memory : 8042.1875MB % 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.32 % CPULimit : 300 % 0.14/0.32 % WCLimit : 300 % 0.14/0.32 % DateTime : Mon May 11 14:27:22 EDT 2026 % 0.14/0.33 % CPUTime : % 2.98/3.43 % SZS status Theorem % 2.98/3.43 % SZS output start Proof % 2.98/3.44 % 2.98/3.44 =============================================================== % 2.98/3.44 TPTP Problem: conj_0 (conjecture with 1185 axiom(s)) % 2.98/3.44 Axioms: [fact_o,fact_n,fact_assms_I2_J,fact_mult__numeral__1__right,fact_mult__numeral__1,fact_Suc__mult__cancel1,fact_Bit0__Pls,fact_rel__simps_I38_J,fact_rel__simps_I44_J,fact_rel__simps_I49_J,fact_rel__simps_I50_J,fact_rel__simps_I39_J,fact_rel__simps_I46_J,fact_mult__Pls,fact_mult__Bit0,fact_Suc__neq__Zero,fact_Zero__neq__Suc,fact_nat_Osimps_I3_J,fact_Suc__not__Zero,fact_nat_Osimps_I2_J,fact_Zero__not__Suc,fact_mult__cancel2,fact_mult__cancel1,fact_mult__is__0,fact_mult__0__right,fact_mult__0,fact_number__of__Pls,fact_semiring__norm_I112_J,fact_nat__number__of__Pls,fact_semiring__norm_I113_J,fact_mult__eq__1__iff,fact_numeral__3__eq__3,fact_numeral__1__eq__Suc__0,fact_eq__number__of,fact_number__of__reorient,fact_rel__simps_I51_J,fact_Suc__inject,fact_nat_Oinject,fact_Suc__n__not__n,fact_n__not__Suc__n,fact_rel__simps_I48_J,fact_nat__mult__assoc,fact_nat__mult__commute,fact_numeral__2__eq__2,fact_semiring__norm_I115_J,fact_mult__number__of__left,fact_arith__simps_I32_J,fact_number__of__mult,fact_odd__Suc__mult__two__ex,fact_even__mult__two__ex,fact_odd__nat__equiv__def2,fact_even__nat__equiv__def2,fact_even__product__nat,fact_even__Suc,fact_even__zero__nat,fact_nat__mult__eq__cancel__disj,fact_power__odd__eq,fact_divisors__zero,fact_no__zero__divisors,fact_mult__eq__0__iff,fact_b,fact_zmult__commute,fact_times__numeral__code_I5_J,fact_zmult__assoc,fact_zpower__zpower,fact_Pls__def,fact_zero__is__num__zero,fact_power__eq__0__iff__number__of,fact_power3__eq__cube,fact_zero__power2,fact_zero__eq__power2,fact_power2__eq__square,fact_power__even__eq,fact_power2__eq__square__number__of,fact_mult__zero__left,fact_mult__zero__right,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I37_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,fact_csqrt,fact_four__x__squared,fact_power__Suc,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I35_J,fact_power__Suc2,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I27_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I28_J,fact_number__of__is__id,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_comm__semiring__1__class_Onormalizing__semiring__rules_I19_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I7_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J,fact_field__power__not__zero,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I30_J,fact_power__mult__distrib,fact_power__commutes,fact_power__Suc__0,fact_nat__power__eq__Suc__0__iff,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,fact_power__mult,fact_power__eq__0__iff,fact_power__0__Suc,fact_odd__0__le__power__imp__0__le,fact_odd__power__less__zero,fact_power__m1__odd,fact_zero__le__even__power_H,fact_even__power__le__0__imp__0,fact_power2__sum,fact_mult__right_Ozero,fact_mult_Ozero__right,fact_mult__left_Ozero,fact_mult_Ozero__left,fact_less__zeroE,fact_le0,fact_lessI,fact_Suc__mono,fact_zero__less__Suc,fact_bin__less__0__simps_I2_J,fact_pos__add__strict,fact_even__less__0__iff,fact_add__number__of__left,fact_add__number__of__eq,fact_number__of__add,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_le__number__of__eq__not__less,fact_less__number__of,fact_le__number__of,fact_rel__simps_I9_J,fact_rel__simps_I13_J,fact_rel__simps_I6_J,fact_rel__simps_I3_J,fact_rel__simps_I8_J,fact_rel__simps_I26_J,fact_rel__simps_I30_J,fact_rel__simps_I23_J,fact_rel__simps_I20_J,fact_rel__simps_I28_J,fact_add__gr__0,fact_less__add__Suc1,fact_less__add__Suc2,fact_less__iff__Suc__add,fact_less__eq__Suc__le,fact_less__Suc__eq__le,fact_Suc__le__eq,fact_le__imp__less__Suc,fact_Suc__leI,fact_le__less__Suc__eq,fact_Suc__le__lessD,fact_rel__simps_I7_J,fact_rel__simps_I24_J,fact_rel__simps_I25_J,fact_rel__simps_I11_J,fact_linorder__neqE__linordered__idom,fact_mult_Oadd__right,fact_mult__right_Oadd,fact_mult_Oadd__left,fact_mult__left_Oadd,fact_add__nat__number__of,fact_power__strict__mono,fact_sum__squares__gt__zero__iff,fact_not__sum__squares__lt__zero,fact_sum__squares__le__zero__iff,fact_sum__squares__ge__zero,fact_mult__left__le__imp__le,fact_mult__right__le__imp__le,fact_mult__less__imp__less__left,fact_mult__left__less__imp__less,fact_mult__less__imp__less__right,fact_mult__right__less__imp__less,fact_mult__le__less__imp__less,fact_mult__less__le__imp__less,fact_mult__strict__mono_H,fact_mult__strict__mono,fact_mult__le__cancel__left__neg,fact_mult__le__cancel__left__pos,fact_power__less__imp__less__base,fact_rel__simps_I5_J,fact_rel__simps_I29_J,fact_rel__simps_I15_J,fact_less__int__code_I14_J,fact_rel__simps_I33_J,fact_less__eq__int__code_I15_J,fact_less__nat__number__of,fact_le__nat__number__of,fact_nat__mult__le__cancel1,fact_mult__le__cancel2,fact_mult__le__cancel1,fact_double__eq__0__iff,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_comm__semiring__class_Odistrib,fact_combine__common__factor,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_Bit1__Min,fact_rel__simps_I43_J,fact_rel__simps_I47_J,fact_rel__simps_I40_J,fact_rel__simps_I37_J,fact_rel__simps_I42_J,fact_rel__simps_I45_J,fact_add__eq__self__zero,fact_add__is__0,fact_Nat_Oadd__0__right,fact_plus__nat_Oadd__0,fact_zadd__0__right,fact_zadd__0,fact_add__Pls,fact_add__Pls__right,fact_Bit0__def,fact_add__Bit0__Bit0,fact_add__Suc__right,fact_add__Suc,fact_add__Suc__shift,fact_zero__less__power__nat__eq,fact_gr0I,fact_gr__implies__not0,fact_less__nat__zero__code,fact_neq0__conv,fact_not__less0,fact_nat__zero__less__power__iff,fact_nat__power__less__imp__less,fact_le__0__eq,fact_less__eq__nat_Osimps_I1_J,fact_rel__simps_I17_J,fact_less__int__code_I16_J,fact_rel__simps_I2_J,fact_rel__simps_I14_J,fact_less__int__code_I13_J,fact_not__less__eq,fact_less__Suc__eq,fact_Suc__less__eq,fact_not__less__less__Suc__eq,fact_less__antisym,fact_less__SucI,fact_Suc__lessI,fact_less__trans__Suc,fact_less__SucE,fact_Suc__lessD,fact_Suc__less__SucD,fact_rel__simps_I34_J,fact_less__eq__int__code_I16_J,fact_Suc__n__not__le__n,fact_not__less__eq__eq,fact_le__Suc__eq,fact_Suc__le__mono,fact_le__SucI,fact_le__SucE,fact_Suc__leD,fact_rel__simps_I19_J,fact_rel__simps_I31_J,fact_less__eq__int__code_I13_J,fact_plus__numeral__code_I9_J,fact_left__add__mult__distrib,fact_add__mult__distrib2,fact_add__mult__distrib,fact_zadd__zmult__distrib2,fact_zadd__zmult__distrib,fact_not__real__square__gt__zero,fact_less__number__of__int__code,fact_le__square,fact_le__cube,fact_mult__le__mono1,fact_mult__le__mono2,fact_mult__le__mono,fact_less__eq__number__of__int__code,fact_even__sum__nat,fact_even__add,fact_odd__add,fact_less__special_I1_J,fact_less__special_I3_J,fact_le__special_I1_J,fact_le__special_I3_J,fact_power__eq__imp__eq__base,fact_less__0__number__of,fact_sum__squares__eq__zero__iff,fact_add__scale__eq__noteq,fact_right__distrib__number__of,fact_left__distrib__number__of,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_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_add__numeral__0__right,fact_add__numeral__0,fact_zero__less__power,fact_zero__le__power,fact_power__mono,fact_power__add,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,fact_eq__number__of__Pls__Min,fact_add__Bit0__Bit1,fact_add__Bit1__Bit0,fact_add__is__1,fact_one__is__add,fact_bin__less__0__simps_I4_J,fact_rel__simps_I12_J,fact_bin__less__0__simps_I1_J,fact_nat__lt__two__imp__zero__or__one,fact_less__Suc__eq__0__disj,fact_less__Suc0,fact_gr0__conv__Suc,fact_rel__simps_I16_J,fact_less__int__code_I15_J,fact_bin__less__0__simps_I3_J,fact_rel__simps_I4_J,fact_rel__simps_I10_J,fact_nat__one__le__power,fact_rel__simps_I22_J,fact_mult__Suc__right,fact_mult__Suc,fact_rel__simps_I32_J,fact_less__eq__int__code_I14_J,fact_rel__simps_I21_J,fact_rel__simps_I27_J,fact_zero__less__power__nat__eq__number__of,fact_nat__mult__less__cancel1,fact_nat__mult__eq__cancel1,fact_mult__less__mono2,fact_mult__less__mono1,fact_mult__less__cancel2,fact_mult__less__cancel1,fact_nat__0__less__mult__iff,fact_zmult__zless__mono2,fact_Suc__mult__less__cancel1,fact_Suc__mult__le__cancel1,fact_power__mono__odd,fact_even__power__nat,fact_odd__pos,fact_zpower__zadd__distrib,fact_not__sum__power2__lt__zero,fact_sum__power2__gt__zero__iff,fact_sum__power2__ge__zero,fact_sum__power2__le__zero__iff,fact_power2__less__imp__less,fact_number__of__Bit0,fact_power__inject__base,fact_power__le__imp__le__base,fact_neg__one__odd__power,fact_power__less__zero__eq,fact_mult__Bit1,fact_zero__le__odd__power,fact_zero__le__even__power,fact_zero__le__power__iff,fact_zero__le__power__eq,fact_eq__0__number__of,fact_eq__number__of__0,fact_n__less__m__mult__n,fact_n__less__n__mult__m,fact_one__less__mult,fact_one__le__mult__iff,fact_zero__less__power__eq,fact_Suc3__eq__add__3,fact_power__less__zero__eq__number__of,fact_power__le__zero__eq,fact_zero__le__power__eq__number__of,fact_mult__2__right,fact_mult__2,fact_zero__less__power__eq__number__of,fact_add__2__eq__Suc_H,fact_add__2__eq__Suc,fact_nat__mult__2__right,fact_nat__mult__2,fact_power__le__zero__eq__number__of,fact_pos2,fact_mult__nat__number__of,fact_nat__number__of__mult__left,fact_sum__power2__eq__zero__iff,fact_power2__less__0,fact_zero__less__power2,fact_zero__le__power2,fact_power2__le__imp__le,fact_power2__eq__imp__eq,fact_less__2__cases,fact_real__sum__squared__expand,fact_realpow__two__sum__zero__iff,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I7_J,fact_number__of1,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I8_J,fact_add__pos__nonneg,fact_add__nonneg__pos,fact_add__strict__increasing,fact_add__strict__increasing2,fact_less__not__refl,fact_not__add__less1,fact_not__add__less2,fact_le__refl,fact_zle__refl,fact_le__add2,fact_le__add1,fact_nat__neq__iff,fact_le__iff__add,fact_nat__add__commute,fact_zadd__commute,fact_nat__le__linear,fact_zle__linear,fact_nat__less__le,fact_zless__le,fact_le__eq__less__or__eq,fact_zless__linear,fact_zadd__left__commute,fact_nat__add__left__commute,fact_nat__add__assoc,fact_zadd__assoc,fact_nat__add__left__cancel,fact_nat__add__right__cancel,fact_nat__add__left__cancel__less,fact_nat__add__left__cancel__le,fact_linorder__neqE__nat,fact_less__irrefl__nat,fact_less__not__refl2,fact_less__not__refl3,fact_eq__imp__le,fact_less__imp__le__nat,fact_trans__less__add1,fact_trans__less__add2,fact_trans__le__add1,fact_trans__le__add2,fact_zadd__strict__right__mono,fact_add__less__mono1,fact_add__le__mono1,fact_zadd__left__mono,fact_le__neq__implies__less,fact_zle__trans,fact_le__trans,fact_le__antisym,fact_zle__antisym,fact_add__less__mono,fact_zadd__zless__mono,fact_add__le__mono,fact_less__add__eq__less,fact_add__lessD1,fact_add__leD2,fact_add__leD1,fact_add__leE,fact_less__or__eq__imp__le,fact_nat__less__cases,fact_real__add__left__mono,fact_less__eq__real__def,fact_real__less__def,fact_zero__reorient,fact_ab__semigroup__mult__class_Omult__ac_I1_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_Nat__Transfer_Otransfer__nat__int__function__closures_I5_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I1_J,fact_real__mult__commute,fact_real__mult__assoc,fact_real__mult__right__cancel,fact_real__mult__left__cancel,fact_real__mult__less__iff1,fact_real__mult__order,fact_real__mult__less__mono2,fact_real__add__mult__distrib,fact_real__two__squares__add__zero__iff,fact_real__mult__le__cancel__iff2,fact_real__mult__le__cancel__iff1,fact_add__0__left,fact_add__0,fact_double__zero__sym,fact_add__0__right,fact_add_Ocomm__neutral,fact_add__le__cancel__right,fact_add__le__cancel__left,fact_add__right__mono,fact_add__left__mono,fact_add__mono,fact_add__le__imp__le__right,fact_add__le__imp__le__left,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_Nat__Transfer_Otransfer__nat__int__function__closures_I2_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I4_J,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_add__less__le__mono,fact_add__le__less__mono,fact_number__of2,fact_add__nonpos__neg,fact_add__neg__nonpos,fact_zdiv__mono2__neg__lemma,fact_unique__quotient__lemma__neg,fact_zdiv__mono2__lemma,fact_unique__quotient__lemma,fact_q__neg__lemma,fact_real__le__antisym,fact_real__le__trans,fact_real__le__linear,fact_real__le__refl,fact_q__pos__lemma,fact_power2__i,fact_order__refl,fact_real__sqrt__sum__squares__mult__ge__zero,fact_real__sqrt__le__iff,fact_real__sqrt__le__mono,fact_i__squared,fact_real__sqrt__eq__iff,fact_real__sqrt__power,fact_real__sqrt__mult,fact_real__sqrt__zero,fact_real__sqrt__eq__0__iff,fact_complex__i__not__number__of,fact_real__sqrt__less__mono,fact_real__sqrt__less__iff,fact_complex__i__not__zero,fact_real__sqrt__eq__zero__cancel,fact_real__sqrt__ge__zero,fact_real__sqrt__le__0__iff,fact_real__sqrt__ge__0__iff,fact_real__sqrt__gt__0__iff,fact_real__sqrt__lt__0__iff,fact_real__sqrt__not__eq__zero,fact_real__sqrt__gt__zero,fact_le__real__sqrt__sumsq,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_order__less__irrefl,fact_linorder__neq__iff,fact_not__less__iff__gr__or__eq,fact_linorder__less__linear,fact_linorder__antisym__conv3,fact_linorder__neqE,fact_less__imp__neq,fact_order__less__not__sym,fact_order__less__imp__not__less,fact_order__less__imp__not__eq,fact_order__less__imp__not__eq2,fact_order__less__asym_H,fact_xt1_I9_J,fact_ord__eq__less__trans,fact_xt1_I1_J,fact_ord__less__eq__trans,fact_xt1_I2_J,fact_order__less__trans,fact_xt1_I10_J,fact_order__less__asym,fact_linorder__cases,fact_real__sqrt__mult__self__sum__ge__zero,fact_real__sqrt__two__ge__zero,fact_real__sqrt__two__gt__zero,fact_real__sqrt__unique,fact_real__sqrt__pow2,fact_real__sqrt__pow2__iff,fact_real__sqrt__pow2__gt__zero,fact_real__sqrt__sum__squares__triangle__ineq,fact_real__sqrt__sum__squares__ge2,fact_real__sqrt__sum__squares__ge1,fact_real__sqrt__sum__squares__eq__cancel2,fact_real__sqrt__sum__squares__eq__cancel,fact_real__sqrt__sum__squares__mult__squared__eq,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_linorder__antisym__conv1,fact_order__neq__le__trans,fact_xt1_I12_J,fact_leD,fact_order__less__imp__le,fact_linorder__antisym__conv2,fact_order__le__imp__less__or__eq,fact_order__le__neq__trans,fact_xt1_I11_J,fact_order__less__le__trans,fact_xt1_I7_J,fact_order__le__less__trans,fact_xt1_I8_J,fact_real__sqrt__sum__squares__ge__zero,fact_lemma__sqrt__hcomplex__capprox,fact_power__m1__even,fact_real__sqrt__ge__abs2,fact_less__fun__def,fact_abs__power__minus__one,fact_real__sqrt__eq__1__iff,fact_real__sqrt__divide,fact_real__sqrt__one,fact_abs__minus__one,fact_complex__i__not__one,fact_abs__add__abs,fact_abs__add__one__not__less__self,fact_mult__1__left,fact_mult__1,fact_mult__1__right,fact_mult_Ocomm__neutral,fact_abs__idempotent,fact_one__reorient,fact_abs__eq__0,fact_abs__zero,fact_right__inverse__eq,fact_divide__self,fact_divide__self__if,fact_real__zero__not__eq__one,fact_real__mult__1,fact_abs__mult__self,fact_abs__mult,fact_power__abs,fact_divide__zero__left,fact_divide__zero,fact_divide_Ozero,fact_times__divide__eq__right,fact_add__divide__distrib,fact_divide_Oadd,fact_power__divide,fact_one__neq__zero,fact_zero__neq__one,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I12_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I11_J,fact_real__divide__square__eq,fact_power__one,fact_power__one__right,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,fact_int__0__neq__1,fact_nat__mult__eq__1__iff,fact_nat__mult__1__right,fact_nat__1__eq__mult__iff,fact_nat__mult__1,fact_zmult__1__right,fact_zmult__1,fact_abs__one,fact_divide__1,fact_power__one__over,fact_abs__add__one__gt__zero,fact_odd__1__nat,fact_abs__ge__self,fact_abs__le__D1,fact_abs__ge__zero,fact_abs__le__zero__iff,fact_abs__of__nonneg,fact_abs__not__less__zero,fact_zero__less__abs__iff,fact_abs__of__pos,fact_abs__mult__less,fact_abs__triangle__ineq,fact_eq__divide__imp,fact_divide__eq__imp,fact_nonzero__divide__eq__eq,fact_nonzero__eq__divide__eq,fact_nonzero__power__divide,fact_power__even__abs,fact_not__one__le__zero,fact_zero__le__one,fact_not__one__less__zero,fact_zero__less__one,fact_less__1__mult,fact_real__0__le__divide__iff,fact_less__add__one,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I4_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I3_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I2_J,fact_one__le__power,fact_power__inject__exp,fact_real__sqrt__abs2,fact_power__0,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I32_J,fact_One__nat__def,fact_Suc__eq__plus1__left,fact_Suc__eq__plus1,fact_mult__eq__self__implies__10,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I6_J,fact_int__0__less__1,fact_Bit1__def,fact_odd__nonzero,fact_zless__add1__eq,fact_real__sqrt__ge__one,fact_real__sqrt__le__1__iff,fact_real__sqrt__ge__1__iff,fact_real__sqrt__gt__1__iff,fact_real__sqrt__lt__1__iff,fact_abs__eq__mult,fact_abs__mult__pos,fact_zero__le__power__abs,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_power__mono__even,fact_divide__Numeral0,fact_power__even__abs__number__of,fact_divide__numeral__1,fact_divide__Numeral1,fact_mult__left__le__one__le,fact_mult__right__le__one__le,fact_zero__less__two,fact_power__gt1__lemma,fact_power__less__power__Suc,fact_power__0__left,fact_number__of__Bit1,fact_power__gt1,fact_power__strict__increasing,fact_power__less__imp__less__exp,fact_power__strict__increasing__iff,fact_power__increasing,fact_semiring__norm_I110_J,fact_numeral__1__eq__1,fact_Numeral1__eq1__nat,fact_nat__numeral__1__eq__1,fact_one__is__num__one,fact_int__one__le__iff__zero__less,fact_odd__less__0,fact_pos__zmult__eq__1__iff,fact_zless__imp__add1__zle,fact_add1__zle__eq,fact_zle__add1__eq__le,fact_zmult__eq__1__iff,fact_pos__zmult__eq__1__iff__lemma,fact_less__divide__eq__number__of1,fact_less__divide__eq__number__of,fact_divide__less__eq__number__of,fact_divide__less__eq__number__of1,fact_convex__bound__le,fact_power__Suc__less,fact_realpow__Suc__le__self,fact_power__Suc__less__one,fact_power__strict__decreasing,fact_double__number__of__Bit0,fact_power__decreasing,fact_power__le__imp__le__exp,fact_power__increasing__iff,fact_one__less__power,fact_power__0__left__number__of,fact_neg__one__even__power,fact_neg__one__even__odd__power,fact_le__imp__0__less,fact_real__sqrt__sum__squares__less,fact_abs__power2,fact_power2__abs,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_convex__bound__lt,fact_le__special_I2_J,fact_le__special_I4_J,fact_one__add__one__is__two,fact_less__special_I2_J,fact_less__special_I4_J,fact_add__special_I2_J,fact_add__special_I3_J,fact_one__power2,fact_nat__1__add__1,fact_self__quotient__aux2,fact_self__quotient__aux1,fact_half__gt__zero__iff,fact_half__gt__zero,fact_real__sqrt__abs,fact_real__less__half__sum,fact_real__gt__half__sum,fact_two__realpow__ge__one,fact_real__sqrt__two__gt__one,fact_lemma__real__divide__sqrt__less,fact_int__pos__lt__two__imp__zero__or__one,fact_real__sqrt__ge__abs1,fact_cos__x__y__le__one,fact_half,fact_less__one__imp__sqr__less__one,fact_abs__zmult__eq__1,fact_zabs__less__one__iff,fact_zero__le__zpower__abs,fact_zero__less__zpower__abs__iff,fact_le__Suc__ex__iff,fact_rabs__ratiotest__lemma,fact_real__sum__of__halves,fact_eq__divide__2__times__iff,fact_IH,fact_le__divide__eq,fact_abs__norm__cancel,fact_norm__zero,fact_norm__eq__zero,fact_norm__mult,fact_complex__mod__triangle__sub,fact_norm__divide,fact_norm__power,fact_norm__not__less__zero,fact_norm__ge__zero,fact_norm__one,fact_norm__le__zero__iff,fact_zero__less__norm__iff,fact_norm__mult__ineq,fact_norm__mult__less,fact_nonzero__norm__divide,fact_norm__triangle__ineq,fact_norm__add__less,fact_norm__power__ineq,fact_norm__number__of,fact_norm__ratiotest__lemma,fact_times__divide__times__eq,fact_abs__divide,fact_divide__right__mono__neg,fact_divide__right__mono,fact_divide__le__0__iff,fact_zero__le__divide__iff,fact_zero__less__divide__iff,fact_divide__less__0__iff,fact_divide__pos__pos,fact_divide__pos__neg,fact_divide__neg__pos,fact_divide__neg__neg,fact_divide__strict__right__mono,fact_divide__strict__right__mono__neg,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_nonzero__abs__divide,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_less__divide__eq,fact_divide__less__eq,fact_pos__less__divide__eq,fact_pos__divide__less__eq,fact_mult__imp__div__pos__less,fact_mult__imp__less__div__pos,fact_neg__less__divide__eq,fact_neg__divide__less__eq,fact_divide__strict__left__mono,fact_divide__strict__left__mono__neg,fact_add__num__frac,fact_add__divide__eq__iff,fact_add__frac__num,fact_divide__add__eq__iff,fact_add__frac__eq,fact_gt__half__sum,fact_less__half__sum,fact_abs__div__pos,fact_divide__left__mono__neg,fact_divide__left__mono,fact_neg__divide__le__eq,fact_neg__le__divide__eq,fact_mult__imp__le__div__pos,fact_mult__imp__div__pos__le,fact_pos__divide__le__eq,fact_pos__le__divide__eq,fact_divide__le__eq,fact_calculation,fact_arctan__half,fact_real__norm__def,fact_arctan__monotone_H,fact_arctan__zero__zero,fact_arctan__monotone,fact_th0,fact_pos__zmod__mult__2,fact_norm__of__real,fact_mod__neg__neg__trivial,fact_neg__mod__conj,fact_neg__mod__sign,fact_mod__pos__pos__trivial,fact_pos__mod__conj,fact_pos__mod__sign,fact_nonzero__of__real__divide,fact_zmod__minus1__right,fact_mod__mult__right__eq,fact_mod__mult__left__eq,fact_mod__mult__eq,fact_mod__mult__mult1,fact_mod__mult__mult2,fact_zmod__simps_I4_J,fact_mod__mult__cong,fact_zmod__zmult1__eq,fact_zmod__simps_I3_J,fact_mod__mult__self2__is__0,fact_mod__mult__self1__is__0,fact_of__real__0,fact_of__real_Ozero,fact_of__real__eq__0__iff,fact_of__real__mult,fact_zmod__self,fact_zmod__zero,fact_mod__self,fact_mod__by__0,fact_mod__0,fact_zpower__zmod,fact_mod__mod__trivial,fact_of__real__eq__iff,fact_complex__of__real__power,fact_of__real__divide,fact_zmod__eq__0__iff,fact_of__real__power,fact_neg__mod__bound,fact_pos__mod__bound,fact_Divides_Otransfer__nat__int__function__closures_I2_J,fact_zmod__le__nonneg__dividend,fact_of__real__number__of__eq,fact_mod__by__1,fact_of__real__1,fact_of__real__add,fact_of__real_Oadd,fact_mod__add__self2,fact_mod__add__self1,fact_mod__add__right__eq,fact_mod__add__left__eq,fact_mod__add__eq,fact_zmod__simps_I2_J,fact_zmod__simps_I1_J,fact_mod__add__cong,fact_mod__mult__self2,fact_mod__mult__self1,fact_mod__pos__neg__trivial,fact_i__mult__eq,fact_zmod__number__of__Bit0,fact_divmod__int__rel__mod__eq,fact_zmult2__lemma__aux2,fact_zmult2__lemma__aux1,fact_zmult2__lemma__aux4,fact_zmult2__lemma__aux3,fact_split__zmod,fact_neq__one__mod__two,fact_neg__zmod__mult__2,fact_zmod__number__of__Bit1,arity_fun__Orderings_Opreorder,arity_fun__Orderings_Oorder,arity_fun__Orderings_Oord,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_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__Divides_Osemiring__div,arity_Int__Oint__Rings_Ocomm__semiring,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__Groups_Omonoid__add,arity_Int__Oint__Rings_Osemiring__1,arity_Int__Oint__Rings_Osemiring__0,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__Power_Opower,arity_Int__Oint__Groups_Ozero,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__Divides_Osemiring__div,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__Orderings_Opreorder,arity_HOL__Obool__Orderings_Oorder,arity_HOL__Obool__Orderings_Oord,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_Ocancel__semigroup__add,arity_RealDef__Oreal__Rings_Olinordered__semiring,arity_RealDef__Oreal__RealVector_Oreal__algebra__1,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__RealVector_Oreal__field,arity_RealDef__Oreal__Rings_Odivision__ring,arity_RealDef__Oreal__Rings_Ocomm__semiring,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__Groups_Omonoid__add,arity_RealDef__Oreal__Rings_Osemiring__1,arity_RealDef__Oreal__Rings_Osemiring__0,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__Fields_Ofield,arity_RealDef__Oreal__Power_Opower,arity_RealDef__Oreal__Groups_Ozero,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__RealVector_Oreal__algebra__1,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__RealVector_Oreal__field,arity_Complex__Ocomplex__Rings_Odivision__ring,arity_Complex__Ocomplex__Rings_Ocomm__semiring,arity_Complex__Ocomplex__Rings_Ozero__neq__one,arity_Complex__Ocomplex__Groups_Omonoid__mult,arity_Complex__Ocomplex__Groups_Omonoid__add,arity_Complex__Ocomplex__Rings_Osemiring__1,arity_Complex__Ocomplex__Rings_Osemiring__0,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__Fields_Ofield,arity_Complex__Ocomplex__Power_Opower,arity_Complex__Ocomplex__Groups_Ozero,arity_Complex__Ocomplex__Int_Onumber,arity_Complex__Ocomplex__Groups_Oone] % 2.98/3.44 =============================================================== % 2.98/3.44 % 2.98/3.44 Combined formula: 1185 axiom(s) => conjecture % 2.98/3.44 % 2.98/3.44 % Equality/functions detected -> nanoCoP oracle mode % 2.98/3.44 nanoCoP : % 2.98/3.44 % 1,371,179 inferences, 1.718 CPU in 1.718 seconds (100% CPU, 798194 Lips) % 2.98/3.44 % 2.98/3.44 % nanoCoP proof (equality/functions) % 2.98/3.44 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 2.98/3.44 % 2.98/3.44 % SZS output end Proof %------------------------------------------------------------------------------