CONSPROP
(p1, p2,  p4, p5,  p7, p8)
UNCONSPROP
(p0,p3,p6,p9)
CONSTRAINT
(= 1)+(p1,p2,p4)
(= 1)+(p4,p5,p7)
(= 1)+(p7,p8,p1)
INIT
(p5 | p3 | p7 | p4 | !p6)
(!p7 | p8 | !p9 | !p2 | p3)
(p0 | !p4 | p9 | !p1 | !p3)
(!p0 | !p6 | !p2)
(!p2 | !p8 | p0)
(p0 | p3 | !p2 | !p1 | !p9)
(p3 | p9 | p0 | p6 | p4)
(!p0 | p6 | !p8 | p2 | p3)
(p5 | !p2 | p9)
(p9 | p7 | !p1 | !p2)
STEP
(p5 & !p4 & p6) => X(!p6 | !p2)
(!p1) => X(!p6 | p9 | p3)
(!p8) => X(!p6 | !p8)
(!p5 & !p4 & !p9) => X(p0)
(p2 & !p6 & p0 & p8) => X(!p0)
(!p8 & p1) => X(!p8 | p1 | p4)
(p7 & !p8) => X(p6 | p9 | !p2)
(true) => X(p3 | p7)
(!p7 & !p9 & !p4 & p1) => X(!p0)
(!p1 & p9 & !p8) => X(!p7 | !p9)
(p5 & !p4 & !p1) => X(!p2 | p3)
(!p2 & p7 & p4 & !p8) => X(p5)
(!p4 & p6) => X(p1 | !p6 | !p3)
(!p5 & p1 & !p2) => X(!p3)
(!p3 & p4) => X(!p5 | !p7 | !p9)
(p1 & p0) => X(!p5 | p3 | !p9)
(p5 & p8) => X(p2)
(!p1 & p2) => X(!p9)
(p3 & p6 & !p2 & p1) => X(p5)
(!p7 & p1) => X(!p4 | p2 | !p5)
EVENTUALITY
F(!p7)
F(p3)
F(!p2)
F(p9)
F(p6)
END