[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/beempgmprot1f2.aig
[runlim] start:			Sun Sep 20 12:20:22 2015
[runlim] main pid:		9561
[runlim] sample:		27.8 time, 10.3 real, 1238.1 MB
[runlim] sample:		67.4 time, 20.3 real, 1455.6 MB
[runlim] sample:		107.1 time, 30.3 real, 1618.2 MB
[runlim] sample:		146.7 time, 40.3 real, 1658.2 MB
[runlim] sample:		186.3 time, 50.3 real, 1689.8 MB
[runlim] sample:		179.5 time, 60.3 real, 1631.7 MB
[runlim] sample:		218.7 time, 70.3 real, 1675.7 MB
[runlim] sample:		257.0 time, 80.3 real, 1724.0 MB
[runlim] sample:		295.2 time, 90.3 real, 1753.8 MB
[runlim] sample:		334.8 time, 100.3 real, 1794.7 MB
[runlim] sample:		373.6 time, 110.3 real, 1826.9 MB
[runlim] sample:		413.3 time, 120.3 real, 1875.0 MB
[runlim] sample:		452.9 time, 130.3 real, 1933.6 MB
[runlim] sample:		492.0 time, 140.3 real, 2012.7 MB
[runlim] sample:		529.8 time, 150.3 real, 2095.0 MB
[runlim] sample:		569.4 time, 160.3 real, 2092.2 MB
[runlim] sample:		609.0 time, 170.3 real, 2107.6 MB
[runlim] sample:		648.6 time, 180.3 real, 2288.6 MB
[runlim] sample:		688.2 time, 190.3 real, 2337.3 MB
[runlim] sample:		724.8 time, 200.3 real, 2371.1 MB
[runlim] sample:		764.4 time, 210.3 real, 2389.8 MB
[runlim] sample:		802.3 time, 220.3 real, 2444.7 MB
[runlim] sample:		841.9 time, 230.3 real, 2483.5 MB
[runlim] sample:		880.6 time, 240.3 real, 2486.9 MB
[runlim] sample:		920.2 time, 250.3 real, 2545.8 MB
[runlim] sample:		959.8 time, 260.3 real, 2622.0 MB
[runlim] sample:		999.4 time, 270.3 real, 2633.8 MB
[runlim] sample:		1037.3 time, 280.3 real, 2707.0 MB
[runlim] sample:		1076.9 time, 290.3 real, 2746.4 MB
[runlim] sample:		1114.8 time, 300.3 real, 2754.3 MB
[runlim] sample:		1154.3 time, 310.3 real, 2810.8 MB
[runlim] sample:		1192.4 time, 320.3 real, 2879.6 MB
[runlim] sample:		1230.1 time, 330.3 real, 2895.8 MB
[runlim] sample:		1269.7 time, 340.3 real, 2940.0 MB
[runlim] sample:		1309.3 time, 350.3 real, 2981.9 MB
[runlim] sample:		1347.5 time, 360.3 real, 3005.4 MB
[runlim] sample:		1387.1 time, 370.3 real, 3065.2 MB
[runlim] sample:		1426.7 time, 380.3 real, 3065.8 MB
[runlim] sample:		1465.4 time, 390.3 real, 3148.3 MB
[runlim] sample:		1505.0 time, 400.3 real, 3220.2 MB
[runlim] sample:		1543.5 time, 410.3 real, 3261.1 MB
[runlim] sample:		1583.0 time, 420.3 real, 3397.7 MB
[runlim] sample:		1621.2 time, 430.3 real, 3418.1 MB
[runlim] sample:		1660.8 time, 440.3 real, 3480.6 MB
[runlim] sample:		1700.2 time, 450.3 real, 3527.2 MB
[runlim] sample:		1739.8 time, 460.3 real, 3504.9 MB
[runlim] sample:		1779.4 time, 470.3 real, 3542.1 MB
[runlim] sample:		1819.0 time, 480.3 real, 3585.3 MB
[runlim] sample:		1858.6 time, 490.3 real, 3599.6 MB
[runlim] sample:		1898.2 time, 500.3 real, 3625.7 MB
[runlim] sample:		1937.8 time, 510.3 real, 3634.8 MB
[runlim] sample:		1977.5 time, 520.3 real, 3733.9 MB
[runlim] sample:		2015.9 time, 530.3 real, 3754.2 MB
[runlim] sample:		2052.3 time, 540.3 real, 3756.6 MB
[runlim] sample:		2091.9 time, 550.3 real, 3835.2 MB
[runlim] sample:		2131.6 time, 560.3 real, 3885.7 MB
[runlim] sample:		2171.2 time, 570.3 real, 3850.1 MB
[runlim] sample:		2210.8 time, 580.3 real, 3905.8 MB
[runlim] sample:		2250.4 time, 590.3 real, 3940.8 MB
[runlim] sample:		2290.1 time, 600.3 real, 3993.1 MB
[runlim] sample:		2329.7 time, 610.3 real, 4196.1 MB
[runlim] sample:		2369.3 time, 620.3 real, 4330.2 MB
[runlim] sample:		2409.0 time, 630.3 real, 4387.9 MB
[runlim] sample:		2448.6 time, 640.3 real, 4540.6 MB
[runlim] sample:		2488.2 time, 650.3 real, 4674.9 MB
[runlim] sample:		2527.7 time, 660.3 real, 4689.2 MB
[runlim] sample:		2566.1 time, 670.3 real, 4806.8 MB
[runlim] sample:		2605.7 time, 680.3 real, 5074.1 MB
[runlim] sample:		2645.3 time, 690.3 real, 5126.9 MB
[runlim] sample:		2684.9 time, 700.3 real, 5156.6 MB
[runlim] sample:		2724.6 time, 710.3 real, 5295.0 MB
[runlim] sample:		2764.2 time, 720.3 real, 5372.7 MB
[runlim] sample:		2803.8 time, 730.3 real, 5628.6 MB
[runlim] sample:		2842.4 time, 740.3 real, 6019.1 MB
[runlim] sample:		2882.0 time, 750.3 real, 6086.8 MB
[runlim] sample:		2921.6 time, 760.3 real, 6120.1 MB
[runlim] sample:		2961.2 time, 770.3 real, 6192.6 MB
[runlim] sample:		3000.9 time, 780.3 real, 6273.1 MB
[runlim] sample:		3040.5 time, 790.3 real, 6355.6 MB
[runlim] sample:		3080.1 time, 800.3 real, 6394.1 MB
[runlim] sample:		3119.7 time, 810.3 real, 6458.4 MB
[runlim] sample:		3159.4 time, 820.3 real, 6494.4 MB
[runlim] sample:		3199.0 time, 830.3 real, 6522.8 MB
[runlim] sample:		3238.6 time, 840.3 real, 6559.1 MB
[runlim] sample:		3278.2 time, 850.3 real, 6609.1 MB
[runlim] sample:		3317.8 time, 860.3 real, 6717.4 MB
[runlim] sample:		3357.5 time, 870.3 real, 6700.8 MB
[runlim] sample:		3397.1 time, 880.3 real, 6810.8 MB
[runlim] sample:		3436.7 time, 890.3 real, 6780.2 MB
[runlim] end:			Sun Sep 20 12:35:19 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		589
[runlim] real:			897.51 seconds
[runlim] time:			3463.96 seconds
[runlim] space:			7002.9 MB
[runlim] samples:		8971
