1 sort bitvec 8
2 sort array 1 1
3 input 2 @arr3
4 input 2 @arr4
5 input 2 @arr5
6 sort bitvec 1
7 input 6 @inp7
8 input 1 @inp8
9 ite 2 -7 4 5
10 read 1 5 8
11 read 1 9 8
12 neq 6 10 11
13 and 6 7 12
14 constraint 13