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 2 3
8 ite 1 6 -7 3
9 and 4 5 6
10 ite 1 9 -2 3
11 eq 4 8 10
12 constraint -11