[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/oski15/submission/single/oski15a14b14s.aig
[runlim] start:			Thu Sep 17 12:20:10 2015
[runlim] main pid:		29645
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/oski15/submission/single/oski15a14b14s.aig
c [blimc] 0.01 MILOA 47456 1071 3519 1 42866
c [blimc] 0.01 BCJK 0 0 0 0 42866
c [blimc] 0.01 3519 latches initialized to 0
c [blimc] 0.01 0 latches initialized to 1
c [blimc] 0.01 0 latches uninitialized
c [blimc] 0.01 literals  in COI:      37266 =  79% out of 47456
c [blimc] 0.01 inputs    in COI:       1022 =  95% out of 1071
c [blimc] 0.01 latches   in COI:       3449 =  98% out of 3519
c [blimc] 0.01 constants in COI:          1 = 100% out of 1
c [blimc] 0.01 ands      in COI:      32794 =  77% out of 42866
c [blimc] 0.04 encoded
c [blimc] 6.36 simplified
c [blimc] 6.37 extracted
c [lglopt]    6.319 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]    6.320 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]        410194 propagations,    64908.6 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 6.3 seconds, 14.8 MB
c [blimc] 6.38 mapped 11391 variables
c [blimc] 6.38 maxk 1000
c [blimc] 6.38 bound 0
c [blimc] 6.43 bound 1
c [blimc] 6.81 bound 2
c [blimc] 6.83 bound 3
c [blimc] 8.36 bound 4
c [blimc] 8.38 bound 5
[runlim] sample:		10.0 time, 10.3 real, 25.5 MB
c [blimc] 11.51 bound 6
c [blimc] 11.54 bound 7
c [blimc] 11.56 bound 8
c [blimc] 14.59 bound 9
c [blimc] 14.62 bound 10
c [blimc] 14.65 bound 11
c [blimc] 14.68 bound 12
[runlim] sample:		20.0 time, 20.3 real, 79.9 MB
c [blimc] 23.25 bound 13
c [blimc] 23.28 bound 14
c [blimc] 23.31 bound 15
c [blimc] 23.34 bound 16
c [blimc] 23.37 bound 17
c [blimc] 23.41 bound 18
c [blimc] 29.89 bound 19
c [blimc] 29.93 bound 20
c [blimc] 29.96 bound 21
[runlim] sample:		30.0 time, 30.3 real, 84.1 MB
c [blimc] 29.99 bound 22
c [blimc] 30.03 bound 23
c [blimc] 30.07 bound 24
c [blimc] 30.11 bound 25
c [blimc] 30.15 bound 26
c [blimc] 30.19 bound 27
c [blimc] 30.23 bound 28
[runlim] sample:		40.0 time, 40.3 real, 193.6 MB
c [blimc] 48.15 bound 29
c [blimc] 48.20 bound 30
c [blimc] 48.24 bound 31
c [blimc] 48.28 bound 32
c [blimc] 48.32 bound 33
c [blimc] 48.35 bound 34
c [blimc] 48.40 bound 35
c [blimc] 48.44 bound 36
c [blimc] 48.49 bound 37
c [blimc] 48.53 bound 38
c [blimc] 48.58 bound 39
c [blimc] 48.63 bound 40
c [blimc] 48.68 bound 41
c [blimc] 48.73 bound 42
c [blimc] 48.78 bound 43
[runlim] sample:		50.0 time, 50.3 real, 187.6 MB
[runlim] sample:		59.9 time, 60.3 real, 277.6 MB
c [blimc] 64.69 bound 44
c [blimc] 64.75 bound 45
c [blimc] 64.80 bound 46
c [blimc] 64.86 bound 47
c [blimc] 64.91 bound 48
c [blimc] 64.96 bound 49
c [blimc] 65.01 bound 50
c [blimc] 65.06 bound 51
c [blimc] 65.11 bound 52
c [blimc] 65.16 bound 53
c [blimc] 65.22 bound 54
c [blimc] 65.27 bound 55
c [blimc] 65.33 bound 56
c [blimc] 65.38 bound 57
c [blimc] 65.44 bound 58
c [blimc] 65.50 bound 59
c [blimc] 65.56 bound 60
c [blimc] 65.62 bound 61
c [blimc] 65.68 bound 62
c [blimc] 65.75 bound 63
c [blimc] 65.82 bound 64
c [blimc] 65.88 bound 65
c [blimc] 65.94 bound 66
c [blimc] 66.01 bound 67
[runlim] sample:		69.9 time, 70.3 real, 252.6 MB
c [blimc] 78.67 bound 68
c [blimc] 78.75 bound 69
c [blimc] 78.82 bound 70
c [blimc] 78.88 bound 71
c [blimc] 78.95 bound 72
c [blimc] 79.02 bound 73
c [blimc] 79.09 bound 74
c [blimc] 79.16 bound 75
c [blimc] 79.24 bound 76
c [blimc] 79.31 bound 77
c [blimc] 79.38 bound 78
c [blimc] 79.45 bound 79
c [blimc] 79.52 bound 80
c [blimc] 79.59 bound 81
c [blimc] 79.66 bound 82
c [blimc] 79.74 bound 83
c [blimc] 79.82 bound 84
c [blimc] 79.90 bound 85
[runlim] sample:		79.9 time, 80.3 real, 335.7 MB
c [blimc] 79.98 bound 86
c [blimc] 80.06 bound 87
c [blimc] 80.14 bound 88
c [blimc] 80.22 bound 89
c [blimc] 80.30 bound 90
c [blimc] 80.39 bound 91
c [blimc] 80.47 bound 92
c [blimc] 80.57 bound 93
c [blimc] 80.65 bound 94
c [blimc] 80.74 bound 95
c [blimc] 80.83 bound 96
c [blimc] 80.93 bound 97
c [blimc] 81.02 bound 98
c [blimc] 81.11 bound 99
c [blimc] 81.21 bound 100
c [blimc] 81.30 bound 101
c [blimc] 81.39 bound 102
c [blimc] 81.48 bound 103
c [blimc] 81.57 bound 104
[runlim] sample:		89.9 time, 90.3 real, 458.1 MB
c [blimc] 98.49 bound 105
c [blimc] 98.59 bound 106
c [blimc] 98.69 bound 107
c [blimc] 98.79 bound 108
c [blimc] 98.88 bound 109
c [blimc] 98.97 bound 110
c [blimc] 99.07 bound 111
c [blimc] 99.16 bound 112
c [blimc] 99.25 bound 113
c [blimc] 99.34 bound 114
c [blimc] 99.43 bound 115
c [blimc] 99.52 bound 116
c [blimc] 99.62 bound 117
c [blimc] 99.71 bound 118
c [blimc] 99.80 bound 119
[runlim] sample:		99.9 time, 100.3 real, 535.8 MB
c [blimc] 99.90 bound 120
c [blimc] 100.00 bound 121
c [blimc] 100.10 bound 122
c [blimc] 100.20 bound 123
c [blimc] 100.30 bound 124
c [blimc] 100.39 bound 125
c [blimc] 100.49 bound 126
c [blimc] 100.59 bound 127
c [blimc] 100.70 bound 128
c [blimc] 100.80 bound 129
c [blimc] 100.90 bound 130
c [blimc] 101.00 bound 131
c [blimc] 101.11 bound 132
c [blimc] 101.21 bound 133
c [blimc] 101.31 bound 134
c [blimc] 101.42 bound 135
c [blimc] 101.53 bound 136
c [blimc] 101.63 bound 137
c [blimc] 101.74 bound 138
c [blimc] 101.85 bound 139
c [blimc] 101.96 bound 140
c [blimc] 102.07 bound 141
c [blimc] 102.18 bound 142
c [blimc] 102.29 bound 143
c [blimc] 102.40 bound 144
c [blimc] 102.51 bound 145
c [blimc] 102.63 bound 146
c [blimc] 102.74 bound 147
c [blimc] 102.86 bound 148
c [blimc] 102.97 bound 149
c [blimc] 103.09 bound 150
c [blimc] 103.22 bound 151
c [blimc] 103.34 bound 152
c [blimc] 103.45 bound 153
c [blimc] 103.57 bound 154
c [blimc] 103.69 bound 155
c [blimc] 103.81 bound 156
c [blimc] 103.93 bound 157
c [blimc] 104.07 bound 158
c [blimc] 104.19 bound 159
c [blimc] 104.31 bound 160
c [blimc] 104.44 bound 161
c [blimc] 104.56 bound 162
[runlim] sample:		109.9 time, 110.3 real, 607.5 MB
[runlim] sample:		119.8 time, 120.3 real, 701.4 MB
c [blimc] 124.97 bound 163
c [blimc] 125.11 bound 164
c [blimc] 125.25 bound 165
c [blimc] 125.39 bound 166
c [blimc] 125.51 bound 167
c [blimc] 125.63 bound 168
c [blimc] 125.75 bound 169
c [blimc] 125.88 bound 170
c [blimc] 126.00 bound 171
c [blimc] 126.12 bound 172
c [blimc] 126.24 bound 173
c [blimc] 126.37 bound 174
c [blimc] 126.50 bound 175
c [blimc] 126.62 bound 176
c [blimc] 126.75 bound 177
c [blimc] 126.87 bound 178
c [blimc] 127.01 bound 179
c [blimc] 127.13 bound 180
c [blimc] 127.26 bound 181
c [blimc] 127.39 bound 182
c [blimc] 127.52 bound 183
c [blimc] 127.65 bound 184
c [blimc] 127.81 bound 185
c [blimc] 127.95 bound 186
c [blimc] 128.08 bound 187
c [blimc] 128.21 bound 188
c [blimc] 128.35 bound 189
c [blimc] 128.48 bound 190
c [blimc] 128.62 bound 191
c [blimc] 128.76 bound 192
c [blimc] 128.90 bound 193
c [blimc] 129.04 bound 194
c [blimc] 129.18 bound 195
c [blimc] 129.32 bound 196
c [blimc] 129.46 bound 197
c [blimc] 129.60 bound 198
c [blimc] 129.75 bound 199
[runlim] sample:		129.8 time, 130.3 real, 913.0 MB
c [blimc] 129.89 bound 200
c [blimc] 130.04 bound 201
c [blimc] 130.18 bound 202
c [blimc] 130.33 bound 203
c [blimc] 130.47 bound 204
c [blimc] 130.62 bound 205
c [blimc] 130.77 bound 206
c [blimc] 130.92 bound 207
c [blimc] 131.06 bound 208
c [blimc] 131.21 bound 209
c [blimc] 131.36 bound 210
c [blimc] 131.51 bound 211
c [blimc] 131.67 bound 212
c [blimc] 131.82 bound 213
c [blimc] 131.97 bound 214
c [blimc] 132.13 bound 215
c [blimc] 132.28 bound 216
c [blimc] 132.44 bound 217
c [blimc] 132.59 bound 218
c [blimc] 132.75 bound 219
c [blimc] 132.91 bound 220
c [blimc] 133.08 bound 221
c [blimc] 133.24 bound 222
c [blimc] 133.40 bound 223
c [blimc] 133.56 bound 224
c [blimc] 133.73 bound 225
c [blimc] 133.89 bound 226
c [blimc] 134.05 bound 227
c [blimc] 134.22 bound 228
c [blimc] 134.38 bound 229
c [blimc] 134.55 bound 230
c [blimc] 134.71 bound 231
c [blimc] 134.88 bound 232
c [blimc] 135.05 bound 233
c [blimc] 135.22 bound 234
c [blimc] 135.39 bound 235
c [blimc] 135.56 bound 236
c [blimc] 135.73 bound 237
c [blimc] 135.90 bound 238
c [blimc] 136.07 bound 239
c [blimc] 136.24 bound 240
c [blimc] 136.42 bound 241
c [blimc] 136.59 bound 242
c [blimc] 136.77 bound 243
c [blimc] 136.94 bound 244
c [blimc] 137.12 bound 245
c [blimc] 137.30 bound 246
c [blimc] 137.48 bound 247
c [blimc] 137.65 bound 248
c [blimc] 137.83 bound 249
c [blimc] 138.02 bound 250
c [blimc] 138.20 bound 251
c [blimc] 138.39 bound 252
c [blimc] 138.57 bound 253
c [blimc] 138.75 bound 254
[runlim] sample:		139.8 time, 140.3 real, 827.9 MB
[runlim] sample:		149.8 time, 150.3 real, 940.6 MB
[runlim] sample:		159.8 time, 160.3 real, 890.0 MB
c [blimc] 164.95 bound 255
c [blimc] 165.20 bound 256
c [blimc] 165.38 bound 257
c [blimc] 165.55 bound 258
c [blimc] 165.73 bound 259
c [blimc] 165.90 bound 260
c [blimc] 166.08 bound 261
c [blimc] 166.25 bound 262
c [blimc] 166.43 bound 263
c [blimc] 166.61 bound 264
c [blimc] 166.78 bound 265
c [blimc] 166.96 bound 266
c [blimc] 167.14 bound 267
c [blimc] 167.32 bound 268
c [blimc] 167.51 bound 269
c [blimc] 167.69 bound 270
c [blimc] 167.87 bound 271
c [blimc] 168.05 bound 272
c [blimc] 168.24 bound 273
c [blimc] 168.42 bound 274
c [blimc] 168.61 bound 275
c [blimc] 168.80 bound 276
c [blimc] 168.98 bound 277
c [blimc] 169.17 bound 278
c [blimc] 169.36 bound 279
c [blimc] 169.55 bound 280
c [blimc] 169.74 bound 281
[runlim] sample:		169.8 time, 170.3 real, 987.0 MB
c [blimc] 169.93 bound 282
c [blimc] 170.13 bound 283
c [blimc] 170.32 bound 284
c [blimc] 170.51 bound 285
c [blimc] 170.71 bound 286
c [blimc] 170.90 bound 287
c [blimc] 171.10 bound 288
c [blimc] 171.29 bound 289
c [blimc] 171.49 bound 290
c [blimc] 171.69 bound 291
c [blimc] 171.89 bound 292
c [blimc] 172.10 bound 293
c [blimc] 172.32 bound 294
c [blimc] 172.52 bound 295
c [blimc] 172.72 bound 296
c [blimc] 172.92 bound 297
c [blimc] 173.12 bound 298
c [blimc] 173.33 bound 299
c [blimc] 173.54 bound 300
c [blimc] 173.75 bound 301
c [blimc] 173.96 bound 302
c [blimc] 174.17 bound 303
c [blimc] 174.38 bound 304
c [blimc] 174.58 bound 305
c [blimc] 174.79 bound 306
c [blimc] 175.00 bound 307
c [blimc] 175.21 bound 308
c [blimc] 175.42 bound 309
c [blimc] 175.63 bound 310
c [blimc] 175.84 bound 311
c [blimc] 176.06 bound 312
c [blimc] 176.27 bound 313
c [blimc] 176.48 bound 314
c [blimc] 176.70 bound 315
c [blimc] 176.91 bound 316
c [blimc] 177.13 bound 317
c [blimc] 177.34 bound 318
c [blimc] 177.56 bound 319
c [blimc] 177.78 bound 320
c [blimc] 178.00 bound 321
c [blimc] 178.22 bound 322
c [blimc] 178.44 bound 323
c [blimc] 178.66 bound 324
c [blimc] 178.88 bound 325
c [blimc] 179.10 bound 326
c [blimc] 179.33 bound 327
c [blimc] 179.55 bound 328
[runlim] sample:		179.7 time, 180.3 real, 1333.9 MB
c [blimc] 179.77 bound 329
c [blimc] 180.00 bound 330
c [blimc] 180.23 bound 331
c [blimc] 180.46 bound 332
c [blimc] 180.68 bound 333
c [blimc] 180.91 bound 334
c [blimc] 181.14 bound 335
c [blimc] 181.37 bound 336
c [blimc] 181.60 bound 337
c [blimc] 181.83 bound 338
c [blimc] 182.06 bound 339
c [blimc] 182.30 bound 340
c [blimc] 182.53 bound 341
c [blimc] 182.77 bound 342
c [blimc] 183.00 bound 343
c [blimc] 183.24 bound 344
c [blimc] 183.47 bound 345
c [blimc] 183.71 bound 346
c [blimc] 183.95 bound 347
c [blimc] 184.18 bound 348
c [blimc] 184.43 bound 349
c [blimc] 184.67 bound 350
c [blimc] 184.91 bound 351
c [blimc] 185.15 bound 352
c [blimc] 185.39 bound 353
c [blimc] 185.63 bound 354
c [blimc] 185.88 bound 355
c [blimc] 186.12 bound 356
c [blimc] 186.37 bound 357
c [blimc] 186.61 bound 358
c [blimc] 186.86 bound 359
c [blimc] 187.11 bound 360
c [blimc] 187.35 bound 361
c [blimc] 187.60 bound 362
c [blimc] 187.85 bound 363
c [blimc] 188.10 bound 364
c [blimc] 188.35 bound 365
c [blimc] 188.61 bound 366
c [blimc] 188.86 bound 367
c [blimc] 189.11 bound 368
c [blimc] 189.39 bound 369
c [blimc] 189.64 bound 370
[runlim] sample:		189.7 time, 190.3 real, 1231.9 MB
c [blimc] 189.90 bound 371
c [blimc] 190.15 bound 372
c [blimc] 190.41 bound 373
c [blimc] 190.67 bound 374
c [blimc] 190.92 bound 375
c [blimc] 191.18 bound 376
c [blimc] 191.44 bound 377
c [blimc] 191.70 bound 378
c [blimc] 191.96 bound 379
c [blimc] 192.22 bound 380
c [blimc] 192.48 bound 381
c [blimc] 192.75 bound 382
c [blimc] 193.01 bound 383
c [blimc] 193.27 bound 384
c [blimc] 193.54 bound 385
c [blimc] 193.80 bound 386
c [blimc] 194.07 bound 387
c [blimc] 194.34 bound 388
c [blimc] 194.61 bound 389
c [blimc] 194.88 bound 390
c [blimc] 195.15 bound 391
c [blimc] 195.42 bound 392
c [blimc] 195.69 bound 393
c [blimc] 195.96 bound 394
c [blimc] 196.23 bound 395
c [blimc] 196.51 bound 396
c [blimc] 196.78 bound 397
c [blimc] 197.07 bound 398
c [blimc] 197.36 bound 399
c [blimc] 197.64 bound 400
[runlim] sample:		199.7 time, 200.3 real, 1165.6 MB
[runlim] sample:		209.7 time, 210.3 real, 1307.9 MB
[runlim] sample:		219.7 time, 220.3 real, 962.9 MB
[runlim] sample:		229.6 time, 230.3 real, 1368.4 MB
[runlim] sample:		239.6 time, 240.3 real, 1326.6 MB
c [blimc] 248.15 bound 401
c [blimc] 248.49 bound 402
c [blimc] 248.78 bound 403
c [blimc] 249.04 bound 404
c [blimc] 249.29 bound 405
c [blimc] 249.55 bound 406
[runlim] sample:		249.6 time, 250.3 real, 1458.6 MB
c [blimc] 249.82 bound 407
c [blimc] 250.08 bound 408
c [blimc] 250.34 bound 409
c [blimc] 250.60 bound 410
c [blimc] 250.86 bound 411
c [blimc] 251.13 bound 412
c [blimc] 251.39 bound 413
c [blimc] 251.65 bound 414
c [blimc] 251.92 bound 415
c [blimc] 252.18 bound 416
c [blimc] 252.45 bound 417
c [blimc] 252.72 bound 418
c [blimc] 252.99 bound 419
c [blimc] 253.26 bound 420
c [blimc] 253.53 bound 421
c [blimc] 253.80 bound 422
c [blimc] 254.07 bound 423
c [blimc] 254.34 bound 424
c [blimc] 254.62 bound 425
c [blimc] 254.89 bound 426
c [blimc] 255.17 bound 427
c [blimc] 255.44 bound 428
c [blimc] 255.72 bound 429
c [blimc] 256.00 bound 430
c [blimc] 256.27 bound 431
c [blimc] 256.55 bound 432
c [blimc] 256.83 bound 433
c [blimc] 257.11 bound 434
c [blimc] 257.39 bound 435
c [blimc] 257.67 bound 436
c [blimc] 257.96 bound 437
c [blimc] 258.24 bound 438
c [blimc] 258.52 bound 439
c [blimc] 258.80 bound 440
c [blimc] 259.09 bound 441
c [blimc] 259.38 bound 442
[runlim] sample:		259.6 time, 260.3 real, 1841.6 MB
c [blimc] 259.66 bound 443
c [blimc] 259.95 bound 444
c [blimc] 260.24 bound 445
c [blimc] 260.53 bound 446
c [blimc] 260.82 bound 447
c [blimc] 261.11 bound 448
c [blimc] 261.40 bound 449
c [blimc] 261.70 bound 450
c [blimc] 261.99 bound 451
c [blimc] 262.28 bound 452
c [blimc] 262.57 bound 453
c [blimc] 262.87 bound 454
c [blimc] 263.16 bound 455
c [blimc] 263.46 bound 456
c [blimc] 263.75 bound 457
c [blimc] 264.05 bound 458
c [blimc] 264.35 bound 459
c [blimc] 264.65 bound 460
c [blimc] 264.95 bound 461
c [blimc] 265.25 bound 462
c [blimc] 265.55 bound 463
c [blimc] 265.85 bound 464
c [blimc] 266.15 bound 465
c [blimc] 266.46 bound 466
c [blimc] 266.76 bound 467
c [blimc] 267.06 bound 468
c [blimc] 267.36 bound 469
c [blimc] 267.67 bound 470
c [blimc] 267.98 bound 471
c [blimc] 268.29 bound 472
c [blimc] 268.59 bound 473
c [blimc] 268.90 bound 474
c [blimc] 269.21 bound 475
c [blimc] 269.52 bound 476
[runlim] sample:		269.6 time, 270.3 real, 1458.5 MB
c [blimc] 269.84 bound 477
c [blimc] 270.15 bound 478
c [blimc] 270.46 bound 479
c [blimc] 270.77 bound 480
c [blimc] 271.09 bound 481
c [blimc] 271.40 bound 482
c [blimc] 271.72 bound 483
c [blimc] 272.03 bound 484
c [blimc] 272.35 bound 485
c [blimc] 272.66 bound 486
c [blimc] 272.98 bound 487
c [blimc] 273.30 bound 488
c [blimc] 273.62 bound 489
c [blimc] 273.94 bound 490
c [blimc] 274.26 bound 491
c [blimc] 274.59 bound 492
c [blimc] 274.91 bound 493
c [blimc] 275.23 bound 494
c [blimc] 275.56 bound 495
c [blimc] 275.88 bound 496
c [blimc] 276.21 bound 497
c [blimc] 276.53 bound 498
c [blimc] 276.86 bound 499
c [blimc] 277.19 bound 500
c [blimc] 277.51 bound 501
c [blimc] 277.84 bound 502
c [blimc] 278.17 bound 503
c [blimc] 278.49 bound 504
c [blimc] 278.82 bound 505
c [blimc] 279.15 bound 506
c [blimc] 279.48 bound 507
[runlim] sample:		279.5 time, 280.3 real, 1521.2 MB
c [blimc] 279.82 bound 508
c [blimc] 280.15 bound 509
c [blimc] 280.48 bound 510
c [blimc] 280.81 bound 511
c [blimc] 281.18 bound 512
c [blimc] 281.51 bound 513
c [blimc] 281.85 bound 514
c [blimc] 282.18 bound 515
c [blimc] 282.52 bound 516
c [blimc] 282.86 bound 517
c [blimc] 283.20 bound 518
c [blimc] 283.55 bound 519
c [blimc] 283.89 bound 520
c [blimc] 284.23 bound 521
c [blimc] 284.57 bound 522
c [blimc] 284.92 bound 523
c [blimc] 285.26 bound 524
c [blimc] 285.61 bound 525
c [blimc] 285.96 bound 526
c [blimc] 286.30 bound 527
c [blimc] 286.65 bound 528
c [blimc] 287.00 bound 529
c [blimc] 287.35 bound 530
c [blimc] 287.70 bound 531
c [blimc] 288.05 bound 532
c [blimc] 288.40 bound 533
c [blimc] 288.75 bound 534
c [blimc] 289.11 bound 535
c [blimc] 289.46 bound 536
[runlim] sample:		289.5 time, 290.3 real, 1513.2 MB
c [blimc] 289.82 bound 537
c [blimc] 290.18 bound 538
c [blimc] 290.53 bound 539
c [blimc] 290.89 bound 540
c [blimc] 291.25 bound 541
c [blimc] 291.61 bound 542
c [blimc] 291.97 bound 543
c [blimc] 292.33 bound 544
c [blimc] 292.69 bound 545
c [blimc] 293.05 bound 546
c [blimc] 293.41 bound 547
c [blimc] 293.77 bound 548
c [blimc] 294.13 bound 549
c [blimc] 294.50 bound 550
c [blimc] 294.86 bound 551
c [blimc] 295.23 bound 552
c [blimc] 295.59 bound 553
c [blimc] 295.96 bound 554
c [blimc] 296.33 bound 555
c [blimc] 296.69 bound 556
c [blimc] 297.06 bound 557
c [blimc] 297.43 bound 558
c [blimc] 297.80 bound 559
c [blimc] 298.17 bound 560
c [blimc] 298.54 bound 561
c [blimc] 298.91 bound 562
c [blimc] 299.28 bound 563
[runlim] sample:		299.5 time, 300.3 real, 1970.0 MB
c [blimc] 299.65 bound 564
c [blimc] 300.02 bound 565
c [blimc] 300.40 bound 566
c [blimc] 300.77 bound 567
c [blimc] 301.15 bound 568
c [blimc] 301.53 bound 569
c [blimc] 301.91 bound 570
c [blimc] 302.29 bound 571
c [blimc] 302.66 bound 572
c [blimc] 303.05 bound 573
c [blimc] 303.43 bound 574
c [blimc] 303.81 bound 575
c [blimc] 304.19 bound 576
c [blimc] 304.58 bound 577
c [blimc] 304.96 bound 578
c [blimc] 305.35 bound 579
c [blimc] 305.73 bound 580
c [blimc] 306.12 bound 581
c [blimc] 306.51 bound 582
c [blimc] 306.90 bound 583
c [blimc] 307.29 bound 584
c [blimc] 307.68 bound 585
c [blimc] 308.07 bound 586
c [blimc] 308.46 bound 587
c [blimc] 308.85 bound 588
c [blimc] 309.25 bound 589
[runlim] sample:		309.4 time, 310.3 real, 1990.4 MB
c [blimc] 309.64 bound 590
c [blimc] 310.03 bound 591
c [blimc] 310.42 bound 592
c [blimc] 310.82 bound 593
c [blimc] 311.21 bound 594
c [blimc] 311.61 bound 595
c [blimc] 312.00 bound 596
c [blimc] 312.40 bound 597
c [blimc] 312.80 bound 598
c [blimc] 313.19 bound 599
c [blimc] 313.59 bound 600
c [blimc] 313.99 bound 601
c [blimc] 314.39 bound 602
c [blimc] 314.79 bound 603
c [blimc] 315.19 bound 604
c [blimc] 315.60 bound 605
c [blimc] 316.00 bound 606
c [blimc] 316.41 bound 607
c [blimc] 316.81 bound 608
c [blimc] 317.22 bound 609
c [blimc] 317.62 bound 610
c [blimc] 318.03 bound 611
c [blimc] 318.44 bound 612
c [blimc] 318.85 bound 613
c [blimc] 319.26 bound 614
[runlim] sample:		319.4 time, 320.3 real, 1899.0 MB
c [blimc] 319.68 bound 615
c [blimc] 320.09 bound 616
c [blimc] 320.50 bound 617
c [blimc] 320.91 bound 618
c [blimc] 321.32 bound 619
c [blimc] 321.73 bound 620
c [blimc] 322.15 bound 621
c [blimc] 322.56 bound 622
c [blimc] 322.98 bound 623
c [blimc] 323.40 bound 624
c [blimc] 323.82 bound 625
c [blimc] 324.24 bound 626
c [blimc] 324.66 bound 627
c [blimc] 325.08 bound 628
c [blimc] 325.52 bound 629
c [blimc] 325.94 bound 630
c [blimc] 326.37 bound 631
c [blimc] 326.79 bound 632
c [blimc] 327.22 bound 633
[runlim] sample:		329.4 time, 330.3 real, 1638.4 MB
[runlim] sample:		339.3 time, 340.3 real, 1572.7 MB
[runlim] sample:		349.3 time, 350.3 real, 1974.8 MB
[runlim] sample:		359.3 time, 360.3 real, 2519.9 MB
[runlim] sample:		369.3 time, 370.3 real, 1660.4 MB
[runlim] sample:		379.3 time, 380.3 real, 2079.0 MB
[runlim] sample:		389.3 time, 390.3 real, 2012.5 MB
[runlim] sample:		399.3 time, 400.3 real, 2374.4 MB
[runlim] sample:		409.3 time, 410.3 real, 1433.3 MB
c [blimc] 416.04 bound 634
c [blimc] 416.47 bound 635
c [blimc] 416.87 bound 636
c [blimc] 417.27 bound 637
c [blimc] 417.66 bound 638
c [blimc] 418.06 bound 639
c [blimc] 418.45 bound 640
c [blimc] 418.85 bound 641
c [blimc] 419.25 bound 642
[runlim] sample:		419.2 time, 420.3 real, 1990.4 MB
c [blimc] 419.65 bound 643
c [blimc] 420.04 bound 644
c [blimc] 420.44 bound 645
c [blimc] 420.84 bound 646
c [blimc] 421.24 bound 647
c [blimc] 421.64 bound 648
c [blimc] 422.04 bound 649
c [blimc] 422.45 bound 650
c [blimc] 422.85 bound 651
c [blimc] 423.25 bound 652
c [blimc] 423.66 bound 653
c [blimc] 424.07 bound 654
c [blimc] 424.47 bound 655
c [blimc] 424.88 bound 656
c [blimc] 425.29 bound 657
c [blimc] 425.70 bound 658
c [blimc] 426.11 bound 659
c [blimc] 426.52 bound 660
c [blimc] 426.93 bound 661
c [blimc] 427.34 bound 662
c [blimc] 427.76 bound 663
c [blimc] 428.17 bound 664
c [blimc] 428.59 bound 665
c [blimc] 429.00 bound 666
[runlim] sample:		429.2 time, 430.3 real, 2493.8 MB
c [blimc] 429.42 bound 667
c [blimc] 429.83 bound 668
c [blimc] 430.25 bound 669
c [blimc] 430.67 bound 670
c [blimc] 431.09 bound 671
c [blimc] 431.51 bound 672
c [blimc] 431.93 bound 673
c [blimc] 432.35 bound 674
c [blimc] 432.77 bound 675
c [blimc] 433.20 bound 676
c [blimc] 433.62 bound 677
c [blimc] 434.04 bound 678
c [blimc] 434.47 bound 679
c [blimc] 434.89 bound 680
c [blimc] 435.32 bound 681
c [blimc] 435.74 bound 682
c [blimc] 436.17 bound 683
c [blimc] 436.60 bound 684
c [blimc] 437.03 bound 685
c [blimc] 437.46 bound 686
c [blimc] 437.89 bound 687
c [blimc] 438.32 bound 688
c [blimc] 438.75 bound 689
c [blimc] 439.18 bound 690
[runlim] sample:		439.2 time, 440.3 real, 2053.6 MB
c [blimc] 439.62 bound 691
c [blimc] 440.05 bound 692
c [blimc] 440.48 bound 693
c [blimc] 440.91 bound 694
c [blimc] 441.35 bound 695
c [blimc] 441.78 bound 696
c [blimc] 442.22 bound 697
c [blimc] 442.65 bound 698
c [blimc] 443.09 bound 699
c [blimc] 443.53 bound 700
c [blimc] 443.96 bound 701
c [blimc] 444.40 bound 702
c [blimc] 444.84 bound 703
c [blimc] 445.28 bound 704
c [blimc] 445.72 bound 705
c [blimc] 446.16 bound 706
c [blimc] 446.61 bound 707
c [blimc] 447.05 bound 708
c [blimc] 447.49 bound 709
c [blimc] 447.93 bound 710
c [blimc] 448.38 bound 711
c [blimc] 448.83 bound 712
[runlim] sample:		449.1 time, 450.3 real, 2823.3 MB
c [blimc] 449.27 bound 713
c [blimc] 449.73 bound 714
c [blimc] 450.18 bound 715
c [blimc] 450.63 bound 716
c [blimc] 451.08 bound 717
c [blimc] 451.54 bound 718
c [blimc] 451.99 bound 719
c [blimc] 452.44 bound 720
c [blimc] 452.90 bound 721
c [blimc] 453.35 bound 722
c [blimc] 453.81 bound 723
c [blimc] 454.27 bound 724
c [blimc] 454.72 bound 725
c [blimc] 455.18 bound 726
c [blimc] 455.64 bound 727
c [blimc] 456.10 bound 728
c [blimc] 456.56 bound 729
c [blimc] 457.02 bound 730
c [blimc] 457.48 bound 731
c [blimc] 457.94 bound 732
c [blimc] 458.40 bound 733
c [blimc] 458.86 bound 734
[runlim] sample:		459.1 time, 460.3 real, 2628.2 MB
c [blimc] 459.33 bound 735
c [blimc] 459.80 bound 736
c [blimc] 460.30 bound 737
c [blimc] 460.76 bound 738
c [blimc] 461.22 bound 739
c [blimc] 461.69 bound 740
c [blimc] 462.16 bound 741
c [blimc] 462.62 bound 742
c [blimc] 463.09 bound 743
c [blimc] 463.56 bound 744
c [blimc] 464.03 bound 745
c [blimc] 464.50 bound 746
c [blimc] 464.97 bound 747
c [blimc] 465.44 bound 748
c [blimc] 465.92 bound 749
c [blimc] 466.39 bound 750
c [blimc] 466.86 bound 751
c [blimc] 467.34 bound 752
c [blimc] 467.82 bound 753
c [blimc] 468.30 bound 754
c [blimc] 468.78 bound 755
[runlim] sample:		469.0 time, 470.3 real, 2861.2 MB
c [blimc] 469.26 bound 756
c [blimc] 469.74 bound 757
c [blimc] 470.23 bound 758
c [blimc] 470.71 bound 759
c [blimc] 471.19 bound 760
c [blimc] 471.68 bound 761
c [blimc] 472.16 bound 762
c [blimc] 472.65 bound 763
c [blimc] 473.14 bound 764
c [blimc] 473.62 bound 765
c [blimc] 474.11 bound 766
c [blimc] 474.60 bound 767
c [blimc] 475.09 bound 768
c [blimc] 475.58 bound 769
c [blimc] 476.08 bound 770
c [blimc] 476.57 bound 771
c [blimc] 477.06 bound 772
c [blimc] 477.56 bound 773
c [blimc] 478.05 bound 774
c [blimc] 478.54 bound 775
[runlim] sample:		479.0 time, 480.3 real, 3085.2 MB
c [blimc] 479.04 bound 776
c [blimc] 479.54 bound 777
c [blimc] 480.04 bound 778
c [blimc] 480.54 bound 779
c [blimc] 481.04 bound 780
c [blimc] 481.53 bound 781
c [blimc] 482.03 bound 782
c [blimc] 482.53 bound 783
c [blimc] 483.02 bound 784
c [blimc] 483.52 bound 785
c [blimc] 484.02 bound 786
c [blimc] 484.52 bound 787
c [blimc] 485.02 bound 788
c [blimc] 485.53 bound 789
c [blimc] 486.03 bound 790
c [blimc] 486.54 bound 791
c [blimc] 487.04 bound 792
c [blimc] 487.55 bound 793
c [blimc] 488.06 bound 794
c [blimc] 488.57 bound 795
[runlim] sample:		489.0 time, 490.3 real, 3137.7 MB
c [blimc] 489.08 bound 796
c [blimc] 489.60 bound 797
c [blimc] 490.11 bound 798
c [blimc] 490.62 bound 799
c [blimc] 491.13 bound 800
c [blimc] 491.64 bound 801
c [blimc] 492.16 bound 802
c [blimc] 492.67 bound 803
c [blimc] 493.19 bound 804
c [blimc] 493.71 bound 805
c [blimc] 494.22 bound 806
c [blimc] 494.74 bound 807
c [blimc] 495.26 bound 808
c [blimc] 495.78 bound 809
c [blimc] 496.30 bound 810
c [blimc] 496.82 bound 811
c [blimc] 497.33 bound 812
c [blimc] 497.85 bound 813
c [blimc] 498.37 bound 814
c [blimc] 498.89 bound 815
[runlim] sample:		498.9 time, 500.3 real, 2367.0 MB
c [blimc] 499.41 bound 816
c [blimc] 499.94 bound 817
c [blimc] 500.46 bound 818
c [blimc] 500.98 bound 819
c [blimc] 501.51 bound 820
c [blimc] 502.03 bound 821
c [blimc] 502.56 bound 822
c [blimc] 503.09 bound 823
c [blimc] 503.62 bound 824
c [blimc] 504.15 bound 825
c [blimc] 504.68 bound 826
c [blimc] 505.21 bound 827
c [blimc] 505.74 bound 828
c [blimc] 506.27 bound 829
c [blimc] 506.81 bound 830
c [blimc] 507.34 bound 831
c [blimc] 507.88 bound 832
c [blimc] 508.42 bound 833
[runlim] sample:		508.9 time, 510.3 real, 3237.7 MB
c [blimc] 508.95 bound 834
c [blimc] 509.49 bound 835
c [blimc] 510.04 bound 836
c [blimc] 510.57 bound 837
c [blimc] 511.11 bound 838
c [blimc] 511.66 bound 839
c [blimc] 512.20 bound 840
c [blimc] 512.74 bound 841
c [blimc] 513.29 bound 842
c [blimc] 513.84 bound 843
c [blimc] 514.38 bound 844
c [blimc] 514.93 bound 845
c [blimc] 515.47 bound 846
c [blimc] 516.02 bound 847
c [blimc] 516.57 bound 848
c [blimc] 517.12 bound 849
c [blimc] 517.68 bound 850
c [blimc] 518.23 bound 851
c [blimc] 518.78 bound 852
[runlim] sample:		518.9 time, 520.3 real, 2580.8 MB
c [blimc] 519.33 bound 853
c [blimc] 519.88 bound 854
c [blimc] 520.43 bound 855
c [blimc] 520.98 bound 856
c [blimc] 521.53 bound 857
c [blimc] 522.08 bound 858
c [blimc] 522.64 bound 859
c [blimc] 523.20 bound 860
c [blimc] 523.76 bound 861
c [blimc] 524.31 bound 862
c [blimc] 524.87 bound 863
c [blimc] 525.43 bound 864
c [blimc] 525.99 bound 865
c [blimc] 526.55 bound 866
c [blimc] 527.11 bound 867
c [blimc] 527.68 bound 868
c [blimc] 528.24 bound 869
c [blimc] 528.80 bound 870
[runlim] sample:		528.9 time, 530.3 real, 2440.2 MB
c [blimc] 529.36 bound 871
c [blimc] 529.92 bound 872
c [blimc] 530.48 bound 873
c [blimc] 531.05 bound 874
c [blimc] 531.61 bound 875
c [blimc] 532.18 bound 876
c [blimc] 532.75 bound 877
c [blimc] 533.32 bound 878
c [blimc] 533.89 bound 879
c [blimc] 534.46 bound 880
c [blimc] 535.03 bound 881
c [blimc] 535.60 bound 882
c [blimc] 536.17 bound 883
c [blimc] 536.74 bound 884
c [blimc] 537.32 bound 885
c [blimc] 537.89 bound 886
c [blimc] 538.47 bound 887
[runlim] sample:		538.8 time, 540.3 real, 3267.2 MB
c [blimc] 539.04 bound 888
c [blimc] 539.62 bound 889
c [blimc] 540.20 bound 890
c [blimc] 540.77 bound 891
c [blimc] 541.35 bound 892
c [blimc] 541.93 bound 893
c [blimc] 542.50 bound 894
c [blimc] 543.08 bound 895
c [blimc] 543.66 bound 896
c [blimc] 544.24 bound 897
c [blimc] 544.83 bound 898
c [blimc] 545.41 bound 899
c [blimc] 546.00 bound 900
c [blimc] 546.59 bound 901
c [blimc] 547.17 bound 902
c [blimc] 547.76 bound 903
c [blimc] 548.34 bound 904
[runlim] sample:		548.8 time, 550.3 real, 3480.5 MB
c [blimc] 548.93 bound 905
c [blimc] 549.52 bound 906
c [blimc] 550.11 bound 907
c [blimc] 550.70 bound 908
c [blimc] 551.30 bound 909
c [blimc] 551.89 bound 910
c [blimc] 552.48 bound 911
c [blimc] 553.08 bound 912
c [blimc] 553.67 bound 913
c [blimc] 554.27 bound 914
c [blimc] 554.87 bound 915
c [blimc] 555.46 bound 916
c [blimc] 556.06 bound 917
c [blimc] 556.66 bound 918
c [blimc] 557.25 bound 919
c [blimc] 557.85 bound 920
c [blimc] 558.44 bound 921
[runlim] sample:		558.7 time, 560.3 real, 3178.4 MB
c [blimc] 559.04 bound 922
c [blimc] 559.64 bound 923
c [blimc] 560.24 bound 924
c [blimc] 560.85 bound 925
c [blimc] 561.45 bound 926
c [blimc] 562.06 bound 927
c [blimc] 562.67 bound 928
c [blimc] 563.27 bound 929
c [blimc] 563.88 bound 930
c [blimc] 564.48 bound 931
c [blimc] 565.09 bound 932
c [blimc] 565.69 bound 933
c [blimc] 566.30 bound 934
c [blimc] 566.90 bound 935
c [blimc] 567.51 bound 936
c [blimc] 568.12 bound 937
[runlim] sample:		568.7 time, 570.3 real, 3570.2 MB
c [blimc] 568.72 bound 938
c [blimc] 569.34 bound 939
c [blimc] 569.95 bound 940
c [blimc] 570.56 bound 941
c [blimc] 571.18 bound 942
c [blimc] 571.79 bound 943
c [blimc] 572.40 bound 944
c [blimc] 573.01 bound 945
c [blimc] 573.63 bound 946
c [blimc] 574.24 bound 947
c [blimc] 574.86 bound 948
c [blimc] 575.47 bound 949
c [blimc] 576.09 bound 950
c [blimc] 576.71 bound 951
c [blimc] 577.33 bound 952
c [blimc] 577.95 bound 953
c [blimc] 578.57 bound 954
[runlim] sample:		578.7 time, 580.3 real, 2673.9 MB
c [blimc] 579.19 bound 955
c [blimc] 579.82 bound 956
c [blimc] 580.45 bound 957
c [blimc] 581.07 bound 958
c [blimc] 581.70 bound 959
c [blimc] 582.33 bound 960
c [blimc] 582.96 bound 961
c [blimc] 583.59 bound 962
c [blimc] 584.22 bound 963
c [blimc] 584.86 bound 964
c [blimc] 585.49 bound 965
c [blimc] 586.12 bound 966
c [blimc] 586.76 bound 967
c [blimc] 587.39 bound 968
c [blimc] 588.02 bound 969
[runlim] sample:		588.6 time, 590.3 real, 3657.4 MB
c [blimc] 588.66 bound 970
c [blimc] 589.30 bound 971
c [blimc] 589.94 bound 972
c [blimc] 590.57 bound 973
c [blimc] 591.21 bound 974
c [blimc] 591.85 bound 975
c [blimc] 592.49 bound 976
c [blimc] 593.13 bound 977
c [blimc] 593.78 bound 978
c [blimc] 594.42 bound 979
c [blimc] 595.06 bound 980
c [blimc] 595.70 bound 981
c [blimc] 596.35 bound 982
c [blimc] 597.00 bound 983
c [blimc] 597.64 bound 984
c [blimc] 598.29 bound 985
[runlim] sample:		598.6 time, 600.3 real, 3306.4 MB
c [blimc] 598.94 bound 986
c [blimc] 599.59 bound 987
c [blimc] 600.23 bound 988
c [blimc] 600.88 bound 989
c [blimc] 601.53 bound 990
c [blimc] 602.17 bound 991
c [blimc] 602.82 bound 992
c [blimc] 603.47 bound 993
c [blimc] 604.12 bound 994
c [blimc] 604.76 bound 995
c [blimc] 605.41 bound 996
c [blimc] 606.09 bound 997
c [blimc] 606.74 bound 998
c [blimc] 607.40 bound 999
c [blimc] 608.05 bound 1000
[runlim] sample:		608.5 time, 610.3 real, 3741.5 MB
c [lgl1000]  270.626  75% simplifying
c [lgl1000]    1.041   0% search
c [lgl1000] ==================================
c [lgl1000]  361.544 100% all
c [lgl1000] 
c [lgl1000]           998 conflicts,           2.8 confs/sec
c [lgl1000]             0 ternaries,           0.0 confs/ternary
c [lgl1000]             0 binaries,            0.0 confs/binary
c [lgl1000]           998 iterations,          1.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]           998 decisions,           2.8 decis/sec,      1.0 decis/conflict
c [lgl1000]       4436489 propagations,    12270.9 props/sec,   4445.4 props/decision
c [lgl1000] 
c [lgl1000] 361.5 seconds, 3675.6 MB
c [blimc] 608.72 reached k = 1001
c [blimc] 608.72 cloned 0 solvers
c [blimc] 608.72 max 3677.4 MB
c [blimc] 608.83 exit 20
[runlim] end:			Thu Sep 17 12:30:20 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			610.67 seconds
[runlim] time:			608.82 seconds
[runlim] space:			3741.5 MB
[runlim] samples:		6103
