Check which rules can directly generate a clause
Currently a common pattern is to have a rule which generates a unit clause where the literal starts with an or
and to then directly use the or
rule to deconstruct the disjunctive.
We now emphasize the importance of clauses. Hence, we should probably eliminate this pattern and directly create clauses. There might also be some rules that create implications which are subsequently deconstructed into disjunctions.