YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 131, 133, 134 using the following rank functions:
    - Rank function 1:
      RF for loc. 31: 1+2*arg1
      RF for loc. 84: 2*arg1
      Bound for (chained) transitions 134: 2
    - Rank function 2:
      RF for loc. 31: 1+2*arg1
      RF for loc. 84: 2*arg1
      Bound for (chained) transitions 133: 2
    - Rank function 3:
      RF for loc. 31: 0
      RF for loc. 84: -1
      Bound for (chained) transitions 131: 0
 * Removed transitions 121, 124, 125 using the following rank functions:
    - Rank function 1:
      RF for loc. 30: 1+arg2+arg3
      RF for loc. 80: arg2+arg3
      Bound for (chained) transitions 124: 2
      Bound for (chained) transitions 125: 2
    - Rank function 2:
      RF for loc. 30: 0
      RF for loc. 80: -1
      Bound for (chained) transitions 121: 0
 * Removed transitions 111, 114, 115 using the following rank functions:
    - Rank function 1:
      RF for loc. 29: arg2+arg3
      RF for loc. 76: -1+arg2+arg3
      Bound for (chained) transitions 114: 1
      Bound for (chained) transitions 115: 1
    - Rank function 2:
      RF for loc. 29: 0
      RF for loc. 76: -1
      Bound for (chained) transitions 111: 0
 * Removed transitions 101, 104, 105 using the following rank functions:
    - Rank function 1:
      RF for loc. 28: 1+arg2+arg3
      RF for loc. 72: arg2+arg3
      Bound for (chained) transitions 104: 2
      Bound for (chained) transitions 105: 2
    - Rank function 2:
      RF for loc. 28: 0
      RF for loc. 72: -1
      Bound for (chained) transitions 101: 0
 * Removed transitions 91, 94, 95 using the following rank functions:
    - Rank function 1:
      RF for loc. 27: 1+arg2+arg3
      RF for loc. 68: arg2+arg3
      Bound for (chained) transitions 94: 2
      Bound for (chained) transitions 95: 2
    - Rank function 2:
      RF for loc. 27: 0
      RF for loc. 68: -1
      Bound for (chained) transitions 91: 0
 * Removed transitions 81, 84, 85 using the following rank functions:
    - Rank function 1:
      RF for loc. 26: 1+arg2+arg3
      RF for loc. 64: arg2+arg3
      Bound for (chained) transitions 84: 2
      Bound for (chained) transitions 85: 2
    - Rank function 2:
      RF for loc. 26: 0
      RF for loc. 64: -1
      Bound for (chained) transitions 81: 0
 * Removed transitions 71, 74, 75 using the following rank functions:
    - Rank function 1:
      RF for loc. 25: 1+arg2+arg3
      RF for loc. 60: arg2+arg3
      Bound for (chained) transitions 74: 2
      Bound for (chained) transitions 75: 2
    - Rank function 2:
      RF for loc. 25: 0
      RF for loc. 60: -1
      Bound for (chained) transitions 71: 0
 * Removed transitions 61, 64, 65 using the following rank functions:
    - Rank function 1:
      RF for loc. 24: 1+arg2+arg3
      RF for loc. 56: arg2+arg3
      Bound for (chained) transitions 64: 2
      Bound for (chained) transitions 65: 2
    - Rank function 2:
      RF for loc. 24: 1
      RF for loc. 56: 0
      Bound for (chained) transitions 61: 1
 * Removed transitions 51, 54, 55 using the following rank functions:
    - Rank function 1:
      RF for loc. 23: 1+arg2+arg3
      RF for loc. 52: arg2+arg3
      Bound for (chained) transitions 54: 2
      Bound for (chained) transitions 55: 2
    - Rank function 2:
      RF for loc. 23: 1
      RF for loc. 52: 0
      Bound for (chained) transitions 51: 1
 * Removed transitions 41, 44, 45 using the following rank functions:
    - Rank function 1:
      RF for loc. 22: 1+arg2+arg3
      RF for loc. 48: arg2+arg3
      Bound for (chained) transitions 44: 2
      Bound for (chained) transitions 45: 2
    - Rank function 2:
      RF for loc. 22: 0
      RF for loc. 48: -1
      Bound for (chained) transitions 41: 0
 * Removed transitions 31, 34, 35 using the following rank functions:
    - Rank function 1:
      RF for loc. 21: arg2+arg3
      RF for loc. 44: -1+arg2+arg3
      Bound for (chained) transitions 34: 1
      Bound for (chained) transitions 35: 1
    - Rank function 2:
      RF for loc. 21: 0
      RF for loc. 44: -1
      Bound for (chained) transitions 31: 0
 * Removed transitions 21, 24, 25 using the following rank functions:
    - Rank function 1:
      RF for loc. 20: 1+arg2+arg3
      RF for loc. 40: arg2+arg3
      Bound for (chained) transitions 24: 2
      Bound for (chained) transitions 25: 2
    - Rank function 2:
      RF for loc. 20: 0
      RF for loc. 40: -1
      Bound for (chained) transitions 21: 0
 * Removed transitions 5, 7, 8, 13, 14, 17, 18 using the following rank functions:
    - Rank function 1:
      RF for loc. 19: 2*arg1
      RF for loc. 32: 1+2*arg1
      RF for loc. 36: 2*arg1
      Bound for (chained) transitions 5, 13: 2
    - Rank function 2:
      RF for loc. 19: -arg2-arg3
      RF for loc. 32: 1-2*arg1
      RF for loc. 36: -1-arg2-arg3
      Bound for (chained) transitions 17: -199
      Bound for (chained) transitions 18: -199
    - Rank function 3:
      RF for loc. 19: 0
      RF for loc. 32: 1
      RF for loc. 36: -1
      Bound for (chained) transitions 8: 1
      Bound for (chained) transitions 14: 0
    - Rank function 4:
      RF for loc. 19: -1
      RF for loc. 32: 0
      Bound for (chained) transitions 7: 0
Errors: