A clarification: a rule is invertible if when the conclusion is provable, each of the premises is. The most important example of a non-invertible rule is weakening:
Gamma |- Delta Gamma |- Delta
----------------- -----------------
Gamma, A |- Delta Gamma |- Delta, A
The point about applying invertible rules eagerly is why proof systems designed for proof search are formulated so that most of the rules are invertible, and use of non-invertible rules can be pushed up the deduction as far as possible: in the case of weakening, the rule can be pushed so it appears before all others.
One interesting thing to do here would be to reorder the clauses of the Prolog predicate to see the effect on the size of the proof. Or write a meta-interpreter to automatically try searching over permutations of the rules, or with a cost parameter... (I'd better stop now or I won't get anything done today.)
Otten has more efficient solvers in "Part 3: Tableau and Connection Provers" but i find the sequent proofs much easier to understand (which makes sense, the "natural" in "Natural Deduction" means something like "intuitive" as used in IT.)
A clarification: a rule is invertible if when the conclusion is provable, each of the premises is. The most important example of a non-invertible rule is weakening:
The point about applying invertible rules eagerly is why proof systems designed for proof search are formulated so that most of the rules are invertible, and use of non-invertible rules can be pushed up the deduction as far as possible: in the case of weakening, the rule can be pushed so it appears before all others.