d_1,d_2,d_3 \rangle}$ as prescribed by Corollary \[cor:degrees\]. For each possible triplet ${\langle d_1,d_2,d_3 \rangle}$, except ${\langle 13,8,8 \rangle}$, we take each of the known corresponding colorings for the subgraphs $G^1_{v_1}$, $G^2_{v_1}$, and $G^3_{v_1}$ and embed them into $A$. We then apply a SAT solver, to (try to) complete the remaining cells in $A$ to satisfy $\varphi_{4,3,3;30}(A)$ as defined by Constraint (\[constraint:coloring\]) of Figure \[fig:gcp\]. If the SAT solver fails, then no such completion exists.

To illustrate the approach, consider the case where $deg(v_1)={\langle 14,8,7 \rangle}$. Figure \[embed\_14\_8\_7\] details one of the embeddings corresponding to this case. The first row and column of $A$ specify the colors of the edges of the 29 neighbors of $v_1$ (in bold). The symbol “$\_$” indicates an integer variable that takes a value between 1 and 3. The neighbors of $v_1$ in color 1 form a submatrix of $A$ embedded in rows (and columns) 2–15 of the matrix in the Figure. By Corollary \[obs:embed\] these are a $(3,3,3;14)$ Ramsey coloring and there are 115 possible such colorings modulo weak isomorphism. The Figure details one of them. Similarly, there are 3 possible $(4,2,3;8)$ colorings which are subgraphs for the neighbors of $v_1$ in color 2. In 