[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/6s105.aig
[runlim] start:			Tue Sep 15 16:00:06 2015
[runlim] main pid:		26174
[runlim] sample:		38.2 time, 10.9 real, 112.4 MB
[runlim] sample:		77.8 time, 20.9 real, 112.4 MB
[runlim] sample:		117.5 time, 30.9 real, 143.8 MB
[runlim] sample:		157.1 time, 40.9 real, 159.4 MB
[runlim] sample:		196.7 time, 50.9 real, 168.8 MB
[runlim] sample:		236.4 time, 60.9 real, 163.4 MB
[runlim] sample:		276.0 time, 70.9 real, 167.2 MB
[runlim] sample:		315.6 time, 80.9 real, 172.4 MB
[runlim] sample:		355.3 time, 90.9 real, 181.1 MB
[runlim] sample:		394.9 time, 100.9 real, 184.0 MB
[runlim] sample:		434.5 time, 110.9 real, 192.9 MB
[runlim] sample:		474.1 time, 120.9 real, 195.6 MB
[runlim] sample:		513.8 time, 130.9 real, 197.2 MB
[runlim] sample:		553.4 time, 140.9 real, 204.7 MB
[runlim] sample:		593.0 time, 150.9 real, 217.4 MB
[runlim] sample:		632.7 time, 160.9 real, 223.3 MB
[runlim] sample:		672.3 time, 170.9 real, 226.3 MB
[runlim] sample:		711.9 time, 180.9 real, 230.1 MB
[runlim] sample:		751.6 time, 190.9 real, 236.3 MB
[runlim] sample:		791.2 time, 200.9 real, 220.2 MB
[runlim] sample:		830.8 time, 210.9 real, 227.1 MB
[runlim] sample:		870.4 time, 220.9 real, 257.2 MB
[runlim] sample:		910.1 time, 230.9 real, 248.4 MB
[runlim] sample:		949.7 time, 240.9 real, 256.9 MB
[runlim] sample:		989.3 time, 250.9 real, 255.6 MB
[runlim] sample:		1029.0 time, 260.9 real, 261.9 MB
[runlim] sample:		1068.6 time, 270.9 real, 262.2 MB
[runlim] sample:		1108.2 time, 280.9 real, 268.0 MB
[runlim] sample:		1147.8 time, 290.9 real, 270.2 MB
[runlim] sample:		1187.5 time, 300.9 real, 272.2 MB
[runlim] sample:		1227.1 time, 310.9 real, 275.8 MB
[runlim] sample:		1266.7 time, 320.9 real, 276.6 MB
[runlim] sample:		1306.3 time, 330.9 real, 278.4 MB
[runlim] sample:		1345.9 time, 340.9 real, 278.4 MB
[runlim] sample:		1385.5 time, 350.9 real, 276.9 MB
[runlim] sample:		1425.2 time, 360.9 real, 283.7 MB
[runlim] sample:		1464.8 time, 370.9 real, 287.7 MB
[runlim] sample:		1504.4 time, 380.9 real, 289.2 MB
[runlim] sample:		1544.0 time, 390.9 real, 291.2 MB
[runlim] sample:		1583.6 time, 400.9 real, 282.3 MB
[runlim] sample:		1623.2 time, 410.9 real, 283.7 MB
[runlim] sample:		1662.9 time, 420.9 real, 270.6 MB
[runlim] sample:		1702.5 time, 430.9 real, 271.9 MB
[runlim] sample:		1742.1 time, 440.9 real, 278.6 MB
[runlim] sample:		1781.7 time, 450.9 real, 277.2 MB
[runlim] sample:		1821.3 time, 460.9 real, 276.2 MB
[runlim] sample:		1861.0 time, 470.9 real, 282.3 MB
[runlim] sample:		1900.6 time, 480.9 real, 303.4 MB
[runlim] sample:		1940.2 time, 490.9 real, 306.4 MB
[runlim] sample:		1979.8 time, 500.9 real, 291.2 MB
[runlim] sample:		2019.5 time, 510.9 real, 292.0 MB
[runlim] sample:		2059.1 time, 520.9 real, 297.3 MB
[runlim] sample:		2098.7 time, 530.9 real, 299.9 MB
[runlim] sample:		2138.3 time, 540.9 real, 302.7 MB
[runlim] sample:		2177.9 time, 550.9 real, 326.5 MB
[runlim] sample:		2217.5 time, 560.9 real, 333.3 MB
[runlim] sample:		2257.2 time, 570.9 real, 335.8 MB
[runlim] sample:		2296.8 time, 580.9 real, 343.1 MB
[runlim] sample:		2336.4 time, 590.9 real, 343.3 MB
[runlim] sample:		2376.0 time, 600.9 real, 340.6 MB
[runlim] sample:		2415.6 time, 610.9 real, 340.8 MB
[runlim] sample:		2455.2 time, 620.9 real, 372.3 MB
[runlim] sample:		2494.8 time, 630.9 real, 380.3 MB
[runlim] sample:		2534.5 time, 640.9 real, 346.5 MB
[runlim] sample:		2574.1 time, 650.9 real, 342.4 MB
[runlim] sample:		2613.7 time, 660.9 real, 346.5 MB
[runlim] sample:		2653.3 time, 670.9 real, 346.5 MB
[runlim] sample:		2692.9 time, 680.9 real, 346.8 MB
[runlim] sample:		2732.5 time, 690.9 real, 341.0 MB
[runlim] sample:		2772.2 time, 700.9 real, 373.8 MB
[runlim] sample:		2811.8 time, 710.9 real, 375.8 MB
[runlim] sample:		2851.4 time, 720.9 real, 375.8 MB
[runlim] sample:		2891.0 time, 730.9 real, 372.0 MB
[runlim] sample:		2930.6 time, 740.9 real, 375.5 MB
[runlim] sample:		2970.2 time, 750.9 real, 376.0 MB
[runlim] sample:		3009.8 time, 760.9 real, 382.0 MB
[runlim] sample:		3049.5 time, 770.9 real, 382.8 MB
[runlim] sample:		3089.1 time, 780.9 real, 386.3 MB
[runlim] sample:		3128.7 time, 790.9 real, 387.3 MB
[runlim] sample:		3168.3 time, 800.9 real, 384.1 MB
[runlim] sample:		3207.9 time, 810.9 real, 389.1 MB
[runlim] sample:		3247.6 time, 820.9 real, 386.7 MB
[runlim] sample:		3287.2 time, 830.9 real, 392.1 MB
[runlim] sample:		3326.8 time, 840.9 real, 389.7 MB
[runlim] sample:		3366.4 time, 850.9 real, 390.0 MB
[runlim] sample:		3406.0 time, 860.9 real, 386.2 MB
[runlim] sample:		3445.6 time, 870.9 real, 386.2 MB
[runlim] sample:		3485.2 time, 880.9 real, 386.4 MB
[runlim] sample:		3524.8 time, 890.9 real, 392.7 MB
[runlim] sample:		3564.5 time, 900.9 real, 397.1 MB
[runlim] sample:		3604.1 time, 910.9 real, 397.1 MB
[runlim] sample:		3643.7 time, 920.9 real, 397.1 MB
[runlim] sample:		3683.3 time, 930.9 real, 397.1 MB
[runlim] sample:		3722.9 time, 940.9 real, 389.1 MB
[runlim] sample:		3762.5 time, 950.9 real, 393.4 MB
[runlim] sample:		3802.1 time, 960.9 real, 404.0 MB
[runlim] sample:		3841.7 time, 970.9 real, 404.5 MB
[runlim] sample:		3881.4 time, 980.9 real, 412.8 MB
[runlim] sample:		3921.0 time, 990.9 real, 467.6 MB
[runlim] sample:		3960.6 time, 1000.9 real, 456.4 MB
[runlim] sample:		4000.2 time, 1010.9 real, 459.2 MB
[runlim] sample:		4039.8 time, 1020.9 real, 444.8 MB
[runlim] sample:		4079.4 time, 1030.9 real, 445.5 MB
[runlim] sample:		4119.1 time, 1040.9 real, 448.1 MB
[runlim] sample:		4158.7 time, 1050.9 real, 448.6 MB
[runlim] sample:		4198.3 time, 1060.9 real, 459.5 MB
[runlim] sample:		4237.9 time, 1070.9 real, 461.5 MB
[runlim] sample:		4277.5 time, 1080.9 real, 461.5 MB
[runlim] sample:		4317.1 time, 1090.9 real, 466.0 MB
[runlim] sample:		4356.8 time, 1100.9 real, 460.7 MB
[runlim] sample:		4396.4 time, 1110.9 real, 421.2 MB
[runlim] sample:		4436.0 time, 1120.9 real, 421.5 MB
[runlim] sample:		4475.6 time, 1130.9 real, 422.0 MB
[runlim] sample:		4515.2 time, 1140.9 real, 471.9 MB
[runlim] sample:		4554.9 time, 1150.9 real, 478.2 MB
[runlim] sample:		4594.5 time, 1160.9 real, 478.9 MB
[runlim] sample:		4634.1 time, 1170.9 real, 466.5 MB
[runlim] sample:		4673.7 time, 1180.9 real, 466.8 MB
[runlim] sample:		4713.3 time, 1190.9 real, 466.8 MB
[runlim] sample:		4752.9 time, 1200.9 real, 466.8 MB
[runlim] sample:		4792.6 time, 1210.9 real, 466.8 MB
[runlim] sample:		4832.2 time, 1220.9 real, 466.8 MB
[runlim] sample:		4871.8 time, 1230.9 real, 466.8 MB
[runlim] sample:		4911.4 time, 1240.9 real, 466.8 MB
[runlim] sample:		4951.0 time, 1250.9 real, 466.8 MB
[runlim] sample:		4990.6 time, 1260.9 real, 466.8 MB
[runlim] sample:		5030.3 time, 1270.9 real, 466.8 MB
[runlim] sample:		5069.9 time, 1280.9 real, 466.8 MB
[runlim] sample:		5109.5 time, 1290.9 real, 466.8 MB
[runlim] sample:		5149.1 time, 1300.9 real, 466.8 MB
[runlim] sample:		5188.7 time, 1310.9 real, 466.7 MB
[runlim] sample:		5228.3 time, 1320.9 real, 466.7 MB
[runlim] sample:		5267.9 time, 1330.9 real, 466.7 MB
[runlim] sample:		5307.6 time, 1340.9 real, 466.7 MB
[runlim] sample:		5347.2 time, 1350.9 real, 466.7 MB
[runlim] sample:		5386.8 time, 1360.9 real, 466.7 MB
[runlim] sample:		5426.4 time, 1370.9 real, 510.0 MB
[runlim] sample:		5466.0 time, 1380.9 real, 510.3 MB
[runlim] sample:		5505.6 time, 1390.9 real, 510.6 MB
[runlim] sample:		5545.2 time, 1400.9 real, 512.6 MB
[runlim] sample:		5584.8 time, 1410.9 real, 512.8 MB
[runlim] sample:		5624.4 time, 1420.9 real, 514.8 MB
[runlim] sample:		5664.0 time, 1430.9 real, 514.8 MB
[runlim] sample:		5703.6 time, 1440.9 real, 514.8 MB
[runlim] sample:		5743.3 time, 1450.9 real, 516.8 MB
[runlim] sample:		5782.9 time, 1460.9 real, 516.8 MB
[runlim] sample:		5822.5 time, 1470.9 real, 516.8 MB
[runlim] sample:		5862.1 time, 1480.9 real, 518.8 MB
[runlim] sample:		5901.7 time, 1490.9 real, 518.8 MB
[runlim] sample:		5941.3 time, 1500.9 real, 518.8 MB
[runlim] sample:		5980.9 time, 1510.9 real, 520.8 MB
[runlim] sample:		6020.5 time, 1520.9 real, 478.8 MB
[runlim] sample:		6060.1 time, 1530.9 real, 484.8 MB
[runlim] sample:		6099.8 time, 1540.9 real, 484.8 MB
[runlim] sample:		6139.4 time, 1550.9 real, 484.8 MB
[runlim] sample:		6179.0 time, 1560.9 real, 478.0 MB
[runlim] sample:		6218.6 time, 1570.9 real, 478.0 MB
[runlim] sample:		6258.2 time, 1580.9 real, 478.0 MB
[runlim] sample:		6297.8 time, 1590.9 real, 484.1 MB
[runlim] sample:		6337.4 time, 1600.9 real, 484.3 MB
[runlim] sample:		6377.1 time, 1610.9 real, 484.3 MB
[runlim] sample:		6416.7 time, 1620.9 real, 484.8 MB
[runlim] sample:		6456.3 time, 1630.9 real, 486.1 MB
[runlim] sample:		6495.9 time, 1640.9 real, 487.2 MB
[runlim] sample:		6535.5 time, 1650.9 real, 487.9 MB
[runlim] sample:		6575.1 time, 1660.9 real, 489.9 MB
[runlim] sample:		6614.7 time, 1670.9 real, 505.1 MB
[runlim] sample:		6654.3 time, 1680.9 real, 507.1 MB
[runlim] sample:		6693.9 time, 1690.9 real, 513.9 MB
[runlim] sample:		6733.5 time, 1700.9 real, 511.2 MB
[runlim] sample:		6773.1 time, 1710.9 real, 512.4 MB
[runlim] sample:		6812.8 time, 1720.9 real, 544.4 MB
[runlim] sample:		6852.4 time, 1730.9 real, 544.8 MB
[runlim] sample:		6892.0 time, 1740.9 real, 545.1 MB
[runlim] sample:		6931.6 time, 1750.9 real, 547.3 MB
[runlim] sample:		6971.2 time, 1760.9 real, 547.3 MB
[runlim] sample:		7010.8 time, 1770.9 real, 549.6 MB
[runlim] sample:		7050.4 time, 1780.9 real, 549.6 MB
[runlim] sample:		7090.0 time, 1790.9 real, 556.1 MB
[runlim] sample:		7129.6 time, 1800.9 real, 558.1 MB
[runlim] sample:		7169.2 time, 1810.9 real, 558.1 MB
[runlim] sample:		7208.9 time, 1820.9 real, 558.1 MB
[runlim] sample:		7248.4 time, 1830.9 real, 560.3 MB
[runlim] sample:		7288.1 time, 1840.9 real, 562.6 MB
[runlim] sample:		7327.7 time, 1850.9 real, 562.8 MB
[runlim] sample:		7367.3 time, 1860.9 real, 565.0 MB
[runlim] sample:		7406.9 time, 1870.9 real, 565.3 MB
[runlim] sample:		7446.5 time, 1880.9 real, 567.5 MB
[runlim] sample:		7486.1 time, 1890.9 real, 569.8 MB
[runlim] sample:		7525.7 time, 1900.9 real, 588.6 MB
[runlim] sample:		7565.3 time, 1910.9 real, 588.9 MB
[runlim] sample:		7604.9 time, 1920.9 real, 591.2 MB
[runlim] sample:		7644.5 time, 1930.9 real, 593.2 MB
[runlim] sample:		7684.1 time, 1940.9 real, 593.2 MB
[runlim] sample:		7723.8 time, 1950.9 real, 595.2 MB
[runlim] sample:		7763.4 time, 1960.9 real, 547.2 MB
[runlim] sample:		7803.0 time, 1970.9 real, 566.3 MB
[runlim] sample:		7842.6 time, 1980.9 real, 570.3 MB
[runlim] sample:		7882.2 time, 1990.9 real, 572.7 MB
[runlim] sample:		7921.8 time, 2000.9 real, 586.5 MB
[runlim] sample:		7961.4 time, 2010.9 real, 589.5 MB
[runlim] sample:		8001.0 time, 2020.9 real, 581.3 MB
[runlim] sample:		8040.6 time, 2030.9 real, 588.9 MB
[runlim] sample:		8080.2 time, 2040.9 real, 590.9 MB
[runlim] sample:		8119.8 time, 2050.9 real, 591.1 MB
[runlim] sample:		8159.4 time, 2060.9 real, 607.8 MB
[runlim] sample:		8199.0 time, 2070.9 real, 610.7 MB
[runlim] sample:		8238.6 time, 2080.9 real, 610.7 MB
[runlim] sample:		8278.2 time, 2090.9 real, 614.3 MB
[runlim] sample:		8317.8 time, 2100.9 real, 616.6 MB
[runlim] sample:		8357.4 time, 2110.9 real, 616.6 MB
[runlim] sample:		8397.0 time, 2120.9 real, 627.4 MB
[runlim] sample:		8436.6 time, 2130.9 real, 627.4 MB
[runlim] sample:		8476.2 time, 2140.9 real, 630.6 MB
[runlim] sample:		8515.8 time, 2150.9 real, 602.8 MB
[runlim] sample:		8555.5 time, 2160.9 real, 593.9 MB
[runlim] sample:		8595.1 time, 2170.9 real, 593.9 MB
[runlim] sample:		8634.7 time, 2180.9 real, 595.9 MB
[runlim] sample:		8674.3 time, 2190.9 real, 595.9 MB
[runlim] sample:		8713.9 time, 2200.9 real, 595.9 MB
[runlim] sample:		8753.5 time, 2210.9 real, 597.9 MB
[runlim] sample:		8793.1 time, 2220.9 real, 597.9 MB
[runlim] sample:		8832.7 time, 2230.9 real, 600.2 MB
[runlim] sample:		8872.4 time, 2240.9 real, 583.5 MB
[runlim] sample:		8912.0 time, 2250.9 real, 583.5 MB
[runlim] sample:		8951.6 time, 2260.9 real, 585.5 MB
[runlim] sample:		8991.2 time, 2270.9 real, 593.3 MB
[runlim] sample:		9030.8 time, 2280.9 real, 588.6 MB
[runlim] sample:		9070.4 time, 2290.9 real, 588.6 MB
[runlim] sample:		9110.0 time, 2300.9 real, 588.6 MB
[runlim] sample:		9149.6 time, 2310.9 real, 590.6 MB
[runlim] sample:		9189.2 time, 2320.9 real, 590.6 MB
[runlim] sample:		9228.9 time, 2330.9 real, 592.6 MB
[runlim] sample:		9268.5 time, 2340.9 real, 556.1 MB
[runlim] sample:		9308.1 time, 2350.9 real, 561.9 MB
[runlim] sample:		9347.7 time, 2360.9 real, 562.9 MB
[runlim] sample:		9387.3 time, 2370.9 real, 575.4 MB
[runlim] sample:		9426.9 time, 2380.9 real, 577.4 MB
[runlim] sample:		9466.5 time, 2390.9 real, 579.4 MB
[runlim] sample:		9506.1 time, 2400.9 real, 591.6 MB
[runlim] sample:		9545.7 time, 2410.9 real, 595.9 MB
[runlim] sample:		9585.3 time, 2420.9 real, 595.9 MB
[runlim] sample:		9625.0 time, 2430.9 real, 578.7 MB
[runlim] sample:		9664.6 time, 2440.9 real, 581.5 MB
[runlim] sample:		9704.2 time, 2450.9 real, 581.5 MB
[runlim] sample:		9743.8 time, 2460.9 real, 589.3 MB
[runlim] sample:		9783.4 time, 2470.9 real, 592.2 MB
[runlim] sample:		9823.0 time, 2480.9 real, 592.2 MB
[runlim] sample:		9862.6 time, 2490.9 real, 594.2 MB
[runlim] sample:		9902.2 time, 2500.9 real, 594.7 MB
[runlim] sample:		9941.8 time, 2510.9 real, 594.7 MB
[runlim] sample:		9981.4 time, 2520.9 real, 586.8 MB
[runlim] sample:		10021.0 time, 2530.9 real, 575.9 MB
[runlim] sample:		10060.6 time, 2540.9 real, 595.9 MB
[runlim] sample:		10100.3 time, 2550.9 real, 597.9 MB
[runlim] sample:		10139.9 time, 2560.9 real, 607.8 MB
[runlim] sample:		10179.5 time, 2570.9 real, 607.8 MB
[runlim] sample:		10219.1 time, 2580.9 real, 607.8 MB
[runlim] sample:		10258.7 time, 2590.9 real, 609.8 MB
[runlim] sample:		10298.3 time, 2600.9 real, 611.8 MB
[runlim] sample:		10337.9 time, 2610.9 real, 601.9 MB
[runlim] sample:		10377.5 time, 2620.9 real, 611.8 MB
[runlim] sample:		10417.1 time, 2630.9 real, 613.8 MB
[runlim] sample:		10456.8 time, 2640.9 real, 615.8 MB
[runlim] sample:		10496.4 time, 2650.9 real, 615.8 MB
[runlim] sample:		10536.0 time, 2660.9 real, 617.8 MB
[runlim] sample:		10575.6 time, 2670.9 real, 597.6 MB
[runlim] sample:		10615.2 time, 2680.9 real, 597.6 MB
[runlim] sample:		10654.8 time, 2690.9 real, 597.6 MB
[runlim] sample:		10694.4 time, 2700.9 real, 624.9 MB
[runlim] sample:		10734.0 time, 2710.9 real, 627.4 MB
[runlim] sample:		10773.6 time, 2720.9 real, 627.6 MB
[runlim] sample:		10813.2 time, 2730.9 real, 629.9 MB
[runlim] sample:		10852.8 time, 2740.9 real, 630.1 MB
[runlim] sample:		10892.5 time, 2750.9 real, 630.4 MB
[runlim] sample:		10932.1 time, 2760.9 real, 632.6 MB
[runlim] sample:		10971.7 time, 2770.9 real, 634.6 MB
[runlim] sample:		11011.3 time, 2780.9 real, 636.6 MB
[runlim] sample:		11050.9 time, 2790.9 real, 636.6 MB
[runlim] sample:		11090.5 time, 2800.9 real, 637.3 MB
[runlim] sample:		11130.1 time, 2810.9 real, 637.8 MB
[runlim] sample:		11169.7 time, 2820.9 real, 627.7 MB
[runlim] sample:		11209.3 time, 2830.9 real, 630.0 MB
[runlim] sample:		11248.9 time, 2840.9 real, 631.6 MB
[runlim] sample:		11288.5 time, 2850.9 real, 631.6 MB
[runlim] sample:		11328.1 time, 2860.9 real, 635.6 MB
[runlim] sample:		11367.8 time, 2870.9 real, 635.6 MB
[runlim] sample:		11407.4 time, 2880.9 real, 635.6 MB
[runlim] sample:		11447.0 time, 2890.9 real, 637.5 MB
[runlim] sample:		11486.6 time, 2900.9 real, 591.6 MB
[runlim] sample:		11526.2 time, 2910.9 real, 592.6 MB
[runlim] sample:		11565.8 time, 2920.9 real, 606.9 MB
[runlim] sample:		11605.4 time, 2930.9 real, 606.9 MB
[runlim] sample:		11645.0 time, 2940.9 real, 630.9 MB
[runlim] sample:		11684.6 time, 2950.9 real, 642.6 MB
[runlim] sample:		11724.2 time, 2960.9 real, 647.1 MB
[runlim] sample:		11763.9 time, 2970.9 real, 650.6 MB
[runlim] sample:		11803.5 time, 2980.9 real, 650.8 MB
[runlim] sample:		11843.0 time, 2990.9 real, 652.8 MB
[runlim] sample:		11882.7 time, 3000.9 real, 654.8 MB
[runlim] sample:		11922.3 time, 3010.9 real, 654.8 MB
[runlim] sample:		11961.9 time, 3020.9 real, 656.8 MB
[runlim] sample:		12001.5 time, 3030.9 real, 656.8 MB
[runlim] sample:		12041.1 time, 3040.9 real, 656.8 MB
[runlim] sample:		12080.7 time, 3050.9 real, 647.7 MB
[runlim] sample:		12120.3 time, 3060.9 real, 650.0 MB
[runlim] sample:		12159.9 time, 3070.9 real, 650.2 MB
[runlim] sample:		12199.5 time, 3080.9 real, 654.0 MB
[runlim] sample:		12239.1 time, 3090.9 real, 654.2 MB
[runlim] sample:		12278.7 time, 3100.9 real, 654.2 MB
[runlim] sample:		12318.3 time, 3110.9 real, 643.3 MB
[runlim] sample:		12358.0 time, 3120.9 real, 643.3 MB
[runlim] sample:		12397.5 time, 3130.9 real, 643.3 MB
[runlim] sample:		12437.2 time, 3140.9 real, 645.3 MB
[runlim] sample:		12476.8 time, 3150.9 real, 647.3 MB
[runlim] sample:		12516.4 time, 3160.9 real, 647.3 MB
[runlim] sample:		12556.0 time, 3170.9 real, 649.3 MB
[runlim] sample:		12595.6 time, 3180.9 real, 649.3 MB
[runlim] sample:		12635.2 time, 3190.9 real, 649.3 MB
[runlim] sample:		12674.8 time, 3200.9 real, 649.3 MB
[runlim] sample:		12714.4 time, 3210.9 real, 651.3 MB
[runlim] sample:		12754.0 time, 3220.9 real, 617.0 MB
[runlim] sample:		12793.6 time, 3230.9 real, 625.0 MB
[runlim] sample:		12833.2 time, 3240.9 real, 637.3 MB
[runlim] sample:		12872.8 time, 3250.9 real, 639.3 MB
[runlim] sample:		12912.4 time, 3260.9 real, 671.5 MB
[runlim] sample:		12952.0 time, 3270.9 real, 674.2 MB
[runlim] sample:		12991.6 time, 3280.9 real, 676.2 MB
[runlim] sample:		13031.3 time, 3290.9 real, 680.4 MB
[runlim] sample:		13070.9 time, 3300.9 real, 680.4 MB
[runlim] sample:		13110.5 time, 3310.9 real, 664.7 MB
[runlim] sample:		13150.1 time, 3320.9 real, 667.7 MB
[runlim] sample:		13189.7 time, 3330.9 real, 670.2 MB
[runlim] sample:		13229.3 time, 3340.9 real, 672.2 MB
[runlim] sample:		13268.9 time, 3350.9 real, 663.3 MB
[runlim] sample:		13308.5 time, 3360.9 real, 667.3 MB
[runlim] sample:		13348.1 time, 3370.9 real, 667.3 MB
[runlim] sample:		13387.7 time, 3380.9 real, 669.3 MB
[runlim] sample:		13427.3 time, 3390.9 real, 680.5 MB
[runlim] sample:		13466.9 time, 3400.9 real, 736.4 MB
[runlim] sample:		13506.5 time, 3410.9 real, 734.0 MB
[runlim] sample:		13546.0 time, 3420.9 real, 778.9 MB
[runlim] sample:		13585.6 time, 3430.9 real, 781.1 MB
[runlim] sample:		13625.2 time, 3440.9 real, 791.2 MB
[runlim] sample:		13664.8 time, 3450.9 real, 797.2 MB
[runlim] sample:		13704.4 time, 3460.9 real, 797.4 MB
[runlim] sample:		13744.0 time, 3470.9 real, 799.9 MB
[runlim] sample:		13783.6 time, 3480.9 real, 803.2 MB
[runlim] sample:		13823.3 time, 3490.9 real, 807.0 MB
[runlim] sample:		13862.9 time, 3500.9 real, 815.3 MB
[runlim] sample:		13902.5 time, 3510.9 real, 815.3 MB
[runlim] sample:		13942.1 time, 3520.9 real, 823.9 MB
[runlim] sample:		13981.7 time, 3530.9 real, 875.3 MB
[runlim] sample:		14021.3 time, 3540.9 real, 917.0 MB
[runlim] sample:		14060.9 time, 3550.9 real, 923.1 MB
[runlim] sample:		14100.5 time, 3560.9 real, 923.4 MB
[runlim] sample:		14140.1 time, 3570.9 real, 927.7 MB
[runlim] sample:		14179.7 time, 3580.9 real, 912.1 MB
[runlim] sample:		14219.3 time, 3590.9 real, 912.1 MB
[runlim] end:			Tue Sep 15 17:00:06 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.11 seconds
[runlim] time:			14255.75 seconds
[runlim] space:			927.7 MB
[runlim] samples:		35992
