YES


Termination: (Ranking Functions Found)
------------
l10: < < k_0 -kk_0 > >
l11: < < k_0 -kk_0 > >
l12: < < k_0 -kk_0 > >
l13: < < k_0 -kk_0 > >
l14: < < k_0 -kk_0 > >
l15: < < k_0 -kk_0 >, < -2 * j_0 + 4 * m_0 > >
l16: < < k_0 -kk_0 >, < -2 * j_0 + m4_0 > >
l17: < < k_0 -kk_0 >, < -3 * joff_0 >, < 4 * facm_0 -j_0 > >
l18: < < k_0 -kk_0 >, < 4 * facm_0 -3 * joff_0 -m43_0 >, < -joff_0 > >
l19: < < k_0 -kk_0 >, < -3 * joff_0 >, < -j_0 + 4 * m_0 > >
l20: < < k_0 -kk_0 >, < -3 * joff_0 >, < -joff_0 > >
l21: < < k_0 -kk_0 >, < -3 * joff_0 >, < -joff_0 > >
l22: < < k_0 -kk_0 >, < -3 * joff_0 >, < -joff_0 > >
l23: < < k_0 -kk_0 >, < -3 * joff_0 >, < -joff_0 > >
l24: < < k_0 -kk_0 >, < -3 * joff_0 >, < -joff_0 > >
l25: < < k_0 -kk_0 >, < -3 * joff_0 >, < -joff_0 > >
l26: < < k_0 -kk_0 >, < -3 * joff_0 >, < -joff_0 > >
l27: < < k_0 -kk_0 >, < -3 * joff_0 >, < -joff_0 > >
l28: < < k_0 -kk_0 >, < -3 * joff_0 >, < -joff_0 > >
l29: < < k_0 -kk_0 > >
l34: < < facm_0 -j_0 > >
l35: < < -j_0 + m_0 > >
l36: < < -2 * j_0 + 2 * mm_0 > >
l37: < < -2 -2 * j_0 + 2 * mm_0 >, < -2 * j_0 + 4 * m_0 > >
l39: < < 4 * facm_0 -2 * j_0 >, < -2 * j_0 + m4_0 > >
l40: < < 4 * facm_0 -2 * j_0 >, < 4 * facm_0 -2 * j_0 > >
l41: < < -2 * j_0 + m4_0 >, < 4 * facm_0 -2 * j_0 > >
l6: < < -1 + k_0 -kk_0 > >
l7: < < k_0 -kk_0 > >
l8: < < k_0 -kk_0 > >
l9: < < k_0 -kk_0 > >


method 1