1 sort bitvec 8
2 input 1 @inp2
3 input 1 @inp3
4 sort bitvec 1
5 input 4 @inp5
6 input 4 @inp6
7 ite 1 5 3 2
8 ite 1 6 3 -7
9 and 4 -5 -6
10 ite 1 9 -2 3
11 eq 4 8 10
12 constraint -11