[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/beemextnc1f1.aig
[runlim] start:			Sat Sep 19 20:42:38 2015
[runlim] main pid:		10897
[runlim] sample:		39.0 time, 10.3 real, 164.6 MB
[runlim] sample:		78.5 time, 20.3 real, 183.3 MB
[runlim] sample:		118.2 time, 30.3 real, 203.3 MB
[runlim] sample:		157.8 time, 40.3 real, 217.0 MB
[runlim] sample:		197.4 time, 50.3 real, 228.7 MB
[runlim] sample:		237.0 time, 60.3 real, 235.4 MB
[runlim] sample:		276.7 time, 70.3 real, 192.0 MB
[runlim] sample:		316.3 time, 80.3 real, 205.5 MB
[runlim] sample:		355.9 time, 90.3 real, 213.8 MB
[runlim] sample:		395.5 time, 100.3 real, 224.1 MB
[runlim] sample:		435.1 time, 110.3 real, 236.7 MB
[runlim] sample:		474.7 time, 120.3 real, 245.2 MB
[runlim] sample:		514.3 time, 130.3 real, 261.5 MB
[runlim] sample:		553.9 time, 140.3 real, 274.6 MB
[runlim] sample:		593.5 time, 150.3 real, 284.6 MB
[runlim] sample:		633.1 time, 160.3 real, 294.6 MB
[runlim] sample:		672.7 time, 170.3 real, 303.6 MB
[runlim] sample:		712.3 time, 180.3 real, 212.2 MB
[runlim] sample:		751.9 time, 190.3 real, 225.8 MB
[runlim] sample:		791.5 time, 200.3 real, 237.6 MB
[runlim] sample:		831.0 time, 210.3 real, 246.2 MB
[runlim] sample:		870.6 time, 220.3 real, 255.9 MB
[runlim] sample:		910.2 time, 230.3 real, 263.9 MB
[runlim] sample:		949.8 time, 240.3 real, 270.9 MB
[runlim] sample:		989.4 time, 250.3 real, 277.7 MB
[runlim] sample:		1028.9 time, 260.3 real, 225.5 MB
[runlim] sample:		1068.5 time, 270.3 real, 235.8 MB
[runlim] sample:		1108.1 time, 280.3 real, 247.8 MB
[runlim] sample:		1147.7 time, 290.3 real, 260.2 MB
[runlim] sample:		1187.3 time, 300.3 real, 270.5 MB
[runlim] sample:		1226.9 time, 310.3 real, 280.8 MB
[runlim] sample:		1266.4 time, 320.3 real, 291.0 MB
[runlim] sample:		1306.0 time, 330.3 real, 299.5 MB
[runlim] sample:		1345.6 time, 340.3 real, 309.8 MB
[runlim] sample:		1385.2 time, 350.3 real, 315.6 MB
[runlim] sample:		1424.7 time, 360.3 real, 322.6 MB
[runlim] sample:		1464.3 time, 370.3 real, 329.4 MB
[runlim] sample:		1503.9 time, 380.3 real, 335.6 MB
[runlim] sample:		1543.4 time, 390.3 real, 342.1 MB
[runlim] sample:		1583.0 time, 400.3 real, 347.5 MB
[runlim] sample:		1622.6 time, 410.3 real, 355.5 MB
[runlim] sample:		1662.2 time, 420.3 real, 362.5 MB
[runlim] sample:		1701.8 time, 430.3 real, 367.2 MB
[runlim] sample:		1741.3 time, 440.3 real, 371.7 MB
[runlim] sample:		1780.9 time, 450.3 real, 223.5 MB
[runlim] sample:		1820.5 time, 460.3 real, 235.3 MB
[runlim] sample:		1860.1 time, 470.3 real, 247.4 MB
[runlim] sample:		1899.6 time, 480.3 real, 255.4 MB
[runlim] sample:		1939.2 time, 490.3 real, 263.4 MB
[runlim] sample:		1978.8 time, 500.3 real, 269.7 MB
[runlim] sample:		2018.4 time, 510.3 real, 276.2 MB
[runlim] sample:		2058.0 time, 520.3 real, 284.5 MB
[runlim] sample:		2097.5 time, 530.3 real, 291.0 MB
[runlim] sample:		2137.1 time, 540.3 real, 295.5 MB
[runlim] sample:		2176.7 time, 550.3 real, 300.0 MB
[runlim] sample:		2216.3 time, 560.3 real, 306.6 MB
[runlim] sample:		2255.9 time, 570.3 real, 312.9 MB
[runlim] sample:		2295.5 time, 580.3 real, 317.1 MB
[runlim] sample:		2335.1 time, 590.3 real, 322.1 MB
[runlim] sample:		2374.6 time, 600.3 real, 324.1 MB
[runlim] sample:		2414.2 time, 610.3 real, 231.6 MB
[runlim] sample:		2453.8 time, 620.3 real, 248.4 MB
[runlim] sample:		2493.5 time, 630.3 real, 260.9 MB
[runlim] sample:		2533.0 time, 640.3 real, 271.2 MB
[runlim] sample:		2572.6 time, 650.3 real, 281.2 MB
[runlim] sample:		2612.1 time, 660.3 real, 289.5 MB
[runlim] sample:		2651.7 time, 670.3 real, 298.0 MB
[runlim] sample:		2691.3 time, 680.3 real, 304.5 MB
[runlim] sample:		2730.8 time, 690.3 real, 316.8 MB
[runlim] sample:		2770.4 time, 700.3 real, 315.4 MB
[runlim] sample:		2809.9 time, 710.3 real, 323.6 MB
[runlim] sample:		2849.5 time, 720.3 real, 331.6 MB
[runlim] sample:		2889.1 time, 730.3 real, 335.6 MB
[runlim] sample:		2928.6 time, 740.3 real, 339.6 MB
[runlim] sample:		2968.2 time, 750.3 real, 346.1 MB
[runlim] sample:		3007.7 time, 760.3 real, 354.1 MB
[runlim] sample:		3047.3 time, 770.3 real, 359.6 MB
[runlim] sample:		3086.9 time, 780.3 real, 363.6 MB
[runlim] sample:		3126.4 time, 790.3 real, 365.6 MB
[runlim] sample:		3166.0 time, 800.3 real, 369.9 MB
[runlim] sample:		3205.5 time, 810.3 real, 372.1 MB
[runlim] sample:		3245.1 time, 820.3 real, 253.3 MB
[runlim] sample:		3284.6 time, 830.3 real, 265.3 MB
[runlim] sample:		3324.2 time, 840.3 real, 275.6 MB
[runlim] sample:		3363.7 time, 850.3 real, 283.9 MB
[runlim] sample:		3403.3 time, 860.3 real, 289.9 MB
[runlim] sample:		3442.9 time, 870.3 real, 297.9 MB
[runlim] sample:		3482.4 time, 880.3 real, 303.9 MB
[runlim] sample:		3522.0 time, 890.3 real, 308.1 MB
[runlim] sample:		3561.5 time, 900.3 real, 312.1 MB
[runlim] sample:		3601.0 time, 910.3 real, 318.1 MB
[runlim] sample:		3640.5 time, 920.3 real, 322.4 MB
[runlim] sample:		3680.1 time, 930.3 real, 326.6 MB
[runlim] sample:		3719.7 time, 940.3 real, 331.7 MB
[runlim] sample:		3759.2 time, 950.3 real, 336.5 MB
[runlim] sample:		3798.8 time, 960.3 real, 340.5 MB
[runlim] sample:		3838.4 time, 970.3 real, 345.0 MB
[runlim] sample:		3877.9 time, 980.3 real, 349.2 MB
[runlim] sample:		3917.5 time, 990.3 real, 351.2 MB
[runlim] sample:		3957.0 time, 1000.3 real, 252.9 MB
[runlim] sample:		3996.6 time, 1010.3 real, 265.5 MB
[runlim] sample:		4036.2 time, 1020.3 real, 272.0 MB
[runlim] sample:		4075.7 time, 1030.3 real, 283.5 MB
[runlim] sample:		4115.2 time, 1040.3 real, 291.5 MB
[runlim] sample:		4154.8 time, 1050.3 real, 297.5 MB
[runlim] sample:		4194.3 time, 1060.3 real, 306.0 MB
[runlim] sample:		4233.9 time, 1070.3 real, 312.0 MB
[runlim] sample:		4273.5 time, 1080.3 real, 316.0 MB
[runlim] sample:		4313.0 time, 1090.3 real, 322.2 MB
[runlim] sample:		4352.5 time, 1100.3 real, 326.5 MB
[runlim] sample:		4392.1 time, 1110.3 real, 330.7 MB
[runlim] sample:		4431.6 time, 1120.3 real, 337.0 MB
[runlim] sample:		4471.2 time, 1130.3 real, 343.0 MB
[runlim] sample:		4510.7 time, 1140.3 real, 349.5 MB
[runlim] sample:		4550.3 time, 1150.3 real, 351.7 MB
[runlim] sample:		4589.9 time, 1160.3 real, 354.5 MB
[runlim] sample:		4629.5 time, 1170.3 real, 358.0 MB
[runlim] sample:		4669.0 time, 1180.3 real, 360.4 MB
[runlim] sample:		4708.6 time, 1190.3 real, 364.9 MB
[runlim] sample:		4748.1 time, 1200.3 real, 259.6 MB
[runlim] sample:		4787.7 time, 1210.3 real, 271.8 MB
[runlim] sample:		4827.3 time, 1220.3 real, 279.8 MB
[runlim] sample:		4866.8 time, 1230.3 real, 290.3 MB
[runlim] sample:		4906.4 time, 1240.3 real, 298.3 MB
[runlim] sample:		4945.9 time, 1250.3 real, 306.3 MB
[runlim] sample:		4985.5 time, 1260.3 real, 312.4 MB
[runlim] sample:		5025.0 time, 1270.3 real, 318.6 MB
[runlim] sample:		5064.6 time, 1280.3 real, 324.8 MB
[runlim] sample:		5104.1 time, 1290.3 real, 330.8 MB
[runlim] sample:		5143.7 time, 1300.3 real, 336.8 MB
[runlim] sample:		5183.2 time, 1310.3 real, 343.1 MB
[runlim] sample:		5222.8 time, 1320.3 real, 347.1 MB
[runlim] sample:		5262.4 time, 1330.3 real, 353.6 MB
[runlim] sample:		5302.0 time, 1340.3 real, 358.6 MB
[runlim] sample:		5341.5 time, 1350.3 real, 364.2 MB
[runlim] sample:		5381.1 time, 1360.3 real, 370.2 MB
[runlim] sample:		5420.6 time, 1370.3 real, 374.4 MB
[runlim] sample:		5460.2 time, 1380.3 real, 380.4 MB
[runlim] sample:		5499.7 time, 1390.3 real, 382.4 MB
[runlim] sample:		5539.3 time, 1400.3 real, 388.9 MB
[runlim] sample:		5578.9 time, 1410.3 real, 392.9 MB
[runlim] sample:		5618.4 time, 1420.3 real, 397.1 MB
[runlim] sample:		5657.9 time, 1430.3 real, 401.4 MB
[runlim] sample:		5697.5 time, 1440.3 real, 405.6 MB
[runlim] sample:		5737.1 time, 1450.3 real, 409.9 MB
[runlim] sample:		5776.6 time, 1460.3 real, 411.9 MB
[runlim] sample:		5816.2 time, 1470.3 real, 416.1 MB
[runlim] sample:		5855.8 time, 1480.3 real, 420.4 MB
[runlim] sample:		5895.4 time, 1490.3 real, 422.9 MB
[runlim] sample:		5934.9 time, 1500.3 real, 427.4 MB
[runlim] sample:		5974.6 time, 1510.3 real, 429.6 MB
[runlim] sample:		6014.1 time, 1520.3 real, 280.0 MB
[runlim] sample:		6053.7 time, 1530.3 real, 292.0 MB
[runlim] sample:		6093.3 time, 1540.3 real, 300.3 MB
[runlim] sample:		6132.8 time, 1550.3 real, 314.3 MB
[runlim] sample:		6172.4 time, 1560.3 real, 322.0 MB
[runlim] sample:		6211.9 time, 1570.3 real, 332.5 MB
[runlim] sample:		6251.5 time, 1580.3 real, 340.5 MB
[runlim] sample:		6291.0 time, 1590.3 real, 474.4 MB
[runlim] sample:		6330.6 time, 1600.3 real, 435.7 MB
[runlim] sample:		6370.1 time, 1610.3 real, 441.7 MB
[runlim] sample:		6409.7 time, 1620.3 real, 448.0 MB
[runlim] sample:		6449.2 time, 1630.3 real, 453.9 MB
[runlim] sample:		6488.8 time, 1640.3 real, 459.9 MB
[runlim] sample:		6528.3 time, 1650.3 real, 467.9 MB
[runlim] sample:		6567.9 time, 1660.3 real, 473.0 MB
[runlim] sample:		6607.4 time, 1670.3 real, 485.0 MB
[runlim] sample:		6646.9 time, 1680.3 real, 489.0 MB
[runlim] sample:		6686.5 time, 1690.3 real, 495.0 MB
[runlim] sample:		6726.1 time, 1700.3 real, 499.3 MB
[runlim] sample:		6765.7 time, 1710.3 real, 503.3 MB
[runlim] sample:		6805.2 time, 1720.3 real, 505.3 MB
[runlim] sample:		6844.8 time, 1730.3 real, 509.3 MB
[runlim] sample:		6884.3 time, 1740.3 real, 513.3 MB
[runlim] sample:		6923.9 time, 1750.3 real, 515.5 MB
[runlim] sample:		6963.4 time, 1760.3 real, 519.7 MB
[runlim] sample:		7003.0 time, 1770.3 real, 523.7 MB
[runlim] sample:		7042.6 time, 1780.3 real, 527.7 MB
[runlim] sample:		7082.1 time, 1790.3 real, 530.4 MB
[runlim] sample:		7121.7 time, 1800.3 real, 534.9 MB
[runlim] sample:		7161.2 time, 1810.3 real, 537.4 MB
[runlim] sample:		7200.8 time, 1820.3 real, 541.1 MB
[runlim] sample:		7240.3 time, 1830.3 real, 546.7 MB
[runlim] sample:		7279.8 time, 1840.3 real, 549.7 MB
[runlim] sample:		7319.4 time, 1850.3 real, 552.6 MB
[runlim] sample:		7359.0 time, 1860.3 real, 558.0 MB
[runlim] sample:		7398.6 time, 1870.3 real, 561.6 MB
[runlim] sample:		7438.1 time, 1880.3 real, 563.8 MB
[runlim] sample:		7477.7 time, 1890.3 real, 567.1 MB
[runlim] sample:		7517.3 time, 1900.3 real, 386.0 MB
[runlim] sample:		7556.9 time, 1910.3 real, 393.8 MB
[runlim] sample:		7596.4 time, 1920.3 real, 405.1 MB
[runlim] sample:		7636.0 time, 1930.3 real, 413.6 MB
[runlim] sample:		7675.6 time, 1940.3 real, 421.4 MB
[runlim] sample:		7715.2 time, 1950.3 real, 429.7 MB
[runlim] sample:		7754.7 time, 1960.3 real, 435.9 MB
[runlim] sample:		7794.3 time, 1970.3 real, 439.9 MB
[runlim] sample:		7833.9 time, 1980.3 real, 446.1 MB
[runlim] sample:		7873.5 time, 1990.3 real, 450.1 MB
[runlim] sample:		7913.1 time, 2000.3 real, 454.1 MB
[runlim] sample:		7952.6 time, 2010.3 real, 458.4 MB
[runlim] sample:		7992.1 time, 2020.3 real, 464.4 MB
[runlim] sample:		8031.7 time, 2030.3 real, 468.4 MB
[runlim] sample:		8071.3 time, 2040.3 real, 473.2 MB
[runlim] sample:		8110.9 time, 2050.3 real, 477.8 MB
[runlim] sample:		8150.4 time, 2060.3 real, 481.8 MB
[runlim] sample:		8190.1 time, 2070.3 real, 483.8 MB
[runlim] sample:		8229.6 time, 2080.3 real, 488.0 MB
[runlim] sample:		8269.2 time, 2090.3 real, 494.2 MB
[runlim] sample:		8308.8 time, 2100.3 real, 498.5 MB
[runlim] sample:		8348.4 time, 2110.3 real, 504.5 MB
[runlim] sample:		8387.9 time, 2120.3 real, 506.5 MB
[runlim] sample:		8427.5 time, 2130.3 real, 510.5 MB
[runlim] sample:		8467.0 time, 2140.3 real, 512.8 MB
[runlim] sample:		8506.6 time, 2150.3 real, 517.0 MB
[runlim] sample:		8546.1 time, 2160.3 real, 519.2 MB
[runlim] sample:		8585.7 time, 2170.3 real, 523.2 MB
[runlim] sample:		8625.3 time, 2180.3 real, 525.5 MB
[runlim] sample:		8664.8 time, 2190.3 real, 529.5 MB
[runlim] sample:		8704.3 time, 2200.3 real, 531.7 MB
[runlim] sample:		8743.9 time, 2210.3 real, 535.9 MB
[runlim] sample:		8783.5 time, 2220.3 real, 539.9 MB
[runlim] sample:		8823.0 time, 2230.3 real, 544.2 MB
[runlim] sample:		8862.5 time, 2240.3 real, 548.2 MB
[runlim] sample:		8902.1 time, 2250.3 real, 551.2 MB
[runlim] sample:		8941.6 time, 2260.3 real, 556.4 MB
[runlim] sample:		8981.2 time, 2270.3 real, 561.7 MB
[runlim] sample:		9020.7 time, 2280.3 real, 563.7 MB
[runlim] sample:		9060.2 time, 2290.3 real, 567.7 MB
[runlim] sample:		9099.8 time, 2300.3 real, 569.7 MB
[runlim] sample:		9139.4 time, 2310.3 real, 573.7 MB
[runlim] sample:		9178.9 time, 2320.3 real, 576.2 MB
[runlim] sample:		9218.5 time, 2330.3 real, 578.2 MB
[runlim] sample:		9258.0 time, 2340.3 real, 582.7 MB
[runlim] sample:		9297.5 time, 2350.3 real, 585.2 MB
[runlim] sample:		9337.1 time, 2360.3 real, 587.7 MB
[runlim] sample:		9376.6 time, 2370.3 real, 592.0 MB
[runlim] sample:		9416.2 time, 2380.3 real, 594.0 MB
[runlim] sample:		9455.7 time, 2390.3 real, 598.0 MB
[runlim] sample:		9495.3 time, 2400.3 real, 600.8 MB
[runlim] sample:		9534.8 time, 2410.3 real, 603.3 MB
[runlim] sample:		9574.4 time, 2420.3 real, 607.5 MB
[runlim] sample:		9613.9 time, 2430.3 real, 609.5 MB
[runlim] sample:		9653.4 time, 2440.3 real, 611.5 MB
[runlim] sample:		9692.9 time, 2450.3 real, 613.8 MB
[runlim] sample:		9732.5 time, 2460.3 real, 616.0 MB
[runlim] sample:		9772.0 time, 2470.3 real, 620.3 MB
[runlim] sample:		9811.6 time, 2480.3 real, 624.3 MB
[runlim] sample:		9851.2 time, 2490.3 real, 626.8 MB
[runlim] sample:		9890.7 time, 2500.3 real, 629.5 MB
[runlim] sample:		9930.3 time, 2510.3 real, 631.5 MB
[runlim] sample:		9969.9 time, 2520.3 real, 635.5 MB
[runlim] sample:		10009.4 time, 2530.3 real, 635.5 MB
[runlim] sample:		10049.0 time, 2540.3 real, 639.8 MB
[runlim] sample:		10088.6 time, 2550.3 real, 642.3 MB
[runlim] sample:		10128.1 time, 2560.3 real, 644.3 MB
[runlim] sample:		10167.7 time, 2570.3 real, 646.5 MB
[runlim] sample:		10207.3 time, 2580.3 real, 648.8 MB
[runlim] sample:		10246.8 time, 2590.3 real, 651.8 MB
[runlim] sample:		10286.4 time, 2600.3 real, 653.8 MB
[runlim] sample:		10326.0 time, 2610.3 real, 658.4 MB
[runlim] sample:		10365.5 time, 2620.3 real, 660.6 MB
[runlim] sample:		10405.1 time, 2630.3 real, 662.9 MB
[runlim] sample:		10444.7 time, 2640.3 real, 664.9 MB
[runlim] sample:		10484.3 time, 2650.3 real, 666.9 MB
[runlim] sample:		10523.8 time, 2660.3 real, 666.9 MB
[runlim] sample:		10563.4 time, 2670.3 real, 669.9 MB
[runlim] sample:		10603.0 time, 2680.3 real, 672.7 MB
[runlim] sample:		10642.5 time, 2690.3 real, 672.7 MB
[runlim] sample:		10682.1 time, 2700.3 real, 674.7 MB
[runlim] sample:		10721.7 time, 2710.3 real, 676.7 MB
[runlim] sample:		10761.3 time, 2720.3 real, 676.9 MB
[runlim] sample:		10800.9 time, 2730.3 real, 678.9 MB
[runlim] sample:		10840.5 time, 2740.3 real, 678.9 MB
[runlim] sample:		10880.0 time, 2750.3 real, 680.9 MB
[runlim] sample:		10919.6 time, 2760.3 real, 681.2 MB
[runlim] sample:		10959.1 time, 2770.3 real, 401.5 MB
[runlim] sample:		10998.7 time, 2780.3 real, 413.3 MB
[runlim] sample:		11038.3 time, 2790.3 real, 423.5 MB
[runlim] sample:		11077.9 time, 2800.3 real, 429.5 MB
[runlim] sample:		11117.5 time, 2810.3 real, 435.8 MB
[runlim] sample:		11157.0 time, 2820.3 real, 441.6 MB
[runlim] sample:		11196.6 time, 2830.3 real, 449.8 MB
[runlim] sample:		11236.1 time, 2840.3 real, 455.8 MB
[runlim] sample:		11275.7 time, 2850.3 real, 463.9 MB
[runlim] sample:		11315.2 time, 2860.3 real, 469.9 MB
[runlim] sample:		11354.8 time, 2870.3 real, 476.1 MB
[runlim] sample:		11394.4 time, 2880.3 real, 484.1 MB
[runlim] sample:		11434.0 time, 2890.3 real, 488.4 MB
[runlim] sample:		11473.6 time, 2900.3 real, 494.3 MB
[runlim] sample:		11513.2 time, 2910.3 real, 498.3 MB
[runlim] sample:		11552.7 time, 2920.3 real, 504.3 MB
[runlim] sample:		11592.3 time, 2930.3 real, 508.3 MB
[runlim] sample:		11631.9 time, 2940.3 real, 512.6 MB
[runlim] sample:		11671.5 time, 2950.3 real, 516.6 MB
[runlim] sample:		11711.1 time, 2960.3 real, 520.6 MB
[runlim] sample:		11750.6 time, 2970.3 real, 524.6 MB
[runlim] sample:		11790.2 time, 2980.3 real, 528.8 MB
[runlim] sample:		11829.8 time, 2990.3 real, 534.8 MB
[runlim] sample:		11869.4 time, 3000.3 real, 538.8 MB
[runlim] sample:		11909.0 time, 3010.3 real, 542.8 MB
[runlim] sample:		11948.6 time, 3020.3 real, 545.7 MB
[runlim] sample:		11988.2 time, 3030.3 real, 550.0 MB
[runlim] sample:		12027.8 time, 3040.3 real, 552.0 MB
[runlim] sample:		12067.4 time, 3050.3 real, 556.0 MB
[runlim] sample:		12106.9 time, 3060.3 real, 558.1 MB
[runlim] sample:		12146.5 time, 3070.3 real, 562.4 MB
[runlim] sample:		12186.1 time, 3080.3 real, 564.4 MB
[runlim] sample:		12225.6 time, 3090.3 real, 568.4 MB
[runlim] sample:		12265.2 time, 3100.3 real, 570.6 MB
[runlim] sample:		12304.8 time, 3110.3 real, 576.4 MB
[runlim] sample:		12344.3 time, 3120.3 real, 582.7 MB
[runlim] sample:		12383.9 time, 3130.3 real, 586.7 MB
[runlim] sample:		12423.5 time, 3140.3 real, 590.7 MB
[runlim] sample:		12463.1 time, 3150.3 real, 594.7 MB
[runlim] sample:		12502.7 time, 3160.3 real, 597.4 MB
[runlim] sample:		12542.2 time, 3170.3 real, 599.4 MB
[runlim] sample:		12581.7 time, 3180.3 real, 601.4 MB
[runlim] sample:		12621.3 time, 3190.3 real, 605.4 MB
[runlim] sample:		12660.9 time, 3200.3 real, 607.4 MB
[runlim] sample:		12700.5 time, 3210.3 real, 609.9 MB
[runlim] sample:		12740.1 time, 3220.3 real, 611.9 MB
[runlim] sample:		12779.6 time, 3230.3 real, 615.9 MB
[runlim] sample:		12819.2 time, 3240.3 real, 617.9 MB
[runlim] sample:		12858.8 time, 3250.3 real, 622.1 MB
[runlim] sample:		12898.4 time, 3260.3 real, 624.1 MB
[runlim] sample:		12937.9 time, 3270.3 real, 626.1 MB
[runlim] sample:		12977.5 time, 3280.3 real, 628.4 MB
[runlim] sample:		13017.1 time, 3290.3 real, 630.6 MB
[runlim] sample:		13056.6 time, 3300.3 real, 632.9 MB
[runlim] sample:		13096.2 time, 3310.3 real, 635.4 MB
[runlim] sample:		13135.8 time, 3320.3 real, 637.6 MB
[runlim] sample:		13175.3 time, 3330.3 real, 639.9 MB
[runlim] sample:		13214.9 time, 3340.3 real, 642.4 MB
[runlim] sample:		13254.5 time, 3350.3 real, 644.4 MB
[runlim] sample:		13294.0 time, 3360.3 real, 646.6 MB
[runlim] sample:		13333.6 time, 3370.3 real, 648.9 MB
[runlim] sample:		13373.1 time, 3380.3 real, 650.9 MB
[runlim] sample:		13412.7 time, 3390.3 real, 653.1 MB
[runlim] sample:		13452.3 time, 3400.3 real, 655.7 MB
[runlim] sample:		13491.9 time, 3410.3 real, 657.7 MB
[runlim] sample:		13531.4 time, 3420.3 real, 659.7 MB
[runlim] sample:		13571.0 time, 3430.3 real, 661.9 MB
[runlim] sample:		13610.5 time, 3440.3 real, 664.5 MB
[runlim] sample:		13650.0 time, 3450.3 real, 666.5 MB
[runlim] sample:		13689.6 time, 3460.3 real, 668.5 MB
[runlim] sample:		13729.1 time, 3470.3 real, 670.7 MB
[runlim] sample:		13768.6 time, 3480.3 real, 673.0 MB
[runlim] sample:		13808.2 time, 3490.3 real, 675.0 MB
[runlim] sample:		13847.7 time, 3500.3 real, 675.0 MB
[runlim] sample:		13887.3 time, 3510.3 real, 677.5 MB
[runlim] sample:		13926.9 time, 3520.3 real, 679.7 MB
[runlim] sample:		13966.4 time, 3530.3 real, 682.3 MB
[runlim] sample:		14006.0 time, 3540.3 real, 685.0 MB
[runlim] sample:		14045.5 time, 3550.3 real, 685.0 MB
[runlim] sample:		14085.1 time, 3560.3 real, 687.0 MB
[runlim] sample:		14124.7 time, 3570.3 real, 690.3 MB
[runlim] sample:		14164.2 time, 3580.3 real, 690.3 MB
[runlim] sample:		14203.7 time, 3590.3 real, 696.6 MB
[runlim] end:			Sat Sep 19 21:42:38 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		143988
[runlim] real:			3600.12 seconds
[runlim] time:			14242.47 seconds
[runlim] space:			698.6 MB
[runlim] samples:		35998
