[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/oski15a14b22s.aig
[runlim] start:			Mon Sep 28 14:24:34 2015
[runlim] main pid:		19307
[runlim] sample:		9.3 time, 10.6 real, 520.4 MB
[runlim] sample:		19.3 time, 20.6 real, 777.6 MB
[runlim] sample:		29.3 time, 30.6 real, 1031.4 MB
[runlim] sample:		39.3 time, 40.6 real, 1402.1 MB
[runlim] sample:		49.2 time, 50.6 real, 1488.9 MB
[runlim] sample:		59.2 time, 60.6 real, 1724.8 MB
[runlim] sample:		69.2 time, 70.6 real, 1901.2 MB
[runlim] sample:		79.2 time, 80.6 real, 2001.9 MB
[runlim] sample:		89.2 time, 90.6 real, 2226.0 MB
[runlim] sample:		99.2 time, 100.6 real, 2293.4 MB
[runlim] sample:		109.2 time, 110.6 real, 2467.3 MB
[runlim] sample:		119.2 time, 120.6 real, 2635.9 MB
[runlim] sample:		129.2 time, 130.6 real, 2635.9 MB
[runlim] sample:		139.1 time, 140.6 real, 2680.9 MB
[runlim] sample:		149.1 time, 150.6 real, 2792.6 MB
[runlim] sample:		159.1 time, 160.6 real, 2815.3 MB
[runlim] sample:		169.1 time, 170.6 real, 2817.1 MB
[runlim] sample:		179.1 time, 180.6 real, 2842.7 MB
[runlim] sample:		189.1 time, 190.6 real, 3010.0 MB
[runlim] sample:		199.1 time, 200.6 real, 3110.0 MB
[runlim] sample:		209.0 time, 210.6 real, 3286.6 MB
[runlim] sample:		219.0 time, 220.6 real, 3297.1 MB
[runlim] sample:		229.0 time, 230.6 real, 3306.1 MB
[runlim] sample:		239.0 time, 240.6 real, 3326.8 MB
[runlim] sample:		249.0 time, 250.6 real, 3329.9 MB
[runlim] sample:		259.0 time, 260.6 real, 3355.1 MB
[runlim] sample:		269.0 time, 270.6 real, 3517.0 MB
[runlim] sample:		279.0 time, 280.6 real, 3600.7 MB
[runlim] sample:		288.9 time, 290.6 real, 3727.3 MB
[runlim] sample:		298.9 time, 300.6 real, 3759.7 MB
[runlim] sample:		308.9 time, 310.6 real, 3763.0 MB
[runlim] sample:		318.9 time, 320.6 real, 3763.5 MB
[runlim] sample:		328.9 time, 330.6 real, 3766.0 MB
[runlim] sample:		338.9 time, 340.6 real, 3784.5 MB
[runlim] sample:		348.9 time, 350.6 real, 3801.5 MB
[runlim] sample:		358.9 time, 360.6 real, 3805.6 MB
[runlim] sample:		368.9 time, 370.6 real, 3807.6 MB
[runlim] sample:		378.9 time, 380.6 real, 3823.8 MB
[runlim] sample:		388.8 time, 390.6 real, 3974.2 MB
[runlim] sample:		398.8 time, 400.6 real, 4046.6 MB
[runlim] sample:		408.8 time, 410.6 real, 4102.6 MB
[runlim] sample:		418.8 time, 420.6 real, 4194.5 MB
[runlim] sample:		428.8 time, 430.6 real, 4306.8 MB
[runlim] sample:		438.8 time, 440.6 real, 4310.0 MB
[runlim] sample:		448.8 time, 450.6 real, 4312.0 MB
[runlim] sample:		458.8 time, 460.6 real, 4312.0 MB
[runlim] sample:		468.8 time, 470.6 real, 4324.5 MB
[runlim] sample:		478.7 time, 480.6 real, 4343.3 MB
[runlim] sample:		488.7 time, 490.6 real, 4345.1 MB
[runlim] sample:		498.7 time, 500.6 real, 4347.4 MB
[runlim] sample:		508.7 time, 510.6 real, 4350.9 MB
[runlim] sample:		518.7 time, 520.6 real, 4353.4 MB
[runlim] sample:		528.7 time, 530.6 real, 4356.7 MB
[runlim] sample:		538.7 time, 540.6 real, 4319.4 MB
[runlim] sample:		548.7 time, 550.6 real, 4323.9 MB
[runlim] sample:		558.6 time, 560.6 real, 4325.9 MB
[runlim] sample:		568.6 time, 570.6 real, 4327.9 MB
[runlim] sample:		578.6 time, 580.6 real, 4330.1 MB
[runlim] sample:		588.6 time, 590.6 real, 4334.6 MB
[runlim] sample:		598.6 time, 600.6 real, 4336.6 MB
[runlim] sample:		608.6 time, 610.6 real, 4341.6 MB
[runlim] sample:		618.6 time, 620.6 real, 4345.6 MB
[runlim] sample:		628.6 time, 630.6 real, 4347.6 MB
[runlim] sample:		638.6 time, 640.6 real, 4351.6 MB
[runlim] sample:		648.5 time, 650.6 real, 4355.8 MB
[runlim] sample:		658.5 time, 660.6 real, 4358.1 MB
[runlim] sample:		668.5 time, 670.6 real, 4362.6 MB
[runlim] sample:		678.5 time, 680.6 real, 4366.8 MB
[runlim] sample:		688.5 time, 690.6 real, 4369.1 MB
[runlim] sample:		698.5 time, 700.6 real, 4516.8 MB
[runlim] sample:		708.5 time, 710.6 real, 4650.9 MB
[runlim] sample:		718.5 time, 720.6 real, 4694.5 MB
[runlim] sample:		728.4 time, 730.6 real, 4775.4 MB
[runlim] sample:		738.4 time, 740.6 real, 4781.4 MB
[runlim] sample:		748.4 time, 750.6 real, 4786.4 MB
[runlim] sample:		758.4 time, 760.6 real, 4918.4 MB
[runlim] sample:		768.4 time, 770.6 real, 4918.4 MB
[runlim] sample:		778.4 time, 780.6 real, 4951.4 MB
[runlim] sample:		788.4 time, 790.6 real, 4953.4 MB
[runlim] sample:		798.4 time, 800.6 real, 4965.4 MB
[runlim] sample:		808.4 time, 810.6 real, 4965.4 MB
[runlim] sample:		818.3 time, 820.6 real, 4981.6 MB
[runlim] sample:		828.3 time, 830.6 real, 4984.1 MB
[runlim] sample:		838.3 time, 840.6 real, 4984.6 MB
[runlim] sample:		848.3 time, 850.6 real, 4986.9 MB
[runlim] sample:		858.3 time, 860.6 real, 4989.4 MB
[runlim] sample:		868.3 time, 870.6 real, 4991.6 MB
[runlim] sample:		878.3 time, 880.6 real, 4993.6 MB
[runlim] sample:		888.3 time, 890.6 real, 4994.1 MB
[runlim] sample:		898.3 time, 900.6 real, 4997.7 MB
[runlim] sample:		8.8 time, 910.6 real, 511.1 MB
[runlim] sample:		18.8 time, 920.6 real, 772.2 MB
[runlim] sample:		28.8 time, 930.6 real, 1014.1 MB
[runlim] sample:		38.8 time, 940.6 real, 1324.1 MB
[runlim] sample:		48.8 time, 950.6 real, 1455.7 MB
[runlim] sample:		58.8 time, 960.6 real, 1476.8 MB
[runlim] sample:		68.8 time, 970.6 real, 1674.0 MB
[runlim] sample:		78.8 time, 980.6 real, 1831.8 MB
[runlim] sample:		88.7 time, 990.6 real, 2068.6 MB
[runlim] sample:		98.7 time, 1000.6 real, 2261.7 MB
[runlim] sample:		108.7 time, 1010.6 real, 2399.8 MB
[runlim] sample:		118.7 time, 1020.6 real, 2449.4 MB
[runlim] sample:		128.7 time, 1030.6 real, 2513.6 MB
[runlim] sample:		138.7 time, 1040.6 real, 2534.1 MB
[runlim] sample:		148.7 time, 1050.6 real, 2641.1 MB
[runlim] sample:		158.7 time, 1060.6 real, 2786.3 MB
[runlim] sample:		168.6 time, 1070.6 real, 2831.0 MB
[runlim] sample:		178.6 time, 1080.6 real, 2989.1 MB
[runlim] sample:		188.6 time, 1090.6 real, 3096.5 MB
[runlim] sample:		198.6 time, 1100.6 real, 3162.4 MB
[runlim] sample:		208.6 time, 1110.6 real, 3270.6 MB
[runlim] sample:		218.6 time, 1120.6 real, 3380.2 MB
[runlim] sample:		228.6 time, 1130.6 real, 3436.7 MB
[runlim] sample:		238.6 time, 1140.6 real, 3483.9 MB
[runlim] sample:		248.6 time, 1150.6 real, 3545.6 MB
[runlim] sample:		258.6 time, 1160.6 real, 3592.3 MB
[runlim] sample:		268.5 time, 1170.6 real, 3807.9 MB
[runlim] sample:		278.5 time, 1180.6 real, 3953.9 MB
[runlim] sample:		288.5 time, 1190.6 real, 3995.3 MB
[runlim] sample:		298.5 time, 1200.6 real, 4017.1 MB
[runlim] sample:		308.5 time, 1210.6 real, 4065.8 MB
[runlim] sample:		318.5 time, 1220.6 real, 4175.9 MB
[runlim] sample:		328.5 time, 1230.6 real, 4287.8 MB
[runlim] sample:		338.5 time, 1240.6 real, 4372.5 MB
[runlim] sample:		348.4 time, 1250.6 real, 4395.4 MB
[runlim] sample:		358.4 time, 1260.6 real, 4466.5 MB
[runlim] sample:		368.4 time, 1270.6 real, 4467.8 MB
[runlim] sample:		378.4 time, 1280.6 real, 4480.5 MB
[runlim] sample:		388.4 time, 1290.6 real, 4545.2 MB
[runlim] sample:		398.4 time, 1300.6 real, 4545.2 MB
[runlim] sample:		408.4 time, 1310.6 real, 4675.4 MB
[runlim] sample:		418.4 time, 1320.6 real, 4751.3 MB
[runlim] sample:		428.4 time, 1330.6 real, 4851.5 MB
[runlim] sample:		438.3 time, 1340.6 real, 4851.5 MB
[runlim] sample:		448.3 time, 1350.6 real, 4879.5 MB
[runlim] sample:		458.3 time, 1360.6 real, 4891.0 MB
[runlim] sample:		468.3 time, 1370.6 real, 4931.9 MB
[runlim] sample:		478.3 time, 1380.6 real, 4957.2 MB
[runlim] sample:		488.3 time, 1390.6 real, 4962.2 MB
[runlim] sample:		498.3 time, 1400.6 real, 4963.2 MB
[runlim] sample:		508.3 time, 1410.6 real, 4965.2 MB
[runlim] sample:		518.2 time, 1420.6 real, 4966.2 MB
[runlim] sample:		528.2 time, 1430.6 real, 4993.5 MB
[runlim] sample:		538.2 time, 1440.6 real, 5031.2 MB
[runlim] sample:		548.2 time, 1450.6 real, 5033.5 MB
[runlim] sample:		558.2 time, 1460.6 real, 5035.0 MB
[runlim] sample:		568.2 time, 1470.6 real, 5035.0 MB
[runlim] sample:		578.2 time, 1480.6 real, 5035.0 MB
[runlim] sample:		588.2 time, 1490.6 real, 5092.2 MB
[runlim] sample:		598.2 time, 1500.6 real, 5094.2 MB
[runlim] sample:		608.1 time, 1510.6 real, 5094.2 MB
[runlim] sample:		618.1 time, 1520.6 real, 5094.4 MB
[runlim] sample:		628.1 time, 1530.6 real, 5095.3 MB
[runlim] sample:		638.1 time, 1540.6 real, 5191.5 MB
[runlim] sample:		648.1 time, 1550.6 real, 5215.0 MB
[runlim] sample:		658.1 time, 1560.6 real, 5250.3 MB
[runlim] sample:		668.1 time, 1570.6 real, 5252.5 MB
[runlim] sample:		678.1 time, 1580.6 real, 5253.0 MB
[runlim] sample:		688.1 time, 1590.6 real, 5255.3 MB
[runlim] sample:		698.1 time, 1600.6 real, 5302.0 MB
[runlim] sample:		708.0 time, 1610.6 real, 5330.3 MB
[runlim] sample:		718.0 time, 1620.6 real, 5317.5 MB
[runlim] sample:		728.0 time, 1630.6 real, 5317.5 MB
[runlim] sample:		738.0 time, 1640.6 real, 5319.5 MB
[runlim] sample:		748.0 time, 1650.6 real, 5319.7 MB
[runlim] sample:		758.0 time, 1660.6 real, 5319.7 MB
[runlim] sample:		768.0 time, 1670.6 real, 5336.2 MB
[runlim] sample:		778.0 time, 1680.6 real, 5337.2 MB
[runlim] sample:		788.0 time, 1690.6 real, 5338.2 MB
[runlim] sample:		797.9 time, 1700.6 real, 5338.7 MB
[runlim] sample:		807.9 time, 1710.6 real, 5341.2 MB
[runlim] sample:		817.9 time, 1720.6 real, 5341.2 MB
[runlim] sample:		827.9 time, 1730.6 real, 5343.2 MB
[runlim] sample:		837.9 time, 1740.6 real, 5343.4 MB
[runlim] sample:		847.9 time, 1750.6 real, 5343.4 MB
[runlim] sample:		857.9 time, 1760.6 real, 5345.7 MB
[runlim] sample:		867.9 time, 1770.6 real, 5437.4 MB
[runlim] sample:		877.9 time, 1780.6 real, 5516.8 MB
[runlim] sample:		887.8 time, 1790.6 real, 5597.4 MB
[runlim] sample:		897.8 time, 1800.6 real, 5597.4 MB
[runlim] sample:		8.3 time, 1810.6 real, 521.9 MB
[runlim] sample:		18.4 time, 1820.6 real, 781.1 MB
[runlim] sample:		28.3 time, 1830.6 real, 1011.0 MB
[runlim] sample:		38.3 time, 1840.6 real, 1300.7 MB
[runlim] sample:		48.3 time, 1850.6 real, 1474.0 MB
[runlim] sample:		58.3 time, 1860.6 real, 1734.6 MB
[runlim] sample:		68.3 time, 1870.6 real, 1866.0 MB
[runlim] sample:		78.3 time, 1880.6 real, 2169.2 MB
[runlim] sample:		88.3 time, 1890.6 real, 2236.2 MB
[runlim] sample:		98.3 time, 1900.6 real, 2372.2 MB
[runlim] sample:		108.2 time, 1910.6 real, 2476.4 MB
[runlim] sample:		118.2 time, 1920.6 real, 2714.4 MB
[runlim] sample:		128.2 time, 1930.6 real, 2966.5 MB
[runlim] sample:		138.2 time, 1940.6 real, 3076.4 MB
[runlim] sample:		148.2 time, 1950.6 real, 3182.7 MB
[runlim] sample:		158.2 time, 1960.6 real, 3540.3 MB
[runlim] sample:		168.2 time, 1970.6 real, 3546.8 MB
[runlim] sample:		178.2 time, 1980.6 real, 3546.8 MB
[runlim] sample:		188.1 time, 1990.6 real, 3546.8 MB
[runlim] sample:		198.1 time, 2000.6 real, 3813.1 MB
[runlim] sample:		208.1 time, 2010.6 real, 3970.8 MB
[runlim] sample:		218.1 time, 2020.6 real, 4240.3 MB
[runlim] sample:		228.1 time, 2030.6 real, 4335.4 MB
[runlim] sample:		238.1 time, 2040.6 real, 4491.8 MB
[runlim] sample:		248.1 time, 2050.6 real, 4625.7 MB
[runlim] sample:		258.1 time, 2060.6 real, 4747.5 MB
[runlim] sample:		268.1 time, 2070.6 real, 4753.9 MB
[runlim] sample:		278.1 time, 2080.6 real, 4754.1 MB
[runlim] sample:		288.0 time, 2090.6 real, 4754.1 MB
[runlim] sample:		298.0 time, 2100.6 real, 4754.1 MB
[runlim] sample:		308.0 time, 2110.6 real, 4754.1 MB
[runlim] sample:		318.0 time, 2120.6 real, 4758.4 MB
[runlim] sample:		328.0 time, 2130.6 real, 4768.2 MB
[runlim] sample:		338.0 time, 2140.6 real, 4797.9 MB
[runlim] sample:		347.9 time, 2150.6 real, 5108.7 MB
[runlim] sample:		357.9 time, 2160.6 real, 5193.4 MB
[runlim] sample:		367.9 time, 2170.6 real, 5409.2 MB
[runlim] sample:		377.9 time, 2180.6 real, 5644.7 MB
[runlim] sample:		387.9 time, 2190.6 real, 6015.4 MB
[runlim] sample:		397.9 time, 2200.6 real, 6142.8 MB
[runlim] sample:		407.9 time, 2210.6 real, 6249.1 MB
[runlim] sample:		417.9 time, 2220.6 real, 6495.6 MB
[runlim] sample:		427.9 time, 2230.6 real, 6642.3 MB
[runlim] sample:		437.8 time, 2240.6 real, 6642.3 MB
[runlim] sample:		447.8 time, 2250.6 real, 6642.5 MB
[runlim] sample:		457.8 time, 2260.6 real, 6643.2 MB
[runlim] sample:		467.8 time, 2270.6 real, 6644.2 MB
[runlim] sample:		477.8 time, 2280.6 real, 6644.9 MB
[runlim] sample:		487.8 time, 2290.6 real, 6645.6 MB
[runlim] sample:		497.8 time, 2300.6 real, 6646.6 MB
[runlim] sample:		507.8 time, 2310.6 real, 6647.3 MB
[runlim] sample:		517.8 time, 2320.6 real, 6649.3 MB
[runlim] sample:		527.8 time, 2330.6 real, 6651.0 MB
[runlim] sample:		537.7 time, 2340.6 real, 6651.5 MB
[runlim] sample:		547.7 time, 2350.6 real, 6653.2 MB
[runlim] sample:		0.5 time, 2360.6 real, 62.3 MB
[runlim] sample:		10.4 time, 2370.6 real, 614.8 MB
[runlim] sample:		20.4 time, 2380.6 real, 921.1 MB
[runlim] sample:		30.4 time, 2390.6 real, 1303.5 MB
[runlim] sample:		40.4 time, 2400.6 real, 1575.4 MB
[runlim] sample:		50.4 time, 2410.6 real, 1736.7 MB
[runlim] sample:		60.4 time, 2420.6 real, 1805.5 MB
[runlim] sample:		70.4 time, 2430.6 real, 1980.5 MB
[runlim] sample:		80.3 time, 2440.6 real, 1981.0 MB
[runlim] sample:		90.3 time, 2450.6 real, 2069.0 MB
[runlim] sample:		100.3 time, 2460.6 real, 2143.4 MB
[runlim] sample:		110.3 time, 2470.6 real, 2190.2 MB
[runlim] sample:		120.3 time, 2480.6 real, 2345.0 MB
[runlim] sample:		130.3 time, 2490.6 real, 2431.3 MB
[runlim] sample:		140.3 time, 2500.6 real, 2455.3 MB
[runlim] sample:		150.3 time, 2510.6 real, 2455.5 MB
[runlim] sample:		160.3 time, 2520.6 real, 2455.7 MB
[runlim] sample:		170.3 time, 2530.6 real, 2456.0 MB
[runlim] sample:		180.2 time, 2540.6 real, 2685.9 MB
[runlim] sample:		190.2 time, 2550.6 real, 2716.4 MB
[runlim] sample:		200.2 time, 2560.6 real, 2789.1 MB
[runlim] sample:		210.2 time, 2570.6 real, 2789.6 MB
[runlim] sample:		220.2 time, 2580.6 real, 2791.9 MB
[runlim] sample:		230.2 time, 2590.6 real, 2792.1 MB
[runlim] sample:		240.2 time, 2600.6 real, 2792.1 MB
[runlim] sample:		250.2 time, 2610.6 real, 2792.6 MB
[runlim] sample:		260.1 time, 2620.6 real, 2792.9 MB
[runlim] sample:		270.1 time, 2630.6 real, 2792.9 MB
[runlim] sample:		280.1 time, 2640.6 real, 2793.4 MB
[runlim] sample:		290.1 time, 2650.6 real, 2795.7 MB
[runlim] sample:		300.1 time, 2660.6 real, 2974.9 MB
[runlim] sample:		310.1 time, 2670.6 real, 3033.2 MB
[runlim] sample:		320.1 time, 2680.6 real, 3074.1 MB
[runlim] sample:		330.1 time, 2690.6 real, 3074.9 MB
[runlim] sample:		340.1 time, 2700.6 real, 3075.2 MB
[runlim] sample:		350.1 time, 2710.6 real, 3077.9 MB
[runlim] sample:		360.0 time, 2720.6 real, 3078.2 MB
[runlim] sample:		370.0 time, 2730.6 real, 3078.7 MB
[runlim] sample:		380.0 time, 2740.6 real, 3078.9 MB
[runlim] sample:		390.0 time, 2750.6 real, 3079.2 MB
[runlim] sample:		400.0 time, 2760.6 real, 3079.2 MB
[runlim] sample:		410.0 time, 2770.6 real, 3081.2 MB
[runlim] sample:		420.0 time, 2780.6 real, 3082.0 MB
[runlim] sample:		430.0 time, 2790.6 real, 3124.4 MB
[runlim] sample:		440.0 time, 2800.6 real, 3283.0 MB
[runlim] sample:		449.9 time, 2810.6 real, 3381.7 MB
[runlim] sample:		459.9 time, 2820.6 real, 3382.5 MB
[runlim] sample:		469.9 time, 2830.6 real, 3384.5 MB
[runlim] sample:		479.9 time, 2840.6 real, 3384.7 MB
[runlim] sample:		489.9 time, 2850.6 real, 3385.0 MB
[runlim] sample:		499.9 time, 2860.6 real, 3385.0 MB
[runlim] sample:		509.9 time, 2870.6 real, 3385.3 MB
[runlim] sample:		519.9 time, 2880.6 real, 3385.5 MB
[runlim] sample:		529.9 time, 2890.6 real, 3385.8 MB
[runlim] sample:		539.8 time, 2900.6 real, 3386.0 MB
[runlim] sample:		549.8 time, 2910.6 real, 3412.5 MB
[runlim] sample:		559.8 time, 2920.6 real, 3585.2 MB
[runlim] sample:		569.8 time, 2930.6 real, 3589.0 MB
[runlim] sample:		579.8 time, 2940.6 real, 3589.0 MB
[runlim] sample:		589.8 time, 2950.6 real, 3687.4 MB
[runlim] sample:		599.8 time, 2960.6 real, 3687.4 MB
[runlim] sample:		609.8 time, 2970.6 real, 3689.4 MB
[runlim] sample:		619.8 time, 2980.6 real, 3689.4 MB
[runlim] sample:		629.8 time, 2990.6 real, 3689.4 MB
[runlim] sample:		639.8 time, 3000.6 real, 3689.4 MB
[runlim] sample:		649.7 time, 3010.6 real, 3713.6 MB
[runlim] sample:		659.7 time, 3020.6 real, 3716.4 MB
[runlim] sample:		669.7 time, 3030.6 real, 3719.4 MB
[runlim] sample:		679.7 time, 3040.6 real, 3913.2 MB
[runlim] sample:		689.7 time, 3050.6 real, 3913.2 MB
[runlim] sample:		699.7 time, 3060.6 real, 3913.2 MB
[runlim] sample:		709.7 time, 3070.6 real, 3956.8 MB
[runlim] sample:		719.7 time, 3080.6 real, 4012.8 MB
[runlim] sample:		729.6 time, 3090.6 real, 4012.8 MB
[runlim] sample:		739.6 time, 3100.6 real, 4012.8 MB
[runlim] sample:		749.6 time, 3110.6 real, 4012.9 MB
[runlim] sample:		759.6 time, 3120.6 real, 4015.5 MB
[runlim] sample:		769.6 time, 3130.6 real, 4015.8 MB
[runlim] sample:		779.6 time, 3140.6 real, 4017.8 MB
[runlim] sample:		789.6 time, 3150.6 real, 4017.8 MB
[runlim] sample:		799.6 time, 3160.6 real, 4017.8 MB
[runlim] sample:		809.6 time, 3170.6 real, 4017.8 MB
[runlim] sample:		819.5 time, 3180.6 real, 4017.8 MB
[runlim] sample:		829.6 time, 3190.6 real, 4019.8 MB
[runlim] sample:		839.5 time, 3200.6 real, 4019.8 MB
[runlim] sample:		849.5 time, 3210.6 real, 4019.8 MB
[runlim] sample:		859.5 time, 3220.6 real, 4019.8 MB
[runlim] sample:		869.5 time, 3230.6 real, 4019.8 MB
[runlim] sample:		0.0 time, 3240.6 real, 32.3 MB
[runlim] sample:		10.0 time, 3250.6 real, 550.9 MB
[runlim] sample:		20.0 time, 3260.6 real, 813.7 MB
[runlim] sample:		30.0 time, 3270.6 real, 1039.2 MB
[runlim] sample:		40.0 time, 3280.6 real, 1360.8 MB
[runlim] sample:		50.0 time, 3290.6 real, 1608.9 MB
[runlim] sample:		59.9 time, 3300.6 real, 1928.5 MB
[runlim] sample:		69.9 time, 3310.6 real, 2036.0 MB
[runlim] sample:		79.9 time, 3320.6 real, 2322.6 MB
[runlim] sample:		89.9 time, 3330.6 real, 2425.3 MB
[runlim] sample:		99.9 time, 3340.6 real, 2607.7 MB
[runlim] sample:		109.9 time, 3350.6 real, 2735.9 MB
[runlim] sample:		119.9 time, 3360.6 real, 2808.1 MB
[runlim] sample:		129.8 time, 3370.6 real, 3021.1 MB
[runlim] sample:		139.8 time, 3380.6 real, 3275.1 MB
[runlim] sample:		149.8 time, 3390.6 real, 3527.2 MB
[runlim] sample:		159.8 time, 3400.6 real, 3537.2 MB
[runlim] sample:		169.8 time, 3410.6 real, 3541.5 MB
[runlim] sample:		179.8 time, 3420.6 real, 3660.8 MB
[runlim] sample:		189.8 time, 3430.6 real, 3744.1 MB
[runlim] sample:		199.8 time, 3440.6 real, 4066.9 MB
[runlim] sample:		209.8 time, 3450.6 real, 4118.0 MB
[runlim] sample:		219.7 time, 3460.6 real, 4118.0 MB
[runlim] sample:		229.7 time, 3470.6 real, 4118.3 MB
[runlim] sample:		239.7 time, 3480.6 real, 4145.5 MB
[runlim] sample:		249.7 time, 3490.6 real, 4305.8 MB
[runlim] sample:		259.7 time, 3500.6 real, 4324.5 MB
[runlim] sample:		269.7 time, 3510.6 real, 4500.7 MB
[runlim] sample:		279.7 time, 3520.6 real, 4822.6 MB
[runlim] sample:		289.7 time, 3530.6 real, 4863.1 MB
[runlim] sample:		299.7 time, 3540.6 real, 4955.8 MB
[runlim] sample:		309.6 time, 3550.6 real, 5322.6 MB
[runlim] sample:		319.6 time, 3560.6 real, 5517.4 MB
[runlim] sample:		329.6 time, 3570.6 real, 5897.4 MB
[runlim] sample:		339.6 time, 3580.6 real, 6223.2 MB
[runlim] sample:		349.6 time, 3590.6 real, 6404.4 MB
[runlim] end:			Mon Sep 28 15:24:34 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		215931
[runlim] real:			3600.19 seconds
[runlim] time:			898.92 seconds
[runlim] space:			6654.8 MB
[runlim] samples:		35996
