矛盾節のLBDと学習節のLBDの関係

[shnarazk]

もしかして矛盾節のLBDが学習節の生成コストになってたりしないだろうか？

LBDが5より小さいものは使ってなくても回収しない方がいいとのことだが、その節をsubsumeできる節が存在するならその節は無駄でしかない。vivififyで引っ掛からなければ部分解の発見までもう削除の機会はないだろう。
消したい。

これで消せるようならvivification要らないのでは。

ということで !20240928-labor-pain