[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/hwmcc14/single/6s280r.aig
[runlim] start:			Wed Sep 16 00:01:10 2015
[runlim] main pid:		28113
[runlim] sample:		35.7 time, 10.5 real, 201.2 MB
[runlim] sample:		75.3 time, 20.5 real, 212.6 MB
[runlim] sample:		114.9 time, 30.5 real, 220.1 MB
[runlim] sample:		154.5 time, 40.5 real, 239.5 MB
[runlim] sample:		194.1 time, 50.5 real, 251.0 MB
[runlim] sample:		233.7 time, 60.5 real, 263.4 MB
[runlim] sample:		273.3 time, 70.5 real, 313.7 MB
[runlim] sample:		312.9 time, 80.5 real, 341.6 MB
[runlim] sample:		352.5 time, 90.5 real, 321.5 MB
[runlim] sample:		392.2 time, 100.5 real, 330.1 MB
[runlim] sample:		431.8 time, 110.5 real, 409.4 MB
[runlim] sample:		471.4 time, 120.5 real, 414.1 MB
[runlim] sample:		511.0 time, 130.5 real, 428.9 MB
[runlim] sample:		550.6 time, 140.5 real, 435.3 MB
[runlim] sample:		590.2 time, 150.5 real, 440.9 MB
[runlim] sample:		629.7 time, 160.5 real, 443.8 MB
[runlim] sample:		669.4 time, 170.5 real, 446.3 MB
[runlim] sample:		708.9 time, 180.5 real, 447.1 MB
[runlim] sample:		748.5 time, 190.5 real, 448.7 MB
[runlim] sample:		788.1 time, 200.5 real, 451.4 MB
[runlim] sample:		827.7 time, 210.5 real, 452.6 MB
[runlim] sample:		867.3 time, 220.5 real, 456.2 MB
[runlim] sample:		906.9 time, 230.5 real, 457.0 MB
[runlim] sample:		946.5 time, 240.5 real, 457.9 MB
[runlim] sample:		986.1 time, 250.5 real, 458.7 MB
[runlim] sample:		1025.7 time, 260.5 real, 459.2 MB
[runlim] sample:		1065.3 time, 270.5 real, 460.0 MB
[runlim] sample:		1104.9 time, 280.5 real, 462.3 MB
[runlim] sample:		1144.5 time, 290.5 real, 467.2 MB
[runlim] sample:		1184.1 time, 300.5 real, 499.3 MB
[runlim] sample:		1223.8 time, 310.5 real, 476.5 MB
[runlim] sample:		1263.3 time, 320.5 real, 497.3 MB
[runlim] sample:		1302.9 time, 330.5 real, 497.7 MB
[runlim] sample:		1342.5 time, 340.5 real, 504.9 MB
[runlim] sample:		1382.1 time, 350.5 real, 507.4 MB
[runlim] sample:		1421.7 time, 360.5 real, 511.0 MB
[runlim] sample:		1461.3 time, 370.5 real, 526.6 MB
[runlim] sample:		1500.9 time, 380.5 real, 528.8 MB
[runlim] sample:		1540.5 time, 390.5 real, 537.8 MB
[runlim] sample:		1580.1 time, 400.5 real, 540.8 MB
[runlim] sample:		1619.7 time, 410.5 real, 541.6 MB
[runlim] sample:		1659.2 time, 420.5 real, 542.1 MB
[runlim] sample:		1698.8 time, 430.5 real, 542.7 MB
[runlim] sample:		1738.4 time, 440.5 real, 542.9 MB
[runlim] sample:		1778.0 time, 450.5 real, 543.4 MB
[runlim] sample:		1817.6 time, 460.5 real, 543.7 MB
[runlim] sample:		1857.2 time, 470.5 real, 544.2 MB
[runlim] sample:		1896.8 time, 480.5 real, 544.5 MB
[runlim] sample:		1936.3 time, 490.5 real, 545.0 MB
[runlim] sample:		1976.0 time, 500.5 real, 545.2 MB
[runlim] sample:		2015.6 time, 510.5 real, 545.8 MB
[runlim] sample:		2055.2 time, 520.5 real, 546.0 MB
[runlim] sample:		2094.8 time, 530.5 real, 547.0 MB
[runlim] sample:		2134.4 time, 540.5 real, 547.6 MB
[runlim] sample:		2174.0 time, 550.5 real, 548.1 MB
[runlim] sample:		2213.6 time, 560.5 real, 548.3 MB
[runlim] sample:		2253.2 time, 570.5 real, 549.0 MB
[runlim] sample:		2292.8 time, 580.5 real, 549.3 MB
[runlim] sample:		2332.4 time, 590.5 real, 549.5 MB
[runlim] sample:		2372.0 time, 600.5 real, 550.0 MB
[runlim] sample:		2411.6 time, 610.5 real, 550.6 MB
[runlim] sample:		2451.2 time, 620.5 real, 550.8 MB
[runlim] sample:		2490.8 time, 630.5 real, 551.3 MB
[runlim] sample:		2530.5 time, 640.5 real, 551.6 MB
[runlim] sample:		2570.1 time, 650.5 real, 552.1 MB
[runlim] sample:		2609.6 time, 660.5 real, 552.4 MB
[runlim] sample:		2649.2 time, 670.5 real, 552.6 MB
[runlim] sample:		2688.8 time, 680.5 real, 569.6 MB
[runlim] sample:		2728.4 time, 690.5 real, 608.9 MB
[runlim] sample:		2768.0 time, 700.5 real, 627.4 MB
[runlim] sample:		2807.6 time, 710.5 real, 619.4 MB
[runlim] sample:		2847.2 time, 720.5 real, 615.9 MB
[runlim] sample:		2886.8 time, 730.5 real, 626.1 MB
[runlim] sample:		2926.3 time, 740.5 real, 514.4 MB
[runlim] sample:		2965.9 time, 750.5 real, 521.9 MB
[runlim] sample:		3005.5 time, 760.5 real, 530.2 MB
[runlim] sample:		3045.1 time, 770.5 real, 534.4 MB
[runlim] sample:		3084.7 time, 780.5 real, 536.7 MB
[runlim] sample:		3124.4 time, 790.5 real, 537.2 MB
[runlim] sample:		3164.0 time, 800.5 real, 540.2 MB
[runlim] sample:		3203.6 time, 810.5 real, 556.0 MB
[runlim] sample:		3243.2 time, 820.5 real, 563.3 MB
[runlim] sample:		3282.8 time, 830.5 real, 592.9 MB
[runlim] sample:		3322.4 time, 840.5 real, 602.9 MB
[runlim] sample:		3362.0 time, 850.5 real, 605.5 MB
[runlim] sample:		3401.6 time, 860.5 real, 749.0 MB
[runlim] sample:		3441.3 time, 870.5 real, 799.0 MB
[runlim] sample:		3480.8 time, 880.5 real, 799.3 MB
[runlim] sample:		3520.4 time, 890.5 real, 799.5 MB
[runlim] sample:		3560.0 time, 900.5 real, 799.9 MB
[runlim] sample:		3599.6 time, 910.5 real, 725.6 MB
[runlim] sample:		3639.2 time, 920.5 real, 735.6 MB
[runlim] sample:		3678.8 time, 930.5 real, 769.5 MB
[runlim] sample:		3718.4 time, 940.5 real, 715.8 MB
[runlim] sample:		3758.1 time, 950.5 real, 773.3 MB
[runlim] sample:		3797.7 time, 960.5 real, 763.6 MB
[runlim] sample:		3837.3 time, 970.5 real, 773.7 MB
[runlim] sample:		3876.9 time, 980.5 real, 650.4 MB
[runlim] sample:		3916.5 time, 990.5 real, 660.2 MB
[runlim] sample:		3956.1 time, 1000.5 real, 692.0 MB
[runlim] sample:		3995.7 time, 1010.5 real, 661.0 MB
[runlim] sample:		4035.3 time, 1020.5 real, 661.3 MB
[runlim] sample:		4074.9 time, 1030.5 real, 664.4 MB
[runlim] sample:		4114.5 time, 1040.5 real, 664.6 MB
[runlim] sample:		4154.0 time, 1050.5 real, 664.9 MB
[runlim] sample:		4193.7 time, 1060.5 real, 665.1 MB
[runlim] sample:		4233.2 time, 1070.5 real, 665.4 MB
[runlim] sample:		4272.9 time, 1080.5 real, 665.6 MB
[runlim] sample:		4312.5 time, 1090.5 real, 665.9 MB
[runlim] sample:		4352.1 time, 1100.5 real, 666.2 MB
[runlim] sample:		4391.7 time, 1110.5 real, 666.4 MB
[runlim] sample:		4431.2 time, 1120.5 real, 666.7 MB
[runlim] sample:		4470.8 time, 1130.5 real, 666.7 MB
[runlim] sample:		4510.4 time, 1140.5 real, 666.9 MB
[runlim] sample:		4550.0 time, 1150.5 real, 674.7 MB
[runlim] sample:		4589.6 time, 1160.5 real, 667.6 MB
[runlim] sample:		4629.2 time, 1170.5 real, 670.5 MB
[runlim] sample:		4668.8 time, 1180.5 real, 672.7 MB
[runlim] sample:		4708.4 time, 1190.5 real, 675.0 MB
[runlim] sample:		4747.9 time, 1200.5 real, 677.3 MB
[runlim] sample:		4787.5 time, 1210.5 real, 679.3 MB
[runlim] sample:		4827.1 time, 1220.5 real, 681.5 MB
[runlim] sample:		4866.7 time, 1230.5 real, 714.6 MB
[runlim] sample:		4906.3 time, 1240.5 real, 717.5 MB
[runlim] sample:		4945.9 time, 1250.5 real, 719.7 MB
[runlim] sample:		4985.5 time, 1260.5 real, 684.3 MB
[runlim] sample:		5025.1 time, 1270.5 real, 684.5 MB
[runlim] sample:		5064.7 time, 1280.5 real, 684.5 MB
[runlim] sample:		5104.3 time, 1290.5 real, 684.8 MB
[runlim] sample:		5143.9 time, 1300.5 real, 685.0 MB
[runlim] sample:		5183.5 time, 1310.5 real, 685.3 MB
[runlim] sample:		5223.1 time, 1320.5 real, 717.1 MB
[runlim] sample:		5262.7 time, 1330.5 real, 719.1 MB
[runlim] sample:		5302.3 time, 1340.5 real, 685.8 MB
[runlim] sample:		5341.9 time, 1350.5 real, 686.1 MB
[runlim] sample:		5381.5 time, 1360.5 real, 686.3 MB
[runlim] sample:		5421.1 time, 1370.5 real, 686.6 MB
[runlim] sample:		5460.7 time, 1380.5 real, 686.8 MB
[runlim] sample:		5500.3 time, 1390.5 real, 687.1 MB
[runlim] sample:		5539.9 time, 1400.5 real, 718.9 MB
[runlim] sample:		5579.5 time, 1410.5 real, 721.2 MB
[runlim] sample:		5619.1 time, 1420.5 real, 723.2 MB
[runlim] sample:		5658.7 time, 1430.5 real, 687.9 MB
[runlim] sample:		5698.3 time, 1440.5 real, 688.1 MB
[runlim] sample:		5737.9 time, 1450.5 real, 688.4 MB
[runlim] sample:		5777.5 time, 1460.5 real, 688.6 MB
[runlim] sample:		5817.1 time, 1470.5 real, 688.6 MB
[runlim] sample:		5856.7 time, 1480.5 real, 688.9 MB
[runlim] sample:		5896.3 time, 1490.5 real, 723.3 MB
[runlim] sample:		5935.9 time, 1500.5 real, 732.5 MB
[runlim] sample:		5975.5 time, 1510.5 real, 734.5 MB
[runlim] sample:		6015.1 time, 1520.5 real, 699.2 MB
[runlim] sample:		6054.6 time, 1530.5 real, 699.2 MB
[runlim] sample:		6094.2 time, 1540.5 real, 699.5 MB
[runlim] sample:		6133.8 time, 1550.5 real, 699.7 MB
[runlim] sample:		6173.4 time, 1560.5 real, 699.7 MB
[runlim] sample:		6213.0 time, 1570.5 real, 700.0 MB
[runlim] sample:		6252.6 time, 1580.5 real, 731.8 MB
[runlim] sample:		6292.2 time, 1590.5 real, 732.0 MB
[runlim] sample:		6331.8 time, 1600.5 real, 734.0 MB
[runlim] sample:		6371.4 time, 1610.5 real, 736.3 MB
[runlim] sample:		6411.0 time, 1620.5 real, 701.0 MB
[runlim] sample:		6450.6 time, 1630.5 real, 701.0 MB
[runlim] sample:		6490.2 time, 1640.5 real, 701.3 MB
[runlim] sample:		6529.8 time, 1650.5 real, 701.5 MB
[runlim] sample:		6569.4 time, 1660.5 real, 702.1 MB
[runlim] sample:		6608.9 time, 1670.5 real, 733.9 MB
[runlim] sample:		6648.5 time, 1680.5 real, 734.2 MB
[runlim] sample:		6688.0 time, 1690.5 real, 736.4 MB
[runlim] sample:		6727.5 time, 1700.5 real, 738.4 MB
[runlim] sample:		6767.1 time, 1710.5 real, 740.4 MB
[runlim] sample:		6806.7 time, 1720.5 real, 703.2 MB
[runlim] sample:		6846.3 time, 1730.5 real, 703.4 MB
[runlim] sample:		6885.9 time, 1740.5 real, 710.4 MB
[runlim] sample:		6925.5 time, 1750.5 real, 712.9 MB
[runlim] sample:		6965.1 time, 1760.5 real, 715.8 MB
[runlim] sample:		7004.6 time, 1770.5 real, 715.8 MB
[runlim] sample:		7044.2 time, 1780.5 real, 747.6 MB
[runlim] sample:		7083.8 time, 1790.5 real, 749.6 MB
[runlim] sample:		7123.4 time, 1800.5 real, 751.8 MB
[runlim] sample:		7163.0 time, 1810.5 real, 754.1 MB
[runlim] sample:		7202.6 time, 1820.5 real, 756.8 MB
[runlim] sample:		7242.2 time, 1830.5 real, 717.8 MB
[runlim] sample:		7281.7 time, 1840.5 real, 717.8 MB
[runlim] sample:		7321.3 time, 1850.5 real, 718.1 MB
[runlim] sample:		7360.9 time, 1860.5 real, 718.6 MB
[runlim] sample:		7400.5 time, 1870.5 real, 750.1 MB
[runlim] sample:		7440.1 time, 1880.5 real, 752.4 MB
[runlim] sample:		7479.7 time, 1890.5 real, 754.6 MB
[runlim] sample:		7519.3 time, 1900.5 real, 756.9 MB
[runlim] sample:		7558.9 time, 1910.5 real, 759.1 MB
[runlim] sample:		7598.5 time, 1920.5 real, 761.1 MB
[runlim] sample:		7638.1 time, 1930.5 real, 719.6 MB
[runlim] sample:		7677.6 time, 1940.5 real, 719.8 MB
[runlim] sample:		7717.2 time, 1950.5 real, 720.3 MB
[runlim] sample:		7756.8 time, 1960.5 real, 720.3 MB
[runlim] sample:		7796.4 time, 1970.5 real, 720.6 MB
[runlim] sample:		7835.9 time, 1980.5 real, 752.1 MB
[runlim] sample:		7875.5 time, 1990.5 real, 754.4 MB
[runlim] sample:		7915.1 time, 2000.5 real, 756.4 MB
[runlim] sample:		7954.6 time, 2010.5 real, 758.7 MB
[runlim] sample:		7994.2 time, 2020.5 real, 760.7 MB
[runlim] sample:		8033.8 time, 2030.5 real, 760.9 MB
[runlim] sample:		8073.4 time, 2040.5 real, 763.2 MB
[runlim] sample:		8113.0 time, 2050.5 real, 721.9 MB
[runlim] sample:		8152.5 time, 2060.5 real, 723.0 MB
[runlim] sample:		8192.1 time, 2070.5 real, 723.3 MB
[runlim] sample:		8231.7 time, 2080.5 real, 723.3 MB
[runlim] sample:		8271.3 time, 2090.5 real, 723.5 MB
[runlim] sample:		8310.9 time, 2100.5 real, 724.3 MB
[runlim] sample:		8350.5 time, 2110.5 real, 756.1 MB
[runlim] sample:		8390.1 time, 2120.5 real, 758.4 MB
[runlim] sample:		8429.7 time, 2130.5 real, 760.6 MB
[runlim] sample:		8469.3 time, 2140.5 real, 763.6 MB
[runlim] sample:		8508.9 time, 2150.5 real, 765.6 MB
[runlim] sample:		8548.4 time, 2160.5 real, 765.8 MB
[runlim] sample:		8588.0 time, 2170.5 real, 767.8 MB
[runlim] sample:		8627.6 time, 2180.5 real, 726.5 MB
[runlim] sample:		8667.2 time, 2190.5 real, 726.5 MB
[runlim] sample:		8706.8 time, 2200.5 real, 727.1 MB
[runlim] sample:		8746.3 time, 2210.5 real, 727.1 MB
[runlim] sample:		8786.0 time, 2220.5 real, 727.6 MB
[runlim] sample:		8825.5 time, 2230.5 real, 759.1 MB
[runlim] sample:		8865.1 time, 2240.5 real, 761.4 MB
[runlim] sample:		8904.7 time, 2250.5 real, 763.4 MB
[runlim] sample:		8944.3 time, 2260.5 real, 765.6 MB
[runlim] sample:		8983.9 time, 2270.5 real, 767.6 MB
[runlim] sample:		9023.5 time, 2280.5 real, 767.6 MB
[runlim] sample:		9063.1 time, 2290.5 real, 769.9 MB
[runlim] sample:		9102.6 time, 2300.5 real, 772.3 MB
[runlim] sample:		9142.2 time, 2310.5 real, 772.8 MB
[runlim] sample:		9181.8 time, 2320.5 real, 729.1 MB
[runlim] sample:		9221.4 time, 2330.5 real, 729.1 MB
[runlim] sample:		9261.0 time, 2340.5 real, 729.4 MB
[runlim] sample:		9300.6 time, 2350.5 real, 729.4 MB
[runlim] sample:		9340.2 time, 2360.5 real, 729.6 MB
[runlim] sample:		9379.8 time, 2370.5 real, 761.4 MB
[runlim] sample:		9419.4 time, 2380.5 real, 763.4 MB
[runlim] sample:		9459.0 time, 2390.5 real, 765.7 MB
[runlim] sample:		9498.5 time, 2400.5 real, 767.7 MB
[runlim] sample:		9538.1 time, 2410.5 real, 769.7 MB
[runlim] sample:		9577.7 time, 2420.5 real, 770.0 MB
[runlim] sample:		9617.3 time, 2430.5 real, 772.1 MB
[runlim] sample:		9656.9 time, 2440.5 real, 774.4 MB
[runlim] sample:		9696.4 time, 2450.5 real, 776.4 MB
[runlim] sample:		9736.0 time, 2460.5 real, 730.9 MB
[runlim] sample:		9775.6 time, 2470.5 real, 730.9 MB
[runlim] sample:		9815.2 time, 2480.5 real, 731.4 MB
[runlim] sample:		9854.8 time, 2490.5 real, 731.4 MB
[runlim] sample:		9894.3 time, 2500.5 real, 731.7 MB
[runlim] sample:		9933.9 time, 2510.5 real, 763.2 MB
[runlim] sample:		9973.5 time, 2520.5 real, 765.5 MB
[runlim] sample:		10013.1 time, 2530.5 real, 767.5 MB
[runlim] sample:		10052.7 time, 2540.5 real, 769.8 MB
[runlim] sample:		10092.3 time, 2550.5 real, 769.8 MB
[runlim] sample:		10131.9 time, 2560.5 real, 772.3 MB
[runlim] sample:		10171.5 time, 2570.5 real, 774.3 MB
[runlim] sample:		10211.1 time, 2580.5 real, 776.7 MB
[runlim] sample:		10250.7 time, 2590.5 real, 778.7 MB
[runlim] sample:		10290.3 time, 2600.5 real, 733.0 MB
[runlim] sample:		10329.8 time, 2610.5 real, 733.2 MB
[runlim] sample:		10369.4 time, 2620.5 real, 733.8 MB
[runlim] sample:		10409.0 time, 2630.5 real, 734.0 MB
[runlim] sample:		10448.6 time, 2640.5 real, 765.8 MB
[runlim] sample:		10488.1 time, 2650.5 real, 767.8 MB
[runlim] sample:		10527.7 time, 2660.5 real, 770.1 MB
[runlim] sample:		10567.3 time, 2670.5 real, 772.1 MB
[runlim] sample:		10606.9 time, 2680.5 real, 774.3 MB
[runlim] sample:		10646.5 time, 2690.5 real, 776.3 MB
[runlim] sample:		10686.1 time, 2700.5 real, 778.5 MB
[runlim] sample:		10725.7 time, 2710.5 real, 781.0 MB
[runlim] sample:		10765.3 time, 2720.5 real, 783.0 MB
[runlim] sample:		10804.9 time, 2730.5 real, 783.3 MB
[runlim] sample:		10844.5 time, 2740.5 real, 735.8 MB
[runlim] sample:		10884.0 time, 2750.5 real, 736.1 MB
[runlim] sample:		10923.6 time, 2760.5 real, 736.3 MB
[runlim] sample:		10963.2 time, 2770.5 real, 767.9 MB
[runlim] sample:		11002.8 time, 2780.5 real, 769.9 MB
[runlim] sample:		11042.4 time, 2790.5 real, 770.1 MB
[runlim] sample:		11082.0 time, 2800.5 real, 774.1 MB
[runlim] sample:		11121.6 time, 2810.5 real, 776.4 MB
[runlim] sample:		11161.2 time, 2820.5 real, 776.4 MB
[runlim] sample:		11200.8 time, 2830.5 real, 778.7 MB
[runlim] sample:		11240.4 time, 2840.5 real, 780.8 MB
[runlim] sample:		11280.0 time, 2850.5 real, 783.1 MB
[runlim] sample:		11319.6 time, 2860.5 real, 785.1 MB
[runlim] sample:		11359.2 time, 2870.5 real, 785.4 MB
[runlim] sample:		11398.7 time, 2880.5 real, 737.9 MB
[runlim] sample:		11438.3 time, 2890.5 real, 737.9 MB
[runlim] sample:		11477.9 time, 2900.5 real, 738.2 MB
[runlim] sample:		11517.5 time, 2910.5 real, 769.7 MB
[runlim] sample:		11557.1 time, 2920.5 real, 769.7 MB
[runlim] sample:		11596.7 time, 2930.5 real, 772.0 MB
[runlim] sample:		11636.2 time, 2940.5 real, 774.0 MB
[runlim] sample:		11675.8 time, 2950.5 real, 776.2 MB
[runlim] sample:		11715.4 time, 2960.5 real, 778.2 MB
[runlim] sample:		11755.0 time, 2970.5 real, 780.5 MB
[runlim] sample:		11794.5 time, 2980.5 real, 782.6 MB
[runlim] sample:		11834.1 time, 2990.5 real, 784.6 MB
[runlim] sample:		11873.7 time, 3000.5 real, 786.9 MB
[runlim] sample:		11913.3 time, 3010.5 real, 787.4 MB
[runlim] sample:		11952.8 time, 3020.5 real, 739.4 MB
[runlim] sample:		11992.4 time, 3030.5 real, 739.6 MB
[runlim] sample:		12032.0 time, 3040.5 real, 740.1 MB
[runlim] sample:		12071.6 time, 3050.5 real, 771.6 MB
[runlim] sample:		12111.2 time, 3060.5 real, 773.6 MB
[runlim] sample:		12150.8 time, 3070.5 real, 773.9 MB
[runlim] sample:		12190.4 time, 3080.5 real, 776.2 MB
[runlim] sample:		12229.9 time, 3090.5 real, 778.2 MB
[runlim] sample:		12269.5 time, 3100.5 real, 780.4 MB
[runlim] sample:		12309.1 time, 3110.5 real, 784.7 MB
[runlim] sample:		12348.7 time, 3120.5 real, 788.5 MB
[runlim] sample:		12388.3 time, 3130.5 real, 790.5 MB
[runlim] sample:		12427.9 time, 3140.5 real, 791.3 MB
[runlim] sample:		12467.5 time, 3150.5 real, 794.3 MB
[runlim] sample:		12507.0 time, 3160.5 real, 743.0 MB
[runlim] sample:		12546.6 time, 3170.5 real, 743.3 MB
[runlim] sample:		12586.2 time, 3180.5 real, 743.3 MB
[runlim] sample:		12625.8 time, 3190.5 real, 783.6 MB
[runlim] sample:		12665.4 time, 3200.5 real, 794.8 MB
[runlim] sample:		12705.0 time, 3210.5 real, 798.1 MB
[runlim] sample:		12744.6 time, 3220.5 real, 800.4 MB
[runlim] sample:		12784.2 time, 3230.5 real, 802.4 MB
[runlim] sample:		12823.8 time, 3240.5 real, 804.4 MB
[runlim] sample:		12863.4 time, 3250.5 real, 806.8 MB
[runlim] sample:		12903.0 time, 3260.5 real, 808.8 MB
[runlim] sample:		12942.6 time, 3270.5 real, 811.1 MB
[runlim] sample:		12982.2 time, 3280.5 real, 811.8 MB
[runlim] sample:		13021.7 time, 3290.5 real, 816.7 MB
[runlim] sample:		13061.3 time, 3300.5 real, 818.7 MB
[runlim] sample:		13100.9 time, 3310.5 real, 765.5 MB
[runlim] sample:		13140.5 time, 3320.5 real, 765.5 MB
[runlim] sample:		13180.1 time, 3330.5 real, 797.3 MB
[runlim] sample:		13219.7 time, 3340.5 real, 799.8 MB
[runlim] sample:		13259.3 time, 3350.5 real, 799.8 MB
[runlim] sample:		13298.9 time, 3360.5 real, 801.8 MB
[runlim] sample:		13338.5 time, 3370.5 real, 804.0 MB
[runlim] sample:		13378.1 time, 3380.5 real, 806.0 MB
[runlim] sample:		13417.6 time, 3390.5 real, 808.5 MB
[runlim] sample:		13457.2 time, 3400.5 real, 810.5 MB
[runlim] sample:		13496.8 time, 3410.5 real, 812.7 MB
[runlim] sample:		13536.4 time, 3420.5 real, 815.0 MB
[runlim] sample:		13576.0 time, 3430.5 real, 815.7 MB
[runlim] sample:		13615.6 time, 3440.5 real, 819.0 MB
[runlim] sample:		13655.2 time, 3450.5 real, 767.8 MB
[runlim] sample:		13694.7 time, 3460.5 real, 767.8 MB
[runlim] sample:		13734.3 time, 3470.5 real, 799.6 MB
[runlim] sample:		13773.9 time, 3480.5 real, 803.8 MB
[runlim] sample:		13813.5 time, 3490.5 real, 806.1 MB
[runlim] sample:		13853.0 time, 3500.5 real, 808.1 MB
[runlim] sample:		13892.6 time, 3510.5 real, 810.1 MB
[runlim] sample:		13932.2 time, 3520.5 real, 812.8 MB
[runlim] sample:		13971.8 time, 3530.5 real, 815.0 MB
[runlim] sample:		14011.4 time, 3540.5 real, 817.3 MB
[runlim] sample:		14051.0 time, 3550.5 real, 817.3 MB
[runlim] sample:		14090.6 time, 3560.5 real, 821.1 MB
[runlim] sample:		14130.1 time, 3570.5 real, 823.3 MB
[runlim] sample:		14169.7 time, 3580.5 real, 769.8 MB
[runlim] sample:		14209.3 time, 3590.5 real, 770.1 MB
[runlim] end:			Wed Sep 16 01:01:10 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		143955
[runlim] real:			3600.08 seconds
[runlim] time:			14247.34 seconds
[runlim] space:			823.3 MB
[runlim] samples:		35996
