[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/hwmcc14/single/6s160.aig
[runlim] start:			Tue Sep 15 18:00:22 2015
[runlim] main pid:		26275
[runlim] sample:		36.4 time, 10.8 real, 209.9 MB
[runlim] sample:		76.0 time, 20.8 real, 227.1 MB
[runlim] sample:		115.5 time, 30.8 real, 247.1 MB
[runlim] sample:		155.0 time, 40.8 real, 255.6 MB
[runlim] sample:		194.6 time, 50.8 real, 262.7 MB
[runlim] sample:		234.2 time, 60.8 real, 281.0 MB
[runlim] sample:		273.7 time, 70.8 real, 302.1 MB
[runlim] sample:		313.3 time, 80.8 real, 302.2 MB
[runlim] sample:		352.8 time, 90.8 real, 308.8 MB
[runlim] sample:		392.3 time, 100.8 real, 326.0 MB
[runlim] sample:		431.9 time, 110.8 real, 316.4 MB
[runlim] sample:		471.4 time, 120.8 real, 318.8 MB
[runlim] sample:		510.9 time, 130.8 real, 323.3 MB
[runlim] sample:		550.5 time, 140.8 real, 326.2 MB
[runlim] sample:		590.0 time, 150.8 real, 328.8 MB
[runlim] sample:		629.5 time, 160.8 real, 331.0 MB
[runlim] sample:		669.1 time, 170.8 real, 333.0 MB
[runlim] sample:		708.6 time, 180.8 real, 333.2 MB
[runlim] sample:		748.1 time, 190.8 real, 333.2 MB
[runlim] sample:		787.7 time, 200.8 real, 339.2 MB
[runlim] sample:		827.2 time, 210.8 real, 339.9 MB
[runlim] sample:		866.8 time, 220.8 real, 377.0 MB
[runlim] sample:		906.4 time, 230.8 real, 363.5 MB
[runlim] sample:		946.0 time, 240.8 real, 363.8 MB
[runlim] sample:		985.5 time, 250.8 real, 363.8 MB
[runlim] sample:		1025.1 time, 260.8 real, 364.8 MB
[runlim] sample:		1064.6 time, 270.8 real, 366.8 MB
[runlim] sample:		1104.2 time, 280.8 real, 367.5 MB
[runlim] sample:		1143.7 time, 290.8 real, 367.5 MB
[runlim] sample:		1183.3 time, 300.8 real, 367.5 MB
[runlim] sample:		1222.8 time, 310.8 real, 373.2 MB
[runlim] sample:		1262.4 time, 320.8 real, 373.5 MB
[runlim] sample:		1301.9 time, 330.8 real, 375.5 MB
[runlim] sample:		1341.5 time, 340.8 real, 375.5 MB
[runlim] sample:		1381.0 time, 350.8 real, 376.5 MB
[runlim] sample:		1420.6 time, 360.8 real, 376.5 MB
[runlim] sample:		1460.1 time, 370.8 real, 378.3 MB
[runlim] sample:		1499.7 time, 380.8 real, 380.3 MB
[runlim] sample:		1539.2 time, 390.8 real, 380.8 MB
[runlim] sample:		1578.8 time, 400.8 real, 381.1 MB
[runlim] sample:		1618.3 time, 410.8 real, 381.1 MB
[runlim] sample:		1657.9 time, 420.8 real, 381.1 MB
[runlim] sample:		1697.5 time, 430.8 real, 381.1 MB
[runlim] sample:		1737.1 time, 440.8 real, 381.1 MB
[runlim] sample:		1776.7 time, 450.8 real, 381.3 MB
[runlim] sample:		1816.2 time, 460.8 real, 381.9 MB
[runlim] sample:		1855.8 time, 470.8 real, 384.4 MB
[runlim] sample:		1895.3 time, 480.8 real, 384.4 MB
[runlim] sample:		1934.9 time, 490.8 real, 385.7 MB
[runlim] sample:		1974.5 time, 500.8 real, 392.0 MB
[runlim] sample:		2014.0 time, 510.8 real, 395.2 MB
[runlim] sample:		2053.6 time, 520.8 real, 417.7 MB
[runlim] sample:		2093.1 time, 530.8 real, 417.7 MB
[runlim] sample:		2132.7 time, 540.8 real, 418.0 MB
[runlim] sample:		2172.2 time, 550.8 real, 418.2 MB
[runlim] sample:		2211.8 time, 560.8 real, 418.2 MB
[runlim] sample:		2251.3 time, 570.8 real, 418.5 MB
[runlim] sample:		2290.9 time, 580.8 real, 419.1 MB
[runlim] sample:		2330.4 time, 590.8 real, 419.4 MB
[runlim] sample:		2370.0 time, 600.8 real, 419.9 MB
[runlim] sample:		2409.5 time, 610.8 real, 420.1 MB
[runlim] sample:		2449.0 time, 620.8 real, 420.4 MB
[runlim] sample:		2488.6 time, 630.8 real, 422.6 MB
[runlim] sample:		2528.1 time, 640.8 real, 422.6 MB
[runlim] sample:		2567.6 time, 650.8 real, 423.2 MB
[runlim] sample:		2607.2 time, 660.8 real, 423.2 MB
[runlim] sample:		2646.8 time, 670.8 real, 423.2 MB
[runlim] sample:		2686.3 time, 680.8 real, 423.2 MB
[runlim] sample:		2725.8 time, 690.8 real, 423.2 MB
[runlim] sample:		2765.4 time, 700.8 real, 424.5 MB
[runlim] sample:		2804.9 time, 710.8 real, 425.3 MB
[runlim] sample:		2844.4 time, 720.8 real, 427.1 MB
[runlim] sample:		2883.9 time, 730.8 real, 429.1 MB
[runlim] sample:		2923.5 time, 740.8 real, 430.0 MB
[runlim] sample:		2963.0 time, 750.8 real, 448.9 MB
[runlim] sample:		3002.5 time, 760.8 real, 450.0 MB
[runlim] sample:		3042.1 time, 770.8 real, 451.5 MB
[runlim] sample:		3081.7 time, 780.8 real, 453.5 MB
[runlim] sample:		3121.2 time, 790.8 real, 453.8 MB
[runlim] sample:		3160.7 time, 800.8 real, 453.8 MB
[runlim] sample:		3200.3 time, 810.8 real, 455.8 MB
[runlim] sample:		3239.9 time, 820.8 real, 456.3 MB
[runlim] sample:		3279.4 time, 830.8 real, 456.3 MB
[runlim] sample:		3319.0 time, 840.8 real, 456.3 MB
[runlim] sample:		3358.5 time, 850.8 real, 456.3 MB
[runlim] sample:		3398.1 time, 860.8 real, 457.4 MB
[runlim] sample:		3437.7 time, 870.8 real, 459.7 MB
[runlim] sample:		3477.2 time, 880.8 real, 459.7 MB
[runlim] sample:		3516.8 time, 890.8 real, 459.7 MB
[runlim] sample:		3556.3 time, 900.8 real, 459.7 MB
[runlim] sample:		3595.9 time, 910.8 real, 459.7 MB
[runlim] sample:		3635.4 time, 920.8 real, 459.7 MB
[runlim] sample:		3675.0 time, 930.8 real, 459.7 MB
[runlim] sample:		3714.5 time, 940.8 real, 459.7 MB
[runlim] sample:		3754.1 time, 950.8 real, 462.0 MB
[runlim] sample:		3793.6 time, 960.8 real, 462.0 MB
[runlim] sample:		3833.2 time, 970.8 real, 462.0 MB
[runlim] sample:		3872.8 time, 980.8 real, 462.0 MB
[runlim] sample:		3912.3 time, 990.8 real, 462.0 MB
[runlim] sample:		3951.9 time, 1000.8 real, 462.0 MB
[runlim] sample:		3991.4 time, 1010.8 real, 462.0 MB
[runlim] sample:		4031.0 time, 1020.8 real, 462.0 MB
[runlim] sample:		4070.6 time, 1030.8 real, 462.2 MB
[runlim] sample:		4110.1 time, 1040.8 real, 464.2 MB
[runlim] sample:		4149.7 time, 1050.8 real, 464.2 MB
[runlim] sample:		4189.2 time, 1060.8 real, 464.2 MB
[runlim] sample:		4228.8 time, 1070.8 real, 464.4 MB
[runlim] sample:		4268.4 time, 1080.8 real, 464.4 MB
[runlim] sample:		4307.9 time, 1090.8 real, 464.4 MB
[runlim] sample:		4347.5 time, 1100.8 real, 464.4 MB
[runlim] sample:		4387.0 time, 1110.8 real, 464.7 MB
[runlim] sample:		4426.6 time, 1120.8 real, 464.7 MB
[runlim] sample:		4466.2 time, 1130.8 real, 464.7 MB
[runlim] sample:		4505.8 time, 1140.8 real, 464.7 MB
[runlim] sample:		4545.3 time, 1150.8 real, 466.7 MB
[runlim] sample:		4584.8 time, 1160.8 real, 466.7 MB
[runlim] sample:		4624.4 time, 1170.8 real, 466.7 MB
[runlim] sample:		4663.9 time, 1180.8 real, 466.7 MB
[runlim] sample:		4703.5 time, 1190.8 real, 467.0 MB
[runlim] sample:		4743.0 time, 1200.8 real, 467.0 MB
[runlim] sample:		4782.6 time, 1210.8 real, 467.0 MB
[runlim] sample:		4822.2 time, 1220.8 real, 467.0 MB
[runlim] sample:		4861.7 time, 1230.8 real, 467.0 MB
[runlim] sample:		4901.2 time, 1240.8 real, 467.0 MB
[runlim] sample:		4940.7 time, 1250.8 real, 467.0 MB
[runlim] sample:		4980.3 time, 1260.8 real, 467.0 MB
[runlim] sample:		5019.8 time, 1270.8 real, 467.2 MB
[runlim] sample:		5059.3 time, 1280.8 real, 472.2 MB
[runlim] sample:		5098.8 time, 1290.8 real, 474.0 MB
[runlim] sample:		5138.4 time, 1300.8 real, 474.3 MB
[runlim] sample:		5178.0 time, 1310.8 real, 474.8 MB
[runlim] sample:		5217.5 time, 1320.8 real, 477.0 MB
[runlim] sample:		5257.1 time, 1330.8 real, 478.3 MB
[runlim] sample:		5296.6 time, 1340.8 real, 485.1 MB
[runlim] sample:		5336.2 time, 1350.8 real, 479.9 MB
[runlim] sample:		5375.8 time, 1360.8 real, 479.9 MB
[runlim] sample:		5415.3 time, 1370.8 real, 483.2 MB
[runlim] sample:		5454.9 time, 1380.8 real, 483.2 MB
[runlim] sample:		5494.4 time, 1390.8 real, 483.2 MB
[runlim] sample:		5534.0 time, 1400.8 real, 483.2 MB
[runlim] sample:		5573.6 time, 1410.8 real, 483.2 MB
[runlim] sample:		5613.1 time, 1420.8 real, 483.4 MB
[runlim] sample:		5652.6 time, 1430.8 real, 483.6 MB
[runlim] sample:		5692.2 time, 1440.8 real, 490.4 MB
[runlim] sample:		5731.8 time, 1450.8 real, 490.4 MB
[runlim] sample:		5771.3 time, 1460.8 real, 490.4 MB
[runlim] sample:		5810.9 time, 1470.8 real, 490.4 MB
[runlim] sample:		5850.4 time, 1480.8 real, 490.4 MB
[runlim] sample:		5890.0 time, 1490.8 real, 490.4 MB
[runlim] sample:		5929.5 time, 1500.8 real, 490.4 MB
[runlim] sample:		5969.1 time, 1510.8 real, 490.9 MB
[runlim] sample:		6008.6 time, 1520.8 real, 490.9 MB
[runlim] sample:		6048.2 time, 1530.8 real, 491.1 MB
[runlim] sample:		6087.7 time, 1540.8 real, 491.1 MB
[runlim] sample:		6127.2 time, 1550.8 real, 491.4 MB
[runlim] sample:		6166.8 time, 1560.8 real, 494.2 MB
[runlim] sample:		6206.3 time, 1570.8 real, 494.4 MB
[runlim] sample:		6245.8 time, 1580.8 real, 494.4 MB
[runlim] sample:		6285.4 time, 1590.8 real, 495.4 MB
[runlim] sample:		6325.0 time, 1600.8 real, 495.4 MB
[runlim] sample:		6364.5 time, 1610.8 real, 495.7 MB
[runlim] sample:		6404.0 time, 1620.8 real, 496.5 MB
[runlim] sample:		6443.5 time, 1630.8 real, 498.5 MB
[runlim] sample:		6483.0 time, 1640.8 real, 498.5 MB
[runlim] sample:		6522.6 time, 1650.8 real, 498.5 MB
[runlim] sample:		6562.2 time, 1660.8 real, 498.5 MB
[runlim] sample:		6601.7 time, 1670.8 real, 498.8 MB
[runlim] sample:		6641.3 time, 1680.8 real, 498.8 MB
[runlim] sample:		6680.9 time, 1690.8 real, 498.8 MB
[runlim] sample:		6720.5 time, 1700.8 real, 499.0 MB
[runlim] sample:		6759.9 time, 1710.8 real, 499.0 MB
[runlim] sample:		6799.5 time, 1720.8 real, 499.0 MB
[runlim] sample:		6839.1 time, 1730.8 real, 501.0 MB
[runlim] sample:		6878.6 time, 1740.8 real, 501.0 MB
[runlim] sample:		6918.2 time, 1750.8 real, 501.3 MB
[runlim] sample:		6957.7 time, 1760.8 real, 501.5 MB
[runlim] sample:		6997.3 time, 1770.8 real, 502.0 MB
[runlim] sample:		7036.9 time, 1780.8 real, 502.0 MB
[runlim] sample:		7076.4 time, 1790.8 real, 502.0 MB
[runlim] sample:		7116.0 time, 1800.8 real, 577.2 MB
[runlim] sample:		7155.5 time, 1810.8 real, 559.0 MB
[runlim] sample:		7195.1 time, 1820.8 real, 561.0 MB
[runlim] sample:		7234.6 time, 1830.8 real, 561.3 MB
[runlim] sample:		7274.2 time, 1840.8 real, 561.3 MB
[runlim] sample:		7313.8 time, 1850.8 real, 561.3 MB
[runlim] sample:		7353.4 time, 1860.8 real, 561.3 MB
[runlim] sample:		7393.0 time, 1870.8 real, 561.3 MB
[runlim] sample:		7432.5 time, 1880.8 real, 561.3 MB
[runlim] sample:		7472.1 time, 1890.8 real, 561.3 MB
[runlim] sample:		7511.7 time, 1900.8 real, 561.3 MB
[runlim] sample:		7551.2 time, 1910.8 real, 561.6 MB
[runlim] sample:		7590.7 time, 1920.8 real, 561.6 MB
[runlim] sample:		7630.3 time, 1930.8 real, 563.6 MB
[runlim] sample:		7669.9 time, 1940.8 real, 563.6 MB
[runlim] sample:		7709.4 time, 1950.8 real, 563.6 MB
[runlim] sample:		7749.0 time, 1960.8 real, 563.6 MB
[runlim] sample:		7788.5 time, 1970.8 real, 563.8 MB
[runlim] sample:		7828.0 time, 1980.8 real, 563.8 MB
[runlim] sample:		7867.5 time, 1990.8 real, 564.1 MB
[runlim] sample:		7907.1 time, 2000.8 real, 564.1 MB
[runlim] sample:		7946.6 time, 2010.8 real, 564.1 MB
[runlim] sample:		7986.2 time, 2020.8 real, 564.1 MB
[runlim] sample:		8025.8 time, 2030.8 real, 564.6 MB
[runlim] sample:		8065.3 time, 2040.8 real, 578.3 MB
[runlim] sample:		8104.9 time, 2050.8 real, 580.3 MB
[runlim] sample:		8144.5 time, 2060.8 real, 580.3 MB
[runlim] sample:		8184.0 time, 2070.8 real, 580.6 MB
[runlim] sample:		8223.5 time, 2080.8 real, 580.6 MB
[runlim] sample:		8263.1 time, 2090.8 real, 582.6 MB
[runlim] sample:		8302.6 time, 2100.8 real, 582.6 MB
[runlim] sample:		8342.2 time, 2110.8 real, 582.6 MB
[runlim] sample:		8381.8 time, 2120.8 real, 582.6 MB
[runlim] sample:		8421.3 time, 2130.8 real, 584.6 MB
[runlim] sample:		8460.8 time, 2140.8 real, 584.6 MB
[runlim] sample:		8500.4 time, 2150.8 real, 584.8 MB
[runlim] sample:		8539.9 time, 2160.8 real, 584.8 MB
[runlim] sample:		8579.4 time, 2170.8 real, 584.8 MB
[runlim] sample:		8619.0 time, 2180.8 real, 586.8 MB
[runlim] sample:		8658.5 time, 2190.8 real, 586.8 MB
[runlim] sample:		8698.0 time, 2200.8 real, 586.8 MB
[runlim] sample:		8737.5 time, 2210.8 real, 586.8 MB
[runlim] sample:		8777.1 time, 2220.8 real, 586.8 MB
[runlim] sample:		8816.7 time, 2230.8 real, 587.1 MB
[runlim] sample:		8856.2 time, 2240.8 real, 587.1 MB
[runlim] sample:		8895.7 time, 2250.8 real, 587.1 MB
[runlim] sample:		8935.3 time, 2260.8 real, 587.1 MB
[runlim] sample:		8974.8 time, 2270.8 real, 589.1 MB
[runlim] sample:		9014.4 time, 2280.8 real, 589.1 MB
[runlim] sample:		9054.0 time, 2290.8 real, 589.1 MB
[runlim] sample:		9093.5 time, 2300.8 real, 593.2 MB
[runlim] sample:		9133.1 time, 2310.8 real, 594.1 MB
[runlim] sample:		9172.6 time, 2320.8 real, 594.1 MB
[runlim] sample:		9212.2 time, 2330.8 real, 594.1 MB
[runlim] sample:		9251.7 time, 2340.8 real, 595.2 MB
[runlim] sample:		9291.3 time, 2350.8 real, 596.9 MB
[runlim] sample:		9330.8 time, 2360.8 real, 598.9 MB
[runlim] sample:		9370.4 time, 2370.8 real, 598.9 MB
[runlim] sample:		9409.9 time, 2380.8 real, 598.9 MB
[runlim] sample:		9449.5 time, 2390.8 real, 599.2 MB
[runlim] sample:		9489.1 time, 2400.8 real, 599.2 MB
[runlim] sample:		9528.6 time, 2410.8 real, 599.2 MB
[runlim] sample:		9568.2 time, 2420.8 real, 599.2 MB
[runlim] sample:		9607.7 time, 2430.8 real, 599.2 MB
[runlim] sample:		9647.3 time, 2440.8 real, 599.2 MB
[runlim] sample:		9686.8 time, 2450.8 real, 599.2 MB
[runlim] sample:		9726.4 time, 2460.8 real, 599.2 MB
[runlim] sample:		9765.9 time, 2470.8 real, 601.6 MB
[runlim] sample:		9805.5 time, 2480.8 real, 601.8 MB
[runlim] sample:		9845.0 time, 2490.8 real, 601.8 MB
[runlim] sample:		9884.6 time, 2500.8 real, 601.8 MB
[runlim] sample:		9924.1 time, 2510.8 real, 601.8 MB
[runlim] sample:		9963.7 time, 2520.8 real, 601.8 MB
[runlim] sample:		10003.2 time, 2530.8 real, 601.8 MB
[runlim] sample:		10042.8 time, 2540.8 real, 601.8 MB
[runlim] sample:		10082.4 time, 2550.8 real, 601.8 MB
[runlim] sample:		10121.9 time, 2560.8 real, 602.1 MB
[runlim] sample:		10161.5 time, 2570.8 real, 604.1 MB
[runlim] sample:		10201.1 time, 2580.8 real, 604.1 MB
[runlim] sample:		10240.7 time, 2590.8 real, 604.1 MB
[runlim] sample:		10280.2 time, 2600.8 real, 604.1 MB
[runlim] sample:		10319.8 time, 2610.8 real, 604.1 MB
[runlim] sample:		10359.3 time, 2620.8 real, 604.1 MB
[runlim] sample:		10398.9 time, 2630.8 real, 604.1 MB
[runlim] sample:		10438.4 time, 2640.8 real, 604.3 MB
[runlim] sample:		10478.0 time, 2650.8 real, 604.3 MB
[runlim] sample:		10517.6 time, 2660.8 real, 604.3 MB
[runlim] sample:		10557.2 time, 2670.8 real, 604.3 MB
[runlim] sample:		10596.6 time, 2680.8 real, 604.3 MB
[runlim] sample:		10636.2 time, 2690.8 real, 606.3 MB
[runlim] sample:		10675.8 time, 2700.8 real, 606.3 MB
[runlim] sample:		10715.3 time, 2710.8 real, 606.3 MB
[runlim] sample:		10754.8 time, 2720.8 real, 606.6 MB
[runlim] sample:		10794.4 time, 2730.8 real, 606.6 MB
[runlim] sample:		10833.9 time, 2740.8 real, 606.6 MB
[runlim] sample:		10873.5 time, 2750.8 real, 606.6 MB
[runlim] sample:		10913.0 time, 2760.8 real, 606.6 MB
[runlim] sample:		10952.6 time, 2770.8 real, 606.6 MB
[runlim] sample:		10992.1 time, 2780.8 real, 606.6 MB
[runlim] sample:		11031.7 time, 2790.8 real, 606.6 MB
[runlim] sample:		11071.2 time, 2800.8 real, 606.8 MB
[runlim] sample:		11110.8 time, 2810.8 real, 606.8 MB
[runlim] sample:		11150.3 time, 2820.8 real, 606.8 MB
[runlim] sample:		11189.9 time, 2830.8 real, 606.8 MB
[runlim] sample:		11229.4 time, 2840.8 real, 606.8 MB
[runlim] sample:		11269.0 time, 2850.8 real, 608.8 MB
[runlim] sample:		11308.5 time, 2860.8 real, 608.8 MB
[runlim] sample:		11348.1 time, 2870.8 real, 608.8 MB
[runlim] sample:		11387.6 time, 2880.8 real, 609.1 MB
[runlim] sample:		11427.1 time, 2890.8 real, 609.1 MB
[runlim] sample:		11466.7 time, 2900.8 real, 609.1 MB
[runlim] sample:		11506.2 time, 2910.8 real, 609.1 MB
[runlim] sample:		11545.8 time, 2920.8 real, 609.1 MB
[runlim] sample:		11585.4 time, 2930.8 real, 609.5 MB
[runlim] sample:		11624.9 time, 2940.8 real, 609.5 MB
[runlim] sample:		11664.5 time, 2950.8 real, 609.5 MB
[runlim] sample:		11704.1 time, 2960.8 real, 609.8 MB
[runlim] sample:		11743.7 time, 2970.8 real, 609.8 MB
[runlim] sample:		11783.2 time, 2980.8 real, 609.8 MB
[runlim] sample:		11822.8 time, 2990.8 real, 611.8 MB
[runlim] sample:		11862.3 time, 3000.8 real, 611.8 MB
[runlim] sample:		11901.9 time, 3010.8 real, 611.8 MB
[runlim] sample:		11941.4 time, 3020.8 real, 611.8 MB
[runlim] sample:		11981.0 time, 3030.8 real, 611.8 MB
[runlim] sample:		12020.5 time, 3040.8 real, 611.8 MB
[runlim] sample:		12060.1 time, 3050.8 real, 612.1 MB
[runlim] sample:		12099.6 time, 3060.8 real, 612.1 MB
[runlim] sample:		12139.2 time, 3070.8 real, 612.8 MB
[runlim] sample:		12178.7 time, 3080.8 real, 613.1 MB
[runlim] sample:		12218.2 time, 3090.8 real, 613.1 MB
[runlim] sample:		12257.8 time, 3100.8 real, 614.8 MB
[runlim] sample:		12297.3 time, 3110.8 real, 614.8 MB
[runlim] sample:		12336.9 time, 3120.8 real, 616.8 MB
[runlim] sample:		12376.4 time, 3130.8 real, 617.1 MB
[runlim] sample:		12416.0 time, 3140.8 real, 617.1 MB
[runlim] sample:		12455.5 time, 3150.8 real, 617.1 MB
[runlim] sample:		12495.1 time, 3160.8 real, 617.1 MB
[runlim] sample:		12534.6 time, 3170.8 real, 617.1 MB
[runlim] sample:		12574.2 time, 3180.8 real, 617.1 MB
[runlim] sample:		12613.8 time, 3190.8 real, 617.1 MB
[runlim] sample:		12653.3 time, 3200.8 real, 617.1 MB
[runlim] sample:		12692.9 time, 3210.8 real, 617.4 MB
[runlim] sample:		12732.4 time, 3220.8 real, 617.4 MB
[runlim] sample:		12771.9 time, 3230.8 real, 617.4 MB
[runlim] sample:		12811.5 time, 3240.8 real, 617.4 MB
[runlim] sample:		12851.0 time, 3250.8 real, 617.4 MB
[runlim] sample:		12890.6 time, 3260.8 real, 619.4 MB
[runlim] sample:		12930.1 time, 3270.8 real, 619.4 MB
[runlim] sample:		12969.7 time, 3280.8 real, 619.4 MB
[runlim] sample:		13009.2 time, 3290.8 real, 619.6 MB
[runlim] sample:		13048.8 time, 3300.8 real, 619.6 MB
[runlim] sample:		13088.3 time, 3310.8 real, 619.6 MB
[runlim] sample:		13127.9 time, 3320.8 real, 619.6 MB
[runlim] sample:		13167.4 time, 3330.8 real, 619.6 MB
[runlim] sample:		13207.0 time, 3340.8 real, 619.6 MB
[runlim] sample:		13246.5 time, 3350.8 real, 619.6 MB
[runlim] sample:		13286.1 time, 3360.8 real, 619.6 MB
[runlim] sample:		13325.7 time, 3370.8 real, 619.9 MB
[runlim] sample:		13365.2 time, 3380.8 real, 529.6 MB
[runlim] sample:		13404.7 time, 3390.8 real, 532.6 MB
[runlim] sample:		13444.3 time, 3400.8 real, 532.6 MB
[runlim] sample:		13483.8 time, 3410.8 real, 532.6 MB
[runlim] sample:		13523.4 time, 3420.8 real, 534.6 MB
[runlim] sample:		13562.9 time, 3430.8 real, 534.6 MB
[runlim] sample:		13602.5 time, 3440.8 real, 534.6 MB
[runlim] sample:		13642.1 time, 3450.8 real, 536.9 MB
[runlim] sample:		13681.6 time, 3460.8 real, 536.9 MB
[runlim] sample:		13721.2 time, 3470.8 real, 537.4 MB
[runlim] sample:		13760.7 time, 3480.8 real, 538.4 MB
[runlim] sample:		13800.3 time, 3490.8 real, 613.9 MB
[runlim] sample:		13839.8 time, 3500.8 real, 664.9 MB
[runlim] sample:		13879.4 time, 3510.8 real, 609.3 MB
[runlim] sample:		13919.0 time, 3520.8 real, 611.8 MB
[runlim] sample:		13958.5 time, 3530.8 real, 611.8 MB
[runlim] sample:		13998.1 time, 3540.8 real, 612.1 MB
[runlim] sample:		14037.6 time, 3550.8 real, 614.1 MB
[runlim] sample:		14077.2 time, 3560.8 real, 614.1 MB
[runlim] sample:		14116.7 time, 3570.8 real, 614.1 MB
[runlim] sample:		14156.3 time, 3580.8 real, 614.1 MB
[runlim] sample:		14195.8 time, 3590.8 real, 614.1 MB
[runlim] end:			Tue Sep 15 19:00:22 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		143942
[runlim] real:			3600.11 seconds
[runlim] time:			14232.63 seconds
[runlim] space:			686.6 MB
[runlim] samples:		35993
