[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/abc/single.abcsimple
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/hwmcc14/single/6s514r.aig
[runlim] start:			Wed Sep 16 15:30:50 2015
[runlim] main pid:		27795
[runlim] sample:		19.8 time, 10.3 real, 363.7 MB
[runlim] sample:		59.5 time, 20.3 real, 382.2 MB
[runlim] sample:		99.1 time, 30.3 real, 397.1 MB
[runlim] sample:		138.7 time, 40.3 real, 415.0 MB
[runlim] sample:		178.3 time, 50.3 real, 446.6 MB
[runlim] sample:		218.0 time, 60.3 real, 456.9 MB
[runlim] sample:		257.6 time, 70.3 real, 467.6 MB
[runlim] sample:		297.2 time, 80.3 real, 471.4 MB
[runlim] sample:		336.8 time, 90.3 real, 474.5 MB
[runlim] sample:		376.4 time, 100.3 real, 484.4 MB
[runlim] sample:		416.0 time, 110.3 real, 489.6 MB
[runlim] sample:		455.6 time, 120.3 real, 496.7 MB
[runlim] sample:		495.2 time, 130.3 real, 501.6 MB
[runlim] sample:		534.9 time, 140.3 real, 505.6 MB
[runlim] sample:		574.4 time, 150.3 real, 511.8 MB
[runlim] sample:		614.1 time, 160.3 real, 522.0 MB
[runlim] sample:		653.6 time, 170.3 real, 519.3 MB
[runlim] sample:		693.2 time, 180.3 real, 532.2 MB
[runlim] sample:		732.8 time, 190.3 real, 536.8 MB
[runlim] sample:		772.4 time, 200.3 real, 549.2 MB
[runlim] sample:		812.0 time, 210.3 real, 542.9 MB
[runlim] sample:		851.6 time, 220.3 real, 559.1 MB
[runlim] sample:		891.2 time, 230.3 real, 566.3 MB
[runlim] sample:		930.8 time, 240.3 real, 571.2 MB
[runlim] sample:		970.4 time, 250.3 real, 574.4 MB
[runlim] sample:		1010.0 time, 260.3 real, 580.8 MB
[runlim] sample:		1049.6 time, 270.3 real, 634.6 MB
[runlim] sample:		1089.2 time, 280.3 real, 608.9 MB
[runlim] sample:		1128.8 time, 290.3 real, 607.8 MB
[runlim] sample:		1168.4 time, 300.3 real, 596.0 MB
[runlim] sample:		1208.0 time, 310.3 real, 606.7 MB
[runlim] sample:		1247.6 time, 320.3 real, 609.3 MB
[runlim] sample:		1287.2 time, 330.3 real, 614.7 MB
[runlim] sample:		1326.8 time, 340.3 real, 618.6 MB
[runlim] sample:		1366.4 time, 350.3 real, 621.1 MB
[runlim] sample:		1406.0 time, 360.3 real, 623.7 MB
[runlim] sample:		1445.6 time, 370.3 real, 624.0 MB
[runlim] sample:		1485.2 time, 380.3 real, 626.0 MB
[runlim] sample:		1524.7 time, 390.3 real, 628.1 MB
[runlim] sample:		1564.3 time, 400.3 real, 629.3 MB
[runlim] sample:		1603.9 time, 410.3 real, 633.9 MB
[runlim] sample:		1643.5 time, 420.3 real, 634.3 MB
[runlim] sample:		1683.1 time, 430.3 real, 636.8 MB
[runlim] sample:		1722.7 time, 440.3 real, 637.2 MB
[runlim] sample:		1762.3 time, 450.3 real, 638.7 MB
[runlim] sample:		1801.9 time, 460.3 real, 640.9 MB
[runlim] sample:		1841.4 time, 470.3 real, 643.1 MB
[runlim] sample:		1881.0 time, 480.3 real, 644.6 MB
[runlim] sample:		1920.6 time, 490.3 real, 646.4 MB
[runlim] sample:		1960.2 time, 500.3 real, 648.9 MB
[runlim] sample:		1999.7 time, 510.3 real, 651.2 MB
[runlim] sample:		2039.4 time, 520.3 real, 654.4 MB
[runlim] sample:		2078.9 time, 530.3 real, 658.7 MB
[runlim] sample:		2118.5 time, 540.3 real, 660.6 MB
[runlim] sample:		2158.1 time, 550.3 real, 663.0 MB
[runlim] sample:		2197.7 time, 560.3 real, 665.3 MB
[runlim] sample:		2237.3 time, 570.3 real, 669.4 MB
[runlim] sample:		2276.9 time, 580.3 real, 670.7 MB
[runlim] sample:		2316.4 time, 590.3 real, 672.8 MB
[runlim] sample:		2356.0 time, 600.3 real, 676.4 MB
[runlim] sample:		2395.6 time, 610.3 real, 678.5 MB
[runlim] sample:		2435.2 time, 620.3 real, 679.5 MB
[runlim] sample:		2474.8 time, 630.3 real, 687.5 MB
[runlim] sample:		2514.4 time, 640.3 real, 688.6 MB
[runlim] sample:		2553.9 time, 650.3 real, 691.3 MB
[runlim] sample:		2593.5 time, 660.3 real, 692.4 MB
[runlim] sample:		2633.1 time, 670.3 real, 694.8 MB
[runlim] sample:		2672.7 time, 680.3 real, 695.1 MB
[runlim] sample:		2712.3 time, 690.3 real, 697.6 MB
[runlim] sample:		2751.9 time, 700.3 real, 698.1 MB
[runlim] sample:		2791.5 time, 710.3 real, 716.1 MB
[runlim] sample:		2831.0 time, 720.3 real, 717.2 MB
[runlim] sample:		2870.6 time, 730.3 real, 718.4 MB
[runlim] sample:		2910.2 time, 740.3 real, 718.8 MB
[runlim] sample:		2949.8 time, 750.3 real, 720.7 MB
[runlim] sample:		2989.3 time, 760.3 real, 722.3 MB
[runlim] sample:		3028.9 time, 770.3 real, 724.4 MB
[runlim] sample:		3068.5 time, 780.3 real, 725.7 MB
[runlim] sample:		3108.1 time, 790.3 real, 732.6 MB
[runlim] sample:		3147.7 time, 800.3 real, 733.7 MB
[runlim] sample:		3187.3 time, 810.3 real, 736.1 MB
[runlim] sample:		3226.8 time, 820.3 real, 736.3 MB
[runlim] sample:		3266.4 time, 830.3 real, 736.3 MB
[runlim] sample:		3306.0 time, 840.3 real, 738.9 MB
[runlim] sample:		3345.6 time, 850.3 real, 740.2 MB
[runlim] sample:		3385.1 time, 860.3 real, 740.5 MB
[runlim] sample:		3424.7 time, 870.3 real, 743.4 MB
[runlim] sample:		3464.3 time, 880.3 real, 745.8 MB
[runlim] sample:		3503.9 time, 890.3 real, 748.2 MB
[runlim] sample:		3543.4 time, 900.3 real, 750.3 MB
[runlim] sample:		3583.0 time, 910.3 real, 751.1 MB
[runlim] sample:		3622.6 time, 920.3 real, 752.4 MB
[runlim] sample:		3662.2 time, 930.3 real, 756.7 MB
[runlim] sample:		3701.7 time, 940.3 real, 757.2 MB
[runlim] sample:		3741.3 time, 950.3 real, 760.7 MB
[runlim] sample:		3780.9 time, 960.3 real, 762.8 MB
[runlim] sample:		3820.5 time, 970.3 real, 764.7 MB
[runlim] sample:		3860.0 time, 980.3 real, 765.0 MB
[runlim] sample:		3899.6 time, 990.3 real, 768.6 MB
[runlim] sample:		3939.2 time, 1000.3 real, 772.0 MB
[runlim] sample:		3978.8 time, 1010.3 real, 772.7 MB
[runlim] sample:		4018.4 time, 1020.3 real, 775.7 MB
[runlim] sample:		4057.9 time, 1030.3 real, 781.1 MB
[runlim] sample:		4097.5 time, 1040.3 real, 781.7 MB
[runlim] sample:		4137.1 time, 1050.3 real, 784.0 MB
[runlim] sample:		4176.6 time, 1060.3 real, 784.4 MB
[runlim] sample:		4216.2 time, 1070.3 real, 785.5 MB
[runlim] sample:		4255.8 time, 1080.3 real, 788.5 MB
[runlim] sample:		4295.3 time, 1090.3 real, 791.1 MB
[runlim] sample:		4334.9 time, 1100.3 real, 791.8 MB
[runlim] sample:		4374.5 time, 1110.3 real, 794.7 MB
[runlim] sample:		4414.1 time, 1120.3 real, 795.3 MB
[runlim] sample:		4453.7 time, 1130.3 real, 797.9 MB
[runlim] sample:		4493.3 time, 1140.3 real, 798.2 MB
[runlim] sample:		4532.8 time, 1150.3 real, 799.5 MB
[runlim] sample:		4572.4 time, 1160.3 real, 802.0 MB
[runlim] sample:		4612.0 time, 1170.3 real, 804.3 MB
[runlim] sample:		4651.5 time, 1180.3 real, 805.3 MB
[runlim] sample:		4691.1 time, 1190.3 real, 806.8 MB
[runlim] sample:		4730.7 time, 1200.3 real, 790.5 MB
[runlim] sample:		4770.3 time, 1210.3 real, 799.2 MB
[runlim] sample:		4809.8 time, 1220.3 real, 807.5 MB
[runlim] sample:		4849.4 time, 1230.3 real, 814.1 MB
[runlim] sample:		4889.0 time, 1240.3 real, 818.9 MB
[runlim] sample:		4928.6 time, 1250.3 real, 821.2 MB
[runlim] sample:		4968.1 time, 1260.3 real, 822.5 MB
[runlim] sample:		5007.7 time, 1270.3 real, 823.6 MB
[runlim] sample:		5047.2 time, 1280.3 real, 832.2 MB
[runlim] sample:		5086.9 time, 1290.3 real, 832.2 MB
[runlim] sample:		5126.4 time, 1300.3 real, 838.5 MB
[runlim] sample:		5166.0 time, 1310.3 real, 838.8 MB
[runlim] sample:		5205.6 time, 1320.3 real, 841.3 MB
[runlim] sample:		5245.2 time, 1330.3 real, 843.8 MB
[runlim] sample:		5284.7 time, 1340.3 real, 844.3 MB
[runlim] sample:		5324.3 time, 1350.3 real, 846.9 MB
[runlim] sample:		5363.9 time, 1360.3 real, 847.4 MB
[runlim] sample:		5403.4 time, 1370.3 real, 847.8 MB
[runlim] sample:		5443.0 time, 1380.3 real, 849.5 MB
[runlim] sample:		5482.6 time, 1390.3 real, 849.8 MB
[runlim] sample:		5522.1 time, 1400.3 real, 850.0 MB
[runlim] sample:		5561.8 time, 1410.3 real, 852.3 MB
[runlim] sample:		5601.3 time, 1420.3 real, 853.3 MB
[runlim] sample:		5640.9 time, 1430.3 real, 854.1 MB
[runlim] sample:		5680.4 time, 1440.3 real, 854.4 MB
[runlim] sample:		5720.0 time, 1450.3 real, 857.0 MB
[runlim] sample:		5759.6 time, 1460.3 real, 857.8 MB
[runlim] sample:		5799.2 time, 1470.3 real, 860.7 MB
[runlim] sample:		5838.7 time, 1480.3 real, 861.7 MB
[runlim] sample:		5878.3 time, 1490.3 real, 861.9 MB
[runlim] sample:		5917.9 time, 1500.3 real, 865.0 MB
[runlim] sample:		5957.5 time, 1510.3 real, 865.5 MB
[runlim] sample:		5997.0 time, 1520.3 real, 868.4 MB
[runlim] sample:		6036.6 time, 1530.3 real, 871.9 MB
[runlim] sample:		6076.2 time, 1540.3 real, 872.2 MB
[runlim] sample:		6115.8 time, 1550.3 real, 873.2 MB
[runlim] sample:		6155.3 time, 1560.3 real, 874.2 MB
[runlim] sample:		6194.9 time, 1570.3 real, 877.5 MB
[runlim] sample:		6234.5 time, 1580.3 real, 878.0 MB
[runlim] sample:		6274.1 time, 1590.3 real, 884.2 MB
[runlim] sample:		6313.6 time, 1600.3 real, 888.1 MB
[runlim] sample:		6353.2 time, 1610.3 real, 890.2 MB
[runlim] sample:		6392.8 time, 1620.3 real, 890.7 MB
[runlim] sample:		6432.4 time, 1630.3 real, 889.1 MB
[runlim] sample:		6471.9 time, 1640.3 real, 893.7 MB
[runlim] sample:		6511.5 time, 1650.3 real, 894.7 MB
[runlim] sample:		6551.1 time, 1660.3 real, 895.8 MB
[runlim] sample:		6590.6 time, 1670.3 real, 898.9 MB
[runlim] sample:		6630.2 time, 1680.3 real, 899.4 MB
[runlim] sample:		6669.8 time, 1690.3 real, 899.6 MB
[runlim] sample:		6709.4 time, 1700.3 real, 906.0 MB
[runlim] sample:		6748.9 time, 1710.3 real, 906.3 MB
[runlim] sample:		6788.5 time, 1720.3 real, 907.2 MB
[runlim] sample:		6828.0 time, 1730.3 real, 913.2 MB
[runlim] sample:		6867.6 time, 1740.3 real, 914.2 MB
[runlim] sample:		6907.2 time, 1750.3 real, 916.0 MB
[runlim] sample:		6946.8 time, 1760.3 real, 918.0 MB
[runlim] sample:		6986.3 time, 1770.3 real, 919.5 MB
[runlim] sample:		7025.9 time, 1780.3 real, 920.3 MB
[runlim] sample:		7065.5 time, 1790.3 real, 923.0 MB
[runlim] sample:		7105.0 time, 1800.3 real, 923.8 MB
[runlim] sample:		7144.6 time, 1810.3 real, 924.3 MB
[runlim] sample:		7184.2 time, 1820.3 real, 927.1 MB
[runlim] sample:		7223.8 time, 1830.3 real, 927.9 MB
[runlim] sample:		7263.4 time, 1840.3 real, 957.6 MB
[runlim] sample:		7302.9 time, 1850.3 real, 959.3 MB
[runlim] sample:		7342.5 time, 1860.3 real, 962.4 MB
[runlim] sample:		7382.1 time, 1870.3 real, 963.2 MB
[runlim] sample:		7421.6 time, 1880.3 real, 963.9 MB
[runlim] sample:		7461.2 time, 1890.3 real, 964.9 MB
[runlim] sample:		7500.8 time, 1900.3 real, 967.1 MB
[runlim] sample:		7540.4 time, 1910.3 real, 967.7 MB
[runlim] sample:		7579.9 time, 1920.3 real, 967.9 MB
[runlim] sample:		7619.5 time, 1930.3 real, 969.0 MB
[runlim] sample:		7659.1 time, 1940.3 real, 969.7 MB
[runlim] sample:		7698.6 time, 1950.3 real, 981.1 MB
[runlim] sample:		7738.2 time, 1960.3 real, 983.9 MB
[runlim] sample:		7777.8 time, 1970.3 real, 983.9 MB
[runlim] sample:		7817.4 time, 1980.3 real, 986.7 MB
[runlim] sample:		7856.9 time, 1990.3 real, 987.0 MB
[runlim] sample:		7896.5 time, 2000.3 real, 987.7 MB
[runlim] sample:		7936.1 time, 2010.3 real, 988.7 MB
[runlim] sample:		7975.6 time, 2020.3 real, 991.1 MB
[runlim] sample:		8015.2 time, 2030.3 real, 991.3 MB
[runlim] sample:		8054.8 time, 2040.3 real, 991.6 MB
[runlim] sample:		8094.4 time, 2050.3 real, 991.8 MB
[runlim] sample:		8134.0 time, 2060.3 real, 992.1 MB
[runlim] sample:		8173.6 time, 2070.3 real, 994.3 MB
[runlim] sample:		8213.1 time, 2080.3 real, 994.3 MB
[runlim] sample:		8252.7 time, 2090.3 real, 996.3 MB
[runlim] sample:		8292.3 time, 2100.3 real, 997.4 MB
[runlim] sample:		8331.9 time, 2110.3 real, 999.7 MB
[runlim] sample:		8371.4 time, 2120.3 real, 1000.2 MB
[runlim] sample:		8411.0 time, 2130.3 real, 1002.8 MB
[runlim] sample:		8450.5 time, 2140.3 real, 1006.4 MB
[runlim] sample:		8490.1 time, 2150.3 real, 1006.9 MB
[runlim] sample:		8529.7 time, 2160.3 real, 1009.2 MB
[runlim] sample:		8569.3 time, 2170.3 real, 1009.7 MB
[runlim] sample:		8608.8 time, 2180.3 real, 1010.2 MB
[runlim] sample:		8648.4 time, 2190.3 real, 1010.7 MB
[runlim] sample:		8688.0 time, 2200.3 real, 1013.2 MB
[runlim] sample:		8727.5 time, 2210.3 real, 1015.6 MB
[runlim] sample:		8767.1 time, 2220.3 real, 1016.4 MB
[runlim] sample:		8806.7 time, 2230.3 real, 1037.9 MB
[runlim] sample:		8846.2 time, 2240.3 real, 1037.9 MB
[runlim] sample:		8885.8 time, 2250.3 real, 1040.6 MB
[runlim] sample:		8925.4 time, 2260.3 real, 1044.6 MB
[runlim] sample:		8964.9 time, 2270.3 real, 1045.7 MB
[runlim] sample:		9004.5 time, 2280.3 real, 1045.7 MB
[runlim] sample:		9044.1 time, 2290.3 real, 1047.4 MB
[runlim] sample:		9083.6 time, 2300.3 real, 1047.7 MB
[runlim] sample:		9123.2 time, 2310.3 real, 1049.9 MB
[runlim] sample:		9162.8 time, 2320.3 real, 1052.2 MB
[runlim] sample:		9202.3 time, 2330.3 real, 1052.2 MB
[runlim] sample:		9241.9 time, 2340.3 real, 1052.4 MB
[runlim] sample:		9281.5 time, 2350.3 real, 1052.6 MB
[runlim] sample:		9321.0 time, 2360.3 real, 1053.6 MB
[runlim] sample:		9360.6 time, 2370.3 real, 1054.5 MB
[runlim] sample:		9400.2 time, 2380.3 real, 1055.9 MB
[runlim] sample:		9439.7 time, 2390.3 real, 1056.7 MB
[runlim] sample:		9479.3 time, 2400.3 real, 1057.5 MB
[runlim] sample:		9518.9 time, 2410.3 real, 1058.3 MB
[runlim] sample:		9558.4 time, 2420.3 real, 1059.6 MB
[runlim] sample:		9598.0 time, 2430.3 real, 1061.9 MB
[runlim] sample:		9637.6 time, 2440.3 real, 1063.2 MB
[runlim] sample:		9677.2 time, 2450.3 real, 1067.4 MB
[runlim] sample:		9716.7 time, 2460.3 real, 1067.7 MB
[runlim] sample:		9756.3 time, 2470.3 real, 1068.1 MB
[runlim] sample:		9795.9 time, 2480.3 real, 1068.9 MB
[runlim] sample:		9835.4 time, 2490.3 real, 1069.9 MB
[runlim] sample:		9875.0 time, 2500.3 real, 1070.9 MB
[runlim] sample:		9914.6 time, 2510.3 real, 1074.5 MB
[runlim] sample:		9954.1 time, 2520.3 real, 1075.4 MB
[runlim] sample:		9993.7 time, 2530.3 real, 1076.2 MB
[runlim] sample:		10033.3 time, 2540.3 real, 1078.7 MB
[runlim] sample:		10072.9 time, 2550.3 real, 1082.7 MB
[runlim] sample:		10112.4 time, 2560.3 real, 1083.4 MB
[runlim] sample:		10152.0 time, 2570.3 real, 1083.9 MB
[runlim] sample:		10191.6 time, 2580.3 real, 1086.7 MB
[runlim] sample:		10231.1 time, 2590.3 real, 1088.0 MB
[runlim] sample:		10270.7 time, 2600.3 real, 1091.3 MB
[runlim] sample:		10310.3 time, 2610.3 real, 1091.8 MB
[runlim] sample:		10349.9 time, 2620.3 real, 1093.7 MB
[runlim] sample:		10389.4 time, 2630.3 real, 1145.2 MB
[runlim] sample:		10429.0 time, 2640.3 real, 1145.5 MB
[runlim] sample:		10468.6 time, 2650.3 real, 1168.3 MB
[runlim] sample:		10508.2 time, 2660.3 real, 1191.8 MB
[runlim] sample:		10547.7 time, 2670.3 real, 1186.8 MB
[runlim] sample:		10587.3 time, 2680.3 real, 1145.5 MB
[runlim] sample:		10626.9 time, 2690.3 real, 1153.2 MB
[runlim] sample:		10666.5 time, 2700.3 real, 1118.8 MB
[runlim] sample:		10706.0 time, 2710.3 real, 1118.8 MB
[runlim] sample:		10745.6 time, 2720.3 real, 1119.3 MB
[runlim] sample:		10785.1 time, 2730.3 real, 1123.6 MB
[runlim] sample:		10824.7 time, 2740.3 real, 1123.9 MB
[runlim] sample:		10864.3 time, 2750.3 real, 1123.9 MB
[runlim] sample:		10903.9 time, 2760.3 real, 1124.2 MB
[runlim] sample:		10943.4 time, 2770.3 real, 1126.5 MB
[runlim] sample:		10983.0 time, 2780.3 real, 1127.0 MB
[runlim] sample:		11022.5 time, 2790.3 real, 1127.0 MB
[runlim] sample:		11062.1 time, 2800.3 real, 1127.3 MB
[runlim] sample:		11101.7 time, 2810.3 real, 1127.5 MB
[runlim] sample:		11141.2 time, 2820.3 real, 1129.6 MB
[runlim] sample:		11180.8 time, 2830.3 real, 1129.6 MB
[runlim] sample:		11220.4 time, 2840.3 real, 1129.9 MB
[runlim] sample:		11259.9 time, 2850.3 real, 1129.9 MB
[runlim] sample:		11299.5 time, 2860.3 real, 1130.4 MB
[runlim] sample:		11339.1 time, 2870.3 real, 1134.6 MB
[runlim] sample:		11378.6 time, 2880.3 real, 1135.4 MB
[runlim] sample:		11418.2 time, 2890.3 real, 1135.4 MB
[runlim] sample:		11457.8 time, 2900.3 real, 1135.8 MB
[runlim] sample:		11497.3 time, 2910.3 real, 1135.8 MB
[runlim] sample:		11536.9 time, 2920.3 real, 1136.1 MB
[runlim] sample:		11576.5 time, 2930.3 real, 1138.3 MB
[runlim] sample:		11616.0 time, 2940.3 real, 1138.3 MB
[runlim] sample:		11655.6 time, 2950.3 real, 1138.3 MB
[runlim] sample:		11695.2 time, 2960.3 real, 1138.6 MB
[runlim] sample:		11734.7 time, 2970.3 real, 1140.9 MB
[runlim] sample:		11774.3 time, 2980.3 real, 1140.8 MB
[runlim] sample:		11813.8 time, 2990.3 real, 1142.9 MB
[runlim] sample:		11853.4 time, 3000.3 real, 1146.2 MB
[runlim] sample:		11893.0 time, 3010.3 real, 1148.3 MB
[runlim] sample:		11932.5 time, 3020.3 real, 1152.6 MB
[runlim] sample:		11972.1 time, 3030.3 real, 1152.9 MB
[runlim] sample:		12011.7 time, 3040.3 real, 1152.9 MB
[runlim] sample:		12051.2 time, 3050.3 real, 1152.9 MB
[runlim] sample:		12090.8 time, 3060.3 real, 1155.3 MB
[runlim] sample:		12130.4 time, 3070.3 real, 1155.8 MB
[runlim] sample:		12170.0 time, 3080.3 real, 1155.8 MB
[runlim] sample:		12209.5 time, 3090.3 real, 1156.1 MB
[runlim] sample:		12249.1 time, 3100.3 real, 1156.1 MB
[runlim] sample:		12288.6 time, 3110.3 real, 1156.1 MB
[runlim] sample:		12328.2 time, 3120.3 real, 1159.8 MB
[runlim] sample:		12367.8 time, 3130.3 real, 1159.8 MB
[runlim] sample:		12407.3 time, 3140.3 real, 1160.2 MB
[runlim] sample:		12446.9 time, 3150.3 real, 1160.9 MB
[runlim] sample:		12486.5 time, 3160.3 real, 1161.1 MB
[runlim] sample:		12526.0 time, 3170.3 real, 1161.1 MB
[runlim] sample:		12565.6 time, 3180.3 real, 1161.6 MB
[runlim] sample:		12605.2 time, 3190.3 real, 1164.5 MB
[runlim] sample:		12644.7 time, 3200.3 real, 1165.0 MB
[runlim] sample:		12684.3 time, 3210.3 real, 1167.4 MB
[runlim] sample:		12723.9 time, 3220.3 real, 1166.9 MB
[runlim] sample:		12763.5 time, 3230.3 real, 1167.4 MB
[runlim] sample:		12803.0 time, 3240.3 real, 1168.0 MB
[runlim] sample:		12842.6 time, 3250.3 real, 1170.3 MB
[runlim] sample:		12882.2 time, 3260.3 real, 1170.8 MB
[runlim] sample:		12921.7 time, 3270.3 real, 1170.8 MB
[runlim] sample:		12961.3 time, 3280.3 real, 1170.8 MB
[runlim] sample:		13000.9 time, 3290.3 real, 1171.1 MB
[runlim] sample:		13040.4 time, 3300.3 real, 1171.6 MB
[runlim] sample:		13080.0 time, 3310.3 real, 1172.1 MB
[runlim] sample:		13119.6 time, 3320.3 real, 1172.6 MB
[runlim] sample:		13159.1 time, 3330.3 real, 1175.5 MB
[runlim] sample:		13198.7 time, 3340.3 real, 1176.0 MB
[runlim] sample:		13238.3 time, 3350.3 real, 1176.8 MB
[runlim] sample:		13277.8 time, 3360.3 real, 1176.8 MB
[runlim] sample:		13317.4 time, 3370.3 real, 1176.8 MB
[runlim] sample:		13357.0 time, 3380.3 real, 1177.3 MB
[runlim] sample:		13396.5 time, 3390.3 real, 1177.6 MB
[runlim] sample:		13436.1 time, 3400.3 real, 1180.6 MB
[runlim] sample:		13475.7 time, 3410.3 real, 1180.9 MB
[runlim] sample:		13515.2 time, 3420.3 real, 1181.4 MB
[runlim] sample:		13554.8 time, 3430.3 real, 1182.4 MB
[runlim] sample:		13594.4 time, 3440.3 real, 1182.4 MB
[runlim] sample:		13633.9 time, 3450.3 real, 1182.9 MB
[runlim] sample:		13673.5 time, 3460.3 real, 1183.4 MB
[runlim] sample:		13713.1 time, 3470.3 real, 1186.7 MB
[runlim] sample:		13752.6 time, 3480.3 real, 1187.8 MB
[runlim] sample:		13792.2 time, 3490.3 real, 1188.5 MB
[runlim] sample:		13831.8 time, 3500.3 real, 1190.8 MB
[runlim] sample:		13871.3 time, 3510.3 real, 1191.8 MB
[runlim] sample:		13910.9 time, 3520.3 real, 1191.8 MB
[runlim] sample:		13950.4 time, 3530.3 real, 1193.8 MB
[runlim] sample:		13990.0 time, 3540.3 real, 1197.1 MB
[runlim] sample:		14029.5 time, 3550.3 real, 1197.3 MB
[runlim] sample:		14069.1 time, 3560.3 real, 1197.6 MB
[runlim] sample:		14108.7 time, 3570.3 real, 1198.3 MB
[runlim] sample:		14148.2 time, 3580.3 real, 1198.9 MB
[runlim] sample:		14187.8 time, 3590.3 real, 1199.1 MB
[runlim] end:			Wed Sep 16 16:30:50 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		432014
[runlim] real:			3600.08 seconds
[runlim] time:			14226.56 seconds
[runlim] space:			1215.4 MB
[runlim] samples:		35998
