implement a strategy that prioritizes sequents with fewer branches first

[salmans]

The strategy would process sequents with fewer branches on right first:

• failing sequents (with bottom on right) will fail first
• sequents that clone the model will fail last