Figure \[embed\_14\_8\_7\], rows (and columns) 16–23 detail one such coloring. Finally, there are 9 possible $(4,3,2;7)$ colorings which are subgraphs for the neighbors of $v_1$ in color 3. In Figure \[embed\_14\_8\_7\], rows (and columns) 24–30 detail one such coloring.

To summarize, Figure \[embed\_14\_8\_7\] is a partially instantiated adjacency matrix. The first row determines the degrees of $v_1$, in the three colors, and 3 corresponding subgraphs are embedded. The uninstantiated values in the matrix must be completed to obtain a solution that satisfies $\varphi_{4,3,3;30}(A)$ as specified in Constraint (\[constraint:coloring\]) of Figure \[fig:gcp\]. This can be determined using a SAT solver. For the specific example in Figure \[embed\_14\_8\_7\], the CNF generated using our tool set consists of 33[,]{}959 clauses, involves 5[,]{}318 Boolean variables, and is shown to be unsatisfiable in 52 seconds of computation time. For the case where $v_1$ has degrees ${\langle 14,8,7 \rangle}$ in the three colors this is one of $115\times 3\times 9 = 3105$ instances that need to be checked.

Table \[table:regular\] summarizes the experiment which proves Theorem \[thm:regular\]. For each of the possible degrees of vertex 1 in a $(4,3,3;30)$ coloring as prescribed by Corollary \[cor:degrees\], except ${\langle 13,8,8 \rangle}$, and for each possible choice of colorings 