NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 172: 0 <= p_post and p_post <= 0 and 0 <= pc_post and pc_post <= 0 and 0 <= var_e_AGAFp_0_p_post and var_e_AGAFp_0_p_post <= 0 and var_e_AGAFp_0_x_0 <= 0 and var_e_AGAFp_0_x_post <= 0 and x_0 <= 0 and p_post-pc_post <= 0 and pc_post-p_post <= 0 and p_post+pc_post <= 0 and 0 <= p_post+pc_post and p_post-var_e_AGAFp_0_p_post <= 0 and var_e_AGAFp_0_p_post-p_post <= 0 and p_post+var_e_AGAFp_0_p_post <= 0 and 0 <= p_post+var_e_AGAFp_0_p_post and var_e_AGAFp_0_x_0-p_post <= 0 and p_post+var_e_AGAFp_0_x_0 <= 0 and var_e_AGAFp_0_x_post-p_post <= 0 and p_post+var_e_AGAFp_0_x_post <= 0 and x_0-p_post <= 0 and p_post+x_0 <= 0 and pc_post-var_e_AGAFp_0_p_post <= 0 and var_e_AGAFp_0_p_post-pc_post <= 0 and pc_post+var_e_AGAFp_0_p_post <= 0 and 0 <= pc_post+var_e_AGAFp_0_p_post and var_e_AGAFp_0_x_0-pc_post <= 0 and pc_post+var_e_AGAFp_0_x_0 <= 0 and var_e_AGAFp_0_x_post-pc_post <= 0 and pc_post+var_e_AGAFp_0_x_post <= 0 and x_0-pc_post <= 0 and pc_post+x_0 <= 0 and var_e_AGAFp_0___rho_1__post-___rho_1__0 <= 0 and ___rho_1__0-var_e_AGAFp_0___rho_1__post <= 0 and var_e_AGAFp_0___rho_2__post-___rho_2__0 <= 0 and ___rho_2__0-var_e_AGAFp_0___rho_2__post <= 0 and var_e_AGAFp_0_x_0-var_e_AGAFp_0_p_post <= 0 and var_e_AGAFp_0_p_post+var_e_AGAFp_0_x_0 <= 0 and var_e_AGAFp_0_x_post-var_e_AGAFp_0_p_post <= 0 and var_e_AGAFp_0_p_post+var_e_AGAFp_0_x_post <= 0 and x_0-var_e_AGAFp_0_p_post <= 0 and var_e_AGAFp_0_p_post+x_0 <= 0 and var_e_AGAFp_0_rv_init_post-rv_init_0 <= 0 and rv_init_0-var_e_AGAFp_0_rv_init_post <= 0 and var_e_AGAFp_0_start_post-start_0 <= 0 and start_0-var_e_AGAFp_0_start_post <= 0 and var_e_AGAFp_0_x_post-var_e_AGAFp_0_x_0 <= 0 and var_e_AGAFp_0_x_0-var_e_AGAFp_0_x_post <= 0 and var_e_AGAFp_0_x_post+var_e_AGAFp_0_x_0 <= 0 and var_e_AGAFp_0_x_post-x_0 <= 0 and x_0-var_e_AGAFp_0_x_post <= 0 and var_e_AGAFp_0_x_post+x_0 <= 0 and var_e_AGAFp_0_y_post-var_e_AGAFp_0_y_0 <= 0 and var_e_AGAFp_0_y_0-var_e_AGAFp_0_y_post <= 0 and var_e_AGAFp_0_y_post-y_0 <= 0 and x_0-var_e_AGAFp_0_x_0 <= 0 and var_e_AGAFp_0_x_0-x_0 <= 0 and x_0+var_e_AGAFp_0_x_0 <= 0 and var_e_AGAFp_0_y_0-y_0 <= 0 and var_e_AGAFp_0_y_0 <= 0
Errors: