YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 69, 71, 72, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84 using the following rank functions:
    - Rank function 1:
      RF for loc. 66: -3+7*a_234_0
      RF for loc. 67: -4+7*a_234_0
      RF for loc. 68: 2+7*a_257_0
      RF for loc. 69: 1+7*a_257_0
      RF for loc. 70: 7*a_257_0
      RF for loc. 71: -1+7*a_257_0
      RF for loc. 79: -2+7*a_234_0
      Bound for (chained) transitions 72: -2
    - Rank function 2:
      RF for loc. 66: -3+7*a_234_0
      RF for loc. 67: -4+7*a_234_0
      RF for loc. 68: 2+7*a_257_0
      RF for loc. 69: 1+7*a_257_0
      RF for loc. 70: 7*a_257_0
      RF for loc. 71: -1+7*a_257_0
      RF for loc. 79: -2+7*a_234_0
      Bound for (chained) transitions 71: -2
    - Rank function 3:
      RF for loc. 66: 4
      RF for loc. 67: 3
      RF for loc. 68: 2
      RF for loc. 69: 1
      RF for loc. 70: 0
      RF for loc. 71: -1
      RF for loc. 79: -2*result_dot_nondet_sdv_special_RETURN_VALUE_13_0
      Bound for (chained) transitions 69, 84: -1
      Bound for (chained) transitions 75: 4
      Bound for (chained) transitions 76: 4
      Bound for (chained) transitions 77: 3
      Bound for (chained) transitions 78: 2
      Bound for (chained) transitions 79: 2
      Bound for (chained) transitions 80: 1
      Bound for (chained) transitions 81: 1
      Bound for (chained) transitions 82: 0
      Bound for (chained) transitions 83: 0
 * Removed transitions 86, 88, 89, 92, 93, 94, 95, 96, 97, 98, 99 using the following rank functions:
    - Rank function 1:
      RF for loc. 74: -3+6*a_144_0
      RF for loc. 75: -4+6*a_144_0
      RF for loc. 76: 1+6*a_181_0
      RF for loc. 77: 6*a_181_0
      RF for loc. 78: -1+6*a_181_0
      RF for loc. 83: -2+6*a_144_0
      Bound for (chained) transitions 88: -2
      Bound for (chained) transitions 89: -2
    - Rank function 2:
      RF for loc. 74: 3
      RF for loc. 75: 2
      RF for loc. 76: 1
      RF for loc. 77: 0
      RF for loc. 78: -1
      RF for loc. 83: -2
      Bound for (chained) transitions 86, 99: -1
      Bound for (chained) transitions 92: 3
      Bound for (chained) transitions 93: 3
      Bound for (chained) transitions 94: 2
      Bound for (chained) transitions 95: 1
      Bound for (chained) transitions 96: 1
      Bound for (chained) transitions 97: 0
      Bound for (chained) transitions 98: 0
 * Removed transitions 101, 103, 104 using the following rank functions:
    - Rank function 1:
      RF for loc. 72: 1-2*i_28_0+2*length_27_0
      RF for loc. 87: -2*i_28_0+2*length_27_0
      Bound for (chained) transitions 104: 2
    - Rank function 2:
      RF for loc. 72: -2*i_28_0+2*length_27_0
      RF for loc. 87: -1-2*i_28_0+2*length_27_0
      Bound for (chained) transitions 103: 1
    - Rank function 3:
      RF for loc. 72: 0
      RF for loc. 87: -1
      Bound for (chained) transitions 101: 0
Errors: