∀x ∀y Ryx ⊨ ∀x Rax
∀x ∀y (Rxy → Fy), ∀x Rax ⊨ ∀x Fx
∀x ∀y Rxy ⊨ ∀x ∀y Ryx
∀x ∀y ((Py ∧ Fyx) → Ly) ⊨ ∀x (Px → ∀y (Fxy → Lx))
∀x ∀y (Ryx → ∀z Rzy), ¬ ∀x ∀y Rxy ⊨ ∀x ∀y ¬ Rxy