word(sc,p) … \(\in\)
word(vp,c)F … \(\mathsf{cls}\)
abbr … \(\{ x \mid P \}\) ≈ \(\mathsf{cls} ( x , P )\)

1 同じ主張、2つの入力

B2(交わり) を、◀ … p; と ◀ … v; の両方で確かめます。
g2 … \(\forall x \, ( x \in \{ y \mid y \in A_{1} , y \in A_{2} \} \Leftrightarrow ( x \in A_{1} , x \in A_{2} ) )\) \(\blacktriangleleft\) O
◀ … p; でProver9が受け取るものです(記号名は実際には内部の一意な名前になります。内包項は C と書きます)。
　clear(auto_denials). assign(max_seconds, 30). assign(max_proofs, 1).
　formulas(sos).
　　　exists xnec (msort_c(xnec)).
　　　exists xnes (msort_s(xnes)).
　　　all a1 all a2 ((msort_c(a1) & msort_c(a2)) -> msort_c(C(a1,a2))).
　　　all A1_ (msort_c(A1_) -> all A2_ (msort_c(A2_) -> all y (msort_s(y) ->
　　　　　(in_(y,C(A1_,A2_)) <-> (in_(y,A1_) & in_(y,A2_)))))).
　end_of_list.
　formulas(goals).
　　　all A1_ all A2_ ((msort_c(A1_) & msort_c(A2_)) -> all x (msort_s(x) ->
　　　　　(in_(x,C(A1_,A2_)) <-> (in_(x,A1_) & in_(x,A2_))))).
　end_of_list.

同じprfの末尾の p; を v; に替えると、Vampireは次を受け取ります。
　tff(mathel_s_type, type, mathel_s: $tType).
　tff(mathel_c_type, type, mathel_c: $tType).
　tff(mathel_f_type, type, mathel_f: $tType).
　tff(C_type, type, C: (mathel_c * mathel_c) > mathel_c).
　tff(in_type, type, in_: (mathel_s * mathel_c) > $o).
　tff(mathel_axiom_1, axiom, ![A1_: mathel_c]: ![A2_: mathel_c]: ![y: mathel_s]:
　　　(in_(y,C(A1_,A2_)) <=> (in_(y,A1_) & in_(y,A2_)))).
　tff(mathel_conjecture, conjecture, ![A1_: mathel_c, A2_: mathel_c]: ![x: mathel_s]:
　　　(in_(x,C(A1_,A2_)) <=> (in_(x,A1_) & in_(x,A2_)))).
内包公理は同じ1本です。上では msort_s msort_c が式に、下では mathel_s mathel_c が型宣言にあります。上にはさらに非空性2本と C の型付け1本が足されます。

2 崖

goal の and を1つずつ増やします。
g3 … \(\forall x \, ( x \in \{ y \mid y \in A_{1} , y \in A_{2} , y \in A_{3} \} \Leftrightarrow ( x \in A_{1} , x \in A_{2} , x \in A_{3} ) )\) \(\blacktriangleleft\) O
g4 … \(\forall x \, ( x \in \{ y \mid y \in A_{1} , y \in A_{2} , y \in A_{3} , y \in A_{4} \} \Leftrightarrow ( x \in A_{1} , x \in A_{2} , x \in A_{3} , x \in A_{4} ) )\) \(\blacktriangleleft\) O
次の n=5 は、同じ形で and が1つ多いだけです。◀ … p; では通りません。この本の .thmel は prover9 search:seconds 10 で、10秒では終わりません。◀ … v; なら通ります。
h5 … \(\forall x \, ( x \in \{ y \mid y \in A_{1} , y \in A_{2} , y \in A_{3} , y \in A_{4} , y \in A_{5} \} \Leftrightarrow ( x \in A_{1} , x \in A_{2} , x \in A_{3} , x \in A_{4} , x \in A_{5} ) )\) \(\blacktriangleleft\) O
h6 … \(\forall x \, ( x \in \{ y \mid y \in A_{1} , y \in A_{2} , y \in A_{3} , y \in A_{4} , y \in A_{5} , y \in A_{6} \} \Leftrightarrow ( x \in A_{1} , x \in A_{2} , x \in A_{3} , x \in A_{4} , x \in A_{5} , x \in A_{6} ) )\) \(\blacktriangleleft\) O
h7 … \(\forall x \, ( x \in \{ y \mid y \in A_{1} , y \in A_{2} , y \in A_{3} , y \in A_{4} , y \in A_{5} , y \in A_{6} , y \in A_{7} \} \Leftrightarrow ( x \in A_{1} , x \in A_{2} , x \in A_{3} , x \in A_{4} , x \in A_{5} , x \in A_{6} , x \in A_{7} ) )\) \(\blacktriangleleft\) O
h8 … \(\forall x \, ( x \in \{ y \mid y \in A_{1} , y \in A_{2} , y \in A_{3} , y \in A_{4} , y \in A_{5} , y \in A_{6} , y \in A_{7} , y \in A_{8} \} \Leftrightarrow ( x \in A_{1} , x \in A_{2} , x \in A_{3} , x \in A_{4} , x \in A_{5} , x \in A_{6} , x \in A_{7} , x \in A_{8} ) )\) \(\blacktriangleleft\) O

3 測ったもの

上の7つを両方の道で投げた結果です(時間は機械で変わります)。
　n　　p; 判定 / length / 入力バイト　　　v; 判定 / 入力バイト
　2　　〇 / 19 / 1278　　　　　　　　　　〇 / 1494
　3　　〇 / 25 / 1559　　　　　　　　　　〇 / 1726
　4　　〇 / 31 / 1840　　　　　　　　　　〇 / 1958
　5　　× / — / 2121　　　　　　　　　　　〇 / 2190
　6　　× / — / 2402　　　　　　　　　　　〇 / 2422
　7　　× / — / 2683　　　　　　　　　　　〇 / 2654
　8　　× / — / 2964　　　　　　　　　　　〇 / 2886
時間は ◀ … p; が n=2,3,4 で 0.06秒 / 0.06秒 / 0.33秒、◀ … v; は n=8 まで 0.05〜0.14秒でした。
n=4 から n=5 で入力は 1840 から 2121 バイトへ 15% 伸びただけです。

4 相対化の代償

相対化した式では msort_s msort_c は他と同じ述語です。
Prover9 は例えば msort_c(C(A1_,A2_)) を、そのつど all a1 all a2 ((msort_c(a1) & msort_c(a2)) -> msort_c(C(a1,a2))) から導きます。
sc翻訳 では同じことが tff(C_type, type, C: (mathel_c * mathel_c) > mathel_c). という宣言で、推論の対象になりません。
前の本の mA を --| … p; で書きましたが、既定の --| の投げ先が v なのはこれが理由です。
教科書の定理のとおり成否は一致します。変わるのは制限時間内に見つかるかだけです。