[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/pdtrav/single.pdtravdeep
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/viscoherencep3.aig
[runlim] start:			Sat Sep 19 04:30:46 2015
[runlim] main pid:		12532
[runlim] sample:		9.7 time, 10.4 real, 368.4 MB
[runlim] sample:		19.6 time, 20.4 real, 437.4 MB
[runlim] sample:		29.6 time, 30.4 real, 454.4 MB
[runlim] sample:		39.6 time, 40.4 real, 480.3 MB
[runlim] sample:		49.6 time, 50.4 real, 516.3 MB
[runlim] sample:		59.6 time, 60.4 real, 565.8 MB
[runlim] sample:		69.6 time, 70.4 real, 586.5 MB
[runlim] sample:		79.6 time, 80.4 real, 557.1 MB
[runlim] sample:		89.6 time, 90.4 real, 641.1 MB
[runlim] sample:		99.5 time, 100.4 real, 627.3 MB
[runlim] sample:		109.5 time, 110.4 real, 683.8 MB
[runlim] sample:		119.5 time, 120.4 real, 667.1 MB
[runlim] sample:		129.5 time, 130.4 real, 788.0 MB
[runlim] sample:		139.5 time, 140.4 real, 816.0 MB
[runlim] sample:		149.5 time, 150.4 real, 799.9 MB
[runlim] sample:		159.5 time, 160.4 real, 829.6 MB
[runlim] sample:		169.5 time, 170.4 real, 876.8 MB
[runlim] sample:		179.4 time, 180.4 real, 833.1 MB
[runlim] sample:		189.4 time, 190.4 real, 873.8 MB
[runlim] sample:		199.4 time, 200.4 real, 911.1 MB
[runlim] sample:		209.4 time, 210.4 real, 892.9 MB
[runlim] sample:		219.4 time, 220.4 real, 923.5 MB
[runlim] sample:		229.4 time, 230.4 real, 952.1 MB
[runlim] sample:		239.4 time, 240.4 real, 1016.1 MB
[runlim] sample:		249.3 time, 250.4 real, 1040.6 MB
[runlim] sample:		259.3 time, 260.4 real, 966.1 MB
[runlim] sample:		269.3 time, 270.4 real, 1007.4 MB
[runlim] sample:		279.3 time, 280.4 real, 1037.4 MB
[runlim] sample:		289.3 time, 290.4 real, 1184.9 MB
[runlim] sample:		299.3 time, 300.4 real, 1224.7 MB
[runlim] sample:		309.3 time, 310.4 real, 1251.9 MB
[runlim] sample:		319.2 time, 320.4 real, 1142.0 MB
[runlim] sample:		329.2 time, 330.4 real, 1173.4 MB
[runlim] sample:		339.2 time, 340.4 real, 1209.2 MB
[runlim] sample:		349.2 time, 350.4 real, 1237.0 MB
[runlim] sample:		359.2 time, 360.4 real, 1271.0 MB
[runlim] sample:		369.2 time, 370.4 real, 1303.2 MB
[runlim] sample:		379.2 time, 380.4 real, 1333.2 MB
[runlim] sample:		389.1 time, 390.4 real, 1371.7 MB
[runlim] sample:		399.1 time, 400.4 real, 1225.6 MB
[runlim] sample:		409.1 time, 410.4 real, 1250.4 MB
[runlim] sample:		419.1 time, 420.4 real, 1282.1 MB
[runlim] sample:		429.1 time, 430.4 real, 1364.1 MB
[runlim] sample:		439.1 time, 440.4 real, 1390.1 MB
[runlim] sample:		449.1 time, 450.4 real, 1427.3 MB
[runlim] sample:		459.0 time, 460.4 real, 1455.4 MB
[runlim] sample:		469.0 time, 470.4 real, 1488.0 MB
[runlim] sample:		479.0 time, 480.4 real, 1515.9 MB
[runlim] sample:		489.0 time, 490.4 real, 1329.5 MB
[runlim] sample:		499.0 time, 500.4 real, 1366.4 MB
[runlim] sample:		509.0 time, 510.4 real, 1405.0 MB
[runlim] sample:		519.0 time, 520.4 real, 1429.1 MB
[runlim] sample:		529.0 time, 530.4 real, 1458.2 MB
[runlim] sample:		538.9 time, 540.4 real, 1483.0 MB
[runlim] sample:		548.9 time, 550.4 real, 1520.2 MB
[runlim] sample:		558.9 time, 560.4 real, 1553.5 MB
[runlim] sample:		568.9 time, 570.4 real, 1585.2 MB
[runlim] sample:		578.9 time, 580.4 real, 1616.9 MB
[runlim] sample:		588.9 time, 590.4 real, 1643.0 MB
[runlim] sample:		598.9 time, 600.4 real, 1425.2 MB
[runlim] sample:		608.8 time, 610.4 real, 1452.6 MB
[runlim] sample:		618.8 time, 620.4 real, 1486.5 MB
[runlim] sample:		628.8 time, 630.4 real, 1514.0 MB
[runlim] sample:		638.8 time, 640.4 real, 1550.1 MB
[runlim] sample:		648.8 time, 650.4 real, 1581.4 MB
[runlim] sample:		658.8 time, 660.4 real, 1614.5 MB
[runlim] sample:		668.7 time, 670.4 real, 1642.1 MB
[runlim] sample:		678.7 time, 680.4 real, 1680.2 MB
[runlim] sample:		688.7 time, 690.4 real, 1711.2 MB
[runlim] sample:		698.7 time, 700.4 real, 1741.0 MB
[runlim] sample:		708.7 time, 710.4 real, 1788.9 MB
[runlim] sample:		718.7 time, 720.4 real, 1817.7 MB
[runlim] sample:		728.6 time, 730.4 real, 1559.6 MB
[runlim] sample:		738.6 time, 740.4 real, 1593.1 MB
[runlim] sample:		748.6 time, 750.4 real, 1617.0 MB
[runlim] sample:		758.6 time, 760.4 real, 1728.1 MB
[runlim] sample:		768.6 time, 770.4 real, 1752.7 MB
[runlim] sample:		778.6 time, 780.4 real, 1776.1 MB
[runlim] sample:		788.6 time, 790.4 real, 1809.7 MB
[runlim] sample:		798.6 time, 800.4 real, 2082.5 MB
[runlim] sample:		808.5 time, 810.4 real, 2107.2 MB
[runlim] sample:		818.5 time, 820.4 real, 2138.3 MB
[runlim] sample:		828.5 time, 830.4 real, 2161.9 MB
[runlim] sample:		838.5 time, 840.4 real, 2201.8 MB
[runlim] sample:		848.5 time, 850.4 real, 2225.4 MB
[runlim] sample:		858.5 time, 860.4 real, 2257.4 MB
[runlim] sample:		868.5 time, 870.4 real, 2284.8 MB
[runlim] sample:		878.5 time, 880.4 real, 1988.8 MB
[runlim] sample:		888.4 time, 890.4 real, 2030.3 MB
[runlim] sample:		898.4 time, 900.4 real, 2055.9 MB
[runlim] sample:		908.4 time, 910.4 real, 2088.5 MB
[runlim] sample:		918.4 time, 920.4 real, 2115.7 MB
[runlim] sample:		928.4 time, 930.4 real, 2158.9 MB
[runlim] sample:		938.4 time, 940.4 real, 2183.7 MB
[runlim] sample:		948.4 time, 950.4 real, 2219.0 MB
[runlim] sample:		958.3 time, 960.4 real, 2253.1 MB
[runlim] sample:		968.3 time, 970.4 real, 2285.5 MB
[runlim] sample:		978.3 time, 980.4 real, 2310.0 MB
[runlim] sample:		988.3 time, 990.4 real, 2337.0 MB
[runlim] sample:		998.3 time, 1000.4 real, 2368.7 MB
[runlim] sample:		1008.3 time, 1010.4 real, 2406.5 MB
[runlim] sample:		1018.2 time, 1020.4 real, 2440.5 MB
[runlim] sample:		1028.2 time, 1030.4 real, 2466.9 MB
[runlim] sample:		1038.2 time, 1040.4 real, 2497.1 MB
[runlim] sample:		1048.2 time, 1050.4 real, 2136.4 MB
[runlim] sample:		1058.2 time, 1060.4 real, 2165.5 MB
[runlim] sample:		1068.2 time, 1070.4 real, 2195.6 MB
[runlim] sample:		1078.2 time, 1080.4 real, 2236.0 MB
[runlim] sample:		1088.2 time, 1090.4 real, 2264.4 MB
[runlim] sample:		1098.1 time, 1100.4 real, 2290.4 MB
[runlim] sample:		1108.1 time, 1110.4 real, 2322.0 MB
[runlim] sample:		1118.1 time, 1120.4 real, 2359.1 MB
[runlim] sample:		1128.1 time, 1130.4 real, 2387.3 MB
[runlim] sample:		1138.1 time, 1140.4 real, 2411.5 MB
[runlim] sample:		1148.1 time, 1150.4 real, 2437.6 MB
[runlim] sample:		1158.0 time, 1160.4 real, 2469.3 MB
[runlim] sample:		1168.0 time, 1170.4 real, 2485.3 MB
[runlim] sample:		1178.0 time, 1180.4 real, 2513.5 MB
[runlim] sample:		1188.0 time, 1190.4 real, 2538.5 MB
[runlim] sample:		1198.0 time, 1200.4 real, 2568.3 MB
[runlim] sample:		1208.0 time, 1210.4 real, 2590.2 MB
[runlim] sample:		1218.0 time, 1220.4 real, 2617.8 MB
[runlim] sample:		1228.0 time, 1230.4 real, 2677.5 MB
[runlim] sample:		1237.9 time, 1240.4 real, 2695.9 MB
[runlim] sample:		1247.9 time, 1250.4 real, 2717.9 MB
[runlim] sample:		1257.9 time, 1260.4 real, 2743.8 MB
[runlim] sample:		1267.9 time, 1270.4 real, 2302.7 MB
[runlim] sample:		1277.9 time, 1280.4 real, 2335.3 MB
[runlim] sample:		1287.9 time, 1290.4 real, 2363.4 MB
[runlim] sample:		1297.9 time, 1300.4 real, 2388.1 MB
[runlim] sample:		1307.8 time, 1310.4 real, 2423.4 MB
[runlim] sample:		1317.8 time, 1320.4 real, 2447.3 MB
[runlim] sample:		1327.8 time, 1330.4 real, 2472.6 MB
[runlim] sample:		1337.8 time, 1340.4 real, 2596.2 MB
[runlim] sample:		1347.8 time, 1350.4 real, 2616.6 MB
[runlim] sample:		1357.8 time, 1360.4 real, 2639.1 MB
[runlim] sample:		1367.8 time, 1370.4 real, 2663.6 MB
[runlim] sample:		1377.7 time, 1380.4 real, 2684.1 MB
[runlim] sample:		1387.7 time, 1390.4 real, 2714.6 MB
[runlim] sample:		1397.7 time, 1400.4 real, 2739.0 MB
[runlim] sample:		1407.7 time, 1410.4 real, 2782.4 MB
[runlim] sample:		1417.7 time, 1420.4 real, 2808.6 MB
[runlim] sample:		1427.7 time, 1430.4 real, 2834.6 MB
[runlim] sample:		1437.7 time, 1440.4 real, 2856.6 MB
[runlim] sample:		1447.7 time, 1450.4 real, 2882.9 MB
[runlim] sample:		1457.6 time, 1460.4 real, 2921.0 MB
[runlim] sample:		1467.6 time, 1470.4 real, 2955.1 MB
[runlim] sample:		1477.6 time, 1480.4 real, 2977.1 MB
[runlim] sample:		1487.6 time, 1490.4 real, 2998.3 MB
[runlim] sample:		1497.6 time, 1500.4 real, 3026.2 MB
[runlim] sample:		1507.6 time, 1510.4 real, 3054.3 MB
[runlim] sample:		1517.5 time, 1520.4 real, 3082.5 MB
[runlim] sample:		1527.5 time, 1530.4 real, 3112.7 MB
[runlim] sample:		1537.5 time, 1540.4 real, 3145.3 MB
[runlim] sample:		1547.5 time, 1550.4 real, 2556.6 MB
[runlim] sample:		1557.5 time, 1560.4 real, 2586.5 MB
[runlim] sample:		1567.5 time, 1570.4 real, 2618.5 MB
[runlim] sample:		1577.5 time, 1580.4 real, 2644.6 MB
[runlim] sample:		1587.4 time, 1590.4 real, 2671.5 MB
[runlim] sample:		1597.4 time, 1600.4 real, 2702.1 MB
[runlim] sample:		1607.4 time, 1610.4 real, 2719.7 MB
[runlim] sample:		1617.4 time, 1620.4 real, 2762.4 MB
[runlim] sample:		1627.4 time, 1630.4 real, 2787.2 MB
[runlim] sample:		1637.4 time, 1640.4 real, 2807.2 MB
[runlim] sample:		1647.3 time, 1650.4 real, 2829.5 MB
[runlim] sample:		1657.3 time, 1660.4 real, 2855.7 MB
[runlim] sample:		1667.3 time, 1670.4 real, 2885.9 MB
[runlim] sample:		1677.3 time, 1680.4 real, 2906.4 MB
[runlim] sample:		1687.3 time, 1690.4 real, 2928.9 MB
[runlim] sample:		1697.3 time, 1700.4 real, 2957.8 MB
[runlim] sample:		1707.3 time, 1710.4 real, 2992.4 MB
[runlim] sample:		1717.2 time, 1720.4 real, 3012.4 MB
[runlim] sample:		1727.2 time, 1730.4 real, 3040.4 MB
[runlim] sample:		1737.2 time, 1740.4 real, 3064.6 MB
[runlim] sample:		1747.2 time, 1750.4 real, 3097.5 MB
[runlim] sample:		1757.2 time, 1760.4 real, 3126.3 MB
[runlim] sample:		1767.2 time, 1770.4 real, 3161.1 MB
[runlim] sample:		1777.2 time, 1780.4 real, 3187.5 MB
[runlim] sample:		1787.1 time, 1790.4 real, 3215.4 MB
[runlim] sample:		1797.1 time, 1800.4 real, 3243.5 MB
[runlim] sample:		1807.1 time, 1810.4 real, 3270.0 MB
[runlim] sample:		1817.1 time, 1820.4 real, 3301.3 MB
[runlim] sample:		1827.1 time, 1830.4 real, 3327.3 MB
[runlim] sample:		1837.1 time, 1840.4 real, 3355.5 MB
[runlim] sample:		1847.1 time, 1850.4 real, 3379.2 MB
[runlim] sample:		1857.0 time, 1860.4 real, 3407.5 MB
[runlim] sample:		1867.0 time, 1870.4 real, 3429.5 MB
[runlim] sample:		1877.0 time, 1880.4 real, 3451.9 MB
[runlim] sample:		1887.0 time, 1890.4 real, 3480.0 MB
[runlim] sample:		1897.0 time, 1900.4 real, 3510.4 MB
[runlim] sample:		1907.0 time, 1910.4 real, 2747.5 MB
[runlim] sample:		1917.0 time, 1920.4 real, 2778.9 MB
[runlim] sample:		1926.9 time, 1930.4 real, 2818.7 MB
[runlim] sample:		1936.9 time, 1940.4 real, 2843.2 MB
[runlim] sample:		1946.9 time, 1950.4 real, 2869.4 MB
[runlim] sample:		1956.9 time, 1960.4 real, 2899.7 MB
[runlim] sample:		1966.9 time, 1970.4 real, 2925.7 MB
[runlim] sample:		1976.9 time, 1980.4 real, 2956.4 MB
[runlim] sample:		1986.8 time, 1990.4 real, 2982.4 MB
[runlim] sample:		1996.8 time, 2000.4 real, 3012.4 MB
[runlim] sample:		2006.8 time, 2010.4 real, 3035.1 MB
[runlim] sample:		2016.8 time, 2020.4 real, 3062.2 MB
[runlim] sample:		2026.8 time, 2030.4 real, 3088.0 MB
[runlim] sample:		2036.8 time, 2040.4 real, 3114.0 MB
[runlim] sample:		2046.8 time, 2050.4 real, 3140.1 MB
[runlim] sample:		2056.8 time, 2060.4 real, 3164.1 MB
[runlim] sample:		2066.7 time, 2070.4 real, 3188.7 MB
[runlim] sample:		2076.7 time, 2080.4 real, 3224.9 MB
[runlim] sample:		2086.7 time, 2090.4 real, 3252.9 MB
[runlim] sample:		2096.7 time, 2100.4 real, 3280.0 MB
[runlim] sample:		2106.7 time, 2110.4 real, 3304.0 MB
[runlim] sample:		2116.7 time, 2120.4 real, 3332.4 MB
[runlim] sample:		2126.6 time, 2130.4 real, 3362.8 MB
[runlim] sample:		2136.6 time, 2140.4 real, 3380.8 MB
[runlim] sample:		2146.6 time, 2150.4 real, 3406.1 MB
[runlim] sample:		2156.6 time, 2160.4 real, 3436.5 MB
[runlim] sample:		2166.6 time, 2170.4 real, 3462.6 MB
[runlim] sample:		2176.6 time, 2180.4 real, 3486.5 MB
[runlim] sample:		2186.6 time, 2190.4 real, 3512.3 MB
[runlim] sample:		2196.5 time, 2200.4 real, 3543.0 MB
[runlim] sample:		2206.5 time, 2210.4 real, 3573.6 MB
[runlim] sample:		2216.5 time, 2220.4 real, 3595.6 MB
[runlim] sample:		2226.5 time, 2230.4 real, 3621.7 MB
[runlim] sample:		2236.5 time, 2240.4 real, 3662.3 MB
[runlim] sample:		2246.5 time, 2250.4 real, 3685.8 MB
[runlim] sample:		2256.4 time, 2260.4 real, 3716.1 MB
[runlim] sample:		2266.4 time, 2270.4 real, 3738.1 MB
[runlim] sample:		2276.4 time, 2280.4 real, 3775.4 MB
[runlim] sample:		2286.4 time, 2290.4 real, 3801.4 MB
[runlim] sample:		2296.4 time, 2300.4 real, 3822.5 MB
[runlim] sample:		2306.4 time, 2310.4 real, 3840.7 MB
[runlim] sample:		2312.4 time, 2320.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2330.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2340.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2350.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2360.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2370.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2380.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2390.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2400.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2410.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2420.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2430.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2440.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2450.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2460.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2470.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2480.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2490.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2500.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2510.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2520.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2530.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2540.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2550.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2560.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2570.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2580.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2590.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2600.4 real, 2970.3 MB
[runlim] sample:		2312.4 time, 2610.4 real, 2970.3 MB
[runlim] sample:		2316.4 time, 2620.4 real, 2979.9 MB
[runlim] sample:		2326.3 time, 2630.4 real, 3010.0 MB
[runlim] sample:		2336.3 time, 2640.4 real, 3046.1 MB
[runlim] sample:		2346.3 time, 2650.4 real, 3077.0 MB
[runlim] sample:		2356.3 time, 2660.4 real, 3100.5 MB
[runlim] sample:		2366.3 time, 2670.4 real, 3126.8 MB
[runlim] sample:		2376.3 time, 2680.4 real, 3153.1 MB
[runlim] sample:		2386.2 time, 2690.4 real, 3179.5 MB
[runlim] sample:		2396.2 time, 2700.4 real, 3206.2 MB
[runlim] sample:		2406.2 time, 2710.4 real, 3226.2 MB
[runlim] sample:		2416.2 time, 2720.4 real, 3670.1 MB
[runlim] sample:		2426.2 time, 2730.4 real, 3690.1 MB
[runlim] sample:		2436.2 time, 2740.4 real, 3715.4 MB
[runlim] sample:		2446.2 time, 2750.4 real, 3741.7 MB
[runlim] sample:		2456.1 time, 2760.4 real, 3766.5 MB
[runlim] sample:		2466.1 time, 2770.4 real, 3795.7 MB
[runlim] sample:		2476.1 time, 2780.4 real, 3815.7 MB
[runlim] sample:		2486.1 time, 2790.4 real, 3842.1 MB
[runlim] sample:		2496.1 time, 2800.4 real, 3894.8 MB
[runlim] sample:		2506.1 time, 2810.4 real, 3919.0 MB
[runlim] sample:		2516.1 time, 2820.4 real, 3939.0 MB
[runlim] sample:		2526.0 time, 2830.4 real, 3959.2 MB
[runlim] sample:		2536.0 time, 2840.4 real, 3981.2 MB
[runlim] sample:		2546.0 time, 2850.4 real, 4003.6 MB
[runlim] sample:		2556.0 time, 2860.4 real, 4027.6 MB
[runlim] sample:		2566.0 time, 2870.4 real, 4047.8 MB
[runlim] sample:		2576.0 time, 2880.4 real, 4067.8 MB
[runlim] sample:		2585.9 time, 2890.4 real, 4075.8 MB
[runlim] sample:		2595.9 time, 2900.4 real, 4094.1 MB
[runlim] sample:		2605.9 time, 2910.4 real, 4116.1 MB
[runlim] sample:		2615.9 time, 2920.4 real, 4133.9 MB
[runlim] sample:		2625.9 time, 2930.4 real, 4149.9 MB
[runlim] sample:		2635.9 time, 2940.4 real, 4184.1 MB
[runlim] sample:		2645.9 time, 2950.4 real, 4204.1 MB
[runlim] sample:		2655.9 time, 2960.4 real, 4228.5 MB
[runlim] sample:		2665.8 time, 2970.4 real, 4250.9 MB
[runlim] sample:		2675.8 time, 2980.4 real, 4272.6 MB
[runlim] sample:		2685.8 time, 2990.4 real, 4298.8 MB
[runlim] sample:		2695.8 time, 3000.4 real, 4322.9 MB
[runlim] sample:		2705.8 time, 3010.4 real, 4354.6 MB
[runlim] sample:		2715.8 time, 3020.4 real, 4378.6 MB
[runlim] sample:		2725.7 time, 3030.4 real, 4405.7 MB
[runlim] sample:		2735.7 time, 3040.4 real, 4432.3 MB
[runlim] sample:		2745.7 time, 3050.4 real, 4454.3 MB
[runlim] sample:		2755.7 time, 3060.4 real, 4477.3 MB
[runlim] sample:		2765.7 time, 3070.4 real, 4501.5 MB
[runlim] sample:		2775.7 time, 3080.4 real, 4528.4 MB
[runlim] sample:		2785.7 time, 3090.4 real, 4552.4 MB
[runlim] sample:		2795.7 time, 3100.4 real, 4574.7 MB
[runlim] sample:		2805.6 time, 3110.4 real, 4598.7 MB
[runlim] sample:		2815.6 time, 3120.4 real, 4627.3 MB
[runlim] sample:		2825.6 time, 3130.4 real, 4754.1 MB
[runlim] sample:		2835.6 time, 3140.4 real, 4806.5 MB
[runlim] sample:		2845.6 time, 3150.4 real, 3740.5 MB
[runlim] sample:		2855.6 time, 3160.4 real, 3766.8 MB
[runlim] sample:		2865.5 time, 3170.4 real, 3793.0 MB
[runlim] sample:		2875.5 time, 3180.4 real, 3815.2 MB
[runlim] sample:		2885.5 time, 3190.4 real, 3837.7 MB
[runlim] sample:		2895.5 time, 3200.4 real, 3863.9 MB
[runlim] sample:		2905.5 time, 3210.4 real, 3889.9 MB
[runlim] sample:		2915.5 time, 3220.4 real, 3920.1 MB
[runlim] sample:		2925.4 time, 3230.4 real, 3946.1 MB
[runlim] sample:		2935.4 time, 3240.4 real, 3970.3 MB
[runlim] sample:		2945.4 time, 3250.4 real, 3990.5 MB
[runlim] sample:		2955.4 time, 3260.4 real, 4008.5 MB
[runlim] sample:		2965.4 time, 3270.4 real, 4032.6 MB
[runlim] sample:		2975.4 time, 3280.4 real, 4052.8 MB
[runlim] sample:		2985.3 time, 3290.4 real, 4074.8 MB
[runlim] sample:		2995.3 time, 3300.4 real, 4103.1 MB
[runlim] sample:		3005.3 time, 3310.4 real, 4137.1 MB
[runlim] sample:		3015.3 time, 3320.4 real, 4163.1 MB
[runlim] sample:		3025.3 time, 3330.4 real, 4191.4 MB
[runlim] sample:		3035.3 time, 3340.4 real, 4217.3 MB
[runlim] sample:		3045.3 time, 3350.4 real, 4246.2 MB
[runlim] sample:		3055.2 time, 3360.4 real, 4268.2 MB
[runlim] sample:		3065.2 time, 3370.4 real, 4296.8 MB
[runlim] sample:		3075.2 time, 3380.4 real, 4322.9 MB
[runlim] sample:		3085.2 time, 3390.4 real, 4344.9 MB
[runlim] sample:		3095.2 time, 3400.4 real, 4371.7 MB
[runlim] sample:		3105.2 time, 3410.4 real, 4395.8 MB
[runlim] sample:		3115.2 time, 3420.4 real, 4425.9 MB
[runlim] sample:		3125.2 time, 3430.4 real, 4454.4 MB
[runlim] sample:		3135.1 time, 3440.4 real, 4474.4 MB
[runlim] sample:		3145.1 time, 3450.4 real, 4502.9 MB
[runlim] sample:		3155.1 time, 3460.4 real, 4524.9 MB
[runlim] sample:		3165.1 time, 3470.4 real, 4562.7 MB
[runlim] sample:		3175.1 time, 3480.4 real, 4588.4 MB
[runlim] sample:		3185.1 time, 3490.4 real, 4610.4 MB
[runlim] sample:		3195.1 time, 3500.4 real, 4634.7 MB
[runlim] sample:		3205.1 time, 3510.4 real, 4657.6 MB
[runlim] sample:		3215.0 time, 3520.4 real, 4677.6 MB
[runlim] sample:		3225.0 time, 3530.4 real, 4705.2 MB
[runlim] sample:		3235.0 time, 3540.4 real, 4721.2 MB
[runlim] sample:		3245.0 time, 3550.4 real, 4744.6 MB
[runlim] sample:		3255.0 time, 3560.4 real, 4768.4 MB
[runlim] sample:		3265.0 time, 3570.4 real, 4782.4 MB
[runlim] sample:		3274.9 time, 3580.4 real, 4804.4 MB
[runlim] sample:		3284.9 time, 3590.4 real, 4832.4 MB
[runlim] end:			Sat Sep 19 05:30:46 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		4
[runlim] real:			3600.18 seconds
[runlim] time:			3294.68 seconds
[runlim] space:			4960.5 MB
[runlim] samples:		35998
