YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 36, 38, 39 using the following rank functions:
    - Rank function 1:
      RF for loc. 11: 1+2*arg1
      RF for loc. 27: 2*arg1
      Bound for (chained) transitions 38: 2
      Bound for (chained) transitions 39: 2
    - Rank function 2:
      RF for loc. 11: 0
      RF for loc. 27: -1
      Bound for (chained) transitions 36: 0
 * Removed transitions 19, 21, 22, 27, 28, 30, 31, 32, 33 using the following rank functions:
    - Rank function 1:
      RF for loc. 13: -1+3*arg1
      RF for loc. 14: 3*arg1
      RF for loc. 19: -2+3*arg1
      RF for loc. 23: 3*arg1
      Bound for (chained) transitions 21: 1
      Bound for (chained) transitions 22: -2
      Bound for (chained) transitions 27: 0
      Bound for (chained) transitions 30: 0
      Bound for (chained) transitions 31: 0
    - Rank function 2:
      RF for loc. 13: 1
      RF for loc. 14: 1+arg2+arg3
      RF for loc. 19: 0
      RF for loc. 23: arg2+arg3
      Bound for (chained) transitions 19: 1
      Bound for (chained) transitions 32: 3
    - Rank function 3:
      RF for loc. 14: arg2+arg3
      RF for loc. 23: -1+arg2+arg3
      Bound for (chained) transitions 33: 1
    - Rank function 4:
      RF for loc. 14: 0
      RF for loc. 23: -1
      Bound for (chained) transitions 28: 0
 * Removed transitions 9, 12, 13 using the following rank functions:
    - Rank function 1:
      RF for loc. 12: 1+arg2+arg3
      RF for loc. 15: arg2+arg3
      Bound for (chained) transitions 12: 3
      Bound for (chained) transitions 13: 2
    - Rank function 2:
      RF for loc. 12: 1
      RF for loc. 15: 0
      Bound for (chained) transitions 9: 1
Errors: