(VAR x y xs)
(THEORY (AC plus))
(RULES
  sum(x, y) -> S(int(x, y))
  S(nil) -> 0
  S(cons(x, xs)) -> plus(x, S(xs))
  plus(x, 0) -> x
  plus(x, s(y)) -> s(plus(x, y))
  int(0, 0) -> cons(0, nil)
  int(0, s(y)) -> cons(0, int(s(0), s(y)))
  int(s(x), 0) -> nil
  int(s(x), s(y)) -> intlist(int(x, y))
  intlist(nil) -> nil
  intlist(cons(x, y)) -> cons(s(x), intlist(y))
)