\section{Introduction}
It is known that RRA cannot be axiomatised by any finite theory \cite{Mon64} nor by any equational theory using only finitely many variables \cite[theorem~3.5.6]{Jon88}.  Moreover, any axiomatisation of RRA must involve infinitely many non-canonical equations \cite{HVCan}. To prove that RRA cannot be axiomatised by any $c$-variable   theory would yield the first two of these results as corollaries and would significantly strengthen what is known. Although the problem remains open, some progress is made here.  Our main new result is that there can be no axiomatisation of RRA of bounded quantifier depth.

This paper arises, partly,  from a difficulty with \cite[problem 1, page 625]{HH:book}.  The problem is to prove that RRA cannot be axiomatised by any $c$-variable first-order theory for finite $c$.  As mentioned above, the problem remains open. The problem statement in the book includes a proposed solution.  The proposal, which is mentioned in \cite[p491]{S-A05}, is to find graphs $G$ and $H$ with no homomorphism from $G$ to $H$, but indistinguishable in a certain $c$-colour graph game.   It is claimed that such graphs could be used to prove that there is is no $c$-variable axiomatisation of RRA.    Readers of the book, who failed to solve the problem, cannot be rebuked  since there was a  flaw in the proposed solution. Fortunately, by noticing the problem and attempting to correct it, we are led to a modification of the rainbow construction, and this modification leads not only to a correction for \cite[problem 1, page 625]{HH:book}, but also to the proof of the main result here.

Those who are not familiar with the open problem, the rainbow construction and the flaw in the suggestion from \cite{HH:book} may prefer to jump ahead to our main result, theorem~\ref{thm:main}, whose proof occupies most of the paper. The paper is structures as follows. In section \ref{S:rainbow} we introduce the modified rainbow construction over pairs of binary relational structures, and prove a theorem relating a certain property of these structures to complete representability of the construction. As a corollary to this we obtain the result that classes of atom structures intermediate between those of completely representable and representable relation algebras cannot be axiomatized using only finitely many variables (see corollary \ref{C:atoms}). In section \ref{S:game} we define the vertex colouring games, building up to a proof of theorem~\ref{thm:main}. Section \ref{S:correction} corrects the proposal from \cite{HH:book}. In the special case of graphs, these games are connected to the famous reconstruction conjecture (see e.g. \cite{Stock88,Bon91,LauSca16} for surveys), and are discussed in more detail in \cite{EgrHirgames}.  For the rest of the introduction we briefly discuss the rainbow construction, how it was hoped it could help solve the open problem of the existence of finite variable axiomatisations for RRA, the flaw in the argument, and the modifications to the construction needed for our new results here.

