# What is the smallest (in terms of vertices) 5-chromatic $K_5$-free graph?

I am looking for graphs that can be vertex-colored using at least 5 colors, but does not contain $K_5$ (a clique of size 5) as a sub-graph. The question is what is the smallest number of vertices a graph need to have in order to meet the desired properties?

By coloring I mean assignment of colors (numbers from 1 to 5) to vertices such that no adjacent vertices are assigned the same color.

The closest result I was able to find is "The size of a minimum five-chromatic K4-free graph" by Denis Hanson, Gary MacGillivray and Dale Youngs:

https://www.sciencedirect.com/science/article/pii/0012365X9390309H

We can certainly accomplish this with $7$ vertices: start with a $5$-cycle (a $3$-chromatic graph with no $K_3$) and add two more vertices adjacent to all others (and to each other), getting this graph.
The two added vertices must use a color not present anywhere else in the graph, and then we need $3$ more colors to color the $C_5$, so we need $5$ colors total. And there is no $K_5$, because a $K_5$ would need to contain three vertices of the cycle, but the cycle does not contain a $3$-clique.
It's clear that $5$ vertices are not enough: the only graph on $5$ vertices with chromatic number $5$ is $K_5$ itself.
If we had a $6$-vertex example, then it would need to have minimum degree $4$. Otherwise, we could delete a vertex with degree $3$, getting a $5$-vertex graph that's not $K_5$, color that with $4$ colors, and give the deleted vertex a color not used by its neighbors.
A $6$-vertex graph with minimum degree $4$ is a $K_6$ with a matching (not necessarily a perfect one) removed. If we remove just one edge, the result still contains a $K_5$; if we remove two independent edges, the result is already $4$-colorable, so we do not get a smaller example here either.