YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 6 using the following rank functions:
    - Rank function 1:
      RF for loc. 7: arg2-arg3
      RF for loc. 8: 0
      Bound for (chained) transitions 6: 0
Used the following cutpoint-specific lexicographic rank functions:
 * For cutpoint 6, used the following rank functions/bounds (in descending priority order):
    - RF -arg3+arg1, bound 1
Errors: