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