YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 54, 92, 94, 95 using the following rank functions:
    - Rank function 1:
      RF for loc. 29: -1+2*x4_0
      RF for loc. 51: 2*x6_0
      Bound for (chained) transitions 54, 92: 1
    - Rank function 2:
      RF for loc. 29: 0
      RF for loc. 51: 1
      Bound for (chained) transitions 94: 1
      Bound for (chained) transitions 95: 1
 * Removed transitions 55, 56, 59, 60 using the following rank functions:
    - Rank function 1:
      RF for loc. 31: 1+2*x7_0
      RF for loc. 35: 2*x6_0
      Bound for (chained) transitions 59: 2
      Bound for (chained) transitions 60: 2
    - Rank function 2:
      RF for loc. 31: 1
      RF for loc. 35: 0
      Bound for (chained) transitions 55, 56: 1
 * Removed transitions 63, 65, 67, 68 using the following rank functions:
    - Rank function 1:
      RF for loc. 33: -15+x5_0
      RF for loc. 39: x5_0
      Bound for (chained) transitions 67: 16
      Bound for (chained) transitions 68: 16
    - Rank function 2:
      RF for loc. 33: 0
      RF for loc. 39: -1
      Bound for (chained) transitions 63, 65: 0
 * Removed transitions 53, 71, 72, 75, 76, 84, 86, 87 using the following rank functions:
    - Rank function 1:
      RF for loc. 28: 4*x5_0
      RF for loc. 43: 4*x5_0
      RF for loc. 47: -22207+4*x4_0
      Bound for (chained) transitions 53, 71, 75, 84: 22208
    - Rank function 2:
      RF for loc. 28: 2*x6_0
      RF for loc. 43: -1+2*x6_0
      RF for loc. 47: 695
      Bound for (chained) transitions 76: 3
      Bound for (chained) transitions 86: 695
      Bound for (chained) transitions 87: 695
    - Rank function 3:
      RF for loc. 28: 0
      RF for loc. 43: -1
      Bound for (chained) transitions 72: 0
Errors: