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+-wpms | MSUnCore | MaxHS | Maxsatz2013f | QMaxSAT2-g | QMaxSAT2-m | Toulbar2 | WMaxSatz+ | WMaxSatz09 | WPM1-2013 | WPM2-2013 | ckmax-small | glpk-maxsat | optimax-ni | optimax | pwbo2.3-wpms | scip-maxsat | toysat | wbo2.1-wcnf | wmifumax |
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
file_rwpms_wcnf_L2_V150_C4000_H150_0.wcnf | S = OPT O = 4231 T = 0.68 |
S = OPT O = 4231 T = 1308.53 (out)(err) |
S = OPT O = 4231 T = 3.52 (out)(err) |
S = N/A O = 4607 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4231 T = 0.68 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4231 T = 1013.63 (out)(err) |
S = OPT O = 4231 T = 1.10 (out)(err) |
S = OPT O = 4231 T = 1.18 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4231 T = 4.70 (out)(err) |
S = N/A O = 4368 T = TO (out)(err) |
S = N/A O = 4738 T = TO (out)(err) |
S = N/A O = 4825 T = TO (out)(err) |
S = N/A O = 20667 T = 1788.59 (out)(err) |
S = OPT O = 4231 T = 656.13 (out)(err) |
S = N/A O = 4824 T = TO (out)(err) |
S = N/A O = N/A T = 325.70 (out)(err) |
S = N/A O = N/A T = 626.92 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_1.wcnf | S = UNSAT O = N/A T = 0.00 |
S = UNSAT O = N/A T = 0.58 (out)(err) |
S = UNSAT O = N/A T = 3.40 (out)(err) |
S = UNSAT O = N/A T = 0.01 (out)(err) |
S = N/A O = N/A T = 0.00 (out)(err) |
S = UNSAT O = N/A T = 0.02 (out)(err) |
S = N/A O = N/A T = 0.00 (out)(err) |
S = N/A O = N/A T = 0.00 (out)(err) |
S = UNSAT O = N/A T = 0.04 (out)(err) |
S = UNSAT O = N/A T = 0.04 (out)(err) |
S = UNSAT O = N/A T = 0.09 (out)(err) |
S = N/A O = N/A T = 0.01 (out)(err) |
S = N/A O = N/A T = 0.00 (out)(err) |
S = UNSAT O = N/A T = 2.24 (out)(err) |
S = UNSAT O = N/A T = 0.39 (out)(err) |
S = UNSAT O = N/A T = 0.01 (out)(err) |
S = UNSAT O = N/A T = 0.00 (out)(err) |
S = UNSAT O = N/A T = 0.02 (out)(err) |
S = UNSAT O = N/A T = 0.05 (out)(err) |
S = UNSAT O = N/A T = 1.90 (out)(err) |
S = UNSAT O = N/A T = 0.00 (out)(err) |
S = UNSAT O = N/A T = 0.00 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_2.wcnf | S = OPT O = 4235 T = 1.27 |
S = OPT O = 4235 T = 279.78 (out)(err) |
S = OPT O = 4235 T = 4.40 (out)(err) |
S = N/A O = 4820 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4235 T = 1.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 = 4235 T = 1110.84 (out)(err) |
S = OPT O = 4235 T = 4.67 (out)(err) |
S = OPT O = 4235 T = 3.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 = 4235 T = 4.76 (out)(err) |
S = N/A O = 4347 T = TO (out)(err) |
S = N/A O = 4881 T = TO (out)(err) |
S = N/A O = 4902 T = TO (out)(err) |
S = N/A O = 20229 T = 1788.66 (out)(err) |
S = N/A O = 4235 T = TO (out)(err) |
S = N/A O = 4991 T = TO (out)(err) |
S = N/A O = N/A T = 318.68 (out)(err) |
S = N/A O = N/A T = 1329.38 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_3.wcnf | S = OPT O = 4037 T = 2.88 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4037 T = 5.03 (out)(err) |
S = N/A O = 4737 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4037 T = 2.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 = 4211 T = TO (out)(err) |
S = OPT O = 4037 T = 8.57 (out)(err) |
S = OPT O = 4037 T = 8.64 (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 = 4037 T = 6.41 (out)(err) |
S = N/A O = 4246 T = TO (out)(err) |
S = N/A O = 4659 T = TO (out)(err) |
S = N/A O = 4649 T = TO (out)(err) |
S = N/A O = 20795 T = 1788.72 (out)(err) |
S = N/A O = 4037 T = TO (out)(err) |
S = N/A O = 4768 T = TO (out)(err) |
S = N/A O = N/A T = 429.51 (out)(err) |
S = N/A O = N/A T = 459.05 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_4.wcnf | S = OPT O = 4031 T = 6.61 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4031 T = 8.43 (out)(err) |
S = N/A O = 4562 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4031 T = 6.61 (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 = 4071 T = TO (out)(err) |
S = OPT O = 4031 T = 21.00 (out)(err) |
S = OPT O = 4031 T = 20.31 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4031 T = 6.96 (out)(err) |
S = N/A O = 4161 T = TO (out)(err) |
S = N/A O = 4932 T = TO (out)(err) |
S = N/A O = 4774 T = TO (out)(err) |
S = N/A O = 20865 T = 1787.98 (out)(err) |
S = N/A O = 4038 T = TO (out)(err) |
S = N/A O = 4607 T = TO (out)(err) |
S = N/A O = N/A T = 429.67 (out)(err) |
S = N/A O = N/A T = 339.98 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_5.wcnf | S = OPT O = 4144 T = 11.87 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4144 T = 13.27 (out)(err) |
S = N/A O = 4886 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4144 T = 13.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 = 4144 T = TO (out)(err) |
S = OPT O = 4144 T = 54.42 (out)(err) |
S = OPT O = 4144 T = 50.71 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4144 T = 11.87 (out)(err) |
S = N/A O = 4239 T = TO (out)(err) |
S = N/A O = 4519 T = TO (out)(err) |
S = N/A O = 4766 T = TO (out)(err) |
S = N/A O = 20977 T = 1788.65 (out)(err) |
S = N/A O = 4155 T = TO (out)(err) |
S = N/A O = 4976 T = TO (out)(err) |
S = N/A O = N/A T = 429.71 (out)(err) |
S = N/A O = N/A T = 583.28 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_6.wcnf | S = OPT O = 4149 T = 12.43 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4149 T = 13.76 (out)(err) |
S = N/A O = 4799 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4149 T = 12.43 (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 = 4291 T = TO (out)(err) |
S = OPT O = 4149 T = 53.91 (out)(err) |
S = OPT O = 4149 T = 54.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 = 4149 T = 26.25 (out)(err) |
S = N/A O = 4305 T = TO (out)(err) |
S = N/A O = 4746 T = TO (out)(err) |
S = N/A O = 4916 T = TO (out)(err) |
S = N/A O = 20466 T = 1787.32 (out)(err) |
S = N/A O = 4166 T = TO (out)(err) |
S = N/A O = 4757 T = TO (out)(err) |
S = N/A O = N/A T = 429.37 (out)(err) |
S = N/A O = N/A T = 364.02 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_7.wcnf | S = OPT O = 4043 T = 12.45 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4043 T = 12.45 (out)(err) |
S = N/A O = 4464 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4043 T = 20.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 = 4301 T = TO (out)(err) |
S = OPT O = 4043 T = 69.02 (out)(err) |
S = OPT O = 4043 T = 70.89 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4043 T = 12.60 (out)(err) |
S = N/A O = 4239 T = TO (out)(err) |
S = N/A O = 4781 T = TO (out)(err) |
S = N/A O = 4914 T = TO (out)(err) |
S = N/A O = 20508 T = 1786.89 (out)(err) |
S = N/A O = 4093 T = TO (out)(err) |
S = N/A O = 5031 T = TO (out)(err) |
S = N/A O = N/A T = 429.02 (out)(err) |
S = N/A O = N/A T = 573.60 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_8.wcnf | S = OPT O = 4078 T = 14.62 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4078 T = 17.54 (out)(err) |
S = N/A O = 4832 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4078 T = 30.89 (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 = 4420 T = TO (out)(err) |
S = OPT O = 4078 T = 111.40 (out)(err) |
S = OPT O = 4078 T = 111.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 = 4078 T = 14.62 (out)(err) |
S = N/A O = 4268 T = TO (out)(err) |
S = N/A O = 4848 T = TO (out)(err) |
S = N/A O = 4741 T = TO (out)(err) |
S = N/A O = 20948 T = 1788.19 (out)(err) |
S = N/A O = 4094 T = TO (out)(err) |
S = N/A O = 5117 T = TO (out)(err) |
S = N/A O = N/A T = 429.08 (out)(err) |
S = N/A O = N/A T = 299.30 (out)(err) |
file_rwpms_wcnf_L2_V150_C4000_H150_9.wcnf | S = OPT O = 4328 T = 4.33 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4328 T = 6.85 (out)(err) |
S = N/A O = 4952 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4328 T = 4.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 = 4407 T = TO (out)(err) |
S = OPT O = 4328 T = 15.83 (out)(err) |
S = OPT O = 4328 T = 12.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 = 4328 T = 6.86 (out)(err) |
S = N/A O = 4436 T = TO (out)(err) |
S = N/A O = 4940 T = TO (out)(err) |
S = N/A O = 5052 T = TO (out)(err) |
S = N/A O = 20961 T = 1788.07 (out)(err) |
S = N/A O = 4359 T = TO (out)(err) |
S = N/A O = 5067 T = TO (out)(err) |
S = N/A O = N/A T = 429.01 (out)(err) |
S = N/A O = N/A T = 839.85 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_0.wcnf | S = OPT O = 4572 T = 15.82 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4572 T = 15.82 (out)(err) |
S = N/A O = 5370 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4572 T = 26.29 (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 = 4759 T = TO (out)(err) |
S = OPT O = 4572 T = 93.28 (out)(err) |
S = OPT O = 4572 T = 91.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 = 4572 T = 19.33 (out)(err) |
S = N/A O = 4773 T = TO (out)(err) |
S = N/A O = 5415 T = TO (out)(err) |
S = N/A O = 5328 T = TO (out)(err) |
S = N/A O = 23465 T = 1788.07 (out)(err) |
S = N/A O = 4640 T = TO (out)(err) |
S = N/A O = 5402 T = TO (out)(err) |
S = N/A O = N/A T = 429.47 (out)(err) |
S = N/A O = N/A T = 622.66 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_1.wcnf | S = OPT O = 4967 T = 15.46 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4967 T = 15.46 (out)(err) |
S = N/A O = 5577 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4967 T = 27.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 = 5196 T = TO (out)(err) |
S = OPT O = 4967 T = 98.43 (out)(err) |
S = OPT O = 4967 T = 103.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 = 4967 T = 30.12 (out)(err) |
S = N/A O = 5154 T = TO (out)(err) |
S = N/A O = 5531 T = TO (out)(err) |
S = N/A O = 5558 T = TO (out)(err) |
S = N/A O = 23558 T = 1787.88 (out)(err) |
S = N/A O = 5050 T = TO (out)(err) |
S = N/A O = 5811 T = TO (out)(err) |
S = N/A O = N/A T = 429.75 (out)(err) |
S = N/A O = N/A T = 431.95 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_2.wcnf | S = OPT O = 4961 T = 5.16 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4961 T = 8.25 (out)(err) |
S = N/A O = 5302 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4961 T = 5.16 (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 = 4978 T = TO (out)(err) |
S = OPT O = 4961 T = 20.65 (out)(err) |
S = OPT O = 4961 T = 18.92 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4961 T = 8.80 (out)(err) |
S = N/A O = 5114 T = TO (out)(err) |
S = N/A O = 5894 T = TO (out)(err) |
S = N/A O = 5959 T = TO (out)(err) |
S = N/A O = 23508 T = 1787.84 (out)(err) |
S = N/A O = 5052 T = TO (out)(err) |
S = N/A O = 6654 T = TO (out)(err) |
S = N/A O = N/A T = 429.28 (out)(err) |
S = N/A O = N/A T = 495.12 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_3.wcnf | S = OPT O = 4614 T = 1.93 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4614 T = 4.88 (out)(err) |
S = N/A O = 5460 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4614 T = 1.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 = 4662 T = TO (out)(err) |
S = OPT O = 4614 T = 10.67 (out)(err) |
S = OPT O = 4614 T = 10.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 = 4614 T = 6.79 (out)(err) |
S = N/A O = 4742 T = TO (out)(err) |
S = N/A O = 5344 T = TO (out)(err) |
S = N/A O = 5446 T = TO (out)(err) |
S = N/A O = 23447 T = 1787.42 (out)(err) |
S = N/A O = 4614 T = TO (out)(err) |
S = N/A O = 5614 T = TO (out)(err) |
S = N/A O = N/A T = 429.67 (out)(err) |
S = N/A O = N/A T = 754.59 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_4.wcnf | S = OPT O = 4794 T = 21.60 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4794 T = 21.60 (out)(err) |
S = N/A O = 5329 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4794 T = 30.83 (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 = 4909 T = TO (out)(err) |
S = OPT O = 4794 T = 113.25 (out)(err) |
S = OPT O = 4794 T = 107.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 = 4794 T = 42.11 (out)(err) |
S = N/A O = 4945 T = TO (out)(err) |
S = N/A O = 5582 T = TO (out)(err) |
S = N/A O = 5509 T = TO (out)(err) |
S = N/A O = 23469 T = 1787.34 (out)(err) |
S = N/A O = 4820 T = TO (out)(err) |
S = N/A O = 5765 T = TO (out)(err) |
S = N/A O = N/A T = 573.24 (out)(err) |
S = N/A O = N/A T = 420.93 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_5.wcnf | S = OPT O = 4687 T = 7.99 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4687 T = 9.41 (out)(err) |
S = N/A O = 5474 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4687 T = 7.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 = 4812 T = TO (out)(err) |
S = OPT O = 4687 T = 28.06 (out)(err) |
S = OPT O = 4687 T = 28.19 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4687 T = 13.02 (out)(err) |
S = N/A O = 4941 T = TO (out)(err) |
S = N/A O = 5427 T = TO (out)(err) |
S = N/A O = 5709 T = TO (out)(err) |
S = N/A O = 23318 T = 1788.73 (out)(err) |
S = N/A O = 4775 T = TO (out)(err) |
S = N/A O = 5433 T = TO (out)(err) |
S = N/A O = N/A T = 429.28 (out)(err) |
S = N/A O = N/A T = 401.87 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_6.wcnf | S = OPT O = 4605 T = 10.05 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4605 T = 10.05 (out)(err) |
S = N/A O = 5274 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4605 T = 11.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 = 4776 T = TO (out)(err) |
S = OPT O = 4605 T = 44.81 (out)(err) |
S = OPT O = 4605 T = 46.72 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4605 T = 10.68 (out)(err) |
S = N/A O = 4845 T = TO (out)(err) |
S = N/A O = 5559 T = TO (out)(err) |
S = N/A O = 5451 T = TO (out)(err) |
S = N/A O = 23595 T = 1787.76 (out)(err) |
S = N/A O = 4635 T = TO (out)(err) |
S = N/A O = 5316 T = TO (out)(err) |
S = N/A O = N/A T = 572.92 (out)(err) |
S = N/A O = N/A T = 430.63 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_7.wcnf | S = OPT O = 4710 T = 10.42 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4710 T = 10.42 (out)(err) |
S = N/A O = 5413 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4710 T = 12.52 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = 4946 T = TO (out)(err) |
S = OPT O = 4710 T = 37.21 (out)(err) |
S = OPT O = 4710 T = 38.18 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4710 T = 15.47 (out)(err) |
S = N/A O = 4833 T = TO (out)(err) |
S = N/A O = 5483 T = TO (out)(err) |
S = N/A O = 5319 T = TO (out)(err) |
S = N/A O = 23574 T = 1787.23 (out)(err) |
S = N/A O = 4712 T = TO (out)(err) |
S = N/A O = 5563 T = TO (out)(err) |
S = N/A O = N/A T = 572.02 (out)(err) |
S = N/A O = N/A T = 551.37 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_8.wcnf | S = OPT O = 4945 T = 6.08 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4945 T = 8.32 (out)(err) |
S = N/A O = 5617 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4945 T = 6.08 (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 = 5135 T = TO (out)(err) |
S = OPT O = 4945 T = 20.72 (out)(err) |
S = OPT O = 4945 T = 25.75 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 4945 T = 6.97 (out)(err) |
S = N/A O = 5155 T = TO (out)(err) |
S = N/A O = 5720 T = TO (out)(err) |
S = N/A O = 5624 T = TO (out)(err) |
S = N/A O = 23310 T = 1788.33 (out)(err) |
S = N/A O = 4950 T = TO (out)(err) |
S = N/A O = 5626 T = TO (out)(err) |
S = N/A O = N/A T = 429.71 (out)(err) |
S = N/A O = N/A T = 1525.57 (out)(err) |
file_rwpms_wcnf_L2_V150_C4500_H150_9.wcnf | S = OPT O = 5023 T = 9.76 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5023 T = 9.76 (out)(err) |
S = N/A O = 5665 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5023 T = 12.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 = 5130 T = TO (out)(err) |
S = OPT O = 5023 T = 33.61 (out)(err) |
S = OPT O = 5023 T = 33.66 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5023 T = 11.12 (out)(err) |
S = N/A O = 5154 T = TO (out)(err) |
S = N/A O = 5470 T = TO (out)(err) |
S = N/A O = 5419 T = TO (out)(err) |
S = N/A O = 23825 T = 1787.78 (out)(err) |
S = N/A O = 5045 T = TO (out)(err) |
S = N/A O = 5502 T = TO (out)(err) |
S = N/A O = N/A T = 429.42 (out)(err) |
S = N/A O = N/A T = 823.38 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_0.wcnf | S = OPT O = 5362 T = 6.07 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5362 T = 7.59 (out)(err) |
S = N/A O = 6316 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5362 T = 6.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 = 5362 T = TO (out)(err) |
S = OPT O = 5362 T = 22.52 (out)(err) |
S = OPT O = 5362 T = 21.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 = 5362 T = 8.34 (out)(err) |
S = N/A O = 5574 T = TO (out)(err) |
S = N/A O = 6022 T = TO (out)(err) |
S = N/A O = 6105 T = TO (out)(err) |
S = N/A O = 26508 T = 1788.04 (out)(err) |
S = N/A O = 5365 T = TO (out)(err) |
S = N/A O = 6228 T = TO (out)(err) |
S = N/A O = N/A T = 429.37 (out)(err) |
S = N/A O = N/A T = 522.30 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_1.wcnf | S = OPT O = 5338 T = 5.36 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5338 T = 10.91 (out)(err) |
S = N/A O = 6064 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5338 T = 11.09 (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 = 5489 T = TO (out)(err) |
S = OPT O = 5338 T = 42.43 (out)(err) |
S = OPT O = 5338 T = 45.05 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5338 T = 5.36 (out)(err) |
S = N/A O = 5496 T = TO (out)(err) |
S = N/A O = 6158 T = TO (out)(err) |
S = N/A O = 6209 T = TO (out)(err) |
S = N/A O = 26509 T = 1787.92 (out)(err) |
S = N/A O = 5349 T = TO (out)(err) |
S = N/A O = 6365 T = TO (out)(err) |
S = N/A O = N/A T = 430.03 (out)(err) |
S = N/A O = N/A T = 1554.66 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_2.wcnf | S = OPT O = 5312 T = 9.29 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5312 T = 14.36 (out)(err) |
S = N/A O = 6424 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5312 T = 24.10 (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 = 5413 T = TO (out)(err) |
S = OPT O = 5312 T = 97.56 (out)(err) |
S = OPT O = 5312 T = 97.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 = 5312 T = 9.29 (out)(err) |
S = N/A O = 5583 T = TO (out)(err) |
S = N/A O = 6085 T = TO (out)(err) |
S = N/A O = 6067 T = TO (out)(err) |
S = N/A O = 26718 T = 1787.23 (out)(err) |
S = N/A O = 5333 T = TO (out)(err) |
S = N/A O = 6526 T = TO (out)(err) |
S = N/A O = N/A T = 429.60 (out)(err) |
S = N/A O = N/A T = 441.42 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_3.wcnf | S = OPT O = 5507 T = 5.43 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5507 T = 7.08 (out)(err) |
S = N/A O = 6372 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5507 T = 5.43 (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 = 5507 T = TO (out)(err) |
S = OPT O = 5507 T = 19.94 (out)(err) |
S = OPT O = 5507 T = 20.29 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5507 T = 10.66 (out)(err) |
S = N/A O = 5721 T = TO (out)(err) |
S = N/A O = 6091 T = TO (out)(err) |
S = N/A O = 6214 T = TO (out)(err) |
S = N/A O = 26653 T = 1787.27 (out)(err) |
S = N/A O = 5507 T = TO (out)(err) |
S = N/A O = 6379 T = TO (out)(err) |
S = N/A O = N/A T = 429.70 (out)(err) |
S = N/A O = N/A T = 456.69 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_4.wcnf | S = OPT O = 5451 T = 41.26 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5451 T = 41.26 (out)(err) |
S = N/A O = 6405 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5451 T = 54.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 = 5747 T = TO (out)(err) |
S = OPT O = 5451 T = 235.90 (out)(err) |
S = OPT O = 5451 T = 236.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 = 5451 T = 52.37 (out)(err) |
S = N/A O = 5669 T = TO (out)(err) |
S = N/A O = 6027 T = TO (out)(err) |
S = N/A O = 6226 T = TO (out)(err) |
S = N/A O = 26382 T = 1787.09 (out)(err) |
S = N/A O = 5559 T = TO (out)(err) |
S = N/A O = 6737 T = TO (out)(err) |
S = N/A O = N/A T = 572.79 (out)(err) |
S = N/A O = N/A T = 740.90 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_5.wcnf | S = OPT O = 5308 T = 7.07 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5308 T = 7.07 (out)(err) |
S = N/A O = 6097 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5308 T = 8.10 (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 = 5366 T = TO (out)(err) |
S = OPT O = 5308 T = 34.62 (out)(err) |
S = OPT O = 5308 T = 35.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 = 5308 T = 8.51 (out)(err) |
S = N/A O = 5423 T = TO (out)(err) |
S = N/A O = 6001 T = TO (out)(err) |
S = N/A O = 6065 T = TO (out)(err) |
S = N/A O = 26286 T = 1787.95 (out)(err) |
S = N/A O = 5310 T = TO (out)(err) |
S = N/A O = 6474 T = TO (out)(err) |
S = N/A O = N/A T = 429.52 (out)(err) |
S = N/A O = N/A T = 392.08 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_6.wcnf | S = OPT O = 5428 T = 8.56 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5428 T = 8.56 (out)(err) |
S = N/A O = 6050 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5428 T = 9.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 = 5788 T = TO (out)(err) |
S = OPT O = 5428 T = 39.50 (out)(err) |
S = OPT O = 5428 T = 39.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 = 5428 T = 20.16 (out)(err) |
S = N/A O = 5615 T = TO (out)(err) |
S = N/A O = 5889 T = TO (out)(err) |
S = N/A O = 6150 T = TO (out)(err) |
S = N/A O = 26424 T = 1786.83 (out)(err) |
S = N/A O = 5511 T = TO (out)(err) |
S = N/A O = 6297 T = TO (out)(err) |
S = N/A O = N/A T = 429.28 (out)(err) |
S = N/A O = N/A T = 777.40 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_7.wcnf | S = OPT O = 5468 T = 16.11 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5468 T = 16.11 (out)(err) |
S = N/A O = 6167 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5468 T = 31.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 = 5550 T = TO (out)(err) |
S = OPT O = 5468 T = 146.39 (out)(err) |
S = OPT O = 5468 T = 138.41 (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 = 5468 T = 22.17 (out)(err) |
S = N/A O = 5704 T = TO (out)(err) |
S = N/A O = 6268 T = TO (out)(err) |
S = N/A O = 6053 T = TO (out)(err) |
S = N/A O = 26822 T = 1787.09 (out)(err) |
S = N/A O = 5534 T = TO (out)(err) |
S = N/A O = 6031 T = TO (out)(err) |
S = N/A O = N/A T = 429.67 (out)(err) |
S = N/A O = N/A T = 340.73 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_8.wcnf | S = OPT O = 5339 T = 2.62 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5339 T = 6.05 (out)(err) |
S = N/A O = 5986 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5339 T = 2.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 = 5339 T = TO (out)(err) |
S = OPT O = 5339 T = 8.54 (out)(err) |
S = OPT O = 5339 T = 9.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 = 5339 T = 5.81 (out)(err) |
S = N/A O = 5516 T = TO (out)(err) |
S = N/A O = 6307 T = TO (out)(err) |
S = N/A O = 6300 T = TO (out)(err) |
S = N/A O = 26505 T = 1786.83 (out)(err) |
S = N/A O = 5339 T = TO (out)(err) |
S = N/A O = 6282 T = TO (out)(err) |
S = N/A O = N/A T = 572.40 (out)(err) |
S = N/A O = N/A T = 640.80 (out)(err) |
file_rwpms_wcnf_L2_V150_C5000_H150_9.wcnf | S = OPT O = 5376 T = 4.68 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5376 T = 8.45 (out)(err) |
S = N/A O = 6289 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 5376 T = 4.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 = 5574 T = TO (out)(err) |
S = OPT O = 5376 T = 16.99 (out)(err) |
S = OPT O = 5376 T = 17.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 = 5376 T = 7.08 (out)(err) |
S = N/A O = 5588 T = TO (out)(err) |
S = N/A O = 6173 T = TO (out)(err) |
S = N/A O = 6153 T = TO (out)(err) |
S = N/A O = 26448 T = 1787.78 (out)(err) |
S = N/A O = 5421 T = TO (out)(err) |
S = N/A O = 7803 T = TO (out)(err) |
S = N/A O = N/A T = 429.30 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_0.wcnf | S = OPT O = 626 T = 0.06 |
S = OPT O = 626 T = 10.50 (out)(err) |
S = OPT O = 626 T = 3.72 (out)(err) |
S = N/A O = 702 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 626 T = 0.06 (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 = 626 T = 1.15 (out)(err) |
S = OPT O = 626 T = 0.18 (out)(err) |
S = OPT O = 626 T = 0.12 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 626 T = 0.64 (out)(err) |
S = OPT O = 626 T = 134.47 (out)(err) |
S = N/A O = 820 T = TO (out)(err) |
S = N/A O = 881 T = TO (out)(err) |
S = N/A O = 3100 T = 1790.13 (out)(err) |
S = OPT O = 626 T = 10.04 (out)(err) |
S = N/A O = 875 T = TO (out)(err) |
S = N/A O = N/A T = 224.29 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_1.wcnf | S = OPT O = 745 T = 0.11 |
S = OPT O = 745 T = 10.15 (out)(err) |
S = OPT O = 745 T = 3.67 (out)(err) |
S = N/A O = 832 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 745 T = 0.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 = 745 T = 1.30 (out)(err) |
S = OPT O = 745 T = 0.30 (out)(err) |
S = OPT O = 745 T = 0.23 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 745 T = 0.94 (out)(err) |
S = OPT O = 745 T = 85.67 (out)(err) |
S = N/A O = 930 T = TO (out)(err) |
S = N/A O = 972 T = TO (out)(err) |
S = N/A O = 2610 T = 1790.22 (out)(err) |
S = OPT O = 745 T = 11.88 (out)(err) |
S = N/A O = 868 T = TO (out)(err) |
S = N/A O = N/A T = 178.95 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_2.wcnf | S = OPT O = 629 T = 0.04 |
S = OPT O = 629 T = 1.39 (out)(err) |
S = OPT O = 629 T = 3.35 (out)(err) |
S = N/A O = 848 T = TO (out)(err) |
S = OPT O = 629 T = 17.63 (out)(err) |
S = OPT O = 629 T = 0.04 (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 = 629 T = 0.07 (out)(err) |
S = OPT O = 629 T = 0.06 (out)(err) |
S = OPT O = 629 T = 0.06 (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 = 629 T = 0.56 (out)(err) |
S = OPT O = 629 T = 4.90 (out)(err) |
S = N/A O = 872 T = TO (out)(err) |
S = N/A O = 775 T = TO (out)(err) |
S = N/A O = 2472 T = 1790.67 (out)(err) |
S = OPT O = 629 T = 2.63 (out)(err) |
S = N/A O = 791 T = TO (out)(err) |
S = N/A O = N/A T = 204.75 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_3.wcnf | S = OPT O = 723 T = 0.20 |
S = OPT O = 723 T = 8.95 (out)(err) |
S = OPT O = 723 T = 3.41 (out)(err) |
S = N/A O = 964 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 723 T = 0.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 = 723 T = 2.06 (out)(err) |
S = OPT O = 723 T = 0.39 (out)(err) |
S = OPT O = 723 T = 0.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 = 723 T = 0.64 (out)(err) |
S = OPT O = 723 T = 396.09 (out)(err) |
S = N/A O = 894 T = TO (out)(err) |
S = N/A O = 1037 T = TO (out)(err) |
S = N/A O = 2474 T = 1790.06 (out)(err) |
S = OPT O = 723 T = 13.02 (out)(err) |
S = N/A O = 939 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) |
file_rwpms_wcnf_L2_V150_C1000_H150_4.wcnf | S = OPT O = 737 T = 0.05 |
S = OPT O = 737 T = 3.88 (out)(err) |
S = OPT O = 737 T = 3.30 (out)(err) |
S = N/A O = 877 T = TO (out)(err) |
S = OPT O = 737 T = 22.21 (out)(err) |
S = OPT O = 737 T = 0.05 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 737 T = 0.23 (out)(err) |
S = OPT O = 737 T = 0.10 (out)(err) |
S = OPT O = 737 T = 0.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 = 737 T = 1.08 (out)(err) |
S = OPT O = 737 T = 14.27 (out)(err) |
S = N/A O = 999 T = TO (out)(err) |
S = N/A O = 954 T = TO (out)(err) |
S = N/A O = 2823 T = 1790.95 (out)(err) |
S = OPT O = 737 T = 3.98 (out)(err) |
S = N/A O = 916 T = TO (out)(err) |
S = N/A O = N/A T = 178.80 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_5.wcnf | S = OPT O = 668 T = 0.06 |
S = OPT O = 668 T = 3.92 (out)(err) |
S = OPT O = 668 T = 3.43 (out)(err) |
S = N/A O = 757 T = TO (out)(err) |
S = OPT O = 668 T = 28.36 (out)(err) |
S = OPT O = 668 T = 0.06 (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 = 668 T = 0.28 (out)(err) |
S = OPT O = 668 T = 0.10 (out)(err) |
S = OPT O = 668 T = 0.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 = 668 T = 0.55 (out)(err) |
S = OPT O = 668 T = 37.91 (out)(err) |
S = N/A O = 900 T = TO (out)(err) |
S = N/A O = 762 T = TO (out)(err) |
S = N/A O = 2660 T = 1790.86 (out)(err) |
S = OPT O = 668 T = 4.08 (out)(err) |
S = N/A O = 757 T = TO (out)(err) |
S = N/A O = N/A T = 348.32 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_6.wcnf | S = OPT O = 641 T = 0.02 |
S = OPT O = 641 T = 0.56 (out)(err) |
S = OPT O = 641 T = 3.19 (out)(err) |
S = N/A O = 727 T = TO (out)(err) |
S = OPT O = 641 T = 10.78 (out)(err) |
S = OPT O = 641 T = 0.02 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 641 T = 0.02 (out)(err) |
S = OPT O = 641 T = 0.05 (out)(err) |
S = OPT O = 641 T = 0.06 (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 = 641 T = 0.67 (out)(err) |
S = OPT O = 641 T = 17.29 (out)(err) |
S = N/A O = 856 T = TO (out)(err) |
S = N/A O = 790 T = TO (out)(err) |
S = N/A O = 2475 T = 1791.46 (out)(err) |
S = OPT O = 641 T = 1.77 (out)(err) |
S = N/A O = 802 T = TO (out)(err) |
S = N/A O = N/A T = 238.76 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_7.wcnf | S = OPT O = 688 T = 0.08 |
S = OPT O = 688 T = 13.98 (out)(err) |
S = OPT O = 688 T = 3.56 (out)(err) |
S = N/A O = 810 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 688 T = 0.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 = 688 T = 0.83 (out)(err) |
S = OPT O = 688 T = 0.17 (out)(err) |
S = OPT O = 688 T = 0.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 = 688 T = 0.93 (out)(err) |
S = OPT O = 688 T = 61.82 (out)(err) |
S = N/A O = 906 T = TO (out)(err) |
S = N/A O = 979 T = TO (out)(err) |
S = N/A O = 2354 T = 1789.84 (out)(err) |
S = OPT O = 688 T = 12.53 (out)(err) |
S = N/A O = 801 T = TO (out)(err) |
S = N/A O = N/A T = 178.97 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_8.wcnf | S = OPT O = 577 T = 0.10 |
S = OPT O = 577 T = 11.50 (out)(err) |
S = OPT O = 577 T = 3.34 (out)(err) |
S = N/A O = 702 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 577 T = 0.10 (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 = 577 T = 2.31 (out)(err) |
S = OPT O = 577 T = 0.21 (out)(err) |
S = OPT O = 577 T = 0.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 = 577 T = 0.66 (out)(err) |
S = OPT O = 577 T = 1336.54 (out)(err) |
S = N/A O = 728 T = TO (out)(err) |
S = N/A O = 800 T = TO (out)(err) |
S = N/A O = 2393 T = 1790.22 (out)(err) |
S = OPT O = 577 T = 10.60 (out)(err) |
S = N/A O = 859 T = TO (out)(err) |
S = N/A O = N/A T = 220.68 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1000_H150_9.wcnf | S = OPT O = 714 T = 0.04 |
S = OPT O = 714 T = 3.34 (out)(err) |
S = OPT O = 714 T = 3.56 (out)(err) |
S = N/A O = 846 T = TO (out)(err) |
S = OPT O = 714 T = 266.14 (out)(err) |
S = OPT O = 714 T = 0.04 (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 = 0.20 (out)(err) |
S = OPT O = 714 T = 0.12 (out)(err) |
S = OPT O = 714 T = 0.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 = 714 T = 1.08 (out)(err) |
S = OPT O = 714 T = 10.25 (out)(err) |
S = N/A O = 912 T = TO (out)(err) |
S = N/A O = 843 T = TO (out)(err) |
S = N/A O = 3423 T = 1790.14 (out)(err) |
S = OPT O = 714 T = 3.71 (out)(err) |
S = N/A O = 885 T = TO (out)(err) |
S = N/A O = N/A T = 250.28 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_0.wcnf | S = OPT O = 1121 T = 0.66 |
S = OPT O = 1121 T = 66.64 (out)(err) |
S = OPT O = 1121 T = 4.17 (out)(err) |
S = N/A O = 1349 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1121 T = 0.66 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1121 T = 1000.91 (out)(err) |
S = OPT O = 1121 T = 1.50 (out)(err) |
S = OPT O = 1121 T = 1.46 (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 = 1121 T = 2.66 (out)(err) |
S = N/A O = 1144 T = TO (out)(err) |
S = N/A O = 1478 T = TO (out)(err) |
S = N/A O = 1435 T = TO (out)(err) |
S = N/A O = 5752 T = 1789.44 (out)(err) |
S = OPT O = 1121 T = 184.15 (out)(err) |
S = N/A O = 1545 T = TO (out)(err) |
S = N/A O = N/A T = 318.33 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_1.wcnf | S = OPT O = 1142 T = 0.35 |
S = OPT O = 1142 T = 12.48 (out)(err) |
S = OPT O = 1142 T = 3.58 (out)(err) |
S = N/A O = 1245 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1142 T = 0.35 (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 = 1142 T = 5.57 (out)(err) |
S = OPT O = 1142 T = 0.71 (out)(err) |
S = OPT O = 1142 T = 0.71 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1142 T = 1.49 (out)(err) |
S = OPT O = 1142 T = 1415.67 (out)(err) |
S = N/A O = 1416 T = TO (out)(err) |
S = N/A O = 1399 T = TO (out)(err) |
S = N/A O = 5961 T = 1790.92 (out)(err) |
S = OPT O = 1142 T = 17.50 (out)(err) |
S = N/A O = 1497 T = TO (out)(err) |
S = N/A O = N/A T = 179.18 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_2.wcnf | S = OPT O = 1252 T = 0.47 |
S = OPT O = 1252 T = 46.34 (out)(err) |
S = OPT O = 1252 T = 3.65 (out)(err) |
S = N/A O = 1406 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1252 T = 0.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 = 1252 T = 204.85 (out)(err) |
S = OPT O = 1252 T = 1.13 (out)(err) |
S = OPT O = 1252 T = 1.14 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1252 T = 1.82 (out)(err) |
S = N/A O = 1260 T = TO (out)(err) |
S = N/A O = 1666 T = TO (out)(err) |
S = N/A O = 1582 T = TO (out)(err) |
S = N/A O = 6663 T = 1788.53 (out)(err) |
S = OPT O = 1252 T = 117.57 (out)(err) |
S = N/A O = 1829 T = TO (out)(err) |
S = N/A O = N/A T = 318.32 (out)(err) |
S = N/A O = N/A T = 1526.74 (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_3.wcnf | S = OPT O = 1295 T = 0.30 |
S = OPT O = 1295 T = 32.71 (out)(err) |
S = OPT O = 1295 T = 3.58 (out)(err) |
S = N/A O = 1532 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1295 T = 0.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 = 1295 T = 62.62 (out)(err) |
S = OPT O = 1295 T = 0.64 (out)(err) |
S = OPT O = 1295 T = 0.64 (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 = 1295 T = 1.44 (out)(err) |
S = N/A O = 1315 T = TO (out)(err) |
S = N/A O = 1623 T = TO (out)(err) |
S = N/A O = 1560 T = TO (out)(err) |
S = N/A O = 5913 T = 1789.54 (out)(err) |
S = OPT O = 1295 T = 45.34 (out)(err) |
S = N/A O = 1605 T = TO (out)(err) |
S = N/A O = N/A T = 318.44 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_4.wcnf | S = OPT O = 1261 T = 0.46 |
S = OPT O = 1261 T = 35.91 (out)(err) |
S = OPT O = 1261 T = 4.00 (out)(err) |
S = N/A O = 1531 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1261 T = 0.46 (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 = 1261 T = 29.42 (out)(err) |
S = OPT O = 1261 T = 1.03 (out)(err) |
S = OPT O = 1261 T = 1.04 (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 = 1261 T = 1.33 (out)(err) |
S = N/A O = 1271 T = TO (out)(err) |
S = N/A O = 1546 T = TO (out)(err) |
S = N/A O = 1616 T = TO (out)(err) |
S = N/A O = 5907 T = 1789.00 (out)(err) |
S = OPT O = 1261 T = 48.16 (out)(err) |
S = N/A O = 1564 T = TO (out)(err) |
S = N/A O = N/A T = 318.31 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_5.wcnf | S = OPT O = 1047 T = 1.24 |
S = OPT O = 1047 T = 35.78 (out)(err) |
S = OPT O = 1047 T = 4.28 (out)(err) |
S = N/A O = 1327 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1047 T = 1.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 = 1047 T = 22.46 (out)(err) |
S = OPT O = 1047 T = 2.40 (out)(err) |
S = OPT O = 1047 T = 2.37 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1047 T = 1.81 (out)(err) |
S = N/A O = 1076 T = TO (out)(err) |
S = N/A O = 1404 T = TO (out)(err) |
S = N/A O = 1412 T = TO (out)(err) |
S = N/A O = 5976 T = 1789.44 (out)(err) |
S = OPT O = 1047 T = 61.92 (out)(err) |
S = N/A O = 1430 T = TO (out)(err) |
S = N/A O = N/A T = 317.74 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_6.wcnf | S = OPT O = 1175 T = 0.10 |
S = OPT O = 1175 T = 17.55 (out)(err) |
S = OPT O = 1175 T = 4.09 (out)(err) |
S = N/A O = 1371 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1175 T = 0.10 (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 = 1175 T = 12.41 (out)(err) |
S = OPT O = 1175 T = 0.16 (out)(err) |
S = OPT O = 1175 T = 0.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 = 1175 T = 1.28 (out)(err) |
S = OPT O = 1175 T = 594.69 (out)(err) |
S = N/A O = 1515 T = TO (out)(err) |
S = N/A O = 1441 T = TO (out)(err) |
S = N/A O = 5897 T = 1790.50 (out)(err) |
S = OPT O = 1175 T = 21.70 (out)(err) |
S = N/A O = 1427 T = TO (out)(err) |
S = N/A O = N/A T = 178.89 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_7.wcnf | S = OPT O = 1145 T = 0.67 |
S = OPT O = 1145 T = 33.35 (out)(err) |
S = OPT O = 1145 T = 4.24 (out)(err) |
S = N/A O = 1331 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1145 T = 0.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 = 1145 T = 125.07 (out)(err) |
S = OPT O = 1145 T = 0.98 (out)(err) |
S = OPT O = 1145 T = 1.06 (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 = 1145 T = 1.36 (out)(err) |
S = N/A O = 1157 T = TO (out)(err) |
S = N/A O = 1472 T = TO (out)(err) |
S = N/A O = 1514 T = TO (out)(err) |
S = N/A O = 5776 T = 1789.41 (out)(err) |
S = OPT O = 1145 T = 75.38 (out)(err) |
S = N/A O = 1467 T = TO (out)(err) |
S = N/A O = N/A T = 317.97 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_8.wcnf | S = OPT O = 1135 T = 1.03 |
S = OPT O = 1135 T = 89.49 (out)(err) |
S = OPT O = 1135 T = 4.66 (out)(err) |
S = N/A O = 1343 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1135 T = 1.03 (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 = 1135 T = 207.84 (out)(err) |
S = OPT O = 1135 T = 2.68 (out)(err) |
S = OPT O = 1135 T = 2.02 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1135 T = 2.62 (out)(err) |
S = N/A O = 1167 T = TO (out)(err) |
S = N/A O = 1427 T = TO (out)(err) |
S = N/A O = 1482 T = TO (out)(err) |
S = N/A O = 5718 T = 1789.18 (out)(err) |
S = OPT O = 1135 T = 378.17 (out)(err) |
S = N/A O = 1578 T = TO (out)(err) |
S = N/A O = N/A T = 297.58 (out)(err) |
S = N/A O = N/A T = 1484.18 (out)(err) |
file_rwpms_wcnf_L2_V150_C1500_H150_9.wcnf | S = OPT O = 1232 T = 0.73 |
S = OPT O = 1232 T = 46.14 (out)(err) |
S = OPT O = 1232 T = 4.09 (out)(err) |
S = N/A O = 1605 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1232 T = 0.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 = 1232 T = 102.17 (out)(err) |
S = OPT O = 1232 T = 1.66 (out)(err) |
S = OPT O = 1232 T = 1.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 = 1232 T = 2.01 (out)(err) |
S = N/A O = 1232 T = TO (out)(err) |
S = N/A O = 1475 T = TO (out)(err) |
S = N/A O = 1609 T = TO (out)(err) |
S = N/A O = 6556 T = 1789.07 (out)(err) |
S = OPT O = 1232 T = 146.97 (out)(err) |
S = N/A O = 1578 T = TO (out)(err) |
S = N/A O = N/A T = 317.83 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_0.wcnf | S = OPT O = 1842 T = 1.70 |
S = OPT O = 1842 T = 136.08 (out)(err) |
S = OPT O = 1842 T = 5.25 (out)(err) |
S = N/A O = 2144 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1842 T = 1.70 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1842 T = 187.03 (out)(err) |
S = OPT O = 1842 T = 4.31 (out)(err) |
S = OPT O = 1842 T = 4.17 (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 = 1842 T = 2.92 (out)(err) |
S = N/A O = 1880 T = TO (out)(err) |
S = N/A O = 2250 T = TO (out)(err) |
S = N/A O = 2399 T = TO (out)(err) |
S = N/A O = 8971 T = 1789.53 (out)(err) |
S = OPT O = 1842 T = 483.48 (out)(err) |
S = N/A O = 2386 T = TO (out)(err) |
S = N/A O = N/A T = 350.87 (out)(err) |
S = N/A O = N/A T = 930.00 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_1.wcnf | S = OPT O = 1699 T = 0.53 |
S = OPT O = 1699 T = 82.66 (out)(err) |
S = OPT O = 1699 T = 4.04 (out)(err) |
S = N/A O = 2074 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1699 T = 0.53 (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 = 1699 T = 151.58 (out)(err) |
S = OPT O = 1699 T = 0.92 (out)(err) |
S = OPT O = 1699 T = 0.93 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1699 T = 2.06 (out)(err) |
S = N/A O = 1724 T = TO (out)(err) |
S = N/A O = 1998 T = TO (out)(err) |
S = N/A O = 2026 T = TO (out)(err) |
S = N/A O = 9066 T = 1789.59 (out)(err) |
S = OPT O = 1699 T = 338.73 (out)(err) |
S = N/A O = 2146 T = TO (out)(err) |
S = N/A O = N/A T = 318.05 (out)(err) |
S = N/A O = N/A T = 474.51 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_2.wcnf | S = OPT O = 1730 T = 0.94 |
S = OPT O = 1730 T = 70.41 (out)(err) |
S = OPT O = 1730 T = 5.01 (out)(err) |
S = N/A O = 2059 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1730 T = 0.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 = 1730 T = 480.39 (out)(err) |
S = OPT O = 1730 T = 2.96 (out)(err) |
S = OPT O = 1730 T = 2.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 = 1730 T = 1.82 (out)(err) |
S = N/A O = 1771 T = TO (out)(err) |
S = N/A O = 2180 T = TO (out)(err) |
S = N/A O = 2099 T = TO (out)(err) |
S = N/A O = 8927 T = 1789.68 (out)(err) |
S = OPT O = 1730 T = 391.80 (out)(err) |
S = N/A O = 2162 T = TO (out)(err) |
S = N/A O = N/A T = 190.27 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_3.wcnf | S = OPT O = 1885 T = 1.06 |
S = OPT O = 1885 T = 77.99 (out)(err) |
S = OPT O = 1885 T = 4.47 (out)(err) |
S = N/A O = 2456 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1885 T = 1.06 (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 = 1885 T = 269.36 (out)(err) |
S = OPT O = 1885 T = 3.28 (out)(err) |
S = OPT O = 1885 T = 2.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 = 1885 T = 2.72 (out)(err) |
S = N/A O = 1911 T = TO (out)(err) |
S = N/A O = 2271 T = TO (out)(err) |
S = N/A O = 2330 T = TO (out)(err) |
S = N/A O = 9050 T = 1788.87 (out)(err) |
S = OPT O = 1885 T = 289.13 (out)(err) |
S = N/A O = 2471 T = TO (out)(err) |
S = N/A O = N/A T = 318.35 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_4.wcnf | S = OPT O = 2043 T = 0.72 |
S = OPT O = 2043 T = 34.38 (out)(err) |
S = OPT O = 2043 T = 3.88 (out)(err) |
S = N/A O = 2371 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2043 T = 0.72 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2043 T = 28.21 (out)(err) |
S = OPT O = 2043 T = 1.70 (out)(err) |
S = OPT O = 2043 T = 1.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 = 2043 T = 4.84 (out)(err) |
S = N/A O = 2046 T = TO (out)(err) |
S = N/A O = 2466 T = TO (out)(err) |
S = N/A O = 2267 T = TO (out)(err) |
S = N/A O = 9016 T = 1789.63 (out)(err) |
S = OPT O = 2043 T = 56.98 (out)(err) |
S = N/A O = 2554 T = TO (out)(err) |
S = N/A O = N/A T = 318.13 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_5.wcnf | S = OPT O = 1818 T = 2.60 |
S = OPT O = 1818 T = 112.82 (out)(err) |
S = OPT O = 1818 T = 5.96 (out)(err) |
S = N/A O = 2061 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1818 T = 2.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 = 1818 T = 558.70 (out)(err) |
S = OPT O = 1818 T = 4.26 (out)(err) |
S = OPT O = 1818 T = 5.18 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1818 T = 4.51 (out)(err) |
S = N/A O = 1861 T = TO (out)(err) |
S = N/A O = 2269 T = TO (out)(err) |
S = N/A O = 2250 T = TO (out)(err) |
S = N/A O = 8962 T = 1789.25 (out)(err) |
S = OPT O = 1818 T = 432.63 (out)(err) |
S = N/A O = 2428 T = TO (out)(err) |
S = N/A O = N/A T = 183.25 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_6.wcnf | S = OPT O = 1832 T = 0.28 |
S = OPT O = 1832 T = 21.50 (out)(err) |
S = OPT O = 1832 T = 4.54 (out)(err) |
S = N/A O = 2162 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1832 T = 0.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 = 1832 T = 5.53 (out)(err) |
S = OPT O = 1832 T = 0.96 (out)(err) |
S = OPT O = 1832 T = 0.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 = 1832 T = 2.94 (out)(err) |
S = N/A O = 1841 T = TO (out)(err) |
S = N/A O = 2278 T = TO (out)(err) |
S = N/A O = 2164 T = TO (out)(err) |
S = N/A O = 8925 T = 1789.09 (out)(err) |
S = OPT O = 1832 T = 22.98 (out)(err) |
S = N/A O = 2355 T = TO (out)(err) |
S = N/A O = N/A T = 317.94 (out)(err) |
S = N/A O = N/A T = 1265.55 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_7.wcnf | S = OPT O = 1780 T = 0.83 |
S = OPT O = 1780 T = 112.37 (out)(err) |
S = OPT O = 1780 T = 4.23 (out)(err) |
S = N/A O = 2186 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1780 T = 0.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 = 1780 T = 64.37 (out)(err) |
S = OPT O = 1780 T = 2.16 (out)(err) |
S = OPT O = 1780 T = 2.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 = 1780 T = 2.56 (out)(err) |
S = N/A O = 1835 T = TO (out)(err) |
S = N/A O = 2278 T = TO (out)(err) |
S = N/A O = 2302 T = TO (out)(err) |
S = N/A O = 8600 T = 1789.49 (out)(err) |
S = OPT O = 1780 T = 169.04 (out)(err) |
S = N/A O = 2093 T = TO (out)(err) |
S = N/A O = N/A T = 318.08 (out)(err) |
S = N/A O = N/A T = 1410.12 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_8.wcnf | S = OPT O = 1726 T = 0.58 |
S = OPT O = 1726 T = 47.57 (out)(err) |
S = OPT O = 1726 T = 4.06 (out)(err) |
S = N/A O = 2034 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1726 T = 0.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 = 1726 T = 28.97 (out)(err) |
S = OPT O = 1726 T = 1.74 (out)(err) |
S = OPT O = 1726 T = 1.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 = 1726 T = 1.55 (out)(err) |
S = N/A O = 1736 T = TO (out)(err) |
S = N/A O = 2190 T = TO (out)(err) |
S = N/A O = 2305 T = TO (out)(err) |
S = N/A O = 9010 T = 1789.85 (out)(err) |
S = OPT O = 1726 T = 76.17 (out)(err) |
S = N/A O = 2091 T = TO (out)(err) |
S = N/A O = N/A T = 318.19 (out)(err) |
S = N/A O = N/A T = 818.81 (out)(err) |
file_rwpms_wcnf_L2_V150_C2000_H150_9.wcnf | S = OPT O = 1807 T = 2.90 |
S = OPT O = 1807 T = 1718.31 (out)(err) |
S = OPT O = 1807 T = 5.93 (out)(err) |
S = N/A O = 2066 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 1807 T = 2.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 = 1807 T = 578.89 (out)(err) |
S = OPT O = 1807 T = 7.35 (out)(err) |
S = OPT O = 1807 T = 7.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 = 1807 T = 4.45 (out)(err) |
S = N/A O = 1861 T = TO (out)(err) |
S = N/A O = 2206 T = TO (out)(err) |
S = N/A O = 2250 T = TO (out)(err) |
S = N/A O = 9072 T = 1789.68 (out)(err) |
S = OPT O = 1807 T = 1067.12 (out)(err) |
S = N/A O = 2266 T = TO (out)(err) |
S = N/A O = N/A T = 317.72 (out)(err) |
S = N/A O = N/A T = 762.23 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_0.wcnf | S = OPT O = 2414 T = 0.72 |
S = OPT O = 2414 T = 60.18 (out)(err) |
S = OPT O = 2414 T = 4.21 (out)(err) |
S = N/A O = 2784 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2414 T = 0.72 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2414 T = 957.96 (out)(err) |
S = OPT O = 2414 T = 1.71 (out)(err) |
S = OPT O = 2414 T = 1.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 = 2414 T = 3.14 (out)(err) |
S = N/A O = 2417 T = TO (out)(err) |
S = N/A O = 2895 T = TO (out)(err) |
S = N/A O = 2990 T = TO (out)(err) |
S = N/A O = 11669 T = 1790.07 (out)(err) |
S = OPT O = 2414 T = 185.61 (out)(err) |
S = N/A O = 3198 T = TO (out)(err) |
S = N/A O = N/A T = 317.94 (out)(err) |
S = N/A O = N/A T = 1296.44 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_1.wcnf | S = OPT O = 2398 T = 1.41 |
S = OPT O = 2398 T = 1729.94 (out)(err) |
S = OPT O = 2398 T = 4.66 (out)(err) |
S = N/A O = 2764 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2398 T = 1.41 (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 = 2398 T = 506.47 (out)(err) |
S = OPT O = 2398 T = 4.17 (out)(err) |
S = OPT O = 2398 T = 4.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 = 2398 T = 3.84 (out)(err) |
S = N/A O = 2441 T = TO (out)(err) |
S = N/A O = 2857 T = TO (out)(err) |
S = N/A O = 2770 T = TO (out)(err) |
S = N/A O = 11934 T = 1789.20 (out)(err) |
S = OPT O = 2398 T = 1047.83 (out)(err) |
S = N/A O = 2897 T = TO (out)(err) |
S = N/A O = N/A T = 327.75 (out)(err) |
S = N/A O = N/A T = 725.50 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_2.wcnf | S = OPT O = 2113 T = 2.57 |
S = OPT O = 2113 T = 220.10 (out)(err) |
S = OPT O = 2113 T = 5.33 (out)(err) |
S = N/A O = 2656 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2113 T = 2.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 = 2113 T = 1199.71 (out)(err) |
S = OPT O = 2113 T = 7.70 (out)(err) |
S = OPT O = 2113 T = 7.59 (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 = 2113 T = 2.57 (out)(err) |
S = N/A O = 2213 T = TO (out)(err) |
S = N/A O = 2577 T = TO (out)(err) |
S = N/A O = 2596 T = TO (out)(err) |
S = N/A O = 11768 T = 1789.40 (out)(err) |
S = OPT O = 2113 T = 1458.21 (out)(err) |
S = N/A O = 2842 T = TO (out)(err) |
S = N/A O = N/A T = 317.88 (out)(err) |
S = N/A O = N/A T = 815.33 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_3.wcnf | S = OPT O = 2339 T = 1.99 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2339 T = 4.87 (out)(err) |
S = N/A O = 2920 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2339 T = 1.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 = 2339 T = 1699.07 (out)(err) |
S = OPT O = 2339 T = 5.94 (out)(err) |
S = OPT O = 2339 T = 6.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 = 2339 T = 4.20 (out)(err) |
S = N/A O = 2401 T = TO (out)(err) |
S = N/A O = 2813 T = TO (out)(err) |
S = N/A O = 2716 T = TO (out)(err) |
S = N/A O = 12075 T = 1789.31 (out)(err) |
S = OPT O = 2339 T = 1540.84 (out)(err) |
S = N/A O = 2886 T = TO (out)(err) |
S = N/A O = N/A T = 319.31 (out)(err) |
S = N/A O = N/A T = 415.92 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_4.wcnf | S = OPT O = 2390 T = 0.64 |
S = OPT O = 2390 T = 246.22 (out)(err) |
S = OPT O = 2390 T = 3.85 (out)(err) |
S = N/A O = 2854 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2390 T = 0.64 (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 = 2390 T = 839.90 (out)(err) |
S = OPT O = 2390 T = 1.93 (out)(err) |
S = OPT O = 2390 T = 1.64 (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 = 2390 T = 3.65 (out)(err) |
S = N/A O = 2451 T = TO (out)(err) |
S = N/A O = 2773 T = TO (out)(err) |
S = N/A O = 2978 T = TO (out)(err) |
S = N/A O = 11715 T = 1789.62 (out)(err) |
S = OPT O = 2390 T = 794.75 (out)(err) |
S = N/A O = 3028 T = TO (out)(err) |
S = N/A O = N/A T = 318.12 (out)(err) |
S = N/A O = N/A T = 1193.35 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_5.wcnf | S = OPT O = 2332 T = 0.31 |
S = OPT O = 2332 T = 89.20 (out)(err) |
S = OPT O = 2332 T = 3.75 (out)(err) |
S = N/A O = 2727 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2332 T = 0.31 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2332 T = 140.97 (out)(err) |
S = OPT O = 2332 T = 0.82 (out)(err) |
S = OPT O = 2332 T = 0.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 = 2332 T = 3.51 (out)(err) |
S = N/A O = 2358 T = TO (out)(err) |
S = N/A O = 2857 T = TO (out)(err) |
S = N/A O = 2841 T = TO (out)(err) |
S = N/A O = 11930 T = 1788.88 (out)(err) |
S = OPT O = 2332 T = 107.42 (out)(err) |
S = N/A O = 2875 T = TO (out)(err) |
S = N/A O = N/A T = 318.34 (out)(err) |
S = N/A O = N/A T = 646.22 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_6.wcnf | S = OPT O = 2488 T = 1.48 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2488 T = 4.49 (out)(err) |
S = N/A O = 2927 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2488 T = 1.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 = 2488 T = TO (out)(err) |
S = OPT O = 2488 T = 5.65 (out)(err) |
S = OPT O = 2488 T = 4.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 = 2488 T = 4.62 (out)(err) |
S = N/A O = 2541 T = TO (out)(err) |
S = N/A O = 2906 T = TO (out)(err) |
S = N/A O = 2829 T = TO (out)(err) |
S = N/A O = 11937 T = 1789.15 (out)(err) |
S = OPT O = 2488 T = 1653.42 (out)(err) |
S = N/A O = 3372 T = TO (out)(err) |
S = N/A O = N/A T = 318.67 (out)(err) |
S = N/A O = N/A T = 829.69 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_7.wcnf | S = OPT O = 2241 T = 3.12 |
S = OPT O = 2241 T = 578.10 (out)(err) |
S = OPT O = 2241 T = 6.32 (out)(err) |
S = N/A O = 2523 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2241 T = 3.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 = 2241 T = TO (out)(err) |
S = OPT O = 2241 T = 8.47 (out)(err) |
S = OPT O = 2241 T = 8.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 = 2241 T = 5.73 (out)(err) |
S = N/A O = 2302 T = TO (out)(err) |
S = N/A O = 2485 T = TO (out)(err) |
S = N/A O = 2648 T = TO (out)(err) |
S = N/A O = 12005 T = 1789.47 (out)(err) |
S = OPT O = 2241 T = 732.65 (out)(err) |
S = N/A O = 2855 T = TO (out)(err) |
S = N/A O = N/A T = 429.27 (out)(err) |
S = N/A O = N/A T = 485.68 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_8.wcnf | S = OPT O = 2353 T = 2.34 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2353 T = 5.22 (out)(err) |
S = N/A O = 2728 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2353 T = 2.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 = 2353 T = 1769.61 (out)(err) |
S = OPT O = 2353 T = 7.23 (out)(err) |
S = OPT O = 2353 T = 8.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 = 2353 T = 9.22 (out)(err) |
S = N/A O = 2367 T = TO (out)(err) |
S = N/A O = 2813 T = TO (out)(err) |
S = N/A O = 2918 T = TO (out)(err) |
S = N/A O = 11663 T = 1789.77 (out)(err) |
S = N/A O = 2353 T = TO (out)(err) |
S = N/A O = 3032 T = TO (out)(err) |
S = N/A O = N/A T = 318.17 (out)(err) |
S = N/A O = N/A T = 800.12 (out)(err) |
file_rwpms_wcnf_L2_V150_C2500_H150_9.wcnf | S = OPT O = 2560 T = 0.46 |
S = OPT O = 2560 T = 24.07 (out)(err) |
S = OPT O = 2560 T = 3.71 (out)(err) |
S = N/A O = 2860 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2560 T = 0.46 (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 = 2560 T = 18.64 (out)(err) |
S = OPT O = 2560 T = 1.56 (out)(err) |
S = OPT O = 2560 T = 1.53 (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 = 2560 T = 2.85 (out)(err) |
S = N/A O = 2576 T = TO (out)(err) |
S = N/A O = 2830 T = TO (out)(err) |
S = N/A O = 2812 T = TO (out)(err) |
S = N/A O = 11640 T = 1790.37 (out)(err) |
S = OPT O = 2560 T = 55.12 (out)(err) |
S = N/A O = 2917 T = TO (out)(err) |
S = N/A O = N/A T = 184.29 (out)(err) |
S = N/A O = N/A T = 615.67 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_0.wcnf | S = OPT O = 2885 T = 8.91 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2885 T = 8.91 (out)(err) |
S = N/A O = 3388 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2885 T = 8.97 (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 = 2947 T = TO (out)(err) |
S = OPT O = 2885 T = 27.69 (out)(err) |
S = OPT O = 2885 T = 30.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 = 2885 T = 13.63 (out)(err) |
S = N/A O = 2977 T = TO (out)(err) |
S = N/A O = 3293 T = TO (out)(err) |
S = N/A O = 3360 T = TO (out)(err) |
S = N/A O = 14697 T = 1788.29 (out)(err) |
S = N/A O = 2910 T = TO (out)(err) |
S = N/A O = 3447 T = TO (out)(err) |
S = N/A O = N/A T = 318.12 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_1.wcnf | S = OPT O = 2918 T = 5.54 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2918 T = 8.04 (out)(err) |
S = N/A O = 3302 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2918 T = 5.54 (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 = 3064 T = TO (out)(err) |
S = OPT O = 2918 T = 18.77 (out)(err) |
S = OPT O = 2918 T = 16.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 = 2918 T = 9.68 (out)(err) |
S = N/A O = 3013 T = TO (out)(err) |
S = N/A O = 3597 T = TO (out)(err) |
S = N/A O = 3544 T = TO (out)(err) |
S = N/A O = 14786 T = 1788.59 (out)(err) |
S = N/A O = 2918 T = TO (out)(err) |
S = N/A O = 3718 T = TO (out)(err) |
S = N/A O = N/A T = 381.89 (out)(err) |
S = N/A O = N/A T = 499.36 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_2.wcnf | S = OPT O = 2878 T = 3.56 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2878 T = 6.42 (out)(err) |
S = N/A O = 3439 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2878 T = 4.42 (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 = 2878 T = TO (out)(err) |
S = OPT O = 2878 T = 15.23 (out)(err) |
S = OPT O = 2878 T = 14.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 = 2878 T = 3.56 (out)(err) |
S = N/A O = 2968 T = TO (out)(err) |
S = N/A O = 3257 T = TO (out)(err) |
S = N/A O = 3372 T = TO (out)(err) |
S = N/A O = 14633 T = 1789.90 (out)(err) |
S = N/A O = 2878 T = TO (out)(err) |
S = N/A O = 3752 T = TO (out)(err) |
S = N/A O = N/A T = 317.87 (out)(err) |
S = N/A O = N/A T = 1431.67 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_3.wcnf | S = OPT O = 3045 T = 8.78 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3045 T = 8.78 (out)(err) |
S = N/A O = 3416 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3045 T = 9.66 (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 = 3125 T = TO (out)(err) |
S = OPT O = 3045 T = 19.65 (out)(err) |
S = OPT O = 3045 T = 22.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 = 3045 T = 11.26 (out)(err) |
S = N/A O = 3128 T = TO (out)(err) |
S = N/A O = 3550 T = TO (out)(err) |
S = N/A O = 3665 T = TO (out)(err) |
S = N/A O = 14926 T = 1789.68 (out)(err) |
S = N/A O = 3045 T = TO (out)(err) |
S = N/A O = 3656 T = TO (out)(err) |
S = N/A O = N/A T = 429.51 (out)(err) |
S = N/A O = N/A T = 1109.57 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_4.wcnf | S = OPT O = 3021 T = 1.26 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3021 T = 4.23 (out)(err) |
S = N/A O = 3457 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3021 T = 1.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 = 3021 T = TO (out)(err) |
S = OPT O = 3021 T = 3.88 (out)(err) |
S = OPT O = 3021 T = 4.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 = 3021 T = 3.92 (out)(err) |
S = N/A O = 3063 T = TO (out)(err) |
S = N/A O = 3426 T = TO (out)(err) |
S = N/A O = 3523 T = TO (out)(err) |
S = N/A O = 14865 T = 1788.51 (out)(err) |
S = OPT O = 3021 T = 972.84 (out)(err) |
S = N/A O = 3642 T = TO (out)(err) |
S = N/A O = N/A T = 318.02 (out)(err) |
S = N/A O = N/A T = 1279.55 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_5.wcnf | S = OPT O = 2812 T = 10.14 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2812 T = 10.14 (out)(err) |
S = N/A O = 3302 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2812 T = 12.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 = 2877 T = TO (out)(err) |
S = OPT O = 2812 T = 34.73 (out)(err) |
S = OPT O = 2812 T = 35.19 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2812 T = 15.75 (out)(err) |
S = N/A O = 2940 T = TO (out)(err) |
S = N/A O = 3418 T = TO (out)(err) |
S = N/A O = 3376 T = TO (out)(err) |
S = N/A O = 14588 T = 1788.66 (out)(err) |
S = N/A O = 2824 T = TO (out)(err) |
S = N/A O = 3503 T = TO (out)(err) |
S = N/A O = N/A T = 429.40 (out)(err) |
S = N/A O = N/A T = 550.32 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_6.wcnf | S = OPT O = 2838 T = 8.53 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2838 T = 9.05 (out)(err) |
S = N/A O = 3303 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2838 T = 8.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 = 2933 T = TO (out)(err) |
S = OPT O = 2838 T = 24.15 (out)(err) |
S = OPT O = 2838 T = 23.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 = 2838 T = 10.05 (out)(err) |
S = N/A O = 2938 T = TO (out)(err) |
S = N/A O = 3324 T = TO (out)(err) |
S = N/A O = 3341 T = TO (out)(err) |
S = N/A O = 14871 T = 1788.64 (out)(err) |
S = N/A O = 2838 T = TO (out)(err) |
S = N/A O = 3582 T = TO (out)(err) |
S = N/A O = N/A T = 429.43 (out)(err) |
S = N/A O = N/A T = 326.93 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_7.wcnf | S = OPT O = 2815 T = 3.21 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2815 T = 5.33 (out)(err) |
S = N/A O = 3320 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2815 T = 3.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 = 2815 T = TO (out)(err) |
S = OPT O = 2815 T = 10.86 (out)(err) |
S = OPT O = 2815 T = 8.81 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2815 T = 4.39 (out)(err) |
S = N/A O = 2917 T = TO (out)(err) |
S = N/A O = 3308 T = TO (out)(err) |
S = N/A O = 3267 T = TO (out)(err) |
S = N/A O = 14966 T = 1789.47 (out)(err) |
S = N/A O = 2815 T = TO (out)(err) |
S = N/A O = 3590 T = TO (out)(err) |
S = N/A O = N/A T = 429.33 (out)(err) |
S = N/A O = N/A T = 351.39 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_8.wcnf | S = OPT O = 3025 T = 7.22 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3025 T = 8.72 (out)(err) |
S = N/A O = 3433 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3025 T = 7.22 (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 = 3175 T = TO (out)(err) |
S = OPT O = 3025 T = 29.27 (out)(err) |
S = OPT O = 3025 T = 25.91 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3025 T = 11.04 (out)(err) |
S = N/A O = 3139 T = TO (out)(err) |
S = N/A O = 3576 T = TO (out)(err) |
S = N/A O = 3502 T = TO (out)(err) |
S = N/A O = 14986 T = 1789.40 (out)(err) |
S = N/A O = 3025 T = TO (out)(err) |
S = N/A O = 3642 T = TO (out)(err) |
S = N/A O = N/A T = 318.97 (out)(err) |
S = N/A O = N/A T = 948.89 (out)(err) |
file_rwpms_wcnf_L2_V150_C3000_H150_9.wcnf | S = OPT O = 2952 T = 3.33 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2952 T = 5.86 (out)(err) |
S = N/A O = 3523 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2952 T = 3.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 = 2952 T = TO (out)(err) |
S = OPT O = 2952 T = 10.61 (out)(err) |
S = OPT O = 2952 T = 9.95 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 2952 T = 4.13 (out)(err) |
S = N/A O = 3049 T = TO (out)(err) |
S = N/A O = 3530 T = TO (out)(err) |
S = N/A O = 3570 T = TO (out)(err) |
S = N/A O = 14840 T = 1789.33 (out)(err) |
S = N/A O = 2952 T = TO (out)(err) |
S = N/A O = 3866 T = TO (out)(err) |
S = N/A O = N/A T = 429.44 (out)(err) |
S = N/A O = N/A T = 840.95 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_0.wcnf | S = OPT O = 3634 T = 9.40 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3634 T = 16.09 (out)(err) |
S = N/A O = 4183 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3634 T = 9.40 (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 = 3716 T = TO (out)(err) |
S = OPT O = 3634 T = 39.35 (out)(err) |
S = OPT O = 3634 T = 38.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 = 3634 T = 10.80 (out)(err) |
S = N/A O = 3775 T = TO (out)(err) |
S = N/A O = 4261 T = TO (out)(err) |
S = N/A O = 4276 T = TO (out)(err) |
S = N/A O = 17735 T = 1788.02 (out)(err) |
S = N/A O = 3781 T = TO (out)(err) |
S = N/A O = 4259 T = TO (out)(err) |
S = N/A O = N/A T = 429.47 (out)(err) |
S = N/A O = N/A T = 953.34 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_1.wcnf | S = OPT O = 3662 T = 3.21 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3662 T = 5.25 (out)(err) |
S = N/A O = 4129 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3662 T = 3.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 = 3663 T = TO (out)(err) |
S = OPT O = 3662 T = 8.24 (out)(err) |
S = OPT O = 3662 T = 8.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 = 3662 T = 6.59 (out)(err) |
S = N/A O = 3742 T = TO (out)(err) |
S = N/A O = 4228 T = TO (out)(err) |
S = N/A O = 4084 T = TO (out)(err) |
S = N/A O = 17845 T = 1788.83 (out)(err) |
S = N/A O = 3662 T = TO (out)(err) |
S = N/A O = 4729 T = TO (out)(err) |
S = N/A O = N/A T = 429.06 (out)(err) |
S = N/A O = N/A T = 1592.06 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_2.wcnf | S = OPT O = 3827 T = 5.85 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3827 T = 7.05 (out)(err) |
S = N/A O = 4173 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3827 T = 5.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 = 3843 T = TO (out)(err) |
S = OPT O = 3827 T = 18.31 (out)(err) |
S = OPT O = 3827 T = 17.71 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3827 T = 10.07 (out)(err) |
S = N/A O = 3895 T = TO (out)(err) |
S = N/A O = 4292 T = TO (out)(err) |
S = N/A O = 4275 T = TO (out)(err) |
S = N/A O = 17696 T = 1788.94 (out)(err) |
S = N/A O = 3845 T = TO (out)(err) |
S = N/A O = 4379 T = TO (out)(err) |
S = N/A O = N/A T = 429.41 (out)(err) |
S = N/A O = N/A T = 636.55 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_3.wcnf | S = OPT O = 3512 T = 4.15 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3512 T = 6.24 (out)(err) |
S = N/A O = 4043 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3512 T = 4.15 (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 = 3512 T = TO (out)(err) |
S = OPT O = 3512 T = 14.04 (out)(err) |
S = OPT O = 3512 T = 14.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 = 3512 T = 6.19 (out)(err) |
S = N/A O = 3620 T = TO (out)(err) |
S = N/A O = 4187 T = TO (out)(err) |
S = N/A O = 4110 T = TO (out)(err) |
S = N/A O = 17780 T = 1787.92 (out)(err) |
S = N/A O = 3512 T = TO (out)(err) |
S = N/A O = 4341 T = TO (out)(err) |
S = N/A O = N/A T = 429.66 (out)(err) |
S = N/A O = N/A T = 1015.88 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_4.wcnf | S = OPT O = 3355 T = 4.87 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3355 T = 6.42 (out)(err) |
S = N/A O = 3868 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3355 T = 4.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 = 3373 T = TO (out)(err) |
S = OPT O = 3355 T = 16.18 (out)(err) |
S = OPT O = 3355 T = 16.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3355 T = 7.80 (out)(err) |
S = N/A O = 3485 T = TO (out)(err) |
S = N/A O = 3910 T = TO (out)(err) |
S = N/A O = 4026 T = TO (out)(err) |
S = N/A O = 17787 T = 1787.97 (out)(err) |
S = N/A O = 3376 T = TO (out)(err) |
S = N/A O = 4023 T = TO (out)(err) |
S = N/A O = N/A T = 429.00 (out)(err) |
S = N/A O = N/A T = 594.64 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_5.wcnf | S = OPT O = 3450 T = 9.57 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3450 T = 9.57 (out)(err) |
S = N/A O = 3933 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3450 T = 12.83 (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 = 3540 T = TO (out)(err) |
S = OPT O = 3450 T = 47.37 (out)(err) |
S = OPT O = 3450 T = 49.03 (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 = 3450 T = 17.49 (out)(err) |
S = N/A O = 3619 T = TO (out)(err) |
S = N/A O = 4086 T = TO (out)(err) |
S = N/A O = 4013 T = TO (out)(err) |
S = N/A O = 17466 T = 1788.91 (out)(err) |
S = N/A O = 3492 T = TO (out)(err) |
S = N/A O = 4189 T = TO (out)(err) |
S = N/A O = N/A T = 348.69 (out)(err) |
S = N/A O = N/A T = 497.52 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_6.wcnf | S = OPT O = 3654 T = 1.23 |
S = OPT O = 3654 T = 62.55 (out)(err) |
S = OPT O = 3654 T = 4.35 (out)(err) |
S = N/A O = 4056 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3654 T = 1.23 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3654 T = 126.39 (out)(err) |
S = OPT O = 3654 T = 3.00 (out)(err) |
S = OPT O = 3654 T = 3.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 = 3654 T = 3.69 (out)(err) |
S = N/A O = 3794 T = TO (out)(err) |
S = N/A O = 4289 T = TO (out)(err) |
S = N/A O = 4061 T = TO (out)(err) |
S = N/A O = 17666 T = 1789.57 (out)(err) |
S = OPT O = 3654 T = 387.07 (out)(err) |
S = N/A O = 4377 T = TO (out)(err) |
S = N/A O = N/A T = 429.84 (out)(err) |
S = N/A O = N/A T = 1297.26 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_7.wcnf | S = OPT O = 3617 T = 1.93 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3617 T = 5.25 (out)(err) |
S = N/A O = 4226 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3617 T = 1.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 = 3617 T = TO (out)(err) |
S = OPT O = 3617 T = 5.86 (out)(err) |
S = OPT O = 3617 T = 6.14 (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 = 3617 T = 7.40 (out)(err) |
S = N/A O = 3710 T = TO (out)(err) |
S = N/A O = 4114 T = TO (out)(err) |
S = N/A O = 4087 T = TO (out)(err) |
S = N/A O = 17496 T = 1788.36 (out)(err) |
S = OPT O = 3617 T = 1591.39 (out)(err) |
S = N/A O = 3964 T = TO (out)(err) |
S = N/A O = N/A T = 429.18 (out)(err) |
S = N/A O = N/A T = 1053.02 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_8.wcnf | S = OPT O = 3525 T = 2.41 |
S = OPT O = 3525 T = 402.21 (out)(err) |
S = OPT O = 3525 T = 5.00 (out)(err) |
S = N/A O = 4040 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3525 T = 2.41 (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 = 3525 T = 1332.87 (out)(err) |
S = OPT O = 3525 T = 14.03 (out)(err) |
S = OPT O = 3525 T = 8.39 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3525 T = 4.25 (out)(err) |
S = N/A O = 3590 T = TO (out)(err) |
S = N/A O = 4174 T = TO (out)(err) |
S = N/A O = 4282 T = TO (out)(err) |
S = N/A O = 17498 T = 1788.12 (out)(err) |
S = N/A O = 3525 T = TO (out)(err) |
S = N/A O = 4134 T = TO (out)(err) |
S = N/A O = N/A T = 431.88 (out)(err) |
S = N/A O = N/A T = 778.50 (out)(err) |
file_rwpms_wcnf_L2_V150_C3500_H150_9.wcnf | S = OPT O = 3240 T = 5.09 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3240 T = 7.19 (out)(err) |
S = N/A O = 3842 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 3240 T = 6.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 = 3240 T = TO (out)(err) |
S = OPT O = 3240 T = 19.85 (out)(err) |
S = OPT O = 3240 T = 21.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 = 3240 T = 5.09 (out)(err) |
S = N/A O = 3446 T = TO (out)(err) |
S = N/A O = 3854 T = TO (out)(err) |
S = N/A O = 3971 T = TO (out)(err) |
S = N/A O = 17376 T = 1789.39 (out)(err) |
S = N/A O = 3240 T = TO (out)(err) |
S = N/A O = 4208 T = TO (out)(err) |
S = N/A O = N/A T = 572.51 (out)(err) |
S = N/A O = N/A T = 528.43 (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_0.wcnf | S = OPT O = 28 T = 5.75 |
S = OPT O = 28 T = 570.67 (out)(err) |
S = OPT O = 28 T = 8.68 (out)(err) |
S = N/A O = 28 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.81 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 28 T = 685.19 (out)(err) |
S = OPT O = 28 T = 5.85 (out)(err) |
S = OPT O = 28 T = 5.75 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 28 T = 23.17 (out)(err) |
S = N/A O = 28 T = TO (out)(err) |
S = N/A O = 59 T = TO (out)(err) |
S = N/A O = 49 T = TO (out)(err) |
S = N/A O = 71 T = 1790.48 (out)(err) |
S = OPT O = 28 T = 293.27 (out)(err) |
S = N/A O = 135 T = TO (out)(err) |
S = N/A O = N/A T = 779.54 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_1.wcnf | S = OPT O = 15 T = 6.97 |
S = OPT O = 15 T = 163.54 (out)(err) |
S = OPT O = 15 T = 6.97 (out)(err) |
S = OPT O = 15 T = 27.94 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.83 (out)(err) |
S = OPT O = 15 T = 258.31 (out)(err) |
S = OPT O = 15 T = 278.94 (out)(err) |
S = OPT O = 15 T = 254.04 (out)(err) |
S = OPT O = 15 T = 8.30 (out)(err) |
S = OPT O = 15 T = 8.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 = 15 T = 20.66 (out)(err) |
S = N/A O = 23 T = TO (out)(err) |
S = OPT O = 15 T = 737.18 (out)(err) |
S = OPT O = 15 T = 759.47 (out)(err) |
S = N/A O = 78 T = 1791.97 (out)(err) |
S = OPT O = 15 T = 112.96 (out)(err) |
S = N/A O = 174 T = TO (out)(err) |
S = N/A O = N/A T = 1791.49 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_2.wcnf | S = OPT O = 25 T = 7.00 |
S = OPT O = 25 T = 676.14 (out)(err) |
S = OPT O = 25 T = 7.28 (out)(err) |
S = N/A O = 26 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 25 T = 588.48 (out)(err) |
S = OPT O = 25 T = 7.39 (out)(err) |
S = OPT O = 25 T = 7.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 25 T = 22.72 (out)(err) |
S = N/A O = 32 T = TO (out)(err) |
S = N/A O = 27 T = TO (out)(err) |
S = N/A O = 36 T = TO (out)(err) |
S = N/A O = 121 T = 1790.83 (out)(err) |
S = OPT O = 25 T = 404.16 (out)(err) |
S = N/A O = 173 T = TO (out)(err) |
S = N/A O = N/A T = 484.65 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_3.wcnf | S = OPT O = 25 T = 8.25 |
S = OPT O = 25 T = 408.68 (out)(err) |
S = OPT O = 25 T = 8.25 (out)(err) |
S = N/A O = 26 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 25 T = 282.52 (out)(err) |
S = OPT O = 25 T = 11.37 (out)(err) |
S = OPT O = 25 T = 10.93 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 25 T = 10.64 (out)(err) |
S = N/A O = 31 T = TO (out)(err) |
S = N/A O = 32 T = TO (out)(err) |
S = N/A O = 28 T = TO (out)(err) |
S = N/A O = 76 T = 1791.00 (out)(err) |
S = OPT O = 25 T = 238.78 (out)(err) |
S = N/A O = 123 T = TO (out)(err) |
S = N/A O = N/A T = 721.10 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_4.wcnf | S = OPT O = 30 T = 4.12 |
S = OPT O = 30 T = 990.20 (out)(err) |
S = OPT O = 30 T = 7.03 (out)(err) |
S = N/A O = 30 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 30 T = 636.67 (out)(err) |
S = OPT O = 30 T = 4.12 (out)(err) |
S = OPT O = 30 T = 4.37 (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 = 30 T = 37.93 (out)(err) |
S = N/A O = 30 T = TO (out)(err) |
S = N/A O = 30 T = TO (out)(err) |
S = N/A O = 30 T = TO (out)(err) |
S = N/A O = 118 T = 1790.78 (out)(err) |
S = OPT O = 30 T = 306.05 (out)(err) |
S = N/A O = 210 T = TO (out)(err) |
S = N/A O = N/A T = 478.51 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_5.wcnf | S = OPT O = 27 T = 2.70 |
S = OPT O = 27 T = 718.69 (out)(err) |
S = OPT O = 27 T = 6.32 (out)(err) |
S = N/A O = 28 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 27 T = 118.81 (out)(err) |
S = OPT O = 27 T = 3.97 (out)(err) |
S = OPT O = 27 T = 2.70 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 27 T = 20.36 (out)(err) |
S = N/A O = 27 T = TO (out)(err) |
S = N/A O = 39 T = TO (out)(err) |
S = N/A O = 42 T = TO (out)(err) |
S = N/A O = 101 T = 1791.67 (out)(err) |
S = OPT O = 27 T = 150.51 (out)(err) |
S = N/A O = 158 T = TO (out)(err) |
S = N/A O = N/A T = 749.66 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_6.wcnf | S = OPT O = 26 T = 7.86 |
S = OPT O = 26 T = 491.10 (out)(err) |
S = OPT O = 26 T = 9.25 (out)(err) |
S = N/A O = 27 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.94 (out)(err) |
S = OPT O = 26 T = 962.59 (out)(err) |
S = N/A O = 26 T = TO (out)(err) |
S = OPT O = 26 T = 529.36 (out)(err) |
S = OPT O = 26 T = 8.00 (out)(err) |
S = OPT O = 26 T = 7.86 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 26 T = 41.60 (out)(err) |
S = N/A O = 26 T = TO (out)(err) |
S = N/A O = 46 T = TO (out)(err) |
S = N/A O = 37 T = TO (out)(err) |
S = N/A O = 104 T = 1790.35 (out)(err) |
S = OPT O = 26 T = 187.97 (out)(err) |
S = N/A O = 180 T = TO (out)(err) |
S = N/A O = N/A T = 847.69 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_7.wcnf | S = OPT O = 29 T = 10.16 |
S = OPT O = 29 T = 1063.97 (out)(err) |
S = OPT O = 29 T = 10.16 (out)(err) |
S = N/A O = 30 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.81 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 29 T = 863.17 (out)(err) |
S = OPT O = 29 T = 21.63 (out)(err) |
S = OPT O = 29 T = 21.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 = 29 T = 88.57 (out)(err) |
S = N/A O = 37 T = TO (out)(err) |
S = N/A O = 80 T = TO (out)(err) |
S = N/A O = 44 T = TO (out)(err) |
S = N/A O = 93 T = 1799.47 (out)(err) |
S = OPT O = 29 T = 882.83 (out)(err) |
S = N/A O = 229 T = TO (out)(err) |
S = N/A O = N/A T = 929.08 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_8.wcnf | S = OPT O = 19 T = 10.29 |
S = OPT O = 19 T = 483.75 (out)(err) |
S = OPT O = 19 T = 10.29 (out)(err) |
S = OPT O = 19 T = 335.87 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.83 (out)(err) |
S = OPT O = 19 T = 1137.06 (out)(err) |
S = OPT O = 19 T = 1368.58 (out)(err) |
S = OPT O = 19 T = 643.84 (out)(err) |
S = OPT O = 19 T = 15.92 (out)(err) |
S = OPT O = 19 T = 13.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 = 19 T = 33.47 (out)(err) |
S = N/A O = 19 T = TO (out)(err) |
S = N/A O = 27 T = TO (out)(err) |
S = N/A O = 19 T = TO (out)(err) |
S = N/A O = 95 T = 1790.52 (out)(err) |
S = OPT O = 19 T = 256.91 (out)(err) |
S = N/A O = 135 T = TO (out)(err) |
S = N/A O = N/A T = 715.54 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C600_H100_9.wcnf | S = OPT O = 30 T = 7.62 |
S = OPT O = 30 T = 841.68 (out)(err) |
S = OPT O = 30 T = 7.62 (out)(err) |
S = N/A O = 34 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 30 T = 1094.09 (out)(err) |
S = OPT O = 30 T = 10.19 (out)(err) |
S = OPT O = 30 T = 8.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 = 30 T = 42.87 (out)(err) |
S = N/A O = 34 T = TO (out)(err) |
S = N/A O = 39 T = TO (out)(err) |
S = N/A O = 34 T = TO (out)(err) |
S = N/A O = 96 T = 1789.64 (out)(err) |
S = OPT O = 30 T = 598.75 (out)(err) |
S = N/A O = 230 T = TO (out)(err) |
S = N/A O = N/A T = 483.99 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_0.wcnf | S = OPT O = 54 T = 25.37 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 54 T = 25.37 (out)(err) |
S = N/A O = 58 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.83 (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 = 72 T = TO (out)(err) |
S = OPT O = 54 T = 64.95 (out)(err) |
S = OPT O = 54 T = 64.03 (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 = 54 T = 91.62 (out)(err) |
S = N/A O = 66 T = TO (out)(err) |
S = N/A O = 104 T = TO (out)(err) |
S = N/A O = 111 T = TO (out)(err) |
S = N/A O = 156 T = 1789.71 (out)(err) |
S = N/A O = 54 T = TO (out)(err) |
S = N/A O = 260 T = TO (out)(err) |
S = N/A O = N/A T = 647.78 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_1.wcnf | S = OPT O = 58 T = 62.56 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 58 T = 83.06 (out)(err) |
S = N/A O = 84 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 81 T = TO (out)(err) |
S = OPT O = 58 T = 62.56 (out)(err) |
S = OPT O = 58 T = 63.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 = 58 T = 266.38 (out)(err) |
S = N/A O = 60 T = TO (out)(err) |
S = N/A O = 188 T = TO (out)(err) |
S = N/A O = 186 T = TO (out)(err) |
S = N/A O = 165 T = 1790.38 (out)(err) |
S = N/A O = 58 T = TO (out)(err) |
S = N/A O = 232 T = TO (out)(err) |
S = N/A O = N/A T = 382.15 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_2.wcnf | S = OPT O = 59 T = 39.00 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 59 T = 39.00 (out)(err) |
S = N/A O = 65 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 96 T = TO (out)(err) |
S = OPT O = 59 T = 72.48 (out)(err) |
S = OPT O = 59 T = 70.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 = 59 T = 151.10 (out)(err) |
S = N/A O = 70 T = TO (out)(err) |
S = N/A O = 174 T = TO (out)(err) |
S = N/A O = 162 T = TO (out)(err) |
S = N/A O = 183 T = 1789.43 (out)(err) |
S = N/A O = 59 T = TO (out)(err) |
S = N/A O = 243 T = TO (out)(err) |
S = N/A O = N/A T = 286.72 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_3.wcnf | S = OPT O = 48 T = 33.69 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 48 T = 33.69 (out)(err) |
S = N/A O = 49 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.98 (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 = 48 T = TO (out)(err) |
S = OPT O = 48 T = 36.78 (out)(err) |
S = OPT O = 48 T = 36.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 = 48 T = 139.71 (out)(err) |
S = N/A O = 59 T = TO (out)(err) |
S = N/A O = 79 T = TO (out)(err) |
S = N/A O = 118 T = TO (out)(err) |
S = N/A O = 158 T = 1789.53 (out)(err) |
S = N/A O = 48 T = TO (out)(err) |
S = N/A O = 221 T = TO (out)(err) |
S = N/A O = N/A T = 357.65 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_4.wcnf | S = OPT O = 42 T = 9.60 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 42 T = 17.99 (out)(err) |
S = N/A O = 66 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 42 T = 989.60 (out)(err) |
S = OPT O = 42 T = 10.99 (out)(err) |
S = OPT O = 42 T = 9.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 = 42 T = 41.95 (out)(err) |
S = N/A O = 52 T = TO (out)(err) |
S = N/A O = 82 T = TO (out)(err) |
S = N/A O = 97 T = TO (out)(err) |
S = N/A O = 116 T = 1789.47 (out)(err) |
S = OPT O = 42 T = 1300.98 (out)(err) |
S = N/A O = 147 T = TO (out)(err) |
S = N/A O = N/A T = 574.57 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_5.wcnf | S = OPT O = 46 T = 27.75 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 46 T = 27.75 (out)(err) |
S = N/A O = 46 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.83 (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 = 59 T = TO (out)(err) |
S = OPT O = 46 T = 55.24 (out)(err) |
S = OPT O = 46 T = 58.14 (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 = 46 T = 226.60 (out)(err) |
S = N/A O = 52 T = TO (out)(err) |
S = N/A O = 83 T = TO (out)(err) |
S = N/A O = 78 T = TO (out)(err) |
S = N/A O = 156 T = 1789.68 (out)(err) |
S = OPT O = 46 T = 1137.11 (out)(err) |
S = N/A O = 228 T = TO (out)(err) |
S = N/A O = N/A T = 523.45 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_6.wcnf | S = OPT O = 51 T = 35.99 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 51 T = 35.99 (out)(err) |
S = N/A O = 56 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 56 T = TO (out)(err) |
S = OPT O = 51 T = 73.35 (out)(err) |
S = OPT O = 51 T = 73.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 = 51 T = 270.69 (out)(err) |
S = N/A O = 61 T = TO (out)(err) |
S = N/A O = 113 T = TO (out)(err) |
S = N/A O = 105 T = TO (out)(err) |
S = N/A O = 137 T = 1790.44 (out)(err) |
S = N/A O = 51 T = TO (out)(err) |
S = N/A O = 186 T = TO (out)(err) |
S = N/A O = N/A T = 357.24 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_7.wcnf | S = OPT O = 63 T = 39.54 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 63 T = 39.54 (out)(err) |
S = N/A O = 111 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 75 T = TO (out)(err) |
S = OPT O = 63 T = 80.78 (out)(err) |
S = OPT O = 63 T = 83.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 = 63 T = 428.43 (out)(err) |
S = N/A O = 83 T = TO (out)(err) |
S = N/A O = 102 T = TO (out)(err) |
S = N/A O = 102 T = TO (out)(err) |
S = N/A O = 151 T = 1788.92 (out)(err) |
S = N/A O = 63 T = TO (out)(err) |
S = N/A O = 247 T = TO (out)(err) |
S = N/A O = N/A T = 285.55 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_8.wcnf | S = OPT O = 64 T = 76.18 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 64 T = 76.18 (out)(err) |
S = N/A O = 86 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.82 (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 = 65 T = TO (out)(err) |
S = OPT O = 64 T = 143.76 (out)(err) |
S = OPT O = 64 T = 143.70 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 64 T = 1199.19 (out)(err) |
S = N/A O = 72 T = TO (out)(err) |
S = N/A O = 108 T = TO (out)(err) |
S = N/A O = 112 T = TO (out)(err) |
S = N/A O = 161 T = 1788.08 (out)(err) |
S = N/A O = 64 T = TO (out)(err) |
S = N/A O = 316 T = TO (out)(err) |
S = N/A O = N/A T = 375.15 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C700_H100_9.wcnf | S = OPT O = 45 T = 17.79 |
S = N/A O = 45 T = TO (out)(err) |
S = OPT O = 45 T = 17.79 (out)(err) |
S = N/A O = 66 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 45 T = TO (out)(err) |
S = OPT O = 45 T = 27.20 (out)(err) |
S = OPT O = 45 T = 26.17 (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 = 45 T = 123.72 (out)(err) |
S = N/A O = 54 T = TO (out)(err) |
S = N/A O = 99 T = TO (out)(err) |
S = N/A O = 97 T = TO (out)(err) |
S = N/A O = 122 T = 1789.51 (out)(err) |
S = OPT O = 45 T = 1104.59 (out)(err) |
S = N/A O = 167 T = TO (out)(err) |
S = N/A O = N/A T = 360.90 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_0.wcnf | S = OPT O = 95 T = 119.93 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 95 T = 119.93 (out)(err) |
S = N/A O = 140 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 129 T = TO (out)(err) |
S = OPT O = 95 T = 274.96 (out)(err) |
S = OPT O = 95 T = 267.97 (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 = 95 T = TO (out)(err) |
S = N/A O = 118 T = TO (out)(err) |
S = N/A O = 128 T = TO (out)(err) |
S = N/A O = 142 T = TO (out)(err) |
S = N/A O = 1224 T = 1788.88 (out)(err) |
S = N/A O = 95 T = TO (out)(err) |
S = N/A O = 198 T = TO (out)(err) |
S = N/A O = N/A T = 286.14 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_1.wcnf | S = OPT O = 81 T = 81.01 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 81 T = 81.01 (out)(err) |
S = N/A O = 117 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 1.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 = 87 T = TO (out)(err) |
S = OPT O = 81 T = 164.25 (out)(err) |
S = OPT O = 81 T = 162.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 = 81 T = 503.23 (out)(err) |
S = N/A O = 96 T = TO (out)(err) |
S = N/A O = 137 T = TO (out)(err) |
S = N/A O = 136 T = TO (out)(err) |
S = N/A O = 1041 T = 1789.31 (out)(err) |
S = N/A O = 81 T = TO (out)(err) |
S = N/A O = 367 T = TO (out)(err) |
S = N/A O = N/A T = 285.72 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_2.wcnf | S = OPT O = 77 T = 104.21 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 77 T = 104.21 (out)(err) |
S = N/A O = 102 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 104 T = TO (out)(err) |
S = OPT O = 77 T = 204.75 (out)(err) |
S = OPT O = 77 T = 203.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 = 77 T = 440.43 (out)(err) |
S = N/A O = 93 T = TO (out)(err) |
S = N/A O = 192 T = TO (out)(err) |
S = N/A O = 219 T = TO (out)(err) |
S = N/A O = 1227 T = 1789.83 (out)(err) |
S = N/A O = 77 T = TO (out)(err) |
S = N/A O = 288 T = TO (out)(err) |
S = N/A O = N/A T = 287.51 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_3.wcnf | S = OPT O = 81 T = 44.11 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 81 T = 44.11 (out)(err) |
S = N/A O = 90 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 1.00 (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 = 145 T = TO (out)(err) |
S = OPT O = 81 T = 101.01 (out)(err) |
S = OPT O = 81 T = 101.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 = 81 T = 179.78 (out)(err) |
S = N/A O = 99 T = TO (out)(err) |
S = N/A O = 152 T = TO (out)(err) |
S = N/A O = 133 T = TO (out)(err) |
S = N/A O = 1050 T = 1788.74 (out)(err) |
S = N/A O = 82 T = TO (out)(err) |
S = N/A O = 390 T = TO (out)(err) |
S = N/A O = N/A T = 466.18 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_4.wcnf | S = OPT O = 75 T = 99.55 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 75 T = 99.55 (out)(err) |
S = N/A O = 103 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 91 T = TO (out)(err) |
S = OPT O = 75 T = 146.70 (out)(err) |
S = OPT O = 75 T = 147.02 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 75 T = 531.48 (out)(err) |
S = N/A O = 79 T = TO (out)(err) |
S = N/A O = 124 T = TO (out)(err) |
S = N/A O = 151 T = TO (out)(err) |
S = N/A O = 1231 T = 1789.62 (out)(err) |
S = N/A O = 75 T = TO (out)(err) |
S = N/A O = 230 T = TO (out)(err) |
S = N/A O = N/A T = 286.00 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_5.wcnf | S = OPT O = 80 T = 37.40 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 80 T = 37.40 (out)(err) |
S = N/A O = 117 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.89 (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 = 87 T = TO (out)(err) |
S = OPT O = 80 T = 73.47 (out)(err) |
S = OPT O = 80 T = 77.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 = 80 T = 342.79 (out)(err) |
S = N/A O = 93 T = TO (out)(err) |
S = N/A O = 210 T = TO (out)(err) |
S = N/A O = 248 T = TO (out)(err) |
S = N/A O = 1066 T = 1788.91 (out)(err) |
S = N/A O = 80 T = TO (out)(err) |
S = N/A O = 353 T = TO (out)(err) |
S = N/A O = N/A T = 290.47 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_6.wcnf | S = OPT O = 74 T = 49.93 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 74 T = 49.93 (out)(err) |
S = N/A O = 118 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 1.00 (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 = 81 T = TO (out)(err) |
S = OPT O = 74 T = 88.35 (out)(err) |
S = OPT O = 74 T = 87.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 = 74 T = 276.50 (out)(err) |
S = N/A O = 81 T = TO (out)(err) |
S = N/A O = 141 T = TO (out)(err) |
S = N/A O = 120 T = TO (out)(err) |
S = N/A O = 1354 T = 1789.34 (out)(err) |
S = N/A O = 74 T = TO (out)(err) |
S = N/A O = 197 T = TO (out)(err) |
S = N/A O = N/A T = 285.95 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_7.wcnf | S = OPT O = 99 T = 110.12 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 99 T = 110.12 (out)(err) |
S = N/A O = 133 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.82 (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 = 146 T = TO (out)(err) |
S = OPT O = 99 T = 267.42 (out)(err) |
S = OPT O = 99 T = 266.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 = 99 T = 624.77 (out)(err) |
S = N/A O = 122 T = TO (out)(err) |
S = N/A O = 127 T = TO (out)(err) |
S = N/A O = 148 T = TO (out)(err) |
S = N/A O = 1091 T = 1788.85 (out)(err) |
S = N/A O = 99 T = TO (out)(err) |
S = N/A O = 381 T = TO (out)(err) |
S = N/A O = N/A T = 320.73 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_8.wcnf | S = OPT O = 90 T = 223.58 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 90 T = 223.58 (out)(err) |
S = N/A O = 134 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.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 = 113 T = TO (out)(err) |
S = OPT O = 90 T = 448.46 (out)(err) |
S = OPT O = 90 T = 441.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 = 90 T = 805.00 (out)(err) |
S = N/A O = 123 T = TO (out)(err) |
S = N/A O = 133 T = TO (out)(err) |
S = N/A O = 135 T = TO (out)(err) |
S = N/A O = 1166 T = 1789.69 (out)(err) |
S = N/A O = 93 T = TO (out)(err) |
S = N/A O = 276 T = TO (out)(err) |
S = N/A O = N/A T = 291.18 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
file_rwpms_wcnf_L3_V100_C800_H100_9.wcnf | S = OPT O = 95 T = 130.96 |
S = N/A O = N/A T = TO (out)(err) |
S = OPT O = 95 T = 130.96 (out)(err) |
S = N/A O = 129 T = TO (out)(err) |
S = N/A O = N/A T = TO (out)(err) |
S = N/A O = N/A T = 0.83 (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 = 120 T = TO (out)(err) |
S = OPT O = 95 T = 249.34 (out)(err) |
S = OPT O = 95 T = 251.03 (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 = 95 T = 1136.33 (out)(err) |
S = N/A O = 120 T = TO (out)(err) |
S = N/A O = 217 T = TO (out)(err) |
S = N/A O = 217 T = TO (out)(err) |
S = N/A O = 1182 T = 1789.85 (out)(err) |
S = N/A O = 95 T = TO (out)(err) |
S = N/A O = 225 T = TO (out)(err) |
S = N/A O = N/A T = 289.37 (out)(err) |
S = N/A O = N/A T = TO (out)(err) |