YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 128, 130, 131 using the following rank functions:
    - Rank function 1:
      RF for loc. 47: 1+2*x5_0
      RF for loc. 72: 2*x5_0
      Bound for (chained) transitions 130: 4
    - Rank function 2:
      RF for loc. 47: 1+2*x5_0
      RF for loc. 72: 2*x5_0
      Bound for (chained) transitions 131: 4
    - Rank function 3:
      RF for loc. 47: 0
      RF for loc. 72: -1
      Bound for (chained) transitions 128: 0
 * Removed transitions 75, 134, 136, 137 using the following rank functions:
    - Rank function 1:
      RF for loc. 32: 4+2*x4_0
      RF for loc. 76: 2*x4_0
      Bound for (chained) transitions 75, 134: 12
    - Rank function 2:
      RF for loc. 32: 0
      RF for loc. 76: 1
      Bound for (chained) transitions 136: 1
      Bound for (chained) transitions 137: 1
 * Removed transitions 95, 97, 98 using the following rank functions:
    - Rank function 1:
      RF for loc. 39: 1+2*x6_0
      RF for loc. 56: 2*x6_0
      Bound for (chained) transitions 97: 4
    - Rank function 2:
      RF for loc. 39: 1+2*x6_0
      RF for loc. 56: 2*x6_0
      Bound for (chained) transitions 98: 4
    - Rank function 3:
      RF for loc. 39: 0
      RF for loc. 56: -1
      Bound for (chained) transitions 95: 0
 * Removed transitions 101, 103, 105, 106 using the following rank functions:
    - Rank function 1:
      RF for loc. 40: -3+x5_0
      RF for loc. 60: x5_0
      Bound for (chained) transitions 105: 4
      Bound for (chained) transitions 106: 4
    - Rank function 2:
      RF for loc. 40: 0
      RF for loc. 60: -1
      Bound for (chained) transitions 101, 103: 0
 * Removed transitions 109, 111, 113, 114 using the following rank functions:
    - Rank function 1:
      RF for loc. 42: -31+x4_0
      RF for loc. 64: x4_0
      Bound for (chained) transitions 113: 32
      Bound for (chained) transitions 114: 32
    - Rank function 2:
      RF for loc. 42: 0
      RF for loc. 64: -1
      Bound for (chained) transitions 109, 111: 0
 * Removed transitions 117, 118, 119, 120, 123, 124 using the following rank functions:
    - Rank function 1:
      RF for loc. 44: -1+4*x3_0
      RF for loc. 46: 4*x3_0
      RF for loc. 68: 2+4*x3_0
      Bound for (chained) transitions 123: 6
      Bound for (chained) transitions 124: 6
    - Rank function 2:
      RF for loc. 44: -1
      RF for loc. 46: 0
      RF for loc. 68: -2
      Bound for (chained) transitions 117, 120: -1
      Bound for (chained) transitions 118: 0
      Bound for (chained) transitions 119: 0
 * Removed transitions 76, 78, 80, 81 using the following rank functions:
    - Rank function 1:
      RF for loc. 34: -31+x3_0
      RF for loc. 48: x3_0
      Bound for (chained) transitions 80: 32
      Bound for (chained) transitions 81: 32
    - Rank function 2:
      RF for loc. 34: 0
      RF for loc. 48: -1
      Bound for (chained) transitions 76, 78: 0
 * Removed transitions 84, 85, 86, 87, 90, 91 using the following rank functions:
    - Rank function 1:
      RF for loc. 36: -3+4*x2_0
      RF for loc. 38: -1+4*x2_0
      RF for loc. 52: 4*x2_0
      Bound for (chained) transitions 90: 4
      Bound for (chained) transitions 91: 4
    - Rank function 2:
      RF for loc. 36: 0
      RF for loc. 38: 1
      RF for loc. 52: -1
      Bound for (chained) transitions 84, 87: 0
      Bound for (chained) transitions 85: 1
      Bound for (chained) transitions 86: 1
Errors: