[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/6s355rb11080.aig
[runlim] start:			Mon Sep 21 02:26:02 2015
[runlim] main pid:		11665
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/6s355rb11080.aig
c [blimc] 0.03 MILOA 179445 55 15091 1 164299
c [blimc] 0.03 BCJK 0 0 0 0 164299
c [blimc] 0.03 15091 latches initialized to 0
c [blimc] 0.03 0 latches initialized to 1
c [blimc] 0.03 0 latches uninitialized
c [blimc] 0.03 literals  in COI:      77444 =  43% out of 179445
c [blimc] 0.03 inputs    in COI:         55 = 100% out of 55
c [blimc] 0.03 latches   in COI:      13467 =  89% out of 15091
c [blimc] 0.03 constants in COI:          1 = 100% out of 1
c [blimc] 0.03 ands      in COI:      63921 =  39% out of 164299
c [blimc] 0.10 encoded
c [blimc] 7.60 simplified
c [blimc] 7.63 extracted
c [lglopt]    7.504 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]    7.507 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]        121957 propagations,    16246.6 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 7.5 seconds, 22.9 MB
c [blimc] 7.63 mapped 42978 variables
c [blimc] 7.63 maxk 1000
c [blimc] 7.63 bound 0
c [blimc] 7.68 bound 1
c [blimc] 7.73 bound 2
c [blimc] 7.75 bound 3
c [blimc] 7.82 bound 4
c [blimc] 7.85 bound 5
c [blimc] 7.88 bound 6
c [blimc] 7.91 bound 7
c [blimc] 8.02 bound 8
c [blimc] 8.05 bound 9
c [blimc] 8.08 bound 10
c [blimc] 8.12 bound 11
c [blimc] 8.16 bound 12
c [blimc] 8.20 bound 13
c [blimc] 8.24 bound 14
c [blimc] 8.29 bound 15
c [blimc] 8.51 bound 16
c [blimc] 8.54 bound 17
c [blimc] 8.58 bound 18
c [blimc] 8.61 bound 19
c [blimc] 8.66 bound 20
c [blimc] 8.70 bound 21
c [blimc] 8.75 bound 22
c [blimc] 8.80 bound 23
c [blimc] 8.86 bound 24
c [blimc] 8.91 bound 25
c [blimc] 8.97 bound 26
c [blimc] 9.04 bound 27
c [blimc] 9.10 bound 28
c [blimc] 9.16 bound 29
c [blimc] 9.23 bound 30
c [blimc] 9.30 bound 31
c [blimc] 9.70 bound 32
c [blimc] 9.74 bound 33
c [blimc] 9.79 bound 34
c [blimc] 9.84 bound 35
c [blimc] 9.89 bound 36
[runlim] sample:		9.9 time, 10.3 real, 198.3 MB
c [blimc] 9.94 bound 37
c [blimc] 10.00 bound 38
c [blimc] 10.06 bound 39
c [blimc] 10.12 bound 40
c [blimc] 10.18 bound 41
c [blimc] 10.25 bound 42
c [blimc] 10.31 bound 43
c [blimc] 10.39 bound 44
c [blimc] 10.46 bound 45
c [blimc] 10.54 bound 46
c [blimc] 10.61 bound 47
c [blimc] 10.68 bound 48
c [blimc] 10.77 bound 49
c [blimc] 10.86 bound 50
c [blimc] 10.95 bound 51
c [blimc] 11.04 bound 52
c [blimc] 11.13 bound 53
c [blimc] 11.24 bound 54
c [blimc] 11.33 bound 55
c [blimc] 11.44 bound 56
c [blimc] 11.55 bound 57
c [blimc] 11.65 bound 58
c [blimc] 11.75 bound 59
c [blimc] 11.85 bound 60
c [blimc] 11.95 bound 61
c [blimc] 12.05 bound 62
c [blimc] 12.16 bound 63
c [blimc] 12.90 bound 64
c [blimc] 12.96 bound 65
c [blimc] 13.03 bound 66
c [blimc] 13.10 bound 67
c [blimc] 13.17 bound 68
c [blimc] 13.24 bound 69
c [blimc] 13.32 bound 70
c [blimc] 13.40 bound 71
c [blimc] 13.48 bound 72
c [blimc] 13.56 bound 73
c [blimc] 13.65 bound 74
c [blimc] 13.74 bound 75
c [blimc] 13.84 bound 76
c [blimc] 13.93 bound 77
c [blimc] 14.03 bound 78
c [blimc] 14.13 bound 79
c [blimc] 14.24 bound 80
c [blimc] 14.34 bound 81
c [blimc] 14.45 bound 82
c [blimc] 14.56 bound 83
c [blimc] 14.68 bound 84
c [blimc] 14.79 bound 85
c [blimc] 14.91 bound 86
c [blimc] 15.03 bound 87
c [blimc] 15.16 bound 88
c [blimc] 15.29 bound 89
c [blimc] 15.43 bound 90
c [blimc] 15.55 bound 91
c [blimc] 15.68 bound 92
c [blimc] 15.81 bound 93
c [blimc] 15.95 bound 94
c [blimc] 16.07 bound 95
c [blimc] 16.20 bound 96
c [blimc] 16.34 bound 97
c [blimc] 16.49 bound 98
c [blimc] 16.62 bound 99
c [blimc] 16.75 bound 100
c [blimc] 16.88 bound 101
c [blimc] 17.02 bound 102
c [blimc] 17.15 bound 103
c [blimc] 17.30 bound 104
c [blimc] 17.43 bound 105
c [blimc] 17.60 bound 106
c [blimc] 17.74 bound 107
c [blimc] 17.89 bound 108
c [blimc] 18.03 bound 109
c [blimc] 18.20 bound 110
c [blimc] 18.35 bound 111
c [blimc] 18.51 bound 112
c [blimc] 18.66 bound 113
c [blimc] 18.82 bound 114
c [blimc] 18.98 bound 115
c [blimc] 19.14 bound 116
c [blimc] 19.30 bound 117
c [blimc] 19.46 bound 118
c [blimc] 19.63 bound 119
c [blimc] 19.80 bound 120
[runlim] sample:		19.9 time, 20.3 real, 606.7 MB
c [blimc] 19.96 bound 121
c [blimc] 20.13 bound 122
c [blimc] 20.31 bound 123
c [blimc] 20.48 bound 124
c [blimc] 20.66 bound 125
c [blimc] 20.84 bound 126
c [blimc] 21.04 bound 127
c [blimc] 22.78 bound 128
c [blimc] 22.88 bound 129
c [blimc] 22.99 bound 130
c [blimc] 23.09 bound 131
c [blimc] 23.21 bound 132
c [blimc] 23.32 bound 133
c [blimc] 23.44 bound 134
c [blimc] 23.56 bound 135
c [blimc] 23.68 bound 136
c [blimc] 23.80 bound 137
c [blimc] 23.94 bound 138
c [blimc] 24.07 bound 139
c [blimc] 24.20 bound 140
c [blimc] 24.34 bound 141
c [blimc] 24.47 bound 142
c [blimc] 24.61 bound 143
c [blimc] 24.75 bound 144
c [blimc] 24.89 bound 145
c [blimc] 25.04 bound 146
c [blimc] 25.19 bound 147
c [blimc] 25.35 bound 148
c [blimc] 25.51 bound 149
c [blimc] 25.67 bound 150
c [blimc] 25.84 bound 151
c [blimc] 26.00 bound 152
c [blimc] 26.16 bound 153
c [blimc] 26.33 bound 154
c [blimc] 26.51 bound 155
c [blimc] 26.67 bound 156
c [blimc] 26.83 bound 157
c [blimc] 26.99 bound 158
c [blimc] 27.15 bound 159
c [blimc] 27.31 bound 160
c [blimc] 27.47 bound 161
c [blimc] 27.64 bound 162
c [blimc] 27.81 bound 163
c [blimc] 27.98 bound 164
c [blimc] 28.15 bound 165
c [blimc] 28.32 bound 166
c [blimc] 28.50 bound 167
c [blimc] 28.68 bound 168
c [blimc] 28.86 bound 169
c [blimc] 29.05 bound 170
c [blimc] 29.23 bound 171
c [blimc] 29.42 bound 172
c [blimc] 29.60 bound 173
c [blimc] 29.81 bound 174
[runlim] sample:		29.9 time, 30.3 real, 569.5 MB
c [blimc] 30.00 bound 175
c [blimc] 30.20 bound 176
c [blimc] 30.39 bound 177
c [blimc] 30.59 bound 178
c [blimc] 30.78 bound 179
c [blimc] 30.99 bound 180
c [blimc] 31.20 bound 181
c [blimc] 31.40 bound 182
c [blimc] 31.61 bound 183
c [blimc] 31.82 bound 184
c [blimc] 32.02 bound 185
c [blimc] 32.23 bound 186
c [blimc] 32.44 bound 187
c [blimc] 32.66 bound 188
c [blimc] 32.87 bound 189
c [blimc] 33.09 bound 190
c [blimc] 33.31 bound 191
c [blimc] 33.54 bound 192
c [blimc] 33.76 bound 193
c [blimc] 33.99 bound 194
c [blimc] 34.21 bound 195
c [blimc] 34.47 bound 196
c [blimc] 34.70 bound 197
c [blimc] 34.94 bound 198
c [blimc] 35.17 bound 199
c [blimc] 35.41 bound 200
c [blimc] 35.65 bound 201
c [blimc] 35.89 bound 202
c [blimc] 36.13 bound 203
c [blimc] 36.37 bound 204
c [blimc] 36.62 bound 205
c [blimc] 36.87 bound 206
c [blimc] 37.12 bound 207
c [blimc] 37.39 bound 208
c [blimc] 37.64 bound 209
c [blimc] 37.90 bound 210
c [blimc] 38.15 bound 211
c [blimc] 38.41 bound 212
c [blimc] 38.67 bound 213
c [blimc] 38.93 bound 214
c [blimc] 39.19 bound 215
c [blimc] 39.46 bound 216
c [blimc] 39.72 bound 217
[runlim] sample:		39.8 time, 40.3 real, 733.8 MB
c [blimc] 39.99 bound 218
c [blimc] 40.26 bound 219
c [blimc] 40.54 bound 220
c [blimc] 40.81 bound 221
c [blimc] 41.09 bound 222
c [blimc] 41.37 bound 223
c [blimc] 41.64 bound 224
c [blimc] 41.92 bound 225
c [blimc] 42.21 bound 226
c [blimc] 42.49 bound 227
c [blimc] 42.78 bound 228
c [blimc] 43.07 bound 229
c [blimc] 43.36 bound 230
c [blimc] 43.65 bound 231
c [blimc] 43.95 bound 232
c [blimc] 44.24 bound 233
c [blimc] 44.54 bound 234
c [blimc] 44.84 bound 235
c [blimc] 45.14 bound 236
c [blimc] 45.45 bound 237
c [blimc] 45.75 bound 238
c [blimc] 46.07 bound 239
c [blimc] 46.38 bound 240
c [blimc] 46.69 bound 241
c [blimc] 47.00 bound 242
c [blimc] 47.31 bound 243
c [blimc] 47.63 bound 244
c [blimc] 47.95 bound 245
c [blimc] 48.27 bound 246
c [blimc] 48.59 bound 247
c [blimc] 48.91 bound 248
c [blimc] 49.24 bound 249
c [blimc] 49.57 bound 250
[runlim] sample:		49.8 time, 50.3 real, 1148.2 MB
c [blimc] 49.89 bound 251
c [blimc] 50.22 bound 252
c [blimc] 50.56 bound 253
c [blimc] 50.89 bound 254
c [blimc] 51.25 bound 255
c [blimc] 54.98 bound 256
c [blimc] 55.16 bound 257
c [blimc] 55.35 bound 258
c [blimc] 55.54 bound 259
c [blimc] 55.74 bound 260
c [blimc] 55.93 bound 261
c [blimc] 56.13 bound 262
c [blimc] 56.33 bound 263
c [blimc] 56.54 bound 264
c [blimc] 56.74 bound 265
c [blimc] 56.95 bound 266
c [blimc] 57.16 bound 267
c [blimc] 57.38 bound 268
c [blimc] 57.59 bound 269
c [blimc] 57.81 bound 270
c [blimc] 58.03 bound 271
c [blimc] 58.26 bound 272
c [blimc] 58.49 bound 273
c [blimc] 58.72 bound 274
c [blimc] 58.95 bound 275
c [blimc] 59.19 bound 276
c [blimc] 59.42 bound 277
c [blimc] 59.66 bound 278
[runlim] sample:		59.7 time, 60.3 real, 552.8 MB
c [blimc] 59.89 bound 279
c [blimc] 60.13 bound 280
c [blimc] 60.37 bound 281
c [blimc] 60.61 bound 282
c [blimc] 60.84 bound 283
c [blimc] 61.08 bound 284
c [blimc] 61.32 bound 285
c [blimc] 61.56 bound 286
c [blimc] 61.80 bound 287
c [blimc] 62.07 bound 288
c [blimc] 62.33 bound 289
c [blimc] 62.61 bound 290
c [blimc] 62.86 bound 291
c [blimc] 63.11 bound 292
c [blimc] 63.36 bound 293
c [blimc] 63.62 bound 294
c [blimc] 63.87 bound 295
c [blimc] 64.13 bound 296
c [blimc] 64.39 bound 297
c [blimc] 64.65 bound 298
c [blimc] 64.91 bound 299
c [blimc] 65.18 bound 300
c [blimc] 65.44 bound 301
c [blimc] 65.71 bound 302
c [blimc] 65.98 bound 303
c [blimc] 66.26 bound 304
c [blimc] 66.53 bound 305
c [blimc] 66.82 bound 306
c [blimc] 67.10 bound 307
c [blimc] 67.38 bound 308
c [blimc] 67.66 bound 309
c [blimc] 67.94 bound 310
c [blimc] 68.23 bound 311
c [blimc] 68.52 bound 312
c [blimc] 68.80 bound 313
c [blimc] 69.09 bound 314
c [blimc] 69.38 bound 315
c [blimc] 69.68 bound 316
[runlim] sample:		69.7 time, 70.3 real, 691.6 MB
c [blimc] 69.97 bound 317
c [blimc] 70.27 bound 318
c [blimc] 70.57 bound 319
c [blimc] 70.88 bound 320
c [blimc] 71.18 bound 321
c [blimc] 71.49 bound 322
c [blimc] 71.79 bound 323
c [blimc] 72.11 bound 324
c [blimc] 72.42 bound 325
c [blimc] 72.74 bound 326
c [blimc] 73.05 bound 327
c [blimc] 73.37 bound 328
c [blimc] 73.68 bound 329
c [blimc] 74.01 bound 330
c [blimc] 74.33 bound 331
c [blimc] 74.65 bound 332
c [blimc] 74.97 bound 333
c [blimc] 75.31 bound 334
c [blimc] 75.65 bound 335
c [blimc] 75.98 bound 336
c [blimc] 76.31 bound 337
c [blimc] 76.65 bound 338
c [blimc] 76.98 bound 339
c [blimc] 77.32 bound 340
c [blimc] 77.65 bound 341
c [blimc] 78.00 bound 342
c [blimc] 78.34 bound 343
c [blimc] 78.68 bound 344
c [blimc] 79.03 bound 345
c [blimc] 79.38 bound 346
[runlim] sample:		79.7 time, 80.3 real, 1045.7 MB
c [blimc] 79.73 bound 347
c [blimc] 80.08 bound 348
c [blimc] 80.43 bound 349
c [blimc] 80.80 bound 350
c [blimc] 81.16 bound 351
c [blimc] 81.52 bound 352
c [blimc] 81.88 bound 353
c [blimc] 82.25 bound 354
c [blimc] 82.61 bound 355
c [blimc] 82.98 bound 356
c [blimc] 83.34 bound 357
c [blimc] 83.72 bound 358
c [blimc] 84.09 bound 359
c [blimc] 84.46 bound 360
c [blimc] 84.84 bound 361
c [blimc] 85.22 bound 362
c [blimc] 85.60 bound 363
c [blimc] 85.99 bound 364
c [blimc] 86.37 bound 365
c [blimc] 86.75 bound 366
c [blimc] 87.14 bound 367
c [blimc] 87.53 bound 368
c [blimc] 87.92 bound 369
c [blimc] 88.32 bound 370
c [blimc] 88.71 bound 371
c [blimc] 89.10 bound 372
c [blimc] 89.50 bound 373
[runlim] sample:		89.7 time, 90.3 real, 1218.1 MB
c [blimc] 89.90 bound 374
c [blimc] 90.30 bound 375
c [blimc] 90.71 bound 376
c [blimc] 91.11 bound 377
c [blimc] 91.52 bound 378
c [blimc] 91.93 bound 379
c [blimc] 92.34 bound 380
c [blimc] 92.75 bound 381
c [blimc] 93.17 bound 382
c [blimc] 93.58 bound 383
c [blimc] 94.01 bound 384
c [blimc] 94.44 bound 385
c [blimc] 94.87 bound 386
c [blimc] 95.29 bound 387
c [blimc] 95.71 bound 388
c [blimc] 96.14 bound 389
c [blimc] 96.57 bound 390
c [blimc] 97.09 bound 391
c [blimc] 97.52 bound 392
c [blimc] 97.96 bound 393
c [blimc] 98.40 bound 394
c [blimc] 98.83 bound 395
c [blimc] 99.28 bound 396
[runlim] sample:		99.7 time, 100.3 real, 1584.4 MB
c [blimc] 99.72 bound 397
c [blimc] 100.16 bound 398
c [blimc] 100.61 bound 399
c [blimc] 101.06 bound 400
c [blimc] 101.50 bound 401
c [blimc] 101.96 bound 402
c [blimc] 102.41 bound 403
c [blimc] 102.87 bound 404
c [blimc] 103.32 bound 405
c [blimc] 103.79 bound 406
c [blimc] 104.24 bound 407
c [blimc] 104.71 bound 408
c [blimc] 105.17 bound 409
c [blimc] 105.64 bound 410
c [blimc] 106.11 bound 411
c [blimc] 106.58 bound 412
c [blimc] 107.05 bound 413
c [blimc] 107.53 bound 414
c [blimc] 108.00 bound 415
c [blimc] 108.48 bound 416
c [blimc] 108.96 bound 417
c [blimc] 109.44 bound 418
[runlim] sample:		109.7 time, 110.3 real, 1618.8 MB
c [blimc] 109.92 bound 419
c [blimc] 110.41 bound 420
c [blimc] 110.89 bound 421
c [blimc] 111.39 bound 422
c [blimc] 111.87 bound 423
c [blimc] 112.37 bound 424
c [blimc] 112.86 bound 425
c [blimc] 113.36 bound 426
c [blimc] 113.86 bound 427
c [blimc] 114.36 bound 428
c [blimc] 114.86 bound 429
c [blimc] 115.37 bound 430
c [blimc] 115.87 bound 431
c [blimc] 116.38 bound 432
c [blimc] 116.90 bound 433
c [blimc] 117.41 bound 434
c [blimc] 117.93 bound 435
c [blimc] 118.45 bound 436
c [blimc] 118.96 bound 437
c [blimc] 119.49 bound 438
[runlim] sample:		119.6 time, 120.3 real, 1436.8 MB
c [blimc] 120.03 bound 439
c [blimc] 120.55 bound 440
c [blimc] 121.08 bound 441
c [blimc] 121.61 bound 442
c [blimc] 122.13 bound 443
c [blimc] 122.67 bound 444
c [blimc] 123.20 bound 445
c [blimc] 123.74 bound 446
c [blimc] 124.27 bound 447
c [blimc] 124.81 bound 448
c [blimc] 125.35 bound 449
c [blimc] 125.90 bound 450
c [blimc] 126.44 bound 451
c [blimc] 126.99 bound 452
c [blimc] 127.53 bound 453
c [blimc] 128.09 bound 454
c [blimc] 128.64 bound 455
c [blimc] 129.20 bound 456
[runlim] sample:		129.6 time, 130.3 real, 1982.3 MB
c [blimc] 129.75 bound 457
c [blimc] 130.31 bound 458
c [blimc] 130.86 bound 459
c [blimc] 131.42 bound 460
c [blimc] 131.98 bound 461
c [blimc] 132.55 bound 462
c [blimc] 133.11 bound 463
c [blimc] 133.68 bound 464
c [blimc] 134.24 bound 465
c [blimc] 134.81 bound 466
c [blimc] 135.38 bound 467
c [blimc] 135.96 bound 468
c [blimc] 136.54 bound 469
c [blimc] 137.12 bound 470
c [blimc] 137.70 bound 471
c [blimc] 138.29 bound 472
c [blimc] 138.87 bound 473
c [blimc] 139.46 bound 474
[runlim] sample:		139.6 time, 140.3 real, 1475.4 MB
c [blimc] 140.05 bound 475
c [blimc] 140.64 bound 476
c [blimc] 141.23 bound 477
c [blimc] 141.83 bound 478
c [blimc] 142.42 bound 479
c [blimc] 143.02 bound 480
c [blimc] 143.62 bound 481
c [blimc] 144.22 bound 482
c [blimc] 144.82 bound 483
c [blimc] 145.43 bound 484
c [blimc] 146.03 bound 485
c [blimc] 146.65 bound 486
c [blimc] 147.25 bound 487
c [blimc] 147.87 bound 488
c [blimc] 148.48 bound 489
c [blimc] 149.10 bound 490
[runlim] sample:		149.5 time, 150.3 real, 2183.0 MB
c [blimc] 149.72 bound 491
c [blimc] 150.34 bound 492
c [blimc] 150.96 bound 493
c [blimc] 151.59 bound 494
c [blimc] 152.21 bound 495
c [blimc] 152.84 bound 496
c [blimc] 153.47 bound 497
c [blimc] 154.10 bound 498
c [blimc] 154.73 bound 499
c [blimc] 155.37 bound 500
c [blimc] 156.00 bound 501
c [blimc] 156.64 bound 502
c [blimc] 157.28 bound 503
c [blimc] 157.92 bound 504
c [blimc] 158.56 bound 505
c [blimc] 159.20 bound 506
[runlim] sample:		159.5 time, 160.3 real, 2150.9 MB
c [blimc] 159.84 bound 507
c [blimc] 160.49 bound 508
c [blimc] 161.13 bound 509
c [blimc] 161.79 bound 510
c [blimc] 162.50 bound 511
[runlim] sample:		169.5 time, 170.3 real, 747.8 MB
c [blimc] 169.71 bound 512
c [blimc] 170.05 bound 513
c [blimc] 170.40 bound 514
c [blimc] 170.74 bound 515
c [blimc] 171.10 bound 516
c [blimc] 171.45 bound 517
c [blimc] 171.81 bound 518
c [blimc] 172.17 bound 519
c [blimc] 172.53 bound 520
c [blimc] 172.90 bound 521
c [blimc] 173.27 bound 522
c [blimc] 173.64 bound 523
c [blimc] 174.01 bound 524
c [blimc] 174.38 bound 525
c [blimc] 174.76 bound 526
c [blimc] 175.14 bound 527
c [blimc] 175.52 bound 528
c [blimc] 175.90 bound 529
c [blimc] 176.29 bound 530
c [blimc] 176.67 bound 531
c [blimc] 177.05 bound 532
c [blimc] 177.45 bound 533
c [blimc] 177.85 bound 534
c [blimc] 178.25 bound 535
c [blimc] 178.65 bound 536
c [blimc] 179.05 bound 537
c [blimc] 179.46 bound 538
[runlim] sample:		179.5 time, 180.3 real, 869.9 MB
c [blimc] 179.85 bound 539
c [blimc] 180.25 bound 540
c [blimc] 180.65 bound 541
c [blimc] 181.05 bound 542
c [blimc] 181.44 bound 543
c [blimc] 181.85 bound 544
c [blimc] 182.25 bound 545
c [blimc] 182.66 bound 546
c [blimc] 183.06 bound 547
c [blimc] 183.48 bound 548
c [blimc] 183.88 bound 549
c [blimc] 184.30 bound 550
c [blimc] 184.71 bound 551
c [blimc] 185.13 bound 552
c [blimc] 185.55 bound 553
c [blimc] 185.97 bound 554
c [blimc] 186.39 bound 555
c [blimc] 186.81 bound 556
c [blimc] 187.24 bound 557
c [blimc] 187.67 bound 558
c [blimc] 188.09 bound 559
c [blimc] 188.55 bound 560
c [blimc] 188.98 bound 561
c [blimc] 189.41 bound 562
[runlim] sample:		189.4 time, 190.3 real, 967.1 MB
c [blimc] 189.86 bound 563
c [blimc] 190.30 bound 564
c [blimc] 190.73 bound 565
c [blimc] 191.18 bound 566
c [blimc] 191.62 bound 567
c [blimc] 192.06 bound 568
c [blimc] 192.51 bound 569
c [blimc] 192.96 bound 570
c [blimc] 193.40 bound 571
c [blimc] 193.86 bound 572
c [blimc] 194.31 bound 573
c [blimc] 194.77 bound 574
c [blimc] 195.23 bound 575
c [blimc] 195.69 bound 576
c [blimc] 196.15 bound 577
c [blimc] 196.62 bound 578
c [blimc] 197.09 bound 579
c [blimc] 197.56 bound 580
c [blimc] 198.03 bound 581
c [blimc] 198.50 bound 582
c [blimc] 198.97 bound 583
[runlim] sample:		199.4 time, 200.3 real, 1186.3 MB
c [blimc] 199.45 bound 584
c [blimc] 199.93 bound 585
c [blimc] 200.42 bound 586
c [blimc] 200.90 bound 587
c [blimc] 201.40 bound 588
c [blimc] 201.88 bound 589
c [blimc] 202.37 bound 590
c [blimc] 202.86 bound 591
c [blimc] 203.35 bound 592
c [blimc] 203.84 bound 593
c [blimc] 204.33 bound 594
c [blimc] 204.82 bound 595
c [blimc] 205.33 bound 596
c [blimc] 205.82 bound 597
c [blimc] 206.33 bound 598
c [blimc] 206.82 bound 599
c [blimc] 207.33 bound 600
c [blimc] 207.83 bound 601
c [blimc] 208.34 bound 602
c [blimc] 208.84 bound 603
c [blimc] 209.36 bound 604
[runlim] sample:		209.4 time, 210.3 real, 1086.9 MB
c [blimc] 209.87 bound 605
c [blimc] 210.38 bound 606
c [blimc] 210.90 bound 607
c [blimc] 211.42 bound 608
c [blimc] 211.94 bound 609
c [blimc] 212.46 bound 610
c [blimc] 212.98 bound 611
c [blimc] 213.51 bound 612
c [blimc] 214.04 bound 613
c [blimc] 214.56 bound 614
c [blimc] 215.10 bound 615
c [blimc] 215.63 bound 616
c [blimc] 216.16 bound 617
c [blimc] 216.70 bound 618
c [blimc] 217.24 bound 619
c [blimc] 217.78 bound 620
c [blimc] 218.32 bound 621
c [blimc] 218.86 bound 622
[runlim] sample:		219.4 time, 220.3 real, 1443.5 MB
c [blimc] 219.41 bound 623
c [blimc] 219.96 bound 624
c [blimc] 220.50 bound 625
c [blimc] 221.06 bound 626
c [blimc] 221.61 bound 627
c [blimc] 222.16 bound 628
c [blimc] 222.72 bound 629
c [blimc] 223.28 bound 630
c [blimc] 223.84 bound 631
c [blimc] 224.40 bound 632
c [blimc] 224.97 bound 633
c [blimc] 225.53 bound 634
c [blimc] 226.10 bound 635
c [blimc] 226.67 bound 636
c [blimc] 227.24 bound 637
c [blimc] 227.82 bound 638
c [blimc] 228.41 bound 639
c [blimc] 228.99 bound 640
[runlim] sample:		229.3 time, 230.3 real, 1575.8 MB
c [blimc] 229.56 bound 641
c [blimc] 230.15 bound 642
c [blimc] 230.73 bound 643
c [blimc] 231.31 bound 644
c [blimc] 231.90 bound 645
c [blimc] 232.49 bound 646
c [blimc] 233.08 bound 647
c [blimc] 233.67 bound 648
c [blimc] 234.26 bound 649
c [blimc] 234.86 bound 650
c [blimc] 235.46 bound 651
c [blimc] 236.06 bound 652
c [blimc] 236.66 bound 653
c [blimc] 237.27 bound 654
c [blimc] 237.87 bound 655
c [blimc] 238.48 bound 656
c [blimc] 239.11 bound 657
[runlim] sample:		239.3 time, 240.3 real, 1576.0 MB
c [blimc] 239.73 bound 658
c [blimc] 240.34 bound 659
c [blimc] 240.95 bound 660
c [blimc] 241.57 bound 661
c [blimc] 242.18 bound 662
c [blimc] 242.80 bound 663
c [blimc] 243.44 bound 664
c [blimc] 244.06 bound 665
c [blimc] 244.69 bound 666
c [blimc] 245.31 bound 667
c [blimc] 245.95 bound 668
c [blimc] 246.58 bound 669
c [blimc] 247.22 bound 670
c [blimc] 247.85 bound 671
c [blimc] 248.49 bound 672
c [blimc] 249.13 bound 673
[runlim] sample:		249.3 time, 250.3 real, 1491.3 MB
c [blimc] 249.77 bound 674
c [blimc] 250.41 bound 675
c [blimc] 251.06 bound 676
c [blimc] 251.70 bound 677
c [blimc] 252.35 bound 678
c [blimc] 252.99 bound 679
c [blimc] 253.64 bound 680
c [blimc] 254.29 bound 681
c [blimc] 254.95 bound 682
c [blimc] 255.60 bound 683
c [blimc] 256.26 bound 684
c [blimc] 256.92 bound 685
c [blimc] 257.58 bound 686
c [blimc] 258.24 bound 687
c [blimc] 258.91 bound 688
[runlim] sample:		259.3 time, 260.3 real, 1934.4 MB
c [blimc] 259.57 bound 689
c [blimc] 260.24 bound 690
c [blimc] 260.91 bound 691
c [blimc] 261.58 bound 692
c [blimc] 262.25 bound 693
c [blimc] 262.93 bound 694
c [blimc] 263.61 bound 695
c [blimc] 264.29 bound 696
c [blimc] 264.97 bound 697
c [blimc] 265.66 bound 698
c [blimc] 266.34 bound 699
c [blimc] 267.03 bound 700
c [blimc] 267.71 bound 701
c [blimc] 268.41 bound 702
c [blimc] 269.09 bound 703
[runlim] sample:		269.3 time, 270.3 real, 1552.7 MB
c [blimc] 269.79 bound 704
c [blimc] 270.49 bound 705
c [blimc] 271.19 bound 706
c [blimc] 271.88 bound 707
c [blimc] 272.59 bound 708
c [blimc] 273.29 bound 709
c [blimc] 273.99 bound 710
c [blimc] 274.70 bound 711
c [blimc] 275.41 bound 712
c [blimc] 276.12 bound 713
c [blimc] 276.84 bound 714
c [blimc] 277.55 bound 715
c [blimc] 278.27 bound 716
c [blimc] 278.98 bound 717
[runlim] sample:		279.2 time, 280.3 real, 1818.4 MB
c [blimc] 279.71 bound 718
c [blimc] 280.43 bound 719
c [blimc] 281.15 bound 720
c [blimc] 281.87 bound 721
c [blimc] 282.60 bound 722
c [blimc] 283.33 bound 723
c [blimc] 284.06 bound 724
c [blimc] 284.79 bound 725
c [blimc] 285.54 bound 726
c [blimc] 286.27 bound 727
c [blimc] 287.01 bound 728
c [blimc] 287.75 bound 729
c [blimc] 288.49 bound 730
[runlim] sample:		289.2 time, 290.3 real, 2182.4 MB
c [blimc] 289.23 bound 731
c [blimc] 289.98 bound 732
c [blimc] 290.72 bound 733
c [blimc] 291.47 bound 734
c [blimc] 292.22 bound 735
c [blimc] 292.98 bound 736
c [blimc] 293.73 bound 737
c [blimc] 294.49 bound 738
c [blimc] 295.24 bound 739
c [blimc] 296.00 bound 740
c [blimc] 296.76 bound 741
c [blimc] 297.53 bound 742
c [blimc] 298.29 bound 743
c [blimc] 299.06 bound 744
[runlim] sample:		299.2 time, 300.3 real, 1580.5 MB
c [blimc] 299.83 bound 745
c [blimc] 300.60 bound 746
c [blimc] 301.37 bound 747
c [blimc] 302.15 bound 748
c [blimc] 302.92 bound 749
c [blimc] 303.70 bound 750
c [blimc] 304.48 bound 751
c [blimc] 305.27 bound 752
c [blimc] 306.05 bound 753
c [blimc] 306.84 bound 754
c [blimc] 307.62 bound 755
c [blimc] 308.42 bound 756
[runlim] sample:		309.2 time, 310.3 real, 2335.9 MB
c [blimc] 309.21 bound 757
c [blimc] 310.00 bound 758
c [blimc] 310.79 bound 759
c [blimc] 311.59 bound 760
c [blimc] 312.39 bound 761
c [blimc] 313.19 bound 762
c [blimc] 313.99 bound 763
c [blimc] 314.80 bound 764
c [blimc] 315.61 bound 765
c [blimc] 316.44 bound 766
c [blimc] 317.25 bound 767
c [blimc] 318.07 bound 768
c [blimc] 318.87 bound 769
[runlim] sample:		319.1 time, 320.3 real, 2031.9 MB
c [blimc] 319.69 bound 770
c [blimc] 320.51 bound 771
c [blimc] 321.33 bound 772
c [blimc] 322.15 bound 773
c [blimc] 322.97 bound 774
c [blimc] 323.79 bound 775
c [blimc] 324.62 bound 776
c [blimc] 325.45 bound 777
c [blimc] 326.29 bound 778
c [blimc] 327.12 bound 779
c [blimc] 327.96 bound 780
c [blimc] 328.94 bound 781
[runlim] sample:		329.1 time, 330.3 real, 2163.2 MB
c [blimc] 329.78 bound 782
c [blimc] 330.63 bound 783
c [blimc] 331.47 bound 784
c [blimc] 332.32 bound 785
c [blimc] 333.17 bound 786
c [blimc] 334.02 bound 787
c [blimc] 334.89 bound 788
c [blimc] 335.74 bound 789
c [blimc] 336.60 bound 790
c [blimc] 337.45 bound 791
c [blimc] 338.31 bound 792
[runlim] sample:		339.1 time, 340.3 real, 2964.4 MB
c [blimc] 339.17 bound 793
c [blimc] 340.04 bound 794
c [blimc] 340.90 bound 795
c [blimc] 341.77 bound 796
c [blimc] 342.63 bound 797
c [blimc] 343.50 bound 798
c [blimc] 344.37 bound 799
c [blimc] 345.27 bound 800
c [blimc] 346.15 bound 801
c [blimc] 347.04 bound 802
c [blimc] 347.92 bound 803
c [blimc] 348.80 bound 804
[runlim] sample:		349.1 time, 350.3 real, 2548.0 MB
c [blimc] 349.68 bound 805
c [blimc] 350.57 bound 806
c [blimc] 351.46 bound 807
c [blimc] 352.35 bound 808
c [blimc] 353.24 bound 809
c [blimc] 354.14 bound 810
c [blimc] 355.03 bound 811
c [blimc] 355.92 bound 812
c [blimc] 356.82 bound 813
c [blimc] 357.72 bound 814
c [blimc] 358.66 bound 815
[runlim] sample:		359.0 time, 360.3 real, 3010.3 MB
c [blimc] 359.57 bound 816
c [blimc] 360.47 bound 817
c [blimc] 361.38 bound 818
c [blimc] 362.28 bound 819
c [blimc] 363.19 bound 820
c [blimc] 364.10 bound 821
c [blimc] 365.02 bound 822
c [blimc] 365.92 bound 823
c [blimc] 366.84 bound 824
c [blimc] 367.76 bound 825
c [blimc] 368.68 bound 826
[runlim] sample:		369.0 time, 370.3 real, 2929.5 MB
c [blimc] 369.60 bound 827
c [blimc] 370.52 bound 828
c [blimc] 371.45 bound 829
c [blimc] 372.38 bound 830
c [blimc] 373.30 bound 831
c [blimc] 374.23 bound 832
c [blimc] 375.17 bound 833
c [blimc] 376.11 bound 834
c [blimc] 377.05 bound 835
c [blimc] 378.00 bound 836
c [blimc] 378.94 bound 837
[runlim] sample:		379.0 time, 380.3 real, 2437.0 MB
c [blimc] 379.88 bound 838
c [blimc] 380.83 bound 839
c [blimc] 381.78 bound 840
c [blimc] 382.73 bound 841
c [blimc] 383.69 bound 842
c [blimc] 384.64 bound 843
c [blimc] 385.59 bound 844
c [blimc] 386.54 bound 845
c [blimc] 387.51 bound 846
c [blimc] 388.46 bound 847
[runlim] sample:		389.0 time, 390.3 real, 3455.1 MB
c [blimc] 389.43 bound 848
c [blimc] 390.39 bound 849
c [blimc] 391.35 bound 850
c [blimc] 392.31 bound 851
c [blimc] 393.28 bound 852
c [blimc] 394.25 bound 853
c [blimc] 395.23 bound 854
c [blimc] 396.20 bound 855
c [blimc] 397.17 bound 856
c [blimc] 398.15 bound 857
[runlim] sample:		398.9 time, 400.3 real, 3514.1 MB
c [blimc] 399.13 bound 858
c [blimc] 400.11 bound 859
c [blimc] 401.09 bound 860
c [blimc] 402.07 bound 861
c [blimc] 403.06 bound 862
c [blimc] 404.05 bound 863
c [blimc] 405.04 bound 864
c [blimc] 406.03 bound 865
c [blimc] 407.02 bound 866
c [blimc] 408.02 bound 867
[runlim] sample:		408.9 time, 410.3 real, 3573.2 MB
c [blimc] 409.02 bound 868
c [blimc] 410.01 bound 869
c [blimc] 411.01 bound 870
c [blimc] 412.02 bound 871
c [blimc] 413.02 bound 872
c [blimc] 414.02 bound 873
c [blimc] 415.03 bound 874
c [blimc] 416.04 bound 875
c [blimc] 417.05 bound 876
c [blimc] 418.06 bound 877
[runlim] sample:		418.9 time, 420.3 real, 3632.1 MB
c [blimc] 419.08 bound 878
c [blimc] 420.09 bound 879
c [blimc] 421.12 bound 880
c [blimc] 422.14 bound 881
c [blimc] 423.16 bound 882
c [blimc] 424.18 bound 883
c [blimc] 425.21 bound 884
c [blimc] 426.24 bound 885
c [blimc] 427.27 bound 886
c [blimc] 428.30 bound 887
[runlim] sample:		428.9 time, 430.3 real, 3671.0 MB
c [blimc] 429.34 bound 888
c [blimc] 430.37 bound 889
c [blimc] 431.41 bound 890
c [blimc] 432.45 bound 891
c [blimc] 433.49 bound 892
c [blimc] 434.53 bound 893
c [blimc] 435.58 bound 894
c [blimc] 436.62 bound 895
c [blimc] 437.67 bound 896
c [blimc] 438.72 bound 897
[runlim] sample:		438.8 time, 440.3 real, 2614.1 MB
c [blimc] 439.77 bound 898
c [blimc] 440.82 bound 899
c [blimc] 441.88 bound 900
c [blimc] 442.93 bound 901
c [blimc] 443.99 bound 902
c [blimc] 445.05 bound 903
c [blimc] 446.13 bound 904
c [blimc] 447.19 bound 905
c [blimc] 448.27 bound 906
[runlim] sample:		448.8 time, 450.3 real, 3656.2 MB
c [blimc] 449.33 bound 907
c [blimc] 450.41 bound 908
c [blimc] 451.48 bound 909
c [blimc] 452.55 bound 910
c [blimc] 453.62 bound 911
c [blimc] 454.71 bound 912
c [blimc] 455.79 bound 913
c [blimc] 456.87 bound 914
c [blimc] 457.95 bound 915
[runlim] sample:		458.8 time, 460.3 real, 3856.3 MB
c [blimc] 459.04 bound 916
c [blimc] 460.13 bound 917
c [blimc] 461.22 bound 918
c [blimc] 462.31 bound 919
c [blimc] 463.40 bound 920
c [blimc] 464.49 bound 921
c [blimc] 465.60 bound 922
c [blimc] 466.69 bound 923
c [blimc] 467.79 bound 924
[runlim] sample:		468.7 time, 470.3 real, 3909.5 MB
c [blimc] 468.89 bound 925
c [blimc] 470.00 bound 926
c [blimc] 471.10 bound 927
c [blimc] 472.21 bound 928
c [blimc] 473.31 bound 929
c [blimc] 474.43 bound 930
c [blimc] 475.55 bound 931
c [blimc] 476.66 bound 932
c [blimc] 477.78 bound 933
[runlim] sample:		478.7 time, 480.3 real, 3962.5 MB
c [blimc] 478.90 bound 934
c [blimc] 480.01 bound 935
c [blimc] 481.14 bound 936
c [blimc] 482.26 bound 937
c [blimc] 483.39 bound 938
c [blimc] 484.52 bound 939
c [blimc] 485.65 bound 940
c [blimc] 486.78 bound 941
c [blimc] 487.91 bound 942
[runlim] sample:		488.7 time, 490.3 real, 4015.6 MB
c [blimc] 489.04 bound 943
c [blimc] 490.19 bound 944
c [blimc] 491.32 bound 945
c [blimc] 492.46 bound 946
c [blimc] 493.60 bound 947
c [blimc] 494.75 bound 948
c [blimc] 495.89 bound 949
c [blimc] 497.04 bound 950
c [blimc] 498.19 bound 951
[runlim] sample:		498.7 time, 500.3 real, 3658.2 MB
c [blimc] 499.34 bound 952
c [blimc] 500.49 bound 953
c [blimc] 501.65 bound 954
c [blimc] 502.80 bound 955
c [blimc] 503.96 bound 956
c [blimc] 505.12 bound 957
c [blimc] 506.30 bound 958
c [blimc] 507.46 bound 959
c [blimc] 508.63 bound 960
[runlim] sample:		508.6 time, 510.3 real, 2800.0 MB
c [blimc] 509.79 bound 961
c [blimc] 510.97 bound 962
c [blimc] 512.13 bound 963
c [blimc] 513.31 bound 964
c [blimc] 514.48 bound 965
c [blimc] 515.66 bound 966
c [blimc] 516.84 bound 967
c [blimc] 518.03 bound 968
[runlim] sample:		518.6 time, 520.3 real, 3937.0 MB
c [blimc] 519.22 bound 969
c [blimc] 520.40 bound 970
c [blimc] 521.58 bound 971
c [blimc] 522.77 bound 972
c [blimc] 523.96 bound 973
c [blimc] 525.15 bound 974
c [blimc] 526.35 bound 975
c [blimc] 527.54 bound 976
[runlim] sample:		528.6 time, 530.3 real, 4216.5 MB
c [blimc] 528.74 bound 977
c [blimc] 529.94 bound 978
c [blimc] 531.13 bound 979
c [blimc] 532.34 bound 980
c [blimc] 533.54 bound 981
c [blimc] 534.76 bound 982
c [blimc] 535.96 bound 983
c [blimc] 537.17 bound 984
c [blimc] 538.38 bound 985
[runlim] sample:		538.5 time, 540.3 real, 2873.8 MB
c [blimc] 539.60 bound 986
c [blimc] 540.81 bound 987
c [blimc] 542.03 bound 988
c [blimc] 543.24 bound 989
c [blimc] 544.47 bound 990
c [blimc] 545.69 bound 991
c [blimc] 546.91 bound 992
c [blimc] 548.14 bound 993
[runlim] sample:		548.5 time, 550.3 real, 3357.1 MB
c [blimc] 549.37 bound 994
c [blimc] 550.59 bound 995
c [blimc] 551.83 bound 996
c [blimc] 553.06 bound 997
c [blimc] 554.29 bound 998
c [blimc] 555.53 bound 999
c [blimc] 556.78 bound 1000
c [lgl1000]   13.861   5% simplifying
c [lgl1000]    0.000   0% search
c [lgl1000] ==================================
c [lgl1000]  258.937 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]      33318549 propagations,   128674.3 props/sec,      0.0 props/decision
c [lgl1000] 
c [lgl1000] 258.9 seconds, 4259.0 MB
c [blimc] 558.02 reached k = 1001
c [blimc] 558.02 cloned 0 solvers
c [blimc] 558.02 max 4263.1 MB
c [blimc] 558.16 exit 20
[runlim] end:			Mon Sep 21 02:35:22 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			560.05 seconds
[runlim] time:			558.14 seconds
[runlim] space:			4357.9 MB
[runlim] samples:		5597
