[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/6s161.aig
[runlim] start:			Tue Sep 15 18:00:30 2015
[runlim] main pid:		29320
[runlim] sample:		38.0 time, 10.8 real, 81.8 MB
[runlim] sample:		77.6 time, 20.8 real, 115.0 MB
[runlim] sample:		117.3 time, 30.8 real, 118.4 MB
[runlim] sample:		156.9 time, 40.8 real, 124.5 MB
[runlim] sample:		196.6 time, 50.8 real, 133.3 MB
[runlim] sample:		236.2 time, 60.8 real, 141.4 MB
[runlim] sample:		275.9 time, 70.8 real, 144.6 MB
[runlim] sample:		315.5 time, 80.8 real, 155.4 MB
[runlim] sample:		355.1 time, 90.8 real, 172.6 MB
[runlim] sample:		394.8 time, 100.8 real, 177.2 MB
[runlim] sample:		434.4 time, 110.8 real, 195.2 MB
[runlim] sample:		474.0 time, 120.8 real, 196.6 MB
[runlim] sample:		513.6 time, 130.8 real, 204.0 MB
[runlim] sample:		553.3 time, 140.8 real, 204.2 MB
[runlim] sample:		592.9 time, 150.8 real, 203.7 MB
[runlim] sample:		632.5 time, 160.8 real, 207.6 MB
[runlim] sample:		672.2 time, 170.8 real, 214.2 MB
[runlim] sample:		711.8 time, 180.8 real, 232.8 MB
[runlim] sample:		751.4 time, 190.8 real, 227.1 MB
[runlim] sample:		791.0 time, 200.8 real, 224.0 MB
[runlim] sample:		830.7 time, 210.8 real, 220.8 MB
[runlim] sample:		870.3 time, 220.8 real, 234.9 MB
[runlim] sample:		909.9 time, 230.8 real, 246.4 MB
[runlim] sample:		949.5 time, 240.8 real, 240.2 MB
[runlim] sample:		989.1 time, 250.8 real, 242.4 MB
[runlim] sample:		1028.8 time, 260.8 real, 235.1 MB
[runlim] sample:		1068.4 time, 270.8 real, 245.6 MB
[runlim] sample:		1108.0 time, 280.8 real, 260.4 MB
[runlim] sample:		1147.6 time, 290.8 real, 261.9 MB
[runlim] sample:		1187.2 time, 300.8 real, 268.1 MB
[runlim] sample:		1226.8 time, 310.8 real, 270.3 MB
[runlim] sample:		1266.4 time, 320.8 real, 279.1 MB
[runlim] sample:		1306.1 time, 330.8 real, 266.6 MB
[runlim] sample:		1345.7 time, 340.8 real, 274.8 MB
[runlim] sample:		1385.3 time, 350.8 real, 274.8 MB
[runlim] sample:		1424.9 time, 360.8 real, 278.1 MB
[runlim] sample:		1464.5 time, 370.8 real, 292.8 MB
[runlim] sample:		1504.2 time, 380.8 real, 296.9 MB
[runlim] sample:		1543.8 time, 390.8 real, 304.1 MB
[runlim] sample:		1583.4 time, 400.8 real, 307.5 MB
[runlim] sample:		1623.0 time, 410.8 real, 295.6 MB
[runlim] sample:		1662.6 time, 420.8 real, 290.6 MB
[runlim] sample:		1702.2 time, 430.8 real, 302.6 MB
[runlim] sample:		1741.8 time, 440.8 real, 306.7 MB
[runlim] sample:		1781.4 time, 450.8 real, 316.0 MB
[runlim] sample:		1821.0 time, 460.8 real, 322.1 MB
[runlim] sample:		1860.6 time, 470.8 real, 324.8 MB
[runlim] sample:		1900.2 time, 480.8 real, 320.6 MB
[runlim] sample:		1939.8 time, 490.8 real, 318.9 MB
[runlim] sample:		1979.5 time, 500.8 real, 309.3 MB
[runlim] sample:		2019.1 time, 510.8 real, 316.2 MB
[runlim] sample:		2058.7 time, 520.8 real, 313.8 MB
[runlim] sample:		2098.3 time, 530.8 real, 314.1 MB
[runlim] sample:		2137.9 time, 540.8 real, 339.4 MB
[runlim] sample:		2177.5 time, 550.8 real, 329.7 MB
[runlim] sample:		2217.1 time, 560.8 real, 335.9 MB
[runlim] sample:		2256.7 time, 570.8 real, 338.4 MB
[runlim] sample:		2296.3 time, 580.8 real, 349.3 MB
[runlim] sample:		2335.9 time, 590.8 real, 341.4 MB
[runlim] sample:		2375.5 time, 600.8 real, 351.1 MB
[runlim] sample:		2415.2 time, 610.8 real, 348.4 MB
[runlim] sample:		2454.8 time, 620.8 real, 343.4 MB
[runlim] sample:		2494.4 time, 630.8 real, 366.6 MB
[runlim] sample:		2534.0 time, 640.8 real, 365.7 MB
[runlim] sample:		2573.6 time, 650.8 real, 363.2 MB
[runlim] sample:		2613.2 time, 660.8 real, 372.7 MB
[runlim] sample:		2652.8 time, 670.8 real, 377.2 MB
[runlim] sample:		2692.4 time, 680.8 real, 381.6 MB
[runlim] sample:		2732.0 time, 690.8 real, 384.9 MB
[runlim] sample:		2771.6 time, 700.8 real, 392.9 MB
[runlim] sample:		2811.2 time, 710.8 real, 409.2 MB
[runlim] sample:		2850.8 time, 720.8 real, 401.8 MB
[runlim] sample:		2890.4 time, 730.8 real, 404.6 MB
[runlim] sample:		2930.1 time, 740.8 real, 407.4 MB
[runlim] sample:		2969.7 time, 750.8 real, 393.8 MB
[runlim] sample:		3009.3 time, 760.8 real, 390.3 MB
[runlim] sample:		3048.9 time, 770.8 real, 390.3 MB
[runlim] sample:		3088.5 time, 780.8 real, 394.3 MB
[runlim] sample:		3128.1 time, 790.8 real, 381.6 MB
[runlim] sample:		3167.7 time, 800.8 real, 401.1 MB
[runlim] sample:		3207.3 time, 810.8 real, 401.1 MB
[runlim] sample:		3246.9 time, 820.8 real, 407.3 MB
[runlim] sample:		3286.5 time, 830.8 real, 409.3 MB
[runlim] sample:		3326.1 time, 840.8 real, 411.3 MB
[runlim] sample:		3365.7 time, 850.8 real, 397.7 MB
[runlim] sample:		3405.3 time, 860.8 real, 399.1 MB
[runlim] sample:		3444.9 time, 870.8 real, 402.2 MB
[runlim] sample:		3484.5 time, 880.8 real, 391.2 MB
[runlim] sample:		3524.1 time, 890.8 real, 395.1 MB
[runlim] sample:		3563.7 time, 900.8 real, 405.3 MB
[runlim] sample:		3603.3 time, 910.8 real, 408.4 MB
[runlim] sample:		3642.9 time, 920.8 real, 412.4 MB
[runlim] sample:		3682.6 time, 930.8 real, 412.4 MB
[runlim] sample:		3722.2 time, 940.8 real, 420.4 MB
[runlim] sample:		3761.8 time, 950.8 real, 422.7 MB
[runlim] sample:		3801.4 time, 960.8 real, 413.1 MB
[runlim] sample:		3841.0 time, 970.8 real, 403.3 MB
[runlim] sample:		3880.6 time, 980.8 real, 405.1 MB
[runlim] sample:		3920.2 time, 990.8 real, 407.4 MB
[runlim] sample:		3959.8 time, 1000.8 real, 408.1 MB
[runlim] sample:		3999.4 time, 1010.8 real, 412.2 MB
[runlim] sample:		4039.0 time, 1020.8 real, 414.4 MB
[runlim] sample:		4078.6 time, 1030.8 real, 416.4 MB
[runlim] sample:		4118.2 time, 1040.8 real, 416.4 MB
[runlim] sample:		4157.8 time, 1050.8 real, 434.2 MB
[runlim] sample:		4197.4 time, 1060.8 real, 416.9 MB
[runlim] sample:		4237.0 time, 1070.8 real, 416.9 MB
[runlim] sample:		4276.6 time, 1080.8 real, 432.3 MB
[runlim] sample:		4316.2 time, 1090.8 real, 432.3 MB
[runlim] sample:		4355.8 time, 1100.8 real, 435.1 MB
[runlim] sample:		4395.4 time, 1110.8 real, 439.2 MB
[runlim] sample:		4435.0 time, 1120.8 real, 461.7 MB
[runlim] sample:		4474.6 time, 1130.8 real, 433.9 MB
[runlim] sample:		4514.2 time, 1140.8 real, 429.2 MB
[runlim] sample:		4553.8 time, 1150.8 real, 411.7 MB
[runlim] sample:		4593.4 time, 1160.8 real, 411.7 MB
[runlim] sample:		4633.0 time, 1170.8 real, 413.9 MB
[runlim] sample:		4672.6 time, 1180.8 real, 420.2 MB
[runlim] sample:		4712.2 time, 1190.8 real, 420.4 MB
[runlim] sample:		4751.8 time, 1200.8 real, 424.5 MB
[runlim] sample:		4791.4 time, 1210.8 real, 430.8 MB
[runlim] sample:		4831.0 time, 1220.8 real, 448.8 MB
[runlim] sample:		4870.6 time, 1230.8 real, 446.9 MB
[runlim] sample:		4910.2 time, 1240.8 real, 447.2 MB
[runlim] sample:		4949.9 time, 1250.8 real, 449.9 MB
[runlim] sample:		4989.4 time, 1260.8 real, 453.0 MB
[runlim] sample:		5029.0 time, 1270.8 real, 453.5 MB
[runlim] sample:		5068.6 time, 1280.8 real, 437.8 MB
[runlim] sample:		5108.2 time, 1290.8 real, 446.1 MB
[runlim] sample:		5147.9 time, 1300.8 real, 448.1 MB
[runlim] sample:		5187.5 time, 1310.8 real, 448.6 MB
[runlim] sample:		5227.1 time, 1320.8 real, 442.4 MB
[runlim] sample:		5266.7 time, 1330.8 real, 442.4 MB
[runlim] sample:		5306.3 time, 1340.8 real, 445.2 MB
[runlim] sample:		5345.9 time, 1350.8 real, 451.2 MB
[runlim] sample:		5385.5 time, 1360.8 real, 453.5 MB
[runlim] sample:		5425.1 time, 1370.8 real, 477.8 MB
[runlim] sample:		5464.7 time, 1380.8 real, 477.8 MB
[runlim] sample:		5504.3 time, 1390.8 real, 479.9 MB
[runlim] sample:		5543.9 time, 1400.8 real, 479.9 MB
[runlim] sample:		5583.5 time, 1410.8 real, 493.5 MB
[runlim] sample:		5623.1 time, 1420.8 real, 451.0 MB
[runlim] sample:		5662.7 time, 1430.8 real, 453.0 MB
[runlim] sample:		5702.3 time, 1440.8 real, 453.0 MB
[runlim] sample:		5741.9 time, 1450.8 real, 455.2 MB
[runlim] sample:		5781.5 time, 1460.8 real, 455.5 MB
[runlim] sample:		5821.1 time, 1470.8 real, 457.2 MB
[runlim] sample:		5860.7 time, 1480.8 real, 458.2 MB
[runlim] sample:		5900.3 time, 1490.8 real, 463.8 MB
[runlim] sample:		5939.9 time, 1500.8 real, 465.8 MB
[runlim] sample:		5979.5 time, 1510.8 real, 469.6 MB
[runlim] sample:		6019.1 time, 1520.8 real, 474.1 MB
[runlim] sample:		6058.7 time, 1530.8 real, 474.3 MB
[runlim] sample:		6098.3 time, 1540.8 real, 475.4 MB
[runlim] sample:		6137.9 time, 1550.8 real, 495.5 MB
[runlim] sample:		6177.5 time, 1560.8 real, 496.0 MB
[runlim] sample:		6217.1 time, 1570.8 real, 498.5 MB
[runlim] sample:		6256.7 time, 1580.8 real, 481.3 MB
[runlim] sample:		6296.3 time, 1590.8 real, 482.0 MB
[runlim] sample:		6335.9 time, 1600.8 real, 483.1 MB
[runlim] sample:		6375.5 time, 1610.8 real, 483.1 MB
[runlim] sample:		6415.1 time, 1620.8 real, 483.1 MB
[runlim] sample:		6454.7 time, 1630.8 real, 483.1 MB
[runlim] sample:		6494.3 time, 1640.8 real, 499.6 MB
[runlim] sample:		6533.9 time, 1650.8 real, 531.1 MB
[runlim] sample:		6573.5 time, 1660.8 real, 513.3 MB
[runlim] sample:		6613.1 time, 1670.8 real, 513.3 MB
[runlim] sample:		6652.7 time, 1680.8 real, 525.2 MB
[runlim] sample:		6692.3 time, 1690.8 real, 527.7 MB
[runlim] sample:		6731.9 time, 1700.8 real, 529.9 MB
[runlim] sample:		6771.5 time, 1710.8 real, 529.9 MB
[runlim] sample:		6811.1 time, 1720.8 real, 539.4 MB
[runlim] sample:		6850.7 time, 1730.8 real, 540.4 MB
[runlim] sample:		6890.3 time, 1740.8 real, 564.7 MB
[runlim] sample:		6929.9 time, 1750.8 real, 566.7 MB
[runlim] sample:		6969.5 time, 1760.8 real, 541.0 MB
[runlim] sample:		7009.1 time, 1770.8 real, 543.0 MB
[runlim] sample:		7048.7 time, 1780.8 real, 545.0 MB
[runlim] sample:		7088.3 time, 1790.8 real, 500.9 MB
[runlim] sample:		7127.9 time, 1800.8 real, 500.9 MB
[runlim] sample:		7167.5 time, 1810.8 real, 500.9 MB
[runlim] sample:		7207.1 time, 1820.8 real, 515.2 MB
[runlim] sample:		7246.7 time, 1830.8 real, 517.2 MB
[runlim] sample:		7286.3 time, 1840.8 real, 519.2 MB
[runlim] sample:		7325.9 time, 1850.8 real, 519.2 MB
[runlim] sample:		7365.5 time, 1860.8 real, 540.9 MB
[runlim] sample:		7405.1 time, 1870.8 real, 542.9 MB
[runlim] sample:		7444.7 time, 1880.8 real, 563.2 MB
[runlim] sample:		7484.3 time, 1890.8 real, 565.2 MB
[runlim] sample:		7523.9 time, 1900.8 real, 565.2 MB
[runlim] sample:		7563.5 time, 1910.8 real, 569.2 MB
[runlim] sample:		7603.1 time, 1920.8 real, 529.2 MB
[runlim] sample:		7642.7 time, 1930.8 real, 529.4 MB
[runlim] sample:		7682.3 time, 1940.8 real, 529.4 MB
[runlim] sample:		7721.9 time, 1950.8 real, 529.4 MB
[runlim] sample:		7761.5 time, 1960.8 real, 543.7 MB
[runlim] sample:		7801.1 time, 1970.8 real, 545.7 MB
[runlim] sample:		7840.7 time, 1980.8 real, 547.7 MB
[runlim] sample:		7880.3 time, 1990.8 real, 547.7 MB
[runlim] sample:		7919.9 time, 2000.8 real, 549.2 MB
[runlim] sample:		7959.5 time, 2010.8 real, 620.7 MB
[runlim] sample:		7999.1 time, 2020.8 real, 639.0 MB
[runlim] sample:		8038.7 time, 2030.8 real, 643.3 MB
[runlim] sample:		8078.3 time, 2040.8 real, 644.2 MB
[runlim] sample:		8117.9 time, 2050.8 real, 648.5 MB
[runlim] sample:		8157.5 time, 2060.8 real, 648.7 MB
[runlim] sample:		8197.1 time, 2070.8 real, 652.7 MB
[runlim] sample:		8236.7 time, 2080.8 real, 654.7 MB
[runlim] sample:		8276.3 time, 2090.8 real, 654.7 MB
[runlim] sample:		8315.9 time, 2100.8 real, 610.7 MB
[runlim] sample:		8355.5 time, 2110.8 real, 612.7 MB
[runlim] sample:		8395.1 time, 2120.8 real, 614.7 MB
[runlim] sample:		8434.7 time, 2130.8 real, 616.7 MB
[runlim] sample:		8474.3 time, 2140.8 real, 629.0 MB
[runlim] sample:		8513.9 time, 2150.8 real, 595.3 MB
[runlim] sample:		8553.5 time, 2160.8 real, 599.3 MB
[runlim] sample:		8593.1 time, 2170.8 real, 599.3 MB
[runlim] sample:		8632.8 time, 2180.8 real, 601.8 MB
[runlim] sample:		8672.4 time, 2190.8 real, 608.5 MB
[runlim] sample:		8712.0 time, 2200.8 real, 629.0 MB
[runlim] sample:		8751.5 time, 2210.8 real, 631.0 MB
[runlim] sample:		8791.2 time, 2220.8 real, 633.0 MB
[runlim] sample:		8830.8 time, 2230.8 real, 633.0 MB
[runlim] sample:		8870.4 time, 2240.8 real, 635.0 MB
[runlim] sample:		8910.0 time, 2250.8 real, 635.0 MB
[runlim] sample:		8949.6 time, 2260.8 real, 635.0 MB
[runlim] sample:		8989.2 time, 2270.8 real, 637.0 MB
[runlim] sample:		9028.8 time, 2280.8 real, 593.1 MB
[runlim] sample:		9068.4 time, 2290.8 real, 625.3 MB
[runlim] sample:		9108.0 time, 2300.8 real, 627.3 MB
[runlim] sample:		9147.6 time, 2310.8 real, 643.3 MB
[runlim] sample:		9187.2 time, 2320.8 real, 645.3 MB
[runlim] sample:		9226.8 time, 2330.8 real, 625.2 MB
[runlim] sample:		9266.4 time, 2340.8 real, 618.3 MB
[runlim] sample:		9306.0 time, 2350.8 real, 618.3 MB
[runlim] sample:		9345.6 time, 2360.8 real, 631.4 MB
[runlim] sample:		9385.2 time, 2370.8 real, 633.4 MB
[runlim] sample:		9424.8 time, 2380.8 real, 635.4 MB
[runlim] sample:		9464.4 time, 2390.8 real, 636.4 MB
[runlim] sample:		9504.0 time, 2400.8 real, 657.2 MB
[runlim] sample:		9543.6 time, 2410.8 real, 621.1 MB
[runlim] sample:		9583.2 time, 2420.8 real, 621.1 MB
[runlim] sample:		9622.8 time, 2430.8 real, 632.7 MB
[runlim] sample:		9662.4 time, 2440.8 real, 607.4 MB
[runlim] sample:		9702.0 time, 2450.8 real, 609.4 MB
[runlim] sample:		9741.6 time, 2460.8 real, 610.7 MB
[runlim] sample:		9781.2 time, 2470.8 real, 631.2 MB
[runlim] sample:		9820.8 time, 2480.8 real, 633.2 MB
[runlim] sample:		9860.4 time, 2490.8 real, 593.1 MB
[runlim] sample:		9900.0 time, 2500.8 real, 593.1 MB
[runlim] sample:		9939.6 time, 2510.8 real, 593.1 MB
[runlim] sample:		9979.2 time, 2520.8 real, 604.6 MB
[runlim] sample:		10018.8 time, 2530.8 real, 607.3 MB
[runlim] sample:		10058.4 time, 2540.8 real, 609.3 MB
[runlim] sample:		10098.0 time, 2550.8 real, 609.6 MB
[runlim] sample:		10137.6 time, 2560.8 real, 613.1 MB
[runlim] sample:		10177.2 time, 2570.8 real, 633.1 MB
[runlim] sample:		10216.8 time, 2580.8 real, 635.1 MB
[runlim] sample:		10256.4 time, 2590.8 real, 637.1 MB
[runlim] sample:		10296.0 time, 2600.8 real, 595.1 MB
[runlim] sample:		10335.6 time, 2610.8 real, 619.1 MB
[runlim] sample:		10375.2 time, 2620.8 real, 619.1 MB
[runlim] sample:		10414.9 time, 2630.8 real, 631.1 MB
[runlim] sample:		10454.5 time, 2640.8 real, 633.3 MB
[runlim] sample:		10494.0 time, 2650.8 real, 635.3 MB
[runlim] sample:		10533.6 time, 2660.8 real, 635.3 MB
[runlim] sample:		10573.2 time, 2670.8 real, 637.8 MB
[runlim] sample:		10612.9 time, 2680.8 real, 639.1 MB
[runlim] sample:		10652.5 time, 2690.8 real, 659.1 MB
[runlim] sample:		10692.1 time, 2700.8 real, 661.1 MB
[runlim] sample:		10731.6 time, 2710.8 real, 661.1 MB
[runlim] sample:		10771.2 time, 2720.8 real, 665.1 MB
[runlim] sample:		10810.9 time, 2730.8 real, 665.1 MB
[runlim] sample:		10850.5 time, 2740.8 real, 667.1 MB
[runlim] sample:		10890.0 time, 2750.8 real, 623.1 MB
[runlim] sample:		10929.6 time, 2760.8 real, 623.1 MB
[runlim] sample:		10969.2 time, 2770.8 real, 623.1 MB
[runlim] sample:		11008.9 time, 2780.8 real, 637.5 MB
[runlim] sample:		11048.5 time, 2790.8 real, 640.0 MB
[runlim] sample:		11088.0 time, 2800.8 real, 664.3 MB
[runlim] sample:		11127.7 time, 2810.8 real, 665.8 MB
[runlim] sample:		11167.3 time, 2820.8 real, 688.0 MB
[runlim] sample:		11206.9 time, 2830.8 real, 692.0 MB
[runlim] sample:		11246.5 time, 2840.8 real, 694.0 MB
[runlim] sample:		11286.0 time, 2850.8 real, 694.0 MB
[runlim] sample:		11325.7 time, 2860.8 real, 696.0 MB
[runlim] sample:		11365.2 time, 2870.8 real, 650.0 MB
[runlim] sample:		11404.9 time, 2880.8 real, 652.0 MB
[runlim] sample:		11444.5 time, 2890.8 real, 652.0 MB
[runlim] sample:		11484.1 time, 2900.8 real, 664.3 MB
[runlim] sample:		11523.6 time, 2910.8 real, 666.3 MB
[runlim] sample:		11563.3 time, 2920.8 real, 668.3 MB
[runlim] sample:		11602.9 time, 2930.8 real, 669.8 MB
[runlim] sample:		11642.5 time, 2940.8 real, 690.8 MB
[runlim] sample:		11682.1 time, 2950.8 real, 693.0 MB
[runlim] sample:		11721.7 time, 2960.8 real, 667.1 MB
[runlim] sample:		11761.2 time, 2970.8 real, 661.1 MB
[runlim] sample:		11800.9 time, 2980.8 real, 665.1 MB
[runlim] sample:		11840.5 time, 2990.8 real, 665.1 MB
[runlim] sample:		11880.0 time, 3000.8 real, 667.1 MB
[runlim] sample:		11919.6 time, 3010.8 real, 667.1 MB
[runlim] sample:		11959.2 time, 3020.8 real, 621.0 MB
[runlim] sample:		11998.9 time, 3030.8 real, 621.0 MB
[runlim] sample:		12038.4 time, 3040.8 real, 623.0 MB
[runlim] sample:		12078.0 time, 3050.8 real, 637.3 MB
[runlim] sample:		12117.6 time, 3060.8 real, 639.3 MB
[runlim] sample:		12157.2 time, 3070.8 real, 639.3 MB
[runlim] sample:		12196.9 time, 3080.8 real, 639.5 MB
[runlim] sample:		12236.4 time, 3090.8 real, 661.0 MB
[runlim] sample:		12276.0 time, 3100.8 real, 661.2 MB
[runlim] sample:		12315.6 time, 3110.8 real, 663.5 MB
[runlim] sample:		12355.2 time, 3120.8 real, 664.0 MB
[runlim] sample:		12394.9 time, 3130.8 real, 666.2 MB
[runlim] sample:		12434.4 time, 3140.8 real, 666.5 MB
[runlim] sample:		12474.0 time, 3150.8 real, 669.0 MB
[runlim] sample:		12513.6 time, 3160.8 real, 749.1 MB
[runlim] sample:		12553.2 time, 3170.8 real, 805.0 MB
[runlim] sample:		12592.8 time, 3180.8 real, 761.5 MB
[runlim] sample:		12632.4 time, 3190.8 real, 764.0 MB
[runlim] sample:		12672.0 time, 3200.8 real, 784.2 MB
[runlim] sample:		12711.6 time, 3210.8 real, 791.1 MB
[runlim] sample:		12751.2 time, 3220.8 real, 924.5 MB
[runlim] sample:		12790.8 time, 3230.8 real, 1042.2 MB
[runlim] sample:		12830.4 time, 3240.8 real, 1166.1 MB
[runlim] sample:		12869.9 time, 3250.8 real, 1187.2 MB
[runlim] sample:		12909.5 time, 3260.8 real, 1241.3 MB
[runlim] sample:		12949.1 time, 3270.8 real, 1251.1 MB
[runlim] sample:		12988.7 time, 3280.8 real, 1323.9 MB
[runlim] sample:		13028.3 time, 3290.8 real, 1349.0 MB
[runlim] sample:		13067.9 time, 3300.8 real, 1398.6 MB
[runlim] sample:		13107.5 time, 3310.8 real, 1449.8 MB
[runlim] sample:		13147.0 time, 3320.8 real, 1488.5 MB
[runlim] sample:		13186.6 time, 3330.8 real, 1489.1 MB
[runlim] sample:		13226.2 time, 3340.8 real, 1491.1 MB
[runlim] sample:		13265.8 time, 3350.8 real, 1545.4 MB
[runlim] sample:		13305.4 time, 3360.8 real, 1573.2 MB
[runlim] sample:		13345.0 time, 3370.8 real, 1573.7 MB
[runlim] sample:		13384.5 time, 3380.8 real, 1588.4 MB
[runlim] sample:		13424.1 time, 3390.8 real, 1592.5 MB
[runlim] sample:		13463.7 time, 3400.8 real, 1595.0 MB
[runlim] sample:		13503.3 time, 3410.8 real, 1598.6 MB
[runlim] sample:		13542.9 time, 3420.8 real, 1606.5 MB
[runlim] sample:		13582.5 time, 3430.8 real, 1610.5 MB
[runlim] sample:		13622.0 time, 3440.8 real, 1623.1 MB
[runlim] sample:		13661.6 time, 3450.8 real, 1625.4 MB
[runlim] sample:		13701.2 time, 3460.8 real, 1629.9 MB
[runlim] sample:		13740.8 time, 3470.8 real, 1631.9 MB
[runlim] sample:		13780.3 time, 3480.8 real, 1633.9 MB
[runlim] sample:		13819.9 time, 3490.8 real, 1633.9 MB
[runlim] sample:		13859.5 time, 3500.8 real, 1633.9 MB
[runlim] sample:		13899.1 time, 3510.8 real, 1603.3 MB
[runlim] sample:		13938.7 time, 3520.8 real, 1605.3 MB
[runlim] sample:		13978.2 time, 3530.8 real, 1620.0 MB
[runlim] sample:		14017.8 time, 3540.8 real, 1614.0 MB
[runlim] sample:		14057.4 time, 3550.8 real, 1618.0 MB
[runlim] sample:		14097.0 time, 3560.8 real, 1618.0 MB
[runlim] sample:		14136.5 time, 3570.8 real, 1621.2 MB
[runlim] sample:		14176.1 time, 3580.8 real, 1623.7 MB
[runlim] sample:		14215.7 time, 3590.8 real, 1623.7 MB
[runlim] end:			Tue Sep 15 19:00:30 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.07 seconds
[runlim] time:			14252.12 seconds
[runlim] space:			1646.0 MB
[runlim] samples:		35992
