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	Sat4j	ShinMaxSat	WMaxSatz+	WMaxSatz09	WPM1	akmaxsat	akmaxsat_ls	iut_rr_ls	iut_rr_rv	pwbo2.1	wbo1.6
file_rwpms_wcnf_L2_V150_C4000_H150_0.wcnf	S = OPT O = 4231 T = 0.62	S = N/A O = 4619 T = TO (out)(err)	S = N/A O = 5351 T = TO (out)(err)	S = OPT O = 4231 T = 1.83 (out)(err)	S = OPT O = 4231 T = 1.98 (out)(err)	S = N/A O = N/A T = 252.37 (out)(err)	S = OPT O = 4231 T = 0.62 (out)(err)	S = OPT O = 4231 T = 1.03 (out)(err)	S = OPT O = 4231 T = 7.75 (out)(err)	S = OPT O = 4231 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)
file_rwpms_wcnf_L2_V150_C4000_H150_1.wcnf	S = UNSAT O = N/A T = 0.01	S = UNSAT O = N/A T = 0.89 (out)(err)	S = UNSAT O = N/A T = 0.16 (out)(err)	S = UNSAT O = N/A T = 0.07 (out)(err)	S = UNSAT O = N/A T = 0.07 (out)(err)	S = UNSAT O = N/A T = 0.01 (out)(err)	S = UNSAT O = N/A T = 0.07 (out)(err)	S = UNSAT O = N/A T = 0.78 (out)(err)	S = UNSAT O = N/A T = 0.79 (out)(err)	S = UNSAT O = N/A T = 0.78 (out)(err)	S = UNSAT O = N/A T = 0.02 (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.52	S = N/A O = 4857 T = TO (out)(err)	S = N/A O = 5083 T = TO (out)(err)	S = OPT O = 4235 T = 7.59 (out)(err)	S = OPT O = 4235 T = 6.46 (out)(err)	S = N/A O = N/A T = 327.92 (out)(err)	S = OPT O = 4235 T = 1.52 (out)(err)	S = OPT O = 4235 T = 1.71 (out)(err)	S = OPT O = 4235 T = 15.32 (out)(err)	S = OPT O = 4235 T = 11.65 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_3.wcnf	S = OPT O = 4037 T = 2.81	S = N/A O = 4841 T = TO (out)(err)	S = N/A O = 5155 T = TO (out)(err)	S = OPT O = 4037 T = 13.51 (out)(err)	S = OPT O = 4037 T = 13.56 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4037 T = 3.50 (out)(err)	S = OPT O = 4037 T = 2.81 (out)(err)	S = OPT O = 4037 T = 16.01 (out)(err)	S = OPT O = 4037 T = 15.79 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_4.wcnf	S = OPT O = 4031 T = 3.09	S = N/A O = 4873 T = TO (out)(err)	S = N/A O = 5691 T = TO (out)(err)	S = OPT O = 4031 T = 32.90 (out)(err)	S = OPT O = 4031 T = 32.63 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4031 T = 10.67 (out)(err)	S = OPT O = 4031 T = 3.09 (out)(err)	S = OPT O = 4031 T = 27.33 (out)(err)	S = OPT O = 4031 T = 27.50 (out)(err)	S = N/A O = N/A 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.09	S = N/A O = 4930 T = TO (out)(err)	S = N/A O = 5016 T = TO (out)(err)	S = OPT O = 4144 T = 77.90 (out)(err)	S = OPT O = 4144 T = 78.71 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4144 T = 18.79 (out)(err)	S = OPT O = 4144 T = 7.09 (out)(err)	S = OPT O = 4144 T = 67.94 (out)(err)	S = OPT O = 4144 T = 66.13 (out)(err)	S = N/A O = N/A 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 = 11.46	S = N/A O = 4934 T = TO (out)(err)	S = N/A O = 5253 T = TO (out)(err)	S = OPT O = 4149 T = 80.25 (out)(err)	S = OPT O = 4149 T = 79.90 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4149 T = 20.48 (out)(err)	S = OPT O = 4149 T = 11.46 (out)(err)	S = OPT O = 4149 T = 96.56 (out)(err)	S = OPT O = 4149 T = 92.11 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_7.wcnf	S = OPT O = 4043 T = 4.30	S = N/A O = 4789 T = TO (out)(err)	S = N/A O = 5262 T = TO (out)(err)	S = OPT O = 4043 T = 105.23 (out)(err)	S = OPT O = 4043 T = 108.50 (out)(err)	S = N/A O = N/A T = 306.70 (out)(err)	S = OPT O = 4043 T = 19.56 (out)(err)	S = OPT O = 4043 T = 4.30 (out)(err)	S = OPT O = 4043 T = 24.07 (out)(err)	S = OPT O = 4043 T = 23.55 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C4000_H150_8.wcnf	S = OPT O = 4078 T = 9.84	S = N/A O = 4896 T = TO (out)(err)	S = N/A O = 4955 T = TO (out)(err)	S = OPT O = 4078 T = 170.18 (out)(err)	S = OPT O = 4078 T = 171.42 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4078 T = 30.15 (out)(err)	S = OPT O = 4078 T = 9.84 (out)(err)	S = OPT O = 4078 T = 54.78 (out)(err)	S = OPT O = 4078 T = 53.71 (out)(err)	S = N/A O = N/A 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.54	S = N/A O = 4996 T = TO (out)(err)	S = N/A O = 5421 T = TO (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 = OPT O = 4328 T = 6.75 (out)(err)	S = OPT O = 4328 T = 3.54 (out)(err)	S = OPT O = 4328 T = 38.92 (out)(err)	S = OPT O = 4328 T = 37.28 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_0.wcnf	S = OPT O = 4572 T = 9.12	S = N/A O = 5485 T = TO (out)(err)	S = N/A O = 6141 T = TO (out)(err)	S = OPT O = 4572 T = 139.82 (out)(err)	S = OPT O = 4572 T = 134.63 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4572 T = 25.79 (out)(err)	S = OPT O = 4572 T = 9.12 (out)(err)	S = OPT O = 4572 T = 66.58 (out)(err)	S = OPT O = 4572 T = 64.18 (out)(err)	S = N/A O = N/A 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 = 9.70	S = N/A O = 5669 T = TO (out)(err)	S = N/A O = 6536 T = TO (out)(err)	S = OPT O = 4967 T = 149.04 (out)(err)	S = OPT O = 4967 T = 150.45 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4967 T = 26.49 (out)(err)	S = OPT O = 4967 T = 9.70 (out)(err)	S = OPT O = 4967 T = 156.77 (out)(err)	S = OPT O = 4967 T = 151.69 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_2.wcnf	S = OPT O = 4961 T = 4.62	S = N/A O = 5845 T = TO (out)(err)	S = N/A O = 6395 T = TO (out)(err)	S = OPT O = 4961 T = 29.70 (out)(err)	S = OPT O = 4961 T = 29.20 (out)(err)	S = N/A O = N/A T = 204.93 (out)(err)	S = OPT O = 4961 T = 7.07 (out)(err)	S = OPT O = 4961 T = 4.62 (out)(err)	S = OPT O = 4961 T = 68.00 (out)(err)	S = OPT O = 4961 T = 67.52 (out)(err)	S = N/A O = N/A 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.85	S = N/A O = 5579 T = TO (out)(err)	S = N/A O = 5749 T = TO (out)(err)	S = OPT O = 4614 T = 16.69 (out)(err)	S = OPT O = 4614 T = 16.61 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4614 T = 2.85 (out)(err)	S = OPT O = 4614 T = 2.88 (out)(err)	S = OPT O = 4614 T = 28.22 (out)(err)	S = OPT O = 4614 T = 27.25 (out)(err)	S = N/A O = N/A 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 = 17.94	S = N/A O = 5473 T = TO (out)(err)	S = N/A O = 6162 T = TO (out)(err)	S = OPT O = 4794 T = 163.94 (out)(err)	S = OPT O = 4794 T = 165.19 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4794 T = 37.63 (out)(err)	S = OPT O = 4794 T = 17.94 (out)(err)	S = OPT O = 4794 T = 223.14 (out)(err)	S = OPT O = 4794 T = 217.51 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_5.wcnf	S = OPT O = 4687 T = 6.71	S = N/A O = 5640 T = TO (out)(err)	S = N/A O = 6127 T = TO (out)(err)	S = OPT O = 4687 T = 42.06 (out)(err)	S = OPT O = 4687 T = 42.42 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4687 T = 11.93 (out)(err)	S = OPT O = 4687 T = 6.71 (out)(err)	S = OPT O = 4687 T = 46.53 (out)(err)	S = OPT O = 4687 T = 46.45 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_6.wcnf	S = OPT O = 4605 T = 2.46	S = N/A O = 5589 T = TO (out)(err)	S = N/A O = 5927 T = TO (out)(err)	S = OPT O = 4605 T = 68.13 (out)(err)	S = OPT O = 4605 T = 68.49 (out)(err)	S = N/A O = N/A T = 213.67 (out)(err)	S = OPT O = 4605 T = 12.89 (out)(err)	S = OPT O = 4605 T = 2.46 (out)(err)	S = OPT O = 4605 T = 17.13 (out)(err)	S = OPT O = 4605 T = 16.36 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_7.wcnf	S = OPT O = 4710 T = 7.89	S = N/A O = 5624 T = TO (out)(err)	S = N/A O = 5978 T = TO (out)(err)	S = OPT O = 4710 T = 56.75 (out)(err)	S = OPT O = 4710 T = 56.12 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4710 T = 13.72 (out)(err)	S = OPT O = 4710 T = 7.89 (out)(err)	S = OPT O = 4710 T = 98.46 (out)(err)	S = OPT O = 4710 T = 93.64 (out)(err)	S = N/A O = N/A 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.31	S = N/A O = 5552 T = TO (out)(err)	S = N/A O = 5880 T = TO (out)(err)	S = OPT O = 4945 T = 32.52 (out)(err)	S = OPT O = 4945 T = 33.72 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 4945 T = 9.86 (out)(err)	S = OPT O = 4945 T = 3.31 (out)(err)	S = OPT O = 4945 T = 53.30 (out)(err)	S = OPT O = 4945 T = 51.14 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C4500_H150_9.wcnf	S = OPT O = 5023 T = 5.70	S = N/A O = 5563 T = TO (out)(err)	S = N/A O = 5766 T = TO (out)(err)	S = OPT O = 5023 T = 51.76 (out)(err)	S = OPT O = 5023 T = 51.78 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 5023 T = 12.77 (out)(err)	S = OPT O = 5023 T = 5.70 (out)(err)	S = OPT O = 5023 T = 97.18 (out)(err)	S = OPT O = 5023 T = 91.93 (out)(err)	S = N/A O = N/A 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.12	S = N/A O = 6138 T = TO (out)(err)	S = N/A O = 6648 T = TO (out)(err)	S = OPT O = 5362 T = 33.56 (out)(err)	S = OPT O = 5362 T = 33.23 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 5362 T = 8.22 (out)(err)	S = OPT O = 5362 T = 2.12 (out)(err)	S = OPT O = 5362 T = 12.59 (out)(err)	S = OPT O = 5362 T = 12.46 (out)(err)	S = N/A O = N/A 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.10	S = N/A O = 6540 T = TO (out)(err)	S = N/A O = 7006 T = TO (out)(err)	S = OPT O = 5338 T = 64.93 (out)(err)	S = OPT O = 5338 T = 69.27 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 5338 T = 15.57 (out)(err)	S = OPT O = 5338 T = 2.10 (out)(err)	S = OPT O = 5338 T = 17.11 (out)(err)	S = OPT O = 5338 T = 16.98 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C5000_H150_2.wcnf	S = OPT O = 5312 T = 4.56	S = N/A O = 6217 T = TO (out)(err)	S = N/A O = 6617 T = TO (out)(err)	S = OPT O = 5312 T = 144.32 (out)(err)	S = OPT O = 5312 T = 143.61 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 5312 T = 23.80 (out)(err)	S = OPT O = 5312 T = 4.56 (out)(err)	S = OPT O = 5312 T = 34.83 (out)(err)	S = OPT O = 5312 T = 33.84 (out)(err)	S = N/A O = N/A 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.37	S = N/A O = 6537 T = TO (out)(err)	S = N/A O = 6811 T = TO (out)(err)	S = OPT O = 5507 T = 29.22 (out)(err)	S = OPT O = 5507 T = 29.80 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 5507 T = 8.17 (out)(err)	S = OPT O = 5507 T = 5.37 (out)(err)	S = OPT O = 5507 T = 40.38 (out)(err)	S = OPT O = 5507 T = 39.66 (out)(err)	S = N/A O = N/A 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 = 21.92	S = N/A O = 6448 T = TO (out)(err)	S = N/A O = 6609 T = TO (out)(err)	S = OPT O = 5451 T = 344.80 (out)(err)	S = OPT O = 5451 T = 343.88 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 5451 T = 87.08 (out)(err)	S = OPT O = 5451 T = 21.92 (out)(err)	S = OPT O = 5451 T = 163.20 (out)(err)	S = OPT O = 5451 T = 158.33 (out)(err)	S = N/A O = N/A 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 = 3.89	S = N/A O = 6133 T = TO (out)(err)	S = N/A O = 6856 T = TO (out)(err)	S = OPT O = 5308 T = 50.91 (out)(err)	S = OPT O = 5308 T = 52.64 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 5308 T = 7.79 (out)(err)	S = OPT O = 5308 T = 3.89 (out)(err)	S = OPT O = 5308 T = 34.76 (out)(err)	S = OPT O = 5308 T = 34.35 (out)(err)	S = N/A O = N/A 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.36	S = N/A O = 6142 T = TO (out)(err)	S = N/A O = 6240 T = TO (out)(err)	S = OPT O = 5428 T = 59.77 (out)(err)	S = OPT O = 5428 T = 58.20 (out)(err)	S = N/A O = N/A T = 200.04 (out)(err)	S = OPT O = 5428 T = 11.42 (out)(err)	S = OPT O = 5428 T = 5.36 (out)(err)	S = OPT O = 5428 T = 54.08 (out)(err)	S = OPT O = 5428 T = 51.64 (out)(err)	S = N/A O = N/A 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.74	S = N/A O = 6142 T = TO (out)(err)	S = N/A O = 6856 T = TO (out)(err)	S = OPT O = 5468 T = 214.71 (out)(err)	S = OPT O = 5468 T = 207.00 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 5468 T = 28.56 (out)(err)	S = OPT O = 5468 T = 11.74 (out)(err)	S = OPT O = 5468 T = 167.37 (out)(err)	S = OPT O = 5468 T = 163.99 (out)(err)	S = N/A O = N/A 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.09	S = N/A O = 6056 T = TO (out)(err)	S = N/A O = 6370 T = TO (out)(err)	S = OPT O = 5339 T = 13.04 (out)(err)	S = OPT O = 5339 T = 12.88 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 5339 T = 5.83 (out)(err)	S = OPT O = 5339 T = 2.09 (out)(err)	S = OPT O = 5339 T = 20.62 (out)(err)	S = OPT O = 5339 T = 20.81 (out)(err)	S = N/A O = N/A 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.08	S = N/A O = 6420 T = TO (out)(err)	S = N/A O = 7017 T = TO (out)(err)	S = OPT O = 5376 T = 26.13 (out)(err)	S = OPT O = 5376 T = 26.84 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 5376 T = 11.40 (out)(err)	S = OPT O = 5376 T = 3.08 (out)(err)	S = OPT O = 5376 T = 36.87 (out)(err)	S = OPT O = 5376 T = 36.25 (out)(err)	S = N/A O = N/A 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.14	S = N/A O = 758 T = TO (out)(err)	S = N/A O = 957 T = TO (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 = OPT O = 626 T = 0.14 (out)(err)	S = OPT O = 626 T = 0.39 (out)(err)	S = OPT O = 626 T = 0.74 (out)(err)	S = OPT O = 626 T = 0.71 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_1.wcnf	S = OPT O = 745 T = 0.33	S = N/A O = 968 T = TO (out)(err)	S = N/A O = 1087 T = TO (out)(err)	S = OPT O = 745 T = 0.34 (out)(err)	S = OPT O = 745 T = 0.34 (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 = OPT O = 745 T = 1.47 (out)(err)	S = OPT O = 745 T = 1.42 (out)(err)	S = N/A O = N/A 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.08	S = N/A O = 746 T = TO (out)(err)	S = N/A O = 970 T = TO (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 = OPT O = 629 T = 0.08 (out)(err)	S = OPT O = 629 T = 0.34 (out)(err)	S = OPT O = 629 T = 0.50 (out)(err)	S = OPT O = 629 T = 0.49 (out)(err)	S = N/A O = N/A 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.36	S = N/A O = 903 T = TO (out)(err)	S = N/A O = 963 T = TO (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 = OPT O = 723 T = 0.36 (out)(err)	S = OPT O = 723 T = 0.48 (out)(err)	S = OPT O = 723 T = 1.42 (out)(err)	S = OPT O = 723 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)
file_rwpms_wcnf_L2_V150_C1000_H150_4.wcnf	S = OPT O = 737 T = 0.11	S = N/A O = 907 T = TO (out)(err)	S = N/A O = 1001 T = TO (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 = OPT O = 737 T = 0.11 (out)(err)	S = OPT O = 737 T = 0.35 (out)(err)	S = OPT O = 737 T = 0.73 (out)(err)	S = OPT O = 737 T = 0.72 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_5.wcnf	S = OPT O = 668 T = 0.12	S = N/A O = 723 T = TO (out)(err)	S = N/A O = 834 T = TO (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 = OPT O = 668 T = 0.14 (out)(err)	S = OPT O = 668 T = 0.37 (out)(err)	S = OPT O = 668 T = 0.93 (out)(err)	S = OPT O = 668 T = 0.89 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_6.wcnf	S = OPT O = 641 T = 0.05	S = N/A O = 801 T = TO (out)(err)	S = N/A O = 1005 T = TO (out)(err)	S = OPT O = 641 T = 0.06 (out)(err)	S = OPT O = 641 T = 0.06 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 641 T = 0.05 (out)(err)	S = OPT O = 641 T = 0.34 (out)(err)	S = OPT O = 641 T = 0.61 (out)(err)	S = OPT O = 641 T = 0.58 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C1000_H150_7.wcnf	S = OPT O = 688 T = 0.21	S = N/A O = 807 T = TO (out)(err)	S = N/A O = 1111 T = TO (out)(err)	S = OPT O = 688 T = 0.26 (out)(err)	S = OPT O = 688 T = 0.24 (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 = OPT O = 688 T = 1.43 (out)(err)	S = OPT O = 688 T = 1.29 (out)(err)	S = N/A O = N/A 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.29	S = N/A O = 775 T = TO (out)(err)	S = N/A O = 963 T = TO (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 = OPT O = 577 T = 0.29 (out)(err)	S = OPT O = 577 T = 0.48 (out)(err)	S = OPT O = 577 T = 1.07 (out)(err)	S = OPT O = 577 T = 1.05 (out)(err)	S = N/A O = N/A 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.11	S = N/A O = 845 T = TO (out)(err)	S = N/A O = 1039 T = TO (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 = OPT O = 714 T = 0.13 (out)(err)	S = OPT O = 714 T = 0.36 (out)(err)	S = OPT O = 714 T = 0.76 (out)(err)	S = OPT O = 714 T = 0.73 (out)(err)	S = N/A O = N/A 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.44	S = N/A O = 1426 T = TO (out)(err)	S = N/A O = 1800 T = TO (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 = OPT O = 1121 T = 1.55 (out)(err)	S = OPT O = 1121 T = 1.44 (out)(err)	S = OPT O = 1121 T = 5.92 (out)(err)	S = OPT O = 1121 T = 5.84 (out)(err)	S = N/A O = N/A 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.57	S = N/A O = 1340 T = TO (out)(err)	S = N/A O = 1732 T = TO (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 = OPT O = 1142 T = 0.74 (out)(err)	S = OPT O = 1142 T = 0.57 (out)(err)	S = OPT O = 1142 T = 1.97 (out)(err)	S = OPT O = 1142 T = 1.90 (out)(err)	S = N/A O = N/A T = TO (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.86	S = N/A O = 1655 T = TO (out)(err)	S = N/A O = 1817 T = TO (out)(err)	S = OPT O = 1252 T = 1.77 (out)(err)	S = OPT O = 1252 T = 1.78 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 1252 T = 0.86 (out)(err)	S = OPT O = 1252 T = 0.89 (out)(err)	S = OPT O = 1252 T = 4.67 (out)(err)	S = OPT O = 1252 T = 4.31 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_3.wcnf	S = OPT O = 1295 T = 0.70	S = N/A O = 1500 T = TO (out)(err)	S = N/A O = 1812 T = TO (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 = OPT O = 1295 T = 0.72 (out)(err)	S = OPT O = 1295 T = 0.70 (out)(err)	S = OPT O = 1295 T = 5.60 (out)(err)	S = OPT O = 1295 T = 5.48 (out)(err)	S = N/A O = N/A 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.90	S = N/A O = 1677 T = TO (out)(err)	S = N/A O = 1820 T = TO (out)(err)	S = OPT O = 1261 T = 1.65 (out)(err)	S = OPT O = 1261 T = 1.66 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 1261 T = 0.90 (out)(err)	S = OPT O = 1261 T = 0.97 (out)(err)	S = OPT O = 1261 T = 5.02 (out)(err)	S = OPT O = 1261 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)
file_rwpms_wcnf_L2_V150_C1500_H150_5.wcnf	S = OPT O = 1047 T = 0.64	S = N/A O = 1292 T = TO (out)(err)	S = N/A O = 1350 T = TO (out)(err)	S = OPT O = 1047 T = 3.79 (out)(err)	S = OPT O = 1047 T = 3.80 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 1047 T = 2.08 (out)(err)	S = OPT O = 1047 T = 0.64 (out)(err)	S = OPT O = 1047 T = 1.64 (out)(err)	S = OPT O = 1047 T = 1.62 (out)(err)	S = N/A O = N/A 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 = N/A O = 1414 T = TO (out)(err)	S = N/A O = 1686 T = TO (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 = OPT O = 1175 T = 0.16 (out)(err)	S = OPT O = 1175 T = 0.49 (out)(err)	S = OPT O = 1175 T = 1.85 (out)(err)	S = OPT O = 1175 T = 1.87 (out)(err)	S = N/A O = N/A 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.77	S = N/A O = 1372 T = TO (out)(err)	S = N/A O = 1836 T = TO (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 = OPT O = 1145 T = 1.03 (out)(err)	S = OPT O = 1145 T = 0.77 (out)(err)	S = OPT O = 1145 T = 2.92 (out)(err)	S = OPT O = 1145 T = 2.93 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C1500_H150_8.wcnf	S = OPT O = 1135 T = 1.21	S = N/A O = 1432 T = TO (out)(err)	S = N/A O = 1755 T = TO (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 = OPT O = 1135 T = 1.45 (out)(err)	S = OPT O = 1135 T = 1.21 (out)(err)	S = OPT O = 1135 T = 4.14 (out)(err)	S = OPT O = 1135 T = 4.04 (out)(err)	S = N/A O = N/A 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.07	S = N/A O = 1462 T = TO (out)(err)	S = N/A O = 1554 T = TO (out)(err)	S = OPT O = 1232 T = 2.19 (out)(err)	S = OPT O = 1232 T = 2.11 (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.07 (out)(err)	S = OPT O = 1232 T = 5.88 (out)(err)	S = OPT O = 1232 T = 5.71 (out)(err)	S = N/A O = N/A 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.29	S = N/A O = 2283 T = TO (out)(err)	S = N/A O = 2432 T = 416.94 (out)(err)	S = OPT O = 1842 T = 7.20 (out)(err)	S = OPT O = 1842 T = 6.90 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 1842 T = 2.87 (out)(err)	S = OPT O = 1842 T = 1.29 (out)(err)	S = OPT O = 1842 T = 8.72 (out)(err)	S = OPT O = 1842 T = 8.77 (out)(err)	S = N/A O = N/A 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 = N/A O = 2239 T = TO (out)(err)	S = N/A O = 2669 T = 211.25 (out)(err)	S = OPT O = 1699 T = 1.48 (out)(err)	S = OPT O = 1699 T = 1.49 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 1699 T = 0.90 (out)(err)	S = OPT O = 1699 T = 1.11 (out)(err)	S = OPT O = 1699 T = 6.31 (out)(err)	S = OPT O = 1699 T = 6.26 (out)(err)	S = N/A O = N/A 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.25	S = N/A O = 2180 T = TO (out)(err)	S = N/A O = 2386 T = TO (out)(err)	S = OPT O = 1730 T = 4.90 (out)(err)	S = OPT O = 1730 T = 4.44 (out)(err)	S = N/A O = N/A T = 286.90 (out)(err)	S = OPT O = 1730 T = 1.38 (out)(err)	S = OPT O = 1730 T = 1.25 (out)(err)	S = OPT O = 1730 T = 5.28 (out)(err)	S = OPT O = 1730 T = 5.47 (out)(err)	S = N/A O = N/A 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.01	S = N/A O = 2221 T = TO (out)(err)	S = N/A O = 2791 T = 456.16 (out)(err)	S = OPT O = 1885 T = 4.51 (out)(err)	S = OPT O = 1885 T = 4.50 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 1885 T = 2.06 (out)(err)	S = OPT O = 1885 T = 1.01 (out)(err)	S = OPT O = 1885 T = 9.43 (out)(err)	S = OPT O = 1885 T = 9.06 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_4.wcnf	S = OPT O = 2043 T = 0.92	S = N/A O = 2417 T = TO (out)(err)	S = N/A O = 2530 T = TO (out)(err)	S = OPT O = 2043 T = 2.37 (out)(err)	S = OPT O = 2043 T = 2.33 (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.92 (out)(err)	S = OPT O = 2043 T = 12.82 (out)(err)	S = OPT O = 2043 T = 12.18 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_5.wcnf	S = OPT O = 1818 T = 1.06	S = N/A O = 2091 T = TO (out)(err)	S = N/A O = 2449 T = 453.06 (out)(err)	S = OPT O = 1818 T = 6.94 (out)(err)	S = OPT O = 1818 T = 7.00 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 1818 T = 5.54 (out)(err)	S = OPT O = 1818 T = 1.06 (out)(err)	S = OPT O = 1818 T = 7.75 (out)(err)	S = OPT O = 1818 T = 7.45 (out)(err)	S = N/A O = N/A 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 = N/A O = 2159 T = TO (out)(err)	S = N/A O = 2963 T = TO (out)(err)	S = OPT O = 1832 T = 1.17 (out)(err)	S = OPT O = 1832 T = 1.17 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 1832 T = 0.60 (out)(err)	S = OPT O = 1832 T = 0.62 (out)(err)	S = OPT O = 1832 T = 2.02 (out)(err)	S = OPT O = 1832 T = 2.01 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C2000_H150_7.wcnf	S = OPT O = 1780 T = 1.14	S = N/A O = 2184 T = TO (out)(err)	S = N/A O = 2591 T = TO (out)(err)	S = OPT O = 1780 T = 3.42 (out)(err)	S = OPT O = 1780 T = 3.45 (out)(err)	S = N/A O = N/A T = 255.97 (out)(err)	S = OPT O = 1780 T = 1.73 (out)(err)	S = OPT O = 1780 T = 1.14 (out)(err)	S = OPT O = 1780 T = 6.11 (out)(err)	S = OPT O = 1780 T = 6.04 (out)(err)	S = N/A O = N/A 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.84	S = N/A O = 2131 T = TO (out)(err)	S = N/A O = 2627 T = TO (out)(err)	S = OPT O = 1726 T = 2.94 (out)(err)	S = OPT O = 1726 T = 2.85 (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.84 (out)(err)	S = OPT O = 1726 T = 2.42 (out)(err)	S = OPT O = 1726 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)
file_rwpms_wcnf_L2_V150_C2000_H150_9.wcnf	S = OPT O = 1807 T = 3.34	S = N/A O = 2262 T = TO (out)(err)	S = N/A O = 2384 T = 465.90 (out)(err)	S = OPT O = 1807 T = 11.85 (out)(err)	S = OPT O = 1807 T = 12.24 (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.34 (out)(err)	S = OPT O = 1807 T = 17.88 (out)(err)	S = OPT O = 1807 T = 17.43 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_0.wcnf	S = OPT O = 2414 T = 0.93	S = N/A O = 2934 T = TO (out)(err)	S = N/A O = 3111 T = TO (out)(err)	S = OPT O = 2414 T = 2.83 (out)(err)	S = OPT O = 2414 T = 2.82 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2414 T = 1.72 (out)(err)	S = OPT O = 2414 T = 0.93 (out)(err)	S = OPT O = 2414 T = 5.56 (out)(err)	S = OPT O = 2414 T = 5.23 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_1.wcnf	S = OPT O = 2398 T = 1.51	S = N/A O = 2814 T = TO (out)(err)	S = N/A O = 2920 T = 242.71 (out)(err)	S = OPT O = 2398 T = 6.89 (out)(err)	S = OPT O = 2398 T = 6.99 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2398 T = 1.87 (out)(err)	S = OPT O = 2398 T = 1.51 (out)(err)	S = OPT O = 2398 T = 16.59 (out)(err)	S = OPT O = 2398 T = 16.81 (out)(err)	S = N/A O = N/A 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 = 0.99	S = N/A O = 2686 T = TO (out)(err)	S = N/A O = 2923 T = TO (out)(err)	S = OPT O = 2113 T = 12.70 (out)(err)	S = OPT O = 2113 T = 12.71 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2113 T = 3.58 (out)(err)	S = OPT O = 2113 T = 0.99 (out)(err)	S = OPT O = 2113 T = 5.20 (out)(err)	S = OPT O = 2113 T = 5.14 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_3.wcnf	S = OPT O = 2339 T = 2.22	S = N/A O = 2885 T = TO (out)(err)	S = N/A O = 3315 T = TO (out)(err)	S = OPT O = 2339 T = 9.87 (out)(err)	S = OPT O = 2339 T = 10.67 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2339 T = 3.12 (out)(err)	S = OPT O = 2339 T = 2.22 (out)(err)	S = OPT O = 2339 T = 16.36 (out)(err)	S = OPT O = 2339 T = 16.18 (out)(err)	S = N/A O = N/A 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.07	S = N/A O = 2933 T = TO (out)(err)	S = N/A O = 3424 T = 237.78 (out)(err)	S = OPT O = 2390 T = 2.80 (out)(err)	S = OPT O = 2390 T = 2.77 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2390 T = 1.07 (out)(err)	S = OPT O = 2390 T = 1.07 (out)(err)	S = OPT O = 2390 T = 8.31 (out)(err)	S = OPT O = 2390 T = 7.98 (out)(err)	S = N/A O = N/A 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 = N/A O = 3028 T = TO (out)(err)	S = N/A O = 2942 T = 228.02 (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 = OPT O = 2332 T = 0.86 (out)(err)	S = OPT O = 2332 T = 1.05 (out)(err)	S = OPT O = 2332 T = 7.04 (out)(err)	S = OPT O = 2332 T = 6.80 (out)(err)	S = N/A O = N/A 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 = 1.82	S = N/A O = 2978 T = TO (out)(err)	S = N/A O = 2876 T = TO (out)(err)	S = OPT O = 2488 T = 6.48 (out)(err)	S = OPT O = 2488 T = 6.61 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2488 T = 2.24 (out)(err)	S = OPT O = 2488 T = 1.82 (out)(err)	S = OPT O = 2488 T = 33.70 (out)(err)	S = OPT O = 2488 T = 32.24 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_7.wcnf	S = OPT O = 2241 T = 1.50	S = N/A O = 2658 T = TO (out)(err)	S = N/A O = 3219 T = 187.14 (out)(err)	S = OPT O = 2241 T = 13.75 (out)(err)	S = OPT O = 2241 T = 13.79 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2241 T = 6.01 (out)(err)	S = OPT O = 2241 T = 1.50 (out)(err)	S = OPT O = 2241 T = 8.10 (out)(err)	S = OPT O = 2241 T = 7.93 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_8.wcnf	S = OPT O = 2353 T = 2.09	S = N/A O = 2832 T = TO (out)(err)	S = N/A O = 3315 T = 224.80 (out)(err)	S = OPT O = 2353 T = 11.85 (out)(err)	S = OPT O = 2353 T = 11.80 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2353 T = 3.73 (out)(err)	S = OPT O = 2353 T = 2.09 (out)(err)	S = OPT O = 2353 T = 13.13 (out)(err)	S = OPT O = 2353 T = 12.66 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C2500_H150_9.wcnf	S = OPT O = 2560 T = 0.73	S = N/A O = 3031 T = TO (out)(err)	S = N/A O = 3268 T = 252.50 (out)(err)	S = OPT O = 2560 T = 2.66 (out)(err)	S = OPT O = 2560 T = 2.59 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2560 T = 0.73 (out)(err)	S = OPT O = 2560 T = 0.85 (out)(err)	S = OPT O = 2560 T = 4.46 (out)(err)	S = OPT O = 2560 T = 4.04 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_0.wcnf	S = OPT O = 2885 T = 7.54	S = N/A O = 3290 T = TO (out)(err)	S = N/A O = 3951 T = TO (out)(err)	S = OPT O = 2885 T = 45.10 (out)(err)	S = OPT O = 2885 T = 50.12 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2885 T = 11.62 (out)(err)	S = OPT O = 2885 T = 7.54 (out)(err)	S = OPT O = 2885 T = 74.25 (out)(err)	S = OPT O = 2885 T = 70.42 (out)(err)	S = N/A O = N/A T = TO (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 = 4.66	S = N/A O = 3316 T = TO (out)(err)	S = N/A O = 3989 T = 369.85 (out)(err)	S = OPT O = 2918 T = 27.42 (out)(err)	S = OPT O = 2918 T = 27.39 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2918 T = 9.62 (out)(err)	S = OPT O = 2918 T = 4.66 (out)(err)	S = OPT O = 2918 T = 36.84 (out)(err)	S = OPT O = 2918 T = 36.19 (out)(err)	S = N/A O = N/A 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.01	S = N/A O = 3345 T = TO (out)(err)	S = N/A O = 4094 T = TO (out)(err)	S = OPT O = 2878 T = 21.61 (out)(err)	S = OPT O = 2878 T = 21.45 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2878 T = 6.06 (out)(err)	S = OPT O = 2878 T = 2.01 (out)(err)	S = OPT O = 2878 T = 10.50 (out)(err)	S = OPT O = 2878 T = 10.47 (out)(err)	S = N/A O = N/A 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.38	S = N/A O = 3501 T = TO (out)(err)	S = N/A O = 3909 T = TO (out)(err)	S = OPT O = 3045 T = 31.62 (out)(err)	S = OPT O = 3045 T = 32.93 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 3045 T = 10.93 (out)(err)	S = OPT O = 3045 T = 5.38 (out)(err)	S = OPT O = 3045 T = 43.41 (out)(err)	S = OPT O = 3045 T = 42.03 (out)(err)	S = N/A O = N/A 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.59	S = N/A O = 3511 T = TO (out)(err)	S = N/A O = 3751 T = TO (out)(err)	S = OPT O = 3021 T = 6.39 (out)(err)	S = OPT O = 3021 T = 6.58 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 3021 T = 1.72 (out)(err)	S = OPT O = 3021 T = 1.59 (out)(err)	S = OPT O = 3021 T = 10.35 (out)(err)	S = OPT O = 3021 T = 9.81 (out)(err)	S = N/A O = N/A 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.59	S = N/A O = 3369 T = TO (out)(err)	S = N/A O = 3695 T = TO (out)(err)	S = OPT O = 2812 T = 55.90 (out)(err)	S = OPT O = 2812 T = 56.86 (out)(err)	S = N/A O = N/A T = 204.62 (out)(err)	S = OPT O = 2812 T = 14.31 (out)(err)	S = OPT O = 2812 T = 6.59 (out)(err)	S = OPT O = 2812 T = 36.75 (out)(err)	S = OPT O = 2812 T = 35.50 (out)(err)	S = N/A O = N/A 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 = 5.77	S = N/A O = 3369 T = TO (out)(err)	S = N/A O = 4247 T = TO (out)(err)	S = OPT O = 2838 T = 37.87 (out)(err)	S = OPT O = 2838 T = 38.94 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2838 T = 12.20 (out)(err)	S = OPT O = 2838 T = 5.77 (out)(err)	S = OPT O = 2838 T = 34.68 (out)(err)	S = OPT O = 2838 T = 32.83 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C3000_H150_7.wcnf	S = OPT O = 2815 T = 1.90	S = N/A O = 3553 T = TO (out)(err)	S = N/A O = 3826 T = TO (out)(err)	S = OPT O = 2815 T = 14.75 (out)(err)	S = OPT O = 2815 T = 14.62 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 2815 T = 4.03 (out)(err)	S = OPT O = 2815 T = 1.90 (out)(err)	S = OPT O = 2815 T = 8.20 (out)(err)	S = OPT O = 2815 T = 7.86 (out)(err)	S = N/A O = N/A 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.28	S = N/A O = 3609 T = TO (out)(err)	S = N/A O = 3796 T = 211.76 (out)(err)	S = OPT O = 3025 T = 39.05 (out)(err)	S = OPT O = 3025 T = 39.31 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 3025 T = 10.82 (out)(err)	S = OPT O = 3025 T = 5.28 (out)(err)	S = OPT O = 3025 T = 43.26 (out)(err)	S = OPT O = 3025 T = 43.30 (out)(err)	S = N/A O = N/A 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.31	S = N/A O = 3433 T = TO (out)(err)	S = N/A O = 3600 T = TO (out)(err)	S = OPT O = 2952 T = 17.30 (out)(err)	S = OPT O = 2952 T = 16.22 (out)(err)	S = N/A O = N/A T = 169.88 (out)(err)	S = OPT O = 2952 T = 4.57 (out)(err)	S = OPT O = 2952 T = 2.31 (out)(err)	S = OPT O = 2952 T = 24.02 (out)(err)	S = OPT O = 2952 T = 22.39 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_0.wcnf	S = OPT O = 3634 T = 7.20	S = N/A O = 4247 T = TO (out)(err)	S = N/A O = 4748 T = TO (out)(err)	S = OPT O = 3634 T = 61.77 (out)(err)	S = OPT O = 3634 T = 61.00 (out)(err)	S = N/A O = N/A T = 260.96 (out)(err)	S = OPT O = 3634 T = 22.94 (out)(err)	S = OPT O = 3634 T = 7.20 (out)(err)	S = OPT O = 3634 T = 94.98 (out)(err)	S = OPT O = 3634 T = 89.09 (out)(err)	S = N/A O = N/A 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.81	S = N/A O = 4317 T = TO (out)(err)	S = N/A O = 4647 T = TO (out)(err)	S = OPT O = 3662 T = 13.18 (out)(err)	S = OPT O = 3662 T = 13.88 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 3662 T = 3.88 (out)(err)	S = OPT O = 3662 T = 2.81 (out)(err)	S = OPT O = 3662 T = 22.51 (out)(err)	S = OPT O = 3662 T = 21.80 (out)(err)	S = N/A O = N/A 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 = 2.99	S = N/A O = 4348 T = TO (out)(err)	S = N/A O = 4429 T = TO (out)(err)	S = OPT O = 3827 T = 29.72 (out)(err)	S = OPT O = 3827 T = 29.10 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 3827 T = 7.48 (out)(err)	S = OPT O = 3827 T = 2.99 (out)(err)	S = OPT O = 3827 T = 54.53 (out)(err)	S = OPT O = 3827 T = 53.10 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = TO (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_3.wcnf	S = OPT O = 3512 T = 1.88	S = N/A O = 4110 T = TO (out)(err)	S = N/A O = 4479 T = TO (out)(err)	S = OPT O = 3512 T = 22.64 (out)(err)	S = OPT O = 3512 T = 22.68 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 3512 T = 5.93 (out)(err)	S = OPT O = 3512 T = 1.88 (out)(err)	S = OPT O = 3512 T = 16.45 (out)(err)	S = OPT O = 3512 T = 15.89 (out)(err)	S = N/A O = N/A 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.07	S = N/A O = 4090 T = TO (out)(err)	S = N/A O = 4109 T = TO (out)(err)	S = OPT O = 3355 T = 25.45 (out)(err)	S = OPT O = 3355 T = 25.22 (out)(err)	S = N/A O = N/A T = 309.39 (out)(err)	S = OPT O = 3355 T = 6.40 (out)(err)	S = OPT O = 3355 T = 5.07 (out)(err)	S = OPT O = 3355 T = 43.41 (out)(err)	S = OPT O = 3355 T = 41.79 (out)(err)	S = N/A O = N/A 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 = 6.90	S = N/A O = 4028 T = TO (out)(err)	S = N/A O = 5124 T = TO (out)(err)	S = OPT O = 3450 T = 74.17 (out)(err)	S = OPT O = 3450 T = 76.69 (out)(err)	S = N/A O = N/A T = 242.94 (out)(err)	S = OPT O = 3450 T = 13.49 (out)(err)	S = OPT O = 3450 T = 6.90 (out)(err)	S = OPT O = 3450 T = 64.58 (out)(err)	S = OPT O = 3450 T = 63.31 (out)(err)	S = N/A O = N/A 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.85	S = N/A O = 4310 T = TO (out)(err)	S = N/A O = 4588 T = TO (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 = OPT O = 3654 T = 1.45 (out)(err)	S = OPT O = 3654 T = 0.85 (out)(err)	S = OPT O = 3654 T = 3.24 (out)(err)	S = OPT O = 3654 T = 3.10 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L2_V150_C3500_H150_7.wcnf	S = OPT O = 3617 T = 2.60	S = N/A O = 4116 T = TO (out)(err)	S = N/A O = 4466 T = TO (out)(err)	S = OPT O = 3617 T = 9.53 (out)(err)	S = OPT O = 3617 T = 9.67 (out)(err)	S = N/A O = N/A T = 268.88 (out)(err)	S = OPT O = 3617 T = 4.06 (out)(err)	S = OPT O = 3617 T = 2.60 (out)(err)	S = OPT O = 3617 T = 24.49 (out)(err)	S = OPT O = 3617 T = 23.41 (out)(err)	S = N/A O = N/A 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.50	S = N/A O = 4214 T = TO (out)(err)	S = N/A O = 4629 T = TO (out)(err)	S = OPT O = 3525 T = 14.60 (out)(err)	S = OPT O = 3525 T = 13.52 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 3525 T = 3.48 (out)(err)	S = OPT O = 3525 T = 1.50 (out)(err)	S = OPT O = 3525 T = 10.49 (out)(err)	S = OPT O = 3525 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)
file_rwpms_wcnf_L2_V150_C3500_H150_9.wcnf	S = OPT O = 3240 T = 2.35	S = N/A O = 4171 T = TO (out)(err)	S = N/A O = 4437 T = TO (out)(err)	S = OPT O = 3240 T = 31.63 (out)(err)	S = OPT O = 3240 T = 33.42 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 3240 T = 8.01 (out)(err)	S = OPT O = 3240 T = 2.35 (out)(err)	S = OPT O = 3240 T = 9.72 (out)(err)	S = OPT O = 3240 T = 9.25 (out)(err)	S = N/A O = N/A 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 = N/A O = 31 T = TO (out)(err)	S = N/A O = 87 T = TO (out)(err)	S = OPT O = 28 T = 8.14 (out)(err)	S = OPT O = 28 T = 7.97 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 28 T = 9.76 (out)(err)	S = OPT O = 28 T = 3.11 (out)(err)	S = OPT O = 28 T = 6.03 (out)(err)	S = OPT O = 28 T = 6.06 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_1.wcnf	S = OPT O = 15 T = 0.99	S = OPT O = 15 T = 162.62 (out)(err)	S = N/A O = 40 T = TO (out)(err)	S = OPT O = 15 T = 11.33 (out)(err)	S = OPT O = 15 T = 11.13 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 15 T = 6.41 (out)(err)	S = OPT O = 15 T = 0.99 (out)(err)	S = OPT O = 15 T = 1.33 (out)(err)	S = OPT O = 15 T = 1.34 (out)(err)	S = N/A O = N/A T = TO (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.20	S = N/A O = 206 T = TO (out)(err)	S = N/A O = 111 T = TO (out)(err)	S = OPT O = 25 T = 9.72 (out)(err)	S = OPT O = 25 T = 9.58 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 25 T = 6.79 (out)(err)	S = OPT O = 25 T = 2.20 (out)(err)	S = OPT O = 25 T = 3.52 (out)(err)	S = OPT O = 25 T = 3.51 (out)(err)	S = N/A O = N/A 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.23	S = N/A O = 185 T = TO (out)(err)	S = N/A O = 83 T = TO (out)(err)	S = OPT O = 25 T = 15.39 (out)(err)	S = OPT O = 25 T = 15.19 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 25 T = 8.27 (out)(err)	S = OPT O = 25 T = 2.23 (out)(err)	S = OPT O = 25 T = 3.73 (out)(err)	S = OPT O = 25 T = 3.65 (out)(err)	S = N/A O = N/A 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.57	S = N/A O = 30 T = TO (out)(err)	S = N/A O = 76 T = TO (out)(err)	S = OPT O = 30 T = 5.68 (out)(err)	S = OPT O = 30 T = 5.64 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 30 T = 5.75 (out)(err)	S = OPT O = 30 T = 3.57 (out)(err)	S = OPT O = 30 T = 6.25 (out)(err)	S = OPT O = 30 T = 6.26 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_5.wcnf	S = OPT O = 27 T = 2.00	S = N/A O = 153 T = TO (out)(err)	S = N/A O = 66 T = TO (out)(err)	S = OPT O = 27 T = 3.76 (out)(err)	S = OPT O = 27 T = 3.71 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 27 T = 5.38 (out)(err)	S = OPT O = 27 T = 2.00 (out)(err)	S = OPT O = 27 T = 3.48 (out)(err)	S = OPT O = 27 T = 3.44 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C600_H100_6.wcnf	S = OPT O = 26 T = 2.72	S = OPT O = 26 T = 1406.26 (out)(err)	S = N/A O = 52 T = TO (out)(err)	S = OPT O = 26 T = 10.95 (out)(err)	S = OPT O = 26 T = 10.74 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 26 T = 10.45 (out)(err)	S = OPT O = 26 T = 2.72 (out)(err)	S = OPT O = 26 T = 4.49 (out)(err)	S = OPT O = 26 T = 4.42 (out)(err)	S = N/A O = N/A 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.76	S = N/A O = 31 T = TO (out)(err)	S = N/A O = 82 T = TO (out)(err)	S = OPT O = 29 T = 29.63 (out)(err)	S = OPT O = 29 T = 29.48 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 29 T = 12.29 (out)(err)	S = OPT O = 29 T = 8.76 (out)(err)	S = OPT O = 29 T = 17.44 (out)(err)	S = OPT O = 29 T = 17.17 (out)(err)	S = N/A O = N/A 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.53	S = OPT O = 19 T = 711.48 (out)(err)	S = N/A O = 27 T = TO (out)(err)	S = OPT O = 19 T = 19.29 (out)(err)	S = OPT O = 19 T = 19.05 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 19 T = 9.72 (out)(err)	S = OPT O = 19 T = 2.53 (out)(err)	S = OPT O = 19 T = 4.76 (out)(err)	S = OPT O = 19 T = 4.70 (out)(err)	S = N/A O = N/A T = TO (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 = 4.88	S = N/A O = 156 T = TO (out)(err)	S = N/A O = 82 T = TO (out)(err)	S = OPT O = 30 T = 11.31 (out)(err)	S = OPT O = 30 T = 11.15 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 30 T = 7.40 (out)(err)	S = OPT O = 30 T = 4.88 (out)(err)	S = OPT O = 30 T = 8.59 (out)(err)	S = OPT O = 30 T = 8.62 (out)(err)	S = N/A O = N/A 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.30	S = N/A O = 214 T = TO (out)(err)	S = N/A O = 194 T = TO (out)(err)	S = OPT O = 54 T = 88.03 (out)(err)	S = OPT O = 54 T = 88.08 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 54 T = 38.62 (out)(err)	S = OPT O = 54 T = 11.30 (out)(err)	S = OPT O = 54 T = 22.18 (out)(err)	S = OPT O = 54 T = 22.36 (out)(err)	S = N/A O = N/A T = TO (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 = 37.76	S = N/A O = 267 T = TO (out)(err)	S = N/A O = 217 T = TO (out)(err)	S = OPT O = 58 T = 84.44 (out)(err)	S = OPT O = 58 T = 83.15 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 58 T = 132.16 (out)(err)	S = OPT O = 58 T = 37.76 (out)(err)	S = OPT O = 58 T = 77.32 (out)(err)	S = OPT O = 58 T = 74.55 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_2.wcnf	S = OPT O = 59 T = 26.21	S = N/A O = 258 T = TO (out)(err)	S = N/A O = 194 T = TO (out)(err)	S = OPT O = 59 T = 97.24 (out)(err)	S = OPT O = 59 T = 96.58 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 59 T = 59.58 (out)(err)	S = OPT O = 59 T = 26.21 (out)(err)	S = OPT O = 59 T = 49.00 (out)(err)	S = OPT O = 59 T = 48.30 (out)(err)	S = N/A O = N/A 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.61	S = N/A O = 223 T = TO (out)(err)	S = N/A O = 161 T = TO (out)(err)	S = OPT O = 48 T = 49.89 (out)(err)	S = OPT O = 48 T = 49.43 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 48 T = 50.99 (out)(err)	S = OPT O = 48 T = 21.61 (out)(err)	S = OPT O = 48 T = 37.64 (out)(err)	S = OPT O = 48 T = 37.45 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_4.wcnf	S = OPT O = 42 T = 7.26	S = N/A O = 279 T = TO (out)(err)	S = N/A O = 214 T = TO (out)(err)	S = OPT O = 42 T = 13.12 (out)(err)	S = OPT O = 42 T = 12.98 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 42 T = 24.46 (out)(err)	S = OPT O = 42 T = 7.26 (out)(err)	S = OPT O = 42 T = 14.07 (out)(err)	S = OPT O = 42 T = 13.91 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C700_H100_5.wcnf	S = OPT O = 46 T = 9.26	S = N/A O = 168 T = TO (out)(err)	S = N/A O = 225 T = TO (out)(err)	S = OPT O = 46 T = 74.10 (out)(err)	S = OPT O = 46 T = 73.65 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 46 T = 41.98 (out)(err)	S = OPT O = 46 T = 9.26 (out)(err)	S = OPT O = 46 T = 19.27 (out)(err)	S = OPT O = 46 T = 19.26 (out)(err)	S = N/A O = N/A 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 = 30.72	S = N/A O = 84 T = TO (out)(err)	S = N/A O = 234 T = TO (out)(err)	S = OPT O = 51 T = 99.48 (out)(err)	S = OPT O = 51 T = 98.67 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 51 T = 56.62 (out)(err)	S = OPT O = 51 T = 30.72 (out)(err)	S = OPT O = 51 T = 58.64 (out)(err)	S = OPT O = 51 T = 58.54 (out)(err)	S = N/A O = N/A 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 = 49.93	S = N/A O = 219 T = TO (out)(err)	S = N/A O = 261 T = TO (out)(err)	S = OPT O = 63 T = 108.79 (out)(err)	S = OPT O = 63 T = 108.45 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 63 T = 61.06 (out)(err)	S = OPT O = 63 T = 49.93 (out)(err)	S = OPT O = 63 T = 111.03 (out)(err)	S = OPT O = 63 T = 110.30 (out)(err)	S = N/A O = N/A 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 = 93.53	S = N/A O = 227 T = TO (out)(err)	S = N/A O = 220 T = TO (out)(err)	S = OPT O = 64 T = 196.42 (out)(err)	S = OPT O = 64 T = 195.60 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 64 T = 131.01 (out)(err)	S = OPT O = 64 T = 93.53 (out)(err)	S = OPT O = 64 T = 194.38 (out)(err)	S = OPT O = 64 T = 190.65 (out)(err)	S = N/A O = N/A T = TO (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 = 8.56	S = N/A O = 234 T = TO (out)(err)	S = N/A O = 187 T = TO (out)(err)	S = OPT O = 45 T = 35.70 (out)(err)	S = OPT O = 45 T = 35.56 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 45 T = 25.08 (out)(err)	S = OPT O = 45 T = 8.56 (out)(err)	S = OPT O = 45 T = 14.72 (out)(err)	S = OPT O = 45 T = 14.69 (out)(err)	S = N/A O = N/A T = TO (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 = 124.93	S = N/A O = 270 T = TO (out)(err)	S = N/A O = 383 T = TO (out)(err)	S = OPT O = 95 T = 358.60 (out)(err)	S = OPT O = 95 T = 358.59 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 95 T = 211.82 (out)(err)	S = OPT O = 95 T = 124.93 (out)(err)	S = OPT O = 95 T = 259.69 (out)(err)	S = OPT O = 95 T = 257.87 (out)(err)	S = N/A O = N/A T = TO (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 = 86.11	S = N/A O = 279 T = TO (out)(err)	S = N/A O = 349 T = TO (out)(err)	S = OPT O = 81 T = 216.84 (out)(err)	S = OPT O = 81 T = 216.33 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 81 T = 135.57 (out)(err)	S = OPT O = 81 T = 86.11 (out)(err)	S = OPT O = 81 T = 166.63 (out)(err)	S = OPT O = 81 T = 164.42 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_2.wcnf	S = OPT O = 77 T = 92.47	S = N/A O = 212 T = TO (out)(err)	S = N/A O = 240 T = TO (out)(err)	S = OPT O = 77 T = 276.03 (out)(err)	S = OPT O = 77 T = 274.46 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 77 T = 171.94 (out)(err)	S = OPT O = 77 T = 92.47 (out)(err)	S = OPT O = 77 T = 176.90 (out)(err)	S = OPT O = 77 T = 174.85 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_3.wcnf	S = OPT O = 81 T = 32.06	S = N/A O = 271 T = TO (out)(err)	S = N/A O = 320 T = TO (out)(err)	S = OPT O = 81 T = 136.51 (out)(err)	S = OPT O = 81 T = 135.62 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 81 T = 71.12 (out)(err)	S = OPT O = 81 T = 32.06 (out)(err)	S = OPT O = 81 T = 74.28 (out)(err)	S = OPT O = 81 T = 73.25 (out)(err)	S = N/A O = N/A T = TO (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 = 87.76	S = N/A O = 306 T = TO (out)(err)	S = N/A O = 318 T = TO (out)(err)	S = OPT O = 75 T = 197.10 (out)(err)	S = OPT O = 75 T = 197.39 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 75 T = 169.18 (out)(err)	S = OPT O = 75 T = 87.76 (out)(err)	S = OPT O = 75 T = 189.75 (out)(err)	S = OPT O = 75 T = 184.98 (out)(err)	S = N/A O = N/A 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.38	S = N/A O = 289 T = TO (out)(err)	S = N/A O = 258 T = TO (out)(err)	S = OPT O = 80 T = 97.87 (out)(err)	S = OPT O = 80 T = 97.17 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 80 T = 60.47 (out)(err)	S = OPT O = 80 T = 50.38 (out)(err)	S = OPT O = 80 T = 106.85 (out)(err)	S = OPT O = 80 T = 106.64 (out)(err)	S = N/A O = N/A 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.02	S = N/A O = 293 T = TO (out)(err)	S = N/A O = 412 T = TO (out)(err)	S = OPT O = 74 T = 118.18 (out)(err)	S = OPT O = 74 T = 117.54 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 74 T = 81.85 (out)(err)	S = OPT O = 74 T = 49.02 (out)(err)	S = OPT O = 74 T = 100.30 (out)(err)	S = OPT O = 74 T = 100.44 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)
file_rwpms_wcnf_L3_V100_C800_H100_7.wcnf	S = OPT O = 99 T = 91.17	S = N/A O = 315 T = TO (out)(err)	S = N/A O = 306 T = TO (out)(err)	S = OPT O = 99 T = 355.50 (out)(err)	S = OPT O = 99 T = 354.53 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 99 T = 190.33 (out)(err)	S = OPT O = 99 T = 91.17 (out)(err)	S = OPT O = 99 T = 229.23 (out)(err)	S = OPT O = 99 T = 224.49 (out)(err)	S = N/A O = N/A 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.38	S = N/A O = 138 T = TO (out)(err)	S = N/A O = 301 T = TO (out)(err)	S = OPT O = 90 T = 591.18 (out)(err)	S = OPT O = 90 T = 592.16 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 90 T = 397.45 (out)(err)	S = OPT O = 90 T = 224.38 (out)(err)	S = OPT O = 90 T = 411.13 (out)(err)	S = OPT O = 90 T = 398.54 (out)(err)	S = N/A O = N/A T = TO (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 = 171.39	S = N/A O = 146 T = TO (out)(err)	S = N/A O = 313 T = TO (out)(err)	S = OPT O = 95 T = 335.92 (out)(err)	S = OPT O = 95 T = 333.96 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = OPT O = 95 T = 229.41 (out)(err)	S = OPT O = 95 T = 171.39 (out)(err)	S = OPT O = 95 T = 424.92 (out)(err)	S = OPT O = 95 T = 420.64 (out)(err)	S = N/A O = N/A T = TO (out)(err)	S = N/A O = N/A T = 1800.00 (out)(err)