[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/6s105.aig
[runlim] start:			Tue Sep 15 16:00:06 2015
[runlim] main pid:		27012
[runlim] sample:		0.0 time, 10.9 real, 0.2 MB
[runlim] sample:		9.5 time, 23.6 real, 371.5 MB
[runlim] sample:		19.5 time, 33.6 real, 384.6 MB
[runlim] sample:		29.5 time, 43.6 real, 421.3 MB
[runlim] sample:		39.5 time, 53.6 real, 391.1 MB
[runlim] sample:		49.5 time, 63.6 real, 427.3 MB
[runlim] sample:		59.4 time, 73.6 real, 469.3 MB
[runlim] sample:		69.4 time, 83.6 real, 507.2 MB
[runlim] sample:		79.4 time, 93.6 real, 379.5 MB
[runlim] sample:		89.4 time, 103.6 real, 413.5 MB
[runlim] sample:		99.4 time, 113.6 real, 447.5 MB
[runlim] sample:		109.4 time, 123.6 real, 487.5 MB
[runlim] sample:		119.3 time, 133.6 real, 523.5 MB
[runlim] sample:		129.3 time, 143.6 real, 559.5 MB
[runlim] sample:		139.3 time, 153.6 real, 587.4 MB
[runlim] sample:		149.3 time, 163.6 real, 393.9 MB
[runlim] sample:		159.3 time, 173.6 real, 405.8 MB
[runlim] sample:		169.3 time, 183.6 real, 438.4 MB
[runlim] sample:		179.2 time, 193.6 real, 477.1 MB
[runlim] sample:		189.2 time, 203.6 real, 509.6 MB
[runlim] sample:		199.2 time, 213.6 real, 545.8 MB
[runlim] sample:		209.2 time, 223.6 real, 413.8 MB
[runlim] sample:		219.2 time, 233.6 real, 469.8 MB
[runlim] sample:		229.2 time, 243.6 real, 523.8 MB
[runlim] sample:		239.2 time, 253.6 real, 557.8 MB
[runlim] sample:		249.2 time, 263.6 real, 589.7 MB
[runlim] sample:		259.1 time, 273.6 real, 621.9 MB
[runlim] sample:		269.1 time, 283.6 real, 648.3 MB
[runlim] sample:		279.1 time, 293.6 real, 405.0 MB
[runlim] sample:		289.1 time, 303.6 real, 435.2 MB
[runlim] sample:		299.1 time, 313.6 real, 465.3 MB
[runlim] sample:		309.1 time, 323.6 real, 497.2 MB
[runlim] sample:		319.1 time, 333.6 real, 529.4 MB
[runlim] sample:		329.0 time, 343.6 real, 405.4 MB
[runlim] sample:		339.0 time, 353.6 real, 453.4 MB
[runlim] sample:		349.0 time, 363.6 real, 503.4 MB
[runlim] sample:		359.0 time, 373.6 real, 545.4 MB
[runlim] sample:		369.0 time, 383.6 real, 575.3 MB
[runlim] sample:		379.0 time, 393.6 real, 609.3 MB
[runlim] sample:		388.9 time, 403.6 real, 643.4 MB
[runlim] sample:		398.9 time, 413.6 real, 675.4 MB
[runlim] sample:		408.9 time, 423.6 real, 709.3 MB
[runlim] sample:		418.9 time, 433.6 real, 741.3 MB
[runlim] sample:		428.9 time, 443.6 real, 398.7 MB
[runlim] sample:		438.9 time, 453.6 real, 420.9 MB
[runlim] sample:		448.9 time, 463.6 real, 449.0 MB
[runlim] sample:		458.8 time, 473.6 real, 489.5 MB
[runlim] sample:		468.8 time, 483.6 real, 511.5 MB
[runlim] sample:		478.8 time, 493.6 real, 395.5 MB
[runlim] sample:		488.8 time, 503.6 real, 439.5 MB
[runlim] sample:		498.8 time, 513.6 real, 497.5 MB
[runlim] sample:		508.8 time, 523.6 real, 525.5 MB
[runlim] sample:		518.8 time, 533.6 real, 555.5 MB
[runlim] sample:		528.7 time, 543.6 real, 589.4 MB
[runlim] sample:		538.7 time, 553.6 real, 627.5 MB
[runlim] sample:		548.7 time, 563.6 real, 663.5 MB
[runlim] sample:		558.7 time, 573.6 real, 704.9 MB
[runlim] sample:		568.7 time, 583.6 real, 461.2 MB
[runlim] sample:		578.7 time, 593.6 real, 501.2 MB
[runlim] sample:		588.6 time, 603.6 real, 543.4 MB
[runlim] sample:		598.6 time, 613.6 real, 599.4 MB
[runlim] sample:		608.6 time, 623.6 real, 645.7 MB
[runlim] sample:		618.6 time, 633.6 real, 691.7 MB
[runlim] sample:		628.6 time, 643.6 real, 737.7 MB
[runlim] sample:		638.6 time, 653.6 real, 771.8 MB
[runlim] sample:		648.5 time, 663.6 real, 799.8 MB
[runlim] sample:		658.5 time, 673.6 real, 450.0 MB
[runlim] sample:		668.5 time, 683.6 real, 509.6 MB
[runlim] sample:		678.5 time, 693.6 real, 565.6 MB
[runlim] sample:		688.5 time, 703.6 real, 605.5 MB
[runlim] sample:		698.5 time, 713.6 real, 647.6 MB
[runlim] sample:		708.5 time, 723.6 real, 683.6 MB
[runlim] sample:		718.5 time, 733.6 real, 711.5 MB
[runlim] sample:		728.4 time, 743.6 real, 739.5 MB
[runlim] sample:		738.4 time, 753.6 real, 777.4 MB
[runlim] sample:		748.4 time, 763.6 real, 825.4 MB
[runlim] sample:		758.4 time, 773.6 real, 859.7 MB
[runlim] sample:		768.4 time, 783.6 real, 426.3 MB
[runlim] sample:		778.4 time, 793.6 real, 423.6 MB
[runlim] sample:		788.4 time, 803.6 real, 457.8 MB
[runlim] sample:		798.3 time, 813.6 real, 489.6 MB
[runlim] sample:		808.3 time, 823.6 real, 519.5 MB
[runlim] sample:		818.3 time, 833.6 real, 545.5 MB
[runlim] sample:		828.3 time, 843.6 real, 575.5 MB
[runlim] sample:		838.3 time, 853.6 real, 599.4 MB
[runlim] sample:		848.3 time, 863.6 real, 447.6 MB
[runlim] sample:		858.2 time, 873.6 real, 499.6 MB
[runlim] sample:		868.2 time, 883.6 real, 541.5 MB
[runlim] sample:		878.2 time, 893.6 real, 579.5 MB
[runlim] sample:		888.2 time, 903.6 real, 623.4 MB
[runlim] sample:		898.2 time, 913.6 real, 657.6 MB
[runlim] sample:		908.2 time, 923.6 real, 695.6 MB
[runlim] sample:		918.2 time, 933.6 real, 733.5 MB
[runlim] sample:		928.1 time, 943.6 real, 765.5 MB
[runlim] sample:		938.1 time, 953.6 real, 787.7 MB
[runlim] sample:		948.1 time, 963.6 real, 813.7 MB
[runlim] sample:		958.1 time, 973.6 real, 839.7 MB
[runlim] sample:		968.1 time, 983.6 real, 441.6 MB
[runlim] sample:		978.1 time, 993.6 real, 495.6 MB
[runlim] sample:		988.0 time, 1003.6 real, 555.6 MB
[runlim] sample:		998.0 time, 1013.6 real, 605.5 MB
[runlim] sample:		1008.0 time, 1023.6 real, 655.7 MB
[runlim] sample:		1018.0 time, 1033.6 real, 699.7 MB
[runlim] sample:		1028.0 time, 1043.6 real, 731.6 MB
[runlim] sample:		1038.0 time, 1053.6 real, 761.6 MB
[runlim] sample:		1048.0 time, 1063.6 real, 793.6 MB
[runlim] sample:		1058.0 time, 1073.6 real, 829.7 MB
[runlim] sample:		1067.9 time, 1083.6 real, 869.7 MB
[runlim] sample:		1077.9 time, 1093.6 real, 455.5 MB
[runlim] sample:		1087.9 time, 1103.6 real, 481.5 MB
[runlim] sample:		1097.9 time, 1113.6 real, 521.7 MB
[runlim] sample:		1107.9 time, 1123.6 real, 546.2 MB
[runlim] sample:		1117.9 time, 1133.6 real, 574.2 MB
[runlim] sample:		1127.8 time, 1143.6 real, 598.1 MB
[runlim] sample:		1137.8 time, 1153.6 real, 430.0 MB
[runlim] sample:		1147.8 time, 1163.6 real, 483.5 MB
[runlim] sample:		1157.8 time, 1173.6 real, 523.4 MB
[runlim] sample:		1167.8 time, 1183.6 real, 557.6 MB
[runlim] sample:		1177.8 time, 1193.6 real, 591.9 MB
[runlim] sample:		1187.7 time, 1203.6 real, 633.9 MB
[runlim] sample:		1197.7 time, 1213.6 real, 669.9 MB
[runlim] sample:		1207.7 time, 1223.6 real, 702.3 MB
[runlim] sample:		1217.7 time, 1233.6 real, 730.5 MB
[runlim] sample:		1227.7 time, 1243.6 real, 762.7 MB
[runlim] sample:		1237.7 time, 1253.6 real, 798.9 MB
[runlim] sample:		1247.6 time, 1263.6 real, 461.0 MB
[runlim] sample:		1257.6 time, 1273.6 real, 509.0 MB
[runlim] sample:		1267.6 time, 1283.6 real, 555.0 MB
[runlim] sample:		1277.6 time, 1293.6 real, 603.1 MB
[runlim] sample:		1287.6 time, 1303.6 real, 653.3 MB
[runlim] sample:		1297.6 time, 1313.6 real, 691.5 MB
[runlim] sample:		1307.5 time, 1323.6 real, 731.5 MB
[runlim] sample:		1317.5 time, 1333.6 real, 765.5 MB
[runlim] sample:		1327.5 time, 1343.6 real, 793.6 MB
[runlim] sample:		1337.5 time, 1353.6 real, 823.8 MB
[runlim] sample:		1347.5 time, 1363.6 real, 856.0 MB
[runlim] sample:		1357.5 time, 1373.6 real, 902.0 MB
[runlim] sample:		1367.5 time, 1383.6 real, 464.9 MB
[runlim] sample:		1377.4 time, 1393.6 real, 504.4 MB
[runlim] sample:		1387.4 time, 1403.6 real, 542.4 MB
[runlim] sample:		1397.4 time, 1413.6 real, 574.4 MB
[runlim] sample:		1407.4 time, 1423.6 real, 612.3 MB
[runlim] sample:		1417.4 time, 1433.6 real, 646.5 MB
[runlim] sample:		1427.4 time, 1443.6 real, 678.7 MB
[runlim] sample:		1437.3 time, 1453.6 real, 712.9 MB
[runlim] sample:		1447.3 time, 1463.6 real, 744.9 MB
[runlim] sample:		1457.3 time, 1473.6 real, 777.1 MB
[runlim] sample:		1467.3 time, 1483.6 real, 809.1 MB
[runlim] sample:		1477.3 time, 1493.6 real, 845.2 MB
[runlim] sample:		1487.3 time, 1503.6 real, 881.2 MB
[runlim] sample:		1497.3 time, 1513.6 real, 916.4 MB
[runlim] sample:		1507.2 time, 1523.6 real, 950.4 MB
[runlim] sample:		1517.2 time, 1533.6 real, 506.3 MB
[runlim] sample:		1527.2 time, 1543.6 real, 566.2 MB
[runlim] sample:		1537.2 time, 1553.6 real, 628.2 MB
[runlim] sample:		1547.2 time, 1563.6 real, 436.2 MB
[runlim] sample:		1557.2 time, 1573.6 real, 462.2 MB
[runlim] sample:		1567.2 time, 1583.6 real, 490.2 MB
[runlim] sample:		1577.2 time, 1593.6 real, 516.4 MB
[runlim] sample:		1587.1 time, 1603.6 real, 542.6 MB
[runlim] sample:		1597.1 time, 1613.6 real, 564.9 MB
[runlim] sample:		1607.1 time, 1623.6 real, 443.0 MB
[runlim] sample:		1617.1 time, 1633.6 real, 481.0 MB
[runlim] sample:		1627.1 time, 1643.6 real, 511.1 MB
[runlim] sample:		1637.1 time, 1653.6 real, 541.2 MB
[runlim] sample:		1647.0 time, 1663.6 real, 569.4 MB
[runlim] sample:		1657.0 time, 1673.6 real, 599.1 MB
[runlim] sample:		1667.0 time, 1683.6 real, 631.6 MB
[runlim] sample:		1677.0 time, 1693.6 real, 657.8 MB
[runlim] sample:		1687.0 time, 1703.6 real, 684.0 MB
[runlim] sample:		1697.0 time, 1713.6 real, 434.2 MB
[runlim] sample:		1707.0 time, 1723.6 real, 480.2 MB
[runlim] sample:		1716.9 time, 1733.6 real, 519.1 MB
[runlim] sample:		1726.9 time, 1743.6 real, 564.2 MB
[runlim] sample:		1736.9 time, 1753.6 real, 610.3 MB
[runlim] sample:		1746.9 time, 1763.6 real, 644.3 MB
[runlim] sample:		1756.9 time, 1773.6 real, 670.5 MB
[runlim] sample:		1766.9 time, 1783.6 real, 694.7 MB
[runlim] sample:		1776.8 time, 1793.6 real, 722.9 MB
[runlim] sample:		1786.8 time, 1803.6 real, 749.1 MB
[runlim] sample:		1796.8 time, 1813.6 real, 773.4 MB
[runlim] sample:		1806.8 time, 1823.6 real, 797.6 MB
[runlim] sample:		1816.8 time, 1833.6 real, 433.5 MB
[runlim] sample:		1826.8 time, 1843.6 real, 479.6 MB
[runlim] sample:		1836.8 time, 1853.6 real, 519.6 MB
[runlim] sample:		1846.8 time, 1863.6 real, 565.6 MB
[runlim] sample:		1856.7 time, 1873.6 real, 611.5 MB
[runlim] sample:		1866.7 time, 1883.6 real, 643.7 MB
[runlim] sample:		1876.7 time, 1893.6 real, 677.7 MB
[runlim] sample:		1886.7 time, 1903.6 real, 713.7 MB
[runlim] sample:		1896.7 time, 1913.6 real, 743.6 MB
[runlim] sample:		1906.7 time, 1923.6 real, 773.8 MB
[runlim] sample:		1916.7 time, 1933.6 real, 805.8 MB
[runlim] sample:		1926.6 time, 1943.6 real, 839.9 MB
[runlim] sample:		1936.6 time, 1953.6 real, 866.1 MB
[runlim] sample:		1946.6 time, 1963.6 real, 896.3 MB
[runlim] sample:		1956.6 time, 1973.6 real, 450.6 MB
[runlim] sample:		1966.6 time, 1983.6 real, 512.6 MB
[runlim] sample:		1976.5 time, 1993.6 real, 558.5 MB
[runlim] sample:		1986.5 time, 2003.6 real, 608.4 MB
[runlim] sample:		1996.5 time, 2013.6 real, 656.6 MB
[runlim] sample:		2006.5 time, 2023.6 real, 706.6 MB
[runlim] sample:		2016.5 time, 2033.6 real, 756.5 MB
[runlim] sample:		2026.5 time, 2043.6 real, 792.7 MB
[runlim] sample:		2036.5 time, 2053.6 real, 834.7 MB
[runlim] sample:		2046.5 time, 2063.6 real, 880.8 MB
[runlim] sample:		2056.4 time, 2073.6 real, 926.8 MB
[runlim] sample:		2066.4 time, 2083.6 real, 974.7 MB
[runlim] sample:		2076.4 time, 2093.6 real, 1025.0 MB
[runlim] sample:		2086.4 time, 2103.6 real, 1069.0 MB
[runlim] sample:		2096.4 time, 2113.6 real, 1107.2 MB
[runlim] sample:		2106.4 time, 2123.6 real, 1135.4 MB
[runlim] sample:		2116.3 time, 2133.6 real, 1171.8 MB
[runlim] sample:		2126.3 time, 2143.6 real, 491.0 MB
[runlim] sample:		2136.3 time, 2153.6 real, 539.2 MB
[runlim] sample:		2146.3 time, 2163.6 real, 595.2 MB
[runlim] sample:		2156.3 time, 2173.6 real, 641.2 MB
[runlim] sample:		2166.3 time, 2183.6 real, 691.2 MB
[runlim] sample:		2176.3 time, 2193.6 real, 731.4 MB
[runlim] sample:		2186.2 time, 2203.6 real, 773.2 MB
[runlim] sample:		2196.2 time, 2213.6 real, 813.2 MB
[runlim] sample:		2206.2 time, 2223.6 real, 851.3 MB
[runlim] sample:		2216.2 time, 2233.6 real, 903.3 MB
[runlim] sample:		2226.2 time, 2243.6 real, 941.4 MB
[runlim] sample:		2236.2 time, 2253.6 real, 971.4 MB
[runlim] sample:		2246.2 time, 2263.6 real, 1001.4 MB
[runlim] sample:		2256.1 time, 2273.6 real, 1033.5 MB
[runlim] sample:		2266.1 time, 2283.6 real, 1065.7 MB
[runlim] sample:		2276.1 time, 2293.6 real, 1097.7 MB
[runlim] sample:		2286.1 time, 2303.6 real, 1127.9 MB
[runlim] sample:		2296.1 time, 2313.6 real, 1160.0 MB
[runlim] sample:		2306.1 time, 2323.6 real, 522.8 MB
[runlim] sample:		2316.1 time, 2333.6 real, 570.8 MB
[runlim] sample:		2326.0 time, 2343.6 real, 620.7 MB
[runlim] sample:		2336.0 time, 2353.6 real, 672.7 MB
[runlim] sample:		2346.0 time, 2363.6 real, 726.8 MB
[runlim] sample:		2356.0 time, 2373.6 real, 776.7 MB
[runlim] sample:		2366.0 time, 2383.6 real, 832.9 MB
[runlim] sample:		2376.0 time, 2393.6 real, 891.0 MB
[runlim] sample:		2385.9 time, 2403.6 real, 925.2 MB
[runlim] sample:		2395.9 time, 2413.6 real, 973.2 MB
[runlim] sample:		2405.9 time, 2423.6 real, 1013.3 MB
[runlim] sample:		2415.9 time, 2433.6 real, 1055.5 MB
[runlim] sample:		2425.9 time, 2443.6 real, 1093.5 MB
[runlim] sample:		2435.9 time, 2453.6 real, 1127.6 MB
[runlim] sample:		2445.9 time, 2463.6 real, 1159.8 MB
[runlim] sample:		2455.8 time, 2473.6 real, 457.4 MB
[runlim] sample:		2465.8 time, 2483.6 real, 485.3 MB
[runlim] sample:		2475.8 time, 2493.6 real, 511.5 MB
[runlim] sample:		2485.8 time, 2503.6 real, 549.6 MB
[runlim] sample:		2495.8 time, 2513.6 real, 577.8 MB
[runlim] sample:		2505.8 time, 2523.6 real, 603.9 MB
[runlim] sample:		2515.8 time, 2533.6 real, 436.6 MB
[runlim] sample:		2525.7 time, 2543.6 real, 488.8 MB
[runlim] sample:		2535.7 time, 2553.6 real, 538.8 MB
[runlim] sample:		2545.7 time, 2563.6 real, 566.8 MB
[runlim] sample:		2555.7 time, 2573.6 real, 598.9 MB
[runlim] sample:		2565.7 time, 2583.6 real, 630.9 MB
[runlim] sample:		2575.7 time, 2593.6 real, 662.9 MB
[runlim] sample:		2585.7 time, 2603.6 real, 691.3 MB
[runlim] sample:		2595.6 time, 2613.6 real, 723.3 MB
[runlim] sample:		2605.6 time, 2623.6 real, 751.5 MB
[runlim] sample:		2615.6 time, 2633.6 real, 489.5 MB
[runlim] sample:		2625.6 time, 2643.6 real, 539.4 MB
[runlim] sample:		2635.6 time, 2653.6 real, 579.4 MB
[runlim] sample:		2645.6 time, 2663.6 real, 637.6 MB
[runlim] sample:		2655.6 time, 2673.6 real, 681.6 MB
[runlim] sample:		2665.5 time, 2683.6 real, 719.7 MB
[runlim] sample:		2675.5 time, 2693.6 real, 757.7 MB
[runlim] sample:		2685.5 time, 2703.6 real, 797.8 MB
[runlim] sample:		2695.5 time, 2713.6 real, 834.0 MB
[runlim] sample:		2705.5 time, 2723.6 real, 870.1 MB
[runlim] sample:		2715.4 time, 2733.6 real, 906.2 MB
[runlim] sample:		2725.4 time, 2743.6 real, 500.6 MB
[runlim] sample:		2735.4 time, 2753.6 real, 550.6 MB
[runlim] sample:		2745.4 time, 2763.6 real, 605.8 MB
[runlim] sample:		2755.4 time, 2773.6 real, 647.6 MB
[runlim] sample:		2765.4 time, 2783.6 real, 695.8 MB
[runlim] sample:		2775.4 time, 2793.6 real, 736.4 MB
[runlim] sample:		2785.3 time, 2803.6 real, 773.9 MB
[runlim] sample:		2795.3 time, 2813.6 real, 811.9 MB
[runlim] sample:		2805.3 time, 2823.6 real, 847.9 MB
[runlim] sample:		2815.3 time, 2833.6 real, 887.9 MB
[runlim] sample:		2825.3 time, 2843.6 real, 920.1 MB
[runlim] sample:		2835.3 time, 2853.6 real, 954.1 MB
[runlim] sample:		2845.2 time, 2863.6 real, 990.1 MB
[runlim] sample:		2855.2 time, 2873.6 real, 1026.2 MB
[runlim] sample:		2865.2 time, 2883.6 real, 451.5 MB
[runlim] sample:		2875.2 time, 2893.6 real, 498.0 MB
[runlim] sample:		2885.2 time, 2903.6 real, 531.9 MB
[runlim] sample:		2895.2 time, 2913.6 real, 579.9 MB
[runlim] sample:		2905.2 time, 2923.6 real, 629.9 MB
[runlim] sample:		2915.2 time, 2933.6 real, 676.0 MB
[runlim] sample:		2925.1 time, 2943.6 real, 726.2 MB
[runlim] sample:		2935.1 time, 2953.6 real, 776.2 MB
[runlim] sample:		2945.1 time, 2963.6 real, 824.3 MB
[runlim] sample:		2955.1 time, 2973.6 real, 872.5 MB
[runlim] sample:		2965.1 time, 2983.6 real, 914.7 MB
[runlim] sample:		2975.1 time, 2993.6 real, 954.6 MB
[runlim] sample:		2985.1 time, 3003.6 real, 988.8 MB
[runlim] sample:		2995.0 time, 3013.6 real, 1016.8 MB
[runlim] sample:		3005.0 time, 3023.6 real, 1037.2 MB
[runlim] sample:		3015.0 time, 3033.6 real, 451.4 MB
[runlim] sample:		3025.0 time, 3043.6 real, 501.4 MB
[runlim] sample:		3035.0 time, 3053.6 real, 541.4 MB
[runlim] sample:		3045.0 time, 3063.6 real, 589.4 MB
[runlim] sample:		3054.9 time, 3073.6 real, 627.6 MB
[runlim] sample:		3064.9 time, 3083.6 real, 659.6 MB
[runlim] sample:		3074.9 time, 3093.6 real, 693.6 MB
[runlim] sample:		3084.9 time, 3103.6 real, 727.6 MB
[runlim] sample:		3094.9 time, 3113.6 real, 763.4 MB
[runlim] sample:		3104.9 time, 3123.6 real, 811.6 MB
[runlim] sample:		3114.9 time, 3133.6 real, 865.6 MB
[runlim] sample:		3124.8 time, 3143.6 real, 897.6 MB
[runlim] sample:		3134.8 time, 3153.6 real, 931.6 MB
[runlim] sample:		3144.8 time, 3163.6 real, 969.6 MB
[runlim] sample:		3154.8 time, 3173.6 real, 1005.6 MB
[runlim] sample:		3164.8 time, 3183.6 real, 1037.7 MB
[runlim] sample:		3174.8 time, 3193.6 real, 488.8 MB
[runlim] sample:		3184.8 time, 3203.6 real, 553.0 MB
[runlim] sample:		3194.7 time, 3213.6 real, 607.0 MB
[runlim] sample:		3204.7 time, 3223.6 real, 664.9 MB
[runlim] sample:		3214.7 time, 3233.6 real, 703.0 MB
[runlim] sample:		3224.7 time, 3243.6 real, 762.9 MB
[runlim] sample:		3234.7 time, 3253.6 real, 790.9 MB
[runlim] sample:		3244.7 time, 3263.6 real, 828.9 MB
[runlim] sample:		3254.7 time, 3273.6 real, 885.0 MB
[runlim] sample:		3264.6 time, 3283.6 real, 947.0 MB
[runlim] sample:		3274.6 time, 3293.6 real, 989.1 MB
[runlim] sample:		3284.6 time, 3303.6 real, 1027.2 MB
[runlim] sample:		3294.6 time, 3313.6 real, 1061.2 MB
[runlim] sample:		3304.6 time, 3323.6 real, 1089.4 MB
[runlim] sample:		3314.6 time, 3333.6 real, 1115.6 MB
[runlim] sample:		3324.6 time, 3343.6 real, 1145.6 MB
[runlim] sample:		3334.5 time, 3353.6 real, 1175.7 MB
[runlim] sample:		3344.5 time, 3363.6 real, 1209.7 MB
[runlim] sample:		3354.5 time, 3373.6 real, 1245.8 MB
[runlim] sample:		3364.5 time, 3383.6 real, 476.9 MB
[runlim] sample:		3374.5 time, 3393.6 real, 528.9 MB
[runlim] sample:		3384.5 time, 3403.6 real, 574.8 MB
[runlim] sample:		3394.4 time, 3413.6 real, 618.7 MB
[runlim] sample:		3404.4 time, 3423.6 real, 662.9 MB
[runlim] sample:		3414.4 time, 3433.6 real, 700.9 MB
[runlim] sample:		3424.4 time, 3443.6 real, 738.9 MB
[runlim] sample:		3434.4 time, 3453.6 real, 778.8 MB
[runlim] sample:		3444.4 time, 3463.6 real, 814.9 MB
[runlim] sample:		3454.3 time, 3473.6 real, 852.9 MB
[runlim] sample:		3464.3 time, 3483.6 real, 900.9 MB
[runlim] sample:		3474.3 time, 3493.6 real, 941.0 MB
[runlim] sample:		3484.3 time, 3503.6 real, 977.2 MB
[runlim] sample:		3494.3 time, 3513.6 real, 1011.2 MB
[runlim] sample:		3504.3 time, 3523.6 real, 1047.3 MB
[runlim] sample:		3514.3 time, 3533.6 real, 1085.3 MB
[runlim] sample:		3524.3 time, 3543.6 real, 1123.5 MB
[runlim] sample:		3534.2 time, 3553.6 real, 1167.6 MB
[runlim] sample:		3544.2 time, 3563.6 real, 1204.1 MB
[runlim] sample:		3554.2 time, 3573.6 real, 515.5 MB
[runlim] sample:		3564.2 time, 3583.6 real, 448.2 MB
[runlim] sample:		3574.2 time, 3593.6 real, 470.1 MB
[runlim] end:			Tue Sep 15 17:00:06 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		14
[runlim] real:			3600.22 seconds
[runlim] time:			3580.69 seconds
[runlim] space:			1262.1 MB
[runlim] samples:		35966
