[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/intel042.aig
[runlim] start:			Sun Sep 20 23:17:34 2015
[runlim] main pid:		12895
[runlim] sample:		9.5 time, 10.4 real, 226.1 MB
[runlim] sample:		19.5 time, 20.4 real, 228.4 MB
[runlim] sample:		29.5 time, 30.4 real, 228.9 MB
[runlim] sample:		39.5 time, 40.4 real, 252.5 MB
[runlim] sample:		49.5 time, 50.4 real, 249.0 MB
[runlim] sample:		59.5 time, 60.4 real, 235.6 MB
[runlim] sample:		69.5 time, 70.4 real, 235.6 MB
[runlim] sample:		79.5 time, 80.4 real, 231.4 MB
[runlim] sample:		89.5 time, 90.4 real, 238.6 MB
[runlim] sample:		99.5 time, 100.4 real, 228.4 MB
[runlim] sample:		109.5 time, 110.4 real, 228.4 MB
[runlim] sample:		119.4 time, 120.4 real, 238.7 MB
[runlim] sample:		134.5 time, 130.4 real, 1261.9 MB
[runlim] sample:		169.5 time, 140.4 real, 1732.3 MB
[runlim] sample:		207.3 time, 150.4 real, 2052.1 MB
[runlim] sample:		245.4 time, 160.4 real, 2315.8 MB
[runlim] sample:		279.8 time, 170.4 real, 2417.4 MB
[runlim] sample:		317.4 time, 180.4 real, 2552.0 MB
[runlim] sample:		354.2 time, 190.4 real, 2762.2 MB
[runlim] sample:		392.6 time, 200.4 real, 2760.3 MB
[runlim] sample:		432.2 time, 210.4 real, 2744.5 MB
[runlim] sample:		471.8 time, 220.4 real, 2896.1 MB
[runlim] sample:		511.3 time, 230.4 real, 2864.3 MB
[runlim] sample:		550.9 time, 240.4 real, 2853.8 MB
[runlim] sample:		590.5 time, 250.4 real, 2949.8 MB
[runlim] sample:		630.0 time, 260.4 real, 3078.8 MB
[runlim] sample:		669.6 time, 270.4 real, 3013.3 MB
[runlim] sample:		709.2 time, 280.4 real, 3041.4 MB
[runlim] sample:		748.8 time, 290.4 real, 3134.3 MB
[runlim] sample:		788.3 time, 300.4 real, 3021.5 MB
[runlim] sample:		827.9 time, 310.4 real, 3049.3 MB
[runlim] sample:		867.5 time, 320.4 real, 3038.9 MB
[runlim] sample:		907.0 time, 330.4 real, 2832.9 MB
[runlim] sample:		946.6 time, 340.4 real, 2895.4 MB
[runlim] sample:		986.2 time, 350.4 real, 2858.1 MB
[runlim] sample:		1025.7 time, 360.4 real, 2956.6 MB
[runlim] sample:		1065.2 time, 370.4 real, 2964.3 MB
[runlim] sample:		1104.8 time, 380.4 real, 2986.8 MB
[runlim] end:			Sun Sep 20 23:24:02 2015
[runlim] status:		ok
[runlim] result:		0
[runlim] children:		8
[runlim] real:			388.96 seconds
[runlim] time:			1137.03 seconds
[runlim] space:			3227.2 MB
[runlim] samples:		3885
