1 sort bitvec 2
2 zero 1
3 sort bitvec 6
4 input 3 @inp4
5 sort bitvec 8
6 concat 5 2 4
7 sort bitvec 3
8 input 7 @inp8
9 sort bitvec 1
10 one 9
11 input 1 @inp11
12 one 9
13 input 9 @inp13
14 sort bitvec 4
15 concat 14 8 10
16 concat 3 15 11
17 sort bitvec 7
18 concat 17 16 12
19 concat 5 18 13
20 udiv 5 6 19
21 sort bitvec 5
22 slice 21 20 7 3
23 zero 21
24 eq 9 22 23
25 constraint -24