-all such graphs are shorter than $2k + 2k^2/2 = k(2k+1)$. Each element of the encoding
-is either a~vertex identifier or a~symbol, so it can attain at most $k+s$ possible values.
-We can therefore enumerate all possible encodings, convert them to the collection $\cal G$
-of all generic graphs and run the computation on them in time $\O(\vert{\cal G}\vert \cdot T(k))
-= \O((k+s)^{k(2k+1)}\cdot T(k))$.
-
-We then use the Unification lemma (\ref{uniflemma}) on the union of the collections
-$\C$ and~$\cal G$ to match the generic graphs with the equivalent graphs in~$\C$
+all such graphs are shorter than $2k + 2k^2/2 = k(k+2)$. Each element of the encoding
+is either a~vertex identifier, or a~symbol, or a~separator, so it can attain at most $k+s$
+possible values for some fixed~$s$.
+We can therefore enumerate all possible encodings, convert them to a~collection $\cal G$
+of all generic graphs and run the computation on all of them in time $\O(\vert{\cal G}\vert \cdot T(k))
+= \O((k+s)^{k(k+2)}\cdot T(k))$.
+
+Then we use the Unification lemma (\ref{uniflemma}) on the union of the collections
+$\C$ and~$\cal G$ to match the generic graphs with the equivalent actual graphs in~$\C$