[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/6s517rb0.aig
[runlim] start:			Wed Sep 16 16:50:22 2015
[runlim] main pid:		29265
[runlim] sample:		25.9 time, 10.2 real, 154.8 MB
[runlim] sample:		65.5 time, 20.2 real, 163.5 MB
[runlim] sample:		105.2 time, 30.2 real, 173.3 MB
[runlim] sample:		144.8 time, 40.2 real, 181.6 MB
[runlim] sample:		184.5 time, 50.2 real, 173.0 MB
[runlim] sample:		224.1 time, 60.2 real, 177.4 MB
[runlim] sample:		263.8 time, 70.2 real, 186.1 MB
[runlim] sample:		303.4 time, 80.2 real, 186.3 MB
[runlim] sample:		343.1 time, 90.2 real, 188.9 MB
[runlim] sample:		382.7 time, 100.2 real, 198.7 MB
[runlim] sample:		422.3 time, 110.2 real, 202.4 MB
[runlim] sample:		461.9 time, 120.2 real, 194.0 MB
[runlim] sample:		501.6 time, 130.2 real, 197.7 MB
[runlim] sample:		541.2 time, 140.2 real, 210.2 MB
[runlim] sample:		580.9 time, 150.2 real, 204.7 MB
[runlim] sample:		620.5 time, 160.2 real, 198.1 MB
[runlim] sample:		660.2 time, 170.2 real, 199.0 MB
[runlim] sample:		699.8 time, 180.2 real, 204.5 MB
[runlim] sample:		739.5 time, 190.2 real, 205.2 MB
[runlim] sample:		779.1 time, 200.2 real, 205.0 MB
[runlim] sample:		818.7 time, 210.2 real, 207.3 MB
[runlim] sample:		858.4 time, 220.2 real, 205.4 MB
[runlim] sample:		898.0 time, 230.2 real, 220.5 MB
[runlim] sample:		937.7 time, 240.2 real, 214.8 MB
[runlim] sample:		977.3 time, 250.2 real, 217.1 MB
[runlim] sample:		1017.0 time, 260.2 real, 219.2 MB
[runlim] sample:		1056.6 time, 270.2 real, 220.4 MB
[runlim] sample:		1096.2 time, 280.2 real, 211.8 MB
[runlim] sample:		1135.9 time, 290.2 real, 217.1 MB
[runlim] sample:		1175.5 time, 300.2 real, 227.2 MB
[runlim] sample:		1215.2 time, 310.2 real, 220.9 MB
[runlim] sample:		1254.8 time, 320.2 real, 221.3 MB
[runlim] sample:		1294.5 time, 330.2 real, 222.2 MB
[runlim] sample:		1334.1 time, 340.2 real, 224.8 MB
[runlim] sample:		1373.7 time, 350.2 real, 227.0 MB
[runlim] sample:		1413.4 time, 360.2 real, 227.1 MB
[runlim] sample:		1453.0 time, 370.2 real, 229.2 MB
[runlim] sample:		1492.7 time, 380.2 real, 238.1 MB
[runlim] sample:		1532.3 time, 390.2 real, 228.8 MB
[runlim] sample:		1571.9 time, 400.2 real, 231.2 MB
[runlim] sample:		1611.6 time, 410.2 real, 240.7 MB
[runlim] sample:		1651.2 time, 420.2 real, 235.0 MB
[runlim] sample:		1690.8 time, 430.2 real, 240.9 MB
[runlim] sample:		1730.5 time, 440.2 real, 237.2 MB
[runlim] sample:		1770.1 time, 450.2 real, 246.2 MB
[runlim] sample:		1809.8 time, 460.2 real, 244.6 MB
[runlim] sample:		1849.4 time, 470.2 real, 243.6 MB
[runlim] sample:		1889.1 time, 480.2 real, 246.9 MB
[runlim] sample:		1928.7 time, 490.2 real, 248.1 MB
[runlim] sample:		1968.3 time, 500.2 real, 249.6 MB
[runlim] sample:		2008.0 time, 510.2 real, 249.3 MB
[runlim] sample:		2047.6 time, 520.2 real, 251.3 MB
[runlim] sample:		2087.3 time, 530.2 real, 254.6 MB
[runlim] sample:		2126.9 time, 540.2 real, 255.2 MB
[runlim] sample:		2166.6 time, 550.2 real, 252.3 MB
[runlim] sample:		2206.2 time, 560.2 real, 258.0 MB
[runlim] sample:		2245.8 time, 570.2 real, 259.7 MB
[runlim] sample:		2285.5 time, 580.2 real, 271.7 MB
[runlim] sample:		2325.1 time, 590.2 real, 260.0 MB
[runlim] sample:		2364.8 time, 600.2 real, 258.8 MB
[runlim] sample:		2404.4 time, 610.2 real, 259.3 MB
[runlim] sample:		2444.0 time, 620.2 real, 277.7 MB
[runlim] sample:		2483.7 time, 630.2 real, 270.5 MB
[runlim] sample:		2523.3 time, 640.2 real, 268.7 MB
[runlim] sample:		2562.9 time, 650.2 real, 270.1 MB
[runlim] sample:		2602.6 time, 660.2 real, 269.8 MB
[runlim] sample:		2642.2 time, 670.2 real, 260.2 MB
[runlim] sample:		2681.9 time, 680.2 real, 264.0 MB
[runlim] sample:		2721.5 time, 690.2 real, 263.1 MB
[runlim] sample:		2761.1 time, 700.2 real, 261.8 MB
[runlim] sample:		2800.8 time, 710.2 real, 267.4 MB
[runlim] sample:		2840.4 time, 720.2 real, 265.0 MB
[runlim] sample:		2880.1 time, 730.2 real, 264.5 MB
[runlim] sample:		2919.7 time, 740.2 real, 266.9 MB
[runlim] sample:		2959.3 time, 750.2 real, 261.8 MB
[runlim] sample:		2999.0 time, 760.2 real, 264.1 MB
[runlim] sample:		3038.6 time, 770.2 real, 269.5 MB
[runlim] sample:		3078.2 time, 780.2 real, 265.3 MB
[runlim] sample:		3117.9 time, 790.2 real, 266.7 MB
[runlim] sample:		3157.5 time, 800.2 real, 272.2 MB
[runlim] sample:		3197.2 time, 810.2 real, 280.7 MB
[runlim] sample:		3236.8 time, 820.2 real, 282.3 MB
[runlim] sample:		3276.4 time, 830.2 real, 282.5 MB
[runlim] sample:		3316.1 time, 840.2 real, 287.8 MB
[runlim] sample:		3355.7 time, 850.2 real, 284.0 MB
[runlim] sample:		3395.3 time, 860.2 real, 299.6 MB
[runlim] sample:		3435.0 time, 870.2 real, 293.5 MB
[runlim] sample:		3474.6 time, 880.2 real, 288.6 MB
[runlim] sample:		3514.2 time, 890.2 real, 288.2 MB
[runlim] sample:		3553.9 time, 900.2 real, 294.6 MB
[runlim] sample:		3593.5 time, 910.2 real, 308.3 MB
[runlim] sample:		3633.2 time, 920.2 real, 300.9 MB
[runlim] sample:		3672.8 time, 930.2 real, 308.1 MB
[runlim] sample:		3712.4 time, 940.2 real, 310.6 MB
[runlim] sample:		3752.0 time, 950.2 real, 311.4 MB
[runlim] sample:		3791.7 time, 960.2 real, 304.4 MB
[runlim] sample:		3831.3 time, 970.2 real, 304.5 MB
[runlim] sample:		3870.9 time, 980.2 real, 311.4 MB
[runlim] sample:		3910.6 time, 990.2 real, 311.7 MB
[runlim] sample:		3950.2 time, 1000.2 real, 309.4 MB
[runlim] sample:		3989.8 time, 1010.2 real, 307.4 MB
[runlim] sample:		4029.5 time, 1020.2 real, 309.1 MB
[runlim] sample:		4069.1 time, 1030.2 real, 323.4 MB
[runlim] sample:		4108.7 time, 1040.2 real, 317.4 MB
[runlim] sample:		4148.4 time, 1050.2 real, 316.3 MB
[runlim] sample:		4188.0 time, 1060.2 real, 332.4 MB
[runlim] sample:		4227.6 time, 1070.2 real, 330.8 MB
[runlim] sample:		4267.3 time, 1080.2 real, 333.1 MB
[runlim] sample:		4306.9 time, 1090.2 real, 325.7 MB
[runlim] sample:		4346.5 time, 1100.2 real, 317.2 MB
[runlim] sample:		4386.2 time, 1110.2 real, 328.4 MB
[runlim] sample:		4425.8 time, 1120.2 real, 319.5 MB
[runlim] sample:		4465.4 time, 1130.2 real, 327.3 MB
[runlim] sample:		4505.1 time, 1140.2 real, 318.1 MB
[runlim] sample:		4544.7 time, 1150.2 real, 318.2 MB
[runlim] sample:		4584.4 time, 1160.2 real, 319.4 MB
[runlim] sample:		4624.0 time, 1170.2 real, 321.3 MB
[runlim] sample:		4663.6 time, 1180.2 real, 321.6 MB
[runlim] sample:		4703.3 time, 1190.2 real, 324.6 MB
[runlim] sample:		4742.9 time, 1200.2 real, 337.7 MB
[runlim] sample:		4782.5 time, 1210.2 real, 331.4 MB
[runlim] sample:		4822.1 time, 1220.2 real, 343.3 MB
[runlim] sample:		4861.8 time, 1230.2 real, 320.3 MB
[runlim] sample:		4901.4 time, 1240.2 real, 336.8 MB
[runlim] sample:		4941.1 time, 1250.2 real, 315.1 MB
[runlim] sample:		4980.7 time, 1260.2 real, 315.1 MB
[runlim] sample:		5020.3 time, 1270.2 real, 324.9 MB
[runlim] sample:		5059.9 time, 1280.2 real, 323.4 MB
[runlim] sample:		5099.6 time, 1290.2 real, 324.4 MB
[runlim] sample:		5139.2 time, 1300.2 real, 318.9 MB
[runlim] sample:		5178.8 time, 1310.2 real, 320.9 MB
[runlim] sample:		5218.5 time, 1320.2 real, 336.9 MB
[runlim] sample:		5258.1 time, 1330.2 real, 350.2 MB
[runlim] sample:		5297.7 time, 1340.2 real, 335.5 MB
[runlim] sample:		5337.4 time, 1350.2 real, 337.3 MB
[runlim] sample:		5377.0 time, 1360.2 real, 337.5 MB
[runlim] sample:		5416.6 time, 1370.2 real, 342.1 MB
[runlim] sample:		5456.2 time, 1380.2 real, 332.7 MB
[runlim] sample:		5495.9 time, 1390.2 real, 346.2 MB
[runlim] sample:		5535.5 time, 1400.2 real, 348.1 MB
[runlim] sample:		5575.1 time, 1410.2 real, 349.0 MB
[runlim] sample:		5614.8 time, 1420.2 real, 347.5 MB
[runlim] sample:		5654.4 time, 1430.2 real, 349.2 MB
[runlim] sample:		5694.0 time, 1440.2 real, 349.6 MB
[runlim] sample:		5733.7 time, 1450.2 real, 352.2 MB
[runlim] sample:		5773.3 time, 1460.2 real, 353.0 MB
[runlim] sample:		5812.9 time, 1470.2 real, 356.7 MB
[runlim] sample:		5852.6 time, 1480.2 real, 357.9 MB
[runlim] sample:		5892.2 time, 1490.2 real, 356.2 MB
[runlim] sample:		5931.8 time, 1500.2 real, 358.1 MB
[runlim] sample:		5971.5 time, 1510.2 real, 356.5 MB
[runlim] sample:		6011.1 time, 1520.2 real, 371.9 MB
[runlim] sample:		6050.7 time, 1530.2 real, 370.5 MB
[runlim] sample:		6090.3 time, 1540.2 real, 374.1 MB
[runlim] sample:		6130.0 time, 1550.2 real, 374.1 MB
[runlim] sample:		6169.6 time, 1560.2 real, 389.8 MB
[runlim] sample:		6209.2 time, 1570.2 real, 397.5 MB
[runlim] sample:		6248.9 time, 1580.2 real, 402.7 MB
[runlim] sample:		6288.5 time, 1590.2 real, 398.0 MB
[runlim] sample:		6328.1 time, 1600.2 real, 400.0 MB
[runlim] sample:		6367.7 time, 1610.2 real, 400.0 MB
[runlim] sample:		6407.4 time, 1620.2 real, 401.0 MB
[runlim] sample:		6447.0 time, 1630.2 real, 401.1 MB
[runlim] sample:		6486.6 time, 1640.2 real, 404.4 MB
[runlim] sample:		6526.2 time, 1650.2 real, 404.4 MB
[runlim] sample:		6565.9 time, 1660.2 real, 408.0 MB
[runlim] sample:		6605.5 time, 1670.2 real, 408.0 MB
[runlim] sample:		6645.1 time, 1680.2 real, 423.8 MB
[runlim] sample:		6684.8 time, 1690.2 real, 424.1 MB
[runlim] sample:		6724.4 time, 1700.2 real, 424.1 MB
[runlim] sample:		6764.0 time, 1710.2 real, 424.3 MB
[runlim] sample:		6803.7 time, 1720.2 real, 436.8 MB
[runlim] sample:		6843.3 time, 1730.2 real, 437.1 MB
[runlim] sample:		6882.9 time, 1740.2 real, 437.1 MB
[runlim] sample:		6922.6 time, 1750.2 real, 437.3 MB
[runlim] sample:		6962.2 time, 1760.2 real, 441.7 MB
[runlim] sample:		7001.8 time, 1770.2 real, 441.7 MB
[runlim] sample:		7041.4 time, 1780.2 real, 441.7 MB
[runlim] sample:		7081.1 time, 1790.2 real, 441.7 MB
[runlim] sample:		7120.7 time, 1800.2 real, 444.2 MB
[runlim] sample:		7160.3 time, 1810.2 real, 446.2 MB
[runlim] sample:		7200.0 time, 1820.2 real, 446.2 MB
[runlim] sample:		7239.6 time, 1830.2 real, 447.0 MB
[runlim] sample:		7279.2 time, 1840.2 real, 448.2 MB
[runlim] sample:		7318.9 time, 1850.2 real, 448.2 MB
[runlim] sample:		7358.5 time, 1860.2 real, 452.3 MB
[runlim] sample:		7398.1 time, 1870.2 real, 452.1 MB
[runlim] sample:		7437.7 time, 1880.2 real, 393.2 MB
[runlim] sample:		7477.4 time, 1890.2 real, 393.2 MB
[runlim] sample:		7517.0 time, 1900.2 real, 413.2 MB
[runlim] sample:		7556.6 time, 1910.2 real, 413.2 MB
[runlim] sample:		7596.2 time, 1920.2 real, 412.5 MB
[runlim] sample:		7635.9 time, 1930.2 real, 415.0 MB
[runlim] sample:		7675.5 time, 1940.2 real, 416.7 MB
[runlim] sample:		7715.1 time, 1950.2 real, 416.9 MB
[runlim] sample:		7754.7 time, 1960.2 real, 415.3 MB
[runlim] sample:		7794.4 time, 1970.2 real, 415.9 MB
[runlim] sample:		7834.0 time, 1980.2 real, 416.2 MB
[runlim] sample:		7873.6 time, 1990.2 real, 416.4 MB
[runlim] sample:		7913.2 time, 2000.2 real, 416.7 MB
[runlim] sample:		7952.9 time, 2010.2 real, 417.1 MB
[runlim] sample:		7992.5 time, 2020.2 real, 420.1 MB
[runlim] sample:		8032.1 time, 2030.2 real, 420.1 MB
[runlim] sample:		8071.7 time, 2040.2 real, 420.4 MB
[runlim] sample:		8111.4 time, 2050.2 real, 420.9 MB
[runlim] sample:		8151.0 time, 2060.2 real, 421.4 MB
[runlim] sample:		8190.6 time, 2070.2 real, 427.4 MB
[runlim] sample:		8230.2 time, 2080.2 real, 427.9 MB
[runlim] sample:		8269.9 time, 2090.2 real, 428.1 MB
[runlim] sample:		8309.5 time, 2100.2 real, 417.2 MB
[runlim] sample:		8349.1 time, 2110.2 real, 421.2 MB
[runlim] sample:		8388.8 time, 2120.2 real, 438.7 MB
[runlim] sample:		8428.4 time, 2130.2 real, 446.7 MB
[runlim] sample:		8468.0 time, 2140.2 real, 454.7 MB
[runlim] sample:		8507.6 time, 2150.2 real, 455.9 MB
[runlim] sample:		8547.3 time, 2160.2 real, 457.9 MB
[runlim] sample:		8586.9 time, 2170.2 real, 457.9 MB
[runlim] sample:		8626.5 time, 2180.2 real, 457.9 MB
[runlim] sample:		8666.2 time, 2190.2 real, 457.9 MB
[runlim] sample:		8705.8 time, 2200.2 real, 457.9 MB
[runlim] sample:		8745.4 time, 2210.2 real, 457.9 MB
[runlim] sample:		8785.0 time, 2220.2 real, 457.9 MB
[runlim] sample:		8824.7 time, 2230.2 real, 457.9 MB
[runlim] sample:		8864.3 time, 2240.2 real, 457.9 MB
[runlim] sample:		8903.9 time, 2250.2 real, 457.9 MB
[runlim] sample:		8943.5 time, 2260.2 real, 458.3 MB
[runlim] sample:		8983.2 time, 2270.2 real, 458.3 MB
[runlim] sample:		9022.8 time, 2280.2 real, 458.3 MB
[runlim] sample:		9062.4 time, 2290.2 real, 458.5 MB
[runlim] sample:		9102.0 time, 2300.2 real, 458.5 MB
[runlim] sample:		9141.7 time, 2310.2 real, 458.5 MB
[runlim] sample:		9181.3 time, 2320.2 real, 458.5 MB
[runlim] sample:		9220.9 time, 2330.2 real, 458.5 MB
[runlim] sample:		9260.5 time, 2340.2 real, 458.5 MB
[runlim] sample:		9300.2 time, 2350.2 real, 460.5 MB
[runlim] sample:		9339.8 time, 2360.2 real, 463.0 MB
[runlim] sample:		9379.4 time, 2370.2 real, 463.0 MB
[runlim] sample:		9419.0 time, 2380.2 real, 463.0 MB
[runlim] sample:		9458.7 time, 2390.2 real, 463.0 MB
[runlim] sample:		9498.3 time, 2400.2 real, 463.0 MB
[runlim] sample:		9537.9 time, 2410.2 real, 463.0 MB
[runlim] sample:		9577.5 time, 2420.2 real, 463.0 MB
[runlim] sample:		9617.2 time, 2430.2 real, 466.1 MB
[runlim] sample:		9656.8 time, 2440.2 real, 466.1 MB
[runlim] sample:		9696.4 time, 2450.2 real, 468.1 MB
[runlim] sample:		9736.0 time, 2460.2 real, 468.1 MB
[runlim] sample:		9775.6 time, 2470.2 real, 473.4 MB
[runlim] sample:		9815.3 time, 2480.2 real, 419.9 MB
[runlim] sample:		9854.9 time, 2490.2 real, 438.4 MB
[runlim] sample:		9894.5 time, 2500.2 real, 439.4 MB
[runlim] sample:		9934.1 time, 2510.2 real, 440.3 MB
[runlim] sample:		9973.8 time, 2520.2 real, 442.6 MB
[runlim] sample:		10013.4 time, 2530.2 real, 444.7 MB
[runlim] sample:		10053.0 time, 2540.2 real, 444.7 MB
[runlim] sample:		10092.6 time, 2550.2 real, 444.7 MB
[runlim] sample:		10132.3 time, 2560.2 real, 444.7 MB
[runlim] sample:		10171.9 time, 2570.2 real, 445.0 MB
[runlim] sample:		10211.5 time, 2580.2 real, 438.3 MB
[runlim] sample:		10251.2 time, 2590.2 real, 449.4 MB
[runlim] sample:		10290.8 time, 2600.2 real, 449.4 MB
[runlim] sample:		10330.4 time, 2610.2 real, 449.6 MB
[runlim] sample:		10370.0 time, 2620.2 real, 450.4 MB
[runlim] sample:		10409.7 time, 2630.2 real, 454.4 MB
[runlim] sample:		10449.3 time, 2640.2 real, 456.4 MB
[runlim] sample:		10488.9 time, 2650.2 real, 456.6 MB
[runlim] sample:		10528.5 time, 2660.2 real, 456.6 MB
[runlim] sample:		10568.1 time, 2670.2 real, 456.8 MB
[runlim] sample:		10607.8 time, 2680.2 real, 456.8 MB
[runlim] sample:		10647.4 time, 2690.2 real, 456.8 MB
[runlim] sample:		10687.0 time, 2700.2 real, 457.0 MB
[runlim] sample:		10726.6 time, 2710.2 real, 457.0 MB
[runlim] sample:		10766.3 time, 2720.2 real, 463.0 MB
[runlim] sample:		10805.9 time, 2730.2 real, 463.0 MB
[runlim] sample:		10845.5 time, 2740.2 real, 463.2 MB
[runlim] sample:		10885.1 time, 2750.2 real, 464.2 MB
[runlim] sample:		10924.8 time, 2760.2 real, 464.5 MB
[runlim] sample:		10964.4 time, 2770.2 real, 500.5 MB
[runlim] sample:		11004.0 time, 2780.2 real, 466.9 MB
[runlim] sample:		11043.6 time, 2790.2 real, 467.0 MB
[runlim] sample:		11083.2 time, 2800.2 real, 467.1 MB
[runlim] sample:		11122.9 time, 2810.2 real, 483.8 MB
[runlim] sample:		11162.5 time, 2820.2 real, 483.8 MB
[runlim] sample:		11202.1 time, 2830.2 real, 483.8 MB
[runlim] sample:		11241.8 time, 2840.2 real, 484.0 MB
[runlim] sample:		11281.4 time, 2850.2 real, 484.0 MB
[runlim] sample:		11321.0 time, 2860.2 real, 484.0 MB
[runlim] sample:		11360.6 time, 2870.2 real, 484.4 MB
[runlim] sample:		11400.2 time, 2880.2 real, 484.5 MB
[runlim] sample:		11439.9 time, 2890.2 real, 484.6 MB
[runlim] sample:		11479.5 time, 2900.2 real, 484.8 MB
[runlim] sample:		11519.1 time, 2910.2 real, 484.9 MB
[runlim] sample:		11558.8 time, 2920.2 real, 478.4 MB
[runlim] sample:		11598.4 time, 2930.2 real, 478.4 MB
[runlim] sample:		11638.0 time, 2940.2 real, 482.7 MB
[runlim] sample:		11677.6 time, 2950.2 real, 477.8 MB
[runlim] sample:		11717.3 time, 2960.2 real, 482.4 MB
[runlim] sample:		11756.9 time, 2970.2 real, 478.3 MB
[runlim] sample:		11796.5 time, 2980.2 real, 484.0 MB
[runlim] sample:		11836.1 time, 2990.2 real, 480.1 MB
[runlim] sample:		11875.8 time, 3000.2 real, 484.2 MB
[runlim] sample:		11915.4 time, 3010.2 real, 480.1 MB
[runlim] sample:		11955.0 time, 3020.2 real, 481.7 MB
[runlim] sample:		11994.6 time, 3030.2 real, 482.4 MB
[runlim] sample:		12034.2 time, 3040.2 real, 482.4 MB
[runlim] sample:		12073.9 time, 3050.2 real, 482.6 MB
[runlim] sample:		12113.5 time, 3060.2 real, 487.2 MB
[runlim] sample:		12153.1 time, 3070.2 real, 487.2 MB
[runlim] sample:		12192.8 time, 3080.2 real, 487.7 MB
[runlim] sample:		12232.4 time, 3090.2 real, 487.4 MB
[runlim] sample:		12272.0 time, 3100.2 real, 487.7 MB
[runlim] sample:		12311.6 time, 3110.2 real, 487.4 MB
[runlim] sample:		12351.2 time, 3120.2 real, 483.5 MB
[runlim] sample:		12390.9 time, 3130.2 real, 442.4 MB
[runlim] sample:		12430.5 time, 3140.2 real, 449.6 MB
[runlim] sample:		12470.1 time, 3150.2 real, 449.3 MB
[runlim] sample:		12509.7 time, 3160.2 real, 415.7 MB
[runlim] sample:		12549.4 time, 3170.2 real, 420.4 MB
[runlim] sample:		12589.0 time, 3180.2 real, 420.8 MB
[runlim] sample:		12628.6 time, 3190.2 real, 422.8 MB
[runlim] sample:		12668.2 time, 3200.2 real, 423.0 MB
[runlim] sample:		12707.9 time, 3210.2 real, 423.3 MB
[runlim] sample:		12747.5 time, 3220.2 real, 423.5 MB
[runlim] sample:		12787.1 time, 3230.2 real, 431.1 MB
[runlim] sample:		12826.7 time, 3240.2 real, 430.2 MB
[runlim] sample:		12866.4 time, 3250.2 real, 430.6 MB
[runlim] sample:		12906.0 time, 3260.2 real, 433.4 MB
[runlim] sample:		12945.6 time, 3270.2 real, 434.2 MB
[runlim] sample:		12985.2 time, 3280.2 real, 429.5 MB
[runlim] sample:		13024.8 time, 3290.2 real, 429.7 MB
[runlim] sample:		13064.5 time, 3300.2 real, 429.7 MB
[runlim] sample:		13104.1 time, 3310.2 real, 430.0 MB
[runlim] sample:		13143.7 time, 3320.2 real, 433.0 MB
[runlim] sample:		13183.3 time, 3330.2 real, 433.5 MB
[runlim] sample:		13223.0 time, 3340.2 real, 434.3 MB
[runlim] sample:		13262.6 time, 3350.2 real, 446.8 MB
[runlim] sample:		13302.2 time, 3360.2 real, 440.8 MB
[runlim] sample:		13341.8 time, 3370.2 real, 446.5 MB
[runlim] sample:		13381.5 time, 3380.2 real, 447.1 MB
[runlim] sample:		13421.1 time, 3390.2 real, 447.4 MB
[runlim] sample:		13460.7 time, 3400.2 real, 473.9 MB
[runlim] sample:		13500.3 time, 3410.2 real, 476.1 MB
[runlim] sample:		13540.0 time, 3420.2 real, 476.1 MB
[runlim] sample:		13579.6 time, 3430.2 real, 476.1 MB
[runlim] sample:		13619.2 time, 3440.2 real, 498.2 MB
[runlim] sample:		13658.9 time, 3450.2 real, 503.1 MB
[runlim] sample:		13698.5 time, 3460.2 real, 503.6 MB
[runlim] sample:		13738.1 time, 3470.2 real, 504.9 MB
[runlim] sample:		13777.7 time, 3480.2 real, 506.4 MB
[runlim] sample:		13817.4 time, 3490.2 real, 508.4 MB
[runlim] sample:		13857.0 time, 3500.2 real, 508.4 MB
[runlim] sample:		13896.6 time, 3510.2 real, 510.4 MB
[runlim] sample:		13936.2 time, 3520.2 real, 511.7 MB
[runlim] sample:		13975.9 time, 3530.2 real, 511.7 MB
[runlim] sample:		14015.5 time, 3540.2 real, 519.7 MB
[runlim] sample:		14055.1 time, 3550.2 real, 519.7 MB
[runlim] sample:		14094.7 time, 3560.2 real, 511.7 MB
[runlim] sample:		14134.4 time, 3570.2 real, 519.7 MB
[runlim] sample:		14174.0 time, 3580.2 real, 511.7 MB
[runlim] sample:		14213.6 time, 3590.2 real, 522.4 MB
[runlim] end:			Wed Sep 16 17:50:22 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.06 seconds
[runlim] time:			14252.45 seconds
[runlim] space:			532.4 MB
[runlim] samples:		35998
