We consider the system 771.

  Alphabet:

    0 : [] --> nat 
    app : [nat -> nat * nat] --> nat 
    plus : [nat * nat] --> nat 
    s : [nat] --> nat 
    star : [nat * nat] --> nat 

  Rules:

    app(/\x.X(x), Y) => X(Y) 
    plus(X, 0) => X 
    plus(X, s(Y)) => s(plus(X, Y)) 
    plus(0, X) => X 
    plus(s(X), Y) => s(plus(X, Y)) 
    star(X, 0) => 0 
    star(X, s(Y)) => plus(star(X, Y), X) 
    star(0, X) => 0 
    star(s(X), Y) => plus(star(X, Y), Y) 
    plus(plus(X, Y), Z) => plus(X, plus(Y, Z)) 
    plus(X, Y) => plus(Y, X) 
    star(X, Y) => star(Y, X) 

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

  plus(x, 0) 
    => plus(0, x) 
    => plus(x, 0) 

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