ws1s; ~ex1 x1: ~ex1 x2: ~ex1 x3: ~ex1 x4: x1 < x2 & x2 < x3 & x3 < x4;