The solution of local model checking is not unique, since there are AND and OR rules. For the OR rules, it is sufficient to choose one subgoal for proving the formula, and for the AND rules it is sufficient to choose one subgoal for disproving the formula. Depending on these choices, we may get different solutions. Apart from that, you may also choose one of the initial states to disprove the formula.