Is the star chromatic index of every subcubic graph at most 6?

A *star edge coloring* is a proper edge coloring (incident edges get different colors) with the extra condition that no path or cycle on four edges is bicolored; equivalently, the union of any two color classes is a star forest. The *star chromatic index* $\chi'_s(G)$ is the least number of colors in a star edge coloring. Dvořák, Mohar & Šámal (2013) proved $\chi'_s(G) \le 7$ for every *subcubic* graph (maximum degree $\Delta \le 3$) and conjectured the truth is $\chi'_s(G) \le 6$. **Question: does there exist a subcubic graph with $\chi'_s = 7$?** Computational sub-question: for all (sub)cubic graphs up to $n$ vertices, compute $\chi'_s$ via a SAT/CP encoding and check none exceeds $6$.

Acceptance. FULLY RESOLVES: (a) a subcubic graph with a SAT-certified proof that $\chi'_s = 7$ (a UNSAT certificate that $6$ colors are infeasible plus a valid $7$-coloring) refutes the conjecture, or (b) a proof of the $\le 6$ bound. PARTIAL PROGRESS: an exhaustive check, using $\texttt{geng}$ to generate all connected cubic graphs up to $n$ vertices and a SAT encoding of the star-coloring constraints, that all satisfy $\chi'_s \le 6$, pushing $n$ beyond published computations. Provide the encoder and per-graph results.