1 sort bitvec 6
2 input 1 @inp2
3 sort bitvec 12
4 uext 3 2 6
5 input 1 @inp5
6 uext 3 5 6
7 mul 3 4 6
8 constd 3 2209
9 sort bitvec 1
10 eq 9 7 8
11 constraint 10