1 sort bitvec 8
2 sort array 1 1
3 input 2 @arr3
4 input 2 @arr4
5 input 2 @arr5
6 sort bitvec 1
7 eq 6 3 4
8 eq 6 4 5
9 eq 6 3 5
10 implies 6 7 9
11 constraint -10