soft: 6 ;
[2] +1 x1 >= 1 ;
[3] -1 x1 >= 0 ;