[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/oski15a14b18s.aig
[runlim] start:			Thu Sep 17 12:24:38 2015
[runlim] main pid:		6701
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/oski15a14b18s.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.15 simplified
c [blimc] 6.15 extracted
c [lglopt]    6.102 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]    6.104 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]        418727 propagations,    68598.3 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 6.1 seconds, 14.8 MB
c [blimc] 6.16 mapped 11361 variables
c [blimc] 6.16 maxk 1000
c [blimc] 6.16 bound 0
c [blimc] 6.22 bound 1
c [blimc] 6.61 bound 2
c [blimc] 6.63 bound 3
c [blimc] 8.22 bound 4
c [blimc] 8.24 bound 5
[runlim] sample:		10.0 time, 10.3 real, 20.5 MB
c [blimc] 10.01 bound 6
c [blimc] 10.04 bound 7
c [blimc] 10.06 bound 8
c [blimc] 15.69 bound 9
c [blimc] 15.72 bound 10
c [blimc] 15.74 bound 11
c [blimc] 15.77 bound 12
[runlim] sample:		20.0 time, 20.3 real, 56.9 MB
c [blimc] 20.14 bound 13
c [blimc] 20.17 bound 14
c [blimc] 20.21 bound 15
c [blimc] 20.24 bound 16
c [blimc] 20.27 bound 17
c [blimc] 20.30 bound 18
[runlim] sample:		30.0 time, 30.3 real, 123.4 MB
c [blimc] 32.67 bound 19
c [blimc] 32.70 bound 20
c [blimc] 32.74 bound 21
c [blimc] 32.78 bound 22
c [blimc] 32.81 bound 23
c [blimc] 32.85 bound 24
c [blimc] 32.89 bound 25
c [blimc] 32.93 bound 26
c [blimc] 32.96 bound 27
c [blimc] 33.01 bound 28
[runlim] sample:		40.0 time, 40.3 real, 189.1 MB
c [blimc] 43.95 bound 29
c [blimc] 43.99 bound 30
c [blimc] 44.03 bound 31
c [blimc] 44.07 bound 32
c [blimc] 44.11 bound 33
c [blimc] 44.15 bound 34
c [blimc] 44.19 bound 35
c [blimc] 44.23 bound 36
c [blimc] 44.28 bound 37
c [blimc] 44.32 bound 38
c [blimc] 44.37 bound 39
c [blimc] 44.42 bound 40
c [blimc] 44.46 bound 41
c [blimc] 44.52 bound 42
c [blimc] 44.56 bound 43
[runlim] sample:		50.0 time, 50.3 real, 271.7 MB
[runlim] sample:		60.0 time, 60.3 real, 271.7 MB
c [blimc] 65.69 bound 44
c [blimc] 65.74 bound 45
c [blimc] 65.79 bound 46
c [blimc] 65.85 bound 47
c [blimc] 65.90 bound 48
c [blimc] 65.95 bound 49
c [blimc] 66.01 bound 50
c [blimc] 66.06 bound 51
c [blimc] 66.11 bound 52
c [blimc] 66.16 bound 53
c [blimc] 66.22 bound 54
c [blimc] 66.27 bound 55
c [blimc] 66.33 bound 56
c [blimc] 66.38 bound 57
c [blimc] 66.45 bound 58
c [blimc] 66.51 bound 59
c [blimc] 66.57 bound 60
c [blimc] 66.63 bound 61
c [blimc] 66.70 bound 62
c [blimc] 66.77 bound 63
c [blimc] 66.84 bound 64
c [blimc] 66.90 bound 65
c [blimc] 66.97 bound 66
[runlim] sample:		69.9 time, 70.3 real, 283.1 MB
[runlim] sample:		79.9 time, 80.3 real, 283.4 MB
c [blimc] 80.95 bound 67
c [blimc] 81.02 bound 68
c [blimc] 81.09 bound 69
c [blimc] 81.16 bound 70
c [blimc] 81.22 bound 71
c [blimc] 81.28 bound 72
c [blimc] 81.35 bound 73
c [blimc] 81.41 bound 74
c [blimc] 81.48 bound 75
c [blimc] 81.54 bound 76
c [blimc] 81.61 bound 77
c [blimc] 81.68 bound 78
c [blimc] 81.75 bound 79
c [blimc] 81.82 bound 80
c [blimc] 81.90 bound 81
c [blimc] 81.98 bound 82
c [blimc] 82.06 bound 83
c [blimc] 82.13 bound 84
c [blimc] 82.21 bound 85
c [blimc] 82.28 bound 86
c [blimc] 82.36 bound 87
c [blimc] 82.44 bound 88
c [blimc] 82.53 bound 89
c [blimc] 82.61 bound 90
c [blimc] 82.70 bound 91
c [blimc] 82.78 bound 92
c [blimc] 82.87 bound 93
c [blimc] 82.96 bound 94
c [blimc] 83.04 bound 95
c [blimc] 83.12 bound 96
c [blimc] 83.20 bound 97
c [blimc] 83.29 bound 98
c [blimc] 83.38 bound 99
c [blimc] 83.46 bound 100
c [blimc] 83.54 bound 101
c [blimc] 83.63 bound 102
[runlim] sample:		89.9 time, 90.3 real, 323.7 MB
[runlim] sample:		99.9 time, 100.3 real, 323.6 MB
c [blimc] 100.36 bound 103
c [blimc] 100.46 bound 104
c [blimc] 100.55 bound 105
c [blimc] 100.63 bound 106
c [blimc] 100.72 bound 107
c [blimc] 100.80 bound 108
c [blimc] 100.89 bound 109
c [blimc] 100.97 bound 110
c [blimc] 101.06 bound 111
c [blimc] 101.15 bound 112
c [blimc] 101.24 bound 113
c [blimc] 101.33 bound 114
c [blimc] 101.42 bound 115
c [blimc] 101.51 bound 116
c [blimc] 101.60 bound 117
c [blimc] 101.70 bound 118
c [blimc] 101.80 bound 119
c [blimc] 101.90 bound 120
c [blimc] 102.00 bound 121
c [blimc] 102.11 bound 122
c [blimc] 102.21 bound 123
c [blimc] 102.32 bound 124
c [blimc] 102.44 bound 125
c [blimc] 102.54 bound 126
c [blimc] 102.64 bound 127
c [blimc] 102.75 bound 128
c [blimc] 102.85 bound 129
c [blimc] 102.95 bound 130
c [blimc] 103.05 bound 131
c [blimc] 103.16 bound 132
c [blimc] 103.27 bound 133
c [blimc] 103.37 bound 134
c [blimc] 103.49 bound 135
c [blimc] 103.59 bound 136
c [blimc] 103.70 bound 137
c [blimc] 103.81 bound 138
c [blimc] 103.93 bound 139
c [blimc] 104.03 bound 140
c [blimc] 104.14 bound 141
c [blimc] 104.26 bound 142
c [blimc] 104.37 bound 143
c [blimc] 104.48 bound 144
c [blimc] 104.59 bound 145
c [blimc] 104.70 bound 146
c [blimc] 104.82 bound 147
c [blimc] 104.93 bound 148
c [blimc] 105.05 bound 149
c [blimc] 105.16 bound 150
c [blimc] 105.28 bound 151
c [blimc] 105.40 bound 152
c [blimc] 105.52 bound 153
c [blimc] 105.64 bound 154
c [blimc] 105.75 bound 155
c [blimc] 105.88 bound 156
c [blimc] 106.00 bound 157
c [blimc] 106.12 bound 158
c [blimc] 106.24 bound 159
[runlim] sample:		109.9 time, 110.3 real, 454.4 MB
[runlim] sample:		119.9 time, 120.3 real, 583.0 MB
c [blimc] 126.18 bound 160
c [blimc] 126.33 bound 161
c [blimc] 126.45 bound 162
c [blimc] 126.57 bound 163
c [blimc] 126.69 bound 164
c [blimc] 126.81 bound 165
c [blimc] 126.93 bound 166
c [blimc] 127.05 bound 167
c [blimc] 127.17 bound 168
c [blimc] 127.29 bound 169
c [blimc] 127.41 bound 170
c [blimc] 127.54 bound 171
c [blimc] 127.66 bound 172
c [blimc] 127.78 bound 173
c [blimc] 127.91 bound 174
c [blimc] 128.03 bound 175
c [blimc] 128.16 bound 176
c [blimc] 128.29 bound 177
c [blimc] 128.42 bound 178
c [blimc] 128.55 bound 179
c [blimc] 128.68 bound 180
c [blimc] 128.81 bound 181
c [blimc] 128.94 bound 182
c [blimc] 129.07 bound 183
c [blimc] 129.21 bound 184
c [blimc] 129.36 bound 185
c [blimc] 129.50 bound 186
c [blimc] 129.63 bound 187
c [blimc] 129.77 bound 188
[runlim] sample:		129.9 time, 130.3 real, 837.5 MB
c [blimc] 129.91 bound 189
c [blimc] 130.04 bound 190
c [blimc] 130.18 bound 191
c [blimc] 130.32 bound 192
c [blimc] 130.46 bound 193
c [blimc] 130.60 bound 194
c [blimc] 130.74 bound 195
c [blimc] 130.88 bound 196
c [blimc] 131.03 bound 197
c [blimc] 131.17 bound 198
c [blimc] 131.31 bound 199
c [blimc] 131.46 bound 200
c [blimc] 131.60 bound 201
c [blimc] 131.75 bound 202
c [blimc] 131.89 bound 203
c [blimc] 132.04 bound 204
c [blimc] 132.19 bound 205
c [blimc] 132.34 bound 206
c [blimc] 132.51 bound 207
c [blimc] 132.67 bound 208
c [blimc] 132.82 bound 209
c [blimc] 132.97 bound 210
c [blimc] 133.12 bound 211
c [blimc] 133.27 bound 212
c [blimc] 133.43 bound 213
c [blimc] 133.58 bound 214
c [blimc] 133.74 bound 215
c [blimc] 133.89 bound 216
c [blimc] 134.05 bound 217
c [blimc] 134.20 bound 218
c [blimc] 134.36 bound 219
c [blimc] 134.52 bound 220
c [blimc] 134.69 bound 221
c [blimc] 134.84 bound 222
c [blimc] 135.00 bound 223
c [blimc] 135.16 bound 224
c [blimc] 135.33 bound 225
c [blimc] 135.49 bound 226
c [blimc] 135.65 bound 227
c [blimc] 135.82 bound 228
c [blimc] 135.98 bound 229
c [blimc] 136.15 bound 230
c [blimc] 136.32 bound 231
c [blimc] 136.49 bound 232
c [blimc] 136.65 bound 233
c [blimc] 136.82 bound 234
c [blimc] 136.99 bound 235
c [blimc] 137.17 bound 236
c [blimc] 137.34 bound 237
c [blimc] 137.51 bound 238
c [blimc] 137.68 bound 239
c [blimc] 137.85 bound 240
c [blimc] 138.03 bound 241
c [blimc] 138.20 bound 242
c [blimc] 138.38 bound 243
c [blimc] 138.56 bound 244
c [blimc] 138.73 bound 245
c [blimc] 138.91 bound 246
c [blimc] 139.09 bound 247
c [blimc] 139.27 bound 248
c [blimc] 139.45 bound 249
[runlim] sample:		139.8 time, 140.3 real, 825.6 MB
[runlim] sample:		149.8 time, 150.3 real, 857.7 MB
[runlim] sample:		159.8 time, 160.3 real, 853.2 MB
c [blimc] 166.98 bound 250
c [blimc] 167.20 bound 251
c [blimc] 167.39 bound 252
c [blimc] 167.56 bound 253
c [blimc] 167.74 bound 254
c [blimc] 167.91 bound 255
c [blimc] 168.09 bound 256
c [blimc] 168.27 bound 257
c [blimc] 168.44 bound 258
c [blimc] 168.61 bound 259
c [blimc] 168.79 bound 260
c [blimc] 168.96 bound 261
c [blimc] 169.14 bound 262
c [blimc] 169.31 bound 263
c [blimc] 169.49 bound 264
c [blimc] 169.67 bound 265
[runlim] sample:		169.8 time, 170.3 real, 1189.4 MB
c [blimc] 169.85 bound 266
c [blimc] 170.03 bound 267
c [blimc] 170.21 bound 268
c [blimc] 170.39 bound 269
c [blimc] 170.57 bound 270
c [blimc] 170.76 bound 271
c [blimc] 170.94 bound 272
c [blimc] 171.12 bound 273
c [blimc] 171.31 bound 274
c [blimc] 171.49 bound 275
c [blimc] 171.68 bound 276
c [blimc] 171.87 bound 277
c [blimc] 172.05 bound 278
c [blimc] 172.24 bound 279
c [blimc] 172.43 bound 280
c [blimc] 172.62 bound 281
c [blimc] 172.81 bound 282
c [blimc] 173.01 bound 283
c [blimc] 173.20 bound 284
c [blimc] 173.39 bound 285
c [blimc] 173.58 bound 286
c [blimc] 173.78 bound 287
c [blimc] 173.97 bound 288
c [blimc] 174.17 bound 289
c [blimc] 174.37 bound 290
c [blimc] 174.57 bound 291
c [blimc] 174.76 bound 292
c [blimc] 174.96 bound 293
c [blimc] 175.16 bound 294
c [blimc] 175.36 bound 295
c [blimc] 175.57 bound 296
c [blimc] 175.77 bound 297
c [blimc] 175.97 bound 298
c [blimc] 176.17 bound 299
c [blimc] 176.38 bound 300
c [blimc] 176.58 bound 301
c [blimc] 176.79 bound 302
c [blimc] 176.99 bound 303
c [blimc] 177.20 bound 304
c [blimc] 177.40 bound 305
c [blimc] 177.61 bound 306
c [blimc] 177.82 bound 307
c [blimc] 178.03 bound 308
c [blimc] 178.24 bound 309
c [blimc] 178.45 bound 310
c [blimc] 178.66 bound 311
c [blimc] 178.87 bound 312
c [blimc] 179.08 bound 313
c [blimc] 179.30 bound 314
c [blimc] 179.51 bound 315
c [blimc] 179.73 bound 316
[runlim] sample:		179.8 time, 180.3 real, 1093.6 MB
c [blimc] 179.94 bound 317
c [blimc] 180.16 bound 318
c [blimc] 180.38 bound 319
c [blimc] 180.59 bound 320
c [blimc] 180.81 bound 321
c [blimc] 181.03 bound 322
c [blimc] 181.25 bound 323
c [blimc] 181.47 bound 324
c [blimc] 181.69 bound 325
c [blimc] 181.91 bound 326
c [blimc] 182.13 bound 327
c [blimc] 182.36 bound 328
c [blimc] 182.58 bound 329
c [blimc] 182.81 bound 330
c [blimc] 183.03 bound 331
c [blimc] 183.26 bound 332
c [blimc] 183.48 bound 333
c [blimc] 183.71 bound 334
c [blimc] 183.94 bound 335
c [blimc] 184.17 bound 336
c [blimc] 184.40 bound 337
c [blimc] 184.64 bound 338
c [blimc] 184.88 bound 339
c [blimc] 185.11 bound 340
c [blimc] 185.34 bound 341
c [blimc] 185.58 bound 342
c [blimc] 185.81 bound 343
c [blimc] 186.05 bound 344
c [blimc] 186.28 bound 345
c [blimc] 186.52 bound 346
c [blimc] 186.75 bound 347
c [blimc] 187.00 bound 348
c [blimc] 187.24 bound 349
c [blimc] 187.48 bound 350
c [blimc] 187.72 bound 351
c [blimc] 187.96 bound 352
c [blimc] 188.20 bound 353
c [blimc] 188.44 bound 354
c [blimc] 188.69 bound 355
c [blimc] 188.93 bound 356
c [blimc] 189.17 bound 357
c [blimc] 189.42 bound 358
c [blimc] 189.66 bound 359
[runlim] sample:		189.8 time, 190.3 real, 1238.1 MB
c [blimc] 189.91 bound 360
c [blimc] 190.16 bound 361
c [blimc] 190.40 bound 362
c [blimc] 190.66 bound 363
c [blimc] 190.91 bound 364
c [blimc] 191.16 bound 365
c [blimc] 191.41 bound 366
c [blimc] 191.66 bound 367
c [blimc] 191.91 bound 368
c [blimc] 192.17 bound 369
c [blimc] 192.44 bound 370
c [blimc] 192.69 bound 371
c [blimc] 192.95 bound 372
c [blimc] 193.21 bound 373
c [blimc] 193.46 bound 374
c [blimc] 193.72 bound 375
c [blimc] 193.98 bound 376
c [blimc] 194.24 bound 377
c [blimc] 194.50 bound 378
c [blimc] 194.76 bound 379
c [blimc] 195.02 bound 380
c [blimc] 195.29 bound 381
c [blimc] 195.55 bound 382
c [blimc] 195.81 bound 383
c [blimc] 196.08 bound 384
c [blimc] 196.34 bound 385
c [blimc] 196.61 bound 386
c [blimc] 196.88 bound 387
c [blimc] 197.15 bound 388
c [blimc] 197.42 bound 389
c [blimc] 197.69 bound 390
c [blimc] 197.96 bound 391
c [blimc] 198.24 bound 392
[runlim] sample:		199.7 time, 200.3 real, 1140.1 MB
[runlim] sample:		209.7 time, 210.3 real, 1263.0 MB
[runlim] sample:		219.7 time, 220.3 real, 991.7 MB
[runlim] sample:		229.7 time, 230.3 real, 1391.5 MB
[runlim] sample:		239.7 time, 240.3 real, 1304.0 MB
[runlim] sample:		249.7 time, 250.3 real, 909.4 MB
c [blimc] 250.42 bound 393
c [blimc] 250.76 bound 394
c [blimc] 251.01 bound 395
c [blimc] 251.27 bound 396
c [blimc] 251.52 bound 397
c [blimc] 251.77 bound 398
c [blimc] 252.03 bound 399
c [blimc] 252.28 bound 400
c [blimc] 252.54 bound 401
c [blimc] 252.79 bound 402
c [blimc] 253.05 bound 403
c [blimc] 253.31 bound 404
c [blimc] 253.57 bound 405
c [blimc] 253.83 bound 406
c [blimc] 254.09 bound 407
c [blimc] 254.35 bound 408
c [blimc] 254.61 bound 409
c [blimc] 254.87 bound 410
c [blimc] 255.13 bound 411
c [blimc] 255.39 bound 412
c [blimc] 255.66 bound 413
c [blimc] 255.92 bound 414
c [blimc] 256.19 bound 415
c [blimc] 256.45 bound 416
c [blimc] 256.72 bound 417
c [blimc] 257.00 bound 418
c [blimc] 257.27 bound 419
c [blimc] 257.54 bound 420
c [blimc] 257.81 bound 421
c [blimc] 258.08 bound 422
c [blimc] 258.35 bound 423
c [blimc] 258.63 bound 424
c [blimc] 258.90 bound 425
c [blimc] 259.17 bound 426
c [blimc] 259.45 bound 427
[runlim] sample:		259.6 time, 260.3 real, 1840.7 MB
c [blimc] 259.72 bound 428
c [blimc] 260.00 bound 429
c [blimc] 260.27 bound 430
c [blimc] 260.55 bound 431
c [blimc] 260.83 bound 432
c [blimc] 261.11 bound 433
c [blimc] 261.39 bound 434
c [blimc] 261.67 bound 435
c [blimc] 261.95 bound 436
c [blimc] 262.23 bound 437
c [blimc] 262.51 bound 438
c [blimc] 262.80 bound 439
c [blimc] 263.08 bound 440
c [blimc] 263.36 bound 441
c [blimc] 263.65 bound 442
c [blimc] 263.93 bound 443
c [blimc] 264.22 bound 444
c [blimc] 264.50 bound 445
c [blimc] 264.79 bound 446
c [blimc] 265.08 bound 447
c [blimc] 265.37 bound 448
c [blimc] 265.66 bound 449
c [blimc] 265.95 bound 450
c [blimc] 266.24 bound 451
c [blimc] 266.54 bound 452
c [blimc] 266.83 bound 453
c [blimc] 267.13 bound 454
c [blimc] 267.42 bound 455
c [blimc] 267.72 bound 456
c [blimc] 268.01 bound 457
c [blimc] 268.31 bound 458
c [blimc] 268.60 bound 459
c [blimc] 268.90 bound 460
c [blimc] 269.20 bound 461
c [blimc] 269.50 bound 462
[runlim] sample:		269.6 time, 270.3 real, 1671.2 MB
c [blimc] 269.80 bound 463
c [blimc] 270.10 bound 464
c [blimc] 270.40 bound 465
c [blimc] 270.71 bound 466
c [blimc] 271.01 bound 467
c [blimc] 271.31 bound 468
c [blimc] 271.62 bound 469
c [blimc] 271.92 bound 470
c [blimc] 272.23 bound 471
c [blimc] 272.53 bound 472
c [blimc] 272.84 bound 473
c [blimc] 273.15 bound 474
c [blimc] 273.46 bound 475
c [blimc] 273.76 bound 476
c [blimc] 274.07 bound 477
c [blimc] 274.39 bound 478
c [blimc] 274.70 bound 479
c [blimc] 275.01 bound 480
c [blimc] 275.32 bound 481
c [blimc] 275.64 bound 482
c [blimc] 275.95 bound 483
c [blimc] 276.26 bound 484
c [blimc] 276.58 bound 485
c [blimc] 276.90 bound 486
c [blimc] 277.22 bound 487
c [blimc] 277.54 bound 488
c [blimc] 277.86 bound 489
c [blimc] 278.18 bound 490
c [blimc] 278.49 bound 491
c [blimc] 278.82 bound 492
c [blimc] 279.14 bound 493
c [blimc] 279.46 bound 494
[runlim] sample:		279.6 time, 280.3 real, 1758.3 MB
c [blimc] 279.78 bound 495
c [blimc] 280.11 bound 496
c [blimc] 280.43 bound 497
c [blimc] 280.76 bound 498
c [blimc] 281.08 bound 499
c [blimc] 281.41 bound 500
c [blimc] 281.74 bound 501
c [blimc] 282.07 bound 502
c [blimc] 282.39 bound 503
c [blimc] 282.72 bound 504
c [blimc] 283.05 bound 505
c [blimc] 283.39 bound 506
c [blimc] 283.72 bound 507
c [blimc] 284.05 bound 508
c [blimc] 284.39 bound 509
c [blimc] 284.72 bound 510
c [blimc] 285.05 bound 511
c [blimc] 285.41 bound 512
c [blimc] 285.75 bound 513
c [blimc] 286.09 bound 514
c [blimc] 286.42 bound 515
c [blimc] 286.76 bound 516
c [blimc] 287.11 bound 517
c [blimc] 287.45 bound 518
c [blimc] 287.79 bound 519
c [blimc] 288.13 bound 520
c [blimc] 288.48 bound 521
c [blimc] 288.82 bound 522
c [blimc] 289.16 bound 523
c [blimc] 289.50 bound 524
[runlim] sample:		289.6 time, 290.3 real, 1584.8 MB
c [blimc] 289.85 bound 525
c [blimc] 290.20 bound 526
c [blimc] 290.54 bound 527
c [blimc] 290.89 bound 528
c [blimc] 291.24 bound 529
c [blimc] 291.59 bound 530
c [blimc] 291.94 bound 531
c [blimc] 292.29 bound 532
c [blimc] 292.64 bound 533
c [blimc] 292.99 bound 534
c [blimc] 293.34 bound 535
c [blimc] 293.69 bound 536
c [blimc] 294.05 bound 537
c [blimc] 294.40 bound 538
c [blimc] 294.76 bound 539
c [blimc] 295.11 bound 540
c [blimc] 295.47 bound 541
c [blimc] 295.83 bound 542
c [blimc] 296.18 bound 543
c [blimc] 296.55 bound 544
c [blimc] 296.91 bound 545
c [blimc] 297.27 bound 546
c [blimc] 297.63 bound 547
c [blimc] 297.99 bound 548
c [blimc] 298.36 bound 549
c [blimc] 298.72 bound 550
c [blimc] 299.08 bound 551
c [blimc] 299.45 bound 552
[runlim] sample:		299.5 time, 300.3 real, 1710.3 MB
c [blimc] 299.81 bound 553
c [blimc] 300.18 bound 554
c [blimc] 300.55 bound 555
c [blimc] 300.91 bound 556
c [blimc] 301.28 bound 557
c [blimc] 301.65 bound 558
c [blimc] 302.02 bound 559
c [blimc] 302.39 bound 560
c [blimc] 302.76 bound 561
c [blimc] 303.13 bound 562
c [blimc] 303.50 bound 563
c [blimc] 303.88 bound 564
c [blimc] 304.25 bound 565
c [blimc] 304.63 bound 566
c [blimc] 305.00 bound 567
c [blimc] 305.38 bound 568
c [blimc] 305.76 bound 569
c [blimc] 306.13 bound 570
c [blimc] 306.51 bound 571
c [blimc] 306.89 bound 572
c [blimc] 307.27 bound 573
c [blimc] 307.66 bound 574
c [blimc] 308.04 bound 575
c [blimc] 308.43 bound 576
c [blimc] 308.81 bound 577
c [blimc] 309.19 bound 578
[runlim] sample:		309.5 time, 310.3 real, 2238.5 MB
c [blimc] 309.58 bound 579
c [blimc] 309.97 bound 580
c [blimc] 310.35 bound 581
c [blimc] 310.74 bound 582
c [blimc] 311.13 bound 583
c [blimc] 311.52 bound 584
c [blimc] 311.91 bound 585
c [blimc] 312.30 bound 586
c [blimc] 312.69 bound 587
c [blimc] 313.08 bound 588
c [blimc] 313.47 bound 589
c [blimc] 313.86 bound 590
c [blimc] 314.25 bound 591
c [blimc] 314.65 bound 592
c [blimc] 315.04 bound 593
c [blimc] 315.44 bound 594
c [blimc] 315.83 bound 595
c [blimc] 316.23 bound 596
c [blimc] 316.63 bound 597
c [blimc] 317.03 bound 598
c [blimc] 317.43 bound 599
c [blimc] 317.83 bound 600
c [blimc] 318.23 bound 601
c [blimc] 318.63 bound 602
c [blimc] 319.03 bound 603
c [blimc] 319.43 bound 604
[runlim] sample:		319.4 time, 320.3 real, 1635.7 MB
c [blimc] 319.84 bound 605
c [blimc] 320.24 bound 606
c [blimc] 320.64 bound 607
c [blimc] 321.05 bound 608
c [blimc] 321.46 bound 609
c [blimc] 321.86 bound 610
c [blimc] 322.27 bound 611
c [blimc] 322.67 bound 612
c [blimc] 323.08 bound 613
c [blimc] 323.49 bound 614
c [blimc] 323.90 bound 615
c [blimc] 324.31 bound 616
c [blimc] 324.72 bound 617
c [blimc] 325.14 bound 618
c [blimc] 325.55 bound 619
c [blimc] 325.97 bound 620
[runlim] sample:		329.4 time, 330.3 real, 1658.1 MB
[runlim] sample:		339.4 time, 340.3 real, 1511.3 MB
[runlim] sample:		349.4 time, 350.3 real, 2364.0 MB
[runlim] sample:		359.4 time, 360.3 real, 1451.2 MB
[runlim] sample:		369.4 time, 370.3 real, 2086.1 MB
[runlim] sample:		379.4 time, 380.3 real, 1960.4 MB
[runlim] sample:		389.4 time, 390.3 real, 1973.3 MB
[runlim] sample:		399.3 time, 400.3 real, 1957.2 MB
[runlim] sample:		409.3 time, 410.3 real, 1402.0 MB
c [blimc] 411.94 bound 621
c [blimc] 412.39 bound 622
c [blimc] 412.78 bound 623
c [blimc] 413.16 bound 624
c [blimc] 413.55 bound 625
c [blimc] 413.94 bound 626
c [blimc] 414.32 bound 627
c [blimc] 414.71 bound 628
c [blimc] 415.09 bound 629
c [blimc] 415.48 bound 630
c [blimc] 415.87 bound 631
c [blimc] 416.26 bound 632
c [blimc] 416.65 bound 633
c [blimc] 417.05 bound 634
c [blimc] 417.44 bound 635
c [blimc] 417.84 bound 636
c [blimc] 418.23 bound 637
c [blimc] 418.63 bound 638
c [blimc] 419.02 bound 639
[runlim] sample:		419.3 time, 420.3 real, 2660.3 MB
c [blimc] 419.42 bound 640
c [blimc] 419.81 bound 641
c [blimc] 420.21 bound 642
c [blimc] 420.61 bound 643
c [blimc] 421.01 bound 644
c [blimc] 421.40 bound 645
c [blimc] 421.80 bound 646
c [blimc] 422.20 bound 647
c [blimc] 422.60 bound 648
c [blimc] 423.00 bound 649
c [blimc] 423.41 bound 650
c [blimc] 423.81 bound 651
c [blimc] 424.22 bound 652
c [blimc] 424.62 bound 653
c [blimc] 425.03 bound 654
c [blimc] 425.43 bound 655
c [blimc] 425.84 bound 656
c [blimc] 426.25 bound 657
c [blimc] 426.65 bound 658
c [blimc] 427.07 bound 659
c [blimc] 427.48 bound 660
c [blimc] 427.89 bound 661
c [blimc] 428.30 bound 662
c [blimc] 428.71 bound 663
c [blimc] 429.12 bound 664
[runlim] sample:		429.3 time, 430.3 real, 2343.8 MB
c [blimc] 429.54 bound 665
c [blimc] 429.95 bound 666
c [blimc] 430.37 bound 667
c [blimc] 430.78 bound 668
c [blimc] 431.20 bound 669
c [blimc] 431.61 bound 670
c [blimc] 432.03 bound 671
c [blimc] 432.45 bound 672
c [blimc] 432.87 bound 673
c [blimc] 433.29 bound 674
c [blimc] 433.71 bound 675
c [blimc] 434.13 bound 676
c [blimc] 434.55 bound 677
c [blimc] 434.97 bound 678
c [blimc] 435.40 bound 679
c [blimc] 435.82 bound 680
c [blimc] 436.25 bound 681
c [blimc] 436.67 bound 682
c [blimc] 437.10 bound 683
c [blimc] 437.53 bound 684
c [blimc] 437.95 bound 685
c [blimc] 438.38 bound 686
c [blimc] 438.81 bound 687
c [blimc] 439.24 bound 688
[runlim] sample:		439.2 time, 440.3 real, 2076.9 MB
c [blimc] 439.67 bound 689
c [blimc] 440.10 bound 690
c [blimc] 440.54 bound 691
c [blimc] 440.97 bound 692
c [blimc] 441.40 bound 693
c [blimc] 441.83 bound 694
c [blimc] 442.27 bound 695
c [blimc] 442.71 bound 696
c [blimc] 443.14 bound 697
c [blimc] 443.58 bound 698
c [blimc] 444.02 bound 699
c [blimc] 444.46 bound 700
c [blimc] 444.90 bound 701
c [blimc] 445.34 bound 702
c [blimc] 445.78 bound 703
c [blimc] 446.22 bound 704
c [blimc] 446.66 bound 705
c [blimc] 447.11 bound 706
c [blimc] 447.55 bound 707
c [blimc] 447.99 bound 708
c [blimc] 448.44 bound 709
c [blimc] 448.89 bound 710
[runlim] sample:		449.2 time, 450.3 real, 2847.3 MB
c [blimc] 449.33 bound 711
c [blimc] 449.78 bound 712
c [blimc] 450.23 bound 713
c [blimc] 450.68 bound 714
c [blimc] 451.13 bound 715
c [blimc] 451.58 bound 716
c [blimc] 452.03 bound 717
c [blimc] 452.48 bound 718
c [blimc] 452.93 bound 719
c [blimc] 453.38 bound 720
c [blimc] 453.83 bound 721
c [blimc] 454.29 bound 722
c [blimc] 454.74 bound 723
c [blimc] 455.19 bound 724
c [blimc] 455.65 bound 725
c [blimc] 456.11 bound 726
c [blimc] 456.57 bound 727
c [blimc] 457.03 bound 728
c [blimc] 457.49 bound 729
c [blimc] 457.96 bound 730
c [blimc] 458.42 bound 731
c [blimc] 458.88 bound 732
[runlim] sample:		459.2 time, 460.3 real, 2827.6 MB
c [blimc] 459.35 bound 733
c [blimc] 459.81 bound 734
c [blimc] 460.28 bound 735
c [blimc] 460.74 bound 736
c [blimc] 461.21 bound 737
c [blimc] 461.68 bound 738
c [blimc] 462.18 bound 739
c [blimc] 462.65 bound 740
c [blimc] 463.12 bound 741
c [blimc] 463.59 bound 742
c [blimc] 464.06 bound 743
c [blimc] 464.53 bound 744
c [blimc] 465.00 bound 745
c [blimc] 465.47 bound 746
c [blimc] 465.95 bound 747
c [blimc] 466.42 bound 748
c [blimc] 466.90 bound 749
c [blimc] 467.38 bound 750
c [blimc] 467.86 bound 751
c [blimc] 468.34 bound 752
c [blimc] 468.82 bound 753
[runlim] sample:		469.1 time, 470.3 real, 3037.1 MB
c [blimc] 469.30 bound 754
c [blimc] 469.78 bound 755
c [blimc] 470.26 bound 756
c [blimc] 470.74 bound 757
c [blimc] 471.23 bound 758
c [blimc] 471.71 bound 759
c [blimc] 472.19 bound 760
c [blimc] 472.68 bound 761
c [blimc] 473.17 bound 762
c [blimc] 473.66 bound 763
c [blimc] 474.14 bound 764
c [blimc] 474.63 bound 765
c [blimc] 475.12 bound 766
c [blimc] 475.61 bound 767
c [blimc] 476.10 bound 768
c [blimc] 476.60 bound 769
c [blimc] 477.10 bound 770
c [blimc] 477.59 bound 771
c [blimc] 478.08 bound 772
c [blimc] 478.57 bound 773
c [blimc] 479.07 bound 774
[runlim] sample:		479.1 time, 480.3 real, 2286.3 MB
c [blimc] 479.56 bound 775
c [blimc] 480.05 bound 776
c [blimc] 480.55 bound 777
c [blimc] 481.04 bound 778
c [blimc] 481.54 bound 779
c [blimc] 482.04 bound 780
c [blimc] 482.53 bound 781
c [blimc] 483.03 bound 782
c [blimc] 483.53 bound 783
c [blimc] 484.03 bound 784
c [blimc] 484.53 bound 785
c [blimc] 485.03 bound 786
c [blimc] 485.53 bound 787
c [blimc] 486.03 bound 788
c [blimc] 486.54 bound 789
c [blimc] 487.05 bound 790
c [blimc] 487.55 bound 791
c [blimc] 488.06 bound 792
c [blimc] 488.56 bound 793
c [blimc] 489.07 bound 794
[runlim] sample:		489.1 time, 490.3 real, 2312.6 MB
c [blimc] 489.58 bound 795
c [blimc] 490.09 bound 796
c [blimc] 490.60 bound 797
c [blimc] 491.11 bound 798
c [blimc] 491.62 bound 799
c [blimc] 492.13 bound 800
c [blimc] 492.64 bound 801
c [blimc] 493.15 bound 802
c [blimc] 493.67 bound 803
c [blimc] 494.18 bound 804
c [blimc] 494.69 bound 805
c [blimc] 495.21 bound 806
c [blimc] 495.72 bound 807
c [blimc] 496.24 bound 808
c [blimc] 496.76 bound 809
c [blimc] 497.28 bound 810
c [blimc] 497.80 bound 811
c [blimc] 498.32 bound 812
c [blimc] 498.84 bound 813
[runlim] sample:		499.0 time, 500.3 real, 2746.0 MB
c [blimc] 499.36 bound 814
c [blimc] 499.88 bound 815
c [blimc] 500.40 bound 816
c [blimc] 500.93 bound 817
c [blimc] 501.45 bound 818
c [blimc] 501.98 bound 819
c [blimc] 502.50 bound 820
c [blimc] 503.03 bound 821
c [blimc] 503.56 bound 822
c [blimc] 504.09 bound 823
c [blimc] 504.62 bound 824
c [blimc] 505.14 bound 825
c [blimc] 505.67 bound 826
c [blimc] 506.20 bound 827
c [blimc] 506.73 bound 828
c [blimc] 507.27 bound 829
c [blimc] 507.80 bound 830
c [blimc] 508.33 bound 831
c [blimc] 508.87 bound 832
[runlim] sample:		509.0 time, 510.3 real, 2591.5 MB
c [blimc] 509.40 bound 833
c [blimc] 509.94 bound 834
c [blimc] 510.47 bound 835
c [blimc] 511.01 bound 836
c [blimc] 511.55 bound 837
c [blimc] 512.09 bound 838
c [blimc] 512.63 bound 839
c [blimc] 513.17 bound 840
c [blimc] 513.71 bound 841
c [blimc] 514.25 bound 842
c [blimc] 514.79 bound 843
c [blimc] 515.33 bound 844
c [blimc] 515.88 bound 845
c [blimc] 516.42 bound 846
c [blimc] 516.97 bound 847
c [blimc] 517.51 bound 848
c [blimc] 518.06 bound 849
c [blimc] 518.61 bound 850
[runlim] sample:		518.9 time, 520.3 real, 3219.9 MB
c [blimc] 519.15 bound 851
c [blimc] 519.70 bound 852
c [blimc] 520.25 bound 853
c [blimc] 520.79 bound 854
c [blimc] 521.35 bound 855
c [blimc] 521.90 bound 856
c [blimc] 522.45 bound 857
c [blimc] 523.00 bound 858
c [blimc] 523.55 bound 859
c [blimc] 524.11 bound 860
c [blimc] 524.66 bound 861
c [blimc] 525.22 bound 862
c [blimc] 525.78 bound 863
c [blimc] 526.34 bound 864
c [blimc] 526.90 bound 865
c [blimc] 527.45 bound 866
c [blimc] 528.01 bound 867
c [blimc] 528.57 bound 868
[runlim] sample:		528.9 time, 530.3 real, 3192.4 MB
c [blimc] 529.13 bound 869
c [blimc] 529.69 bound 870
c [blimc] 530.26 bound 871
c [blimc] 530.82 bound 872
c [blimc] 531.38 bound 873
c [blimc] 531.95 bound 874
c [blimc] 532.51 bound 875
c [blimc] 533.08 bound 876
c [blimc] 533.65 bound 877
c [blimc] 534.21 bound 878
c [blimc] 534.78 bound 879
c [blimc] 535.35 bound 880
c [blimc] 535.92 bound 881
c [blimc] 536.50 bound 882
c [blimc] 537.07 bound 883
c [blimc] 537.64 bound 884
c [blimc] 538.21 bound 885
c [blimc] 538.79 bound 886
[runlim] sample:		538.9 time, 540.3 real, 2517.4 MB
c [blimc] 539.36 bound 887
c [blimc] 539.93 bound 888
c [blimc] 540.51 bound 889
c [blimc] 541.09 bound 890
c [blimc] 541.66 bound 891
c [blimc] 542.24 bound 892
c [blimc] 542.82 bound 893
c [blimc] 543.40 bound 894
c [blimc] 543.98 bound 895
c [blimc] 544.56 bound 896
c [blimc] 545.14 bound 897
c [blimc] 545.72 bound 898
c [blimc] 546.30 bound 899
c [blimc] 546.89 bound 900
c [blimc] 547.47 bound 901
c [blimc] 548.06 bound 902
c [blimc] 548.65 bound 903
[runlim] sample:		548.8 time, 550.3 real, 2810.7 MB
c [blimc] 549.24 bound 904
c [blimc] 549.82 bound 905
c [blimc] 550.41 bound 906
c [blimc] 551.00 bound 907
c [blimc] 551.59 bound 908
c [blimc] 552.18 bound 909
c [blimc] 552.77 bound 910
c [blimc] 553.36 bound 911
c [blimc] 553.95 bound 912
c [blimc] 554.55 bound 913
c [blimc] 555.14 bound 914
c [blimc] 555.74 bound 915
c [blimc] 556.33 bound 916
c [blimc] 556.93 bound 917
c [blimc] 557.53 bound 918
c [blimc] 558.12 bound 919
c [blimc] 558.72 bound 920
[runlim] sample:		558.8 time, 560.3 real, 2510.9 MB
c [blimc] 559.32 bound 921
c [blimc] 559.92 bound 922
c [blimc] 560.52 bound 923
c [blimc] 561.12 bound 924
c [blimc] 561.72 bound 925
c [blimc] 562.33 bound 926
c [blimc] 562.93 bound 927
c [blimc] 563.53 bound 928
c [blimc] 564.14 bound 929
c [blimc] 564.74 bound 930
c [blimc] 565.35 bound 931
c [blimc] 565.96 bound 932
c [blimc] 566.57 bound 933
c [blimc] 567.18 bound 934
c [blimc] 567.79 bound 935
c [blimc] 568.40 bound 936
[runlim] sample:		568.7 time, 570.3 real, 3324.6 MB
c [blimc] 569.01 bound 937
c [blimc] 569.62 bound 938
c [blimc] 570.24 bound 939
c [blimc] 570.85 bound 940
c [blimc] 571.46 bound 941
c [blimc] 572.08 bound 942
c [blimc] 572.69 bound 943
c [blimc] 573.31 bound 944
c [blimc] 573.92 bound 945
c [blimc] 574.54 bound 946
c [blimc] 575.16 bound 947
c [blimc] 575.78 bound 948
c [blimc] 576.40 bound 949
c [blimc] 577.02 bound 950
c [blimc] 577.64 bound 951
c [blimc] 578.26 bound 952
[runlim] sample:		578.7 time, 580.3 real, 3581.2 MB
c [blimc] 578.89 bound 953
c [blimc] 579.51 bound 954
c [blimc] 580.14 bound 955
c [blimc] 580.76 bound 956
c [blimc] 581.39 bound 957
c [blimc] 582.01 bound 958
c [blimc] 582.64 bound 959
c [blimc] 583.27 bound 960
c [blimc] 583.90 bound 961
c [blimc] 584.53 bound 962
c [blimc] 585.16 bound 963
c [blimc] 585.79 bound 964
c [blimc] 586.42 bound 965
c [blimc] 587.05 bound 966
c [blimc] 587.69 bound 967
c [blimc] 588.32 bound 968
[runlim] sample:		588.7 time, 590.3 real, 3439.7 MB
c [blimc] 588.95 bound 969
c [blimc] 589.59 bound 970
c [blimc] 590.22 bound 971
c [blimc] 590.86 bound 972
c [blimc] 591.50 bound 973
c [blimc] 592.13 bound 974
c [blimc] 592.77 bound 975
c [blimc] 593.41 bound 976
c [blimc] 594.05 bound 977
c [blimc] 594.69 bound 978
c [blimc] 595.33 bound 979
c [blimc] 596.00 bound 980
c [blimc] 596.64 bound 981
c [blimc] 597.29 bound 982
c [blimc] 597.93 bound 983
[runlim] sample:		598.6 time, 600.3 real, 2819.2 MB
[runlim] sample:		608.6 time, 610.3 real, 2540.0 MB
[runlim] sample:		618.6 time, 620.3 real, 4182.9 MB
[runlim] sample:		628.6 time, 630.3 real, 3356.9 MB
[runlim] sample:		638.6 time, 640.3 real, 3206.7 MB
[runlim] sample:		648.6 time, 650.3 real, 3006.4 MB
[runlim] sample:		658.6 time, 660.3 real, 2244.3 MB
[runlim] sample:		668.6 time, 670.3 real, 2244.3 MB
c [blimc] 673.01 bound 984
c [blimc] 673.67 bound 985
c [blimc] 674.27 bound 986
c [blimc] 674.87 bound 987
c [blimc] 675.46 bound 988
c [blimc] 676.06 bound 989
c [blimc] 676.65 bound 990
c [blimc] 677.25 bound 991
c [blimc] 677.85 bound 992
c [blimc] 678.44 bound 993
[runlim] sample:		678.5 time, 680.3 real, 3194.2 MB
c [blimc] 679.04 bound 994
c [blimc] 679.64 bound 995
c [blimc] 680.25 bound 996
c [blimc] 680.85 bound 997
c [blimc] 681.45 bound 998
c [blimc] 682.05 bound 999
c [blimc] 682.65 bound 1000
c [lgl1000]  346.829  79% simplifying
c [lgl1000]    0.861   0% search
c [lgl1000] ==================================
c [lgl1000]  437.085 100% all
c [lgl1000] 
c [lgl1000]           996 conflicts,           2.3 confs/sec
c [lgl1000]             0 ternaries,           0.0 confs/ternary
c [lgl1000]             0 binaries,            0.0 confs/binary
c [lgl1000]           996 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]           996 decisions,           2.3 decis/sec,      1.0 decis/conflict
c [lgl1000]       4802593 propagations,    10987.8 props/sec,   4821.9 props/decision
c [lgl1000] 
c [lgl1000] 437.1 seconds, 4082.2 MB
c [blimc] 683.26 reached k = 1001
c [blimc] 683.26 cloned 0 solvers
c [blimc] 683.26 max 4084.0 MB
c [blimc] 683.40 exit 20
[runlim] end:			Thu Sep 17 12:36:03 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			685.27 seconds
[runlim] time:			683.39 seconds
[runlim] space:			4182.9 MB
[runlim] samples:		6850
