1 sort bitvec 8
2 input 1 a
3 input 1 b
4 input 1 x
5 sort bitvec 1
6 slte 5 2 3
7 slte 5 2 4
8 slte 5 4 3
9 and 5 7 8
10 sub 1 4 2
11 sub 1 3 2
12 ulte 5 10 11
13 eq 5 9 12
14 implies 5 6 13
15 constraint -14