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([NVV78]), 
or([NVV85]), 
or([NVV102]), 
or([NVV123]), 
or([NVV127]), 
or([NVV125]), 
or([NVV154]), 
or([NVV169]), 
or([NVV87]), 
or([NVV188]), 
or([NVV203]), 
or([NVV226]), 
or([NVV231]), 
or([NVV248]), 
or([NVV257]), 
or([NVV263]), 
or([NVV268]), 
or([NVV293]), 
or([NVV314]), 
or([NVV331]), 
or([E1SalaryInvF(constant(S2))]), 
or([E1SalaryInvF(constant(S1))]), 
or([NVV344]), 
or([NVV363]), 
or([NVV388]), 
or([PersonF(constant(John))]), 
or([NVV411]), 
or([NVV420]), 
or([NVV259]), 
or([NVV261]), 
or([NVV421]), 
or([NVV434]), 
or([NVV93]), 
or([NVV437]), 
or([NVV97]), 
or([NVV444]), 
or([E2SalaryF(constant(John))]), 
or([NVV455]), 
or([NVV91]), 
or([NVV458]), 
or([NVV95]), 
or([NVV101]), 
or([NVV469]), 
or([NVV89]), 
or([NVV99]), 
or([NVV496]),
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 NVV79, NVV80])), 
always(or([not NVV81, NVV82])), 
always(or([not NVV83, NVV84])), 
always(or([not NVV86, NVV87])), 
always(or([not NVV88, NVV89])), 
always(or([not NVV90, NVV91])), 
always(or([not NVV92, NVV93])), 
always(or([not NVV94, NVV95])), 
always(or([not NVV96, NVV97])), 
always(or([not NVV98, NVV99])), 
always(or([not NVV100, NVV101])), 
always(or([not NVV103, NVV104])), 
always(or([not NVV105, NVV106])), 
always(or([not NVV107, NVV108])), 
always(or([not NVV109, NVV110])), 
always(or([not NVV111, NVV112])), 
always(or([not NVV113, NVV114])), 
always(or([not NVV115, NVV116])), 
always(or([not NVV117, NVV118])), 
always(or([not NVV119, NVV120])), 
always(or([not NVV121, NVV122])), 
always(or([not NVV124, NVV125])), 
always(or([not NVV126, NVV85])), 
always(or([not NVV128, NVV129])), 
always(or([not NVV130, NVV131])), 
always(or([not NVV132, NVV133])), 
always(or([not NVV134, NVV135])), 
always(or([not NVV136, NVV137])), 
always(or([not NVV138, NVV139])), 
always(or([not NVV140, NVV141])), 
always(or([not NVV142, NVV143])), 
always(or([not NVV144, NVV145])), 
always(or([not NVV146, NVV147])), 
always(or([not NVV148, NVV149])), 
always(or([not NVV150, NVV151])), 
always(or([not NVV152, NVV153])), 
always(or([not NVV155, NVV156])), 
always(or([not NVV157, NVV158])), 
always(or([not NVV159, NVV160])), 
always(or([not NVV161, NVV162])), 
always(or([not NVV163, NVV164])), 
always(or([not NVV165, NVV166])), 
always(or([not NVV167, NVV168])), 
always(or([not NVV170, NVV171])), 
always(or([not NVV172, NVV173])), 
always(or([not NVV174, NVV175])), 
always(or([not NVV176, NVV177])), 
always(or([not NVV178, NVV179])), 
always(or([not NVV180, NVV181])), 
always(or([not NVV182, NVV183])), 
always(or([not NVV184, NVV185])), 
always(or([not NVV186, NVV187])), 
always(or([not NVV189, NVV190])), 
always(or([not NVV191, NVV192])), 
always(or([not NVV193, NVV194])), 
always(or([not NVV195, NVV196])), 
always(or([not NVV197, NVV198])), 
always(or([not NVV199, NVV200])), 
always(or([not NVV201, NVV202])), 
always(or([not NVV204, NVV205])), 
always(or([not NVV206, NVV207])), 
always(or([not NVV208, NVV209])), 
always(or([not NVV210, NVV211])), 
always(or([not NVV212, NVV213])), 
always(or([not NVV214, NVV215])), 
always(or([not NVV216, NVV217])), 
always(or([not NVV218, NVV219])), 
always(or([not NVV220, NVV221])), 
always(or([not NVV222, NVV223])), 
always(or([not NVV224, NVV225])), 
always(or([not NVV227, NVV228])), 
always(or([not NVV229, NVV230])), 
always(or([not NVV232, NVV233])), 
always(or([not NVV234, NVV235])), 
always(or([not NVV236, NVV237])), 
always(or([not NVV238, NVV239])), 
always(or([not NVV240, NVV241])), 
always(or([not NVV242, NVV243])), 
always(or([not NVV244, NVV245])), 
always(or([not NVV246, NVV247])), 
always(or([not NVV249, NVV250])), 
always(or([not NVV251, NVV252])), 
always(or([not NVV253, NVV254])), 
always(or([not NVV255, NVV256])), 
always(or([not NVV258, NVV259])), 
always(or([not NVV260, NVV261])), 
always(or([not NVV262, NVV123])), 
always(or([not NVV264, NVV265])), 
always(or([not NVV266, NVV267])), 
always(or([not NVV269, NVV270])), 
always(or([not NVV271, NVV272])), 
always(or([not NVV273, NVV274])), 
always(or([not NVV275, NVV276])), 
always(or([not NVV277, NVV278])), 
always(or([not NVV279, NVV280])), 
always(or([not NVV281, NVV282])), 
always(or([not NVV283, NVV284])), 
always(or([not NVV285, NVV286])), 
always(or([not NVV287, NVV288])), 
always(or([not NVV289, NVV290])), 
always(or([not NVV291, NVV292])), 
always(or([not NVV294, NVV295])), 
always(or([not NVV296, NVV297])), 
always(or([not NVV298, NVV299])), 
always(or([not NVV300, NVV301])), 
always(or([not NVV302, NVV303])), 
always(or([not NVV304, NVV305])), 
always(or([not NVV306, NVV307])), 
always(or([not NVV308, NVV309])), 
always(or([not NVV310, NVV311])), 
always(or([not NVV312, NVV313])), 
always(or([not NVV315, NVV316])), 
always(or([not NVV317, NVV318])), 
always(or([not NVV319, NVV320])), 
always(or([not NVV321, NVV322])), 
always(or([not NVV323, NVV324])), 
always(or([not NVV325, NVV326])), 
always(or([not NVV327, NVV328])), 
always(or([not NVV329, NVV330])), 
always(or([not NVV332, NVV333])), 
always(or([not NVV334, NVV335])), 
always(or([not NVV336, NVV337])), 
always(or([not NVV338, NVV339])), 
always(or([not NVV340, NVV341])), 
always(or([not NVV342, NVV343])), 
always(or([not NVV345, NVV346])), 
always(or([not NVV347, NVV348])), 
always(or([not NVV349, NVV350])), 
always(or([not NVV351, NVV352])), 
always(or([not NVV353, NVV354])), 
always(or([not NVV355, NVV356])), 
always(or([not NVV357, NVV358])), 
always(or([not NVV359, NVV360])), 
always(or([not NVV361, NVV362])), 
always(or([not NVV364, NVV365])), 
always(or([not NVV366, NVV367])), 
always(or([not NVV368, NVV369])), 
always(or([not NVV370, NVV371])), 
always(or([not NVV372, NVV373])), 
always(or([not NVV374, NVV375])), 
always(or([not NVV376, NVV377])), 
always(or([not NVV378, NVV379])), 
always(or([not NVV380, NVV381])), 
always(or([not NVV382, NVV383])), 
always(or([not NVV384, NVV385])), 
always(or([not NVV386, NVV387])), 
always(or([not NVV389, NVV390])), 
always(or([not NVV391, NVV392])), 
always(or([not NVV393, NVV394])), 
always(or([not NVV395, NVV396])), 
always(or([not NVV397, NVV398])), 
always(or([not NVV399, NVV400])), 
always(or([not NVV401, NVV402])), 
always(or([not NVV403, NVV404])), 
always(or([not NVV405, NVV406])), 
always(or([not NVV407, NVV408])), 
always(or([not NVV409, NVV410])), 
always(or([not NVV412, NVV413])), 
always(or([not NVV414, NVV415])), 
always(or([not NVV416, NVV417])), 
always(or([not NVV418, NVV419])), 
always(or([not NVV422, NVV423])), 
always(or([not NVV424, NVV425])), 
always(or([not NVV426, NVV427])), 
always(or([not NVV428, NVV429])), 
always(or([not NVV430, NVV431])), 
always(or([not NVV432, NVV433])), 
always(or([not NVV435, NVV436])), 
always(or([not NVV438, NVV439])), 
always(or([not NVV440, NVV441])), 
always(or([not NVV442, NVV443])), 
always(or([not NVV445, NVV446])), 
always(or([not NVV447, NVV448])), 
always(or([not NVV449, NVV450])), 
always(or([not NVV451, NVV452])), 
always(or([not NVV453, NVV454])), 
always(or([not NVV456, NVV457])), 
always(or([not NVV459, NVV460])), 
always(or([not NVV461, NVV462])), 
always(or([not NVV463, NVV464])), 
always(or([not NVV465, NVV466])), 
always(or([not NVV467, NVV468])), 
always(or([not NVV470, NVV471])), 
always(or([not NVV472, NVV473])), 
always(or([not NVV474, NVV475])), 
always(or([not NVV476, NVV477])), 
always(or([not NVV478, NVV479])), 
always(or([not NVV480, NVV481])), 
always(or([not NVV482, NVV483])), 
always(or([not NVV484, NVV485])), 
always(or([not NVV486, NVV487])), 
always(or([not NVV488, NVV489])), 
always(or([not NVV490, NVV491])), 
always(or([not NVV492, NVV493])), 
always(or([not NVV494, NVV495])),
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 NVV78, next(NVV79)])), 
always(or([not NVV80, next(NVV81)])), 
always(or([not NVV82, next(NVV83)])), 
always(or([not NVV84, next(E1SalaryInvF(S10))])), 
always(or([not NVV85, next(NVV86)])), 
always(or([not NVV87, next(NVV88)])), 
always(or([not NVV89, next(NVV90)])), 
always(or([not NVV91, next(NVV92)])), 
always(or([not NVV93, next(NVV94)])), 
always(or([not NVV95, next(NVV96)])), 
always(or([not NVV97, next(NVV98)])), 
always(or([not NVV99, next(NVV100)])), 
always(or([not NVV101, next(E2SalaryF(John))])), 
always(or([not NVV102, next(NVV103)])), 
always(or([not NVV104, next(NVV105)])), 
always(or([not NVV106, next(NVV107)])), 
always(or([not NVV108, next(NVV109)])), 
always(or([not NVV110, next(NVV111)])), 
always(or([not NVV112, next(NVV113)])), 
always(or([not NVV114, next(NVV115)])), 
always(or([not NVV116, next(NVV117)])), 
always(or([not NVV118, next(NVV119)])), 
always(or([not NVV120, next(NVV121)])), 
always(or([not NVV122, next(E1SalaryInvF(S23))])), 
always(or([not NVV123, next(NVV124)])), 
always(or([not NVV125, next(NVV126)])), 
always(or([not NVV127, next(NVV128)])), 
always(or([not NVV129, next(NVV130)])), 
always(or([not NVV131, next(NVV132)])), 
always(or([not NVV133, next(NVV134)])), 
always(or([not NVV135, next(NVV136)])), 
always(or([not NVV137, next(NVV138)])), 
always(or([not NVV139, next(NVV140)])), 
always(or([not NVV141, next(NVV142)])), 
always(or([not NVV143, next(NVV144)])), 
always(or([not NVV145, next(NVV146)])), 
always(or([not NVV147, next(NVV148)])), 
always(or([not NVV149, next(NVV150)])), 
always(or([not NVV151, next(NVV152)])), 
always(or([not NVV153, next(E1SalaryInvF(S29))])), 
always(or([not NVV154, next(NVV155)])), 
always(or([not NVV156, next(NVV157)])), 
always(or([not NVV158, next(NVV159)])), 
always(or([not NVV160, next(NVV161)])), 
always(or([not NVV162, next(NVV163)])), 
always(or([not NVV164, next(NVV165)])), 
always(or([not NVV166, next(NVV167)])), 
always(or([not NVV168, next(E1SalaryInvF(S18))])), 
always(or([not NVV169, next(NVV170)])), 
always(or([not NVV171, next(NVV172)])), 
always(or([not NVV173, next(NVV174)])), 
always(or([not NVV175, next(NVV176)])), 
always(or([not NVV177, next(NVV178)])), 
always(or([not NVV179, next(NVV180)])), 
always(or([not NVV181, next(NVV182)])), 
always(or([not NVV183, next(NVV184)])), 
always(or([not NVV185, next(NVV186)])), 
always(or([not NVV187, next(E1SalaryInvF(S22))])), 
always(or([not NVV188, next(NVV189)])), 
always(or([not NVV190, next(NVV191)])), 
always(or([not NVV192, next(NVV193)])), 
always(or([not NVV194, next(NVV195)])), 
always(or([not NVV196, next(NVV197)])), 
always(or([not NVV198, next(NVV199)])), 
always(or([not NVV200, next(NVV201)])), 
always(or([not NVV202, next(E1SalaryInvF(S17))])), 
always(or([not NVV203, next(NVV204)])), 
always(or([not NVV205, next(NVV206)])), 
always(or([not NVV207, next(NVV208)])), 
always(or([not NVV209, next(NVV210)])), 
always(or([not NVV211, next(NVV212)])), 
always(or([not NVV213, next(NVV214)])), 
always(or([not NVV215, next(NVV216)])), 
always(or([not NVV217, next(NVV218)])), 
always(or([not NVV219, next(NVV220)])), 
always(or([not NVV221, next(NVV222)])), 
always(or([not NVV223, next(NVV224)])), 
always(or([not NVV225, next(E1SalaryInvF(S26))])), 
always(or([not NVV226, next(NVV227)])), 
always(or([not NVV228, next(NVV229)])), 
always(or([not NVV230, next(E1SalaryInvF(S7))])), 
always(or([not NVV231, next(NVV232)])), 
always(or([not NVV233, next(NVV234)])), 
always(or([not NVV235, next(NVV236)])), 
always(or([not NVV237, next(NVV238)])), 
always(or([not NVV239, next(NVV240)])), 
always(or([not NVV241, next(NVV242)])), 
always(or([not NVV243, next(NVV244)])), 
always(or([not NVV245, next(NVV246)])), 
always(or([not NVV247, next(E1SalaryInvF(S19))])), 
always(or([not NVV248, next(NVV249)])), 
always(or([not NVV250, next(NVV251)])), 
always(or([not NVV252, next(NVV253)])), 
always(or([not NVV254, next(NVV255)])), 
always(or([not NVV256, next(E1SalaryInvF(S11))])), 
always(or([not NVV257, next(NVV258)])), 
always(or([not NVV259, next(NVV260)])), 
always(or([not NVV261, next(NVV262)])), 
always(or([not NVV263, next(NVV264)])), 
always(or([not NVV265, next(NVV266)])), 
always(or([not NVV267, next(E1SalaryInvF(S8))])), 
always(or([not NVV268, next(NVV269)])), 
always(or([not NVV270, next(NVV271)])), 
always(or([not NVV272, next(NVV273)])), 
always(or([not NVV274, next(NVV275)])), 
always(or([not NVV276, next(NVV277)])), 
always(or([not NVV278, next(NVV279)])), 
always(or([not NVV280, next(NVV281)])), 
always(or([not NVV282, next(NVV283)])), 
always(or([not NVV284, next(NVV285)])), 
always(or([not NVV286, next(NVV287)])), 
always(or([not NVV288, next(NVV289)])), 
always(or([not NVV290, next(NVV291)])), 
always(or([not NVV292, next(E1SalaryInvF(S27))])), 
always(or([not NVV293, next(NVV294)])), 
always(or([not NVV295, next(NVV296)])), 
always(or([not NVV297, next(NVV298)])), 
always(or([not NVV299, next(NVV300)])), 
always(or([not NVV301, next(NVV302)])), 
always(or([not NVV303, next(NVV304)])), 
always(or([not NVV305, next(NVV306)])), 
always(or([not NVV307, next(NVV308)])), 
always(or([not NVV309, next(NVV310)])), 
always(or([not NVV311, next(NVV312)])), 
always(or([not NVV313, next(E1SalaryInvF(S24))])), 
always(or([not NVV314, next(NVV315)])), 
always(or([not NVV316, next(NVV317)])), 
always(or([not NVV318, next(NVV319)])), 
always(or([not NVV320, next(NVV321)])), 
always(or([not NVV322, next(NVV323)])), 
always(or([not NVV324, next(NVV325)])), 
always(or([not NVV326, next(NVV327)])), 
always(or([not NVV328, next(NVV329)])), 
always(or([not NVV330, next(E1SalaryInvF(S20))])), 
always(or([not NVV331, next(NVV332)])), 
always(or([not NVV333, next(NVV334)])), 
always(or([not NVV335, next(NVV336)])), 
always(or([not NVV337, next(NVV338)])), 
always(or([not NVV339, next(NVV340)])), 
always(or([not NVV341, next(NVV342)])), 
always(or([not NVV343, next(E1SalaryInvF(S15))])), 
always(or([not NVV344, next(NVV345)])), 
always(or([not NVV346, next(NVV347)])), 
always(or([not NVV348, next(NVV349)])), 
always(or([not NVV350, next(NVV351)])), 
always(or([not NVV352, next(NVV353)])), 
always(or([not NVV354, next(NVV355)])), 
always(or([not NVV356, next(NVV357)])), 
always(or([not NVV358, next(NVV359)])), 
always(or([not NVV360, next(NVV361)])), 
always(or([not NVV362, next(E1SalaryInvF(S21))])), 
always(or([not NVV363, next(NVV364)])), 
always(or([not NVV365, next(NVV366)])), 
always(or([not NVV367, next(NVV368)])), 
always(or([not NVV369, next(NVV370)])), 
always(or([not NVV371, next(NVV372)])), 
always(or([not NVV373, next(NVV374)])), 
always(or([not NVV375, next(NVV376)])), 
always(or([not NVV377, next(NVV378)])), 
always(or([not NVV379, next(NVV380)])), 
always(or([not NVV381, next(NVV382)])), 
always(or([not NVV383, next(NVV384)])), 
always(or([not NVV385, next(NVV386)])), 
always(or([not NVV387, next(E1SalaryInvF(S28))])), 
always(or([not NVV388, next(NVV389)])), 
always(or([not NVV390, next(NVV391)])), 
always(or([not NVV392, next(NVV393)])), 
always(or([not NVV394, next(NVV395)])), 
always(or([not NVV396, next(NVV397)])), 
always(or([not NVV398, next(NVV399)])), 
always(or([not NVV400, next(NVV401)])), 
always(or([not NVV402, next(NVV403)])), 
always(or([not NVV404, next(NVV405)])), 
always(or([not NVV406, next(NVV407)])), 
always(or([not NVV408, next(NVV409)])), 
always(or([not NVV410, next(E1SalaryInvF(S25))])), 
always(or([not NVV411, next(NVV412)])), 
always(or([not NVV413, next(NVV414)])), 
always(or([not NVV415, next(NVV416)])), 
always(or([not NVV417, next(NVV418)])), 
always(or([not NVV419, next(E1SalaryInvF(S12))])), 
always(or([not NVV420, next(E1SalaryInvF(S3))])), 
always(or([not NVV421, next(NVV422)])), 
always(or([not NVV423, next(NVV424)])), 
always(or([not NVV425, next(NVV426)])), 
always(or([not NVV427, next(NVV428)])), 
always(or([not NVV429, next(NVV430)])), 
always(or([not NVV431, next(NVV432)])), 
always(or([not NVV433, next(E1SalaryInvF(S16))])), 
always(or([not NVV434, next(NVV435)])), 
always(or([not NVV436, next(E1SalaryInvF(S6))])), 
always(or([not NVV437, next(NVV438)])), 
always(or([not NVV439, next(NVV440)])), 
always(or([not NVV441, next(NVV442)])), 
always(or([not NVV443, next(E1SalaryInvF(S9))])), 
always(or([not NVV444, next(NVV445)])), 
always(or([not NVV446, next(NVV447)])), 
always(or([not NVV448, next(NVV449)])), 
always(or([not NVV450, next(NVV451)])), 
always(or([not NVV452, next(NVV453)])), 
always(or([not NVV454, next(E1SalaryInvF(S14))])), 
always(or([not NVV455, next(NVV456)])), 
always(or([not NVV457, next(E1SalaryInvF(S5))])), 
always(or([not NVV458, next(NVV459)])), 
always(or([not NVV460, next(NVV461)])), 
always(or([not NVV462, next(NVV463)])), 
always(or([not NVV464, next(NVV465)])), 
always(or([not NVV466, next(NVV467)])), 
always(or([not NVV468, next(E1SalaryInvF(S13))])), 
always(or([not NVV469, next(NVV470)])), 
always(or([not NVV471, next(NVV472)])), 
always(or([not NVV473, next(NVV474)])), 
always(or([not NVV475, next(NVV476)])), 
always(or([not NVV477, next(NVV478)])), 
always(or([not NVV479, next(NVV480)])), 
always(or([not NVV481, next(NVV482)])), 
always(or([not NVV483, next(NVV484)])), 
always(or([not NVV485, next(NVV486)])), 
always(or([not NVV487, next(NVV488)])), 
always(or([not NVV489, next(NVV490)])), 
always(or([not NVV491, next(NVV492)])), 
always(or([not NVV493, next(NVV494)])), 
always(or([not NVV495, next(E1SalaryInvF(S30))])), 
always(or([not NVV496, next(E1SalaryInvF(S4))])),
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(S23)), sometime(NVV4(constant(S23)))])), 
always(or([not NVV3(constant(S29)), sometime(NVV4(constant(S29)))])), 
always(or([not NVV3(constant(S18)), sometime(NVV4(constant(S18)))])), 
always(or([not NVV3(constant(S22)), sometime(NVV4(constant(S22)))])), 
always(or([not NVV3(constant(S17)), sometime(NVV4(constant(S17)))])), 
always(or([not NVV3(constant(S26)), sometime(NVV4(constant(S26)))])), 
always(or([not NVV3(constant(S7)), sometime(NVV4(constant(S7)))])), 
always(or([not NVV3(constant(S19)), sometime(NVV4(constant(S19)))])), 
always(or([not NVV3(constant(S11)), sometime(NVV4(constant(S11)))])), 
always(or([not NVV3(constant(S8)), sometime(NVV4(constant(S8)))])), 
always(or([not NVV3(constant(S27)), sometime(NVV4(constant(S27)))])), 
always(or([not NVV3(constant(S24)), sometime(NVV4(constant(S24)))])), 
always(or([not NVV3(constant(S20)), sometime(NVV4(constant(S20)))])), 
always(or([not NVV3(constant(S15)), sometime(NVV4(constant(S15)))])), 
always(or([not NVV3(constant(S2)), sometime(NVV4(constant(S2)))])), 
always(or([not NVV3(constant(S1)), sometime(NVV4(constant(S1)))])), 
always(or([not NVV3(constant(S21)), sometime(NVV4(constant(S21)))])), 
always(or([not NVV3(constant(S28)), sometime(NVV4(constant(S28)))])), 
always(or([not NVV3(constant(S25)), sometime(NVV4(constant(S25)))])), 
always(or([not NVV3(constant(S12)), sometime(NVV4(constant(S12)))])), 
always(or([not NVV3(constant(S3)), sometime(NVV4(constant(S3)))])), 
always(or([not NVV3(constant(S16)), sometime(NVV4(constant(S16)))])), 
always(or([not NVV3(constant(S6)), sometime(NVV4(constant(S6)))])), 
always(or([not NVV3(constant(S9)), sometime(NVV4(constant(S9)))])), 
always(or([not NVV3(constant(S14)), sometime(NVV4(constant(S14)))])), 
always(or([not NVV3(constant(S5)), sometime(NVV4(constant(S5)))])), 
always(or([not NVV3(constant(S13)), sometime(NVV4(constant(S13)))])), 
always(or([not NVV3(constant(S30)), sometime(NVV4(constant(S30)))])), 
always(or([not NVV3(constant(John)), sometime(NVV4(constant(John)))])), 
always(or([not NVV3(constant(S4)), sometime(NVV4(constant(S4)))])), 
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(S23)), sometime(NVV7(constant(S23)))])), 
always(or([not NVV6(constant(S29)), sometime(NVV7(constant(S29)))])), 
always(or([not NVV6(constant(S18)), sometime(NVV7(constant(S18)))])), 
always(or([not NVV6(constant(S22)), sometime(NVV7(constant(S22)))])), 
always(or([not NVV6(constant(S17)), sometime(NVV7(constant(S17)))])), 
always(or([not NVV6(constant(S26)), sometime(NVV7(constant(S26)))])), 
always(or([not NVV6(constant(S7)), sometime(NVV7(constant(S7)))])), 
always(or([not NVV6(constant(S19)), sometime(NVV7(constant(S19)))])), 
always(or([not NVV6(constant(S11)), sometime(NVV7(constant(S11)))])), 
always(or([not NVV6(constant(S8)), sometime(NVV7(constant(S8)))])), 
always(or([not NVV6(constant(S27)), sometime(NVV7(constant(S27)))])), 
always(or([not NVV6(constant(S24)), sometime(NVV7(constant(S24)))])), 
always(or([not NVV6(constant(S20)), sometime(NVV7(constant(S20)))])), 
always(or([not NVV6(constant(S15)), sometime(NVV7(constant(S15)))])), 
always(or([not NVV6(constant(S2)), sometime(NVV7(constant(S2)))])), 
always(or([not NVV6(constant(S1)), sometime(NVV7(constant(S1)))])), 
always(or([not NVV6(constant(S21)), sometime(NVV7(constant(S21)))])), 
always(or([not NVV6(constant(S28)), sometime(NVV7(constant(S28)))])), 
always(or([not NVV6(constant(S25)), sometime(NVV7(constant(S25)))])), 
always(or([not NVV6(constant(S12)), sometime(NVV7(constant(S12)))])), 
always(or([not NVV6(constant(S3)), sometime(NVV7(constant(S3)))])), 
always(or([not NVV6(constant(S16)), sometime(NVV7(constant(S16)))])), 
always(or([not NVV6(constant(S6)), sometime(NVV7(constant(S6)))])), 
always(or([not NVV6(constant(S9)), sometime(NVV7(constant(S9)))])), 
always(or([not NVV6(constant(S14)), sometime(NVV7(constant(S14)))])), 
always(or([not NVV6(constant(S5)), sometime(NVV7(constant(S5)))])), 
always(or([not NVV6(constant(S13)), sometime(NVV7(constant(S13)))])), 
always(or([not NVV6(constant(S30)), sometime(NVV7(constant(S30)))])), 
always(or([not NVV6(constant(John)), sometime(NVV7(constant(John)))])), 
always(or([not NVV6(constant(S4)), sometime(NVV7(constant(S4)))])), 
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(S23)), sometime(NVV20(constant(S23)))])), 
always(or([not NVV19(constant(S29)), sometime(NVV20(constant(S29)))])), 
always(or([not NVV19(constant(S18)), sometime(NVV20(constant(S18)))])), 
always(or([not NVV19(constant(S22)), sometime(NVV20(constant(S22)))])), 
always(or([not NVV19(constant(S17)), sometime(NVV20(constant(S17)))])), 
always(or([not NVV19(constant(S26)), sometime(NVV20(constant(S26)))])), 
always(or([not NVV19(constant(S7)), sometime(NVV20(constant(S7)))])), 
always(or([not NVV19(constant(S19)), sometime(NVV20(constant(S19)))])), 
always(or([not NVV19(constant(S11)), sometime(NVV20(constant(S11)))])), 
always(or([not NVV19(constant(S8)), sometime(NVV20(constant(S8)))])), 
always(or([not NVV19(constant(S27)), sometime(NVV20(constant(S27)))])), 
always(or([not NVV19(constant(S24)), sometime(NVV20(constant(S24)))])), 
always(or([not NVV19(constant(S20)), sometime(NVV20(constant(S20)))])), 
always(or([not NVV19(constant(S15)), sometime(NVV20(constant(S15)))])), 
always(or([not NVV19(constant(S2)), sometime(NVV20(constant(S2)))])), 
always(or([not NVV19(constant(S1)), sometime(NVV20(constant(S1)))])), 
always(or([not NVV19(constant(S21)), sometime(NVV20(constant(S21)))])), 
always(or([not NVV19(constant(S28)), sometime(NVV20(constant(S28)))])), 
always(or([not NVV19(constant(S25)), sometime(NVV20(constant(S25)))])), 
always(or([not NVV19(constant(S12)), sometime(NVV20(constant(S12)))])), 
always(or([not NVV19(constant(S3)), sometime(NVV20(constant(S3)))])), 
always(or([not NVV19(constant(S16)), sometime(NVV20(constant(S16)))])), 
always(or([not NVV19(constant(S6)), sometime(NVV20(constant(S6)))])), 
always(or([not NVV19(constant(S9)), sometime(NVV20(constant(S9)))])), 
always(or([not NVV19(constant(S14)), sometime(NVV20(constant(S14)))])), 
always(or([not NVV19(constant(S5)), sometime(NVV20(constant(S5)))])), 
always(or([not NVV19(constant(S13)), sometime(NVV20(constant(S13)))])), 
always(or([not NVV19(constant(S30)), sometime(NVV20(constant(S30)))])), 
always(or([not NVV19(constant(John)), sometime(NVV20(constant(John)))])), 
always(or([not NVV19(constant(S4)), sometime(NVV20(constant(S4)))])), 
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(S23)), sometime(NVV33(constant(S23)))])), 
always(or([not NVV32(constant(S29)), sometime(NVV33(constant(S29)))])), 
always(or([not NVV32(constant(S18)), sometime(NVV33(constant(S18)))])), 
always(or([not NVV32(constant(S22)), sometime(NVV33(constant(S22)))])), 
always(or([not NVV32(constant(S17)), sometime(NVV33(constant(S17)))])), 
always(or([not NVV32(constant(S26)), sometime(NVV33(constant(S26)))])), 
always(or([not NVV32(constant(S7)), sometime(NVV33(constant(S7)))])), 
always(or([not NVV32(constant(S19)), sometime(NVV33(constant(S19)))])), 
always(or([not NVV32(constant(S11)), sometime(NVV33(constant(S11)))])), 
always(or([not NVV32(constant(S8)), sometime(NVV33(constant(S8)))])), 
always(or([not NVV32(constant(S27)), sometime(NVV33(constant(S27)))])), 
always(or([not NVV32(constant(S24)), sometime(NVV33(constant(S24)))])), 
always(or([not NVV32(constant(S20)), sometime(NVV33(constant(S20)))])), 
always(or([not NVV32(constant(S15)), sometime(NVV33(constant(S15)))])), 
always(or([not NVV32(constant(S2)), sometime(NVV33(constant(S2)))])), 
always(or([not NVV32(constant(S1)), sometime(NVV33(constant(S1)))])), 
always(or([not NVV32(constant(S21)), sometime(NVV33(constant(S21)))])), 
always(or([not NVV32(constant(S28)), sometime(NVV33(constant(S28)))])), 
always(or([not NVV32(constant(S25)), sometime(NVV33(constant(S25)))])), 
always(or([not NVV32(constant(S12)), sometime(NVV33(constant(S12)))])), 
always(or([not NVV32(constant(S3)), sometime(NVV33(constant(S3)))])), 
always(or([not NVV32(constant(S16)), sometime(NVV33(constant(S16)))])), 
always(or([not NVV32(constant(S6)), sometime(NVV33(constant(S6)))])), 
always(or([not NVV32(constant(S9)), sometime(NVV33(constant(S9)))])), 
always(or([not NVV32(constant(S14)), sometime(NVV33(constant(S14)))])), 
always(or([not NVV32(constant(S5)), sometime(NVV33(constant(S5)))])), 
always(or([not NVV32(constant(S13)), sometime(NVV33(constant(S13)))])), 
always(or([not NVV32(constant(S30)), sometime(NVV33(constant(S30)))])), 
always(or([not NVV32(constant(John)), sometime(NVV33(constant(John)))])), 
always(or([not NVV32(constant(S4)), sometime(NVV33(constant(S4)))])), 
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(S23)), sometime(NVV36(constant(S23)))])), 
always(or([not NVV35(constant(S29)), sometime(NVV36(constant(S29)))])), 
always(or([not NVV35(constant(S18)), sometime(NVV36(constant(S18)))])), 
always(or([not NVV35(constant(S22)), sometime(NVV36(constant(S22)))])), 
always(or([not NVV35(constant(S17)), sometime(NVV36(constant(S17)))])), 
always(or([not NVV35(constant(S26)), sometime(NVV36(constant(S26)))])), 
always(or([not NVV35(constant(S7)), sometime(NVV36(constant(S7)))])), 
always(or([not NVV35(constant(S19)), sometime(NVV36(constant(S19)))])), 
always(or([not NVV35(constant(S11)), sometime(NVV36(constant(S11)))])), 
always(or([not NVV35(constant(S8)), sometime(NVV36(constant(S8)))])), 
always(or([not NVV35(constant(S27)), sometime(NVV36(constant(S27)))])), 
always(or([not NVV35(constant(S24)), sometime(NVV36(constant(S24)))])), 
always(or([not NVV35(constant(S20)), sometime(NVV36(constant(S20)))])), 
always(or([not NVV35(constant(S15)), sometime(NVV36(constant(S15)))])), 
always(or([not NVV35(constant(S2)), sometime(NVV36(constant(S2)))])), 
always(or([not NVV35(constant(S1)), sometime(NVV36(constant(S1)))])), 
always(or([not NVV35(constant(S21)), sometime(NVV36(constant(S21)))])), 
always(or([not NVV35(constant(S28)), sometime(NVV36(constant(S28)))])), 
always(or([not NVV35(constant(S25)), sometime(NVV36(constant(S25)))])), 
always(or([not NVV35(constant(S12)), sometime(NVV36(constant(S12)))])), 
always(or([not NVV35(constant(S3)), sometime(NVV36(constant(S3)))])), 
always(or([not NVV35(constant(S16)), sometime(NVV36(constant(S16)))])), 
always(or([not NVV35(constant(S6)), sometime(NVV36(constant(S6)))])), 
always(or([not NVV35(constant(S9)), sometime(NVV36(constant(S9)))])), 
always(or([not NVV35(constant(S14)), sometime(NVV36(constant(S14)))])), 
always(or([not NVV35(constant(S5)), sometime(NVV36(constant(S5)))])), 
always(or([not NVV35(constant(S13)), sometime(NVV36(constant(S13)))])), 
always(or([not NVV35(constant(S30)), sometime(NVV36(constant(S30)))])), 
always(or([not NVV35(constant(John)), sometime(NVV36(constant(John)))])), 
always(or([not NVV35(constant(S4)), sometime(NVV36(constant(S4)))])), 
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(S23)), sometime(NVV50(constant(S23)))])), 
always(or([not NVV49(constant(S29)), sometime(NVV50(constant(S29)))])), 
always(or([not NVV49(constant(S18)), sometime(NVV50(constant(S18)))])), 
always(or([not NVV49(constant(S22)), sometime(NVV50(constant(S22)))])), 
always(or([not NVV49(constant(S17)), sometime(NVV50(constant(S17)))])), 
always(or([not NVV49(constant(S26)), sometime(NVV50(constant(S26)))])), 
always(or([not NVV49(constant(S7)), sometime(NVV50(constant(S7)))])), 
always(or([not NVV49(constant(S19)), sometime(NVV50(constant(S19)))])), 
always(or([not NVV49(constant(S11)), sometime(NVV50(constant(S11)))])), 
always(or([not NVV49(constant(S8)), sometime(NVV50(constant(S8)))])), 
always(or([not NVV49(constant(S27)), sometime(NVV50(constant(S27)))])), 
always(or([not NVV49(constant(S24)), sometime(NVV50(constant(S24)))])), 
always(or([not NVV49(constant(S20)), sometime(NVV50(constant(S20)))])), 
always(or([not NVV49(constant(S15)), sometime(NVV50(constant(S15)))])), 
always(or([not NVV49(constant(S2)), sometime(NVV50(constant(S2)))])), 
always(or([not NVV49(constant(S1)), sometime(NVV50(constant(S1)))])), 
always(or([not NVV49(constant(S21)), sometime(NVV50(constant(S21)))])), 
always(or([not NVV49(constant(S28)), sometime(NVV50(constant(S28)))])), 
always(or([not NVV49(constant(S25)), sometime(NVV50(constant(S25)))])), 
always(or([not NVV49(constant(S12)), sometime(NVV50(constant(S12)))])), 
always(or([not NVV49(constant(S3)), sometime(NVV50(constant(S3)))])), 
always(or([not NVV49(constant(S16)), sometime(NVV50(constant(S16)))])), 
always(or([not NVV49(constant(S6)), sometime(NVV50(constant(S6)))])), 
always(or([not NVV49(constant(S9)), sometime(NVV50(constant(S9)))])), 
always(or([not NVV49(constant(S14)), sometime(NVV50(constant(S14)))])), 
always(or([not NVV49(constant(S5)), sometime(NVV50(constant(S5)))])), 
always(or([not NVV49(constant(S13)), sometime(NVV50(constant(S13)))])), 
always(or([not NVV49(constant(S30)), sometime(NVV50(constant(S30)))])), 
always(or([not NVV49(constant(John)), sometime(NVV50(constant(John)))])), 
always(or([not NVV49(constant(S4)), sometime(NVV50(constant(S4)))])), 
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(S23)), sometime(NVV63(constant(S23)))])), 
always(or([not NVV62(constant(S29)), sometime(NVV63(constant(S29)))])), 
always(or([not NVV62(constant(S18)), sometime(NVV63(constant(S18)))])), 
always(or([not NVV62(constant(S22)), sometime(NVV63(constant(S22)))])), 
always(or([not NVV62(constant(S17)), sometime(NVV63(constant(S17)))])), 
always(or([not NVV62(constant(S26)), sometime(NVV63(constant(S26)))])), 
always(or([not NVV62(constant(S7)), sometime(NVV63(constant(S7)))])), 
always(or([not NVV62(constant(S19)), sometime(NVV63(constant(S19)))])), 
always(or([not NVV62(constant(S11)), sometime(NVV63(constant(S11)))])), 
always(or([not NVV62(constant(S8)), sometime(NVV63(constant(S8)))])), 
always(or([not NVV62(constant(S27)), sometime(NVV63(constant(S27)))])), 
always(or([not NVV62(constant(S24)), sometime(NVV63(constant(S24)))])), 
always(or([not NVV62(constant(S20)), sometime(NVV63(constant(S20)))])), 
always(or([not NVV62(constant(S15)), sometime(NVV63(constant(S15)))])), 
always(or([not NVV62(constant(S2)), sometime(NVV63(constant(S2)))])), 
always(or([not NVV62(constant(S1)), sometime(NVV63(constant(S1)))])), 
always(or([not NVV62(constant(S21)), sometime(NVV63(constant(S21)))])), 
always(or([not NVV62(constant(S28)), sometime(NVV63(constant(S28)))])), 
always(or([not NVV62(constant(S25)), sometime(NVV63(constant(S25)))])), 
always(or([not NVV62(constant(S12)), sometime(NVV63(constant(S12)))])), 
always(or([not NVV62(constant(S3)), sometime(NVV63(constant(S3)))])), 
always(or([not NVV62(constant(S16)), sometime(NVV63(constant(S16)))])), 
always(or([not NVV62(constant(S6)), sometime(NVV63(constant(S6)))])), 
always(or([not NVV62(constant(S9)), sometime(NVV63(constant(S9)))])), 
always(or([not NVV62(constant(S14)), sometime(NVV63(constant(S14)))])), 
always(or([not NVV62(constant(S5)), sometime(NVV63(constant(S5)))])), 
always(or([not NVV62(constant(S13)), sometime(NVV63(constant(S13)))])), 
always(or([not NVV62(constant(S30)), sometime(NVV63(constant(S30)))])), 
always(or([not NVV62(constant(John)), sometime(NVV63(constant(John)))])), 
always(or([not NVV62(constant(S4)), sometime(NVV63(constant(S4)))])), 
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(S23)), sometime(NVV66(constant(S23)))])), 
always(or([not NVV65(constant(S29)), sometime(NVV66(constant(S29)))])), 
always(or([not NVV65(constant(S18)), sometime(NVV66(constant(S18)))])), 
always(or([not NVV65(constant(S22)), sometime(NVV66(constant(S22)))])), 
always(or([not NVV65(constant(S17)), sometime(NVV66(constant(S17)))])), 
always(or([not NVV65(constant(S26)), sometime(NVV66(constant(S26)))])), 
always(or([not NVV65(constant(S7)), sometime(NVV66(constant(S7)))])), 
always(or([not NVV65(constant(S19)), sometime(NVV66(constant(S19)))])), 
always(or([not NVV65(constant(S11)), sometime(NVV66(constant(S11)))])), 
always(or([not NVV65(constant(S8)), sometime(NVV66(constant(S8)))])), 
always(or([not NVV65(constant(S27)), sometime(NVV66(constant(S27)))])), 
always(or([not NVV65(constant(S24)), sometime(NVV66(constant(S24)))])), 
always(or([not NVV65(constant(S20)), sometime(NVV66(constant(S20)))])), 
always(or([not NVV65(constant(S15)), sometime(NVV66(constant(S15)))])), 
always(or([not NVV65(constant(S2)), sometime(NVV66(constant(S2)))])), 
always(or([not NVV65(constant(S1)), sometime(NVV66(constant(S1)))])), 
always(or([not NVV65(constant(S21)), sometime(NVV66(constant(S21)))])), 
always(or([not NVV65(constant(S28)), sometime(NVV66(constant(S28)))])), 
always(or([not NVV65(constant(S25)), sometime(NVV66(constant(S25)))])), 
always(or([not NVV65(constant(S12)), sometime(NVV66(constant(S12)))])), 
always(or([not NVV65(constant(S3)), sometime(NVV66(constant(S3)))])), 
always(or([not NVV65(constant(S16)), sometime(NVV66(constant(S16)))])), 
always(or([not NVV65(constant(S6)), sometime(NVV66(constant(S6)))])), 
always(or([not NVV65(constant(S9)), sometime(NVV66(constant(S9)))])), 
always(or([not NVV65(constant(S14)), sometime(NVV66(constant(S14)))])), 
always(or([not NVV65(constant(S5)), sometime(NVV66(constant(S5)))])), 
always(or([not NVV65(constant(S13)), sometime(NVV66(constant(S13)))])), 
always(or([not NVV65(constant(S30)), sometime(NVV66(constant(S30)))])), 
always(or([not NVV65(constant(John)), sometime(NVV66(constant(John)))])), 
always(or([not NVV65(constant(S4)), sometime(NVV66(constant(S4)))])), 
always(or([not NVV68, sometime(NVV69)]))]).

