and([
or([BOX0F(X)]), 
or([NVV1(X)]), 
or([not BOX13F(X), BOX2P(X)]), 
or([not BOX2P(X), BOX13F(X)]), 
or([not E2NameF(X), E2NameP(X)]), 
or([not E2NameP(X), E2NameF(X)]), 
or([not BOX17F(X), BOX6P(X)]), 
or([not BOX6P(X), BOX17F(X)]), 
or([not BOX22F(X), BOX11P(X)]), 
or([not BOX11P(X), BOX22F(X)]), 
or([not BOX23F(X), BOX12P(X)]), 
or([not BOX12P(X), BOX23F(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 PinvNameF, PinvNameP]), 
or([not PinvNameP, PinvNameF]), 
or([not BOX0F(X), BOX1P(X)]), 
or([not BOX1P(X), BOX0F(X)]), 
or([not BOX19F(X), BOX8P(X)]), 
or([not BOX8P(X), BOX19F(X)]), 
or([not BOX21F(X), BOX10P(X)]), 
or([not BOX10P(X), BOX21F(X)]), 
or([not BOX20F(X), BOX9P(X)]), 
or([not BOX9P(X), BOX20F(X)]), 
or([not BOX18F(X), BOX7P(X)]), 
or([not BOX7P(X), BOX18F(X)]), 
or([not PNameF, PNameP]), 
or([not PNameP, PNameF]), 
or([not E1NameF(X), E1NameP(X)]), 
or([not E1NameP(X), E1NameF(X)]), 
or([not PersonF(X), PersonP(X)]), 
or([not PersonP(X), PersonF(X)]), 
or([not BOX14F(X), BOX3P(X)]), 
or([not BOX3P(X), BOX14F(X)]), 
or([not PinvNameF, E1NameF(constant(dName))]), 
or([not PNameF, E1NameInvF(constant(dNameInv))]), 
or([NVV88]), 
or([NVV108]), 
or([NVV124]), 
or([NVV157]), 
or([NVV162]), 
or([NVV118]), 
or([NVV94]), 
or([NVV184]), 
or([NVV176]), 
or([NVV196]), 
or([NVV144]), 
or([NVV192]), 
or([NVV204]), 
or([NVV120]), 
or([NVV122]), 
or([NVV136]), 
or([NVV96]), 
or([NVV174]), 
or([NVV134]), 
or([NVV128]), 
or([NVV224]), 
or([NVV190]), 
or([NVV106]), 
or([NVV234]), 
or([NVV194]), 
or([NVV150]), 
or([E1NameInvF(constant(N0))]), 
or([NVV112]), 
or([NVV130]), 
or([NVV198]), 
or([NVV90]), 
or([NVV114]), 
or([NVV172]), 
or([E2NameF(constant(John))]), 
or([NVV142]), 
or([NVV218]), 
or([NVV126]), 
or([NVV200]), 
or([NVV116]), 
or([NVV138]), 
or([NVV216]), 
or([NVV92]), 
or([NVV182]), 
or([NVV168]), 
or([NVV178]), 
or([NVV236]), 
or([NVV230]), 
or([NVV240]), 
or([NVV202]), 
or([NVV214]), 
or([NVV228]), 
or([NVV212]), 
or([NVV159]), 
or([NVV154]), 
or([NVV98]), 
or([NVV220]), 
or([NVV132]), 
or([NVV222]), 
or([NVV104]), 
or([NVV164]), 
or([NVV110]), 
or([NVV232]), 
or([NVV166]), 
or([NVV170]), 
or([NVV238]), 
or([NVV161]), 
or([PersonF(constant(John))]), 
or([NVV146]), 
or([NVV148]), 
or([NVV188]), 
or([NVV226]), 
or([NVV186]), 
or([NVV140]), 
or([NVV152]), 
or([NVV102]), 
or([NVV180]), 
or([NVV156]), 
or([NVV206]), 
or([NVV208]), 
or([NVV100]), 
or([NVV210]),
always(or([not NVV1(X), not BOX4P(X), NVV2])), 
always(or([not NVV1(X), NVV3, BOX4P(X)])), 
always(or([not NVV1(X), NVV5(X), BOX13F(X)])), 
always(or([not NVV1(X), NVV5(X), NVV6(X)])), 
always(or([not NVV1(X), not BOX13F(X), NVV8(X), NVV10(X)])), 
always(or([not NVV1(X), not BOX0F(X), NVV11(X)])), 
always(or([not NVV1(X), NVV12(X), BOX0F(X)])), 
always(or([not NVV1(X), NVV14(X), BOX17F(X)])), 
always(or([not NVV1(X), NVV14(X), NVV15(X)])), 
always(or([not NVV1(X), not BOX17F(X), NVV16(X), NVV17(X)])), 
always(or([not NVV1(X), NVV18(X), BOX11P(X)])), 
always(or([not NVV1(X), NVV18(X), NVV19(X)])), 
always(or([not NVV1(X), not BOX11P(X), NVV20(X), NVV21(X)])), 
always(or([not NVV1(X), not BOX16F(X), NVV22(X)])), 
always(or([not NVV1(X), NVV23(X), BOX16F(X)])), 
always(or([not NVV1(X), not BOX2P(X), NVV25(X)])), 
always(or([not NVV1(X), NVV26(X), BOX2P(X)])), 
always(or([not NVV1(X), NVV28(X), BOX7P(X)])), 
always(or([not NVV1(X), NVV28(X), NVV29(X)])), 
always(or([not NVV1(X), not BOX7P(X), NVV30(X), NVV31(X)])), 
always(or([not NVV1(X), not BOX20F(X), NVV32(X)])), 
always(or([not NVV1(X), NVV33(X), BOX20F(X)])), 
always(or([not NVV1(X), NVV35(X), BOX3P(X)])), 
always(or([not NVV1(X), NVV35(X), NVV36(X)])), 
always(or([not NVV1(X), not BOX3P(X), NVV37(X), NVV38(X)])), 
always(or([not NVV1(X), not BOX14F(X), NVV39(X)])), 
always(or([not NVV1(X), NVV40(X), BOX14F(X)])), 
always(or([not NVV1(X), NVV42(X), BOX21F(X)])), 
always(or([not NVV1(X), NVV42(X), NVV43(X)])), 
always(or([not NVV1(X), not BOX21F(X), NVV44(X), NVV45(X)])), 
always(or([not NVV1(X), NVV46(X), BOX19F(X)])), 
always(or([not NVV1(X), NVV46(X), NVV47])), 
always(or([not NVV1(X), not BOX19F(X), NVV48, NVV49(X)])), 
always(or([not NVV1(X), NVV50(X), BOX5P(X)])), 
always(or([not NVV1(X), NVV50(X), NVV51(X)])), 
always(or([not NVV1(X), not BOX5P(X), NVV52(X), NVV53(X)])), 
always(or([not NVV1(X), not BOX18F(X), NVV54(X)])), 
always(or([not NVV1(X), NVV55(X), BOX18F(X)])), 
always(or([not NVV1(X), NVV57(X), BOX23F(X)])), 
always(or([not NVV1(X), NVV57(X), NVV58(X)])), 
always(or([not NVV1(X), not BOX23F(X), NVV59(X), NVV60(X)])), 
always(or([not NVV1(X), NVV61(X), BOX15F(X)])), 
always(or([not NVV1(X), NVV61(X), NVV62])), 
always(or([not NVV1(X), not BOX15F(X), NVV63, NVV64(X)])), 
always(or([not NVV1(X), not BOX8P(X), NVV65])), 
always(or([not NVV1(X), NVV66, BOX8P(X)])), 
always(or([not NVV1(X), not BOX10P(X), NVV68(X)])), 
always(or([not NVV1(X), NVV69(X), BOX10P(X)])), 
always(or([not NVV1(X), NVV71(X), BOX1P(X)])), 
always(or([not NVV1(X), NVV71(X), NVV72(X)])), 
always(or([not NVV1(X), not BOX1P(X), NVV73(X), NVV74(X)])), 
always(or([not NVV1(X), not BOX22F(X), NVV75(X)])), 
always(or([not NVV1(X), NVV76(X), BOX22F(X)])), 
always(or([not NVV1(X), not BOX12P(X), NVV78(X)])), 
always(or([not NVV1(X), NVV79(X), BOX12P(X)])), 
always(or([not NVV1(X), NVV81(X), BOX9P(X)])), 
always(or([not NVV1(X), NVV81(X), NVV82(X)])), 
always(or([not NVV1(X), not BOX9P(X), NVV83(X), NVV84(X)])), 
always(or([not NVV1(X), not BOX6P(X), NVV85(X)])), 
always(or([not NVV1(X), NVV86(X), BOX6P(X)])), 
always(or([not NVV2, PNameP])), 
always(or([not NVV4, not PNameP])), 
always(or([not NVV7(X), not PersonF(X), not E2NameF(X)])), 
always(or([not NVV7(X), not PersonF(X), E1NameF(X)])), 
always(or([not NVV7(X), not E1NameF(X), BOX14F(X)])), 
always(or([not NVV7(X), not E1NameF(X), BOX16F(X)])), 
always(or([not NVV7(X), not E1NameInvF(X), BOX18F(X)])), 
always(or([not NVV7(X), not E2NameF(X), BOX20F(X)])), 
always(or([not NVV7(X), not E2NameF(X), E1NameF(X)])), 
always(or([not NVV7(X), not E1NameInvF(X), BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameF(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), E1NameF(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX16F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX16F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX18F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX18F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX18F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E2NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E1NameF(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not BOX14F(X), E1NameF(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E1NameF(X), not BOX16F(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not BOX14F(X), not BOX16F(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX18F(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E1NameF(X), not BOX18F(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), E1NameF(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), E1NameF(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), not BOX14F(X), E1NameF(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), E1NameF(X), not BOX16F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), E1NameInvF(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), E1NameInvF(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), E1NameInvF(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), E1NameInvF(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX18F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX18F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX18F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), E1NameInvF(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), E1NameInvF(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), E1NameInvF(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), E2NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), E1NameInvF(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E1NameF(X), E1NameInvF(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX18F(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E1NameF(X), not BOX18F(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not BOX14F(X), E1NameF(X), not BOX18F(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), E1NameF(X), E1NameInvF(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), E1NameInvF(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), E1NameF(X), E1NameInvF(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), not BOX14F(X), E1NameF(X), E1NameInvF(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), E1NameF(X), not BOX16F(X), E1NameInvF(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), not BOX14F(X), E1NameF(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), E1NameF(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV9(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not BOX20F(X), not E1NameF(X), not BOX22F(X)])), 
always(or([not NVV11(X), BOX13F(X)])), 
always(or([not NVV13(X), not BOX13F(X)])), 
always(or([not NVV22(X), BOX17F(X)])), 
always(or([not NVV24(X), not BOX17F(X)])), 
always(or([not NVV25(X), not PersonP(X), not E2NameP(X)])), 
always(or([not NVV25(X), not PersonP(X), E1NameP(X)])), 
always(or([not NVV25(X), not E1NameP(X), BOX3P(X)])), 
always(or([not NVV25(X), not E1NameP(X), BOX5P(X)])), 
always(or([not NVV25(X), not E1NameInvP(X), BOX7P(X)])), 
always(or([not NVV25(X), not E2NameP(X), BOX9P(X)])), 
always(or([not NVV25(X), not E2NameP(X), E1NameP(X)])), 
always(or([not NVV25(X), not E1NameInvP(X), BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameP(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), E1NameP(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX5P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX5P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX7P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX7P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX7P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E2NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E1NameP(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not BOX3P(X), E1NameP(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E1NameP(X), not BOX5P(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not BOX3P(X), not BOX5P(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX7P(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E1NameP(X), not BOX7P(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), E1NameP(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), E1NameP(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), not BOX3P(X), E1NameP(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), E1NameP(X), not BOX5P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), E1NameInvP(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), E1NameInvP(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), E1NameInvP(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), E1NameInvP(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX7P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX7P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX7P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), E1NameInvP(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), E1NameInvP(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), E1NameInvP(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), E2NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), E1NameInvP(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E1NameP(X), E1NameInvP(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX7P(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E1NameP(X), not BOX7P(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not BOX3P(X), E1NameP(X), not BOX7P(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), E1NameP(X), E1NameInvP(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), E1NameInvP(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), E1NameP(X), E1NameInvP(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), not BOX3P(X), E1NameP(X), E1NameInvP(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), E1NameP(X), not BOX5P(X), E1NameInvP(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), not BOX3P(X), E1NameP(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), E1NameP(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV27(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not BOX9P(X), not E1NameP(X), not BOX11P(X)])), 
always(or([not NVV32(X), BOX21F(X)])), 
always(or([not NVV34(X), not BOX21F(X)])), 
always(or([not NVV39(X), BOX15F(X)])), 
always(or([not NVV41(X), not BOX15F(X)])), 
always(or([not NVV54(X), BOX19F(X)])), 
always(or([not NVV56(X), not BOX19F(X)])), 
always(or([not NVV65, PinvNameP])), 
always(or([not NVV67, not PinvNameP])), 
always(or([not NVV68(X), E2NameP(X)])), 
always(or([not NVV70(X), not E2NameP(X)])), 
always(or([not NVV75(X), BOX23F(X)])), 
always(or([not NVV77(X), not BOX23F(X)])), 
always(or([not NVV78(X), E1NameInvP(X)])), 
always(or([not NVV80(X), not E1NameInvP(X)])), 
always(or([not NVV85(X), E1NameP(X)])), 
always(or([not NVV87(X), not E1NameP(X)])), 
always(or([not NVV89, NVV90])), 
always(or([not NVV91, NVV92])), 
always(or([not NVV93, NVV94])), 
always(or([not NVV95, NVV96])), 
always(or([not NVV97, NVV98])), 
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, NVV122])), 
always(or([not NVV123, NVV124])), 
always(or([not NVV125, NVV126])), 
always(or([not NVV127, NVV128])), 
always(or([not NVV129, NVV130])), 
always(or([not NVV131, NVV132])), 
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, NVV144])), 
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 NVV158, NVV159])), 
always(or([not NVV160, NVV161])), 
always(or([not NVV163, NVV164])), 
always(or([not NVV165, NVV166])), 
always(or([not NVV167, NVV168])), 
always(or([not NVV169, NVV170])), 
always(or([not NVV171, NVV172])), 
always(or([not NVV173, NVV174])), 
always(or([not NVV175, NVV176])), 
always(or([not NVV177, NVV178])), 
always(or([not NVV179, NVV180])), 
always(or([not NVV181, NVV182])), 
always(or([not NVV183, NVV157])), 
always(or([not NVV185, NVV186])), 
always(or([not NVV187, NVV188])), 
always(or([not NVV189, NVV190])), 
always(or([not NVV191, NVV192])), 
always(or([not NVV193, NVV194])), 
always(or([not NVV195, NVV162])), 
always(or([not NVV197, NVV198])), 
always(or([not NVV199, NVV200])), 
always(or([not NVV201, NVV202])), 
always(or([not NVV203, NVV184])), 
always(or([not NVV205, NVV206])), 
always(or([not NVV207, NVV208])), 
always(or([not NVV209, NVV210])), 
always(or([not NVV211, NVV212])), 
always(or([not NVV213, NVV214])), 
always(or([not NVV215, NVV216])), 
always(or([not NVV217, NVV218])), 
always(or([not NVV219, NVV220])), 
always(or([not NVV221, NVV222])), 
always(or([not NVV223, NVV224])), 
always(or([not NVV225, NVV226])), 
always(or([not NVV227, NVV228])), 
always(or([not NVV229, NVV230])), 
always(or([not NVV231, NVV232])), 
always(or([not NVV233, NVV196])), 
always(or([not NVV235, NVV236])), 
always(or([not NVV237, NVV238])), 
always(or([not NVV239, NVV88])), 
always(or([not NVV241, NVV242])), 
always(or([not NVV243, NVV244])), 
always(or([not NVV245, NVV246])), 
always(or([not NVV247, NVV248])), 
always(or([not NVV249, NVV250])), 
always(or([not NVV251, NVV252])), 
always(or([not NVV253, NVV254])), 
always(or([not NVV255, NVV256])), 
always(or([not NVV257, NVV258])), 
always(or([not NVV259, NVV260])), 
always(or([not NVV261, NVV262])), 
always(or([not NVV263, NVV264])), 
always(or([not NVV265, NVV266])), 
always(or([not NVV267, NVV268])), 
always(or([not NVV269, NVV270])), 
always(or([not NVV271, NVV272])), 
always(or([not NVV273, NVV274])), 
always(or([not NVV275, NVV276])), 
always(or([not NVV277, NVV278])), 
always(or([not NVV279, NVV280])), 
always(or([not NVV281, NVV282])), 
always(or([not NVV283, NVV284])), 
always(or([not NVV285, NVV286])), 
always(or([not NVV287, NVV288])), 
always(or([not NVV289, NVV290])), 
always(or([not NVV291, NVV292])), 
always(or([not NVV293, NVV294])), 
always(or([not NVV295, NVV296])), 
always(or([not NVV297, NVV298])), 
always(or([not NVV299, NVV300])), 
always(or([not NVV301, NVV302])), 
always(or([not NVV303, NVV304])), 
always(or([not NVV305, NVV306])), 
always(or([not NVV307, NVV308])), 
always(or([not NVV309, NVV310])), 
always(or([not NVV311, NVV312])), 
always(or([not NVV313, NVV314])), 
always(or([not NVV315, NVV316])),
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(not BOX13F(hidden(X)))])), 
always(or([not NVV5(constant(X)), next(not BOX13F(constant(X)))])), 
always(or([not NVV6(X), next(NVV7(hidden(X)))])), 
always(or([not NVV6(constant(X)), next(NVV7(constant(X)))])), 
always(or([not NVV8(X), next(NVV9(hidden(X)))])), 
always(or([not NVV8(constant(X)), next(NVV9(constant(X)))])), 
always(or([not NVV10(X), next(BOX13F(hidden(X)))])), 
always(or([not NVV10(constant(X)), next(BOX13F(constant(X)))])), 
always(or([not NVV11(X), next(NVV11(hidden(X)))])), 
always(or([not NVV11(constant(X)), next(NVV11(constant(X)))])), 
always(or([not NVV14(X), next(not BOX17F(hidden(X)))])), 
always(or([not NVV14(constant(X)), next(not BOX17F(constant(X)))])), 
always(or([not NVV15(X), next(E1NameF(hidden(X)))])), 
always(or([not NVV15(constant(X)), next(E1NameF(constant(X)))])), 
always(or([not NVV16(X), next(not E1NameF(hidden(X)))])), 
always(or([not NVV16(constant(X)), next(not E1NameF(constant(X)))])), 
always(or([not NVV17(X), next(BOX17F(hidden(X)))])), 
always(or([not NVV17(constant(X)), next(BOX17F(constant(X)))])), 
always(or([not NVV18(X), next(not BOX11P(hidden(X)))])), 
always(or([not NVV18(constant(X)), next(not BOX11P(constant(X)))])), 
always(or([not NVV19(X), next(BOX12P(hidden(X)))])), 
always(or([not NVV19(constant(X)), next(BOX12P(constant(X)))])), 
always(or([not NVV20(X), next(not BOX12P(hidden(X)))])), 
always(or([not NVV20(constant(X)), next(not BOX12P(constant(X)))])), 
always(or([not NVV21(X), next(BOX11P(hidden(X)))])), 
always(or([not NVV21(constant(X)), next(BOX11P(constant(X)))])), 
always(or([not NVV22(X), next(NVV22(hidden(X)))])), 
always(or([not NVV22(constant(X)), next(NVV22(constant(X)))])), 
always(or([not NVV25(X), next(NVV25(hidden(X)))])), 
always(or([not NVV25(constant(X)), next(NVV25(constant(X)))])), 
always(or([not NVV28(X), next(not BOX7P(hidden(X)))])), 
always(or([not NVV28(constant(X)), next(not BOX7P(constant(X)))])), 
always(or([not NVV29(X), next(BOX8P(hidden(X)))])), 
always(or([not NVV29(constant(X)), next(BOX8P(constant(X)))])), 
always(or([not NVV30(X), next(not BOX8P(hidden(X)))])), 
always(or([not NVV30(constant(X)), next(not BOX8P(constant(X)))])), 
always(or([not NVV31(X), next(BOX7P(hidden(X)))])), 
always(or([not NVV31(constant(X)), next(BOX7P(constant(X)))])), 
always(or([not NVV32(X), next(NVV32(hidden(X)))])), 
always(or([not NVV32(constant(X)), next(NVV32(constant(X)))])), 
always(or([not NVV35(X), next(not BOX3P(hidden(X)))])), 
always(or([not NVV35(constant(X)), next(not BOX3P(constant(X)))])), 
always(or([not NVV36(X), next(BOX4P(hidden(X)))])), 
always(or([not NVV36(constant(X)), next(BOX4P(constant(X)))])), 
always(or([not NVV37(X), next(not BOX4P(hidden(X)))])), 
always(or([not NVV37(constant(X)), next(not BOX4P(constant(X)))])), 
always(or([not NVV38(X), next(BOX3P(hidden(X)))])), 
always(or([not NVV38(constant(X)), next(BOX3P(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(not BOX21F(hidden(X)))])), 
always(or([not NVV42(constant(X)), next(not BOX21F(constant(X)))])), 
always(or([not NVV43(X), next(E2NameF(hidden(X)))])), 
always(or([not NVV43(constant(X)), next(E2NameF(constant(X)))])), 
always(or([not NVV44(X), next(not E2NameF(hidden(X)))])), 
always(or([not NVV44(constant(X)), next(not E2NameF(constant(X)))])), 
always(or([not NVV45(X), next(BOX21F(hidden(X)))])), 
always(or([not NVV45(constant(X)), next(BOX21F(constant(X)))])), 
always(or([not NVV46(X), next(not BOX19F(hidden(X)))])), 
always(or([not NVV46(constant(X)), next(not BOX19F(constant(X)))])), 
always(or([not NVV47, next(PinvNameF)])), 
always(or([not NVV48, next(not PinvNameF)])), 
always(or([not NVV49(X), next(BOX19F(hidden(X)))])), 
always(or([not NVV49(constant(X)), next(BOX19F(constant(X)))])), 
always(or([not NVV50(X), next(not BOX5P(hidden(X)))])), 
always(or([not NVV50(constant(X)), next(not BOX5P(constant(X)))])), 
always(or([not NVV51(X), next(BOX6P(hidden(X)))])), 
always(or([not NVV51(constant(X)), next(BOX6P(constant(X)))])), 
always(or([not NVV52(X), next(not BOX6P(hidden(X)))])), 
always(or([not NVV52(constant(X)), next(not BOX6P(constant(X)))])), 
always(or([not NVV53(X), next(BOX5P(hidden(X)))])), 
always(or([not NVV53(constant(X)), next(BOX5P(constant(X)))])), 
always(or([not NVV54(X), next(NVV54(hidden(X)))])), 
always(or([not NVV54(constant(X)), next(NVV54(constant(X)))])), 
always(or([not NVV57(X), next(not BOX23F(hidden(X)))])), 
always(or([not NVV57(constant(X)), next(not BOX23F(constant(X)))])), 
always(or([not NVV58(X), next(E1NameInvF(hidden(X)))])), 
always(or([not NVV58(constant(X)), next(E1NameInvF(constant(X)))])), 
always(or([not NVV59(X), next(not E1NameInvF(hidden(X)))])), 
always(or([not NVV59(constant(X)), next(not E1NameInvF(constant(X)))])), 
always(or([not NVV60(X), next(BOX23F(hidden(X)))])), 
always(or([not NVV60(constant(X)), next(BOX23F(constant(X)))])), 
always(or([not NVV61(X), next(not BOX15F(hidden(X)))])), 
always(or([not NVV61(constant(X)), next(not BOX15F(constant(X)))])), 
always(or([not NVV62, next(PNameF)])), 
always(or([not NVV63, next(not PNameF)])), 
always(or([not NVV64(X), next(BOX15F(hidden(X)))])), 
always(or([not NVV64(constant(X)), next(BOX15F(constant(X)))])), 
always(or([not NVV65, next(NVV65)])), 
always(or([not NVV68(X), next(NVV68(hidden(X)))])), 
always(or([not NVV68(constant(X)), next(NVV68(constant(X)))])), 
always(or([not NVV71(X), next(not BOX1P(hidden(X)))])), 
always(or([not NVV71(constant(X)), next(not BOX1P(constant(X)))])), 
always(or([not NVV72(X), next(BOX2P(hidden(X)))])), 
always(or([not NVV72(constant(X)), next(BOX2P(constant(X)))])), 
always(or([not NVV73(X), next(not BOX2P(hidden(X)))])), 
always(or([not NVV73(constant(X)), next(not BOX2P(constant(X)))])), 
always(or([not NVV74(X), next(BOX1P(hidden(X)))])), 
always(or([not NVV74(constant(X)), next(BOX1P(constant(X)))])), 
always(or([not NVV75(X), next(NVV75(hidden(X)))])), 
always(or([not NVV75(constant(X)), next(NVV75(constant(X)))])), 
always(or([not NVV78(X), next(NVV78(hidden(X)))])), 
always(or([not NVV78(constant(X)), next(NVV78(constant(X)))])), 
always(or([not NVV81(X), next(not BOX9P(hidden(X)))])), 
always(or([not NVV81(constant(X)), next(not BOX9P(constant(X)))])), 
always(or([not NVV82(X), next(BOX10P(hidden(X)))])), 
always(or([not NVV82(constant(X)), next(BOX10P(constant(X)))])), 
always(or([not NVV83(X), next(not BOX10P(hidden(X)))])), 
always(or([not NVV83(constant(X)), next(not BOX10P(constant(X)))])), 
always(or([not NVV84(X), next(BOX9P(hidden(X)))])), 
always(or([not NVV84(constant(X)), next(BOX9P(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(NVV91)])), 
always(or([not NVV92, next(NVV93)])), 
always(or([not NVV94, next(NVV95)])), 
always(or([not NVV96, next(NVV97)])), 
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(E1NameInvF(N0))])), 
always(or([not NVV157, next(NVV158)])), 
always(or([not NVV159, next(NVV160)])), 
always(or([not NVV161, next(E2NameF(John))])), 
always(or([not NVV162, next(NVV163)])), 
always(or([not NVV164, next(NVV165)])), 
always(or([not NVV166, next(NVV167)])), 
always(or([not NVV168, next(NVV169)])), 
always(or([not NVV170, next(NVV171)])), 
always(or([not NVV172, next(NVV173)])), 
always(or([not NVV174, next(NVV175)])), 
always(or([not NVV176, next(NVV177)])), 
always(or([not NVV178, next(NVV179)])), 
always(or([not NVV180, next(NVV181)])), 
always(or([not NVV182, next(NVV183)])), 
always(or([not NVV184, next(NVV185)])), 
always(or([not NVV186, next(NVV187)])), 
always(or([not NVV188, next(NVV189)])), 
always(or([not NVV190, next(NVV191)])), 
always(or([not NVV192, next(NVV193)])), 
always(or([not NVV194, next(NVV195)])), 
always(or([not NVV196, next(NVV197)])), 
always(or([not NVV198, next(NVV199)])), 
always(or([not NVV200, next(NVV201)])), 
always(or([not NVV202, next(NVV203)])), 
always(or([not NVV204, next(NVV205)])), 
always(or([not NVV206, next(NVV207)])), 
always(or([not NVV208, next(NVV209)])), 
always(or([not NVV210, next(NVV211)])), 
always(or([not NVV212, next(NVV213)])), 
always(or([not NVV214, next(NVV215)])), 
always(or([not NVV216, next(NVV217)])), 
always(or([not NVV218, next(NVV219)])), 
always(or([not NVV220, next(NVV221)])), 
always(or([not NVV222, next(NVV223)])), 
always(or([not NVV224, next(NVV225)])), 
always(or([not NVV226, next(NVV227)])), 
always(or([not NVV228, next(NVV229)])), 
always(or([not NVV230, next(NVV231)])), 
always(or([not NVV232, next(NVV233)])), 
always(or([not NVV234, next(NVV235)])), 
always(or([not NVV236, next(NVV237)])), 
always(or([not NVV238, next(NVV239)])), 
always(or([not NVV240, next(NVV241)])), 
always(or([not NVV242, next(NVV243)])), 
always(or([not NVV244, next(NVV245)])), 
always(or([not NVV246, next(NVV247)])), 
always(or([not NVV248, next(NVV249)])), 
always(or([not NVV250, next(NVV251)])), 
always(or([not NVV252, next(NVV253)])), 
always(or([not NVV254, next(NVV255)])), 
always(or([not NVV256, next(NVV257)])), 
always(or([not NVV258, next(NVV259)])), 
always(or([not NVV260, next(NVV261)])), 
always(or([not NVV262, next(NVV263)])), 
always(or([not NVV264, next(NVV265)])), 
always(or([not NVV266, next(NVV267)])), 
always(or([not NVV268, next(NVV269)])), 
always(or([not NVV270, next(NVV271)])), 
always(or([not NVV272, next(NVV273)])), 
always(or([not NVV274, next(NVV275)])), 
always(or([not NVV276, next(NVV277)])), 
always(or([not NVV278, next(NVV279)])), 
always(or([not NVV280, next(NVV281)])), 
always(or([not NVV282, next(NVV283)])), 
always(or([not NVV284, next(NVV285)])), 
always(or([not NVV286, next(NVV287)])), 
always(or([not NVV288, next(NVV289)])), 
always(or([not NVV290, next(NVV291)])), 
always(or([not NVV292, next(NVV293)])), 
always(or([not NVV294, next(NVV295)])), 
always(or([not NVV296, next(NVV297)])), 
always(or([not NVV298, next(NVV299)])), 
always(or([not NVV300, next(NVV301)])), 
always(or([not NVV302, next(NVV303)])), 
always(or([not NVV304, next(NVV305)])), 
always(or([not NVV306, next(NVV307)])), 
always(or([not NVV308, next(NVV309)])), 
always(or([not NVV310, next(NVV311)])), 
always(or([not NVV312, next(NVV313)])), 
always(or([not NVV314, next(NVV315)])), 
always(or([not NVV316, next(E1NameInvF(N1))])),
always(or([not NVV3, sometime(NVV4)])), 
always(or([not NVV12(X), sometime(NVV13(X))])), 
always(or([not NVV12(constant(dName)), sometime(NVV13(constant(dName)))])), 
always(or([not NVV12(constant(dNameInv)), sometime(NVV13(constant(dNameInv)))])), 
always(or([not NVV12(constant(N1)), sometime(NVV13(constant(N1)))])), 
always(or([not NVV12(constant(N0)), sometime(NVV13(constant(N0)))])), 
always(or([not NVV12(constant(John)), sometime(NVV13(constant(John)))])), 
always(or([not NVV23(X), sometime(NVV24(X))])), 
always(or([not NVV23(constant(dName)), sometime(NVV24(constant(dName)))])), 
always(or([not NVV23(constant(dNameInv)), sometime(NVV24(constant(dNameInv)))])), 
always(or([not NVV23(constant(N1)), sometime(NVV24(constant(N1)))])), 
always(or([not NVV23(constant(N0)), sometime(NVV24(constant(N0)))])), 
always(or([not NVV23(constant(John)), sometime(NVV24(constant(John)))])), 
always(or([not NVV26(X), sometime(NVV27(X))])), 
always(or([not NVV26(constant(dName)), sometime(NVV27(constant(dName)))])), 
always(or([not NVV26(constant(dNameInv)), sometime(NVV27(constant(dNameInv)))])), 
always(or([not NVV26(constant(N1)), sometime(NVV27(constant(N1)))])), 
always(or([not NVV26(constant(N0)), sometime(NVV27(constant(N0)))])), 
always(or([not NVV26(constant(John)), sometime(NVV27(constant(John)))])), 
always(or([not NVV33(X), sometime(NVV34(X))])), 
always(or([not NVV33(constant(dName)), sometime(NVV34(constant(dName)))])), 
always(or([not NVV33(constant(dNameInv)), sometime(NVV34(constant(dNameInv)))])), 
always(or([not NVV33(constant(N1)), sometime(NVV34(constant(N1)))])), 
always(or([not NVV33(constant(N0)), sometime(NVV34(constant(N0)))])), 
always(or([not NVV33(constant(John)), sometime(NVV34(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(N1)), sometime(NVV41(constant(N1)))])), 
always(or([not NVV40(constant(N0)), sometime(NVV41(constant(N0)))])), 
always(or([not NVV40(constant(John)), sometime(NVV41(constant(John)))])), 
always(or([not NVV55(X), sometime(NVV56(X))])), 
always(or([not NVV55(constant(dName)), sometime(NVV56(constant(dName)))])), 
always(or([not NVV55(constant(dNameInv)), sometime(NVV56(constant(dNameInv)))])), 
always(or([not NVV55(constant(N1)), sometime(NVV56(constant(N1)))])), 
always(or([not NVV55(constant(N0)), sometime(NVV56(constant(N0)))])), 
always(or([not NVV55(constant(John)), sometime(NVV56(constant(John)))])), 
always(or([not NVV66, sometime(NVV67)])), 
always(or([not NVV69(X), sometime(NVV70(X))])), 
always(or([not NVV69(constant(dName)), sometime(NVV70(constant(dName)))])), 
always(or([not NVV69(constant(dNameInv)), sometime(NVV70(constant(dNameInv)))])), 
always(or([not NVV69(constant(N1)), sometime(NVV70(constant(N1)))])), 
always(or([not NVV69(constant(N0)), sometime(NVV70(constant(N0)))])), 
always(or([not NVV69(constant(John)), sometime(NVV70(constant(John)))])), 
always(or([not NVV76(X), sometime(NVV77(X))])), 
always(or([not NVV76(constant(dName)), sometime(NVV77(constant(dName)))])), 
always(or([not NVV76(constant(dNameInv)), sometime(NVV77(constant(dNameInv)))])), 
always(or([not NVV76(constant(N1)), sometime(NVV77(constant(N1)))])), 
always(or([not NVV76(constant(N0)), sometime(NVV77(constant(N0)))])), 
always(or([not NVV76(constant(John)), sometime(NVV77(constant(John)))])), 
always(or([not NVV79(X), sometime(NVV80(X))])), 
always(or([not NVV79(constant(dName)), sometime(NVV80(constant(dName)))])), 
always(or([not NVV79(constant(dNameInv)), sometime(NVV80(constant(dNameInv)))])), 
always(or([not NVV79(constant(N1)), sometime(NVV80(constant(N1)))])), 
always(or([not NVV79(constant(N0)), sometime(NVV80(constant(N0)))])), 
always(or([not NVV79(constant(John)), sometime(NVV80(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(N1)), sometime(NVV87(constant(N1)))])), 
always(or([not NVV86(constant(N0)), sometime(NVV87(constant(N0)))])), 
always(or([not NVV86(constant(John)), sometime(NVV87(constant(John)))]))]).

