[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/6s362rb1.aig
[runlim] start:			Sun Sep 20 05:01:02 2015
[runlim] main pid:		10295
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/6s362rb1.aig
c [blimc] 0.00 MILOA 9831 13 1863 1 7955
c [blimc] 0.00 BCJK 0 0 0 0 7955
c [blimc] 0.00 1863 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:       9747 =  99% out of 9831
c [blimc] 0.00 inputs    in COI:         13 = 100% out of 13
c [blimc] 0.00 latches   in COI:       1850 =  99% out of 1863
c [blimc] 0.00 constants in COI:          1 = 100% out of 1
c [blimc] 0.00 ands      in COI:       7883 =  99% out of 7955
c [blimc] 0.01 encoded
c [blimc] 1.32 simplified
c [blimc] 1.32 extracted
c [lglopt]    1.307 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]    1.307 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]        218759 propagations,   167357.4 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 1.3 seconds, 2.5 MB
c [blimc] 1.32 mapped 4775 variables
c [blimc] 1.32 maxk 1000
c [blimc] 1.32 bound 0
c [blimc] 1.33 bound 1
c [blimc] 1.33 bound 2
c [blimc] 1.33 bound 3
c [blimc] 1.35 bound 4
c [blimc] 1.35 bound 5
c [blimc] 1.35 bound 6
c [blimc] 1.36 bound 7
c [blimc] 1.37 bound 8
c [blimc] 1.37 bound 9
c [blimc] 1.38 bound 10
c [blimc] 1.38 bound 11
c [blimc] 1.38 bound 12
c [blimc] 1.39 bound 13
c [blimc] 1.39 bound 14
c [blimc] 1.40 bound 15
c [blimc] 1.43 bound 16
c [blimc] 1.43 bound 17
c [blimc] 1.43 bound 18
c [blimc] 1.44 bound 19
c [blimc] 1.44 bound 20
c [blimc] 1.45 bound 21
c [blimc] 1.45 bound 22
c [blimc] 1.46 bound 23
c [blimc] 1.47 bound 24
c [blimc] 1.48 bound 25
c [blimc] 1.48 bound 26
c [blimc] 1.49 bound 27
c [blimc] 1.51 bound 28
c [blimc] 1.52 bound 29
c [blimc] 1.53 bound 30
c [blimc] 1.54 bound 31
c [blimc] 2.54 bound 32
c [blimc] 2.55 bound 33
c [blimc] 2.56 bound 34
c [blimc] 2.57 bound 35
c [blimc] 2.58 bound 36
c [blimc] 2.59 bound 37
c [blimc] 2.59 bound 38
c [blimc] 2.60 bound 39
c [blimc] 2.62 bound 40
c [blimc] 2.63 bound 41
c [blimc] 2.64 bound 42
c [blimc] 2.65 bound 43
c [blimc] 2.66 bound 44
c [blimc] 2.67 bound 45
c [blimc] 2.69 bound 46
c [blimc] 2.70 bound 47
c [blimc] 2.72 bound 48
c [blimc] 2.73 bound 49
c [blimc] 2.75 bound 50
c [blimc] 2.77 bound 51
c [blimc] 2.78 bound 52
c [blimc] 2.80 bound 53
c [blimc] 2.81 bound 54
c [blimc] 2.83 bound 55
c [blimc] 2.85 bound 56
c [blimc] 2.86 bound 57
c [blimc] 2.88 bound 58
c [blimc] 2.90 bound 59
c [blimc] 2.91 bound 60
c [blimc] 2.93 bound 61
c [blimc] 2.95 bound 62
c [blimc] 2.97 bound 63
[runlim] sample:		10.0 time, 10.3 real, 61.4 MB
c [blimc] 16.90 bound 64
c [blimc] 16.92 bound 65
c [blimc] 16.94 bound 66
c [blimc] 16.96 bound 67
c [blimc] 16.97 bound 68
c [blimc] 16.99 bound 69
c [blimc] 17.00 bound 70
c [blimc] 17.02 bound 71
c [blimc] 17.03 bound 72
c [blimc] 17.05 bound 73
c [blimc] 17.06 bound 74
c [blimc] 17.08 bound 75
c [blimc] 17.10 bound 76
c [blimc] 17.12 bound 77
c [blimc] 17.13 bound 78
c [blimc] 17.16 bound 79
c [blimc] 17.18 bound 80
c [blimc] 17.20 bound 81
c [blimc] 17.22 bound 82
c [blimc] 17.25 bound 83
c [blimc] 17.27 bound 84
c [blimc] 17.29 bound 85
c [blimc] 17.31 bound 86
c [blimc] 17.34 bound 87
c [blimc] 17.36 bound 88
c [blimc] 17.38 bound 89
c [blimc] 17.40 bound 90
c [blimc] 17.43 bound 91
c [blimc] 17.45 bound 92
c [blimc] 17.47 bound 93
c [blimc] 17.50 bound 94
c [blimc] 17.53 bound 95
c [blimc] 17.55 bound 96
c [blimc] 17.58 bound 97
c [blimc] 17.61 bound 98
c [blimc] 17.64 bound 99
c [blimc] 17.66 bound 100
c [blimc] 17.69 bound 101
c [blimc] 17.72 bound 102
c [blimc] 17.74 bound 103
c [blimc] 17.78 bound 104
c [blimc] 17.80 bound 105
c [blimc] 17.83 bound 106
c [blimc] 17.87 bound 107
c [blimc] 17.89 bound 108
c [blimc] 17.92 bound 109
c [blimc] 17.96 bound 110
c [blimc] 17.99 bound 111
c [blimc] 18.02 bound 112
c [blimc] 18.05 bound 113
c [blimc] 18.08 bound 114
c [blimc] 18.11 bound 115
c [blimc] 18.15 bound 116
c [blimc] 18.18 bound 117
c [blimc] 18.21 bound 118
c [blimc] 18.25 bound 119
c [blimc] 18.28 bound 120
c [blimc] 18.31 bound 121
c [blimc] 18.34 bound 122
c [blimc] 18.38 bound 123
c [blimc] 18.41 bound 124
c [blimc] 18.45 bound 125
c [blimc] 18.49 bound 126
c [blimc] 18.53 bound 127
[runlim] sample:		20.0 time, 20.3 real, 167.8 MB
[runlim] sample:		30.0 time, 30.3 real, 174.7 MB
[runlim] sample:		40.0 time, 40.3 real, 174.7 MB
c [blimc] 41.94 bound 128
c [blimc] 41.98 bound 129
c [blimc] 42.02 bound 130
c [blimc] 42.04 bound 131
c [blimc] 42.07 bound 132
c [blimc] 42.10 bound 133
c [blimc] 42.13 bound 134
c [blimc] 42.16 bound 135
c [blimc] 42.19 bound 136
c [blimc] 42.23 bound 137
c [blimc] 42.26 bound 138
c [blimc] 42.29 bound 139
c [blimc] 42.32 bound 140
c [blimc] 42.35 bound 141
c [blimc] 42.38 bound 142
c [blimc] 42.42 bound 143
c [blimc] 42.45 bound 144
c [blimc] 42.48 bound 145
c [blimc] 42.51 bound 146
c [blimc] 42.54 bound 147
c [blimc] 42.57 bound 148
c [blimc] 42.61 bound 149
c [blimc] 42.64 bound 150
c [blimc] 42.67 bound 151
c [blimc] 42.70 bound 152
c [blimc] 42.74 bound 153
c [blimc] 42.77 bound 154
c [blimc] 42.81 bound 155
c [blimc] 42.84 bound 156
c [blimc] 42.88 bound 157
c [blimc] 42.91 bound 158
c [blimc] 42.95 bound 159
c [blimc] 42.99 bound 160
c [blimc] 43.02 bound 161
c [blimc] 43.06 bound 162
c [blimc] 43.09 bound 163
c [blimc] 43.13 bound 164
c [blimc] 43.17 bound 165
c [blimc] 43.21 bound 166
c [blimc] 43.24 bound 167
c [blimc] 43.28 bound 168
c [blimc] 43.32 bound 169
c [blimc] 43.36 bound 170
c [blimc] 43.39 bound 171
c [blimc] 43.43 bound 172
c [blimc] 43.47 bound 173
c [blimc] 43.51 bound 174
c [blimc] 43.55 bound 175
c [blimc] 43.59 bound 176
c [blimc] 43.63 bound 177
c [blimc] 43.67 bound 178
c [blimc] 43.71 bound 179
c [blimc] 43.76 bound 180
c [blimc] 43.81 bound 181
c [blimc] 43.86 bound 182
c [blimc] 43.91 bound 183
c [blimc] 43.95 bound 184
c [blimc] 44.01 bound 185
c [blimc] 44.05 bound 186
c [blimc] 44.10 bound 187
c [blimc] 44.14 bound 188
c [blimc] 44.19 bound 189
c [blimc] 44.23 bound 190
c [blimc] 44.27 bound 191
c [blimc] 44.32 bound 192
c [blimc] 44.36 bound 193
c [blimc] 44.41 bound 194
c [blimc] 44.46 bound 195
c [blimc] 44.51 bound 196
c [blimc] 44.56 bound 197
c [blimc] 44.60 bound 198
c [blimc] 44.65 bound 199
c [blimc] 44.70 bound 200
c [blimc] 44.74 bound 201
c [blimc] 44.79 bound 202
c [blimc] 44.84 bound 203
c [blimc] 44.89 bound 204
c [blimc] 44.93 bound 205
c [blimc] 44.98 bound 206
c [blimc] 45.04 bound 207
c [blimc] 45.11 bound 208
c [blimc] 45.17 bound 209
c [blimc] 45.23 bound 210
c [blimc] 45.28 bound 211
c [blimc] 45.34 bound 212
c [blimc] 45.39 bound 213
c [blimc] 45.45 bound 214
c [blimc] 45.50 bound 215
c [blimc] 45.55 bound 216
c [blimc] 45.60 bound 217
c [blimc] 45.66 bound 218
c [blimc] 45.71 bound 219
c [blimc] 45.77 bound 220
c [blimc] 45.82 bound 221
c [blimc] 45.87 bound 222
c [blimc] 45.92 bound 223
c [blimc] 45.97 bound 224
c [blimc] 46.03 bound 225
c [blimc] 46.08 bound 226
c [blimc] 46.14 bound 227
c [blimc] 46.19 bound 228
c [blimc] 46.24 bound 229
c [blimc] 46.30 bound 230
c [blimc] 46.35 bound 231
c [blimc] 46.42 bound 232
c [blimc] 46.48 bound 233
c [blimc] 46.55 bound 234
c [blimc] 46.61 bound 235
c [blimc] 46.68 bound 236
c [blimc] 46.75 bound 237
c [blimc] 46.82 bound 238
c [blimc] 46.88 bound 239
c [blimc] 46.95 bound 240
c [blimc] 47.01 bound 241
c [blimc] 47.08 bound 242
c [blimc] 47.14 bound 243
c [blimc] 47.21 bound 244
c [blimc] 47.28 bound 245
c [blimc] 47.35 bound 246
c [blimc] 47.41 bound 247
c [blimc] 47.48 bound 248
c [blimc] 47.54 bound 249
c [blimc] 47.60 bound 250
c [blimc] 47.66 bound 251
c [blimc] 47.72 bound 252
c [blimc] 47.78 bound 253
c [blimc] 47.84 bound 254
c [blimc] 47.90 bound 255
[runlim] sample:		49.9 time, 50.3 real, 248.8 MB
[runlim] sample:		59.9 time, 60.3 real, 339.8 MB
c [blimc] 66.12 bound 256
c [blimc] 66.21 bound 257
c [blimc] 66.27 bound 258
c [blimc] 66.34 bound 259
c [blimc] 66.39 bound 260
c [blimc] 66.45 bound 261
c [blimc] 66.50 bound 262
c [blimc] 66.56 bound 263
c [blimc] 66.61 bound 264
c [blimc] 66.67 bound 265
c [blimc] 66.72 bound 266
c [blimc] 66.78 bound 267
c [blimc] 66.83 bound 268
c [blimc] 66.89 bound 269
c [blimc] 66.94 bound 270
c [blimc] 67.00 bound 271
c [blimc] 67.06 bound 272
c [blimc] 67.12 bound 273
c [blimc] 67.19 bound 274
c [blimc] 67.24 bound 275
c [blimc] 67.30 bound 276
c [blimc] 67.36 bound 277
c [blimc] 67.41 bound 278
c [blimc] 67.47 bound 279
c [blimc] 67.53 bound 280
c [blimc] 67.59 bound 281
c [blimc] 67.65 bound 282
c [blimc] 67.70 bound 283
c [blimc] 67.76 bound 284
c [blimc] 67.82 bound 285
c [blimc] 67.88 bound 286
c [blimc] 67.94 bound 287
c [blimc] 68.00 bound 288
c [blimc] 68.06 bound 289
c [blimc] 68.12 bound 290
c [blimc] 68.18 bound 291
c [blimc] 68.24 bound 292
c [blimc] 68.31 bound 293
c [blimc] 68.37 bound 294
c [blimc] 68.43 bound 295
c [blimc] 68.49 bound 296
c [blimc] 68.55 bound 297
c [blimc] 68.62 bound 298
c [blimc] 68.68 bound 299
c [blimc] 68.74 bound 300
c [blimc] 68.81 bound 301
c [blimc] 68.87 bound 302
c [blimc] 68.93 bound 303
c [blimc] 69.00 bound 304
c [blimc] 69.06 bound 305
c [blimc] 69.13 bound 306
c [blimc] 69.19 bound 307
c [blimc] 69.26 bound 308
c [blimc] 69.33 bound 309
c [blimc] 69.41 bound 310
c [blimc] 69.48 bound 311
c [blimc] 69.55 bound 312
c [blimc] 69.62 bound 313
c [blimc] 69.68 bound 314
c [blimc] 69.75 bound 315
c [blimc] 69.82 bound 316
c [blimc] 69.89 bound 317
[runlim] sample:		69.9 time, 70.3 real, 406.7 MB
c [blimc] 69.96 bound 318
c [blimc] 70.02 bound 319
c [blimc] 70.09 bound 320
c [blimc] 70.16 bound 321
c [blimc] 70.23 bound 322
c [blimc] 70.30 bound 323
c [blimc] 70.37 bound 324
c [blimc] 70.44 bound 325
c [blimc] 70.51 bound 326
c [blimc] 70.58 bound 327
c [blimc] 70.65 bound 328
c [blimc] 70.72 bound 329
c [blimc] 70.79 bound 330
c [blimc] 70.87 bound 331
c [blimc] 70.94 bound 332
c [blimc] 71.01 bound 333
c [blimc] 71.08 bound 334
c [blimc] 71.16 bound 335
c [blimc] 71.23 bound 336
c [blimc] 71.30 bound 337
c [blimc] 71.39 bound 338
c [blimc] 71.48 bound 339
c [blimc] 71.56 bound 340
c [blimc] 71.65 bound 341
c [blimc] 71.73 bound 342
c [blimc] 71.82 bound 343
c [blimc] 71.90 bound 344
c [blimc] 71.99 bound 345
c [blimc] 72.07 bound 346
c [blimc] 72.16 bound 347
c [blimc] 72.24 bound 348
c [blimc] 72.33 bound 349
c [blimc] 72.42 bound 350
c [blimc] 72.50 bound 351
c [blimc] 72.58 bound 352
c [blimc] 72.66 bound 353
c [blimc] 72.73 bound 354
c [blimc] 72.81 bound 355
c [blimc] 72.89 bound 356
c [blimc] 72.97 bound 357
c [blimc] 73.05 bound 358
c [blimc] 73.13 bound 359
c [blimc] 73.21 bound 360
c [blimc] 73.29 bound 361
c [blimc] 73.37 bound 362
c [blimc] 73.45 bound 363
c [blimc] 73.53 bound 364
c [blimc] 73.61 bound 365
c [blimc] 73.69 bound 366
c [blimc] 73.77 bound 367
c [blimc] 73.85 bound 368
c [blimc] 73.94 bound 369
c [blimc] 74.02 bound 370
c [blimc] 74.10 bound 371
c [blimc] 74.18 bound 372
c [blimc] 74.26 bound 373
c [blimc] 74.35 bound 374
c [blimc] 74.43 bound 375
c [blimc] 74.51 bound 376
c [blimc] 74.60 bound 377
c [blimc] 74.68 bound 378
c [blimc] 74.77 bound 379
c [blimc] 74.85 bound 380
c [blimc] 74.94 bound 381
c [blimc] 75.02 bound 382
c [blimc] 75.11 bound 383
c [blimc] 75.19 bound 384
c [blimc] 75.28 bound 385
c [blimc] 75.36 bound 386
c [blimc] 75.45 bound 387
c [blimc] 75.54 bound 388
c [blimc] 75.62 bound 389
c [blimc] 75.71 bound 390
c [blimc] 75.80 bound 391
c [blimc] 75.89 bound 392
c [blimc] 75.97 bound 393
c [blimc] 76.06 bound 394
c [blimc] 76.15 bound 395
c [blimc] 76.24 bound 396
c [blimc] 76.33 bound 397
c [blimc] 76.42 bound 398
c [blimc] 76.51 bound 399
c [blimc] 76.60 bound 400
c [blimc] 76.69 bound 401
c [blimc] 76.78 bound 402
c [blimc] 76.87 bound 403
c [blimc] 76.96 bound 404
c [blimc] 77.05 bound 405
c [blimc] 77.15 bound 406
c [blimc] 77.24 bound 407
c [blimc] 77.33 bound 408
c [blimc] 77.42 bound 409
c [blimc] 77.51 bound 410
c [blimc] 77.61 bound 411
c [blimc] 77.71 bound 412
c [blimc] 77.80 bound 413
c [blimc] 77.89 bound 414
c [blimc] 77.99 bound 415
c [blimc] 78.08 bound 416
c [blimc] 78.18 bound 417
c [blimc] 78.27 bound 418
c [blimc] 78.37 bound 419
c [blimc] 78.46 bound 420
c [blimc] 78.56 bound 421
c [blimc] 78.65 bound 422
c [blimc] 78.75 bound 423
c [blimc] 78.85 bound 424
c [blimc] 78.95 bound 425
c [blimc] 79.04 bound 426
c [blimc] 79.14 bound 427
c [blimc] 79.24 bound 428
c [blimc] 79.34 bound 429
c [blimc] 79.44 bound 430
c [blimc] 79.53 bound 431
c [blimc] 79.63 bound 432
c [blimc] 79.73 bound 433
c [blimc] 79.83 bound 434
[runlim] sample:		79.9 time, 80.3 real, 527.5 MB
c [blimc] 79.93 bound 435
c [blimc] 80.03 bound 436
c [blimc] 80.13 bound 437
c [blimc] 80.23 bound 438
c [blimc] 80.33 bound 439
c [blimc] 80.44 bound 440
c [blimc] 80.59 bound 441
c [blimc] 80.69 bound 442
c [blimc] 80.79 bound 443
c [blimc] 80.89 bound 444
c [blimc] 81.00 bound 445
c [blimc] 81.10 bound 446
c [blimc] 81.23 bound 447
c [blimc] 81.34 bound 448
c [blimc] 81.44 bound 449
c [blimc] 81.54 bound 450
c [blimc] 81.64 bound 451
c [blimc] 81.75 bound 452
c [blimc] 81.85 bound 453
c [blimc] 81.95 bound 454
c [blimc] 82.06 bound 455
c [blimc] 82.16 bound 456
c [blimc] 82.26 bound 457
c [blimc] 82.37 bound 458
c [blimc] 82.47 bound 459
c [blimc] 82.58 bound 460
c [blimc] 82.68 bound 461
c [blimc] 82.79 bound 462
c [blimc] 82.89 bound 463
c [blimc] 83.00 bound 464
c [blimc] 83.11 bound 465
c [blimc] 83.21 bound 466
c [blimc] 83.32 bound 467
c [blimc] 83.43 bound 468
c [blimc] 83.53 bound 469
c [blimc] 83.64 bound 470
c [blimc] 83.74 bound 471
c [blimc] 83.85 bound 472
c [blimc] 83.96 bound 473
c [blimc] 84.07 bound 474
c [blimc] 84.18 bound 475
c [blimc] 84.29 bound 476
c [blimc] 84.40 bound 477
c [blimc] 84.51 bound 478
c [blimc] 84.62 bound 479
c [blimc] 84.73 bound 480
c [blimc] 84.84 bound 481
c [blimc] 84.95 bound 482
c [blimc] 85.06 bound 483
c [blimc] 85.17 bound 484
c [blimc] 85.28 bound 485
c [blimc] 85.39 bound 486
c [blimc] 85.50 bound 487
c [blimc] 85.62 bound 488
c [blimc] 85.73 bound 489
c [blimc] 85.84 bound 490
c [blimc] 85.95 bound 491
c [blimc] 86.07 bound 492
c [blimc] 86.18 bound 493
c [blimc] 86.29 bound 494
c [blimc] 86.41 bound 495
c [blimc] 86.52 bound 496
c [blimc] 86.63 bound 497
c [blimc] 86.75 bound 498
c [blimc] 86.86 bound 499
c [blimc] 86.98 bound 500
c [blimc] 87.10 bound 501
c [blimc] 87.21 bound 502
c [blimc] 87.33 bound 503
c [blimc] 87.45 bound 504
c [blimc] 87.56 bound 505
c [blimc] 87.68 bound 506
c [blimc] 87.80 bound 507
c [blimc] 87.92 bound 508
c [blimc] 88.03 bound 509
c [blimc] 88.15 bound 510
c [blimc] 88.27 bound 511
[runlim] sample:		89.9 time, 90.3 real, 536.0 MB
[runlim] sample:		99.8 time, 100.3 real, 588.2 MB
[runlim] sample:		109.8 time, 110.3 real, 421.4 MB
c [blimc] 110.57 bound 512
c [blimc] 110.75 bound 513
c [blimc] 110.86 bound 514
c [blimc] 110.96 bound 515
c [blimc] 111.06 bound 516
c [blimc] 111.16 bound 517
c [blimc] 111.27 bound 518
c [blimc] 111.37 bound 519
c [blimc] 111.48 bound 520
c [blimc] 111.58 bound 521
c [blimc] 111.68 bound 522
c [blimc] 111.79 bound 523
c [blimc] 111.89 bound 524
c [blimc] 112.00 bound 525
c [blimc] 112.10 bound 526
c [blimc] 112.21 bound 527
c [blimc] 112.32 bound 528
c [blimc] 112.42 bound 529
c [blimc] 112.53 bound 530
c [blimc] 112.64 bound 531
c [blimc] 112.75 bound 532
c [blimc] 112.85 bound 533
c [blimc] 112.96 bound 534
c [blimc] 113.07 bound 535
c [blimc] 113.17 bound 536
c [blimc] 113.28 bound 537
c [blimc] 113.40 bound 538
c [blimc] 113.51 bound 539
c [blimc] 113.62 bound 540
c [blimc] 113.73 bound 541
c [blimc] 113.84 bound 542
c [blimc] 113.95 bound 543
c [blimc] 114.06 bound 544
c [blimc] 114.17 bound 545
c [blimc] 114.28 bound 546
c [blimc] 114.39 bound 547
c [blimc] 114.50 bound 548
c [blimc] 114.61 bound 549
c [blimc] 114.72 bound 550
c [blimc] 114.83 bound 551
c [blimc] 114.95 bound 552
c [blimc] 115.06 bound 553
c [blimc] 115.17 bound 554
c [blimc] 115.28 bound 555
c [blimc] 115.40 bound 556
c [blimc] 115.51 bound 557
c [blimc] 115.62 bound 558
c [blimc] 115.74 bound 559
c [blimc] 115.85 bound 560
c [blimc] 115.96 bound 561
c [blimc] 116.08 bound 562
c [blimc] 116.19 bound 563
c [blimc] 116.31 bound 564
c [blimc] 116.42 bound 565
c [blimc] 116.54 bound 566
c [blimc] 116.65 bound 567
c [blimc] 116.77 bound 568
c [blimc] 116.88 bound 569
c [blimc] 117.00 bound 570
c [blimc] 117.12 bound 571
c [blimc] 117.23 bound 572
c [blimc] 117.35 bound 573
c [blimc] 117.47 bound 574
c [blimc] 117.58 bound 575
c [blimc] 117.70 bound 576
c [blimc] 117.82 bound 577
c [blimc] 117.94 bound 578
c [blimc] 118.06 bound 579
c [blimc] 118.18 bound 580
c [blimc] 118.30 bound 581
c [blimc] 118.42 bound 582
c [blimc] 118.54 bound 583
c [blimc] 118.66 bound 584
c [blimc] 118.78 bound 585
c [blimc] 118.90 bound 586
c [blimc] 119.02 bound 587
c [blimc] 119.14 bound 588
c [blimc] 119.26 bound 589
c [blimc] 119.38 bound 590
c [blimc] 119.50 bound 591
c [blimc] 119.62 bound 592
c [blimc] 119.74 bound 593
[runlim] sample:		119.8 time, 120.3 real, 765.5 MB
c [blimc] 119.87 bound 594
c [blimc] 119.99 bound 595
c [blimc] 120.11 bound 596
c [blimc] 120.23 bound 597
c [blimc] 120.35 bound 598
c [blimc] 120.48 bound 599
c [blimc] 120.60 bound 600
c [blimc] 120.73 bound 601
c [blimc] 120.85 bound 602
c [blimc] 120.97 bound 603
c [blimc] 121.10 bound 604
c [blimc] 121.22 bound 605
c [blimc] 121.35 bound 606
c [blimc] 121.47 bound 607
c [blimc] 121.60 bound 608
c [blimc] 121.73 bound 609
c [blimc] 121.85 bound 610
c [blimc] 121.98 bound 611
c [blimc] 122.11 bound 612
c [blimc] 122.23 bound 613
c [blimc] 122.36 bound 614
c [blimc] 122.49 bound 615
c [blimc] 122.62 bound 616
c [blimc] 122.74 bound 617
c [blimc] 122.87 bound 618
c [blimc] 123.00 bound 619
c [blimc] 123.13 bound 620
c [blimc] 123.26 bound 621
c [blimc] 123.38 bound 622
c [blimc] 123.51 bound 623
c [blimc] 123.64 bound 624
c [blimc] 123.77 bound 625
c [blimc] 123.90 bound 626
c [blimc] 124.03 bound 627
c [blimc] 124.17 bound 628
c [blimc] 124.30 bound 629
c [blimc] 124.43 bound 630
c [blimc] 124.56 bound 631
c [blimc] 124.69 bound 632
c [blimc] 124.82 bound 633
c [blimc] 124.95 bound 634
c [blimc] 125.09 bound 635
c [blimc] 125.22 bound 636
c [blimc] 125.35 bound 637
c [blimc] 125.49 bound 638
c [blimc] 125.62 bound 639
c [blimc] 125.76 bound 640
c [blimc] 125.89 bound 641
c [blimc] 126.03 bound 642
c [blimc] 126.16 bound 643
c [blimc] 126.29 bound 644
c [blimc] 126.43 bound 645
c [blimc] 126.56 bound 646
c [blimc] 126.70 bound 647
c [blimc] 126.84 bound 648
c [blimc] 126.97 bound 649
c [blimc] 127.11 bound 650
c [blimc] 127.26 bound 651
c [blimc] 127.40 bound 652
c [blimc] 127.53 bound 653
c [blimc] 127.67 bound 654
c [blimc] 127.81 bound 655
c [blimc] 127.94 bound 656
c [blimc] 128.08 bound 657
c [blimc] 128.22 bound 658
c [blimc] 128.36 bound 659
c [blimc] 128.50 bound 660
c [blimc] 128.64 bound 661
c [blimc] 128.78 bound 662
c [blimc] 128.92 bound 663
c [blimc] 129.06 bound 664
c [blimc] 129.20 bound 665
c [blimc] 129.34 bound 666
c [blimc] 129.48 bound 667
c [blimc] 129.62 bound 668
c [blimc] 129.76 bound 669
[runlim] sample:		129.8 time, 130.3 real, 759.5 MB
c [blimc] 129.90 bound 670
c [blimc] 130.04 bound 671
c [blimc] 130.18 bound 672
c [blimc] 130.32 bound 673
c [blimc] 130.47 bound 674
c [blimc] 130.61 bound 675
c [blimc] 130.75 bound 676
c [blimc] 130.89 bound 677
c [blimc] 131.03 bound 678
c [blimc] 131.18 bound 679
c [blimc] 131.32 bound 680
c [blimc] 131.47 bound 681
c [blimc] 131.61 bound 682
c [blimc] 131.75 bound 683
c [blimc] 131.90 bound 684
c [blimc] 132.04 bound 685
c [blimc] 132.19 bound 686
c [blimc] 132.33 bound 687
c [blimc] 132.48 bound 688
c [blimc] 132.62 bound 689
c [blimc] 132.77 bound 690
c [blimc] 132.91 bound 691
c [blimc] 133.06 bound 692
c [blimc] 133.21 bound 693
c [blimc] 133.36 bound 694
c [blimc] 133.50 bound 695
c [blimc] 133.65 bound 696
c [blimc] 133.80 bound 697
c [blimc] 133.95 bound 698
c [blimc] 134.09 bound 699
c [blimc] 134.24 bound 700
c [blimc] 134.39 bound 701
c [blimc] 134.54 bound 702
c [blimc] 134.69 bound 703
c [blimc] 134.84 bound 704
c [blimc] 134.99 bound 705
c [blimc] 135.14 bound 706
c [blimc] 135.29 bound 707
c [blimc] 135.44 bound 708
c [blimc] 135.59 bound 709
c [blimc] 135.74 bound 710
c [blimc] 135.89 bound 711
c [blimc] 136.04 bound 712
c [blimc] 136.20 bound 713
c [blimc] 136.35 bound 714
c [blimc] 136.50 bound 715
c [blimc] 136.65 bound 716
c [blimc] 136.80 bound 717
c [blimc] 136.96 bound 718
c [blimc] 137.11 bound 719
c [blimc] 137.27 bound 720
c [blimc] 137.42 bound 721
c [blimc] 137.57 bound 722
c [blimc] 137.73 bound 723
c [blimc] 137.88 bound 724
c [blimc] 138.04 bound 725
c [blimc] 138.19 bound 726
c [blimc] 138.34 bound 727
c [blimc] 138.50 bound 728
c [blimc] 138.65 bound 729
c [blimc] 138.81 bound 730
c [blimc] 138.97 bound 731
c [blimc] 139.12 bound 732
c [blimc] 139.28 bound 733
c [blimc] 139.44 bound 734
c [blimc] 139.60 bound 735
c [blimc] 139.75 bound 736
[runlim] sample:		139.8 time, 140.3 real, 741.2 MB
c [blimc] 139.91 bound 737
c [blimc] 140.07 bound 738
c [blimc] 140.23 bound 739
c [blimc] 140.39 bound 740
c [blimc] 140.55 bound 741
c [blimc] 140.71 bound 742
c [blimc] 140.87 bound 743
c [blimc] 141.03 bound 744
c [blimc] 141.20 bound 745
c [blimc] 141.36 bound 746
c [blimc] 141.52 bound 747
c [blimc] 141.68 bound 748
c [blimc] 141.85 bound 749
c [blimc] 142.01 bound 750
c [blimc] 142.17 bound 751
c [blimc] 142.33 bound 752
c [blimc] 142.50 bound 753
c [blimc] 142.66 bound 754
c [blimc] 142.82 bound 755
c [blimc] 142.99 bound 756
c [blimc] 143.15 bound 757
c [blimc] 143.32 bound 758
c [blimc] 143.48 bound 759
c [blimc] 143.64 bound 760
c [blimc] 143.81 bound 761
c [blimc] 143.97 bound 762
c [blimc] 144.14 bound 763
c [blimc] 144.30 bound 764
c [blimc] 144.47 bound 765
c [blimc] 144.64 bound 766
c [blimc] 144.80 bound 767
c [blimc] 144.97 bound 768
c [blimc] 145.13 bound 769
c [blimc] 145.30 bound 770
c [blimc] 145.47 bound 771
c [blimc] 145.64 bound 772
c [blimc] 145.80 bound 773
c [blimc] 145.97 bound 774
c [blimc] 146.14 bound 775
c [blimc] 146.31 bound 776
c [blimc] 146.48 bound 777
c [blimc] 146.65 bound 778
c [blimc] 146.81 bound 779
c [blimc] 146.98 bound 780
c [blimc] 147.16 bound 781
c [blimc] 147.33 bound 782
c [blimc] 147.49 bound 783
c [blimc] 147.66 bound 784
c [blimc] 147.83 bound 785
c [blimc] 148.00 bound 786
c [blimc] 148.18 bound 787
c [blimc] 148.35 bound 788
c [blimc] 148.52 bound 789
c [blimc] 148.69 bound 790
c [blimc] 148.87 bound 791
c [blimc] 149.04 bound 792
c [blimc] 149.22 bound 793
c [blimc] 149.40 bound 794
c [blimc] 149.57 bound 795
c [blimc] 149.74 bound 796
[runlim] sample:		149.8 time, 150.3 real, 676.9 MB
c [blimc] 149.92 bound 797
c [blimc] 150.09 bound 798
c [blimc] 150.27 bound 799
c [blimc] 150.44 bound 800
c [blimc] 150.61 bound 801
c [blimc] 150.79 bound 802
c [blimc] 150.96 bound 803
c [blimc] 151.14 bound 804
c [blimc] 151.32 bound 805
c [blimc] 151.50 bound 806
c [blimc] 151.67 bound 807
c [blimc] 151.85 bound 808
c [blimc] 152.03 bound 809
c [blimc] 152.20 bound 810
c [blimc] 152.38 bound 811
c [blimc] 152.55 bound 812
c [blimc] 152.73 bound 813
c [blimc] 152.91 bound 814
c [blimc] 153.08 bound 815
c [blimc] 153.26 bound 816
c [blimc] 153.44 bound 817
c [blimc] 153.62 bound 818
c [blimc] 153.80 bound 819
c [blimc] 153.98 bound 820
c [blimc] 154.16 bound 821
c [blimc] 154.34 bound 822
c [blimc] 154.52 bound 823
c [blimc] 154.70 bound 824
c [blimc] 154.88 bound 825
c [blimc] 155.06 bound 826
c [blimc] 155.24 bound 827
c [blimc] 155.42 bound 828
c [blimc] 155.60 bound 829
c [blimc] 155.79 bound 830
c [blimc] 155.97 bound 831
c [blimc] 156.15 bound 832
c [blimc] 156.33 bound 833
c [blimc] 156.51 bound 834
c [blimc] 156.70 bound 835
c [blimc] 156.88 bound 836
c [blimc] 157.06 bound 837
c [blimc] 157.25 bound 838
c [blimc] 157.43 bound 839
c [blimc] 157.61 bound 840
c [blimc] 157.80 bound 841
c [blimc] 157.98 bound 842
c [blimc] 158.17 bound 843
c [blimc] 158.36 bound 844
c [blimc] 158.54 bound 845
c [blimc] 158.73 bound 846
c [blimc] 158.91 bound 847
c [blimc] 159.10 bound 848
c [blimc] 159.29 bound 849
c [blimc] 159.47 bound 850
c [blimc] 159.66 bound 851
[runlim] sample:		159.7 time, 160.3 real, 887.4 MB
c [blimc] 159.84 bound 852
c [blimc] 160.03 bound 853
c [blimc] 160.22 bound 854
c [blimc] 160.40 bound 855
c [blimc] 160.59 bound 856
c [blimc] 160.78 bound 857
c [blimc] 160.97 bound 858
c [blimc] 161.16 bound 859
c [blimc] 161.35 bound 860
c [blimc] 161.54 bound 861
c [blimc] 161.73 bound 862
c [blimc] 161.92 bound 863
c [blimc] 162.11 bound 864
c [blimc] 162.30 bound 865
c [blimc] 162.49 bound 866
c [blimc] 162.68 bound 867
c [blimc] 162.87 bound 868
c [blimc] 163.06 bound 869
c [blimc] 163.25 bound 870
c [blimc] 163.44 bound 871
c [blimc] 163.63 bound 872
c [blimc] 163.82 bound 873
c [blimc] 164.02 bound 874
c [blimc] 164.21 bound 875
c [blimc] 164.40 bound 876
c [blimc] 164.59 bound 877
c [blimc] 164.78 bound 878
c [blimc] 165.00 bound 879
c [blimc] 165.19 bound 880
c [blimc] 165.38 bound 881
c [blimc] 165.58 bound 882
c [blimc] 165.77 bound 883
c [blimc] 165.97 bound 884
c [blimc] 166.16 bound 885
c [blimc] 166.36 bound 886
c [blimc] 166.56 bound 887
c [blimc] 166.75 bound 888
c [blimc] 166.95 bound 889
c [blimc] 167.15 bound 890
c [blimc] 167.34 bound 891
c [blimc] 167.54 bound 892
c [blimc] 167.74 bound 893
c [blimc] 167.93 bound 894
c [blimc] 168.13 bound 895
c [blimc] 168.33 bound 896
c [blimc] 168.53 bound 897
c [blimc] 168.73 bound 898
c [blimc] 168.93 bound 899
c [blimc] 169.12 bound 900
c [blimc] 169.32 bound 901
c [blimc] 169.52 bound 902
c [blimc] 169.72 bound 903
[runlim] sample:		169.7 time, 170.3 real, 768.3 MB
c [blimc] 169.92 bound 904
c [blimc] 170.12 bound 905
c [blimc] 170.32 bound 906
c [blimc] 170.52 bound 907
c [blimc] 170.72 bound 908
c [blimc] 170.92 bound 909
c [blimc] 171.12 bound 910
c [blimc] 171.33 bound 911
c [blimc] 171.54 bound 912
c [blimc] 171.74 bound 913
c [blimc] 171.94 bound 914
c [blimc] 172.24 bound 915
c [blimc] 172.44 bound 916
c [blimc] 172.64 bound 917
c [blimc] 172.85 bound 918
c [blimc] 173.05 bound 919
c [blimc] 173.25 bound 920
c [blimc] 173.45 bound 921
c [blimc] 173.66 bound 922
c [blimc] 173.86 bound 923
c [blimc] 174.06 bound 924
c [blimc] 174.27 bound 925
c [blimc] 174.47 bound 926
c [blimc] 174.68 bound 927
c [blimc] 174.88 bound 928
c [blimc] 175.09 bound 929
c [blimc] 175.30 bound 930
c [blimc] 175.50 bound 931
c [blimc] 175.71 bound 932
c [blimc] 175.92 bound 933
c [blimc] 176.12 bound 934
c [blimc] 176.33 bound 935
c [blimc] 176.54 bound 936
c [blimc] 176.75 bound 937
c [blimc] 176.95 bound 938
c [blimc] 177.16 bound 939
c [blimc] 177.37 bound 940
c [blimc] 177.58 bound 941
c [blimc] 177.79 bound 942
c [blimc] 178.00 bound 943
c [blimc] 178.21 bound 944
c [blimc] 178.42 bound 945
c [blimc] 178.63 bound 946
c [blimc] 178.84 bound 947
c [blimc] 179.05 bound 948
c [blimc] 179.26 bound 949
c [blimc] 179.47 bound 950
c [blimc] 179.68 bound 951
[runlim] sample:		179.7 time, 180.3 real, 1051.3 MB
c [blimc] 179.89 bound 952
c [blimc] 180.10 bound 953
c [blimc] 180.31 bound 954
c [blimc] 180.53 bound 955
c [blimc] 180.74 bound 956
c [blimc] 180.95 bound 957
c [blimc] 181.16 bound 958
c [blimc] 181.38 bound 959
c [blimc] 181.59 bound 960
c [blimc] 181.80 bound 961
c [blimc] 182.01 bound 962
c [blimc] 182.23 bound 963
c [blimc] 182.44 bound 964
c [blimc] 182.66 bound 965
c [blimc] 182.87 bound 966
c [blimc] 183.09 bound 967
c [blimc] 183.31 bound 968
c [blimc] 183.53 bound 969
c [blimc] 183.75 bound 970
c [blimc] 183.96 bound 971
c [blimc] 184.18 bound 972
c [blimc] 184.40 bound 973
c [blimc] 184.61 bound 974
c [blimc] 184.83 bound 975
c [blimc] 185.05 bound 976
c [blimc] 185.27 bound 977
c [blimc] 185.49 bound 978
c [blimc] 185.71 bound 979
c [blimc] 185.93 bound 980
c [blimc] 186.15 bound 981
c [blimc] 186.37 bound 982
c [blimc] 186.59 bound 983
c [blimc] 186.81 bound 984
c [blimc] 187.03 bound 985
c [blimc] 187.25 bound 986
c [blimc] 187.47 bound 987
c [blimc] 187.69 bound 988
c [blimc] 187.92 bound 989
c [blimc] 188.14 bound 990
c [blimc] 188.36 bound 991
c [blimc] 188.58 bound 992
c [blimc] 188.80 bound 993
c [blimc] 189.02 bound 994
c [blimc] 189.25 bound 995
c [blimc] 189.47 bound 996
[runlim] sample:		189.7 time, 190.3 real, 1392.5 MB
c [blimc] 189.70 bound 997
c [blimc] 189.92 bound 998
c [blimc] 190.14 bound 999
c [blimc] 190.37 bound 1000
c [lgl1000]   78.653  68% simplifying
c [lgl1000]    0.000   0% search
c [lgl1000] ==================================
c [lgl1000]  115.697 100% all
c [lgl1000] 
c [lgl1000]             0 conflicts,           0.0 confs/sec
c [lgl1000]             0 ternaries,           0.0 confs/ternary
c [lgl1000]             0 binaries,            0.0 confs/binary
c [lgl1000]             0 iterations,          0.0 confs/iteration
c [lgl1000] 
c [lgl1000]             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c [lgl1000]             0 restarts,            0.0 rests/sec,      0.0 confs/restart
c [lgl1000]             0 decisions,           0.0 decis/sec,      0.0 decis/conflict
c [lgl1000]       1657814 propagations,    14328.9 props/sec,      0.0 props/decision
c [lgl1000] 
c [lgl1000] 115.7 seconds, 1354.2 MB
c [blimc] 190.59 reached k = 1001
c [blimc] 190.59 cloned 0 solvers
c [blimc] 190.59 max 1354.6 MB
c [blimc] 190.64 exit 20
[runlim] end:			Sun Sep 20 05:04:13 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			191.35 seconds
[runlim] time:			190.63 seconds
[runlim] space:			1396.0 MB
[runlim] samples:		1910
