we endow first order logic with counting quantifiers. The formula $\exists^{\geq i}x  \varphi(x)$ expresses then the fact that there are at least $i$ distinct elements that satisfy the formula $\varphi$. For example the formula $\exists^{\geq 3} x \exists^{\geq 4} y E(x,y)$ would express that the graph contains at least 3 vertices of degree at least 4. The logic $\mathbf{C}^{k}$ is the fragment of said logic which allows formulas to only use $k$ distinct variables (that can however be reused an arbitrary number of times). We refer to [@MR1060782] for a more thorough introduction to these logics and a proof that two graphs can be distinguished by $k$-dimensional WL exactly if there is a formula in $\mathbf{C}^{k+1}$ that holds on the one graph but not on the other. Often such logics are endowed with a fixed-point operator, but since we will only apply the formulas to structures of fixed size, this will not be necessary for us (see [@DBLP:books/cu/O2017] for more information).

The pebble game {#subsec:pebble:game:graphs}
---------------

There is a third concept, the bijective pebble game [@DBLP:journals/iandc/Hella96], that has a deeper connection to the logic $\mathbf{C}^{k+1}$ and the $k$-WL. This game is often used to show that graphs cannot be distinguished 