and([
or([BOX0F(X)]), 
or([NVV1(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 BOX5F(X), BOX3P(X)]), 
or([not BOX3P(X), BOX5F(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 AdultF(X), AdultP(X)]), 
or([not AdultP(X), AdultF(X)]), 
or([NVV25]), 
or([NVV30]), 
or([NVV37]), 
or([NVV57]), 
or([NVV45]), 
or([NVV65]), 
or([NVV73]), 
or([NVV34]), 
or([NVV53]), 
or([NVV29]), 
or([NVV85]), 
or([NVV81]), 
or([NVV69]), 
or([NVV61]), 
or([MinorF(constant(John))]), 
or([NVV77]), 
or([NVV89]), 
or([NVV49]), 
or([NVV93]), 
or([NVV41]),
always(or([not NVV1(X), not BOX2P(X), NVV2(X)])), 
always(or([not NVV1(X), NVV3(X), BOX2P(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), not BOX5F(X), NVV9(X)])), 
always(or([not NVV1(X), NVV10(X), BOX5F(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), NVV16(X), BOX4F(X)])), 
always(or([not NVV1(X), NVV16(X), NVV17(X)])), 
always(or([not NVV1(X), not BOX4F(X), NVV19(X), NVV21(X)])), 
always(or([not NVV1(X), not BOX0F(X), NVV22(X)])), 
always(or([not NVV1(X), NVV23(X), BOX0F(X)])), 
always(or([not NVV2(X), not MinorP(X), PersonP(X)])), 
always(or([not NVV2(X), not AdultP(X), PersonP(X)])), 
always(or([not NVV2(X), not AdultP(X), BOX3P(X)])), 
always(or([not NVV2(X), not MinorP(X), not AdultP(X)])), 
always(or([not NVV4(X), AdultP(X), MinorP(X)])), 
always(or([not NVV4(X), not PersonP(X), AdultP(X), MinorP(X)])), 
always(or([not NVV4(X), AdultP(X), not BOX3P(X), MinorP(X)])), 
always(or([not NVV4(X), not PersonP(X), AdultP(X), not BOX3P(X), MinorP(X)])), 
always(or([not NVV4(X), not PersonP(X), not BOX3P(X), MinorP(X)])), 
always(or([not NVV4(X), MinorP(X), AdultP(X)])), 
always(or([not NVV4(X), MinorP(X), not PersonP(X), AdultP(X)])), 
always(or([not NVV4(X), not PersonP(X), AdultP(X)])), 
always(or([not NVV4(X), MinorP(X), not BOX3P(X), AdultP(X)])), 
always(or([not NVV4(X), MinorP(X), not PersonP(X), not BOX3P(X), AdultP(X)])), 
always(or([not NVV4(X), not PersonP(X), not BOX3P(X), AdultP(X)])), 
always(or([not NVV9(X), AdultF(X)])), 
always(or([not NVV11(X), not AdultF(X)])), 
always(or([not NVV18(X), not MinorF(X), PersonF(X)])), 
always(or([not NVV18(X), not AdultF(X), PersonF(X)])), 
always(or([not NVV18(X), not AdultF(X), BOX5F(X)])), 
always(or([not NVV18(X), not MinorF(X), not AdultF(X)])), 
always(or([not NVV20(X), AdultF(X), MinorF(X)])), 
always(or([not NVV20(X), not PersonF(X), AdultF(X), MinorF(X)])), 
always(or([not NVV20(X), AdultF(X), not BOX5F(X), MinorF(X)])), 
always(or([not NVV20(X), not PersonF(X), AdultF(X), not BOX5F(X), MinorF(X)])), 
always(or([not NVV20(X), not PersonF(X), not BOX5F(X), MinorF(X)])), 
always(or([not NVV20(X), MinorF(X), AdultF(X)])), 
always(or([not NVV20(X), MinorF(X), not PersonF(X), AdultF(X)])), 
always(or([not NVV20(X), not PersonF(X), AdultF(X)])), 
always(or([not NVV20(X), MinorF(X), not BOX5F(X), AdultF(X)])), 
always(or([not NVV20(X), MinorF(X), not PersonF(X), not BOX5F(X), AdultF(X)])), 
always(or([not NVV20(X), not PersonF(X), not BOX5F(X), AdultF(X)])), 
always(or([not NVV22(X), BOX4F(X)])), 
always(or([not NVV24(X), not BOX4F(X)])), 
always(or([not NVV26, NVV27])), 
always(or([not NVV28, NVV29])), 
always(or([not NVV31, NVV32])), 
always(or([not NVV33, NVV34])), 
always(or([not NVV35, NVV36])), 
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, NVV30])), 
always(or([not NVV58, NVV59])), 
always(or([not NVV60, NVV61])), 
always(or([not NVV62, NVV63])), 
always(or([not NVV64, NVV37])), 
always(or([not NVV66, NVV67])), 
always(or([not NVV68, NVV69])), 
always(or([not NVV70, NVV71])), 
always(or([not NVV72, NVV25])), 
always(or([not NVV74, NVV75])), 
always(or([not NVV76, NVV77])), 
always(or([not NVV78, NVV79])), 
always(or([not NVV80, NVV81])), 
always(or([not NVV82, NVV83])), 
always(or([not NVV84, NVV85])), 
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, NVV65])),
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(NVV9(hidden(X)))])), 
always(or([not NVV9(constant(X)), next(NVV9(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(not BOX4F(hidden(X)))])), 
always(or([not NVV16(constant(X)), next(not BOX4F(constant(X)))])), 
always(or([not NVV17(X), next(NVV18(hidden(X)))])), 
always(or([not NVV17(constant(X)), next(NVV18(constant(X)))])), 
always(or([not NVV19(X), next(NVV20(hidden(X)))])), 
always(or([not NVV19(constant(X)), next(NVV20(constant(X)))])), 
always(or([not NVV21(X), next(BOX4F(hidden(X)))])), 
always(or([not NVV21(constant(X)), next(BOX4F(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(AdultF(John))])), 
always(or([not NVV30, next(NVV31)])), 
always(or([not NVV32, next(NVV33)])), 
always(or([not NVV34, next(NVV35)])), 
always(or([not NVV36, next(MinorF(John))])), 
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(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 NVV3(X), sometime(NVV4(X))])), 
always(or([not NVV3(constant(John)), sometime(NVV4(constant(John)))])), 
always(or([not NVV10(X), sometime(NVV11(X))])), 
always(or([not NVV10(constant(John)), sometime(NVV11(constant(John)))])), 
always(or([not NVV23(X), sometime(NVV24(X))])), 
always(or([not NVV23(constant(John)), sometime(NVV24(constant(John)))]))]).

