and([
or([not PinvNameF, E1NameF(constant(dName))]), 
or([not PNameF, E1NameInvF(constant(dNameInv))]), 
or([BOX2F(X)]), 
or([BOX0F(X)]), 
or([BOX1F(X)]), 
or([NVV1(X)]), 
or([not BOX20F(X), BOX9P(X)]), 
or([not BOX9P(X), BOX20F(X)]), 
or([not E1NameF(constant(dName)), E1NameP(constant(dName))]), 
or([not E1NameP(constant(dName)), E1NameF(constant(dName))]), 
or([not BOX22F(X), BOX11P(X)]), 
or([not BOX11P(X), BOX22F(X)]), 
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 PNameF, PNameF]), 
or([not E1NameInvF(X), E1NameInvP(X)]), 
or([not E1NameInvP(X), E1NameInvF(X)]), 
or([not E1NameInvF(constant(dNameInv)), E1NameInvP(constant(dNameInv))]), 
or([not E1NameInvP(constant(dNameInv)), E1NameInvF(constant(dNameInv))]), 
or([not BOX16F(X), BOX5P(X)]), 
or([not BOX5P(X), BOX16F(X)]), 
or([not PNameF, PNameP]), 
or([not PNameP, PNameF]), 
or([not BOX0F(X), BOX25P(X)]), 
or([not BOX25P(X), BOX0F(X)]), 
or([not PinvNameF, PinvNameP]), 
or([not PinvNameP, PinvNameF]), 
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 E1NameF(X), E1NameP(X)]), 
or([not E1NameP(X), E1NameF(X)]), 
or([not PinvNameF, PinvNameF]), 
or([not BOX14F(X), BOX3P(X)]), 
or([not BOX3P(X), BOX14F(X)]), 
or([not BOX24F(X), BOX13P(X)]), 
or([not BOX13P(X), BOX24F(X)]), 
or([not PersonF(X), PersonP(X)]), 
or([not PersonP(X), PersonF(X)]), 
or([not BOX23F(X), BOX12P(X)]), 
or([not BOX12P(X), BOX23F(X)]), 
or([not BOX2F(X), BOX27P(X)]), 
or([not BOX27P(X), BOX2F(X)]), 
or([not BOX1F(X), BOX26P(X)]), 
or([not BOX26P(X), BOX1F(X)]), 
or([not BOX18F(X), BOX7P(X)]), 
or([not BOX7P(X), BOX18F(X)]), 
or([not BOX15F(X), BOX4P(X)]), 
or([not BOX4P(X), BOX15F(X)]), 
or([E1NameF(constant(John))]), 
or([E1NameInvF(constant(N0))]), 
or([PersonF(constant(John))]),
always(or([not NVV1(X), not BOX19F(X), NVV2])), 
always(or([not NVV1(X), NVV3, BOX19F(X)])), 
always(or([not NVV1(X), not BOX25P(X), NVV5(X)])), 
always(or([not NVV1(X), NVV6(X), BOX25P(X)])), 
always(or([not NVV1(X), NVV8(X), BOX8P(X)])), 
always(or([not NVV1(X), NVV8(X), NVV9])), 
always(or([not NVV1(X), not BOX8P(X), NVV10, NVV11(X)])), 
always(or([not NVV1(X), NVV12(X), BOX10P(X)])), 
always(or([not NVV1(X), NVV12(X), NVV13(X)])), 
always(or([not NVV1(X), not BOX10P(X), NVV14(X), NVV15(X)])), 
always(or([not NVV1(X), not BOX17F(X), NVV16(X)])), 
always(or([not NVV1(X), NVV17(X), BOX17F(X)])), 
always(or([not NVV1(X), NVV19(X), BOX18F(X)])), 
always(or([not NVV1(X), NVV19(X), NVV20(X)])), 
always(or([not NVV1(X), not BOX18F(X), NVV21(X), NVV22(X)])), 
always(or([not NVV1(X), not BOX26P(X), NVV23(X)])), 
always(or([not NVV1(X), NVV24(X), BOX26P(X)])), 
always(or([not NVV1(X), not BOX27P(X), NVV26(X)])), 
always(or([not NVV1(X), NVV27(X), BOX27P(X)])), 
always(or([not NVV1(X), NVV29(X), BOX5P(X)])), 
always(or([not NVV1(X), NVV29(X), NVV30])), 
always(or([not NVV1(X), not BOX5P(X), NVV31, NVV32(X)])), 
always(or([not NVV1(X), NVV33(X), BOX15F(X)])), 
always(or([not NVV1(X), NVV33(X), NVV34(X)])), 
always(or([not NVV1(X), not BOX15F(X), NVV35(X), NVV36(X)])), 
always(or([not NVV1(X), not BOX12P(X), NVV37(X)])), 
always(or([not NVV1(X), NVV38(X), BOX12P(X)])), 
always(or([not NVV1(X), not BOX7P(X), NVV40(X)])), 
always(or([not NVV1(X), NVV41(X), BOX7P(X)])), 
always(or([not NVV1(X), not BOX14F(X), NVV43(X)])), 
always(or([not NVV1(X), NVV44(X), BOX14F(X)])), 
always(or([not NVV1(X), NVV46(X), BOX2F(X)])), 
always(or([not NVV1(X), NVV46(X), NVV47(X)])), 
always(or([not NVV1(X), not BOX2F(X), NVV48(X), NVV49(X)])), 
always(or([not NVV1(X), NVV50(X), BOX23F(X)])), 
always(or([not NVV1(X), NVV50(X), NVV51(X)])), 
always(or([not NVV1(X), not BOX23F(X), NVV52(X), NVV53(X)])), 
always(or([not NVV1(X), NVV54(X), BOX11P(X)])), 
always(or([not NVV1(X), NVV54(X), NVV55(X)])), 
always(or([not NVV1(X), not BOX11P(X), NVV56(X), NVV57(X)])), 
always(or([not NVV1(X), NVV58(X), BOX3P(X)])), 
always(or([not NVV1(X), NVV58(X), NVV59(X)])), 
always(or([not NVV1(X), not BOX3P(X), NVV61(X), NVV63(X)])), 
always(or([not NVV1(X), not BOX16F(X), NVV64])), 
always(or([not NVV1(X), NVV65, BOX16F(X)])), 
always(or([not NVV1(X), not BOX4P(X), NVV67(X)])), 
always(or([not NVV1(X), NVV68(X), BOX4P(X)])), 
always(or([not NVV1(X), NVV70(X), BOX9P(X)])), 
always(or([not NVV1(X), NVV70(X), NVV71(X)])), 
always(or([not NVV1(X), not BOX9P(X), NVV73(X), NVV75(X)])), 
always(or([not NVV1(X), not BOX21F(X), NVV76(X)])), 
always(or([not NVV1(X), NVV77(X), BOX21F(X)])), 
always(or([not NVV1(X), NVV79(X), BOX1F(X)])), 
always(or([not NVV1(X), NVV79(X), NVV80(X)])), 
always(or([not NVV1(X), not BOX1F(X), NVV81(X), NVV82(X)])), 
always(or([not NVV1(X), not BOX22F(X), NVV83(X)])), 
always(or([not NVV1(X), NVV84(X), BOX22F(X)])), 
always(or([not NVV1(X), NVV86(X), BOX6P(X)])), 
always(or([not NVV1(X), NVV86(X), NVV87(X)])), 
always(or([not NVV1(X), not BOX6P(X), NVV89(X), NVV91(X)])), 
always(or([not NVV1(X), NVV92(X), BOX24F(X)])), 
always(or([not NVV1(X), NVV92(X), NVV93(X)])), 
always(or([not NVV1(X), not BOX24F(X), NVV94(X), NVV95(X)])), 
always(or([not NVV1(X), not BOX13P(X), NVV96(X)])), 
always(or([not NVV1(X), NVV97(X), BOX13P(X)])), 
always(or([not NVV1(X), NVV99(X), BOX0F(X)])), 
always(or([not NVV1(X), NVV99(X), NVV100(X)])), 
always(or([not NVV1(X), not BOX0F(X), NVV101(X), NVV102(X)])), 
always(or([not NVV1(X), not BOX20F(X), NVV103(X)])), 
always(or([not NVV1(X), NVV104(X), BOX20F(X)])), 
always(or([not NVV2, PinvNameF])), 
always(or([not NVV4, not PinvNameF])), 
always(or([not NVV5(X), BOX3P(X)])), 
always(or([not NVV7(X), not BOX3P(X)])), 
always(or([not NVV16(X), not E1NameInvF(X), BOX18F(X)])), 
always(or([not NVV18(X), E1NameInvF(X)])), 
always(or([not NVV18(X), not BOX18F(X)])), 
always(or([not NVV23(X), BOX6P(X)])), 
always(or([not NVV25(X), not BOX6P(X)])), 
always(or([not NVV26(X), BOX9P(X)])), 
always(or([not NVV28(X), not BOX9P(X)])), 
always(or([not NVV37(X), E1NameP(X)])), 
always(or([not NVV39(X), not E1NameP(X)])), 
always(or([not NVV40(X), BOX8P(X)])), 
always(or([not NVV42(X), not BOX8P(X)])), 
always(or([not NVV43(X), not E1NameF(X), BOX15F(X)])), 
always(or([not NVV45(X), E1NameF(X)])), 
always(or([not NVV45(X), not BOX15F(X)])), 
always(or([not NVV60(X), not E1NameP(X), BOX4P(X)])), 
always(or([not NVV62(X), E1NameP(X)])), 
always(or([not NVV62(X), not BOX4P(X)])), 
always(or([not NVV64, PNameF])), 
always(or([not NVV66, not PNameF])), 
always(or([not NVV67(X), BOX5P(X)])), 
always(or([not NVV69(X), not BOX5P(X)])), 
always(or([not NVV72(X), not PersonP(X), E1NameP(X)])), 
always(or([not NVV72(X), not PersonP(X), not E2NameP(X)])), 
always(or([not NVV72(X), not E2NameP(X), E1NameP(X)])), 
always(or([not NVV72(X), not E1NameP(X), BOX10P(X)])), 
always(or([not NVV72(X), not E2NameP(X), BOX11P(X)])), 
always(or([not NVV74(X), not E1NameP(X), PersonP(X), E1NameP(X), E2NameP(X)])), 
always(or([not NVV74(X), PersonP(X), E1NameP(X), E2NameP(X)])), 
always(or([not NVV74(X), PersonP(X), not E1NameP(X), E1NameP(X), E2NameP(X)])), 
always(or([not NVV74(X), not E1NameP(X), E1NameP(X), E2NameP(X)])), 
always(or([not NVV74(X), not E1NameP(X), PersonP(X), not BOX10P(X), E2NameP(X)])), 
always(or([not NVV74(X), PersonP(X), not BOX10P(X), E2NameP(X)])), 
always(or([not NVV74(X), PersonP(X), not E1NameP(X), not BOX10P(X), E2NameP(X)])), 
always(or([not NVV74(X), not E1NameP(X), not BOX10P(X), E2NameP(X)])), 
always(or([not NVV74(X), not E1NameP(X), PersonP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV74(X), PersonP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV74(X), not E1NameP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV74(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV74(X), PersonP(X), E2NameP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV74(X), E2NameP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV74(X), not E1NameP(X), PersonP(X), E2NameP(X), not BOX10P(X), not BOX11P(X)])), 
always(or([not NVV74(X), PersonP(X), E2NameP(X), not BOX10P(X), not BOX11P(X)])), 
always(or([not NVV74(X), not E1NameP(X), E2NameP(X), not BOX10P(X), not BOX11P(X)])), 
always(or([not NVV74(X), PersonP(X), not E1NameP(X), not BOX10P(X), not BOX11P(X)])), 
always(or([not NVV74(X), PersonP(X), E2NameP(X), not E1NameP(X), not BOX10P(X), not BOX11P(X)])), 
always(or([not NVV74(X), E2NameP(X), not E1NameP(X), not BOX10P(X), not BOX11P(X)])), 
always(or([not NVV76(X), BOX23F(X)])), 
always(or([not NVV78(X), not BOX23F(X)])), 
always(or([not NVV83(X), BOX24F(X)])), 
always(or([not NVV85(X), not BOX24F(X)])), 
always(or([not NVV88(X), not E1NameInvP(X), BOX7P(X)])), 
always(or([not NVV90(X), E1NameInvP(X)])), 
always(or([not NVV90(X), not BOX7P(X)])), 
always(or([not NVV96(X), E2NameP(X)])), 
always(or([not NVV98(X), not E2NameP(X)])), 
always(or([not NVV103(X), not PersonF(X), E1NameF(X)])), 
always(or([not NVV103(X), not PersonF(X), not E2NameF(X)])), 
always(or([not NVV103(X), not E2NameF(X), E1NameF(X)])), 
always(or([not NVV103(X), not E1NameF(X), BOX21F(X)])), 
always(or([not NVV103(X), not E2NameF(X), BOX22F(X)])), 
always(or([not NVV105(X), not E1NameF(X), PersonF(X), E1NameF(X), E2NameF(X)])), 
always(or([not NVV105(X), PersonF(X), E1NameF(X), E2NameF(X)])), 
always(or([not NVV105(X), PersonF(X), not E1NameF(X), E1NameF(X), E2NameF(X)])), 
always(or([not NVV105(X), not E1NameF(X), E1NameF(X), E2NameF(X)])), 
always(or([not NVV105(X), not E1NameF(X), PersonF(X), not BOX21F(X), E2NameF(X)])), 
always(or([not NVV105(X), PersonF(X), not BOX21F(X), E2NameF(X)])), 
always(or([not NVV105(X), PersonF(X), not E1NameF(X), not BOX21F(X), E2NameF(X)])), 
always(or([not NVV105(X), not E1NameF(X), not BOX21F(X), E2NameF(X)])), 
always(or([not NVV105(X), not E1NameF(X), PersonF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV105(X), PersonF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV105(X), not E1NameF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV105(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV105(X), PersonF(X), E2NameF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV105(X), E2NameF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV105(X), not E1NameF(X), PersonF(X), E2NameF(X), not BOX21F(X), not BOX22F(X)])), 
always(or([not NVV105(X), PersonF(X), E2NameF(X), not BOX21F(X), not BOX22F(X)])), 
always(or([not NVV105(X), not E1NameF(X), E2NameF(X), not BOX21F(X), not BOX22F(X)])), 
always(or([not NVV105(X), PersonF(X), not E1NameF(X), not BOX21F(X), not BOX22F(X)])), 
always(or([not NVV105(X), PersonF(X), E2NameF(X), not E1NameF(X), not BOX21F(X), not BOX22F(X)])), 
always(or([not NVV105(X), E2NameF(X), not E1NameF(X), not BOX21F(X), not BOX22F(X)])),
always(or([not NVV1(X), next(NVV1(hidden(X)))])), 
always(or([not NVV1(constant(X)), next(NVV1(constant(X)))])), 
always(or([not NVV2, next(NVV2)])), 
always(or([not NVV5(X), next(NVV5(hidden(X)))])), 
always(or([not NVV5(constant(X)), next(NVV5(constant(X)))])), 
always(or([not NVV8(X), next(not BOX8P(hidden(X)))])), 
always(or([not NVV8(constant(X)), next(not BOX8P(constant(X)))])), 
always(or([not NVV9, next(PinvNameF)])), 
always(or([not NVV10, next(not PinvNameF)])), 
always(or([not NVV11(X), next(BOX8P(hidden(X)))])), 
always(or([not NVV11(constant(X)), next(BOX8P(constant(X)))])), 
always(or([not NVV12(X), next(not BOX10P(hidden(X)))])), 
always(or([not NVV12(constant(X)), next(not BOX10P(constant(X)))])), 
always(or([not NVV13(X), next(BOX12P(hidden(X)))])), 
always(or([not NVV13(constant(X)), next(BOX12P(constant(X)))])), 
always(or([not NVV14(X), next(not BOX12P(hidden(X)))])), 
always(or([not NVV14(constant(X)), next(not BOX12P(constant(X)))])), 
always(or([not NVV15(X), next(BOX10P(hidden(X)))])), 
always(or([not NVV15(constant(X)), next(BOX10P(constant(X)))])), 
always(or([not NVV16(X), next(NVV16(hidden(X)))])), 
always(or([not NVV16(constant(X)), next(NVV16(constant(X)))])), 
always(or([not NVV19(X), next(not BOX18F(hidden(X)))])), 
always(or([not NVV19(constant(X)), next(not BOX18F(constant(X)))])), 
always(or([not NVV20(X), next(BOX19F(hidden(X)))])), 
always(or([not NVV20(constant(X)), next(BOX19F(constant(X)))])), 
always(or([not NVV21(X), next(not BOX19F(hidden(X)))])), 
always(or([not NVV21(constant(X)), next(not BOX19F(constant(X)))])), 
always(or([not NVV22(X), next(BOX18F(hidden(X)))])), 
always(or([not NVV22(constant(X)), next(BOX18F(constant(X)))])), 
always(or([not NVV23(X), next(NVV23(hidden(X)))])), 
always(or([not NVV23(constant(X)), next(NVV23(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 BOX5P(hidden(X)))])), 
always(or([not NVV29(constant(X)), next(not BOX5P(constant(X)))])), 
always(or([not NVV30, next(PNameF)])), 
always(or([not NVV31, next(not PNameF)])), 
always(or([not NVV32(X), next(BOX5P(hidden(X)))])), 
always(or([not NVV32(constant(X)), next(BOX5P(constant(X)))])), 
always(or([not NVV33(X), next(not BOX15F(hidden(X)))])), 
always(or([not NVV33(constant(X)), next(not BOX15F(constant(X)))])), 
always(or([not NVV34(X), next(BOX16F(hidden(X)))])), 
always(or([not NVV34(constant(X)), next(BOX16F(constant(X)))])), 
always(or([not NVV35(X), next(not BOX16F(hidden(X)))])), 
always(or([not NVV35(constant(X)), next(not BOX16F(constant(X)))])), 
always(or([not NVV36(X), next(BOX15F(hidden(X)))])), 
always(or([not NVV36(constant(X)), next(BOX15F(constant(X)))])), 
always(or([not NVV37(X), next(NVV37(hidden(X)))])), 
always(or([not NVV37(constant(X)), next(NVV37(constant(X)))])), 
always(or([not NVV40(X), next(NVV40(hidden(X)))])), 
always(or([not NVV40(constant(X)), next(NVV40(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 BOX2F(hidden(X)))])), 
always(or([not NVV46(constant(X)), next(not BOX2F(constant(X)))])), 
always(or([not NVV47(X), next(BOX20F(hidden(X)))])), 
always(or([not NVV47(constant(X)), next(BOX20F(constant(X)))])), 
always(or([not NVV48(X), next(not BOX20F(hidden(X)))])), 
always(or([not NVV48(constant(X)), next(not BOX20F(constant(X)))])), 
always(or([not NVV49(X), next(BOX2F(hidden(X)))])), 
always(or([not NVV49(constant(X)), next(BOX2F(constant(X)))])), 
always(or([not NVV50(X), next(not BOX23F(hidden(X)))])), 
always(or([not NVV50(constant(X)), next(not BOX23F(constant(X)))])), 
always(or([not NVV51(X), next(E1NameF(hidden(X)))])), 
always(or([not NVV51(constant(X)), next(E1NameF(constant(X)))])), 
always(or([not NVV52(X), next(not E1NameF(hidden(X)))])), 
always(or([not NVV52(constant(X)), next(not E1NameF(constant(X)))])), 
always(or([not NVV53(X), next(BOX23F(hidden(X)))])), 
always(or([not NVV53(constant(X)), next(BOX23F(constant(X)))])), 
always(or([not NVV54(X), next(not BOX11P(hidden(X)))])), 
always(or([not NVV54(constant(X)), next(not BOX11P(constant(X)))])), 
always(or([not NVV55(X), next(BOX13P(hidden(X)))])), 
always(or([not NVV55(constant(X)), next(BOX13P(constant(X)))])), 
always(or([not NVV56(X), next(not BOX13P(hidden(X)))])), 
always(or([not NVV56(constant(X)), next(not BOX13P(constant(X)))])), 
always(or([not NVV57(X), next(BOX11P(hidden(X)))])), 
always(or([not NVV57(constant(X)), next(BOX11P(constant(X)))])), 
always(or([not NVV58(X), next(not BOX3P(hidden(X)))])), 
always(or([not NVV58(constant(X)), next(not BOX3P(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(NVV62(hidden(X)))])), 
always(or([not NVV61(constant(X)), next(NVV62(constant(X)))])), 
always(or([not NVV63(X), next(BOX3P(hidden(X)))])), 
always(or([not NVV63(constant(X)), next(BOX3P(constant(X)))])), 
always(or([not NVV64, next(NVV64)])), 
always(or([not NVV67(X), next(NVV67(hidden(X)))])), 
always(or([not NVV67(constant(X)), next(NVV67(constant(X)))])), 
always(or([not NVV70(X), next(not BOX9P(hidden(X)))])), 
always(or([not NVV70(constant(X)), next(not BOX9P(constant(X)))])), 
always(or([not NVV71(X), next(NVV72(hidden(X)))])), 
always(or([not NVV71(constant(X)), next(NVV72(constant(X)))])), 
always(or([not NVV73(X), next(NVV74(hidden(X)))])), 
always(or([not NVV73(constant(X)), next(NVV74(constant(X)))])), 
always(or([not NVV75(X), next(BOX9P(hidden(X)))])), 
always(or([not NVV75(constant(X)), next(BOX9P(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(not BOX1F(hidden(X)))])), 
always(or([not NVV79(constant(X)), next(not BOX1F(constant(X)))])), 
always(or([not NVV80(X), next(BOX17F(hidden(X)))])), 
always(or([not NVV80(constant(X)), next(BOX17F(constant(X)))])), 
always(or([not NVV81(X), next(not BOX17F(hidden(X)))])), 
always(or([not NVV81(constant(X)), next(not BOX17F(constant(X)))])), 
always(or([not NVV82(X), next(BOX1F(hidden(X)))])), 
always(or([not NVV82(constant(X)), next(BOX1F(constant(X)))])), 
always(or([not NVV83(X), next(NVV83(hidden(X)))])), 
always(or([not NVV83(constant(X)), next(NVV83(constant(X)))])), 
always(or([not NVV86(X), next(not BOX6P(hidden(X)))])), 
always(or([not NVV86(constant(X)), next(not BOX6P(constant(X)))])), 
always(or([not NVV87(X), next(NVV88(hidden(X)))])), 
always(or([not NVV87(constant(X)), next(NVV88(constant(X)))])), 
always(or([not NVV89(X), next(NVV90(hidden(X)))])), 
always(or([not NVV89(constant(X)), next(NVV90(constant(X)))])), 
always(or([not NVV91(X), next(BOX6P(hidden(X)))])), 
always(or([not NVV91(constant(X)), next(BOX6P(constant(X)))])), 
always(or([not NVV92(X), next(not BOX24F(hidden(X)))])), 
always(or([not NVV92(constant(X)), next(not BOX24F(constant(X)))])), 
always(or([not NVV93(X), next(E2NameF(hidden(X)))])), 
always(or([not NVV93(constant(X)), next(E2NameF(constant(X)))])), 
always(or([not NVV94(X), next(not E2NameF(hidden(X)))])), 
always(or([not NVV94(constant(X)), next(not E2NameF(constant(X)))])), 
always(or([not NVV95(X), next(BOX24F(hidden(X)))])), 
always(or([not NVV95(constant(X)), next(BOX24F(constant(X)))])), 
always(or([not NVV96(X), next(NVV96(hidden(X)))])), 
always(or([not NVV96(constant(X)), next(NVV96(constant(X)))])), 
always(or([not NVV99(X), next(not BOX0F(hidden(X)))])), 
always(or([not NVV99(constant(X)), next(not BOX0F(constant(X)))])), 
always(or([not NVV100(X), next(BOX14F(hidden(X)))])), 
always(or([not NVV100(constant(X)), next(BOX14F(constant(X)))])), 
always(or([not NVV101(X), next(not BOX14F(hidden(X)))])), 
always(or([not NVV101(constant(X)), next(not BOX14F(constant(X)))])), 
always(or([not NVV102(X), next(BOX0F(hidden(X)))])), 
always(or([not NVV102(constant(X)), next(BOX0F(constant(X)))])), 
always(or([not NVV103(X), next(NVV103(hidden(X)))])), 
always(or([not NVV103(constant(X)), next(NVV103(constant(X)))])),
always(or([not NVV3, sometime(NVV4)])), 
always(or([not NVV6(X), sometime(NVV7(X))])), 
always(or([not NVV6(constant(dName)), sometime(NVV7(constant(dName)))])), 
always(or([not NVV6(constant(dNameInv)), sometime(NVV7(constant(dNameInv)))])), 
always(or([not NVV6(constant(N0)), sometime(NVV7(constant(N0)))])), 
always(or([not NVV6(constant(John)), sometime(NVV7(constant(John)))])), 
always(or([not NVV17(X), sometime(NVV18(X))])), 
always(or([not NVV17(constant(dName)), sometime(NVV18(constant(dName)))])), 
always(or([not NVV17(constant(dNameInv)), sometime(NVV18(constant(dNameInv)))])), 
always(or([not NVV17(constant(N0)), sometime(NVV18(constant(N0)))])), 
always(or([not NVV17(constant(John)), sometime(NVV18(constant(John)))])), 
always(or([not NVV24(X), sometime(NVV25(X))])), 
always(or([not NVV24(constant(dName)), sometime(NVV25(constant(dName)))])), 
always(or([not NVV24(constant(dNameInv)), sometime(NVV25(constant(dNameInv)))])), 
always(or([not NVV24(constant(N0)), sometime(NVV25(constant(N0)))])), 
always(or([not NVV24(constant(John)), sometime(NVV25(constant(John)))])), 
always(or([not NVV27(X), sometime(NVV28(X))])), 
always(or([not NVV27(constant(dName)), sometime(NVV28(constant(dName)))])), 
always(or([not NVV27(constant(dNameInv)), sometime(NVV28(constant(dNameInv)))])), 
always(or([not NVV27(constant(N0)), sometime(NVV28(constant(N0)))])), 
always(or([not NVV27(constant(John)), sometime(NVV28(constant(John)))])), 
always(or([not NVV38(X), sometime(NVV39(X))])), 
always(or([not NVV38(constant(dName)), sometime(NVV39(constant(dName)))])), 
always(or([not NVV38(constant(dNameInv)), sometime(NVV39(constant(dNameInv)))])), 
always(or([not NVV38(constant(N0)), sometime(NVV39(constant(N0)))])), 
always(or([not NVV38(constant(John)), sometime(NVV39(constant(John)))])), 
always(or([not NVV41(X), sometime(NVV42(X))])), 
always(or([not NVV41(constant(dName)), sometime(NVV42(constant(dName)))])), 
always(or([not NVV41(constant(dNameInv)), sometime(NVV42(constant(dNameInv)))])), 
always(or([not NVV41(constant(N0)), sometime(NVV42(constant(N0)))])), 
always(or([not NVV41(constant(John)), sometime(NVV42(constant(John)))])), 
always(or([not NVV44(X), sometime(NVV45(X))])), 
always(or([not NVV44(constant(dName)), sometime(NVV45(constant(dName)))])), 
always(or([not NVV44(constant(dNameInv)), sometime(NVV45(constant(dNameInv)))])), 
always(or([not NVV44(constant(N0)), sometime(NVV45(constant(N0)))])), 
always(or([not NVV44(constant(John)), sometime(NVV45(constant(John)))])), 
always(or([not NVV65, sometime(NVV66)])), 
always(or([not NVV68(X), sometime(NVV69(X))])), 
always(or([not NVV68(constant(dName)), sometime(NVV69(constant(dName)))])), 
always(or([not NVV68(constant(dNameInv)), sometime(NVV69(constant(dNameInv)))])), 
always(or([not NVV68(constant(N0)), sometime(NVV69(constant(N0)))])), 
always(or([not NVV68(constant(John)), sometime(NVV69(constant(John)))])), 
always(or([not NVV77(X), sometime(NVV78(X))])), 
always(or([not NVV77(constant(dName)), sometime(NVV78(constant(dName)))])), 
always(or([not NVV77(constant(dNameInv)), sometime(NVV78(constant(dNameInv)))])), 
always(or([not NVV77(constant(N0)), sometime(NVV78(constant(N0)))])), 
always(or([not NVV77(constant(John)), sometime(NVV78(constant(John)))])), 
always(or([not NVV84(X), sometime(NVV85(X))])), 
always(or([not NVV84(constant(dName)), sometime(NVV85(constant(dName)))])), 
always(or([not NVV84(constant(dNameInv)), sometime(NVV85(constant(dNameInv)))])), 
always(or([not NVV84(constant(N0)), sometime(NVV85(constant(N0)))])), 
always(or([not NVV84(constant(John)), sometime(NVV85(constant(John)))])), 
always(or([not NVV97(X), sometime(NVV98(X))])), 
always(or([not NVV97(constant(dName)), sometime(NVV98(constant(dName)))])), 
always(or([not NVV97(constant(dNameInv)), sometime(NVV98(constant(dNameInv)))])), 
always(or([not NVV97(constant(N0)), sometime(NVV98(constant(N0)))])), 
always(or([not NVV97(constant(John)), sometime(NVV98(constant(John)))])), 
always(or([not NVV104(X), sometime(NVV105(X))])), 
always(or([not NVV104(constant(dName)), sometime(NVV105(constant(dName)))])), 
always(or([not NVV104(constant(dNameInv)), sometime(NVV105(constant(dNameInv)))])), 
always(or([not NVV104(constant(N0)), sometime(NVV105(constant(N0)))])), 
always(or([not NVV104(constant(John)), sometime(NVV105(constant(John)))]))]).

