(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(Dk,z),z) -> Ap(E,z)
)
(COMMENT from p.208 of \cite{Klo80})