How to express a structure of a 5-colorable graph in logic
General ideas:


Require that each vertex ($\forall x \ldots$) satisfies at least one color predicate (Use $\lor$ among five color predicates).
Also require that no vertex ($\lnot\exists x \ldots$) has two distinct colors (you can enumerate all the ten distinct pairs: $\lnot({\sf red}(x)\land{\sf blue}(x))\land \lnot(\ldots)\land \cdots$).
For each color (repeat this axiom five times, once for each color), require that if $x$ has that color and $R(x,y)$ then $y$ has not that color (e.g. $\forall x y.\ {\sf red}(x)\land R(x,y) \implies \lnot{\sf red}(y)$).