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+-wms MSUnCore MaxHS Maxsatz2013f Toulbar2 WMaxSatz+ WMaxSatz09 WPM1-2013 WPM2-2013 ahmaxsat ckmax-small glpk-maxsat optimax-ni optimax scip-maxsat toysat wbo2.1-wcnf wmifumax
s2v100c1200_1.wcnf S = OPT
O = 865
T = 6.07
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 865
T = 6.94
(out)(err)
S = N/A
O = 1065
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 865
T = 12.28
(out)(err)
S = N/A
O = 940
T = TO
(out)(err)
S = OPT
O = 865
T = 31.09
(out)(err)
S = OPT
O = 865
T = 28.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 = 865
T = 354.94
(out)(err)
S = OPT
O = 865
T = 6.07
(out)(err)
S = N/A
O = 932
T = TO
(out)(err)
S = N/A
O = 1236
T = TO
(out)(err)
S = N/A
O = 1211
T = TO
(out)(err)
S = N/A
O = 896
T = TO
(out)(err)
S = N/A
O = 1299
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.97
(out)(err)
S = N/A
O = N/A
T = 1750.65
(out)(err)
s2v100c1200_2.wcnf S = OPT
O = 774
T = 2.85
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 774
T = 5.01
(out)(err)
S = N/A
O = 992
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 774
T = 6.72
(out)(err)
S = N/A
O = 859
T = TO
(out)(err)
S = OPT
O = 774
T = 18.73
(out)(err)
S = OPT
O = 774
T = 20.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 = 774
T = 258.95
(out)(err)
S = OPT
O = 774
T = 2.85
(out)(err)
S = N/A
O = 841
T = TO
(out)(err)
S = N/A
O = 1088
T = TO
(out)(err)
S = N/A
O = 1100
T = TO
(out)(err)
S = N/A
O = 782
T = TO
(out)(err)
S = N/A
O = 1016
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.81
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1200_3.wcnf S = OPT
O = 933
T = 27.10
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 933
T = 27.57
(out)(err)
S = N/A
O = 1199
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 933
T = 48.92
(out)(err)
S = N/A
O = 993
T = TO
(out)(err)
S = OPT
O = 933
T = 147.82
(out)(err)
S = OPT
O = 933
T = 134.37
(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 = 938
T = 1797.81
(out)(err)
S = OPT
O = 933
T = 27.10
(out)(err)
S = N/A
O = 1009
T = TO
(out)(err)
S = N/A
O = 1318
T = TO
(out)(err)
S = N/A
O = 1276
T = TO
(out)(err)
S = N/A
O = 948
T = TO
(out)(err)
S = N/A
O = 1231
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.75
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1200_4.wcnf S = OPT
O = 798
T = 2.73
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 798
T = 4.49
(out)(err)
S = N/A
O = 1039
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 798
T = 4.35
(out)(err)
S = N/A
O = 931
T = TO
(out)(err)
S = OPT
O = 798
T = 11.34
(out)(err)
S = OPT
O = 798
T = 11.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 = 798
T = 169.06
(out)(err)
S = OPT
O = 798
T = 2.73
(out)(err)
S = N/A
O = 892
T = TO
(out)(err)
S = N/A
O = 1229
T = TO
(out)(err)
S = N/A
O = 1154
T = TO
(out)(err)
S = N/A
O = 805
T = TO
(out)(err)
S = N/A
O = 1256
T = TO
(out)(err)
S = N/A
O = N/A
T = 198.97
(out)(err)
S = N/A
O = N/A
T = 1438.41
(out)(err)
s2v100c1200_5.wcnf S = OPT
O = 876
T = 4.03
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 876
T = 5.39
(out)(err)
S = N/A
O = 1097
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 876
T = 10.70
(out)(err)
S = N/A
O = 950
T = TO
(out)(err)
S = OPT
O = 876
T = 30.23
(out)(err)
S = OPT
O = 876
T = 29.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 = 876
T = 507.85
(out)(err)
S = OPT
O = 876
T = 4.03
(out)(err)
S = N/A
O = 979
T = TO
(out)(err)
S = N/A
O = 1107
T = TO
(out)(err)
S = N/A
O = 1237
T = TO
(out)(err)
S = N/A
O = 903
T = TO
(out)(err)
S = N/A
O = 1263
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.83
(out)(err)
S = N/A
O = N/A
T = 990.47
(out)(err)
s2v100c1200_6.wcnf S = OPT
O = 734
T = 0.72
S = OPT
O = 734
T = 222.47
(out)(err)
S = OPT
O = 734
T = 1.08
(out)(err)
S = N/A
O = 1005
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 734
T = 0.72
(out)(err)
S = N/A
O = 747
T = TO
(out)(err)
S = OPT
O = 734
T = 2.38
(out)(err)
S = OPT
O = 734
T = 2.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 = 734
T = 22.03
(out)(err)
S = OPT
O = 734
T = 0.89
(out)(err)
S = N/A
O = 815
T = TO
(out)(err)
S = N/A
O = 963
T = TO
(out)(err)
S = N/A
O = 957
T = TO
(out)(err)
S = N/A
O = 735
T = TO
(out)(err)
S = N/A
O = 1063
T = TO
(out)(err)
S = N/A
O = N/A
T = 181.06
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1200_7.wcnf S = OPT
O = 800
T = 10.97
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 800
T = 12.95
(out)(err)
S = N/A
O = 1069
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 800
T = 17.17
(out)(err)
S = N/A
O = 868
T = TO
(out)(err)
S = OPT
O = 800
T = 50.64
(out)(err)
S = OPT
O = 800
T = 48.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 = 800
T = 708.15
(out)(err)
S = OPT
O = 800
T = 10.97
(out)(err)
S = N/A
O = 857
T = TO
(out)(err)
S = N/A
O = 1128
T = TO
(out)(err)
S = N/A
O = 1106
T = TO
(out)(err)
S = N/A
O = 805
T = TO
(out)(err)
S = N/A
O = 1258
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.64
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1200_8.wcnf S = OPT
O = 962
T = 28.71
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 962
T = 28.71
(out)(err)
S = N/A
O = 1374
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 962
T = 74.82
(out)(err)
S = N/A
O = 1030
T = TO
(out)(err)
S = OPT
O = 962
T = 231.66
(out)(err)
S = OPT
O = 962
T = 231.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 = 962
T = 1797.73
(out)(err)
S = OPT
O = 962
T = 34.90
(out)(err)
S = N/A
O = 1047
T = TO
(out)(err)
S = N/A
O = 1291
T = TO
(out)(err)
S = N/A
O = 1326
T = TO
(out)(err)
S = N/A
O = 1002
T = TO
(out)(err)
S = N/A
O = 1456
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.62
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1300_1.wcnf S = OPT
O = 971
T = 6.26
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 971
T = 6.26
(out)(err)
S = N/A
O = 1260
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 971
T = 16.82
(out)(err)
S = N/A
O = 1042
T = TO
(out)(err)
S = OPT
O = 971
T = 54.97
(out)(err)
S = OPT
O = 971
T = 44.76
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 971
T = 796.11
(out)(err)
S = OPT
O = 971
T = 11.53
(out)(err)
S = N/A
O = 1048
T = TO
(out)(err)
S = N/A
O = 1251
T = TO
(out)(err)
S = N/A
O = 1310
T = TO
(out)(err)
S = N/A
O = 1002
T = TO
(out)(err)
S = N/A
O = 1439
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.75
(out)(err)
S = N/A
O = N/A
T = 1478.73
(out)(err)
s2v100c1300_2.wcnf S = OPT
O = 930
T = 11.34
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 930
T = 11.71
(out)(err)
S = N/A
O = 1151
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 930
T = 51.77
(out)(err)
S = N/A
O = 1007
T = TO
(out)(err)
S = OPT
O = 930
T = 153.01
(out)(err)
S = OPT
O = 930
T = 155.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 = 930
T = 1245.37
(out)(err)
S = OPT
O = 930
T = 11.34
(out)(err)
S = N/A
O = 1033
T = TO
(out)(err)
S = N/A
O = 1386
T = TO
(out)(err)
S = N/A
O = 1293
T = TO
(out)(err)
S = N/A
O = 972
T = TO
(out)(err)
S = N/A
O = 1404
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.84
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1300_3.wcnf S = OPT
O = 925
T = 3.54
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 925
T = 6.99
(out)(err)
S = N/A
O = 1057
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 925
T = 10.22
(out)(err)
S = N/A
O = 993
T = TO
(out)(err)
S = OPT
O = 925
T = 27.05
(out)(err)
S = OPT
O = 925
T = 27.52
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 925
T = 385.40
(out)(err)
S = OPT
O = 925
T = 3.54
(out)(err)
S = N/A
O = 1025
T = TO
(out)(err)
S = N/A
O = 1266
T = TO
(out)(err)
S = N/A
O = 1139
T = TO
(out)(err)
S = N/A
O = 926
T = TO
(out)(err)
S = N/A
O = 1271
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.85
(out)(err)
S = N/A
O = N/A
T = 1057.62
(out)(err)
s2v100c1300_4.wcnf S = OPT
O = 970
T = 7.44
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 970
T = 10.42
(out)(err)
S = N/A
O = 1279
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 970
T = 25.34
(out)(err)
S = N/A
O = 1061
T = TO
(out)(err)
S = OPT
O = 970
T = 75.44
(out)(err)
S = OPT
O = 970
T = 75.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 = 970
T = 1421.33
(out)(err)
S = OPT
O = 970
T = 7.44
(out)(err)
S = N/A
O = 1083
T = TO
(out)(err)
S = N/A
O = 1293
T = TO
(out)(err)
S = N/A
O = 1295
T = TO
(out)(err)
S = N/A
O = 1006
T = TO
(out)(err)
S = N/A
O = 1550
T = TO
(out)(err)
S = N/A
O = N/A
T = 181.97
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1300_5.wcnf S = OPT
O = 962
T = 17.60
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 962
T = 21.43
(out)(err)
S = N/A
O = 1246
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 962
T = 52.70
(out)(err)
S = N/A
O = 1095
T = TO
(out)(err)
S = OPT
O = 962
T = 142.03
(out)(err)
S = OPT
O = 962
T = 149.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 = 962
T = 1343.69
(out)(err)
S = OPT
O = 962
T = 17.60
(out)(err)
S = N/A
O = 1054
T = TO
(out)(err)
S = N/A
O = 1305
T = TO
(out)(err)
S = N/A
O = 1237
T = TO
(out)(err)
S = N/A
O = 980
T = TO
(out)(err)
S = N/A
O = 1244
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.88
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1300_6.wcnf S = OPT
O = 933
T = 3.97
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 933
T = 3.97
(out)(err)
S = N/A
O = 1271
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 933
T = 15.21
(out)(err)
S = N/A
O = 983
T = TO
(out)(err)
S = OPT
O = 933
T = 31.14
(out)(err)
S = OPT
O = 933
T = 33.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 = 933
T = 482.56
(out)(err)
S = OPT
O = 933
T = 5.57
(out)(err)
S = N/A
O = 1040
T = TO
(out)(err)
S = N/A
O = 1236
T = TO
(out)(err)
S = N/A
O = 1361
T = TO
(out)(err)
S = N/A
O = 970
T = TO
(out)(err)
S = N/A
O = 1223
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.96
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1300_7.wcnf S = OPT
O = 877
T = 3.44
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 877
T = 8.02
(out)(err)
S = N/A
O = 1187
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 877
T = 11.41
(out)(err)
S = N/A
O = 958
T = TO
(out)(err)
S = OPT
O = 877
T = 32.65
(out)(err)
S = OPT
O = 877
T = 31.63
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 877
T = 590.32
(out)(err)
S = OPT
O = 877
T = 3.44
(out)(err)
S = N/A
O = 962
T = TO
(out)(err)
S = N/A
O = 1235
T = TO
(out)(err)
S = N/A
O = 1281
T = TO
(out)(err)
S = N/A
O = 892
T = TO
(out)(err)
S = N/A
O = 1316
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.81
(out)(err)
S = N/A
O = N/A
T = 1673.37
(out)(err)
s2v100c1300_8.wcnf S = OPT
O = 941
T = 8.32
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 941
T = 17.07
(out)(err)
S = N/A
O = 1261
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 941
T = 35.12
(out)(err)
S = N/A
O = 1011
T = TO
(out)(err)
S = OPT
O = 941
T = 105.44
(out)(err)
S = OPT
O = 941
T = 105.27
(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 = 962
T = 1797.61
(out)(err)
S = OPT
O = 941
T = 8.32
(out)(err)
S = N/A
O = 1043
T = TO
(out)(err)
S = N/A
O = 1169
T = TO
(out)(err)
S = N/A
O = 1213
T = TO
(out)(err)
S = N/A
O = 986
T = TO
(out)(err)
S = N/A
O = 1251
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.94
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1400_1.wcnf S = OPT
O = 1019
T = 23.03
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1019
T = 23.92
(out)(err)
S = N/A
O = 1398
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1019
T = 35.74
(out)(err)
S = N/A
O = 1140
T = TO
(out)(err)
S = OPT
O = 1019
T = 112.25
(out)(err)
S = OPT
O = 1019
T = 109.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 = 1019
T = 1797.88
(out)(err)
S = OPT
O = 1019
T = 23.03
(out)(err)
S = N/A
O = 1123
T = TO
(out)(err)
S = N/A
O = 1358
T = TO
(out)(err)
S = N/A
O = 1388
T = TO
(out)(err)
S = N/A
O = 1052
T = TO
(out)(err)
S = N/A
O = 1468
T = TO
(out)(err)
S = N/A
O = N/A
T = 317.88
(out)(err)
S = N/A
O = N/A
T = 1758.46
(out)(err)
s2v100c1400_2.wcnf S = OPT
O = 1002
T = 9.77
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1002
T = 9.77
(out)(err)
S = N/A
O = 1363
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1002
T = 29.18
(out)(err)
S = N/A
O = 1126
T = TO
(out)(err)
S = OPT
O = 1002
T = 88.82
(out)(err)
S = OPT
O = 1002
T = 85.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 = 1002
T = 977.71
(out)(err)
S = OPT
O = 1002
T = 12.53
(out)(err)
S = N/A
O = 1073
T = TO
(out)(err)
S = N/A
O = 1384
T = TO
(out)(err)
S = N/A
O = 1338
T = TO
(out)(err)
S = N/A
O = 1010
T = TO
(out)(err)
S = N/A
O = 1280
T = TO
(out)(err)
S = N/A
O = N/A
T = 193.97
(out)(err)
S = N/A
O = N/A
T = 1541.79
(out)(err)
s2v100c1400_3.wcnf S = OPT
O = 1020
T = 13.16
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1020
T = 13.16
(out)(err)
S = N/A
O = 1372
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1020
T = 58.76
(out)(err)
S = N/A
O = 1116
T = TO
(out)(err)
S = OPT
O = 1020
T = 183.05
(out)(err)
S = OPT
O = 1020
T = 174.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 = 1020
T = 1797.86
(out)(err)
S = OPT
O = 1020
T = 22.55
(out)(err)
S = N/A
O = 1108
T = TO
(out)(err)
S = N/A
O = 1341
T = TO
(out)(err)
S = N/A
O = 1400
T = TO
(out)(err)
S = N/A
O = 1039
T = TO
(out)(err)
S = N/A
O = 1253
T = TO
(out)(err)
S = N/A
O = N/A
T = 212.64
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1400_4.wcnf S = OPT
O = 1094
T = 28.40
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1094
T = 28.40
(out)(err)
S = N/A
O = 1425
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1094
T = 74.35
(out)(err)
S = N/A
O = 1149
T = TO
(out)(err)
S = OPT
O = 1094
T = 213.08
(out)(err)
S = OPT
O = 1094
T = 229.51
(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 = 1097
T = 1797.83
(out)(err)
S = OPT
O = 1094
T = 46.43
(out)(err)
S = N/A
O = 1188
T = TO
(out)(err)
S = N/A
O = 1583
T = TO
(out)(err)
S = N/A
O = 1638
T = TO
(out)(err)
S = N/A
O = 1140
T = TO
(out)(err)
S = N/A
O = 1466
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.54
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1400_5.wcnf S = OPT
O = 1018
T = 10.09
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1018
T = 12.47
(out)(err)
S = N/A
O = 1323
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1018
T = 33.93
(out)(err)
S = N/A
O = 1077
T = TO
(out)(err)
S = OPT
O = 1018
T = 108.08
(out)(err)
S = OPT
O = 1018
T = 105.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 = 1018
T = 1339.34
(out)(err)
S = OPT
O = 1018
T = 10.09
(out)(err)
S = N/A
O = 1147
T = TO
(out)(err)
S = N/A
O = 1379
T = TO
(out)(err)
S = N/A
O = 1437
T = TO
(out)(err)
S = N/A
O = 1048
T = TO
(out)(err)
S = N/A
O = 1437
T = TO
(out)(err)
S = N/A
O = N/A
T = 199.03
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1400_6.wcnf S = OPT
O = 997
T = 3.28
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 997
T = 3.28
(out)(err)
S = N/A
O = 1420
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 997
T = 8.31
(out)(err)
S = N/A
O = 1106
T = TO
(out)(err)
S = OPT
O = 997
T = 21.92
(out)(err)
S = OPT
O = 997
T = 21.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 = 997
T = 684.40
(out)(err)
S = OPT
O = 997
T = 4.35
(out)(err)
S = N/A
O = 1119
T = TO
(out)(err)
S = N/A
O = 1390
T = TO
(out)(err)
S = N/A
O = 1417
T = TO
(out)(err)
S = N/A
O = 1025
T = TO
(out)(err)
S = N/A
O = 1427
T = TO
(out)(err)
S = N/A
O = N/A
T = 317.49
(out)(err)
S = N/A
O = N/A
T = 1491.17
(out)(err)
s2v100c1400_7.wcnf S = OPT
O = 1001
T = 24.33
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1001
T = 24.33
(out)(err)
S = N/A
O = 1308
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1001
T = 57.93
(out)(err)
S = N/A
O = 1056
T = TO
(out)(err)
S = OPT
O = 1001
T = 160.01
(out)(err)
S = OPT
O = 1001
T = 165.01
(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 = 1002
T = 1797.84
(out)(err)
S = OPT
O = 1001
T = 30.98
(out)(err)
S = N/A
O = 1075
T = TO
(out)(err)
S = N/A
O = 1185
T = TO
(out)(err)
S = N/A
O = 1339
T = TO
(out)(err)
S = N/A
O = 1052
T = TO
(out)(err)
S = N/A
O = 1580
T = TO
(out)(err)
S = N/A
O = N/A
T = 188.81
(out)(err)
S = N/A
O = N/A
T = 1002.49
(out)(err)
s2v100c1400_8.wcnf S = OPT
O = 1084
T = 19.95
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1084
T = 19.95
(out)(err)
S = N/A
O = 1341
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1084
T = 68.32
(out)(err)
S = N/A
O = 1143
T = TO
(out)(err)
S = OPT
O = 1084
T = 107.62
(out)(err)
S = OPT
O = 1084
T = 194.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 = 1084
T = 1797.81
(out)(err)
S = OPT
O = 1084
T = 21.79
(out)(err)
S = N/A
O = 1186
T = TO
(out)(err)
S = N/A
O = 1392
T = TO
(out)(err)
S = N/A
O = 1455
T = TO
(out)(err)
S = N/A
O = 1109
T = TO
(out)(err)
S = N/A
O = 1472
T = TO
(out)(err)
S = N/A
O = N/A
T = 201.55
(out)(err)
S = N/A
O = N/A
T = 1470.61
(out)(err)
s2v100c1500_1.wcnf S = OPT
O = 1077
T = 12.32
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1077
T = 16.24
(out)(err)
S = N/A
O = 1449
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1077
T = 27.37
(out)(err)
S = N/A
O = 1204
T = TO
(out)(err)
S = OPT
O = 1077
T = 80.06
(out)(err)
S = OPT
O = 1077
T = 79.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 = 1077
T = 1242.31
(out)(err)
S = OPT
O = 1077
T = 12.32
(out)(err)
S = N/A
O = 1156
T = TO
(out)(err)
S = N/A
O = 1436
T = TO
(out)(err)
S = N/A
O = 1450
T = TO
(out)(err)
S = N/A
O = 1092
T = TO
(out)(err)
S = N/A
O = 1627
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.87
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1500_2.wcnf S = OPT
O = 1125
T = 11.89
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1125
T = 11.89
(out)(err)
S = N/A
O = 1456
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1125
T = 67.53
(out)(err)
S = N/A
O = 1263
T = TO
(out)(err)
S = OPT
O = 1125
T = 195.70
(out)(err)
S = OPT
O = 1125
T = 197.23
(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 = 1155
T = 1797.86
(out)(err)
S = OPT
O = 1125
T = 16.32
(out)(err)
S = N/A
O = 1229
T = TO
(out)(err)
S = N/A
O = 1582
T = TO
(out)(err)
S = N/A
O = 1484
T = TO
(out)(err)
S = N/A
O = 1138
T = TO
(out)(err)
S = N/A
O = 1444
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.58
(out)(err)
S = N/A
O = N/A
T = 971.88
(out)(err)
s2v100c1500_3.wcnf S = OPT
O = 1151
T = 22.68
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1151
T = 22.68
(out)(err)
S = N/A
O = 1490
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1151
T = 66.26
(out)(err)
S = N/A
O = 1267
T = TO
(out)(err)
S = OPT
O = 1151
T = 190.02
(out)(err)
S = OPT
O = 1151
T = 188.74
(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 = 1151
T = 1797.88
(out)(err)
S = OPT
O = 1151
T = 39.51
(out)(err)
S = N/A
O = 1265
T = TO
(out)(err)
S = N/A
O = 1474
T = TO
(out)(err)
S = N/A
O = 1478
T = TO
(out)(err)
S = N/A
O = 1197
T = TO
(out)(err)
S = N/A
O = 1419
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.77
(out)(err)
S = N/A
O = N/A
T = 1366.77
(out)(err)
s2v100c1500_4.wcnf S = OPT
O = 1072
T = 13.78
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1072
T = 38.75
(out)(err)
S = N/A
O = 1536
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1072
T = 65.63
(out)(err)
S = N/A
O = 1137
T = TO
(out)(err)
S = OPT
O = 1072
T = 195.66
(out)(err)
S = OPT
O = 1072
T = 199.39
(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 = 1098
T = 1797.73
(out)(err)
S = OPT
O = 1072
T = 13.78
(out)(err)
S = N/A
O = 1180
T = TO
(out)(err)
S = N/A
O = 1442
T = TO
(out)(err)
S = N/A
O = 1452
T = TO
(out)(err)
S = N/A
O = 1094
T = TO
(out)(err)
S = N/A
O = 1461
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.52
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1500_5.wcnf S = OPT
O = 1151
T = 20.97
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1151
T = 20.97
(out)(err)
S = N/A
O = 1347
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1151
T = 82.83
(out)(err)
S = N/A
O = 1292
T = TO
(out)(err)
S = OPT
O = 1151
T = 226.75
(out)(err)
S = OPT
O = 1151
T = 252.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 = 1152
T = 1797.77
(out)(err)
S = OPT
O = 1151
T = 29.06
(out)(err)
S = N/A
O = 1313
T = TO
(out)(err)
S = N/A
O = 1463
T = TO
(out)(err)
S = N/A
O = 1455
T = TO
(out)(err)
S = N/A
O = 1217
T = TO
(out)(err)
S = N/A
O = 1427
T = TO
(out)(err)
S = N/A
O = N/A
T = 192.64
(out)(err)
S = N/A
O = N/A
T = 1521.17
(out)(err)
s2v100c1500_6.wcnf S = OPT
O = 1225
T = 35.16
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1225
T = 39.86
(out)(err)
S = N/A
O = 1520
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1225
T = 141.34
(out)(err)
S = N/A
O = 1386
T = TO
(out)(err)
S = OPT
O = 1225
T = 425.67
(out)(err)
S = OPT
O = 1225
T = 447.34
(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 = 1255
T = 1797.75
(out)(err)
S = OPT
O = 1225
T = 35.16
(out)(err)
S = N/A
O = 1380
T = TO
(out)(err)
S = N/A
O = 1606
T = TO
(out)(err)
S = N/A
O = 1687
T = TO
(out)(err)
S = N/A
O = 1297
T = TO
(out)(err)
S = N/A
O = 1703
T = TO
(out)(err)
S = N/A
O = N/A
T = 317.78
(out)(err)
S = N/A
O = N/A
T = 1638.21
(out)(err)
s2v100c1500_7.wcnf S = OPT
O = 1186
T = 14.28
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1186
T = 14.28
(out)(err)
S = N/A
O = 1569
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1186
T = 56.11
(out)(err)
S = N/A
O = 1319
T = TO
(out)(err)
S = OPT
O = 1186
T = 157.51
(out)(err)
S = OPT
O = 1186
T = 159.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 = 1186
T = 1797.89
(out)(err)
S = OPT
O = 1186
T = 21.00
(out)(err)
S = N/A
O = 1319
T = TO
(out)(err)
S = N/A
O = 1649
T = TO
(out)(err)
S = N/A
O = 1585
T = TO
(out)(err)
S = N/A
O = 1210
T = TO
(out)(err)
S = N/A
O = 1676
T = TO
(out)(err)
S = N/A
O = N/A
T = 206.92
(out)(err)
S = N/A
O = N/A
T = 1025.16
(out)(err)
s2v100c1500_8.wcnf S = OPT
O = 1217
T = 35.16
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1217
T = 40.51
(out)(err)
S = N/A
O = 1589
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1217
T = 232.62
(out)(err)
S = N/A
O = 1316
T = TO
(out)(err)
S = OPT
O = 1217
T = 701.81
(out)(err)
S = OPT
O = 1217
T = 696.34
(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 = 1253
T = 1796.94
(out)(err)
S = OPT
O = 1217
T = 35.16
(out)(err)
S = N/A
O = 1365
T = TO
(out)(err)
S = N/A
O = 1587
T = TO
(out)(err)
S = N/A
O = 1737
T = TO
(out)(err)
S = N/A
O = 1291
T = TO
(out)(err)
S = N/A
O = 1580
T = TO
(out)(err)
S = N/A
O = N/A
T = 317.83
(out)(err)
S = N/A
O = N/A
T = 920.48
(out)(err)
s2v100c1600_1.wcnf S = OPT
O = 1230
T = 12.79
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1230
T = 13.92
(out)(err)
S = N/A
O = 1735
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1230
T = 51.85
(out)(err)
S = N/A
O = 1378
T = TO
(out)(err)
S = OPT
O = 1230
T = 164.09
(out)(err)
S = OPT
O = 1230
T = 158.03
(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 = 1230
T = 1797.85
(out)(err)
S = OPT
O = 1230
T = 12.79
(out)(err)
S = N/A
O = 1355
T = TO
(out)(err)
S = N/A
O = 1688
T = TO
(out)(err)
S = N/A
O = 1714
T = TO
(out)(err)
S = N/A
O = 1336
T = TO
(out)(err)
S = N/A
O = 1710
T = TO
(out)(err)
S = N/A
O = N/A
T = 318.21
(out)(err)
S = N/A
O = N/A
T = 593.79
(out)(err)
s2v100c1600_2.wcnf S = OPT
O = 1265
T = 112.60
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1265
T = 112.60
(out)(err)
S = N/A
O = 1501
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1265
T = 415.89
(out)(err)
S = N/A
O = 1408
T = TO
(out)(err)
S = OPT
O = 1265
T = 1232.74
(out)(err)
S = OPT
O = 1265
T = 1237.91
(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 = 1265
T = 1797.58
(out)(err)
S = OPT
O = 1265
T = 118.01
(out)(err)
S = N/A
O = 1394
T = TO
(out)(err)
S = N/A
O = 1710
T = TO
(out)(err)
S = N/A
O = 1652
T = TO
(out)(err)
S = N/A
O = 1358
T = TO
(out)(err)
S = N/A
O = 1709
T = TO
(out)(err)
S = N/A
O = N/A
T = 317.72
(out)(err)
S = N/A
O = N/A
T = 1309.51
(out)(err)
s2v100c1600_3.wcnf S = OPT
O = 1309
T = 75.65
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1309
T = 79.92
(out)(err)
S = N/A
O = 1647
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1309
T = 214.49
(out)(err)
S = N/A
O = 1393
T = TO
(out)(err)
S = OPT
O = 1309
T = 661.93
(out)(err)
S = OPT
O = 1309
T = 664.49
(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 = 1335
T = 1797.88
(out)(err)
S = OPT
O = 1309
T = 75.65
(out)(err)
S = N/A
O = 1457
T = TO
(out)(err)
S = N/A
O = 1718
T = TO
(out)(err)
S = N/A
O = 1706
T = TO
(out)(err)
S = N/A
O = 1354
T = TO
(out)(err)
S = N/A
O = 1861
T = TO
(out)(err)
S = N/A
O = N/A
T = 317.68
(out)(err)
S = N/A
O = N/A
T = 1514.29
(out)(err)
s2v100c1600_4.wcnf S = OPT
O = 1267
T = 35.90
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1267
T = 93.98
(out)(err)
S = N/A
O = 1560
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1267
T = 568.83
(out)(err)
S = N/A
O = 1418
T = TO
(out)(err)
S = OPT
O = 1267
T = 1776.04
(out)(err)
S = OPT
O = 1267
T = 1710.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 = 1311
T = 1797.86
(out)(err)
S = OPT
O = 1267
T = 35.90
(out)(err)
S = N/A
O = 1409
T = TO
(out)(err)
S = N/A
O = 1735
T = TO
(out)(err)
S = N/A
O = 1642
T = TO
(out)(err)
S = N/A
O = 1454
T = TO
(out)(err)
S = N/A
O = 1801
T = TO
(out)(err)
S = N/A
O = N/A
T = 317.46
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1600_5.wcnf S = OPT
O = 1298
T = 26.24
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1298
T = 26.24
(out)(err)
S = N/A
O = 1646
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1298
T = 92.72
(out)(err)
S = N/A
O = 1436
T = TO
(out)(err)
S = OPT
O = 1298
T = 291.79
(out)(err)
S = OPT
O = 1298
T = 280.44
(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 = 1305
T = 1797.92
(out)(err)
S = OPT
O = 1298
T = 37.44
(out)(err)
S = N/A
O = 1417
T = TO
(out)(err)
S = N/A
O = 1653
T = TO
(out)(err)
S = N/A
O = 1529
T = TO
(out)(err)
S = N/A
O = 1354
T = TO
(out)(err)
S = N/A
O = 1614
T = TO
(out)(err)
S = N/A
O = N/A
T = 317.91
(out)(err)
S = N/A
O = N/A
T = 884.58
(out)(err)
s2v100c1600_6.wcnf S = OPT
O = 1190
T = 12.10
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1190
T = 12.10
(out)(err)
S = N/A
O = 1434
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1190
T = 66.20
(out)(err)
S = N/A
O = 1328
T = TO
(out)(err)
S = OPT
O = 1190
T = 194.03
(out)(err)
S = OPT
O = 1190
T = 189.56
(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 = 1199
T = 1797.80
(out)(err)
S = OPT
O = 1190
T = 19.35
(out)(err)
S = N/A
O = 1312
T = TO
(out)(err)
S = N/A
O = 1578
T = TO
(out)(err)
S = N/A
O = 1630
T = TO
(out)(err)
S = N/A
O = 1227
T = TO
(out)(err)
S = N/A
O = 1815
T = TO
(out)(err)
S = N/A
O = N/A
T = 317.45
(out)(err)
S = N/A
O = N/A
T = 1147.41
(out)(err)
s2v100c1600_7.wcnf S = OPT
O = 1243
T = 69.06
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1243
T = 69.06
(out)(err)
S = N/A
O = 1581
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1243
T = 305.29
(out)(err)
S = N/A
O = 1397
T = TO
(out)(err)
S = OPT
O = 1243
T = 952.19
(out)(err)
S = OPT
O = 1243
T = 1037.51
(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 = 1256
T = 1797.84
(out)(err)
S = OPT
O = 1243
T = 71.06
(out)(err)
S = N/A
O = 1361
T = TO
(out)(err)
S = N/A
O = 1681
T = TO
(out)(err)
S = N/A
O = 1679
T = TO
(out)(err)
S = N/A
O = 1289
T = TO
(out)(err)
S = N/A
O = 1542
T = TO
(out)(err)
S = N/A
O = N/A
T = 317.87
(out)(err)
S = N/A
O = N/A
T = 1080.50
(out)(err)
s2v100c1600_8.wcnf S = OPT
O = 1184
T = 3.68
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1184
T = 6.27
(out)(err)
S = N/A
O = 1544
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1184
T = 18.69
(out)(err)
S = N/A
O = 1264
T = TO
(out)(err)
S = OPT
O = 1184
T = 53.04
(out)(err)
S = OPT
O = 1184
T = 54.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 = 1184
T = 1618.39
(out)(err)
S = OPT
O = 1184
T = 3.68
(out)(err)
S = N/A
O = 1330
T = TO
(out)(err)
S = N/A
O = 1500
T = TO
(out)(err)
S = N/A
O = 1765
T = TO
(out)(err)
S = N/A
O = 1235
T = TO
(out)(err)
S = N/A
O = 1837
T = TO
(out)(err)
S = N/A
O = N/A
T = 318.19
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1200_1.wcnf S = OPT
O = 840
T = 15.09
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 840
T = 30.08
(out)(err)
S = N/A
O = 1091
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 840
T = 50.45
(out)(err)
S = N/A
O = 954
T = TO
(out)(err)
S = OPT
O = 840
T = 137.03
(out)(err)
S = OPT
O = 840
T = 135.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 = 849
T = 1797.86
(out)(err)
S = OPT
O = 840
T = 15.09
(out)(err)
S = N/A
O = 891
T = TO
(out)(err)
S = N/A
O = 1066
T = TO
(out)(err)
S = N/A
O = 1113
T = TO
(out)(err)
S = N/A
O = 870
T = TO
(out)(err)
S = N/A
O = 1147
T = TO
(out)(err)
S = N/A
O = N/A
T = 212.79
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1200_2.wcnf S = OPT
O = 803
T = 3.26
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 803
T = 5.71
(out)(err)
S = N/A
O = 1073
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 803
T = 7.90
(out)(err)
S = N/A
O = 870
T = TO
(out)(err)
S = OPT
O = 803
T = 13.48
(out)(err)
S = OPT
O = 803
T = 13.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 = 803
T = 257.63
(out)(err)
S = OPT
O = 803
T = 3.26
(out)(err)
S = N/A
O = 864
T = TO
(out)(err)
S = N/A
O = 1067
T = TO
(out)(err)
S = N/A
O = 1105
T = TO
(out)(err)
S = N/A
O = 810
T = TO
(out)(err)
S = N/A
O = 1148
T = TO
(out)(err)
S = N/A
O = N/A
T = 207.04
(out)(err)
S = N/A
O = N/A
T = 1307.53
(out)(err)
s2v120c1200_3.wcnf S = OPT
O = 834
T = 9.08
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 834
T = 14.63
(out)(err)
S = N/A
O = 1109
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 834
T = 16.78
(out)(err)
S = N/A
O = 922
T = TO
(out)(err)
S = OPT
O = 834
T = 54.72
(out)(err)
S = OPT
O = 834
T = 55.45
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 834
T = 999.02
(out)(err)
S = OPT
O = 834
T = 9.08
(out)(err)
S = N/A
O = 914
T = TO
(out)(err)
S = N/A
O = 1128
T = TO
(out)(err)
S = N/A
O = 1085
T = TO
(out)(err)
S = N/A
O = 853
T = TO
(out)(err)
S = N/A
O = 1172
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.53
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1200_4.wcnf S = OPT
O = 811
T = 9.15
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 811
T = 10.40
(out)(err)
S = N/A
O = 1180
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 811
T = 9.15
(out)(err)
S = N/A
O = 890
T = TO
(out)(err)
S = OPT
O = 811
T = 27.48
(out)(err)
S = OPT
O = 811
T = 24.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 = 811
T = 467.28
(out)(err)
S = OPT
O = 811
T = 11.02
(out)(err)
S = N/A
O = 870
T = TO
(out)(err)
S = N/A
O = 1170
T = TO
(out)(err)
S = N/A
O = 1062
T = TO
(out)(err)
S = N/A
O = 813
T = TO
(out)(err)
S = N/A
O = 1254
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)
s2v120c1200_5.wcnf S = OPT
O = 850
T = 26.12
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 850
T = 28.15
(out)(err)
S = N/A
O = 1156
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 850
T = 43.42
(out)(err)
S = N/A
O = 962
T = TO
(out)(err)
S = OPT
O = 850
T = 294.51
(out)(err)
S = OPT
O = 850
T = 307.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 = 850
T = 1797.90
(out)(err)
S = OPT
O = 850
T = 26.12
(out)(err)
S = N/A
O = 921
T = TO
(out)(err)
S = N/A
O = 1062
T = TO
(out)(err)
S = N/A
O = 1098
T = TO
(out)(err)
S = N/A
O = 866
T = TO
(out)(err)
S = N/A
O = 1047
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.25
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1200_6.wcnf S = OPT
O = 784
T = 12.04
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 784
T = 34.19
(out)(err)
S = N/A
O = 1021
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 784
T = 40.86
(out)(err)
S = N/A
O = 919
T = TO
(out)(err)
S = OPT
O = 784
T = 166.34
(out)(err)
S = OPT
O = 784
T = 172.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 = 784
T = 999.63
(out)(err)
S = OPT
O = 784
T = 12.04
(out)(err)
S = N/A
O = 845
T = TO
(out)(err)
S = N/A
O = 1116
T = TO
(out)(err)
S = N/A
O = 1057
T = TO
(out)(err)
S = N/A
O = 789
T = TO
(out)(err)
S = N/A
O = 1106
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.76
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1200_7.wcnf S = OPT
O = 747
T = 1.59
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 747
T = 3.11
(out)(err)
S = N/A
O = 1036
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 747
T = 3.36
(out)(err)
S = N/A
O = 784
T = TO
(out)(err)
S = OPT
O = 747
T = 8.57
(out)(err)
S = OPT
O = 747
T = 8.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 = 747
T = 86.08
(out)(err)
S = OPT
O = 747
T = 1.59
(out)(err)
S = N/A
O = 827
T = TO
(out)(err)
S = N/A
O = 916
T = TO
(out)(err)
S = N/A
O = 972
T = TO
(out)(err)
S = N/A
O = 758
T = TO
(out)(err)
S = N/A
O = 1070
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.61
(out)(err)
S = N/A
O = N/A
T = 1703.61
(out)(err)
s2v120c1200_8.wcnf S = OPT
O = 813
T = 6.90
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 813
T = 6.90
(out)(err)
S = N/A
O = 1169
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 813
T = 10.38
(out)(err)
S = N/A
O = 928
T = TO
(out)(err)
S = OPT
O = 813
T = 30.54
(out)(err)
S = OPT
O = 813
T = 29.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 = 813
T = 512.77
(out)(err)
S = OPT
O = 813
T = 7.31
(out)(err)
S = N/A
O = 890
T = TO
(out)(err)
S = N/A
O = 1026
T = TO
(out)(err)
S = N/A
O = 1074
T = TO
(out)(err)
S = N/A
O = 826
T = TO
(out)(err)
S = N/A
O = 1279
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.77
(out)(err)
S = N/A
O = N/A
T = 1670.59
(out)(err)
s2v120c1300_1.wcnf S = OPT
O = 890
T = 6.07
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 890
T = 6.53
(out)(err)
S = N/A
O = 1126
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 890
T = 9.46
(out)(err)
S = N/A
O = 989
T = TO
(out)(err)
S = OPT
O = 890
T = 30.38
(out)(err)
S = OPT
O = 890
T = 29.56
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 890
T = 546.74
(out)(err)
S = OPT
O = 890
T = 6.07
(out)(err)
S = N/A
O = 966
T = TO
(out)(err)
S = N/A
O = 1228
T = TO
(out)(err)
S = N/A
O = 1114
T = TO
(out)(err)
S = N/A
O = 897
T = TO
(out)(err)
S = N/A
O = 1138
T = TO
(out)(err)
S = N/A
O = N/A
T = 307.00
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1300_2.wcnf S = OPT
O = 847
T = 2.88
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 847
T = 5.64
(out)(err)
S = N/A
O = 1109
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 847
T = 10.79
(out)(err)
S = N/A
O = 987
T = TO
(out)(err)
S = OPT
O = 847
T = 26.41
(out)(err)
S = OPT
O = 847
T = 21.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 = 847
T = 357.49
(out)(err)
S = OPT
O = 847
T = 2.88
(out)(err)
S = N/A
O = 912
T = TO
(out)(err)
S = N/A
O = 1126
T = TO
(out)(err)
S = N/A
O = 1049
T = TO
(out)(err)
S = N/A
O = 865
T = TO
(out)(err)
S = N/A
O = 1267
T = TO
(out)(err)
S = N/A
O = N/A
T = 248.96
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1300_3.wcnf S = OPT
O = 941
T = 7.84
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 941
T = 16.29
(out)(err)
S = N/A
O = 1239
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 941
T = 34.80
(out)(err)
S = N/A
O = 1044
T = TO
(out)(err)
S = OPT
O = 941
T = 69.50
(out)(err)
S = OPT
O = 941
T = 67.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 = 941
T = 1771.52
(out)(err)
S = OPT
O = 941
T = 7.84
(out)(err)
S = N/A
O = 1025
T = TO
(out)(err)
S = N/A
O = 1183
T = TO
(out)(err)
S = N/A
O = 1269
T = TO
(out)(err)
S = N/A
O = 960
T = TO
(out)(err)
S = N/A
O = 1358
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.90
(out)(err)
S = N/A
O = N/A
T = 1490.84
(out)(err)
s2v120c1300_4.wcnf S = OPT
O = 939
T = 11.13
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 939
T = 16.04
(out)(err)
S = N/A
O = 1251
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 939
T = 33.99
(out)(err)
S = N/A
O = 1041
T = TO
(out)(err)
S = OPT
O = 939
T = 113.06
(out)(err)
S = OPT
O = 939
T = 99.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 = 939
T = 1303.46
(out)(err)
S = OPT
O = 939
T = 11.13
(out)(err)
S = N/A
O = 1043
T = TO
(out)(err)
S = N/A
O = 1216
T = TO
(out)(err)
S = N/A
O = 1197
T = TO
(out)(err)
S = N/A
O = 978
T = TO
(out)(err)
S = N/A
O = 1313
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.91
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1300_5.wcnf S = OPT
O = 949
T = 24.66
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 949
T = 59.56
(out)(err)
S = N/A
O = 1433
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 949
T = 102.68
(out)(err)
S = N/A
O = 1051
T = TO
(out)(err)
S = OPT
O = 949
T = 288.49
(out)(err)
S = OPT
O = 949
T = 281.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 = 1000
T = 1797.85
(out)(err)
S = OPT
O = 949
T = 24.66
(out)(err)
S = N/A
O = 1027
T = TO
(out)(err)
S = N/A
O = 1214
T = TO
(out)(err)
S = N/A
O = 1277
T = TO
(out)(err)
S = N/A
O = 977
T = TO
(out)(err)
S = N/A
O = 1382
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.90
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1300_6.wcnf S = OPT
O = 865
T = 4.45
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 865
T = 10.18
(out)(err)
S = N/A
O = 1235
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 865
T = 13.59
(out)(err)
S = N/A
O = 898
T = TO
(out)(err)
S = OPT
O = 865
T = 43.85
(out)(err)
S = OPT
O = 865
T = 38.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 = 865
T = 939.96
(out)(err)
S = OPT
O = 865
T = 4.45
(out)(err)
S = N/A
O = 956
T = TO
(out)(err)
S = N/A
O = 1135
T = TO
(out)(err)
S = N/A
O = 1204
T = TO
(out)(err)
S = N/A
O = 868
T = TO
(out)(err)
S = N/A
O = 1182
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.76
(out)(err)
S = N/A
O = N/A
T = 1275.11
(out)(err)
s2v120c1300_7.wcnf S = OPT
O = 879
T = 3.50
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 879
T = 6.08
(out)(err)
S = N/A
O = 1101
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 879
T = 10.49
(out)(err)
S = N/A
O = 992
T = TO
(out)(err)
S = OPT
O = 879
T = 22.98
(out)(err)
S = OPT
O = 879
T = 23.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 = 879
T = 919.25
(out)(err)
S = OPT
O = 879
T = 3.50
(out)(err)
S = N/A
O = 970
T = TO
(out)(err)
S = N/A
O = 1167
T = TO
(out)(err)
S = N/A
O = 1264
T = TO
(out)(err)
S = N/A
O = 901
T = TO
(out)(err)
S = N/A
O = 1369
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.74
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1300_8.wcnf S = OPT
O = 868
T = 7.28
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 868
T = 8.08
(out)(err)
S = N/A
O = 1220
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 868
T = 12.13
(out)(err)
S = N/A
O = 919
T = TO
(out)(err)
S = OPT
O = 868
T = 32.62
(out)(err)
S = OPT
O = 868
T = 33.62
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 868
T = 566.95
(out)(err)
S = OPT
O = 868
T = 7.28
(out)(err)
S = N/A
O = 935
T = TO
(out)(err)
S = N/A
O = 1142
T = TO
(out)(err)
S = N/A
O = 1119
T = TO
(out)(err)
S = N/A
O = 877
T = TO
(out)(err)
S = N/A
O = 1265
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.82
(out)(err)
S = N/A
O = N/A
T = 1228.14
(out)(err)
s2v120c1400_1.wcnf S = OPT
O = 1028
T = 16.58
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1028
T = 18.74
(out)(err)
S = N/A
O = 1308
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1028
T = 29.99
(out)(err)
S = N/A
O = 1199
T = TO
(out)(err)
S = OPT
O = 1028
T = 70.53
(out)(err)
S = OPT
O = 1028
T = 71.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 = 1028
T = 1401.03
(out)(err)
S = OPT
O = 1028
T = 16.58
(out)(err)
S = N/A
O = 1095
T = TO
(out)(err)
S = N/A
O = 1327
T = TO
(out)(err)
S = N/A
O = 1352
T = TO
(out)(err)
S = N/A
O = 1040
T = TO
(out)(err)
S = N/A
O = 1372
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.00
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1400_2.wcnf S = OPT
O = 1008
T = 21.78
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1008
T = 64.87
(out)(err)
S = N/A
O = 1464
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1008
T = 99.92
(out)(err)
S = N/A
O = 1079
T = TO
(out)(err)
S = OPT
O = 1008
T = 376.17
(out)(err)
S = OPT
O = 1008
T = 361.95
(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 = 1038
T = 1797.89
(out)(err)
S = OPT
O = 1008
T = 21.78
(out)(err)
S = N/A
O = 1121
T = TO
(out)(err)
S = N/A
O = 1351
T = TO
(out)(err)
S = N/A
O = 1326
T = TO
(out)(err)
S = N/A
O = 1067
T = TO
(out)(err)
S = N/A
O = 1482
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.55
(out)(err)
S = N/A
O = N/A
T = 1554.11
(out)(err)
s2v120c1400_3.wcnf S = OPT
O = 983
T = 3.79
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 983
T = 10.13
(out)(err)
S = N/A
O = 1375
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 983
T = 8.06
(out)(err)
S = N/A
O = 1009
T = TO
(out)(err)
S = OPT
O = 983
T = 26.91
(out)(err)
S = OPT
O = 983
T = 25.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 = 983
T = 447.91
(out)(err)
S = OPT
O = 983
T = 3.79
(out)(err)
S = N/A
O = 1119
T = TO
(out)(err)
S = N/A
O = 1324
T = TO
(out)(err)
S = N/A
O = 1348
T = TO
(out)(err)
S = N/A
O = 1064
T = TO
(out)(err)
S = N/A
O = 1525
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.96
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1400_4.wcnf S = OPT
O = 1007
T = 32.28
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1007
T = 32.28
(out)(err)
S = N/A
O = 1361
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1007
T = 69.78
(out)(err)
S = N/A
O = 1082
T = TO
(out)(err)
S = OPT
O = 1007
T = 184.92
(out)(err)
S = OPT
O = 1007
T = 189.69
(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 = 1007
T = 1797.80
(out)(err)
S = OPT
O = 1007
T = 33.71
(out)(err)
S = N/A
O = 1103
T = TO
(out)(err)
S = N/A
O = 1259
T = TO
(out)(err)
S = N/A
O = 1260
T = TO
(out)(err)
S = N/A
O = 1049
T = TO
(out)(err)
S = N/A
O = 1341
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.81
(out)(err)
S = N/A
O = N/A
T = 1059.36
(out)(err)
s2v120c1400_5.wcnf S = OPT
O = 1108
T = 156.89
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1108
T = 156.89
(out)(err)
S = N/A
O = 1425
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1108
T = 469.74
(out)(err)
S = N/A
O = 1212
T = TO
(out)(err)
S = OPT
O = 1108
T = 1400.61
(out)(err)
S = OPT
O = 1108
T = 1370.65
(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 = 1108
T = 1797.87
(out)(err)
S = OPT
O = 1108
T = 290.16
(out)(err)
S = N/A
O = 1181
T = TO
(out)(err)
S = N/A
O = 1451
T = TO
(out)(err)
S = N/A
O = 1440
T = TO
(out)(err)
S = N/A
O = 1215
T = TO
(out)(err)
S = N/A
O = 1475
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.13
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1400_6.wcnf S = OPT
O = 959
T = 7.10
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 959
T = 7.10
(out)(err)
S = N/A
O = 1267
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 959
T = 14.01
(out)(err)
S = N/A
O = 1050
T = TO
(out)(err)
S = OPT
O = 959
T = 32.75
(out)(err)
S = OPT
O = 959
T = 32.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 = 959
T = 686.10
(out)(err)
S = OPT
O = 959
T = 8.30
(out)(err)
S = N/A
O = 1047
T = TO
(out)(err)
S = N/A
O = 1213
T = TO
(out)(err)
S = N/A
O = 1228
T = TO
(out)(err)
S = N/A
O = 968
T = TO
(out)(err)
S = N/A
O = 1457
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.75
(out)(err)
S = N/A
O = N/A
T = 641.49
(out)(err)
s2v120c1400_7.wcnf S = OPT
O = 1040
T = 38.14
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1040
T = 56.64
(out)(err)
S = N/A
O = 1317
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1040
T = 133.14
(out)(err)
S = N/A
O = 1076
T = TO
(out)(err)
S = OPT
O = 1040
T = 371.43
(out)(err)
S = OPT
O = 1040
T = 387.67
(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 = 1062
T = 1797.88
(out)(err)
S = OPT
O = 1040
T = 38.14
(out)(err)
S = N/A
O = 1142
T = TO
(out)(err)
S = N/A
O = 1373
T = TO
(out)(err)
S = N/A
O = 1304
T = TO
(out)(err)
S = N/A
O = 1063
T = TO
(out)(err)
S = N/A
O = 1387
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.53
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1400_8.wcnf S = OPT
O = 1025
T = 26.88
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1025
T = 26.88
(out)(err)
S = N/A
O = 1529
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1025
T = 79.77
(out)(err)
S = N/A
O = 1090
T = TO
(out)(err)
S = OPT
O = 1025
T = 188.94
(out)(err)
S = OPT
O = 1025
T = 183.91
(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 = 1035
T = 1797.84
(out)(err)
S = OPT
O = 1025
T = 32.92
(out)(err)
S = N/A
O = 1114
T = TO
(out)(err)
S = N/A
O = 1318
T = TO
(out)(err)
S = N/A
O = 1323
T = TO
(out)(err)
S = N/A
O = 1050
T = TO
(out)(err)
S = N/A
O = 1453
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.92
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1500_1.wcnf S = OPT
O = 1119
T = 24.90
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1119
T = 90.17
(out)(err)
S = N/A
O = 1535
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1119
T = 74.25
(out)(err)
S = N/A
O = 1279
T = TO
(out)(err)
S = OPT
O = 1119
T = 200.13
(out)(err)
S = OPT
O = 1119
T = 195.41
(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 = 1136
T = 1797.85
(out)(err)
S = OPT
O = 1119
T = 24.90
(out)(err)
S = N/A
O = 1254
T = TO
(out)(err)
S = N/A
O = 1388
T = TO
(out)(err)
S = N/A
O = 1505
T = TO
(out)(err)
S = N/A
O = 1161
T = TO
(out)(err)
S = N/A
O = 1668
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.87
(out)(err)
S = N/A
O = N/A
T = 1492.41
(out)(err)
s2v120c1500_2.wcnf S = OPT
O = 1136
T = 34.16
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1136
T = 98.26
(out)(err)
S = N/A
O = 1564
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1136
T = 81.20
(out)(err)
S = N/A
O = 1208
T = TO
(out)(err)
S = OPT
O = 1136
T = 270.64
(out)(err)
S = OPT
O = 1136
T = 282.49
(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 = 1190
T = 1797.83
(out)(err)
S = OPT
O = 1136
T = 34.16
(out)(err)
S = N/A
O = 1298
T = TO
(out)(err)
S = N/A
O = 1459
T = TO
(out)(err)
S = N/A
O = 1483
T = TO
(out)(err)
S = N/A
O = 1203
T = TO
(out)(err)
S = N/A
O = 1663
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.77
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1500_3.wcnf S = OPT
O = 1062
T = 8.13
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1062
T = 13.81
(out)(err)
S = N/A
O = 1489
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1062
T = 13.11
(out)(err)
S = N/A
O = 1273
T = TO
(out)(err)
S = OPT
O = 1062
T = 38.70
(out)(err)
S = OPT
O = 1062
T = 38.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 = 1062
T = 1142.98
(out)(err)
S = OPT
O = 1062
T = 8.13
(out)(err)
S = N/A
O = 1196
T = TO
(out)(err)
S = N/A
O = 1400
T = TO
(out)(err)
S = N/A
O = 1365
T = TO
(out)(err)
S = N/A
O = 1099
T = TO
(out)(err)
S = N/A
O = 1570
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.90
(out)(err)
S = N/A
O = N/A
T = 1504.61
(out)(err)
s2v120c1500_4.wcnf S = OPT
O = 1041
T = 4.93
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1041
T = 5.57
(out)(err)
S = N/A
O = 1428
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1041
T = 12.52
(out)(err)
S = N/A
O = 1173
T = TO
(out)(err)
S = OPT
O = 1041
T = 27.59
(out)(err)
S = OPT
O = 1041
T = 31.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 = 1041
T = 1094.73
(out)(err)
S = OPT
O = 1041
T = 4.93
(out)(err)
S = N/A
O = 1162
T = TO
(out)(err)
S = N/A
O = 1362
T = TO
(out)(err)
S = N/A
O = 1447
T = TO
(out)(err)
S = N/A
O = 1062
T = TO
(out)(err)
S = N/A
O = 1496
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.90
(out)(err)
S = N/A
O = N/A
T = 703.58
(out)(err)
s2v120c1500_5.wcnf S = OPT
O = 1125
T = 5.85
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1125
T = 15.62
(out)(err)
S = N/A
O = 1634
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1125
T = 37.28
(out)(err)
S = N/A
O = 1323
T = TO
(out)(err)
S = OPT
O = 1125
T = 76.09
(out)(err)
S = OPT
O = 1125
T = 76.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 = 1125
T = 1564.55
(out)(err)
S = OPT
O = 1125
T = 5.85
(out)(err)
S = N/A
O = 1222
T = TO
(out)(err)
S = N/A
O = 1468
T = TO
(out)(err)
S = N/A
O = 1600
T = TO
(out)(err)
S = N/A
O = 1242
T = TO
(out)(err)
S = N/A
O = 1746
T = TO
(out)(err)
S = N/A
O = N/A
T = 188.86
(out)(err)
S = N/A
O = N/A
T = 1207.88
(out)(err)
s2v120c1500_6.wcnf S = OPT
O = 1113
T = 25.33
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1113
T = 38.99
(out)(err)
S = N/A
O = 1500
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1113
T = 82.89
(out)(err)
S = N/A
O = 1308
T = TO
(out)(err)
S = OPT
O = 1113
T = 157.97
(out)(err)
S = OPT
O = 1113
T = 242.75
(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 = 1113
T = 1797.63
(out)(err)
S = OPT
O = 1113
T = 25.33
(out)(err)
S = N/A
O = 1220
T = TO
(out)(err)
S = N/A
O = 1471
T = TO
(out)(err)
S = N/A
O = 1504
T = TO
(out)(err)
S = N/A
O = 1175
T = TO
(out)(err)
S = N/A
O = 1536
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.20
(out)(err)
S = N/A
O = N/A
T = 1008.42
(out)(err)
s2v120c1500_7.wcnf S = OPT
O = 1163
T = 76.60
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1163
T = 76.60
(out)(err)
S = N/A
O = 1495
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1163
T = 266.44
(out)(err)
S = N/A
O = 1209
T = TO
(out)(err)
S = OPT
O = 1163
T = 526.48
(out)(err)
S = OPT
O = 1163
T = 561.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 = 1177
T = 1797.86
(out)(err)
S = OPT
O = 1163
T = 77.55
(out)(err)
S = N/A
O = 1279
T = TO
(out)(err)
S = N/A
O = 1444
T = TO
(out)(err)
S = N/A
O = 1451
T = TO
(out)(err)
S = N/A
O = 1231
T = TO
(out)(err)
S = N/A
O = 1538
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.07
(out)(err)
S = N/A
O = N/A
T = 864.94
(out)(err)
s2v120c1500_8.wcnf S = OPT
O = 1097
T = 4.67
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1097
T = 10.02
(out)(err)
S = N/A
O = 1711
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1097
T = 16.75
(out)(err)
S = N/A
O = 1208
T = TO
(out)(err)
S = OPT
O = 1097
T = 73.72
(out)(err)
S = OPT
O = 1097
T = 69.96
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1097
T = 856.45
(out)(err)
S = OPT
O = 1097
T = 4.67
(out)(err)
S = N/A
O = 1225
T = TO
(out)(err)
S = N/A
O = 1451
T = TO
(out)(err)
S = N/A
O = 1505
T = TO
(out)(err)
S = N/A
O = 1143
T = TO
(out)(err)
S = N/A
O = 1550
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.86
(out)(err)
S = N/A
O = N/A
T = 1007.89
(out)(err)
s2v120c1600_1.wcnf S = OPT
O = 1190
T = 8.51
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1190
T = 8.51
(out)(err)
S = N/A
O = 1732
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1190
T = 29.55
(out)(err)
S = N/A
O = 1328
T = TO
(out)(err)
S = OPT
O = 1190
T = 98.25
(out)(err)
S = OPT
O = 1190
T = 101.23
(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 = 1190
T = 1797.93
(out)(err)
S = OPT
O = 1190
T = 9.75
(out)(err)
S = N/A
O = 1332
T = TO
(out)(err)
S = N/A
O = 1458
T = TO
(out)(err)
S = N/A
O = 1595
T = TO
(out)(err)
S = N/A
O = 1266
T = TO
(out)(err)
S = N/A
O = 1807
T = TO
(out)(err)
S = N/A
O = N/A
T = 317.84
(out)(err)
S = N/A
O = N/A
T = 907.96
(out)(err)
s2v120c1600_2.wcnf S = OPT
O = 1227
T = 55.97
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1227
T = 74.18
(out)(err)
S = N/A
O = 1639
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1227
T = 191.93
(out)(err)
S = N/A
O = 1443
T = TO
(out)(err)
S = OPT
O = 1227
T = 546.13
(out)(err)
S = OPT
O = 1227
T = 566.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 = 1227
T = 1797.86
(out)(err)
S = OPT
O = 1227
T = 55.97
(out)(err)
S = N/A
O = 1332
T = TO
(out)(err)
S = N/A
O = 1588
T = TO
(out)(err)
S = N/A
O = 1630
T = TO
(out)(err)
S = N/A
O = 1288
T = TO
(out)(err)
S = N/A
O = 1720
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.91
(out)(err)
S = N/A
O = N/A
T = 1039.08
(out)(err)
s2v120c1600_3.wcnf S = OPT
O = 1224
T = 57.08
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1224
T = 57.08
(out)(err)
S = N/A
O = 1509
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1224
T = 197.80
(out)(err)
S = N/A
O = 1286
T = TO
(out)(err)
S = OPT
O = 1224
T = 594.28
(out)(err)
S = OPT
O = 1224
T = 603.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 = 1274
T = 1797.81
(out)(err)
S = OPT
O = 1224
T = 59.25
(out)(err)
S = N/A
O = 1372
T = TO
(out)(err)
S = N/A
O = 1585
T = TO
(out)(err)
S = N/A
O = 1615
T = TO
(out)(err)
S = N/A
O = 1348
T = TO
(out)(err)
S = N/A
O = 1742
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.96
(out)(err)
S = N/A
O = N/A
T = 571.16
(out)(err)
s2v120c1600_4.wcnf S = OPT
O = 1264
T = 150.53
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1264
T = 150.53
(out)(err)
S = N/A
O = 1544
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1264
T = 361.56
(out)(err)
S = N/A
O = 1349
T = TO
(out)(err)
S = OPT
O = 1264
T = 1130.62
(out)(err)
S = OPT
O = 1264
T = 1124.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 = 1299
T = 1797.77
(out)(err)
S = OPT
O = 1264
T = 153.72
(out)(err)
S = N/A
O = 1398
T = TO
(out)(err)
S = N/A
O = 1633
T = TO
(out)(err)
S = N/A
O = 1786
T = TO
(out)(err)
S = N/A
O = 1331
T = TO
(out)(err)
S = N/A
O = 1689
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.05
(out)(err)
S = N/A
O = N/A
T = 1755.95
(out)(err)
s2v120c1600_5.wcnf S = OPT
O = 1252
T = 57.67
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1252
T = 66.28
(out)(err)
S = N/A
O = 1498
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1252
T = 200.19
(out)(err)
S = N/A
O = 1335
T = TO
(out)(err)
S = OPT
O = 1252
T = 716.75
(out)(err)
S = OPT
O = 1252
T = 731.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 = 1295
T = 1797.87
(out)(err)
S = OPT
O = 1252
T = 57.67
(out)(err)
S = N/A
O = 1367
T = TO
(out)(err)
S = N/A
O = 1581
T = TO
(out)(err)
S = N/A
O = 1715
T = TO
(out)(err)
S = N/A
O = 1297
T = TO
(out)(err)
S = N/A
O = 1586
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.78
(out)(err)
S = N/A
O = N/A
T = 808.28
(out)(err)
s2v120c1600_6.wcnf S = OPT
O = 1246
T = 25.48
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1246
T = 26.73
(out)(err)
S = N/A
O = 1711
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1246
T = 70.44
(out)(err)
S = N/A
O = 1358
T = TO
(out)(err)
S = OPT
O = 1246
T = 354.44
(out)(err)
S = OPT
O = 1246
T = 368.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 = 1262
T = 1797.85
(out)(err)
S = OPT
O = 1246
T = 25.48
(out)(err)
S = N/A
O = 1390
T = TO
(out)(err)
S = N/A
O = 1560
T = TO
(out)(err)
S = N/A
O = 1665
T = TO
(out)(err)
S = N/A
O = 1308
T = TO
(out)(err)
S = N/A
O = 1704
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.94
(out)(err)
S = N/A
O = N/A
T = 1482.52
(out)(err)
s2v120c1600_7.wcnf S = OPT
O = 1159
T = 7.69
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1159
T = 7.69
(out)(err)
S = N/A
O = 1624
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1159
T = 15.38
(out)(err)
S = N/A
O = 1248
T = TO
(out)(err)
S = OPT
O = 1159
T = 47.40
(out)(err)
S = OPT
O = 1159
T = 46.56
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1159
T = 1056.69
(out)(err)
S = OPT
O = 1159
T = 8.18
(out)(err)
S = N/A
O = 1307
T = TO
(out)(err)
S = N/A
O = 1402
T = TO
(out)(err)
S = N/A
O = 1511
T = TO
(out)(err)
S = N/A
O = 1167
T = TO
(out)(err)
S = N/A
O = 1636
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.91
(out)(err)
S = N/A
O = N/A
T = 801.72
(out)(err)
s2v120c1600_8.wcnf S = OPT
O = 1150
T = 3.57
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1150
T = 12.43
(out)(err)
S = N/A
O = 1399
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1150
T = 29.45
(out)(err)
S = N/A
O = 1344
T = TO
(out)(err)
S = OPT
O = 1150
T = 101.00
(out)(err)
S = OPT
O = 1150
T = 104.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 = 1150
T = 1797.83
(out)(err)
S = OPT
O = 1150
T = 3.57
(out)(err)
S = N/A
O = 1277
T = TO
(out)(err)
S = N/A
O = 1494
T = TO
(out)(err)
S = N/A
O = 1555
T = TO
(out)(err)
S = N/A
O = 1214
T = TO
(out)(err)
S = N/A
O = 1834
T = TO
(out)(err)
S = N/A
O = N/A
T = 182.26
(out)(err)
S = N/A
O = N/A
T = 1101.56
(out)(err)
s2v140c1200_1.wcnf S = OPT
O = 780
T = 33.12
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 780
T = 58.17
(out)(err)
S = N/A
O = 1067
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 780
T = 67.00
(out)(err)
S = N/A
O = 899
T = TO
(out)(err)
S = OPT
O = 780
T = 195.11
(out)(err)
S = OPT
O = 780
T = 207.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 = 789
T = 1797.81
(out)(err)
S = OPT
O = 780
T = 33.12
(out)(err)
S = N/A
O = 863
T = TO
(out)(err)
S = N/A
O = 1051
T = TO
(out)(err)
S = N/A
O = 1035
T = TO
(out)(err)
S = N/A
O = 799
T = TO
(out)(err)
S = N/A
O = 1006
T = TO
(out)(err)
S = N/A
O = N/A
T = 232.00
(out)(err)
S = N/A
O = N/A
T = 1255.43
(out)(err)
s2v140c1200_2.wcnf S = OPT
O = 733
T = 18.05
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 733
T = 20.87
(out)(err)
S = N/A
O = 957
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 733
T = 34.49
(out)(err)
S = N/A
O = 816
T = TO
(out)(err)
S = OPT
O = 733
T = 80.82
(out)(err)
S = OPT
O = 733
T = 84.78
(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 = 733
T = 1797.87
(out)(err)
S = OPT
O = 733
T = 18.05
(out)(err)
S = N/A
O = 821
T = TO
(out)(err)
S = N/A
O = 966
T = TO
(out)(err)
S = N/A
O = 1004
T = TO
(out)(err)
S = N/A
O = 739
T = TO
(out)(err)
S = N/A
O = 1061
T = TO
(out)(err)
S = N/A
O = N/A
T = 204.98
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1200_3.wcnf S = OPT
O = 741
T = 13.12
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 741
T = 45.28
(out)(err)
S = N/A
O = 940
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 741
T = 50.67
(out)(err)
S = N/A
O = 854
T = TO
(out)(err)
S = OPT
O = 741
T = 142.58
(out)(err)
S = OPT
O = 741
T = 141.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 = 758
T = 1797.84
(out)(err)
S = OPT
O = 741
T = 13.12
(out)(err)
S = N/A
O = 796
T = TO
(out)(err)
S = N/A
O = 951
T = TO
(out)(err)
S = N/A
O = 1018
T = TO
(out)(err)
S = N/A
O = 758
T = TO
(out)(err)
S = N/A
O = 1044
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.88
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1200_4.wcnf S = OPT
O = 667
T = 1.52
S = OPT
O = 667
T = 1480.46
(out)(err)
S = OPT
O = 667
T = 2.62
(out)(err)
S = N/A
O = 948
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 667
T = 4.12
(out)(err)
S = N/A
O = 769
T = TO
(out)(err)
S = OPT
O = 667
T = 10.79
(out)(err)
S = OPT
O = 667
T = 10.01
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 667
T = 127.96
(out)(err)
S = OPT
O = 667
T = 1.52
(out)(err)
S = N/A
O = 746
T = TO
(out)(err)
S = N/A
O = 952
T = TO
(out)(err)
S = N/A
O = 933
T = TO
(out)(err)
S = N/A
O = 671
T = TO
(out)(err)
S = N/A
O = 1093
T = TO
(out)(err)
S = N/A
O = N/A
T = 234.77
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1200_5.wcnf S = OPT
O = 714
T = 4.90
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 714
T = 12.18
(out)(err)
S = N/A
O = 932
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 714
T = 13.77
(out)(err)
S = N/A
O = 757
T = TO
(out)(err)
S = OPT
O = 714
T = 42.91
(out)(err)
S = OPT
O = 714
T = 31.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 = 714
T = 490.77
(out)(err)
S = OPT
O = 714
T = 4.90
(out)(err)
S = N/A
O = 804
T = TO
(out)(err)
S = N/A
O = 1023
T = TO
(out)(err)
S = N/A
O = 969
T = TO
(out)(err)
S = N/A
O = 721
T = TO
(out)(err)
S = N/A
O = 997
T = TO
(out)(err)
S = N/A
O = N/A
T = 236.20
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1200_6.wcnf S = OPT
O = 803
T = 52.18
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 803
T = 69.73
(out)(err)
S = N/A
O = 1202
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 803
T = 111.13
(out)(err)
S = N/A
O = 909
T = TO
(out)(err)
S = OPT
O = 803
T = 310.87
(out)(err)
S = OPT
O = 803
T = 315.45
(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 = 803
T = 1797.79
(out)(err)
S = OPT
O = 803
T = 52.18
(out)(err)
S = N/A
O = 899
T = TO
(out)(err)
S = N/A
O = 1084
T = TO
(out)(err)
S = N/A
O = 1096
T = TO
(out)(err)
S = N/A
O = 811
T = TO
(out)(err)
S = N/A
O = 1460
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.88
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1200_7.wcnf S = OPT
O = 774
T = 64.09
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 774
T = 112.17
(out)(err)
S = N/A
O = 962
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 774
T = 128.19
(out)(err)
S = N/A
O = 800
T = TO
(out)(err)
S = OPT
O = 774
T = 305.12
(out)(err)
S = OPT
O = 774
T = 312.37
(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 = 778
T = 1797.82
(out)(err)
S = OPT
O = 774
T = 64.09
(out)(err)
S = N/A
O = 839
T = TO
(out)(err)
S = N/A
O = 1006
T = TO
(out)(err)
S = N/A
O = 1051
T = TO
(out)(err)
S = N/A
O = 792
T = TO
(out)(err)
S = N/A
O = 1001
T = TO
(out)(err)
S = N/A
O = N/A
T = 204.73
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1200_8.wcnf S = OPT
O = 745
T = 28.35
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 745
T = 57.12
(out)(err)
S = N/A
O = 984
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 745
T = 89.17
(out)(err)
S = N/A
O = 793
T = TO
(out)(err)
S = OPT
O = 745
T = 152.47
(out)(err)
S = OPT
O = 745
T = 152.26
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 745
T = 1698.22
(out)(err)
S = OPT
O = 745
T = 28.35
(out)(err)
S = N/A
O = 810
T = TO
(out)(err)
S = N/A
O = 1017
T = TO
(out)(err)
S = N/A
O = 994
T = TO
(out)(err)
S = N/A
O = 754
T = TO
(out)(err)
S = N/A
O = 1057
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.96
(out)(err)
S = N/A
O = N/A
T = 1285.43
(out)(err)
s2v140c1300_1.wcnf S = OPT
O = 846
T = 20.05
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 846
T = 33.03
(out)(err)
S = N/A
O = 1142
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 846
T = 61.85
(out)(err)
S = N/A
O = 980
T = TO
(out)(err)
S = OPT
O = 846
T = 130.95
(out)(err)
S = OPT
O = 846
T = 128.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 = 846
T = 1797.80
(out)(err)
S = OPT
O = 846
T = 20.05
(out)(err)
S = N/A
O = 917
T = TO
(out)(err)
S = N/A
O = 1179
T = TO
(out)(err)
S = N/A
O = 1379
T = TO
(out)(err)
S = N/A
O = 869
T = TO
(out)(err)
S = N/A
O = 1163
T = TO
(out)(err)
S = N/A
O = N/A
T = 204.81
(out)(err)
S = N/A
O = N/A
T = 1219.62
(out)(err)
s2v140c1300_2.wcnf S = OPT
O = 774
T = 2.91
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 774
T = 4.67
(out)(err)
S = N/A
O = 1046
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 774
T = 5.35
(out)(err)
S = N/A
O = 819
T = TO
(out)(err)
S = OPT
O = 774
T = 17.88
(out)(err)
S = OPT
O = 774
T = 19.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 = 774
T = 483.01
(out)(err)
S = OPT
O = 774
T = 2.91
(out)(err)
S = N/A
O = 855
T = TO
(out)(err)
S = N/A
O = 986
T = TO
(out)(err)
S = N/A
O = 1043
T = TO
(out)(err)
S = N/A
O = 792
T = TO
(out)(err)
S = N/A
O = 1234
T = TO
(out)(err)
S = N/A
O = N/A
T = 357.68
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1300_3.wcnf S = OPT
O = 832
T = 17.15
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 832
T = 30.26
(out)(err)
S = N/A
O = 1158
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 832
T = 81.29
(out)(err)
S = N/A
O = 959
T = TO
(out)(err)
S = OPT
O = 832
T = 210.44
(out)(err)
S = OPT
O = 832
T = 220.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 = 832
T = 1797.85
(out)(err)
S = OPT
O = 832
T = 17.15
(out)(err)
S = N/A
O = 921
T = TO
(out)(err)
S = N/A
O = 1139
T = TO
(out)(err)
S = N/A
O = 1108
T = TO
(out)(err)
S = N/A
O = 853
T = TO
(out)(err)
S = N/A
O = 1060
T = TO
(out)(err)
S = N/A
O = N/A
T = 212.81
(out)(err)
S = N/A
O = N/A
T = 1753.71
(out)(err)
s2v140c1300_4.wcnf S = OPT
O = 871
T = 80.00
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 871
T = 153.03
(out)(err)
S = N/A
O = 1219
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 871
T = 175.60
(out)(err)
S = N/A
O = 920
T = TO
(out)(err)
S = OPT
O = 871
T = 438.81
(out)(err)
S = OPT
O = 871
T = 450.76
(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 = 875
T = 1797.90
(out)(err)
S = OPT
O = 871
T = 80.00
(out)(err)
S = N/A
O = 968
T = TO
(out)(err)
S = N/A
O = 1171
T = TO
(out)(err)
S = N/A
O = 1229
T = TO
(out)(err)
S = N/A
O = 895
T = TO
(out)(err)
S = N/A
O = 1240
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.98
(out)(err)
S = N/A
O = N/A
T = 1397.28
(out)(err)
s2v140c1300_5.wcnf S = OPT
O = 844
T = 23.86
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 844
T = 33.15
(out)(err)
S = N/A
O = 1168
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 844
T = 57.07
(out)(err)
S = N/A
O = 863
T = TO
(out)(err)
S = OPT
O = 844
T = 147.13
(out)(err)
S = OPT
O = 844
T = 146.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 = 853
T = 1797.90
(out)(err)
S = OPT
O = 844
T = 23.86
(out)(err)
S = N/A
O = 931
T = TO
(out)(err)
S = N/A
O = 1080
T = TO
(out)(err)
S = N/A
O = 1054
T = TO
(out)(err)
S = N/A
O = 863
T = TO
(out)(err)
S = N/A
O = 1230
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.91
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1300_6.wcnf S = OPT
O = 884
T = 130.51
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 884
T = 259.29
(out)(err)
S = N/A
O = 1078
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 884
T = 370.84
(out)(err)
S = N/A
O = 990
T = TO
(out)(err)
S = OPT
O = 884
T = 1025.23
(out)(err)
S = OPT
O = 884
T = 1022.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 = 894
T = 1797.90
(out)(err)
S = OPT
O = 884
T = 130.51
(out)(err)
S = N/A
O = 988
T = TO
(out)(err)
S = N/A
O = 1196
T = TO
(out)(err)
S = N/A
O = 1185
T = TO
(out)(err)
S = N/A
O = 908
T = TO
(out)(err)
S = N/A
O = 1275
T = TO
(out)(err)
S = N/A
O = N/A
T = 326.00
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1300_7.wcnf S = OPT
O = 874
T = 47.96
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 874
T = 96.24
(out)(err)
S = N/A
O = 1070
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 874
T = 116.96
(out)(err)
S = N/A
O = 908
T = TO
(out)(err)
S = OPT
O = 874
T = 290.58
(out)(err)
S = OPT
O = 874
T = 286.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 = 898
T = 1797.85
(out)(err)
S = OPT
O = 874
T = 47.96
(out)(err)
S = N/A
O = 982
T = TO
(out)(err)
S = N/A
O = 1149
T = TO
(out)(err)
S = N/A
O = 1179
T = TO
(out)(err)
S = N/A
O = 914
T = TO
(out)(err)
S = N/A
O = 1159
T = TO
(out)(err)
S = N/A
O = N/A
T = 209.01
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1300_8.wcnf S = OPT
O = 812
T = 34.65
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 812
T = 55.65
(out)(err)
S = N/A
O = 1016
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 812
T = 94.02
(out)(err)
S = N/A
O = 981
T = TO
(out)(err)
S = OPT
O = 812
T = 234.76
(out)(err)
S = OPT
O = 812
T = 232.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 = 812
T = 1797.86
(out)(err)
S = OPT
O = 812
T = 34.65
(out)(err)
S = N/A
O = 892
T = TO
(out)(err)
S = N/A
O = 1160
T = TO
(out)(err)
S = N/A
O = 1076
T = TO
(out)(err)
S = N/A
O = 832
T = TO
(out)(err)
S = N/A
O = 1139
T = TO
(out)(err)
S = N/A
O = N/A
T = 204.88
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1400_1.wcnf S = OPT
O = 926
T = 44.88
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 926
T = 60.82
(out)(err)
S = N/A
O = 1230
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 926
T = 162.87
(out)(err)
S = N/A
O = 986
T = TO
(out)(err)
S = OPT
O = 926
T = 407.56
(out)(err)
S = OPT
O = 926
T = 428.76
(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 = 926
T = 1797.88
(out)(err)
S = OPT
O = 926
T = 44.88
(out)(err)
S = N/A
O = 1026
T = TO
(out)(err)
S = N/A
O = 1244
T = TO
(out)(err)
S = N/A
O = 1204
T = TO
(out)(err)
S = N/A
O = 970
T = TO
(out)(err)
S = N/A
O = 1348
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.78
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1400_2.wcnf S = OPT
O = 879
T = 15.02
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 879
T = 21.58
(out)(err)
S = N/A
O = 1243
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 879
T = 23.85
(out)(err)
S = N/A
O = 1054
T = TO
(out)(err)
S = OPT
O = 879
T = 75.38
(out)(err)
S = OPT
O = 879
T = 73.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 = 879
T = 1654.56
(out)(err)
S = OPT
O = 879
T = 15.02
(out)(err)
S = N/A
O = 963
T = TO
(out)(err)
S = N/A
O = 1123
T = TO
(out)(err)
S = N/A
O = 1118
T = TO
(out)(err)
S = N/A
O = 904
T = TO
(out)(err)
S = N/A
O = 1155
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.85
(out)(err)
S = N/A
O = N/A
T = 1723.75
(out)(err)
s2v140c1400_3.wcnf S = OPT
O = 936
T = 46.88
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 936
T = 53.79
(out)(err)
S = N/A
O = 1354
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 936
T = 95.76
(out)(err)
S = N/A
O = 1058
T = TO
(out)(err)
S = OPT
O = 936
T = 244.96
(out)(err)
S = OPT
O = 936
T = 248.18
(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 = 936
T = 1797.83
(out)(err)
S = OPT
O = 936
T = 46.88
(out)(err)
S = N/A
O = 1058
T = TO
(out)(err)
S = N/A
O = 1226
T = TO
(out)(err)
S = N/A
O = 1286
T = TO
(out)(err)
S = N/A
O = 974
T = TO
(out)(err)
S = N/A
O = 1393
T = TO
(out)(err)
S = N/A
O = N/A
T = 316.11
(out)(err)
S = N/A
O = N/A
T = 1377.16
(out)(err)
s2v140c1400_4.wcnf S = OPT
O = 932
T = 26.01
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 932
T = 59.72
(out)(err)
S = N/A
O = 1227
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 932
T = 58.95
(out)(err)
S = N/A
O = 1136
T = TO
(out)(err)
S = OPT
O = 932
T = 162.11
(out)(err)
S = OPT
O = 932
T = 157.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 = 938
T = 1797.87
(out)(err)
S = OPT
O = 932
T = 26.01
(out)(err)
S = N/A
O = 1066
T = TO
(out)(err)
S = N/A
O = 1202
T = TO
(out)(err)
S = N/A
O = 1286
T = TO
(out)(err)
S = N/A
O = 939
T = TO
(out)(err)
S = N/A
O = 1332
T = TO
(out)(err)
S = N/A
O = N/A
T = 204.82
(out)(err)
S = N/A
O = N/A
T = 1139.57
(out)(err)
s2v140c1400_5.wcnf S = OPT
O = 968
T = 52.46
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 968
T = 102.10
(out)(err)
S = N/A
O = 1388
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 968
T = 185.23
(out)(err)
S = N/A
O = 1036
T = TO
(out)(err)
S = OPT
O = 968
T = 517.51
(out)(err)
S = OPT
O = 968
T = 515.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 = 982
T = 1797.88
(out)(err)
S = OPT
O = 968
T = 52.46
(out)(err)
S = N/A
O = 1080
T = TO
(out)(err)
S = N/A
O = 1251
T = TO
(out)(err)
S = N/A
O = 1218
T = TO
(out)(err)
S = N/A
O = 1004
T = TO
(out)(err)
S = N/A
O = 1470
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.91
(out)(err)
S = N/A
O = N/A
T = 1268.03
(out)(err)
s2v140c1400_6.wcnf S = OPT
O = 967
T = 181.52
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 967
T = 238.11
(out)(err)
S = N/A
O = 1305
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 967
T = 387.03
(out)(err)
S = N/A
O = 1195
T = TO
(out)(err)
S = OPT
O = 967
T = 941.22
(out)(err)
S = OPT
O = 967
T = 1041.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 = 999
T = 1797.90
(out)(err)
S = OPT
O = 967
T = 181.52
(out)(err)
S = N/A
O = 1062
T = TO
(out)(err)
S = N/A
O = 1270
T = TO
(out)(err)
S = N/A
O = 1186
T = TO
(out)(err)
S = N/A
O = 1015
T = TO
(out)(err)
S = N/A
O = 1480
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.79
(out)(err)
S = N/A
O = N/A
T = 1288.46
(out)(err)
s2v140c1400_7.wcnf S = OPT
O = 923
T = 13.41
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 923
T = 43.52
(out)(err)
S = N/A
O = 1246
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 923
T = 41.66
(out)(err)
S = N/A
O = 1032
T = TO
(out)(err)
S = OPT
O = 923
T = 104.52
(out)(err)
S = OPT
O = 923
T = 103.06
(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 = 982
T = 1797.80
(out)(err)
S = OPT
O = 923
T = 13.41
(out)(err)
S = N/A
O = 1021
T = TO
(out)(err)
S = N/A
O = 1182
T = TO
(out)(err)
S = N/A
O = 1253
T = TO
(out)(err)
S = N/A
O = 959
T = TO
(out)(err)
S = N/A
O = 1391
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.96
(out)(err)
S = N/A
O = N/A
T = 1605.72
(out)(err)
s2v140c1400_8.wcnf S = OPT
O = 957
T = 61.67
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 957
T = 172.87
(out)(err)
S = N/A
O = 1233
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 957
T = 329.42
(out)(err)
S = N/A
O = 1073
T = TO
(out)(err)
S = OPT
O = 957
T = 972.66
(out)(err)
S = OPT
O = 957
T = 869.75
(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 = 970
T = 1797.88
(out)(err)
S = OPT
O = 957
T = 61.67
(out)(err)
S = N/A
O = 1067
T = TO
(out)(err)
S = N/A
O = 1213
T = TO
(out)(err)
S = N/A
O = 1288
T = TO
(out)(err)
S = N/A
O = 1011
T = TO
(out)(err)
S = N/A
O = 1290
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.10
(out)(err)
S = N/A
O = N/A
T = 1120.97
(out)(err)
s2v140c1500_1.wcnf S = OPT
O = 986
T = 18.89
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 986
T = 79.15
(out)(err)
S = N/A
O = 1252
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 986
T = 78.33
(out)(err)
S = N/A
O = 1081
T = TO
(out)(err)
S = OPT
O = 986
T = 226.96
(out)(err)
S = OPT
O = 986
T = 220.13
(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 = 994
T = 1797.91
(out)(err)
S = OPT
O = 986
T = 18.89
(out)(err)
S = N/A
O = 1104
T = TO
(out)(err)
S = N/A
O = 1241
T = TO
(out)(err)
S = N/A
O = 1385
T = TO
(out)(err)
S = N/A
O = 1034
T = TO
(out)(err)
S = N/A
O = 1645
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.19
(out)(err)
S = N/A
O = N/A
T = 931.91
(out)(err)
s2v140c1500_2.wcnf S = OPT
O = 998
T = 32.93
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 998
T = 75.22
(out)(err)
S = N/A
O = 1432
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 998
T = 118.86
(out)(err)
S = N/A
O = 1184
T = TO
(out)(err)
S = OPT
O = 998
T = 306.13
(out)(err)
S = OPT
O = 998
T = 316.77
(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 = 1018
T = 1797.89
(out)(err)
S = OPT
O = 998
T = 32.93
(out)(err)
S = N/A
O = 1090
T = TO
(out)(err)
S = N/A
O = 1271
T = TO
(out)(err)
S = N/A
O = 1300
T = TO
(out)(err)
S = N/A
O = 1044
T = TO
(out)(err)
S = N/A
O = 1576
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.78
(out)(err)
S = N/A
O = N/A
T = 1107.24
(out)(err)
s2v140c1500_3.wcnf S = OPT
O = 1073
T = 183.98
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1073
T = 242.93
(out)(err)
S = N/A
O = 1473
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1073
T = 694.87
(out)(err)
S = N/A
O = 1234
T = TO
(out)(err)
S = OPT
O = 1073
T = 1141.40
(out)(err)
S = OPT
O = 1073
T = 1158.78
(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 = 1078
T = 1797.91
(out)(err)
S = OPT
O = 1073
T = 183.98
(out)(err)
S = N/A
O = 1191
T = TO
(out)(err)
S = N/A
O = 1373
T = TO
(out)(err)
S = N/A
O = 1402
T = TO
(out)(err)
S = N/A
O = 1125
T = TO
(out)(err)
S = N/A
O = 1543
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.88
(out)(err)
S = N/A
O = N/A
T = 909.38
(out)(err)
s2v140c1500_4.wcnf S = OPT
O = 1047
T = 154.64
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1047
T = 352.74
(out)(err)
S = N/A
O = 1299
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1047
T = 972.79
(out)(err)
S = N/A
O = 1151
T = TO
(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 = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = 1090
T = 1797.89
(out)(err)
S = OPT
O = 1047
T = 154.64
(out)(err)
S = N/A
O = 1185
T = TO
(out)(err)
S = N/A
O = 1411
T = TO
(out)(err)
S = N/A
O = 1454
T = TO
(out)(err)
S = N/A
O = 1097
T = TO
(out)(err)
S = N/A
O = 1572
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.80
(out)(err)
S = N/A
O = N/A
T = 1435.74
(out)(err)
s2v140c1500_5.wcnf S = OPT
O = 1058
T = 90.19
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1058
T = 321.22
(out)(err)
S = N/A
O = 1469
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1058
T = 662.66
(out)(err)
S = N/A
O = 1254
T = TO
(out)(err)
S = N/A
O = 1058
T = TO
(out)(err)
S = N/A
O = 1058
T = TO
(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 = 1122
T = 1797.85
(out)(err)
S = OPT
O = 1058
T = 90.19
(out)(err)
S = N/A
O = 1185
T = TO
(out)(err)
S = N/A
O = 1401
T = TO
(out)(err)
S = N/A
O = 1508
T = TO
(out)(err)
S = N/A
O = 1145
T = TO
(out)(err)
S = N/A
O = 1493
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.95
(out)(err)
S = N/A
O = N/A
T = 1207.27
(out)(err)
s2v140c1500_6.wcnf S = OPT
O = 1102
T = 298.53
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1102
T = 350.16
(out)(err)
S = N/A
O = 1506
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1102
T = 640.37
(out)(err)
S = N/A
O = 1234
T = TO
(out)(err)
S = OPT
O = 1102
T = 1779.48
(out)(err)
S = OPT
O = 1102
T = 1767.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 = 1102
T = 1797.88
(out)(err)
S = OPT
O = 1102
T = 298.53
(out)(err)
S = N/A
O = 1220
T = TO
(out)(err)
S = N/A
O = 1389
T = TO
(out)(err)
S = N/A
O = 1549
T = TO
(out)(err)
S = N/A
O = 1223
T = TO
(out)(err)
S = N/A
O = 1581
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)
s2v140c1500_7.wcnf S = OPT
O = 1010
T = 19.02
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1010
T = 27.19
(out)(err)
S = N/A
O = 1357
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1010
T = 60.98
(out)(err)
S = N/A
O = 1081
T = TO
(out)(err)
S = OPT
O = 1010
T = 171.48
(out)(err)
S = OPT
O = 1010
T = 161.79
(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 = 1035
T = 1797.88
(out)(err)
S = OPT
O = 1010
T = 19.02
(out)(err)
S = N/A
O = 1130
T = TO
(out)(err)
S = N/A
O = 1208
T = TO
(out)(err)
S = N/A
O = 1285
T = TO
(out)(err)
S = N/A
O = 1046
T = TO
(out)(err)
S = N/A
O = 1381
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.01
(out)(err)
S = N/A
O = N/A
T = 1757.05
(out)(err)
s2v140c1500_8.wcnf S = OPT
O = 1045
T = 59.40
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1045
T = 107.06
(out)(err)
S = N/A
O = 1521
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1045
T = 128.07
(out)(err)
S = N/A
O = 1167
T = TO
(out)(err)
S = OPT
O = 1045
T = 416.79
(out)(err)
S = OPT
O = 1045
T = 420.06
(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 = 1068
T = 1797.91
(out)(err)
S = OPT
O = 1045
T = 59.40
(out)(err)
S = N/A
O = 1172
T = TO
(out)(err)
S = N/A
O = 1345
T = TO
(out)(err)
S = N/A
O = 1428
T = TO
(out)(err)
S = N/A
O = 1110
T = TO
(out)(err)
S = N/A
O = 1481
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.02
(out)(err)
S = N/A
O = N/A
T = 1084.79
(out)(err)
s2v140c1600_1.wcnf S = OPT
O = 1143
T = 43.50
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1143
T = 54.76
(out)(err)
S = N/A
O = 1584
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1143
T = 91.11
(out)(err)
S = N/A
O = 1314
T = TO
(out)(err)
S = OPT
O = 1143
T = 265.67
(out)(err)
S = OPT
O = 1143
T = 273.44
(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 = 1144
T = 1797.89
(out)(err)
S = OPT
O = 1143
T = 43.50
(out)(err)
S = N/A
O = 1255
T = TO
(out)(err)
S = N/A
O = 1456
T = TO
(out)(err)
S = N/A
O = 1460
T = TO
(out)(err)
S = N/A
O = 1196
T = TO
(out)(err)
S = N/A
O = 1650
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.00
(out)(err)
S = N/A
O = N/A
T = 1584.91
(out)(err)
s2v140c1600_2.wcnf S = OPT
O = 1140
T = 36.20
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1140
T = 44.38
(out)(err)
S = N/A
O = 1435
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1140
T = 107.17
(out)(err)
S = N/A
O = 1248
T = TO
(out)(err)
S = OPT
O = 1140
T = 287.44
(out)(err)
S = OPT
O = 1140
T = 283.38
(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 = 1145
T = 1797.93
(out)(err)
S = OPT
O = 1140
T = 36.20
(out)(err)
S = N/A
O = 1258
T = TO
(out)(err)
S = N/A
O = 1706
T = TO
(out)(err)
S = N/A
O = 1546
T = TO
(out)(err)
S = N/A
O = 1193
T = TO
(out)(err)
S = N/A
O = 1466
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.82
(out)(err)
S = N/A
O = N/A
T = 1044.37
(out)(err)
s2v140c1600_3.wcnf S = OPT
O = 1079
T = 30.63
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1079
T = 33.67
(out)(err)
S = N/A
O = 1356
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1079
T = 61.40
(out)(err)
S = N/A
O = 1371
T = TO
(out)(err)
S = OPT
O = 1079
T = 179.54
(out)(err)
S = OPT
O = 1079
T = 183.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 = 1079
T = 1797.94
(out)(err)
S = OPT
O = 1079
T = 30.63
(out)(err)
S = N/A
O = 1157
T = TO
(out)(err)
S = N/A
O = 1403
T = TO
(out)(err)
S = N/A
O = 1423
T = TO
(out)(err)
S = N/A
O = 1140
T = TO
(out)(err)
S = N/A
O = 1578
T = TO
(out)(err)
S = N/A
O = N/A
T = 340.10
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1600_4.wcnf S = OPT
O = 1157
T = 94.90
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1157
T = 98.49
(out)(err)
S = N/A
O = 1639
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1157
T = 286.75
(out)(err)
S = N/A
O = 1278
T = TO
(out)(err)
S = OPT
O = 1157
T = 767.09
(out)(err)
S = OPT
O = 1157
T = 766.18
(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 = 1171
T = 1797.86
(out)(err)
S = OPT
O = 1157
T = 94.90
(out)(err)
S = N/A
O = 1300
T = TO
(out)(err)
S = N/A
O = 1453
T = TO
(out)(err)
S = N/A
O = 1653
T = TO
(out)(err)
S = N/A
O = 1195
T = TO
(out)(err)
S = N/A
O = 1702
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.93
(out)(err)
S = N/A
O = N/A
T = 679.56
(out)(err)
s2v140c1600_5.wcnf S = OPT
O = 1119
T = 89.04
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1119
T = 158.98
(out)(err)
S = N/A
O = 1484
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1119
T = 294.29
(out)(err)
S = N/A
O = 1252
T = TO
(out)(err)
S = OPT
O = 1119
T = 991.31
(out)(err)
S = OPT
O = 1119
T = 1012.71
(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 = 1146
T = 1797.86
(out)(err)
S = OPT
O = 1119
T = 89.04
(out)(err)
S = N/A
O = 1281
T = TO
(out)(err)
S = N/A
O = 1560
T = TO
(out)(err)
S = N/A
O = 1425
T = TO
(out)(err)
S = N/A
O = 1196
T = TO
(out)(err)
S = N/A
O = 1601
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.89
(out)(err)
S = N/A
O = N/A
T = 673.41
(out)(err)
s2v140c1600_6.wcnf S = OPT
O = 1212
T = 170.16
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1212
T = 265.93
(out)(err)
S = N/A
O = 1582
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1212
T = 532.56
(out)(err)
S = N/A
O = 1424
T = TO
(out)(err)
S = OPT
O = 1212
T = 1321.56
(out)(err)
S = OPT
O = 1212
T = 1341.55
(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 = 1212
T = 1797.86
(out)(err)
S = OPT
O = 1212
T = 170.16
(out)(err)
S = N/A
O = 1328
T = TO
(out)(err)
S = N/A
O = 1491
T = TO
(out)(err)
S = N/A
O = 1646
T = TO
(out)(err)
S = N/A
O = 1300
T = TO
(out)(err)
S = N/A
O = 1725
T = TO
(out)(err)
S = N/A
O = N/A
T = 179.00
(out)(err)
S = N/A
O = N/A
T = 721.20
(out)(err)
s2v140c1600_7.wcnf S = OPT
O = 1150
T = 95.03
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1150
T = 162.54
(out)(err)
S = N/A
O = 1616
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1150
T = 436.01
(out)(err)
S = N/A
O = 1355
T = TO
(out)(err)
S = OPT
O = 1150
T = 1025.08
(out)(err)
S = OPT
O = 1150
T = 1122.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 = 1218
T = 1797.82
(out)(err)
S = OPT
O = 1150
T = 95.03
(out)(err)
S = N/A
O = 1291
T = TO
(out)(err)
S = N/A
O = 1395
T = TO
(out)(err)
S = N/A
O = 1422
T = TO
(out)(err)
S = N/A
O = 1190
T = TO
(out)(err)
S = N/A
O = 1644
T = TO
(out)(err)
S = N/A
O = N/A
T = 178.65
(out)(err)
S = N/A
O = N/A
T = 1005.62
(out)(err)
s2v140c1600_8.wcnf S = OPT
O = 1180
T = 72.10
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1180
T = 102.79
(out)(err)
S = N/A
O = 1474
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1180
T = 226.95
(out)(err)
S = N/A
O = 1295
T = TO
(out)(err)
S = OPT
O = 1180
T = 640.14
(out)(err)
S = OPT
O = 1180
T = 641.17
(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 = 1226
T = 1797.84
(out)(err)
S = OPT
O = 1180
T = 72.10
(out)(err)
S = N/A
O = 1324
T = TO
(out)(err)
S = N/A
O = 1416
T = TO
(out)(err)
S = N/A
O = 1590
T = TO
(out)(err)
S = N/A
O = 1243
T = TO
(out)(err)
S = N/A
O = 1589
T = TO
(out)(err)
S = N/A
O = N/A
T = 180.43
(out)(err)
S = N/A
O = N/A
T = 666.60
(out)(err)
file_rwms_wcnf_L3_V70_C1000_0.wcnf S = OPT
O = 198
T = 143.40
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 198
T = 143.40
(out)(err)
S = N/A
O = 318
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 198
T = 195.52
(out)(err)
S = N/A
O = 308
T = TO
(out)(err)
S = OPT
O = 198
T = 549.69
(out)(err)
S = OPT
O = 198
T = 551.30
(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 = 208
T = 1797.47
(out)(err)
S = OPT
O = 198
T = 196.56
(out)(err)
S = N/A
O = 237
T = TO
(out)(err)
S = N/A
O = 421
T = TO
(out)(err)
S = N/A
O = 495
T = TO
(out)(err)
S = N/A
O = 213
T = TO
(out)(err)
S = N/A
O = 470
T = TO
(out)(err)
S = N/A
O = N/A
T = 614.43
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C1000_1.wcnf S = OPT
O = 212
T = 92.21
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 212
T = 92.21
(out)(err)
S = N/A
O = 333
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 212
T = 111.20
(out)(err)
S = N/A
O = 256
T = TO
(out)(err)
S = OPT
O = 212
T = 295.18
(out)(err)
S = OPT
O = 212
T = 300.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 = 212
T = 1375.67
(out)(err)
S = OPT
O = 212
T = 154.66
(out)(err)
S = N/A
O = 247
T = TO
(out)(err)
S = N/A
O = 455
T = TO
(out)(err)
S = N/A
O = 450
T = TO
(out)(err)
S = N/A
O = 227
T = TO
(out)(err)
S = N/A
O = 497
T = TO
(out)(err)
S = N/A
O = N/A
T = 414.37
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C1000_2.wcnf S = OPT
O = 211
T = 128.49
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 211
T = 128.49
(out)(err)
S = N/A
O = 290
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 211
T = 162.87
(out)(err)
S = N/A
O = 230
T = TO
(out)(err)
S = OPT
O = 211
T = 432.74
(out)(err)
S = OPT
O = 211
T = 435.94
(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 = 211
T = 1797.57
(out)(err)
S = OPT
O = 211
T = 270.83
(out)(err)
S = N/A
O = 247
T = TO
(out)(err)
S = N/A
O = 476
T = TO
(out)(err)
S = N/A
O = 452
T = TO
(out)(err)
S = N/A
O = 215
T = TO
(out)(err)
S = N/A
O = 354
T = TO
(out)(err)
S = N/A
O = N/A
T = 613.88
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C1000_3.wcnf S = OPT
O = 229
T = 177.70
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 229
T = 177.70
(out)(err)
S = N/A
O = 321
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 229
T = 222.32
(out)(err)
S = N/A
O = 250
T = TO
(out)(err)
S = OPT
O = 229
T = 600.85
(out)(err)
S = OPT
O = 229
T = 609.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 = 229
T = 1797.30
(out)(err)
S = OPT
O = 229
T = 312.20
(out)(err)
S = N/A
O = 269
T = TO
(out)(err)
S = N/A
O = 466
T = TO
(out)(err)
S = N/A
O = 495
T = TO
(out)(err)
S = N/A
O = 237
T = TO
(out)(err)
S = N/A
O = 512
T = TO
(out)(err)
S = N/A
O = N/A
T = 409.38
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C1000_4.wcnf S = OPT
O = 202
T = 114.25
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 202
T = 114.25
(out)(err)
S = N/A
O = 289
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 202
T = 137.46
(out)(err)
S = N/A
O = 228
T = TO
(out)(err)
S = OPT
O = 202
T = 376.14
(out)(err)
S = OPT
O = 202
T = 386.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 = 202
T = 1673.54
(out)(err)
S = OPT
O = 202
T = 155.16
(out)(err)
S = N/A
O = 223
T = TO
(out)(err)
S = N/A
O = 416
T = TO
(out)(err)
S = N/A
O = 453
T = TO
(out)(err)
S = N/A
O = 210
T = TO
(out)(err)
S = N/A
O = 374
T = TO
(out)(err)
S = N/A
O = N/A
T = 615.66
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C1000_5.wcnf S = OPT
O = 214
T = 167.71
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 214
T = 221.86
(out)(err)
S = N/A
O = 352
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 214
T = 257.71
(out)(err)
S = N/A
O = 247
T = TO
(out)(err)
S = OPT
O = 214
T = 707.57
(out)(err)
S = OPT
O = 214
T = 699.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 = 248
T = 1797.22
(out)(err)
S = OPT
O = 214
T = 167.71
(out)(err)
S = N/A
O = 268
T = TO
(out)(err)
S = N/A
O = 437
T = TO
(out)(err)
S = N/A
O = 444
T = TO
(out)(err)
S = N/A
O = 214
T = TO
(out)(err)
S = N/A
O = 433
T = TO
(out)(err)
S = N/A
O = N/A
T = 207.98
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C1000_6.wcnf S = OPT
O = 203
T = 61.34
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 203
T = 61.34
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 203
T = 68.69
(out)(err)
S = N/A
O = 232
T = TO
(out)(err)
S = OPT
O = 203
T = 182.48
(out)(err)
S = OPT
O = 203
T = 187.32
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 203
T = 792.11
(out)(err)
S = OPT
O = 203
T = 115.10
(out)(err)
S = N/A
O = 251
T = TO
(out)(err)
S = N/A
O = 452
T = TO
(out)(err)
S = N/A
O = 526
T = TO
(out)(err)
S = N/A
O = 208
T = TO
(out)(err)
S = N/A
O = 543
T = TO
(out)(err)
S = N/A
O = N/A
T = 204.41
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C1000_7.wcnf S = OPT
O = 200
T = 68.36
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 200
T = 82.79
(out)(err)
S = N/A
O = 285
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 200
T = 68.36
(out)(err)
S = N/A
O = 265
T = TO
(out)(err)
S = OPT
O = 200
T = 197.69
(out)(err)
S = OPT
O = 200
T = 195.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 = 200
T = 966.15
(out)(err)
S = OPT
O = 200
T = 97.02
(out)(err)
S = N/A
O = 245
T = TO
(out)(err)
S = N/A
O = 372
T = TO
(out)(err)
S = N/A
O = 499
T = TO
(out)(err)
S = N/A
O = 200
T = TO
(out)(err)
S = N/A
O = 414
T = TO
(out)(err)
S = N/A
O = N/A
T = 238.86
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C1000_8.wcnf S = OPT
O = 188
T = 54.14
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 188
T = 80.38
(out)(err)
S = N/A
O = 275
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 188
T = 106.38
(out)(err)
S = N/A
O = 255
T = TO
(out)(err)
S = OPT
O = 188
T = 282.84
(out)(err)
S = OPT
O = 188
T = 284.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 = 188
T = 1275.07
(out)(err)
S = OPT
O = 188
T = 54.14
(out)(err)
S = N/A
O = 213
T = TO
(out)(err)
S = N/A
O = 392
T = TO
(out)(err)
S = N/A
O = 393
T = TO
(out)(err)
S = N/A
O = 191
T = TO
(out)(err)
S = N/A
O = 438
T = TO
(out)(err)
S = N/A
O = N/A
T = 542.13
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C1000_9.wcnf S = OPT
O = 226
T = 161.00
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 226
T = 161.00
(out)(err)
S = N/A
O = 305
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 226
T = 215.95
(out)(err)
S = N/A
O = 240
T = TO
(out)(err)
S = OPT
O = 226
T = 575.95
(out)(err)
S = OPT
O = 226
T = 582.27
(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 = 226
T = 1797.38
(out)(err)
S = OPT
O = 226
T = 337.07
(out)(err)
S = N/A
O = 252
T = TO
(out)(err)
S = N/A
O = 406
T = TO
(out)(err)
S = N/A
O = 445
T = TO
(out)(err)
S = N/A
O = 229
T = TO
(out)(err)
S = N/A
O = 455
T = TO
(out)(err)
S = N/A
O = N/A
T = 204.29
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C700_0.wcnf S = OPT
O = 103
T = 22.36
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 103
T = 25.60
(out)(err)
S = N/A
O = 125
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 103
T = 22.36
(out)(err)
S = N/A
O = 108
T = TO
(out)(err)
S = OPT
O = 103
T = 65.41
(out)(err)
S = OPT
O = 103
T = 65.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 = 103
T = 354.11
(out)(err)
S = OPT
O = 103
T = 52.63
(out)(err)
S = N/A
O = 109
T = TO
(out)(err)
S = N/A
O = 143
T = TO
(out)(err)
S = N/A
O = 247
T = TO
(out)(err)
S = N/A
O = 103
T = TO
(out)(err)
S = N/A
O = 187
T = TO
(out)(err)
S = N/A
O = N/A
T = 285.70
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C700_1.wcnf S = OPT
O = 107
T = 12.84
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 107
T = 15.78
(out)(err)
S = N/A
O = 145
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 107
T = 12.84
(out)(err)
S = N/A
O = 107
T = TO
(out)(err)
S = OPT
O = 107
T = 34.53
(out)(err)
S = OPT
O = 107
T = 35.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 = 107
T = 185.82
(out)(err)
S = OPT
O = 107
T = 35.78
(out)(err)
S = N/A
O = 118
T = TO
(out)(err)
S = N/A
O = 286
T = TO
(out)(err)
S = N/A
O = 139
T = TO
(out)(err)
S = N/A
O = 107
T = TO
(out)(err)
S = N/A
O = 322
T = TO
(out)(err)
S = N/A
O = N/A
T = 317.51
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C700_2.wcnf S = OPT
O = 110
T = 19.36
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 110
T = 19.36
(out)(err)
S = N/A
O = 125
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 110
T = 19.92
(out)(err)
S = N/A
O = 110
T = TO
(out)(err)
S = OPT
O = 110
T = 54.28
(out)(err)
S = OPT
O = 110
T = 57.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 = 110
T = 294.84
(out)(err)
S = OPT
O = 110
T = 52.95
(out)(err)
S = N/A
O = 117
T = TO
(out)(err)
S = N/A
O = 139
T = TO
(out)(err)
S = N/A
O = 162
T = TO
(out)(err)
S = N/A
O = 110
T = TO
(out)(err)
S = N/A
O = 298
T = TO
(out)(err)
S = N/A
O = N/A
T = 293.87
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C700_3.wcnf S = OPT
O = 102
T = 6.56
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 102
T = 8.94
(out)(err)
S = N/A
O = 129
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 102
T = 6.56
(out)(err)
S = N/A
O = 108
T = TO
(out)(err)
S = OPT
O = 102
T = 18.15
(out)(err)
S = OPT
O = 102
T = 19.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 = 102
T = 101.60
(out)(err)
S = OPT
O = 102
T = 20.72
(out)(err)
S = N/A
O = 116
T = TO
(out)(err)
S = N/A
O = 316
T = TO
(out)(err)
S = N/A
O = 143
T = TO
(out)(err)
S = N/A
O = 102
T = TO
(out)(err)
S = N/A
O = 318
T = TO
(out)(err)
S = N/A
O = N/A
T = 298.83
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C700_4.wcnf S = OPT
O = 110
T = 22.67
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 110
T = 25.05
(out)(err)
S = N/A
O = 142
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 110
T = 22.67
(out)(err)
S = N/A
O = 116
T = TO
(out)(err)
S = OPT
O = 110
T = 62.51
(out)(err)
S = OPT
O = 110
T = 62.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 = 110
T = 359.17
(out)(err)
S = OPT
O = 110
T = 69.29
(out)(err)
S = N/A
O = 124
T = TO
(out)(err)
S = N/A
O = 270
T = TO
(out)(err)
S = N/A
O = 247
T = TO
(out)(err)
S = N/A
O = 110
T = TO
(out)(err)
S = N/A
O = 339
T = TO
(out)(err)
S = N/A
O = N/A
T = 237.70
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C700_5.wcnf S = OPT
O = 103
T = 15.33
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 103
T = 19.02
(out)(err)
S = N/A
O = 125
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 103
T = 15.33
(out)(err)
S = N/A
O = 103
T = TO
(out)(err)
S = OPT
O = 103
T = 39.84
(out)(err)
S = OPT
O = 103
T = 41.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 = 103
T = 221.28
(out)(err)
S = OPT
O = 103
T = 25.38
(out)(err)
S = N/A
O = 118
T = TO
(out)(err)
S = N/A
O = 141
T = TO
(out)(err)
S = N/A
O = 183
T = TO
(out)(err)
S = N/A
O = 103
T = TO
(out)(err)
S = N/A
O = 198
T = TO
(out)(err)
S = N/A
O = N/A
T = 297.82
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C700_6.wcnf S = OPT
O = 102
T = 10.81
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 102
T = 12.54
(out)(err)
S = N/A
O = 132
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 102
T = 10.81
(out)(err)
S = N/A
O = 102
T = TO
(out)(err)
S = OPT
O = 102
T = 29.92
(out)(err)
S = OPT
O = 102
T = 29.82
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 102
T = 167.68
(out)(err)
S = OPT
O = 102
T = 26.59
(out)(err)
S = N/A
O = 121
T = TO
(out)(err)
S = N/A
O = 234
T = TO
(out)(err)
S = N/A
O = 254
T = TO
(out)(err)
S = N/A
O = 102
T = TO
(out)(err)
S = N/A
O = 268
T = TO
(out)(err)
S = N/A
O = N/A
T = 396.14
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C700_7.wcnf S = OPT
O = 104
T = 11.87
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 104
T = 13.50
(out)(err)
S = N/A
O = 160
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 104
T = 11.87
(out)(err)
S = N/A
O = 114
T = TO
(out)(err)
S = OPT
O = 104
T = 32.40
(out)(err)
S = OPT
O = 104
T = 32.52
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 104
T = 169.96
(out)(err)
S = OPT
O = 104
T = 35.33
(out)(err)
S = N/A
O = 121
T = TO
(out)(err)
S = N/A
O = 312
T = TO
(out)(err)
S = N/A
O = 145
T = TO
(out)(err)
S = N/A
O = 104
T = TO
(out)(err)
S = N/A
O = 306
T = TO
(out)(err)
S = N/A
O = N/A
T = 285.87
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C700_8.wcnf S = OPT
O = 82
T = 2.06
S = N/A
O = 82
T = TO
(out)(err)
S = OPT
O = 82
T = 2.71
(out)(err)
S = N/A
O = 85
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 82
T = 2.06
(out)(err)
S = N/A
O = 91
T = TO
(out)(err)
S = OPT
O = 82
T = 5.00
(out)(err)
S = OPT
O = 82
T = 4.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 = 82
T = 28.99
(out)(err)
S = OPT
O = 82
T = 5.84
(out)(err)
S = N/A
O = 86
T = TO
(out)(err)
S = N/A
O = 127
T = TO
(out)(err)
S = N/A
O = 166
T = TO
(out)(err)
S = OPT
O = 82
T = 670.25
(out)(err)
S = N/A
O = 145
T = TO
(out)(err)
S = N/A
O = N/A
T = 285.98
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C700_9.wcnf S = OPT
O = 104
T = 12.50
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 104
T = 12.50
(out)(err)
S = N/A
O = 152
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 104
T = 13.43
(out)(err)
S = N/A
O = 104
T = TO
(out)(err)
S = OPT
O = 104
T = 36.15
(out)(err)
S = OPT
O = 104
T = 35.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 = 104
T = 187.27
(out)(err)
S = OPT
O = 104
T = 39.68
(out)(err)
S = N/A
O = 111
T = TO
(out)(err)
S = N/A
O = 257
T = TO
(out)(err)
S = N/A
O = 259
T = TO
(out)(err)
S = N/A
O = 104
T = TO
(out)(err)
S = N/A
O = 279
T = TO
(out)(err)
S = N/A
O = N/A
T = 285.57
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C800_0.wcnf S = OPT
O = 132
T = 28.57
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 132
T = 28.57
(out)(err)
S = N/A
O = 147
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 132
T = 30.72
(out)(err)
S = N/A
O = 158
T = TO
(out)(err)
S = OPT
O = 132
T = 84.49
(out)(err)
S = OPT
O = 132
T = 85.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 = 132
T = 426.17
(out)(err)
S = OPT
O = 132
T = 54.24
(out)(err)
S = N/A
O = 142
T = TO
(out)(err)
S = N/A
O = 334
T = TO
(out)(err)
S = N/A
O = 166
T = TO
(out)(err)
S = N/A
O = 132
T = TO
(out)(err)
S = N/A
O = 238
T = TO
(out)(err)
S = N/A
O = N/A
T = 238.14
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C800_1.wcnf S = OPT
O = 138
T = 42.48
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 138
T = 42.48
(out)(err)
S = N/A
O = 191
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 138
T = 49.10
(out)(err)
S = N/A
O = 165
T = TO
(out)(err)
S = OPT
O = 138
T = 134.56
(out)(err)
S = OPT
O = 138
T = 133.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 = 138
T = 697.12
(out)(err)
S = OPT
O = 138
T = 63.69
(out)(err)
S = N/A
O = 160
T = TO
(out)(err)
S = N/A
O = 346
T = TO
(out)(err)
S = N/A
O = 290
T = TO
(out)(err)
S = N/A
O = 138
T = TO
(out)(err)
S = N/A
O = 408
T = TO
(out)(err)
S = N/A
O = N/A
T = 237.59
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C800_2.wcnf S = OPT
O = 127
T = 28.62
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 127
T = 28.70
(out)(err)
S = N/A
O = 195
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 127
T = 28.62
(out)(err)
S = N/A
O = 147
T = TO
(out)(err)
S = OPT
O = 127
T = 79.81
(out)(err)
S = OPT
O = 127
T = 79.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 = 127
T = 368.69
(out)(err)
S = OPT
O = 127
T = 32.10
(out)(err)
S = N/A
O = 150
T = TO
(out)(err)
S = N/A
O = 317
T = TO
(out)(err)
S = N/A
O = 296
T = TO
(out)(err)
S = N/A
O = 127
T = TO
(out)(err)
S = N/A
O = 335
T = TO
(out)(err)
S = N/A
O = N/A
T = 286.74
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C800_3.wcnf S = OPT
O = 134
T = 12.95
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 134
T = 12.95
(out)(err)
S = N/A
O = 233
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 134
T = 19.41
(out)(err)
S = N/A
O = 159
T = TO
(out)(err)
S = OPT
O = 134
T = 50.94
(out)(err)
S = OPT
O = 134
T = 52.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 = 134
T = 280.95
(out)(err)
S = OPT
O = 134
T = 23.12
(out)(err)
S = N/A
O = 148
T = TO
(out)(err)
S = N/A
O = 302
T = TO
(out)(err)
S = N/A
O = 356
T = TO
(out)(err)
S = N/A
O = 134
T = TO
(out)(err)
S = N/A
O = 434
T = TO
(out)(err)
S = N/A
O = N/A
T = 607.17
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C800_4.wcnf S = OPT
O = 143
T = 65.89
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 143
T = 88.74
(out)(err)
S = N/A
O = 278
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 143
T = 69.73
(out)(err)
S = N/A
O = 186
T = TO
(out)(err)
S = OPT
O = 143
T = 188.89
(out)(err)
S = OPT
O = 143
T = 188.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 = 143
T = 1014.77
(out)(err)
S = OPT
O = 143
T = 65.89
(out)(err)
S = N/A
O = 166
T = TO
(out)(err)
S = N/A
O = 213
T = TO
(out)(err)
S = N/A
O = 210
T = TO
(out)(err)
S = N/A
O = 143
T = TO
(out)(err)
S = N/A
O = 285
T = TO
(out)(err)
S = N/A
O = N/A
T = 258.64
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C800_5.wcnf S = OPT
O = 144
T = 68.22
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 144
T = 68.22
(out)(err)
S = N/A
O = 204
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 144
T = 73.25
(out)(err)
S = N/A
O = 153
T = TO
(out)(err)
S = OPT
O = 144
T = 210.41
(out)(err)
S = OPT
O = 144
T = 210.40
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 144
T = 1033.26
(out)(err)
S = OPT
O = 144
T = 134.30
(out)(err)
S = N/A
O = 167
T = TO
(out)(err)
S = N/A
O = 210
T = TO
(out)(err)
S = N/A
O = 327
T = TO
(out)(err)
S = N/A
O = 144
T = TO
(out)(err)
S = N/A
O = 421
T = TO
(out)(err)
S = N/A
O = N/A
T = 241.12
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C800_6.wcnf S = OPT
O = 135
T = 31.76
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 135
T = 36.63
(out)(err)
S = N/A
O = 165
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 135
T = 31.76
(out)(err)
S = N/A
O = 136
T = TO
(out)(err)
S = OPT
O = 135
T = 91.19
(out)(err)
S = OPT
O = 135
T = 94.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 = 135
T = 495.18
(out)(err)
S = OPT
O = 135
T = 61.35
(out)(err)
S = N/A
O = 142
T = TO
(out)(err)
S = N/A
O = 389
T = TO
(out)(err)
S = N/A
O = 297
T = TO
(out)(err)
S = N/A
O = 135
T = TO
(out)(err)
S = N/A
O = 349
T = TO
(out)(err)
S = N/A
O = N/A
T = 237.88
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C800_7.wcnf S = OPT
O = 147
T = 36.61
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 147
T = 36.61
(out)(err)
S = N/A
O = 225
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 147
T = 56.74
(out)(err)
S = N/A
O = 161
T = TO
(out)(err)
S = OPT
O = 147
T = 148.95
(out)(err)
S = OPT
O = 147
T = 152.96
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 147
T = 821.86
(out)(err)
S = OPT
O = 147
T = 62.34
(out)(err)
S = N/A
O = 175
T = TO
(out)(err)
S = N/A
O = 384
T = TO
(out)(err)
S = N/A
O = 323
T = TO
(out)(err)
S = N/A
O = 150
T = TO
(out)(err)
S = N/A
O = 515
T = TO
(out)(err)
S = N/A
O = N/A
T = 242.08
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C800_8.wcnf S = OPT
O = 126
T = 28.98
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 126
T = 36.06
(out)(err)
S = N/A
O = 159
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 126
T = 39.32
(out)(err)
S = N/A
O = 126
T = TO
(out)(err)
S = OPT
O = 126
T = 99.79
(out)(err)
S = OPT
O = 126
T = 100.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 = 126
T = 507.47
(out)(err)
S = OPT
O = 126
T = 28.98
(out)(err)
S = N/A
O = 151
T = TO
(out)(err)
S = N/A
O = 287
T = TO
(out)(err)
S = N/A
O = 390
T = TO
(out)(err)
S = N/A
O = 126
T = TO
(out)(err)
S = N/A
O = 252
T = TO
(out)(err)
S = N/A
O = N/A
T = 237.83
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C800_9.wcnf S = OPT
O = 138
T = 32.23
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 138
T = 34.80
(out)(err)
S = N/A
O = 167
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 138
T = 32.23
(out)(err)
S = N/A
O = 156
T = TO
(out)(err)
S = OPT
O = 138
T = 89.83
(out)(err)
S = OPT
O = 138
T = 90.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 = 138
T = 452.40
(out)(err)
S = OPT
O = 138
T = 52.41
(out)(err)
S = N/A
O = 151
T = TO
(out)(err)
S = N/A
O = 308
T = TO
(out)(err)
S = N/A
O = 331
T = TO
(out)(err)
S = N/A
O = 138
T = TO
(out)(err)
S = N/A
O = 321
T = TO
(out)(err)
S = N/A
O = N/A
T = 238.69
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C900_0.wcnf S = OPT
O = 157
T = 31.40
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 157
T = 31.40
(out)(err)
S = N/A
O = 213
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 157
T = 34.30
(out)(err)
S = N/A
O = 224
T = TO
(out)(err)
S = OPT
O = 157
T = 95.03
(out)(err)
S = OPT
O = 157
T = 97.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 = 157
T = 446.32
(out)(err)
S = OPT
O = 157
T = 73.18
(out)(err)
S = N/A
O = 159
T = TO
(out)(err)
S = N/A
O = 359
T = TO
(out)(err)
S = N/A
O = 364
T = TO
(out)(err)
S = N/A
O = 157
T = TO
(out)(err)
S = N/A
O = 424
T = TO
(out)(err)
S = N/A
O = N/A
T = 538.59
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C900_1.wcnf S = OPT
O = 192
T = 121.84
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 192
T = 137.26
(out)(err)
S = N/A
O = 260
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 192
T = 121.84
(out)(err)
S = N/A
O = 211
T = TO
(out)(err)
S = OPT
O = 192
T = 328.33
(out)(err)
S = OPT
O = 192
T = 335.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 = 192
T = 1721.86
(out)(err)
S = OPT
O = 192
T = 231.75
(out)(err)
S = N/A
O = 213
T = TO
(out)(err)
S = N/A
O = 386
T = TO
(out)(err)
S = N/A
O = 543
T = TO
(out)(err)
S = N/A
O = 194
T = TO
(out)(err)
S = N/A
O = 422
T = TO
(out)(err)
S = N/A
O = N/A
T = 243.96
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C900_2.wcnf S = OPT
O = 177
T = 91.99
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 177
T = 91.99
(out)(err)
S = N/A
O = 199
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 177
T = 98.47
(out)(err)
S = N/A
O = 184
T = TO
(out)(err)
S = OPT
O = 177
T = 275.08
(out)(err)
S = OPT
O = 177
T = 272.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 = 177
T = 1398.86
(out)(err)
S = OPT
O = 177
T = 152.52
(out)(err)
S = N/A
O = 191
T = TO
(out)(err)
S = N/A
O = 333
T = TO
(out)(err)
S = N/A
O = 405
T = TO
(out)(err)
S = N/A
O = 178
T = TO
(out)(err)
S = N/A
O = 375
T = TO
(out)(err)
S = N/A
O = N/A
T = 240.00
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C900_3.wcnf S = OPT
O = 163
T = 50.67
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 163
T = 50.67
(out)(err)
S = N/A
O = 194
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 163
T = 63.14
(out)(err)
S = N/A
O = 163
T = TO
(out)(err)
S = OPT
O = 163
T = 176.46
(out)(err)
S = OPT
O = 163
T = 176.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 = 163
T = 826.40
(out)(err)
S = OPT
O = 163
T = 76.89
(out)(err)
S = N/A
O = 194
T = TO
(out)(err)
S = N/A
O = 198
T = TO
(out)(err)
S = N/A
O = 203
T = TO
(out)(err)
S = N/A
O = 163
T = TO
(out)(err)
S = N/A
O = 376
T = TO
(out)(err)
S = N/A
O = N/A
T = 238.15
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C900_4.wcnf S = OPT
O = 171
T = 78.84
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 171
T = 78.84
(out)(err)
S = N/A
O = 234
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 171
T = 88.30
(out)(err)
S = N/A
O = 218
T = TO
(out)(err)
S = OPT
O = 171
T = 236.88
(out)(err)
S = OPT
O = 171
T = 239.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 = 171
T = 1169.79
(out)(err)
S = OPT
O = 171
T = 129.76
(out)(err)
S = N/A
O = 206
T = TO
(out)(err)
S = N/A
O = 404
T = TO
(out)(err)
S = N/A
O = 329
T = TO
(out)(err)
S = N/A
O = 174
T = TO
(out)(err)
S = N/A
O = 442
T = TO
(out)(err)
S = N/A
O = N/A
T = 267.62
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C900_5.wcnf S = OPT
O = 175
T = 56.19
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 175
T = 58.28
(out)(err)
S = N/A
O = 225
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 175
T = 56.19
(out)(err)
S = N/A
O = 196
T = TO
(out)(err)
S = OPT
O = 175
T = 156.58
(out)(err)
S = OPT
O = 175
T = 158.52
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 175
T = 770.91
(out)(err)
S = OPT
O = 175
T = 115.88
(out)(err)
S = N/A
O = 205
T = TO
(out)(err)
S = N/A
O = 384
T = TO
(out)(err)
S = N/A
O = 351
T = TO
(out)(err)
S = N/A
O = 175
T = TO
(out)(err)
S = N/A
O = 397
T = TO
(out)(err)
S = N/A
O = N/A
T = 241.56
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C900_6.wcnf S = OPT
O = 174
T = 60.75
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 174
T = 86.49
(out)(err)
S = N/A
O = 276
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 174
T = 60.75
(out)(err)
S = N/A
O = 174
T = TO
(out)(err)
S = OPT
O = 174
T = 164.19
(out)(err)
S = OPT
O = 174
T = 170.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 = 174
T = 769.31
(out)(err)
S = OPT
O = 174
T = 106.05
(out)(err)
S = N/A
O = 197
T = TO
(out)(err)
S = N/A
O = 410
T = TO
(out)(err)
S = N/A
O = 222
T = TO
(out)(err)
S = N/A
O = 174
T = TO
(out)(err)
S = N/A
O = 400
T = TO
(out)(err)
S = N/A
O = N/A
T = 613.96
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C900_7.wcnf S = OPT
O = 194
T = 142.06
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 194
T = 142.06
(out)(err)
S = N/A
O = 246
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 194
T = 175.15
(out)(err)
S = N/A
O = 227
T = TO
(out)(err)
S = OPT
O = 194
T = 473.58
(out)(err)
S = OPT
O = 194
T = 476.56
(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 = 200
T = 1797.44
(out)(err)
S = OPT
O = 194
T = 241.77
(out)(err)
S = N/A
O = 223
T = TO
(out)(err)
S = N/A
O = 348
T = TO
(out)(err)
S = N/A
O = 369
T = TO
(out)(err)
S = N/A
O = 200
T = TO
(out)(err)
S = N/A
O = 411
T = TO
(out)(err)
S = N/A
O = N/A
T = 613.93
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C900_8.wcnf S = OPT
O = 179
T = 62.65
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 179
T = 62.65
(out)(err)
S = N/A
O = 276
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 179
T = 64.33
(out)(err)
S = N/A
O = 202
T = TO
(out)(err)
S = OPT
O = 179
T = 177.39
(out)(err)
S = OPT
O = 179
T = 176.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 = 179
T = 889.84
(out)(err)
S = OPT
O = 179
T = 126.64
(out)(err)
S = N/A
O = 203
T = TO
(out)(err)
S = N/A
O = 396
T = TO
(out)(err)
S = N/A
O = 430
T = TO
(out)(err)
S = N/A
O = 179
T = TO
(out)(err)
S = N/A
O = 443
T = TO
(out)(err)
S = N/A
O = N/A
T = 567.01
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
file_rwms_wcnf_L3_V70_C900_9.wcnf S = OPT
O = 181
T = 69.00
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 181
T = 69.00
(out)(err)
S = N/A
O = 229
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 181
T = 70.71
(out)(err)
S = N/A
O = 188
T = TO
(out)(err)
S = OPT
O = 181
T = 190.68
(out)(err)
S = OPT
O = 181
T = 191.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 = 181
T = 877.85
(out)(err)
S = OPT
O = 181
T = 139.65
(out)(err)
S = N/A
O = 208
T = TO
(out)(err)
S = N/A
O = 387
T = TO
(out)(err)
S = N/A
O = 411
T = TO
(out)(err)
S = N/A
O = 182
T = TO
(out)(err)
S = N/A
O = 487
T = TO
(out)(err)
S = N/A
O = N/A
T = 239.15
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)