(VAR x y z)
(THEORY (AC plus times))
(RULES
  plus(x, 0) -> x
  plus(x, s(y)) -> s(plus(x, y))
  plus(x, plus(s(y), z)) -> plus(s(plus(x, y)), z)
  times(x, 0) -> 0
  times(x, times(0, z)) -> times(0, z)
  times(x, s(y)) -> plus(times(x, y), x)
  times(x, times(s(y), z)) -> times(plus(times(x, y), x), z)
)