Recursive minimisation when logging full proof

Currently, recursive minimisation is disabled when logging a full proof. Ideally, we want minimisation, but we have to be careful to log only the inferences that are used to remove predicates. Simply logging all inferences does not work, because at certain points the minimisation will stop and leave premises unassigned in the checking of the deduction step.