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