FAILED
Error message:
[Error on node 653:problem in checking validity of formula Disj[False, Disj[! (xv3869 = xv3880), ! (xv3870 = xv3877), ! (xv3869 <= xv3880), ! (xv3880 <= xv3869), ! (xv3870 <= xv3877), ! (xv3877 <= xv3870)], xv3873 = 1, Conj[True, Conj[xv3869 = xv3880, xv3870 = xv3877, xv3873 = 0, xv3869 <= xv3880, xv3880 <= xv3869, xv3870 <= xv3877, xv3877 <= xv3870]]]
Could not prove unsatisfiability of IA conjunction
xv3880 + -1*xv3869 = 0 && xv3877 + -1*xv3870 = 0 && xv3880 + -1*xv3869 >= 0 && xv3869 + -1*xv3880 >= 0 && xv3877 + -1*xv3870 >= 0 && xv3870 + -1*xv3877 >= 0 && -1*xv3873 >= 0 && -1*xv3873 + -1 >= 0
The linear inequalities
  xv3880 + -1*xv3869 = 0
  xv3877 + -1*xv3870 = 0
  xv3880 + -1*xv3869 >= 0
  xv3869 + -1*xv3880 >= 0
  xv3877 + -1*xv3870 >= 0
  xv3870 + -1*xv3877 >= 0
  -1*xv3873 >= 0
  -1*xv3873 + -1 >= 0
cannot be proved unsatisfiable via hints
  Simplex
could not use simplex algorithm to prove unsatisfiability, Error on node 655:problem in checking validity of formula Disj[False, Disj[! (xv3893 = 0), ! (xv3895 = xv3894), ! (xv3884 = xv3895), ! (xv3885 = xv3892), ! (xv3892 < 1), ! (xv3893 <= 0), ! (0 <= xv3893), ! (xv3895 <= xv3894), ! (xv3894 <= xv3895), ! (xv3892 <= 1), ! (xv3884 <= xv3895), ! (xv3895 <= xv3884), ! (xv3885 <= xv3892), ! (xv3892 <= xv3885)], xv3888 = 1, Conj[True, Conj[xv3893 = 0, xv3895 = xv3894, xv3884 = xv3895, xv3885 = xv3892, xv3888 = 0, xv3892 < 1, xv3893 <= 0, 0 <= xv3893, xv3895 <= xv3894, xv3894 <= xv3895, xv3892 <= 1, xv3884 <= xv3895, xv3895 <= xv3884, xv3885 <= xv3892, xv3892 <= xv3885]]]
Could not prove unsatisfiability of IA conjunction
-1*xv3893 = 0 && xv3894 + -1*xv3895 = 0 && xv3895 + -1*xv3884 = 0 && xv3892 + -1*xv3885 = 0 && -1*xv3892 >= 0 && -1*xv3893 >= 0 && xv3893 >= 0 && xv3894 + -1*xv3895 >= 0 && xv3895 + -1*xv3894 >= 0 && 1 + -1*xv3892 >= 0 && xv3895 + -1*xv3884 >= 0 && xv3884 + -1*xv3895 >= 0 && xv3892 + -1*xv3885 >= 0 && xv3885 + -1*xv3892 >= 0 && -1*xv3888 >= 0 && -1*xv3888 + -1 >= 0
The linear inequalities
  -1*xv3893 = 0
  xv3894 + -1*xv3895 = 0
  xv3895 + -1*xv3884 = 0
  xv3892 + -1*xv3885 = 0
  -1*xv3892 >= 0
  -1*xv3893 >= 0
  xv3893 >= 0
  xv3894 + -1*xv3895 >= 0
  xv3895 + -1*xv3894 >= 0
  1 + -1*xv3892 >= 0
  xv3895 + -1*xv3884 >= 0
  xv3884 + -1*xv3895 >= 0
  xv3892 + -1*xv3885 >= 0
  xv3885 + -1*xv3892 >= 0
  -1*xv3888 >= 0
  -1*xv3888 + -1 >= 0
cannot be proved unsatisfiable via hints
  Simplex
could not use simplex algorithm to prove unsatisfiability]
        6.71 real        12.57 user         3.16 sys