YES

Problem:
 a() -> b()
 b() -> f(a(),a())
 f(x,a()) -> b()

Proof:
 Qed (right-reducible TRS)