[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/iprover/single.iproverdeep
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/hwmcc14/single/6s105.aig
[runlim] start:			Tue Sep 15 16:00:06 2015
[runlim] main pid:		29101
[runlim] sample:		2.8 time, 10.9 real, 105.5 MB
[runlim] sample:		12.7 time, 20.9 real, 271.8 MB
[runlim] sample:		22.7 time, 30.9 real, 401.6 MB
[runlim] sample:		32.7 time, 40.9 real, 555.9 MB
[runlim] sample:		42.7 time, 50.9 real, 665.5 MB
[runlim] sample:		52.7 time, 60.9 real, 667.5 MB
[runlim] sample:		62.7 time, 70.9 real, 711.0 MB
[runlim] sample:		72.7 time, 80.9 real, 781.2 MB
[runlim] sample:		82.6 time, 90.9 real, 790.4 MB
[runlim] sample:		92.6 time, 100.9 real, 785.9 MB
[runlim] sample:		102.6 time, 110.9 real, 791.9 MB
[runlim] sample:		112.6 time, 120.9 real, 865.6 MB
[runlim] sample:		122.6 time, 130.9 real, 870.9 MB
[runlim] sample:		132.6 time, 140.9 real, 878.9 MB
[runlim] sample:		142.5 time, 150.9 real, 914.1 MB
[runlim] sample:		152.5 time, 160.9 real, 878.9 MB
[runlim] sample:		162.5 time, 170.9 real, 878.9 MB
[runlim] sample:		172.5 time, 180.9 real, 902.7 MB
[runlim] sample:		182.5 time, 190.9 real, 983.4 MB
[runlim] sample:		192.5 time, 200.9 real, 983.4 MB
[runlim] sample:		202.4 time, 210.9 real, 993.4 MB
[runlim] sample:		212.4 time, 220.9 real, 993.4 MB
[runlim] sample:		222.4 time, 230.9 real, 993.4 MB
[runlim] sample:		232.4 time, 240.9 real, 1029.9 MB
[runlim] sample:		242.4 time, 250.9 real, 1035.9 MB
[runlim] sample:		252.4 time, 260.9 real, 996.7 MB
[runlim] sample:		262.4 time, 270.9 real, 996.7 MB
[runlim] sample:		272.3 time, 280.9 real, 996.7 MB
[runlim] sample:		282.3 time, 290.9 real, 1027.9 MB
[runlim] sample:		292.3 time, 300.9 real, 1031.9 MB
[runlim] sample:		302.3 time, 310.9 real, 1046.1 MB
[runlim] sample:		312.3 time, 320.9 real, 1046.1 MB
[runlim] sample:		322.3 time, 330.9 real, 1046.1 MB
[runlim] sample:		332.3 time, 340.9 real, 1046.1 MB
[runlim] sample:		342.2 time, 350.9 real, 1079.4 MB
[runlim] sample:		352.2 time, 360.9 real, 1083.4 MB
[runlim] sample:		362.2 time, 370.9 real, 1089.4 MB
[runlim] sample:		372.2 time, 380.9 real, 1046.3 MB
[runlim] sample:		382.2 time, 390.9 real, 1046.3 MB
[runlim] sample:		392.2 time, 400.9 real, 1046.3 MB
[runlim] sample:		402.1 time, 410.9 real, 1081.5 MB
[runlim] sample:		412.1 time, 420.9 real, 1087.5 MB
[runlim] sample:		422.1 time, 430.9 real, 1091.5 MB
[runlim] sample:		432.1 time, 440.9 real, 1097.7 MB
[runlim] sample:		442.1 time, 450.9 real, 1046.3 MB
[runlim] sample:		452.1 time, 460.9 real, 1046.3 MB
[runlim] sample:		462.1 time, 470.9 real, 1046.3 MB
[runlim] sample:		472.1 time, 480.9 real, 1079.5 MB
[runlim] sample:		482.0 time, 490.9 real, 1071.7 MB
[runlim] sample:		492.0 time, 500.9 real, 1071.7 MB
[runlim] sample:		502.0 time, 510.9 real, 1071.7 MB
[runlim] sample:		512.0 time, 520.9 real, 1107.0 MB
[runlim] sample:		522.0 time, 530.9 real, 1113.0 MB
[runlim] sample:		532.0 time, 540.9 real, 1071.8 MB
[runlim] sample:		542.0 time, 550.9 real, 1079.8 MB
[runlim] sample:		551.9 time, 560.9 real, 1079.8 MB
[runlim] sample:		561.9 time, 570.9 real, 1111.0 MB
[runlim] sample:		571.9 time, 580.9 real, 1117.0 MB
[runlim] sample:		581.9 time, 590.9 real, 1121.0 MB
[runlim] sample:		591.9 time, 600.9 real, 1125.0 MB
[runlim] sample:		601.9 time, 610.9 real, 1079.8 MB
[runlim] sample:		611.9 time, 620.9 real, 1079.8 MB
[runlim] sample:		621.8 time, 630.9 real, 1111.0 MB
[runlim] sample:		631.8 time, 640.9 real, 1115.0 MB
[runlim] sample:		641.8 time, 650.9 real, 1119.0 MB
[runlim] sample:		651.8 time, 660.9 real, 1125.0 MB
[runlim] sample:		661.8 time, 670.9 real, 1127.2 MB
[runlim] sample:		671.8 time, 680.9 real, 1133.2 MB
[runlim] sample:		681.7 time, 690.9 real, 1079.8 MB
[runlim] sample:		691.7 time, 700.9 real, 1079.8 MB
[runlim] sample:		701.7 time, 710.9 real, 1079.8 MB
[runlim] sample:		711.7 time, 720.9 real, 1111.0 MB
[runlim] sample:		721.7 time, 730.9 real, 1115.0 MB
[runlim] sample:		731.7 time, 740.9 real, 1121.0 MB
[runlim] sample:		741.6 time, 750.9 real, 1127.0 MB
[runlim] sample:		751.6 time, 760.9 real, 1129.0 MB
[runlim] sample:		761.6 time, 770.9 real, 1133.2 MB
[runlim] sample:		771.6 time, 780.9 real, 1079.8 MB
[runlim] sample:		781.6 time, 790.9 real, 1079.8 MB
[runlim] sample:		791.6 time, 800.9 real, 1124.1 MB
[runlim] sample:		801.6 time, 810.9 real, 1151.1 MB
[runlim] sample:		811.5 time, 820.9 real, 1159.1 MB
[runlim] sample:		821.5 time, 830.9 real, 1197.3 MB
[runlim] sample:		831.5 time, 840.9 real, 1203.3 MB
[runlim] sample:		841.5 time, 850.9 real, 1209.3 MB
[runlim] sample:		851.5 time, 860.9 real, 1213.6 MB
[runlim] sample:		861.5 time, 870.9 real, 1164.2 MB
[runlim] sample:		871.5 time, 880.9 real, 1164.2 MB
[runlim] sample:		881.4 time, 890.9 real, 1195.4 MB
[runlim] sample:		891.4 time, 900.9 real, 1203.4 MB
[runlim] sample:		901.4 time, 910.9 real, 1209.4 MB
[runlim] sample:		911.4 time, 920.9 real, 1213.4 MB
[runlim] sample:		921.4 time, 930.9 real, 1219.6 MB
[runlim] sample:		931.4 time, 940.9 real, 1223.6 MB
[runlim] sample:		941.4 time, 950.9 real, 1164.2 MB
[runlim] sample:		951.3 time, 960.9 real, 1164.2 MB
[runlim] sample:		961.3 time, 970.9 real, 1164.2 MB
[runlim] sample:		971.3 time, 980.9 real, 1199.4 MB
[runlim] sample:		981.3 time, 990.9 real, 1205.4 MB
[runlim] sample:		991.3 time, 1000.9 real, 1211.4 MB
[runlim] sample:		1001.3 time, 1010.9 real, 1215.6 MB
[runlim] sample:		1011.3 time, 1020.9 real, 1219.6 MB
[runlim] sample:		1021.2 time, 1030.9 real, 1221.6 MB
[runlim] sample:		1031.2 time, 1040.9 real, 1225.6 MB
[runlim] sample:		1041.2 time, 1050.9 real, 1164.2 MB
[runlim] sample:		1051.2 time, 1060.9 real, 1164.2 MB
[runlim] sample:		1061.2 time, 1070.9 real, 1164.2 MB
[runlim] sample:		1071.2 time, 1080.9 real, 1195.4 MB
[runlim] sample:		1081.2 time, 1090.9 real, 1201.4 MB
[runlim] sample:		1091.1 time, 1100.9 real, 1205.4 MB
[runlim] sample:		1101.1 time, 1110.9 real, 1211.4 MB
[runlim] sample:		1111.1 time, 1120.9 real, 1215.6 MB
[runlim] sample:		1121.1 time, 1130.9 real, 1217.6 MB
[runlim] sample:		1131.1 time, 1140.9 real, 1223.6 MB
[runlim] sample:		1141.1 time, 1150.9 real, 1227.6 MB
[runlim] sample:		1151.0 time, 1160.9 real, 1231.6 MB
[runlim] sample:		1161.0 time, 1170.9 real, 1164.2 MB
[runlim] sample:		1171.0 time, 1180.9 real, 1164.2 MB
[runlim] sample:		1181.0 time, 1190.9 real, 1145.0 MB
[runlim] sample:		1191.0 time, 1200.9 real, 1198.3 MB
[runlim] sample:		1201.0 time, 1210.9 real, 1208.3 MB
[runlim] sample:		1211.0 time, 1220.9 real, 1218.3 MB
[runlim] sample:		1221.0 time, 1230.9 real, 1232.5 MB
[runlim] sample:		1230.9 time, 1240.9 real, 1232.5 MB
[runlim] sample:		1240.9 time, 1250.9 real, 1232.5 MB
[runlim] sample:		1250.9 time, 1260.9 real, 1264.0 MB
[runlim] sample:		1260.9 time, 1270.9 real, 1270.0 MB
[runlim] sample:		1270.9 time, 1280.9 real, 1272.0 MB
[runlim] sample:		1280.8 time, 1290.9 real, 1276.0 MB
[runlim] sample:		1290.8 time, 1300.9 real, 1232.5 MB
[runlim] sample:		1300.8 time, 1310.9 real, 1232.5 MB
[runlim] sample:		1310.8 time, 1320.9 real, 1232.5 MB
[runlim] sample:		1320.8 time, 1330.9 real, 1264.0 MB
[runlim] sample:		1330.8 time, 1340.9 real, 1268.0 MB
[runlim] sample:		1340.8 time, 1350.9 real, 1274.0 MB
[runlim] sample:		1350.8 time, 1360.9 real, 1278.0 MB
[runlim] sample:		1360.7 time, 1370.9 real, 1282.0 MB
[runlim] sample:		1370.7 time, 1380.9 real, 1287.2 MB
[runlim] sample:		1380.7 time, 1390.9 real, 1293.2 MB
[runlim] sample:		1390.7 time, 1400.9 real, 1233.6 MB
[runlim] sample:		1400.7 time, 1410.9 real, 1233.6 MB
[runlim] sample:		1410.7 time, 1420.9 real, 1269.1 MB
[runlim] sample:		1420.7 time, 1430.9 real, 1275.1 MB
[runlim] sample:		1430.6 time, 1440.9 real, 1284.8 MB
[runlim] sample:		1440.6 time, 1450.9 real, 1291.0 MB
[runlim] sample:		1450.6 time, 1460.9 real, 1293.0 MB
[runlim] sample:		1460.6 time, 1470.9 real, 1299.0 MB
[runlim] sample:		1470.6 time, 1480.9 real, 1301.0 MB
[runlim] sample:		1480.6 time, 1490.9 real, 1305.0 MB
[runlim] sample:		1490.5 time, 1500.9 real, 1311.0 MB
[runlim] sample:		1500.5 time, 1510.9 real, 1235.4 MB
[runlim] sample:		1510.5 time, 1520.9 real, 1235.4 MB
[runlim] sample:		1520.5 time, 1530.9 real, 1268.9 MB
[runlim] sample:		1530.5 time, 1540.9 real, 1274.9 MB
[runlim] sample:		1540.5 time, 1550.9 real, 1278.9 MB
[runlim] sample:		1550.5 time, 1560.9 real, 1282.9 MB
[runlim] sample:		1560.5 time, 1570.9 real, 1287.1 MB
[runlim] sample:		1570.4 time, 1580.9 real, 1291.1 MB
[runlim] sample:		1580.4 time, 1590.9 real, 1297.1 MB
[runlim] sample:		1590.4 time, 1600.9 real, 1301.1 MB
[runlim] sample:		1600.4 time, 1610.9 real, 1305.1 MB
[runlim] sample:		1610.4 time, 1620.9 real, 1309.1 MB
[runlim] sample:		1620.3 time, 1630.9 real, 1235.4 MB
[runlim] sample:		1630.3 time, 1640.9 real, 1235.4 MB
[runlim] sample:		1640.3 time, 1650.9 real, 1266.9 MB
[runlim] sample:		1650.3 time, 1660.9 real, 1272.9 MB
[runlim] sample:		1660.3 time, 1670.9 real, 1278.9 MB
[runlim] sample:		1670.3 time, 1680.9 real, 1282.9 MB
[runlim] sample:		1680.3 time, 1690.9 real, 1289.1 MB
[runlim] sample:		1690.2 time, 1700.9 real, 1295.1 MB
[runlim] sample:		1700.2 time, 1710.9 real, 1297.1 MB
[runlim] sample:		1710.2 time, 1720.9 real, 1301.1 MB
[runlim] sample:		1720.2 time, 1730.9 real, 1303.1 MB
[runlim] sample:		1730.2 time, 1740.9 real, 1305.1 MB
[runlim] sample:		1740.2 time, 1750.9 real, 1311.1 MB
[runlim] sample:		1750.2 time, 1760.9 real, 1313.6 MB
[runlim] sample:		1760.2 time, 1770.9 real, 1235.4 MB
[runlim] sample:		1770.1 time, 1780.9 real, 1309.5 MB
[runlim] sample:		1780.1 time, 1790.9 real, 1309.5 MB
[runlim] sample:		1790.1 time, 1800.9 real, 1309.5 MB
[runlim] sample:		1800.1 time, 1810.9 real, 1329.5 MB
[runlim] sample:		1810.1 time, 1820.9 real, 1330.0 MB
[runlim] sample:		1820.1 time, 1830.9 real, 1363.5 MB
[runlim] sample:		1830.0 time, 1840.9 real, 1367.5 MB
[runlim] sample:		1840.0 time, 1850.9 real, 1373.5 MB
[runlim] sample:		1850.0 time, 1860.9 real, 1377.5 MB
[runlim] sample:		1860.0 time, 1870.9 real, 1381.6 MB
[runlim] sample:		1870.0 time, 1880.9 real, 1330.0 MB
[runlim] sample:		1880.0 time, 1890.9 real, 1330.0 MB
[runlim] sample:		1890.0 time, 1900.9 real, 1330.0 MB
[runlim] sample:		1900.0 time, 1910.9 real, 1365.5 MB
[runlim] sample:		1909.9 time, 1920.9 real, 1369.5 MB
[runlim] sample:		1919.9 time, 1930.9 real, 1373.5 MB
[runlim] sample:		1929.9 time, 1940.9 real, 1377.9 MB
[runlim] sample:		1939.9 time, 1950.9 real, 1383.7 MB
[runlim] sample:		1949.9 time, 1960.9 real, 1389.7 MB
[runlim] sample:		1959.9 time, 1970.9 real, 1330.0 MB
[runlim] sample:		1969.8 time, 1980.9 real, 1330.0 MB
[runlim] sample:		1979.8 time, 1990.9 real, 1330.0 MB
[runlim] sample:		1989.8 time, 2000.9 real, 1367.5 MB
[runlim] sample:		1999.8 time, 2010.9 real, 1373.5 MB
[runlim] sample:		2009.8 time, 2020.9 real, 1377.9 MB
[runlim] sample:		2019.8 time, 2030.9 real, 1383.7 MB
[runlim] sample:		2029.8 time, 2040.9 real, 1389.7 MB
[runlim] sample:		2039.8 time, 2050.9 real, 1393.7 MB
[runlim] sample:		2049.7 time, 2060.9 real, 1397.7 MB
[runlim] sample:		2059.7 time, 2070.9 real, 1401.7 MB
[runlim] sample:		2069.7 time, 2080.9 real, 1405.7 MB
[runlim] sample:		2079.7 time, 2090.9 real, 1330.0 MB
[runlim] sample:		2089.7 time, 2100.9 real, 1330.0 MB
[runlim] sample:		2099.7 time, 2110.9 real, 1363.5 MB
[runlim] sample:		2109.6 time, 2120.9 real, 1371.5 MB
[runlim] sample:		2119.6 time, 2130.9 real, 1377.5 MB
[runlim] sample:		2129.6 time, 2140.9 real, 1383.7 MB
[runlim] sample:		2139.6 time, 2150.9 real, 1385.7 MB
[runlim] sample:		2149.6 time, 2160.9 real, 1389.7 MB
[runlim] sample:		2159.6 time, 2170.9 real, 1395.7 MB
[runlim] sample:		2169.6 time, 2180.9 real, 1401.7 MB
[runlim] sample:		2179.5 time, 2190.9 real, 1405.7 MB
[runlim] sample:		2189.5 time, 2200.9 real, 1410.7 MB
[runlim] sample:		2199.5 time, 2210.9 real, 1330.0 MB
[runlim] sample:		2209.5 time, 2220.9 real, 1330.0 MB
[runlim] sample:		2219.5 time, 2230.9 real, 1367.5 MB
[runlim] sample:		2229.5 time, 2240.9 real, 1375.5 MB
[runlim] sample:		2239.4 time, 2250.9 real, 1381.7 MB
[runlim] sample:		2249.4 time, 2260.9 real, 1387.7 MB
[runlim] sample:		2259.4 time, 2270.9 real, 1393.7 MB
[runlim] sample:		2269.4 time, 2280.9 real, 1397.7 MB
[runlim] sample:		2279.4 time, 2290.9 real, 1407.7 MB
[runlim] sample:		2289.4 time, 2300.9 real, 1342.0 MB
[runlim] sample:		2299.4 time, 2310.9 real, 1342.0 MB
[runlim] sample:		2309.3 time, 2320.9 real, 1377.5 MB
[runlim] sample:		2319.3 time, 2330.9 real, 1381.5 MB
[runlim] sample:		2329.3 time, 2340.9 real, 1387.5 MB
[runlim] sample:		2339.3 time, 2350.9 real, 1390.7 MB
[runlim] sample:		2349.3 time, 2360.9 real, 1395.7 MB
[runlim] sample:		2359.3 time, 2370.9 real, 1342.0 MB
[runlim] sample:		2369.3 time, 2380.9 real, 1342.0 MB
[runlim] sample:		2379.2 time, 2390.9 real, 1375.5 MB
[runlim] sample:		2389.2 time, 2400.9 real, 1381.5 MB
[runlim] sample:		2399.2 time, 2410.9 real, 1385.5 MB
[runlim] sample:		2409.2 time, 2420.9 real, 1389.5 MB
[runlim] sample:		2419.2 time, 2430.9 real, 1391.4 MB
[runlim] sample:		2429.2 time, 2440.9 real, 1395.7 MB
[runlim] sample:		2439.2 time, 2450.9 real, 1397.7 MB
[runlim] sample:		2449.2 time, 2460.9 real, 1401.7 MB
[runlim] sample:		2459.1 time, 2470.9 real, 1342.0 MB
[runlim] sample:		2469.1 time, 2480.9 real, 1342.0 MB
[runlim] sample:		2479.1 time, 2490.9 real, 1373.5 MB
[runlim] sample:		2489.1 time, 2500.9 real, 1379.5 MB
[runlim] sample:		2499.1 time, 2510.9 real, 1383.5 MB
[runlim] sample:		2509.1 time, 2520.9 real, 1389.5 MB
[runlim] sample:		2519.1 time, 2530.9 real, 1393.7 MB
[runlim] sample:		2529.0 time, 2540.9 real, 1397.7 MB
[runlim] sample:		2539.0 time, 2550.9 real, 1401.7 MB
[runlim] sample:		2549.0 time, 2560.9 real, 1405.7 MB
[runlim] sample:		2559.0 time, 2570.9 real, 1409.7 MB
[runlim] sample:		2569.0 time, 2580.9 real, 1411.7 MB
[runlim] sample:		2578.9 time, 2590.9 real, 1342.0 MB
[runlim] sample:		2588.9 time, 2600.9 real, 1342.0 MB
[runlim] sample:		2598.9 time, 2610.9 real, 1348.4 MB
[runlim] sample:		2608.9 time, 2620.9 real, 1396.6 MB
[runlim] sample:		2618.9 time, 2630.9 real, 1410.6 MB
[runlim] sample:		2628.9 time, 2640.9 real, 1421.8 MB
[runlim] sample:		2638.9 time, 2650.9 real, 1457.4 MB
[runlim] sample:		2648.9 time, 2660.9 real, 1465.4 MB
[runlim] sample:		2658.8 time, 2670.9 real, 1471.4 MB
[runlim] sample:		2668.8 time, 2680.9 real, 1477.5 MB
[runlim] sample:		2678.8 time, 2690.9 real, 1423.8 MB
[runlim] sample:		2688.8 time, 2700.9 real, 1423.8 MB
[runlim] sample:		2698.8 time, 2710.9 real, 1423.8 MB
[runlim] sample:		2708.8 time, 2720.9 real, 1459.4 MB
[runlim] sample:		2718.8 time, 2730.9 real, 1465.4 MB
[runlim] sample:		2728.7 time, 2740.9 real, 1471.4 MB
[runlim] sample:		2738.7 time, 2750.9 real, 1477.5 MB
[runlim] sample:		2748.7 time, 2760.9 real, 1483.5 MB
[runlim] sample:		2758.7 time, 2770.9 real, 1487.5 MB
[runlim] sample:		2768.7 time, 2780.9 real, 1491.5 MB
[runlim] sample:		2778.7 time, 2790.9 real, 1423.8 MB
[runlim] sample:		2788.7 time, 2800.9 real, 1423.8 MB
[runlim] sample:		2798.6 time, 2810.9 real, 1423.8 MB
[runlim] sample:		2808.6 time, 2820.9 real, 1457.4 MB
[runlim] sample:		2818.6 time, 2830.9 real, 1463.4 MB
[runlim] sample:		2828.6 time, 2840.9 real, 1469.4 MB
[runlim] sample:		2838.6 time, 2850.9 real, 1471.8 MB
[runlim] sample:		2848.6 time, 2860.9 real, 1475.5 MB
[runlim] sample:		2858.5 time, 2870.9 real, 1483.5 MB
[runlim] sample:		2868.5 time, 2880.9 real, 1487.5 MB
[runlim] sample:		2878.5 time, 2890.9 real, 1491.5 MB
[runlim] sample:		2888.5 time, 2900.9 real, 1493.5 MB
[runlim] sample:		2898.5 time, 2910.9 real, 1497.5 MB
[runlim] sample:		2908.5 time, 2920.9 real, 1501.5 MB
[runlim] sample:		2918.5 time, 2930.9 real, 1423.8 MB
[runlim] sample:		2928.4 time, 2940.9 real, 1423.8 MB
[runlim] sample:		2938.4 time, 2950.9 real, 1459.4 MB
[runlim] sample:		2948.4 time, 2960.9 real, 1465.4 MB
[runlim] sample:		2958.4 time, 2970.9 real, 1471.4 MB
[runlim] sample:		2968.4 time, 2980.9 real, 1475.5 MB
[runlim] sample:		2978.4 time, 2990.9 real, 1479.5 MB
[runlim] sample:		2988.4 time, 3000.9 real, 1485.5 MB
[runlim] sample:		2998.3 time, 3010.9 real, 1489.5 MB
[runlim] sample:		3008.3 time, 3020.9 real, 1493.5 MB
[runlim] sample:		3018.3 time, 3030.9 real, 1495.5 MB
[runlim] sample:		3028.3 time, 3040.9 real, 1499.5 MB
[runlim] sample:		3038.3 time, 3050.9 real, 1501.5 MB
[runlim] sample:		3048.3 time, 3060.9 real, 1502.4 MB
[runlim] sample:		3058.2 time, 3070.9 real, 1506.6 MB
[runlim] sample:		3068.2 time, 3080.9 real, 1508.6 MB
[runlim] sample:		3078.2 time, 3090.9 real, 1512.8 MB
[runlim] sample:		3088.2 time, 3100.9 real, 1423.8 MB
[runlim] sample:		3098.2 time, 3110.9 real, 1423.8 MB
[runlim] sample:		3108.2 time, 3120.9 real, 1423.8 MB
[runlim] sample:		3118.1 time, 3130.9 real, 1455.4 MB
[runlim] sample:		3128.1 time, 3140.9 real, 1459.4 MB
[runlim] sample:		3138.1 time, 3150.9 real, 1465.4 MB
[runlim] sample:		3148.1 time, 3160.9 real, 1471.4 MB
[runlim] sample:		3158.1 time, 3170.9 real, 1475.5 MB
[runlim] sample:		3168.1 time, 3180.9 real, 1479.5 MB
[runlim] sample:		3178.1 time, 3190.9 real, 1483.5 MB
[runlim] sample:		3188.0 time, 3200.9 real, 1485.5 MB
[runlim] sample:		3198.0 time, 3210.9 real, 1491.5 MB
[runlim] sample:		3208.0 time, 3220.9 real, 1493.5 MB
[runlim] sample:		3218.0 time, 3230.9 real, 1497.5 MB
[runlim] sample:		3228.0 time, 3240.9 real, 1501.5 MB
[runlim] sample:		3238.0 time, 3250.9 real, 1504.6 MB
[runlim] sample:		3247.9 time, 3260.9 real, 1506.6 MB
[runlim] sample:		3257.9 time, 3270.9 real, 1423.9 MB
[runlim] sample:		3267.9 time, 3280.9 real, 1423.9 MB
[runlim] sample:		3277.9 time, 3290.9 real, 1457.4 MB
[runlim] sample:		3287.9 time, 3300.9 real, 1463.4 MB
[runlim] sample:		3297.9 time, 3310.9 real, 1469.4 MB
[runlim] sample:		3307.9 time, 3320.9 real, 1472.5 MB
[runlim] sample:		3317.8 time, 3330.9 real, 1479.5 MB
[runlim] sample:		3327.8 time, 3340.9 real, 1483.5 MB
[runlim] sample:		3337.8 time, 3350.9 real, 1485.5 MB
[runlim] sample:		3347.8 time, 3360.9 real, 1489.5 MB
[runlim] sample:		3357.8 time, 3370.9 real, 1491.5 MB
[runlim] sample:		3367.8 time, 3380.9 real, 1495.5 MB
[runlim] sample:		3377.8 time, 3390.9 real, 1497.5 MB
[runlim] sample:		3387.7 time, 3400.9 real, 1431.8 MB
[runlim] sample:		3397.7 time, 3410.9 real, 1514.0 MB
[runlim] sample:		3407.7 time, 3420.9 real, 1532.0 MB
[runlim] sample:		3417.7 time, 3430.9 real, 1552.0 MB
[runlim] sample:		3427.7 time, 3440.9 real, 1552.0 MB
[runlim] sample:		3437.7 time, 3450.9 real, 1552.0 MB
[runlim] sample:		3447.7 time, 3460.9 real, 1587.6 MB
[runlim] sample:		3457.6 time, 3470.9 real, 1593.6 MB
[runlim] sample:		3467.6 time, 3480.9 real, 1599.6 MB
[runlim] sample:		3477.6 time, 3490.9 real, 1605.8 MB
[runlim] sample:		3487.6 time, 3500.9 real, 1611.8 MB
[runlim] sample:		3497.6 time, 3510.9 real, 1615.8 MB
[runlim] sample:		3507.6 time, 3520.9 real, 1552.1 MB
[runlim] sample:		3517.6 time, 3530.9 real, 1552.1 MB
[runlim] sample:		3527.5 time, 3540.9 real, 1585.6 MB
[runlim] sample:		3537.5 time, 3550.9 real, 1591.6 MB
[runlim] sample:		3547.5 time, 3560.9 real, 1599.6 MB
[runlim] sample:		3557.5 time, 3570.9 real, 1607.8 MB
[runlim] sample:		3567.5 time, 3580.9 real, 1611.8 MB
[runlim] sample:		3577.5 time, 3590.9 real, 1615.8 MB
[runlim] end:			Tue Sep 15 17:00:06 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		179940
[runlim] real:			3600.10 seconds
[runlim] time:			3586.65 seconds
[runlim] space:			1619.8 MB
[runlim] samples:		35992
