NO
Nontermination proof succeeded
Found this recurrent set for cutpoint 216: 1132 <= cmd1_0 and cmd1_0 <= 1132 and 19846 <= cmd2_0 and cmd2_0 <= 19846 and i1592_0 <= -1 and i1592_post <= -1 and i16_0 <= -1 and i16_post <= -1 and i1895_0 <= -1 and i1895_post <= -1 and i18_0 <= -1 and i18_post <= -1 and 0 <= i88_0 and 0 <= i88_post and zer_0 <= 0 and cmd1_0-cmd2_0 <= -18714 and cmd2_0-cmd1_0 <= 18714 and cmd1_0+cmd2_0 <= 20978 and 20978 <= cmd1_0+cmd2_0 and i1592_0-cmd1_0 <= -1133 and cmd1_0+i1592_0 <= 1131 and i1592_post-cmd1_0 <= -1133 and cmd1_0+i1592_post <= 1131 and i1895_0-cmd1_0 <= -1133 and cmd1_0+i1895_0 <= 1131 and i1895_post-cmd1_0 <= -1133 and cmd1_0+i1895_post <= 1131 and cmd1_0-i88_0 <= 1132 and 1132 <= cmd1_0+i88_0 and cmd1_0-i88_post <= 1132 and 1132 <= cmd1_0+i88_post and zer_0-cmd1_0 <= -1132 and cmd1_0+zer_0 <= 1132 and i1592_0-cmd2_0 <= -19847 and cmd2_0+i1592_0 <= 19845 and i1592_post-cmd2_0 <= -19847 and cmd2_0+i1592_post <= 19845 and i1895_0-cmd2_0 <= -19847 and cmd2_0+i1895_0 <= 19845 and i1895_post-cmd2_0 <= -19847 and cmd2_0+i1895_post <= 19845 and cmd2_0-i88_0 <= 19846 and 19846 <= cmd2_0+i88_0 and cmd2_0-i88_post <= 19846 and 19846 <= cmd2_0+i88_post and i1592_0+i1895_0 <= -2 and i1592_0+i1895_post <= -2 and i1592_0-i88_0 <= -1 and i1592_0-i88_post <= -1 and i1592_post-i1592_0 <= 0 and i1592_0-i1592_post <= 0 and i1592_post+i1592_0 <= -2 and i1592_post+i1895_0 <= -2 and i1592_post+i1895_post <= -2 and i1592_post-i88_0 <= -1 and i1592_post-i88_post <= -1 and i16_0-cmd1_0 <= -1133 and i16_0+cmd1_0 <= 1131 and i16_0-cmd2_0 <= -19847 and i16_0+cmd2_0 <= 19845 and i16_0+i1592_0 <= -2 and i16_0+i1592_post <= -2 and i16_0+i1895_0 <= -2 and i16_0+i1895_post <= -2 and i16_0+i18_0 <= -2 and i16_0+i18_post <= -2 and i16_0-i88_0 <= -1 and i16_0-i88_post <= -1 and i16_0+zer_0 <= -1 and i16_post-cmd1_0 <= -1133 and i16_post+cmd1_0 <= 1131 and i16_post-cmd2_0 <= -19847 and i16_post+cmd2_0 <= 19845 and i16_post+i1592_0 <= -2 and i16_post+i1592_post <= -2 and i16_post-i16_0 <= 0 and i16_0-i16_post <= 0 and i16_post+i16_0 <= -2 and i16_post+i1895_0 <= -2 and i16_post+i1895_post <= -2 and i16_post+i18_0 <= -2 and i16_post+i18_post <= -2 and i16_post-i88_0 <= -1 and i16_post-i88_post <= -1 and i16_post+zer_0 <= -1 and i1895_0-i88_0 <= -1 and i1895_0-i88_post <= -1 and i1895_post-i1895_0 <= 0 and i1895_0-i1895_post <= 0 and i1895_post+i1895_0 <= -2 and i1895_post-i88_0 <= -1 and i1895_post-i88_post <= -1 and i18_0-cmd1_0 <= -1133 and i18_0+cmd1_0 <= 1131 and i18_0-cmd2_0 <= -19847 and i18_0+cmd2_0 <= 19845 and i18_0+i1592_0 <= -2 and i18_0+i1592_post <= -2 and i18_0+i1895_0 <= -2 and i18_0+i1895_post <= -2 and i18_0-i88_0 <= -1 and i18_0-i88_post <= -1 and i18_0+zer_0 <= -1 and i18_post-cmd1_0 <= -1133 and i18_post+cmd1_0 <= 1131 and i18_post-cmd2_0 <= -19847 and i18_post+cmd2_0 <= 19845 and i18_post+i1592_0 <= -2 and i18_post+i1592_post <= -2 and i18_post+i1895_0 <= -2 and i18_post+i1895_post <= -2 and i18_post-i18_0 <= 0 and i18_0-i18_post <= 0 and i18_post+i18_0 <= -2 and i18_post-i88_0 <= -1 and i18_post-i88_post <= -1 and i18_post+zer_0 <= -1 and i88_post-i88_0 <= 0 and i88_0-i88_post <= 0 and 0 <= i88_post+i88_0 and zer_0-cmd2_0 <= -19846 and zer_0+cmd2_0 <= 19846 and zer_0+i1592_0 <= -1 and zer_0+i1592_post <= -1 and zer_0+i1895_0 <= -1 and zer_0+i1895_post <= -1 and zer_0-i88_0 <= 0 and zer_0-i88_post <= 0 and 0 <= 0
Errors: