[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/6s366r.aig
[runlim] start:			Wed Sep 16 08:01:18 2015
[runlim] main pid:		26198
[runlim] sample:		30.0 time, 10.2 real, 197.2 MB
[runlim] sample:		69.7 time, 20.2 real, 199.4 MB
[runlim] sample:		109.3 time, 30.2 real, 228.8 MB
[runlim] sample:		149.0 time, 40.2 real, 223.1 MB
[runlim] sample:		188.7 time, 50.2 real, 229.7 MB
[runlim] sample:		228.3 time, 60.2 real, 225.1 MB
[runlim] sample:		267.9 time, 70.2 real, 240.9 MB
[runlim] sample:		307.6 time, 80.2 real, 239.6 MB
[runlim] sample:		347.2 time, 90.2 real, 274.3 MB
[runlim] sample:		386.8 time, 100.2 real, 272.2 MB
[runlim] sample:		426.5 time, 110.2 real, 269.9 MB
[runlim] sample:		466.1 time, 120.2 real, 262.1 MB
[runlim] sample:		505.8 time, 130.2 real, 266.0 MB
[runlim] sample:		545.4 time, 140.2 real, 290.1 MB
[runlim] sample:		585.0 time, 150.2 real, 259.6 MB
[runlim] sample:		624.6 time, 160.2 real, 260.3 MB
[runlim] sample:		664.3 time, 170.2 real, 268.6 MB
[runlim] sample:		703.9 time, 180.2 real, 276.3 MB
[runlim] sample:		743.5 time, 190.2 real, 277.8 MB
[runlim] sample:		783.2 time, 200.2 real, 299.1 MB
[runlim] sample:		822.8 time, 210.2 real, 304.8 MB
[runlim] sample:		862.5 time, 220.2 real, 306.1 MB
[runlim] sample:		902.1 time, 230.2 real, 311.9 MB
[runlim] sample:		941.7 time, 240.2 real, 351.0 MB
[runlim] sample:		981.4 time, 250.2 real, 326.7 MB
[runlim] sample:		1021.0 time, 260.2 real, 363.1 MB
[runlim] sample:		1060.7 time, 270.2 real, 329.6 MB
[runlim] sample:		1100.3 time, 280.2 real, 356.0 MB
[runlim] sample:		1139.9 time, 290.2 real, 317.7 MB
[runlim] sample:		1179.6 time, 300.2 real, 338.5 MB
[runlim] sample:		1219.2 time, 310.2 real, 362.4 MB
[runlim] sample:		1258.8 time, 320.2 real, 330.8 MB
[runlim] sample:		1298.5 time, 330.2 real, 344.3 MB
[runlim] sample:		1338.1 time, 340.2 real, 342.6 MB
[runlim] sample:		1377.8 time, 350.2 real, 370.7 MB
[runlim] sample:		1417.4 time, 360.2 real, 363.9 MB
[runlim] sample:		1457.0 time, 370.2 real, 385.5 MB
[runlim] sample:		1496.7 time, 380.2 real, 393.0 MB
[runlim] sample:		1536.3 time, 390.2 real, 344.6 MB
[runlim] sample:		1576.0 time, 400.2 real, 353.7 MB
[runlim] sample:		1615.6 time, 410.2 real, 353.5 MB
[runlim] sample:		1655.2 time, 420.2 real, 386.8 MB
[runlim] sample:		1694.8 time, 430.2 real, 407.1 MB
[runlim] sample:		1734.5 time, 440.2 real, 357.4 MB
[runlim] sample:		1774.1 time, 450.2 real, 364.2 MB
[runlim] sample:		1813.7 time, 460.2 real, 386.3 MB
[runlim] sample:		1853.4 time, 470.2 real, 414.6 MB
[runlim] sample:		1893.0 time, 480.2 real, 374.6 MB
[runlim] sample:		1932.6 time, 490.2 real, 374.6 MB
[runlim] sample:		1972.3 time, 500.2 real, 373.9 MB
[runlim] sample:		2011.9 time, 510.2 real, 377.2 MB
[runlim] sample:		2051.5 time, 520.2 real, 374.6 MB
[runlim] sample:		2091.2 time, 530.2 real, 389.7 MB
[runlim] sample:		2130.8 time, 540.2 real, 401.4 MB
[runlim] sample:		2170.4 time, 550.2 real, 387.5 MB
[runlim] sample:		2210.1 time, 560.2 real, 398.5 MB
[runlim] sample:		2249.7 time, 570.2 real, 406.3 MB
[runlim] sample:		2289.4 time, 580.2 real, 437.1 MB
[runlim] sample:		2329.0 time, 590.2 real, 437.9 MB
[runlim] sample:		2368.6 time, 600.2 real, 438.2 MB
[runlim] sample:		2408.3 time, 610.2 real, 406.3 MB
[runlim] sample:		2447.9 time, 620.2 real, 407.0 MB
[runlim] sample:		2487.5 time, 630.2 real, 409.8 MB
[runlim] sample:		2527.2 time, 640.2 real, 419.8 MB
[runlim] sample:		2566.8 time, 650.2 real, 431.5 MB
[runlim] sample:		2606.4 time, 660.2 real, 418.6 MB
[runlim] sample:		2646.1 time, 670.2 real, 419.7 MB
[runlim] sample:		2685.7 time, 680.2 real, 425.4 MB
[runlim] sample:		2725.3 time, 690.2 real, 472.3 MB
[runlim] sample:		2764.9 time, 700.2 real, 470.4 MB
[runlim] sample:		2804.6 time, 710.2 real, 454.3 MB
[runlim] sample:		2844.2 time, 720.2 real, 470.4 MB
[runlim] sample:		2883.8 time, 730.2 real, 443.1 MB
[runlim] sample:		2923.5 time, 740.2 real, 445.4 MB
[runlim] sample:		2963.1 time, 750.2 real, 433.1 MB
[runlim] sample:		3002.8 time, 760.2 real, 434.8 MB
[runlim] sample:		3042.4 time, 770.2 real, 455.8 MB
[runlim] sample:		3082.0 time, 780.2 real, 453.7 MB
[runlim] sample:		3121.7 time, 790.2 real, 457.2 MB
[runlim] sample:		3161.3 time, 800.2 real, 459.2 MB
[runlim] sample:		3200.9 time, 810.2 real, 461.5 MB
[runlim] sample:		3240.6 time, 820.2 real, 461.7 MB
[runlim] sample:		3280.2 time, 830.2 real, 464.0 MB
[runlim] sample:		3319.8 time, 840.2 real, 444.8 MB
[runlim] sample:		3359.4 time, 850.2 real, 432.7 MB
[runlim] sample:		3399.1 time, 860.2 real, 433.5 MB
[runlim] sample:		3438.7 time, 870.2 real, 441.5 MB
[runlim] sample:		3478.3 time, 880.2 real, 440.0 MB
[runlim] sample:		3518.0 time, 890.2 real, 440.3 MB
[runlim] sample:		3557.6 time, 900.2 real, 426.6 MB
[runlim] sample:		3597.2 time, 910.2 real, 448.4 MB
[runlim] sample:		3636.9 time, 920.2 real, 447.1 MB
[runlim] sample:		3676.5 time, 930.2 real, 459.9 MB
[runlim] sample:		3716.1 time, 940.2 real, 460.9 MB
[runlim] sample:		3755.8 time, 950.2 real, 463.5 MB
[runlim] sample:		3795.4 time, 960.2 real, 449.3 MB
[runlim] sample:		3835.0 time, 970.2 real, 455.0 MB
[runlim] sample:		3874.7 time, 980.2 real, 473.0 MB
[runlim] sample:		3914.3 time, 990.2 real, 475.3 MB
[runlim] sample:		3953.9 time, 1000.2 real, 462.4 MB
[runlim] sample:		3993.5 time, 1010.2 real, 462.7 MB
[runlim] sample:		4033.2 time, 1020.2 real, 484.5 MB
[runlim] sample:		4072.8 time, 1030.2 real, 484.5 MB
[runlim] sample:		4112.4 time, 1040.2 real, 486.8 MB
[runlim] sample:		4152.1 time, 1050.2 real, 488.8 MB
[runlim] sample:		4191.7 time, 1060.2 real, 472.4 MB
[runlim] sample:		4231.3 time, 1070.2 real, 488.8 MB
[runlim] sample:		4270.9 time, 1080.2 real, 494.9 MB
[runlim] sample:		4310.6 time, 1090.2 real, 492.8 MB
[runlim] sample:		4350.2 time, 1100.2 real, 498.6 MB
[runlim] sample:		4389.8 time, 1110.2 real, 496.0 MB
[runlim] sample:		4429.4 time, 1120.2 real, 474.4 MB
[runlim] sample:		4469.1 time, 1130.2 real, 483.7 MB
[runlim] sample:		4508.7 time, 1140.2 real, 483.2 MB
[runlim] sample:		4548.3 time, 1150.2 real, 487.5 MB
[runlim] sample:		4587.9 time, 1160.2 real, 479.2 MB
[runlim] sample:		4627.6 time, 1170.2 real, 507.6 MB
[runlim] sample:		4667.2 time, 1180.2 real, 509.4 MB
[runlim] sample:		4706.9 time, 1190.2 real, 511.7 MB
[runlim] sample:		4746.5 time, 1200.2 real, 521.6 MB
[runlim] sample:		4786.1 time, 1210.2 real, 527.9 MB
[runlim] sample:		4825.7 time, 1220.2 real, 533.3 MB
[runlim] sample:		4865.4 time, 1230.2 real, 517.0 MB
[runlim] sample:		4905.0 time, 1240.2 real, 521.3 MB
[runlim] sample:		4944.6 time, 1250.2 real, 522.2 MB
[runlim] sample:		4984.2 time, 1260.2 real, 521.7 MB
[runlim] sample:		5023.9 time, 1270.2 real, 543.7 MB
[runlim] sample:		5063.5 time, 1280.2 real, 544.0 MB
[runlim] sample:		5103.1 time, 1290.2 real, 522.5 MB
[runlim] sample:		5142.7 time, 1300.2 real, 531.4 MB
[runlim] sample:		5182.4 time, 1310.2 real, 523.0 MB
[runlim] sample:		5222.0 time, 1320.2 real, 526.5 MB
[runlim] sample:		5261.6 time, 1330.2 real, 530.4 MB
[runlim] sample:		5301.2 time, 1340.2 real, 533.7 MB
[runlim] sample:		5340.9 time, 1350.2 real, 542.4 MB
[runlim] sample:		5380.5 time, 1360.2 real, 542.7 MB
[runlim] sample:		5420.1 time, 1370.2 real, 548.6 MB
[runlim] sample:		5459.7 time, 1380.2 real, 544.5 MB
[runlim] sample:		5499.3 time, 1390.2 real, 546.7 MB
[runlim] sample:		5539.0 time, 1400.2 real, 552.3 MB
[runlim] sample:		5578.6 time, 1410.2 real, 539.1 MB
[runlim] sample:		5618.2 time, 1420.2 real, 539.6 MB
[runlim] sample:		5657.8 time, 1430.2 real, 544.1 MB
[runlim] sample:		5697.4 time, 1440.2 real, 551.0 MB
[runlim] sample:		5737.1 time, 1450.2 real, 559.0 MB
[runlim] sample:		5776.7 time, 1460.2 real, 554.1 MB
[runlim] sample:		5816.3 time, 1470.2 real, 556.6 MB
[runlim] sample:		5855.9 time, 1480.2 real, 562.9 MB
[runlim] sample:		5895.6 time, 1490.2 real, 560.0 MB
[runlim] sample:		5935.2 time, 1500.2 real, 566.7 MB
[runlim] sample:		5974.8 time, 1510.2 real, 561.5 MB
[runlim] sample:		6014.4 time, 1520.2 real, 564.6 MB
[runlim] sample:		6054.1 time, 1530.2 real, 570.9 MB
[runlim] sample:		6093.7 time, 1540.2 real, 567.6 MB
[runlim] sample:		6133.3 time, 1550.2 real, 573.9 MB
[runlim] sample:		6172.9 time, 1560.2 real, 570.1 MB
[runlim] sample:		6212.5 time, 1570.2 real, 577.4 MB
[runlim] sample:		6252.1 time, 1580.2 real, 556.8 MB
[runlim] sample:		6291.8 time, 1590.2 real, 560.4 MB
[runlim] sample:		6331.4 time, 1600.2 real, 560.7 MB
[runlim] sample:		6371.0 time, 1610.2 real, 568.5 MB
[runlim] sample:		6410.6 time, 1620.2 real, 562.8 MB
[runlim] sample:		6450.3 time, 1630.2 real, 564.8 MB
[runlim] sample:		6489.9 time, 1640.2 real, 565.0 MB
[runlim] sample:		6529.5 time, 1650.2 real, 567.6 MB
[runlim] sample:		6569.1 time, 1660.2 real, 568.7 MB
[runlim] sample:		6608.7 time, 1670.2 real, 576.5 MB
[runlim] sample:		6648.4 time, 1680.2 real, 576.2 MB
[runlim] sample:		6688.0 time, 1690.2 real, 578.9 MB
[runlim] sample:		6727.6 time, 1700.2 real, 586.0 MB
[runlim] sample:		6767.2 time, 1710.2 real, 581.8 MB
[runlim] sample:		6806.8 time, 1720.2 real, 581.8 MB
[runlim] sample:		6846.4 time, 1730.2 real, 581.8 MB
[runlim] sample:		6886.1 time, 1740.2 real, 583.9 MB
[runlim] sample:		6925.7 time, 1750.2 real, 579.3 MB
[runlim] sample:		6965.3 time, 1760.2 real, 581.3 MB
[runlim] sample:		7004.9 time, 1770.2 real, 567.4 MB
[runlim] sample:		7044.6 time, 1780.2 real, 574.2 MB
[runlim] sample:		7084.2 time, 1790.2 real, 567.4 MB
[runlim] sample:		7123.8 time, 1800.2 real, 579.5 MB
[runlim] sample:		7163.4 time, 1810.2 real, 589.8 MB
[runlim] sample:		7203.0 time, 1820.2 real, 583.0 MB
[runlim] sample:		7242.6 time, 1830.2 real, 585.0 MB
[runlim] sample:		7282.3 time, 1840.2 real, 594.1 MB
[runlim] sample:		7321.9 time, 1850.2 real, 596.1 MB
[runlim] sample:		7361.5 time, 1860.2 real, 589.1 MB
[runlim] sample:		7401.1 time, 1870.2 real, 590.1 MB
[runlim] sample:		7440.7 time, 1880.2 real, 592.4 MB
[runlim] sample:		7480.4 time, 1890.2 real, 592.4 MB
[runlim] sample:		7520.0 time, 1900.2 real, 594.7 MB
[runlim] sample:		7559.6 time, 1910.2 real, 594.8 MB
[runlim] sample:		7599.2 time, 1920.2 real, 564.8 MB
[runlim] sample:		7638.8 time, 1930.2 real, 557.1 MB
[runlim] sample:		7678.4 time, 1940.2 real, 564.9 MB
[runlim] sample:		7718.1 time, 1950.2 real, 557.1 MB
[runlim] sample:		7757.7 time, 1960.2 real, 574.0 MB
[runlim] sample:		7797.3 time, 1970.2 real, 566.2 MB
[runlim] sample:		7836.9 time, 1980.2 real, 566.5 MB
[runlim] sample:		7876.6 time, 1990.2 real, 578.7 MB
[runlim] sample:		7916.2 time, 2000.2 real, 573.4 MB
[runlim] sample:		7955.8 time, 2010.2 real, 574.2 MB
[runlim] sample:		7995.4 time, 2020.2 real, 582.7 MB
[runlim] sample:		8035.0 time, 2030.2 real, 576.6 MB
[runlim] sample:		8074.6 time, 2040.2 real, 586.7 MB
[runlim] sample:		8114.3 time, 2050.2 real, 577.7 MB
[runlim] sample:		8153.9 time, 2060.2 real, 586.0 MB
[runlim] sample:		8193.5 time, 2070.2 real, 595.0 MB
[runlim] sample:		8233.1 time, 2080.2 real, 607.5 MB
[runlim] sample:		8272.8 time, 2090.2 real, 612.6 MB
[runlim] sample:		8312.4 time, 2100.2 real, 634.2 MB
[runlim] sample:		8352.0 time, 2110.2 real, 636.3 MB
[runlim] sample:		8391.6 time, 2120.2 real, 630.1 MB
[runlim] sample:		8431.2 time, 2130.2 real, 632.1 MB
[runlim] sample:		8470.8 time, 2140.2 real, 632.3 MB
[runlim] sample:		8510.5 time, 2150.2 real, 644.2 MB
[runlim] sample:		8550.1 time, 2160.2 real, 650.9 MB
[runlim] sample:		8589.7 time, 2170.2 real, 645.5 MB
[runlim] sample:		8629.3 time, 2180.2 real, 648.2 MB
[runlim] sample:		8668.9 time, 2190.2 real, 650.0 MB
[runlim] sample:		8708.5 time, 2200.2 real, 655.3 MB
[runlim] sample:		8748.2 time, 2210.2 real, 650.5 MB
[runlim] sample:		8787.8 time, 2220.2 real, 657.6 MB
[runlim] sample:		8827.4 time, 2230.2 real, 654.3 MB
[runlim] sample:		8867.0 time, 2240.2 real, 656.3 MB
[runlim] sample:		8906.6 time, 2250.2 real, 662.0 MB
[runlim] sample:		8946.2 time, 2260.2 real, 657.5 MB
[runlim] sample:		8985.8 time, 2270.2 real, 685.3 MB
[runlim] sample:		9025.5 time, 2280.2 real, 687.1 MB
[runlim] sample:		9065.1 time, 2290.2 real, 687.9 MB
[runlim] sample:		9104.7 time, 2300.2 real, 685.1 MB
[runlim] sample:		9144.3 time, 2310.2 real, 691.2 MB
[runlim] sample:		9183.9 time, 2320.2 real, 690.2 MB
[runlim] sample:		9223.5 time, 2330.2 real, 695.0 MB
[runlim] sample:		9263.1 time, 2340.2 real, 690.1 MB
[runlim] sample:		9302.7 time, 2350.2 real, 699.7 MB
[runlim] sample:		9342.3 time, 2360.2 real, 696.4 MB
[runlim] sample:		9382.0 time, 2370.2 real, 676.0 MB
[runlim] sample:		9421.6 time, 2380.2 real, 673.2 MB
[runlim] sample:		9461.2 time, 2390.2 real, 678.2 MB
[runlim] sample:		9500.8 time, 2400.2 real, 672.1 MB
[runlim] sample:		9540.4 time, 2410.2 real, 677.9 MB
[runlim] sample:		9580.0 time, 2420.2 real, 668.2 MB
[runlim] sample:		9619.6 time, 2430.2 real, 682.0 MB
[runlim] sample:		9659.2 time, 2440.2 real, 668.7 MB
[runlim] sample:		9698.9 time, 2450.2 real, 676.3 MB
[runlim] sample:		9738.5 time, 2460.2 real, 678.6 MB
[runlim] sample:		9778.1 time, 2470.2 real, 694.9 MB
[runlim] sample:		9817.7 time, 2480.2 real, 698.9 MB
[runlim] sample:		9857.3 time, 2490.2 real, 699.7 MB
[runlim] sample:		9896.9 time, 2500.2 real, 704.2 MB
[runlim] sample:		9936.5 time, 2510.2 real, 705.0 MB
[runlim] sample:		9976.1 time, 2520.2 real, 707.2 MB
[runlim] sample:		10015.7 time, 2530.2 real, 722.0 MB
[runlim] sample:		10055.3 time, 2540.2 real, 722.5 MB
[runlim] sample:		10095.0 time, 2550.2 real, 724.7 MB
[runlim] sample:		10134.6 time, 2560.2 real, 727.1 MB
[runlim] sample:		10174.2 time, 2570.2 real, 729.3 MB
[runlim] sample:		10213.8 time, 2580.2 real, 729.7 MB
[runlim] sample:		10253.4 time, 2590.2 real, 727.6 MB
[runlim] sample:		10293.0 time, 2600.2 real, 709.5 MB
[runlim] sample:		10332.6 time, 2610.2 real, 709.8 MB
[runlim] sample:		10372.2 time, 2620.2 real, 710.3 MB
[runlim] sample:		10411.9 time, 2630.2 real, 692.5 MB
[runlim] sample:		10451.5 time, 2640.2 real, 693.1 MB
[runlim] sample:		10491.1 time, 2650.2 real, 694.0 MB
[runlim] sample:		10530.7 time, 2660.2 real, 694.4 MB
[runlim] sample:		10570.3 time, 2670.2 real, 694.5 MB
[runlim] sample:		10609.9 time, 2680.2 real, 695.1 MB
[runlim] sample:		10649.5 time, 2690.2 real, 701.8 MB
[runlim] sample:		10689.1 time, 2700.2 real, 701.9 MB
[runlim] sample:		10728.7 time, 2710.2 real, 743.5 MB
[runlim] sample:		10768.3 time, 2720.2 real, 748.3 MB
[runlim] sample:		10808.0 time, 2730.2 real, 749.8 MB
[runlim] sample:		10847.5 time, 2740.2 real, 753.8 MB
[runlim] sample:		10887.2 time, 2750.2 real, 755.8 MB
[runlim] sample:		10926.8 time, 2760.2 real, 757.8 MB
[runlim] sample:		10966.4 time, 2770.2 real, 757.8 MB
[runlim] sample:		11006.0 time, 2780.2 real, 761.7 MB
[runlim] sample:		11045.6 time, 2790.2 real, 761.7 MB
[runlim] sample:		11085.2 time, 2800.2 real, 763.8 MB
[runlim] sample:		11124.8 time, 2810.2 real, 765.8 MB
[runlim] sample:		11164.4 time, 2820.2 real, 766.2 MB
[runlim] sample:		11204.0 time, 2830.2 real, 766.2 MB
[runlim] sample:		11243.6 time, 2840.2 real, 768.2 MB
[runlim] sample:		11283.2 time, 2850.2 real, 768.2 MB
[runlim] sample:		11322.8 time, 2860.2 real, 770.2 MB
[runlim] sample:		11362.5 time, 2870.2 real, 771.5 MB
[runlim] sample:		11402.1 time, 2880.2 real, 771.8 MB
[runlim] sample:		11441.7 time, 2890.2 real, 771.8 MB
[runlim] sample:		11481.3 time, 2900.2 real, 782.1 MB
[runlim] sample:		11520.9 time, 2910.2 real, 773.6 MB
[runlim] sample:		11560.5 time, 2920.2 real, 785.8 MB
[runlim] sample:		11600.1 time, 2930.2 real, 786.9 MB
[runlim] sample:		11639.8 time, 2940.2 real, 779.8 MB
[runlim] sample:		11679.4 time, 2950.2 real, 780.1 MB
[runlim] sample:		11719.0 time, 2960.2 real, 782.4 MB
[runlim] sample:		11758.6 time, 2970.2 real, 782.6 MB
[runlim] sample:		11798.2 time, 2980.2 real, 785.1 MB
[runlim] sample:		11837.8 time, 2990.2 real, 787.3 MB
[runlim] sample:		11877.4 time, 3000.2 real, 790.0 MB
[runlim] sample:		11917.0 time, 3010.2 real, 792.0 MB
[runlim] sample:		11956.7 time, 3020.2 real, 792.2 MB
[runlim] sample:		11996.3 time, 3030.2 real, 792.5 MB
[runlim] sample:		12035.9 time, 3040.2 real, 802.0 MB
[runlim] sample:		12075.5 time, 3050.2 real, 804.4 MB
[runlim] sample:		12115.1 time, 3060.2 real, 800.4 MB
[runlim] sample:		12154.7 time, 3070.2 real, 806.0 MB
[runlim] sample:		12194.3 time, 3080.2 real, 819.0 MB
[runlim] sample:		12233.9 time, 3090.2 real, 810.0 MB
[runlim] sample:		12273.5 time, 3100.2 real, 819.7 MB
[runlim] sample:		12313.1 time, 3110.2 real, 811.2 MB
[runlim] sample:		12352.7 time, 3120.2 real, 825.2 MB
[runlim] sample:		12392.4 time, 3130.2 real, 824.2 MB
[runlim] sample:		12432.0 time, 3140.2 real, 824.9 MB
[runlim] sample:		12471.6 time, 3150.2 real, 828.2 MB
[runlim] sample:		12511.2 time, 3160.2 real, 829.5 MB
[runlim] sample:		12550.8 time, 3170.2 real, 823.5 MB
[runlim] sample:		12590.4 time, 3180.2 real, 823.5 MB
[runlim] sample:		12630.0 time, 3190.2 real, 824.0 MB
[runlim] sample:		12669.6 time, 3200.2 real, 835.9 MB
[runlim] sample:		12709.2 time, 3210.2 real, 826.9 MB
[runlim] sample:		12748.8 time, 3220.2 real, 837.9 MB
[runlim] sample:		12788.5 time, 3230.2 real, 828.9 MB
[runlim] sample:		12828.1 time, 3240.2 real, 838.8 MB
[runlim] sample:		12867.7 time, 3250.2 real, 831.2 MB
[runlim] sample:		12907.3 time, 3260.2 real, 833.5 MB
[runlim] sample:		12946.9 time, 3270.2 real, 842.5 MB
[runlim] sample:		12986.5 time, 3280.2 real, 833.5 MB
[runlim] sample:		13026.1 time, 3290.2 real, 843.3 MB
[runlim] sample:		13065.7 time, 3300.2 real, 843.3 MB
[runlim] sample:		13105.3 time, 3310.2 real, 837.4 MB
[runlim] sample:		13144.9 time, 3320.2 real, 845.4 MB
[runlim] sample:		13184.6 time, 3330.2 real, 845.2 MB
[runlim] sample:		13224.2 time, 3340.2 real, 836.2 MB
[runlim] sample:		13263.8 time, 3350.2 real, 847.4 MB
[runlim] sample:		13303.4 time, 3360.2 real, 848.8 MB
[runlim] sample:		13343.0 time, 3370.2 real, 851.3 MB
[runlim] sample:		13382.5 time, 3380.2 real, 852.1 MB
[runlim] sample:		13422.2 time, 3390.2 real, 842.2 MB
[runlim] sample:		13461.8 time, 3400.2 real, 842.7 MB
[runlim] sample:		13501.4 time, 3410.2 real, 843.5 MB
[runlim] sample:		13541.0 time, 3420.2 real, 852.7 MB
[runlim] sample:		13580.6 time, 3430.2 real, 854.7 MB
[runlim] sample:		13620.2 time, 3440.2 real, 845.7 MB
[runlim] sample:		13659.8 time, 3450.2 real, 855.7 MB
[runlim] sample:		13699.4 time, 3460.2 real, 855.0 MB
[runlim] sample:		13739.0 time, 3470.2 real, 775.5 MB
[runlim] sample:		13778.7 time, 3480.2 real, 800.1 MB
[runlim] sample:		13818.3 time, 3490.2 real, 802.1 MB
[runlim] sample:		13857.9 time, 3500.2 real, 803.0 MB
[runlim] sample:		13897.5 time, 3510.2 real, 806.6 MB
[runlim] sample:		13937.1 time, 3520.2 real, 801.3 MB
[runlim] sample:		13976.7 time, 3530.2 real, 811.8 MB
[runlim] sample:		14016.3 time, 3540.2 real, 813.0 MB
[runlim] sample:		14055.9 time, 3550.2 real, 815.5 MB
[runlim] sample:		14095.5 time, 3560.2 real, 805.8 MB
[runlim] sample:		14135.1 time, 3570.2 real, 817.8 MB
[runlim] sample:		14174.8 time, 3580.2 real, 816.8 MB
[runlim] sample:		14214.4 time, 3590.2 real, 807.0 MB
[runlim] end:			Wed Sep 16 09:01:18 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.07 seconds
[runlim] time:			14253.19 seconds
[runlim] space:			901.5 MB
[runlim] samples:		35998
