1 sort bitvec 1
2 input 1 turn
3 state 1 state0
4 state 1 state1
5 ite 1 -2 -3 3
6 ite 1 2 -4 4
7 next 1 3 5
8 next 1 4 6
9 eq 1 3 4
10 one 1
11 state 1 initially
12 init 1 11 10
13 zero 1
14 next 1 11 13
15 implies 1 11 -9
16 constraint 15
17 bad 9