[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/beemptrsn7f1.aig
[runlim] start:			Wed Sep 16 19:00:26 2015
[runlim] main pid:		28125
[runlim] sample:		38.8 time, 10.6 real, 60.8 MB
[runlim] sample:		78.5 time, 20.6 real, 78.9 MB
[runlim] sample:		118.2 time, 30.6 real, 85.0 MB
[runlim] sample:		157.8 time, 40.6 real, 99.0 MB
[runlim] sample:		197.5 time, 50.6 real, 120.7 MB
[runlim] sample:		237.2 time, 60.6 real, 130.3 MB
[runlim] sample:		276.8 time, 70.6 real, 130.6 MB
[runlim] sample:		316.4 time, 80.6 real, 147.3 MB
[runlim] sample:		356.1 time, 90.6 real, 161.4 MB
[runlim] sample:		395.7 time, 100.6 real, 163.9 MB
[runlim] sample:		435.4 time, 110.6 real, 171.2 MB
[runlim] sample:		475.0 time, 120.6 real, 179.3 MB
[runlim] sample:		514.7 time, 130.6 real, 181.7 MB
[runlim] sample:		554.3 time, 140.6 real, 193.1 MB
[runlim] sample:		593.9 time, 150.6 real, 197.7 MB
[runlim] sample:		633.6 time, 160.6 real, 193.7 MB
[runlim] sample:		673.2 time, 170.6 real, 206.0 MB
[runlim] sample:		712.8 time, 180.6 real, 205.7 MB
[runlim] sample:		752.5 time, 190.6 real, 210.9 MB
[runlim] sample:		792.1 time, 200.6 real, 217.4 MB
[runlim] sample:		831.7 time, 210.6 real, 235.0 MB
[runlim] sample:		871.4 time, 220.6 real, 231.9 MB
[runlim] sample:		911.0 time, 230.6 real, 237.8 MB
[runlim] sample:		950.6 time, 240.6 real, 303.5 MB
[runlim] sample:		990.2 time, 250.6 real, 298.1 MB
[runlim] sample:		1029.8 time, 260.6 real, 300.4 MB
[runlim] sample:		1069.5 time, 270.6 real, 307.8 MB
[runlim] sample:		1109.1 time, 280.6 real, 311.7 MB
[runlim] sample:		1148.7 time, 290.6 real, 301.3 MB
[runlim] sample:		1188.3 time, 300.6 real, 294.4 MB
[runlim] sample:		1227.9 time, 310.6 real, 301.4 MB
[runlim] sample:		1267.5 time, 320.6 real, 317.2 MB
[runlim] sample:		1307.2 time, 330.6 real, 320.4 MB
[runlim] sample:		1346.8 time, 340.6 real, 320.5 MB
[runlim] sample:		1386.4 time, 350.6 real, 324.7 MB
[runlim] sample:		1426.0 time, 360.6 real, 331.4 MB
[runlim] sample:		1465.6 time, 370.6 real, 342.7 MB
[runlim] sample:		1505.2 time, 380.6 real, 342.0 MB
[runlim] sample:		1544.8 time, 390.6 real, 339.2 MB
[runlim] sample:		1584.4 time, 400.6 real, 346.9 MB
[runlim] sample:		1624.0 time, 410.6 real, 330.7 MB
[runlim] sample:		1663.7 time, 420.6 real, 343.2 MB
[runlim] sample:		1703.3 time, 430.6 real, 345.4 MB
[runlim] sample:		1742.9 time, 440.6 real, 346.1 MB
[runlim] sample:		1782.5 time, 450.6 real, 348.4 MB
[runlim] sample:		1822.1 time, 460.6 real, 357.3 MB
[runlim] sample:		1861.8 time, 470.6 real, 361.6 MB
[runlim] sample:		1901.4 time, 480.6 real, 347.1 MB
[runlim] sample:		1941.0 time, 490.6 real, 351.1 MB
[runlim] sample:		1980.6 time, 500.6 real, 357.0 MB
[runlim] sample:		2020.2 time, 510.6 real, 364.1 MB
[runlim] sample:		2059.8 time, 520.6 real, 352.0 MB
[runlim] sample:		2099.4 time, 530.6 real, 367.8 MB
[runlim] sample:		2139.0 time, 540.6 real, 350.2 MB
[runlim] sample:		2178.7 time, 550.6 real, 364.4 MB
[runlim] sample:		2218.3 time, 560.6 real, 387.0 MB
[runlim] sample:		2257.9 time, 570.6 real, 410.6 MB
[runlim] sample:		2297.5 time, 580.6 real, 415.1 MB
[runlim] sample:		2337.1 time, 590.6 real, 392.9 MB
[runlim] sample:		2376.7 time, 600.6 real, 385.1 MB
[runlim] sample:		2416.3 time, 610.6 real, 379.9 MB
[runlim] sample:		2456.0 time, 620.6 real, 382.5 MB
[runlim] sample:		2495.6 time, 630.6 real, 391.1 MB
[runlim] sample:		2535.2 time, 640.6 real, 396.2 MB
[runlim] sample:		2574.8 time, 650.6 real, 385.0 MB
[runlim] sample:		2614.4 time, 660.6 real, 387.0 MB
[runlim] sample:		2654.0 time, 670.6 real, 392.8 MB
[runlim] sample:		2693.6 time, 680.6 real, 395.8 MB
[runlim] sample:		2733.2 time, 690.6 real, 400.3 MB
[runlim] sample:		2772.9 time, 700.6 real, 402.8 MB
[runlim] sample:		2812.5 time, 710.6 real, 405.6 MB
[runlim] sample:		2852.1 time, 720.6 real, 399.9 MB
[runlim] sample:		2891.7 time, 730.6 real, 400.4 MB
[runlim] sample:		2931.3 time, 740.6 real, 409.0 MB
[runlim] sample:		2970.9 time, 750.6 real, 408.0 MB
[runlim] sample:		3010.5 time, 760.6 real, 407.0 MB
[runlim] sample:		3050.1 time, 770.6 real, 403.7 MB
[runlim] sample:		3089.7 time, 780.6 real, 409.0 MB
[runlim] sample:		3129.3 time, 790.6 real, 423.7 MB
[runlim] sample:		3168.9 time, 800.6 real, 429.2 MB
[runlim] sample:		3208.6 time, 810.6 real, 432.6 MB
[runlim] sample:		3248.2 time, 820.6 real, 442.4 MB
[runlim] sample:		3287.7 time, 830.6 real, 454.4 MB
[runlim] sample:		3327.3 time, 840.6 real, 437.8 MB
[runlim] sample:		3366.9 time, 850.6 real, 454.6 MB
[runlim] sample:		3406.5 time, 860.6 real, 460.7 MB
[runlim] sample:		3446.1 time, 870.6 real, 461.5 MB
[runlim] sample:		3485.8 time, 880.6 real, 465.9 MB
[runlim] sample:		3525.4 time, 890.6 real, 458.3 MB
[runlim] sample:		3565.0 time, 900.6 real, 440.9 MB
[runlim] sample:		3604.6 time, 910.6 real, 447.9 MB
[runlim] sample:		3644.2 time, 920.6 real, 452.0 MB
[runlim] sample:		3683.8 time, 930.6 real, 456.5 MB
[runlim] sample:		3723.4 time, 940.6 real, 464.3 MB
[runlim] sample:		3763.0 time, 950.6 real, 457.5 MB
[runlim] sample:		3802.6 time, 960.6 real, 464.5 MB
[runlim] sample:		3842.2 time, 970.6 real, 475.0 MB
[runlim] sample:		3881.8 time, 980.6 real, 475.5 MB
[runlim] sample:		3921.4 time, 990.6 real, 473.4 MB
[runlim] sample:		3961.0 time, 1000.6 real, 482.0 MB
[runlim] sample:		4000.6 time, 1010.6 real, 474.9 MB
[runlim] sample:		4040.2 time, 1020.6 real, 474.5 MB
[runlim] sample:		4079.9 time, 1030.6 real, 481.9 MB
[runlim] sample:		4119.5 time, 1040.6 real, 487.0 MB
[runlim] sample:		4159.1 time, 1050.6 real, 489.8 MB
[runlim] sample:		4198.7 time, 1060.6 real, 482.8 MB
[runlim] sample:		4238.3 time, 1070.6 real, 480.9 MB
[runlim] sample:		4277.9 time, 1080.6 real, 483.4 MB
[runlim] sample:		4317.5 time, 1090.6 real, 489.5 MB
[runlim] sample:		4357.1 time, 1100.6 real, 490.3 MB
[runlim] sample:		4396.7 time, 1110.6 real, 493.8 MB
[runlim] sample:		4436.3 time, 1120.6 real, 476.7 MB
[runlim] sample:		4475.9 time, 1130.6 real, 476.7 MB
[runlim] sample:		4515.5 time, 1140.6 real, 490.3 MB
[runlim] sample:		4555.1 time, 1150.6 real, 485.7 MB
[runlim] sample:		4594.7 time, 1160.6 real, 491.9 MB
[runlim] sample:		4634.4 time, 1170.6 real, 482.7 MB
[runlim] sample:		4673.9 time, 1180.6 real, 492.5 MB
[runlim] sample:		4713.6 time, 1190.6 real, 484.3 MB
[runlim] sample:		4753.2 time, 1200.6 real, 480.9 MB
[runlim] sample:		4792.8 time, 1210.6 real, 485.5 MB
[runlim] sample:		4832.4 time, 1220.6 real, 480.3 MB
[runlim] sample:		4872.0 time, 1230.6 real, 483.4 MB
[runlim] sample:		4911.6 time, 1240.6 real, 495.3 MB
[runlim] sample:		4951.2 time, 1250.6 real, 498.1 MB
[runlim] sample:		4990.8 time, 1260.6 real, 489.0 MB
[runlim] sample:		5030.4 time, 1270.6 real, 489.2 MB
[runlim] sample:		5070.0 time, 1280.6 real, 496.0 MB
[runlim] sample:		5109.6 time, 1290.6 real, 491.0 MB
[runlim] sample:		5149.2 time, 1300.6 real, 502.5 MB
[runlim] sample:		5188.8 time, 1310.6 real, 504.5 MB
[runlim] sample:		5228.4 time, 1320.6 real, 506.5 MB
[runlim] sample:		5268.0 time, 1330.6 real, 509.0 MB
[runlim] sample:		5307.6 time, 1340.6 real, 486.5 MB
[runlim] sample:		5347.2 time, 1350.6 real, 498.7 MB
[runlim] sample:		5386.8 time, 1360.6 real, 498.8 MB
[runlim] sample:		5426.4 time, 1370.6 real, 502.8 MB
[runlim] sample:		5466.0 time, 1380.6 real, 501.4 MB
[runlim] sample:		5505.6 time, 1390.6 real, 504.9 MB
[runlim] sample:		5545.2 time, 1400.6 real, 502.4 MB
[runlim] sample:		5584.8 time, 1410.6 real, 512.9 MB
[runlim] sample:		5624.4 time, 1420.6 real, 517.6 MB
[runlim] sample:		5664.0 time, 1430.6 real, 511.4 MB
[runlim] sample:		5703.6 time, 1440.6 real, 527.5 MB
[runlim] sample:		5743.2 time, 1450.6 real, 529.5 MB
[runlim] sample:		5782.8 time, 1460.6 real, 517.3 MB
[runlim] sample:		5822.4 time, 1470.6 real, 517.3 MB
[runlim] sample:		5862.0 time, 1480.6 real, 526.3 MB
[runlim] sample:		5901.6 time, 1490.6 real, 546.5 MB
[runlim] sample:		5941.2 time, 1500.6 real, 546.8 MB
[runlim] sample:		5980.8 time, 1510.6 real, 587.8 MB
[runlim] sample:		6020.4 time, 1520.6 real, 594.6 MB
[runlim] sample:		6060.0 time, 1530.6 real, 596.8 MB
[runlim] sample:		6099.6 time, 1540.6 real, 592.8 MB
[runlim] sample:		6139.2 time, 1550.6 real, 594.8 MB
[runlim] sample:		6178.8 time, 1560.6 real, 598.0 MB
[runlim] sample:		6218.4 time, 1570.6 real, 596.5 MB
[runlim] sample:		6258.0 time, 1580.6 real, 590.6 MB
[runlim] sample:		6297.6 time, 1590.6 real, 576.1 MB
[runlim] sample:		6337.2 time, 1600.6 real, 578.8 MB
[runlim] sample:		6376.8 time, 1610.6 real, 576.5 MB
[runlim] sample:		6416.3 time, 1620.6 real, 576.4 MB
[runlim] sample:		6455.9 time, 1630.6 real, 578.9 MB
[runlim] sample:		6495.5 time, 1640.6 real, 591.4 MB
[runlim] sample:		6535.1 time, 1650.6 real, 595.9 MB
[runlim] sample:		6574.7 time, 1660.6 real, 605.7 MB
[runlim] sample:		6614.3 time, 1670.6 real, 613.8 MB
[runlim] sample:		6653.9 time, 1680.6 real, 600.8 MB
[runlim] sample:		6693.5 time, 1690.6 real, 594.9 MB
[runlim] sample:		6733.1 time, 1700.6 real, 597.9 MB
[runlim] sample:		6772.7 time, 1710.6 real, 574.4 MB
[runlim] sample:		6812.3 time, 1720.6 real, 574.4 MB
[runlim] sample:		6851.9 time, 1730.6 real, 581.4 MB
[runlim] sample:		6891.5 time, 1740.6 real, 585.2 MB
[runlim] sample:		6931.1 time, 1750.6 real, 589.5 MB
[runlim] sample:		6970.7 time, 1760.6 real, 597.8 MB
[runlim] sample:		7010.3 time, 1770.6 real, 589.6 MB
[runlim] sample:		7049.9 time, 1780.6 real, 590.3 MB
[runlim] sample:		7089.5 time, 1790.6 real, 600.8 MB
[runlim] sample:		7129.1 time, 1800.6 real, 603.6 MB
[runlim] sample:		7168.7 time, 1810.6 real, 599.3 MB
[runlim] sample:		7208.3 time, 1820.6 real, 589.2 MB
[runlim] sample:		7247.9 time, 1830.6 real, 593.1 MB
[runlim] sample:		7287.6 time, 1840.6 real, 595.2 MB
[runlim] sample:		7327.2 time, 1850.6 real, 595.4 MB
[runlim] sample:		7366.8 time, 1860.6 real, 595.4 MB
[runlim] sample:		7406.4 time, 1870.6 real, 595.7 MB
[runlim] sample:		7445.9 time, 1880.6 real, 634.2 MB
[runlim] sample:		7485.6 time, 1890.6 real, 609.5 MB
[runlim] sample:		7525.2 time, 1900.6 real, 617.0 MB
[runlim] sample:		7564.8 time, 1910.6 real, 618.2 MB
[runlim] sample:		7604.4 time, 1920.6 real, 632.7 MB
[runlim] sample:		7644.0 time, 1930.6 real, 638.0 MB
[runlim] sample:		7683.6 time, 1940.6 real, 624.5 MB
[runlim] sample:		7723.2 time, 1950.6 real, 624.5 MB
[runlim] sample:		7762.8 time, 1960.6 real, 630.4 MB
[runlim] sample:		7802.4 time, 1970.6 real, 632.4 MB
[runlim] sample:		7842.0 time, 1980.6 real, 639.9 MB
[runlim] sample:		7881.6 time, 1990.6 real, 642.4 MB
[runlim] sample:		7921.2 time, 2000.6 real, 616.7 MB
[runlim] sample:		7960.8 time, 2010.6 real, 625.0 MB
[runlim] sample:		8000.4 time, 2020.6 real, 639.0 MB
[runlim] sample:		8040.0 time, 2030.6 real, 641.0 MB
[runlim] sample:		8079.6 time, 2040.6 real, 634.7 MB
[runlim] sample:		8119.2 time, 2050.6 real, 640.1 MB
[runlim] sample:		8158.8 time, 2060.6 real, 642.4 MB
[runlim] sample:		8198.4 time, 2070.6 real, 629.1 MB
[runlim] sample:		8238.0 time, 2080.6 real, 629.1 MB
[runlim] sample:		8277.6 time, 2090.6 real, 643.1 MB
[runlim] sample:		8317.2 time, 2100.6 real, 645.1 MB
[runlim] sample:		8356.8 time, 2110.6 real, 647.1 MB
[runlim] sample:		8396.5 time, 2120.6 real, 650.6 MB
[runlim] sample:		8436.0 time, 2130.6 real, 621.1 MB
[runlim] sample:		8475.6 time, 2140.6 real, 621.1 MB
[runlim] sample:		8515.2 time, 2150.6 real, 651.4 MB
[runlim] sample:		8554.8 time, 2160.6 real, 655.4 MB
[runlim] sample:		8594.4 time, 2170.6 real, 657.9 MB
[runlim] sample:		8634.0 time, 2180.6 real, 661.2 MB
[runlim] sample:		8673.6 time, 2190.6 real, 663.2 MB
[runlim] sample:		8713.2 time, 2200.6 real, 637.6 MB
[runlim] sample:		8752.8 time, 2210.6 real, 649.9 MB
[runlim] sample:		8792.4 time, 2220.6 real, 654.4 MB
[runlim] sample:		8832.0 time, 2230.6 real, 649.9 MB
[runlim] sample:		8871.6 time, 2240.6 real, 660.2 MB
[runlim] sample:		8911.2 time, 2250.6 real, 669.1 MB
[runlim] sample:		8950.8 time, 2260.6 real, 672.1 MB
[runlim] sample:		8990.4 time, 2270.6 real, 633.1 MB
[runlim] sample:		9030.0 time, 2280.6 real, 634.9 MB
[runlim] sample:		9069.6 time, 2290.6 real, 634.9 MB
[runlim] sample:		9109.2 time, 2300.6 real, 648.9 MB
[runlim] sample:		9148.8 time, 2310.6 real, 653.4 MB
[runlim] sample:		9188.4 time, 2320.6 real, 657.6 MB
[runlim] sample:		9228.0 time, 2330.6 real, 666.4 MB
[runlim] sample:		9267.6 time, 2340.6 real, 673.7 MB
[runlim] sample:		9307.2 time, 2350.6 real, 650.2 MB
[runlim] sample:		9346.8 time, 2360.6 real, 654.2 MB
[runlim] sample:		9386.4 time, 2370.6 real, 666.4 MB
[runlim] sample:		9426.0 time, 2380.6 real, 668.4 MB
[runlim] sample:		9465.6 time, 2390.6 real, 666.7 MB
[runlim] sample:		9505.2 time, 2400.6 real, 677.5 MB
[runlim] sample:		9544.8 time, 2410.6 real, 677.5 MB
[runlim] sample:		9584.4 time, 2420.6 real, 680.5 MB
[runlim] sample:		9624.0 time, 2430.6 real, 683.8 MB
[runlim] sample:		9663.6 time, 2440.6 real, 660.0 MB
[runlim] sample:		9703.2 time, 2450.6 real, 660.0 MB
[runlim] sample:		9742.8 time, 2460.6 real, 687.9 MB
[runlim] sample:		9782.4 time, 2470.6 real, 693.9 MB
[runlim] sample:		9822.0 time, 2480.6 real, 698.0 MB
[runlim] sample:		9861.6 time, 2490.6 real, 700.0 MB
[runlim] sample:		9901.2 time, 2500.6 real, 700.0 MB
[runlim] sample:		9940.8 time, 2510.6 real, 702.7 MB
[runlim] sample:		9980.4 time, 2520.6 real, 682.0 MB
[runlim] sample:		10020.0 time, 2530.6 real, 682.0 MB
[runlim] sample:		10059.6 time, 2540.6 real, 688.0 MB
[runlim] sample:		10099.2 time, 2550.6 real, 696.3 MB
[runlim] sample:		10138.8 time, 2560.6 real, 698.3 MB
[runlim] sample:		10178.4 time, 2570.6 real, 700.3 MB
[runlim] sample:		10218.0 time, 2580.6 real, 702.8 MB
[runlim] sample:		10257.6 time, 2590.6 real, 690.5 MB
[runlim] sample:		10297.2 time, 2600.6 real, 690.8 MB
[runlim] sample:		10336.8 time, 2610.6 real, 702.8 MB
[runlim] sample:		10376.4 time, 2620.6 real, 717.0 MB
[runlim] sample:		10416.0 time, 2630.6 real, 719.3 MB
[runlim] sample:		10455.6 time, 2640.6 real, 721.3 MB
[runlim] sample:		10495.2 time, 2650.6 real, 723.8 MB
[runlim] sample:		10534.8 time, 2660.6 real, 729.3 MB
[runlim] sample:		10574.4 time, 2670.6 real, 705.5 MB
[runlim] sample:		10614.0 time, 2680.6 real, 705.8 MB
[runlim] sample:		10653.6 time, 2690.6 real, 706.0 MB
[runlim] sample:		10693.2 time, 2700.6 real, 708.0 MB
[runlim] sample:		10732.8 time, 2710.6 real, 714.8 MB
[runlim] sample:		10772.4 time, 2720.6 real, 717.8 MB
[runlim] sample:		10812.0 time, 2730.6 real, 710.5 MB
[runlim] sample:		10851.6 time, 2740.6 real, 690.0 MB
[runlim] sample:		10891.2 time, 2750.6 real, 698.0 MB
[runlim] sample:		10930.9 time, 2760.6 real, 703.2 MB
[runlim] sample:		10970.5 time, 2770.6 real, 705.2 MB
[runlim] sample:		11010.1 time, 2780.6 real, 709.7 MB
[runlim] sample:		11049.7 time, 2790.6 real, 712.9 MB
[runlim] sample:		11089.3 time, 2800.6 real, 705.4 MB
[runlim] sample:		11128.9 time, 2810.6 real, 679.9 MB
[runlim] sample:		11168.5 time, 2820.6 real, 679.9 MB
[runlim] sample:		11208.1 time, 2830.6 real, 679.9 MB
[runlim] sample:		11247.7 time, 2840.6 real, 693.9 MB
[runlim] sample:		11287.3 time, 2850.6 real, 697.7 MB
[runlim] sample:		11326.9 time, 2860.6 real, 700.4 MB
[runlim] sample:		11366.5 time, 2870.6 real, 707.8 MB
[runlim] sample:		11406.1 time, 2880.6 real, 717.4 MB
[runlim] sample:		11445.7 time, 2890.6 real, 691.6 MB
[runlim] sample:		11485.3 time, 2900.6 real, 710.9 MB
[runlim] sample:		11524.9 time, 2910.6 real, 711.2 MB
[runlim] sample:		11564.5 time, 2920.6 real, 715.8 MB
[runlim] sample:		11604.1 time, 2930.6 real, 717.8 MB
[runlim] sample:		11643.7 time, 2940.6 real, 719.8 MB
[runlim] sample:		11683.3 time, 2950.6 real, 723.0 MB
[runlim] sample:		11722.9 time, 2960.6 real, 725.8 MB
[runlim] sample:		11762.5 time, 2970.6 real, 727.3 MB
[runlim] sample:		11802.1 time, 2980.6 real, 718.4 MB
[runlim] sample:		11841.8 time, 2990.6 real, 718.4 MB
[runlim] sample:		11881.4 time, 3000.6 real, 730.7 MB
[runlim] sample:		11921.0 time, 3010.6 real, 733.2 MB
[runlim] sample:		11960.6 time, 3020.6 real, 735.5 MB
[runlim] sample:		12000.2 time, 3030.6 real, 737.7 MB
[runlim] sample:		12039.8 time, 3040.6 real, 750.4 MB
[runlim] sample:		12079.4 time, 3050.6 real, 753.7 MB
[runlim] sample:		12119.0 time, 3060.6 real, 751.4 MB
[runlim] sample:		12158.6 time, 3070.6 real, 708.6 MB
[runlim] sample:		12198.2 time, 3080.6 real, 702.8 MB
[runlim] sample:		12237.8 time, 3090.6 real, 702.8 MB
[runlim] sample:		12277.4 time, 3100.6 real, 716.8 MB
[runlim] sample:		12317.0 time, 3110.6 real, 718.8 MB
[runlim] sample:		12356.6 time, 3120.6 real, 720.8 MB
[runlim] sample:		12396.2 time, 3130.6 real, 724.3 MB
[runlim] sample:		12435.8 time, 3140.6 real, 727.8 MB
[runlim] sample:		12475.4 time, 3150.6 real, 731.1 MB
[runlim] sample:		12515.0 time, 3160.6 real, 731.3 MB
[runlim] sample:		12554.6 time, 3170.6 real, 707.8 MB
[runlim] sample:		12594.2 time, 3180.6 real, 720.0 MB
[runlim] sample:		12633.8 time, 3190.6 real, 718.1 MB
[runlim] sample:		12673.4 time, 3200.6 real, 745.3 MB
[runlim] sample:		12713.0 time, 3210.6 real, 713.6 MB
[runlim] sample:		12752.6 time, 3220.6 real, 728.4 MB
[runlim] sample:		12792.2 time, 3230.6 real, 703.5 MB
[runlim] sample:		12831.8 time, 3240.6 real, 728.5 MB
[runlim] sample:		12871.4 time, 3250.6 real, 743.2 MB
[runlim] sample:		12911.0 time, 3260.6 real, 746.2 MB
[runlim] sample:		12950.6 time, 3270.6 real, 763.2 MB
[runlim] sample:		12990.2 time, 3280.6 real, 765.2 MB
[runlim] sample:		13029.8 time, 3290.6 real, 744.5 MB
[runlim] sample:		13069.4 time, 3300.6 real, 753.3 MB
[runlim] sample:		13109.0 time, 3310.6 real, 737.8 MB
[runlim] sample:		13148.6 time, 3320.6 real, 710.7 MB
[runlim] sample:		13188.3 time, 3330.6 real, 721.1 MB
[runlim] sample:		13227.9 time, 3340.6 real, 744.0 MB
[runlim] sample:		13267.5 time, 3350.6 real, 751.0 MB
[runlim] sample:		13307.1 time, 3360.6 real, 723.9 MB
[runlim] sample:		13346.7 time, 3370.6 real, 739.6 MB
[runlim] sample:		13386.3 time, 3380.6 real, 754.6 MB
[runlim] sample:		13425.9 time, 3390.6 real, 758.6 MB
[runlim] sample:		13465.5 time, 3400.6 real, 740.3 MB
[runlim] sample:		13505.1 time, 3410.6 real, 765.4 MB
[runlim] sample:		13544.7 time, 3420.6 real, 769.4 MB
[runlim] sample:		13584.3 time, 3430.6 real, 772.9 MB
[runlim] sample:		13623.9 time, 3440.6 real, 751.0 MB
[runlim] sample:		13663.5 time, 3450.6 real, 744.1 MB
[runlim] sample:		13703.1 time, 3460.6 real, 732.6 MB
[runlim] sample:		13742.7 time, 3470.6 real, 740.9 MB
[runlim] sample:		13782.3 time, 3480.6 real, 740.9 MB
[runlim] sample:		13822.0 time, 3490.6 real, 757.5 MB
[runlim] sample:		13861.5 time, 3500.6 real, 759.5 MB
[runlim] sample:		13901.1 time, 3510.6 real, 753.2 MB
[runlim] sample:		13940.7 time, 3520.6 real, 755.2 MB
[runlim] sample:		13980.3 time, 3530.6 real, 755.7 MB
[runlim] sample:		14019.9 time, 3540.6 real, 729.2 MB
[runlim] sample:		14039.2 time, 3550.6 real, 376.5 MB
[runlim] end:			Wed Sep 16 19:59:40 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		0
[runlim] real:			3554.87 seconds
[runlim] time:			14043.39 seconds
[runlim] space:			778.9 MB
[runlim] samples:		35542
