and([
or([BOX0F(X)]), 
or([NVV1(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 BOX0F(X), BOX1P(X)]), 
or([not BOX1P(X), BOX0F(X)]), 
or([not MinorF(X), MinorP(X)]), 
or([not MinorP(X), MinorF(X)]), 
or([not PersonF(X), PersonP(X)]), 
or([not PersonP(X), PersonF(X)]), 
or([not BOX4F(X), BOX2P(X)]), 
or([not BOX2P(X), BOX4F(X)]), 
or([NVV25]), 
or([NVV64]), 
or([NVV75]), 
or([NVV31]), 
or([NVV85]), 
or([NVV72]), 
or([NVV99]), 
or([NVV105]), 
or([NVV68]), 
or([NVV70]), 
or([NVV97]), 
or([MinorF(constant(John))]), 
or([NVV35]), 
or([NVV83]), 
or([NVV91]), 
or([NVV89]), 
or([NVV107]), 
or([NVV29]), 
or([NVV93]), 
or([NVV27]), 
or([NVV95]), 
or([NVV77]), 
or([NVV101]), 
or([NVV33]), 
or([NVV79]), 
or([NVV87]), 
or([NVV74]), 
or([NVV103]), 
or([NVV66]), 
or([NVV81]),
always(or([not NVV1(X), not BOX0F(X), NVV2(X)])), 
always(or([not NVV1(X), NVV3(X), BOX0F(X)])), 
always(or([not NVV1(X), not BOX5F(X), NVV5(X)])), 
always(or([not NVV1(X), NVV6(X), BOX5F(X)])), 
always(or([not NVV1(X), NVV8(X), BOX4F(X)])), 
always(or([not NVV1(X), NVV8(X), NVV9(X)])), 
always(or([not NVV1(X), not BOX4F(X), NVV11(X), NVV13(X)])), 
always(or([not NVV1(X), not BOX2P(X), NVV14(X)])), 
always(or([not NVV1(X), NVV15(X), BOX2P(X)])), 
always(or([not NVV1(X), NVV17(X), BOX1P(X)])), 
always(or([not NVV1(X), NVV17(X), NVV18(X)])), 
always(or([not NVV1(X), not BOX1P(X), NVV19(X), NVV20(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 NVV5(X), AdultF(X)])), 
always(or([not NVV7(X), not AdultF(X)])), 
always(or([not NVV10(X), not MinorF(X), not AdultF(X)])), 
always(or([not NVV10(X), not MinorF(X), PersonF(X)])), 
always(or([not NVV10(X), not AdultF(X), PersonF(X)])), 
always(or([not NVV10(X), not AdultF(X), BOX5F(X)])), 
always(or([not NVV12(X), MinorF(X), AdultF(X)])), 
always(or([not NVV12(X), MinorF(X), not PersonF(X), AdultF(X)])), 
always(or([not NVV12(X), not PersonF(X), AdultF(X)])), 
always(or([not NVV12(X), MinorF(X), AdultF(X), not BOX5F(X)])), 
always(or([not NVV12(X), MinorF(X), not PersonF(X), AdultF(X), not BOX5F(X)])), 
always(or([not NVV12(X), not PersonF(X), AdultF(X), not BOX5F(X)])), 
always(or([not NVV12(X), AdultF(X), MinorF(X), not PersonF(X), not BOX5F(X)])), 
always(or([not NVV12(X), MinorF(X), not PersonF(X), not BOX5F(X)])), 
always(or([not NVV12(X), AdultF(X), not PersonF(X), not BOX5F(X)])), 
always(or([not NVV14(X), not MinorP(X), not AdultP(X)])), 
always(or([not NVV14(X), not MinorP(X), PersonP(X)])), 
always(or([not NVV14(X), not AdultP(X), PersonP(X)])), 
always(or([not NVV14(X), not AdultP(X), BOX3P(X)])), 
always(or([not NVV16(X), MinorP(X), AdultP(X)])), 
always(or([not NVV16(X), MinorP(X), not PersonP(X), AdultP(X)])), 
always(or([not NVV16(X), not PersonP(X), AdultP(X)])), 
always(or([not NVV16(X), MinorP(X), AdultP(X), not BOX3P(X)])), 
always(or([not NVV16(X), MinorP(X), not PersonP(X), AdultP(X), not BOX3P(X)])), 
always(or([not NVV16(X), not PersonP(X), AdultP(X), not BOX3P(X)])), 
always(or([not NVV16(X), AdultP(X), MinorP(X), not PersonP(X), not BOX3P(X)])), 
always(or([not NVV16(X), MinorP(X), not PersonP(X), not BOX3P(X)])), 
always(or([not NVV16(X), AdultP(X), not PersonP(X), not BOX3P(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 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 NVV76, NVV77])), 
always(or([not NVV78, NVV79])), 
always(or([not NVV80, NVV81])), 
always(or([not NVV82, NVV83])), 
always(or([not NVV84, NVV64])), 
always(or([not NVV86, NVV87])), 
always(or([not NVV88, NVV89])), 
always(or([not NVV90, NVV91])), 
always(or([not NVV92, NVV93])), 
always(or([not NVV94, NVV95])), 
always(or([not NVV96, NVV97])), 
always(or([not NVV98, NVV25])), 
always(or([not NVV100, NVV101])), 
always(or([not NVV102, NVV103])), 
always(or([not NVV104, NVV75])), 
always(or([not NVV106, NVV85])), 
always(or([not NVV108, NVV105])),
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 BOX4F(hidden(X)))])), 
always(or([not NVV8(constant(X)), next(not BOX4F(constant(X)))])), 
always(or([not NVV9(X), next(NVV10(hidden(X)))])), 
always(or([not NVV9(constant(X)), next(NVV10(constant(X)))])), 
always(or([not NVV11(X), next(NVV12(hidden(X)))])), 
always(or([not NVV11(constant(X)), next(NVV12(constant(X)))])), 
always(or([not NVV13(X), next(BOX4F(hidden(X)))])), 
always(or([not NVV13(constant(X)), next(BOX4F(constant(X)))])), 
always(or([not NVV14(X), next(NVV14(hidden(X)))])), 
always(or([not NVV14(constant(X)), next(NVV14(constant(X)))])), 
always(or([not NVV17(X), next(not BOX1P(hidden(X)))])), 
always(or([not NVV17(constant(X)), next(not BOX1P(constant(X)))])), 
always(or([not NVV18(X), next(BOX2P(hidden(X)))])), 
always(or([not NVV18(constant(X)), next(BOX2P(constant(X)))])), 
always(or([not NVV19(X), next(not BOX2P(hidden(X)))])), 
always(or([not NVV19(constant(X)), next(not BOX2P(constant(X)))])), 
always(or([not NVV20(X), next(BOX1P(hidden(X)))])), 
always(or([not NVV20(constant(X)), next(BOX1P(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(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(AdultF(John))])), 
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(MinorF(John))])), 
always(or([not NVV75, next(NVV76)])), 
always(or([not NVV77, next(NVV78)])), 
always(or([not NVV79, next(NVV80)])), 
always(or([not NVV81, next(NVV82)])), 
always(or([not NVV83, next(NVV84)])), 
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 NVV3(X), sometime(NVV4(X))])), 
always(or([not NVV3(constant(John)), sometime(NVV4(constant(John)))])), 
always(or([not NVV6(X), sometime(NVV7(X))])), 
always(or([not NVV6(constant(John)), sometime(NVV7(constant(John)))])), 
always(or([not NVV15(X), sometime(NVV16(X))])), 
always(or([not NVV15(constant(John)), sometime(NVV16(constant(John)))]))]).

