Well, have a look at https://q2a.cs.uni-kl.de/2418/exercize-8-problem-1-b.

Simply adapt that to your problem: Given formulas S1=[b SU [c WU a]] and S2=[b SU [c SU a]], we first check whether the one implies the other one.

The tool quickly tells us that [b SU [c SU a]] -> [b SU [c WU a]] is valid, while we get a counterexample for [b SU [c WU a]] -> [b SU [c SU a]] so that S1&!S2 is satisfiable. That counterexample consists of an infinite path where G(!a&!b&c) holds. Hence, we know that the following are valid:

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

which is also easily seen with the semantics of the LTL operators. Hence, we already have a first formula to distinguish between the two formulas, namely G(!a&!b&c).

To find a second one, we ask the tool whether this is the only counterexample in that we let the tool check the following

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

A counterexamle would satisfy !G(!a&!b&c) & [b SU [c WU a]] & ![b SU [c SU a]]. The tools gives a counterexample which is an infinite path where G(!a&b&c) holds. So, we have a second counterexample.

So, since S1&!S2 is satisfiable, we have case 1 mentioned in the exercise, so that your answer could be

1; G(!a&!b&c); G(!a&b&c)

Right?