and([
or([BOX2F(X)]), 
or([not PSalaryF, E1SalaryInvF(constant(dSalaryInv))]), 
or([BOX0F(X)]), 
or([BOX1F(X)]), 
or([not PinvSalaryF, E1SalaryF(constant(dSalary))]), 
or([NVV1(X)]), 
or([not BOX12F(X), BOX5P(X)]), 
or([not BOX5P(X), BOX12F(X)]), 
or([not BOX13F(X), BOX6P(X)]), 
or([not BOX6P(X), BOX13F(X)]), 
or([not BOX15F(X), BOX8P(X)]), 
or([not BOX8P(X), BOX15F(X)]), 
or([not BOX2F(X), BOX19P(X)]), 
or([not BOX19P(X), BOX2F(X)]), 
or([not BOX0F(X), BOX17P(X)]), 
or([not BOX17P(X), BOX0F(X)]), 
or([not E1SalaryF(X), E1SalaryP(X)]), 
or([not E1SalaryP(X), E1SalaryF(X)]), 
or([not E2SalaryF(X), E2SalaryP(X)]), 
or([not E2SalaryP(X), E2SalaryF(X)]), 
or([not BOX10F(X), BOX3P(X)]), 
or([not BOX3P(X), BOX10F(X)]), 
or([not PersonF(X), PersonP(X)]), 
or([not PersonP(X), PersonF(X)]), 
or([not BOX1F(X), BOX18P(X)]), 
or([not BOX18P(X), BOX1F(X)]), 
or([not E1SalaryF(constant(dSalary)), E1SalaryP(constant(dSalary))]), 
or([not E1SalaryP(constant(dSalary)), E1SalaryF(constant(dSalary))]), 
or([not BOX11F(X), BOX4P(X)]), 
or([not BOX4P(X), BOX11F(X)]), 
or([not BOX14F(X), BOX7P(X)]), 
or([not BOX7P(X), BOX14F(X)]), 
or([not PSalaryF, PSalaryP]), 
or([not PSalaryP, PSalaryF]), 
or([not BOX16F(X), BOX9P(X)]), 
or([not BOX9P(X), BOX16F(X)]), 
or([not PinvSalaryF, PinvSalaryP]), 
or([not PinvSalaryP, PinvSalaryF]), 
or([not E1SalaryInvF(X), E1SalaryInvP(X)]), 
or([not E1SalaryInvP(X), E1SalaryInvF(X)]), 
or([not PSalaryF, PSalaryF]), 
or([not PinvSalaryF, PinvSalaryF]), 
or([not E1SalaryInvF(constant(dSalaryInv)), E1SalaryInvP(constant(dSalaryInv))]), 
or([not E1SalaryInvP(constant(dSalaryInv)), E1SalaryInvF(constant(dSalaryInv))]), 
or([E1SalaryInvF(constant(S18))]), 
or([E1SalaryInvF(constant(S22))]), 
or([E1SalaryInvF(constant(S23))]), 
or([E1SalaryInvF(constant(S25))]), 
or([E1SalaryInvF(constant(S33))]), 
or([E1SalaryInvF(constant(S24))]), 
or([E1SalaryInvF(constant(S21))]), 
or([E1SalaryInvF(constant(S10))]), 
or([E1SalaryInvF(constant(S3))]), 
or([E1SalaryInvF(constant(S5))]), 
or([E1SalaryInvF(constant(S8))]), 
or([E1SalaryInvF(constant(S12))]), 
or([E1SalaryInvF(constant(S7))]), 
or([E1SalaryInvF(constant(S9))]), 
or([E1SalaryInvF(constant(S17))]), 
or([E1SalaryInvF(constant(S4))]), 
or([E1SalaryInvF(constant(S19))]), 
or([E1SalaryInvF(constant(S38))]), 
or([E1SalaryInvF(constant(S1))]), 
or([E1SalaryInvF(constant(S29))]), 
or([E1SalaryInvF(constant(S27))]), 
or([E1SalaryInvF(constant(S32))]), 
or([E1SalaryInvF(constant(S13))]), 
or([E1SalaryInvF(constant(S35))]), 
or([E1SalaryInvF(constant(S30))]), 
or([E1SalaryInvF(constant(S0))]), 
or([E1SalaryInvF(constant(S36))]), 
or([E1SalaryInvF(constant(S11))]), 
or([E1SalaryInvF(constant(S20))]), 
or([E1SalaryInvF(constant(S15))]), 
or([E1SalaryInvF(constant(S6))]), 
or([E1SalaryInvF(constant(S14))]), 
or([E1SalaryInvF(constant(S37))]), 
or([E1SalaryInvF(constant(S26))]), 
or([E1SalaryInvF(constant(S34))]), 
or([E1SalaryInvF(constant(S2))]), 
or([E1SalaryInvF(constant(S16))]), 
or([E1SalaryInvF(constant(S39))]), 
or([E1SalaryInvF(constant(S31))]), 
or([E1SalaryInvF(constant(S28))]), 
or([PersonF(constant(John))]), 
or([E2SalaryF(constant(John))]),
always(or([not NVV1(X), not BOX12F(X), NVV2])), 
always(or([not NVV1(X), NVV3, BOX12F(X)])), 
always(or([not NVV1(X), not BOX17P(X), NVV5(X)])), 
always(or([not NVV1(X), NVV6(X), BOX17P(X)])), 
always(or([not NVV1(X), not BOX13F(X), NVV8(X)])), 
always(or([not NVV1(X), NVV9(X), BOX13F(X)])), 
always(or([not NVV1(X), NVV11(X), BOX6P(X)])), 
always(or([not NVV1(X), NVV11(X), NVV12(X)])), 
always(or([not NVV1(X), not BOX6P(X), NVV14(X), NVV16(X)])), 
always(or([not NVV1(X), not BOX15F(X), NVV17])), 
always(or([not NVV1(X), NVV18, BOX15F(X)])), 
always(or([not NVV1(X), not BOX18P(X), NVV20(X)])), 
always(or([not NVV1(X), NVV21(X), BOX18P(X)])), 
always(or([not NVV1(X), NVV23(X), BOX0F(X)])), 
always(or([not NVV1(X), NVV23(X), NVV24(X)])), 
always(or([not NVV1(X), not BOX0F(X), NVV25(X), NVV26(X)])), 
always(or([not NVV1(X), NVV27(X), BOX5P(X)])), 
always(or([not NVV1(X), NVV27(X), NVV28])), 
always(or([not NVV1(X), not BOX5P(X), NVV29, NVV30(X)])), 
always(or([not NVV1(X), NVV31(X), BOX14F(X)])), 
always(or([not NVV1(X), NVV31(X), NVV32(X)])), 
always(or([not NVV1(X), not BOX14F(X), NVV33(X), NVV34(X)])), 
always(or([not NVV1(X), NVV35(X), BOX3P(X)])), 
always(or([not NVV1(X), NVV35(X), NVV36(X)])), 
always(or([not NVV1(X), not BOX3P(X), NVV38(X), NVV40(X)])), 
always(or([not NVV1(X), NVV41(X), BOX11F(X)])), 
always(or([not NVV1(X), NVV41(X), NVV42(X)])), 
always(or([not NVV1(X), not BOX11F(X), NVV43(X), NVV44(X)])), 
always(or([not NVV1(X), not BOX16F(X), NVV45(X)])), 
always(or([not NVV1(X), NVV46(X), BOX16F(X)])), 
always(or([not NVV1(X), NVV48(X), BOX8P(X)])), 
always(or([not NVV1(X), NVV48(X), NVV49])), 
always(or([not NVV1(X), not BOX8P(X), NVV50, NVV51(X)])), 
always(or([not NVV1(X), not BOX10F(X), NVV52(X)])), 
always(or([not NVV1(X), NVV53(X), BOX10F(X)])), 
always(or([not NVV1(X), NVV55(X), BOX1F(X)])), 
always(or([not NVV1(X), NVV55(X), NVV56(X)])), 
always(or([not NVV1(X), not BOX1F(X), NVV57(X), NVV58(X)])), 
always(or([not NVV1(X), not BOX4P(X), NVV59(X)])), 
always(or([not NVV1(X), NVV60(X), BOX4P(X)])), 
always(or([not NVV1(X), not BOX7P(X), NVV62(X)])), 
always(or([not NVV1(X), NVV63(X), BOX7P(X)])), 
always(or([not NVV1(X), NVV65(X), BOX2F(X)])), 
always(or([not NVV1(X), NVV65(X), NVV66(X)])), 
always(or([not NVV1(X), not BOX2F(X), NVV67(X), NVV68(X)])), 
always(or([not NVV1(X), not BOX19P(X), NVV69(X)])), 
always(or([not NVV1(X), NVV70(X), BOX19P(X)])), 
always(or([not NVV1(X), NVV72(X), BOX9P(X)])), 
always(or([not NVV1(X), NVV72(X), NVV73(X)])), 
always(or([not NVV1(X), not BOX9P(X), NVV75(X), NVV77(X)])), 
always(or([not NVV2, PinvSalaryF])), 
always(or([not NVV4, not PinvSalaryF])), 
always(or([not NVV5(X), BOX3P(X)])), 
always(or([not NVV7(X), not BOX3P(X)])), 
always(or([not NVV8(X), not E1SalaryF(X), BOX14F(X)])), 
always(or([not NVV10(X), E1SalaryF(X)])), 
always(or([not NVV10(X), not BOX14F(X)])), 
always(or([not NVV13(X), not E1SalaryP(X), BOX7P(X)])), 
always(or([not NVV15(X), E1SalaryP(X)])), 
always(or([not NVV15(X), not BOX7P(X)])), 
always(or([not NVV17, PSalaryF])), 
always(or([not NVV19, not PSalaryF])), 
always(or([not NVV20(X), BOX6P(X)])), 
always(or([not NVV22(X), not BOX6P(X)])), 
always(or([not NVV37(X), not E1SalaryInvP(X), BOX4P(X)])), 
always(or([not NVV39(X), E1SalaryInvP(X)])), 
always(or([not NVV39(X), not BOX4P(X)])), 
always(or([not NVV45(X), not PersonF(X), E1SalaryF(X)])), 
always(or([not NVV45(X), not PersonF(X), not E2SalaryF(X)])), 
always(or([not NVV45(X), not E2SalaryF(X), E1SalaryF(X)])), 
always(or([not NVV47(X), not E1SalaryF(X), PersonF(X), E2SalaryF(X)])), 
always(or([not NVV47(X), PersonF(X), E2SalaryF(X)])), 
always(or([not NVV47(X), not E1SalaryF(X), E2SalaryF(X)])), 
always(or([not NVV47(X), PersonF(X), not E1SalaryF(X)])), 
always(or([not NVV47(X), PersonF(X), E2SalaryF(X), not E1SalaryF(X)])), 
always(or([not NVV47(X), E2SalaryF(X), not E1SalaryF(X)])), 
always(or([not NVV52(X), not E1SalaryInvF(X), BOX11F(X)])), 
always(or([not NVV54(X), E1SalaryInvF(X)])), 
always(or([not NVV54(X), not BOX11F(X)])), 
always(or([not NVV59(X), BOX5P(X)])), 
always(or([not NVV61(X), not BOX5P(X)])), 
always(or([not NVV62(X), BOX8P(X)])), 
always(or([not NVV64(X), not BOX8P(X)])), 
always(or([not NVV69(X), BOX9P(X)])), 
always(or([not NVV71(X), not BOX9P(X)])), 
always(or([not NVV74(X), not PersonP(X), E1SalaryP(X)])), 
always(or([not NVV74(X), not PersonP(X), not E2SalaryP(X)])), 
always(or([not NVV74(X), not E2SalaryP(X), E1SalaryP(X)])), 
always(or([not NVV76(X), not E1SalaryP(X), PersonP(X), E2SalaryP(X)])), 
always(or([not NVV76(X), PersonP(X), E2SalaryP(X)])), 
always(or([not NVV76(X), not E1SalaryP(X), E2SalaryP(X)])), 
always(or([not NVV76(X), PersonP(X), not E1SalaryP(X)])), 
always(or([not NVV76(X), PersonP(X), E2SalaryP(X), not E1SalaryP(X)])), 
always(or([not NVV76(X), E2SalaryP(X), not E1SalaryP(X)])),
always(or([not NVV1(X), next(NVV1(hidden(X)))])), 
always(or([not NVV1(constant(X)), next(NVV1(constant(X)))])), 
always(or([not NVV2, next(NVV2)])), 
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(NVV8(hidden(X)))])), 
always(or([not NVV8(constant(X)), next(NVV8(constant(X)))])), 
always(or([not NVV11(X), next(not BOX6P(hidden(X)))])), 
always(or([not NVV11(constant(X)), next(not BOX6P(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(NVV15(hidden(X)))])), 
always(or([not NVV14(constant(X)), next(NVV15(constant(X)))])), 
always(or([not NVV16(X), next(BOX6P(hidden(X)))])), 
always(or([not NVV16(constant(X)), next(BOX6P(constant(X)))])), 
always(or([not NVV17, next(NVV17)])), 
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(not BOX0F(hidden(X)))])), 
always(or([not NVV23(constant(X)), next(not BOX0F(constant(X)))])), 
always(or([not NVV24(X), next(BOX10F(hidden(X)))])), 
always(or([not NVV24(constant(X)), next(BOX10F(constant(X)))])), 
always(or([not NVV25(X), next(not BOX10F(hidden(X)))])), 
always(or([not NVV25(constant(X)), next(not BOX10F(constant(X)))])), 
always(or([not NVV26(X), next(BOX0F(hidden(X)))])), 
always(or([not NVV26(constant(X)), next(BOX0F(constant(X)))])), 
always(or([not NVV27(X), next(not BOX5P(hidden(X)))])), 
always(or([not NVV27(constant(X)), next(not BOX5P(constant(X)))])), 
always(or([not NVV28, next(PinvSalaryF)])), 
always(or([not NVV29, next(not PinvSalaryF)])), 
always(or([not NVV30(X), next(BOX5P(hidden(X)))])), 
always(or([not NVV30(constant(X)), next(BOX5P(constant(X)))])), 
always(or([not NVV31(X), next(not BOX14F(hidden(X)))])), 
always(or([not NVV31(constant(X)), next(not BOX14F(constant(X)))])), 
always(or([not NVV32(X), next(BOX15F(hidden(X)))])), 
always(or([not NVV32(constant(X)), next(BOX15F(constant(X)))])), 
always(or([not NVV33(X), next(not BOX15F(hidden(X)))])), 
always(or([not NVV33(constant(X)), next(not BOX15F(constant(X)))])), 
always(or([not NVV34(X), next(BOX14F(hidden(X)))])), 
always(or([not NVV34(constant(X)), next(BOX14F(constant(X)))])), 
always(or([not NVV35(X), next(not BOX3P(hidden(X)))])), 
always(or([not NVV35(constant(X)), next(not BOX3P(constant(X)))])), 
always(or([not NVV36(X), next(NVV37(hidden(X)))])), 
always(or([not NVV36(constant(X)), next(NVV37(constant(X)))])), 
always(or([not NVV38(X), next(NVV39(hidden(X)))])), 
always(or([not NVV38(constant(X)), next(NVV39(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(not BOX11F(hidden(X)))])), 
always(or([not NVV41(constant(X)), next(not BOX11F(constant(X)))])), 
always(or([not NVV42(X), next(BOX12F(hidden(X)))])), 
always(or([not NVV42(constant(X)), next(BOX12F(constant(X)))])), 
always(or([not NVV43(X), next(not BOX12F(hidden(X)))])), 
always(or([not NVV43(constant(X)), next(not BOX12F(constant(X)))])), 
always(or([not NVV44(X), next(BOX11F(hidden(X)))])), 
always(or([not NVV44(constant(X)), next(BOX11F(constant(X)))])), 
always(or([not NVV45(X), next(NVV45(hidden(X)))])), 
always(or([not NVV45(constant(X)), next(NVV45(constant(X)))])), 
always(or([not NVV48(X), next(not BOX8P(hidden(X)))])), 
always(or([not NVV48(constant(X)), next(not BOX8P(constant(X)))])), 
always(or([not NVV49, next(PSalaryF)])), 
always(or([not NVV50, next(not PSalaryF)])), 
always(or([not NVV51(X), next(BOX8P(hidden(X)))])), 
always(or([not NVV51(constant(X)), next(BOX8P(constant(X)))])), 
always(or([not NVV52(X), next(NVV52(hidden(X)))])), 
always(or([not NVV52(constant(X)), next(NVV52(constant(X)))])), 
always(or([not NVV55(X), next(not BOX1F(hidden(X)))])), 
always(or([not NVV55(constant(X)), next(not BOX1F(constant(X)))])), 
always(or([not NVV56(X), next(BOX13F(hidden(X)))])), 
always(or([not NVV56(constant(X)), next(BOX13F(constant(X)))])), 
always(or([not NVV57(X), next(not BOX13F(hidden(X)))])), 
always(or([not NVV57(constant(X)), next(not BOX13F(constant(X)))])), 
always(or([not NVV58(X), next(BOX1F(hidden(X)))])), 
always(or([not NVV58(constant(X)), next(BOX1F(constant(X)))])), 
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(NVV62(hidden(X)))])), 
always(or([not NVV62(constant(X)), next(NVV62(constant(X)))])), 
always(or([not NVV65(X), next(not BOX2F(hidden(X)))])), 
always(or([not NVV65(constant(X)), next(not BOX2F(constant(X)))])), 
always(or([not NVV66(X), next(BOX16F(hidden(X)))])), 
always(or([not NVV66(constant(X)), next(BOX16F(constant(X)))])), 
always(or([not NVV67(X), next(not BOX16F(hidden(X)))])), 
always(or([not NVV67(constant(X)), next(not BOX16F(constant(X)))])), 
always(or([not NVV68(X), next(BOX2F(hidden(X)))])), 
always(or([not NVV68(constant(X)), next(BOX2F(constant(X)))])), 
always(or([not NVV69(X), next(NVV69(hidden(X)))])), 
always(or([not NVV69(constant(X)), next(NVV69(constant(X)))])), 
always(or([not NVV72(X), next(not BOX9P(hidden(X)))])), 
always(or([not NVV72(constant(X)), next(not BOX9P(constant(X)))])), 
always(or([not NVV73(X), next(NVV74(hidden(X)))])), 
always(or([not NVV73(constant(X)), next(NVV74(constant(X)))])), 
always(or([not NVV75(X), next(NVV76(hidden(X)))])), 
always(or([not NVV75(constant(X)), next(NVV76(constant(X)))])), 
always(or([not NVV77(X), next(BOX9P(hidden(X)))])), 
always(or([not NVV77(constant(X)), next(BOX9P(constant(X)))])),
always(or([not NVV3, sometime(NVV4)])), 
always(or([not NVV6(X), sometime(NVV7(X))])), 
always(or([not NVV6(constant(dSalary)), sometime(NVV7(constant(dSalary)))])), 
always(or([not NVV6(constant(dSalaryInv)), sometime(NVV7(constant(dSalaryInv)))])), 
always(or([not NVV6(constant(S18)), sometime(NVV7(constant(S18)))])), 
always(or([not NVV6(constant(S22)), sometime(NVV7(constant(S22)))])), 
always(or([not NVV6(constant(S23)), sometime(NVV7(constant(S23)))])), 
always(or([not NVV6(constant(S25)), sometime(NVV7(constant(S25)))])), 
always(or([not NVV6(constant(S33)), sometime(NVV7(constant(S33)))])), 
always(or([not NVV6(constant(S24)), sometime(NVV7(constant(S24)))])), 
always(or([not NVV6(constant(S21)), sometime(NVV7(constant(S21)))])), 
always(or([not NVV6(constant(S10)), sometime(NVV7(constant(S10)))])), 
always(or([not NVV6(constant(S3)), sometime(NVV7(constant(S3)))])), 
always(or([not NVV6(constant(S5)), sometime(NVV7(constant(S5)))])), 
always(or([not NVV6(constant(S8)), sometime(NVV7(constant(S8)))])), 
always(or([not NVV6(constant(S12)), sometime(NVV7(constant(S12)))])), 
always(or([not NVV6(constant(S7)), sometime(NVV7(constant(S7)))])), 
always(or([not NVV6(constant(S9)), sometime(NVV7(constant(S9)))])), 
always(or([not NVV6(constant(S17)), sometime(NVV7(constant(S17)))])), 
always(or([not NVV6(constant(S4)), sometime(NVV7(constant(S4)))])), 
always(or([not NVV6(constant(S19)), sometime(NVV7(constant(S19)))])), 
always(or([not NVV6(constant(S38)), sometime(NVV7(constant(S38)))])), 
always(or([not NVV6(constant(S1)), sometime(NVV7(constant(S1)))])), 
always(or([not NVV6(constant(S29)), sometime(NVV7(constant(S29)))])), 
always(or([not NVV6(constant(S27)), sometime(NVV7(constant(S27)))])), 
always(or([not NVV6(constant(S32)), sometime(NVV7(constant(S32)))])), 
always(or([not NVV6(constant(S13)), sometime(NVV7(constant(S13)))])), 
always(or([not NVV6(constant(S35)), sometime(NVV7(constant(S35)))])), 
always(or([not NVV6(constant(S30)), sometime(NVV7(constant(S30)))])), 
always(or([not NVV6(constant(S0)), sometime(NVV7(constant(S0)))])), 
always(or([not NVV6(constant(S36)), sometime(NVV7(constant(S36)))])), 
always(or([not NVV6(constant(S11)), sometime(NVV7(constant(S11)))])), 
always(or([not NVV6(constant(S20)), sometime(NVV7(constant(S20)))])), 
always(or([not NVV6(constant(S15)), sometime(NVV7(constant(S15)))])), 
always(or([not NVV6(constant(S6)), sometime(NVV7(constant(S6)))])), 
always(or([not NVV6(constant(S14)), sometime(NVV7(constant(S14)))])), 
always(or([not NVV6(constant(S37)), sometime(NVV7(constant(S37)))])), 
always(or([not NVV6(constant(S26)), sometime(NVV7(constant(S26)))])), 
always(or([not NVV6(constant(S34)), sometime(NVV7(constant(S34)))])), 
always(or([not NVV6(constant(S2)), sometime(NVV7(constant(S2)))])), 
always(or([not NVV6(constant(S16)), sometime(NVV7(constant(S16)))])), 
always(or([not NVV6(constant(S39)), sometime(NVV7(constant(S39)))])), 
always(or([not NVV6(constant(S31)), sometime(NVV7(constant(S31)))])), 
always(or([not NVV6(constant(S28)), sometime(NVV7(constant(S28)))])), 
always(or([not NVV6(constant(John)), sometime(NVV7(constant(John)))])), 
always(or([not NVV9(X), sometime(NVV10(X))])), 
always(or([not NVV9(constant(dSalary)), sometime(NVV10(constant(dSalary)))])), 
always(or([not NVV9(constant(dSalaryInv)), sometime(NVV10(constant(dSalaryInv)))])), 
always(or([not NVV9(constant(S18)), sometime(NVV10(constant(S18)))])), 
always(or([not NVV9(constant(S22)), sometime(NVV10(constant(S22)))])), 
always(or([not NVV9(constant(S23)), sometime(NVV10(constant(S23)))])), 
always(or([not NVV9(constant(S25)), sometime(NVV10(constant(S25)))])), 
always(or([not NVV9(constant(S33)), sometime(NVV10(constant(S33)))])), 
always(or([not NVV9(constant(S24)), sometime(NVV10(constant(S24)))])), 
always(or([not NVV9(constant(S21)), sometime(NVV10(constant(S21)))])), 
always(or([not NVV9(constant(S10)), sometime(NVV10(constant(S10)))])), 
always(or([not NVV9(constant(S3)), sometime(NVV10(constant(S3)))])), 
always(or([not NVV9(constant(S5)), sometime(NVV10(constant(S5)))])), 
always(or([not NVV9(constant(S8)), sometime(NVV10(constant(S8)))])), 
always(or([not NVV9(constant(S12)), sometime(NVV10(constant(S12)))])), 
always(or([not NVV9(constant(S7)), sometime(NVV10(constant(S7)))])), 
always(or([not NVV9(constant(S9)), sometime(NVV10(constant(S9)))])), 
always(or([not NVV9(constant(S17)), sometime(NVV10(constant(S17)))])), 
always(or([not NVV9(constant(S4)), sometime(NVV10(constant(S4)))])), 
always(or([not NVV9(constant(S19)), sometime(NVV10(constant(S19)))])), 
always(or([not NVV9(constant(S38)), sometime(NVV10(constant(S38)))])), 
always(or([not NVV9(constant(S1)), sometime(NVV10(constant(S1)))])), 
always(or([not NVV9(constant(S29)), sometime(NVV10(constant(S29)))])), 
always(or([not NVV9(constant(S27)), sometime(NVV10(constant(S27)))])), 
always(or([not NVV9(constant(S32)), sometime(NVV10(constant(S32)))])), 
always(or([not NVV9(constant(S13)), sometime(NVV10(constant(S13)))])), 
always(or([not NVV9(constant(S35)), sometime(NVV10(constant(S35)))])), 
always(or([not NVV9(constant(S30)), sometime(NVV10(constant(S30)))])), 
always(or([not NVV9(constant(S0)), sometime(NVV10(constant(S0)))])), 
always(or([not NVV9(constant(S36)), sometime(NVV10(constant(S36)))])), 
always(or([not NVV9(constant(S11)), sometime(NVV10(constant(S11)))])), 
always(or([not NVV9(constant(S20)), sometime(NVV10(constant(S20)))])), 
always(or([not NVV9(constant(S15)), sometime(NVV10(constant(S15)))])), 
always(or([not NVV9(constant(S6)), sometime(NVV10(constant(S6)))])), 
always(or([not NVV9(constant(S14)), sometime(NVV10(constant(S14)))])), 
always(or([not NVV9(constant(S37)), sometime(NVV10(constant(S37)))])), 
always(or([not NVV9(constant(S26)), sometime(NVV10(constant(S26)))])), 
always(or([not NVV9(constant(S34)), sometime(NVV10(constant(S34)))])), 
always(or([not NVV9(constant(S2)), sometime(NVV10(constant(S2)))])), 
always(or([not NVV9(constant(S16)), sometime(NVV10(constant(S16)))])), 
always(or([not NVV9(constant(S39)), sometime(NVV10(constant(S39)))])), 
always(or([not NVV9(constant(S31)), sometime(NVV10(constant(S31)))])), 
always(or([not NVV9(constant(S28)), sometime(NVV10(constant(S28)))])), 
always(or([not NVV9(constant(John)), sometime(NVV10(constant(John)))])), 
always(or([not NVV18, sometime(NVV19)])), 
always(or([not NVV21(X), sometime(NVV22(X))])), 
always(or([not NVV21(constant(dSalary)), sometime(NVV22(constant(dSalary)))])), 
always(or([not NVV21(constant(dSalaryInv)), sometime(NVV22(constant(dSalaryInv)))])), 
always(or([not NVV21(constant(S18)), sometime(NVV22(constant(S18)))])), 
always(or([not NVV21(constant(S22)), sometime(NVV22(constant(S22)))])), 
always(or([not NVV21(constant(S23)), sometime(NVV22(constant(S23)))])), 
always(or([not NVV21(constant(S25)), sometime(NVV22(constant(S25)))])), 
always(or([not NVV21(constant(S33)), sometime(NVV22(constant(S33)))])), 
always(or([not NVV21(constant(S24)), sometime(NVV22(constant(S24)))])), 
always(or([not NVV21(constant(S21)), sometime(NVV22(constant(S21)))])), 
always(or([not NVV21(constant(S10)), sometime(NVV22(constant(S10)))])), 
always(or([not NVV21(constant(S3)), sometime(NVV22(constant(S3)))])), 
always(or([not NVV21(constant(S5)), sometime(NVV22(constant(S5)))])), 
always(or([not NVV21(constant(S8)), sometime(NVV22(constant(S8)))])), 
always(or([not NVV21(constant(S12)), sometime(NVV22(constant(S12)))])), 
always(or([not NVV21(constant(S7)), sometime(NVV22(constant(S7)))])), 
always(or([not NVV21(constant(S9)), sometime(NVV22(constant(S9)))])), 
always(or([not NVV21(constant(S17)), sometime(NVV22(constant(S17)))])), 
always(or([not NVV21(constant(S4)), sometime(NVV22(constant(S4)))])), 
always(or([not NVV21(constant(S19)), sometime(NVV22(constant(S19)))])), 
always(or([not NVV21(constant(S38)), sometime(NVV22(constant(S38)))])), 
always(or([not NVV21(constant(S1)), sometime(NVV22(constant(S1)))])), 
always(or([not NVV21(constant(S29)), sometime(NVV22(constant(S29)))])), 
always(or([not NVV21(constant(S27)), sometime(NVV22(constant(S27)))])), 
always(or([not NVV21(constant(S32)), sometime(NVV22(constant(S32)))])), 
always(or([not NVV21(constant(S13)), sometime(NVV22(constant(S13)))])), 
always(or([not NVV21(constant(S35)), sometime(NVV22(constant(S35)))])), 
always(or([not NVV21(constant(S30)), sometime(NVV22(constant(S30)))])), 
always(or([not NVV21(constant(S0)), sometime(NVV22(constant(S0)))])), 
always(or([not NVV21(constant(S36)), sometime(NVV22(constant(S36)))])), 
always(or([not NVV21(constant(S11)), sometime(NVV22(constant(S11)))])), 
always(or([not NVV21(constant(S20)), sometime(NVV22(constant(S20)))])), 
always(or([not NVV21(constant(S15)), sometime(NVV22(constant(S15)))])), 
always(or([not NVV21(constant(S6)), sometime(NVV22(constant(S6)))])), 
always(or([not NVV21(constant(S14)), sometime(NVV22(constant(S14)))])), 
always(or([not NVV21(constant(S37)), sometime(NVV22(constant(S37)))])), 
always(or([not NVV21(constant(S26)), sometime(NVV22(constant(S26)))])), 
always(or([not NVV21(constant(S34)), sometime(NVV22(constant(S34)))])), 
always(or([not NVV21(constant(S2)), sometime(NVV22(constant(S2)))])), 
always(or([not NVV21(constant(S16)), sometime(NVV22(constant(S16)))])), 
always(or([not NVV21(constant(S39)), sometime(NVV22(constant(S39)))])), 
always(or([not NVV21(constant(S31)), sometime(NVV22(constant(S31)))])), 
always(or([not NVV21(constant(S28)), sometime(NVV22(constant(S28)))])), 
always(or([not NVV21(constant(John)), sometime(NVV22(constant(John)))])), 
always(or([not NVV46(X), sometime(NVV47(X))])), 
always(or([not NVV46(constant(dSalary)), sometime(NVV47(constant(dSalary)))])), 
always(or([not NVV46(constant(dSalaryInv)), sometime(NVV47(constant(dSalaryInv)))])), 
always(or([not NVV46(constant(S18)), sometime(NVV47(constant(S18)))])), 
always(or([not NVV46(constant(S22)), sometime(NVV47(constant(S22)))])), 
always(or([not NVV46(constant(S23)), sometime(NVV47(constant(S23)))])), 
always(or([not NVV46(constant(S25)), sometime(NVV47(constant(S25)))])), 
always(or([not NVV46(constant(S33)), sometime(NVV47(constant(S33)))])), 
always(or([not NVV46(constant(S24)), sometime(NVV47(constant(S24)))])), 
always(or([not NVV46(constant(S21)), sometime(NVV47(constant(S21)))])), 
always(or([not NVV46(constant(S10)), sometime(NVV47(constant(S10)))])), 
always(or([not NVV46(constant(S3)), sometime(NVV47(constant(S3)))])), 
always(or([not NVV46(constant(S5)), sometime(NVV47(constant(S5)))])), 
always(or([not NVV46(constant(S8)), sometime(NVV47(constant(S8)))])), 
always(or([not NVV46(constant(S12)), sometime(NVV47(constant(S12)))])), 
always(or([not NVV46(constant(S7)), sometime(NVV47(constant(S7)))])), 
always(or([not NVV46(constant(S9)), sometime(NVV47(constant(S9)))])), 
always(or([not NVV46(constant(S17)), sometime(NVV47(constant(S17)))])), 
always(or([not NVV46(constant(S4)), sometime(NVV47(constant(S4)))])), 
always(or([not NVV46(constant(S19)), sometime(NVV47(constant(S19)))])), 
always(or([not NVV46(constant(S38)), sometime(NVV47(constant(S38)))])), 
always(or([not NVV46(constant(S1)), sometime(NVV47(constant(S1)))])), 
always(or([not NVV46(constant(S29)), sometime(NVV47(constant(S29)))])), 
always(or([not NVV46(constant(S27)), sometime(NVV47(constant(S27)))])), 
always(or([not NVV46(constant(S32)), sometime(NVV47(constant(S32)))])), 
always(or([not NVV46(constant(S13)), sometime(NVV47(constant(S13)))])), 
always(or([not NVV46(constant(S35)), sometime(NVV47(constant(S35)))])), 
always(or([not NVV46(constant(S30)), sometime(NVV47(constant(S30)))])), 
always(or([not NVV46(constant(S0)), sometime(NVV47(constant(S0)))])), 
always(or([not NVV46(constant(S36)), sometime(NVV47(constant(S36)))])), 
always(or([not NVV46(constant(S11)), sometime(NVV47(constant(S11)))])), 
always(or([not NVV46(constant(S20)), sometime(NVV47(constant(S20)))])), 
always(or([not NVV46(constant(S15)), sometime(NVV47(constant(S15)))])), 
always(or([not NVV46(constant(S6)), sometime(NVV47(constant(S6)))])), 
always(or([not NVV46(constant(S14)), sometime(NVV47(constant(S14)))])), 
always(or([not NVV46(constant(S37)), sometime(NVV47(constant(S37)))])), 
always(or([not NVV46(constant(S26)), sometime(NVV47(constant(S26)))])), 
always(or([not NVV46(constant(S34)), sometime(NVV47(constant(S34)))])), 
always(or([not NVV46(constant(S2)), sometime(NVV47(constant(S2)))])), 
always(or([not NVV46(constant(S16)), sometime(NVV47(constant(S16)))])), 
always(or([not NVV46(constant(S39)), sometime(NVV47(constant(S39)))])), 
always(or([not NVV46(constant(S31)), sometime(NVV47(constant(S31)))])), 
always(or([not NVV46(constant(S28)), sometime(NVV47(constant(S28)))])), 
always(or([not NVV46(constant(John)), sometime(NVV47(constant(John)))])), 
always(or([not NVV53(X), sometime(NVV54(X))])), 
always(or([not NVV53(constant(dSalary)), sometime(NVV54(constant(dSalary)))])), 
always(or([not NVV53(constant(dSalaryInv)), sometime(NVV54(constant(dSalaryInv)))])), 
always(or([not NVV53(constant(S18)), sometime(NVV54(constant(S18)))])), 
always(or([not NVV53(constant(S22)), sometime(NVV54(constant(S22)))])), 
always(or([not NVV53(constant(S23)), sometime(NVV54(constant(S23)))])), 
always(or([not NVV53(constant(S25)), sometime(NVV54(constant(S25)))])), 
always(or([not NVV53(constant(S33)), sometime(NVV54(constant(S33)))])), 
always(or([not NVV53(constant(S24)), sometime(NVV54(constant(S24)))])), 
always(or([not NVV53(constant(S21)), sometime(NVV54(constant(S21)))])), 
always(or([not NVV53(constant(S10)), sometime(NVV54(constant(S10)))])), 
always(or([not NVV53(constant(S3)), sometime(NVV54(constant(S3)))])), 
always(or([not NVV53(constant(S5)), sometime(NVV54(constant(S5)))])), 
always(or([not NVV53(constant(S8)), sometime(NVV54(constant(S8)))])), 
always(or([not NVV53(constant(S12)), sometime(NVV54(constant(S12)))])), 
always(or([not NVV53(constant(S7)), sometime(NVV54(constant(S7)))])), 
always(or([not NVV53(constant(S9)), sometime(NVV54(constant(S9)))])), 
always(or([not NVV53(constant(S17)), sometime(NVV54(constant(S17)))])), 
always(or([not NVV53(constant(S4)), sometime(NVV54(constant(S4)))])), 
always(or([not NVV53(constant(S19)), sometime(NVV54(constant(S19)))])), 
always(or([not NVV53(constant(S38)), sometime(NVV54(constant(S38)))])), 
always(or([not NVV53(constant(S1)), sometime(NVV54(constant(S1)))])), 
always(or([not NVV53(constant(S29)), sometime(NVV54(constant(S29)))])), 
always(or([not NVV53(constant(S27)), sometime(NVV54(constant(S27)))])), 
always(or([not NVV53(constant(S32)), sometime(NVV54(constant(S32)))])), 
always(or([not NVV53(constant(S13)), sometime(NVV54(constant(S13)))])), 
always(or([not NVV53(constant(S35)), sometime(NVV54(constant(S35)))])), 
always(or([not NVV53(constant(S30)), sometime(NVV54(constant(S30)))])), 
always(or([not NVV53(constant(S0)), sometime(NVV54(constant(S0)))])), 
always(or([not NVV53(constant(S36)), sometime(NVV54(constant(S36)))])), 
always(or([not NVV53(constant(S11)), sometime(NVV54(constant(S11)))])), 
always(or([not NVV53(constant(S20)), sometime(NVV54(constant(S20)))])), 
always(or([not NVV53(constant(S15)), sometime(NVV54(constant(S15)))])), 
always(or([not NVV53(constant(S6)), sometime(NVV54(constant(S6)))])), 
always(or([not NVV53(constant(S14)), sometime(NVV54(constant(S14)))])), 
always(or([not NVV53(constant(S37)), sometime(NVV54(constant(S37)))])), 
always(or([not NVV53(constant(S26)), sometime(NVV54(constant(S26)))])), 
always(or([not NVV53(constant(S34)), sometime(NVV54(constant(S34)))])), 
always(or([not NVV53(constant(S2)), sometime(NVV54(constant(S2)))])), 
always(or([not NVV53(constant(S16)), sometime(NVV54(constant(S16)))])), 
always(or([not NVV53(constant(S39)), sometime(NVV54(constant(S39)))])), 
always(or([not NVV53(constant(S31)), sometime(NVV54(constant(S31)))])), 
always(or([not NVV53(constant(S28)), sometime(NVV54(constant(S28)))])), 
always(or([not NVV53(constant(John)), sometime(NVV54(constant(John)))])), 
always(or([not NVV60(X), sometime(NVV61(X))])), 
always(or([not NVV60(constant(dSalary)), sometime(NVV61(constant(dSalary)))])), 
always(or([not NVV60(constant(dSalaryInv)), sometime(NVV61(constant(dSalaryInv)))])), 
always(or([not NVV60(constant(S18)), sometime(NVV61(constant(S18)))])), 
always(or([not NVV60(constant(S22)), sometime(NVV61(constant(S22)))])), 
always(or([not NVV60(constant(S23)), sometime(NVV61(constant(S23)))])), 
always(or([not NVV60(constant(S25)), sometime(NVV61(constant(S25)))])), 
always(or([not NVV60(constant(S33)), sometime(NVV61(constant(S33)))])), 
always(or([not NVV60(constant(S24)), sometime(NVV61(constant(S24)))])), 
always(or([not NVV60(constant(S21)), sometime(NVV61(constant(S21)))])), 
always(or([not NVV60(constant(S10)), sometime(NVV61(constant(S10)))])), 
always(or([not NVV60(constant(S3)), sometime(NVV61(constant(S3)))])), 
always(or([not NVV60(constant(S5)), sometime(NVV61(constant(S5)))])), 
always(or([not NVV60(constant(S8)), sometime(NVV61(constant(S8)))])), 
always(or([not NVV60(constant(S12)), sometime(NVV61(constant(S12)))])), 
always(or([not NVV60(constant(S7)), sometime(NVV61(constant(S7)))])), 
always(or([not NVV60(constant(S9)), sometime(NVV61(constant(S9)))])), 
always(or([not NVV60(constant(S17)), sometime(NVV61(constant(S17)))])), 
always(or([not NVV60(constant(S4)), sometime(NVV61(constant(S4)))])), 
always(or([not NVV60(constant(S19)), sometime(NVV61(constant(S19)))])), 
always(or([not NVV60(constant(S38)), sometime(NVV61(constant(S38)))])), 
always(or([not NVV60(constant(S1)), sometime(NVV61(constant(S1)))])), 
always(or([not NVV60(constant(S29)), sometime(NVV61(constant(S29)))])), 
always(or([not NVV60(constant(S27)), sometime(NVV61(constant(S27)))])), 
always(or([not NVV60(constant(S32)), sometime(NVV61(constant(S32)))])), 
always(or([not NVV60(constant(S13)), sometime(NVV61(constant(S13)))])), 
always(or([not NVV60(constant(S35)), sometime(NVV61(constant(S35)))])), 
always(or([not NVV60(constant(S30)), sometime(NVV61(constant(S30)))])), 
always(or([not NVV60(constant(S0)), sometime(NVV61(constant(S0)))])), 
always(or([not NVV60(constant(S36)), sometime(NVV61(constant(S36)))])), 
always(or([not NVV60(constant(S11)), sometime(NVV61(constant(S11)))])), 
always(or([not NVV60(constant(S20)), sometime(NVV61(constant(S20)))])), 
always(or([not NVV60(constant(S15)), sometime(NVV61(constant(S15)))])), 
always(or([not NVV60(constant(S6)), sometime(NVV61(constant(S6)))])), 
always(or([not NVV60(constant(S14)), sometime(NVV61(constant(S14)))])), 
always(or([not NVV60(constant(S37)), sometime(NVV61(constant(S37)))])), 
always(or([not NVV60(constant(S26)), sometime(NVV61(constant(S26)))])), 
always(or([not NVV60(constant(S34)), sometime(NVV61(constant(S34)))])), 
always(or([not NVV60(constant(S2)), sometime(NVV61(constant(S2)))])), 
always(or([not NVV60(constant(S16)), sometime(NVV61(constant(S16)))])), 
always(or([not NVV60(constant(S39)), sometime(NVV61(constant(S39)))])), 
always(or([not NVV60(constant(S31)), sometime(NVV61(constant(S31)))])), 
always(or([not NVV60(constant(S28)), sometime(NVV61(constant(S28)))])), 
always(or([not NVV60(constant(John)), sometime(NVV61(constant(John)))])), 
always(or([not NVV63(X), sometime(NVV64(X))])), 
always(or([not NVV63(constant(dSalary)), sometime(NVV64(constant(dSalary)))])), 
always(or([not NVV63(constant(dSalaryInv)), sometime(NVV64(constant(dSalaryInv)))])), 
always(or([not NVV63(constant(S18)), sometime(NVV64(constant(S18)))])), 
always(or([not NVV63(constant(S22)), sometime(NVV64(constant(S22)))])), 
always(or([not NVV63(constant(S23)), sometime(NVV64(constant(S23)))])), 
always(or([not NVV63(constant(S25)), sometime(NVV64(constant(S25)))])), 
always(or([not NVV63(constant(S33)), sometime(NVV64(constant(S33)))])), 
always(or([not NVV63(constant(S24)), sometime(NVV64(constant(S24)))])), 
always(or([not NVV63(constant(S21)), sometime(NVV64(constant(S21)))])), 
always(or([not NVV63(constant(S10)), sometime(NVV64(constant(S10)))])), 
always(or([not NVV63(constant(S3)), sometime(NVV64(constant(S3)))])), 
always(or([not NVV63(constant(S5)), sometime(NVV64(constant(S5)))])), 
always(or([not NVV63(constant(S8)), sometime(NVV64(constant(S8)))])), 
always(or([not NVV63(constant(S12)), sometime(NVV64(constant(S12)))])), 
always(or([not NVV63(constant(S7)), sometime(NVV64(constant(S7)))])), 
always(or([not NVV63(constant(S9)), sometime(NVV64(constant(S9)))])), 
always(or([not NVV63(constant(S17)), sometime(NVV64(constant(S17)))])), 
always(or([not NVV63(constant(S4)), sometime(NVV64(constant(S4)))])), 
always(or([not NVV63(constant(S19)), sometime(NVV64(constant(S19)))])), 
always(or([not NVV63(constant(S38)), sometime(NVV64(constant(S38)))])), 
always(or([not NVV63(constant(S1)), sometime(NVV64(constant(S1)))])), 
always(or([not NVV63(constant(S29)), sometime(NVV64(constant(S29)))])), 
always(or([not NVV63(constant(S27)), sometime(NVV64(constant(S27)))])), 
always(or([not NVV63(constant(S32)), sometime(NVV64(constant(S32)))])), 
always(or([not NVV63(constant(S13)), sometime(NVV64(constant(S13)))])), 
always(or([not NVV63(constant(S35)), sometime(NVV64(constant(S35)))])), 
always(or([not NVV63(constant(S30)), sometime(NVV64(constant(S30)))])), 
always(or([not NVV63(constant(S0)), sometime(NVV64(constant(S0)))])), 
always(or([not NVV63(constant(S36)), sometime(NVV64(constant(S36)))])), 
always(or([not NVV63(constant(S11)), sometime(NVV64(constant(S11)))])), 
always(or([not NVV63(constant(S20)), sometime(NVV64(constant(S20)))])), 
always(or([not NVV63(constant(S15)), sometime(NVV64(constant(S15)))])), 
always(or([not NVV63(constant(S6)), sometime(NVV64(constant(S6)))])), 
always(or([not NVV63(constant(S14)), sometime(NVV64(constant(S14)))])), 
always(or([not NVV63(constant(S37)), sometime(NVV64(constant(S37)))])), 
always(or([not NVV63(constant(S26)), sometime(NVV64(constant(S26)))])), 
always(or([not NVV63(constant(S34)), sometime(NVV64(constant(S34)))])), 
always(or([not NVV63(constant(S2)), sometime(NVV64(constant(S2)))])), 
always(or([not NVV63(constant(S16)), sometime(NVV64(constant(S16)))])), 
always(or([not NVV63(constant(S39)), sometime(NVV64(constant(S39)))])), 
always(or([not NVV63(constant(S31)), sometime(NVV64(constant(S31)))])), 
always(or([not NVV63(constant(S28)), sometime(NVV64(constant(S28)))])), 
always(or([not NVV63(constant(John)), sometime(NVV64(constant(John)))])), 
always(or([not NVV70(X), sometime(NVV71(X))])), 
always(or([not NVV70(constant(dSalary)), sometime(NVV71(constant(dSalary)))])), 
always(or([not NVV70(constant(dSalaryInv)), sometime(NVV71(constant(dSalaryInv)))])), 
always(or([not NVV70(constant(S18)), sometime(NVV71(constant(S18)))])), 
always(or([not NVV70(constant(S22)), sometime(NVV71(constant(S22)))])), 
always(or([not NVV70(constant(S23)), sometime(NVV71(constant(S23)))])), 
always(or([not NVV70(constant(S25)), sometime(NVV71(constant(S25)))])), 
always(or([not NVV70(constant(S33)), sometime(NVV71(constant(S33)))])), 
always(or([not NVV70(constant(S24)), sometime(NVV71(constant(S24)))])), 
always(or([not NVV70(constant(S21)), sometime(NVV71(constant(S21)))])), 
always(or([not NVV70(constant(S10)), sometime(NVV71(constant(S10)))])), 
always(or([not NVV70(constant(S3)), sometime(NVV71(constant(S3)))])), 
always(or([not NVV70(constant(S5)), sometime(NVV71(constant(S5)))])), 
always(or([not NVV70(constant(S8)), sometime(NVV71(constant(S8)))])), 
always(or([not NVV70(constant(S12)), sometime(NVV71(constant(S12)))])), 
always(or([not NVV70(constant(S7)), sometime(NVV71(constant(S7)))])), 
always(or([not NVV70(constant(S9)), sometime(NVV71(constant(S9)))])), 
always(or([not NVV70(constant(S17)), sometime(NVV71(constant(S17)))])), 
always(or([not NVV70(constant(S4)), sometime(NVV71(constant(S4)))])), 
always(or([not NVV70(constant(S19)), sometime(NVV71(constant(S19)))])), 
always(or([not NVV70(constant(S38)), sometime(NVV71(constant(S38)))])), 
always(or([not NVV70(constant(S1)), sometime(NVV71(constant(S1)))])), 
always(or([not NVV70(constant(S29)), sometime(NVV71(constant(S29)))])), 
always(or([not NVV70(constant(S27)), sometime(NVV71(constant(S27)))])), 
always(or([not NVV70(constant(S32)), sometime(NVV71(constant(S32)))])), 
always(or([not NVV70(constant(S13)), sometime(NVV71(constant(S13)))])), 
always(or([not NVV70(constant(S35)), sometime(NVV71(constant(S35)))])), 
always(or([not NVV70(constant(S30)), sometime(NVV71(constant(S30)))])), 
always(or([not NVV70(constant(S0)), sometime(NVV71(constant(S0)))])), 
always(or([not NVV70(constant(S36)), sometime(NVV71(constant(S36)))])), 
always(or([not NVV70(constant(S11)), sometime(NVV71(constant(S11)))])), 
always(or([not NVV70(constant(S20)), sometime(NVV71(constant(S20)))])), 
always(or([not NVV70(constant(S15)), sometime(NVV71(constant(S15)))])), 
always(or([not NVV70(constant(S6)), sometime(NVV71(constant(S6)))])), 
always(or([not NVV70(constant(S14)), sometime(NVV71(constant(S14)))])), 
always(or([not NVV70(constant(S37)), sometime(NVV71(constant(S37)))])), 
always(or([not NVV70(constant(S26)), sometime(NVV71(constant(S26)))])), 
always(or([not NVV70(constant(S34)), sometime(NVV71(constant(S34)))])), 
always(or([not NVV70(constant(S2)), sometime(NVV71(constant(S2)))])), 
always(or([not NVV70(constant(S16)), sometime(NVV71(constant(S16)))])), 
always(or([not NVV70(constant(S39)), sometime(NVV71(constant(S39)))])), 
always(or([not NVV70(constant(S31)), sometime(NVV71(constant(S31)))])), 
always(or([not NVV70(constant(S28)), sometime(NVV71(constant(S28)))])), 
always(or([not NVV70(constant(John)), sometime(NVV71(constant(John)))]))]).

