FAILED
Error message:
[Error on node 575:problem in checking validity of formula Disj[False, Disj[! (xv3098 = 0), ! (xv3100 = xv3099), ! (xv3089 = xv3100), ! (xv3090 = xv3097), xv3097 = 1, ! (xv3097 < 1), ! (xv3098 <= 0), ! (0 <= xv3098), ! (xv3100 <= xv3099), ! (xv3099 <= xv3100), ! (xv3089 <= xv3100), ! (xv3100 <= xv3089), ! (xv3090 <= xv3097), ! (xv3097 <= xv3090)], xv3093 = 1, Conj[True, Conj[xv3098 = 0, xv3100 = xv3099, xv3089 = xv3100, xv3090 = xv3097, xv3093 = 0, ! (xv3097 = 1), xv3097 < 1, xv3098 <= 0, 0 <= xv3098, xv3100 <= xv3099, xv3099 <= xv3100, xv3089 <= xv3100, xv3100 <= xv3089, xv3090 <= xv3097, xv3097 <= xv3090, xv3097 <= 1]]]
Could not prove unsatisfiability of IA conjunction
-1*xv3098 = 0 && xv3099 + -1*xv3100 = 0 && xv3100 + -1*xv3089 = 0 && xv3097 + -1*xv3090 = 0 && -1*xv3097 >= 0 && -1*xv3097 >= 0 && -1*xv3098 >= 0 && xv3098 >= 0 && xv3099 + -1*xv3100 >= 0 && xv3100 + -1*xv3099 >= 0 && xv3100 + -1*xv3089 >= 0 && xv3089 + -1*xv3100 >= 0 && xv3097 + -1*xv3090 >= 0 && xv3090 + -1*xv3097 >= 0 && -1*xv3093 >= 0 && -1*xv3093 + -1 >= 0
The linear inequalities
  -1*xv3098 = 0
  xv3099 + -1*xv3100 = 0
  xv3100 + -1*xv3089 = 0
  xv3097 + -1*xv3090 = 0
  -1*xv3097 >= 0
  -1*xv3097 >= 0
  -1*xv3098 >= 0
  xv3098 >= 0
  xv3099 + -1*xv3100 >= 0
  xv3100 + -1*xv3099 >= 0
  xv3100 + -1*xv3089 >= 0
  xv3089 + -1*xv3100 >= 0
  xv3097 + -1*xv3090 >= 0
  xv3090 + -1*xv3097 >= 0
  -1*xv3093 >= 0
  -1*xv3093 + -1 >= 0
cannot be proved unsatisfiable via hints
  Simplex
could not use simplex algorithm to prove unsatisfiability]
       15.02 real        28.68 user         5.34 sys