This question is from Shoenfield's "Mathematical Logic", an exercise on page 25.
Show that the formula $((x \neq x) \vee \neg(x \neq x \vee x \neq x)) \vee (x \neq x \vee x \neq x)$ is a theorem, but is not provable without the associative rule.
There is also a hint:
Consider the mapping $f$ from the set of formulas to the set of integers defined as:
$f(A) = 0 $ for atomic formulas
$f(\neg A) = 1 - f(A)$
$f(A \vee B) = f(A).f(B).(f(A) + f(B) - 1)$
$f(\exists x A) = f(A)$
Show that if $A$ is provable without the associative rule, then $f(A) = 0$
The hint is easy to verify, but the given formula also evaluates to $0$. So what should I do next?