[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/beemextnc1f1.aig
[runlim] start:			Sat Sep 19 20:51:02 2015
[runlim] main pid:		8236
[runlim] sample:		31.5 time, 10.3 real, 1037.9 MB
[runlim] sample:		71.2 time, 20.3 real, 1137.3 MB
[runlim] sample:		110.8 time, 30.3 real, 1233.5 MB
[runlim] sample:		150.4 time, 40.3 real, 1332.7 MB
[runlim] sample:		190.1 time, 50.3 real, 1414.2 MB
[runlim] sample:		229.7 time, 60.3 real, 1495.0 MB
[runlim] sample:		269.3 time, 70.3 real, 1587.9 MB
[runlim] sample:		308.9 time, 80.3 real, 1685.6 MB
[runlim] sample:		348.6 time, 90.3 real, 1757.8 MB
[runlim] sample:		388.2 time, 100.3 real, 1460.5 MB
[runlim] sample:		427.9 time, 110.3 real, 1542.7 MB
[runlim] sample:		467.5 time, 120.3 real, 1600.1 MB
[runlim] sample:		507.1 time, 130.3 real, 1677.6 MB
[runlim] sample:		546.8 time, 140.3 real, 1752.0 MB
[runlim] sample:		586.4 time, 150.3 real, 1778.0 MB
[runlim] sample:		626.0 time, 160.3 real, 1841.1 MB
[runlim] sample:		665.6 time, 170.3 real, 1926.1 MB
[runlim] sample:		705.3 time, 180.3 real, 1970.6 MB
[runlim] sample:		744.9 time, 190.3 real, 2041.1 MB
[runlim] sample:		784.5 time, 200.3 real, 2111.1 MB
[runlim] sample:		824.1 time, 210.3 real, 2167.8 MB
[runlim] sample:		863.8 time, 220.3 real, 2211.7 MB
[runlim] sample:		903.4 time, 230.3 real, 2269.6 MB
[runlim] sample:		943.0 time, 240.3 real, 2382.1 MB
[runlim] sample:		982.7 time, 250.3 real, 1680.2 MB
[runlim] sample:		1022.3 time, 260.3 real, 1747.4 MB
[runlim] sample:		1061.9 time, 270.3 real, 1843.0 MB
[runlim] sample:		1101.5 time, 280.3 real, 1889.8 MB
[runlim] sample:		1141.2 time, 290.3 real, 2002.0 MB
[runlim] sample:		1180.8 time, 300.3 real, 2062.0 MB
[runlim] sample:		1220.4 time, 310.3 real, 2190.0 MB
[runlim] sample:		1260.0 time, 320.3 real, 2264.0 MB
[runlim] sample:		1299.7 time, 330.3 real, 2329.5 MB
[runlim] sample:		1339.3 time, 340.3 real, 2368.9 MB
[runlim] sample:		1378.9 time, 350.3 real, 2437.4 MB
[runlim] sample:		1418.6 time, 360.3 real, 2496.3 MB
[runlim] sample:		1458.2 time, 370.3 real, 2551.3 MB
[runlim] sample:		1497.8 time, 380.3 real, 2618.1 MB
[runlim] sample:		1537.5 time, 390.3 real, 2670.7 MB
[runlim] sample:		1577.1 time, 400.3 real, 2717.9 MB
[runlim] sample:		1616.7 time, 410.3 real, 2076.6 MB
[runlim] sample:		1656.3 time, 420.3 real, 2135.3 MB
[runlim] sample:		1696.0 time, 430.3 real, 2198.2 MB
[runlim] sample:		1735.6 time, 440.3 real, 2265.3 MB
[runlim] sample:		1775.2 time, 450.3 real, 2322.1 MB
[runlim] sample:		1814.8 time, 460.3 real, 2432.2 MB
[runlim] sample:		1854.5 time, 470.3 real, 2495.1 MB
[runlim] sample:		1894.1 time, 480.3 real, 2509.6 MB
[runlim] sample:		1933.8 time, 490.3 real, 2566.7 MB
[runlim] sample:		1973.4 time, 500.3 real, 2635.9 MB
[runlim] sample:		2013.0 time, 510.3 real, 2696.2 MB
[runlim] sample:		2052.6 time, 520.3 real, 2748.7 MB
[runlim] sample:		2092.3 time, 530.3 real, 2799.7 MB
[runlim] sample:		2131.9 time, 540.3 real, 2854.4 MB
[runlim] sample:		2171.5 time, 550.3 real, 2902.6 MB
[runlim] sample:		2211.1 time, 560.3 real, 2969.5 MB
[runlim] sample:		2250.8 time, 570.3 real, 3014.7 MB
[runlim] sample:		2290.4 time, 580.3 real, 3085.8 MB
[runlim] sample:		2330.0 time, 590.3 real, 3320.5 MB
[runlim] sample:		2369.7 time, 600.3 real, 3365.2 MB
[runlim] sample:		2409.3 time, 610.3 real, 3394.4 MB
[runlim] sample:		2448.9 time, 620.3 real, 3542.4 MB
[runlim] sample:		2488.6 time, 630.3 real, 3581.9 MB
[runlim] sample:		2528.2 time, 640.3 real, 3626.7 MB
[runlim] sample:		2567.8 time, 650.3 real, 3661.1 MB
[runlim] sample:		2607.4 time, 660.3 real, 3704.3 MB
[runlim] sample:		2647.1 time, 670.3 real, 3733.6 MB
[runlim] sample:		2686.7 time, 680.3 real, 3785.9 MB
[runlim] sample:		2726.3 time, 690.3 real, 3876.4 MB
[runlim] sample:		2765.9 time, 700.3 real, 3916.8 MB
[runlim] sample:		2805.6 time, 710.3 real, 3967.4 MB
[runlim] sample:		2845.2 time, 720.3 real, 4012.0 MB
[runlim] sample:		2884.8 time, 730.3 real, 2661.5 MB
[runlim] sample:		2924.4 time, 740.3 real, 2717.3 MB
[runlim] sample:		2964.0 time, 750.3 real, 2798.6 MB
[runlim] sample:		3003.6 time, 760.3 real, 2873.0 MB
[runlim] sample:		3043.3 time, 770.3 real, 2957.3 MB
[runlim] sample:		3082.9 time, 780.3 real, 3037.8 MB
[runlim] sample:		3122.5 time, 790.3 real, 3098.1 MB
[runlim] sample:		3162.1 time, 800.3 real, 3166.7 MB
[runlim] sample:		3201.8 time, 810.3 real, 3239.7 MB
[runlim] sample:		3241.4 time, 820.3 real, 3304.0 MB
[runlim] sample:		3281.0 time, 830.3 real, 3374.0 MB
[runlim] sample:		3320.6 time, 840.3 real, 3462.5 MB
[runlim] sample:		3360.2 time, 850.3 real, 3534.9 MB
[runlim] sample:		3399.9 time, 860.3 real, 3593.5 MB
[runlim] sample:		3439.5 time, 870.3 real, 3650.8 MB
[runlim] sample:		3479.1 time, 880.3 real, 3701.0 MB
[runlim] sample:		3518.8 time, 890.3 real, 3787.6 MB
[runlim] sample:		3558.4 time, 900.3 real, 3851.9 MB
[runlim] sample:		3598.0 time, 910.3 real, 3910.1 MB
[runlim] sample:		3637.6 time, 920.3 real, 3968.6 MB
[runlim] sample:		3677.2 time, 930.3 real, 4026.9 MB
[runlim] sample:		3716.8 time, 940.3 real, 4095.1 MB
[runlim] sample:		3756.5 time, 950.3 real, 4163.6 MB
[runlim] sample:		3796.1 time, 960.3 real, 4191.2 MB
[runlim] sample:		3835.7 time, 970.3 real, 4257.2 MB
[runlim] sample:		3875.3 time, 980.3 real, 4335.6 MB
[runlim] sample:		3914.9 time, 990.3 real, 3247.7 MB
[runlim] sample:		3954.6 time, 1000.3 real, 3350.0 MB
[runlim] sample:		3994.2 time, 1010.3 real, 3472.8 MB
[runlim] sample:		4033.8 time, 1020.3 real, 3550.9 MB
[runlim] sample:		4073.4 time, 1030.3 real, 3632.8 MB
[runlim] sample:		4113.0 time, 1040.3 real, 3693.2 MB
[runlim] sample:		4152.6 time, 1050.3 real, 3777.5 MB
[runlim] sample:		4192.3 time, 1060.3 real, 3850.3 MB
[runlim] sample:		4231.9 time, 1070.3 real, 3924.9 MB
[runlim] sample:		4271.5 time, 1080.3 real, 4003.2 MB
[runlim] sample:		4311.1 time, 1090.3 real, 4083.2 MB
[runlim] sample:		4350.8 time, 1100.3 real, 4136.1 MB
[runlim] sample:		4390.4 time, 1110.3 real, 4092.6 MB
[runlim] sample:		4430.0 time, 1120.3 real, 4173.3 MB
[runlim] sample:		4469.6 time, 1130.3 real, 4256.3 MB
[runlim] sample:		4509.3 time, 1140.3 real, 4336.8 MB
[runlim] sample:		4548.9 time, 1150.3 real, 4411.2 MB
[runlim] sample:		4588.5 time, 1160.3 real, 4474.3 MB
[runlim] sample:		4628.1 time, 1170.3 real, 4537.0 MB
[runlim] sample:		4667.8 time, 1180.3 real, 4597.1 MB
[runlim] sample:		4707.4 time, 1190.3 real, 4705.7 MB
[runlim] sample:		4747.0 time, 1200.3 real, 4776.1 MB
[runlim] sample:		4786.6 time, 1210.3 real, 4899.0 MB
[runlim] sample:		4826.2 time, 1220.3 real, 4051.6 MB
[runlim] sample:		4865.8 time, 1230.3 real, 4123.7 MB
[runlim] sample:		4905.4 time, 1240.3 real, 4195.2 MB
[runlim] sample:		4945.0 time, 1250.3 real, 4276.4 MB
[runlim] sample:		4984.6 time, 1260.3 real, 4362.9 MB
[runlim] sample:		5024.3 time, 1270.3 real, 4442.1 MB
[runlim] sample:		5063.9 time, 1280.3 real, 4508.5 MB
[runlim] sample:		5103.5 time, 1290.3 real, 4586.7 MB
[runlim] sample:		5143.1 time, 1300.3 real, 4660.2 MB
[runlim] sample:		5182.7 time, 1310.3 real, 4722.9 MB
[runlim] sample:		5222.3 time, 1320.3 real, 4756.9 MB
[runlim] sample:		5261.9 time, 1330.3 real, 4830.4 MB
[runlim] sample:		5301.6 time, 1340.3 real, 4912.9 MB
[runlim] sample:		5341.2 time, 1350.3 real, 4997.6 MB
[runlim] sample:		5380.8 time, 1360.3 real, 5090.4 MB
[runlim] sample:		5420.4 time, 1370.3 real, 5184.7 MB
[runlim] sample:		5460.0 time, 1380.3 real, 5263.7 MB
[runlim] sample:		5499.6 time, 1390.3 real, 5343.9 MB
[runlim] sample:		5539.2 time, 1400.3 real, 5428.5 MB
[runlim] sample:		5578.9 time, 1410.3 real, 5514.9 MB
[runlim] sample:		5618.5 time, 1420.3 real, 5607.9 MB
[runlim] sample:		5658.1 time, 1430.3 real, 5692.5 MB
[runlim] sample:		5697.7 time, 1440.3 real, 5742.2 MB
[runlim] sample:		5737.4 time, 1450.3 real, 5814.5 MB
[runlim] sample:		5777.0 time, 1460.3 real, 5891.1 MB
[runlim] sample:		5816.6 time, 1470.3 real, 5951.2 MB
[runlim] sample:		5856.2 time, 1480.3 real, 6036.3 MB
[runlim] sample:		5895.8 time, 1490.3 real, 6101.0 MB
[runlim] sample:		5935.4 time, 1500.3 real, 6163.7 MB
[runlim] sample:		5975.0 time, 1510.3 real, 6212.3 MB
[runlim] sample:		6014.6 time, 1520.3 real, 6270.8 MB
[runlim] sample:		6054.3 time, 1530.3 real, 6335.7 MB
[runlim] sample:		6093.9 time, 1540.3 real, 6384.2 MB
[runlim] sample:		6133.5 time, 1550.3 real, 6446.4 MB
[runlim] sample:		6173.1 time, 1560.3 real, 6509.1 MB
[runlim] sample:		6212.7 time, 1570.3 real, 6568.2 MB
[runlim] sample:		6252.3 time, 1580.3 real, 6642.8 MB
[runlim] sample:		6291.9 time, 1590.3 real, 6715.1 MB
[runlim] sample:		6331.5 time, 1600.3 real, 6783.8 MB
[runlim] sample:		6371.1 time, 1610.3 real, 6846.2 MB
[runlim] sample:		6410.7 time, 1620.3 real, 6900.7 MB
[runlim] sample:		6450.4 time, 1630.3 real, 6957.9 MB
[runlim] end:			Sat Sep 19 21:18:21 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		28
[runlim] real:			1639.04 seconds
[runlim] time:			6483.95 seconds
[runlim] space:			7000.2 MB
[runlim] samples:		16387
