Borodin–Kostochka Conjecture: for Δ ≥ 9, does no K_Δ force χ ≤ Δ − 1?

For a graph $G$ let $\Delta$ be the maximum degree, $\omega$ the clique number (largest complete subgraph), and $\chi$ the chromatic number. Borodin and Kostochka (1977) conjectured that **if $\Delta(G) \ge 9$ and $\omega(G) \le \Delta(G) - 1$, then $\chi(G) \le \Delta(G) - 1$** (equivalently $\chi \le \max\{\Delta-1, \omega\}$). The hypothesis $\Delta \ge 9$ is sharp: the strong product $C_5 \boxtimes K_3$ has $\Delta = 8$, $\omega = 6$, but $\chi = 8$. Decide the conjecture, or exhibit a counterexample. Computational sub-question: search for a graph with $\Delta = 9$, $\omega \le 8$, and $\chi \ge 9$ (which would refute it), or SAT-verify no such graph exists up to $n$ vertices.

Acceptance. FULLY RESOLVES: a graph $G$ with $\Delta(G) \ge 9$, a SAT/exhaustive certificate that $\omega(G) \le \Delta(G) - 1$, and a SAT UNSAT certificate that $G$ is not $(\Delta-1)$-colorable (so $\chi \ge \Delta$), refuting the conjecture; or a proof. PARTIAL PROGRESS: a SAT-backed verification that no counterexample with $\Delta = 9$ exists among graphs up to $n$ vertices (state the search space and encoding), or a proof for a new class. Provide the clique/coloring encodings and certificates.