(VAR X)
(RULES

f(a,a) -> f(a,b)
f(a,b) -> f(s(a),c)
f(s(X),c) -> f(X,c)
f(c,c) -> f(a,a)

)