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))
    add(c(x,xs),nil()) -> p(x
                           ,add(xs,nil()))
    p(x,s(y)) -> s(p(x,y))
    p(zero(),x1) -> x1
    p(x,zero()) -> x
    add(nil(),nil()) -> zero()
    p(s(x2),x1) -> s(p(x1,x2))
    add(nil(),c(y,ys)) -> p(y
                           ,add(nil(),ys))
)