[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/intel009.aig
[runlim] start:			Sun Sep 20 21:34:06 2015
[runlim] main pid:		9112
[runlim] sample:		9.4 time, 10.3 real, 187.7 MB
[runlim] sample:		19.4 time, 20.3 real, 187.7 MB
[runlim] sample:		29.4 time, 30.3 real, 187.7 MB
[runlim] sample:		39.4 time, 40.3 real, 207.3 MB
[runlim] sample:		49.4 time, 50.3 real, 204.4 MB
[runlim] sample:		59.4 time, 60.3 real, 204.7 MB
[runlim] sample:		69.4 time, 70.3 real, 204.7 MB
[runlim] sample:		79.4 time, 80.3 real, 204.7 MB
[runlim] sample:		89.3 time, 90.3 real, 207.0 MB
[runlim] sample:		99.3 time, 100.3 real, 201.5 MB
[runlim] sample:		109.3 time, 110.3 real, 201.5 MB
[runlim] sample:		135.6 time, 120.3 real, 1775.7 MB
[runlim] sample:		175.2 time, 130.3 real, 2027.5 MB
[runlim] sample:		214.8 time, 140.3 real, 2120.2 MB
[runlim] sample:		254.4 time, 150.3 real, 2296.6 MB
[runlim] sample:		294.0 time, 160.3 real, 2462.4 MB
[runlim] sample:		333.6 time, 170.3 real, 2491.6 MB
[runlim] sample:		373.2 time, 180.3 real, 2755.1 MB
[runlim] sample:		412.8 time, 190.3 real, 2704.3 MB
[runlim] sample:		452.4 time, 200.3 real, 2783.9 MB
[runlim] sample:		492.0 time, 210.3 real, 2928.8 MB
[runlim] sample:		531.6 time, 220.3 real, 2929.5 MB
[runlim] sample:		571.2 time, 230.3 real, 3068.9 MB
[runlim] sample:		610.8 time, 240.3 real, 3154.9 MB
[runlim] sample:		650.4 time, 250.3 real, 3243.0 MB
[runlim] sample:		690.0 time, 260.3 real, 3183.4 MB
[runlim] sample:		729.6 time, 270.3 real, 3332.3 MB
[runlim] sample:		769.2 time, 280.3 real, 3763.5 MB
[runlim] sample:		808.9 time, 290.3 real, 3790.2 MB
[runlim] sample:		848.5 time, 300.3 real, 3719.3 MB
[runlim] sample:		888.1 time, 310.3 real, 3824.9 MB
[runlim] sample:		927.7 time, 320.3 real, 3808.0 MB
[runlim] sample:		967.3 time, 330.3 real, 3792.4 MB
[runlim] sample:		1006.9 time, 340.3 real, 4006.7 MB
[runlim] sample:		1046.5 time, 350.3 real, 4022.8 MB
[runlim] sample:		1086.1 time, 360.3 real, 3945.9 MB
[runlim] sample:		1125.7 time, 370.3 real, 3968.5 MB
[runlim] sample:		1165.3 time, 380.3 real, 3931.6 MB
[runlim] sample:		1204.8 time, 390.3 real, 3834.5 MB
[runlim] sample:		1244.4 time, 400.3 real, 4110.4 MB
[runlim] sample:		1284.0 time, 410.3 real, 4059.0 MB
[runlim] sample:		1323.5 time, 420.3 real, 4016.3 MB
[runlim] sample:		1363.1 time, 430.3 real, 3970.5 MB
[runlim] sample:		1402.6 time, 440.3 real, 3927.7 MB
[runlim] sample:		1442.2 time, 450.3 real, 4080.1 MB
[runlim] sample:		1481.8 time, 460.3 real, 4041.2 MB
[runlim] sample:		1521.4 time, 470.3 real, 3925.2 MB
[runlim] sample:		1561.0 time, 480.3 real, 4216.2 MB
[runlim] sample:		1600.6 time, 490.3 real, 4070.9 MB
[runlim] sample:		1640.2 time, 500.3 real, 4072.0 MB
[runlim] sample:		1679.8 time, 510.3 real, 4083.1 MB
[runlim] sample:		1719.4 time, 520.3 real, 4085.0 MB
[runlim] sample:		1759.0 time, 530.3 real, 4185.7 MB
[runlim] sample:		1798.6 time, 540.3 real, 4090.8 MB
[runlim] sample:		1838.2 time, 550.3 real, 4300.3 MB
[runlim] sample:		1877.7 time, 560.3 real, 4308.3 MB
[runlim] sample:		1917.3 time, 570.3 real, 4154.6 MB
[runlim] sample:		1956.9 time, 580.3 real, 4114.4 MB
[runlim] sample:		1996.5 time, 590.3 real, 4120.1 MB
[runlim] sample:		2036.0 time, 600.3 real, 4149.4 MB
[runlim] sample:		2075.6 time, 610.3 real, 4161.0 MB
[runlim] sample:		2115.2 time, 620.3 real, 4455.5 MB
[runlim] sample:		2154.8 time, 630.3 real, 4411.8 MB
[runlim] sample:		2194.4 time, 640.3 real, 4591.8 MB
[runlim] sample:		2234.0 time, 650.3 real, 4668.0 MB
[runlim] sample:		2273.6 time, 660.3 real, 4530.3 MB
[runlim] sample:		2313.2 time, 670.3 real, 4669.8 MB
[runlim] sample:		2352.8 time, 680.3 real, 4773.6 MB
[runlim] sample:		2392.4 time, 690.3 real, 4848.0 MB
[runlim] sample:		2432.0 time, 700.3 real, 4848.1 MB
[runlim] sample:		2471.7 time, 710.3 real, 5059.3 MB
[runlim] sample:		2511.3 time, 720.3 real, 5034.7 MB
[runlim] sample:		2550.9 time, 730.3 real, 5237.7 MB
[runlim] sample:		2590.5 time, 740.3 real, 5299.5 MB
[runlim] sample:		2630.1 time, 750.3 real, 5351.2 MB
[runlim] sample:		2669.7 time, 760.3 real, 5517.6 MB
[runlim] sample:		2709.3 time, 770.3 real, 5569.4 MB
[runlim] sample:		2748.9 time, 780.3 real, 5727.3 MB
[runlim] sample:		2788.5 time, 790.3 real, 5810.5 MB
[runlim] sample:		2828.1 time, 800.3 real, 5818.8 MB
[runlim] sample:		2867.7 time, 810.3 real, 6005.9 MB
[runlim] sample:		2907.3 time, 820.3 real, 6135.7 MB
[runlim] sample:		2946.9 time, 830.3 real, 6135.5 MB
[runlim] sample:		2986.6 time, 840.3 real, 6231.8 MB
[runlim] sample:		3026.2 time, 850.3 real, 6409.3 MB
[runlim] sample:		3065.8 time, 860.3 real, 6533.1 MB
[runlim] sample:		3105.4 time, 870.3 real, 6543.2 MB
[runlim] sample:		3145.0 time, 880.3 real, 6414.9 MB
[runlim] sample:		3184.6 time, 890.3 real, 6468.6 MB
[runlim] sample:		3224.2 time, 900.3 real, 6546.5 MB
[runlim] sample:		3263.8 time, 910.3 real, 6961.6 MB
[runlim] end:			Sun Sep 20 21:49:17 2015
[runlim] status:		out of memory
[runlim] result:		3
[runlim] children:		8
[runlim] real:			911.80 seconds
[runlim] time:			3268.43 seconds
[runlim] space:			7002.1 MB
[runlim] samples:		9114
