Introduce new splitting inference in sets + cardinality (#8290)

Introduce new splitting inference in sets + cardinality (#8290)

Fixes cvc5/cvc5-projects#486.

This introduces a new strategy which splits on whether Venn regions are equal to each other before it splits them into sub-Venn regions.

The issue in the above was caused by a case where the sets solver decided to make 2 Venn regions of the same equivalence class disjoint. By splitting on their equality first, this should introduce the necessary information to discover this is a conflict (via disequality witnessing). It should also be more efficient since we introduce new set terms lazier.