1 早見表

この Book は、prf を実際に書くときの判断（どの投げ先に投げるか・FAIL したら何をするか・難しい定理をどう進めるか）をまとめた実践編です。定義や記号は 6.book のもの（ヘッダは import 6 だけ。thmel 行を書かないので .thmel は /common/default）。基本の書き方は 3.book、slash の規則は 4.book、クラスと -|・--| は 5.book にあります。灰色の枠の prf の例は、ソースでは1行ですが、表示（Web の画面か ai_reading.php）では段ごとに改行されます。
まず表にまとめます。理由と実測は後の節にあります。

段の式に含まれるもの	書く段	理由・実測
クラス変数も述語変数も無い（一階の式）	-| … p;	掲載した例では最速。まず試す候補（「一階の式」の小節）
クラス変数（X_ など）	◀ … v; か --| … v;（本が紹介した Wc. の定義も前提に入る＝5.book）	-| は「|0 翻訳不可」。◀ … p; も通るが、相対化で式が大きくなるので項が増えると遅くなりやすい（「クラス変数」の小節。遅くなる実例は「一階の式」の小節の5項）。◀ … v; と --| … v; はどちらも通る例が多い（--| はアロー関数を fn-elim・内包を cls-elim し Wc. を足す＝5.book）
内包 \{ cls x | … \} を含む多ソートの段	v;	掲載した例では vampire+ が速かった（「内包記法と分出公理」の小節）
述語への代入が要る（schema を使う段）	実例 SOURCE[P:=θ] を sos に書いて v; など	証明器に述語を探させない。prop の高階変数にはどの backend でも代入しない（「述語変数の代入」の小節）
goal の断片が自明で数が多い	p[whole];	起動の回数が減る（4.book）
1段で通らない	補題に切って段ごとに投げ先を選び、最後を h; で結ぶ	p; で timeout する段も v; なら一瞬で通ることがある（「一階の式」の小節の5項：◀ p; は timeout、◀ v; は 0.012秒）

証明器は、時間内に証明が見つからないと timeout を返します。探索を早く打ち切って not_proved を返すこともあります（Prover9 の not_proved は「証明が見つからなかった」で、無いことが確定したわけではありません）。Vampire の CounterSatisfiable は「渡した問題には反例がある」という答えです。どちらも FAIL で、主張が偽という判定ではありません。
FAIL したときの次の一手（原因は候補で、どれかを確かめながら試します）。FAIL の行の頭（zz.book:11）は thm の行、文言の「13行目の段」は落ちた段の行です。直す所（ラベルの定義など）はその前の行にあることもあります。

症状（FAIL の文言）	意味	次の一手
「|0 翻訳不可: … ∈_ が残っています」	クラス変数を含む段を -| で投げた	◀ … v; か --| … v; にする
すぐ not_proved（Vampire なら CounterSatisfiable）	この前提とこの展開では証明が見つからなかった（CounterSatisfiable なら、渡した問題には反例がある）。定義が開ききっていない・前提（橋渡しの定義や補題）が足りない・主張が偽のどれか	review_cli.php … --inputs で投げた入力を読み、開いていない記号が残っていれば、goal と、同じ記号を含む sos の項の両方に / を足し（「goal と sos で形を揃える」）、足りない補題は前提に置く（「実例①」「実例②」）
timeout	考えられる原因：定義を開きすぎ（/ W. の本数が多い・=. の外延性など）か、1段に詰め込みすぎ。必要な前提を消した場合もある	W.!名.（名は開かない定義の名前。例 W.!=.）で開く定義を減らす・補題に切る・投げ先を替える
h; の段で落ちる	各段は示せたが、組み合わせても thm の主張にならない	最後の段（h;）の goal・sos が thm の行と同じか、途中で使った定義が W. に入っているか、h; の段の関係がつなぐ段と合っているか（/ で展開した段をつなぐなら -| h;・3.book「h; の段の関係」）を確かめる。sos の項がラベルを含む式なら、ラベルの名前を前の Thm の変数にそろえる（「名前の付け方」4）
「前の段に出てきた名前「a」に後からラベル…」「本が紹介した prop と同じ名前「A」にラベル…」「thm の行の主張に出てくる名前「x」に…」「ラベル `u` と同じ名前が、後の段の式の中に…」	ラベルの付け方の誤り	定義を使う段より前へ移す／別の名前に替える（「名前の付け方」）
「prf の最後の段が thm の主張と違います」	最後の段の goal・sos が thm の行と綴りで違う（中身が同じラベルの名前でも違う）	最後の段を thm の行と同じ綴りに直す（「名前の付け方」）
「Prop の名前 … は付けられません」	名前の付け方の誤り（「名前の付け方」）	名前を替え、使う所も替える。査読はここで止まるので、直すと次の FAIL が出ることがある

表の各行の詳しい見分け方と、実際に直した例は「失敗の種類を見分ける」の節にあります。

1.1 backend

prfの各段は、末尾の投げ先の文字で backend を選びます（仕組みは3.book）。どれに投げるかで、通るか・どれだけ速いかが大きく変わります。
・prover+（p;）… Prover9 を使います。一階言語のThmを受け取ります。-| の段は Thm を |cvt+|0 で翻訳して、◀ の段は{s,c}ソートを一項述語で相対化して投げます。goal を断片に割って投げ、すべて証明できたら OK です（割らない p[whole]; は4.book）。
・vampire+（v;）… Vampire を使います。{s,c}ソート言語のThmを、ソートを保ったまま（多ソートの TFF 形式で）受け取ります。
・satallax+（s;）… Satallax を使います。高階言語のThmを受け取ります。Thm に自由に現れる命題変数・述語変数は、Thm 全体で1つの記号として渡します（|v-elim をした p; v; と同じ意味・7.book）。 ただし .thmel に satallax+ predicate:all と書いた本で、--| … s; の段の sos に素の名前で書いた ∀ ?R^ ( … ) の prop だけは、その式の中で ?R^ を ∀ で閉じた高階の公理として渡します（下の「述語変数の代入」）。
・hyperion（h;）… 証明器ではありません。prf の前の段で示したThmを組み合わせて、thm の主張を導けるかを確かめます（例外：関係をまたいで Thm を確かめ直すときだけ Vampire を呼ぶ・3.book「h; の段の関係」）。
投げ先の文字は .thmel の backend 行が決めます（1.book の .thmel の節に表があります）。今ある .thmel はどれも p v h s の4つを持ちます。