1 sort bitvec 1 2 sort array 1 1 3 input 2 @arr3 4 input 2 @arr4 5 input 1 @inp5 6 input 1 @inp6 7 input 1 @inp7 8 input 1 @inp8 9 read 1 3 5 10 read 1 3 6 11 read 1 4 7 12 read 1 4 8 13 ult 1 9 10 14 ult 1 11 12 15 ult 1 5 6 16 ult 1 7 8 17 iff 1 15 16 18 and 1 13 14 19 and 1 17 18 20 neq 1 3 4 21 and 1 19 20 22 constraint 21