1 sort bitvec 8 2 sort array 1 1 3 input 2 @arr3 4 constd 1 5 5 input 1 @inp5 6 add 1 4 5 7 write 2 3 5 5 8 read 1 7 6 9 sort bitvec 1 10 redand 9 8 11 constraint 10