1 sort bitvec 32
2 sort bitvec 16
3 sort array 2 1
4 input 3 @arr4
5 input 3 @arr5
6 input 3 @arr6
7 input 1 @inp7
8 input 1 @inp8
9 input 1 @inp9
10 mul 1 7 8
11 mul 1 7 9
12 mul 1 8 9
13 mul 1 10 11
14 mul 1 12 13
15 input 2 @inp15
16 write 3 4 15 14
17 sort bitvec 1
18 input 17 @inp18
19 ite 3 18 5 6
20 neq 17 16 19
21 constraint 20