for the derived subgraphs $G^1_{v_1}$, $G^2_{v_1}$, and $G^3_{v_1}$, we apply a SAT solver to show that the instance $\varphi_{(4,3,3;30)}(A)$ of Constraint (\[constraint:coloring\]) of Figure \[fig:gcp\] cannot be satisfied. The table details for each degree triple, the number of instances, their average size (number of clauses and Boolean variables), and the average and total times to show that the constraint is not satisfiable.

   $v_1$ degrees         \# clauses (avg.)    \# vars (avg.)   unsat (avg)    unsat (total) 
  --------------- ------ ------------------- ---------------- ------------- --------------- -------------
     (16,8,5)         54 = 2\*3\*9                32432           5279              51 sec.     0.77 hrs.
     (16,7,6)        270 = 2\*9\*15               32460           5233             420 sec.    31.50 hrs.
     (15,8,6)         90 = 2\*3\*15               33607           5450              93 sec.     2.32 hrs.
     (15,7,7)        162 = 2\*9\*9                33340           5326            1554 sec.    69.94 hrs.
     (14,8,7)       3105 = 115\*3\*9              34069           5324             294 sec.   253.40 hrs.

  : Proving that any $(4,3,3;30)$ Ramsey coloring is ${\langle 13,8,8 \rangle}$ regular (summary).[]{data-label="table:regular"}

All of the SAT instances described in the experiment summarized by Table \[table:regular\] are unsatisfiable. The solver reports “unsat”. To gain confidence in our implementation, we illustrate its application on a satisfiable instance: to find a, known to exist, $(4,3,3;29)$ coloring. This experiment involves some reverse engineering.

[r]{}[.460]{}

In 1966 Kalbfleisch [@kalb66] reported the existence of 