[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/6s39.aig
[runlim] start:			Wed Sep 16 14:07:02 2015
[runlim] main pid:		27300
[runlim] sample:		25.4 time, 10.2 real, 1090.0 MB
[runlim] sample:		65.0 time, 20.2 real, 1243.7 MB
[runlim] sample:		90.2 time, 30.2 real, 1198.3 MB
[runlim] sample:		129.8 time, 40.2 real, 1223.7 MB
[runlim] sample:		169.4 time, 50.2 real, 1260.6 MB
[runlim] sample:		209.0 time, 60.2 real, 1279.0 MB
[runlim] sample:		248.6 time, 70.2 real, 1319.6 MB
[runlim] sample:		288.2 time, 80.2 real, 1316.0 MB
[runlim] sample:		327.9 time, 90.2 real, 1395.4 MB
[runlim] sample:		367.5 time, 100.2 real, 1357.9 MB
[runlim] sample:		407.1 time, 110.2 real, 1366.5 MB
[runlim] sample:		446.7 time, 120.2 real, 1449.4 MB
[runlim] sample:		486.3 time, 130.2 real, 1436.5 MB
[runlim] sample:		525.9 time, 140.2 real, 1478.1 MB
[runlim] sample:		565.6 time, 150.2 real, 1517.1 MB
[runlim] sample:		605.2 time, 160.2 real, 1531.3 MB
[runlim] sample:		644.8 time, 170.2 real, 1506.3 MB
[runlim] sample:		684.4 time, 180.2 real, 1554.3 MB
[runlim] sample:		724.0 time, 190.2 real, 1538.1 MB
[runlim] sample:		763.7 time, 200.2 real, 1565.0 MB
[runlim] sample:		803.3 time, 210.2 real, 1557.3 MB
[runlim] sample:		842.9 time, 220.2 real, 1557.6 MB
[runlim] sample:		882.5 time, 230.2 real, 1631.0 MB
[runlim] sample:		922.1 time, 240.2 real, 1585.7 MB
[runlim] sample:		961.7 time, 250.2 real, 1661.3 MB
[runlim] sample:		1001.3 time, 260.2 real, 1670.1 MB
[runlim] sample:		1041.0 time, 270.2 real, 1619.4 MB
[runlim] sample:		1080.6 time, 280.2 real, 1640.7 MB
[runlim] sample:		1120.2 time, 290.2 real, 1723.0 MB
[runlim] sample:		1159.8 time, 300.2 real, 1581.1 MB
[runlim] sample:		1199.4 time, 310.2 real, 1643.5 MB
[runlim] sample:		1239.0 time, 320.2 real, 1593.1 MB
[runlim] sample:		1278.6 time, 330.2 real, 1583.4 MB
[runlim] sample:		1318.3 time, 340.2 real, 1698.5 MB
[runlim] sample:		1357.9 time, 350.2 real, 1704.4 MB
[runlim] sample:		1397.5 time, 360.2 real, 1621.6 MB
[runlim] sample:		1437.1 time, 370.2 real, 1630.2 MB
[runlim] sample:		1476.7 time, 380.2 real, 1741.3 MB
[runlim] sample:		1516.3 time, 390.2 real, 1737.6 MB
[runlim] sample:		1555.9 time, 400.2 real, 1655.7 MB
[runlim] sample:		1595.5 time, 410.2 real, 1760.6 MB
[runlim] sample:		1635.1 time, 420.2 real, 1808.8 MB
[runlim] sample:		1674.8 time, 430.2 real, 1682.0 MB
[runlim] sample:		1714.4 time, 440.2 real, 1775.5 MB
[runlim] sample:		1754.0 time, 450.2 real, 1797.4 MB
[runlim] sample:		1793.6 time, 460.2 real, 1828.5 MB
[runlim] sample:		1833.2 time, 470.2 real, 1747.9 MB
[runlim] sample:		1872.8 time, 480.2 real, 1709.5 MB
[runlim] sample:		1912.5 time, 490.2 real, 1803.7 MB
[runlim] sample:		1952.1 time, 500.2 real, 1861.3 MB
[runlim] sample:		1991.7 time, 510.2 real, 1873.9 MB
[runlim] sample:		2031.3 time, 520.2 real, 1886.7 MB
[runlim] sample:		2070.9 time, 530.2 real, 1893.5 MB
[runlim] sample:		2110.5 time, 540.2 real, 1810.6 MB
[runlim] sample:		2150.1 time, 550.2 real, 1869.4 MB
[runlim] sample:		2189.7 time, 560.2 real, 1948.2 MB
[runlim] sample:		2229.3 time, 570.2 real, 1955.7 MB
[runlim] sample:		2268.9 time, 580.2 real, 1961.2 MB
[runlim] sample:		2308.5 time, 590.2 real, 1964.0 MB
[runlim] sample:		2348.1 time, 600.2 real, 1969.9 MB
[runlim] sample:		2387.7 time, 610.2 real, 2112.5 MB
[runlim] sample:		2427.4 time, 620.2 real, 2120.0 MB
[runlim] sample:		2467.0 time, 630.2 real, 2241.4 MB
[runlim] sample:		2506.6 time, 640.2 real, 2282.6 MB
[runlim] sample:		2546.2 time, 650.2 real, 2411.6 MB
[runlim] sample:		2585.8 time, 660.2 real, 2466.3 MB
[runlim] sample:		2625.4 time, 670.2 real, 2504.2 MB
[runlim] sample:		2665.0 time, 680.2 real, 2562.8 MB
[runlim] sample:		2704.7 time, 690.2 real, 2702.7 MB
[runlim] sample:		2744.3 time, 700.2 real, 2789.9 MB
[runlim] sample:		2783.9 time, 710.2 real, 2885.1 MB
[runlim] sample:		2823.5 time, 720.2 real, 2979.2 MB
[runlim] sample:		2863.1 time, 730.2 real, 3158.0 MB
[runlim] sample:		2902.8 time, 740.2 real, 3297.0 MB
[runlim] sample:		2942.4 time, 750.2 real, 3408.5 MB
[runlim] sample:		2982.0 time, 760.2 real, 3503.6 MB
[runlim] sample:		3021.6 time, 770.2 real, 3614.5 MB
[runlim] sample:		3061.2 time, 780.2 real, 4097.9 MB
[runlim] sample:		3100.9 time, 790.2 real, 4145.6 MB
[runlim] sample:		3140.5 time, 800.2 real, 4205.8 MB
[runlim] sample:		3180.1 time, 810.2 real, 4269.8 MB
[runlim] sample:		3219.7 time, 820.2 real, 4364.0 MB
[runlim] sample:		3259.4 time, 830.2 real, 4405.6 MB
[runlim] sample:		3299.0 time, 840.2 real, 4508.8 MB
[runlim] sample:		3338.6 time, 850.2 real, 4538.2 MB
[runlim] sample:		3378.2 time, 860.2 real, 4548.9 MB
[runlim] sample:		3417.9 time, 870.2 real, 4569.7 MB
[runlim] sample:		3457.5 time, 880.2 real, 4643.2 MB
[runlim] sample:		3497.1 time, 890.2 real, 4686.8 MB
[runlim] sample:		3536.7 time, 900.2 real, 4714.2 MB
[runlim] sample:		3576.3 time, 910.2 real, 4779.3 MB
[runlim] sample:		3615.9 time, 920.2 real, 4788.8 MB
[runlim] sample:		3655.6 time, 930.2 real, 4842.8 MB
[runlim] sample:		3695.2 time, 940.2 real, 4857.2 MB
[runlim] sample:		3734.8 time, 950.2 real, 4930.7 MB
[runlim] sample:		3774.4 time, 960.2 real, 5381.0 MB
[runlim] sample:		3814.0 time, 970.2 real, 5420.1 MB
[runlim] sample:		3853.6 time, 980.2 real, 5385.0 MB
[runlim] sample:		3893.2 time, 990.2 real, 5504.8 MB
[runlim] sample:		3932.9 time, 1000.2 real, 5522.8 MB
[runlim] sample:		3972.5 time, 1010.2 real, 5595.5 MB
[runlim] sample:		4012.1 time, 1020.2 real, 5616.1 MB
[runlim] sample:		4051.7 time, 1030.2 real, 5659.5 MB
[runlim] sample:		4091.3 time, 1040.2 real, 5677.0 MB
[runlim] sample:		4130.9 time, 1050.2 real, 5714.9 MB
[runlim] sample:		4170.6 time, 1060.2 real, 5689.8 MB
[runlim] sample:		4210.2 time, 1070.2 real, 5738.7 MB
[runlim] sample:		4249.8 time, 1080.2 real, 5825.2 MB
[runlim] sample:		4289.4 time, 1090.2 real, 5935.7 MB
[runlim] sample:		4329.1 time, 1100.2 real, 6096.5 MB
[runlim] sample:		4368.7 time, 1110.2 real, 6091.3 MB
[runlim] sample:		4408.3 time, 1120.2 real, 6158.3 MB
[runlim] sample:		4448.0 time, 1130.2 real, 6247.8 MB
[runlim] sample:		4487.6 time, 1140.2 real, 6258.2 MB
[runlim] sample:		4527.2 time, 1150.2 real, 6386.7 MB
[runlim] sample:		4566.9 time, 1160.2 real, 6470.4 MB
[runlim] sample:		4606.5 time, 1170.2 real, 6623.5 MB
[runlim] sample:		4646.1 time, 1180.2 real, 6938.4 MB
[runlim] sample:		4685.7 time, 1190.2 real, 6949.6 MB
[runlim] sample:		4725.3 time, 1200.2 real, 6887.6 MB
[runlim] sample:		4764.9 time, 1210.2 real, 6930.0 MB
[runlim] end:			Wed Sep 16 14:27:17 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		195
[runlim] real:			1215.53 seconds
[runlim] time:			4784.91 seconds
[runlim] space:			7011.9 MB
[runlim] samples:		12152
