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.