NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 509: a_131_0 == 0 and a_131_post == 0 and a_195_0 == 0 and a_195_1 == 1 and a_195_post == 0 and a_235_post == 0 and a_354_0 == 0 and a_354_post == 0 and a_355_0 == 0 and a_355_post == 0 and a_450_0 == 0 and a_450_post == 0 and a_451_0 == 0 and a_451_post == 0 and a_509_0 == 0 and a_509_post == 0 and a_510_0 == 0 and a_510_post == 0 and a_656_0 == 0 and a_656_post == 0 and a_657_0 == 1 and a_78_post == 2 and a_911_0 == 0 and a_911_post == 0 and ct_18_0 == 0 and ct_18_post == 0 and f_804_0 == -1 and f_804_post == -1 and h_15_0 == -1 and h_15_post == -1 and h_32_0 == -1 and h_32_post == 0 and i_123_0 == 2 and i_123_post == 1 and i_225_0 == 1 and i_225_post == 1 and i_27_0 == 0 and i_27_1 == 0 and i_27_post == 0 and i_30_0 == 2 and i_30_1 == 2 and i_30_post == 2 and l_180_0 == 1 and l_29_0 == 2 and l_29_post == 0 and nd_12_1 == -1 and rt_11_1 == -1 and rv_13_0 == 2 and rv_13_post == 2 and rv_28_0 == -1 and rv_28_post == -1 and rv_33_post == 0 and st_31_1 == -1 and t_24_0 == -1 and t_24_post == -1 and t_34_post == 0 and t_790_0 == 1 and t_790_post == 1 and tp_35_0 == 16 and tp_35_post == 0 and x_14_0 == -1 and x_14_post == -1 and x_17_0 == -1 and x_17_post == -1 and x_19_0 == -1 and x_19_post == -1 and x_21_0 == -1 and x_21_post == -1 and y_20_0 == 0 and y_20_post == 0
Errors: