[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/pdtrav/single.pdtravthrd
[runlim] argv[1]:		/home/biere/hwmcc15/benchmarks/all/selection/random/beemcmbrdg7f2.aig
[runlim] start:			Sun Sep 20 03:55:50 2015
[runlim] main pid:		7396
[runlim] sample:		29.6 time, 10.3 real, 1022.1 MB
[runlim] sample:		69.2 time, 20.3 real, 1120.0 MB
[runlim] sample:		108.8 time, 30.3 real, 1193.4 MB
[runlim] sample:		148.5 time, 40.3 real, 1194.9 MB
[runlim] sample:		188.1 time, 50.3 real, 1148.8 MB
[runlim] sample:		227.8 time, 60.3 real, 1240.9 MB
[runlim] sample:		267.4 time, 70.3 real, 1305.8 MB
[runlim] sample:		307.0 time, 80.3 real, 1274.6 MB
[runlim] sample:		346.6 time, 90.3 real, 1326.5 MB
[runlim] sample:		386.2 time, 100.3 real, 1255.1 MB
[runlim] sample:		425.9 time, 110.3 real, 1309.3 MB
[runlim] sample:		465.5 time, 120.3 real, 1366.4 MB
[runlim] sample:		505.1 time, 130.3 real, 1428.2 MB
[runlim] sample:		544.7 time, 140.3 real, 1471.4 MB
[runlim] sample:		584.4 time, 150.3 real, 1481.2 MB
[runlim] sample:		624.0 time, 160.3 real, 1520.2 MB
[runlim] sample:		663.6 time, 170.3 real, 1483.4 MB
[runlim] sample:		703.2 time, 180.3 real, 1554.8 MB
[runlim] sample:		742.8 time, 190.3 real, 1612.1 MB
[runlim] sample:		782.4 time, 200.3 real, 1474.7 MB
[runlim] sample:		822.1 time, 210.3 real, 1530.9 MB
[runlim] sample:		861.7 time, 220.3 real, 1474.1 MB
[runlim] sample:		901.3 time, 230.3 real, 1501.3 MB
[runlim] sample:		940.9 time, 240.3 real, 1530.0 MB
[runlim] sample:		980.5 time, 250.3 real, 1557.0 MB
[runlim] sample:		1020.1 time, 260.3 real, 1585.4 MB
[runlim] sample:		1059.8 time, 270.3 real, 1508.4 MB
[runlim] sample:		1099.4 time, 280.3 real, 1562.9 MB
[runlim] sample:		1139.0 time, 290.3 real, 1604.8 MB
[runlim] sample:		1178.6 time, 300.3 real, 1639.2 MB
[runlim] sample:		1218.2 time, 310.3 real, 1672.5 MB
[runlim] sample:		1257.8 time, 320.3 real, 1708.9 MB
[runlim] sample:		1297.5 time, 330.3 real, 1810.7 MB
[runlim] sample:		1337.1 time, 340.3 real, 1925.1 MB
[runlim] sample:		1376.7 time, 350.3 real, 1984.7 MB
[runlim] sample:		1416.3 time, 360.3 real, 2051.4 MB
[runlim] sample:		1456.0 time, 370.3 real, 1759.4 MB
[runlim] sample:		1495.6 time, 380.3 real, 1843.0 MB
[runlim] sample:		1535.2 time, 390.3 real, 1947.2 MB
[runlim] sample:		1574.8 time, 400.3 real, 2016.4 MB
[runlim] sample:		1614.5 time, 410.3 real, 2091.5 MB
[runlim] sample:		1654.1 time, 420.3 real, 2165.7 MB
[runlim] sample:		1693.7 time, 430.3 real, 2230.2 MB
[runlim] sample:		1733.3 time, 440.3 real, 2296.9 MB
[runlim] sample:		1772.9 time, 450.3 real, 2353.4 MB
[runlim] sample:		1812.6 time, 460.3 real, 2460.1 MB
[runlim] sample:		1852.2 time, 470.3 real, 2528.8 MB
[runlim] sample:		1891.8 time, 480.3 real, 2568.2 MB
[runlim] sample:		1931.4 time, 490.3 real, 2612.1 MB
[runlim] sample:		1971.0 time, 500.3 real, 2164.5 MB
[runlim] sample:		2010.6 time, 510.3 real, 2231.9 MB
[runlim] sample:		2050.2 time, 520.3 real, 2172.0 MB
[runlim] sample:		2089.9 time, 530.3 real, 2206.7 MB
[runlim] sample:		2129.5 time, 540.3 real, 2239.6 MB
[runlim] sample:		2169.1 time, 550.3 real, 2299.0 MB
[runlim] sample:		2208.7 time, 560.3 real, 2181.7 MB
[runlim] sample:		2248.3 time, 570.3 real, 2222.4 MB
[runlim] sample:		2287.9 time, 580.3 real, 2252.5 MB
[runlim] sample:		2327.6 time, 590.3 real, 2281.3 MB
[runlim] sample:		2367.2 time, 600.3 real, 2327.5 MB
[runlim] sample:		2406.8 time, 610.3 real, 2468.8 MB
[runlim] sample:		2446.4 time, 620.3 real, 2510.9 MB
[runlim] sample:		2486.0 time, 630.3 real, 2539.9 MB
[runlim] sample:		2525.6 time, 640.3 real, 2589.1 MB
[runlim] sample:		2565.2 time, 650.3 real, 2627.2 MB
[runlim] sample:		2604.8 time, 660.3 real, 2419.0 MB
[runlim] sample:		2644.4 time, 670.3 real, 2463.6 MB
[runlim] sample:		2684.1 time, 680.3 real, 2509.5 MB
[runlim] sample:		2723.7 time, 690.3 real, 2571.7 MB
[runlim] sample:		2763.3 time, 700.3 real, 2647.7 MB
[runlim] sample:		2802.9 time, 710.3 real, 2716.2 MB
[runlim] sample:		2842.5 time, 720.3 real, 2766.6 MB
[runlim] sample:		2882.1 time, 730.3 real, 2805.0 MB
[runlim] sample:		2921.7 time, 740.3 real, 2847.8 MB
[runlim] sample:		2961.3 time, 750.3 real, 2902.2 MB
[runlim] sample:		3001.0 time, 760.3 real, 2974.8 MB
[runlim] sample:		3040.6 time, 770.3 real, 3033.4 MB
[runlim] sample:		3080.2 time, 780.3 real, 3091.1 MB
[runlim] sample:		3119.8 time, 790.3 real, 3147.0 MB
[runlim] sample:		3159.4 time, 800.3 real, 3212.2 MB
[runlim] sample:		3199.0 time, 810.3 real, 3270.2 MB
[runlim] sample:		3238.6 time, 820.3 real, 3331.5 MB
[runlim] sample:		3278.2 time, 830.3 real, 2909.1 MB
[runlim] sample:		3317.9 time, 840.3 real, 3001.6 MB
[runlim] sample:		3357.5 time, 850.3 real, 3101.7 MB
[runlim] sample:		3397.1 time, 860.3 real, 3164.0 MB
[runlim] sample:		3436.7 time, 870.3 real, 3245.8 MB
[runlim] sample:		3476.3 time, 880.3 real, 3315.0 MB
[runlim] sample:		3515.9 time, 890.3 real, 3388.7 MB
[runlim] sample:		3555.5 time, 900.3 real, 3466.2 MB
[runlim] sample:		3595.2 time, 910.3 real, 3540.7 MB
[runlim] sample:		3634.8 time, 920.3 real, 3595.3 MB
[runlim] sample:		3674.4 time, 930.3 real, 3657.9 MB
[runlim] sample:		3714.0 time, 940.3 real, 3721.3 MB
[runlim] sample:		3753.6 time, 950.3 real, 3773.7 MB
[runlim] sample:		3793.2 time, 960.3 real, 3824.0 MB
[runlim] sample:		3832.8 time, 970.3 real, 3873.8 MB
[runlim] sample:		3872.4 time, 980.3 real, 3917.0 MB
[runlim] sample:		3912.0 time, 990.3 real, 3964.7 MB
[runlim] sample:		3951.6 time, 1000.3 real, 3454.4 MB
[runlim] sample:		3991.2 time, 1010.3 real, 3666.6 MB
[runlim] sample:		4030.8 time, 1020.3 real, 3728.1 MB
[runlim] sample:		4070.4 time, 1030.3 real, 3793.9 MB
[runlim] sample:		4110.1 time, 1040.3 real, 3853.8 MB
[runlim] sample:		4149.7 time, 1050.3 real, 3881.9 MB
[runlim] sample:		4189.3 time, 1060.3 real, 3957.7 MB
[runlim] sample:		4228.9 time, 1070.3 real, 4023.0 MB
[runlim] sample:		4268.5 time, 1080.3 real, 3853.8 MB
[runlim] sample:		4308.1 time, 1090.3 real, 3904.9 MB
[runlim] sample:		4347.8 time, 1100.3 real, 3953.7 MB
[runlim] sample:		4387.4 time, 1110.3 real, 4040.3 MB
[runlim] sample:		4426.9 time, 1120.3 real, 4108.4 MB
[runlim] sample:		4466.6 time, 1130.3 real, 4190.6 MB
[runlim] sample:		4506.2 time, 1140.3 real, 4308.5 MB
[runlim] sample:		4545.8 time, 1150.3 real, 4356.6 MB
[runlim] sample:		4585.4 time, 1160.3 real, 4403.2 MB
[runlim] sample:		4625.0 time, 1170.3 real, 4465.6 MB
[runlim] sample:		4664.6 time, 1180.3 real, 4537.0 MB
[runlim] sample:		4704.2 time, 1190.3 real, 4587.9 MB
[runlim] sample:		4743.8 time, 1200.3 real, 4650.8 MB
[runlim] sample:		4783.4 time, 1210.3 real, 4720.3 MB
[runlim] sample:		4823.1 time, 1220.3 real, 4779.6 MB
[runlim] sample:		4862.7 time, 1230.3 real, 4840.1 MB
[runlim] sample:		4902.3 time, 1240.3 real, 4905.4 MB
[runlim] sample:		4941.9 time, 1250.3 real, 4259.5 MB
[runlim] sample:		4981.5 time, 1260.3 real, 4354.9 MB
[runlim] sample:		5021.1 time, 1270.3 real, 4425.4 MB
[runlim] sample:		5060.7 time, 1280.3 real, 4496.2 MB
[runlim] sample:		5100.3 time, 1290.3 real, 4575.4 MB
[runlim] sample:		5139.9 time, 1300.3 real, 4675.0 MB
[runlim] sample:		5179.6 time, 1310.3 real, 4760.5 MB
[runlim] sample:		5219.1 time, 1320.3 real, 4839.8 MB
[runlim] sample:		5258.8 time, 1330.3 real, 4903.9 MB
[runlim] sample:		5298.4 time, 1340.3 real, 4973.7 MB
[runlim] sample:		5338.0 time, 1350.3 real, 5040.2 MB
[runlim] sample:		5377.6 time, 1360.3 real, 5128.6 MB
[runlim] sample:		5417.2 time, 1370.3 real, 5204.9 MB
[runlim] sample:		5456.8 time, 1380.3 real, 5281.8 MB
[runlim] sample:		5496.4 time, 1390.3 real, 5357.2 MB
[runlim] sample:		5536.0 time, 1400.3 real, 5421.4 MB
[runlim] sample:		5575.6 time, 1410.3 real, 5485.4 MB
[runlim] sample:		5615.2 time, 1420.3 real, 5554.3 MB
[runlim] sample:		5654.8 time, 1430.3 real, 5604.3 MB
[runlim] sample:		5694.4 time, 1440.3 real, 5678.8 MB
[runlim] sample:		5734.0 time, 1450.3 real, 5733.7 MB
[runlim] sample:		5773.6 time, 1460.3 real, 5799.8 MB
[runlim] sample:		5813.2 time, 1470.3 real, 5867.9 MB
[runlim] sample:		5852.8 time, 1480.3 real, 5926.4 MB
[runlim] sample:		5892.4 time, 1490.3 real, 5276.7 MB
[runlim] sample:		5932.0 time, 1500.3 real, 5357.7 MB
[runlim] sample:		5971.6 time, 1510.3 real, 5467.5 MB
[runlim] sample:		6011.2 time, 1520.3 real, 5531.7 MB
[runlim] sample:		6050.8 time, 1530.3 real, 5598.3 MB
[runlim] sample:		6090.4 time, 1540.3 real, 5666.7 MB
[runlim] sample:		6130.1 time, 1550.3 real, 5735.2 MB
[runlim] sample:		6169.7 time, 1560.3 real, 5803.1 MB
[runlim] sample:		6209.2 time, 1570.3 real, 5873.2 MB
[runlim] sample:		6248.8 time, 1580.3 real, 5585.6 MB
[runlim] sample:		6288.4 time, 1590.3 real, 5648.5 MB
[runlim] sample:		6328.0 time, 1600.3 real, 5707.3 MB
[runlim] sample:		6367.6 time, 1610.3 real, 5776.3 MB
[runlim] sample:		6407.2 time, 1620.3 real, 5832.7 MB
[runlim] sample:		6446.8 time, 1630.3 real, 5879.2 MB
[runlim] sample:		6486.4 time, 1640.3 real, 5779.4 MB
[runlim] sample:		6526.0 time, 1650.3 real, 5837.9 MB
[runlim] sample:		6565.6 time, 1660.3 real, 5898.6 MB
[runlim] sample:		6605.2 time, 1670.3 real, 5965.3 MB
[runlim] sample:		6644.8 time, 1680.3 real, 6023.6 MB
[runlim] sample:		6684.4 time, 1690.3 real, 6080.2 MB
[runlim] sample:		6723.9 time, 1700.3 real, 6120.4 MB
[runlim] sample:		6763.5 time, 1710.3 real, 6159.0 MB
[runlim] sample:		6803.1 time, 1720.3 real, 6195.4 MB
[runlim] sample:		6842.7 time, 1730.3 real, 6222.5 MB
[runlim] sample:		6882.4 time, 1740.3 real, 6258.9 MB
[runlim] sample:		6922.0 time, 1750.3 real, 6305.3 MB
[runlim] sample:		6961.6 time, 1760.3 real, 6086.0 MB
[runlim] sample:		7001.1 time, 1770.3 real, 6130.2 MB
[runlim] sample:		7040.7 time, 1780.3 real, 6190.9 MB
[runlim] sample:		7080.3 time, 1790.3 real, 6224.1 MB
[runlim] sample:		7119.9 time, 1800.3 real, 6257.2 MB
[runlim] sample:		7159.6 time, 1810.3 real, 6301.2 MB
[runlim] sample:		7199.1 time, 1820.3 real, 6361.5 MB
[runlim] sample:		7238.8 time, 1830.3 real, 6387.6 MB
[runlim] sample:		7278.3 time, 1840.3 real, 6414.2 MB
[runlim] sample:		7317.9 time, 1850.3 real, 6458.5 MB
[runlim] sample:		7357.5 time, 1860.3 real, 6492.5 MB
[runlim] sample:		7397.1 time, 1870.3 real, 6535.3 MB
[runlim] sample:		7436.7 time, 1880.3 real, 6581.9 MB
[runlim] sample:		7476.3 time, 1890.3 real, 6622.0 MB
[runlim] sample:		7515.9 time, 1900.3 real, 6272.3 MB
[runlim] sample:		7555.5 time, 1910.3 real, 6308.9 MB
[runlim] sample:		7595.1 time, 1920.3 real, 4627.9 MB
[runlim] sample:		7634.7 time, 1930.3 real, 4687.4 MB
[runlim] sample:		7674.3 time, 1940.3 real, 4734.4 MB
[runlim] sample:		7713.8 time, 1950.3 real, 4793.2 MB
[runlim] sample:		7753.4 time, 1960.3 real, 4869.6 MB
[runlim] sample:		7793.0 time, 1970.3 real, 4952.5 MB
[runlim] sample:		7832.6 time, 1980.3 real, 5002.9 MB
[runlim] sample:		7872.2 time, 1990.3 real, 5044.9 MB
[runlim] sample:		7911.8 time, 2000.3 real, 5099.9 MB
[runlim] sample:		7951.4 time, 2010.3 real, 5138.4 MB
[runlim] sample:		7991.0 time, 2020.3 real, 5186.1 MB
[runlim] sample:		8030.6 time, 2030.3 real, 5230.7 MB
[runlim] sample:		8070.2 time, 2040.3 real, 5286.6 MB
[runlim] sample:		8109.8 time, 2050.3 real, 5332.6 MB
[runlim] sample:		8149.4 time, 2060.3 real, 5384.8 MB
[runlim] sample:		8189.0 time, 2070.3 real, 5428.9 MB
[runlim] sample:		8228.6 time, 2080.3 real, 5487.4 MB
[runlim] sample:		8268.2 time, 2090.3 real, 5561.3 MB
[runlim] sample:		8307.8 time, 2100.3 real, 5153.4 MB
[runlim] sample:		8347.4 time, 2110.3 real, 5199.7 MB
[runlim] sample:		8387.0 time, 2120.3 real, 5262.0 MB
[runlim] sample:		8426.6 time, 2130.3 real, 5328.1 MB
[runlim] sample:		8466.2 time, 2140.3 real, 5387.9 MB
[runlim] sample:		8505.8 time, 2150.3 real, 5454.0 MB
[runlim] sample:		8545.4 time, 2160.3 real, 5514.0 MB
[runlim] sample:		8585.0 time, 2170.3 real, 5564.5 MB
[runlim] sample:		8624.5 time, 2180.3 real, 5606.6 MB
[runlim] sample:		8664.1 time, 2190.3 real, 5662.5 MB
[runlim] sample:		8703.7 time, 2200.3 real, 5718.5 MB
[runlim] sample:		8743.3 time, 2210.3 real, 5760.5 MB
[runlim] sample:		8782.9 time, 2220.3 real, 5804.5 MB
[runlim] sample:		8822.5 time, 2230.3 real, 5842.7 MB
[runlim] sample:		8862.1 time, 2240.3 real, 5877.8 MB
[runlim] sample:		8901.7 time, 2250.3 real, 5930.2 MB
[runlim] sample:		8941.3 time, 2260.3 real, 5976.3 MB
[runlim] sample:		8980.9 time, 2270.3 real, 6039.4 MB
[runlim] sample:		9020.4 time, 2280.3 real, 5548.6 MB
[runlim] sample:		9060.0 time, 2290.3 real, 5610.8 MB
[runlim] sample:		9099.6 time, 2300.3 real, 5710.7 MB
[runlim] sample:		9139.2 time, 2310.3 real, 5789.3 MB
[runlim] sample:		9178.8 time, 2320.3 real, 5863.7 MB
[runlim] sample:		9218.4 time, 2330.3 real, 5922.0 MB
[runlim] sample:		9258.0 time, 2340.3 real, 5975.9 MB
[runlim] sample:		9297.6 time, 2350.3 real, 6038.1 MB
[runlim] sample:		9337.2 time, 2360.3 real, 6094.1 MB
[runlim] sample:		9376.7 time, 2370.3 real, 6137.9 MB
[runlim] sample:		9416.4 time, 2380.3 real, 6190.2 MB
[runlim] sample:		9456.0 time, 2390.3 real, 6246.9 MB
[runlim] sample:		9495.6 time, 2400.3 real, 6298.2 MB
[runlim] sample:		9535.2 time, 2410.3 real, 6370.2 MB
[runlim] sample:		9574.8 time, 2420.3 real, 6434.4 MB
[runlim] sample:		9614.4 time, 2430.3 real, 6490.6 MB
[runlim] sample:		9654.0 time, 2440.3 real, 6550.9 MB
[runlim] sample:		9693.6 time, 2450.3 real, 6602.4 MB
[runlim] sample:		9733.2 time, 2460.3 real, 6646.2 MB
[runlim] sample:		9772.8 time, 2470.3 real, 6696.3 MB
[runlim] sample:		9812.5 time, 2480.3 real, 6749.1 MB
[runlim] sample:		9852.1 time, 2490.3 real, 6792.8 MB
[runlim] sample:		9891.7 time, 2500.3 real, 6822.5 MB
[runlim] sample:		9931.3 time, 2510.3 real, 6863.4 MB
[runlim] sample:		9970.9 time, 2520.3 real, 6894.3 MB
[runlim] sample:		10010.5 time, 2530.3 real, 6934.2 MB
[runlim] end:			Sun Sep 20 04:38:03 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		37
[runlim] real:			2533.33 seconds
[runlim] time:			10021.50 seconds
[runlim] space:			7027.4 MB
[runlim] samples:		25330
