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 input 1 @inp14
15 concat 11 2 14
16 input 11 @inp16
17 eq 1 15 16
18 eq 1 13 17
19 and 1 10 18
20 and 1 9 19
21 and 1 14 -13
22 ite 1 21 -2 2
23 and 1 -14 13
24 ite 1 23 13 2
25 and 1 -22 -24
26 input 1 @inp26
27 sort bitvec 3
28 input 27 @inp28
29 slice 1 28 1 1
30 and 1 -26 -29
31 and 1 26 29
32 and 1 -30 -31
33 and 1 25 32
34 and 1 -32 9
35 and 1 -33 -34
36 and 1 20 35
37 constraint 36