1 sort bitvec 8
2 input 1 x
3 input 1 y
4 one 1
5 constd 1 2
6 sub 1 2 3
7 add 1 2 -3
8 add 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 sub 1 11 13
15 neq 9 6 14
16 and 1 2 -3
17 sub 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