((0 (.in v0 v1) :hyp nil) (1 (.to (.in v0 v1) (.or (.in v0 v1) (.in v0 v2))) :th (th-or-intro-l)) (2 (.or (.in v0 v1) (.in v0 v2)) :ir (mp 1 0)))

行の形: (番号 論理式 :役割 (根拠 引数...))。役割は :hyp :axiom :ir :th :th-ded。 ライブラリで定理を開き「エディタで開く」を押すと、その証明が入ります。