(VAR x y xs ys)
(THEORY (AC p))
(RULES
p(x,zero) -> x
p(x,s(y)) -> s(p(x,y))
add(nil,nil) -> zero
add(c(x,xs),nil) -> p(x,add(xs,nil))
add(nil,c(y,ys)) -> p(y,add(nil,ys))
add(c(x,xs),c(y,ys)) -> p(p(x,y),add(xs,ys))
append(nil,ys) -> ys
append(c(x,xs),ys) -> c(x,append(xs,ys))
rev(nil) -> nil
rev(c(x,xs)) -> append(rev(xs),c(x,nil))
rev(rev(xs)) -> xs
)