I am still not quite sure about how it works.
1. How do we choose the variable to be resolved? That is, how do we know which
inequalities are to be summed?
2. When can we be sure that no more conflicts can be introduced by resolution?
It seems that the order that we conduct resolution operations can affect
the slack. Is this true? And if so, when can we stop the process?