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

