YES
Termination proof succeeded
Initially, performed program simplifications using lexicographic rank functions:
 * Removed transitions 92, 94, 95, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107 using the following rank functions:
    - Rank function 1:
      RF for loc. 99: -3+6*a_330_0
      RF for loc. 100: -3+6*a_330_0
      RF for loc. 101: 2+6*a_353_0
      RF for loc. 102: 1+6*a_353_0
      RF for loc. 103: 6*a_353_0
      RF for loc. 104: -1+6*a_353_0
      RF for loc. 112: -2+6*a_330_0
      Bound for (chained) transitions 94: -2
    - Rank function 2:
      RF for loc. 99: -3+6*a_330_0
      RF for loc. 100: -3+6*a_330_0
      RF for loc. 101: 2+6*a_353_0
      RF for loc. 102: 1+6*a_353_0
      RF for loc. 103: 6*a_353_0
      RF for loc. 104: -1+6*a_353_0
      RF for loc. 112: -2+6*a_330_0
      Bound for (chained) transitions 95: -2
    - Rank function 3:
      RF for loc. 99: 4
      RF for loc. 100: 3
      RF for loc. 101: 2
      RF for loc. 102: 1
      RF for loc. 103: 0
      RF for loc. 104: -1
      RF for loc. 112: -2
      Bound for (chained) transitions 92, 107: -1
      Bound for (chained) transitions 98: 4
      Bound for (chained) transitions 99: 4
      Bound for (chained) transitions 100: 3
      Bound for (chained) transitions 101: 2
      Bound for (chained) transitions 102: 2
      Bound for (chained) transitions 103: 1
      Bound for (chained) transitions 104: 1
      Bound for (chained) transitions 105: 0
      Bound for (chained) transitions 106: 0
 * Removed transitions 131, 133, 134, 137, 138, 139, 140, 141, 142, 143, 144 using the following rank functions:
    - Rank function 1:
      RF for loc. 93: -3+6*a_241_0
      RF for loc. 94: -4+6*a_241_0
      RF for loc. 95: 1+6*a_277_0
      RF for loc. 96: 6*a_277_0
      RF for loc. 97: -1+6*a_277_0
      RF for loc. 124: -2+6*a_241_0
      Bound for (chained) transitions 133: -2
      Bound for (chained) transitions 134: -2
    - Rank function 2:
      RF for loc. 93: 3
      RF for loc. 94: 2
      RF for loc. 95: 1
      RF for loc. 96: 0
      RF for loc. 97: -1
      RF for loc. 124: -result_dot_nondet_sdv_special_RETURN_VALUE_13_0
      Bound for (chained) transitions 131, 144: -1
      Bound for (chained) transitions 137: 3
      Bound for (chained) transitions 138: 3
      Bound for (chained) transitions 139: 2
      Bound for (chained) transitions 140: 1
      Bound for (chained) transitions 141: 1
      Bound for (chained) transitions 142: 0
      Bound for (chained) transitions 143: 0
 * Removed transitions 109, 111, 112, 115, 116, 117, 118, 119, 120, 121, 122 using the following rank functions:
    - Rank function 1:
      RF for loc. 106: -3+6*a_147_0
      RF for loc. 107: -4+6*a_147_0
      RF for loc. 108: 1+6*a_184_0
      RF for loc. 109: 6*a_184_0
      RF for loc. 110: -1+6*a_184_0
      RF for loc. 116: -2+6*a_147_0
      Bound for (chained) transitions 111: -2
      Bound for (chained) transitions 112: -2
    - Rank function 2:
      RF for loc. 106: 3
      RF for loc. 107: 2
      RF for loc. 108: 1
      RF for loc. 109: 0
      RF for loc. 110: -1
      RF for loc. 116: -2*result_dot_nondet_sdv_special_RETURN_VALUE_13_0
      Bound for (chained) transitions 109, 122: -1
      Bound for (chained) transitions 115: 3
      Bound for (chained) transitions 116: 3
      Bound for (chained) transitions 117: 2
      Bound for (chained) transitions 118: 1
      Bound for (chained) transitions 119: 1
      Bound for (chained) transitions 120: 0
      Bound for (chained) transitions 121: 0
 * Removed transitions 124, 126, 127 using the following rank functions:
    - Rank function 1:
      RF for loc. 111: 1-2*i_30_0+2*length_29_0
      RF for loc. 120: -2*i_30_0+2*length_29_0
      Bound for (chained) transitions 126: 2
      Bound for (chained) transitions 127: 2
    - Rank function 2:
      RF for loc. 111: 0
      RF for loc. 120: -1
      Bound for (chained) transitions 124: 0
Errors: