YES Termination proof succeeded Initially, performed program simplifications using lexicographic rank functions: * Removed transitions 107, 109, 110, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122 using the following rank functions: - Rank function 1: RF for loc. 64: -3+7*a_305_0 RF for loc. 65: -4+7*a_305_0 RF for loc. 66: 2+7*a_328_0 RF for loc. 67: 1+7*a_328_0 RF for loc. 68: 7*a_328_0 RF for loc. 69: -1+7*a_328_0 RF for loc. 85: -2+7*a_305_0 Bound for (chained) transitions 110: -2 - Rank function 2: RF for loc. 64: -3+6*a_305_0 RF for loc. 65: -3+6*a_305_0 RF for loc. 66: 2+6*a_328_0 RF for loc. 67: 1+6*a_328_0 RF for loc. 68: 6*a_328_0 RF for loc. 69: -1+6*a_328_0 RF for loc. 85: -2+6*a_305_0 Bound for (chained) transitions 109: -2 - Rank function 3: RF for loc. 64: 4 RF for loc. 65: 3 RF for loc. 66: 2 RF for loc. 67: 1 RF for loc. 68: 0 RF for loc. 69: -1 RF for loc. 85: -result_dot_nondet_sdv_special_RETURN_VALUE_13_0 Bound for (chained) transitions 107, 122: -1 Bound for (chained) transitions 113: 4 Bound for (chained) transitions 114: 4 Bound for (chained) transitions 115: 3 Bound for (chained) transitions 116: 2 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 92, 94, 95, 98, 99, 100, 101, 102, 103, 104, 105 using the following rank functions: - Rank function 1: RF for loc. 72: -3+6*a_197_0 RF for loc. 73: -4+6*a_197_0 RF for loc. 74: 1+6*a_247_0 RF for loc. 75: 6*a_247_0 RF for loc. 76: -1+6*a_247_0 RF for loc. 81: -2+6*a_197_0 Bound for (chained) transitions 94: -2 Bound for (chained) transitions 95: -2 - Rank function 2: RF for loc. 72: 2 RF for loc. 73: 1 RF for loc. 74: 0 RF for loc. 75: -1 RF for loc. 76: -2 RF for loc. 81: -3 Bound for (chained) transitions 92, 105: -2 Bound for (chained) transitions 98: 2 Bound for (chained) transitions 99: 2 Bound for (chained) transitions 100: 1 Bound for (chained) transitions 101: 0 Bound for (chained) transitions 102: 0 Bound for (chained) transitions 103: -1 Bound for (chained) transitions 104: -1 * Removed transitions 85, 87, 88 using the following rank functions: - Rank function 1: RF for loc. 70: 1-2*i_44_0+2*length_43_0 RF for loc. 77: -2*i_44_0+2*length_43_0 Bound for (chained) transitions 87: 2 Bound for (chained) transitions 88: 2 - Rank function 2: RF for loc. 70: 1 RF for loc. 77: 0 Bound for (chained) transitions 85: 1 Errors: