1 sort bitvec 1
2 input 1 @inp2
3 sort bitvec 4
4 input 3 @inp4
5 input 3 @inp5
6 input 3 @inp6
7 mul 3 4 5
8 mul 3 4 6
9 ite 3 2 7 8
10 ite 3 2 5 6
11 mul 3 10 4
12 eq 1 9 11
13 mul 3 4 6
14 mul 3 5 6
15 ite 3 2 13 14
16 ite 3 2 4 5
17 mul 3 16 6
18 eq 1 15 17
19 mul 3 4 5
20 mul 3 5 6
21 ite 3 2 19 20
22 ite 3 2 4 6
23 mul 3 22 5
24 eq 1 21 23
25 mul 3 5 6
26 mul 3 4 5
27 ite 3 2 25 26
28 ite 3 2 6 4
29 mul 3 28 5
30 eq 1 27 29
31 or 1 -12 -18
32 or 1 -24 -30
33 or 1 31 32
34 constraint 33