Problem with TLAPM

[Amira Methni <methni...@xxxxxxxxx>]

Hi,

I'm trying to prove a lemma with TLAPS.But, I get an error message (see the attached picture)
For information, the lemma used a predicate composed of a disjunction of several formulas. When I comment some formulas of this disjunction, TLAPS succeeds to prove the lemma. Otherwise, I have the error message.
Is this due to the size of my predicate?

Thank you,

Amira

Attachment: error.PNG
Description: PNG image