YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 7, 9, 10, 15, 16, 18, 19 using the following rank functions:
    - Rank function 1:
      RF for loc. 11: 3*arg1
      RF for loc. 13: 1+3*arg1
      RF for loc. 17: 3*arg1
      Bound for (chained) transitions 7, 15: 6
      Bound for (chained) transitions 9: 7
      Bound for (chained) transitions 10: 7
    - Rank function 2:
      RF for loc. 11: 1-2*arg2+2*arg3
      RF for loc. 17: -2*arg2+2*arg3
      Bound for (chained) transitions 18: 2
      Bound for (chained) transitions 19: 2
    - Rank function 3:
      RF for loc. 11: 0
      RF for loc. 17: -1
      Bound for (chained) transitions 16: 0
 * Removed transitions 22, 25, 26, 27 using the following rank functions:
    - Rank function 1:
      RF for loc. 12: 1+arg2
      RF for loc. 21: arg2
      Bound for (chained) transitions 25: 3
      Bound for (chained) transitions 26: 3
      Bound for (chained) transitions 27: 3
    - Rank function 2:
      RF for loc. 12: 0
      RF for loc. 21: -1
      Bound for (chained) transitions 22: 0
Errors: