This was discovered by playing with the online translator's random formulas.
The formula is p1 <-> !((X(p0 <-> Xp0) xor G(p1 & p2)) W Fp0), and the unambiguous version of the automaton is smaller.
p1 <-> !((X(p0 <-> Xp0) xor G(p1 & p2)) W Fp0)
It would be better to generate that unambiguous automaton right away.