We consider the system 451.

  Alphabet:

    a : [] --> o 
    b : [] --> o 
    f : [o] --> o 

  Rules:

    f(X) => f(b) 
    f(a) => f(b) 

It is easy to see that this system is non-terminating:

  f(x) 
    => f(b) 

That is, a term s reduces to a term t which instantiates s.