[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.iproverdeephc
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/kenflashp01.aig
[runlim] start:			Mon Sep 28 20:00:06 2015
[runlim] main pid:		19858
[runlim] sample:		9.5 time, 10.4 real, 308.1 MB
[runlim] sample:		19.5 time, 20.4 real, 503.5 MB
[runlim] sample:		29.5 time, 30.4 real, 657.6 MB
[runlim] sample:		39.5 time, 40.4 real, 840.6 MB
[runlim] sample:		49.4 time, 50.4 real, 1022.2 MB
[runlim] sample:		59.4 time, 60.4 real, 1186.6 MB
[runlim] sample:		69.4 time, 70.4 real, 1287.0 MB
[runlim] sample:		79.4 time, 80.4 real, 1438.2 MB
[runlim] sample:		89.4 time, 90.4 real, 1578.3 MB
[runlim] sample:		99.4 time, 100.4 real, 1714.0 MB
[runlim] sample:		109.3 time, 110.4 real, 1855.4 MB
[runlim] sample:		119.3 time, 120.4 real, 1989.3 MB
[runlim] sample:		129.3 time, 130.4 real, 2117.8 MB
[runlim] sample:		139.3 time, 140.4 real, 2256.5 MB
[runlim] sample:		149.3 time, 150.4 real, 2384.7 MB
[runlim] sample:		159.3 time, 160.4 real, 2516.3 MB
[runlim] sample:		169.2 time, 170.4 real, 2583.2 MB
[runlim] sample:		179.2 time, 180.4 real, 2650.2 MB
[runlim] sample:		189.2 time, 190.4 real, 2742.7 MB
[runlim] sample:		199.2 time, 200.4 real, 2828.5 MB
[runlim] sample:		209.2 time, 210.4 real, 2935.6 MB
[runlim] sample:		219.2 time, 220.4 real, 3068.0 MB
[runlim] sample:		229.2 time, 230.4 real, 3191.3 MB
[runlim] sample:		239.1 time, 240.4 real, 3306.1 MB
[runlim] sample:		249.1 time, 250.4 real, 3414.6 MB
[runlim] sample:		259.1 time, 260.4 real, 3527.4 MB
[runlim] sample:		269.1 time, 270.4 real, 3662.3 MB
[runlim] sample:		279.1 time, 280.4 real, 3773.2 MB
[runlim] sample:		289.1 time, 290.4 real, 3885.9 MB
[runlim] sample:		299.1 time, 300.4 real, 3998.3 MB
[runlim] sample:		309.1 time, 310.4 real, 4111.6 MB
[runlim] sample:		319.0 time, 320.4 real, 4222.3 MB
[runlim] sample:		329.0 time, 330.4 real, 4346.8 MB
[runlim] sample:		339.0 time, 340.4 real, 4457.0 MB
[runlim] sample:		349.0 time, 350.4 real, 4562.4 MB
[runlim] sample:		359.0 time, 360.4 real, 4671.6 MB
[runlim] sample:		369.0 time, 370.4 real, 4776.0 MB
[runlim] sample:		378.9 time, 380.4 real, 4882.2 MB
[runlim] sample:		388.9 time, 390.4 real, 4960.4 MB
[runlim] sample:		398.9 time, 400.4 real, 5020.6 MB
[runlim] sample:		408.9 time, 410.4 real, 5122.8 MB
[runlim] sample:		418.9 time, 420.4 real, 5231.2 MB
[runlim] sample:		428.9 time, 430.4 real, 5336.3 MB
[runlim] sample:		438.9 time, 440.4 real, 5439.7 MB
[runlim] sample:		448.9 time, 450.4 real, 5532.9 MB
[runlim] sample:		458.8 time, 460.4 real, 5633.4 MB
[runlim] sample:		468.8 time, 470.4 real, 5658.6 MB
[runlim] sample:		478.8 time, 480.4 real, 5659.3 MB
[runlim] sample:		488.8 time, 490.4 real, 5724.0 MB
[runlim] sample:		498.8 time, 500.4 real, 5733.5 MB
[runlim] sample:		508.8 time, 510.4 real, 5791.5 MB
[runlim] sample:		518.7 time, 520.4 real, 5869.2 MB
[runlim] sample:		528.7 time, 530.4 real, 5933.4 MB
[runlim] sample:		538.7 time, 540.4 real, 6006.3 MB
[runlim] sample:		548.7 time, 550.4 real, 6102.2 MB
[runlim] sample:		558.7 time, 560.4 real, 6197.8 MB
[runlim] sample:		568.7 time, 570.4 real, 6294.0 MB
[runlim] sample:		578.6 time, 580.4 real, 6400.4 MB
[runlim] sample:		588.6 time, 590.4 real, 6502.2 MB
[runlim] sample:		598.6 time, 600.4 real, 6609.7 MB
Fatal error: out of memory.
[runlim] sample:		5.6 time, 610.4 real, 216.0 MB
[runlim] sample:		15.6 time, 620.4 real, 441.2 MB
[runlim] sample:		25.5 time, 630.4 real, 677.8 MB
[runlim] sample:		35.5 time, 640.4 real, 840.3 MB
[runlim] sample:		45.5 time, 650.4 real, 1028.8 MB
[runlim] sample:		55.5 time, 660.4 real, 1244.5 MB
[runlim] sample:		65.5 time, 670.4 real, 1449.7 MB
[runlim] sample:		75.5 time, 680.4 real, 1565.0 MB
[runlim] sample:		85.5 time, 690.4 real, 1678.1 MB
[runlim] sample:		95.4 time, 700.4 real, 1868.6 MB
[runlim] sample:		105.4 time, 710.4 real, 2059.8 MB
[runlim] sample:		115.4 time, 720.4 real, 2243.1 MB
[runlim] sample:		125.4 time, 730.4 real, 2429.5 MB
[runlim] sample:		135.4 time, 740.4 real, 2609.7 MB
[runlim] sample:		145.4 time, 750.4 real, 2797.3 MB
[runlim] sample:		155.4 time, 760.4 real, 2986.1 MB
[runlim] sample:		165.3 time, 770.4 real, 3079.3 MB
[runlim] sample:		175.3 time, 780.4 real, 3080.5 MB
[runlim] sample:		185.3 time, 790.4 real, 3166.5 MB
[runlim] sample:		195.3 time, 800.4 real, 3315.1 MB
[runlim] sample:		205.3 time, 810.4 real, 3493.7 MB
[runlim] sample:		215.3 time, 820.4 real, 3670.3 MB
[runlim] sample:		225.2 time, 830.4 real, 3839.1 MB
[runlim] sample:		235.2 time, 840.4 real, 4013.7 MB
[runlim] sample:		245.2 time, 850.4 real, 4204.2 MB
[runlim] sample:		255.2 time, 860.4 real, 4382.6 MB
[runlim] sample:		265.2 time, 870.4 real, 4551.2 MB
[runlim] sample:		275.2 time, 880.4 real, 4747.1 MB
[runlim] sample:		285.2 time, 890.4 real, 4931.7 MB
[runlim] sample:		295.2 time, 900.4 real, 5106.3 MB
[runlim] sample:		305.1 time, 910.4 real, 5270.9 MB
[runlim] sample:		315.1 time, 920.4 real, 5439.4 MB
[runlim] sample:		325.1 time, 930.4 real, 5624.2 MB
[runlim] sample:		335.1 time, 940.4 real, 5791.3 MB
[runlim] sample:		345.1 time, 950.4 real, 5939.9 MB
[runlim] sample:		355.1 time, 960.4 real, 6090.1 MB
[runlim] sample:		365.0 time, 970.4 real, 6093.2 MB
[runlim] sample:		375.0 time, 980.4 real, 6093.7 MB
[runlim] sample:		385.0 time, 990.4 real, 6094.5 MB
[runlim] sample:		395.0 time, 1000.4 real, 6095.0 MB
[runlim] sample:		405.0 time, 1010.4 real, 6163.5 MB
[runlim] sample:		415.0 time, 1020.4 real, 6297.0 MB
[runlim] sample:		424.9 time, 1030.4 real, 6459.1 MB
[runlim] sample:		434.9 time, 1040.4 real, 6612.0 MB
Fatal error: out of memory.
[runlim] sample:		5.1 time, 1050.4 real, 186.0 MB
[runlim] sample:		15.1 time, 1060.4 real, 324.5 MB
[runlim] sample:		25.1 time, 1070.4 real, 443.5 MB
[runlim] sample:		35.1 time, 1080.4 real, 543.1 MB
[runlim] sample:		45.0 time, 1090.4 real, 600.6 MB
[runlim] sample:		55.0 time, 1100.4 real, 711.2 MB
[runlim] sample:		65.0 time, 1110.4 real, 778.4 MB
[runlim] sample:		75.0 time, 1120.4 real, 851.1 MB
[runlim] sample:		85.0 time, 1130.4 real, 910.2 MB
[runlim] sample:		95.0 time, 1140.4 real, 974.9 MB
[runlim] sample:		105.0 time, 1150.4 real, 979.0 MB
[runlim] sample:		114.9 time, 1160.4 real, 1112.1 MB
[runlim] sample:		124.9 time, 1170.4 real, 1114.9 MB
[runlim] sample:		134.9 time, 1180.4 real, 1181.9 MB
[runlim] sample:		144.9 time, 1190.4 real, 1184.8 MB
[runlim] sample:		154.9 time, 1200.4 real, 1316.5 MB
[runlim] sample:		164.9 time, 1210.4 real, 1316.7 MB
[runlim] sample:		174.8 time, 1220.4 real, 1426.6 MB
[runlim] sample:		184.8 time, 1230.4 real, 1445.6 MB
[runlim] sample:		194.8 time, 1240.4 real, 1448.1 MB
[runlim] sample:		204.8 time, 1250.4 real, 1576.4 MB
[runlim] sample:		214.8 time, 1260.4 real, 1576.7 MB
[runlim] sample:		224.8 time, 1270.4 real, 1641.9 MB
[runlim] sample:		234.8 time, 1280.4 real, 1645.4 MB
[runlim] sample:		244.7 time, 1290.4 real, 1646.4 MB
[runlim] sample:		254.7 time, 1300.4 real, 1775.3 MB
[runlim] sample:		264.7 time, 1310.4 real, 1778.4 MB
[runlim] sample:		274.7 time, 1320.4 real, 1779.7 MB
[runlim] sample:		284.7 time, 1330.4 real, 1845.6 MB
[runlim] sample:		294.7 time, 1340.4 real, 1847.4 MB
[runlim] sample:		304.6 time, 1350.4 real, 1849.9 MB
[runlim] sample:		314.6 time, 1360.4 real, 1978.5 MB
[runlim] sample:		324.6 time, 1370.4 real, 1979.2 MB
[runlim] sample:		334.6 time, 1380.4 real, 1979.8 MB
[runlim] sample:		344.6 time, 1390.4 real, 2108.1 MB
[runlim] sample:		354.6 time, 1400.4 real, 2110.7 MB
[runlim] sample:		364.6 time, 1410.4 real, 2113.2 MB
[runlim] sample:		374.5 time, 1420.4 real, 2249.4 MB
[runlim] sample:		384.5 time, 1430.4 real, 2250.0 MB
[runlim] sample:		394.5 time, 1440.4 real, 2250.2 MB
[runlim] sample:		404.5 time, 1450.4 real, 2251.4 MB
[runlim] sample:		414.5 time, 1460.4 real, 2318.9 MB
[runlim] sample:		424.5 time, 1470.4 real, 2319.2 MB
[runlim] sample:		434.4 time, 1480.4 real, 2319.4 MB
[runlim] sample:		444.4 time, 1490.4 real, 2447.8 MB
[runlim] sample:		454.4 time, 1500.4 real, 2448.3 MB
[runlim] sample:		464.4 time, 1510.4 real, 2448.5 MB
[runlim] sample:		474.4 time, 1520.4 real, 2452.6 MB
[runlim] sample:		484.4 time, 1530.4 real, 2518.3 MB
[runlim] sample:		494.3 time, 1540.4 real, 2518.5 MB
[runlim] sample:		504.3 time, 1550.4 real, 2522.6 MB
[runlim] sample:		514.3 time, 1560.4 real, 2619.1 MB
[runlim] sample:		524.3 time, 1570.4 real, 2651.5 MB
[runlim] sample:		534.3 time, 1580.4 real, 2651.8 MB
[runlim] sample:		544.3 time, 1590.4 real, 2654.0 MB
[runlim] sample:		554.3 time, 1600.4 real, 2774.5 MB
[runlim] sample:		564.2 time, 1610.4 real, 2784.6 MB
[runlim] sample:		574.2 time, 1620.4 real, 2790.0 MB
[runlim] sample:		584.2 time, 1630.4 real, 2791.1 MB
[runlim] sample:		594.2 time, 1640.4 real, 2899.8 MB
[runlim] sample:		604.2 time, 1650.4 real, 2919.5 MB
[runlim] sample:		614.2 time, 1660.4 real, 2920.0 MB
[runlim] sample:		624.1 time, 1670.4 real, 2920.3 MB
[runlim] sample:		634.1 time, 1680.4 real, 2959.3 MB
[runlim] sample:		644.1 time, 1690.4 real, 2987.5 MB
[runlim] sample:		654.1 time, 1700.4 real, 2987.8 MB
[runlim] sample:		664.1 time, 1710.4 real, 2988.3 MB
[runlim] sample:		674.1 time, 1720.4 real, 2988.8 MB
[runlim] sample:		684.1 time, 1730.4 real, 3119.0 MB
[runlim] sample:		694.0 time, 1740.4 real, 3121.5 MB
[runlim] sample:		704.0 time, 1750.4 real, 3123.7 MB
[runlim] sample:		714.0 time, 1760.4 real, 3123.7 MB
[runlim] sample:		724.0 time, 1770.4 real, 3187.9 MB
[runlim] sample:		734.0 time, 1780.4 real, 3187.9 MB
[runlim] sample:		744.0 time, 1790.4 real, 3188.5 MB
[runlim] sample:		753.9 time, 1800.4 real, 3188.5 MB
[runlim] sample:		763.9 time, 1810.4 real, 3245.0 MB
[runlim] sample:		773.9 time, 1820.4 real, 3318.6 MB
[runlim] sample:		783.9 time, 1830.4 real, 3318.6 MB
[runlim] sample:		793.9 time, 1840.4 real, 3318.8 MB
[runlim] sample:		803.9 time, 1850.4 real, 3318.8 MB
[runlim] sample:		813.9 time, 1860.4 real, 3447.0 MB
[runlim] sample:		823.8 time, 1870.4 real, 3447.0 MB
[runlim] sample:		833.8 time, 1880.4 real, 3447.0 MB
[runlim] sample:		843.8 time, 1890.4 real, 3447.2 MB
[runlim] sample:		853.8 time, 1900.4 real, 3449.2 MB
[runlim] sample:		863.8 time, 1910.4 real, 3513.4 MB
[runlim] sample:		873.8 time, 1920.4 real, 3513.4 MB
[runlim] sample:		883.8 time, 1930.4 real, 3513.7 MB
[runlim] sample:		893.7 time, 1940.4 real, 3515.7 MB
[runlim] sample:		903.7 time, 1950.4 real, 3516.0 MB
[runlim] sample:		913.7 time, 1960.4 real, 3643.8 MB
[runlim] sample:		923.7 time, 1970.4 real, 3644.1 MB
[runlim] sample:		933.7 time, 1980.4 real, 3646.1 MB
[runlim] sample:		943.7 time, 1990.4 real, 3646.4 MB
[runlim] sample:		953.6 time, 2000.4 real, 3646.4 MB
[runlim] sample:		963.6 time, 2010.4 real, 3774.5 MB
[runlim] sample:		973.6 time, 2020.4 real, 3774.5 MB
[runlim] sample:		983.6 time, 2030.4 real, 3774.8 MB
[runlim] sample:		993.6 time, 2040.4 real, 3774.8 MB
[runlim] sample:		1003.6 time, 2050.4 real, 3775.0 MB
[runlim] sample:		1013.6 time, 2060.4 real, 3905.2 MB
[runlim] sample:		1023.5 time, 2070.4 real, 3907.7 MB
[runlim] sample:		1033.5 time, 2080.4 real, 3910.0 MB
[runlim] sample:		1043.5 time, 2090.4 real, 3910.2 MB
[runlim] sample:		1053.5 time, 2100.4 real, 3910.2 MB
[runlim] sample:		1063.5 time, 2110.4 real, 3974.5 MB
[runlim] sample:		1073.5 time, 2120.4 real, 3974.5 MB
[runlim] sample:		1083.4 time, 2130.4 real, 3974.7 MB
[runlim] sample:		1093.4 time, 2140.4 real, 3974.7 MB
[runlim] sample:		1103.4 time, 2150.4 real, 3983.1 MB
[runlim] sample:		1113.4 time, 2160.4 real, 4113.2 MB
[runlim] sample:		1123.4 time, 2170.4 real, 4113.5 MB
[runlim] sample:		1133.4 time, 2180.4 real, 4113.5 MB
[runlim] sample:		1143.4 time, 2190.4 real, 4113.7 MB
[runlim] sample:		1153.4 time, 2200.4 real, 4113.9 MB
[runlim] sample:		1163.3 time, 2210.4 real, 4113.9 MB
[runlim] sample:		1173.3 time, 2220.4 real, 4178.1 MB
[runlim] sample:		1183.3 time, 2230.4 real, 4178.1 MB
[runlim] sample:		1193.3 time, 2240.4 real, 4178.3 MB
[runlim] sample:		1203.3 time, 2250.4 real, 4180.9 MB
[runlim] sample:		1213.3 time, 2260.4 real, 4182.9 MB
[runlim] sample:		1223.2 time, 2270.4 real, 4327.1 MB
[runlim] sample:		1233.2 time, 2280.4 real, 4327.1 MB
[runlim] sample:		1243.2 time, 2290.4 real, 4331.6 MB
[runlim] sample:		1253.2 time, 2300.4 real, 4331.8 MB
[runlim] sample:		1263.2 time, 2310.4 real, 4331.8 MB
[runlim] sample:		1273.2 time, 2320.4 real, 4333.6 MB
[runlim] sample:		1283.2 time, 2330.4 real, 4397.8 MB
[runlim] sample:		1293.1 time, 2340.4 real, 4400.3 MB
[runlim] sample:		1303.1 time, 2350.4 real, 4400.3 MB
[runlim] sample:		1313.1 time, 2360.4 real, 4402.6 MB
[runlim] sample:		1323.1 time, 2370.4 real, 4402.6 MB
[runlim] sample:		1333.1 time, 2380.4 real, 4455.3 MB
[runlim] sample:		1343.1 time, 2390.4 real, 4531.1 MB
[runlim] sample:		1353.0 time, 2400.4 real, 4531.2 MB
[runlim] sample:		1363.0 time, 2410.4 real, 4531.4 MB
[runlim] sample:		1373.0 time, 2420.4 real, 4531.7 MB
[runlim] sample:		1383.0 time, 2430.4 real, 4531.9 MB
[runlim] sample:		1393.0 time, 2440.4 real, 4612.3 MB
[runlim] sample:		1403.0 time, 2450.4 real, 4662.2 MB
[runlim] sample:		1413.0 time, 2460.4 real, 4662.7 MB
[runlim] sample:		1422.9 time, 2470.4 real, 4663.2 MB
[runlim] sample:		1432.9 time, 2480.4 real, 4663.2 MB
[runlim] sample:		1442.9 time, 2490.4 real, 4665.5 MB
[runlim] sample:		1452.9 time, 2500.4 real, 4729.9 MB
[runlim] sample:		1462.9 time, 2510.4 real, 4730.1 MB
[runlim] sample:		1472.9 time, 2520.4 real, 4730.4 MB
[runlim] sample:		1482.9 time, 2530.4 real, 4730.9 MB
[runlim] sample:		1492.8 time, 2540.4 real, 4731.1 MB
[runlim] sample:		1502.8 time, 2550.4 real, 4731.6 MB
[runlim] sample:		1512.8 time, 2560.4 real, 4791.8 MB
[runlim] sample:		1522.8 time, 2570.4 real, 4859.9 MB
[runlim] sample:		1532.8 time, 2580.4 real, 4860.3 MB
[runlim] sample:		1542.8 time, 2590.4 real, 4862.5 MB
[runlim] sample:		1552.8 time, 2600.4 real, 4862.5 MB
[runlim] sample:		1562.7 time, 2610.4 real, 4862.8 MB
[runlim] sample:		1572.7 time, 2620.4 real, 4862.8 MB
[runlim] sample:		1582.7 time, 2630.4 real, 4990.9 MB
[runlim] sample:		1592.7 time, 2640.4 real, 4990.9 MB
[runlim] sample:		1602.7 time, 2650.4 real, 4991.2 MB
[runlim] sample:		1612.7 time, 2660.4 real, 4991.2 MB
[runlim] sample:		1622.7 time, 2670.4 real, 4991.4 MB
[runlim] sample:		1632.6 time, 2680.4 real, 4991.6 MB
[runlim] sample:		1642.6 time, 2690.4 real, 5055.5 MB
[runlim] sample:		1652.6 time, 2700.4 real, 5057.5 MB
[runlim] sample:		1662.6 time, 2710.4 real, 5057.8 MB
[runlim] sample:		1672.6 time, 2720.4 real, 5060.0 MB
[runlim] sample:		1682.6 time, 2730.4 real, 5060.0 MB
[runlim] sample:		1692.5 time, 2740.4 real, 5062.0 MB
[runlim] sample:		1702.5 time, 2750.4 real, 5190.2 MB
[runlim] sample:		1712.5 time, 2760.4 real, 5190.2 MB
[runlim] sample:		1722.5 time, 2770.4 real, 5190.2 MB
[runlim] sample:		1732.5 time, 2780.4 real, 5190.4 MB
[runlim] sample:		1742.5 time, 2790.4 real, 5190.4 MB
[runlim] sample:		1752.5 time, 2800.4 real, 5190.4 MB
[runlim] sample:		1762.4 time, 2810.4 real, 5224.5 MB
[runlim] sample:		1772.4 time, 2820.4 real, 5320.8 MB
[runlim] sample:		1782.4 time, 2830.4 real, 5321.1 MB
[runlim] sample:		1792.4 time, 2840.4 real, 5321.1 MB
[runlim] sample:		1802.4 time, 2850.4 real, 5321.3 MB
[runlim] sample:		1812.4 time, 2860.4 real, 5321.3 MB
[runlim] sample:		1822.4 time, 2870.4 real, 5321.6 MB
[runlim] sample:		1832.3 time, 2880.4 real, 5385.5 MB
[runlim] sample:		1842.3 time, 2890.4 real, 5385.8 MB
[runlim] sample:		1852.3 time, 2900.4 real, 5385.8 MB
[runlim] sample:		1862.3 time, 2910.4 real, 5386.0 MB
[runlim] sample:		1872.3 time, 2920.4 real, 5386.0 MB
[runlim] sample:		1882.3 time, 2930.4 real, 5388.0 MB
[runlim] sample:		1892.3 time, 2940.4 real, 5388.3 MB
[runlim] sample:		1902.2 time, 2950.4 real, 5516.2 MB
[runlim] sample:		1912.2 time, 2960.4 real, 5516.2 MB
[runlim] sample:		1922.2 time, 2970.4 real, 5516.4 MB
[runlim] sample:		1932.2 time, 2980.4 real, 5516.4 MB
[runlim] sample:		1942.2 time, 2990.4 real, 5516.4 MB
[runlim] sample:		1952.2 time, 3000.4 real, 5516.4 MB
[runlim] sample:		1962.2 time, 3010.4 real, 5566.5 MB
[runlim] sample:		1972.1 time, 3020.4 real, 5580.6 MB
[runlim] sample:		1982.1 time, 3030.4 real, 5582.9 MB
[runlim] sample:		1992.1 time, 3040.4 real, 5582.9 MB
[runlim] sample:		2002.1 time, 3050.4 real, 5584.9 MB
[runlim] sample:		2012.1 time, 3060.4 real, 5584.9 MB
[runlim] sample:		2022.1 time, 3070.4 real, 5584.9 MB
[runlim] sample:		2032.0 time, 3080.4 real, 5713.0 MB
[runlim] sample:		2042.0 time, 3090.4 real, 5713.0 MB
[runlim] sample:		2052.0 time, 3100.4 real, 5713.0 MB
[runlim] sample:		2062.0 time, 3110.4 real, 5713.3 MB
[runlim] sample:		2072.0 time, 3120.4 real, 5713.3 MB
[runlim] sample:		2082.0 time, 3130.4 real, 5713.3 MB
[runlim] sample:		2092.0 time, 3140.4 real, 5713.5 MB
[runlim] sample:		2102.0 time, 3150.4 real, 5777.5 MB
[runlim] sample:		2112.0 time, 3160.4 real, 5779.5 MB
[runlim] sample:		2121.9 time, 3170.4 real, 5779.5 MB
[runlim] sample:		2131.9 time, 3180.4 real, 5783.3 MB
[runlim] sample:		2141.9 time, 3190.4 real, 5788.0 MB
[runlim] sample:		2151.9 time, 3200.4 real, 5788.0 MB
[runlim] sample:		2161.9 time, 3210.4 real, 5788.0 MB
[runlim] sample:		2171.9 time, 3220.4 real, 5904.0 MB
[runlim] sample:		2181.9 time, 3230.4 real, 5918.2 MB
[runlim] sample:		2191.8 time, 3240.4 real, 5918.2 MB
[runlim] sample:		2201.8 time, 3250.4 real, 5918.4 MB
[runlim] sample:		2211.8 time, 3260.4 real, 5918.4 MB
[runlim] sample:		2221.8 time, 3270.4 real, 5918.4 MB
[runlim] sample:		2231.8 time, 3280.4 real, 5918.4 MB
[runlim] sample:		2241.8 time, 3290.4 real, 5946.2 MB
[runlim] sample:		2251.8 time, 3300.4 real, 5982.7 MB
[runlim] sample:		2261.7 time, 3310.4 real, 5983.0 MB
[runlim] sample:		2271.7 time, 3320.4 real, 5983.2 MB
[runlim] sample:		2281.7 time, 3330.4 real, 5983.4 MB
[runlim] sample:		2291.7 time, 3340.4 real, 5983.4 MB
[runlim] sample:		2301.7 time, 3350.4 real, 5984.0 MB
[runlim] sample:		2311.7 time, 3360.4 real, 5984.2 MB
[runlim] sample:		2321.7 time, 3370.4 real, 6176.2 MB
[runlim] sample:		2331.6 time, 3380.4 real, 6176.7 MB
[runlim] sample:		2341.6 time, 3390.4 real, 6177.2 MB
[runlim] sample:		2351.6 time, 3400.4 real, 6177.2 MB
[runlim] sample:		2361.6 time, 3410.4 real, 6177.7 MB
[runlim] sample:		2371.6 time, 3420.4 real, 6177.7 MB
[runlim] sample:		2381.6 time, 3430.4 real, 6178.0 MB
[runlim] sample:		2391.6 time, 3440.4 real, 6246.4 MB
[runlim] sample:		2401.5 time, 3450.4 real, 6246.4 MB
[runlim] sample:		2411.5 time, 3460.4 real, 6246.6 MB
[runlim] sample:		2421.5 time, 3470.4 real, 6247.1 MB
[runlim] sample:		2431.5 time, 3480.4 real, 6247.1 MB
[runlim] sample:		2441.5 time, 3490.4 real, 6247.6 MB
[runlim] sample:		2451.5 time, 3500.4 real, 6247.6 MB
[runlim] sample:		2461.5 time, 3510.4 real, 6248.1 MB
[runlim] sample:		2471.4 time, 3520.4 real, 6376.5 MB
[runlim] sample:		2481.4 time, 3530.4 real, 6376.5 MB
[runlim] sample:		2491.4 time, 3540.4 real, 6377.0 MB
[runlim] sample:		2501.4 time, 3550.4 real, 6377.0 MB
[runlim] sample:		2511.4 time, 3560.4 real, 6377.3 MB
[runlim] sample:		2521.4 time, 3570.4 real, 6377.8 MB
[runlim] sample:		2531.3 time, 3580.4 real, 6377.8 MB
[runlim] sample:		2541.3 time, 3590.4 real, 6427.8 MB
[runlim] end:			Mon Sep 28 21:00:06 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		179969
[runlim] real:			3600.12 seconds
[runlim] time:			2551.03 seconds
[runlim] space:			6674.6 MB
[runlim] samples:		35997
