(VAR P Q x )
(RULES 
        and(P, forall()) -> forall()
        or(P, forall()) -> forall()
        and(forall(), P) -> forall()
        or(forall(), P) -> forall()
        not(forall()) -> exists()
        and(P, exists()) -> exists()
        or(P, exists()) -> exists()
        and(exists(), P) -> exists()
        or(exists(), P) -> exists()
        not(exists()) -> forall()
        
)