I have the following experimental results on random regular graphs. I would like to know current theory on colorability of random regular graphs.

Almost all 5 regular graphs are 3 colorable.

Almost all 9 regular graphs are 4 colorable.

Almost all 13 regular graphs are 5 colorable.

These appear to be tight experimentally. Are they?

Exhibiting such colorings is difficult as the size of the graph grows, and I have trouble with degree 9 and 13. I am particularly interested in degree 9 graphs, as these 4 coloring problems produce very difficult 4-CNFs for satisfiability programs.

I am preparing a paper for Satisfiability 2017 on regular graph coloring, and would like references on known theory.