YES
(THEORY
    (AC
        p
    )
    
)
(VAR
    x y x1
)
(RULES
    f(p(x,y)) -> p(f(x),f(y))
    p(x,zero()) -> x
    f(zero()) -> zero()
    p(zero(),x1) -> x1
)