Strahler of tree like refutations
You have asked (at least) two questions. The answer to your first question is that sometimes it is much easier to refute a formula given that $x=0$ compared to given $x=1$. Hence the $\max$. In other cases, $x=1$ is easier. That's why we need to go over both possible values of $b$. Finally, the reason why the formula in part 3 of the lemma also maximizes over the variable $x$ is that $x$ represents the last variable which is cut (the one at the root of the tree).

The answer to your second question is as follows. The cut rule allows deriving $a \lor b$ given $a \lor x$ and $b \lor \bar{x}$. Here $a,b$ are arbitrary formulas, in this context clauses. In particular, from $x$ and $\bar{x}$ you can conclude contradiction. The cut rule is the only rule in the resolution proof system.