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

