1 sort bitvec 1
2 input 1 @inp2
3 const 1 0
4 eq 1 2 3
5 sort array 1 1
6 input 5 @arr6
7 input 1 6
8 input 5 @arr8
9 write 5 8 2 3
10 ite 5 7 9 8
11 eq 1 6 10
12 constraint 4
13 constraint 11