Faster Conversion to Normal Forms

You might be more specific here. There are many ways that a clause can be redundant. Does this just remove clauses that are always false, or does it do more? For instance, if you have `x | y` as a clause, then `x | y | z` is redundant via propagation. I don't actually think this should worry about those cases, as that's better suited for the SAT solver, but it should be clear in the docstring what you mean.