Sort resolvents, biggest first

If they subsume each other, adding the biggest first is the best: later,
the smaller ones can subsume the larger ones.