1 sort bitvec 8
2 input 1 x
3 input 1 y
4 sort bitvec 1
5 eq 4 2 3
6 sub 1 2 3
7 sub 1 3 2
8 or 1 6 7
9 slice 4 8 7 7
10 eq 4 5 -9
11 eq 4 -5 9
12 or 4 -10 -11
13 constraint 12