NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 92: ___rho_1__0 == 0 and ___rho_2__0 == 0 and copied2_post == 0 and copied3_0 == 0 and copied3_post == 0 and ndi3_0 == 0 and ndi3_post == 0 and p_post == 0 and pc_post == 0 and ret_enc_LLe_p_98_post == 0 and ret_enc_Le_EGp_924_0 == 0 and ret_enc_Le_EGp_924_post == 0 and rv_LLe_p_0 == 0 and rv_LLe_p_post == 0 and rv_Le_EGp_0 == 0 and rv_Le_EGp_post == 0 and rv_init_0 == 0 and var_LLe_p_9___rho_1__post == 0 and var_LLe_p_9___rho_2__post == 0 and var_LLe_p_9_p_0 == 0 and var_LLe_p_9_p_post == 0 and var_LLe_p_9_rv_init_post == 0 and var_LLe_p_9_x_post == 0 and var_Le_EGp_9___rho_1__0 == 0 and var_Le_EGp_9___rho_1__post == 0 and var_Le_EGp_9___rho_2__0 == 0 and var_Le_EGp_9___rho_2__post == 0 and var_Le_EGp_9_p_0 == 0 and var_Le_EGp_9_p_post == 0 and var_Le_EGp_9_rv_init_0 == 0 and var_Le_EGp_9_rv_init_post == 0 and var_Le_EGp_9_x_0 == 0 and var_Le_EGp_9_x_post == 0 and var_e_EFEGp_0___rho_1__0 == 0 and var_e_EFEGp_0___rho_1__post == 0 and var_e_EFEGp_0___rho_2__0 == 0 and var_e_EFEGp_0___rho_2__post == 0 and var_e_EFEGp_0_p_0 == 0 and var_e_EFEGp_0_p_post == 0 and var_e_EFEGp_0_rv_init_0 == 0 and var_e_EFEGp_0_rv_init_post == 0 and var_e_EFEGp_0_x_0 == 0 and var_e_EFEGp_0_x_post == 0 and x_0 == 0
Errors: