Consider the function $f = \lambda x \mapsto \neg (x\ x)$ where $\neg$ is negation.
It then follows that
$$ f\ f = \neg (f\ f) $$
Thus proving a contradiction, but $(f\ f)$ is an expression that does not have a $\beta$-normal form. This expression simply never returns. My intuition tells me that we can't say anything about the equivalence between the two terms because they're both irreducible to $\beta$-normal form.
Does voiding expressions containing non-$\beta$-normal forms make the untyped lambda calculus consistent?