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 ISAC+-2016-co
s2v120c1200-1.cnf S = OPT
O = 161
T = 9.33		 S = OPT
O = 161
T = 9.33
s2v120c1200-2.cnf S = OPT
O = 159
T = 9.12		 S = OPT
O = 159
T = 9.12
s2v120c1200-3.cnf S = OPT
O = 160
T = 5.37		 S = OPT
O = 160
T = 5.37
s2v120c1300-1.cnf S = OPT
O = 180
T = 15.83		 S = OPT
O = 180
T = 15.83
s2v120c1300-2.cnf S = OPT
O = 172
T = 7.68		 S = OPT
O = 172
T = 7.68
s2v120c1300-3.cnf S = OPT
O = 173
T = 7.87		 S = OPT
O = 173
T = 7.87
s2v120c1400-1.cnf S = OPT
O = 197
T = 14.70		 S = OPT
O = 197
T = 14.70
s2v120c1400-2.cnf S = OPT
O = 191
T = 10.46		 S = OPT
O = 191
T = 10.46
s2v120c1400-3.cnf S = OPT
O = 189
T = 10.37		 S = OPT
O = 189
T = 10.37
s2v120c1500-1.cnf S = OPT
O = 211
T = 10.72		 S = OPT
O = 211
T = 10.72
s2v120c1500-2.cnf S = OPT
O = 213
T = 24.88		 S = OPT
O = 213
T = 24.88
s2v120c1500-3.cnf S = OPT
O = 207
T = 8.76		 S = OPT
O = 207
T = 8.76
s2v120c1600-1.cnf S = OPT
O = 233
T = 23.15		 S = OPT
O = 233
T = 23.15
s2v120c1600-2.cnf S = OPT
O = 239
T = 97.50		 S = OPT
O = 239
T = 97.50
s2v120c1600-3.cnf S = OPT
O = 233
T = 30.95		 S = OPT
O = 233
T = 30.95
s2v120c1700-1.cnf S = OPT
O = 257
T = 46.76		 S = OPT
O = 257
T = 46.76
s2v120c1700-2.cnf S = OPT
O = 248
T = 72.78		 S = OPT
O = 248
T = 72.78
s2v120c1700-3.cnf S = OPT
O = 239
T = 7.29		 S = OPT
O = 239
T = 7.29
s2v120c1800-1.cnf S = OPT
O = 291
T = 436.74		 S = OPT
O = 291
T = 436.74
s2v120c1800-2.cnf S = OPT
O = 262
T = 17.85		 S = OPT
O = 262
T = 17.85
s2v120c1800-3.cnf S = OPT
O = 279
T = 58.31		 S = OPT
O = 279
T = 58.31
s2v120c1900-1.cnf S = OPT
O = 293
T = 67.00		 S = OPT
O = 293
T = 67.00
s2v120c1900-2.cnf S = OPT
O = 296
T = 151.91		 S = OPT
O = 296
T = 151.91
s2v120c1900-3.cnf S = OPT
O = 294
T = 101.97		 S = OPT
O = 294
T = 101.97
s2v120c2000-1.cnf S = OPT
O = 307
T = 25.09		 S = OPT
O = 307
T = 25.09
s2v120c2000-2.cnf S = OPT
O = 321
T = 664.99		 S = OPT
O = 321
T = 664.99
s2v120c2000-3.cnf S = OPT
O = 307
T = 74.04		 S = OPT
O = 307
T = 74.04
s2v120c2100-1.cnf S = OPT
O = 336
T = 49.71		 S = OPT
O = 336
T = 49.71
s2v120c2100-2.cnf S = OPT
O = 336
T = 504.90		 S = OPT
O = 336
T = 504.90
s2v120c2100-3.cnf S = OPT
O = 332
T = 212.59		 S = OPT
O = 332
T = 212.59
s2v120c2200-1.cnf S = OPT
O = 358
T = 436.18		 S = OPT
O = 358
T = 436.18
s2v120c2200-2.cnf S = OPT
O = 371
T = 1518.74		 S = OPT
O = 371
T = 1518.74
s2v120c2200-3.cnf S = OPT
O = 359
T = 337.10		 S = OPT
O = 359
T = 337.10
s2v120c2300-1.cnf S = OPT
O = 380
T = 385.20		 S = OPT
O = 380
T = 385.20
s2v120c2300-2.cnf S = OPT
O = 383
T = 595.09		 S = OPT
O = 383
T = 595.09
s2v120c2300-3.cnf S = OPT
O = 365
T = 77.32		 S = OPT
O = 365
T = 77.32
s2v120c2400-1.cnf S = OPT
O = 389
T = 156.09		 S = OPT
O = 389
T = 156.09
s2v120c2400-2.cnf S = OPT
O = 402
T = 953.71		 S = OPT
O = 402
T = 953.71
s2v120c2400-3.cnf S = OPT
O = 380
T = 42.30		 S = OPT
O = 380
T = 42.30
s2v120c2500-1.cnf S = OPT
O = 418
T = 256.39		 S = OPT
O = 418
T = 256.39
s2v120c2500-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = 435
T = TO
s2v120c2500-3.cnf S = OPT
O = 425
T = 885.54		 S = OPT
O = 425
T = 885.54
s2v120c2600-1.cnf S = OPT
O = 439
T = 874.54		 S = OPT
O = 439
T = 874.54
s2v120c2600-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v120c2600-3.cnf S = OPT
O = 440
T = 435.70		 S = OPT
O = 440
T = 435.70
s2v140c1200-1.cnf S = OPT
O = 144
T = 9.68		 S = OPT
O = 144
T = 9.68
s2v140c1200-2.cnf S = OPT
O = 155
T = 126.79		 S = OPT
O = 155
T = 126.79
s2v140c1200-3.cnf S = OPT
O = 155
T = 16.87		 S = OPT
O = 155
T = 16.87
s2v140c1300-1.cnf S = OPT
O = 162
T = 21.74		 S = OPT
O = 162
T = 21.74
s2v140c1300-2.cnf S = OPT
O = 171
T = 82.44		 S = OPT
O = 171
T = 82.44
s2v140c1300-3.cnf S = OPT
O = 168
T = 40.75		 S = OPT
O = 168
T = 40.75
s2v140c1400-1.cnf S = OPT
O = 182
T = 37.06		 S = OPT
O = 182
T = 37.06
s2v140c1400-2.cnf S = OPT
O = 178
T = 20.17		 S = OPT
O = 178
T = 20.17
s2v140c1400-3.cnf S = OPT
O = 193
T = 93.38		 S = OPT
O = 193
T = 93.38
s2v140c1500-1.cnf S = OPT
O = 205
T = 117.59		 S = OPT
O = 205
T = 117.59
s2v140c1500-2.cnf S = OPT
O = 199
T = 124.00		 S = OPT
O = 199
T = 124.00
s2v140c1500-3.cnf S = OPT
O = 212
T = 469.43		 S = OPT
O = 212
T = 469.43
s2v140c1600-1.cnf S = OPT
O = 221
T = 77.09		 S = OPT
O = 221
T = 77.09
s2v140c1600-2.cnf S = OPT
O = 221
T = 137.44		 S = OPT
O = 221
T = 137.44
s2v140c1600-3.cnf S = OPT
O = 226
T = 191.35		 S = OPT
O = 226
T = 191.35
s2v140c1700-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v140c1700-2.cnf S = OPT
O = 242
T = 145.44		 S = OPT
O = 242
T = 145.44
s2v140c1700-3.cnf S = OPT
O = 236
T = 67.24		 S = OPT
O = 236
T = 67.24
s2v140c1800-1.cnf S = OPT
O = 254
T = 249.36		 S = OPT
O = 254
T = 249.36
s2v140c1800-2.cnf S = OPT
O = 257
T = 149.24		 S = OPT
O = 257
T = 149.24
s2v140c1800-3.cnf S = OPT
O = 255
T = 61.72		 S = OPT
O = 255
T = 61.72
s2v140c1900-1.cnf S = OPT
O = 283
T = 1577.81		 S = OPT
O = 283
T = 1577.81
s2v140c1900-2.cnf S = OPT
O = 273
T = 54.88		 S = OPT
O = 273
T = 54.88
s2v140c1900-3.cnf S = OPT
O = 278
T = 258.05		 S = OPT
O = 278
T = 258.05
s2v140c2000-1.cnf S = OPT
O = 298
T = 555.77		 S = OPT
O = 298
T = 555.77
s2v140c2000-2.cnf S = OPT
O = 308
T = 1623.58		 S = OPT
O = 308
T = 1623.58
s2v140c2000-3.cnf S = OPT
O = 296
T = 209.18		 S = OPT
O = 296
T = 209.18
s2v140c2100-1.cnf S = OPT
O = 293
T = 31.49		 S = OPT
O = 293
T = 31.49
s2v140c2100-2.cnf S = OPT
O = 310
T = 170.31		 S = OPT
O = 310
T = 170.31
s2v140c2100-3.cnf S = OPT
O = 319
T = 437.45		 S = OPT
O = 319
T = 437.45
s2v140c2200-1.cnf S = OPT
O = 336
T = 1031.49		 S = OPT
O = 336
T = 1031.49
s2v140c2200-2.cnf S = OPT
O = 332
T = 872.20		 S = OPT
O = 332
T = 872.20
s2v140c2200-3.cnf S = OPT
O = 329
T = 389.00		 S = OPT
O = 329
T = 389.00
s2v140c2300-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v140c2300-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v140c2300-3.cnf S = OPT
O = 352
T = 824.53		 S = OPT
O = 352
T = 824.53
s2v140c2400-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v140c2400-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v140c2400-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v140c2500-1.cnf S = OPT
O = 393
T = 805.32		 S = OPT
O = 393
T = 805.32
s2v140c2500-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v140c2500-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v140c2600-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v140c2600-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v140c2600-3.cnf S = OPT
O = 406
T = 1073.29		 S = OPT
O = 406
T = 1073.29
s2v160c1200-1.cnf S = OPT
O = 142
T = 38.11		 S = OPT
O = 142
T = 38.11
s2v160c1200-2.cnf S = OPT
O = 133
T = 10.02		 S = OPT
O = 133
T = 10.02
s2v160c1200-3.cnf S = OPT
O = 143
T = 94.47		 S = OPT
O = 143
T = 94.47
s2v160c1300-1.cnf S = OPT
O = 167
T = 258.84		 S = OPT
O = 167
T = 258.84
s2v160c1300-2.cnf S = OPT
O = 139
T = 6.30		 S = OPT
O = 139
T = 6.30
s2v160c1300-3.cnf S = OPT
O = 157
T = 66.41		 S = OPT
O = 157
T = 66.41
s2v160c1400-1.cnf S = OPT
O = 166
T = 37.50		 S = OPT
O = 166
T = 37.50
s2v160c1400-2.cnf S = OPT
O = 164
T = 35.70		 S = OPT
O = 164
T = 35.70
s2v160c1400-3.cnf S = OPT
O = 167
T = 23.27		 S = OPT
O = 167
T = 23.27
s2v160c1500-1.cnf S = OPT
O = 183
T = 14.56		 S = OPT
O = 183
T = 14.56
s2v160c1500-2.cnf S = OPT
O = 200
T = 753.07		 S = OPT
O = 200
T = 753.07
s2v160c1500-3.cnf S = OPT
O = 184
T = 50.41		 S = OPT
O = 184
T = 50.41
s2v160c1600-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c1600-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c1600-3.cnf S = OPT
O = 213
T = 505.02		 S = OPT
O = 213
T = 505.02
s2v160c1700-1.cnf S = OPT
O = 226
T = 561.34		 S = OPT
O = 226
T = 561.34
s2v160c1700-2.cnf S = OPT
O = 230
T = 416.48		 S = OPT
O = 230
T = 416.48
s2v160c1700-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c1800-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c1800-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c1800-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c1900-1.cnf S = OPT
O = 261
T = 1179.68		 S = OPT
O = 261
T = 1179.68
s2v160c1900-2.cnf S = OPT
O = 262
T = 1088.63		 S = OPT
O = 262
T = 1088.63
s2v160c1900-3.cnf S = OPT
O = 264
T = 683.28		 S = OPT
O = 264
T = 683.28
s2v160c2000-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2000-2.cnf S = OPT
O = 272
T = 87.04		 S = OPT
O = 272
T = 87.04
s2v160c2000-3.cnf S = OPT
O = 282
T = 776.22		 S = OPT
O = 282
T = 776.22
s2v160c2100-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2100-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2100-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2200-1.cnf S = OPT
O = 310
T = 448.18		 S = OPT
O = 310
T = 448.18
s2v160c2200-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2200-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2300-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2300-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2300-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2400-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2400-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2400-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2500-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2500-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2500-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2600-1.cnf S = OPT
O = 392
T = 1391.60		 S = OPT
O = 392
T = 1391.60
s2v160c2600-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v160c2600-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c1200-1.cnf S = OPT
O = 134
T = 180.21		 S = OPT
O = 134
T = 180.21
s2v180c1200-2.cnf S = OPT
O = 130
T = 64.56		 S = OPT
O = 130
T = 64.56
s2v180c1200-3.cnf S = OPT
O = 131
T = 101.58		 S = OPT
O = 131
T = 101.58
s2v180c1200-4.cnf S = OPT
O = 128
T = 146.50		 S = OPT
O = 128
T = 146.50
s2v180c1300-1.cnf S = OPT
O = 153
T = 479.48		 S = OPT
O = 153
T = 479.48
s2v180c1300-2.cnf S = OPT
O = 138
T = 43.66		 S = OPT
O = 138
T = 43.66
s2v180c1300-3.cnf S = OPT
O = 150
T = 135.66		 S = OPT
O = 150
T = 135.66
s2v180c1300-4.cnf S = OPT
O = 149
T = 209.16		 S = OPT
O = 149
T = 209.16
s2v180c1400-1.cnf S = OPT
O = 165
T = 355.77		 S = OPT
O = 165
T = 355.77
s2v180c1400-2.cnf S = OPT
O = 165
T = 424.18		 S = OPT
O = 165
T = 424.18
s2v180c1400-3.cnf S = OPT
O = 156
T = 113.20		 S = OPT
O = 156
T = 113.20
s2v180c1400-4.cnf S = OPT
O = 160
T = 150.81		 S = OPT
O = 160
T = 150.81
s2v180c1500-1.cnf S = OPT
O = 184
T = 1401.29		 S = OPT
O = 184
T = 1401.29
s2v180c1500-2.cnf S = OPT
O = 180
T = 1203.57		 S = OPT
O = 180
T = 1203.57
s2v180c1500-3.cnf S = OPT
O = 179
T = 238.02		 S = OPT
O = 179
T = 238.02
s2v180c1500-4.cnf S = OPT
O = 181
T = 320.67		 S = OPT
O = 181
T = 320.67
s2v180c1600-1.cnf S = OPT
O = 200
T = 1700.55		 S = OPT
O = 200
T = 1700.55
s2v180c1600-2.cnf S = OPT
O = 204
T = 1382.70		 S = OPT
O = 204
T = 1382.70
s2v180c1600-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c1600-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c1700-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c1700-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c1700-3.cnf S = OPT
O = 209
T = 819.76		 S = OPT
O = 209
T = 819.76
s2v180c1700-4.cnf S = OPT
O = 206
T = 207.78		 S = OPT
O = 206
T = 207.78
s2v180c1800-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c1800-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c1800-3.cnf S = OPT
O = 232
T = 1015.88		 S = OPT
O = 232
T = 1015.88
s2v180c1800-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c1900-1.cnf S = OPT
O = 245
T = 635.15		 S = OPT
O = 245
T = 635.15
s2v180c1900-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c1900-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c1900-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c2000-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c2000-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c2000-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c2000-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c2100-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c2100-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c2100-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c2100-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c2200-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c2200-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c2200-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v180c2200-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1200-1.cnf S = OPT
O = 118
T = 112.80		 S = OPT
O = 118
T = 112.80
s2v200c1200-2.cnf S = OPT
O = 127
T = 278.49		 S = OPT
O = 127
T = 278.49
s2v200c1200-3.cnf S = OPT
O = 125
T = 428.77		 S = OPT
O = 125
T = 428.77
s2v200c1200-4.cnf S = OPT
O = 115
T = 30.81		 S = OPT
O = 115
T = 30.81
s2v200c1200-5.cnf S = OPT
O = 117
T = 120.39		 S = OPT
O = 117
T = 120.39
s2v200c1200-6.cnf S = OPT
O = 127
T = 219.29		 S = OPT
O = 127
T = 219.29
s2v200c1200-7.cnf S = OPT
O = 112
T = 16.55		 S = OPT
O = 112
T = 16.55
s2v200c1300-1.cnf S = OPT
O = 144
T = 538.03		 S = OPT
O = 144
T = 538.03
s2v200c1300-2.cnf S = OPT
O = 143
T = 642.77		 S = OPT
O = 143
T = 642.77
s2v200c1300-3.cnf S = OPT
O = 121
T = 51.09		 S = OPT
O = 121
T = 51.09
s2v200c1300-4.cnf S = OPT
O = 139
T = 300.03		 S = OPT
O = 139
T = 300.03
s2v200c1300-5.cnf S = OPT
O = 142
T = 481.96		 S = OPT
O = 142
T = 481.96
s2v200c1300-6.cnf S = OPT
O = 134
T = 433.69		 S = OPT
O = 134
T = 433.69
s2v200c1300-7.cnf S = OPT
O = 128
T = 25.67		 S = OPT
O = 128
T = 25.67
s2v200c1400-1.cnf S = OPT
O = 156
T = 587.66		 S = OPT
O = 156
T = 587.66
s2v200c1400-2.cnf S = OPT
O = 147
T = 104.31		 S = OPT
O = 147
T = 104.31
s2v200c1400-3.cnf S = OPT
O = 150
T = 140.75		 S = OPT
O = 150
T = 140.75
s2v200c1400-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = 164
T = TO
s2v200c1400-5.cnf S = OPT
O = 153
T = 269.77		 S = OPT
O = 153
T = 269.77
s2v200c1400-6.cnf S = OPT
O = 145
T = 104.41		 S = OPT
O = 145
T = 104.41
s2v200c1400-7.cnf S = OPT
O = 142
T = 110.27		 S = OPT
O = 142
T = 110.27
s2v200c1500-1.cnf S = OPT
O = 165
T = 141.83		 S = OPT
O = 165
T = 141.83
s2v200c1500-2.cnf S = OPT
O = 165
T = 345.75		 S = OPT
O = 165
T = 345.75
s2v200c1500-3.cnf S = OPT
O = 165
T = 569.29		 S = OPT
O = 165
T = 569.29
s2v200c1500-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1500-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1500-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1500-7.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1600-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1600-2.cnf S = OPT
O = 178
T = 209.56		 S = OPT
O = 178
T = 209.56
s2v200c1600-3.cnf S = OPT
O = 186
T = 1697.76		 S = OPT
O = 186
T = 1697.76
s2v200c1600-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1600-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1600-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = 179
T = TO
s2v200c1600-7.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1700-1.cnf S = OPT
O = 193
T = 101.28		 S = OPT
O = 193
T = 101.28
s2v200c1700-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1700-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1700-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1700-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1700-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1700-7.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1800-1.cnf S = OPT
O = 206
T = 337.97		 S = OPT
O = 206
T = 337.97
s2v200c1800-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = 223
T = TO
s2v200c1800-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1800-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1800-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1800-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s2v200c1800-7.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1000-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1000-10.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1000-2.cnf S = OPT
O = 27
T = 1734.00		 S = OPT
O = 27
T = 1734.00
s3v110c1000-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1000-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1000-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1000-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1000-7.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1000-8.cnf S = OPT
O = 26
T = 1375.49		 S = OPT
O = 26
T = 1375.49
s3v110c1000-9.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1100-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1100-10.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1100-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1100-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1100-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1100-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1100-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1100-7.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1100-8.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c1100-9.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v110c700-1.cnf S = OPT
O = 11
T = 58.36		 S = OPT
O = 11
T = 58.36
s3v110c700-10.cnf S = OPT
O = 9
T = 14.39		 S = OPT
O = 9
T = 14.39
s3v110c700-2.cnf S = OPT
O = 12
T = 106.80		 S = OPT
O = 12
T = 106.80
s3v110c700-3.cnf S = OPT
O = 10
T = 29.68		 S = OPT
O = 10
T = 29.68
s3v110c700-4.cnf S = OPT
O = 11
T = 42.61		 S = OPT
O = 11
T = 42.61
s3v110c700-5.cnf S = OPT
O = 10
T = 30.78		 S = OPT
O = 10
T = 30.78
s3v110c700-6.cnf S = OPT
O = 11
T = 53.75		 S = OPT
O = 11
T = 53.75
s3v110c700-7.cnf S = OPT
O = 9
T = 20.36		 S = OPT
O = 9
T = 20.36
s3v110c700-8.cnf S = OPT
O = 11
T = 58.65		 S = OPT
O = 11
T = 58.65
s3v110c700-9.cnf S = OPT
O = 10
T = 44.72		 S = OPT
O = 10
T = 44.72
s3v110c800-1.cnf S = OPT
O = 17
T = 307.74		 S = OPT
O = 17
T = 307.74
s3v110c800-10.cnf S = OPT
O = 14
T = 73.91		 S = OPT
O = 14
T = 73.91
s3v110c800-2.cnf S = OPT
O = 17
T = 398.29		 S = OPT
O = 17
T = 398.29
s3v110c800-3.cnf S = OPT
O = 15
T = 163.30		 S = OPT
O = 15
T = 163.30
s3v110c800-4.cnf S = OPT
O = 18
T = 250.23		 S = OPT
O = 18
T = 250.23
s3v110c800-5.cnf S = OPT
O = 17
T = 235.72		 S = OPT
O = 17
T = 235.72
s3v110c800-6.cnf S = OPT
O = 18
T = 414.90		 S = OPT
O = 18
T = 414.90
s3v110c800-7.cnf S = OPT
O = 16
T = 202.42		 S = OPT
O = 16
T = 202.42
s3v110c800-8.cnf S = OPT
O = 17
T = 468.71		 S = OPT
O = 17
T = 468.71
s3v110c800-9.cnf S = OPT
O = 16
T = 138.12		 S = OPT
O = 16
T = 138.12
s3v110c900-1.cnf S = OPT
O = 22
T = 748.65		 S = OPT
O = 22
T = 748.65
s3v110c900-10.cnf S = OPT
O = 21
T = 583.62		 S = OPT
O = 21
T = 583.62
s3v110c900-2.cnf S = OPT
O = 22
T = 985.46		 S = OPT
O = 22
T = 985.46
s3v110c900-3.cnf S = OPT
O = 17
T = 78.08		 S = OPT
O = 17
T = 78.08
s3v110c900-4.cnf S = OPT
O = 21
T = 472.09		 S = OPT
O = 21
T = 472.09
s3v110c900-5.cnf S = OPT
O = 22
T = 516.58		 S = OPT
O = 22
T = 516.58
s3v110c900-6.cnf S = OPT
O = 23
T = 728.42		 S = OPT
O = 23
T = 728.42
s3v110c900-7.cnf S = OPT
O = 21
T = 807.26		 S = OPT
O = 21
T = 807.26
s3v110c900-8.cnf S = OPT
O = 22
T = 598.88		 S = OPT
O = 22
T = 598.88
s3v110c900-9.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v70c1000-1.cnf S = OPT
O = 47
T = 123.07		 S = OPT
O = 47
T = 123.07
s3v70c1000-2.cnf S = OPT
O = 43
T = 57.90		 S = OPT
O = 43
T = 57.90
s3v70c1000-3.cnf S = OPT
O = 45
T = 79.72		 S = OPT
O = 45
T = 79.72
s3v70c1000-4.cnf S = OPT
O = 47
T = 121.79		 S = OPT
O = 47
T = 121.79
s3v70c1000-5.cnf S = OPT
O = 42
T = 48.78		 S = OPT
O = 42
T = 48.78
s3v70c1100-1.cnf S = OPT
O = 56
T = 323.97		 S = OPT
O = 56
T = 323.97
s3v70c1100-2.cnf S = OPT
O = 55
T = 224.27		 S = OPT
O = 55
T = 224.27
s3v70c1100-3.cnf S = OPT
O = 53
T = 134.60		 S = OPT
O = 53
T = 134.60
s3v70c1100-4.cnf S = OPT
O = 52
T = 166.79		 S = OPT
O = 52
T = 166.79
s3v70c1100-5.cnf S = OPT
O = 53
T = 181.50		 S = OPT
O = 53
T = 181.50
s3v70c1200-1.cnf S = OPT
O = 66
T = 733.47		 S = OPT
O = 66
T = 733.47
s3v70c1200-2.cnf S = OPT
O = 63
T = 317.93		 S = OPT
O = 63
T = 317.93
s3v70c1200-3.cnf S = OPT
O = 65
T = 584.12		 S = OPT
O = 65
T = 584.12
s3v70c1200-4.cnf S = OPT
O = 67
T = 987.73		 S = OPT
O = 67
T = 987.73
s3v70c1200-5.cnf S = OPT
O = 65
T = 526.44		 S = OPT
O = 65
T = 526.44
s3v70c1300-1.cnf S = OPT
O = 75
T = 1124.09		 S = OPT
O = 75
T = 1124.09
s3v70c1300-2.cnf S = OPT
O = 74
T = 918.86		 S = OPT
O = 74
T = 918.86
s3v70c1300-3.cnf S = OPT
O = 70
T = 704.12		 S = OPT
O = 70
T = 704.12
s3v70c1300-4.cnf S = OPT
O = 68
T = 318.72		 S = OPT
O = 68
T = 318.72
s3v70c1300-5.cnf S = OPT
O = 70
T = 664.78		 S = OPT
O = 70
T = 664.78
s3v70c1400-1.cnf S = OPT
O = 78
T = 710.56		 S = OPT
O = 78
T = 710.56
s3v70c1400-2.cnf S = OPT
O = 83
T = 1285.05		 S = OPT
O = 83
T = 1285.05
s3v70c1400-3.cnf S = OPT
O = 79
T = 968.01		 S = OPT
O = 79
T = 968.01
s3v70c1400-4.cnf S = OPT
O = 75
T = 278.63		 S = OPT
O = 75
T = 278.63
s3v70c1400-5.cnf S = OPT
O = 82
T = 1035.77		 S = OPT
O = 82
T = 1035.77
s3v70c1500-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v70c1500-2.cnf S = OPT
O = 89
T = 1153.71		 S = OPT
O = 89
T = 1153.71
s3v70c1500-3.cnf S = OPT
O = 86
T = 913.57		 S = OPT
O = 86
T = 913.57
s3v70c1500-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v70c1500-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v70c700-1.cnf S = OPT
O = 21
T = 8.51		 S = OPT
O = 21
T = 8.51
s3v70c700-2.cnf S = OPT
O = 21
T = 10.46		 S = OPT
O = 21
T = 10.46
s3v70c700-3.cnf S = OPT
O = 25
T = 17.05		 S = OPT
O = 25
T = 17.05
s3v70c700-4.cnf S = OPT
O = 24
T = 16.89		 S = OPT
O = 24
T = 16.89
s3v70c700-5.cnf S = OPT
O = 22
T = 8.12		 S = OPT
O = 22
T = 8.12
s3v70c800-1.cnf S = OPT
O = 31
T = 29.78		 S = OPT
O = 31
T = 29.78
s3v70c800-2.cnf S = OPT
O = 34
T = 82.82		 S = OPT
O = 34
T = 82.82
s3v70c800-3.cnf S = OPT
O = 30
T = 19.85		 S = OPT
O = 30
T = 19.85
s3v70c800-4.cnf S = OPT
O = 28
T = 18.19		 S = OPT
O = 28
T = 18.19
s3v70c800-5.cnf S = OPT
O = 31
T = 28.80		 S = OPT
O = 31
T = 28.80
s3v70c900-1.cnf S = OPT
O = 39
T = 69.35		 S = OPT
O = 39
T = 69.35
s3v70c900-2.cnf S = OPT
O = 38
T = 61.22		 S = OPT
O = 38
T = 61.22
s3v70c900-3.cnf S = OPT
O = 39
T = 54.70		 S = OPT
O = 39
T = 54.70
s3v70c900-4.cnf S = OPT
O = 39
T = 55.18		 S = OPT
O = 39
T = 55.18
s3v70c900-5.cnf S = OPT
O = 40
T = 87.33		 S = OPT
O = 40
T = 87.33
s3v90c1000-1.cnf S = OPT
O = 34
T = 236.26		 S = OPT
O = 34
T = 236.26
s3v90c1000-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = 38
T = TO
s3v90c1000-3.cnf S = OPT
O = 39
T = 1601.94		 S = OPT
O = 39
T = 1601.94
s3v90c1000-4.cnf S = OPT
O = 34
T = 260.36		 S = OPT
O = 34
T = 260.36
s3v90c1000-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1000-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1000-7.cnf S = OPT
O = 38
T = 930.95		 S = OPT
O = 38
T = 930.95
s3v90c1100-1.cnf S = OPT
O = 44
T = 1438.64		 S = OPT
O = 44
T = 1438.64
s3v90c1100-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = 44
T = TO
s3v90c1100-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1100-4.cnf S = OPT
O = 43
T = 1662.37		 S = OPT
O = 43
T = 1662.37
s3v90c1100-5.cnf S = OPT
O = 44
T = 1721.41		 S = OPT
O = 44
T = 1721.41
s3v90c1100-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1100-7.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1200-1.cnf S = OPT
O = 47
T = 1733.95		 S = OPT
O = 47
T = 1733.95
s3v90c1200-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1200-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1200-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1200-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1200-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = 55
T = TO
s3v90c1200-7.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1300-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1300-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1300-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1300-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1300-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1300-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c1300-7.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
s3v90c700-1.cnf S = OPT
O = 16
T = 34.33		 S = OPT
O = 16
T = 34.33
s3v90c700-2.cnf S = OPT
O = 17
T = 44.63		 S = OPT
O = 17
T = 44.63
s3v90c700-3.cnf S = OPT
O = 15
T = 22.02		 S = OPT
O = 15
T = 22.02
s3v90c700-4.cnf S = OPT
O = 18
T = 53.63		 S = OPT
O = 18
T = 53.63
s3v90c700-5.cnf S = OPT
O = 16
T = 29.14		 S = OPT
O = 16
T = 29.14
s3v90c700-6.cnf S = OPT
O = 18
T = 61.41		 S = OPT
O = 18
T = 61.41
s3v90c700-7.cnf S = OPT
O = 18
T = 63.29		 S = OPT
O = 18
T = 63.29
s3v90c800-1.cnf S = OPT
O = 22
T = 110.16		 S = OPT
O = 22
T = 110.16
s3v90c800-2.cnf S = OPT
O = 23
T = 130.61		 S = OPT
O = 23
T = 130.61
s3v90c800-3.cnf S = OPT
O = 23
T = 135.63		 S = OPT
O = 23
T = 135.63
s3v90c800-4.cnf S = OPT
O = 20
T = 48.73		 S = OPT
O = 20
T = 48.73
s3v90c800-5.cnf S = OPT
O = 24
T = 234.40		 S = OPT
O = 24
T = 234.40
s3v90c800-6.cnf S = OPT
O = 26
T = 432.03		 S = OPT
O = 26
T = 432.03
s3v90c800-7.cnf S = OPT
O = 24
T = 195.56		 S = OPT
O = 24
T = 195.56
s3v90c900-1.cnf S = OPT
O = 28
T = 139.76		 S = OPT
O = 28
T = 139.76
s3v90c900-2.cnf S = OPT
O = 28
T = 185.58		 S = OPT
O = 28
T = 185.58
s3v90c900-3.cnf S = OPT
O = 32
T = 527.27		 S = OPT
O = 32
T = 527.27
s3v90c900-4.cnf S = OPT
O = 28
T = 214.15		 S = OPT
O = 28
T = 214.15
s3v90c900-5.cnf S = OPT
O = 25
T = 57.23		 S = OPT
O = 25
T = 57.23
s3v90c900-6.cnf S = OPT
O = 30
T = 330.67		 S = OPT
O = 30
T = 330.67
s3v90c900-7.cnf S = OPT
O = 27
T = 150.09		 S = OPT
O = 27
T = 150.09
HG-3SAT-V250-C1000-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-10.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-100.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-11.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-12.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-13.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-14.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-15.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-16.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-17.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-18.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-19.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-20.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-21.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-22.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-23.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-24.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-7.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-8.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V250-C1000-9.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-10.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-100.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-11.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-12.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-13.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-14.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-15.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-16.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-17.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-18.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-19.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-20.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-21.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-22.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-23.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-24.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-7.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-8.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-3SAT-V300-C1200-9.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V100-C900-14.cnf S = OPT
O = 2
T = 1061.09		 S = OPT
O = 2
T = 1061.09
HG-4SAT-V100-C900-19.cnf S = OPT
O = 2
T = 1719.51		 S = OPT
O = 2
T = 1719.51
HG-4SAT-V100-C900-2.cnf S = OPT
O = 2
T = 1074.72		 S = OPT
O = 2
T = 1074.72
HG-4SAT-V100-C900-20.cnf S = OPT
O = 2
T = 895.56		 S = OPT
O = 2
T = 895.56
HG-4SAT-V100-C900-23.cnf S = OPT
O = 2
T = 663.58		 S = OPT
O = 2
T = 663.58
HG-4SAT-V100-C900-4.cnf S = OPT
O = 2
T = 1151.25		 S = OPT
O = 2
T = 1151.25
HG-4SAT-V100-C900-7.cnf S = OPT
O = 2
T = 1351.52		 S = OPT
O = 2
T = 1351.52
HG-4SAT-V150-C1350-1.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-10.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-100.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-11.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-12.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-13.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-14.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-15.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-16.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-17.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-18.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-19.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-2.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-20.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-21.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-22.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-23.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-24.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-3.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-4.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-5.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-6.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-7.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-8.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO
HG-4SAT-V150-C1350-9.cnf S = N/A
O = N/A
T = TO		 S = N/A
O = N/A
T = TO