NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 7: x_0-y_0 <= 0 and y_0-x_0 <= 0 and 0 <= 0
Errors: