I am trying to show that a certain family of graphs can always be properly coloured with at most $6$ colours (where "properly coloured" means that each vertex gets a colour and no edge has both ends the same colour).

I'll describe the construction of the family of graphs with a $20$-vertex example, but in general there can be $4k$ vertices.

Start with five vertex-disjoint $4$-cliques (i.e $5K_4$) which obviously creates a graph with chromatic number $4$. Now add (to the same vertex set) another "layer" of edges which also form five vertex-disjoint $4$-cliques, with no restriction on how the new cliques overlap the old cliques. The resulting graph will have vertices with degrees between 3 and 6 but, after some thought, it becomes apparent that it still has chromatic number $4$. Finally, add a *third* layer of edges, which also form five vertex-disjoint $4$-cliques. I'll call this collection of $15$ cliques the *defining cliques* to distinguish them from any new cliques that may be formed by combining edges from more than one defining clique.

If there are no restrictions on how the third set of cliques overlaps the others, then the entire graph can contain a $7$-clique. However if we add the restriction that no two vertices can belong to the same triple of defining cliques, then it is no longer possible to create $7$-cliques, and so it is conceivalbe that they can be coloured with $6$ colours. And this is the question:

**Do all of these graphs have proper $6$-colourings?**

I have searched by computer, probably exhaustively, on $20$ vertices and am convinced that there are no graphs of this structure that need $7$ colours. Finding one that *does* require $7$ colours would help to provide a combinatorial proof of some complicated result that I don't understand, and hence would be A Good Thing (and therefore by Murphy's Law, it won't exist). But for this purpose, it doesn't need to be $20$ vertices, but could instead be any graph on $4k$ vertices formed by the union of three layers with each layer being $k$ vertex-disjoint $4$-cliques, and so I'd like to rule out this avenue entirely, rather than always being tempted to run a few more cases.

There are quite a few known results on colouring graphs whose edge set is the union of cliques, but none that have this particular structure. The closest I came is a paper by Klotz who considered graphs whose edge set is the union of overlapping cliques, and gave bounds based on the sizes of the cliques and the maximum number of cliques in which each vertex lies, but his greater generality (the cliques don't have to occur in "layers") gives bounds that are too weak.

There are a handful of results about "equivalence subgraphs" which are defined to be disjoint unions of cliques covering the vertex set (i.e. the relationship graph of an equivalence relation), but the few results that I found are mostly about trying to partition graphs into equivalence subgraphs rather than colouring unions of equivalence subgraphs.

One can also rewrite the problem by noting that each vertex is uniquely defined by an ordered triple (i.e. 124 would mean that the vertex is in the first clique in Layer 1, the second clique in Layer 2 and the 4th clique in Layer 3) and so we have a set of 20 triples such that each symbol from 1 to 5 occurs exactly four times in each coordinate position. This doesn't seem to help (me).