We consider the system 759.

  Alphabet:

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

  Rules:

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

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

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

That is, a term reduces to itself.