[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/iprover/single.iproverhc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a07b0s.aig
[runlim] start:			Mon Sep 28 15:25:46 2015
[runlim] main pid:		18607
[runlim] sample:		9.2 time, 10.7 real, 639.8 MB
[runlim] sample:		19.2 time, 20.7 real, 1209.5 MB
[runlim] sample:		29.2 time, 30.7 real, 1491.5 MB
[runlim] sample:		39.1 time, 40.7 real, 1827.9 MB
[runlim] sample:		49.1 time, 50.7 real, 2077.3 MB
[runlim] sample:		59.1 time, 60.7 real, 2307.1 MB
[runlim] sample:		69.1 time, 70.7 real, 2405.3 MB
[runlim] sample:		79.1 time, 80.7 real, 2513.2 MB
[runlim] sample:		89.1 time, 90.7 real, 2921.3 MB
[runlim] sample:		99.1 time, 100.7 real, 3177.3 MB
[runlim] sample:		109.0 time, 110.7 real, 3562.8 MB
[runlim] sample:		119.0 time, 120.7 real, 3925.4 MB
[runlim] sample:		129.0 time, 130.7 real, 4246.6 MB
[runlim] sample:		139.0 time, 140.7 real, 4608.3 MB
[runlim] sample:		149.0 time, 150.7 real, 4629.7 MB
[runlim] sample:		159.0 time, 160.7 real, 4648.3 MB
[runlim] sample:		169.0 time, 170.7 real, 4683.1 MB
[runlim] sample:		178.9 time, 180.7 real, 5043.9 MB
[runlim] sample:		188.9 time, 190.7 real, 5090.9 MB
[runlim] sample:		198.9 time, 200.7 real, 5113.3 MB
[runlim] sample:		208.9 time, 210.7 real, 5140.5 MB
[runlim] sample:		218.9 time, 220.7 real, 5164.9 MB
[runlim] sample:		228.8 time, 230.7 real, 5184.1 MB
[runlim] sample:		238.8 time, 240.7 real, 5187.0 MB
[runlim] sample:		248.8 time, 250.7 real, 5231.5 MB
[runlim] sample:		258.8 time, 260.7 real, 5259.4 MB
[runlim] sample:		268.8 time, 270.7 real, 5278.4 MB
[runlim] sample:		278.8 time, 280.7 real, 5298.6 MB
[runlim] sample:		288.8 time, 290.7 real, 5327.1 MB
[runlim] sample:		298.7 time, 300.7 real, 5345.6 MB
[runlim] sample:		308.7 time, 310.7 real, 5365.6 MB
[runlim] sample:		318.7 time, 320.7 real, 5387.1 MB
[runlim] sample:		328.7 time, 330.7 real, 5405.4 MB
[runlim] sample:		338.7 time, 340.7 real, 5424.9 MB
[runlim] sample:		348.6 time, 350.7 real, 5443.1 MB
[runlim] sample:		358.6 time, 360.7 real, 5463.4 MB
[runlim] sample:		368.6 time, 370.7 real, 5482.3 MB
[runlim] sample:		378.6 time, 380.7 real, 5497.1 MB
[runlim] sample:		388.6 time, 390.7 real, 5523.4 MB
[runlim] sample:		398.6 time, 400.7 real, 5537.6 MB
[runlim] sample:		408.6 time, 410.7 real, 5552.6 MB
[runlim] sample:		418.5 time, 420.7 real, 5563.2 MB
[runlim] sample:		428.5 time, 430.7 real, 5576.7 MB
[runlim] sample:		438.5 time, 440.7 real, 5592.8 MB
[runlim] sample:		448.5 time, 450.7 real, 5605.1 MB
[runlim] sample:		458.5 time, 460.7 real, 5613.6 MB
[runlim] sample:		468.5 time, 470.7 real, 5620.6 MB
[runlim] sample:		478.5 time, 480.7 real, 5629.0 MB
[runlim] sample:		488.5 time, 490.7 real, 5636.0 MB
[runlim] sample:		498.4 time, 500.7 real, 5647.0 MB
[runlim] sample:		508.4 time, 510.7 real, 5658.6 MB
[runlim] sample:		518.4 time, 520.7 real, 5669.6 MB
[runlim] sample:		528.4 time, 530.7 real, 5679.1 MB
[runlim] sample:		538.4 time, 540.7 real, 5688.4 MB
[runlim] sample:		548.4 time, 550.7 real, 5695.6 MB
[runlim] sample:		558.4 time, 560.7 real, 5704.7 MB
[runlim] sample:		568.4 time, 570.7 real, 5716.7 MB
[runlim] sample:		578.4 time, 580.7 real, 5729.5 MB
[runlim] sample:		588.3 time, 590.7 real, 5735.7 MB
[runlim] sample:		598.3 time, 600.7 real, 5746.3 MB
[runlim] sample:		608.3 time, 610.7 real, 5754.3 MB
[runlim] sample:		618.3 time, 620.7 real, 5158.0 MB
[runlim] sample:		628.3 time, 630.7 real, 5194.2 MB
[runlim] sample:		638.3 time, 640.7 real, 5219.5 MB
[runlim] sample:		648.3 time, 650.7 real, 5247.5 MB
[runlim] sample:		658.3 time, 660.7 real, 5266.2 MB
[runlim] sample:		668.3 time, 670.7 real, 5268.2 MB
[runlim] sample:		678.2 time, 680.7 real, 5284.2 MB
[runlim] sample:		688.2 time, 690.7 real, 5312.2 MB
[runlim] sample:		698.2 time, 700.7 real, 5341.9 MB
[runlim] sample:		708.2 time, 710.7 real, 5369.9 MB
[runlim] sample:		718.2 time, 720.7 real, 5394.1 MB
[runlim] sample:		728.2 time, 730.7 real, 5420.1 MB
[runlim] sample:		738.2 time, 740.7 real, 5438.1 MB
[runlim] sample:		748.2 time, 750.7 real, 5452.1 MB
[runlim] sample:		758.2 time, 760.7 real, 5476.0 MB
[runlim] sample:		768.1 time, 770.7 real, 5496.0 MB
[runlim] sample:		778.1 time, 780.7 real, 5512.2 MB
[runlim] sample:		788.1 time, 790.7 real, 5538.2 MB
[runlim] sample:		798.1 time, 800.7 real, 5556.2 MB
[runlim] sample:		808.1 time, 810.7 real, 5570.2 MB
[runlim] sample:		818.1 time, 820.7 real, 5580.2 MB
[runlim] sample:		828.1 time, 830.7 real, 5588.2 MB
[runlim] sample:		838.1 time, 840.7 real, 5602.2 MB
[runlim] sample:		848.1 time, 850.7 real, 5618.5 MB
[runlim] sample:		858.1 time, 860.7 real, 5630.5 MB
[runlim] sample:		868.0 time, 870.7 real, 5650.5 MB
[runlim] sample:		878.0 time, 880.7 real, 5664.6 MB
[runlim] sample:		888.0 time, 890.7 real, 5679.4 MB
[runlim] sample:		898.0 time, 900.7 real, 5697.4 MB
[runlim] sample:		8.9 time, 910.7 real, 618.7 MB
[runlim] sample:		18.9 time, 920.7 real, 1181.4 MB
[runlim] sample:		28.9 time, 930.7 real, 1479.5 MB
[runlim] sample:		38.9 time, 940.7 real, 1816.8 MB
[runlim] sample:		48.9 time, 950.7 real, 2067.1 MB
[runlim] sample:		58.9 time, 960.7 real, 2299.0 MB
[runlim] sample:		68.9 time, 970.7 real, 2395.1 MB
[runlim] sample:		78.8 time, 980.7 real, 2507.1 MB
[runlim] sample:		88.8 time, 990.7 real, 2915.2 MB
[runlim] sample:		98.8 time, 1000.7 real, 3159.7 MB
[runlim] sample:		108.8 time, 1010.7 real, 3297.7 MB
[runlim] sample:		118.8 time, 1020.7 real, 3575.4 MB
[runlim] sample:		128.8 time, 1030.7 real, 3723.3 MB
[runlim] sample:		138.8 time, 1040.7 real, 4010.5 MB
[runlim] sample:		148.8 time, 1050.7 real, 4162.6 MB
[runlim] sample:		158.8 time, 1060.7 real, 4511.3 MB
[runlim] sample:		168.7 time, 1070.7 real, 4699.6 MB
[runlim] sample:		178.7 time, 1080.7 real, 4818.7 MB
[runlim] sample:		188.7 time, 1090.7 real, 5108.0 MB
[runlim] sample:		198.7 time, 1100.7 real, 5269.5 MB
[runlim] sample:		208.7 time, 1110.7 real, 5386.4 MB
[runlim] sample:		218.7 time, 1120.7 real, 5409.8 MB
[runlim] sample:		228.7 time, 1130.7 real, 5431.2 MB
[runlim] sample:		238.7 time, 1140.7 real, 5482.9 MB
[runlim] sample:		248.6 time, 1150.7 real, 5616.9 MB
[runlim] sample:		258.6 time, 1160.7 real, 5618.4 MB
[runlim] sample:		268.6 time, 1170.7 real, 5618.4 MB
[runlim] sample:		278.6 time, 1180.7 real, 5641.6 MB
[runlim] sample:		288.6 time, 1190.7 real, 5662.4 MB
[runlim] sample:		298.6 time, 1200.7 real, 5688.7 MB
[runlim] sample:		308.6 time, 1210.7 real, 5708.1 MB
[runlim] sample:		318.6 time, 1220.7 real, 5730.1 MB
[runlim] sample:		328.6 time, 1230.7 real, 5763.1 MB
[runlim] sample:		338.5 time, 1240.7 real, 5783.7 MB
[runlim] sample:		348.5 time, 1250.7 real, 5789.5 MB
[runlim] sample:		358.5 time, 1260.7 real, 5801.8 MB
[runlim] sample:		368.5 time, 1270.7 real, 5820.1 MB
[runlim] sample:		378.5 time, 1280.7 real, 5843.9 MB
[runlim] sample:		388.5 time, 1290.7 real, 5868.7 MB
[runlim] sample:		398.5 time, 1300.7 real, 5887.2 MB
[runlim] sample:		408.5 time, 1310.7 real, 5911.0 MB
[runlim] sample:		418.5 time, 1320.7 real, 5930.7 MB
[runlim] sample:		428.4 time, 1330.7 real, 5945.0 MB
[runlim] sample:		438.4 time, 1340.7 real, 5955.3 MB
[runlim] sample:		448.4 time, 1350.7 real, 5966.5 MB
[runlim] sample:		458.4 time, 1360.7 real, 5978.6 MB
[runlim] sample:		468.4 time, 1370.7 real, 5987.8 MB
[runlim] sample:		478.4 time, 1380.7 real, 5997.4 MB
[runlim] sample:		488.4 time, 1390.7 real, 6013.9 MB
[runlim] sample:		498.4 time, 1400.7 real, 6033.7 MB
[runlim] sample:		508.4 time, 1410.7 real, 6051.2 MB
[runlim] sample:		518.3 time, 1420.7 real, 6080.2 MB
[runlim] sample:		528.3 time, 1430.7 real, 6096.4 MB
[runlim] sample:		538.3 time, 1440.7 real, 6109.2 MB
[runlim] sample:		548.3 time, 1450.7 real, 6124.2 MB
[runlim] sample:		558.3 time, 1460.7 real, 6137.5 MB
[runlim] sample:		568.3 time, 1470.7 real, 6147.8 MB
[runlim] sample:		578.3 time, 1480.7 real, 6156.0 MB
[runlim] sample:		588.3 time, 1490.7 real, 6175.6 MB
[runlim] sample:		598.3 time, 1500.7 real, 6192.9 MB
[runlim] sample:		608.2 time, 1510.7 real, 6205.2 MB
[runlim] sample:		618.2 time, 1520.7 real, 6221.8 MB
[runlim] sample:		628.2 time, 1530.7 real, 6232.0 MB
[runlim] sample:		638.2 time, 1540.7 real, 6242.5 MB
[runlim] sample:		648.2 time, 1550.7 real, 6255.6 MB
[runlim] sample:		658.2 time, 1560.7 real, 6265.3 MB
[runlim] sample:		668.2 time, 1570.7 real, 6273.0 MB
[runlim] sample:		678.2 time, 1580.7 real, 6284.7 MB
[runlim] sample:		688.2 time, 1590.7 real, 6296.7 MB
[runlim] sample:		698.2 time, 1600.7 real, 5686.9 MB
[runlim] sample:		708.1 time, 1610.7 real, 5727.4 MB
[runlim] sample:		718.1 time, 1620.7 real, 5761.7 MB
[runlim] sample:		728.1 time, 1630.7 real, 5794.2 MB
[runlim] sample:		738.1 time, 1640.7 real, 5826.2 MB
[runlim] sample:		748.1 time, 1650.7 real, 5856.2 MB
[runlim] sample:		758.1 time, 1660.7 real, 5880.6 MB
[runlim] sample:		768.1 time, 1670.7 real, 5894.6 MB
[runlim] sample:		778.1 time, 1680.7 real, 5913.4 MB
[runlim] sample:		788.1 time, 1690.7 real, 5933.4 MB
[runlim] sample:		798.0 time, 1700.7 real, 5941.4 MB
[runlim] sample:		808.0 time, 1710.7 real, 5962.6 MB
[runlim] sample:		818.0 time, 1720.7 real, 5982.3 MB
[runlim] sample:		828.0 time, 1730.7 real, 6002.3 MB
[runlim] sample:		838.0 time, 1740.7 real, 6020.3 MB
[runlim] sample:		848.0 time, 1750.7 real, 6034.3 MB
[runlim] sample:		858.0 time, 1760.7 real, 6057.7 MB
[runlim] sample:		868.0 time, 1770.7 real, 6075.7 MB
[runlim] sample:		878.0 time, 1780.7 real, 6085.7 MB
[runlim] sample:		888.0 time, 1790.7 real, 6101.7 MB
[runlim] sample:		898.0 time, 1800.7 real, 6116.1 MB
[runlim] sample:		8.5 time, 1810.7 real, 606.5 MB
[runlim] sample:		18.5 time, 1820.7 real, 1176.9 MB
[runlim] sample:		28.5 time, 1830.7 real, 1484.8 MB
[runlim] sample:		38.4 time, 1840.7 real, 1825.2 MB
[runlim] sample:		48.4 time, 1850.7 real, 2078.7 MB
[runlim] sample:		58.4 time, 1860.7 real, 2316.7 MB
[runlim] sample:		68.4 time, 1870.7 real, 2412.7 MB
[runlim] sample:		78.4 time, 1880.7 real, 2526.8 MB
[runlim] sample:		88.4 time, 1890.7 real, 2916.2 MB
[runlim] sample:		98.4 time, 1900.7 real, 3216.7 MB
[runlim] sample:		108.4 time, 1910.7 real, 3393.1 MB
[runlim] sample:		118.3 time, 1920.7 real, 3683.0 MB
[runlim] sample:		128.3 time, 1930.7 real, 3825.0 MB
[runlim] sample:		138.3 time, 1940.7 real, 3911.0 MB
[runlim] sample:		148.3 time, 1950.7 real, 4167.4 MB
[runlim] sample:		158.3 time, 1960.7 real, 4409.9 MB
[runlim] sample:		168.3 time, 1970.7 real, 4597.2 MB
[runlim] sample:		178.2 time, 1980.7 real, 4717.3 MB
[runlim] sample:		188.2 time, 1990.7 real, 4827.3 MB
[runlim] sample:		198.2 time, 2000.7 real, 4936.7 MB
[runlim] sample:		208.2 time, 2010.7 real, 5058.9 MB
[runlim] sample:		218.2 time, 2020.7 real, 5153.3 MB
[runlim] sample:		228.2 time, 2030.7 real, 5277.2 MB
[runlim] sample:		238.2 time, 2040.7 real, 5277.2 MB
[runlim] sample:		248.2 time, 2050.7 real, 5277.2 MB
[runlim] sample:		258.2 time, 2060.7 real, 5277.2 MB
[runlim] sample:		268.1 time, 2070.7 real, 5277.2 MB
[runlim] sample:		278.1 time, 2080.7 real, 5306.5 MB
[runlim] sample:		288.1 time, 2090.7 real, 5393.2 MB
[runlim] sample:		298.1 time, 2100.7 real, 5434.6 MB
[runlim] sample:		308.1 time, 2110.7 real, 5505.8 MB
[runlim] sample:		318.1 time, 2120.7 real, 5572.8 MB
[runlim] sample:		328.1 time, 2130.7 real, 5686.7 MB
[runlim] sample:		338.1 time, 2140.7 real, 5762.4 MB
[runlim] sample:		348.0 time, 2150.7 real, 5792.9 MB
[runlim] sample:		358.0 time, 2160.7 real, 5989.2 MB
[runlim] sample:		368.0 time, 2170.7 real, 6082.6 MB
[runlim] sample:		378.0 time, 2180.7 real, 6236.5 MB
[runlim] sample:		388.0 time, 2190.7 real, 6368.7 MB
[runlim] sample:		398.0 time, 2200.7 real, 6523.7 MB
[runlim] sample:		4.0 time, 2210.7 real, 324.7 MB
[runlim] sample:		14.0 time, 2220.7 real, 958.0 MB
[runlim] sample:		24.0 time, 2230.7 real, 1305.1 MB
[runlim] sample:		33.9 time, 2240.7 real, 1822.7 MB
[runlim] sample:		43.9 time, 2250.7 real, 1983.8 MB
[runlim] sample:		53.9 time, 2260.7 real, 2542.6 MB
[runlim] sample:		63.9 time, 2270.7 real, 2706.6 MB
[runlim] sample:		73.9 time, 2280.7 real, 3175.7 MB
[runlim] sample:		83.9 time, 2290.7 real, 3339.1 MB
[runlim] sample:		93.9 time, 2300.7 real, 3684.7 MB
[runlim] sample:		103.8 time, 2310.7 real, 3974.5 MB
[runlim] sample:		113.8 time, 2320.7 real, 4053.0 MB
[runlim] sample:		123.8 time, 2330.7 real, 4501.5 MB
[runlim] sample:		133.8 time, 2340.7 real, 4687.0 MB
[runlim] sample:		143.8 time, 2350.7 real, 4778.1 MB
[runlim] sample:		153.8 time, 2360.7 real, 4791.8 MB
[runlim] sample:		163.8 time, 2370.7 real, 4803.8 MB
[runlim] sample:		173.8 time, 2380.7 real, 4813.4 MB
[runlim] sample:		183.7 time, 2390.7 real, 4825.6 MB
[runlim] sample:		193.7 time, 2400.7 real, 4833.6 MB
[runlim] sample:		203.7 time, 2410.7 real, 4849.6 MB
[runlim] sample:		213.7 time, 2420.7 real, 4861.1 MB
[runlim] sample:		223.7 time, 2430.7 real, 4870.7 MB
[runlim] sample:		233.7 time, 2440.7 real, 4884.7 MB
[runlim] sample:		243.7 time, 2450.7 real, 4893.4 MB
[runlim] sample:		253.7 time, 2460.7 real, 4904.5 MB
[runlim] sample:		263.6 time, 2470.7 real, 4913.5 MB
[runlim] sample:		273.6 time, 2480.7 real, 4925.1 MB
[runlim] sample:		283.6 time, 2490.7 real, 4936.1 MB
[runlim] sample:		293.6 time, 2500.7 real, 4946.8 MB
[runlim] sample:		303.6 time, 2510.7 real, 4959.4 MB
[runlim] sample:		313.6 time, 2520.7 real, 4967.4 MB
[runlim] sample:		323.6 time, 2530.7 real, 4977.2 MB
[runlim] sample:		333.6 time, 2540.7 real, 4984.9 MB
[runlim] sample:		343.6 time, 2550.7 real, 4994.0 MB
[runlim] sample:		353.6 time, 2560.7 real, 5394.7 MB
[runlim] sample:		363.5 time, 2570.7 real, 5706.7 MB
[runlim] sample:		373.5 time, 2580.7 real, 5803.1 MB
[runlim] sample:		383.5 time, 2590.7 real, 5837.8 MB
[runlim] sample:		393.5 time, 2600.7 real, 5846.0 MB
[runlim] sample:		403.5 time, 2610.7 real, 5852.0 MB
[runlim] sample:		413.5 time, 2620.7 real, 5861.8 MB
[runlim] sample:		423.5 time, 2630.7 real, 5872.1 MB
[runlim] sample:		433.5 time, 2640.7 real, 5884.4 MB
[runlim] sample:		443.4 time, 2650.7 real, 5898.6 MB
[runlim] sample:		453.4 time, 2660.7 real, 5909.8 MB
[runlim] sample:		463.4 time, 2670.7 real, 5918.1 MB
[runlim] sample:		473.4 time, 2680.7 real, 5927.4 MB
[runlim] sample:		483.4 time, 2690.7 real, 5939.6 MB
[runlim] sample:		493.4 time, 2700.7 real, 5949.6 MB
[runlim] sample:		503.4 time, 2710.7 real, 5962.4 MB
[runlim] sample:		513.4 time, 2720.7 real, 5976.4 MB
[runlim] sample:		523.4 time, 2730.7 real, 5980.8 MB
[runlim] sample:		533.4 time, 2740.7 real, 5985.1 MB
[runlim] sample:		543.3 time, 2750.7 real, 5991.3 MB
[runlim] sample:		553.3 time, 2760.7 real, 5997.8 MB
[runlim] sample:		563.3 time, 2770.7 real, 6014.9 MB
[runlim] sample:		573.3 time, 2780.7 real, 6024.2 MB
[runlim] sample:		583.3 time, 2790.7 real, 6030.2 MB
[runlim] sample:		593.3 time, 2800.7 real, 6041.4 MB
[runlim] sample:		603.3 time, 2810.7 real, 6051.4 MB
[runlim] sample:		613.2 time, 2820.7 real, 6061.0 MB
[runlim] sample:		623.3 time, 2830.7 real, 6071.7 MB
[runlim] sample:		633.2 time, 2840.7 real, 6083.2 MB
[runlim] sample:		643.2 time, 2850.7 real, 6094.2 MB
[runlim] sample:		653.2 time, 2860.7 real, 6103.3 MB
[runlim] sample:		663.2 time, 2870.7 real, 6111.1 MB
[runlim] sample:		673.2 time, 2880.7 real, 6119.3 MB
[runlim] sample:		683.2 time, 2890.7 real, 6129.1 MB
[runlim] sample:		693.2 time, 2900.7 real, 6136.6 MB
[runlim] sample:		703.1 time, 2910.7 real, 6144.4 MB
[runlim] sample:		713.1 time, 2920.7 real, 6151.7 MB
[runlim] sample:		723.1 time, 2930.7 real, 6157.8 MB
[runlim] sample:		733.1 time, 2940.7 real, 6167.8 MB
[runlim] sample:		743.1 time, 2950.7 real, 6178.5 MB
[runlim] sample:		753.1 time, 2960.7 real, 6181.8 MB
[runlim] sample:		763.1 time, 2970.7 real, 6184.6 MB
[runlim] sample:		773.1 time, 2980.7 real, 6188.9 MB
[runlim] sample:		783.1 time, 2990.7 real, 6192.2 MB
[runlim] sample:		793.1 time, 3000.7 real, 6195.7 MB
[runlim] sample:		803.0 time, 3010.7 real, 6198.3 MB
[runlim] sample:		813.0 time, 3020.7 real, 6202.1 MB
[runlim] sample:		823.0 time, 3030.7 real, 6218.0 MB
[runlim] sample:		833.0 time, 3040.7 real, 6229.3 MB
[runlim] sample:		843.0 time, 3050.7 real, 6239.0 MB
[runlim] sample:		853.0 time, 3060.7 real, 6249.2 MB
[runlim] sample:		863.0 time, 3070.7 real, 6260.0 MB
[runlim] sample:		873.0 time, 3080.7 real, 6272.0 MB
[runlim] sample:		3.5 time, 3090.7 real, 287.0 MB
[runlim] sample:		13.5 time, 3100.7 real, 932.1 MB
[runlim] sample:		23.5 time, 3110.7 real, 1418.5 MB
[runlim] sample:		33.5 time, 3120.7 real, 1645.7 MB
[runlim] sample:		43.5 time, 3130.7 real, 1949.7 MB
[runlim] sample:		53.4 time, 3140.7 real, 2214.8 MB
[runlim] sample:		63.4 time, 3150.7 real, 2370.7 MB
[runlim] sample:		73.4 time, 3160.7 real, 2452.7 MB
[runlim] sample:		83.4 time, 3170.7 real, 2723.1 MB
[runlim] sample:		93.4 time, 3180.7 real, 3063.0 MB
[runlim] sample:		103.4 time, 3190.7 real, 3320.7 MB
[runlim] sample:		113.4 time, 3200.7 real, 3658.8 MB
[runlim] sample:		123.3 time, 3210.7 real, 3963.8 MB
[runlim] sample:		133.3 time, 3220.7 real, 4235.0 MB
[runlim] sample:		143.3 time, 3230.7 real, 4514.8 MB
[runlim] sample:		153.3 time, 3240.7 real, 4652.1 MB
[runlim] sample:		163.3 time, 3250.7 real, 5539.7 MB
[runlim] sample:		173.3 time, 3260.7 real, 5540.0 MB
[runlim] sample:		183.3 time, 3270.7 real, 5542.0 MB
[runlim] sample:		193.3 time, 3280.7 real, 5542.0 MB
[runlim] sample:		203.2 time, 3290.7 real, 5546.0 MB
[runlim] sample:		213.2 time, 3300.7 real, 5676.3 MB
[runlim] sample:		223.2 time, 3310.7 real, 5869.1 MB
[runlim] sample:		233.2 time, 3320.7 real, 5899.3 MB
[runlim] sample:		243.2 time, 3330.7 real, 5917.3 MB
[runlim] sample:		253.2 time, 3340.7 real, 5936.5 MB
[runlim] sample:		263.2 time, 3350.7 real, 5948.5 MB
[runlim] sample:		273.2 time, 3360.7 real, 5968.7 MB
[runlim] sample:		283.2 time, 3370.7 real, 5988.7 MB
[runlim] sample:		293.2 time, 3380.7 real, 6018.7 MB
[runlim] sample:		303.2 time, 3390.7 real, 6030.8 MB
[runlim] sample:		313.1 time, 3400.7 real, 6048.8 MB
[runlim] sample:		323.1 time, 3410.7 real, 6093.6 MB
[runlim] sample:		333.1 time, 3420.7 real, 6239.7 MB
[runlim] sample:		343.1 time, 3430.7 real, 6438.1 MB
[runlim] end:			Mon Sep 28 16:23:03 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		206144
[runlim] real:			3437.23 seconds
[runlim] time:			899.04 seconds
[runlim] space:			6603.1 MB
[runlim] samples:		34365
