simplifier
elimination
nonsplitting cut
use patterns
Quantifier closing
weak cut
if-then-else split
pl case distinction
Quantifier
