YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 27, 28, 29, 38, 39, 40, 41, 42, 43, 44, 45, 47, 49, 50 using the following rank functions:
    - Rank function 1:
      RF for loc. 22: -7-8*i_0
      RF for loc. 23: -5-8*i_0
      RF for loc. 24: -6-8*i_0
      RF for loc. 25: -4-8*i_0
      RF for loc. 26: -3-8*i_0
      RF for loc. 27: -2-8*i_0
      RF for loc. 28: -1-8*i_0
      RF for loc. 41: -8*i_0
      Bound for (chained) transitions 45: -793
    - Rank function 2:
      RF for loc. 22: -5
      RF for loc. 23: -3
      RF for loc. 24: -4
      RF for loc. 25: -2
      RF for loc. 26: -1
      RF for loc. 27: 0
      RF for loc. 28: -7
      RF for loc. 41: -6
      Bound for (chained) transitions 27, 47: -5
      Bound for (chained) transitions 28: -3
      Bound for (chained) transitions 29: -4
      Bound for (chained) transitions 38: -2
      Bound for (chained) transitions 39: -2
      Bound for (chained) transitions 40: -2
      Bound for (chained) transitions 41: -1
      Bound for (chained) transitions 42: 0
      Bound for (chained) transitions 43: 0
      Bound for (chained) transitions 44: 0
      Bound for (chained) transitions 49: -6
      Bound for (chained) transitions 50: -6
 * Removed transitions 26, 30, 32, 33, 46, 55, 56, 57, 58, 59, 60, 61, 62, 63 using the following rank functions:
    - Rank function 1:
      RF for loc. 29: 1-7*i_0
      RF for loc. 30: -7*i_0
      RF for loc. 32: -4-7*i_0
      RF for loc. 33: -2-7*i_0
      RF for loc. 34: -3-7*i_0
      RF for loc. 35: -1-7*i_0
      RF for loc. 36: -1-7*i_0
      RF for loc. 37: 2-7*i_0
      Bound for (chained) transitions 26: -692
    - Rank function 2:
      RF for loc. 29: -7
      RF for loc. 30: 0
      RF for loc. 32: -5
      RF for loc. 33: -3
      RF for loc. 34: -4
      RF for loc. 35: -2
      RF for loc. 36: -1
      RF for loc. 37: -6
      Bound for (chained) transitions 30, 46: -5
      Bound for (chained) transitions 32: -6
      Bound for (chained) transitions 33: -6
      Bound for (chained) transitions 55: -3
      Bound for (chained) transitions 56: -4
      Bound for (chained) transitions 57: -2
      Bound for (chained) transitions 58: -2
      Bound for (chained) transitions 59: -2
      Bound for (chained) transitions 60: -1
      Bound for (chained) transitions 61: 0
      Bound for (chained) transitions 62: 0
      Bound for (chained) transitions 63: 0
Errors: