We consider the system 467.

  Alphabet:

    abs : [term -> term] --> term 
    app : [term * term] --> term 

  Rules:

    app(abs(/\x.X(x)), Y) => X(Y) 
    abs(/\x.app(abs(/\y.X(y, x)), Y)) => app(abs(/\z.abs(/\u.X(z, u))), Y) 
    app(app(abs(/\x.X(x)), Y), Z) => app(abs(/\y.app(X(y), Z)), Y) 
    app(abs(/\x.app(abs(/\y.X(y, x)), Y)), Z) => app(abs(/\z.app(abs(/\u.X(z, u)), Z)), Y) 

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

  app(abs(/\x.app(abs(/\y.f y x), z)), u) 
    => app(abs(/\x.app(abs(/\y.f x y), u)), z) 
    => app(abs(/\x.app(abs(/\y.f y x), z)), u) 

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