YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 47, 48, 49, 50, 106, 108, 109 using the following rank functions:
    - Rank function 1:
      RF for loc. 37: -3-4*j24_0+4*len19_0
      RF for loc. 39: -2-4*j24_0+4*len19_0
      RF for loc. 40: -1-4*j24_0+4*len19_0
      RF for loc. 77: -4*j24_0+4*len19_0
      Bound for (chained) transitions 50: -1
    - Rank function 2:
      RF for loc. 37: 1
      RF for loc. 39: 2
      RF for loc. 40: -1
      RF for loc. 77: 0
      Bound for (chained) transitions 47, 106: 1
      Bound for (chained) transitions 48: 2
      Bound for (chained) transitions 49: 2
      Bound for (chained) transitions 108: 0
      Bound for (chained) transitions 109: 0
 * Removed transitions 51, 52, 53, 54, 55, 64, 85, 87, 88, 93, 95, 96 using the following rank functions:
    - Rank function 1:
      RF for loc. 41: 3*___const_255_0-3*j24_0
      RF for loc. 42: 3*___const_255_0-3*j24_0
      RF for loc. 43: 3*___const_255_0-3*j24_0
      RF for loc. 44: 3*___const_255_0-3*j24_0
      RF for loc. 46: 3*___const_255_0+1-3*j24_0
      RF for loc. 69: 3*___const_255_0+2-3*j24_0
      RF for loc. 73: 3*___const_255_0-3*j24_0
      Bound for (chained) transitions 64: 1
    - Rank function 2:
      RF for loc. 41: 5*___const_8_0+-2-5*i1128_0
      RF for loc. 42: 5*___const_8_0+2-5*i1128_0
      RF for loc. 43: 5*___const_8_0+-1-5*i1128_0
      RF for loc. 44: 5*___const_8_0-5*i1128_0
      RF for loc. 46: 5*___const_8_0+-2-5*i1128_0
      RF for loc. 69: 5*___const_8_0+-1-5*i1128_0
      RF for loc. 73: 5*___const_8_0+1-5*i1128_0
      Bound for (chained) transitions 55: 5
    - Rank function 3:
      RF for loc. 41: 2
      RF for loc. 42: 1
      RF for loc. 43: 3
      RF for loc. 44: -1
      RF for loc. 46: -3
      RF for loc. 69: -2
      RF for loc. 73: 0
      Bound for (chained) transitions 51: 2
      Bound for (chained) transitions 52: 3
      Bound for (chained) transitions 53: 3
      Bound for (chained) transitions 54, 85: -1
      Bound for (chained) transitions 87: -2
      Bound for (chained) transitions 88: -2
      Bound for (chained) transitions 93: 1
      Bound for (chained) transitions 95: 0
      Bound for (chained) transitions 96: 0
 * Removed transitions 73, 75, 76, 81, 82, 83, 84 using the following rank functions:
    - Rank function 1:
      RF for loc. 54: -4*j10_0+4*len5_0
      RF for loc. 55: -2-4*j10_0+4*len5_0
      RF for loc. 56: -1-4*j10_0+4*len5_0
      RF for loc. 65: 1-4*j10_0+4*len5_0
      Bound for (chained) transitions 84: 0
    - Rank function 2:
      RF for loc. 54: -1
      RF for loc. 55: 1
      RF for loc. 56: 2
      RF for loc. 65: 0
      Bound for (chained) transitions 73, 81: 1
      Bound for (chained) transitions 75: 0
      Bound for (chained) transitions 76: 0
      Bound for (chained) transitions 82: 2
      Bound for (chained) transitions 83: 2
 * Removed transitions 56, 58, 59, 65, 67, 68, 101, 102, 103, 104, 105, 114 using the following rank functions:
    - Rank function 1:
      RF for loc. 48: 3*___const_255_0-3*j10_0
      RF for loc. 49: 3*___const_255_0+-1-3*j10_0
      RF for loc. 50: 3*___const_255_0+-1-3*j10_0
      RF for loc. 51: 3*___const_255_0+-1-3*j10_0
      RF for loc. 52: 3*___const_255_0+-1-3*j10_0
      RF for loc. 57: 3*___const_255_0+1-3*j10_0
      RF for loc. 61: 3*___const_255_0+-1-3*j10_0
      Bound for (chained) transitions 114: 0
    - Rank function 2:
      RF for loc. 48: 5*___const_8_0+-2-5*i1114_0
      RF for loc. 49: 5*___const_8_0+2-5*i1114_0
      RF for loc. 50: 5*___const_8_0-5*i1114_0
      RF for loc. 51: 5*___const_8_0+-2-5*i1114_0
      RF for loc. 52: 5*___const_8_0+-1-5*i1114_0
      RF for loc. 57: 5*___const_8_0+-1-5*i1114_0
      RF for loc. 61: 5*___const_8_0+1-5*i1114_0
      Bound for (chained) transitions 105: 5
    - Rank function 3:
      RF for loc. 48: -6
      RF for loc. 49: -2
      RF for loc. 50: -4
      RF for loc. 51: -1
      RF for loc. 52: 0
      RF for loc. 57: -5
      RF for loc. 61: -3
      Bound for (chained) transitions 56, 104: -4
      Bound for (chained) transitions 58: -5
      Bound for (chained) transitions 59: -5
      Bound for (chained) transitions 65: -2
      Bound for (chained) transitions 67: -3
      Bound for (chained) transitions 68: -3
      Bound for (chained) transitions 101: -1
      Bound for (chained) transitions 102: 0
      Bound for (chained) transitions 103: 0
Errors: