syntactic simplifications sometime better than automata-based ones?
I would expect level 3 to be better than level 2.
% ltlfilt -f 'p0 U (F(p1 <-> Fp1) W Fp1)' --simplify=1
F(p1 | GF((p1 & Fp1) | (!p1 & G!p1)))
% ltlfilt -f 'p0 U (F(p1 <-> Fp1) W Fp1)' --simplify=2
1
% ltlfilt -f 'p0 U (F(p1 <-> Fp1) W Fp1)' --simplify=3
F(p1 | G!p1)