and([
or([BOX2F(X)]), 
or([not PinvNameF, E1NameF(constant(dName))]), 
or([BOX0F(X)]), 
or([BOX1F(X)]), 
or([not PNameF, E1NameInvF(constant(dNameInv))]), 
or([NVV1(X)]), 
or([not BOX23F(X), BOX12P(X)]), 
or([not BOX12P(X), BOX23F(X)]), 
or([not BOX1F(X), BOX26P(X)]), 
or([not BOX26P(X), BOX1F(X)]), 
or([not BOX21F(X), BOX10P(X)]), 
or([not BOX10P(X), BOX21F(X)]), 
or([not BOX17F(X), BOX6P(X)]), 
or([not BOX6P(X), BOX17F(X)]), 
or([not PNameF, PNameF]), 
or([not BOX19F(X), BOX8P(X)]), 
or([not BOX8P(X), BOX19F(X)]), 
or([not E2NameF(X), E2NameP(X)]), 
or([not E2NameP(X), E2NameF(X)]), 
or([not BOX0F(X), BOX25P(X)]), 
or([not BOX25P(X), BOX0F(X)]), 
or([not BOX24F(X), BOX13P(X)]), 
or([not BOX13P(X), BOX24F(X)]), 
or([not BOX15F(X), BOX4P(X)]), 
or([not BOX4P(X), BOX15F(X)]), 
or([not BOX2F(X), BOX27P(X)]), 
or([not BOX27P(X), BOX2F(X)]), 
or([not E1NameInvF(constant(dNameInv)), E1NameInvP(constant(dNameInv))]), 
or([not E1NameInvP(constant(dNameInv)), E1NameInvF(constant(dNameInv))]), 
or([not BOX22F(X), BOX11P(X)]), 
or([not BOX11P(X), BOX22F(X)]), 
or([not PersonF(X), PersonP(X)]), 
or([not PersonP(X), PersonF(X)]), 
or([not BOX20F(X), BOX9P(X)]), 
or([not BOX9P(X), BOX20F(X)]), 
or([not PinvNameF, PinvNameF]), 
or([not BOX16F(X), BOX5P(X)]), 
or([not BOX5P(X), BOX16F(X)]), 
or([not BOX18F(X), BOX7P(X)]), 
or([not BOX7P(X), BOX18F(X)]), 
or([not PNameF, PNameP]), 
or([not PNameP, PNameF]), 
or([not BOX14F(X), BOX3P(X)]), 
or([not BOX3P(X), BOX14F(X)]), 
or([not PinvNameF, PinvNameP]), 
or([not PinvNameP, PinvNameF]), 
or([not E1NameInvF(X), E1NameInvP(X)]), 
or([not E1NameInvP(X), E1NameInvF(X)]), 
or([not E1NameF(constant(dName)), E1NameP(constant(dName))]), 
or([not E1NameP(constant(dName)), E1NameF(constant(dName))]), 
or([not E1NameF(X), E1NameP(X)]), 
or([not E1NameP(X), E1NameF(X)]), 
or([PersonF(constant(John))]), 
or([E1NameInvF(constant(N3))]), 
or([E1NameInvF(constant(N21))]), 
or([E1NameInvF(constant(N25))]), 
or([E1NameInvF(constant(N39))]), 
or([E1NameInvF(constant(N5))]), 
or([E1NameInvF(constant(N22))]), 
or([E1NameInvF(constant(N34))]), 
or([E1NameInvF(constant(N2))]), 
or([E1NameInvF(constant(N4))]), 
or([E1NameInvF(constant(N12))]), 
or([E1NameInvF(constant(N10))]), 
or([E1NameInvF(constant(N0))]), 
or([E1NameInvF(constant(N29))]), 
or([E1NameInvF(constant(N18))]), 
or([E1NameInvF(constant(N16))]), 
or([E1NameInvF(constant(N14))]), 
or([E1NameInvF(constant(N19))]), 
or([E1NameInvF(constant(N37))]), 
or([E1NameInvF(constant(N36))]), 
or([E1NameInvF(constant(N11))]), 
or([E1NameInvF(constant(N27))]), 
or([E1NameInvF(constant(N13))]), 
or([E1NameInvF(constant(N24))]), 
or([E1NameInvF(constant(N8))]), 
or([E1NameInvF(constant(N1))]), 
or([E1NameInvF(constant(N30))]), 
or([E1NameInvF(constant(N33))]), 
or([E1NameInvF(constant(N15))]), 
or([E1NameInvF(constant(N32))]), 
or([E1NameInvF(constant(N23))]), 
or([E1NameInvF(constant(N38))]), 
or([E1NameInvF(constant(N26))]), 
or([E1NameInvF(constant(N31))]), 
or([E1NameInvF(constant(N6))]), 
or([E1NameInvF(constant(N20))]), 
or([E1NameInvF(constant(N7))]), 
or([E1NameInvF(constant(N9))]), 
or([E1NameInvF(constant(N17))]), 
or([E1NameInvF(constant(N28))]), 
or([E1NameInvF(constant(N35))]), 
or([E2NameF(constant(John))]),
always(or([not NVV1(X), NVV2(X), BOX5P(X)])), 
always(or([not NVV1(X), NVV2(X), NVV3])), 
always(or([not NVV1(X), not BOX5P(X), NVV4, NVV5(X)])), 
always(or([not NVV1(X), not BOX7P(X), NVV6(X)])), 
always(or([not NVV1(X), NVV7(X), BOX7P(X)])), 
always(or([not NVV1(X), not BOX19F(X), NVV9])), 
always(or([not NVV1(X), NVV10, BOX19F(X)])), 
always(or([not NVV1(X), not BOX26P(X), NVV12(X)])), 
always(or([not NVV1(X), NVV13(X), BOX26P(X)])), 
always(or([not NVV1(X), NVV15(X), BOX8P(X)])), 
always(or([not NVV1(X), NVV15(X), NVV16])), 
always(or([not NVV1(X), not BOX8P(X), NVV17, NVV18(X)])), 
always(or([not NVV1(X), not BOX21F(X), NVV19(X)])), 
always(or([not NVV1(X), NVV20(X), BOX21F(X)])), 
always(or([not NVV1(X), NVV22(X), BOX10P(X)])), 
always(or([not NVV1(X), NVV22(X), NVV23(X)])), 
always(or([not NVV1(X), not BOX10P(X), NVV24(X), NVV25(X)])), 
always(or([not NVV1(X), not BOX13P(X), NVV26(X)])), 
always(or([not NVV1(X), NVV27(X), BOX13P(X)])), 
always(or([not NVV1(X), NVV29(X), BOX11P(X)])), 
always(or([not NVV1(X), NVV29(X), NVV30(X)])), 
always(or([not NVV1(X), not BOX11P(X), NVV31(X), NVV32(X)])), 
always(or([not NVV1(X), NVV33(X), BOX9P(X)])), 
always(or([not NVV1(X), NVV33(X), NVV34(X)])), 
always(or([not NVV1(X), not BOX9P(X), NVV36(X), NVV38(X)])), 
always(or([not NVV1(X), NVV39(X), BOX23F(X)])), 
always(or([not NVV1(X), NVV39(X), NVV40(X)])), 
always(or([not NVV1(X), not BOX23F(X), NVV41(X), NVV42(X)])), 
always(or([not NVV1(X), not BOX4P(X), NVV43(X)])), 
always(or([not NVV1(X), NVV44(X), BOX4P(X)])), 
always(or([not NVV1(X), NVV46(X), BOX15F(X)])), 
always(or([not NVV1(X), NVV46(X), NVV47(X)])), 
always(or([not NVV1(X), not BOX15F(X), NVV48(X), NVV49(X)])), 
always(or([not NVV1(X), not BOX17F(X), NVV50(X)])), 
always(or([not NVV1(X), NVV51(X), BOX17F(X)])), 
always(or([not NVV1(X), not BOX12P(X), NVV53(X)])), 
always(or([not NVV1(X), NVV54(X), BOX12P(X)])), 
always(or([not NVV1(X), NVV56(X), BOX6P(X)])), 
always(or([not NVV1(X), NVV56(X), NVV57(X)])), 
always(or([not NVV1(X), not BOX6P(X), NVV59(X), NVV61(X)])), 
always(or([not NVV1(X), NVV62(X), BOX18F(X)])), 
always(or([not NVV1(X), NVV62(X), NVV63(X)])), 
always(or([not NVV1(X), not BOX18F(X), NVV64(X), NVV65(X)])), 
always(or([not NVV1(X), NVV66(X), BOX24F(X)])), 
always(or([not NVV1(X), NVV66(X), NVV67(X)])), 
always(or([not NVV1(X), not BOX24F(X), NVV68(X), NVV69(X)])), 
always(or([not NVV1(X), not BOX27P(X), NVV70(X)])), 
always(or([not NVV1(X), NVV71(X), BOX27P(X)])), 
always(or([not NVV1(X), not BOX25P(X), NVV73(X)])), 
always(or([not NVV1(X), NVV74(X), BOX25P(X)])), 
always(or([not NVV1(X), not BOX16F(X), NVV76])), 
always(or([not NVV1(X), NVV77, BOX16F(X)])), 
always(or([not NVV1(X), NVV79(X), BOX3P(X)])), 
always(or([not NVV1(X), NVV79(X), NVV80(X)])), 
always(or([not NVV1(X), not BOX3P(X), NVV82(X), NVV84(X)])), 
always(or([not NVV1(X), not BOX14F(X), NVV85(X)])), 
always(or([not NVV1(X), NVV86(X), BOX14F(X)])), 
always(or([not NVV1(X), not BOX20F(X), NVV88(X)])), 
always(or([not NVV1(X), NVV89(X), BOX20F(X)])), 
always(or([not NVV1(X), NVV91(X), BOX2F(X)])), 
always(or([not NVV1(X), NVV91(X), NVV92(X)])), 
always(or([not NVV1(X), not BOX2F(X), NVV93(X), NVV94(X)])), 
always(or([not NVV1(X), not BOX22F(X), NVV95(X)])), 
always(or([not NVV1(X), NVV96(X), BOX22F(X)])), 
always(or([not NVV1(X), NVV98(X), BOX1F(X)])), 
always(or([not NVV1(X), NVV98(X), NVV99(X)])), 
always(or([not NVV1(X), not BOX1F(X), NVV100(X), NVV101(X)])), 
always(or([not NVV1(X), NVV102(X), BOX0F(X)])), 
always(or([not NVV1(X), NVV102(X), NVV103(X)])), 
always(or([not NVV1(X), not BOX0F(X), NVV104(X), NVV105(X)])), 
always(or([not NVV6(X), BOX8P(X)])), 
always(or([not NVV8(X), not BOX8P(X)])), 
always(or([not NVV9, PNameF])), 
always(or([not NVV11, not PNameF])), 
always(or([not NVV12(X), BOX6P(X)])), 
always(or([not NVV14(X), not BOX6P(X)])), 
always(or([not NVV19(X), BOX23F(X)])), 
always(or([not NVV21(X), not BOX23F(X)])), 
always(or([not NVV26(X), E2NameP(X)])), 
always(or([not NVV28(X), not E2NameP(X)])), 
always(or([not NVV35(X), not PersonP(X), E1NameP(X)])), 
always(or([not NVV35(X), not PersonP(X), not E2NameP(X)])), 
always(or([not NVV35(X), not E2NameP(X), E1NameP(X)])), 
always(or([not NVV35(X), not E1NameP(X), BOX10P(X)])), 
always(or([not NVV35(X), not E2NameP(X), BOX11P(X)])), 
always(or([not NVV37(X), not E1NameP(X), PersonP(X), E1NameP(X), E2NameP(X)])), 
always(or([not NVV37(X), PersonP(X), E1NameP(X), E2NameP(X)])), 
always(or([not NVV37(X), PersonP(X), not E1NameP(X), E1NameP(X), E2NameP(X)])), 
always(or([not NVV37(X), not E1NameP(X), E1NameP(X), E2NameP(X)])), 
always(or([not NVV37(X), not E1NameP(X), PersonP(X), not BOX10P(X), E2NameP(X)])), 
always(or([not NVV37(X), PersonP(X), not BOX10P(X), E2NameP(X)])), 
always(or([not NVV37(X), PersonP(X), not E1NameP(X), not BOX10P(X), E2NameP(X)])), 
always(or([not NVV37(X), not E1NameP(X), not BOX10P(X), E2NameP(X)])), 
always(or([not NVV37(X), not E1NameP(X), PersonP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV37(X), PersonP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV37(X), not E1NameP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV37(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV37(X), PersonP(X), E2NameP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV37(X), E2NameP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV37(X), not E1NameP(X), PersonP(X), E2NameP(X), not BOX10P(X), not BOX11P(X)])), 
always(or([not NVV37(X), PersonP(X), E2NameP(X), not BOX10P(X), not BOX11P(X)])), 
always(or([not NVV37(X), not E1NameP(X), E2NameP(X), not BOX10P(X), not BOX11P(X)])), 
always(or([not NVV37(X), PersonP(X), not E1NameP(X), not BOX10P(X), not BOX11P(X)])), 
always(or([not NVV37(X), PersonP(X), E2NameP(X), not E1NameP(X), not BOX10P(X), not BOX11P(X)])), 
always(or([not NVV37(X), E2NameP(X), not E1NameP(X), not BOX10P(X), not BOX11P(X)])), 
always(or([not NVV43(X), BOX5P(X)])), 
always(or([not NVV45(X), not BOX5P(X)])), 
always(or([not NVV50(X), not E1NameF(X), BOX18F(X)])), 
always(or([not NVV52(X), E1NameF(X)])), 
always(or([not NVV52(X), not BOX18F(X)])), 
always(or([not NVV53(X), E1NameP(X)])), 
always(or([not NVV55(X), not E1NameP(X)])), 
always(or([not NVV58(X), not E1NameP(X), BOX7P(X)])), 
always(or([not NVV60(X), E1NameP(X)])), 
always(or([not NVV60(X), not BOX7P(X)])), 
always(or([not NVV70(X), BOX9P(X)])), 
always(or([not NVV72(X), not BOX9P(X)])), 
always(or([not NVV73(X), BOX3P(X)])), 
always(or([not NVV75(X), not BOX3P(X)])), 
always(or([not NVV76, PinvNameF])), 
always(or([not NVV78, not PinvNameF])), 
always(or([not NVV81(X), not E1NameInvP(X), BOX4P(X)])), 
always(or([not NVV83(X), E1NameInvP(X)])), 
always(or([not NVV83(X), not BOX4P(X)])), 
always(or([not NVV85(X), not E1NameInvF(X), BOX15F(X)])), 
always(or([not NVV87(X), E1NameInvF(X)])), 
always(or([not NVV87(X), not BOX15F(X)])), 
always(or([not NVV88(X), not PersonF(X), E1NameF(X)])), 
always(or([not NVV88(X), not PersonF(X), not E2NameF(X)])), 
always(or([not NVV88(X), not E2NameF(X), E1NameF(X)])), 
always(or([not NVV88(X), not E1NameF(X), BOX21F(X)])), 
always(or([not NVV88(X), not E2NameF(X), BOX22F(X)])), 
always(or([not NVV90(X), not E1NameF(X), PersonF(X), E1NameF(X), E2NameF(X)])), 
always(or([not NVV90(X), PersonF(X), E1NameF(X), E2NameF(X)])), 
always(or([not NVV90(X), PersonF(X), not E1NameF(X), E1NameF(X), E2NameF(X)])), 
always(or([not NVV90(X), not E1NameF(X), E1NameF(X), E2NameF(X)])), 
always(or([not NVV90(X), not E1NameF(X), PersonF(X), not BOX21F(X), E2NameF(X)])), 
always(or([not NVV90(X), PersonF(X), not BOX21F(X), E2NameF(X)])), 
always(or([not NVV90(X), PersonF(X), not E1NameF(X), not BOX21F(X), E2NameF(X)])), 
always(or([not NVV90(X), not E1NameF(X), not BOX21F(X), E2NameF(X)])), 
always(or([not NVV90(X), not E1NameF(X), PersonF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV90(X), PersonF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV90(X), not E1NameF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV90(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV90(X), PersonF(X), E2NameF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV90(X), E2NameF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV90(X), not E1NameF(X), PersonF(X), E2NameF(X), not BOX21F(X), not BOX22F(X)])), 
always(or([not NVV90(X), PersonF(X), E2NameF(X), not BOX21F(X), not BOX22F(X)])), 
always(or([not NVV90(X), not E1NameF(X), E2NameF(X), not BOX21F(X), not BOX22F(X)])), 
always(or([not NVV90(X), PersonF(X), not E1NameF(X), not BOX21F(X), not BOX22F(X)])), 
always(or([not NVV90(X), PersonF(X), E2NameF(X), not E1NameF(X), not BOX21F(X), not BOX22F(X)])), 
always(or([not NVV90(X), E2NameF(X), not E1NameF(X), not BOX21F(X), not BOX22F(X)])), 
always(or([not NVV95(X), BOX24F(X)])), 
always(or([not NVV97(X), not BOX24F(X)])),
always(or([not NVV1(X), next(NVV1(hidden(X)))])), 
always(or([not NVV1(constant(X)), next(NVV1(constant(X)))])), 
always(or([not NVV2(X), next(not BOX5P(hidden(X)))])), 
always(or([not NVV2(constant(X)), next(not BOX5P(constant(X)))])), 
always(or([not NVV3, next(PinvNameF)])), 
always(or([not NVV4, next(not PinvNameF)])), 
always(or([not NVV5(X), next(BOX5P(hidden(X)))])), 
always(or([not NVV5(constant(X)), next(BOX5P(constant(X)))])), 
always(or([not NVV6(X), next(NVV6(hidden(X)))])), 
always(or([not NVV6(constant(X)), next(NVV6(constant(X)))])), 
always(or([not NVV9, next(NVV9)])), 
always(or([not NVV12(X), next(NVV12(hidden(X)))])), 
always(or([not NVV12(constant(X)), next(NVV12(constant(X)))])), 
always(or([not NVV15(X), next(not BOX8P(hidden(X)))])), 
always(or([not NVV15(constant(X)), next(not BOX8P(constant(X)))])), 
always(or([not NVV16, next(PNameF)])), 
always(or([not NVV17, next(not PNameF)])), 
always(or([not NVV18(X), next(BOX8P(hidden(X)))])), 
always(or([not NVV18(constant(X)), next(BOX8P(constant(X)))])), 
always(or([not NVV19(X), next(NVV19(hidden(X)))])), 
always(or([not NVV19(constant(X)), next(NVV19(constant(X)))])), 
always(or([not NVV22(X), next(not BOX10P(hidden(X)))])), 
always(or([not NVV22(constant(X)), next(not BOX10P(constant(X)))])), 
always(or([not NVV23(X), next(BOX12P(hidden(X)))])), 
always(or([not NVV23(constant(X)), next(BOX12P(constant(X)))])), 
always(or([not NVV24(X), next(not BOX12P(hidden(X)))])), 
always(or([not NVV24(constant(X)), next(not BOX12P(constant(X)))])), 
always(or([not NVV25(X), next(BOX10P(hidden(X)))])), 
always(or([not NVV25(constant(X)), next(BOX10P(constant(X)))])), 
always(or([not NVV26(X), next(NVV26(hidden(X)))])), 
always(or([not NVV26(constant(X)), next(NVV26(constant(X)))])), 
always(or([not NVV29(X), next(not BOX11P(hidden(X)))])), 
always(or([not NVV29(constant(X)), next(not BOX11P(constant(X)))])), 
always(or([not NVV30(X), next(BOX13P(hidden(X)))])), 
always(or([not NVV30(constant(X)), next(BOX13P(constant(X)))])), 
always(or([not NVV31(X), next(not BOX13P(hidden(X)))])), 
always(or([not NVV31(constant(X)), next(not BOX13P(constant(X)))])), 
always(or([not NVV32(X), next(BOX11P(hidden(X)))])), 
always(or([not NVV32(constant(X)), next(BOX11P(constant(X)))])), 
always(or([not NVV33(X), next(not BOX9P(hidden(X)))])), 
always(or([not NVV33(constant(X)), next(not BOX9P(constant(X)))])), 
always(or([not NVV34(X), next(NVV35(hidden(X)))])), 
always(or([not NVV34(constant(X)), next(NVV35(constant(X)))])), 
always(or([not NVV36(X), next(NVV37(hidden(X)))])), 
always(or([not NVV36(constant(X)), next(NVV37(constant(X)))])), 
always(or([not NVV38(X), next(BOX9P(hidden(X)))])), 
always(or([not NVV38(constant(X)), next(BOX9P(constant(X)))])), 
always(or([not NVV39(X), next(not BOX23F(hidden(X)))])), 
always(or([not NVV39(constant(X)), next(not BOX23F(constant(X)))])), 
always(or([not NVV40(X), next(E1NameF(hidden(X)))])), 
always(or([not NVV40(constant(X)), next(E1NameF(constant(X)))])), 
always(or([not NVV41(X), next(not E1NameF(hidden(X)))])), 
always(or([not NVV41(constant(X)), next(not E1NameF(constant(X)))])), 
always(or([not NVV42(X), next(BOX23F(hidden(X)))])), 
always(or([not NVV42(constant(X)), next(BOX23F(constant(X)))])), 
always(or([not NVV43(X), next(NVV43(hidden(X)))])), 
always(or([not NVV43(constant(X)), next(NVV43(constant(X)))])), 
always(or([not NVV46(X), next(not BOX15F(hidden(X)))])), 
always(or([not NVV46(constant(X)), next(not BOX15F(constant(X)))])), 
always(or([not NVV47(X), next(BOX16F(hidden(X)))])), 
always(or([not NVV47(constant(X)), next(BOX16F(constant(X)))])), 
always(or([not NVV48(X), next(not BOX16F(hidden(X)))])), 
always(or([not NVV48(constant(X)), next(not BOX16F(constant(X)))])), 
always(or([not NVV49(X), next(BOX15F(hidden(X)))])), 
always(or([not NVV49(constant(X)), next(BOX15F(constant(X)))])), 
always(or([not NVV50(X), next(NVV50(hidden(X)))])), 
always(or([not NVV50(constant(X)), next(NVV50(constant(X)))])), 
always(or([not NVV53(X), next(NVV53(hidden(X)))])), 
always(or([not NVV53(constant(X)), next(NVV53(constant(X)))])), 
always(or([not NVV56(X), next(not BOX6P(hidden(X)))])), 
always(or([not NVV56(constant(X)), next(not BOX6P(constant(X)))])), 
always(or([not NVV57(X), next(NVV58(hidden(X)))])), 
always(or([not NVV57(constant(X)), next(NVV58(constant(X)))])), 
always(or([not NVV59(X), next(NVV60(hidden(X)))])), 
always(or([not NVV59(constant(X)), next(NVV60(constant(X)))])), 
always(or([not NVV61(X), next(BOX6P(hidden(X)))])), 
always(or([not NVV61(constant(X)), next(BOX6P(constant(X)))])), 
always(or([not NVV62(X), next(not BOX18F(hidden(X)))])), 
always(or([not NVV62(constant(X)), next(not BOX18F(constant(X)))])), 
always(or([not NVV63(X), next(BOX19F(hidden(X)))])), 
always(or([not NVV63(constant(X)), next(BOX19F(constant(X)))])), 
always(or([not NVV64(X), next(not BOX19F(hidden(X)))])), 
always(or([not NVV64(constant(X)), next(not BOX19F(constant(X)))])), 
always(or([not NVV65(X), next(BOX18F(hidden(X)))])), 
always(or([not NVV65(constant(X)), next(BOX18F(constant(X)))])), 
always(or([not NVV66(X), next(not BOX24F(hidden(X)))])), 
always(or([not NVV66(constant(X)), next(not BOX24F(constant(X)))])), 
always(or([not NVV67(X), next(E2NameF(hidden(X)))])), 
always(or([not NVV67(constant(X)), next(E2NameF(constant(X)))])), 
always(or([not NVV68(X), next(not E2NameF(hidden(X)))])), 
always(or([not NVV68(constant(X)), next(not E2NameF(constant(X)))])), 
always(or([not NVV69(X), next(BOX24F(hidden(X)))])), 
always(or([not NVV69(constant(X)), next(BOX24F(constant(X)))])), 
always(or([not NVV70(X), next(NVV70(hidden(X)))])), 
always(or([not NVV70(constant(X)), next(NVV70(constant(X)))])), 
always(or([not NVV73(X), next(NVV73(hidden(X)))])), 
always(or([not NVV73(constant(X)), next(NVV73(constant(X)))])), 
always(or([not NVV76, next(NVV76)])), 
always(or([not NVV79(X), next(not BOX3P(hidden(X)))])), 
always(or([not NVV79(constant(X)), next(not BOX3P(constant(X)))])), 
always(or([not NVV80(X), next(NVV81(hidden(X)))])), 
always(or([not NVV80(constant(X)), next(NVV81(constant(X)))])), 
always(or([not NVV82(X), next(NVV83(hidden(X)))])), 
always(or([not NVV82(constant(X)), next(NVV83(constant(X)))])), 
always(or([not NVV84(X), next(BOX3P(hidden(X)))])), 
always(or([not NVV84(constant(X)), next(BOX3P(constant(X)))])), 
always(or([not NVV85(X), next(NVV85(hidden(X)))])), 
always(or([not NVV85(constant(X)), next(NVV85(constant(X)))])), 
always(or([not NVV88(X), next(NVV88(hidden(X)))])), 
always(or([not NVV88(constant(X)), next(NVV88(constant(X)))])), 
always(or([not NVV91(X), next(not BOX2F(hidden(X)))])), 
always(or([not NVV91(constant(X)), next(not BOX2F(constant(X)))])), 
always(or([not NVV92(X), next(BOX20F(hidden(X)))])), 
always(or([not NVV92(constant(X)), next(BOX20F(constant(X)))])), 
always(or([not NVV93(X), next(not BOX20F(hidden(X)))])), 
always(or([not NVV93(constant(X)), next(not BOX20F(constant(X)))])), 
always(or([not NVV94(X), next(BOX2F(hidden(X)))])), 
always(or([not NVV94(constant(X)), next(BOX2F(constant(X)))])), 
always(or([not NVV95(X), next(NVV95(hidden(X)))])), 
always(or([not NVV95(constant(X)), next(NVV95(constant(X)))])), 
always(or([not NVV98(X), next(not BOX1F(hidden(X)))])), 
always(or([not NVV98(constant(X)), next(not BOX1F(constant(X)))])), 
always(or([not NVV99(X), next(BOX17F(hidden(X)))])), 
always(or([not NVV99(constant(X)), next(BOX17F(constant(X)))])), 
always(or([not NVV100(X), next(not BOX17F(hidden(X)))])), 
always(or([not NVV100(constant(X)), next(not BOX17F(constant(X)))])), 
always(or([not NVV101(X), next(BOX1F(hidden(X)))])), 
always(or([not NVV101(constant(X)), next(BOX1F(constant(X)))])), 
always(or([not NVV102(X), next(not BOX0F(hidden(X)))])), 
always(or([not NVV102(constant(X)), next(not BOX0F(constant(X)))])), 
always(or([not NVV103(X), next(BOX14F(hidden(X)))])), 
always(or([not NVV103(constant(X)), next(BOX14F(constant(X)))])), 
always(or([not NVV104(X), next(not BOX14F(hidden(X)))])), 
always(or([not NVV104(constant(X)), next(not BOX14F(constant(X)))])), 
always(or([not NVV105(X), next(BOX0F(hidden(X)))])), 
always(or([not NVV105(constant(X)), next(BOX0F(constant(X)))])),
always(or([not NVV7(X), sometime(NVV8(X))])), 
always(or([not NVV7(constant(dNameInv)), sometime(NVV8(constant(dNameInv)))])), 
always(or([not NVV7(constant(dName)), sometime(NVV8(constant(dName)))])), 
always(or([not NVV7(constant(N3)), sometime(NVV8(constant(N3)))])), 
always(or([not NVV7(constant(N21)), sometime(NVV8(constant(N21)))])), 
always(or([not NVV7(constant(N25)), sometime(NVV8(constant(N25)))])), 
always(or([not NVV7(constant(N39)), sometime(NVV8(constant(N39)))])), 
always(or([not NVV7(constant(N5)), sometime(NVV8(constant(N5)))])), 
always(or([not NVV7(constant(N22)), sometime(NVV8(constant(N22)))])), 
always(or([not NVV7(constant(N34)), sometime(NVV8(constant(N34)))])), 
always(or([not NVV7(constant(N2)), sometime(NVV8(constant(N2)))])), 
always(or([not NVV7(constant(N4)), sometime(NVV8(constant(N4)))])), 
always(or([not NVV7(constant(N12)), sometime(NVV8(constant(N12)))])), 
always(or([not NVV7(constant(N10)), sometime(NVV8(constant(N10)))])), 
always(or([not NVV7(constant(N0)), sometime(NVV8(constant(N0)))])), 
always(or([not NVV7(constant(N29)), sometime(NVV8(constant(N29)))])), 
always(or([not NVV7(constant(N18)), sometime(NVV8(constant(N18)))])), 
always(or([not NVV7(constant(N16)), sometime(NVV8(constant(N16)))])), 
always(or([not NVV7(constant(N14)), sometime(NVV8(constant(N14)))])), 
always(or([not NVV7(constant(N19)), sometime(NVV8(constant(N19)))])), 
always(or([not NVV7(constant(N37)), sometime(NVV8(constant(N37)))])), 
always(or([not NVV7(constant(N36)), sometime(NVV8(constant(N36)))])), 
always(or([not NVV7(constant(N11)), sometime(NVV8(constant(N11)))])), 
always(or([not NVV7(constant(N27)), sometime(NVV8(constant(N27)))])), 
always(or([not NVV7(constant(N13)), sometime(NVV8(constant(N13)))])), 
always(or([not NVV7(constant(N24)), sometime(NVV8(constant(N24)))])), 
always(or([not NVV7(constant(N8)), sometime(NVV8(constant(N8)))])), 
always(or([not NVV7(constant(N1)), sometime(NVV8(constant(N1)))])), 
always(or([not NVV7(constant(N30)), sometime(NVV8(constant(N30)))])), 
always(or([not NVV7(constant(N33)), sometime(NVV8(constant(N33)))])), 
always(or([not NVV7(constant(N15)), sometime(NVV8(constant(N15)))])), 
always(or([not NVV7(constant(N32)), sometime(NVV8(constant(N32)))])), 
always(or([not NVV7(constant(N23)), sometime(NVV8(constant(N23)))])), 
always(or([not NVV7(constant(N38)), sometime(NVV8(constant(N38)))])), 
always(or([not NVV7(constant(N26)), sometime(NVV8(constant(N26)))])), 
always(or([not NVV7(constant(N31)), sometime(NVV8(constant(N31)))])), 
always(or([not NVV7(constant(N6)), sometime(NVV8(constant(N6)))])), 
always(or([not NVV7(constant(N20)), sometime(NVV8(constant(N20)))])), 
always(or([not NVV7(constant(N7)), sometime(NVV8(constant(N7)))])), 
always(or([not NVV7(constant(N9)), sometime(NVV8(constant(N9)))])), 
always(or([not NVV7(constant(N17)), sometime(NVV8(constant(N17)))])), 
always(or([not NVV7(constant(N28)), sometime(NVV8(constant(N28)))])), 
always(or([not NVV7(constant(N35)), sometime(NVV8(constant(N35)))])), 
always(or([not NVV7(constant(John)), sometime(NVV8(constant(John)))])), 
always(or([not NVV10, sometime(NVV11)])), 
always(or([not NVV13(X), sometime(NVV14(X))])), 
always(or([not NVV13(constant(dNameInv)), sometime(NVV14(constant(dNameInv)))])), 
always(or([not NVV13(constant(dName)), sometime(NVV14(constant(dName)))])), 
always(or([not NVV13(constant(N3)), sometime(NVV14(constant(N3)))])), 
always(or([not NVV13(constant(N21)), sometime(NVV14(constant(N21)))])), 
always(or([not NVV13(constant(N25)), sometime(NVV14(constant(N25)))])), 
always(or([not NVV13(constant(N39)), sometime(NVV14(constant(N39)))])), 
always(or([not NVV13(constant(N5)), sometime(NVV14(constant(N5)))])), 
always(or([not NVV13(constant(N22)), sometime(NVV14(constant(N22)))])), 
always(or([not NVV13(constant(N34)), sometime(NVV14(constant(N34)))])), 
always(or([not NVV13(constant(N2)), sometime(NVV14(constant(N2)))])), 
always(or([not NVV13(constant(N4)), sometime(NVV14(constant(N4)))])), 
always(or([not NVV13(constant(N12)), sometime(NVV14(constant(N12)))])), 
always(or([not NVV13(constant(N10)), sometime(NVV14(constant(N10)))])), 
always(or([not NVV13(constant(N0)), sometime(NVV14(constant(N0)))])), 
always(or([not NVV13(constant(N29)), sometime(NVV14(constant(N29)))])), 
always(or([not NVV13(constant(N18)), sometime(NVV14(constant(N18)))])), 
always(or([not NVV13(constant(N16)), sometime(NVV14(constant(N16)))])), 
always(or([not NVV13(constant(N14)), sometime(NVV14(constant(N14)))])), 
always(or([not NVV13(constant(N19)), sometime(NVV14(constant(N19)))])), 
always(or([not NVV13(constant(N37)), sometime(NVV14(constant(N37)))])), 
always(or([not NVV13(constant(N36)), sometime(NVV14(constant(N36)))])), 
always(or([not NVV13(constant(N11)), sometime(NVV14(constant(N11)))])), 
always(or([not NVV13(constant(N27)), sometime(NVV14(constant(N27)))])), 
always(or([not NVV13(constant(N13)), sometime(NVV14(constant(N13)))])), 
always(or([not NVV13(constant(N24)), sometime(NVV14(constant(N24)))])), 
always(or([not NVV13(constant(N8)), sometime(NVV14(constant(N8)))])), 
always(or([not NVV13(constant(N1)), sometime(NVV14(constant(N1)))])), 
always(or([not NVV13(constant(N30)), sometime(NVV14(constant(N30)))])), 
always(or([not NVV13(constant(N33)), sometime(NVV14(constant(N33)))])), 
always(or([not NVV13(constant(N15)), sometime(NVV14(constant(N15)))])), 
always(or([not NVV13(constant(N32)), sometime(NVV14(constant(N32)))])), 
always(or([not NVV13(constant(N23)), sometime(NVV14(constant(N23)))])), 
always(or([not NVV13(constant(N38)), sometime(NVV14(constant(N38)))])), 
always(or([not NVV13(constant(N26)), sometime(NVV14(constant(N26)))])), 
always(or([not NVV13(constant(N31)), sometime(NVV14(constant(N31)))])), 
always(or([not NVV13(constant(N6)), sometime(NVV14(constant(N6)))])), 
always(or([not NVV13(constant(N20)), sometime(NVV14(constant(N20)))])), 
always(or([not NVV13(constant(N7)), sometime(NVV14(constant(N7)))])), 
always(or([not NVV13(constant(N9)), sometime(NVV14(constant(N9)))])), 
always(or([not NVV13(constant(N17)), sometime(NVV14(constant(N17)))])), 
always(or([not NVV13(constant(N28)), sometime(NVV14(constant(N28)))])), 
always(or([not NVV13(constant(N35)), sometime(NVV14(constant(N35)))])), 
always(or([not NVV13(constant(John)), sometime(NVV14(constant(John)))])), 
always(or([not NVV20(X), sometime(NVV21(X))])), 
always(or([not NVV20(constant(dNameInv)), sometime(NVV21(constant(dNameInv)))])), 
always(or([not NVV20(constant(dName)), sometime(NVV21(constant(dName)))])), 
always(or([not NVV20(constant(N3)), sometime(NVV21(constant(N3)))])), 
always(or([not NVV20(constant(N21)), sometime(NVV21(constant(N21)))])), 
always(or([not NVV20(constant(N25)), sometime(NVV21(constant(N25)))])), 
always(or([not NVV20(constant(N39)), sometime(NVV21(constant(N39)))])), 
always(or([not NVV20(constant(N5)), sometime(NVV21(constant(N5)))])), 
always(or([not NVV20(constant(N22)), sometime(NVV21(constant(N22)))])), 
always(or([not NVV20(constant(N34)), sometime(NVV21(constant(N34)))])), 
always(or([not NVV20(constant(N2)), sometime(NVV21(constant(N2)))])), 
always(or([not NVV20(constant(N4)), sometime(NVV21(constant(N4)))])), 
always(or([not NVV20(constant(N12)), sometime(NVV21(constant(N12)))])), 
always(or([not NVV20(constant(N10)), sometime(NVV21(constant(N10)))])), 
always(or([not NVV20(constant(N0)), sometime(NVV21(constant(N0)))])), 
always(or([not NVV20(constant(N29)), sometime(NVV21(constant(N29)))])), 
always(or([not NVV20(constant(N18)), sometime(NVV21(constant(N18)))])), 
always(or([not NVV20(constant(N16)), sometime(NVV21(constant(N16)))])), 
always(or([not NVV20(constant(N14)), sometime(NVV21(constant(N14)))])), 
always(or([not NVV20(constant(N19)), sometime(NVV21(constant(N19)))])), 
always(or([not NVV20(constant(N37)), sometime(NVV21(constant(N37)))])), 
always(or([not NVV20(constant(N36)), sometime(NVV21(constant(N36)))])), 
always(or([not NVV20(constant(N11)), sometime(NVV21(constant(N11)))])), 
always(or([not NVV20(constant(N27)), sometime(NVV21(constant(N27)))])), 
always(or([not NVV20(constant(N13)), sometime(NVV21(constant(N13)))])), 
always(or([not NVV20(constant(N24)), sometime(NVV21(constant(N24)))])), 
always(or([not NVV20(constant(N8)), sometime(NVV21(constant(N8)))])), 
always(or([not NVV20(constant(N1)), sometime(NVV21(constant(N1)))])), 
always(or([not NVV20(constant(N30)), sometime(NVV21(constant(N30)))])), 
always(or([not NVV20(constant(N33)), sometime(NVV21(constant(N33)))])), 
always(or([not NVV20(constant(N15)), sometime(NVV21(constant(N15)))])), 
always(or([not NVV20(constant(N32)), sometime(NVV21(constant(N32)))])), 
always(or([not NVV20(constant(N23)), sometime(NVV21(constant(N23)))])), 
always(or([not NVV20(constant(N38)), sometime(NVV21(constant(N38)))])), 
always(or([not NVV20(constant(N26)), sometime(NVV21(constant(N26)))])), 
always(or([not NVV20(constant(N31)), sometime(NVV21(constant(N31)))])), 
always(or([not NVV20(constant(N6)), sometime(NVV21(constant(N6)))])), 
always(or([not NVV20(constant(N20)), sometime(NVV21(constant(N20)))])), 
always(or([not NVV20(constant(N7)), sometime(NVV21(constant(N7)))])), 
always(or([not NVV20(constant(N9)), sometime(NVV21(constant(N9)))])), 
always(or([not NVV20(constant(N17)), sometime(NVV21(constant(N17)))])), 
always(or([not NVV20(constant(N28)), sometime(NVV21(constant(N28)))])), 
always(or([not NVV20(constant(N35)), sometime(NVV21(constant(N35)))])), 
always(or([not NVV20(constant(John)), sometime(NVV21(constant(John)))])), 
always(or([not NVV27(X), sometime(NVV28(X))])), 
always(or([not NVV27(constant(dNameInv)), sometime(NVV28(constant(dNameInv)))])), 
always(or([not NVV27(constant(dName)), sometime(NVV28(constant(dName)))])), 
always(or([not NVV27(constant(N3)), sometime(NVV28(constant(N3)))])), 
always(or([not NVV27(constant(N21)), sometime(NVV28(constant(N21)))])), 
always(or([not NVV27(constant(N25)), sometime(NVV28(constant(N25)))])), 
always(or([not NVV27(constant(N39)), sometime(NVV28(constant(N39)))])), 
always(or([not NVV27(constant(N5)), sometime(NVV28(constant(N5)))])), 
always(or([not NVV27(constant(N22)), sometime(NVV28(constant(N22)))])), 
always(or([not NVV27(constant(N34)), sometime(NVV28(constant(N34)))])), 
always(or([not NVV27(constant(N2)), sometime(NVV28(constant(N2)))])), 
always(or([not NVV27(constant(N4)), sometime(NVV28(constant(N4)))])), 
always(or([not NVV27(constant(N12)), sometime(NVV28(constant(N12)))])), 
always(or([not NVV27(constant(N10)), sometime(NVV28(constant(N10)))])), 
always(or([not NVV27(constant(N0)), sometime(NVV28(constant(N0)))])), 
always(or([not NVV27(constant(N29)), sometime(NVV28(constant(N29)))])), 
always(or([not NVV27(constant(N18)), sometime(NVV28(constant(N18)))])), 
always(or([not NVV27(constant(N16)), sometime(NVV28(constant(N16)))])), 
always(or([not NVV27(constant(N14)), sometime(NVV28(constant(N14)))])), 
always(or([not NVV27(constant(N19)), sometime(NVV28(constant(N19)))])), 
always(or([not NVV27(constant(N37)), sometime(NVV28(constant(N37)))])), 
always(or([not NVV27(constant(N36)), sometime(NVV28(constant(N36)))])), 
always(or([not NVV27(constant(N11)), sometime(NVV28(constant(N11)))])), 
always(or([not NVV27(constant(N27)), sometime(NVV28(constant(N27)))])), 
always(or([not NVV27(constant(N13)), sometime(NVV28(constant(N13)))])), 
always(or([not NVV27(constant(N24)), sometime(NVV28(constant(N24)))])), 
always(or([not NVV27(constant(N8)), sometime(NVV28(constant(N8)))])), 
always(or([not NVV27(constant(N1)), sometime(NVV28(constant(N1)))])), 
always(or([not NVV27(constant(N30)), sometime(NVV28(constant(N30)))])), 
always(or([not NVV27(constant(N33)), sometime(NVV28(constant(N33)))])), 
always(or([not NVV27(constant(N15)), sometime(NVV28(constant(N15)))])), 
always(or([not NVV27(constant(N32)), sometime(NVV28(constant(N32)))])), 
always(or([not NVV27(constant(N23)), sometime(NVV28(constant(N23)))])), 
always(or([not NVV27(constant(N38)), sometime(NVV28(constant(N38)))])), 
always(or([not NVV27(constant(N26)), sometime(NVV28(constant(N26)))])), 
always(or([not NVV27(constant(N31)), sometime(NVV28(constant(N31)))])), 
always(or([not NVV27(constant(N6)), sometime(NVV28(constant(N6)))])), 
always(or([not NVV27(constant(N20)), sometime(NVV28(constant(N20)))])), 
always(or([not NVV27(constant(N7)), sometime(NVV28(constant(N7)))])), 
always(or([not NVV27(constant(N9)), sometime(NVV28(constant(N9)))])), 
always(or([not NVV27(constant(N17)), sometime(NVV28(constant(N17)))])), 
always(or([not NVV27(constant(N28)), sometime(NVV28(constant(N28)))])), 
always(or([not NVV27(constant(N35)), sometime(NVV28(constant(N35)))])), 
always(or([not NVV27(constant(John)), sometime(NVV28(constant(John)))])), 
always(or([not NVV44(X), sometime(NVV45(X))])), 
always(or([not NVV44(constant(dNameInv)), sometime(NVV45(constant(dNameInv)))])), 
always(or([not NVV44(constant(dName)), sometime(NVV45(constant(dName)))])), 
always(or([not NVV44(constant(N3)), sometime(NVV45(constant(N3)))])), 
always(or([not NVV44(constant(N21)), sometime(NVV45(constant(N21)))])), 
always(or([not NVV44(constant(N25)), sometime(NVV45(constant(N25)))])), 
always(or([not NVV44(constant(N39)), sometime(NVV45(constant(N39)))])), 
always(or([not NVV44(constant(N5)), sometime(NVV45(constant(N5)))])), 
always(or([not NVV44(constant(N22)), sometime(NVV45(constant(N22)))])), 
always(or([not NVV44(constant(N34)), sometime(NVV45(constant(N34)))])), 
always(or([not NVV44(constant(N2)), sometime(NVV45(constant(N2)))])), 
always(or([not NVV44(constant(N4)), sometime(NVV45(constant(N4)))])), 
always(or([not NVV44(constant(N12)), sometime(NVV45(constant(N12)))])), 
always(or([not NVV44(constant(N10)), sometime(NVV45(constant(N10)))])), 
always(or([not NVV44(constant(N0)), sometime(NVV45(constant(N0)))])), 
always(or([not NVV44(constant(N29)), sometime(NVV45(constant(N29)))])), 
always(or([not NVV44(constant(N18)), sometime(NVV45(constant(N18)))])), 
always(or([not NVV44(constant(N16)), sometime(NVV45(constant(N16)))])), 
always(or([not NVV44(constant(N14)), sometime(NVV45(constant(N14)))])), 
always(or([not NVV44(constant(N19)), sometime(NVV45(constant(N19)))])), 
always(or([not NVV44(constant(N37)), sometime(NVV45(constant(N37)))])), 
always(or([not NVV44(constant(N36)), sometime(NVV45(constant(N36)))])), 
always(or([not NVV44(constant(N11)), sometime(NVV45(constant(N11)))])), 
always(or([not NVV44(constant(N27)), sometime(NVV45(constant(N27)))])), 
always(or([not NVV44(constant(N13)), sometime(NVV45(constant(N13)))])), 
always(or([not NVV44(constant(N24)), sometime(NVV45(constant(N24)))])), 
always(or([not NVV44(constant(N8)), sometime(NVV45(constant(N8)))])), 
always(or([not NVV44(constant(N1)), sometime(NVV45(constant(N1)))])), 
always(or([not NVV44(constant(N30)), sometime(NVV45(constant(N30)))])), 
always(or([not NVV44(constant(N33)), sometime(NVV45(constant(N33)))])), 
always(or([not NVV44(constant(N15)), sometime(NVV45(constant(N15)))])), 
always(or([not NVV44(constant(N32)), sometime(NVV45(constant(N32)))])), 
always(or([not NVV44(constant(N23)), sometime(NVV45(constant(N23)))])), 
always(or([not NVV44(constant(N38)), sometime(NVV45(constant(N38)))])), 
always(or([not NVV44(constant(N26)), sometime(NVV45(constant(N26)))])), 
always(or([not NVV44(constant(N31)), sometime(NVV45(constant(N31)))])), 
always(or([not NVV44(constant(N6)), sometime(NVV45(constant(N6)))])), 
always(or([not NVV44(constant(N20)), sometime(NVV45(constant(N20)))])), 
always(or([not NVV44(constant(N7)), sometime(NVV45(constant(N7)))])), 
always(or([not NVV44(constant(N9)), sometime(NVV45(constant(N9)))])), 
always(or([not NVV44(constant(N17)), sometime(NVV45(constant(N17)))])), 
always(or([not NVV44(constant(N28)), sometime(NVV45(constant(N28)))])), 
always(or([not NVV44(constant(N35)), sometime(NVV45(constant(N35)))])), 
always(or([not NVV44(constant(John)), sometime(NVV45(constant(John)))])), 
always(or([not NVV51(X), sometime(NVV52(X))])), 
always(or([not NVV51(constant(dNameInv)), sometime(NVV52(constant(dNameInv)))])), 
always(or([not NVV51(constant(dName)), sometime(NVV52(constant(dName)))])), 
always(or([not NVV51(constant(N3)), sometime(NVV52(constant(N3)))])), 
always(or([not NVV51(constant(N21)), sometime(NVV52(constant(N21)))])), 
always(or([not NVV51(constant(N25)), sometime(NVV52(constant(N25)))])), 
always(or([not NVV51(constant(N39)), sometime(NVV52(constant(N39)))])), 
always(or([not NVV51(constant(N5)), sometime(NVV52(constant(N5)))])), 
always(or([not NVV51(constant(N22)), sometime(NVV52(constant(N22)))])), 
always(or([not NVV51(constant(N34)), sometime(NVV52(constant(N34)))])), 
always(or([not NVV51(constant(N2)), sometime(NVV52(constant(N2)))])), 
always(or([not NVV51(constant(N4)), sometime(NVV52(constant(N4)))])), 
always(or([not NVV51(constant(N12)), sometime(NVV52(constant(N12)))])), 
always(or([not NVV51(constant(N10)), sometime(NVV52(constant(N10)))])), 
always(or([not NVV51(constant(N0)), sometime(NVV52(constant(N0)))])), 
always(or([not NVV51(constant(N29)), sometime(NVV52(constant(N29)))])), 
always(or([not NVV51(constant(N18)), sometime(NVV52(constant(N18)))])), 
always(or([not NVV51(constant(N16)), sometime(NVV52(constant(N16)))])), 
always(or([not NVV51(constant(N14)), sometime(NVV52(constant(N14)))])), 
always(or([not NVV51(constant(N19)), sometime(NVV52(constant(N19)))])), 
always(or([not NVV51(constant(N37)), sometime(NVV52(constant(N37)))])), 
always(or([not NVV51(constant(N36)), sometime(NVV52(constant(N36)))])), 
always(or([not NVV51(constant(N11)), sometime(NVV52(constant(N11)))])), 
always(or([not NVV51(constant(N27)), sometime(NVV52(constant(N27)))])), 
always(or([not NVV51(constant(N13)), sometime(NVV52(constant(N13)))])), 
always(or([not NVV51(constant(N24)), sometime(NVV52(constant(N24)))])), 
always(or([not NVV51(constant(N8)), sometime(NVV52(constant(N8)))])), 
always(or([not NVV51(constant(N1)), sometime(NVV52(constant(N1)))])), 
always(or([not NVV51(constant(N30)), sometime(NVV52(constant(N30)))])), 
always(or([not NVV51(constant(N33)), sometime(NVV52(constant(N33)))])), 
always(or([not NVV51(constant(N15)), sometime(NVV52(constant(N15)))])), 
always(or([not NVV51(constant(N32)), sometime(NVV52(constant(N32)))])), 
always(or([not NVV51(constant(N23)), sometime(NVV52(constant(N23)))])), 
always(or([not NVV51(constant(N38)), sometime(NVV52(constant(N38)))])), 
always(or([not NVV51(constant(N26)), sometime(NVV52(constant(N26)))])), 
always(or([not NVV51(constant(N31)), sometime(NVV52(constant(N31)))])), 
always(or([not NVV51(constant(N6)), sometime(NVV52(constant(N6)))])), 
always(or([not NVV51(constant(N20)), sometime(NVV52(constant(N20)))])), 
always(or([not NVV51(constant(N7)), sometime(NVV52(constant(N7)))])), 
always(or([not NVV51(constant(N9)), sometime(NVV52(constant(N9)))])), 
always(or([not NVV51(constant(N17)), sometime(NVV52(constant(N17)))])), 
always(or([not NVV51(constant(N28)), sometime(NVV52(constant(N28)))])), 
always(or([not NVV51(constant(N35)), sometime(NVV52(constant(N35)))])), 
always(or([not NVV51(constant(John)), sometime(NVV52(constant(John)))])), 
always(or([not NVV54(X), sometime(NVV55(X))])), 
always(or([not NVV54(constant(dNameInv)), sometime(NVV55(constant(dNameInv)))])), 
always(or([not NVV54(constant(dName)), sometime(NVV55(constant(dName)))])), 
always(or([not NVV54(constant(N3)), sometime(NVV55(constant(N3)))])), 
always(or([not NVV54(constant(N21)), sometime(NVV55(constant(N21)))])), 
always(or([not NVV54(constant(N25)), sometime(NVV55(constant(N25)))])), 
always(or([not NVV54(constant(N39)), sometime(NVV55(constant(N39)))])), 
always(or([not NVV54(constant(N5)), sometime(NVV55(constant(N5)))])), 
always(or([not NVV54(constant(N22)), sometime(NVV55(constant(N22)))])), 
always(or([not NVV54(constant(N34)), sometime(NVV55(constant(N34)))])), 
always(or([not NVV54(constant(N2)), sometime(NVV55(constant(N2)))])), 
always(or([not NVV54(constant(N4)), sometime(NVV55(constant(N4)))])), 
always(or([not NVV54(constant(N12)), sometime(NVV55(constant(N12)))])), 
always(or([not NVV54(constant(N10)), sometime(NVV55(constant(N10)))])), 
always(or([not NVV54(constant(N0)), sometime(NVV55(constant(N0)))])), 
always(or([not NVV54(constant(N29)), sometime(NVV55(constant(N29)))])), 
always(or([not NVV54(constant(N18)), sometime(NVV55(constant(N18)))])), 
always(or([not NVV54(constant(N16)), sometime(NVV55(constant(N16)))])), 
always(or([not NVV54(constant(N14)), sometime(NVV55(constant(N14)))])), 
always(or([not NVV54(constant(N19)), sometime(NVV55(constant(N19)))])), 
always(or([not NVV54(constant(N37)), sometime(NVV55(constant(N37)))])), 
always(or([not NVV54(constant(N36)), sometime(NVV55(constant(N36)))])), 
always(or([not NVV54(constant(N11)), sometime(NVV55(constant(N11)))])), 
always(or([not NVV54(constant(N27)), sometime(NVV55(constant(N27)))])), 
always(or([not NVV54(constant(N13)), sometime(NVV55(constant(N13)))])), 
always(or([not NVV54(constant(N24)), sometime(NVV55(constant(N24)))])), 
always(or([not NVV54(constant(N8)), sometime(NVV55(constant(N8)))])), 
always(or([not NVV54(constant(N1)), sometime(NVV55(constant(N1)))])), 
always(or([not NVV54(constant(N30)), sometime(NVV55(constant(N30)))])), 
always(or([not NVV54(constant(N33)), sometime(NVV55(constant(N33)))])), 
always(or([not NVV54(constant(N15)), sometime(NVV55(constant(N15)))])), 
always(or([not NVV54(constant(N32)), sometime(NVV55(constant(N32)))])), 
always(or([not NVV54(constant(N23)), sometime(NVV55(constant(N23)))])), 
always(or([not NVV54(constant(N38)), sometime(NVV55(constant(N38)))])), 
always(or([not NVV54(constant(N26)), sometime(NVV55(constant(N26)))])), 
always(or([not NVV54(constant(N31)), sometime(NVV55(constant(N31)))])), 
always(or([not NVV54(constant(N6)), sometime(NVV55(constant(N6)))])), 
always(or([not NVV54(constant(N20)), sometime(NVV55(constant(N20)))])), 
always(or([not NVV54(constant(N7)), sometime(NVV55(constant(N7)))])), 
always(or([not NVV54(constant(N9)), sometime(NVV55(constant(N9)))])), 
always(or([not NVV54(constant(N17)), sometime(NVV55(constant(N17)))])), 
always(or([not NVV54(constant(N28)), sometime(NVV55(constant(N28)))])), 
always(or([not NVV54(constant(N35)), sometime(NVV55(constant(N35)))])), 
always(or([not NVV54(constant(John)), sometime(NVV55(constant(John)))])), 
always(or([not NVV71(X), sometime(NVV72(X))])), 
always(or([not NVV71(constant(dNameInv)), sometime(NVV72(constant(dNameInv)))])), 
always(or([not NVV71(constant(dName)), sometime(NVV72(constant(dName)))])), 
always(or([not NVV71(constant(N3)), sometime(NVV72(constant(N3)))])), 
always(or([not NVV71(constant(N21)), sometime(NVV72(constant(N21)))])), 
always(or([not NVV71(constant(N25)), sometime(NVV72(constant(N25)))])), 
always(or([not NVV71(constant(N39)), sometime(NVV72(constant(N39)))])), 
always(or([not NVV71(constant(N5)), sometime(NVV72(constant(N5)))])), 
always(or([not NVV71(constant(N22)), sometime(NVV72(constant(N22)))])), 
always(or([not NVV71(constant(N34)), sometime(NVV72(constant(N34)))])), 
always(or([not NVV71(constant(N2)), sometime(NVV72(constant(N2)))])), 
always(or([not NVV71(constant(N4)), sometime(NVV72(constant(N4)))])), 
always(or([not NVV71(constant(N12)), sometime(NVV72(constant(N12)))])), 
always(or([not NVV71(constant(N10)), sometime(NVV72(constant(N10)))])), 
always(or([not NVV71(constant(N0)), sometime(NVV72(constant(N0)))])), 
always(or([not NVV71(constant(N29)), sometime(NVV72(constant(N29)))])), 
always(or([not NVV71(constant(N18)), sometime(NVV72(constant(N18)))])), 
always(or([not NVV71(constant(N16)), sometime(NVV72(constant(N16)))])), 
always(or([not NVV71(constant(N14)), sometime(NVV72(constant(N14)))])), 
always(or([not NVV71(constant(N19)), sometime(NVV72(constant(N19)))])), 
always(or([not NVV71(constant(N37)), sometime(NVV72(constant(N37)))])), 
always(or([not NVV71(constant(N36)), sometime(NVV72(constant(N36)))])), 
always(or([not NVV71(constant(N11)), sometime(NVV72(constant(N11)))])), 
always(or([not NVV71(constant(N27)), sometime(NVV72(constant(N27)))])), 
always(or([not NVV71(constant(N13)), sometime(NVV72(constant(N13)))])), 
always(or([not NVV71(constant(N24)), sometime(NVV72(constant(N24)))])), 
always(or([not NVV71(constant(N8)), sometime(NVV72(constant(N8)))])), 
always(or([not NVV71(constant(N1)), sometime(NVV72(constant(N1)))])), 
always(or([not NVV71(constant(N30)), sometime(NVV72(constant(N30)))])), 
always(or([not NVV71(constant(N33)), sometime(NVV72(constant(N33)))])), 
always(or([not NVV71(constant(N15)), sometime(NVV72(constant(N15)))])), 
always(or([not NVV71(constant(N32)), sometime(NVV72(constant(N32)))])), 
always(or([not NVV71(constant(N23)), sometime(NVV72(constant(N23)))])), 
always(or([not NVV71(constant(N38)), sometime(NVV72(constant(N38)))])), 
always(or([not NVV71(constant(N26)), sometime(NVV72(constant(N26)))])), 
always(or([not NVV71(constant(N31)), sometime(NVV72(constant(N31)))])), 
always(or([not NVV71(constant(N6)), sometime(NVV72(constant(N6)))])), 
always(or([not NVV71(constant(N20)), sometime(NVV72(constant(N20)))])), 
always(or([not NVV71(constant(N7)), sometime(NVV72(constant(N7)))])), 
always(or([not NVV71(constant(N9)), sometime(NVV72(constant(N9)))])), 
always(or([not NVV71(constant(N17)), sometime(NVV72(constant(N17)))])), 
always(or([not NVV71(constant(N28)), sometime(NVV72(constant(N28)))])), 
always(or([not NVV71(constant(N35)), sometime(NVV72(constant(N35)))])), 
always(or([not NVV71(constant(John)), sometime(NVV72(constant(John)))])), 
always(or([not NVV74(X), sometime(NVV75(X))])), 
always(or([not NVV74(constant(dNameInv)), sometime(NVV75(constant(dNameInv)))])), 
always(or([not NVV74(constant(dName)), sometime(NVV75(constant(dName)))])), 
always(or([not NVV74(constant(N3)), sometime(NVV75(constant(N3)))])), 
always(or([not NVV74(constant(N21)), sometime(NVV75(constant(N21)))])), 
always(or([not NVV74(constant(N25)), sometime(NVV75(constant(N25)))])), 
always(or([not NVV74(constant(N39)), sometime(NVV75(constant(N39)))])), 
always(or([not NVV74(constant(N5)), sometime(NVV75(constant(N5)))])), 
always(or([not NVV74(constant(N22)), sometime(NVV75(constant(N22)))])), 
always(or([not NVV74(constant(N34)), sometime(NVV75(constant(N34)))])), 
always(or([not NVV74(constant(N2)), sometime(NVV75(constant(N2)))])), 
always(or([not NVV74(constant(N4)), sometime(NVV75(constant(N4)))])), 
always(or([not NVV74(constant(N12)), sometime(NVV75(constant(N12)))])), 
always(or([not NVV74(constant(N10)), sometime(NVV75(constant(N10)))])), 
always(or([not NVV74(constant(N0)), sometime(NVV75(constant(N0)))])), 
always(or([not NVV74(constant(N29)), sometime(NVV75(constant(N29)))])), 
always(or([not NVV74(constant(N18)), sometime(NVV75(constant(N18)))])), 
always(or([not NVV74(constant(N16)), sometime(NVV75(constant(N16)))])), 
always(or([not NVV74(constant(N14)), sometime(NVV75(constant(N14)))])), 
always(or([not NVV74(constant(N19)), sometime(NVV75(constant(N19)))])), 
always(or([not NVV74(constant(N37)), sometime(NVV75(constant(N37)))])), 
always(or([not NVV74(constant(N36)), sometime(NVV75(constant(N36)))])), 
always(or([not NVV74(constant(N11)), sometime(NVV75(constant(N11)))])), 
always(or([not NVV74(constant(N27)), sometime(NVV75(constant(N27)))])), 
always(or([not NVV74(constant(N13)), sometime(NVV75(constant(N13)))])), 
always(or([not NVV74(constant(N24)), sometime(NVV75(constant(N24)))])), 
always(or([not NVV74(constant(N8)), sometime(NVV75(constant(N8)))])), 
always(or([not NVV74(constant(N1)), sometime(NVV75(constant(N1)))])), 
always(or([not NVV74(constant(N30)), sometime(NVV75(constant(N30)))])), 
always(or([not NVV74(constant(N33)), sometime(NVV75(constant(N33)))])), 
always(or([not NVV74(constant(N15)), sometime(NVV75(constant(N15)))])), 
always(or([not NVV74(constant(N32)), sometime(NVV75(constant(N32)))])), 
always(or([not NVV74(constant(N23)), sometime(NVV75(constant(N23)))])), 
always(or([not NVV74(constant(N38)), sometime(NVV75(constant(N38)))])), 
always(or([not NVV74(constant(N26)), sometime(NVV75(constant(N26)))])), 
always(or([not NVV74(constant(N31)), sometime(NVV75(constant(N31)))])), 
always(or([not NVV74(constant(N6)), sometime(NVV75(constant(N6)))])), 
always(or([not NVV74(constant(N20)), sometime(NVV75(constant(N20)))])), 
always(or([not NVV74(constant(N7)), sometime(NVV75(constant(N7)))])), 
always(or([not NVV74(constant(N9)), sometime(NVV75(constant(N9)))])), 
always(or([not NVV74(constant(N17)), sometime(NVV75(constant(N17)))])), 
always(or([not NVV74(constant(N28)), sometime(NVV75(constant(N28)))])), 
always(or([not NVV74(constant(N35)), sometime(NVV75(constant(N35)))])), 
always(or([not NVV74(constant(John)), sometime(NVV75(constant(John)))])), 
always(or([not NVV77, sometime(NVV78)])), 
always(or([not NVV86(X), sometime(NVV87(X))])), 
always(or([not NVV86(constant(dNameInv)), sometime(NVV87(constant(dNameInv)))])), 
always(or([not NVV86(constant(dName)), sometime(NVV87(constant(dName)))])), 
always(or([not NVV86(constant(N3)), sometime(NVV87(constant(N3)))])), 
always(or([not NVV86(constant(N21)), sometime(NVV87(constant(N21)))])), 
always(or([not NVV86(constant(N25)), sometime(NVV87(constant(N25)))])), 
always(or([not NVV86(constant(N39)), sometime(NVV87(constant(N39)))])), 
always(or([not NVV86(constant(N5)), sometime(NVV87(constant(N5)))])), 
always(or([not NVV86(constant(N22)), sometime(NVV87(constant(N22)))])), 
always(or([not NVV86(constant(N34)), sometime(NVV87(constant(N34)))])), 
always(or([not NVV86(constant(N2)), sometime(NVV87(constant(N2)))])), 
always(or([not NVV86(constant(N4)), sometime(NVV87(constant(N4)))])), 
always(or([not NVV86(constant(N12)), sometime(NVV87(constant(N12)))])), 
always(or([not NVV86(constant(N10)), sometime(NVV87(constant(N10)))])), 
always(or([not NVV86(constant(N0)), sometime(NVV87(constant(N0)))])), 
always(or([not NVV86(constant(N29)), sometime(NVV87(constant(N29)))])), 
always(or([not NVV86(constant(N18)), sometime(NVV87(constant(N18)))])), 
always(or([not NVV86(constant(N16)), sometime(NVV87(constant(N16)))])), 
always(or([not NVV86(constant(N14)), sometime(NVV87(constant(N14)))])), 
always(or([not NVV86(constant(N19)), sometime(NVV87(constant(N19)))])), 
always(or([not NVV86(constant(N37)), sometime(NVV87(constant(N37)))])), 
always(or([not NVV86(constant(N36)), sometime(NVV87(constant(N36)))])), 
always(or([not NVV86(constant(N11)), sometime(NVV87(constant(N11)))])), 
always(or([not NVV86(constant(N27)), sometime(NVV87(constant(N27)))])), 
always(or([not NVV86(constant(N13)), sometime(NVV87(constant(N13)))])), 
always(or([not NVV86(constant(N24)), sometime(NVV87(constant(N24)))])), 
always(or([not NVV86(constant(N8)), sometime(NVV87(constant(N8)))])), 
always(or([not NVV86(constant(N1)), sometime(NVV87(constant(N1)))])), 
always(or([not NVV86(constant(N30)), sometime(NVV87(constant(N30)))])), 
always(or([not NVV86(constant(N33)), sometime(NVV87(constant(N33)))])), 
always(or([not NVV86(constant(N15)), sometime(NVV87(constant(N15)))])), 
always(or([not NVV86(constant(N32)), sometime(NVV87(constant(N32)))])), 
always(or([not NVV86(constant(N23)), sometime(NVV87(constant(N23)))])), 
always(or([not NVV86(constant(N38)), sometime(NVV87(constant(N38)))])), 
always(or([not NVV86(constant(N26)), sometime(NVV87(constant(N26)))])), 
always(or([not NVV86(constant(N31)), sometime(NVV87(constant(N31)))])), 
always(or([not NVV86(constant(N6)), sometime(NVV87(constant(N6)))])), 
always(or([not NVV86(constant(N20)), sometime(NVV87(constant(N20)))])), 
always(or([not NVV86(constant(N7)), sometime(NVV87(constant(N7)))])), 
always(or([not NVV86(constant(N9)), sometime(NVV87(constant(N9)))])), 
always(or([not NVV86(constant(N17)), sometime(NVV87(constant(N17)))])), 
always(or([not NVV86(constant(N28)), sometime(NVV87(constant(N28)))])), 
always(or([not NVV86(constant(N35)), sometime(NVV87(constant(N35)))])), 
always(or([not NVV86(constant(John)), sometime(NVV87(constant(John)))])), 
always(or([not NVV89(X), sometime(NVV90(X))])), 
always(or([not NVV89(constant(dNameInv)), sometime(NVV90(constant(dNameInv)))])), 
always(or([not NVV89(constant(dName)), sometime(NVV90(constant(dName)))])), 
always(or([not NVV89(constant(N3)), sometime(NVV90(constant(N3)))])), 
always(or([not NVV89(constant(N21)), sometime(NVV90(constant(N21)))])), 
always(or([not NVV89(constant(N25)), sometime(NVV90(constant(N25)))])), 
always(or([not NVV89(constant(N39)), sometime(NVV90(constant(N39)))])), 
always(or([not NVV89(constant(N5)), sometime(NVV90(constant(N5)))])), 
always(or([not NVV89(constant(N22)), sometime(NVV90(constant(N22)))])), 
always(or([not NVV89(constant(N34)), sometime(NVV90(constant(N34)))])), 
always(or([not NVV89(constant(N2)), sometime(NVV90(constant(N2)))])), 
always(or([not NVV89(constant(N4)), sometime(NVV90(constant(N4)))])), 
always(or([not NVV89(constant(N12)), sometime(NVV90(constant(N12)))])), 
always(or([not NVV89(constant(N10)), sometime(NVV90(constant(N10)))])), 
always(or([not NVV89(constant(N0)), sometime(NVV90(constant(N0)))])), 
always(or([not NVV89(constant(N29)), sometime(NVV90(constant(N29)))])), 
always(or([not NVV89(constant(N18)), sometime(NVV90(constant(N18)))])), 
always(or([not NVV89(constant(N16)), sometime(NVV90(constant(N16)))])), 
always(or([not NVV89(constant(N14)), sometime(NVV90(constant(N14)))])), 
always(or([not NVV89(constant(N19)), sometime(NVV90(constant(N19)))])), 
always(or([not NVV89(constant(N37)), sometime(NVV90(constant(N37)))])), 
always(or([not NVV89(constant(N36)), sometime(NVV90(constant(N36)))])), 
always(or([not NVV89(constant(N11)), sometime(NVV90(constant(N11)))])), 
always(or([not NVV89(constant(N27)), sometime(NVV90(constant(N27)))])), 
always(or([not NVV89(constant(N13)), sometime(NVV90(constant(N13)))])), 
always(or([not NVV89(constant(N24)), sometime(NVV90(constant(N24)))])), 
always(or([not NVV89(constant(N8)), sometime(NVV90(constant(N8)))])), 
always(or([not NVV89(constant(N1)), sometime(NVV90(constant(N1)))])), 
always(or([not NVV89(constant(N30)), sometime(NVV90(constant(N30)))])), 
always(or([not NVV89(constant(N33)), sometime(NVV90(constant(N33)))])), 
always(or([not NVV89(constant(N15)), sometime(NVV90(constant(N15)))])), 
always(or([not NVV89(constant(N32)), sometime(NVV90(constant(N32)))])), 
always(or([not NVV89(constant(N23)), sometime(NVV90(constant(N23)))])), 
always(or([not NVV89(constant(N38)), sometime(NVV90(constant(N38)))])), 
always(or([not NVV89(constant(N26)), sometime(NVV90(constant(N26)))])), 
always(or([not NVV89(constant(N31)), sometime(NVV90(constant(N31)))])), 
always(or([not NVV89(constant(N6)), sometime(NVV90(constant(N6)))])), 
always(or([not NVV89(constant(N20)), sometime(NVV90(constant(N20)))])), 
always(or([not NVV89(constant(N7)), sometime(NVV90(constant(N7)))])), 
always(or([not NVV89(constant(N9)), sometime(NVV90(constant(N9)))])), 
always(or([not NVV89(constant(N17)), sometime(NVV90(constant(N17)))])), 
always(or([not NVV89(constant(N28)), sometime(NVV90(constant(N28)))])), 
always(or([not NVV89(constant(N35)), sometime(NVV90(constant(N35)))])), 
always(or([not NVV89(constant(John)), sometime(NVV90(constant(John)))])), 
always(or([not NVV96(X), sometime(NVV97(X))])), 
always(or([not NVV96(constant(dNameInv)), sometime(NVV97(constant(dNameInv)))])), 
always(or([not NVV96(constant(dName)), sometime(NVV97(constant(dName)))])), 
always(or([not NVV96(constant(N3)), sometime(NVV97(constant(N3)))])), 
always(or([not NVV96(constant(N21)), sometime(NVV97(constant(N21)))])), 
always(or([not NVV96(constant(N25)), sometime(NVV97(constant(N25)))])), 
always(or([not NVV96(constant(N39)), sometime(NVV97(constant(N39)))])), 
always(or([not NVV96(constant(N5)), sometime(NVV97(constant(N5)))])), 
always(or([not NVV96(constant(N22)), sometime(NVV97(constant(N22)))])), 
always(or([not NVV96(constant(N34)), sometime(NVV97(constant(N34)))])), 
always(or([not NVV96(constant(N2)), sometime(NVV97(constant(N2)))])), 
always(or([not NVV96(constant(N4)), sometime(NVV97(constant(N4)))])), 
always(or([not NVV96(constant(N12)), sometime(NVV97(constant(N12)))])), 
always(or([not NVV96(constant(N10)), sometime(NVV97(constant(N10)))])), 
always(or([not NVV96(constant(N0)), sometime(NVV97(constant(N0)))])), 
always(or([not NVV96(constant(N29)), sometime(NVV97(constant(N29)))])), 
always(or([not NVV96(constant(N18)), sometime(NVV97(constant(N18)))])), 
always(or([not NVV96(constant(N16)), sometime(NVV97(constant(N16)))])), 
always(or([not NVV96(constant(N14)), sometime(NVV97(constant(N14)))])), 
always(or([not NVV96(constant(N19)), sometime(NVV97(constant(N19)))])), 
always(or([not NVV96(constant(N37)), sometime(NVV97(constant(N37)))])), 
always(or([not NVV96(constant(N36)), sometime(NVV97(constant(N36)))])), 
always(or([not NVV96(constant(N11)), sometime(NVV97(constant(N11)))])), 
always(or([not NVV96(constant(N27)), sometime(NVV97(constant(N27)))])), 
always(or([not NVV96(constant(N13)), sometime(NVV97(constant(N13)))])), 
always(or([not NVV96(constant(N24)), sometime(NVV97(constant(N24)))])), 
always(or([not NVV96(constant(N8)), sometime(NVV97(constant(N8)))])), 
always(or([not NVV96(constant(N1)), sometime(NVV97(constant(N1)))])), 
always(or([not NVV96(constant(N30)), sometime(NVV97(constant(N30)))])), 
always(or([not NVV96(constant(N33)), sometime(NVV97(constant(N33)))])), 
always(or([not NVV96(constant(N15)), sometime(NVV97(constant(N15)))])), 
always(or([not NVV96(constant(N32)), sometime(NVV97(constant(N32)))])), 
always(or([not NVV96(constant(N23)), sometime(NVV97(constant(N23)))])), 
always(or([not NVV96(constant(N38)), sometime(NVV97(constant(N38)))])), 
always(or([not NVV96(constant(N26)), sometime(NVV97(constant(N26)))])), 
always(or([not NVV96(constant(N31)), sometime(NVV97(constant(N31)))])), 
always(or([not NVV96(constant(N6)), sometime(NVV97(constant(N6)))])), 
always(or([not NVV96(constant(N20)), sometime(NVV97(constant(N20)))])), 
always(or([not NVV96(constant(N7)), sometime(NVV97(constant(N7)))])), 
always(or([not NVV96(constant(N9)), sometime(NVV97(constant(N9)))])), 
always(or([not NVV96(constant(N17)), sometime(NVV97(constant(N17)))])), 
always(or([not NVV96(constant(N28)), sometime(NVV97(constant(N28)))])), 
always(or([not NVV96(constant(N35)), sometime(NVV97(constant(N35)))])), 
always(or([not NVV96(constant(John)), sometime(NVV97(constant(John)))]))]).

