YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 10, 11, 12, 13, 15, 16, 21, 23, 24, 29, 30, 31, 32, 33 using the following rank functions:
    - Rank function 1:
      RF for loc. 12: -3*i_0+3*n_0
      RF for loc. 14: -3*i_0+3*n_0
      RF for loc. 15: 1-3*i_0+3*n_0
      RF for loc. 16: -3*i_0+3*n_0
      RF for loc. 17: -3*i_0+3*n_0
      RF for loc. 18: -1-3*i_0+3*n_0
      RF for loc. 19: 2-3*i_0+3*n_0
      RF for loc. 23: -3*i_0+3*n_0
      Bound for (chained) transitions 12: 4
    - Rank function 2:
      RF for loc. 12: 1-6*j_0+6*n_0
      RF for loc. 14: -6*j_0+6*n_0
      RF for loc. 15: -1-6*j_0+6*n_0
      RF for loc. 16: 3-6*j_0+6*n_0
      RF for loc. 17: -2-6*j_0+6*n_0
      RF for loc. 18: -1-6*j_0+6*n_0
      RF for loc. 19: -6*j_0+6*n_0
      RF for loc. 23: 2-6*j_0+6*n_0
      Bound for (chained) transitions 11: 7
    - Rank function 3:
      RF for loc. 12: -5
      RF for loc. 14: 0
      RF for loc. 15: -7
      RF for loc. 16: -3
      RF for loc. 17: -2
      RF for loc. 18: -1
      RF for loc. 19: -6
      RF for loc. 23: -4
      Bound for (chained) transitions 10, 13: -5
      Bound for (chained) transitions 15: -6
      Bound for (chained) transitions 21: -3
      Bound for (chained) transitions 23: -4
      Bound for (chained) transitions 24: -4
      Bound for (chained) transitions 29: -2
      Bound for (chained) transitions 30: -1
      Bound for (chained) transitions 31: 0
      Bound for (chained) transitions 32: 0
      Bound for (chained) transitions 33: 0
    - Rank function 4:
      RF for loc. 15: 0
      RF for loc. 19: 1
      Bound for (chained) transitions 16: 1
Errors: