Consider the given formulas S1 = [[a WU b] WU c] and S2 = [[a WU b] SU c]. First note that S2 implies S1, i.e., [[a WU b] SU c] -> [[a WU b] WU c] since the strong until implies the weak until. However, the converse implication, i.e., [[a WU b] WU c] -> [[a WU b] SU c] is not valid: As a counterexample, consider a path where we have G(a&!b&!c) such that [a WU b] and therefore also [[a WU b] WU c] hold from the initial point of time on. Since c never holds, [[a WU b] SU c] is however false which is the difference between weak and strong until.

The exercise wants you to determine two formulas (different to false) that show the difference between the two formulas, i.e., that imply S1&!S2. Your answer was "1 ; G a; G (a & b)" which means that you claim that the following should hold:

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

However, both implications are not valid: A counterexample for the first one is G(a&!b&c) since then (G a), [a WU b], [[a WU b] WU c], and [[a WU b] SU c] are all true from the beginning. A counterexample for the second implication is G(a&b&c) so that (G(a&b)), [a WU b], [[a WU b] WU c], and [[a WU b] SU c] are again all true from the beginning. Hence, both implications are false.

I guess that you have verified something else with the tool. What you need are two formulas that imply [[a WU b] WU c] & ![[a WU b] SU c], i.e., that satisfy [[a WU b] WU c], but not [[a WU b] SU c]. One of the two should be clear from what is written above. However, I should not give the complete solution to the exercise here, and leave the rest up to you.