[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/iimc/single.iimc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/oski15/submission/single/oski15a14b28s.aig
[runlim] start:			Thu Sep 17 11:58:06 2015
[runlim] main pid:		1178
[runlim] sample:		10.0 time, 10.3 real, 103.6 MB
[runlim] sample:		19.9 time, 20.3 real, 107.4 MB
[runlim] sample:		29.9 time, 30.3 real, 107.4 MB
[runlim] sample:		52.2 time, 40.3 real, 260.0 MB
[runlim] sample:		90.3 time, 50.3 real, 636.5 MB
[runlim] sample:		130.0 time, 60.3 real, 664.1 MB
[runlim] sample:		169.6 time, 70.3 real, 679.7 MB
[runlim] sample:		209.2 time, 80.3 real, 691.2 MB
[runlim] sample:		248.8 time, 90.3 real, 717.5 MB
[runlim] sample:		288.4 time, 100.3 real, 698.4 MB
[runlim] sample:		328.1 time, 110.3 real, 716.1 MB
[runlim] sample:		367.7 time, 120.3 real, 749.6 MB
[runlim] sample:		407.3 time, 130.3 real, 760.9 MB
[runlim] sample:		446.9 time, 140.3 real, 767.6 MB
[runlim] sample:		486.5 time, 150.3 real, 768.4 MB
[runlim] sample:		526.1 time, 160.3 real, 777.9 MB
[runlim] sample:		565.7 time, 170.3 real, 778.9 MB
[runlim] sample:		605.3 time, 180.3 real, 781.2 MB
[runlim] sample:		644.9 time, 190.3 real, 784.3 MB
[runlim] sample:		684.5 time, 200.3 real, 785.9 MB
[runlim] sample:		724.1 time, 210.3 real, 792.9 MB
[runlim] sample:		763.7 time, 220.3 real, 798.7 MB
[runlim] sample:		803.3 time, 230.3 real, 801.0 MB
[runlim] sample:		842.9 time, 240.3 real, 813.3 MB
[runlim] sample:		882.5 time, 250.3 real, 822.1 MB
[runlim] sample:		922.1 time, 260.3 real, 819.9 MB
[runlim] sample:		961.7 time, 270.3 real, 828.1 MB
[runlim] sample:		1001.3 time, 280.3 real, 829.3 MB
[runlim] sample:		1040.8 time, 290.3 real, 825.5 MB
[runlim] sample:		1080.5 time, 300.3 real, 828.0 MB
[runlim] sample:		1120.1 time, 310.3 real, 830.9 MB
[runlim] sample:		1159.7 time, 320.3 real, 835.6 MB
[runlim] sample:		1199.3 time, 330.3 real, 847.7 MB
[runlim] sample:		1238.9 time, 340.3 real, 850.7 MB
[runlim] sample:		1278.5 time, 350.3 real, 860.1 MB
[runlim] sample:		1318.1 time, 360.3 real, 860.7 MB
[runlim] sample:		1357.7 time, 370.3 real, 863.2 MB
[runlim] sample:		1397.2 time, 380.3 real, 870.4 MB
[runlim] sample:		1436.8 time, 390.3 real, 877.9 MB
[runlim] sample:		1476.5 time, 400.3 real, 885.7 MB
[runlim] sample:		1516.0 time, 410.3 real, 896.3 MB
[runlim] sample:		1555.7 time, 420.3 real, 889.2 MB
[runlim] sample:		1595.3 time, 430.3 real, 896.4 MB
[runlim] sample:		1634.9 time, 440.3 real, 896.4 MB
[runlim] sample:		1674.5 time, 450.3 real, 896.5 MB
[runlim] sample:		1714.1 time, 460.3 real, 902.2 MB
[runlim] sample:		1753.7 time, 470.3 real, 914.1 MB
[runlim] sample:		1793.3 time, 480.3 real, 905.7 MB
[runlim] sample:		1832.9 time, 490.3 real, 907.9 MB
[runlim] sample:		1872.5 time, 500.3 real, 878.9 MB
[runlim] sample:		1912.1 time, 510.3 real, 853.9 MB
[runlim] sample:		1951.7 time, 520.3 real, 865.9 MB
[runlim] sample:		1991.2 time, 530.3 real, 872.4 MB
[runlim] sample:		2030.8 time, 540.3 real, 948.5 MB
[runlim] sample:		2070.4 time, 550.3 real, 924.0 MB
[runlim] sample:		2110.1 time, 560.3 real, 912.9 MB
[runlim] sample:		2149.7 time, 570.3 real, 887.7 MB
[runlim] sample:		2189.3 time, 580.3 real, 835.4 MB
[runlim] sample:		2228.9 time, 590.3 real, 828.8 MB
[runlim] sample:		2268.5 time, 600.3 real, 828.6 MB
[runlim] sample:		2308.2 time, 610.3 real, 837.1 MB
[runlim] sample:		2347.8 time, 620.3 real, 828.0 MB
[runlim] sample:		2387.4 time, 630.3 real, 915.4 MB
[runlim] sample:		2427.0 time, 640.3 real, 882.8 MB
[runlim] sample:		2466.6 time, 650.3 real, 878.1 MB
[runlim] sample:		2506.2 time, 660.3 real, 857.4 MB
[runlim] sample:		2545.8 time, 670.3 real, 839.5 MB
[runlim] sample:		2585.4 time, 680.3 real, 844.1 MB
[runlim] sample:		2625.1 time, 690.3 real, 841.7 MB
[runlim] sample:		2664.7 time, 700.3 real, 847.5 MB
[runlim] sample:		2704.3 time, 710.3 real, 847.5 MB
[runlim] sample:		2743.9 time, 720.3 real, 847.5 MB
[runlim] sample:		2783.5 time, 730.3 real, 865.4 MB
[runlim] sample:		2823.1 time, 740.3 real, 916.9 MB
[runlim] sample:		2862.8 time, 750.3 real, 900.1 MB
[runlim] sample:		2902.3 time, 760.3 real, 890.2 MB
[runlim] sample:		2942.0 time, 770.3 real, 865.8 MB
[runlim] sample:		2981.6 time, 780.3 real, 865.4 MB
[runlim] sample:		3021.2 time, 790.3 real, 865.1 MB
[runlim] sample:		3060.8 time, 800.3 real, 873.5 MB
[runlim] sample:		3100.4 time, 810.3 real, 885.8 MB
[runlim] sample:		3140.0 time, 820.3 real, 902.1 MB
[runlim] sample:		3179.6 time, 830.3 real, 956.0 MB
[runlim] sample:		3219.2 time, 840.3 real, 931.1 MB
[runlim] sample:		3258.9 time, 850.3 real, 918.9 MB
[runlim] sample:		3298.5 time, 860.3 real, 898.8 MB
[runlim] sample:		3338.1 time, 870.3 real, 899.1 MB
[runlim] sample:		3377.7 time, 880.3 real, 900.7 MB
[runlim] sample:		3417.3 time, 890.3 real, 895.7 MB
[runlim] sample:		3456.9 time, 900.3 real, 896.7 MB
[runlim] sample:		3496.5 time, 910.3 real, 897.2 MB
[runlim] sample:		3536.2 time, 920.3 real, 896.8 MB
[runlim] sample:		3575.8 time, 930.3 real, 1002.7 MB
[runlim] sample:		3615.4 time, 940.3 real, 968.2 MB
[runlim] sample:		3655.0 time, 950.3 real, 963.7 MB
[runlim] sample:		3694.6 time, 960.3 real, 943.2 MB
[runlim] sample:		3734.2 time, 970.3 real, 915.0 MB
[runlim] sample:		3773.8 time, 980.3 real, 920.0 MB
[runlim] sample:		3813.4 time, 990.3 real, 920.0 MB
[runlim] sample:		3853.1 time, 1000.3 real, 927.5 MB
[runlim] sample:		3892.7 time, 1010.3 real, 927.5 MB
[runlim] sample:		3932.3 time, 1020.3 real, 930.8 MB
[runlim] sample:		3971.9 time, 1030.3 real, 925.3 MB
[runlim] sample:		4011.5 time, 1040.3 real, 977.2 MB
[runlim] sample:		4051.1 time, 1050.3 real, 963.1 MB
[runlim] sample:		4090.7 time, 1060.3 real, 953.0 MB
[runlim] sample:		4130.3 time, 1070.3 real, 943.2 MB
[runlim] sample:		4169.9 time, 1080.3 real, 943.9 MB
[runlim] sample:		4209.6 time, 1090.3 real, 944.7 MB
[runlim] sample:		4249.2 time, 1100.3 real, 956.3 MB
[runlim] sample:		4288.8 time, 1110.3 real, 958.8 MB
[runlim] sample:		4328.4 time, 1120.3 real, 958.8 MB
[runlim] sample:		4368.0 time, 1130.3 real, 949.9 MB
[runlim] sample:		4407.6 time, 1140.3 real, 951.8 MB
[runlim] sample:		4447.2 time, 1150.3 real, 1007.5 MB
[runlim] sample:		4486.8 time, 1160.3 real, 1013.4 MB
[runlim] sample:		4526.4 time, 1170.3 real, 993.5 MB
[runlim] sample:		4566.0 time, 1180.3 real, 991.5 MB
[runlim] sample:		4605.7 time, 1190.3 real, 976.9 MB
[runlim] sample:		4645.3 time, 1200.3 real, 963.0 MB
[runlim] sample:		4684.9 time, 1210.3 real, 963.2 MB
[runlim] sample:		4724.5 time, 1220.3 real, 972.0 MB
[runlim] sample:		4764.1 time, 1230.3 real, 965.9 MB
[runlim] sample:		4803.7 time, 1240.3 real, 965.7 MB
[runlim] sample:		4843.3 time, 1250.3 real, 957.2 MB
[runlim] sample:		4882.9 time, 1260.3 real, 953.8 MB
[runlim] sample:		4922.5 time, 1270.3 real, 1036.2 MB
[runlim] sample:		4962.1 time, 1280.3 real, 995.3 MB
[runlim] sample:		5001.8 time, 1290.3 real, 992.6 MB
[runlim] sample:		5041.4 time, 1300.3 real, 984.6 MB
[runlim] sample:		5081.0 time, 1310.3 real, 964.4 MB
[runlim] sample:		5120.6 time, 1320.3 real, 958.2 MB
[runlim] sample:		5160.2 time, 1330.3 real, 960.1 MB
[runlim] sample:		5199.8 time, 1340.3 real, 966.9 MB
[runlim] sample:		5239.4 time, 1350.3 real, 957.3 MB
[runlim] sample:		5279.0 time, 1360.3 real, 959.3 MB
[runlim] sample:		5318.6 time, 1370.3 real, 961.8 MB
[runlim] sample:		5358.2 time, 1380.3 real, 961.8 MB
[runlim] sample:		5397.9 time, 1390.3 real, 1059.0 MB
[runlim] sample:		5437.5 time, 1400.3 real, 1040.8 MB
[runlim] sample:		5477.1 time, 1410.3 real, 1032.4 MB
[runlim] sample:		5516.7 time, 1420.3 real, 1016.4 MB
[runlim] sample:		5556.3 time, 1430.3 real, 1006.5 MB
[runlim] sample:		5595.9 time, 1440.3 real, 992.2 MB
[runlim] sample:		5635.5 time, 1450.3 real, 998.5 MB
[runlim] sample:		5675.1 time, 1460.3 real, 994.3 MB
[runlim] sample:		5714.8 time, 1470.3 real, 996.3 MB
[runlim] sample:		5754.4 time, 1480.3 real, 996.3 MB
[runlim] sample:		5794.0 time, 1490.3 real, 998.4 MB
[runlim] sample:		5833.6 time, 1500.3 real, 913.3 MB
[runlim] sample:		5873.2 time, 1510.3 real, 915.3 MB
[runlim] sample:		5912.8 time, 1520.3 real, 997.1 MB
[runlim] sample:		5952.5 time, 1530.3 real, 962.8 MB
[runlim] sample:		5992.1 time, 1540.3 real, 958.6 MB
[runlim] sample:		6031.7 time, 1550.3 real, 943.0 MB
[runlim] sample:		6071.3 time, 1560.3 real, 955.7 MB
[runlim] sample:		6110.9 time, 1570.3 real, 934.1 MB
[runlim] sample:		6150.5 time, 1580.3 real, 936.1 MB
[runlim] sample:		6190.1 time, 1590.3 real, 936.7 MB
[runlim] sample:		6229.8 time, 1600.3 real, 938.7 MB
[runlim] sample:		6269.4 time, 1610.3 real, 938.7 MB
[runlim] sample:		6309.0 time, 1620.3 real, 940.7 MB
[runlim] sample:		6348.6 time, 1630.3 real, 940.8 MB
[runlim] sample:		6388.2 time, 1640.3 real, 976.4 MB
[runlim] sample:		6427.8 time, 1650.3 real, 1003.1 MB
[runlim] sample:		6467.4 time, 1660.3 real, 992.1 MB
[runlim] sample:		6507.0 time, 1670.3 real, 983.7 MB
[runlim] sample:		6546.7 time, 1680.3 real, 965.9 MB
[runlim] sample:		6586.3 time, 1690.3 real, 949.9 MB
[runlim] sample:		6625.9 time, 1700.3 real, 953.4 MB
[runlim] sample:		6665.5 time, 1710.3 real, 949.9 MB
[runlim] sample:		6705.1 time, 1720.3 real, 955.5 MB
[runlim] sample:		6744.7 time, 1730.3 real, 969.7 MB
[runlim] sample:		6784.4 time, 1740.3 real, 1057.1 MB
[runlim] sample:		6824.0 time, 1750.3 real, 1021.4 MB
[runlim] sample:		6863.6 time, 1760.3 real, 997.6 MB
[runlim] sample:		6903.2 time, 1770.3 real, 982.6 MB
[runlim] sample:		6942.8 time, 1780.3 real, 988.2 MB
[runlim] sample:		6982.4 time, 1790.3 real, 990.2 MB
[runlim] sample:		7022.1 time, 1800.3 real, 988.6 MB
[runlim] sample:		7061.6 time, 1810.3 real, 994.2 MB
[runlim] sample:		7101.3 time, 1820.3 real, 990.6 MB
[runlim] sample:		7140.9 time, 1830.3 real, 1054.8 MB
[runlim] sample:		7180.5 time, 1840.3 real, 1041.3 MB
[runlim] sample:		7220.1 time, 1850.3 real, 1017.1 MB
[runlim] sample:		7259.7 time, 1860.3 real, 997.1 MB
[runlim] sample:		7299.3 time, 1870.3 real, 997.7 MB
[runlim] sample:		7338.9 time, 1880.3 real, 997.8 MB
[runlim] sample:		7378.5 time, 1890.3 real, 997.8 MB
[runlim] sample:		7418.1 time, 1900.3 real, 984.4 MB
[runlim] sample:		7457.7 time, 1910.3 real, 984.4 MB
[runlim] sample:		7497.4 time, 1920.3 real, 1046.3 MB
[runlim] sample:		7537.0 time, 1930.3 real, 1046.3 MB
[runlim] sample:		7576.6 time, 1940.3 real, 1030.9 MB
[runlim] sample:		7616.2 time, 1950.3 real, 1016.7 MB
[runlim] sample:		7655.8 time, 1960.3 real, 988.6 MB
[runlim] sample:		7695.4 time, 1970.3 real, 1005.4 MB
[runlim] sample:		7735.0 time, 1980.3 real, 1012.0 MB
[runlim] sample:		7774.6 time, 1990.3 real, 1014.0 MB
[runlim] sample:		7814.2 time, 2000.3 real, 1016.2 MB
[runlim] sample:		7853.9 time, 2010.3 real, 1014.9 MB
[runlim] sample:		7893.5 time, 2020.3 real, 1101.8 MB
[runlim] sample:		7933.1 time, 2030.3 real, 1066.9 MB
[runlim] sample:		7972.7 time, 2040.3 real, 1052.2 MB
[runlim] sample:		8012.3 time, 2050.3 real, 1028.0 MB
[runlim] sample:		8051.9 time, 2060.3 real, 1030.0 MB
[runlim] sample:		8091.5 time, 2070.3 real, 1027.9 MB
[runlim] sample:		8131.1 time, 2080.3 real, 1029.9 MB
[runlim] sample:		8170.8 time, 2090.3 real, 1037.1 MB
[runlim] sample:		8210.4 time, 2100.3 real, 1037.8 MB
[runlim] sample:		8250.0 time, 2110.3 real, 1116.7 MB
[runlim] sample:		8289.6 time, 2120.3 real, 1076.8 MB
[runlim] sample:		8329.2 time, 2130.3 real, 1042.2 MB
[runlim] sample:		8368.8 time, 2140.3 real, 1026.1 MB
[runlim] sample:		8408.5 time, 2150.3 real, 1029.3 MB
[runlim] sample:		8448.1 time, 2160.3 real, 1042.7 MB
[runlim] sample:		8487.7 time, 2170.3 real, 1044.7 MB
[runlim] sample:		8527.3 time, 2180.3 real, 1130.2 MB
[runlim] sample:		8566.9 time, 2190.3 real, 1090.6 MB
[runlim] sample:		8606.5 time, 2200.3 real, 1074.1 MB
[runlim] sample:		8646.2 time, 2210.3 real, 1057.6 MB
[runlim] sample:		8685.8 time, 2220.3 real, 1036.0 MB
[runlim] sample:		8725.4 time, 2230.3 real, 1038.0 MB
[runlim] sample:		8765.0 time, 2240.3 real, 1043.1 MB
[runlim] sample:		8804.6 time, 2250.3 real, 1057.3 MB
[runlim] sample:		8844.3 time, 2260.3 real, 1139.7 MB
[runlim] sample:		8883.9 time, 2270.3 real, 1099.4 MB
[runlim] sample:		8923.5 time, 2280.3 real, 1079.6 MB
[runlim] sample:		8963.1 time, 2290.3 real, 1066.6 MB
[runlim] sample:		9002.7 time, 2300.3 real, 1067.9 MB
[runlim] sample:		9042.3 time, 2310.3 real, 1064.8 MB
[runlim] sample:		9082.0 time, 2320.3 real, 1070.1 MB
[runlim] sample:		9121.6 time, 2330.3 real, 1103.3 MB
[runlim] sample:		9161.2 time, 2340.3 real, 1109.8 MB
[runlim] sample:		9200.8 time, 2350.3 real, 1093.0 MB
[runlim] sample:		9240.4 time, 2360.3 real, 1076.0 MB
[runlim] sample:		9280.0 time, 2370.3 real, 1056.3 MB
[runlim] sample:		9319.6 time, 2380.3 real, 1064.4 MB
[runlim] sample:		9359.2 time, 2390.3 real, 1077.6 MB
[runlim] sample:		9398.9 time, 2400.3 real, 1079.9 MB
[runlim] sample:		9438.5 time, 2410.3 real, 1087.3 MB
[runlim] sample:		9478.1 time, 2420.3 real, 1167.9 MB
[runlim] sample:		9517.7 time, 2430.3 real, 1127.1 MB
[runlim] sample:		9557.3 time, 2440.3 real, 1099.5 MB
[runlim] sample:		9596.9 time, 2450.3 real, 1076.4 MB
[runlim] sample:		9636.5 time, 2460.3 real, 1072.5 MB
[runlim] sample:		9676.1 time, 2470.3 real, 1078.3 MB
[runlim] sample:		9715.7 time, 2480.3 real, 1080.6 MB
[runlim] sample:		9755.3 time, 2490.3 real, 1077.4 MB
[runlim] sample:		9795.0 time, 2500.3 real, 1153.9 MB
[runlim] sample:		9834.6 time, 2510.3 real, 1145.0 MB
[runlim] sample:		9874.2 time, 2520.3 real, 1109.5 MB
[runlim] sample:		9913.8 time, 2530.3 real, 1081.4 MB
[runlim] sample:		9953.4 time, 2540.3 real, 1085.6 MB
[runlim] sample:		9993.0 time, 2550.3 real, 1091.7 MB
[runlim] sample:		10032.6 time, 2560.3 real, 1093.4 MB
[runlim] sample:		10072.2 time, 2570.3 real, 1094.3 MB
[runlim] sample:		10111.9 time, 2580.3 real, 1168.2 MB
[runlim] sample:		10151.5 time, 2590.3 real, 1048.3 MB
[runlim] sample:		10191.1 time, 2600.3 real, 1041.4 MB
[runlim] sample:		10230.7 time, 2610.3 real, 1022.2 MB
[runlim] sample:		10270.3 time, 2620.3 real, 1016.2 MB
[runlim] sample:		10309.9 time, 2630.3 real, 1018.7 MB
[runlim] sample:		10349.5 time, 2640.3 real, 1019.5 MB
[runlim] sample:		10389.1 time, 2650.3 real, 1021.0 MB
[runlim] sample:		10428.7 time, 2660.3 real, 1045.0 MB
[runlim] sample:		10468.3 time, 2670.3 real, 1075.4 MB
[runlim] sample:		10508.0 time, 2680.3 real, 1043.4 MB
[runlim] sample:		10547.5 time, 2690.3 real, 1061.3 MB
[runlim] sample:		10587.2 time, 2700.3 real, 1038.9 MB
[runlim] sample:		10626.8 time, 2710.3 real, 1051.5 MB
[runlim] sample:		10666.4 time, 2720.3 real, 1053.0 MB
[runlim] sample:		10706.0 time, 2730.3 real, 1036.2 MB
[runlim] sample:		10745.6 time, 2740.3 real, 1037.4 MB
[runlim] sample:		10785.2 time, 2750.3 real, 1129.0 MB
[runlim] sample:		10824.9 time, 2760.3 real, 1084.1 MB
[runlim] sample:		10864.5 time, 2770.3 real, 1055.7 MB
[runlim] sample:		10904.1 time, 2780.3 real, 1048.0 MB
[runlim] sample:		10943.7 time, 2790.3 real, 1043.6 MB
[runlim] sample:		10983.3 time, 2800.3 real, 1052.0 MB
[runlim] sample:		11023.0 time, 2810.3 real, 1047.6 MB
[runlim] sample:		11062.6 time, 2820.3 real, 1054.0 MB
[runlim] sample:		11102.2 time, 2830.3 real, 1107.5 MB
[runlim] sample:		11141.8 time, 2840.3 real, 1095.3 MB
[runlim] sample:		11181.4 time, 2850.3 real, 1057.6 MB
[runlim] sample:		11221.0 time, 2860.3 real, 1059.6 MB
[runlim] sample:		11260.7 time, 2870.3 real, 1055.5 MB
[runlim] sample:		11300.3 time, 2880.3 real, 1061.9 MB
[runlim] sample:		11339.9 time, 2890.3 real, 1055.5 MB
[runlim] sample:		11379.5 time, 2900.3 real, 1093.8 MB
[runlim] sample:		11419.2 time, 2910.3 real, 1118.3 MB
[runlim] sample:		11458.8 time, 2920.3 real, 1102.3 MB
[runlim] sample:		11498.4 time, 2930.3 real, 1081.6 MB
[runlim] sample:		11538.0 time, 2940.3 real, 1065.5 MB
[runlim] sample:		11577.6 time, 2950.3 real, 1065.5 MB
[runlim] sample:		11617.2 time, 2960.3 real, 1067.5 MB
[runlim] sample:		11656.9 time, 2970.3 real, 1067.5 MB
[runlim] sample:		11696.5 time, 2980.3 real, 1073.5 MB
[runlim] sample:		11736.1 time, 2990.3 real, 1153.4 MB
[runlim] sample:		11775.7 time, 3000.3 real, 1131.7 MB
[runlim] sample:		11815.4 time, 3010.3 real, 1103.7 MB
[runlim] sample:		11855.0 time, 3020.3 real, 1097.6 MB
[runlim] sample:		11894.6 time, 3030.3 real, 1099.6 MB
[runlim] sample:		11934.2 time, 3040.3 real, 1099.6 MB
[runlim] sample:		11973.8 time, 3050.3 real, 1099.6 MB
[runlim] sample:		12013.5 time, 3060.3 real, 1140.1 MB
[runlim] sample:		12053.1 time, 3070.3 real, 1153.6 MB
[runlim] sample:		12092.7 time, 3080.3 real, 1127.4 MB
[runlim] sample:		12132.3 time, 3090.3 real, 1103.3 MB
[runlim] sample:		12171.9 time, 3100.3 real, 1103.3 MB
[runlim] sample:		12211.5 time, 3110.3 real, 1112.7 MB
[runlim] sample:		12251.1 time, 3120.3 real, 1113.5 MB
[runlim] sample:		12290.8 time, 3130.3 real, 1105.3 MB
[runlim] sample:		12330.4 time, 3140.3 real, 1107.3 MB
[runlim] sample:		12370.0 time, 3150.3 real, 1176.8 MB
[runlim] sample:		12409.6 time, 3160.3 real, 1157.9 MB
[runlim] sample:		12449.2 time, 3170.3 real, 1134.7 MB
[runlim] sample:		12488.8 time, 3180.3 real, 1115.0 MB
[runlim] sample:		12528.4 time, 3190.3 real, 1115.7 MB
[runlim] sample:		12568.0 time, 3200.3 real, 1123.9 MB
[runlim] sample:		12607.6 time, 3210.3 real, 1159.0 MB
[runlim] sample:		12647.2 time, 3220.3 real, 1163.5 MB
[runlim] sample:		12686.9 time, 3230.3 real, 1141.1 MB
[runlim] sample:		12726.5 time, 3240.3 real, 1093.8 MB
[runlim] sample:		12766.1 time, 3250.3 real, 1093.8 MB
[runlim] sample:		12805.7 time, 3260.3 real, 1104.8 MB
[runlim] sample:		12845.3 time, 3270.3 real, 1107.3 MB
[runlim] sample:		12884.9 time, 3280.3 real, 1185.9 MB
[runlim] sample:		12924.6 time, 3290.3 real, 1144.2 MB
[runlim] sample:		12964.2 time, 3300.3 real, 1125.2 MB
[runlim] sample:		13003.8 time, 3310.3 real, 1103.3 MB
[runlim] sample:		13043.4 time, 3320.3 real, 1111.0 MB
[runlim] sample:		13083.0 time, 3330.3 real, 1113.4 MB
[runlim] sample:		13122.6 time, 3340.3 real, 1107.5 MB
[runlim] sample:		13162.3 time, 3350.3 real, 1200.3 MB
[runlim] sample:		13201.9 time, 3360.3 real, 1150.8 MB
[runlim] sample:		13241.5 time, 3370.3 real, 1131.1 MB
[runlim] sample:		13281.1 time, 3380.3 real, 1122.5 MB
[runlim] sample:		13320.7 time, 3390.3 real, 1125.0 MB
[runlim] sample:		13360.4 time, 3400.3 real, 1127.5 MB
[runlim] sample:		13400.0 time, 3410.3 real, 1118.3 MB
[runlim] sample:		13439.6 time, 3420.3 real, 1198.1 MB
[runlim] sample:		13479.2 time, 3430.3 real, 1170.3 MB
[runlim] sample:		13518.8 time, 3440.3 real, 1152.9 MB
[runlim] sample:		13558.4 time, 3450.3 real, 1131.5 MB
[runlim] sample:		13598.0 time, 3460.3 real, 1139.9 MB
[runlim] sample:		13637.6 time, 3470.3 real, 1141.9 MB
[runlim] sample:		13677.2 time, 3480.3 real, 1143.9 MB
[runlim] sample:		13716.9 time, 3490.3 real, 1145.9 MB
[runlim] sample:		13756.5 time, 3500.3 real, 1187.2 MB
[runlim] sample:		13796.1 time, 3510.3 real, 1167.6 MB
[runlim] sample:		13835.7 time, 3520.3 real, 1156.5 MB
[runlim] sample:		13875.3 time, 3530.3 real, 1141.0 MB
[runlim] sample:		13914.9 time, 3540.3 real, 1149.4 MB
[runlim] sample:		13954.5 time, 3550.3 real, 1140.9 MB
[runlim] sample:		13994.1 time, 3560.3 real, 1145.4 MB
[runlim] sample:		14033.8 time, 3570.3 real, 1145.4 MB
[runlim] sample:		14073.4 time, 3580.3 real, 1216.1 MB
[runlim] sample:		14113.0 time, 3590.3 real, 1192.3 MB
[runlim] end:			Thu Sep 17 12:58:06 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.05 seconds
[runlim] time:			14151.41 seconds
[runlim] space:			1249.7 MB
[runlim] samples:		35997
