[true SU a] is not equivalent to (F a) | (G a), instead it is equivalent to F a only, and therefore no G(a⊕b) is generated at all. The solution could also be as follows:

¬E(X X X G F G F ¬([true SU (a ⊕ b)]))

<-> ¬E(X X X G F G F ¬F (a ⊕ b))

<-> ¬E(X X X G F G F G ¬(a ⊕ b))

<-> ¬E(X X X F G ¬(a ⊕ b))

<-> ¬E(F G ¬(a ⊕ b))

<-> A G F (a ⊕ b)

<-> A G A F (a ⊕ b)