begin

@ n1 -<>n1;
@ n1 <>true;
@ n1 [][] down x1 . @ n1 <> x1;
@ n1 [] down x1 . [] down x2 . @ x1 [] down x3 .@ x1 [] down x4 . ((@ x2 x3 ) v (@ x2 x4) v (@ x3 x4));
@ n1 [] down x1 . [][] down x2 . @ x1 [][] down x3 . @ x1 [][] down x4 . @ x1 [][] down x5 . ((@ x2 x3) v (@ x2 x4) v (@ x2 x5) v (@ x3 x4) v (@ x3 x5) v (@ x4 x5))

end