1 sort bitvec 1
2 zero 1
3 sort bitvec 15
4 zero 3
5 input 1 @inp5
6 input 3 @inp6
7 sort bitvec 2
8 input 7 @inp8
9 sort bitvec 13
10 sort array 9 9
11 input 10 @arr11
12 sort bitvec 8
13 sort array 12 3
14 input 13 @arr14
15 input 12 @inp15
16 input 3 @inp16
17 write 13 14 15 16
18 input 12 @inp18
19 write 13 17 18 16
20 input 12 @inp20
21 read 3 19 20
22 slice 9 21 12 0
23 input 9 @inp23
24 write 10 11 22 23
25 input 9 @inp25
26 input 9 @inp26
27 read 9 24 26
28 write 10 24 25 27
29 input 9 @inp29
30 read 9 28 29
31 concat 3 8 30
32 ite 3 5 6 31
33 mul 3 -4 32
34 input 3 @inp34
35 ult 1 33 34
36 eq 1 2 -35
37 eq 1 -36 -2
38 constraint -37