1 sort bitvec 1
2 zero 1
3 input 1 @inp3
4 eq 1 -2 3
5 input 1 @inp5
6 input 1 @inp6
7 eq 1 6 3
8 and 1 5 -7
9 and 1 4 -8
10 eq 1 6 2
11 and 1 9 10
12 eq 1 3 2
13 and 1 5 -12
14 and 1 11 -13
15 constraint 14