While converting this problem into a self contained script I
discovered that the theorem is in fact incorrect.
All the universal quantifiers except one should appear inside
the existential quantifier.
Added to this it isn't a unique existential, which is what
ProofPower normally requires (though I have a fix to this
restriction). So an immediate conversion into a self-
contained script runs aground.
I will go back to the original and see if the problem
disappears when I get the quantifiers right.
Proofpower mailing list