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!

Roger Jones

Proofpower mailing list

Reply via email to