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
TextBest solver column
TextOptimal solution with the best CPU time
TextOptimal solution and finished within the Time Out
TextOptimal solution and did not finish within the Time Out
TextTime Out
TextBuggy solution

Instance file name Best solver Sat4j ShinMaxSat WMaxSatz+ WMaxSatz09 WPM1 akmaxsat akmaxsat_ls iut_rr_ls iut_rr_rv wbo1.6
s2v100c1200_1.wcnf S = OPT
O = 865
T = 4.36
S = N/A
O = 1253
T = TO
(out)(err)
S = N/A
O = 1421
T = TO
(out)(err)
S = OPT
O = 865
T = 46.47
(out)(err)
S = OPT
O = 865
T = 44.27
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 865
T = 11.50
(out)(err)
S = OPT
O = 865
T = 4.36
(out)(err)
S = OPT
O = 865
T = 4.79
(out)(err)
S = OPT
O = 865
T = 4.67
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1200_2.wcnf S = OPT
O = 774
T = 3.31
S = N/A
O = 1100
T = TO
(out)(err)
S = N/A
O = 1403
T = TO
(out)(err)
S = OPT
O = 774
T = 27.92
(out)(err)
S = OPT
O = 774
T = 30.59
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 774
T = 8.47
(out)(err)
S = OPT
O = 774
T = 3.31
(out)(err)
S = OPT
O = 774
T = 3.69
(out)(err)
S = OPT
O = 774
T = 3.59
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1200_3.wcnf S = OPT
O = 933
T = 33.32
S = N/A
O = 1160
T = TO
(out)(err)
S = N/A
O = 1503
T = TO
(out)(err)
S = OPT
O = 933
T = 203.26
(out)(err)
S = OPT
O = 933
T = 204.33
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 933
T = 51.86
(out)(err)
S = OPT
O = 933
T = 33.32
(out)(err)
S = OPT
O = 933
T = 37.19
(out)(err)
S = OPT
O = 933
T = 36.27
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1200_4.wcnf S = OPT
O = 798
T = 3.45
S = N/A
O = 1214
T = TO
(out)(err)
S = N/A
O = 1438
T = TO
(out)(err)
S = OPT
O = 798
T = 17.17
(out)(err)
S = OPT
O = 798
T = 16.86
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 798
T = 7.02
(out)(err)
S = OPT
O = 798
T = 3.45
(out)(err)
S = OPT
O = 798
T = 3.90
(out)(err)
S = OPT
O = 798
T = 3.79
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1200_5.wcnf S = OPT
O = 876
T = 4.06
S = N/A
O = 1176
T = TO
(out)(err)
S = N/A
O = 1545
T = TO
(out)(err)
S = OPT
O = 876
T = 43.72
(out)(err)
S = OPT
O = 876
T = 44.83
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 876
T = 9.35
(out)(err)
S = OPT
O = 876
T = 4.06
(out)(err)
S = OPT
O = 876
T = 4.48
(out)(err)
S = OPT
O = 876
T = 4.37
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1200_6.wcnf S = OPT
O = 734
T = 0.67
S = N/A
O = 1011
T = TO
(out)(err)
S = N/A
O = 1328
T = TO
(out)(err)
S = OPT
O = 734
T = 2.92
(out)(err)
S = OPT
O = 734
T = 3.13
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 734
T = 1.13
(out)(err)
S = OPT
O = 734
T = 0.68
(out)(err)
S = OPT
O = 734
T = 0.69
(out)(err)
S = OPT
O = 734
T = 0.67
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1200_7.wcnf S = OPT
O = 800
T = 12.00
S = N/A
O = 1175
T = TO
(out)(err)
S = N/A
O = 1267
T = TO
(out)(err)
S = OPT
O = 800
T = 75.10
(out)(err)
S = OPT
O = 800
T = 72.15
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 800
T = 23.48
(out)(err)
S = OPT
O = 800
T = 12.00
(out)(err)
S = OPT
O = 800
T = 13.46
(out)(err)
S = OPT
O = 800
T = 12.97
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1200_8.wcnf S = OPT
O = 962
T = 37.30
S = N/A
O = 1300
T = TO
(out)(err)
S = N/A
O = 1436
T = TO
(out)(err)
S = OPT
O = 962
T = 350.85
(out)(err)
S = OPT
O = 962
T = 349.72
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 962
T = 53.12
(out)(err)
S = OPT
O = 962
T = 37.30
(out)(err)
S = OPT
O = 962
T = 41.10
(out)(err)
S = OPT
O = 962
T = 40.02
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1300_1.wcnf S = OPT
O = 971
T = 9.58
S = N/A
O = 1314
T = TO
(out)(err)
S = N/A
O = 1691
T = TO
(out)(err)
S = OPT
O = 971
T = 72.36
(out)(err)
S = OPT
O = 971
T = 68.18
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 971
T = 11.02
(out)(err)
S = OPT
O = 971
T = 9.58
(out)(err)
S = OPT
O = 971
T = 10.53
(out)(err)
S = OPT
O = 971
T = 10.21
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1300_2.wcnf S = OPT
O = 930
T = 14.29
S = N/A
O = 1313
T = TO
(out)(err)
S = N/A
O = 1451
T = TO
(out)(err)
S = OPT
O = 930
T = 234.91
(out)(err)
S = OPT
O = 930
T = 237.03
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 930
T = 20.90
(out)(err)
S = OPT
O = 930
T = 14.29
(out)(err)
S = OPT
O = 930
T = 15.96
(out)(err)
S = OPT
O = 930
T = 15.26
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1300_3.wcnf S = OPT
O = 925
T = 4.52
S = N/A
O = 1178
T = TO
(out)(err)
S = N/A
O = 1511
T = TO
(out)(err)
S = OPT
O = 925
T = 41.36
(out)(err)
S = OPT
O = 925
T = 42.67
(out)(err)
S = N/A
O = N/A
T = 326.68
(out)(err)
S = OPT
O = 925
T = 12.34
(out)(err)
S = OPT
O = 925
T = 4.52
(out)(err)
S = OPT
O = 925
T = 5.05
(out)(err)
S = OPT
O = 925
T = 4.85
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1300_4.wcnf S = OPT
O = 970
T = 8.56
S = N/A
O = 1402
T = TO
(out)(err)
S = N/A
O = 1571
T = TO
(out)(err)
S = OPT
O = 970
T = 116.91
(out)(err)
S = OPT
O = 970
T = 116.91
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 970
T = 18.41
(out)(err)
S = OPT
O = 970
T = 8.56
(out)(err)
S = OPT
O = 970
T = 9.51
(out)(err)
S = OPT
O = 970
T = 9.24
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1300_5.wcnf S = OPT
O = 962
T = 16.74
S = N/A
O = 1258
T = TO
(out)(err)
S = N/A
O = 1444
T = TO
(out)(err)
S = OPT
O = 962
T = 217.79
(out)(err)
S = OPT
O = 962
T = 226.19
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 962
T = 39.34
(out)(err)
S = OPT
O = 962
T = 16.74
(out)(err)
S = OPT
O = 962
T = 18.37
(out)(err)
S = OPT
O = 962
T = 18.26
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1300_6.wcnf S = OPT
O = 933
T = 5.72
S = N/A
O = 1328
T = TO
(out)(err)
S = N/A
O = 1468
T = TO
(out)(err)
S = OPT
O = 933
T = 48.28
(out)(err)
S = OPT
O = 933
T = 50.81
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 933
T = 6.49
(out)(err)
S = OPT
O = 933
T = 5.72
(out)(err)
S = OPT
O = 933
T = 6.31
(out)(err)
S = OPT
O = 933
T = 6.16
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1300_7.wcnf S = OPT
O = 877
T = 4.20
S = N/A
O = 1184
T = TO
(out)(err)
S = N/A
O = 1410
T = TO
(out)(err)
S = OPT
O = 877
T = 49.18
(out)(err)
S = OPT
O = 877
T = 48.22
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 877
T = 14.15
(out)(err)
S = OPT
O = 877
T = 4.20
(out)(err)
S = OPT
O = 877
T = 4.70
(out)(err)
S = OPT
O = 877
T = 4.55
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1300_8.wcnf S = OPT
O = 941
T = 10.34
S = N/A
O = 1270
T = TO
(out)(err)
S = N/A
O = 1395
T = TO
(out)(err)
S = OPT
O = 941
T = 157.36
(out)(err)
S = OPT
O = 941
T = 160.63
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 941
T = 31.00
(out)(err)
S = OPT
O = 941
T = 10.34
(out)(err)
S = OPT
O = 941
T = 11.45
(out)(err)
S = OPT
O = 941
T = 11.17
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1400_1.wcnf S = OPT
O = 1019
T = 23.65
S = N/A
O = 1364
T = TO
(out)(err)
S = N/A
O = 1477
T = TO
(out)(err)
S = OPT
O = 1019
T = 167.25
(out)(err)
S = OPT
O = 1019
T = 168.12
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1019
T = 44.12
(out)(err)
S = OPT
O = 1019
T = 23.65
(out)(err)
S = OPT
O = 1019
T = 26.01
(out)(err)
S = OPT
O = 1019
T = 25.34
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1400_2.wcnf S = OPT
O = 1002
T = 11.50
S = N/A
O = 1289
T = TO
(out)(err)
S = N/A
O = 1546
T = TO
(out)(err)
S = OPT
O = 1002
T = 135.93
(out)(err)
S = OPT
O = 1002
T = 131.86
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1002
T = 17.14
(out)(err)
S = OPT
O = 1002
T = 11.50
(out)(err)
S = OPT
O = 1002
T = 12.60
(out)(err)
S = OPT
O = 1002
T = 12.25
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1400_3.wcnf S = OPT
O = 1020
T = 20.57
S = N/A
O = 1288
T = TO
(out)(err)
S = N/A
O = 1790
T = TO
(out)(err)
S = OPT
O = 1020
T = 281.14
(out)(err)
S = OPT
O = 1020
T = 272.95
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1020
T = 23.78
(out)(err)
S = OPT
O = 1020
T = 20.57
(out)(err)
S = OPT
O = 1020
T = 22.71
(out)(err)
S = OPT
O = 1020
T = 22.33
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1400_4.wcnf S = OPT
O = 1094
T = 44.31
S = N/A
O = 1409
T = TO
(out)(err)
S = N/A
O = 1601
T = TO
(out)(err)
S = OPT
O = 1094
T = 329.14
(out)(err)
S = OPT
O = 1094
T = 358.23
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1094
T = 54.04
(out)(err)
S = OPT
O = 1094
T = 44.31
(out)(err)
S = OPT
O = 1094
T = 47.78
(out)(err)
S = OPT
O = 1094
T = 47.17
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1400_5.wcnf S = OPT
O = 1018
T = 11.27
S = N/A
O = 1340
T = TO
(out)(err)
S = N/A
O = 1597
T = TO
(out)(err)
S = OPT
O = 1018
T = 167.93
(out)(err)
S = OPT
O = 1018
T = 164.89
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1018
T = 21.96
(out)(err)
S = OPT
O = 1018
T = 11.27
(out)(err)
S = OPT
O = 1018
T = 11.83
(out)(err)
S = OPT
O = 1018
T = 11.51
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1400_6.wcnf S = OPT
O = 997
T = 2.81
S = N/A
O = 1390
T = TO
(out)(err)
S = N/A
O = 1681
T = TO
(out)(err)
S = OPT
O = 997
T = 33.66
(out)(err)
S = OPT
O = 997
T = 33.66
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 997
T = 5.38
(out)(err)
S = OPT
O = 997
T = 2.81
(out)(err)
S = OPT
O = 997
T = 3.01
(out)(err)
S = OPT
O = 997
T = 2.96
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1400_7.wcnf S = OPT
O = 1001
T = 38.93
S = N/A
O = 1372
T = TO
(out)(err)
S = N/A
O = 1583
T = TO
(out)(err)
S = OPT
O = 1001
T = 246.35
(out)(err)
S = OPT
O = 1001
T = 249.56
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1001
T = 45.80
(out)(err)
S = OPT
O = 1001
T = 38.93
(out)(err)
S = OPT
O = 1001
T = 42.60
(out)(err)
S = OPT
O = 1001
T = 41.20
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1400_8.wcnf S = OPT
O = 1084
T = 24.73
S = N/A
O = 1334
T = TO
(out)(err)
S = N/A
O = 1682
T = TO
(out)(err)
S = OPT
O = 1084
T = 166.95
(out)(err)
S = OPT
O = 1084
T = 302.21
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1084
T = 38.17
(out)(err)
S = OPT
O = 1084
T = 24.73
(out)(err)
S = OPT
O = 1084
T = 26.97
(out)(err)
S = OPT
O = 1084
T = 26.32
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1500_1.wcnf S = OPT
O = 1077
T = 14.52
S = N/A
O = 1409
T = TO
(out)(err)
S = N/A
O = 1568
T = TO
(out)(err)
S = OPT
O = 1077
T = 124.55
(out)(err)
S = OPT
O = 1077
T = 123.90
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1077
T = 29.86
(out)(err)
S = OPT
O = 1077
T = 14.52
(out)(err)
S = OPT
O = 1077
T = 15.94
(out)(err)
S = OPT
O = 1077
T = 15.52
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1500_2.wcnf S = OPT
O = 1125
T = 18.40
S = N/A
O = 1456
T = TO
(out)(err)
S = N/A
O = 1781
T = TO
(out)(err)
S = OPT
O = 1125
T = 303.91
(out)(err)
S = OPT
O = 1125
T = 304.24
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1125
T = 22.45
(out)(err)
S = OPT
O = 1125
T = 18.40
(out)(err)
S = OPT
O = 1125
T = 19.97
(out)(err)
S = OPT
O = 1125
T = 19.41
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1500_3.wcnf S = OPT
O = 1151
T = 39.48
S = N/A
O = 1378
T = TO
(out)(err)
S = N/A
O = 1847
T = TO
(out)(err)
S = OPT
O = 1151
T = 292.50
(out)(err)
S = OPT
O = 1151
T = 291.38
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1151
T = 43.16
(out)(err)
S = OPT
O = 1151
T = 39.48
(out)(err)
S = OPT
O = 1151
T = 43.48
(out)(err)
S = OPT
O = 1151
T = 42.02
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1500_4.wcnf S = OPT
O = 1072
T = 14.50
S = N/A
O = 1462
T = TO
(out)(err)
S = N/A
O = 1807
T = TO
(out)(err)
S = OPT
O = 1072
T = 302.51
(out)(err)
S = OPT
O = 1072
T = 304.62
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1072
T = 73.25
(out)(err)
S = OPT
O = 1072
T = 14.50
(out)(err)
S = OPT
O = 1072
T = 15.97
(out)(err)
S = OPT
O = 1072
T = 15.61
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1500_5.wcnf S = OPT
O = 1151
T = 32.12
S = N/A
O = 1434
T = TO
(out)(err)
S = N/A
O = 1848
T = TO
(out)(err)
S = OPT
O = 1151
T = 348.99
(out)(err)
S = OPT
O = 1151
T = 393.05
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1151
T = 39.72
(out)(err)
S = OPT
O = 1151
T = 32.12
(out)(err)
S = OPT
O = 1151
T = 34.20
(out)(err)
S = OPT
O = 1151
T = 33.67
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1500_6.wcnf S = OPT
O = 1225
T = 39.32
S = N/A
O = 1624
T = TO
(out)(err)
S = N/A
O = 2010
T = TO
(out)(err)
S = OPT
O = 1225
T = 663.22
(out)(err)
S = OPT
O = 1225
T = 698.29
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1225
T = 79.13
(out)(err)
S = OPT
O = 1225
T = 39.32
(out)(err)
S = OPT
O = 1225
T = 42.57
(out)(err)
S = OPT
O = 1225
T = 41.46
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1500_7.wcnf S = OPT
O = 1186
T = 24.84
S = N/A
O = 1577
T = TO
(out)(err)
S = N/A
O = 2017
T = TO
(out)(err)
S = OPT
O = 1186
T = 246.90
(out)(err)
S = OPT
O = 1186
T = 247.75
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1186
T = 26.93
(out)(err)
S = OPT
O = 1186
T = 24.84
(out)(err)
S = OPT
O = 1186
T = 26.99
(out)(err)
S = OPT
O = 1186
T = 26.23
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1500_8.wcnf S = OPT
O = 1217
T = 34.24
S = N/A
O = 1512
T = TO
(out)(err)
S = N/A
O = 1800
T = TO
(out)(err)
S = OPT
O = 1217
T = 1062.06
(out)(err)
S = OPT
O = 1217
T = 1084.53
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1217
T = 78.45
(out)(err)
S = OPT
O = 1217
T = 34.24
(out)(err)
S = OPT
O = 1217
T = 37.03
(out)(err)
S = OPT
O = 1217
T = 36.47
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1600_1.wcnf S = OPT
O = 1230
T = 14.38
S = N/A
O = 1639
T = TO
(out)(err)
S = N/A
O = 2063
T = TO
(out)(err)
S = OPT
O = 1230
T = 253.37
(out)(err)
S = OPT
O = 1230
T = 248.23
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1230
T = 26.50
(out)(err)
S = OPT
O = 1230
T = 14.38
(out)(err)
S = OPT
O = 1230
T = 15.43
(out)(err)
S = OPT
O = 1230
T = 15.22
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1600_2.wcnf S = OPT
O = 1265
T = 140.39
S = N/A
O = 1534
T = TO
(out)(err)
S = N/A
O = 1840
T = TO
(out)(err)
S = N/A
O = 1265
T = TO
(out)(err)
S = N/A
O = 1265
T = TO
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1265
T = 215.72
(out)(err)
S = OPT
O = 1265
T = 140.39
(out)(err)
S = OPT
O = 1265
T = 149.74
(out)(err)
S = OPT
O = 1265
T = 144.96
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1600_3.wcnf S = OPT
O = 1309
T = 80.81
S = N/A
O = 1657
T = TO
(out)(err)
S = N/A
O = 1862
T = TO
(out)(err)
S = OPT
O = 1309
T = 1037.61
(out)(err)
S = OPT
O = 1309
T = 1051.02
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1309
T = 156.60
(out)(err)
S = OPT
O = 1309
T = 80.81
(out)(err)
S = OPT
O = 1309
T = 87.03
(out)(err)
S = OPT
O = 1309
T = 84.42
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1600_4.wcnf S = OPT
O = 1267
T = 41.43
S = N/A
O = 1693
T = TO
(out)(err)
S = N/A
O = 1821
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 = OPT
O = 1267
T = 183.60
(out)(err)
S = OPT
O = 1267
T = 41.43
(out)(err)
S = OPT
O = 1267
T = 44.59
(out)(err)
S = OPT
O = 1267
T = 43.50
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v100c1600_5.wcnf S = OPT
O = 1298
T = 35.15
S = N/A
O = 1711
T = TO
(out)(err)
S = N/A
O = 1795
T = TO
(out)(err)
S = OPT
O = 1298
T = 443.68
(out)(err)
S = OPT
O = 1298
T = 445.48
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1298
T = 51.67
(out)(err)
S = OPT
O = 1298
T = 35.15
(out)(err)
S = OPT
O = 1298
T = 38.33
(out)(err)
S = OPT
O = 1298
T = 37.23
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1600_6.wcnf S = OPT
O = 1190
T = 11.35
S = N/A
O = 1754
T = TO
(out)(err)
S = N/A
O = 1805
T = TO
(out)(err)
S = OPT
O = 1190
T = 298.11
(out)(err)
S = OPT
O = 1190
T = 299.29
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1190
T = 21.11
(out)(err)
S = OPT
O = 1190
T = 11.35
(out)(err)
S = OPT
O = 1190
T = 12.37
(out)(err)
S = OPT
O = 1190
T = 12.05
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1600_7.wcnf S = OPT
O = 1243
T = 64.53
S = N/A
O = 1584
T = TO
(out)(err)
S = N/A
O = 1740
T = 432.99
(out)(err)
S = OPT
O = 1243
T = 1504.72
(out)(err)
S = OPT
O = 1243
T = 1650.48
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1243
T = 132.94
(out)(err)
S = OPT
O = 1243
T = 64.53
(out)(err)
S = OPT
O = 1243
T = 70.56
(out)(err)
S = OPT
O = 1243
T = 68.45
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v100c1600_8.wcnf S = OPT
O = 1184
T = 4.25
S = N/A
O = 1648
T = TO
(out)(err)
S = N/A
O = 1923
T = 443.71
(out)(err)
S = OPT
O = 1184
T = 83.56
(out)(err)
S = OPT
O = 1184
T = 84.45
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1184
T = 11.54
(out)(err)
S = OPT
O = 1184
T = 4.25
(out)(err)
S = OPT
O = 1184
T = 4.55
(out)(err)
S = OPT
O = 1184
T = 4.46
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1200_1.wcnf S = OPT
O = 840
T = 26.62
S = N/A
O = 1067
T = TO
(out)(err)
S = N/A
O = 1542
T = TO
(out)(err)
S = OPT
O = 840
T = 205.19
(out)(err)
S = OPT
O = 840
T = 202.29
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 840
T = 54.60
(out)(err)
S = OPT
O = 840
T = 26.62
(out)(err)
S = OPT
O = 840
T = 29.46
(out)(err)
S = OPT
O = 840
T = 29.04
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1200_2.wcnf S = OPT
O = 803
T = 5.84
S = N/A
O = 1083
T = TO
(out)(err)
S = N/A
O = 1570
T = TO
(out)(err)
S = OPT
O = 803
T = 19.56
(out)(err)
S = OPT
O = 803
T = 19.50
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 803
T = 7.58
(out)(err)
S = OPT
O = 803
T = 5.84
(out)(err)
S = OPT
O = 803
T = 6.50
(out)(err)
S = OPT
O = 803
T = 6.32
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1200_3.wcnf S = OPT
O = 834
T = 13.53
S = N/A
O = 1186
T = TO
(out)(err)
S = N/A
O = 1569
T = TO
(out)(err)
S = OPT
O = 834
T = 79.74
(out)(err)
S = OPT
O = 834
T = 81.08
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 834
T = 26.93
(out)(err)
S = OPT
O = 834
T = 13.53
(out)(err)
S = OPT
O = 834
T = 15.90
(out)(err)
S = OPT
O = 834
T = 15.50
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1200_4.wcnf S = OPT
O = 811
T = 10.68
S = N/A
O = 1207
T = TO
(out)(err)
S = N/A
O = 1537
T = TO
(out)(err)
S = OPT
O = 811
T = 40.90
(out)(err)
S = OPT
O = 811
T = 36.03
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 811
T = 18.99
(out)(err)
S = OPT
O = 811
T = 10.68
(out)(err)
S = OPT
O = 811
T = 12.11
(out)(err)
S = OPT
O = 811
T = 11.66
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1200_5.wcnf S = OPT
O = 850
T = 39.39
S = N/A
O = 1074
T = TO
(out)(err)
S = N/A
O = 1603
T = TO
(out)(err)
S = OPT
O = 850
T = 441.79
(out)(err)
S = OPT
O = 850
T = 458.75
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 850
T = 51.73
(out)(err)
S = OPT
O = 850
T = 39.39
(out)(err)
S = OPT
O = 850
T = 43.83
(out)(err)
S = OPT
O = 850
T = 43.19
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1200_6.wcnf S = OPT
O = 784
T = 16.41
S = N/A
O = 1047
T = TO
(out)(err)
S = N/A
O = 1430
T = TO
(out)(err)
S = OPT
O = 784
T = 249.50
(out)(err)
S = OPT
O = 784
T = 250.69
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 784
T = 63.92
(out)(err)
S = OPT
O = 784
T = 16.41
(out)(err)
S = OPT
O = 784
T = 18.25
(out)(err)
S = OPT
O = 784
T = 17.80
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1200_7.wcnf S = OPT
O = 747
T = 2.93
S = N/A
O = 1055
T = TO
(out)(err)
S = N/A
O = 1438
T = TO
(out)(err)
S = OPT
O = 747
T = 12.53
(out)(err)
S = OPT
O = 747
T = 12.53
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 747
T = 4.93
(out)(err)
S = OPT
O = 747
T = 2.93
(out)(err)
S = OPT
O = 747
T = 3.30
(out)(err)
S = OPT
O = 747
T = 3.20
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1200_8.wcnf S = OPT
O = 813
T = 11.23
S = N/A
O = 1230
T = TO
(out)(err)
S = N/A
O = 1546
T = TO
(out)(err)
S = OPT
O = 813
T = 44.43
(out)(err)
S = OPT
O = 813
T = 43.75
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 813
T = 12.32
(out)(err)
S = OPT
O = 813
T = 11.23
(out)(err)
S = OPT
O = 813
T = 12.58
(out)(err)
S = OPT
O = 813
T = 12.15
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1300_1.wcnf S = OPT
O = 890
T = 8.79
S = N/A
O = 1096
T = TO
(out)(err)
S = N/A
O = 1884
T = TO
(out)(err)
S = OPT
O = 890
T = 46.32
(out)(err)
S = OPT
O = 890
T = 44.98
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 890
T = 11.45
(out)(err)
S = OPT
O = 890
T = 8.79
(out)(err)
S = OPT
O = 890
T = 10.03
(out)(err)
S = OPT
O = 890
T = 9.43
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1300_2.wcnf S = OPT
O = 847
T = 3.75
S = N/A
O = 1108
T = TO
(out)(err)
S = N/A
O = 1631
T = TO
(out)(err)
S = OPT
O = 847
T = 40.43
(out)(err)
S = OPT
O = 847
T = 33.59
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 847
T = 9.57
(out)(err)
S = OPT
O = 847
T = 3.75
(out)(err)
S = OPT
O = 847
T = 4.30
(out)(err)
S = OPT
O = 847
T = 4.05
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1300_3.wcnf S = OPT
O = 941
T = 10.45
S = N/A
O = 1338
T = TO
(out)(err)
S = N/A
O = 1597
T = TO
(out)(err)
S = OPT
O = 941
T = 104.44
(out)(err)
S = OPT
O = 941
T = 104.32
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 941
T = 28.84
(out)(err)
S = OPT
O = 941
T = 10.45
(out)(err)
S = OPT
O = 941
T = 11.64
(out)(err)
S = OPT
O = 941
T = 11.49
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1300_4.wcnf S = OPT
O = 939
T = 17.92
S = N/A
O = 1264
T = TO
(out)(err)
S = N/A
O = 1698
T = TO
(out)(err)
S = OPT
O = 939
T = 169.87
(out)(err)
S = OPT
O = 939
T = 151.64
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 939
T = 29.50
(out)(err)
S = OPT
O = 939
T = 17.92
(out)(err)
S = OPT
O = 939
T = 20.18
(out)(err)
S = OPT
O = 939
T = 19.68
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1300_5.wcnf S = OPT
O = 949
T = 45.22
S = N/A
O = 1475
T = TO
(out)(err)
S = N/A
O = 1715
T = TO
(out)(err)
S = OPT
O = 949
T = 439.24
(out)(err)
S = OPT
O = 949
T = 419.29
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 949
T = 111.85
(out)(err)
S = OPT
O = 949
T = 45.22
(out)(err)
S = OPT
O = 949
T = 50.48
(out)(err)
S = OPT
O = 949
T = 49.93
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1300_6.wcnf S = OPT
O = 865
T = 5.39
S = N/A
O = 1192
T = TO
(out)(err)
S = N/A
O = 1720
T = TO
(out)(err)
S = OPT
O = 865
T = 64.07
(out)(err)
S = OPT
O = 865
T = 59.18
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 865
T = 18.02
(out)(err)
S = OPT
O = 865
T = 5.39
(out)(err)
S = OPT
O = 865
T = 6.06
(out)(err)
S = OPT
O = 865
T = 5.90
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1300_7.wcnf S = OPT
O = 879
T = 4.76
S = N/A
O = 1167
T = TO
(out)(err)
S = N/A
O = 1767
T = TO
(out)(err)
S = OPT
O = 879
T = 34.70
(out)(err)
S = OPT
O = 879
T = 36.17
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 879
T = 10.64
(out)(err)
S = OPT
O = 879
T = 4.76
(out)(err)
S = OPT
O = 879
T = 5.33
(out)(err)
S = OPT
O = 879
T = 5.14
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1300_8.wcnf S = OPT
O = 868
T = 10.65
S = N/A
O = 1188
T = TO
(out)(err)
S = N/A
O = 1710
T = TO
(out)(err)
S = OPT
O = 868
T = 49.34
(out)(err)
S = OPT
O = 868
T = 50.64
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 868
T = 12.95
(out)(err)
S = OPT
O = 868
T = 10.65
(out)(err)
S = OPT
O = 868
T = 12.07
(out)(err)
S = OPT
O = 868
T = 11.93
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1400_1.wcnf S = OPT
O = 1028
T = 24.73
S = N/A
O = 1283
T = TO
(out)(err)
S = N/A
O = 1829
T = TO
(out)(err)
S = OPT
O = 1028
T = 107.27
(out)(err)
S = OPT
O = 1028
T = 109.00
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1028
T = 33.72
(out)(err)
S = OPT
O = 1028
T = 24.73
(out)(err)
S = OPT
O = 1028
T = 28.25
(out)(err)
S = OPT
O = 1028
T = 27.56
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1400_2.wcnf S = OPT
O = 1008
T = 32.41
S = N/A
O = 1395
T = TO
(out)(err)
S = N/A
O = 2035
T = TO
(out)(err)
S = OPT
O = 1008
T = 585.94
(out)(err)
S = OPT
O = 1008
T = 554.95
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1008
T = 125.33
(out)(err)
S = OPT
O = 1008
T = 32.41
(out)(err)
S = OPT
O = 1008
T = 35.65
(out)(err)
S = OPT
O = 1008
T = 34.95
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1400_3.wcnf S = OPT
O = 983
T = 7.07
S = N/A
O = 1339
T = TO
(out)(err)
S = N/A
O = 1959
T = TO
(out)(err)
S = OPT
O = 983
T = 41.42
(out)(err)
S = OPT
O = 983
T = 40.01
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 983
T = 17.50
(out)(err)
S = OPT
O = 983
T = 7.07
(out)(err)
S = OPT
O = 983
T = 7.93
(out)(err)
S = OPT
O = 983
T = 7.67
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1400_4.wcnf S = OPT
O = 1007
T = 47.04
S = N/A
O = 1234
T = TO
(out)(err)
S = N/A
O = 1837
T = TO
(out)(err)
S = OPT
O = 1007
T = 285.51
(out)(err)
S = OPT
O = 1007
T = 291.27
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1007
T = 60.19
(out)(err)
S = OPT
O = 1007
T = 47.04
(out)(err)
S = OPT
O = 1007
T = 52.20
(out)(err)
S = OPT
O = 1007
T = 51.37
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1400_5.wcnf S = OPT
O = 1108
T = 284.10
S = N/A
O = 1494
T = TO
(out)(err)
S = N/A
O = 1825
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 = OPT
O = 1108
T = 295.08
(out)(err)
S = OPT
O = 1108
T = 284.10
(out)(err)
S = OPT
O = 1108
T = 315.87
(out)(err)
S = OPT
O = 1108
T = 303.76
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1400_6.wcnf S = OPT
O = 959
T = 10.19
S = N/A
O = 1359
T = TO
(out)(err)
S = N/A
O = 1519
T = TO
(out)(err)
S = OPT
O = 959
T = 49.22
(out)(err)
S = OPT
O = 959
T = 50.06
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 959
T = 12.39
(out)(err)
S = OPT
O = 959
T = 10.19
(out)(err)
S = OPT
O = 959
T = 11.75
(out)(err)
S = OPT
O = 959
T = 11.36
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1400_7.wcnf S = OPT
O = 1040
T = 53.84
S = N/A
O = 1404
T = TO
(out)(err)
S = N/A
O = 1830
T = TO
(out)(err)
S = OPT
O = 1040
T = 565.79
(out)(err)
S = OPT
O = 1040
T = 589.55
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1040
T = 102.83
(out)(err)
S = OPT
O = 1040
T = 53.84
(out)(err)
S = OPT
O = 1040
T = 59.94
(out)(err)
S = OPT
O = 1040
T = 58.31
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1400_8.wcnf S = OPT
O = 1025
T = 39.77
S = N/A
O = 1418
T = TO
(out)(err)
S = N/A
O = 2000
T = TO
(out)(err)
S = OPT
O = 1025
T = 293.47
(out)(err)
S = OPT
O = 1025
T = 286.64
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1025
T = 49.82
(out)(err)
S = OPT
O = 1025
T = 39.77
(out)(err)
S = OPT
O = 1025
T = 44.76
(out)(err)
S = OPT
O = 1025
T = 43.98
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1500_1.wcnf S = OPT
O = 1119
T = 41.70
S = N/A
O = 1512
T = TO
(out)(err)
S = N/A
O = 2057
T = TO
(out)(err)
S = OPT
O = 1119
T = 303.95
(out)(err)
S = OPT
O = 1119
T = 302.61
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1119
T = 170.98
(out)(err)
S = OPT
O = 1119
T = 41.70
(out)(err)
S = OPT
O = 1119
T = 46.07
(out)(err)
S = OPT
O = 1119
T = 45.12
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1500_2.wcnf S = OPT
O = 1136
T = 57.70
S = N/A
O = 1527
T = TO
(out)(err)
S = N/A
O = 1877
T = TO
(out)(err)
S = OPT
O = 1136
T = 423.69
(out)(err)
S = OPT
O = 1136
T = 445.80
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1136
T = 185.63
(out)(err)
S = OPT
O = 1136
T = 57.70
(out)(err)
S = OPT
O = 1136
T = 64.87
(out)(err)
S = OPT
O = 1136
T = 62.74
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1500_3.wcnf S = OPT
O = 1062
T = 11.47
S = N/A
O = 1329
T = TO
(out)(err)
S = N/A
O = 1815
T = 490.72
(out)(err)
S = OPT
O = 1062
T = 58.84
(out)(err)
S = OPT
O = 1062
T = 59.50
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1062
T = 20.97
(out)(err)
S = OPT
O = 1062
T = 11.47
(out)(err)
S = OPT
O = 1062
T = 12.77
(out)(err)
S = OPT
O = 1062
T = 12.47
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1500_4.wcnf S = OPT
O = 1041
T = 6.07
S = N/A
O = 1437
T = TO
(out)(err)
S = N/A
O = 1946
T = TO
(out)(err)
S = OPT
O = 1041
T = 41.45
(out)(err)
S = OPT
O = 1041
T = 48.00
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1041
T = 9.79
(out)(err)
S = OPT
O = 1041
T = 6.07
(out)(err)
S = OPT
O = 1041
T = 6.77
(out)(err)
S = OPT
O = 1041
T = 6.54
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1500_5.wcnf S = OPT
O = 1125
T = 8.41
S = N/A
O = 1563
T = TO
(out)(err)
S = N/A
O = 1869
T = TO
(out)(err)
S = OPT
O = 1125
T = 117.45
(out)(err)
S = OPT
O = 1125
T = 119.19
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1125
T = 28.94
(out)(err)
S = OPT
O = 1125
T = 8.41
(out)(err)
S = OPT
O = 1125
T = 9.23
(out)(err)
S = OPT
O = 1125
T = 8.99
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1500_6.wcnf S = OPT
O = 1113
T = 39.00
S = N/A
O = 1500
T = TO
(out)(err)
S = N/A
O = 1842
T = TO
(out)(err)
S = OPT
O = 1113
T = 243.88
(out)(err)
S = OPT
O = 1113
T = 369.64
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1113
T = 73.76
(out)(err)
S = OPT
O = 1113
T = 39.00
(out)(err)
S = OPT
O = 1113
T = 43.53
(out)(err)
S = OPT
O = 1113
T = 41.99
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1500_7.wcnf S = OPT
O = 1163
T = 109.31
S = N/A
O = 1501
T = TO
(out)(err)
S = N/A
O = 2039
T = TO
(out)(err)
S = OPT
O = 1163
T = 814.84
(out)(err)
S = OPT
O = 1163
T = 864.27
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1163
T = 146.67
(out)(err)
S = OPT
O = 1163
T = 109.31
(out)(err)
S = OPT
O = 1163
T = 122.15
(out)(err)
S = OPT
O = 1163
T = 119.36
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1500_8.wcnf S = OPT
O = 1097
T = 7.08
S = N/A
O = 1649
T = TO
(out)(err)
S = N/A
O = 1978
T = TO
(out)(err)
S = OPT
O = 1097
T = 115.86
(out)(err)
S = OPT
O = 1097
T = 109.84
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1097
T = 18.31
(out)(err)
S = OPT
O = 1097
T = 7.08
(out)(err)
S = OPT
O = 1097
T = 7.86
(out)(err)
S = OPT
O = 1097
T = 7.60
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1600_1.wcnf S = OPT
O = 1190
T = 13.32
S = N/A
O = 1579
T = TO
(out)(err)
S = N/A
O = 1971
T = 457.07
(out)(err)
S = OPT
O = 1190
T = 156.47
(out)(err)
S = OPT
O = 1190
T = 162.73
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1190
T = 15.59
(out)(err)
S = OPT
O = 1190
T = 13.32
(out)(err)
S = OPT
O = 1190
T = 14.96
(out)(err)
S = OPT
O = 1190
T = 14.26
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1600_2.wcnf S = OPT
O = 1227
T = 88.91
S = N/A
O = 1684
T = TO
(out)(err)
S = N/A
O = 1890
T = TO
(out)(err)
S = OPT
O = 1227
T = 860.57
(out)(err)
S = OPT
O = 1227
T = 892.50
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1227
T = 144.38
(out)(err)
S = OPT
O = 1227
T = 88.91
(out)(err)
S = OPT
O = 1227
T = 98.93
(out)(err)
S = OPT
O = 1227
T = 96.07
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1600_3.wcnf S = OPT
O = 1224
T = 71.42
S = N/A
O = 1672
T = TO
(out)(err)
S = N/A
O = 2301
T = 474.25
(out)(err)
S = OPT
O = 1224
T = 938.35
(out)(err)
S = OPT
O = 1224
T = 950.62
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1224
T = 111.67
(out)(err)
S = OPT
O = 1224
T = 71.42
(out)(err)
S = OPT
O = 1224
T = 76.35
(out)(err)
S = OPT
O = 1224
T = 74.58
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1600_4.wcnf S = OPT
O = 1264
T = 178.24
S = N/A
O = 1810
T = TO
(out)(err)
S = N/A
O = 2195
T = TO
(out)(err)
S = OPT
O = 1264
T = 1767.71
(out)(err)
S = OPT
O = 1264
T = 1783.97
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1264
T = 288.50
(out)(err)
S = OPT
O = 1264
T = 178.24
(out)(err)
S = OPT
O = 1264
T = 195.34
(out)(err)
S = OPT
O = 1264
T = 189.14
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1600_5.wcnf S = OPT
O = 1252
T = 76.27
S = N/A
O = 1597
T = TO
(out)(err)
S = N/A
O = 2266
T = TO
(out)(err)
S = OPT
O = 1252
T = 1132.86
(out)(err)
S = OPT
O = 1252
T = 1150.97
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1252
T = 123.33
(out)(err)
S = OPT
O = 1252
T = 76.27
(out)(err)
S = OPT
O = 1252
T = 83.97
(out)(err)
S = OPT
O = 1252
T = 82.80
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1600_6.wcnf S = OPT
O = 1246
T = 31.11
S = N/A
O = 1592
T = TO
(out)(err)
S = N/A
O = 2423
T = TO
(out)(err)
S = OPT
O = 1246
T = 555.71
(out)(err)
S = OPT
O = 1246
T = 576.80
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1246
T = 51.46
(out)(err)
S = OPT
O = 1246
T = 31.11
(out)(err)
S = OPT
O = 1246
T = 32.87
(out)(err)
S = OPT
O = 1246
T = 32.14
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v120c1600_7.wcnf S = OPT
O = 1159
T = 11.94
S = N/A
O = 1588
T = TO
(out)(err)
S = N/A
O = 2316
T = TO
(out)(err)
S = OPT
O = 1159
T = 73.94
(out)(err)
S = OPT
O = 1159
T = 72.83
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1159
T = 13.85
(out)(err)
S = OPT
O = 1159
T = 11.94
(out)(err)
S = OPT
O = 1159
T = 13.41
(out)(err)
S = OPT
O = 1159
T = 13.01
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v120c1600_8.wcnf S = OPT
O = 1150
T = 5.31
S = N/A
O = 1592
T = TO
(out)(err)
S = N/A
O = 2041
T = TO
(out)(err)
S = OPT
O = 1150
T = 159.35
(out)(err)
S = OPT
O = 1150
T = 164.71
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1150
T = 22.25
(out)(err)
S = OPT
O = 1150
T = 5.31
(out)(err)
S = OPT
O = 1150
T = 5.92
(out)(err)
S = OPT
O = 1150
T = 5.83
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1200_1.wcnf S = OPT
O = 780
T = 59.52
S = N/A
O = 1052
T = TO
(out)(err)
S = N/A
O = 1624
T = TO
(out)(err)
S = OPT
O = 780
T = 285.33
(out)(err)
S = OPT
O = 780
T = 306.29
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 780
T = 110.36
(out)(err)
S = OPT
O = 780
T = 59.52
(out)(err)
S = OPT
O = 780
T = 68.08
(out)(err)
S = OPT
O = 780
T = 64.72
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1200_2.wcnf S = OPT
O = 733
T = 26.44
S = N/A
O = 1188
T = TO
(out)(err)
S = N/A
O = 1454
T = TO
(out)(err)
S = OPT
O = 733
T = 119.86
(out)(err)
S = OPT
O = 733
T = 124.76
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 733
T = 37.54
(out)(err)
S = OPT
O = 733
T = 26.44
(out)(err)
S = OPT
O = 733
T = 30.07
(out)(err)
S = OPT
O = 733
T = 29.39
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1200_3.wcnf S = OPT
O = 741
T = 29.10
S = N/A
O = 1014
T = TO
(out)(err)
S = N/A
O = 1361
T = TO
(out)(err)
S = OPT
O = 741
T = 215.25
(out)(err)
S = OPT
O = 741
T = 209.80
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 741
T = 84.10
(out)(err)
S = OPT
O = 741
T = 29.10
(out)(err)
S = OPT
O = 741
T = 33.87
(out)(err)
S = OPT
O = 741
T = 32.77
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1200_4.wcnf S = OPT
O = 667
T = 2.64
S = N/A
O = 1113
T = TO
(out)(err)
S = N/A
O = 1414
T = TO
(out)(err)
S = OPT
O = 667
T = 15.13
(out)(err)
S = OPT
O = 667
T = 14.52
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 667
T = 3.69
(out)(err)
S = OPT
O = 667
T = 2.64
(out)(err)
S = OPT
O = 667
T = 3.04
(out)(err)
S = OPT
O = 667
T = 3.00
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1200_5.wcnf S = OPT
O = 714
T = 13.01
S = N/A
O = 1012
T = TO
(out)(err)
S = N/A
O = 1450
T = TO
(out)(err)
S = OPT
O = 714
T = 63.56
(out)(err)
S = OPT
O = 714
T = 47.04
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 714
T = 22.04
(out)(err)
S = OPT
O = 714
T = 13.01
(out)(err)
S = OPT
O = 714
T = 15.30
(out)(err)
S = OPT
O = 714
T = 14.69
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1200_6.wcnf S = OPT
O = 803
T = 121.97
S = N/A
O = 1199
T = TO
(out)(err)
S = N/A
O = 1455
T = TO
(out)(err)
S = OPT
O = 803
T = 460.21
(out)(err)
S = OPT
O = 803
T = 469.01
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 803
T = 130.66
(out)(err)
S = OPT
O = 803
T = 121.97
(out)(err)
S = OPT
O = 803
T = 142.53
(out)(err)
S = OPT
O = 803
T = 133.80
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1200_7.wcnf S = OPT
O = 774
T = 145.30
S = N/A
O = 1000
T = TO
(out)(err)
S = N/A
O = 1454
T = TO
(out)(err)
S = OPT
O = 774
T = 456.36
(out)(err)
S = OPT
O = 774
T = 463.21
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 774
T = 209.91
(out)(err)
S = OPT
O = 774
T = 145.30
(out)(err)
S = OPT
O = 774
T = 168.62
(out)(err)
S = OPT
O = 774
T = 166.43
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1200_8.wcnf S = OPT
O = 745
T = 51.20
S = N/A
O = 1006
T = TO
(out)(err)
S = N/A
O = 1414
T = TO
(out)(err)
S = OPT
O = 745
T = 223.27
(out)(err)
S = OPT
O = 745
T = 220.79
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 745
T = 105.24
(out)(err)
S = OPT
O = 745
T = 51.20
(out)(err)
S = OPT
O = 745
T = 57.65
(out)(err)
S = OPT
O = 745
T = 56.27
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1300_1.wcnf S = OPT
O = 846
T = 43.93
S = N/A
O = 1167
T = TO
(out)(err)
S = N/A
O = 1562
T = TO
(out)(err)
S = OPT
O = 846
T = 189.31
(out)(err)
S = OPT
O = 846
T = 193.70
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 846
T = 59.97
(out)(err)
S = OPT
O = 846
T = 43.93
(out)(err)
S = OPT
O = 846
T = 50.51
(out)(err)
S = OPT
O = 846
T = 48.31
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1300_2.wcnf S = OPT
O = 774
T = 3.96
S = N/A
O = 1096
T = TO
(out)(err)
S = N/A
O = 1513
T = TO
(out)(err)
S = OPT
O = 774
T = 26.78
(out)(err)
S = OPT
O = 774
T = 28.92
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 774
T = 7.61
(out)(err)
S = OPT
O = 774
T = 3.96
(out)(err)
S = OPT
O = 774
T = 4.52
(out)(err)
S = OPT
O = 774
T = 4.37
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1300_3.wcnf S = OPT
O = 832
T = 27.47
S = N/A
O = 1058
T = TO
(out)(err)
S = N/A
O = 1664
T = TO
(out)(err)
S = OPT
O = 832
T = 315.85
(out)(err)
S = OPT
O = 832
T = 333.99
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 832
T = 55.15
(out)(err)
S = OPT
O = 832
T = 27.47
(out)(err)
S = OPT
O = 832
T = 30.96
(out)(err)
S = OPT
O = 832
T = 30.37
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1300_4.wcnf S = OPT
O = 871
T = 191.32
S = N/A
O = 1132
T = TO
(out)(err)
S = N/A
O = 1685
T = TO
(out)(err)
S = OPT
O = 871
T = 668.63
(out)(err)
S = OPT
O = 871
T = 681.38
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 871
T = 293.04
(out)(err)
S = OPT
O = 871
T = 191.32
(out)(err)
S = OPT
O = 871
T = 216.43
(out)(err)
S = OPT
O = 871
T = 211.74
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1300_5.wcnf S = OPT
O = 844
T = 54.42
S = N/A
O = 1224
T = TO
(out)(err)
S = N/A
O = 1625
T = TO
(out)(err)
S = OPT
O = 844
T = 222.18
(out)(err)
S = OPT
O = 844
T = 220.82
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 844
T = 62.49
(out)(err)
S = OPT
O = 844
T = 54.42
(out)(err)
S = OPT
O = 844
T = 62.18
(out)(err)
S = OPT
O = 844
T = 60.38
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1300_6.wcnf S = OPT
O = 884
T = 313.09
S = N/A
O = 1232
T = TO
(out)(err)
S = N/A
O = 1568
T = TO
(out)(err)
S = OPT
O = 884
T = 1540.60
(out)(err)
S = OPT
O = 884
T = 1535.78
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 884
T = 494.07
(out)(err)
S = OPT
O = 884
T = 313.09
(out)(err)
S = OPT
O = 884
T = 353.35
(out)(err)
S = OPT
O = 884
T = 344.39
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1300_7.wcnf S = OPT
O = 874
T = 90.76
S = N/A
O = 1099
T = TO
(out)(err)
S = N/A
O = 1559
T = TO
(out)(err)
S = OPT
O = 874
T = 431.86
(out)(err)
S = OPT
O = 874
T = 428.18
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 874
T = 181.63
(out)(err)
S = OPT
O = 874
T = 90.76
(out)(err)
S = OPT
O = 874
T = 104.99
(out)(err)
S = OPT
O = 874
T = 103.44
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1300_8.wcnf S = OPT
O = 812
T = 79.33
S = N/A
O = 1039
T = TO
(out)(err)
S = N/A
O = 1515
T = TO
(out)(err)
S = OPT
O = 812
T = 350.25
(out)(err)
S = OPT
O = 812
T = 345.36
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 812
T = 103.24
(out)(err)
S = OPT
O = 812
T = 79.33
(out)(err)
S = OPT
O = 812
T = 91.53
(out)(err)
S = OPT
O = 812
T = 90.46
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1400_1.wcnf S = OPT
O = 926
T = 94.05
S = N/A
O = 1297
T = TO
(out)(err)
S = N/A
O = 1766
T = TO
(out)(err)
S = OPT
O = 926
T = 622.48
(out)(err)
S = OPT
O = 926
T = 649.57
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 926
T = 116.03
(out)(err)
S = OPT
O = 926
T = 94.05
(out)(err)
S = OPT
O = 926
T = 106.03
(out)(err)
S = OPT
O = 926
T = 101.49
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1400_2.wcnf S = OPT
O = 879
T = 32.59
S = N/A
O = 1190
T = TO
(out)(err)
S = N/A
O = 1657
T = TO
(out)(err)
S = OPT
O = 879
T = 110.70
(out)(err)
S = OPT
O = 879
T = 112.68
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 879
T = 40.55
(out)(err)
S = OPT
O = 879
T = 32.59
(out)(err)
S = OPT
O = 879
T = 37.45
(out)(err)
S = OPT
O = 879
T = 37.05
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1400_3.wcnf S = OPT
O = 936
T = 87.06
S = N/A
O = 1236
T = TO
(out)(err)
S = N/A
O = 1732
T = TO
(out)(err)
S = OPT
O = 936
T = 368.56
(out)(err)
S = OPT
O = 936
T = 373.45
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 936
T = 101.22
(out)(err)
S = OPT
O = 936
T = 87.06
(out)(err)
S = OPT
O = 936
T = 99.09
(out)(err)
S = OPT
O = 936
T = 95.31
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1400_4.wcnf S = OPT
O = 932
T = 40.84
S = N/A
O = 1286
T = TO
(out)(err)
S = N/A
O = 1727
T = TO
(out)(err)
S = OPT
O = 932
T = 244.11
(out)(err)
S = OPT
O = 932
T = 239.41
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 932
T = 98.48
(out)(err)
S = OPT
O = 932
T = 40.84
(out)(err)
S = OPT
O = 932
T = 44.97
(out)(err)
S = OPT
O = 932
T = 44.22
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1400_5.wcnf S = OPT
O = 968
T = 108.14
S = N/A
O = 1537
T = TO
(out)(err)
S = N/A
O = 1862
T = TO
(out)(err)
S = OPT
O = 968
T = 797.73
(out)(err)
S = OPT
O = 968
T = 776.85
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 968
T = 197.10
(out)(err)
S = OPT
O = 968
T = 108.14
(out)(err)
S = OPT
O = 968
T = 121.94
(out)(err)
S = OPT
O = 968
T = 115.61
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1400_6.wcnf S = OPT
O = 967
T = 327.40
S = N/A
O = 1330
T = TO
(out)(err)
S = N/A
O = 1547
T = TO
(out)(err)
S = OPT
O = 967
T = 1434.88
(out)(err)
S = OPT
O = 967
T = 1585.41
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 967
T = 464.06
(out)(err)
S = OPT
O = 967
T = 327.40
(out)(err)
S = OPT
O = 967
T = 373.43
(out)(err)
S = OPT
O = 967
T = 359.67
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1400_7.wcnf S = OPT
O = 923
T = 29.75
S = N/A
O = 1283
T = TO
(out)(err)
S = N/A
O = 1724
T = 459.20
(out)(err)
S = OPT
O = 923
T = 159.66
(out)(err)
S = OPT
O = 923
T = 152.93
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 923
T = 72.68
(out)(err)
S = OPT
O = 923
T = 29.75
(out)(err)
S = OPT
O = 923
T = 33.48
(out)(err)
S = OPT
O = 923
T = 32.02
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1400_8.wcnf S = OPT
O = 957
T = 147.94
S = N/A
O = 1224
T = TO
(out)(err)
S = N/A
O = 1667
T = TO
(out)(err)
S = OPT
O = 957
T = 1482.04
(out)(err)
S = OPT
O = 957
T = 1315.74
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 957
T = 323.30
(out)(err)
S = OPT
O = 957
T = 147.94
(out)(err)
S = OPT
O = 957
T = 163.09
(out)(err)
S = OPT
O = 957
T = 162.66
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1500_1.wcnf S = OPT
O = 986
T = 50.69
S = N/A
O = 1332
T = TO
(out)(err)
S = N/A
O = 1737
T = TO
(out)(err)
S = OPT
O = 986
T = 343.52
(out)(err)
S = OPT
O = 986
T = 337.03
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 986
T = 149.97
(out)(err)
S = OPT
O = 986
T = 50.69
(out)(err)
S = OPT
O = 986
T = 57.06
(out)(err)
S = OPT
O = 986
T = 55.13
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1500_2.wcnf S = OPT
O = 998
T = 68.31
S = N/A
O = 1384
T = TO
(out)(err)
S = N/A
O = 1734
T = TO
(out)(err)
S = OPT
O = 998
T = 471.35
(out)(err)
S = OPT
O = 998
T = 488.41
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 998
T = 141.65
(out)(err)
S = OPT
O = 998
T = 68.31
(out)(err)
S = OPT
O = 998
T = 76.97
(out)(err)
S = OPT
O = 998
T = 74.81
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1500_3.wcnf S = OPT
O = 1073
T = 340.76
S = N/A
O = 1380
T = TO
(out)(err)
S = N/A
O = 1976
T = 207.85
(out)(err)
S = OPT
O = 1073
T = 1743.89
(out)(err)
S = OPT
O = 1073
T = 1737.62
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1073
T = 479.29
(out)(err)
S = OPT
O = 1073
T = 340.76
(out)(err)
S = OPT
O = 1073
T = 374.91
(out)(err)
S = OPT
O = 1073
T = 363.28
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1500_4.wcnf S = OPT
O = 1047
T = 315.02
S = N/A
O = 1374
T = TO
(out)(err)
S = N/A
O = 1795
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 = OPT
O = 1047
T = 702.29
(out)(err)
S = OPT
O = 1047
T = 315.02
(out)(err)
S = OPT
O = 1047
T = 341.38
(out)(err)
S = OPT
O = 1047
T = 335.43
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1500_5.wcnf S = OPT
O = 1058
T = 189.10
S = N/A
O = 1356
T = TO
(out)(err)
S = N/A
O = 2042
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 = OPT
O = 1058
T = 623.99
(out)(err)
S = OPT
O = 1058
T = 189.10
(out)(err)
S = OPT
O = 1058
T = 208.49
(out)(err)
S = OPT
O = 1058
T = 205.39
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1500_6.wcnf S = OPT
O = 1102
T = 619.78
S = N/A
O = 1427
T = TO
(out)(err)
S = N/A
O = 1772
T = 206.04
(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 = OPT
O = 1102
T = 663.69
(out)(err)
S = OPT
O = 1102
T = 619.78
(out)(err)
S = OPT
O = 1102
T = 713.49
(out)(err)
S = OPT
O = 1102
T = 714.04
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1500_7.wcnf S = OPT
O = 1010
T = 36.30
S = N/A
O = 1344
T = TO
(out)(err)
S = N/A
O = 2022
T = TO
(out)(err)
S = OPT
O = 1010
T = 247.12
(out)(err)
S = OPT
O = 1010
T = 250.81
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1010
T = 51.97
(out)(err)
S = OPT
O = 1010
T = 36.30
(out)(err)
S = OPT
O = 1010
T = 40.73
(out)(err)
S = OPT
O = 1010
T = 39.23
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1500_8.wcnf S = OPT
O = 1045
T = 110.74
S = N/A
O = 1472
T = TO
(out)(err)
S = N/A
O = 1980
T = TO
(out)(err)
S = OPT
O = 1045
T = 650.52
(out)(err)
S = OPT
O = 1045
T = 646.49
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1045
T = 203.06
(out)(err)
S = OPT
O = 1045
T = 110.74
(out)(err)
S = OPT
O = 1045
T = 127.54
(out)(err)
S = OPT
O = 1045
T = 121.62
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1600_1.wcnf S = OPT
O = 1143
T = 62.85
S = N/A
O = 1622
T = TO
(out)(err)
S = N/A
O = 2242
T = TO
(out)(err)
S = OPT
O = 1143
T = 406.21
(out)(err)
S = OPT
O = 1143
T = 415.91
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1143
T = 106.41
(out)(err)
S = OPT
O = 1143
T = 62.85
(out)(err)
S = OPT
O = 1143
T = 70.73
(out)(err)
S = OPT
O = 1143
T = 68.83
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1600_2.wcnf S = OPT
O = 1140
T = 57.32
S = N/A
O = 1477
T = TO
(out)(err)
S = N/A
O = 2218
T = 415.65
(out)(err)
S = OPT
O = 1140
T = 437.41
(out)(err)
S = OPT
O = 1140
T = 438.45
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1140
T = 85.06
(out)(err)
S = OPT
O = 1140
T = 57.32
(out)(err)
S = OPT
O = 1140
T = 63.86
(out)(err)
S = OPT
O = 1140
T = 61.84
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1600_3.wcnf S = OPT
O = 1079
T = 61.04
S = N/A
O = 1395
T = TO
(out)(err)
S = N/A
O = 1884
T = 489.36
(out)(err)
S = OPT
O = 1079
T = 281.37
(out)(err)
S = OPT
O = 1079
T = 281.52
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1079
T = 64.38
(out)(err)
S = OPT
O = 1079
T = 61.04
(out)(err)
S = OPT
O = 1079
T = 69.08
(out)(err)
S = OPT
O = 1079
T = 66.56
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1600_4.wcnf S = OPT
O = 1157
T = 192.79
S = N/A
O = 1606
T = TO
(out)(err)
S = N/A
O = 2133
T = 447.39
(out)(err)
S = OPT
O = 1157
T = 1188.30
(out)(err)
S = OPT
O = 1157
T = 1195.00
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1157
T = 193.14
(out)(err)
S = OPT
O = 1157
T = 192.79
(out)(err)
S = OPT
O = 1157
T = 207.31
(out)(err)
S = OPT
O = 1157
T = 201.18
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1600_5.wcnf S = OPT
O = 1119
T = 168.93
S = N/A
O = 1563
T = TO
(out)(err)
S = N/A
O = 2085
T = TO
(out)(err)
S = OPT
O = 1119
T = 1552.57
(out)(err)
S = OPT
O = 1119
T = 1576.09
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1119
T = 315.68
(out)(err)
S = OPT
O = 1119
T = 168.93
(out)(err)
S = OPT
O = 1119
T = 187.69
(out)(err)
S = OPT
O = 1119
T = 181.70
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
s2v140c1600_6.wcnf S = OPT
O = 1212
T = 400.74
S = N/A
O = 1628
T = TO
(out)(err)
S = N/A
O = 2123
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 = OPT
O = 1212
T = 518.49
(out)(err)
S = OPT
O = 1212
T = 400.74
(out)(err)
S = OPT
O = 1212
T = 446.16
(out)(err)
S = OPT
O = 1212
T = 431.24
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1600_7.wcnf S = OPT
O = 1150
T = 163.91
S = N/A
O = 1698
T = TO
(out)(err)
S = N/A
O = 1980
T = TO
(out)(err)
S = OPT
O = 1150
T = 1579.41
(out)(err)
S = OPT
O = 1150
T = 1728.86
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1150
T = 321.14
(out)(err)
S = OPT
O = 1150
T = 163.91
(out)(err)
S = OPT
O = 1150
T = 176.63
(out)(err)
S = OPT
O = 1150
T = 172.56
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
s2v140c1600_8.wcnf S = OPT
O = 1180
T = 140.18
S = N/A
O = 1526
T = TO
(out)(err)
S = N/A
O = 2224
T = TO
(out)(err)
S = OPT
O = 1180
T = 996.15
(out)(err)
S = OPT
O = 1180
T = 997.25
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 1180
T = 200.15
(out)(err)
S = OPT
O = 1180
T = 140.18
(out)(err)
S = OPT
O = 1180
T = 166.77
(out)(err)
S = OPT
O = 1180
T = 154.80
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C1000_0.wcnf S = OPT
O = 198
T = 169.89
S = N/A
O = 331
T = TO
(out)(err)
S = N/A
O = 761
T = TO
(out)(err)
S = OPT
O = 198
T = 731.12
(out)(err)
S = OPT
O = 198
T = 738.48
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 198
T = 247.51
(out)(err)
S = OPT
O = 198
T = 169.89
(out)(err)
S = OPT
O = 198
T = 188.39
(out)(err)
S = OPT
O = 198
T = 187.13
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C1000_1.wcnf S = OPT
O = 212
T = 132.70
S = N/A
O = 356
T = TO
(out)(err)
S = N/A
O = 838
T = TO
(out)(err)
S = OPT
O = 212
T = 395.12
(out)(err)
S = OPT
O = 212
T = 398.29
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 212
T = 162.99
(out)(err)
S = OPT
O = 212
T = 132.70
(out)(err)
S = OPT
O = 212
T = 149.23
(out)(err)
S = OPT
O = 212
T = 145.00
(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 = 205.72
S = N/A
O = 334
T = TO
(out)(err)
S = N/A
O = 772
T = TO
(out)(err)
S = OPT
O = 211
T = 581.45
(out)(err)
S = OPT
O = 211
T = 582.01
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 211
T = 226.07
(out)(err)
S = OPT
O = 211
T = 205.72
(out)(err)
S = OPT
O = 211
T = 223.58
(out)(err)
S = OPT
O = 211
T = 220.59
(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 = 275.74
S = N/A
O = 338
T = TO
(out)(err)
S = N/A
O = 795
T = TO
(out)(err)
S = OPT
O = 229
T = 801.45
(out)(err)
S = OPT
O = 229
T = 811.40
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 229
T = 312.88
(out)(err)
S = OPT
O = 229
T = 275.74
(out)(err)
S = OPT
O = 229
T = 311.54
(out)(err)
S = OPT
O = 229
T = 305.82
(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 = 146.55
S = N/A
O = 602
T = TO
(out)(err)
S = N/A
O = 702
T = TO
(out)(err)
S = OPT
O = 202
T = 506.09
(out)(err)
S = OPT
O = 202
T = 508.43
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 202
T = 203.06
(out)(err)
S = OPT
O = 202
T = 146.55
(out)(err)
S = OPT
O = 202
T = 164.04
(out)(err)
S = OPT
O = 202
T = 162.02
(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 = 156.92
S = N/A
O = 371
T = TO
(out)(err)
S = N/A
O = 798
T = TO
(out)(err)
S = OPT
O = 214
T = 937.89
(out)(err)
S = OPT
O = 214
T = 945.00
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 214
T = 392.65
(out)(err)
S = OPT
O = 214
T = 156.92
(out)(err)
S = OPT
O = 214
T = 177.81
(out)(err)
S = OPT
O = 214
T = 172.92
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C1000_6.wcnf S = OPT
O = 203
T = 106.94
S = N/A
O = 443
T = TO
(out)(err)
S = N/A
O = 629
T = TO
(out)(err)
S = OPT
O = 203
T = 246.30
(out)(err)
S = OPT
O = 203
T = 248.17
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 203
T = 107.29
(out)(err)
S = OPT
O = 203
T = 106.94
(out)(err)
S = OPT
O = 203
T = 118.00
(out)(err)
S = OPT
O = 203
T = 117.38
(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 = 91.74
S = N/A
O = 221
T = TO
(out)(err)
S = N/A
O = 722
T = TO
(out)(err)
S = OPT
O = 200
T = 260.66
(out)(err)
S = OPT
O = 200
T = 260.90
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 200
T = 146.67
(out)(err)
S = OPT
O = 200
T = 91.74
(out)(err)
S = OPT
O = 200
T = 102.21
(out)(err)
S = OPT
O = 200
T = 100.29
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C1000_8.wcnf S = OPT
O = 188
T = 51.48
S = N/A
O = 430
T = TO
(out)(err)
S = N/A
O = 709
T = TO
(out)(err)
S = OPT
O = 188
T = 378.82
(out)(err)
S = OPT
O = 188
T = 383.30
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 188
T = 141.93
(out)(err)
S = OPT
O = 188
T = 51.48
(out)(err)
S = OPT
O = 188
T = 57.64
(out)(err)
S = OPT
O = 188
T = 57.01
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C1000_9.wcnf S = OPT
O = 226
T = 282.63
S = N/A
O = 369
T = TO
(out)(err)
S = N/A
O = 766
T = TO
(out)(err)
S = OPT
O = 226
T = 764.96
(out)(err)
S = OPT
O = 226
T = 774.96
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 226
T = 282.63
(out)(err)
S = OPT
O = 226
T = 290.29
(out)(err)
S = OPT
O = 226
T = 317.48
(out)(err)
S = OPT
O = 226
T = 314.25
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C700_0.wcnf S = OPT
O = 103
T = 32.25
S = N/A
O = 346
T = TO
(out)(err)
S = N/A
O = 325
T = TO
(out)(err)
S = OPT
O = 103
T = 89.91
(out)(err)
S = OPT
O = 103
T = 89.62
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 103
T = 43.02
(out)(err)
S = OPT
O = 103
T = 32.25
(out)(err)
S = OPT
O = 103
T = 37.70
(out)(err)
S = OPT
O = 103
T = 36.85
(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 = 19.67
S = N/A
O = 169
T = TO
(out)(err)
S = N/A
O = 319
T = TO
(out)(err)
S = OPT
O = 107
T = 47.51
(out)(err)
S = OPT
O = 107
T = 47.12
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 107
T = 25.71
(out)(err)
S = OPT
O = 107
T = 19.67
(out)(err)
S = OPT
O = 107
T = 22.41
(out)(err)
S = OPT
O = 107
T = 22.35
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C700_2.wcnf S = OPT
O = 110
T = 32.40
S = N/A
O = 163
T = TO
(out)(err)
S = N/A
O = 407
T = TO
(out)(err)
S = OPT
O = 110
T = 74.37
(out)(err)
S = OPT
O = 110
T = 74.59
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 110
T = 32.65
(out)(err)
S = OPT
O = 110
T = 32.40
(out)(err)
S = OPT
O = 110
T = 37.12
(out)(err)
S = OPT
O = 110
T = 37.19
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C700_3.wcnf S = OPT
O = 102
T = 12.32
S = N/A
O = 228
T = TO
(out)(err)
S = N/A
O = 377
T = TO
(out)(err)
S = OPT
O = 102
T = 25.17
(out)(err)
S = OPT
O = 102
T = 24.81
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 102
T = 14.21
(out)(err)
S = OPT
O = 102
T = 12.32
(out)(err)
S = OPT
O = 102
T = 14.34
(out)(err)
S = OPT
O = 102
T = 14.20
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C700_4.wcnf S = OPT
O = 110
T = 26.29
S = N/A
O = 152
T = TO
(out)(err)
S = N/A
O = 431
T = TO
(out)(err)
S = OPT
O = 110
T = 86.58
(out)(err)
S = OPT
O = 110
T = 86.87
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 110
T = 41.94
(out)(err)
S = OPT
O = 110
T = 26.29
(out)(err)
S = OPT
O = 110
T = 29.54
(out)(err)
S = OPT
O = 110
T = 29.37
(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.42
S = N/A
O = 237
T = TO
(out)(err)
S = N/A
O = 365
T = TO
(out)(err)
S = OPT
O = 103
T = 56.09
(out)(err)
S = OPT
O = 103
T = 55.79
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 103
T = 30.99
(out)(err)
S = OPT
O = 103
T = 15.42
(out)(err)
S = OPT
O = 103
T = 17.37
(out)(err)
S = OPT
O = 103
T = 17.20
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C700_6.wcnf S = OPT
O = 102
T = 15.85
S = N/A
O = 137
T = TO
(out)(err)
S = N/A
O = 374
T = TO
(out)(err)
S = OPT
O = 102
T = 41.41
(out)(err)
S = OPT
O = 102
T = 41.24
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 102
T = 20.15
(out)(err)
S = OPT
O = 102
T = 15.85
(out)(err)
S = OPT
O = 102
T = 18.57
(out)(err)
S = OPT
O = 102
T = 18.34
(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 = 20.47
S = N/A
O = 273
T = TO
(out)(err)
S = N/A
O = 378
T = TO
(out)(err)
S = OPT
O = 104
T = 44.33
(out)(err)
S = OPT
O = 104
T = 44.19
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 104
T = 22.48
(out)(err)
S = OPT
O = 104
T = 20.47
(out)(err)
S = OPT
O = 104
T = 24.07
(out)(err)
S = OPT
O = 104
T = 23.82
(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 = 3.76
S = N/A
O = 314
T = TO
(out)(err)
S = N/A
O = 390
T = TO
(out)(err)
S = OPT
O = 82
T = 6.89
(out)(err)
S = OPT
O = 82
T = 6.89
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 82
T = 3.91
(out)(err)
S = OPT
O = 82
T = 3.76
(out)(err)
S = OPT
O = 82
T = 4.35
(out)(err)
S = OPT
O = 82
T = 4.36
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C700_9.wcnf S = OPT
O = 104
T = 20.12
S = N/A
O = 288
T = TO
(out)(err)
S = N/A
O = 346
T = TO
(out)(err)
S = OPT
O = 104
T = 49.67
(out)(err)
S = OPT
O = 104
T = 50.15
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 104
T = 21.06
(out)(err)
S = OPT
O = 104
T = 20.12
(out)(err)
S = OPT
O = 104
T = 23.02
(out)(err)
S = OPT
O = 104
T = 22.82
(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 = 37.32
S = N/A
O = 429
T = TO
(out)(err)
S = N/A
O = 536
T = TO
(out)(err)
S = OPT
O = 132
T = 114.34
(out)(err)
S = OPT
O = 132
T = 115.12
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 132
T = 48.37
(out)(err)
S = OPT
O = 132
T = 37.32
(out)(err)
S = OPT
O = 132
T = 42.02
(out)(err)
S = OPT
O = 132
T = 40.92
(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 = 44.63
S = N/A
O = 183
T = TO
(out)(err)
S = N/A
O = 505
T = TO
(out)(err)
S = OPT
O = 138
T = 180.26
(out)(err)
S = OPT
O = 138
T = 179.05
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 138
T = 73.50
(out)(err)
S = OPT
O = 138
T = 44.63
(out)(err)
S = OPT
O = 138
T = 50.18
(out)(err)
S = OPT
O = 138
T = 49.62
(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 = 23.14
S = N/A
O = 399
T = TO
(out)(err)
S = N/A
O = 502
T = TO
(out)(err)
S = OPT
O = 127
T = 107.15
(out)(err)
S = OPT
O = 127
T = 107.43
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 127
T = 48.91
(out)(err)
S = OPT
O = 127
T = 23.14
(out)(err)
S = OPT
O = 127
T = 26.57
(out)(err)
S = OPT
O = 127
T = 26.11
(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 = 13.11
S = N/A
O = 291
T = TO
(out)(err)
S = N/A
O = 591
T = TO
(out)(err)
S = OPT
O = 134
T = 68.46
(out)(err)
S = OPT
O = 134
T = 68.43
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 134
T = 21.91
(out)(err)
S = OPT
O = 134
T = 13.11
(out)(err)
S = OPT
O = 134
T = 14.97
(out)(err)
S = OPT
O = 134
T = 14.89
(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 = 43.98
S = N/A
O = 443
T = TO
(out)(err)
S = N/A
O = 633
T = TO
(out)(err)
S = OPT
O = 143
T = 255.44
(out)(err)
S = OPT
O = 143
T = 255.22
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 143
T = 154.01
(out)(err)
S = OPT
O = 143
T = 43.98
(out)(err)
S = OPT
O = 143
T = 50.23
(out)(err)
S = OPT
O = 143
T = 49.20
(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 = 74.54
S = N/A
O = 252
T = TO
(out)(err)
S = N/A
O = 598
T = TO
(out)(err)
S = OPT
O = 144
T = 283.64
(out)(err)
S = OPT
O = 144
T = 283.50
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 144
T = 118.20
(out)(err)
S = OPT
O = 144
T = 74.54
(out)(err)
S = OPT
O = 144
T = 86.01
(out)(err)
S = OPT
O = 144
T = 84.20
(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 = 41.43
S = N/A
O = 371
T = TO
(out)(err)
S = N/A
O = 518
T = TO
(out)(err)
S = OPT
O = 135
T = 123.59
(out)(err)
S = OPT
O = 135
T = 123.90
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 135
T = 62.39
(out)(err)
S = OPT
O = 135
T = 41.43
(out)(err)
S = OPT
O = 135
T = 46.40
(out)(err)
S = OPT
O = 135
T = 46.54
(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 = 44.28
S = N/A
O = 232
T = TO
(out)(err)
S = N/A
O = 596
T = TO
(out)(err)
S = OPT
O = 147
T = 201.82
(out)(err)
S = OPT
O = 147
T = 204.08
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 147
T = 61.88
(out)(err)
S = OPT
O = 147
T = 44.28
(out)(err)
S = OPT
O = 147
T = 50.15
(out)(err)
S = OPT
O = 147
T = 50.36
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C800_8.wcnf S = OPT
O = 126
T = 22.12
S = N/A
O = 392
T = TO
(out)(err)
S = N/A
O = 542
T = TO
(out)(err)
S = OPT
O = 126
T = 134.91
(out)(err)
S = OPT
O = 126
T = 134.34
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 126
T = 60.30
(out)(err)
S = OPT
O = 126
T = 22.12
(out)(err)
S = OPT
O = 126
T = 25.43
(out)(err)
S = OPT
O = 126
T = 24.90
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C800_9.wcnf S = OPT
O = 138
T = 34.08
S = N/A
O = 381
T = TO
(out)(err)
S = N/A
O = 496
T = TO
(out)(err)
S = OPT
O = 138
T = 120.93
(out)(err)
S = OPT
O = 138
T = 120.59
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 138
T = 57.51
(out)(err)
S = OPT
O = 138
T = 34.08
(out)(err)
S = OPT
O = 138
T = 38.96
(out)(err)
S = OPT
O = 138
T = 39.59
(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 = 51.75
S = N/A
O = 293
T = TO
(out)(err)
S = N/A
O = 698
T = TO
(out)(err)
S = OPT
O = 157
T = 127.58
(out)(err)
S = OPT
O = 157
T = 128.41
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 157
T = 53.78
(out)(err)
S = OPT
O = 157
T = 51.75
(out)(err)
S = OPT
O = 157
T = 60.02
(out)(err)
S = OPT
O = 157
T = 58.45
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C900_1.wcnf S = OPT
O = 192
T = 177.39
S = N/A
O = 243
T = TO
(out)(err)
S = N/A
O = 691
T = TO
(out)(err)
S = OPT
O = 192
T = 445.00
(out)(err)
S = OPT
O = 192
T = 446.25
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 192
T = 214.75
(out)(err)
S = OPT
O = 192
T = 177.39
(out)(err)
S = OPT
O = 192
T = 200.22
(out)(err)
S = OPT
O = 192
T = 198.48
(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 = 126.24
S = N/A
O = 211
T = TO
(out)(err)
S = N/A
O = 574
T = TO
(out)(err)
S = OPT
O = 177
T = 369.22
(out)(err)
S = OPT
O = 177
T = 373.56
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 177
T = 157.69
(out)(err)
S = OPT
O = 177
T = 126.24
(out)(err)
S = OPT
O = 177
T = 142.08
(out)(err)
S = OPT
O = 177
T = 139.44
(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 = 57.86
S = N/A
O = 242
T = TO
(out)(err)
S = N/A
O = 459
T = TO
(out)(err)
S = OPT
O = 163
T = 237.84
(out)(err)
S = OPT
O = 163
T = 239.51
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 163
T = 85.84
(out)(err)
S = OPT
O = 163
T = 57.86
(out)(err)
S = OPT
O = 163
T = 66.20
(out)(err)
S = OPT
O = 163
T = 63.72
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C900_4.wcnf S = OPT
O = 171
T = 105.79
S = N/A
O = 413
T = TO
(out)(err)
S = N/A
O = 660
T = TO
(out)(err)
S = OPT
O = 171
T = 318.98
(out)(err)
S = OPT
O = 171
T = 320.26
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 171
T = 136.85
(out)(err)
S = OPT
O = 171
T = 105.79
(out)(err)
S = OPT
O = 171
T = 118.38
(out)(err)
S = OPT
O = 171
T = 118.61
(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 = 89.41
S = N/A
O = 499
T = TO
(out)(err)
S = N/A
O = 614
T = TO
(out)(err)
S = OPT
O = 175
T = 211.12
(out)(err)
S = OPT
O = 175
T = 212.93
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 175
T = 102.64
(out)(err)
S = OPT
O = 175
T = 89.41
(out)(err)
S = OPT
O = 175
T = 101.53
(out)(err)
S = OPT
O = 175
T = 99.79
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C900_6.wcnf S = OPT
O = 174
T = 82.36
S = N/A
O = 466
T = TO
(out)(err)
S = N/A
O = 542
T = 1581.02
(out)(err)
S = OPT
O = 174
T = 221.42
(out)(err)
S = OPT
O = 174
T = 223.25
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 174
T = 149.41
(out)(err)
S = OPT
O = 174
T = 82.36
(out)(err)
S = OPT
O = 174
T = 94.55
(out)(err)
S = OPT
O = 174
T = 90.57
(out)(err)
S = N/A
O = N/A
T = 1800.00
(out)(err)
file_rwms_wcnf_L3_V70_C900_7.wcnf S = OPT
O = 194
T = 192.02
S = N/A
O = 271
T = TO
(out)(err)
S = N/A
O = 802
T = TO
(out)(err)
S = OPT
O = 194
T = 643.70
(out)(err)
S = OPT
O = 194
T = 644.76
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 194
T = 250.73
(out)(err)
S = OPT
O = 194
T = 192.02
(out)(err)
S = OPT
O = 194
T = 213.62
(out)(err)
S = OPT
O = 194
T = 211.98
(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 = 106.06
S = N/A
O = 244
T = TO
(out)(err)
S = N/A
O = 589
T = TO
(out)(err)
S = OPT
O = 179
T = 239.63
(out)(err)
S = OPT
O = 179
T = 240.00
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 179
T = 107.58
(out)(err)
S = OPT
O = 179
T = 106.06
(out)(err)
S = OPT
O = 179
T = 116.51
(out)(err)
S = OPT
O = 179
T = 114.26
(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 = 98.09
S = N/A
O = 450
T = TO
(out)(err)
S = N/A
O = 756
T = TO
(out)(err)
S = OPT
O = 181
T = 255.38
(out)(err)
S = OPT
O = 181
T = 257.25
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)
S = OPT
O = 181
T = 116.58
(out)(err)
S = OPT
O = 181
T = 98.09
(out)(err)
S = OPT
O = 181
T = 111.83
(out)(err)
S = OPT
O = 181
T = 108.76
(out)(err)
S = N/A
O = N/A
T = TO
(out)(err)