Please repeat the question of the exercise sheet so that also students of later semesters can understand what we are discussing here. The question is that for a given LTL formulas S1 and S2, we should construct two LTL formulas φ1 and φ2 that satisfy the following requirements:

- φ1 and φ2 are not equivalent
- φ1 and φ2 are both satisfiable
- either φ1->S1&!S2 and φ2->S1&!S2 or φ1->!S1&S2 and φ2->!S1&S2are valid

For the given formulas S1=[b WU [c WU a]] and S2=[b WU [c SU a]], you believe that [b WU [c WU a]] -> [b WU [c SU a]] would be valid, but that is not true. A counterexample is a single path where always !a&!b&c holds which obviously satisfies S1 but not S2. Note that [c WU a] holds here at every point of time, so that [b WU [c WU a]] is true at time 0, but [c SU a] is always false, and since b is also always false, S2 is false at initial time.

The formulas you suggest as a solution are φ1=G(!b&!a&c) and φ2=(!a&!b&c) & X(!a&b&c) & G(!b&!a&c). Formula φ1 holds exactly on the counterexample that I discussed above, so that the following is indeed valid:

G(!b&!a&c) -> [b WU [c WU a]] & ![b WU [c SU a]]

Also φ2->S1&!S2, i.e., the following formula is valid

(!a&!b&c) & X(!a&b&c) & G(!b&!a&c) -> [b WU [c WU a]] & ![b WU [c SU a]]

However, the above is valid since φ2 is not satisfiable: If G(!b&!a&c) holds at initial time, then also X(!b&!a&c) must hold which contradicts X(!a&b&c).

I guess you mean (!a&!b&c) & X((!a&b&c) & G(!b&!a&c)) as formula φ2, right?