We consider the system 481.

  Alphabet:

    a : [] --> o 
    f : [(o -> o) -> o -> o] --> o 
    g : [] --> o -> o 
    h : [o * o] --> o 

  Rules:

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

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

  g a 
    => f(/\i./\x.h(i a, x)) 
    => h(h(g a, a), h(g a, a)) 
    |> g a 

That is, a term s reduces to a term t which has a subterm that is an instance of the original term.