Cases where predicates evaluate to constant values are already detected and handled. But besides such trivial simplifications we should also try to handle more advanced simplification rules like:

• X || X => X
• X && X => X
• !X || !X => !X
• !X && !X => !X
• X || !X => TRUE (tautology)
• X && !X => FALSE (contradiction)
  (where X is a predicate not a general boolean expression)

Even further simplification could be achieved if we were able to handle the general case where X is a general boolean expression, but we'll not try that yet for the sake of complexity.