1 sort bitvec 1
2 input 1 @inp2
3 sort bitvec 8
4 sort bitvec 32
5 sort array 4 3
6 input 5 @arr6
7 input 5 @arr7
8 ite 5 2 6 7
9 eq 1 8 7
10 eq 1 6 7
11 or 1 -2 10
12 eq 1 9 11
13 eq 1 7 8
14 eq 1 11 13
15 or 1 -12 -14
16 constraint 15