We consider the system 513.

  Alphabet:

    all : [T -> F] --> F 
    and : [F * F] --> F 
    ex : [T -> F] --> F 
    not : [F] --> F 
    or : [F * F] --> F 

  Rules:

    and(X, all(/\x.Y(x))) => all(/\y.and(X, Y(y))) 
    and(all(/\x.X(x)), Y) => all(/\y.and(X(y), Y)) 
    or(X, all(/\x.Y(x))) => all(/\y.or(X, Y(y))) 
    or(all(/\x.X(x)), Y) => all(/\y.or(X(y), Y)) 
    and(X, ex(/\x.Y(x))) => ex(/\y.and(X, Y(y))) 
    and(ex(/\x.X(x)), Y) => ex(/\y.and(X(y), Y)) 
    or(X, ex(/\x.Y(x))) => ex(/\y.or(X, Y(y))) 
    or(ex(/\x.X(x)), Y) => ex(/\y.or(X(y), Y)) 
    not(all(/\x.X(x))) => ex(/\y.not(X(y))) 
    not(ex(/\x.X(x))) => all(/\y.not(X(y))) 
    and(X, Y) => and(Y, X) 
    or(X, Y) => or(Y, X) 

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

  and(x, all(/\y.f y)) 
    => and(all(/\y.f y), x) 
    => and(x, all(/\y.f y)) 

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