1 sort bitvec 1
2 one 1
3 sort bitvec 7
4 input 3 @inp4
5 sort bitvec 8
6 concat 5 2 4
7 input 5 @inp7
8 ugte 1 6 -7
9 constraint -8