フォロー
全部わからん
Skolem depth, Recursion depth, Unsat core {granularity, minimization}, Decompose strategy
https://alloytools.org/quickguide/gui.html
Jackson 本に書いてあったような
> (translate) 多くの場合、定量化された式は、量指定子を使用せずに同等の式に還元できます。この縮小はスコーレム化と呼ばれ
https://alloytools.org/quickguide/skolem.html