YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 23, 24, 25, 27, 28, 33, 35, 36, 41, 42, 43, 44, 46, 47, 52, 53, 54, 55, 56, 57, 59, 60, 65, 66, 67, 68, 69, 70, 72, 73, 78 using the following rank functions:
    - Rank function 1:
      RF for loc. 21: -14-16*m_0+16*n_0
      RF for loc. 23: -14-16*m_0+16*n_0
      RF for loc. 24: -16*m_0+16*n_0
      RF for loc. 25: -7-16*m_0+16*n_0
      RF for loc. 26: -7-16*m_0+16*n_0
      RF for loc. 27: -13-16*m_0+16*n_0
      RF for loc. 28: -13-16*m_0+16*n_0
      RF for loc. 29: -12-16*m_0+16*n_0
      RF for loc. 30: -10-16*m_0+16*n_0
      RF for loc. 31: -10-16*m_0+16*n_0
      RF for loc. 32: -11-16*m_0+16*n_0
      RF for loc. 33: -9-16*m_0+16*n_0
      RF for loc. 34: -8-16*m_0+16*n_0
      RF for loc. 35: 1-16*m_0+16*n_0
      RF for loc. 39: -7-16*m_0+16*n_0
      RF for loc. 43: -10-16*m_0+16*n_0
      RF for loc. 47: -13-16*m_0+16*n_0
      RF for loc. 51: -14-16*m_0+16*n_0
      Bound for (chained) transitions 78: 0
    - Rank function 2:
      RF for loc. 21: -j_0+k_0-3*m2_0+3*m2_post-m_0
      RF for loc. 23: 1-j_0+k_0-3*m2_0+3*m2_post-m_0
      RF for loc. 24: -1-3*j_0+k_0-m2_0+3*m2_post-m_0
      RF for loc. 25: 6
      RF for loc. 26: 6
      RF for loc. 27: 1
      RF for loc. 28: 1
      RF for loc. 29: 2
      RF for loc. 30: 4
      RF for loc. 31: 4
      RF for loc. 32: 3
      RF for loc. 33: 5
      RF for loc. 34: 6
      RF for loc. 35: -3*j_0+k_0-m2_0+3*m2_post-m_0
      RF for loc. 39: 6
      RF for loc. 43: 4
      RF for loc. 47: 1
      RF for loc. 51: 1-j_0+k_0-3*m2_0+3*m2_post-m_0
      Bound for (chained) transitions 41: 1
      Bound for (chained) transitions 43: 2
      Bound for (chained) transitions 52: 3
      Bound for (chained) transitions 53: 3
      Bound for (chained) transitions 55: 4
      Bound for (chained) transitions 56: 5
      Bound for (chained) transitions 65: 6
      Bound for (chained) transitions 67: 6
    - Rank function 3:
      RF for loc. 21: -1-j_0+2*k_0
      RF for loc. 23: 1-j_0+2*k_0
      RF for loc. 24: -3-j_0+2*k_0
      RF for loc. 25: -3*j_0+3*m_0
      RF for loc. 26: -2-3*j_0+3*m_0
      RF for loc. 27: -1-2*j_0+2*m_0
      RF for loc. 28: 1-2*j_0+2*m_0
      RF for loc. 30: 1-3*j_0
      RF for loc. 31: -1-3*j_0
      RF for loc. 33: -4-3*j_0+3*m_0
      RF for loc. 34: -3-3*j_0+3*m_0
      RF for loc. 35: -2-j_0+2*k_0
      RF for loc. 39: -1-3*j_0+3*m_0
      RF for loc. 43: -3*j_0
      RF for loc. 47: -2*j_0+2*m_0
      RF for loc. 51: -j_0+2*k_0
      Bound for (chained) transitions 68: -2
    - Rank function 4:
      RF for loc. 21: -4*j_0+2*k_0
      RF for loc. 23: 1-4*j_0+2*k_0
      RF for loc. 24: -2-4*j_0+2*k_0
      RF for loc. 25: 2
      RF for loc. 26: 0
      RF for loc. 27: -1-4*j_0
      RF for loc. 28: 1-4*j_0
      RF for loc. 30: -3*j_0
      RF for loc. 31: -2-3*j_0
      RF for loc. 33: -1
      RF for loc. 34: 0
      RF for loc. 35: -1-4*j_0+2*k_0
      RF for loc. 39: 1
      RF for loc. 43: -1-3*j_0
      RF for loc. 47: -4*j_0
      RF for loc. 51: 1-4*j_0+2*k_0
      Bound for (chained) transitions 36: 1
      Bound for (chained) transitions 66: 0
    - Rank function 5:
      RF for loc. 21: -4*j_0+2*k_0+4*m2_0
      RF for loc. 23: 2-4*j_0+2*k_0+4*m2_0
      RF for loc. 24: -2-4*j_0+2*k_0+4*m2_0
      RF for loc. 25: 1
      RF for loc. 26: -1
      RF for loc. 27: 0
      RF for loc. 28: 0
      RF for loc. 30: 2-4*j_0+4*m_0
      RF for loc. 31: -4*j_0+4*m_0
      RF for loc. 34: -1
      RF for loc. 35: -1-4*j_0+2*k_0+4*m2_0
      RF for loc. 39: 0
      RF for loc. 43: 1-4*j_0+4*m_0
      RF for loc. 47: 0
      RF for loc. 51: 1-4*j_0+2*k_0+4*m2_0
      Bound for (chained) transitions 33: 1
      Bound for (chained) transitions 35: 0
      Bound for (chained) transitions 54: 0
    - Rank function 6:
      RF for loc. 21: -j_0+m2_0
      RF for loc. 23: 1-j_0+m2_0
      RF for loc. 24: -2-j_0+m2_0
      RF for loc. 26: 1
      RF for loc. 27: 0
      RF for loc. 28: 0
      RF for loc. 30: 1
      RF for loc. 31: -1
      RF for loc. 34: 0
      RF for loc. 35: -1-j_0+m2_0
      RF for loc. 43: 0
      RF for loc. 47: 0
      RF for loc. 51: 1-j_0+m2_0
      Bound for (chained) transitions 44: 1
      Bound for (chained) transitions 46: 0
      Bound for (chained) transitions 47: 0
      Bound for (chained) transitions 69: 1
    - Rank function 7:
      RF for loc. 21: -1-2*j_0+k_0
      RF for loc. 23: 1-2*j_0+k_0
      RF for loc. 24: -2-2*j_0+k_0
      RF for loc. 27: -1-3*j_0+3*m_0
      RF for loc. 28: 1-3*j_0+3*m_0
      RF for loc. 35: -2-2*j_0+k_0
      RF for loc. 47: -3*j_0+3*m_0
      RF for loc. 51: -2*j_0+k_0
      Bound for (chained) transitions 42: -1
    - Rank function 8:
      RF for loc. 21: -1-j_0+2*k_0
      RF for loc. 23: 1-j_0+2*k_0
      RF for loc. 24: -3-j_0+2*k_0
      RF for loc. 27: -1
      RF for loc. 28: 1
      RF for loc. 35: -2-j_0+2*k_0
      RF for loc. 47: 0
      RF for loc. 51: -j_0+2*k_0
      Bound for (chained) transitions 59: 0
    - Rank function 9:
      RF for loc. 21: -4*j_0+2*k_0+4*m2_0
      RF for loc. 23: 2-4*j_0+2*k_0+4*m2_0
      RF for loc. 24: -2-4*j_0+2*k_0+4*m2_0
      RF for loc. 27: -2
      RF for loc. 28: 0
      RF for loc. 35: -1-4*j_0+2*k_0+4*m2_0
      RF for loc. 47: -1
      RF for loc. 51: 1-4*j_0+2*k_0+4*m2_0
      Bound for (chained) transitions 57: 0
    - Rank function 10:
      RF for loc. 21: -2*j_0+k_0+2*m2_0
      RF for loc. 23: 2-2*j_0+k_0+2*m2_0
      RF for loc. 24: -2-2*j_0+k_0+2*m2_0
      RF for loc. 27: 0
      RF for loc. 35: -1-2*j_0+k_0+2*m2_0
      RF for loc. 47: 1
      RF for loc. 51: 1-2*j_0+k_0+2*m2_0
      Bound for (chained) transitions 60: 1
    - Rank function 11:
      RF for loc. 21: -1-3*j_0+3*m2_0
      RF for loc. 23: 1-3*j_0+3*m2_0
      RF for loc. 24: -3-3*j_0+3*m2_0
      RF for loc. 35: -2-3*j_0+3*m2_0
      RF for loc. 51: -3*j_0+3*m2_0
      Bound for (chained) transitions 24: -1
    - Rank function 12:
      RF for loc. 21: -1
      RF for loc. 23: 1
      RF for loc. 24: -3
      RF for loc. 35: -2
      RF for loc. 51: 0
      Bound for (chained) transitions 23, 25: -1
      Bound for (chained) transitions 27: -2
      Bound for (chained) transitions 28: -2
      Bound for (chained) transitions 70: 1
      Bound for (chained) transitions 72: 0
      Bound for (chained) transitions 73: 0
Errors: