NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 124: ___rho_1__0 == 0 and ___rho_2__0 == 0 and copied2_post == 0 and copied3_post == 0 and p_post == 0 and pc_post == 0 and ret_enc_LLe_p_1110_post == 1 and ret_enc_LLe_p_128_post == 1 and rv_LLe_p_0 == 1 and rv_LLe_p_post == 1 and rv_init_0 == 0 and start_post == 0 and var_LLe_p_11___rho_1__post == 0 and var_LLe_p_11___rho_2__post == 1 and var_LLe_p_11_p_0 == 1 and var_LLe_p_11_p_post == 1 and var_LLe_p_11_rv_init_post == 0 and var_LLe_p_11_start_post == 0 and var_LLe_p_11_x_post == 0 and var_LLe_p_12___rho_1__post == 0 and var_LLe_p_12___rho_2__post == 1 and var_LLe_p_12_p_0 == 1 and var_LLe_p_12_p_post == 1 and var_LLe_p_12_rv_init_post == 0 and var_LLe_p_12_start_post == 0 and var_LLe_p_12_x_post == 0 and var_Le_AGp_12___rho_1__0 == 0 and var_Le_AGp_12___rho_1__post == 0 and var_Le_AGp_12___rho_2__0 == 1 and var_Le_AGp_12___rho_2__post == 1 and var_Le_AGp_12_p_0 == 1 and var_Le_AGp_12_p_post == 1 and var_Le_AGp_12_rv_init_0 == 0 and var_Le_AGp_12_rv_init_post == 0 and var_Le_AGp_12_start_0 == 0 and var_Le_AGp_12_start_post == 0 and var_Le_AGp_12_x_0 == 0 and var_Le_AGp_12_x_post == 0 and var_e_AFAGp_0___rho_1__0 == 0 and var_e_AFAGp_0___rho_1__post == 0 and var_e_AFAGp_0___rho_2__0 == 1 and var_e_AFAGp_0___rho_2__post == 1 and var_e_AFAGp_0_p_post == 1 and var_e_AFAGp_0_rv_init_0 == 0 and var_e_AFAGp_0_rv_init_post == 0 and var_e_AFAGp_0_start_0 == 0 and var_e_AFAGp_0_start_1 == 1 and var_e_AFAGp_0_start_post == 0 and var_e_AFAGp_0_x_0 == 0 and var_e_AFAGp_0_x_post == 0 and x_0 == 0
Errors: