a curious case of smaller "unambiguous" automaton
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.
It would be better to generate that unambiguous automaton right away.