(VAR x y)
(THEORY (AC plus times))
(RULES
  0(S) -> S
  plus(S, x) -> x
  plus(0(x), 0(y)) -> 0(plus(x, y))
  plus(0(x), 1(y)) -> 1(plus(x, y))
  plus(1(x), 1(y)) -> 0(plus(x, plus(y, 1(S))))
  times(S, x) -> S
  times(0(x), y) -> 0(times(x, y))
  times(1(x), y) -> plus(0(times(x, y)), y)
)