We are looking for a proof or counter-examples for the following hypothesis.

Two combinators $M$ and $N$ are solvable and equivalent in [the HP-complete sensible $\lambda$-theory](http://mathgate.info/cebrown/notes/barendregt.php#4) iff either
$$
\exists n \in \mathbb N: \langle\varnothing\ |\ \Gamma(M, x) \cup \Gamma^*(N, x)\rangle \rightarrow^* \langle\varnothing\ |\ x_1 = x_1,\dots, x_n = x_n\rangle,
$$
or
$$
\forall n \in \mathbb N: \langle\varnothing\ |\ \Gamma(M, x) \cup \Gamma^*(N, x)\rangle \rightarrow^* \langle\varnothing\ |\ x_1 = x_1,\dots, x_n = x_n, \Delta\rangle,
$$
where $\Gamma(M, x)$ and $\Gamma^*(N, x)$ are defined in [a compact encoding for $\lambda$-terms in interaction calculus](http://arxiv.org/abs/1304.2290).

Any help would be appreciated.