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

