[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/pdtvistwoall3.aig
[runlim] start:			Sat Sep 19 05:20:22 2015
[runlim] main pid:		7774
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/pdtvistwoall3.aig
c [blimc] 0.00 MILOA 1776 30 33 1 1713
c [blimc] 0.00 BCJK 0 0 0 0 1713
c [blimc] 0.00 33 latches initialized to 0
c [blimc] 0.00 0 latches initialized to 1
c [blimc] 0.00 0 latches uninitialized
c [blimc] 0.00 literals  in COI:        472 =  27% out of 1776
c [blimc] 0.00 inputs    in COI:          6 =  20% out of 30
c [blimc] 0.00 latches   in COI:         31 =  94% out of 33
c [blimc] 0.00 constants in COI:          0 =   0% out of 1
c [blimc] 0.00 ands      in COI:        435 =  25% out of 1713
c [blimc] 0.00 encoded
c [blimc] 0.04 simplified
c [blimc] 0.04 extracted
c [lglopt]    0.035 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]    0.035 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]          5288 propagations,   149387.0 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 0.0 seconds, 0.2 MB
c [blimc] 0.04 mapped 94 variables
c [blimc] 0.04 maxk 1000
c [blimc] 0.04 bound 0
c [blimc] 0.04 bound 1
c [blimc] 0.04 bound 2
c [blimc] 0.05 bound 3
c [blimc] 0.05 bound 4
c [blimc] 0.07 bound 5
c [blimc] 0.07 bound 6
c [blimc] 0.08 bound 7
c [blimc] 0.08 bound 8
c [blimc] 0.09 bound 9
c [blimc] 0.09 bound 10
c [blimc] 0.10 bound 11
c [blimc] 0.10 bound 12
c [blimc] 0.12 bound 13
c [blimc] 0.14 bound 14
c [blimc] 0.14 bound 15
c [blimc] 0.15 bound 16
c [blimc] 0.16 bound 17
c [blimc] 0.16 bound 18
c [blimc] 0.18 bound 19
c [blimc] 0.18 bound 20
c [blimc] 0.19 bound 21
c [blimc] 0.24 bound 22
c [blimc] 0.24 bound 23
c [blimc] 0.24 bound 24
c [blimc] 0.25 bound 25
c [blimc] 0.30 bound 26
c [blimc] 0.30 bound 27
c [blimc] 0.30 bound 28
c [blimc] 0.33 bound 29
c [blimc] 0.33 bound 30
c [blimc] 0.33 bound 31
c [blimc] 0.33 bound 32
c [blimc] 0.33 bound 33
c [blimc] 0.38 bound 34
c [blimc] 0.39 bound 35
c [blimc] 0.41 bound 36
c [blimc] 0.46 bound 37
c [blimc] 0.46 bound 38
c [blimc] 0.51 bound 39
c [blimc] 0.51 bound 40
c [blimc] 0.52 bound 41
c [blimc] 0.52 bound 42
c [blimc] 0.52 bound 43
c [blimc] 0.52 bound 44
c [blimc] 0.60 bound 45
c [blimc] 0.60 bound 46
c [blimc] 0.60 bound 47
c [blimc] 0.60 bound 48
c [blimc] 0.60 bound 49
c [blimc] 0.64 bound 50
c [blimc] 0.65 bound 51
c [blimc] 0.65 bound 52
c [blimc] 0.65 bound 53
c [blimc] 0.65 bound 54
c [blimc] 0.66 bound 55
c [blimc] 0.67 bound 56
c [blimc] 0.91 bound 57
c [blimc] 0.99 bound 58
c [blimc] 1.25 bound 59
c [blimc] 1.26 bound 60
c [blimc] 1.47 bound 61
c [blimc] 1.48 bound 62
c [blimc] 1.48 bound 63
c [blimc] 1.49 bound 64
c [blimc] 1.69 bound 65
c [blimc] 1.70 bound 66
c [blimc] 2.02 bound 67
c [blimc] 2.14 bound 68
c [blimc] 2.15 bound 69
c [blimc] 2.28 bound 70
c [blimc] 2.28 bound 71
c [blimc] 2.28 bound 72
c [blimc] 2.29 bound 73
c [blimc] 2.29 bound 74
c [blimc] 2.29 bound 75
c [blimc] 2.30 bound 76
c [blimc] 2.31 bound 77
c [blimc] 2.44 bound 78
c [blimc] 2.45 bound 79
c [blimc] 2.46 bound 80
c [blimc] 2.62 bound 81
c [blimc] 2.62 bound 82
c [blimc] 2.71 bound 83
c [blimc] 2.72 bound 84
c [blimc] 2.84 bound 85
c [blimc] 2.84 bound 86
c [blimc] 2.85 bound 87
c [blimc] 2.99 bound 88
c [blimc] 2.99 bound 89
c [blimc] 2.99 bound 90
c [blimc] 2.99 bound 91
c [blimc] 2.99 bound 92
c [blimc] 3.00 bound 93
c [blimc] 3.00 bound 94
c [blimc] 3.01 bound 95
c [blimc] 3.22 bound 96
c [blimc] 3.22 bound 97
c [blimc] 3.39 bound 98
c [blimc] 3.39 bound 99
c [blimc] 3.39 bound 100
c [blimc] 3.57 bound 101
c [blimc] 3.57 bound 102
c [blimc] 3.57 bound 103
c [blimc] 3.57 bound 104
c [blimc] 3.58 bound 105
c [blimc] 3.58 bound 106
c [blimc] 3.59 bound 107
c [blimc] 3.83 bound 108
c [blimc] 3.83 bound 109
c [blimc] 3.83 bound 110
c [blimc] 3.84 bound 111
c [blimc] 3.85 bound 112
c [blimc] 4.00 bound 113
c [blimc] 4.00 bound 114
c [blimc] 4.00 bound 115
c [blimc] 4.00 bound 116
c [blimc] 4.01 bound 117
c [blimc] 4.59 bound 118
c [blimc] 4.78 bound 119
c [blimc] 4.99 bound 120
c [blimc] 4.99 bound 121
c [blimc] 4.99 bound 122
c [blimc] 4.99 bound 123
c [blimc] 4.99 bound 124
c [blimc] 5.00 bound 125
c [blimc] 5.01 bound 126
c [blimc] 5.02 bound 127
c [blimc] 5.23 bound 128
c [blimc] 5.46 bound 129
c [blimc] 5.47 bound 130
c [blimc] 5.70 bound 131
c [blimc] 5.71 bound 132
c [blimc] 5.99 bound 133
c [blimc] 6.21 bound 134
c [blimc] 6.22 bound 135
c [blimc] 6.23 bound 136
c [blimc] 6.48 bound 137
c [blimc] 6.77 bound 138
c [blimc] 7.00 bound 139
c [blimc] 7.00 bound 140
c [blimc] 7.00 bound 141
c [blimc] 7.00 bound 142
c [blimc] 7.01 bound 143
c [blimc] 7.09 bound 144
c [blimc] 7.09 bound 145
c [blimc] 7.09 bound 146
c [blimc] 7.43 bound 147
c [blimc] 7.44 bound 148
c [blimc] 7.45 bound 149
c [blimc] 7.46 bound 150
c [blimc] 7.76 bound 151
c [blimc] 8.06 bound 152
c [blimc] 8.08 bound 153
c [blimc] 9.49 bound 154
c [blimc] 9.52 bound 155
c [blimc] 9.88 bound 156
[runlim] sample:		10.0 time, 10.6 real, 7.8 MB
c [blimc] 10.23 bound 157
c [blimc] 10.24 bound 158
c [blimc] 10.61 bound 159
c [blimc] 11.03 bound 160
c [blimc] 11.05 bound 161
c [blimc] 11.42 bound 162
c [blimc] 11.44 bound 163
c [blimc] 11.45 bound 164
c [blimc] 11.81 bound 165
c [blimc] 12.15 bound 166
c [blimc] 13.34 bound 167
c [blimc] 14.02 bound 168
c [blimc] 14.42 bound 169
c [blimc] 15.00 bound 170
c [blimc] 15.56 bound 171
c [blimc] 15.98 bound 172
c [blimc] 16.00 bound 173
c [blimc] 16.02 bound 174
c [blimc] 16.03 bound 175
c [blimc] 16.47 bound 176
c [blimc] 16.93 bound 177
c [blimc] 17.37 bound 178
c [blimc] 17.83 bound 179
c [blimc] 17.84 bound 180
c [blimc] 18.29 bound 181
c [blimc] 18.79 bound 182
c [blimc] 19.70 bound 183
[runlim] sample:		20.0 time, 20.6 real, 11.0 MB
c [blimc] 21.02 bound 184
c [blimc] 21.93 bound 185
c [blimc] 22.81 bound 186
c [blimc] 23.79 bound 187
c [blimc] 24.36 bound 188
c [blimc] 24.94 bound 189
c [blimc] 26.35 bound 190
c [blimc] 26.87 bound 191
c [blimc] 27.42 bound 192
c [blimc] 27.94 bound 193
c [blimc] 28.46 bound 194
c [blimc] 28.48 bound 195
c [blimc] 29.01 bound 196
c [blimc] 29.03 bound 197
c [blimc] 29.58 bound 198
[runlim] sample:		29.9 time, 30.6 real, 16.9 MB
c [blimc] 30.15 bound 199
c [blimc] 30.71 bound 200
c [blimc] 31.28 bound 201
c [blimc] 31.85 bound 202
c [blimc] 31.87 bound 203
c [blimc] 33.10 bound 204
c [blimc] 33.12 bound 205
c [blimc] 33.82 bound 206
c [blimc] 34.35 bound 207
c [blimc] 35.31 bound 208
c [blimc] 36.29 bound 209
c [blimc] 37.78 bound 210
c [blimc] 38.45 bound 211
c [blimc] 39.21 bound 212
c [blimc] 39.85 bound 213
[runlim] sample:		40.0 time, 40.6 real, 15.8 MB
c [blimc] 40.97 bound 214
c [blimc] 42.48 bound 215
c [blimc] 44.32 bound 216
c [blimc] 45.72 bound 217
c [blimc] 46.79 bound 218
c [blimc] 48.56 bound 219
c [blimc] 49.53 bound 220
[runlim] sample:		49.9 time, 50.6 real, 19.0 MB
c [blimc] 50.44 bound 221
c [blimc] 51.41 bound 222
c [blimc] 52.42 bound 223
c [blimc] 53.99 bound 224
c [blimc] 54.95 bound 225
c [blimc] 55.92 bound 226
c [blimc] 55.94 bound 227
c [blimc] 56.86 bound 228
c [blimc] 57.89 bound 229
c [blimc] 59.39 bound 230
[runlim] sample:		59.9 time, 60.6 real, 20.4 MB
c [blimc] 60.66 bound 231
c [blimc] 60.68 bound 232
c [blimc] 61.30 bound 233
c [blimc] 61.94 bound 234
c [blimc] 62.60 bound 235
c [blimc] 62.89 bound 236
c [blimc] 62.91 bound 237
c [blimc] 63.55 bound 238
c [blimc] 64.25 bound 239
c [blimc] 64.27 bound 240
c [blimc] 64.29 bound 241
c [blimc] 64.31 bound 242
c [blimc] 65.01 bound 243
c [blimc] 65.74 bound 244
c [blimc] 66.51 bound 245
c [blimc] 66.52 bound 246
c [blimc] 66.55 bound 247
c [blimc] 66.58 bound 248
c [blimc] 67.37 bound 249
c [blimc] 68.15 bound 250
c [blimc] 68.93 bound 251
c [blimc] 69.71 bound 252
c [blimc] 69.72 bound 253
[runlim] sample:		69.9 time, 70.6 real, 26.3 MB
c [blimc] 70.55 bound 254
c [blimc] 71.37 bound 255
c [blimc] 72.35 bound 256
c [blimc] 73.18 bound 257
c [blimc] 74.02 bound 258
c [blimc] 74.06 bound 259
c [blimc] 74.94 bound 260
c [blimc] 75.80 bound 261
c [blimc] 76.70 bound 262
c [blimc] 77.59 bound 263
c [blimc] 78.42 bound 264
c [blimc] 79.28 bound 265
[runlim] sample:		79.9 time, 80.6 real, 27.6 MB
c [blimc] 80.98 bound 266
c [blimc] 82.32 bound 267
c [blimc] 83.98 bound 268
c [blimc] 84.02 bound 269
c [blimc] 85.09 bound 270
c [blimc] 86.20 bound 271
c [blimc] 87.37 bound 272
c [blimc] 88.24 bound 273
c [blimc] 89.19 bound 274
[runlim] sample:		89.9 time, 90.6 real, 29.2 MB
c [blimc] 90.06 bound 275
c [blimc] 91.05 bound 276
c [blimc] 91.95 bound 277
c [blimc] 92.83 bound 278
c [blimc] 93.91 bound 279
c [blimc] 95.28 bound 280
c [blimc] 96.20 bound 281
c [blimc] 96.23 bound 282
c [blimc] 97.14 bound 283
c [blimc] 98.05 bound 284
c [blimc] 99.00 bound 285
c [blimc] 99.02 bound 286
[runlim] sample:		99.9 time, 100.6 real, 30.6 MB
c [blimc] 99.97 bound 287
c [blimc] 99.98 bound 288
c [blimc] 100.94 bound 289
c [blimc] 101.91 bound 290
c [blimc] 102.90 bound 291
c [blimc] 103.86 bound 292
c [blimc] 103.88 bound 293
c [blimc] 103.90 bound 294
c [blimc] 104.93 bound 295
c [blimc] 104.96 bound 296
c [blimc] 106.00 bound 297
c [blimc] 106.03 bound 298
c [blimc] 106.06 bound 299
c [blimc] 106.08 bound 300
c [blimc] 106.10 bound 301
c [blimc] 106.12 bound 302
c [blimc] 107.21 bound 303
c [blimc] 108.28 bound 304
c [blimc] 109.35 bound 305
[runlim] sample:		109.9 time, 110.6 real, 35.9 MB
c [blimc] 110.48 bound 306
c [blimc] 111.60 bound 307
c [blimc] 112.76 bound 308
c [blimc] 113.91 bound 309
c [blimc] 115.09 bound 310
c [blimc] 116.23 bound 311
[runlim] sample:		119.8 time, 120.6 real, 46.2 MB
c [blimc] 121.50 bound 312
c [blimc] 121.53 bound 313
c [blimc] 122.68 bound 314
c [blimc] 123.92 bound 315
c [blimc] 125.02 bound 316
c [blimc] 126.11 bound 317
c [blimc] 127.21 bound 318
c [blimc] 128.29 bound 319
[runlim] sample:		129.8 time, 130.6 real, 37.0 MB
c [blimc] 130.34 bound 320
c [blimc] 131.40 bound 321
c [blimc] 131.42 bound 322
c [blimc] 133.16 bound 323
c [blimc] 136.80 bound 324
c [blimc] 137.89 bound 325
[runlim] sample:		139.8 time, 140.6 real, 46.2 MB
c [blimc] 147.22 bound 326
[runlim] sample:		149.8 time, 150.6 real, 46.2 MB
c [blimc] 150.46 bound 327
c [blimc] 156.98 bound 328
[runlim] sample:		159.8 time, 160.6 real, 46.3 MB
c [blimc] 167.04 bound 329
[runlim] sample:		169.8 time, 170.6 real, 46.3 MB
c [blimc] 174.39 bound 330
c [blimc] 178.54 bound 331
[runlim] sample:		179.8 time, 180.6 real, 46.4 MB
c [blimc] 181.85 bound 332
[runlim] sample:		189.8 time, 190.6 real, 46.4 MB
c [blimc] 193.86 bound 333
c [blimc] 197.26 bound 334
[runlim] sample:		199.8 time, 200.6 real, 35.7 MB
c [blimc] 206.79 bound 335
c [blimc] 207.99 bound 336
[runlim] sample:		209.8 time, 210.6 real, 49.8 MB
[runlim] sample:		219.7 time, 220.6 real, 52.8 MB
c [blimc] 220.59 bound 337
[runlim] sample:		229.7 time, 230.6 real, 46.6 MB
c [blimc] 230.52 bound 338
c [blimc] 235.33 bound 339
[runlim] sample:		239.7 time, 240.6 real, 55.0 MB
c [blimc] 242.68 bound 340
c [blimc] 243.88 bound 341
c [blimc] 245.03 bound 342
c [blimc] 245.05 bound 343
c [blimc] 245.07 bound 344
c [blimc] 246.21 bound 345
c [blimc] 247.39 bound 346
c [blimc] 248.56 bound 347
c [blimc] 248.58 bound 348
[runlim] sample:		249.7 time, 250.6 real, 47.2 MB
c [blimc] 249.76 bound 349
c [blimc] 250.94 bound 350
c [blimc] 250.97 bound 351
c [blimc] 252.17 bound 352
c [blimc] 252.19 bound 353
c [blimc] 252.22 bound 354
c [blimc] 252.24 bound 355
c [blimc] 252.26 bound 356
c [blimc] 252.29 bound 357
c [blimc] 253.55 bound 358
c [blimc] 254.80 bound 359
c [blimc] 256.09 bound 360
c [blimc] 257.34 bound 361
c [blimc] 258.64 bound 362
c [blimc] 258.67 bound 363
[runlim] sample:		259.7 time, 260.6 real, 47.6 MB
c [blimc] 259.93 bound 364
c [blimc] 261.25 bound 365
c [blimc] 262.61 bound 366
c [blimc] 263.94 bound 367
c [blimc] 265.44 bound 368
[runlim] sample:		269.7 time, 270.6 real, 52.0 MB
[runlim] sample:		279.7 time, 280.6 real, 67.0 MB
[runlim] sample:		289.7 time, 290.6 real, 71.2 MB
[runlim] sample:		299.6 time, 300.6 real, 80.6 MB
c [blimc] 303.29 bound 369
c [blimc] 304.65 bound 370
c [blimc] 306.24 bound 371
c [blimc] 307.65 bound 372
c [blimc] 309.00 bound 373
[runlim] sample:		309.6 time, 310.6 real, 42.5 MB
c [blimc] 310.42 bound 374
c [blimc] 311.90 bound 375
c [blimc] 313.31 bound 376
c [blimc] 314.79 bound 377
c [blimc] 316.25 bound 378
c [blimc] 317.72 bound 379
[runlim] sample:		319.6 time, 320.6 real, 43.3 MB
[runlim] sample:		329.6 time, 330.6 real, 59.0 MB
c [blimc] 333.14 bound 380
c [blimc] 334.61 bound 381
c [blimc] 336.23 bound 382
c [blimc] 337.74 bound 383
c [blimc] 339.21 bound 384
[runlim] sample:		339.6 time, 340.6 real, 47.7 MB
c [blimc] 340.77 bound 385
c [blimc] 342.30 bound 386
[runlim] sample:		349.6 time, 350.6 real, 58.7 MB
c [blimc] 353.80 bound 387
c [blimc] 355.25 bound 388
c [blimc] 356.66 bound 389
c [blimc] 358.07 bound 390
[runlim] sample:		359.6 time, 360.6 real, 46.2 MB
c [blimc] 359.63 bound 391
c [blimc] 368.22 bound 392
[runlim] sample:		369.6 time, 370.6 real, 39.8 MB
c [blimc] 369.70 bound 393
c [blimc] 371.14 bound 394
c [blimc] 372.60 bound 395
c [blimc] 374.52 bound 396
c [blimc] 376.42 bound 397
c [blimc] 377.67 bound 398
[runlim] sample:		379.6 time, 380.6 real, 44.5 MB
c [blimc] 380.66 bound 399
c [blimc] 382.46 bound 400
c [blimc] 384.31 bound 401
[runlim] sample:		389.6 time, 390.6 real, 58.0 MB
c [blimc] 392.54 bound 402
[runlim] sample:		399.5 time, 400.6 real, 56.2 MB
[runlim] sample:		409.5 time, 410.6 real, 59.1 MB
c [blimc] 413.20 bound 403
[runlim] sample:		419.5 time, 420.6 real, 56.0 MB
[runlim] sample:		429.5 time, 430.6 real, 74.3 MB
[runlim] sample:		439.5 time, 440.6 real, 77.1 MB
[runlim] sample:		449.5 time, 450.6 real, 80.7 MB
[runlim] sample:		459.5 time, 460.6 real, 108.8 MB
[runlim] sample:		469.5 time, 470.6 real, 110.4 MB
[runlim] sample:		479.5 time, 480.6 real, 111.8 MB
[runlim] sample:		489.5 time, 490.6 real, 113.1 MB
[runlim] sample:		499.4 time, 500.6 real, 113.4 MB
[runlim] sample:		509.4 time, 510.6 real, 113.9 MB
c [blimc] 515.05 bound 404
c [blimc] 516.98 bound 405
c [blimc] 518.85 bound 406
[runlim] sample:		519.4 time, 520.6 real, 43.8 MB
c [blimc] 520.71 bound 407
c [blimc] 520.73 bound 408
c [blimc] 522.38 bound 409
c [blimc] 524.28 bound 410
c [blimc] 524.31 bound 411
c [blimc] 524.33 bound 412
c [blimc] 524.36 bound 413
c [blimc] 524.38 bound 414
c [blimc] 524.40 bound 415
c [blimc] 526.34 bound 416
c [blimc] 526.36 bound 417
c [blimc] 526.39 bound 418
c [blimc] 528.12 bound 419
[runlim] sample:		529.4 time, 530.6 real, 45.1 MB
c [blimc] 530.09 bound 420
c [blimc] 532.08 bound 421
c [blimc] 533.28 bound 422
c [blimc] 535.34 bound 423
c [blimc] 537.33 bound 424
c [blimc] 539.32 bound 425
c [blimc] 539.36 bound 426
[runlim] sample:		539.4 time, 540.6 real, 50.8 MB
c [blimc] 539.41 bound 427
c [blimc] 541.49 bound 428
[runlim] sample:		549.4 time, 550.6 real, 63.6 MB
c [blimc] 552.10 bound 429
c [blimc] 554.20 bound 430
c [blimc] 554.24 bound 431
[runlim] sample:		559.4 time, 560.6 real, 66.0 MB
c [blimc] 559.90 bound 432
c [blimc] 562.07 bound 433
c [blimc] 564.94 bound 434
c [blimc] 567.08 bound 435
c [blimc] 569.26 bound 436
[runlim] sample:		569.4 time, 570.6 real, 66.1 MB
c [blimc] 571.66 bound 437
c [blimc] 573.84 bound 438
c [blimc] 576.12 bound 439
c [blimc] 578.37 bound 440
[runlim] sample:		579.4 time, 580.6 real, 66.2 MB
c [blimc] 580.58 bound 441
c [blimc] 584.21 bound 442
c [blimc] 586.46 bound 443
c [blimc] 588.44 bound 444
[runlim] sample:		589.3 time, 590.6 real, 66.4 MB
c [blimc] 590.95 bound 445
[runlim] sample:		599.3 time, 600.6 real, 67.7 MB
[runlim] sample:		609.3 time, 610.6 real, 67.7 MB
c [blimc] 616.28 bound 446
c [blimc] 616.31 bound 447
c [blimc] 616.33 bound 448
c [blimc] 616.35 bound 449
c [blimc] 616.37 bound 450
c [blimc] 618.40 bound 451
[runlim] sample:		619.3 time, 620.6 real, 68.0 MB
c [blimc] 620.71 bound 452
c [blimc] 623.02 bound 453
c [blimc] 625.40 bound 454
c [blimc] 627.72 bound 455
c [blimc] 627.74 bound 456
[runlim] sample:		629.3 time, 630.6 real, 68.1 MB
c [blimc] 630.16 bound 457
c [blimc] 632.54 bound 458
c [blimc] 635.03 bound 459
c [blimc] 637.50 bound 460
[runlim] sample:		639.3 time, 640.6 real, 68.2 MB
c [blimc] 639.97 bound 461
c [blimc] 642.45 bound 462
c [blimc] 644.73 bound 463
c [blimc] 647.14 bound 464
[runlim] sample:		649.3 time, 650.6 real, 67.7 MB
c [blimc] 649.50 bound 465
c [blimc] 651.82 bound 466
c [blimc] 651.86 bound 467
c [blimc] 654.24 bound 468
c [blimc] 656.54 bound 469
c [blimc] 656.58 bound 470
c [blimc] 658.95 bound 471
[runlim] sample:		659.3 time, 660.6 real, 67.9 MB
c [blimc] 661.45 bound 472
c [blimc] 661.48 bound 473
c [blimc] 663.66 bound 474
c [blimc] 666.05 bound 475
c [blimc] 668.56 bound 476
c [blimc] 668.58 bound 477
[runlim] sample:		669.3 time, 670.6 real, 68.1 MB
c [blimc] 671.09 bound 478
c [blimc] 673.59 bound 479
c [blimc] 676.15 bound 480
c [blimc] 678.68 bound 481
[runlim] sample:		679.2 time, 680.6 real, 68.2 MB
c [blimc] 681.23 bound 482
c [blimc] 683.84 bound 483
c [blimc] 686.37 bound 484
c [blimc] 688.99 bound 485
[runlim] sample:		689.2 time, 690.6 real, 68.3 MB
c [blimc] 691.50 bound 486
[runlim] sample:		699.2 time, 700.6 real, 72.2 MB
c [blimc] 701.70 bound 487
c [blimc] 704.35 bound 488
c [blimc] 706.94 bound 489
[runlim] sample:		709.2 time, 710.6 real, 73.7 MB
c [blimc] 710.07 bound 490
[runlim] sample:		719.2 time, 720.6 real, 73.7 MB
[runlim] sample:		729.2 time, 730.6 real, 75.0 MB
[runlim] sample:		739.2 time, 740.6 real, 84.6 MB
[runlim] sample:		749.2 time, 750.6 real, 91.0 MB
c [blimc] 752.22 bound 491
c [blimc] 754.96 bound 492
c [blimc] 757.64 bound 493
c [blimc] 757.68 bound 494
c [blimc] 757.72 bound 495
c [blimc] 757.74 bound 496
c [blimc] 757.77 bound 497
[runlim] sample:		759.2 time, 760.6 real, 54.3 MB
c [blimc] 760.48 bound 498
c [blimc] 760.52 bound 499
c [blimc] 760.54 bound 500
c [blimc] 763.29 bound 501
c [blimc] 763.32 bound 502
c [blimc] 763.35 bound 503
c [blimc] 763.38 bound 504
c [blimc] 763.41 bound 505
c [blimc] 766.26 bound 506
c [blimc] 766.31 bound 507
c [blimc] 766.36 bound 508
c [blimc] 766.41 bound 509
c [blimc] 766.43 bound 510
c [blimc] 767.40 bound 511
c [blimc] 767.44 bound 512
[runlim] sample:		769.2 time, 770.6 real, 66.2 MB
c [blimc] 771.20 bound 513
c [blimc] 771.25 bound 514
c [blimc] 773.20 bound 515
c [blimc] 773.23 bound 516
c [blimc] 775.85 bound 517
c [blimc] 777.65 bound 518
[runlim] sample:		779.1 time, 780.6 real, 62.6 MB
c [blimc] 779.42 bound 519
c [blimc] 781.28 bound 520
c [blimc] 783.18 bound 521
c [blimc] 785.68 bound 522
c [blimc] 787.73 bound 523
[runlim] sample:		789.1 time, 790.6 real, 63.3 MB
c [blimc] 789.57 bound 524
c [blimc] 791.55 bound 525
c [blimc] 793.40 bound 526
c [blimc] 798.51 bound 527
[runlim] sample:		799.1 time, 800.6 real, 64.5 MB
c [blimc] 800.36 bound 528
c [blimc] 802.22 bound 529
c [blimc] 804.12 bound 530
c [blimc] 806.10 bound 531
c [blimc] 807.98 bound 532
[runlim] sample:		809.1 time, 810.6 real, 64.7 MB
c [blimc] 809.95 bound 533
c [blimc] 811.86 bound 534
c [blimc] 813.77 bound 535
c [blimc] 815.73 bound 536
[runlim] sample:		819.1 time, 820.6 real, 73.0 MB
c [blimc] 820.79 bound 537
c [blimc] 822.73 bound 538
c [blimc] 822.76 bound 539
[runlim] sample:		829.1 time, 830.6 real, 73.6 MB
c [blimc] 838.75 bound 540
[runlim] sample:		839.1 time, 840.6 real, 86.2 MB
c [blimc] 840.78 bound 541
[runlim] sample:		849.1 time, 850.6 real, 86.2 MB
[runlim] sample:		859.1 time, 860.6 real, 86.2 MB
c [blimc] 868.18 bound 542
[runlim] sample:		869.0 time, 870.6 real, 59.1 MB
[runlim] sample:		879.0 time, 880.6 real, 81.2 MB
[runlim] sample:		889.0 time, 890.6 real, 92.6 MB
[runlim] sample:		899.0 time, 900.6 real, 101.7 MB
c [blimc] 902.30 bound 543
[runlim] sample:		909.0 time, 910.6 real, 82.3 MB
[runlim] sample:		919.0 time, 920.6 real, 92.3 MB
[runlim] sample:		929.0 time, 930.6 real, 107.1 MB
[runlim] sample:		939.0 time, 940.6 real, 110.9 MB
[runlim] sample:		949.0 time, 950.6 real, 110.9 MB
[runlim] sample:		959.0 time, 960.6 real, 91.3 MB
[runlim] sample:		969.0 time, 970.6 real, 113.6 MB
[runlim] sample:		978.9 time, 980.6 real, 95.0 MB
[runlim] sample:		988.9 time, 990.6 real, 119.3 MB
[runlim] sample:		998.9 time, 1000.6 real, 119.3 MB
[runlim] sample:		1008.9 time, 1010.6 real, 121.4 MB
[runlim] sample:		1018.9 time, 1020.6 real, 121.4 MB
[runlim] sample:		1028.9 time, 1030.6 real, 150.2 MB
[runlim] sample:		1038.9 time, 1040.6 real, 150.2 MB
[runlim] sample:		1048.9 time, 1050.6 real, 150.2 MB
[runlim] sample:		1058.9 time, 1060.6 real, 132.2 MB
[runlim] sample:		1068.9 time, 1070.6 real, 132.2 MB
[runlim] sample:		1078.8 time, 1080.6 real, 163.1 MB
[runlim] sample:		1088.8 time, 1090.6 real, 163.9 MB
[runlim] sample:		1098.8 time, 1100.6 real, 165.2 MB
[runlim] sample:		1108.8 time, 1110.6 real, 200.8 MB
[runlim] sample:		1118.8 time, 1120.6 real, 202.1 MB
[runlim] sample:		1128.8 time, 1130.6 real, 171.6 MB
[runlim] sample:		1138.8 time, 1140.6 real, 173.0 MB
[runlim] sample:		1148.8 time, 1150.6 real, 173.5 MB
[runlim] sample:		1158.8 time, 1160.6 real, 153.0 MB
[runlim] sample:		1168.8 time, 1170.6 real, 150.9 MB
[runlim] sample:		1178.7 time, 1180.6 real, 167.6 MB
[runlim] sample:		1188.7 time, 1190.6 real, 168.9 MB
[runlim] sample:		1198.7 time, 1200.6 real, 171.2 MB
[runlim] sample:		1208.7 time, 1210.6 real, 208.3 MB
[runlim] sample:		1218.7 time, 1220.6 real, 175.1 MB
[runlim] sample:		1228.7 time, 1230.6 real, 174.7 MB
[runlim] sample:		1238.7 time, 1240.6 real, 176.1 MB
[runlim] sample:		1248.7 time, 1250.6 real, 178.2 MB
[runlim] sample:		1258.7 time, 1260.6 real, 177.8 MB
[runlim] sample:		1268.7 time, 1270.6 real, 179.9 MB
[runlim] sample:		1278.7 time, 1280.6 real, 180.5 MB
[runlim] sample:		1288.7 time, 1290.6 real, 140.3 MB
c [blimc] 1293.38 bound 544
c [blimc] 1295.38 bound 545
c [blimc] 1297.38 bound 546
c [blimc] 1297.40 bound 547
c [blimc] 1297.41 bound 548
[runlim] sample:		1298.6 time, 1300.6 real, 69.2 MB
c [blimc] 1299.43 bound 549
c [blimc] 1299.46 bound 550
c [blimc] 1301.58 bound 551
c [blimc] 1303.64 bound 552
c [blimc] 1303.67 bound 553
c [blimc] 1305.73 bound 554
c [blimc] 1307.78 bound 555
[runlim] sample:		1308.6 time, 1310.6 real, 69.4 MB
c [blimc] 1309.96 bound 556
c [blimc] 1310.00 bound 557
c [blimc] 1312.01 bound 558
c [blimc] 1312.04 bound 559
c [blimc] 1314.09 bound 560
c [blimc] 1316.11 bound 561
c [blimc] 1316.15 bound 562
c [blimc] 1316.17 bound 563
c [blimc] 1316.21 bound 564
c [blimc] 1316.26 bound 565
c [blimc] 1316.31 bound 566
c [blimc] 1318.39 bound 567
c [blimc] 1318.43 bound 568
[runlim] sample:		1318.6 time, 1320.6 real, 69.1 MB
c [blimc] 1320.58 bound 569
c [blimc] 1322.63 bound 570
c [blimc] 1324.75 bound 571
c [blimc] 1326.85 bound 572
[runlim] sample:		1328.6 time, 1330.6 real, 69.3 MB
c [blimc] 1328.94 bound 573
c [blimc] 1329.03 bound 574
c [blimc] 1331.16 bound 575
c [blimc] 1333.30 bound 576
[runlim] sample:		1338.6 time, 1340.6 real, 71.7 MB
[runlim] sample:		1348.6 time, 1350.6 real, 85.1 MB
[runlim] sample:		1358.6 time, 1360.6 real, 90.1 MB
[runlim] sample:		1368.6 time, 1370.6 real, 104.7 MB
[runlim] sample:		1378.6 time, 1380.6 real, 122.7 MB
[runlim] sample:		1388.5 time, 1390.6 real, 122.7 MB
[runlim] sample:		1398.5 time, 1400.6 real, 127.5 MB
[runlim] sample:		1408.5 time, 1410.6 real, 130.6 MB
[runlim] sample:		1418.5 time, 1420.6 real, 132.6 MB
[runlim] sample:		1428.5 time, 1430.6 real, 132.6 MB
[runlim] sample:		1438.5 time, 1440.6 real, 187.8 MB
[runlim] sample:		1448.5 time, 1450.6 real, 187.8 MB
[runlim] sample:		1458.5 time, 1460.6 real, 191.0 MB
c [blimc] 1459.78 bound 577
c [blimc] 1460.72 bound 578
[runlim] sample:		1468.5 time, 1470.6 real, 77.9 MB
[runlim] sample:		1478.5 time, 1480.6 real, 87.0 MB
[runlim] sample:		1488.4 time, 1490.6 real, 103.1 MB
c [blimc] 1497.10 bound 579
[runlim] sample:		1498.4 time, 1500.6 real, 60.8 MB
c [blimc] 1499.28 bound 580
c [blimc] 1501.52 bound 581
c [blimc] 1503.76 bound 582
c [blimc] 1506.00 bound 583
[runlim] sample:		1508.4 time, 1510.6 real, 65.6 MB
[runlim] sample:		1518.4 time, 1520.6 real, 84.7 MB
[runlim] sample:		1528.4 time, 1530.6 real, 88.8 MB
[runlim] sample:		1538.4 time, 1540.6 real, 92.6 MB
[runlim] sample:		1548.4 time, 1550.6 real, 113.2 MB
[runlim] sample:		1558.4 time, 1560.6 real, 135.2 MB
[runlim] sample:		1568.4 time, 1570.6 real, 138.5 MB
[runlim] sample:		1578.3 time, 1580.6 real, 139.0 MB
[runlim] sample:		1588.3 time, 1590.6 real, 144.3 MB
c [blimc] 1588.98 bound 584
c [blimc] 1591.19 bound 585
c [blimc] 1591.23 bound 586
c [blimc] 1593.63 bound 587
[runlim] sample:		1598.3 time, 1600.6 real, 75.9 MB
[runlim] sample:		1608.3 time, 1610.6 real, 86.0 MB
[runlim] sample:		1618.3 time, 1620.6 real, 90.6 MB
[runlim] sample:		1628.3 time, 1630.6 real, 112.5 MB
[runlim] sample:		1638.3 time, 1640.6 real, 112.5 MB
[runlim] sample:		1648.3 time, 1650.6 real, 134.8 MB
[runlim] sample:		1658.3 time, 1660.6 real, 134.8 MB
[runlim] sample:		1668.3 time, 1670.6 real, 121.2 MB
[runlim] sample:		1678.2 time, 1680.6 real, 123.9 MB
[runlim] sample:		1688.2 time, 1690.6 real, 123.9 MB
c [blimc] 1689.71 bound 588
c [blimc] 1691.97 bound 589
c [blimc] 1694.38 bound 590
c [blimc] 1696.68 bound 591
[runlim] sample:		1698.2 time, 1700.6 real, 66.6 MB
[runlim] sample:		1708.2 time, 1710.6 real, 86.2 MB
c [blimc] 1711.02 bound 592
c [blimc] 1713.34 bound 593
c [blimc] 1715.64 bound 594
c [blimc] 1717.99 bound 595
[runlim] sample:		1718.2 time, 1720.6 real, 88.5 MB
c [blimc] 1720.29 bound 596
c [blimc] 1722.62 bound 597
c [blimc] 1724.92 bound 598
c [blimc] 1727.29 bound 599
[runlim] sample:		1728.2 time, 1730.6 real, 88.6 MB
c [blimc] 1729.63 bound 600
c [blimc] 1732.06 bound 601
c [blimc] 1734.49 bound 602
c [blimc] 1736.94 bound 603
[runlim] sample:		1738.2 time, 1740.6 real, 88.7 MB
[runlim] sample:		1748.2 time, 1750.6 real, 91.6 MB
[runlim] sample:		1758.2 time, 1760.6 real, 102.6 MB
[runlim] sample:		1768.2 time, 1770.6 real, 106.9 MB
[runlim] sample:		1778.2 time, 1780.6 real, 128.7 MB
[runlim] sample:		1788.1 time, 1790.6 real, 150.5 MB
[runlim] sample:		1798.1 time, 1800.6 real, 131.3 MB
[runlim] sample:		1808.1 time, 1810.6 real, 131.3 MB
[runlim] sample:		1818.1 time, 1820.6 real, 134.7 MB
[runlim] sample:		1828.1 time, 1830.6 real, 134.7 MB
[runlim] sample:		1838.1 time, 1840.6 real, 162.5 MB
[runlim] sample:		1848.1 time, 1850.6 real, 138.3 MB
[runlim] sample:		1858.1 time, 1860.6 real, 138.3 MB
[runlim] sample:		1868.1 time, 1870.6 real, 169.8 MB
[runlim] sample:		1878.0 time, 1880.6 real, 169.8 MB
[runlim] sample:		1888.0 time, 1890.6 real, 169.8 MB
[runlim] sample:		1898.0 time, 1900.6 real, 169.8 MB
[runlim] sample:		1908.0 time, 1910.6 real, 169.8 MB
[runlim] sample:		1918.0 time, 1920.6 real, 146.8 MB
c [blimc] 1922.63 bound 604
[runlim] sample:		1928.0 time, 1930.6 real, 73.6 MB
[runlim] sample:		1938.0 time, 1940.6 real, 84.7 MB
[runlim] sample:		1948.0 time, 1950.6 real, 100.2 MB
[runlim] sample:		1958.0 time, 1960.6 real, 122.2 MB
[runlim] sample:		1968.0 time, 1970.6 real, 122.5 MB
[runlim] sample:		1978.0 time, 1980.6 real, 144.5 MB
[runlim] sample:		1988.0 time, 1990.6 real, 124.2 MB
[runlim] sample:		1997.9 time, 2000.6 real, 148.2 MB
[runlim] sample:		2007.9 time, 2010.6 real, 131.0 MB
[runlim] sample:		2017.9 time, 2020.6 real, 131.0 MB
[runlim] sample:		2027.9 time, 2030.6 real, 158.5 MB
[runlim] sample:		2037.9 time, 2040.6 real, 134.7 MB
[runlim] sample:		2047.9 time, 2050.6 real, 134.7 MB
[runlim] sample:		2057.9 time, 2060.6 real, 134.7 MB
[runlim] sample:		2067.9 time, 2070.6 real, 166.2 MB
[runlim] sample:		2077.9 time, 2080.6 real, 166.2 MB
[runlim] sample:		2087.9 time, 2090.6 real, 137.4 MB
[runlim] sample:		2097.8 time, 2100.6 real, 148.6 MB
[runlim] sample:		2107.8 time, 2110.6 real, 148.6 MB
[runlim] sample:		2117.8 time, 2120.6 real, 149.5 MB
[runlim] sample:		2127.8 time, 2130.6 real, 150.6 MB
[runlim] sample:		2137.8 time, 2140.6 real, 150.6 MB
c [blimc] 2146.42 bound 605
[runlim] sample:		2147.8 time, 2150.6 real, 68.6 MB
c [blimc] 2148.96 bound 606
c [blimc] 2151.34 bound 607
c [blimc] 2153.74 bound 608
c [blimc] 2156.23 bound 609
c [blimc] 2156.28 bound 610
[runlim] sample:		2157.8 time, 2160.6 real, 69.0 MB
c [blimc] 2158.78 bound 611
c [blimc] 2158.82 bound 612
c [blimc] 2158.85 bound 613
c [blimc] 2158.87 bound 614
c [blimc] 2161.29 bound 615
c [blimc] 2163.71 bound 616
c [blimc] 2166.14 bound 617
[runlim] sample:		2167.8 time, 2170.6 real, 69.8 MB
c [blimc] 2168.57 bound 618
c [blimc] 2171.00 bound 619
c [blimc] 2173.42 bound 620
c [blimc] 2175.91 bound 621
[runlim] sample:		2177.8 time, 2180.6 real, 69.3 MB
c [blimc] 2178.34 bound 622
c [blimc] 2178.37 bound 623
c [blimc] 2178.42 bound 624
c [blimc] 2178.48 bound 625
c [blimc] 2179.71 bound 626
c [blimc] 2179.79 bound 627
c [blimc] 2182.23 bound 628
c [blimc] 2184.66 bound 629
c [blimc] 2187.14 bound 630
c [blimc] 2187.18 bound 631
[runlim] sample:		2187.8 time, 2190.6 real, 69.6 MB
[runlim] sample:		2197.8 time, 2200.6 real, 92.2 MB
[runlim] sample:		2207.7 time, 2210.6 real, 95.8 MB
[runlim] sample:		2217.7 time, 2220.6 real, 109.1 MB
[runlim] sample:		2227.7 time, 2230.6 real, 114.2 MB
[runlim] sample:		2237.7 time, 2240.6 real, 114.2 MB
[runlim] sample:		2247.7 time, 2250.6 real, 114.2 MB
[runlim] sample:		2257.7 time, 2260.6 real, 114.2 MB
[runlim] sample:		2267.7 time, 2270.6 real, 114.2 MB
c [blimc] 2272.45 bound 632
c [blimc] 2274.97 bound 633
c [blimc] 2277.48 bound 634
[runlim] sample:		2277.7 time, 2280.6 real, 69.5 MB
c [blimc] 2279.97 bound 635
c [blimc] 2280.07 bound 636
[runlim] sample:		2287.7 time, 2290.6 real, 79.5 MB
[runlim] sample:		2297.7 time, 2300.6 real, 93.8 MB
[runlim] sample:		2307.6 time, 2310.6 real, 97.1 MB
[runlim] sample:		2317.6 time, 2320.6 real, 114.3 MB
[runlim] sample:		2327.6 time, 2330.6 real, 114.3 MB
[runlim] sample:		2337.6 time, 2340.6 real, 114.3 MB
[runlim] sample:		2347.6 time, 2350.6 real, 114.3 MB
[runlim] sample:		2357.6 time, 2360.6 real, 143.1 MB
[runlim] sample:		2367.6 time, 2370.6 real, 143.9 MB
[runlim] sample:		2377.6 time, 2380.6 real, 147.3 MB
[runlim] sample:		2387.6 time, 2390.6 real, 147.3 MB
[runlim] sample:		2397.5 time, 2400.6 real, 177.3 MB
[runlim] sample:		2407.5 time, 2410.6 real, 177.3 MB
[runlim] sample:		2417.5 time, 2420.6 real, 152.0 MB
[runlim] sample:		2427.5 time, 2430.6 real, 152.5 MB
[runlim] sample:		2437.5 time, 2440.6 real, 153.4 MB
[runlim] sample:		2447.5 time, 2450.6 real, 155.4 MB
[runlim] sample:		2457.5 time, 2460.6 real, 156.6 MB
[runlim] sample:		2467.5 time, 2470.6 real, 157.5 MB
[runlim] sample:		2477.5 time, 2480.6 real, 158.4 MB
[runlim] sample:		2487.5 time, 2490.6 real, 158.4 MB
[runlim] sample:		2497.4 time, 2500.6 real, 136.4 MB
c [blimc] 2498.70 bound 637
c [blimc] 2501.27 bound 638
c [blimc] 2503.84 bound 639
c [blimc] 2506.47 bound 640
[runlim] sample:		2507.4 time, 2510.6 real, 70.2 MB
c [blimc] 2509.11 bound 641
[runlim] sample:		2517.4 time, 2520.6 real, 79.9 MB
[runlim] sample:		2527.4 time, 2530.6 real, 95.5 MB
[runlim] sample:		2537.4 time, 2540.6 real, 97.1 MB
[runlim] sample:		2547.4 time, 2550.6 real, 133.8 MB
[runlim] sample:		2557.4 time, 2560.6 real, 138.5 MB
[runlim] sample:		2567.4 time, 2570.6 real, 145.6 MB
[runlim] sample:		2577.4 time, 2580.6 real, 147.9 MB
[runlim] sample:		2587.3 time, 2590.6 real, 147.9 MB
[runlim] sample:		2597.3 time, 2600.6 real, 156.7 MB
[runlim] sample:		2607.3 time, 2610.6 real, 156.7 MB
[runlim] sample:		2617.3 time, 2620.6 real, 186.7 MB
[runlim] sample:		2627.3 time, 2630.6 real, 168.2 MB
[runlim] sample:		2637.3 time, 2640.6 real, 168.2 MB
[runlim] sample:		2647.3 time, 2650.6 real, 168.2 MB
[runlim] sample:		2657.3 time, 2660.6 real, 201.9 MB
[runlim] sample:		2667.3 time, 2670.6 real, 201.9 MB
[runlim] sample:		2677.3 time, 2680.6 real, 172.1 MB
[runlim] sample:		2687.3 time, 2690.6 real, 172.1 MB
[runlim] sample:		2697.2 time, 2700.6 real, 172.8 MB
c [blimc] 2699.70 bound 642
[runlim] sample:		2707.2 time, 2710.6 real, 81.6 MB
[runlim] sample:		2717.2 time, 2720.6 real, 96.7 MB
[runlim] sample:		2727.2 time, 2730.6 real, 99.0 MB
[runlim] sample:		2737.2 time, 2740.6 real, 99.8 MB
[runlim] sample:		2747.2 time, 2750.6 real, 118.3 MB
[runlim] sample:		2757.2 time, 2760.6 real, 146.1 MB
[runlim] sample:		2767.2 time, 2770.6 real, 146.0 MB
[runlim] sample:		2777.2 time, 2780.6 real, 146.8 MB
[runlim] sample:		2787.2 time, 2790.6 real, 146.8 MB
[runlim] sample:		2797.1 time, 2800.6 real, 175.3 MB
[runlim] sample:		2807.1 time, 2810.6 real, 175.3 MB
[runlim] sample:		2817.1 time, 2820.6 real, 151.6 MB
c [blimc] 2826.87 bound 643
c [blimc] 2826.95 bound 644
[runlim] sample:		2827.1 time, 2830.6 real, 69.5 MB
c [blimc] 2829.53 bound 645
c [blimc] 2832.10 bound 646
c [blimc] 2834.69 bound 647
[runlim] sample:		2837.1 time, 2840.6 real, 75.9 MB
c [blimc] 2837.40 bound 648
c [blimc] 2840.11 bound 649
c [blimc] 2840.14 bound 650
c [blimc] 2842.75 bound 651
c [blimc] 2842.79 bound 652
c [blimc] 2842.81 bound 653
c [blimc] 2842.84 bound 654
c [blimc] 2842.87 bound 655
c [blimc] 2842.89 bound 656
c [blimc] 2842.94 bound 657
c [blimc] 2842.98 bound 658
c [blimc] 2843.01 bound 659
c [blimc] 2845.69 bound 660
c [blimc] 2845.74 bound 661
c [blimc] 2845.76 bound 662
c [blimc] 2845.79 bound 663
c [blimc] 2845.94 bound 664
c [blimc] 2845.98 bound 665
[runlim] sample:		2847.1 time, 2850.6 real, 77.3 MB
c [blimc] 2848.70 bound 666
c [blimc] 2851.48 bound 667
c [blimc] 2851.52 bound 668
c [blimc] 2854.38 bound 669
c [blimc] 2854.42 bound 670
[runlim] sample:		2857.1 time, 2860.6 real, 89.9 MB
c [blimc] 2857.17 bound 671
c [blimc] 2859.98 bound 672
c [blimc] 2862.83 bound 673
c [blimc] 2862.86 bound 674
c [blimc] 2865.76 bound 675
[runlim] sample:		2867.1 time, 2870.6 real, 90.2 MB
c [blimc] 2868.73 bound 676
c [blimc] 2871.59 bound 677
c [blimc] 2874.54 bound 678
[runlim] sample:		2877.1 time, 2880.6 real, 90.3 MB
c [blimc] 2877.38 bound 679
c [blimc] 2880.27 bound 680
c [blimc] 2883.11 bound 681
c [blimc] 2886.02 bound 682
[runlim] sample:		2887.0 time, 2890.6 real, 90.4 MB
c [blimc] 2888.95 bound 683
c [blimc] 2891.80 bound 684
[runlim] sample:		2897.0 time, 2900.6 real, 95.7 MB
[runlim] sample:		2907.0 time, 2910.6 real, 111.9 MB
[runlim] sample:		2917.0 time, 2920.6 real, 111.9 MB
[runlim] sample:		2927.0 time, 2930.6 real, 116.8 MB
[runlim] sample:		2937.0 time, 2940.6 real, 122.6 MB
[runlim] sample:		2947.0 time, 2950.6 real, 122.6 MB
[runlim] sample:		2957.0 time, 2960.6 real, 122.6 MB
[runlim] sample:		2966.9 time, 2970.6 real, 150.7 MB
[runlim] sample:		2976.9 time, 2980.6 real, 150.7 MB
[runlim] sample:		2986.9 time, 2990.6 real, 150.7 MB
[runlim] sample:		2996.9 time, 3000.6 real, 178.7 MB
[runlim] sample:		3006.9 time, 3010.6 real, 155.4 MB
[runlim] sample:		3016.9 time, 3020.6 real, 155.4 MB
[runlim] sample:		3026.9 time, 3030.6 real, 188.4 MB
[runlim] sample:		3036.9 time, 3040.6 real, 188.4 MB
[runlim] sample:		3046.9 time, 3050.6 real, 159.8 MB
[runlim] sample:		3056.9 time, 3060.6 real, 159.8 MB
[runlim] sample:		3066.9 time, 3070.6 real, 159.8 MB
[runlim] sample:		3076.9 time, 3080.6 real, 197.0 MB
[runlim] sample:		3086.8 time, 3090.6 real, 172.0 MB
c [blimc] 3092.39 bound 685
[runlim] sample:		3096.8 time, 3100.6 real, 72.9 MB
c [blimc] 3097.47 bound 686
c [blimc] 3101.19 bound 687
[runlim] sample:		3106.8 time, 3110.6 real, 84.8 MB
[runlim] sample:		3116.8 time, 3120.6 real, 102.3 MB
[runlim] sample:		3126.8 time, 3130.6 real, 105.0 MB
[runlim] sample:		3136.8 time, 3140.6 real, 123.8 MB
[runlim] sample:		3146.8 time, 3150.6 real, 123.8 MB
[runlim] sample:		3156.8 time, 3160.6 real, 123.8 MB
[runlim] sample:		3166.8 time, 3170.6 real, 134.8 MB
[runlim] sample:		3176.7 time, 3180.6 real, 134.8 MB
[runlim] sample:		3186.7 time, 3190.6 real, 139.6 MB
[runlim] sample:		3196.7 time, 3200.6 real, 139.6 MB
[runlim] sample:		3206.7 time, 3210.6 real, 139.6 MB
[runlim] sample:		3216.7 time, 3220.6 real, 139.6 MB
[runlim] sample:		3226.7 time, 3230.6 real, 139.6 MB
[runlim] sample:		3236.7 time, 3240.6 real, 139.6 MB
[runlim] sample:		3246.7 time, 3250.6 real, 139.6 MB
[runlim] sample:		3256.7 time, 3260.6 real, 155.5 MB
[runlim] sample:		3266.7 time, 3270.6 real, 123.2 MB
[runlim] sample:		3276.7 time, 3280.6 real, 152.8 MB
[runlim] sample:		3286.6 time, 3290.6 real, 193.6 MB
[runlim] sample:		3296.6 time, 3300.6 real, 157.2 MB
c [blimc] 3297.80 bound 688
c [blimc] 3301.62 bound 689
c [blimc] 3305.53 bound 690
[runlim] sample:		3306.6 time, 3310.6 real, 79.3 MB
c [blimc] 3310.49 bound 691
[runlim] sample:		3316.6 time, 3320.6 real, 79.3 MB
[runlim] sample:		3326.6 time, 3330.6 real, 109.5 MB
[runlim] sample:		3336.6 time, 3340.6 real, 111.6 MB
[runlim] sample:		3346.6 time, 3350.6 real, 117.1 MB
[runlim] sample:		3356.6 time, 3360.6 real, 120.4 MB
[runlim] sample:		3366.6 time, 3370.6 real, 123.7 MB
[runlim] sample:		3376.5 time, 3380.6 real, 123.7 MB
[runlim] sample:		3386.5 time, 3390.6 real, 130.6 MB
[runlim] sample:		3396.5 time, 3400.6 real, 131.9 MB
[runlim] sample:		3406.5 time, 3410.6 real, 131.9 MB
[runlim] sample:		3416.5 time, 3420.6 real, 193.6 MB
[runlim] sample:		3426.5 time, 3430.6 real, 193.6 MB
[runlim] sample:		3436.5 time, 3440.6 real, 193.6 MB
[runlim] sample:		3446.5 time, 3450.6 real, 196.0 MB
[runlim] sample:		3456.5 time, 3460.6 real, 196.0 MB
c [blimc] 3464.77 bound 692
[runlim] sample:		3466.4 time, 3470.6 real, 73.8 MB
[runlim] sample:		3476.4 time, 3480.6 real, 102.8 MB
[runlim] sample:		3486.4 time, 3490.6 real, 106.9 MB
[runlim] sample:		3496.4 time, 3500.6 real, 109.4 MB
[runlim] sample:		3506.4 time, 3510.6 real, 109.4 MB
[runlim] sample:		3516.4 time, 3520.6 real, 133.5 MB
[runlim] sample:		3526.4 time, 3530.6 real, 158.5 MB
[runlim] sample:		3536.4 time, 3540.6 real, 158.5 MB
[runlim] sample:		3546.4 time, 3550.6 real, 163.8 MB
[runlim] sample:		3556.3 time, 3560.6 real, 163.8 MB
[runlim] sample:		3566.3 time, 3570.6 real, 152.6 MB
[runlim] sample:		3576.3 time, 3580.6 real, 125.3 MB
c [blimc] 3585.83 bound 693
[runlim] sample:		3586.3 time, 3590.6 real, 73.7 MB
c [blimc] 3588.58 bound 694
c [blimc] 3591.32 bound 695
c [blimc] 3594.10 bound 696
s UNKNOWN
c [blimc]
c [blimc] CAUGHT SIGNAL 15
c [blimc]
c [lgl696clone420]   31.841  56% simplifying
c [lgl696clone420]   24.875  44% search
c [lgl696clone420] ==================================
c [lgl696clone420]   56.955 100% all
c [lgl696clone420] 
c [lgl696clone420]        563988 conflicts,        9902.3 confs/sec
c [lgl696clone420]         21836 ternaries,          25.8 confs/ternary
c [lgl696clone420]          1175 binaries,          480.0 confs/binary
c [lgl696clone420]           913 iterations,        617.7 confs/iteration
c [lgl696clone420] 
c [lgl696clone420]             5 reductions,          0.1 redus/sec, 112797.6 confs/reduction
c [lgl696clone420]          1985 restarts,           34.9 rests/sec,    284.1 confs/restart
c [lgl696clone420]       8134377 decisions,      142820.0 decis/sec,     14.4 decis/conflict
c [lgl696clone420]      56907510 propagations,   999158.1 props/sec,      7.0 props/decision
c [lgl696clone420] 
c [lgl696clone420] 57.0 seconds, 52.3 MB
c [lgl696]   30.266  55% simplifying
c [lgl696]   24.875  45% search
c [lgl696] ==================================
c [lgl696]   55.379 100% all
c [lgl696] 
c [lgl696]        563988 conflicts,       10184.1 confs/sec
c [lgl696]         21836 ternaries,          25.8 confs/ternary
c [lgl696]          1175 binaries,          480.0 confs/binary
c [lgl696]           913 iterations,        617.7 confs/iteration
c [lgl696] 
c [lgl696]             5 reductions,          0.1 redus/sec, 112797.6 confs/reduction
c [lgl696]          1985 restarts,           35.8 rests/sec,    284.1 confs/restart
c [lgl696]       8134377 decisions,      146884.7 decis/sec,     14.4 decis/conflict
c [lgl696]      56907503 propagations,  1027594.6 props/sec,      7.0 props/decision
c [lgl696] 
c [lgl696] 55.4 seconds, 52.3 MB
c [blimc] 3595.73 reached k = 696
c [blimc] 3595.73 cloned 421 solvers
c [blimc] 3595.73 max 200.4 MB
c [blimc]
c [blimc] CAUGHT SIGNAL 15
c [blimc]
[runlim] end:			Sat Sep 19 06:20:22 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.10 seconds
[runlim] time:			3595.71 seconds
[runlim] space:			240.2 MB
[runlim] samples:		35994
