1 sort bitvec 1
2 zero 1
3 constraint 2
4 input 1 @inp4
5 eq 1 4 -2
6 eq 1 5 -2
7 constraint 6
8 input 1 @inp8
9 eq 1 8 4
10 constraint 9
11 input 1 @inp11
12 input 1 @inp12
13 and 1 12 8
14 eq 1 11 13
15 constraint 14
16 input 1 @inp16
17 eq 1 16 11
18 constraint 17
19 input 1 @inp19
20 eq 1 19 -2
21 eq 1 16 -2
22 input 1 @inp22
23 and 1 21 -22
24 eq 1 20 -23
25 constraint 24
26 input 1 @inp26
27 eq 1 26 19
28 constraint 27
29 eq 1 26 -2
30 eq 1 2 29
31 constraint 30