We consider the system 456.

  Alphabet:

    0 : [] --> term 
    Y : [] --> term 
    abs : [term -> term] --> term 
    app : [term * term] --> term 
    ff : [] --> term 
    if : [] --> term 
    iszero : [] --> term 
    pred : [] --> term 
    s : [term] --> term 
    succ : [] --> term 
    tt : [] --> term 

  Rules:

    app(succ, X) => s(X) 
    app(pred, s(X)) => X 
    app(iszero, 0) => tt 
    app(iszero, s(X)) => ff 
    app(app(app(if, tt), X), Z) => X 
    app(app(app(if, ff), X), Z) => Z 
    app(abs(/\x.X(x)), Z) => X(Z) 
    app(Y, X) => app(X, app(Y, X)) 

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

  app(Y, x) 
    => app(x, app(Y, x)) 
    |> app(Y, x) 

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