[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/oski15/submission/single/oski15a08b12s.aig
[runlim] start:			Fri Sep 18 11:47:30 2015
[runlim] main pid:		3239
[runlim] sample:		9.0 time, 10.2 real, 200.1 MB
[runlim] sample:		19.0 time, 20.2 real, 219.5 MB
[runlim] sample:		28.9 time, 30.3 real, 302.3 MB
[runlim] sample:		39.0 time, 40.2 real, 224.7 MB
[runlim] sample:		48.9 time, 50.2 real, 207.7 MB
[runlim] sample:		58.9 time, 60.2 real, 233.4 MB
[runlim] sample:		68.9 time, 70.2 real, 353.4 MB
[runlim] sample:		78.9 time, 80.2 real, 244.1 MB
[runlim] sample:		88.9 time, 90.2 real, 253.7 MB
[runlim] sample:		98.9 time, 100.2 real, 301.6 MB
[runlim] sample:		108.9 time, 110.2 real, 381.0 MB
[runlim] sample:		118.9 time, 120.2 real, 98.9 MB
[runlim] sample:		128.9 time, 130.2 real, 98.9 MB
[runlim] sample:		138.9 time, 140.3 real, 99.2 MB
[runlim] sample:		148.8 time, 150.2 real, 99.2 MB
[runlim] sample:		158.8 time, 160.2 real, 99.2 MB
[runlim] sample:		168.8 time, 170.2 real, 101.8 MB
[runlim] sample:		178.8 time, 180.2 real, 101.8 MB
[runlim] sample:		188.8 time, 190.2 real, 101.8 MB
[runlim] sample:		198.8 time, 200.2 real, 263.7 MB
[runlim] sample:		208.8 time, 210.2 real, 211.0 MB
[runlim] sample:		218.8 time, 220.2 real, 263.1 MB
[runlim] sample:		228.8 time, 230.2 real, 241.3 MB
[runlim] sample:		238.7 time, 240.2 real, 355.3 MB
[runlim] sample:		248.7 time, 250.2 real, 384.6 MB
[runlim] sample:		258.7 time, 260.2 real, 384.6 MB
[runlim] sample:		268.7 time, 270.2 real, 329.1 MB
[runlim] sample:		278.7 time, 280.2 real, 334.8 MB
[runlim] sample:		288.7 time, 290.3 real, 126.5 MB
[runlim] sample:		298.7 time, 300.3 real, 126.5 MB
[runlim] sample:		308.7 time, 310.3 real, 135.7 MB
[runlim] sample:		318.7 time, 320.3 real, 157.2 MB
[runlim] sample:		328.6 time, 330.3 real, 140.7 MB
[runlim] sample:		13.5 time, 340.3 real, 1080.9 MB
[runlim] sample:		52.9 time, 350.3 real, 2364.7 MB
[runlim] sample:		92.5 time, 360.2 real, 3100.7 MB
[runlim] sample:		132.1 time, 370.3 real, 3608.4 MB
[runlim] sample:		171.6 time, 380.3 real, 3561.5 MB
[runlim] sample:		211.1 time, 390.2 real, 4273.2 MB
[runlim] sample:		250.7 time, 400.3 real, 4456.9 MB
[runlim] sample:		290.2 time, 410.2 real, 5103.7 MB
[runlim] sample:		329.6 time, 420.3 real, 5290.1 MB
[runlim] sample:		369.2 time, 430.3 real, 5334.6 MB
[runlim] sample:		408.8 time, 440.2 real, 5357.9 MB
[runlim] sample:		448.3 time, 450.3 real, 5372.9 MB
[runlim] sample:		487.8 time, 460.3 real, 5499.2 MB
[runlim] sample:		527.3 time, 470.3 real, 5502.3 MB
[runlim] sample:		566.9 time, 480.3 real, 5567.3 MB
[runlim] sample:		606.4 time, 490.3 real, 5617.2 MB
[runlim] sample:		646.0 time, 500.3 real, 5842.9 MB
[runlim] sample:		685.5 time, 510.3 real, 5940.2 MB
[runlim] sample:		725.0 time, 520.3 real, 5947.2 MB
[runlim] sample:		764.5 time, 530.3 real, 5952.2 MB
[runlim] sample:		804.1 time, 540.3 real, 5967.3 MB
[runlim] sample:		843.6 time, 550.3 real, 5848.3 MB
[runlim] sample:		883.1 time, 560.3 real, 5857.1 MB
[runlim] sample:		922.6 time, 570.3 real, 5863.8 MB
[runlim] sample:		962.2 time, 580.3 real, 5868.6 MB
[runlim] sample:		1001.7 time, 590.3 real, 5870.1 MB
[runlim] sample:		1041.2 time, 600.3 real, 5871.4 MB
[runlim] sample:		1080.8 time, 610.3 real, 5874.4 MB
[runlim] sample:		1120.3 time, 620.3 real, 5877.0 MB
[runlim] sample:		1159.8 time, 630.3 real, 5877.5 MB
[runlim] sample:		1199.3 time, 640.3 real, 5885.5 MB
[runlim] sample:		1238.8 time, 650.3 real, 5890.2 MB
[runlim] sample:		1278.3 time, 660.3 real, 5996.3 MB
[runlim] sample:		1317.8 time, 670.3 real, 6039.8 MB
[runlim] sample:		1357.3 time, 680.3 real, 6201.5 MB
[runlim] sample:		1396.9 time, 690.3 real, 6298.2 MB
[runlim] sample:		1436.4 time, 700.3 real, 6308.9 MB
[runlim] sample:		1475.9 time, 710.3 real, 6317.5 MB
[runlim] sample:		1515.4 time, 720.3 real, 6326.0 MB
[runlim] sample:		1554.9 time, 730.3 real, 6330.2 MB
[runlim] sample:		1594.4 time, 740.3 real, 6337.0 MB
[runlim] sample:		1633.9 time, 750.3 real, 6341.7 MB
[runlim] sample:		1673.4 time, 760.3 real, 6345.9 MB
[runlim] sample:		1712.9 time, 770.3 real, 6346.4 MB
[runlim] sample:		1752.5 time, 780.3 real, 6348.7 MB
[runlim] sample:		1792.0 time, 790.3 real, 6355.3 MB
[runlim] sample:		1831.4 time, 800.3 real, 6358.4 MB
[runlim] sample:		1871.0 time, 810.3 real, 6359.1 MB
[runlim] sample:		1910.5 time, 820.3 real, 6368.2 MB
[runlim] sample:		1950.0 time, 830.3 real, 6368.9 MB
[runlim] sample:		1989.4 time, 840.3 real, 6369.7 MB
[runlim] sample:		2028.9 time, 850.3 real, 6370.7 MB
[runlim] sample:		2068.3 time, 860.3 real, 6303.6 MB
[runlim] sample:		2107.8 time, 870.3 real, 6314.6 MB
[runlim] sample:		2147.4 time, 880.2 real, 6331.9 MB
[runlim] sample:		2186.9 time, 890.3 real, 6337.2 MB
[runlim] sample:		2226.4 time, 900.3 real, 6339.7 MB
[runlim] sample:		2265.8 time, 910.3 real, 6348.2 MB
[runlim] sample:		2305.3 time, 920.3 real, 6361.0 MB
[runlim] sample:		2344.9 time, 930.3 real, 6368.0 MB
[runlim] sample:		2384.4 time, 940.3 real, 6380.8 MB
[runlim] sample:		2423.9 time, 950.3 real, 6385.6 MB
[runlim] sample:		2463.4 time, 960.3 real, 6396.6 MB
[runlim] sample:		2502.9 time, 970.3 real, 6409.4 MB
[runlim] sample:		2542.4 time, 980.3 real, 6417.9 MB
[runlim] sample:		2581.9 time, 990.3 real, 6420.7 MB
[runlim] sample:		2621.4 time, 1000.3 real, 6425.2 MB
[runlim] sample:		2660.9 time, 1010.3 real, 6670.7 MB
[runlim] sample:		2700.4 time, 1020.3 real, 6354.0 MB
[runlim] sample:		2740.0 time, 1030.3 real, 6360.5 MB
[runlim] sample:		2779.5 time, 1040.3 real, 6363.0 MB
[runlim] sample:		2819.0 time, 1050.3 real, 6365.3 MB
[runlim] sample:		2858.5 time, 1060.3 real, 6371.8 MB
[runlim] sample:		2898.0 time, 1070.3 real, 6372.3 MB
[runlim] sample:		2937.5 time, 1080.3 real, 6374.6 MB
[runlim] sample:		2977.0 time, 1090.3 real, 6381.1 MB
[runlim] sample:		3016.5 time, 1100.3 real, 6315.1 MB
[runlim] sample:		3056.0 time, 1110.3 real, 6315.8 MB
[runlim] sample:		3095.5 time, 1120.3 real, 6320.0 MB
[runlim] sample:		3135.1 time, 1130.2 real, 6320.3 MB
[runlim] sample:		3174.6 time, 1140.3 real, 6326.8 MB
[runlim] sample:		3214.1 time, 1150.3 real, 6327.3 MB
[runlim] sample:		3253.6 time, 1160.3 real, 6331.5 MB
[runlim] sample:		3293.1 time, 1170.3 real, 6331.7 MB
[runlim] sample:		3332.7 time, 1180.3 real, 6332.2 MB
[runlim] sample:		3372.2 time, 1190.3 real, 6334.7 MB
[runlim] sample:		3411.7 time, 1200.3 real, 6337.3 MB
[runlim] sample:		3451.2 time, 1210.2 real, 6339.3 MB
[runlim] sample:		3490.8 time, 1220.2 real, 6353.8 MB
[runlim] sample:		3530.3 time, 1230.3 real, 6362.3 MB
[runlim] sample:		3569.8 time, 1240.3 real, 6365.4 MB
[runlim] sample:		3609.3 time, 1250.3 real, 5854.2 MB
[runlim] sample:		3648.8 time, 1260.3 real, 5870.5 MB
[runlim] sample:		3688.3 time, 1270.3 real, 5872.2 MB
[runlim] sample:		3727.9 time, 1280.3 real, 5872.4 MB
[runlim] sample:		3767.4 time, 1290.3 real, 5876.1 MB
[runlim] sample:		3806.9 time, 1300.3 real, 5876.3 MB
[runlim] sample:		3846.5 time, 1310.3 real, 5876.8 MB
[runlim] sample:		3885.9 time, 1320.3 real, 5877.1 MB
[runlim] sample:		3925.4 time, 1330.3 real, 5877.4 MB
[runlim] sample:		3964.9 time, 1340.3 real, 5879.6 MB
[runlim] sample:		4004.4 time, 1350.3 real, 5879.9 MB
[runlim] sample:		4044.0 time, 1360.3 real, 5880.4 MB
[runlim] sample:		4083.5 time, 1370.3 real, 5882.7 MB
[runlim] sample:		4123.1 time, 1380.3 real, 5883.2 MB
[runlim] sample:		4162.6 time, 1390.3 real, 5883.7 MB
[runlim] sample:		4202.2 time, 1400.3 real, 5885.9 MB
[runlim] sample:		4241.7 time, 1410.3 real, 5886.2 MB
[runlim] sample:		4281.3 time, 1420.3 real, 5890.5 MB
[runlim] sample:		4320.8 time, 1430.3 real, 5892.8 MB
[runlim] sample:		4360.4 time, 1440.3 real, 5895.1 MB
[runlim] sample:		4399.9 time, 1450.3 real, 5895.7 MB
[runlim] sample:		4439.4 time, 1460.2 real, 5899.7 MB
[runlim] sample:		4478.9 time, 1470.3 real, 5900.2 MB
[runlim] sample:		4518.4 time, 1480.3 real, 5900.5 MB
[runlim] sample:		4558.0 time, 1490.3 real, 5900.8 MB
[runlim] sample:		4597.5 time, 1500.3 real, 5901.0 MB
[runlim] sample:		4637.0 time, 1510.3 real, 5903.5 MB
[runlim] sample:		4676.6 time, 1520.3 real, 5905.8 MB
[runlim] sample:		4716.1 time, 1530.3 real, 5906.2 MB
[runlim] sample:		4755.6 time, 1540.3 real, 5906.7 MB
[runlim] sample:		4795.1 time, 1550.3 real, 5909.3 MB
[runlim] sample:		4834.7 time, 1560.2 real, 5909.5 MB
[runlim] sample:		4874.2 time, 1570.3 real, 5911.8 MB
[runlim] sample:		4913.8 time, 1580.3 real, 5931.0 MB
[runlim] sample:		4953.3 time, 1590.3 real, 6027.9 MB
[runlim] sample:		4992.8 time, 1600.3 real, 6039.0 MB
[runlim] sample:		5032.3 time, 1610.3 real, 6041.5 MB
[runlim] sample:		5071.9 time, 1620.3 real, 6057.7 MB
[runlim] sample:		5111.4 time, 1630.3 real, 6060.9 MB
[runlim] sample:		5151.0 time, 1640.3 real, 6066.5 MB
[runlim] sample:		5190.5 time, 1650.3 real, 6068.7 MB
[runlim] sample:		5230.1 time, 1660.3 real, 6071.0 MB
[runlim] sample:		5269.6 time, 1670.3 real, 6073.4 MB
[runlim] sample:		5309.1 time, 1680.3 real, 6073.7 MB
[runlim] sample:		5348.6 time, 1690.3 real, 6074.6 MB
[runlim] sample:		5388.1 time, 1700.2 real, 6075.7 MB
[runlim] sample:		5427.6 time, 1710.3 real, 6078.0 MB
[runlim] sample:		5467.2 time, 1720.3 real, 6082.5 MB
[runlim] sample:		5506.7 time, 1730.3 real, 5937.8 MB
[runlim] sample:		5546.2 time, 1740.3 real, 5940.2 MB
[runlim] sample:		5585.8 time, 1750.2 real, 5944.2 MB
[runlim] sample:		5625.3 time, 1760.2 real, 5944.5 MB
[runlim] sample:		5664.8 time, 1770.2 real, 5945.0 MB
[runlim] sample:		5704.4 time, 1780.2 real, 5947.3 MB
[runlim] sample:		5743.9 time, 1790.2 real, 5947.5 MB
[runlim] sample:		5783.5 time, 1800.3 real, 5953.8 MB
[runlim] sample:		5822.9 time, 1810.3 real, 6008.8 MB
[runlim] sample:		5862.5 time, 1820.3 real, 6012.1 MB
[runlim] sample:		5902.0 time, 1830.3 real, 5986.5 MB
[runlim] sample:		5941.5 time, 1840.3 real, 5987.6 MB
[runlim] sample:		5981.0 time, 1850.2 real, 5990.3 MB
[runlim] sample:		6020.5 time, 1860.2 real, 5993.4 MB
[runlim] sample:		6060.0 time, 1870.3 real, 5996.1 MB
[runlim] sample:		6099.4 time, 1880.2 real, 6003.3 MB
[runlim] sample:		6139.0 time, 1890.3 real, 6035.1 MB
[runlim] sample:		6178.5 time, 1900.3 real, 6080.9 MB
[runlim] sample:		6218.1 time, 1910.3 real, 6199.5 MB
[runlim] sample:		6257.6 time, 1920.3 real, 6349.9 MB
[runlim] sample:		6297.2 time, 1930.3 real, 6555.6 MB
[runlim] sample:		6336.7 time, 1940.3 real, 6562.4 MB
[runlim] sample:		6376.2 time, 1950.3 real, 6567.1 MB
[runlim] sample:		6415.8 time, 1960.2 real, 6570.2 MB
[runlim] sample:		6455.4 time, 1970.2 real, 6578.9 MB
[runlim] sample:		6494.9 time, 1980.3 real, 6582.0 MB
[runlim] sample:		6534.4 time, 1990.3 real, 6586.5 MB
[runlim] sample:		6573.9 time, 2000.3 real, 6593.3 MB
[runlim] sample:		6613.4 time, 2010.3 real, 6600.3 MB
[runlim] sample:		6652.9 time, 2020.3 real, 6609.3 MB
[runlim] sample:		6692.4 time, 2030.2 real, 6612.4 MB
[runlim] sample:		6731.9 time, 2040.3 real, 6617.4 MB
[runlim] sample:		6771.4 time, 2050.3 real, 6622.2 MB
[runlim] sample:		6810.9 time, 2060.3 real, 6626.2 MB
[runlim] sample:		6850.5 time, 2070.3 real, 6632.5 MB
[runlim] sample:		6890.0 time, 2080.3 real, 6640.9 MB
[runlim] sample:		6929.5 time, 2090.3 real, 6714.4 MB
[runlim] sample:		6969.0 time, 2100.3 real, 6717.5 MB
[runlim] sample:		7008.5 time, 2110.3 real, 6723.6 MB
[runlim] sample:		7048.0 time, 2120.3 real, 6727.6 MB
[runlim] sample:		7087.5 time, 2130.3 real, 6727.6 MB
[runlim] end:			Fri Sep 18 12:23:09 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		75502
[runlim] real:			2139.53 seconds
[runlim] time:			7123.88 seconds
[runlim] space:			7008.8 MB
[runlim] samples:		21392
