1 sort bitvec 1
2 input 1 @inp2
3 input 1 @inp3
4 input 1 @inp4
5 and 1 3 4
6 input 1 @inp6
7 and 1 6 4
8 and 1 -5 -7
9 and 1 -2 8
10 input 1 @inp10
11 sort bitvec 2
12 input 11 @inp12
13 slice 1 12 0 0
14 zero 1
15 input 1 @inp15
16 concat 11 14 15
17 input 11 @inp17
18 eq 1 -16 17
19 eq 1 -13 18
20 and 1 10 -19
21 and 1 9 20
22 slice 1 15 0 0
23 slice 1 13 0 0
24 and 1 22 -23
25 ite 1 24 -14 14
26 and 1 -22 23
27 ite 1 26 13 14
28 add 1 -14 -14
29 and 1 -27 -28
30 and 1 -25 29
31 input 1 @inp31
32 sort bitvec 3
33 input 32 @inp33
34 slice 1 33 1 1
35 and 1 -31 -34
36 and 1 31 34
37 and 1 -35 -36
38 and 1 30 37
39 and 1 -37 9
40 and 1 -38 -39
41 and 1 21 40
42 constraint 41