Implement aggressive pruning in CAD solver (#7650)

Implement aggressive pruning in CAD solver (#7650)

This PR implements a more aggressive pruning of redundant intervals, namely intervals that are covered by two other intervals, but not a single one. As already discussed in the respective paper, it is not entirely clear whether this is beneficial as removing such an interval may make the "overlap" smaller and thus the generated interval in the lower dimension may become smaller as well. It is thus only enabled via a (new) option.
Experiments show that such redundant intervals are relatively common (878 benchmarks on QF_NRA), the impact of this option is very limited and not strictly beneficial.