$j^{th}$ rows of $A$ (viewed as strings) omitting the elements at positions $i$ and $j$ (in both rows).

We omit the precise details of how Constraint (\[eq:symbreak\]) is encoded to CNF. In our implementation this is performed by the finite domain constraint compiler  and details can be found in [@jair2013]. Table \[tab:333n1\] illustrates the impact of the symmetry breaking Constraint (\[eq:symbreak\]) on the search for the Ramsey colorings required in the proof of Theorem \[thm:regular\].

The first four rows in the table portray the required instances of the forms $(4,3,2;n)$ and $(4,2,3;n)$ which by definition correspond to $(4,3;n)$ colorings (respectively in colors 1 and 3, and in colors 1 and 2). The next three rows correspond to $(3,3,3;n)$ colorings where $n\in\{14,15,16\}$. The last row illustrates our failed attempt to apply a SAT encoding to compute ${{\cal R}}(3,3,3;13)$. The first column in the table specifies the instance. The column headed by “\#${\setminus}_{\approx}$” specifies the known (except for the last row) number of colorings modulo weak isomorphism [@Rad]. The columns headed by “vars” and “clauses” indicate, the numbers of variables and clauses in the corresponding CNF encodings of the coloring problems with and without the symmetry breaking Constraint (\[eq:symbreak\]). The columns headed 