and([
or([not PinvNameF, E1NameF(constant(dName))]), 
or([not PNameF, E1NameInvF(constant(dNameInv))]), 
or([BOX0F(X)]), 
or([NVV1(X)]), 
or([not E1NameF(X), E1NameP(X)]), 
or([not E1NameP(X), E1NameF(X)]), 
or([not BOX21F(X), BOX10P(X)]), 
or([not BOX10P(X), BOX21F(X)]), 
or([not BOX22F(X), BOX11P(X)]), 
or([not BOX11P(X), BOX22F(X)]), 
or([not BOX20F(X), BOX9P(X)]), 
or([not BOX9P(X), BOX20F(X)]), 
or([not BOX17F(X), BOX6P(X)]), 
or([not BOX6P(X), BOX17F(X)]), 
or([not PinvNameF, PinvNameP]), 
or([not PinvNameP, PinvNameF]), 
or([not BOX14F(X), BOX3P(X)]), 
or([not BOX3P(X), BOX14F(X)]), 
or([not BOX16F(X), BOX5P(X)]), 
or([not BOX5P(X), BOX16F(X)]), 
or([not BOX19F(X), BOX8P(X)]), 
or([not BOX8P(X), BOX19F(X)]), 
or([not PersonF(X), PersonP(X)]), 
or([not PersonP(X), PersonF(X)]), 
or([not E1NameInvF(X), E1NameInvP(X)]), 
or([not E1NameInvP(X), E1NameInvF(X)]), 
or([not BOX13F(X), BOX2P(X)]), 
or([not BOX2P(X), BOX13F(X)]), 
or([not BOX18F(X), BOX7P(X)]), 
or([not BOX7P(X), BOX18F(X)]), 
or([not PNameF, PNameP]), 
or([not PNameP, PNameF]), 
or([not BOX15F(X), BOX4P(X)]), 
or([not BOX4P(X), BOX15F(X)]), 
or([not BOX0F(X), BOX1P(X)]), 
or([not BOX1P(X), BOX0F(X)]), 
or([not E2NameF(X), E2NameP(X)]), 
or([not E2NameP(X), E2NameF(X)]), 
or([not BOX23F(X), BOX12P(X)]), 
or([not BOX12P(X), BOX23F(X)]), 
or([NVV88]), 
or([NVV91]), 
or([NVV98]), 
or([NVV108]), 
or([NVV122]), 
or([NVV116]), 
or([NVV124]), 
or([NVV126]), 
or([NVV104]), 
or([NVV95]), 
or([NVV132]), 
or([NVV144]), 
or([NVV152]), 
or([NVV142]), 
or([NVV128]), 
or([NVV110]), 
or([NVV120]), 
or([NVV156]), 
or([NVV134]), 
or([NVV102]), 
or([PersonF(constant(John))]), 
or([NVV130]), 
or([NVV148]), 
or([NVV150]), 
or([NVV112]), 
or([NVV106]), 
or([NVV100]), 
or([NVV114]), 
or([NVV140]), 
or([NVV136]), 
or([E1NameInvF(constant(N0))]), 
or([NVV93]), 
or([NVV97]), 
or([NVV158]), 
or([NVV118]), 
or([NVV146]), 
or([NVV154]), 
or([E1NameF(constant(John))]), 
or([NVV160]), 
or([NVV138]), 
or([NVV90]),
always(or([not NVV1(X), NVV2(X), BOX7P(X)])), 
always(or([not NVV1(X), NVV2(X), NVV3(X)])), 
always(or([not NVV1(X), not BOX7P(X), NVV4(X), NVV5(X)])), 
always(or([not NVV1(X), not BOX18F(X), NVV6(X)])), 
always(or([not NVV1(X), NVV7(X), BOX18F(X)])), 
always(or([not NVV1(X), not BOX12P(X), NVV9])), 
always(or([not NVV1(X), NVV10, BOX12P(X)])), 
always(or([not NVV1(X), not BOX8P(X), NVV12(X)])), 
always(or([not NVV1(X), NVV13(X), BOX8P(X)])), 
always(or([not NVV1(X), NVV15(X), BOX23F(X)])), 
always(or([not NVV1(X), NVV15(X), NVV16])), 
always(or([not NVV1(X), not BOX23F(X), NVV17, NVV18(X)])), 
always(or([not NVV1(X), NVV19(X), BOX17F(X)])), 
always(or([not NVV1(X), NVV19(X), NVV20])), 
always(or([not NVV1(X), not BOX17F(X), NVV21, NVV22(X)])), 
always(or([not NVV1(X), NVV23(X), BOX1P(X)])), 
always(or([not NVV1(X), NVV23(X), NVV24(X)])), 
always(or([not NVV1(X), not BOX1P(X), NVV25(X), NVV26(X)])), 
always(or([not NVV1(X), NVV27(X), BOX3P(X)])), 
always(or([not NVV1(X), NVV27(X), NVV28(X)])), 
always(or([not NVV1(X), not BOX3P(X), NVV29(X), NVV30(X)])), 
always(or([not NVV1(X), NVV31(X), BOX11P(X)])), 
always(or([not NVV1(X), NVV31(X), NVV32(X)])), 
always(or([not NVV1(X), not BOX11P(X), NVV33(X), NVV34(X)])), 
always(or([not NVV1(X), NVV35(X), BOX5P(X)])), 
always(or([not NVV1(X), NVV35(X), NVV36(X)])), 
always(or([not NVV1(X), not BOX5P(X), NVV37(X), NVV38(X)])), 
always(or([not NVV1(X), not BOX22F(X), NVV39(X)])), 
always(or([not NVV1(X), NVV40(X), BOX22F(X)])), 
always(or([not NVV1(X), not BOX2P(X), NVV42(X)])), 
always(or([not NVV1(X), NVV43(X), BOX2P(X)])), 
always(or([not NVV1(X), not BOX10P(X), NVV45(X)])), 
always(or([not NVV1(X), NVV46(X), BOX10P(X)])), 
always(or([not NVV1(X), not BOX4P(X), NVV48(X)])), 
always(or([not NVV1(X), NVV49(X), BOX4P(X)])), 
always(or([not NVV1(X), NVV51(X), BOX21F(X)])), 
always(or([not NVV1(X), NVV51(X), NVV52(X)])), 
always(or([not NVV1(X), not BOX21F(X), NVV53(X), NVV54(X)])), 
always(or([not NVV1(X), not BOX0F(X), NVV55(X)])), 
always(or([not NVV1(X), NVV56(X), BOX0F(X)])), 
always(or([not NVV1(X), NVV58(X), BOX19F(X)])), 
always(or([not NVV1(X), NVV58(X), NVV59(X)])), 
always(or([not NVV1(X), not BOX19F(X), NVV60(X), NVV61(X)])), 
always(or([not NVV1(X), NVV62(X), BOX9P(X)])), 
always(or([not NVV1(X), NVV62(X), NVV63(X)])), 
always(or([not NVV1(X), not BOX9P(X), NVV64(X), NVV65(X)])), 
always(or([not NVV1(X), not BOX6P(X), NVV66])), 
always(or([not NVV1(X), NVV67, BOX6P(X)])), 
always(or([not NVV1(X), NVV69(X), BOX15F(X)])), 
always(or([not NVV1(X), NVV69(X), NVV70(X)])), 
always(or([not NVV1(X), not BOX15F(X), NVV71(X), NVV72(X)])), 
always(or([not NVV1(X), not BOX14F(X), NVV73(X)])), 
always(or([not NVV1(X), NVV74(X), BOX14F(X)])), 
always(or([not NVV1(X), not BOX16F(X), NVV76(X)])), 
always(or([not NVV1(X), NVV77(X), BOX16F(X)])), 
always(or([not NVV1(X), NVV79(X), BOX13F(X)])), 
always(or([not NVV1(X), NVV79(X), NVV80(X)])), 
always(or([not NVV1(X), not BOX13F(X), NVV82(X), NVV84(X)])), 
always(or([not NVV1(X), not BOX20F(X), NVV85(X)])), 
always(or([not NVV1(X), NVV86(X), BOX20F(X)])), 
always(or([not NVV6(X), BOX19F(X)])), 
always(or([not NVV8(X), not BOX19F(X)])), 
always(or([not NVV9, PinvNameP])), 
always(or([not NVV11, not PinvNameP])), 
always(or([not NVV12(X), E2NameP(X)])), 
always(or([not NVV14(X), not E2NameP(X)])), 
always(or([not NVV39(X), BOX23F(X)])), 
always(or([not NVV41(X), not BOX23F(X)])), 
always(or([not NVV42(X), not PersonP(X), E1NameP(X)])), 
always(or([not NVV42(X), not PersonP(X), not E2NameP(X)])), 
always(or([not NVV42(X), not E1NameP(X), BOX3P(X)])), 
always(or([not NVV42(X), not E1NameP(X), BOX5P(X)])), 
always(or([not NVV42(X), not E2NameP(X), BOX7P(X)])), 
always(or([not NVV42(X), not E1NameInvP(X), BOX9P(X)])), 
always(or([not NVV42(X), not E1NameInvP(X), BOX11P(X)])), 
always(or([not NVV42(X), not E2NameP(X), E1NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), E2NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), E2NameP(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), E1NameP(X), E2NameP(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), E2NameP(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), not BOX3P(X), E1NameP(X), E2NameP(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), E2NameP(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), E1NameP(X), not BOX5P(X), E2NameP(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), E2NameP(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), not BOX3P(X), not BOX5P(X), E2NameP(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), E2NameP(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), E1NameP(X), E2NameP(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), E2NameP(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), not BOX3P(X), E1NameP(X), E2NameP(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), E2NameP(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), E1NameP(X), not BOX5P(X), E2NameP(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), E2NameP(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), not BOX3P(X), not BOX5P(X), E2NameP(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E1NameInvP(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), E2NameP(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), E1NameP(X), E2NameP(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), E2NameP(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), not BOX3P(X), E1NameP(X), E2NameP(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), E2NameP(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), E1NameP(X), not BOX5P(X), E2NameP(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), E2NameP(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), not BOX3P(X), not BOX5P(X), E2NameP(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E1NameInvP(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), E2NameP(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), E1NameP(X), E2NameP(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), E2NameP(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), not BOX3P(X), E1NameP(X), E2NameP(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), E2NameP(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), E1NameP(X), not BOX5P(X), E2NameP(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), E2NameP(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), not BOX3P(X), not BOX5P(X), E2NameP(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), PersonP(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV44(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not BOX11P(X), not E1NameP(X)])), 
always(or([not NVV45(X), E1NameInvP(X)])), 
always(or([not NVV47(X), not E1NameInvP(X)])), 
always(or([not NVV48(X), E1NameP(X)])), 
always(or([not NVV50(X), not E1NameP(X)])), 
always(or([not NVV55(X), BOX13F(X)])), 
always(or([not NVV57(X), not BOX13F(X)])), 
always(or([not NVV66, PNameP])), 
always(or([not NVV68, not PNameP])), 
always(or([not NVV73(X), BOX15F(X)])), 
always(or([not NVV75(X), not BOX15F(X)])), 
always(or([not NVV76(X), BOX17F(X)])), 
always(or([not NVV78(X), not BOX17F(X)])), 
always(or([not NVV81(X), not PersonF(X), E1NameF(X)])), 
always(or([not NVV81(X), not PersonF(X), not E2NameF(X)])), 
always(or([not NVV81(X), not E1NameF(X), BOX14F(X)])), 
always(or([not NVV81(X), not E1NameF(X), BOX16F(X)])), 
always(or([not NVV81(X), not E2NameF(X), BOX18F(X)])), 
always(or([not NVV81(X), not E1NameInvF(X), BOX20F(X)])), 
always(or([not NVV81(X), not E1NameInvF(X), BOX22F(X)])), 
always(or([not NVV81(X), not E2NameF(X), E1NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), E2NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), E2NameF(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), E1NameF(X), E2NameF(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), E2NameF(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), not BOX14F(X), E1NameF(X), E2NameF(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), E2NameF(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), E1NameF(X), not BOX16F(X), E2NameF(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), E2NameF(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), not BOX14F(X), not BOX16F(X), E2NameF(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), E2NameF(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), E1NameF(X), E2NameF(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), E2NameF(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), not BOX14F(X), E1NameF(X), E2NameF(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), E2NameF(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), E1NameF(X), not BOX16F(X), E2NameF(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), E2NameF(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), not BOX14F(X), not BOX16F(X), E2NameF(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E1NameInvF(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), E2NameF(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), E1NameF(X), E2NameF(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), E2NameF(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), not BOX14F(X), E1NameF(X), E2NameF(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), E2NameF(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), E1NameF(X), not BOX16F(X), E2NameF(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), E2NameF(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), not BOX14F(X), not BOX16F(X), E2NameF(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E1NameInvF(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), E2NameF(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), E1NameF(X), E2NameF(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), E2NameF(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), not BOX14F(X), E1NameF(X), E2NameF(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), E2NameF(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), E1NameF(X), not BOX16F(X), E2NameF(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), E2NameF(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), not BOX14F(X), not BOX16F(X), E2NameF(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), PersonF(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV83(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not BOX22F(X), not E1NameF(X)])), 
always(or([not NVV85(X), BOX21F(X)])), 
always(or([not NVV87(X), not BOX21F(X)])), 
always(or([not NVV89, NVV90])), 
always(or([not NVV92, NVV93])), 
always(or([not NVV94, NVV95])), 
always(or([not NVV96, NVV97])), 
always(or([not NVV99, NVV100])), 
always(or([not NVV101, NVV102])), 
always(or([not NVV103, NVV104])), 
always(or([not NVV105, NVV106])), 
always(or([not NVV107, NVV108])), 
always(or([not NVV109, NVV110])), 
always(or([not NVV111, NVV112])), 
always(or([not NVV113, NVV114])), 
always(or([not NVV115, NVV116])), 
always(or([not NVV117, NVV118])), 
always(or([not NVV119, NVV120])), 
always(or([not NVV121, NVV88])), 
always(or([not NVV123, NVV124])), 
always(or([not NVV125, NVV98])), 
always(or([not NVV127, NVV128])), 
always(or([not NVV129, NVV130])), 
always(or([not NVV131, NVV122])), 
always(or([not NVV133, NVV134])), 
always(or([not NVV135, NVV136])), 
always(or([not NVV137, NVV138])), 
always(or([not NVV139, NVV140])), 
always(or([not NVV141, NVV142])), 
always(or([not NVV143, NVV91])), 
always(or([not NVV145, NVV146])), 
always(or([not NVV147, NVV148])), 
always(or([not NVV149, NVV150])), 
always(or([not NVV151, NVV152])), 
always(or([not NVV153, NVV154])), 
always(or([not NVV155, NVV156])), 
always(or([not NVV157, NVV158])), 
always(or([not NVV159, NVV132])), 
always(or([not NVV161, NVV144])),
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 BOX7P(hidden(X)))])), 
always(or([not NVV2(constant(X)), next(not BOX7P(constant(X)))])), 
always(or([not NVV3(X), next(BOX8P(hidden(X)))])), 
always(or([not NVV3(constant(X)), next(BOX8P(constant(X)))])), 
always(or([not NVV4(X), next(not BOX8P(hidden(X)))])), 
always(or([not NVV4(constant(X)), next(not BOX8P(constant(X)))])), 
always(or([not NVV5(X), next(BOX7P(hidden(X)))])), 
always(or([not NVV5(constant(X)), next(BOX7P(constant(X)))])), 
always(or([not NVV6(X), next(NVV6(hidden(X)))])), 
always(or([not NVV6(constant(X)), next(NVV6(constant(X)))])), 
always(or([not NVV9, next(NVV9)])), 
always(or([not NVV12(X), next(NVV12(hidden(X)))])), 
always(or([not NVV12(constant(X)), next(NVV12(constant(X)))])), 
always(or([not NVV15(X), next(not BOX23F(hidden(X)))])), 
always(or([not NVV15(constant(X)), next(not BOX23F(constant(X)))])), 
always(or([not NVV16, next(PinvNameF)])), 
always(or([not NVV17, next(not PinvNameF)])), 
always(or([not NVV18(X), next(BOX23F(hidden(X)))])), 
always(or([not NVV18(constant(X)), next(BOX23F(constant(X)))])), 
always(or([not NVV19(X), next(not BOX17F(hidden(X)))])), 
always(or([not NVV19(constant(X)), next(not BOX17F(constant(X)))])), 
always(or([not NVV20, next(PNameF)])), 
always(or([not NVV21, next(not PNameF)])), 
always(or([not NVV22(X), next(BOX17F(hidden(X)))])), 
always(or([not NVV22(constant(X)), next(BOX17F(constant(X)))])), 
always(or([not NVV23(X), next(not BOX1P(hidden(X)))])), 
always(or([not NVV23(constant(X)), next(not BOX1P(constant(X)))])), 
always(or([not NVV24(X), next(BOX2P(hidden(X)))])), 
always(or([not NVV24(constant(X)), next(BOX2P(constant(X)))])), 
always(or([not NVV25(X), next(not BOX2P(hidden(X)))])), 
always(or([not NVV25(constant(X)), next(not BOX2P(constant(X)))])), 
always(or([not NVV26(X), next(BOX1P(hidden(X)))])), 
always(or([not NVV26(constant(X)), next(BOX1P(constant(X)))])), 
always(or([not NVV27(X), next(not BOX3P(hidden(X)))])), 
always(or([not NVV27(constant(X)), next(not BOX3P(constant(X)))])), 
always(or([not NVV28(X), next(BOX4P(hidden(X)))])), 
always(or([not NVV28(constant(X)), next(BOX4P(constant(X)))])), 
always(or([not NVV29(X), next(not BOX4P(hidden(X)))])), 
always(or([not NVV29(constant(X)), next(not BOX4P(constant(X)))])), 
always(or([not NVV30(X), next(BOX3P(hidden(X)))])), 
always(or([not NVV30(constant(X)), next(BOX3P(constant(X)))])), 
always(or([not NVV31(X), next(not BOX11P(hidden(X)))])), 
always(or([not NVV31(constant(X)), next(not BOX11P(constant(X)))])), 
always(or([not NVV32(X), next(BOX12P(hidden(X)))])), 
always(or([not NVV32(constant(X)), next(BOX12P(constant(X)))])), 
always(or([not NVV33(X), next(not BOX12P(hidden(X)))])), 
always(or([not NVV33(constant(X)), next(not BOX12P(constant(X)))])), 
always(or([not NVV34(X), next(BOX11P(hidden(X)))])), 
always(or([not NVV34(constant(X)), next(BOX11P(constant(X)))])), 
always(or([not NVV35(X), next(not BOX5P(hidden(X)))])), 
always(or([not NVV35(constant(X)), next(not BOX5P(constant(X)))])), 
always(or([not NVV36(X), next(BOX6P(hidden(X)))])), 
always(or([not NVV36(constant(X)), next(BOX6P(constant(X)))])), 
always(or([not NVV37(X), next(not BOX6P(hidden(X)))])), 
always(or([not NVV37(constant(X)), next(not BOX6P(constant(X)))])), 
always(or([not NVV38(X), next(BOX5P(hidden(X)))])), 
always(or([not NVV38(constant(X)), next(BOX5P(constant(X)))])), 
always(or([not NVV39(X), next(NVV39(hidden(X)))])), 
always(or([not NVV39(constant(X)), next(NVV39(constant(X)))])), 
always(or([not NVV42(X), next(NVV42(hidden(X)))])), 
always(or([not NVV42(constant(X)), next(NVV42(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(NVV48(hidden(X)))])), 
always(or([not NVV48(constant(X)), next(NVV48(constant(X)))])), 
always(or([not NVV51(X), next(not BOX21F(hidden(X)))])), 
always(or([not NVV51(constant(X)), next(not BOX21F(constant(X)))])), 
always(or([not NVV52(X), next(E1NameInvF(hidden(X)))])), 
always(or([not NVV52(constant(X)), next(E1NameInvF(constant(X)))])), 
always(or([not NVV53(X), next(not E1NameInvF(hidden(X)))])), 
always(or([not NVV53(constant(X)), next(not E1NameInvF(constant(X)))])), 
always(or([not NVV54(X), next(BOX21F(hidden(X)))])), 
always(or([not NVV54(constant(X)), next(BOX21F(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(X), next(not BOX19F(hidden(X)))])), 
always(or([not NVV58(constant(X)), next(not BOX19F(constant(X)))])), 
always(or([not NVV59(X), next(E2NameF(hidden(X)))])), 
always(or([not NVV59(constant(X)), next(E2NameF(constant(X)))])), 
always(or([not NVV60(X), next(not E2NameF(hidden(X)))])), 
always(or([not NVV60(constant(X)), next(not E2NameF(constant(X)))])), 
always(or([not NVV61(X), next(BOX19F(hidden(X)))])), 
always(or([not NVV61(constant(X)), next(BOX19F(constant(X)))])), 
always(or([not NVV62(X), next(not BOX9P(hidden(X)))])), 
always(or([not NVV62(constant(X)), next(not BOX9P(constant(X)))])), 
always(or([not NVV63(X), next(BOX10P(hidden(X)))])), 
always(or([not NVV63(constant(X)), next(BOX10P(constant(X)))])), 
always(or([not NVV64(X), next(not BOX10P(hidden(X)))])), 
always(or([not NVV64(constant(X)), next(not BOX10P(constant(X)))])), 
always(or([not NVV65(X), next(BOX9P(hidden(X)))])), 
always(or([not NVV65(constant(X)), next(BOX9P(constant(X)))])), 
always(or([not NVV66, next(NVV66)])), 
always(or([not NVV69(X), next(not BOX15F(hidden(X)))])), 
always(or([not NVV69(constant(X)), next(not BOX15F(constant(X)))])), 
always(or([not NVV70(X), next(E1NameF(hidden(X)))])), 
always(or([not NVV70(constant(X)), next(E1NameF(constant(X)))])), 
always(or([not NVV71(X), next(not E1NameF(hidden(X)))])), 
always(or([not NVV71(constant(X)), next(not E1NameF(constant(X)))])), 
always(or([not NVV72(X), next(BOX15F(hidden(X)))])), 
always(or([not NVV72(constant(X)), next(BOX15F(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(not BOX13F(hidden(X)))])), 
always(or([not NVV79(constant(X)), next(not BOX13F(constant(X)))])), 
always(or([not NVV80(X), next(NVV81(hidden(X)))])), 
always(or([not NVV80(constant(X)), next(NVV81(constant(X)))])), 
always(or([not NVV82(X), next(NVV83(hidden(X)))])), 
always(or([not NVV82(constant(X)), next(NVV83(constant(X)))])), 
always(or([not NVV84(X), next(BOX13F(hidden(X)))])), 
always(or([not NVV84(constant(X)), next(BOX13F(constant(X)))])), 
always(or([not NVV85(X), next(NVV85(hidden(X)))])), 
always(or([not NVV85(constant(X)), next(NVV85(constant(X)))])), 
always(or([not NVV88, next(NVV89)])), 
always(or([not NVV90, next(E1NameF(John))])), 
always(or([not NVV91, next(NVV92)])), 
always(or([not NVV93, next(NVV94)])), 
always(or([not NVV95, next(NVV96)])), 
always(or([not NVV97, next(E1NameInvF(N0))])), 
always(or([not NVV98, next(NVV99)])), 
always(or([not NVV100, next(NVV101)])), 
always(or([not NVV102, next(NVV103)])), 
always(or([not NVV104, next(NVV105)])), 
always(or([not NVV106, next(NVV107)])), 
always(or([not NVV108, next(NVV109)])), 
always(or([not NVV110, next(NVV111)])), 
always(or([not NVV112, next(NVV113)])), 
always(or([not NVV114, next(NVV115)])), 
always(or([not NVV116, next(NVV117)])), 
always(or([not NVV118, next(NVV119)])), 
always(or([not NVV120, next(NVV121)])), 
always(or([not NVV122, next(NVV123)])), 
always(or([not NVV124, next(NVV125)])), 
always(or([not NVV126, next(NVV127)])), 
always(or([not NVV128, next(NVV129)])), 
always(or([not NVV130, next(NVV131)])), 
always(or([not NVV132, next(NVV133)])), 
always(or([not NVV134, next(NVV135)])), 
always(or([not NVV136, next(NVV137)])), 
always(or([not NVV138, next(NVV139)])), 
always(or([not NVV140, next(NVV141)])), 
always(or([not NVV142, next(NVV143)])), 
always(or([not NVV144, next(NVV145)])), 
always(or([not NVV146, next(NVV147)])), 
always(or([not NVV148, next(NVV149)])), 
always(or([not NVV150, next(NVV151)])), 
always(or([not NVV152, next(NVV153)])), 
always(or([not NVV154, next(NVV155)])), 
always(or([not NVV156, next(NVV157)])), 
always(or([not NVV158, next(NVV159)])), 
always(or([not NVV160, next(NVV161)])),
always(or([not NVV7(X), sometime(NVV8(X))])), 
always(or([not NVV7(constant(dName)), sometime(NVV8(constant(dName)))])), 
always(or([not NVV7(constant(dNameInv)), sometime(NVV8(constant(dNameInv)))])), 
always(or([not NVV7(constant(N0)), sometime(NVV8(constant(N0)))])), 
always(or([not NVV7(constant(John)), sometime(NVV8(constant(John)))])), 
always(or([not NVV10, sometime(NVV11)])), 
always(or([not NVV13(X), sometime(NVV14(X))])), 
always(or([not NVV13(constant(dName)), sometime(NVV14(constant(dName)))])), 
always(or([not NVV13(constant(dNameInv)), sometime(NVV14(constant(dNameInv)))])), 
always(or([not NVV13(constant(N0)), sometime(NVV14(constant(N0)))])), 
always(or([not NVV13(constant(John)), sometime(NVV14(constant(John)))])), 
always(or([not NVV40(X), sometime(NVV41(X))])), 
always(or([not NVV40(constant(dName)), sometime(NVV41(constant(dName)))])), 
always(or([not NVV40(constant(dNameInv)), sometime(NVV41(constant(dNameInv)))])), 
always(or([not NVV40(constant(N0)), sometime(NVV41(constant(N0)))])), 
always(or([not NVV40(constant(John)), sometime(NVV41(constant(John)))])), 
always(or([not NVV43(X), sometime(NVV44(X))])), 
always(or([not NVV43(constant(dName)), sometime(NVV44(constant(dName)))])), 
always(or([not NVV43(constant(dNameInv)), sometime(NVV44(constant(dNameInv)))])), 
always(or([not NVV43(constant(N0)), sometime(NVV44(constant(N0)))])), 
always(or([not NVV43(constant(John)), sometime(NVV44(constant(John)))])), 
always(or([not NVV46(X), sometime(NVV47(X))])), 
always(or([not NVV46(constant(dName)), sometime(NVV47(constant(dName)))])), 
always(or([not NVV46(constant(dNameInv)), sometime(NVV47(constant(dNameInv)))])), 
always(or([not NVV46(constant(N0)), sometime(NVV47(constant(N0)))])), 
always(or([not NVV46(constant(John)), sometime(NVV47(constant(John)))])), 
always(or([not NVV49(X), sometime(NVV50(X))])), 
always(or([not NVV49(constant(dName)), sometime(NVV50(constant(dName)))])), 
always(or([not NVV49(constant(dNameInv)), sometime(NVV50(constant(dNameInv)))])), 
always(or([not NVV49(constant(N0)), sometime(NVV50(constant(N0)))])), 
always(or([not NVV49(constant(John)), sometime(NVV50(constant(John)))])), 
always(or([not NVV56(X), sometime(NVV57(X))])), 
always(or([not NVV56(constant(dName)), sometime(NVV57(constant(dName)))])), 
always(or([not NVV56(constant(dNameInv)), sometime(NVV57(constant(dNameInv)))])), 
always(or([not NVV56(constant(N0)), sometime(NVV57(constant(N0)))])), 
always(or([not NVV56(constant(John)), sometime(NVV57(constant(John)))])), 
always(or([not NVV67, sometime(NVV68)])), 
always(or([not NVV74(X), sometime(NVV75(X))])), 
always(or([not NVV74(constant(dName)), sometime(NVV75(constant(dName)))])), 
always(or([not NVV74(constant(dNameInv)), sometime(NVV75(constant(dNameInv)))])), 
always(or([not NVV74(constant(N0)), sometime(NVV75(constant(N0)))])), 
always(or([not NVV74(constant(John)), sometime(NVV75(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 NVV86(X), sometime(NVV87(X))])), 
always(or([not NVV86(constant(dName)), sometime(NVV87(constant(dName)))])), 
always(or([not NVV86(constant(dNameInv)), sometime(NVV87(constant(dNameInv)))])), 
always(or([not NVV86(constant(N0)), sometime(NVV87(constant(N0)))])), 
always(or([not NVV86(constant(John)), sometime(NVV87(constant(John)))]))]).

