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 BOX11F(X), BOX4P(X)]), 
or([not BOX4P(X), BOX11F(X)]), 
or([not E1SalaryF(X), E1SalaryP(X)]), 
or([not E1SalaryP(X), E1SalaryF(X)]), 
or([not BOX10F(X), BOX3P(X)]), 
or([not BOX3P(X), BOX10F(X)]), 
or([not BOX2F(X), BOX19P(X)]), 
or([not BOX19P(X), BOX2F(X)]), 
or([not BOX14F(X), BOX7P(X)]), 
or([not BOX7P(X), BOX14F(X)]), 
or([not PinvSalaryF, PinvSalaryF]), 
or([not E1SalaryInvF(X), E1SalaryInvP(X)]), 
or([not E1SalaryInvP(X), E1SalaryInvF(X)]), 
or([not PSalaryF, PSalaryP]), 
or([not PSalaryP, PSalaryF]), 
or([not E1SalaryF(constant(dSalary)), E1SalaryP(constant(dSalary))]), 
or([not E1SalaryP(constant(dSalary)), E1SalaryF(constant(dSalary))]), 
or([not BOX1F(X), BOX18P(X)]), 
or([not BOX18P(X), BOX1F(X)]), 
or([not PSalaryF, PSalaryF]), 
or([not E1SalaryInvF(constant(dSalaryInv)), E1SalaryInvP(constant(dSalaryInv))]), 
or([not E1SalaryInvP(constant(dSalaryInv)), E1SalaryInvF(constant(dSalaryInv))]), 
or([not PersonF(X), PersonP(X)]), 
or([not PersonP(X), PersonF(X)]), 
or([not BOX12F(X), BOX5P(X)]), 
or([not BOX5P(X), BOX12F(X)]), 
or([not BOX0F(X), BOX17P(X)]), 
or([not BOX17P(X), BOX0F(X)]), 
or([not BOX15F(X), BOX8P(X)]), 
or([not BOX8P(X), BOX15F(X)]), 
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 PinvSalaryF, PinvSalaryP]), 
or([not PinvSalaryP, PinvSalaryF]), 
or([E1SalaryF(constant(John))]), 
or([E1SalaryInvF(constant(S1))]), 
or([PersonF(constant(John))]),
always(or([not NVV1(X), not BOX17P(X), NVV2(X)])), 
always(or([not NVV1(X), NVV3(X), BOX17P(X)])), 
always(or([not NVV1(X), not BOX15F(X), NVV5])), 
always(or([not NVV1(X), NVV6, BOX15F(X)])), 
always(or([not NVV1(X), not BOX10F(X), NVV8(X)])), 
always(or([not NVV1(X), NVV9(X), BOX10F(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), NVV17(X), BOX0F(X)])), 
always(or([not NVV1(X), NVV17(X), NVV18(X)])), 
always(or([not NVV1(X), not BOX0F(X), NVV19(X), NVV20(X)])), 
always(or([not NVV1(X), NVV21(X), BOX14F(X)])), 
always(or([not NVV1(X), NVV21(X), NVV22(X)])), 
always(or([not NVV1(X), not BOX14F(X), NVV23(X), NVV24(X)])), 
always(or([not NVV1(X), NVV25(X), BOX5P(X)])), 
always(or([not NVV1(X), NVV25(X), NVV26])), 
always(or([not NVV1(X), not BOX5P(X), NVV27, NVV28(X)])), 
always(or([not NVV1(X), NVV29(X), BOX9P(X)])), 
always(or([not NVV1(X), NVV29(X), NVV30(X)])), 
always(or([not NVV1(X), not BOX9P(X), NVV32(X), NVV34(X)])), 
always(or([not NVV1(X), not BOX16F(X), NVV35(X)])), 
always(or([not NVV1(X), NVV36(X), BOX16F(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), not BOX12F(X), NVV45])), 
always(or([not NVV1(X), NVV46, BOX12F(X)])), 
always(or([not NVV1(X), not BOX7P(X), NVV48(X)])), 
always(or([not NVV1(X), NVV49(X), BOX7P(X)])), 
always(or([not NVV1(X), NVV51(X), BOX8P(X)])), 
always(or([not NVV1(X), NVV51(X), NVV52])), 
always(or([not NVV1(X), not BOX8P(X), NVV53, NVV54(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 BOX13F(X), NVV59(X)])), 
always(or([not NVV1(X), NVV60(X), BOX13F(X)])), 
always(or([not NVV1(X), not BOX19P(X), NVV62(X)])), 
always(or([not NVV1(X), NVV63(X), BOX19P(X)])), 
always(or([not NVV1(X), NVV65(X), BOX3P(X)])), 
always(or([not NVV1(X), NVV65(X), NVV66(X)])), 
always(or([not NVV1(X), not BOX3P(X), NVV68(X), NVV70(X)])), 
always(or([not NVV1(X), not BOX4P(X), NVV71(X)])), 
always(or([not NVV1(X), NVV72(X), BOX4P(X)])), 
always(or([not NVV1(X), NVV74(X), BOX11F(X)])), 
always(or([not NVV1(X), NVV74(X), NVV75(X)])), 
always(or([not NVV1(X), not BOX11F(X), NVV76(X), NVV77(X)])), 
always(or([not NVV2(X), BOX3P(X)])), 
always(or([not NVV4(X), not BOX3P(X)])), 
always(or([not NVV5, PSalaryF])), 
always(or([not NVV7, not PSalaryF])), 
always(or([not NVV8(X), not E1SalaryInvF(X), BOX11F(X)])), 
always(or([not NVV10(X), E1SalaryInvF(X)])), 
always(or([not NVV10(X), not BOX11F(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 NVV31(X), not PersonP(X), E1SalaryP(X)])), 
always(or([not NVV31(X), not PersonP(X), not E2SalaryP(X)])), 
always(or([not NVV31(X), not E2SalaryP(X), E1SalaryP(X)])), 
always(or([not NVV33(X), not E1SalaryP(X), PersonP(X), E2SalaryP(X)])), 
always(or([not NVV33(X), PersonP(X), E2SalaryP(X)])), 
always(or([not NVV33(X), not E1SalaryP(X), E2SalaryP(X)])), 
always(or([not NVV33(X), PersonP(X), not E1SalaryP(X)])), 
always(or([not NVV33(X), PersonP(X), E2SalaryP(X), not E1SalaryP(X)])), 
always(or([not NVV33(X), E2SalaryP(X), not E1SalaryP(X)])), 
always(or([not NVV35(X), not PersonF(X), E1SalaryF(X)])), 
always(or([not NVV35(X), not PersonF(X), not E2SalaryF(X)])), 
always(or([not NVV35(X), not E2SalaryF(X), E1SalaryF(X)])), 
always(or([not NVV37(X), not E1SalaryF(X), PersonF(X), E2SalaryF(X)])), 
always(or([not NVV37(X), PersonF(X), E2SalaryF(X)])), 
always(or([not NVV37(X), not E1SalaryF(X), E2SalaryF(X)])), 
always(or([not NVV37(X), PersonF(X), not E1SalaryF(X)])), 
always(or([not NVV37(X), PersonF(X), E2SalaryF(X), not E1SalaryF(X)])), 
always(or([not NVV37(X), E2SalaryF(X), not E1SalaryF(X)])), 
always(or([not NVV42(X), BOX6P(X)])), 
always(or([not NVV44(X), not BOX6P(X)])), 
always(or([not NVV45, PinvSalaryF])), 
always(or([not NVV47, not PinvSalaryF])), 
always(or([not NVV48(X), BOX8P(X)])), 
always(or([not NVV50(X), not BOX8P(X)])), 
always(or([not NVV59(X), not E1SalaryF(X), BOX14F(X)])), 
always(or([not NVV61(X), E1SalaryF(X)])), 
always(or([not NVV61(X), not BOX14F(X)])), 
always(or([not NVV62(X), BOX9P(X)])), 
always(or([not NVV64(X), not BOX9P(X)])), 
always(or([not NVV67(X), not E1SalaryInvP(X), BOX4P(X)])), 
always(or([not NVV69(X), E1SalaryInvP(X)])), 
always(or([not NVV69(X), not BOX4P(X)])), 
always(or([not NVV71(X), BOX5P(X)])), 
always(or([not NVV73(X), not BOX5P(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, next(NVV5)])), 
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(X), next(not BOX0F(hidden(X)))])), 
always(or([not NVV17(constant(X)), next(not BOX0F(constant(X)))])), 
always(or([not NVV18(X), next(BOX10F(hidden(X)))])), 
always(or([not NVV18(constant(X)), next(BOX10F(constant(X)))])), 
always(or([not NVV19(X), next(not BOX10F(hidden(X)))])), 
always(or([not NVV19(constant(X)), next(not BOX10F(constant(X)))])), 
always(or([not NVV20(X), next(BOX0F(hidden(X)))])), 
always(or([not NVV20(constant(X)), next(BOX0F(constant(X)))])), 
always(or([not NVV21(X), next(not BOX14F(hidden(X)))])), 
always(or([not NVV21(constant(X)), next(not BOX14F(constant(X)))])), 
always(or([not NVV22(X), next(BOX15F(hidden(X)))])), 
always(or([not NVV22(constant(X)), next(BOX15F(constant(X)))])), 
always(or([not NVV23(X), next(not BOX15F(hidden(X)))])), 
always(or([not NVV23(constant(X)), next(not BOX15F(constant(X)))])), 
always(or([not NVV24(X), next(BOX14F(hidden(X)))])), 
always(or([not NVV24(constant(X)), next(BOX14F(constant(X)))])), 
always(or([not NVV25(X), next(not BOX5P(hidden(X)))])), 
always(or([not NVV25(constant(X)), next(not BOX5P(constant(X)))])), 
always(or([not NVV26, next(PinvSalaryF)])), 
always(or([not NVV27, next(not PinvSalaryF)])), 
always(or([not NVV28(X), next(BOX5P(hidden(X)))])), 
always(or([not NVV28(constant(X)), next(BOX5P(constant(X)))])), 
always(or([not NVV29(X), next(not BOX9P(hidden(X)))])), 
always(or([not NVV29(constant(X)), next(not BOX9P(constant(X)))])), 
always(or([not NVV30(X), next(NVV31(hidden(X)))])), 
always(or([not NVV30(constant(X)), next(NVV31(constant(X)))])), 
always(or([not NVV32(X), next(NVV33(hidden(X)))])), 
always(or([not NVV32(constant(X)), next(NVV33(constant(X)))])), 
always(or([not NVV34(X), next(BOX9P(hidden(X)))])), 
always(or([not NVV34(constant(X)), next(BOX9P(constant(X)))])), 
always(or([not NVV35(X), next(NVV35(hidden(X)))])), 
always(or([not NVV35(constant(X)), next(NVV35(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, 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 BOX8P(hidden(X)))])), 
always(or([not NVV51(constant(X)), next(not BOX8P(constant(X)))])), 
always(or([not NVV52, next(PSalaryF)])), 
always(or([not NVV53, next(not PSalaryF)])), 
always(or([not NVV54(X), next(BOX8P(hidden(X)))])), 
always(or([not NVV54(constant(X)), next(BOX8P(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 BOX3P(hidden(X)))])), 
always(or([not NVV65(constant(X)), next(not BOX3P(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(BOX3P(hidden(X)))])), 
always(or([not NVV70(constant(X)), next(BOX3P(constant(X)))])), 
always(or([not NVV71(X), next(NVV71(hidden(X)))])), 
always(or([not NVV71(constant(X)), next(NVV71(constant(X)))])), 
always(or([not NVV74(X), next(not BOX11F(hidden(X)))])), 
always(or([not NVV74(constant(X)), next(not BOX11F(constant(X)))])), 
always(or([not NVV75(X), next(BOX12F(hidden(X)))])), 
always(or([not NVV75(constant(X)), next(BOX12F(constant(X)))])), 
always(or([not NVV76(X), next(not BOX12F(hidden(X)))])), 
always(or([not NVV76(constant(X)), next(not BOX12F(constant(X)))])), 
always(or([not NVV77(X), next(BOX11F(hidden(X)))])), 
always(or([not NVV77(constant(X)), next(BOX11F(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(S1)), sometime(NVV4(constant(S1)))])), 
always(or([not NVV3(constant(John)), sometime(NVV4(constant(John)))])), 
always(or([not NVV6, sometime(NVV7)])), 
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(S1)), sometime(NVV10(constant(S1)))])), 
always(or([not NVV9(constant(John)), sometime(NVV10(constant(John)))])), 
always(or([not NVV36(X), sometime(NVV37(X))])), 
always(or([not NVV36(constant(dSalary)), sometime(NVV37(constant(dSalary)))])), 
always(or([not NVV36(constant(dSalaryInv)), sometime(NVV37(constant(dSalaryInv)))])), 
always(or([not NVV36(constant(S1)), sometime(NVV37(constant(S1)))])), 
always(or([not NVV36(constant(John)), sometime(NVV37(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(S1)), sometime(NVV44(constant(S1)))])), 
always(or([not NVV43(constant(John)), sometime(NVV44(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(S1)), sometime(NVV50(constant(S1)))])), 
always(or([not NVV49(constant(John)), sometime(NVV50(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(S1)), sometime(NVV61(constant(S1)))])), 
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(S1)), sometime(NVV64(constant(S1)))])), 
always(or([not NVV63(constant(John)), sometime(NVV64(constant(John)))])), 
always(or([not NVV72(X), sometime(NVV73(X))])), 
always(or([not NVV72(constant(dSalary)), sometime(NVV73(constant(dSalary)))])), 
always(or([not NVV72(constant(dSalaryInv)), sometime(NVV73(constant(dSalaryInv)))])), 
always(or([not NVV72(constant(S1)), sometime(NVV73(constant(S1)))])), 
always(or([not NVV72(constant(John)), sometime(NVV73(constant(John)))]))]).

