[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/6s148.aig
[runlim] start:			Tue Sep 15 17:00:14 2015
[runlim] main pid:		32260
[runlim] sample:		0.1 time, 10.6 real, 13.3 MB
[runlim] sample:		3.3 time, 20.6 real, 59.6 MB
[runlim] sample:		35.1 time, 30.6 real, 1093.0 MB
[runlim] sample:		70.5 time, 40.6 real, 1149.0 MB
[runlim] sample:		110.1 time, 50.6 real, 1188.8 MB
[runlim] sample:		138.9 time, 60.6 real, 1111.3 MB
[runlim] sample:		178.4 time, 70.6 real, 1160.6 MB
[runlim] sample:		218.0 time, 80.6 real, 1172.5 MB
[runlim] sample:		243.4 time, 90.6 real, 1132.7 MB
[runlim] sample:		282.9 time, 100.6 real, 1163.3 MB
[runlim] sample:		322.5 time, 110.6 real, 1179.5 MB
[runlim] sample:		362.0 time, 120.6 real, 1189.5 MB
[runlim] sample:		374.8 time, 130.6 real, 1048.5 MB
[runlim] sample:		414.4 time, 140.6 real, 1199.7 MB
[runlim] sample:		453.9 time, 150.6 real, 1204.7 MB
[runlim] sample:		492.6 time, 160.6 real, 1437.2 MB
[runlim] sample:		531.8 time, 170.6 real, 1461.0 MB
[runlim] sample:		571.3 time, 180.6 real, 1477.3 MB
[runlim] sample:		596.7 time, 190.6 real, 1233.9 MB
[runlim] sample:		636.3 time, 200.6 real, 1243.6 MB
[runlim] sample:		675.8 time, 210.6 real, 1247.1 MB
[runlim] sample:		715.3 time, 220.6 real, 1261.7 MB
[runlim] sample:		754.8 time, 230.6 real, 1272.8 MB
[runlim] sample:		794.3 time, 240.6 real, 1279.2 MB
[runlim] sample:		833.9 time, 250.6 real, 1265.1 MB
[runlim] sample:		873.4 time, 260.6 real, 1266.2 MB
[runlim] sample:		913.0 time, 270.6 real, 1255.3 MB
[runlim] sample:		952.4 time, 280.6 real, 1262.5 MB
[runlim] sample:		911.6 time, 290.6 real, 1204.1 MB
[runlim] sample:		951.2 time, 300.6 real, 1196.3 MB
[runlim] sample:		990.7 time, 310.6 real, 1215.7 MB
[runlim] sample:		1030.3 time, 320.6 real, 1220.9 MB
[runlim] sample:		1069.8 time, 330.6 real, 1228.2 MB
[runlim] sample:		1108.5 time, 340.6 real, 1459.9 MB
[runlim] sample:		1144.9 time, 350.6 real, 1362.7 MB
[runlim] sample:		1184.4 time, 360.6 real, 1365.5 MB
[runlim] sample:		1214.0 time, 370.6 real, 1246.8 MB
[runlim] sample:		1253.5 time, 380.6 real, 1260.0 MB
[runlim] sample:		1293.1 time, 390.6 real, 1273.6 MB
[runlim] sample:		1332.6 time, 400.6 real, 1266.6 MB
[runlim] sample:		1372.2 time, 410.6 real, 1283.3 MB
[runlim] sample:		1411.7 time, 420.6 real, 1276.1 MB
[runlim] sample:		1451.3 time, 430.6 real, 1276.6 MB
[runlim] sample:		1490.8 time, 440.6 real, 1308.8 MB
[runlim] sample:		1530.3 time, 450.6 real, 1324.1 MB
[runlim] sample:		1454.2 time, 460.6 real, 1251.0 MB
[runlim] sample:		42.8 time, 470.6 real, 931.7 MB
[runlim] sample:		82.3 time, 480.6 real, 963.3 MB
[runlim] sample:		121.8 time, 490.6 real, 1009.8 MB
[runlim] sample:		161.4 time, 500.6 real, 1033.4 MB
[runlim] sample:		200.9 time, 510.6 real, 1034.1 MB
[runlim] sample:		240.4 time, 520.6 real, 1045.0 MB
[runlim] sample:		280.0 time, 530.6 real, 1065.6 MB
[runlim] sample:		319.5 time, 540.6 real, 1105.4 MB
[runlim] sample:		359.0 time, 550.6 real, 1147.4 MB
[runlim] sample:		398.6 time, 560.6 real, 1123.8 MB
[runlim] sample:		438.1 time, 570.6 real, 1133.0 MB
[runlim] sample:		477.7 time, 580.6 real, 1152.6 MB
[runlim] sample:		517.2 time, 590.6 real, 1154.4 MB
[runlim] sample:		556.7 time, 600.6 real, 1173.5 MB
[runlim] sample:		596.2 time, 610.6 real, 1182.1 MB
[runlim] sample:		635.7 time, 620.6 real, 1199.8 MB
[runlim] sample:		675.3 time, 630.6 real, 1226.0 MB
[runlim] sample:		714.8 time, 640.6 real, 1232.4 MB
[runlim] sample:		754.4 time, 650.6 real, 1235.7 MB
[runlim] sample:		793.9 time, 660.6 real, 1245.6 MB
[runlim] sample:		833.4 time, 670.6 real, 1248.9 MB
[runlim] sample:		873.0 time, 680.6 real, 1279.6 MB
[runlim] sample:		912.5 time, 690.6 real, 1266.8 MB
[runlim] sample:		952.1 time, 700.6 real, 1268.6 MB
[runlim] sample:		991.6 time, 710.6 real, 1275.4 MB
[runlim] sample:		1031.1 time, 720.6 real, 1302.6 MB
[runlim] sample:		1070.7 time, 730.6 real, 1303.6 MB
[runlim] sample:		1110.2 time, 740.6 real, 1310.3 MB
[runlim] sample:		1149.7 time, 750.6 real, 1313.3 MB
[runlim] sample:		1189.3 time, 760.6 real, 1322.7 MB
[runlim] sample:		36.3 time, 770.6 real, 671.6 MB
[runlim] sample:		75.8 time, 780.6 real, 704.7 MB
[runlim] sample:		115.3 time, 790.6 real, 725.6 MB
[runlim] sample:		154.8 time, 800.6 real, 737.3 MB
[runlim] sample:		194.4 time, 810.6 real, 750.8 MB
[runlim] sample:		233.9 time, 820.6 real, 763.3 MB
[runlim] sample:		273.4 time, 830.6 real, 791.1 MB
[runlim] sample:		312.9 time, 840.6 real, 800.4 MB
[runlim] sample:		352.4 time, 850.6 real, 803.3 MB
[runlim] sample:		391.9 time, 860.6 real, 799.2 MB
[runlim] sample:		37.4 time, 870.6 real, 618.2 MB
[runlim] sample:		77.0 time, 880.6 real, 663.2 MB
[runlim] sample:		116.5 time, 890.6 real, 677.8 MB
[runlim] sample:		156.1 time, 900.6 real, 696.2 MB
[runlim] sample:		195.7 time, 910.6 real, 721.4 MB
[runlim] sample:		235.2 time, 920.6 real, 742.4 MB
[runlim] sample:		274.8 time, 930.6 real, 749.9 MB
[runlim] sample:		314.4 time, 940.6 real, 772.5 MB
[runlim] sample:		354.0 time, 950.6 real, 789.3 MB
[runlim] sample:		393.5 time, 960.6 real, 801.8 MB
[runlim] sample:		433.1 time, 970.6 real, 787.6 MB
[runlim] sample:		472.6 time, 980.6 real, 792.8 MB
[runlim] sample:		512.2 time, 990.6 real, 820.4 MB
[runlim] sample:		551.8 time, 1000.6 real, 826.2 MB
[runlim] sample:		591.3 time, 1010.6 real, 836.5 MB
[runlim] sample:		630.9 time, 1020.6 real, 843.8 MB
[runlim] sample:		670.4 time, 1030.6 real, 851.9 MB
[runlim] sample:		710.0 time, 1040.6 real, 890.8 MB
[runlim] sample:		749.6 time, 1050.6 real, 899.0 MB
[runlim] sample:		789.1 time, 1060.6 real, 909.9 MB
[runlim] sample:		828.7 time, 1070.6 real, 918.2 MB
[runlim] sample:		868.2 time, 1080.6 real, 925.0 MB
[runlim] sample:		907.8 time, 1090.6 real, 932.0 MB
[runlim] sample:		947.3 time, 1100.6 real, 936.5 MB
[runlim] sample:		986.9 time, 1110.6 real, 940.0 MB
[runlim] sample:		1026.5 time, 1120.6 real, 942.8 MB
[runlim] sample:		1066.0 time, 1130.6 real, 951.7 MB
[runlim] sample:		1105.6 time, 1140.6 real, 973.1 MB
[runlim] sample:		1145.1 time, 1150.6 real, 977.6 MB
[runlim] sample:		1184.7 time, 1160.6 real, 985.0 MB
[runlim] sample:		1224.2 time, 1170.6 real, 986.4 MB
[runlim] sample:		1263.8 time, 1180.6 real, 996.9 MB
[runlim] sample:		1303.3 time, 1190.6 real, 998.1 MB
[runlim] sample:		1342.9 time, 1200.6 real, 1004.2 MB
[runlim] sample:		1382.4 time, 1210.6 real, 1005.2 MB
[runlim] sample:		1422.0 time, 1220.6 real, 1057.8 MB
[runlim] sample:		1461.6 time, 1230.6 real, 1060.1 MB
[runlim] sample:		1501.1 time, 1240.6 real, 1062.9 MB
[runlim] sample:		1540.7 time, 1250.6 real, 1069.9 MB
[runlim] sample:		1580.2 time, 1260.6 real, 1070.3 MB
[runlim] sample:		1619.8 time, 1270.6 real, 1072.9 MB
[runlim] sample:		1659.4 time, 1280.6 real, 1079.3 MB
[runlim] sample:		1698.9 time, 1290.6 real, 1081.5 MB
[runlim] sample:		1738.4 time, 1300.6 real, 1087.5 MB
[runlim] sample:		1778.0 time, 1310.6 real, 1090.6 MB
[runlim] sample:		1817.6 time, 1320.6 real, 1094.4 MB
[runlim] sample:		1857.1 time, 1330.6 real, 1099.9 MB
[runlim] sample:		1896.7 time, 1340.6 real, 1103.5 MB
[runlim] sample:		1936.2 time, 1350.6 real, 1104.8 MB
[runlim] sample:		1975.8 time, 1360.6 real, 1111.4 MB
[runlim] sample:		2015.3 time, 1370.6 real, 1116.4 MB
[runlim] sample:		2054.9 time, 1380.6 real, 1117.9 MB
[runlim] sample:		2094.5 time, 1390.6 real, 1126.1 MB
[runlim] sample:		2134.0 time, 1400.6 real, 1129.9 MB
[runlim] sample:		2173.6 time, 1410.6 real, 1130.8 MB
[runlim] sample:		2213.2 time, 1420.6 real, 1132.4 MB
[runlim] sample:		2252.7 time, 1430.6 real, 1135.4 MB
[runlim] sample:		2292.3 time, 1440.6 real, 1143.4 MB
[runlim] sample:		2331.9 time, 1450.6 real, 1146.2 MB
[runlim] sample:		2371.4 time, 1460.6 real, 1147.3 MB
[runlim] sample:		2411.0 time, 1470.6 real, 1092.3 MB
[runlim] sample:		2450.5 time, 1480.6 real, 1098.1 MB
[runlim] sample:		2490.1 time, 1490.6 real, 1101.6 MB
[runlim] sample:		2529.6 time, 1500.6 real, 1108.3 MB
[runlim] sample:		2569.2 time, 1510.6 real, 1111.1 MB
[runlim] sample:		2608.8 time, 1520.6 real, 1113.1 MB
[runlim] sample:		2648.3 time, 1530.6 real, 1117.7 MB
[runlim] sample:		2687.9 time, 1540.6 real, 1125.3 MB
[runlim] sample:		2727.5 time, 1550.6 real, 1128.0 MB
[runlim] sample:		2767.0 time, 1560.6 real, 1131.3 MB
[runlim] sample:		2806.6 time, 1570.6 real, 1133.4 MB
[runlim] sample:		2846.1 time, 1580.6 real, 1143.3 MB
[runlim] sample:		2885.7 time, 1590.6 real, 1146.7 MB
[runlim] sample:		2925.2 time, 1600.6 real, 1150.2 MB
[runlim] sample:		2964.8 time, 1610.6 real, 1170.4 MB
[runlim] sample:		3004.4 time, 1620.6 real, 1177.5 MB
[runlim] sample:		3043.9 time, 1630.6 real, 1178.8 MB
[runlim] sample:		3083.5 time, 1640.6 real, 1183.1 MB
[runlim] sample:		3123.0 time, 1650.6 real, 1197.1 MB
[runlim] sample:		3162.6 time, 1660.6 real, 1200.6 MB
[runlim] sample:		3202.1 time, 1670.6 real, 1204.5 MB
[runlim] sample:		3241.7 time, 1680.6 real, 1214.0 MB
[runlim] sample:		3281.2 time, 1690.6 real, 1217.0 MB
[runlim] sample:		3320.8 time, 1700.6 real, 1194.6 MB
[runlim] sample:		3360.3 time, 1710.6 real, 1197.9 MB
[runlim] sample:		3399.8 time, 1720.6 real, 1206.3 MB
[runlim] sample:		3439.4 time, 1730.6 real, 1208.9 MB
[runlim] sample:		3478.9 time, 1740.6 real, 1212.4 MB
[runlim] sample:		3518.5 time, 1750.6 real, 1216.7 MB
[runlim] sample:		3558.1 time, 1760.6 real, 1225.2 MB
[runlim] sample:		3597.6 time, 1770.6 real, 1228.5 MB
[runlim] sample:		3637.2 time, 1780.6 real, 1230.5 MB
[runlim] sample:		3676.8 time, 1790.6 real, 1233.0 MB
[runlim] sample:		3716.3 time, 1800.6 real, 1234.5 MB
[runlim] sample:		3755.9 time, 1810.6 real, 1246.7 MB
[runlim] sample:		3795.4 time, 1820.6 real, 1249.0 MB
[runlim] sample:		3835.0 time, 1830.6 real, 1253.0 MB
[runlim] sample:		3874.5 time, 1840.6 real, 1255.9 MB
[runlim] sample:		3914.1 time, 1850.6 real, 1259.1 MB
[runlim] sample:		3953.6 time, 1860.6 real, 1267.8 MB
[runlim] sample:		3993.1 time, 1870.6 real, 1270.2 MB
[runlim] sample:		4032.7 time, 1880.6 real, 1272.0 MB
[runlim] sample:		4072.2 time, 1890.6 real, 1276.6 MB
[runlim] sample:		4111.8 time, 1900.6 real, 1278.2 MB
[runlim] sample:		4151.3 time, 1910.6 real, 1291.4 MB
[runlim] sample:		4190.9 time, 1920.6 real, 1293.5 MB
[runlim] sample:		4230.5 time, 1930.6 real, 1295.3 MB
[runlim] sample:		4270.0 time, 1940.6 real, 1299.8 MB
[runlim] sample:		4309.6 time, 1950.6 real, 1302.7 MB
[runlim] sample:		4349.2 time, 1960.6 real, 1313.4 MB
[runlim] sample:		4388.7 time, 1970.6 real, 1317.7 MB
[runlim] sample:		4428.3 time, 1980.6 real, 1319.8 MB
[runlim] sample:		4467.8 time, 1990.6 real, 1323.8 MB
[runlim] sample:		4507.4 time, 2000.6 real, 1329.0 MB
[runlim] sample:		4547.0 time, 2010.6 real, 1329.7 MB
[runlim] sample:		4586.5 time, 2020.6 real, 1334.1 MB
[runlim] sample:		4626.1 time, 2030.6 real, 1338.1 MB
[runlim] sample:		4665.7 time, 2040.6 real, 1343.9 MB
[runlim] sample:		4705.2 time, 2050.6 real, 1348.7 MB
[runlim] sample:		4744.8 time, 2060.6 real, 1351.5 MB
[runlim] sample:		4784.4 time, 2070.6 real, 1353.8 MB
[runlim] sample:		4823.9 time, 2080.6 real, 1361.5 MB
[runlim] sample:		4863.5 time, 2090.6 real, 1364.1 MB
[runlim] sample:		4903.0 time, 2100.6 real, 1366.1 MB
[runlim] sample:		4942.6 time, 2110.6 real, 1375.5 MB
[runlim] sample:		4982.2 time, 2120.6 real, 1380.4 MB
[runlim] sample:		5021.8 time, 2130.6 real, 1385.7 MB
[runlim] sample:		5061.3 time, 2140.6 real, 1391.0 MB
[runlim] sample:		5100.9 time, 2150.6 real, 1464.2 MB
[runlim] sample:		5140.5 time, 2160.6 real, 1467.5 MB
[runlim] sample:		5180.0 time, 2170.6 real, 1469.0 MB
[runlim] sample:		5219.6 time, 2180.6 real, 1470.9 MB
[runlim] sample:		5259.2 time, 2190.6 real, 1473.4 MB
[runlim] sample:		5298.7 time, 2200.6 real, 1476.9 MB
[runlim] sample:		5338.3 time, 2210.6 real, 1481.1 MB
[runlim] sample:		5377.9 time, 2220.6 real, 1483.3 MB
[runlim] sample:		5417.4 time, 2230.6 real, 1485.1 MB
[runlim] sample:		5457.0 time, 2240.6 real, 1410.5 MB
[runlim] sample:		5496.6 time, 2250.6 real, 1418.8 MB
[runlim] sample:		5536.1 time, 2260.6 real, 1426.1 MB
[runlim] sample:		5575.7 time, 2270.6 real, 1431.8 MB
[runlim] sample:		5615.3 time, 2280.6 real, 1435.8 MB
[runlim] sample:		5654.8 time, 2290.6 real, 1473.7 MB
[runlim] sample:		5694.4 time, 2300.6 real, 1481.0 MB
[runlim] sample:		5733.9 time, 2310.6 real, 1485.6 MB
[runlim] sample:		5773.5 time, 2320.6 real, 1488.1 MB
[runlim] sample:		5813.1 time, 2330.6 real, 1491.3 MB
[runlim] sample:		5852.7 time, 2340.6 real, 1498.2 MB
[runlim] sample:		5892.2 time, 2350.6 real, 1502.0 MB
[runlim] sample:		5931.8 time, 2360.6 real, 1503.3 MB
[runlim] sample:		5971.4 time, 2370.6 real, 1506.9 MB
[runlim] sample:		6011.0 time, 2380.6 real, 1516.2 MB
[runlim] sample:		6050.6 time, 2390.6 real, 1522.5 MB
[runlim] sample:		6090.1 time, 2400.6 real, 1525.5 MB
[runlim] sample:		6129.7 time, 2410.6 real, 1530.4 MB
[runlim] sample:		6169.2 time, 2420.6 real, 1533.6 MB
[runlim] sample:		6208.8 time, 2430.6 real, 1544.5 MB
[runlim] sample:		6248.4 time, 2440.6 real, 1547.4 MB
[runlim] sample:		6287.9 time, 2450.6 real, 1554.9 MB
[runlim] sample:		6327.5 time, 2460.6 real, 1560.7 MB
[runlim] sample:		6367.1 time, 2470.6 real, 1564.8 MB
[runlim] sample:		6406.6 time, 2480.6 real, 1570.6 MB
[runlim] sample:		6446.2 time, 2490.6 real, 1573.9 MB
[runlim] sample:		6485.7 time, 2500.6 real, 1584.8 MB
[runlim] sample:		6525.3 time, 2510.6 real, 1594.1 MB
[runlim] sample:		6564.9 time, 2520.6 real, 1598.4 MB
[runlim] sample:		6604.4 time, 2530.6 real, 1599.9 MB
[runlim] sample:		6644.0 time, 2540.6 real, 1600.9 MB
[runlim] sample:		6683.6 time, 2550.6 real, 1606.3 MB
[runlim] sample:		6723.1 time, 2560.6 real, 1606.5 MB
[runlim] sample:		6762.7 time, 2570.6 real, 1608.8 MB
[runlim] sample:		6802.2 time, 2580.6 real, 1609.0 MB
[runlim] sample:		6841.8 time, 2590.6 real, 1617.4 MB
[runlim] sample:		6881.4 time, 2600.6 real, 1619.2 MB
[runlim] sample:		6921.0 time, 2610.6 real, 1618.7 MB
[runlim] sample:		6960.5 time, 2620.6 real, 1626.9 MB
[runlim] sample:		7000.1 time, 2630.6 real, 1628.8 MB
[runlim] sample:		7039.7 time, 2640.6 real, 1633.8 MB
[runlim] sample:		7079.2 time, 2650.6 real, 1640.2 MB
[runlim] sample:		7118.8 time, 2660.6 real, 1643.5 MB
[runlim] sample:		7158.4 time, 2670.6 real, 1648.4 MB
[runlim] sample:		7198.0 time, 2680.6 real, 1656.3 MB
[runlim] sample:		7237.5 time, 2690.6 real, 1658.5 MB
[runlim] sample:		7277.1 time, 2700.6 real, 1659.0 MB
[runlim] sample:		7316.7 time, 2710.6 real, 1659.2 MB
[runlim] sample:		7356.3 time, 2720.6 real, 1662.8 MB
[runlim] sample:		7395.8 time, 2730.6 real, 1666.3 MB
[runlim] sample:		7435.4 time, 2740.6 real, 1675.4 MB
[runlim] sample:		7475.0 time, 2750.6 real, 1676.4 MB
[runlim] sample:		7514.6 time, 2760.6 real, 1677.5 MB
[runlim] sample:		7554.1 time, 2770.6 real, 1681.0 MB
[runlim] sample:		7593.7 time, 2780.6 real, 1682.1 MB
[runlim] sample:		7633.3 time, 2790.6 real, 1689.0 MB
[runlim] sample:		7672.8 time, 2800.6 real, 1692.5 MB
[runlim] sample:		7712.4 time, 2810.6 real, 1693.5 MB
[runlim] sample:		7751.9 time, 2820.6 real, 1697.1 MB
[runlim] sample:		7791.5 time, 2830.6 real, 1703.1 MB
[runlim] sample:		7831.0 time, 2840.6 real, 1706.6 MB
[runlim] sample:		7870.6 time, 2850.6 real, 1707.7 MB
[runlim] sample:		7910.2 time, 2860.6 real, 1709.0 MB
[runlim] sample:		7949.8 time, 2870.6 real, 1716.1 MB
[runlim] sample:		7989.3 time, 2880.6 real, 1717.9 MB
[runlim] sample:		8028.9 time, 2890.6 real, 1727.4 MB
[runlim] sample:		8068.5 time, 2900.6 real, 1729.9 MB
[runlim] sample:		8108.1 time, 2910.6 real, 1731.9 MB
[runlim] sample:		8147.7 time, 2920.6 real, 1732.2 MB
[runlim] sample:		8187.2 time, 2930.6 real, 1738.7 MB
[runlim] sample:		8226.8 time, 2940.6 real, 1740.7 MB
[runlim] sample:		8266.4 time, 2950.6 real, 1741.2 MB
[runlim] sample:		8306.0 time, 2960.6 real, 1743.0 MB
[runlim] sample:		8345.5 time, 2970.6 real, 1744.3 MB
[runlim] sample:		8385.1 time, 2980.6 real, 1747.1 MB
[runlim] sample:		8424.7 time, 2990.6 real, 1748.3 MB
[runlim] sample:		8464.3 time, 3000.6 real, 1774.4 MB
[runlim] sample:		8503.8 time, 3010.6 real, 1774.4 MB
[runlim] sample:		8543.4 time, 3020.6 real, 1784.5 MB
[runlim] sample:		8583.0 time, 3030.6 real, 1784.6 MB
[runlim] sample:		8622.6 time, 3040.6 real, 1786.1 MB
[runlim] sample:		8662.1 time, 3050.6 real, 1788.9 MB
[runlim] sample:		8701.7 time, 3060.6 real, 1792.0 MB
[runlim] sample:		8741.3 time, 3070.6 real, 1678.5 MB
[runlim] sample:		8780.9 time, 3080.6 real, 1690.7 MB
[runlim] sample:		8820.5 time, 3090.6 real, 1691.7 MB
[runlim] sample:		8860.0 time, 3100.6 real, 1697.8 MB
[runlim] sample:		8899.6 time, 3110.6 real, 1700.6 MB
[runlim] sample:		8939.2 time, 3120.6 real, 1701.6 MB
[runlim] sample:		8978.8 time, 3130.6 real, 1707.5 MB
[runlim] sample:		9018.3 time, 3140.6 real, 1712.1 MB
[runlim] sample:		9057.9 time, 3150.6 real, 1716.9 MB
[runlim] sample:		9097.5 time, 3160.6 real, 1720.5 MB
[runlim] sample:		9137.0 time, 3170.6 real, 1750.5 MB
[runlim] sample:		9176.6 time, 3180.6 real, 1754.3 MB
[runlim] sample:		9216.2 time, 3190.6 real, 1763.5 MB
[runlim] sample:		9255.8 time, 3200.6 real, 1766.2 MB
[runlim] sample:		9295.4 time, 3210.6 real, 1767.5 MB
[runlim] sample:		9335.0 time, 3220.6 real, 1736.2 MB
[runlim] sample:		9374.5 time, 3230.6 real, 1738.5 MB
[runlim] sample:		9414.1 time, 3240.6 real, 1742.1 MB
[runlim] sample:		9453.7 time, 3250.6 real, 1745.7 MB
[runlim] sample:		9493.2 time, 3260.6 real, 1746.7 MB
[runlim] sample:		9532.8 time, 3270.6 real, 1751.7 MB
[runlim] sample:		9572.4 time, 3280.6 real, 1761.6 MB
[runlim] sample:		9612.0 time, 3290.6 real, 1766.7 MB
[runlim] sample:		9651.5 time, 3300.6 real, 1772.2 MB
[runlim] sample:		9691.1 time, 3310.6 real, 1773.5 MB
[runlim] sample:		9730.7 time, 3320.6 real, 1807.8 MB
[runlim] sample:		9770.3 time, 3330.6 real, 1812.9 MB
[runlim] sample:		9809.8 time, 3340.6 real, 1815.6 MB
[runlim] sample:		9849.4 time, 3350.6 real, 1822.8 MB
[runlim] sample:		9889.0 time, 3360.6 real, 1825.8 MB
[runlim] sample:		9928.6 time, 3370.6 real, 1828.7 MB
[runlim] sample:		9968.2 time, 3380.6 real, 1832.8 MB
[runlim] sample:		10007.8 time, 3390.6 real, 1841.8 MB
[runlim] sample:		10047.3 time, 3400.6 real, 1845.4 MB
[runlim] sample:		10086.9 time, 3410.6 real, 1848.4 MB
[runlim] sample:		10126.4 time, 3420.6 real, 1851.4 MB
[runlim] sample:		10166.0 time, 3430.6 real, 1856.3 MB
[runlim] sample:		10205.6 time, 3440.6 real, 1857.4 MB
[runlim] sample:		10245.1 time, 3450.6 real, 1863.3 MB
[runlim] sample:		10284.7 time, 3460.6 real, 1868.7 MB
[runlim] sample:		10324.2 time, 3470.6 real, 1871.9 MB
[runlim] sample:		10363.8 time, 3480.6 real, 1880.9 MB
[runlim] sample:		10403.4 time, 3490.6 real, 1884.0 MB
[runlim] sample:		10442.9 time, 3500.6 real, 1887.3 MB
[runlim] sample:		10482.5 time, 3510.6 real, 1888.3 MB
[runlim] sample:		10522.1 time, 3520.6 real, 1891.8 MB
[runlim] sample:		10561.7 time, 3530.6 real, 1894.6 MB
[runlim] sample:		10601.3 time, 3540.6 real, 1895.4 MB
[runlim] sample:		10640.8 time, 3550.6 real, 1904.0 MB
[runlim] sample:		10680.4 time, 3560.6 real, 1905.3 MB
[runlim] sample:		10720.0 time, 3570.6 real, 1908.3 MB
[runlim] sample:		10759.5 time, 3580.6 real, 1909.1 MB
[runlim] sample:		10799.1 time, 3590.6 real, 1910.8 MB
[runlim] end:			Tue Sep 15 18:00:14 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		471737
[runlim] real:			3600.04 seconds
[runlim] time:			10836.33 seconds
[runlim] space:			1914.9 MB
[runlim] samples:		35994
