(VAR x y z)
(RULES
f(f(f(a,x),y),z) -> f(f(x,z),f(y,z))
f(f(b,x),y) -> x
f(c,y) -> y
)
(COMMENT Example 4.40 (Combinatory Logic) in \cite{SK90}) 
(COMMENT This TRS is not terminating!)