// --initial-memory 'a=[5,15]; b=[5,20]; c=[5,56]'
// --final-memory   'a=[7,9] ; b=[6,8];  c=[5,7]'

assume ((b < a) && ((c < b) && (a < 10)))