- \item Idea: Add aditional information when considering second
- alternative of an or: ${\phi \vee \psi}$ becomes ${\phi \vee
- (¬\phi \wedge \psi)}$
- \item Do not reexplore branches already known to be unsat already
+ \item Idea: Add additional information when considering second
+ alternative of a disjunction: ${\phi \vee \psi}$ becomes ${\phi
+ \vee (¬\phi \wedge \psi)}$
+ \item Do not re-explore branches already known to be unsatisfiable already