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