Input

1. Apply ⊓+-rule