Function two_wl_pair_colors 

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

2-dimensional Weisfeiler–Leman (2-WL) of a formula’s variables — color refinement lifted from vertices to ordered pairs. Each pair (i,j) is colored: the diagonal by its 1-WL vertex color, an off-diagonal pair by (1-WL(i), 1-WL(j), co-occurrence signature) where the signature is the sorted multiset over clauses containing both of (clause width, sign of i, sign of j). Each round recolors (i,j) by (old color, sorted multiset over all k of (color(i,k), color(k,j))), to a fixpoint.

Strictly stronger than 1-WL (its diagonal refines the 1-WL coloring, and it sees pair structure 1-WL is blind to) and a SOUND over-approximation of the orbitals (orbits on ordered pairs): every variable automorphism preserves the pair coloring, so orbital(i,j) ⊆ paircell(i,j). Returns the n×n color matrix. O(rounds · n³), so intended for moderate n.