begin
(p1 <--> p2) & (p3 <--> p4) v (p5 <--> p6) v (p6<-->p7);
[](!p1 & !p2 & !p3 & !p4 & !p5 & !p6 & !p7);
<>(n1:p1) & <>(n2:p2) & <>(n3:p3) & <>(n4:p4) & <>(n5:p5) & <>(n6:p6) & <>(n7:p7);
<><>(n1:p1) & <><>(n2:p2) & <><>(n3:p3) & <><>(n4:p4) & <><>(n5:p5) & <><>(n6:p6) &
<><>(n7:p7);
n1:n2 & n2:n3 & n3:n4 & n4:n5 & n5:n6 & n6:n7 
end