We consider the system 432.

  Alphabet:

    abs : [T -> T] --> T 
    app : [T * T] --> T 
    p1 : [T] --> T 
    p2 : [T] --> T 
    pair : [T * T] --> T 

  Rules:

    app(abs(/\x.X(x)), Y) => X(Y) 
    p1(pair(X, Y)) => X 
    p2(pair(X, Y)) => Y 
    pair(p1(X), p2(X)) => X 

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.