A first counterexample is G(!a&b&!c) which is generated by the LTL teaching tool when we try to prove [c WU [b WU a]] -> [c WU [b SU a]].
Why is that so? If c is initially false, then [c WU [b WU a]] can only be satisfied when the condition [b WU a] is already initially true, and same way we must have that [b SU a] is initially false. That is the case when all the time b holds but never a holds which is exactly the difference between the weak and the strong operator. This is your first formula.
Looking at your second formula, I guess your idea was to delay the first counterexample by one point of time to create a second example. To this end, you demand X G(!a&b&!c) and also F c which is then equivalent to c. However, trying to prove
(F c) & X G(!a&b&!c) -> [c WU [b WU a]] & ![c WU [b SU a]]
gives as us another counterexmaple where initially a=c=1 and b=0 holds and from the next point of time on, we have a=c=0 and b=1. Thus, we initially have (F c) & X G(!a&b&!c) while the until formulas reduce as follows
[c WU [b WU a]] = [b WU a] | c & X[c WU [b WU a]]
= a | b & X[b WU a] | c & X[c WU [b WU a]]
and since initially a=c=1 and b=0 holds, we have initially
[c WU [b WU a]] = 1 and also [c WU [b SU a]] = 1
So, that is why your second formula does not work (the above counterexample makes both S1 and S2 true while satisfying also your constraint).
Can we make your idea work, i.e., postpone the problem by one point of time? Looking at the above unrolled formula, we would have to have at the initial point a=b=0 and c=1 to achieve that [c WU [b WU a]] = X[c WU [b WU a]]. So, you should better try
(!a&!b&c) & X G(!a&b&!c) -> [c WU [b WU a]] & ![c WU [b SU a]]
which encodes your idea above (if I understand it right). That will work.
How can we find another example? As usual, I suggest to prove [c WU [b WU a]] -> [c WU [b SU a]] under the additional assumption that excludes the current counterexample, i.e., !(G(!a&b&!c)) & [c WU [b WU a]] -> [c WU [b SU a]]. If you try that with the LTL prover in the teaching tools, you will obtain a path where !a&b&!c and !a&b&c are alternating. I leave it up to you to describe that as an LTL formula.
