[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/hwmcc14/single/intel066.aig
[runlim] start:			Thu Sep 17 01:19:58 2015
[runlim] main pid:		31795
[runlim] sample:		18.1 time, 10.3 real, 228.4 MB
[runlim] sample:		38.1 time, 20.3 real, 228.6 MB
[runlim] sample:		72.7 time, 30.3 real, 1278.9 MB
[runlim] sample:		112.3 time, 40.3 real, 1328.5 MB
[runlim] sample:		152.0 time, 50.3 real, 1452.2 MB
[runlim] sample:		191.6 time, 60.3 real, 1509.1 MB
[runlim] sample:		231.2 time, 70.3 real, 1566.4 MB
[runlim] sample:		270.8 time, 80.3 real, 1684.9 MB
[runlim] sample:		310.4 time, 90.3 real, 1717.0 MB
[runlim] sample:		349.9 time, 100.3 real, 1826.4 MB
[runlim] sample:		389.5 time, 110.3 real, 1864.4 MB
[runlim] sample:		429.1 time, 120.3 real, 1954.1 MB
[runlim] sample:		468.7 time, 130.3 real, 1977.0 MB
[runlim] sample:		508.4 time, 140.3 real, 2059.7 MB
[runlim] sample:		547.9 time, 150.3 real, 2098.9 MB
[runlim] sample:		587.5 time, 160.3 real, 2187.2 MB
[runlim] sample:		627.2 time, 170.3 real, 2286.8 MB
[runlim] sample:		666.8 time, 180.3 real, 2301.9 MB
[runlim] sample:		706.4 time, 190.3 real, 2367.9 MB
[runlim] sample:		746.0 time, 200.3 real, 2376.6 MB
[runlim] sample:		785.6 time, 210.3 real, 2453.4 MB
[runlim] sample:		825.2 time, 220.3 real, 2517.0 MB
[runlim] sample:		864.8 time, 230.3 real, 2534.0 MB
[runlim] sample:		904.4 time, 240.3 real, 2604.0 MB
[runlim] sample:		944.0 time, 250.3 real, 2685.6 MB
[runlim] sample:		983.6 time, 260.3 real, 2676.2 MB
[runlim] sample:		1023.2 time, 270.3 real, 2754.3 MB
[runlim] sample:		1062.8 time, 280.3 real, 2824.9 MB
[runlim] sample:		1102.4 time, 290.3 real, 2828.7 MB
[runlim] sample:		1142.0 time, 300.3 real, 2905.3 MB
[runlim] sample:		1181.6 time, 310.3 real, 2919.3 MB
[runlim] sample:		1221.2 time, 320.3 real, 3009.6 MB
[runlim] sample:		1260.8 time, 330.3 real, 3089.9 MB
[runlim] sample:		1300.4 time, 340.3 real, 3074.9 MB
[runlim] sample:		1340.0 time, 350.3 real, 3170.4 MB
[runlim] sample:		1379.6 time, 360.3 real, 3252.6 MB
[runlim] sample:		1419.2 time, 370.3 real, 3319.5 MB
[runlim] sample:		1458.8 time, 380.3 real, 3311.8 MB
[runlim] sample:		1498.4 time, 390.3 real, 3351.0 MB
[runlim] sample:		1538.0 time, 400.3 real, 3403.5 MB
[runlim] sample:		1577.6 time, 410.3 real, 3398.1 MB
[runlim] sample:		1617.2 time, 420.3 real, 3479.9 MB
[runlim] sample:		1656.8 time, 430.3 real, 3549.0 MB
[runlim] sample:		1696.4 time, 440.3 real, 3521.1 MB
[runlim] sample:		1736.0 time, 450.3 real, 3595.6 MB
[runlim] sample:		1775.6 time, 460.3 real, 3652.1 MB
[runlim] sample:		1815.2 time, 470.3 real, 3734.0 MB
[runlim] sample:		1854.8 time, 480.3 real, 3728.5 MB
[runlim] sample:		1894.4 time, 490.3 real, 3800.6 MB
[runlim] sample:		1934.1 time, 500.3 real, 3865.9 MB
[runlim] sample:		1973.7 time, 510.3 real, 3798.2 MB
[runlim] sample:		2013.3 time, 520.3 real, 3853.5 MB
[runlim] sample:		2052.9 time, 530.3 real, 3918.0 MB
[runlim] sample:		2092.5 time, 540.3 real, 3880.9 MB
[runlim] sample:		2132.1 time, 550.3 real, 3976.1 MB
[runlim] sample:		2171.7 time, 560.3 real, 4049.5 MB
[runlim] sample:		2211.3 time, 570.3 real, 4127.6 MB
[runlim] sample:		2250.9 time, 580.3 real, 4172.1 MB
[runlim] sample:		2290.5 time, 590.3 real, 4169.7 MB
[runlim] sample:		2330.1 time, 600.3 real, 4227.7 MB
[runlim] sample:		2369.7 time, 610.3 real, 4293.4 MB
[runlim] sample:		2409.3 time, 620.3 real, 4264.9 MB
[runlim] sample:		2448.9 time, 630.3 real, 4331.9 MB
[runlim] sample:		2488.5 time, 640.3 real, 4395.0 MB
[runlim] sample:		2528.1 time, 650.3 real, 4472.2 MB
[runlim] sample:		2567.8 time, 660.3 real, 4524.2 MB
[runlim] sample:		2607.3 time, 670.3 real, 4514.8 MB
[runlim] sample:		2647.0 time, 680.3 real, 4581.2 MB
[runlim] sample:		2686.6 time, 690.3 real, 4651.2 MB
[runlim] sample:		2726.2 time, 700.3 real, 4641.6 MB
[runlim] sample:		2765.8 time, 710.3 real, 4717.4 MB
[runlim] sample:		2805.4 time, 720.3 real, 4691.5 MB
[runlim] sample:		2845.0 time, 730.3 real, 4784.0 MB
[runlim] sample:		2884.6 time, 740.3 real, 4862.4 MB
[runlim] sample:		2924.2 time, 750.3 real, 4944.0 MB
[runlim] sample:		2963.8 time, 760.3 real, 5013.5 MB
[runlim] sample:		3003.4 time, 770.3 real, 5074.3 MB
[runlim] sample:		2512.6 time, 780.3 real, 4897.7 MB
[runlim] sample:		2552.2 time, 790.3 real, 5002.0 MB
[runlim] sample:		2591.8 time, 800.3 real, 5093.9 MB
[runlim] sample:		2631.4 time, 810.3 real, 5090.6 MB
[runlim] sample:		2671.0 time, 820.3 real, 5221.5 MB
[runlim] sample:		2710.6 time, 830.3 real, 5322.4 MB
[runlim] sample:		2750.2 time, 840.3 real, 5329.7 MB
[runlim] sample:		2789.8 time, 850.3 real, 5402.4 MB
[runlim] sample:		2829.4 time, 860.3 real, 5479.2 MB
[runlim] sample:		2869.0 time, 870.3 real, 5549.6 MB
[runlim] sample:		2908.6 time, 880.3 real, 5616.6 MB
[runlim] sample:		2948.2 time, 890.3 real, 5592.1 MB
[runlim] sample:		2987.8 time, 900.3 real, 5668.1 MB
[runlim] sample:		3027.4 time, 910.3 real, 5737.0 MB
[runlim] sample:		3067.0 time, 920.3 real, 5803.1 MB
[runlim] sample:		3106.6 time, 930.3 real, 5778.0 MB
[runlim] sample:		3146.2 time, 940.3 real, 5864.7 MB
[runlim] sample:		3185.7 time, 950.3 real, 5922.0 MB
[runlim] sample:		3225.3 time, 960.3 real, 5973.9 MB
[runlim] sample:		3264.9 time, 970.3 real, 6019.8 MB
[runlim] sample:		3304.5 time, 980.3 real, 5986.1 MB
[runlim] sample:		3344.1 time, 990.3 real, 6069.1 MB
[runlim] sample:		3383.6 time, 1000.3 real, 6145.0 MB
[runlim] sample:		3423.2 time, 1010.3 real, 6195.9 MB
[runlim] sample:		3462.7 time, 1020.3 real, 6180.0 MB
[runlim] sample:		3502.3 time, 1030.3 real, 6283.7 MB
[runlim] sample:		3541.9 time, 1040.3 real, 6351.3 MB
[runlim] sample:		3581.5 time, 1050.3 real, 6419.8 MB
[runlim] sample:		3621.1 time, 1060.3 real, 6466.4 MB
[runlim] sample:		3660.7 time, 1070.3 real, 6413.1 MB
[runlim] sample:		3700.3 time, 1080.3 real, 6477.7 MB
[runlim] sample:		3739.9 time, 1090.3 real, 6543.7 MB
[runlim] sample:		3779.5 time, 1100.3 real, 6614.8 MB
[runlim] sample:		3819.1 time, 1110.3 real, 6593.4 MB
[runlim] sample:		3858.6 time, 1120.3 real, 6686.8 MB
[runlim] sample:		3898.2 time, 1130.3 real, 6765.2 MB
[runlim] sample:		3937.7 time, 1140.3 real, 6871.0 MB
[runlim] sample:		3977.2 time, 1150.3 real, 6927.4 MB
[runlim] sample:		4016.7 time, 1160.3 real, 6791.2 MB
[runlim] sample:		4056.2 time, 1170.3 real, 6869.5 MB
[runlim] sample:		4095.8 time, 1180.3 real, 6918.9 MB
[runlim] sample:		4135.4 time, 1190.3 real, 6984.4 MB
[runlim] end:			Thu Sep 17 01:39:51 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		7779
[runlim] real:			1193.40 seconds
[runlim] time:			4147.00 seconds
[runlim] space:			7000.5 MB
[runlim] samples:		11930
