YES
(THEORY
    (AC
        and or
    )
    
)
(VAR
    x2 x3 x1 x y z
)
(RULES
    or(and(x2,x3),x1) -> and(or(x1
                               ,x2)
                            ,or(x1,x3))
    not(and(x,y)) -> and(not(x)
                        ,not(y))
    not(not(x)) -> x
    not(or(x,y)) -> or(not(x)
                      ,not(y))
    or(x,and(y,z)) -> and(or(x,y)
                         ,or(x,z))
)