[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/viscoherencep2.aig
[runlim] start:			Sat Sep 19 04:32:38 2015
[runlim] main pid:		7423
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/viscoherencep2.aig
c [blimc] 0.00 MILOA 1657 8 37 1 1612
c [blimc] 0.00 BCJK 0 0 0 0 1612
c [blimc] 0.00 37 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:       1228 =  74% out of 1657
c [blimc] 0.00 inputs    in COI:          6 =  75% out of 8
c [blimc] 0.00 latches   in COI:         29 =  78% out of 37
c [blimc] 0.00 constants in COI:          0 =   0% out of 1
c [blimc] 0.00 ands      in COI:       1193 =  74% out of 1612
c [blimc] 0.00 encoded
c [blimc] 0.13 simplified
c [blimc] 0.13 extracted
c [lglopt]    0.126 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]    0.126 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]          4878 propagations,    38641.9 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 0.1 seconds, 1.0 MB
c [blimc] 0.13 mapped 159 variables
c [blimc] 0.13 maxk 1000
c [blimc] 0.13 bound 0
c [blimc] 0.13 bound 1
c [blimc] 0.13 bound 2
c [blimc] 0.13 bound 3
c [blimc] 0.23 bound 4
c [blimc] 0.26 bound 5
c [blimc] 0.26 bound 6
c [blimc] 0.29 bound 7
c [blimc] 0.29 bound 8
c [blimc] 0.30 bound 9
c [blimc] 0.36 bound 10
c [blimc] 0.42 bound 11
c [blimc] 0.44 bound 12
c [blimc] 0.46 bound 13
c [blimc] 0.48 bound 14
c [blimc] 0.58 bound 15
c [blimc] 0.59 bound 16
c [blimc] 0.60 bound 17
c [blimc] 0.72 bound 18
c [blimc] 0.74 bound 19
c [blimc] 0.78 bound 20
c [blimc] 0.97 bound 21
c [blimc] 0.99 bound 22
c [blimc] 1.16 bound 23
c [blimc] 1.18 bound 24
c [blimc] 1.20 bound 25
c [blimc] 1.37 bound 26
c [blimc] 1.40 bound 27
c [blimc] 1.78 bound 28
c [blimc] 1.99 bound 29
c [blimc] 2.19 bound 30
c [blimc] 2.23 bound 31
c [blimc] 3.02 bound 32
c [blimc] 3.24 bound 33
c [blimc] 3.49 bound 34
c [blimc] 3.94 bound 35
c [blimc] 3.98 bound 36
c [blimc] 4.49 bound 37
c [blimc] 4.51 bound 38
c [blimc] 5.03 bound 39
c [blimc] 5.32 bound 40
c [blimc] 5.84 bound 41
c [blimc] 5.87 bound 42
c [blimc] 6.23 bound 43
c [blimc] 6.60 bound 44
c [blimc] 7.22 bound 45
c [blimc] 7.62 bound 46
c [blimc] 8.24 bound 47
c [blimc] 8.74 bound 48
c [blimc] 9.11 bound 49
c [blimc] 9.50 bound 50
c [blimc] 9.91 bound 51
[runlim] sample:		10.0 time, 10.5 real, 11.7 MB
c [blimc] 10.43 bound 52
c [blimc] 10.86 bound 53
c [blimc] 12.47 bound 54
c [blimc] 13.25 bound 55
c [blimc] 13.70 bound 56
c [blimc] 14.49 bound 57
c [blimc] 14.93 bound 58
c [blimc] 15.39 bound 59
c [blimc] 15.85 bound 60
c [blimc] 15.89 bound 61
c [blimc] 16.38 bound 62
c [blimc] 16.89 bound 63
c [blimc] 17.44 bound 64
c [blimc] 17.95 bound 65
c [blimc] 18.50 bound 66
c [blimc] 19.05 bound 67
c [blimc] 19.62 bound 68
[runlim] sample:		20.0 time, 20.5 real, 18.7 MB
c [blimc] 20.30 bound 69
c [blimc] 21.38 bound 70
c [blimc] 21.96 bound 71
c [blimc] 23.90 bound 72
c [blimc] 24.95 bound 73
c [blimc] 24.99 bound 74
c [blimc] 25.58 bound 75
c [blimc] 26.19 bound 76
c [blimc] 26.77 bound 77
c [blimc] 27.42 bound 78
c [blimc] 28.19 bound 79
c [blimc] 28.85 bound 80
c [blimc] 29.54 bound 81
c [blimc] 29.58 bound 82
[runlim] sample:		30.0 time, 30.5 real, 22.9 MB
c [blimc] 30.25 bound 83
c [blimc] 31.02 bound 84
c [blimc] 31.72 bound 85
c [blimc] 32.43 bound 86
c [blimc] 33.13 bound 87
c [blimc] 33.97 bound 88
c [blimc] 34.72 bound 89
c [blimc] 35.48 bound 90
c [blimc] 36.91 bound 91
c [blimc] 37.64 bound 92
c [blimc] 39.14 bound 93
c [blimc] 39.91 bound 94
[runlim] sample:		40.0 time, 40.5 real, 22.0 MB
c [blimc] 40.65 bound 95
c [blimc] 41.48 bound 96
c [blimc] 42.23 bound 97
c [blimc] 43.01 bound 98
c [blimc] 43.82 bound 99
c [blimc] 44.58 bound 100
c [blimc] 44.62 bound 101
c [blimc] 45.44 bound 102
c [blimc] 46.26 bound 103
c [blimc] 47.07 bound 104
c [blimc] 47.90 bound 105
c [blimc] 47.95 bound 106
c [blimc] 47.99 bound 107
c [blimc] 49.00 bound 108
[runlim] sample:		49.9 time, 50.5 real, 32.7 MB
c [blimc] 49.95 bound 109
c [blimc] 50.88 bound 110
c [blimc] 51.81 bound 111
c [blimc] 52.90 bound 112
c [blimc] 53.91 bound 113
c [blimc] 54.98 bound 114
c [blimc] 55.91 bound 115
c [blimc] 56.89 bound 116
c [blimc] 58.77 bound 117
[runlim] sample:		59.9 time, 60.5 real, 32.1 MB
c [blimc] 60.62 bound 118
c [blimc] 61.57 bound 119
c [blimc] 63.54 bound 120
c [blimc] 64.49 bound 121
c [blimc] 64.54 bound 122
c [blimc] 64.58 bound 123
c [blimc] 64.60 bound 124
c [blimc] 64.62 bound 125
c [blimc] 64.64 bound 126
c [blimc] 64.67 bound 127
c [blimc] 65.67 bound 128
c [blimc] 65.72 bound 129
c [blimc] 65.76 bound 130
c [blimc] 66.92 bound 131
c [blimc] 69.89 bound 132
[runlim] sample:		69.9 time, 70.5 real, 28.7 MB
c [blimc] 71.04 bound 133
c [blimc] 72.19 bound 134
c [blimc] 73.33 bound 135
c [blimc] 74.58 bound 136
c [blimc] 75.93 bound 137
c [blimc] 77.19 bound 138
c [blimc] 78.61 bound 139
c [blimc] 79.88 bound 140
[runlim] sample:		79.9 time, 80.5 real, 34.4 MB
c [blimc] 81.30 bound 141
c [blimc] 82.53 bound 142
c [blimc] 83.93 bound 143
c [blimc] 85.45 bound 144
c [blimc] 87.05 bound 145
c [blimc] 88.48 bound 146
[runlim] sample:		89.9 time, 90.5 real, 39.2 MB
c [blimc] 89.98 bound 147
c [blimc] 91.37 bound 148
c [blimc] 92.89 bound 149
c [blimc] 94.35 bound 150
c [blimc] 95.70 bound 151
c [blimc] 97.19 bound 152
c [blimc] 98.66 bound 153
[runlim] sample:		99.9 time, 100.5 real, 45.5 MB
c [blimc] 100.21 bound 154
c [blimc] 104.23 bound 155
c [blimc] 106.13 bound 156
c [blimc] 107.67 bound 157
[runlim] sample:		109.9 time, 110.5 real, 47.6 MB
c [blimc] 111.57 bound 158
c [blimc] 115.52 bound 159
c [blimc] 119.45 bound 160
[runlim] sample:		119.9 time, 120.5 real, 50.9 MB
c [blimc] 122.90 bound 161
c [blimc] 124.77 bound 162
c [blimc] 127.05 bound 163
c [blimc] 128.87 bound 164
[runlim] sample:		129.9 time, 130.5 real, 46.3 MB
c [blimc] 130.72 bound 165
c [blimc] 132.51 bound 166
c [blimc] 134.30 bound 167
c [blimc] 136.15 bound 168
c [blimc] 138.08 bound 169
[runlim] sample:		139.8 time, 140.5 real, 46.5 MB
c [blimc] 139.96 bound 170
c [blimc] 141.60 bound 171
c [blimc] 143.45 bound 172
c [blimc] 145.18 bound 173
c [blimc] 146.91 bound 174
c [blimc] 148.31 bound 175
[runlim] sample:		149.8 time, 150.5 real, 46.5 MB
c [blimc] 150.17 bound 176
c [blimc] 151.55 bound 177
c [blimc] 153.32 bound 178
c [blimc] 155.23 bound 179
c [blimc] 156.57 bound 180
c [blimc] 158.04 bound 181
c [blimc] 159.65 bound 182
[runlim] sample:		159.8 time, 160.5 real, 46.7 MB
c [blimc] 161.31 bound 183
c [blimc] 162.98 bound 184
c [blimc] 164.63 bound 185
c [blimc] 166.25 bound 186
c [blimc] 167.94 bound 187
c [blimc] 169.58 bound 188
[runlim] sample:		169.8 time, 170.5 real, 47.0 MB
c [blimc] 171.45 bound 189
c [blimc] 173.04 bound 190
c [blimc] 174.71 bound 191
c [blimc] 176.37 bound 192
c [blimc] 178.13 bound 193
[runlim] sample:		179.8 time, 180.5 real, 47.2 MB
c [blimc] 180.18 bound 194
c [blimc] 181.78 bound 195
c [blimc] 183.67 bound 196
c [blimc] 185.44 bound 197
c [blimc] 187.36 bound 198
c [blimc] 189.01 bound 199
[runlim] sample:		189.8 time, 190.5 real, 47.4 MB
c [blimc] 193.67 bound 200
c [blimc] 195.59 bound 201
c [blimc] 198.04 bound 202
[runlim] sample:		199.8 time, 200.5 real, 49.3 MB
c [blimc] 199.87 bound 203
c [blimc] 202.09 bound 204
c [blimc] 204.94 bound 205
c [blimc] 207.44 bound 206
c [blimc] 209.67 bound 207
[runlim] sample:		209.8 time, 210.5 real, 50.5 MB
c [blimc] 211.93 bound 208
c [blimc] 214.16 bound 209
c [blimc] 216.59 bound 210
c [blimc] 219.03 bound 211
[runlim] sample:		219.8 time, 220.5 real, 51.2 MB
c [blimc] 221.23 bound 212
c [blimc] 223.40 bound 213
[runlim] sample:		229.8 time, 230.5 real, 58.7 MB
c [blimc] 229.94 bound 214
c [blimc] 234.68 bound 215
c [blimc] 238.32 bound 216
[runlim] sample:		239.8 time, 240.5 real, 47.8 MB
c [blimc] 243.78 bound 217
c [blimc] 247.87 bound 218
[runlim] sample:		249.8 time, 250.5 real, 48.7 MB
c [blimc] 250.21 bound 219
c [blimc] 252.42 bound 220
c [blimc] 254.91 bound 221
c [blimc] 257.08 bound 222
c [blimc] 259.61 bound 223
[runlim] sample:		259.7 time, 260.5 real, 51.4 MB
c [blimc] 262.16 bound 224
c [blimc] 264.74 bound 225
c [blimc] 266.91 bound 226
c [blimc] 269.56 bound 227
[runlim] sample:		269.7 time, 270.5 real, 51.9 MB
c [blimc] 272.58 bound 228
c [blimc] 274.78 bound 229
c [blimc] 277.00 bound 230
c [blimc] 279.33 bound 231
[runlim] sample:		279.7 time, 280.5 real, 53.4 MB
c [blimc] 281.44 bound 232
c [blimc] 284.13 bound 233
c [blimc] 286.72 bound 234
[runlim] sample:		289.7 time, 290.5 real, 54.6 MB
c [blimc] 290.22 bound 235
c [blimc] 292.21 bound 236
c [blimc] 294.54 bound 237
c [blimc] 297.42 bound 238
[runlim] sample:		299.7 time, 300.5 real, 56.9 MB
c [blimc] 300.01 bound 239
c [blimc] 302.17 bound 240
c [blimc] 305.07 bound 241
c [blimc] 307.89 bound 242
[runlim] sample:		309.7 time, 310.5 real, 57.6 MB
c [blimc] 310.49 bound 243
c [blimc] 313.49 bound 244
c [blimc] 316.29 bound 245
c [blimc] 318.80 bound 246
[runlim] sample:		319.7 time, 320.5 real, 64.4 MB
c [blimc] 321.08 bound 247
c [blimc] 323.52 bound 248
c [blimc] 326.76 bound 249
c [blimc] 329.65 bound 250
[runlim] sample:		329.7 time, 330.5 real, 58.7 MB
c [blimc] 332.82 bound 251
c [blimc] 335.69 bound 252
c [blimc] 339.42 bound 253
[runlim] sample:		339.7 time, 340.5 real, 59.1 MB
c [blimc] 342.85 bound 254
c [blimc] 346.18 bound 255
c [blimc] 348.95 bound 256
[runlim] sample:		349.6 time, 350.5 real, 66.6 MB
c [blimc] 352.13 bound 257
c [blimc] 355.73 bound 258
c [blimc] 358.89 bound 259
[runlim] sample:		359.6 time, 360.5 real, 67.5 MB
c [blimc] 361.90 bound 260
c [blimc] 364.97 bound 261
c [blimc] 368.60 bound 262
[runlim] sample:		369.6 time, 370.5 real, 67.7 MB
c [blimc] 371.88 bound 263
c [blimc] 375.87 bound 264
c [blimc] 378.97 bound 265
[runlim] sample:		379.6 time, 380.5 real, 60.7 MB
c [blimc] 382.32 bound 266
c [blimc] 385.26 bound 267
c [blimc] 388.19 bound 268
[runlim] sample:		389.6 time, 390.5 real, 61.6 MB
c [blimc] 391.67 bound 269
c [blimc] 394.99 bound 270
c [blimc] 398.27 bound 271
[runlim] sample:		399.6 time, 400.5 real, 62.5 MB
c [blimc] 401.22 bound 272
c [blimc] 405.30 bound 273
c [blimc] 408.85 bound 274
[runlim] sample:		409.6 time, 410.5 real, 63.0 MB
c [blimc] 411.78 bound 275
c [blimc] 414.27 bound 276
c [blimc] 418.17 bound 277
[runlim] sample:		419.6 time, 420.5 real, 63.4 MB
c [blimc] 421.13 bound 278
c [blimc] 424.62 bound 279
c [blimc] 429.00 bound 280
[runlim] sample:		429.6 time, 430.5 real, 63.6 MB
c [blimc] 433.11 bound 281
c [blimc] 436.27 bound 282
c [blimc] 439.19 bound 283
[runlim] sample:		439.6 time, 440.5 real, 64.1 MB
c [blimc] 442.17 bound 284
c [blimc] 445.86 bound 285
c [blimc] 449.25 bound 286
[runlim] sample:		449.6 time, 450.5 real, 64.9 MB
c [blimc] 453.69 bound 287
c [blimc] 458.31 bound 288
[runlim] sample:		459.6 time, 460.5 real, 65.3 MB
c [blimc] 462.66 bound 289
c [blimc] 466.99 bound 290
[runlim] sample:		469.5 time, 470.5 real, 65.9 MB
c [blimc] 470.65 bound 291
c [blimc] 473.87 bound 292
c [blimc] 476.88 bound 293
[runlim] sample:		479.5 time, 480.5 real, 66.0 MB
c [blimc] 481.18 bound 294
c [blimc] 488.59 bound 295
[runlim] sample:		489.5 time, 490.5 real, 69.5 MB
c [blimc] 492.30 bound 296
c [blimc] 496.97 bound 297
[runlim] sample:		499.5 time, 500.5 real, 67.0 MB
c [blimc] 500.16 bound 298
c [blimc] 508.36 bound 299
[runlim] sample:		509.5 time, 510.5 real, 66.3 MB
c [blimc] 515.20 bound 300
[runlim] sample:		519.5 time, 520.5 real, 66.1 MB
c [blimc] 524.53 bound 301
[runlim] sample:		529.5 time, 530.5 real, 77.8 MB
c [blimc] 533.67 bound 302
[runlim] sample:		539.5 time, 540.5 real, 95.0 MB
c [blimc] 541.48 bound 303
c [blimc] 548.21 bound 304
[runlim] sample:		549.5 time, 550.5 real, 66.7 MB
c [blimc] 552.21 bound 305
c [blimc] 556.20 bound 306
[runlim] sample:		559.5 time, 560.5 real, 67.0 MB
c [blimc] 561.00 bound 307
c [blimc] 565.69 bound 308
[runlim] sample:		569.4 time, 570.5 real, 67.4 MB
c [blimc] 569.65 bound 309
c [blimc] 577.65 bound 310
[runlim] sample:		579.4 time, 580.5 real, 67.8 MB
c [blimc] 583.44 bound 311
[runlim] sample:		589.4 time, 590.5 real, 80.0 MB
c [blimc] 591.70 bound 312
c [blimc] 595.86 bound 313
[runlim] sample:		599.4 time, 600.5 real, 81.9 MB
c [blimc] 604.40 bound 314
c [blimc] 608.48 bound 315
[runlim] sample:		609.4 time, 610.5 real, 71.1 MB
c [blimc] 612.43 bound 316
c [blimc] 616.84 bound 317
[runlim] sample:		619.4 time, 620.5 real, 71.5 MB
c [blimc] 622.61 bound 318
c [blimc] 626.00 bound 319
[runlim] sample:		629.4 time, 630.5 real, 71.8 MB
c [blimc] 630.71 bound 320
c [blimc] 636.50 bound 321
[runlim] sample:		639.4 time, 640.5 real, 72.3 MB
c [blimc] 641.59 bound 322
[runlim] sample:		649.4 time, 650.5 real, 83.9 MB
c [blimc] 651.71 bound 323
c [blimc] 657.34 bound 324
[runlim] sample:		659.3 time, 660.5 real, 70.1 MB
c [blimc] 663.76 bound 325
c [blimc] 669.15 bound 326
[runlim] sample:		669.3 time, 670.5 real, 66.1 MB
c [blimc] 675.43 bound 327
[runlim] sample:		679.3 time, 680.5 real, 75.1 MB
c [blimc] 679.65 bound 328
c [blimc] 684.64 bound 329
c [blimc] 688.99 bound 330
[runlim] sample:		689.3 time, 690.5 real, 75.6 MB
c [blimc] 694.41 bound 331
[runlim] sample:		699.3 time, 700.5 real, 90.6 MB
c [blimc] 700.28 bound 332
c [blimc] 705.70 bound 333
[runlim] sample:		709.3 time, 710.5 real, 76.2 MB
c [blimc] 711.29 bound 334
c [blimc] 716.22 bound 335
[runlim] sample:		719.3 time, 720.5 real, 77.0 MB
c [blimc] 723.56 bound 336
[runlim] sample:		729.3 time, 730.5 real, 91.9 MB
c [blimc] 729.46 bound 337
c [blimc] 734.36 bound 338
c [blimc] 738.70 bound 339
[runlim] sample:		739.2 time, 740.5 real, 78.0 MB
c [blimc] 744.35 bound 340
[runlim] sample:		749.2 time, 750.5 real, 77.7 MB
c [blimc] 751.85 bound 341
c [blimc] 757.58 bound 342
[runlim] sample:		759.2 time, 760.5 real, 77.9 MB
c [blimc] 764.55 bound 343
[runlim] sample:		769.2 time, 770.5 real, 78.4 MB
c [blimc] 770.21 bound 344
[runlim] sample:		779.2 time, 780.5 real, 89.2 MB
c [blimc] 779.46 bound 345
c [blimc] 786.36 bound 346
[runlim] sample:		789.2 time, 790.5 real, 78.6 MB
c [blimc] 791.82 bound 347
c [blimc] 797.64 bound 348
[runlim] sample:		799.2 time, 800.5 real, 79.0 MB
c [blimc] 803.40 bound 349
[runlim] sample:		809.2 time, 810.5 real, 87.8 MB
c [blimc] 812.59 bound 350
c [blimc] 818.66 bound 351
[runlim] sample:		819.2 time, 820.5 real, 75.8 MB
c [blimc] 824.23 bound 352
[runlim] sample:		829.2 time, 830.5 real, 89.4 MB
c [blimc] 834.58 bound 353
[runlim] sample:		839.1 time, 840.5 real, 76.2 MB
c [blimc] 840.04 bound 354
[runlim] sample:		849.1 time, 850.5 real, 89.9 MB
c [blimc] 851.29 bound 355
c [blimc] 856.43 bound 356
[runlim] sample:		859.1 time, 860.5 real, 74.9 MB
c [blimc] 861.27 bound 357
c [blimc] 868.07 bound 358
[runlim] sample:		869.1 time, 870.5 real, 72.3 MB
c [blimc] 875.20 bound 359
[runlim] sample:		879.1 time, 880.5 real, 75.6 MB
c [blimc] 880.69 bound 360
c [blimc] 887.05 bound 361
[runlim] sample:		889.1 time, 890.5 real, 72.9 MB
c [blimc] 893.12 bound 362
[runlim] sample:		899.1 time, 900.5 real, 93.6 MB
c [blimc] 899.15 bound 363
c [blimc] 905.10 bound 364
[runlim] sample:		909.1 time, 910.5 real, 76.5 MB
c [blimc] 912.55 bound 365
c [blimc] 919.04 bound 366
[runlim] sample:		919.1 time, 920.5 real, 58.5 MB
c [blimc] 925.06 bound 367
[runlim] sample:		929.0 time, 930.5 real, 76.9 MB
c [blimc] 932.61 bound 368
c [blimc] 938.93 bound 369
[runlim] sample:		939.0 time, 940.5 real, 58.7 MB
[runlim] sample:		949.0 time, 950.5 real, 90.0 MB
c [blimc] 951.26 bound 370
c [blimc] 958.15 bound 371
[runlim] sample:		959.0 time, 960.5 real, 79.6 MB
[runlim] sample:		969.0 time, 970.5 real, 93.7 MB
c [blimc] 969.71 bound 372
c [blimc] 977.11 bound 373
[runlim] sample:		979.0 time, 980.5 real, 74.8 MB
c [blimc] 987.61 bound 374
[runlim] sample:		989.0 time, 990.5 real, 75.0 MB
c [blimc] 994.58 bound 375
[runlim] sample:		999.0 time, 1000.5 real, 78.2 MB
c [blimc] 1001.16 bound 376
c [blimc] 1007.08 bound 377
[runlim] sample:		1009.0 time, 1010.5 real, 75.4 MB
c [blimc] 1013.28 bound 378
[runlim] sample:		1018.9 time, 1020.5 real, 97.7 MB
c [blimc] 1019.99 bound 379
c [blimc] 1027.00 bound 380
[runlim] sample:		1028.9 time, 1030.5 real, 75.9 MB
c [blimc] 1032.67 bound 381
[runlim] sample:		1038.9 time, 1040.5 real, 98.2 MB
c [blimc] 1039.57 bound 382
c [blimc] 1047.81 bound 383
[runlim] sample:		1048.9 time, 1050.5 real, 76.4 MB
c [blimc] 1054.48 bound 384
[runlim] sample:		1058.9 time, 1060.5 real, 79.7 MB
c [blimc] 1060.01 bound 385
[runlim] sample:		1068.9 time, 1070.5 real, 95.1 MB
c [blimc] 1069.64 bound 386
c [blimc] 1077.28 bound 387
[runlim] sample:		1078.9 time, 1080.5 real, 77.1 MB
c [blimc] 1084.82 bound 388
[runlim] sample:		1088.9 time, 1090.5 real, 80.6 MB
c [blimc] 1090.92 bound 389
c [blimc] 1097.58 bound 390
[runlim] sample:		1098.9 time, 1100.5 real, 77.5 MB
c [blimc] 1104.79 bound 391
[runlim] sample:		1108.8 time, 1110.5 real, 81.0 MB
c [blimc] 1113.15 bound 392
[runlim] sample:		1118.8 time, 1120.5 real, 94.9 MB
c [blimc] 1124.26 bound 393
[runlim] sample:		1128.8 time, 1130.5 real, 81.3 MB
c [blimc] 1131.07 bound 394
[runlim] sample:		1138.8 time, 1140.5 real, 102.5 MB
c [blimc] 1139.12 bound 395
[runlim] sample:		1148.8 time, 1150.5 real, 105.4 MB
c [blimc] 1151.17 bound 396
[runlim] sample:		1158.8 time, 1160.5 real, 131.4 MB
c [blimc] 1160.69 bound 397
[runlim] sample:		1168.8 time, 1170.5 real, 112.9 MB
c [blimc] 1169.03 bound 398
c [blimc] 1176.95 bound 399
[runlim] sample:		1178.8 time, 1180.5 real, 91.3 MB
c [blimc] 1188.30 bound 400
[runlim] sample:		1188.8 time, 1190.5 real, 91.5 MB
c [blimc] 1195.74 bound 401
[runlim] sample:		1198.8 time, 1200.5 real, 92.7 MB
c [blimc] 1203.52 bound 402
[runlim] sample:		1208.8 time, 1210.5 real, 92.8 MB
c [blimc] 1210.16 bound 403
[runlim] sample:		1218.7 time, 1220.5 real, 101.3 MB
c [blimc] 1221.83 bound 404
c [blimc] 1227.40 bound 405
[runlim] sample:		1228.7 time, 1230.5 real, 89.1 MB
c [blimc] 1238.16 bound 406
[runlim] sample:		1238.7 time, 1240.5 real, 86.2 MB
c [blimc] 1245.77 bound 407
[runlim] sample:		1248.7 time, 1250.5 real, 106.4 MB
c [blimc] 1252.83 bound 408
[runlim] sample:		1258.7 time, 1260.5 real, 89.9 MB
c [blimc] 1260.48 bound 409
c [blimc] 1268.29 bound 410
[runlim] sample:		1268.7 time, 1270.5 real, 86.9 MB
c [blimc] 1277.44 bound 411
[runlim] sample:		1278.7 time, 1280.5 real, 87.0 MB
c [blimc] 1284.52 bound 412
[runlim] sample:		1288.7 time, 1290.5 real, 90.4 MB
c [blimc] 1291.14 bound 413
[runlim] sample:		1298.7 time, 1300.5 real, 107.3 MB
c [blimc] 1300.25 bound 414
c [blimc] 1307.84 bound 415
[runlim] sample:		1308.6 time, 1310.5 real, 87.8 MB
c [blimc] 1315.44 bound 416
[runlim] sample:		1318.6 time, 1320.5 real, 91.2 MB
c [blimc] 1323.81 bound 417
[runlim] sample:		1328.6 time, 1330.5 real, 91.4 MB
c [blimc] 1332.49 bound 418
[runlim] sample:		1338.6 time, 1340.5 real, 92.9 MB
c [blimc] 1339.59 bound 419
c [blimc] 1348.02 bound 420
[runlim] sample:		1348.6 time, 1350.5 real, 89.1 MB
c [blimc] 1357.28 bound 421
[runlim] sample:		1358.6 time, 1360.5 real, 90.8 MB
c [blimc] 1365.59 bound 422
[runlim] sample:		1368.6 time, 1370.5 real, 96.9 MB
[runlim] sample:		1378.6 time, 1380.5 real, 115.6 MB
c [blimc] 1379.34 bound 423
[runlim] sample:		1388.5 time, 1390.5 real, 113.3 MB
c [blimc] 1392.98 bound 424
[runlim] sample:		1398.5 time, 1400.5 real, 97.1 MB
c [blimc] 1400.23 bound 425
[runlim] sample:		1408.5 time, 1410.5 real, 113.7 MB
c [blimc] 1413.05 bound 426
[runlim] sample:		1418.5 time, 1420.5 real, 113.9 MB
c [blimc] 1426.87 bound 427
[runlim] sample:		1428.5 time, 1430.5 real, 97.8 MB
[runlim] sample:		1438.5 time, 1440.5 real, 114.1 MB
c [blimc] 1440.38 bound 428
[runlim] sample:		1448.5 time, 1450.5 real, 114.1 MB
[runlim] sample:		1458.5 time, 1460.5 real, 143.1 MB
c [blimc] 1465.94 bound 429
[runlim] sample:		1468.5 time, 1470.5 real, 91.4 MB
c [blimc] 1477.45 bound 430
[runlim] sample:		1478.4 time, 1480.5 real, 91.7 MB
[runlim] sample:		1488.4 time, 1490.5 real, 110.3 MB
c [blimc] 1491.56 bound 431
[runlim] sample:		1498.4 time, 1500.5 real, 118.0 MB
c [blimc] 1503.27 bound 432
[runlim] sample:		1508.4 time, 1510.5 real, 92.0 MB
c [blimc] 1512.47 bound 433
[runlim] sample:		1518.4 time, 1520.5 real, 105.4 MB
c [blimc] 1525.80 bound 434
[runlim] sample:		1528.4 time, 1530.5 real, 105.3 MB
c [blimc] 1533.45 bound 435
[runlim] sample:		1538.4 time, 1540.5 real, 104.6 MB
c [blimc] 1539.72 bound 436
c [blimc] 1547.31 bound 437
[runlim] sample:		1548.4 time, 1550.5 real, 89.6 MB
[runlim] sample:		1558.3 time, 1560.5 real, 106.4 MB
c [blimc] 1559.74 bound 438
c [blimc] 1566.87 bound 439
[runlim] sample:		1568.3 time, 1570.5 real, 90.0 MB
[runlim] sample:		1578.3 time, 1580.5 real, 106.5 MB
c [blimc] 1580.94 bound 440
[runlim] sample:		1588.3 time, 1590.5 real, 106.8 MB
c [blimc] 1594.40 bound 441
[runlim] sample:		1598.3 time, 1600.5 real, 90.4 MB
c [blimc] 1600.88 bound 442
[runlim] sample:		1608.3 time, 1610.5 real, 109.4 MB
c [blimc] 1614.29 bound 443
[runlim] sample:		1618.3 time, 1620.5 real, 103.0 MB
c [blimc] 1623.76 bound 444
[runlim] sample:		1628.3 time, 1630.5 real, 90.8 MB
c [blimc] 1631.57 bound 445
[runlim] sample:		1638.3 time, 1640.5 real, 91.0 MB
c [blimc] 1638.58 bound 446
c [blimc] 1645.49 bound 447
[runlim] sample:		1648.3 time, 1650.5 real, 91.3 MB
c [blimc] 1653.23 bound 448
[runlim] sample:		1658.2 time, 1660.5 real, 91.4 MB
c [blimc] 1660.95 bound 449
[runlim] sample:		1668.2 time, 1670.5 real, 115.7 MB
c [blimc] 1668.26 bound 450
[runlim] sample:		1678.2 time, 1680.5 real, 108.9 MB
c [blimc] 1684.22 bound 451
[runlim] sample:		1688.2 time, 1690.5 real, 91.9 MB
c [blimc] 1691.85 bound 452
[runlim] sample:		1698.2 time, 1700.5 real, 109.6 MB
c [blimc] 1705.61 bound 453
[runlim] sample:		1708.2 time, 1710.5 real, 92.3 MB
c [blimc] 1714.42 bound 454
[runlim] sample:		1718.2 time, 1720.5 real, 92.4 MB
c [blimc] 1722.79 bound 455
[runlim] sample:		1728.2 time, 1730.5 real, 92.5 MB
c [blimc] 1731.42 bound 456
[runlim] sample:		1738.2 time, 1740.5 real, 110.2 MB
c [blimc] 1744.32 bound 457
[runlim] sample:		1748.2 time, 1750.5 real, 110.2 MB
[runlim] sample:		1758.1 time, 1760.5 real, 110.5 MB
c [blimc] 1760.05 bound 458
c [blimc] 1767.57 bound 459
[runlim] sample:		1768.1 time, 1770.5 real, 93.2 MB
c [blimc] 1776.36 bound 460
[runlim] sample:		1778.1 time, 1780.5 real, 93.3 MB
[runlim] sample:		1788.1 time, 1790.5 real, 110.7 MB
c [blimc] 1791.20 bound 461
c [blimc] 1797.99 bound 462
[runlim] sample:		1798.1 time, 1800.5 real, 93.7 MB
c [blimc] 1806.13 bound 463
[runlim] sample:		1808.1 time, 1810.5 real, 93.9 MB
[runlim] sample:		1818.1 time, 1820.5 real, 132.6 MB
c [blimc] 1825.33 bound 464
[runlim] sample:		1828.1 time, 1830.5 real, 93.9 MB
c [blimc] 1835.19 bound 465
[runlim] sample:		1838.0 time, 1840.5 real, 94.2 MB
[runlim] sample:		1848.0 time, 1850.5 real, 111.8 MB
c [blimc] 1850.81 bound 466
[runlim] sample:		1858.0 time, 1860.5 real, 119.7 MB
c [blimc] 1859.12 bound 467
c [blimc] 1866.82 bound 468
[runlim] sample:		1868.0 time, 1870.5 real, 94.6 MB
c [blimc] 1874.57 bound 469
[runlim] sample:		1878.0 time, 1880.5 real, 98.9 MB
c [blimc] 1883.66 bound 470
[runlim] sample:		1888.0 time, 1890.5 real, 99.1 MB
c [blimc] 1894.15 bound 471
[runlim] sample:		1898.0 time, 1900.5 real, 108.7 MB
[runlim] sample:		1908.0 time, 1910.5 real, 123.3 MB
c [blimc] 1909.53 bound 472
[runlim] sample:		1918.0 time, 1920.5 real, 123.2 MB
c [blimc] 1919.13 bound 473
[runlim] sample:		1928.0 time, 1930.5 real, 115.7 MB
c [blimc] 1929.82 bound 474
[runlim] sample:		1937.9 time, 1940.5 real, 123.8 MB
c [blimc] 1939.68 bound 475
c [blimc] 1947.31 bound 476
[runlim] sample:		1947.9 time, 1950.5 real, 95.8 MB
c [blimc] 1955.63 bound 477
[runlim] sample:		1957.9 time, 1960.5 real, 109.7 MB
c [blimc] 1964.30 bound 478
[runlim] sample:		1967.9 time, 1970.5 real, 109.9 MB
c [blimc] 1974.52 bound 479
[runlim] sample:		1977.9 time, 1980.5 real, 110.1 MB
c [blimc] 1982.01 bound 480
[runlim] sample:		1987.9 time, 1990.5 real, 110.5 MB
c [blimc] 1992.52 bound 481
[runlim] sample:		1997.9 time, 2000.5 real, 110.5 MB
c [blimc] 2000.59 bound 482
[runlim] sample:		2007.9 time, 2010.5 real, 110.9 MB
c [blimc] 2008.66 bound 483
c [blimc] 2017.73 bound 484
[runlim] sample:		2017.8 time, 2020.5 real, 77.9 MB
c [blimc] 2025.63 bound 485
[runlim] sample:		2027.8 time, 2030.5 real, 111.4 MB
c [blimc] 2032.79 bound 486
[runlim] sample:		2037.8 time, 2040.5 real, 111.6 MB
c [blimc] 2042.66 bound 487
[runlim] sample:		2047.8 time, 2050.5 real, 111.9 MB
c [blimc] 2050.02 bound 488
[runlim] sample:		2057.8 time, 2060.5 real, 134.2 MB
c [blimc] 2059.96 bound 489
[runlim] sample:		2067.8 time, 2070.5 real, 112.2 MB
c [blimc] 2068.72 bound 490
[runlim] sample:		2077.8 time, 2080.5 real, 134.8 MB
c [blimc] 2079.07 bound 491
[runlim] sample:		2087.8 time, 2090.5 real, 112.5 MB
c [blimc] 2087.93 bound 492
[runlim] sample:		2097.8 time, 2100.5 real, 135.3 MB
c [blimc] 2098.56 bound 493
[runlim] sample:		2107.8 time, 2110.5 real, 135.8 MB
c [blimc] 2108.50 bound 494
c [blimc] 2115.83 bound 495
[runlim] sample:		2117.7 time, 2120.5 real, 114.2 MB
c [blimc] 2123.44 bound 496
[runlim] sample:		2127.7 time, 2130.5 real, 115.3 MB
c [blimc] 2132.68 bound 497
[runlim] sample:		2137.7 time, 2140.5 real, 114.8 MB
c [blimc] 2141.55 bound 498
[runlim] sample:		2147.7 time, 2150.5 real, 115.6 MB
c [blimc] 2151.28 bound 499
[runlim] sample:		2157.7 time, 2160.5 real, 114.1 MB
c [blimc] 2159.58 bound 500
[runlim] sample:		2167.7 time, 2170.5 real, 107.1 MB
c [blimc] 2169.00 bound 501
[runlim] sample:		2177.7 time, 2180.5 real, 129.3 MB
c [blimc] 2181.84 bound 502
[runlim] sample:		2187.7 time, 2190.5 real, 107.3 MB
c [blimc] 2190.00 bound 503
[runlim] sample:		2197.7 time, 2200.5 real, 107.6 MB
c [blimc] 2199.40 bound 504
[runlim] sample:		2207.6 time, 2210.5 real, 127.4 MB
c [blimc] 2217.44 bound 505
[runlim] sample:		2217.6 time, 2220.5 real, 80.6 MB
c [blimc] 2225.45 bound 506
[runlim] sample:		2227.6 time, 2230.5 real, 108.2 MB
c [blimc] 2234.18 bound 507
[runlim] sample:		2237.6 time, 2240.5 real, 108.4 MB
[runlim] sample:		2247.6 time, 2250.5 real, 128.3 MB
c [blimc] 2257.48 bound 508
[runlim] sample:		2257.6 time, 2260.5 real, 114.4 MB
[runlim] sample:		2267.6 time, 2270.5 real, 128.4 MB
c [blimc] 2273.22 bound 509
[runlim] sample:		2277.6 time, 2280.5 real, 113.2 MB
c [blimc] 2283.14 bound 510
[runlim] sample:		2287.6 time, 2290.5 real, 113.4 MB
[runlim] sample:		2297.5 time, 2300.5 real, 124.7 MB
c [blimc] 2299.57 bound 511
[runlim] sample:		2307.5 time, 2310.5 real, 131.8 MB
[runlim] sample:		2317.5 time, 2320.5 real, 161.1 MB
c [blimc] 2318.84 bound 512
[runlim] sample:		2327.5 time, 2330.5 real, 113.8 MB
c [blimc] 2329.93 bound 513
[runlim] sample:		2337.5 time, 2340.5 real, 109.6 MB
c [blimc] 2338.54 bound 514
[runlim] sample:		2347.5 time, 2350.5 real, 114.1 MB
c [blimc] 2348.98 bound 515
[runlim] sample:		2357.5 time, 2360.5 real, 125.6 MB
[runlim] sample:		2367.5 time, 2370.5 real, 134.2 MB
c [blimc] 2367.93 bound 516
c [blimc] 2376.66 bound 517
[runlim] sample:		2377.4 time, 2380.5 real, 117.1 MB
[runlim] sample:		2387.4 time, 2390.5 real, 142.9 MB
c [blimc] 2392.96 bound 518
[runlim] sample:		2397.4 time, 2400.5 real, 123.7 MB
c [blimc] 2402.33 bound 519
[runlim] sample:		2407.4 time, 2410.5 real, 141.7 MB
[runlim] sample:		2417.4 time, 2420.5 real, 147.3 MB
c [blimc] 2418.39 bound 520
[runlim] sample:		2427.4 time, 2430.5 real, 139.5 MB
c [blimc] 2434.47 bound 521
[runlim] sample:		2437.4 time, 2440.5 real, 124.1 MB
[runlim] sample:		2447.4 time, 2450.5 real, 139.9 MB
c [blimc] 2451.59 bound 522
[runlim] sample:		2457.4 time, 2460.5 real, 124.5 MB
c [blimc] 2463.24 bound 523
[runlim] sample:		2467.3 time, 2470.5 real, 124.7 MB
c [blimc] 2473.64 bound 524
[runlim] sample:		2477.3 time, 2480.5 real, 124.7 MB
[runlim] sample:		2487.3 time, 2490.5 real, 140.5 MB
c [blimc] 2490.05 bound 525
[runlim] sample:		2497.3 time, 2500.5 real, 140.4 MB
[runlim] sample:		2507.3 time, 2510.5 real, 149.2 MB
c [blimc] 2508.04 bound 526
[runlim] sample:		2517.3 time, 2520.5 real, 148.9 MB
c [blimc] 2518.07 bound 527
[runlim] sample:		2527.3 time, 2530.5 real, 148.9 MB
c [blimc] 2530.56 bound 528
[runlim] sample:		2537.3 time, 2540.5 real, 125.7 MB
c [blimc] 2542.11 bound 529
[runlim] sample:		2547.3 time, 2550.5 real, 125.8 MB
c [blimc] 2550.93 bound 530
[runlim] sample:		2557.2 time, 2560.5 real, 141.9 MB
[runlim] sample:		2567.2 time, 2570.5 real, 150.9 MB
c [blimc] 2568.41 bound 531
[runlim] sample:		2577.2 time, 2580.5 real, 145.1 MB
c [blimc] 2584.41 bound 532
[runlim] sample:		2587.2 time, 2590.5 real, 126.5 MB
c [blimc] 2593.92 bound 533
[runlim] sample:		2597.2 time, 2600.5 real, 126.8 MB
[runlim] sample:		2607.2 time, 2610.5 real, 150.5 MB
c [blimc] 2609.22 bound 534
[runlim] sample:		2617.2 time, 2620.5 real, 112.0 MB
c [blimc] 2617.88 bound 535
c [blimc] 2625.80 bound 536
[runlim] sample:		2627.2 time, 2630.5 real, 112.3 MB
[runlim] sample:		2637.2 time, 2640.5 real, 132.6 MB
c [blimc] 2644.88 bound 537
[runlim] sample:		2647.1 time, 2650.5 real, 112.5 MB
[runlim] sample:		2657.1 time, 2660.5 real, 132.5 MB
c [blimc] 2661.85 bound 538
[runlim] sample:		2667.1 time, 2670.5 real, 112.6 MB
c [blimc] 2672.50 bound 539
[runlim] sample:		2677.1 time, 2680.5 real, 112.6 MB
c [blimc] 2685.20 bound 540
[runlim] sample:		2687.1 time, 2690.5 real, 113.0 MB
[runlim] sample:		2697.1 time, 2700.5 real, 133.3 MB
c [blimc] 2704.33 bound 541
[runlim] sample:		2707.1 time, 2710.5 real, 120.7 MB
c [blimc] 2715.63 bound 542
[runlim] sample:		2717.1 time, 2720.5 real, 120.8 MB
c [blimc] 2725.28 bound 543
[runlim] sample:		2727.1 time, 2730.5 real, 120.9 MB
[runlim] sample:		2737.0 time, 2740.5 real, 149.9 MB
c [blimc] 2739.16 bound 544
[runlim] sample:		2747.0 time, 2750.5 real, 121.1 MB
c [blimc] 2751.57 bound 545
[runlim] sample:		2757.0 time, 2760.5 real, 121.5 MB
c [blimc] 2762.86 bound 546
[runlim] sample:		2767.0 time, 2770.5 real, 121.3 MB
c [blimc] 2774.66 bound 547
[runlim] sample:		2777.0 time, 2780.5 real, 121.7 MB
c [blimc] 2785.16 bound 548
[runlim] sample:		2787.0 time, 2790.5 real, 121.7 MB
c [blimc] 2794.78 bound 549
[runlim] sample:		2797.0 time, 2800.5 real, 114.2 MB
c [blimc] 2803.29 bound 550
[runlim] sample:		2807.0 time, 2810.5 real, 114.4 MB
[runlim] sample:		2816.9 time, 2820.5 real, 135.7 MB
c [blimc] 2825.51 bound 551
[runlim] sample:		2826.9 time, 2830.5 real, 114.7 MB
[runlim] sample:		2836.9 time, 2840.5 real, 169.5 MB
c [blimc] 2838.40 bound 552
[runlim] sample:		2846.9 time, 2850.5 real, 114.8 MB
c [blimc] 2849.97 bound 553
[runlim] sample:		2856.9 time, 2860.5 real, 114.9 MB
c [blimc] 2862.76 bound 554
[runlim] sample:		2866.9 time, 2870.5 real, 115.3 MB
[runlim] sample:		2876.9 time, 2880.5 real, 136.6 MB
c [blimc] 2884.36 bound 555
[runlim] sample:		2886.9 time, 2890.5 real, 115.5 MB
c [blimc] 2892.12 bound 556
[runlim] sample:		2896.9 time, 2900.5 real, 115.6 MB
[runlim] sample:		2906.9 time, 2910.5 real, 170.9 MB
c [blimc] 2907.50 bound 557
[runlim] sample:		2916.8 time, 2920.5 real, 171.5 MB
c [blimc] 2919.51 bound 558
[runlim] sample:		2926.8 time, 2930.5 real, 116.1 MB
c [blimc] 2929.17 bound 559
[runlim] sample:		2936.8 time, 2940.5 real, 116.1 MB
c [blimc] 2940.89 bound 560
[runlim] sample:		2946.8 time, 2950.5 real, 116.1 MB
c [blimc] 2954.91 bound 561
[runlim] sample:		2956.8 time, 2960.5 real, 116.4 MB
c [blimc] 2966.03 bound 562
[runlim] sample:		2966.8 time, 2970.5 real, 116.5 MB
[runlim] sample:		2976.8 time, 2980.5 real, 140.7 MB
c [blimc] 2982.36 bound 563
[runlim] sample:		2986.8 time, 2990.5 real, 116.7 MB
c [blimc] 2992.58 bound 564
[runlim] sample:		2996.8 time, 3000.5 real, 121.6 MB
[runlim] sample:		3006.7 time, 3010.5 real, 141.2 MB
c [blimc] 3010.27 bound 565
[runlim] sample:		3016.7 time, 3020.5 real, 117.1 MB
c [blimc] 3020.95 bound 566
[runlim] sample:		3026.7 time, 3030.5 real, 117.1 MB
c [blimc] 3033.93 bound 567
[runlim] sample:		3036.7 time, 3040.5 real, 117.5 MB
c [blimc] 3045.08 bound 568
[runlim] sample:		3046.7 time, 3050.5 real, 117.7 MB
[runlim] sample:		3056.7 time, 3060.5 real, 147.8 MB
c [blimc] 3057.34 bound 569
[runlim] sample:		3066.7 time, 3070.5 real, 139.3 MB
[runlim] sample:		3076.7 time, 3080.5 real, 165.9 MB
c [blimc] 3081.20 bound 570
[runlim] sample:		3086.7 time, 3090.5 real, 117.9 MB
[runlim] sample:		3096.6 time, 3100.5 real, 139.7 MB
[runlim] sample:		3106.6 time, 3110.5 real, 166.5 MB
c [blimc] 3108.83 bound 571
[runlim] sample:		3116.6 time, 3120.5 real, 117.9 MB
c [blimc] 3121.09 bound 572
[runlim] sample:		3126.6 time, 3130.5 real, 143.0 MB
[runlim] sample:		3136.6 time, 3140.5 real, 143.0 MB
c [blimc] 3143.14 bound 573
[runlim] sample:		3146.6 time, 3150.5 real, 118.3 MB
[runlim] sample:		3156.6 time, 3160.5 real, 140.6 MB
c [blimc] 3163.12 bound 574
[runlim] sample:		3166.6 time, 3170.5 real, 118.5 MB
c [blimc] 3173.99 bound 575
[runlim] sample:		3176.6 time, 3180.5 real, 118.8 MB
[runlim] sample:		3186.5 time, 3190.5 real, 143.7 MB
c [blimc] 3189.84 bound 576
[runlim] sample:		3196.5 time, 3200.5 real, 141.0 MB
[runlim] sample:		3206.5 time, 3210.5 real, 166.3 MB
c [blimc] 3211.56 bound 577
[runlim] sample:		3216.5 time, 3220.5 real, 127.5 MB
c [blimc] 3225.30 bound 578
[runlim] sample:		3226.5 time, 3230.5 real, 127.6 MB
[runlim] sample:		3236.5 time, 3240.5 real, 149.5 MB
c [blimc] 3246.22 bound 579
[runlim] sample:		3246.5 time, 3250.5 real, 128.2 MB
[runlim] sample:		3256.5 time, 3260.5 real, 135.8 MB
[runlim] sample:		3266.4 time, 3270.5 real, 146.9 MB
c [blimc] 3266.51 bound 580
[runlim] sample:		3276.4 time, 3280.5 real, 158.5 MB
c [blimc] 3277.53 bound 581
[runlim] sample:		3286.4 time, 3290.5 real, 136.2 MB
c [blimc] 3296.34 bound 582
[runlim] sample:		3296.4 time, 3300.5 real, 120.6 MB
[runlim] sample:		3306.4 time, 3310.5 real, 136.8 MB
[runlim] sample:		3316.4 time, 3320.5 real, 147.3 MB
c [blimc] 3318.03 bound 583
[runlim] sample:		3326.4 time, 3330.5 real, 176.9 MB
[runlim] sample:		3336.4 time, 3340.5 real, 177.0 MB
c [blimc] 3337.40 bound 584
[runlim] sample:		3346.3 time, 3350.5 real, 129.0 MB
c [blimc] 3349.28 bound 585
[runlim] sample:		3356.3 time, 3360.5 real, 128.9 MB
c [blimc] 3361.39 bound 586
[runlim] sample:		3366.3 time, 3370.5 real, 129.2 MB
[runlim] sample:		3376.3 time, 3380.5 real, 137.6 MB
c [blimc] 3381.88 bound 587
[runlim] sample:		3386.3 time, 3390.5 real, 129.2 MB
[runlim] sample:		3396.3 time, 3400.5 real, 177.9 MB
c [blimc] 3405.33 bound 588
[runlim] sample:		3406.3 time, 3410.5 real, 113.2 MB
[runlim] sample:		3416.3 time, 3420.5 real, 137.7 MB
[runlim] sample:		3426.3 time, 3430.5 real, 148.5 MB
[runlim] sample:		3436.2 time, 3440.5 real, 156.8 MB
c [blimc] 3440.72 bound 589
[runlim] sample:		3446.2 time, 3450.5 real, 129.7 MB
c [blimc] 3450.67 bound 590
[runlim] sample:		3456.2 time, 3460.5 real, 129.8 MB
c [blimc] 3463.34 bound 591
[runlim] sample:		3466.2 time, 3470.5 real, 130.0 MB
c [blimc] 3475.05 bound 592
[runlim] sample:		3476.2 time, 3480.5 real, 130.2 MB
[runlim] sample:		3486.2 time, 3490.5 real, 189.2 MB
c [blimc] 3490.33 bound 593
[runlim] sample:		3496.2 time, 3500.5 real, 122.7 MB
[runlim] sample:		3506.2 time, 3510.5 real, 138.9 MB
c [blimc] 3511.70 bound 594
[runlim] sample:		3516.2 time, 3520.5 real, 130.7 MB
[runlim] sample:		3526.2 time, 3530.5 real, 180.2 MB
c [blimc] 3533.78 bound 595
[runlim] sample:		3536.1 time, 3540.5 real, 130.8 MB
c [blimc] 3545.71 bound 596
[runlim] sample:		3546.1 time, 3550.5 real, 129.4 MB
[runlim] sample:		3556.1 time, 3560.5 real, 180.5 MB
[runlim] sample:		3566.1 time, 3570.5 real, 180.8 MB
c [blimc] 3567.83 bound 597
[runlim] sample:		3576.1 time, 3580.5 real, 130.7 MB
c [blimc] 3581.26 bound 598
[runlim] sample:		3586.1 time, 3590.5 real, 131.3 MB
c [blimc] 3594.96 bound 599
s UNKNOWN
c [blimc]
c [blimc] CAUGHT SIGNAL 15
c [blimc]
c [lgl599clone552]   24.089  33% simplifying
c [lgl599clone552]   49.048  67% search
c [lgl599clone552] ==================================
c [lgl599clone552]   73.466 100% all
c [lgl599clone552] 
c [lgl599clone552]        581990 conflicts,        7921.9 confs/sec
c [lgl599clone552]         36458 ternaries,          16.0 confs/ternary
c [lgl599clone552]          9935 binaries,           58.6 confs/binary
c [lgl599clone552]            42 iterations,      13856.9 confs/iteration
c [lgl599clone552] 
c [lgl599clone552]             5 reductions,          0.1 redus/sec, 116398.0 confs/reduction
c [lgl599clone552]          4909 restarts,           66.8 rests/sec,    118.6 confs/restart
c [lgl599clone552]       3280164 decisions,       44648.7 decis/sec,      5.6 decis/conflict
c [lgl599clone552]      93206991 propagations,  1268708.5 props/sec,     28.4 props/decision
c [lgl599clone552] 
c [lgl599clone552] 73.5 seconds, 88.0 MB
c [lgl599]   23.567  32% simplifying
c [lgl599]   49.048  67% search
c [lgl599] ==================================
c [lgl599]   72.944 100% all
c [lgl599] 
c [lgl599]        581990 conflicts,        7978.6 confs/sec
c [lgl599]         36458 ternaries,          16.0 confs/ternary
c [lgl599]          9935 binaries,           58.6 confs/binary
c [lgl599]            42 iterations,      13856.9 confs/iteration
c [lgl599] 
c [lgl599]             5 reductions,          0.1 redus/sec, 116398.0 confs/reduction
c [lgl599]          4909 restarts,           67.3 rests/sec,    118.6 confs/restart
c [lgl599]       3280164 decisions,       44968.4 decis/sec,      5.6 decis/conflict
c [lgl599]      93206982 propagations,  1277792.9 props/sec,     28.4 props/decision
c [lgl599] 
c [lgl599] 72.9 seconds, 88.0 MB
c [blimc] 3595.69 reached k = 599
c [blimc] 3595.69 cloned 553 solvers
c [blimc] 3595.69 max 133.4 MB
c [blimc]
c [blimc] CAUGHT SIGNAL 15
c [blimc]
[runlim] end:			Sat Sep 19 05:32:38 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.24 seconds
[runlim] time:			3595.68 seconds
[runlim] space:			190.6 MB
[runlim] samples:		35997
