1 sort bitvec 8
2 input 1 a
3 input 1 b
4 input 1 c
5 input 1 x
6 input 1 y
7 input 1 z
8 input 1 u
9 input 1 v
10 add 1 2 3
11 sort bitvec 1
12 eq 11 5 10
13 add 1 6 4
14 eq 11 3 13
15 constd 1 7
16 add 1 15 6
17 eq 11 4 16
18 constd 1 2
19 mul 1 18 5
20 eq 11 6 19
21 constd 1 3
22 mul 1 21 3
23 add 1 22 9
24 eq 11 8 23
25 mul 1 15 7
26 eq 11 9 25
27 constraint 12
28 constraint 14
29 constraint 17
30 constraint 20
31 constraint 24
32 constraint 26