NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 7: 1 <= cnt_33_0 and 1 <= lt_12_1 and lt_10_1-cnt_40_0 <= 0 and 2 <= lt_12_1+cnt_33_0 and px_8_0-q_9_post <= 0 and q_9_post-px_8_0 <= 0 and px_8_post-px_8_0 <= 0 and px_8_0-px_8_post <= 0 and px_8_post-q_9_post <= 0 and q_9_post-px_8_post <= 0 and x_7_post-x_7_0 <= 0 and x_7_0-x_7_post <= 0 and y_5_0-y_5_post <= 0 and y_5_post-y_5_0 <= 0 and 0 <= 0
Errors: