Characterising invisible equivalences by confluent rewrite rules In response to another question, Extensions of beta theory of lambda calculus, Evgenij offered the answer:

beta + the rule {s = t | s and t are closed unsolvable terms}

where a term M is solvable if we can find a sequence of terms such that M's application to them is equal to I.  

Evgenij's answer gives an equational theory over the lambda calculus, but not one characterised by a reduction system, i.e., a confluent, recursive set of rewrite rules.

Let's call an invisible equivalence over a theory of the lambda calculus, a reduction system that equates some nontrivial set of closed unsolvable lambda terms, but doesn't add any new equations involving solvable terms.

Are there any invisible equivalences over the beta theory of the lambda calculus?

Postscript An example that characterises an invisible equivalence, but is not confluent.  Let M=(λx.x x) and N=(λx.x x x), two unsolvable terms.  Adding the rule rewriting N N to M M induces an invisible equivalence containing M M = N N, but has the bad critical pair where N N reduces to both M M and M M N, each of which has one rewrite available, which rewrites to itself.
Yes.  With M=(λx.x x) per the question, consider the rewrite &zeta; that takes M M p to M M.

It is confluent, and so characterises a reduction system over the lambda calculus.  Argument sketch for confluence: since M M is closed, we only need to consider critical pairs of the form M M N1 ... Nk.  These can be resolved.

It is an invisible equivalence, because terms of the form M M I ... I (with zero or more I s) are closed unsolvable terms that reduce only to themselves in the base lambda calculus, thus are distinct, and so the infinite set of these terms is nontrivial, and is obviously equated by &zeta;.

I don't like accepting my answer to my question, so I'll accept an answer from someone who provides a less absurdly incomplete confluence argument.