Benchmark

LabelMeaning
SSolution {OPTIMUM FOUND or OPT | UNSATISFIABLE or UNSAT | UNKNOWN | Not available or N/A}
OBest solution found
TCPU time (TO for Time Out)
(out)(err)Standard output and standard error for each solver

ColorMeaning for Complete SolversMeaning for Incomplete Solvers
TextBest solver columnBest solver column
TextOptimal solution with the best CPU timeBest solution with the best CPU time
TextOptimal solution and finished within the Time OutBest solution without the best CPU time
TextOptimal solution and did not finish within the Time OutSolution found but not the best
TextTime OutTime Out
TextBuggy solutionBuggy solution

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