Important to note, in practice, the given rewrite rules are not how we put an expression into DNF when doing SAT, since they can exponentially blow up the expression. Instead we use a different set of rewrites which add new variables which stand in for subexpressions of the original formula