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