(VAR x y) (THEORY (AC plus)) (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)) -> j(plus(x,plus(y, one(sharp)))) plus(zero(x), j(y)) -> j(plus(x,y)) plus(j(x), one(y)) -> zero(plus(x,y)) plus(j(x), j(y)) -> one(plus(x,plus(y, j(sharp)))) )