[](!p0)
<>p1 -> (!p0 U p1)
[](p2 -> [](!p0))
[]((p2 & !p1 & <>p1) -> (!p0 U p1))
[](p2 & !p1 -> (!p0 U (p1 | []!p0)))
<>(p0)
!p1 U ((p0 & !p1) | []!p1)
[](!p2) | <>(p2 & <>p0)
[](p2 & !p1 -> (!p1 U ((p0 & !p1) | []!p1)))
[](p2 & !p1 -> (!p1 U (p0 & !p1)))
<>p1 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1)))))))))
[]((p2 & <>p1) -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1))))))))))
[](p2 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U (p1 | []!p0)) | []p0)))))))))
[](p0)
<>p1 -> (p0 U p1)
[](p2 -> [](p0))
[]((p2 & !p1 & <>p1) -> (p0 U p1))
[](p2 & !p1 -> (p0 U (p1 | [] p0)))
!p0 U (p3 | []!p0)
<>p1 -> (!p0 U (p3 | p1))
[]!p2 | <>(p2 & (!p0 U (p3 | []!p0)))
[]((p2 & !p1 & <>p1) -> (!p0 U (p3 | p1)))
[](p2 & !p1 -> (!p0 U ((p3 | p1) | []!p0)))
[](p0 -> <>p3)
<>p1 -> (p0 -> (!p1 U (p3 & !p1))) U p1
[](p2 -> [](p0 -> <>p3))
[]((p2 & !p1 & <>p1) -> (p0 -> (!p1 U (p3 & !p1))) U p1)
[](p2 & !p1 -> ((p0 -> (!p1 U (p3 & !p1))) U (p1 | [](p0 -> (!p1 U (p3 & !p1))))))
<>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))
<>p1 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))
([]!p2) | (!p2 U (p2 & <>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))))
[]((p2 & <>p1) -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))))
[](p2 -> (<>p0 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))))
(<>(p3 & X<>p4)) -> ((!p3) U p0)
<>p1 -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0))
([]!p2) | ((!p2) U (p2 & ((<>(p3 & X<>p4)) -> ((!p3) U p0))))
[]((p2 & <>p1) -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0)))
[](p2 -> (!(p3 & (!p1) & X(!p1 U (p4 & !p1))) U (p1 | p0) | [](!(p3 & X<>p4))))
[] (p3 & X<> p4 -> X(<>(p4 & <> p0)))
<>p1 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1
[] (p2 -> [] (p3 & X<> p4 -> X(!p4 U (p4 & <> p0))))
[] ((p2 & <>p1) -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1)
[] (p2 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U (p1 | [] (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0)))))
[] (p0 -> <>(p3 & X<>p4))
<>p1 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1
[] (p2 -> [] (p0 -> (p3 & X<> p4)))
[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1)
[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U (p1 | [] (p0 -> (p3 & X<> p4))))
[] (p0 -> <>(p3 & !p5 & X(!p5 U p4)))
<>p1 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1
[] (p2 -> [] (p0 -> (p3 & !p5 & X(!p5 U p4))))
[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1)
[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U (p1 | [] (p0 -> (p3 & !p5 & X(!p5 U p4)))))
!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0)
<>p2 -> (!p2 U (p2 & (!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0))))
p0 U p1
p0 U (p1 U p2)
!p0 R (!p1 R !p2)
(1 U (0 R !p0)) | (0 R (1 U p1))
(1 U p0) U (0 R p1)
(0 R p0) U p1
(1 U p0) & (1 U (1 U p0)) & (0 R !p0) & (0 R (0 R !p0))
(0 R (1 U p0)) & (1 U (0 R !p1))
((0 R (1 U p0)) & (1 U (0 R !p1))) | ((0 R (1 U p1)) & (1 U (0 R !p0)))
p0 R (p0 | p1)
(Xp0 U Xp1) | X(!p0 R !p1)
(Xp0 U p1) | X(!p0 R (!p0 | !p1))
(0 R (!p0 | (1 U p1))) & ((Xp0 U p1) | X(!p0 R (!p0 | !p1)))
(0 R (!p0 | (1 U p1))) & ((Xp0 U Xp1) | X(!p0 R !p1))
0 R (!p0 | (1 U p1))
1 U (p0 & X(!p1 U !p2))
(1 U (0 R !p0)) & (0 R (1 U !p1))
0 R ((1 U p0) & (1 U p1))
(1 U p0) & (1 U !p0)
(Xp1 & p2) R X(((p3 U p0) R p2) U (p3 R p2))
((0 R (p1 | (0 R (1 U p0)))) & (0 R (p2 | (0 R (1 U !p0))))) | (0 R p1) | (0 R p2)
((0 R (p1 | (1 U (0 R p0)))) & (0 R (p2 | (1 U (0 R !p0))))) | (0 R p1) | (0 R p2)
(0 R (p1 | X(0 R p0))) & (0 R (p2 | X(0 R !p0)))
0 R (p1 | (Xp0 & X!p0))
p0 | (p1 U p0)
p0 U (p1 & (0 R p2))
p0 U (p1 & X(p2 U p3))
p0 U (p1 & X(p2 & (1 U (p3 & X(1 U (p4 & X(1 U (p5 & X(1 U p6)))))))))
1 U (p0 & X(0 R p1))
1 U (p0 & X(p1 & X(1 U p2)))
1 U (p0 & X(p1 U p2))
(1 U (0 R p0)) | (1 U (0 R p1))
0 R (!p0 | (p1 U p2))
1 U (p0 & X(1 U (p1 & X(1 U (p2 & X(1 U p3))))))
(0 R (1 U p0)) & (0 R (1 U p1)) & (0 R (1 U p2)) & (0 R (1 U p3)) & (0 R (1 U p4))
(p0 U (p1 U p2)) | (p1 U (p2 U p0)) | (p2 U (p0 U p1))
0 R (!p0 | (p1 U ((0 R p2) | (0 R p3))))