We consider the system 484.

  Alphabet:

    g : [o * o] --> o 
    h : [o -> o] --> o 
    i : [o] --> o 

  Rules:

    i(X) => g(X, X) 
    g(h(/\x.X(x)), Y) => X(Y) 

This system is non-terminating, as demonstrated by the following reduction:

  g(h(/\x.g(x, x)), h(/\y.g(y, y))) 
    => (/\x.g(x, x)) h(/\y.g(y, y)) 
    =>_beta g(h(/\x.g(x, x)), h(/\y.g(y, y))) 

That is, a term reduces to itself.