⇄ CORRESPONDENCE ← All solvers
a first-order statement about R: R(w,u), w = u, forall, exists. Leave it empty to just see which frames validate the axiom