NO Nontermination proof succeeded Found this recurrent set for cutpoint 19: Pdolen_0 == 0 and ___rho_1__0 == 0 and ___rho_1__post == 0 and i_0 == 0 and num_post == 0 and set_post == 0 and unset_0 == 0 and unset_1 == 1 and unset_post == 0 Errors: