C$_2$MS model-checking algorithm for graphs of bounded rank-width

Let $G$ be a graph, let $\phi(\mathcal{X})$ be a C$_2$MS formula, and let $\alpha$ be an assignment to its free variables. Write $\operatorname{qr}(\phi)$ for the quantifier rank of $\phi$ and $\operatorname{rwd}(G)$ for the rank-width of $G$. Then there is a computable function $f$ such that the following holds. C$_2$MS rank-width conjecture. There exists an algorithm which decides whether

$$G\models\phi(\alpha(\mathcal{X}))$$

and whose running time is

$$\mathcal{O}\bigl(f(\operatorname{qr}(\phi),\operatorname{rwd}(G))\cdot |G|^3\bigr).$$

This would extend the known fixed-parameter model-checking bounds for monadic second-order logic on graphs of bounded clique-width to the counting extension C$_2$MS and rank-width. The conjecture is presented as an expected algorithmic extension, and its resolution is not established in the supplied text.