FAILED
Error message:
[Error on node 348:problem in checking validity of formula Disj[False, Disj[! (xv735 = xv734), ! (xv735 = 1), ! (xv734 = 1), ! (xv930 = 0), ! (xv923 = xv928), ! (xv924 = xv731), ! (xv925 = 1), ! (xv927 = xv926), ! (0 < xv923), ! (xv733 <= 1), ! (0 <= xv734), ! (xv735 <= xv734), ! (xv734 <= xv735), ! (xv735 <= 1), ! (1 <= xv735), ! (xv734 <= 1), ! (1 <= xv734), ! (xv929 <= 1), ! (xv930 <= 0), ! (0 <= xv930), ! (xv923 <= xv928), ! (xv928 <= xv923), ! (xv924 <= xv731), ! (xv731 <= xv924), ! (xv925 <= 1), ! (1 <= xv925), ! (0 <= xv926), ! (xv927 <= xv926), ! (xv926 <= xv927)], xv927 = 1, Conj[True, Conj[xv735 = xv734, xv735 = 1, xv734 = 1, xv930 = 0, xv923 = xv928, xv924 = xv731, xv925 = 1, xv927 = xv926, xv927 = 0, 0 < xv923, xv733 <= 1, 0 <= xv734, xv735 <= xv734, xv734 <= xv735, xv735 <= 1, 1 <= xv735, xv734 <= 1, 1 <= xv734, xv929 <= 1, xv930 <= 0, 0 <= xv930, xv923 <= xv928, xv928 <= xv923, xv924 <= xv731, xv731 <= xv924, xv925 <= 1, 1 <= xv925, 0 <= xv926, xv927 <= xv926, xv926 <= xv927]]]
Could not prove unsatisfiability of IA conjunction
xv734 + -1*xv735 = 0 && 1 + -1*xv735 = 0 && 1 + -1*xv734 = 0 && -1*xv930 = 0 && xv928 + -1*xv923 = 0 && xv731 + -1*xv924 = 0 && 1 + -1*xv925 = 0 && xv926 + -1*xv927 = 0 && xv923 + -1 >= 0 && 1 + -1*xv733 >= 0 && xv734 >= 0 && xv734 + -1*xv735 >= 0 && xv735 + -1*xv734 >= 0 && 1 + -1*xv735 >= 0 && xv735 + -1 >= 0 && 1 + -1*xv734 >= 0 && xv734 + -1 >= 0 && 1 + -1*xv929 >= 0 && -1*xv930 >= 0 && xv930 >= 0 && xv928 + -1*xv923 >= 0 && xv923 + -1*xv928 >= 0 && xv731 + -1*xv924 >= 0 && xv924 + -1*xv731 >= 0 && 1 + -1*xv925 >= 0 && xv925 + -1 >= 0 && xv926 >= 0 && xv926 + -1*xv927 >= 0 && xv927 + -1*xv926 >= 0 && xv927 + -2 >= 0 && xv927 + -1 >= 0
The linear inequalities
  xv734 + -1*xv735 = 0
  1 + -1*xv735 = 0
  1 + -1*xv734 = 0
  -1*xv930 = 0
  xv928 + -1*xv923 = 0
  xv731 + -1*xv924 = 0
  1 + -1*xv925 = 0
  xv926 + -1*xv927 = 0
  xv923 + -1 >= 0
  1 + -1*xv733 >= 0
  xv734 >= 0
  xv734 + -1*xv735 >= 0
  xv735 + -1*xv734 >= 0
  1 + -1*xv735 >= 0
  xv735 + -1 >= 0
  1 + -1*xv734 >= 0
  xv734 + -1 >= 0
  1 + -1*xv929 >= 0
  -1*xv930 >= 0
  xv930 >= 0
  xv928 + -1*xv923 >= 0
  xv923 + -1*xv928 >= 0
  xv731 + -1*xv924 >= 0
  xv924 + -1*xv731 >= 0
  1 + -1*xv925 >= 0
  xv925 + -1 >= 0
  xv926 >= 0
  xv926 + -1*xv927 >= 0
  xv927 + -1*xv926 >= 0
  xv927 + -2 >= 0
  xv927 + -1 >= 0
cannot be proved unsatisfiable via hints
  Simplex
could not use simplex algorithm to prove unsatisfiability]
        2.05 real         1.97 user         0.05 sys