[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/v3s/single.v3s
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/hwmcc14/single/6s23.aig
[runlim] start:			Tue Sep 15 21:00:46 2015
[runlim] main pid:		928
[runlim] sample:		29.1 time, 10.5 real, 193.3 MB
[runlim] sample:		59.0 time, 20.5 real, 210.1 MB
[runlim] sample:		89.0 time, 30.5 real, 218.3 MB
[runlim] sample:		119.0 time, 40.5 real, 225.1 MB
[runlim] sample:		148.9 time, 50.5 real, 238.5 MB
[runlim] sample:		178.9 time, 60.5 real, 248.4 MB
[runlim] sample:		208.9 time, 70.5 real, 257.0 MB
[runlim] sample:		238.8 time, 80.5 real, 264.5 MB
[runlim] sample:		268.8 time, 90.5 real, 268.9 MB
[runlim] sample:		298.8 time, 100.5 real, 271.7 MB
[runlim] sample:		328.7 time, 110.5 real, 281.0 MB
[runlim] sample:		358.7 time, 120.5 real, 282.0 MB
[runlim] sample:		388.6 time, 130.5 real, 289.3 MB
[runlim] sample:		418.6 time, 140.5 real, 299.1 MB
[runlim] sample:		448.0 time, 150.5 real, 297.4 MB
[runlim] sample:		477.9 time, 160.5 real, 307.3 MB
[runlim] sample:		507.9 time, 170.5 real, 314.6 MB
[runlim] sample:		537.8 time, 180.5 real, 327.1 MB
[runlim] sample:		567.8 time, 190.5 real, 329.1 MB
[runlim] sample:		597.7 time, 200.5 real, 333.1 MB
[runlim] sample:		627.7 time, 210.5 real, 344.2 MB
[runlim] sample:		657.6 time, 220.5 real, 358.9 MB
[runlim] sample:		687.6 time, 230.5 real, 365.5 MB
[runlim] sample:		717.5 time, 240.5 real, 371.0 MB
[runlim] sample:		747.5 time, 250.5 real, 372.9 MB
[runlim] sample:		777.4 time, 260.5 real, 378.9 MB
[runlim] sample:		807.4 time, 270.5 real, 380.9 MB
[runlim] sample:		837.4 time, 280.5 real, 383.4 MB
[runlim] sample:		867.3 time, 290.5 real, 384.7 MB
[runlim] sample:		897.3 time, 300.5 real, 385.5 MB
[runlim] sample:		927.2 time, 310.5 real, 386.6 MB
[runlim] sample:		957.2 time, 320.5 real, 387.4 MB
[runlim] sample:		987.1 time, 330.5 real, 445.5 MB
[runlim] sample:		1017.1 time, 340.5 real, 379.7 MB
[runlim] sample:		1047.1 time, 350.5 real, 381.6 MB
[runlim] sample:		1077.0 time, 360.5 real, 390.3 MB
[runlim] sample:		1107.0 time, 370.5 real, 391.1 MB
[runlim] sample:		1136.9 time, 380.5 real, 392.1 MB
[runlim] sample:		1166.9 time, 390.5 real, 395.0 MB
[runlim] sample:		1196.8 time, 400.5 real, 397.0 MB
[runlim] sample:		1226.8 time, 410.5 real, 400.3 MB
[runlim] sample:		1256.8 time, 420.5 real, 400.6 MB
[runlim] sample:		1286.7 time, 430.5 real, 407.6 MB
[runlim] sample:		1316.7 time, 440.5 real, 408.6 MB
[runlim] sample:		1346.7 time, 450.5 real, 409.4 MB
[runlim] sample:		1376.6 time, 460.5 real, 410.1 MB
[runlim] sample:		1406.6 time, 470.5 real, 410.7 MB
[runlim] sample:		1436.6 time, 480.5 real, 411.0 MB
[runlim] sample:		1466.5 time, 490.5 real, 415.9 MB
[runlim] sample:		1496.5 time, 500.5 real, 419.9 MB
[runlim] sample:		1526.5 time, 510.5 real, 445.6 MB
[runlim] sample:		1556.4 time, 520.5 real, 448.7 MB
[runlim] sample:		1586.4 time, 530.5 real, 457.8 MB
[runlim] sample:		1616.4 time, 540.5 real, 462.3 MB
[runlim] sample:		1646.3 time, 550.5 real, 465.1 MB
[runlim] sample:		1676.3 time, 560.5 real, 470.4 MB
[runlim] sample:		1706.3 time, 570.5 real, 472.1 MB
[runlim] sample:		1736.2 time, 580.5 real, 473.6 MB
[runlim] sample:		1766.2 time, 590.5 real, 467.6 MB
[runlim] sample:		1796.2 time, 600.5 real, 468.4 MB
[runlim] sample:		1826.2 time, 610.5 real, 468.9 MB
[runlim] sample:		1856.1 time, 620.5 real, 469.5 MB
[runlim] sample:		1886.1 time, 630.5 real, 422.0 MB
[runlim] sample:		1916.0 time, 640.5 real, 440.9 MB
[runlim] sample:		1946.0 time, 650.5 real, 436.4 MB
[runlim] sample:		1976.0 time, 660.5 real, 437.3 MB
[runlim] sample:		2005.9 time, 670.5 real, 438.7 MB
[runlim] sample:		2035.9 time, 680.5 real, 438.7 MB
[runlim] sample:		2065.8 time, 690.5 real, 442.9 MB
[runlim] sample:		2095.8 time, 700.5 real, 443.6 MB
[runlim] sample:		2125.7 time, 710.5 real, 445.6 MB
[runlim] sample:		2155.7 time, 720.5 real, 451.0 MB
[runlim] sample:		2185.7 time, 730.5 real, 452.8 MB
[runlim] sample:		2215.6 time, 740.5 real, 456.1 MB
[runlim] sample:		2245.6 time, 750.5 real, 459.1 MB
[runlim] sample:		2275.5 time, 760.5 real, 456.6 MB
[runlim] sample:		2305.5 time, 770.5 real, 460.4 MB
[runlim] sample:		2335.4 time, 780.5 real, 454.0 MB
[runlim] sample:		2365.4 time, 790.5 real, 455.6 MB
[runlim] sample:		2395.3 time, 800.5 real, 460.8 MB
[runlim] sample:		2425.3 time, 810.5 real, 462.7 MB
[runlim] sample:		2455.2 time, 820.5 real, 465.3 MB
[runlim] sample:		2485.2 time, 830.5 real, 471.7 MB
[runlim] sample:		2515.2 time, 840.5 real, 472.9 MB
[runlim] sample:		2545.1 time, 850.5 real, 474.6 MB
[runlim] sample:		2575.1 time, 860.5 real, 477.5 MB
[runlim] sample:		2605.0 time, 870.5 real, 468.6 MB
[runlim] sample:		2635.0 time, 880.5 real, 473.2 MB
[runlim] sample:		2664.9 time, 890.5 real, 485.8 MB
[runlim] sample:		2694.9 time, 900.5 real, 488.7 MB
[runlim] sample:		2724.9 time, 910.5 real, 492.4 MB
[runlim] sample:		2754.9 time, 920.5 real, 492.5 MB
[runlim] sample:		2784.8 time, 930.5 real, 497.5 MB
[runlim] sample:		2814.8 time, 940.5 real, 500.4 MB
[runlim] sample:		2844.8 time, 950.5 real, 500.8 MB
[runlim] sample:		2874.7 time, 960.5 real, 518.8 MB
[runlim] sample:		2904.7 time, 970.5 real, 519.9 MB
[runlim] sample:		2934.7 time, 980.5 real, 522.0 MB
[runlim] sample:		2964.6 time, 990.5 real, 521.6 MB
[runlim] sample:		2994.6 time, 1000.5 real, 521.5 MB
[runlim] sample:		3024.6 time, 1010.5 real, 542.1 MB
[runlim] sample:		3054.5 time, 1020.5 real, 546.0 MB
[runlim] sample:		3084.5 time, 1030.5 real, 547.2 MB
[runlim] sample:		3114.4 time, 1040.5 real, 548.2 MB
[runlim] sample:		3144.4 time, 1050.5 real, 548.9 MB
[runlim] sample:		3174.4 time, 1060.5 real, 550.8 MB
[runlim] sample:		3204.4 time, 1070.5 real, 551.9 MB
[runlim] sample:		3234.3 time, 1080.5 real, 653.9 MB
[runlim] sample:		3264.1 time, 1090.5 real, 528.1 MB
[runlim] sample:		3294.1 time, 1100.5 real, 582.1 MB
[runlim] sample:		3324.1 time, 1110.5 real, 642.0 MB
[runlim] sample:		3354.0 time, 1120.5 real, 662.7 MB
[runlim] sample:		3384.0 time, 1130.5 real, 698.2 MB
[runlim] sample:		3414.0 time, 1140.5 real, 728.4 MB
[runlim] sample:		3443.9 time, 1150.5 real, 743.5 MB
[runlim] sample:		3473.9 time, 1160.5 real, 787.1 MB
[runlim] sample:		3503.8 time, 1170.5 real, 862.3 MB
[runlim] sample:		3533.8 time, 1180.5 real, 864.7 MB
[runlim] sample:		3563.8 time, 1190.5 real, 867.6 MB
[runlim] sample:		3593.7 time, 1200.5 real, 872.5 MB
[runlim] sample:		3623.7 time, 1210.5 real, 877.6 MB
[runlim] sample:		3653.7 time, 1220.5 real, 888.9 MB
[runlim] sample:		3683.6 time, 1230.5 real, 899.3 MB
[runlim] sample:		3713.6 time, 1240.5 real, 906.1 MB
[runlim] sample:		3743.6 time, 1250.5 real, 912.6 MB
[runlim] sample:		3773.5 time, 1260.5 real, 915.6 MB
[runlim] sample:		3803.5 time, 1270.5 real, 926.8 MB
[runlim] sample:		3833.5 time, 1280.5 real, 935.1 MB
[runlim] sample:		3863.4 time, 1290.5 real, 939.0 MB
[runlim] sample:		3893.4 time, 1300.5 real, 946.1 MB
[runlim] sample:		3923.3 time, 1310.5 real, 951.3 MB
[runlim] sample:		3953.3 time, 1320.5 real, 958.6 MB
[runlim] sample:		3983.3 time, 1330.5 real, 966.1 MB
[runlim] sample:		4013.3 time, 1340.5 real, 972.9 MB
[runlim] sample:		4043.2 time, 1350.5 real, 979.4 MB
[runlim] sample:		4073.2 time, 1360.5 real, 983.7 MB
[runlim] sample:		4103.1 time, 1370.5 real, 988.1 MB
[runlim] sample:		4133.1 time, 1380.5 real, 1001.0 MB
[runlim] sample:		4163.1 time, 1390.5 real, 1014.1 MB
[runlim] sample:		4193.1 time, 1400.5 real, 1025.4 MB
[runlim] sample:		4223.0 time, 1410.5 real, 1030.3 MB
[runlim] sample:		4253.0 time, 1420.5 real, 1035.0 MB
[runlim] sample:		4283.0 time, 1430.5 real, 1042.9 MB
[runlim] sample:		4312.9 time, 1440.5 real, 1046.4 MB
[runlim] sample:		4342.9 time, 1450.5 real, 1052.8 MB
[runlim] sample:		4372.8 time, 1460.5 real, 1062.4 MB
[runlim] sample:		4402.8 time, 1470.5 real, 1066.8 MB
[runlim] sample:		4432.7 time, 1480.5 real, 1069.1 MB
[runlim] sample:		4462.6 time, 1490.5 real, 1074.1 MB
[runlim] sample:		4492.6 time, 1500.5 real, 1078.9 MB
[runlim] sample:		4522.5 time, 1510.5 real, 1083.9 MB
[runlim] sample:		4552.5 time, 1520.5 real, 1088.6 MB
[runlim] sample:		4582.4 time, 1530.5 real, 1099.6 MB
[runlim] sample:		4612.4 time, 1540.5 real, 1106.2 MB
[runlim] sample:		4642.4 time, 1550.5 real, 1108.7 MB
[runlim] sample:		4672.3 time, 1560.5 real, 1113.4 MB
[runlim] sample:		4702.3 time, 1570.5 real, 1116.2 MB
[runlim] sample:		4732.2 time, 1580.5 real, 1123.6 MB
[runlim] sample:		4762.2 time, 1590.5 real, 1126.3 MB
[runlim] sample:		4792.2 time, 1600.5 real, 1133.0 MB
[runlim] sample:		4822.2 time, 1610.5 real, 1138.6 MB
[runlim] sample:		4852.1 time, 1620.5 real, 1141.5 MB
[runlim] sample:		4882.1 time, 1630.5 real, 1145.0 MB
[runlim] sample:		4912.1 time, 1640.5 real, 1150.6 MB
[runlim] sample:		4942.0 time, 1650.5 real, 1153.2 MB
[runlim] sample:		4972.0 time, 1660.5 real, 1157.9 MB
[runlim] sample:		5002.0 time, 1670.5 real, 1166.0 MB
[runlim] sample:		5031.9 time, 1680.5 real, 1174.9 MB
[runlim] sample:		5061.9 time, 1690.5 real, 1187.2 MB
[runlim] sample:		5091.8 time, 1700.5 real, 1200.4 MB
[runlim] sample:		5121.8 time, 1710.5 real, 1208.9 MB
[runlim] sample:		5151.8 time, 1720.5 real, 1217.4 MB
[runlim] sample:		5181.7 time, 1730.5 real, 1224.1 MB
[runlim] sample:		5211.7 time, 1740.5 real, 1235.3 MB
[runlim] sample:		5241.7 time, 1750.5 real, 1241.1 MB
[runlim] sample:		5271.6 time, 1760.5 real, 1246.3 MB
[runlim] sample:		5301.6 time, 1770.5 real, 1250.6 MB
[runlim] sample:		5331.6 time, 1780.5 real, 1254.1 MB
[runlim] sample:		5361.5 time, 1790.5 real, 1258.9 MB
[runlim] sample:		5391.5 time, 1800.5 real, 1261.6 MB
[runlim] sample:		5421.4 time, 1810.5 real, 1264.4 MB
[runlim] sample:		5451.4 time, 1820.5 real, 1267.2 MB
[runlim] sample:		5481.3 time, 1830.5 real, 1277.4 MB
[runlim] sample:		5511.2 time, 1840.5 real, 1279.2 MB
[runlim] sample:		5541.2 time, 1850.5 real, 1281.7 MB
[runlim] sample:		5571.1 time, 1860.5 real, 1284.2 MB
[runlim] sample:		5601.1 time, 1870.5 real, 1287.2 MB
[runlim] sample:		5631.0 time, 1880.5 real, 1292.0 MB
[runlim] sample:		5661.0 time, 1890.5 real, 1296.8 MB
[runlim] sample:		5690.9 time, 1900.5 real, 1301.5 MB
[runlim] sample:		5720.9 time, 1910.5 real, 1305.1 MB
[runlim] sample:		5750.9 time, 1920.5 real, 1310.1 MB
[runlim] sample:		5780.8 time, 1930.5 real, 1319.0 MB
[runlim] sample:		5810.8 time, 1940.5 real, 1323.3 MB
[runlim] sample:		5840.7 time, 1950.5 real, 1328.4 MB
[runlim] sample:		5870.7 time, 1960.5 real, 1332.4 MB
[runlim] sample:		5900.6 time, 1970.5 real, 1332.4 MB
[runlim] sample:		5930.6 time, 1980.5 real, 1337.7 MB
[runlim] sample:		5960.6 time, 1990.5 real, 1341.7 MB
[runlim] sample:		5990.5 time, 2000.5 real, 1344.0 MB
[runlim] sample:		6020.5 time, 2010.5 real, 1347.6 MB
[runlim] sample:		6050.4 time, 2020.5 real, 1349.9 MB
[runlim] sample:		6080.4 time, 2030.5 real, 1354.2 MB
[runlim] sample:		6110.4 time, 2040.5 real, 1359.2 MB
[runlim] sample:		6140.3 time, 2050.5 real, 1364.2 MB
[runlim] sample:		6170.3 time, 2060.5 real, 1367.3 MB
[runlim] sample:		6200.3 time, 2070.5 real, 1369.5 MB
[runlim] sample:		6230.2 time, 2080.5 real, 1374.1 MB
[runlim] sample:		6260.2 time, 2090.5 real, 1376.7 MB
[runlim] sample:		6290.1 time, 2100.5 real, 1379.0 MB
[runlim] sample:		6320.1 time, 2110.5 real, 1381.6 MB
[runlim] sample:		6350.1 time, 2120.5 real, 1387.6 MB
[runlim] sample:		6380.0 time, 2130.5 real, 1396.3 MB
[runlim] sample:		6410.0 time, 2140.5 real, 1407.4 MB
[runlim] sample:		6440.0 time, 2150.5 real, 1415.1 MB
[runlim] sample:		6469.9 time, 2160.5 real, 1422.3 MB
[runlim] sample:		6499.9 time, 2170.5 real, 1429.1 MB
[runlim] sample:		6529.9 time, 2180.5 real, 1431.7 MB
[runlim] sample:		6559.8 time, 2190.5 real, 1434.2 MB
[runlim] sample:		6589.8 time, 2200.5 real, 1436.8 MB
[runlim] sample:		6619.8 time, 2210.5 real, 1439.6 MB
[runlim] sample:		6649.7 time, 2220.5 real, 1446.1 MB
[runlim] sample:		6679.7 time, 2230.5 real, 1450.2 MB
[runlim] sample:		6709.6 time, 2240.5 real, 1459.7 MB
[runlim] sample:		6739.6 time, 2250.5 real, 1462.4 MB
[runlim] sample:		6769.5 time, 2260.5 real, 1468.2 MB
[runlim] sample:		6799.5 time, 2270.5 real, 1474.3 MB
[runlim] sample:		6829.4 time, 2280.5 real, 1477.4 MB
[runlim] sample:		6859.4 time, 2290.5 real, 1482.2 MB
[runlim] sample:		6889.3 time, 2300.5 real, 1484.6 MB
[runlim] sample:		6919.3 time, 2310.5 real, 1486.6 MB
[runlim] sample:		6949.3 time, 2320.5 real, 1489.6 MB
[runlim] sample:		6979.2 time, 2330.5 real, 1494.0 MB
[runlim] sample:		7009.2 time, 2340.5 real, 1494.2 MB
[runlim] sample:		7039.1 time, 2350.5 real, 1496.6 MB
[runlim] sample:		7069.1 time, 2360.5 real, 1498.8 MB
[runlim] sample:		7099.0 time, 2370.5 real, 1503.3 MB
[runlim] sample:		7129.0 time, 2380.5 real, 1507.7 MB
[runlim] sample:		7158.9 time, 2390.5 real, 1511.8 MB
[runlim] sample:		7188.9 time, 2400.5 real, 1516.9 MB
[runlim] sample:		7218.9 time, 2410.5 real, 1521.5 MB
[runlim] sample:		7248.8 time, 2420.5 real, 1527.9 MB
[runlim] sample:		7278.8 time, 2430.5 real, 1525.6 MB
[runlim] sample:		7308.8 time, 2440.5 real, 1529.8 MB
[runlim] sample:		7338.7 time, 2450.5 real, 1533.3 MB
[runlim] sample:		7368.6 time, 2460.5 real, 1536.9 MB
[runlim] sample:		7398.6 time, 2470.5 real, 1542.4 MB
[runlim] sample:		7428.6 time, 2480.5 real, 1544.4 MB
[runlim] sample:		7458.5 time, 2490.5 real, 1550.2 MB
[runlim] sample:		7488.5 time, 2500.5 real, 1552.2 MB
[runlim] sample:		7518.4 time, 2510.5 real, 1552.8 MB
[runlim] sample:		7548.4 time, 2520.5 real, 1554.5 MB
[runlim] sample:		7578.3 time, 2530.5 real, 1558.7 MB
[runlim] sample:		7608.3 time, 2540.5 real, 1567.0 MB
[runlim] sample:		7638.2 time, 2550.5 real, 1565.8 MB
[runlim] sample:		7668.2 time, 2560.5 real, 1566.0 MB
[runlim] sample:		7698.1 time, 2570.5 real, 1569.7 MB
[runlim] sample:		7728.1 time, 2580.5 real, 1574.0 MB
[runlim] sample:		7758.1 time, 2590.5 real, 1575.1 MB
[runlim] sample:		7788.0 time, 2600.5 real, 1579.3 MB
[runlim] sample:		7818.0 time, 2610.5 real, 1583.9 MB
[runlim] sample:		7847.9 time, 2620.5 real, 1585.4 MB
[runlim] sample:		7877.9 time, 2630.5 real, 1590.6 MB
[runlim] sample:		7907.8 time, 2640.5 real, 1594.5 MB
[runlim] sample:		7937.8 time, 2650.5 real, 1600.2 MB
[runlim] sample:		7967.7 time, 2660.5 real, 1611.4 MB
[runlim] sample:		7997.7 time, 2670.5 real, 1613.2 MB
[runlim] sample:		8027.7 time, 2680.5 real, 1618.6 MB
[runlim] sample:		8057.6 time, 2690.5 real, 1632.6 MB
[runlim] sample:		8087.6 time, 2700.5 real, 1645.4 MB
[runlim] sample:		8117.5 time, 2710.5 real, 1651.4 MB
[runlim] sample:		8147.5 time, 2720.5 real, 1655.7 MB
[runlim] sample:		8177.4 time, 2730.5 real, 1664.2 MB
[runlim] sample:		8207.4 time, 2740.5 real, 1664.4 MB
[runlim] sample:		8237.4 time, 2750.5 real, 1674.4 MB
[runlim] sample:		8267.3 time, 2760.5 real, 1677.0 MB
[runlim] sample:		8297.3 time, 2770.5 real, 1681.5 MB
[runlim] sample:		8327.2 time, 2780.5 real, 1685.6 MB
[runlim] sample:		8357.2 time, 2790.5 real, 1688.0 MB
[runlim] sample:		8387.1 time, 2800.5 real, 1695.9 MB
[runlim] sample:		8417.1 time, 2810.5 real, 1698.7 MB
[runlim] sample:		8447.0 time, 2820.5 real, 1708.6 MB
[runlim] sample:		8477.0 time, 2830.5 real, 1712.4 MB
[runlim] sample:		8507.0 time, 2840.5 real, 1719.2 MB
[runlim] sample:		8536.9 time, 2850.5 real, 1725.6 MB
[runlim] sample:		8566.9 time, 2860.5 real, 1733.2 MB
[runlim] sample:		8596.8 time, 2870.5 real, 1739.9 MB
[runlim] sample:		8626.8 time, 2880.5 real, 1746.4 MB
[runlim] sample:		8656.8 time, 2890.5 real, 1763.8 MB
[runlim] sample:		8686.7 time, 2900.5 real, 1773.8 MB
[runlim] sample:		8716.7 time, 2910.5 real, 1781.3 MB
[runlim] sample:		8746.6 time, 2920.5 real, 1785.3 MB
[runlim] sample:		8776.6 time, 2930.5 real, 1793.3 MB
[runlim] sample:		8806.6 time, 2940.5 real, 1800.8 MB
[runlim] sample:		8836.5 time, 2950.5 real, 1807.3 MB
[runlim] sample:		8866.5 time, 2960.5 real, 1812.6 MB
[runlim] sample:		8896.5 time, 2970.5 real, 1814.2 MB
[runlim] sample:		8926.4 time, 2980.5 real, 1816.7 MB
[runlim] sample:		8956.4 time, 2990.5 real, 1820.5 MB
[runlim] sample:		8986.4 time, 3000.5 real, 1827.0 MB
[runlim] sample:		9016.3 time, 3010.5 real, 1832.7 MB
[runlim] sample:		9046.3 time, 3020.5 real, 1835.5 MB
[runlim] sample:		9076.2 time, 3030.5 real, 1841.5 MB
[runlim] sample:		9106.2 time, 3040.5 real, 1844.4 MB
[runlim] sample:		9136.2 time, 3050.5 real, 1848.4 MB
[runlim] sample:		9166.1 time, 3060.5 real, 1849.4 MB
[runlim] sample:		9196.1 time, 3070.5 real, 1852.1 MB
[runlim] sample:		9226.1 time, 3080.5 real, 1854.6 MB
[runlim] sample:		9256.1 time, 3090.5 real, 1860.0 MB
[runlim] sample:		9286.0 time, 3100.5 real, 1862.3 MB
[runlim] sample:		9316.0 time, 3110.5 real, 1867.4 MB
[runlim] sample:		9345.9 time, 3120.5 real, 1869.7 MB
[runlim] sample:		9375.9 time, 3130.5 real, 1872.5 MB
[runlim] sample:		9405.9 time, 3140.5 real, 1874.9 MB
[runlim] sample:		9435.9 time, 3150.5 real, 1877.6 MB
[runlim] sample:		9465.8 time, 3160.5 real, 1881.5 MB
[runlim] sample:		9495.8 time, 3170.5 real, 1879.4 MB
[runlim] sample:		9525.8 time, 3180.5 real, 1881.7 MB
[runlim] sample:		9555.7 time, 3190.5 real, 1885.0 MB
[runlim] sample:		9585.7 time, 3200.5 real, 1884.9 MB
[runlim] sample:		9615.6 time, 3210.5 real, 1887.5 MB
[runlim] sample:		9645.6 time, 3220.5 real, 1890.0 MB
[runlim] sample:		9675.6 time, 3230.5 real, 1893.7 MB
[runlim] sample:		9705.5 time, 3240.5 real, 1898.0 MB
[runlim] sample:		9735.5 time, 3250.5 real, 1902.1 MB
[runlim] sample:		9765.5 time, 3260.5 real, 1908.6 MB
[runlim] sample:		9795.4 time, 3270.5 real, 1915.9 MB
[runlim] sample:		9825.4 time, 3280.5 real, 1918.4 MB
[runlim] sample:		9855.4 time, 3290.5 real, 1919.5 MB
[runlim] sample:		9885.3 time, 3300.5 real, 1919.9 MB
[runlim] sample:		9915.3 time, 3310.5 real, 1927.9 MB
[runlim] sample:		9945.2 time, 3320.5 real, 1927.4 MB
[runlim] sample:		9975.2 time, 3330.5 real, 1932.2 MB
[runlim] sample:		10005.2 time, 3340.5 real, 1931.9 MB
[runlim] sample:		10035.1 time, 3350.5 real, 1936.2 MB
[runlim] sample:		10065.1 time, 3360.5 real, 1934.8 MB
[runlim] sample:		10095.1 time, 3370.5 real, 1945.2 MB
[runlim] sample:		10125.0 time, 3380.5 real, 1939.8 MB
[runlim] sample:		10155.0 time, 3390.5 real, 1943.1 MB
[runlim] sample:		10185.0 time, 3400.5 real, 1946.6 MB
[runlim] sample:		10214.9 time, 3410.5 real, 1948.9 MB
[runlim] sample:		10244.9 time, 3420.5 real, 1952.2 MB
[runlim] sample:		10274.8 time, 3430.5 real, 1956.7 MB
[runlim] sample:		10304.8 time, 3440.5 real, 1960.8 MB
[runlim] sample:		10334.8 time, 3450.5 real, 1965.2 MB
[runlim] sample:		10364.7 time, 3460.5 real, 1969.8 MB
[runlim] sample:		10394.7 time, 3470.5 real, 1974.2 MB
[runlim] sample:		10424.6 time, 3480.5 real, 1980.5 MB
[runlim] sample:		10454.6 time, 3490.5 real, 1983.0 MB
[runlim] sample:		10484.5 time, 3500.5 real, 1985.2 MB
[runlim] sample:		10514.5 time, 3510.5 real, 1987.5 MB
[runlim] sample:		10544.4 time, 3520.5 real, 1987.5 MB
[runlim] sample:		10574.4 time, 3530.5 real, 1989.4 MB
[runlim] sample:		10604.3 time, 3540.5 real, 1991.6 MB
[runlim] sample:		10634.3 time, 3550.5 real, 1996.0 MB
[runlim] sample:		10664.2 time, 3560.5 real, 1998.2 MB
[runlim] sample:		10694.2 time, 3570.5 real, 2002.3 MB
[runlim] sample:		10724.1 time, 3580.5 real, 2008.6 MB
[runlim] sample:		10754.1 time, 3590.5 real, 2011.1 MB
[runlim] end:			Tue Sep 15 22:00:46 2015
[runlim] status:		out of time
[runlim] result:		2
[runlim] children:		0
[runlim] real:			3600.21 seconds
[runlim] time:			10782.90 seconds
[runlim] space:			2015.9 MB
[runlim] samples:		35997
