UNCONSPROP
(d1, d2, d3, d4, d5, d6, a)
CONSPROP
(p1,r1,i1, p2,r2,i2, p3,r3,i3, p4,r4,i4, p5,r5,i5, p6,r6,i6,g1, g2, g3, g4, g5, g6)
CONSTRAINT
(< 6)+(p1, p2, p3, p4, p5, p6)
(= 1)+(p1, r1,i1)
(= 1)+(p2, r2,i2)
(= 1)+(p3, r3,i3)
(= 1)+(p4, r4,i4)
(= 1)+(p5, r5,i5)
(= 1)+(p6, r6,i6)
(< 4)+(r1, r2, r3, r4, r5, r6, i1, i2, i3, i4, i5, i6)
(< 2)+(g1, g2, g3, g4, g5, g6)
INIT
(p1)
(p2)
(p3)
(p4)
(p5)
(r6)
(!g1 | p1)
(!g2 | p2)
(!g3 | p3)
(!g4 | p4)
(!g5 | p5)
(!g6 | p6)
(!a | i1)
(!a | i2)
(!a | i3)
(!a | i4)
(!a | i5)
(!a | i6)
(!d1 | p1 | i1)
(!d2 | p2 | i2)
(!d3 | p3 | i3)
(!d4 | p4 | i4)
(!d5 | p5 | i5)
(!d6 | p6 | i6)
STEP
true => X(!d1 | p1 | i1)
true => X(!d2 | p2 | i2)
true => X(!d3 | p3 | i3)
true => X(!d4 | p4 | i4)
true => X(!d5 | p5 | i5)
true => X(!d6 | p6 | i6)
(r1) => X(p1 | r1)
(r2) => X(p2 | r2) 
(r3) => X(p3 | r3)
(r4) => X(p4 | r4)
(r5) => X(p5 | r5)
(r6) => X(p6 | r6)
(i1) => X(i1)
(i2) => X(i2)
(i3) => X(i3)
(i4) => X(i4)
(i5) => X(i5)
(i6) => X(i6)
true  => X(!g1 | p1)
true  => X(!g2 | p2)
true  => X(!g3 | p3)
true  => X(!g4 | p4)
true  => X(!g5 | p5)
true  => X(!g6 | p6)
true => X(!a | i1)
true => X(!a | i2)
true => X(!a | i3)
true => X(!a | i4)
true => X(!a | i5)
true => X(!a | i6)
EVENTUALITY
F(d1)
F(d2)
F(d3)
F(d4)
F(d5)
F(d6)
F(a)
END