can distinguish certain pairs of non-isomorphic graphs, but not all of them. A graph is said to have WL-dimension at most $k$, if $k$-WL distinguishes the graph from every non-isomorphic graph. For many important classes of graphs the WL-dimension has been shown to be bounded; examples include planar graphs [@DBLP:conf/stoc/Grohe00; @DBLP:journals/jacm/KieferPS19] for which even $3$ suffices and more generally classes defined by forbidden minors [@MR3729479]. On the other hand, Cai, Fürer and Immerman constructed an infinite family of graphs, for which the WL-dimension is linear in the number of vertices, and thus unbounded [@DBLP:journals/combinatorica/CaiFI92]. Higher dimensional versions of $k$-WL also appear in Babai’s breakthrough result putting graph-isomorphism in quasi-polynomial time [@DBLP:conf/stoc/Babai16].

There is a deep and well-understood connection between $k$-WL and the expressiveness in the logic $\mathbf{C}^{k+1}$, the extension of the $(k+1)$-variable fragment of first order logic on graphs with counting quantifiers [@DBLP:journals/combinatorica/CaiFI92]. For example, two graphs can be distinguished by $k$-WL exactly if there is a formula in $\mathbf{C}^{k+1}$ that distinguishes the graphs. Therefore, in some well-defined sense, the $k$-WL algorithm is universal in that it simultaneously checks all combinatorial properties in an input graph expressible in the aforementioned logic.

**Contribution.** The first aim of this paper is to 