[runlim] version:		1.9
[runlim] time limit:		311040000 seconds
[runlim] real time limit:	3600 seconds
[runlim] space limit:		7000 MB
[runlim] argv[0]:		/home/biere/hwmcc15/solvers/blimc/single.blimc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/kenflashp01.aig
[runlim] start:			Sat Sep 19 00:41:50 2015
[runlim] main pid:		2528
c [blimc] BLIMC Bounded Lingeling Model Checker
c [blimc] 
c [blimc] Version bas 67f8c2b0db74be9343c0b7d4c974e5121193fe90
c [blimc] 
c [blimc] Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c [blimc] All rights reserved.
c [blimc] 
c [blimc] released Tue Sep  8 16:12:24 CEST 2015
c [blimc] compiled Tue Sep  8 16:12:24 CEST 2015
c [blimc] 
c [blimc] gcc (Ubuntu 4.9.2-0ubuntu1~14.04) 4.9.2
c [blimc] -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT
c [blimc] -DNLGLFILES -DNLGLDEMA
c [blimc] Linux sili7 3.13.0-63-generic x86_64
c [blimc] 
c [blimc] 0.00 reading /home/biere/hwmcc15/benchmarks/all/selection/random/kenflashp01.aig
c [blimc] 0.00 MILOA 1351 61 57 1 1233
c [blimc] 0.00 BCJK 0 0 0 0 1233
c [blimc] 0.00 57 latches initialized to 0
c [blimc] 0.00 0 latches initialized to 1
c [blimc] 0.00 0 latches uninitialized
c [blimc] 0.00 literals  in COI:       1346 = 100% out of 1351
c [blimc] 0.00 inputs    in COI:         55 =  90% out of 61
c [blimc] 0.00 latches   in COI:         57 = 100% out of 57
c [blimc] 0.00 constants in COI:          1 = 100% out of 1
c [blimc] 0.00 ands      in COI:       1233 = 100% out of 1233
c [blimc] 0.00 encoded
c [blimc] 0.19 simplified
c [blimc] 0.19 extracted
c [lglopt]    0.183 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]    0.183 100% all
c [lglopt] 
c [lglopt]             0 conflicts,           0.0 confs/sec
c [lglopt]             0 ternaries,           0.0 confs/ternary
c [lglopt]             0 binaries,            0.0 confs/binary
c [lglopt]             0 iterations,          0.0 confs/iteration
c [lglopt] 
c [lglopt]             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c [lglopt]             0 restarts,            0.0 rests/sec,      0.0 confs/restart
c [lglopt]             0 decisions,           0.0 decis/sec,      0.0 decis/conflict
c [lglopt]         19763 propagations,   108038.8 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 0.2 seconds, 0.6 MB
c [blimc] 0.19 mapped 229 variables
c [blimc] 0.19 maxk 1000
c [blimc] 0.19 bound 0
c [blimc] 0.19 bound 1
c [blimc] 0.21 bound 2
c [blimc] 0.24 bound 3
c [blimc] 0.25 bound 4
c [blimc] 0.28 bound 5
c [blimc] 0.28 bound 6
c [blimc] 0.28 bound 7
c [blimc] 0.38 bound 8
c [blimc] 0.38 bound 9
c [blimc] 0.38 bound 10
c [blimc] 0.38 bound 11
c [blimc] 0.51 bound 12
c [blimc] 0.51 bound 13
c [blimc] 0.51 bound 14
c [blimc] 0.51 bound 15
c [blimc] 0.52 bound 16
c [blimc] 0.52 bound 17
c [blimc] 0.74 bound 18
c [blimc] 0.74 bound 19
c [blimc] 0.74 bound 20
c [blimc] 0.75 bound 21
c [blimc] 0.75 bound 22
c [blimc] 0.75 bound 23
c [blimc] 0.75 bound 24
c [blimc] 0.75 bound 25
c [blimc] 1.07 bound 26
c [blimc] 1.07 bound 27
c [blimc] 1.08 bound 28
c [blimc] 1.08 bound 29
c [blimc] 1.08 bound 30
c [blimc] 1.08 bound 31
c [blimc] 1.08 bound 32
c [blimc] 1.08 bound 33
c [blimc] 1.08 bound 34
c [blimc] 1.09 bound 35
c [blimc] 1.09 bound 36
c [blimc] 1.71 bound 37
c [blimc] 1.72 bound 38
c [blimc] 1.72 bound 39
c [blimc] 1.72 bound 40
c [blimc] 1.72 bound 41
c [blimc] 1.72 bound 42
c [blimc] 1.72 bound 43
c [blimc] 1.73 bound 44
c [blimc] 1.73 bound 45
c [blimc] 1.73 bound 46
c [blimc] 1.73 bound 47
c [blimc] 1.73 bound 48
c [blimc] 1.73 bound 49
c [blimc] 2.01 bound 50
c [blimc] 2.02 bound 51
c [blimc] 2.02 bound 52
c [blimc] 2.02 bound 53
c [blimc] 2.02 bound 54
c [blimc] 2.02 bound 55
c [blimc] 2.03 bound 56
c [blimc] 2.03 bound 57
c [blimc] 2.03 bound 58
c [blimc] 2.03 bound 59
c [blimc] 2.03 bound 60
c [blimc] 2.04 bound 61
c [blimc] 2.04 bound 62
c [blimc] 2.04 bound 63
c [blimc] 3.22 bound 64
c [blimc] 3.23 bound 65
c [blimc] 3.24 bound 66
c [blimc] 3.24 bound 67
c [blimc] 3.24 bound 68
c [blimc] 3.24 bound 69
c [blimc] 3.25 bound 70
c [blimc] 3.25 bound 71
c [blimc] 3.26 bound 72
c [blimc] 3.26 bound 73
c [blimc] 3.26 bound 74
c [blimc] 3.27 bound 75
c [blimc] 3.27 bound 76
c [blimc] 3.27 bound 77
c [blimc] 3.27 bound 78
c [blimc] 3.28 bound 79
c [blimc] 3.28 bound 80
c [blimc] 3.28 bound 81
c [blimc] 3.28 bound 82
c [blimc] 3.28 bound 83
c [blimc] 3.29 bound 84
c [blimc] 3.29 bound 85
c [blimc] 3.29 bound 86
c [blimc] 3.29 bound 87
c [blimc] 5.25 bound 88
c [blimc] 5.25 bound 89
c [blimc] 5.25 bound 90
c [blimc] 5.25 bound 91
c [blimc] 5.26 bound 92
c [blimc] 5.26 bound 93
c [blimc] 5.26 bound 94
c [blimc] 5.26 bound 95
c [blimc] 5.27 bound 96
c [blimc] 5.27 bound 97
c [blimc] 5.27 bound 98
c [blimc] 5.27 bound 99
c [blimc] 5.28 bound 100
c [blimc] 5.28 bound 101
c [blimc] 5.28 bound 102
c [blimc] 5.28 bound 103
c [blimc] 5.29 bound 104
c [blimc] 5.29 bound 105
c [blimc] 5.29 bound 106
c [blimc] 5.29 bound 107
c [blimc] 5.30 bound 108
c [blimc] 5.30 bound 109
c [blimc] 5.30 bound 110
c [blimc] 5.31 bound 111
c [blimc] 5.31 bound 112
c [blimc] 5.31 bound 113
c [blimc] 5.31 bound 114
c [blimc] 5.32 bound 115
c [blimc] 5.32 bound 116
c [blimc] 5.32 bound 117
c [blimc] 5.33 bound 118
c [blimc] 5.33 bound 119
c [blimc] 8.91 bound 120
c [blimc] 8.94 bound 121
c [blimc] 8.94 bound 122
c [blimc] 8.94 bound 123
c [blimc] 8.95 bound 124
c [blimc] 8.95 bound 125
c [blimc] 8.95 bound 126
c [blimc] 8.95 bound 127
c [blimc] 8.96 bound 128
c [blimc] 8.96 bound 129
c [blimc] 8.96 bound 130
c [blimc] 8.96 bound 131
c [blimc] 8.99 bound 132
c [blimc] 8.99 bound 133
c [blimc] 8.99 bound 134
c [blimc] 9.00 bound 135
c [blimc] 9.00 bound 136
c [blimc] 9.01 bound 137
c [blimc] 9.01 bound 138
c [blimc] 9.01 bound 139
c [blimc] 9.02 bound 140
c [blimc] 9.02 bound 141
c [blimc] 9.02 bound 142
c [blimc] 9.03 bound 143
c [blimc] 9.03 bound 144
c [blimc] 9.03 bound 145
c [blimc] 9.04 bound 146
c [blimc] 9.04 bound 147
c [blimc] 9.05 bound 148
c [blimc] 9.05 bound 149
c [blimc] 9.05 bound 150
c [blimc] 9.06 bound 151
c [blimc] 9.06 bound 152
c [blimc] 9.07 bound 153
c [blimc] 9.07 bound 154
c [blimc] 9.08 bound 155
c [blimc] 9.08 bound 156
[runlim] sample:		10.0 time, 10.3 real, 19.5 MB
c [blimc] 10.88 bound 157
c [blimc] 10.89 bound 158
c [blimc] 10.89 bound 159
c [blimc] 10.89 bound 160
c [blimc] 10.90 bound 161
c [blimc] 10.90 bound 162
c [blimc] 10.90 bound 163
c [blimc] 10.91 bound 164
c [blimc] 10.92 bound 165
c [blimc] 10.92 bound 166
c [blimc] 10.92 bound 167
c [blimc] 10.93 bound 168
c [blimc] 10.93 bound 169
c [blimc] 10.94 bound 170
c [blimc] 10.94 bound 171
c [blimc] 10.95 bound 172
c [blimc] 10.95 bound 173
c [blimc] 10.95 bound 174
c [blimc] 10.96 bound 175
c [blimc] 10.96 bound 176
c [blimc] 10.97 bound 177
c [blimc] 10.97 bound 178
c [blimc] 10.98 bound 179
c [blimc] 10.98 bound 180
c [blimc] 10.99 bound 181
c [blimc] 11.00 bound 182
c [blimc] 11.00 bound 183
c [blimc] 11.00 bound 184
c [blimc] 11.01 bound 185
c [blimc] 11.02 bound 186
c [blimc] 11.02 bound 187
c [blimc] 11.03 bound 188
c [blimc] 11.04 bound 189
c [blimc] 11.04 bound 190
c [blimc] 11.05 bound 191
c [blimc] 11.05 bound 192
c [blimc] 11.06 bound 193
c [blimc] 11.06 bound 194
c [blimc] 11.07 bound 195
c [blimc] 11.07 bound 196
c [blimc] 11.08 bound 197
c [blimc] 11.09 bound 198
c [blimc] 11.09 bound 199
c [blimc] 11.10 bound 200
c [blimc] 11.11 bound 201
c [blimc] 11.11 bound 202
c [blimc] 11.12 bound 203
c [blimc] 11.13 bound 204
c [blimc] 11.13 bound 205
c [blimc] 11.14 bound 206
c [blimc] 11.15 bound 207
c [blimc] 11.15 bound 208
c [blimc] 11.16 bound 209
c [blimc] 11.17 bound 210
c [blimc] 11.18 bound 211
c [blimc] 11.18 bound 212
c [blimc] 11.19 bound 213
c [blimc] 11.20 bound 214
c [blimc] 11.21 bound 215
c [blimc] 12.79 bound 216
c [blimc] 12.79 bound 217
c [blimc] 12.83 bound 218
c [blimc] 12.84 bound 219
c [blimc] 12.85 bound 220
c [blimc] 12.85 bound 221
c [blimc] 12.86 bound 222
c [blimc] 12.86 bound 223
c [blimc] 12.87 bound 224
c [blimc] 12.88 bound 225
c [blimc] 12.89 bound 226
c [blimc] 12.89 bound 227
c [blimc] 12.90 bound 228
c [blimc] 12.91 bound 229
c [blimc] 12.92 bound 230
c [blimc] 12.92 bound 231
c [blimc] 12.93 bound 232
c [blimc] 12.94 bound 233
c [blimc] 15.08 bound 234
c [blimc] 15.10 bound 235
c [blimc] 15.10 bound 236
c [blimc] 15.11 bound 237
c [blimc] 15.21 bound 238
c [blimc] 15.22 bound 239
c [blimc] 15.23 bound 240
c [blimc] 15.23 bound 241
c [blimc] 15.24 bound 242
c [blimc] 15.25 bound 243
c [blimc] 15.25 bound 244
c [blimc] 15.26 bound 245
c [blimc] 15.27 bound 246
c [blimc] 15.28 bound 247
c [blimc] 15.28 bound 248
c [blimc] 15.29 bound 249
c [blimc] 15.30 bound 250
c [blimc] 15.31 bound 251
c [blimc] 15.31 bound 252
c [blimc] 15.32 bound 253
c [blimc] 15.33 bound 254
c [blimc] 15.33 bound 255
c [blimc] 15.34 bound 256
c [blimc] 15.35 bound 257
c [blimc] 15.36 bound 258
c [blimc] 15.36 bound 259
c [blimc] 15.38 bound 260
c [blimc] 15.38 bound 261
c [blimc] 15.39 bound 262
c [blimc] 15.40 bound 263
c [blimc] 15.41 bound 264
c [blimc] 15.41 bound 265
c [blimc] 15.42 bound 266
c [blimc] 15.43 bound 267
c [blimc] 15.44 bound 268
c [blimc] 15.45 bound 269
c [blimc] 15.46 bound 270
c [blimc] 15.46 bound 271
c [blimc] 15.47 bound 272
c [blimc] 15.48 bound 273
c [blimc] 15.49 bound 274
c [blimc] 15.50 bound 275
c [blimc] 15.51 bound 276
c [blimc] 15.52 bound 277
c [blimc] 15.53 bound 278
c [blimc] 15.54 bound 279
c [blimc] 15.54 bound 280
c [blimc] 15.56 bound 281
c [blimc] 15.56 bound 282
c [blimc] 15.57 bound 283
c [blimc] 15.58 bound 284
c [blimc] 15.59 bound 285
c [blimc] 15.60 bound 286
c [blimc] 15.61 bound 287
c [blimc] 15.62 bound 288
c [blimc] 15.63 bound 289
c [blimc] 15.64 bound 290
c [blimc] 15.65 bound 291
c [blimc] 15.66 bound 292
c [blimc] 15.67 bound 293
c [blimc] 15.68 bound 294
c [blimc] 15.69 bound 295
c [blimc] 15.70 bound 296
c [blimc] 15.71 bound 297
c [blimc] 15.72 bound 298
c [blimc] 15.80 bound 299
c [blimc] 15.80 bound 300
c [blimc] 15.82 bound 301
c [blimc] 15.83 bound 302
c [blimc] 15.85 bound 303
c [blimc] 15.85 bound 304
c [blimc] 15.86 bound 305
c [blimc] 15.88 bound 306
c [blimc] 15.89 bound 307
c [blimc] 15.90 bound 308
c [blimc] 15.91 bound 309
c [blimc] 15.92 bound 310
c [blimc] 15.93 bound 311
c [blimc] 15.94 bound 312
c [blimc] 15.96 bound 313
c [blimc] 15.97 bound 314
c [blimc] 15.98 bound 315
c [blimc] 15.99 bound 316
c [blimc] 16.00 bound 317
c [blimc] 16.01 bound 318
c [blimc] 16.02 bound 319
c [blimc] 16.03 bound 320
c [blimc] 16.04 bound 321
c [blimc] 16.06 bound 322
c [blimc] 16.07 bound 323
c [blimc] 16.08 bound 324
c [blimc] 16.09 bound 325
c [blimc] 16.10 bound 326
c [blimc] 16.11 bound 327
c [blimc] 18.11 bound 328
c [blimc] 18.12 bound 329
c [blimc] 18.13 bound 330
c [blimc] 18.14 bound 331
c [blimc] 18.15 bound 332
c [blimc] 18.16 bound 333
c [blimc] 18.17 bound 334
c [blimc] 18.18 bound 335
c [blimc] 18.19 bound 336
c [blimc] 18.20 bound 337
c [blimc] 18.21 bound 338
c [blimc] 18.22 bound 339
c [blimc] 18.23 bound 340
c [blimc] 18.24 bound 341
c [blimc] 18.25 bound 342
c [blimc] 18.27 bound 343
c [blimc] 18.27 bound 344
c [blimc] 18.28 bound 345
c [blimc] 18.30 bound 346
c [blimc] 18.31 bound 347
c [blimc] 18.32 bound 348
c [blimc] 18.33 bound 349
c [blimc] 18.34 bound 350
c [blimc] 18.35 bound 351
c [blimc] 18.36 bound 352
c [blimc] 18.37 bound 353
c [blimc] 18.38 bound 354
c [blimc] 18.40 bound 355
c [blimc] 18.40 bound 356
c [blimc] 18.41 bound 357
c [blimc] 18.43 bound 358
c [blimc] 18.44 bound 359
[runlim] sample:		20.0 time, 20.3 real, 48.5 MB
c [blimc] 21.78 bound 360
c [blimc] 21.80 bound 361
c [blimc] 21.92 bound 362
c [blimc] 21.94 bound 363
c [blimc] 21.96 bound 364
c [blimc] 21.97 bound 365
c [blimc] 21.98 bound 366
c [blimc] 21.99 bound 367
c [blimc] 22.00 bound 368
c [blimc] 22.02 bound 369
c [blimc] 22.02 bound 370
c [blimc] 22.03 bound 371
c [blimc] 22.05 bound 372
c [blimc] 22.06 bound 373
c [blimc] 22.07 bound 374
c [blimc] 22.08 bound 375
c [blimc] 22.20 bound 376
c [blimc] 22.21 bound 377
c [blimc] 22.22 bound 378
c [blimc] 22.23 bound 379
c [blimc] 22.25 bound 380
c [blimc] 22.26 bound 381
c [blimc] 22.30 bound 382
c [blimc] 22.31 bound 383
c [blimc] 22.33 bound 384
c [blimc] 22.34 bound 385
c [blimc] 22.35 bound 386
c [blimc] 22.36 bound 387
c [blimc] 22.38 bound 388
c [blimc] 22.39 bound 389
c [blimc] 22.40 bound 390
c [blimc] 22.41 bound 391
c [blimc] 22.43 bound 392
c [blimc] 22.44 bound 393
c [blimc] 22.46 bound 394
c [blimc] 22.47 bound 395
c [blimc] 22.48 bound 396
c [blimc] 22.49 bound 397
c [blimc] 22.51 bound 398
c [blimc] 22.52 bound 399
c [blimc] 22.54 bound 400
c [blimc] 22.55 bound 401
c [blimc] 22.57 bound 402
c [blimc] 22.58 bound 403
c [blimc] 22.59 bound 404
c [blimc] 22.60 bound 405
c [blimc] 22.62 bound 406
c [blimc] 22.63 bound 407
c [blimc] 22.65 bound 408
c [blimc] 22.66 bound 409
c [blimc] 22.68 bound 410
c [blimc] 22.69 bound 411
c [blimc] 22.71 bound 412
c [blimc] 22.72 bound 413
c [blimc] 22.74 bound 414
c [blimc] 22.75 bound 415
c [blimc] 22.77 bound 416
c [blimc] 22.78 bound 417
c [blimc] 22.80 bound 418
c [blimc] 22.81 bound 419
c [blimc] 22.83 bound 420
c [blimc] 22.84 bound 421
c [blimc] 22.86 bound 422
c [blimc] 22.87 bound 423
c [blimc] 22.89 bound 424
c [blimc] 22.90 bound 425
c [blimc] 22.92 bound 426
c [blimc] 22.93 bound 427
c [blimc] 22.95 bound 428
c [blimc] 22.96 bound 429
c [blimc] 22.98 bound 430
c [blimc] 22.99 bound 431
c [blimc] 23.01 bound 432
c [blimc] 23.02 bound 433
c [blimc] 23.04 bound 434
c [blimc] 23.06 bound 435
c [blimc] 23.08 bound 436
c [blimc] 23.09 bound 437
c [blimc] 23.11 bound 438
c [blimc] 23.12 bound 439
c [blimc] 23.14 bound 440
c [blimc] 23.15 bound 441
c [blimc] 23.17 bound 442
c [blimc] 23.18 bound 443
c [blimc] 23.21 bound 444
c [blimc] 23.22 bound 445
c [blimc] 23.24 bound 446
c [blimc] 23.25 bound 447
c [blimc] 23.27 bound 448
c [blimc] 23.28 bound 449
c [blimc] 23.31 bound 450
c [blimc] 23.32 bound 451
c [blimc] 23.34 bound 452
c [blimc] 23.35 bound 453
c [blimc] 23.37 bound 454
c [blimc] 23.39 bound 455
c [blimc] 23.41 bound 456
c [blimc] 23.42 bound 457
c [blimc] 23.44 bound 458
c [blimc] 23.46 bound 459
c [blimc] 23.48 bound 460
c [blimc] 23.49 bound 461
c [blimc] 23.51 bound 462
c [blimc] 23.53 bound 463
c [blimc] 25.79 bound 464
c [blimc] 25.81 bound 465
c [blimc] 25.82 bound 466
c [blimc] 25.84 bound 467
c [blimc] 25.85 bound 468
c [blimc] 25.87 bound 469
c [blimc] 25.94 bound 470
c [blimc] 25.95 bound 471
c [blimc] 25.97 bound 472
c [blimc] 25.98 bound 473
c [blimc] 26.01 bound 474
c [blimc] 26.02 bound 475
c [blimc] 26.04 bound 476
c [blimc] 26.05 bound 477
c [blimc] 26.08 bound 478
c [blimc] 26.09 bound 479
c [blimc] 26.10 bound 480
c [blimc] 26.36 bound 481
c [blimc] 26.37 bound 482
c [blimc] 26.40 bound 483
c [blimc] 26.41 bound 484
c [blimc] 26.44 bound 485
c [blimc] 26.45 bound 486
c [blimc] 26.47 bound 487
c [blimc] 26.49 bound 488
c [blimc] 26.51 bound 489
c [blimc] 26.52 bound 490
c [blimc] 26.54 bound 491
c [blimc] 26.56 bound 492
c [blimc] 26.58 bound 493
c [blimc] 26.59 bound 494
c [blimc] 26.61 bound 495
c [blimc] 26.63 bound 496
c [blimc] 26.65 bound 497
c [blimc] 26.66 bound 498
c [blimc] 26.69 bound 499
c [blimc] 26.70 bound 500
c [blimc] 26.72 bound 501
c [blimc] 26.73 bound 502
c [blimc] 26.75 bound 503
c [blimc] 26.79 bound 504
c [blimc] 26.80 bound 505
c [blimc] 26.82 bound 506
c [blimc] 26.84 bound 507
c [blimc] 26.86 bound 508
c [blimc] 26.87 bound 509
c [blimc] 26.88 bound 510
c [blimc] 26.91 bound 511
c [blimc] 26.92 bound 512
c [blimc] 26.95 bound 513
c [blimc] 26.96 bound 514
c [blimc] 26.98 bound 515
c [blimc] 27.00 bound 516
c [blimc] 27.01 bound 517
c [blimc] 27.04 bound 518
c [blimc] 27.05 bound 519
c [blimc] 27.07 bound 520
c [blimc] 27.09 bound 521
c [blimc] 27.10 bound 522
c [blimc] 27.13 bound 523
c [blimc] 27.14 bound 524
c [blimc] 27.16 bound 525
c [blimc] 27.18 bound 526
c [blimc] 27.19 bound 527
c [blimc] 27.22 bound 528
c [blimc] 27.23 bound 529
c [blimc] 27.26 bound 530
c [blimc] 27.27 bound 531
c [blimc] 27.29 bound 532
c [blimc] 27.31 bound 533
c [blimc] 27.33 bound 534
c [blimc] 27.35 bound 535
c [blimc] 27.37 bound 536
c [blimc] 27.38 bound 537
c [blimc] 27.41 bound 538
c [blimc] 27.43 bound 539
c [blimc] 27.45 bound 540
c [blimc] 27.47 bound 541
c [blimc] 27.48 bound 542
c [blimc] 27.51 bound 543
c [blimc] 27.52 bound 544
c [blimc] 27.55 bound 545
c [blimc] 27.57 bound 546
c [blimc] 27.58 bound 547
c [blimc] 27.61 bound 548
c [blimc] 27.63 bound 549
c [blimc] 27.65 bound 550
c [blimc] 27.67 bound 551
c [blimc] 27.68 bound 552
c [blimc] 27.71 bound 553
c [blimc] 27.73 bound 554
c [blimc] 27.76 bound 555
c [blimc] 27.77 bound 556
c [blimc] 27.79 bound 557
c [blimc] 27.81 bound 558
c [blimc] 27.83 bound 559
c [blimc] 27.86 bound 560
c [blimc] 27.88 bound 561
c [blimc] 27.89 bound 562
c [blimc] 27.92 bound 563
c [blimc] 27.94 bound 564
c [blimc] 27.97 bound 565
c [blimc] 27.99 bound 566
c [blimc] 28.00 bound 567
c [blimc] 28.03 bound 568
c [blimc] 28.05 bound 569
c [blimc] 28.08 bound 570
c [blimc] 28.10 bound 571
c [blimc] 28.12 bound 572
c [blimc] 28.15 bound 573
c [blimc] 28.17 bound 574
c [blimc] 28.19 bound 575
c [blimc] 28.22 bound 576
c [blimc] 28.24 bound 577
c [blimc] 28.26 bound 578
c [blimc] 28.29 bound 579
c [blimc] 28.31 bound 580
c [blimc] 28.33 bound 581
c [blimc] 28.36 bound 582
c [blimc] 28.37 bound 583
c [blimc] 28.40 bound 584
c [blimc] 28.43 bound 585
c [blimc] 28.44 bound 586
c [blimc] 28.47 bound 587
c [blimc] 28.50 bound 588
c [blimc] 28.51 bound 589
c [blimc] 28.54 bound 590
c [blimc] 28.57 bound 591
c [blimc] 28.59 bound 592
c [blimc] 28.60 bound 593
c [blimc] 28.63 bound 594
c [blimc] 28.65 bound 595
c [blimc] 29.39 bound 596
c [blimc] 29.41 bound 597
c [blimc] 29.43 bound 598
c [blimc] 29.46 bound 599
c [blimc] 29.48 bound 600
c [blimc] 29.52 bound 601
c [blimc] 29.53 bound 602
c [blimc] 29.55 bound 603
c [blimc] 29.59 bound 604
[runlim] sample:		29.9 time, 30.3 real, 74.0 MB
c [blimc] 34.93 bound 605
c [blimc] 34.99 bound 606
c [blimc] 35.01 bound 607
c [blimc] 35.04 bound 608
c [blimc] 35.05 bound 609
c [blimc] 35.07 bound 610
c [blimc] 35.09 bound 611
c [blimc] 35.11 bound 612
c [blimc] 35.14 bound 613
c [blimc] 35.15 bound 614
c [blimc] 35.17 bound 615
c [blimc] 35.20 bound 616
c [blimc] 35.22 bound 617
c [blimc] 35.24 bound 618
c [blimc] 35.26 bound 619
c [blimc] 35.27 bound 620
c [blimc] 35.30 bound 621
c [blimc] 35.32 bound 622
c [blimc] 35.35 bound 623
c [blimc] 35.36 bound 624
c [blimc] 35.38 bound 625
c [blimc] 35.41 bound 626
c [blimc] 35.43 bound 627
c [blimc] 35.45 bound 628
c [blimc] 35.48 bound 629
c [blimc] 35.49 bound 630
c [blimc] 35.51 bound 631
c [blimc] 35.54 bound 632
c [blimc] 35.56 bound 633
c [blimc] 35.58 bound 634
c [blimc] 35.61 bound 635
c [blimc] 35.62 bound 636
c [blimc] 35.64 bound 637
c [blimc] 35.67 bound 638
c [blimc] 35.69 bound 639
c [blimc] 35.71 bound 640
c [blimc] 35.74 bound 641
c [blimc] 35.76 bound 642
c [blimc] 35.78 bound 643
c [blimc] 35.81 bound 644
c [blimc] 35.82 bound 645
c [blimc] 35.84 bound 646
c [blimc] 35.87 bound 647
c [blimc] 35.89 bound 648
c [blimc] 35.91 bound 649
c [blimc] 35.94 bound 650
c [blimc] 35.97 bound 651
c [blimc] 36.00 bound 652
c [blimc] 36.02 bound 653
c [blimc] 36.32 bound 654
c [blimc] 36.34 bound 655
c [blimc] 36.36 bound 656
c [blimc] 36.39 bound 657
c [blimc] 36.41 bound 658
c [blimc] 36.45 bound 659
c [blimc] 36.46 bound 660
c [blimc] 36.48 bound 661
c [blimc] 36.51 bound 662
c [blimc] 36.54 bound 663
c [blimc] 36.57 bound 664
c [blimc] 36.59 bound 665
c [blimc] 36.60 bound 666
c [blimc] 36.64 bound 667
c [blimc] 36.66 bound 668
c [blimc] 36.69 bound 669
c [blimc] 36.71 bound 670
c [blimc] 36.73 bound 671
c [blimc] 36.76 bound 672
c [blimc] 36.78 bound 673
c [blimc] 36.82 bound 674
c [blimc] 36.83 bound 675
c [blimc] 36.85 bound 676
c [blimc] 36.89 bound 677
c [blimc] 36.91 bound 678
c [blimc] 36.94 bound 679
c [blimc] 36.96 bound 680
c [blimc] 36.98 bound 681
c [blimc] 37.02 bound 682
c [blimc] 37.04 bound 683
c [blimc] 37.07 bound 684
c [blimc] 37.09 bound 685
c [blimc] 37.11 bound 686
c [blimc] 37.14 bound 687
c [blimc] 37.16 bound 688
c [blimc] 37.20 bound 689
c [blimc] 37.22 bound 690
c [blimc] 37.24 bound 691
c [blimc] 37.27 bound 692
c [blimc] 37.29 bound 693
c [blimc] 37.33 bound 694
c [blimc] 37.35 bound 695
c [blimc] 37.37 bound 696
c [blimc] 37.40 bound 697
c [blimc] 37.43 bound 698
c [blimc] 37.46 bound 699
c [blimc] 37.48 bound 700
c [blimc] 37.50 bound 701
c [blimc] 37.54 bound 702
c [blimc] 37.56 bound 703
c [blimc] 37.59 bound 704
[runlim] sample:		39.9 time, 40.3 real, 86.0 MB
c [blimc] 41.02 bound 705
c [blimc] 41.05 bound 706
c [blimc] 41.08 bound 707
c [blimc] 41.10 bound 708
c [blimc] 41.12 bound 709
c [blimc] 41.15 bound 710
c [blimc] 41.17 bound 711
c [blimc] 41.18 bound 712
c [blimc] 41.22 bound 713
c [blimc] 41.24 bound 714
c [blimc] 41.27 bound 715
c [blimc] 41.29 bound 716
c [blimc] 41.30 bound 717
c [blimc] 41.34 bound 718
c [blimc] 41.36 bound 719
c [blimc] 41.39 bound 720
c [blimc] 41.41 bound 721
c [blimc] 41.43 bound 722
c [blimc] 41.46 bound 723
c [blimc] 41.48 bound 724
c [blimc] 41.52 bound 725
c [blimc] 41.53 bound 726
c [blimc] 41.55 bound 727
c [blimc] 41.59 bound 728
c [blimc] 41.61 bound 729
c [blimc] 41.64 bound 730
c [blimc] 41.66 bound 731
c [blimc] 41.68 bound 732
c [blimc] 41.72 bound 733
c [blimc] 41.74 bound 734
c [blimc] 41.77 bound 735
c [blimc] 41.79 bound 736
c [blimc] 41.81 bound 737
c [blimc] 41.85 bound 738
c [blimc] 41.87 bound 739
c [blimc] 41.90 bound 740
c [blimc] 41.92 bound 741
c [blimc] 41.94 bound 742
c [blimc] 41.98 bound 743
c [blimc] 42.00 bound 744
c [blimc] 42.03 bound 745
c [blimc] 42.05 bound 746
c [blimc] 42.09 bound 747
c [blimc] 42.11 bound 748
c [blimc] 42.15 bound 749
c [blimc] 42.17 bound 750
c [blimc] 42.20 bound 751
c [blimc] 42.22 bound 752
c [blimc] 42.26 bound 753
c [blimc] 42.28 bound 754
c [blimc] 42.31 bound 755
c [blimc] 42.34 bound 756
c [blimc] 42.37 bound 757
c [blimc] 42.39 bound 758
c [blimc] 42.43 bound 759
c [blimc] 42.45 bound 760
c [blimc] 42.49 bound 761
c [blimc] 42.51 bound 762
c [blimc] 42.54 bound 763
c [blimc] 42.56 bound 764
c [blimc] 42.60 bound 765
c [blimc] 42.62 bound 766
c [blimc] 42.66 bound 767
c [blimc] 42.71 bound 768
c [blimc] 42.73 bound 769
c [blimc] 43.56 bound 770
c [blimc] 43.58 bound 771
c [blimc] 43.60 bound 772
c [blimc] 43.75 bound 773
c [blimc] 43.77 bound 774
c [blimc] 43.81 bound 775
c [blimc] 43.83 bound 776
c [blimc] 43.87 bound 777
c [blimc] 43.89 bound 778
c [blimc] 43.93 bound 779
c [blimc] 43.95 bound 780
c [blimc] 43.98 bound 781
c [blimc] 44.01 bound 782
c [blimc] 44.04 bound 783
c [blimc] 44.07 bound 784
c [blimc] 44.10 bound 785
c [blimc] 44.12 bound 786
c [blimc] 44.16 bound 787
c [blimc] 44.18 bound 788
c [blimc] 44.22 bound 789
c [blimc] 44.25 bound 790
c [blimc] 44.28 bound 791
c [blimc] 44.31 bound 792
c [blimc] 44.34 bound 793
c [blimc] 44.37 bound 794
c [blimc] 44.41 bound 795
c [blimc] 44.43 bound 796
c [blimc] 44.47 bound 797
c [blimc] 44.49 bound 798
c [blimc] 44.53 bound 799
c [blimc] 44.55 bound 800
c [blimc] 44.59 bound 801
c [blimc] 44.61 bound 802
c [blimc] 44.65 bound 803
c [blimc] 44.68 bound 804
c [blimc] 44.72 bound 805
c [blimc] 44.74 bound 806
c [blimc] 44.78 bound 807
c [blimc] 44.80 bound 808
c [blimc] 44.84 bound 809
c [blimc] 44.86 bound 810
c [blimc] 44.90 bound 811
c [blimc] 44.93 bound 812
c [blimc] 44.97 bound 813
c [blimc] 44.99 bound 814
c [blimc] 45.03 bound 815
c [blimc] 45.06 bound 816
c [blimc] 45.10 bound 817
c [blimc] 45.12 bound 818
c [blimc] 45.16 bound 819
c [blimc] 45.19 bound 820
c [blimc] 45.23 bound 821
c [blimc] 45.25 bound 822
c [blimc] 45.29 bound 823
c [blimc] 45.32 bound 824
c [blimc] 45.36 bound 825
c [blimc] 45.38 bound 826
c [blimc] 45.42 bound 827
c [blimc] 45.45 bound 828
c [blimc] 45.49 bound 829
c [blimc] 45.51 bound 830
c [blimc] 45.56 bound 831
c [blimc] 45.58 bound 832
c [blimc] 45.62 bound 833
c [blimc] 45.65 bound 834
c [blimc] 45.69 bound 835
c [blimc] 45.72 bound 836
c [blimc] 45.76 bound 837
c [blimc] 45.79 bound 838
c [blimc] 45.83 bound 839
c [blimc] 45.86 bound 840
c [blimc] 45.90 bound 841
c [blimc] 45.93 bound 842
c [blimc] 45.97 bound 843
c [blimc] 46.00 bound 844
c [blimc] 46.04 bound 845
c [blimc] 46.07 bound 846
c [blimc] 46.11 bound 847
c [blimc] 46.14 bound 848
c [blimc] 46.18 bound 849
c [blimc] 46.21 bound 850
c [blimc] 46.26 bound 851
c [blimc] 46.28 bound 852
c [blimc] 46.33 bound 853
c [blimc] 46.35 bound 854
c [blimc] 46.40 bound 855
c [blimc] 46.42 bound 856
c [blimc] 46.47 bound 857
c [blimc] 46.49 bound 858
c [blimc] 46.54 bound 859
[runlim] sample:		49.9 time, 50.3 real, 104.2 MB
c [blimc] 57.30 bound 860
c [blimc] 57.46 bound 861
c [blimc] 57.49 bound 862
c [blimc] 58.19 bound 863
c [blimc] 58.21 bound 864
c [blimc] 58.23 bound 865
c [blimc] 58.27 bound 866
c [blimc] 58.29 bound 867
c [blimc] 58.31 bound 868
c [blimc] 58.40 bound 869
c [blimc] 58.43 bound 870
c [blimc] 58.47 bound 871
c [blimc] 58.59 bound 872
c [blimc] 58.61 bound 873
c [blimc] 58.66 bound 874
c [blimc] 58.69 bound 875
c [blimc] 58.73 bound 876
c [blimc] 58.75 bound 877
c [blimc] 58.79 bound 878
[runlim] sample:		59.9 time, 60.3 real, 86.6 MB
[runlim] sample:		69.9 time, 70.3 real, 134.5 MB
[runlim] sample:		79.9 time, 80.3 real, 170.3 MB
c [blimc] 89.54 bound 879
c [blimc] 89.61 bound 880
c [blimc] 89.63 bound 881
[runlim] sample:		89.9 time, 90.3 real, 90.9 MB
c [blimc] 89.96 bound 882
c [blimc] 89.98 bound 883
c [blimc] 90.03 bound 884
c [blimc] 90.05 bound 885
c [blimc] 90.10 bound 886
c [blimc] 90.12 bound 887
c [blimc] 90.16 bound 888
c [blimc] 90.18 bound 889
c [blimc] 90.23 bound 890
c [blimc] 90.25 bound 891
c [blimc] 90.29 bound 892
c [blimc] 90.32 bound 893
c [blimc] 90.36 bound 894
c [blimc] 90.38 bound 895
c [blimc] 90.42 bound 896
c [blimc] 90.45 bound 897
c [blimc] 90.49 bound 898
c [blimc] 90.52 bound 899
c [blimc] 90.56 bound 900
c [blimc] 90.58 bound 901
c [blimc] 90.63 bound 902
c [blimc] 90.65 bound 903
c [blimc] 90.70 bound 904
c [blimc] 90.72 bound 905
c [blimc] 90.76 bound 906
c [blimc] 90.79 bound 907
c [blimc] 90.83 bound 908
c [blimc] 90.86 bound 909
c [blimc] 90.90 bound 910
c [blimc] 90.93 bound 911
c [blimc] 90.97 bound 912
c [blimc] 90.99 bound 913
c [blimc] 91.04 bound 914
c [blimc] 91.06 bound 915
c [blimc] 91.11 bound 916
c [blimc] 91.13 bound 917
c [blimc] 91.18 bound 918
c [blimc] 91.20 bound 919
c [blimc] 91.24 bound 920
c [blimc] 91.27 bound 921
c [blimc] 91.31 bound 922
c [blimc] 91.34 bound 923
c [blimc] 91.38 bound 924
c [blimc] 91.41 bound 925
c [blimc] 91.45 bound 926
c [blimc] 91.48 bound 927
c [blimc] 91.52 bound 928
c [blimc] 91.55 bound 929
c [blimc] 91.59 bound 930
c [blimc] 91.62 bound 931
c [blimc] 91.66 bound 932
c [blimc] 91.69 bound 933
c [blimc] 91.74 bound 934
c [blimc] 91.76 bound 935
c [blimc] 91.81 bound 936
c [blimc] 91.83 bound 937
c [blimc] 91.88 bound 938
c [blimc] 91.90 bound 939
c [blimc] 91.95 bound 940
c [blimc] 91.98 bound 941
c [blimc] 92.02 bound 942
c [blimc] 92.05 bound 943
c [blimc] 92.10 bound 944
c [blimc] 92.13 bound 945
c [blimc] 92.17 bound 946
c [blimc] 92.20 bound 947
c [blimc] 92.25 bound 948
c [blimc] 92.27 bound 949
c [blimc] 92.32 bound 950
c [blimc] 92.34 bound 951
c [blimc] 92.39 bound 952
c [blimc] 92.42 bound 953
c [blimc] 92.47 bound 954
c [blimc] 92.49 bound 955
c [blimc] 92.54 bound 956
c [blimc] 92.57 bound 957
c [blimc] 92.61 bound 958
c [blimc] 92.64 bound 959
c [blimc] 92.69 bound 960
c [blimc] 92.72 bound 961
c [blimc] 92.76 bound 962
c [blimc] 92.79 bound 963
c [blimc] 92.84 bound 964
c [blimc] 92.89 bound 965
c [blimc] 92.91 bound 966
c [blimc] 94.18 bound 967
c [blimc] 94.21 bound 968
c [blimc] 94.26 bound 969
c [blimc] 94.29 bound 970
c [blimc] 94.40 bound 971
c [blimc] 94.42 bound 972
c [blimc] 94.45 bound 973
c [blimc] 94.79 bound 974
c [blimc] 94.82 bound 975
c [blimc] 94.87 bound 976
c [blimc] 94.90 bound 977
c [blimc] 94.93 bound 978
c [blimc] 94.98 bound 979
c [blimc] 95.02 bound 980
c [blimc] 95.07 bound 981
c [blimc] 95.10 bound 982
c [blimc] 95.15 bound 983
c [blimc] 95.18 bound 984
c [blimc] 95.21 bound 985
c [blimc] 95.28 bound 986
c [blimc] 95.31 bound 987
[runlim] sample:		99.9 time, 100.3 real, 119.0 MB
[runlim] sample:		109.8 time, 110.3 real, 134.3 MB
c [blimc] 115.86 bound 988
c [blimc] 116.02 bound 989
c [blimc] 116.04 bound 990
c [blimc] 116.12 bound 991
c [blimc] 116.15 bound 992
c [blimc] 116.18 bound 993
c [blimc] 116.23 bound 994
c [blimc] 116.26 bound 995
c [blimc] 116.29 bound 996
c [blimc] 116.53 bound 997
c [blimc] 116.56 bound 998
c [blimc] 116.58 bound 999
c [blimc] 116.63 bound 1000
c [lgl1000]   85.977  80% simplifying
c [lgl1000]   20.330  19% search
c [lgl1000] ==================================
c [lgl1000]  107.971 100% all
c [lgl1000] 
c [lgl1000]         20670 conflicts,         191.4 confs/sec
c [lgl1000]          5031 ternaries,           4.1 confs/ternary
c [lgl1000]          1625 binaries,           12.7 confs/binary
c [lgl1000]           998 iterations,         20.7 confs/iteration
c [lgl1000] 
c [lgl1000]             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c [lgl1000]           187 restarts,            1.7 rests/sec,    110.5 confs/restart
c [lgl1000]       6961935 decisions,       64479.6 decis/sec,    336.8 decis/conflict
c [lgl1000]      67505404 propagations,   625217.4 props/sec,      9.7 props/decision
c [lgl1000] 
c [lgl1000] 108.0 seconds, 244.9 MB
c [blimc] 116.67 reached k = 1001
c [blimc] 116.67 cloned 2 solvers
c [blimc] 116.67 max 244.9 MB
c [blimc] 116.67 exit 20
[runlim] end:			Sat Sep 19 00:43:47 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			117.21 seconds
[runlim] time:			116.64 seconds
[runlim] space:			242.3 MB
[runlim] samples:		1168
