[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/6s184.aig
[runlim] start:			Sun Sep 20 09:18:22 2015
[runlim] main pid:		4347
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/6s184.aig
c [blimc] 0.00 MILOA 15940 256 607 1 15077
c [blimc] 0.00 BCJK 0 0 0 0 15077
c [blimc] 0.00 607 latches initialized to 0
c [blimc] 0.00 0 latches initialized to 1
c [blimc] 0.00 0 latches uninitialized
c [blimc] 0.01 literals  in COI:      15941 = 100% out of 15940
c [blimc] 0.01 inputs    in COI:        256 = 100% out of 256
c [blimc] 0.01 latches   in COI:        607 = 100% out of 607
c [blimc] 0.01 constants in COI:          1 = 100% out of 1
c [blimc] 0.01 ands      in COI:      15077 = 100% out of 15077
c [blimc] 0.03 encoded
c [blimc] 3.74 simplified
c [blimc] 3.74 extracted
c [lglopt]    3.710 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]    3.710 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]        182601 propagations,    49216.9 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 3.7 seconds, 6.2 MB
c [blimc] 3.74 mapped 4782 variables
c [blimc] 3.74 maxk 1000
c [blimc] 3.74 bound 0
c [blimc] 3.98 bound 1
c [blimc] 4.51 bound 2
c [blimc] 4.85 bound 3
c [blimc] 6.63 bound 4
c [blimc] 7.79 bound 5
[runlim] sample:		10.0 time, 10.3 real, 17.5 MB
c [blimc] 18.01 bound 6
[runlim] sample:		20.0 time, 20.3 real, 22.1 MB
[runlim] sample:		30.0 time, 30.3 real, 22.6 MB
[runlim] sample:		40.0 time, 40.3 real, 25.4 MB
c [blimc] 47.82 bound 7
[runlim] sample:		49.9 time, 50.3 real, 27.1 MB
[runlim] sample:		59.9 time, 60.3 real, 29.5 MB
[runlim] sample:		69.9 time, 70.3 real, 28.8 MB
[runlim] sample:		79.9 time, 80.3 real, 33.8 MB
[runlim] sample:		89.9 time, 90.3 real, 34.3 MB
[runlim] sample:		99.9 time, 100.3 real, 36.8 MB
c [blimc] 103.24 bound 8
[runlim] sample:		109.9 time, 110.3 real, 33.3 MB
[runlim] sample:		119.9 time, 120.3 real, 33.3 MB
[runlim] sample:		129.9 time, 130.3 real, 41.6 MB
[runlim] sample:		139.9 time, 140.3 real, 41.6 MB
[runlim] sample:		149.8 time, 150.3 real, 47.0 MB
[runlim] sample:		159.8 time, 160.3 real, 48.8 MB
[runlim] sample:		169.8 time, 170.3 real, 48.8 MB
[runlim] sample:		179.8 time, 180.3 real, 55.7 MB
[runlim] sample:		189.8 time, 190.3 real, 62.8 MB
[runlim] sample:		199.8 time, 200.3 real, 62.8 MB
[runlim] sample:		209.8 time, 210.3 real, 60.8 MB
c [blimc] 213.26 bound 9
[runlim] sample:		219.8 time, 220.3 real, 37.5 MB
[runlim] sample:		229.8 time, 230.3 real, 38.0 MB
[runlim] sample:		239.8 time, 240.3 real, 38.0 MB
[runlim] sample:		249.7 time, 250.3 real, 43.4 MB
[runlim] sample:		259.7 time, 260.3 real, 49.2 MB
[runlim] sample:		269.7 time, 270.3 real, 56.8 MB
[runlim] sample:		279.7 time, 280.3 real, 58.2 MB
[runlim] sample:		289.7 time, 290.3 real, 57.2 MB
[runlim] sample:		299.7 time, 300.3 real, 65.3 MB
[runlim] sample:		309.7 time, 310.3 real, 58.8 MB
[runlim] sample:		319.6 time, 320.3 real, 58.8 MB
[runlim] sample:		329.6 time, 330.3 real, 58.8 MB
[runlim] sample:		339.6 time, 340.3 real, 59.2 MB
[runlim] sample:		349.6 time, 350.3 real, 59.2 MB
[runlim] sample:		359.6 time, 360.3 real, 68.7 MB
[runlim] sample:		369.6 time, 370.3 real, 68.9 MB
[runlim] sample:		379.6 time, 380.3 real, 60.0 MB
[runlim] sample:		389.6 time, 390.3 real, 60.0 MB
[runlim] sample:		399.5 time, 400.3 real, 60.0 MB
[runlim] sample:		409.5 time, 410.3 real, 70.6 MB
[runlim] sample:		419.5 time, 420.3 real, 70.6 MB
[runlim] sample:		429.5 time, 430.3 real, 70.6 MB
[runlim] sample:		439.5 time, 440.3 real, 71.3 MB
[runlim] sample:		449.5 time, 450.3 real, 71.3 MB
[runlim] sample:		459.5 time, 460.3 real, 66.7 MB
[runlim] sample:		469.4 time, 470.3 real, 66.7 MB
[runlim] sample:		479.4 time, 480.3 real, 73.5 MB
[runlim] sample:		489.4 time, 490.3 real, 73.5 MB
c [blimc] 492.86 bound 10
[runlim] sample:		499.4 time, 500.3 real, 41.3 MB
[runlim] sample:		509.4 time, 510.3 real, 45.7 MB
[runlim] sample:		519.4 time, 520.3 real, 45.7 MB
[runlim] sample:		529.4 time, 530.3 real, 50.8 MB
[runlim] sample:		539.4 time, 540.3 real, 50.8 MB
[runlim] sample:		549.4 time, 550.3 real, 57.8 MB
[runlim] sample:		559.4 time, 560.3 real, 59.6 MB
[runlim] sample:		569.3 time, 570.3 real, 60.1 MB
[runlim] sample:		579.3 time, 580.3 real, 60.1 MB
[runlim] sample:		589.3 time, 590.3 real, 67.9 MB
[runlim] sample:		599.3 time, 600.3 real, 67.9 MB
[runlim] sample:		609.3 time, 610.3 real, 58.7 MB
[runlim] sample:		619.3 time, 620.3 real, 62.2 MB
[runlim] sample:		629.3 time, 630.3 real, 62.2 MB
[runlim] sample:		639.2 time, 640.3 real, 67.8 MB
[runlim] sample:		649.2 time, 650.3 real, 67.8 MB
[runlim] sample:		659.2 time, 660.3 real, 89.5 MB
c [lgl10]    5.253  85% simplifying
c [lgl10]    0.930  15% search
c [lgl10] ==================================
c [lgl10]    6.187 100% all
c [lgl10] 
c [lgl10]          8074 conflicts,        1304.9 confs/sec
c [lgl10]           573 ternaries,          14.1 confs/ternary
c [lgl10]           225 binaries,           35.9 confs/binary
c [lgl10]            35 iterations,        230.7 confs/iteration
c [lgl10] 
c [lgl10]             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c [lgl10]           362 restarts,           58.5 rests/sec,     22.3 confs/restart
c [lgl10]         90184 decisions,       14575.5 decis/sec,     11.2 decis/conflict
c [lgl10]       4483099 propagations,   724555.5 props/sec,     49.7 props/decision
c [lgl10] 
c [lgl10] 6.2 seconds, 18.4 MB
c [blimc] 664.25 reached k = 10
c [blimc] 664.25 cloned 8 solvers
c [blimc] 664.25 max 64.1 MB
c [blimc] 664.25 exit 10
[runlim] end:			Sun Sep 20 09:29:27 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			665.37 seconds
[runlim] time:			664.22 seconds
[runlim] space:			89.5 MB
[runlim] samples:		6650
