[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/avy/single.avy
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/6s359r.aig
[runlim] start:			Sun Sep 20 14:37:02 2015
[runlim] main pid:		10199
[runlim] sample:		33.2 time, 10.3 real, 156.7 MB
[runlim] sample:		72.8 time, 20.3 real, 183.6 MB
[runlim] sample:		112.4 time, 30.3 real, 195.8 MB
[runlim] sample:		152.0 time, 40.3 real, 202.5 MB
[runlim] sample:		191.6 time, 50.3 real, 221.9 MB
[runlim] sample:		231.1 time, 60.3 real, 247.2 MB
[runlim] sample:		270.6 time, 70.3 real, 252.0 MB
[runlim] sample:		310.2 time, 80.3 real, 261.9 MB
[runlim] sample:		349.7 time, 90.3 real, 266.0 MB
[runlim] sample:		389.2 time, 100.3 real, 272.1 MB
[runlim] sample:		428.7 time, 110.3 real, 280.6 MB
[runlim] sample:		468.3 time, 120.3 real, 284.7 MB
[runlim] sample:		507.9 time, 130.3 real, 325.2 MB
[runlim] sample:		547.5 time, 140.3 real, 298.2 MB
[runlim] sample:		587.1 time, 150.3 real, 338.2 MB
[runlim] sample:		626.6 time, 160.3 real, 304.6 MB
[runlim] sample:		666.2 time, 170.3 real, 309.2 MB
[runlim] sample:		705.8 time, 180.3 real, 353.7 MB
[runlim] sample:		745.4 time, 190.3 real, 316.2 MB
[runlim] sample:		784.9 time, 200.3 real, 319.2 MB
[runlim] sample:		824.5 time, 210.3 real, 362.8 MB
[runlim] sample:		864.1 time, 220.3 real, 327.3 MB
[runlim] sample:		903.6 time, 230.3 real, 365.8 MB
[runlim] sample:		943.2 time, 240.3 real, 380.8 MB
[runlim] sample:		982.7 time, 250.3 real, 344.6 MB
[runlim] sample:		1022.3 time, 260.3 real, 348.9 MB
[runlim] sample:		1061.8 time, 270.3 real, 392.4 MB
[runlim] sample:		1101.4 time, 280.3 real, 402.6 MB
[runlim] sample:		1140.9 time, 290.3 real, 350.9 MB
[runlim] sample:		1180.5 time, 300.3 real, 351.4 MB
[runlim] sample:		1220.0 time, 310.3 real, 388.5 MB
[runlim] sample:		1259.5 time, 320.3 real, 399.0 MB
[runlim] sample:		1299.1 time, 330.3 real, 409.2 MB
[runlim] sample:		1338.7 time, 340.3 real, 353.8 MB
[runlim] sample:		1378.2 time, 350.3 real, 396.0 MB
[runlim] sample:		1417.8 time, 360.3 real, 408.2 MB
[runlim] sample:		1457.4 time, 370.3 real, 416.7 MB
[runlim] sample:		1496.9 time, 380.3 real, 357.0 MB
[runlim] sample:		1536.4 time, 390.3 real, 357.6 MB
[runlim] sample:		1576.0 time, 400.3 real, 397.8 MB
[runlim] sample:		1615.5 time, 410.3 real, 407.0 MB
[runlim] sample:		1655.1 time, 420.3 real, 415.3 MB
[runlim] sample:		1694.7 time, 430.3 real, 427.5 MB
[runlim] sample:		1734.2 time, 440.3 real, 360.1 MB
[runlim] sample:		1773.7 time, 450.3 real, 398.6 MB
[runlim] sample:		1813.3 time, 460.3 real, 406.6 MB
[runlim] sample:		1852.8 time, 470.3 real, 418.8 MB
[runlim] sample:		1892.4 time, 480.3 real, 429.1 MB
[runlim] sample:		1931.9 time, 490.3 real, 369.9 MB
[runlim] sample:		1971.5 time, 500.3 real, 408.8 MB
[runlim] sample:		2011.1 time, 510.3 real, 417.1 MB
[runlim] sample:		2050.6 time, 520.3 real, 427.3 MB
[runlim] sample:		2090.1 time, 530.3 real, 435.6 MB
[runlim] sample:		2129.7 time, 540.3 real, 443.9 MB
[runlim] sample:		2169.2 time, 550.3 real, 454.2 MB
[runlim] sample:		2208.7 time, 560.3 real, 376.6 MB
[runlim] sample:		2248.3 time, 570.3 real, 412.9 MB
[runlim] sample:		2287.8 time, 580.3 real, 423.1 MB
[runlim] sample:		2327.4 time, 590.3 real, 433.4 MB
[runlim] sample:		2367.0 time, 600.3 real, 443.6 MB
[runlim] sample:		2406.5 time, 610.3 real, 453.9 MB
[runlim] sample:		2446.1 time, 620.3 real, 378.4 MB
[runlim] sample:		2485.7 time, 630.3 real, 412.9 MB
[runlim] sample:		2525.3 time, 640.3 real, 425.2 MB
[runlim] sample:		2564.8 time, 650.3 real, 433.2 MB
[runlim] sample:		2604.4 time, 660.3 real, 443.4 MB
[runlim] sample:		2643.9 time, 670.3 real, 451.7 MB
[runlim] sample:		2683.5 time, 680.3 real, 380.0 MB
[runlim] sample:		2723.0 time, 690.3 real, 380.2 MB
[runlim] sample:		2762.6 time, 700.3 real, 420.5 MB
[runlim] sample:		2802.2 time, 710.3 real, 430.7 MB
[runlim] sample:		2841.8 time, 720.3 real, 448.9 MB
[runlim] sample:		2881.3 time, 730.3 real, 473.3 MB
[runlim] sample:		2920.8 time, 740.3 real, 494.5 MB
[runlim] sample:		2960.3 time, 750.3 real, 502.7 MB
[runlim] sample:		2999.9 time, 760.3 real, 509.0 MB
[runlim] sample:		3039.4 time, 770.3 real, 436.8 MB
[runlim] sample:		3079.0 time, 780.3 real, 499.7 MB
[runlim] sample:		3118.5 time, 790.3 real, 509.4 MB
[runlim] sample:		3158.0 time, 800.3 real, 526.7 MB
[runlim] sample:		3197.6 time, 810.3 real, 536.7 MB
[runlim] sample:		3237.1 time, 820.3 real, 575.7 MB
[runlim] sample:		3276.6 time, 830.3 real, 586.0 MB
[runlim] sample:		3316.1 time, 840.3 real, 496.2 MB
[runlim] sample:		3355.7 time, 850.3 real, 530.5 MB
[runlim] sample:		3395.3 time, 860.3 real, 538.5 MB
[runlim] sample:		3434.8 time, 870.3 real, 553.0 MB
[runlim] sample:		3474.3 time, 880.3 real, 563.2 MB
[runlim] sample:		3513.9 time, 890.3 real, 574.2 MB
[runlim] sample:		3553.4 time, 900.3 real, 583.0 MB
[runlim] sample:		3593.0 time, 910.3 real, 591.8 MB
[runlim] sample:		3632.5 time, 920.3 real, 600.5 MB
[runlim] sample:		3672.1 time, 930.3 real, 608.8 MB
[runlim] sample:		3711.6 time, 940.3 real, 530.1 MB
[runlim] sample:		3751.0 time, 950.3 real, 568.4 MB
[runlim] sample:		3790.5 time, 960.3 real, 578.6 MB
[runlim] sample:		3830.0 time, 970.3 real, 587.1 MB
[runlim] sample:		3869.6 time, 980.3 real, 597.6 MB
[runlim] sample:		3909.1 time, 990.3 real, 607.6 MB
[runlim] sample:		3948.6 time, 1000.3 real, 679.4 MB
[runlim] sample:		3988.2 time, 1010.3 real, 687.4 MB
[runlim] sample:		4027.6 time, 1020.3 real, 693.8 MB
[runlim] sample:		4067.2 time, 1030.3 real, 700.1 MB
[runlim] sample:		4106.8 time, 1040.3 real, 708.3 MB
[runlim] sample:		4146.3 time, 1050.3 real, 598.6 MB
[runlim] sample:		4185.8 time, 1060.3 real, 640.9 MB
[runlim] sample:		4225.4 time, 1070.3 real, 653.1 MB
[runlim] sample:		4264.9 time, 1080.3 real, 665.9 MB
[runlim] sample:		4304.4 time, 1090.3 real, 674.1 MB
[runlim] sample:		4343.9 time, 1100.3 real, 684.4 MB
[runlim] sample:		4383.4 time, 1110.3 real, 692.4 MB
[runlim] sample:		4422.9 time, 1120.3 real, 698.6 MB
[runlim] sample:		4462.5 time, 1130.3 real, 706.9 MB
[runlim] sample:		4501.9 time, 1140.3 real, 715.2 MB
[runlim] sample:		4541.5 time, 1150.3 real, 761.5 MB
[runlim] sample:		4581.1 time, 1160.3 real, 767.5 MB
[runlim] sample:		4620.6 time, 1170.3 real, 653.8 MB
[runlim] sample:		4660.1 time, 1180.3 real, 686.1 MB
[runlim] sample:		4699.6 time, 1190.3 real, 698.4 MB
[runlim] sample:		4739.2 time, 1200.3 real, 708.3 MB
[runlim] sample:		4778.7 time, 1210.3 real, 719.1 MB
[runlim] sample:		4818.3 time, 1220.3 real, 746.6 MB
[runlim] sample:		4857.8 time, 1230.3 real, 737.1 MB
[runlim] sample:		4897.4 time, 1240.3 real, 746.4 MB
[runlim] sample:		4936.9 time, 1250.3 real, 755.0 MB
[runlim] sample:		4976.4 time, 1260.3 real, 765.3 MB
[runlim] sample:		5016.0 time, 1270.3 real, 772.1 MB
[runlim] sample:		5055.5 time, 1280.3 real, 780.6 MB
[runlim] sample:		5095.1 time, 1290.3 real, 663.2 MB
[runlim] sample:		5134.6 time, 1300.3 real, 699.4 MB
[runlim] sample:		5174.1 time, 1310.3 real, 713.7 MB
[runlim] sample:		5213.6 time, 1320.3 real, 736.2 MB
[runlim] sample:		5253.1 time, 1330.3 real, 744.9 MB
[runlim] sample:		5292.6 time, 1340.3 real, 754.9 MB
[runlim] sample:		5332.2 time, 1350.3 real, 768.5 MB
[runlim] sample:		5371.7 time, 1360.3 real, 779.0 MB
[runlim] sample:		5411.2 time, 1370.3 real, 787.0 MB
[runlim] sample:		5450.8 time, 1380.3 real, 799.0 MB
[runlim] sample:		5490.4 time, 1390.3 real, 805.3 MB
[runlim] sample:		5529.9 time, 1400.3 real, 811.5 MB
[runlim] sample:		5569.5 time, 1410.3 real, 816.4 MB
[runlim] sample:		5609.0 time, 1420.3 real, 690.5 MB
[runlim] sample:		5648.5 time, 1430.3 real, 733.1 MB
[runlim] sample:		5688.0 time, 1440.3 real, 741.7 MB
[runlim] sample:		5727.6 time, 1450.3 real, 754.3 MB
[runlim] sample:		5767.1 time, 1460.3 real, 764.3 MB
[runlim] sample:		5806.6 time, 1470.3 real, 774.8 MB
[runlim] sample:		5846.2 time, 1480.3 real, 785.1 MB
[runlim] sample:		5885.7 time, 1490.3 real, 793.6 MB
[runlim] sample:		5925.2 time, 1500.3 real, 800.6 MB
[runlim] sample:		5964.8 time, 1510.3 real, 806.6 MB
[runlim] sample:		6004.2 time, 1520.3 real, 816.5 MB
[runlim] sample:		6043.8 time, 1530.3 real, 822.8 MB
[runlim] sample:		6083.3 time, 1540.3 real, 829.3 MB
[runlim] sample:		6122.8 time, 1550.3 real, 704.1 MB
[runlim] sample:		6162.3 time, 1560.3 real, 901.5 MB
[runlim] sample:		6201.8 time, 1570.3 real, 909.5 MB
[runlim] sample:		6241.4 time, 1580.3 real, 919.5 MB
[runlim] sample:		6280.9 time, 1590.3 real, 928.0 MB
[runlim] sample:		6320.5 time, 1600.3 real, 936.0 MB
[runlim] sample:		6360.0 time, 1610.3 real, 944.2 MB
[runlim] sample:		6399.5 time, 1620.3 real, 954.8 MB
[runlim] sample:		6439.1 time, 1630.3 real, 967.3 MB
[runlim] sample:		6478.6 time, 1640.3 real, 977.3 MB
[runlim] sample:		6518.1 time, 1650.3 real, 989.5 MB
[runlim] sample:		6557.6 time, 1660.3 real, 997.5 MB
[runlim] sample:		6597.1 time, 1670.3 real, 1006.0 MB
[runlim] sample:		6636.7 time, 1680.3 real, 904.6 MB
[runlim] sample:		6676.2 time, 1690.3 real, 920.5 MB
[runlim] sample:		6715.7 time, 1700.3 real, 932.8 MB
[runlim] sample:		6755.2 time, 1710.3 real, 941.3 MB
[runlim] sample:		6794.7 time, 1720.3 real, 952.1 MB
[runlim] sample:		6834.2 time, 1730.3 real, 958.3 MB
[runlim] sample:		6873.7 time, 1740.3 real, 962.8 MB
[runlim] sample:		6913.3 time, 1750.3 real, 969.1 MB
[runlim] sample:		6952.8 time, 1760.3 real, 971.3 MB
[runlim] sample:		6992.4 time, 1770.3 real, 975.6 MB
[runlim] sample:		7031.9 time, 1780.3 real, 869.9 MB
[runlim] sample:		7071.5 time, 1790.3 real, 870.1 MB
[runlim] sample:		7111.0 time, 1800.3 real, 870.1 MB
[runlim] sample:		7150.6 time, 1810.3 real, 904.7 MB
[runlim] sample:		7190.1 time, 1820.3 real, 911.5 MB
[runlim] sample:		7229.7 time, 1830.3 real, 915.8 MB
[runlim] sample:		7269.2 time, 1840.3 real, 919.8 MB
[runlim] sample:		7308.8 time, 1850.3 real, 924.0 MB
[runlim] sample:		7348.3 time, 1860.3 real, 926.0 MB
[runlim] sample:		7387.9 time, 1870.3 real, 931.0 MB
[runlim] sample:		7427.5 time, 1880.3 real, 937.3 MB
[runlim] sample:		7467.0 time, 1890.3 real, 941.3 MB
[runlim] sample:		7506.5 time, 1900.3 real, 943.5 MB
[runlim] sample:		7546.1 time, 1910.3 real, 947.5 MB
[runlim] sample:		7585.7 time, 1920.3 real, 875.8 MB
[runlim] sample:		7625.2 time, 1930.3 real, 875.8 MB
[runlim] sample:		7664.8 time, 1940.3 real, 910.6 MB
[runlim] sample:		7704.3 time, 1950.3 real, 916.6 MB
[runlim] sample:		7743.9 time, 1960.3 real, 926.7 MB
[runlim] sample:		7783.4 time, 1970.3 real, 932.6 MB
[runlim] sample:		7823.0 time, 1980.3 real, 936.6 MB
[runlim] sample:		7862.5 time, 1990.3 real, 944.9 MB
[runlim] sample:		7902.0 time, 2000.3 real, 948.9 MB
[runlim] sample:		7941.6 time, 2010.3 real, 955.1 MB
[runlim] sample:		7981.1 time, 2020.3 real, 959.1 MB
[runlim] sample:		8020.7 time, 2030.3 real, 963.8 MB
[runlim] sample:		8060.2 time, 2040.3 real, 881.9 MB
[runlim] sample:		8099.8 time, 2050.3 real, 882.1 MB
[runlim] sample:		8139.3 time, 2060.3 real, 882.2 MB
[runlim] sample:		8178.8 time, 2070.3 real, 917.9 MB
[runlim] sample:		8218.4 time, 2080.3 real, 923.9 MB
[runlim] sample:		8257.9 time, 2090.3 real, 929.9 MB
[runlim] sample:		8297.4 time, 2100.3 real, 938.1 MB
[runlim] sample:		8337.0 time, 2110.3 real, 948.6 MB
[runlim] sample:		8376.4 time, 2120.3 real, 954.9 MB
[runlim] sample:		8416.0 time, 2130.3 real, 962.9 MB
[runlim] sample:		8455.5 time, 2140.3 real, 969.1 MB
[runlim] sample:		8495.0 time, 2150.3 real, 975.7 MB
[runlim] sample:		8534.6 time, 2160.3 real, 981.9 MB
[runlim] sample:		8574.1 time, 2170.3 real, 988.7 MB
[runlim] sample:		8613.7 time, 2180.3 real, 992.9 MB
[runlim] sample:		8653.2 time, 2190.3 real, 889.0 MB
[runlim] sample:		8692.7 time, 2200.3 real, 889.5 MB
[runlim] sample:		8732.3 time, 2210.3 real, 923.5 MB
[runlim] sample:		8771.8 time, 2220.3 real, 930.0 MB
[runlim] sample:		8811.4 time, 2230.3 real, 935.0 MB
[runlim] sample:		8850.9 time, 2240.3 real, 939.0 MB
[runlim] sample:		8890.4 time, 2250.3 real, 945.2 MB
[runlim] sample:		8929.9 time, 2260.3 real, 951.2 MB
[runlim] sample:		8969.4 time, 2270.3 real, 957.5 MB
[runlim] sample:		9008.9 time, 2280.3 real, 961.5 MB
[runlim] sample:		9048.5 time, 2290.3 real, 970.0 MB
[runlim] sample:		9088.0 time, 2300.3 real, 978.3 MB
[runlim] sample:		9127.5 time, 2310.3 real, 984.5 MB
[runlim] sample:		9167.1 time, 2320.3 real, 990.8 MB
[runlim] sample:		9206.6 time, 2330.3 real, 993.3 MB
[runlim] sample:		9246.2 time, 2340.3 real, 1001.3 MB
[runlim] sample:		9285.7 time, 2350.3 real, 1007.8 MB
[runlim] sample:		9325.2 time, 2360.3 real, 1012.3 MB
[runlim] sample:		9364.8 time, 2370.3 real, 1466.1 MB
[runlim] sample:		9404.3 time, 2380.3 real, 1816.8 MB
[runlim] sample:		9443.9 time, 2390.3 real, 3139.0 MB
[runlim] sample:		9483.4 time, 2400.3 real, 4072.5 MB
[runlim] sample:		9523.0 time, 2410.3 real, 4809.1 MB
[runlim] sample:		9562.5 time, 2420.3 real, 4823.4 MB
[runlim] sample:		9602.0 time, 2430.3 real, 4847.4 MB
[runlim] sample:		9641.6 time, 2440.3 real, 4852.7 MB
[runlim] sample:		9681.0 time, 2450.3 real, 4859.0 MB
[runlim] sample:		9720.6 time, 2460.3 real, 4862.7 MB
[runlim] sample:		9760.1 time, 2470.3 real, 4822.6 MB
[runlim] sample:		9799.7 time, 2480.3 real, 4831.7 MB
[runlim] sample:		9839.2 time, 2490.3 real, 4837.9 MB
[runlim] sample:		9878.7 time, 2500.3 real, 4844.2 MB
[runlim] sample:		9918.3 time, 2510.3 real, 4855.5 MB
[runlim] sample:		9957.8 time, 2520.3 real, 4863.0 MB
[runlim] sample:		9997.2 time, 2530.3 real, 4890.8 MB
[runlim] sample:		10036.8 time, 2540.3 real, 4899.8 MB
[runlim] sample:		10076.4 time, 2550.3 real, 4805.4 MB
[runlim] sample:		10115.9 time, 2560.3 real, 4822.2 MB
[runlim] sample:		10155.4 time, 2570.3 real, 4831.7 MB
[runlim] sample:		10194.9 time, 2580.3 real, 4849.0 MB
[runlim] sample:		10234.5 time, 2590.3 real, 4861.0 MB
[runlim] sample:		10274.0 time, 2600.3 real, 4873.5 MB
[runlim] sample:		10313.5 time, 2610.3 real, 4881.8 MB
[runlim] sample:		10353.1 time, 2620.3 real, 4888.8 MB
[runlim] sample:		10392.6 time, 2630.3 real, 4895.1 MB
[runlim] sample:		10432.2 time, 2640.3 real, 4901.3 MB
[runlim] sample:		10471.7 time, 2650.3 real, 4909.3 MB
[runlim] sample:		10511.2 time, 2660.3 real, 4914.8 MB
[runlim] sample:		10550.8 time, 2670.3 real, 4921.5 MB
[runlim] sample:		10590.2 time, 2680.3 real, 4930.1 MB
[runlim] sample:		10629.8 time, 2690.3 real, 4821.4 MB
[runlim] sample:		10669.2 time, 2700.3 real, 4829.7 MB
[runlim] sample:		10708.8 time, 2710.3 real, 4841.9 MB
[runlim] sample:		10748.3 time, 2720.3 real, 4847.9 MB
[runlim] sample:		10787.8 time, 2730.3 real, 4854.1 MB
[runlim] sample:		10827.4 time, 2740.3 real, 4860.7 MB
[runlim] sample:		10866.9 time, 2750.3 real, 4868.9 MB
[runlim] sample:		10906.4 time, 2760.3 real, 4874.9 MB
[runlim] sample:		10946.0 time, 2770.3 real, 4880.9 MB
[runlim] sample:		10985.5 time, 2780.3 real, 4888.9 MB
[runlim] sample:		11025.1 time, 2790.3 real, 4896.9 MB
[runlim] sample:		11064.6 time, 2800.3 real, 4902.9 MB
[runlim] sample:		11104.1 time, 2810.3 real, 4909.2 MB
[runlim] sample:		11143.6 time, 2820.3 real, 4915.2 MB
[runlim] sample:		11183.1 time, 2830.3 real, 4921.2 MB
[runlim] sample:		11222.7 time, 2840.3 real, 4929.4 MB
[runlim] sample:		11262.2 time, 2850.3 real, 4937.4 MB
[runlim] sample:		11301.8 time, 2860.3 real, 4823.5 MB
[runlim] sample:		11341.3 time, 2870.3 real, 4833.7 MB
[runlim] sample:		11380.9 time, 2880.3 real, 4839.7 MB
[runlim] sample:		11420.3 time, 2890.3 real, 4845.7 MB
[runlim] sample:		11459.9 time, 2900.3 real, 4851.9 MB
[runlim] sample:		11499.4 time, 2910.3 real, 4857.9 MB
[runlim] sample:		11539.0 time, 2920.3 real, 4865.9 MB
[runlim] sample:		11578.5 time, 2930.3 real, 4871.4 MB
[runlim] sample:		11618.1 time, 2940.3 real, 4880.2 MB
[runlim] sample:		11657.6 time, 2950.3 real, 4884.5 MB
[runlim] sample:		11697.1 time, 2960.3 real, 4892.5 MB
[runlim] sample:		11736.6 time, 2970.3 real, 4898.7 MB
[runlim] sample:		11776.0 time, 2980.3 real, 4904.7 MB
[runlim] sample:		11815.6 time, 2990.3 real, 4910.7 MB
[runlim] sample:		11855.1 time, 3000.3 real, 4922.2 MB
[runlim] sample:		11894.7 time, 3010.3 real, 4929.2 MB
[runlim] sample:		11934.2 time, 3020.3 real, 4935.5 MB
[runlim] sample:		11973.8 time, 3030.3 real, 4941.7 MB
[runlim] sample:		12013.3 time, 3040.3 real, 4948.2 MB
[runlim] sample:		12052.8 time, 3050.3 real, 4796.3 MB
[runlim] sample:		12092.3 time, 3060.3 real, 4840.8 MB
[runlim] sample:		12131.8 time, 3070.3 real, 4902.7 MB
[runlim] sample:		12171.4 time, 3080.3 real, 4942.1 MB
[runlim] sample:		12210.9 time, 3090.3 real, 4950.4 MB
[runlim] sample:		12250.4 time, 3100.3 real, 4956.4 MB
[runlim] sample:		12289.9 time, 3110.3 real, 4964.4 MB
[runlim] sample:		12329.4 time, 3120.3 real, 4973.2 MB
[runlim] sample:		12369.0 time, 3130.3 real, 4994.9 MB
[runlim] sample:		12408.5 time, 3140.3 real, 5012.7 MB
[runlim] sample:		12448.1 time, 3150.3 real, 5018.9 MB
[runlim] sample:		12487.6 time, 3160.3 real, 5035.2 MB
[runlim] sample:		12527.2 time, 3170.3 real, 5056.9 MB
[runlim] sample:		12566.8 time, 3180.3 real, 5075.7 MB
[runlim] sample:		12606.3 time, 3190.3 real, 5095.4 MB
[runlim] sample:		12645.8 time, 3200.3 real, 5114.2 MB
[runlim] sample:		12685.3 time, 3210.3 real, 5124.1 MB
[runlim] sample:		12724.9 time, 3220.3 real, 5138.7 MB
[runlim] sample:		12764.4 time, 3230.3 real, 5008.4 MB
[runlim] sample:		12803.9 time, 3240.3 real, 5018.7 MB
[runlim] sample:		12843.5 time, 3250.3 real, 5028.9 MB
[runlim] sample:		12883.0 time, 3260.3 real, 5038.5 MB
[runlim] sample:		12922.6 time, 3270.3 real, 5047.9 MB
[runlim] sample:		12962.1 time, 3280.3 real, 5065.8 MB
[runlim] sample:		13001.7 time, 3290.3 real, 5081.9 MB
[runlim] sample:		13041.1 time, 3300.3 real, 5095.2 MB
[runlim] sample:		13080.7 time, 3310.3 real, 5103.9 MB
[runlim] sample:		13120.2 time, 3320.3 real, 5107.1 MB
[runlim] sample:		13159.7 time, 3330.3 real, 5111.4 MB
[runlim] sample:		13199.3 time, 3340.3 real, 5115.7 MB
[runlim] sample:		13238.8 time, 3350.3 real, 5120.2 MB
[runlim] sample:		13278.3 time, 3360.3 real, 5138.7 MB
[runlim] sample:		13317.9 time, 3370.3 real, 5141.4 MB
[runlim] sample:		13357.4 time, 3380.3 real, 5147.7 MB
[runlim] sample:		13396.9 time, 3390.3 real, 5156.6 MB
[runlim] sample:		13436.5 time, 3400.3 real, 5177.0 MB
[runlim] sample:		13476.0 time, 3410.3 real, 5190.4 MB
[runlim] sample:		13515.6 time, 3420.3 real, 5204.4 MB
[runlim] sample:		13555.1 time, 3430.3 real, 5213.2 MB
[runlim] sample:		13594.7 time, 3440.3 real, 5084.5 MB
[runlim] sample:		13634.2 time, 3450.3 real, 5125.8 MB
[runlim] sample:		13673.7 time, 3460.3 real, 5142.1 MB
[runlim] sample:		13713.2 time, 3470.3 real, 5157.8 MB
[runlim] sample:		13752.8 time, 3480.3 real, 5179.5 MB
[runlim] sample:		13792.3 time, 3490.3 real, 5228.3 MB
[runlim] sample:		13831.9 time, 3500.3 real, 5209.5 MB
[runlim] sample:		13871.4 time, 3510.3 real, 5224.1 MB
[runlim] sample:		13910.9 time, 3520.3 real, 5238.1 MB
[runlim] sample:		13950.5 time, 3530.3 real, 5247.5 MB
[runlim] sample:		13990.0 time, 3540.3 real, 5263.2 MB
[runlim] sample:		14029.6 time, 3550.3 real, 5267.5 MB
[runlim] sample:		14069.1 time, 3560.3 real, 5272.0 MB
[runlim] sample:		14108.6 time, 3570.3 real, 5276.2 MB
[runlim] sample:		14148.1 time, 3580.3 real, 5281.5 MB
[runlim] sample:		14187.6 time, 3590.3 real, 5286.8 MB
[runlim] end:			Sun Sep 20 15:37:02 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		143942
[runlim] real:			3600.09 seconds
[runlim] time:			14226.00 seconds
[runlim] space:			5294.1 MB
[runlim] samples:		35997
