and([
  always(or([not x1 , sometime(p)])),
  always(or([not x2 , sometime(q)])),
  always(or([not p , next(p)])),
  always(or([not q , next(q)])),
  always(or([not x4 , sometime(x5)])),
  always(or([not x5 , not p, not q])),
  always(or([not x3 , x4])),
  always(or([not x3 , x6])),
  always(or([not x6 , next(x4)])),
  always(or([not x6 , next(x6)])),
  or([x1]),
  or([x2]),
  or([x3])
]).