It looks like the problem arises when the quantifiers are
wrong, and is difficult to reproduce without the mod to allow
non-unique quantifiers, since (at least in the example I was
working with) if you get the quantifiers wrong you can prove
the existential but you can't prove the unique existential.
I have made a tarfile which should reproduce the problem, but
the uninformative error message may only arise if the
liberalisation to allow non-unique quantification is
incorporated in ProofPower. (which I was hoping for).
So you may not feel motivated to address this small issue!
Proofpower mailing list