Okay, let's clarify. We have the formulas S1 := [[b SB a] WB c] and S2 := [[b WB a] WB c]. Using the LTL prover, we find out that S1->S2 holds, but S2->S1 does not hold. For the latter, we obtain a counterexample that demonstrates that !S1&S2, i.e., that ![[b SB a] WB c] & [[b WB a] WB c] holds.
The counterexample has initially all variables false, and then a self-loop in a state where !a&!b&c holds. Hence, if [alpha WB c] should hold initially for some formula alpha, it must be the case that alpha must hold initially, since at the next point of time already c holds, and it is therefore too late for alpha. Initially, we have [b WB a] since a and b are always false, but we do not have [b SB a] since the strong before demands that b eventually holds which is however not the case.
Looking at the counterexample, I think a suitable phi1 should be (!a&!b&!c) & X G(!a&!b&c). We can also check that (!a&!b&!c) & X G(!a&!b&c) -> ![[b SB a] WB c] & [[b WB a] WB c] holds.
The formula phi1 that has been used above, i.e., G((!a&!b&c)& X(!a&b&c)) contradicts itself, since it says in particular that b should be false at all points of time, and b should hold at all points of time t>0 which is impossible. Thus, that phi1 is equivalent to false, and that is the reason why you can also prove phi1->S1&!S2 with it (which is equivalent to false->false). The student portal will however not accept that solution since it will check that your formulas phi1 and phi2 are not equivalent to false.
Finally, let's consider your phi2 := (!a&!b&!c) & G X(!a&!b&c) which describes the counterexample discussed above. You say that (!a&!b&!c) & G(X(!a&!b&c))-> [[b SB a] WB c]& ![[b WB a] WB c] is not valid which is true, but we have to check that (!a&!b&!c) & G(X(!a&!b&c))-> ![[b SB a] WB c] & [[b WB a] WB c] which is true. Note that we have to find examples for !S1&S2 since there are no examples for S1&!S2 (since we checked that S1->S2 holds).
Hence, you proved phi1->S1&!S2 with a formula phi1 equivalent to false (which is pointless), and could not prove phi2->S1&!S2 since the latter cannot be proved with a formula different to false. Instead, you should prove phi1->!S1&S2 and phi2->!S1&S2 which will work for your phi2. It does also work for your phi1, but just because it is false and that is not allowed.
Still confused?