[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/6s206rb025.aig
[runlim] start:			Mon Sep 21 02:00:22 2015
[runlim] main pid:		10837
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/6s206rb025.aig
c [blimc] 0.03 MILOA 181499 9204 28643 1 143652
c [blimc] 0.03 BCJK 0 0 0 0 143652
c [blimc] 0.03 28643 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:     109480 =  60% out of 181499
c [blimc] 0.03 inputs    in COI:        285 =   3% out of 9204
c [blimc] 0.03 latches   in COI:      14586 =  51% out of 28643
c [blimc] 0.03 constants in COI:          1 = 100% out of 1
c [blimc] 0.03 ands      in COI:      94608 =  66% out of 143652
c [blimc] 0.12 encoded
c [blimc] 7.32 simplified
c [blimc] 7.35 extracted
c [lglopt]    7.201 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]    7.204 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]        107437 propagations,    14914.4 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 7.2 seconds, 25.5 MB
c [blimc] 7.36 mapped 73987 variables
c [blimc] 7.36 maxk 1000
c [blimc] 7.36 bound 0
c [blimc] 7.46 bound 1
c [blimc] 7.56 bound 2
c [blimc] 7.59 bound 3
c [blimc] 7.78 bound 4
c [blimc] 7.82 bound 5
c [blimc] 7.87 bound 6
c [blimc] 7.93 bound 7
c [blimc] 8.36 bound 8
c [blimc] 8.41 bound 9
c [blimc] 8.47 bound 10
c [blimc] 8.53 bound 11
c [blimc] 8.60 bound 12
c [blimc] 8.67 bound 13
c [blimc] 8.75 bound 14
c [blimc] 8.83 bound 15
c [blimc] 9.63 bound 16
c [blimc] 9.68 bound 17
c [blimc] 9.75 bound 18
c [blimc] 9.81 bound 19
c [blimc] 9.89 bound 20
c [blimc] 9.97 bound 21
[runlim] sample:		10.0 time, 10.3 real, 123.2 MB
c [blimc] 10.06 bound 22
c [blimc] 10.15 bound 23
c [blimc] 10.25 bound 24
c [blimc] 10.34 bound 25
c [blimc] 10.45 bound 26
c [blimc] 10.54 bound 27
c [blimc] 10.67 bound 28
c [blimc] 10.80 bound 29
c [blimc] 10.93 bound 30
c [blimc] 11.04 bound 31
c [blimc] 12.90 bound 32
c [blimc] 12.98 bound 33
c [blimc] 13.06 bound 34
c [blimc] 13.14 bound 35
c [blimc] 13.24 bound 36
c [blimc] 13.33 bound 37
c [blimc] 13.44 bound 38
c [blimc] 13.53 bound 39
c [blimc] 13.65 bound 40
c [blimc] 13.76 bound 41
c [blimc] 13.88 bound 42
c [blimc] 14.00 bound 43
c [blimc] 14.13 bound 44
c [blimc] 14.25 bound 45
c [blimc] 14.38 bound 46
c [blimc] 14.50 bound 47
c [blimc] 14.63 bound 48
c [blimc] 14.76 bound 49
c [blimc] 14.90 bound 50
c [blimc] 15.06 bound 51
c [blimc] 15.22 bound 52
c [blimc] 15.37 bound 53
c [blimc] 15.55 bound 54
c [blimc] 15.70 bound 55
c [blimc] 15.87 bound 56
c [blimc] 16.04 bound 57
c [blimc] 16.21 bound 58
c [blimc] 16.37 bound 59
c [blimc] 16.54 bound 60
c [blimc] 16.71 bound 61
c [blimc] 16.90 bound 62
c [blimc] 17.07 bound 63
[runlim] sample:		19.9 time, 20.3 real, 282.7 MB
c [blimc] 20.83 bound 64
c [blimc] 20.94 bound 65
c [blimc] 21.07 bound 66
c [blimc] 21.18 bound 67
c [blimc] 21.31 bound 68
c [blimc] 21.44 bound 69
c [blimc] 21.57 bound 70
c [blimc] 21.71 bound 71
c [blimc] 21.86 bound 72
c [blimc] 22.00 bound 73
c [blimc] 22.16 bound 74
c [blimc] 22.31 bound 75
c [blimc] 22.48 bound 76
c [blimc] 22.65 bound 77
c [blimc] 22.82 bound 78
c [blimc] 22.97 bound 79
c [blimc] 23.16 bound 80
c [blimc] 23.32 bound 81
c [blimc] 23.49 bound 82
c [blimc] 23.66 bound 83
c [blimc] 23.84 bound 84
c [blimc] 24.02 bound 85
c [blimc] 24.22 bound 86
c [blimc] 24.40 bound 87
c [blimc] 24.60 bound 88
c [blimc] 24.80 bound 89
c [blimc] 25.00 bound 90
c [blimc] 25.19 bound 91
c [blimc] 25.40 bound 92
c [blimc] 25.60 bound 93
c [blimc] 25.81 bound 94
c [blimc] 26.03 bound 95
c [blimc] 26.25 bound 96
c [blimc] 26.47 bound 97
c [blimc] 26.70 bound 98
c [blimc] 26.93 bound 99
c [blimc] 27.17 bound 100
c [blimc] 27.39 bound 101
c [blimc] 27.64 bound 102
c [blimc] 27.87 bound 103
c [blimc] 28.12 bound 104
c [blimc] 28.36 bound 105
c [blimc] 28.61 bound 106
c [blimc] 28.85 bound 107
c [blimc] 29.12 bound 108
c [blimc] 29.37 bound 109
c [blimc] 29.64 bound 110
c [blimc] 29.90 bound 111
[runlim] sample:		29.9 time, 30.3 real, 577.5 MB
c [blimc] 30.19 bound 112
c [blimc] 30.46 bound 113
c [blimc] 30.79 bound 114
c [blimc] 31.06 bound 115
c [blimc] 31.35 bound 116
c [blimc] 31.63 bound 117
c [blimc] 31.92 bound 118
c [blimc] 32.21 bound 119
c [blimc] 32.51 bound 120
c [blimc] 32.80 bound 121
c [blimc] 33.11 bound 122
c [blimc] 33.41 bound 123
c [blimc] 33.73 bound 124
c [blimc] 34.03 bound 125
c [blimc] 34.38 bound 126
c [blimc] 34.69 bound 127
[runlim] sample:		39.9 time, 40.3 real, 436.1 MB
c [blimc] 42.22 bound 128
c [blimc] 42.39 bound 129
c [blimc] 42.59 bound 130
c [blimc] 42.77 bound 131
c [blimc] 42.97 bound 132
c [blimc] 43.17 bound 133
c [blimc] 43.38 bound 134
c [blimc] 43.57 bound 135
c [blimc] 43.79 bound 136
c [blimc] 44.01 bound 137
c [blimc] 44.24 bound 138
c [blimc] 44.47 bound 139
c [blimc] 44.71 bound 140
c [blimc] 44.94 bound 141
c [blimc] 45.18 bound 142
c [blimc] 45.42 bound 143
c [blimc] 45.68 bound 144
c [blimc] 45.93 bound 145
c [blimc] 46.17 bound 146
c [blimc] 46.41 bound 147
c [blimc] 46.67 bound 148
c [blimc] 46.94 bound 149
c [blimc] 47.21 bound 150
c [blimc] 47.45 bound 151
c [blimc] 47.72 bound 152
c [blimc] 47.98 bound 153
c [blimc] 48.25 bound 154
c [blimc] 48.52 bound 155
c [blimc] 48.80 bound 156
c [blimc] 49.07 bound 157
c [blimc] 49.36 bound 158
c [blimc] 49.63 bound 159
[runlim] sample:		49.9 time, 50.3 real, 818.4 MB
c [blimc] 49.92 bound 160
c [blimc] 50.21 bound 161
c [blimc] 50.50 bound 162
c [blimc] 50.79 bound 163
c [blimc] 51.10 bound 164
c [blimc] 51.39 bound 165
c [blimc] 51.70 bound 166
c [blimc] 52.01 bound 167
c [blimc] 52.33 bound 168
c [blimc] 52.65 bound 169
c [blimc] 52.98 bound 170
c [blimc] 53.29 bound 171
c [blimc] 53.62 bound 172
c [blimc] 53.94 bound 173
c [blimc] 54.28 bound 174
c [blimc] 54.61 bound 175
c [blimc] 54.97 bound 176
c [blimc] 55.31 bound 177
c [blimc] 55.66 bound 178
c [blimc] 56.00 bound 179
c [blimc] 56.36 bound 180
c [blimc] 56.71 bound 181
c [blimc] 57.08 bound 182
c [blimc] 57.43 bound 183
c [blimc] 57.80 bound 184
c [blimc] 58.17 bound 185
c [blimc] 58.54 bound 186
c [blimc] 58.91 bound 187
c [blimc] 59.30 bound 188
c [blimc] 59.67 bound 189
[runlim] sample:		59.9 time, 60.3 real, 1167.9 MB
c [blimc] 60.07 bound 190
c [blimc] 60.45 bound 191
c [blimc] 60.85 bound 192
c [blimc] 61.24 bound 193
c [blimc] 61.64 bound 194
c [blimc] 62.04 bound 195
c [blimc] 62.45 bound 196
c [blimc] 62.85 bound 197
c [blimc] 63.27 bound 198
c [blimc] 63.68 bound 199
c [blimc] 64.11 bound 200
c [blimc] 64.52 bound 201
c [blimc] 64.95 bound 202
c [blimc] 65.38 bound 203
c [blimc] 65.82 bound 204
c [blimc] 66.24 bound 205
c [blimc] 66.69 bound 206
c [blimc] 67.13 bound 207
c [blimc] 67.60 bound 208
c [blimc] 68.04 bound 209
c [blimc] 68.53 bound 210
c [blimc] 68.98 bound 211
c [blimc] 69.45 bound 212
[runlim] sample:		69.9 time, 70.3 real, 1532.0 MB
c [blimc] 69.91 bound 213
c [blimc] 70.38 bound 214
c [blimc] 70.84 bound 215
c [blimc] 71.31 bound 216
c [blimc] 71.78 bound 217
c [blimc] 72.26 bound 218
c [blimc] 72.74 bound 219
c [blimc] 73.22 bound 220
c [blimc] 73.70 bound 221
c [blimc] 74.20 bound 222
c [blimc] 74.69 bound 223
c [blimc] 75.25 bound 224
c [blimc] 75.75 bound 225
c [blimc] 76.26 bound 226
c [blimc] 76.83 bound 227
c [blimc] 77.34 bound 228
c [blimc] 77.85 bound 229
c [blimc] 78.38 bound 230
c [blimc] 78.89 bound 231
c [blimc] 79.42 bound 232
[runlim] sample:		79.8 time, 80.3 real, 2023.3 MB
c [blimc] 79.94 bound 233
c [blimc] 80.48 bound 234
c [blimc] 81.00 bound 235
c [blimc] 81.55 bound 236
c [blimc] 82.08 bound 237
c [blimc] 82.64 bound 238
c [blimc] 83.18 bound 239
c [blimc] 83.74 bound 240
c [blimc] 84.29 bound 241
c [blimc] 84.85 bound 242
c [blimc] 85.41 bound 243
c [blimc] 85.98 bound 244
c [blimc] 86.54 bound 245
c [blimc] 87.12 bound 246
c [blimc] 87.69 bound 247
c [blimc] 88.28 bound 248
c [blimc] 88.86 bound 249
c [blimc] 89.45 bound 250
[runlim] sample:		89.8 time, 90.3 real, 2206.2 MB
c [blimc] 90.03 bound 251
c [blimc] 90.63 bound 252
c [blimc] 91.21 bound 253
c [blimc] 91.81 bound 254
c [blimc] 92.41 bound 255
[runlim] sample:		99.8 time, 100.3 real, 868.3 MB
c [blimc] 107.40 bound 256
c [blimc] 107.72 bound 257
c [blimc] 108.05 bound 258
c [blimc] 108.38 bound 259
c [blimc] 108.72 bound 260
c [blimc] 109.05 bound 261
c [blimc] 109.41 bound 262
c [blimc] 109.75 bound 263
[runlim] sample:		109.8 time, 110.3 real, 832.8 MB
c [blimc] 110.10 bound 264
c [blimc] 110.45 bound 265
c [blimc] 110.82 bound 266
c [blimc] 111.18 bound 267
c [blimc] 111.55 bound 268
c [blimc] 111.91 bound 269
c [blimc] 112.29 bound 270
c [blimc] 112.65 bound 271
c [blimc] 113.03 bound 272
c [blimc] 113.42 bound 273
c [blimc] 113.81 bound 274
c [blimc] 114.19 bound 275
c [blimc] 114.58 bound 276
c [blimc] 114.97 bound 277
c [blimc] 115.37 bound 278
c [blimc] 115.78 bound 279
c [blimc] 116.19 bound 280
c [blimc] 116.59 bound 281
c [blimc] 117.00 bound 282
c [blimc] 117.41 bound 283
c [blimc] 117.82 bound 284
c [blimc] 118.23 bound 285
c [blimc] 118.66 bound 286
c [blimc] 119.07 bound 287
c [blimc] 119.50 bound 288
[runlim] sample:		119.8 time, 120.3 real, 1171.0 MB
c [blimc] 119.93 bound 289
c [blimc] 120.37 bound 290
c [blimc] 120.80 bound 291
c [blimc] 121.24 bound 292
c [blimc] 121.68 bound 293
c [blimc] 122.13 bound 294
c [blimc] 122.57 bound 295
c [blimc] 123.03 bound 296
c [blimc] 123.48 bound 297
c [blimc] 123.94 bound 298
c [blimc] 124.40 bound 299
c [blimc] 124.87 bound 300
c [blimc] 125.33 bound 301
c [blimc] 125.81 bound 302
c [blimc] 126.28 bound 303
c [blimc] 126.77 bound 304
c [blimc] 127.25 bound 305
c [blimc] 127.77 bound 306
c [blimc] 128.25 bound 307
c [blimc] 128.75 bound 308
c [blimc] 129.26 bound 309
[runlim] sample:		129.7 time, 130.3 real, 1422.5 MB
c [blimc] 129.77 bound 310
c [blimc] 130.27 bound 311
c [blimc] 130.78 bound 312
c [blimc] 131.28 bound 313
c [blimc] 131.79 bound 314
c [blimc] 132.30 bound 315
c [blimc] 132.83 bound 316
c [blimc] 133.34 bound 317
c [blimc] 133.87 bound 318
c [blimc] 134.39 bound 319
c [blimc] 134.93 bound 320
c [blimc] 135.46 bound 321
c [blimc] 136.00 bound 322
c [blimc] 136.54 bound 323
c [blimc] 137.09 bound 324
c [blimc] 137.62 bound 325
c [blimc] 138.18 bound 326
c [blimc] 138.73 bound 327
c [blimc] 139.29 bound 328
[runlim] sample:		139.7 time, 140.3 real, 1616.3 MB
c [blimc] 139.84 bound 329
c [blimc] 140.42 bound 330
c [blimc] 140.98 bound 331
c [blimc] 141.56 bound 332
c [blimc] 142.13 bound 333
c [blimc] 142.72 bound 334
c [blimc] 143.29 bound 335
c [blimc] 143.88 bound 336
c [blimc] 144.46 bound 337
c [blimc] 145.06 bound 338
c [blimc] 145.65 bound 339
c [blimc] 146.25 bound 340
c [blimc] 146.84 bound 341
c [blimc] 147.45 bound 342
c [blimc] 148.05 bound 343
c [blimc] 148.67 bound 344
c [blimc] 149.27 bound 345
[runlim] sample:		149.7 time, 150.3 real, 1789.1 MB
c [blimc] 149.90 bound 346
c [blimc] 150.51 bound 347
c [blimc] 151.14 bound 348
c [blimc] 151.76 bound 349
c [blimc] 152.40 bound 350
c [blimc] 153.02 bound 351
c [blimc] 153.68 bound 352
c [blimc] 154.32 bound 353
c [blimc] 154.97 bound 354
c [blimc] 155.61 bound 355
c [blimc] 156.29 bound 356
c [blimc] 156.93 bound 357
c [blimc] 157.64 bound 358
c [blimc] 158.29 bound 359
c [blimc] 158.96 bound 360
c [blimc] 159.62 bound 361
[runlim] sample:		159.7 time, 160.3 real, 1610.7 MB
c [blimc] 160.30 bound 362
c [blimc] 160.96 bound 363
c [blimc] 161.64 bound 364
c [blimc] 162.32 bound 365
c [blimc] 163.01 bound 366
c [blimc] 163.68 bound 367
c [blimc] 164.38 bound 368
c [blimc] 165.06 bound 369
c [blimc] 165.77 bound 370
c [blimc] 166.46 bound 371
c [blimc] 167.17 bound 372
c [blimc] 167.87 bound 373
c [blimc] 168.58 bound 374
c [blimc] 169.29 bound 375
[runlim] sample:		169.7 time, 170.3 real, 2291.0 MB
c [blimc] 170.01 bound 376
c [blimc] 170.72 bound 377
c [blimc] 171.45 bound 378
c [blimc] 172.17 bound 379
c [blimc] 172.90 bound 380
c [blimc] 173.63 bound 381
c [blimc] 174.37 bound 382
c [blimc] 175.10 bound 383
c [blimc] 175.85 bound 384
c [blimc] 176.59 bound 385
c [blimc] 177.34 bound 386
c [blimc] 178.09 bound 387
c [blimc] 178.85 bound 388
c [blimc] 179.60 bound 389
[runlim] sample:		179.6 time, 180.3 real, 1759.6 MB
c [blimc] 180.37 bound 390
c [blimc] 181.13 bound 391
c [blimc] 181.91 bound 392
c [blimc] 182.67 bound 393
c [blimc] 183.45 bound 394
c [blimc] 184.22 bound 395
c [blimc] 185.01 bound 396
c [blimc] 185.79 bound 397
c [blimc] 186.58 bound 398
c [blimc] 187.37 bound 399
c [blimc] 188.17 bound 400
c [blimc] 188.96 bound 401
[runlim] sample:		189.5 time, 190.3 real, 2561.1 MB
c [blimc] 189.77 bound 402
c [blimc] 190.57 bound 403
c [blimc] 191.38 bound 404
c [blimc] 192.18 bound 405
c [blimc] 193.00 bound 406
c [blimc] 193.81 bound 407
c [blimc] 194.64 bound 408
c [blimc] 195.46 bound 409
c [blimc] 196.29 bound 410
c [blimc] 197.11 bound 411
c [blimc] 197.95 bound 412
c [blimc] 198.79 bound 413
[runlim] sample:		199.5 time, 200.3 real, 2684.9 MB
c [blimc] 199.63 bound 414
c [blimc] 200.47 bound 415
c [blimc] 201.32 bound 416
c [blimc] 202.17 bound 417
c [blimc] 203.03 bound 418
c [blimc] 203.88 bound 419
c [blimc] 204.75 bound 420
c [blimc] 205.60 bound 421
c [blimc] 206.47 bound 422
c [blimc] 207.34 bound 423
c [blimc] 208.22 bound 424
c [blimc] 209.09 bound 425
[runlim] sample:		209.5 time, 210.3 real, 2677.6 MB
c [blimc] 209.98 bound 426
c [blimc] 210.86 bound 427
c [blimc] 211.75 bound 428
c [blimc] 212.63 bound 429
c [blimc] 213.53 bound 430
c [blimc] 214.43 bound 431
c [blimc] 215.34 bound 432
c [blimc] 216.24 bound 433
c [blimc] 217.15 bound 434
c [blimc] 218.06 bound 435
c [blimc] 218.98 bound 436
[runlim] sample:		219.5 time, 220.3 real, 2919.6 MB
c [blimc] 219.89 bound 437
c [blimc] 220.81 bound 438
c [blimc] 221.73 bound 439
c [blimc] 222.66 bound 440
c [blimc] 223.59 bound 441
c [blimc] 224.53 bound 442
c [blimc] 225.46 bound 443
c [blimc] 226.41 bound 444
c [blimc] 227.34 bound 445
c [blimc] 228.30 bound 446
c [blimc] 229.24 bound 447
[runlim] sample:		229.4 time, 230.3 real, 2183.0 MB
c [blimc] 230.25 bound 448
c [blimc] 231.21 bound 449
c [blimc] 232.18 bound 450
c [blimc] 233.14 bound 451
c [blimc] 234.11 bound 452
c [blimc] 235.08 bound 453
c [blimc] 236.19 bound 454
c [blimc] 237.17 bound 455
c [blimc] 238.16 bound 456
c [blimc] 239.16 bound 457
[runlim] sample:		239.4 time, 240.3 real, 2889.5 MB
c [blimc] 240.16 bound 458
c [blimc] 241.15 bound 459
c [blimc] 242.15 bound 460
c [blimc] 243.14 bound 461
c [blimc] 244.15 bound 462
c [blimc] 245.15 bound 463
c [blimc] 246.24 bound 464
c [blimc] 247.25 bound 465
c [blimc] 248.27 bound 466
c [blimc] 249.29 bound 467
[runlim] sample:		249.4 time, 250.3 real, 2920.9 MB
c [blimc] 250.31 bound 468
c [blimc] 251.33 bound 469
c [blimc] 252.36 bound 470
c [blimc] 253.39 bound 471
c [blimc] 254.43 bound 472
c [blimc] 255.46 bound 473
c [blimc] 256.51 bound 474
c [blimc] 257.54 bound 475
c [blimc] 258.59 bound 476
[runlim] sample:		259.4 time, 260.3 real, 4086.0 MB
c [blimc] 259.64 bound 477
c [blimc] 260.70 bound 478
c [blimc] 261.75 bound 479
c [blimc] 262.84 bound 480
c [blimc] 263.90 bound 481
c [blimc] 264.97 bound 482
c [blimc] 266.03 bound 483
c [blimc] 267.11 bound 484
c [blimc] 268.18 bound 485
c [blimc] 269.27 bound 486
[runlim] sample:		269.3 time, 270.3 real, 3041.2 MB
c [blimc] 270.34 bound 487
c [blimc] 271.44 bound 488
c [blimc] 272.53 bound 489
c [blimc] 273.63 bound 490
c [blimc] 274.73 bound 491
c [blimc] 275.83 bound 492
c [blimc] 276.93 bound 493
c [blimc] 278.04 bound 494
c [blimc] 279.14 bound 495
[runlim] sample:		279.3 time, 280.3 real, 3087.7 MB
c [blimc] 280.27 bound 496
c [blimc] 281.38 bound 497
c [blimc] 282.51 bound 498
c [blimc] 283.63 bound 499
c [blimc] 284.76 bound 500
c [blimc] 285.88 bound 501
c [blimc] 287.02 bound 502
c [blimc] 288.15 bound 503
[runlim] sample:		289.3 time, 290.3 real, 4410.9 MB
c [blimc] 289.30 bound 504
c [blimc] 290.44 bound 505
c [blimc] 291.60 bound 506
c [blimc] 292.75 bound 507
c [blimc] 293.91 bound 508
c [blimc] 295.07 bound 509
c [blimc] 296.23 bound 510
c [blimc] 297.39 bound 511
[runlim] sample:		299.2 time, 300.3 real, 4043.9 MB
[runlim] sample:		309.2 time, 310.3 real, 2112.4 MB
[runlim] sample:		319.2 time, 320.3 real, 1744.6 MB
c [blimc] 324.27 bound 512
c [blimc] 324.87 bound 513
c [blimc] 325.49 bound 514
c [blimc] 326.10 bound 515
c [blimc] 326.72 bound 516
c [blimc] 327.33 bound 517
c [blimc] 327.97 bound 518
c [blimc] 328.59 bound 519
[runlim] sample:		329.2 time, 330.3 real, 1388.5 MB
c [blimc] 329.23 bound 520
c [blimc] 329.88 bound 521
c [blimc] 330.53 bound 522
c [blimc] 331.17 bound 523
c [blimc] 331.83 bound 524
c [blimc] 332.48 bound 525
c [blimc] 333.15 bound 526
c [blimc] 333.80 bound 527
c [blimc] 334.46 bound 528
c [blimc] 335.12 bound 529
c [blimc] 335.80 bound 530
c [blimc] 336.45 bound 531
c [blimc] 337.14 bound 532
c [blimc] 337.80 bound 533
c [blimc] 338.47 bound 534
c [blimc] 339.14 bound 535
[runlim] sample:		339.2 time, 340.3 real, 1601.9 MB
c [blimc] 339.84 bound 536
c [blimc] 340.52 bound 537
c [blimc] 341.21 bound 538
c [blimc] 341.89 bound 539
c [blimc] 342.59 bound 540
c [blimc] 343.28 bound 541
c [blimc] 343.98 bound 542
c [blimc] 344.68 bound 543
c [blimc] 345.40 bound 544
c [blimc] 346.10 bound 545
c [blimc] 346.82 bound 546
c [blimc] 347.52 bound 547
c [blimc] 348.25 bound 548
c [blimc] 348.96 bound 549
[runlim] sample:		349.1 time, 350.3 real, 1725.6 MB
c [blimc] 349.69 bound 550
c [blimc] 350.41 bound 551
c [blimc] 351.15 bound 552
c [blimc] 351.88 bound 553
c [blimc] 352.62 bound 554
c [blimc] 353.35 bound 555
c [blimc] 354.10 bound 556
c [blimc] 354.84 bound 557
c [blimc] 355.60 bound 558
c [blimc] 356.35 bound 559
c [blimc] 357.12 bound 560
c [blimc] 357.88 bound 561
c [blimc] 358.65 bound 562
[runlim] sample:		359.1 time, 360.3 real, 2008.3 MB
c [blimc] 359.41 bound 563
c [blimc] 360.19 bound 564
c [blimc] 360.96 bound 565
c [blimc] 361.74 bound 566
c [blimc] 362.52 bound 567
c [blimc] 363.31 bound 568
c [blimc] 364.11 bound 569
c [blimc] 364.91 bound 570
c [blimc] 365.70 bound 571
c [blimc] 366.50 bound 572
c [blimc] 367.30 bound 573
c [blimc] 368.11 bound 574
c [blimc] 368.91 bound 575
[runlim] sample:		369.1 time, 370.3 real, 1923.8 MB
c [blimc] 369.72 bound 576
c [blimc] 370.53 bound 577
c [blimc] 371.35 bound 578
c [blimc] 372.16 bound 579
c [blimc] 372.99 bound 580
c [blimc] 373.81 bound 581
c [blimc] 374.65 bound 582
c [blimc] 375.47 bound 583
c [blimc] 376.32 bound 584
c [blimc] 377.15 bound 585
c [blimc] 378.00 bound 586
c [blimc] 378.84 bound 587
[runlim] sample:		379.1 time, 380.3 real, 2088.1 MB
c [blimc] 379.70 bound 588
c [blimc] 380.54 bound 589
c [blimc] 381.40 bound 590
c [blimc] 382.25 bound 591
c [blimc] 383.12 bound 592
c [blimc] 383.98 bound 593
c [blimc] 384.86 bound 594
c [blimc] 385.72 bound 595
c [blimc] 386.60 bound 596
c [blimc] 387.48 bound 597
c [blimc] 388.37 bound 598
[runlim] sample:		389.1 time, 390.3 real, 2405.1 MB
c [blimc] 389.24 bound 599
c [blimc] 390.14 bound 600
c [blimc] 391.03 bound 601
c [blimc] 391.93 bound 602
c [blimc] 392.82 bound 603
c [blimc] 393.73 bound 604
c [blimc] 394.63 bound 605
c [blimc] 395.58 bound 606
c [blimc] 396.48 bound 607
c [blimc] 397.41 bound 608
c [blimc] 398.32 bound 609
[runlim] sample:		399.1 time, 400.3 real, 2610.6 MB
c [blimc] 399.24 bound 610
c [blimc] 400.16 bound 611
c [blimc] 401.09 bound 612
c [blimc] 402.02 bound 613
c [blimc] 402.97 bound 614
c [blimc] 403.92 bound 615
c [blimc] 404.87 bound 616
c [blimc] 405.81 bound 617
c [blimc] 406.76 bound 618
c [blimc] 407.70 bound 619
c [blimc] 408.66 bound 620
[runlim] sample:		409.0 time, 410.3 real, 2644.8 MB
c [blimc] 409.61 bound 621
c [blimc] 410.58 bound 622
c [blimc] 411.53 bound 623
c [blimc] 412.50 bound 624
c [blimc] 413.46 bound 625
c [blimc] 414.44 bound 626
c [blimc] 415.41 bound 627
c [blimc] 416.40 bound 628
c [blimc] 417.37 bound 629
c [blimc] 418.37 bound 630
[runlim] sample:		419.0 time, 420.3 real, 2794.0 MB
c [blimc] 419.35 bound 631
c [blimc] 420.37 bound 632
c [blimc] 421.36 bound 633
c [blimc] 422.41 bound 634
c [blimc] 423.41 bound 635
c [blimc] 424.42 bound 636
c [blimc] 425.42 bound 637
c [blimc] 426.44 bound 638
c [blimc] 427.45 bound 639
c [blimc] 428.47 bound 640
[runlim] sample:		429.0 time, 430.3 real, 3069.1 MB
c [blimc] 429.49 bound 641
c [blimc] 430.52 bound 642
c [blimc] 431.55 bound 643
c [blimc] 432.59 bound 644
c [blimc] 433.62 bound 645
c [blimc] 434.66 bound 646
c [blimc] 435.69 bound 647
c [blimc] 436.75 bound 648
c [blimc] 437.79 bound 649
c [blimc] 438.84 bound 650
[runlim] sample:		439.0 time, 440.3 real, 2448.4 MB
c [blimc] 439.90 bound 651
c [blimc] 440.96 bound 652
c [blimc] 442.01 bound 653
c [blimc] 443.08 bound 654
c [blimc] 444.14 bound 655
c [blimc] 445.22 bound 656
c [blimc] 446.29 bound 657
c [blimc] 447.38 bound 658
c [blimc] 448.45 bound 659
[runlim] sample:		449.0 time, 450.3 real, 3264.2 MB
c [blimc] 449.55 bound 660
c [blimc] 450.63 bound 661
c [blimc] 451.73 bound 662
c [blimc] 452.82 bound 663
c [blimc] 453.92 bound 664
c [blimc] 455.01 bound 665
c [blimc] 456.12 bound 666
c [blimc] 457.22 bound 667
c [blimc] 458.34 bound 668
[runlim] sample:		458.9 time, 460.3 real, 3358.4 MB
c [blimc] 459.45 bound 669
c [blimc] 460.58 bound 670
c [blimc] 461.69 bound 671
c [blimc] 462.82 bound 672
c [blimc] 463.94 bound 673
c [blimc] 465.08 bound 674
c [blimc] 466.21 bound 675
c [blimc] 467.35 bound 676
c [blimc] 468.49 bound 677
[runlim] sample:		468.9 time, 470.3 real, 3214.0 MB
c [blimc] 469.64 bound 678
c [blimc] 470.79 bound 679
c [blimc] 471.95 bound 680
c [blimc] 473.10 bound 681
c [blimc] 474.26 bound 682
c [blimc] 475.42 bound 683
c [blimc] 476.59 bound 684
c [blimc] 477.75 bound 685
[runlim] sample:		478.9 time, 480.3 real, 2634.3 MB
c [blimc] 478.93 bound 686
c [blimc] 480.10 bound 687
c [blimc] 481.29 bound 688
c [blimc] 482.47 bound 689
c [blimc] 483.66 bound 690
c [blimc] 484.85 bound 691
c [blimc] 486.04 bound 692
c [blimc] 487.23 bound 693
c [blimc] 488.43 bound 694
[runlim] sample:		488.9 time, 490.3 real, 3300.7 MB
c [blimc] 489.63 bound 695
c [blimc] 490.84 bound 696
c [blimc] 492.04 bound 697
c [blimc] 493.25 bound 698
c [blimc] 494.46 bound 699
c [blimc] 495.68 bound 700
c [blimc] 496.90 bound 701
c [blimc] 498.13 bound 702
[runlim] sample:		498.9 time, 500.3 real, 3709.8 MB
c [blimc] 499.35 bound 703
c [blimc] 500.60 bound 704
c [blimc] 501.83 bound 705
c [blimc] 503.07 bound 706
c [blimc] 504.30 bound 707
c [blimc] 505.55 bound 708
c [blimc] 506.79 bound 709
c [blimc] 508.04 bound 710
[runlim] sample:		508.8 time, 510.3 real, 3794.8 MB
c [blimc] 509.29 bound 711
c [blimc] 510.56 bound 712
c [blimc] 511.81 bound 713
c [blimc] 513.08 bound 714
c [blimc] 514.34 bound 715
c [blimc] 515.61 bound 716
c [blimc] 516.88 bound 717
c [blimc] 518.16 bound 718
[runlim] sample:		518.8 time, 520.3 real, 3879.9 MB
c [blimc] 519.43 bound 719
c [blimc] 520.72 bound 720
c [blimc] 522.00 bound 721
c [blimc] 523.30 bound 722
c [blimc] 524.58 bound 723
c [blimc] 525.88 bound 724
c [blimc] 527.17 bound 725
c [blimc] 528.49 bound 726
[runlim] sample:		528.8 time, 530.3 real, 3035.4 MB
c [blimc] 529.79 bound 727
c [blimc] 531.11 bound 728
c [blimc] 532.42 bound 729
c [blimc] 533.74 bound 730
c [blimc] 535.05 bound 731
c [blimc] 536.38 bound 732
c [blimc] 537.69 bound 733
[runlim] sample:		538.8 time, 540.3 real, 4036.7 MB
c [blimc] 539.03 bound 734
c [blimc] 540.35 bound 735
c [blimc] 541.70 bound 736
c [blimc] 543.03 bound 737
c [blimc] 544.37 bound 738
c [blimc] 545.71 bound 739
c [blimc] 547.06 bound 740
c [blimc] 548.41 bound 741
[runlim] sample:		548.7 time, 550.3 real, 3178.7 MB
c [blimc] 549.78 bound 742
c [blimc] 551.13 bound 743
c [blimc] 552.50 bound 744
c [blimc] 553.85 bound 745
c [blimc] 555.23 bound 746
c [blimc] 556.59 bound 747
c [blimc] 557.97 bound 748
[runlim] sample:		558.7 time, 560.3 real, 4193.9 MB
c [blimc] 559.34 bound 749
c [blimc] 560.73 bound 750
c [blimc] 562.11 bound 751
c [blimc] 563.53 bound 752
c [blimc] 564.91 bound 753
c [blimc] 566.31 bound 754
c [blimc] 567.70 bound 755
[runlim] sample:		568.7 time, 570.3 real, 4334.1 MB
c [blimc] 569.11 bound 756
c [blimc] 570.51 bound 757
c [blimc] 571.93 bound 758
c [blimc] 573.34 bound 759
c [blimc] 574.75 bound 760
c [blimc] 576.16 bound 761
c [blimc] 577.59 bound 762
[runlim] sample:		578.7 time, 580.3 real, 4408.4 MB
c [blimc] 579.01 bound 763
c [blimc] 580.55 bound 764
c [blimc] 581.98 bound 765
c [blimc] 583.42 bound 766
c [blimc] 584.85 bound 767
c [blimc] 586.30 bound 768
c [blimc] 587.74 bound 769
[runlim] sample:		588.6 time, 590.3 real, 4756.4 MB
c [blimc] 589.19 bound 770
c [blimc] 590.65 bound 771
c [blimc] 592.11 bound 772
c [blimc] 593.56 bound 773
c [blimc] 595.02 bound 774
c [blimc] 596.48 bound 775
c [blimc] 597.95 bound 776
[runlim] sample:		598.6 time, 600.3 real, 4661.4 MB
c [blimc] 599.42 bound 777
c [blimc] 600.90 bound 778
c [blimc] 602.37 bound 779
c [blimc] 603.86 bound 780
c [blimc] 605.34 bound 781
c [blimc] 606.83 bound 782
c [blimc] 608.31 bound 783
[runlim] sample:		608.6 time, 610.3 real, 3554.5 MB
c [blimc] 609.82 bound 784
c [blimc] 611.30 bound 785
c [blimc] 612.81 bound 786
c [blimc] 614.31 bound 787
c [blimc] 615.82 bound 788
c [blimc] 617.32 bound 789
[runlim] sample:		618.6 time, 620.3 real, 4966.9 MB
c [blimc] 618.84 bound 790
c [blimc] 620.36 bound 791
c [blimc] 621.89 bound 792
c [blimc] 623.41 bound 793
c [blimc] 624.94 bound 794
c [blimc] 626.46 bound 795
c [blimc] 628.00 bound 796
[runlim] sample:		628.5 time, 630.3 real, 4365.1 MB
c [blimc] 629.53 bound 797
c [blimc] 631.08 bound 798
c [blimc] 632.62 bound 799
c [blimc] 634.17 bound 800
c [blimc] 635.71 bound 801
c [blimc] 637.27 bound 802
[runlim] sample:		638.5 time, 640.3 real, 5101.8 MB
c [blimc] 638.82 bound 803
c [blimc] 640.38 bound 804
c [blimc] 641.94 bound 805
c [blimc] 643.51 bound 806
c [blimc] 645.07 bound 807
c [blimc] 646.65 bound 808
c [blimc] 648.23 bound 809
[runlim] sample:		648.5 time, 650.3 real, 3651.2 MB
c [blimc] 649.82 bound 810
c [blimc] 651.39 bound 811
c [blimc] 652.98 bound 812
c [blimc] 654.57 bound 813
c [blimc] 656.17 bound 814
c [blimc] 657.75 bound 815
[runlim] sample:		658.5 time, 660.3 real, 5020.8 MB
c [blimc] 659.36 bound 816
c [blimc] 660.95 bound 817
c [blimc] 662.56 bound 818
c [blimc] 664.16 bound 819
c [blimc] 665.78 bound 820
c [blimc] 667.39 bound 821
[runlim] sample:		668.5 time, 670.3 real, 5342.5 MB
c [blimc] 669.01 bound 822
c [blimc] 670.63 bound 823
c [blimc] 672.26 bound 824
c [blimc] 673.88 bound 825
c [blimc] 675.52 bound 826
c [blimc] 677.15 bound 827
[runlim] sample:		678.4 time, 680.3 real, 5405.3 MB
c [blimc] 678.79 bound 828
c [blimc] 680.42 bound 829
c [blimc] 682.07 bound 830
c [blimc] 683.72 bound 831
c [blimc] 685.38 bound 832
c [blimc] 687.02 bound 833
[runlim] sample:		688.4 time, 690.3 real, 5468.2 MB
c [blimc] 688.68 bound 834
c [blimc] 690.34 bound 835
c [blimc] 692.02 bound 836
c [blimc] 693.68 bound 837
c [blimc] 695.36 bound 838
c [blimc] 697.03 bound 839
[runlim] sample:		698.4 time, 700.3 real, 5531.0 MB
c [blimc] 698.71 bound 840
c [blimc] 700.38 bound 841
c [blimc] 702.07 bound 842
c [blimc] 703.75 bound 843
c [blimc] 705.45 bound 844
c [blimc] 707.14 bound 845
[runlim] sample:		708.4 time, 710.3 real, 5593.9 MB
c [blimc] 708.84 bound 846
c [blimc] 710.54 bound 847
c [blimc] 712.25 bound 848
c [blimc] 713.95 bound 849
c [blimc] 715.66 bound 850
c [blimc] 717.37 bound 851
[runlim] sample:		718.3 time, 720.3 real, 5656.7 MB
c [blimc] 719.10 bound 852
c [blimc] 720.81 bound 853
c [blimc] 722.54 bound 854
c [blimc] 724.26 bound 855
c [blimc] 726.00 bound 856
c [blimc] 727.72 bound 857
[runlim] sample:		728.3 time, 730.3 real, 4783.4 MB
c [blimc] 729.47 bound 858
c [blimc] 731.20 bound 859
c [blimc] 732.95 bound 860
c [blimc] 734.69 bound 861
c [blimc] 736.45 bound 862
c [blimc] 738.19 bound 863
[runlim] sample:		738.3 time, 740.3 real, 3933.2 MB
c [blimc] 739.96 bound 864
c [blimc] 741.72 bound 865
c [blimc] 743.51 bound 866
c [blimc] 745.28 bound 867
c [blimc] 747.07 bound 868
[runlim] sample:		748.2 time, 750.3 real, 5834.9 MB
c [blimc] 748.84 bound 869
c [blimc] 750.64 bound 870
c [blimc] 752.42 bound 871
c [blimc] 754.21 bound 872
c [blimc] 755.99 bound 873
c [blimc] 757.78 bound 874
[runlim] sample:		758.2 time, 760.3 real, 4412.6 MB
c [blimc] 759.58 bound 875
c [blimc] 761.38 bound 876
c [blimc] 763.17 bound 877
c [blimc] 764.99 bound 878
c [blimc] 766.79 bound 879
[runlim] sample:		768.2 time, 770.3 real, 5949.8 MB
c [blimc] 768.61 bound 880
c [blimc] 770.43 bound 881
c [blimc] 772.26 bound 882
c [blimc] 774.07 bound 883
c [blimc] 775.91 bound 884
c [blimc] 777.73 bound 885
[runlim] sample:		778.2 time, 780.3 real, 4435.9 MB
c [blimc] 779.59 bound 886
c [blimc] 781.41 bound 887
c [blimc] 783.26 bound 888
c [blimc] 785.09 bound 889
c [blimc] 786.95 bound 890
[runlim] sample:		788.1 time, 790.3 real, 6065.2 MB
c [blimc] 788.79 bound 891
c [blimc] 790.66 bound 892
c [blimc] 792.51 bound 893
c [blimc] 794.38 bound 894
c [blimc] 796.23 bound 895
[runlim] sample:		798.1 time, 800.3 real, 4134.0 MB
c [blimc] 798.24 bound 896
c [blimc] 800.19 bound 897
c [blimc] 802.24 bound 898
c [blimc] 804.12 bound 899
c [blimc] 806.01 bound 900
c [blimc] 807.88 bound 901
[runlim] sample:		808.1 time, 810.3 real, 4318.9 MB
c [blimc] 809.79 bound 902
c [blimc] 811.67 bound 903
c [blimc] 813.56 bound 904
c [blimc] 815.45 bound 905
c [blimc] 817.35 bound 906
[runlim] sample:		818.0 time, 820.3 real, 5453.5 MB
c [blimc] 819.25 bound 907
s UNKNOWN
c [blimc]
c [blimc] CAUGHT SIGNAL 15
c [blimc]
c [lgl907]   56.877  14% simplifying
c [lgl907]    0.000   0% search
c [lgl907] ==================================
c [lgl907]  414.318 100% all
c [lgl907] 
c [lgl907]             0 conflicts,           0.0 confs/sec
c [lgl907]             0 ternaries,           0.0 confs/ternary
c [lgl907]             0 binaries,            0.0 confs/binary
c [lgl907]             0 iterations,          0.0 confs/iteration
c [lgl907] 
c [lgl907]             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c [lgl907]             0 restarts,            0.0 rests/sec,      0.0 confs/restart
c [lgl907]             0 decisions,           0.0 decis/sec,      0.0 decis/conflict
c [lgl907]      40863096 propagations,    98627.4 props/sec,      0.0 props/decision
c [lgl907] 
c [lgl907] 414.3 seconds, 7130.2 MB
c [blimc] 820.65 reached k = 907
c [blimc] 820.65 cloned 0 solvers
c [blimc] 820.65 max 7135.7 MB
c [blimc]
c [blimc] CAUGHT SIGNAL 15
c [blimc]
[runlim] end:			Mon Sep 21 02:14:05 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		0
[runlim] real:			823.27 seconds
[runlim] time:			820.89 seconds
[runlim] space:			7025.4 MB
[runlim] samples:		8229
