[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/all/selection/random/6s7.aig
[runlim] start:			Sat Sep 19 13:33:34 2015
[runlim] main pid:		9992
[runlim] sample:		4.2 time, 10.3 real, 360.9 MB
[runlim] sample:		43.8 time, 20.3 real, 386.1 MB
[runlim] sample:		83.5 time, 30.3 real, 398.7 MB
[runlim] sample:		123.1 time, 40.3 real, 416.5 MB
[runlim] sample:		162.7 time, 50.3 real, 430.5 MB
[runlim] sample:		202.3 time, 60.3 real, 443.2 MB
[runlim] sample:		241.9 time, 70.3 real, 458.7 MB
[runlim] sample:		281.5 time, 80.3 real, 470.0 MB
[runlim] sample:		321.1 time, 90.3 real, 477.6 MB
[runlim] sample:		360.8 time, 100.3 real, 482.1 MB
[runlim] sample:		400.4 time, 110.3 real, 493.3 MB
[runlim] sample:		440.0 time, 120.3 real, 500.3 MB
[runlim] sample:		479.6 time, 130.3 real, 504.8 MB
[runlim] sample:		519.2 time, 140.3 real, 514.8 MB
[runlim] sample:		558.8 time, 150.3 real, 518.3 MB
[runlim] sample:		598.4 time, 160.3 real, 519.8 MB
[runlim] sample:		638.1 time, 170.3 real, 522.7 MB
[runlim] sample:		677.6 time, 180.3 real, 533.8 MB
[runlim] sample:		717.3 time, 190.3 real, 539.3 MB
[runlim] sample:		756.9 time, 200.3 real, 543.3 MB
[runlim] sample:		796.5 time, 210.3 real, 546.4 MB
[runlim] sample:		836.1 time, 220.3 real, 548.3 MB
[runlim] sample:		875.7 time, 230.3 real, 547.7 MB
[runlim] sample:		915.3 time, 240.3 real, 539.9 MB
[runlim] sample:		954.9 time, 250.3 real, 542.6 MB
[runlim] sample:		994.6 time, 260.3 real, 546.5 MB
[runlim] sample:		1034.2 time, 270.3 real, 550.5 MB
[runlim] sample:		1073.8 time, 280.3 real, 561.0 MB
[runlim] sample:		1113.4 time, 290.3 real, 570.4 MB
[runlim] sample:		1153.0 time, 300.3 real, 580.3 MB
[runlim] sample:		1192.6 time, 310.3 real, 583.6 MB
[runlim] sample:		1232.2 time, 320.3 real, 586.9 MB
[runlim] sample:		1271.8 time, 330.3 real, 593.6 MB
[runlim] sample:		1311.4 time, 340.3 real, 606.5 MB
[runlim] sample:		1351.0 time, 350.3 real, 613.8 MB
[runlim] sample:		1390.7 time, 360.3 real, 626.1 MB
[runlim] sample:		1430.3 time, 370.3 real, 630.1 MB
[runlim] sample:		1469.9 time, 380.3 real, 628.6 MB
[runlim] sample:		1509.5 time, 390.3 real, 630.9 MB
[runlim] sample:		1549.1 time, 400.3 real, 638.4 MB
[runlim] sample:		1588.7 time, 410.3 real, 633.0 MB
[runlim] sample:		1628.3 time, 420.3 real, 636.3 MB
[runlim] sample:		1667.9 time, 430.3 real, 643.2 MB
[runlim] sample:		1707.5 time, 440.3 real, 656.1 MB
[runlim] sample:		1747.1 time, 450.3 real, 657.4 MB
[runlim] sample:		1786.7 time, 460.3 real, 657.9 MB
[runlim] sample:		1826.4 time, 470.3 real, 661.8 MB
[runlim] sample:		1865.9 time, 480.3 real, 665.7 MB
[runlim] sample:		1905.6 time, 490.3 real, 669.2 MB
[runlim] sample:		1945.2 time, 500.3 real, 666.7 MB
[runlim] sample:		1984.8 time, 510.3 real, 667.0 MB
[runlim] sample:		2024.4 time, 520.3 real, 670.8 MB
[runlim] sample:		2064.0 time, 530.3 real, 607.2 MB
[runlim] sample:		2103.6 time, 540.3 real, 612.4 MB
[runlim] sample:		2143.2 time, 550.3 real, 615.7 MB
[runlim] sample:		2182.8 time, 560.3 real, 621.3 MB
[runlim] sample:		2222.5 time, 570.3 real, 626.7 MB
[runlim] sample:		2262.1 time, 580.3 real, 638.3 MB
[runlim] sample:		2301.7 time, 590.3 real, 663.6 MB
[runlim] sample:		2341.3 time, 600.3 real, 634.5 MB
[runlim] sample:		2380.9 time, 610.3 real, 637.9 MB
[runlim] sample:		2420.5 time, 620.3 real, 641.9 MB
[runlim] sample:		2460.2 time, 630.3 real, 642.8 MB
[runlim] sample:		2499.8 time, 640.3 real, 646.7 MB
[runlim] sample:		2539.4 time, 650.3 real, 650.2 MB
[runlim] sample:		2579.0 time, 660.3 real, 657.9 MB
[runlim] sample:		2618.6 time, 670.3 real, 664.6 MB
[runlim] sample:		2658.2 time, 680.3 real, 669.6 MB
[runlim] sample:		2697.8 time, 690.3 real, 674.7 MB
[runlim] sample:		2737.4 time, 700.3 real, 685.2 MB
[runlim] sample:		2777.0 time, 710.3 real, 691.4 MB
[runlim] sample:		2816.7 time, 720.3 real, 696.7 MB
[runlim] sample:		2856.3 time, 730.3 real, 786.7 MB
[runlim] sample:		2895.9 time, 740.3 real, 754.9 MB
[runlim] sample:		2935.5 time, 750.3 real, 694.5 MB
[runlim] sample:		2975.1 time, 760.3 real, 697.1 MB
[runlim] sample:		3014.7 time, 770.3 real, 701.0 MB
[runlim] sample:		3054.3 time, 780.3 real, 702.8 MB
[runlim] sample:		3093.8 time, 790.3 real, 706.2 MB
[runlim] sample:		3133.4 time, 800.3 real, 711.4 MB
[runlim] sample:		3173.1 time, 810.3 real, 711.9 MB
[runlim] sample:		3212.7 time, 820.3 real, 712.8 MB
[runlim] sample:		3252.3 time, 830.3 real, 716.2 MB
[runlim] sample:		3291.9 time, 840.3 real, 723.8 MB
[runlim] sample:		3331.5 time, 850.3 real, 762.6 MB
[runlim] sample:		3371.1 time, 860.3 real, 773.4 MB
[runlim] sample:		3410.7 time, 870.3 real, 781.3 MB
[runlim] sample:		3450.3 time, 880.3 real, 787.4 MB
[runlim] sample:		3489.9 time, 890.3 real, 756.2 MB
[runlim] sample:		3529.5 time, 900.3 real, 760.5 MB
[runlim] sample:		3569.1 time, 910.3 real, 767.8 MB
[runlim] sample:		3608.7 time, 920.3 real, 770.7 MB
[runlim] sample:		3648.3 time, 930.3 real, 775.5 MB
[runlim] sample:		3688.0 time, 940.3 real, 778.8 MB
[runlim] sample:		3727.6 time, 950.3 real, 782.2 MB
[runlim] sample:		3767.2 time, 960.3 real, 786.3 MB
[runlim] sample:		3806.8 time, 970.3 real, 863.4 MB
[runlim] sample:		3846.4 time, 980.3 real, 845.3 MB
[runlim] sample:		3886.0 time, 990.3 real, 796.4 MB
[runlim] sample:		3925.6 time, 1000.3 real, 806.7 MB
[runlim] sample:		3965.2 time, 1010.3 real, 810.2 MB
[runlim] sample:		4004.8 time, 1020.3 real, 814.8 MB
[runlim] sample:		4044.4 time, 1030.3 real, 835.4 MB
[runlim] sample:		4084.0 time, 1040.3 real, 836.7 MB
[runlim] sample:		4123.6 time, 1050.3 real, 840.2 MB
[runlim] sample:		4163.3 time, 1060.3 real, 843.8 MB
[runlim] sample:		4202.9 time, 1070.3 real, 846.9 MB
[runlim] sample:		4242.5 time, 1080.3 real, 852.6 MB
[runlim] sample:		4282.1 time, 1090.3 real, 856.2 MB
[runlim] sample:		4321.7 time, 1100.3 real, 806.1 MB
[runlim] sample:		4361.3 time, 1110.3 real, 807.9 MB
[runlim] sample:		4400.9 time, 1120.3 real, 811.9 MB
[runlim] sample:		4440.5 time, 1130.3 real, 814.0 MB
[runlim] sample:		4480.1 time, 1140.3 real, 821.8 MB
[runlim] sample:		4519.8 time, 1150.3 real, 822.8 MB
[runlim] sample:		4559.4 time, 1160.3 real, 828.6 MB
[runlim] sample:		4599.0 time, 1170.3 real, 831.5 MB
[runlim] sample:		4638.6 time, 1180.3 real, 868.1 MB
[runlim] sample:		4678.2 time, 1190.3 real, 873.0 MB
[runlim] sample:		4717.8 time, 1200.3 real, 883.0 MB
[runlim] sample:		4757.4 time, 1210.3 real, 885.0 MB
[runlim] sample:		4797.0 time, 1220.3 real, 891.6 MB
[runlim] sample:		4836.6 time, 1230.3 real, 896.2 MB
[runlim] sample:		4876.2 time, 1240.3 real, 902.5 MB
[runlim] sample:		4915.8 time, 1250.3 real, 908.1 MB
[runlim] sample:		4955.4 time, 1260.3 real, 912.6 MB
[runlim] sample:		4995.0 time, 1270.3 real, 915.4 MB
[runlim] sample:		5034.6 time, 1280.3 real, 969.8 MB
[runlim] sample:		5074.2 time, 1290.3 real, 935.5 MB
[runlim] sample:		5113.8 time, 1300.3 real, 918.5 MB
[runlim] sample:		5153.4 time, 1310.3 real, 868.4 MB
[runlim] sample:		5193.0 time, 1320.3 real, 869.9 MB
[runlim] sample:		5232.6 time, 1330.3 real, 873.0 MB
[runlim] sample:		5272.2 time, 1340.3 real, 874.9 MB
[runlim] sample:		5311.8 time, 1350.3 real, 875.2 MB
[runlim] sample:		5351.4 time, 1360.3 real, 875.2 MB
[runlim] sample:		5391.0 time, 1370.3 real, 875.7 MB
[runlim] sample:		5430.6 time, 1380.3 real, 876.0 MB
[runlim] sample:		5470.1 time, 1390.3 real, 910.2 MB
[runlim] sample:		5509.7 time, 1400.3 real, 912.9 MB
[runlim] sample:		5549.3 time, 1410.3 real, 916.7 MB
[runlim] sample:		5589.0 time, 1420.3 real, 918.9 MB
[runlim] sample:		5628.6 time, 1430.3 real, 923.7 MB
[runlim] sample:		5668.2 time, 1440.3 real, 929.2 MB
[runlim] sample:		5707.8 time, 1450.3 real, 930.8 MB
[runlim] sample:		5747.4 time, 1460.3 real, 933.8 MB
[runlim] sample:		5787.0 time, 1470.3 real, 937.6 MB
[runlim] sample:		5826.6 time, 1480.3 real, 938.6 MB
[runlim] sample:		5866.2 time, 1490.3 real, 942.6 MB
[runlim] sample:		5905.8 time, 1500.3 real, 946.1 MB
[runlim] sample:		5945.4 time, 1510.3 real, 953.2 MB
[runlim] sample:		5985.0 time, 1520.3 real, 955.1 MB
[runlim] sample:		6024.6 time, 1530.3 real, 902.9 MB
[runlim] sample:		6064.2 time, 1540.3 real, 903.0 MB
[runlim] sample:		6103.8 time, 1550.3 real, 903.8 MB
[runlim] sample:		6143.4 time, 1560.3 real, 905.8 MB
[runlim] sample:		6183.0 time, 1570.3 real, 906.6 MB
[runlim] sample:		6222.7 time, 1580.3 real, 908.4 MB
[runlim] sample:		6262.3 time, 1590.3 real, 908.6 MB
[runlim] sample:		6301.9 time, 1600.3 real, 913.9 MB
[runlim] sample:		6341.5 time, 1610.3 real, 944.7 MB
[runlim] sample:		6381.1 time, 1620.3 real, 947.0 MB
[runlim] sample:		6420.7 time, 1630.3 real, 951.1 MB
[runlim] sample:		6460.3 time, 1640.3 real, 953.4 MB
[runlim] sample:		6499.9 time, 1650.3 real, 956.2 MB
[runlim] sample:		6539.5 time, 1660.3 real, 957.1 MB
[runlim] sample:		6579.1 time, 1670.3 real, 964.0 MB
[runlim] sample:		6618.7 time, 1680.3 real, 967.5 MB
[runlim] sample:		6658.3 time, 1690.3 real, 968.5 MB
[runlim] sample:		6697.9 time, 1700.3 real, 978.4 MB
[runlim] sample:		6737.5 time, 1710.3 real, 981.8 MB
[runlim] sample:		6777.1 time, 1720.3 real, 984.2 MB
[runlim] sample:		6816.7 time, 1730.3 real, 986.0 MB
[runlim] sample:		6856.3 time, 1740.3 real, 989.1 MB
[runlim] sample:		6895.9 time, 1750.3 real, 992.1 MB
[runlim] sample:		6935.5 time, 1760.3 real, 997.8 MB
[runlim] sample:		6975.1 time, 1770.3 real, 998.9 MB
[runlim] sample:		7014.7 time, 1780.3 real, 1046.4 MB
[runlim] sample:		7054.3 time, 1790.3 real, 952.0 MB
[runlim] sample:		7093.9 time, 1800.3 real, 954.0 MB
[runlim] sample:		7133.5 time, 1810.3 real, 954.0 MB
[runlim] sample:		7173.1 time, 1820.3 real, 954.0 MB
[runlim] sample:		7212.7 time, 1830.3 real, 954.6 MB
[runlim] sample:		7252.3 time, 1840.3 real, 955.3 MB
[runlim] sample:		7291.9 time, 1850.3 real, 956.6 MB
[runlim] sample:		7331.5 time, 1860.3 real, 990.1 MB
[runlim] sample:		7371.1 time, 1870.3 real, 993.9 MB
[runlim] sample:		7410.7 time, 1880.3 real, 1001.2 MB
[runlim] sample:		7450.3 time, 1890.3 real, 1004.2 MB
[runlim] sample:		7489.9 time, 1900.3 real, 1007.2 MB
[runlim] sample:		7529.5 time, 1910.3 real, 1010.8 MB
[runlim] sample:		7569.1 time, 1920.3 real, 1013.7 MB
[runlim] sample:		7608.7 time, 1930.3 real, 1017.5 MB
[runlim] sample:		7648.3 time, 1940.3 real, 1022.2 MB
[runlim] sample:		7687.9 time, 1950.3 real, 1027.4 MB
[runlim] sample:		7727.4 time, 1960.3 real, 1031.7 MB
[runlim] sample:		7767.0 time, 1970.3 real, 1033.7 MB
[runlim] sample:		7806.6 time, 1980.3 real, 1036.8 MB
[runlim] sample:		7846.2 time, 1990.3 real, 1041.7 MB
[runlim] sample:		7885.8 time, 2000.3 real, 1042.5 MB
[runlim] sample:		7925.4 time, 2010.3 real, 1045.6 MB
[runlim] sample:		7965.1 time, 2020.3 real, 1048.6 MB
[runlim] sample:		8004.6 time, 2030.3 real, 1052.2 MB
[runlim] sample:		8044.2 time, 2040.3 real, 1064.7 MB
[runlim] sample:		8083.8 time, 2050.3 real, 1071.1 MB
[runlim] sample:		8123.5 time, 2060.3 real, 1071.4 MB
[runlim] sample:		8163.1 time, 2070.3 real, 1073.9 MB
[runlim] sample:		8202.7 time, 2080.3 real, 1007.9 MB
[runlim] sample:		8242.3 time, 2090.3 real, 1010.4 MB
[runlim] sample:		8281.9 time, 2100.3 real, 1010.7 MB
[runlim] sample:		8321.5 time, 2110.3 real, 1011.4 MB
[runlim] sample:		8361.1 time, 2120.3 real, 1013.1 MB
[runlim] sample:		8400.7 time, 2130.3 real, 1013.9 MB
[runlim] sample:		8440.3 time, 2140.3 real, 1017.8 MB
[runlim] sample:		8479.9 time, 2150.3 real, 1051.5 MB
[runlim] sample:		8519.5 time, 2160.3 real, 1054.9 MB
[runlim] sample:		8559.1 time, 2170.3 real, 1059.8 MB
[runlim] sample:		8598.7 time, 2180.3 real, 1062.4 MB
[runlim] sample:		8638.2 time, 2190.3 real, 1067.0 MB
[runlim] sample:		8677.9 time, 2200.3 real, 1071.8 MB
[runlim] sample:		8717.5 time, 2210.3 real, 1074.6 MB
[runlim] sample:		8757.1 time, 2220.3 real, 1100.8 MB
[runlim] sample:		8796.6 time, 2230.3 real, 1101.5 MB
[runlim] sample:		8836.3 time, 2240.3 real, 1103.0 MB
[runlim] sample:		8875.9 time, 2250.3 real, 1107.5 MB
[runlim] sample:		8915.5 time, 2260.3 real, 1110.1 MB
[runlim] sample:		8955.1 time, 2270.3 real, 1112.3 MB
[runlim] sample:		8994.7 time, 2280.3 real, 1193.0 MB
[runlim] sample:		9034.3 time, 2290.3 real, 1197.0 MB
[runlim] sample:		9073.9 time, 2300.3 real, 1149.7 MB
[runlim] sample:		9113.5 time, 2310.3 real, 1151.7 MB
[runlim] sample:		9153.1 time, 2320.3 real, 1135.1 MB
[runlim] sample:		9192.8 time, 2330.3 real, 1137.9 MB
[runlim] sample:		9232.3 time, 2340.3 real, 1141.2 MB
[runlim] sample:		9271.9 time, 2350.3 real, 1144.1 MB
[runlim] sample:		9311.5 time, 2360.3 real, 1148.0 MB
[runlim] sample:		9351.1 time, 2370.3 real, 1150.0 MB
[runlim] sample:		9390.7 time, 2380.3 real, 1152.3 MB
[runlim] sample:		9430.3 time, 2390.3 real, 1154.5 MB
[runlim] sample:		9469.9 time, 2400.3 real, 1155.1 MB
[runlim] sample:		9509.5 time, 2410.3 real, 1084.4 MB
[runlim] sample:		9549.1 time, 2420.3 real, 1084.7 MB
[runlim] sample:		9588.7 time, 2430.3 real, 1084.7 MB
[runlim] sample:		9628.3 time, 2440.3 real, 1084.9 MB
[runlim] sample:		9667.9 time, 2450.3 real, 1085.4 MB
[runlim] sample:		9707.5 time, 2460.3 real, 1113.2 MB
[runlim] sample:		9747.1 time, 2470.3 real, 1146.4 MB
[runlim] sample:		9786.7 time, 2480.3 real, 1150.4 MB
[runlim] sample:		9826.3 time, 2490.3 real, 1152.9 MB
[runlim] sample:		9865.9 time, 2500.3 real, 1154.9 MB
[runlim] sample:		9905.5 time, 2510.3 real, 1157.2 MB
[runlim] sample:		9945.1 time, 2520.3 real, 1160.3 MB
[runlim] sample:		9984.7 time, 2530.3 real, 1164.6 MB
[runlim] sample:		10024.3 time, 2540.3 real, 1166.7 MB
[runlim] sample:		10063.9 time, 2550.3 real, 1168.4 MB
[runlim] sample:		10103.5 time, 2560.3 real, 1177.1 MB
[runlim] sample:		10143.1 time, 2570.3 real, 1183.1 MB
[runlim] sample:		10182.6 time, 2580.3 real, 1185.6 MB
[runlim] sample:		10222.2 time, 2590.3 real, 1187.5 MB
[runlim] sample:		10261.8 time, 2600.3 real, 1189.7 MB
[runlim] sample:		10301.4 time, 2610.3 real, 1194.0 MB
[runlim] sample:		10341.0 time, 2620.3 real, 1196.0 MB
[runlim] sample:		10380.5 time, 2630.3 real, 1196.2 MB
[runlim] sample:		10420.1 time, 2640.3 real, 1198.2 MB
[runlim] sample:		10459.8 time, 2650.3 real, 1200.2 MB
[runlim] sample:		10499.4 time, 2660.3 real, 1204.7 MB
[runlim] sample:		10538.9 time, 2670.3 real, 1207.7 MB
[runlim] sample:		10578.5 time, 2680.3 real, 1213.3 MB
[runlim] sample:		10618.1 time, 2690.3 real, 1215.3 MB
[runlim] sample:		10657.7 time, 2700.3 real, 1215.4 MB
[runlim] sample:		10697.3 time, 2710.3 real, 1219.9 MB
[runlim] sample:		10736.9 time, 2720.3 real, 1222.1 MB
[runlim] sample:		10776.5 time, 2730.3 real, 1224.2 MB
[runlim] sample:		10816.1 time, 2740.3 real, 1224.9 MB
[runlim] sample:		10855.7 time, 2750.3 real, 1226.2 MB
[runlim] sample:		10895.3 time, 2760.3 real, 1230.6 MB
[runlim] sample:		10934.9 time, 2770.3 real, 1149.5 MB
[runlim] sample:		10974.5 time, 2780.3 real, 1151.3 MB
[runlim] sample:		11014.1 time, 2790.3 real, 1151.5 MB
[runlim] sample:		11053.7 time, 2800.3 real, 1153.8 MB
[runlim] sample:		11093.3 time, 2810.3 real, 1156.3 MB
[runlim] sample:		11132.9 time, 2820.3 real, 1156.3 MB
[runlim] sample:		11172.5 time, 2830.3 real, 1165.8 MB
[runlim] sample:		11212.1 time, 2840.3 real, 1167.9 MB
[runlim] sample:		11251.7 time, 2850.3 real, 1170.0 MB
[runlim] sample:		11291.4 time, 2860.3 real, 1170.0 MB
[runlim] sample:		11330.9 time, 2870.3 real, 1170.3 MB
[runlim] sample:		11370.5 time, 2880.3 real, 1172.5 MB
[runlim] sample:		11410.2 time, 2890.3 real, 1172.6 MB
[runlim] sample:		11449.8 time, 2900.3 real, 1206.8 MB
[runlim] sample:		11489.4 time, 2910.3 real, 1209.0 MB
[runlim] sample:		11529.0 time, 2920.3 real, 1211.6 MB
[runlim] sample:		11568.6 time, 2930.3 real, 1214.3 MB
[runlim] sample:		11608.2 time, 2940.3 real, 1219.4 MB
[runlim] sample:		11647.8 time, 2950.3 real, 1223.6 MB
[runlim] sample:		11687.4 time, 2960.3 real, 1223.9 MB
[runlim] sample:		11727.0 time, 2970.3 real, 1225.9 MB
[runlim] sample:		11766.6 time, 2980.3 real, 1230.2 MB
[runlim] sample:		11806.2 time, 2990.3 real, 1232.4 MB
[runlim] sample:		11845.8 time, 3000.3 real, 1236.9 MB
[runlim] sample:		11885.4 time, 3010.3 real, 1236.9 MB
[runlim] sample:		11925.0 time, 3020.3 real, 1239.1 MB
[runlim] sample:		11964.6 time, 3030.3 real, 1241.1 MB
[runlim] sample:		12004.2 time, 3040.3 real, 1247.7 MB
[runlim] sample:		12043.8 time, 3050.3 real, 1247.7 MB
[runlim] sample:		12083.4 time, 3060.3 real, 1249.9 MB
[runlim] sample:		12123.0 time, 3070.3 real, 1252.0 MB
[runlim] sample:		12162.6 time, 3080.3 real, 1254.4 MB
[runlim] sample:		12202.2 time, 3090.3 real, 1256.6 MB
[runlim] sample:		12241.8 time, 3100.3 real, 1257.0 MB
[runlim] sample:		12281.4 time, 3110.3 real, 1261.5 MB
[runlim] sample:		12321.0 time, 3120.3 real, 1263.5 MB
[runlim] sample:		12360.6 time, 3130.3 real, 1263.7 MB
[runlim] sample:		12400.2 time, 3140.3 real, 1265.7 MB
[runlim] sample:		12439.8 time, 3150.3 real, 1266.5 MB
[runlim] sample:		12479.4 time, 3160.3 real, 1267.9 MB
[runlim] sample:		12519.0 time, 3170.3 real, 1272.7 MB
[runlim] sample:		12558.6 time, 3180.3 real, 1274.7 MB
[runlim] sample:		12598.2 time, 3190.3 real, 1277.0 MB
[runlim] sample:		12637.8 time, 3200.3 real, 1277.7 MB
[runlim] sample:		12677.4 time, 3210.3 real, 1284.0 MB
[runlim] sample:		12717.0 time, 3220.3 real, 1286.0 MB
[runlim] sample:		12756.6 time, 3230.3 real, 1288.5 MB
[runlim] sample:		12796.2 time, 3240.3 real, 1294.5 MB
[runlim] sample:		12835.8 time, 3250.3 real, 1203.2 MB
[runlim] sample:		12875.4 time, 3260.3 real, 1203.5 MB
[runlim] sample:		12915.0 time, 3270.3 real, 1203.5 MB
[runlim] sample:		12954.6 time, 3280.3 real, 1204.9 MB
[runlim] sample:		12994.2 time, 3290.3 real, 1204.9 MB
[runlim] sample:		13033.9 time, 3300.3 real, 1205.4 MB
[runlim] sample:		13073.4 time, 3310.3 real, 1207.5 MB
[runlim] sample:		13113.0 time, 3320.3 real, 1207.5 MB
[runlim] sample:		13152.6 time, 3330.3 real, 1239.3 MB
[runlim] sample:		13192.2 time, 3340.3 real, 1239.6 MB
[runlim] sample:		13231.8 time, 3350.3 real, 1243.8 MB
[runlim] sample:		13271.4 time, 3360.3 real, 1246.8 MB
[runlim] sample:		13311.0 time, 3370.3 real, 1249.8 MB
[runlim] sample:		13350.6 time, 3380.3 real, 1250.6 MB
[runlim] sample:		13390.2 time, 3390.3 real, 1255.7 MB
[runlim] sample:		13429.8 time, 3400.3 real, 1257.7 MB
[runlim] sample:		13469.4 time, 3410.3 real, 1260.0 MB
[runlim] sample:		13509.0 time, 3420.3 real, 1214.8 MB
[runlim] sample:		13548.6 time, 3430.3 real, 1215.0 MB
[runlim] sample:		13588.1 time, 3440.3 real, 1217.3 MB
[runlim] sample:		13627.7 time, 3450.3 real, 1217.8 MB
[runlim] sample:		13667.3 time, 3460.3 real, 1217.8 MB
[runlim] sample:		13706.9 time, 3470.3 real, 1218.1 MB
[runlim] sample:		13746.5 time, 3480.3 real, 1249.6 MB
[runlim] sample:		13786.1 time, 3490.3 real, 1254.1 MB
[runlim] sample:		13825.7 time, 3500.3 real, 1256.1 MB
[runlim] sample:		13865.3 time, 3510.3 real, 1258.8 MB
[runlim] sample:		13904.9 time, 3520.3 real, 1263.2 MB
[runlim] sample:		13944.5 time, 3530.3 real, 1265.4 MB
[runlim] sample:		13984.1 time, 3540.3 real, 1267.7 MB
[runlim] sample:		14023.7 time, 3550.3 real, 1269.7 MB
[runlim] sample:		14063.2 time, 3560.3 real, 1271.9 MB
[runlim] sample:		14102.9 time, 3570.3 real, 1278.2 MB
[runlim] sample:		14142.5 time, 3580.3 real, 1278.2 MB
[runlim] sample:		14182.1 time, 3590.3 real, 1280.4 MB
[runlim] end:			Sat Sep 19 14:33:34 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		432210
[runlim] real:			3600.05 seconds
[runlim] time:			14220.48 seconds
[runlim] space:			1294.7 MB
[runlim] samples:		35997
