x1 or x2 x2 or not x3 x3 or not x1