Given a conflict graph $G = (V, E)$, a man has to transport a set $V$ of items/vertices across the river. Two items are connected by an edge in $E$, if they are conflicting and thus cannot be left alone together without human supervision. The available boat has capacity $b\geq 1$, and thus can carry the man together with any subset of at most $b$ items. A feasible schedule is a finite sequence of triples $(L_1, B_1, R_1),\dots, (L_s, B_s, R_s)$ of subsets of the item set V that satisfies the following conditions (FS1)–(FS3). The odd integer $s$ is called the length of the schedule.
(FS1) For every $k$, the sets $L_k, B_k, R_k$ form a partition of V . The sets $L_k$ and $R_k$ form stable sets in $G$. The set $B_k$ contains at most $b$ elements.
(FS2) The sequence starts with $L_1 \cup B_1 = V$ and $R_1 = \emptyset$, and the sequence ends with $L_s = \emptyset$ and $B_s\cup R_s = V$.
(FS3) For even $k \geq 2$, we have $B_k\cup R_k = B_{k-1} \cup R_{k-1}$ and $L_k = L_{k-1}$. For odd $k \geq3$, we have $L_k\cup B_k= L_{k-1}\cup B_{k-1}$ and $R_k = R_{k-1}$.
Known Result: $VertexCover(G) \geq b \geq VertexCover(G)+1$.
Please help formulate this problem in MSO.