%------------------------------------------------------------------------------ % File : G4Plus---1.5.2 % Problem : SWW196+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 : n027.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.74s 3.44s % Output : Proof 2.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWW196+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 : n027.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:50 EDT 2026 % 0.16/0.33 % CPUTime : % 2.74/3.44 % SZS status Theorem % 2.74/3.44 % SZS output start Proof % 2.74/3.44 % 2.74/3.44 =============================================================== % 2.74/3.44 TPTP Problem: conj_1 (conjecture with 1171 axiom(s)) % 2.74/3.44 Axioms: [fact__096EX_Am_O_An_A_061_A2_A_K_Am_096,fact_n,fact_e,fact_assms_I2_J,fact_mult__numeral__1__right,fact_mult__numeral__1,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_number__of__mult,fact_arith__simps_I32_J,fact_zmult__commute,fact_times__numeral__code_I5_J,fact_zmult__assoc,fact_mult__Pls,fact_mult__Bit0,fact_number__of__Pls,fact_eq__number__of,fact_number__of__reorient,fact_rel__simps_I51_J,fact_rel__simps_I48_J,fact_mult__number__of__left,fact_even__mult__two__ex,fact_nat__number__of__Pls,fact_semiring__norm_I113_J,fact_semiring__norm_I112_J,fact_even__product__nat,fact_even__zero__nat,fact_mult__cancel2,fact_mult__cancel1,fact_nat__mult__eq__cancel__disj,fact_mult__is__0,fact_mult__0__right,fact_mult__0,fact_number__of__is__id,fact_Pls__def,fact_zero__is__num__zero,fact_nat__mult__commute,fact_nat__mult__assoc,fact_mult__zero__left,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I9_J,fact_mult_Ozero__left,fact_mult__left_Ozero,fact_mult__zero__right,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I10_J,fact_mult_Ozero__right,fact_mult__right_Ozero,fact_mult__eq__0__iff,fact_no__zero__divisors,fact_divisors__zero,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_odd__Suc__mult__two__ex,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I36_J,fact_power2__eq__square__number__of,fact_even__equiv__def,fact_nat__number__of__mult__left,fact_mult__nat__number__of,fact_nat__mult__2,fact_nat__mult__2__right,fact_not__iszero__Numeral1,fact_nat__even__iff__2__dvd,fact_numeral__2__eq__2,fact_dvd_Oorder__refl,fact_dvd__0__right,fact_dvd__1__left,fact_pos__add__strict,fact_dvd__refl,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_linorder__neqE__linordered__idom,fact_dvd__trans,fact_dvd__add,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_even__less__0__iff,fact_zless__linear,fact_n__not__Suc__n,fact_Suc__n__not__n,fact_nat__add__commute,fact_dvd_Oeq__iff,fact_dvd_Ole__less,fact_add__Suc__right,fact_dvd__reduce,fact_nat__add__left__commute,fact_add__Suc,fact_add__Suc__shift,fact_nat_Oinject,fact_nat__add__assoc,fact_dvd_Oless__le,fact_nat__add__left__cancel,fact_nat__add__right__cancel,fact_dvd_Oneq__le__trans,fact_dvd_Oeq__refl,fact_dvd_Oantisym__conv,fact_dvd_Ole__imp__less__or__eq,fact_dvd_Ole__neq__trans,fact_dvd_Oord__eq__le__trans,fact_dvd_Oord__le__eq__trans,fact_dvd__antisym,fact_dvd_Oantisym,fact_dvd_Oorder__trans,fact_dvd_Oord__eq__less__trans,fact_dvd_Ole__less__trans,fact_Suc__inject,fact_dvd_Oless__imp__neq,fact_dvd_Oless__not__sym,fact_dvd_Oless__imp__le,fact_dvd_Oless__imp__not__less,fact_dvd_Oless__imp__not__eq,fact_dvd_Oless__imp__not__eq2,fact_dvd_Oord__less__eq__trans,fact_dvd_Oless__le__trans,fact_dvd_Oless__asym_H,fact_dvd_Oless__trans,fact_dvd_Oless__asym,fact_odd__pow,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I26_J,fact_add__number__of__left,fact_add__number__of__eq,fact_number__of__add,fact_dvd__1__iff__1,fact_less__number__of,fact_one__is__add,fact_add__is__1,fact_zpower__zadd__distrib,fact_mult__Suc__right,fact_mult__Suc,fact_even__power,fact_sum__squares__gt__zero__iff,fact_not__sum__squares__lt__zero,fact_power__less__zero__eq,fact_dvd__0__left,fact_dvd__triv__left,fact_dvd__triv__right,fact_dvd__mult2,fact_dvd__mult,fact_mult__dvd__mono,fact_dvdI,fact_dvd__mult__left,fact_dvd__mult__right,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I30_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_mult_Oadd__right,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I34_J,fact_mult__right_Oadd,fact_crossproduct__noteq,fact_comm__semiring__class_Odistrib,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I8_J,fact_mult_Oadd__left,fact_mult__left_Oadd,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I1_J,fact_combine__common__factor,fact_crossproduct__eq,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_comm__semiring__1__class_Onormalizing__semiring__rules_I31_J,fact_zpower__zpower,fact_add__eq__self__zero,fact_add__is__0,fact_Nat_Oadd__0__right,fact_plus__nat_Oadd__0,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_Suc__mult__cancel1,fact_add__mult__distrib2,fact_add__mult__distrib,fact_left__add__mult__distrib,fact_less__number__of__int__code,fact_even__Suc,fact_even__sum__nat,fact_even__add,fact_odd__add,fact_even__zero__int,fact_odd__times__odd,fact_anything__times__even,fact_even__times__anything,fact_even__product,fact_less__special_I1_J,fact_less__special_I3_J,fact_zero__less__power__eq,fact_power__less__zero__eq__number__of,fact_Suc3__eq__add__3,fact_not__sum__power2__lt__zero,fact_sum__power2__gt__zero__iff,fact_dvd__mult__cancel__left,fact_dvd__mult__cancel__right,fact_odd__power__less__zero,fact_iszero__def,fact_iszero__0,fact_zero__less__power__eq__number__of,fact_add__2__eq__Suc_H,fact_add__2__eq__Suc,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_add__numeral__0__right,fact_add__numeral__0,fact_nat__mult__dvd__cancel__disj,fact_mult__eq__1__iff,fact_bin__less__0__simps_I4_J,fact_rel__simps_I12_J,fact_bin__less__0__simps_I1_J,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_zmult__zless__mono2,fact_sum__power2__eq__zero__iff,fact_power2__less__0,fact_zero__less__power2,fact_power2__sum,fact_power__odd__eq,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I37_J,fact_power__eq__0__iff__number__of,fact_number__of__Bit0,fact_odd__nat__equiv__def2,fact_even__nat__equiv__def2,fact_iszero__number__of__Bit1,fact_iszero__Numeral0,fact_iszero__number__of__Bit0,fact_power3__eq__cube,fact_numeral__1__eq__Suc__0,fact_numeral__3__eq__3,fact_zero__power2,fact_zero__eq__power2,fact_power2__eq__square,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I29_J,fact_mult__2__right,fact_mult__2,fact_power__even__eq,fact_semiring__norm_I115_J,fact_csqrt,fact_four__x__squared,fact_unity__coeff__ex,fact_power__add,fact_power__Suc,fact_power__Suc2,fact_power__0__Suc,fact_power__eq__0__iff,fact_zero__less__power,fact_zero__less__double__add__iff__zero__less__single__add,fact_less__zeroE,fact_Suc__mono,fact_lessI,fact_zero__less__Suc,fact_not__real__square__gt__zero,fact_zadd__commute,fact_zadd__left__commute,fact_zadd__assoc,fact_zdvd__period,fact_zdvd__reduce,fact_nat__power__less__imp__less,fact_nat__zero__less__power__iff,fact_zadd__0,fact_zadd__0__right,fact_add__Pls__right,fact_add__Pls,fact_add__Bit0__Bit0,fact_Bit0__def,fact_not__less0,fact_neq0__conv,fact_less__nat__zero__code,fact_gr__implies__not0,fact_gr0I,fact_zero__less__power__nat__eq,fact_zadd__strict__right__mono,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_plus__numeral__code_I9_J,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_zadd__zmult__distrib2,fact_zadd__zmult__distrib,fact_zdvd__mono,fact_even__sum,fact_even__plus__even,fact_even__plus__odd,fact_odd__plus__even,fact_odd__plus__odd,fact_zdvd__not__zless,fact_zdvd__mult__cancel,fact_add__Bit1__Bit0,fact_add__Bit0__Bit1,fact_nat__lt__two__imp__zero__or__one,fact_less__Suc__eq__0__disj,fact_less__Suc0,fact_gr0__conv__Suc,fact_nat__dvd__not__less,fact_zero__less__power__nat__eq__number__of,fact_add__gr__0,fact_less__iff__Suc__add,fact_less__add__Suc2,fact_less__add__Suc1,fact_nat__0__less__mult__iff,fact_mult__less__cancel1,fact_mult__less__cancel2,fact_nat__mult__eq__cancel1,fact_nat__mult__less__cancel1,fact_mult__less__mono1,fact_mult__less__mono2,fact_Suc__mult__less__cancel1,fact_odd__pos,fact_even__power__nat,fact_mult__Bit1,fact_zero__reorient,fact_n__less__m__mult__n,fact_n__less__n__mult__m,fact_one__less__mult,fact_nat__mult__dvd__cancel1,fact_dvd__mult__cancel,fact_less__nat__number__of,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_pos2,fact_add__nat__number__of,fact_less__0__number__of,fact_int__even__iff__2__dvd,fact_less__2__cases,fact_add__0__left,fact_add__0,fact_double__zero__sym,fact_add__0__right,fact_add_Ocomm__neutral,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_field__power__not__zero,fact_power__mult__distrib,fact_power__commutes,fact_nat__power__eq__Suc__0__iff,fact_power__Suc__0,fact_dvd__power__same,fact_power__mult,fact_add__neg__neg,fact_add__pos__pos,fact_double__add__less__zero__iff__single__add__less__zero,fact_real__sum__squared__expand,fact_realpow__two__sum__zero__iff,fact_odd__0__le__power__imp__0__le,fact_power__m1__odd,fact_power2__diff,fact_odd__equiv__def,fact_le0,fact_real__mult__le__cancel__iff1,fact_real__mult__le__cancel__iff2,fact_power__decreasing,fact_zle__diff1__eq,fact_zdvd__zdiffD,fact_power__increasing,fact_real__add__left__mono,fact_power__le__imp__le__exp,fact_power__increasing__iff,fact_one__le__power,fact_less__eq__real__def,fact_real__less__def,fact_less__not__refl,fact_nat__neq__iff,fact_nat__less__le,fact_le__eq__less__or__eq,fact_linorder__neqE__nat,fact_less__irrefl__nat,fact_less__not__refl2,fact_less__not__refl3,fact_less__imp__le__nat,fact_less__imp__diff__less,fact_le__neq__implies__less,fact_diff__less__mono,fact_diff__less__mono2,fact_less__diff__iff,fact_less__or__eq__imp__le,fact_nat__less__cases,fact_le__number__of,fact_one__reorient,fact_diff__eq__diff__eq,fact_diff__eq__diff__less__eq,fact_number__of__diff,fact_le__iff__diff__le__0,fact_dvd__diffD,fact_dvd__diffD1,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_real__squared__diff__one__factored,fact_le__special_I4_J,fact_le__special_I2_J,fact_le__add__iff2,fact_le__add__iff1,fact_real__le__eq__diff,fact_rel__simps_I24_J,fact_rel__simps_I28_J,fact_rel__simps_I23_J,fact_rel__simps_I20_J,fact_rel__simps_I26_J,fact_rel__simps_I30_J,fact_diff__is__0__eq_H,fact_diff__is__0__eq,fact_not__one__le__zero,fact_zero__le__one,fact_Suc__diff__le,fact_mult__left__le__one__le,fact_mult__right__le__one__le,fact_diff__bin__simps_I4_J,fact_diff__bin__simps_I5_J,fact_diff__bin__simps_I6_J,fact_diff__Suc__diff__eq1,fact_diff__Suc__diff__eq2,fact_rel__simps_I25_J,fact_rel__simps_I11_J,fact_nat__le__add__iff1,fact_nat__diff__add__eq1,fact_nat__eq__add__iff1,fact_nat__le__add__iff2,fact_nat__diff__add__eq2,fact_nat__eq__add__iff2,fact_nat__less__add__iff1,fact_nat__less__add__iff2,fact_le__nat__number__of,fact_int__one__le__iff__zero__less,fact_pos__zmult__eq__1__iff__lemma,fact_zmult__eq__1__iff,fact_zless__imp__add1__zle,fact_add1__zle__eq,fact_zle__add1__eq__le,fact_right__minus__eq,fact_eq__iff__diff__eq__0,fact_diff__self,fact_diff__0__right,fact_diff__eq__diff__less,fact_mult_Odiff__right,fact_mult__right_Odiff,fact_mult_Odiff__left,fact_mult__left_Odiff,fact_add__diff__cancel,fact_diff__add__cancel,fact_realpow__Suc__le__self,fact_dvd__diff,fact_zero__neq__one,fact_one__neq__zero,fact_diff__bin__simps_I1_J,fact_diff__bin__simps_I7_J,fact_diffs0__imp__equal,fact_diff__self__eq__0,fact_minus__nat_Odiff__0,fact_diff__0__eq__0,fact_diff__less,fact_zero__less__diff,fact_Bit1__Min,fact_rel__simps_I43_J,fact_rel__simps_I47_J,fact_rel__simps_I40_J,fact_rel__simps_I37_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I11_J,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I12_J,fact_mult__1__left,fact_mult__1,fact_mult__1__right,fact_mult_Ocomm__neutral,fact_rel__simps_I42_J,fact_rel__simps_I45_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_diff__Suc__Suc,fact_Suc__diff__diff,fact_diff__less__Suc,fact_dvd__diff__nat,fact_diff__add__inverse2,fact_diff__add__inverse,fact_diff__diff__left,fact_diff__cancel,fact_diff__cancel2,fact_less__diff__conv,fact_add__diff__inverse,fact_rel__simps_I7_J,fact_zdiff__zmult__distrib,fact_zdiff__zmult__distrib2,fact_one__dvd,fact_power__one,fact_diff__mult__distrib2,fact_diff__mult__distrib,fact_le__0__eq,fact_less__eq__nat_Osimps_I1_J,fact_rel__simps_I34_J,fact_less__eq__int__code_I16_J,fact_zdvd__antisym__nonneg,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_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_I19_J,fact_rel__simps_I31_J,fact_less__eq__int__code_I13_J,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_zless__le,fact_int__0__neq__1,fact_le__square,fact_le__cube,fact_mult__le__mono1,fact_mult__le__mono2,fact_mult__le__mono,fact_zadd__left__mono,fact_less__eq__number__of__int__code,fact_even__difference__nat,fact_mult__diff__mult,fact_zmult__1__right,fact_zmult__1,fact_even__difference,fact_odd__one__int,fact_convex__bound__le,fact_le__special_I1_J,fact_le__special_I3_J,fact_not__iszero__1,fact_neg__one__even__power,fact_neg__one__even__odd__power,fact_le__imp__0__less,fact_convex__bound__lt,fact_less__iff__diff__less__0,fact_eq__add__iff1,fact_eq__add__iff2,fact_mult_Oprod__diff__prod,fact_right__diff__distrib__number__of,fact_left__diff__distrib__number__of,fact_zero__less__one,fact_not__one__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_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_diff__bin__simps_I9_J,fact_diff__bin__simps_I10_J,fact_diff__bin__simps_I3_J,fact_add__le__less__mono,fact_add__less__le__mono,fact_less__1__mult,fact_le__number__of__eq__not__less,fact_less__add__one,fact_Suc__pred,fact_diff__Suc__less,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_less__bin__lemma,fact_zero__le__power,fact_power__mono,fact_diff__add__0,fact_nat__diff__split__asm,fact_nat__diff__split,fact_power__strict__increasing,fact_power__less__imp__less__exp,fact_power__strict__increasing__iff,fact_power__inject__exp,fact_rel__simps_I13_J,fact_rel__simps_I9_J,fact_bin__less__0__simps_I2_J,fact_rel__simps_I3_J,fact_rel__simps_I6_J,fact_rel__simps_I8_J,fact_eq__number__of__Pls__Min,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I32_J,fact_power__0,fact_nat__one__le__power,fact_power__le__dvd,fact_dvd__power__le,fact_le__imp__power__dvd,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_dvd__imp__le,fact_nat__mult__le__cancel1,fact_mult__le__cancel2,fact_mult__le__cancel1,fact_zdvd__imp__le,fact_Suc__mult__le__cancel1,fact_zadd__zless__mono,fact_power__mono__odd,fact_int__0__less__1,fact_Bit1__def,fact_odd__nonzero,fact_zless__add1__eq,fact_nonzero__number__of__Min,fact_less__add__iff1,fact_less__add__iff2,fact_inf__period_I4_J,fact_inf__period_I3_J,fact_add__number__of__diff1,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_add__pos__nonneg,fact_add__nonneg__pos,fact_add__strict__increasing,fact_add__strict__increasing2,fact_add__neg__nonpos,fact_add__nonpos__neg,fact_sum__squares__le__zero__iff,fact_sum__squares__ge__zero,fact_zero__less__two,fact_int__pos__lt__two__imp__zero__or__one,fact_power__less__imp__less__base,fact_power__strict__decreasing,fact_power__gt1__lemma,fact_power__less__power__Suc,fact_power__eq__imp__eq__base,fact_power__0__left,fact_power__le__imp__le__base,fact_power__inject__base,fact_one__less__power,fact_number__of__Bit1,fact_power__gt1,fact_semiring__norm_I110_J,fact_numeral__1__eq__1,fact_neg__one__odd__power,fact_dvd__power,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_one__le__mult__iff,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_number__of2,fact_one__is__num__one,fact_odd__less__0,fact_pos__zmult__eq__1__iff,fact_power__m1__even,fact_real__mult__right__cancel,fact_real__mult__left__cancel,fact_real__mult__commute,fact_real__mult__assoc,fact_real__add__mult__distrib,fact_real__mult__less__mono2,fact_real__mult__order,fact_real__mult__less__iff1,fact_real__two__squares__add__zero__iff,fact_realpow__two__diff,fact_power__Suc__less,fact_power__strict__mono,fact_power__Suc__less__one,fact_Suc__diff__eq__diff__pred,fact_double__number__of__Bit0,fact_power__0__left__number__of,fact_power__le__zero__eq,fact_zero__le__power__eq__number__of,fact_number__of1,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_power__le__zero__eq__number__of,fact_zero__le__power2,fact_power2__le__imp__le,fact_power2__eq__imp__eq,fact_power2__less__imp__less,fact_sum__power2__ge__zero,fact_sum__power2__le__zero__iff,fact_zero__le__even__power_H,fact_even__power__le__0__imp__0,fact_self__quotient__aux2,fact_self__quotient__aux1,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I7_J,fact_q__pos__lemma,fact_q__neg__lemma,fact_real__mult__1,fact_diff__Suc__1,fact_diff__Suc__eq__diff__pred,fact_real__zero__not__eq__one,fact_zle__refl,fact_zle__linear,fact_zle__trans,fact_zle__antisym,fact_real__le__antisym,fact_real__le__trans,fact_real__le__linear,fact_real__le__refl,fact_le__refl,fact_diff__le__self,fact_nat__le__linear,fact_diff__commute,fact_eq__imp__le,fact_diff__le__mono2,fact_diff__le__mono,fact_diff__diff__cancel,fact_le__trans,fact_le__antisym,fact_eq__diff__iff,fact_Nat_Odiff__diff__eq,fact_le__diff__iff,fact_comm__semiring__1__class_Onormalizing__semiring__rules_I33_J,fact_power__one__right,fact_nat__dvd__1__iff__1,fact_nat__mult__1,fact_nat__1__eq__mult__iff,fact_nat__mult__1__right,fact_nat__mult__eq__1__iff,fact_odd__1__nat,fact_One__nat__def,fact_Suc__eq__plus1,fact_Suc__eq__plus1__left,fact_mult__eq__self__implies__10,fact_Suc__diff__1,fact_Suc__pred_H,fact_add__eq__if,fact_nat__numeral__1__eq__1,fact_Numeral1__eq1__nat,fact_mult__eq__if,fact_even__num__iff,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I5_J,fact_power__eq__if,fact_power__dvd__imp__le,fact_realpow__minus__mult,fact_expand__Suc,fact_dvd__mult__cancel1,fact_dvd__mult__cancel2,fact_nat__1__add__1,fact_two__realpow__ge__one,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_Nat__Transfer_Otransfer__nat__int__function__closures_I4_J,fact_Nat__Transfer_Otransfer__nat__int__function__closures_I8_J,fact_zdiv__mono2__neg__lemma,fact_unique__quotient__lemma__neg,fact_zdiv__mono2__lemma,fact_unique__quotient__lemma,fact_lemma__realpow__diff,fact_realpow__num__eq__if,fact_pow__divides__eq__int,fact_pow__divides__pow__int,fact_gcd__lcm__complete__lattice__nat_Otop__greatest,fact_gcd__lcm__complete__lattice__nat_Obot__least,fact_dvd__pos__nat,fact_pow__divides__pow__nat,fact_pow__divides__eq__nat,fact_zmod__number__of__Bit1,fact_neg__zmod__mult__2,fact_zdvd__zmod__imp__zdvd,fact_zdvd__zmod,fact_zpower__zmod,fact_zmod__eq__dvd__iff,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_dvd__mod__iff,fact_mod__mod__cancel,fact_dvd__mod,fact_dvd__mod__imp__dvd,fact_zmod__zero,fact_zmod__self,fact_zmod__le__nonneg__dividend,fact_Divides_Otransfer__nat__int__function__closures_I2_J,fact_mod__diff__cong,fact_zdiff__zmod__left,fact_zdiff__zmod__right,fact_mod__diff__eq,fact_mod__diff__left__eq,fact_mod__diff__right__eq,fact_mod__0,fact_mod__by__0,fact_mod__self,fact_mod__mult__self1__is__0,fact_mod__mult__self2__is__0,fact_mod__mult__self2,fact_mod__mult__self1,fact_dvd__eq__mod__eq__0,fact_dvd__imp__mod__0,fact_mod__mod__trivial,fact_zmod__simps_I3_J,fact_zmod__zmult1__eq,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_neg__mod__bound,fact_pos__mod__bound,fact_zmod__eq__0__iff,fact_dvd__eq__mod__eq__0__number__of,fact_mod__by__1,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_zmod__minus1__right,fact_zdvd__iff__zmod__eq__0__number__of,fact_mod__pos__neg__trivial,fact_zmod__number__of__Bit0,fact_split__zmod,fact_zmult2__lemma__aux3,fact_zmult2__lemma__aux4,fact_zmult2__lemma__aux1,fact_zmult2__lemma__aux2,fact_divmod__int__rel__mod__eq,fact_neq__one__mod__two,fact_even__def,fact_zmod__minus1,fact_pos__zmod__mult__2,fact_neg__zdiv__mult__2,fact_pos__zdiv__mult__2,fact_mod__mult__self4,fact_mod__less,fact_mod__geq,fact_zdiv__zadd1__eq,fact_mod__if,fact_DIVISION__BY__ZERO,fact_mod__div__trivial,fact_zmod__zdiv__trivial,fact_le__mod__geq,fact_mod__less__eq__dividend,fact_mod__mult__distrib2,fact_mod__mult__distrib,fact_mod__Suc__eq__Suc__mod,fact_mod__Suc,fact_mod__1,fact_mod__less__divisor,fact_mod__eq__0__iff,fact_mod__mult__self3,fact_mod__le__divisor,fact_odd__nat__mod__two__eq__one,fact_even__nat__mod__two__eq__zero,fact_odd__nat__equiv__def,fact_even__nat__equiv__def,fact_div__by__1,fact_zdiv__self,fact_div__self,fact_zdiv__mono1__neg,fact_zdiv__mono1,fact_div__neg__neg__trivial,fact_zdiv__mono2__neg,fact_div__nonpos__pos__le0,fact_neg__imp__zdiv__nonneg__iff,fact_div__pos__pos__trivial,fact_div__nonneg__neg__le0,fact_zdiv__mono2,fact_nonneg1__imp__zdiv__pos__iff,fact_pos__imp__zdiv__pos__iff,fact_pos__imp__zdiv__nonneg__iff,fact_zdiv__eq__0__iff,fact_int__div__less__self,fact_zdiv__zmult2__eq,fact_div__power,fact_div__add,fact_dvd__mult__div__cancel,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__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_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__Groups_Oab__group__add,arity_Int__Oint__Rings_Ozero__neq__one,arity_Int__Oint__Rings_Oordered__ring,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__Divides_Oring__div,arity_Int__Oint__Rings_Omult__zero,arity_Int__Oint__Rings_Ocomm__ring,arity_Int__Oint__Int_Oring__char__0,arity_Int__Oint__Int_Onumber__ring,arity_Int__Oint__Rings_Osemiring,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_Int__Oint__Rings_Odvd,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_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__Rings_Osemiring,arity_Nat__Onat__Power_Opower,arity_Nat__Onat__Groups_Ozero,arity_Nat__Onat__Int_Onumber,arity_Nat__Onat__Groups_Oone,arity_Nat__Onat__Rings_Odvd,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__Rings_Olinordered__semiring__1__strict,arity_RealDef__Oreal__Rings_Olinordered__semiring__strict,arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add,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__Rings_Olinordered__ring__strict,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__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__Rings_Oordered__semiring,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_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_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__Rings_Ocomm__ring,arity_RealDef__Oreal__Int_Oring__char__0,arity_RealDef__Oreal__Int_Onumber__ring,arity_RealDef__Oreal__Rings_Osemiring,arity_RealDef__Oreal__Rings_Oring__1,arity_RealDef__Oreal__Power_Opower,arity_RealDef__Oreal__Groups_Ozero,arity_RealDef__Oreal__Rings_Oring,arity_RealDef__Oreal__Rings_Oidom,arity_RealDef__Oreal__Int_Onumber,arity_RealDef__Oreal__Groups_Oone,arity_RealDef__Oreal__Rings_Odvd,arity_Complex__Ocomplex__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct,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__Rings_Oring__no__zero__divisors,arity_Complex__Ocomplex__Groups_Ocancel__semigroup__add,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_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__Rings_Ocomm__ring,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__Power_Opower,arity_Complex__Ocomplex__Groups_Ozero,arity_Complex__Ocomplex__Rings_Oring,arity_Complex__Ocomplex__Rings_Oidom,arity_Complex__Ocomplex__Int_Onumber,arity_Complex__Ocomplex__Groups_Oone,arity_Complex__Ocomplex__Rings_Odvd,conj_0] % 2.74/3.44 =============================================================== % 2.74/3.44 % 2.74/3.44 Combined formula: 1171 axiom(s) => conjecture % 2.74/3.44 % 2.74/3.44 % Equality/functions detected -> nanoCoP oracle mode % 2.74/3.44 nanoCoP : % 2.74/3.44 % 1,287,340 inferences, 1.536 CPU in 1.536 seconds (100% CPU, 837913 Lips) % 2.74/3.44 % 2.74/3.44 % nanoCoP proof (equality/functions) % 2.74/3.44 % nanoCoP proof is given at https://g4-mic.vidal-rosset.net/wasm/tinker via nanocop_proves(Your_Formula). % 2.74/3.44 % 2.74/3.44 % SZS output end Proof %------------------------------------------------------------------------------