FAILED
Error message:
[Error on node 306:problem in checking validity of formula Disj[False, Disj[! (xv347 = 1), ! (xv350 = 1), ! (xv464 = 0), ! (xv466 = xv346), ! (xv467 = 0), ! (xv465 = xv466), ! (xv458 = xv465), ! (xv459 = xv345), ! (xv461 = 1), ! (xv462 = 1), xv345 = 0, xv346 = xv345, ! (0 < xv345), ! (xv346 < xv345), ! (0 <= xv346), ! (0 <= xv345), ! (xv466 <= xv345), ! (xv347 <= 1), ! (1 <= xv347), ! (xv350 <= 1), ! (1 <= xv350), ! (xv464 <= 0), ! (0 <= xv464), ! (xv466 <= xv346), ! (xv346 <= xv466), ! (xv467 <= 0), ! (0 <= xv467), ! (xv465 <= xv466), ! (xv466 <= xv465), ! (0 <= xv459), ! (0 <= xv458), ! (xv458 <= xv465), ! (xv465 <= xv458), ! (xv459 <= xv345), ! (xv345 <= xv459), ! (xv460 <= 1), ! (xv461 <= 1), ! (1 <= xv461), ! (xv462 <= 1), ! (1 <= xv462), ! (xv463 <= xv462)], xv463 = 1, Conj[True, Conj[xv347 = 1, xv350 = 1, xv464 = 0, xv466 = xv346, xv467 = 0, xv465 = xv466, xv458 = xv465, xv459 = xv345, xv461 = 1, xv462 = 1, xv350 = xv462, xv463 = 0, ! (xv345 = 0), ! (xv346 = xv345), 0 < xv345, xv346 < xv345, 0 <= xv346, 0 <= xv345, xv466 <= xv345, xv347 <= 1, 1 <= xv347, xv350 <= 1, 1 <= xv350, xv464 <= 0, 0 <= xv464, xv466 <= xv346, xv346 <= xv466, xv467 <= 0, 0 <= xv467, xv465 <= xv466, xv466 <= xv465, 0 <= xv459, 0 <= xv458, xv458 <= xv465, xv465 <= xv458, xv459 <= xv345, xv345 <= xv459, xv460 <= 1, xv461 <= 1, 1 <= xv461, xv462 <= 1, 1 <= xv462, xv463 <= xv462, xv350 <= xv462, xv462 <= xv350]]]
Could not prove unsatisfiability of IA conjunction
1 + -1*xv347 = 0 && 1 + -1*xv350 = 0 && -1*xv464 = 0 && xv346 + -1*xv466 = 0 && -1*xv467 = 0 && xv466 + -1*xv465 = 0 && xv465 + -1*xv458 = 0 && xv345 + -1*xv459 = 0 && 1 + -1*xv461 = 0 && 1 + -1*xv462 = 0 && xv345 + -1 >= 0 && xv345 + -1*xv346 + -1 >= 0 && xv345 + -1 >= 0 && xv345 + -1*xv346 + -1 >= 0 && xv346 >= 0 && xv345 >= 0 && xv345 + -1*xv466 >= 0 && 1 + -1*xv347 >= 0 && xv347 + -1 >= 0 && 1 + -1*xv350 >= 0 && xv350 + -1 >= 0 && -1*xv464 >= 0 && xv464 >= 0 && xv346 + -1*xv466 >= 0 && xv466 + -1*xv346 >= 0 && -1*xv467 >= 0 && xv467 >= 0 && xv466 + -1*xv465 >= 0 && xv465 + -1*xv466 >= 0 && xv459 >= 0 && xv458 >= 0 && xv465 + -1*xv458 >= 0 && xv458 + -1*xv465 >= 0 && xv345 + -1*xv459 >= 0 && xv459 + -1*xv345 >= 0 && 1 + -1*xv460 >= 0 && 1 + -1*xv461 >= 0 && xv461 + -1 >= 0 && 1 + -1*xv462 >= 0 && xv462 + -1 >= 0 && xv462 + -1*xv463 >= 0 && -1*xv463 >= 0 && -1*xv463 + -1 >= 0
The linear inequalities
  1 + -1*xv347 = 0
  1 + -1*xv350 = 0
  -1*xv464 = 0
  xv346 + -1*xv466 = 0
  -1*xv467 = 0
  xv466 + -1*xv465 = 0
  xv465 + -1*xv458 = 0
  xv345 + -1*xv459 = 0
  1 + -1*xv461 = 0
  1 + -1*xv462 = 0
  xv345 + -1 >= 0
  xv345 + -1*xv346 + -1 >= 0
  xv345 + -1 >= 0
  xv345 + -1*xv346 + -1 >= 0
  xv346 >= 0
  xv345 >= 0
  xv345 + -1*xv466 >= 0
  1 + -1*xv347 >= 0
  xv347 + -1 >= 0
  1 + -1*xv350 >= 0
  xv350 + -1 >= 0
  -1*xv464 >= 0
  xv464 >= 0
  xv346 + -1*xv466 >= 0
  xv466 + -1*xv346 >= 0
  -1*xv467 >= 0
  xv467 >= 0
  xv466 + -1*xv465 >= 0
  xv465 + -1*xv466 >= 0
  xv459 >= 0
  xv458 >= 0
  xv465 + -1*xv458 >= 0
  xv458 + -1*xv465 >= 0
  xv345 + -1*xv459 >= 0
  xv459 + -1*xv345 >= 0
  1 + -1*xv460 >= 0
  1 + -1*xv461 >= 0
  xv461 + -1 >= 0
  1 + -1*xv462 >= 0
  xv462 + -1 >= 0
  xv462 + -1*xv463 >= 0
  -1*xv463 >= 0
  -1*xv463 + -1 >= 0
cannot be proved unsatisfiable via hints
  Simplex
could not use simplex algorithm to prove unsatisfiability]
        9.40 real        17.53 user         3.72 sys