I don't think that the path satisfies S1: To simplify matters, we may write (a<->b) as ¬(a⨁b), so that S1 becomes ¬XX(G(a⨁b)⨁F¬(a⨁b)) and moreover equivalent to ¬XX(G(a⨁b)⨁¬G(a⨁b)). If you now abbreviate G(a⨁b) as p, the formula becomes ¬XX(p⨁¬p) and since p⨁¬p holds for any p, it is simply true. Hence, it follows that S1 is simply false on every path.
The path does also not satisfy S2, so it does not distinguish between these two formulas. You can quickly check this with the online tool using the following:
(¬a&¬b) & X(¬a&¬b) & X X G(a&b) -> X X G((a⊕X a)&(b⊕X X b))
To distinguish between the two formulas, we therefore need a path that satisfies S2. Obviously, this path must satisfy after two steps G((a⊕X a)&(b⊕X X b)) and that means that a always alternates between true and false, and b does the same but with a period of 2.
For instance, the following will satisfy S2, but not S2:
