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 6 @inp8 9 input 1 @inp9 10 ite 2 -7 3 4 11 ite 2 -8 3 5 12 read 1 10 9 13 read 1 11 9 14 neq 6 12 13 15 and 6 -7 -8 16 and 6 14 15 17 constraint 16