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