1 sort bitvec 8
2 input 1 x
3 input 1 y
4 one 1
5 constd 1 2
6 add 1 2 3
7 sub 1 2 -3
8 sub 1 7 4
9 sort bitvec 1
10 neq 9 6 8
11 xor 1 2 3
12 and 1 2 3
13 mul 1 12 5
14 add 1 11 13
15 neq 9 6 14
16 or 1 2 3
17 add 1 16 12
18 neq 9 6 17
19 mul 1 16 5
20 sub 1 19 11
21 neq 9 6 20
22 or 9 10 15
23 or 9 18 21
24 or 9 22 23
25 constraint 24