Proofs of conjunctions can be slow because the operator

The command `resume by /\` directs LP to resume the proof of the current
conjecture using this method. It is applicable only when the current
conjecture has been reduced to a conjunction.

Users should beware that employing this method too early in a proof can result in lengthening the proof considerably, for example, when the same sequence of commands or the same lemma is needed to prove more than one conjunct.