Has any full, finitely-generated and Church-Rosser term-rewriting system (or system with bound variables) a recursive, one-step, normalizing reduction strategy?

The source page states the original problem together with its recorded qualifications and progress updates as follows.

Let a term-rewriting system (or more generally, a system with bound variables [Kennaway, 1991]) have the following properties: it is finitely generated'' (has finitely many function symbols and rules), it is full'' (its terms are all that can be formed from the function symbols), and it is Church-Rosser. Does it follow that it has a recursive, one-step, normalizing reduction strategy? (There are counterexamples if any of the three conditions is dropped.) Kennaway [Kennaway, 1991] showed that for ``weakly'' orthogonal systems the answer is yes. So, any counterexample must come from the murky world of non-orthogonal systems. See also [Kennaway, 1991].