and([
or([BOX0F(X)]), 
or([NVV1(X)]), 
or([not AdultF(X), AdultP(X)]), 
or([not AdultP(X), AdultF(X)]), 
or([not BOX4F(X), BOX2P(X)]), 
or([not BOX2P(X), BOX4F(X)]), 
or([not PersonF(X), PersonP(X)]), 
or([not PersonP(X), PersonF(X)]), 
or([not MinorF(X), MinorP(X)]), 
or([not MinorP(X), MinorF(X)]), 
or([not BOX0F(X), BOX1P(X)]), 
or([not BOX1P(X), BOX0F(X)]), 
or([not BOX5F(X), BOX3P(X)]), 
or([not BOX3P(X), BOX5F(X)]), 
or([NVV25]), 
or([NVV44]), 
or([NVV48]), 
or([NVV76]), 
or([NVV113]), 
or([NVV145]), 
or([NVV33]), 
or([NVV125]), 
or([NVV112]), 
or([NVV108]), 
or([NVV52]), 
or([NVV72]), 
or([NVV161]), 
or([NVV92]), 
or([NVV177]), 
or([NVV117]), 
or([NVV121]), 
or([NVV165]), 
or([NVV153]), 
or([NVV37]), 
or([NVV137]), 
or([NVV149]), 
or([NVV183]), 
or([NVV88]), 
or([NVV187]), 
or([NVV104]), 
or([NVV203]), 
or([NVV157]), 
or([NVV211]), 
or([NVV173]), 
or([NVV133]), 
or([NVV129]), 
or([NVV29]), 
or([NVV84]), 
or([NVV68]), 
or([NVV191]), 
or([NVV60]), 
or([NVV100]), 
or([MinorF(constant(John))]), 
or([NVV96]), 
or([NVV169]), 
or([NVV213]), 
or([NVV64]), 
or([NVV80]), 
or([NVV199]), 
or([NVV195]), 
or([NVV207]), 
or([NVV41]), 
or([NVV56]), 
or([NVV141]),
always(or([not NVV1(X), not BOX0F(X), NVV2(X)])), 
always(or([not NVV1(X), NVV3(X), BOX0F(X)])), 
always(or([not NVV1(X), NVV5(X), BOX1P(X)])), 
always(or([not NVV1(X), NVV5(X), NVV6(X)])), 
always(or([not NVV1(X), not BOX1P(X), NVV7(X), NVV8(X)])), 
always(or([not NVV1(X), NVV9(X), BOX4F(X)])), 
always(or([not NVV1(X), NVV9(X), NVV10(X)])), 
always(or([not NVV1(X), not BOX4F(X), NVV12(X), NVV14(X)])), 
always(or([not NVV1(X), not BOX2P(X), NVV15(X)])), 
always(or([not NVV1(X), NVV16(X), BOX2P(X)])), 
always(or([not NVV1(X), not BOX5F(X), NVV18(X)])), 
always(or([not NVV1(X), NVV19(X), BOX5F(X)])), 
always(or([not NVV1(X), NVV21(X), BOX3P(X)])), 
always(or([not NVV1(X), NVV21(X), NVV22(X)])), 
always(or([not NVV1(X), not BOX3P(X), NVV23(X), NVV24(X)])), 
always(or([not NVV2(X), BOX4F(X)])), 
always(or([not NVV4(X), not BOX4F(X)])), 
always(or([not NVV11(X), not AdultF(X), PersonF(X)])), 
always(or([not NVV11(X), not AdultF(X), BOX5F(X)])), 
always(or([not NVV11(X), not MinorF(X), PersonF(X)])), 
always(or([not NVV11(X), not MinorF(X), not AdultF(X)])), 
always(or([not NVV13(X), AdultF(X), MinorF(X)])), 
always(or([not NVV13(X), not PersonF(X), AdultF(X), MinorF(X)])), 
always(or([not NVV13(X), AdultF(X), not BOX5F(X), MinorF(X)])), 
always(or([not NVV13(X), not PersonF(X), not BOX5F(X), MinorF(X)])), 
always(or([not NVV13(X), AdultF(X), not PersonF(X), MinorF(X)])), 
always(or([not NVV13(X), AdultF(X), not BOX5F(X), not PersonF(X), MinorF(X)])), 
always(or([not NVV13(X), not BOX5F(X), not PersonF(X), MinorF(X)])), 
always(or([not NVV13(X), MinorF(X), AdultF(X)])), 
always(or([not NVV13(X), not PersonF(X), MinorF(X), AdultF(X)])), 
always(or([not NVV13(X), not BOX5F(X), MinorF(X), AdultF(X)])), 
always(or([not NVV13(X), not PersonF(X), not BOX5F(X), MinorF(X), AdultF(X)])), 
always(or([not NVV13(X), not PersonF(X), AdultF(X)])), 
always(or([not NVV13(X), not BOX5F(X), not PersonF(X), AdultF(X)])), 
always(or([not NVV15(X), not AdultP(X), PersonP(X)])), 
always(or([not NVV15(X), not AdultP(X), BOX3P(X)])), 
always(or([not NVV15(X), not MinorP(X), PersonP(X)])), 
always(or([not NVV15(X), not MinorP(X), not AdultP(X)])), 
always(or([not NVV17(X), AdultP(X), MinorP(X)])), 
always(or([not NVV17(X), not PersonP(X), AdultP(X), MinorP(X)])), 
always(or([not NVV17(X), AdultP(X), not BOX3P(X), MinorP(X)])), 
always(or([not NVV17(X), not PersonP(X), not BOX3P(X), MinorP(X)])), 
always(or([not NVV17(X), AdultP(X), not PersonP(X), MinorP(X)])), 
always(or([not NVV17(X), AdultP(X), not BOX3P(X), not PersonP(X), MinorP(X)])), 
always(or([not NVV17(X), not BOX3P(X), not PersonP(X), MinorP(X)])), 
always(or([not NVV17(X), MinorP(X), AdultP(X)])), 
always(or([not NVV17(X), not PersonP(X), MinorP(X), AdultP(X)])), 
always(or([not NVV17(X), not BOX3P(X), MinorP(X), AdultP(X)])), 
always(or([not NVV17(X), not PersonP(X), not BOX3P(X), MinorP(X), AdultP(X)])), 
always(or([not NVV17(X), not PersonP(X), AdultP(X)])), 
always(or([not NVV17(X), not BOX3P(X), not PersonP(X), AdultP(X)])), 
always(or([not NVV18(X), AdultF(X)])), 
always(or([not NVV20(X), not AdultF(X)])), 
always(or([not NVV26, NVV27])), 
always(or([not NVV28, NVV29])), 
always(or([not NVV30, NVV31])), 
always(or([not NVV32, NVV33])), 
always(or([not NVV34, NVV35])), 
always(or([not NVV36, NVV37])), 
always(or([not NVV38, NVV39])), 
always(or([not NVV40, NVV41])), 
always(or([not NVV42, NVV43])), 
always(or([not NVV45, NVV46])), 
always(or([not NVV47, NVV48])), 
always(or([not NVV49, NVV50])), 
always(or([not NVV51, NVV52])), 
always(or([not NVV53, NVV54])), 
always(or([not NVV55, NVV56])), 
always(or([not NVV57, NVV58])), 
always(or([not NVV59, NVV60])), 
always(or([not NVV61, NVV62])), 
always(or([not NVV63, NVV64])), 
always(or([not NVV65, NVV66])), 
always(or([not NVV67, NVV68])), 
always(or([not NVV69, NVV70])), 
always(or([not NVV71, NVV72])), 
always(or([not NVV73, NVV74])), 
always(or([not NVV75, NVV25])), 
always(or([not NVV77, NVV78])), 
always(or([not NVV79, NVV80])), 
always(or([not NVV81, NVV82])), 
always(or([not NVV83, NVV84])), 
always(or([not NVV85, NVV86])), 
always(or([not NVV87, NVV88])), 
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 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, NVV141])), 
always(or([not NVV142, NVV143])), 
always(or([not NVV144, NVV44])), 
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, NVV76])), 
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, NVV145])), 
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, NVV161])), 
always(or([not NVV204, NVV205])), 
always(or([not NVV206, NVV207])), 
always(or([not NVV208, NVV209])), 
always(or([not NVV210, NVV113])), 
always(or([not NVV212, NVV203])), 
always(or([not NVV214, NVV215])), 
always(or([not NVV216, NVV211])),
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 BOX1P(hidden(X)))])), 
always(or([not NVV5(constant(X)), next(not BOX1P(constant(X)))])), 
always(or([not NVV6(X), next(BOX2P(hidden(X)))])), 
always(or([not NVV6(constant(X)), next(BOX2P(constant(X)))])), 
always(or([not NVV7(X), next(not BOX2P(hidden(X)))])), 
always(or([not NVV7(constant(X)), next(not BOX2P(constant(X)))])), 
always(or([not NVV8(X), next(BOX1P(hidden(X)))])), 
always(or([not NVV8(constant(X)), next(BOX1P(constant(X)))])), 
always(or([not NVV9(X), next(not BOX4F(hidden(X)))])), 
always(or([not NVV9(constant(X)), next(not BOX4F(constant(X)))])), 
always(or([not NVV10(X), next(NVV11(hidden(X)))])), 
always(or([not NVV10(constant(X)), next(NVV11(constant(X)))])), 
always(or([not NVV12(X), next(NVV13(hidden(X)))])), 
always(or([not NVV12(constant(X)), next(NVV13(constant(X)))])), 
always(or([not NVV14(X), next(BOX4F(hidden(X)))])), 
always(or([not NVV14(constant(X)), next(BOX4F(constant(X)))])), 
always(or([not NVV15(X), next(NVV15(hidden(X)))])), 
always(or([not NVV15(constant(X)), next(NVV15(constant(X)))])), 
always(or([not NVV18(X), next(NVV18(hidden(X)))])), 
always(or([not NVV18(constant(X)), next(NVV18(constant(X)))])), 
always(or([not NVV21(X), next(not BOX3P(hidden(X)))])), 
always(or([not NVV21(constant(X)), next(not BOX3P(constant(X)))])), 
always(or([not NVV22(X), next(AdultP(hidden(X)))])), 
always(or([not NVV22(constant(X)), next(AdultP(constant(X)))])), 
always(or([not NVV23(X), next(not AdultP(hidden(X)))])), 
always(or([not NVV23(constant(X)), next(not AdultP(constant(X)))])), 
always(or([not NVV24(X), next(BOX3P(hidden(X)))])), 
always(or([not NVV24(constant(X)), next(BOX3P(constant(X)))])), 
always(or([not NVV25, next(NVV26)])), 
always(or([not NVV27, next(NVV28)])), 
always(or([not NVV29, next(NVV30)])), 
always(or([not NVV31, next(NVV32)])), 
always(or([not NVV33, next(NVV34)])), 
always(or([not NVV35, next(NVV36)])), 
always(or([not NVV37, next(NVV38)])), 
always(or([not NVV39, next(NVV40)])), 
always(or([not NVV41, next(NVV42)])), 
always(or([not NVV43, next(MinorF(John))])), 
always(or([not NVV44, next(NVV45)])), 
always(or([not NVV46, next(NVV47)])), 
always(or([not NVV48, next(NVV49)])), 
always(or([not NVV50, next(NVV51)])), 
always(or([not NVV52, next(NVV53)])), 
always(or([not NVV54, next(NVV55)])), 
always(or([not NVV56, next(NVV57)])), 
always(or([not NVV58, next(NVV59)])), 
always(or([not NVV60, next(NVV61)])), 
always(or([not NVV62, next(NVV63)])), 
always(or([not NVV64, next(NVV65)])), 
always(or([not NVV66, next(NVV67)])), 
always(or([not NVV68, next(NVV69)])), 
always(or([not NVV70, next(NVV71)])), 
always(or([not NVV72, next(NVV73)])), 
always(or([not NVV74, next(NVV75)])), 
always(or([not NVV76, next(NVV77)])), 
always(or([not NVV78, next(NVV79)])), 
always(or([not NVV80, next(NVV81)])), 
always(or([not NVV82, next(NVV83)])), 
always(or([not NVV84, next(NVV85)])), 
always(or([not NVV86, next(NVV87)])), 
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(AdultF(John))])), 
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(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 NVV3(X), sometime(NVV4(X))])), 
always(or([not NVV3(constant(John)), sometime(NVV4(constant(John)))])), 
always(or([not NVV16(X), sometime(NVV17(X))])), 
always(or([not NVV16(constant(John)), sometime(NVV17(constant(John)))])), 
always(or([not NVV19(X), sometime(NVV20(X))])), 
always(or([not NVV19(constant(John)), sometime(NVV20(constant(John)))]))]).

