bself: pick only the "biggest" overapproximations

From the overapproximations, use only those that has the most models
and at least some models are distinct.