(cl-text axiom
  (P x)
  (and (P x) (Q y))
)

(cl-text correct
  (Q y)
) %implied

(cl-text incorrect (P y)) %implied