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 | IncWMaxSatz | WMaxSatz+ | WMaxSatz-2009 | WPM1 | WPM2 | akmaxsat | akmaxsat_ls | claspMaxSat | sat4j-maxsat | wbo1.6 |
---|---|---|---|---|---|---|---|---|---|---|---|
s2v100c1200_1.wcnf | S = OPT O = 865 T = 5.03 |
S = OPT O = 865 T = 84.16 (out)(err) |
S = OPT O = 865 T = 46.46 (out)(err) |
S = OPT O = 865 T = 44.27 (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 = 865 T = 11.40 (out)(err) |
S = OPT O = 865 T = 5.03 (out)(err) |
S = N/A O = 1126 T = TO (out)(err) |
S = N/A O = 1176 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1200_2.wcnf | S = OPT O = 774 T = 3.45 |
S = OPT O = 774 T = 60.81 (out)(err) |
S = OPT O = 774 T = 27.93 (out)(err) |
S = OPT O = 774 T = 30.55 (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 = 774 T = 8.52 (out)(err) |
S = OPT O = 774 T = 3.45 (out)(err) |
S = N/A O = 953 T = TO (out)(err) |
S = N/A O = 1100 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1200_3.wcnf | S = OPT O = 933 T = 33.08 |
S = OPT O = 933 T = 371.26 (out)(err) |
S = OPT O = 933 T = 202.19 (out)(err) |
S = OPT O = 933 T = 203.89 (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 = 933 T = 52.37 (out)(err) |
S = OPT O = 933 T = 33.08 (out)(err) |
S = N/A O = 1108 T = TO (out)(err) |
S = N/A O = 1127 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1200_4.wcnf | S = OPT O = 798 T = 3.76 |
S = OPT O = 798 T = 43.80 (out)(err) |
S = OPT O = 798 T = 17.16 (out)(err) |
S = OPT O = 798 T = 16.88 (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 = 798 T = 7.01 (out)(err) |
S = OPT O = 798 T = 3.76 (out)(err) |
S = N/A O = 1044 T = TO (out)(err) |
S = N/A O = 1090 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1200_5.wcnf | S = OPT O = 876 T = 4.45 |
S = OPT O = 876 T = 96.33 (out)(err) |
S = OPT O = 876 T = 43.88 (out)(err) |
S = OPT O = 876 T = 44.70 (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 = 876 T = 9.22 (out)(err) |
S = OPT O = 876 T = 4.45 (out)(err) |
S = N/A O = 1035 T = TO (out)(err) |
S = N/A O = 1160 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1200_6.wcnf | S = OPT O = 734 T = 0.72 |
S = OPT O = 734 T = 8.24 (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 = N/A O = N/A T = TO (out)(err) |
S = OPT O = 734 T = 1.12 (out)(err) |
S = OPT O = 734 T = 0.72 (out)(err) |
S = N/A O = 1009 T = TO (out)(err) |
S = N/A O = 1011 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1200_7.wcnf | S = OPT O = 800 T = 12.62 |
S = OPT O = 800 T = 98.35 (out)(err) |
S = OPT O = 800 T = 75.25 (out)(err) |
S = OPT O = 800 T = 72.29 (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 = 800 T = 23.24 (out)(err) |
S = OPT O = 800 T = 12.62 (out)(err) |
S = N/A O = 1006 T = TO (out)(err) |
S = N/A O = 1120 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1200_8.wcnf | S = OPT O = 962 T = 38.98 |
S = OPT O = 962 T = 492.39 (out)(err) |
S = OPT O = 962 T = 350.78 (out)(err) |
S = OPT O = 962 T = 350.88 (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 = 962 T = 52.98 (out)(err) |
S = OPT O = 962 T = 38.98 (out)(err) |
S = N/A O = 1185 T = TO (out)(err) |
S = N/A O = 1206 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_1.wcnf | S = OPT O = 971 T = 10.43 |
S = OPT O = 971 T = 127.71 (out)(err) |
S = OPT O = 971 T = 72.62 (out)(err) |
S = OPT O = 971 T = 67.86 (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 = 971 T = 11.12 (out)(err) |
S = OPT O = 971 T = 10.43 (out)(err) |
S = N/A O = 1229 T = TO (out)(err) |
S = N/A O = 1249 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_2.wcnf | S = OPT O = 930 T = 13.62 |
S = OPT O = 930 T = 247.89 (out)(err) |
S = OPT O = 930 T = 234.73 (out)(err) |
S = OPT O = 930 T = 237.48 (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 = 930 T = 20.85 (out)(err) |
S = OPT O = 930 T = 13.62 (out)(err) |
S = N/A O = 1194 T = TO (out)(err) |
S = N/A O = 1216 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_3.wcnf | S = OPT O = 925 T = 4.06 |
S = OPT O = 925 T = 77.04 (out)(err) |
S = OPT O = 925 T = 41.37 (out)(err) |
S = OPT O = 925 T = 42.65 (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 = 925 T = 12.30 (out)(err) |
S = OPT O = 925 T = 4.06 (out)(err) |
S = N/A O = 1152 T = TO (out)(err) |
S = N/A O = 1141 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1300_4.wcnf | S = OPT O = 970 T = 8.64 |
S = OPT O = 970 T = 198.24 (out)(err) |
S = OPT O = 970 T = 116.94 (out)(err) |
S = OPT O = 970 T = 117.02 (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 = 970 T = 18.54 (out)(err) |
S = OPT O = 970 T = 8.64 (out)(err) |
S = N/A O = 1234 T = TO (out)(err) |
S = N/A O = 1370 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_5.wcnf | S = OPT O = 962 T = 16.34 |
S = OPT O = 962 T = 432.91 (out)(err) |
S = OPT O = 962 T = 218.00 (out)(err) |
S = OPT O = 962 T = 226.90 (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 = 962 T = 39.53 (out)(err) |
S = OPT O = 962 T = 16.34 (out)(err) |
S = N/A O = 1202 T = TO (out)(err) |
S = N/A O = 1245 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1300_6.wcnf | S = OPT O = 933 T = 6.30 |
S = OPT O = 933 T = 80.63 (out)(err) |
S = OPT O = 933 T = 48.24 (out)(err) |
S = OPT O = 933 T = 50.80 (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 = 933 T = 6.58 (out)(err) |
S = OPT O = 933 T = 6.30 (out)(err) |
S = N/A O = 1179 T = TO (out)(err) |
S = N/A O = 1256 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_7.wcnf | S = OPT O = 877 T = 4.36 |
S = OPT O = 877 T = 120.10 (out)(err) |
S = OPT O = 877 T = 49.18 (out)(err) |
S = OPT O = 877 T = 48.11 (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 = 877 T = 14.14 (out)(err) |
S = OPT O = 877 T = 4.36 (out)(err) |
S = N/A O = 1157 T = TO (out)(err) |
S = N/A O = 1161 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_8.wcnf | S = OPT O = 941 T = 10.31 |
S = OPT O = 941 T = 331.40 (out)(err) |
S = OPT O = 941 T = 157.52 (out)(err) |
S = OPT O = 941 T = 160.72 (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 = 941 T = 31.23 (out)(err) |
S = OPT O = 941 T = 10.31 (out)(err) |
S = N/A O = 1190 T = TO (out)(err) |
S = N/A O = 1202 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1400_1.wcnf | S = OPT O = 1019 T = 25.40 |
S = OPT O = 1019 T = 350.62 (out)(err) |
S = OPT O = 1019 T = 167.23 (out)(err) |
S = OPT O = 1019 T = 168.66 (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 = 1019 T = 44.15 (out)(err) |
S = OPT O = 1019 T = 25.40 (out)(err) |
S = N/A O = 1269 T = TO (out)(err) |
S = N/A O = 1283 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1400_2.wcnf | S = OPT O = 1002 T = 12.76 |
S = OPT O = 1002 T = 212.51 (out)(err) |
S = OPT O = 1002 T = 135.95 (out)(err) |
S = OPT O = 1002 T = 132.01 (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 = 1002 T = 17.04 (out)(err) |
S = OPT O = 1002 T = 12.76 (out)(err) |
S = N/A O = 1224 T = TO (out)(err) |
S = N/A O = 1237 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1400_3.wcnf | S = OPT O = 1020 T = 22.02 |
S = OPT O = 1020 T = 353.01 (out)(err) |
S = OPT O = 1020 T = 281.12 (out)(err) |
S = OPT O = 1020 T = 271.58 (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 = 1020 T = 23.61 (out)(err) |
S = OPT O = 1020 T = 22.02 (out)(err) |
S = N/A O = 1202 T = TO (out)(err) |
S = N/A O = 1263 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1400_4.wcnf | S = OPT O = 1094 T = 40.64 |
S = OPT O = 1094 T = 701.95 (out)(err) |
S = OPT O = 1094 T = 329.14 (out)(err) |
S = OPT O = 1094 T = 356.98 (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 = 1094 T = 53.43 (out)(err) |
S = OPT O = 1094 T = 40.64 (out)(err) |
S = N/A O = 1338 T = TO (out)(err) |
S = N/A O = 1392 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1400_5.wcnf | S = OPT O = 1018 T = 13.74 |
S = OPT O = 1018 T = 237.84 (out)(err) |
S = OPT O = 1018 T = 168.54 (out)(err) |
S = OPT O = 1018 T = 163.98 (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 = 1018 T = 22.09 (out)(err) |
S = OPT O = 1018 T = 13.74 (out)(err) |
S = N/A O = 1289 T = TO (out)(err) |
S = N/A O = 1340 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1400_6.wcnf | S = OPT O = 997 T = 2.99 |
S = OPT O = 997 T = 156.42 (out)(err) |
S = OPT O = 997 T = 33.68 (out)(err) |
S = OPT O = 997 T = 33.70 (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 = 997 T = 5.40 (out)(err) |
S = OPT O = 997 T = 2.99 (out)(err) |
S = N/A O = 1290 T = TO (out)(err) |
S = N/A O = 1375 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1400_7.wcnf | S = OPT O = 1001 T = 39.94 |
S = OPT O = 1001 T = 451.02 (out)(err) |
S = OPT O = 1001 T = 246.14 (out)(err) |
S = OPT O = 1001 T = 250.52 (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 = 1001 T = 45.43 (out)(err) |
S = OPT O = 1001 T = 39.94 (out)(err) |
S = N/A O = 1265 T = TO (out)(err) |
S = N/A O = 1329 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1400_8.wcnf | S = OPT O = 1084 T = 22.36 |
S = OPT O = 1084 T = 466.62 (out)(err) |
S = OPT O = 1084 T = 166.92 (out)(err) |
S = OPT O = 1084 T = 303.39 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 195.93 (out)(err) |
S = OPT O = 1084 T = 38.07 (out)(err) |
S = OPT O = 1084 T = 22.36 (out)(err) |
S = N/A O = 1363 T = TO (out)(err) |
S = N/A O = 1324 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1500_1.wcnf | S = OPT O = 1077 T = 15.07 |
S = OPT O = 1077 T = 225.99 (out)(err) |
S = OPT O = 1077 T = 124.74 (out)(err) |
S = OPT O = 1077 T = 123.86 (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 = 1077 T = 29.96 (out)(err) |
S = OPT O = 1077 T = 15.07 (out)(err) |
S = N/A O = 1386 T = TO (out)(err) |
S = N/A O = 1381 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1500_2.wcnf | S = OPT O = 1125 T = 19.28 |
S = OPT O = 1125 T = 535.01 (out)(err) |
S = OPT O = 1125 T = 304.20 (out)(err) |
S = OPT O = 1125 T = 304.15 (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 = 1125 T = 22.42 (out)(err) |
S = OPT O = 1125 T = 19.28 (out)(err) |
S = N/A O = 1413 T = TO (out)(err) |
S = N/A O = 1410 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1500_3.wcnf | S = OPT O = 1151 T = 41.12 |
S = OPT O = 1151 T = 673.51 (out)(err) |
S = OPT O = 1151 T = 292.82 (out)(err) |
S = OPT O = 1151 T = 292.12 (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 = 1151 T = 43.15 (out)(err) |
S = OPT O = 1151 T = 41.12 (out)(err) |
S = N/A O = 1401 T = TO (out)(err) |
S = N/A O = 1378 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1500_4.wcnf | S = OPT O = 1072 T = 15.48 |
S = OPT O = 1072 T = 609.52 (out)(err) |
S = OPT O = 1072 T = 303.21 (out)(err) |
S = OPT O = 1072 T = 304.89 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 21.51 (out)(err) |
S = OPT O = 1072 T = 73.14 (out)(err) |
S = OPT O = 1072 T = 15.48 (out)(err) |
S = N/A O = 1340 T = TO (out)(err) |
S = N/A O = 1452 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1500_5.wcnf | S = OPT O = 1151 T = 32.47 |
S = OPT O = 1151 T = 780.39 (out)(err) |
S = OPT O = 1151 T = 349.28 (out)(err) |
S = OPT O = 1151 T = 393.82 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 101.11 (out)(err) |
S = OPT O = 1151 T = 40.27 (out)(err) |
S = OPT O = 1151 T = 32.47 (out)(err) |
S = N/A O = 1400 T = TO (out)(err) |
S = N/A O = 1361 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1500_6.wcnf | S = OPT O = 1225 T = 38.18 |
S = OPT O = 1225 T = 1129.62 (out)(err) |
S = OPT O = 1225 T = 665.24 (out)(err) |
S = OPT O = 1225 T = 697.91 (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 = 1225 T = 78.86 (out)(err) |
S = OPT O = 1225 T = 38.18 (out)(err) |
S = N/A O = 1527 T = TO (out)(err) |
S = N/A O = 1591 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1500_7.wcnf | S = OPT O = 1186 T = 26.75 |
S = OPT O = 1186 T = 877.11 (out)(err) |
S = OPT O = 1186 T = 246.35 (out)(err) |
S = OPT O = 1186 T = 247.85 (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 = 1186 T = 26.75 (out)(err) |
S = OPT O = 1186 T = 28.70 (out)(err) |
S = N/A O = 1486 T = TO (out)(err) |
S = N/A O = 1531 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1500_8.wcnf | S = OPT O = 1217 T = 32.17 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1217 T = 1061.45 (out)(err) |
S = OPT O = 1217 T = 1085.48 (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 = 1217 T = 78.02 (out)(err) |
S = OPT O = 1217 T = 32.17 (out)(err) |
S = N/A O = 1541 T = TO (out)(err) |
S = N/A O = 1501 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1600_1.wcnf | S = OPT O = 1230 T = 15.17 |
S = OPT O = 1230 T = 614.58 (out)(err) |
S = OPT O = 1230 T = 253.75 (out)(err) |
S = OPT O = 1230 T = 247.95 (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 = 1230 T = 26.24 (out)(err) |
S = OPT O = 1230 T = 15.17 (out)(err) |
S = N/A O = 1580 T = TO (out)(err) |
S = N/A O = 1612 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1600_2.wcnf | S = OPT O = 1265 T = 158.75 |
S = N/A O = N/A 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 = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1265 T = 216.32 (out)(err) |
S = OPT O = 1265 T = 158.75 (out)(err) |
S = N/A O = 1566 T = TO (out)(err) |
S = N/A O = 1534 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1600_3.wcnf | S = OPT O = 1309 T = 81.92 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1309 T = 1036.38 (out)(err) |
S = OPT O = 1309 T = 1052.10 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 483.95 (out)(err) |
S = OPT O = 1309 T = 154.44 (out)(err) |
S = OPT O = 1309 T = 81.92 (out)(err) |
S = N/A O = 1624 T = TO (out)(err) |
S = N/A O = 1657 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1600_4.wcnf | S = OPT O = 1267 T = 40.63 |
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 = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1267 T = 181.89 (out)(err) |
S = OPT O = 1267 T = 40.63 (out)(err) |
S = N/A O = 1600 T = TO (out)(err) |
S = N/A O = 1621 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1600_5.wcnf | S = OPT O = 1298 T = 32.10 |
S = OPT O = 1298 T = 853.82 (out)(err) |
S = OPT O = 1298 T = 444.00 (out)(err) |
S = OPT O = 1298 T = 446.52 (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 = 1298 T = 52.19 (out)(err) |
S = OPT O = 1298 T = 32.10 (out)(err) |
S = N/A O = 1604 T = TO (out)(err) |
S = N/A O = 1554 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1600_6.wcnf | S = OPT O = 1190 T = 11.98 |
S = OPT O = 1190 T = 615.65 (out)(err) |
S = OPT O = 1190 T = 298.50 (out)(err) |
S = OPT O = 1190 T = 299.40 (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 = 1190 T = 21.31 (out)(err) |
S = OPT O = 1190 T = 11.98 (out)(err) |
S = N/A O = 1526 T = TO (out)(err) |
S = N/A O = 1588 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1600_7.wcnf | S = OPT O = 1243 T = 72.94 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1243 T = 1505.57 (out)(err) |
S = OPT O = 1243 T = 1646.94 (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 = 1243 T = 131.63 (out)(err) |
S = OPT O = 1243 T = 72.94 (out)(err) |
S = N/A O = 1498 T = TO (out)(err) |
S = N/A O = 1585 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v100c1600_8.wcnf | S = OPT O = 1184 T = 4.31 |
S = OPT O = 1184 T = 331.61 (out)(err) |
S = OPT O = 1184 T = 83.64 (out)(err) |
S = OPT O = 1184 T = 84.69 (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 = 1184 T = 11.52 (out)(err) |
S = OPT O = 1184 T = 4.31 (out)(err) |
S = N/A O = 1531 T = TO (out)(err) |
S = N/A O = 1648 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_1.wcnf | S = OPT O = 840 T = 27.82 |
S = OPT O = 840 T = 292.70 (out)(err) |
S = OPT O = 840 T = 205.01 (out)(err) |
S = OPT O = 840 T = 201.80 (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 = 840 T = 54.72 (out)(err) |
S = OPT O = 840 T = 27.82 (out)(err) |
S = N/A O = 1080 T = TO (out)(err) |
S = N/A O = 1067 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_2.wcnf | S = OPT O = 803 T = 6.39 |
S = OPT O = 803 T = 53.69 (out)(err) |
S = OPT O = 803 T = 19.62 (out)(err) |
S = OPT O = 803 T = 19.49 (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 = 803 T = 7.53 (out)(err) |
S = OPT O = 803 T = 6.39 (out)(err) |
S = N/A O = 1079 T = TO (out)(err) |
S = N/A O = 1067 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1200_3.wcnf | S = OPT O = 834 T = 14.50 |
S = OPT O = 834 T = 168.82 (out)(err) |
S = OPT O = 834 T = 79.94 (out)(err) |
S = OPT O = 834 T = 81.43 (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 = 834 T = 26.68 (out)(err) |
S = OPT O = 834 T = 14.50 (out)(err) |
S = N/A O = 1114 T = TO (out)(err) |
S = N/A O = 1175 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_4.wcnf | S = OPT O = 811 T = 11.81 |
S = OPT O = 811 T = 80.84 (out)(err) |
S = OPT O = 811 T = 40.88 (out)(err) |
S = OPT O = 811 T = 36.01 (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 = 811 T = 19.10 (out)(err) |
S = OPT O = 811 T = 11.81 (out)(err) |
S = N/A O = 1103 T = TO (out)(err) |
S = N/A O = 1078 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1200_5.wcnf | S = OPT O = 850 T = 47.60 |
S = OPT O = 850 T = 312.12 (out)(err) |
S = OPT O = 850 T = 440.37 (out)(err) |
S = OPT O = 850 T = 458.68 (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 = 850 T = 51.86 (out)(err) |
S = OPT O = 850 T = 47.60 (out)(err) |
S = N/A O = 1046 T = TO (out)(err) |
S = N/A O = 1074 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_6.wcnf | S = OPT O = 784 T = 18.03 |
S = OPT O = 784 T = 238.90 (out)(err) |
S = OPT O = 784 T = 249.45 (out)(err) |
S = OPT O = 784 T = 250.63 (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 = 784 T = 63.64 (out)(err) |
S = OPT O = 784 T = 18.03 (out)(err) |
S = N/A O = 1054 T = TO (out)(err) |
S = N/A O = 1047 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_7.wcnf | S = OPT O = 747 T = 3.39 |
S = OPT O = 747 T = 20.63 (out)(err) |
S = OPT O = 747 T = 12.54 (out)(err) |
S = OPT O = 747 T = 12.52 (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 = 747 T = 4.91 (out)(err) |
S = OPT O = 747 T = 3.39 (out)(err) |
S = N/A O = 1018 T = TO (out)(err) |
S = N/A O = 1044 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_8.wcnf | S = OPT O = 813 T = 12.33 |
S = OPT O = 813 T = 112.60 (out)(err) |
S = OPT O = 813 T = 44.29 (out)(err) |
S = OPT O = 813 T = 43.71 (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 = 813 T = 12.33 (out)(err) |
S = OPT O = 813 T = 12.92 (out)(err) |
S = N/A O = 1092 T = TO (out)(err) |
S = N/A O = 1158 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1300_1.wcnf | S = OPT O = 890 T = 10.52 |
S = OPT O = 890 T = 96.41 (out)(err) |
S = OPT O = 890 T = 46.35 (out)(err) |
S = OPT O = 890 T = 45.11 (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 = 890 T = 11.37 (out)(err) |
S = OPT O = 890 T = 10.52 (out)(err) |
S = N/A O = 1099 T = TO (out)(err) |
S = N/A O = 1093 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1300_2.wcnf | S = OPT O = 847 T = 4.20 |
S = OPT O = 847 T = 51.65 (out)(err) |
S = OPT O = 847 T = 40.50 (out)(err) |
S = OPT O = 847 T = 33.58 (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 = 847 T = 9.61 (out)(err) |
S = OPT O = 847 T = 4.20 (out)(err) |
S = N/A O = 1067 T = TO (out)(err) |
S = N/A O = 1132 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_3.wcnf | S = OPT O = 941 T = 12.04 |
S = OPT O = 941 T = 251.40 (out)(err) |
S = OPT O = 941 T = 104.43 (out)(err) |
S = OPT O = 941 T = 103.78 (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 = 941 T = 28.49 (out)(err) |
S = OPT O = 941 T = 12.04 (out)(err) |
S = N/A O = 1257 T = TO (out)(err) |
S = N/A O = 1319 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_4.wcnf | S = OPT O = 939 T = 18.83 |
S = OPT O = 939 T = 301.60 (out)(err) |
S = OPT O = 939 T = 169.54 (out)(err) |
S = OPT O = 939 T = 151.86 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 36.52 (out)(err) |
S = OPT O = 939 T = 29.49 (out)(err) |
S = OPT O = 939 T = 18.83 (out)(err) |
S = N/A O = 1167 T = TO (out)(err) |
S = N/A O = 1227 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1300_5.wcnf | S = OPT O = 949 T = 48.63 |
S = OPT O = 949 T = 1094.05 (out)(err) |
S = OPT O = 949 T = 439.52 (out)(err) |
S = OPT O = 949 T = 419.34 (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 = 949 T = 113.36 (out)(err) |
S = OPT O = 949 T = 48.63 (out)(err) |
S = N/A O = 1248 T = TO (out)(err) |
S = N/A O = 1395 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_6.wcnf | S = OPT O = 865 T = 5.82 |
S = OPT O = 865 T = 159.91 (out)(err) |
S = OPT O = 865 T = 63.79 (out)(err) |
S = OPT O = 865 T = 59.19 (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 = 865 T = 18.15 (out)(err) |
S = OPT O = 865 T = 5.82 (out)(err) |
S = N/A O = 1195 T = TO (out)(err) |
S = N/A O = 1192 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_7.wcnf | S = OPT O = 879 T = 4.97 |
S = OPT O = 879 T = 111.41 (out)(err) |
S = OPT O = 879 T = 34.82 (out)(err) |
S = OPT O = 879 T = 36.07 (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 = 879 T = 10.60 (out)(err) |
S = OPT O = 879 T = 4.97 (out)(err) |
S = N/A O = 1178 T = TO (out)(err) |
S = N/A O = 1168 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1300_8.wcnf | S = OPT O = 868 T = 10.66 |
S = OPT O = 868 T = 115.13 (out)(err) |
S = OPT O = 868 T = 49.36 (out)(err) |
S = OPT O = 868 T = 50.86 (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 = 868 T = 13.04 (out)(err) |
S = OPT O = 868 T = 10.66 (out)(err) |
S = N/A O = 1145 T = TO (out)(err) |
S = N/A O = 1196 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1400_1.wcnf | S = OPT O = 1028 T = 24.14 |
S = OPT O = 1028 T = 281.68 (out)(err) |
S = OPT O = 1028 T = 107.45 (out)(err) |
S = OPT O = 1028 T = 108.82 (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 = 1028 T = 33.79 (out)(err) |
S = OPT O = 1028 T = 24.14 (out)(err) |
S = N/A O = 1348 T = TO (out)(err) |
S = N/A O = 1275 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_2.wcnf | S = OPT O = 1008 T = 36.72 |
S = OPT O = 1008 T = 1175.83 (out)(err) |
S = OPT O = 1008 T = 585.10 (out)(err) |
S = OPT O = 1008 T = 556.84 (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 = 1008 T = 125.54 (out)(err) |
S = OPT O = 1008 T = 36.72 (out)(err) |
S = N/A O = 1353 T = TO (out)(err) |
S = N/A O = 1338 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_3.wcnf | S = OPT O = 983 T = 7.58 |
S = OPT O = 983 T = 114.89 (out)(err) |
S = OPT O = 983 T = 41.39 (out)(err) |
S = OPT O = 983 T = 39.87 (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 = 983 T = 17.54 (out)(err) |
S = OPT O = 983 T = 7.58 (out)(err) |
S = N/A O = 1288 T = TO (out)(err) |
S = N/A O = 1331 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_4.wcnf | S = OPT O = 1007 T = 49.95 |
S = OPT O = 1007 T = 748.98 (out)(err) |
S = OPT O = 1007 T = 286.09 (out)(err) |
S = OPT O = 1007 T = 291.44 (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 = 1007 T = 61.04 (out)(err) |
S = OPT O = 1007 T = 49.95 (out)(err) |
S = N/A O = 1280 T = TO (out)(err) |
S = N/A O = 1200 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_5.wcnf | S = OPT O = 1108 T = 275.60 |
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 = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1108 T = 294.60 (out)(err) |
S = OPT O = 1108 T = 275.60 (out)(err) |
S = N/A O = 1374 T = TO (out)(err) |
S = N/A O = 1475 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_6.wcnf | S = OPT O = 959 T = 11.36 |
S = OPT O = 959 T = 100.25 (out)(err) |
S = OPT O = 959 T = 49.33 (out)(err) |
S = OPT O = 959 T = 50.05 (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 = 959 T = 12.41 (out)(err) |
S = OPT O = 959 T = 11.36 (out)(err) |
S = N/A O = 1237 T = TO (out)(err) |
S = N/A O = 1347 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_7.wcnf | S = OPT O = 1040 T = 54.77 |
S = OPT O = 1040 T = 1190.47 (out)(err) |
S = OPT O = 1040 T = 563.10 (out)(err) |
S = OPT O = 1040 T = 587.93 (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 = 1040 T = 102.21 (out)(err) |
S = OPT O = 1040 T = 54.77 (out)(err) |
S = N/A O = 1271 T = TO (out)(err) |
S = N/A O = 1385 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1400_8.wcnf | S = OPT O = 1025 T = 40.79 |
S = OPT O = 1025 T = 1006.75 (out)(err) |
S = OPT O = 1025 T = 293.74 (out)(err) |
S = OPT O = 1025 T = 287.05 (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 = 1025 T = 50.33 (out)(err) |
S = OPT O = 1025 T = 40.79 (out)(err) |
S = N/A O = 1364 T = TO (out)(err) |
S = N/A O = 1390 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_1.wcnf | S = OPT O = 1119 T = 46.94 |
S = OPT O = 1119 T = 1163.22 (out)(err) |
S = OPT O = 1119 T = 304.20 (out)(err) |
S = OPT O = 1119 T = 302.63 (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 = 1119 T = 172.16 (out)(err) |
S = OPT O = 1119 T = 46.94 (out)(err) |
S = N/A O = 1439 T = TO (out)(err) |
S = N/A O = 1501 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_2.wcnf | S = OPT O = 1136 T = 58.28 |
S = OPT O = 1136 T = 1383.96 (out)(err) |
S = OPT O = 1136 T = 423.33 (out)(err) |
S = OPT O = 1136 T = 443.63 (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 = 1136 T = 184.56 (out)(err) |
S = OPT O = 1136 T = 58.28 (out)(err) |
S = N/A O = 1492 T = TO (out)(err) |
S = N/A O = 1515 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_3.wcnf | S = OPT O = 1062 T = 12.97 |
S = OPT O = 1062 T = 366.52 (out)(err) |
S = OPT O = 1062 T = 58.81 (out)(err) |
S = OPT O = 1062 T = 59.55 (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 = 1062 T = 21.03 (out)(err) |
S = OPT O = 1062 T = 12.97 (out)(err) |
S = N/A O = 1443 T = TO (out)(err) |
S = N/A O = 1329 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_4.wcnf | S = OPT O = 1041 T = 6.31 |
S = OPT O = 1041 T = 141.79 (out)(err) |
S = OPT O = 1041 T = 41.53 (out)(err) |
S = OPT O = 1041 T = 48.07 (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 = 1041 T = 9.69 (out)(err) |
S = OPT O = 1041 T = 6.31 (out)(err) |
S = N/A O = 1425 T = TO (out)(err) |
S = N/A O = 1495 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_5.wcnf | S = OPT O = 1125 T = 9.05 |
S = OPT O = 1125 T = 374.24 (out)(err) |
S = OPT O = 1125 T = 117.76 (out)(err) |
S = OPT O = 1125 T = 118.90 (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 = 1125 T = 29.02 (out)(err) |
S = OPT O = 1125 T = 9.05 (out)(err) |
S = N/A O = 1515 T = TO (out)(err) |
S = N/A O = 1535 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_6.wcnf | S = OPT O = 1113 T = 41.15 |
S = OPT O = 1113 T = 566.89 (out)(err) |
S = OPT O = 1113 T = 244.78 (out)(err) |
S = OPT O = 1113 T = 369.88 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 147.15 (out)(err) |
S = OPT O = 1113 T = 74.06 (out)(err) |
S = OPT O = 1113 T = 41.15 (out)(err) |
S = N/A O = 1448 T = TO (out)(err) |
S = N/A O = 1488 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_7.wcnf | S = OPT O = 1163 T = 110.64 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1163 T = 815.35 (out)(err) |
S = OPT O = 1163 T = 864.81 (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 = 1163 T = 148.05 (out)(err) |
S = OPT O = 1163 T = 110.64 (out)(err) |
S = N/A O = 1460 T = TO (out)(err) |
S = N/A O = 1501 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_8.wcnf | S = OPT O = 1097 T = 7.81 |
S = OPT O = 1097 T = 285.32 (out)(err) |
S = OPT O = 1097 T = 115.97 (out)(err) |
S = OPT O = 1097 T = 110.05 (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 = 1097 T = 18.31 (out)(err) |
S = OPT O = 1097 T = 7.81 (out)(err) |
S = N/A O = 1468 T = TO (out)(err) |
S = N/A O = 1446 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1600_1.wcnf | S = OPT O = 1190 T = 14.24 |
S = OPT O = 1190 T = 575.33 (out)(err) |
S = OPT O = 1190 T = 156.63 (out)(err) |
S = OPT O = 1190 T = 162.31 (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 = 1190 T = 15.64 (out)(err) |
S = OPT O = 1190 T = 14.24 (out)(err) |
S = N/A O = 1560 T = TO (out)(err) |
S = N/A O = 1544 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1600_2.wcnf | S = OPT O = 1227 T = 98.31 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1227 T = 860.57 (out)(err) |
S = OPT O = 1227 T = 893.80 (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 = 1227 T = 144.41 (out)(err) |
S = OPT O = 1227 T = 98.31 (out)(err) |
S = N/A O = 1556 T = TO (out)(err) |
S = N/A O = 1666 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1600_3.wcnf | S = OPT O = 1224 T = 73.31 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1224 T = 936.29 (out)(err) |
S = OPT O = 1224 T = 947.66 (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 = 1224 T = 111.75 (out)(err) |
S = OPT O = 1224 T = 73.31 (out)(err) |
S = N/A O = 1569 T = TO (out)(err) |
S = N/A O = 1615 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1600_4.wcnf | S = OPT O = 1264 T = 185.70 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1264 T = 1756.92 (out)(err) |
S = OPT O = 1264 T = 1777.84 (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 = 1264 T = 291.02 (out)(err) |
S = OPT O = 1264 T = 185.70 (out)(err) |
S = N/A O = 1628 T = TO (out)(err) |
S = N/A O = 1580 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1600_5.wcnf | S = OPT O = 1252 T = 78.07 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1252 T = 1130.52 (out)(err) |
S = OPT O = 1252 T = 1150.80 (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 = 1252 T = 123.30 (out)(err) |
S = OPT O = 1252 T = 78.07 (out)(err) |
S = N/A O = 1553 T = TO (out)(err) |
S = N/A O = 1505 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1600_6.wcnf | S = OPT O = 1246 T = 29.95 |
S = OPT O = 1246 T = 1286.75 (out)(err) |
S = OPT O = 1246 T = 554.64 (out)(err) |
S = OPT O = 1246 T = 577.40 (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 = 1246 T = 51.18 (out)(err) |
S = OPT O = 1246 T = 29.95 (out)(err) |
S = N/A O = 1582 T = TO (out)(err) |
S = N/A O = 1592 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1600_7.wcnf | S = OPT O = 1159 T = 12.86 |
S = OPT O = 1159 T = 270.30 (out)(err) |
S = OPT O = 1159 T = 74.22 (out)(err) |
S = OPT O = 1159 T = 73.08 (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 = 1159 T = 13.90 (out)(err) |
S = OPT O = 1159 T = 12.86 (out)(err) |
S = N/A O = 1407 T = TO (out)(err) |
S = N/A O = 1588 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v120c1600_8.wcnf | S = OPT O = 1150 T = 5.66 |
S = OPT O = 1150 T = 613.99 (out)(err) |
S = OPT O = 1150 T = 159.17 (out)(err) |
S = OPT O = 1150 T = 164.78 (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 = 1150 T = 22.39 (out)(err) |
S = OPT O = 1150 T = 5.66 (out)(err) |
S = N/A O = 1533 T = TO (out)(err) |
S = N/A O = 1566 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1200_1.wcnf | S = OPT O = 780 T = 65.48 |
S = OPT O = 780 T = 489.04 (out)(err) |
S = OPT O = 780 T = 284.41 (out)(err) |
S = OPT O = 780 T = 306.75 (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 = 780 T = 108.92 (out)(err) |
S = OPT O = 780 T = 65.48 (out)(err) |
S = N/A O = 1000 T = TO (out)(err) |
S = N/A O = 1037 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1200_2.wcnf | S = OPT O = 733 T = 24.38 |
S = OPT O = 733 T = 242.45 (out)(err) |
S = OPT O = 733 T = 119.58 (out)(err) |
S = OPT O = 733 T = 124.70 (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 = 733 T = 37.37 (out)(err) |
S = OPT O = 733 T = 24.38 (out)(err) |
S = N/A O = 1007 T = TO (out)(err) |
S = N/A O = 1106 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1200_3.wcnf | S = OPT O = 741 T = 30.26 |
S = OPT O = 741 T = 223.56 (out)(err) |
S = OPT O = 741 T = 215.32 (out)(err) |
S = OPT O = 741 T = 209.43 (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 = 741 T = 84.40 (out)(err) |
S = OPT O = 741 T = 30.26 (out)(err) |
S = N/A O = 970 T = TO (out)(err) |
S = N/A O = 973 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1200_4.wcnf | S = OPT O = 667 T = 2.98 |
S = OPT O = 667 T = 31.35 (out)(err) |
S = OPT O = 667 T = 15.17 (out)(err) |
S = OPT O = 667 T = 14.56 (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 = 667 T = 3.67 (out)(err) |
S = OPT O = 667 T = 2.98 (out)(err) |
S = N/A O = 1012 T = TO (out)(err) |
S = N/A O = 1095 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1200_5.wcnf | S = OPT O = 714 T = 12.08 |
S = OPT O = 714 T = 56.65 (out)(err) |
S = OPT O = 714 T = 63.56 (out)(err) |
S = OPT O = 714 T = 46.94 (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 = 714 T = 21.88 (out)(err) |
S = OPT O = 714 T = 12.08 (out)(err) |
S = N/A O = 974 T = TO (out)(err) |
S = N/A O = 995 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1200_6.wcnf | S = OPT O = 803 T = 119.00 |
S = OPT O = 803 T = 648.44 (out)(err) |
S = OPT O = 803 T = 459.78 (out)(err) |
S = OPT O = 803 T = 469.11 (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 = 803 T = 132.91 (out)(err) |
S = OPT O = 803 T = 119.00 (out)(err) |
S = N/A O = 1100 T = TO (out)(err) |
S = N/A O = 1166 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1200_7.wcnf | S = OPT O = 774 T = 167.24 |
S = OPT O = 774 T = 845.68 (out)(err) |
S = OPT O = 774 T = 458.18 (out)(err) |
S = OPT O = 774 T = 463.38 (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 = 774 T = 212.59 (out)(err) |
S = OPT O = 774 T = 167.24 (out)(err) |
S = N/A O = 1049 T = TO (out)(err) |
S = N/A O = 991 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1200_8.wcnf | S = OPT O = 745 T = 52.87 |
S = OPT O = 745 T = 402.55 (out)(err) |
S = OPT O = 745 T = 223.73 (out)(err) |
S = OPT O = 745 T = 220.93 (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 = 745 T = 106.45 (out)(err) |
S = OPT O = 745 T = 52.87 (out)(err) |
S = N/A O = 976 T = TO (out)(err) |
S = N/A O = 970 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1300_1.wcnf | S = OPT O = 846 T = 46.02 |
S = OPT O = 846 T = 441.81 (out)(err) |
S = OPT O = 846 T = 189.89 (out)(err) |
S = OPT O = 846 T = 192.94 (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 = 846 T = 59.55 (out)(err) |
S = OPT O = 846 T = 46.02 (out)(err) |
S = N/A O = 1121 T = TO (out)(err) |
S = N/A O = 1131 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1300_2.wcnf | S = OPT O = 774 T = 3.91 |
S = OPT O = 774 T = 51.23 (out)(err) |
S = OPT O = 774 T = 26.80 (out)(err) |
S = OPT O = 774 T = 28.92 (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 = 774 T = 7.65 (out)(err) |
S = OPT O = 774 T = 3.91 (out)(err) |
S = N/A O = 1132 T = TO (out)(err) |
S = N/A O = 1096 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1300_3.wcnf | S = OPT O = 832 T = 38.91 |
S = OPT O = 832 T = 515.54 (out)(err) |
S = OPT O = 832 T = 317.19 (out)(err) |
S = OPT O = 832 T = 333.85 (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 = 832 T = 54.71 (out)(err) |
S = OPT O = 832 T = 38.91 (out)(err) |
S = N/A O = 1041 T = TO (out)(err) |
S = N/A O = 1034 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1300_4.wcnf | S = OPT O = 871 T = 192.03 |
S = OPT O = 871 T = 1505.76 (out)(err) |
S = OPT O = 871 T = 669.78 (out)(err) |
S = OPT O = 871 T = 677.55 (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 = 871 T = 292.61 (out)(err) |
S = OPT O = 871 T = 192.03 (out)(err) |
S = N/A O = 1191 T = TO (out)(err) |
S = N/A O = 1129 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1300_5.wcnf | S = OPT O = 844 T = 55.60 |
S = OPT O = 844 T = 533.46 (out)(err) |
S = OPT O = 844 T = 222.34 (out)(err) |
S = OPT O = 844 T = 220.98 (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 = 844 T = 62.32 (out)(err) |
S = OPT O = 844 T = 55.60 (out)(err) |
S = N/A O = 1141 T = TO (out)(err) |
S = N/A O = 1217 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1300_6.wcnf | S = OPT O = 884 T = 338.55 |
S = N/A O = 884 T = TO (out)(err) |
S = OPT O = 884 T = 1544.42 (out)(err) |
S = OPT O = 884 T = 1535.57 (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 = 884 T = 493.90 (out)(err) |
S = OPT O = 884 T = 338.55 (out)(err) |
S = N/A O = 1207 T = TO (out)(err) |
S = N/A O = 1211 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1300_7.wcnf | S = OPT O = 874 T = 100.10 |
S = OPT O = 874 T = 909.89 (out)(err) |
S = OPT O = 874 T = 432.49 (out)(err) |
S = OPT O = 874 T = 428.74 (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 = 874 T = 182.12 (out)(err) |
S = OPT O = 874 T = 100.10 (out)(err) |
S = N/A O = 1088 T = TO (out)(err) |
S = N/A O = 1097 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1300_8.wcnf | S = OPT O = 812 T = 81.21 |
S = OPT O = 812 T = 681.05 (out)(err) |
S = OPT O = 812 T = 350.15 (out)(err) |
S = OPT O = 812 T = 345.68 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 475.12 (out)(err) |
S = OPT O = 812 T = 104.18 (out)(err) |
S = OPT O = 812 T = 81.21 (out)(err) |
S = N/A O = 1046 T = TO (out)(err) |
S = N/A O = 1035 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_1.wcnf | S = OPT O = 926 T = 107.34 |
S = OPT O = 926 T = 1164.47 (out)(err) |
S = OPT O = 926 T = 621.50 (out)(err) |
S = OPT O = 926 T = 649.00 (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 = 926 T = 116.53 (out)(err) |
S = OPT O = 926 T = 107.34 (out)(err) |
S = N/A O = 1240 T = TO (out)(err) |
S = N/A O = 1274 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_2.wcnf | S = OPT O = 879 T = 34.37 |
S = OPT O = 879 T = 283.52 (out)(err) |
S = OPT O = 879 T = 110.61 (out)(err) |
S = OPT O = 879 T = 113.16 (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 = 879 T = 40.38 (out)(err) |
S = OPT O = 879 T = 34.37 (out)(err) |
S = N/A O = 1190 T = TO (out)(err) |
S = N/A O = 1152 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_3.wcnf | S = OPT O = 936 T = 92.49 |
S = OPT O = 936 T = 944.21 (out)(err) |
S = OPT O = 936 T = 368.30 (out)(err) |
S = OPT O = 936 T = 373.16 (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 = 936 T = 101.71 (out)(err) |
S = OPT O = 936 T = 92.49 (out)(err) |
S = N/A O = 1267 T = TO (out)(err) |
S = N/A O = 1223 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_4.wcnf | S = OPT O = 932 T = 37.45 |
S = OPT O = 932 T = 799.29 (out)(err) |
S = OPT O = 932 T = 244.01 (out)(err) |
S = OPT O = 932 T = 239.56 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 15.46 (out)(err) |
S = OPT O = 932 T = 97.81 (out)(err) |
S = OPT O = 932 T = 37.45 (out)(err) |
S = N/A O = 1223 T = TO (out)(err) |
S = N/A O = 1286 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_5.wcnf | S = OPT O = 968 T = 101.75 |
S = OPT O = 968 T = 1698.44 (out)(err) |
S = OPT O = 968 T = 797.19 (out)(err) |
S = OPT O = 968 T = 778.27 (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 = 968 T = 197.49 (out)(err) |
S = OPT O = 968 T = 101.75 (out)(err) |
S = N/A O = 1330 T = TO (out)(err) |
S = N/A O = 1465 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_6.wcnf | S = OPT O = 967 T = 365.93 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 967 T = 1439.34 (out)(err) |
S = OPT O = 967 T = 1582.11 (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 = 967 T = 461.32 (out)(err) |
S = OPT O = 967 T = 365.93 (out)(err) |
S = N/A O = 1317 T = TO (out)(err) |
S = N/A O = 1291 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1400_7.wcnf | S = OPT O = 923 T = 28.57 |
S = OPT O = 923 T = 368.67 (out)(err) |
S = OPT O = 923 T = 160.00 (out)(err) |
S = OPT O = 923 T = 153.21 (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 = 923 T = 73.55 (out)(err) |
S = OPT O = 923 T = 28.57 (out)(err) |
S = N/A O = 1259 T = TO (out)(err) |
S = N/A O = 1259 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_8.wcnf | S = OPT O = 957 T = 154.92 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 957 T = 1482.34 (out)(err) |
S = OPT O = 957 T = 1312.96 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 1.33 (out)(err) |
S = OPT O = 957 T = 324.06 (out)(err) |
S = OPT O = 957 T = 154.92 (out)(err) |
S = N/A O = 1272 T = TO (out)(err) |
S = N/A O = 1214 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1500_1.wcnf | S = OPT O = 986 T = 60.19 |
S = OPT O = 986 T = 1063.46 (out)(err) |
S = OPT O = 986 T = 343.12 (out)(err) |
S = OPT O = 986 T = 337.98 (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 = 986 T = 149.80 (out)(err) |
S = OPT O = 986 T = 60.19 (out)(err) |
S = N/A O = 1360 T = TO (out)(err) |
S = N/A O = 1328 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1500_2.wcnf | S = OPT O = 998 T = 70.97 |
S = OPT O = 998 T = 1674.93 (out)(err) |
S = OPT O = 998 T = 473.40 (out)(err) |
S = OPT O = 998 T = 489.77 (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 = 998 T = 141.95 (out)(err) |
S = OPT O = 998 T = 70.97 (out)(err) |
S = N/A O = 1368 T = TO (out)(err) |
S = N/A O = 1388 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1500_3.wcnf | S = OPT O = 1073 T = 335.10 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1073 T = 1746.93 (out)(err) |
S = OPT O = 1073 T = 1739.39 (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 = 1073 T = 480.00 (out)(err) |
S = OPT O = 1073 T = 335.10 (out)(err) |
S = N/A O = 1438 T = TO (out)(err) |
S = N/A O = 1367 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1500_4.wcnf | S = OPT O = 1047 T = 341.32 |
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 = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1047 T = 691.87 (out)(err) |
S = OPT O = 1047 T = 341.32 (out)(err) |
S = N/A O = 1429 T = TO (out)(err) |
S = N/A O = 1346 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1500_5.wcnf | S = OPT O = 1058 T = 185.65 |
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 = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1058 T = 622.37 (out)(err) |
S = OPT O = 1058 T = 185.65 (out)(err) |
S = N/A O = 1347 T = TO (out)(err) |
S = N/A O = 1356 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1500_6.wcnf | S = OPT O = 1102 T = 649.53 |
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 = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1102 T = 662.79 (out)(err) |
S = OPT O = 1102 T = 649.53 (out)(err) |
S = N/A O = 1485 T = TO (out)(err) |
S = N/A O = 1427 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1500_7.wcnf | S = OPT O = 1010 T = 35.22 |
S = OPT O = 1010 T = 698.45 (out)(err) |
S = OPT O = 1010 T = 247.50 (out)(err) |
S = OPT O = 1010 T = 251.57 (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 = 1010 T = 51.62 (out)(err) |
S = OPT O = 1010 T = 35.22 (out)(err) |
S = N/A O = 1339 T = TO (out)(err) |
S = N/A O = 1393 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1500_8.wcnf | S = OPT O = 1045 T = 113.40 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1045 T = 649.58 (out)(err) |
S = OPT O = 1045 T = 647.05 (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 = 1045 T = 202.36 (out)(err) |
S = OPT O = 1045 T = 113.40 (out)(err) |
S = N/A O = 1380 T = TO (out)(err) |
S = N/A O = 1462 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1600_1.wcnf | S = OPT O = 1143 T = 71.27 |
S = OPT O = 1143 T = 1761.80 (out)(err) |
S = OPT O = 1143 T = 406.60 (out)(err) |
S = OPT O = 1143 T = 415.79 (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 = 1143 T = 105.95 (out)(err) |
S = OPT O = 1143 T = 71.27 (out)(err) |
S = N/A O = 1465 T = TO (out)(err) |
S = N/A O = 1512 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1600_2.wcnf | S = OPT O = 1140 T = 62.09 |
S = OPT O = 1140 T = 1237.29 (out)(err) |
S = OPT O = 1140 T = 439.04 (out)(err) |
S = OPT O = 1140 T = 437.76 (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 = 1140 T = 86.00 (out)(err) |
S = OPT O = 1140 T = 62.09 (out)(err) |
S = N/A O = 1386 T = TO (out)(err) |
S = N/A O = 1438 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1600_3.wcnf | S = OPT O = 1079 T = 63.97 |
S = OPT O = 1079 T = 855.93 (out)(err) |
S = OPT O = 1079 T = 281.24 (out)(err) |
S = OPT O = 1079 T = 280.50 (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 = 1079 T = 63.97 (out)(err) |
S = OPT O = 1079 T = 64.28 (out)(err) |
S = N/A O = 1422 T = TO (out)(err) |
S = N/A O = 1355 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1600_4.wcnf | S = OPT O = 1157 T = 193.61 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1157 T = 1184.59 (out)(err) |
S = OPT O = 1157 T = 1196.71 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 315.46 (out)(err) |
S = OPT O = 1157 T = 193.61 (out)(err) |
S = OPT O = 1157 T = 207.13 (out)(err) |
S = N/A O = 1459 T = TO (out)(err) |
S = N/A O = 1592 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1600_5.wcnf | S = OPT O = 1119 T = 179.39 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1119 T = 1556.86 (out)(err) |
S = OPT O = 1119 T = 1576.58 (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 = 1119 T = 314.55 (out)(err) |
S = OPT O = 1119 T = 179.39 (out)(err) |
S = N/A O = 1498 T = TO (out)(err) |
S = N/A O = 1557 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1600_6.wcnf | S = OPT O = 1212 T = 420.40 |
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 = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1212 T = 517.88 (out)(err) |
S = OPT O = 1212 T = 420.40 (out)(err) |
S = N/A O = 1603 T = TO (out)(err) |
S = N/A O = 1617 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
s2v140c1600_7.wcnf | S = OPT O = 1150 T = 174.84 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1150 T = 1581.40 (out)(err) |
S = OPT O = 1150 T = 1726.38 (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 = 1150 T = 320.70 (out)(err) |
S = OPT O = 1150 T = 174.84 (out)(err) |
S = N/A O = 1530 T = TO (out)(err) |
S = N/A O = 1698 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1600_8.wcnf | S = OPT O = 1180 T = 158.15 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1180 T = 998.55 (out)(err) |
S = OPT O = 1180 T = 995.18 (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 = 1180 T = 201.93 (out)(err) |
S = OPT O = 1180 T = 158.15 (out)(err) |
S = N/A O = 1560 T = TO (out)(err) |
S = N/A O = 1481 T = TO (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 = 170.09 |
S = OPT O = 198 T = 488.37 (out)(err) |
S = OPT O = 198 T = 731.66 (out)(err) |
S = OPT O = 198 T = 737.02 (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 = 198 T = 248.71 (out)(err) |
S = OPT O = 198 T = 170.09 (out)(err) |
S = N/A O = 310 T = TO (out)(err) |
S = N/A O = 326 T = TO (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 = 134.12 |
S = OPT O = 212 T = 261.45 (out)(err) |
S = OPT O = 212 T = 396.94 (out)(err) |
S = OPT O = 212 T = 398.61 (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 = 212 T = 164.77 (out)(err) |
S = OPT O = 212 T = 134.12 (out)(err) |
S = N/A O = 293 T = TO (out)(err) |
S = N/A O = 326 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C1000_2.wcnf | S = OPT O = 211 T = 208.37 |
S = OPT O = 211 T = 380.31 (out)(err) |
S = OPT O = 211 T = 583.94 (out)(err) |
S = OPT O = 211 T = 584.36 (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 = 211 T = 224.84 (out)(err) |
S = OPT O = 211 T = 208.37 (out)(err) |
S = N/A O = 300 T = TO (out)(err) |
S = N/A O = 262 T = TO (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 = 278.75 |
S = OPT O = 229 T = 530.11 (out)(err) |
S = OPT O = 229 T = 803.58 (out)(err) |
S = OPT O = 229 T = 812.88 (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 = 229 T = 311.39 (out)(err) |
S = OPT O = 229 T = 278.75 (out)(err) |
S = N/A O = 331 T = TO (out)(err) |
S = N/A O = 286 T = TO (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 = 147.43 |
S = OPT O = 202 T = 334.34 (out)(err) |
S = OPT O = 202 T = 506.71 (out)(err) |
S = OPT O = 202 T = 511.21 (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 = 202 T = 201.48 (out)(err) |
S = OPT O = 202 T = 147.43 (out)(err) |
S = N/A O = 269 T = TO (out)(err) |
S = N/A O = 269 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C1000_5.wcnf | S = OPT O = 214 T = 158.44 |
S = OPT O = 214 T = 637.65 (out)(err) |
S = OPT O = 214 T = 936.17 (out)(err) |
S = OPT O = 214 T = 938.95 (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 = 214 T = 387.25 (out)(err) |
S = OPT O = 214 T = 158.44 (out)(err) |
S = N/A O = 285 T = TO (out)(err) |
S = N/A O = 253 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C1000_6.wcnf | S = OPT O = 203 T = 107.05 |
S = OPT O = 203 T = 159.49 (out)(err) |
S = OPT O = 203 T = 246.40 (out)(err) |
S = OPT O = 203 T = 247.75 (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 = 203 T = 107.36 (out)(err) |
S = OPT O = 203 T = 107.05 (out)(err) |
S = N/A O = 275 T = TO (out)(err) |
S = N/A O = 294 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C1000_7.wcnf | S = OPT O = 200 T = 92.48 |
S = OPT O = 200 T = 168.07 (out)(err) |
S = OPT O = 200 T = 260.62 (out)(err) |
S = OPT O = 200 T = 261.63 (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 = 200 T = 148.97 (out)(err) |
S = OPT O = 200 T = 92.48 (out)(err) |
S = N/A O = 214 T = TO (out)(err) |
S = N/A O = 218 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C1000_8.wcnf | S = OPT O = 188 T = 51.78 |
S = OPT O = 188 T = 263.48 (out)(err) |
S = OPT O = 188 T = 379.37 (out)(err) |
S = OPT O = 188 T = 381.23 (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 = 188 T = 140.94 (out)(err) |
S = OPT O = 188 T = 51.78 (out)(err) |
S = N/A O = 282 T = TO (out)(err) |
S = N/A O = 282 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C1000_9.wcnf | S = OPT O = 226 T = 287.84 |
S = OPT O = 226 T = 525.10 (out)(err) |
S = OPT O = 226 T = 768.05 (out)(err) |
S = OPT O = 226 T = 774.67 (out)(err) |
S = N/A O = N/A T = 339.09 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 226 T = 287.84 (out)(err) |
S = OPT O = 226 T = 288.62 (out)(err) |
S = N/A O = 283 T = TO (out)(err) |
S = N/A O = 263 T = TO (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.65 |
S = OPT O = 103 T = 52.38 (out)(err) |
S = OPT O = 103 T = 90.28 (out)(err) |
S = OPT O = 103 T = 89.30 (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 = 103 T = 42.92 (out)(err) |
S = OPT O = 103 T = 32.65 (out)(err) |
S = N/A O = 125 T = TO (out)(err) |
S = N/A O = 125 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C700_1.wcnf | S = OPT O = 107 T = 19.88 |
S = OPT O = 107 T = 27.32 (out)(err) |
S = OPT O = 107 T = 47.63 (out)(err) |
S = OPT O = 107 T = 47.43 (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 = 107 T = 25.52 (out)(err) |
S = OPT O = 107 T = 19.88 (out)(err) |
S = N/A O = 150 T = TO (out)(err) |
S = N/A O = 156 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C700_2.wcnf | S = OPT O = 110 T = 32.76 |
S = OPT O = 110 T = 42.12 (out)(err) |
S = OPT O = 110 T = 74.77 (out)(err) |
S = OPT O = 110 T = 74.33 (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 = 110 T = 32.76 (out)(err) |
S = OPT O = 110 T = 32.77 (out)(err) |
S = N/A O = 129 T = TO (out)(err) |
S = N/A O = 129 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C700_3.wcnf | S = OPT O = 102 T = 12.76 |
S = OPT O = 102 T = 14.34 (out)(err) |
S = OPT O = 102 T = 24.97 (out)(err) |
S = OPT O = 102 T = 24.85 (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 = 102 T = 14.46 (out)(err) |
S = OPT O = 102 T = 12.76 (out)(err) |
S = N/A O = 123 T = TO (out)(err) |
S = N/A O = 119 T = TO (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.61 |
S = OPT O = 110 T = 49.69 (out)(err) |
S = OPT O = 110 T = 86.56 (out)(err) |
S = OPT O = 110 T = 86.58 (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 = 110 T = 42.24 (out)(err) |
S = OPT O = 110 T = 26.61 (out)(err) |
S = N/A O = 137 T = TO (out)(err) |
S = N/A O = 152 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C700_5.wcnf | S = OPT O = 103 T = 15.55 |
S = OPT O = 103 T = 33.00 (out)(err) |
S = OPT O = 103 T = 55.93 (out)(err) |
S = OPT O = 103 T = 55.73 (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 = 103 T = 31.32 (out)(err) |
S = OPT O = 103 T = 15.55 (out)(err) |
S = N/A O = 126 T = TO (out)(err) |
S = N/A O = 172 T = TO (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 = 16.21 |
S = OPT O = 102 T = 23.71 (out)(err) |
S = OPT O = 102 T = 41.30 (out)(err) |
S = OPT O = 102 T = 41.29 (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 = 102 T = 19.96 (out)(err) |
S = OPT O = 102 T = 16.21 (out)(err) |
S = N/A O = 132 T = TO (out)(err) |
S = N/A O = 132 T = TO (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.94 |
S = OPT O = 104 T = 26.07 (out)(err) |
S = OPT O = 104 T = 44.32 (out)(err) |
S = OPT O = 104 T = 44.12 (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 = 104 T = 22.46 (out)(err) |
S = OPT O = 104 T = 20.94 (out)(err) |
S = N/A O = 141 T = TO (out)(err) |
S = N/A O = 152 T = TO (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.71 |
S = OPT O = 82 T = 3.71 (out)(err) |
S = OPT O = 82 T = 6.90 (out)(err) |
S = OPT O = 82 T = 6.88 (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 = 82 T = 3.94 (out)(err) |
S = OPT O = 82 T = 3.88 (out)(err) |
S = N/A O = 102 T = TO (out)(err) |
S = N/A O = 115 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C700_9.wcnf | S = OPT O = 104 T = 20.11 |
S = OPT O = 104 T = 29.25 (out)(err) |
S = OPT O = 104 T = 49.82 (out)(err) |
S = OPT O = 104 T = 49.74 (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 = 104 T = 21.25 (out)(err) |
S = OPT O = 104 T = 20.11 (out)(err) |
S = N/A O = 119 T = TO (out)(err) |
S = N/A O = 118 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C800_0.wcnf | S = OPT O = 132 T = 36.78 |
S = OPT O = 132 T = 70.62 (out)(err) |
S = OPT O = 132 T = 114.36 (out)(err) |
S = OPT O = 132 T = 114.90 (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 = 132 T = 49.13 (out)(err) |
S = OPT O = 132 T = 36.78 (out)(err) |
S = N/A O = 165 T = TO (out)(err) |
S = N/A O = 165 T = TO (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.67 |
S = OPT O = 138 T = 122.60 (out)(err) |
S = OPT O = 138 T = 179.81 (out)(err) |
S = OPT O = 138 T = 179.90 (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 = 138 T = 72.39 (out)(err) |
S = OPT O = 138 T = 44.67 (out)(err) |
S = N/A O = 180 T = TO (out)(err) |
S = N/A O = 157 T = TO (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.56 |
S = OPT O = 127 T = 65.95 (out)(err) |
S = OPT O = 127 T = 107.35 (out)(err) |
S = OPT O = 127 T = 107.61 (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 = 127 T = 48.59 (out)(err) |
S = OPT O = 127 T = 23.56 (out)(err) |
S = N/A O = 185 T = TO (out)(err) |
S = N/A O = 170 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C800_3.wcnf | S = OPT O = 134 T = 13.40 |
S = OPT O = 134 T = 45.51 (out)(err) |
S = OPT O = 134 T = 68.72 (out)(err) |
S = OPT O = 134 T = 68.67 (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 = 134 T = 21.86 (out)(err) |
S = OPT O = 134 T = 13.40 (out)(err) |
S = N/A O = 223 T = TO (out)(err) |
S = N/A O = 223 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C800_4.wcnf | S = OPT O = 143 T = 44.94 |
S = OPT O = 143 T = 164.09 (out)(err) |
S = OPT O = 143 T = 255.19 (out)(err) |
S = OPT O = 143 T = 255.90 (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 = 143 T = 153.59 (out)(err) |
S = OPT O = 143 T = 44.94 (out)(err) |
S = N/A O = 200 T = TO (out)(err) |
S = N/A O = 167 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C800_5.wcnf | S = OPT O = 144 T = 75.48 |
S = OPT O = 144 T = 182.68 (out)(err) |
S = OPT O = 144 T = 281.68 (out)(err) |
S = OPT O = 144 T = 280.77 (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 = 144 T = 117.65 (out)(err) |
S = OPT O = 144 T = 75.48 (out)(err) |
S = N/A O = 211 T = TO (out)(err) |
S = N/A O = 155 T = TO (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.29 |
S = OPT O = 135 T = 77.84 (out)(err) |
S = OPT O = 135 T = 123.80 (out)(err) |
S = OPT O = 135 T = 123.83 (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 = 135 T = 62.29 (out)(err) |
S = OPT O = 135 T = 41.29 (out)(err) |
S = N/A O = 163 T = TO (out)(err) |
S = N/A O = 174 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C800_7.wcnf | S = OPT O = 147 T = 44.39 |
S = OPT O = 147 T = 133.28 (out)(err) |
S = OPT O = 147 T = 201.78 (out)(err) |
S = OPT O = 147 T = 205.55 (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 = 147 T = 62.02 (out)(err) |
S = OPT O = 147 T = 44.39 (out)(err) |
S = N/A O = 212 T = TO (out)(err) |
S = N/A O = 202 T = TO (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.71 |
S = OPT O = 126 T = 89.09 (out)(err) |
S = OPT O = 126 T = 134.33 (out)(err) |
S = OPT O = 126 T = 135.13 (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 = 126 T = 60.61 (out)(err) |
S = OPT O = 126 T = 22.71 (out)(err) |
S = N/A O = 206 T = TO (out)(err) |
S = N/A O = 169 T = TO (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.22 |
S = OPT O = 138 T = 78.84 (out)(err) |
S = OPT O = 138 T = 120.59 (out)(err) |
S = OPT O = 138 T = 121.02 (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 = 138 T = 57.64 (out)(err) |
S = OPT O = 138 T = 34.22 (out)(err) |
S = N/A O = 165 T = TO (out)(err) |
S = N/A O = 215 T = TO (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 = 52.85 |
S = OPT O = 157 T = 79.37 (out)(err) |
S = OPT O = 157 T = 127.14 (out)(err) |
S = OPT O = 157 T = 128.11 (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 = 157 T = 53.58 (out)(err) |
S = OPT O = 157 T = 52.85 (out)(err) |
S = N/A O = 212 T = TO (out)(err) |
S = N/A O = 209 T = TO (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 = 179.79 |
S = OPT O = 192 T = 298.27 (out)(err) |
S = OPT O = 192 T = 442.39 (out)(err) |
S = OPT O = 192 T = 445.88 (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 = 192 T = 216.52 (out)(err) |
S = OPT O = 192 T = 179.79 (out)(err) |
S = N/A O = 256 T = TO (out)(err) |
S = N/A O = 224 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C900_2.wcnf | S = OPT O = 177 T = 127.21 |
S = OPT O = 177 T = 244.02 (out)(err) |
S = OPT O = 177 T = 370.70 (out)(err) |
S = OPT O = 177 T = 373.01 (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 = 177 T = 157.23 (out)(err) |
S = OPT O = 177 T = 127.21 (out)(err) |
S = N/A O = 208 T = TO (out)(err) |
S = N/A O = 208 T = TO (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 = 58.30 |
S = OPT O = 163 T = 152.12 (out)(err) |
S = OPT O = 163 T = 239.12 (out)(err) |
S = OPT O = 163 T = 239.07 (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 = 163 T = 85.41 (out)(err) |
S = OPT O = 163 T = 58.30 (out)(err) |
S = N/A O = 171 T = TO (out)(err) |
S = N/A O = 225 T = TO (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 = 104.65 |
S = OPT O = 171 T = 211.93 (out)(err) |
S = OPT O = 171 T = 319.38 (out)(err) |
S = OPT O = 171 T = 321.97 (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 = 171 T = 135.70 (out)(err) |
S = OPT O = 171 T = 104.65 (out)(err) |
S = N/A O = 229 T = TO (out)(err) |
S = N/A O = 226 T = TO (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 = 91.15 |
S = OPT O = 175 T = 138.07 (out)(err) |
S = OPT O = 175 T = 211.56 (out)(err) |
S = OPT O = 175 T = 212.65 (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 = 175 T = 102.75 (out)(err) |
S = OPT O = 175 T = 91.15 (out)(err) |
S = N/A O = 208 T = TO (out)(err) |
S = N/A O = 228 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C900_6.wcnf | S = OPT O = 174 T = 81.54 |
S = OPT O = 174 T = 139.87 (out)(err) |
S = OPT O = 174 T = 222.11 (out)(err) |
S = OPT O = 174 T = 224.16 (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 = 174 T = 150.47 (out)(err) |
S = OPT O = 174 T = 81.54 (out)(err) |
S = N/A O = 233 T = TO (out)(err) |
S = N/A O = 187 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C900_7.wcnf | S = OPT O = 194 T = 194.58 |
S = OPT O = 194 T = 431.37 (out)(err) |
S = OPT O = 194 T = 644.90 (out)(err) |
S = OPT O = 194 T = 644.57 (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 = 194 T = 250.03 (out)(err) |
S = OPT O = 194 T = 194.58 (out)(err) |
S = N/A O = 249 T = TO (out)(err) |
S = N/A O = 271 T = TO (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 = 105.92 |
S = OPT O = 179 T = 154.29 (out)(err) |
S = OPT O = 179 T = 241.39 (out)(err) |
S = OPT O = 179 T = 240.15 (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 = 179 T = 107.40 (out)(err) |
S = OPT O = 179 T = 105.92 (out)(err) |
S = N/A O = 255 T = TO (out)(err) |
S = N/A O = 244 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |
file_rwms_wcnf_L3_V70_C900_9.wcnf | S = OPT O = 181 T = 98.03 |
S = OPT O = 181 T = 166.72 (out)(err) |
S = OPT O = 181 T = 256.99 (out)(err) |
S = OPT O = 181 T = 257.49 (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 = 181 T = 116.25 (out)(err) |
S = OPT O = 181 T = 98.03 (out)(err) |
S = N/A O = 210 T = TO (out)(err) |
S = N/A O = 210 T = TO (out)(err) |
S = N/A O = N/A T = 1800.00 (out)(err) |