(VAR x y z)
(THEORY (AC +))
(RULES
+(f(a),g(b)) -> +(f(b),g(a))
k(a,g(g(a))) -> k(g(a),f(a))
+(g(x),y) -> g(+(x,y))
f(+(x,y)) -> +(f(x),y)
k(a,b) -> k(b,a)
k(g(a),a) -> k(a,g(b))
k(g(a),b) -> k(a,g(a))
)