1 sort bitvec 32
2 input 1 @inp2
3 input 1 @inp3
4 input 1 @inp4
5 input 1 @inp5
6 input 1 @inp6
7 mul 1 2 3
8 mul 1 4 6
9 mul 1 7 5
10 mul 1 9 8
11 mul 1 2 6
12 mul 1 3 5
13 mul 1 12 4
14 mul 1 13 11
15 mul 1 2 3
16 mul 1 4 5
17 mul 1 15 6
18 mul 1 16 17
19 mul 1 2 3
20 mul 1 4 5
21 mul 1 20 6
22 mul 1 19 21
23 mul 1 2 6
24 mul 1 3 5
25 mul 1 23 4
26 mul 1 24 25
27 mul 1 2 4
28 mul 1 3 5
29 mul 1 27 6
30 mul 1 28 29
31 sort bitvec 1
32 eq 31 10 14
33 eq 31 10 18
34 eq 31 10 22
35 eq 31 10 26
36 eq 31 10 30
37 eq 31 14 18
38 eq 31 14 22
39 eq 31 14 26
40 eq 31 14 30
41 eq 31 18 22
42 eq 31 18 26
43 eq 31 18 30
44 eq 31 22 26
45 eq 31 22 30
46 eq 31 26 30
47 or 31 -32 -33
48 or 31 -34 -35
49 or 31 -36 -37
50 or 31 -38 -39
51 or 31 -40 -41
52 or 31 -42 -43
53 or 31 -44 -45
54 or 31 53 -46
55 or 31 47 48
56 or 31 49 50
57 or 31 51 52
58 or 31 53 54
59 or 31 55 56
60 or 31 57 58
61 or 31 59 60
62 constraint 61