Help with proving an obligation

[saksha...@xxxxxxxxxxxxxx]

Hi,

Line 3403 of the attached tla file has the following obligation which fails on TLAPS(Version 1.5.6 of 29 January 2018) on my machine (Ubuntu 17.10):

  <5>6. Next BY <2>6 DEF Next

where

  Next == \/ \E p \in Proposers : Phase1a(p) \/ Phase2a1(p) \/ Phase2a11(p) \/ Phase2a12(p) \/ Phase2a13(p)
          \/ \E a \in Acceptors : Phase1b(a) \/ Phase2b(a)  \/ PhasePr(a)

and <2>6 is

  <2>6. ASSUME NEW a \in Acceptors,
               Phase1b(a)
        PROVE  Inv'

Also attached is the screenshot showing the interesting obligations. I'm wondering if I'm making a really dumb mistake here or is it something else?

Thanks,
Saksham Chand

Attachment: Screenshot_tla_Next.png
Description: PNG image

Attachment: vRAMultiPaxos.tla
Description: Binary data