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

**Hypothesis.** In [interaction calculus][1] $\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \downarrow \langle \varnothing\ |\ x_1 = x_1, \dots, x_n = x_n \rangle$, where the $\Gamma$ mapping is defined in [a compact encoding][2] for $\lambda$-terms, $M, N \in \Lambda_0$ are combinators, and $n \geq 1$, *if and only if* $\lambda K\beta\eta \vdash M = N$.

In the case if the hypothesis holds true, we have an effective model for the $\lambda K\beta\eta$ equational theory.

[1]: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.46.3594
[2]: http://arxiv.org/abs/1304.2290