%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SWW194+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 : n026.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 29.08s 28.33s % Output : Proof 29.08s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW194+1 : TPTP v9.2.1. Released v5.2.0. % 0.00/0.12 % Command : g4plus.sh /export/starexec/sandbox/benchmark/theBenchmark.p 300 % 0.16/0.33 % Computer : n026.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Mon May 11 14:27:54 EDT 2026 % 0.16/0.33 % CPUTime : % 29.08/28.33 % SZS status Theorem % 29.08/28.33 % SZS output start Proof % 29.08/28.33 % 29.08/28.33 =============================================================== % 29.08/28.33 TPTP Problem: conj_0 (conjecture with 1198 axiom(s)) % 29.08/28.33 Axioms: [fact_ext,fact__096abs_A_I2_A_K_Ax_J_A_060_061_A1_096,fact__096abs_A_I2_A_K_Ay_J_A_060_061_A1_096,fact__0962_A_K_Ax_A_060_061_A1_096,fact__0962_A_K_Ay_A_060_061_A1_096,fact_two__realpow__ge__one,fact_four__x__squared,fact_power2__eq__square__number__of,fact_abs__power2,fact_power2__abs,fact_one__power2,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,fact_power2__eq__square,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,fact__096_N1_A_060_061_A2_A_K_Ax_096,fact_power3__eq__cube,fact__096_N1_A_060_061_A2_A_K_Ay_096,fact_eq__number__of__Pls__Min,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,fact_nat__numeral__1__eq__1,fact_Numeral1__eq1__nat,fact_power__m1__even,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_real__le__antisym,fact_real__le__trans,fact_real__le__linear,fact_real__le__refl,fact_real__mult__assoc,fact_real__mult__commute,fact_power__even__eq,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_I30_J,fact_real__mult__1,fact_semiring__norm_I110_J,fact_xy,fact_abs__power__minus__one,fact_le__special_I4_J,fact_le__special_I2_J,fact_csqrt,fact_abs__minus__one,fact_numeral__1__eq__1,fact_mult__numeral__1,fact_mult__numeral__1__right,fact_power__increasing,fact_one__le__power,fact_z,fact_assms,fact_number__of__is__id,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_add__number__of__eq,fact_times__numeral__code_I5_J,fact_less__eq__number__of__int__code,fact_add__number__of__left,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_zle__antisym,fact_zle__trans,fact_zle__linear,fact_zle__refl,fact_rel__simps_I34_J,fact_less__eq__int__code_I16_J,fact_rel__simps_I19_J,fact_rel__simps_I31_J,fact_less__eq__int__code_I13_J,fact_rel__simps_I24_J,fact_le__nat__number__of,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_real__add__left__mono,fact_real__add__mult__distrib,fact_right__distrib__number__of,fact_left__distrib__number__of,fact_add__numeral__0__right,fact_add__numeral__0,fact_rel__simps_I22_J,fact_rel__simps_I32_J,fact_less__eq__int__code_I14_J,fact_rel__simps_I21_J,fact_rel__simps_I27_J,fact_rel__simps_I30_J,fact_rel__simps_I26_J,fact_rel__simps_I20_J,fact_rel__simps_I23_J,fact_rel__simps_I28_J,fact_add__special_I2_J,fact_add__special_I3_J,fact_number__of__Bit1,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_double__number__of__Bit0,fact_number__of__reorient,fact_eq__number__of,fact_rel__simps_I51_J,fact_power__one__right,fact_mult__Pls,fact_rel__simps_I48_J,fact_mult__Bit0,fact_zpower__zpower,fact_mult__2__right,fact_mult__2,fact_one__add__one__is__two,fact_pos__zmult__eq__1__iff__lemma,fact_zmult__eq__1__iff,fact_le__number__of,fact_number__of__mult,fact_arith__simps_I32_J,fact_mult__number__of__left,fact_power__commutes,fact_power__mult__distrib,fact_power__one,fact_power2__sum,fact_rel__simps_I39_J,fact_rel__simps_I46_J,fact_one__is__num__one,fact_rel__simps_I49_J,fact_rel__simps_I50_J,fact_Bit0__Pls,fact_rel__simps_I38_J,fact_rel__simps_I44_J,fact_power__mult,fact_power__abs,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_real__sum__squared__expand,fact__096_B_Bthesis_O_A_I_B_Bx_Ay_O_Az_A_061_AComplex_Ax_Ay_A_061_061_062_Athesis_J_A_061_061_062_Athesis_096,fact_abs__triangle__ineq,fact_order__refl,fact_power__m1__odd,fact_power__power__power,fact_power2__diff,fact_zero__le__even__power_H,fact_real__sqrt__ge__abs1,fact_real__sqrt__ge__abs2,fact_sum__power2__ge__zero,fact_C_I2_J,fact_C_I1_J,fact_C_I4_J,fact_C_I3_J,fact_int__0__neq__1,fact_odd__nonzero,fact_number__of__diff,fact_zmult__1,fact_zmult__1__right,fact_zmult__commute,fact_add__eq__if,fact_zpower__zadd__distrib,fact_zadd__zmult__distrib2,fact_zdiff__zmult__distrib2,fact_power__Suc__0,fact_zmult__assoc,fact_zadd__zmult__distrib,fact_zdiff__zmult__distrib,fact_nat__power__eq__Suc__0__iff,fact_abs__zmult__eq__1,fact_power_Opower_Opower__Suc,fact_power_Opower_Opower__0,fact_complex__diff,fact_zadd__assoc,fact_Complex__eq__0,fact_complex__mod__triangle__ineq2,fact_zadd__left__commute,fact_le__iff__diff__le__0,fact_zadd__commute,fact_zadd__0__right,fact_zadd__0,fact_complex__zero__def,fact_zero__reorient,fact_diff__0__right,fact_diff__self,fact_eq__iff__diff__eq__0,fact_right__minus__eq,fact_diff__eq__diff__eq,fact_real__sqrt__eq__iff,fact_real__sqrt__eq__0__iff,fact_real__sqrt__zero,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__le__eq__diff,fact_diff__Suc__eq__diff__pred,fact_power__0__Suc,fact_Suc__eq__plus1,fact_Suc__eq__plus1__left,fact_nat__one__le__power,fact_diff__eq__diff__less__eq,fact_power__eq__0__iff,fact_diff__add__cancel,fact_add__diff__cancel,fact_abs__minus__commute,fact_add__0__left,fact_add__0,fact_double__zero__sym,fact_add__0__right,fact_add_Ocomm__neutral,fact_mult__eq__if,fact_abs__eq__0,fact_abs__zero,fact_realpow__two__diff,fact_complex__mod__triangle__sub,fact_power__inject__base,fact_power__le__imp__le__base,fact_real__sqrt__le__mono,fact_real__sqrt__le__iff,fact_power__0__left,fact_power__eq__if,fact_real__sqrt__mult,fact_real__sqrt__power,fact_real__sqrt__eq__1__iff,fact_real__sqrt__one,fact_diff__bin__simps_I1_J,fact_diff__bin__simps_I7_J,fact_Bit1__def,fact_add__Pls__right,fact_add__Pls,fact_add__Bit0__Bit0,fact_Bit0__def,fact_zadd__left__mono,fact_plus__numeral__code_I9_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J,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_field__power__not__zero,fact_Pls__def,fact_zero__le__zpower__abs,fact_abs__triangle__ineq2__sym,fact_abs__triangle__ineq2,fact_abs__triangle__ineq3,fact_real__mult__left__cancel,fact_real__mult__right__cancel,fact_real__zero__not__eq__one,fact_zero__le__double__add__iff__zero__le__single__add,fact_double__add__le__zero__iff__single__add__le__zero,fact_add__nonneg__nonneg,fact_add__nonneg__eq__0__iff,fact_add__increasing,fact_add__increasing2,fact_add__nonpos__nonpos,fact_abs__of__nonneg,fact_abs__le__zero__iff,fact_abs__ge__zero,fact_complex__add,fact_Suc3__eq__add__3,fact_real__sqrt__mult__self__sum__ge__zero,fact_realpow__Suc__le__self,fact_numeral__3__eq__3,fact_numeral__1__eq__Suc__0,fact_Complex__eq__number__of,fact_Complex__eq__1,fact_complex__one__def,fact_add__2__eq__Suc,fact_add__2__eq__Suc_H,fact_real__sqrt__ge__one,fact_real__sqrt__le__1__iff,fact_real__sqrt__ge__1__iff,fact_mult__diff__mult,fact_left__diff__distrib__number__of,fact_right__diff__distrib__number__of,fact_add__number__of__diff1,fact_abs__diff__triangle__ineq,fact_abs__triangle__ineq4,fact_real__sqrt__abs2,fact_numeral__2__eq__2,fact_semiring__norm_I115_J,fact_diff__bin__simps_I10_J,fact_diff__bin__simps_I9_J,fact_diff__bin__simps_I3_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I28_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I27_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I35_J,fact_power__Suc2,fact_power__Suc,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,fact_power__add,fact_mult__Bit1,fact_add__Bit1__Bit0,fact_add__Bit0__Bit1,fact_sum__squares__eq__zero__iff,fact_add__scale__eq__noteq,fact_complex__mult,fact_power__mono,fact_zero__le__power,fact_semiring__norm_I112_J,fact_number__of__Pls,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I32_J,fact_power__0,fact_nat__number__of__Pls,fact_semiring__norm_I113_J,fact_zero__is__num__zero,fact_real__two__squares__add__zero__iff,fact_real__sqrt__two__ge__zero,fact_complex__norm,fact_le__real__sqrt__sumsq,fact_real__sqrt__unique,fact_real__sqrt__pow2,fact_real__sqrt__pow2__iff,fact_real__squared__diff__one__factored,fact_real__sqrt__sum__squares__eq__cancel2,fact_real__sqrt__sum__squares__eq__cancel,fact_diff__bin__simps_I4_J,fact_diff__bin__simps_I6_J,fact_diff__bin__simps_I5_J,fact_sum__squares__le__zero__iff,fact_sum__squares__ge__zero,fact_linorder__le__cases,fact_le__funE,fact_xt1_I6_J,fact_xt1_I5_J,fact_order__trans,fact_order__antisym,fact_xt1_I4_J,fact_ord__le__eq__trans,fact_xt1_I3_J,fact_ord__eq__le__trans,fact_order__antisym__conv,fact_le__funD,fact_order__eq__refl,fact_order__eq__iff,fact_linorder__linear,fact_le__fun__def,fact_ab__semigroup__mult__class_Omult__ac_I1_J,fact_number__of__Bit0,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_zero__le__power__abs,fact_one__reorient,fact_eq__number__of__0,fact_eq__0__number__of,fact_real__sqrt__sum__squares__ge__zero,fact_abs__idempotent,fact_odd__0__le__power__imp__0__le,fact_complex_Oinject,fact_real__sqrt__sum__squares__mult__ge__zero,fact_le__special_I3_J,fact_le__special_I1_J,fact_power__decreasing,fact_nat__mult__2,fact_nat__mult__2__right,fact_nat__1__add__1,fact_zero__eq__power2,fact_zero__power2,fact_real__sqrt__abs,fact_power2__eq__imp__eq,fact_power2__le__imp__le,fact_zero__le__power2,fact_sum__power2__eq__zero__iff,fact_real__sqrt__sum__squares__triangle__ineq,fact_real__sqrt__sum__squares__ge2,fact_real__sqrt__sum__squares__ge1,fact_real__sqrt__sum__squares__mult__squared__eq,fact_realpow__two__sum__zero__iff,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_mult_Ocomm__neutral,fact_mult__1__right,fact_mult__1,fact_mult__1__left,fact_abs__le__D1,fact_abs__ge__self,fact_abs__add__abs,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I37_J,fact_power__odd__eq,fact_sum__power2__le__zero__iff,fact_even__power__le__0__imp__0,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I7_J,fact_norm__diff__triangle__ineq,fact_convex__bound__le,fact_norm__number__of,fact_norm__triangle__ineq3,fact_norm__power__ineq,fact_norm__triangle__ineq4,fact_complex__i__not__one,fact_complex__i__not__number__of,fact_complex__i__not__zero,fact_real__norm__def,fact_i__squared,fact_Complex__eq__i,fact_i__def,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I5_J,fact_mult__zero__left,fact_mult_Ozero__left,fact_mult__left_Ozero,fact_mult__zero__right,fact_mult_Ozero__right,fact_mult__right_Ozero,fact_mult__eq__0__iff,fact_no__zero__divisors,fact_divisors__zero,fact_one__neq__zero,fact_zero__neq__one,fact_mult_Oadd__right,fact_mult__right_Oadd,fact_comm__semiring__class_Odistrib,fact_mult_Oadd__left,fact_mult__left_Oadd,fact_combine__common__factor,fact_mult_Odiff__right,fact_mult__right_Odiff,fact_mult_Odiff__left,fact_mult__left_Odiff,fact_norm__eq__zero,fact_norm__zero,fact_abs__mult,fact_abs__mult__self,fact_abs__one,fact_norm__minus__commute,fact_norm__ge__zero,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I6_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I1_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I2_J,fact_abs__norm__cancel,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I4_J,fact_power2__i,fact_zero__le__square,fact_zero__le__mult__iff,fact_mult__le__0__iff,fact_mult__nonneg__nonneg,fact_mult__nonneg__nonpos,fact_mult__nonneg__nonpos2,fact_mult__nonpos__nonneg,fact_mult__nonpos__nonpos,fact_mult__right__mono,fact_mult__left__mono,fact_comm__mult__left__mono,fact_mult__right__mono__neg,fact_mult__left__mono__neg,fact_mult__mono_H,fact_mult__mono,fact_split__mult__pos__le,fact_split__mult__neg__le,fact_not__one__le__zero,fact_zero__le__one,fact_mult_Oprod__diff__prod,fact_eq__add__iff2,fact_eq__add__iff1,fact_power__eq__0__iff__number__of,fact_norm__le__zero__iff,fact_norm__diff__ineq,fact_norm__triangle__ineq2,fact_norm__mult,fact_norm__one,fact_norm__power,fact_mult__right__le__one__le,fact_mult__left__le__one__le,fact_le__add__iff2,fact_le__add__iff1,fact_abs__mult__pos,fact_abs__eq__mult,fact_power__0__left__number__of,fact_norm__mult__ineq,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I8_J,fact_norm__triangle__ineq,fact_realpow__num__eq__if,fact_number__of1,fact_lemma__realpow__diff,fact_le0,fact_norm__ratiotest__lemma,fact_n__not__Suc__n,fact_Suc__n__not__n,fact_nat_Oinject,fact_Suc__inject,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__refl,fact_nat__le__linear,fact_eq__imp__le,fact_le__trans,fact_le__antisym,fact_nat__mult__commute,fact_nat__mult__assoc,fact_diff__commute,fact_Zero__not__Suc,fact_nat_Osimps_I2_J,fact_Suc__not__Zero,fact_nat_Osimps_I3_J,fact_Zero__neq__Suc,fact_Suc__neq__Zero,fact_plus__nat_Oadd__0,fact_Nat_Oadd__0__right,fact_add__is__0,fact_add__eq__self__zero,fact_less__eq__nat_Osimps_I1_J,fact_le__0__eq,fact_add__Suc__shift,fact_add__Suc,fact_add__Suc__right,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_mult__0,fact_mult__0__right,fact_mult__is__0,fact_mult__cancel1,fact_mult__cancel2,fact_diffs0__imp__equal,fact_diff__self__eq__0,fact_minus__nat_Odiff__0,fact_diff__0__eq__0,fact_Suc__mult__cancel1,fact_le__add2,fact_le__add1,fact_le__Suc__ex__iff,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_diff__Suc__Suc,fact_Suc__diff__diff,fact_add__mult__distrib2,fact_add__mult__distrib,fact_le__square,fact_le__cube,fact_mult__le__mono1,fact_mult__le__mono2,fact_mult__le__mono,fact_diff__add__inverse2,fact_diff__add__inverse,fact_diff__diff__left,fact_diff__cancel,fact_diff__cancel2,fact_diff__le__self,fact_diff__le__mono2,fact_diff__le__mono,fact_diff__diff__cancel,fact_eq__diff__iff,fact_Nat_Odiff__diff__eq,fact_le__diff__iff,fact_diff__mult__distrib2,fact_diff__mult__distrib,fact_nat__mult__1,fact_nat__1__eq__mult__iff,fact_nat__mult__1__right,fact_nat__mult__eq__1__iff,fact_add__is__1,fact_one__is__add,fact_mult__eq__1__iff,fact_One__nat__def,fact_diff__add__0,fact_diff__is__0__eq_H,fact_diff__is__0__eq,fact_mult__Suc__right,fact_mult__Suc,fact_Suc__mult__le__cancel1,fact_Suc__diff__le,fact_mult__eq__self__implies__10,fact_diff__add__assoc2,fact_add__diff__assoc2,fact_diff__add__assoc,fact_le__imp__diff__is__add,fact_le__add__diff__inverse2,fact_le__diff__conv2,fact_add__diff__assoc,fact_le__add__diff__inverse,fact_le__add__diff,fact_le__diff__conv,fact_diff__diff__right,fact_diff__Suc__1,fact_one__le__mult__iff,fact_number__of2,fact_diff__Suc__diff__eq2,fact_diff__Suc__diff__eq1,fact_rabs__ratiotest__lemma,fact_complex_Osize_I1_J,fact_nat__le__add__iff1,fact_nat__diff__add__eq1,fact_nat__eq__add__iff1,fact_nat__mult__eq__cancel__disj,fact_left__add__mult__distrib,fact_nat__eq__add__iff2,fact_nat__diff__add__eq2,fact_nat__le__add__iff2,fact_cos__x__y__le__one,fact_complex_Osize_I2_J,fact_complex_Osimps_I2_J,fact_divide__zero__left,fact_divide_Ozero,fact_divide__zero,fact_diff__divide__distrib,fact_divide_Odiff,fact_times__divide__eq__right,fact_add__divide__distrib,fact_divide_Oadd,fact_divide__1,fact_power__divide,fact_real__divide__square__eq,fact_real__sqrt__divide,fact_nonzero__norm__divide,fact_norm__divide,fact_eq__divide__imp,fact_divide__eq__imp,fact_nonzero__divide__eq__eq,fact_nonzero__eq__divide__eq,fact_divide__self__if,fact_divide__self,fact_right__inverse__eq,fact_nonzero__power__divide,fact_power__one__over,fact_real__0__le__divide__iff,fact_divide__eq__eq__number__of1,fact_divide__eq__eq__number__of,fact_eq__divide__eq__number__of,fact_eq__divide__eq__number__of1,fact_divide__Numeral0,fact_divide__Numeral1,fact_divide__numeral__1,fact_power__diff,fact_real__average__minus__second,fact_real__average__minus__first,fact_real__sum__of__halves,fact_Deriv_Oadd__diff__add,fact_lemma__MVT,fact_DERIV__mult__lemma,fact_eq__divide__2__times__iff,fact_diff__divide__eq__iff,fact_divide__diff__eq__iff,fact_diff__frac__eq,fact_times__divide__times__eq,fact_abs__divide,fact_zero__le__divide__iff,fact_divide__le__0__iff,fact_divide__right__mono,fact_divide__right__mono__neg,fact_eq__divide__eq,fact_divide__eq__eq,fact_mult__divide__mult__cancel__right,fact_mult__divide__mult__cancel__left,fact_frac__eq__eq,fact_nonzero__abs__divide,fact_add__frac__eq,fact_divide__add__eq__iff,fact_add__frac__num,fact_add__divide__eq__iff,fact_add__num__frac,fact_arctan__half,fact_lemma__sqrt__hcomplex__capprox,fact_real__sqrt__sum__squares__less,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_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_even__less__0__iff,fact_pos__add__strict,fact_arctan__zero__zero,fact_arctan__monotone_H,fact_arctan__monotone,fact_real__sqrt__less__mono,fact_real__sqrt__less__iff,fact_less__special_I3_J,fact_less__special_I1_J,fact_power__strict__decreasing,fact_one__less__power,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_less__eq__real__def,fact_real__less__def,fact_diff__eq__diff__less,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_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_not__leE,fact_leI,fact_order__le__less,fact_less__le__not__le,fact_order__less__le,fact_linorder__le__less__linear,fact_linorder__not__le,fact_linorder__not__less,fact_power__strict__increasing,fact_power__less__imp__less__exp,fact_power__strict__increasing__iff,fact_linorder__neqE__linordered__idom,fact_less__number__of,fact_less__special_I4_J,fact_less__special_I2_J,fact_power__strict__mono,fact_add__le__less__mono,fact_add__less__le__mono,fact_le__number__of__eq__not__less,fact_zero__less__one,fact_not__one__less__zero,fact_less__iff__diff__less__0,fact_less__1__mult,fact_zero__less__power,fact_less__add__one,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_power__inject__exp,fact_abs__not__less__zero,fact_zero__less__abs__iff,fact_abs__of__pos,fact_abs__mult__less,fact_real__mult__less__mono2,fact_real__mult__order,fact_real__mult__less__iff1,fact_not__real__square__gt__zero,fact_norm__not__less__zero,fact_real__sqrt__gt__0__iff,fact_real__sqrt__lt__0__iff,fact_real__sqrt__not__eq__zero,fact_real__sqrt__gt__zero,fact_real__sqrt__lt__1__iff,fact_real__sqrt__gt__1__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_add__nonpos__neg,fact_add__neg__nonpos,fact_add__strict__increasing2,fact_add__strict__increasing,fact_add__nonneg__pos,fact_add__pos__nonneg,fact_not__sum__squares__lt__zero,fact_sum__squares__gt__zero__iff,fact_power__less__imp__less__base,fact_zero__less__two,fact_divide__nonneg__pos,fact_divide__nonneg__neg,fact_frac__less2,fact_frac__less,fact_frac__le,fact_divide__nonpos__pos,fact_divide__nonpos__neg,fact_less__add__iff2,fact_less__add__iff1,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_power__gt1__lemma,fact_power__less__power__Suc,fact_less__half__sum,fact_gt__half__sum,fact_power__gt1,fact_abs__diff__less__iff,fact_abs__div__pos,fact_zero__less__norm__iff,fact_real__mult__le__cancel__iff1,fact_real__mult__le__cancel__iff2,fact_norm__mult__less,fact_norm__add__less,fact_abs__add__one__not__less__self,fact_arctan__add,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_le__divide__eq,fact_power__Suc__less,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_power__Suc__less__one,fact_power__increasing__iff,fact_power__le__imp__le__exp,fact_abs__add__one__gt__zero,fact_convex__bound__lt,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_half__gt__zero__iff,fact_half__gt__zero,fact_power2__less__0,fact_zero__less__power2,fact_real__sqrt__two__gt__zero,fact_real__less__half__sum,fact_real__gt__half__sum,fact_real__sqrt__two__gt__one,fact_power2__less__imp__less,fact_half,fact_not__sum__power2__lt__zero,fact_sum__power2__gt__zero__iff,fact_real__sqrt__pow2__gt__zero,fact_lemma__real__divide__sqrt__less,fact_less__one__imp__sqr__less__one,fact_odd__power__less__zero,fact_machin,fact_complex_Orecs,fact_natceiling__add__one,fact_less__zeroE,fact_Suc__mono,fact_lessI,fact_zero__less__Suc,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_pi__not__less__zero,fact_not__less0,fact_pi__gt__zero,fact_neq0__conv,fact_less__nat__zero__code,fact_gr__implies__not0,fact_less__imp__diff__less,fact_diff__less__mono2,fact_gr0I,fact_nat__less__le,fact_le__eq__less__or__eq,fact_less__imp__le__nat,fact_le__neq__implies__less,fact_less__or__eq__imp__le,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_Suc__less__SucD,fact_Suc__lessD,fact_less__SucE,fact_less__trans__Suc,fact_Suc__lessI,fact_less__SucI,fact_less__antisym,fact_not__less__less__Suc__eq,fact_Suc__less__eq,fact_less__Suc__eq,fact_not__less__eq,fact_rel__simps_I7_J,fact_zless__linear,fact_less__number__of__int__code,fact_zadd__strict__right__mono,fact_zless__le,fact_less__int__code_I13_J,fact_rel__simps_I14_J,fact_rel__simps_I2_J,fact_less__int__code_I16_J,fact_rel__simps_I17_J,fact_less__nat__number__of,fact_less__fun__def,fact_less__0__number__of,fact_pi__ge__zero,fact_pi__neq__zero,fact_bin__less__0__simps_I4_J,fact_rel__simps_I12_J,fact_bin__less__0__simps_I1_J,fact_less__int__code_I15_J,fact_rel__simps_I16_J,fact_bin__less__0__simps_I3_J,fact_less__Suc__eq__0__disj,fact_less__Suc0,fact_gr0__conv__Suc,fact_nat__lt__two__imp__zero__or__one,fact_rel__simps_I10_J,fact_rel__simps_I4_J,fact_add__gr__0,fact_less__add__Suc1,fact_less__add__Suc2,fact_less__iff__Suc__add,fact_Suc__le__lessD,fact_le__less__Suc__eq,fact_Suc__leI,fact_le__imp__less__Suc,fact_Suc__le__eq,fact_less__Suc__eq__le,fact_less__eq__Suc__le,fact_int__0__less__1,fact_nat__0__less__mult__iff,fact_mult__less__cancel1,fact_mult__less__cancel2,fact_mult__less__mono1,fact_mult__less__mono2,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_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__Rings_Oring__1,arity_Int__Oint__Power_Opower,arity_Int__Oint__Groups_Ozero,arity_Int__Oint__Rings_Oring,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__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_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__RealVector_Oreal__field,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__Rings_Oring__1,arity_RealDef__Oreal__Fields_Ofield,arity_RealDef__Oreal__Power_Opower,arity_RealDef__Oreal__Groups_Ozero,arity_RealDef__Oreal__Rings_Oring,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__RealVector_Oreal__field,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__Rings_Oring__1,arity_Complex__Ocomplex__Fields_Ofield,arity_Complex__Ocomplex__Power_Opower,arity_Complex__Ocomplex__Groups_Ozero,arity_Complex__Ocomplex__Rings_Oring,arity_Complex__Ocomplex__Int_Onumber,arity_Complex__Ocomplex__Groups_Oone] % 29.08/28.33 =============================================================== % 29.08/28.33 % 29.08/28.33 Combined formula: 1198 axiom(s) => conjecture % 29.08/28.33 % 29.08/28.33 % Equality/functions detected -> nanoCoP oracle mode % 29.08/28.33 nanoCoP : % 29.08/28.33 % 35,344,303 inferences, 26.757 CPU in 26.773 seconds (100% CPU, 1320915 Lips) % 29.08/28.33 % 29.08/28.33 % nanoCoP proof (equality/functions) % 29.08/28.33 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 29.08/28.33 % 29.08/28.33 % SZS output end Proof %------------------------------------------------------------------------------