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