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. Roger Jones _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
