[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/avy/single.avy
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/hwmcc14/single/6s35.aig
[runlim] start:			Wed Sep 16 07:02:06 2015
[runlim] main pid:		32443
[runlim] sample:		32.4 time, 10.3 real, 410.7 MB
[runlim] sample:		71.9 time, 20.3 real, 568.6 MB
[runlim] sample:		111.4 time, 30.3 real, 554.7 MB
[runlim] sample:		151.0 time, 40.3 real, 725.6 MB
[runlim] sample:		190.5 time, 50.3 real, 800.8 MB
[runlim] sample:		230.0 time, 60.3 real, 855.8 MB
[runlim] sample:		269.6 time, 70.3 real, 895.0 MB
[runlim] sample:		309.1 time, 80.3 real, 940.1 MB
[runlim] sample:		348.7 time, 90.3 real, 965.0 MB
[runlim] sample:		388.2 time, 100.3 real, 1001.2 MB
[runlim] sample:		427.8 time, 110.3 real, 1014.2 MB
[runlim] sample:		467.3 time, 120.3 real, 1060.3 MB
[runlim] sample:		506.9 time, 130.3 real, 1010.1 MB
[runlim] sample:		546.4 time, 140.3 real, 1115.6 MB
[runlim] sample:		586.0 time, 150.3 real, 1125.8 MB
[runlim] sample:		625.4 time, 160.3 real, 1138.4 MB
[runlim] sample:		665.0 time, 170.3 real, 1195.8 MB
[runlim] sample:		704.5 time, 180.3 real, 1209.2 MB
[runlim] sample:		744.1 time, 190.3 real, 1178.7 MB
[runlim] sample:		783.6 time, 200.3 real, 1237.1 MB
[runlim] sample:		823.1 time, 210.3 real, 1206.9 MB
[runlim] sample:		862.6 time, 220.3 real, 1257.1 MB
[runlim] sample:		902.1 time, 230.3 real, 1283.6 MB
[runlim] sample:		941.6 time, 240.3 real, 1350.8 MB
[runlim] sample:		981.1 time, 250.3 real, 1417.8 MB
[runlim] sample:		1020.6 time, 260.3 real, 1431.7 MB
[runlim] sample:		1060.2 time, 270.3 real, 1489.0 MB
[runlim] sample:		1099.7 time, 280.3 real, 1534.8 MB
[runlim] sample:		1139.2 time, 290.3 real, 1434.1 MB
[runlim] sample:		1178.8 time, 300.3 real, 1582.5 MB
[runlim] sample:		1218.4 time, 310.3 real, 1614.2 MB
[runlim] sample:		1257.9 time, 320.3 real, 1722.7 MB
[runlim] sample:		1297.4 time, 330.3 real, 1726.2 MB
[runlim] sample:		1337.0 time, 340.3 real, 1603.7 MB
[runlim] sample:		1376.5 time, 350.3 real, 1732.2 MB
[runlim] sample:		1416.0 time, 360.3 real, 1739.2 MB
[runlim] sample:		1455.5 time, 370.3 real, 1791.6 MB
[runlim] sample:		1495.1 time, 380.3 real, 1865.2 MB
[runlim] sample:		1534.6 time, 390.3 real, 1867.5 MB
[runlim] sample:		1574.1 time, 400.3 real, 1870.5 MB
[runlim] sample:		1613.6 time, 410.3 real, 1863.3 MB
[runlim] sample:		1653.1 time, 420.3 real, 1924.0 MB
[runlim] sample:		1692.7 time, 430.3 real, 1927.0 MB
[runlim] sample:		1732.3 time, 440.3 real, 1930.8 MB
[runlim] sample:		1771.8 time, 450.3 real, 1826.6 MB
[runlim] sample:		1811.4 time, 460.3 real, 1964.8 MB
[runlim] sample:		1851.0 time, 470.3 real, 1970.5 MB
[runlim] sample:		1890.5 time, 480.3 real, 1938.5 MB
[runlim] sample:		1930.0 time, 490.3 real, 1940.7 MB
[runlim] sample:		1969.6 time, 500.3 real, 1948.4 MB
[runlim] sample:		2009.2 time, 510.3 real, 1847.4 MB
[runlim] sample:		2048.7 time, 520.3 real, 1981.3 MB
[runlim] sample:		2088.3 time, 530.3 real, 1941.3 MB
[runlim] sample:		2127.8 time, 540.3 real, 1976.7 MB
[runlim] sample:		2167.4 time, 550.3 real, 1982.7 MB
[runlim] sample:		2206.9 time, 560.3 real, 1987.1 MB
[runlim] sample:		2246.5 time, 570.3 real, 1990.7 MB
[runlim] sample:		2286.1 time, 580.3 real, 1994.5 MB
[runlim] sample:		2325.6 time, 590.3 real, 1895.3 MB
[runlim] sample:		2365.2 time, 600.3 real, 2039.5 MB
[runlim] sample:		2404.7 time, 610.3 real, 2045.0 MB
[runlim] sample:		2444.3 time, 620.3 real, 2048.6 MB
[runlim] sample:		2483.9 time, 630.3 real, 2051.9 MB
[runlim] sample:		2523.4 time, 640.3 real, 2054.6 MB
[runlim] sample:		2562.9 time, 650.3 real, 2057.4 MB
[runlim] sample:		2602.5 time, 660.3 real, 2062.4 MB
[runlim] sample:		2642.0 time, 670.3 real, 2065.2 MB
[runlim] sample:		2681.6 time, 680.3 real, 1968.0 MB
[runlim] sample:		2721.1 time, 690.3 real, 2097.9 MB
[runlim] sample:		2760.7 time, 700.3 real, 2103.2 MB
[runlim] sample:		2800.2 time, 710.3 real, 2106.5 MB
[runlim] sample:		2839.7 time, 720.3 real, 2111.8 MB
[runlim] sample:		2879.3 time, 730.3 real, 2114.8 MB
[runlim] sample:		2918.8 time, 740.3 real, 2115.6 MB
[runlim] sample:		2958.3 time, 750.3 real, 2120.8 MB
[runlim] sample:		2997.8 time, 760.3 real, 2123.1 MB
[runlim] sample:		3037.3 time, 770.3 real, 2000.8 MB
[runlim] sample:		3076.9 time, 780.3 real, 2198.5 MB
[runlim] sample:		3116.4 time, 790.3 real, 2152.9 MB
[runlim] sample:		3155.9 time, 800.3 real, 2160.7 MB
[runlim] sample:		3195.5 time, 810.3 real, 2166.0 MB
[runlim] sample:		3235.0 time, 820.3 real, 2202.3 MB
[runlim] sample:		3274.5 time, 830.3 real, 2207.1 MB
[runlim] sample:		3314.0 time, 840.3 real, 2214.4 MB
[runlim] sample:		3353.5 time, 850.3 real, 2181.6 MB
[runlim] sample:		3393.0 time, 860.3 real, 2174.0 MB
[runlim] sample:		3432.6 time, 870.3 real, 2242.5 MB
[runlim] sample:		3472.1 time, 880.3 real, 2247.6 MB
[runlim] sample:		3511.7 time, 890.3 real, 2257.8 MB
[runlim] sample:		3551.3 time, 900.3 real, 2264.3 MB
[runlim] sample:		3590.9 time, 910.3 real, 2270.8 MB
[runlim] sample:		3630.3 time, 920.3 real, 2265.2 MB
[runlim] sample:		3669.9 time, 930.3 real, 2269.6 MB
[runlim] sample:		3709.4 time, 940.3 real, 2275.9 MB
[runlim] sample:		3749.0 time, 950.3 real, 2282.3 MB
[runlim] sample:		3788.5 time, 960.3 real, 2288.6 MB
[runlim] sample:		3828.1 time, 970.3 real, 2293.5 MB
[runlim] sample:		3867.6 time, 980.3 real, 2300.5 MB
[runlim] sample:		3907.1 time, 990.3 real, 2097.8 MB
[runlim] sample:		3946.7 time, 1000.3 real, 2711.9 MB
[runlim] sample:		3986.3 time, 1010.3 real, 4988.3 MB
[runlim] end:			Wed Sep 16 07:19:04 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		40660
[runlim] real:			1018.17 seconds
[runlim] time:			4017.09 seconds
[runlim] space:			7006.9 MB
[runlim] samples:		10178
