NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 30: a_131_post == 0 and a_195_0 == 1 and a_195_post == 1 and a_235_post == 0 and a_353_post == 0 and a_355_post == 1 and a_449_post == 0 and a_450_post == 0 and a_496_post == 0 and a_509_post == 1 and a_510_post == 0 and a_654_0 == 0 and a_655_0 == 0 and a_655_post == 0 and a_78_post == 2 and a_910_post == 0 and ct_18_post == 0 and f_793_post == 0 and h_15_0 == 0 and h_15_post == 0 and h_32_0 == 0 and h_32_post == 0 and i_123_0 == 2 and i_123_post == 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_180_post == 1 and l_29_0 == 2 and l_29_post == 0 and nd_12_1 == 0 and rt_11_1 == 0 and rv_13_post == 2 and rv_28_post == 0 and rv_33_post == 0 and st_31_1 == 0 and t_24_post == 0 and t_34_post == 0 and tp_35_0 == 14 and tp_35_post == 0 and x_14_post == 0 and x_17_post == 0 and x_19_post == 0 and x_21_0 == 0 and x_21_post == 0 and y_20_0 == 0 and y_20_post == 0
Errors: