[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/6s320rb0.aig
[runlim] start:			Sun Sep 20 16:07:22 2015
[runlim] main pid:		8862
[runlim] sample:		18.1 time, 10.5 real, 228.1 MB
[runlim] sample:		38.1 time, 20.5 real, 228.7 MB
[runlim] sample:		58.1 time, 30.5 real, 229.0 MB
[runlim] sample:		78.0 time, 40.5 real, 229.0 MB
[runlim] sample:		98.0 time, 50.5 real, 229.2 MB
[runlim] sample:		118.0 time, 60.5 real, 229.2 MB
[runlim] sample:		141.7 time, 70.5 real, 1025.9 MB
[runlim] sample:		181.3 time, 80.5 real, 1116.5 MB
[runlim] sample:		221.0 time, 90.5 real, 1164.0 MB
[runlim] sample:		260.6 time, 100.5 real, 1187.6 MB
[runlim] sample:		300.2 time, 110.5 real, 1226.2 MB
[runlim] sample:		339.8 time, 120.5 real, 1279.7 MB
[runlim] sample:		379.4 time, 130.5 real, 1291.1 MB
[runlim] sample:		419.0 time, 140.5 real, 1303.6 MB
[runlim] sample:		458.7 time, 150.5 real, 1319.6 MB
[runlim] sample:		498.3 time, 160.5 real, 1352.2 MB
[runlim] sample:		537.9 time, 170.5 real, 1382.7 MB
[runlim] sample:		577.5 time, 180.5 real, 1390.9 MB
[runlim] sample:		617.1 time, 190.5 real, 1403.7 MB
[runlim] sample:		656.7 time, 200.5 real, 1412.9 MB
[runlim] sample:		696.3 time, 210.5 real, 1454.9 MB
[runlim] sample:		596.3 time, 220.5 real, 1249.3 MB
[runlim] sample:		635.9 time, 230.5 real, 1275.9 MB
[runlim] sample:		675.5 time, 240.5 real, 1275.2 MB
[runlim] sample:		715.1 time, 250.5 real, 1302.1 MB
[runlim] sample:		754.7 time, 260.5 real, 1337.3 MB
[runlim] sample:		794.3 time, 270.5 real, 1369.6 MB
[runlim] sample:		834.0 time, 280.5 real, 1399.4 MB
[runlim] sample:		873.6 time, 290.5 real, 1432.6 MB
[runlim] sample:		913.2 time, 300.5 real, 1493.3 MB
[runlim] sample:		952.8 time, 310.5 real, 1526.4 MB
[runlim] sample:		992.4 time, 320.5 real, 1548.4 MB
[runlim] sample:		1032.0 time, 330.5 real, 1587.3 MB
[runlim] sample:		1071.6 time, 340.5 real, 1628.2 MB
[runlim] sample:		1111.2 time, 350.5 real, 1672.5 MB
[runlim] sample:		1150.9 time, 360.5 real, 1703.1 MB
[runlim] sample:		1190.5 time, 370.5 real, 1727.3 MB
[runlim] sample:		1230.1 time, 380.5 real, 1760.2 MB
[runlim] sample:		1269.7 time, 390.5 real, 1791.1 MB
[runlim] sample:		1309.3 time, 400.5 real, 1809.3 MB
[runlim] sample:		1349.0 time, 410.5 real, 1620.5 MB
[runlim] sample:		1388.6 time, 420.5 real, 1643.9 MB
[runlim] sample:		1428.2 time, 430.5 real, 1670.7 MB
[runlim] sample:		1467.8 time, 440.5 real, 1689.7 MB
[runlim] sample:		1507.4 time, 450.5 real, 1713.0 MB
[runlim] sample:		1547.0 time, 460.5 real, 1733.5 MB
[runlim] sample:		1586.7 time, 470.5 real, 1751.7 MB
[runlim] sample:		1626.3 time, 480.5 real, 1766.0 MB
[runlim] sample:		1665.9 time, 490.5 real, 1786.3 MB
[runlim] sample:		1705.5 time, 500.5 real, 1801.8 MB
[runlim] sample:		1745.1 time, 510.5 real, 1820.7 MB
[runlim] sample:		1784.7 time, 520.5 real, 1839.4 MB
[runlim] sample:		1824.3 time, 530.5 real, 1859.7 MB
[runlim] sample:		1864.0 time, 540.5 real, 1879.5 MB
[runlim] sample:		1903.6 time, 550.5 real, 1896.2 MB
[runlim] sample:		1943.2 time, 560.5 real, 1910.5 MB
[runlim] sample:		1982.8 time, 570.5 real, 1921.9 MB
[runlim] sample:		2022.4 time, 580.5 real, 1937.9 MB
[runlim] sample:		2062.0 time, 590.5 real, 1954.2 MB
[runlim] sample:		2101.6 time, 600.5 real, 1974.3 MB
[runlim] sample:		2141.2 time, 610.5 real, 2045.0 MB
[runlim] sample:		2180.8 time, 620.5 real, 2066.0 MB
[runlim] sample:		2220.4 time, 630.5 real, 2095.0 MB
[runlim] sample:		2260.1 time, 640.5 real, 2113.1 MB
[runlim] sample:		2299.7 time, 650.5 real, 2139.2 MB
[runlim] sample:		2339.3 time, 660.5 real, 1770.3 MB
[runlim] sample:		2378.9 time, 670.5 real, 1800.8 MB
[runlim] sample:		2418.5 time, 680.5 real, 1826.4 MB
[runlim] sample:		2458.1 time, 690.5 real, 1860.0 MB
[runlim] sample:		2497.7 time, 700.5 real, 1894.9 MB
[runlim] sample:		2537.3 time, 710.5 real, 1951.4 MB
[runlim] sample:		2576.9 time, 720.5 real, 1991.8 MB
[runlim] sample:		2616.5 time, 730.5 real, 2019.7 MB
[runlim] sample:		2656.1 time, 740.5 real, 2048.7 MB
[runlim] sample:		2695.8 time, 750.5 real, 2076.0 MB
[runlim] sample:		2735.3 time, 760.5 real, 2111.7 MB
[runlim] sample:		2775.0 time, 770.5 real, 2142.2 MB
[runlim] sample:		2814.6 time, 780.5 real, 2177.1 MB
[runlim] sample:		2854.2 time, 790.5 real, 2212.5 MB
[runlim] sample:		2893.8 time, 800.5 real, 2251.8 MB
[runlim] sample:		2933.4 time, 810.5 real, 2285.2 MB
[runlim] sample:		2973.0 time, 820.5 real, 2308.6 MB
[runlim] sample:		3012.6 time, 830.5 real, 2339.8 MB
[runlim] sample:		3052.2 time, 840.5 real, 2372.3 MB
[runlim] sample:		3091.8 time, 850.5 real, 2392.9 MB
[runlim] sample:		3131.5 time, 860.5 real, 2418.8 MB
[runlim] sample:		3171.1 time, 870.5 real, 2440.0 MB
[runlim] sample:		3210.7 time, 880.5 real, 2468.3 MB
[runlim] sample:		3250.3 time, 890.5 real, 2496.8 MB
[runlim] sample:		3289.9 time, 900.5 real, 2539.5 MB
[runlim] sample:		3329.5 time, 910.5 real, 2572.1 MB
[runlim] sample:		3369.1 time, 920.5 real, 2653.8 MB
[runlim] sample:		3408.7 time, 930.5 real, 2692.2 MB
[runlim] sample:		3448.3 time, 940.5 real, 2743.1 MB
[runlim] sample:		3487.9 time, 950.5 real, 2773.4 MB
[runlim] sample:		3527.5 time, 960.5 real, 2806.5 MB
[runlim] sample:		3567.1 time, 970.5 real, 2839.5 MB
[runlim] sample:		3606.7 time, 980.5 real, 2872.8 MB
[runlim] sample:		3646.3 time, 990.5 real, 2902.0 MB
[runlim] sample:		3685.9 time, 1000.5 real, 2927.0 MB
[runlim] sample:		3725.5 time, 1010.5 real, 2954.8 MB
[runlim] sample:		3765.1 time, 1020.5 real, 2987.0 MB
[runlim] sample:		3804.7 time, 1030.5 real, 2699.2 MB
[runlim] sample:		3844.3 time, 1040.5 real, 2732.1 MB
[runlim] sample:		3883.9 time, 1050.5 real, 2764.5 MB
[runlim] sample:		3923.5 time, 1060.5 real, 2798.2 MB
[runlim] sample:		3963.2 time, 1070.5 real, 2661.2 MB
[runlim] sample:		4002.8 time, 1080.5 real, 2694.6 MB
[runlim] sample:		4042.4 time, 1090.5 real, 2718.8 MB
[runlim] sample:		4082.0 time, 1100.5 real, 2752.3 MB
[runlim] sample:		4121.6 time, 1110.5 real, 2789.2 MB
[runlim] end:			Sun Sep 20 16:25:59 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		2123
[runlim] real:			1117.30 seconds
[runlim] time:			4147.66 seconds
[runlim] space:			5177.3 MB
[runlim] samples:		11167
