and([
or([BOX0F(X)]), 
or([NVV1(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 BOX4F(X), BOX2P(X)]), 
or([not BOX2P(X), BOX4F(X)]), 
or([not AdultF(X), AdultP(X)]), 
or([not AdultP(X), AdultF(X)]), 
or([not BOX5F(X), BOX3P(X)]), 
or([not BOX3P(X), BOX5F(X)]), 
or([not PersonF(X), PersonP(X)]), 
or([not PersonP(X), PersonF(X)]), 
or([NVV25]), 
or([NVV53]), 
or([NVV80]), 
or([NVV85]), 
or([NVV33]), 
or([NVV93]), 
or([NVV49]), 
or([NVV145]), 
or([NVV149]), 
or([NVV65]), 
or([NVV37]), 
or([NVV137]), 
or([NVV157]), 
or([NVV89]), 
or([NVV133]), 
or([NVV165]), 
or([NVV73]), 
or([NVV61]), 
or([MinorF(constant(John))]), 
or([NVV117]), 
or([NVV161]), 
or([NVV29]), 
or([NVV69]), 
or([NVV129]), 
or([NVV57]), 
or([NVV45]), 
or([NVV153]), 
or([NVV109]), 
or([NVV141]), 
or([NVV101]), 
or([NVV97]), 
or([NVV169]), 
or([NVV77]), 
or([NVV173]), 
or([NVV41]), 
or([NVV125]), 
or([NVV113]), 
or([NVV84]), 
or([NVV105]), 
or([NVV121]),
always(or([not NVV1(X), NVV2(X), BOX4F(X)])), 
always(or([not NVV1(X), NVV2(X), NVV3(X)])), 
always(or([not NVV1(X), not BOX4F(X), NVV5(X), NVV7(X)])), 
always(or([not NVV1(X), NVV8(X), BOX1P(X)])), 
always(or([not NVV1(X), NVV8(X), NVV9(X)])), 
always(or([not NVV1(X), not BOX1P(X), NVV10(X), NVV11(X)])), 
always(or([not NVV1(X), NVV12(X), BOX3P(X)])), 
always(or([not NVV1(X), NVV12(X), NVV13(X)])), 
always(or([not NVV1(X), not BOX3P(X), NVV14(X), NVV15(X)])), 
always(or([not NVV1(X), not BOX0F(X), NVV16(X)])), 
always(or([not NVV1(X), NVV17(X), BOX0F(X)])), 
always(or([not NVV1(X), not BOX5F(X), NVV19(X)])), 
always(or([not NVV1(X), NVV20(X), BOX5F(X)])), 
always(or([not NVV1(X), not BOX2P(X), NVV22(X)])), 
always(or([not NVV1(X), NVV23(X), BOX2P(X)])), 
always(or([not NVV4(X), not AdultF(X), BOX5F(X)])), 
always(or([not NVV4(X), not MinorF(X), PersonF(X)])), 
always(or([not NVV4(X), not AdultF(X), PersonF(X)])), 
always(or([not NVV4(X), not MinorF(X), not AdultF(X)])), 
always(or([not NVV6(X), AdultF(X), MinorF(X)])), 
always(or([not NVV6(X), not BOX5F(X), AdultF(X), MinorF(X)])), 
always(or([not NVV6(X), not PersonF(X), AdultF(X), MinorF(X)])), 
always(or([not NVV6(X), not BOX5F(X), not PersonF(X), AdultF(X), MinorF(X)])), 
always(or([not NVV6(X), AdultF(X), not PersonF(X), MinorF(X)])), 
always(or([not NVV6(X), not BOX5F(X), not PersonF(X), MinorF(X)])), 
always(or([not NVV6(X), MinorF(X), AdultF(X)])), 
always(or([not NVV6(X), not BOX5F(X), MinorF(X), AdultF(X)])), 
always(or([not NVV6(X), MinorF(X), not PersonF(X), AdultF(X)])), 
always(or([not NVV6(X), not BOX5F(X), MinorF(X), not PersonF(X), AdultF(X)])), 
always(or([not NVV6(X), not PersonF(X), AdultF(X)])), 
always(or([not NVV6(X), not BOX5F(X), not PersonF(X), AdultF(X)])), 
always(or([not NVV16(X), BOX4F(X)])), 
always(or([not NVV18(X), not BOX4F(X)])), 
always(or([not NVV19(X), AdultF(X)])), 
always(or([not NVV21(X), not AdultF(X)])), 
always(or([not NVV22(X), not AdultP(X), BOX3P(X)])), 
always(or([not NVV22(X), not MinorP(X), PersonP(X)])), 
always(or([not NVV22(X), not AdultP(X), PersonP(X)])), 
always(or([not NVV22(X), not MinorP(X), not AdultP(X)])), 
always(or([not NVV24(X), AdultP(X), MinorP(X)])), 
always(or([not NVV24(X), not BOX3P(X), AdultP(X), MinorP(X)])), 
always(or([not NVV24(X), not PersonP(X), AdultP(X), MinorP(X)])), 
always(or([not NVV24(X), not BOX3P(X), not PersonP(X), AdultP(X), MinorP(X)])), 
always(or([not NVV24(X), AdultP(X), not PersonP(X), MinorP(X)])), 
always(or([not NVV24(X), not BOX3P(X), not PersonP(X), MinorP(X)])), 
always(or([not NVV24(X), MinorP(X), AdultP(X)])), 
always(or([not NVV24(X), not BOX3P(X), MinorP(X), AdultP(X)])), 
always(or([not NVV24(X), MinorP(X), not PersonP(X), AdultP(X)])), 
always(or([not NVV24(X), not BOX3P(X), MinorP(X), not PersonP(X), AdultP(X)])), 
always(or([not NVV24(X), not PersonP(X), AdultP(X)])), 
always(or([not NVV24(X), not BOX3P(X), not PersonP(X), AdultP(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 NVV44, NVV45])), 
always(or([not NVV46, NVV47])), 
always(or([not NVV48, NVV49])), 
always(or([not NVV50, NVV51])), 
always(or([not NVV52, NVV53])), 
always(or([not NVV54, NVV55])), 
always(or([not NVV56, NVV57])), 
always(or([not NVV58, NVV59])), 
always(or([not NVV60, NVV61])), 
always(or([not NVV62, NVV63])), 
always(or([not NVV64, NVV65])), 
always(or([not NVV66, NVV67])), 
always(or([not NVV68, NVV69])), 
always(or([not NVV70, NVV71])), 
always(or([not NVV72, NVV73])), 
always(or([not NVV74, NVV75])), 
always(or([not NVV76, NVV77])), 
always(or([not NVV78, NVV79])), 
always(or([not NVV81, NVV82])), 
always(or([not NVV83, NVV84])), 
always(or([not NVV86, NVV87])), 
always(or([not NVV88, NVV89])), 
always(or([not NVV90, NVV91])), 
always(or([not NVV92, NVV80])), 
always(or([not NVV94, NVV95])), 
always(or([not NVV96, NVV97])), 
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, NVV141])), 
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, NVV85])), 
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, NVV25])), 
always(or([not NVV170, NVV171])), 
always(or([not NVV172, NVV173])), 
always(or([not NVV174, NVV175])), 
always(or([not NVV176, NVV157])),
always(or([not NVV1(X), next(NVV1(hidden(X)))])), 
always(or([not NVV1(constant(X)), next(NVV1(constant(X)))])), 
always(or([not NVV2(X), next(not BOX4F(hidden(X)))])), 
always(or([not NVV2(constant(X)), next(not BOX4F(constant(X)))])), 
always(or([not NVV3(X), next(NVV4(hidden(X)))])), 
always(or([not NVV3(constant(X)), next(NVV4(constant(X)))])), 
always(or([not NVV5(X), next(NVV6(hidden(X)))])), 
always(or([not NVV5(constant(X)), next(NVV6(constant(X)))])), 
always(or([not NVV7(X), next(BOX4F(hidden(X)))])), 
always(or([not NVV7(constant(X)), next(BOX4F(constant(X)))])), 
always(or([not NVV8(X), next(not BOX1P(hidden(X)))])), 
always(or([not NVV8(constant(X)), next(not BOX1P(constant(X)))])), 
always(or([not NVV9(X), next(BOX2P(hidden(X)))])), 
always(or([not NVV9(constant(X)), next(BOX2P(constant(X)))])), 
always(or([not NVV10(X), next(not BOX2P(hidden(X)))])), 
always(or([not NVV10(constant(X)), next(not BOX2P(constant(X)))])), 
always(or([not NVV11(X), next(BOX1P(hidden(X)))])), 
always(or([not NVV11(constant(X)), next(BOX1P(constant(X)))])), 
always(or([not NVV12(X), next(not BOX3P(hidden(X)))])), 
always(or([not NVV12(constant(X)), next(not BOX3P(constant(X)))])), 
always(or([not NVV13(X), next(AdultP(hidden(X)))])), 
always(or([not NVV13(constant(X)), next(AdultP(constant(X)))])), 
always(or([not NVV14(X), next(not AdultP(hidden(X)))])), 
always(or([not NVV14(constant(X)), next(not AdultP(constant(X)))])), 
always(or([not NVV15(X), next(BOX3P(hidden(X)))])), 
always(or([not NVV15(constant(X)), next(BOX3P(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(NVV19(hidden(X)))])), 
always(or([not NVV19(constant(X)), next(NVV19(constant(X)))])), 
always(or([not NVV22(X), next(NVV22(hidden(X)))])), 
always(or([not NVV22(constant(X)), next(NVV22(constant(X)))])), 
always(or([not NVV25, 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(NVV44)])), 
always(or([not NVV45, next(NVV46)])), 
always(or([not NVV47, next(NVV48)])), 
always(or([not NVV49, next(NVV50)])), 
always(or([not NVV51, next(NVV52)])), 
always(or([not NVV53, next(NVV54)])), 
always(or([not NVV55, next(NVV56)])), 
always(or([not NVV57, next(NVV58)])), 
always(or([not NVV59, next(NVV60)])), 
always(or([not NVV61, next(NVV62)])), 
always(or([not NVV63, next(NVV64)])), 
always(or([not NVV65, next(NVV66)])), 
always(or([not NVV67, next(NVV68)])), 
always(or([not NVV69, next(NVV70)])), 
always(or([not NVV71, next(NVV72)])), 
always(or([not NVV73, next(NVV74)])), 
always(or([not NVV75, next(NVV76)])), 
always(or([not NVV77, next(NVV78)])), 
always(or([not NVV79, next(MinorF(John))])), 
always(or([not NVV80, next(NVV81)])), 
always(or([not NVV82, next(NVV83)])), 
always(or([not NVV84, next(AdultF(John))])), 
always(or([not NVV85, next(NVV86)])), 
always(or([not NVV87, next(NVV88)])), 
always(or([not NVV89, next(NVV90)])), 
always(or([not NVV91, next(NVV92)])), 
always(or([not NVV93, next(NVV94)])), 
always(or([not NVV95, next(NVV96)])), 
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 NVV17(X), sometime(NVV18(X))])), 
always(or([not NVV17(constant(John)), sometime(NVV18(constant(John)))])), 
always(or([not NVV20(X), sometime(NVV21(X))])), 
always(or([not NVV20(constant(John)), sometime(NVV21(constant(John)))])), 
always(or([not NVV23(X), sometime(NVV24(X))])), 
always(or([not NVV23(constant(John)), sometime(NVV24(constant(John)))]))]).

