1 sort bitvec 2
2 input 1 @inp2
3 input 1 @inp3
4 input 1 @inp4
5 input 1 @inp5
6 sort bitvec 8
7 sort array 1 6
8 input 7 @arr8
9 input 1 92
10 input 6 93
11 write 7 8 9 10
12 input 1 95
13 input 6 96
14 write 7 11 12 13
15 input 1 98
16 input 6 99
17 write 7 14 15 16
18 read 6 17 2
19 read 6 17 3
20 read 6 17 4
21 read 6 17 5
22 sort bitvec 1
23 ult 22 18 19
24 ult 22 19 20
25 ult 22 20 21
26 and 22 23 24
27 and 22 25 26
28 constraint 27