[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/beemloyd3b1.aig
[runlim] start:			Wed Sep 16 18:18:46 2015
[runlim] main pid:		5410
[runlim] sample:		37.6 time, 10.2 real, 81.3 MB
[runlim] sample:		77.3 time, 20.2 real, 109.8 MB
[runlim] sample:		116.9 time, 30.2 real, 125.0 MB
[runlim] sample:		156.5 time, 40.2 real, 144.4 MB
[runlim] sample:		196.2 time, 50.2 real, 152.4 MB
[runlim] sample:		235.8 time, 60.2 real, 153.1 MB
[runlim] sample:		275.5 time, 70.2 real, 158.8 MB
[runlim] sample:		315.1 time, 80.2 real, 167.0 MB
[runlim] sample:		354.7 time, 90.2 real, 173.9 MB
[runlim] sample:		394.3 time, 100.2 real, 179.8 MB
[runlim] sample:		433.9 time, 110.2 real, 201.5 MB
[runlim] sample:		473.6 time, 120.2 real, 206.3 MB
[runlim] sample:		513.2 time, 130.2 real, 209.4 MB
[runlim] sample:		552.8 time, 140.2 real, 220.4 MB
[runlim] sample:		592.5 time, 150.2 real, 257.3 MB
[runlim] sample:		632.1 time, 160.2 real, 229.9 MB
[runlim] sample:		671.7 time, 170.2 real, 230.6 MB
[runlim] sample:		711.3 time, 180.2 real, 227.8 MB
[runlim] sample:		751.0 time, 190.2 real, 236.6 MB
[runlim] sample:		790.6 time, 200.2 real, 233.4 MB
[runlim] sample:		830.2 time, 210.2 real, 238.5 MB
[runlim] sample:		869.8 time, 220.2 real, 234.7 MB
[runlim] sample:		909.4 time, 230.2 real, 244.9 MB
[runlim] sample:		949.0 time, 240.2 real, 242.3 MB
[runlim] sample:		988.7 time, 250.2 real, 247.0 MB
[runlim] sample:		1028.3 time, 260.2 real, 249.6 MB
[runlim] sample:		1067.9 time, 270.2 real, 253.1 MB
[runlim] sample:		1107.5 time, 280.2 real, 268.6 MB
[runlim] sample:		1147.1 time, 290.2 real, 276.4 MB
[runlim] sample:		1186.7 time, 300.2 real, 281.7 MB
[runlim] sample:		1226.4 time, 310.2 real, 283.7 MB
[runlim] sample:		1266.0 time, 320.2 real, 283.7 MB
[runlim] sample:		1305.6 time, 330.2 real, 288.8 MB
[runlim] sample:		1345.2 time, 340.2 real, 291.3 MB
[runlim] sample:		1384.8 time, 350.2 real, 390.5 MB
[runlim] sample:		1424.5 time, 360.2 real, 391.7 MB
[runlim] sample:		1464.1 time, 370.2 real, 423.1 MB
[runlim] sample:		1503.7 time, 380.2 real, 404.0 MB
[runlim] sample:		1543.3 time, 390.2 real, 395.8 MB
[runlim] sample:		1583.0 time, 400.2 real, 387.0 MB
[runlim] sample:		1622.6 time, 410.2 real, 390.2 MB
[runlim] sample:		1662.2 time, 420.2 real, 399.6 MB
[runlim] sample:		1701.8 time, 430.2 real, 411.0 MB
[runlim] sample:		1741.4 time, 440.2 real, 410.7 MB
[runlim] sample:		1781.0 time, 450.2 real, 412.5 MB
[runlim] sample:		1820.7 time, 460.2 real, 412.7 MB
[runlim] sample:		1860.3 time, 470.2 real, 422.7 MB
[runlim] sample:		1899.9 time, 480.2 real, 423.9 MB
[runlim] sample:		1939.5 time, 490.2 real, 419.0 MB
[runlim] sample:		1979.1 time, 500.2 real, 423.1 MB
[runlim] sample:		2018.8 time, 510.2 real, 428.9 MB
[runlim] sample:		2058.4 time, 520.2 real, 430.9 MB
[runlim] sample:		2098.0 time, 530.2 real, 437.2 MB
[runlim] sample:		2137.6 time, 540.2 real, 430.0 MB
[runlim] sample:		2177.2 time, 550.2 real, 430.5 MB
[runlim] sample:		2216.8 time, 560.2 real, 440.5 MB
[runlim] sample:		2256.4 time, 570.2 real, 446.4 MB
[runlim] sample:		2296.1 time, 580.2 real, 447.6 MB
[runlim] sample:		2335.7 time, 590.2 real, 443.5 MB
[runlim] sample:		2375.3 time, 600.2 real, 444.9 MB
[runlim] sample:		2414.8 time, 610.2 real, 452.6 MB
[runlim] sample:		2454.4 time, 620.2 real, 472.6 MB
[runlim] sample:		2494.0 time, 630.2 real, 472.6 MB
[runlim] sample:		2533.7 time, 640.2 real, 472.8 MB
[runlim] sample:		2573.3 time, 650.2 real, 473.3 MB
[runlim] sample:		2612.9 time, 660.2 real, 475.5 MB
[runlim] sample:		2652.5 time, 670.2 real, 475.8 MB
[runlim] sample:		2692.1 time, 680.2 real, 494.1 MB
[runlim] sample:		2731.7 time, 690.2 real, 495.5 MB
[runlim] sample:		2771.3 time, 700.2 real, 495.5 MB
[runlim] sample:		2810.9 time, 710.2 real, 499.7 MB
[runlim] sample:		2850.5 time, 720.2 real, 477.7 MB
[runlim] sample:		2890.1 time, 730.2 real, 478.0 MB
[runlim] sample:		2929.8 time, 740.2 real, 478.2 MB
[runlim] sample:		2969.4 time, 750.2 real, 478.4 MB
[runlim] sample:		3009.0 time, 760.2 real, 468.2 MB
[runlim] sample:		3048.6 time, 770.2 real, 479.0 MB
[runlim] sample:		3088.2 time, 780.2 real, 480.1 MB
[runlim] sample:		3127.8 time, 790.2 real, 480.9 MB
[runlim] sample:		3167.4 time, 800.2 real, 482.0 MB
[runlim] sample:		3207.0 time, 810.2 real, 480.2 MB
[runlim] sample:		3246.6 time, 820.2 real, 485.3 MB
[runlim] sample:		3286.2 time, 830.2 real, 485.3 MB
[runlim] sample:		3325.9 time, 840.2 real, 493.3 MB
[runlim] sample:		3365.5 time, 850.2 real, 495.5 MB
[runlim] sample:		3405.1 time, 860.2 real, 506.8 MB
[runlim] sample:		3444.7 time, 870.2 real, 516.6 MB
[runlim] sample:		3484.3 time, 880.2 real, 510.6 MB
[runlim] sample:		3523.9 time, 890.2 real, 514.4 MB
[runlim] sample:		3563.5 time, 900.2 real, 514.4 MB
[runlim] sample:		3603.1 time, 910.2 real, 514.4 MB
[runlim] sample:		3642.7 time, 920.2 real, 516.4 MB
[runlim] sample:		3682.4 time, 930.2 real, 524.4 MB
[runlim] sample:		3721.9 time, 940.2 real, 524.6 MB
[runlim] sample:		3761.6 time, 950.2 real, 524.9 MB
[runlim] sample:		3801.2 time, 960.2 real, 516.2 MB
[runlim] sample:		3840.8 time, 970.2 real, 516.2 MB
[runlim] sample:		3880.4 time, 980.2 real, 516.2 MB
[runlim] sample:		3920.0 time, 990.2 real, 519.9 MB
[runlim] sample:		3959.6 time, 1000.2 real, 519.9 MB
[runlim] sample:		3999.2 time, 1010.2 real, 526.9 MB
[runlim] sample:		4038.8 time, 1020.2 real, 556.9 MB
[runlim] sample:		4078.4 time, 1030.2 real, 550.5 MB
[runlim] sample:		4118.0 time, 1040.2 real, 551.0 MB
[runlim] sample:		4157.6 time, 1050.2 real, 564.0 MB
[runlim] sample:		4197.2 time, 1060.2 real, 566.2 MB
[runlim] sample:		4236.8 time, 1070.2 real, 582.2 MB
[runlim] sample:		4276.4 time, 1080.2 real, 590.7 MB
[runlim] sample:		4316.1 time, 1090.2 real, 592.9 MB
[runlim] sample:		4355.7 time, 1100.2 real, 594.9 MB
[runlim] sample:		4395.3 time, 1110.2 real, 594.9 MB
[runlim] sample:		4434.9 time, 1120.2 real, 594.9 MB
[runlim] sample:		4474.5 time, 1130.2 real, 555.0 MB
[runlim] sample:		4514.1 time, 1140.2 real, 566.0 MB
[runlim] sample:		4553.7 time, 1150.2 real, 566.2 MB
[runlim] sample:		4593.3 time, 1160.2 real, 573.5 MB
[runlim] sample:		4632.9 time, 1170.2 real, 573.8 MB
[runlim] sample:		4672.5 time, 1180.2 real, 574.3 MB
[runlim] sample:		4712.1 time, 1190.2 real, 576.7 MB
[runlim] sample:		4751.8 time, 1200.2 real, 564.4 MB
[runlim] sample:		4791.4 time, 1210.2 real, 564.6 MB
[runlim] sample:		4831.0 time, 1220.2 real, 564.8 MB
[runlim] sample:		4870.6 time, 1230.2 real, 574.6 MB
[runlim] sample:		4910.2 time, 1240.2 real, 574.9 MB
[runlim] sample:		4949.8 time, 1250.2 real, 587.9 MB
[runlim] sample:		4989.4 time, 1260.2 real, 588.4 MB
[runlim] sample:		5029.1 time, 1270.2 real, 590.6 MB
[runlim] sample:		5068.7 time, 1280.2 real, 592.9 MB
[runlim] sample:		5108.3 time, 1290.2 real, 593.1 MB
[runlim] sample:		5147.9 time, 1300.2 real, 595.3 MB
[runlim] sample:		5187.5 time, 1310.2 real, 595.2 MB
[runlim] sample:		5227.1 time, 1320.2 real, 595.2 MB
[runlim] sample:		5266.7 time, 1330.2 real, 597.2 MB
[runlim] sample:		5306.3 time, 1340.2 real, 597.5 MB
[runlim] sample:		5345.9 time, 1350.2 real, 599.5 MB
[runlim] sample:		5385.5 time, 1360.2 real, 582.2 MB
[runlim] sample:		5425.1 time, 1370.2 real, 586.3 MB
[runlim] sample:		5464.7 time, 1380.2 real, 606.3 MB
[runlim] sample:		5504.3 time, 1390.2 real, 608.5 MB
[runlim] sample:		5543.9 time, 1400.2 real, 608.5 MB
[runlim] sample:		5583.5 time, 1410.2 real, 608.5 MB
[runlim] sample:		5623.1 time, 1420.2 real, 610.5 MB
[runlim] sample:		5662.7 time, 1430.2 real, 610.5 MB
[runlim] sample:		5702.3 time, 1440.2 real, 610.5 MB
[runlim] sample:		5741.9 time, 1450.2 real, 610.8 MB
[runlim] sample:		5781.5 time, 1460.2 real, 610.8 MB
[runlim] sample:		5821.1 time, 1470.2 real, 612.8 MB
[runlim] sample:		5860.7 time, 1480.2 real, 612.8 MB
[runlim] sample:		5900.3 time, 1490.2 real, 612.8 MB
[runlim] sample:		5939.9 time, 1500.2 real, 612.8 MB
[runlim] sample:		5979.5 time, 1510.2 real, 612.8 MB
[runlim] sample:		6019.1 time, 1520.2 real, 626.8 MB
[runlim] sample:		6058.8 time, 1530.2 real, 626.8 MB
[runlim] sample:		6098.4 time, 1540.2 real, 626.8 MB
[runlim] sample:		6138.0 time, 1550.2 real, 626.8 MB
[runlim] sample:		6177.6 time, 1560.2 real, 634.3 MB
[runlim] sample:		6217.2 time, 1570.2 real, 590.7 MB
[runlim] sample:		6256.8 time, 1580.2 real, 590.7 MB
[runlim] sample:		6296.4 time, 1590.2 real, 602.4 MB
[runlim] sample:		6336.0 time, 1600.2 real, 604.4 MB
[runlim] sample:		6375.6 time, 1610.2 real, 604.7 MB
[runlim] sample:		6415.2 time, 1620.2 real, 606.4 MB
[runlim] sample:		6454.9 time, 1630.2 real, 606.4 MB
[runlim] sample:		6494.5 time, 1640.2 real, 606.4 MB
[runlim] sample:		6534.1 time, 1650.2 real, 606.4 MB
[runlim] sample:		6573.7 time, 1660.2 real, 606.4 MB
[runlim] sample:		6613.3 time, 1670.2 real, 606.4 MB
[runlim] sample:		6652.9 time, 1680.2 real, 618.4 MB
[runlim] sample:		6692.5 time, 1690.2 real, 620.4 MB
[runlim] sample:		6732.1 time, 1700.2 real, 620.4 MB
[runlim] sample:		6771.8 time, 1710.2 real, 622.4 MB
[runlim] sample:		6811.4 time, 1720.2 real, 624.4 MB
[runlim] sample:		6851.0 time, 1730.2 real, 624.4 MB
[runlim] sample:		6890.6 time, 1740.2 real, 637.4 MB
[runlim] sample:		6930.2 time, 1750.2 real, 637.4 MB
[runlim] sample:		6969.8 time, 1760.2 real, 637.7 MB
[runlim] sample:		7009.4 time, 1770.2 real, 641.9 MB
[runlim] sample:		7049.0 time, 1780.2 real, 643.1 MB
[runlim] sample:		7088.7 time, 1790.2 real, 644.9 MB
[runlim] sample:		7128.3 time, 1800.2 real, 632.8 MB
[runlim] sample:		7167.9 time, 1810.2 real, 632.8 MB
[runlim] sample:		7207.5 time, 1820.2 real, 632.8 MB
[runlim] sample:		7247.1 time, 1830.2 real, 632.8 MB
[runlim] sample:		7286.7 time, 1840.2 real, 634.9 MB
[runlim] sample:		7326.3 time, 1850.2 real, 635.4 MB
[runlim] sample:		7365.9 time, 1860.2 real, 611.6 MB
[runlim] sample:		7405.6 time, 1870.2 real, 613.6 MB
[runlim] sample:		7445.2 time, 1880.2 real, 615.6 MB
[runlim] sample:		7484.8 time, 1890.2 real, 615.6 MB
[runlim] sample:		7524.4 time, 1900.2 real, 625.4 MB
[runlim] sample:		7564.0 time, 1910.2 real, 637.9 MB
[runlim] sample:		7603.6 time, 1920.2 real, 639.9 MB
[runlim] sample:		7643.2 time, 1930.2 real, 639.9 MB
[runlim] sample:		7682.9 time, 1940.2 real, 639.9 MB
[runlim] sample:		7722.5 time, 1950.2 real, 639.9 MB
[runlim] sample:		7762.1 time, 1960.2 real, 641.9 MB
[runlim] sample:		7801.7 time, 1970.2 real, 659.9 MB
[runlim] sample:		7841.3 time, 1980.2 real, 659.9 MB
[runlim] sample:		7880.9 time, 1990.2 real, 657.2 MB
[runlim] sample:		7920.5 time, 2000.2 real, 659.2 MB
[runlim] sample:		7960.1 time, 2010.2 real, 659.2 MB
[runlim] sample:		7999.7 time, 2020.2 real, 659.2 MB
[runlim] sample:		8039.3 time, 2030.2 real, 661.2 MB
[runlim] sample:		8078.9 time, 2040.2 real, 663.3 MB
[runlim] sample:		8118.6 time, 2050.2 real, 663.8 MB
[runlim] sample:		8158.1 time, 2060.2 real, 664.3 MB
[runlim] sample:		8197.8 time, 2070.2 real, 664.8 MB
[runlim] sample:		8237.4 time, 2080.2 real, 653.1 MB
[runlim] sample:		8277.0 time, 2090.2 real, 655.1 MB
[runlim] sample:		8316.6 time, 2100.2 real, 655.1 MB
[runlim] sample:		8356.2 time, 2110.2 real, 655.1 MB
[runlim] sample:		8395.8 time, 2120.2 real, 657.1 MB
[runlim] sample:		8435.4 time, 2130.2 real, 657.1 MB
[runlim] sample:		8475.0 time, 2140.2 real, 657.1 MB
[runlim] sample:		8514.6 time, 2150.2 real, 659.1 MB
[runlim] sample:		8554.2 time, 2160.2 real, 659.1 MB
[runlim] sample:		8593.9 time, 2170.2 real, 661.1 MB
[runlim] sample:		8633.5 time, 2180.2 real, 661.1 MB
[runlim] sample:		8673.1 time, 2190.2 real, 661.1 MB
[runlim] sample:		8712.7 time, 2200.2 real, 661.1 MB
[runlim] sample:		8752.3 time, 2210.2 real, 635.4 MB
[runlim] sample:		8791.9 time, 2220.2 real, 646.0 MB
[runlim] sample:		8831.5 time, 2230.2 real, 646.0 MB
[runlim] sample:		8871.1 time, 2240.2 real, 648.6 MB
[runlim] sample:		8910.7 time, 2250.2 real, 649.6 MB
[runlim] sample:		8950.3 time, 2260.2 real, 649.8 MB
[runlim] sample:		8990.0 time, 2270.2 real, 650.6 MB
[runlim] sample:		9029.6 time, 2280.2 real, 664.8 MB
[runlim] sample:		9069.2 time, 2290.2 real, 680.8 MB
[runlim] sample:		9108.8 time, 2300.2 real, 680.8 MB
[runlim] sample:		9148.4 time, 2310.2 real, 680.8 MB
[runlim] sample:		9188.0 time, 2320.2 real, 684.8 MB
[runlim] sample:		9227.6 time, 2330.2 real, 684.8 MB
[runlim] sample:		9267.2 time, 2340.2 real, 684.8 MB
[runlim] sample:		9306.8 time, 2350.2 real, 688.8 MB
[runlim] sample:		9346.5 time, 2360.2 real, 688.8 MB
[runlim] sample:		9386.1 time, 2370.2 real, 688.8 MB
[runlim] sample:		9425.7 time, 2380.2 real, 702.8 MB
[runlim] sample:		9465.3 time, 2390.2 real, 702.8 MB
[runlim] sample:		9504.9 time, 2400.2 real, 705.1 MB
[runlim] sample:		9544.5 time, 2410.2 real, 707.6 MB
[runlim] sample:		9584.1 time, 2420.2 real, 708.1 MB
[runlim] sample:		9623.7 time, 2430.2 real, 708.4 MB
[runlim] sample:		9663.3 time, 2440.2 real, 710.6 MB
[runlim] sample:		9703.0 time, 2450.2 real, 710.6 MB
[runlim] sample:		9742.6 time, 2460.2 real, 710.9 MB
[runlim] sample:		9782.2 time, 2470.2 real, 711.1 MB
[runlim] sample:		9821.8 time, 2480.2 real, 713.1 MB
[runlim] sample:		9861.4 time, 2490.2 real, 713.3 MB
[runlim] sample:		9901.0 time, 2500.2 real, 713.3 MB
[runlim] sample:		9940.6 time, 2510.2 real, 713.6 MB
[runlim] sample:		9980.2 time, 2520.2 real, 715.8 MB
[runlim] sample:		10019.9 time, 2530.2 real, 735.8 MB
[runlim] sample:		10059.5 time, 2540.2 real, 735.8 MB
[runlim] sample:		10099.1 time, 2550.2 real, 735.8 MB
[runlim] sample:		10138.7 time, 2560.2 real, 735.8 MB
[runlim] sample:		10178.3 time, 2570.2 real, 737.8 MB
[runlim] sample:		10217.9 time, 2580.2 real, 737.8 MB
[runlim] sample:		10257.5 time, 2590.2 real, 737.8 MB
[runlim] sample:		10297.1 time, 2600.2 real, 737.8 MB
[runlim] sample:		10336.8 time, 2610.2 real, 737.8 MB
[runlim] sample:		10376.4 time, 2620.2 real, 737.8 MB
[runlim] sample:		10416.0 time, 2630.2 real, 701.8 MB
[runlim] sample:		10455.6 time, 2640.2 real, 661.1 MB
[runlim] sample:		10495.2 time, 2650.2 real, 661.1 MB
[runlim] sample:		10534.8 time, 2660.2 real, 668.7 MB
[runlim] sample:		10574.4 time, 2670.2 real, 671.5 MB
[runlim] sample:		10614.0 time, 2680.2 real, 673.5 MB
[runlim] sample:		10653.7 time, 2690.2 real, 669.8 MB
[runlim] sample:		10693.3 time, 2700.2 real, 669.8 MB
[runlim] sample:		10732.9 time, 2710.2 real, 670.3 MB
[runlim] sample:		10772.5 time, 2720.2 real, 683.0 MB
[runlim] sample:		10812.1 time, 2730.2 real, 695.0 MB
[runlim] sample:		10851.7 time, 2740.2 real, 697.0 MB
[runlim] sample:		10891.3 time, 2750.2 real, 699.0 MB
[runlim] sample:		10930.9 time, 2760.2 real, 701.0 MB
[runlim] sample:		10970.5 time, 2770.2 real, 701.0 MB
[runlim] sample:		11010.1 time, 2780.2 real, 703.0 MB
[runlim] sample:		11049.8 time, 2790.2 real, 705.0 MB
[runlim] sample:		11089.4 time, 2800.2 real, 705.0 MB
[runlim] sample:		11129.0 time, 2810.2 real, 705.8 MB
[runlim] sample:		11168.6 time, 2820.2 real, 705.8 MB
[runlim] sample:		11208.2 time, 2830.2 real, 709.8 MB
[runlim] sample:		11247.8 time, 2840.2 real, 709.8 MB
[runlim] sample:		11287.4 time, 2850.2 real, 709.8 MB
[runlim] sample:		11327.0 time, 2860.2 real, 709.8 MB
[runlim] sample:		11366.6 time, 2870.2 real, 709.8 MB
[runlim] sample:		11406.3 time, 2880.2 real, 710.2 MB
[runlim] sample:		11445.9 time, 2890.2 real, 712.3 MB
[runlim] sample:		11485.5 time, 2900.2 real, 714.8 MB
[runlim] sample:		11525.1 time, 2910.2 real, 715.3 MB
[runlim] sample:		11564.7 time, 2920.2 real, 719.1 MB
[runlim] sample:		11604.3 time, 2930.2 real, 739.5 MB
[runlim] sample:		11643.9 time, 2940.2 real, 739.5 MB
[runlim] sample:		11683.5 time, 2950.2 real, 739.5 MB
[runlim] sample:		11723.1 time, 2960.2 real, 739.5 MB
[runlim] sample:		11762.7 time, 2970.2 real, 756.5 MB
[runlim] sample:		11802.3 time, 2980.2 real, 762.5 MB
[runlim] sample:		11842.0 time, 2990.2 real, 762.5 MB
[runlim] sample:		11881.6 time, 3000.2 real, 762.5 MB
[runlim] sample:		11921.2 time, 3010.2 real, 762.5 MB
[runlim] sample:		11960.8 time, 3020.2 real, 762.5 MB
[runlim] sample:		12000.4 time, 3030.2 real, 778.5 MB
[runlim] sample:		12040.0 time, 3040.2 real, 784.5 MB
[runlim] sample:		12079.6 time, 3050.2 real, 784.5 MB
[runlim] sample:		12119.2 time, 3060.2 real, 784.5 MB
[runlim] sample:		12158.8 time, 3070.2 real, 784.5 MB
[runlim] sample:		12198.4 time, 3080.2 real, 802.5 MB
[runlim] sample:		12238.0 time, 3090.2 real, 802.5 MB
[runlim] sample:		12277.6 time, 3100.2 real, 804.5 MB
[runlim] sample:		12317.2 time, 3110.2 real, 804.5 MB
[runlim] sample:		12356.9 time, 3120.2 real, 806.5 MB
[runlim] sample:		12396.4 time, 3130.2 real, 790.8 MB
[runlim] sample:		12436.0 time, 3140.2 real, 776.9 MB
[runlim] sample:		12475.7 time, 3150.2 real, 776.9 MB
[runlim] sample:		12515.3 time, 3160.2 real, 778.9 MB
[runlim] sample:		12554.9 time, 3170.2 real, 779.6 MB
[runlim] sample:		12594.5 time, 3180.2 real, 780.1 MB
[runlim] sample:		12634.1 time, 3190.2 real, 784.3 MB
[runlim] sample:		12673.7 time, 3200.2 real, 786.3 MB
[runlim] sample:		12713.3 time, 3210.2 real, 788.6 MB
[runlim] sample:		12752.9 time, 3220.2 real, 794.6 MB
[runlim] sample:		12792.5 time, 3230.2 real, 794.8 MB
[runlim] sample:		12832.1 time, 3240.2 real, 830.5 MB
[runlim] sample:		12871.7 time, 3250.2 real, 831.5 MB
[runlim] sample:		12911.4 time, 3260.2 real, 822.5 MB
[runlim] sample:		12951.0 time, 3270.2 real, 824.5 MB
[runlim] sample:		12990.6 time, 3280.2 real, 826.1 MB
[runlim] sample:		13030.2 time, 3290.2 real, 828.6 MB
[runlim] sample:		13069.8 time, 3300.2 real, 867.9 MB
[runlim] sample:		13109.3 time, 3310.2 real, 899.3 MB
[runlim] sample:		13148.9 time, 3320.2 real, 913.2 MB
[runlim] sample:		13188.5 time, 3330.2 real, 914.2 MB
[runlim] sample:		13228.1 time, 3340.2 real, 914.2 MB
[runlim] sample:		13267.7 time, 3350.2 real, 915.8 MB
[runlim] sample:		13307.3 time, 3360.2 real, 915.8 MB
[runlim] sample:		13347.0 time, 3370.2 real, 918.9 MB
[runlim] sample:		13386.6 time, 3380.2 real, 920.9 MB
[runlim] sample:		13426.2 time, 3390.2 real, 922.0 MB
[runlim] sample:		13465.8 time, 3400.2 real, 938.3 MB
[runlim] sample:		13505.4 time, 3410.2 real, 938.8 MB
[runlim] sample:		13544.9 time, 3420.2 real, 940.3 MB
[runlim] sample:		13584.5 time, 3430.2 real, 945.4 MB
[runlim] sample:		13624.1 time, 3440.2 real, 948.4 MB
[runlim] sample:		13663.7 time, 3450.2 real, 950.4 MB
[runlim] sample:		13703.3 time, 3460.2 real, 994.0 MB
[runlim] sample:		13742.9 time, 3470.2 real, 1042.9 MB
[runlim] sample:		13782.5 time, 3480.2 real, 1065.1 MB
[runlim] sample:		13822.1 time, 3490.2 real, 1078.0 MB
[runlim] sample:		13861.7 time, 3500.2 real, 1115.8 MB
[runlim] sample:		13901.3 time, 3510.2 real, 1110.3 MB
[runlim] sample:		13940.9 time, 3520.2 real, 1130.3 MB
[runlim] sample:		13980.5 time, 3530.2 real, 1131.0 MB
[runlim] sample:		14020.1 time, 3540.2 real, 1137.1 MB
[runlim] sample:		14059.7 time, 3550.2 real, 1137.1 MB
[runlim] sample:		14099.3 time, 3560.2 real, 1137.1 MB
[runlim] sample:		14138.9 time, 3570.2 real, 1137.1 MB
[runlim] sample:		14178.5 time, 3580.2 real, 1139.2 MB
[runlim] sample:		14218.1 time, 3590.2 real, 1143.2 MB
[runlim] end:			Wed Sep 16 19:18:46 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.06 seconds
[runlim] time:			14256.90 seconds
[runlim] space:			1143.2 MB
[runlim] samples:		35998
