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 Sat4j-i ubcsat-irots
HG-3SAT-V250-C1000-1.cnf O = 5
T = 6.61		 O = 35
T = 2.98
(out)(err)		 O = 5
T = 6.61
(out)(err)
HG-3SAT-V250-C1000-10.cnf O = 6
T = 5.84		 O = 40
T = 6.27
(out)(err)		 O = 6
T = 5.84
(out)(err)
HG-3SAT-V250-C1000-100.cnf O = 6
T = 4.82		 O = 37
T = 65.74
(out)(err)		 O = 6
T = 4.82
(out)(err)
HG-3SAT-V250-C1000-11.cnf O = 6
T = 3.31		 O = 34
T = 8.18
(out)(err)		 O = 6
T = 3.31
(out)(err)
HG-3SAT-V250-C1000-12.cnf O = 6
T = 4.28		 O = 45
T = 58.35
(out)(err)		 O = 6
T = 4.28
(out)(err)
HG-3SAT-V250-C1000-13.cnf O = 5
T = 1.79		 O = 38
T = 192.95
(out)(err)		 O = 5
T = 1.79
(out)(err)
HG-3SAT-V250-C1000-14.cnf O = 5
T = 16.25		 O = 37
T = 169.92
(out)(err)		 O = 5
T = 16.25
(out)(err)
HG-3SAT-V250-C1000-15.cnf O = 5
T = 5.61		 O = 39
T = 175.23
(out)(err)		 O = 5
T = 5.61
(out)(err)
HG-3SAT-V250-C1000-16.cnf O = 5
T = 5.06		 O = 44
T = 25.44
(out)(err)		 O = 5
T = 5.06
(out)(err)
HG-3SAT-V250-C1000-17.cnf O = 6
T = 3.32		 O = 38
T = 3.74
(out)(err)		 O = 6
T = 3.32
(out)(err)
HG-3SAT-V250-C1000-18.cnf O = 6
T = 3.97		 O = 36
T = 45.50
(out)(err)		 O = 6
T = 3.97
(out)(err)
HG-3SAT-V250-C1000-19.cnf O = 5
T = 4.38		 O = 41
T = 5.84
(out)(err)		 O = 5
T = 4.38
(out)(err)
HG-3SAT-V250-C1000-2.cnf O = 5
T = 6.62		 O = 36
T = 5.41
(out)(err)		 O = 5
T = 6.62
(out)(err)
HG-3SAT-V250-C1000-20.cnf O = 7
T = 3.89		 O = 36
T = 4.06
(out)(err)		 O = 7
T = 3.89
(out)(err)
HG-3SAT-V250-C1000-21.cnf O = 4
T = 3.69		 O = 39
T = 64.86
(out)(err)		 O = 4
T = 3.69
(out)(err)
HG-3SAT-V250-C1000-22.cnf O = 5
T = 5.00		 O = 36
T = 2.68
(out)(err)		 O = 5
T = 5.00
(out)(err)
HG-3SAT-V250-C1000-23.cnf O = 6
T = 3.54		 O = 40
T = 15.43
(out)(err)		 O = 6
T = 3.54
(out)(err)
HG-3SAT-V250-C1000-24.cnf O = 5
T = 5.72		 O = 46
T = 1.95
(out)(err)		 O = 5
T = 5.72
(out)(err)
HG-3SAT-V250-C1000-3.cnf O = 5
T = 4.60		 O = 40
T = 4.12
(out)(err)		 O = 5
T = 4.60
(out)(err)
HG-3SAT-V250-C1000-4.cnf O = 6
T = 4.36		 O = 37
T = 12.38
(out)(err)		 O = 6
T = 4.36
(out)(err)
HG-3SAT-V250-C1000-5.cnf O = 6
T = 1.17		 O = 42
T = 1.91
(out)(err)		 O = 6
T = 1.17
(out)(err)
HG-3SAT-V250-C1000-6.cnf O = 6
T = 6.89		 O = 37
T = 141.79
(out)(err)		 O = 6
T = 6.89
(out)(err)
HG-3SAT-V250-C1000-7.cnf O = 6
T = 3.88		 O = 39
T = 4.46
(out)(err)		 O = 6
T = 3.88
(out)(err)
HG-3SAT-V250-C1000-8.cnf O = 5
T = 5.46		 O = 31
T = 14.30
(out)(err)		 O = 5
T = 5.46
(out)(err)
HG-3SAT-V250-C1000-9.cnf O = 6
T = 4.23		 O = 35
T = 12.98
(out)(err)		 O = 6
T = 4.23
(out)(err)
HG-3SAT-V300-C1200-1.cnf O = 6
T = 120.60		 O = 51
T = 146.44
(out)(err)		 O = 6
T = 120.60
(out)(err)
HG-3SAT-V300-C1200-10.cnf O = 7
T = 5.42		 O = 44
T = 59.01
(out)(err)		 O = 7
T = 5.42
(out)(err)
HG-3SAT-V300-C1200-100.cnf O = 6
T = 2.16		 O = 43
T = 237.51
(out)(err)		 O = 6
T = 2.16
(out)(err)
HG-3SAT-V300-C1200-11.cnf O = 6
T = 8.65		 O = 46
T = 103.43
(out)(err)		 O = 6
T = 8.65
(out)(err)
HG-3SAT-V300-C1200-12.cnf O = 7
T = 7.34		 O = 44
T = 30.35
(out)(err)		 O = 7
T = 7.34
(out)(err)
HG-3SAT-V300-C1200-13.cnf O = 6
T = 9.59		 O = 49
T = 78.76
(out)(err)		 O = 6
T = 9.59
(out)(err)
HG-3SAT-V300-C1200-14.cnf O = 6
T = 8.96		 O = 42
T = 36.17
(out)(err)		 O = 6
T = 8.96
(out)(err)
HG-3SAT-V300-C1200-15.cnf O = 7
T = 9.15		 O = 45
T = 90.14
(out)(err)		 O = 7
T = 9.15
(out)(err)
HG-3SAT-V300-C1200-16.cnf O = 6
T = 8.49		 O = 47
T = 104.11
(out)(err)		 O = 6
T = 8.49
(out)(err)
HG-3SAT-V300-C1200-17.cnf O = 7
T = 7.04		 O = 49
T = 180.89
(out)(err)		 O = 7
T = 7.04
(out)(err)
HG-3SAT-V300-C1200-18.cnf O = 7
T = 6.51		 O = 50
T = 51.93
(out)(err)		 O = 7
T = 6.51
(out)(err)
HG-3SAT-V300-C1200-19.cnf O = 6
T = 3.10		 O = 50
T = 108.91
(out)(err)		 O = 6
T = 3.10
(out)(err)
HG-3SAT-V300-C1200-2.cnf O = 5
T = 9.09		 O = 47
T = 29.11
(out)(err)		 O = 5
T = 9.09
(out)(err)
HG-3SAT-V300-C1200-20.cnf O = 6
T = 8.19		 O = 48
T = 49.33
(out)(err)		 O = 6
T = 8.19
(out)(err)
HG-3SAT-V300-C1200-21.cnf O = 5
T = 7.97		 O = 39
T = 132.22
(out)(err)		 O = 5
T = 7.97
(out)(err)
HG-3SAT-V300-C1200-22.cnf O = 6
T = 8.49		 O = 46
T = 22.74
(out)(err)		 O = 6
T = 8.49
(out)(err)
HG-3SAT-V300-C1200-23.cnf O = 7
T = 8.72		 O = 47
T = 51.25
(out)(err)		 O = 7
T = 8.72
(out)(err)
HG-3SAT-V300-C1200-24.cnf O = 7
T = 8.69		 O = 44
T = 158.94
(out)(err)		 O = 7
T = 8.69
(out)(err)
HG-3SAT-V300-C1200-3.cnf O = 6
T = 12.43		 O = 45
T = 149.17
(out)(err)		 O = 6
T = 12.43
(out)(err)
HG-3SAT-V300-C1200-4.cnf O = 7
T = 5.41		 O = 48
T = 13.29
(out)(err)		 O = 7
T = 5.41
(out)(err)
HG-3SAT-V300-C1200-5.cnf O = 6
T = 4.63		 O = 45
T = 131.79
(out)(err)		 O = 6
T = 4.63
(out)(err)
HG-3SAT-V300-C1200-6.cnf O = 6
T = 7.47		 O = 48
T = 5.39
(out)(err)		 O = 6
T = 7.47
(out)(err)
HG-3SAT-V300-C1200-7.cnf O = 5
T = 5.90		 O = 47
T = 97.31
(out)(err)		 O = 5
T = 5.90
(out)(err)
HG-3SAT-V300-C1200-8.cnf O = 7
T = 7.67		 O = 47
T = 8.28
(out)(err)		 O = 7
T = 7.67
(out)(err)
HG-3SAT-V300-C1200-9.cnf O = 7
T = 1.68		 O = 47
T = 3.21
(out)(err)		 O = 7
T = 1.68
(out)(err)
HG-4SAT-V100-C900-14.cnf O = 2
T = 3.00		 O = 23
T = 1.84
(out)(err)		 O = 2
T = 3.00
(out)(err)
HG-4SAT-V100-C900-19.cnf O = 2
T = 1.75		 O = 16
T = 100.04
(out)(err)		 O = 2
T = 1.75
(out)(err)
HG-4SAT-V100-C900-2.cnf O = 2
T = 1.90		 O = 20
T = 2.81
(out)(err)		 O = 2
T = 1.90
(out)(err)
HG-4SAT-V100-C900-20.cnf O = 2
T = 3.24		 O = 19
T = 11.74
(out)(err)		 O = 2
T = 3.24
(out)(err)
HG-4SAT-V100-C900-23.cnf O = 2
T = 2.80		 O = 25
T = 4.46
(out)(err)		 O = 2
T = 2.80
(out)(err)
HG-4SAT-V100-C900-4.cnf O = 2
T = 4.40		 O = 25
T = 1.88
(out)(err)		 O = 2
T = 4.40
(out)(err)
HG-4SAT-V100-C900-7.cnf O = 2
T = 0.39		 O = 16
T = 8.82
(out)(err)		 O = 2
T = 0.39
(out)(err)
HG-4SAT-V150-C1350-1.cnf O = 1
T = 1.93		 O = 31
T = 8.08
(out)(err)		 O = 1
T = 1.93
(out)(err)
HG-4SAT-V150-C1350-10.cnf O = 1
T = 2.76		 O = 29
T = 153.29
(out)(err)		 O = 1
T = 2.76
(out)(err)
HG-4SAT-V150-C1350-100.cnf O = 1
T = 2.70		 O = 30
T = 1.20
(out)(err)		 O = 1
T = 2.70
(out)(err)
HG-4SAT-V150-C1350-11.cnf O = 1
T = 3.16		 O = 33
T = 11.61
(out)(err)		 O = 1
T = 3.16
(out)(err)
HG-4SAT-V150-C1350-12.cnf O = 2
T = 2.85		 O = 29
T = 3.60
(out)(err)		 O = 2
T = 2.85
(out)(err)
HG-4SAT-V150-C1350-13.cnf O = 1
T = 1.21		 O = 31
T = 8.56
(out)(err)		 O = 1
T = 1.21
(out)(err)
HG-4SAT-V150-C1350-14.cnf O = 1
T = 4.78		 O = 32
T = 57.72
(out)(err)		 O = 1
T = 4.78
(out)(err)
HG-4SAT-V150-C1350-15.cnf O = 1
T = 3.03		 O = 39
T = 87.82
(out)(err)		 O = 1
T = 3.03
(out)(err)
HG-4SAT-V150-C1350-16.cnf O = 1
T = 17.23		 O = 35
T = 2.73
(out)(err)		 O = 1
T = 17.23
(out)(err)
HG-4SAT-V150-C1350-17.cnf O = 2
T = 0.64		 O = 28
T = 217.69
(out)(err)		 O = 2
T = 0.64
(out)(err)
HG-4SAT-V150-C1350-18.cnf O = 1
T = 4.41		 O = 30
T = 231.46
(out)(err)		 O = 1
T = 4.41
(out)(err)
HG-4SAT-V150-C1350-19.cnf O = 1
T = 4.51		 O = 32
T = 122.15
(out)(err)		 O = 1
T = 4.51
(out)(err)
HG-4SAT-V150-C1350-2.cnf O = 1
T = 4.41		 O = 27
T = 233.88
(out)(err)		 O = 1
T = 4.41
(out)(err)
HG-4SAT-V150-C1350-20.cnf O = 1
T = 3.72		 O = 23
T = 21.82
(out)(err)		 O = 1
T = 3.72
(out)(err)
HG-4SAT-V150-C1350-21.cnf O = 1
T = 28.24		 O = 26
T = 252.24
(out)(err)		 O = 1
T = 28.24
(out)(err)
HG-4SAT-V150-C1350-22.cnf O = 1
T = 4.49		 O = 34
T = 16.41
(out)(err)		 O = 1
T = 4.49
(out)(err)
HG-4SAT-V150-C1350-23.cnf O = 0
T = 0.01		 O = 33
T = 40.09
(out)(err)		 O = 0
T = 0.01
(out)(err)
HG-4SAT-V150-C1350-24.cnf O = 2
T = 3.81		 O = 21
T = 40.72
(out)(err)		 O = 2
T = 3.81
(out)(err)
HG-4SAT-V150-C1350-3.cnf O = 1
T = 4.75		 O = 30
T = 91.02
(out)(err)		 O = 1
T = 4.75
(out)(err)
HG-4SAT-V150-C1350-4.cnf O = 1
T = 4.39		 O = 29
T = 165.65
(out)(err)		 O = 1
T = 4.39
(out)(err)
HG-4SAT-V150-C1350-5.cnf O = 2
T = 4.79		 O = 29
T = 3.15
(out)(err)		 O = 2
T = 4.79
(out)(err)
HG-4SAT-V150-C1350-6.cnf O = 1
T = 4.92		 O = 28
T = 258.99
(out)(err)		 O = 1
T = 4.92
(out)(err)
HG-4SAT-V150-C1350-7.cnf O = 1
T = 4.54		 O = 32
T = 178.69
(out)(err)		 O = 1
T = 4.54
(out)(err)
HG-4SAT-V150-C1350-8.cnf O = 2
T = 4.18		 O = 31
T = 144.14
(out)(err)		 O = 2
T = 4.18
(out)(err)
HG-4SAT-V150-C1350-9.cnf O = 2
T = 5.17		 O = 34
T = 2.22
(out)(err)		 O = 2
T = 5.17
(out)(err)
s2v120c1200-1.cnf O = 161
T = 3.81		 O = 230
T = 6.26
(out)(err)		 O = 161
T = 3.81
(out)(err)
s2v120c1200-10.cnf O = 154
T = 3.76		 O = 221
T = 3.23
(out)(err)		 O = 154
T = 3.76
(out)(err)
s2v120c1200-2.cnf O = 159
T = 5.03		 O = 246
T = 2.84
(out)(err)		 O = 159
T = 5.03
(out)(err)
s2v120c1200-3.cnf O = 160
T = 0.31		 O = 247
T = 3.26
(out)(err)		 O = 160
T = 0.31
(out)(err)
s2v120c1200-4.cnf O = 157
T = 5.58		 O = 233
T = 0.76
(out)(err)		 O = 157
T = 5.58
(out)(err)
s2v120c1200-5.cnf O = 143
T = 4.44		 O = 217
T = 3.50
(out)(err)		 O = 143
T = 4.44
(out)(err)
s2v120c1200-6.cnf O = 167
T = 4.74		 O = 245
T = 3.45
(out)(err)		 O = 167
T = 4.74
(out)(err)
s2v120c1200-7.cnf O = 162
T = 4.25		 O = 224
T = 5.81
(out)(err)		 O = 162
T = 4.25
(out)(err)
s2v120c1200-8.cnf O = 165
T = 4.35		 O = 246
T = 2.69
(out)(err)		 O = 165
T = 4.35
(out)(err)
s2v120c1200-9.cnf O = 148
T = 3.24		 O = 222
T = 3.20
(out)(err)		 O = 148
T = 3.24
(out)(err)
s2v120c1300-1.cnf O = 180
T = 4.14		 O = 251
T = 2.74
(out)(err)		 O = 180
T = 4.14
(out)(err)
s2v120c1300-10.cnf O = 180
T = 3.21		 O = 260
T = 2.94
(out)(err)		 O = 180
T = 3.21
(out)(err)
s2v120c1300-2.cnf O = 172
T = 3.95		 O = 259
T = 4.86
(out)(err)		 O = 172
T = 3.95
(out)(err)
s2v120c1300-3.cnf O = 173
T = 5.09		 O = 258
T = 2.92
(out)(err)		 O = 173
T = 5.09
(out)(err)
s2v120c1300-4.cnf O = 176
T = 3.53		 O = 277
T = 2.96
(out)(err)		 O = 176
T = 3.53
(out)(err)
s2v120c1300-5.cnf O = 168
T = 4.66		 O = 275
T = 2.53
(out)(err)		 O = 168
T = 4.66
(out)(err)
s2v120c1300-6.cnf O = 180
T = 5.20		 O = 242
T = 3.90
(out)(err)		 O = 180
T = 5.20
(out)(err)
s2v120c1300-7.cnf O = 169
T = 4.07		 O = 260
T = 1.73
(out)(err)		 O = 169
T = 4.07
(out)(err)
s2v120c1300-8.cnf O = 174
T = 4.58		 O = 275
T = 1.41
(out)(err)		 O = 174
T = 4.58
(out)(err)
s2v120c1300-9.cnf O = 186
T = 4.48		 O = 273
T = 1.45
(out)(err)		 O = 186
T = 4.48
(out)(err)
s2v120c1400-1.cnf O = 197
T = 4.22		 O = 270
T = 3.39
(out)(err)		 O = 197
T = 4.22
(out)(err)
s2v120c1400-10.cnf O = 211
T = 5.63		 O = 272
T = 5.51
(out)(err)		 O = 211
T = 5.63
(out)(err)
s2v120c1400-2.cnf O = 191
T = 4.36		 O = 327
T = 4.49
(out)(err)		 O = 191
T = 4.36
(out)(err)
s2v120c1400-3.cnf O = 189
T = 5.37		 O = 305
T = 3.92
(out)(err)		 O = 189
T = 5.37
(out)(err)
s2v120c1400-4.cnf O = 200
T = 4.81		 O = 261
T = 3.78
(out)(err)		 O = 200
T = 4.81
(out)(err)
s2v120c1400-5.cnf O = 199
T = 5.37		 O = 278
T = 4.53
(out)(err)		 O = 199
T = 5.37
(out)(err)
s2v120c1400-6.cnf O = 196
T = 4.73		 O = 272
T = 3.34
(out)(err)		 O = 196
T = 4.73
(out)(err)
s2v120c1400-7.cnf O = 206
T = 5.01		 O = 272
T = 3.85
(out)(err)		 O = 206
T = 5.01
(out)(err)
s2v120c1400-8.cnf O = 194
T = 4.16		 O = 278
T = 2.53
(out)(err)		 O = 194
T = 4.16
(out)(err)
s2v120c1400-9.cnf O = 198
T = 4.27		 O = 295
T = 3.56
(out)(err)		 O = 198
T = 4.27
(out)(err)
s2v120c1500-1.cnf O = 211
T = 5.32		 O = 294
T = 4.49
(out)(err)		 O = 211
T = 5.32
(out)(err)
s2v120c1500-10.cnf O = 213
T = 4.89		 O = 294
T = 4.34
(out)(err)		 O = 213
T = 4.89
(out)(err)
s2v120c1500-2.cnf O = 213
T = 2.21		 O = 330
T = 3.24
(out)(err)		 O = 213
T = 2.21
(out)(err)
s2v120c1500-3.cnf O = 207
T = 1.42		 O = 305
T = 3.07
(out)(err)		 O = 207
T = 1.42
(out)(err)
s2v120c1500-4.cnf O = 212
T = 0.58		 O = 298
T = 2.70
(out)(err)		 O = 212
T = 0.58
(out)(err)
s2v120c1500-5.cnf O = 233
T = 0.55		 O = 317
T = 1.88
(out)(err)		 O = 233
T = 0.55
(out)(err)
s2v120c1500-6.cnf O = 209
T = 2.71		 O = 302
T = 3.93
(out)(err)		 O = 209
T = 2.71
(out)(err)
s2v120c1500-7.cnf O = 216
T = 2.66		 O = 316
T = 3.62
(out)(err)		 O = 216
T = 2.66
(out)(err)
s2v120c1500-8.cnf O = 212
T = 1.73		 O = 314
T = 3.34
(out)(err)		 O = 212
T = 1.73
(out)(err)
s2v120c1500-9.cnf O = 223
T = 1.57		 O = 316
T = 5.28
(out)(err)		 O = 223
T = 1.57
(out)(err)
s2v120c1600-1.cnf O = 233
T = 0.69		 O = 312
T = 4.86
(out)(err)		 O = 233
T = 0.69
(out)(err)
s2v120c1600-10.cnf O = 233
T = 6.24		 O = 320
T = 3.73
(out)(err)		 O = 233
T = 6.24
(out)(err)
s2v120c1600-2.cnf O = 239
T = 4.29		 O = 350
T = 2.67
(out)(err)		 O = 239
T = 4.29
(out)(err)
s2v120c1600-3.cnf O = 233
T = 5.34		 O = 321
T = 2.77
(out)(err)		 O = 233
T = 5.34
(out)(err)
s2v120c1600-4.cnf O = 219
T = 4.30		 O = 319
T = 0.72
(out)(err)		 O = 219
T = 4.30
(out)(err)
s2v120c1600-5.cnf O = 247
T = 4.39		 O = 338
T = 0.83
(out)(err)		 O = 247
T = 4.39
(out)(err)
s2v120c1600-6.cnf O = 235
T = 4.71		 O = 319
T = 2.55
(out)(err)		 O = 235
T = 4.71
(out)(err)
s2v120c1600-7.cnf O = 225
T = 4.84		 O = 323
T = 4.26
(out)(err)		 O = 225
T = 4.84
(out)(err)
s2v120c1600-8.cnf O = 237
T = 5.16		 O = 333
T = 3.85
(out)(err)		 O = 237
T = 5.16
(out)(err)
s2v120c1600-9.cnf O = 240
T = 4.98		 O = 345
T = 4.66
(out)(err)		 O = 240
T = 4.98
(out)(err)
s2v140c1200-1.cnf O = 144
T = 5.01		 O = 216
T = 3.36
(out)(err)		 O = 144
T = 5.01
(out)(err)
s2v140c1200-10.cnf O = 140
T = 6.05		 O = 208
T = 2.89
(out)(err)		 O = 140
T = 6.05
(out)(err)
s2v140c1200-2.cnf O = 155
T = 5.08		 O = 217
T = 4.01
(out)(err)		 O = 155
T = 5.08
(out)(err)
s2v140c1200-3.cnf O = 155
T = 5.16		 O = 237
T = 4.58
(out)(err)		 O = 155
T = 5.16
(out)(err)
s2v140c1200-4.cnf O = 148
T = 4.78		 O = 198
T = 5.23
(out)(err)		 O = 148
T = 4.78
(out)(err)
s2v140c1200-5.cnf O = 143
T = 4.26		 O = 214
T = 2.46
(out)(err)		 O = 143
T = 4.26
(out)(err)
s2v140c1200-6.cnf O = 148
T = 5.16		 O = 226
T = 3.66
(out)(err)		 O = 148
T = 5.16
(out)(err)
s2v140c1200-7.cnf O = 148
T = 5.92		 O = 217
T = 4.20
(out)(err)		 O = 148
T = 5.92
(out)(err)
s2v140c1200-8.cnf O = 152
T = 0.41		 O = 226
T = 1.38
(out)(err)		 O = 152
T = 0.41
(out)(err)
s2v140c1200-9.cnf O = 151
T = 4.37		 O = 229
T = 2.08
(out)(err)		 O = 151
T = 4.37
(out)(err)
s2v140c1300-1.cnf O = 162
T = 2.61		 O = 253
T = 4.46
(out)(err)		 O = 162
T = 2.61
(out)(err)
s2v140c1300-10.cnf O = 170
T = 0.50		 O = 268
T = 3.35
(out)(err)		 O = 170
T = 0.50
(out)(err)
s2v140c1300-2.cnf O = 171
T = 3.39		 O = 262
T = 3.35
(out)(err)		 O = 171
T = 3.39
(out)(err)
s2v140c1300-3.cnf O = 168
T = 2.49		 O = 230
T = 4.01
(out)(err)		 O = 168
T = 2.49
(out)(err)
s2v140c1300-4.cnf O = 164
T = 4.74		 O = 237
T = 5.00
(out)(err)		 O = 164
T = 4.74
(out)(err)
s2v140c1300-5.cnf O = 169
T = 5.65		 O = 274
T = 2.76
(out)(err)		 O = 169
T = 5.65
(out)(err)
s2v140c1300-6.cnf O = 168
T = 5.20		 O = 236
T = 2.45
(out)(err)		 O = 168
T = 5.20
(out)(err)
s2v140c1300-7.cnf O = 160
T = 6.27		 O = 257
T = 1.78
(out)(err)		 O = 160
T = 6.27
(out)(err)
s2v140c1300-8.cnf O = 157
T = 5.20		 O = 238
T = 4.13
(out)(err)		 O = 157
T = 5.20
(out)(err)
s2v140c1300-9.cnf O = 162
T = 5.35		 O = 239
T = 11.97
(out)(err)		 O = 162
T = 5.35
(out)(err)
s2v140c1400-1.cnf O = 182
T = 5.11		 O = 276
T = 2.45
(out)(err)		 O = 182
T = 5.11
(out)(err)
s2v140c1400-10.cnf O = 188
T = 6.44		 O = 263
T = 4.06
(out)(err)		 O = 188
T = 6.44
(out)(err)
s2v140c1400-2.cnf O = 178
T = 5.22		 O = 248
T = 2.86
(out)(err)		 O = 178
T = 5.22
(out)(err)
s2v140c1400-3.cnf O = 193
T = 5.24		 O = 284
T = 1.89
(out)(err)		 O = 193
T = 5.24
(out)(err)
s2v140c1400-4.cnf O = 184
T = 5.30		 O = 271
T = 4.01
(out)(err)		 O = 184
T = 5.30
(out)(err)
s2v140c1400-5.cnf O = 187
T = 6.08		 O = 269
T = 2.72
(out)(err)		 O = 187
T = 6.08
(out)(err)
s2v140c1400-6.cnf O = 188
T = 5.75		 O = 269
T = 2.28
(out)(err)		 O = 188
T = 5.75
(out)(err)
s2v140c1400-7.cnf O = 187
T = 5.79		 O = 270
T = 3.52
(out)(err)		 O = 187
T = 5.79
(out)(err)
s2v140c1400-8.cnf O = 181
T = 4.95		 O = 250
T = 3.71
(out)(err)		 O = 181
T = 4.95
(out)(err)
s2v140c1400-9.cnf O = 185
T = 5.61		 O = 301
T = 3.73
(out)(err)		 O = 185
T = 5.61
(out)(err)
s2v140c1500-1.cnf O = 205
T = 5.23		 O = 305
T = 1.35
(out)(err)		 O = 205
T = 5.23
(out)(err)
s2v140c1500-10.cnf O = 202
T = 4.82		 O = 310
T = 3.41
(out)(err)		 O = 202
T = 4.82
(out)(err)
s2v140c1500-2.cnf O = 199
T = 4.71		 O = 291
T = 2.88
(out)(err)		 O = 199
T = 4.71
(out)(err)
s2v140c1500-3.cnf O = 212
T = 5.60		 O = 294
T = 4.93
(out)(err)		 O = 212
T = 5.60
(out)(err)
s2v140c1500-4.cnf O = 197
T = 5.22		 O = 286
T = 3.84
(out)(err)		 O = 197
T = 5.22
(out)(err)
s2v140c1500-5.cnf O = 205
T = 4.45		 O = 313
T = 2.51
(out)(err)		 O = 205
T = 4.45
(out)(err)
s2v140c1500-6.cnf O = 198
T = 5.71		 O = 325
T = 2.32
(out)(err)		 O = 198
T = 5.71
(out)(err)
s2v140c1500-7.cnf O = 202
T = 3.92		 O = 301
T = 2.43
(out)(err)		 O = 202
T = 3.92
(out)(err)
s2v140c1500-8.cnf O = 199
T = 0.71		 O = 313
T = 6.16
(out)(err)		 O = 199
T = 0.71
(out)(err)
s2v140c1500-9.cnf O = 199
T = 0.81		 O = 324
T = 3.64
(out)(err)		 O = 199
T = 0.81
(out)(err)
s2v140c1600-1.cnf O = 221
T = 0.61		 O = 330
T = 3.92
(out)(err)		 O = 221
T = 0.61
(out)(err)
s2v140c1600-10.cnf O = 226
T = 0.79		 O = 322
T = 3.32
(out)(err)		 O = 226
T = 0.79
(out)(err)
s2v140c1600-2.cnf O = 221
T = 0.84		 O = 342
T = 3.46
(out)(err)		 O = 221
T = 0.84
(out)(err)
s2v140c1600-3.cnf O = 226
T = 0.88		 O = 312
T = 3.63
(out)(err)		 O = 226
T = 0.88
(out)(err)
s2v140c1600-4.cnf O = 220
T = 0.99		 O = 319
T = 4.37
(out)(err)		 O = 220
T = 0.99
(out)(err)
s2v140c1600-5.cnf O = 228
T = 0.78		 O = 338
T = 1.81
(out)(err)		 O = 228
T = 0.78
(out)(err)
s2v140c1600-6.cnf O = 220
T = 5.31		 O = 346
T = 2.55
(out)(err)		 O = 220
T = 5.31
(out)(err)
s2v140c1600-7.cnf O = 218
T = 5.12		 O = 325
T = 1.97
(out)(err)		 O = 218
T = 5.12
(out)(err)
s2v140c1600-8.cnf O = 227
T = 4.01		 O = 345
T = 1.52
(out)(err)		 O = 227
T = 4.01
(out)(err)
s2v140c1600-9.cnf O = 228
T = 4.94		 O = 334
T = 3.51
(out)(err)		 O = 228
T = 4.94
(out)(err)
s3v70c1000-1.cnf O = 47
T = 2.84		 O = 86
T = 2.61
(out)(err)		 O = 47
T = 2.84
(out)(err)
s3v70c1000-10.cnf O = 45
T = 3.34		 O = 106
T = 3.64
(out)(err)		 O = 45
T = 3.34
(out)(err)
s3v70c1000-2.cnf O = 43
T = 2.77		 O = 90
T = 2.22
(out)(err)		 O = 43
T = 2.77
(out)(err)
s3v70c1000-3.cnf O = 45
T = 3.49		 O = 92
T = 5.10
(out)(err)		 O = 45
T = 3.49
(out)(err)
s3v70c1000-4.cnf O = 47
T = 2.70		 O = 75
T = 5.34
(out)(err)		 O = 47
T = 2.70
(out)(err)
s3v70c1000-5.cnf O = 42
T = 2.29		 O = 93
T = 2.65
(out)(err)		 O = 42
T = 2.29
(out)(err)
s3v70c1000-6.cnf O = 50
T = 2.80		 O = 87
T = 9.25
(out)(err)		 O = 50
T = 2.80
(out)(err)
s3v70c1000-7.cnf O = 49
T = 3.47		 O = 98
T = 2.57
(out)(err)		 O = 49
T = 3.47
(out)(err)
s3v70c1000-8.cnf O = 48
T = 3.67		 O = 73
T = 4.69
(out)(err)		 O = 48
T = 3.67
(out)(err)
s3v70c1000-9.cnf O = 49
T = 2.28		 O = 89
T = 4.28
(out)(err)		 O = 49
T = 2.28
(out)(err)
s3v70c1100-1.cnf O = 56
T = 3.16		 O = 81
T = 6.08
(out)(err)		 O = 56
T = 3.16
(out)(err)
s3v70c1100-10.cnf O = 58
T = 2.93		 O = 82
T = 4.69
(out)(err)		 O = 58
T = 2.93
(out)(err)
s3v70c1100-2.cnf O = 55
T = 3.33		 O = 99
T = 3.74
(out)(err)		 O = 55
T = 3.33
(out)(err)
s3v70c1100-3.cnf O = 53
T = 3.17		 O = 114
T = 2.71
(out)(err)		 O = 53
T = 3.17
(out)(err)
s3v70c1100-4.cnf O = 52
T = 2.74		 O = 115
T = 3.40
(out)(err)		 O = 52
T = 2.74
(out)(err)
s3v70c1100-5.cnf O = 53
T = 3.55		 O = 85
T = 4.39
(out)(err)		 O = 53
T = 3.55
(out)(err)
s3v70c1100-6.cnf O = 53
T = 4.00		 O = 83
T = 6.60
(out)(err)		 O = 53
T = 4.00
(out)(err)
s3v70c1100-7.cnf O = 53
T = 3.25		 O = 106
T = 3.27
(out)(err)		 O = 53
T = 3.25
(out)(err)
s3v70c1100-8.cnf O = 51
T = 3.55		 O = 102
T = 5.64
(out)(err)		 O = 51
T = 3.55
(out)(err)
s3v70c1100-9.cnf O = 48
T = 2.81		 O = 83
T = 2.24
(out)(err)		 O = 48
T = 2.81
(out)(err)
s3v70c1200-1.cnf O = 66
T = 3.20		 O = 122
T = 5.19
(out)(err)		 O = 66
T = 3.20
(out)(err)
s3v70c1200-10.cnf O = 63
T = 4.32		 O = 111
T = 3.43
(out)(err)		 O = 63
T = 4.32
(out)(err)
s3v70c1200-2.cnf O = 63
T = 3.35		 O = 97
T = 5.20
(out)(err)		 O = 63
T = 3.35
(out)(err)
s3v70c1200-3.cnf O = 65
T = 2.66		 O = 108
T = 3.46
(out)(err)		 O = 65
T = 2.66
(out)(err)
s3v70c1200-4.cnf O = 67
T = 3.57		 O = 111
T = 3.71
(out)(err)		 O = 67
T = 3.57
(out)(err)
s3v70c1200-5.cnf O = 65
T = 3.06		 O = 113
T = 4.53
(out)(err)		 O = 65
T = 3.06
(out)(err)
s3v70c1200-6.cnf O = 66
T = 3.04		 O = 99
T = 4.32
(out)(err)		 O = 66
T = 3.04
(out)(err)
s3v70c1200-7.cnf O = 62
T = 3.77		 O = 116
T = 3.29
(out)(err)		 O = 62
T = 3.77
(out)(err)
s3v70c1200-8.cnf O = 63
T = 2.96		 O = 123
T = 4.63
(out)(err)		 O = 63
T = 2.96
(out)(err)
s3v70c1200-9.cnf O = 61
T = 4.53		 O = 94
T = 3.65
(out)(err)		 O = 61
T = 4.53
(out)(err)
s3v70c800-1.cnf O = 31
T = 2.68		 O = 57
T = 4.93
(out)(err)		 O = 31
T = 2.68
(out)(err)
s3v70c800-10.cnf O = 30
T = 2.54		 O = 57
T = 3.57
(out)(err)		 O = 30
T = 2.54
(out)(err)
s3v70c800-2.cnf O = 34
T = 2.30		 O = 71
T = 3.85
(out)(err)		 O = 34
T = 2.30
(out)(err)
s3v70c800-3.cnf O = 30
T = 2.95		 O = 73
T = 5.00
(out)(err)		 O = 30
T = 2.95
(out)(err)
s3v70c800-4.cnf O = 28
T = 2.32		 O = 65
T = 4.28
(out)(err)		 O = 28
T = 2.32
(out)(err)
s3v70c800-5.cnf O = 31
T = 2.67		 O = 51
T = 7.76
(out)(err)		 O = 31
T = 2.67
(out)(err)
s3v70c800-6.cnf O = 30
T = 2.43		 O = 68
T = 3.10
(out)(err)		 O = 30
T = 2.43
(out)(err)
s3v70c800-7.cnf O = 31
T = 3.20		 O = 50
T = 5.31
(out)(err)		 O = 31
T = 3.20
(out)(err)
s3v70c800-8.cnf O = 34
T = 3.05		 O = 57
T = 6.10
(out)(err)		 O = 34
T = 3.05
(out)(err)
s3v70c800-9.cnf O = 32
T = 2.65		 O = 56
T = 5.66
(out)(err)		 O = 32
T = 2.65
(out)(err)
s3v70c900-1.cnf O = 39
T = 3.08		 O = 66
T = 4.72
(out)(err)		 O = 39
T = 3.08
(out)(err)
s3v70c900-10.cnf O = 39
T = 3.06		 O = 59
T = 4.60
(out)(err)		 O = 39
T = 3.06
(out)(err)
s3v70c900-2.cnf O = 38
T = 2.22		 O = 68
T = 8.54
(out)(err)		 O = 38
T = 2.22
(out)(err)
s3v70c900-3.cnf O = 39
T = 2.57		 O = 92
T = 4.37
(out)(err)		 O = 39
T = 2.57
(out)(err)
s3v70c900-4.cnf O = 39
T = 1.01		 O = 66
T = 5.32
(out)(err)		 O = 39
T = 1.01
(out)(err)
s3v70c900-5.cnf O = 40
T = 0.34		 O = 67
T = 3.58
(out)(err)		 O = 40
T = 0.34
(out)(err)
s3v70c900-6.cnf O = 41
T = 0.25		 O = 66
T = 4.30
(out)(err)		 O = 41
T = 0.25
(out)(err)
s3v70c900-7.cnf O = 40
T = 0.42		 O = 78
T = 5.28
(out)(err)		 O = 40
T = 0.42
(out)(err)
s3v70c900-8.cnf O = 42
T = 0.24		 O = 60
T = 4.54
(out)(err)		 O = 42
T = 0.24
(out)(err)
s3v70c900-9.cnf O = 35
T = 2.19		 O = 74
T = 5.38
(out)(err)		 O = 35
T = 2.19
(out)(err)
s3v80c1000-1.cnf O = 44
T = 2.95		 O = 96
T = 1.96
(out)(err)		 O = 44
T = 2.95
(out)(err)
s3v80c1000-10.cnf O = 39
T = 0.54		 O = 101
T = 2.72
(out)(err)		 O = 39
T = 0.54
(out)(err)
s3v80c1000-2.cnf O = 43
T = 0.48		 O = 73
T = 2.79
(out)(err)		 O = 43
T = 0.48
(out)(err)
s3v80c1000-3.cnf O = 39
T = 3.91		 O = 83
T = 9.26
(out)(err)		 O = 39
T = 3.91
(out)(err)
s3v80c1000-4.cnf O = 45
T = 3.03		 O = 75
T = 6.37
(out)(err)		 O = 45
T = 3.03
(out)(err)
s3v80c1000-5.cnf O = 41
T = 2.69		 O = 84
T = 3.27
(out)(err)		 O = 41
T = 2.69
(out)(err)
s3v80c1000-6.cnf O = 40
T = 3.26		 O = 92
T = 3.73
(out)(err)		 O = 40
T = 3.26
(out)(err)
s3v80c1000-7.cnf O = 40
T = 3.63		 O = 85
T = 3.71
(out)(err)		 O = 40
T = 3.63
(out)(err)
s3v80c1000-8.cnf O = 41
T = 3.01		 O = 87
T = 3.44
(out)(err)		 O = 41
T = 3.01
(out)(err)
s3v80c1000-9.cnf O = 38
T = 3.94		 O = 95
T = 3.01
(out)(err)		 O = 38
T = 3.94
(out)(err)
s3v80c600-1.cnf O = 14
T = 3.03		 O = 32
T = 5.49
(out)(err)		 O = 14
T = 3.03
(out)(err)
s3v80c600-10.cnf O = 15
T = 2.25		 O = 46
T = 3.83
(out)(err)		 O = 15
T = 2.25
(out)(err)
s3v80c600-2.cnf O = 16
T = 2.91		 O = 52
T = 1.43
(out)(err)		 O = 16
T = 2.91
(out)(err)
s3v80c600-3.cnf O = 11
T = 2.86		 O = 37
T = 2.69
(out)(err)		 O = 11
T = 2.86
(out)(err)
s3v80c600-4.cnf O = 13
T = 3.34		 O = 30
T = 4.95
(out)(err)		 O = 13
T = 3.34
(out)(err)
s3v80c600-5.cnf O = 12
T = 0.59		 O = 38
T = 5.65
(out)(err)		 O = 12
T = 0.59
(out)(err)
s3v80c600-6.cnf O = 14
T = 2.76		 O = 45
T = 4.00
(out)(err)		 O = 14
T = 2.76
(out)(err)
s3v80c600-7.cnf O = 12
T = 0.32		 O = 40
T = 2.75
(out)(err)		 O = 12
T = 0.32
(out)(err)
s3v80c600-8.cnf O = 15
T = 2.84		 O = 38
T = 5.94
(out)(err)		 O = 15
T = 2.84
(out)(err)
s3v80c600-9.cnf O = 12
T = 2.14		 O = 39
T = 0.85
(out)(err)		 O = 12
T = 2.14
(out)(err)
s3v80c700-1.cnf O = 19
T = 2.89		 O = 63
T = 1.88
(out)(err)		 O = 19
T = 2.89
(out)(err)
s3v80c700-10.cnf O = 19
T = 2.62		 O = 38
T = 4.81
(out)(err)		 O = 19
T = 2.62
(out)(err)
s3v80c700-2.cnf O = 20
T = 3.27		 O = 31
T = 5.81
(out)(err)		 O = 20
T = 3.27
(out)(err)
s3v80c700-3.cnf O = 18
T = 3.13		 O = 58
T = 4.32
(out)(err)		 O = 18
T = 3.13
(out)(err)
s3v80c700-4.cnf O = 15
T = 2.69		 O = 34
T = 5.99
(out)(err)		 O = 15
T = 2.69
(out)(err)
s3v80c700-5.cnf O = 21
T = 3.28		 O = 54
T = 4.11
(out)(err)		 O = 21
T = 3.28
(out)(err)
s3v80c700-6.cnf O = 18
T = 2.63		 O = 39
T = 6.39
(out)(err)		 O = 18
T = 2.63
(out)(err)
s3v80c700-7.cnf O = 21
T = 3.57		 O = 62
T = 7.09
(out)(err)		 O = 21
T = 3.57
(out)(err)
s3v80c700-8.cnf O = 19
T = 3.41		 O = 54
T = 3.80
(out)(err)		 O = 19
T = 3.41
(out)(err)
s3v80c700-9.cnf O = 18
T = 2.66		 O = 32
T = 7.21
(out)(err)		 O = 18
T = 2.66
(out)(err)
s3v80c800-1.cnf O = 28
T = 3.17		 O = 43
T = 5.53
(out)(err)		 O = 28
T = 3.17
(out)(err)
s3v80c800-10.cnf O = 27
T = 3.08		 O = 55
T = 3.82
(out)(err)		 O = 27
T = 3.08
(out)(err)
s3v80c800-2.cnf O = 32
T = 3.59		 O = 50
T = 5.63
(out)(err)		 O = 32
T = 3.59
(out)(err)
s3v80c800-3.cnf O = 27
T = 2.82		 O = 48
T = 4.53
(out)(err)		 O = 27
T = 2.82
(out)(err)
s3v80c800-4.cnf O = 26
T = 2.43		 O = 55
T = 5.40
(out)(err)		 O = 26
T = 2.43
(out)(err)
s3v80c800-5.cnf O = 27
T = 3.18		 O = 67
T = 2.68
(out)(err)		 O = 27
T = 3.18
(out)(err)
s3v80c800-6.cnf O = 28
T = 3.16		 O = 79
T = 2.88
(out)(err)		 O = 28
T = 3.16
(out)(err)
s3v80c800-7.cnf O = 27
T = 3.53		 O = 77
T = 6.71
(out)(err)		 O = 27
T = 3.53
(out)(err)
s3v80c800-8.cnf O = 25
T = 2.80		 O = 61
T = 2.48
(out)(err)		 O = 25
T = 2.80
(out)(err)
s3v80c800-9.cnf O = 26
T = 2.72		 O = 57
T = 2.04
(out)(err)		 O = 26
T = 2.72
(out)(err)
s3v80c900-1.cnf O = 35
T = 3.58		 O = 81
T = 3.22
(out)(err)		 O = 35
T = 3.58
(out)(err)
s3v80c900-10.cnf O = 35
T = 3.87		 O = 63
T = 3.03
(out)(err)		 O = 35
T = 3.87
(out)(err)
s3v80c900-2.cnf O = 37
T = 2.78		 O = 75
T = 2.61
(out)(err)		 O = 37
T = 2.78
(out)(err)
s3v80c900-3.cnf O = 34
T = 3.47		 O = 87
T = 4.30
(out)(err)		 O = 34
T = 3.47
(out)(err)
s3v80c900-4.cnf O = 35
T = 3.00		 O = 87
T = 3.27
(out)(err)		 O = 35
T = 3.00
(out)(err)
s3v80c900-5.cnf O = 32
T = 3.64		 O = 61
T = 7.69
(out)(err)		 O = 32
T = 3.64
(out)(err)
s3v80c900-6.cnf O = 31
T = 3.13		 O = 58
T = 9.38
(out)(err)		 O = 31
T = 3.13
(out)(err)
s3v80c900-7.cnf O = 34
T = 4.04		 O = 72
T = 3.35
(out)(err)		 O = 34
T = 4.04
(out)(err)
s3v80c900-8.cnf O = 33
T = 2.64		 O = 76
T = 2.34
(out)(err)		 O = 33
T = 2.64
(out)(err)
s3v80c900-9.cnf O = 36
T = 3.63		 O = 82
T = 4.24
(out)(err)		 O = 36
T = 3.63
(out)(err)
min1s2v160c640_0.cnf O = 359
T = 0.60		 O = 411
T = 2.94
(out)(err)		 O = 359
T = 0.60
(out)(err)
min1s2v160c640_1.cnf O = 356
T = 0.82		 O = 402
T = 2.69
(out)(err)		 O = 356
T = 0.82
(out)(err)
min1s2v160c640_10.cnf O = 351
T = 6.36		 O = 400
T = 2.40
(out)(err)		 O = 351
T = 6.36
(out)(err)
min1s2v160c640_11.cnf O = 350
T = 4.30		 O = 392
T = 3.76
(out)(err)		 O = 350
T = 4.30
(out)(err)
min1s2v160c640_12.cnf O = 361
T = 5.80		 O = 404
T = 4.06
(out)(err)		 O = 361
T = 5.80
(out)(err)
min1s2v160c640_13.cnf O = 365
T = 5.17		 O = 401
T = 2.60
(out)(err)		 O = 365
T = 5.17
(out)(err)
min1s2v160c640_14.cnf O = 354
T = 4.41		 O = 408
T = 1.10
(out)(err)		 O = 354
T = 4.41
(out)(err)
min1s2v160c640_15.cnf O = 357
T = 5.42		 O = 406
T = 2.43
(out)(err)		 O = 357
T = 5.42
(out)(err)
min1s2v160c640_2.cnf O = 345
T = 6.41		 O = 395
T = 1.44
(out)(err)		 O = 345
T = 6.41
(out)(err)
min1s2v160c640_3.cnf O = 349
T = 4.96		 O = 411
T = 3.54
(out)(err)		 O = 349
T = 4.96
(out)(err)
min1s2v160c640_4.cnf O = 355
T = 4.24		 O = 397
T = 5.27
(out)(err)		 O = 355
T = 4.24
(out)(err)
min1s2v160c640_5.cnf O = 348
T = 6.01		 O = 396
T = 1.83
(out)(err)		 O = 348
T = 6.01
(out)(err)
min1s2v160c640_6.cnf O = 348
T = 5.70		 O = 381
T = 1.45
(out)(err)		 O = 348
T = 5.70
(out)(err)
min1s2v160c640_7.cnf O = 355
T = 5.47		 O = 391
T = 3.53
(out)(err)		 O = 355
T = 5.47
(out)(err)
min1s2v160c640_8.cnf O = 363
T = 5.48		 O = 399
T = 2.58
(out)(err)		 O = 363
T = 5.48
(out)(err)
min1s2v160c640_9.cnf O = 353
T = 6.88		 O = 396
T = 1.00
(out)(err)		 O = 353
T = 6.88
(out)(err)
min1s2v160c800_0.cnf O = 452
T = 5.70		 O = 506
T = 2.80
(out)(err)		 O = 452
T = 5.70
(out)(err)
min1s2v160c800_1.cnf O = 463
T = 6.23		 O = 513
T = 3.14
(out)(err)		 O = 463
T = 6.23
(out)(err)
min1s2v160c800_10.cnf O = 457
T = 4.98		 O = 515
T = 3.22
(out)(err)		 O = 457
T = 4.98
(out)(err)
min1s2v160c800_11.cnf O = 462
T = 4.90		 O = 504
T = 1.36
(out)(err)		 O = 462
T = 4.90
(out)(err)
min1s2v160c800_12.cnf O = 462
T = 1.76		 O = 520
T = 4.80
(out)(err)		 O = 462
T = 1.76
(out)(err)
min1s2v160c800_13.cnf O = 467
T = 6.15		 O = 505
T = 1.62
(out)(err)		 O = 467
T = 6.15
(out)(err)
min1s2v160c800_14.cnf O = 464
T = 5.98		 O = 520
T = 3.70
(out)(err)		 O = 464
T = 5.98
(out)(err)
min1s2v160c800_15.cnf O = 459
T = 5.89		 O = 520
T = 3.93
(out)(err)		 O = 459
T = 5.89
(out)(err)
min1s2v160c800_2.cnf O = 457
T = 6.64		 O = 515
T = 4.17
(out)(err)		 O = 457
T = 6.64
(out)(err)
min1s2v160c800_3.cnf O = 459
T = 5.92		 O = 501
T = 5.14
(out)(err)		 O = 459
T = 5.92
(out)(err)
min1s2v160c800_4.cnf O = 464
T = 4.65		 O = 509
T = 2.00
(out)(err)		 O = 464
T = 4.65
(out)(err)
min1s2v160c800_5.cnf O = 455
T = 5.79		 O = 489
T = 3.72
(out)(err)		 O = 455
T = 5.79
(out)(err)
min1s2v160c800_6.cnf O = 445
T = 5.50		 O = 485
T = 2.92
(out)(err)		 O = 445
T = 5.50
(out)(err)
min1s2v160c800_7.cnf O = 460
T = 5.13		 O = 507
T = 3.39
(out)(err)		 O = 460
T = 5.13
(out)(err)
min1s2v160c800_8.cnf O = 464
T = 0.46		 O = 516
T = 5.11
(out)(err)		 O = 464
T = 0.46
(out)(err)
min1s2v160c800_9.cnf O = 459
T = 5.55		 O = 522
T = 2.84
(out)(err)		 O = 459
T = 5.55
(out)(err)
min1s2v160c960_0.cnf O = 562
T = 6.12		 O = 628
T = 3.35
(out)(err)		 O = 562
T = 6.12
(out)(err)
min1s2v160c960_1.cnf O = 578
T = 6.28		 O = 651
T = 4.79
(out)(err)		 O = 578
T = 6.28
(out)(err)
min1s2v160c960_10.cnf O = 564
T = 5.88		 O = 641
T = 2.82
(out)(err)		 O = 564
T = 5.88
(out)(err)
min1s2v160c960_11.cnf O = 567
T = 6.63		 O = 610
T = 1.72
(out)(err)		 O = 567
T = 6.63
(out)(err)
min1s2v160c960_12.cnf O = 568
T = 6.55		 O = 628
T = 5.51
(out)(err)		 O = 568
T = 6.55
(out)(err)
min1s2v160c960_13.cnf O = 572
T = 5.49		 O = 610
T = 2.67
(out)(err)		 O = 572
T = 5.49
(out)(err)
min1s2v160c960_14.cnf O = 568
T = 5.81		 O = 619
T = 3.28
(out)(err)		 O = 568
T = 5.81
(out)(err)
min1s2v160c960_15.cnf O = 558
T = 6.07		 O = 620
T = 3.64
(out)(err)		 O = 558
T = 6.07
(out)(err)
min1s2v160c960_2.cnf O = 561
T = 6.10		 O = 612
T = 2.14
(out)(err)		 O = 561
T = 6.10
(out)(err)
min1s2v160c960_3.cnf O = 563
T = 6.25		 O = 624
T = 1.85
(out)(err)		 O = 563
T = 6.25
(out)(err)
min1s2v160c960_4.cnf O = 574
T = 4.87		 O = 618
T = 3.13
(out)(err)		 O = 574
T = 4.87
(out)(err)
min1s2v160c960_5.cnf O = 571
T = 5.21		 O = 634
T = 3.97
(out)(err)		 O = 571
T = 5.21
(out)(err)
min1s2v160c960_6.cnf O = 549
T = 5.39		 O = 606
T = 3.51
(out)(err)		 O = 549
T = 5.39
(out)(err)
min1s2v160c960_7.cnf O = 565
T = 6.46		 O = 629
T = 2.37
(out)(err)		 O = 565
T = 6.46
(out)(err)
min1s2v160c960_8.cnf O = 566
T = 7.75		 O = 630
T = 3.25
(out)(err)		 O = 566
T = 7.75
(out)(err)
min1s2v160c960_9.cnf O = 555
T = 7.71		 O = 603
T = 3.77
(out)(err)		 O = 555
T = 7.71
(out)(err)
min1s2v200c1000_0.cnf O = 580
T = 6.61		 O = 662
T = 3.73
(out)(err)		 O = 580
T = 6.61
(out)(err)
min1s2v200c1000_1.cnf O = 570
T = 6.16		 O = 641
T = 3.53
(out)(err)		 O = 570
T = 6.16
(out)(err)
min1s2v200c1000_10.cnf O = 574
T = 8.04		 O = 649
T = 5.57
(out)(err)		 O = 574
T = 8.04
(out)(err)
min1s2v200c1000_11.cnf O = 570
T = 7.55		 O = 628
T = 5.53
(out)(err)		 O = 570
T = 7.55
(out)(err)
min1s2v200c1000_12.cnf O = 569
T = 7.33		 O = 626
T = 3.22
(out)(err)		 O = 569
T = 7.33
(out)(err)
min1s2v200c1000_13.cnf O = 573
T = 7.00		 O = 625
T = 1.27
(out)(err)		 O = 573
T = 7.00
(out)(err)
min1s2v200c1000_14.cnf O = 571
T = 8.70		 O = 650
T = 2.21
(out)(err)		 O = 571
T = 8.70
(out)(err)
min1s2v200c1000_15.cnf O = 573
T = 6.37		 O = 654
T = 3.57
(out)(err)		 O = 573
T = 6.37
(out)(err)
min1s2v200c1000_2.cnf O = 575
T = 3.65		 O = 647
T = 1.60
(out)(err)		 O = 575
T = 3.65
(out)(err)
min1s2v200c1000_3.cnf O = 574
T = 0.83		 O = 632
T = 4.06
(out)(err)		 O = 574
T = 0.83
(out)(err)
min1s2v200c1000_4.cnf O = 570
T = 8.49		 O = 637
T = 5.97
(out)(err)		 O = 570
T = 8.49
(out)(err)
min1s2v200c1000_5.cnf O = 571
T = 7.04		 O = 665
T = 2.59
(out)(err)		 O = 571
T = 7.04
(out)(err)
min1s2v200c1000_6.cnf O = 570
T = 4.53		 O = 635
T = 2.94
(out)(err)		 O = 570
T = 4.53
(out)(err)
min1s2v200c1000_7.cnf O = 561
T = 7.68		 O = 618
T = 3.38
(out)(err)		 O = 561
T = 7.68
(out)(err)
min1s2v200c1000_8.cnf O = 559
T = 7.56		 O = 615
T = 1.90
(out)(err)		 O = 559
T = 7.56
(out)(err)
min1s2v200c1000_9.cnf O = 563
T = 6.88		 O = 636
T = 2.02
(out)(err)		 O = 563
T = 6.88
(out)(err)
min1s2v200c1200_0.cnf O = 708
T = 7.23		 O = 789
T = 1.46
(out)(err)		 O = 708
T = 7.23
(out)(err)
min1s2v200c1200_1.cnf O = 699
T = 6.79		 O = 793
T = 3.17
(out)(err)		 O = 699
T = 6.79
(out)(err)
min1s2v200c1200_10.cnf O = 708
T = 7.86		 O = 800
T = 0.71
(out)(err)		 O = 708
T = 7.86
(out)(err)
min1s2v200c1200_11.cnf O = 699
T = 7.84		 O = 784
T = 5.42
(out)(err)		 O = 699
T = 7.84
(out)(err)
min1s2v200c1200_12.cnf O = 704
T = 5.37		 O = 766
T = 3.35
(out)(err)		 O = 704
T = 5.37
(out)(err)
min1s2v200c1200_13.cnf O = 710
T = 3.67		 O = 797
T = 2.11
(out)(err)		 O = 710
T = 3.67
(out)(err)
min1s2v200c1200_14.cnf O = 707
T = 3.48		 O = 780
T = 1.70
(out)(err)		 O = 707
T = 3.48
(out)(err)
min1s2v200c1200_15.cnf O = 709
T = 4.86		 O = 770
T = 2.48
(out)(err)		 O = 709
T = 4.86
(out)(err)
min1s2v200c1200_2.cnf O = 706
T = 7.01		 O = 770
T = 3.27
(out)(err)		 O = 706
T = 7.01
(out)(err)
min1s2v200c1200_3.cnf O = 703
T = 8.03		 O = 768
T = 1.00
(out)(err)		 O = 703
T = 8.03
(out)(err)
min1s2v200c1200_4.cnf O = 710
T = 6.95		 O = 798
T = 2.21
(out)(err)		 O = 710
T = 6.95
(out)(err)
min1s2v200c1200_5.cnf O = 700
T = 7.45		 O = 779
T = 1.80
(out)(err)		 O = 700
T = 7.45
(out)(err)
min1s2v200c1200_6.cnf O = 709
T = 7.54		 O = 795
T = 1.81
(out)(err)		 O = 709
T = 7.54
(out)(err)
min1s2v200c1200_7.cnf O = 704
T = 5.31		 O = 779
T = 3.88
(out)(err)		 O = 704
T = 5.31
(out)(err)
min1s2v200c1200_8.cnf O = 685
T = 7.27		 O = 755
T = 2.93
(out)(err)		 O = 685
T = 7.27
(out)(err)
min1s2v200c1200_9.cnf O = 696
T = 6.86		 O = 763
T = 3.12
(out)(err)		 O = 696
T = 6.86
(out)(err)
min1s2v200c800_0.cnf O = 446
T = 6.22		 O = 510
T = 2.75
(out)(err)		 O = 446
T = 6.22
(out)(err)
min1s2v200c800_1.cnf O = 444
T = 7.68		 O = 511
T = 4.53
(out)(err)		 O = 444
T = 7.68
(out)(err)
min1s2v200c800_10.cnf O = 438
T = 6.81		 O = 506
T = 4.34
(out)(err)		 O = 438
T = 6.81
(out)(err)
min1s2v200c800_11.cnf O = 437
T = 6.90		 O = 497
T = 0.61
(out)(err)		 O = 437
T = 6.90
(out)(err)
min1s2v200c800_12.cnf O = 436
T = 7.83		 O = 494
T = 3.77
(out)(err)		 O = 436
T = 7.83
(out)(err)
min1s2v200c800_13.cnf O = 439
T = 6.80		 O = 491
T = 1.89
(out)(err)		 O = 439
T = 6.80
(out)(err)
min1s2v200c800_14.cnf O = 436
T = 7.93		 O = 482
T = 3.01
(out)(err)		 O = 436
T = 7.93
(out)(err)
min1s2v200c800_15.cnf O = 438
T = 6.67		 O = 483
T = 4.52
(out)(err)		 O = 438
T = 6.67
(out)(err)
min1s2v200c800_2.cnf O = 438
T = 6.76		 O = 499
T = 3.41
(out)(err)		 O = 438
T = 6.76
(out)(err)
min1s2v200c800_3.cnf O = 439
T = 6.27		 O = 488
T = 3.47
(out)(err)		 O = 439
T = 6.27
(out)(err)
min1s2v200c800_4.cnf O = 437
T = 7.46		 O = 493
T = 1.30
(out)(err)		 O = 437
T = 7.46
(out)(err)
min1s2v200c800_5.cnf O = 435
T = 6.79		 O = 489
T = 3.69
(out)(err)		 O = 435
T = 6.79
(out)(err)
min1s2v200c800_6.cnf O = 445
T = 4.01		 O = 496
T = 3.12
(out)(err)		 O = 445
T = 4.01
(out)(err)
min1s2v200c800_7.cnf O = 440
T = 5.76		 O = 503
T = 2.10
(out)(err)		 O = 440
T = 5.76
(out)(err)
min1s2v200c800_8.cnf O = 436
T = 6.81		 O = 505
T = 3.14
(out)(err)		 O = 436
T = 6.81
(out)(err)
min1s2v200c800_9.cnf O = 438
T = 7.14		 O = 501
T = 4.39
(out)(err)		 O = 438
T = 7.14
(out)(err)