1 sort bitvec 3
2 input 1 @inp2
3 sort bitvec 1
4 slice 3 2 0 0
5 sort bitvec 2
6 concat 5 -4 -4
7 zero 5
8 eq 3 6 7
9 slice 5 2 1 0
10 add 5 -9 -7
11 mul 5 10 10
12 slice 3 11 0 0
13 and 3 -8 12
14 constraint 13