NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 5: 3000 <= y_0 and y_0 <= 3000 and 3000 <= y_post and y_post <= 3000 and y_post-y_0 <= 0 and y_0-y_post <= 0 and y_post+y_0 <= 6000 and 6000 <= y_post+y_0 and y_0+-3999 <= 0
Errors: