and([
or([BOX0F(X)]), 
or([NVV1(X)]), 
or([not BOX18F(X), BOX7P(X)]), 
or([not BOX7P(X), BOX18F(X)]), 
or([not PNameF, PNameP]), 
or([not PNameP, PNameF]), 
or([not E2NameF(X), E2NameP(X)]), 
or([not E2NameP(X), E2NameF(X)]), 
or([not BOX21F(X), BOX10P(X)]), 
or([not BOX10P(X), BOX21F(X)]), 
or([not E1NameF(X), E1NameP(X)]), 
or([not E1NameP(X), E1NameF(X)]), 
or([not BOX0F(X), BOX1P(X)]), 
or([not BOX1P(X), BOX0F(X)]), 
or([not BOX14F(X), BOX3P(X)]), 
or([not BOX3P(X), BOX14F(X)]), 
or([not BOX20F(X), BOX9P(X)]), 
or([not BOX9P(X), BOX20F(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 BOX16F(X), BOX5P(X)]), 
or([not BOX5P(X), BOX16F(X)]), 
or([not BOX13F(X), BOX2P(X)]), 
or([not BOX2P(X), BOX13F(X)]), 
or([not PinvNameF, PinvNameP]), 
or([not PinvNameP, PinvNameF]), 
or([not BOX17F(X), BOX6P(X)]), 
or([not BOX6P(X), BOX17F(X)]), 
or([not BOX23F(X), BOX12P(X)]), 
or([not BOX12P(X), BOX23F(X)]), 
or([not BOX22F(X), BOX11P(X)]), 
or([not BOX11P(X), BOX22F(X)]), 
or([not BOX19F(X), BOX8P(X)]), 
or([not BOX8P(X), BOX19F(X)]), 
or([not BOX15F(X), BOX4P(X)]), 
or([not BOX4P(X), BOX15F(X)]), 
or([not PNameF, E1NameInvF(constant(dNameInv))]), 
or([not PinvNameF, E1NameF(constant(dName))]), 
or([NVV88]), 
or([NVV154]), 
or([NVV152]), 
or([NVV110]), 
or([NVV106]), 
or([NVV165]), 
or([NVV262]), 
or([NVV316]), 
or([NVV136]), 
or([NVV337]), 
or([NVV294]), 
or([NVV158]), 
or([NVV268]), 
or([NVV302]), 
or([NVV326]), 
or([NVV162]), 
or([NVV324]), 
or([NVV272]), 
or([NVV160]), 
or([NVV345]), 
or([NVV336]), 
or([NVV98]), 
or([NVV90]), 
or([NVV292]), 
or([NVV341]), 
or([NVV347]), 
or([NVV330]), 
or([NVV310]), 
or([NVV355]), 
or([NVV290]), 
or([NVV278]), 
or([PersonF(constant(John))]), 
or([NVV365]), 
or([NVV102]), 
or([NVV94]), 
or([NVV276]), 
or([NVV132]), 
or([NVV134]), 
or([NVV334]), 
or([NVV369]), 
or([NVV124]), 
or([NVV312]), 
or([NVV318]), 
or([NVV359]), 
or([NVV300]), 
or([NVV343]), 
or([NVV274]), 
or([NVV156]), 
or([NVV266]), 
or([NVV138]), 
or([NVV130]), 
or([NVV164]), 
or([NVV104]), 
or([NVV120]), 
or([NVV288]), 
or([NVV322]), 
or([NVV349]), 
or([NVV284]), 
or([NVV304]), 
or([NVV298]), 
or([NVV144]), 
or([NVV308]), 
or([NVV148]), 
or([E1NameInvF(constant(N0))]), 
or([NVV351]), 
or([NVV363]), 
or([NVV353]), 
or([NVV126]), 
or([NVV100]), 
or([NVV96]), 
or([NVV371]), 
or([NVV92]), 
or([E2NameF(constant(John))]), 
or([NVV357]), 
or([NVV306]), 
or([NVV296]), 
or([NVV286]), 
or([NVV116]), 
or([NVV108]), 
or([NVV328]), 
or([NVV270]), 
or([NVV140]), 
or([NVV280]), 
or([NVV128]), 
or([NVV314]), 
or([NVV339]), 
or([NVV118]), 
or([NVV373]), 
or([NVV112]), 
or([NVV146]), 
or([NVV150]), 
or([NVV332]), 
or([NVV367]), 
or([NVV361]), 
or([NVV114]), 
or([NVV264]), 
or([NVV375]), 
or([NVV122]), 
or([NVV320]), 
or([NVV282]), 
or([NVV142]),
always(or([not NVV1(X), not BOX18F(X), NVV2(X)])), 
always(or([not NVV1(X), NVV3(X), BOX18F(X)])), 
always(or([not NVV1(X), not BOX6P(X), NVV5(X)])), 
always(or([not NVV1(X), NVV6(X), BOX6P(X)])), 
always(or([not NVV1(X), NVV8(X), BOX5P(X)])), 
always(or([not NVV1(X), NVV8(X), NVV9(X)])), 
always(or([not NVV1(X), not BOX5P(X), NVV10(X), NVV11(X)])), 
always(or([not NVV1(X), NVV12(X), BOX9P(X)])), 
always(or([not NVV1(X), NVV12(X), NVV13(X)])), 
always(or([not NVV1(X), not BOX9P(X), NVV14(X), NVV15(X)])), 
always(or([not NVV1(X), not BOX16F(X), NVV16(X)])), 
always(or([not NVV1(X), NVV17(X), BOX16F(X)])), 
always(or([not NVV1(X), NVV19(X), BOX21F(X)])), 
always(or([not NVV1(X), NVV19(X), NVV20(X)])), 
always(or([not NVV1(X), not BOX21F(X), NVV21(X), NVV22(X)])), 
always(or([not NVV1(X), not BOX10P(X), NVV23(X)])), 
always(or([not NVV1(X), NVV24(X), BOX10P(X)])), 
always(or([not NVV1(X), NVV26(X), BOX1P(X)])), 
always(or([not NVV1(X), NVV26(X), NVV27(X)])), 
always(or([not NVV1(X), not BOX1P(X), NVV28(X), NVV29(X)])), 
always(or([not NVV1(X), NVV30(X), BOX17F(X)])), 
always(or([not NVV1(X), NVV30(X), NVV31(X)])), 
always(or([not NVV1(X), not BOX17F(X), NVV32(X), NVV33(X)])), 
always(or([not NVV1(X), not BOX12P(X), NVV34])), 
always(or([not NVV1(X), NVV35, BOX12P(X)])), 
always(or([not NVV1(X), not BOX0F(X), NVV37(X)])), 
always(or([not NVV1(X), NVV38(X), BOX0F(X)])), 
always(or([not NVV1(X), NVV40(X), BOX23F(X)])), 
always(or([not NVV1(X), NVV40(X), NVV41])), 
always(or([not NVV1(X), not BOX23F(X), NVV42, NVV43(X)])), 
always(or([not NVV1(X), not BOX2P(X), NVV44(X)])), 
always(or([not NVV1(X), NVV45(X), BOX2P(X)])), 
always(or([not NVV1(X), NVV47(X), BOX11P(X)])), 
always(or([not NVV1(X), NVV47(X), NVV48(X)])), 
always(or([not NVV1(X), not BOX11P(X), NVV49(X), NVV50(X)])), 
always(or([not NVV1(X), not BOX14F(X), NVV51(X)])), 
always(or([not NVV1(X), NVV52(X), BOX14F(X)])), 
always(or([not NVV1(X), not BOX8P(X), NVV54])), 
always(or([not NVV1(X), NVV55, BOX8P(X)])), 
always(or([not NVV1(X), NVV57(X), BOX7P(X)])), 
always(or([not NVV1(X), NVV57(X), NVV58(X)])), 
always(or([not NVV1(X), not BOX7P(X), NVV59(X), NVV60(X)])), 
always(or([not NVV1(X), not BOX22F(X), NVV61(X)])), 
always(or([not NVV1(X), NVV62(X), BOX22F(X)])), 
always(or([not NVV1(X), NVV64(X), BOX19F(X)])), 
always(or([not NVV1(X), NVV64(X), NVV65])), 
always(or([not NVV1(X), not BOX19F(X), NVV66, NVV67(X)])), 
always(or([not NVV1(X), NVV68(X), BOX13F(X)])), 
always(or([not NVV1(X), NVV68(X), NVV69(X)])), 
always(or([not NVV1(X), not BOX13F(X), NVV71(X), NVV73(X)])), 
always(or([not NVV1(X), NVV74(X), BOX3P(X)])), 
always(or([not NVV1(X), NVV74(X), NVV75(X)])), 
always(or([not NVV1(X), not BOX3P(X), NVV76(X), NVV77(X)])), 
always(or([not NVV1(X), not BOX4P(X), NVV78(X)])), 
always(or([not NVV1(X), NVV79(X), BOX4P(X)])), 
always(or([not NVV1(X), NVV81(X), BOX15F(X)])), 
always(or([not NVV1(X), NVV81(X), NVV82(X)])), 
always(or([not NVV1(X), not BOX15F(X), NVV83(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 NVV2(X), BOX19F(X)])), 
always(or([not NVV4(X), not BOX19F(X)])), 
always(or([not NVV5(X), E1NameInvP(X)])), 
always(or([not NVV7(X), not E1NameInvP(X)])), 
always(or([not NVV16(X), BOX17F(X)])), 
always(or([not NVV18(X), not BOX17F(X)])), 
always(or([not NVV23(X), E1NameP(X)])), 
always(or([not NVV25(X), not E1NameP(X)])), 
always(or([not NVV34, PNameP])), 
always(or([not NVV36, not PNameP])), 
always(or([not NVV37(X), BOX13F(X)])), 
always(or([not NVV39(X), not BOX13F(X)])), 
always(or([not NVV44(X), not PersonP(X), not E2NameP(X)])), 
always(or([not NVV44(X), not PersonP(X), E1NameP(X)])), 
always(or([not NVV44(X), not E2NameP(X), BOX3P(X)])), 
always(or([not NVV44(X), not E1NameInvP(X), BOX5P(X)])), 
always(or([not NVV44(X), not E1NameInvP(X), BOX7P(X)])), 
always(or([not NVV44(X), not E2NameP(X), E1NameP(X)])), 
always(or([not NVV44(X), not E1NameP(X), BOX9P(X)])), 
always(or([not NVV44(X), not E1NameP(X), BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), E1NameInvP(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), E1NameInvP(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), E1NameInvP(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), E1NameInvP(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), E1NameInvP(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), E1NameP(X)])), 
always(or([not NVV46(X), PersonP(X), E1NameInvP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), E1NameInvP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), E1NameInvP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), E1NameInvP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), E1NameInvP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), E1NameP(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), not E1NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), E2NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), not BOX5P(X), E1NameInvP(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), E1NameInvP(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), E2NameP(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), PersonP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV46(X), E2NameP(X), not BOX3P(X), not BOX5P(X), not BOX7P(X), not E1NameP(X), not BOX9P(X), not BOX11P(X)])), 
always(or([not NVV51(X), BOX15F(X)])), 
always(or([not NVV53(X), not BOX15F(X)])), 
always(or([not NVV54, PinvNameP])), 
always(or([not NVV56, not PinvNameP])), 
always(or([not NVV61(X), BOX23F(X)])), 
always(or([not NVV63(X), not BOX23F(X)])), 
always(or([not NVV70(X), not PersonF(X), not E2NameF(X)])), 
always(or([not NVV70(X), not PersonF(X), E1NameF(X)])), 
always(or([not NVV70(X), not E2NameF(X), BOX14F(X)])), 
always(or([not NVV70(X), not E1NameInvF(X), BOX16F(X)])), 
always(or([not NVV70(X), not E1NameInvF(X), BOX18F(X)])), 
always(or([not NVV70(X), not E2NameF(X), E1NameF(X)])), 
always(or([not NVV70(X), not E1NameF(X), BOX20F(X)])), 
always(or([not NVV70(X), not E1NameF(X), BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), E1NameInvF(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), E1NameInvF(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), E1NameInvF(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), E1NameInvF(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), E1NameInvF(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), E1NameF(X)])), 
always(or([not NVV72(X), PersonF(X), E1NameInvF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), E1NameInvF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), E1NameInvF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), E1NameInvF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), E1NameInvF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), E1NameF(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), not E1NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), E2NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), not BOX16F(X), E1NameInvF(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), E1NameInvF(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), E2NameF(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), PersonF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV72(X), E2NameF(X), not BOX14F(X), not BOX16F(X), not BOX18F(X), not E1NameF(X), not BOX20F(X), not BOX22F(X)])), 
always(or([not NVV78(X), E2NameP(X)])), 
always(or([not NVV80(X), not E2NameP(X)])), 
always(or([not NVV85(X), BOX21F(X)])), 
always(or([not NVV87(X), not BOX21F(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 NVV157, NVV158])), 
always(or([not NVV159, NVV160])), 
always(or([not NVV161, NVV162])), 
always(or([not NVV163, NVV164])), 
always(or([not NVV166, NVV167])), 
always(or([not NVV168, NVV169])), 
always(or([not NVV170, NVV171])), 
always(or([not NVV172, NVV173])), 
always(or([not NVV174, NVV175])), 
always(or([not NVV176, NVV177])), 
always(or([not NVV178, NVV179])), 
always(or([not NVV180, NVV181])), 
always(or([not NVV182, NVV183])), 
always(or([not NVV184, NVV185])), 
always(or([not NVV186, NVV187])), 
always(or([not NVV188, NVV189])), 
always(or([not NVV190, NVV191])), 
always(or([not NVV192, NVV193])), 
always(or([not NVV194, NVV195])), 
always(or([not NVV196, NVV197])), 
always(or([not NVV198, NVV199])), 
always(or([not NVV200, NVV201])), 
always(or([not NVV202, NVV203])), 
always(or([not NVV204, NVV205])), 
always(or([not NVV206, NVV207])), 
always(or([not NVV208, NVV209])), 
always(or([not NVV210, NVV211])), 
always(or([not NVV212, NVV213])), 
always(or([not NVV214, NVV215])), 
always(or([not NVV216, NVV217])), 
always(or([not NVV218, NVV219])), 
always(or([not NVV220, NVV221])), 
always(or([not NVV222, NVV223])), 
always(or([not NVV224, NVV225])), 
always(or([not NVV226, NVV227])), 
always(or([not NVV228, NVV229])), 
always(or([not NVV230, NVV231])), 
always(or([not NVV232, NVV233])), 
always(or([not NVV234, NVV235])), 
always(or([not NVV236, NVV237])), 
always(or([not NVV238, NVV239])), 
always(or([not NVV240, NVV241])), 
always(or([not NVV242, NVV243])), 
always(or([not NVV244, NVV245])), 
always(or([not NVV246, NVV247])), 
always(or([not NVV248, NVV249])), 
always(or([not NVV250, NVV251])), 
always(or([not NVV252, NVV253])), 
always(or([not NVV254, NVV255])), 
always(or([not NVV256, NVV257])), 
always(or([not NVV258, NVV259])), 
always(or([not NVV260, NVV261])), 
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 NVV317, NVV318])), 
always(or([not NVV319, NVV320])), 
always(or([not NVV321, NVV322])), 
always(or([not NVV323, NVV324])), 
always(or([not NVV325, NVV326])), 
always(or([not NVV327, NVV328])), 
always(or([not NVV329, NVV330])), 
always(or([not NVV331, NVV332])), 
always(or([not NVV333, NVV334])), 
always(or([not NVV335, NVV336])), 
always(or([not NVV338, NVV339])), 
always(or([not NVV340, NVV341])), 
always(or([not NVV342, NVV343])), 
always(or([not NVV344, NVV262])), 
always(or([not NVV346, NVV88])), 
always(or([not NVV348, NVV349])), 
always(or([not NVV350, NVV351])), 
always(or([not NVV352, NVV353])), 
always(or([not NVV354, NVV337])), 
always(or([not NVV356, NVV357])), 
always(or([not NVV358, NVV359])), 
always(or([not NVV360, NVV361])), 
always(or([not NVV362, NVV363])), 
always(or([not NVV364, NVV345])), 
always(or([not NVV366, NVV367])), 
always(or([not NVV368, NVV347])), 
always(or([not NVV370, NVV365])), 
always(or([not NVV372, NVV355])), 
always(or([not NVV374, NVV371])), 
always(or([not NVV376, NVV373])),
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(NVV2(hidden(X)))])), 
always(or([not NVV2(constant(X)), next(NVV2(constant(X)))])), 
always(or([not NVV5(X), next(NVV5(hidden(X)))])), 
always(or([not NVV5(constant(X)), next(NVV5(constant(X)))])), 
always(or([not NVV8(X), next(not BOX5P(hidden(X)))])), 
always(or([not NVV8(constant(X)), next(not BOX5P(constant(X)))])), 
always(or([not NVV9(X), next(BOX6P(hidden(X)))])), 
always(or([not NVV9(constant(X)), next(BOX6P(constant(X)))])), 
always(or([not NVV10(X), next(not BOX6P(hidden(X)))])), 
always(or([not NVV10(constant(X)), next(not BOX6P(constant(X)))])), 
always(or([not NVV11(X), next(BOX5P(hidden(X)))])), 
always(or([not NVV11(constant(X)), next(BOX5P(constant(X)))])), 
always(or([not NVV12(X), next(not BOX9P(hidden(X)))])), 
always(or([not NVV12(constant(X)), next(not BOX9P(constant(X)))])), 
always(or([not NVV13(X), next(BOX10P(hidden(X)))])), 
always(or([not NVV13(constant(X)), next(BOX10P(constant(X)))])), 
always(or([not NVV14(X), next(not BOX10P(hidden(X)))])), 
always(or([not NVV14(constant(X)), next(not BOX10P(constant(X)))])), 
always(or([not NVV15(X), next(BOX9P(hidden(X)))])), 
always(or([not NVV15(constant(X)), next(BOX9P(constant(X)))])), 
always(or([not NVV16(X), next(NVV16(hidden(X)))])), 
always(or([not NVV16(constant(X)), next(NVV16(constant(X)))])), 
always(or([not NVV19(X), next(not BOX21F(hidden(X)))])), 
always(or([not NVV19(constant(X)), next(not BOX21F(constant(X)))])), 
always(or([not NVV20(X), next(E1NameF(hidden(X)))])), 
always(or([not NVV20(constant(X)), next(E1NameF(constant(X)))])), 
always(or([not NVV21(X), next(not E1NameF(hidden(X)))])), 
always(or([not NVV21(constant(X)), next(not E1NameF(constant(X)))])), 
always(or([not NVV22(X), next(BOX21F(hidden(X)))])), 
always(or([not NVV22(constant(X)), next(BOX21F(constant(X)))])), 
always(or([not NVV23(X), next(NVV23(hidden(X)))])), 
always(or([not NVV23(constant(X)), next(NVV23(constant(X)))])), 
always(or([not NVV26(X), next(not BOX1P(hidden(X)))])), 
always(or([not NVV26(constant(X)), next(not BOX1P(constant(X)))])), 
always(or([not NVV27(X), next(BOX2P(hidden(X)))])), 
always(or([not NVV27(constant(X)), next(BOX2P(constant(X)))])), 
always(or([not NVV28(X), next(not BOX2P(hidden(X)))])), 
always(or([not NVV28(constant(X)), next(not BOX2P(constant(X)))])), 
always(or([not NVV29(X), next(BOX1P(hidden(X)))])), 
always(or([not NVV29(constant(X)), next(BOX1P(constant(X)))])), 
always(or([not NVV30(X), next(not BOX17F(hidden(X)))])), 
always(or([not NVV30(constant(X)), next(not BOX17F(constant(X)))])), 
always(or([not NVV31(X), next(E1NameInvF(hidden(X)))])), 
always(or([not NVV31(constant(X)), next(E1NameInvF(constant(X)))])), 
always(or([not NVV32(X), next(not E1NameInvF(hidden(X)))])), 
always(or([not NVV32(constant(X)), next(not E1NameInvF(constant(X)))])), 
always(or([not NVV33(X), next(BOX17F(hidden(X)))])), 
always(or([not NVV33(constant(X)), next(BOX17F(constant(X)))])), 
always(or([not NVV34, next(NVV34)])), 
always(or([not NVV37(X), next(NVV37(hidden(X)))])), 
always(or([not NVV37(constant(X)), next(NVV37(constant(X)))])), 
always(or([not NVV40(X), next(not BOX23F(hidden(X)))])), 
always(or([not NVV40(constant(X)), next(not BOX23F(constant(X)))])), 
always(or([not NVV41, next(PNameF)])), 
always(or([not NVV42, next(not PNameF)])), 
always(or([not NVV43(X), next(BOX23F(hidden(X)))])), 
always(or([not NVV43(constant(X)), next(BOX23F(constant(X)))])), 
always(or([not NVV44(X), next(NVV44(hidden(X)))])), 
always(or([not NVV44(constant(X)), next(NVV44(constant(X)))])), 
always(or([not NVV47(X), next(not BOX11P(hidden(X)))])), 
always(or([not NVV47(constant(X)), next(not BOX11P(constant(X)))])), 
always(or([not NVV48(X), next(BOX12P(hidden(X)))])), 
always(or([not NVV48(constant(X)), next(BOX12P(constant(X)))])), 
always(or([not NVV49(X), next(not BOX12P(hidden(X)))])), 
always(or([not NVV49(constant(X)), next(not BOX12P(constant(X)))])), 
always(or([not NVV50(X), next(BOX11P(hidden(X)))])), 
always(or([not NVV50(constant(X)), next(BOX11P(constant(X)))])), 
always(or([not NVV51(X), next(NVV51(hidden(X)))])), 
always(or([not NVV51(constant(X)), next(NVV51(constant(X)))])), 
always(or([not NVV54, next(NVV54)])), 
always(or([not NVV57(X), next(not BOX7P(hidden(X)))])), 
always(or([not NVV57(constant(X)), next(not BOX7P(constant(X)))])), 
always(or([not NVV58(X), next(BOX8P(hidden(X)))])), 
always(or([not NVV58(constant(X)), next(BOX8P(constant(X)))])), 
always(or([not NVV59(X), next(not BOX8P(hidden(X)))])), 
always(or([not NVV59(constant(X)), next(not BOX8P(constant(X)))])), 
always(or([not NVV60(X), next(BOX7P(hidden(X)))])), 
always(or([not NVV60(constant(X)), next(BOX7P(constant(X)))])), 
always(or([not NVV61(X), next(NVV61(hidden(X)))])), 
always(or([not NVV61(constant(X)), next(NVV61(constant(X)))])), 
always(or([not NVV64(X), next(not BOX19F(hidden(X)))])), 
always(or([not NVV64(constant(X)), next(not BOX19F(constant(X)))])), 
always(or([not NVV65, next(PinvNameF)])), 
always(or([not NVV66, next(not PinvNameF)])), 
always(or([not NVV67(X), next(BOX19F(hidden(X)))])), 
always(or([not NVV67(constant(X)), next(BOX19F(constant(X)))])), 
always(or([not NVV68(X), next(not BOX13F(hidden(X)))])), 
always(or([not NVV68(constant(X)), next(not BOX13F(constant(X)))])), 
always(or([not NVV69(X), next(NVV70(hidden(X)))])), 
always(or([not NVV69(constant(X)), next(NVV70(constant(X)))])), 
always(or([not NVV71(X), next(NVV72(hidden(X)))])), 
always(or([not NVV71(constant(X)), next(NVV72(constant(X)))])), 
always(or([not NVV73(X), next(BOX13F(hidden(X)))])), 
always(or([not NVV73(constant(X)), next(BOX13F(constant(X)))])), 
always(or([not NVV74(X), next(not BOX3P(hidden(X)))])), 
always(or([not NVV74(constant(X)), next(not BOX3P(constant(X)))])), 
always(or([not NVV75(X), next(BOX4P(hidden(X)))])), 
always(or([not NVV75(constant(X)), next(BOX4P(constant(X)))])), 
always(or([not NVV76(X), next(not BOX4P(hidden(X)))])), 
always(or([not NVV76(constant(X)), next(not BOX4P(constant(X)))])), 
always(or([not NVV77(X), next(BOX3P(hidden(X)))])), 
always(or([not NVV77(constant(X)), next(BOX3P(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 BOX15F(hidden(X)))])), 
always(or([not NVV81(constant(X)), next(not BOX15F(constant(X)))])), 
always(or([not NVV82(X), next(E2NameF(hidden(X)))])), 
always(or([not NVV82(constant(X)), next(E2NameF(constant(X)))])), 
always(or([not NVV83(X), next(not E2NameF(hidden(X)))])), 
always(or([not NVV83(constant(X)), next(not E2NameF(constant(X)))])), 
always(or([not NVV84(X), next(BOX15F(hidden(X)))])), 
always(or([not NVV84(constant(X)), next(BOX15F(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(NVV157)])), 
always(or([not NVV158, next(NVV159)])), 
always(or([not NVV160, next(NVV161)])), 
always(or([not NVV162, next(NVV163)])), 
always(or([not NVV164, next(E1NameInvF(N0))])), 
always(or([not NVV165, next(NVV166)])), 
always(or([not NVV167, next(NVV168)])), 
always(or([not NVV169, next(NVV170)])), 
always(or([not NVV171, next(NVV172)])), 
always(or([not NVV173, next(NVV174)])), 
always(or([not NVV175, next(NVV176)])), 
always(or([not NVV177, next(NVV178)])), 
always(or([not NVV179, next(NVV180)])), 
always(or([not NVV181, next(NVV182)])), 
always(or([not NVV183, next(NVV184)])), 
always(or([not NVV185, next(NVV186)])), 
always(or([not NVV187, next(NVV188)])), 
always(or([not NVV189, next(NVV190)])), 
always(or([not NVV191, next(NVV192)])), 
always(or([not NVV193, next(NVV194)])), 
always(or([not NVV195, next(NVV196)])), 
always(or([not NVV197, next(NVV198)])), 
always(or([not NVV199, next(NVV200)])), 
always(or([not NVV201, next(NVV202)])), 
always(or([not NVV203, next(NVV204)])), 
always(or([not NVV205, next(NVV206)])), 
always(or([not NVV207, next(NVV208)])), 
always(or([not NVV209, next(NVV210)])), 
always(or([not NVV211, next(NVV212)])), 
always(or([not NVV213, next(NVV214)])), 
always(or([not NVV215, next(NVV216)])), 
always(or([not NVV217, next(NVV218)])), 
always(or([not NVV219, next(NVV220)])), 
always(or([not NVV221, next(NVV222)])), 
always(or([not NVV223, next(NVV224)])), 
always(or([not NVV225, next(NVV226)])), 
always(or([not NVV227, next(NVV228)])), 
always(or([not NVV229, next(NVV230)])), 
always(or([not NVV231, next(NVV232)])), 
always(or([not NVV233, next(NVV234)])), 
always(or([not NVV235, next(NVV236)])), 
always(or([not NVV237, next(NVV238)])), 
always(or([not NVV239, next(NVV240)])), 
always(or([not NVV241, next(NVV242)])), 
always(or([not NVV243, next(NVV244)])), 
always(or([not NVV245, next(NVV246)])), 
always(or([not NVV247, next(NVV248)])), 
always(or([not NVV249, next(NVV250)])), 
always(or([not NVV251, next(NVV252)])), 
always(or([not NVV253, next(NVV254)])), 
always(or([not NVV255, next(NVV256)])), 
always(or([not NVV257, next(NVV258)])), 
always(or([not NVV259, next(NVV260)])), 
always(or([not NVV261, next(E1NameInvF(N1))])), 
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(NVV317)])), 
always(or([not NVV318, next(NVV319)])), 
always(or([not NVV320, next(NVV321)])), 
always(or([not NVV322, next(NVV323)])), 
always(or([not NVV324, next(NVV325)])), 
always(or([not NVV326, next(NVV327)])), 
always(or([not NVV328, next(NVV329)])), 
always(or([not NVV330, next(NVV331)])), 
always(or([not NVV332, next(NVV333)])), 
always(or([not NVV334, next(NVV335)])), 
always(or([not NVV336, next(E2NameF(John))])), 
always(or([not NVV337, next(NVV338)])), 
always(or([not NVV339, next(NVV340)])), 
always(or([not NVV341, next(NVV342)])), 
always(or([not NVV343, next(NVV344)])), 
always(or([not NVV345, next(NVV346)])), 
always(or([not NVV347, next(NVV348)])), 
always(or([not NVV349, next(NVV350)])), 
always(or([not NVV351, next(NVV352)])), 
always(or([not NVV353, next(NVV354)])), 
always(or([not NVV355, next(NVV356)])), 
always(or([not NVV357, next(NVV358)])), 
always(or([not NVV359, next(NVV360)])), 
always(or([not NVV361, next(NVV362)])), 
always(or([not NVV363, next(NVV364)])), 
always(or([not NVV365, next(NVV366)])), 
always(or([not NVV367, next(NVV368)])), 
always(or([not NVV369, next(NVV370)])), 
always(or([not NVV371, next(NVV372)])), 
always(or([not NVV373, next(NVV374)])), 
always(or([not NVV375, next(NVV376)])),
always(or([not NVV3(X), sometime(NVV4(X))])), 
always(or([not NVV3(constant(dNameInv)), sometime(NVV4(constant(dNameInv)))])), 
always(or([not NVV3(constant(dName)), sometime(NVV4(constant(dName)))])), 
always(or([not NVV3(constant(N1)), sometime(NVV4(constant(N1)))])), 
always(or([not NVV3(constant(John)), sometime(NVV4(constant(John)))])), 
always(or([not NVV3(constant(N0)), sometime(NVV4(constant(N0)))])), 
always(or([not NVV6(X), sometime(NVV7(X))])), 
always(or([not NVV6(constant(dNameInv)), sometime(NVV7(constant(dNameInv)))])), 
always(or([not NVV6(constant(dName)), sometime(NVV7(constant(dName)))])), 
always(or([not NVV6(constant(N1)), sometime(NVV7(constant(N1)))])), 
always(or([not NVV6(constant(John)), sometime(NVV7(constant(John)))])), 
always(or([not NVV6(constant(N0)), sometime(NVV7(constant(N0)))])), 
always(or([not NVV17(X), sometime(NVV18(X))])), 
always(or([not NVV17(constant(dNameInv)), sometime(NVV18(constant(dNameInv)))])), 
always(or([not NVV17(constant(dName)), sometime(NVV18(constant(dName)))])), 
always(or([not NVV17(constant(N1)), sometime(NVV18(constant(N1)))])), 
always(or([not NVV17(constant(John)), sometime(NVV18(constant(John)))])), 
always(or([not NVV17(constant(N0)), sometime(NVV18(constant(N0)))])), 
always(or([not NVV24(X), sometime(NVV25(X))])), 
always(or([not NVV24(constant(dNameInv)), sometime(NVV25(constant(dNameInv)))])), 
always(or([not NVV24(constant(dName)), sometime(NVV25(constant(dName)))])), 
always(or([not NVV24(constant(N1)), sometime(NVV25(constant(N1)))])), 
always(or([not NVV24(constant(John)), sometime(NVV25(constant(John)))])), 
always(or([not NVV24(constant(N0)), sometime(NVV25(constant(N0)))])), 
always(or([not NVV35, sometime(NVV36)])), 
always(or([not NVV38(X), sometime(NVV39(X))])), 
always(or([not NVV38(constant(dNameInv)), sometime(NVV39(constant(dNameInv)))])), 
always(or([not NVV38(constant(dName)), sometime(NVV39(constant(dName)))])), 
always(or([not NVV38(constant(N1)), sometime(NVV39(constant(N1)))])), 
always(or([not NVV38(constant(John)), sometime(NVV39(constant(John)))])), 
always(or([not NVV38(constant(N0)), sometime(NVV39(constant(N0)))])), 
always(or([not NVV45(X), sometime(NVV46(X))])), 
always(or([not NVV45(constant(dNameInv)), sometime(NVV46(constant(dNameInv)))])), 
always(or([not NVV45(constant(dName)), sometime(NVV46(constant(dName)))])), 
always(or([not NVV45(constant(N1)), sometime(NVV46(constant(N1)))])), 
always(or([not NVV45(constant(John)), sometime(NVV46(constant(John)))])), 
always(or([not NVV45(constant(N0)), sometime(NVV46(constant(N0)))])), 
always(or([not NVV52(X), sometime(NVV53(X))])), 
always(or([not NVV52(constant(dNameInv)), sometime(NVV53(constant(dNameInv)))])), 
always(or([not NVV52(constant(dName)), sometime(NVV53(constant(dName)))])), 
always(or([not NVV52(constant(N1)), sometime(NVV53(constant(N1)))])), 
always(or([not NVV52(constant(John)), sometime(NVV53(constant(John)))])), 
always(or([not NVV52(constant(N0)), sometime(NVV53(constant(N0)))])), 
always(or([not NVV55, sometime(NVV56)])), 
always(or([not NVV62(X), sometime(NVV63(X))])), 
always(or([not NVV62(constant(dNameInv)), sometime(NVV63(constant(dNameInv)))])), 
always(or([not NVV62(constant(dName)), sometime(NVV63(constant(dName)))])), 
always(or([not NVV62(constant(N1)), sometime(NVV63(constant(N1)))])), 
always(or([not NVV62(constant(John)), sometime(NVV63(constant(John)))])), 
always(or([not NVV62(constant(N0)), sometime(NVV63(constant(N0)))])), 
always(or([not NVV79(X), sometime(NVV80(X))])), 
always(or([not NVV79(constant(dNameInv)), sometime(NVV80(constant(dNameInv)))])), 
always(or([not NVV79(constant(dName)), sometime(NVV80(constant(dName)))])), 
always(or([not NVV79(constant(N1)), sometime(NVV80(constant(N1)))])), 
always(or([not NVV79(constant(John)), sometime(NVV80(constant(John)))])), 
always(or([not NVV79(constant(N0)), sometime(NVV80(constant(N0)))])), 
always(or([not NVV86(X), sometime(NVV87(X))])), 
always(or([not NVV86(constant(dNameInv)), sometime(NVV87(constant(dNameInv)))])), 
always(or([not NVV86(constant(dName)), sometime(NVV87(constant(dName)))])), 
always(or([not NVV86(constant(N1)), sometime(NVV87(constant(N1)))])), 
always(or([not NVV86(constant(John)), sometime(NVV87(constant(John)))])), 
always(or([not NVV86(constant(N0)), sometime(NVV87(constant(N0)))]))]).

