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

