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

Reply via email to