For given LTL formulas S1 and S2, you have to find two satisfiable formulas phi1 and phi2 which are not equivalent that one of the following holds:

(1) phi1->S1&!S2 and phi2->S1&!S2
(2) phi1->!S1&S2 and phi2->!S1&S2

To indicate which of the above cases you mean, you have to enter either one of the following two lines with the right formulas phi1 and phi2:

1; phi1 ; phi2
2; phi1 ; phi2

So, you have to give two nontrivial counterexamples to either S1->S2 or to S2->S1.

Now consider your particular task: Your formulas are S1 := [c WU [a WU b]] and S2 := [c WU [a SU b]].

Checking S2->S1, i.e., [c WU [a SU b]] -> [c WU [a WU b]] by the LTL prover shows that this implication is valid. Hence, !S1&S2 is unsatisfiable and we can therefore not use case 2.

So, we have to find formulas phi1 and phi2 that satisfy phi1->S1&!S2 and phi2->S1&!S2. Checking S1->S2, i.e., [c WU [a WU b]] -> [c WU [a SU b]] with the tool shows us that this implication is not valid.

You tried as an answer 1 ; G(a) ; G(!b) which was wrong. Why is that so? Well, check whether the following formulas are valid:

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

But none of them are valid! You have to find other formulas that will meet the requirements. If you look at the counterexample that is generated by the LTL prover, you can see that it is a path where (G(a&!b&!c)) holds.

Hence, (G(a&!b&!c)) is such a candidate formula, while the two you tried do not meet the requirements. It is up to you to find a second one.