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

