I checked your two formulas and the second one is not correct. We can prove that

(G(a & !b & !c)) -> [[b WB a] WB c] & ![[b WB a] SB c]

is valid, but (G(!b & !c) & X(a)) -> [[b WB a] WB c] & ![[b WB a] SB c] is not valid.

To find your formulas, I suggest to first disprove [[b WB a] WB c] -> [[b WB a] SB c] so that the tool gives you a counterexample that satisfies [[b WB a] WB c] & ![[b WB a] SB c]. When I do that, I obtain a single path that is described by your first formula G(a & !b & !c).

To find the second formula, try a proof for !(G(a & !b & !c)) & [[b WB a] WB c] -> [[b WB a] SB c]. Since that is not valid, a counterexample will satisfy !(G(a & !b & !c)) & [[b WB a] WB c] & ![[b WB a] SB c] and will give you a second formula.