Case 2 means that !S1&S2 will be implied, but we have S1->S2, i.e., [b SB [a WB c]] -> [b WB [a WB c]] is valid. Hence, you should better go for case 1.
For case 1, G (!b & !a &c) is good.
Your second formula is however equivalent to false: G(!b&!a) contradicts to X a.