[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/hwmcc14/single/6s13.aig
[runlim] start:			Tue Sep 15 17:00:14 2015
[runlim] main pid:		27053
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/hwmcc14/single/6s13.aig
c [blimc] 0.01 MILOA 27234 439 811 1 25984
c [blimc] 0.01 BCJK 0 0 0 0 25984
c [blimc] 0.01 811 latches initialized to 0
c [blimc] 0.01 0 latches initialized to 1
c [blimc] 0.01 0 latches uninitialized
c [blimc] 0.01 literals  in COI:      19220 =  71% out of 27234
c [blimc] 0.01 inputs    in COI:        275 =  63% out of 439
c [blimc] 0.01 latches   in COI:        603 =  74% out of 811
c [blimc] 0.01 constants in COI:          1 = 100% out of 1
c [blimc] 0.01 ands      in COI:      18341 =  71% out of 25984
c [blimc] 0.02 encoded
c [blimc] 3.88 simplified
c [blimc] 3.88 extracted
c [lglopt]    3.851 100% simplifying
c [lglopt]    0.000   0% search
c [lglopt] ==================================
c [lglopt]    3.852 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]        202597 propagations,    52600.5 props/sec,      0.0 props/decision
c [lglopt] 
c [lglopt] 3.9 seconds, 7.8 MB
c [blimc] 3.88 mapped 5804 variables
c [blimc] 3.88 maxk 1000
c [blimc] 3.88 bound 0
c [blimc] 4.15 bound 1
c [blimc] 4.72 bound 2
c [blimc] 7.31 bound 3
[runlim] sample:		9.8 time, 10.6 real, 13.8 MB
c [blimc] 15.48 bound 4
[runlim] sample:		19.8 time, 20.6 real, 16.7 MB
c [blimc] 28.05 bound 5
[runlim] sample:		29.8 time, 30.6 real, 22.2 MB
[runlim] sample:		39.8 time, 40.6 real, 26.3 MB
[runlim] sample:		49.8 time, 50.6 real, 32.2 MB
c [blimc] 54.98 bound 6
[runlim] sample:		59.8 time, 60.6 real, 25.6 MB
[runlim] sample:		69.7 time, 70.6 real, 25.0 MB
[runlim] sample:		79.7 time, 80.6 real, 32.4 MB
[runlim] sample:		89.7 time, 90.6 real, 38.9 MB
[runlim] sample:		99.7 time, 100.6 real, 40.8 MB
[runlim] sample:		109.7 time, 110.6 real, 46.4 MB
[runlim] sample:		119.7 time, 120.6 real, 41.3 MB
c [blimc] 127.37 bound 7
[runlim] sample:		129.7 time, 130.6 real, 36.1 MB
[runlim] sample:		139.7 time, 140.6 real, 36.1 MB
[runlim] sample:		149.7 time, 150.6 real, 36.1 MB
[runlim] sample:		159.7 time, 160.6 real, 43.4 MB
[runlim] sample:		169.6 time, 170.6 real, 44.5 MB
[runlim] sample:		179.6 time, 180.6 real, 52.3 MB
[runlim] sample:		189.6 time, 190.6 real, 52.3 MB
[runlim] sample:		199.6 time, 200.6 real, 57.3 MB
[runlim] sample:		209.6 time, 210.6 real, 57.3 MB
[runlim] sample:		219.6 time, 220.6 real, 60.6 MB
[runlim] sample:		229.6 time, 230.6 real, 76.1 MB
[runlim] sample:		239.6 time, 240.6 real, 68.0 MB
[runlim] sample:		249.5 time, 250.6 real, 75.5 MB
[runlim] sample:		259.5 time, 260.6 real, 75.5 MB
[runlim] sample:		269.5 time, 270.6 real, 75.5 MB
c [blimc] 275.45 bound 8
[runlim] sample:		279.5 time, 280.6 real, 37.1 MB
[runlim] sample:		289.5 time, 290.6 real, 37.1 MB
[runlim] sample:		299.5 time, 300.6 real, 37.1 MB
[runlim] sample:		309.5 time, 310.6 real, 43.6 MB
[runlim] sample:		319.5 time, 320.6 real, 44.9 MB
[runlim] sample:		329.5 time, 330.6 real, 46.9 MB
[runlim] sample:		339.4 time, 340.6 real, 63.2 MB
[runlim] sample:		349.4 time, 350.6 real, 55.5 MB
[runlim] sample:		359.4 time, 360.6 real, 55.3 MB
[runlim] sample:		369.4 time, 370.6 real, 63.6 MB
[runlim] sample:		379.4 time, 380.6 real, 57.3 MB
[runlim] sample:		389.4 time, 390.6 real, 59.7 MB
[runlim] sample:		399.4 time, 400.6 real, 59.7 MB
[runlim] sample:		409.4 time, 410.6 real, 66.1 MB
[runlim] sample:		419.3 time, 420.6 real, 66.1 MB
[runlim] sample:		429.3 time, 430.6 real, 76.4 MB
[runlim] sample:		439.3 time, 440.6 real, 76.4 MB
[runlim] sample:		449.3 time, 450.6 real, 68.0 MB
[runlim] sample:		459.3 time, 460.6 real, 68.0 MB
[runlim] sample:		469.3 time, 470.6 real, 68.0 MB
[runlim] sample:		479.2 time, 480.6 real, 79.1 MB
[runlim] sample:		489.2 time, 490.6 real, 79.1 MB
[runlim] sample:		499.2 time, 500.6 real, 79.1 MB
[runlim] sample:		509.2 time, 510.6 real, 79.1 MB
[runlim] sample:		519.2 time, 520.6 real, 71.3 MB
[runlim] sample:		529.2 time, 530.6 real, 71.3 MB
[runlim] sample:		539.2 time, 540.6 real, 71.3 MB
[runlim] sample:		549.2 time, 550.6 real, 83.1 MB
[runlim] sample:		559.1 time, 560.6 real, 83.1 MB
[runlim] sample:		569.1 time, 570.6 real, 83.1 MB
[runlim] sample:		579.1 time, 580.6 real, 83.1 MB
[runlim] sample:		589.1 time, 590.6 real, 83.1 MB
[runlim] sample:		599.1 time, 600.6 real, 83.1 MB
[runlim] sample:		609.1 time, 610.6 real, 83.1 MB
[runlim] sample:		619.1 time, 620.6 real, 83.1 MB
[runlim] sample:		629.0 time, 630.6 real, 83.1 MB
[runlim] sample:		639.0 time, 640.6 real, 83.1 MB
[runlim] sample:		649.0 time, 650.6 real, 83.1 MB
[runlim] sample:		659.0 time, 660.6 real, 83.1 MB
[runlim] sample:		669.0 time, 670.6 real, 83.4 MB
[runlim] sample:		679.0 time, 680.6 real, 83.4 MB
c [blimc] 680.34 bound 9
[runlim] sample:		689.0 time, 690.6 real, 38.7 MB
[runlim] sample:		699.0 time, 700.6 real, 44.7 MB
[runlim] sample:		709.0 time, 710.6 real, 45.8 MB
[runlim] sample:		719.0 time, 720.6 real, 47.0 MB
[runlim] sample:		728.9 time, 730.6 real, 54.1 MB
[runlim] sample:		738.9 time, 740.6 real, 55.6 MB
[runlim] sample:		748.9 time, 750.6 real, 55.6 MB
[runlim] sample:		758.9 time, 760.6 real, 61.0 MB
[runlim] sample:		768.9 time, 770.6 real, 63.0 MB
[runlim] sample:		778.9 time, 780.6 real, 63.0 MB
[runlim] sample:		788.9 time, 790.6 real, 63.0 MB
[runlim] sample:		798.9 time, 800.6 real, 65.3 MB
[runlim] sample:		808.8 time, 810.6 real, 65.3 MB
[runlim] sample:		818.8 time, 820.6 real, 65.3 MB
[runlim] sample:		828.8 time, 830.6 real, 67.1 MB
[runlim] sample:		838.8 time, 840.6 real, 67.1 MB
[runlim] sample:		848.8 time, 850.6 real, 67.1 MB
[runlim] sample:		858.8 time, 860.6 real, 89.9 MB
[runlim] sample:		868.8 time, 870.6 real, 89.9 MB
[runlim] sample:		878.7 time, 880.6 real, 78.9 MB
[runlim] sample:		888.7 time, 890.6 real, 78.9 MB
[runlim] sample:		898.7 time, 900.6 real, 78.9 MB
[runlim] sample:		908.7 time, 910.6 real, 90.4 MB
[runlim] sample:		918.7 time, 920.6 real, 90.4 MB
[runlim] sample:		928.7 time, 930.6 real, 90.4 MB
[runlim] sample:		938.6 time, 940.6 real, 89.6 MB
[runlim] sample:		948.6 time, 950.6 real, 89.6 MB
[runlim] sample:		958.6 time, 960.6 real, 89.6 MB
[runlim] sample:		968.6 time, 970.6 real, 102.1 MB
[runlim] sample:		978.6 time, 980.6 real, 102.1 MB
[runlim] sample:		988.6 time, 990.6 real, 102.1 MB
[runlim] sample:		998.6 time, 1000.6 real, 102.1 MB
[runlim] sample:		1008.6 time, 1010.6 real, 102.1 MB
[runlim] sample:		1018.5 time, 1020.6 real, 102.1 MB
[runlim] sample:		1028.5 time, 1030.6 real, 86.4 MB
[runlim] sample:		1038.5 time, 1040.6 real, 92.9 MB
[runlim] sample:		1048.5 time, 1050.6 real, 92.9 MB
[runlim] sample:		1058.5 time, 1060.6 real, 92.9 MB
[runlim] sample:		1068.5 time, 1070.6 real, 106.2 MB
[runlim] sample:		1078.5 time, 1080.6 real, 106.2 MB
[runlim] sample:		1088.4 time, 1090.6 real, 106.2 MB
[runlim] sample:		1098.4 time, 1100.6 real, 106.2 MB
[runlim] sample:		1108.4 time, 1110.6 real, 106.2 MB
[runlim] sample:		1118.4 time, 1120.6 real, 106.2 MB
[runlim] sample:		1128.4 time, 1130.6 real, 106.2 MB
[runlim] sample:		1138.4 time, 1140.6 real, 106.2 MB
[runlim] sample:		1148.3 time, 1150.6 real, 106.2 MB
[runlim] sample:		1158.3 time, 1160.6 real, 106.2 MB
[runlim] sample:		1168.3 time, 1170.6 real, 106.2 MB
[runlim] sample:		1178.3 time, 1180.6 real, 94.3 MB
[runlim] sample:		1188.3 time, 1190.6 real, 94.3 MB
[runlim] sample:		1198.3 time, 1200.6 real, 94.3 MB
[runlim] sample:		1208.3 time, 1210.6 real, 94.3 MB
[runlim] sample:		1218.3 time, 1220.6 real, 108.8 MB
[runlim] sample:		1228.2 time, 1230.6 real, 108.8 MB
[runlim] sample:		1238.2 time, 1240.6 real, 108.8 MB
[runlim] sample:		1248.2 time, 1250.6 real, 108.8 MB
[runlim] sample:		1258.2 time, 1260.6 real, 108.8 MB
[runlim] sample:		1268.2 time, 1270.6 real, 108.8 MB
[runlim] sample:		1278.2 time, 1280.6 real, 96.0 MB
[runlim] sample:		1288.2 time, 1290.6 real, 97.4 MB
[runlim] sample:		1298.2 time, 1300.6 real, 97.4 MB
[runlim] sample:		1308.1 time, 1310.6 real, 97.4 MB
[runlim] sample:		1318.1 time, 1320.6 real, 97.4 MB
[runlim] sample:		1328.1 time, 1330.6 real, 112.2 MB
[runlim] sample:		1338.1 time, 1340.6 real, 112.2 MB
[runlim] sample:		1348.1 time, 1350.6 real, 112.2 MB
[runlim] sample:		1358.1 time, 1360.6 real, 112.2 MB
[runlim] sample:		1368.0 time, 1370.6 real, 112.2 MB
[runlim] sample:		1378.0 time, 1380.6 real, 112.2 MB
[runlim] sample:		1388.0 time, 1390.6 real, 112.2 MB
[runlim] sample:		1398.0 time, 1400.6 real, 112.2 MB
[runlim] sample:		1408.0 time, 1410.6 real, 112.2 MB
[runlim] sample:		1418.0 time, 1420.6 real, 112.2 MB
[runlim] sample:		1428.0 time, 1430.6 real, 112.2 MB
[runlim] sample:		1438.0 time, 1440.6 real, 112.2 MB
[runlim] sample:		1447.9 time, 1450.6 real, 112.2 MB
[runlim] sample:		1457.9 time, 1460.6 real, 112.2 MB
[runlim] sample:		1467.9 time, 1470.6 real, 112.2 MB
[runlim] sample:		1477.9 time, 1480.6 real, 112.2 MB
[runlim] sample:		1487.9 time, 1490.6 real, 112.2 MB
[runlim] sample:		1497.9 time, 1500.6 real, 112.2 MB
[runlim] sample:		1507.8 time, 1510.6 real, 112.2 MB
[runlim] sample:		1517.8 time, 1520.6 real, 98.9 MB
[runlim] sample:		1527.8 time, 1530.6 real, 98.9 MB
[runlim] sample:		1537.8 time, 1540.6 real, 98.9 MB
[runlim] sample:		1547.8 time, 1550.6 real, 98.9 MB
[runlim] sample:		1557.8 time, 1560.6 real, 98.9 MB
[runlim] sample:		1567.8 time, 1570.6 real, 98.9 MB
[runlim] sample:		1577.8 time, 1580.6 real, 98.9 MB
[runlim] sample:		1587.7 time, 1590.6 real, 114.9 MB
[runlim] sample:		1597.7 time, 1600.6 real, 114.9 MB
[runlim] sample:		1607.7 time, 1610.6 real, 114.9 MB
[runlim] sample:		1617.7 time, 1620.6 real, 114.9 MB
[runlim] sample:		1627.7 time, 1630.6 real, 114.9 MB
[runlim] sample:		1637.7 time, 1640.6 real, 109.7 MB
[runlim] sample:		1647.7 time, 1650.6 real, 109.7 MB
[runlim] sample:		1657.6 time, 1660.6 real, 119.9 MB
[runlim] sample:		1667.6 time, 1670.6 real, 119.9 MB
[runlim] sample:		1677.6 time, 1680.6 real, 119.9 MB
[runlim] sample:		1687.6 time, 1690.6 real, 119.9 MB
[runlim] sample:		1697.6 time, 1700.6 real, 136.5 MB
[runlim] sample:		1707.6 time, 1710.6 real, 136.5 MB
[runlim] sample:		1717.5 time, 1720.6 real, 136.5 MB
[runlim] sample:		1727.5 time, 1730.6 real, 136.5 MB
[runlim] sample:		1737.5 time, 1740.6 real, 136.5 MB
[runlim] sample:		1747.5 time, 1750.6 real, 136.5 MB
[runlim] sample:		1757.5 time, 1760.6 real, 136.5 MB
[runlim] sample:		1767.5 time, 1770.6 real, 136.5 MB
[runlim] sample:		1777.5 time, 1780.6 real, 136.5 MB
[runlim] sample:		1787.4 time, 1790.6 real, 136.5 MB
[runlim] sample:		1797.4 time, 1800.6 real, 136.5 MB
[runlim] sample:		1807.4 time, 1810.6 real, 136.5 MB
[runlim] sample:		1817.4 time, 1820.6 real, 136.5 MB
[runlim] sample:		1827.4 time, 1830.6 real, 136.5 MB
[runlim] sample:		1837.4 time, 1840.6 real, 136.5 MB
[runlim] sample:		1847.4 time, 1850.6 real, 136.5 MB
[runlim] sample:		1857.3 time, 1860.6 real, 136.5 MB
[runlim] sample:		1867.3 time, 1870.6 real, 136.5 MB
[runlim] sample:		1877.3 time, 1880.6 real, 136.5 MB
[runlim] sample:		1887.3 time, 1890.6 real, 136.5 MB
[runlim] sample:		1897.3 time, 1900.6 real, 136.5 MB
[runlim] sample:		1907.3 time, 1910.6 real, 136.5 MB
[runlim] sample:		1917.3 time, 1920.6 real, 136.5 MB
[runlim] sample:		1927.2 time, 1930.6 real, 136.5 MB
[runlim] sample:		1937.2 time, 1940.6 real, 136.5 MB
[runlim] sample:		1947.2 time, 1950.6 real, 136.5 MB
[runlim] sample:		1957.2 time, 1960.6 real, 136.5 MB
[runlim] sample:		1967.2 time, 1970.6 real, 136.5 MB
[runlim] sample:		1977.2 time, 1980.6 real, 136.5 MB
[runlim] sample:		1987.2 time, 1990.6 real, 136.5 MB
[runlim] sample:		1997.1 time, 2000.6 real, 136.5 MB
[runlim] sample:		2007.1 time, 2010.6 real, 136.5 MB
[runlim] sample:		2017.1 time, 2020.6 real, 136.5 MB
[runlim] sample:		2027.1 time, 2030.6 real, 136.5 MB
[runlim] sample:		2037.1 time, 2040.6 real, 120.7 MB
[runlim] sample:		2047.1 time, 2050.6 real, 120.7 MB
[runlim] sample:		2057.1 time, 2060.6 real, 120.7 MB
[runlim] sample:		2067.1 time, 2070.6 real, 120.7 MB
[runlim] sample:		2077.0 time, 2080.6 real, 120.7 MB
[runlim] sample:		2087.0 time, 2090.6 real, 120.7 MB
[runlim] sample:		2097.0 time, 2100.6 real, 120.7 MB
[runlim] sample:		2107.0 time, 2110.6 real, 120.7 MB
[runlim] sample:		2117.0 time, 2120.6 real, 120.7 MB
[runlim] sample:		2127.0 time, 2130.6 real, 138.2 MB
c [blimc] 2131.00 bound 10
[runlim] sample:		2136.9 time, 2140.6 real, 51.9 MB
[runlim] sample:		2146.9 time, 2150.6 real, 51.9 MB
[runlim] sample:		2156.9 time, 2160.6 real, 51.9 MB
[runlim] sample:		2166.9 time, 2170.6 real, 54.4 MB
[runlim] sample:		2176.9 time, 2180.6 real, 55.6 MB
[runlim] sample:		2186.9 time, 2190.6 real, 57.2 MB
[runlim] sample:		2196.9 time, 2200.6 real, 57.2 MB
[runlim] sample:		2206.9 time, 2210.6 real, 66.2 MB
[runlim] sample:		2216.9 time, 2220.6 real, 66.2 MB
[runlim] sample:		2226.9 time, 2230.6 real, 66.2 MB
[runlim] sample:		2236.8 time, 2240.6 real, 66.2 MB
[runlim] sample:		2246.8 time, 2250.6 real, 78.0 MB
[runlim] sample:		2256.8 time, 2260.6 real, 78.0 MB
[runlim] sample:		2266.8 time, 2270.6 real, 78.0 MB
[runlim] sample:		2276.8 time, 2280.6 real, 90.1 MB
[runlim] sample:		2286.8 time, 2290.6 real, 78.9 MB
[runlim] sample:		2296.8 time, 2300.6 real, 78.9 MB
[runlim] sample:		2306.7 time, 2310.6 real, 78.9 MB
[runlim] sample:		2316.7 time, 2320.6 real, 78.9 MB
[runlim] sample:		2326.7 time, 2330.6 real, 91.5 MB
[runlim] sample:		2336.7 time, 2340.6 real, 91.5 MB
[runlim] sample:		2346.7 time, 2350.6 real, 91.5 MB
[runlim] sample:		2356.7 time, 2360.6 real, 91.5 MB
[runlim] sample:		2366.7 time, 2370.6 real, 91.5 MB
[runlim] sample:		2376.6 time, 2380.6 real, 83.4 MB
c [lgl10]    8.967  93% simplifying
c [lgl10]    0.704   7% search
c [lgl10] ==================================
c [lgl10]    9.676 100% all
c [lgl10] 
c [lgl10]          9143 conflicts,         944.9 confs/sec
c [lgl10]           598 ternaries,          15.3 confs/ternary
c [lgl10]           164 binaries,           55.8 confs/binary
c [lgl10]            10 iterations,        914.3 confs/iteration
c [lgl10] 
c [lgl10]             0 reductions,          0.0 redus/sec,      0.0 confs/reduction
c [lgl10]           125 restarts,           12.9 rests/sec,     73.1 confs/restart
c [lgl10]         71288 decisions,        7367.8 decis/sec,      7.8 decis/conflict
c [lgl10]       3160191 propagations,   326612.1 props/sec,     44.3 props/decision
c [lgl10] 
c [lgl10] 9.7 seconds, 22.0 MB
c [blimc] 2384.49 reached k = 10
c [blimc] 2384.49 cloned 9 solvers
c [blimc] 2384.49 max 101.3 MB
c [blimc] 2384.49 exit 10
[runlim] end:			Tue Sep 15 17:40:02 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			2388.57 seconds
[runlim] time:			2384.48 seconds
[runlim] space:			138.2 MB
[runlim] samples:		23879
