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.)
