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