Suppose φ(x̄; ȳ) has the independence property on $C$. The left tuple is not empty, since otherwise all $aᵢ$ agree. By Shelah's reduction, carried out with Ramsey's theorem on finite shattered sequences, some formula $ψ(x; z̄)$ with a single left variable has the independence property, and so has its dual $ψ*(z̄; x)$. Then $ψ*(z̄; x) ∧ ψ*(z̄'; x)$ codes pairs: for tuples $aᵢ$ and $a_{n+j}$ the elements $b_{{k, n+l}}$ satisfy it exactly when $(i, j) = (k, l)$. Among all formulas coding on $C$, with any number of colors, take one of least total arity. If it has two left variables, then either $x$ extends by elements of a color $A$ to a tuple coding $z$ and no other element of a color $C$, which is a coding formula with a single left variable, or a spurious witness gives a coding formula with parameters and fewer left variables. By symmetry the minimal formula is $θ(x, y, z)$ in single variables. With a color $C₀$ for the codes $c_{i,J}$ with $i ∈ J$, the formula $∃z (C₀(z) ∧ θ(x, y, z))$ has the independence property. So $C$ is not monadically dependent.

The argument is carried out for the graph classes of the archive and mathlib formulas, and transferred to the graph classes used here and the translation of formulas.