We consider the system 480.

  Alphabet:

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

  Rules:

    f(X, /\x.Y(x)) => Y(X) 
    g(a, a) => f(a, /\x.g(b, x)) 
    b => a 

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

  g(a, a) 
    => f(a, /\x.g(b, x)) 
    => f(a, /\x.g(a, x)) 
    => g(a, a) 

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