[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/iimc/single.iimc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/hwmcc14/single/6s13.aig
[runlim] start:			Tue Sep 15 17:00:14 2015
[runlim] main pid:		31295
[runlim] sample:		13.3 time, 10.6 real, 150.2 MB
[runlim] sample:		52.3 time, 20.6 real, 430.6 MB
[runlim] sample:		91.9 time, 30.6 real, 447.2 MB
[runlim] sample:		131.5 time, 40.6 real, 445.1 MB
[runlim] sample:		171.1 time, 50.6 real, 488.3 MB
[runlim] sample:		210.7 time, 60.6 real, 465.5 MB
[runlim] sample:		250.3 time, 70.6 real, 473.8 MB
[runlim] sample:		289.9 time, 80.6 real, 498.8 MB
[runlim] sample:		329.5 time, 90.6 real, 490.0 MB
[runlim] sample:		369.1 time, 100.6 real, 487.3 MB
[runlim] sample:		408.7 time, 110.6 real, 503.2 MB
[runlim] sample:		448.3 time, 120.6 real, 499.6 MB
[runlim] sample:		487.9 time, 130.6 real, 515.6 MB
[runlim] sample:		527.5 time, 140.6 real, 505.9 MB
[runlim] sample:		567.1 time, 150.6 real, 527.3 MB
[runlim] sample:		606.7 time, 160.6 real, 513.6 MB
[runlim] sample:		646.3 time, 170.6 real, 512.9 MB
[runlim] sample:		685.9 time, 180.6 real, 517.7 MB
[runlim] sample:		725.5 time, 190.6 real, 521.3 MB
[runlim] sample:		765.0 time, 200.6 real, 515.5 MB
[runlim] sample:		804.6 time, 210.6 real, 502.4 MB
[runlim] sample:		844.2 time, 220.6 real, 513.8 MB
[runlim] sample:		883.8 time, 230.6 real, 521.1 MB
[runlim] sample:		923.4 time, 240.6 real, 503.1 MB
[runlim] sample:		963.0 time, 250.6 real, 509.4 MB
[runlim] sample:		1002.6 time, 260.6 real, 518.1 MB
[runlim] sample:		1042.2 time, 270.6 real, 527.8 MB
[runlim] sample:		1081.8 time, 280.6 real, 542.2 MB
[runlim] sample:		1121.4 time, 290.6 real, 548.9 MB
[runlim] sample:		1161.0 time, 300.6 real, 569.5 MB
[runlim] sample:		1200.6 time, 310.6 real, 575.5 MB
[runlim] sample:		1240.2 time, 320.6 real, 572.2 MB
[runlim] sample:		1279.8 time, 330.6 real, 576.5 MB
[runlim] sample:		1319.4 time, 340.6 real, 599.0 MB
[runlim] sample:		1359.0 time, 350.6 real, 606.7 MB
[runlim] sample:		1398.6 time, 360.6 real, 616.4 MB
[runlim] sample:		1438.2 time, 370.6 real, 609.1 MB
[runlim] sample:		1477.7 time, 380.6 real, 653.4 MB
[runlim] sample:		1517.3 time, 390.6 real, 655.7 MB
[runlim] sample:		1556.9 time, 400.6 real, 660.1 MB
[runlim] sample:		1596.5 time, 410.6 real, 659.1 MB
[runlim] sample:		1636.1 time, 420.6 real, 660.1 MB
[runlim] sample:		1675.8 time, 430.6 real, 650.2 MB
[runlim] sample:		1715.3 time, 440.6 real, 654.2 MB
[runlim] sample:		1755.0 time, 450.6 real, 656.5 MB
[runlim] sample:		1794.5 time, 460.6 real, 657.5 MB
[runlim] sample:		1834.2 time, 470.6 real, 659.0 MB
[runlim] sample:		1873.7 time, 480.6 real, 667.5 MB
[runlim] sample:		1913.3 time, 490.6 real, 666.1 MB
[runlim] sample:		1952.9 time, 500.6 real, 666.1 MB
[runlim] sample:		1992.5 time, 510.6 real, 662.1 MB
[runlim] sample:		2032.1 time, 520.6 real, 662.1 MB
[runlim] sample:		2071.7 time, 530.6 real, 670.1 MB
[runlim] sample:		2111.3 time, 540.6 real, 672.6 MB
[runlim] sample:		2150.9 time, 550.6 real, 674.6 MB
[runlim] sample:		2190.5 time, 560.6 real, 674.8 MB
[runlim] sample:		2230.1 time, 570.6 real, 675.3 MB
[runlim] sample:		2269.7 time, 580.6 real, 679.3 MB
[runlim] sample:		2309.3 time, 590.6 real, 679.5 MB
[runlim] sample:		2348.9 time, 600.6 real, 679.8 MB
[runlim] sample:		2388.5 time, 610.6 real, 682.4 MB
[runlim] sample:		2428.1 time, 620.6 real, 683.5 MB
[runlim] sample:		2467.7 time, 630.6 real, 682.5 MB
[runlim] sample:		2507.3 time, 640.6 real, 682.5 MB
[runlim] sample:		2546.9 time, 650.6 real, 682.7 MB
[runlim] sample:		2586.5 time, 660.6 real, 689.7 MB
[runlim] sample:		2626.1 time, 670.6 real, 691.3 MB
[runlim] sample:		2665.7 time, 680.6 real, 701.9 MB
[runlim] sample:		2705.3 time, 690.6 real, 704.1 MB
[runlim] sample:		2744.9 time, 700.6 real, 706.4 MB
[runlim] sample:		2784.5 time, 710.6 real, 709.5 MB
[runlim] sample:		2824.1 time, 720.6 real, 712.6 MB
[runlim] sample:		2863.7 time, 730.6 real, 667.5 MB
[runlim] sample:		2903.3 time, 740.6 real, 665.1 MB
[runlim] sample:		2942.9 time, 750.6 real, 666.1 MB
[runlim] sample:		2982.5 time, 760.6 real, 666.6 MB
[runlim] sample:		3022.1 time, 770.6 real, 662.2 MB
[runlim] sample:		3061.7 time, 780.6 real, 664.2 MB
[runlim] sample:		3101.3 time, 790.6 real, 664.5 MB
[runlim] sample:		3140.9 time, 800.6 real, 664.7 MB
[runlim] sample:		3180.5 time, 810.6 real, 669.0 MB
[runlim] sample:		3220.1 time, 820.6 real, 669.0 MB
[runlim] sample:		3259.7 time, 830.6 real, 669.5 MB
[runlim] sample:		3299.2 time, 840.6 real, 671.5 MB
[runlim] sample:		3338.8 time, 850.6 real, 673.9 MB
[runlim] sample:		3378.4 time, 860.6 real, 685.3 MB
[runlim] sample:		3418.1 time, 870.6 real, 687.8 MB
[runlim] sample:		3457.7 time, 880.6 real, 669.1 MB
[runlim] sample:		3497.2 time, 890.6 real, 669.1 MB
[runlim] sample:		3536.8 time, 900.6 real, 669.3 MB
[runlim] sample:		3576.4 time, 910.6 real, 716.0 MB
[runlim] sample:		3616.0 time, 920.6 real, 716.2 MB
[runlim] sample:		3655.6 time, 930.6 real, 718.2 MB
[runlim] sample:		3695.2 time, 940.6 real, 720.2 MB
[runlim] sample:		3734.8 time, 950.6 real, 722.2 MB
[runlim] sample:		3774.4 time, 960.6 real, 722.2 MB
[runlim] sample:		3814.0 time, 970.6 real, 726.4 MB
[runlim] sample:		3853.6 time, 980.6 real, 728.5 MB
[runlim] sample:		3893.2 time, 990.6 real, 724.0 MB
[runlim] sample:		3932.8 time, 1000.6 real, 724.3 MB
[runlim] sample:		3972.4 time, 1010.6 real, 726.3 MB
[runlim] sample:		4012.0 time, 1020.6 real, 726.5 MB
[runlim] sample:		4051.6 time, 1030.6 real, 734.3 MB
[runlim] sample:		4091.2 time, 1040.6 real, 734.6 MB
[runlim] sample:		4130.8 time, 1050.6 real, 734.8 MB
[runlim] sample:		4170.4 time, 1060.6 real, 737.3 MB
[runlim] sample:		4210.0 time, 1070.6 real, 725.7 MB
[runlim] sample:		4249.6 time, 1080.6 real, 729.7 MB
[runlim] sample:		4289.2 time, 1090.6 real, 690.6 MB
[runlim] sample:		4328.8 time, 1100.6 real, 693.3 MB
[runlim] sample:		4368.4 time, 1110.6 real, 693.8 MB
[runlim] sample:		4408.0 time, 1120.6 real, 689.2 MB
[runlim] sample:		4447.6 time, 1130.6 real, 689.4 MB
[runlim] sample:		4487.2 time, 1140.6 real, 689.4 MB
[runlim] sample:		4526.8 time, 1150.6 real, 689.7 MB
[runlim] sample:		4566.4 time, 1160.6 real, 689.7 MB
[runlim] sample:		4606.0 time, 1170.6 real, 696.6 MB
[runlim] sample:		4645.6 time, 1180.6 real, 697.1 MB
[runlim] sample:		4685.2 time, 1190.6 real, 699.4 MB
[runlim] sample:		4724.8 time, 1200.6 real, 701.0 MB
[runlim] sample:		4764.4 time, 1210.6 real, 704.4 MB
[runlim] sample:		4804.0 time, 1220.6 real, 704.4 MB
[runlim] sample:		4843.6 time, 1230.6 real, 704.7 MB
[runlim] sample:		4883.2 time, 1240.6 real, 736.7 MB
[runlim] sample:		4922.9 time, 1250.6 real, 739.2 MB
[runlim] sample:		4962.4 time, 1260.6 real, 739.4 MB
[runlim] sample:		5002.1 time, 1270.6 real, 738.2 MB
[runlim] sample:		5041.6 time, 1280.6 real, 738.5 MB
[runlim] sample:		5081.3 time, 1290.6 real, 740.8 MB
[runlim] sample:		5120.9 time, 1300.6 real, 743.0 MB
[runlim] sample:		5160.4 time, 1310.6 real, 750.1 MB
[runlim] sample:		5200.1 time, 1320.6 real, 752.6 MB
[runlim] sample:		5239.6 time, 1330.6 real, 755.1 MB
[runlim] sample:		5279.2 time, 1340.6 real, 755.4 MB
[runlim] sample:		5318.9 time, 1350.6 real, 757.4 MB
[runlim] sample:		5358.4 time, 1360.6 real, 759.9 MB
[runlim] sample:		5398.0 time, 1370.6 real, 761.7 MB
[runlim] sample:		5437.6 time, 1380.6 real, 767.5 MB
[runlim] sample:		5477.2 time, 1390.6 real, 768.2 MB
[runlim] sample:		5516.9 time, 1400.6 real, 771.8 MB
[runlim] sample:		5556.5 time, 1410.6 real, 772.0 MB
[runlim] sample:		5596.1 time, 1420.6 real, 774.3 MB
[runlim] sample:		5635.7 time, 1430.6 real, 776.3 MB
[runlim] sample:		5675.3 time, 1440.6 real, 772.6 MB
[runlim] sample:		5714.9 time, 1450.6 real, 776.6 MB
[runlim] sample:		5754.5 time, 1460.6 real, 780.6 MB
[runlim] sample:		5794.1 time, 1470.6 real, 782.6 MB
[runlim] sample:		5833.7 time, 1480.6 real, 782.6 MB
[runlim] sample:		5873.3 time, 1490.6 real, 784.6 MB
[runlim] sample:		5912.9 time, 1500.6 real, 784.6 MB
[runlim] sample:		5952.5 time, 1510.6 real, 790.7 MB
[runlim] sample:		5992.1 time, 1520.6 real, 790.7 MB
[runlim] sample:		6031.7 time, 1530.6 real, 788.8 MB
[runlim] sample:		6071.3 time, 1540.6 real, 788.8 MB
[runlim] sample:		6110.9 time, 1550.6 real, 788.8 MB
[runlim] sample:		6150.5 time, 1560.6 real, 791.0 MB
[runlim] sample:		6190.1 time, 1570.6 real, 791.0 MB
[runlim] sample:		6229.7 time, 1580.6 real, 793.0 MB
[runlim] sample:		6269.3 time, 1590.6 real, 793.0 MB
[runlim] sample:		6308.9 time, 1600.6 real, 795.0 MB
[runlim] sample:		6348.5 time, 1610.6 real, 795.0 MB
[runlim] sample:		6388.1 time, 1620.6 real, 769.2 MB
[runlim] sample:		6427.7 time, 1630.6 real, 771.2 MB
[runlim] sample:		6467.3 time, 1640.6 real, 775.0 MB
[runlim] sample:		6506.9 time, 1650.6 real, 777.0 MB
[runlim] sample:		6546.6 time, 1660.6 real, 777.0 MB
[runlim] sample:		6586.1 time, 1670.6 real, 781.0 MB
[runlim] sample:		6625.8 time, 1680.6 real, 781.2 MB
[runlim] sample:		6665.4 time, 1690.6 real, 781.7 MB
[runlim] sample:		6705.0 time, 1700.6 real, 782.5 MB
[runlim] sample:		6744.6 time, 1710.6 real, 794.5 MB
[runlim] sample:		6784.2 time, 1720.6 real, 794.8 MB
[runlim] sample:		6823.8 time, 1730.6 real, 760.8 MB
[runlim] sample:		6863.4 time, 1740.6 real, 763.6 MB
[runlim] sample:		6903.0 time, 1750.6 real, 762.3 MB
[runlim] sample:		6942.6 time, 1760.6 real, 765.1 MB
[runlim] sample:		6982.2 time, 1770.6 real, 765.3 MB
[runlim] sample:		7021.8 time, 1780.6 real, 769.4 MB
[runlim] sample:		7061.4 time, 1790.6 real, 770.0 MB
[runlim] sample:		7101.0 time, 1800.6 real, 774.0 MB
[runlim] sample:		7140.6 time, 1810.6 real, 772.5 MB
[runlim] sample:		7180.2 time, 1820.6 real, 774.5 MB
[runlim] sample:		7219.8 time, 1830.6 real, 768.5 MB
[runlim] sample:		7259.4 time, 1840.6 real, 688.8 MB
[runlim] sample:		7299.0 time, 1850.6 real, 692.6 MB
[runlim] sample:		7338.6 time, 1860.6 real, 694.5 MB
[runlim] sample:		7378.2 time, 1870.6 real, 699.0 MB
[runlim] sample:		7417.8 time, 1880.6 real, 701.0 MB
[runlim] sample:		7457.4 time, 1890.6 real, 703.0 MB
[runlim] sample:		7497.0 time, 1900.6 real, 703.0 MB
[runlim] sample:		7536.6 time, 1910.6 real, 704.0 MB
[runlim] sample:		7576.2 time, 1920.6 real, 709.6 MB
[runlim] sample:		7615.9 time, 1930.6 real, 711.6 MB
[runlim] sample:		7655.4 time, 1940.6 real, 705.9 MB
[runlim] sample:		7695.1 time, 1950.6 real, 707.9 MB
[runlim] sample:		7734.7 time, 1960.6 real, 709.9 MB
[runlim] sample:		7774.3 time, 1970.6 real, 712.7 MB
[runlim] sample:		7813.9 time, 1980.6 real, 716.0 MB
[runlim] sample:		7853.5 time, 1990.6 real, 721.9 MB
[runlim] sample:		7893.1 time, 2000.6 real, 721.9 MB
[runlim] sample:		7932.7 time, 2010.6 real, 724.1 MB
[runlim] sample:		7972.3 time, 2020.6 real, 726.3 MB
[runlim] sample:		8011.9 time, 2030.6 real, 704.5 MB
[runlim] sample:		8051.5 time, 2040.6 real, 710.3 MB
[runlim] sample:		8091.1 time, 2050.6 real, 713.1 MB
[runlim] sample:		8130.7 time, 2060.6 real, 709.0 MB
[runlim] sample:		8170.3 time, 2070.6 real, 711.0 MB
[runlim] sample:		8209.9 time, 2080.6 real, 711.0 MB
[runlim] sample:		8249.5 time, 2090.6 real, 711.2 MB
[runlim] sample:		8289.1 time, 2100.6 real, 713.2 MB
[runlim] sample:		8328.7 time, 2110.6 real, 717.9 MB
[runlim] sample:		8368.3 time, 2120.6 real, 720.1 MB
[runlim] sample:		8407.9 time, 2130.6 real, 716.5 MB
[runlim] sample:		8447.5 time, 2140.6 real, 717.8 MB
[runlim] sample:		8487.1 time, 2150.6 real, 719.8 MB
[runlim] sample:		8526.7 time, 2160.6 real, 720.3 MB
[runlim] sample:		8566.3 time, 2170.6 real, 722.8 MB
[runlim] sample:		8605.9 time, 2180.6 real, 723.8 MB
[runlim] sample:		8645.5 time, 2190.6 real, 726.8 MB
[runlim] sample:		8685.1 time, 2200.6 real, 738.9 MB
[runlim] sample:		8724.7 time, 2210.6 real, 741.1 MB
[runlim] sample:		8764.3 time, 2220.6 real, 747.6 MB
[runlim] sample:		8803.9 time, 2230.6 real, 749.6 MB
[runlim] sample:		8843.5 time, 2240.6 real, 754.0 MB
[runlim] sample:		8883.1 time, 2250.6 real, 762.5 MB
[runlim] sample:		8922.7 time, 2260.6 real, 762.5 MB
[runlim] sample:		8962.3 time, 2270.6 real, 764.8 MB
[runlim] sample:		9001.9 time, 2280.6 real, 765.0 MB
[runlim] sample:		9041.5 time, 2290.6 real, 761.2 MB
[runlim] sample:		9081.1 time, 2300.6 real, 773.8 MB
[runlim] sample:		9120.7 time, 2310.6 real, 775.7 MB
[runlim] sample:		9160.3 time, 2320.6 real, 772.1 MB
[runlim] sample:		9199.9 time, 2330.6 real, 774.1 MB
[runlim] sample:		9239.5 time, 2340.6 real, 774.1 MB
[runlim] sample:		9279.1 time, 2350.6 real, 776.1 MB
[runlim] sample:		9318.7 time, 2360.6 real, 780.1 MB
[runlim] sample:		9358.3 time, 2370.6 real, 780.4 MB
[runlim] sample:		9397.9 time, 2380.6 real, 782.4 MB
[runlim] sample:		9437.5 time, 2390.6 real, 784.6 MB
[runlim] sample:		9477.1 time, 2400.6 real, 784.6 MB
[runlim] sample:		9516.8 time, 2410.6 real, 787.4 MB
[runlim] sample:		9556.4 time, 2420.6 real, 791.4 MB
[runlim] sample:		9596.0 time, 2430.6 real, 791.9 MB
[runlim] sample:		9635.5 time, 2440.6 real, 800.1 MB
[runlim] sample:		9675.1 time, 2450.6 real, 800.9 MB
[runlim] sample:		9714.8 time, 2460.6 real, 801.4 MB
[runlim] sample:		9754.4 time, 2470.6 real, 802.1 MB
[runlim] sample:		9793.9 time, 2480.6 real, 804.1 MB
[runlim] sample:		9833.5 time, 2490.6 real, 804.9 MB
[runlim] sample:		9873.1 time, 2500.6 real, 809.9 MB
[runlim] sample:		9912.7 time, 2510.6 real, 809.9 MB
[runlim] sample:		9952.3 time, 2520.6 real, 812.4 MB
[runlim] sample:		9991.9 time, 2530.6 real, 812.4 MB
[runlim] sample:		10031.5 time, 2540.6 real, 812.7 MB
[runlim] sample:		10071.1 time, 2550.6 real, 818.2 MB
[runlim] sample:		10110.7 time, 2560.6 real, 818.4 MB
[runlim] sample:		10150.3 time, 2570.6 real, 828.2 MB
[runlim] sample:		10189.9 time, 2580.6 real, 822.0 MB
[runlim] sample:		10229.5 time, 2590.6 real, 822.2 MB
[runlim] sample:		10269.1 time, 2600.6 real, 824.2 MB
[runlim] sample:		10308.7 time, 2610.6 real, 824.2 MB
[runlim] sample:		10348.3 time, 2620.6 real, 826.2 MB
[runlim] sample:		10387.9 time, 2630.6 real, 828.2 MB
[runlim] sample:		10427.5 time, 2640.6 real, 828.2 MB
[runlim] sample:		10467.1 time, 2650.6 real, 837.1 MB
[runlim] sample:		10506.7 time, 2660.6 real, 841.1 MB
[runlim] sample:		10546.3 time, 2670.6 real, 841.1 MB
[runlim] sample:		10585.9 time, 2680.6 real, 841.1 MB
[runlim] sample:		10625.5 time, 2690.6 real, 843.4 MB
[runlim] sample:		10665.1 time, 2700.6 real, 843.6 MB
[runlim] sample:		10704.7 time, 2710.6 real, 843.6 MB
[runlim] sample:		10744.3 time, 2720.6 real, 847.6 MB
[runlim] sample:		10783.9 time, 2730.6 real, 847.9 MB
[runlim] sample:		10823.5 time, 2740.6 real, 838.2 MB
[runlim] sample:		10863.1 time, 2750.6 real, 838.2 MB
[runlim] sample:		10902.7 time, 2760.6 real, 850.7 MB
[runlim] sample:		10942.3 time, 2770.6 real, 852.7 MB
[runlim] sample:		10981.9 time, 2780.6 real, 852.7 MB
[runlim] sample:		11021.5 time, 2790.6 real, 852.7 MB
[runlim] sample:		11061.1 time, 2800.6 real, 854.7 MB
[runlim] sample:		11100.7 time, 2810.6 real, 854.7 MB
[runlim] sample:		11140.3 time, 2820.6 real, 855.0 MB
[runlim] sample:		11179.9 time, 2830.6 real, 859.0 MB
[runlim] sample:		11219.5 time, 2840.6 real, 860.3 MB
[runlim] sample:		11259.1 time, 2850.6 real, 860.3 MB
[runlim] sample:		11298.8 time, 2860.6 real, 862.5 MB
[runlim] sample:		11338.4 time, 2870.6 real, 862.5 MB
[runlim] sample:		11378.0 time, 2880.6 real, 866.5 MB
[runlim] sample:		11417.6 time, 2890.6 real, 765.6 MB
[runlim] sample:		11457.2 time, 2900.6 real, 768.9 MB
[runlim] sample:		11496.8 time, 2910.6 real, 772.1 MB
[runlim] sample:		11536.4 time, 2920.6 real, 772.1 MB
[runlim] sample:		11576.0 time, 2930.6 real, 782.9 MB
[runlim] sample:		11615.6 time, 2940.6 real, 784.9 MB
[runlim] sample:		11655.2 time, 2950.6 real, 788.4 MB
[runlim] sample:		11694.8 time, 2960.6 real, 790.4 MB
[runlim] sample:		11734.4 time, 2970.6 real, 792.4 MB
[runlim] sample:		11774.0 time, 2980.6 real, 794.4 MB
[runlim] sample:		11813.6 time, 2990.6 real, 794.4 MB
[runlim] sample:		11853.2 time, 3000.6 real, 796.4 MB
[runlim] sample:		11892.8 time, 3010.6 real, 796.6 MB
[runlim] sample:		11932.4 time, 3020.6 real, 801.9 MB
[runlim] sample:		11972.0 time, 3030.6 real, 801.9 MB
[runlim] sample:		12011.6 time, 3040.6 real, 803.9 MB
[runlim] sample:		12051.2 time, 3050.6 real, 805.9 MB
[runlim] sample:		12090.8 time, 3060.6 real, 806.2 MB
[runlim] sample:		12130.4 time, 3070.6 real, 808.2 MB
[runlim] sample:		12170.0 time, 3080.6 real, 808.2 MB
[runlim] sample:		12209.6 time, 3090.6 real, 810.2 MB
[runlim] sample:		12249.2 time, 3100.6 real, 812.2 MB
[runlim] sample:		12288.8 time, 3110.6 real, 812.2 MB
[runlim] sample:		12328.4 time, 3120.6 real, 814.2 MB
[runlim] sample:		12368.0 time, 3130.6 real, 814.2 MB
[runlim] sample:		12407.6 time, 3140.6 real, 807.4 MB
[runlim] sample:		12447.2 time, 3150.6 real, 807.4 MB
[runlim] sample:		12486.8 time, 3160.6 real, 809.4 MB
[runlim] sample:		12526.4 time, 3170.6 real, 809.4 MB
[runlim] sample:		12566.0 time, 3180.6 real, 810.4 MB
[runlim] sample:		12605.6 time, 3190.6 real, 813.4 MB
[runlim] sample:		12645.2 time, 3200.6 real, 813.4 MB
[runlim] sample:		12684.8 time, 3210.6 real, 813.4 MB
[runlim] sample:		12724.4 time, 3220.6 real, 815.4 MB
[runlim] sample:		12764.0 time, 3230.6 real, 815.4 MB
[runlim] sample:		12803.6 time, 3240.6 real, 817.4 MB
[runlim] sample:		12843.2 time, 3250.6 real, 817.4 MB
[runlim] sample:		12882.8 time, 3260.6 real, 819.4 MB
[runlim] sample:		12922.4 time, 3270.6 real, 819.4 MB
[runlim] sample:		12962.0 time, 3280.6 real, 821.4 MB
[runlim] sample:		13001.6 time, 3290.6 real, 821.4 MB
[runlim] sample:		13041.2 time, 3300.6 real, 821.4 MB
[runlim] sample:		13080.8 time, 3310.6 real, 825.4 MB
[runlim] sample:		13120.4 time, 3320.6 real, 825.4 MB
[runlim] sample:		13160.0 time, 3330.6 real, 825.4 MB
[runlim] sample:		13199.6 time, 3340.6 real, 827.4 MB
[runlim] sample:		13239.2 time, 3350.6 real, 827.4 MB
[runlim] sample:		13278.8 time, 3360.6 real, 827.8 MB
[runlim] sample:		13318.4 time, 3370.6 real, 829.8 MB
[runlim] sample:		13358.0 time, 3380.6 real, 829.8 MB
[runlim] sample:		13397.6 time, 3390.6 real, 839.6 MB
[runlim] sample:		13437.2 time, 3400.6 real, 841.6 MB
[runlim] sample:		13476.8 time, 3410.6 real, 841.6 MB
[runlim] sample:		13516.4 time, 3420.6 real, 841.6 MB
[runlim] sample:		13556.0 time, 3430.6 real, 843.6 MB
[runlim] sample:		13595.6 time, 3440.6 real, 843.9 MB
[runlim] sample:		13635.2 time, 3450.6 real, 845.9 MB
[runlim] sample:		13674.8 time, 3460.6 real, 846.4 MB
[runlim] sample:		13714.4 time, 3470.6 real, 846.4 MB
[runlim] sample:		13754.0 time, 3480.6 real, 848.4 MB
[runlim] sample:		13793.6 time, 3490.6 real, 848.6 MB
[runlim] sample:		13833.2 time, 3500.6 real, 848.6 MB
[runlim] sample:		13872.8 time, 3510.6 real, 850.9 MB
[runlim] sample:		13912.4 time, 3520.6 real, 851.1 MB
[runlim] sample:		13952.0 time, 3530.6 real, 842.7 MB
[runlim] sample:		13991.6 time, 3540.6 real, 842.7 MB
[runlim] sample:		14031.2 time, 3550.6 real, 844.9 MB
[runlim] sample:		14070.8 time, 3560.6 real, 844.9 MB
[runlim] sample:		14110.4 time, 3570.6 real, 845.4 MB
[runlim] sample:		14150.0 time, 3580.6 real, 848.2 MB
[runlim] sample:		14189.6 time, 3590.6 real, 843.0 MB
[runlim] end:			Tue Sep 15 18:00:14 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.04 seconds
[runlim] time:			14226.78 seconds
[runlim] space:			875.6 MB
[runlim] samples:		35994
