Q:

Finite Model Property on the First-Order Theory of Two Equivalence Relations

I know that there is a first-order sentence $\varphi$  such that 

$\varphi$ is written in the vocabulary given by just two binary relation symbols $E_1$, $E_2$ (and hence, without the equality symbol*),
$\varphi$ is satisfiable in a model where $E_1$ and $E_2$ are equivalence relations,
$\varphi$ is not satisfiable in a finite model where $E_1$ and $E_2$ are equivalence relations. 

This has to be true because the first-order theory of two equivalence relations is undecidable (see the paper A. Janiczak, Undecidability of some simple formalized theories, Fundamenta Mathematicae, 1953, 40, 131--139).  However, I am not able to find any such formula.  
Does anybody know an example of a formula (or a family) with these three properties? 
Footnote *: The assumption of not allowing the equality symbol is not important.  Indeed, if we know a formula with equality where the last two previous properties hold, then the formula obtained replacing all subformulas $x \approx y$ with the formula $E_1(x,y) \land E_2(x,y)$ also satisfies these two properties.  

A:

Let's call two elements $x$ and $y$ $E_1$-neighbors if $(x \neq y \wedge E_1(x, y))$, and $E_2$-neighbors if $(x \neq y \wedge E_2(x, y))$.  Then the following assertions should suffice to force an infinite model:

Every element has exactly one $E_1$-neighbor. 
There exists an element with no $E_2$-neighbor; every other element has exactly one $E_2$-neighbor. 

In particular, the single element with no $E_2$-neighbor can be identified with $0$; and the remaining natural numbers are generated by alternating conditions 1) and 2).