Label | Meaning |
---|---|
S | Solution {OPTIMUM FOUND or OPT | UNSATISFIABLE or UNSAT | UNKNOWN | Not available or N/A} |
O | Best solution found |
T | CPU time (TO for Time Out) |
(out)(err) | Standard output and standard error for each solver |
Color | Meaning |
---|---|
Text | Best solver column |
Text | Optimal solution with the best CPU time |
Text | Optimal solution and finished within the Time Out |
Text | Optimal solution and did not finish within the Time Out |
Text | Time Out |
Text | Buggy solution |
Instance file name | Best solver | Sat4j | ShinMaxSat | WMaxSatz+ | WMaxSatz09 | WPM1 | akmaxsat | akmaxsat_ls | iut_rr_ls | iut_rr_rv | wbo1.6 |
---|---|---|---|---|---|---|---|---|---|---|---|
s2v100c1200_1.wcnf | S = OPT O = 865 T = 4.36 |
S = N/A O = 1253 T = TO (out)(err) |
S = N/A O = 1421 T = TO (out)(err) |
S = OPT O = 865 T = 46.47 (out)(err) |
S = OPT O = 865 T = 44.27 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 865 T = 11.50 (out)(err) |
S = OPT O = 865 T = 4.36 (out)(err) |
S = OPT O = 865 T = 4.79 (out)(err) |
S = OPT O = 865 T = 4.67 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1200_2.wcnf | S = OPT O = 774 T = 3.31 |
S = N/A O = 1100 T = TO (out)(err) |
S = N/A O = 1403 T = TO (out)(err) |
S = OPT O = 774 T = 27.92 (out)(err) |
S = OPT O = 774 T = 30.59 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 774 T = 8.47 (out)(err) |
S = OPT O = 774 T = 3.31 (out)(err) |
S = OPT O = 774 T = 3.69 (out)(err) |
S = OPT O = 774 T = 3.59 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1200_3.wcnf | S = OPT O = 933 T = 33.32 |
S = N/A O = 1160 T = TO (out)(err) |
S = N/A O = 1503 T = TO (out)(err) |
S = OPT O = 933 T = 203.26 (out)(err) |
S = OPT O = 933 T = 204.33 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 933 T = 51.86 (out)(err) |
S = OPT O = 933 T = 33.32 (out)(err) |
S = OPT O = 933 T = 37.19 (out)(err) |
S = OPT O = 933 T = 36.27 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1200_4.wcnf | S = OPT O = 798 T = 3.45 |
S = N/A O = 1214 T = TO (out)(err) |
S = N/A O = 1438 T = TO (out)(err) |
S = OPT O = 798 T = 17.17 (out)(err) |
S = OPT O = 798 T = 16.86 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 798 T = 7.02 (out)(err) |
S = OPT O = 798 T = 3.45 (out)(err) |
S = OPT O = 798 T = 3.90 (out)(err) |
S = OPT O = 798 T = 3.79 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1200_5.wcnf | S = OPT O = 876 T = 4.06 |
S = N/A O = 1176 T = TO (out)(err) |
S = N/A O = 1545 T = TO (out)(err) |
S = OPT O = 876 T = 43.72 (out)(err) |
S = OPT O = 876 T = 44.83 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 876 T = 9.35 (out)(err) |
S = OPT O = 876 T = 4.06 (out)(err) |
S = OPT O = 876 T = 4.48 (out)(err) |
S = OPT O = 876 T = 4.37 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1200_6.wcnf | S = OPT O = 734 T = 0.67 |
S = N/A O = 1011 T = TO (out)(err) |
S = N/A O = 1328 T = TO (out)(err) |
S = OPT O = 734 T = 2.92 (out)(err) |
S = OPT O = 734 T = 3.13 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 734 T = 1.13 (out)(err) |
S = OPT O = 734 T = 0.68 (out)(err) |
S = OPT O = 734 T = 0.69 (out)(err) |
S = OPT O = 734 T = 0.67 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1200_7.wcnf | S = OPT O = 800 T = 12.00 |
S = N/A O = 1175 T = TO (out)(err) |
S = N/A O = 1267 T = TO (out)(err) |
S = OPT O = 800 T = 75.10 (out)(err) |
S = OPT O = 800 T = 72.15 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 800 T = 23.48 (out)(err) |
S = OPT O = 800 T = 12.00 (out)(err) |
S = OPT O = 800 T = 13.46 (out)(err) |
S = OPT O = 800 T = 12.97 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1200_8.wcnf | S = OPT O = 962 T = 37.30 |
S = N/A O = 1300 T = TO (out)(err) |
S = N/A O = 1436 T = TO (out)(err) |
S = OPT O = 962 T = 350.85 (out)(err) |
S = OPT O = 962 T = 349.72 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 962 T = 53.12 (out)(err) |
S = OPT O = 962 T = 37.30 (out)(err) |
S = OPT O = 962 T = 41.10 (out)(err) |
S = OPT O = 962 T = 40.02 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1300_1.wcnf | S = OPT O = 971 T = 9.58 |
S = N/A O = 1314 T = TO (out)(err) |
S = N/A O = 1691 T = TO (out)(err) |
S = OPT O = 971 T = 72.36 (out)(err) |
S = OPT O = 971 T = 68.18 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 971 T = 11.02 (out)(err) |
S = OPT O = 971 T = 9.58 (out)(err) |
S = OPT O = 971 T = 10.53 (out)(err) |
S = OPT O = 971 T = 10.21 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_2.wcnf | S = OPT O = 930 T = 14.29 |
S = N/A O = 1313 T = TO (out)(err) |
S = N/A O = 1451 T = TO (out)(err) |
S = OPT O = 930 T = 234.91 (out)(err) |
S = OPT O = 930 T = 237.03 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 930 T = 20.90 (out)(err) |
S = OPT O = 930 T = 14.29 (out)(err) |
S = OPT O = 930 T = 15.96 (out)(err) |
S = OPT O = 930 T = 15.26 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_3.wcnf | S = OPT O = 925 T = 4.52 |
S = N/A O = 1178 T = TO (out)(err) |
S = N/A O = 1511 T = TO (out)(err) |
S = OPT O = 925 T = 41.36 (out)(err) |
S = OPT O = 925 T = 42.67 (out)(err) |
S = N/A O = N/A T = 326.68 (out)(err) |
S = OPT O = 925 T = 12.34 (out)(err) |
S = OPT O = 925 T = 4.52 (out)(err) |
S = OPT O = 925 T = 5.05 (out)(err) |
S = OPT O = 925 T = 4.85 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1300_4.wcnf | S = OPT O = 970 T = 8.56 |
S = N/A O = 1402 T = TO (out)(err) |
S = N/A O = 1571 T = TO (out)(err) |
S = OPT O = 970 T = 116.91 (out)(err) |
S = OPT O = 970 T = 116.91 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 970 T = 18.41 (out)(err) |
S = OPT O = 970 T = 8.56 (out)(err) |
S = OPT O = 970 T = 9.51 (out)(err) |
S = OPT O = 970 T = 9.24 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1300_5.wcnf | S = OPT O = 962 T = 16.74 |
S = N/A O = 1258 T = TO (out)(err) |
S = N/A O = 1444 T = TO (out)(err) |
S = OPT O = 962 T = 217.79 (out)(err) |
S = OPT O = 962 T = 226.19 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 962 T = 39.34 (out)(err) |
S = OPT O = 962 T = 16.74 (out)(err) |
S = OPT O = 962 T = 18.37 (out)(err) |
S = OPT O = 962 T = 18.26 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_6.wcnf | S = OPT O = 933 T = 5.72 |
S = N/A O = 1328 T = TO (out)(err) |
S = N/A O = 1468 T = TO (out)(err) |
S = OPT O = 933 T = 48.28 (out)(err) |
S = OPT O = 933 T = 50.81 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 933 T = 6.49 (out)(err) |
S = OPT O = 933 T = 5.72 (out)(err) |
S = OPT O = 933 T = 6.31 (out)(err) |
S = OPT O = 933 T = 6.16 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_7.wcnf | S = OPT O = 877 T = 4.20 |
S = N/A O = 1184 T = TO (out)(err) |
S = N/A O = 1410 T = TO (out)(err) |
S = OPT O = 877 T = 49.18 (out)(err) |
S = OPT O = 877 T = 48.22 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 877 T = 14.15 (out)(err) |
S = OPT O = 877 T = 4.20 (out)(err) |
S = OPT O = 877 T = 4.70 (out)(err) |
S = OPT O = 877 T = 4.55 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1300_8.wcnf | S = OPT O = 941 T = 10.34 |
S = N/A O = 1270 T = TO (out)(err) |
S = N/A O = 1395 T = TO (out)(err) |
S = OPT O = 941 T = 157.36 (out)(err) |
S = OPT O = 941 T = 160.63 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 941 T = 31.00 (out)(err) |
S = OPT O = 941 T = 10.34 (out)(err) |
S = OPT O = 941 T = 11.45 (out)(err) |
S = OPT O = 941 T = 11.17 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1400_1.wcnf | S = OPT O = 1019 T = 23.65 |
S = N/A O = 1364 T = TO (out)(err) |
S = N/A O = 1477 T = TO (out)(err) |
S = OPT O = 1019 T = 167.25 (out)(err) |
S = OPT O = 1019 T = 168.12 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1019 T = 44.12 (out)(err) |
S = OPT O = 1019 T = 23.65 (out)(err) |
S = OPT O = 1019 T = 26.01 (out)(err) |
S = OPT O = 1019 T = 25.34 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1400_2.wcnf | S = OPT O = 1002 T = 11.50 |
S = N/A O = 1289 T = TO (out)(err) |
S = N/A O = 1546 T = TO (out)(err) |
S = OPT O = 1002 T = 135.93 (out)(err) |
S = OPT O = 1002 T = 131.86 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1002 T = 17.14 (out)(err) |
S = OPT O = 1002 T = 11.50 (out)(err) |
S = OPT O = 1002 T = 12.60 (out)(err) |
S = OPT O = 1002 T = 12.25 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1400_3.wcnf | S = OPT O = 1020 T = 20.57 |
S = N/A O = 1288 T = TO (out)(err) |
S = N/A O = 1790 T = TO (out)(err) |
S = OPT O = 1020 T = 281.14 (out)(err) |
S = OPT O = 1020 T = 272.95 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1020 T = 23.78 (out)(err) |
S = OPT O = 1020 T = 20.57 (out)(err) |
S = OPT O = 1020 T = 22.71 (out)(err) |
S = OPT O = 1020 T = 22.33 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1400_4.wcnf | S = OPT O = 1094 T = 44.31 |
S = N/A O = 1409 T = TO (out)(err) |
S = N/A O = 1601 T = TO (out)(err) |
S = OPT O = 1094 T = 329.14 (out)(err) |
S = OPT O = 1094 T = 358.23 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1094 T = 54.04 (out)(err) |
S = OPT O = 1094 T = 44.31 (out)(err) |
S = OPT O = 1094 T = 47.78 (out)(err) |
S = OPT O = 1094 T = 47.17 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1400_5.wcnf | S = OPT O = 1018 T = 11.27 |
S = N/A O = 1340 T = TO (out)(err) |
S = N/A O = 1597 T = TO (out)(err) |
S = OPT O = 1018 T = 167.93 (out)(err) |
S = OPT O = 1018 T = 164.89 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1018 T = 21.96 (out)(err) |
S = OPT O = 1018 T = 11.27 (out)(err) |
S = OPT O = 1018 T = 11.83 (out)(err) |
S = OPT O = 1018 T = 11.51 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1400_6.wcnf | S = OPT O = 997 T = 2.81 |
S = N/A O = 1390 T = TO (out)(err) |
S = N/A O = 1681 T = TO (out)(err) |
S = OPT O = 997 T = 33.66 (out)(err) |
S = OPT O = 997 T = 33.66 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 997 T = 5.38 (out)(err) |
S = OPT O = 997 T = 2.81 (out)(err) |
S = OPT O = 997 T = 3.01 (out)(err) |
S = OPT O = 997 T = 2.96 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1400_7.wcnf | S = OPT O = 1001 T = 38.93 |
S = N/A O = 1372 T = TO (out)(err) |
S = N/A O = 1583 T = TO (out)(err) |
S = OPT O = 1001 T = 246.35 (out)(err) |
S = OPT O = 1001 T = 249.56 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1001 T = 45.80 (out)(err) |
S = OPT O = 1001 T = 38.93 (out)(err) |
S = OPT O = 1001 T = 42.60 (out)(err) |
S = OPT O = 1001 T = 41.20 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1400_8.wcnf | S = OPT O = 1084 T = 24.73 |
S = N/A O = 1334 T = TO (out)(err) |
S = N/A O = 1682 T = TO (out)(err) |
S = OPT O = 1084 T = 166.95 (out)(err) |
S = OPT O = 1084 T = 302.21 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1084 T = 38.17 (out)(err) |
S = OPT O = 1084 T = 24.73 (out)(err) |
S = OPT O = 1084 T = 26.97 (out)(err) |
S = OPT O = 1084 T = 26.32 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1500_1.wcnf | S = OPT O = 1077 T = 14.52 |
S = N/A O = 1409 T = TO (out)(err) |
S = N/A O = 1568 T = TO (out)(err) |
S = OPT O = 1077 T = 124.55 (out)(err) |
S = OPT O = 1077 T = 123.90 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1077 T = 29.86 (out)(err) |
S = OPT O = 1077 T = 14.52 (out)(err) |
S = OPT O = 1077 T = 15.94 (out)(err) |
S = OPT O = 1077 T = 15.52 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1500_2.wcnf | S = OPT O = 1125 T = 18.40 |
S = N/A O = 1456 T = TO (out)(err) |
S = N/A O = 1781 T = TO (out)(err) |
S = OPT O = 1125 T = 303.91 (out)(err) |
S = OPT O = 1125 T = 304.24 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1125 T = 22.45 (out)(err) |
S = OPT O = 1125 T = 18.40 (out)(err) |
S = OPT O = 1125 T = 19.97 (out)(err) |
S = OPT O = 1125 T = 19.41 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1500_3.wcnf | S = OPT O = 1151 T = 39.48 |
S = N/A O = 1378 T = TO (out)(err) |
S = N/A O = 1847 T = TO (out)(err) |
S = OPT O = 1151 T = 292.50 (out)(err) |
S = OPT O = 1151 T = 291.38 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1151 T = 43.16 (out)(err) |
S = OPT O = 1151 T = 39.48 (out)(err) |
S = OPT O = 1151 T = 43.48 (out)(err) |
S = OPT O = 1151 T = 42.02 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1500_4.wcnf | S = OPT O = 1072 T = 14.50 |
S = N/A O = 1462 T = TO (out)(err) |
S = N/A O = 1807 T = TO (out)(err) |
S = OPT O = 1072 T = 302.51 (out)(err) |
S = OPT O = 1072 T = 304.62 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1072 T = 73.25 (out)(err) |
S = OPT O = 1072 T = 14.50 (out)(err) |
S = OPT O = 1072 T = 15.97 (out)(err) |
S = OPT O = 1072 T = 15.61 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1500_5.wcnf | S = OPT O = 1151 T = 32.12 |
S = N/A O = 1434 T = TO (out)(err) |
S = N/A O = 1848 T = TO (out)(err) |
S = OPT O = 1151 T = 348.99 (out)(err) |
S = OPT O = 1151 T = 393.05 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1151 T = 39.72 (out)(err) |
S = OPT O = 1151 T = 32.12 (out)(err) |
S = OPT O = 1151 T = 34.20 (out)(err) |
S = OPT O = 1151 T = 33.67 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1500_6.wcnf | S = OPT O = 1225 T = 39.32 |
S = N/A O = 1624 T = TO (out)(err) |
S = N/A O = 2010 T = TO (out)(err) |
S = OPT O = 1225 T = 663.22 (out)(err) |
S = OPT O = 1225 T = 698.29 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1225 T = 79.13 (out)(err) |
S = OPT O = 1225 T = 39.32 (out)(err) |
S = OPT O = 1225 T = 42.57 (out)(err) |
S = OPT O = 1225 T = 41.46 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1500_7.wcnf | S = OPT O = 1186 T = 24.84 |
S = N/A O = 1577 T = TO (out)(err) |
S = N/A O = 2017 T = TO (out)(err) |
S = OPT O = 1186 T = 246.90 (out)(err) |
S = OPT O = 1186 T = 247.75 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1186 T = 26.93 (out)(err) |
S = OPT O = 1186 T = 24.84 (out)(err) |
S = OPT O = 1186 T = 26.99 (out)(err) |
S = OPT O = 1186 T = 26.23 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1500_8.wcnf | S = OPT O = 1217 T = 34.24 |
S = N/A O = 1512 T = TO (out)(err) |
S = N/A O = 1800 T = TO (out)(err) |
S = OPT O = 1217 T = 1062.06 (out)(err) |
S = OPT O = 1217 T = 1084.53 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1217 T = 78.45 (out)(err) |
S = OPT O = 1217 T = 34.24 (out)(err) |
S = OPT O = 1217 T = 37.03 (out)(err) |
S = OPT O = 1217 T = 36.47 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1600_1.wcnf | S = OPT O = 1230 T = 14.38 |
S = N/A O = 1639 T = TO (out)(err) |
S = N/A O = 2063 T = TO (out)(err) |
S = OPT O = 1230 T = 253.37 (out)(err) |
S = OPT O = 1230 T = 248.23 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1230 T = 26.50 (out)(err) |
S = OPT O = 1230 T = 14.38 (out)(err) |
S = OPT O = 1230 T = 15.43 (out)(err) |
S = OPT O = 1230 T = 15.22 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1600_2.wcnf | S = OPT O = 1265 T = 140.39 |
S = N/A O = 1534 T = TO (out)(err) |
S = N/A O = 1840 T = TO (out)(err) |
S = N/A O = 1265 T = TO (out)(err) |
S = N/A O = 1265 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1265 T = 215.72 (out)(err) |
S = OPT O = 1265 T = 140.39 (out)(err) |
S = OPT O = 1265 T = 149.74 (out)(err) |
S = OPT O = 1265 T = 144.96 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1600_3.wcnf | S = OPT O = 1309 T = 80.81 |
S = N/A O = 1657 T = TO (out)(err) |
S = N/A O = 1862 T = TO (out)(err) |
S = OPT O = 1309 T = 1037.61 (out)(err) |
S = OPT O = 1309 T = 1051.02 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1309 T = 156.60 (out)(err) |
S = OPT O = 1309 T = 80.81 (out)(err) |
S = OPT O = 1309 T = 87.03 (out)(err) |
S = OPT O = 1309 T = 84.42 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1600_4.wcnf | S = OPT O = 1267 T = 41.43 |
S = N/A O = 1693 T = TO (out)(err) |
S = N/A O = 1821 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1267 T = 183.60 (out)(err) |
S = OPT O = 1267 T = 41.43 (out)(err) |
S = OPT O = 1267 T = 44.59 (out)(err) |
S = OPT O = 1267 T = 43.50 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1600_5.wcnf | S = OPT O = 1298 T = 35.15 |
S = N/A O = 1711 T = TO (out)(err) |
S = N/A O = 1795 T = TO (out)(err) |
S = OPT O = 1298 T = 443.68 (out)(err) |
S = OPT O = 1298 T = 445.48 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1298 T = 51.67 (out)(err) |
S = OPT O = 1298 T = 35.15 (out)(err) |
S = OPT O = 1298 T = 38.33 (out)(err) |
S = OPT O = 1298 T = 37.23 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1600_6.wcnf | S = OPT O = 1190 T = 11.35 |
S = N/A O = 1754 T = TO (out)(err) |
S = N/A O = 1805 T = TO (out)(err) |
S = OPT O = 1190 T = 298.11 (out)(err) |
S = OPT O = 1190 T = 299.29 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1190 T = 21.11 (out)(err) |
S = OPT O = 1190 T = 11.35 (out)(err) |
S = OPT O = 1190 T = 12.37 (out)(err) |
S = OPT O = 1190 T = 12.05 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1600_7.wcnf | S = OPT O = 1243 T = 64.53 |
S = N/A O = 1584 T = TO (out)(err) |
S = N/A O = 1740 T = 432.99 (out)(err) |
S = OPT O = 1243 T = 1504.72 (out)(err) |
S = OPT O = 1243 T = 1650.48 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1243 T = 132.94 (out)(err) |
S = OPT O = 1243 T = 64.53 (out)(err) |
S = OPT O = 1243 T = 70.56 (out)(err) |
S = OPT O = 1243 T = 68.45 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1600_8.wcnf | S = OPT O = 1184 T = 4.25 |
S = N/A O = 1648 T = TO (out)(err) |
S = N/A O = 1923 T = 443.71 (out)(err) |
S = OPT O = 1184 T = 83.56 (out)(err) |
S = OPT O = 1184 T = 84.45 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1184 T = 11.54 (out)(err) |
S = OPT O = 1184 T = 4.25 (out)(err) |
S = OPT O = 1184 T = 4.55 (out)(err) |
S = OPT O = 1184 T = 4.46 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1200_1.wcnf | S = OPT O = 840 T = 26.62 |
S = N/A O = 1067 T = TO (out)(err) |
S = N/A O = 1542 T = TO (out)(err) |
S = OPT O = 840 T = 205.19 (out)(err) |
S = OPT O = 840 T = 202.29 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 840 T = 54.60 (out)(err) |
S = OPT O = 840 T = 26.62 (out)(err) |
S = OPT O = 840 T = 29.46 (out)(err) |
S = OPT O = 840 T = 29.04 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_2.wcnf | S = OPT O = 803 T = 5.84 |
S = N/A O = 1083 T = TO (out)(err) |
S = N/A O = 1570 T = TO (out)(err) |
S = OPT O = 803 T = 19.56 (out)(err) |
S = OPT O = 803 T = 19.50 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 803 T = 7.58 (out)(err) |
S = OPT O = 803 T = 5.84 (out)(err) |
S = OPT O = 803 T = 6.50 (out)(err) |
S = OPT O = 803 T = 6.32 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1200_3.wcnf | S = OPT O = 834 T = 13.53 |
S = N/A O = 1186 T = TO (out)(err) |
S = N/A O = 1569 T = TO (out)(err) |
S = OPT O = 834 T = 79.74 (out)(err) |
S = OPT O = 834 T = 81.08 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 834 T = 26.93 (out)(err) |
S = OPT O = 834 T = 13.53 (out)(err) |
S = OPT O = 834 T = 15.90 (out)(err) |
S = OPT O = 834 T = 15.50 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1200_4.wcnf | S = OPT O = 811 T = 10.68 |
S = N/A O = 1207 T = TO (out)(err) |
S = N/A O = 1537 T = TO (out)(err) |
S = OPT O = 811 T = 40.90 (out)(err) |
S = OPT O = 811 T = 36.03 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 811 T = 18.99 (out)(err) |
S = OPT O = 811 T = 10.68 (out)(err) |
S = OPT O = 811 T = 12.11 (out)(err) |
S = OPT O = 811 T = 11.66 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_5.wcnf | S = OPT O = 850 T = 39.39 |
S = N/A O = 1074 T = TO (out)(err) |
S = N/A O = 1603 T = TO (out)(err) |
S = OPT O = 850 T = 441.79 (out)(err) |
S = OPT O = 850 T = 458.75 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 850 T = 51.73 (out)(err) |
S = OPT O = 850 T = 39.39 (out)(err) |
S = OPT O = 850 T = 43.83 (out)(err) |
S = OPT O = 850 T = 43.19 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_6.wcnf | S = OPT O = 784 T = 16.41 |
S = N/A O = 1047 T = TO (out)(err) |
S = N/A O = 1430 T = TO (out)(err) |
S = OPT O = 784 T = 249.50 (out)(err) |
S = OPT O = 784 T = 250.69 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 784 T = 63.92 (out)(err) |
S = OPT O = 784 T = 16.41 (out)(err) |
S = OPT O = 784 T = 18.25 (out)(err) |
S = OPT O = 784 T = 17.80 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1200_7.wcnf | S = OPT O = 747 T = 2.93 |
S = N/A O = 1055 T = TO (out)(err) |
S = N/A O = 1438 T = TO (out)(err) |
S = OPT O = 747 T = 12.53 (out)(err) |
S = OPT O = 747 T = 12.53 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 747 T = 4.93 (out)(err) |
S = OPT O = 747 T = 2.93 (out)(err) |
S = OPT O = 747 T = 3.30 (out)(err) |
S = OPT O = 747 T = 3.20 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1200_8.wcnf | S = OPT O = 813 T = 11.23 |
S = N/A O = 1230 T = TO (out)(err) |
S = N/A O = 1546 T = TO (out)(err) |
S = OPT O = 813 T = 44.43 (out)(err) |
S = OPT O = 813 T = 43.75 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 813 T = 12.32 (out)(err) |
S = OPT O = 813 T = 11.23 (out)(err) |
S = OPT O = 813 T = 12.58 (out)(err) |
S = OPT O = 813 T = 12.15 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1300_1.wcnf | S = OPT O = 890 T = 8.79 |
S = N/A O = 1096 T = TO (out)(err) |
S = N/A O = 1884 T = TO (out)(err) |
S = OPT O = 890 T = 46.32 (out)(err) |
S = OPT O = 890 T = 44.98 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 890 T = 11.45 (out)(err) |
S = OPT O = 890 T = 8.79 (out)(err) |
S = OPT O = 890 T = 10.03 (out)(err) |
S = OPT O = 890 T = 9.43 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_2.wcnf | S = OPT O = 847 T = 3.75 |
S = N/A O = 1108 T = TO (out)(err) |
S = N/A O = 1631 T = TO (out)(err) |
S = OPT O = 847 T = 40.43 (out)(err) |
S = OPT O = 847 T = 33.59 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 847 T = 9.57 (out)(err) |
S = OPT O = 847 T = 3.75 (out)(err) |
S = OPT O = 847 T = 4.30 (out)(err) |
S = OPT O = 847 T = 4.05 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_3.wcnf | S = OPT O = 941 T = 10.45 |
S = N/A O = 1338 T = TO (out)(err) |
S = N/A O = 1597 T = TO (out)(err) |
S = OPT O = 941 T = 104.44 (out)(err) |
S = OPT O = 941 T = 104.32 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 941 T = 28.84 (out)(err) |
S = OPT O = 941 T = 10.45 (out)(err) |
S = OPT O = 941 T = 11.64 (out)(err) |
S = OPT O = 941 T = 11.49 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_4.wcnf | S = OPT O = 939 T = 17.92 |
S = N/A O = 1264 T = TO (out)(err) |
S = N/A O = 1698 T = TO (out)(err) |
S = OPT O = 939 T = 169.87 (out)(err) |
S = OPT O = 939 T = 151.64 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 939 T = 29.50 (out)(err) |
S = OPT O = 939 T = 17.92 (out)(err) |
S = OPT O = 939 T = 20.18 (out)(err) |
S = OPT O = 939 T = 19.68 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1300_5.wcnf | S = OPT O = 949 T = 45.22 |
S = N/A O = 1475 T = TO (out)(err) |
S = N/A O = 1715 T = TO (out)(err) |
S = OPT O = 949 T = 439.24 (out)(err) |
S = OPT O = 949 T = 419.29 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 949 T = 111.85 (out)(err) |
S = OPT O = 949 T = 45.22 (out)(err) |
S = OPT O = 949 T = 50.48 (out)(err) |
S = OPT O = 949 T = 49.93 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_6.wcnf | S = OPT O = 865 T = 5.39 |
S = N/A O = 1192 T = TO (out)(err) |
S = N/A O = 1720 T = TO (out)(err) |
S = OPT O = 865 T = 64.07 (out)(err) |
S = OPT O = 865 T = 59.18 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 865 T = 18.02 (out)(err) |
S = OPT O = 865 T = 5.39 (out)(err) |
S = OPT O = 865 T = 6.06 (out)(err) |
S = OPT O = 865 T = 5.90 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_7.wcnf | S = OPT O = 879 T = 4.76 |
S = N/A O = 1167 T = TO (out)(err) |
S = N/A O = 1767 T = TO (out)(err) |
S = OPT O = 879 T = 34.70 (out)(err) |
S = OPT O = 879 T = 36.17 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 879 T = 10.64 (out)(err) |
S = OPT O = 879 T = 4.76 (out)(err) |
S = OPT O = 879 T = 5.33 (out)(err) |
S = OPT O = 879 T = 5.14 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_8.wcnf | S = OPT O = 868 T = 10.65 |
S = N/A O = 1188 T = TO (out)(err) |
S = N/A O = 1710 T = TO (out)(err) |
S = OPT O = 868 T = 49.34 (out)(err) |
S = OPT O = 868 T = 50.64 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 868 T = 12.95 (out)(err) |
S = OPT O = 868 T = 10.65 (out)(err) |
S = OPT O = 868 T = 12.07 (out)(err) |
S = OPT O = 868 T = 11.93 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_1.wcnf | S = OPT O = 1028 T = 24.73 |
S = N/A O = 1283 T = TO (out)(err) |
S = N/A O = 1829 T = TO (out)(err) |
S = OPT O = 1028 T = 107.27 (out)(err) |
S = OPT O = 1028 T = 109.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1028 T = 33.72 (out)(err) |
S = OPT O = 1028 T = 24.73 (out)(err) |
S = OPT O = 1028 T = 28.25 (out)(err) |
S = OPT O = 1028 T = 27.56 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_2.wcnf | S = OPT O = 1008 T = 32.41 |
S = N/A O = 1395 T = TO (out)(err) |
S = N/A O = 2035 T = TO (out)(err) |
S = OPT O = 1008 T = 585.94 (out)(err) |
S = OPT O = 1008 T = 554.95 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1008 T = 125.33 (out)(err) |
S = OPT O = 1008 T = 32.41 (out)(err) |
S = OPT O = 1008 T = 35.65 (out)(err) |
S = OPT O = 1008 T = 34.95 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1400_3.wcnf | S = OPT O = 983 T = 7.07 |
S = N/A O = 1339 T = TO (out)(err) |
S = N/A O = 1959 T = TO (out)(err) |
S = OPT O = 983 T = 41.42 (out)(err) |
S = OPT O = 983 T = 40.01 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 983 T = 17.50 (out)(err) |
S = OPT O = 983 T = 7.07 (out)(err) |
S = OPT O = 983 T = 7.93 (out)(err) |
S = OPT O = 983 T = 7.67 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_4.wcnf | S = OPT O = 1007 T = 47.04 |
S = N/A O = 1234 T = TO (out)(err) |
S = N/A O = 1837 T = TO (out)(err) |
S = OPT O = 1007 T = 285.51 (out)(err) |
S = OPT O = 1007 T = 291.27 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1007 T = 60.19 (out)(err) |
S = OPT O = 1007 T = 47.04 (out)(err) |
S = OPT O = 1007 T = 52.20 (out)(err) |
S = OPT O = 1007 T = 51.37 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1400_5.wcnf | S = OPT O = 1108 T = 284.10 |
S = N/A O = 1494 T = TO (out)(err) |
S = N/A O = 1825 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1108 T = 295.08 (out)(err) |
S = OPT O = 1108 T = 284.10 (out)(err) |
S = OPT O = 1108 T = 315.87 (out)(err) |
S = OPT O = 1108 T = 303.76 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_6.wcnf | S = OPT O = 959 T = 10.19 |
S = N/A O = 1359 T = TO (out)(err) |
S = N/A O = 1519 T = TO (out)(err) |
S = OPT O = 959 T = 49.22 (out)(err) |
S = OPT O = 959 T = 50.06 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 959 T = 12.39 (out)(err) |
S = OPT O = 959 T = 10.19 (out)(err) |
S = OPT O = 959 T = 11.75 (out)(err) |
S = OPT O = 959 T = 11.36 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_7.wcnf | S = OPT O = 1040 T = 53.84 |
S = N/A O = 1404 T = TO (out)(err) |
S = N/A O = 1830 T = TO (out)(err) |
S = OPT O = 1040 T = 565.79 (out)(err) |
S = OPT O = 1040 T = 589.55 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1040 T = 102.83 (out)(err) |
S = OPT O = 1040 T = 53.84 (out)(err) |
S = OPT O = 1040 T = 59.94 (out)(err) |
S = OPT O = 1040 T = 58.31 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1400_8.wcnf | S = OPT O = 1025 T = 39.77 |
S = N/A O = 1418 T = TO (out)(err) |
S = N/A O = 2000 T = TO (out)(err) |
S = OPT O = 1025 T = 293.47 (out)(err) |
S = OPT O = 1025 T = 286.64 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1025 T = 49.82 (out)(err) |
S = OPT O = 1025 T = 39.77 (out)(err) |
S = OPT O = 1025 T = 44.76 (out)(err) |
S = OPT O = 1025 T = 43.98 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_1.wcnf | S = OPT O = 1119 T = 41.70 |
S = N/A O = 1512 T = TO (out)(err) |
S = N/A O = 2057 T = TO (out)(err) |
S = OPT O = 1119 T = 303.95 (out)(err) |
S = OPT O = 1119 T = 302.61 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1119 T = 170.98 (out)(err) |
S = OPT O = 1119 T = 41.70 (out)(err) |
S = OPT O = 1119 T = 46.07 (out)(err) |
S = OPT O = 1119 T = 45.12 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1500_2.wcnf | S = OPT O = 1136 T = 57.70 |
S = N/A O = 1527 T = TO (out)(err) |
S = N/A O = 1877 T = TO (out)(err) |
S = OPT O = 1136 T = 423.69 (out)(err) |
S = OPT O = 1136 T = 445.80 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1136 T = 185.63 (out)(err) |
S = OPT O = 1136 T = 57.70 (out)(err) |
S = OPT O = 1136 T = 64.87 (out)(err) |
S = OPT O = 1136 T = 62.74 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_3.wcnf | S = OPT O = 1062 T = 11.47 |
S = N/A O = 1329 T = TO (out)(err) |
S = N/A O = 1815 T = 490.72 (out)(err) |
S = OPT O = 1062 T = 58.84 (out)(err) |
S = OPT O = 1062 T = 59.50 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1062 T = 20.97 (out)(err) |
S = OPT O = 1062 T = 11.47 (out)(err) |
S = OPT O = 1062 T = 12.77 (out)(err) |
S = OPT O = 1062 T = 12.47 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_4.wcnf | S = OPT O = 1041 T = 6.07 |
S = N/A O = 1437 T = TO (out)(err) |
S = N/A O = 1946 T = TO (out)(err) |
S = OPT O = 1041 T = 41.45 (out)(err) |
S = OPT O = 1041 T = 48.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1041 T = 9.79 (out)(err) |
S = OPT O = 1041 T = 6.07 (out)(err) |
S = OPT O = 1041 T = 6.77 (out)(err) |
S = OPT O = 1041 T = 6.54 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1500_5.wcnf | S = OPT O = 1125 T = 8.41 |
S = N/A O = 1563 T = TO (out)(err) |
S = N/A O = 1869 T = TO (out)(err) |
S = OPT O = 1125 T = 117.45 (out)(err) |
S = OPT O = 1125 T = 119.19 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1125 T = 28.94 (out)(err) |
S = OPT O = 1125 T = 8.41 (out)(err) |
S = OPT O = 1125 T = 9.23 (out)(err) |
S = OPT O = 1125 T = 8.99 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1500_6.wcnf | S = OPT O = 1113 T = 39.00 |
S = N/A O = 1500 T = TO (out)(err) |
S = N/A O = 1842 T = TO (out)(err) |
S = OPT O = 1113 T = 243.88 (out)(err) |
S = OPT O = 1113 T = 369.64 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1113 T = 73.76 (out)(err) |
S = OPT O = 1113 T = 39.00 (out)(err) |
S = OPT O = 1113 T = 43.53 (out)(err) |
S = OPT O = 1113 T = 41.99 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_7.wcnf | S = OPT O = 1163 T = 109.31 |
S = N/A O = 1501 T = TO (out)(err) |
S = N/A O = 2039 T = TO (out)(err) |
S = OPT O = 1163 T = 814.84 (out)(err) |
S = OPT O = 1163 T = 864.27 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1163 T = 146.67 (out)(err) |
S = OPT O = 1163 T = 109.31 (out)(err) |
S = OPT O = 1163 T = 122.15 (out)(err) |
S = OPT O = 1163 T = 119.36 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1500_8.wcnf | S = OPT O = 1097 T = 7.08 |
S = N/A O = 1649 T = TO (out)(err) |
S = N/A O = 1978 T = TO (out)(err) |
S = OPT O = 1097 T = 115.86 (out)(err) |
S = OPT O = 1097 T = 109.84 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1097 T = 18.31 (out)(err) |
S = OPT O = 1097 T = 7.08 (out)(err) |
S = OPT O = 1097 T = 7.86 (out)(err) |
S = OPT O = 1097 T = 7.60 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1600_1.wcnf | S = OPT O = 1190 T = 13.32 |
S = N/A O = 1579 T = TO (out)(err) |
S = N/A O = 1971 T = 457.07 (out)(err) |
S = OPT O = 1190 T = 156.47 (out)(err) |
S = OPT O = 1190 T = 162.73 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1190 T = 15.59 (out)(err) |
S = OPT O = 1190 T = 13.32 (out)(err) |
S = OPT O = 1190 T = 14.96 (out)(err) |
S = OPT O = 1190 T = 14.26 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1600_2.wcnf | S = OPT O = 1227 T = 88.91 |
S = N/A O = 1684 T = TO (out)(err) |
S = N/A O = 1890 T = TO (out)(err) |
S = OPT O = 1227 T = 860.57 (out)(err) |
S = OPT O = 1227 T = 892.50 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1227 T = 144.38 (out)(err) |
S = OPT O = 1227 T = 88.91 (out)(err) |
S = OPT O = 1227 T = 98.93 (out)(err) |
S = OPT O = 1227 T = 96.07 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1600_3.wcnf | S = OPT O = 1224 T = 71.42 |
S = N/A O = 1672 T = TO (out)(err) |
S = N/A O = 2301 T = 474.25 (out)(err) |
S = OPT O = 1224 T = 938.35 (out)(err) |
S = OPT O = 1224 T = 950.62 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1224 T = 111.67 (out)(err) |
S = OPT O = 1224 T = 71.42 (out)(err) |
S = OPT O = 1224 T = 76.35 (out)(err) |
S = OPT O = 1224 T = 74.58 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1600_4.wcnf | S = OPT O = 1264 T = 178.24 |
S = N/A O = 1810 T = TO (out)(err) |
S = N/A O = 2195 T = TO (out)(err) |
S = OPT O = 1264 T = 1767.71 (out)(err) |
S = OPT O = 1264 T = 1783.97 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1264 T = 288.50 (out)(err) |
S = OPT O = 1264 T = 178.24 (out)(err) |
S = OPT O = 1264 T = 195.34 (out)(err) |
S = OPT O = 1264 T = 189.14 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1600_5.wcnf | S = OPT O = 1252 T = 76.27 |
S = N/A O = 1597 T = TO (out)(err) |
S = N/A O = 2266 T = TO (out)(err) |
S = OPT O = 1252 T = 1132.86 (out)(err) |
S = OPT O = 1252 T = 1150.97 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1252 T = 123.33 (out)(err) |
S = OPT O = 1252 T = 76.27 (out)(err) |
S = OPT O = 1252 T = 83.97 (out)(err) |
S = OPT O = 1252 T = 82.80 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1600_6.wcnf | S = OPT O = 1246 T = 31.11 |
S = N/A O = 1592 T = TO (out)(err) |
S = N/A O = 2423 T = TO (out)(err) |
S = OPT O = 1246 T = 555.71 (out)(err) |
S = OPT O = 1246 T = 576.80 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1246 T = 51.46 (out)(err) |
S = OPT O = 1246 T = 31.11 (out)(err) |
S = OPT O = 1246 T = 32.87 (out)(err) |
S = OPT O = 1246 T = 32.14 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1600_7.wcnf | S = OPT O = 1159 T = 11.94 |
S = N/A O = 1588 T = TO (out)(err) |
S = N/A O = 2316 T = TO (out)(err) |
S = OPT O = 1159 T = 73.94 (out)(err) |
S = OPT O = 1159 T = 72.83 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1159 T = 13.85 (out)(err) |
S = OPT O = 1159 T = 11.94 (out)(err) |
S = OPT O = 1159 T = 13.41 (out)(err) |
S = OPT O = 1159 T = 13.01 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1600_8.wcnf | S = OPT O = 1150 T = 5.31 |
S = N/A O = 1592 T = TO (out)(err) |
S = N/A O = 2041 T = TO (out)(err) |
S = OPT O = 1150 T = 159.35 (out)(err) |
S = OPT O = 1150 T = 164.71 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1150 T = 22.25 (out)(err) |
S = OPT O = 1150 T = 5.31 (out)(err) |
S = OPT O = 1150 T = 5.92 (out)(err) |
S = OPT O = 1150 T = 5.83 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1200_1.wcnf | S = OPT O = 780 T = 59.52 |
S = N/A O = 1052 T = TO (out)(err) |
S = N/A O = 1624 T = TO (out)(err) |
S = OPT O = 780 T = 285.33 (out)(err) |
S = OPT O = 780 T = 306.29 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 780 T = 110.36 (out)(err) |
S = OPT O = 780 T = 59.52 (out)(err) |
S = OPT O = 780 T = 68.08 (out)(err) |
S = OPT O = 780 T = 64.72 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1200_2.wcnf | S = OPT O = 733 T = 26.44 |
S = N/A O = 1188 T = TO (out)(err) |
S = N/A O = 1454 T = TO (out)(err) |
S = OPT O = 733 T = 119.86 (out)(err) |
S = OPT O = 733 T = 124.76 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 733 T = 37.54 (out)(err) |
S = OPT O = 733 T = 26.44 (out)(err) |
S = OPT O = 733 T = 30.07 (out)(err) |
S = OPT O = 733 T = 29.39 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1200_3.wcnf | S = OPT O = 741 T = 29.10 |
S = N/A O = 1014 T = TO (out)(err) |
S = N/A O = 1361 T = TO (out)(err) |
S = OPT O = 741 T = 215.25 (out)(err) |
S = OPT O = 741 T = 209.80 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 741 T = 84.10 (out)(err) |
S = OPT O = 741 T = 29.10 (out)(err) |
S = OPT O = 741 T = 33.87 (out)(err) |
S = OPT O = 741 T = 32.77 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1200_4.wcnf | S = OPT O = 667 T = 2.64 |
S = N/A O = 1113 T = TO (out)(err) |
S = N/A O = 1414 T = TO (out)(err) |
S = OPT O = 667 T = 15.13 (out)(err) |
S = OPT O = 667 T = 14.52 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 667 T = 3.69 (out)(err) |
S = OPT O = 667 T = 2.64 (out)(err) |
S = OPT O = 667 T = 3.04 (out)(err) |
S = OPT O = 667 T = 3.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1200_5.wcnf | S = OPT O = 714 T = 13.01 |
S = N/A O = 1012 T = TO (out)(err) |
S = N/A O = 1450 T = TO (out)(err) |
S = OPT O = 714 T = 63.56 (out)(err) |
S = OPT O = 714 T = 47.04 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 714 T = 22.04 (out)(err) |
S = OPT O = 714 T = 13.01 (out)(err) |
S = OPT O = 714 T = 15.30 (out)(err) |
S = OPT O = 714 T = 14.69 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1200_6.wcnf | S = OPT O = 803 T = 121.97 |
S = N/A O = 1199 T = TO (out)(err) |
S = N/A O = 1455 T = TO (out)(err) |
S = OPT O = 803 T = 460.21 (out)(err) |
S = OPT O = 803 T = 469.01 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 803 T = 130.66 (out)(err) |
S = OPT O = 803 T = 121.97 (out)(err) |
S = OPT O = 803 T = 142.53 (out)(err) |
S = OPT O = 803 T = 133.80 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1200_7.wcnf | S = OPT O = 774 T = 145.30 |
S = N/A O = 1000 T = TO (out)(err) |
S = N/A O = 1454 T = TO (out)(err) |
S = OPT O = 774 T = 456.36 (out)(err) |
S = OPT O = 774 T = 463.21 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 774 T = 209.91 (out)(err) |
S = OPT O = 774 T = 145.30 (out)(err) |
S = OPT O = 774 T = 168.62 (out)(err) |
S = OPT O = 774 T = 166.43 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1200_8.wcnf | S = OPT O = 745 T = 51.20 |
S = N/A O = 1006 T = TO (out)(err) |
S = N/A O = 1414 T = TO (out)(err) |
S = OPT O = 745 T = 223.27 (out)(err) |
S = OPT O = 745 T = 220.79 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 745 T = 105.24 (out)(err) |
S = OPT O = 745 T = 51.20 (out)(err) |
S = OPT O = 745 T = 57.65 (out)(err) |
S = OPT O = 745 T = 56.27 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1300_1.wcnf | S = OPT O = 846 T = 43.93 |
S = N/A O = 1167 T = TO (out)(err) |
S = N/A O = 1562 T = TO (out)(err) |
S = OPT O = 846 T = 189.31 (out)(err) |
S = OPT O = 846 T = 193.70 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 846 T = 59.97 (out)(err) |
S = OPT O = 846 T = 43.93 (out)(err) |
S = OPT O = 846 T = 50.51 (out)(err) |
S = OPT O = 846 T = 48.31 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1300_2.wcnf | S = OPT O = 774 T = 3.96 |
S = N/A O = 1096 T = TO (out)(err) |
S = N/A O = 1513 T = TO (out)(err) |
S = OPT O = 774 T = 26.78 (out)(err) |
S = OPT O = 774 T = 28.92 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 774 T = 7.61 (out)(err) |
S = OPT O = 774 T = 3.96 (out)(err) |
S = OPT O = 774 T = 4.52 (out)(err) |
S = OPT O = 774 T = 4.37 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1300_3.wcnf | S = OPT O = 832 T = 27.47 |
S = N/A O = 1058 T = TO (out)(err) |
S = N/A O = 1664 T = TO (out)(err) |
S = OPT O = 832 T = 315.85 (out)(err) |
S = OPT O = 832 T = 333.99 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 832 T = 55.15 (out)(err) |
S = OPT O = 832 T = 27.47 (out)(err) |
S = OPT O = 832 T = 30.96 (out)(err) |
S = OPT O = 832 T = 30.37 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1300_4.wcnf | S = OPT O = 871 T = 191.32 |
S = N/A O = 1132 T = TO (out)(err) |
S = N/A O = 1685 T = TO (out)(err) |
S = OPT O = 871 T = 668.63 (out)(err) |
S = OPT O = 871 T = 681.38 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 871 T = 293.04 (out)(err) |
S = OPT O = 871 T = 191.32 (out)(err) |
S = OPT O = 871 T = 216.43 (out)(err) |
S = OPT O = 871 T = 211.74 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1300_5.wcnf | S = OPT O = 844 T = 54.42 |
S = N/A O = 1224 T = TO (out)(err) |
S = N/A O = 1625 T = TO (out)(err) |
S = OPT O = 844 T = 222.18 (out)(err) |
S = OPT O = 844 T = 220.82 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 844 T = 62.49 (out)(err) |
S = OPT O = 844 T = 54.42 (out)(err) |
S = OPT O = 844 T = 62.18 (out)(err) |
S = OPT O = 844 T = 60.38 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1300_6.wcnf | S = OPT O = 884 T = 313.09 |
S = N/A O = 1232 T = TO (out)(err) |
S = N/A O = 1568 T = TO (out)(err) |
S = OPT O = 884 T = 1540.60 (out)(err) |
S = OPT O = 884 T = 1535.78 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 884 T = 494.07 (out)(err) |
S = OPT O = 884 T = 313.09 (out)(err) |
S = OPT O = 884 T = 353.35 (out)(err) |
S = OPT O = 884 T = 344.39 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1300_7.wcnf | S = OPT O = 874 T = 90.76 |
S = N/A O = 1099 T = TO (out)(err) |
S = N/A O = 1559 T = TO (out)(err) |
S = OPT O = 874 T = 431.86 (out)(err) |
S = OPT O = 874 T = 428.18 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 874 T = 181.63 (out)(err) |
S = OPT O = 874 T = 90.76 (out)(err) |
S = OPT O = 874 T = 104.99 (out)(err) |
S = OPT O = 874 T = 103.44 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1300_8.wcnf | S = OPT O = 812 T = 79.33 |
S = N/A O = 1039 T = TO (out)(err) |
S = N/A O = 1515 T = TO (out)(err) |
S = OPT O = 812 T = 350.25 (out)(err) |
S = OPT O = 812 T = 345.36 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 812 T = 103.24 (out)(err) |
S = OPT O = 812 T = 79.33 (out)(err) |
S = OPT O = 812 T = 91.53 (out)(err) |
S = OPT O = 812 T = 90.46 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1400_1.wcnf | S = OPT O = 926 T = 94.05 |
S = N/A O = 1297 T = TO (out)(err) |
S = N/A O = 1766 T = TO (out)(err) |
S = OPT O = 926 T = 622.48 (out)(err) |
S = OPT O = 926 T = 649.57 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 926 T = 116.03 (out)(err) |
S = OPT O = 926 T = 94.05 (out)(err) |
S = OPT O = 926 T = 106.03 (out)(err) |
S = OPT O = 926 T = 101.49 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_2.wcnf | S = OPT O = 879 T = 32.59 |
S = N/A O = 1190 T = TO (out)(err) |
S = N/A O = 1657 T = TO (out)(err) |
S = OPT O = 879 T = 110.70 (out)(err) |
S = OPT O = 879 T = 112.68 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 879 T = 40.55 (out)(err) |
S = OPT O = 879 T = 32.59 (out)(err) |
S = OPT O = 879 T = 37.45 (out)(err) |
S = OPT O = 879 T = 37.05 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_3.wcnf | S = OPT O = 936 T = 87.06 |
S = N/A O = 1236 T = TO (out)(err) |
S = N/A O = 1732 T = TO (out)(err) |
S = OPT O = 936 T = 368.56 (out)(err) |
S = OPT O = 936 T = 373.45 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 936 T = 101.22 (out)(err) |
S = OPT O = 936 T = 87.06 (out)(err) |
S = OPT O = 936 T = 99.09 (out)(err) |
S = OPT O = 936 T = 95.31 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_4.wcnf | S = OPT O = 932 T = 40.84 |
S = N/A O = 1286 T = TO (out)(err) |
S = N/A O = 1727 T = TO (out)(err) |
S = OPT O = 932 T = 244.11 (out)(err) |
S = OPT O = 932 T = 239.41 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 932 T = 98.48 (out)(err) |
S = OPT O = 932 T = 40.84 (out)(err) |
S = OPT O = 932 T = 44.97 (out)(err) |
S = OPT O = 932 T = 44.22 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_5.wcnf | S = OPT O = 968 T = 108.14 |
S = N/A O = 1537 T = TO (out)(err) |
S = N/A O = 1862 T = TO (out)(err) |
S = OPT O = 968 T = 797.73 (out)(err) |
S = OPT O = 968 T = 776.85 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 968 T = 197.10 (out)(err) |
S = OPT O = 968 T = 108.14 (out)(err) |
S = OPT O = 968 T = 121.94 (out)(err) |
S = OPT O = 968 T = 115.61 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1400_6.wcnf | S = OPT O = 967 T = 327.40 |
S = N/A O = 1330 T = TO (out)(err) |
S = N/A O = 1547 T = TO (out)(err) |
S = OPT O = 967 T = 1434.88 (out)(err) |
S = OPT O = 967 T = 1585.41 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 967 T = 464.06 (out)(err) |
S = OPT O = 967 T = 327.40 (out)(err) |
S = OPT O = 967 T = 373.43 (out)(err) |
S = OPT O = 967 T = 359.67 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1400_7.wcnf | S = OPT O = 923 T = 29.75 |
S = N/A O = 1283 T = TO (out)(err) |
S = N/A O = 1724 T = 459.20 (out)(err) |
S = OPT O = 923 T = 159.66 (out)(err) |
S = OPT O = 923 T = 152.93 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 923 T = 72.68 (out)(err) |
S = OPT O = 923 T = 29.75 (out)(err) |
S = OPT O = 923 T = 33.48 (out)(err) |
S = OPT O = 923 T = 32.02 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_8.wcnf | S = OPT O = 957 T = 147.94 |
S = N/A O = 1224 T = TO (out)(err) |
S = N/A O = 1667 T = TO (out)(err) |
S = OPT O = 957 T = 1482.04 (out)(err) |
S = OPT O = 957 T = 1315.74 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 957 T = 323.30 (out)(err) |
S = OPT O = 957 T = 147.94 (out)(err) |
S = OPT O = 957 T = 163.09 (out)(err) |
S = OPT O = 957 T = 162.66 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1500_1.wcnf | S = OPT O = 986 T = 50.69 |
S = N/A O = 1332 T = TO (out)(err) |
S = N/A O = 1737 T = TO (out)(err) |
S = OPT O = 986 T = 343.52 (out)(err) |
S = OPT O = 986 T = 337.03 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 986 T = 149.97 (out)(err) |
S = OPT O = 986 T = 50.69 (out)(err) |
S = OPT O = 986 T = 57.06 (out)(err) |
S = OPT O = 986 T = 55.13 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1500_2.wcnf | S = OPT O = 998 T = 68.31 |
S = N/A O = 1384 T = TO (out)(err) |
S = N/A O = 1734 T = TO (out)(err) |
S = OPT O = 998 T = 471.35 (out)(err) |
S = OPT O = 998 T = 488.41 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 998 T = 141.65 (out)(err) |
S = OPT O = 998 T = 68.31 (out)(err) |
S = OPT O = 998 T = 76.97 (out)(err) |
S = OPT O = 998 T = 74.81 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1500_3.wcnf | S = OPT O = 1073 T = 340.76 |
S = N/A O = 1380 T = TO (out)(err) |
S = N/A O = 1976 T = 207.85 (out)(err) |
S = OPT O = 1073 T = 1743.89 (out)(err) |
S = OPT O = 1073 T = 1737.62 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1073 T = 479.29 (out)(err) |
S = OPT O = 1073 T = 340.76 (out)(err) |
S = OPT O = 1073 T = 374.91 (out)(err) |
S = OPT O = 1073 T = 363.28 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1500_4.wcnf | S = OPT O = 1047 T = 315.02 |
S = N/A O = 1374 T = TO (out)(err) |
S = N/A O = 1795 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1047 T = 702.29 (out)(err) |
S = OPT O = 1047 T = 315.02 (out)(err) |
S = OPT O = 1047 T = 341.38 (out)(err) |
S = OPT O = 1047 T = 335.43 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1500_5.wcnf | S = OPT O = 1058 T = 189.10 |
S = N/A O = 1356 T = TO (out)(err) |
S = N/A O = 2042 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1058 T = 623.99 (out)(err) |
S = OPT O = 1058 T = 189.10 (out)(err) |
S = OPT O = 1058 T = 208.49 (out)(err) |
S = OPT O = 1058 T = 205.39 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1500_6.wcnf | S = OPT O = 1102 T = 619.78 |
S = N/A O = 1427 T = TO (out)(err) |
S = N/A O = 1772 T = 206.04 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1102 T = 663.69 (out)(err) |
S = OPT O = 1102 T = 619.78 (out)(err) |
S = OPT O = 1102 T = 713.49 (out)(err) |
S = OPT O = 1102 T = 714.04 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1500_7.wcnf | S = OPT O = 1010 T = 36.30 |
S = N/A O = 1344 T = TO (out)(err) |
S = N/A O = 2022 T = TO (out)(err) |
S = OPT O = 1010 T = 247.12 (out)(err) |
S = OPT O = 1010 T = 250.81 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1010 T = 51.97 (out)(err) |
S = OPT O = 1010 T = 36.30 (out)(err) |
S = OPT O = 1010 T = 40.73 (out)(err) |
S = OPT O = 1010 T = 39.23 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1500_8.wcnf | S = OPT O = 1045 T = 110.74 |
S = N/A O = 1472 T = TO (out)(err) |
S = N/A O = 1980 T = TO (out)(err) |
S = OPT O = 1045 T = 650.52 (out)(err) |
S = OPT O = 1045 T = 646.49 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1045 T = 203.06 (out)(err) |
S = OPT O = 1045 T = 110.74 (out)(err) |
S = OPT O = 1045 T = 127.54 (out)(err) |
S = OPT O = 1045 T = 121.62 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1600_1.wcnf | S = OPT O = 1143 T = 62.85 |
S = N/A O = 1622 T = TO (out)(err) |
S = N/A O = 2242 T = TO (out)(err) |
S = OPT O = 1143 T = 406.21 (out)(err) |
S = OPT O = 1143 T = 415.91 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1143 T = 106.41 (out)(err) |
S = OPT O = 1143 T = 62.85 (out)(err) |
S = OPT O = 1143 T = 70.73 (out)(err) |
S = OPT O = 1143 T = 68.83 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1600_2.wcnf | S = OPT O = 1140 T = 57.32 |
S = N/A O = 1477 T = TO (out)(err) |
S = N/A O = 2218 T = 415.65 (out)(err) |
S = OPT O = 1140 T = 437.41 (out)(err) |
S = OPT O = 1140 T = 438.45 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1140 T = 85.06 (out)(err) |
S = OPT O = 1140 T = 57.32 (out)(err) |
S = OPT O = 1140 T = 63.86 (out)(err) |
S = OPT O = 1140 T = 61.84 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1600_3.wcnf | S = OPT O = 1079 T = 61.04 |
S = N/A O = 1395 T = TO (out)(err) |
S = N/A O = 1884 T = 489.36 (out)(err) |
S = OPT O = 1079 T = 281.37 (out)(err) |
S = OPT O = 1079 T = 281.52 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1079 T = 64.38 (out)(err) |
S = OPT O = 1079 T = 61.04 (out)(err) |
S = OPT O = 1079 T = 69.08 (out)(err) |
S = OPT O = 1079 T = 66.56 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1600_4.wcnf | S = OPT O = 1157 T = 192.79 |
S = N/A O = 1606 T = TO (out)(err) |
S = N/A O = 2133 T = 447.39 (out)(err) |
S = OPT O = 1157 T = 1188.30 (out)(err) |
S = OPT O = 1157 T = 1195.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1157 T = 193.14 (out)(err) |
S = OPT O = 1157 T = 192.79 (out)(err) |
S = OPT O = 1157 T = 207.31 (out)(err) |
S = OPT O = 1157 T = 201.18 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1600_5.wcnf | S = OPT O = 1119 T = 168.93 |
S = N/A O = 1563 T = TO (out)(err) |
S = N/A O = 2085 T = TO (out)(err) |
S = OPT O = 1119 T = 1552.57 (out)(err) |
S = OPT O = 1119 T = 1576.09 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1119 T = 315.68 (out)(err) |
S = OPT O = 1119 T = 168.93 (out)(err) |
S = OPT O = 1119 T = 187.69 (out)(err) |
S = OPT O = 1119 T = 181.70 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1600_6.wcnf | S = OPT O = 1212 T = 400.74 |
S = N/A O = 1628 T = TO (out)(err) |
S = N/A O = 2123 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1212 T = 518.49 (out)(err) |
S = OPT O = 1212 T = 400.74 (out)(err) |
S = OPT O = 1212 T = 446.16 (out)(err) |
S = OPT O = 1212 T = 431.24 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1600_7.wcnf | S = OPT O = 1150 T = 163.91 |
S = N/A O = 1698 T = TO (out)(err) |
S = N/A O = 1980 T = TO (out)(err) |
S = OPT O = 1150 T = 1579.41 (out)(err) |
S = OPT O = 1150 T = 1728.86 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1150 T = 321.14 (out)(err) |
S = OPT O = 1150 T = 163.91 (out)(err) |
S = OPT O = 1150 T = 176.63 (out)(err) |
S = OPT O = 1150 T = 172.56 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1600_8.wcnf | S = OPT O = 1180 T = 140.18 |
S = N/A O = 1526 T = TO (out)(err) |
S = N/A O = 2224 T = TO (out)(err) |
S = OPT O = 1180 T = 996.15 (out)(err) |
S = OPT O = 1180 T = 997.25 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1180 T = 200.15 (out)(err) |
S = OPT O = 1180 T = 140.18 (out)(err) |
S = OPT O = 1180 T = 166.77 (out)(err) |
S = OPT O = 1180 T = 154.80 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C1000_0.wcnf | S = OPT O = 198 T = 169.89 |
S = N/A O = 331 T = TO (out)(err) |
S = N/A O = 761 T = TO (out)(err) |
S = OPT O = 198 T = 731.12 (out)(err) |
S = OPT O = 198 T = 738.48 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 198 T = 247.51 (out)(err) |
S = OPT O = 198 T = 169.89 (out)(err) |
S = OPT O = 198 T = 188.39 (out)(err) |
S = OPT O = 198 T = 187.13 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C1000_1.wcnf | S = OPT O = 212 T = 132.70 |
S = N/A O = 356 T = TO (out)(err) |
S = N/A O = 838 T = TO (out)(err) |
S = OPT O = 212 T = 395.12 (out)(err) |
S = OPT O = 212 T = 398.29 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 212 T = 162.99 (out)(err) |
S = OPT O = 212 T = 132.70 (out)(err) |
S = OPT O = 212 T = 149.23 (out)(err) |
S = OPT O = 212 T = 145.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C1000_2.wcnf | S = OPT O = 211 T = 205.72 |
S = N/A O = 334 T = TO (out)(err) |
S = N/A O = 772 T = TO (out)(err) |
S = OPT O = 211 T = 581.45 (out)(err) |
S = OPT O = 211 T = 582.01 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 211 T = 226.07 (out)(err) |
S = OPT O = 211 T = 205.72 (out)(err) |
S = OPT O = 211 T = 223.58 (out)(err) |
S = OPT O = 211 T = 220.59 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C1000_3.wcnf | S = OPT O = 229 T = 275.74 |
S = N/A O = 338 T = TO (out)(err) |
S = N/A O = 795 T = TO (out)(err) |
S = OPT O = 229 T = 801.45 (out)(err) |
S = OPT O = 229 T = 811.40 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 229 T = 312.88 (out)(err) |
S = OPT O = 229 T = 275.74 (out)(err) |
S = OPT O = 229 T = 311.54 (out)(err) |
S = OPT O = 229 T = 305.82 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C1000_4.wcnf | S = OPT O = 202 T = 146.55 |
S = N/A O = 602 T = TO (out)(err) |
S = N/A O = 702 T = TO (out)(err) |
S = OPT O = 202 T = 506.09 (out)(err) |
S = OPT O = 202 T = 508.43 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 202 T = 203.06 (out)(err) |
S = OPT O = 202 T = 146.55 (out)(err) |
S = OPT O = 202 T = 164.04 (out)(err) |
S = OPT O = 202 T = 162.02 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C1000_5.wcnf | S = OPT O = 214 T = 156.92 |
S = N/A O = 371 T = TO (out)(err) |
S = N/A O = 798 T = TO (out)(err) |
S = OPT O = 214 T = 937.89 (out)(err) |
S = OPT O = 214 T = 945.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 214 T = 392.65 (out)(err) |
S = OPT O = 214 T = 156.92 (out)(err) |
S = OPT O = 214 T = 177.81 (out)(err) |
S = OPT O = 214 T = 172.92 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C1000_6.wcnf | S = OPT O = 203 T = 106.94 |
S = N/A O = 443 T = TO (out)(err) |
S = N/A O = 629 T = TO (out)(err) |
S = OPT O = 203 T = 246.30 (out)(err) |
S = OPT O = 203 T = 248.17 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 203 T = 107.29 (out)(err) |
S = OPT O = 203 T = 106.94 (out)(err) |
S = OPT O = 203 T = 118.00 (out)(err) |
S = OPT O = 203 T = 117.38 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C1000_7.wcnf | S = OPT O = 200 T = 91.74 |
S = N/A O = 221 T = TO (out)(err) |
S = N/A O = 722 T = TO (out)(err) |
S = OPT O = 200 T = 260.66 (out)(err) |
S = OPT O = 200 T = 260.90 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 200 T = 146.67 (out)(err) |
S = OPT O = 200 T = 91.74 (out)(err) |
S = OPT O = 200 T = 102.21 (out)(err) |
S = OPT O = 200 T = 100.29 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C1000_8.wcnf | S = OPT O = 188 T = 51.48 |
S = N/A O = 430 T = TO (out)(err) |
S = N/A O = 709 T = TO (out)(err) |
S = OPT O = 188 T = 378.82 (out)(err) |
S = OPT O = 188 T = 383.30 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 188 T = 141.93 (out)(err) |
S = OPT O = 188 T = 51.48 (out)(err) |
S = OPT O = 188 T = 57.64 (out)(err) |
S = OPT O = 188 T = 57.01 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C1000_9.wcnf | S = OPT O = 226 T = 282.63 |
S = N/A O = 369 T = TO (out)(err) |
S = N/A O = 766 T = TO (out)(err) |
S = OPT O = 226 T = 764.96 (out)(err) |
S = OPT O = 226 T = 774.96 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 226 T = 282.63 (out)(err) |
S = OPT O = 226 T = 290.29 (out)(err) |
S = OPT O = 226 T = 317.48 (out)(err) |
S = OPT O = 226 T = 314.25 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C700_0.wcnf | S = OPT O = 103 T = 32.25 |
S = N/A O = 346 T = TO (out)(err) |
S = N/A O = 325 T = TO (out)(err) |
S = OPT O = 103 T = 89.91 (out)(err) |
S = OPT O = 103 T = 89.62 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 103 T = 43.02 (out)(err) |
S = OPT O = 103 T = 32.25 (out)(err) |
S = OPT O = 103 T = 37.70 (out)(err) |
S = OPT O = 103 T = 36.85 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C700_1.wcnf | S = OPT O = 107 T = 19.67 |
S = N/A O = 169 T = TO (out)(err) |
S = N/A O = 319 T = TO (out)(err) |
S = OPT O = 107 T = 47.51 (out)(err) |
S = OPT O = 107 T = 47.12 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 107 T = 25.71 (out)(err) |
S = OPT O = 107 T = 19.67 (out)(err) |
S = OPT O = 107 T = 22.41 (out)(err) |
S = OPT O = 107 T = 22.35 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C700_2.wcnf | S = OPT O = 110 T = 32.40 |
S = N/A O = 163 T = TO (out)(err) |
S = N/A O = 407 T = TO (out)(err) |
S = OPT O = 110 T = 74.37 (out)(err) |
S = OPT O = 110 T = 74.59 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 110 T = 32.65 (out)(err) |
S = OPT O = 110 T = 32.40 (out)(err) |
S = OPT O = 110 T = 37.12 (out)(err) |
S = OPT O = 110 T = 37.19 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C700_3.wcnf | S = OPT O = 102 T = 12.32 |
S = N/A O = 228 T = TO (out)(err) |
S = N/A O = 377 T = TO (out)(err) |
S = OPT O = 102 T = 25.17 (out)(err) |
S = OPT O = 102 T = 24.81 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 102 T = 14.21 (out)(err) |
S = OPT O = 102 T = 12.32 (out)(err) |
S = OPT O = 102 T = 14.34 (out)(err) |
S = OPT O = 102 T = 14.20 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C700_4.wcnf | S = OPT O = 110 T = 26.29 |
S = N/A O = 152 T = TO (out)(err) |
S = N/A O = 431 T = TO (out)(err) |
S = OPT O = 110 T = 86.58 (out)(err) |
S = OPT O = 110 T = 86.87 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 110 T = 41.94 (out)(err) |
S = OPT O = 110 T = 26.29 (out)(err) |
S = OPT O = 110 T = 29.54 (out)(err) |
S = OPT O = 110 T = 29.37 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C700_5.wcnf | S = OPT O = 103 T = 15.42 |
S = N/A O = 237 T = TO (out)(err) |
S = N/A O = 365 T = TO (out)(err) |
S = OPT O = 103 T = 56.09 (out)(err) |
S = OPT O = 103 T = 55.79 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 103 T = 30.99 (out)(err) |
S = OPT O = 103 T = 15.42 (out)(err) |
S = OPT O = 103 T = 17.37 (out)(err) |
S = OPT O = 103 T = 17.20 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C700_6.wcnf | S = OPT O = 102 T = 15.85 |
S = N/A O = 137 T = TO (out)(err) |
S = N/A O = 374 T = TO (out)(err) |
S = OPT O = 102 T = 41.41 (out)(err) |
S = OPT O = 102 T = 41.24 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 102 T = 20.15 (out)(err) |
S = OPT O = 102 T = 15.85 (out)(err) |
S = OPT O = 102 T = 18.57 (out)(err) |
S = OPT O = 102 T = 18.34 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C700_7.wcnf | S = OPT O = 104 T = 20.47 |
S = N/A O = 273 T = TO (out)(err) |
S = N/A O = 378 T = TO (out)(err) |
S = OPT O = 104 T = 44.33 (out)(err) |
S = OPT O = 104 T = 44.19 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 104 T = 22.48 (out)(err) |
S = OPT O = 104 T = 20.47 (out)(err) |
S = OPT O = 104 T = 24.07 (out)(err) |
S = OPT O = 104 T = 23.82 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C700_8.wcnf | S = OPT O = 82 T = 3.76 |
S = N/A O = 314 T = TO (out)(err) |
S = N/A O = 390 T = TO (out)(err) |
S = OPT O = 82 T = 6.89 (out)(err) |
S = OPT O = 82 T = 6.89 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 82 T = 3.91 (out)(err) |
S = OPT O = 82 T = 3.76 (out)(err) |
S = OPT O = 82 T = 4.35 (out)(err) |
S = OPT O = 82 T = 4.36 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C700_9.wcnf | S = OPT O = 104 T = 20.12 |
S = N/A O = 288 T = TO (out)(err) |
S = N/A O = 346 T = TO (out)(err) |
S = OPT O = 104 T = 49.67 (out)(err) |
S = OPT O = 104 T = 50.15 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 104 T = 21.06 (out)(err) |
S = OPT O = 104 T = 20.12 (out)(err) |
S = OPT O = 104 T = 23.02 (out)(err) |
S = OPT O = 104 T = 22.82 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C800_0.wcnf | S = OPT O = 132 T = 37.32 |
S = N/A O = 429 T = TO (out)(err) |
S = N/A O = 536 T = TO (out)(err) |
S = OPT O = 132 T = 114.34 (out)(err) |
S = OPT O = 132 T = 115.12 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 132 T = 48.37 (out)(err) |
S = OPT O = 132 T = 37.32 (out)(err) |
S = OPT O = 132 T = 42.02 (out)(err) |
S = OPT O = 132 T = 40.92 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C800_1.wcnf | S = OPT O = 138 T = 44.63 |
S = N/A O = 183 T = TO (out)(err) |
S = N/A O = 505 T = TO (out)(err) |
S = OPT O = 138 T = 180.26 (out)(err) |
S = OPT O = 138 T = 179.05 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 138 T = 73.50 (out)(err) |
S = OPT O = 138 T = 44.63 (out)(err) |
S = OPT O = 138 T = 50.18 (out)(err) |
S = OPT O = 138 T = 49.62 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C800_2.wcnf | S = OPT O = 127 T = 23.14 |
S = N/A O = 399 T = TO (out)(err) |
S = N/A O = 502 T = TO (out)(err) |
S = OPT O = 127 T = 107.15 (out)(err) |
S = OPT O = 127 T = 107.43 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 127 T = 48.91 (out)(err) |
S = OPT O = 127 T = 23.14 (out)(err) |
S = OPT O = 127 T = 26.57 (out)(err) |
S = OPT O = 127 T = 26.11 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C800_3.wcnf | S = OPT O = 134 T = 13.11 |
S = N/A O = 291 T = TO (out)(err) |
S = N/A O = 591 T = TO (out)(err) |
S = OPT O = 134 T = 68.46 (out)(err) |
S = OPT O = 134 T = 68.43 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 134 T = 21.91 (out)(err) |
S = OPT O = 134 T = 13.11 (out)(err) |
S = OPT O = 134 T = 14.97 (out)(err) |
S = OPT O = 134 T = 14.89 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C800_4.wcnf | S = OPT O = 143 T = 43.98 |
S = N/A O = 443 T = TO (out)(err) |
S = N/A O = 633 T = TO (out)(err) |
S = OPT O = 143 T = 255.44 (out)(err) |
S = OPT O = 143 T = 255.22 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 143 T = 154.01 (out)(err) |
S = OPT O = 143 T = 43.98 (out)(err) |
S = OPT O = 143 T = 50.23 (out)(err) |
S = OPT O = 143 T = 49.20 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C800_5.wcnf | S = OPT O = 144 T = 74.54 |
S = N/A O = 252 T = TO (out)(err) |
S = N/A O = 598 T = TO (out)(err) |
S = OPT O = 144 T = 283.64 (out)(err) |
S = OPT O = 144 T = 283.50 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 144 T = 118.20 (out)(err) |
S = OPT O = 144 T = 74.54 (out)(err) |
S = OPT O = 144 T = 86.01 (out)(err) |
S = OPT O = 144 T = 84.20 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C800_6.wcnf | S = OPT O = 135 T = 41.43 |
S = N/A O = 371 T = TO (out)(err) |
S = N/A O = 518 T = TO (out)(err) |
S = OPT O = 135 T = 123.59 (out)(err) |
S = OPT O = 135 T = 123.90 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 135 T = 62.39 (out)(err) |
S = OPT O = 135 T = 41.43 (out)(err) |
S = OPT O = 135 T = 46.40 (out)(err) |
S = OPT O = 135 T = 46.54 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C800_7.wcnf | S = OPT O = 147 T = 44.28 |
S = N/A O = 232 T = TO (out)(err) |
S = N/A O = 596 T = TO (out)(err) |
S = OPT O = 147 T = 201.82 (out)(err) |
S = OPT O = 147 T = 204.08 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 147 T = 61.88 (out)(err) |
S = OPT O = 147 T = 44.28 (out)(err) |
S = OPT O = 147 T = 50.15 (out)(err) |
S = OPT O = 147 T = 50.36 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C800_8.wcnf | S = OPT O = 126 T = 22.12 |
S = N/A O = 392 T = TO (out)(err) |
S = N/A O = 542 T = TO (out)(err) |
S = OPT O = 126 T = 134.91 (out)(err) |
S = OPT O = 126 T = 134.34 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 126 T = 60.30 (out)(err) |
S = OPT O = 126 T = 22.12 (out)(err) |
S = OPT O = 126 T = 25.43 (out)(err) |
S = OPT O = 126 T = 24.90 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C800_9.wcnf | S = OPT O = 138 T = 34.08 |
S = N/A O = 381 T = TO (out)(err) |
S = N/A O = 496 T = TO (out)(err) |
S = OPT O = 138 T = 120.93 (out)(err) |
S = OPT O = 138 T = 120.59 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 138 T = 57.51 (out)(err) |
S = OPT O = 138 T = 34.08 (out)(err) |
S = OPT O = 138 T = 38.96 (out)(err) |
S = OPT O = 138 T = 39.59 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C900_0.wcnf | S = OPT O = 157 T = 51.75 |
S = N/A O = 293 T = TO (out)(err) |
S = N/A O = 698 T = TO (out)(err) |
S = OPT O = 157 T = 127.58 (out)(err) |
S = OPT O = 157 T = 128.41 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 157 T = 53.78 (out)(err) |
S = OPT O = 157 T = 51.75 (out)(err) |
S = OPT O = 157 T = 60.02 (out)(err) |
S = OPT O = 157 T = 58.45 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C900_1.wcnf | S = OPT O = 192 T = 177.39 |
S = N/A O = 243 T = TO (out)(err) |
S = N/A O = 691 T = TO (out)(err) |
S = OPT O = 192 T = 445.00 (out)(err) |
S = OPT O = 192 T = 446.25 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 192 T = 214.75 (out)(err) |
S = OPT O = 192 T = 177.39 (out)(err) |
S = OPT O = 192 T = 200.22 (out)(err) |
S = OPT O = 192 T = 198.48 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C900_2.wcnf | S = OPT O = 177 T = 126.24 |
S = N/A O = 211 T = TO (out)(err) |
S = N/A O = 574 T = TO (out)(err) |
S = OPT O = 177 T = 369.22 (out)(err) |
S = OPT O = 177 T = 373.56 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 177 T = 157.69 (out)(err) |
S = OPT O = 177 T = 126.24 (out)(err) |
S = OPT O = 177 T = 142.08 (out)(err) |
S = OPT O = 177 T = 139.44 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C900_3.wcnf | S = OPT O = 163 T = 57.86 |
S = N/A O = 242 T = TO (out)(err) |
S = N/A O = 459 T = TO (out)(err) |
S = OPT O = 163 T = 237.84 (out)(err) |
S = OPT O = 163 T = 239.51 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 163 T = 85.84 (out)(err) |
S = OPT O = 163 T = 57.86 (out)(err) |
S = OPT O = 163 T = 66.20 (out)(err) |
S = OPT O = 163 T = 63.72 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C900_4.wcnf | S = OPT O = 171 T = 105.79 |
S = N/A O = 413 T = TO (out)(err) |
S = N/A O = 660 T = TO (out)(err) |
S = OPT O = 171 T = 318.98 (out)(err) |
S = OPT O = 171 T = 320.26 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 171 T = 136.85 (out)(err) |
S = OPT O = 171 T = 105.79 (out)(err) |
S = OPT O = 171 T = 118.38 (out)(err) |
S = OPT O = 171 T = 118.61 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C900_5.wcnf | S = OPT O = 175 T = 89.41 |
S = N/A O = 499 T = TO (out)(err) |
S = N/A O = 614 T = TO (out)(err) |
S = OPT O = 175 T = 211.12 (out)(err) |
S = OPT O = 175 T = 212.93 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 175 T = 102.64 (out)(err) |
S = OPT O = 175 T = 89.41 (out)(err) |
S = OPT O = 175 T = 101.53 (out)(err) |
S = OPT O = 175 T = 99.79 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C900_6.wcnf | S = OPT O = 174 T = 82.36 |
S = N/A O = 466 T = TO (out)(err) |
S = N/A O = 542 T = 1581.02 (out)(err) |
S = OPT O = 174 T = 221.42 (out)(err) |
S = OPT O = 174 T = 223.25 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 174 T = 149.41 (out)(err) |
S = OPT O = 174 T = 82.36 (out)(err) |
S = OPT O = 174 T = 94.55 (out)(err) |
S = OPT O = 174 T = 90.57 (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C900_7.wcnf | S = OPT O = 194 T = 192.02 |
S = N/A O = 271 T = TO (out)(err) |
S = N/A O = 802 T = TO (out)(err) |
S = OPT O = 194 T = 643.70 (out)(err) |
S = OPT O = 194 T = 644.76 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 194 T = 250.73 (out)(err) |
S = OPT O = 194 T = 192.02 (out)(err) |
S = OPT O = 194 T = 213.62 (out)(err) |
S = OPT O = 194 T = 211.98 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C900_8.wcnf | S = OPT O = 179 T = 106.06 |
S = N/A O = 244 T = TO (out)(err) |
S = N/A O = 589 T = TO (out)(err) |
S = OPT O = 179 T = 239.63 (out)(err) |
S = OPT O = 179 T = 240.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 179 T = 107.58 (out)(err) |
S = OPT O = 179 T = 106.06 (out)(err) |
S = OPT O = 179 T = 116.51 (out)(err) |
S = OPT O = 179 T = 114.26 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C900_9.wcnf | S = OPT O = 181 T = 98.09 |
S = N/A O = 450 T = TO (out)(err) |
S = N/A O = 756 T = TO (out)(err) |
S = OPT O = 181 T = 255.38 (out)(err) |
S = OPT O = 181 T = 257.25 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 181 T = 116.58 (out)(err) |
S = OPT O = 181 T = 98.09 (out)(err) |
S = OPT O = 181 T = 111.83 (out)(err) |
S = OPT O = 181 T = 108.76 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |