YES


Termination: (Ranking Functions Found)
------------
l1: < < a_924_0 > >
l119: < < 2 * i_27_0 + i_30_0, 0 > >
l120: < < -a_1089_0 + a_1162_0 + i_1053_0 > >
l131: < < -2 + 2 * i_106_0 + i_107_0, 0 > >
l132: < < -2 + 2 * i_27_0 + i_30_0, 2 * i_27_0 > >
l133: < < -2 + 2 * i_27_0 + i_30_0, 2 * i_27_0 > >
l134: < < -2 + 2 * i_27_0 + i_30_0, 0 > >
l135: < < -2 + 2 * i_27_0 + i_30_0, 0 > >
l136: < < -2 + 2 * i_106_0 + i_107_0, 0 > >
l137: < < 2 * i_27_0 + i_30_0, 0 > >
l138: < < -2 + 2 * i_106_0 + i_107_0, 0 > >
l146: < < -i_30_0 + length_29_0 > >
l150: < < -a_1089_0 + a_1162_0 + i_1053_0 > >
l151: < < a_1162_0 > >
l152: < < a_1162_0 > >
l153: < < a_1162_0 > >
l154: < < a_1162_0 > >
l155: < < a_1162_0 > >
l156: < < a_1162_0 > >
l16: < < 1 + a_176_0 >, < -a_121_0 + 2 * a_176_0 + len_161_0 > >
l169: < < a_924_0 > >
l17: < < a_176_0 > >
l170: < < a_121_0 + a_924_0 -i_113_0 > >
l171: < < a_902_0 + a_924_0 -len_161_0 > >
l172: < < -1 + a_924_0 > >
l173: < < a_947_0 > >
l174: < < a_947_0 > >
l175: < < a_121_0 + a_924_0 -i_113_0 > >
l18: < < a_176_0 > >
l19: < < a_176_0 > >
l20: < < a_176_0 > >
l21: < < a_176_0 > >
l22: < < a_176_0 > >
l222: < < -1 -i_94_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 > >
l23: < < 1 + a_239_0 >, < a_121_0 + i_229_0 > >
l24: < < 1 + a_176_0 >, < a_121_0 + i_27_0 > >
l25: < < 1 + a_176_0 >, < a_121_0 + i_27_0 > >
l26: < < 1 + a_176_0 >, < -1 + i_113_0 + i_27_0 > >
l27: < < 1 + a_176_0 >, < -1 + i_113_0 + i_27_0 > >
l28: < < -a_121_0 + 2 * a_239_0 + len_161_0 >, < -1 + i_113_0 + i_229_0 > >
l29: < < 1 + a_239_0 >, < a_176_0 + i_27_0 + len_161_0 > >
l30: < < a_239_0 + i_229_0 -i_27_0 >, < a_239_0 + i_27_0 + len_161_0 > >
l31: < < 1 + a_239_0 >, < 1 + a_121_0 + i_27_0 > >
l32: < < 1 + a_239_0 >, < a_176_0 + i_27_0 + len_238_0 > >
l35: < < 1 + a_176_0 >, < 1 + a_176_0 > >
l36: < < a_176_0 >, < a_176_0 > >
l37: < < a_176_0 >, < a_176_0 > >
l38: < < a_176_0 >, < a_176_0 > >
l39: < < a_176_0 >, < a_176_0 > >
l40: < < a_176_0 >, < a_176_0 > >
l41: < < 1 + a_176_0 > >
l42: < < 1 + a_176_0 > >
l43: < < 1 + a_176_0 > >
l44: < < 1 + a_176_0 > >
l45: < < 1 + a_176_0 > >
l46: < < 2 + a_121_0 -len_161_0 > >
l47: < < 1 + a_176_0 > >
l48: < < 1 + a_176_0 > >
l49: < < i_27_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 >, < i_27_0 > >
l61: < < i_1248_0 >, < i_1248_0 -result_dot_nondet_sdv_special_RETURN_VALUE_13_0 > >
l62: < < 1 + i_27_0 >, < i_27_0 > >
l63: < < 1 + i_27_0 >, < i_27_0 > >
l64: < < 1 + i_27_0 >, < i_27_0 > >
l65: < < i_27_0 >, < i_27_0 > >
l66: < < i_1248_0 >, < i_27_0 > >
l67: < < 1 + i_27_0 >, < -1 + i_1248_0 > >
l68: < < i_1248_0 >, < i_27_0 > >
l8: < < 2 + a_121_0 -len_161_0 >, < 1 + a_121_0 + i_27_0 > >


method 1