[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/hwmcc14/single/6s195.aig
[runlim] start:			Tue Sep 15 20:00:38 2015
[runlim] main pid:		26281
[runlim] sample:		7.4 time, 10.6 real, 400.5 MB
[runlim] sample:		17.4 time, 20.6 real, 464.7 MB
[runlim] sample:		27.3 time, 30.6 real, 512.7 MB
[runlim] sample:		37.3 time, 40.6 real, 517.3 MB
[runlim] sample:		47.3 time, 50.6 real, 567.3 MB
[runlim] sample:		57.3 time, 60.6 real, 582.9 MB
[runlim] sample:		67.3 time, 70.6 real, 594.4 MB
[runlim] sample:		77.3 time, 80.6 real, 594.4 MB
[runlim] sample:		87.2 time, 90.6 real, 601.6 MB
[runlim] sample:		97.2 time, 100.6 real, 603.8 MB
[runlim] sample:		107.2 time, 110.6 real, 633.6 MB
[runlim] sample:		117.2 time, 120.6 real, 635.6 MB
[runlim] sample:		127.2 time, 130.6 real, 644.3 MB
[runlim] sample:		137.2 time, 140.6 real, 646.3 MB
[runlim] sample:		147.2 time, 150.6 real, 646.3 MB
[runlim] sample:		157.1 time, 160.6 real, 651.4 MB
[runlim] sample:		167.1 time, 170.6 real, 653.4 MB
[runlim] sample:		177.1 time, 180.6 real, 715.1 MB
[runlim] sample:		187.1 time, 190.6 real, 719.9 MB
[runlim] sample:		197.1 time, 200.6 real, 721.9 MB
[runlim] sample:		207.1 time, 210.6 real, 721.9 MB
[runlim] sample:		217.1 time, 220.6 real, 733.1 MB
[runlim] sample:		227.0 time, 230.6 real, 733.1 MB
[runlim] sample:		237.0 time, 240.6 real, 733.3 MB
[runlim] sample:		247.0 time, 250.6 real, 752.9 MB
[runlim] sample:		257.0 time, 260.6 real, 753.1 MB
[runlim] sample:		267.0 time, 270.6 real, 753.6 MB
[runlim] sample:		276.9 time, 280.6 real, 771.7 MB
[runlim] sample:		286.9 time, 290.6 real, 771.7 MB
[runlim] sample:		296.9 time, 300.6 real, 771.7 MB
[runlim] sample:		306.9 time, 310.6 real, 771.7 MB
[runlim] sample:		316.9 time, 320.6 real, 781.6 MB
[runlim] sample:		326.9 time, 330.6 real, 781.6 MB
[runlim] sample:		336.9 time, 340.6 real, 781.6 MB
[runlim] sample:		346.9 time, 350.6 real, 781.6 MB
[runlim] sample:		356.8 time, 360.6 real, 789.6 MB
[runlim] sample:		366.8 time, 370.6 real, 788.0 MB
[runlim] sample:		376.8 time, 380.6 real, 788.0 MB
[runlim] sample:		386.8 time, 390.6 real, 788.0 MB
[runlim] sample:		396.8 time, 400.6 real, 788.0 MB
[runlim] sample:		406.8 time, 410.6 real, 798.9 MB
[runlim] sample:		416.8 time, 420.6 real, 798.9 MB
[runlim] sample:		426.7 time, 430.6 real, 798.9 MB
[runlim] sample:		436.7 time, 440.6 real, 798.9 MB
[runlim] sample:		446.7 time, 450.6 real, 798.9 MB
[runlim] sample:		456.7 time, 460.6 real, 810.3 MB
[runlim] sample:		466.7 time, 470.6 real, 810.3 MB
[runlim] sample:		476.7 time, 480.6 real, 810.3 MB
[runlim] sample:		486.6 time, 490.6 real, 810.3 MB
[runlim] sample:		496.6 time, 500.6 real, 810.3 MB
[runlim] sample:		506.6 time, 510.6 real, 819.6 MB
[runlim] sample:		516.6 time, 520.6 real, 819.6 MB
[runlim] sample:		526.6 time, 530.6 real, 819.6 MB
[runlim] sample:		536.6 time, 540.6 real, 819.6 MB
[runlim] sample:		546.5 time, 550.6 real, 824.3 MB
[runlim] sample:		556.5 time, 560.6 real, 865.6 MB
[runlim] sample:		566.5 time, 570.6 real, 865.6 MB
[runlim] sample:		576.5 time, 580.6 real, 865.6 MB
[runlim] sample:		586.5 time, 590.6 real, 865.6 MB
[runlim] sample:		596.5 time, 600.6 real, 865.6 MB
[runlim] sample:		606.5 time, 610.6 real, 865.6 MB
[runlim] sample:		616.4 time, 620.6 real, 875.4 MB
[runlim] sample:		626.4 time, 630.6 real, 875.4 MB
[runlim] sample:		636.4 time, 640.6 real, 875.4 MB
[runlim] sample:		646.4 time, 650.6 real, 875.4 MB
[runlim] sample:		656.4 time, 660.6 real, 875.4 MB
[runlim] sample:		666.4 time, 670.6 real, 875.4 MB
[runlim] sample:		676.4 time, 680.6 real, 885.7 MB
[runlim] sample:		686.3 time, 690.6 real, 885.9 MB
[runlim] sample:		696.3 time, 700.6 real, 886.0 MB
[runlim] sample:		706.3 time, 710.6 real, 886.2 MB
[runlim] sample:		716.3 time, 720.6 real, 886.3 MB
[runlim] sample:		726.3 time, 730.6 real, 886.5 MB
[runlim] sample:		736.3 time, 740.6 real, 1009.2 MB
[runlim] sample:		746.2 time, 750.6 real, 1009.4 MB
[runlim] sample:		756.2 time, 760.6 real, 1009.5 MB
[runlim] sample:		766.2 time, 770.6 real, 1009.7 MB
[runlim] sample:		776.2 time, 780.6 real, 1009.8 MB
[runlim] sample:		786.2 time, 790.6 real, 1011.9 MB
[runlim] sample:		796.2 time, 800.6 real, 1011.9 MB
[runlim] sample:		806.1 time, 810.6 real, 1019.3 MB
[runlim] sample:		816.1 time, 820.6 real, 1019.3 MB
[runlim] sample:		826.1 time, 830.6 real, 1019.3 MB
[runlim] sample:		836.1 time, 840.6 real, 1019.3 MB
[runlim] sample:		846.1 time, 850.6 real, 1026.3 MB
[runlim] sample:		856.1 time, 860.6 real, 1021.3 MB
[runlim] sample:		866.1 time, 870.6 real, 1021.3 MB
[runlim] sample:		876.0 time, 880.6 real, 1025.4 MB
[runlim] sample:		886.0 time, 890.6 real, 1025.4 MB
[runlim] sample:		896.0 time, 900.6 real, 1025.4 MB
[runlim] sample:		906.0 time, 910.6 real, 1025.4 MB
[runlim] sample:		916.0 time, 920.6 real, 1025.4 MB
[runlim] sample:		926.0 time, 930.6 real, 1025.4 MB
[runlim] sample:		936.0 time, 940.6 real, 1027.4 MB
[runlim] sample:		945.9 time, 950.6 real, 1034.6 MB
[runlim] sample:		955.9 time, 960.6 real, 1033.9 MB
[runlim] sample:		965.9 time, 970.6 real, 1033.9 MB
[runlim] sample:		975.9 time, 980.6 real, 1033.9 MB
[runlim] sample:		985.9 time, 990.6 real, 1033.9 MB
[runlim] sample:		995.9 time, 1000.6 real, 1033.9 MB
[runlim] sample:		1005.9 time, 1010.6 real, 1033.9 MB
[runlim] sample:		1015.8 time, 1020.6 real, 1035.9 MB
[runlim] sample:		1025.8 time, 1030.6 real, 1044.0 MB
[runlim] sample:		1035.8 time, 1040.6 real, 1044.0 MB
[runlim] sample:		1045.8 time, 1050.6 real, 1044.0 MB
[runlim] sample:		1055.8 time, 1060.6 real, 1044.0 MB
[runlim] sample:		1065.8 time, 1070.6 real, 1044.0 MB
[runlim] sample:		1075.8 time, 1080.6 real, 1044.0 MB
[runlim] sample:		1085.7 time, 1090.6 real, 1044.0 MB
[runlim] sample:		1095.7 time, 1100.6 real, 1044.0 MB
[runlim] sample:		1105.7 time, 1110.6 real, 1054.4 MB
[runlim] sample:		1115.7 time, 1120.6 real, 1054.4 MB
[runlim] sample:		1125.7 time, 1130.6 real, 1056.1 MB
[runlim] sample:		1135.7 time, 1140.6 real, 1057.2 MB
[runlim] sample:		1145.7 time, 1150.6 real, 1057.2 MB
[runlim] sample:		1155.6 time, 1160.6 real, 1057.2 MB
[runlim] sample:		1165.6 time, 1170.6 real, 1057.2 MB
[runlim] sample:		1175.6 time, 1180.6 real, 1057.2 MB
[runlim] sample:		1185.6 time, 1190.6 real, 1067.6 MB
[runlim] sample:		1195.6 time, 1200.6 real, 1067.6 MB
[runlim] sample:		1205.6 time, 1210.6 real, 1067.6 MB
[runlim] sample:		1215.5 time, 1220.6 real, 1067.6 MB
[runlim] sample:		1225.5 time, 1230.6 real, 1067.6 MB
[runlim] sample:		1235.5 time, 1240.6 real, 1067.6 MB
[runlim] sample:		1245.5 time, 1250.6 real, 1067.6 MB
[runlim] sample:		1255.5 time, 1260.6 real, 1068.9 MB
[runlim] sample:		1265.5 time, 1270.6 real, 1082.5 MB
[runlim] sample:		1275.5 time, 1280.6 real, 1082.5 MB
[runlim] sample:		1285.4 time, 1290.6 real, 1082.5 MB
[runlim] sample:		1295.4 time, 1300.6 real, 1082.5 MB
[runlim] sample:		1305.4 time, 1310.6 real, 1082.5 MB
[runlim] sample:		1315.4 time, 1320.6 real, 1082.5 MB
[runlim] sample:		1325.4 time, 1330.6 real, 1082.5 MB
[runlim] sample:		1335.4 time, 1340.6 real, 1095.7 MB
[runlim] sample:		1345.3 time, 1350.6 real, 1084.2 MB
[runlim] sample:		1355.3 time, 1360.6 real, 1112.8 MB
[runlim] sample:		1365.3 time, 1370.6 real, 1113.1 MB
[runlim] sample:		1375.3 time, 1380.6 real, 1113.1 MB
[runlim] sample:		1385.3 time, 1390.6 real, 1113.1 MB
[runlim] sample:		1395.2 time, 1400.6 real, 1113.4 MB
[runlim] sample:		1405.2 time, 1410.6 real, 1113.4 MB
[runlim] sample:		1415.2 time, 1420.6 real, 1113.4 MB
[runlim] sample:		1425.2 time, 1430.6 real, 1113.4 MB
[runlim] sample:		1435.2 time, 1440.6 real, 1113.4 MB
[runlim] sample:		1445.2 time, 1450.6 real, 1121.7 MB
[runlim] sample:		1455.1 time, 1460.6 real, 1124.9 MB
[runlim] sample:		1465.1 time, 1470.6 real, 1124.9 MB
[runlim] sample:		1475.1 time, 1480.6 real, 1124.9 MB
[runlim] sample:		1485.1 time, 1490.6 real, 1124.9 MB
[runlim] sample:		1495.1 time, 1500.6 real, 1124.9 MB
[runlim] sample:		1505.0 time, 1510.6 real, 1126.1 MB
[runlim] sample:		1515.0 time, 1520.6 real, 1127.6 MB
[runlim] sample:		1525.0 time, 1530.6 real, 1127.6 MB
[runlim] sample:		1535.0 time, 1540.6 real, 1138.7 MB
[runlim] sample:		1545.0 time, 1550.6 real, 1137.2 MB
[runlim] sample:		1555.0 time, 1560.6 real, 1137.2 MB
[runlim] sample:		1564.9 time, 1570.6 real, 1137.8 MB
[runlim] sample:		1574.9 time, 1580.6 real, 1137.8 MB
[runlim] sample:		1584.9 time, 1590.6 real, 1137.8 MB
[runlim] sample:		1594.9 time, 1600.6 real, 1137.8 MB
[runlim] sample:		1604.9 time, 1610.6 real, 1140.1 MB
[runlim] sample:		1614.8 time, 1620.6 real, 1140.1 MB
[runlim] sample:		1624.8 time, 1630.6 real, 1147.0 MB
[runlim] sample:		1634.8 time, 1640.6 real, 1147.0 MB
[runlim] sample:		1644.8 time, 1650.6 real, 1147.0 MB
[runlim] sample:		1654.8 time, 1660.6 real, 1147.0 MB
[runlim] sample:		1664.8 time, 1670.6 real, 1147.0 MB
[runlim] sample:		1674.7 time, 1680.6 real, 1147.0 MB
[runlim] sample:		1684.7 time, 1690.6 real, 1147.0 MB
[runlim] sample:		1694.7 time, 1700.6 real, 1147.0 MB
[runlim] sample:		1704.7 time, 1710.6 real, 1147.0 MB
[runlim] sample:		1714.7 time, 1720.6 real, 1173.6 MB
[runlim] sample:		1724.7 time, 1730.6 real, 1174.3 MB
[runlim] sample:		1734.6 time, 1740.6 real, 1174.3 MB
[runlim] sample:		1744.6 time, 1750.6 real, 1174.3 MB
[runlim] sample:		1754.6 time, 1760.6 real, 1174.3 MB
[runlim] sample:		1764.6 time, 1770.6 real, 1174.3 MB
[runlim] sample:		1774.6 time, 1780.6 real, 1174.3 MB
[runlim] sample:		1784.5 time, 1790.6 real, 1174.3 MB
[runlim] sample:		1794.5 time, 1800.6 real, 1175.5 MB
[runlim] sample:		1804.5 time, 1810.6 real, 1175.5 MB
[runlim] sample:		1814.5 time, 1820.6 real, 1187.7 MB
[runlim] sample:		1824.5 time, 1830.6 real, 1187.7 MB
[runlim] sample:		1834.5 time, 1840.6 real, 1187.7 MB
[runlim] sample:		1844.4 time, 1850.6 real, 1187.7 MB
[runlim] sample:		1854.4 time, 1860.6 real, 1187.7 MB
[runlim] sample:		1864.4 time, 1870.6 real, 1187.7 MB
[runlim] sample:		1874.4 time, 1880.6 real, 1187.7 MB
[runlim] sample:		1884.4 time, 1890.6 real, 1187.7 MB
[runlim] sample:		1894.4 time, 1900.6 real, 1187.7 MB
[runlim] sample:		1904.3 time, 1910.6 real, 1196.0 MB
[runlim] sample:		1914.3 time, 1920.6 real, 1196.2 MB
[runlim] sample:		1924.3 time, 1930.6 real, 1196.2 MB
[runlim] sample:		1934.3 time, 1940.6 real, 1196.2 MB
[runlim] sample:		1944.3 time, 1950.6 real, 1196.2 MB
[runlim] sample:		1954.3 time, 1960.6 real, 1196.2 MB
[runlim] sample:		1964.2 time, 1970.6 real, 1196.2 MB
[runlim] sample:		1974.2 time, 1980.6 real, 1196.2 MB
[runlim] sample:		1984.2 time, 1990.6 real, 1196.2 MB
[runlim] sample:		1994.2 time, 2000.6 real, 1196.2 MB
[runlim] sample:		2004.2 time, 2010.6 real, 1200.9 MB
[runlim] sample:		2014.2 time, 2020.6 real, 1201.0 MB
[runlim] sample:		2024.2 time, 2030.6 real, 1201.1 MB
[runlim] sample:		2034.2 time, 2040.6 real, 1201.2 MB
[runlim] sample:		2044.1 time, 2050.6 real, 1201.3 MB
[runlim] sample:		2054.1 time, 2060.6 real, 1201.4 MB
[runlim] sample:		2064.1 time, 2070.6 real, 1201.5 MB
[runlim] sample:		2074.1 time, 2080.6 real, 1201.6 MB
[runlim] sample:		2084.1 time, 2090.6 real, 1201.6 MB
[runlim] sample:		2094.1 time, 2100.6 real, 1206.1 MB
[runlim] sample:		2104.1 time, 2110.6 real, 1225.0 MB
[runlim] sample:		2114.0 time, 2120.6 real, 1223.2 MB
[runlim] sample:		2124.0 time, 2130.6 real, 1223.2 MB
[runlim] sample:		2134.0 time, 2140.6 real, 1223.2 MB
[runlim] sample:		2144.0 time, 2150.6 real, 1223.2 MB
[runlim] sample:		2154.0 time, 2160.6 real, 1223.2 MB
[runlim] sample:		2164.0 time, 2170.6 real, 1223.2 MB
[runlim] sample:		2173.9 time, 2180.6 real, 1223.2 MB
[runlim] sample:		2183.9 time, 2190.6 real, 1223.2 MB
[runlim] sample:		2193.9 time, 2200.6 real, 1223.2 MB
[runlim] sample:		2203.9 time, 2210.6 real, 1223.2 MB
[runlim] sample:		2213.9 time, 2220.6 real, 1231.1 MB
[runlim] sample:		2223.9 time, 2230.6 real, 1231.1 MB
[runlim] sample:		2233.8 time, 2240.6 real, 1231.1 MB
[runlim] sample:		2243.8 time, 2250.6 real, 1231.1 MB
[runlim] sample:		2253.8 time, 2260.6 real, 1231.1 MB
[runlim] sample:		2263.8 time, 2270.6 real, 1231.1 MB
[runlim] sample:		2273.8 time, 2280.6 real, 1231.1 MB
[runlim] sample:		2283.8 time, 2290.6 real, 1231.1 MB
[runlim] sample:		2293.8 time, 2300.6 real, 1231.1 MB
[runlim] sample:		2303.7 time, 2310.6 real, 1231.1 MB
[runlim] sample:		2313.7 time, 2320.6 real, 1231.1 MB
[runlim] sample:		2323.7 time, 2330.6 real, 1243.8 MB
[runlim] sample:		2333.7 time, 2340.6 real, 1243.8 MB
[runlim] sample:		2343.7 time, 2350.6 real, 1243.8 MB
[runlim] sample:		2353.7 time, 2360.6 real, 1243.8 MB
[runlim] sample:		2363.7 time, 2370.6 real, 1243.8 MB
[runlim] sample:		2373.6 time, 2380.6 real, 1243.8 MB
[runlim] sample:		2383.6 time, 2390.6 real, 1243.8 MB
[runlim] sample:		2393.6 time, 2400.6 real, 1243.8 MB
[runlim] sample:		2403.6 time, 2410.6 real, 1243.8 MB
[runlim] sample:		2413.6 time, 2420.6 real, 1243.8 MB
[runlim] sample:		2423.6 time, 2430.6 real, 1243.8 MB
[runlim] sample:		2433.6 time, 2440.6 real, 1254.2 MB
[runlim] sample:		2443.5 time, 2450.6 real, 1254.2 MB
[runlim] sample:		2453.5 time, 2460.6 real, 1254.2 MB
[runlim] sample:		2463.5 time, 2470.6 real, 1254.2 MB
[runlim] sample:		2473.5 time, 2480.6 real, 1254.2 MB
[runlim] sample:		2483.5 time, 2490.6 real, 1254.2 MB
[runlim] sample:		2493.5 time, 2500.6 real, 1254.2 MB
[runlim] sample:		2503.4 time, 2510.6 real, 1254.2 MB
[runlim] sample:		2513.4 time, 2520.6 real, 1254.2 MB
[runlim] sample:		2523.4 time, 2530.6 real, 1254.2 MB
[runlim] sample:		2533.4 time, 2540.6 real, 1254.2 MB
[runlim] sample:		2543.4 time, 2550.6 real, 1254.2 MB
[runlim] sample:		2553.4 time, 2560.6 real, 1268.3 MB
[runlim] sample:		2563.4 time, 2570.6 real, 1268.3 MB
[runlim] sample:		2573.3 time, 2580.6 real, 1268.3 MB
[runlim] sample:		2583.3 time, 2590.6 real, 1268.3 MB
[runlim] sample:		2593.3 time, 2600.6 real, 1268.3 MB
[runlim] sample:		2603.3 time, 2610.6 real, 1268.3 MB
[runlim] sample:		2613.3 time, 2620.6 real, 1268.3 MB
[runlim] sample:		2623.3 time, 2630.6 real, 1270.5 MB
[runlim] sample:		2633.2 time, 2640.6 real, 1270.5 MB
[runlim] sample:		2643.2 time, 2650.6 real, 1270.5 MB
[runlim] sample:		2653.2 time, 2660.6 real, 1270.5 MB
[runlim] sample:		2663.2 time, 2670.6 real, 1270.5 MB
[runlim] sample:		2673.2 time, 2680.6 real, 1278.7 MB
[runlim] sample:		2683.2 time, 2690.6 real, 1278.7 MB
[runlim] sample:		2693.2 time, 2700.6 real, 1278.7 MB
[runlim] sample:		2703.2 time, 2710.6 real, 1278.7 MB
[runlim] sample:		2713.1 time, 2720.6 real, 1281.0 MB
[runlim] sample:		2723.1 time, 2730.6 real, 1281.0 MB
[runlim] sample:		2733.1 time, 2740.6 real, 1281.0 MB
[runlim] sample:		2743.1 time, 2750.6 real, 1281.1 MB
[runlim] sample:		2753.1 time, 2760.6 real, 1281.1 MB
[runlim] sample:		2763.1 time, 2770.6 real, 1281.1 MB
[runlim] sample:		2773.0 time, 2780.6 real, 1281.1 MB
[runlim] sample:		2783.0 time, 2790.6 real, 1281.1 MB
[runlim] sample:		2793.0 time, 2800.6 real, 1287.4 MB
[runlim] sample:		2803.0 time, 2810.6 real, 1289.4 MB
[runlim] sample:		2813.0 time, 2820.6 real, 1289.4 MB
[runlim] sample:		2823.0 time, 2830.6 real, 1289.4 MB
[runlim] sample:		2833.0 time, 2840.6 real, 1289.4 MB
[runlim] sample:		2842.9 time, 2850.6 real, 1289.4 MB
[runlim] sample:		2852.9 time, 2860.6 real, 1289.4 MB
[runlim] sample:		2862.9 time, 2870.6 real, 1289.4 MB
[runlim] sample:		2872.9 time, 2880.6 real, 1289.4 MB
[runlim] sample:		2882.9 time, 2890.6 real, 1289.4 MB
[runlim] sample:		2892.9 time, 2900.6 real, 1289.4 MB
[runlim] sample:		2902.8 time, 2910.6 real, 1289.4 MB
[runlim] sample:		2912.8 time, 2920.6 real, 1289.7 MB
[runlim] sample:		2922.8 time, 2930.6 real, 1298.2 MB
[runlim] sample:		2932.8 time, 2940.6 real, 1300.2 MB
[runlim] sample:		2942.8 time, 2950.6 real, 1300.2 MB
[runlim] sample:		2952.8 time, 2960.6 real, 1303.6 MB
[runlim] sample:		2962.8 time, 2970.6 real, 1303.6 MB
[runlim] sample:		2972.7 time, 2980.6 real, 1303.6 MB
[runlim] sample:		2982.7 time, 2990.6 real, 1303.6 MB
[runlim] sample:		2992.7 time, 3000.6 real, 1307.0 MB
[runlim] sample:		3002.7 time, 3010.6 real, 1307.0 MB
[runlim] sample:		3012.7 time, 3020.6 real, 1307.0 MB
[runlim] sample:		3022.7 time, 3030.6 real, 1307.0 MB
[runlim] sample:		3032.7 time, 3040.6 real, 1307.0 MB
[runlim] sample:		3042.7 time, 3050.6 real, 1307.0 MB
[runlim] sample:		3052.6 time, 3060.6 real, 1330.2 MB
[runlim] sample:		3062.6 time, 3070.6 real, 1330.2 MB
[runlim] sample:		3072.6 time, 3080.6 real, 1330.2 MB
[runlim] sample:		3082.6 time, 3090.6 real, 1332.3 MB
[runlim] sample:		3092.6 time, 3100.6 real, 1332.3 MB
[runlim] sample:		3102.6 time, 3110.6 real, 1332.3 MB
[runlim] sample:		3112.5 time, 3120.6 real, 1332.3 MB
[runlim] sample:		3122.5 time, 3130.6 real, 1332.3 MB
[runlim] sample:		3132.5 time, 3140.6 real, 1332.3 MB
[runlim] sample:		3142.5 time, 3150.6 real, 1334.2 MB
[runlim] sample:		3152.5 time, 3160.6 real, 1334.2 MB
[runlim] sample:		3162.5 time, 3170.6 real, 1334.2 MB
[runlim] sample:		3172.4 time, 3180.6 real, 1334.2 MB
[runlim] sample:		3182.4 time, 3190.6 real, 1338.3 MB
[runlim] sample:		3192.4 time, 3200.6 real, 1338.4 MB
[runlim] sample:		3202.4 time, 3210.6 real, 1338.4 MB
[runlim] sample:		3212.4 time, 3220.6 real, 1338.4 MB
[runlim] sample:		3222.4 time, 3230.6 real, 1340.4 MB
[runlim] sample:		3232.4 time, 3240.6 real, 1340.4 MB
[runlim] sample:		3242.3 time, 3250.6 real, 1340.4 MB
[runlim] sample:		3252.3 time, 3260.6 real, 1340.4 MB
[runlim] sample:		3262.3 time, 3270.6 real, 1340.4 MB
[runlim] sample:		3272.3 time, 3280.6 real, 1340.6 MB
[runlim] sample:		3282.3 time, 3290.6 real, 1342.3 MB
[runlim] sample:		3292.3 time, 3300.6 real, 1342.3 MB
[runlim] sample:		3302.2 time, 3310.6 real, 1342.3 MB
[runlim] sample:		3312.2 time, 3320.6 real, 1342.3 MB
[runlim] sample:		3322.2 time, 3330.6 real, 1551.0 MB
[runlim] sample:		3332.2 time, 3340.6 real, 1550.5 MB
[runlim] sample:		3342.2 time, 3350.6 real, 1550.5 MB
[runlim] sample:		3352.2 time, 3360.6 real, 1550.5 MB
[runlim] sample:		3362.2 time, 3370.6 real, 1550.5 MB
[runlim] sample:		3372.2 time, 3380.6 real, 1552.5 MB
[runlim] sample:		3382.1 time, 3390.6 real, 1552.5 MB
[runlim] sample:		3392.1 time, 3400.6 real, 1552.5 MB
[runlim] sample:		3402.1 time, 3410.6 real, 1552.5 MB
[runlim] sample:		3412.1 time, 3420.6 real, 1553.5 MB
[runlim] sample:		3422.1 time, 3430.6 real, 1553.5 MB
[runlim] sample:		3432.0 time, 3440.6 real, 1554.4 MB
[runlim] sample:		3442.0 time, 3450.6 real, 1554.4 MB
[runlim] sample:		3452.0 time, 3460.6 real, 1554.4 MB
[runlim] sample:		3462.0 time, 3470.6 real, 1560.9 MB
[runlim] sample:		3472.0 time, 3480.6 real, 1560.6 MB
[runlim] sample:		3482.0 time, 3490.6 real, 1560.6 MB
[runlim] sample:		3492.0 time, 3500.6 real, 1560.6 MB
[runlim] sample:		3501.9 time, 3510.6 real, 1560.6 MB
[runlim] sample:		3511.9 time, 3520.6 real, 1560.6 MB
[runlim] sample:		3521.9 time, 3530.6 real, 1562.6 MB
[runlim] sample:		3531.9 time, 3540.6 real, 1562.6 MB
[runlim] sample:		3541.9 time, 3550.6 real, 1562.6 MB
[runlim] sample:		3551.9 time, 3560.6 real, 1562.6 MB
[runlim] sample:		3561.9 time, 3570.6 real, 1562.6 MB
[runlim] sample:		3571.8 time, 3580.6 real, 1563.0 MB
[runlim] sample:		3581.8 time, 3590.6 real, 1563.0 MB
[runlim] end:			Tue Sep 15 21:00:38 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		6
[runlim] real:			3600.19 seconds
[runlim] time:			3591.35 seconds
[runlim] space:			1580.2 MB
[runlim] samples:		35996
