YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 267, 270, 271 using the following rank functions:
    - Rank function 1:
      RF for loc. 38: 1+2*arg2
      RF for loc. 87: 2*arg2
      Bound for (chained) transitions 270: 2
      Bound for (chained) transitions 271: 2
    - Rank function 2:
      RF for loc. 38: 1
      RF for loc. 87: 0
      Bound for (chained) transitions 267: 1
 * Removed transitions 242, 245, 246, 247, 248, 249, 250, 251, 252, 265, 266 using the following rank functions:
    - Rank function 1:
      RF for loc. 52: 3*arg7
      RF for loc. 53: 1+3*arg7
      RF for loc. 54: 1+3*arg5
      RF for loc. 83: -1+3*arg7
      Bound for (chained) transitions 245: 2
      Bound for (chained) transitions 246: 2
      Bound for (chained) transitions 247: 2
      Bound for (chained) transitions 248: 2
      Bound for (chained) transitions 249: 2
      Bound for (chained) transitions 250: 2
      Bound for (chained) transitions 251: 2
      Bound for (chained) transitions 252: 2
    - Rank function 2:
      RF for loc. 52: 0
      RF for loc. 53: arg2
      RF for loc. 54: arg2
      RF for loc. 83: -1
      Bound for (chained) transitions 242: 0
      Bound for (chained) transitions 265: 8
      Bound for (chained) transitions 266: 10
 * Removed transitions 219, 222, 223, 224, 225, 226, 227, 228, 229, 263, 264 using the following rank functions:
    - Rank function 1:
      RF for loc. 49: 3*arg7
      RF for loc. 50: 1+3*arg7
      RF for loc. 51: 1+3*arg5
      RF for loc. 79: -1+3*arg7
      Bound for (chained) transitions 222: 2
      Bound for (chained) transitions 223: 2
      Bound for (chained) transitions 224: 2
      Bound for (chained) transitions 225: 2
      Bound for (chained) transitions 226: 2
      Bound for (chained) transitions 227: 2
      Bound for (chained) transitions 228: 2
    - Rank function 2:
      RF for loc. 49: 0
      RF for loc. 50: arg2
      RF for loc. 51: 1-3*arg4
      RF for loc. 79: -1
      Bound for (chained) transitions 219: 0
      Bound for (chained) transitions 229: -1
      Bound for (chained) transitions 263: 8
      Bound for (chained) transitions 264: 1
 * Removed transitions 206, 211, 212 using the following rank functions:
    - Rank function 1:
      RF for loc. 48: 1+2*arg5
      RF for loc. 75: 2*arg5
      Bound for (chained) transitions 211: 2
      Bound for (chained) transitions 212: 2
    - Rank function 2:
      RF for loc. 48: 0
      RF for loc. 75: -1
      Bound for (chained) transitions 206: 0
 * Removed transitions 195, 200, 201 using the following rank functions:
    - Rank function 1:
      RF for loc. 47: 1+2*arg5
      RF for loc. 71: 2*arg5
      Bound for (chained) transitions 200: 2
      Bound for (chained) transitions 201: 2
    - Rank function 2:
      RF for loc. 47: 0
      RF for loc. 71: -1
      Bound for (chained) transitions 195: 0
 * Removed transitions 180, 183, 184, 185, 186, 187 using the following rank functions:
    - Rank function 1:
      RF for loc. 46: 1-2*arg4+2*arg5
      RF for loc. 67: -2*arg4+2*arg5
      Bound for (chained) transitions 183: 0
      Bound for (chained) transitions 184: 0
      Bound for (chained) transitions 185: 0
      Bound for (chained) transitions 186: 0
      Bound for (chained) transitions 187: 0
    - Rank function 2:
      RF for loc. 46: 1
      RF for loc. 67: 0
      Bound for (chained) transitions 180: 1
 * Removed transitions 161, 166, 167, 168, 169, 170 using the following rank functions:
    - Rank function 1:
      RF for loc. 45: 1+2*arg4-2*arg5
      RF for loc. 63: 2*arg4-2*arg5
      Bound for (chained) transitions 166: 2
      Bound for (chained) transitions 167: 2
      Bound for (chained) transitions 168: 2
      Bound for (chained) transitions 169: 2
      Bound for (chained) transitions 170: 2
    - Rank function 2:
      RF for loc. 45: 0
      RF for loc. 63: -1
      Bound for (chained) transitions 161: 0
 * Removed transitions 134, 139, 140, 141, 142, 143, 144, 145, 146, 159, 160 using the following rank functions:
    - Rank function 1:
      RF for loc. 42: 3*arg6
      RF for loc. 43: 1+3*arg7
      RF for loc. 44: 1+3*arg5
      RF for loc. 59: -1+3*arg6
      Bound for (chained) transitions 139: 2
      Bound for (chained) transitions 140: 2
      Bound for (chained) transitions 141: 2
      Bound for (chained) transitions 142: 2
      Bound for (chained) transitions 143: 2
      Bound for (chained) transitions 144: 2
      Bound for (chained) transitions 145: 2
      Bound for (chained) transitions 146: 2
    - Rank function 2:
      RF for loc. 42: 0
      RF for loc. 43: arg3
      RF for loc. 44: arg1
      RF for loc. 59: -1
      Bound for (chained) transitions 134: 0
      Bound for (chained) transitions 159: 3
      Bound for (chained) transitions 160: 1
 * Removed transitions 111, 116, 117, 118, 119, 120, 121, 122, 123, 157, 158 using the following rank functions:
    - Rank function 1:
      RF for loc. 39: 3*arg6
      RF for loc. 40: 1+3*arg7
      RF for loc. 41: 1+3*arg5
      RF for loc. 55: -1+3*arg6
      Bound for (chained) transitions 116: 2
      Bound for (chained) transitions 117: 2
      Bound for (chained) transitions 118: 2
      Bound for (chained) transitions 119: 2
      Bound for (chained) transitions 120: 2
      Bound for (chained) transitions 121: 2
      Bound for (chained) transitions 122: 2
      Bound for (chained) transitions 123: 2
    - Rank function 2:
      RF for loc. 39: 0
      RF for loc. 40: arg1
      RF for loc. 41: 1
      RF for loc. 55: -1
      Bound for (chained) transitions 111: 0
      Bound for (chained) transitions 157: 1
    - Rank function 3:
      RF for loc. 39: 0
      RF for loc. 41: arg2
      Bound for (chained) transitions 158: 10
Errors: