1 sort bitvec 1
2 input 1 @inp2
3 sort bitvec 6
4 zero 3
5 sort bitvec 2
6 input 5 @inp6
7 sort bitvec 8
8 concat 7 4 6
9 slice 5 -8 3 2
10 slice 1 -9 1 1
11 and 1 2 10
12 constraint 11