(VAR x y)
(THEORY (AC plus) (AC mult))
(RULES
zero(sharp) -> sharp
plus(x, sharp) -> x
plus(zero(x), zero(y)) -> zero(plus(x,y))
plus(zero(x), one(y)) -> one(plus(x,y))
plus(one(x), one(y)) -> zero(plus(x,plus(y, one(sharp))))
mult(x, sharp) -> sharp
mult(zero(x), y) -> zero(mult(x, y))
mult(one(x), y) -> plus(zero(mult(x, y)), y)
)