1 sort bitvec 8
2 input 1 x
3 input 1 y
4 or 1 2 3
5 add 1 2 3
6 xor 1 2 3
7 sort bitvec 1
8 uaddo 7 2 3
9 ulte 7 4 5
10 implies 7 -8 9
11 implies 7 8 -9
12 ugt 7 2 3
13 ite 1 12 2 3
14 ult 7 2 3
15 ite 1 14 2 3
16 sub 1 13 15
17 ulte 7 16 6
18 or 7 -10 -11
19 or 7 18 -17
20 constraint 19