YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 28, 42, 44, 45 using the following rank functions:
    - Rank function 1:
      RF for loc. 23: 2*N6_0+-1-2*j7_0
      RF for loc. 37: 2*N6_0-2*j7_0
      Bound for (chained) transitions 28, 42: 3
    - Rank function 2:
      RF for loc. 23: -1
      RF for loc. 37: 0
      Bound for (chained) transitions 44: 0
      Bound for (chained) transitions 45: 0
 * Removed transitions 20, 22, 23, 29, 31, 32, 37, 38, 39, 40, 41, 51 using the following rank functions:
    - Rank function 1:
      RF for loc. 18: 9*N6_0-9*j7_0
      RF for loc. 19: 9*N6_0+-4-9*j7_0
      RF for loc. 20: 9*N6_0+-4-9*j7_0
      RF for loc. 21: 9*N6_0+-4-9*j7_0
      RF for loc. 22: 9*N6_0+-4-9*j7_0
      RF for loc. 29: 9*N6_0+1-9*j7_0
      RF for loc. 33: 9*N6_0+-4-9*j7_0
      Bound for (chained) transitions 51: 18
    - Rank function 2:
      RF for loc. 18: 4*N6_0+-2-4*i8_0
      RF for loc. 19: 4*N6_0+2-4*i8_0
      RF for loc. 20: 4*N6_0-4*i8_0
      RF for loc. 21: 4*N6_0+-2-4*i8_0
      RF for loc. 22: 4*N6_0+-1-4*i8_0
      RF for loc. 29: 4*N6_0+-1-4*i8_0
      RF for loc. 33: 4*N6_0+1-4*i8_0
      Bound for (chained) transitions 41: 4
    - Rank function 3:
      RF for loc. 18: -6
      RF for loc. 19: -2
      RF for loc. 20: -4
      RF for loc. 21: -1
      RF for loc. 22: 0
      RF for loc. 29: -5
      RF for loc. 33: -3
      Bound for (chained) transitions 20, 40: -4
      Bound for (chained) transitions 22: -5
      Bound for (chained) transitions 23: -5
      Bound for (chained) transitions 29: -2
      Bound for (chained) transitions 31: -3
      Bound for (chained) transitions 32: -3
      Bound for (chained) transitions 37: -1
      Bound for (chained) transitions 38: 0
      Bound for (chained) transitions 39: 0
 * Removed transitions 12, 14, 15, 53 using the following rank functions:
    - Rank function 1:
      RF for loc. 16: 2*N_0+-1-2*i_0
      RF for loc. 25: 2*N_0-2*i_0
      Bound for (chained) transitions 12, 53: 1
    - Rank function 2:
      RF for loc. 16: 0
      RF for loc. 25: 1
      Bound for (chained) transitions 14: 1
      Bound for (chained) transitions 15: 1
Errors: