1 sort bitvec 4
2 input 1 @inp2
3 input 1 @inp3
4 input 1 @inp4
5 sort bitvec 2
6 input 5 @inp6
7 input 5 @inp7
8 sort bitvec 1
9 input 8 @inp9
10 input 8 @inp10
11 input 8 @inp11
12 slice 5 3 3 2
13 eq 8 6 12
14 const 8 1
15 eq 8 9 14
16 const 5 00
17 eq 8 6 16
18 and 8 -15 -17
19 and 8 15 17
20 and 8 -18 -19
21 eq 8 14 9
22 slice 5 4 3 2
23 eq 8 7 22
24 eq 8 10 14
25 eq 8 7 16
26 and 8 -24 -25
27 and 8 24 25
28 and 8 -26 -27
29 eq 8 14 10
30 eq 8 11 14
31 const 1 1001
32 eq 8 31 2
33 and 8 -30 -32
34 and 8 30 32
35 and 8 -33 -34
36 eq 8 14 11
37 mul 1 3 4
38 eq 8 2 37
39 and 8 13 21
40 and 8 23 29
41 and 8 36 38
42 and 8 -20 -28
43 and 8 39 40
44 and 8 41 42
45 and 8 43 44
46 and 8 45 -35
47 constraint 46