The formula of the paper. $θ_S(a, b)$ says that $a$ and $b$ have the same atomic type over $S$, with one quantifier. $e^±_S(a, b; x, y)$ says that $a$ and $b$ lie in opposite parts among the parts of $x$ and $y$ and are equal or adjacent, respectively non-adjacent. $ρ^±_S(x, y)$ says that there are $z₁, …, z₄$ such that every consecutive pair of $x, z₁, …, z₄, y$ satisfies $e^±_S$, and $φ_R = x ≠ y ∧ ρ⁺_S ∧ ρ⁻_S$. Such a chain is a walk of length $5$ between opposite copies of $x$ and $y$ in $G[X, Y]$, respectively Ḡ[X, Y]. Conversely, every walk of length at most $5$ between opposite copies has odd length and can be padded to length exactly $5$ by going back and forth along an edge. The pair relation is symmetric, as exchanging the two copies maps $G[X, Y]$ to $G[Y, X]$. The rank is $4 + 1 = 5$.

The paper's formula takes the disjunction over walks of length $1$, $3$ and $5$. The padding argument makes the walks of length $5$ suffice.