FAILED Error message: [Error on node 321:problem in checking validity of formula Disj[False, Disj[! (xv667 = xv666), ! (xv668 = xv665), ! (xv669 = 1), ! (xv670 = 0), ! (xv671 = xv670), ! (xv671 = 0), ! (xv675 = 1), ! (xv676 = xv672 + 1), ! (xv677 = xv674 + 1), ! (xv678 = xv676), ! (xv679 = xv673), ! (xv680 = 1), ! (xv682 = xv681), ! (0 < xv668), ! (0 < xv673), ! (0 < xv679), ! (xv667 <= 0), ! (xv667 <= xv666), ! (xv666 <= xv667), ! (xv668 <= xv665), ! (xv665 <= xv668), ! (xv669 <= 1), ! (1 <= xv669), ! (xv670 <= 0), ! (0 <= xv670), ! (xv671 <= xv670), ! (xv670 <= xv671), ! (xv671 <= 0), ! (0 <= xv671), ! (xv675 <= 1), ! (1 <= xv675), ! (xv676 <= xv672 + 1), ! (xv672 + 1 <= xv676), ! (xv677 <= xv674 + 1), ! (xv674 + 1 <= xv677), ! (xv678 <= xv676), ! (xv676 <= xv678), ! (xv679 <= xv673), ! (xv673 <= xv679), ! (xv680 <= 1), ! (1 <= xv680), ! (xv682 <= xv681), ! (xv681 <= xv682)], xv682 = 1, Conj[True, Conj[xv667 = xv666, xv668 = xv665, xv669 = 1, xv670 = 0, xv671 = xv670, xv671 = 0, xv675 = 1, xv676 = xv672 + 1, xv677 = xv674 + 1, xv678 = xv676, xv679 = xv673, xv680 = 1, xv682 = xv681, xv682 = 0, 0 < xv668, 0 < xv673, 0 < xv679, xv667 <= 0, xv667 <= xv666, xv666 <= xv667, xv668 <= xv665, xv665 <= xv668, xv669 <= 1, 1 <= xv669, xv670 <= 0, 0 <= xv670, xv671 <= xv670, xv670 <= xv671, xv671 <= 0, 0 <= xv671, xv675 <= 1, 1 <= xv675, xv676 <= xv672 + 1, xv672 + 1 <= xv676, xv677 <= xv674 + 1, xv674 + 1 <= xv677, xv678 <= xv676, xv676 <= xv678, xv679 <= xv673, xv673 <= xv679, xv680 <= 1, 1 <= xv680, xv682 <= xv681, xv681 <= xv682]]] Could not prove unsatisfiability of IA conjunction xv666 + -1*xv667 = 0 && xv665 + -1*xv668 = 0 && 1 + -1*xv669 = 0 && -1*xv670 = 0 && xv670 + -1*xv671 = 0 && -1*xv671 = 0 && 1 + -1*xv675 = 0 && xv672 + 1 + -1*xv676 = 0 && xv674 + 1 + -1*xv677 = 0 && xv676 + -1*xv678 = 0 && xv673 + -1*xv679 = 0 && 1 + -1*xv680 = 0 && xv681 + -1*xv682 = 0 && xv668 + -1 >= 0 && xv673 + -1 >= 0 && xv679 + -1 >= 0 && -1*xv667 >= 0 && xv666 + -1*xv667 >= 0 && xv667 + -1*xv666 >= 0 && xv665 + -1*xv668 >= 0 && xv668 + -1*xv665 >= 0 && 1 + -1*xv669 >= 0 && xv669 + -1 >= 0 && -1*xv670 >= 0 && xv670 >= 0 && xv670 + -1*xv671 >= 0 && xv671 + -1*xv670 >= 0 && -1*xv671 >= 0 && xv671 >= 0 && 1 + -1*xv675 >= 0 && xv675 + -1 >= 0 && xv672 + 1 + -1*xv676 >= 0 && xv676 + -1*xv672 + -1 >= 0 && xv674 + 1 + -1*xv677 >= 0 && xv677 + -1*xv674 + -1 >= 0 && xv676 + -1*xv678 >= 0 && xv678 + -1*xv676 >= 0 && xv673 + -1*xv679 >= 0 && xv679 + -1*xv673 >= 0 && 1 + -1*xv680 >= 0 && xv680 + -1 >= 0 && xv681 + -1*xv682 >= 0 && xv682 + -1*xv681 >= 0 && -1*xv682 >= 0 && -1*xv682 + -1 >= 0 The linear inequalities xv666 + -1*xv667 = 0 xv665 + -1*xv668 = 0 1 + -1*xv669 = 0 -1*xv670 = 0 xv670 + -1*xv671 = 0 -1*xv671 = 0 1 + -1*xv675 = 0 xv672 + 1 + -1*xv676 = 0 xv674 + 1 + -1*xv677 = 0 xv676 + -1*xv678 = 0 xv673 + -1*xv679 = 0 1 + -1*xv680 = 0 xv681 + -1*xv682 = 0 xv668 + -1 >= 0 xv673 + -1 >= 0 xv679 + -1 >= 0 -1*xv667 >= 0 xv666 + -1*xv667 >= 0 xv667 + -1*xv666 >= 0 xv665 + -1*xv668 >= 0 xv668 + -1*xv665 >= 0 1 + -1*xv669 >= 0 xv669 + -1 >= 0 -1*xv670 >= 0 xv670 >= 0 xv670 + -1*xv671 >= 0 xv671 + -1*xv670 >= 0 -1*xv671 >= 0 xv671 >= 0 1 + -1*xv675 >= 0 xv675 + -1 >= 0 xv672 + 1 + -1*xv676 >= 0 xv676 + -1*xv672 + -1 >= 0 xv674 + 1 + -1*xv677 >= 0 xv677 + -1*xv674 + -1 >= 0 xv676 + -1*xv678 >= 0 xv678 + -1*xv676 >= 0 xv673 + -1*xv679 >= 0 xv679 + -1*xv673 >= 0 1 + -1*xv680 >= 0 xv680 + -1 >= 0 xv681 + -1*xv682 >= 0 xv682 + -1*xv681 >= 0 -1*xv682 >= 0 -1*xv682 + -1 >= 0 cannot be proved unsatisfiable via hints Simplex could not use simplex algorithm to prove unsatisfiability, Error on node 449:problem in checking validity of formula Disj[False, Disj[! (xv1370 = xv1369), ! (xv1371 = xv1368), ! (xv1372 = 1), ! (xv1373 = 0), ! (xv1374 = xv1373), ! (xv1374 = 0), ! (xv1378 = 1), ! (xv1379 = xv1375 + 1), ! (xv1380 = xv1377 + 1), ! (0 < xv1371), ! (0 < xv1376), ! (xv1370 <= 0), ! (xv1370 <= xv1369), ! (xv1369 <= xv1370), ! (xv1371 <= xv1368), ! (xv1368 <= xv1371), ! (xv1372 <= 1), ! (1 <= xv1372), ! (xv1373 <= 0), ! (0 <= xv1373), ! (xv1374 <= xv1373), ! (xv1373 <= xv1374), ! (xv1374 <= 0), ! (0 <= xv1374), ! (xv1378 <= 1), ! (1 <= xv1378), ! (xv1379 <= xv1375 + 1), ! (xv1375 + 1 <= xv1379), ! (xv1380 <= xv1377 + 1), ! (xv1377 + 1 <= xv1380)], xv1385 = 1, Conj[True, Conj[xv1370 = xv1369, xv1371 = xv1368, xv1372 = 1, xv1373 = 0, xv1374 = xv1373, xv1374 = 0, xv1378 = 1, xv1379 = xv1375 + 1, xv1380 = xv1377 + 1, xv1385 = 0, 0 < xv1371, 0 < xv1376, xv1370 <= 0, xv1370 <= xv1369, xv1369 <= xv1370, xv1371 <= xv1368, xv1368 <= xv1371, xv1372 <= 1, 1 <= xv1372, xv1373 <= 0, 0 <= xv1373, xv1374 <= xv1373, xv1373 <= xv1374, xv1374 <= 0, 0 <= xv1374, xv1378 <= 1, 1 <= xv1378, xv1379 <= xv1375 + 1, xv1375 + 1 <= xv1379, xv1380 <= xv1377 + 1, xv1377 + 1 <= xv1380]]] Could not prove unsatisfiability of IA conjunction xv1369 + -1*xv1370 = 0 && xv1368 + -1*xv1371 = 0 && 1 + -1*xv1372 = 0 && -1*xv1373 = 0 && xv1373 + -1*xv1374 = 0 && -1*xv1374 = 0 && 1 + -1*xv1378 = 0 && xv1375 + 1 + -1*xv1379 = 0 && xv1377 + 1 + -1*xv1380 = 0 && xv1371 + -1 >= 0 && xv1376 + -1 >= 0 && -1*xv1370 >= 0 && xv1369 + -1*xv1370 >= 0 && xv1370 + -1*xv1369 >= 0 && xv1368 + -1*xv1371 >= 0 && xv1371 + -1*xv1368 >= 0 && 1 + -1*xv1372 >= 0 && xv1372 + -1 >= 0 && -1*xv1373 >= 0 && xv1373 >= 0 && xv1373 + -1*xv1374 >= 0 && xv1374 + -1*xv1373 >= 0 && -1*xv1374 >= 0 && xv1374 >= 0 && 1 + -1*xv1378 >= 0 && xv1378 + -1 >= 0 && xv1375 + 1 + -1*xv1379 >= 0 && xv1379 + -1*xv1375 + -1 >= 0 && xv1377 + 1 + -1*xv1380 >= 0 && xv1380 + -1*xv1377 + -1 >= 0 && -1*xv1385 >= 0 && -1*xv1385 + -1 >= 0 The linear inequalities xv1369 + -1*xv1370 = 0 xv1368 + -1*xv1371 = 0 1 + -1*xv1372 = 0 -1*xv1373 = 0 xv1373 + -1*xv1374 = 0 -1*xv1374 = 0 1 + -1*xv1378 = 0 xv1375 + 1 + -1*xv1379 = 0 xv1377 + 1 + -1*xv1380 = 0 xv1371 + -1 >= 0 xv1376 + -1 >= 0 -1*xv1370 >= 0 xv1369 + -1*xv1370 >= 0 xv1370 + -1*xv1369 >= 0 xv1368 + -1*xv1371 >= 0 xv1371 + -1*xv1368 >= 0 1 + -1*xv1372 >= 0 xv1372 + -1 >= 0 -1*xv1373 >= 0 xv1373 >= 0 xv1373 + -1*xv1374 >= 0 xv1374 + -1*xv1373 >= 0 -1*xv1374 >= 0 xv1374 >= 0 1 + -1*xv1378 >= 0 xv1378 + -1 >= 0 xv1375 + 1 + -1*xv1379 >= 0 xv1379 + -1*xv1375 + -1 >= 0 xv1377 + 1 + -1*xv1380 >= 0 xv1380 + -1*xv1377 + -1 >= 0 -1*xv1385 >= 0 -1*xv1385 + -1 >= 0 cannot be proved unsatisfiable via hints Simplex could not use simplex algorithm to prove unsatisfiability] 9.78 real 9.60 user 0.16 sys