[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/all/selection/random/beemcmbrdg7f2.aig
[runlim] start:			Sun Sep 20 03:39:18 2015
[runlim] main pid:		11671
[runlim] sample:		37.1 time, 10.3 real, 94.6 MB
[runlim] sample:		76.8 time, 20.3 real, 114.5 MB
[runlim] sample:		116.4 time, 30.3 real, 134.0 MB
[runlim] sample:		156.1 time, 40.3 real, 147.6 MB
[runlim] sample:		195.7 time, 50.3 real, 147.3 MB
[runlim] sample:		235.4 time, 60.3 real, 162.4 MB
[runlim] sample:		275.0 time, 70.3 real, 176.0 MB
[runlim] sample:		314.6 time, 80.3 real, 184.7 MB
[runlim] sample:		354.3 time, 90.3 real, 174.8 MB
[runlim] sample:		393.9 time, 100.3 real, 192.2 MB
[runlim] sample:		433.6 time, 110.3 real, 189.1 MB
[runlim] sample:		473.2 time, 120.3 real, 198.6 MB
[runlim] sample:		512.9 time, 130.3 real, 228.2 MB
[runlim] sample:		552.5 time, 140.3 real, 232.4 MB
[runlim] sample:		592.1 time, 150.3 real, 235.4 MB
[runlim] sample:		631.7 time, 160.3 real, 243.9 MB
[runlim] sample:		671.3 time, 170.3 real, 254.7 MB
[runlim] sample:		711.0 time, 180.3 real, 254.8 MB
[runlim] sample:		750.6 time, 190.3 real, 233.3 MB
[runlim] sample:		790.2 time, 200.3 real, 233.8 MB
[runlim] sample:		829.9 time, 210.3 real, 243.0 MB
[runlim] sample:		869.5 time, 220.3 real, 249.0 MB
[runlim] sample:		909.1 time, 230.3 real, 281.3 MB
[runlim] sample:		948.7 time, 240.3 real, 312.1 MB
[runlim] sample:		988.4 time, 250.3 real, 317.1 MB
[runlim] sample:		1028.0 time, 260.3 real, 321.9 MB
[runlim] sample:		1067.6 time, 270.3 real, 322.6 MB
[runlim] sample:		1107.2 time, 280.3 real, 329.8 MB
[runlim] sample:		1146.8 time, 290.3 real, 332.4 MB
[runlim] sample:		1186.4 time, 300.3 real, 338.9 MB
[runlim] sample:		1226.0 time, 310.3 real, 356.9 MB
[runlim] sample:		1265.6 time, 320.3 real, 358.1 MB
[runlim] sample:		1305.2 time, 330.3 real, 360.2 MB
[runlim] sample:		1344.8 time, 340.3 real, 360.5 MB
[runlim] sample:		1384.5 time, 350.3 real, 369.3 MB
[runlim] sample:		1424.1 time, 360.3 real, 356.5 MB
[runlim] sample:		1463.7 time, 370.3 real, 311.1 MB
[runlim] sample:		1503.3 time, 380.3 real, 323.3 MB
[runlim] sample:		1542.9 time, 390.3 real, 327.8 MB
[runlim] sample:		1582.5 time, 400.3 real, 338.2 MB
[runlim] sample:		1622.1 time, 410.3 real, 356.5 MB
[runlim] sample:		1661.8 time, 420.3 real, 353.0 MB
[runlim] sample:		1701.4 time, 430.3 real, 332.7 MB
[runlim] sample:		1741.0 time, 440.3 real, 346.9 MB
[runlim] sample:		1780.6 time, 450.3 real, 351.9 MB
[runlim] sample:		1820.2 time, 460.3 real, 365.3 MB
[runlim] sample:		1859.8 time, 470.3 real, 383.1 MB
[runlim] sample:		1899.4 time, 480.3 real, 387.1 MB
[runlim] sample:		1939.0 time, 490.3 real, 391.2 MB
[runlim] sample:		1978.6 time, 500.3 real, 389.1 MB
[runlim] sample:		2018.2 time, 510.3 real, 391.5 MB
[runlim] sample:		2057.8 time, 520.3 real, 377.3 MB
[runlim] sample:		2097.4 time, 530.3 real, 379.8 MB
[runlim] sample:		2137.1 time, 540.3 real, 396.5 MB
[runlim] sample:		2176.7 time, 550.3 real, 431.6 MB
[runlim] sample:		2216.3 time, 560.3 real, 452.7 MB
[runlim] sample:		2255.9 time, 570.3 real, 470.4 MB
[runlim] sample:		2295.5 time, 580.3 real, 467.4 MB
[runlim] sample:		2335.1 time, 590.3 real, 467.4 MB
[runlim] sample:		2374.7 time, 600.3 real, 468.0 MB
[runlim] sample:		2414.3 time, 610.3 real, 477.0 MB
[runlim] sample:		2453.9 time, 620.3 real, 478.2 MB
[runlim] sample:		2493.5 time, 630.3 real, 432.5 MB
[runlim] sample:		2533.1 time, 640.3 real, 447.0 MB
[runlim] sample:		2572.7 time, 650.3 real, 458.5 MB
[runlim] sample:		2612.3 time, 660.3 real, 489.8 MB
[runlim] sample:		2651.9 time, 670.3 real, 492.2 MB
[runlim] sample:		2691.5 time, 680.3 real, 494.5 MB
[runlim] sample:		2731.1 time, 690.3 real, 489.1 MB
[runlim] sample:		2770.7 time, 700.3 real, 475.1 MB
[runlim] sample:		2810.3 time, 710.3 real, 477.1 MB
[runlim] sample:		2849.9 time, 720.3 real, 477.1 MB
[runlim] sample:		2889.5 time, 730.3 real, 491.1 MB
[runlim] sample:		2929.1 time, 740.3 real, 493.1 MB
[runlim] sample:		2968.7 time, 750.3 real, 495.1 MB
[runlim] sample:		3008.3 time, 760.3 real, 497.4 MB
[runlim] sample:		3047.9 time, 770.3 real, 501.6 MB
[runlim] sample:		3087.5 time, 780.3 real, 501.4 MB
[runlim] sample:		3127.1 time, 790.3 real, 504.2 MB
[runlim] sample:		3166.7 time, 800.3 real, 506.2 MB
[runlim] sample:		3206.3 time, 810.3 real, 510.2 MB
[runlim] sample:		3245.9 time, 820.3 real, 510.2 MB
[runlim] sample:		3285.5 time, 830.3 real, 512.2 MB
[runlim] sample:		3325.1 time, 840.3 real, 524.2 MB
[runlim] sample:		3364.7 time, 850.3 real, 516.9 MB
[runlim] sample:		3404.3 time, 860.3 real, 517.2 MB
[runlim] sample:		3443.9 time, 870.3 real, 519.4 MB
[runlim] sample:		3483.5 time, 880.3 real, 523.3 MB
[runlim] sample:		3523.1 time, 890.3 real, 525.6 MB
[runlim] sample:		3562.7 time, 900.3 real, 514.6 MB
[runlim] sample:		3602.3 time, 910.3 real, 516.6 MB
[runlim] sample:		3641.9 time, 920.3 real, 474.6 MB
[runlim] sample:		3681.5 time, 930.3 real, 476.9 MB
[runlim] sample:		3721.1 time, 940.3 real, 479.4 MB
[runlim] sample:		3760.7 time, 950.3 real, 509.4 MB
[runlim] sample:		3800.3 time, 960.3 real, 508.2 MB
[runlim] sample:		3839.9 time, 970.3 real, 513.0 MB
[runlim] sample:		3879.5 time, 980.3 real, 517.0 MB
[runlim] sample:		3919.2 time, 990.3 real, 517.0 MB
[runlim] sample:		3958.8 time, 1000.3 real, 510.9 MB
[runlim] sample:		3998.4 time, 1010.3 real, 524.9 MB
[runlim] sample:		4038.0 time, 1020.3 real, 526.9 MB
[runlim] sample:		4077.6 time, 1030.3 real, 519.3 MB
[runlim] sample:		4117.2 time, 1040.3 real, 529.4 MB
[runlim] sample:		4156.8 time, 1050.3 real, 518.7 MB
[runlim] sample:		4196.4 time, 1060.3 real, 521.0 MB
[runlim] sample:		4236.0 time, 1070.3 real, 537.2 MB
[runlim] sample:		4275.6 time, 1080.3 real, 537.2 MB
[runlim] sample:		4315.2 time, 1090.3 real, 506.3 MB
[runlim] sample:		4354.8 time, 1100.3 real, 509.1 MB
[runlim] sample:		4394.4 time, 1110.3 real, 516.5 MB
[runlim] sample:		4434.0 time, 1120.3 real, 520.6 MB
[runlim] sample:		4473.6 time, 1130.3 real, 549.7 MB
[runlim] sample:		4513.2 time, 1140.3 real, 552.2 MB
[runlim] sample:		4552.8 time, 1150.3 real, 556.7 MB
[runlim] sample:		4592.4 time, 1160.3 real, 534.7 MB
[runlim] sample:		4632.1 time, 1170.3 real, 524.7 MB
[runlim] sample:		4671.6 time, 1180.3 real, 527.7 MB
[runlim] sample:		4711.2 time, 1190.3 real, 529.9 MB
[runlim] sample:		4750.9 time, 1200.3 real, 546.2 MB
[runlim] sample:		4790.5 time, 1210.3 real, 548.4 MB
[runlim] sample:		4830.1 time, 1220.3 real, 564.0 MB
[runlim] sample:		4869.7 time, 1230.3 real, 566.2 MB
[runlim] sample:		4909.3 time, 1240.3 real, 577.1 MB
[runlim] sample:		4948.9 time, 1250.3 real, 580.4 MB
[runlim] sample:		4988.5 time, 1260.3 real, 582.6 MB
[runlim] sample:		5028.1 time, 1270.3 real, 574.4 MB
[runlim] sample:		5067.7 time, 1280.3 real, 576.4 MB
[runlim] sample:		5107.3 time, 1290.3 real, 580.4 MB
[runlim] sample:		5146.9 time, 1300.3 real, 584.4 MB
[runlim] sample:		5186.5 time, 1310.3 real, 597.4 MB
[runlim] sample:		5226.1 time, 1320.3 real, 601.7 MB
[runlim] sample:		5265.7 time, 1330.3 real, 603.9 MB
[runlim] sample:		5305.3 time, 1340.3 real, 547.6 MB
[runlim] sample:		5344.9 time, 1350.3 real, 560.3 MB
[runlim] sample:		5384.6 time, 1360.3 real, 583.8 MB
[runlim] sample:		5424.2 time, 1370.3 real, 587.8 MB
[runlim] sample:		5463.8 time, 1380.3 real, 589.8 MB
[runlim] sample:		5503.4 time, 1390.3 real, 591.8 MB
[runlim] sample:		5543.0 time, 1400.3 real, 577.8 MB
[runlim] sample:		5582.6 time, 1410.3 real, 580.0 MB
[runlim] sample:		5622.2 time, 1420.3 real, 582.0 MB
[runlim] sample:		5661.8 time, 1430.3 real, 584.0 MB
[runlim] sample:		5701.4 time, 1440.3 real, 588.0 MB
[runlim] sample:		5741.1 time, 1450.3 real, 588.0 MB
[runlim] sample:		5780.7 time, 1460.3 real, 601.3 MB
[runlim] sample:		5820.2 time, 1470.3 real, 592.5 MB
[runlim] sample:		5859.9 time, 1480.3 real, 594.5 MB
[runlim] sample:		5899.5 time, 1490.3 real, 569.6 MB
[runlim] sample:		5939.1 time, 1500.3 real, 570.8 MB
[runlim] sample:		5978.7 time, 1510.3 real, 573.6 MB
[runlim] sample:		6018.3 time, 1520.3 real, 573.9 MB
[runlim] sample:		6057.9 time, 1530.3 real, 575.9 MB
[runlim] sample:		6097.6 time, 1540.3 real, 579.9 MB
[runlim] sample:		6137.2 time, 1550.3 real, 579.9 MB
[runlim] sample:		6176.8 time, 1560.3 real, 581.9 MB
[runlim] sample:		6216.4 time, 1570.3 real, 583.9 MB
[runlim] sample:		6256.0 time, 1580.3 real, 601.9 MB
[runlim] sample:		6295.6 time, 1590.3 real, 608.8 MB
[runlim] sample:		6335.3 time, 1600.3 real, 621.9 MB
[runlim] sample:		6374.9 time, 1610.3 real, 624.2 MB
[runlim] sample:		6414.5 time, 1620.3 real, 626.4 MB
[runlim] sample:		6454.1 time, 1630.3 real, 628.5 MB
[runlim] sample:		6493.8 time, 1640.3 real, 630.5 MB
[runlim] sample:		6533.4 time, 1650.3 real, 633.1 MB
[runlim] sample:		6573.0 time, 1660.3 real, 566.3 MB
[runlim] sample:		6612.6 time, 1670.3 real, 571.1 MB
[runlim] sample:		6652.2 time, 1680.3 real, 573.3 MB
[runlim] sample:		6691.9 time, 1690.3 real, 595.8 MB
[runlim] sample:		6731.5 time, 1700.3 real, 598.0 MB
[runlim] sample:		6771.1 time, 1710.3 real, 600.0 MB
[runlim] sample:		6810.7 time, 1720.3 real, 602.1 MB
[runlim] sample:		6850.3 time, 1730.3 real, 604.1 MB
[runlim] sample:		6889.9 time, 1740.3 real, 594.0 MB
[runlim] sample:		6929.5 time, 1750.3 real, 596.0 MB
[runlim] sample:		6969.1 time, 1760.3 real, 598.0 MB
[runlim] sample:		7008.7 time, 1770.3 real, 600.0 MB
[runlim] sample:		7048.3 time, 1780.3 real, 602.0 MB
[runlim] sample:		7087.9 time, 1790.3 real, 604.0 MB
[runlim] sample:		7127.5 time, 1800.3 real, 606.0 MB
[runlim] sample:		7167.1 time, 1810.3 real, 606.0 MB
[runlim] sample:		7206.8 time, 1820.3 real, 608.0 MB
[runlim] sample:		7246.4 time, 1830.3 real, 612.0 MB
[runlim] sample:		7286.0 time, 1840.3 real, 617.9 MB
[runlim] sample:		7325.6 time, 1850.3 real, 617.9 MB
[runlim] sample:		7365.2 time, 1860.3 real, 619.9 MB
[runlim] sample:		7404.8 time, 1870.3 real, 623.9 MB
[runlim] sample:		7444.4 time, 1880.3 real, 626.2 MB
[runlim] sample:		7484.0 time, 1890.3 real, 626.2 MB
[runlim] sample:		7523.6 time, 1900.3 real, 628.2 MB
[runlim] sample:		7563.2 time, 1910.3 real, 630.2 MB
[runlim] sample:		7602.8 time, 1920.3 real, 630.2 MB
[runlim] sample:		7642.4 time, 1930.3 real, 632.2 MB
[runlim] sample:		7682.0 time, 1940.3 real, 634.2 MB
[runlim] sample:		7721.6 time, 1950.3 real, 636.4 MB
[runlim] sample:		7761.2 time, 1960.3 real, 638.4 MB
[runlim] sample:		7800.8 time, 1970.3 real, 640.7 MB
[runlim] sample:		7840.4 time, 1980.3 real, 640.7 MB
[runlim] sample:		7880.0 time, 1990.3 real, 642.7 MB
[runlim] sample:		7919.6 time, 2000.3 real, 644.7 MB
[runlim] sample:		7959.2 time, 2010.3 real, 664.7 MB
[runlim] sample:		7998.8 time, 2020.3 real, 609.4 MB
[runlim] sample:		8038.4 time, 2030.3 real, 611.4 MB
[runlim] sample:		8078.0 time, 2040.3 real, 613.4 MB
[runlim] sample:		8117.6 time, 2050.3 real, 625.4 MB
[runlim] sample:		8157.2 time, 2060.3 real, 619.3 MB
[runlim] sample:		8196.9 time, 2070.3 real, 624.3 MB
[runlim] sample:		8236.5 time, 2080.3 real, 626.3 MB
[runlim] sample:		8276.0 time, 2090.3 real, 626.3 MB
[runlim] sample:		8315.6 time, 2100.3 real, 628.7 MB
[runlim] sample:		8355.2 time, 2110.3 real, 639.2 MB
[runlim] sample:		8394.9 time, 2120.3 real, 639.2 MB
[runlim] sample:		8434.5 time, 2130.3 real, 628.8 MB
[runlim] sample:		8474.0 time, 2140.3 real, 633.0 MB
[runlim] sample:		8513.6 time, 2150.3 real, 611.1 MB
[runlim] sample:		8553.2 time, 2160.3 real, 616.7 MB
[runlim] sample:		8592.9 time, 2170.3 real, 609.1 MB
[runlim] sample:		8632.5 time, 2180.3 real, 612.5 MB
[runlim] sample:		8672.1 time, 2190.3 real, 618.5 MB
[runlim] sample:		8711.7 time, 2200.3 real, 622.5 MB
[runlim] sample:		8751.3 time, 2210.3 real, 623.7 MB
[runlim] sample:		8790.9 time, 2220.3 real, 625.7 MB
[runlim] sample:		8830.5 time, 2230.3 real, 629.7 MB
[runlim] sample:		8870.1 time, 2240.3 real, 629.7 MB
[runlim] sample:		8909.7 time, 2250.3 real, 664.2 MB
[runlim] sample:		8949.3 time, 2260.3 real, 666.2 MB
[runlim] sample:		8988.9 time, 2270.3 real, 688.5 MB
[runlim] sample:		9028.5 time, 2280.3 real, 691.0 MB
[runlim] sample:		9068.1 time, 2290.3 real, 676.4 MB
[runlim] sample:		9107.6 time, 2300.3 real, 678.7 MB
[runlim] sample:		9147.2 time, 2310.3 real, 678.7 MB
[runlim] sample:		9186.8 time, 2320.3 real, 680.7 MB
[runlim] sample:		9226.5 time, 2330.3 real, 684.6 MB
[runlim] sample:		9266.0 time, 2340.3 real, 697.3 MB
[runlim] sample:		9305.6 time, 2350.3 real, 701.3 MB
[runlim] sample:		9345.2 time, 2360.3 real, 701.3 MB
[runlim] sample:		9384.9 time, 2370.3 real, 706.4 MB
[runlim] sample:		9424.5 time, 2380.3 real, 710.4 MB
[runlim] sample:		9464.0 time, 2390.3 real, 712.4 MB
[runlim] sample:		9503.6 time, 2400.3 real, 732.6 MB
[runlim] sample:		9543.3 time, 2410.3 real, 732.9 MB
[runlim] sample:		9582.9 time, 2420.3 real, 737.1 MB
[runlim] sample:		9622.5 time, 2430.3 real, 739.7 MB
[runlim] sample:		9662.1 time, 2440.3 real, 711.4 MB
[runlim] sample:		9701.7 time, 2450.3 real, 651.4 MB
[runlim] sample:		9741.2 time, 2460.3 real, 654.4 MB
[runlim] sample:		9780.9 time, 2470.3 real, 677.2 MB
[runlim] sample:		9820.5 time, 2480.3 real, 679.2 MB
[runlim] sample:		9860.1 time, 2490.3 real, 681.2 MB
[runlim] sample:		9899.7 time, 2500.3 real, 683.2 MB
[runlim] sample:		9939.3 time, 2510.3 real, 686.7 MB
[runlim] sample:		9978.9 time, 2520.3 real, 671.2 MB
[runlim] sample:		10018.5 time, 2530.3 real, 675.2 MB
[runlim] sample:		10058.1 time, 2540.3 real, 695.5 MB
[runlim] sample:		10097.7 time, 2550.3 real, 697.7 MB
[runlim] sample:		10137.3 time, 2560.3 real, 710.8 MB
[runlim] sample:		10176.9 time, 2570.3 real, 713.2 MB
[runlim] sample:		10216.5 time, 2580.3 real, 733.6 MB
[runlim] sample:		10256.1 time, 2590.3 real, 737.4 MB
[runlim] sample:		10295.7 time, 2600.3 real, 739.4 MB
[runlim] sample:		10335.3 time, 2610.3 real, 743.4 MB
[runlim] sample:		10374.9 time, 2620.3 real, 745.4 MB
[runlim] sample:		10414.5 time, 2630.3 real, 749.4 MB
[runlim] sample:		10454.1 time, 2640.3 real, 751.4 MB
[runlim] sample:		10493.6 time, 2650.3 real, 753.4 MB
[runlim] sample:		10533.2 time, 2660.3 real, 755.4 MB
[runlim] sample:		10572.8 time, 2670.3 real, 755.4 MB
[runlim] sample:		10612.4 time, 2680.3 real, 759.4 MB
[runlim] sample:		10652.0 time, 2690.3 real, 761.4 MB
[runlim] sample:		10691.6 time, 2700.3 real, 769.4 MB
[runlim] sample:		10731.2 time, 2710.3 real, 771.4 MB
[runlim] sample:		10770.8 time, 2720.3 real, 773.4 MB
[runlim] sample:		10810.4 time, 2730.3 real, 775.4 MB
[runlim] sample:		10850.0 time, 2740.3 real, 777.4 MB
[runlim] sample:		10889.6 time, 2750.3 real, 778.7 MB
[runlim] sample:		10929.2 time, 2760.3 real, 781.2 MB
[runlim] sample:		10968.8 time, 2770.3 real, 801.4 MB
[runlim] sample:		11008.4 time, 2780.3 real, 801.7 MB
[runlim] sample:		11048.0 time, 2790.3 real, 803.9 MB
[runlim] sample:		11087.6 time, 2800.3 real, 806.2 MB
[runlim] sample:		11127.2 time, 2810.3 real, 808.2 MB
[runlim] sample:		11166.8 time, 2820.3 real, 810.4 MB
[runlim] sample:		11206.4 time, 2830.3 real, 734.2 MB
[runlim] sample:		11246.0 time, 2840.3 real, 757.6 MB
[runlim] sample:		11285.6 time, 2850.3 real, 773.2 MB
[runlim] sample:		11325.2 time, 2860.3 real, 775.2 MB
[runlim] sample:		11364.8 time, 2870.3 real, 779.2 MB
[runlim] sample:		11404.4 time, 2880.3 real, 763.3 MB
[runlim] sample:		11444.0 time, 2890.3 real, 776.8 MB
[runlim] sample:		11483.6 time, 2900.3 real, 778.8 MB
[runlim] sample:		11523.2 time, 2910.3 real, 781.0 MB
[runlim] sample:		11562.8 time, 2920.3 real, 785.5 MB
[runlim] sample:		11602.4 time, 2930.3 real, 787.8 MB
[runlim] sample:		11642.0 time, 2940.3 real, 792.0 MB
[runlim] sample:		11681.6 time, 2950.3 real, 795.0 MB
[runlim] sample:		11721.2 time, 2960.3 real, 802.3 MB
[runlim] sample:		11760.8 time, 2970.3 real, 793.2 MB
[runlim] sample:		11800.4 time, 2980.3 real, 797.2 MB
[runlim] sample:		11840.0 time, 2990.3 real, 801.2 MB
[runlim] sample:		11879.6 time, 3000.3 real, 803.2 MB
[runlim] sample:		11919.2 time, 3010.3 real, 805.2 MB
[runlim] sample:		11958.8 time, 3020.3 real, 807.2 MB
[runlim] sample:		11998.4 time, 3030.3 real, 827.2 MB
[runlim] sample:		12038.0 time, 3040.3 real, 849.2 MB
[runlim] sample:		12077.6 time, 3050.3 real, 867.2 MB
[runlim] sample:		12117.2 time, 3060.3 real, 869.2 MB
[runlim] sample:		12156.8 time, 3070.3 real, 873.2 MB
[runlim] sample:		12196.4 time, 3080.3 real, 877.2 MB
[runlim] sample:		12236.0 time, 3090.3 real, 877.9 MB
[runlim] sample:		12275.6 time, 3100.3 real, 879.1 MB
[runlim] sample:		12315.2 time, 3110.3 real, 883.4 MB
[runlim] sample:		12354.8 time, 3120.3 real, 874.5 MB
[runlim] sample:		12394.4 time, 3130.3 real, 874.5 MB
[runlim] sample:		12434.0 time, 3140.3 real, 879.8 MB
[runlim] sample:		12473.6 time, 3150.3 real, 835.6 MB
[runlim] sample:		12513.2 time, 3160.3 real, 837.6 MB
[runlim] sample:		12552.9 time, 3170.3 real, 839.6 MB
[runlim] sample:		12592.5 time, 3180.3 real, 839.6 MB
[runlim] sample:		12632.1 time, 3190.3 real, 843.6 MB
[runlim] sample:		12671.7 time, 3200.3 real, 847.6 MB
[runlim] sample:		12711.3 time, 3210.3 real, 847.6 MB
[runlim] sample:		12750.9 time, 3220.3 real, 849.6 MB
[runlim] sample:		12790.5 time, 3230.3 real, 859.5 MB
[runlim] sample:		12830.1 time, 3240.3 real, 776.7 MB
[runlim] sample:		12869.7 time, 3250.3 real, 781.5 MB
[runlim] sample:		12909.3 time, 3260.3 real, 802.5 MB
[runlim] sample:		12948.9 time, 3270.3 real, 806.5 MB
[runlim] sample:		12988.5 time, 3280.3 real, 797.6 MB
[runlim] sample:		13028.1 time, 3290.3 real, 801.6 MB
[runlim] sample:		13067.7 time, 3300.3 real, 802.0 MB
[runlim] sample:		13107.3 time, 3310.3 real, 787.5 MB
[runlim] sample:		13146.9 time, 3320.3 real, 787.5 MB
[runlim] sample:		13186.5 time, 3330.3 real, 791.5 MB
[runlim] sample:		13226.1 time, 3340.3 real, 793.5 MB
[runlim] sample:		13265.7 time, 3350.3 real, 795.5 MB
[runlim] sample:		13305.3 time, 3360.3 real, 797.5 MB
[runlim] sample:		13345.0 time, 3370.3 real, 799.5 MB
[runlim] sample:		13384.5 time, 3380.3 real, 801.5 MB
[runlim] sample:		13424.2 time, 3390.3 real, 803.5 MB
[runlim] sample:		13463.8 time, 3400.3 real, 805.5 MB
[runlim] sample:		13503.4 time, 3410.3 real, 808.5 MB
[runlim] sample:		13543.0 time, 3420.3 real, 810.7 MB
[runlim] sample:		13582.6 time, 3430.3 real, 814.7 MB
[runlim] sample:		13622.2 time, 3440.3 real, 816.7 MB
[runlim] sample:		13661.8 time, 3450.3 real, 816.7 MB
[runlim] sample:		13701.4 time, 3460.3 real, 818.7 MB
[runlim] sample:		13741.0 time, 3470.3 real, 833.7 MB
[runlim] sample:		13780.6 time, 3480.3 real, 824.7 MB
[runlim] sample:		13820.2 time, 3490.3 real, 826.7 MB
[runlim] sample:		13859.8 time, 3500.3 real, 826.8 MB
[runlim] sample:		13899.4 time, 3510.3 real, 828.8 MB
[runlim] sample:		13939.0 time, 3520.3 real, 851.6 MB
[runlim] sample:		13978.6 time, 3530.3 real, 853.6 MB
[runlim] sample:		14018.2 time, 3540.3 real, 853.6 MB
[runlim] sample:		14057.8 time, 3550.3 real, 855.6 MB
[runlim] sample:		14097.4 time, 3560.3 real, 859.6 MB
[runlim] sample:		14137.0 time, 3570.3 real, 859.9 MB
[runlim] sample:		14176.6 time, 3580.3 real, 861.2 MB
[runlim] sample:		14216.2 time, 3590.3 real, 863.4 MB
[runlim] end:			Sun Sep 20 04:39:18 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.06 seconds
[runlim] time:			14254.63 seconds
[runlim] space:			885.4 MB
[runlim] samples:		35997
