[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/6s35.aig
[runlim] start:			Wed Sep 16 07:02:06 2015
[runlim] main pid:		2220
[runlim] sample:		26.1 time, 10.5 real, 187.7 MB
[runlim] sample:		65.8 time, 20.5 real, 190.3 MB
[runlim] sample:		105.5 time, 30.5 real, 208.8 MB
[runlim] sample:		145.1 time, 40.5 real, 212.9 MB
[runlim] sample:		184.8 time, 50.5 real, 224.3 MB
[runlim] sample:		224.4 time, 60.5 real, 219.0 MB
[runlim] sample:		264.0 time, 70.5 real, 229.6 MB
[runlim] sample:		303.6 time, 80.5 real, 253.5 MB
[runlim] sample:		343.3 time, 90.5 real, 242.3 MB
[runlim] sample:		382.9 time, 100.5 real, 237.2 MB
[runlim] sample:		422.6 time, 110.5 real, 294.9 MB
[runlim] sample:		462.2 time, 120.5 real, 281.3 MB
[runlim] sample:		501.8 time, 130.5 real, 255.0 MB
[runlim] sample:		541.4 time, 140.5 real, 272.3 MB
[runlim] sample:		581.0 time, 150.5 real, 303.6 MB
[runlim] sample:		620.7 time, 160.5 real, 281.3 MB
[runlim] sample:		660.3 time, 170.5 real, 285.6 MB
[runlim] sample:		699.9 time, 180.5 real, 269.0 MB
[runlim] sample:		739.5 time, 190.5 real, 273.9 MB
[runlim] sample:		779.1 time, 200.5 real, 303.5 MB
[runlim] sample:		818.8 time, 210.5 real, 315.4 MB
[runlim] sample:		858.4 time, 220.5 real, 295.8 MB
[runlim] sample:		898.0 time, 230.5 real, 312.7 MB
[runlim] sample:		937.7 time, 240.5 real, 332.3 MB
[runlim] sample:		977.3 time, 250.5 real, 302.3 MB
[runlim] sample:		1016.9 time, 260.5 real, 303.9 MB
[runlim] sample:		1056.5 time, 270.5 real, 296.1 MB
[runlim] sample:		1096.2 time, 280.5 real, 312.3 MB
[runlim] sample:		1135.8 time, 290.5 real, 333.6 MB
[runlim] sample:		1175.4 time, 300.5 real, 301.4 MB
[runlim] sample:		1215.0 time, 310.5 real, 308.2 MB
[runlim] sample:		1254.7 time, 320.5 real, 311.3 MB
[runlim] sample:		1294.3 time, 330.5 real, 311.0 MB
[runlim] sample:		1333.9 time, 340.5 real, 314.4 MB
[runlim] sample:		1373.6 time, 350.5 real, 324.2 MB
[runlim] sample:		1413.2 time, 360.5 real, 329.7 MB
[runlim] sample:		1452.8 time, 370.5 real, 335.2 MB
[runlim] sample:		1492.5 time, 380.5 real, 315.7 MB
[runlim] sample:		1532.1 time, 390.5 real, 330.5 MB
[runlim] sample:		1571.7 time, 400.5 real, 317.5 MB
[runlim] sample:		1611.4 time, 410.5 real, 320.3 MB
[runlim] sample:		1651.0 time, 420.5 real, 324.5 MB
[runlim] sample:		1690.6 time, 430.5 real, 333.6 MB
[runlim] sample:		1730.3 time, 440.5 real, 331.1 MB
[runlim] sample:		1769.9 time, 450.5 real, 333.6 MB
[runlim] sample:		1809.5 time, 460.5 real, 321.1 MB
[runlim] sample:		1849.2 time, 470.5 real, 357.3 MB
[runlim] sample:		1888.8 time, 480.5 real, 341.8 MB
[runlim] sample:		1928.4 time, 490.5 real, 326.6 MB
[runlim] sample:		1968.0 time, 500.5 real, 331.2 MB
[runlim] sample:		2007.7 time, 510.5 real, 342.7 MB
[runlim] sample:		2047.3 time, 520.5 real, 385.3 MB
[runlim] sample:		2086.9 time, 530.5 real, 375.2 MB
[runlim] sample:		2126.6 time, 540.5 real, 377.7 MB
[runlim] sample:		2166.2 time, 550.5 real, 378.3 MB
[runlim] sample:		2205.8 time, 560.5 real, 399.1 MB
[runlim] sample:		2245.4 time, 570.5 real, 387.6 MB
[runlim] sample:		2285.1 time, 580.5 real, 340.8 MB
[runlim] sample:		2324.7 time, 590.5 real, 337.2 MB
[runlim] sample:		2364.3 time, 600.5 real, 369.4 MB
[runlim] sample:		2403.9 time, 610.5 real, 358.3 MB
[runlim] sample:		2443.6 time, 620.5 real, 363.7 MB
[runlim] sample:		2483.2 time, 630.5 real, 363.8 MB
[runlim] sample:		2522.8 time, 640.5 real, 415.2 MB
[runlim] sample:		2562.4 time, 650.5 real, 382.6 MB
[runlim] sample:		2602.1 time, 660.5 real, 424.3 MB
[runlim] sample:		2641.7 time, 670.5 real, 394.6 MB
[runlim] sample:		2681.3 time, 680.5 real, 401.3 MB
[runlim] sample:		2720.9 time, 690.5 real, 400.7 MB
[runlim] sample:		2760.6 time, 700.5 real, 402.3 MB
[runlim] sample:		2800.2 time, 710.5 real, 407.5 MB
[runlim] sample:		2839.8 time, 720.5 real, 414.6 MB
[runlim] sample:		2879.4 time, 730.5 real, 420.5 MB
[runlim] sample:		2919.1 time, 740.5 real, 420.5 MB
[runlim] sample:		2958.7 time, 750.5 real, 423.4 MB
[runlim] sample:		2998.3 time, 760.5 real, 428.0 MB
[runlim] sample:		3037.9 time, 770.5 real, 429.0 MB
[runlim] sample:		3077.6 time, 780.5 real, 440.5 MB
[runlim] sample:		3117.2 time, 790.5 real, 452.1 MB
[runlim] sample:		3156.8 time, 800.5 real, 458.5 MB
[runlim] sample:		3196.4 time, 810.5 real, 458.8 MB
[runlim] sample:		3236.0 time, 820.5 real, 460.6 MB
[runlim] sample:		3275.7 time, 830.5 real, 478.2 MB
[runlim] sample:		3315.3 time, 840.5 real, 487.4 MB
[runlim] sample:		3354.9 time, 850.5 real, 489.7 MB
[runlim] sample:		3394.5 time, 860.5 real, 468.0 MB
[runlim] sample:		3434.1 time, 870.5 real, 468.3 MB
[runlim] sample:		3473.7 time, 880.5 real, 476.1 MB
[runlim] sample:		3513.4 time, 890.5 real, 476.6 MB
[runlim] sample:		3553.0 time, 900.5 real, 498.6 MB
[runlim] sample:		3592.6 time, 910.5 real, 501.2 MB
[runlim] sample:		3632.2 time, 920.5 real, 501.3 MB
[runlim] sample:		3671.8 time, 930.5 real, 485.8 MB
[runlim] sample:		3711.4 time, 940.5 real, 499.5 MB
[runlim] sample:		3751.1 time, 950.5 real, 500.6 MB
[runlim] sample:		3790.7 time, 960.5 real, 508.5 MB
[runlim] sample:		3830.3 time, 970.5 real, 510.8 MB
[runlim] sample:		3869.9 time, 980.5 real, 512.9 MB
[runlim] sample:		3909.5 time, 990.5 real, 518.2 MB
[runlim] sample:		3949.1 time, 1000.5 real, 521.7 MB
[runlim] sample:		3988.7 time, 1010.5 real, 518.3 MB
[runlim] sample:		4028.4 time, 1020.5 real, 524.6 MB
[runlim] sample:		4068.0 time, 1030.5 real, 524.8 MB
[runlim] sample:		4107.6 time, 1040.5 real, 486.9 MB
[runlim] sample:		4147.2 time, 1050.5 real, 490.3 MB
[runlim] sample:		4186.8 time, 1060.5 real, 493.1 MB
[runlim] sample:		4226.5 time, 1070.5 real, 491.0 MB
[runlim] sample:		4266.1 time, 1080.5 real, 497.1 MB
[runlim] sample:		4305.7 time, 1090.5 real, 479.1 MB
[runlim] sample:		4345.3 time, 1100.5 real, 481.8 MB
[runlim] sample:		4384.9 time, 1110.5 real, 481.5 MB
[runlim] sample:		4424.5 time, 1120.5 real, 478.0 MB
[runlim] sample:		4464.2 time, 1130.5 real, 481.5 MB
[runlim] sample:		4503.8 time, 1140.5 real, 480.0 MB
[runlim] sample:		4543.4 time, 1150.5 real, 480.0 MB
[runlim] sample:		4583.0 time, 1160.5 real, 482.0 MB
[runlim] sample:		4622.6 time, 1170.5 real, 482.0 MB
[runlim] sample:		4662.2 time, 1180.5 real, 512.0 MB
[runlim] sample:		4701.8 time, 1190.5 real, 505.3 MB
[runlim] sample:		4741.4 time, 1200.5 real, 511.1 MB
[runlim] sample:		4781.1 time, 1210.5 real, 535.8 MB
[runlim] sample:		4820.7 time, 1220.5 real, 532.0 MB
[runlim] sample:		4860.3 time, 1230.5 real, 512.9 MB
[runlim] sample:		4899.9 time, 1240.5 real, 513.4 MB
[runlim] sample:		4939.5 time, 1250.5 real, 533.4 MB
[runlim] sample:		4979.1 time, 1260.5 real, 536.2 MB
[runlim] sample:		5018.8 time, 1270.5 real, 514.2 MB
[runlim] sample:		5058.4 time, 1280.5 real, 536.7 MB
[runlim] sample:		5098.0 time, 1290.5 real, 538.9 MB
[runlim] sample:		5137.6 time, 1300.5 real, 540.9 MB
[runlim] sample:		5177.2 time, 1310.5 real, 520.5 MB
[runlim] sample:		5216.8 time, 1320.5 real, 520.7 MB
[runlim] sample:		5256.4 time, 1330.5 real, 526.5 MB
[runlim] sample:		5296.1 time, 1340.5 real, 522.5 MB
[runlim] sample:		5335.7 time, 1350.5 real, 531.7 MB
[runlim] sample:		5375.3 time, 1360.5 real, 530.5 MB
[runlim] sample:		5414.9 time, 1370.5 real, 522.9 MB
[runlim] sample:		5454.5 time, 1380.5 real, 523.2 MB
[runlim] sample:		5494.1 time, 1390.5 real, 531.5 MB
[runlim] sample:		5533.7 time, 1400.5 real, 540.4 MB
[runlim] sample:		5573.4 time, 1410.5 real, 542.7 MB
[runlim] sample:		5613.0 time, 1420.5 real, 528.4 MB
[runlim] sample:		5652.6 time, 1430.5 real, 530.4 MB
[runlim] sample:		5692.2 time, 1440.5 real, 530.5 MB
[runlim] sample:		5731.8 time, 1450.5 real, 550.8 MB
[runlim] sample:		5771.4 time, 1460.5 real, 546.5 MB
[runlim] sample:		5811.0 time, 1470.5 real, 571.1 MB
[runlim] sample:		5850.6 time, 1480.5 real, 570.1 MB
[runlim] sample:		5890.3 time, 1490.5 real, 557.9 MB
[runlim] sample:		5929.9 time, 1500.5 real, 557.1 MB
[runlim] sample:		5969.5 time, 1510.5 real, 557.4 MB
[runlim] sample:		6009.1 time, 1520.5 real, 590.3 MB
[runlim] sample:		6048.7 time, 1530.5 real, 584.4 MB
[runlim] sample:		6088.3 time, 1540.5 real, 584.4 MB
[runlim] sample:		6127.9 time, 1550.5 real, 584.6 MB
[runlim] sample:		6167.5 time, 1560.5 real, 585.1 MB
[runlim] sample:		6207.1 time, 1570.5 real, 591.4 MB
[runlim] sample:		6246.8 time, 1580.5 real, 587.1 MB
[runlim] sample:		6286.4 time, 1590.5 real, 587.1 MB
[runlim] sample:		6326.0 time, 1600.5 real, 589.1 MB
[runlim] sample:		6365.6 time, 1610.5 real, 589.1 MB
[runlim] sample:		6405.2 time, 1620.5 real, 589.1 MB
[runlim] sample:		6444.8 time, 1630.5 real, 589.1 MB
[runlim] sample:		6484.4 time, 1640.5 real, 589.1 MB
[runlim] sample:		6524.0 time, 1650.5 real, 591.4 MB
[runlim] sample:		6563.6 time, 1660.5 real, 591.4 MB
[runlim] sample:		6603.2 time, 1670.5 real, 591.4 MB
[runlim] sample:		6642.9 time, 1680.5 real, 591.4 MB
[runlim] sample:		6682.5 time, 1690.5 real, 592.9 MB
[runlim] sample:		6722.1 time, 1700.5 real, 605.6 MB
[runlim] sample:		6761.7 time, 1710.5 real, 583.8 MB
[runlim] sample:		6801.3 time, 1720.5 real, 583.8 MB
[runlim] sample:		6840.9 time, 1730.5 real, 583.8 MB
[runlim] sample:		6880.6 time, 1740.5 real, 585.7 MB
[runlim] sample:		6920.2 time, 1750.5 real, 584.5 MB
[runlim] sample:		6959.8 time, 1760.5 real, 588.4 MB
[runlim] sample:		6999.4 time, 1770.5 real, 591.8 MB
[runlim] sample:		7039.0 time, 1780.5 real, 593.8 MB
[runlim] sample:		7078.6 time, 1790.5 real, 593.8 MB
[runlim] sample:		7118.2 time, 1800.5 real, 595.8 MB
[runlim] sample:		7157.8 time, 1810.5 real, 595.8 MB
[runlim] sample:		7197.4 time, 1820.5 real, 606.3 MB
[runlim] sample:		7237.1 time, 1830.5 real, 594.7 MB
[runlim] sample:		7276.7 time, 1840.5 real, 597.5 MB
[runlim] sample:		7316.3 time, 1850.5 real, 597.8 MB
[runlim] sample:		7355.9 time, 1860.5 real, 598.5 MB
[runlim] sample:		7395.5 time, 1870.5 real, 602.9 MB
[runlim] sample:		7435.1 time, 1880.5 real, 602.9 MB
[runlim] sample:		7474.7 time, 1890.5 real, 604.9 MB
[runlim] sample:		7514.3 time, 1900.5 real, 606.9 MB
[runlim] sample:		7553.9 time, 1910.5 real, 607.1 MB
[runlim] sample:		7593.5 time, 1920.5 real, 609.1 MB
[runlim] sample:		7633.1 time, 1930.5 real, 626.6 MB
[runlim] sample:		7672.7 time, 1940.5 real, 647.4 MB
[runlim] sample:		7712.4 time, 1950.5 real, 649.4 MB
[runlim] sample:		7752.0 time, 1960.5 real, 601.5 MB
[runlim] sample:		7791.6 time, 1970.5 real, 621.1 MB
[runlim] sample:		7831.2 time, 1980.5 real, 622.1 MB
[runlim] sample:		7870.8 time, 1990.5 real, 623.1 MB
[runlim] sample:		7910.4 time, 2000.5 real, 625.3 MB
[runlim] sample:		7950.0 time, 2010.5 real, 627.3 MB
[runlim] sample:		7989.6 time, 2020.5 real, 627.5 MB
[runlim] sample:		8029.2 time, 2030.5 real, 636.8 MB
[runlim] sample:		8068.8 time, 2040.5 real, 651.2 MB
[runlim] sample:		8108.4 time, 2050.5 real, 663.5 MB
[runlim] sample:		8148.1 time, 2060.5 real, 657.2 MB
[runlim] sample:		8187.6 time, 2070.5 real, 657.2 MB
[runlim] sample:		8227.3 time, 2080.5 real, 659.2 MB
[runlim] sample:		8266.9 time, 2090.5 real, 667.7 MB
[runlim] sample:		8306.5 time, 2100.5 real, 660.4 MB
[runlim] sample:		8346.1 time, 2110.5 real, 639.7 MB
[runlim] sample:		8385.7 time, 2120.5 real, 640.0 MB
[runlim] sample:		8425.3 time, 2130.5 real, 632.0 MB
[runlim] sample:		8464.9 time, 2140.5 real, 632.5 MB
[runlim] sample:		8504.5 time, 2150.5 real, 634.1 MB
[runlim] sample:		8544.1 time, 2160.5 real, 646.3 MB
[runlim] sample:		8583.7 time, 2170.5 real, 638.3 MB
[runlim] sample:		8623.4 time, 2180.5 real, 648.7 MB
[runlim] sample:		8663.0 time, 2190.5 real, 640.3 MB
[runlim] sample:		8702.6 time, 2200.5 real, 646.4 MB
[runlim] sample:		8742.2 time, 2210.5 real, 648.5 MB
[runlim] sample:		8781.8 time, 2220.5 real, 637.0 MB
[runlim] sample:		8821.4 time, 2230.5 real, 647.3 MB
[runlim] sample:		8861.0 time, 2240.5 real, 662.4 MB
[runlim] sample:		8900.6 time, 2250.5 real, 658.4 MB
[runlim] sample:		8940.2 time, 2260.5 real, 663.9 MB
[runlim] sample:		8979.8 time, 2270.5 real, 660.7 MB
[runlim] sample:		9019.5 time, 2280.5 real, 662.9 MB
[runlim] sample:		9059.0 time, 2290.5 real, 662.9 MB
[runlim] sample:		9098.7 time, 2300.5 real, 658.6 MB
[runlim] sample:		9138.3 time, 2310.5 real, 658.6 MB
[runlim] sample:		9177.9 time, 2320.5 real, 658.6 MB
[runlim] sample:		9217.5 time, 2330.5 real, 660.6 MB
[runlim] sample:		9257.1 time, 2340.5 real, 660.6 MB
[runlim] sample:		9296.7 time, 2350.5 real, 667.9 MB
[runlim] sample:		9336.3 time, 2360.5 real, 663.4 MB
[runlim] sample:		9375.9 time, 2370.5 real, 663.4 MB
[runlim] sample:		9415.5 time, 2380.5 real, 664.4 MB
[runlim] sample:		9455.1 time, 2390.5 real, 668.6 MB
[runlim] sample:		9494.7 time, 2400.5 real, 636.9 MB
[runlim] sample:		9534.4 time, 2410.5 real, 637.0 MB
[runlim] sample:		9574.0 time, 2420.5 real, 655.5 MB
[runlim] sample:		9613.6 time, 2430.5 real, 657.7 MB
[runlim] sample:		9653.2 time, 2440.5 real, 651.7 MB
[runlim] sample:		9692.8 time, 2450.5 real, 651.7 MB
[runlim] sample:		9732.4 time, 2460.5 real, 647.4 MB
[runlim] sample:		9772.0 time, 2470.5 real, 647.4 MB
[runlim] sample:		9811.6 time, 2480.5 real, 645.1 MB
[runlim] sample:		9851.2 time, 2490.5 real, 661.5 MB
[runlim] sample:		9890.8 time, 2500.5 real, 666.2 MB
[runlim] sample:		9930.5 time, 2510.5 real, 670.2 MB
[runlim] sample:		9970.0 time, 2520.5 real, 670.5 MB
[runlim] sample:		10009.6 time, 2530.5 real, 700.5 MB
[runlim] sample:		10049.3 time, 2540.5 real, 701.0 MB
[runlim] sample:		10088.9 time, 2550.5 real, 698.2 MB
[runlim] sample:		10128.5 time, 2560.5 real, 698.2 MB
[runlim] sample:		10168.1 time, 2570.5 real, 706.6 MB
[runlim] sample:		10207.7 time, 2580.5 real, 708.1 MB
[runlim] sample:		10247.3 time, 2590.5 real, 715.2 MB
[runlim] sample:		10286.9 time, 2600.5 real, 726.9 MB
[runlim] sample:		10326.5 time, 2610.5 real, 724.4 MB
[runlim] sample:		10366.1 time, 2620.5 real, 737.9 MB
[runlim] sample:		10405.7 time, 2630.5 real, 741.2 MB
[runlim] sample:		10445.3 time, 2640.5 real, 752.5 MB
[runlim] sample:		10485.0 time, 2650.5 real, 752.8 MB
[runlim] sample:		10524.6 time, 2660.5 real, 755.0 MB
[runlim] sample:		10564.2 time, 2670.5 real, 755.0 MB
[runlim] sample:		10603.8 time, 2680.5 real, 757.0 MB
[runlim] sample:		10643.4 time, 2690.5 real, 757.0 MB
[runlim] sample:		10683.0 time, 2700.5 real, 757.3 MB
[runlim] sample:		10722.6 time, 2710.5 real, 759.3 MB
[runlim] sample:		10762.2 time, 2720.5 real, 761.1 MB
[runlim] sample:		10801.9 time, 2730.5 real, 761.4 MB
[runlim] sample:		10841.5 time, 2740.5 real, 762.1 MB
[runlim] sample:		10881.1 time, 2750.5 real, 765.3 MB
[runlim] sample:		10920.7 time, 2760.5 real, 767.6 MB
[runlim] sample:		10960.3 time, 2770.5 real, 774.6 MB
[runlim] sample:		10999.9 time, 2780.5 real, 769.8 MB
[runlim] sample:		11039.5 time, 2790.5 real, 772.5 MB
[runlim] sample:		11079.1 time, 2800.5 real, 782.0 MB
[runlim] sample:		11118.8 time, 2810.5 real, 775.2 MB
[runlim] sample:		11158.4 time, 2820.5 real, 776.2 MB
[runlim] sample:		11198.0 time, 2830.5 real, 784.9 MB
[runlim] sample:		11237.6 time, 2840.5 real, 786.9 MB
[runlim] sample:		11277.2 time, 2850.5 real, 778.2 MB
[runlim] sample:		11316.8 time, 2860.5 real, 778.5 MB
[runlim] sample:		11356.5 time, 2870.5 real, 741.3 MB
[runlim] sample:		11396.0 time, 2880.5 real, 743.7 MB
[runlim] sample:		11435.7 time, 2890.5 real, 744.4 MB
[runlim] sample:		11475.3 time, 2900.5 real, 705.0 MB
[runlim] sample:		11514.9 time, 2910.5 real, 706.7 MB
[runlim] sample:		11554.5 time, 2920.5 real, 688.8 MB
[runlim] sample:		11594.1 time, 2930.5 real, 688.8 MB
[runlim] sample:		11633.8 time, 2940.5 real, 690.7 MB
[runlim] sample:		11673.4 time, 2950.5 real, 690.7 MB
[runlim] sample:		11713.0 time, 2960.5 real, 691.0 MB
[runlim] sample:		11752.6 time, 2970.5 real, 691.0 MB
[runlim] sample:		11792.2 time, 2980.5 real, 691.0 MB
[runlim] sample:		11831.8 time, 2990.5 real, 691.2 MB
[runlim] sample:		11871.4 time, 3000.5 real, 691.2 MB
[runlim] sample:		11911.0 time, 3010.5 real, 721.2 MB
[runlim] sample:		11950.7 time, 3020.5 real, 723.2 MB
[runlim] sample:		11990.3 time, 3030.5 real, 725.0 MB
[runlim] sample:		12029.9 time, 3040.5 real, 725.2 MB
[runlim] sample:		12069.5 time, 3050.5 real, 727.2 MB
[runlim] sample:		12109.1 time, 3060.5 real, 727.5 MB
[runlim] sample:		12148.7 time, 3070.5 real, 713.4 MB
[runlim] sample:		12188.3 time, 3080.5 real, 713.4 MB
[runlim] sample:		12227.9 time, 3090.5 real, 714.2 MB
[runlim] sample:		12267.5 time, 3100.5 real, 714.2 MB
[runlim] sample:		12307.1 time, 3110.5 real, 714.2 MB
[runlim] sample:		12346.8 time, 3120.5 real, 714.5 MB
[runlim] sample:		12386.4 time, 3130.5 real, 714.5 MB
[runlim] sample:		12426.0 time, 3140.5 real, 714.5 MB
[runlim] sample:		12465.6 time, 3150.5 real, 714.8 MB
[runlim] sample:		12505.2 time, 3160.5 real, 714.8 MB
[runlim] sample:		12544.8 time, 3170.5 real, 714.8 MB
[runlim] sample:		12584.4 time, 3180.5 real, 714.8 MB
[runlim] sample:		12624.0 time, 3190.5 real, 747.0 MB
[runlim] sample:		12663.6 time, 3200.5 real, 749.0 MB
[runlim] sample:		12703.2 time, 3210.5 real, 749.0 MB
[runlim] sample:		12742.9 time, 3220.5 real, 749.0 MB
[runlim] sample:		12782.5 time, 3230.5 real, 751.0 MB
[runlim] sample:		12822.1 time, 3240.5 real, 751.3 MB
[runlim] sample:		12861.7 time, 3250.5 real, 753.3 MB
[runlim] sample:		12901.3 time, 3260.5 real, 755.5 MB
[runlim] sample:		12940.9 time, 3270.5 real, 755.5 MB
[runlim] sample:		12980.5 time, 3280.5 real, 755.8 MB
[runlim] sample:		13020.1 time, 3290.5 real, 757.8 MB
[runlim] sample:		13059.7 time, 3300.5 real, 759.8 MB
[runlim] sample:		13099.3 time, 3310.5 real, 759.8 MB
[runlim] sample:		13139.0 time, 3320.5 real, 762.0 MB
[runlim] sample:		13178.6 time, 3330.5 real, 762.0 MB
[runlim] sample:		13218.2 time, 3340.5 real, 766.1 MB
[runlim] sample:		13257.8 time, 3350.5 real, 766.1 MB
[runlim] sample:		13297.4 time, 3360.5 real, 768.3 MB
[runlim] sample:		13337.0 time, 3370.5 real, 772.3 MB
[runlim] sample:		13376.6 time, 3380.5 real, 774.3 MB
[runlim] sample:		13416.2 time, 3390.5 real, 776.3 MB
[runlim] sample:		13455.8 time, 3400.5 real, 776.6 MB
[runlim] sample:		13495.5 time, 3410.5 real, 786.6 MB
[runlim] sample:		13535.1 time, 3420.5 real, 777.4 MB
[runlim] sample:		13574.7 time, 3430.5 real, 779.4 MB
[runlim] sample:		13614.3 time, 3440.5 real, 791.4 MB
[runlim] sample:		13653.9 time, 3450.5 real, 791.4 MB
[runlim] sample:		13693.5 time, 3460.5 real, 793.4 MB
[runlim] sample:		13733.2 time, 3470.5 real, 793.4 MB
[runlim] sample:		13772.8 time, 3480.5 real, 795.4 MB
[runlim] sample:		13812.4 time, 3490.5 real, 797.4 MB
[runlim] sample:		13852.0 time, 3500.5 real, 801.4 MB
[runlim] sample:		13891.6 time, 3510.5 real, 805.1 MB
[runlim] sample:		13931.2 time, 3520.5 real, 807.1 MB
[runlim] sample:		13970.9 time, 3530.5 real, 807.1 MB
[runlim] sample:		14010.5 time, 3540.5 real, 811.1 MB
[runlim] sample:		14050.1 time, 3550.5 real, 813.1 MB
[runlim] sample:		14089.7 time, 3560.5 real, 813.1 MB
[runlim] sample:		14129.3 time, 3570.5 real, 813.3 MB
[runlim] sample:		14168.9 time, 3580.5 real, 814.8 MB
[runlim] sample:		14208.5 time, 3590.5 real, 817.1 MB
[runlim] end:			Wed Sep 16 08:02:06 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.11 seconds
[runlim] time:			14246.56 seconds
[runlim] space:			826.4 MB
[runlim] samples:		35996
