| 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 | SAT4Jms-ext-i | SAT4Jms-int-i | optimax-it |
|---|---|---|---|---|
| file_rwpms_wcnf_L2_V150_C4000_H150_0.wcnf | O = 4825 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4825 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4000_H150_1.wcnf | O = N/A T = TO |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
| file_rwpms_wcnf_L2_V150_C4000_H150_2.wcnf | O = 4902 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4902 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4000_H150_3.wcnf | O = 4649 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4649 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4000_H150_4.wcnf | O = 4774 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4774 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4000_H150_5.wcnf | O = 4766 T = 0.10 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4766 T = 0.10 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4000_H150_6.wcnf | O = 4916 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4916 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4000_H150_7.wcnf | O = 4914 T = 0.15 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4914 T = 0.15 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4000_H150_8.wcnf | O = 4741 T = 0.10 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4741 T = 0.10 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4000_H150_9.wcnf | O = 5052 T = 0.14 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 5052 T = 0.14 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4500_H150_0.wcnf | O = 5328 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 5328 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4500_H150_1.wcnf | O = 5558 T = 0.18 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 5558 T = 0.18 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4500_H150_2.wcnf | O = 5959 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 5959 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4500_H150_3.wcnf | O = 5446 T = 0.13 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 5446 T = 0.13 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4500_H150_4.wcnf | O = 5509 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 5509 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4500_H150_5.wcnf | O = 5709 T = 0.15 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 5709 T = 0.15 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4500_H150_6.wcnf | O = 5451 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 5451 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4500_H150_7.wcnf | O = 5319 T = 0.15 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 5319 T = 0.15 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4500_H150_8.wcnf | O = 5624 T = 0.15 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 5624 T = 0.15 (out)(err) |
| file_rwpms_wcnf_L2_V150_C4500_H150_9.wcnf | O = 5419 T = 0.15 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 5419 T = 0.15 (out)(err) |
| file_rwpms_wcnf_L2_V150_C5000_H150_0.wcnf | O = 6105 T = 0.21 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 6105 T = 0.21 (out)(err) |
| file_rwpms_wcnf_L2_V150_C5000_H150_1.wcnf | O = 6209 T = 0.17 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 6209 T = 0.17 (out)(err) |
| file_rwpms_wcnf_L2_V150_C5000_H150_2.wcnf | O = 6067 T = 0.16 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 6067 T = 0.16 (out)(err) |
| file_rwpms_wcnf_L2_V150_C5000_H150_3.wcnf | O = 6214 T = 0.15 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 6214 T = 0.15 (out)(err) |
| file_rwpms_wcnf_L2_V150_C5000_H150_4.wcnf | O = 6226 T = 0.14 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 6226 T = 0.14 (out)(err) |
| file_rwpms_wcnf_L2_V150_C5000_H150_5.wcnf | O = 6065 T = 0.15 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 6065 T = 0.15 (out)(err) |
| file_rwpms_wcnf_L2_V150_C5000_H150_6.wcnf | O = 6150 T = 0.15 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 6150 T = 0.15 (out)(err) |
| file_rwpms_wcnf_L2_V150_C5000_H150_7.wcnf | O = 6053 T = 0.15 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 6053 T = 0.15 (out)(err) |
| file_rwpms_wcnf_L2_V150_C5000_H150_8.wcnf | O = 6300 T = 0.18 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 6300 T = 0.18 (out)(err) |
| file_rwpms_wcnf_L2_V150_C5000_H150_9.wcnf | O = 6153 T = 0.16 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 6153 T = 0.16 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1000_H150_0.wcnf | O = 881 T = 0.14 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 881 T = 0.14 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1000_H150_1.wcnf | O = 972 T = 0.09 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 972 T = 0.09 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1000_H150_2.wcnf | O = 775 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 775 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1000_H150_3.wcnf | O = 1037 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1037 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1000_H150_4.wcnf | O = 954 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 954 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1000_H150_5.wcnf | O = 762 T = 0.08 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 762 T = 0.08 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1000_H150_6.wcnf | O = 790 T = 0.09 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 790 T = 0.09 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1000_H150_7.wcnf | O = 979 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 979 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1000_H150_8.wcnf | O = 800 T = 0.09 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 800 T = 0.09 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1000_H150_9.wcnf | O = 843 T = 0.08 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 843 T = 0.08 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1500_H150_0.wcnf | O = 1435 T = 0.09 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1435 T = 0.09 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1500_H150_1.wcnf | O = 1399 T = 0.10 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1399 T = 0.10 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1500_H150_2.wcnf | O = 1582 T = 0.10 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1582 T = 0.10 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1500_H150_3.wcnf | O = 1560 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1560 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1500_H150_4.wcnf | O = 1616 T = 0.13 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1616 T = 0.13 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1500_H150_5.wcnf | O = 1412 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1412 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1500_H150_6.wcnf | O = 1441 T = 0.13 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1441 T = 0.13 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1500_H150_7.wcnf | O = 1514 T = 0.08 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1514 T = 0.08 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1500_H150_8.wcnf | O = 1482 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1482 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C1500_H150_9.wcnf | O = 1609 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 1609 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2000_H150_0.wcnf | O = 2399 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2399 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2000_H150_1.wcnf | O = 2026 T = 0.08 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2026 T = 0.08 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2000_H150_2.wcnf | O = 2099 T = 0.10 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2099 T = 0.10 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2000_H150_3.wcnf | O = 2330 T = 0.09 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2330 T = 0.09 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2000_H150_4.wcnf | O = 2267 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2267 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2000_H150_5.wcnf | O = 2250 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2250 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2000_H150_6.wcnf | O = 2164 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2164 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2000_H150_7.wcnf | O = 2302 T = 0.13 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2302 T = 0.13 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2000_H150_8.wcnf | O = 2305 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2305 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2000_H150_9.wcnf | O = 2250 T = 0.08 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2250 T = 0.08 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2500_H150_0.wcnf | O = 2990 T = 0.08 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2990 T = 0.08 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2500_H150_1.wcnf | O = 2770 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2770 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2500_H150_2.wcnf | O = 2596 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2596 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2500_H150_3.wcnf | O = 2716 T = 0.13 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2716 T = 0.13 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2500_H150_4.wcnf | O = 2978 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2978 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2500_H150_5.wcnf | O = 2841 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2841 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2500_H150_6.wcnf | O = 2829 T = 0.08 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2829 T = 0.08 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2500_H150_7.wcnf | O = 2648 T = 0.08 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2648 T = 0.08 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2500_H150_8.wcnf | O = 2918 T = 0.08 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2918 T = 0.08 (out)(err) |
| file_rwpms_wcnf_L2_V150_C2500_H150_9.wcnf | O = 2812 T = 0.10 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 2812 T = 0.10 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3000_H150_0.wcnf | O = 3360 T = 0.08 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 3360 T = 0.08 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3000_H150_1.wcnf | O = 3544 T = 0.13 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 3544 T = 0.13 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3000_H150_2.wcnf | O = 3372 T = 0.13 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 3372 T = 0.13 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3000_H150_3.wcnf | O = 3665 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 3665 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3000_H150_4.wcnf | O = 3523 T = 0.07 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 3523 T = 0.07 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3000_H150_5.wcnf | O = 3376 T = 0.10 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 3376 T = 0.10 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3000_H150_6.wcnf | O = 3341 T = 0.09 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 3341 T = 0.09 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3000_H150_7.wcnf | O = 3267 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 3267 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3000_H150_8.wcnf | O = 3502 T = 0.09 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 3502 T = 0.09 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3000_H150_9.wcnf | O = 3570 T = 0.13 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 3570 T = 0.13 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3500_H150_0.wcnf | O = 4276 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4276 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3500_H150_1.wcnf | O = 4084 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4084 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3500_H150_2.wcnf | O = 4275 T = 0.13 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4275 T = 0.13 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3500_H150_3.wcnf | O = 4110 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4110 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3500_H150_4.wcnf | O = 4026 T = 0.08 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4026 T = 0.08 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3500_H150_5.wcnf | O = 4013 T = 0.13 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4013 T = 0.13 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3500_H150_6.wcnf | O = 4061 T = 0.10 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4061 T = 0.10 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3500_H150_7.wcnf | O = 4087 T = 0.13 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4087 T = 0.13 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3500_H150_8.wcnf | O = 4282 T = 0.09 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 4282 T = 0.09 (out)(err) |
| file_rwpms_wcnf_L2_V150_C3500_H150_9.wcnf | O = 3971 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 3971 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L3_V100_C600_H100_0.wcnf | O = 98 T = 47.24 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 98 T = 47.24 (out)(err) |
| file_rwpms_wcnf_L3_V100_C600_H100_1.wcnf | O = 37 T = 54.33 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 37 T = 54.33 (out)(err) |
| file_rwpms_wcnf_L3_V100_C600_H100_2.wcnf | O = 36 T = 17.30 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 36 T = 17.30 (out)(err) |
| file_rwpms_wcnf_L3_V100_C600_H100_3.wcnf | O = 54 T = 36.57 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 54 T = 36.57 (out)(err) |
| file_rwpms_wcnf_L3_V100_C600_H100_4.wcnf | O = 30 T = 44.35 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 30 T = 44.35 (out)(err) |
| file_rwpms_wcnf_L3_V100_C600_H100_5.wcnf | O = 42 T = 7.60 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 42 T = 7.60 (out)(err) |
| file_rwpms_wcnf_L3_V100_C600_H100_6.wcnf | O = 72 T = 0.22 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 72 T = 0.22 (out)(err) |
| file_rwpms_wcnf_L3_V100_C600_H100_7.wcnf | O = 44 T = 39.43 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 44 T = 39.43 (out)(err) |
| file_rwpms_wcnf_L3_V100_C600_H100_8.wcnf | O = 25 T = 152.35 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 25 T = 152.35 (out)(err) |
| file_rwpms_wcnf_L3_V100_C600_H100_9.wcnf | O = 34 T = 269.73 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 34 T = 269.73 (out)(err) |
| file_rwpms_wcnf_L3_V100_C700_H100_0.wcnf | O = 111 T = 0.98 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 111 T = 0.98 (out)(err) |
| file_rwpms_wcnf_L3_V100_C700_H100_1.wcnf | O = 186 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 186 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L3_V100_C700_H100_2.wcnf | O = 162 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 162 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L3_V100_C700_H100_3.wcnf | O = 118 T = 0.81 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 118 T = 0.81 (out)(err) |
| file_rwpms_wcnf_L3_V100_C700_H100_4.wcnf | O = 97 T = 0.24 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 97 T = 0.24 (out)(err) |
| file_rwpms_wcnf_L3_V100_C700_H100_5.wcnf | O = 78 T = 0.23 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 78 T = 0.23 (out)(err) |
| file_rwpms_wcnf_L3_V100_C700_H100_6.wcnf | O = 105 T = 0.22 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 105 T = 0.22 (out)(err) |
| file_rwpms_wcnf_L3_V100_C700_H100_7.wcnf | O = 102 T = 3.02 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 102 T = 3.02 (out)(err) |
| file_rwpms_wcnf_L3_V100_C700_H100_8.wcnf | O = 112 T = 4.68 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 112 T = 4.68 (out)(err) |
| file_rwpms_wcnf_L3_V100_C700_H100_9.wcnf | O = 97 T = 0.18 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 97 T = 0.18 (out)(err) |
| file_rwpms_wcnf_L3_V100_C800_H100_0.wcnf | O = 291 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 291 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L3_V100_C800_H100_1.wcnf | O = 136 T = 11.78 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 136 T = 11.78 (out)(err) |
| file_rwpms_wcnf_L3_V100_C800_H100_2.wcnf | O = 219 T = 0.07 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 219 T = 0.07 (out)(err) |
| file_rwpms_wcnf_L3_V100_C800_H100_3.wcnf | O = 133 T = 34.10 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 133 T = 34.10 (out)(err) |
| file_rwpms_wcnf_L3_V100_C800_H100_4.wcnf | O = 151 T = 0.35 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 151 T = 0.35 (out)(err) |
| file_rwpms_wcnf_L3_V100_C800_H100_5.wcnf | O = 248 T = 0.12 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 248 T = 0.12 (out)(err) |
| file_rwpms_wcnf_L3_V100_C800_H100_6.wcnf | O = 120 T = 17.77 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 120 T = 17.77 (out)(err) |
| file_rwpms_wcnf_L3_V100_C800_H100_7.wcnf | O = 297 T = 0.11 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 297 T = 0.11 (out)(err) |
| file_rwpms_wcnf_L3_V100_C800_H100_8.wcnf | O = 135 T = 178.40 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 135 T = 178.40 (out)(err) |
| file_rwpms_wcnf_L3_V100_C800_H100_9.wcnf | O = 217 T = 0.10 |
O = N/A T = TO (out)(err) |
O = N/A T = TO (out)(err) |
O = 217 T = 0.10 (out)(err) |