ws1s; ex1 x1: ex1 x2: ex1 x3: ex1 x4: ~ex1 x5: ~ex1 x6: ~ex1 x7: ~ex1 x8: x1 < x2 & x2 < x3 & x3 < x4 & x4 < x5 & x5 < x6 & x6 < x7 & x7 < x8;