(VAR x1 x2 x3 x4 )
(THEORY (AC f))
(RULES 
 f(h(x1),f(h(a), g(a))) -> h(x1)
 f(g(x1),f(h(a), g(a))) -> g(x1)
 f(a,x1)  ->  f(h(x1),h(a))
 f(a,x1)  ->  f(g(x1),g(a))
 f(g(x2),h(x1)) -> f(g(x1),h(x2))
)