[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/intel009.aig
[runlim] start:			Sun Sep 20 21:26:18 2015
[runlim] main pid:		11494
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/intel009.aig
c [blimc] 0.01 MILOA 88731 5400 5399 1 77932
c [blimc] 0.01 BCJK 0 0 0 0 77932
c [blimc] 0.01 5399 latches initialized to 0
c [blimc] 0.01 0 latches initialized to 1
c [blimc] 0.01 0 latches uninitialized
c [blimc] 0.02 literals  in COI:      86249 =  97% out of 88731
c [blimc] 0.02 inputs    in COI:       5392 = 100% out of 5400
c [blimc] 0.02 latches   in COI:       2924 =  54% out of 5399
c [blimc] 0.02 constants in COI:          1 = 100% out of 1
c [blimc] 0.02 ands      in COI:      77932 = 100% out of 77932
c [blimc] 0.09 encoded
[runlim] sample:		10.0 time, 10.3 real, 33.3 MB
c [blimc] 15.48 simplified
c [blimc] 15.49 extracted
c [lglopt]   15.381 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]   15.383 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]        350827 propagations,    22806.1 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 15.4 seconds, 33.4 MB
c [blimc] 15.49 mapped 22162 variables
c [blimc] 15.49 maxk 1000
c [blimc] 15.49 bound 0
c [blimc] 16.18 bound 1
c [blimc] 17.85 bound 2
[runlim] sample:		19.9 time, 20.3 real, 35.5 MB
c [blimc] 21.54 bound 3
c [blimc] 21.58 bound 4
c [blimc] 25.39 bound 5
c [blimc] 25.44 bound 6
c [blimc] 25.48 bound 7
[runlim] sample:		29.9 time, 30.3 real, 79.7 MB
c [blimc] 35.92 bound 8
c [blimc] 35.97 bound 9
c [blimc] 36.02 bound 10
c [blimc] 36.08 bound 11
c [blimc] 36.14 bound 12
[runlim] sample:		39.9 time, 40.3 real, 117.3 MB
c [blimc] 45.79 bound 13
c [blimc] 45.85 bound 14
c [blimc] 45.90 bound 15
c [blimc] 45.96 bound 16
c [blimc] 46.03 bound 17
c [blimc] 46.09 bound 18
c [blimc] 46.16 bound 19
c [blimc] 46.22 bound 20
[runlim] sample:		49.9 time, 50.3 real, 194.4 MB
[runlim] sample:		59.9 time, 60.3 real, 194.4 MB
c [blimc] 66.38 bound 21
c [blimc] 66.45 bound 22
c [blimc] 66.52 bound 23
c [blimc] 66.59 bound 24
c [blimc] 66.66 bound 25
c [blimc] 66.74 bound 26
c [blimc] 66.82 bound 27
c [blimc] 66.89 bound 28
c [blimc] 66.97 bound 29
c [blimc] 67.05 bound 30
c [blimc] 67.13 bound 31
c [blimc] 67.21 bound 32
[runlim] sample:		69.9 time, 70.3 real, 184.2 MB
[runlim] sample:		79.9 time, 80.3 real, 251.1 MB
c [blimc] 81.44 bound 33
c [blimc] 81.53 bound 34
c [blimc] 81.62 bound 35
c [blimc] 81.72 bound 36
c [blimc] 81.81 bound 37
c [blimc] 81.91 bound 38
c [blimc] 82.01 bound 39
c [blimc] 82.11 bound 40
c [blimc] 82.21 bound 41
c [blimc] 82.32 bound 42
c [blimc] 82.42 bound 43
c [blimc] 82.53 bound 44
c [blimc] 82.64 bound 45
c [blimc] 82.76 bound 46
c [blimc] 82.86 bound 47
c [blimc] 82.99 bound 48
c [blimc] 83.10 bound 49
c [blimc] 83.24 bound 50
c [blimc] 83.36 bound 51
[runlim] sample:		89.9 time, 90.3 real, 358.5 MB
c [blimc] 98.12 bound 52
c [blimc] 98.24 bound 53
c [blimc] 98.46 bound 54
c [blimc] 98.59 bound 55
c [blimc] 98.71 bound 56
c [blimc] 98.85 bound 57
c [blimc] 99.02 bound 58
c [blimc] 99.15 bound 59
c [blimc] 99.29 bound 60
c [blimc] 99.42 bound 61
c [blimc] 99.69 bound 62
c [blimc] 99.83 bound 63
[runlim] sample:		99.9 time, 100.3 real, 457.4 MB
c [blimc] 99.98 bound 64
c [blimc] 100.13 bound 65
c [blimc] 100.33 bound 66
c [blimc] 100.47 bound 67
c [blimc] 100.62 bound 68
c [blimc] 100.76 bound 69
c [blimc] 100.98 bound 70
c [blimc] 101.13 bound 71
c [blimc] 101.28 bound 72
c [blimc] 101.43 bound 73
c [blimc] 101.82 bound 74
c [blimc] 101.96 bound 75
c [blimc] 102.12 bound 76
c [blimc] 102.27 bound 77
c [blimc] 102.52 bound 78
c [blimc] 102.68 bound 79
c [blimc] 102.85 bound 80
c [blimc] 103.00 bound 81
c [blimc] 103.28 bound 82
[runlim] sample:		109.9 time, 110.3 real, 577.3 MB
[runlim] sample:		119.8 time, 120.3 real, 444.4 MB
c [blimc] 121.46 bound 83
c [blimc] 121.65 bound 84
c [blimc] 121.81 bound 85
c [blimc] 122.25 bound 86
c [blimc] 122.42 bound 87
c [blimc] 122.58 bound 88
c [blimc] 122.75 bound 89
c [blimc] 123.01 bound 90
c [blimc] 123.18 bound 91
c [blimc] 123.35 bound 92
c [blimc] 123.52 bound 93
c [blimc] 123.96 bound 94
c [blimc] 124.15 bound 95
c [blimc] 124.34 bound 96
c [blimc] 124.52 bound 97
c [blimc] 124.82 bound 98
c [blimc] 124.99 bound 99
c [blimc] 125.19 bound 100
c [blimc] 125.36 bound 101
c [blimc] 125.69 bound 102
c [blimc] 125.87 bound 103
c [blimc] 126.08 bound 104
c [blimc] 126.25 bound 105
c [blimc] 126.80 bound 106
c [blimc] 126.98 bound 107
c [blimc] 127.19 bound 108
c [blimc] 127.37 bound 109
[runlim] sample:		129.8 time, 130.3 real, 709.5 MB
[runlim] sample:		139.8 time, 140.3 real, 907.4 MB
[runlim] sample:		149.8 time, 150.3 real, 944.0 MB
[runlim] sample:		159.8 time, 160.3 real, 925.9 MB
[runlim] sample:		169.8 time, 170.3 real, 988.7 MB
[runlim] sample:		179.8 time, 180.3 real, 927.6 MB
[runlim] sample:		189.8 time, 190.3 real, 973.0 MB
[runlim] sample:		199.8 time, 200.3 real, 904.3 MB
[runlim] sample:		209.8 time, 210.3 real, 959.0 MB
[runlim] sample:		219.7 time, 220.3 real, 959.0 MB
[runlim] sample:		229.7 time, 230.3 real, 959.0 MB
[runlim] sample:		239.7 time, 240.3 real, 886.5 MB
c [blimc] 240.22 bound 110
c [blimc] 240.48 bound 111
c [blimc] 240.72 bound 112
c [blimc] 240.90 bound 113
[runlim] sample:		249.7 time, 250.3 real, 733.4 MB
[runlim] sample:		259.7 time, 260.3 real, 784.2 MB
[runlim] sample:		269.7 time, 270.3 real, 499.3 MB
[runlim] sample:		279.7 time, 280.3 real, 938.0 MB
[runlim] sample:		289.7 time, 290.3 real, 829.8 MB
[runlim] sample:		299.7 time, 300.3 real, 972.2 MB
[runlim] sample:		309.6 time, 310.3 real, 882.1 MB
[runlim] sample:		319.6 time, 320.3 real, 950.6 MB
[runlim] sample:		329.6 time, 330.3 real, 871.3 MB
[runlim] sample:		339.6 time, 340.3 real, 941.9 MB
[runlim] sample:		349.6 time, 350.3 real, 941.9 MB
[runlim] sample:		359.6 time, 360.3 real, 869.2 MB
[runlim] sample:		369.6 time, 370.3 real, 930.7 MB
[runlim] sample:		379.6 time, 380.3 real, 850.8 MB
[runlim] sample:		389.6 time, 390.3 real, 925.7 MB
[runlim] sample:		399.6 time, 400.3 real, 925.7 MB
[runlim] sample:		409.6 time, 410.3 real, 841.8 MB
[runlim] sample:		419.6 time, 420.3 real, 906.3 MB
[runlim] sample:		429.6 time, 430.3 real, 916.7 MB
[runlim] sample:		439.6 time, 440.3 real, 916.7 MB
[runlim] sample:		449.5 time, 450.3 real, 905.3 MB
[runlim] sample:		459.5 time, 460.3 real, 916.7 MB
[runlim] sample:		469.5 time, 470.3 real, 838.0 MB
[runlim] sample:		479.5 time, 480.3 real, 904.9 MB
[runlim] sample:		489.5 time, 490.3 real, 916.3 MB
[runlim] sample:		499.5 time, 500.3 real, 837.7 MB
[runlim] sample:		509.5 time, 510.3 real, 838.6 MB
[runlim] sample:		519.5 time, 520.3 real, 906.8 MB
[runlim] sample:		529.5 time, 530.3 real, 918.3 MB
[runlim] sample:		539.5 time, 540.3 real, 839.9 MB
[runlim] sample:		549.4 time, 550.3 real, 869.4 MB
[runlim] sample:		559.4 time, 560.3 real, 841.2 MB
[runlim] sample:		569.4 time, 570.3 real, 842.6 MB
[runlim] sample:		579.4 time, 580.3 real, 842.6 MB
[runlim] sample:		589.4 time, 590.3 real, 842.6 MB
[runlim] sample:		599.4 time, 600.3 real, 845.2 MB
[runlim] sample:		609.4 time, 610.3 real, 923.5 MB
[runlim] sample:		619.4 time, 620.3 real, 804.6 MB
[runlim] sample:		629.4 time, 630.3 real, 844.9 MB
[runlim] sample:		639.3 time, 640.3 real, 844.9 MB
[runlim] sample:		649.3 time, 650.3 real, 844.9 MB
[runlim] sample:		659.3 time, 660.3 real, 844.9 MB
[runlim] sample:		669.3 time, 670.3 real, 847.2 MB
c [lgl113]  126.369  89% simplifying
c [lgl113]   12.825   9% search
c [lgl113] ==================================
c [lgl113]  141.498 100% all
c [lgl113] 
c [lgl113]          2878 conflicts,          20.3 confs/sec
c [lgl113]           212 ternaries,          13.6 confs/ternary
c [lgl113]           109 binaries,           26.4 confs/binary
c [lgl113]           162 iterations,         17.8 confs/iteration
c [lgl113] 
c [lgl113]             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c [lgl113]           106 restarts,            0.7 rests/sec,     27.2 confs/restart
c [lgl113]        270475 decisions,        1911.5 decis/sec,     94.0 decis/conflict
c [lgl113]      41005067 propagations,   289792.6 props/sec,    151.6 props/decision
c [lgl113] 
c [lgl113] 141.5 seconds, 960.8 MB
c [blimc] 672.53 reached k = 113
c [blimc] 672.53 cloned 2 solvers
c [blimc] 672.53 max 1238.9 MB
c [blimc] 672.54 exit 10
[runlim] end:			Sun Sep 20 21:37:31 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			673.75 seconds
[runlim] time:			672.52 seconds
[runlim] space:			1331.5 MB
[runlim] samples:		6734
