1 sort bitvec 4
2 constd 1 5
3 neg 1 2
4 constd 1 3
5 input 1 res
6 smod 1 3 4
7 sort bitvec 1
8 eq 7 5 6
9 constraint 8