Clarify and restrict resolution rules

Currently, we say that resolution steps are arbitrary. Reconstructing such n-ary resolution steps is theoretically hard. The real resolution steps, however, are somewhat ordered. Often from left to right as the resolution is applied.

This is especially the case for cvc5, which guarantees a certain order and can also provide additional hints.

We should go through the source code of veriT and understand how resolution steps are generated. th_resolution is often generated by "hand". Such steps might need adjustment.

Furthermore, there are some resolution rules that could be improved. Sometimes there are steps where no resolution happens (see comments), or some premises are unused.