Hmh, I see what you have done and you will be annoyed when you will realize what is wrong: As you want to show that S1&!S2 is satisfiable, you tried a proof for S1->S2 and got the following counterexample for (X c & F b) -> (X c & G b):

You described it with the formula

phi1 = !b&!c & G( (!b&!c <-> X b&c) & !a)

but it should be rather (I come back to this later):

phi1 = !b&!c & G((!b&!c <-> X(b&c)) & !a)

To generate another formula phi2, you tried a proof of !phi1 & S1 -> S2, i.e.,

!(!b&!c & G( (!b&!c <-> X b&c) & !a)) & (X c & F b) -> (X c & G b)

which gave you

which you described as

phi2 = !a&!b&!c & (G(!a&!b&!c <-> X (a&b&c)))

That far that good, now let's check what is wrong.

As already remarked above, you made a mistake in phi1 since you forgot brackets. Your formula phi1 is not satisfiable, since

!b&!c & G( (!b&!c <-> X b&c) & !a)
= !b&!c & G( (!b&!c <-> (X b) & c) & !a)
= !b&!c & (G(!b&!c <-> (X b) & c)) & G(!a)
= !b&!c & (G(c? (!X b) : b)) & G(!a)
= !b&!c & (c? (!X b) : b) & X(G(c? (!X b) : b)) & G(!a)
= !b&!c & b & X(G(c? (!X b) : b)) & G(!a)
= false

You can check this also with the LTL prover by checking that the negation !phi1 of your formula phi1 is valid.

Since phi1 is false, the implications phi1 -> ... are trivially true, and the tool does not accept them (the exercise forbids to use a phi1 that is false because that would be as trivial as S1&!S2).