#DECLARATION
init deadlock elected
#END
0 init
2595 elected
2596 elected
2599 elected
2969 elected