[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/nuxmv/single.nuxmv
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/beemcmbrdg7f2.aig
[runlim] start:			Sun Sep 20 03:44:58 2015
[runlim] main pid:		8254
[runlim] sample:		38.9 time, 10.4 real, 158.0 MB
[runlim] sample:		78.5 time, 20.4 real, 166.4 MB
[runlim] sample:		118.1 time, 30.4 real, 169.4 MB
[runlim] sample:		157.8 time, 40.4 real, 191.6 MB
[runlim] sample:		197.4 time, 50.4 real, 212.4 MB
[runlim] sample:		237.1 time, 60.4 real, 250.2 MB
[runlim] sample:		276.8 time, 70.4 real, 256.3 MB
[runlim] sample:		316.4 time, 80.4 real, 264.5 MB
[runlim] sample:		356.1 time, 90.4 real, 218.8 MB
[runlim] sample:		395.7 time, 100.4 real, 221.3 MB
[runlim] sample:		435.4 time, 110.4 real, 256.3 MB
[runlim] sample:		475.0 time, 120.4 real, 265.6 MB
[runlim] sample:		514.6 time, 130.4 real, 283.0 MB
[runlim] sample:		554.3 time, 140.4 real, 278.5 MB
[runlim] sample:		593.9 time, 150.4 real, 284.1 MB
[runlim] sample:		633.6 time, 160.4 real, 232.6 MB
[runlim] sample:		673.2 time, 170.4 real, 235.6 MB
[runlim] sample:		712.8 time, 180.4 real, 232.5 MB
[runlim] sample:		752.5 time, 190.4 real, 236.3 MB
[runlim] sample:		792.2 time, 200.4 real, 269.6 MB
[runlim] sample:		831.8 time, 210.4 real, 276.7 MB
[runlim] sample:		871.4 time, 220.4 real, 283.0 MB
[runlim] sample:		911.0 time, 230.4 real, 285.4 MB
[runlim] sample:		950.6 time, 240.4 real, 237.7 MB
[runlim] sample:		990.2 time, 250.4 real, 237.7 MB
[runlim] sample:		1029.8 time, 260.4 real, 237.7 MB
[runlim] sample:		1069.4 time, 270.4 real, 270.8 MB
[runlim] sample:		1109.0 time, 280.4 real, 277.2 MB
[runlim] sample:		1148.7 time, 290.4 real, 313.0 MB
[runlim] sample:		1188.3 time, 300.4 real, 303.2 MB
[runlim] sample:		1227.9 time, 310.4 real, 256.0 MB
[runlim] sample:		1267.5 time, 320.4 real, 256.0 MB
[runlim] sample:		1307.1 time, 330.4 real, 291.2 MB
[runlim] sample:		1346.7 time, 340.4 real, 297.9 MB
[runlim] sample:		1386.3 time, 350.4 real, 304.2 MB
[runlim] sample:		1425.9 time, 360.4 real, 309.7 MB
[runlim] sample:		1465.5 time, 370.4 real, 316.2 MB
[runlim] sample:		1505.1 time, 380.4 real, 260.9 MB
[runlim] sample:		1544.7 time, 390.4 real, 266.5 MB
[runlim] sample:		1584.3 time, 400.4 real, 294.2 MB
[runlim] sample:		1623.9 time, 410.4 real, 300.7 MB
[runlim] sample:		1663.5 time, 420.4 real, 304.7 MB
[runlim] sample:		1703.1 time, 430.4 real, 309.1 MB
[runlim] sample:		1742.7 time, 440.4 real, 314.7 MB
[runlim] sample:		1782.3 time, 450.4 real, 322.2 MB
[runlim] sample:		1821.9 time, 460.4 real, 328.7 MB
[runlim] sample:		1861.5 time, 470.4 real, 330.7 MB
[runlim] sample:		1901.1 time, 480.4 real, 265.7 MB
[runlim] sample:		1940.8 time, 490.4 real, 265.7 MB
[runlim] sample:		1980.4 time, 500.4 real, 265.7 MB
[runlim] sample:		2020.0 time, 510.4 real, 298.8 MB
[runlim] sample:		2059.6 time, 520.4 real, 304.9 MB
[runlim] sample:		2099.2 time, 530.4 real, 310.9 MB
[runlim] sample:		2138.8 time, 540.4 real, 316.9 MB
[runlim] sample:		2178.4 time, 550.4 real, 321.2 MB
[runlim] sample:		2218.1 time, 560.4 real, 325.2 MB
[runlim] sample:		2257.7 time, 570.4 real, 329.2 MB
[runlim] sample:		2297.3 time, 580.4 real, 266.0 MB
[runlim] sample:		2336.9 time, 590.4 real, 266.0 MB
[runlim] sample:		2376.5 time, 600.4 real, 299.0 MB
[runlim] sample:		2416.1 time, 610.4 real, 307.8 MB
[runlim] sample:		2455.8 time, 620.4 real, 311.8 MB
[runlim] sample:		2495.4 time, 630.4 real, 317.6 MB
[runlim] sample:		2535.0 time, 640.4 real, 323.8 MB
[runlim] sample:		2574.6 time, 650.4 real, 327.8 MB
[runlim] sample:		2614.2 time, 660.4 real, 266.6 MB
[runlim] sample:		2653.8 time, 670.4 real, 266.6 MB
[runlim] sample:		2693.4 time, 680.4 real, 299.9 MB
[runlim] sample:		2733.1 time, 690.4 real, 308.1 MB
[runlim] sample:		2772.7 time, 700.4 real, 312.1 MB
[runlim] sample:		2812.3 time, 710.4 real, 317.9 MB
[runlim] sample:		2851.9 time, 720.4 real, 323.9 MB
[runlim] sample:		2891.5 time, 730.4 real, 350.6 MB
[runlim] sample:		2931.1 time, 740.4 real, 356.6 MB
[runlim] sample:		2970.8 time, 750.4 real, 368.7 MB
[runlim] sample:		3010.4 time, 760.4 real, 371.4 MB
[runlim] sample:		3050.0 time, 770.4 real, 378.0 MB
[runlim] sample:		3089.6 time, 780.4 real, 299.5 MB
[runlim] sample:		3129.2 time, 790.4 real, 299.5 MB
[runlim] sample:		3168.8 time, 800.4 real, 299.5 MB
[runlim] sample:		3208.4 time, 810.4 real, 336.7 MB
[runlim] sample:		3248.1 time, 820.4 real, 345.0 MB
[runlim] sample:		3287.7 time, 830.4 real, 352.7 MB
[runlim] sample:		3327.3 time, 840.4 real, 359.0 MB
[runlim] sample:		3366.9 time, 850.4 real, 365.0 MB
[runlim] sample:		3406.5 time, 860.4 real, 369.0 MB
[runlim] sample:		3446.0 time, 870.4 real, 373.0 MB
[runlim] sample:		3485.7 time, 880.4 real, 383.0 MB
[runlim] sample:		3525.3 time, 890.4 real, 368.9 MB
[runlim] sample:		3564.9 time, 900.4 real, 372.9 MB
[runlim] sample:		3604.6 time, 910.4 real, 287.7 MB
[runlim] sample:		3644.2 time, 920.4 real, 287.7 MB
[runlim] sample:		3683.8 time, 930.4 real, 324.9 MB
[runlim] sample:		3723.4 time, 940.4 real, 328.9 MB
[runlim] sample:		3763.0 time, 950.4 real, 340.2 MB
[runlim] sample:		3802.6 time, 960.4 real, 350.6 MB
[runlim] sample:		3842.3 time, 970.4 real, 355.1 MB
[runlim] sample:		3881.9 time, 980.4 real, 361.1 MB
[runlim] sample:		3921.5 time, 990.4 real, 367.1 MB
[runlim] sample:		3961.1 time, 1000.4 real, 371.1 MB
[runlim] sample:		4000.8 time, 1010.4 real, 375.1 MB
[runlim] sample:		4040.4 time, 1020.4 real, 377.4 MB
[runlim] sample:		4080.0 time, 1030.4 real, 381.3 MB
[runlim] sample:		4119.6 time, 1040.4 real, 385.3 MB
[runlim] sample:		4159.2 time, 1050.4 real, 387.3 MB
[runlim] sample:		4198.9 time, 1060.4 real, 300.1 MB
[runlim] sample:		4238.5 time, 1070.4 real, 302.1 MB
[runlim] sample:		4278.1 time, 1080.4 real, 306.1 MB
[runlim] sample:		4317.8 time, 1090.4 real, 339.6 MB
[runlim] sample:		4357.4 time, 1100.4 real, 343.6 MB
[runlim] sample:		4397.0 time, 1110.4 real, 349.6 MB
[runlim] sample:		4436.6 time, 1120.4 real, 351.6 MB
[runlim] sample:		4476.2 time, 1130.4 real, 359.6 MB
[runlim] sample:		4515.9 time, 1140.4 real, 363.6 MB
[runlim] sample:		4555.5 time, 1150.4 real, 369.6 MB
[runlim] sample:		4595.1 time, 1160.4 real, 306.7 MB
[runlim] sample:		4634.7 time, 1170.4 real, 308.7 MB
[runlim] sample:		4674.3 time, 1180.4 real, 341.9 MB
[runlim] sample:		4713.9 time, 1190.4 real, 349.9 MB
[runlim] sample:		4753.6 time, 1200.4 real, 357.6 MB
[runlim] sample:		4793.2 time, 1210.4 real, 365.9 MB
[runlim] sample:		4832.8 time, 1220.4 real, 371.9 MB
[runlim] sample:		4872.4 time, 1230.4 real, 378.1 MB
[runlim] sample:		4912.0 time, 1240.4 real, 384.1 MB
[runlim] sample:		4951.6 time, 1250.4 real, 308.9 MB
[runlim] sample:		4991.3 time, 1260.4 real, 339.9 MB
[runlim] sample:		5030.9 time, 1270.4 real, 350.1 MB
[runlim] sample:		5070.5 time, 1280.4 real, 356.1 MB
[runlim] sample:		5110.1 time, 1290.4 real, 363.9 MB
[runlim] sample:		5149.7 time, 1300.4 real, 370.4 MB
[runlim] sample:		5189.3 time, 1310.4 real, 376.4 MB
[runlim] sample:		5229.0 time, 1320.4 real, 382.4 MB
[runlim] sample:		5268.6 time, 1330.4 real, 386.4 MB
[runlim] sample:		5308.2 time, 1340.4 real, 392.4 MB
[runlim] sample:		5347.8 time, 1350.4 real, 396.4 MB
[runlim] sample:		5387.4 time, 1360.4 real, 400.4 MB
[runlim] sample:		5427.1 time, 1370.4 real, 311.4 MB
[runlim] sample:		5466.7 time, 1380.4 real, 342.5 MB
[runlim] sample:		5506.3 time, 1390.4 real, 350.7 MB
[runlim] sample:		5545.9 time, 1400.4 real, 358.7 MB
[runlim] sample:		5585.5 time, 1410.4 real, 364.4 MB
[runlim] sample:		5625.1 time, 1420.4 real, 372.4 MB
[runlim] sample:		5664.7 time, 1430.4 real, 381.2 MB
[runlim] sample:		5704.4 time, 1440.4 real, 388.2 MB
[runlim] sample:		5744.0 time, 1450.4 real, 394.9 MB
[runlim] sample:		5783.6 time, 1460.4 real, 411.2 MB
[runlim] sample:		5823.2 time, 1470.4 real, 403.4 MB
[runlim] sample:		5862.8 time, 1480.4 real, 407.4 MB
[runlim] sample:		5902.4 time, 1490.4 real, 411.4 MB
[runlim] sample:		5942.0 time, 1500.4 real, 415.4 MB
[runlim] sample:		5981.7 time, 1510.4 real, 419.7 MB
[runlim] sample:		6021.3 time, 1520.4 real, 320.5 MB
[runlim] sample:		6060.9 time, 1530.4 real, 322.5 MB
[runlim] sample:		6100.5 time, 1540.4 real, 357.7 MB
[runlim] sample:		6140.1 time, 1550.4 real, 365.7 MB
[runlim] sample:		6179.7 time, 1560.4 real, 369.7 MB
[runlim] sample:		6219.3 time, 1570.4 real, 381.7 MB
[runlim] sample:		6259.0 time, 1580.4 real, 386.0 MB
[runlim] sample:		6298.6 time, 1590.4 real, 392.0 MB
[runlim] sample:		6338.2 time, 1600.4 real, 396.0 MB
[runlim] sample:		6377.8 time, 1610.4 real, 436.0 MB
[runlim] sample:		6417.4 time, 1620.4 real, 412.9 MB
[runlim] sample:		6457.0 time, 1630.4 real, 417.2 MB
[runlim] sample:		6496.6 time, 1640.4 real, 421.2 MB
[runlim] sample:		6536.2 time, 1650.4 real, 425.4 MB
[runlim] sample:		6575.8 time, 1660.4 real, 429.4 MB
[runlim] sample:		6615.5 time, 1670.4 real, 444.7 MB
[runlim] sample:		6655.1 time, 1680.4 real, 446.7 MB
[runlim] sample:		6694.7 time, 1690.4 real, 450.7 MB
[runlim] sample:		6734.3 time, 1700.4 real, 343.5 MB
[runlim] sample:		6773.9 time, 1710.4 real, 345.5 MB
[runlim] sample:		6813.6 time, 1720.4 real, 381.0 MB
[runlim] sample:		6853.2 time, 1730.4 real, 387.0 MB
[runlim] sample:		6892.8 time, 1740.4 real, 393.0 MB
[runlim] sample:		6932.4 time, 1750.4 real, 402.7 MB
[runlim] sample:		6972.0 time, 1760.4 real, 413.0 MB
[runlim] sample:		7011.6 time, 1770.4 real, 421.0 MB
[runlim] sample:		7051.3 time, 1780.4 real, 426.8 MB
[runlim] sample:		7090.9 time, 1790.4 real, 431.0 MB
[runlim] sample:		7130.5 time, 1800.4 real, 437.2 MB
[runlim] sample:		7170.1 time, 1810.4 real, 443.2 MB
[runlim] sample:		7209.7 time, 1820.4 real, 447.5 MB
[runlim] sample:		7249.3 time, 1830.4 real, 453.5 MB
[runlim] sample:		7289.0 time, 1840.4 real, 459.5 MB
[runlim] sample:		7328.5 time, 1850.4 real, 463.5 MB
[runlim] sample:		7368.2 time, 1860.4 real, 467.8 MB
[runlim] sample:		7407.8 time, 1870.4 real, 469.8 MB
[runlim] sample:		7447.4 time, 1880.4 real, 472.2 MB
[runlim] sample:		7487.0 time, 1890.4 real, 475.8 MB
[runlim] sample:		7526.6 time, 1900.4 real, 479.8 MB
[runlim] sample:		7566.2 time, 1910.4 real, 346.6 MB
[runlim] sample:		7605.8 time, 1920.4 real, 348.6 MB
[runlim] sample:		7645.4 time, 1930.4 real, 379.8 MB
[runlim] sample:		7685.0 time, 1940.4 real, 386.0 MB
[runlim] sample:		7724.6 time, 1950.4 real, 392.0 MB
[runlim] sample:		7764.2 time, 1960.4 real, 397.3 MB
[runlim] sample:		7803.8 time, 1970.4 real, 403.8 MB
[runlim] sample:		7843.4 time, 1980.4 real, 411.8 MB
[runlim] sample:		7883.0 time, 1990.4 real, 416.0 MB
[runlim] sample:		7922.7 time, 2000.4 real, 418.3 MB
[runlim] sample:		7962.3 time, 2010.4 real, 422.3 MB
[runlim] sample:		8001.9 time, 2020.4 real, 428.3 MB
[runlim] sample:		8041.5 time, 2030.4 real, 432.1 MB
[runlim] sample:		8081.1 time, 2040.4 real, 436.3 MB
[runlim] sample:		8120.7 time, 2050.4 real, 438.3 MB
[runlim] sample:		8160.3 time, 2060.4 real, 440.3 MB
[runlim] sample:		8199.9 time, 2070.4 real, 442.6 MB
[runlim] sample:		8239.5 time, 2080.4 real, 450.6 MB
[runlim] sample:		8279.0 time, 2090.4 real, 454.6 MB
[runlim] sample:		8318.6 time, 2100.4 real, 458.6 MB
[runlim] sample:		8358.2 time, 2110.4 real, 460.6 MB
[runlim] sample:		8397.7 time, 2120.4 real, 462.6 MB
[runlim] sample:		8437.3 time, 2130.4 real, 466.6 MB
[runlim] sample:		8476.9 time, 2140.4 real, 474.6 MB
[runlim] sample:		8516.5 time, 2150.4 real, 361.4 MB
[runlim] sample:		8556.1 time, 2160.4 real, 363.4 MB
[runlim] sample:		8595.7 time, 2170.4 real, 401.2 MB
[runlim] sample:		8635.3 time, 2180.4 real, 381.8 MB
[runlim] sample:		8674.9 time, 2190.4 real, 388.0 MB
[runlim] sample:		8714.6 time, 2200.4 real, 392.0 MB
[runlim] sample:		8754.2 time, 2210.4 real, 398.2 MB
[runlim] sample:		8793.8 time, 2220.4 real, 404.2 MB
[runlim] sample:		8833.4 time, 2230.4 real, 410.2 MB
[runlim] sample:		8873.0 time, 2240.4 real, 418.4 MB
[runlim] sample:		8912.6 time, 2250.4 real, 424.4 MB
[runlim] sample:		8952.2 time, 2260.4 real, 428.7 MB
[runlim] sample:		8991.9 time, 2270.4 real, 432.7 MB
[runlim] sample:		9031.5 time, 2280.4 real, 436.9 MB
[runlim] sample:		9071.1 time, 2290.4 real, 440.9 MB
[runlim] sample:		9110.7 time, 2300.4 real, 444.9 MB
[runlim] sample:		9150.3 time, 2310.4 real, 448.9 MB
[runlim] sample:		9189.9 time, 2320.4 real, 450.9 MB
[runlim] sample:		9229.6 time, 2330.4 real, 454.9 MB
[runlim] sample:		9269.2 time, 2340.4 real, 456.9 MB
[runlim] sample:		9308.8 time, 2350.4 real, 459.2 MB
[runlim] sample:		9348.4 time, 2360.4 real, 461.2 MB
[runlim] sample:		9388.0 time, 2370.4 real, 342.0 MB
[runlim] sample:		9427.6 time, 2380.4 real, 344.0 MB
[runlim] sample:		9467.2 time, 2390.4 real, 376.7 MB
[runlim] sample:		9506.9 time, 2400.4 real, 382.7 MB
[runlim] sample:		9546.5 time, 2410.4 real, 388.7 MB
[runlim] sample:		9586.1 time, 2420.4 real, 393.0 MB
[runlim] sample:		9625.7 time, 2430.4 real, 401.0 MB
[runlim] sample:		9665.3 time, 2440.4 real, 407.0 MB
[runlim] sample:		9704.9 time, 2450.4 real, 411.0 MB
[runlim] sample:		9744.5 time, 2460.4 real, 415.2 MB
[runlim] sample:		9784.1 time, 2470.4 real, 417.2 MB
[runlim] sample:		9823.8 time, 2480.4 real, 421.2 MB
[runlim] sample:		9863.4 time, 2490.4 real, 423.5 MB
[runlim] sample:		9903.0 time, 2500.4 real, 427.5 MB
[runlim] sample:		9942.6 time, 2510.4 real, 431.5 MB
[runlim] sample:		9982.2 time, 2520.4 real, 435.5 MB
[runlim] sample:		10021.8 time, 2530.4 real, 439.5 MB
[runlim] sample:		10061.4 time, 2540.4 real, 441.5 MB
[runlim] sample:		10101.0 time, 2550.4 real, 443.5 MB
[runlim] sample:		10140.6 time, 2560.4 real, 445.7 MB
[runlim] sample:		10180.2 time, 2570.4 real, 447.7 MB
[runlim] sample:		10219.8 time, 2580.4 real, 348.5 MB
[runlim] sample:		10259.4 time, 2590.4 real, 348.5 MB
[runlim] sample:		10299.0 time, 2600.4 real, 385.7 MB
[runlim] sample:		10338.7 time, 2610.4 real, 393.7 MB
[runlim] sample:		10378.3 time, 2620.4 real, 399.5 MB
[runlim] sample:		10417.9 time, 2630.4 real, 408.0 MB
[runlim] sample:		10457.5 time, 2640.4 real, 414.0 MB
[runlim] sample:		10497.1 time, 2650.4 real, 420.0 MB
[runlim] sample:		10536.7 time, 2660.4 real, 426.0 MB
[runlim] sample:		10576.3 time, 2670.4 real, 350.8 MB
[runlim] sample:		10615.9 time, 2680.4 real, 386.0 MB
[runlim] sample:		10655.5 time, 2690.4 real, 394.0 MB
[runlim] sample:		10695.1 time, 2700.4 real, 398.5 MB
[runlim] sample:		10734.7 time, 2710.4 real, 404.5 MB
[runlim] sample:		10774.4 time, 2720.4 real, 410.5 MB
[runlim] sample:		10814.0 time, 2730.4 real, 416.5 MB
[runlim] sample:		10853.6 time, 2740.4 real, 424.5 MB
[runlim] sample:		10893.2 time, 2750.4 real, 429.4 MB
[runlim] sample:		10932.8 time, 2760.4 real, 436.5 MB
[runlim] sample:		10972.4 time, 2770.4 real, 440.7 MB
[runlim] sample:		11012.0 time, 2780.4 real, 444.7 MB
[runlim] sample:		11051.6 time, 2790.4 real, 448.7 MB
[runlim] sample:		11091.2 time, 2800.4 real, 369.3 MB
[runlim] sample:		11130.8 time, 2810.4 real, 379.3 MB
[runlim] sample:		11170.4 time, 2820.4 real, 419.6 MB
[runlim] sample:		11210.1 time, 2830.4 real, 429.8 MB
[runlim] sample:		11249.7 time, 2840.4 real, 442.0 MB
[runlim] sample:		11289.3 time, 2850.4 real, 461.8 MB
[runlim] sample:		11328.9 time, 2860.4 real, 468.5 MB
[runlim] sample:		11368.5 time, 2870.4 real, 475.8 MB
[runlim] sample:		11408.0 time, 2880.4 real, 479.8 MB
[runlim] sample:		11447.6 time, 2890.4 real, 486.3 MB
[runlim] sample:		11487.2 time, 2900.4 real, 499.3 MB
[runlim] sample:		11526.8 time, 2910.4 real, 505.3 MB
[runlim] sample:		11566.5 time, 2920.4 real, 511.5 MB
[runlim] sample:		11606.0 time, 2930.4 real, 518.0 MB
[runlim] sample:		11645.7 time, 2940.4 real, 527.5 MB
[runlim] sample:		11685.3 time, 2950.4 real, 531.5 MB
[runlim] sample:		11724.9 time, 2960.4 real, 387.7 MB
[runlim] sample:		11764.5 time, 2970.4 real, 420.7 MB
[runlim] sample:		11804.1 time, 2980.4 real, 428.9 MB
[runlim] sample:		11843.7 time, 2990.4 real, 433.1 MB
[runlim] sample:		11883.3 time, 3000.4 real, 440.9 MB
[runlim] sample:		11922.9 time, 3010.4 real, 448.9 MB
[runlim] sample:		11962.5 time, 3020.4 real, 457.1 MB
[runlim] sample:		12002.1 time, 3030.4 real, 461.1 MB
[runlim] sample:		12041.8 time, 3040.4 real, 465.1 MB
[runlim] sample:		12081.3 time, 3050.4 real, 469.1 MB
[runlim] sample:		12121.0 time, 3060.4 real, 473.4 MB
[runlim] sample:		12160.6 time, 3070.4 real, 477.4 MB
[runlim] sample:		12200.2 time, 3080.4 real, 481.4 MB
[runlim] sample:		12239.8 time, 3090.4 real, 485.4 MB
[runlim] sample:		12279.4 time, 3100.4 real, 489.4 MB
[runlim] sample:		12319.0 time, 3110.4 real, 491.4 MB
[runlim] sample:		12358.6 time, 3120.4 real, 495.4 MB
[runlim] sample:		12398.2 time, 3130.4 real, 499.6 MB
[runlim] sample:		12437.8 time, 3140.4 real, 503.6 MB
[runlim] sample:		12477.4 time, 3150.4 real, 507.6 MB
[runlim] sample:		12517.0 time, 3160.4 real, 509.6 MB
[runlim] sample:		12556.6 time, 3170.4 real, 388.4 MB
[runlim] sample:		12596.2 time, 3180.4 real, 423.7 MB
[runlim] sample:		12635.8 time, 3190.4 real, 431.7 MB
[runlim] sample:		12675.4 time, 3200.4 real, 439.7 MB
[runlim] sample:		12715.0 time, 3210.4 real, 449.9 MB
[runlim] sample:		12754.6 time, 3220.4 real, 457.9 MB
[runlim] sample:		12794.2 time, 3230.4 real, 465.9 MB
[runlim] sample:		12833.9 time, 3240.4 real, 469.7 MB
[runlim] sample:		12873.5 time, 3250.4 real, 475.9 MB
[runlim] sample:		12913.1 time, 3260.4 real, 483.9 MB
[runlim] sample:		12952.7 time, 3270.4 real, 490.2 MB
[runlim] sample:		12992.3 time, 3280.4 real, 494.2 MB
[runlim] sample:		13031.9 time, 3290.4 real, 500.2 MB
[runlim] sample:		13071.5 time, 3300.4 real, 506.2 MB
[runlim] sample:		13111.1 time, 3310.4 real, 510.2 MB
[runlim] sample:		13150.7 time, 3320.4 real, 514.2 MB
[runlim] sample:		13190.3 time, 3330.4 real, 518.1 MB
[runlim] sample:		13229.9 time, 3340.4 real, 522.4 MB
[runlim] sample:		13269.5 time, 3350.4 real, 526.4 MB
[runlim] sample:		13309.1 time, 3360.4 real, 530.4 MB
[runlim] sample:		13348.7 time, 3370.4 real, 532.4 MB
[runlim] sample:		13388.3 time, 3380.4 real, 536.4 MB
[runlim] sample:		13427.9 time, 3390.4 real, 389.2 MB
[runlim] sample:		13467.6 time, 3400.4 real, 422.2 MB
[runlim] sample:		13507.2 time, 3410.4 real, 430.7 MB
[runlim] sample:		13546.8 time, 3420.4 real, 436.7 MB
[runlim] sample:		13586.4 time, 3430.4 real, 444.5 MB
[runlim] sample:		13626.0 time, 3440.4 real, 450.7 MB
[runlim] sample:		13665.6 time, 3450.4 real, 454.7 MB
[runlim] sample:		13705.2 time, 3460.4 real, 462.7 MB
[runlim] sample:		13744.8 time, 3470.4 real, 466.7 MB
[runlim] sample:		13784.4 time, 3480.4 real, 472.4 MB
[runlim] sample:		13824.0 time, 3490.4 real, 476.9 MB
[runlim] sample:		13863.6 time, 3500.4 real, 482.9 MB
[runlim] sample:		13903.2 time, 3510.4 real, 486.9 MB
[runlim] sample:		13942.9 time, 3520.4 real, 490.9 MB
[runlim] sample:		13982.5 time, 3530.4 real, 494.9 MB
[runlim] sample:		14022.1 time, 3540.4 real, 498.9 MB
[runlim] sample:		14061.7 time, 3550.4 real, 502.9 MB
[runlim] sample:		14101.3 time, 3560.4 real, 505.2 MB
[runlim] sample:		14140.9 time, 3570.4 real, 509.2 MB
[runlim] sample:		14180.5 time, 3580.4 real, 513.2 MB
[runlim] sample:		14220.1 time, 3590.4 real, 515.2 MB
[runlim] end:			Sun Sep 20 04:44:58 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		143981
[runlim] real:			3600.07 seconds
[runlim] time:			14258.12 seconds
[runlim] space:			536.4 MB
[runlim] samples:		35996
