YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 107, 110, 111 using the following rank functions:
    - Rank function 1:
      RF for loc. 23: 1
      RF for loc. 53: 0
      Bound for (chained) transitions 107: 1
      Bound for (chained) transitions 110: 0
      Bound for (chained) transitions 111: 0
 * Removed transitions 37, 38, 89, 92, 93, 101, 102, 103, 104, 105, 106 using the following rank functions:
    - Rank function 1:
      RF for loc. 18: -1+2*arg15-2*arg1+2*arg2-2*arg9
      RF for loc. 19: -1+2*arg18-2*arg1+2*arg2-2*arg9
      RF for loc. 20: -2*arg2+2*arg3+2*arg4-2*arg5
      RF for loc. 21: 2*arg13-2*arg1+2*arg2-2*arg8
      RF for loc. 22: -1+2*arg12-2*arg1+2*arg2-2*arg8
      RF for loc. 49: -1-2*arg2+2*arg3+2*arg4-2*arg5
      Bound for (chained) transitions 92: 3
    - Rank function 2:
      RF for loc. 18: 1-arg15-6*arg1+6*arg2+arg9
      RF for loc. 19: -arg18-6*arg1+6*arg2+arg9
      RF for loc. 20: 5-6*arg2+6*arg3-arg4+arg5
      RF for loc. 21: 2-arg13-6*arg1+6*arg2+arg8
      RF for loc. 22: -arg12-6*arg1+6*arg2+arg8
      RF for loc. 49: 4-6*arg2+6*arg3-arg4+arg5
      Bound for (chained) transitions 93: 11
    - Rank function 3:
      RF for loc. 18: 2
      RF for loc. 19: 1
      RF for loc. 20: 0
      RF for loc. 21: 3
      RF for loc. 22: 1
      RF for loc. 49: -1
      Bound for (chained) transitions 37: 2
      Bound for (chained) transitions 38: 2
      Bound for (chained) transitions 89: 0
      Bound for (chained) transitions 101: 3
      Bound for (chained) transitions 102: 3
      Bound for (chained) transitions 103: 1
      Bound for (chained) transitions 104: 1
      Bound for (chained) transitions 105: 1
      Bound for (chained) transitions 106: 1
 * Removed transitions 79, 83, 84 using the following rank functions:
    - Rank function 1:
      RF for loc. 28: 1-2*arg10+2*arg3
      RF for loc. 45: -2*arg10+2*arg3
      Bound for (chained) transitions 83: 2
      Bound for (chained) transitions 84: 2
    - Rank function 2:
      RF for loc. 28: 0
      RF for loc. 45: -1
      Bound for (chained) transitions 79: 0
 * Removed transitions 69, 73, 74 using the following rank functions:
    - Rank function 1:
      RF for loc. 27: 1-2*arg11+2*arg3
      RF for loc. 41: -2*arg11+2*arg3
      Bound for (chained) transitions 73: 2
      Bound for (chained) transitions 74: 2
    - Rank function 2:
      RF for loc. 27: 1
      RF for loc. 41: 0
      Bound for (chained) transitions 69: 1
 * Removed transitions 62, 65, 66 using the following rank functions:
    - Rank function 1:
      RF for loc. 26: 1+2*arg3-2*arg5
      RF for loc. 37: 2*arg3-2*arg5
      Bound for (chained) transitions 65: 2
      Bound for (chained) transitions 66: 2
    - Rank function 2:
      RF for loc. 26: 0
      RF for loc. 37: -1
      Bound for (chained) transitions 62: 0
 * Removed transitions 55, 58, 59 using the following rank functions:
    - Rank function 1:
      RF for loc. 25: 1+2*arg3-2*arg6
      RF for loc. 33: 2*arg3-2*arg6
      Bound for (chained) transitions 58: 2
      Bound for (chained) transitions 59: 2
    - Rank function 2:
      RF for loc. 25: 1
      RF for loc. 33: 0
      Bound for (chained) transitions 55: 1
 * Removed transitions 39, 43, 44, 45, 46, 47 using the following rank functions:
    - Rank function 1:
      RF for loc. 24: 1+arg13+arg19
      RF for loc. 29: arg13+arg19
      Bound for (chained) transitions 43: 2
      Bound for (chained) transitions 45: 2
      Bound for (chained) transitions 46: 2
      Bound for (chained) transitions 47: 2
    - Rank function 2:
      RF for loc. 24: 2*arg6
      RF for loc. 29: -2+2*arg6
      Bound for (chained) transitions 44: -2
    - Rank function 3:
      RF for loc. 24: 0
      RF for loc. 29: -1
      Bound for (chained) transitions 39: 0
Errors: