[runlim] version:		1.9
[runlim] time limit:		311040000 seconds
[runlim] real time limit:	3600 seconds
[runlim] space limit:		7000 MB
[runlim] argv[0]:		/home/biere/hwmcc15/solvers/blimc/single.blimc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a08b14s.aig
[runlim] start:			Fri Sep 18 12:38:50 2015
[runlim] main pid:		2224
c [blimc] BLIMC Bounded Lingeling Model Checker
c [blimc] 
c [blimc] Version bas 67f8c2b0db74be9343c0b7d4c974e5121193fe90
c [blimc] 
c [blimc] Copyright (C) 2010-2014 Armin Biere JKU Linz Austria.
c [blimc] All rights reserved.
c [blimc] 
c [blimc] released Tue Sep  8 16:12:24 CEST 2015
c [blimc] compiled Tue Sep  8 16:12:24 CEST 2015
c [blimc] 
c [blimc] gcc (Ubuntu 4.9.2-0ubuntu1~14.04) 4.9.2
c [blimc] -Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT
c [blimc] -DNLGLFILES -DNLGLDEMA
c [blimc] Linux sili7 3.13.0-63-generic x86_64
c [blimc] 
c [blimc] 0.00 reading /home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a08b14s.aig
c [blimc] 0.10 MILOA 842642 15696 16357 1 810589
c [blimc] 0.10 BCJK 0 0 0 0 810589
c [blimc] 0.10 16357 latches initialized to 0
c [blimc] 0.10 0 latches initialized to 1
c [blimc] 0.10 0 latches uninitialized
c [blimc] 0.13 literals  in COI:     842079 = 100% out of 842642
c [blimc] 0.13 inputs    in COI:      15696 = 100% out of 15696
c [blimc] 0.13 latches   in COI:      16149 =  99% out of 16357
c [blimc] 0.13 constants in COI:          1 = 100% out of 1
c [blimc] 0.13 ands      in COI:     810233 = 100% out of 810589
c [blimc] 0.89 encoded
[runlim] sample:		9.8 time, 10.2 real, 260.0 MB
[runlim] sample:		19.8 time, 20.2 real, 203.6 MB
[runlim] sample:		29.8 time, 30.2 real, 245.7 MB
[runlim] sample:		39.7 time, 40.2 real, 275.7 MB
c [blimc] 46.17 simplified
c [blimc] 46.33 extracted
c [lglopt]   45.260 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]   45.277 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]       1387584 propagations,    30646.4 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 45.3 seconds, 304.1 MB
c [blimc] 46.36 mapped 271797 variables
c [blimc] 46.37 maxk 1000
c [blimc] 46.37 bound 0
c [blimc] 47.03 bound 1
[runlim] sample:		49.7 time, 50.2 real, 200.8 MB
[runlim] sample:		59.7 time, 60.2 real, 218.0 MB
c [blimc] 62.06 bound 2
c [blimc] 62.70 bound 3
[runlim] sample:		69.7 time, 70.2 real, 366.3 MB
c [blimc] 76.20 bound 4
c [blimc] 76.88 bound 5
c [blimc] 77.78 bound 6
[runlim] sample:		79.7 time, 80.2 real, 574.8 MB
[runlim] sample:		89.7 time, 90.2 real, 547.4 MB
c [blimc] 96.35 bound 7
c [blimc] 97.40 bound 8
c [blimc] 98.55 bound 9
[runlim] sample:		99.7 time, 100.2 real, 766.9 MB
c [blimc] 99.70 bound 10
[runlim] sample:		109.7 time, 110.2 real, 979.0 MB
[runlim] sample:		119.7 time, 120.2 real, 1110.0 MB
[runlim] sample:		129.6 time, 130.2 real, 1006.2 MB
[runlim] sample:		139.6 time, 140.2 real, 882.5 MB
c [blimc] 140.62 bound 11
[runlim] sample:		149.6 time, 150.2 real, 870.6 MB
[runlim] sample:		159.6 time, 160.2 real, 806.1 MB
[runlim] sample:		169.6 time, 170.2 real, 1148.8 MB
[runlim] sample:		179.6 time, 180.2 real, 1177.1 MB
[runlim] sample:		189.6 time, 190.2 real, 1081.9 MB
[runlim] sample:		199.6 time, 200.2 real, 1922.6 MB
[runlim] sample:		209.5 time, 210.2 real, 1660.5 MB
[runlim] sample:		219.5 time, 220.2 real, 1670.9 MB
[runlim] sample:		229.5 time, 230.2 real, 1590.6 MB
[runlim] sample:		239.5 time, 240.2 real, 1590.6 MB
[runlim] sample:		249.5 time, 250.2 real, 1896.1 MB
[runlim] sample:		259.5 time, 260.2 real, 1358.5 MB
[runlim] sample:		269.5 time, 270.2 real, 1569.4 MB
[runlim] sample:		279.4 time, 280.2 real, 1340.0 MB
[runlim] sample:		289.4 time, 290.2 real, 1588.6 MB
[runlim] sample:		299.4 time, 300.2 real, 1588.6 MB
[runlim] sample:		309.4 time, 310.2 real, 1588.6 MB
[runlim] sample:		319.4 time, 320.2 real, 1588.6 MB
[runlim] sample:		329.4 time, 330.2 real, 1588.6 MB
[runlim] sample:		339.4 time, 340.2 real, 1588.6 MB
[runlim] sample:		349.4 time, 350.2 real, 1588.6 MB
[runlim] sample:		359.4 time, 360.2 real, 1588.6 MB
[runlim] sample:		369.3 time, 370.2 real, 1588.6 MB
[runlim] sample:		379.3 time, 380.2 real, 1588.6 MB
[runlim] sample:		389.3 time, 390.2 real, 1588.6 MB
[runlim] sample:		399.3 time, 400.2 real, 1588.6 MB
[runlim] sample:		409.3 time, 410.2 real, 1588.6 MB
[runlim] sample:		419.3 time, 420.2 real, 1588.6 MB
[runlim] sample:		429.2 time, 430.2 real, 1588.6 MB
[runlim] sample:		439.2 time, 440.2 real, 1588.6 MB
[runlim] sample:		449.2 time, 450.2 real, 1339.5 MB
[runlim] sample:		459.2 time, 460.2 real, 1686.1 MB
[runlim] sample:		469.2 time, 470.2 real, 1605.7 MB
[runlim] sample:		479.2 time, 480.2 real, 1565.4 MB
[runlim] sample:		489.2 time, 490.2 real, 1588.4 MB
[runlim] sample:		499.1 time, 500.2 real, 1588.4 MB
[runlim] sample:		509.1 time, 510.2 real, 1588.4 MB
[runlim] sample:		519.1 time, 520.2 real, 1588.4 MB
[runlim] sample:		529.1 time, 530.2 real, 1588.4 MB
[runlim] sample:		539.1 time, 540.2 real, 1588.4 MB
[runlim] sample:		549.1 time, 550.2 real, 1588.4 MB
[runlim] sample:		559.1 time, 560.2 real, 1588.4 MB
[runlim] sample:		569.1 time, 570.2 real, 1588.4 MB
[runlim] sample:		579.0 time, 580.2 real, 1588.4 MB
[runlim] sample:		589.0 time, 590.2 real, 1588.4 MB
[runlim] sample:		599.0 time, 600.2 real, 1588.4 MB
[runlim] sample:		609.0 time, 610.2 real, 1588.4 MB
[runlim] sample:		619.0 time, 620.2 real, 1588.4 MB
[runlim] sample:		629.0 time, 630.2 real, 1586.5 MB
[runlim] sample:		639.0 time, 640.2 real, 1584.5 MB
[runlim] sample:		649.0 time, 650.2 real, 1679.9 MB
[runlim] sample:		659.0 time, 660.2 real, 1679.9 MB
[runlim] sample:		669.0 time, 670.2 real, 1344.8 MB
[runlim] sample:		678.9 time, 680.2 real, 1574.2 MB
[runlim] sample:		688.9 time, 690.2 real, 1574.2 MB
[runlim] sample:		698.9 time, 700.2 real, 1574.2 MB
[runlim] sample:		708.9 time, 710.2 real, 1574.3 MB
[runlim] sample:		718.9 time, 720.2 real, 1433.8 MB
[runlim] sample:		728.9 time, 730.2 real, 1574.8 MB
[runlim] sample:		738.9 time, 740.2 real, 1559.4 MB
[runlim] sample:		748.9 time, 750.2 real, 1660.5 MB
[runlim] sample:		758.9 time, 760.2 real, 1660.5 MB
[runlim] sample:		768.9 time, 770.2 real, 1660.5 MB
[runlim] sample:		778.8 time, 780.2 real, 1556.4 MB
c [lgl11]  126.950  93% simplifying
c [lgl11]    9.676   7% search
c [lgl11] ==================================
c [lgl11]  136.956 100% all
c [lgl11] 
c [lgl11]          1527 conflicts,          11.1 confs/sec
c [lgl11]           217 ternaries,           7.0 confs/ternary
c [lgl11]            44 binaries,           34.7 confs/binary
c [lgl11]            13 iterations,        117.5 confs/iteration
c [lgl11] 
c [lgl11]             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c [lgl11]            28 restarts,            0.2 rests/sec,     54.5 confs/restart
c [lgl11]        145567 decisions,        1062.9 decis/sec,     95.3 decis/conflict
c [lgl11]      24493324 propagations,   178840.4 props/sec,    168.3 props/decision
c [lgl11] 
c [lgl11] 137.0 seconds, 1378.2 MB
c [blimc] 788.76 reached k = 11
c [blimc] 788.76 cloned 1 solvers
c [blimc] 788.76 max 1884.8 MB
c [blimc] 788.77 exit 10
[runlim] sample:		788.8 time, 790.2 real, 0.0 MB
[runlim] end:			Fri Sep 18 12:52:00 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			790.30 seconds
[runlim] time:			788.76 seconds
[runlim] space:			2032.7 MB
[runlim] samples:		7900
