>751
イメージはそんな感じです。もっと簡単に整数の行列で、

　1: ∃matrix={a[i,j]}.∀i.a[i,i]=1…対角成分が1の行列は存在する
　2: ∀matrix={a[i,j]}.∃i.a[i,i]=1…どんな行列も対角成分のどれかが1

を考えるとき、751のalistを使って

　１．Resolve[Exists[alist, Element[alist, Integers], ForAll[i, Element[i, Integers], a[i, i] == 1]]]
　２．Resolve[ForAll[alist, Element[alist, Integers], Exists[i, Element[i, Integers], a[i, i] == 1]]]

のようにすると、1はTrue、2はFalseとなってほしいのですが、
論理式が表示されるだけでTrue/Falseを計算してくれないのが
どうしてなのかわからないのです（ちなみに５版です）。