Function three_wl_colors 

pub fn three_wl_colors(
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> Vec<Vec<Vec<usize>>>

3-dimensional Weisfeiler–Leman (3-WL) of a formula’s variables — color refinement on ordered triples. A triple (i,j,k) is initialized by the 2-WL colors of its three pairs (pc[i][j], pc[i][k], pc[j][k]), then each round recolored by (old color, sorted multiset over all w of (color(w,j,k), color(i,w,k), color(i,j,w))) to a fixpoint. Returns the n×n×n color tensor.

Strictly stronger than 2-WL (it distinguishes graphs with identical 2-WL colorings — e.g. the rook’s graph from the Shrikhande graph) and a SOUND over-approximation of the 3-orbits (orbits on ordered triples): every automorphism preserves the coloring, so 3-orbit(i,j,k) ⊆ triplecell(i,j,k). O(rounds · n⁴), so for small n only.