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 CCLS SAT4Jms-ext-i SAT4Jms-int-i iraNovelty++ optimax-it
s2v100c1200_1.wcnf O = 865
T = 2.39
O = 865
T = 2.39
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 865
T = 2.56
(out)(err)
O = 1211
T = 0.08
(out)(err)
s2v100c1200_2.wcnf O = 774
T = 2.07
O = 774
T = 2.07
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 774
T = 4.32
(out)(err)
O = 1100
T = 1.57
(out)(err)
s2v100c1200_3.wcnf O = 933
T = 1.59
O = 933
T = 1.59
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 933
T = 28.45
(out)(err)
O = 1276
T = 0.09
(out)(err)
s2v100c1200_4.wcnf O = 798
T = 1.99
O = 798
T = 2.22
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 798
T = 1.99
(out)(err)
O = 1154
T = 0.08
(out)(err)
s2v100c1200_5.wcnf O = 876
T = 2.24
O = 876
T = 2.24
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 876
T = 2.48
(out)(err)
O = 1237
T = 0.08
(out)(err)
s2v100c1200_6.wcnf O = 734
T = 1.85
O = 734
T = 1.85
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 734
T = 2.11
(out)(err)
O = 957
T = 0.07
(out)(err)
s2v100c1200_7.wcnf O = 800
T = 1.59
O = 800
T = 1.59
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 800
T = 3.65
(out)(err)
O = 1106
T = 0.09
(out)(err)
s2v100c1200_8.wcnf O = 962
T = 2.36
O = 962
T = 2.36
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 962
T = 15.82
(out)(err)
O = 1326
T = 0.05
(out)(err)
s2v100c1300_1.wcnf O = 971
T = 1.87
O = 971
T = 1.91
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 971
T = 1.87
(out)(err)
O = 1310
T = 0.08
(out)(err)
s2v100c1300_2.wcnf O = 930
T = 1.80
O = 930
T = 2.37
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 930
T = 1.80
(out)(err)
O = 1293
T = 0.08
(out)(err)
s2v100c1300_3.wcnf O = 925
T = 1.63
O = 925
T = 1.63
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 925
T = 5.15
(out)(err)
O = 1139
T = 0.08
(out)(err)
s2v100c1300_4.wcnf O = 970
T = 2.95
O = 970
T = 2.95
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 970
T = 4.54
(out)(err)
O = 1295
T = 0.08
(out)(err)
s2v100c1300_5.wcnf O = 962
T = 1.74
O = 962
T = 3.02
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 962
T = 1.74
(out)(err)
O = 1237
T = 0.08
(out)(err)
s2v100c1300_6.wcnf O = 933
T = 2.06
O = 933
T = 2.06
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 933
T = 29.01
(out)(err)
O = 1361
T = 0.08
(out)(err)
s2v100c1300_7.wcnf O = 877
T = 1.87
O = 877
T = 1.87
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 877
T = 8.37
(out)(err)
O = 1281
T = 0.10
(out)(err)
s2v100c1300_8.wcnf O = 941
T = 2.29
O = 941
T = 2.29
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 941
T = 89.41
(out)(err)
O = 1213
T = 0.10
(out)(err)
s2v100c1400_1.wcnf O = 1019
T = 2.12
O = 1019
T = 2.12
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1019
T = 9.04
(out)(err)
O = 1388
T = 0.08
(out)(err)
s2v100c1400_2.wcnf O = 1002
T = 1.79
O = 1002
T = 1.79
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1002
T = 15.89
(out)(err)
O = 1338
T = 0.09
(out)(err)
s2v100c1400_3.wcnf O = 1020
T = 1.94
O = 1020
T = 1.94
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1020
T = 10.87
(out)(err)
O = 1400
T = 0.07
(out)(err)
s2v100c1400_4.wcnf O = 1094
T = 1.76
O = 1094
T = 1.76
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1094
T = 20.24
(out)(err)
O = 1638
T = 0.07
(out)(err)
s2v100c1400_5.wcnf O = 1018
T = 2.20
O = 1018
T = 2.20
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1018
T = 2.21
(out)(err)
O = 1437
T = 0.07
(out)(err)
s2v100c1400_6.wcnf O = 997
T = 1.91
O = 997
T = 2.40
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 997
T = 1.91
(out)(err)
O = 1417
T = 0.08
(out)(err)
s2v100c1400_7.wcnf O = 1001
T = 2.31
O = 1001
T = 2.31
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1001
T = 21.62
(out)(err)
O = 1339
T = 0.08
(out)(err)
s2v100c1400_8.wcnf O = 1084
T = 2.32
O = 1084
T = 2.32
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1084
T = 5.94
(out)(err)
O = 1455
T = 0.08
(out)(err)
s2v100c1500_1.wcnf O = 1077
T = 2.16
O = 1077
T = 2.16
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1077
T = 8.42
(out)(err)
O = 1450
T = 0.09
(out)(err)
s2v100c1500_2.wcnf O = 1125
T = 2.49
O = 1125
T = 2.49
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1125
T = 235.90
(out)(err)
O = 1484
T = 0.07
(out)(err)
s2v100c1500_3.wcnf O = 1151
T = 2.30
O = 1151
T = 2.30
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1151
T = 6.55
(out)(err)
O = 1478
T = 0.08
(out)(err)
s2v100c1500_4.wcnf O = 1072
T = 1.40
O = 1072
T = 1.98
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1072
T = 1.40
(out)(err)
O = 1452
T = 0.07
(out)(err)
s2v100c1500_5.wcnf O = 1151
T = 2.21
O = 1151
T = 2.21
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1151
T = 2.72
(out)(err)
O = 1455
T = 0.08
(out)(err)
s2v100c1500_6.wcnf O = 1225
T = 2.11
O = 1225
T = 2.11
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1225
T = 18.10
(out)(err)
O = 1687
T = 0.09
(out)(err)
s2v100c1500_7.wcnf O = 1186
T = 2.02
O = 1186
T = 2.43
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1186
T = 2.02
(out)(err)
O = 1585
T = 0.09
(out)(err)
s2v100c1500_8.wcnf O = 1217
T = 2.35
O = 1217
T = 2.35
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1218
T = 219.58
(out)(err)
O = 1737
T = 0.08
(out)(err)
s2v100c1600_1.wcnf O = 1230
T = 2.41
O = 1230
T = 2.41
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1230
T = 2.46
(out)(err)
O = 1714
T = 0.08
(out)(err)
s2v100c1600_2.wcnf O = 1265
T = 2.40
O = 1265
T = 2.40
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1265
T = 6.70
(out)(err)
O = 1652
T = 0.10
(out)(err)
s2v100c1600_3.wcnf O = 1309
T = 2.05
O = 1309
T = 2.05
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1309
T = 2.14
(out)(err)
O = 1706
T = 0.07
(out)(err)
s2v100c1600_4.wcnf O = 1267
T = 1.93
O = 1267
T = 1.93
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1267
T = 2.16
(out)(err)
O = 1642
T = 0.08
(out)(err)
s2v100c1600_5.wcnf O = 1298
T = 2.52
O = 1298
T = 2.52
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1298
T = 9.47
(out)(err)
O = 1529
T = 0.09
(out)(err)
s2v100c1600_6.wcnf O = 1190
T = 2.34
O = 1190
T = 2.34
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1190
T = 2.67
(out)(err)
O = 1630
T = 0.09
(out)(err)
s2v100c1600_7.wcnf O = 1243
T = 2.37
O = 1243
T = 2.37
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1243
T = 128.12
(out)(err)
O = 1679
T = 0.08
(out)(err)
s2v100c1600_8.wcnf O = 1184
T = 2.23
O = 1184
T = 2.23
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1184
T = 2.25
(out)(err)
O = 1765
T = 0.09
(out)(err)
s2v120c1200_1.wcnf O = 840
T = 2.53
O = 840
T = 2.53
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 840
T = 8.57
(out)(err)
O = 1113
T = 0.07
(out)(err)
s2v120c1200_2.wcnf O = 803
T = 2.72
O = 803
T = 2.72
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 803
T = 18.64
(out)(err)
O = 1105
T = 0.08
(out)(err)
s2v120c1200_3.wcnf O = 834
T = 2.91
O = 834
T = 2.91
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 834
T = 14.88
(out)(err)
O = 1085
T = 0.10
(out)(err)
s2v120c1200_4.wcnf O = 811
T = 2.25
O = 811
T = 2.25
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 811
T = 9.10
(out)(err)
O = 1062
T = 0.06
(out)(err)
s2v120c1200_5.wcnf O = 850
T = 2.40
O = 850
T = 2.52
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 850
T = 2.40
(out)(err)
O = 1098
T = 0.08
(out)(err)
s2v120c1200_6.wcnf O = 784
T = 2.46
O = 784
T = 2.46
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 784
T = 10.02
(out)(err)
O = 1057
T = 0.09
(out)(err)
s2v120c1200_7.wcnf O = 747
T = 2.64
O = 747
T = 2.64
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 747
T = 6.45
(out)(err)
O = 972
T = 0.09
(out)(err)
s2v120c1200_8.wcnf O = 813
T = 2.09
O = 813
T = 2.09
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 813
T = 8.72
(out)(err)
O = 1074
T = 0.10
(out)(err)
s2v120c1300_1.wcnf O = 890
T = 2.89
O = 890
T = 2.89
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 890
T = 15.06
(out)(err)
O = 1114
T = 0.09
(out)(err)
s2v120c1300_2.wcnf O = 847
T = 2.79
O = 847
T = 2.79
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 847
T = 16.80
(out)(err)
O = 1049
T = 0.10
(out)(err)
s2v120c1300_3.wcnf O = 941
T = 2.89
O = 941
T = 2.89
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 941
T = 16.55
(out)(err)
O = 1269
T = 0.10
(out)(err)
s2v120c1300_4.wcnf O = 939
T = 3.24
O = 939
T = 3.24
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 939
T = 5.59
(out)(err)
O = 1197
T = 0.09
(out)(err)
s2v120c1300_5.wcnf O = 949
T = 2.89
O = 949
T = 2.89
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 949
T = 47.35
(out)(err)
O = 1277
T = 0.08
(out)(err)
s2v120c1300_6.wcnf O = 865
T = 2.46
O = 865
T = 3.25
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 865
T = 2.46
(out)(err)
O = 1204
T = 0.06
(out)(err)
s2v120c1300_7.wcnf O = 879
T = 2.19
O = 879
T = 3.40
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 879
T = 2.19
(out)(err)
O = 1264
T = 0.09
(out)(err)
s2v120c1300_8.wcnf O = 868
T = 3.10
O = 868
T = 3.30
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 868
T = 3.10
(out)(err)
O = 1119
T = 0.09
(out)(err)
s2v120c1400_1.wcnf O = 1028
T = 3.72
O = 1028
T = 3.72
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1028
T = 201.84
(out)(err)
O = 1352
T = 0.09
(out)(err)
s2v120c1400_2.wcnf O = 1008
T = 3.22
O = 1008
T = 3.61
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1008
T = 3.22
(out)(err)
O = 1326
T = 0.08
(out)(err)
s2v120c1400_3.wcnf O = 983
T = 3.81
O = 983
T = 3.81
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 983
T = 5.43
(out)(err)
O = 1348
T = 0.09
(out)(err)
s2v120c1400_4.wcnf O = 1007
T = 3.51
O = 1007
T = 3.51
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1007
T = 51.66
(out)(err)
O = 1260
T = 0.08
(out)(err)
s2v120c1400_5.wcnf O = 1108
T = 3.50
O = 1108
T = 3.50
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1108
T = 11.16
(out)(err)
O = 1440
T = 0.08
(out)(err)
s2v120c1400_6.wcnf O = 959
T = 2.73
O = 959
T = 3.55
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 959
T = 2.73
(out)(err)
O = 1228
T = 0.11
(out)(err)
s2v120c1400_7.wcnf O = 1040
T = 2.97
O = 1040
T = 2.97
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1040
T = 16.63
(out)(err)
O = 1304
T = 0.09
(out)(err)
s2v120c1400_8.wcnf O = 1025
T = 3.02
O = 1025
T = 3.02
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1025
T = 131.95
(out)(err)
O = 1323
T = 0.12
(out)(err)
s2v120c1500_1.wcnf O = 1119
T = 3.18
O = 1119
T = 3.18
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1119
T = 18.67
(out)(err)
O = 1505
T = 0.09
(out)(err)
s2v120c1500_2.wcnf O = 1136
T = 2.72
O = 1136
T = 2.72
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1136
T = 14.42
(out)(err)
O = 1483
T = 0.10
(out)(err)
s2v120c1500_3.wcnf O = 1062
T = 2.52
O = 1062
T = 2.52
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1062
T = 3.13
(out)(err)
O = 1365
T = 0.08
(out)(err)
s2v120c1500_4.wcnf O = 1041
T = 2.37
O = 1041
T = 2.37
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1041
T = 8.36
(out)(err)
O = 1447
T = 0.08
(out)(err)
s2v120c1500_5.wcnf O = 1125
T = 3.27
O = 1125
T = 3.40
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1125
T = 3.27
(out)(err)
O = 1600
T = 0.08
(out)(err)
s2v120c1500_6.wcnf O = 1113
T = 2.18
O = 1113
T = 3.54
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1113
T = 2.18
(out)(err)
O = 1504
T = 0.10
(out)(err)
s2v120c1500_7.wcnf O = 1163
T = 3.16
O = 1163
T = 3.16
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1163
T = 13.06
(out)(err)
O = 1451
T = 0.10
(out)(err)
s2v120c1500_8.wcnf O = 1097
T = 2.03
O = 1097
T = 3.50
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1097
T = 2.03
(out)(err)
O = 1505
T = 0.11
(out)(err)
s2v120c1600_1.wcnf O = 1190
T = 1.81
O = 1190
T = 3.63
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1190
T = 1.81
(out)(err)
O = 1595
T = 0.12
(out)(err)
s2v120c1600_2.wcnf O = 1227
T = 2.01
O = 1227
T = 2.64
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1227
T = 2.01
(out)(err)
O = 1630
T = 0.07
(out)(err)
s2v120c1600_3.wcnf O = 1224
T = 2.87
O = 1224
T = 2.87
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1224
T = 6.89
(out)(err)
O = 1615
T = 0.11
(out)(err)
s2v120c1600_4.wcnf O = 1264
T = 2.33
O = 1264
T = 2.33
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1264
T = 2.80
(out)(err)
O = 1786
T = 0.13
(out)(err)
s2v120c1600_5.wcnf O = 1252
T = 2.37
O = 1252
T = 2.47
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1252
T = 2.37
(out)(err)
O = 1715
T = 0.10
(out)(err)
s2v120c1600_6.wcnf O = 1246
T = 3.23
O = 1246
T = 3.23
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1246
T = 6.43
(out)(err)
O = 1665
T = 0.13
(out)(err)
s2v120c1600_7.wcnf O = 1159
T = 2.67
O = 1159
T = 2.67
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1159
T = 7.03
(out)(err)
O = 1511
T = 0.12
(out)(err)
s2v120c1600_8.wcnf O = 1150
T = 2.95
O = 1150
T = 2.95
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1150
T = 102.68
(out)(err)
O = 1555
T = 0.13
(out)(err)
s2v140c1200_1.wcnf O = 780
T = 3.29
O = 780
T = 3.29
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 780
T = 9.52
(out)(err)
O = 1035
T = 0.11
(out)(err)
s2v140c1200_2.wcnf O = 733
T = 3.45
O = 733
T = 3.45
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 733
T = 90.22
(out)(err)
O = 1004
T = 0.07
(out)(err)
s2v140c1200_3.wcnf O = 741
T = 3.77
O = 741
T = 3.77
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 741
T = 45.99
(out)(err)
O = 1018
T = 0.09
(out)(err)
s2v140c1200_4.wcnf O = 667
T = 4.15
O = 667
T = 4.15
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 667
T = 5.52
(out)(err)
O = 933
T = 0.09
(out)(err)
s2v140c1200_5.wcnf O = 714
T = 3.77
O = 714
T = 3.77
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 714
T = 5.71
(out)(err)
O = 969
T = 0.10
(out)(err)
s2v140c1200_6.wcnf O = 803
T = 4.35
O = 803
T = 4.35
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 803
T = 11.15
(out)(err)
O = 1096
T = 0.08
(out)(err)
s2v140c1200_7.wcnf O = 774
T = 4.10
O = 774
T = 4.10
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 774
T = 184.15
(out)(err)
O = 1051
T = 0.07
(out)(err)
s2v140c1200_8.wcnf O = 745
T = 4.40
O = 745
T = 4.40
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 745
T = 10.77
(out)(err)
O = 994
T = 0.08
(out)(err)
s2v140c1300_1.wcnf O = 846
T = 4.16
O = 846
T = 4.55
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 846
T = 4.16
(out)(err)
O = 1379
T = 0.10
(out)(err)
s2v140c1300_2.wcnf O = 774
T = 3.81
O = 774
T = 3.81
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 774
T = 4.08
(out)(err)
O = 1043
T = 0.08
(out)(err)
s2v140c1300_3.wcnf O = 832
T = 4.68
O = 832
T = 4.68
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 832
T = 229.22
(out)(err)
O = 1108
T = 0.10
(out)(err)
s2v140c1300_4.wcnf O = 871
T = 4.41
O = 871
T = 4.41
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 872
T = 42.25
(out)(err)
O = 1229
T = 0.11
(out)(err)
s2v140c1300_5.wcnf O = 844
T = 4.40
O = 844
T = 4.40
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 844
T = 6.83
(out)(err)
O = 1054
T = 0.10
(out)(err)
s2v140c1300_6.wcnf O = 884
T = 4.49
O = 884
T = 4.49
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 884
T = 6.03
(out)(err)
O = 1185
T = 0.11
(out)(err)
s2v140c1300_7.wcnf O = 874
T = 3.35
O = 874
T = 4.10
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 874
T = 3.35
(out)(err)
O = 1179
T = 0.12
(out)(err)
s2v140c1300_8.wcnf O = 812
T = 3.02
O = 812
T = 3.02
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 812
T = 60.37
(out)(err)
O = 1076
T = 0.09
(out)(err)
s2v140c1400_1.wcnf O = 926
T = 2.55
O = 926
T = 2.82
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 926
T = 2.55
(out)(err)
O = 1204
T = 0.12
(out)(err)
s2v140c1400_2.wcnf O = 879
T = 3.05
O = 879
T = 3.05
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 879
T = 12.09
(out)(err)
O = 1118
T = 0.09
(out)(err)
s2v140c1400_3.wcnf O = 936
T = 3.41
O = 936
T = 3.41
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 936
T = 23.93
(out)(err)
O = 1286
T = 0.11
(out)(err)
s2v140c1400_4.wcnf O = 932
T = 2.53
O = 932
T = 3.94
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 932
T = 2.53
(out)(err)
O = 1286
T = 0.12
(out)(err)
s2v140c1400_5.wcnf O = 968
T = 3.61
O = 968
T = 3.61
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 968
T = 3.85
(out)(err)
O = 1218
T = 0.09
(out)(err)
s2v140c1400_6.wcnf O = 967
T = 3.01
O = 967
T = 3.12
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 967
T = 3.01
(out)(err)
O = 1186
T = 0.08
(out)(err)
s2v140c1400_7.wcnf O = 923
T = 3.18
O = 923
T = 3.18
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 923
T = 18.19
(out)(err)
O = 1253
T = 0.12
(out)(err)
s2v140c1400_8.wcnf O = 957
T = 2.74
O = 957
T = 3.33
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 957
T = 2.74
(out)(err)
O = 1288
T = 0.11
(out)(err)
s2v140c1500_1.wcnf O = 986
T = 2.92
O = 986
T = 3.58
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 986
T = 2.92
(out)(err)
O = 1385
T = 0.08
(out)(err)
s2v140c1500_2.wcnf O = 998
T = 3.43
O = 998
T = 3.43
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 998
T = 9.37
(out)(err)
O = 1300
T = 0.08
(out)(err)
s2v140c1500_3.wcnf O = 1073
T = 2.98
O = 1073
T = 2.98
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1073
T = 39.08
(out)(err)
O = 1402
T = 0.09
(out)(err)
s2v140c1500_4.wcnf O = 1047
T = 2.24
O = 1047
T = 2.24
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1047
T = 221.52
(out)(err)
O = 1454
T = 0.09
(out)(err)
s2v140c1500_5.wcnf O = 1058
T = 2.38
O = 1058
T = 2.38
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1058
T = 9.70
(out)(err)
O = 1508
T = 0.12
(out)(err)
s2v140c1500_6.wcnf O = 1102
T = 3.59
O = 1102
T = 3.59
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1102
T = 96.49
(out)(err)
O = 1549
T = 0.12
(out)(err)
s2v140c1500_7.wcnf O = 1010
T = 2.98
O = 1010
T = 2.98
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1011
T = 102.57
(out)(err)
O = 1285
T = 0.09
(out)(err)
s2v140c1500_8.wcnf O = 1045
T = 2.39
O = 1045
T = 2.39
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1045
T = 29.50
(out)(err)
O = 1428
T = 0.12
(out)(err)
s2v140c1600_1.wcnf O = 1143
T = 2.59
O = 1143
T = 2.59
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1143
T = 41.59
(out)(err)
O = 1460
T = 0.11
(out)(err)
s2v140c1600_2.wcnf O = 1140
T = 3.35
O = 1140
T = 3.35
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1140
T = 15.74
(out)(err)
O = 1546
T = 0.12
(out)(err)
s2v140c1600_3.wcnf O = 1079
T = 2.42
O = 1079
T = 2.42
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1080
T = 7.19
(out)(err)
O = 1423
T = 0.11
(out)(err)
s2v140c1600_4.wcnf O = 1157
T = 3.13
O = 1157
T = 4.37
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1157
T = 3.13
(out)(err)
O = 1653
T = 0.10
(out)(err)
s2v140c1600_5.wcnf O = 1119
T = 2.86
O = 1119
T = 2.86
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1119
T = 4.00
(out)(err)
O = 1425
T = 0.09
(out)(err)
s2v140c1600_6.wcnf O = 1212
T = 3.92
O = 1212
T = 3.92
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1212
T = 26.06
(out)(err)
O = 1646
T = 0.11
(out)(err)
s2v140c1600_7.wcnf O = 1150
T = 3.21
O = 1150
T = 3.21
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1150
T = 16.06
(out)(err)
O = 1422
T = 0.13
(out)(err)
s2v140c1600_8.wcnf O = 1180
T = 2.79
O = 1180
T = 2.79
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 1180
T = 58.22
(out)(err)
O = 1590
T = 0.13
(out)(err)
file_rwms_wcnf_L3_V70_C1000_0.wcnf O = 198
T = 1.37
O = 198
T = 2.51
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 198
T = 1.37
(out)(err)
O = 495
T = 0.13
(out)(err)
file_rwms_wcnf_L3_V70_C1000_1.wcnf O = 212
T = 1.58
O = 212
T = 1.83
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 212
T = 1.58
(out)(err)
O = 450
T = 0.13
(out)(err)
file_rwms_wcnf_L3_V70_C1000_2.wcnf O = 211
T = 1.71
O = 211
T = 1.71
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 211
T = 17.17
(out)(err)
O = 452
T = 0.13
(out)(err)
file_rwms_wcnf_L3_V70_C1000_3.wcnf O = 229
T = 1.43
O = 229
T = 1.43
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 229
T = 1.94
(out)(err)
O = 495
T = 0.12
(out)(err)
file_rwms_wcnf_L3_V70_C1000_4.wcnf O = 202
T = 1.67
O = 202
T = 1.67
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 202
T = 5.54
(out)(err)
O = 453
T = 0.12
(out)(err)
file_rwms_wcnf_L3_V70_C1000_5.wcnf O = 214
T = 2.20
O = 214
T = 2.32
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 214
T = 2.20
(out)(err)
O = 444
T = 0.11
(out)(err)
file_rwms_wcnf_L3_V70_C1000_6.wcnf O = 203
T = 1.78
O = 203
T = 1.93
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 203
T = 1.78
(out)(err)
O = 526
T = 0.11
(out)(err)
file_rwms_wcnf_L3_V70_C1000_7.wcnf O = 200
T = 1.41
O = 200
T = 1.64
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 200
T = 1.41
(out)(err)
O = 499
T = 0.10
(out)(err)
file_rwms_wcnf_L3_V70_C1000_8.wcnf O = 188
T = 2.37
O = 188
T = 2.78
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 188
T = 2.37
(out)(err)
O = 393
T = 0.09
(out)(err)
file_rwms_wcnf_L3_V70_C1000_9.wcnf O = 226
T = 1.30
O = 226
T = 1.99
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 226
T = 1.30
(out)(err)
O = 445
T = 0.08
(out)(err)
file_rwms_wcnf_L3_V70_C700_0.wcnf O = 103
T = 1.77
O = 103
T = 1.77
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 103
T = 1.97
(out)(err)
O = 247
T = 0.10
(out)(err)
file_rwms_wcnf_L3_V70_C700_1.wcnf O = 107
T = 2.06
O = 107
T = 2.06
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 107
T = 4.09
(out)(err)
O = 139
T = 46.91
(out)(err)
file_rwms_wcnf_L3_V70_C700_2.wcnf O = 110
T = 1.91
O = 110
T = 1.91
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 110
T = 8.65
(out)(err)
O = 162
T = 1.72
(out)(err)
file_rwms_wcnf_L3_V70_C700_3.wcnf O = 102
T = 1.45
O = 102
T = 1.91
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 102
T = 1.45
(out)(err)
O = 294
T = 0.09
(out)(err)
file_rwms_wcnf_L3_V70_C700_4.wcnf O = 110
T = 1.89
O = 110
T = 2.02
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 110
T = 1.89
(out)(err)
O = 247
T = 0.12
(out)(err)
file_rwms_wcnf_L3_V70_C700_5.wcnf O = 103
T = 1.15
O = 103
T = 2.49
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 103
T = 1.15
(out)(err)
O = 183
T = 10.09
(out)(err)
file_rwms_wcnf_L3_V70_C700_6.wcnf O = 102
T = 0.91
O = 102
T = 2.10
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 102
T = 0.91
(out)(err)
O = 254
T = 0.11
(out)(err)
file_rwms_wcnf_L3_V70_C700_7.wcnf O = 104
T = 1.24
O = 104
T = 2.23
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 104
T = 1.24
(out)(err)
O = 145
T = 0.70
(out)(err)
file_rwms_wcnf_L3_V70_C700_8.wcnf O = 82
T = 1.00
O = 82
T = 2.24
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 82
T = 1.00
(out)(err)
O = 166
T = 2.92
(out)(err)
file_rwms_wcnf_L3_V70_C700_9.wcnf O = 104
T = 1.84
O = 104
T = 1.84
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 104
T = 2.29
(out)(err)
O = 259
T = 0.13
(out)(err)
file_rwms_wcnf_L3_V70_C800_0.wcnf O = 132
T = 1.87
O = 132
T = 1.87
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 132
T = 2.25
(out)(err)
O = 166
T = 0.82
(out)(err)
file_rwms_wcnf_L3_V70_C800_1.wcnf O = 138
T = 2.09
O = 138
T = 2.09
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 138
T = 11.00
(out)(err)
O = 290
T = 0.11
(out)(err)
file_rwms_wcnf_L3_V70_C800_2.wcnf O = 127
T = 1.47
O = 127
T = 1.47
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 127
T = 1.76
(out)(err)
O = 296
T = 0.08
(out)(err)
file_rwms_wcnf_L3_V70_C800_3.wcnf O = 134
T = 1.79
O = 134
T = 2.01
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 134
T = 1.79
(out)(err)
O = 356
T = 0.10
(out)(err)
file_rwms_wcnf_L3_V70_C800_4.wcnf O = 143
T = 1.47
O = 143
T = 2.16
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 143
T = 1.47
(out)(err)
O = 210
T = 9.47
(out)(err)
file_rwms_wcnf_L3_V70_C800_5.wcnf O = 144
T = 1.21
O = 144
T = 1.21
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 144
T = 3.28
(out)(err)
O = 327
T = 0.09
(out)(err)
file_rwms_wcnf_L3_V70_C800_6.wcnf O = 135
T = 2.23
O = 135
T = 2.23
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 135
T = 2.57
(out)(err)
O = 297
T = 0.12
(out)(err)
file_rwms_wcnf_L3_V70_C800_7.wcnf O = 147
T = 1.79
O = 147
T = 2.17
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 147
T = 1.79
(out)(err)
O = 323
T = 0.11
(out)(err)
file_rwms_wcnf_L3_V70_C800_8.wcnf O = 126
T = 1.26
O = 126
T = 2.13
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 126
T = 1.26
(out)(err)
O = 390
T = 0.04
(out)(err)
file_rwms_wcnf_L3_V70_C800_9.wcnf O = 138
T = 1.47
O = 138
T = 2.56
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 138
T = 1.47
(out)(err)
O = 331
T = 0.11
(out)(err)
file_rwms_wcnf_L3_V70_C900_0.wcnf O = 157
T = 1.40
O = 157
T = 2.05
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 157
T = 1.40
(out)(err)
O = 364
T = 0.04
(out)(err)
file_rwms_wcnf_L3_V70_C900_1.wcnf O = 192
T = 2.42
O = 192
T = 2.42
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 192
T = 4.51
(out)(err)
O = 543
T = 0.12
(out)(err)
file_rwms_wcnf_L3_V70_C900_2.wcnf O = 177
T = 1.81
O = 177
T = 2.23
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 177
T = 1.81
(out)(err)
O = 405
T = 0.08
(out)(err)
file_rwms_wcnf_L3_V70_C900_3.wcnf O = 163
T = 1.57
O = 163
T = 2.06
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 163
T = 1.57
(out)(err)
O = 203
T = 146.17
(out)(err)
file_rwms_wcnf_L3_V70_C900_4.wcnf O = 171
T = 1.68
O = 171
T = 2.51
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 171
T = 1.68
(out)(err)
O = 329
T = 0.13
(out)(err)
file_rwms_wcnf_L3_V70_C900_5.wcnf O = 175
T = 1.98
O = 175
T = 1.98
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 175
T = 5.81
(out)(err)
O = 351
T = 0.08
(out)(err)
file_rwms_wcnf_L3_V70_C900_6.wcnf O = 174
T = 1.68
O = 174
T = 2.31
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 174
T = 1.68
(out)(err)
O = 222
T = 32.45
(out)(err)
file_rwms_wcnf_L3_V70_C900_7.wcnf O = 194
T = 2.29
O = 194
T = 2.29
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 194
T = 3.35
(out)(err)
O = 369
T = 0.09
(out)(err)
file_rwms_wcnf_L3_V70_C900_8.wcnf O = 179
T = 1.35
O = 179
T = 1.83
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 179
T = 1.35
(out)(err)
O = 430
T = 0.08
(out)(err)
file_rwms_wcnf_L3_V70_C900_9.wcnf O = 181
T = 1.50
O = 181
T = 2.06
(out)(err)
O = N/A
T = TO
(out)(err)
O = N/A
T = TO
(out)(err)
O = 181
T = 1.50
(out)(err)
O = 411
T = 0.08
(out)(err)