Benchmark

Label	Meaning
S	Solution {OPTIMUM FOUND or OPT \| UNSATISFIABLE or UNSAT \| UNKNOWN \| Not available or N/A}
O	Best solution found
T	CPU time (TO for Time Out)
(out)(err)	Standard output and standard error for each solver

Color	Meaning
Text	Best solver column
Text	Optimal solution with the best CPU time
Text	Optimal solution and finished within the Time Out
Text	Optimal solution and did not finish within the Time Out
Text	Time Out
Text	Buggy solution

Instance file name	Best solver	IncWMaxSatz	WMaxSatz+	WMaxSatz-2009	WPM1	WPM2	akmaxsat	akmaxsat_ls	claspMaxSat	sat4j-maxsat	wbo1.6
file_rwpms_wcnf_L2_V150_C4000_H150_0.wcnf	S = OPT O = 4231 T = 0.62	S = OPT O = 4231 T = 2.53 (out)(err)	S = OPT O = 4231 T = 1.82 (out)(err)	S = OPT O = 4231 T = 1.97 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 81.80 (out)(err)	S = OPT O = 4231 T = 0.62 (out)(err)	S = OPT O = 4231 T = 1.04 (out)(err)	S = N/A O = 4595 T = TO (out)(err)	S = N/A O = 4619 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_1.wcnf	S = UNSAT O = N/A T = 0.01	S = UNSAT O = 21959 T = 0.15 (out)(err)	S = UNSAT O = 21959 T = 0.07 (out)(err)	S = UNSAT O = 21959 T = 0.07 (out)(err)	S = UNSAT O = N/A T = 0.01 (out)(err)	S = N/A O = N/A T = 0.08 (out)(err)	S = UNSAT O = N/A T = 0.07 (out)(err)	S = UNSAT O = 21959 T = 0.78 (out)(err)	S = UNSAT O = N/A T = 0.02 (out)(err)	S = UNSAT O = N/A T = 1.19 (out)(err)	S = UNSAT O = N/A T = 0.01 (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_2.wcnf	S = OPT O = 4235 T = 1.51	S = OPT O = 4235 T = 7.45 (out)(err)	S = OPT O = 4235 T = 7.61 (out)(err)	S = OPT O = 4235 T = 6.50 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 35.20 (out)(err)	S = OPT O = 4235 T = 1.51 (out)(err)	S = OPT O = 4235 T = 1.70 (out)(err)	S = N/A O = 4829 T = TO (out)(err)	S = N/A O = 4747 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_3.wcnf	S = OPT O = 4037 T = 3.03	S = OPT O = 4037 T = 44.55 (out)(err)	S = OPT O = 4037 T = 13.51 (out)(err)	S = OPT O = 4037 T = 13.57 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 29.43 (out)(err)	S = OPT O = 4037 T = 3.50 (out)(err)	S = OPT O = 4037 T = 3.03 (out)(err)	S = N/A O = 4718 T = TO (out)(err)	S = N/A O = 4755 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_4.wcnf	S = OPT O = 4031 T = 3.36	S = OPT O = 4031 T = 91.59 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4031 T = 32.51 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 16.24 (out)(err)	S = OPT O = 4031 T = 10.67 (out)(err)	S = OPT O = 4031 T = 3.36 (out)(err)	S = N/A O = 4573 T = TO (out)(err)	S = N/A O = 4697 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_5.wcnf	S = OPT O = 4144 T = 7.60	S = OPT O = 4144 T = 172.94 (out)(err)	S = OPT O = 4144 T = 77.91 (out)(err)	S = OPT O = 4144 T = 78.67 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 48.24 (out)(err)	S = OPT O = 4144 T = 18.62 (out)(err)	S = OPT O = 4144 T = 7.60 (out)(err)	S = N/A O = 4799 T = TO (out)(err)	S = N/A O = 4814 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_6.wcnf	S = OPT O = 4149 T = 12.05	S = OPT O = 4149 T = 169.66 (out)(err)	S = OPT O = 4149 T = 80.15 (out)(err)	S = OPT O = 4149 T = 79.91 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 6.96 (out)(err)	S = OPT O = 4149 T = 20.61 (out)(err)	S = OPT O = 4149 T = 12.05 (out)(err)	S = N/A O = 4636 T = TO (out)(err)	S = N/A O = 4813 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_7.wcnf	S = OPT O = 4043 T = 4.63	S = OPT O = 4043 T = 306.69 (out)(err)	S = OPT O = 4043 T = 105.22 (out)(err)	S = OPT O = 4043 T = 108.47 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 58.72 (out)(err)	S = OPT O = 4043 T = 19.53 (out)(err)	S = OPT O = 4043 T = 4.63 (out)(err)	S = N/A O = 4656 T = TO (out)(err)	S = N/A O = 4669 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_8.wcnf	S = OPT O = 4078 T = 10.47	S = OPT O = 4078 T = 538.09 (out)(err)	S = OPT O = 4078 T = 169.73 (out)(err)	S = OPT O = 4078 T = 171.93 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 23.63 (out)(err)	S = OPT O = 4078 T = 30.28 (out)(err)	S = OPT O = 4078 T = 10.47 (out)(err)	S = N/A O = 4771 T = TO (out)(err)	S = N/A O = 4720 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_9.wcnf	S = OPT O = 4328 T = 3.83	S = OPT O = 4328 T = 71.59 (out)(err)	S = OPT O = 4328 T = 20.16 (out)(err)	S = OPT O = 4328 T = 19.72 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 47.32 (out)(err)	S = OPT O = 4328 T = 6.72 (out)(err)	S = OPT O = 4328 T = 3.83 (out)(err)	S = N/A O = 4839 T = TO (out)(err)	S = N/A O = 4938 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_0.wcnf	S = OPT O = 4572 T = 9.10	S = OPT O = 4572 T = 766.13 (out)(err)	S = OPT O = 4572 T = 139.56 (out)(err)	S = OPT O = 4572 T = 134.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 = 4572 T = 25.82 (out)(err)	S = OPT O = 4572 T = 9.10 (out)(err)	S = N/A O = 5281 T = TO (out)(err)	S = N/A O = 5409 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_1.wcnf	S = OPT O = 4967 T = 10.62	S = OPT O = 4967 T = 485.36 (out)(err)	S = OPT O = 4967 T = 149.62 (out)(err)	S = OPT O = 4967 T = 150.41 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 230.75 (out)(err)	S = OPT O = 4967 T = 26.43 (out)(err)	S = OPT O = 4967 T = 10.62 (out)(err)	S = N/A O = 5527 T = TO (out)(err)	S = N/A O = 5623 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_2.wcnf	S = OPT O = 4961 T = 4.75	S = OPT O = 4961 T = 87.03 (out)(err)	S = OPT O = 4961 T = 29.87 (out)(err)	S = OPT O = 4961 T = 29.21 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 171.77 (out)(err)	S = OPT O = 4961 T = 7.08 (out)(err)	S = OPT O = 4961 T = 4.75 (out)(err)	S = N/A O = 5434 T = TO (out)(err)	S = N/A O = 5567 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_3.wcnf	S = OPT O = 4614 T = 2.88	S = OPT O = 4614 T = 28.85 (out)(err)	S = OPT O = 4614 T = 16.66 (out)(err)	S = OPT O = 4614 T = 16.61 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 113.00 (out)(err)	S = OPT O = 4614 T = 2.88 (out)(err)	S = OPT O = 4614 T = 3.12 (out)(err)	S = N/A O = 5262 T = TO (out)(err)	S = N/A O = 5329 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_4.wcnf	S = OPT O = 4794 T = 19.56	S = OPT O = 4794 T = 946.37 (out)(err)	S = OPT O = 4794 T = 163.75 (out)(err)	S = OPT O = 4794 T = 165.65 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 26.88 (out)(err)	S = OPT O = 4794 T = 37.54 (out)(err)	S = OPT O = 4794 T = 19.56 (out)(err)	S = N/A O = 5379 T = TO (out)(err)	S = N/A O = 5424 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_5.wcnf	S = OPT O = 4687 T = 7.23	S = OPT O = 4687 T = 171.47 (out)(err)	S = OPT O = 4687 T = 42.12 (out)(err)	S = OPT O = 4687 T = 42.47 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 5.46 (out)(err)	S = OPT O = 4687 T = 11.94 (out)(err)	S = OPT O = 4687 T = 7.23 (out)(err)	S = N/A O = 5280 T = TO (out)(err)	S = N/A O = 5440 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_6.wcnf	S = OPT O = 4605 T = 2.58	S = OPT O = 4605 T = 199.60 (out)(err)	S = OPT O = 4605 T = 68.23 (out)(err)	S = OPT O = 4605 T = 68.55 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 55.12 (out)(err)	S = OPT O = 4605 T = 12.88 (out)(err)	S = OPT O = 4605 T = 2.58 (out)(err)	S = N/A O = 5187 T = TO (out)(err)	S = N/A O = 5381 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_7.wcnf	S = OPT O = 4710 T = 7.72	S = OPT O = 4710 T = 237.48 (out)(err)	S = OPT O = 4710 T = 56.58 (out)(err)	S = OPT O = 4710 T = 55.98 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 74.50 (out)(err)	S = OPT O = 4710 T = 13.71 (out)(err)	S = OPT O = 4710 T = 7.72 (out)(err)	S = N/A O = 5338 T = TO (out)(err)	S = N/A O = 5400 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_8.wcnf	S = OPT O = 4945 T = 3.46	S = OPT O = 4945 T = 64.23 (out)(err)	S = OPT O = 4945 T = 32.41 (out)(err)	S = OPT O = 4945 T = 33.67 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 22.42 (out)(err)	S = OPT O = 4945 T = 9.89 (out)(err)	S = OPT O = 4945 T = 3.46 (out)(err)	S = N/A O = 5475 T = TO (out)(err)	S = N/A O = 5508 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_9.wcnf	S = OPT O = 5023 T = 6.08	S = OPT O = 5023 T = 105.11 (out)(err)	S = OPT O = 5023 T = 51.87 (out)(err)	S = OPT O = 5023 T = 51.72 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 64.73 (out)(err)	S = OPT O = 5023 T = 12.76 (out)(err)	S = OPT O = 5023 T = 6.08 (out)(err)	S = N/A O = 5380 T = TO (out)(err)	S = N/A O = 5573 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_0.wcnf	S = OPT O = 5362 T = 2.21	S = OPT O = 5362 T = 70.07 (out)(err)	S = OPT O = 5362 T = 33.43 (out)(err)	S = OPT O = 5362 T = 33.26 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 8.18 (out)(err)	S = OPT O = 5362 T = 8.18 (out)(err)	S = OPT O = 5362 T = 2.21 (out)(err)	S = N/A O = 5998 T = TO (out)(err)	S = N/A O = 6053 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_1.wcnf	S = OPT O = 5338 T = 2.12	S = OPT O = 5338 T = 146.78 (out)(err)	S = OPT O = 5338 T = 64.94 (out)(err)	S = OPT O = 5338 T = 69.58 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 44.56 (out)(err)	S = OPT O = 5338 T = 15.50 (out)(err)	S = OPT O = 5338 T = 2.12 (out)(err)	S = N/A O = 5968 T = TO (out)(err)	S = N/A O = 6137 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_2.wcnf	S = OPT O = 5312 T = 4.77	S = OPT O = 5312 T = 493.66 (out)(err)	S = OPT O = 5312 T = 144.13 (out)(err)	S = OPT O = 5312 T = 143.08 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1.36 (out)(err)	S = OPT O = 5312 T = 23.64 (out)(err)	S = OPT O = 5312 T = 4.77 (out)(err)	S = N/A O = 6155 T = TO (out)(err)	S = N/A O = 6131 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_3.wcnf	S = OPT O = 5507 T = 5.44	S = OPT O = 5507 T = 96.41 (out)(err)	S = OPT O = 5507 T = 29.27 (out)(err)	S = OPT O = 5507 T = 29.71 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 21.87 (out)(err)	S = OPT O = 5507 T = 8.18 (out)(err)	S = OPT O = 5507 T = 5.44 (out)(err)	S = N/A O = 5947 T = TO (out)(err)	S = N/A O = 6219 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_4.wcnf	S = OPT O = 5451 T = 24.09	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 5451 T = 345.56 (out)(err)	S = OPT O = 5451 T = 343.69 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 247.62 (out)(err)	S = OPT O = 5451 T = 87.36 (out)(err)	S = OPT O = 5451 T = 24.09 (out)(err)	S = N/A O = 6036 T = TO (out)(err)	S = N/A O = 6218 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_5.wcnf	S = OPT O = 5308 T = 4.23	S = OPT O = 5308 T = 172.64 (out)(err)	S = OPT O = 5308 T = 50.88 (out)(err)	S = OPT O = 5308 T = 52.65 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 36.19 (out)(err)	S = OPT O = 5308 T = 7.76 (out)(err)	S = OPT O = 5308 T = 4.23 (out)(err)	S = N/A O = 5955 T = TO (out)(err)	S = N/A O = 6015 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_6.wcnf	S = OPT O = 5428 T = 5.48	S = OPT O = 5428 T = 175.63 (out)(err)	S = OPT O = 5428 T = 59.17 (out)(err)	S = OPT O = 5428 T = 58.21 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 29.92 (out)(err)	S = OPT O = 5428 T = 11.42 (out)(err)	S = OPT O = 5428 T = 5.48 (out)(err)	S = N/A O = 6023 T = TO (out)(err)	S = N/A O = 6029 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_7.wcnf	S = OPT O = 5468 T = 11.67	S = OPT O = 5468 T = 582.98 (out)(err)	S = OPT O = 5468 T = 214.74 (out)(err)	S = OPT O = 5468 T = 207.43 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 9.50 (out)(err)	S = OPT O = 5468 T = 28.48 (out)(err)	S = OPT O = 5468 T = 11.67 (out)(err)	S = N/A O = 5958 T = TO (out)(err)	S = N/A O = 5952 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_8.wcnf	S = OPT O = 5339 T = 2.15	S = OPT O = 5339 T = 16.36 (out)(err)	S = OPT O = 5339 T = 13.06 (out)(err)	S = OPT O = 5339 T = 12.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 = 5339 T = 5.82 (out)(err)	S = OPT O = 5339 T = 2.15 (out)(err)	S = N/A O = 5923 T = TO (out)(err)	S = N/A O = 5955 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_9.wcnf	S = OPT O = 5376 T = 3.15	S = OPT O = 5376 T = 135.50 (out)(err)	S = OPT O = 5376 T = 26.03 (out)(err)	S = OPT O = 5376 T = 26.93 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 692.97 (out)(err)	S = OPT O = 5376 T = 11.36 (out)(err)	S = OPT O = 5376 T = 3.15 (out)(err)	S = N/A O = 6070 T = TO (out)(err)	S = N/A O = 6163 T = TO (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.10	S = OPT O = 626 T = 0.10 (out)(err)	S = OPT O = 626 T = 0.18 (out)(err)	S = OPT O = 626 T = 0.18 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 9.64 (out)(err)	S = OPT O = 626 T = 0.14 (out)(err)	S = OPT O = 626 T = 0.39 (out)(err)	S = N/A O = 746 T = TO (out)(err)	S = N/A O = 756 T = TO (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.19	S = OPT O = 745 T = 0.19 (out)(err)	S = OPT O = 745 T = 0.35 (out)(err)	S = OPT O = 745 T = 0.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 = 745 T = 0.33 (out)(err)	S = OPT O = 745 T = 0.58 (out)(err)	S = N/A O = 811 T = TO (out)(err)	S = N/A O = 876 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_2.wcnf	S = OPT O = 629 T = 0.07	S = OPT O = 629 T = 0.07 (out)(err)	S = OPT O = 629 T = 0.09 (out)(err)	S = OPT O = 629 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 = 629 T = 0.08 (out)(err)	S = OPT O = 629 T = 0.34 (out)(err)	S = N/A O = 746 T = TO (out)(err)	S = N/A O = 746 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_3.wcnf	S = OPT O = 723 T = 0.33	S = OPT O = 723 T = 0.33 (out)(err)	S = OPT O = 723 T = 0.56 (out)(err)	S = OPT O = 723 T = 0.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 = 723 T = 0.36 (out)(err)	S = OPT O = 723 T = 0.47 (out)(err)	S = N/A O = 847 T = TO (out)(err)	S = N/A O = 873 T = TO (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.09	S = OPT O = 737 T = 0.09 (out)(err)	S = OPT O = 737 T = 0.14 (out)(err)	S = OPT O = 737 T = 0.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 = 737 T = 0.11 (out)(err)	S = OPT O = 737 T = 0.35 (out)(err)	S = N/A O = 836 T = TO (out)(err)	S = N/A O = 856 T = TO (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.08	S = OPT O = 668 T = 0.08 (out)(err)	S = OPT O = 668 T = 0.14 (out)(err)	S = OPT O = 668 T = 0.12 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 0.52 (out)(err)	S = OPT O = 668 T = 0.14 (out)(err)	S = OPT O = 668 T = 0.37 (out)(err)	S = N/A O = 749 T = TO (out)(err)	S = N/A O = 721 T = TO (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.04	S = OPT O = 641 T = 0.04 (out)(err)	S = OPT O = 641 T = 0.07 (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 = 1.28 (out)(err)	S = OPT O = 641 T = 0.05 (out)(err)	S = OPT O = 641 T = 0.34 (out)(err)	S = N/A O = 723 T = TO (out)(err)	S = N/A O = 759 T = TO (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.16	S = OPT O = 688 T = 0.16 (out)(err)	S = OPT O = 688 T = 0.25 (out)(err)	S = OPT O = 688 T = 0.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 = 688 T = 0.21 (out)(err)	S = OPT O = 688 T = 0.45 (out)(err)	S = N/A O = 767 T = TO (out)(err)	S = N/A O = 784 T = TO (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.23	S = OPT O = 577 T = 0.23 (out)(err)	S = OPT O = 577 T = 0.31 (out)(err)	S = OPT O = 577 T = 0.30 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 0.97 (out)(err)	S = OPT O = 577 T = 0.29 (out)(err)	S = OPT O = 577 T = 0.47 (out)(err)	S = N/A O = 757 T = TO (out)(err)	S = N/A O = 739 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_9.wcnf	S = OPT O = 714 T = 0.08	S = OPT O = 714 T = 0.08 (out)(err)	S = OPT O = 714 T = 0.11 (out)(err)	S = OPT O = 714 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 = 714 T = 0.13 (out)(err)	S = OPT O = 714 T = 0.36 (out)(err)	S = N/A O = 835 T = TO (out)(err)	S = N/A O = 819 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_0.wcnf	S = OPT O = 1121 T = 1.49	S = OPT O = 1121 T = 2.63 (out)(err)	S = OPT O = 1121 T = 2.32 (out)(err)	S = OPT O = 1121 T = 2.27 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 711.96 (out)(err)	S = OPT O = 1121 T = 1.55 (out)(err)	S = OPT O = 1121 T = 1.49 (out)(err)	S = N/A O = 1306 T = TO (out)(err)	S = N/A O = 1384 T = TO (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.53	S = OPT O = 1142 T = 0.53 (out)(err)	S = OPT O = 1142 T = 1.13 (out)(err)	S = OPT O = 1142 T = 1.11 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 2.53 (out)(err)	S = OPT O = 1142 T = 0.74 (out)(err)	S = OPT O = 1142 T = 0.57 (out)(err)	S = N/A O = 1353 T = TO (out)(err)	S = N/A O = 1322 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_2.wcnf	S = OPT O = 1252 T = 0.86	S = OPT O = 1252 T = 1.59 (out)(err)	S = OPT O = 1252 T = 1.77 (out)(err)	S = OPT O = 1252 T = 1.77 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 49.45 (out)(err)	S = OPT O = 1252 T = 0.86 (out)(err)	S = OPT O = 1252 T = 0.92 (out)(err)	S = N/A O = 1509 T = TO (out)(err)	S = N/A O = 1586 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_3.wcnf	S = OPT O = 1295 T = 0.71	S = OPT O = 1295 T = 1.33 (out)(err)	S = OPT O = 1295 T = 0.99 (out)(err)	S = OPT O = 1295 T = 0.97 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 4.78 (out)(err)	S = OPT O = 1295 T = 0.71 (out)(err)	S = OPT O = 1295 T = 0.71 (out)(err)	S = N/A O = 1464 T = TO (out)(err)	S = N/A O = 1475 T = TO (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.91	S = OPT O = 1261 T = 1.03 (out)(err)	S = OPT O = 1261 T = 1.64 (out)(err)	S = OPT O = 1261 T = 1.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 = 1261 T = 0.91 (out)(err)	S = OPT O = 1261 T = 1.05 (out)(err)	S = N/A O = 1495 T = TO (out)(err)	S = N/A O = 1561 T = TO (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 = 0.64	S = OPT O = 1047 T = 2.35 (out)(err)	S = OPT O = 1047 T = 3.80 (out)(err)	S = OPT O = 1047 T = 3.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 = 1047 T = 2.09 (out)(err)	S = OPT O = 1047 T = 0.64 (out)(err)	S = N/A O = 1314 T = TO (out)(err)	S = N/A O = 1292 T = TO (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.16	S = OPT O = 1175 T = 0.20 (out)(err)	S = OPT O = 1175 T = 0.23 (out)(err)	S = OPT O = 1175 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 = 1175 T = 0.16 (out)(err)	S = OPT O = 1175 T = 0.49 (out)(err)	S = N/A O = 1350 T = TO (out)(err)	S = N/A O = 1361 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_7.wcnf	S = OPT O = 1145 T = 0.79	S = OPT O = 1145 T = 1.29 (out)(err)	S = OPT O = 1145 T = 1.56 (out)(err)	S = OPT O = 1145 T = 1.70 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 7.35 (out)(err)	S = OPT O = 1145 T = 1.04 (out)(err)	S = OPT O = 1145 T = 0.79 (out)(err)	S = N/A O = 1357 T = TO (out)(err)	S = N/A O = 1359 T = TO (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.24	S = OPT O = 1135 T = 2.17 (out)(err)	S = OPT O = 1135 T = 3.20 (out)(err)	S = OPT O = 1135 T = 3.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 = 1135 T = 1.46 (out)(err)	S = OPT O = 1135 T = 1.24 (out)(err)	S = N/A O = 1380 T = TO (out)(err)	S = N/A O = 1359 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_9.wcnf	S = OPT O = 1232 T = 1.11	S = OPT O = 1232 T = 1.64 (out)(err)	S = OPT O = 1232 T = 2.21 (out)(err)	S = OPT O = 1232 T = 2.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 = 1232 T = 1.25 (out)(err)	S = OPT O = 1232 T = 1.11 (out)(err)	S = N/A O = 1434 T = TO (out)(err)	S = N/A O = 1436 T = TO (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.39	S = OPT O = 1842 T = 5.24 (out)(err)	S = OPT O = 1842 T = 7.21 (out)(err)	S = OPT O = 1842 T = 6.92 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 20.69 (out)(err)	S = OPT O = 1842 T = 2.88 (out)(err)	S = OPT O = 1842 T = 1.39 (out)(err)	S = N/A O = 2173 T = TO (out)(err)	S = N/A O = 2208 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_1.wcnf	S = OPT O = 1699 T = 0.90	S = OPT O = 1699 T = 1.95 (out)(err)	S = OPT O = 1699 T = 1.47 (out)(err)	S = OPT O = 1699 T = 1.49 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 4.63 (out)(err)	S = OPT O = 1699 T = 0.90 (out)(err)	S = OPT O = 1699 T = 1.10 (out)(err)	S = N/A O = 2081 T = TO (out)(err)	S = N/A O = 2100 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_2.wcnf	S = OPT O = 1730 T = 1.19	S = OPT O = 1730 T = 3.01 (out)(err)	S = OPT O = 1730 T = 4.91 (out)(err)	S = OPT O = 1730 T = 4.44 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 1730 T = 1.39 (out)(err)	S = OPT O = 1730 T = 1.19 (out)(err)	S = N/A O = 2102 T = TO (out)(err)	S = N/A O = 2122 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_3.wcnf	S = OPT O = 1885 T = 1.04	S = OPT O = 1885 T = 3.41 (out)(err)	S = OPT O = 1885 T = 4.54 (out)(err)	S = OPT O = 1885 T = 4.49 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 6.98 (out)(err)	S = OPT O = 1885 T = 2.07 (out)(err)	S = OPT O = 1885 T = 1.04 (out)(err)	S = N/A O = 2089 T = TO (out)(err)	S = N/A O = 2197 T = TO (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.95	S = OPT O = 2043 T = 1.65 (out)(err)	S = OPT O = 2043 T = 2.38 (out)(err)	S = OPT O = 2043 T = 2.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 = 2043 T = 0.98 (out)(err)	S = OPT O = 2043 T = 0.95 (out)(err)	S = N/A O = 2237 T = TO (out)(err)	S = N/A O = 2281 T = TO (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 = 1.12	S = OPT O = 1818 T = 14.48 (out)(err)	S = OPT O = 1818 T = 6.95 (out)(err)	S = OPT O = 1818 T = 6.99 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 17.66 (out)(err)	S = OPT O = 1818 T = 5.55 (out)(err)	S = OPT O = 1818 T = 1.12 (out)(err)	S = N/A O = 2121 T = TO (out)(err)	S = N/A O = 2056 T = TO (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.60	S = OPT O = 1832 T = 0.72 (out)(err)	S = OPT O = 1832 T = 1.17 (out)(err)	S = OPT O = 1832 T = 1.16 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 9.00 (out)(err)	S = OPT O = 1832 T = 0.60 (out)(err)	S = OPT O = 1832 T = 0.62 (out)(err)	S = N/A O = 2191 T = TO (out)(err)	S = N/A O = 2097 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_7.wcnf	S = OPT O = 1780 T = 1.21	S = OPT O = 1780 T = 3.86 (out)(err)	S = OPT O = 1780 T = 3.44 (out)(err)	S = OPT O = 1780 T = 3.45 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 28.06 (out)(err)	S = OPT O = 1780 T = 1.71 (out)(err)	S = OPT O = 1780 T = 1.21 (out)(err)	S = N/A O = 2049 T = TO (out)(err)	S = N/A O = 2064 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_8.wcnf	S = OPT O = 1726 T = 0.92	S = OPT O = 1726 T = 1.83 (out)(err)	S = OPT O = 1726 T = 2.94 (out)(err)	S = OPT O = 1726 T = 2.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 = 1726 T = 1.78 (out)(err)	S = OPT O = 1726 T = 0.92 (out)(err)	S = N/A O = 2008 T = TO (out)(err)	S = N/A O = 2072 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_9.wcnf	S = OPT O = 1807 T = 3.52	S = OPT O = 1807 T = 16.21 (out)(err)	S = OPT O = 1807 T = 11.85 (out)(err)	S = OPT O = 1807 T = 12.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 = 1807 T = 4.36 (out)(err)	S = OPT O = 1807 T = 3.52 (out)(err)	S = N/A O = 2111 T = TO (out)(err)	S = N/A O = 2191 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_0.wcnf	S = OPT O = 2414 T = 0.94	S = OPT O = 2414 T = 2.82 (out)(err)	S = OPT O = 2414 T = 2.82 (out)(err)	S = OPT O = 2414 T = 2.81 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 10.56 (out)(err)	S = OPT O = 2414 T = 1.71 (out)(err)	S = OPT O = 2414 T = 0.94 (out)(err)	S = N/A O = 2772 T = TO (out)(err)	S = N/A O = 2813 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_1.wcnf	S = OPT O = 2398 T = 1.68	S = OPT O = 2398 T = 10.11 (out)(err)	S = OPT O = 2398 T = 6.90 (out)(err)	S = OPT O = 2398 T = 6.98 (out)(err)	S = N/A O = N/A T = 109.07 (out)(err)	S = N/A O = N/A T = 16.12 (out)(err)	S = OPT O = 2398 T = 1.86 (out)(err)	S = OPT O = 2398 T = 1.68 (out)(err)	S = N/A O = 2735 T = TO (out)(err)	S = N/A O = 2680 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_2.wcnf	S = OPT O = 2113 T = 1.02	S = OPT O = 2113 T = 15.69 (out)(err)	S = OPT O = 2113 T = 12.72 (out)(err)	S = OPT O = 2113 T = 12.73 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 154.95 (out)(err)	S = OPT O = 2113 T = 3.58 (out)(err)	S = OPT O = 2113 T = 1.02 (out)(err)	S = N/A O = 2626 T = TO (out)(err)	S = N/A O = 2644 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_3.wcnf	S = OPT O = 2339 T = 2.31	S = OPT O = 2339 T = 10.78 (out)(err)	S = OPT O = 2339 T = 9.86 (out)(err)	S = OPT O = 2339 T = 10.71 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 13.72 (out)(err)	S = OPT O = 2339 T = 3.14 (out)(err)	S = OPT O = 2339 T = 2.31 (out)(err)	S = N/A O = 2766 T = TO (out)(err)	S = N/A O = 2821 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_4.wcnf	S = OPT O = 2390 T = 1.08	S = OPT O = 2390 T = 4.62 (out)(err)	S = OPT O = 2390 T = 2.79 (out)(err)	S = OPT O = 2390 T = 2.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 = 2390 T = 1.08 (out)(err)	S = OPT O = 2390 T = 1.12 (out)(err)	S = N/A O = 2672 T = TO (out)(err)	S = N/A O = 2765 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_5.wcnf	S = OPT O = 2332 T = 0.86	S = OPT O = 2332 T = 1.40 (out)(err)	S = OPT O = 2332 T = 1.36 (out)(err)	S = OPT O = 2332 T = 1.34 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 12.71 (out)(err)	S = OPT O = 2332 T = 0.86 (out)(err)	S = OPT O = 2332 T = 1.05 (out)(err)	S = N/A O = 2766 T = TO (out)(err)	S = N/A O = 2832 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_6.wcnf	S = OPT O = 2488 T = 2.05	S = OPT O = 2488 T = 8.09 (out)(err)	S = OPT O = 2488 T = 6.49 (out)(err)	S = OPT O = 2488 T = 6.61 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 7.08 (out)(err)	S = OPT O = 2488 T = 2.25 (out)(err)	S = OPT O = 2488 T = 2.05 (out)(err)	S = N/A O = 2841 T = TO (out)(err)	S = N/A O = 2871 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_7.wcnf	S = OPT O = 2241 T = 1.58	S = OPT O = 2241 T = 18.11 (out)(err)	S = OPT O = 2241 T = 13.68 (out)(err)	S = OPT O = 2241 T = 13.82 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 27.07 (out)(err)	S = OPT O = 2241 T = 6.02 (out)(err)	S = OPT O = 2241 T = 1.58 (out)(err)	S = N/A O = 2677 T = TO (out)(err)	S = N/A O = 2600 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_8.wcnf	S = OPT O = 2353 T = 2.15	S = OPT O = 2353 T = 16.37 (out)(err)	S = OPT O = 2353 T = 11.85 (out)(err)	S = OPT O = 2353 T = 11.88 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1.92 (out)(err)	S = OPT O = 2353 T = 3.77 (out)(err)	S = OPT O = 2353 T = 2.15 (out)(err)	S = N/A O = 2799 T = TO (out)(err)	S = N/A O = 2754 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_9.wcnf	S = OPT O = 2560 T = 0.72	S = OPT O = 2560 T = 1.34 (out)(err)	S = OPT O = 2560 T = 2.65 (out)(err)	S = OPT O = 2560 T = 2.58 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 5.23 (out)(err)	S = OPT O = 2560 T = 0.72 (out)(err)	S = OPT O = 2560 T = 0.82 (out)(err)	S = N/A O = 2829 T = TO (out)(err)	S = N/A O = 2941 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_0.wcnf	S = OPT O = 2885 T = 8.76	S = OPT O = 2885 T = 89.32 (out)(err)	S = OPT O = 2885 T = 44.93 (out)(err)	S = OPT O = 2885 T = 50.49 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 6.50 (out)(err)	S = OPT O = 2885 T = 11.57 (out)(err)	S = OPT O = 2885 T = 8.76 (out)(err)	S = N/A O = 3247 T = TO (out)(err)	S = N/A O = 3268 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_1.wcnf	S = OPT O = 2918 T = 5.01	S = OPT O = 2918 T = 77.96 (out)(err)	S = OPT O = 2918 T = 27.49 (out)(err)	S = OPT O = 2918 T = 27.47 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 18.56 (out)(err)	S = OPT O = 2918 T = 9.60 (out)(err)	S = OPT O = 2918 T = 5.01 (out)(err)	S = N/A O = 3369 T = TO (out)(err)	S = N/A O = 3316 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_2.wcnf	S = OPT O = 2878 T = 2.07	S = OPT O = 2878 T = 25.34 (out)(err)	S = OPT O = 2878 T = 21.61 (out)(err)	S = OPT O = 2878 T = 21.43 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 45.52 (out)(err)	S = OPT O = 2878 T = 6.05 (out)(err)	S = OPT O = 2878 T = 2.07 (out)(err)	S = N/A O = 3273 T = TO (out)(err)	S = N/A O = 3345 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_3.wcnf	S = OPT O = 3045 T = 5.69	S = OPT O = 3045 T = 76.96 (out)(err)	S = OPT O = 3045 T = 31.58 (out)(err)	S = OPT O = 3045 T = 32.98 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 17.24 (out)(err)	S = OPT O = 3045 T = 10.96 (out)(err)	S = OPT O = 3045 T = 5.69 (out)(err)	S = N/A O = 3411 T = TO (out)(err)	S = N/A O = 3496 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_4.wcnf	S = OPT O = 3021 T = 1.69	S = OPT O = 3021 T = 6.94 (out)(err)	S = OPT O = 3021 T = 6.39 (out)(err)	S = OPT O = 3021 T = 6.57 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 89.95 (out)(err)	S = OPT O = 3021 T = 1.72 (out)(err)	S = OPT O = 3021 T = 1.69 (out)(err)	S = N/A O = 3416 T = TO (out)(err)	S = N/A O = 3355 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_5.wcnf	S = OPT O = 2812 T = 6.99	S = OPT O = 2812 T = 217.17 (out)(err)	S = OPT O = 2812 T = 56.02 (out)(err)	S = OPT O = 2812 T = 56.98 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 684.38 (out)(err)	S = OPT O = 2812 T = 14.26 (out)(err)	S = OPT O = 2812 T = 6.99 (out)(err)	S = N/A O = 3311 T = TO (out)(err)	S = N/A O = 3323 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_6.wcnf	S = OPT O = 2838 T = 6.54	S = OPT O = 2838 T = 78.00 (out)(err)	S = OPT O = 2838 T = 37.93 (out)(err)	S = OPT O = 2838 T = 38.88 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 3.87 (out)(err)	S = OPT O = 2838 T = 12.29 (out)(err)	S = OPT O = 2838 T = 6.54 (out)(err)	S = N/A O = 3371 T = TO (out)(err)	S = N/A O = 3311 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_7.wcnf	S = OPT O = 2815 T = 2.12	S = OPT O = 2815 T = 20.23 (out)(err)	S = OPT O = 2815 T = 14.77 (out)(err)	S = OPT O = 2815 T = 14.59 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 9.61 (out)(err)	S = OPT O = 2815 T = 4.00 (out)(err)	S = OPT O = 2815 T = 2.12 (out)(err)	S = N/A O = 3361 T = TO (out)(err)	S = N/A O = 3435 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_8.wcnf	S = OPT O = 3025 T = 5.67	S = OPT O = 3025 T = 95.38 (out)(err)	S = OPT O = 3025 T = 38.99 (out)(err)	S = OPT O = 3025 T = 39.43 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 6.32 (out)(err)	S = OPT O = 3025 T = 10.76 (out)(err)	S = OPT O = 3025 T = 5.67 (out)(err)	S = N/A O = 3344 T = TO (out)(err)	S = N/A O = 3512 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_9.wcnf	S = OPT O = 2952 T = 2.47	S = OPT O = 2952 T = 31.91 (out)(err)	S = OPT O = 2952 T = 17.33 (out)(err)	S = OPT O = 2952 T = 16.20 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 56.44 (out)(err)	S = OPT O = 2952 T = 4.58 (out)(err)	S = OPT O = 2952 T = 2.47 (out)(err)	S = N/A O = 3319 T = TO (out)(err)	S = N/A O = 3431 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_0.wcnf	S = OPT O = 3634 T = 7.59	S = OPT O = 3634 T = 266.66 (out)(err)	S = OPT O = 3634 T = 61.94 (out)(err)	S = OPT O = 3634 T = 61.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 = 3634 T = 22.83 (out)(err)	S = OPT O = 3634 T = 7.59 (out)(err)	S = N/A O = 4097 T = TO (out)(err)	S = N/A O = 4164 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_1.wcnf	S = OPT O = 3662 T = 2.89	S = OPT O = 3662 T = 15.33 (out)(err)	S = OPT O = 3662 T = 13.15 (out)(err)	S = OPT O = 3662 T = 13.92 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 199.66 (out)(err)	S = OPT O = 3662 T = 3.88 (out)(err)	S = OPT O = 3662 T = 2.89 (out)(err)	S = N/A O = 4257 T = TO (out)(err)	S = N/A O = 4219 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_2.wcnf	S = OPT O = 3827 T = 3.26	S = OPT O = 3827 T = 52.48 (out)(err)	S = OPT O = 3827 T = 29.71 (out)(err)	S = OPT O = 3827 T = 29.12 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 72.68 (out)(err)	S = OPT O = 3827 T = 7.46 (out)(err)	S = OPT O = 3827 T = 3.26 (out)(err)	S = N/A O = 4186 T = TO (out)(err)	S = N/A O = 4259 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_3.wcnf	S = OPT O = 3512 T = 1.87	S = OPT O = 3512 T = 47.62 (out)(err)	S = OPT O = 3512 T = 22.60 (out)(err)	S = OPT O = 3512 T = 22.79 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 53.99 (out)(err)	S = OPT O = 3512 T = 5.92 (out)(err)	S = OPT O = 3512 T = 1.87 (out)(err)	S = N/A O = 3986 T = TO (out)(err)	S = N/A O = 3984 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_4.wcnf	S = OPT O = 3355 T = 5.47	S = OPT O = 3355 T = 77.30 (out)(err)	S = OPT O = 3355 T = 25.46 (out)(err)	S = OPT O = 3355 T = 25.21 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 98.13 (out)(err)	S = OPT O = 3355 T = 6.45 (out)(err)	S = OPT O = 3355 T = 5.47 (out)(err)	S = N/A O = 3933 T = TO (out)(err)	S = N/A O = 3999 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_5.wcnf	S = OPT O = 3450 T = 7.00	S = OPT O = 3450 T = 243.53 (out)(err)	S = OPT O = 3450 T = 74.47 (out)(err)	S = OPT O = 3450 T = 76.73 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 7.67 (out)(err)	S = OPT O = 3450 T = 13.49 (out)(err)	S = OPT O = 3450 T = 7.00 (out)(err)	S = N/A O = 3959 T = TO (out)(err)	S = N/A O = 3941 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_6.wcnf	S = OPT O = 3654 T = 0.84	S = OPT O = 3654 T = 4.50 (out)(err)	S = OPT O = 3654 T = 5.04 (out)(err)	S = OPT O = 3654 T = 5.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 = 3654 T = 1.45 (out)(err)	S = OPT O = 3654 T = 0.84 (out)(err)	S = N/A O = 4132 T = TO (out)(err)	S = N/A O = 4070 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_7.wcnf	S = OPT O = 3617 T = 2.67	S = OPT O = 3617 T = 14.26 (out)(err)	S = OPT O = 3617 T = 9.52 (out)(err)	S = OPT O = 3617 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 = 3617 T = 4.03 (out)(err)	S = OPT O = 3617 T = 2.67 (out)(err)	S = N/A O = 3884 T = TO (out)(err)	S = N/A O = 3994 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_8.wcnf	S = OPT O = 3525 T = 1.69	S = OPT O = 3525 T = 18.84 (out)(err)	S = OPT O = 3525 T = 14.59 (out)(err)	S = OPT O = 3525 T = 13.55 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1.63 (out)(err)	S = OPT O = 3525 T = 3.48 (out)(err)	S = OPT O = 3525 T = 1.69 (out)(err)	S = N/A O = 4052 T = TO (out)(err)	S = N/A O = 4150 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_9.wcnf	S = OPT O = 3240 T = 2.48	S = OPT O = 3240 T = 63.28 (out)(err)	S = OPT O = 3240 T = 31.73 (out)(err)	S = OPT O = 3240 T = 33.48 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 29.26 (out)(err)	S = OPT O = 3240 T = 8.06 (out)(err)	S = OPT O = 3240 T = 2.48 (out)(err)	S = N/A O = 3888 T = TO (out)(err)	S = N/A O = 4073 T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_0.wcnf	S = OPT O = 28 T = 3.11	S = OPT O = 28 T = 4.76 (out)(err)	S = OPT O = 28 T = 8.11 (out)(err)	S = OPT O = 28 T = 8.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 = 28 T = 9.61 (out)(err)	S = OPT O = 28 T = 3.11 (out)(err)	S = N/A O = 28 T = TO (out)(err)	S = N/A O = 31 T = TO (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 = 1.02	S = OPT O = 15 T = 6.65 (out)(err)	S = OPT O = 15 T = 11.31 (out)(err)	S = OPT O = 15 T = 11.16 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 15 T = 288.75 (out)(err)	S = OPT O = 15 T = 6.47 (out)(err)	S = OPT O = 15 T = 1.02 (out)(err)	S = OPT O = 15 T = 29.86 (out)(err)	S = OPT O = 15 T = 43.31 (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_2.wcnf	S = OPT O = 25 T = 2.18	S = OPT O = 25 T = 5.83 (out)(err)	S = OPT O = 25 T = 9.62 (out)(err)	S = OPT O = 25 T = 9.56 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 25 T = 6.78 (out)(err)	S = OPT O = 25 T = 2.18 (out)(err)	S = N/A O = 25 T = TO (out)(err)	S = N/A O = 25 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_3.wcnf	S = OPT O = 25 T = 2.22	S = OPT O = 25 T = 9.35 (out)(err)	S = OPT O = 25 T = 15.32 (out)(err)	S = OPT O = 25 T = 15.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 = 25 T = 8.18 (out)(err)	S = OPT O = 25 T = 2.22 (out)(err)	S = N/A O = 25 T = TO (out)(err)	S = N/A O = 25 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_4.wcnf	S = OPT O = 30 T = 3.23	S = OPT O = 30 T = 3.23 (out)(err)	S = OPT O = 30 T = 5.70 (out)(err)	S = OPT O = 30 T = 5.61 (out)(err)	S = N/A O = N/A T = 437.31 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 30 T = 5.68 (out)(err)	S = OPT O = 30 T = 3.61 (out)(err)	S = N/A O = 30 T = TO (out)(err)	S = N/A O = 30 T = TO (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 = 1.99	S = OPT O = 27 T = 2.14 (out)(err)	S = OPT O = 27 T = 3.78 (out)(err)	S = OPT O = 27 T = 3.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 = 27 T = 5.26 (out)(err)	S = OPT O = 27 T = 1.99 (out)(err)	S = OPT O = 27 T = 985.17 (out)(err)	S = N/A O = 27 T = TO (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 = 2.73	S = OPT O = 26 T = 6.71 (out)(err)	S = OPT O = 26 T = 10.98 (out)(err)	S = OPT O = 26 T = 10.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 = 26 T = 10.14 (out)(err)	S = OPT O = 26 T = 2.73 (out)(err)	S = OPT O = 26 T = 1064.14 (out)(err)	S = N/A O = 26 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_7.wcnf	S = OPT O = 29 T = 8.83	S = OPT O = 29 T = 17.32 (out)(err)	S = OPT O = 29 T = 29.64 (out)(err)	S = OPT O = 29 T = 29.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 = 29 T = 11.94 (out)(err)	S = OPT O = 29 T = 8.83 (out)(err)	S = N/A O = 29 T = TO (out)(err)	S = N/A O = 31 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_8.wcnf	S = OPT O = 19 T = 2.58	S = OPT O = 19 T = 11.33 (out)(err)	S = OPT O = 19 T = 19.24 (out)(err)	S = OPT O = 19 T = 19.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 = 19 T = 9.73 (out)(err)	S = OPT O = 19 T = 2.58 (out)(err)	S = OPT O = 19 T = 593.03 (out)(err)	S = N/A O = 19 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_9.wcnf	S = OPT O = 30 T = 4.79	S = OPT O = 30 T = 6.68 (out)(err)	S = OPT O = 30 T = 11.29 (out)(err)	S = OPT O = 30 T = 11.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 = 30 T = 7.24 (out)(err)	S = OPT O = 30 T = 4.79 (out)(err)	S = N/A O = 30 T = TO (out)(err)	S = N/A O = 33 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_0.wcnf	S = OPT O = 54 T = 11.24	S = OPT O = 54 T = 62.98 (out)(err)	S = OPT O = 54 T = 88.02 (out)(err)	S = OPT O = 54 T = 87.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 = 54 T = 38.78 (out)(err)	S = OPT O = 54 T = 11.24 (out)(err)	S = N/A O = 96 T = TO (out)(err)	S = N/A O = 77 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_1.wcnf	S = OPT O = 58 T = 38.82	S = OPT O = 58 T = 58.70 (out)(err)	S = OPT O = 58 T = 83.56 (out)(err)	S = OPT O = 58 T = 83.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 = 58 T = 135.43 (out)(err)	S = OPT O = 58 T = 38.82 (out)(err)	S = N/A O = 60 T = TO (out)(err)	S = N/A O = 60 T = TO (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 = 25.63	S = OPT O = 59 T = 71.11 (out)(err)	S = OPT O = 59 T = 97.55 (out)(err)	S = OPT O = 59 T = 96.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 = 59 T = 59.47 (out)(err)	S = OPT O = 59 T = 25.63 (out)(err)	S = N/A O = 73 T = TO (out)(err)	S = N/A O = 73 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_3.wcnf	S = OPT O = 48 T = 21.73	S = OPT O = 48 T = 35.15 (out)(err)	S = OPT O = 48 T = 49.95 (out)(err)	S = OPT O = 48 T = 49.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 = 48 T = 52.30 (out)(err)	S = OPT O = 48 T = 21.73 (out)(err)	S = N/A O = 48 T = TO (out)(err)	S = N/A O = 66 T = TO (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 = 7.39	S = OPT O = 42 T = 8.80 (out)(err)	S = OPT O = 42 T = 13.12 (out)(err)	S = OPT O = 42 T = 13.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 = 42 T = 24.04 (out)(err)	S = OPT O = 42 T = 7.39 (out)(err)	S = N/A O = 45 T = TO (out)(err)	S = N/A O = 45 T = TO (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 = 9.65	S = OPT O = 46 T = 51.95 (out)(err)	S = OPT O = 46 T = 74.53 (out)(err)	S = OPT O = 46 T = 73.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 = 46 T = 42.45 (out)(err)	S = OPT O = 46 T = 9.65 (out)(err)	S = N/A O = 63 T = TO (out)(err)	S = N/A O = 64 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_6.wcnf	S = OPT O = 51 T = 31.76	S = OPT O = 51 T = 69.31 (out)(err)	S = OPT O = 51 T = 99.36 (out)(err)	S = OPT O = 51 T = 99.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 = 51 T = 56.75 (out)(err)	S = OPT O = 51 T = 31.76 (out)(err)	S = N/A O = 58 T = TO (out)(err)	S = N/A O = 59 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_7.wcnf	S = OPT O = 63 T = 51.12	S = OPT O = 63 T = 78.41 (out)(err)	S = OPT O = 63 T = 109.03 (out)(err)	S = OPT O = 63 T = 108.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 = 63 T = 61.52 (out)(err)	S = OPT O = 63 T = 51.12 (out)(err)	S = N/A O = 84 T = TO (out)(err)	S = N/A O = 87 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_8.wcnf	S = OPT O = 64 T = 97.22	S = OPT O = 64 T = 141.76 (out)(err)	S = OPT O = 64 T = 196.22 (out)(err)	S = OPT O = 64 T = 197.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 = 64 T = 132.22 (out)(err)	S = OPT O = 64 T = 97.22 (out)(err)	S = N/A O = 76 T = TO (out)(err)	S = N/A O = 114 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_9.wcnf	S = OPT O = 45 T = 8.86	S = OPT O = 45 T = 22.73 (out)(err)	S = OPT O = 45 T = 35.88 (out)(err)	S = OPT O = 45 T = 35.63 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 45 T = 25.57 (out)(err)	S = OPT O = 45 T = 8.86 (out)(err)	S = N/A O = 65 T = TO (out)(err)	S = N/A O = 66 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_0.wcnf	S = OPT O = 95 T = 127.32	S = OPT O = 95 T = 309.51 (out)(err)	S = OPT O = 95 T = 358.90 (out)(err)	S = OPT O = 95 T = 357.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 = 95 T = 211.85 (out)(err)	S = OPT O = 95 T = 127.32 (out)(err)	S = N/A O = 128 T = TO (out)(err)	S = N/A O = 114 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_1.wcnf	S = OPT O = 81 T = 87.45	S = OPT O = 81 T = 178.95 (out)(err)	S = OPT O = 81 T = 217.75 (out)(err)	S = OPT O = 81 T = 216.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 = 136.05 (out)(err)	S = OPT O = 81 T = 87.45 (out)(err)	S = N/A O = 87 T = TO (out)(err)	S = N/A O = 106 T = TO (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 = 91.93	S = OPT O = 77 T = 214.19 (out)(err)	S = OPT O = 77 T = 274.34 (out)(err)	S = OPT O = 77 T = 273.26 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 77 T = 172.18 (out)(err)	S = OPT O = 77 T = 91.93 (out)(err)	S = N/A O = 109 T = TO (out)(err)	S = N/A O = 97 T = TO (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 = 32.06	S = OPT O = 81 T = 100.94 (out)(err)	S = OPT O = 81 T = 136.28 (out)(err)	S = OPT O = 81 T = 135.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 = 81 T = 69.27 (out)(err)	S = OPT O = 81 T = 32.06 (out)(err)	S = N/A O = 105 T = TO (out)(err)	S = N/A O = 100 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_4.wcnf	S = OPT O = 75 T = 90.96	S = OPT O = 75 T = 154.48 (out)(err)	S = OPT O = 75 T = 197.51 (out)(err)	S = OPT O = 75 T = 196.96 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 75 T = 169.47 (out)(err)	S = OPT O = 75 T = 90.96 (out)(err)	S = N/A O = 90 T = TO (out)(err)	S = N/A O = 87 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_5.wcnf	S = OPT O = 80 T = 50.31	S = OPT O = 80 T = 79.14 (out)(err)	S = OPT O = 80 T = 97.65 (out)(err)	S = OPT O = 80 T = 97.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 = 80 T = 59.98 (out)(err)	S = OPT O = 80 T = 50.31 (out)(err)	S = N/A O = 82 T = TO (out)(err)	S = N/A O = 172 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_6.wcnf	S = OPT O = 74 T = 49.37	S = OPT O = 74 T = 92.39 (out)(err)	S = OPT O = 74 T = 118.31 (out)(err)	S = OPT O = 74 T = 117.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 = 74 T = 81.42 (out)(err)	S = OPT O = 74 T = 49.37 (out)(err)	S = N/A O = 106 T = TO (out)(err)	S = N/A O = 114 T = TO (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 = 93.12	S = OPT O = 99 T = 317.24 (out)(err)	S = OPT O = 99 T = 354.37 (out)(err)	S = OPT O = 99 T = 354.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 = 99 T = 192.74 (out)(err)	S = OPT O = 99 T = 93.12 (out)(err)	S = N/A O = 150 T = TO (out)(err)	S = N/A O = 119 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_8.wcnf	S = OPT O = 90 T = 224.01	S = OPT O = 90 T = 521.17 (out)(err)	S = OPT O = 90 T = 589.21 (out)(err)	S = OPT O = 90 T = 588.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 = 90 T = 395.71 (out)(err)	S = OPT O = 90 T = 224.01 (out)(err)	S = N/A O = 110 T = TO (out)(err)	S = N/A O = 111 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_9.wcnf	S = OPT O = 95 T = 174.59	S = OPT O = 95 T = 259.06 (out)(err)	S = OPT O = 95 T = 335.73 (out)(err)	S = OPT O = 95 T = 338.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 = 95 T = 226.10 (out)(err)	S = OPT O = 95 T = 174.59 (out)(err)	S = N/A O = 124 T = TO (out)(err)	S = N/A O = 121 T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)