[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/abc/single.abcsuprove
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/hwmcc14/single/6s387rb181.aig
[runlim] start:			Wed Sep 16 09:58:06 2015
[runlim] main pid:		30463
[runlim] sample:		9.5 time, 10.2 real, 153.0 MB
[runlim] sample:		41.3 time, 20.2 real, 2897.6 MB
[runlim] sample:		80.9 time, 30.2 real, 3371.0 MB
[runlim] sample:		115.7 time, 40.2 real, 3248.2 MB
[runlim] sample:		144.9 time, 50.2 real, 2998.3 MB
[runlim] sample:		184.5 time, 60.2 real, 3122.4 MB
[runlim] sample:		190.7 time, 70.2 real, 2650.7 MB
[runlim] sample:		230.2 time, 80.2 real, 3444.8 MB
[runlim] sample:		268.8 time, 90.2 real, 4154.3 MB
[runlim] sample:		308.3 time, 100.2 real, 4104.5 MB
[runlim] sample:		347.9 time, 110.2 real, 4303.5 MB
[runlim] sample:		387.3 time, 120.2 real, 4346.2 MB
[runlim] sample:		408.2 time, 130.2 real, 3836.4 MB
[runlim] sample:		446.8 time, 140.2 real, 3984.0 MB
[runlim] sample:		486.3 time, 150.2 real, 3987.6 MB
[runlim] sample:		525.9 time, 160.2 real, 4007.8 MB
[runlim] sample:		565.4 time, 170.2 real, 3965.7 MB
[runlim] sample:		604.0 time, 180.2 real, 4546.8 MB
[runlim] sample:		643.5 time, 190.2 real, 4669.2 MB
[runlim] sample:		683.0 time, 200.2 real, 4669.5 MB
[runlim] sample:		701.9 time, 210.2 real, 4067.6 MB
[runlim] sample:		741.5 time, 220.2 real, 4112.8 MB
[runlim] sample:		780.1 time, 230.2 real, 4175.7 MB
[runlim] sample:		14.0 time, 240.2 real, 146.3 MB
[runlim] sample:		39.9 time, 250.2 real, 1509.4 MB
[runlim] sample:		79.3 time, 260.2 real, 3304.9 MB
[runlim] sample:		118.9 time, 270.2 real, 3665.0 MB
[runlim] sample:		158.5 time, 280.2 real, 3701.0 MB
[runlim] sample:		198.0 time, 290.2 real, 3728.9 MB
[runlim] sample:		237.5 time, 300.2 real, 3729.2 MB
[runlim] sample:		277.1 time, 310.2 real, 3668.3 MB
[runlim] sample:		316.6 time, 320.2 real, 3878.3 MB
[runlim] sample:		356.2 time, 330.2 real, 3667.8 MB
[runlim] sample:		395.7 time, 340.2 real, 3929.6 MB
[runlim] sample:		435.2 time, 350.2 real, 3823.3 MB
[runlim] sample:		474.8 time, 360.2 real, 4008.8 MB
[runlim] sample:		514.3 time, 370.2 real, 4067.2 MB
[runlim] sample:		553.8 time, 380.2 real, 3936.5 MB
[runlim] sample:		593.4 time, 390.2 real, 4146.3 MB
[runlim] sample:		632.9 time, 400.2 real, 4154.2 MB
[runlim] sample:		672.5 time, 410.2 real, 4150.9 MB
[runlim] sample:		712.0 time, 420.2 real, 4208.7 MB
[runlim] sample:		751.5 time, 430.2 real, 4282.4 MB
[runlim] sample:		791.1 time, 440.2 real, 4029.4 MB
[runlim] sample:		830.6 time, 450.2 real, 4359.9 MB
[runlim] sample:		870.2 time, 460.2 real, 4460.3 MB
[runlim] sample:		909.7 time, 470.2 real, 4471.0 MB
[runlim] sample:		949.2 time, 480.2 real, 4436.4 MB
[runlim] sample:		988.8 time, 490.2 real, 4460.0 MB
[runlim] sample:		1028.3 time, 500.2 real, 4508.9 MB
[runlim] sample:		1067.9 time, 510.2 real, 4324.8 MB
[runlim] sample:		1107.4 time, 520.2 real, 4580.6 MB
[runlim] sample:		1146.9 time, 530.2 real, 4582.4 MB
[runlim] sample:		1186.4 time, 540.2 real, 4589.2 MB
[runlim] sample:		1226.0 time, 550.2 real, 4625.0 MB
[runlim] sample:		25.4 time, 560.2 real, 1667.2 MB
[runlim] sample:		65.0 time, 570.2 real, 2584.9 MB
[runlim] sample:		104.5 time, 580.2 real, 2668.3 MB
[runlim] sample:		144.1 time, 590.2 real, 2601.5 MB
[runlim] sample:		183.7 time, 600.2 real, 2613.7 MB
[runlim] sample:		223.2 time, 610.2 real, 2787.1 MB
[runlim] sample:		262.8 time, 620.2 real, 2841.6 MB
[runlim] sample:		302.4 time, 630.2 real, 2726.4 MB
[runlim] sample:		341.9 time, 640.2 real, 2925.4 MB
[runlim] sample:		381.5 time, 650.2 real, 2801.0 MB
[runlim] sample:		421.1 time, 660.2 real, 3006.5 MB
[runlim] sample:		460.6 time, 670.2 real, 3015.7 MB
[runlim] sample:		500.1 time, 680.2 real, 3017.9 MB
[runlim] sample:		539.7 time, 690.2 real, 3086.4 MB
[runlim] sample:		579.2 time, 700.2 real, 3023.5 MB
[runlim] sample:		618.8 time, 710.2 real, 3200.9 MB
[runlim] sample:		658.3 time, 720.2 real, 3205.3 MB
[runlim] sample:		697.8 time, 730.2 real, 3209.7 MB
[runlim] sample:		737.4 time, 740.2 real, 3213.2 MB
[runlim] sample:		776.9 time, 750.2 real, 3035.7 MB
[runlim] sample:		816.5 time, 760.2 real, 3140.8 MB
[runlim] sample:		856.1 time, 770.2 real, 3162.9 MB
[runlim] sample:		895.6 time, 780.2 real, 3194.7 MB
[runlim] sample:		935.2 time, 790.2 real, 3199.7 MB
[runlim] sample:		974.7 time, 800.2 real, 3194.0 MB
[runlim] sample:		1014.3 time, 810.2 real, 3213.5 MB
[runlim] sample:		1053.8 time, 820.2 real, 3216.3 MB
[runlim] sample:		1093.4 time, 830.2 real, 3219.4 MB
[runlim] sample:		1133.0 time, 840.2 real, 3346.7 MB
[runlim] sample:		1172.6 time, 850.2 real, 3347.8 MB
[runlim] sample:		1212.1 time, 860.2 real, 3383.1 MB
[runlim] sample:		1251.6 time, 870.2 real, 3379.6 MB
[runlim] sample:		1291.2 time, 880.2 real, 3412.7 MB
[runlim] sample:		1330.8 time, 890.2 real, 3421.0 MB
[runlim] sample:		1370.3 time, 900.2 real, 3425.8 MB
[runlim] sample:		1409.9 time, 910.2 real, 3428.0 MB
[runlim] sample:		1449.4 time, 920.2 real, 3381.2 MB
[runlim] sample:		1489.0 time, 930.2 real, 3385.3 MB
[runlim] sample:		1528.6 time, 940.2 real, 3382.2 MB
[runlim] sample:		1568.2 time, 950.2 real, 3383.5 MB
[runlim] sample:		1607.7 time, 960.2 real, 3384.0 MB
[runlim] sample:		1647.3 time, 970.2 real, 3388.4 MB
[runlim] sample:		1686.8 time, 980.2 real, 3389.4 MB
[runlim] sample:		1726.3 time, 990.2 real, 3451.6 MB
[runlim] sample:		1765.9 time, 1000.2 real, 3456.7 MB
[runlim] sample:		1805.5 time, 1010.2 real, 3466.0 MB
[runlim] sample:		1845.1 time, 1020.2 real, 3471.9 MB
[runlim] sample:		1884.6 time, 1030.2 real, 3435.9 MB
[runlim] sample:		1924.2 time, 1040.2 real, 3435.4 MB
[runlim] sample:		1963.7 time, 1050.2 real, 3435.6 MB
[runlim] sample:		2003.3 time, 1060.2 real, 3436.7 MB
[runlim] sample:		2042.8 time, 1070.2 real, 3438.2 MB
[runlim] sample:		2082.4 time, 1080.2 real, 3475.3 MB
[runlim] sample:		2122.0 time, 1090.2 real, 3477.1 MB
[runlim] sample:		2161.5 time, 1100.2 real, 3515.8 MB
[runlim] sample:		2201.1 time, 1110.2 real, 3631.9 MB
[runlim] sample:		2240.6 time, 1120.2 real, 3635.9 MB
[runlim] sample:		2053.1 time, 1130.2 real, 3390.3 MB
[runlim] sample:		27.2 time, 1140.2 real, 126.3 MB
[runlim] sample:		31.0 time, 1150.2 real, 126.4 MB
[runlim] sample:		36.9 time, 1160.2 real, 126.4 MB
[runlim] sample:		40.7 time, 1170.2 real, 126.4 MB
[runlim] sample:		44.6 time, 1180.2 real, 126.4 MB
[runlim] sample:		47.9 time, 1190.2 real, 126.4 MB
[runlim] sample:		52.0 time, 1200.2 real, 126.4 MB
[runlim] sample:		78.9 time, 1210.2 real, 1287.1 MB
[runlim] sample:		79.2 time, 1220.2 real, 1270.6 MB
[runlim] sample:		84.4 time, 1230.2 real, 1265.5 MB
[runlim] sample:		87.5 time, 1240.2 real, 1458.4 MB
[runlim] sample:		87.9 time, 1250.2 real, 1459.2 MB
[runlim] sample:		88.2 time, 1260.2 real, 1294.3 MB
[runlim] sample:		82.7 time, 1270.2 real, 126.4 MB
[runlim] sample:		84.9 time, 1280.2 real, 126.5 MB
[runlim] sample:		88.9 time, 1290.2 real, 126.5 MB
[runlim] sample:		117.6 time, 1300.2 real, 1282.8 MB
[runlim] sample:		111.0 time, 1310.2 real, 1458.1 MB
[runlim] sample:		114.8 time, 1320.2 real, 1452.4 MB
[runlim] sample:		108.0 time, 1330.2 real, 1124.8 MB
[runlim] sample:		110.1 time, 1340.2 real, 145.9 MB
[runlim] sample:		141.3 time, 1350.2 real, 2244.8 MB
[runlim] sample:		180.9 time, 1360.2 real, 2216.2 MB
[runlim] sample:		220.5 time, 1370.2 real, 2326.1 MB
[runlim] sample:		260.0 time, 1380.2 real, 2373.8 MB
[runlim] sample:		299.6 time, 1390.2 real, 2429.5 MB
[runlim] sample:		339.1 time, 1400.2 real, 2339.6 MB
[runlim] sample:		378.7 time, 1410.2 real, 2296.2 MB
[runlim] sample:		418.2 time, 1420.2 real, 2571.0 MB
[runlim] sample:		457.8 time, 1430.2 real, 2327.9 MB
[runlim] sample:		497.4 time, 1440.2 real, 2653.9 MB
[runlim] sample:		537.0 time, 1450.2 real, 2660.2 MB
[runlim] sample:		576.5 time, 1460.2 real, 2716.8 MB
[runlim] sample:		616.1 time, 1470.2 real, 2734.5 MB
[runlim] sample:		655.6 time, 1480.2 real, 2851.6 MB
[runlim] sample:		695.1 time, 1490.2 real, 2869.4 MB
[runlim] sample:		734.7 time, 1500.2 real, 2872.7 MB
[runlim] sample:		774.2 time, 1510.2 real, 2877.7 MB
[runlim] sample:		813.7 time, 1520.2 real, 2703.9 MB
[runlim] sample:		853.3 time, 1530.2 real, 2934.9 MB
[runlim] sample:		892.8 time, 1540.2 real, 2965.2 MB
[runlim] sample:		932.4 time, 1550.2 real, 2965.7 MB
[runlim] sample:		971.9 time, 1560.2 real, 2967.0 MB
[runlim] sample:		1011.5 time, 1570.2 real, 3014.7 MB
[runlim] sample:		1051.0 time, 1580.2 real, 3015.2 MB
[runlim] sample:		1090.6 time, 1590.2 real, 3047.3 MB
[runlim] sample:		1130.2 time, 1600.2 real, 3180.4 MB
[runlim] sample:		1169.7 time, 1610.2 real, 3187.2 MB
[runlim] sample:		1209.3 time, 1620.2 real, 3190.8 MB
[runlim] sample:		1248.9 time, 1630.2 real, 3195.3 MB
[runlim] sample:		1288.4 time, 1640.2 real, 3173.5 MB
[runlim] sample:		1328.0 time, 1650.2 real, 3178.4 MB
[runlim] sample:		1367.6 time, 1660.2 real, 3179.9 MB
[runlim] sample:		1407.1 time, 1670.2 real, 3181.7 MB
[runlim] sample:		1446.7 time, 1680.2 real, 3182.5 MB
[runlim] sample:		1486.2 time, 1690.2 real, 3183.5 MB
[runlim] sample:		1525.8 time, 1700.2 real, 3217.1 MB
[runlim] sample:		1565.3 time, 1710.2 real, 3220.1 MB
[runlim] sample:		1604.9 time, 1720.2 real, 3223.6 MB
[runlim] sample:		1644.5 time, 1730.2 real, 3226.2 MB
[runlim] sample:		1684.0 time, 1740.2 real, 3220.5 MB
[runlim] sample:		1723.5 time, 1750.2 real, 3223.9 MB
[runlim] sample:		1763.1 time, 1760.2 real, 3230.0 MB
[runlim] sample:		1802.7 time, 1770.2 real, 3231.8 MB
[runlim] sample:		1842.2 time, 1780.2 real, 3236.3 MB
[runlim] sample:		1881.8 time, 1790.2 real, 3237.9 MB
[runlim] sample:		1921.3 time, 1800.2 real, 3272.9 MB
[runlim] sample:		1960.9 time, 1810.2 real, 3275.4 MB
[runlim] sample:		2000.4 time, 1820.2 real, 3278.2 MB
[runlim] sample:		2040.0 time, 1830.2 real, 3317.2 MB
[runlim] sample:		2079.6 time, 1840.2 real, 3322.4 MB
[runlim] sample:		2119.1 time, 1850.2 real, 3281.5 MB
[runlim] sample:		2158.7 time, 1860.2 real, 3282.8 MB
[runlim] sample:		2198.2 time, 1870.2 real, 3285.1 MB
[runlim] sample:		2237.8 time, 1880.2 real, 3285.6 MB
[runlim] sample:		2277.3 time, 1890.2 real, 3289.8 MB
[runlim] sample:		2316.9 time, 1900.2 real, 3290.5 MB
[runlim] sample:		2356.4 time, 1910.2 real, 3330.1 MB
[runlim] sample:		2396.0 time, 1920.2 real, 3371.2 MB
[runlim] sample:		2435.5 time, 1930.2 real, 3376.5 MB
[runlim] sample:		2475.1 time, 1940.2 real, 3383.0 MB
[runlim] sample:		2514.6 time, 1950.2 real, 3416.9 MB
[runlim] sample:		2554.1 time, 1960.2 real, 3374.8 MB
[runlim] sample:		2593.7 time, 1970.2 real, 3375.3 MB
[runlim] sample:		2633.2 time, 1980.2 real, 3384.3 MB
[runlim] sample:		2672.8 time, 1990.2 real, 3388.8 MB
[runlim] sample:		2712.3 time, 2000.2 real, 3394.9 MB
[runlim] sample:		2751.9 time, 2010.2 real, 3399.0 MB
[runlim] sample:		2791.5 time, 2020.2 real, 3436.3 MB
[runlim] sample:		2831.0 time, 2030.2 real, 3442.9 MB
[runlim] sample:		2870.5 time, 2040.2 real, 3449.3 MB
[runlim] sample:		2910.0 time, 2050.2 real, 3453.6 MB
[runlim] sample:		2949.6 time, 2060.2 real, 3459.8 MB
[runlim] sample:		2989.1 time, 2070.2 real, 3510.3 MB
[runlim] sample:		3028.6 time, 2080.2 real, 3514.6 MB
[runlim] sample:		3068.2 time, 2090.2 real, 3517.6 MB
[runlim] sample:		3107.7 time, 2100.2 real, 3471.1 MB
[runlim] sample:		3147.2 time, 2110.2 real, 3472.4 MB
[runlim] sample:		3186.8 time, 2120.2 real, 3474.8 MB
[runlim] sample:		3226.3 time, 2130.2 real, 3476.3 MB
[runlim] sample:		3265.8 time, 2140.2 real, 3476.3 MB
[runlim] sample:		3305.4 time, 2150.2 real, 3476.8 MB
[runlim] sample:		3344.9 time, 2160.2 real, 3510.0 MB
[runlim] sample:		3384.5 time, 2170.2 real, 3543.6 MB
[runlim] sample:		3424.0 time, 2180.2 real, 3548.9 MB
[runlim] sample:		3463.6 time, 2190.2 real, 3552.4 MB
[runlim] sample:		3503.1 time, 2200.2 real, 3557.8 MB
[runlim] sample:		3542.7 time, 2210.2 real, 3560.2 MB
[runlim] sample:		3582.2 time, 2220.2 real, 3563.2 MB
[runlim] sample:		3621.8 time, 2230.2 real, 3564.5 MB
[runlim] sample:		3661.3 time, 2240.2 real, 3568.1 MB
[runlim] sample:		3700.9 time, 2250.2 real, 3522.3 MB
[runlim] sample:		3740.4 time, 2260.2 real, 3557.8 MB
[runlim] sample:		3779.9 time, 2270.2 real, 3558.8 MB
[runlim] sample:		3819.5 time, 2280.2 real, 3559.8 MB
[runlim] sample:		3859.0 time, 2290.2 real, 3561.9 MB
[runlim] sample:		3898.6 time, 2300.2 real, 3562.2 MB
[runlim] sample:		3938.1 time, 2310.2 real, 3596.4 MB
[runlim] sample:		3977.7 time, 2320.2 real, 3599.7 MB
[runlim] sample:		4017.2 time, 2330.2 real, 3604.3 MB
[runlim] sample:		4056.7 time, 2340.2 real, 3607.1 MB
[runlim] sample:		4096.3 time, 2350.2 real, 3783.4 MB
[runlim] sample:		4135.9 time, 2360.2 real, 3786.4 MB
[runlim] sample:		4175.5 time, 2370.2 real, 3790.3 MB
[runlim] sample:		4215.0 time, 2380.2 real, 3792.7 MB
[runlim] sample:		4254.5 time, 2390.2 real, 3796.5 MB
[runlim] sample:		4294.1 time, 2400.2 real, 3799.3 MB
[runlim] sample:		4333.6 time, 2410.2 real, 3752.3 MB
[runlim] sample:		4373.1 time, 2420.2 real, 3753.1 MB
[runlim] sample:		4412.7 time, 2430.2 real, 3755.4 MB
[runlim] sample:		4452.2 time, 2440.2 real, 3756.7 MB
[runlim] sample:		4491.8 time, 2450.2 real, 3776.0 MB
[runlim] sample:		4531.3 time, 2460.2 real, 3776.7 MB
[runlim] sample:		4570.9 time, 2470.2 real, 3777.3 MB
[runlim] sample:		4610.4 time, 2480.2 real, 3778.8 MB
[runlim] sample:		4650.0 time, 2490.2 real, 3812.6 MB
[runlim] sample:		4689.6 time, 2500.2 real, 3816.9 MB
[runlim] sample:		4729.1 time, 2510.2 real, 3819.7 MB
[runlim] sample:		4768.7 time, 2520.2 real, 3823.2 MB
[runlim] sample:		4808.2 time, 2530.2 real, 3827.1 MB
[runlim] sample:		4847.8 time, 2540.2 real, 3831.8 MB
[runlim] sample:		4887.3 time, 2550.2 real, 3836.1 MB
[runlim] sample:		4926.9 time, 2560.2 real, 3839.7 MB
[runlim] sample:		4966.4 time, 2570.2 real, 3844.6 MB
[runlim] sample:		5006.0 time, 2580.2 real, 3793.8 MB
[runlim] sample:		5045.5 time, 2590.2 real, 3794.5 MB
[runlim] sample:		5085.1 time, 2600.2 real, 3797.1 MB
[runlim] sample:		5124.6 time, 2610.2 real, 3798.4 MB
[runlim] sample:		5164.2 time, 2620.2 real, 3833.0 MB
[runlim] sample:		5203.8 time, 2630.2 real, 3833.5 MB
[runlim] sample:		5243.3 time, 2640.2 real, 3837.4 MB
[runlim] sample:		5282.9 time, 2650.2 real, 3874.6 MB
[runlim] sample:		5322.4 time, 2660.2 real, 3879.7 MB
[runlim] sample:		5362.0 time, 2670.2 real, 3886.8 MB
[runlim] sample:		5401.5 time, 2680.2 real, 3893.9 MB
[runlim] sample:		5441.1 time, 2690.2 real, 3901.3 MB
[runlim] sample:		5480.6 time, 2700.2 real, 3910.2 MB
[runlim] sample:		5520.2 time, 2710.2 real, 3915.3 MB
[runlim] sample:		5559.7 time, 2720.2 real, 3922.1 MB
[runlim] sample:		5599.3 time, 2730.2 real, 3872.8 MB
[runlim] sample:		5638.9 time, 2740.2 real, 3875.3 MB
[runlim] sample:		5678.4 time, 2750.2 real, 3921.5 MB
[runlim] sample:		5718.0 time, 2760.2 real, 3926.1 MB
[runlim] sample:		5757.5 time, 2770.2 real, 3930.5 MB
[runlim] sample:		5797.1 time, 2780.2 real, 3966.3 MB
[runlim] sample:		5836.6 time, 2790.2 real, 3973.6 MB
[runlim] sample:		5876.2 time, 2800.2 real, 3979.4 MB
[runlim] sample:		5915.8 time, 2810.2 real, 4019.3 MB
[runlim] sample:		5955.3 time, 2820.2 real, 4025.6 MB
[runlim] sample:		5994.9 time, 2830.2 real, 4032.1 MB
[runlim] sample:		6034.5 time, 2840.2 real, 4037.7 MB
[runlim] sample:		6074.1 time, 2850.2 real, 4042.8 MB
[runlim] sample:		6113.6 time, 2860.2 real, 4046.1 MB
[runlim] sample:		6153.1 time, 2870.2 real, 4050.6 MB
[runlim] sample:		6192.7 time, 2880.2 real, 4053.9 MB
[runlim] sample:		6232.2 time, 2890.2 real, 4056.4 MB
[runlim] sample:		6271.8 time, 2900.2 real, 4063.9 MB
[runlim] sample:		6311.3 time, 2910.2 real, 4105.5 MB
[runlim] sample:		6350.9 time, 2920.2 real, 4108.3 MB
[runlim] sample:		6390.5 time, 2930.2 real, 4113.1 MB
[runlim] sample:		6430.0 time, 2940.2 real, 4114.9 MB
[runlim] sample:		6469.6 time, 2950.2 real, 4118.4 MB
[runlim] sample:		6509.1 time, 2960.2 real, 4122.2 MB
[runlim] sample:		6548.6 time, 2970.2 real, 4039.1 MB
[runlim] sample:		6588.2 time, 2980.2 real, 4040.1 MB
[runlim] sample:		6627.8 time, 2990.2 real, 4042.1 MB
[runlim] sample:		6667.3 time, 3000.2 real, 4044.5 MB
[runlim] sample:		6706.9 time, 3010.2 real, 4085.7 MB
[runlim] sample:		6746.4 time, 3020.2 real, 4088.3 MB
[runlim] sample:		6786.0 time, 3030.2 real, 4091.6 MB
[runlim] sample:		6825.5 time, 3040.2 real, 4124.1 MB
[runlim] sample:		6865.0 time, 3050.2 real, 4126.9 MB
[runlim] sample:		6904.6 time, 3060.2 real, 4131.2 MB
[runlim] sample:		6944.1 time, 3070.2 real, 4136.0 MB
[runlim] sample:		6983.7 time, 3080.2 real, 4138.7 MB
[runlim] sample:		7023.3 time, 3090.2 real, 4141.3 MB
[runlim] sample:		7062.8 time, 3100.2 real, 4145.3 MB
[runlim] sample:		7102.4 time, 3110.2 real, 4149.0 MB
[runlim] sample:		7141.9 time, 3120.2 real, 4185.5 MB
[runlim] sample:		7181.4 time, 3130.2 real, 4192.1 MB
[runlim] sample:		7220.9 time, 3140.2 real, 4194.7 MB
[runlim] sample:		7260.5 time, 3150.2 real, 4199.5 MB
[runlim] sample:		7300.1 time, 3160.2 real, 4204.0 MB
[runlim] sample:		7339.6 time, 3170.2 real, 4207.6 MB
[runlim] sample:		7379.2 time, 3180.2 real, 4211.4 MB
[runlim] sample:		7418.8 time, 3190.2 real, 4215.2 MB
[runlim] sample:		7458.3 time, 3200.2 real, 4219.5 MB
[runlim] sample:		7497.9 time, 3210.2 real, 4225.3 MB
[runlim] sample:		7537.5 time, 3220.2 real, 4228.1 MB
[runlim] sample:		7577.0 time, 3230.2 real, 4274.1 MB
[runlim] sample:		7616.6 time, 3240.2 real, 4204.9 MB
[runlim] sample:		7656.2 time, 3250.2 real, 4208.2 MB
[runlim] sample:		7695.8 time, 3260.2 real, 4210.5 MB
[runlim] sample:		7735.3 time, 3270.2 real, 4214.6 MB
[runlim] sample:		7774.9 time, 3280.2 real, 4219.2 MB
[runlim] sample:		7814.4 time, 3290.2 real, 4255.4 MB
[runlim] sample:		7854.0 time, 3300.2 real, 4261.2 MB
[runlim] sample:		7893.6 time, 3310.2 real, 4268.6 MB
[runlim] sample:		7933.1 time, 3320.2 real, 4305.7 MB
[runlim] sample:		7972.7 time, 3330.2 real, 4308.7 MB
[runlim] sample:		8012.3 time, 3340.2 real, 4311.8 MB
[runlim] sample:		8051.8 time, 3350.2 real, 4316.8 MB
[runlim] sample:		8091.4 time, 3360.2 real, 4318.2 MB
[runlim] sample:		8131.0 time, 3370.2 real, 4322.3 MB
[runlim] sample:		8170.5 time, 3380.2 real, 4325.8 MB
[runlim] sample:		8210.1 time, 3390.2 real, 4330.1 MB
[runlim] sample:		8249.6 time, 3400.2 real, 4333.2 MB
[runlim] sample:		8289.2 time, 3410.2 real, 4337.0 MB
[runlim] sample:		8328.8 time, 3420.2 real, 4374.3 MB
[runlim] sample:		8368.3 time, 3430.2 real, 4313.7 MB
[runlim] sample:		8407.9 time, 3440.2 real, 4315.5 MB
[runlim] sample:		8447.5 time, 3450.2 real, 4328.6 MB
[runlim] sample:		8487.0 time, 3460.2 real, 4331.8 MB
[runlim] sample:		8526.6 time, 3470.2 real, 4338.2 MB
[runlim] sample:		8566.1 time, 3480.2 real, 4341.2 MB
[runlim] sample:		8605.7 time, 3490.2 real, 4373.4 MB
[runlim] sample:		8645.2 time, 3500.2 real, 4378.5 MB
[runlim] sample:		8684.7 time, 3510.2 real, 4383.0 MB
[runlim] sample:		8724.3 time, 3520.2 real, 4387.2 MB
[runlim] sample:		8763.8 time, 3530.2 real, 4391.7 MB
[runlim] sample:		8803.4 time, 3540.2 real, 4392.0 MB
[runlim] sample:		8843.0 time, 3550.2 real, 4395.0 MB
[runlim] sample:		8882.5 time, 3560.2 real, 4398.8 MB
[runlim] sample:		8922.0 time, 3570.2 real, 4403.0 MB
[runlim] sample:		8961.6 time, 3580.2 real, 4409.0 MB
[runlim] sample:		9001.1 time, 3590.2 real, 4475.1 MB
[runlim] end:			Wed Sep 16 10:58:06 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		456299
[runlim] real:			3600.10 seconds
[runlim] time:			9039.92 seconds
[runlim] space:			4670.8 MB
[runlim] samples:		35998
