YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 14, 15, 16, 17, 19, 20, 25 using the following rank functions:
    - Rank function 1:
      RF for loc. 13: 5*N_0+-3-5*i_0
      RF for loc. 14: 5*N_0+-4-5*i_0
      RF for loc. 15: 5*N_0+-1-5*i_0
      RF for loc. 17: 5*N_0-5*i_0
      Bound for (chained) transitions 16: 4
    - Rank function 2:
      RF for loc. 13: 2
      RF for loc. 14: 1
      RF for loc. 15: -1
      RF for loc. 17: 0
      Bound for (chained) transitions 14: 2
      Bound for (chained) transitions 15: 2
      Bound for (chained) transitions 17, 25: 1
      Bound for (chained) transitions 19: 0
      Bound for (chained) transitions 20: 0
Errors: