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 for Complete Solvers | Meaning for Incomplete Solvers |
---|---|---|
Text | Best solver column | Best solver column |
Text | Optimal solution with the best CPU time | Best solution with the best CPU time |
Text | Optimal solution and finished within the Time Out | Best solution without the best CPU time |
Text | Optimal solution and did not finish within the Time Out | Solution found but not the best |
Text | Time Out | Time Out |
Text | Buggy solution | Buggy solution |
Instance file name | Best solver | ILP-2013 | ISAC+-wms | MSUnCore | MaxHS | Maxsatz2013f | Toulbar2 | WMaxSatz+ | WMaxSatz09 | WPM1-2013 | WPM2-2013 | ahmaxsat | ckmax-small | glpk-maxsat | optimax-ni | optimax | scip-maxsat | toysat | wbo2.1-wcnf | wmifumax |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
s2v100c1200_1.wcnf | S = OPT O = 865 T = 6.07 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 865 T = 6.94 (out)(err) |
S = N/A O = 1065 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 865 T = 12.28 (out)(err) |
S = N/A O = 940 T = TO (out)(err) |
S = OPT O = 865 T = 31.09 (out)(err) |
S = OPT O = 865 T = 28.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 = 865 T = 354.94 (out)(err) |
S = OPT O = 865 T = 6.07 (out)(err) |
S = N/A O = 932 T = TO (out)(err) |
S = N/A O = 1236 T = TO (out)(err) |
S = N/A O = 1211 T = TO (out)(err) |
S = N/A O = 896 T = TO (out)(err) |
S = N/A O = 1299 T = TO (out)(err) |
S = N/A O = N/A T = 178.97 (out)(err) |
S = N/A O = N/A T = 1750.65 (out)(err) |
s2v100c1200_2.wcnf | S = OPT O = 774 T = 2.85 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 774 T = 5.01 (out)(err) |
S = N/A O = 992 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 774 T = 6.72 (out)(err) |
S = N/A O = 859 T = TO (out)(err) |
S = OPT O = 774 T = 18.73 (out)(err) |
S = OPT O = 774 T = 20.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 = 774 T = 258.95 (out)(err) |
S = OPT O = 774 T = 2.85 (out)(err) |
S = N/A O = 841 T = TO (out)(err) |
S = N/A O = 1088 T = TO (out)(err) |
S = N/A O = 1100 T = TO (out)(err) |
S = N/A O = 782 T = TO (out)(err) |
S = N/A O = 1016 T = TO (out)(err) |
S = N/A O = N/A T = 178.81 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1200_3.wcnf | S = OPT O = 933 T = 27.10 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 933 T = 27.57 (out)(err) |
S = N/A O = 1199 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 933 T = 48.92 (out)(err) |
S = N/A O = 993 T = TO (out)(err) |
S = OPT O = 933 T = 147.82 (out)(err) |
S = OPT O = 933 T = 134.37 (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 = 938 T = 1797.81 (out)(err) |
S = OPT O = 933 T = 27.10 (out)(err) |
S = N/A O = 1009 T = TO (out)(err) |
S = N/A O = 1318 T = TO (out)(err) |
S = N/A O = 1276 T = TO (out)(err) |
S = N/A O = 948 T = TO (out)(err) |
S = N/A O = 1231 T = TO (out)(err) |
S = N/A O = N/A T = 178.75 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1200_4.wcnf | S = OPT O = 798 T = 2.73 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 798 T = 4.49 (out)(err) |
S = N/A O = 1039 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 798 T = 4.35 (out)(err) |
S = N/A O = 931 T = TO (out)(err) |
S = OPT O = 798 T = 11.34 (out)(err) |
S = OPT O = 798 T = 11.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 = 798 T = 169.06 (out)(err) |
S = OPT O = 798 T = 2.73 (out)(err) |
S = N/A O = 892 T = TO (out)(err) |
S = N/A O = 1229 T = TO (out)(err) |
S = N/A O = 1154 T = TO (out)(err) |
S = N/A O = 805 T = TO (out)(err) |
S = N/A O = 1256 T = TO (out)(err) |
S = N/A O = N/A T = 198.97 (out)(err) |
S = N/A O = N/A T = 1438.41 (out)(err) |
s2v100c1200_5.wcnf | S = OPT O = 876 T = 4.03 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 876 T = 5.39 (out)(err) |
S = N/A O = 1097 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 876 T = 10.70 (out)(err) |
S = N/A O = 950 T = TO (out)(err) |
S = OPT O = 876 T = 30.23 (out)(err) |
S = OPT O = 876 T = 29.28 (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 = 507.85 (out)(err) |
S = OPT O = 876 T = 4.03 (out)(err) |
S = N/A O = 979 T = TO (out)(err) |
S = N/A O = 1107 T = TO (out)(err) |
S = N/A O = 1237 T = TO (out)(err) |
S = N/A O = 903 T = TO (out)(err) |
S = N/A O = 1263 T = TO (out)(err) |
S = N/A O = N/A T = 178.83 (out)(err) |
S = N/A O = N/A T = 990.47 (out)(err) |
s2v100c1200_6.wcnf | S = OPT O = 734 T = 0.72 |
S = OPT O = 734 T = 222.47 (out)(err) |
S = OPT O = 734 T = 1.08 (out)(err) |
S = N/A O = 1005 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 734 T = 0.72 (out)(err) |
S = N/A O = 747 T = TO (out)(err) |
S = OPT O = 734 T = 2.38 (out)(err) |
S = OPT O = 734 T = 2.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 = 734 T = 22.03 (out)(err) |
S = OPT O = 734 T = 0.89 (out)(err) |
S = N/A O = 815 T = TO (out)(err) |
S = N/A O = 963 T = TO (out)(err) |
S = N/A O = 957 T = TO (out)(err) |
S = N/A O = 735 T = TO (out)(err) |
S = N/A O = 1063 T = TO (out)(err) |
S = N/A O = N/A T = 181.06 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1200_7.wcnf | S = OPT O = 800 T = 10.97 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 800 T = 12.95 (out)(err) |
S = N/A O = 1069 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 800 T = 17.17 (out)(err) |
S = N/A O = 868 T = TO (out)(err) |
S = OPT O = 800 T = 50.64 (out)(err) |
S = OPT O = 800 T = 48.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 = 800 T = 708.15 (out)(err) |
S = OPT O = 800 T = 10.97 (out)(err) |
S = N/A O = 857 T = TO (out)(err) |
S = N/A O = 1128 T = TO (out)(err) |
S = N/A O = 1106 T = TO (out)(err) |
S = N/A O = 805 T = TO (out)(err) |
S = N/A O = 1258 T = TO (out)(err) |
S = N/A O = N/A T = 178.64 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1200_8.wcnf | S = OPT O = 962 T = 28.71 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 962 T = 28.71 (out)(err) |
S = N/A O = 1374 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 962 T = 74.82 (out)(err) |
S = N/A O = 1030 T = TO (out)(err) |
S = OPT O = 962 T = 231.66 (out)(err) |
S = OPT O = 962 T = 231.02 (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 = 962 T = 1797.73 (out)(err) |
S = OPT O = 962 T = 34.90 (out)(err) |
S = N/A O = 1047 T = TO (out)(err) |
S = N/A O = 1291 T = TO (out)(err) |
S = N/A O = 1326 T = TO (out)(err) |
S = N/A O = 1002 T = TO (out)(err) |
S = N/A O = 1456 T = TO (out)(err) |
S = N/A O = N/A T = 178.62 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_1.wcnf | S = OPT O = 971 T = 6.26 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 971 T = 6.26 (out)(err) |
S = N/A O = 1260 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 971 T = 16.82 (out)(err) |
S = N/A O = 1042 T = TO (out)(err) |
S = OPT O = 971 T = 54.97 (out)(err) |
S = OPT O = 971 T = 44.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 = 971 T = 796.11 (out)(err) |
S = OPT O = 971 T = 11.53 (out)(err) |
S = N/A O = 1048 T = TO (out)(err) |
S = N/A O = 1251 T = TO (out)(err) |
S = N/A O = 1310 T = TO (out)(err) |
S = N/A O = 1002 T = TO (out)(err) |
S = N/A O = 1439 T = TO (out)(err) |
S = N/A O = N/A T = 178.75 (out)(err) |
S = N/A O = N/A T = 1478.73 (out)(err) |
s2v100c1300_2.wcnf | S = OPT O = 930 T = 11.34 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 930 T = 11.71 (out)(err) |
S = N/A O = 1151 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 930 T = 51.77 (out)(err) |
S = N/A O = 1007 T = TO (out)(err) |
S = OPT O = 930 T = 153.01 (out)(err) |
S = OPT O = 930 T = 155.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 = 930 T = 1245.37 (out)(err) |
S = OPT O = 930 T = 11.34 (out)(err) |
S = N/A O = 1033 T = TO (out)(err) |
S = N/A O = 1386 T = TO (out)(err) |
S = N/A O = 1293 T = TO (out)(err) |
S = N/A O = 972 T = TO (out)(err) |
S = N/A O = 1404 T = TO (out)(err) |
S = N/A O = N/A T = 179.84 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_3.wcnf | S = OPT O = 925 T = 3.54 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 925 T = 6.99 (out)(err) |
S = N/A O = 1057 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 925 T = 10.22 (out)(err) |
S = N/A O = 993 T = TO (out)(err) |
S = OPT O = 925 T = 27.05 (out)(err) |
S = OPT O = 925 T = 27.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 = 925 T = 385.40 (out)(err) |
S = OPT O = 925 T = 3.54 (out)(err) |
S = N/A O = 1025 T = TO (out)(err) |
S = N/A O = 1266 T = TO (out)(err) |
S = N/A O = 1139 T = TO (out)(err) |
S = N/A O = 926 T = TO (out)(err) |
S = N/A O = 1271 T = TO (out)(err) |
S = N/A O = N/A T = 178.85 (out)(err) |
S = N/A O = N/A T = 1057.62 (out)(err) |
s2v100c1300_4.wcnf | S = OPT O = 970 T = 7.44 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 970 T = 10.42 (out)(err) |
S = N/A O = 1279 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 970 T = 25.34 (out)(err) |
S = N/A O = 1061 T = TO (out)(err) |
S = OPT O = 970 T = 75.44 (out)(err) |
S = OPT O = 970 T = 75.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 = 970 T = 1421.33 (out)(err) |
S = OPT O = 970 T = 7.44 (out)(err) |
S = N/A O = 1083 T = TO (out)(err) |
S = N/A O = 1293 T = TO (out)(err) |
S = N/A O = 1295 T = TO (out)(err) |
S = N/A O = 1006 T = TO (out)(err) |
S = N/A O = 1550 T = TO (out)(err) |
S = N/A O = N/A T = 181.97 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_5.wcnf | S = OPT O = 962 T = 17.60 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 962 T = 21.43 (out)(err) |
S = N/A O = 1246 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 962 T = 52.70 (out)(err) |
S = N/A O = 1095 T = TO (out)(err) |
S = OPT O = 962 T = 142.03 (out)(err) |
S = OPT O = 962 T = 149.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 = 962 T = 1343.69 (out)(err) |
S = OPT O = 962 T = 17.60 (out)(err) |
S = N/A O = 1054 T = TO (out)(err) |
S = N/A O = 1305 T = TO (out)(err) |
S = N/A O = 1237 T = TO (out)(err) |
S = N/A O = 980 T = TO (out)(err) |
S = N/A O = 1244 T = TO (out)(err) |
S = N/A O = N/A T = 178.88 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_6.wcnf | S = OPT O = 933 T = 3.97 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 933 T = 3.97 (out)(err) |
S = N/A O = 1271 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 933 T = 15.21 (out)(err) |
S = N/A O = 983 T = TO (out)(err) |
S = OPT O = 933 T = 31.14 (out)(err) |
S = OPT O = 933 T = 33.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 = 933 T = 482.56 (out)(err) |
S = OPT O = 933 T = 5.57 (out)(err) |
S = N/A O = 1040 T = TO (out)(err) |
S = N/A O = 1236 T = TO (out)(err) |
S = N/A O = 1361 T = TO (out)(err) |
S = N/A O = 970 T = TO (out)(err) |
S = N/A O = 1223 T = TO (out)(err) |
S = N/A O = N/A T = 178.96 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1300_7.wcnf | S = OPT O = 877 T = 3.44 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 877 T = 8.02 (out)(err) |
S = N/A O = 1187 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 877 T = 11.41 (out)(err) |
S = N/A O = 958 T = TO (out)(err) |
S = OPT O = 877 T = 32.65 (out)(err) |
S = OPT O = 877 T = 31.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 = 877 T = 590.32 (out)(err) |
S = OPT O = 877 T = 3.44 (out)(err) |
S = N/A O = 962 T = TO (out)(err) |
S = N/A O = 1235 T = TO (out)(err) |
S = N/A O = 1281 T = TO (out)(err) |
S = N/A O = 892 T = TO (out)(err) |
S = N/A O = 1316 T = TO (out)(err) |
S = N/A O = N/A T = 178.81 (out)(err) |
S = N/A O = N/A T = 1673.37 (out)(err) |
s2v100c1300_8.wcnf | S = OPT O = 941 T = 8.32 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 941 T = 17.07 (out)(err) |
S = N/A O = 1261 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 941 T = 35.12 (out)(err) |
S = N/A O = 1011 T = TO (out)(err) |
S = OPT O = 941 T = 105.44 (out)(err) |
S = OPT O = 941 T = 105.27 (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 = 962 T = 1797.61 (out)(err) |
S = OPT O = 941 T = 8.32 (out)(err) |
S = N/A O = 1043 T = TO (out)(err) |
S = N/A O = 1169 T = TO (out)(err) |
S = N/A O = 1213 T = TO (out)(err) |
S = N/A O = 986 T = TO (out)(err) |
S = N/A O = 1251 T = TO (out)(err) |
S = N/A O = N/A T = 178.94 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1400_1.wcnf | S = OPT O = 1019 T = 23.03 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1019 T = 23.92 (out)(err) |
S = N/A O = 1398 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1019 T = 35.74 (out)(err) |
S = N/A O = 1140 T = TO (out)(err) |
S = OPT O = 1019 T = 112.25 (out)(err) |
S = OPT O = 1019 T = 109.81 (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 = 1019 T = 1797.88 (out)(err) |
S = OPT O = 1019 T = 23.03 (out)(err) |
S = N/A O = 1123 T = TO (out)(err) |
S = N/A O = 1358 T = TO (out)(err) |
S = N/A O = 1388 T = TO (out)(err) |
S = N/A O = 1052 T = TO (out)(err) |
S = N/A O = 1468 T = TO (out)(err) |
S = N/A O = N/A T = 317.88 (out)(err) |
S = N/A O = N/A T = 1758.46 (out)(err) |
s2v100c1400_2.wcnf | S = OPT O = 1002 T = 9.77 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1002 T = 9.77 (out)(err) |
S = N/A O = 1363 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1002 T = 29.18 (out)(err) |
S = N/A O = 1126 T = TO (out)(err) |
S = OPT O = 1002 T = 88.82 (out)(err) |
S = OPT O = 1002 T = 85.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 = 1002 T = 977.71 (out)(err) |
S = OPT O = 1002 T = 12.53 (out)(err) |
S = N/A O = 1073 T = TO (out)(err) |
S = N/A O = 1384 T = TO (out)(err) |
S = N/A O = 1338 T = TO (out)(err) |
S = N/A O = 1010 T = TO (out)(err) |
S = N/A O = 1280 T = TO (out)(err) |
S = N/A O = N/A T = 193.97 (out)(err) |
S = N/A O = N/A T = 1541.79 (out)(err) |
s2v100c1400_3.wcnf | S = OPT O = 1020 T = 13.16 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1020 T = 13.16 (out)(err) |
S = N/A O = 1372 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1020 T = 58.76 (out)(err) |
S = N/A O = 1116 T = TO (out)(err) |
S = OPT O = 1020 T = 183.05 (out)(err) |
S = OPT O = 1020 T = 174.68 (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 = 1020 T = 1797.86 (out)(err) |
S = OPT O = 1020 T = 22.55 (out)(err) |
S = N/A O = 1108 T = TO (out)(err) |
S = N/A O = 1341 T = TO (out)(err) |
S = N/A O = 1400 T = TO (out)(err) |
S = N/A O = 1039 T = TO (out)(err) |
S = N/A O = 1253 T = TO (out)(err) |
S = N/A O = N/A T = 212.64 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1400_4.wcnf | S = OPT O = 1094 T = 28.40 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1094 T = 28.40 (out)(err) |
S = N/A O = 1425 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1094 T = 74.35 (out)(err) |
S = N/A O = 1149 T = TO (out)(err) |
S = OPT O = 1094 T = 213.08 (out)(err) |
S = OPT O = 1094 T = 229.51 (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 = 1097 T = 1797.83 (out)(err) |
S = OPT O = 1094 T = 46.43 (out)(err) |
S = N/A O = 1188 T = TO (out)(err) |
S = N/A O = 1583 T = TO (out)(err) |
S = N/A O = 1638 T = TO (out)(err) |
S = N/A O = 1140 T = TO (out)(err) |
S = N/A O = 1466 T = TO (out)(err) |
S = N/A O = N/A T = 179.54 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1400_5.wcnf | S = OPT O = 1018 T = 10.09 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1018 T = 12.47 (out)(err) |
S = N/A O = 1323 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1018 T = 33.93 (out)(err) |
S = N/A O = 1077 T = TO (out)(err) |
S = OPT O = 1018 T = 108.08 (out)(err) |
S = OPT O = 1018 T = 105.42 (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 = 1339.34 (out)(err) |
S = OPT O = 1018 T = 10.09 (out)(err) |
S = N/A O = 1147 T = TO (out)(err) |
S = N/A O = 1379 T = TO (out)(err) |
S = N/A O = 1437 T = TO (out)(err) |
S = N/A O = 1048 T = TO (out)(err) |
S = N/A O = 1437 T = TO (out)(err) |
S = N/A O = N/A T = 199.03 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1400_6.wcnf | S = OPT O = 997 T = 3.28 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 997 T = 3.28 (out)(err) |
S = N/A O = 1420 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 997 T = 8.31 (out)(err) |
S = N/A O = 1106 T = TO (out)(err) |
S = OPT O = 997 T = 21.92 (out)(err) |
S = OPT O = 997 T = 21.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 = 997 T = 684.40 (out)(err) |
S = OPT O = 997 T = 4.35 (out)(err) |
S = N/A O = 1119 T = TO (out)(err) |
S = N/A O = 1390 T = TO (out)(err) |
S = N/A O = 1417 T = TO (out)(err) |
S = N/A O = 1025 T = TO (out)(err) |
S = N/A O = 1427 T = TO (out)(err) |
S = N/A O = N/A T = 317.49 (out)(err) |
S = N/A O = N/A T = 1491.17 (out)(err) |
s2v100c1400_7.wcnf | S = OPT O = 1001 T = 24.33 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1001 T = 24.33 (out)(err) |
S = N/A O = 1308 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1001 T = 57.93 (out)(err) |
S = N/A O = 1056 T = TO (out)(err) |
S = OPT O = 1001 T = 160.01 (out)(err) |
S = OPT O = 1001 T = 165.01 (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 = 1002 T = 1797.84 (out)(err) |
S = OPT O = 1001 T = 30.98 (out)(err) |
S = N/A O = 1075 T = TO (out)(err) |
S = N/A O = 1185 T = TO (out)(err) |
S = N/A O = 1339 T = TO (out)(err) |
S = N/A O = 1052 T = TO (out)(err) |
S = N/A O = 1580 T = TO (out)(err) |
S = N/A O = N/A T = 188.81 (out)(err) |
S = N/A O = N/A T = 1002.49 (out)(err) |
s2v100c1400_8.wcnf | S = OPT O = 1084 T = 19.95 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1084 T = 19.95 (out)(err) |
S = N/A O = 1341 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1084 T = 68.32 (out)(err) |
S = N/A O = 1143 T = TO (out)(err) |
S = OPT O = 1084 T = 107.62 (out)(err) |
S = OPT O = 1084 T = 194.81 (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 = 1084 T = 1797.81 (out)(err) |
S = OPT O = 1084 T = 21.79 (out)(err) |
S = N/A O = 1186 T = TO (out)(err) |
S = N/A O = 1392 T = TO (out)(err) |
S = N/A O = 1455 T = TO (out)(err) |
S = N/A O = 1109 T = TO (out)(err) |
S = N/A O = 1472 T = TO (out)(err) |
S = N/A O = N/A T = 201.55 (out)(err) |
S = N/A O = N/A T = 1470.61 (out)(err) |
s2v100c1500_1.wcnf | S = OPT O = 1077 T = 12.32 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1077 T = 16.24 (out)(err) |
S = N/A O = 1449 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1077 T = 27.37 (out)(err) |
S = N/A O = 1204 T = TO (out)(err) |
S = OPT O = 1077 T = 80.06 (out)(err) |
S = OPT O = 1077 T = 79.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 = 1077 T = 1242.31 (out)(err) |
S = OPT O = 1077 T = 12.32 (out)(err) |
S = N/A O = 1156 T = TO (out)(err) |
S = N/A O = 1436 T = TO (out)(err) |
S = N/A O = 1450 T = TO (out)(err) |
S = N/A O = 1092 T = TO (out)(err) |
S = N/A O = 1627 T = TO (out)(err) |
S = N/A O = N/A T = 178.87 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1500_2.wcnf | S = OPT O = 1125 T = 11.89 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1125 T = 11.89 (out)(err) |
S = N/A O = 1456 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1125 T = 67.53 (out)(err) |
S = N/A O = 1263 T = TO (out)(err) |
S = OPT O = 1125 T = 195.70 (out)(err) |
S = OPT O = 1125 T = 197.23 (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 = 1155 T = 1797.86 (out)(err) |
S = OPT O = 1125 T = 16.32 (out)(err) |
S = N/A O = 1229 T = TO (out)(err) |
S = N/A O = 1582 T = TO (out)(err) |
S = N/A O = 1484 T = TO (out)(err) |
S = N/A O = 1138 T = TO (out)(err) |
S = N/A O = 1444 T = TO (out)(err) |
S = N/A O = N/A T = 179.58 (out)(err) |
S = N/A O = N/A T = 971.88 (out)(err) |
s2v100c1500_3.wcnf | S = OPT O = 1151 T = 22.68 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1151 T = 22.68 (out)(err) |
S = N/A O = 1490 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1151 T = 66.26 (out)(err) |
S = N/A O = 1267 T = TO (out)(err) |
S = OPT O = 1151 T = 190.02 (out)(err) |
S = OPT O = 1151 T = 188.74 (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 = 1151 T = 1797.88 (out)(err) |
S = OPT O = 1151 T = 39.51 (out)(err) |
S = N/A O = 1265 T = TO (out)(err) |
S = N/A O = 1474 T = TO (out)(err) |
S = N/A O = 1478 T = TO (out)(err) |
S = N/A O = 1197 T = TO (out)(err) |
S = N/A O = 1419 T = TO (out)(err) |
S = N/A O = N/A T = 178.77 (out)(err) |
S = N/A O = N/A T = 1366.77 (out)(err) |
s2v100c1500_4.wcnf | S = OPT O = 1072 T = 13.78 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1072 T = 38.75 (out)(err) |
S = N/A O = 1536 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1072 T = 65.63 (out)(err) |
S = N/A O = 1137 T = TO (out)(err) |
S = OPT O = 1072 T = 195.66 (out)(err) |
S = OPT O = 1072 T = 199.39 (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 = 1098 T = 1797.73 (out)(err) |
S = OPT O = 1072 T = 13.78 (out)(err) |
S = N/A O = 1180 T = TO (out)(err) |
S = N/A O = 1442 T = TO (out)(err) |
S = N/A O = 1452 T = TO (out)(err) |
S = N/A O = 1094 T = TO (out)(err) |
S = N/A O = 1461 T = TO (out)(err) |
S = N/A O = N/A T = 179.52 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1500_5.wcnf | S = OPT O = 1151 T = 20.97 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1151 T = 20.97 (out)(err) |
S = N/A O = 1347 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1151 T = 82.83 (out)(err) |
S = N/A O = 1292 T = TO (out)(err) |
S = OPT O = 1151 T = 226.75 (out)(err) |
S = OPT O = 1151 T = 252.96 (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 = 1152 T = 1797.77 (out)(err) |
S = OPT O = 1151 T = 29.06 (out)(err) |
S = N/A O = 1313 T = TO (out)(err) |
S = N/A O = 1463 T = TO (out)(err) |
S = N/A O = 1455 T = TO (out)(err) |
S = N/A O = 1217 T = TO (out)(err) |
S = N/A O = 1427 T = TO (out)(err) |
S = N/A O = N/A T = 192.64 (out)(err) |
S = N/A O = N/A T = 1521.17 (out)(err) |
s2v100c1500_6.wcnf | S = OPT O = 1225 T = 35.16 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1225 T = 39.86 (out)(err) |
S = N/A O = 1520 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1225 T = 141.34 (out)(err) |
S = N/A O = 1386 T = TO (out)(err) |
S = OPT O = 1225 T = 425.67 (out)(err) |
S = OPT O = 1225 T = 447.34 (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 = 1255 T = 1797.75 (out)(err) |
S = OPT O = 1225 T = 35.16 (out)(err) |
S = N/A O = 1380 T = TO (out)(err) |
S = N/A O = 1606 T = TO (out)(err) |
S = N/A O = 1687 T = TO (out)(err) |
S = N/A O = 1297 T = TO (out)(err) |
S = N/A O = 1703 T = TO (out)(err) |
S = N/A O = N/A T = 317.78 (out)(err) |
S = N/A O = N/A T = 1638.21 (out)(err) |
s2v100c1500_7.wcnf | S = OPT O = 1186 T = 14.28 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1186 T = 14.28 (out)(err) |
S = N/A O = 1569 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1186 T = 56.11 (out)(err) |
S = N/A O = 1319 T = TO (out)(err) |
S = OPT O = 1186 T = 157.51 (out)(err) |
S = OPT O = 1186 T = 159.07 (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 = 1186 T = 1797.89 (out)(err) |
S = OPT O = 1186 T = 21.00 (out)(err) |
S = N/A O = 1319 T = TO (out)(err) |
S = N/A O = 1649 T = TO (out)(err) |
S = N/A O = 1585 T = TO (out)(err) |
S = N/A O = 1210 T = TO (out)(err) |
S = N/A O = 1676 T = TO (out)(err) |
S = N/A O = N/A T = 206.92 (out)(err) |
S = N/A O = N/A T = 1025.16 (out)(err) |
s2v100c1500_8.wcnf | S = OPT O = 1217 T = 35.16 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1217 T = 40.51 (out)(err) |
S = N/A O = 1589 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1217 T = 232.62 (out)(err) |
S = N/A O = 1316 T = TO (out)(err) |
S = OPT O = 1217 T = 701.81 (out)(err) |
S = OPT O = 1217 T = 696.34 (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 = 1253 T = 1796.94 (out)(err) |
S = OPT O = 1217 T = 35.16 (out)(err) |
S = N/A O = 1365 T = TO (out)(err) |
S = N/A O = 1587 T = TO (out)(err) |
S = N/A O = 1737 T = TO (out)(err) |
S = N/A O = 1291 T = TO (out)(err) |
S = N/A O = 1580 T = TO (out)(err) |
S = N/A O = N/A T = 317.83 (out)(err) |
S = N/A O = N/A T = 920.48 (out)(err) |
s2v100c1600_1.wcnf | S = OPT O = 1230 T = 12.79 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1230 T = 13.92 (out)(err) |
S = N/A O = 1735 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1230 T = 51.85 (out)(err) |
S = N/A O = 1378 T = TO (out)(err) |
S = OPT O = 1230 T = 164.09 (out)(err) |
S = OPT O = 1230 T = 158.03 (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 = 1230 T = 1797.85 (out)(err) |
S = OPT O = 1230 T = 12.79 (out)(err) |
S = N/A O = 1355 T = TO (out)(err) |
S = N/A O = 1688 T = TO (out)(err) |
S = N/A O = 1714 T = TO (out)(err) |
S = N/A O = 1336 T = TO (out)(err) |
S = N/A O = 1710 T = TO (out)(err) |
S = N/A O = N/A T = 318.21 (out)(err) |
S = N/A O = N/A T = 593.79 (out)(err) |
s2v100c1600_2.wcnf | S = OPT O = 1265 T = 112.60 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1265 T = 112.60 (out)(err) |
S = N/A O = 1501 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1265 T = 415.89 (out)(err) |
S = N/A O = 1408 T = TO (out)(err) |
S = OPT O = 1265 T = 1232.74 (out)(err) |
S = OPT O = 1265 T = 1237.91 (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 = 1265 T = 1797.58 (out)(err) |
S = OPT O = 1265 T = 118.01 (out)(err) |
S = N/A O = 1394 T = TO (out)(err) |
S = N/A O = 1710 T = TO (out)(err) |
S = N/A O = 1652 T = TO (out)(err) |
S = N/A O = 1358 T = TO (out)(err) |
S = N/A O = 1709 T = TO (out)(err) |
S = N/A O = N/A T = 317.72 (out)(err) |
S = N/A O = N/A T = 1309.51 (out)(err) |
s2v100c1600_3.wcnf | S = OPT O = 1309 T = 75.65 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1309 T = 79.92 (out)(err) |
S = N/A O = 1647 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1309 T = 214.49 (out)(err) |
S = N/A O = 1393 T = TO (out)(err) |
S = OPT O = 1309 T = 661.93 (out)(err) |
S = OPT O = 1309 T = 664.49 (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 = 1335 T = 1797.88 (out)(err) |
S = OPT O = 1309 T = 75.65 (out)(err) |
S = N/A O = 1457 T = TO (out)(err) |
S = N/A O = 1718 T = TO (out)(err) |
S = N/A O = 1706 T = TO (out)(err) |
S = N/A O = 1354 T = TO (out)(err) |
S = N/A O = 1861 T = TO (out)(err) |
S = N/A O = N/A T = 317.68 (out)(err) |
S = N/A O = N/A T = 1514.29 (out)(err) |
s2v100c1600_4.wcnf | S = OPT O = 1267 T = 35.90 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1267 T = 93.98 (out)(err) |
S = N/A O = 1560 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1267 T = 568.83 (out)(err) |
S = N/A O = 1418 T = TO (out)(err) |
S = OPT O = 1267 T = 1776.04 (out)(err) |
S = OPT O = 1267 T = 1710.87 (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 = 1311 T = 1797.86 (out)(err) |
S = OPT O = 1267 T = 35.90 (out)(err) |
S = N/A O = 1409 T = TO (out)(err) |
S = N/A O = 1735 T = TO (out)(err) |
S = N/A O = 1642 T = TO (out)(err) |
S = N/A O = 1454 T = TO (out)(err) |
S = N/A O = 1801 T = TO (out)(err) |
S = N/A O = N/A T = 317.46 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v100c1600_5.wcnf | S = OPT O = 1298 T = 26.24 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1298 T = 26.24 (out)(err) |
S = N/A O = 1646 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1298 T = 92.72 (out)(err) |
S = N/A O = 1436 T = TO (out)(err) |
S = OPT O = 1298 T = 291.79 (out)(err) |
S = OPT O = 1298 T = 280.44 (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 = 1305 T = 1797.92 (out)(err) |
S = OPT O = 1298 T = 37.44 (out)(err) |
S = N/A O = 1417 T = TO (out)(err) |
S = N/A O = 1653 T = TO (out)(err) |
S = N/A O = 1529 T = TO (out)(err) |
S = N/A O = 1354 T = TO (out)(err) |
S = N/A O = 1614 T = TO (out)(err) |
S = N/A O = N/A T = 317.91 (out)(err) |
S = N/A O = N/A T = 884.58 (out)(err) |
s2v100c1600_6.wcnf | S = OPT O = 1190 T = 12.10 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1190 T = 12.10 (out)(err) |
S = N/A O = 1434 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1190 T = 66.20 (out)(err) |
S = N/A O = 1328 T = TO (out)(err) |
S = OPT O = 1190 T = 194.03 (out)(err) |
S = OPT O = 1190 T = 189.56 (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 = 1199 T = 1797.80 (out)(err) |
S = OPT O = 1190 T = 19.35 (out)(err) |
S = N/A O = 1312 T = TO (out)(err) |
S = N/A O = 1578 T = TO (out)(err) |
S = N/A O = 1630 T = TO (out)(err) |
S = N/A O = 1227 T = TO (out)(err) |
S = N/A O = 1815 T = TO (out)(err) |
S = N/A O = N/A T = 317.45 (out)(err) |
S = N/A O = N/A T = 1147.41 (out)(err) |
s2v100c1600_7.wcnf | S = OPT O = 1243 T = 69.06 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1243 T = 69.06 (out)(err) |
S = N/A O = 1581 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1243 T = 305.29 (out)(err) |
S = N/A O = 1397 T = TO (out)(err) |
S = OPT O = 1243 T = 952.19 (out)(err) |
S = OPT O = 1243 T = 1037.51 (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 = 1256 T = 1797.84 (out)(err) |
S = OPT O = 1243 T = 71.06 (out)(err) |
S = N/A O = 1361 T = TO (out)(err) |
S = N/A O = 1681 T = TO (out)(err) |
S = N/A O = 1679 T = TO (out)(err) |
S = N/A O = 1289 T = TO (out)(err) |
S = N/A O = 1542 T = TO (out)(err) |
S = N/A O = N/A T = 317.87 (out)(err) |
S = N/A O = N/A T = 1080.50 (out)(err) |
s2v100c1600_8.wcnf | S = OPT O = 1184 T = 3.68 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1184 T = 6.27 (out)(err) |
S = N/A O = 1544 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1184 T = 18.69 (out)(err) |
S = N/A O = 1264 T = TO (out)(err) |
S = OPT O = 1184 T = 53.04 (out)(err) |
S = OPT O = 1184 T = 54.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 = 1184 T = 1618.39 (out)(err) |
S = OPT O = 1184 T = 3.68 (out)(err) |
S = N/A O = 1330 T = TO (out)(err) |
S = N/A O = 1500 T = TO (out)(err) |
S = N/A O = 1765 T = TO (out)(err) |
S = N/A O = 1235 T = TO (out)(err) |
S = N/A O = 1837 T = TO (out)(err) |
S = N/A O = N/A T = 318.19 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_1.wcnf | S = OPT O = 840 T = 15.09 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 840 T = 30.08 (out)(err) |
S = N/A O = 1091 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 840 T = 50.45 (out)(err) |
S = N/A O = 954 T = TO (out)(err) |
S = OPT O = 840 T = 137.03 (out)(err) |
S = OPT O = 840 T = 135.58 (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 = 849 T = 1797.86 (out)(err) |
S = OPT O = 840 T = 15.09 (out)(err) |
S = N/A O = 891 T = TO (out)(err) |
S = N/A O = 1066 T = TO (out)(err) |
S = N/A O = 1113 T = TO (out)(err) |
S = N/A O = 870 T = TO (out)(err) |
S = N/A O = 1147 T = TO (out)(err) |
S = N/A O = N/A T = 212.79 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_2.wcnf | S = OPT O = 803 T = 3.26 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 803 T = 5.71 (out)(err) |
S = N/A O = 1073 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 803 T = 7.90 (out)(err) |
S = N/A O = 870 T = TO (out)(err) |
S = OPT O = 803 T = 13.48 (out)(err) |
S = OPT O = 803 T = 13.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 = 803 T = 257.63 (out)(err) |
S = OPT O = 803 T = 3.26 (out)(err) |
S = N/A O = 864 T = TO (out)(err) |
S = N/A O = 1067 T = TO (out)(err) |
S = N/A O = 1105 T = TO (out)(err) |
S = N/A O = 810 T = TO (out)(err) |
S = N/A O = 1148 T = TO (out)(err) |
S = N/A O = N/A T = 207.04 (out)(err) |
S = N/A O = N/A T = 1307.53 (out)(err) |
s2v120c1200_3.wcnf | S = OPT O = 834 T = 9.08 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 834 T = 14.63 (out)(err) |
S = N/A O = 1109 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 834 T = 16.78 (out)(err) |
S = N/A O = 922 T = TO (out)(err) |
S = OPT O = 834 T = 54.72 (out)(err) |
S = OPT O = 834 T = 55.45 (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 = 999.02 (out)(err) |
S = OPT O = 834 T = 9.08 (out)(err) |
S = N/A O = 914 T = TO (out)(err) |
S = N/A O = 1128 T = TO (out)(err) |
S = N/A O = 1085 T = TO (out)(err) |
S = N/A O = 853 T = TO (out)(err) |
S = N/A O = 1172 T = TO (out)(err) |
S = N/A O = N/A T = 178.53 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_4.wcnf | S = OPT O = 811 T = 9.15 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 811 T = 10.40 (out)(err) |
S = N/A O = 1180 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 811 T = 9.15 (out)(err) |
S = N/A O = 890 T = TO (out)(err) |
S = OPT O = 811 T = 27.48 (out)(err) |
S = OPT O = 811 T = 24.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 = 811 T = 467.28 (out)(err) |
S = OPT O = 811 T = 11.02 (out)(err) |
S = N/A O = 870 T = TO (out)(err) |
S = N/A O = 1170 T = TO (out)(err) |
S = N/A O = 1062 T = TO (out)(err) |
S = N/A O = 813 T = TO (out)(err) |
S = N/A O = 1254 T = TO (out)(err) |
S = N/A O = N/A T = 178.85 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_5.wcnf | S = OPT O = 850 T = 26.12 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 850 T = 28.15 (out)(err) |
S = N/A O = 1156 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 850 T = 43.42 (out)(err) |
S = N/A O = 962 T = TO (out)(err) |
S = OPT O = 850 T = 294.51 (out)(err) |
S = OPT O = 850 T = 307.93 (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 = 850 T = 1797.90 (out)(err) |
S = OPT O = 850 T = 26.12 (out)(err) |
S = N/A O = 921 T = TO (out)(err) |
S = N/A O = 1062 T = TO (out)(err) |
S = N/A O = 1098 T = TO (out)(err) |
S = N/A O = 866 T = TO (out)(err) |
S = N/A O = 1047 T = TO (out)(err) |
S = N/A O = N/A T = 178.25 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_6.wcnf | S = OPT O = 784 T = 12.04 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 784 T = 34.19 (out)(err) |
S = N/A O = 1021 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 784 T = 40.86 (out)(err) |
S = N/A O = 919 T = TO (out)(err) |
S = OPT O = 784 T = 166.34 (out)(err) |
S = OPT O = 784 T = 172.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 = 784 T = 999.63 (out)(err) |
S = OPT O = 784 T = 12.04 (out)(err) |
S = N/A O = 845 T = TO (out)(err) |
S = N/A O = 1116 T = TO (out)(err) |
S = N/A O = 1057 T = TO (out)(err) |
S = N/A O = 789 T = TO (out)(err) |
S = N/A O = 1106 T = TO (out)(err) |
S = N/A O = N/A T = 178.76 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1200_7.wcnf | S = OPT O = 747 T = 1.59 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 747 T = 3.11 (out)(err) |
S = N/A O = 1036 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 747 T = 3.36 (out)(err) |
S = N/A O = 784 T = TO (out)(err) |
S = OPT O = 747 T = 8.57 (out)(err) |
S = OPT O = 747 T = 8.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 = 747 T = 86.08 (out)(err) |
S = OPT O = 747 T = 1.59 (out)(err) |
S = N/A O = 827 T = TO (out)(err) |
S = N/A O = 916 T = TO (out)(err) |
S = N/A O = 972 T = TO (out)(err) |
S = N/A O = 758 T = TO (out)(err) |
S = N/A O = 1070 T = TO (out)(err) |
S = N/A O = N/A T = 178.61 (out)(err) |
S = N/A O = N/A T = 1703.61 (out)(err) |
s2v120c1200_8.wcnf | S = OPT O = 813 T = 6.90 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 813 T = 6.90 (out)(err) |
S = N/A O = 1169 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 813 T = 10.38 (out)(err) |
S = N/A O = 928 T = TO (out)(err) |
S = OPT O = 813 T = 30.54 (out)(err) |
S = OPT O = 813 T = 29.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 = 813 T = 512.77 (out)(err) |
S = OPT O = 813 T = 7.31 (out)(err) |
S = N/A O = 890 T = TO (out)(err) |
S = N/A O = 1026 T = TO (out)(err) |
S = N/A O = 1074 T = TO (out)(err) |
S = N/A O = 826 T = TO (out)(err) |
S = N/A O = 1279 T = TO (out)(err) |
S = N/A O = N/A T = 178.77 (out)(err) |
S = N/A O = N/A T = 1670.59 (out)(err) |
s2v120c1300_1.wcnf | S = OPT O = 890 T = 6.07 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 890 T = 6.53 (out)(err) |
S = N/A O = 1126 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 890 T = 9.46 (out)(err) |
S = N/A O = 989 T = TO (out)(err) |
S = OPT O = 890 T = 30.38 (out)(err) |
S = OPT O = 890 T = 29.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 = 890 T = 546.74 (out)(err) |
S = OPT O = 890 T = 6.07 (out)(err) |
S = N/A O = 966 T = TO (out)(err) |
S = N/A O = 1228 T = TO (out)(err) |
S = N/A O = 1114 T = TO (out)(err) |
S = N/A O = 897 T = TO (out)(err) |
S = N/A O = 1138 T = TO (out)(err) |
S = N/A O = N/A T = 307.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_2.wcnf | S = OPT O = 847 T = 2.88 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 847 T = 5.64 (out)(err) |
S = N/A O = 1109 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 847 T = 10.79 (out)(err) |
S = N/A O = 987 T = TO (out)(err) |
S = OPT O = 847 T = 26.41 (out)(err) |
S = OPT O = 847 T = 21.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 = 847 T = 357.49 (out)(err) |
S = OPT O = 847 T = 2.88 (out)(err) |
S = N/A O = 912 T = TO (out)(err) |
S = N/A O = 1126 T = TO (out)(err) |
S = N/A O = 1049 T = TO (out)(err) |
S = N/A O = 865 T = TO (out)(err) |
S = N/A O = 1267 T = TO (out)(err) |
S = N/A O = N/A T = 248.96 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_3.wcnf | S = OPT O = 941 T = 7.84 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 941 T = 16.29 (out)(err) |
S = N/A O = 1239 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 941 T = 34.80 (out)(err) |
S = N/A O = 1044 T = TO (out)(err) |
S = OPT O = 941 T = 69.50 (out)(err) |
S = OPT O = 941 T = 67.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 = 941 T = 1771.52 (out)(err) |
S = OPT O = 941 T = 7.84 (out)(err) |
S = N/A O = 1025 T = TO (out)(err) |
S = N/A O = 1183 T = TO (out)(err) |
S = N/A O = 1269 T = TO (out)(err) |
S = N/A O = 960 T = TO (out)(err) |
S = N/A O = 1358 T = TO (out)(err) |
S = N/A O = N/A T = 178.90 (out)(err) |
S = N/A O = N/A T = 1490.84 (out)(err) |
s2v120c1300_4.wcnf | S = OPT O = 939 T = 11.13 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 939 T = 16.04 (out)(err) |
S = N/A O = 1251 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 939 T = 33.99 (out)(err) |
S = N/A O = 1041 T = TO (out)(err) |
S = OPT O = 939 T = 113.06 (out)(err) |
S = OPT O = 939 T = 99.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 = 939 T = 1303.46 (out)(err) |
S = OPT O = 939 T = 11.13 (out)(err) |
S = N/A O = 1043 T = TO (out)(err) |
S = N/A O = 1216 T = TO (out)(err) |
S = N/A O = 1197 T = TO (out)(err) |
S = N/A O = 978 T = TO (out)(err) |
S = N/A O = 1313 T = TO (out)(err) |
S = N/A O = N/A T = 178.91 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_5.wcnf | S = OPT O = 949 T = 24.66 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 949 T = 59.56 (out)(err) |
S = N/A O = 1433 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 949 T = 102.68 (out)(err) |
S = N/A O = 1051 T = TO (out)(err) |
S = OPT O = 949 T = 288.49 (out)(err) |
S = OPT O = 949 T = 281.84 (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 = 1000 T = 1797.85 (out)(err) |
S = OPT O = 949 T = 24.66 (out)(err) |
S = N/A O = 1027 T = TO (out)(err) |
S = N/A O = 1214 T = TO (out)(err) |
S = N/A O = 1277 T = TO (out)(err) |
S = N/A O = 977 T = TO (out)(err) |
S = N/A O = 1382 T = TO (out)(err) |
S = N/A O = N/A T = 178.90 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_6.wcnf | S = OPT O = 865 T = 4.45 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 865 T = 10.18 (out)(err) |
S = N/A O = 1235 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 865 T = 13.59 (out)(err) |
S = N/A O = 898 T = TO (out)(err) |
S = OPT O = 865 T = 43.85 (out)(err) |
S = OPT O = 865 T = 38.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 = 865 T = 939.96 (out)(err) |
S = OPT O = 865 T = 4.45 (out)(err) |
S = N/A O = 956 T = TO (out)(err) |
S = N/A O = 1135 T = TO (out)(err) |
S = N/A O = 1204 T = TO (out)(err) |
S = N/A O = 868 T = TO (out)(err) |
S = N/A O = 1182 T = TO (out)(err) |
S = N/A O = N/A T = 178.76 (out)(err) |
S = N/A O = N/A T = 1275.11 (out)(err) |
s2v120c1300_7.wcnf | S = OPT O = 879 T = 3.50 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 879 T = 6.08 (out)(err) |
S = N/A O = 1101 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 879 T = 10.49 (out)(err) |
S = N/A O = 992 T = TO (out)(err) |
S = OPT O = 879 T = 22.98 (out)(err) |
S = OPT O = 879 T = 23.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 = 879 T = 919.25 (out)(err) |
S = OPT O = 879 T = 3.50 (out)(err) |
S = N/A O = 970 T = TO (out)(err) |
S = N/A O = 1167 T = TO (out)(err) |
S = N/A O = 1264 T = TO (out)(err) |
S = N/A O = 901 T = TO (out)(err) |
S = N/A O = 1369 T = TO (out)(err) |
S = N/A O = N/A T = 178.74 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1300_8.wcnf | S = OPT O = 868 T = 7.28 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 868 T = 8.08 (out)(err) |
S = N/A O = 1220 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 868 T = 12.13 (out)(err) |
S = N/A O = 919 T = TO (out)(err) |
S = OPT O = 868 T = 32.62 (out)(err) |
S = OPT O = 868 T = 33.62 (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 = 566.95 (out)(err) |
S = OPT O = 868 T = 7.28 (out)(err) |
S = N/A O = 935 T = TO (out)(err) |
S = N/A O = 1142 T = TO (out)(err) |
S = N/A O = 1119 T = TO (out)(err) |
S = N/A O = 877 T = TO (out)(err) |
S = N/A O = 1265 T = TO (out)(err) |
S = N/A O = N/A T = 178.82 (out)(err) |
S = N/A O = N/A T = 1228.14 (out)(err) |
s2v120c1400_1.wcnf | S = OPT O = 1028 T = 16.58 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1028 T = 18.74 (out)(err) |
S = N/A O = 1308 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1028 T = 29.99 (out)(err) |
S = N/A O = 1199 T = TO (out)(err) |
S = OPT O = 1028 T = 70.53 (out)(err) |
S = OPT O = 1028 T = 71.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 = 1028 T = 1401.03 (out)(err) |
S = OPT O = 1028 T = 16.58 (out)(err) |
S = N/A O = 1095 T = TO (out)(err) |
S = N/A O = 1327 T = TO (out)(err) |
S = N/A O = 1352 T = TO (out)(err) |
S = N/A O = 1040 T = TO (out)(err) |
S = N/A O = 1372 T = TO (out)(err) |
S = N/A O = N/A T = 179.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_2.wcnf | S = OPT O = 1008 T = 21.78 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1008 T = 64.87 (out)(err) |
S = N/A O = 1464 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1008 T = 99.92 (out)(err) |
S = N/A O = 1079 T = TO (out)(err) |
S = OPT O = 1008 T = 376.17 (out)(err) |
S = OPT O = 1008 T = 361.95 (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 = 1038 T = 1797.89 (out)(err) |
S = OPT O = 1008 T = 21.78 (out)(err) |
S = N/A O = 1121 T = TO (out)(err) |
S = N/A O = 1351 T = TO (out)(err) |
S = N/A O = 1326 T = TO (out)(err) |
S = N/A O = 1067 T = TO (out)(err) |
S = N/A O = 1482 T = TO (out)(err) |
S = N/A O = N/A T = 178.55 (out)(err) |
S = N/A O = N/A T = 1554.11 (out)(err) |
s2v120c1400_3.wcnf | S = OPT O = 983 T = 3.79 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 983 T = 10.13 (out)(err) |
S = N/A O = 1375 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 983 T = 8.06 (out)(err) |
S = N/A O = 1009 T = TO (out)(err) |
S = OPT O = 983 T = 26.91 (out)(err) |
S = OPT O = 983 T = 25.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 = 983 T = 447.91 (out)(err) |
S = OPT O = 983 T = 3.79 (out)(err) |
S = N/A O = 1119 T = TO (out)(err) |
S = N/A O = 1324 T = TO (out)(err) |
S = N/A O = 1348 T = TO (out)(err) |
S = N/A O = 1064 T = TO (out)(err) |
S = N/A O = 1525 T = TO (out)(err) |
S = N/A O = N/A T = 178.96 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_4.wcnf | S = OPT O = 1007 T = 32.28 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1007 T = 32.28 (out)(err) |
S = N/A O = 1361 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1007 T = 69.78 (out)(err) |
S = N/A O = 1082 T = TO (out)(err) |
S = OPT O = 1007 T = 184.92 (out)(err) |
S = OPT O = 1007 T = 189.69 (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 = 1007 T = 1797.80 (out)(err) |
S = OPT O = 1007 T = 33.71 (out)(err) |
S = N/A O = 1103 T = TO (out)(err) |
S = N/A O = 1259 T = TO (out)(err) |
S = N/A O = 1260 T = TO (out)(err) |
S = N/A O = 1049 T = TO (out)(err) |
S = N/A O = 1341 T = TO (out)(err) |
S = N/A O = N/A T = 178.81 (out)(err) |
S = N/A O = N/A T = 1059.36 (out)(err) |
s2v120c1400_5.wcnf | S = OPT O = 1108 T = 156.89 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1108 T = 156.89 (out)(err) |
S = N/A O = 1425 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1108 T = 469.74 (out)(err) |
S = N/A O = 1212 T = TO (out)(err) |
S = OPT O = 1108 T = 1400.61 (out)(err) |
S = OPT O = 1108 T = 1370.65 (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 = 1108 T = 1797.87 (out)(err) |
S = OPT O = 1108 T = 290.16 (out)(err) |
S = N/A O = 1181 T = TO (out)(err) |
S = N/A O = 1451 T = TO (out)(err) |
S = N/A O = 1440 T = TO (out)(err) |
S = N/A O = 1215 T = TO (out)(err) |
S = N/A O = 1475 T = TO (out)(err) |
S = N/A O = N/A T = 179.13 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_6.wcnf | S = OPT O = 959 T = 7.10 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 959 T = 7.10 (out)(err) |
S = N/A O = 1267 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 959 T = 14.01 (out)(err) |
S = N/A O = 1050 T = TO (out)(err) |
S = OPT O = 959 T = 32.75 (out)(err) |
S = OPT O = 959 T = 32.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 = 959 T = 686.10 (out)(err) |
S = OPT O = 959 T = 8.30 (out)(err) |
S = N/A O = 1047 T = TO (out)(err) |
S = N/A O = 1213 T = TO (out)(err) |
S = N/A O = 1228 T = TO (out)(err) |
S = N/A O = 968 T = TO (out)(err) |
S = N/A O = 1457 T = TO (out)(err) |
S = N/A O = N/A T = 178.75 (out)(err) |
S = N/A O = N/A T = 641.49 (out)(err) |
s2v120c1400_7.wcnf | S = OPT O = 1040 T = 38.14 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1040 T = 56.64 (out)(err) |
S = N/A O = 1317 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1040 T = 133.14 (out)(err) |
S = N/A O = 1076 T = TO (out)(err) |
S = OPT O = 1040 T = 371.43 (out)(err) |
S = OPT O = 1040 T = 387.67 (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 = 1062 T = 1797.88 (out)(err) |
S = OPT O = 1040 T = 38.14 (out)(err) |
S = N/A O = 1142 T = TO (out)(err) |
S = N/A O = 1373 T = TO (out)(err) |
S = N/A O = 1304 T = TO (out)(err) |
S = N/A O = 1063 T = TO (out)(err) |
S = N/A O = 1387 T = TO (out)(err) |
S = N/A O = N/A T = 178.53 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1400_8.wcnf | S = OPT O = 1025 T = 26.88 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1025 T = 26.88 (out)(err) |
S = N/A O = 1529 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1025 T = 79.77 (out)(err) |
S = N/A O = 1090 T = TO (out)(err) |
S = OPT O = 1025 T = 188.94 (out)(err) |
S = OPT O = 1025 T = 183.91 (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 = 1035 T = 1797.84 (out)(err) |
S = OPT O = 1025 T = 32.92 (out)(err) |
S = N/A O = 1114 T = TO (out)(err) |
S = N/A O = 1318 T = TO (out)(err) |
S = N/A O = 1323 T = TO (out)(err) |
S = N/A O = 1050 T = TO (out)(err) |
S = N/A O = 1453 T = TO (out)(err) |
S = N/A O = N/A T = 178.92 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_1.wcnf | S = OPT O = 1119 T = 24.90 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1119 T = 90.17 (out)(err) |
S = N/A O = 1535 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1119 T = 74.25 (out)(err) |
S = N/A O = 1279 T = TO (out)(err) |
S = OPT O = 1119 T = 200.13 (out)(err) |
S = OPT O = 1119 T = 195.41 (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 = 1136 T = 1797.85 (out)(err) |
S = OPT O = 1119 T = 24.90 (out)(err) |
S = N/A O = 1254 T = TO (out)(err) |
S = N/A O = 1388 T = TO (out)(err) |
S = N/A O = 1505 T = TO (out)(err) |
S = N/A O = 1161 T = TO (out)(err) |
S = N/A O = 1668 T = TO (out)(err) |
S = N/A O = N/A T = 178.87 (out)(err) |
S = N/A O = N/A T = 1492.41 (out)(err) |
s2v120c1500_2.wcnf | S = OPT O = 1136 T = 34.16 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1136 T = 98.26 (out)(err) |
S = N/A O = 1564 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1136 T = 81.20 (out)(err) |
S = N/A O = 1208 T = TO (out)(err) |
S = OPT O = 1136 T = 270.64 (out)(err) |
S = OPT O = 1136 T = 282.49 (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 = 1190 T = 1797.83 (out)(err) |
S = OPT O = 1136 T = 34.16 (out)(err) |
S = N/A O = 1298 T = TO (out)(err) |
S = N/A O = 1459 T = TO (out)(err) |
S = N/A O = 1483 T = TO (out)(err) |
S = N/A O = 1203 T = TO (out)(err) |
S = N/A O = 1663 T = TO (out)(err) |
S = N/A O = N/A T = 178.77 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v120c1500_3.wcnf | S = OPT O = 1062 T = 8.13 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1062 T = 13.81 (out)(err) |
S = N/A O = 1489 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1062 T = 13.11 (out)(err) |
S = N/A O = 1273 T = TO (out)(err) |
S = OPT O = 1062 T = 38.70 (out)(err) |
S = OPT O = 1062 T = 38.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 = 1062 T = 1142.98 (out)(err) |
S = OPT O = 1062 T = 8.13 (out)(err) |
S = N/A O = 1196 T = TO (out)(err) |
S = N/A O = 1400 T = TO (out)(err) |
S = N/A O = 1365 T = TO (out)(err) |
S = N/A O = 1099 T = TO (out)(err) |
S = N/A O = 1570 T = TO (out)(err) |
S = N/A O = N/A T = 178.90 (out)(err) |
S = N/A O = N/A T = 1504.61 (out)(err) |
s2v120c1500_4.wcnf | S = OPT O = 1041 T = 4.93 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1041 T = 5.57 (out)(err) |
S = N/A O = 1428 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1041 T = 12.52 (out)(err) |
S = N/A O = 1173 T = TO (out)(err) |
S = OPT O = 1041 T = 27.59 (out)(err) |
S = OPT O = 1041 T = 31.20 (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 = 1094.73 (out)(err) |
S = OPT O = 1041 T = 4.93 (out)(err) |
S = N/A O = 1162 T = TO (out)(err) |
S = N/A O = 1362 T = TO (out)(err) |
S = N/A O = 1447 T = TO (out)(err) |
S = N/A O = 1062 T = TO (out)(err) |
S = N/A O = 1496 T = TO (out)(err) |
S = N/A O = N/A T = 178.90 (out)(err) |
S = N/A O = N/A T = 703.58 (out)(err) |
s2v120c1500_5.wcnf | S = OPT O = 1125 T = 5.85 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1125 T = 15.62 (out)(err) |
S = N/A O = 1634 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1125 T = 37.28 (out)(err) |
S = N/A O = 1323 T = TO (out)(err) |
S = OPT O = 1125 T = 76.09 (out)(err) |
S = OPT O = 1125 T = 76.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 = 1125 T = 1564.55 (out)(err) |
S = OPT O = 1125 T = 5.85 (out)(err) |
S = N/A O = 1222 T = TO (out)(err) |
S = N/A O = 1468 T = TO (out)(err) |
S = N/A O = 1600 T = TO (out)(err) |
S = N/A O = 1242 T = TO (out)(err) |
S = N/A O = 1746 T = TO (out)(err) |
S = N/A O = N/A T = 188.86 (out)(err) |
S = N/A O = N/A T = 1207.88 (out)(err) |
s2v120c1500_6.wcnf | S = OPT O = 1113 T = 25.33 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1113 T = 38.99 (out)(err) |
S = N/A O = 1500 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1113 T = 82.89 (out)(err) |
S = N/A O = 1308 T = TO (out)(err) |
S = OPT O = 1113 T = 157.97 (out)(err) |
S = OPT O = 1113 T = 242.75 (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 = 1113 T = 1797.63 (out)(err) |
S = OPT O = 1113 T = 25.33 (out)(err) |
S = N/A O = 1220 T = TO (out)(err) |
S = N/A O = 1471 T = TO (out)(err) |
S = N/A O = 1504 T = TO (out)(err) |
S = N/A O = 1175 T = TO (out)(err) |
S = N/A O = 1536 T = TO (out)(err) |
S = N/A O = N/A T = 179.20 (out)(err) |
S = N/A O = N/A T = 1008.42 (out)(err) |
s2v120c1500_7.wcnf | S = OPT O = 1163 T = 76.60 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1163 T = 76.60 (out)(err) |
S = N/A O = 1495 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1163 T = 266.44 (out)(err) |
S = N/A O = 1209 T = TO (out)(err) |
S = OPT O = 1163 T = 526.48 (out)(err) |
S = OPT O = 1163 T = 561.12 (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 = 1177 T = 1797.86 (out)(err) |
S = OPT O = 1163 T = 77.55 (out)(err) |
S = N/A O = 1279 T = TO (out)(err) |
S = N/A O = 1444 T = TO (out)(err) |
S = N/A O = 1451 T = TO (out)(err) |
S = N/A O = 1231 T = TO (out)(err) |
S = N/A O = 1538 T = TO (out)(err) |
S = N/A O = N/A T = 179.07 (out)(err) |
S = N/A O = N/A T = 864.94 (out)(err) |
s2v120c1500_8.wcnf | S = OPT O = 1097 T = 4.67 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1097 T = 10.02 (out)(err) |
S = N/A O = 1711 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1097 T = 16.75 (out)(err) |
S = N/A O = 1208 T = TO (out)(err) |
S = OPT O = 1097 T = 73.72 (out)(err) |
S = OPT O = 1097 T = 69.96 (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 = 856.45 (out)(err) |
S = OPT O = 1097 T = 4.67 (out)(err) |
S = N/A O = 1225 T = TO (out)(err) |
S = N/A O = 1451 T = TO (out)(err) |
S = N/A O = 1505 T = TO (out)(err) |
S = N/A O = 1143 T = TO (out)(err) |
S = N/A O = 1550 T = TO (out)(err) |
S = N/A O = N/A T = 178.86 (out)(err) |
S = N/A O = N/A T = 1007.89 (out)(err) |
s2v120c1600_1.wcnf | S = OPT O = 1190 T = 8.51 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1190 T = 8.51 (out)(err) |
S = N/A O = 1732 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1190 T = 29.55 (out)(err) |
S = N/A O = 1328 T = TO (out)(err) |
S = OPT O = 1190 T = 98.25 (out)(err) |
S = OPT O = 1190 T = 101.23 (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 = 1190 T = 1797.93 (out)(err) |
S = OPT O = 1190 T = 9.75 (out)(err) |
S = N/A O = 1332 T = TO (out)(err) |
S = N/A O = 1458 T = TO (out)(err) |
S = N/A O = 1595 T = TO (out)(err) |
S = N/A O = 1266 T = TO (out)(err) |
S = N/A O = 1807 T = TO (out)(err) |
S = N/A O = N/A T = 317.84 (out)(err) |
S = N/A O = N/A T = 907.96 (out)(err) |
s2v120c1600_2.wcnf | S = OPT O = 1227 T = 55.97 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1227 T = 74.18 (out)(err) |
S = N/A O = 1639 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1227 T = 191.93 (out)(err) |
S = N/A O = 1443 T = TO (out)(err) |
S = OPT O = 1227 T = 546.13 (out)(err) |
S = OPT O = 1227 T = 566.31 (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 = 1227 T = 1797.86 (out)(err) |
S = OPT O = 1227 T = 55.97 (out)(err) |
S = N/A O = 1332 T = TO (out)(err) |
S = N/A O = 1588 T = TO (out)(err) |
S = N/A O = 1630 T = TO (out)(err) |
S = N/A O = 1288 T = TO (out)(err) |
S = N/A O = 1720 T = TO (out)(err) |
S = N/A O = N/A T = 178.91 (out)(err) |
S = N/A O = N/A T = 1039.08 (out)(err) |
s2v120c1600_3.wcnf | S = OPT O = 1224 T = 57.08 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1224 T = 57.08 (out)(err) |
S = N/A O = 1509 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1224 T = 197.80 (out)(err) |
S = N/A O = 1286 T = TO (out)(err) |
S = OPT O = 1224 T = 594.28 (out)(err) |
S = OPT O = 1224 T = 603.57 (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 = 1274 T = 1797.81 (out)(err) |
S = OPT O = 1224 T = 59.25 (out)(err) |
S = N/A O = 1372 T = TO (out)(err) |
S = N/A O = 1585 T = TO (out)(err) |
S = N/A O = 1615 T = TO (out)(err) |
S = N/A O = 1348 T = TO (out)(err) |
S = N/A O = 1742 T = TO (out)(err) |
S = N/A O = N/A T = 178.96 (out)(err) |
S = N/A O = N/A T = 571.16 (out)(err) |
s2v120c1600_4.wcnf | S = OPT O = 1264 T = 150.53 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1264 T = 150.53 (out)(err) |
S = N/A O = 1544 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1264 T = 361.56 (out)(err) |
S = N/A O = 1349 T = TO (out)(err) |
S = OPT O = 1264 T = 1130.62 (out)(err) |
S = OPT O = 1264 T = 1124.24 (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 = 1299 T = 1797.77 (out)(err) |
S = OPT O = 1264 T = 153.72 (out)(err) |
S = N/A O = 1398 T = TO (out)(err) |
S = N/A O = 1633 T = TO (out)(err) |
S = N/A O = 1786 T = TO (out)(err) |
S = N/A O = 1331 T = TO (out)(err) |
S = N/A O = 1689 T = TO (out)(err) |
S = N/A O = N/A T = 179.05 (out)(err) |
S = N/A O = N/A T = 1755.95 (out)(err) |
s2v120c1600_5.wcnf | S = OPT O = 1252 T = 57.67 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1252 T = 66.28 (out)(err) |
S = N/A O = 1498 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1252 T = 200.19 (out)(err) |
S = N/A O = 1335 T = TO (out)(err) |
S = OPT O = 1252 T = 716.75 (out)(err) |
S = OPT O = 1252 T = 731.26 (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 = 1295 T = 1797.87 (out)(err) |
S = OPT O = 1252 T = 57.67 (out)(err) |
S = N/A O = 1367 T = TO (out)(err) |
S = N/A O = 1581 T = TO (out)(err) |
S = N/A O = 1715 T = TO (out)(err) |
S = N/A O = 1297 T = TO (out)(err) |
S = N/A O = 1586 T = TO (out)(err) |
S = N/A O = N/A T = 178.78 (out)(err) |
S = N/A O = N/A T = 808.28 (out)(err) |
s2v120c1600_6.wcnf | S = OPT O = 1246 T = 25.48 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1246 T = 26.73 (out)(err) |
S = N/A O = 1711 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1246 T = 70.44 (out)(err) |
S = N/A O = 1358 T = TO (out)(err) |
S = OPT O = 1246 T = 354.44 (out)(err) |
S = OPT O = 1246 T = 368.85 (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 = 1262 T = 1797.85 (out)(err) |
S = OPT O = 1246 T = 25.48 (out)(err) |
S = N/A O = 1390 T = TO (out)(err) |
S = N/A O = 1560 T = TO (out)(err) |
S = N/A O = 1665 T = TO (out)(err) |
S = N/A O = 1308 T = TO (out)(err) |
S = N/A O = 1704 T = TO (out)(err) |
S = N/A O = N/A T = 178.94 (out)(err) |
S = N/A O = N/A T = 1482.52 (out)(err) |
s2v120c1600_7.wcnf | S = OPT O = 1159 T = 7.69 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1159 T = 7.69 (out)(err) |
S = N/A O = 1624 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1159 T = 15.38 (out)(err) |
S = N/A O = 1248 T = TO (out)(err) |
S = OPT O = 1159 T = 47.40 (out)(err) |
S = OPT O = 1159 T = 46.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 = 1159 T = 1056.69 (out)(err) |
S = OPT O = 1159 T = 8.18 (out)(err) |
S = N/A O = 1307 T = TO (out)(err) |
S = N/A O = 1402 T = TO (out)(err) |
S = N/A O = 1511 T = TO (out)(err) |
S = N/A O = 1167 T = TO (out)(err) |
S = N/A O = 1636 T = TO (out)(err) |
S = N/A O = N/A T = 178.91 (out)(err) |
S = N/A O = N/A T = 801.72 (out)(err) |
s2v120c1600_8.wcnf | S = OPT O = 1150 T = 3.57 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1150 T = 12.43 (out)(err) |
S = N/A O = 1399 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1150 T = 29.45 (out)(err) |
S = N/A O = 1344 T = TO (out)(err) |
S = OPT O = 1150 T = 101.00 (out)(err) |
S = OPT O = 1150 T = 104.52 (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 = 1150 T = 1797.83 (out)(err) |
S = OPT O = 1150 T = 3.57 (out)(err) |
S = N/A O = 1277 T = TO (out)(err) |
S = N/A O = 1494 T = TO (out)(err) |
S = N/A O = 1555 T = TO (out)(err) |
S = N/A O = 1214 T = TO (out)(err) |
S = N/A O = 1834 T = TO (out)(err) |
S = N/A O = N/A T = 182.26 (out)(err) |
S = N/A O = N/A T = 1101.56 (out)(err) |
s2v140c1200_1.wcnf | S = OPT O = 780 T = 33.12 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 780 T = 58.17 (out)(err) |
S = N/A O = 1067 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 780 T = 67.00 (out)(err) |
S = N/A O = 899 T = TO (out)(err) |
S = OPT O = 780 T = 195.11 (out)(err) |
S = OPT O = 780 T = 207.07 (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 = 789 T = 1797.81 (out)(err) |
S = OPT O = 780 T = 33.12 (out)(err) |
S = N/A O = 863 T = TO (out)(err) |
S = N/A O = 1051 T = TO (out)(err) |
S = N/A O = 1035 T = TO (out)(err) |
S = N/A O = 799 T = TO (out)(err) |
S = N/A O = 1006 T = TO (out)(err) |
S = N/A O = N/A T = 232.00 (out)(err) |
S = N/A O = N/A T = 1255.43 (out)(err) |
s2v140c1200_2.wcnf | S = OPT O = 733 T = 18.05 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 733 T = 20.87 (out)(err) |
S = N/A O = 957 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 733 T = 34.49 (out)(err) |
S = N/A O = 816 T = TO (out)(err) |
S = OPT O = 733 T = 80.82 (out)(err) |
S = OPT O = 733 T = 84.78 (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 = 733 T = 1797.87 (out)(err) |
S = OPT O = 733 T = 18.05 (out)(err) |
S = N/A O = 821 T = TO (out)(err) |
S = N/A O = 966 T = TO (out)(err) |
S = N/A O = 1004 T = TO (out)(err) |
S = N/A O = 739 T = TO (out)(err) |
S = N/A O = 1061 T = TO (out)(err) |
S = N/A O = N/A T = 204.98 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1200_3.wcnf | S = OPT O = 741 T = 13.12 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 741 T = 45.28 (out)(err) |
S = N/A O = 940 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 741 T = 50.67 (out)(err) |
S = N/A O = 854 T = TO (out)(err) |
S = OPT O = 741 T = 142.58 (out)(err) |
S = OPT O = 741 T = 141.36 (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 = 758 T = 1797.84 (out)(err) |
S = OPT O = 741 T = 13.12 (out)(err) |
S = N/A O = 796 T = TO (out)(err) |
S = N/A O = 951 T = TO (out)(err) |
S = N/A O = 1018 T = TO (out)(err) |
S = N/A O = 758 T = TO (out)(err) |
S = N/A O = 1044 T = TO (out)(err) |
S = N/A O = N/A T = 178.88 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1200_4.wcnf | S = OPT O = 667 T = 1.52 |
S = OPT O = 667 T = 1480.46 (out)(err) |
S = OPT O = 667 T = 2.62 (out)(err) |
S = N/A O = 948 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 667 T = 4.12 (out)(err) |
S = N/A O = 769 T = TO (out)(err) |
S = OPT O = 667 T = 10.79 (out)(err) |
S = OPT O = 667 T = 10.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 = 667 T = 127.96 (out)(err) |
S = OPT O = 667 T = 1.52 (out)(err) |
S = N/A O = 746 T = TO (out)(err) |
S = N/A O = 952 T = TO (out)(err) |
S = N/A O = 933 T = TO (out)(err) |
S = N/A O = 671 T = TO (out)(err) |
S = N/A O = 1093 T = TO (out)(err) |
S = N/A O = N/A T = 234.77 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1200_5.wcnf | S = OPT O = 714 T = 4.90 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 714 T = 12.18 (out)(err) |
S = N/A O = 932 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 714 T = 13.77 (out)(err) |
S = N/A O = 757 T = TO (out)(err) |
S = OPT O = 714 T = 42.91 (out)(err) |
S = OPT O = 714 T = 31.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 = 714 T = 490.77 (out)(err) |
S = OPT O = 714 T = 4.90 (out)(err) |
S = N/A O = 804 T = TO (out)(err) |
S = N/A O = 1023 T = TO (out)(err) |
S = N/A O = 969 T = TO (out)(err) |
S = N/A O = 721 T = TO (out)(err) |
S = N/A O = 997 T = TO (out)(err) |
S = N/A O = N/A T = 236.20 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1200_6.wcnf | S = OPT O = 803 T = 52.18 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 803 T = 69.73 (out)(err) |
S = N/A O = 1202 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 803 T = 111.13 (out)(err) |
S = N/A O = 909 T = TO (out)(err) |
S = OPT O = 803 T = 310.87 (out)(err) |
S = OPT O = 803 T = 315.45 (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 = 803 T = 1797.79 (out)(err) |
S = OPT O = 803 T = 52.18 (out)(err) |
S = N/A O = 899 T = TO (out)(err) |
S = N/A O = 1084 T = TO (out)(err) |
S = N/A O = 1096 T = TO (out)(err) |
S = N/A O = 811 T = TO (out)(err) |
S = N/A O = 1460 T = TO (out)(err) |
S = N/A O = N/A T = 178.88 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1200_7.wcnf | S = OPT O = 774 T = 64.09 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 774 T = 112.17 (out)(err) |
S = N/A O = 962 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 774 T = 128.19 (out)(err) |
S = N/A O = 800 T = TO (out)(err) |
S = OPT O = 774 T = 305.12 (out)(err) |
S = OPT O = 774 T = 312.37 (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 = 778 T = 1797.82 (out)(err) |
S = OPT O = 774 T = 64.09 (out)(err) |
S = N/A O = 839 T = TO (out)(err) |
S = N/A O = 1006 T = TO (out)(err) |
S = N/A O = 1051 T = TO (out)(err) |
S = N/A O = 792 T = TO (out)(err) |
S = N/A O = 1001 T = TO (out)(err) |
S = N/A O = N/A T = 204.73 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1200_8.wcnf | S = OPT O = 745 T = 28.35 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 745 T = 57.12 (out)(err) |
S = N/A O = 984 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 745 T = 89.17 (out)(err) |
S = N/A O = 793 T = TO (out)(err) |
S = OPT O = 745 T = 152.47 (out)(err) |
S = OPT O = 745 T = 152.26 (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 = 1698.22 (out)(err) |
S = OPT O = 745 T = 28.35 (out)(err) |
S = N/A O = 810 T = TO (out)(err) |
S = N/A O = 1017 T = TO (out)(err) |
S = N/A O = 994 T = TO (out)(err) |
S = N/A O = 754 T = TO (out)(err) |
S = N/A O = 1057 T = TO (out)(err) |
S = N/A O = N/A T = 178.96 (out)(err) |
S = N/A O = N/A T = 1285.43 (out)(err) |
s2v140c1300_1.wcnf | S = OPT O = 846 T = 20.05 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 846 T = 33.03 (out)(err) |
S = N/A O = 1142 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 846 T = 61.85 (out)(err) |
S = N/A O = 980 T = TO (out)(err) |
S = OPT O = 846 T = 130.95 (out)(err) |
S = OPT O = 846 T = 128.36 (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 = 846 T = 1797.80 (out)(err) |
S = OPT O = 846 T = 20.05 (out)(err) |
S = N/A O = 917 T = TO (out)(err) |
S = N/A O = 1179 T = TO (out)(err) |
S = N/A O = 1379 T = TO (out)(err) |
S = N/A O = 869 T = TO (out)(err) |
S = N/A O = 1163 T = TO (out)(err) |
S = N/A O = N/A T = 204.81 (out)(err) |
S = N/A O = N/A T = 1219.62 (out)(err) |
s2v140c1300_2.wcnf | S = OPT O = 774 T = 2.91 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 774 T = 4.67 (out)(err) |
S = N/A O = 1046 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 774 T = 5.35 (out)(err) |
S = N/A O = 819 T = TO (out)(err) |
S = OPT O = 774 T = 17.88 (out)(err) |
S = OPT O = 774 T = 19.25 (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 = 483.01 (out)(err) |
S = OPT O = 774 T = 2.91 (out)(err) |
S = N/A O = 855 T = TO (out)(err) |
S = N/A O = 986 T = TO (out)(err) |
S = N/A O = 1043 T = TO (out)(err) |
S = N/A O = 792 T = TO (out)(err) |
S = N/A O = 1234 T = TO (out)(err) |
S = N/A O = N/A T = 357.68 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1300_3.wcnf | S = OPT O = 832 T = 17.15 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 832 T = 30.26 (out)(err) |
S = N/A O = 1158 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 832 T = 81.29 (out)(err) |
S = N/A O = 959 T = TO (out)(err) |
S = OPT O = 832 T = 210.44 (out)(err) |
S = OPT O = 832 T = 220.81 (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 = 832 T = 1797.85 (out)(err) |
S = OPT O = 832 T = 17.15 (out)(err) |
S = N/A O = 921 T = TO (out)(err) |
S = N/A O = 1139 T = TO (out)(err) |
S = N/A O = 1108 T = TO (out)(err) |
S = N/A O = 853 T = TO (out)(err) |
S = N/A O = 1060 T = TO (out)(err) |
S = N/A O = N/A T = 212.81 (out)(err) |
S = N/A O = N/A T = 1753.71 (out)(err) |
s2v140c1300_4.wcnf | S = OPT O = 871 T = 80.00 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 871 T = 153.03 (out)(err) |
S = N/A O = 1219 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 871 T = 175.60 (out)(err) |
S = N/A O = 920 T = TO (out)(err) |
S = OPT O = 871 T = 438.81 (out)(err) |
S = OPT O = 871 T = 450.76 (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 = 875 T = 1797.90 (out)(err) |
S = OPT O = 871 T = 80.00 (out)(err) |
S = N/A O = 968 T = TO (out)(err) |
S = N/A O = 1171 T = TO (out)(err) |
S = N/A O = 1229 T = TO (out)(err) |
S = N/A O = 895 T = TO (out)(err) |
S = N/A O = 1240 T = TO (out)(err) |
S = N/A O = N/A T = 178.98 (out)(err) |
S = N/A O = N/A T = 1397.28 (out)(err) |
s2v140c1300_5.wcnf | S = OPT O = 844 T = 23.86 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 844 T = 33.15 (out)(err) |
S = N/A O = 1168 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 844 T = 57.07 (out)(err) |
S = N/A O = 863 T = TO (out)(err) |
S = OPT O = 844 T = 147.13 (out)(err) |
S = OPT O = 844 T = 146.88 (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 = 853 T = 1797.90 (out)(err) |
S = OPT O = 844 T = 23.86 (out)(err) |
S = N/A O = 931 T = TO (out)(err) |
S = N/A O = 1080 T = TO (out)(err) |
S = N/A O = 1054 T = TO (out)(err) |
S = N/A O = 863 T = TO (out)(err) |
S = N/A O = 1230 T = TO (out)(err) |
S = N/A O = N/A T = 178.91 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1300_6.wcnf | S = OPT O = 884 T = 130.51 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 884 T = 259.29 (out)(err) |
S = N/A O = 1078 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 884 T = 370.84 (out)(err) |
S = N/A O = 990 T = TO (out)(err) |
S = OPT O = 884 T = 1025.23 (out)(err) |
S = OPT O = 884 T = 1022.21 (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 = 894 T = 1797.90 (out)(err) |
S = OPT O = 884 T = 130.51 (out)(err) |
S = N/A O = 988 T = TO (out)(err) |
S = N/A O = 1196 T = TO (out)(err) |
S = N/A O = 1185 T = TO (out)(err) |
S = N/A O = 908 T = TO (out)(err) |
S = N/A O = 1275 T = TO (out)(err) |
S = N/A O = N/A T = 326.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1300_7.wcnf | S = OPT O = 874 T = 47.96 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 874 T = 96.24 (out)(err) |
S = N/A O = 1070 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 874 T = 116.96 (out)(err) |
S = N/A O = 908 T = TO (out)(err) |
S = OPT O = 874 T = 290.58 (out)(err) |
S = OPT O = 874 T = 286.33 (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 = 898 T = 1797.85 (out)(err) |
S = OPT O = 874 T = 47.96 (out)(err) |
S = N/A O = 982 T = TO (out)(err) |
S = N/A O = 1149 T = TO (out)(err) |
S = N/A O = 1179 T = TO (out)(err) |
S = N/A O = 914 T = TO (out)(err) |
S = N/A O = 1159 T = TO (out)(err) |
S = N/A O = N/A T = 209.01 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1300_8.wcnf | S = OPT O = 812 T = 34.65 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 812 T = 55.65 (out)(err) |
S = N/A O = 1016 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 812 T = 94.02 (out)(err) |
S = N/A O = 981 T = TO (out)(err) |
S = OPT O = 812 T = 234.76 (out)(err) |
S = OPT O = 812 T = 232.85 (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 = 812 T = 1797.86 (out)(err) |
S = OPT O = 812 T = 34.65 (out)(err) |
S = N/A O = 892 T = TO (out)(err) |
S = N/A O = 1160 T = TO (out)(err) |
S = N/A O = 1076 T = TO (out)(err) |
S = N/A O = 832 T = TO (out)(err) |
S = N/A O = 1139 T = TO (out)(err) |
S = N/A O = N/A T = 204.88 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_1.wcnf | S = OPT O = 926 T = 44.88 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 926 T = 60.82 (out)(err) |
S = N/A O = 1230 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 926 T = 162.87 (out)(err) |
S = N/A O = 986 T = TO (out)(err) |
S = OPT O = 926 T = 407.56 (out)(err) |
S = OPT O = 926 T = 428.76 (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 = 926 T = 1797.88 (out)(err) |
S = OPT O = 926 T = 44.88 (out)(err) |
S = N/A O = 1026 T = TO (out)(err) |
S = N/A O = 1244 T = TO (out)(err) |
S = N/A O = 1204 T = TO (out)(err) |
S = N/A O = 970 T = TO (out)(err) |
S = N/A O = 1348 T = TO (out)(err) |
S = N/A O = N/A T = 178.78 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1400_2.wcnf | S = OPT O = 879 T = 15.02 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 879 T = 21.58 (out)(err) |
S = N/A O = 1243 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 879 T = 23.85 (out)(err) |
S = N/A O = 1054 T = TO (out)(err) |
S = OPT O = 879 T = 75.38 (out)(err) |
S = OPT O = 879 T = 73.60 (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 = 1654.56 (out)(err) |
S = OPT O = 879 T = 15.02 (out)(err) |
S = N/A O = 963 T = TO (out)(err) |
S = N/A O = 1123 T = TO (out)(err) |
S = N/A O = 1118 T = TO (out)(err) |
S = N/A O = 904 T = TO (out)(err) |
S = N/A O = 1155 T = TO (out)(err) |
S = N/A O = N/A T = 178.85 (out)(err) |
S = N/A O = N/A T = 1723.75 (out)(err) |
s2v140c1400_3.wcnf | S = OPT O = 936 T = 46.88 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 936 T = 53.79 (out)(err) |
S = N/A O = 1354 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 936 T = 95.76 (out)(err) |
S = N/A O = 1058 T = TO (out)(err) |
S = OPT O = 936 T = 244.96 (out)(err) |
S = OPT O = 936 T = 248.18 (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 = 936 T = 1797.83 (out)(err) |
S = OPT O = 936 T = 46.88 (out)(err) |
S = N/A O = 1058 T = TO (out)(err) |
S = N/A O = 1226 T = TO (out)(err) |
S = N/A O = 1286 T = TO (out)(err) |
S = N/A O = 974 T = TO (out)(err) |
S = N/A O = 1393 T = TO (out)(err) |
S = N/A O = N/A T = 316.11 (out)(err) |
S = N/A O = N/A T = 1377.16 (out)(err) |
s2v140c1400_4.wcnf | S = OPT O = 932 T = 26.01 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 932 T = 59.72 (out)(err) |
S = N/A O = 1227 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 932 T = 58.95 (out)(err) |
S = N/A O = 1136 T = TO (out)(err) |
S = OPT O = 932 T = 162.11 (out)(err) |
S = OPT O = 932 T = 157.84 (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 = 938 T = 1797.87 (out)(err) |
S = OPT O = 932 T = 26.01 (out)(err) |
S = N/A O = 1066 T = TO (out)(err) |
S = N/A O = 1202 T = TO (out)(err) |
S = N/A O = 1286 T = TO (out)(err) |
S = N/A O = 939 T = TO (out)(err) |
S = N/A O = 1332 T = TO (out)(err) |
S = N/A O = N/A T = 204.82 (out)(err) |
S = N/A O = N/A T = 1139.57 (out)(err) |
s2v140c1400_5.wcnf | S = OPT O = 968 T = 52.46 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 968 T = 102.10 (out)(err) |
S = N/A O = 1388 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 968 T = 185.23 (out)(err) |
S = N/A O = 1036 T = TO (out)(err) |
S = OPT O = 968 T = 517.51 (out)(err) |
S = OPT O = 968 T = 515.99 (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 = 982 T = 1797.88 (out)(err) |
S = OPT O = 968 T = 52.46 (out)(err) |
S = N/A O = 1080 T = TO (out)(err) |
S = N/A O = 1251 T = TO (out)(err) |
S = N/A O = 1218 T = TO (out)(err) |
S = N/A O = 1004 T = TO (out)(err) |
S = N/A O = 1470 T = TO (out)(err) |
S = N/A O = N/A T = 178.91 (out)(err) |
S = N/A O = N/A T = 1268.03 (out)(err) |
s2v140c1400_6.wcnf | S = OPT O = 967 T = 181.52 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 967 T = 238.11 (out)(err) |
S = N/A O = 1305 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 967 T = 387.03 (out)(err) |
S = N/A O = 1195 T = TO (out)(err) |
S = OPT O = 967 T = 941.22 (out)(err) |
S = OPT O = 967 T = 1041.86 (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 = 999 T = 1797.90 (out)(err) |
S = OPT O = 967 T = 181.52 (out)(err) |
S = N/A O = 1062 T = TO (out)(err) |
S = N/A O = 1270 T = TO (out)(err) |
S = N/A O = 1186 T = TO (out)(err) |
S = N/A O = 1015 T = TO (out)(err) |
S = N/A O = 1480 T = TO (out)(err) |
S = N/A O = N/A T = 178.79 (out)(err) |
S = N/A O = N/A T = 1288.46 (out)(err) |
s2v140c1400_7.wcnf | S = OPT O = 923 T = 13.41 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 923 T = 43.52 (out)(err) |
S = N/A O = 1246 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 923 T = 41.66 (out)(err) |
S = N/A O = 1032 T = TO (out)(err) |
S = OPT O = 923 T = 104.52 (out)(err) |
S = OPT O = 923 T = 103.06 (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 = 982 T = 1797.80 (out)(err) |
S = OPT O = 923 T = 13.41 (out)(err) |
S = N/A O = 1021 T = TO (out)(err) |
S = N/A O = 1182 T = TO (out)(err) |
S = N/A O = 1253 T = TO (out)(err) |
S = N/A O = 959 T = TO (out)(err) |
S = N/A O = 1391 T = TO (out)(err) |
S = N/A O = N/A T = 178.96 (out)(err) |
S = N/A O = N/A T = 1605.72 (out)(err) |
s2v140c1400_8.wcnf | S = OPT O = 957 T = 61.67 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 957 T = 172.87 (out)(err) |
S = N/A O = 1233 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 957 T = 329.42 (out)(err) |
S = N/A O = 1073 T = TO (out)(err) |
S = OPT O = 957 T = 972.66 (out)(err) |
S = OPT O = 957 T = 869.75 (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 = 970 T = 1797.88 (out)(err) |
S = OPT O = 957 T = 61.67 (out)(err) |
S = N/A O = 1067 T = TO (out)(err) |
S = N/A O = 1213 T = TO (out)(err) |
S = N/A O = 1288 T = TO (out)(err) |
S = N/A O = 1011 T = TO (out)(err) |
S = N/A O = 1290 T = TO (out)(err) |
S = N/A O = N/A T = 179.10 (out)(err) |
S = N/A O = N/A T = 1120.97 (out)(err) |
s2v140c1500_1.wcnf | S = OPT O = 986 T = 18.89 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 986 T = 79.15 (out)(err) |
S = N/A O = 1252 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 986 T = 78.33 (out)(err) |
S = N/A O = 1081 T = TO (out)(err) |
S = OPT O = 986 T = 226.96 (out)(err) |
S = OPT O = 986 T = 220.13 (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 = 994 T = 1797.91 (out)(err) |
S = OPT O = 986 T = 18.89 (out)(err) |
S = N/A O = 1104 T = TO (out)(err) |
S = N/A O = 1241 T = TO (out)(err) |
S = N/A O = 1385 T = TO (out)(err) |
S = N/A O = 1034 T = TO (out)(err) |
S = N/A O = 1645 T = TO (out)(err) |
S = N/A O = N/A T = 179.19 (out)(err) |
S = N/A O = N/A T = 931.91 (out)(err) |
s2v140c1500_2.wcnf | S = OPT O = 998 T = 32.93 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 998 T = 75.22 (out)(err) |
S = N/A O = 1432 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 998 T = 118.86 (out)(err) |
S = N/A O = 1184 T = TO (out)(err) |
S = OPT O = 998 T = 306.13 (out)(err) |
S = OPT O = 998 T = 316.77 (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 = 1018 T = 1797.89 (out)(err) |
S = OPT O = 998 T = 32.93 (out)(err) |
S = N/A O = 1090 T = TO (out)(err) |
S = N/A O = 1271 T = TO (out)(err) |
S = N/A O = 1300 T = TO (out)(err) |
S = N/A O = 1044 T = TO (out)(err) |
S = N/A O = 1576 T = TO (out)(err) |
S = N/A O = N/A T = 178.78 (out)(err) |
S = N/A O = N/A T = 1107.24 (out)(err) |
s2v140c1500_3.wcnf | S = OPT O = 1073 T = 183.98 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1073 T = 242.93 (out)(err) |
S = N/A O = 1473 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1073 T = 694.87 (out)(err) |
S = N/A O = 1234 T = TO (out)(err) |
S = OPT O = 1073 T = 1141.40 (out)(err) |
S = OPT O = 1073 T = 1158.78 (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 = 1078 T = 1797.91 (out)(err) |
S = OPT O = 1073 T = 183.98 (out)(err) |
S = N/A O = 1191 T = TO (out)(err) |
S = N/A O = 1373 T = TO (out)(err) |
S = N/A O = 1402 T = TO (out)(err) |
S = N/A O = 1125 T = TO (out)(err) |
S = N/A O = 1543 T = TO (out)(err) |
S = N/A O = N/A T = 178.88 (out)(err) |
S = N/A O = N/A T = 909.38 (out)(err) |
s2v140c1500_4.wcnf | S = OPT O = 1047 T = 154.64 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1047 T = 352.74 (out)(err) |
S = N/A O = 1299 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1047 T = 972.79 (out)(err) |
S = N/A O = 1151 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 = N/A O = 1090 T = 1797.89 (out)(err) |
S = OPT O = 1047 T = 154.64 (out)(err) |
S = N/A O = 1185 T = TO (out)(err) |
S = N/A O = 1411 T = TO (out)(err) |
S = N/A O = 1454 T = TO (out)(err) |
S = N/A O = 1097 T = TO (out)(err) |
S = N/A O = 1572 T = TO (out)(err) |
S = N/A O = N/A T = 178.80 (out)(err) |
S = N/A O = N/A T = 1435.74 (out)(err) |
s2v140c1500_5.wcnf | S = OPT O = 1058 T = 90.19 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1058 T = 321.22 (out)(err) |
S = N/A O = 1469 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1058 T = 662.66 (out)(err) |
S = N/A O = 1254 T = TO (out)(err) |
S = N/A O = 1058 T = TO (out)(err) |
S = N/A O = 1058 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 = 1122 T = 1797.85 (out)(err) |
S = OPT O = 1058 T = 90.19 (out)(err) |
S = N/A O = 1185 T = TO (out)(err) |
S = N/A O = 1401 T = TO (out)(err) |
S = N/A O = 1508 T = TO (out)(err) |
S = N/A O = 1145 T = TO (out)(err) |
S = N/A O = 1493 T = TO (out)(err) |
S = N/A O = N/A T = 178.95 (out)(err) |
S = N/A O = N/A T = 1207.27 (out)(err) |
s2v140c1500_6.wcnf | S = OPT O = 1102 T = 298.53 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1102 T = 350.16 (out)(err) |
S = N/A O = 1506 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1102 T = 640.37 (out)(err) |
S = N/A O = 1234 T = TO (out)(err) |
S = OPT O = 1102 T = 1779.48 (out)(err) |
S = OPT O = 1102 T = 1767.93 (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 = 1102 T = 1797.88 (out)(err) |
S = OPT O = 1102 T = 298.53 (out)(err) |
S = N/A O = 1220 T = TO (out)(err) |
S = N/A O = 1389 T = TO (out)(err) |
S = N/A O = 1549 T = TO (out)(err) |
S = N/A O = 1223 T = TO (out)(err) |
S = N/A O = 1581 T = TO (out)(err) |
S = N/A O = N/A T = 178.85 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1500_7.wcnf | S = OPT O = 1010 T = 19.02 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1010 T = 27.19 (out)(err) |
S = N/A O = 1357 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1010 T = 60.98 (out)(err) |
S = N/A O = 1081 T = TO (out)(err) |
S = OPT O = 1010 T = 171.48 (out)(err) |
S = OPT O = 1010 T = 161.79 (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 = 1035 T = 1797.88 (out)(err) |
S = OPT O = 1010 T = 19.02 (out)(err) |
S = N/A O = 1130 T = TO (out)(err) |
S = N/A O = 1208 T = TO (out)(err) |
S = N/A O = 1285 T = TO (out)(err) |
S = N/A O = 1046 T = TO (out)(err) |
S = N/A O = 1381 T = TO (out)(err) |
S = N/A O = N/A T = 179.01 (out)(err) |
S = N/A O = N/A T = 1757.05 (out)(err) |
s2v140c1500_8.wcnf | S = OPT O = 1045 T = 59.40 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1045 T = 107.06 (out)(err) |
S = N/A O = 1521 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1045 T = 128.07 (out)(err) |
S = N/A O = 1167 T = TO (out)(err) |
S = OPT O = 1045 T = 416.79 (out)(err) |
S = OPT O = 1045 T = 420.06 (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 = 1068 T = 1797.91 (out)(err) |
S = OPT O = 1045 T = 59.40 (out)(err) |
S = N/A O = 1172 T = TO (out)(err) |
S = N/A O = 1345 T = TO (out)(err) |
S = N/A O = 1428 T = TO (out)(err) |
S = N/A O = 1110 T = TO (out)(err) |
S = N/A O = 1481 T = TO (out)(err) |
S = N/A O = N/A T = 179.02 (out)(err) |
S = N/A O = N/A T = 1084.79 (out)(err) |
s2v140c1600_1.wcnf | S = OPT O = 1143 T = 43.50 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1143 T = 54.76 (out)(err) |
S = N/A O = 1584 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1143 T = 91.11 (out)(err) |
S = N/A O = 1314 T = TO (out)(err) |
S = OPT O = 1143 T = 265.67 (out)(err) |
S = OPT O = 1143 T = 273.44 (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 = 1144 T = 1797.89 (out)(err) |
S = OPT O = 1143 T = 43.50 (out)(err) |
S = N/A O = 1255 T = TO (out)(err) |
S = N/A O = 1456 T = TO (out)(err) |
S = N/A O = 1460 T = TO (out)(err) |
S = N/A O = 1196 T = TO (out)(err) |
S = N/A O = 1650 T = TO (out)(err) |
S = N/A O = N/A T = 179.00 (out)(err) |
S = N/A O = N/A T = 1584.91 (out)(err) |
s2v140c1600_2.wcnf | S = OPT O = 1140 T = 36.20 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1140 T = 44.38 (out)(err) |
S = N/A O = 1435 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1140 T = 107.17 (out)(err) |
S = N/A O = 1248 T = TO (out)(err) |
S = OPT O = 1140 T = 287.44 (out)(err) |
S = OPT O = 1140 T = 283.38 (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 = 1145 T = 1797.93 (out)(err) |
S = OPT O = 1140 T = 36.20 (out)(err) |
S = N/A O = 1258 T = TO (out)(err) |
S = N/A O = 1706 T = TO (out)(err) |
S = N/A O = 1546 T = TO (out)(err) |
S = N/A O = 1193 T = TO (out)(err) |
S = N/A O = 1466 T = TO (out)(err) |
S = N/A O = N/A T = 178.82 (out)(err) |
S = N/A O = N/A T = 1044.37 (out)(err) |
s2v140c1600_3.wcnf | S = OPT O = 1079 T = 30.63 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1079 T = 33.67 (out)(err) |
S = N/A O = 1356 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1079 T = 61.40 (out)(err) |
S = N/A O = 1371 T = TO (out)(err) |
S = OPT O = 1079 T = 179.54 (out)(err) |
S = OPT O = 1079 T = 183.48 (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 = 1079 T = 1797.94 (out)(err) |
S = OPT O = 1079 T = 30.63 (out)(err) |
S = N/A O = 1157 T = TO (out)(err) |
S = N/A O = 1403 T = TO (out)(err) |
S = N/A O = 1423 T = TO (out)(err) |
S = N/A O = 1140 T = TO (out)(err) |
S = N/A O = 1578 T = TO (out)(err) |
S = N/A O = N/A T = 340.10 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
s2v140c1600_4.wcnf | S = OPT O = 1157 T = 94.90 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1157 T = 98.49 (out)(err) |
S = N/A O = 1639 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1157 T = 286.75 (out)(err) |
S = N/A O = 1278 T = TO (out)(err) |
S = OPT O = 1157 T = 767.09 (out)(err) |
S = OPT O = 1157 T = 766.18 (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 = 1171 T = 1797.86 (out)(err) |
S = OPT O = 1157 T = 94.90 (out)(err) |
S = N/A O = 1300 T = TO (out)(err) |
S = N/A O = 1453 T = TO (out)(err) |
S = N/A O = 1653 T = TO (out)(err) |
S = N/A O = 1195 T = TO (out)(err) |
S = N/A O = 1702 T = TO (out)(err) |
S = N/A O = N/A T = 178.93 (out)(err) |
S = N/A O = N/A T = 679.56 (out)(err) |
s2v140c1600_5.wcnf | S = OPT O = 1119 T = 89.04 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1119 T = 158.98 (out)(err) |
S = N/A O = 1484 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1119 T = 294.29 (out)(err) |
S = N/A O = 1252 T = TO (out)(err) |
S = OPT O = 1119 T = 991.31 (out)(err) |
S = OPT O = 1119 T = 1012.71 (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 = 1146 T = 1797.86 (out)(err) |
S = OPT O = 1119 T = 89.04 (out)(err) |
S = N/A O = 1281 T = TO (out)(err) |
S = N/A O = 1560 T = TO (out)(err) |
S = N/A O = 1425 T = TO (out)(err) |
S = N/A O = 1196 T = TO (out)(err) |
S = N/A O = 1601 T = TO (out)(err) |
S = N/A O = N/A T = 178.89 (out)(err) |
S = N/A O = N/A T = 673.41 (out)(err) |
s2v140c1600_6.wcnf | S = OPT O = 1212 T = 170.16 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1212 T = 265.93 (out)(err) |
S = N/A O = 1582 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1212 T = 532.56 (out)(err) |
S = N/A O = 1424 T = TO (out)(err) |
S = OPT O = 1212 T = 1321.56 (out)(err) |
S = OPT O = 1212 T = 1341.55 (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 = 1212 T = 1797.86 (out)(err) |
S = OPT O = 1212 T = 170.16 (out)(err) |
S = N/A O = 1328 T = TO (out)(err) |
S = N/A O = 1491 T = TO (out)(err) |
S = N/A O = 1646 T = TO (out)(err) |
S = N/A O = 1300 T = TO (out)(err) |
S = N/A O = 1725 T = TO (out)(err) |
S = N/A O = N/A T = 179.00 (out)(err) |
S = N/A O = N/A T = 721.20 (out)(err) |
s2v140c1600_7.wcnf | S = OPT O = 1150 T = 95.03 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1150 T = 162.54 (out)(err) |
S = N/A O = 1616 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1150 T = 436.01 (out)(err) |
S = N/A O = 1355 T = TO (out)(err) |
S = OPT O = 1150 T = 1025.08 (out)(err) |
S = OPT O = 1150 T = 1122.62 (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 = 1218 T = 1797.82 (out)(err) |
S = OPT O = 1150 T = 95.03 (out)(err) |
S = N/A O = 1291 T = TO (out)(err) |
S = N/A O = 1395 T = TO (out)(err) |
S = N/A O = 1422 T = TO (out)(err) |
S = N/A O = 1190 T = TO (out)(err) |
S = N/A O = 1644 T = TO (out)(err) |
S = N/A O = N/A T = 178.65 (out)(err) |
S = N/A O = N/A T = 1005.62 (out)(err) |
s2v140c1600_8.wcnf | S = OPT O = 1180 T = 72.10 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1180 T = 102.79 (out)(err) |
S = N/A O = 1474 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1180 T = 226.95 (out)(err) |
S = N/A O = 1295 T = TO (out)(err) |
S = OPT O = 1180 T = 640.14 (out)(err) |
S = OPT O = 1180 T = 641.17 (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 = 1226 T = 1797.84 (out)(err) |
S = OPT O = 1180 T = 72.10 (out)(err) |
S = N/A O = 1324 T = TO (out)(err) |
S = N/A O = 1416 T = TO (out)(err) |
S = N/A O = 1590 T = TO (out)(err) |
S = N/A O = 1243 T = TO (out)(err) |
S = N/A O = 1589 T = TO (out)(err) |
S = N/A O = N/A T = 180.43 (out)(err) |
S = N/A O = N/A T = 666.60 (out)(err) |
file_rwms_wcnf_L3_V70_C1000_0.wcnf | S = OPT O = 198 T = 143.40 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 198 T = 143.40 (out)(err) |
S = N/A O = 318 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 198 T = 195.52 (out)(err) |
S = N/A O = 308 T = TO (out)(err) |
S = OPT O = 198 T = 549.69 (out)(err) |
S = OPT O = 198 T = 551.30 (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 = 208 T = 1797.47 (out)(err) |
S = OPT O = 198 T = 196.56 (out)(err) |
S = N/A O = 237 T = TO (out)(err) |
S = N/A O = 421 T = TO (out)(err) |
S = N/A O = 495 T = TO (out)(err) |
S = N/A O = 213 T = TO (out)(err) |
S = N/A O = 470 T = TO (out)(err) |
S = N/A O = N/A T = 614.43 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C1000_1.wcnf | S = OPT O = 212 T = 92.21 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 212 T = 92.21 (out)(err) |
S = N/A O = 333 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 212 T = 111.20 (out)(err) |
S = N/A O = 256 T = TO (out)(err) |
S = OPT O = 212 T = 295.18 (out)(err) |
S = OPT O = 212 T = 300.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 = 212 T = 1375.67 (out)(err) |
S = OPT O = 212 T = 154.66 (out)(err) |
S = N/A O = 247 T = TO (out)(err) |
S = N/A O = 455 T = TO (out)(err) |
S = N/A O = 450 T = TO (out)(err) |
S = N/A O = 227 T = TO (out)(err) |
S = N/A O = 497 T = TO (out)(err) |
S = N/A O = N/A T = 414.37 (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 = 128.49 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 211 T = 128.49 (out)(err) |
S = N/A O = 290 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 211 T = 162.87 (out)(err) |
S = N/A O = 230 T = TO (out)(err) |
S = OPT O = 211 T = 432.74 (out)(err) |
S = OPT O = 211 T = 435.94 (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 = 211 T = 1797.57 (out)(err) |
S = OPT O = 211 T = 270.83 (out)(err) |
S = N/A O = 247 T = TO (out)(err) |
S = N/A O = 476 T = TO (out)(err) |
S = N/A O = 452 T = TO (out)(err) |
S = N/A O = 215 T = TO (out)(err) |
S = N/A O = 354 T = TO (out)(err) |
S = N/A O = N/A T = 613.88 (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 = 177.70 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 229 T = 177.70 (out)(err) |
S = N/A O = 321 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 229 T = 222.32 (out)(err) |
S = N/A O = 250 T = TO (out)(err) |
S = OPT O = 229 T = 600.85 (out)(err) |
S = OPT O = 229 T = 609.93 (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 = 229 T = 1797.30 (out)(err) |
S = OPT O = 229 T = 312.20 (out)(err) |
S = N/A O = 269 T = TO (out)(err) |
S = N/A O = 466 T = TO (out)(err) |
S = N/A O = 495 T = TO (out)(err) |
S = N/A O = 237 T = TO (out)(err) |
S = N/A O = 512 T = TO (out)(err) |
S = N/A O = N/A T = 409.38 (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 = 114.25 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 202 T = 114.25 (out)(err) |
S = N/A O = 289 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 202 T = 137.46 (out)(err) |
S = N/A O = 228 T = TO (out)(err) |
S = OPT O = 202 T = 376.14 (out)(err) |
S = OPT O = 202 T = 386.20 (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 = 1673.54 (out)(err) |
S = OPT O = 202 T = 155.16 (out)(err) |
S = N/A O = 223 T = TO (out)(err) |
S = N/A O = 416 T = TO (out)(err) |
S = N/A O = 453 T = TO (out)(err) |
S = N/A O = 210 T = TO (out)(err) |
S = N/A O = 374 T = TO (out)(err) |
S = N/A O = N/A T = 615.66 (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 = 167.71 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 214 T = 221.86 (out)(err) |
S = N/A O = 352 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 214 T = 257.71 (out)(err) |
S = N/A O = 247 T = TO (out)(err) |
S = OPT O = 214 T = 707.57 (out)(err) |
S = OPT O = 214 T = 699.53 (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 = 248 T = 1797.22 (out)(err) |
S = OPT O = 214 T = 167.71 (out)(err) |
S = N/A O = 268 T = TO (out)(err) |
S = N/A O = 437 T = TO (out)(err) |
S = N/A O = 444 T = TO (out)(err) |
S = N/A O = 214 T = TO (out)(err) |
S = N/A O = 433 T = TO (out)(err) |
S = N/A O = N/A T = 207.98 (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 = 61.34 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 203 T = 61.34 (out)(err) |
S = N/A O = 302 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 203 T = 68.69 (out)(err) |
S = N/A O = 232 T = TO (out)(err) |
S = OPT O = 203 T = 182.48 (out)(err) |
S = OPT O = 203 T = 187.32 (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 = 792.11 (out)(err) |
S = OPT O = 203 T = 115.10 (out)(err) |
S = N/A O = 251 T = TO (out)(err) |
S = N/A O = 452 T = TO (out)(err) |
S = N/A O = 526 T = TO (out)(err) |
S = N/A O = 208 T = TO (out)(err) |
S = N/A O = 543 T = TO (out)(err) |
S = N/A O = N/A T = 204.41 (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 = 68.36 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 200 T = 82.79 (out)(err) |
S = N/A O = 285 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 200 T = 68.36 (out)(err) |
S = N/A O = 265 T = TO (out)(err) |
S = OPT O = 200 T = 197.69 (out)(err) |
S = OPT O = 200 T = 195.22 (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 = 966.15 (out)(err) |
S = OPT O = 200 T = 97.02 (out)(err) |
S = N/A O = 245 T = TO (out)(err) |
S = N/A O = 372 T = TO (out)(err) |
S = N/A O = 499 T = TO (out)(err) |
S = N/A O = 200 T = TO (out)(err) |
S = N/A O = 414 T = TO (out)(err) |
S = N/A O = N/A T = 238.86 (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 = 54.14 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 188 T = 80.38 (out)(err) |
S = N/A O = 275 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 188 T = 106.38 (out)(err) |
S = N/A O = 255 T = TO (out)(err) |
S = OPT O = 188 T = 282.84 (out)(err) |
S = OPT O = 188 T = 284.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 = 188 T = 1275.07 (out)(err) |
S = OPT O = 188 T = 54.14 (out)(err) |
S = N/A O = 213 T = TO (out)(err) |
S = N/A O = 392 T = TO (out)(err) |
S = N/A O = 393 T = TO (out)(err) |
S = N/A O = 191 T = TO (out)(err) |
S = N/A O = 438 T = TO (out)(err) |
S = N/A O = N/A T = 542.13 (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 = 161.00 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 226 T = 161.00 (out)(err) |
S = N/A O = 305 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 226 T = 215.95 (out)(err) |
S = N/A O = 240 T = TO (out)(err) |
S = OPT O = 226 T = 575.95 (out)(err) |
S = OPT O = 226 T = 582.27 (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 = 226 T = 1797.38 (out)(err) |
S = OPT O = 226 T = 337.07 (out)(err) |
S = N/A O = 252 T = TO (out)(err) |
S = N/A O = 406 T = TO (out)(err) |
S = N/A O = 445 T = TO (out)(err) |
S = N/A O = 229 T = TO (out)(err) |
S = N/A O = 455 T = TO (out)(err) |
S = N/A O = N/A T = 204.29 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C700_0.wcnf | S = OPT O = 103 T = 22.36 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 103 T = 25.60 (out)(err) |
S = N/A O = 125 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 103 T = 22.36 (out)(err) |
S = N/A O = 108 T = TO (out)(err) |
S = OPT O = 103 T = 65.41 (out)(err) |
S = OPT O = 103 T = 65.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 = 103 T = 354.11 (out)(err) |
S = OPT O = 103 T = 52.63 (out)(err) |
S = N/A O = 109 T = TO (out)(err) |
S = N/A O = 143 T = TO (out)(err) |
S = N/A O = 247 T = TO (out)(err) |
S = N/A O = 103 T = TO (out)(err) |
S = N/A O = 187 T = TO (out)(err) |
S = N/A O = N/A T = 285.70 (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 = 12.84 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 107 T = 15.78 (out)(err) |
S = N/A O = 145 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 107 T = 12.84 (out)(err) |
S = N/A O = 107 T = TO (out)(err) |
S = OPT O = 107 T = 34.53 (out)(err) |
S = OPT O = 107 T = 35.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 = 107 T = 185.82 (out)(err) |
S = OPT O = 107 T = 35.78 (out)(err) |
S = N/A O = 118 T = TO (out)(err) |
S = N/A O = 286 T = TO (out)(err) |
S = N/A O = 139 T = TO (out)(err) |
S = N/A O = 107 T = TO (out)(err) |
S = N/A O = 322 T = TO (out)(err) |
S = N/A O = N/A T = 317.51 (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 = 19.36 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 110 T = 19.36 (out)(err) |
S = N/A O = 125 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 110 T = 19.92 (out)(err) |
S = N/A O = 110 T = TO (out)(err) |
S = OPT O = 110 T = 54.28 (out)(err) |
S = OPT O = 110 T = 57.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 = 110 T = 294.84 (out)(err) |
S = OPT O = 110 T = 52.95 (out)(err) |
S = N/A O = 117 T = TO (out)(err) |
S = N/A O = 139 T = TO (out)(err) |
S = N/A O = 162 T = TO (out)(err) |
S = N/A O = 110 T = TO (out)(err) |
S = N/A O = 298 T = TO (out)(err) |
S = N/A O = N/A T = 293.87 (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 = 6.56 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 102 T = 8.94 (out)(err) |
S = N/A O = 129 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 102 T = 6.56 (out)(err) |
S = N/A O = 108 T = TO (out)(err) |
S = OPT O = 102 T = 18.15 (out)(err) |
S = OPT O = 102 T = 19.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 = 102 T = 101.60 (out)(err) |
S = OPT O = 102 T = 20.72 (out)(err) |
S = N/A O = 116 T = TO (out)(err) |
S = N/A O = 316 T = TO (out)(err) |
S = N/A O = 143 T = TO (out)(err) |
S = N/A O = 102 T = TO (out)(err) |
S = N/A O = 318 T = TO (out)(err) |
S = N/A O = N/A T = 298.83 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C700_4.wcnf | S = OPT O = 110 T = 22.67 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 110 T = 25.05 (out)(err) |
S = N/A O = 142 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 110 T = 22.67 (out)(err) |
S = N/A O = 116 T = TO (out)(err) |
S = OPT O = 110 T = 62.51 (out)(err) |
S = OPT O = 110 T = 62.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 = 110 T = 359.17 (out)(err) |
S = OPT O = 110 T = 69.29 (out)(err) |
S = N/A O = 124 T = TO (out)(err) |
S = N/A O = 270 T = TO (out)(err) |
S = N/A O = 247 T = TO (out)(err) |
S = N/A O = 110 T = TO (out)(err) |
S = N/A O = 339 T = TO (out)(err) |
S = N/A O = N/A T = 237.70 (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.33 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 103 T = 19.02 (out)(err) |
S = N/A O = 125 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 103 T = 15.33 (out)(err) |
S = N/A O = 103 T = TO (out)(err) |
S = OPT O = 103 T = 39.84 (out)(err) |
S = OPT O = 103 T = 41.60 (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 = 221.28 (out)(err) |
S = OPT O = 103 T = 25.38 (out)(err) |
S = N/A O = 118 T = TO (out)(err) |
S = N/A O = 141 T = TO (out)(err) |
S = N/A O = 183 T = TO (out)(err) |
S = N/A O = 103 T = TO (out)(err) |
S = N/A O = 198 T = TO (out)(err) |
S = N/A O = N/A T = 297.82 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C700_6.wcnf | S = OPT O = 102 T = 10.81 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 102 T = 12.54 (out)(err) |
S = N/A O = 132 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 102 T = 10.81 (out)(err) |
S = N/A O = 102 T = TO (out)(err) |
S = OPT O = 102 T = 29.92 (out)(err) |
S = OPT O = 102 T = 29.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 = 102 T = 167.68 (out)(err) |
S = OPT O = 102 T = 26.59 (out)(err) |
S = N/A O = 121 T = TO (out)(err) |
S = N/A O = 234 T = TO (out)(err) |
S = N/A O = 254 T = TO (out)(err) |
S = N/A O = 102 T = TO (out)(err) |
S = N/A O = 268 T = TO (out)(err) |
S = N/A O = N/A T = 396.14 (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 = 11.87 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 104 T = 13.50 (out)(err) |
S = N/A O = 160 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 104 T = 11.87 (out)(err) |
S = N/A O = 114 T = TO (out)(err) |
S = OPT O = 104 T = 32.40 (out)(err) |
S = OPT O = 104 T = 32.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 = 104 T = 169.96 (out)(err) |
S = OPT O = 104 T = 35.33 (out)(err) |
S = N/A O = 121 T = TO (out)(err) |
S = N/A O = 312 T = TO (out)(err) |
S = N/A O = 145 T = TO (out)(err) |
S = N/A O = 104 T = TO (out)(err) |
S = N/A O = 306 T = TO (out)(err) |
S = N/A O = N/A T = 285.87 (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 = 2.06 |
S = N/A O = 82 T = TO (out)(err) |
S = OPT O = 82 T = 2.71 (out)(err) |
S = N/A O = 85 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 82 T = 2.06 (out)(err) |
S = N/A O = 91 T = TO (out)(err) |
S = OPT O = 82 T = 5.00 (out)(err) |
S = OPT O = 82 T = 4.99 (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 = 28.99 (out)(err) |
S = OPT O = 82 T = 5.84 (out)(err) |
S = N/A O = 86 T = TO (out)(err) |
S = N/A O = 127 T = TO (out)(err) |
S = N/A O = 166 T = TO (out)(err) |
S = OPT O = 82 T = 670.25 (out)(err) |
S = N/A O = 145 T = TO (out)(err) |
S = N/A O = N/A T = 285.98 (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 = 12.50 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 104 T = 12.50 (out)(err) |
S = N/A O = 152 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 104 T = 13.43 (out)(err) |
S = N/A O = 104 T = TO (out)(err) |
S = OPT O = 104 T = 36.15 (out)(err) |
S = OPT O = 104 T = 35.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 = 104 T = 187.27 (out)(err) |
S = OPT O = 104 T = 39.68 (out)(err) |
S = N/A O = 111 T = TO (out)(err) |
S = N/A O = 257 T = TO (out)(err) |
S = N/A O = 259 T = TO (out)(err) |
S = N/A O = 104 T = TO (out)(err) |
S = N/A O = 279 T = TO (out)(err) |
S = N/A O = N/A T = 285.57 (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 = 28.57 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 132 T = 28.57 (out)(err) |
S = N/A O = 147 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 132 T = 30.72 (out)(err) |
S = N/A O = 158 T = TO (out)(err) |
S = OPT O = 132 T = 84.49 (out)(err) |
S = OPT O = 132 T = 85.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 = 132 T = 426.17 (out)(err) |
S = OPT O = 132 T = 54.24 (out)(err) |
S = N/A O = 142 T = TO (out)(err) |
S = N/A O = 334 T = TO (out)(err) |
S = N/A O = 166 T = TO (out)(err) |
S = N/A O = 132 T = TO (out)(err) |
S = N/A O = 238 T = TO (out)(err) |
S = N/A O = N/A T = 238.14 (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 = 42.48 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 138 T = 42.48 (out)(err) |
S = N/A O = 191 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 138 T = 49.10 (out)(err) |
S = N/A O = 165 T = TO (out)(err) |
S = OPT O = 138 T = 134.56 (out)(err) |
S = OPT O = 138 T = 133.54 (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 = 697.12 (out)(err) |
S = OPT O = 138 T = 63.69 (out)(err) |
S = N/A O = 160 T = TO (out)(err) |
S = N/A O = 346 T = TO (out)(err) |
S = N/A O = 290 T = TO (out)(err) |
S = N/A O = 138 T = TO (out)(err) |
S = N/A O = 408 T = TO (out)(err) |
S = N/A O = N/A T = 237.59 (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 = 28.62 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 127 T = 28.70 (out)(err) |
S = N/A O = 195 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 127 T = 28.62 (out)(err) |
S = N/A O = 147 T = TO (out)(err) |
S = OPT O = 127 T = 79.81 (out)(err) |
S = OPT O = 127 T = 79.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 = 127 T = 368.69 (out)(err) |
S = OPT O = 127 T = 32.10 (out)(err) |
S = N/A O = 150 T = TO (out)(err) |
S = N/A O = 317 T = TO (out)(err) |
S = N/A O = 296 T = TO (out)(err) |
S = N/A O = 127 T = TO (out)(err) |
S = N/A O = 335 T = TO (out)(err) |
S = N/A O = N/A T = 286.74 (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 = 12.95 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 134 T = 12.95 (out)(err) |
S = N/A O = 233 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 134 T = 19.41 (out)(err) |
S = N/A O = 159 T = TO (out)(err) |
S = OPT O = 134 T = 50.94 (out)(err) |
S = OPT O = 134 T = 52.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 = 280.95 (out)(err) |
S = OPT O = 134 T = 23.12 (out)(err) |
S = N/A O = 148 T = TO (out)(err) |
S = N/A O = 302 T = TO (out)(err) |
S = N/A O = 356 T = TO (out)(err) |
S = N/A O = 134 T = TO (out)(err) |
S = N/A O = 434 T = TO (out)(err) |
S = N/A O = N/A T = 607.17 (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 = 65.89 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 143 T = 88.74 (out)(err) |
S = N/A O = 278 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 143 T = 69.73 (out)(err) |
S = N/A O = 186 T = TO (out)(err) |
S = OPT O = 143 T = 188.89 (out)(err) |
S = OPT O = 143 T = 188.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 = 143 T = 1014.77 (out)(err) |
S = OPT O = 143 T = 65.89 (out)(err) |
S = N/A O = 166 T = TO (out)(err) |
S = N/A O = 213 T = TO (out)(err) |
S = N/A O = 210 T = TO (out)(err) |
S = N/A O = 143 T = TO (out)(err) |
S = N/A O = 285 T = TO (out)(err) |
S = N/A O = N/A T = 258.64 (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 = 68.22 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 144 T = 68.22 (out)(err) |
S = N/A O = 204 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 144 T = 73.25 (out)(err) |
S = N/A O = 153 T = TO (out)(err) |
S = OPT O = 144 T = 210.41 (out)(err) |
S = OPT O = 144 T = 210.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 = 144 T = 1033.26 (out)(err) |
S = OPT O = 144 T = 134.30 (out)(err) |
S = N/A O = 167 T = TO (out)(err) |
S = N/A O = 210 T = TO (out)(err) |
S = N/A O = 327 T = TO (out)(err) |
S = N/A O = 144 T = TO (out)(err) |
S = N/A O = 421 T = TO (out)(err) |
S = N/A O = N/A T = 241.12 (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 = 31.76 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 135 T = 36.63 (out)(err) |
S = N/A O = 165 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 135 T = 31.76 (out)(err) |
S = N/A O = 136 T = TO (out)(err) |
S = OPT O = 135 T = 91.19 (out)(err) |
S = OPT O = 135 T = 94.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 = 135 T = 495.18 (out)(err) |
S = OPT O = 135 T = 61.35 (out)(err) |
S = N/A O = 142 T = TO (out)(err) |
S = N/A O = 389 T = TO (out)(err) |
S = N/A O = 297 T = TO (out)(err) |
S = N/A O = 135 T = TO (out)(err) |
S = N/A O = 349 T = TO (out)(err) |
S = N/A O = N/A T = 237.88 (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 = 36.61 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 147 T = 36.61 (out)(err) |
S = N/A O = 225 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 147 T = 56.74 (out)(err) |
S = N/A O = 161 T = TO (out)(err) |
S = OPT O = 147 T = 148.95 (out)(err) |
S = OPT O = 147 T = 152.96 (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 = 821.86 (out)(err) |
S = OPT O = 147 T = 62.34 (out)(err) |
S = N/A O = 175 T = TO (out)(err) |
S = N/A O = 384 T = TO (out)(err) |
S = N/A O = 323 T = TO (out)(err) |
S = N/A O = 150 T = TO (out)(err) |
S = N/A O = 515 T = TO (out)(err) |
S = N/A O = N/A T = 242.08 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C800_8.wcnf | S = OPT O = 126 T = 28.98 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 126 T = 36.06 (out)(err) |
S = N/A O = 159 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 126 T = 39.32 (out)(err) |
S = N/A O = 126 T = TO (out)(err) |
S = OPT O = 126 T = 99.79 (out)(err) |
S = OPT O = 126 T = 100.24 (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 = 507.47 (out)(err) |
S = OPT O = 126 T = 28.98 (out)(err) |
S = N/A O = 151 T = TO (out)(err) |
S = N/A O = 287 T = TO (out)(err) |
S = N/A O = 390 T = TO (out)(err) |
S = N/A O = 126 T = TO (out)(err) |
S = N/A O = 252 T = TO (out)(err) |
S = N/A O = N/A T = 237.83 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C800_9.wcnf | S = OPT O = 138 T = 32.23 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 138 T = 34.80 (out)(err) |
S = N/A O = 167 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 138 T = 32.23 (out)(err) |
S = N/A O = 156 T = TO (out)(err) |
S = OPT O = 138 T = 89.83 (out)(err) |
S = OPT O = 138 T = 90.22 (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 = 452.40 (out)(err) |
S = OPT O = 138 T = 52.41 (out)(err) |
S = N/A O = 151 T = TO (out)(err) |
S = N/A O = 308 T = TO (out)(err) |
S = N/A O = 331 T = TO (out)(err) |
S = N/A O = 138 T = TO (out)(err) |
S = N/A O = 321 T = TO (out)(err) |
S = N/A O = N/A T = 238.69 (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 = 31.40 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 157 T = 31.40 (out)(err) |
S = N/A O = 213 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 157 T = 34.30 (out)(err) |
S = N/A O = 224 T = TO (out)(err) |
S = OPT O = 157 T = 95.03 (out)(err) |
S = OPT O = 157 T = 97.51 (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 = 446.32 (out)(err) |
S = OPT O = 157 T = 73.18 (out)(err) |
S = N/A O = 159 T = TO (out)(err) |
S = N/A O = 359 T = TO (out)(err) |
S = N/A O = 364 T = TO (out)(err) |
S = N/A O = 157 T = TO (out)(err) |
S = N/A O = 424 T = TO (out)(err) |
S = N/A O = N/A T = 538.59 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C900_1.wcnf | S = OPT O = 192 T = 121.84 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 192 T = 137.26 (out)(err) |
S = N/A O = 260 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 192 T = 121.84 (out)(err) |
S = N/A O = 211 T = TO (out)(err) |
S = OPT O = 192 T = 328.33 (out)(err) |
S = OPT O = 192 T = 335.22 (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 = 1721.86 (out)(err) |
S = OPT O = 192 T = 231.75 (out)(err) |
S = N/A O = 213 T = TO (out)(err) |
S = N/A O = 386 T = TO (out)(err) |
S = N/A O = 543 T = TO (out)(err) |
S = N/A O = 194 T = TO (out)(err) |
S = N/A O = 422 T = TO (out)(err) |
S = N/A O = N/A T = 243.96 (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 = 91.99 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 177 T = 91.99 (out)(err) |
S = N/A O = 199 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 177 T = 98.47 (out)(err) |
S = N/A O = 184 T = TO (out)(err) |
S = OPT O = 177 T = 275.08 (out)(err) |
S = OPT O = 177 T = 272.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 = 177 T = 1398.86 (out)(err) |
S = OPT O = 177 T = 152.52 (out)(err) |
S = N/A O = 191 T = TO (out)(err) |
S = N/A O = 333 T = TO (out)(err) |
S = N/A O = 405 T = TO (out)(err) |
S = N/A O = 178 T = TO (out)(err) |
S = N/A O = 375 T = TO (out)(err) |
S = N/A O = N/A T = 240.00 (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 = 50.67 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 163 T = 50.67 (out)(err) |
S = N/A O = 194 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 163 T = 63.14 (out)(err) |
S = N/A O = 163 T = TO (out)(err) |
S = OPT O = 163 T = 176.46 (out)(err) |
S = OPT O = 163 T = 176.09 (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 = 826.40 (out)(err) |
S = OPT O = 163 T = 76.89 (out)(err) |
S = N/A O = 194 T = TO (out)(err) |
S = N/A O = 198 T = TO (out)(err) |
S = N/A O = 203 T = TO (out)(err) |
S = N/A O = 163 T = TO (out)(err) |
S = N/A O = 376 T = TO (out)(err) |
S = N/A O = N/A T = 238.15 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwms_wcnf_L3_V70_C900_4.wcnf | S = OPT O = 171 T = 78.84 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 171 T = 78.84 (out)(err) |
S = N/A O = 234 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 171 T = 88.30 (out)(err) |
S = N/A O = 218 T = TO (out)(err) |
S = OPT O = 171 T = 236.88 (out)(err) |
S = OPT O = 171 T = 239.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 = 171 T = 1169.79 (out)(err) |
S = OPT O = 171 T = 129.76 (out)(err) |
S = N/A O = 206 T = TO (out)(err) |
S = N/A O = 404 T = TO (out)(err) |
S = N/A O = 329 T = TO (out)(err) |
S = N/A O = 174 T = TO (out)(err) |
S = N/A O = 442 T = TO (out)(err) |
S = N/A O = N/A T = 267.62 (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 = 56.19 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 175 T = 58.28 (out)(err) |
S = N/A O = 225 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 175 T = 56.19 (out)(err) |
S = N/A O = 196 T = TO (out)(err) |
S = OPT O = 175 T = 156.58 (out)(err) |
S = OPT O = 175 T = 158.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 = 175 T = 770.91 (out)(err) |
S = OPT O = 175 T = 115.88 (out)(err) |
S = N/A O = 205 T = TO (out)(err) |
S = N/A O = 384 T = TO (out)(err) |
S = N/A O = 351 T = TO (out)(err) |
S = N/A O = 175 T = TO (out)(err) |
S = N/A O = 397 T = TO (out)(err) |
S = N/A O = N/A T = 241.56 (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 = 60.75 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 174 T = 86.49 (out)(err) |
S = N/A O = 276 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 174 T = 60.75 (out)(err) |
S = N/A O = 174 T = TO (out)(err) |
S = OPT O = 174 T = 164.19 (out)(err) |
S = OPT O = 174 T = 170.22 (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 = 769.31 (out)(err) |
S = OPT O = 174 T = 106.05 (out)(err) |
S = N/A O = 197 T = TO (out)(err) |
S = N/A O = 410 T = TO (out)(err) |
S = N/A O = 222 T = TO (out)(err) |
S = N/A O = 174 T = TO (out)(err) |
S = N/A O = 400 T = TO (out)(err) |
S = N/A O = N/A T = 613.96 (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 = 142.06 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 194 T = 142.06 (out)(err) |
S = N/A O = 246 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 194 T = 175.15 (out)(err) |
S = N/A O = 227 T = TO (out)(err) |
S = OPT O = 194 T = 473.58 (out)(err) |
S = OPT O = 194 T = 476.56 (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 = 200 T = 1797.44 (out)(err) |
S = OPT O = 194 T = 241.77 (out)(err) |
S = N/A O = 223 T = TO (out)(err) |
S = N/A O = 348 T = TO (out)(err) |
S = N/A O = 369 T = TO (out)(err) |
S = N/A O = 200 T = TO (out)(err) |
S = N/A O = 411 T = TO (out)(err) |
S = N/A O = N/A T = 613.93 (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 = 62.65 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 179 T = 62.65 (out)(err) |
S = N/A O = 276 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 179 T = 64.33 (out)(err) |
S = N/A O = 202 T = TO (out)(err) |
S = OPT O = 179 T = 177.39 (out)(err) |
S = OPT O = 179 T = 176.99 (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 = 889.84 (out)(err) |
S = OPT O = 179 T = 126.64 (out)(err) |
S = N/A O = 203 T = TO (out)(err) |
S = N/A O = 396 T = TO (out)(err) |
S = N/A O = 430 T = TO (out)(err) |
S = N/A O = 179 T = TO (out)(err) |
S = N/A O = 443 T = TO (out)(err) |
S = N/A O = N/A T = 567.01 (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 = 69.00 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 181 T = 69.00 (out)(err) |
S = N/A O = 229 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 181 T = 70.71 (out)(err) |
S = N/A O = 188 T = TO (out)(err) |
S = OPT O = 181 T = 190.68 (out)(err) |
S = OPT O = 181 T = 191.47 (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 = 877.85 (out)(err) |
S = OPT O = 181 T = 139.65 (out)(err) |
S = N/A O = 208 T = TO (out)(err) |
S = N/A O = 387 T = TO (out)(err) |
S = N/A O = 411 T = TO (out)(err) |
S = N/A O = 182 T = TO (out)(err) |
S = N/A O = 487 T = TO (out)(err) |
S = N/A O = N/A T = 239.15 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |