1 sort bitvec 4
2 input 1 @inp2
3 input 1 @inp3
4 input 1 @inp4
5 urem 1 2 3
6 urem 1 2 4
7 sort bitvec 1
8 eq 7 5 6
9 eq 7 3 4
10 eq 7 8 9
11 constraint -10