We consider the system 444.

  Alphabet:

    mu : [o -> o] --> o 

  Rules:

    mu(/\x.X(x)) => X(mu(/\y.X(y))) 

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

  mu(/\x.f x) 
    => f mu(/\x.f x) 
    |> mu(/\y.f y) 

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