Local model checking is a top-down procedure which means that the question whether s5 satisfies !b, i.e., the sequent s5 |- !b is reduced to the question whether s5 satisfies b, i.e., s5 |- b. Once propositional variables are found on the right hand side, we can check the truth value by considering the label of state s5. In this case, s5 is labeled with b, so b holds in s5, and therefore, we have s5 |- b. For this reason, we do not have s5 |- !b and neither do we have s5 |- a&!b, so this result propagates upwards the tree.
About the selection of s4 for the subgoal: That was a matter of luck, the tool stops when the first subgoal of a disjunctive split is satisfied.
