1 sort bitvec 8
2 input 1 @inp2
3 input 1 @inp3
4 zero 1
5 add 1 2 3
6 sort bitvec 1
7 eq 6 3 4
8 eq 6 2 5
9 implies 6 -7 -8
10 constraint -9