Suppose we can find graphs $G, H$, with no homomorphism from $G$ to $H$, that are indistinguishable in a certain colouring game using $c$ colours (call them \emph{$c$-indistinguishable} for short).  The problem statement uses a `rainbow relation algebra' $\c A_{G, H}$ built from the two graphs.  It can be shown that $\c A_{H, H}$ is representable but $\c A_{G, H}$ is not (see \cite[theorem 16.5]{HH:book}).  It is claimed in the problem statement that, since $G, H$ are $c$-indistinguishable, it follows that $\c A_{H, H}$ and $\c A_{G, H}$ could not be distinguished by any $c$-variable formula (i.e. that $\c A_{G, F}\equiv^c \c A_{H, F}$).  Unfortunately, that implication is false.  The problem is that  there are white atoms ${\sf w}_S\in\c A_{G,H}$ for every set of $G$-nodes $S$ of size at most two, which would be represented by binary predicates over graph nodes, but only monadic predicates are used in the graph colouring game.  Thus the proof cannot be completed.

To fix that, the idea is to  let $\c B_{G, H}$ be obtained from $\c A_{G, H}$ by deleting all white atoms ${\sf w}_S$ (and deleting any forbidden triple involving these deleted atoms).  This solves one problem, because now it is true that  if $G$ and $H$ are $c$-indistinguishable  then it can be shown  $\c B_{G, F}\equiv^c \c B_{H, F}$.  But it creates another, since $\exists$ really needed atoms ${\sf w}_S$ in her { winning strategy}\ for the representation game over $\c A_{H, H}$, so we can no longer be sure that $\c B_{H, H}$ is representable.  However, if it happens that every partial homomorphism from $H$ to $H$ of size  two extends to a homomorphism, then  it can be shown that $\c B_{H, H}$ is representable. This property is satisfied by complete graphs, for example, and we use this in the proof of theorem~\ref{thm:main}.

\medskip
We now give a formal statement of our main result.
\begin{theorem}\label{thm:main}
If $\Sigma$ is a set of first-order formulas defining RRA, then $\Sigma$ includes formulas of arbitrary quantifier depth.
\end{theorem}
The proof is developed in the next two sections.

\section{The modified rainbow construction}\label{S:rainbow}
Let $G, H$ be structures in a signature consisting of only binary predicates, which we refer to as \emph{binary structures}.  For most purposes we can assume $G$ and $H$ to be directed graphs, but it will be convenient at one point later to be able to force graph homomorphisms to preserve non-edges, and so we phrase our results here in terms of binary structures so we can formally handle this without issue.

Given two binary structures $G$ and $ H$, we define an atomic relation algebra $\c B_{G, H}$ by defining its atom structure.    A partial homomorphism is a partial map $h$ from $G$ to $H$ such that if $i\neq i'\in G$ and $(i, i')$ belongs to a binary predicate interpreted in $G$ then $(h(i), h(i'))$ also belongs to that predicate interpreted in $H$.
The atoms are
\[ \set{1', \bb, {\sf w}, {\sf y}}\cup\set{ {\sf g}_i,: i\in G}\cup\set{ {\sf r}_{j,j'}:    j, j'\in H}\]
The non-identity atoms are considered to be black, white, yellow, green or red.
All atoms are self-converse, except ${\sf r}_{j,j'}^\smile = {\sf r}_{j',j}$.
Forbidden triples of atoms are Peircean transforms of
\begin{enumerate}
\renewcommand{\theenumi}{\Roman{enumi}}
\item $(1', a, b)$ where $a\neq b$\label{f:1}
\item $({\sf g}_i, {\sf g}_{i'}, {\sf g}_{i''}), ({\sf g}_i, {\sf g}_{i'}, {\sf w})$, any $i, i', i''\in G$\label{f:nog}
\item $({\sf y}, {\sf y}, {\sf y}), ({\sf y}, {\sf y}, \bb)$\label{f:noy}
\item $({\sf r}_{j_1, j_2}, {\sf r}_{j_2', j_3'} , {\sf r}_{j_1^*, j_3^*})$, unless $j_1=j_1^*, \; j_2=j_2',\;j_3'=j_3^*$\label{f:red}.
\item \label{f:pim} $({\sf g}_i, {\sf g}_{i'}, {\sf r}_{j, j'})$ unless $\set{(i, i'), (j, j')}$ is a partial homomorphism.
\item \label{f:ii} $({\sf g}_i, {\sf g}_i, {\sf r}_{j, j'})$ any  $j,  j\in H'$.

\end{enumerate}
Observe for later that the only combinations of three colours where some but not all triples of atoms with those colours are forbidden are  green-green-red and red-red-red, see \eqref{f:red}, \eqref{f:pim} and \eqref{f:ii}.

  The relation algebra $\c B_{G, H}$ is the complex algebra of this atom structure. Note that here a triple $(a,b,c)$ being forbidden corresponds to setting $(a\comp b)\cdot c = 0$ in the complex algebra. This is slightly different from the approach taken in \cite{HH:book}, but the differences are entirely superficial.

To build complete representations for these algebras, we will employ a game played by two players, $\forall$ and $\exists$, over a kind of labeled complete digraph. We describe this game now, basing our exposition on the material in \cite[section~11]{HH:book}. An \emph{atomic network} $N$ for an atomic relation algebra $\c A$ consists of a  set of nodes (denoted ${\sf nodes}(N)$) and a map (also denoted $N$) from pairs of nodes to atoms of $\c A$, such that
$N(x, x)\leq 1', \;
N(y, x)= N(x, y)^\smile$ and $(N(x, y), N(y, z), N(x, z))$ is not forbidden, for all $x, y, z\in {\sf nodes}(N)$. This property of not containing edge labels forming a forbidden triple $(N(x, y), N(y, z), N(x, z))$ is often referred to as the \emph{consistency} of $N$. For atomic networks $M, N$ we write $M\subseteq N$ if ${\sf nodes}(M)\subseteq {\sf nodes}(N)$ and for all $x, y\in{\sf nodes}(M)$ we have $N(x, y)=M(x, y)$.    If $N_i:i<\lambda$ is a sequence of atomic networks where $i<j\rightarrow N_i\subseteq N_j$ then the \emph{limit} $N=\bigcup_{i<\lambda}N_i$ is the atomic network with nodes $\bigcup_{i<\lambda}{\sf nodes}(N_i)$ and where $N(x, y)=N_i(x, y)$ where $x, y\in{\sf nodes}(N_i)$ (and this label does not depend on $i$, since the sequence is nested).

Given an atomic relation algebra $\c A$, the complete representation game for
$\c A$ has $\min(\omega,|\c A|)$ rounds. $\exists$ is trying to build an atomic network for $\c A$, and $\forall$ is trying to force a situation where this is impossible. In a play of this game, let the current atomic network be $N$. Then  $\forall$ picks nodes $x, y\in{\sf nodes}(N)$ and atoms $\alpha, \beta$ such that $(\alpha, \beta, N(x, y))$ is not forbidden. In response, $\exists$ is required to extend $N$ to $N'$ such that there is a node $z\in{\sf nodes}(N)'$ where $N(x, z)=\alpha,\;N(z, y)=\beta$. The difficulty is that she must label all new edges induced by adding $z$ without causing the resulting network to be inconsistent. In other words, without creating any triangles corresponding to forbidden triples (we also call these \emph{forbidden triangles}).  We can assume that no suitable witness $z$ is already in $N$, else the move is trivial as $\exists$ does not need to add any extra nodes to the network. If $\forall$ has no non-trivial move to make then $\exists$ wins, as the network now reveals the required complete representation.   This is how $N'$ is obtained from $N$ at rounds indexed by successor ordinals.    At a round indexed by a limit ordinal the network is simply the limit of all the previous networks, which is well defined since the networks are nested.  The game starts with $\forall$ playing a non-identity atom $\alpha$, and $\exists$ creating a two node network $\{x_0,y_0\}$ such that the edge $(x_0,y_0)$ is labeled by $\alpha$. We say $\forall$ wins if in some round before $\min(\omega,|\c A|)$ he makes a move such that $\exists$ cannot extend the network consistently, and we say $\exists$ wins if she survives $\min(\omega,|\c A|)$ rounds, or if $\forall$ cannot make a non-trivial move at some point. We say $\exists$ has a { winning strategy}\ if she can play so that her victory is guaranteed. The key result, as proved in \cite[theorem 11.7]{HH:book} in the countable case, and discussed in \cite[exercise 11.4.3]{HH:book} for higher cardinalities, is that $\c A$  is completely representable if and only if $\exists$ has a winning strategy in the complete representation game over $\c A$.

 We return now to the relation algebra $\c B_{G, H}$ defined above.  Given an atomic  network $N$ for $\c B_{G, H}$ and nodes $x, y\in{\sf nodes}(N)$ let
\[R_N(x, y)=\set{z\in{\sf nodes}(N): N(x, z)\mbox{ is green and } N(y, z)={\sf y}}.\]
Observe that $R_N(x, y)$ depends only on the green and yellow edge labels of $N$.
  A set of nodes of a network where every edge  between distinct nodes has a  red label is called a red clique.  For any $x, y$, by forbidden triples \eqref{f:nog} and \eqref{f:noy}, $R_N(x, y)$ is a red clique.  In a red clique $C$ of size at least two,   by forbidden triple \eqref{f:red}, each node $z\in C$ has a well-defined index $\rho_C(z)\in H$ such that $N(z_1, z_2)={\sf r}_{\rho_C(z_1), \rho_C(z_2)}$, for $z_1\neq z_2\in C$.    So $\rho_C$ is defined on $z\in R_N(x,y)$ by  taking the first  subscript in the label of  $(z, z')$ where $z'\in R_N(x, y)\setminus\set{z}$ is arbitrary. By rule \eqref{f:red}, this subscript does not depend on choice of $z'$.  By consistency of $N$ and \eqref{f:ii}, for each $i\in G$ there can be at most one node $z$ such that $z\in R_N(x, y)$ and $N(x, z)={\sf g}_i$.

 Similarly, if $\theta$ is a complete representation of $\c B_{G,H}$ over base $X$, then for $x, y\in X$, let
 \[ R_\theta(x,y)=\set{z\in X: (x,z)\in\bigcup_{i\in G}{\sf g}_i^\theta\wedge (z, y)\in{\sf y}^\theta}.\]
  As with networks, if $|R_\theta(x, y)|>1$, then each point $z\in R_\theta(x, y)$  has an index $\rho_{(\theta, x, y)}(z)\in H$. This is defined by noticing that if $z_1\neq z_2 \in R_\theta(x, y)$, then $(z_1,z_2)\in {\sf g}_i^\theta\comp {\sf g}_{i'}^\theta\;\cap\;{\sf y}^\theta;{\sf y}^\theta$ for some $i,i'\in G$. As $\theta$ is a complete representation, there is an atom $\alpha$ with $(z_1,z_2)\in \alpha^\theta$  (see \cite[theorem 2.21]{HH:book}) and from the forbidden triple rules we see that $\alpha$ must be ${\sf r}_{j,j'}$ for some $j,j'\in H$. We define $\rho_{(\theta, x, y)}(z_1)$ to be $j$, which does not depend on the choice of $z_2\in R_\theta(x, y)\setminus\set{z_1}$.

\begin{theorem} \label{thm:rainbow}
Let $G, H$ be binary structures.
The following are equivalent.
\begin{enumerate}
\item  For all $i\neq i'\in G$ there are $j, j'\in H$ such that $\set{(i, i'), (j, j')}$ is a partial homomorphism

, and every partial homomorphism  $\set{(i, j), (i', j')}$ where $i\neq i'$  from a substructure of $G$ into $H$ extends to  a homomorphism $G\rightarrow H$.
\item $\c B_{G, H}$ is completely representable.
\end{enumerate}
\end{theorem}

\begin{proof}

Suppose $\c B_{G, H}$ is  completely representable, say $\theta$ is a complete representation.  Since $\theta$ is complete, for every pair of points $(x, y)\in 1^\theta$ in the base of the representation there is a unique atom $\alpha$ such that $(x, y)\in\alpha^\theta$ (by \cite[theorem 2.21]{HH:book}).

Let $i_1\neq i_2\in G$.
   Find points $x, y$ in the base of the representation such that $(x, y)\in{\sf w}^\theta$, see  the first part of figure~\ref{fig}.  Since $({\sf g}_{i_t},{\sf y},{\sf w})$ is not forbidden (for $t=1,2$), there are points $z_{1}, z_{2}$ such that $(x, z_{t})\in{\sf g}_{i_t}^\theta$ and $(z_{t}, y)\in{\sf y}^\theta$, for $t=1,2$.  The unique atom that holds on $(z_{1}, z_{2})$ cannot be the identity by forbidden triple \eqref{f:1}, nor green, white, yellow or black, by forbidden triples \eqref{f:nog}, \eqref{f:noy}, hence it must be red, say ${\sf r}_{j_1,j_2}$. We also have $(z_1,z_2)\in {\sf g}_{i_1}^\theta\comp {\sf g}_{i_2}^\theta$, and so, by forbidden triple \eqref{f:pim}, the map $\set{(i_1,j_1),(i_2,j_2)}$ is a partial homomorphism of size two.

To show that partial homomorphisms of size two extend,  let  $\set{(i_1, j_1), (i_2, j_2)}$  be a partial homomorphism from $G$ to $H$, where $i_1\neq i_2$.
Let $z_{i_1}, z_{i_2}$ be distinct points in the base of the representation such that $(z_{i_1}, z_{i_2})\in {\sf r}_{j_1, j_2}^\theta$ (see  the second part of figure~\ref{fig}).  Since $\set{(i_1,j_1),(i_2,j_2)}$ is a partial homomorphism it follows from rule \eqref{f:pim} that $({\sf g}_{i_1}, {\sf g}_{i_2}, {\sf r}_{j_1, j_2})$ is not forbidden, so there is a point $x$ where $(x, z_{i_1})\in{\sf g}_{i_1}^\theta$ and $(x, z_{i_2})\in {\sf g}_{i_2}^\theta$.  Also, $({\sf y}, {\sf y}, {\sf r}_{j_1, j_2})$ is not forbidden, so there is a point $y$ where $(y, z_{i_1}), (y, z_{i_2})\in{\sf y}^\theta$, and clearly $x\neq y$.  Since the representation is complete, there must be an atom $\alpha$ such that $(x, y)\in\alpha^\theta$ (by \cite[theorem 2.21]{HH:book}), and as $x\neq y$ this atom cannot be $1'$ (by rule \eqref{f:1}).

We have shown that $z_{i_1}\neq z_{i_2}\in R_\theta(x, y)$.  Write $\rho$ for $\rho_{(\theta, x, y)}$, so for $w\in R_\theta(x, y)$, $\rho(w)$ denotes the index of $w$ in $H$, and for $w, w'\in R_\theta(x, y)$ we have $(w, w')\in{\sf r}_{\rho(w), \rho(w')}^\theta$.    Since $(z_{i_1}, z_{i_2})\in{\sf r}_{j_1, j_2}^\theta$,
we have $\rho(z_{i_1})=j_1,\;\rho(z_{i_2})=j_2$.

Regardless of which non-identity atom $\alpha$ is, for each node $i$ of $G\setminus\set{i_1,i_2}$, the triple $({\sf g}_{i}, {\sf y}, \alpha)$ is not forbidden, from which it follows that $(x,y)\in {\sf g}_i\comp {\sf y}$, and so there must be a point $z\in R_\theta(x, y)$ where $(x, z)\in g_{i}^\theta$ and $(z, y)\in{\sf y}^\theta$.   This point is unique, as if $z'$ is a point with the same properties, then we have $(z,z')\in ({\sf g}_i^\theta\comp {\sf g}_i^\theta)\cap ({\sf y}^\theta\comp {\sf y}^\theta)$. As $\theta$ is complete, $(z,z')$ is contained in the interpretation of some atom, and the forbidden triple rules imply that this atom must be the identity. Thus $z=z'$, by definition of the identity in proper relation algebras. The map from $G$ to $H$  that sends $i\in G$ to $\rho(z_i)$ is therefore well defined,
is a homomorphism, by \eqref{f:pim}, and extends $\set{(i_1,j_1), (i_2,j_2)}$ as required.

\begin{figure}
\[
\xymatrix@!=2.5pc{
z_1\ar@{-}[rd]|-(.3){{\sf y}}\ar@{-->}[r]^{{\sf r}_{j_1, j_2}}&z_2\ar@{-}[d]^{{\sf y}}\\
x\ar@{-}[r]_{{\sf w}}\ar@{-}[u]^{{\sf g}_{i_1}}\ar@{-}[ur]|-(.4){{\sf g}_{i_2}}&y
}\hspace{.5in}
\xymatrix@!=2.5pc{
z_{i_1}\ar@{-}[rd]|-(.3){{\sf y}}\ar@{--}@{->}[r]^{{\sf r}_{j_1, j_2}}\ar@{-->}@/^2pc/ [rr]^{{\sf r}_{j_1,j}}&z_{i_2}\ar@{-}[d]^(.6){{\sf y}}\ar@{-->}[r]^{{\sf r}_{j_2,j}}&z_i\\
x\ar@{--}[r]_{\alpha}  \ar@{-}[u]^{{\sf g}_{i_1}}\ar@{-}[ur]|-(.4){{\sf g}_{i_2}}\ar@{-}[rru]|-(.25){{\sf g}_{i}}&y\ar@{-}[ru]_{{\sf y}}&
}
\]
\caption{\label{fig}From the  representation, a partial homomorphism $\set{(i_1, j_1), (i_2, j_2)}$ exists and extends to $i$.}
\end{figure}

\medskip

Now we check the converse.  Assume the first condition in the theorem. As discussed above, it is sufficient to show she has a { winning strategy}\ in the complete representation game for $\c B_{G,H}$.  The basic idea behind $\exists$'s strategy is that she will, as far as possible, use labels which obviously do not interfere with the integrity of the network, and never any labels that are not either white, black or red. The difficult cases turn out to be when she is forced to use a red atom. This occurs only when $z$ is in $R_N'(x,y)$  (or $R_{N'}(y, x)$), and $|R_{N'}(x,y)|>1$ (respectively, $|R_{N'}(y,x)|>1$).

There are three ways to extend the network $N$ to $N'$ so that a new red clique of form $R_{N'}$ is created with $|R_{N'}(x,y)|>1$. The first is if $|R_N(x,y)|=1$ and $\forall$ plays $(x,y,{\sf g}_{i'},{\sf y})$ for some appropriate $i'\in G$.
In this case, $R_{N'}(x, y)=\set{w, z}$ for some $w\in N$, with $N(x, w)={\sf g}_{i}$ for some $i\neq i'\in G$, and by the first part of our assumption there are $j, j'\in H$ such that $h= \set{(i, j), (i', j')}$ is a partial homomorphism.  Here $\exists$ sets $N'(w, z)={\sf r}_{j, j'}$.
The second way such a red clique of size greater than one can be created is where $w\in N$, \/ $z$ is the new node, and $\forall$'s move is $(x,y,{\sf y},{\sf y})$, with $N(w,x)= {\sf g}_i$ and $N(w,y) = {\sf g}_{i'}$ for some $i\neq i'\in G$.  Since $\exists$ does not use green or yellow labels, $R_{N'}(w,z)=\set{x, y}$.  Here the map $h$ from green subscripts to red indices is a partial homomorphism of size two, by consistency of the previous network and of $\forall$'s move.  The third way is similar to the second, except $\forall$ plays $(x,y,{\sf g}_i,{\sf g}_{i'})$, and $N(w,x)=N(w,y)={\sf y}$. Here a partial homomorphism $h$ is defined as in the second case.

In all three cases, the second part of our assumption tells us that $h$ extends to a homomorphism $h^+:G\rightarrow H$.  In later rounds, whenever a new node is added to $R_N(x, y)$, \/ $\exists$ will use $h^+$ to get the index of the new node and hence to label all edges in $R_N(x, y)$ incident with the new node $z$. The fact that  red labels are defined by node indices will ensure that \eqref{f:red} is not violated and the fact that $h^+$ is a homomorphism will ensure that \eqref{f:pim} is not violated. Although in general it turns out that two distinct red cliques can intersect in up to two points, crucially the new point $z$ belongs to at most a single clique in the round when it is added,  so, $\exists$ is never conflicted about which homomorphism to use, as we shall see.

Now we have sketched out $\exists$'s plan, we must check that it works. Since the initial round and rounds indexed by limit ordinals present no difficulties, we consider rounds indexed by successor ordinals.   Suppose the current network is $N$ with $|N|\geq 2$, and $\forall$'s move is $(x, y, \alpha, \beta)$, with $\exists$ responding by adding a new node $z$ to create $N'=N\cup\{z\}$.  We have two induction hypotheses:
\begin{enumerate}
\renewcommand{\labelenumi}{\text{\theenumi}}
\renewcommand{\theenumi}{(\text{H\arabic{enumi}})}
\item\label{eq:induct}  For all $x', y'\in N$ where $|R_N(x', y')|\geq 2$ there is a homomorphism $h :G\rightarrow H$ such that for all $z\neq z'\in R_N(x', y')$ we have
\begin{equation*}
 (N(x', z)={\sf g}_i\wedge N(x', z)={\sf g}_{i'})\rightarrow N(z, z')={\sf r}_{h(i), h(i')}.
 \end{equation*}
\item\label{eq:induct2}  For any $x\neq y\in N$, if $\alpha$ and $\beta$ are green or yellow then there is at most a single node $z\in N$ such that $N(x, z)=\alpha,\; N(z, y)=\beta$.
\end{enumerate}

Given $N$, for each $x', y'\in N$ where $|R_N(x', y')|\geq 2$ let $h_{x'y'}$ be a homomorphism satisfying \eqref{eq:induct}.
For each $w\in N\setminus \{x,y\}$ she must assign $N'(w,z)$ in such a way that $N'$ is a network, and the induction hypothesis is maintained.    She proceeds as follows:
\begin{enumerate}[(a)]
\item
 If  $N(w, x)$ and $\alpha$ are not both green, and $N(w, y), \beta$ are not both green, she lets $N'(w, z)={\sf w}$.
  \item If $N(w, x), \alpha$ are both green but $N(w, y),\beta$ are not both yellow, or if $N(w, y), \beta$ are both green but $N(w, x), \alpha$ are not both yellow, she lets $N'(w, z)=\bb$.
  \item \label{case:rem} The remaining case is where $N(x, w)={\sf g}_{i},\;\alpha={\sf g}_{i'},\; N(w, y)=\beta={\sf y}$ (or similar with $x, y$ swapped). Note that $i\neq i'$, by the `no trivial moves' assumption.  Here $z,w\in R_N(x,y)$, and she is forced to choose $N'(w, z)={\sf r}_{j,j'}$ for some $j, j'\in H$.  If $h_{xy}$ is already defined  for $N$ she lets $N'(w, z)={\sf r}_{h_{xy}(i), h_{xy}(i')}$, thereby maintaining \ref{eq:induct} for $(x, y)$.  Otherwise, $R_N(x, y)=\set w$ and she may pick any  $j, j'\in H$ such that $\set{(i, j), (i', j')}$ is a partial homomorphism and extend it to a homomorphism $h_{xy}:G\rightarrow H$  (using both parts of  (1)) and again let $R_{N'}(w, z)={\sf r}_{h_{xy}(i), h_{xy}(i')}$, establishing \ref{eq:induct} for  $(x, y)$ in $N'$. Note that if $z \in R_{N'}(x',y')$, then, as $\exists$ never uses green or yellow labels, it's easy to show that $x=x'$ and $y=y'$, so the above strategy is well defined.
	\end{enumerate}

  First we show that $N'$ is a consistent network by checking that the labeling of each triangle $(w, w^*, z)$ for $w\neq w^*\in N$ is not forbidden.  If $\set{w, w^*}=\set{x, y}$ then the triangle is consistent (else $\forall$'s move would be illegal), so without loss of generality we assume that $w\notin \{x,y\}$.
  Observe that $N'(w, z)$ must be either white, black or red, as, if $N'(w, z)$ is green or yellow it follows that $w\in\set{x, y}$, contradicting our assumption.  If $N'(w, z)={\sf w}$, then the only possibility that the triangle $(w, w^*, z)$ could be forbidden comes from \eqref{f:nog}, but this requires that $N(w^*,z)$ and $N(w,w^*)$ be green, and thus that $w^*\in\{x,y\}$. But then the conditions of (a) would not have been met, so $N'(w,z)$ could not be ${\sf w}$ after all.  Similarly, if $N'(w, z)=\bb$ then the possibility of violating \eqref{f:noy} is ruled out by  case (b)  conditions.

	In the remaining case, $N'(w, z)$ is red, and the only forbidden triples involving red atoms are  \eqref{f:red}, \eqref{f:pim} and \eqref{f:ii}.    We assume $N(x, w)={\sf g}_i,\;\alpha={\sf g}_{i'}$, and the case where $x, y$ are swapped follows by symmetry.      A triangle $(w, w^*, z)$ could only violate forbidden triple \eqref{f:red} if all three edges were red, which only happens when $w, w^*, z\in R_{N'}(x, y)$. In this case, by \ref{eq:induct} we have $N'(w,w^*)= {\sf r}_{h_{xy}(i), h_{xy}(i^*)}$ for some $i^*\in G$ and some $h_{xy}$, and according to $\exists$'s strategy the other edge labels are $N'(w, z)={\sf r}_{h_{xy}(i), h_{xy}(i')}$ and $N'(z, w^*)={\sf r}_{h_{xy}(i'), h_{xy}(i^*)}$, so \eqref{f:red} is not violated.
  For forbidden triple \eqref{f:pim},  the only possible  green-green-red triangle incident with $z$ and $w$ is $(x, w, z)$ and the edge labels  $({\sf g}_i, {\sf g}_{i'},{\sf r}_{h_{xy}(i), h_{xy}(i')})$ do not violate \eqref{f:pim}, since $h_{xy}$ is a homomorphism.     The only triangle  containing $\set{w, z}$ which could violate \eqref{f:ii} is $(w, x, z)$ (only this can be green-green-red), but in this case $i\neq i'$ (else $w$ is a witness to the current move, contrary to the `no trivial moves' assumption) so \eqref{f:ii} is not violated.   Hence $N'$ is a consistent network.

It remains to check the induction hypotheses.  \ref{eq:induct2} is clear, since $\exists$ never adds a new node to the network if a suitable witness is already in $N$.  We check
 \ref{eq:induct}.  Suppose $\exists$ is playing according to the strategy we have described, and she adds $z$ to $N$ to obtain $N'$ in response to a move $(x, y, \alpha, \beta)$ by $\forall$.  We say that a pair $(x', y')$ is \emph{safe} if either $x', y' \in N$ and $R_{N'}(x', y')=R_N(x', y'),$ or $|R_{N'}(x', y')|\leq 1$.   If $(x', y')$ is safe then \ref{eq:induct} is true for $(x', y')$ in $N'$ either trivially because the size of $R_{N'}(x', y')$ is less than two, or inductively, since \ref{eq:induct} is assumed true for $N$.

  We check   induction hypothesis \ref{eq:induct} according to whether $\alpha$ and $\beta$ are green, yellow or neither.
 \begin{enumerate}[(i)]
\item \label{obs:2}
If $\alpha={\sf g}_i,\;\beta={\sf y}$ then $R_{N'}(x, y)=R_N(x, y)\cup\set z$ and  all other red cliques  are safe.
\item If $\alpha={\sf y},\;\beta={\sf g}_i$ then $R_{N'}(y, x)=R_N(y, x)\cup\set z$ and all other cliques are safe.
\item  If $\alpha={\sf g}_i,\;\beta={\sf g}_{i'}$ and $N(x, w)=N(w, y)={\sf y}$ for some $w\in N$, then $R_{N'}(z, w)=\set{x, y}$, and, by \ref{eq:induct2}, all other red cliques are safe.
\item If $\alpha=\beta={\sf y},\; N(x, w)={\sf g}_i, \; N(y, w)={\sf g}_{i'}$ for some $w\in N$,  then $R_{N'}(w, z)=\set{x, y}$,   and, \ref{eq:induct2},  all other red cliques are safe.
\item Else $\set{\alpha, \beta}\not\subseteq\set{{\sf g}_i, {\sf g}_{i'},{\sf y}}$ (for any $i, i'\in G$) and  all red cliques are safe.
\end{enumerate}
For case (i), if $R_{N'}(x, y)=\set{w, z}$ (some $w\in N$) then this red clique has size two in this round, for the first time.    Say $N(x, w)={\sf g}_{i'}$, where $i'\neq i$ else $w$ is already a witness.    By assumption (1) there is a partial homomorphism defined on $\set{i, i'}$ which extends to a homomorphism, and  her strategy chooses such a homomorphism $h_{xy}$ and lets  $N'(w, z)={\sf r}_{h_{xy}(i'), h_{xy}(i)}$,  as required for the induction hypothesis.    If $|R_{N'}(x, y)|\geq 3$ then $|R_N(x, y)|\geq 2$, so inductively there is already a homomorphism $h_{xy}:G\rightarrow H$ determining red labels in $R_N(x, y)$.  In this case, for each $w\in R_{N'}(x,y)$, her strategy defines $N'(w, z)={\sf r}_{h_{xy}(i'), h_{xy}(i)}$, where $N(x, w)={\sf g}_{i'}$, thereby maintaining \ref{eq:induct} for $(x, y)$ in $N'$.     Case (ii) is similar.

 In case (iii)  when $R_{N'}(z, w)=\set{x, y}$, since it follows from the stated conditions that $({\sf g}_i\comp {\sf g}_{i'})\cdot({\sf y}\comp {\sf y}) \geq N(x, y)$, we know that $N(x, y)={\sf r}_{j, j'}$ for some $j, j'\in H$, and, by \eqref{f:ii}, we must have $i\neq i'$.  By \eqref{f:pim} and the  legality of $\forall$'s move, $\set{(i,j), (i', j')}$ is a partial homomorphism.  By  assumption (1) this extends to a homomorphism $h_{zw}:G\rightarrow H$, as required by the induction hypothesis. Case (iv) is similar, and case (v) is trivial. So the strategy described above is indeed a winning one for $\exists$.
\end{proof}

The class of atom structures of representable relation algebras is known to be elementary \cite{V97:atom}.   We can apply the result above to say something about classes of atom structures intermediate between this class and that of the atom structures of completely representable relation algebras.

\begin{corollary}\label{C:atoms}
   If $\c K$ is a class of relation algebra atom structures including all atom structures of completely representable relation algebras, and contained in the class of atom structures of representable atomic relation algebras, then $\c K$ cannot be defined by any theory in the language of RA atom structures using only finitely many  atom valued variables.
\end{corollary}
\begin{proof}
A digraph may be considered as a binary structure with a single predicate denoting edges.
Given $m\geq 1$ let $K_m$ be the complete irreflexive digraph with $m$ vertices, and consider the algebras $\c B_{K_m, K_m}$ and $\c B_{K_{m+1}, K_m}$.  By theorem~\ref{thm:rainbow}, the former is completely representable while the latter is not, and, since they are finite, representability is the same as complete representability. Thus $\c B_{K_m, K_m}\in \c K$ and $\c B_{K_{m+1}, K_m}\notin \c K$. However,   $\exists$ has a winning strategy in the $m$-pebble, $\omega$-round Ehrenfeucht Fra\"iss\'e-game over the atom structures of $\c B_{K_m, K_m}$ and $\c B_{K_{m+1}, K_m}$ which we describe now (see e.g. \cite[chapter 6]{Im99} for a full description of the game). Whenever $\forall$ picks a non-green atom, $\exists$ picks the corresponding non-green atom in the other atom structure.  If $\forall$ places a pebble where another pebble is already placed, then $\exists$ covers the corresponding pebble in the other algebra. If $\forall$ picks a green atom, not already in play, then $\exists$ picks any green atom in the other atom structure not currently selected. There are always enough green atoms for this. This strategy is a winning one because the  underlying graphs are complete, so  a triple $({\sf g}_i, {\sf g}_{i'},{\sf r}_{j,j'})$ will be forbidden iff $i=i'$ or $j=j'$, in either atom structure. It follows that the two atom structures agree on all $m$-variable formulas (see e.g. \cite[theorem 6.10]{Im99}).

\end{proof}

The corollary shows that the atom structures of $\c B_{K_m, K_m}$ and $\c B_{K_{m+1}, K_m}$ cannot be distinguished in the language of atom structures restricted to $m$ atomic variables.
If we use formulas with variables that range over arbitrary elements of a relation algebra, much more  can be expressed.
Consider, for example, the formula $\phi_k(x)$ with  variables $x, y$ of which only $x$ appears free, which we will define shortly.  It is intended to express that $x$ is above  at least $k$ atoms, in an atomic relation algebra.  So $\phi_1(x)$ is $\neg(x=0)$.  Recursively, suppose $\phi_k(x)$ and $\phi_k(y)$ have been defined (the variables $x$ and $y$ are swapped throughout in the latter formula),  and  suppose the formula holds exactly when the free variable denotes an element  above at least $k$ atoms.  Let $\phi_{k+1}(x)$ be the formula $\exists y(y<x\wedge\phi_k(y))$.
If $k$ is the number of atoms in $\c B_{K_{m+1}, K_m}$ then $\exists x \phi_k(x)$ is true in  $\c B_{K_{m+1}, K_m}$ but not in $\c B_{K_m, K_m}$.  As well as defining the finite cardinality of an algebra, two variable formulas can express many other properties. Indeed, it is conceivable that any pair of non-isomorphic  finite relation algebras can be distinguished by a two variable formula; this remains an open problem.  The proof of corollary \ref{C:atoms} is a kind of warm up for the proof of theorem \ref{thm:main}, which involves formulas with variables ranging over arbitrary relation algebra elements, and  occupies most of the next section.

\section{A vertex colouring game}\label{S:game}

We now define a vertex colouring game played by $\forall$ and $\exists$ over a pair of binary structures using a finite number of colours, which are used to colour \emph{sets} of vertices, rather than the individual vertices used in the pebble game used in the proof of corollary \ref{C:atoms}. This game is studied in more detail for digraphs in \cite{EgrHirgames}, where it is called a \emph{Seurat game} in reference to the pointillist style of painting.
Let $c<\omega,\; n\leq \omega$.
Given two binary structures $G, H$ we define the  $c$-colour, $n$-round  colouring game ${\bf G}^c_n(G, H)$ to test equivalence of the binary structures using $c$ monadic predicates, $n$ times.  A $G$-interpretation is a map $\set{0, \ldots, c-1}\to\wp(G)$  to subsets of the vertices of $G$, and an $H$-interpretation is a mapping $\set{   0, \ldots, c-1}\rightarrow\wp(H)$. Intuitively, these maps associate vertices in $G$ and $H$ with the different colours.   A \emph{position} in the game consists of a $G$-interpretation and an $H$-interpretation.    A play of the game is a sequence of $1+n$ positions $(g_0, h_0),\ldots, (g_{i}, h_{i}), \ldots$ \/ ($i\leq n$). Round 0 begins with the starting position $(g_0, h_0)$, where  $g_0(t)=h_0(t)=\emptyset$, for all $t<c$ (i.e. initially all vertices are uncoloured).
 If $n=0$ then neither player does anything, and the result of the game is determined completely by the starting position (which for us is always the same, though this need not be required). For $n>0$, at the start of  round $r<n$, if the current position is $(g_{r}, h_{r})$, then $\forall$ chooses $t<c$ and a subset of the vertices of $G$ or a subset of the vertices of $H$, \/ $\exists$ responds with a subset of the nodes of the other binary structure. The intuition here is that $\forall$ is colouring some set of vertices in one of the structures, and $\exists$ is responding by colouring a set of vertices of the other structure with the same colour. If $\forall$ reuses a colour that has already been used, then its previous use is first erased from both binary structures. To reflect the new situation,  the position is updated  to $(g_{r+1},  h_{r+1})$ from $(g_r, h_r)$ by changing $g_{r+1}(t)\subseteq G$ and  $h_{r+1}(t) \subseteq H$ according to these choices.
	If $n$ is finite, the final position is $(g_n, h_n)$.

 A \emph{palette}
$\pi$ is a subset of $\set{0, \ldots, c-1}$.  Given a $G$-interpretation $g$, we may interpret $\pi$ by
\begin{equation*}\label{def:pal}\pi^g=\{x\in G: \forall t\in \pi (x\in g(t))\text{ and } \forall t\in\{0,\ldots,c-1\} \setminus \pi (x\notin g(t))\}.\end{equation*}
Intuitively, $\pi^g$ tells us which vertices of $G$ are coloured according to $g$ with exactly the combination of colours defined by $\pi$.
Observe that the set of vertices of $G$ is the disjoint union of the sets $\pi^g$, as $\pi$ ranges over palettes.
A position $(g, h)$ is a win for $\forall$ if  either
\begin{enumerate}[(C1)]
\renewcommand{\labelenumi}{\text{\theenumi}}
\renewcommand{\theenumi}{(\text{C\arabic{enumi}})}
\item\label{C1} there is a palette $\pi$ where $\pi^g$ is empty but $\pi^h$ is not or the other way round,  or
\item\label{C2} there are palettes $\pi, \pi'$ and a binary predicate $b$ such $(\pi^{g}\times(\pi')^{g})\;\cap\; b^G$ is empty but $(\pi^{h}\times (\pi')^{h})\;\cap \; b^H$ is not, or the other way round.
\end{enumerate}

We say that $\forall$ wins in round $k$ if $(g_k,h_k)$ is the first winning position for him.  For $n<\omega$, if $\forall$ does not win in any round $i\leq n$, then $\exists$ is the winner. If $n=\omega$, then $\exists$ wins if $(g_k,h_k)$ is not a win for $\forall$ for all $k<\omega$.

\medskip
In addition to the game described above, we will use the following minor variation of the classic Ehrenfeucht-Fra\"iss\'e game used in the proof of corollary \ref{C:atoms}. Given two relation algebras $\c A, \c B$ we define the $c$-pebble, $n$-round equivalence game $\Gamma^c_n(\c A, \alpha_0, \c B,\beta_0)$.  The pair $(\alpha_0, \beta_0)$ defines the starting position of the game, and consists of two partial maps $\alpha_0:\set{0, \ldots, c-1} \rightarrow \c A$ and $\beta_0:\set{0, \ldots, c-1}\rightarrow \c B$. We require that $\alpha_0$ and $\beta_0$ have the same domains (i.e. that they are defined for the same elements).  If the initial position is defined by maps with empty domains, then we may refer to the game just as $\Gamma^c_n(\c A, \c B)$ for brevity.

If $n=0$, then the game is entirely determined by the starting position, and neither player does anything. For $n\geq 1$, in each round $k<n$, if the position is $(\alpha_k, \beta_k)$, \/  $\forall$ picks $t<c$ and an element of $\c A$ or of $\c B$, and then $\exists$ picks an element of the other algebra.  At the end of the round, the position is updated by changing $\alpha_k(t)\in\c A,\;\beta_k(t)\in\c B$ according to these
choices, but leaving other values unchanged.
This defines $\alpha_{k+1}$ and $\beta_{k+1}$ ready for the start of the next round. Let $\c A_\alpha$ and $\c B_\beta$
denote the subalgebras of $\c A$ and $\c B$ generated by the images of $\alpha$ and $\beta$, respectively.
 At the start of round $k$, consider the binary relation $\alpha_k^{\smile}\circ\beta_k=\set{(\alpha_k(t), \beta_k(t)): t\in dom(\alpha_k)}$ (here $\circ$ and ${}^\smile$
 denote, respectively, ordinary composition and conversion of relations). If   $\alpha_k^{\smile}\circ\beta_k$ is a partial function
then it induces a homomorphism $\R{\alpha_k}{\beta_k}$ from $\c A_{\alpha_k}$ to $\c B_{\beta_k}$, else if $\alpha_k^{\smile}\circ\beta_k$ is not a function then let $\R{\alpha_k}{\beta_k}$ be an arbitrary non-isomorphism. We say $\forall$ wins the game in round $k$ if   $\R{\alpha_k}{\beta_k}$ is not an isomorphism, and the maps have been isomorphisms in
all previous rounds. On the other hand, $\exists$ wins if the maps we have described are isomorphisms for all $k\leq n$. The value of these modified Ehrenfeucht-Fra\"iss\'e games is given by the following definition and lemma.

	\begin{definition}
	Let $\c A$ and $\c B$ be relation algebras, and let $\alpha$ and $\beta$ be partial maps from $\{0,\ldots,c-1\}$ to $\c A$ and $\c B$, respectively, and suppose also that $\alpha$ and $\beta$ have the same domains. We say
	\[(\c A, \alpha) \equiv^c_n (\c B, \beta)\]
	if whenever $\phi$ is a first-order formula in the language of relation algebras with the additional restrictions that the quantifier depth in $\phi$ be at most $n$, that $\phi$ involves only  variables from the set $\{x_0,\ldots,x_{n-1}\}$, and that the free variables of $\phi$ are all indexed by values from the domain of $\alpha$ and $\beta$, we have
	\[\c A, \alpha \models \phi \iff \c B, \beta \models \phi.\]
	Here, for example, $\c A, \alpha \models \phi$ means that $\c A \models \phi$ if all variables $x_i$ occurring free in $\phi$ are assigned to $\alpha(i)$ in $\c A$.
	\end{definition}

\begin{lemma}\label{L:EF}
For $1\leq n \leq \omega$, if  $\exists$ has a winning strategy in $\Gamma^c_n(\c A,\alpha_0, \c B, \beta_0)$  then we must have $(\c A, \alpha) \equiv^c_n (\c B, \beta)$.
\end{lemma}
\begin{proof}
This is half the well known result for relational signatures (see e.g. \cite[theorem 6.10]{Im99}). Having functions in the signature blocks the proof of the converse. We induct on $n$. For the base case, $\exists$ has a winning strategy in $\Gamma^c_0(\c A,\alpha_0, \c B, \beta_0)$ if and only if the induced map $\R{\alpha_0}{\beta_0}$ is an isomorphism, if and only if $(\c A, \alpha_0), (\c B, \beta_0)$ agree on all equations using appropriate variables, if and only if $(\c A, \alpha_0) \equiv^c_0 (\c B, \beta_0)$.

For the inductive step, suppose $\exists$ has a winning strategy in $\Gamma^c_{n+1}(\c A, \alpha_0, \c B, \beta_0)$.   Let $\phi=\exists x_i \psi$ be a formula of quantifier depth at most $n+1$, where the variables occurring free in $\psi$ are either indexed by values for which $\alpha_0$ and $\beta_0$ are defined, or are $x_i$.    If $\c A, \alpha_0\models \exists x_i\psi$ then there is an $x_i$-variant $\alpha_1$ of $\alpha_0$ such that $\c A, \alpha_1\models \psi$.  If $\forall$ plays $\alpha_1(x_i)$ in the game, then since $\exists$ has a winning strategy there is an $x_i$-variant $\beta_1$ of $\beta$ where $\exists$ has a { winning strategy}\ in $\Gamma^c_n(\c A, \alpha_1, \c B, \beta_1)$.    Inductively, $\c B, \beta_1\models\psi$, hence $\c B, \beta_0\models\exists x_i \psi$.  Since the argument is symmetric, it follows that $(\c A, \alpha_0)$ agrees with $(\c B, \beta_0)$ on all $c$-variable formulas  $\exists x_i\psi$ where $\psi$ has quantifier depth at most $n$, hence they agree on all $c$-variable formulas of quantifier depth at most $n+1$.      By induction, the lemma holds for all finite $n$.  For the case $n=\omega$ then a { winning strategy}\ for $\exists$ in $\Gamma^c_\omega(\c A, \alpha_0, \c B, \beta_0)$ entails a { winning strategy}\ in all finite length games, so $(\c A, \alpha_0)\equiv^c_n(\c B, \beta_0)$ for all finite $n$.  Hence $(\c A, \alpha_0)\equiv^c_\omega(\c B, \beta_0)$, as required.
\end{proof}

Now we return to the Seurat game ${\bf G}$. This has a connection to the game $\Gamma$ which we will exploit in the proof of lemma \ref{L:K-equiv} to come. First, given $m>0$, let $K_m$ be the complete irreflexive directed graph with $m$ vertices.

\begin{lemma}\label{L:K}
Let $1\leq c,n < \omega$, and let $m,m'\geq 2^n$. Then $\exists$ has a winning strategy in ${\bf G}^c_{n-1}(K_m,K_{m'})$.
\end{lemma}
\begin{proof}
Note that, since the graphs are complete, $\forall$ wins in a round if and only if at the start of that round there is a palette $\pi\subseteq \{0,\ldots,c-1\}$ where
\begin{align*} \tag{$\ast$}  \label{eq:win} |\pi^g|\neq|\pi^h| \mbox{and either }|\pi^g|< 2 \mbox{ or } |\pi^h|< 2.
\end{align*}

Suppose $\exists$ plays according to the following principle. She ensures that:
\begin{align*}\tag{$\dagger_r$}\label{t:dag} \text{For all palettes $\pi$, if either $|\pi^{g_r}|< 2^{n-r}$ or $|\pi^{h_r}|< 2^{n-r}$ then $|\pi^{g_r}|=|\pi^{h_r}|$}.\end{align*}
If $\exists$ can maintain $(\dagger_r)$ while $r\leq n-1$ she will survive at least up to the beginning of round $n-1$, when $(g_{n-1},h_{n-1})$ is checked and the games ends. Note that if the game were  to continue for another round then she might lose, because with $r=n$ she is not insured against violating \eqref{eq:win} above.

We now prove by induction that $\exists$ can indeed always play so as to ensure the above condition holds up to and including $r=n-1$. The condition is obviously satisfied at the beginning of the game, because all vertices of both binary structures are uncoloured, so the empty palette is interpreted as the whole structure, and all other palettes are interpreted as the empty set. Suppose now that the condition is satisfied going into round $r$, for some $ r< n-1$. That is, if $(g_{r},h_{r})$ was the state of play at the start of round $r$, we can assume that $\exists$ has played so that $(\dagger_{r})$ is satisfied.

Suppose  that $\forall$ picks $t<c$ and, without loss of generality, a subset $X$ of $G$ (the case where he chooses a subset of $H$ is similar).  Let $(g'_{r}, h'_{r})$ be the position identical to $(g_{r}, h_{r})$ except $g'_{r}(t)=h'_{r}(t)=\emptyset$ (so we essentially `delete' colour $t$ from both graphs).  Observe that ($\dagger_{r}$) remains true for $(g'_{r},h'_{r})$.  We also have $X=\bigcup_{\pi\subseteq\set{0,\ldots, c-1}}(X\cap \pi^{g'_{r}})$.

For $\exists$'s response $Y\subseteq H$ to $\forall$'s move $(t, X)$ she will pick  disjoint subsets
$Y_{\pi}\subseteq \pi^{h'_{r}}$ for each palette $\pi$, and then she will define $Y=\bigcup_{\pi\subseteq\set{0,\ldots, c-1}}Y_\pi$. How she chooses $Y_{\pi}$ is explained below. Let $\pi$ be any palette not containing $t$, as if $t\in \pi$ we have $\pi^{h_r'}=\emptyset$ so her choice is trivial.   She defines $Y_\pi$  as follows:
\begin{itemize}
\item If  $|\pi^{g'_{r}}\cap X|< 2^{n-(r+1)}$ and $|\pi^{g'_{r}}\setminus X|< 2^{n-(r+1)}$, then  $|\pi^{g'_{r}}|< 2^{n-r}$,  so inductively $|\pi^{g'_{r}}|=|\pi^{h'_{r}}|$. Here she lets $Y_\pi$ be any subset of $\pi^{h'_{r}}$ of size $|\pi^{g'_{r}}\cap X|$, and it follows immediately that   $\pi^{h'_{r}}\setminus Y_\pi$ has the same size as $\pi^{g'_{r}}\setminus X$.

\item If $|\pi^{g'_{r}}\cap X|< 2^{n-(r+1)}$ but $|\pi^{g'_{r}}\setminus X|\geq 2^{n-(r+1)}$ then she lets $Y_\pi$ be any subset of $\pi^{h'_{r}}$ of the same size as $\pi^{g'_{r}}\cap X$. It follows that $\pi^{h'_{r}}\setminus Y_{\pi}$ will be of size at least $2^{n-(r+1)}$.  The case where $|\pi^{g'_{r}}\setminus X|< 2^{n-(r+1)}$ but $|\pi^{g'_{r}}\cap X|\geq 2^{n-(r+1)}$ is similar. Here she chooses $Y_\pi$ so that $|\pi^{h'_{r}}\setminus Y_\pi|=|\pi^{g'_{r}}\setminus X|$.

\item Finally, if both $\pi^{g'_{r}}\cap X$ and $\pi^{g'_{r}}\setminus X$ have size at least $2^{n-(r+1)}$, then $|\pi^{g'_{r}}|\geq  2^{n-r}$, so inductively $|\pi^{h'_{r}}|\geq 2^{n-r}$.  She lets $Y_\pi\subseteq \pi^{h'_{r}}$  be any subset of size $2^{n-(r+1)}$, so $\pi^{h'_{r}}\setminus Y_\pi$ must have size at least $2^{n-(r+1)}$.
\end{itemize}

Then $\exists$ lets $h_{r+1}$ be the same as $h_{r}$ except $h_r(t)=Y=\bigcup_{\pi\subseteq\set{0,\ldots, c-1}}Y_\pi$. Now, given a palette $\pi$  we have
\[\pi^{g_{r+1}} = \begin{cases} \pi^{g'_r}\setminus X \text{ if } t\notin\pi \\
 \pi^{g'_r}\cap X \text{ if } t\in \pi\end{cases}\]  \[\pi^{h_{r+1}} = \begin{cases}\pi^{h'_r}\setminus Y = \pi^{h'_r}\setminus Y_\pi \text{ if } t\notin\pi \\
 \pi^{h'_r}\cap Y=Y_\pi \text{ if } t\in\pi\end{cases}\] By the definition by cases given above, the cardinalities of these sets agree when necessary. Thus ($\dagger_{r+1}$) is established for the new position $(g_{r+1}, h_{r+1})$.
\end{proof}

Let $F, G, H$ be finite digraphs.   We are interested in the games $\Gamma^c_n(\c B_{G,F}, \c B_{H,F})$. Note that $\c B_{G,F}$ and $\c B_{H,F}$ are both finite (and thus atomic), and differ only with respect to their sets of green atoms (we identify the non-green atoms between each algebra in the obvious way).
Given an element $x\in \c B_{G,F}$, we define the set of vertices of $G$ indexing green atoms under $x$ to be $G_x$. Similarly, given $y\in \c B_{H,F}$, we define the set of vertices of $H$ indexing green atoms under $y$ to be $H_y$.

\begin{lemma}\label{L:K-equiv}
Let $1\leq c,n<\omega$ and let $F$ be any digraph.
If  $m,m'\geq 2^n$  then $\c B_{K_m, F}\equiv^c_{n-1}\c B_{K_{m'}, F}$.
\end{lemma}

\begin{proof}
By the previous lemma, we know that $\exists$ has a { winning strategy}\ in the game ${\bf G}^c_{n-1}(K_m, K_{m'})$.
To prove the equivalence it suffices, by lemma~\ref{L:EF}, to prove that $\exists$ has a { winning strategy}\ in $\Gamma^c_{n-1}(\c B_{K_m, F}, \c B_{K_{m'}, F})$.
Her strategy is to simulate a corresponding play of ${\bf G}^c_{n-1}(K_m, K_{m'})$ in which she uses her { winning strategy},  and to maintain a correspondence between the plays of the games.  So, if $\forall$ selects $x\in\c B_{K_m, F}$, then she selects $y\in \c B_{K_{m'}, F}$ whose non-green part is identical to that of $x$ and whose green part is defined by her response to the $\forall$-move $G_x$ in the play of ${\bf G}^c_{n-1}(K_m, K_{m'})$, and similar when he picks $y\in\c B_{K_{m'}, F}$.

Let $(\alpha, \beta)$ be a position in a play of $\Gamma^c_{n-1}(\c B_{K_m, F}, \c B_{K_{m'}, F})$ in which $\exists$ uses this strategy, and let $(g, h)$ be the corresponding position in a play of ${\bf G}^c_{n-1}(K_m, K_{m'})$.  Using our assumption that $(g, h)$ is not a win for $\forall$ we have
\[\label{t:dag2}\tag{$\dagger$} \text{either $|\pi^g|=|\pi^h|$ or $|\pi^g|, |\pi^h|\geq2$, for all palettes $\pi$},\]
and we have to prove that $\exists$'s move does not result in a losing position in the game $\Gamma^c_{n-1}(\c B_{K_m, F}, \c B_{K_{m'}, F})$, by showing that  there is a relation algebra isomorphism from $(\c B_{K_m, F})_\alpha$  to $(\c B_{K_{m'}, F})_\beta$ (recall that these are the subalgebras generated by the ranges of $\alpha$ and $\beta$ respectively).

   Consider the boolean subalgebra $\c B$ of $\c B_{K_m, F}$ generated (using boolean operators) by  the range of $\alpha$ and all non-green atoms.   For any palette $\pi$, let $\pi^{\c B}=\sum_{t\in\pi^g}{\sf g}_t\in \c B$, the corresponding green element  of $\c B$.  If $\pi^g=\emptyset$ then  the sum is empty and $\pi^{\c B}=0$, else  the sum is non-empty and $\pi^{\c B}$  is a an atom of $\c B$. A little thought reveals that all green atoms of $\c B$ arise in this way.
  Similarly, let $\c B'$ be the boolean sub-algebra of $\c B_{K_{m'}, F}$ generated by the non-green atoms and $rng(\beta)$, and let  $\pi^{\c B'}=\sum_{t\in \pi^h}{\sf g}_t$.
   Since $\pi^g=\emptyset\iff \pi^h=\emptyset$, for all palettes (by \eqref{t:dag2}), the map
	\[\phi=\set{ (\pi^{\c B}, \pi^{\c B'}):\pi\subseteq\set{0, \ldots, c-1}}\setminus\set{(0,0)}\]
	is a bijection from the green atoms of $\c B$ to those of $\c B'$ which extends to a unique boolean isomorphism $\hat{\phi}:\c B\rightarrow\c B'$ fixing non-green atoms.

   $\c B$ contains the identity and is closed under conversion, since all green elements are self-converse. In order to show that it is also closed under composition we have to check that whenever  $x, y, z$ are  boolean atoms in $\c B$, we have either $(x\comp y)\cdot z = 0$ or $x\comp y\geq z$. We indicate the former case by writing $\times$ and the latter case by writing $\checkmark$.

The cases where $1'\in\set{x, y, z}$ are easy, so suppose $x, y, z$ are non-identity atoms of $\c B$ (so each has a colour).  Recall that the only sets of three colours where some but not all triples of atoms of those colours are forbidden, are green-green-red and red-red-red.  In all other cases  either all triples of atoms of those colours are forbidden and we have $\times$ or none is forbidden and we have $\checkmark$.   If $z$ is red we get $\checkmark$ or $\times$ since $z$ is an atom of $\c B_{K_m,F}$.   So, without loss of generality suppose that $x = \pi_1^{\c B}$ and $z=\pi_2^{\c B}$ are green and $y={\sf r}_{j',j}$ is red (for some $j, j'\in F$). So we are interested in $(\pi_1^{\c B}\comp {\sf r}_{j',j})\cdot \pi_2^{\c B}$. We want to show that either for every green atom ${\sf g}_i$ (of $\c B_{K_m, F}$) below $\pi_2^{\c B}$ there is a green atom ${\sf g}_{i'}$ below $\pi_1^{\c B}$ such that $({\sf g}_{i'},{\sf r}_{j',j},{\sf g}_{i})$ is not forbidden (for $\checkmark$), or that for every green atom ${\sf g}_i$ (of $\c B_{K_m, F}$) below $\pi_2^{\c B}$ and for every green atom ${\sf g}_{i'}$ below $\pi_1^{\c B}$, the triple $({\sf g}_{i'},{\sf r}_{j',j},{\sf g}_{i})$ is forbidden (for $\times$).

Applying the Peircean equivalences, the triple under consideration here is equivalent to $({\sf g}_i,{\sf g}_{i'},{\sf r}_{j,j'})$.  In this case, if either $(j,j')$ or $(j', j)$ is not an edge of $F$, then we have $\times$ since $K_m$ is complete, which means the triple will be forbidden when $i\neq i'$, and the triple is always forbidden when $i=i'$ anyway. Suppose then that both $(j,j')$ and $(j', j)$ are edges.   Here we also have $\times$ if $x=z$ and $|\pi_1^g|=|\pi_2^g|=1$, since $({\sf g}_i,{\sf g}_i,{\sf r}_{j,j'})$ is always forbidden.  However, if $x=z$ and $|\pi^g|\geq 2$, or if $x\neq z$, we get $\checkmark$, since $K_m$ is complete.

    It follows that $\c B$ is closed under all relation algebra operations, and is a sub-relation algebra of $\c B_{K_m, F}$.     Since $rng(\alpha)\subseteq\c B$ we have the inclusion of relation algebras,  $(\c B_{K_m, F} )_\alpha \subseteq \c B\subseteq \c B_{K_m, F}$.  Similarly, the boolean subalgebra $\c B'$ of $\c B_{K_{m'}, F}$ generated by non-green atoms and $\set{\beta(t):t\in dom(\beta)}$ is a sub-relation algebra of $\c B_{K_{m'}, F}$ extending $(\c B_{K_{m'},F})_\beta$.

To show that the map $\hat{\phi}:\c B \to \c B'$ is a relation algebra isomorphism, it is sufficient to show that for all atoms $x,y,z$ of $\c B$, we have \[(x\comp y)\cdot z = 0 \iff (\phi(x)\comp \phi(y))\cdot \phi(z) =0.\] In other words, that $ (x, y, z)$ corresponding to $\checkmark$ or $\times$ means $ (\phi(x), \phi(y), \phi(z))$ corresponds to $\checkmark$ or $\times$ appropriately. By what we have just proved,  the division of triples of diversity atoms $ (x, y, z)$ in $\c B$  into $\checkmark$ and $\times$ depends on the colours of $x, y, z$, whether $x=z$ in the case where both $x$ and $z$ are green,  and, if $x=z=\pi^{\c B}$ is green, on whether $|\pi^g|$ is at least two or not.  In all cases, this will be matched by $(\phi(x),\phi(y),\phi(z))$, as $\exists$ is using a winning strategy in the parallel game ${\bf G}^c_{n-1}(K_m, K_{m'})$,  and thus $\hat{\phi}$ is an isomorphism as required.

Moreover, for all $t$ in the domain of $\alpha$ we have $\hat{\phi}(\alpha(t)) = \beta(t)$, as $\exists$'s strategy in $\Gamma^c_{n-1}(\c B_{K_m, F}, \c B_{K_{m'}, F})$ ensures this is true. It follows that the restriction of $\hat{\phi}$ to $(\c B_{K_m, F})_\alpha$, which, as we have just proved, is an isomorphism onto $(\c B_{K_{m'}, F})_\beta$, is $\R{\alpha}{\beta}$. Thus $\exists$ survives the game $\Gamma^c_{n-1}(\c B_{K_m, F}, \c B_{K_{m'}, F})$ for another round, as required.
\end{proof}

Now let $\c A=\c B_{K_{2^{n+1}},  K_{2^{n+1}}}$ and $\c B=\c B_{K_{1+2^{n+1}}, K_{2^{n+1}}}$.  Then $\c A\in RRA$ but $\c B\not\in RRA$, by theorem \ref{thm:rainbow}, and $\c A\equiv^c_{n}\c B$ by lemma \ref{L:K-equiv}.  It follows that RRA cannot be axiomatised by any theory consisting of $c$-variable  formulas of quantifier depth at most $n$. This proves theorem~\ref{thm:main}, and so RRA cannot be defined by formulas of bounded quantifier depth as claimed.

\begin{remark}
This suggests that a similar construction could be used to prove that the class of representable cylindric algebras of dimension $n$ cannot be defined by a theory of bounded quantifier depth, however we have not succeeded in demonstrating this.    There is a way of constructing a \emph{rainbow cylindric algebra} of dimension $n\geq 4$ from two graphs $G, H$ given in \cite[\S4.3.3] {HH2}.  The atoms of this cylindric algebra are labelled hypergraphs on $n$ nodes.  The two-dimensional edges of these hypergraphs have green, red and other labels generalising the green, red, yellow and black atoms of  the rainbow relation algebra $\c A_{G, H}$, but the white atoms ${\sf w}_S$ are replaced by $(n-1)$-ary hyperlabels in the cylindric version.  Our modified rainbow construction, in which the atom ${\sf w}_S$ are all deleted,  can be used to make a slightly easier cylindric algebra $\c C^n_{G, H}$ from two graphs whose atoms are labelled graphs on $n$-nodes, and no hyperlabels are needed.    It follows that $\c C^n_{G, H}$ is generated by its \emph{relation algebra reduct}.  By considering the graphs $K_{m+1}$ and $K_m$ we can show that $\c C^n_{K_{m+1}, K_m}$ is not in $RCA_n$ but $\c C^n_{K_m, K_m}$ is in $RCA_n$.       The problem is that although the atom structures of these two cylindric algebra agree on all $m$-variable atom structure formulas, we cannot prove that the two cylindric algebras are equivalent with respect to unrestricted formulas of quantifier depth at most $\log m$.  Thus our attempt to extend to various algebras of higher order relations using the known connections between relation algebras and cylindric algebras was not successful.

\end{remark}

\section{A corrected strategy for proving no finite variable axiomatisation exists for RRA}\label{S:correction}
It turns out that if $\exists$ has a winning strategy in the infinite game ${\bf G}^{c+3}_\omega(G,H)$, then she also has a winning strategy in $\Gamma^c_n(\c B_{G,F}, \c B_{H,F})$ for all $n<\omega$, and this can be used to correct the claims of \cite[problem 1, page 625]{HH:book}. We will prove this soon, but first we will need the following lemmas.

\begin{lemma}\label{L:size}
Let $G$ and $H$ be binary structures and let $c\geq 2$. Then, if $\exists$ is playing ${\bf G}^c_\omega(G,H)$ according to a winning strategy, whenever $\forall$ colours a set in one of the binary structures, $\exists$ must respond by colouring a set of nodes of the other binary structure with the same cardinality
\end{lemma}
\begin{proof} If the set of nodes with a certain colour is bigger in one structure than the other, then $\forall$ may use a second colour to colour all but one node in the larger set (and $\exists$ must colour a proper subset of the smaller set to avoid losing straight away), and he may repeat by re-using his first colour to colour all but one node of the larger set, and so on, until he colours a non-empty set of nodes in the first graph but $\exists$ has only the empty set to choose in the other graph, so $\forall$ wins.
See \cite[Proposition 2.3]{EgrHirgames} for the details.
\end{proof}

Now consider the relation algebra equivalence game $\Gamma^c_\omega(\c B_{G, F}, \c B_{H, F})$.
As in the proof of lemma \ref{L:K-equiv}, we suppose that $\exists$ maintains a private corresponding play of a colouring game over $(G,H)$, but now we suppose she is playing according to a winning strategy in the infinite game ${\bf G}^{c+3}_\omega(G, H)$, which has three extra colours.
So, to recap, if, for example, $\forall$ picks an element $x\in\c B_{G, F}$, she picks the element $y\in\c B_{H, F}$ with the identical non-green part and green part determined by $H_y$, where $H_y$ is the response to $G_x$ in the parallel play of ${\bf G}^{c+3}_\omega(G, H)$.    These moves in the play of ${\bf G}^{c+3}_\omega(G, H)$ are determined by the play of $\Gamma^c_\omega(\c B_{G, F}, \c B_{H, F})$ and only involve the first $c$ colours.  Our assumption is that  at each position $(g, h)$ occurring in the play of  ${\bf G}^{c+3}_\omega(G, H)$,\/   $\exists$ has a { winning strategy}\ in the game proceeding from $(g, h)$, even if $\forall$ decides to use the three additional colours. In other words, $\exists$ cannot make any move in the parallel game resulting in a position from which $\forall$ could force a win.

Suppose $(\alpha, \beta)$  is a position in $\Gamma^c_\omega(\c B_{G, F}, \c B_{H, F})$, played as described above, and let $(g,h)$ be the corresponding position in ${\bf G}^{c+3}_\omega(G, H)$. We will need to interpret terms in the language of relation algebras with finite variable set $\{x_0,\ldots,x_{c-1}\}$ in the algebras $\c B_{G, F}$ and $\c B_{H, F}$.    For any variable $x_i$ where $i\in dom(\alpha)$, we interpret $x_i$ in $\c B_{G, F}$ by defining $x_i^\alpha=\alpha(i)\in\c B_{G, F}$. If $b$ is a relation algebra constant, we define $b^\alpha$ to be the interpretation of $b$ in $\c B_{G, F}$.  Thus, any relation algebra term  $t$ involving only variables with indices in $dom(\alpha)$ and relation algebra constants has an obvious interpretation $t^\alpha\in\c B_{G, H}$, and similarly $t^\beta\in\c B_{H, F}$.  For any such term $t$ we define $\gamma(t)=\set{x\in G:{\sf g}_x\leq t^\alpha}$ and $\eta(t)=\set{y\in H:{\sf g}_y\leq t^\beta}$.
\begin{lemma}\label{L:terms}
Let $(\alpha,\beta)$ be a position arrived at in a game $\Gamma^c_n(\c B_{G,F}, \c B_{H,F})$ during which $\exists$ plays using a winning strategy in a parallel game ${\bf G}^{c+3}_\omega(G,H)$, as described above. Let $t$ be a term involving only variables indexed by values from $dom(\alpha)=dom(\beta)$. Then:
\begin{enumerate}
\item The sets of non-green atoms below $t^\alpha$ and $t^\beta$ are identical. \label{e:ng}
\item In the parallel game ${\bf G}^{c+3}_\omega(G, H)$, if $\forall$ were to use a colour not previously used to colour $\gamma(t)$, then $\exists$   would have to respond by colouring $\eta(t)$, otherwise $\forall$ could force a win, and similar with  $\gamma(t)$ and $\eta(t)$ switched. \label{e:win}
\item $|\gamma(t)|=|\eta(t)|$. \label{e:card}
\end{enumerate}
\end{lemma}
\begin{proof}
For convenience we match the colours $\{0,\ldots,c-1\}$ in $\Gamma^c_n(\c B_{G,F}, \c B_{H,F})$ and ${\bf G}^{c+3}_\omega(G,H)$ in the obvious way, and we refer to the colours $\{c,c+1,c+2\}$ used in ${\bf G}^{c+3}_\omega(G,H)$ as \emph{additional colours}, or words to that effect.

We will use induction on $t$ to prove \eqref{e:ng} and \eqref{e:win}, and we note that \eqref{e:card} follows from \eqref{e:win}, because if $|\gamma(t)|\neq|\eta(t)|$, then by colouring $\gamma(t)$ with one of the extra colours, $\forall$ could force $\exists$ to colour a set with a different size, and thus force a win in ${\bf G}^{c+3}_\omega(G,H)$ (see Lemma \ref{L:size}). In the base case, \eqref{e:ng} is automatic. For \eqref{e:win}, suppose $t = x_i$, and $t^\alpha = \alpha(i)$ for some $i\in dom(\alpha)$. So $\gamma(t) =\gamma(x_i)=\{x\in G:{\sf g}_x\leq \alpha(i)\}$ is already coloured by the $i$th colour. Moreover, $\eta(t)=\{y\in H: {\sf g}_y\leq \beta(i)\}$ must also be coloured by this colour, as according to $\exists$'s strategy $\beta(i)$ is defined to make this true. If $\forall$ uses one of the additional colours to colour $\gamma(t)$, then $\exists$ must colour all of $\eta(t)$ in response, otherwise there will be a palette mismatch between $G$ and $H$. The cases where $t$ is one of the relation algebra constants are also easy. For the inductive step, we proceed as follows (assuming the result for terms $s,s_1,s_2$):

$t = -s$: As the non-green parts of the two relation algebras are identical, \eqref{e:ng} holds for $t$. For \eqref{e:win}, if $\forall$ uses an additional colour to colour $\gamma(-s)\subseteq G$ then $\exists$ must colour a set $Y\subseteq H$ with the same  colour.  If he goes on to colour $\gamma(s)\subseteq G$ with a second additional colour, then by inductive assumption $\exists$ will colour $\eta(s)\subseteq H$ with that colour.    We know that $\gamma(s), \gamma(-s)$ are disjoint and cover $H$.  Since the position is a winning position it must be that  $Y, \eta(s)$ are disjoint and cover $G$, hence $Y$ is the complement in $H$ of $\eta(s)$, so $Y=\eta(-s)$, as required.

$t = s_1\cdot s_2$: For \eqref{e:ng}, if $a$ is a non-green atom, then, appealing to the inductive hypothesis, we have
\[a\leq (s_1\cdot s_2)^\alpha \iff a\leq s_1^\alpha \wedge a\leq s_2^\alpha \iff a\leq s_1^\beta \wedge a\leq s_2^\beta \iff a\leq (s_1\cdot s_2)^\beta.\]
For \eqref{e:win}, if $\forall$ uses an additional colour to colour $\gamma(s_1\cdot s_1)\subseteq G$ then $\exists$ must colour some set $Y\subseteq H$ with the same colour.  If he went on in the next two rounds to use the other two additional colours to colour $\gamma(s_1)$ and then $\gamma(s_2)$, then inductively we know that $\exists$ colours $\eta(s_1), \eta(s_2)\subseteq H$.  Since the position at the end of this is not a win for $\forall$ we must have $Y=\eta(s_1)\cap\eta(s_2) = \eta(s_1\cdot s_2)$, as required.

$t = s^\smile$: For any non-green atom $a$ we know $a^\smile$ is also a non-green atom and so
\[a\leq (s^\smile)^\alpha\iff a^\smile \leq (s^\alpha)^\smile \iff a^\smile\leq s^\alpha \iff a^\smile\leq s^\beta\iff a\leq (s^\smile)^\beta,\] proving \eqref{e:ng}.  Part \eqref{e:win} is easy since all green elements are self-converse, so $\gamma(s^\smile)=\gamma(s)$ and $\eta(s^\smile)=\eta(s)$.

$t = s_1\comp s_2$: We show first that \eqref{e:ng} holds. If $a\leq (s_1\comp s_2)^\alpha$ is a non-green atom then there are atoms  $b_1\leq s_1^\alpha,\;b_2\leq s_2^\alpha$ where $a\leq b_1\comp b_2$.     Not all triples of atoms of the colours of $b_1, b_2, a$ are forbidden, as we are assuming $a\leq b_1\comp b_2$.   If no triple of atoms of the colours of $b_1, b_2, a$ is forbidden, then $a\leq (s_1\comp s_2)^\beta$, because, by the inductive hypothesis with \eqref{e:ng} and \eqref{e:card}, the non-green atoms below $s_1^\alpha$ and $s_1^\beta$ are the same, and likewise for $s_2$, and $|\gamma(s_1)|=|\eta(s_1)|$, and likewise for $s_2$.

This leaves the case where some but not all triples of atoms of the colours of $b_1, b_2, a$ are forbidden. Recall that the only such colour combinations are red-red-red and green-green-red.    If $b_1, b_2, a$ are all red then, by the inductive hypothesis on \eqref{e:ng}, we have $b_1\leq s_1^\beta,\;b_2\leq s_2^\beta$, so $a\leq b_1;b_2\leq  (s_1;s_2)^\beta$.   This leaves the case where $a={\sf r}_{j_1,j_2}$ is a red atom, and $b_1={\sf g}_{x_1}, b_2={\sf g}_{x_2}$ are both green.    Since $({\sf g}_{x_1},{\sf g}_{x_2},{\sf r}_{j_1,j_2})$ is not forbidden,  we know that $x_1\neq x_2$ and $\set{(x_1, j_1), (x_2, j_2)}$ is a partial homomorphism.  Since $(g, h)$ is a position from which $\exists$ has a winning strategy in ${\bf G}^{c+3}_\omega(G, H)$, after a short but technical argument to come, we shall see that there must be $y_1\in\eta(s_1),\; y_2\in\eta(s_2)$ such that $\set{(y_1, j_1), (y_2, j_2)}$ is a partial homomorphism.

To this end, suppose for contradiction that there are no such $y_1, y_2$.
In the parallel game ${\bf G}^{c+3}_\omega(G, H)$, if  $\forall$ were to colour $\gamma(s_1)$ with one of the extra colours, and then to use another to colour $\gamma(s_2)$, then, by the inductive hypothesis on \eqref{e:win}, $\exists$ would have to respond by colouring $\eta(s_1)$ and $\eta(s_2)$ respectively. Suppose that $\forall$ then uses the final additional colour to colour $\{x_1, x_2\}$. Then $\exists$ must colour some $\{y_1,y_2\}\subseteq H$. Since $x_1\in \gamma(s_1)$ and $x_2\in \gamma(s_2)$,  we can suppose without loss of generality $y_1\in \eta(s_1)$ and $y_2\in \eta(s_2)$. Suppose that, in a further move, $\forall$ uses one of the original colours (i.e. $\{0,\ldots,c-1\}$)  to colour $\set{x_1}$, and without loss of generality we can assume that $\exists$ responds by colouring $\set{y_1}$ (if $\exists$ can colour $\set{y_2}$ then we must have $x_1,x_2\in\gamma(s_1)\cap \gamma(s_2)$ and $y_1,y_2\in\eta(s_1)\cap \eta(s_2)$, in which case we can just switch the labels of $y_1$ and $y_2$).  But then  $\set{(y_1, j_1), (y_2, j_2)}$ is not a partial homomorphism but $\set{(x_1, j_1),(x_2,j_2)}$ is a partial homomorphism, and it follows that $\set{(x_1,y_1),(x_2,y_2)}$ is not a partial isomorphism, indicating that \ref{C2} holds. Thus $\forall$ wins, contrary to our assumption that $\exists$ is following a winning strategy.
    The implication $a\leq (s_1;s_2)^\beta\Rightarrow a\leq(s_1;s_2)^\alpha$, for non-green atoms $a$, is proved similarly. This proves \eqref{e:ng}.

For \eqref{e:win}, the cases where either $s_1^\alpha$ or $s_2^\alpha$ is zero or the identity are trivial, so assume not.
First we suppose that $s_1^\alpha$ is either a single non-green atom, or pure green (i.e. above only green atoms), and the same for $s_2^\alpha$. By our induction hypothesis, $s_1^\beta$ is the same non-green atom in the former case and green in the latter case, and similar for $s_2^\beta$.  Suppose the colour of $s_1^\alpha$ is $c_1$, and that the colour of $s_2^\alpha$ is $c_2$.
  If all triples of atoms of colours $c_1$-$c_2$-green are forbidden (i.e. $c_1$ is green, $c_2$ is green or white, or the other way round) then $\gamma(s_1\comp s_2)=\eta(s_1\comp s_2)=\emptyset$.    If no triple of atoms of colours  $c_1$-$c_2$-green
  are forbidden then
  $\gamma(s_1;s_2)=G$
   and $\eta(s_1;s_2)=H$.    In both these cases, if $\forall$ colours $\gamma(s_1\comp s_2)$, then $\exists$ must obviously respond by colouring $\eta(s_1\comp s_2)$.
  The only colour combinations where some but not all triples of atoms of those colours are forbidden are red-red-red and green-green-red.
   So the remaining cases are where $c_1$ is green, $c_2$ is red, or the other way round.   Without loss of generality, suppose $s_1^\alpha$ is  green and $s_2^\alpha={\sf r}_{j, j'}$ is a red atom.    Observe that
  \[\gamma(s_1\comp s_2)=\set{x'\in G: \exists x\in\gamma(s_1)\text{ s.t. } \set{(x,j), (x', j')}\mbox{ is a partial homomorphism}},\] and
	\[\eta(s_1\comp s_2)=\set{y'\in H:\exists y\in\eta(s_1)\text{ s.t. } \set{(y,j), (y', j')}\mbox{ is a partial homomorphism}},\] using a Peircean transformation with \eqref{f:pim}. If either of these is empty then the result is trivial, so we assume not.

  If $\forall$ makes an additional move by colouring $\gamma(s_1\comp s_2)\subseteq G$ with $k$ where $c\leq k<c+3$, then $\exists$ responds by colouring some set $Y\subseteq H$ with $k$.    We have to prove that $Y= \eta(s_1\comp s_2)$.

   If he made another additional move by colouring $\gamma(s_1)$ with another additional colour $k'$ then, by our induction hypothesis, $\exists$ would colour $\eta(s_1)\subseteq H$ with that colour.
For any $y'\in\eta(s_1\comp s_2 )$, \/  $\forall$ could use the third additional colour $k''$ to colour $\{y'\}$, and in response, $\exists$ would have to colour some $\{x'\}\subseteq G$.  He could continue by picking $y\in \eta(s_1)$ such that $\set{(y, j), (y', j')}$ is a partial homomorphism and colouring $\set{y}$ with one of the original colours (say colour $0$) and $\forall$ would have to colour $\set{x}$ with $0$, where $x\in\gamma(s_1)$ as $\gamma(s_1), \eta(s_1)$ are coloured with $k'$.  Since $\forall$ does not win at this point, we know that $\set{(x, y), (x', y')}$ is a partial isomorphism, hence $\set{(x, j), (x', j')}$ is a partial homomorphism and $x'\in\gamma(s_1\comp s_2)$.  Since $x'$ is coloured with $k$ and $\forall$ does not win, $y'$ must also be coloured $k$, and so $y'\in Y$.

Conversely, suppose $y'\in Y$ (and so is coloured with $k$).    If $\forall$ uses the third additional colour $k''$ for $\set{y'}$ then $\exists$ must respond with $\set{x'}\subseteq \gamma(s_1\comp s_2)$. \/ $\forall$ picks $x\in\gamma(s_1)$ such that $\set{(x, j), (x', j')}$ is a partial homomorphism and colours $\set{x}$ with $0$, then $\exists$ responds by colouring $\set{y}$ with $0$, where $y\in\eta(s_1)$ and  $\set{(y, j), (y', j')}$ is a partial homomorphism.  Hence $y'\in\eta(s_1\comp s_2)$.  Thus $Y=\eta(s_1\comp s_2)$.

More generally, $s_1^\alpha$ and $s_2^\alpha$ are sums of non-green atoms and a single green element, and \eqref{e:win} holds for $(s_1\comp s_2)^\alpha$ since, as $\comp$ is additive, $s_1\comp s_2$ is the sum of simple terms where we have just shown it holds (the inductive case where $t=s_1+s_2$ being covered by the $-$ and $\cdot$ cases).

\end{proof}

 \begin{corollary}\label{C:terms}
If $\exists$ has a winning strategy in ${\bf G}^{c+3}_\omega(G,H)$, then she also has a winning strategy in $\Gamma^c_n(\c B_{G,F}, \c B_{H,F})$ for all $n\in\mbox{\( \mathbb N \)}$.
\end{corollary}
\begin{proof}
We assume that $\exists$ plays $\Gamma^c_n(\c B_{G,F}, \c B_{H,F})$ using the strategy used in lemma \ref{L:terms}. Suppose $(\alpha,\beta)$ is a position reached during play,  and let $t$ be a term such that $t^\alpha\neq 0$.  Then there is an atom below $t^\alpha$, and so by lemma \ref{L:terms} there must be an atom below $t^\beta$. By this and symmetry we have $t^\alpha =0 \iff t^\beta = 0$, and it follows that $\forall$ does not win at $(\alpha, \beta)$, as the map $\R{\alpha}{\beta}:(\c B_{G,F} )_{\alpha}\to(\c B_{H,F})_{\beta}$, which sends $t^\alpha$ to $t^\beta$, is thus an isomorphism.
\end{proof}

The following theorem, based on our modified rainbow algebras, corrects the argument presented in \cite[problem 1]{HH:book}.
\begin{theorem}\label{T:correction}
Suppose $G, H$ are finite binary structures such that
\begin{enumerate}[1.]
\item $\exists$ has a winning strategy in ${\bf G}^{c+3}_\omega(G, H)$,
\item every partial homomorphism of $H$ of size two extends to a full homomorphism  from $H$ into itself, and
\item either \begin{enumerate}[a.]
\item  there is no homomorphism $G\to H$, or
\item  there are $i\neq i'\in G$ and $j,j'\in H$ such that $\{(i,j),(i',j')\}$ is a partial homomorphism that does not extend to a homomorphism $G\to H$.
\end{enumerate}
\end{enumerate}
Then RRA cannot be defined by any $c$-variable first-order theory.
\end{theorem}

\begin{proof}
First note that by the partial homomorphism extension property assumed of $H$, there being no homomorphism $G\to H$ is equivalent to there being $i\neq i'\in G$ such that for all $j,j'\in H$ the partial map $\{(i,j),(i',j')\}$ is not a homomorphism. So it follows from lemma \ref{L:EF} and corollary \ref{C:terms} that $\c B_{G, H}$ and $\c B_{H, H}$ would agree about all first-order formulas with at most $c$ variables, but  by theorem~\ref{thm:rainbow} the latter relation algebra would be completely representable while the former would not.  Since both algebras are finite, all representations are complete, and it would follow immediately that
  $\c B_{H, H}  \in RRA,\; \c B_{G, H}\not\in RRA$.

\end{proof}

In the result above, conditions a) and b) seem to be incomparable. This is suggested by the following example.

\begin{example}
Let $G$ be the cyclic graph with three vertices $C_3$, and let $H$ be the discrete graph with a single vertex $D_1$. Then $H$ trivially satisfies condition 2, and $(G,H)$ satisfies condition 3.a. However, $(G,H)$ does not satisfy condition 3.b as there are no partial homomorphisms of size two from $G$ into $H$.

Alternatively, let $G$ be the three element walk (AKA chain) graph $W_3$ (this has vertices $\{v_0,v_1,v_2\}$ and edges $(v_0,v_1)$ and $(v_1,v_2)$), and let $H$ be the disjoint union of two copies of $C_3$. Then $H$ satisfies condition 2, and $(G,H)$ does not satisfy 3.a, as there's an obvious homomorphism $W_3\to C_3$, but does satisfy 3.b, as the partial homomorphism taking $v_0$ to a vertex in one copy of $C_3$ and $v_3$ to a vertex of the other copy of $C_3$ does not extend.
\end{example}

The above example is not conclusive as in neither case does $(G,H)$ satisfy condition 1. However, it's not clear if non-isomorphic binary structures satisfying this condition even exist. In the special case of graphs, the existence of such a non-isomorphic pair would disprove the reconstruction conjecture, as we discuss briefly after corollary \ref{C:digraph} below. On the subject of graphs, we can apply theorem \ref{T:correction} to obtain two ways to correct the graph based formulation of \cite[problem 1]{HH:book}. The first way is given by simply replacing `binary structure' with `graph' or `digraph' in the statement of that theorem. The second way is given by the result below.

\begin{corollary}\label{C:digraph}
Let $G, H$ be finite digraphs such that
\begin{enumerate}[1.]
\item $G, H$ cannot be distinguished in a modified infinitely long $(c+3)$-colour game where $\forall$ can also win at position $(g, h)$  if there are two palettes $\pi, \pi'$ and every pair from $\pi^g\times(\pi')^g$ is an edge but not every pair from $\pi^h\times (\pi')^h$ is an edge, or the other way round,
\item every partial embedding of $H$ into itself of size two extends to an automorphism of $H$, and
\item there is no embedding of $G$ into $H$.
\end{enumerate}
Then RRA cannot be defined by any $c$-variable first-order theory.
\end{corollary}
\begin{proof}
Two digraphs $G, H$ may be considered as binary structures with three predicates, one for edges, another for non-edges and a third for `non-equality' given by $\{(u,v):u\neq v\}$. The modified game for digraphs understood as binary structures with a single edge relation (the standard setting) is equivalent to the original game played over the same digraphs understood as binary structures with `edge', `non-edge' and `non-equality' relations. To see this, note that for palettes $\pi_1$ and $\pi_2$ the non-edge relation holding between $\pi_1^g$ and $\pi_2^g$ and not between $\pi_1^h$ and $\pi_2^h$ results in a win for $\forall$ according to the modified rules, even if we only consider the `edge' relation. Moreover, when $\pi_1\neq \pi_2$ the `non-equality' relation holds between $\pi_1^g$ and $\pi_2^g$ whenever these are both non-empty, as interpretations of distinct palettes are disjoint. Similar holds for $\pi_1^h$ and $\pi_2^h$, and so accommodating `non-equality' in the standard digraph setting does not require any modification to the game rules.

Now, homomorphisms in the `three relation' setting clearly correspond to embeddings in the standard digraph setting, and so condition 2 of theorem \ref{T:correction} translates into condition 2 here. Moreover, if there exists an embedding $G\to H$, then, by assumption of condition 2, every partial embedding $G\to H$ of size two must extend to a full embedding of $G$ into $H$, so condition 3 here covers both conditions 3.a and 3.b from theorem \ref{T:correction}.
\end{proof}

The result of corollary~\ref{C:digraph} and the graph result obtained from theorem \ref{T:correction} by writing `digraph' for `binary structure' seem to be incomparable in strength, though again the uncertainty around condition 1 prevents us from being sure. We get some indication of this by examining the conditions on the graph $H$ in the two results. Respectively, these are:
\begin{enumerate}[(1)]
\item Every partial homomorphism of size two of $H$ into itself extends to a full homomorphism.
\item Every partial embedding of $H$ into itself of size two extends to an automorphism.
\end{enumerate}
Observe that the cyclic graph $C_4$ satisfies (2) but not (1), and we can construct a graph satisfying  (1) but not (2) as follows (we work with undirected graphs here for simplicity). Let $W_2$ and $W_3$ be walk (AKA chain) graphs, and let $R$ be the graph with a single reflexive vertex $v$. Define $H$ by taking the disjoint union of $W_2$, $W_3$ and $R$, and adding an edge $(w,v)$ for each $w\in W_2\cup W_3$. Then $H$ satisfies (1), as every partial homomorphism can be extended by sending every other vertex to $v$. On the other hand, $H$ does not satisfy (2) as, if we suppose the vertices of $W_2$ and $W_3$ are $\{u_0,u_1\}$ and $\{w_0,w_1,w_2\}$ respectively, the partial embedding $\{(w_0,u_0),(w_1,u_1)\}$ cannot be extended to an automorphism.

Looking at the conditions on $H$ may well be beside the point however, as, as mentioned previously, we do not know whether non-isomorphic graphs $G, H$ exist such that $\exists$ can win even ${\bf G}^{2}_\omega(G, H)$.  The power of the game ${\bf G}$ to distinguish between graphs is investigated in more detail in \cite{EgrHirgames}. In particular, it is shown there in section 6 that finding non-isomorphic graphs indistinguishable in the 3-colour game would disprove the reconstruction conjecture for graphs (or one of its variations, in the case of directed graphs). This indicates that, at the very least, such graphs will likely be difficult to find.

\bibliographystyle{alpha}
 \def/\allowbreak{/\allowbreak}