We consider the system 465.

  Alphabet:

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

  Rules:

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

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

  app(abs(/\x.app(x, x)), abs(/\y.app(y, y))) 
    => (/\x.app(x, x)) abs(/\y.app(y, y)) 
    =>_beta app(abs(/\x.app(x, x)), abs(/\y.app(y, y))) 

That is, a term reduces to itself.