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 | Sat4j-i | ubcsat-irots |
---|---|---|---|
file_rwpms_wcnf_L2_V150_C4000_H150_0.wcnf | O = 4231 T = 6.18 |
O = 4619 T = 4.70 (out)(err) |
O = 4231 T = 6.18 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_1.wcnf | O = 26218 T = 10.11 |
O = N/A T = TO (out)(err) |
O = 26218 T = 10.11 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_2.wcnf | O = 4235 T = 1.73 |
O = 4857 T = 4.31 (out)(err) |
O = 4235 T = 1.73 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_3.wcnf | O = 4037 T = 10.37 |
O = 4841 T = 2.01 (out)(err) |
O = 4037 T = 10.37 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_4.wcnf | O = 4031 T = 10.21 |
O = 4873 T = 7.83 (out)(err) |
O = 4031 T = 10.21 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_5.wcnf | O = 4144 T = 11.20 |
O = 4930 T = 7.56 (out)(err) |
O = 4144 T = 11.20 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_6.wcnf | O = 4149 T = 8.59 |
O = 4934 T = 3.07 (out)(err) |
O = 4149 T = 8.59 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_7.wcnf | O = 4043 T = 9.80 |
O = 4789 T = 7.56 (out)(err) |
O = 4043 T = 9.80 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_8.wcnf | O = 4078 T = 10.09 |
O = 4896 T = 5.93 (out)(err) |
O = 4078 T = 10.09 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_9.wcnf | O = 4328 T = 8.67 |
O = 4963 T = 3.91 (out)(err) |
O = 4328 T = 8.67 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_0.wcnf | O = 4572 T = 7.86 |
O = 5484 T = 3.74 (out)(err) |
O = 4572 T = 7.86 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_1.wcnf | O = 4967 T = 17.12 |
O = 5669 T = 4.45 (out)(err) |
O = 4967 T = 17.12 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_2.wcnf | O = 4961 T = 16.77 |
O = 5845 T = 5.92 (out)(err) |
O = 4961 T = 16.77 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_3.wcnf | O = 4614 T = 8.93 |
O = 5572 T = 4.24 (out)(err) |
O = 4614 T = 8.93 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_4.wcnf | O = 4794 T = 14.08 |
O = 5473 T = 5.19 (out)(err) |
O = 4794 T = 14.08 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_5.wcnf | O = 4687 T = 15.17 |
O = 5640 T = 2.74 (out)(err) |
O = 4687 T = 15.17 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_6.wcnf | O = 4605 T = 12.20 |
O = 5589 T = 5.88 (out)(err) |
O = 4605 T = 12.20 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_7.wcnf | O = 4710 T = 11.48 |
O = 5624 T = 3.27 (out)(err) |
O = 4710 T = 11.48 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_8.wcnf | O = 4945 T = 13.03 |
O = 5552 T = 9.15 (out)(err) |
O = 4945 T = 13.03 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_9.wcnf | O = 5023 T = 8.32 |
O = 5477 T = 1.84 (out)(err) |
O = 5023 T = 8.32 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_0.wcnf | O = 5362 T = 8.06 |
O = 6138 T = 4.23 (out)(err) |
O = 5362 T = 8.06 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_1.wcnf | O = 5338 T = 13.27 |
O = 6414 T = 4.50 (out)(err) |
O = 5338 T = 13.27 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_2.wcnf | O = 5312 T = 11.04 |
O = 6217 T = 7.33 (out)(err) |
O = 5312 T = 11.04 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_3.wcnf | O = 5507 T = 8.61 |
O = 6537 T = 3.78 (out)(err) |
O = 5507 T = 8.61 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_4.wcnf | O = 5451 T = 6.13 |
O = 6448 T = 3.78 (out)(err) |
O = 5451 T = 6.13 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_5.wcnf | O = 5308 T = 14.23 |
O = 6133 T = 4.81 (out)(err) |
O = 5308 T = 14.23 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_6.wcnf | O = 5428 T = 11.12 |
O = 6142 T = 4.35 (out)(err) |
O = 5428 T = 11.12 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_7.wcnf | O = 5468 T = 9.87 |
O = 6142 T = 6.24 (out)(err) |
O = 5468 T = 9.87 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_8.wcnf | O = 5339 T = 8.52 |
O = 6046 T = 2.90 (out)(err) |
O = 5339 T = 8.52 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_9.wcnf | O = 5376 T = 9.37 |
O = 6368 T = 2.52 (out)(err) |
O = 5376 T = 9.37 (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_0.wcnf | O = 626 T = 10.30 |
O = 758 T = 5.89 (out)(err) |
O = 626 T = 10.30 (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_1.wcnf | O = 745 T = 9.25 |
O = 968 T = 6.00 (out)(err) |
O = 745 T = 9.25 (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_2.wcnf | O = 629 T = 6.77 |
O = 746 T = 2.36 (out)(err) |
O = 629 T = 6.77 (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_3.wcnf | O = 723 T = 7.90 |
O = 903 T = 1.85 (out)(err) |
O = 723 T = 7.90 (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_4.wcnf | O = 737 T = 8.67 |
O = 907 T = 5.23 (out)(err) |
O = 737 T = 8.67 (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_5.wcnf | O = 668 T = 9.10 |
O = 723 T = 5.25 (out)(err) |
O = 668 T = 9.10 (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_6.wcnf | O = 641 T = 9.52 |
O = 801 T = 2.41 (out)(err) |
O = 641 T = 9.52 (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_7.wcnf | O = 688 T = 10.71 |
O = 807 T = 1.42 (out)(err) |
O = 688 T = 10.71 (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_8.wcnf | O = 577 T = 7.18 |
O = 739 T = 3.47 (out)(err) |
O = 577 T = 7.18 (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_9.wcnf | O = 714 T = 9.81 |
O = 823 T = 4.47 (out)(err) |
O = 714 T = 9.81 (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_0.wcnf | O = 1121 T = 7.73 |
O = 1381 T = 1.37 (out)(err) |
O = 1121 T = 7.73 (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_1.wcnf | O = 1142 T = 10.05 |
O = 1340 T = 5.83 (out)(err) |
O = 1142 T = 10.05 (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_2.wcnf | O = 1252 T = 7.69 |
O = 1655 T = 6.46 (out)(err) |
O = 1252 T = 7.69 (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_3.wcnf | O = 1295 T = 9.33 |
O = 1500 T = 3.86 (out)(err) |
O = 1295 T = 9.33 (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_4.wcnf | O = 1261 T = 7.17 |
O = 1620 T = 5.38 (out)(err) |
O = 1261 T = 7.17 (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_5.wcnf | O = 1047 T = 8.78 |
O = 1292 T = 3.85 (out)(err) |
O = 1047 T = 8.78 (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_6.wcnf | O = 1175 T = 8.20 |
O = 1414 T = 6.74 (out)(err) |
O = 1175 T = 8.20 (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_7.wcnf | O = 1145 T = 7.39 |
O = 1364 T = 5.52 (out)(err) |
O = 1145 T = 7.39 (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_8.wcnf | O = 1135 T = 7.94 |
O = 1432 T = 7.54 (out)(err) |
O = 1135 T = 7.94 (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_9.wcnf | O = 1232 T = 8.68 |
O = 1462 T = 2.08 (out)(err) |
O = 1232 T = 8.68 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_0.wcnf | O = 1842 T = 7.40 |
O = 2283 T = 2.66 (out)(err) |
O = 1842 T = 7.40 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_1.wcnf | O = 1699 T = 4.86 |
O = 2239 T = 5.15 (out)(err) |
O = 1699 T = 4.86 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_2.wcnf | O = 1730 T = 9.23 |
O = 2166 T = 1.75 (out)(err) |
O = 1730 T = 9.23 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_3.wcnf | O = 1885 T = 9.38 |
O = 2214 T = 3.35 (out)(err) |
O = 1885 T = 9.38 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_4.wcnf | O = 2043 T = 40.96 |
O = 2417 T = 4.62 (out)(err) |
O = 2043 T = 40.96 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_5.wcnf | O = 1818 T = 9.08 |
O = 2091 T = 5.07 (out)(err) |
O = 1818 T = 9.08 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_6.wcnf | O = 1832 T = 13.33 |
O = 2159 T = 1.34 (out)(err) |
O = 1832 T = 13.33 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_7.wcnf | O = 1780 T = 11.09 |
O = 2184 T = 5.57 (out)(err) |
O = 1780 T = 11.09 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_8.wcnf | O = 1726 T = 11.76 |
O = 2131 T = 7.40 (out)(err) |
O = 1726 T = 11.76 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_9.wcnf | O = 1807 T = 6.85 |
O = 2262 T = 4.34 (out)(err) |
O = 1807 T = 6.85 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_0.wcnf | O = 2414 T = 10.19 |
O = 2934 T = 3.11 (out)(err) |
O = 2414 T = 10.19 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_1.wcnf | O = 2398 T = 4.96 |
O = 2814 T = 4.99 (out)(err) |
O = 2398 T = 4.96 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_2.wcnf | O = 2113 T = 10.58 |
O = 2686 T = 3.09 (out)(err) |
O = 2113 T = 10.58 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_3.wcnf | O = 2339 T = 11.28 |
O = 2885 T = 2.46 (out)(err) |
O = 2339 T = 11.28 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_4.wcnf | O = 2390 T = 12.99 |
O = 2933 T = 3.13 (out)(err) |
O = 2390 T = 12.99 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_5.wcnf | O = 2332 T = 9.12 |
O = 3028 T = 4.56 (out)(err) |
O = 2332 T = 9.12 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_6.wcnf | O = 2488 T = 8.84 |
O = 2978 T = 4.33 (out)(err) |
O = 2488 T = 8.84 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_7.wcnf | O = 2241 T = 8.19 |
O = 2611 T = 3.78 (out)(err) |
O = 2241 T = 8.19 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_8.wcnf | O = 2353 T = 9.25 |
O = 2832 T = 6.44 (out)(err) |
O = 2353 T = 9.25 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_9.wcnf | O = 2560 T = 9.65 |
O = 3031 T = 3.72 (out)(err) |
O = 2560 T = 9.65 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_0.wcnf | O = 2885 T = 9.50 |
O = 3290 T = 4.82 (out)(err) |
O = 2885 T = 9.50 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_1.wcnf | O = 2918 T = 9.40 |
O = 3316 T = 2.42 (out)(err) |
O = 2918 T = 9.40 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_2.wcnf | O = 2878 T = 8.66 |
O = 3345 T = 4.77 (out)(err) |
O = 2878 T = 8.66 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_3.wcnf | O = 3045 T = 11.60 |
O = 3501 T = 7.90 (out)(err) |
O = 3045 T = 11.60 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_4.wcnf | O = 3021 T = 9.08 |
O = 3511 T = 7.38 (out)(err) |
O = 3021 T = 9.08 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_5.wcnf | O = 2812 T = 1.47 |
O = 3369 T = 6.06 (out)(err) |
O = 2812 T = 1.47 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_6.wcnf | O = 2838 T = 8.86 |
O = 3369 T = 3.19 (out)(err) |
O = 2838 T = 8.86 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_7.wcnf | O = 2815 T = 9.15 |
O = 3506 T = 5.80 (out)(err) |
O = 2815 T = 9.15 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_8.wcnf | O = 3025 T = 10.24 |
O = 3609 T = 5.68 (out)(err) |
O = 3025 T = 10.24 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_9.wcnf | O = 2952 T = 11.71 |
O = 3433 T = 2.92 (out)(err) |
O = 2952 T = 11.71 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_0.wcnf | O = 3634 T = 13.03 |
O = 4247 T = 6.20 (out)(err) |
O = 3634 T = 13.03 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_1.wcnf | O = 3662 T = 12.44 |
O = 4317 T = 4.87 (out)(err) |
O = 3662 T = 12.44 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_2.wcnf | O = 3827 T = 10.03 |
O = 4348 T = 7.12 (out)(err) |
O = 3827 T = 10.03 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_3.wcnf | O = 3512 T = 16.68 |
O = 4016 T = 4.99 (out)(err) |
O = 3512 T = 16.68 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_4.wcnf | O = 3355 T = 8.63 |
O = 4090 T = 4.49 (out)(err) |
O = 3355 T = 8.63 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_5.wcnf | O = 3450 T = 6.89 |
O = 4028 T = 4.55 (out)(err) |
O = 3450 T = 6.89 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_6.wcnf | O = 3654 T = 11.34 |
O = 4310 T = 5.60 (out)(err) |
O = 3654 T = 11.34 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_7.wcnf | O = 3617 T = 6.96 |
O = 4116 T = 3.29 (out)(err) |
O = 3617 T = 6.96 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_8.wcnf | O = 3525 T = 10.41 |
O = 4108 T = 5.25 (out)(err) |
O = 3525 T = 10.41 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_9.wcnf | O = 3240 T = 7.20 |
O = 4171 T = 3.29 (out)(err) |
O = 3240 T = 7.20 (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_0.wcnf | O = 28 T = 4.56 |
O = 31 T = 9.85 (out)(err) |
O = 28 T = 4.56 (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_1.wcnf | O = 15 T = 2.60 |
O = 15 T = 156.21 (out)(err) |
O = 15 T = 2.60 (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_2.wcnf | O = 25 T = 6.55 |
O = 180 T = 5.31 (out)(err) |
O = 25 T = 6.55 (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_3.wcnf | O = 25 T = 5.33 |
O = 183 T = 4.16 (out)(err) |
O = 25 T = 5.33 (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_4.wcnf | O = 30 T = 2.83 |
O = 30 T = 180.60 (out)(err) |
O = 30 T = 2.83 (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_5.wcnf | O = 27 T = 4.12 |
O = 152 T = 5.72 (out)(err) |
O = 27 T = 4.12 (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_6.wcnf | O = 26 T = 5.53 |
O = 159 T = 5.77 (out)(err) |
O = 26 T = 5.53 (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_7.wcnf | O = 29 T = 3.07 |
O = 138 T = 5.64 (out)(err) |
O = 29 T = 3.07 (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_8.wcnf | O = 19 T = 3.76 |
O = 29 T = 10.34 (out)(err) |
O = 19 T = 3.76 (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_9.wcnf | O = 30 T = 4.98 |
O = 142 T = 2.70 (out)(err) |
O = 30 T = 4.98 (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_0.wcnf | O = 54 T = 6.14 |
O = 162 T = 2.96 (out)(err) |
O = 54 T = 6.14 (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_1.wcnf | O = 58 T = 5.33 |
O = 260 T = 2.32 (out)(err) |
O = 58 T = 5.33 (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_2.wcnf | O = 59 T = 5.18 |
O = 247 T = 4.94 (out)(err) |
O = 59 T = 5.18 (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_3.wcnf | O = 48 T = 5.01 |
O = 214 T = 6.36 (out)(err) |
O = 48 T = 5.01 (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_4.wcnf | O = 42 T = 4.60 |
O = 279 T = 4.13 (out)(err) |
O = 42 T = 4.60 (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_5.wcnf | O = 46 T = 4.59 |
O = 151 T = 5.43 (out)(err) |
O = 46 T = 4.59 (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_6.wcnf | O = 51 T = 5.39 |
O = 84 T = 5.07 (out)(err) |
O = 51 T = 5.39 (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_7.wcnf | O = 63 T = 5.49 |
O = 200 T = 4.78 (out)(err) |
O = 63 T = 5.49 (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_8.wcnf | O = 64 T = 4.50 |
O = 226 T = 4.77 (out)(err) |
O = 64 T = 4.50 (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_9.wcnf | O = 45 T = 0.67 |
O = 226 T = 4.21 (out)(err) |
O = 45 T = 0.67 (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_0.wcnf | O = 95 T = 4.64 |
O = 231 T = 4.27 (out)(err) |
O = 95 T = 4.64 (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_1.wcnf | O = 81 T = 5.26 |
O = 274 T = 4.85 (out)(err) |
O = 81 T = 5.26 (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_2.wcnf | O = 77 T = 5.76 |
O = 188 T = 4.92 (out)(err) |
O = 77 T = 5.76 (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_3.wcnf | O = 81 T = 6.56 |
O = 264 T = 5.53 (out)(err) |
O = 81 T = 6.56 (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_4.wcnf | O = 75 T = 4.97 |
O = 303 T = 5.06 (out)(err) |
O = 75 T = 4.97 (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_5.wcnf | O = 80 T = 5.09 |
O = 285 T = 4.31 (out)(err) |
O = 80 T = 5.09 (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_6.wcnf | O = 74 T = 3.90 |
O = 287 T = 5.22 (out)(err) |
O = 74 T = 3.90 (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_7.wcnf | O = 99 T = 4.79 |
O = 315 T = 4.58 (out)(err) |
O = 99 T = 4.79 (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_8.wcnf | O = 90 T = 4.45 |
O = 138 T = 7.57 (out)(err) |
O = 90 T = 4.45 (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_9.wcnf | O = 95 T = 5.10 |
O = 146 T = 10.43 (out)(err) |
O = 95 T = 5.10 (out)(err) |