[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.abcsuprove
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/hwmcc14/single/6s39.aig
[runlim] start:			Wed Sep 16 13:32:02 2015
[runlim] main pid:		31464
[runlim] sample:		20.9 time, 10.3 real, 635.3 MB
[runlim] sample:		55.8 time, 20.3 real, 582.7 MB
[runlim] sample:		84.9 time, 30.3 real, 626.7 MB
[runlim] sample:		124.5 time, 40.3 real, 651.5 MB
[runlim] sample:		142.9 time, 50.3 real, 551.0 MB
[runlim] sample:		6.5 time, 60.3 real, 542.2 MB
[runlim] sample:		33.7 time, 70.3 real, 274.4 MB
[runlim] sample:		73.3 time, 80.3 real, 288.4 MB
[runlim] sample:		112.9 time, 90.3 real, 293.0 MB
[runlim] sample:		152.5 time, 100.3 real, 309.4 MB
[runlim] sample:		192.1 time, 110.3 real, 325.2 MB
[runlim] sample:		231.7 time, 120.3 real, 338.4 MB
[runlim] sample:		271.3 time, 130.3 real, 358.1 MB
[runlim] sample:		310.9 time, 140.3 real, 363.5 MB
[runlim] sample:		350.5 time, 150.3 real, 370.4 MB
[runlim] sample:		390.1 time, 160.3 real, 376.7 MB
[runlim] sample:		429.7 time, 170.3 real, 379.3 MB
[runlim] sample:		469.3 time, 180.3 real, 382.1 MB
[runlim] sample:		508.9 time, 190.3 real, 385.6 MB
[runlim] sample:		548.5 time, 200.3 real, 388.4 MB
[runlim] sample:		588.1 time, 210.3 real, 392.5 MB
[runlim] sample:		627.7 time, 220.3 real, 397.9 MB
[runlim] sample:		667.3 time, 230.3 real, 400.7 MB
[runlim] sample:		706.9 time, 240.3 real, 404.1 MB
[runlim] sample:		746.5 time, 250.3 real, 414.6 MB
[runlim] sample:		786.1 time, 260.3 real, 416.4 MB
[runlim] sample:		825.7 time, 270.3 real, 417.7 MB
[runlim] sample:		865.3 time, 280.3 real, 422.3 MB
[runlim] sample:		905.0 time, 290.3 real, 427.2 MB
[runlim] sample:		944.6 time, 300.3 real, 430.3 MB
[runlim] sample:		984.2 time, 310.3 real, 433.1 MB
[runlim] sample:		1023.8 time, 320.3 real, 434.1 MB
[runlim] sample:		1063.4 time, 330.3 real, 436.4 MB
[runlim] sample:		1103.0 time, 340.3 real, 441.4 MB
[runlim] sample:		1142.6 time, 350.3 real, 444.3 MB
[runlim] sample:		1182.2 time, 360.3 real, 446.3 MB
[runlim] sample:		22.8 time, 370.3 real, 467.1 MB
[runlim] sample:		62.4 time, 380.3 real, 497.6 MB
[runlim] sample:		101.9 time, 390.3 real, 525.2 MB
[runlim] sample:		141.5 time, 400.3 real, 544.5 MB
[runlim] sample:		181.1 time, 410.3 real, 560.6 MB
[runlim] sample:		220.7 time, 420.3 real, 567.9 MB
[runlim] sample:		260.2 time, 430.3 real, 595.0 MB
[runlim] sample:		299.8 time, 440.3 real, 608.0 MB
[runlim] sample:		339.4 time, 450.3 real, 612.1 MB
[runlim] sample:		379.0 time, 460.3 real, 617.3 MB
[runlim] sample:		17.5 time, 470.3 real, 433.6 MB
[runlim] sample:		57.2 time, 480.3 real, 479.2 MB
[runlim] sample:		96.8 time, 490.3 real, 505.6 MB
[runlim] sample:		136.4 time, 500.3 real, 529.8 MB
[runlim] sample:		176.0 time, 510.3 real, 543.2 MB
[runlim] sample:		215.6 time, 520.3 real, 558.1 MB
[runlim] sample:		255.2 time, 530.3 real, 575.2 MB
[runlim] sample:		294.8 time, 540.3 real, 585.6 MB
[runlim] sample:		334.4 time, 550.3 real, 591.4 MB
[runlim] sample:		374.0 time, 560.3 real, 593.3 MB
[runlim] sample:		413.6 time, 570.3 real, 613.7 MB
[runlim] sample:		453.2 time, 580.3 real, 615.0 MB
[runlim] sample:		492.8 time, 590.3 real, 618.3 MB
[runlim] sample:		532.4 time, 600.3 real, 621.6 MB
[runlim] sample:		572.1 time, 610.3 real, 627.9 MB
[runlim] sample:		611.7 time, 620.3 real, 638.9 MB
[runlim] sample:		651.3 time, 630.3 real, 639.9 MB
[runlim] sample:		690.9 time, 640.3 real, 646.8 MB
[runlim] sample:		730.5 time, 650.3 real, 648.0 MB
[runlim] sample:		770.1 time, 660.3 real, 655.8 MB
[runlim] sample:		809.7 time, 670.3 real, 655.1 MB
[runlim] sample:		849.3 time, 680.3 real, 659.3 MB
[runlim] sample:		888.9 time, 690.3 real, 661.1 MB
[runlim] sample:		928.5 time, 700.3 real, 673.6 MB
[runlim] sample:		968.1 time, 710.3 real, 674.4 MB
[runlim] sample:		1007.7 time, 720.3 real, 677.4 MB
[runlim] sample:		1047.3 time, 730.3 real, 683.5 MB
[runlim] sample:		1086.9 time, 740.3 real, 688.9 MB
[runlim] sample:		1126.5 time, 750.3 real, 690.2 MB
[runlim] sample:		1166.2 time, 760.3 real, 692.3 MB
[runlim] sample:		1205.8 time, 770.3 real, 692.9 MB
[runlim] sample:		1245.4 time, 780.3 real, 695.2 MB
[runlim] sample:		1285.0 time, 790.3 real, 699.4 MB
[runlim] sample:		1324.6 time, 800.3 real, 710.4 MB
[runlim] sample:		1364.3 time, 810.3 real, 713.2 MB
[runlim] sample:		1403.9 time, 820.3 real, 710.3 MB
[runlim] sample:		1443.5 time, 830.3 real, 731.8 MB
[runlim] sample:		1483.1 time, 840.3 real, 734.4 MB
[runlim] sample:		1522.7 time, 850.3 real, 719.9 MB
[runlim] sample:		1562.3 time, 860.3 real, 732.5 MB
[runlim] sample:		1601.9 time, 870.3 real, 740.4 MB
[runlim] sample:		1641.5 time, 880.3 real, 747.5 MB
[runlim] sample:		1681.1 time, 890.3 real, 750.7 MB
[runlim] sample:		1720.7 time, 900.3 real, 752.5 MB
[runlim] sample:		1760.3 time, 910.3 real, 757.1 MB
[runlim] sample:		1799.9 time, 920.3 real, 759.5 MB
[runlim] sample:		1839.5 time, 930.3 real, 762.3 MB
[runlim] sample:		1879.1 time, 940.3 real, 761.5 MB
[runlim] sample:		1918.7 time, 950.3 real, 761.3 MB
[runlim] sample:		1958.3 time, 960.3 real, 765.4 MB
[runlim] sample:		1997.9 time, 970.3 real, 768.5 MB
[runlim] sample:		2037.5 time, 980.3 real, 769.1 MB
[runlim] sample:		2077.1 time, 990.3 real, 771.9 MB
[runlim] sample:		2116.7 time, 1000.3 real, 774.9 MB
[runlim] sample:		2156.3 time, 1010.3 real, 779.1 MB
[runlim] sample:		2195.9 time, 1020.3 real, 781.1 MB
[runlim] sample:		2235.5 time, 1030.3 real, 786.6 MB
[runlim] sample:		2275.1 time, 1040.3 real, 795.6 MB
[runlim] sample:		2314.7 time, 1050.3 real, 787.7 MB
[runlim] sample:		2354.3 time, 1060.3 real, 788.3 MB
[runlim] sample:		2393.8 time, 1070.3 real, 800.3 MB
[runlim] sample:		2433.4 time, 1080.3 real, 805.4 MB
[runlim] sample:		2473.0 time, 1090.3 real, 809.6 MB
[runlim] sample:		2512.6 time, 1100.3 real, 810.6 MB
[runlim] sample:		2552.2 time, 1110.3 real, 815.7 MB
[runlim] sample:		2591.8 time, 1120.3 real, 815.7 MB
[runlim] sample:		2631.4 time, 1130.3 real, 819.0 MB
[runlim] sample:		2671.0 time, 1140.3 real, 823.3 MB
[runlim] sample:		2710.6 time, 1150.3 real, 827.0 MB
[runlim] sample:		2750.2 time, 1160.3 real, 829.8 MB
[runlim] sample:		2789.8 time, 1170.3 real, 832.5 MB
[runlim] sample:		2829.4 time, 1180.3 real, 833.5 MB
[runlim] sample:		2869.0 time, 1190.3 real, 841.1 MB
[runlim] sample:		2908.6 time, 1200.3 real, 844.7 MB
[runlim] sample:		2948.2 time, 1210.3 real, 847.2 MB
[runlim] sample:		2987.8 time, 1220.3 real, 847.8 MB
[runlim] sample:		3027.4 time, 1230.3 real, 814.4 MB
[runlim] sample:		3067.0 time, 1240.3 real, 815.7 MB
[runlim] sample:		3106.6 time, 1250.3 real, 815.7 MB
[runlim] sample:		3146.2 time, 1260.3 real, 817.9 MB
[runlim] sample:		3185.8 time, 1270.3 real, 817.9 MB
[runlim] sample:		3225.4 time, 1280.3 real, 821.3 MB
[runlim] sample:		3265.0 time, 1290.3 real, 821.1 MB
[runlim] sample:		3304.6 time, 1300.3 real, 821.1 MB
[runlim] sample:		3344.2 time, 1310.3 real, 821.1 MB
[runlim] sample:		3383.8 time, 1320.3 real, 824.8 MB
[runlim] sample:		3423.4 time, 1330.3 real, 830.1 MB
[runlim] sample:		3463.0 time, 1340.3 real, 832.6 MB
[runlim] sample:		3502.6 time, 1350.3 real, 834.9 MB
[runlim] sample:		3542.2 time, 1360.3 real, 839.0 MB
[runlim] sample:		3581.8 time, 1370.3 real, 877.6 MB
[runlim] sample:		3621.4 time, 1380.3 real, 865.7 MB
[runlim] sample:		3661.0 time, 1390.3 real, 863.7 MB
[runlim] sample:		3700.6 time, 1400.3 real, 867.5 MB
[runlim] sample:		3740.2 time, 1410.3 real, 868.8 MB
[runlim] sample:		3779.8 time, 1420.3 real, 869.6 MB
[runlim] sample:		3819.3 time, 1430.3 real, 871.4 MB
[runlim] sample:		3858.9 time, 1440.3 real, 903.2 MB
[runlim] sample:		3898.5 time, 1450.3 real, 907.3 MB
[runlim] sample:		3938.1 time, 1460.3 real, 877.5 MB
[runlim] sample:		3977.7 time, 1470.3 real, 879.6 MB
[runlim] sample:		4017.3 time, 1480.3 real, 879.1 MB
[runlim] sample:		4056.9 time, 1490.3 real, 886.4 MB
[runlim] sample:		4096.5 time, 1500.3 real, 886.6 MB
[runlim] sample:		4136.1 time, 1510.3 real, 891.8 MB
[runlim] sample:		4175.7 time, 1520.3 real, 893.6 MB
[runlim] sample:		4215.3 time, 1530.3 real, 894.1 MB
[runlim] sample:		4254.9 time, 1540.3 real, 895.3 MB
[runlim] sample:		4294.4 time, 1550.3 real, 896.5 MB
[runlim] sample:		4334.0 time, 1560.3 real, 899.1 MB
[runlim] sample:		4373.6 time, 1570.3 real, 899.9 MB
[runlim] sample:		4413.2 time, 1580.3 real, 900.2 MB
[runlim] sample:		4452.8 time, 1590.3 real, 901.1 MB
[runlim] sample:		4492.4 time, 1600.3 real, 905.1 MB
[runlim] sample:		4532.0 time, 1610.3 real, 908.2 MB
[runlim] sample:		4571.6 time, 1620.3 real, 909.0 MB
[runlim] sample:		4611.2 time, 1630.3 real, 911.3 MB
[runlim] sample:		4650.8 time, 1640.3 real, 942.5 MB
[runlim] sample:		4690.4 time, 1650.3 real, 944.8 MB
[runlim] sample:		4730.0 time, 1660.3 real, 947.4 MB
[runlim] sample:		4769.6 time, 1670.3 real, 947.6 MB
[runlim] sample:		4809.2 time, 1680.3 real, 926.6 MB
[runlim] sample:		4848.8 time, 1690.3 real, 926.9 MB
[runlim] sample:		4888.4 time, 1700.3 real, 929.1 MB
[runlim] sample:		4928.0 time, 1710.3 real, 932.5 MB
[runlim] sample:		4967.6 time, 1720.3 real, 934.5 MB
[runlim] sample:		5007.2 time, 1730.3 real, 937.2 MB
[runlim] sample:		5046.8 time, 1740.3 real, 943.8 MB
[runlim] sample:		5086.5 time, 1750.3 real, 952.6 MB
[runlim] sample:		5126.1 time, 1760.3 real, 947.9 MB
[runlim] sample:		5165.7 time, 1770.3 real, 942.0 MB
[runlim] sample:		5205.2 time, 1780.3 real, 942.5 MB
[runlim] sample:		5244.9 time, 1790.3 real, 944.8 MB
[runlim] sample:		5284.4 time, 1800.3 real, 947.4 MB
[runlim] sample:		5324.1 time, 1810.3 real, 950.4 MB
[runlim] sample:		5363.6 time, 1820.3 real, 953.2 MB
[runlim] sample:		5403.2 time, 1830.3 real, 955.9 MB
[runlim] sample:		5442.8 time, 1840.3 real, 961.5 MB
[runlim] sample:		5482.4 time, 1850.3 real, 963.8 MB
[runlim] sample:		5522.0 time, 1860.3 real, 964.0 MB
[runlim] sample:		5561.6 time, 1870.3 real, 939.0 MB
[runlim] sample:		5601.2 time, 1880.3 real, 940.0 MB
[runlim] sample:		5640.8 time, 1890.3 real, 942.8 MB
[runlim] sample:		5680.4 time, 1900.3 real, 943.3 MB
[runlim] sample:		5719.9 time, 1910.3 real, 930.4 MB
[runlim] sample:		5759.5 time, 1920.3 real, 952.5 MB
[runlim] sample:		5799.1 time, 1930.3 real, 953.8 MB
[runlim] sample:		5838.7 time, 1940.3 real, 957.1 MB
[runlim] sample:		5878.3 time, 1950.3 real, 963.7 MB
[runlim] sample:		5917.9 time, 1960.3 real, 964.2 MB
[runlim] sample:		5957.5 time, 1970.3 real, 966.8 MB
[runlim] sample:		5997.1 time, 1980.3 real, 968.1 MB
[runlim] sample:		6036.7 time, 1990.3 real, 970.6 MB
[runlim] sample:		6076.3 time, 2000.3 real, 972.9 MB
[runlim] sample:		6115.9 time, 2010.3 real, 975.2 MB
[runlim] sample:		6155.5 time, 2020.3 real, 975.7 MB
[runlim] sample:		6195.1 time, 2030.3 real, 975.9 MB
[runlim] sample:		6234.7 time, 2040.3 real, 976.4 MB
[runlim] sample:		6274.3 time, 2050.3 real, 976.9 MB
[runlim] sample:		6313.9 time, 2060.3 real, 981.6 MB
[runlim] sample:		6353.5 time, 2070.3 real, 1016.1 MB
[runlim] sample:		6393.1 time, 2080.3 real, 1016.8 MB
[runlim] sample:		6432.6 time, 2090.3 real, 1018.8 MB
[runlim] sample:		6472.2 time, 2100.3 real, 1019.4 MB
[runlim] sample:		6511.8 time, 2110.3 real, 1019.6 MB
[runlim] sample:		6551.4 time, 2120.3 real, 1025.1 MB
[runlim] sample:		6591.0 time, 2130.3 real, 1025.1 MB
[runlim] sample:		6630.6 time, 2140.3 real, 1025.6 MB
[runlim] sample:		6670.2 time, 2150.3 real, 1028.9 MB
[runlim] sample:		6709.8 time, 2160.3 real, 1029.4 MB
[runlim] sample:		6749.4 time, 2170.3 real, 1032.8 MB
[runlim] sample:		6789.0 time, 2180.3 real, 1035.3 MB
[runlim] sample:		6828.6 time, 2190.3 real, 1035.6 MB
[runlim] sample:		6868.2 time, 2200.3 real, 1035.6 MB
[runlim] sample:		6907.9 time, 2210.3 real, 1037.8 MB
[runlim] sample:		6947.5 time, 2220.3 real, 1038.3 MB
[runlim] sample:		6987.1 time, 2230.3 real, 998.3 MB
[runlim] sample:		7026.7 time, 2240.3 real, 1005.3 MB
[runlim] sample:		7066.3 time, 2250.3 real, 1010.8 MB
[runlim] sample:		7105.9 time, 2260.3 real, 1013.1 MB
[runlim] sample:		7145.5 time, 2270.3 real, 1013.3 MB
[runlim] sample:		7185.1 time, 2280.3 real, 1013.6 MB
[runlim] sample:		7224.7 time, 2290.3 real, 1014.4 MB
[runlim] sample:		7264.3 time, 2300.3 real, 1017.5 MB
[runlim] sample:		7303.9 time, 2310.3 real, 1020.7 MB
[runlim] sample:		7343.5 time, 2320.3 real, 1022.3 MB
[runlim] sample:		7383.1 time, 2330.3 real, 1023.6 MB
[runlim] sample:		7422.7 time, 2340.3 real, 1024.6 MB
[runlim] sample:		7462.4 time, 2350.3 real, 1025.9 MB
[runlim] sample:		7502.0 time, 2360.3 real, 1027.2 MB
[runlim] sample:		7541.6 time, 2370.3 real, 1028.5 MB
[runlim] sample:		7581.2 time, 2380.3 real, 1029.8 MB
[runlim] sample:		7620.8 time, 2390.3 real, 1032.4 MB
[runlim] sample:		7660.4 time, 2400.3 real, 1034.7 MB
[runlim] sample:		7700.0 time, 2410.3 real, 1036.8 MB
[runlim] sample:		7739.6 time, 2420.3 real, 1039.6 MB
[runlim] sample:		7779.2 time, 2430.3 real, 1042.2 MB
[runlim] sample:		7818.8 time, 2440.3 real, 1076.1 MB
[runlim] sample:		7858.4 time, 2450.3 real, 1084.7 MB
[runlim] sample:		7898.0 time, 2460.3 real, 1055.8 MB
[runlim] sample:		7937.6 time, 2470.3 real, 1059.1 MB
[runlim] sample:		7977.2 time, 2480.3 real, 1032.2 MB
[runlim] sample:		8016.8 time, 2490.3 real, 1059.7 MB
[runlim] sample:		8056.4 time, 2500.3 real, 1094.3 MB
[runlim] sample:		8096.0 time, 2510.3 real, 1100.3 MB
[runlim] sample:		8135.6 time, 2520.3 real, 1106.4 MB
[runlim] sample:		8175.2 time, 2530.3 real, 1108.0 MB
[runlim] sample:		8214.8 time, 2540.3 real, 1111.3 MB
[runlim] sample:		8254.3 time, 2550.3 real, 1115.1 MB
[runlim] sample:		8293.9 time, 2560.3 real, 1116.3 MB
[runlim] sample:		8333.5 time, 2570.3 real, 1117.6 MB
[runlim] sample:		8373.1 time, 2580.3 real, 1120.0 MB
[runlim] sample:		8412.7 time, 2590.3 real, 1120.8 MB
[runlim] sample:		8452.3 time, 2600.3 real, 1123.8 MB
[runlim] sample:		8491.8 time, 2610.3 real, 1124.6 MB
[runlim] sample:		8531.4 time, 2620.3 real, 1125.1 MB
[runlim] sample:		8571.0 time, 2630.3 real, 1129.3 MB
[runlim] sample:		8610.6 time, 2640.3 real, 1130.1 MB
[runlim] sample:		8650.2 time, 2650.3 real, 1131.9 MB
[runlim] sample:		8689.8 time, 2660.3 real, 1136.2 MB
[runlim] sample:		8729.4 time, 2670.3 real, 1136.7 MB
[runlim] sample:		8769.0 time, 2680.3 real, 1137.6 MB
[runlim] sample:		8808.6 time, 2690.3 real, 1140.9 MB
[runlim] sample:		8848.1 time, 2700.3 real, 1143.7 MB
[runlim] sample:		8887.7 time, 2710.3 real, 1144.8 MB
[runlim] sample:		8927.3 time, 2720.3 real, 1146.9 MB
[runlim] sample:		8966.9 time, 2730.3 real, 1148.1 MB
[runlim] sample:		9006.5 time, 2740.3 real, 1148.8 MB
[runlim] sample:		9046.0 time, 2750.3 real, 1153.3 MB
[runlim] sample:		9085.7 time, 2760.3 real, 1098.1 MB
[runlim] sample:		9125.3 time, 2770.3 real, 1099.4 MB
[runlim] sample:		9164.8 time, 2780.3 real, 1102.4 MB
[runlim] sample:		9204.5 time, 2790.3 real, 1103.4 MB
[runlim] sample:		9244.0 time, 2800.3 real, 1103.9 MB
[runlim] sample:		9283.7 time, 2810.3 real, 1104.7 MB
[runlim] sample:		9323.3 time, 2820.3 real, 1111.6 MB
[runlim] sample:		9362.9 time, 2830.3 real, 1113.1 MB
[runlim] sample:		9402.4 time, 2840.3 real, 1114.9 MB
[runlim] sample:		9442.0 time, 2850.3 real, 1116.6 MB
[runlim] sample:		9481.7 time, 2860.3 real, 1117.7 MB
[runlim] sample:		9521.3 time, 2870.3 real, 1118.8 MB
[runlim] sample:		9560.9 time, 2880.3 real, 1120.4 MB
[runlim] sample:		9600.5 time, 2890.3 real, 1120.9 MB
[runlim] sample:		9640.1 time, 2900.3 real, 1124.0 MB
[runlim] sample:		9679.7 time, 2910.3 real, 1125.0 MB
[runlim] sample:		9719.3 time, 2920.3 real, 1126.2 MB
[runlim] sample:		9758.9 time, 2930.3 real, 1158.7 MB
[runlim] sample:		9798.5 time, 2940.3 real, 1159.8 MB
[runlim] sample:		9838.1 time, 2950.3 real, 1161.0 MB
[runlim] sample:		9877.7 time, 2960.3 real, 1164.8 MB
[runlim] sample:		9917.3 time, 2970.3 real, 1171.2 MB
[runlim] sample:		9956.9 time, 2980.3 real, 1174.8 MB
[runlim] sample:		9996.5 time, 2990.3 real, 1180.3 MB
[runlim] sample:		10036.1 time, 3000.3 real, 1183.8 MB
[runlim] sample:		10075.8 time, 3010.3 real, 1184.0 MB
[runlim] sample:		10115.4 time, 3020.3 real, 1187.6 MB
[runlim] sample:		10155.0 time, 3030.3 real, 1188.9 MB
[runlim] sample:		10194.6 time, 3040.3 real, 1190.7 MB
[runlim] sample:		10234.2 time, 3050.3 real, 1193.8 MB
[runlim] sample:		10273.8 time, 3060.3 real, 1197.8 MB
[runlim] sample:		10313.4 time, 3070.3 real, 1200.3 MB
[runlim] sample:		10353.0 time, 3080.3 real, 1204.1 MB
[runlim] sample:		10392.6 time, 3090.3 real, 1205.7 MB
[runlim] sample:		10432.2 time, 3100.3 real, 1209.0 MB
[runlim] sample:		10471.8 time, 3110.3 real, 1169.8 MB
[runlim] sample:		10511.4 time, 3120.3 real, 1171.8 MB
[runlim] sample:		10551.0 time, 3130.3 real, 1175.4 MB
[runlim] sample:		10590.7 time, 3140.3 real, 1177.9 MB
[runlim] sample:		10630.2 time, 3150.3 real, 1190.1 MB
[runlim] sample:		10669.8 time, 3160.3 real, 1176.0 MB
[runlim] sample:		10709.4 time, 3170.3 real, 1151.7 MB
[runlim] sample:		10749.0 time, 3180.3 real, 1152.0 MB
[runlim] sample:		10788.6 time, 3190.3 real, 1153.1 MB
[runlim] sample:		10828.2 time, 3200.3 real, 1153.8 MB
[runlim] sample:		10867.8 time, 3210.3 real, 1155.3 MB
[runlim] sample:		10907.4 time, 3220.3 real, 1156.3 MB
[runlim] sample:		10947.0 time, 3230.3 real, 1188.9 MB
[runlim] sample:		10986.6 time, 3240.3 real, 1191.4 MB
[runlim] sample:		11026.2 time, 3250.3 real, 1195.1 MB
[runlim] sample:		11065.8 time, 3260.3 real, 1196.6 MB
[runlim] sample:		11105.4 time, 3270.3 real, 1198.1 MB
[runlim] sample:		11145.0 time, 3280.3 real, 1198.9 MB
[runlim] sample:		11184.5 time, 3290.3 real, 1202.2 MB
[runlim] sample:		11224.1 time, 3300.3 real, 1209.9 MB
[runlim] sample:		11263.7 time, 3310.3 real, 1212.9 MB
[runlim] sample:		11303.3 time, 3320.3 real, 1214.5 MB
[runlim] sample:		11342.9 time, 3330.3 real, 1216.3 MB
[runlim] sample:		11382.5 time, 3340.3 real, 1219.6 MB
[runlim] sample:		11422.0 time, 3350.3 real, 1220.6 MB
[runlim] sample:		11461.6 time, 3360.3 real, 1223.4 MB
[runlim] sample:		11501.2 time, 3370.3 real, 1226.1 MB
[runlim] sample:		11540.8 time, 3380.3 real, 1229.7 MB
[runlim] sample:		11580.4 time, 3390.3 real, 1230.7 MB
[runlim] sample:		11620.0 time, 3400.3 real, 1231.7 MB
[runlim] sample:		11659.6 time, 3410.3 real, 1233.6 MB
[runlim] sample:		11699.2 time, 3420.3 real, 1193.4 MB
[runlim] sample:		11738.8 time, 3430.3 real, 1194.2 MB
[runlim] sample:		11778.4 time, 3440.3 real, 1195.4 MB
[runlim] sample:		11818.0 time, 3450.3 real, 1196.0 MB
[runlim] sample:		11857.6 time, 3460.3 real, 1196.7 MB
[runlim] sample:		11897.2 time, 3470.3 real, 1198.0 MB
[runlim] sample:		11936.8 time, 3480.3 real, 1199.1 MB
[runlim] sample:		11976.4 time, 3490.3 real, 1199.6 MB
[runlim] sample:		12016.0 time, 3500.3 real, 1201.8 MB
[runlim] sample:		12055.6 time, 3510.3 real, 1202.5 MB
[runlim] sample:		12095.2 time, 3520.3 real, 1204.0 MB
[runlim] sample:		12134.8 time, 3530.3 real, 1204.8 MB
[runlim] sample:		12174.4 time, 3540.3 real, 1206.4 MB
[runlim] sample:		12214.0 time, 3550.3 real, 1206.9 MB
[runlim] sample:		12253.6 time, 3560.3 real, 1207.4 MB
[runlim] sample:		12293.2 time, 3570.3 real, 1208.7 MB
[runlim] sample:		12332.8 time, 3580.3 real, 1208.7 MB
[runlim] sample:		12372.4 time, 3590.3 real, 1209.7 MB
[runlim] end:			Wed Sep 16 14:32:02 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		416276
[runlim] real:			3600.04 seconds
[runlim] time:			12410.79 seconds
[runlim] space:			1234.2 MB
[runlim] samples:		35997
