For example, framing `P` in `(P ∨ Q) ∗ R` now succeeds and turns the goal into `R`.