(VAR x y z)
(RULES
  Ap(Ap(Ap(S,x),y),z) -> Ap(Ap(x,z),Ap(y,z))
  Ap(Ap(K,x),y) -> x
  Ap(I,x) -> x
  Ap(Ap(Ap(B,true),x),y) -> x
  Ap(Ap(Ap(B,false),x),y) -> y
  Ap(Ap(Ap(B,z),x),x) -> x
)
(COMMENT from p.209 of \cite{Klop80})