and([
or([BOX2F(X)]), 
or([not PSalaryF, E1SalaryInvF(constant(dSalaryInv))]), 
or([BOX0F(X)]), 
or([BOX1F(X)]), 
or([not PinvSalaryF, E1SalaryF(constant(dSalary))]), 
or([NVV1(X)]), 
or([not BOX12F(X), BOX5P(X)]), 
or([not BOX5P(X), BOX12F(X)]), 
or([not BOX13F(X), BOX6P(X)]), 
or([not BOX6P(X), BOX13F(X)]), 
or([not BOX15F(X), BOX8P(X)]), 
or([not BOX8P(X), BOX15F(X)]), 
or([not BOX2F(X), BOX19P(X)]), 
or([not BOX19P(X), BOX2F(X)]), 
or([not BOX0F(X), BOX17P(X)]), 
or([not BOX17P(X), BOX0F(X)]), 
or([not E1SalaryF(X), E1SalaryP(X)]), 
or([not E1SalaryP(X), E1SalaryF(X)]), 
or([not E2SalaryF(X), E2SalaryP(X)]), 
or([not E2SalaryP(X), E2SalaryF(X)]), 
or([not BOX10F(X), BOX3P(X)]), 
or([not BOX3P(X), BOX10F(X)]), 
or([not PersonF(X), PersonP(X)]), 
or([not PersonP(X), PersonF(X)]), 
or([not BOX1F(X), BOX18P(X)]), 
or([not BOX18P(X), BOX1F(X)]), 
or([not E1SalaryF(constant(dSalary)), E1SalaryP(constant(dSalary))]), 
or([not E1SalaryP(constant(dSalary)), E1SalaryF(constant(dSalary))]), 
or([not BOX11F(X), BOX4P(X)]), 
or([not BOX4P(X), BOX11F(X)]), 
or([not BOX14F(X), BOX7P(X)]), 
or([not BOX7P(X), BOX14F(X)]), 
or([not PSalaryF, PSalaryP]), 
or([not PSalaryP, PSalaryF]), 
or([not BOX16F(X), BOX9P(X)]), 
or([not BOX9P(X), BOX16F(X)]), 
or([not PinvSalaryF, PinvSalaryP]), 
or([not PinvSalaryP, PinvSalaryF]), 
or([not E1SalaryInvF(X), E1SalaryInvP(X)]), 
or([not E1SalaryInvP(X), E1SalaryInvF(X)]), 
or([not PSalaryF, PSalaryF]), 
or([not PinvSalaryF, PinvSalaryF]), 
or([not E1SalaryInvF(constant(dSalaryInv)), E1SalaryInvP(constant(dSalaryInv))]), 
or([not E1SalaryInvP(constant(dSalaryInv)), E1SalaryInvF(constant(dSalaryInv))]), 
or([NVV78]), 
or([NVV81]), 
or([NVV92]), 
or([NVV102]), 
or([NVV112]), 
or([NVV121]), 
or([NVV127]), 
or([NVV140]), 
or([NVV159]), 
or([NVV123]), 
or([NVV184]), 
or([NVV205]), 
or([NVV104]), 
or([NVV220]), 
or([NVV249]), 
or([NVV284]), 
or([NVV321]), 
or([NVV98]), 
or([NVV110]), 
or([E2SalaryF(constant(John))]), 
or([NVV358]), 
or([NVV361]), 
or([NVV372]), 
or([NVV106]), 
or([NVV381]), 
or([NVV385]), 
or([NVV400]), 
or([NVV402]), 
or([NVV435]), 
or([NVV440]), 
or([NVV465]), 
or([NVV94]), 
or([NVV472]), 
or([NVV499]), 
or([NVV501]), 
or([NVV518]), 
or([NVV537]), 
or([NVV540]), 
or([NVV561]), 
or([NVV562]), 
or([NVV597]), 
or([NVV602]), 
or([NVV603]), 
or([E1SalaryInvF(constant(S1))]), 
or([E1SalaryInvF(constant(S2))]), 
or([NVV632]), 
or([PersonF(constant(John))]), 
or([NVV639]), 
or([NVV383]), 
or([NVV96]), 
or([NVV656]), 
or([NVV108]), 
or([NVV689]), 
or([NVV720]), 
or([NVV743]), 
or([NVV766]), 
or([NVV125]), 
or([NVV80]), 
or([NVV100]), 
or([NVV797]), 
or([NVV810]),
always(or([not NVV1(X), not BOX12F(X), NVV2])), 
always(or([not NVV1(X), NVV3, BOX12F(X)])), 
always(or([not NVV1(X), not BOX17P(X), NVV5(X)])), 
always(or([not NVV1(X), NVV6(X), BOX17P(X)])), 
always(or([not NVV1(X), not BOX13F(X), NVV8(X)])), 
always(or([not NVV1(X), NVV9(X), BOX13F(X)])), 
always(or([not NVV1(X), NVV11(X), BOX6P(X)])), 
always(or([not NVV1(X), NVV11(X), NVV12(X)])), 
always(or([not NVV1(X), not BOX6P(X), NVV14(X), NVV16(X)])), 
always(or([not NVV1(X), not BOX15F(X), NVV17])), 
always(or([not NVV1(X), NVV18, BOX15F(X)])), 
always(or([not NVV1(X), not BOX18P(X), NVV20(X)])), 
always(or([not NVV1(X), NVV21(X), BOX18P(X)])), 
always(or([not NVV1(X), NVV23(X), BOX0F(X)])), 
always(or([not NVV1(X), NVV23(X), NVV24(X)])), 
always(or([not NVV1(X), not BOX0F(X), NVV25(X), NVV26(X)])), 
always(or([not NVV1(X), NVV27(X), BOX5P(X)])), 
always(or([not NVV1(X), NVV27(X), NVV28])), 
always(or([not NVV1(X), not BOX5P(X), NVV29, NVV30(X)])), 
always(or([not NVV1(X), NVV31(X), BOX14F(X)])), 
always(or([not NVV1(X), NVV31(X), NVV32(X)])), 
always(or([not NVV1(X), not BOX14F(X), NVV33(X), NVV34(X)])), 
always(or([not NVV1(X), NVV35(X), BOX3P(X)])), 
always(or([not NVV1(X), NVV35(X), NVV36(X)])), 
always(or([not NVV1(X), not BOX3P(X), NVV38(X), NVV40(X)])), 
always(or([not NVV1(X), NVV41(X), BOX11F(X)])), 
always(or([not NVV1(X), NVV41(X), NVV42(X)])), 
always(or([not NVV1(X), not BOX11F(X), NVV43(X), NVV44(X)])), 
always(or([not NVV1(X), not BOX16F(X), NVV45(X)])), 
always(or([not NVV1(X), NVV46(X), BOX16F(X)])), 
always(or([not NVV1(X), NVV48(X), BOX8P(X)])), 
always(or([not NVV1(X), NVV48(X), NVV49])), 
always(or([not NVV1(X), not BOX8P(X), NVV50, NVV51(X)])), 
always(or([not NVV1(X), not BOX10F(X), NVV52(X)])), 
always(or([not NVV1(X), NVV53(X), BOX10F(X)])), 
always(or([not NVV1(X), NVV55(X), BOX1F(X)])), 
always(or([not NVV1(X), NVV55(X), NVV56(X)])), 
always(or([not NVV1(X), not BOX1F(X), NVV57(X), NVV58(X)])), 
always(or([not NVV1(X), not BOX4P(X), NVV59(X)])), 
always(or([not NVV1(X), NVV60(X), BOX4P(X)])), 
always(or([not NVV1(X), not BOX7P(X), NVV62(X)])), 
always(or([not NVV1(X), NVV63(X), BOX7P(X)])), 
always(or([not NVV1(X), NVV65(X), BOX2F(X)])), 
always(or([not NVV1(X), NVV65(X), NVV66(X)])), 
always(or([not NVV1(X), not BOX2F(X), NVV67(X), NVV68(X)])), 
always(or([not NVV1(X), not BOX19P(X), NVV69(X)])), 
always(or([not NVV1(X), NVV70(X), BOX19P(X)])), 
always(or([not NVV1(X), NVV72(X), BOX9P(X)])), 
always(or([not NVV1(X), NVV72(X), NVV73(X)])), 
always(or([not NVV1(X), not BOX9P(X), NVV75(X), NVV77(X)])), 
always(or([not NVV2, PinvSalaryF])), 
always(or([not NVV4, not PinvSalaryF])), 
always(or([not NVV5(X), BOX3P(X)])), 
always(or([not NVV7(X), not BOX3P(X)])), 
always(or([not NVV8(X), not E1SalaryF(X), BOX14F(X)])), 
always(or([not NVV10(X), E1SalaryF(X)])), 
always(or([not NVV10(X), not BOX14F(X)])), 
always(or([not NVV13(X), not E1SalaryP(X), BOX7P(X)])), 
always(or([not NVV15(X), E1SalaryP(X)])), 
always(or([not NVV15(X), not BOX7P(X)])), 
always(or([not NVV17, PSalaryF])), 
always(or([not NVV19, not PSalaryF])), 
always(or([not NVV20(X), BOX6P(X)])), 
always(or([not NVV22(X), not BOX6P(X)])), 
always(or([not NVV37(X), not E1SalaryInvP(X), BOX4P(X)])), 
always(or([not NVV39(X), E1SalaryInvP(X)])), 
always(or([not NVV39(X), not BOX4P(X)])), 
always(or([not NVV45(X), not PersonF(X), E1SalaryF(X)])), 
always(or([not NVV45(X), not PersonF(X), not E2SalaryF(X)])), 
always(or([not NVV45(X), not E2SalaryF(X), E1SalaryF(X)])), 
always(or([not NVV47(X), not E1SalaryF(X), PersonF(X), E2SalaryF(X)])), 
always(or([not NVV47(X), PersonF(X), E2SalaryF(X)])), 
always(or([not NVV47(X), not E1SalaryF(X), E2SalaryF(X)])), 
always(or([not NVV47(X), PersonF(X), not E1SalaryF(X)])), 
always(or([not NVV47(X), PersonF(X), E2SalaryF(X), not E1SalaryF(X)])), 
always(or([not NVV47(X), E2SalaryF(X), not E1SalaryF(X)])), 
always(or([not NVV52(X), not E1SalaryInvF(X), BOX11F(X)])), 
always(or([not NVV54(X), E1SalaryInvF(X)])), 
always(or([not NVV54(X), not BOX11F(X)])), 
always(or([not NVV59(X), BOX5P(X)])), 
always(or([not NVV61(X), not BOX5P(X)])), 
always(or([not NVV62(X), BOX8P(X)])), 
always(or([not NVV64(X), not BOX8P(X)])), 
always(or([not NVV69(X), BOX9P(X)])), 
always(or([not NVV71(X), not BOX9P(X)])), 
always(or([not NVV74(X), not PersonP(X), E1SalaryP(X)])), 
always(or([not NVV74(X), not PersonP(X), not E2SalaryP(X)])), 
always(or([not NVV74(X), not E2SalaryP(X), E1SalaryP(X)])), 
always(or([not NVV76(X), not E1SalaryP(X), PersonP(X), E2SalaryP(X)])), 
always(or([not NVV76(X), PersonP(X), E2SalaryP(X)])), 
always(or([not NVV76(X), not E1SalaryP(X), E2SalaryP(X)])), 
always(or([not NVV76(X), PersonP(X), not E1SalaryP(X)])), 
always(or([not NVV76(X), PersonP(X), E2SalaryP(X), not E1SalaryP(X)])), 
always(or([not NVV76(X), E2SalaryP(X), not E1SalaryP(X)])), 
always(or([not NVV79, NVV80])), 
always(or([not NVV82, NVV83])), 
always(or([not NVV84, NVV85])), 
always(or([not NVV86, NVV87])), 
always(or([not NVV88, NVV89])), 
always(or([not NVV90, NVV91])), 
always(or([not NVV93, NVV94])), 
always(or([not NVV95, NVV96])), 
always(or([not NVV97, NVV98])), 
always(or([not NVV99, NVV100])), 
always(or([not NVV101, NVV78])), 
always(or([not NVV103, NVV104])), 
always(or([not NVV105, NVV106])), 
always(or([not NVV107, NVV108])), 
always(or([not NVV109, NVV110])), 
always(or([not NVV111, NVV92])), 
always(or([not NVV113, NVV114])), 
always(or([not NVV115, NVV116])), 
always(or([not NVV117, NVV118])), 
always(or([not NVV119, NVV120])), 
always(or([not NVV122, NVV123])), 
always(or([not NVV124, NVV125])), 
always(or([not NVV126, NVV102])), 
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 NVV141, NVV142])), 
always(or([not NVV143, NVV144])), 
always(or([not NVV145, NVV146])), 
always(or([not NVV147, NVV148])), 
always(or([not NVV149, NVV150])), 
always(or([not NVV151, NVV152])), 
always(or([not NVV153, NVV154])), 
always(or([not NVV155, NVV156])), 
always(or([not NVV157, NVV158])), 
always(or([not NVV160, NVV161])), 
always(or([not NVV162, NVV163])), 
always(or([not NVV164, NVV165])), 
always(or([not NVV166, NVV167])), 
always(or([not NVV168, NVV169])), 
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 NVV185, NVV186])), 
always(or([not NVV187, NVV188])), 
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 NVV203, NVV204])), 
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 NVV221, NVV222])), 
always(or([not NVV223, NVV224])), 
always(or([not NVV225, NVV226])), 
always(or([not NVV227, NVV228])), 
always(or([not NVV229, NVV230])), 
always(or([not NVV231, NVV232])), 
always(or([not NVV233, NVV234])), 
always(or([not NVV235, NVV236])), 
always(or([not NVV237, NVV238])), 
always(or([not NVV239, NVV240])), 
always(or([not NVV241, NVV242])), 
always(or([not NVV243, NVV244])), 
always(or([not NVV245, NVV246])), 
always(or([not NVV247, NVV248])), 
always(or([not NVV250, NVV251])), 
always(or([not NVV252, NVV253])), 
always(or([not NVV254, NVV255])), 
always(or([not NVV256, NVV257])), 
always(or([not NVV258, NVV259])), 
always(or([not NVV260, NVV261])), 
always(or([not NVV262, NVV263])), 
always(or([not NVV264, NVV265])), 
always(or([not NVV266, NVV267])), 
always(or([not NVV268, NVV269])), 
always(or([not NVV270, NVV271])), 
always(or([not NVV272, NVV273])), 
always(or([not NVV274, NVV275])), 
always(or([not NVV276, NVV277])), 
always(or([not NVV278, NVV279])), 
always(or([not NVV280, NVV281])), 
always(or([not NVV282, NVV283])), 
always(or([not NVV285, NVV286])), 
always(or([not NVV287, NVV288])), 
always(or([not NVV289, NVV290])), 
always(or([not NVV291, NVV292])), 
always(or([not NVV293, NVV294])), 
always(or([not NVV295, NVV296])), 
always(or([not NVV297, NVV298])), 
always(or([not NVV299, NVV300])), 
always(or([not NVV301, NVV302])), 
always(or([not NVV303, NVV304])), 
always(or([not NVV305, NVV306])), 
always(or([not NVV307, NVV308])), 
always(or([not NVV309, NVV310])), 
always(or([not NVV311, NVV312])), 
always(or([not NVV313, NVV314])), 
always(or([not NVV315, NVV316])), 
always(or([not NVV317, NVV318])), 
always(or([not NVV319, NVV320])), 
always(or([not NVV322, NVV323])), 
always(or([not NVV324, NVV325])), 
always(or([not NVV326, NVV327])), 
always(or([not NVV328, NVV329])), 
always(or([not NVV330, NVV331])), 
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 NVV344, NVV345])), 
always(or([not NVV346, NVV347])), 
always(or([not NVV348, NVV349])), 
always(or([not NVV350, NVV351])), 
always(or([not NVV352, NVV353])), 
always(or([not NVV354, NVV355])), 
always(or([not NVV356, NVV357])), 
always(or([not NVV359, NVV360])), 
always(or([not NVV362, NVV363])), 
always(or([not NVV364, NVV365])), 
always(or([not NVV366, NVV367])), 
always(or([not NVV368, NVV369])), 
always(or([not NVV370, NVV371])), 
always(or([not NVV373, NVV374])), 
always(or([not NVV375, NVV376])), 
always(or([not NVV377, NVV378])), 
always(or([not NVV379, NVV380])), 
always(or([not NVV382, NVV383])), 
always(or([not NVV384, NVV121])), 
always(or([not NVV386, NVV387])), 
always(or([not NVV388, NVV389])), 
always(or([not NVV390, NVV391])), 
always(or([not NVV392, NVV393])), 
always(or([not NVV394, NVV395])), 
always(or([not NVV396, NVV397])), 
always(or([not NVV398, NVV399])), 
always(or([not NVV401, NVV381])), 
always(or([not NVV403, NVV404])), 
always(or([not NVV405, NVV406])), 
always(or([not NVV407, NVV408])), 
always(or([not NVV409, NVV410])), 
always(or([not NVV411, NVV412])), 
always(or([not NVV413, NVV414])), 
always(or([not NVV415, NVV416])), 
always(or([not NVV417, NVV418])), 
always(or([not NVV419, NVV420])), 
always(or([not NVV421, NVV422])), 
always(or([not NVV423, NVV424])), 
always(or([not NVV425, NVV426])), 
always(or([not NVV427, NVV428])), 
always(or([not NVV429, NVV430])), 
always(or([not NVV431, NVV432])), 
always(or([not NVV433, NVV434])), 
always(or([not NVV436, NVV437])), 
always(or([not NVV438, NVV439])), 
always(or([not NVV441, NVV442])), 
always(or([not NVV443, NVV444])), 
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 NVV455, NVV456])), 
always(or([not NVV457, NVV458])), 
always(or([not NVV459, NVV460])), 
always(or([not NVV461, NVV462])), 
always(or([not NVV463, NVV464])), 
always(or([not NVV466, NVV467])), 
always(or([not NVV468, NVV469])), 
always(or([not NVV470, NVV471])), 
always(or([not NVV473, NVV474])), 
always(or([not NVV475, NVV476])), 
always(or([not NVV477, NVV478])), 
always(or([not NVV479, NVV480])), 
always(or([not NVV481, NVV482])), 
always(or([not NVV483, NVV484])), 
always(or([not NVV485, NVV486])), 
always(or([not NVV487, NVV488])), 
always(or([not NVV489, NVV490])), 
always(or([not NVV491, NVV492])), 
always(or([not NVV493, NVV494])), 
always(or([not NVV495, NVV496])), 
always(or([not NVV497, NVV498])), 
always(or([not NVV500, NVV400])), 
always(or([not NVV502, NVV503])), 
always(or([not NVV504, NVV505])), 
always(or([not NVV506, NVV507])), 
always(or([not NVV508, NVV509])), 
always(or([not NVV510, NVV511])), 
always(or([not NVV512, NVV513])), 
always(or([not NVV514, NVV515])), 
always(or([not NVV516, NVV517])), 
always(or([not NVV519, NVV520])), 
always(or([not NVV521, NVV522])), 
always(or([not NVV523, NVV524])), 
always(or([not NVV525, NVV526])), 
always(or([not NVV527, NVV528])), 
always(or([not NVV529, NVV530])), 
always(or([not NVV531, NVV532])), 
always(or([not NVV533, NVV534])), 
always(or([not NVV535, NVV536])), 
always(or([not NVV538, NVV539])), 
always(or([not NVV541, NVV542])), 
always(or([not NVV543, NVV544])), 
always(or([not NVV545, NVV546])), 
always(or([not NVV547, NVV548])), 
always(or([not NVV549, NVV550])), 
always(or([not NVV551, NVV552])), 
always(or([not NVV553, NVV554])), 
always(or([not NVV555, NVV556])), 
always(or([not NVV557, NVV558])), 
always(or([not NVV559, NVV560])), 
always(or([not NVV563, NVV564])), 
always(or([not NVV565, NVV566])), 
always(or([not NVV567, NVV568])), 
always(or([not NVV569, NVV570])), 
always(or([not NVV571, NVV572])), 
always(or([not NVV573, NVV574])), 
always(or([not NVV575, NVV576])), 
always(or([not NVV577, NVV578])), 
always(or([not NVV579, NVV580])), 
always(or([not NVV581, NVV582])), 
always(or([not NVV583, NVV584])), 
always(or([not NVV585, NVV586])), 
always(or([not NVV587, NVV588])), 
always(or([not NVV589, NVV590])), 
always(or([not NVV591, NVV592])), 
always(or([not NVV593, NVV594])), 
always(or([not NVV595, NVV596])), 
always(or([not NVV598, NVV599])), 
always(or([not NVV600, NVV601])), 
always(or([not NVV604, NVV605])), 
always(or([not NVV606, NVV607])), 
always(or([not NVV608, NVV609])), 
always(or([not NVV610, NVV611])), 
always(or([not NVV612, NVV613])), 
always(or([not NVV614, NVV615])), 
always(or([not NVV616, NVV617])), 
always(or([not NVV618, NVV619])), 
always(or([not NVV620, NVV621])), 
always(or([not NVV622, NVV623])), 
always(or([not NVV624, NVV625])), 
always(or([not NVV626, NVV627])), 
always(or([not NVV628, NVV629])), 
always(or([not NVV630, NVV631])), 
always(or([not NVV633, NVV634])), 
always(or([not NVV635, NVV636])), 
always(or([not NVV637, NVV638])), 
always(or([not NVV640, NVV641])), 
always(or([not NVV642, NVV643])), 
always(or([not NVV644, NVV645])), 
always(or([not NVV646, NVV647])), 
always(or([not NVV648, NVV649])), 
always(or([not NVV650, NVV651])), 
always(or([not NVV652, NVV653])), 
always(or([not NVV654, NVV655])), 
always(or([not NVV657, NVV658])), 
always(or([not NVV659, NVV660])), 
always(or([not NVV661, NVV662])), 
always(or([not NVV663, NVV664])), 
always(or([not NVV665, NVV666])), 
always(or([not NVV667, NVV668])), 
always(or([not NVV669, NVV670])), 
always(or([not NVV671, NVV672])), 
always(or([not NVV673, NVV674])), 
always(or([not NVV675, NVV676])), 
always(or([not NVV677, NVV678])), 
always(or([not NVV679, NVV680])), 
always(or([not NVV681, NVV682])), 
always(or([not NVV683, NVV684])), 
always(or([not NVV685, NVV686])), 
always(or([not NVV687, NVV688])), 
always(or([not NVV690, NVV691])), 
always(or([not NVV692, NVV693])), 
always(or([not NVV694, NVV695])), 
always(or([not NVV696, NVV697])), 
always(or([not NVV698, NVV699])), 
always(or([not NVV700, NVV701])), 
always(or([not NVV702, NVV703])), 
always(or([not NVV704, NVV705])), 
always(or([not NVV706, NVV707])), 
always(or([not NVV708, NVV709])), 
always(or([not NVV710, NVV711])), 
always(or([not NVV712, NVV713])), 
always(or([not NVV714, NVV715])), 
always(or([not NVV716, NVV717])), 
always(or([not NVV718, NVV719])), 
always(or([not NVV721, NVV722])), 
always(or([not NVV723, NVV724])), 
always(or([not NVV725, NVV726])), 
always(or([not NVV727, NVV728])), 
always(or([not NVV729, NVV730])), 
always(or([not NVV731, NVV732])), 
always(or([not NVV733, NVV734])), 
always(or([not NVV735, NVV736])), 
always(or([not NVV737, NVV738])), 
always(or([not NVV739, NVV740])), 
always(or([not NVV741, NVV742])), 
always(or([not NVV744, NVV745])), 
always(or([not NVV746, NVV747])), 
always(or([not NVV748, NVV749])), 
always(or([not NVV750, NVV751])), 
always(or([not NVV752, NVV753])), 
always(or([not NVV754, NVV755])), 
always(or([not NVV756, NVV757])), 
always(or([not NVV758, NVV759])), 
always(or([not NVV760, NVV761])), 
always(or([not NVV762, NVV763])), 
always(or([not NVV764, NVV765])), 
always(or([not NVV767, NVV768])), 
always(or([not NVV769, NVV770])), 
always(or([not NVV771, NVV772])), 
always(or([not NVV773, NVV774])), 
always(or([not NVV775, NVV776])), 
always(or([not NVV777, NVV778])), 
always(or([not NVV779, NVV780])), 
always(or([not NVV781, NVV782])), 
always(or([not NVV783, NVV784])), 
always(or([not NVV785, NVV786])), 
always(or([not NVV787, NVV788])), 
always(or([not NVV789, NVV790])), 
always(or([not NVV791, NVV792])), 
always(or([not NVV793, NVV794])), 
always(or([not NVV795, NVV796])), 
always(or([not NVV798, NVV799])), 
always(or([not NVV800, NVV801])), 
always(or([not NVV802, NVV803])), 
always(or([not NVV804, NVV805])), 
always(or([not NVV806, NVV807])), 
always(or([not NVV808, NVV809])), 
always(or([not NVV811, NVV812])), 
always(or([not NVV813, NVV814])), 
always(or([not NVV815, NVV816])), 
always(or([not NVV817, NVV818])), 
always(or([not NVV819, NVV820])), 
always(or([not NVV821, NVV822])), 
always(or([not NVV823, NVV824])), 
always(or([not NVV825, NVV826])), 
always(or([not NVV827, NVV828])), 
always(or([not NVV829, NVV830])), 
always(or([not NVV831, NVV832])), 
always(or([not NVV833, NVV834])), 
always(or([not NVV835, NVV836])),
always(or([not NVV1(X), next(NVV1(hidden(X)))])), 
always(or([not NVV1(constant(X)), next(NVV1(constant(X)))])), 
always(or([not NVV2, next(NVV2)])), 
always(or([not NVV5(X), next(NVV5(hidden(X)))])), 
always(or([not NVV5(constant(X)), next(NVV5(constant(X)))])), 
always(or([not NVV8(X), next(NVV8(hidden(X)))])), 
always(or([not NVV8(constant(X)), next(NVV8(constant(X)))])), 
always(or([not NVV11(X), next(not BOX6P(hidden(X)))])), 
always(or([not NVV11(constant(X)), next(not BOX6P(constant(X)))])), 
always(or([not NVV12(X), next(NVV13(hidden(X)))])), 
always(or([not NVV12(constant(X)), next(NVV13(constant(X)))])), 
always(or([not NVV14(X), next(NVV15(hidden(X)))])), 
always(or([not NVV14(constant(X)), next(NVV15(constant(X)))])), 
always(or([not NVV16(X), next(BOX6P(hidden(X)))])), 
always(or([not NVV16(constant(X)), next(BOX6P(constant(X)))])), 
always(or([not NVV17, next(NVV17)])), 
always(or([not NVV20(X), next(NVV20(hidden(X)))])), 
always(or([not NVV20(constant(X)), next(NVV20(constant(X)))])), 
always(or([not NVV23(X), next(not BOX0F(hidden(X)))])), 
always(or([not NVV23(constant(X)), next(not BOX0F(constant(X)))])), 
always(or([not NVV24(X), next(BOX10F(hidden(X)))])), 
always(or([not NVV24(constant(X)), next(BOX10F(constant(X)))])), 
always(or([not NVV25(X), next(not BOX10F(hidden(X)))])), 
always(or([not NVV25(constant(X)), next(not BOX10F(constant(X)))])), 
always(or([not NVV26(X), next(BOX0F(hidden(X)))])), 
always(or([not NVV26(constant(X)), next(BOX0F(constant(X)))])), 
always(or([not NVV27(X), next(not BOX5P(hidden(X)))])), 
always(or([not NVV27(constant(X)), next(not BOX5P(constant(X)))])), 
always(or([not NVV28, next(PinvSalaryF)])), 
always(or([not NVV29, next(not PinvSalaryF)])), 
always(or([not NVV30(X), next(BOX5P(hidden(X)))])), 
always(or([not NVV30(constant(X)), next(BOX5P(constant(X)))])), 
always(or([not NVV31(X), next(not BOX14F(hidden(X)))])), 
always(or([not NVV31(constant(X)), next(not BOX14F(constant(X)))])), 
always(or([not NVV32(X), next(BOX15F(hidden(X)))])), 
always(or([not NVV32(constant(X)), next(BOX15F(constant(X)))])), 
always(or([not NVV33(X), next(not BOX15F(hidden(X)))])), 
always(or([not NVV33(constant(X)), next(not BOX15F(constant(X)))])), 
always(or([not NVV34(X), next(BOX14F(hidden(X)))])), 
always(or([not NVV34(constant(X)), next(BOX14F(constant(X)))])), 
always(or([not NVV35(X), next(not BOX3P(hidden(X)))])), 
always(or([not NVV35(constant(X)), next(not BOX3P(constant(X)))])), 
always(or([not NVV36(X), next(NVV37(hidden(X)))])), 
always(or([not NVV36(constant(X)), next(NVV37(constant(X)))])), 
always(or([not NVV38(X), next(NVV39(hidden(X)))])), 
always(or([not NVV38(constant(X)), next(NVV39(constant(X)))])), 
always(or([not NVV40(X), next(BOX3P(hidden(X)))])), 
always(or([not NVV40(constant(X)), next(BOX3P(constant(X)))])), 
always(or([not NVV41(X), next(not BOX11F(hidden(X)))])), 
always(or([not NVV41(constant(X)), next(not BOX11F(constant(X)))])), 
always(or([not NVV42(X), next(BOX12F(hidden(X)))])), 
always(or([not NVV42(constant(X)), next(BOX12F(constant(X)))])), 
always(or([not NVV43(X), next(not BOX12F(hidden(X)))])), 
always(or([not NVV43(constant(X)), next(not BOX12F(constant(X)))])), 
always(or([not NVV44(X), next(BOX11F(hidden(X)))])), 
always(or([not NVV44(constant(X)), next(BOX11F(constant(X)))])), 
always(or([not NVV45(X), next(NVV45(hidden(X)))])), 
always(or([not NVV45(constant(X)), next(NVV45(constant(X)))])), 
always(or([not NVV48(X), next(not BOX8P(hidden(X)))])), 
always(or([not NVV48(constant(X)), next(not BOX8P(constant(X)))])), 
always(or([not NVV49, next(PSalaryF)])), 
always(or([not NVV50, next(not PSalaryF)])), 
always(or([not NVV51(X), next(BOX8P(hidden(X)))])), 
always(or([not NVV51(constant(X)), next(BOX8P(constant(X)))])), 
always(or([not NVV52(X), next(NVV52(hidden(X)))])), 
always(or([not NVV52(constant(X)), next(NVV52(constant(X)))])), 
always(or([not NVV55(X), next(not BOX1F(hidden(X)))])), 
always(or([not NVV55(constant(X)), next(not BOX1F(constant(X)))])), 
always(or([not NVV56(X), next(BOX13F(hidden(X)))])), 
always(or([not NVV56(constant(X)), next(BOX13F(constant(X)))])), 
always(or([not NVV57(X), next(not BOX13F(hidden(X)))])), 
always(or([not NVV57(constant(X)), next(not BOX13F(constant(X)))])), 
always(or([not NVV58(X), next(BOX1F(hidden(X)))])), 
always(or([not NVV58(constant(X)), next(BOX1F(constant(X)))])), 
always(or([not NVV59(X), next(NVV59(hidden(X)))])), 
always(or([not NVV59(constant(X)), next(NVV59(constant(X)))])), 
always(or([not NVV62(X), next(NVV62(hidden(X)))])), 
always(or([not NVV62(constant(X)), next(NVV62(constant(X)))])), 
always(or([not NVV65(X), next(not BOX2F(hidden(X)))])), 
always(or([not NVV65(constant(X)), next(not BOX2F(constant(X)))])), 
always(or([not NVV66(X), next(BOX16F(hidden(X)))])), 
always(or([not NVV66(constant(X)), next(BOX16F(constant(X)))])), 
always(or([not NVV67(X), next(not BOX16F(hidden(X)))])), 
always(or([not NVV67(constant(X)), next(not BOX16F(constant(X)))])), 
always(or([not NVV68(X), next(BOX2F(hidden(X)))])), 
always(or([not NVV68(constant(X)), next(BOX2F(constant(X)))])), 
always(or([not NVV69(X), next(NVV69(hidden(X)))])), 
always(or([not NVV69(constant(X)), next(NVV69(constant(X)))])), 
always(or([not NVV72(X), next(not BOX9P(hidden(X)))])), 
always(or([not NVV72(constant(X)), next(not BOX9P(constant(X)))])), 
always(or([not NVV73(X), next(NVV74(hidden(X)))])), 
always(or([not NVV73(constant(X)), next(NVV74(constant(X)))])), 
always(or([not NVV75(X), next(NVV76(hidden(X)))])), 
always(or([not NVV75(constant(X)), next(NVV76(constant(X)))])), 
always(or([not NVV77(X), next(BOX9P(hidden(X)))])), 
always(or([not NVV77(constant(X)), next(BOX9P(constant(X)))])), 
always(or([not NVV78, next(NVV79)])), 
always(or([not NVV80, next(E2SalaryF(John))])), 
always(or([not NVV81, next(NVV82)])), 
always(or([not NVV83, next(NVV84)])), 
always(or([not NVV85, next(NVV86)])), 
always(or([not NVV87, next(NVV88)])), 
always(or([not NVV89, next(NVV90)])), 
always(or([not NVV91, next(E1SalaryInvF(S14))])), 
always(or([not NVV92, next(NVV93)])), 
always(or([not NVV94, next(NVV95)])), 
always(or([not NVV96, next(NVV97)])), 
always(or([not NVV98, next(NVV99)])), 
always(or([not NVV100, next(NVV101)])), 
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(E1SalaryInvF(S12))])), 
always(or([not NVV121, next(NVV122)])), 
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(E1SalaryInvF(S16))])), 
always(or([not NVV140, next(NVV141)])), 
always(or([not NVV142, next(NVV143)])), 
always(or([not NVV144, next(NVV145)])), 
always(or([not NVV146, next(NVV147)])), 
always(or([not NVV148, next(NVV149)])), 
always(or([not NVV150, next(NVV151)])), 
always(or([not NVV152, next(NVV153)])), 
always(or([not NVV154, next(NVV155)])), 
always(or([not NVV156, next(NVV157)])), 
always(or([not NVV158, next(E1SalaryInvF(S21))])), 
always(or([not NVV159, next(NVV160)])), 
always(or([not NVV161, next(NVV162)])), 
always(or([not NVV163, next(NVV164)])), 
always(or([not NVV165, next(NVV166)])), 
always(or([not NVV167, next(NVV168)])), 
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(E1SalaryInvF(S27))])), 
always(or([not NVV184, next(NVV185)])), 
always(or([not NVV186, next(NVV187)])), 
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(NVV203)])), 
always(or([not NVV204, next(E1SalaryInvF(S23))])), 
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(E1SalaryInvF(S18))])), 
always(or([not NVV220, next(NVV221)])), 
always(or([not NVV222, next(NVV223)])), 
always(or([not NVV224, next(NVV225)])), 
always(or([not NVV226, next(NVV227)])), 
always(or([not NVV228, next(NVV229)])), 
always(or([not NVV230, next(NVV231)])), 
always(or([not NVV232, next(NVV233)])), 
always(or([not NVV234, next(NVV235)])), 
always(or([not NVV236, next(NVV237)])), 
always(or([not NVV238, next(NVV239)])), 
always(or([not NVV240, next(NVV241)])), 
always(or([not NVV242, next(NVV243)])), 
always(or([not NVV244, next(NVV245)])), 
always(or([not NVV246, next(NVV247)])), 
always(or([not NVV248, next(E1SalaryInvF(S32))])), 
always(or([not NVV249, next(NVV250)])), 
always(or([not NVV251, next(NVV252)])), 
always(or([not NVV253, next(NVV254)])), 
always(or([not NVV255, next(NVV256)])), 
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(NVV268)])), 
always(or([not NVV269, next(NVV270)])), 
always(or([not NVV271, next(NVV272)])), 
always(or([not NVV273, next(NVV274)])), 
always(or([not NVV275, next(NVV276)])), 
always(or([not NVV277, next(NVV278)])), 
always(or([not NVV279, next(NVV280)])), 
always(or([not NVV281, next(NVV282)])), 
always(or([not NVV283, next(E1SalaryInvF(S38))])), 
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(NVV293)])), 
always(or([not NVV294, next(NVV295)])), 
always(or([not NVV296, next(NVV297)])), 
always(or([not NVV298, next(NVV299)])), 
always(or([not NVV300, next(NVV301)])), 
always(or([not NVV302, next(NVV303)])), 
always(or([not NVV304, next(NVV305)])), 
always(or([not NVV306, next(NVV307)])), 
always(or([not NVV308, next(NVV309)])), 
always(or([not NVV310, next(NVV311)])), 
always(or([not NVV312, next(NVV313)])), 
always(or([not NVV314, next(NVV315)])), 
always(or([not NVV316, next(NVV317)])), 
always(or([not NVV318, next(NVV319)])), 
always(or([not NVV320, next(E1SalaryInvF(S40))])), 
always(or([not NVV321, next(NVV322)])), 
always(or([not NVV323, next(NVV324)])), 
always(or([not NVV325, next(NVV326)])), 
always(or([not NVV327, next(NVV328)])), 
always(or([not NVV329, next(NVV330)])), 
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(NVV344)])), 
always(or([not NVV345, next(NVV346)])), 
always(or([not NVV347, next(NVV348)])), 
always(or([not NVV349, next(NVV350)])), 
always(or([not NVV351, next(NVV352)])), 
always(or([not NVV353, next(NVV354)])), 
always(or([not NVV355, next(NVV356)])), 
always(or([not NVV357, next(E1SalaryInvF(S39))])), 
always(or([not NVV358, next(NVV359)])), 
always(or([not NVV360, next(E1SalaryInvF(S6))])), 
always(or([not NVV361, next(NVV362)])), 
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(E1SalaryInvF(S13))])), 
always(or([not NVV372, next(NVV373)])), 
always(or([not NVV374, next(NVV375)])), 
always(or([not NVV376, next(NVV377)])), 
always(or([not NVV378, next(NVV379)])), 
always(or([not NVV380, next(E1SalaryInvF(S11))])), 
always(or([not NVV381, next(NVV382)])), 
always(or([not NVV383, next(NVV384)])), 
always(or([not NVV385, next(NVV386)])), 
always(or([not NVV387, next(NVV388)])), 
always(or([not NVV389, next(NVV390)])), 
always(or([not NVV391, next(NVV392)])), 
always(or([not NVV393, next(NVV394)])), 
always(or([not NVV395, next(NVV396)])), 
always(or([not NVV397, next(NVV398)])), 
always(or([not NVV399, next(E1SalaryInvF(S17))])), 
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(NVV411)])), 
always(or([not NVV412, next(NVV413)])), 
always(or([not NVV414, next(NVV415)])), 
always(or([not NVV416, next(NVV417)])), 
always(or([not NVV418, next(NVV419)])), 
always(or([not NVV420, next(NVV421)])), 
always(or([not NVV422, next(NVV423)])), 
always(or([not NVV424, next(NVV425)])), 
always(or([not NVV426, next(NVV427)])), 
always(or([not NVV428, next(NVV429)])), 
always(or([not NVV430, next(NVV431)])), 
always(or([not NVV432, next(NVV433)])), 
always(or([not NVV434, next(E1SalaryInvF(S36))])), 
always(or([not NVV435, next(NVV436)])), 
always(or([not NVV437, next(NVV438)])), 
always(or([not NVV439, next(E1SalaryInvF(S8))])), 
always(or([not NVV440, next(NVV441)])), 
always(or([not NVV442, next(NVV443)])), 
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(NVV455)])), 
always(or([not NVV456, next(NVV457)])), 
always(or([not NVV458, next(NVV459)])), 
always(or([not NVV460, next(NVV461)])), 
always(or([not NVV462, next(NVV463)])), 
always(or([not NVV464, next(E1SalaryInvF(S28))])), 
always(or([not NVV465, next(NVV466)])), 
always(or([not NVV467, next(NVV468)])), 
always(or([not NVV469, next(NVV470)])), 
always(or([not NVV471, next(E1SalaryInvF(S9))])), 
always(or([not NVV472, next(NVV473)])), 
always(or([not NVV474, next(NVV475)])), 
always(or([not NVV476, next(NVV477)])), 
always(or([not NVV478, next(NVV479)])), 
always(or([not NVV480, next(NVV481)])), 
always(or([not NVV482, next(NVV483)])), 
always(or([not NVV484, next(NVV485)])), 
always(or([not NVV486, next(NVV487)])), 
always(or([not NVV488, next(NVV489)])), 
always(or([not NVV490, next(NVV491)])), 
always(or([not NVV492, next(NVV493)])), 
always(or([not NVV494, next(NVV495)])), 
always(or([not NVV496, next(NVV497)])), 
always(or([not NVV498, next(E1SalaryInvF(S30))])), 
always(or([not NVV499, next(NVV500)])), 
always(or([not NVV501, next(NVV502)])), 
always(or([not NVV503, next(NVV504)])), 
always(or([not NVV505, next(NVV506)])), 
always(or([not NVV507, next(NVV508)])), 
always(or([not NVV509, next(NVV510)])), 
always(or([not NVV511, next(NVV512)])), 
always(or([not NVV513, next(NVV514)])), 
always(or([not NVV515, next(NVV516)])), 
always(or([not NVV517, next(E1SalaryInvF(S20))])), 
always(or([not NVV518, next(NVV519)])), 
always(or([not NVV520, next(NVV521)])), 
always(or([not NVV522, next(NVV523)])), 
always(or([not NVV524, next(NVV525)])), 
always(or([not NVV526, next(NVV527)])), 
always(or([not NVV528, next(NVV529)])), 
always(or([not NVV530, next(NVV531)])), 
always(or([not NVV532, next(NVV533)])), 
always(or([not NVV534, next(NVV535)])), 
always(or([not NVV536, next(E1SalaryInvF(S22))])), 
always(or([not NVV537, next(NVV538)])), 
always(or([not NVV539, next(E1SalaryInvF(S5))])), 
always(or([not NVV540, next(NVV541)])), 
always(or([not NVV542, next(NVV543)])), 
always(or([not NVV544, next(NVV545)])), 
always(or([not NVV546, next(NVV547)])), 
always(or([not NVV548, next(NVV549)])), 
always(or([not NVV550, next(NVV551)])), 
always(or([not NVV552, next(NVV553)])), 
always(or([not NVV554, next(NVV555)])), 
always(or([not NVV556, next(NVV557)])), 
always(or([not NVV558, next(NVV559)])), 
always(or([not NVV560, next(E1SalaryInvF(S24))])), 
always(or([not NVV561, next(E1SalaryInvF(S4))])), 
always(or([not NVV562, next(NVV563)])), 
always(or([not NVV564, next(NVV565)])), 
always(or([not NVV566, next(NVV567)])), 
always(or([not NVV568, next(NVV569)])), 
always(or([not NVV570, next(NVV571)])), 
always(or([not NVV572, next(NVV573)])), 
always(or([not NVV574, next(NVV575)])), 
always(or([not NVV576, next(NVV577)])), 
always(or([not NVV578, next(NVV579)])), 
always(or([not NVV580, next(NVV581)])), 
always(or([not NVV582, next(NVV583)])), 
always(or([not NVV584, next(NVV585)])), 
always(or([not NVV586, next(NVV587)])), 
always(or([not NVV588, next(NVV589)])), 
always(or([not NVV590, next(NVV591)])), 
always(or([not NVV592, next(NVV593)])), 
always(or([not NVV594, next(NVV595)])), 
always(or([not NVV596, next(E1SalaryInvF(S37))])), 
always(or([not NVV597, next(NVV598)])), 
always(or([not NVV599, next(NVV600)])), 
always(or([not NVV601, next(E1SalaryInvF(S7))])), 
always(or([not NVV602, next(E1SalaryInvF(S3))])), 
always(or([not NVV603, next(NVV604)])), 
always(or([not NVV605, next(NVV606)])), 
always(or([not NVV607, next(NVV608)])), 
always(or([not NVV609, next(NVV610)])), 
always(or([not NVV611, next(NVV612)])), 
always(or([not NVV613, next(NVV614)])), 
always(or([not NVV615, next(NVV616)])), 
always(or([not NVV617, next(NVV618)])), 
always(or([not NVV619, next(NVV620)])), 
always(or([not NVV621, next(NVV622)])), 
always(or([not NVV623, next(NVV624)])), 
always(or([not NVV625, next(NVV626)])), 
always(or([not NVV627, next(NVV628)])), 
always(or([not NVV629, next(NVV630)])), 
always(or([not NVV631, next(E1SalaryInvF(S31))])), 
always(or([not NVV632, next(NVV633)])), 
always(or([not NVV634, next(NVV635)])), 
always(or([not NVV636, next(NVV637)])), 
always(or([not NVV638, next(E1SalaryInvF(S10))])), 
always(or([not NVV639, next(NVV640)])), 
always(or([not NVV641, next(NVV642)])), 
always(or([not NVV643, next(NVV644)])), 
always(or([not NVV645, next(NVV646)])), 
always(or([not NVV647, next(NVV648)])), 
always(or([not NVV649, next(NVV650)])), 
always(or([not NVV651, next(NVV652)])), 
always(or([not NVV653, next(NVV654)])), 
always(or([not NVV655, next(E1SalaryInvF(S19))])), 
always(or([not NVV656, next(NVV657)])), 
always(or([not NVV658, next(NVV659)])), 
always(or([not NVV660, next(NVV661)])), 
always(or([not NVV662, next(NVV663)])), 
always(or([not NVV664, next(NVV665)])), 
always(or([not NVV666, next(NVV667)])), 
always(or([not NVV668, next(NVV669)])), 
always(or([not NVV670, next(NVV671)])), 
always(or([not NVV672, next(NVV673)])), 
always(or([not NVV674, next(NVV675)])), 
always(or([not NVV676, next(NVV677)])), 
always(or([not NVV678, next(NVV679)])), 
always(or([not NVV680, next(NVV681)])), 
always(or([not NVV682, next(NVV683)])), 
always(or([not NVV684, next(NVV685)])), 
always(or([not NVV686, next(NVV687)])), 
always(or([not NVV688, next(E1SalaryInvF(S35))])), 
always(or([not NVV689, next(NVV690)])), 
always(or([not NVV691, next(NVV692)])), 
always(or([not NVV693, next(NVV694)])), 
always(or([not NVV695, next(NVV696)])), 
always(or([not NVV697, next(NVV698)])), 
always(or([not NVV699, next(NVV700)])), 
always(or([not NVV701, next(NVV702)])), 
always(or([not NVV703, next(NVV704)])), 
always(or([not NVV705, next(NVV706)])), 
always(or([not NVV707, next(NVV708)])), 
always(or([not NVV709, next(NVV710)])), 
always(or([not NVV711, next(NVV712)])), 
always(or([not NVV713, next(NVV714)])), 
always(or([not NVV715, next(NVV716)])), 
always(or([not NVV717, next(NVV718)])), 
always(or([not NVV719, next(E1SalaryInvF(S33))])), 
always(or([not NVV720, next(NVV721)])), 
always(or([not NVV722, next(NVV723)])), 
always(or([not NVV724, next(NVV725)])), 
always(or([not NVV726, next(NVV727)])), 
always(or([not NVV728, next(NVV729)])), 
always(or([not NVV730, next(NVV731)])), 
always(or([not NVV732, next(NVV733)])), 
always(or([not NVV734, next(NVV735)])), 
always(or([not NVV736, next(NVV737)])), 
always(or([not NVV738, next(NVV739)])), 
always(or([not NVV740, next(NVV741)])), 
always(or([not NVV742, next(E1SalaryInvF(S26))])), 
always(or([not NVV743, next(NVV744)])), 
always(or([not NVV745, next(NVV746)])), 
always(or([not NVV747, next(NVV748)])), 
always(or([not NVV749, next(NVV750)])), 
always(or([not NVV751, next(NVV752)])), 
always(or([not NVV753, next(NVV754)])), 
always(or([not NVV755, next(NVV756)])), 
always(or([not NVV757, next(NVV758)])), 
always(or([not NVV759, next(NVV760)])), 
always(or([not NVV761, next(NVV762)])), 
always(or([not NVV763, next(NVV764)])), 
always(or([not NVV765, next(E1SalaryInvF(S25))])), 
always(or([not NVV766, next(NVV767)])), 
always(or([not NVV768, next(NVV769)])), 
always(or([not NVV770, next(NVV771)])), 
always(or([not NVV772, next(NVV773)])), 
always(or([not NVV774, next(NVV775)])), 
always(or([not NVV776, next(NVV777)])), 
always(or([not NVV778, next(NVV779)])), 
always(or([not NVV780, next(NVV781)])), 
always(or([not NVV782, next(NVV783)])), 
always(or([not NVV784, next(NVV785)])), 
always(or([not NVV786, next(NVV787)])), 
always(or([not NVV788, next(NVV789)])), 
always(or([not NVV790, next(NVV791)])), 
always(or([not NVV792, next(NVV793)])), 
always(or([not NVV794, next(NVV795)])), 
always(or([not NVV796, next(E1SalaryInvF(S34))])), 
always(or([not NVV797, next(NVV798)])), 
always(or([not NVV799, next(NVV800)])), 
always(or([not NVV801, next(NVV802)])), 
always(or([not NVV803, next(NVV804)])), 
always(or([not NVV805, next(NVV806)])), 
always(or([not NVV807, next(NVV808)])), 
always(or([not NVV809, next(E1SalaryInvF(S15))])), 
always(or([not NVV810, next(NVV811)])), 
always(or([not NVV812, next(NVV813)])), 
always(or([not NVV814, next(NVV815)])), 
always(or([not NVV816, next(NVV817)])), 
always(or([not NVV818, next(NVV819)])), 
always(or([not NVV820, next(NVV821)])), 
always(or([not NVV822, next(NVV823)])), 
always(or([not NVV824, next(NVV825)])), 
always(or([not NVV826, next(NVV827)])), 
always(or([not NVV828, next(NVV829)])), 
always(or([not NVV830, next(NVV831)])), 
always(or([not NVV832, next(NVV833)])), 
always(or([not NVV834, next(NVV835)])), 
always(or([not NVV836, next(E1SalaryInvF(S29))])),
always(or([not NVV3, sometime(NVV4)])), 
always(or([not NVV6(X), sometime(NVV7(X))])), 
always(or([not NVV6(constant(dSalary)), sometime(NVV7(constant(dSalary)))])), 
always(or([not NVV6(constant(dSalaryInv)), sometime(NVV7(constant(dSalaryInv)))])), 
always(or([not NVV6(constant(S14)), sometime(NVV7(constant(S14)))])), 
always(or([not NVV6(constant(S12)), sometime(NVV7(constant(S12)))])), 
always(or([not NVV6(constant(S16)), sometime(NVV7(constant(S16)))])), 
always(or([not NVV6(constant(S21)), sometime(NVV7(constant(S21)))])), 
always(or([not NVV6(constant(S27)), sometime(NVV7(constant(S27)))])), 
always(or([not NVV6(constant(S23)), sometime(NVV7(constant(S23)))])), 
always(or([not NVV6(constant(S18)), sometime(NVV7(constant(S18)))])), 
always(or([not NVV6(constant(S32)), sometime(NVV7(constant(S32)))])), 
always(or([not NVV6(constant(S38)), sometime(NVV7(constant(S38)))])), 
always(or([not NVV6(constant(S40)), sometime(NVV7(constant(S40)))])), 
always(or([not NVV6(constant(S39)), sometime(NVV7(constant(S39)))])), 
always(or([not NVV6(constant(S6)), sometime(NVV7(constant(S6)))])), 
always(or([not NVV6(constant(S13)), sometime(NVV7(constant(S13)))])), 
always(or([not NVV6(constant(S11)), sometime(NVV7(constant(S11)))])), 
always(or([not NVV6(constant(S17)), sometime(NVV7(constant(S17)))])), 
always(or([not NVV6(constant(S36)), sometime(NVV7(constant(S36)))])), 
always(or([not NVV6(constant(S8)), sometime(NVV7(constant(S8)))])), 
always(or([not NVV6(constant(S28)), sometime(NVV7(constant(S28)))])), 
always(or([not NVV6(constant(S9)), sometime(NVV7(constant(S9)))])), 
always(or([not NVV6(constant(S30)), sometime(NVV7(constant(S30)))])), 
always(or([not NVV6(constant(S20)), sometime(NVV7(constant(S20)))])), 
always(or([not NVV6(constant(S22)), sometime(NVV7(constant(S22)))])), 
always(or([not NVV6(constant(S5)), sometime(NVV7(constant(S5)))])), 
always(or([not NVV6(constant(S24)), sometime(NVV7(constant(S24)))])), 
always(or([not NVV6(constant(S4)), sometime(NVV7(constant(S4)))])), 
always(or([not NVV6(constant(S37)), sometime(NVV7(constant(S37)))])), 
always(or([not NVV6(constant(S7)), sometime(NVV7(constant(S7)))])), 
always(or([not NVV6(constant(S3)), sometime(NVV7(constant(S3)))])), 
always(or([not NVV6(constant(S31)), sometime(NVV7(constant(S31)))])), 
always(or([not NVV6(constant(S1)), sometime(NVV7(constant(S1)))])), 
always(or([not NVV6(constant(S2)), sometime(NVV7(constant(S2)))])), 
always(or([not NVV6(constant(S10)), sometime(NVV7(constant(S10)))])), 
always(or([not NVV6(constant(S19)), sometime(NVV7(constant(S19)))])), 
always(or([not NVV6(constant(S35)), sometime(NVV7(constant(S35)))])), 
always(or([not NVV6(constant(S33)), sometime(NVV7(constant(S33)))])), 
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(S34)), sometime(NVV7(constant(S34)))])), 
always(or([not NVV6(constant(John)), sometime(NVV7(constant(John)))])), 
always(or([not NVV6(constant(S15)), sometime(NVV7(constant(S15)))])), 
always(or([not NVV6(constant(S29)), sometime(NVV7(constant(S29)))])), 
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(S14)), sometime(NVV10(constant(S14)))])), 
always(or([not NVV9(constant(S12)), sometime(NVV10(constant(S12)))])), 
always(or([not NVV9(constant(S16)), sometime(NVV10(constant(S16)))])), 
always(or([not NVV9(constant(S21)), sometime(NVV10(constant(S21)))])), 
always(or([not NVV9(constant(S27)), sometime(NVV10(constant(S27)))])), 
always(or([not NVV9(constant(S23)), sometime(NVV10(constant(S23)))])), 
always(or([not NVV9(constant(S18)), sometime(NVV10(constant(S18)))])), 
always(or([not NVV9(constant(S32)), sometime(NVV10(constant(S32)))])), 
always(or([not NVV9(constant(S38)), sometime(NVV10(constant(S38)))])), 
always(or([not NVV9(constant(S40)), sometime(NVV10(constant(S40)))])), 
always(or([not NVV9(constant(S39)), sometime(NVV10(constant(S39)))])), 
always(or([not NVV9(constant(S6)), sometime(NVV10(constant(S6)))])), 
always(or([not NVV9(constant(S13)), sometime(NVV10(constant(S13)))])), 
always(or([not NVV9(constant(S11)), sometime(NVV10(constant(S11)))])), 
always(or([not NVV9(constant(S17)), sometime(NVV10(constant(S17)))])), 
always(or([not NVV9(constant(S36)), sometime(NVV10(constant(S36)))])), 
always(or([not NVV9(constant(S8)), sometime(NVV10(constant(S8)))])), 
always(or([not NVV9(constant(S28)), sometime(NVV10(constant(S28)))])), 
always(or([not NVV9(constant(S9)), sometime(NVV10(constant(S9)))])), 
always(or([not NVV9(constant(S30)), sometime(NVV10(constant(S30)))])), 
always(or([not NVV9(constant(S20)), sometime(NVV10(constant(S20)))])), 
always(or([not NVV9(constant(S22)), sometime(NVV10(constant(S22)))])), 
always(or([not NVV9(constant(S5)), sometime(NVV10(constant(S5)))])), 
always(or([not NVV9(constant(S24)), sometime(NVV10(constant(S24)))])), 
always(or([not NVV9(constant(S4)), sometime(NVV10(constant(S4)))])), 
always(or([not NVV9(constant(S37)), sometime(NVV10(constant(S37)))])), 
always(or([not NVV9(constant(S7)), sometime(NVV10(constant(S7)))])), 
always(or([not NVV9(constant(S3)), sometime(NVV10(constant(S3)))])), 
always(or([not NVV9(constant(S31)), sometime(NVV10(constant(S31)))])), 
always(or([not NVV9(constant(S1)), sometime(NVV10(constant(S1)))])), 
always(or([not NVV9(constant(S2)), sometime(NVV10(constant(S2)))])), 
always(or([not NVV9(constant(S10)), sometime(NVV10(constant(S10)))])), 
always(or([not NVV9(constant(S19)), sometime(NVV10(constant(S19)))])), 
always(or([not NVV9(constant(S35)), sometime(NVV10(constant(S35)))])), 
always(or([not NVV9(constant(S33)), sometime(NVV10(constant(S33)))])), 
always(or([not NVV9(constant(S26)), sometime(NVV10(constant(S26)))])), 
always(or([not NVV9(constant(S25)), sometime(NVV10(constant(S25)))])), 
always(or([not NVV9(constant(S34)), sometime(NVV10(constant(S34)))])), 
always(or([not NVV9(constant(John)), sometime(NVV10(constant(John)))])), 
always(or([not NVV9(constant(S15)), sometime(NVV10(constant(S15)))])), 
always(or([not NVV9(constant(S29)), sometime(NVV10(constant(S29)))])), 
always(or([not NVV18, sometime(NVV19)])), 
always(or([not NVV21(X), sometime(NVV22(X))])), 
always(or([not NVV21(constant(dSalary)), sometime(NVV22(constant(dSalary)))])), 
always(or([not NVV21(constant(dSalaryInv)), sometime(NVV22(constant(dSalaryInv)))])), 
always(or([not NVV21(constant(S14)), sometime(NVV22(constant(S14)))])), 
always(or([not NVV21(constant(S12)), sometime(NVV22(constant(S12)))])), 
always(or([not NVV21(constant(S16)), sometime(NVV22(constant(S16)))])), 
always(or([not NVV21(constant(S21)), sometime(NVV22(constant(S21)))])), 
always(or([not NVV21(constant(S27)), sometime(NVV22(constant(S27)))])), 
always(or([not NVV21(constant(S23)), sometime(NVV22(constant(S23)))])), 
always(or([not NVV21(constant(S18)), sometime(NVV22(constant(S18)))])), 
always(or([not NVV21(constant(S32)), sometime(NVV22(constant(S32)))])), 
always(or([not NVV21(constant(S38)), sometime(NVV22(constant(S38)))])), 
always(or([not NVV21(constant(S40)), sometime(NVV22(constant(S40)))])), 
always(or([not NVV21(constant(S39)), sometime(NVV22(constant(S39)))])), 
always(or([not NVV21(constant(S6)), sometime(NVV22(constant(S6)))])), 
always(or([not NVV21(constant(S13)), sometime(NVV22(constant(S13)))])), 
always(or([not NVV21(constant(S11)), sometime(NVV22(constant(S11)))])), 
always(or([not NVV21(constant(S17)), sometime(NVV22(constant(S17)))])), 
always(or([not NVV21(constant(S36)), sometime(NVV22(constant(S36)))])), 
always(or([not NVV21(constant(S8)), sometime(NVV22(constant(S8)))])), 
always(or([not NVV21(constant(S28)), sometime(NVV22(constant(S28)))])), 
always(or([not NVV21(constant(S9)), sometime(NVV22(constant(S9)))])), 
always(or([not NVV21(constant(S30)), sometime(NVV22(constant(S30)))])), 
always(or([not NVV21(constant(S20)), sometime(NVV22(constant(S20)))])), 
always(or([not NVV21(constant(S22)), sometime(NVV22(constant(S22)))])), 
always(or([not NVV21(constant(S5)), sometime(NVV22(constant(S5)))])), 
always(or([not NVV21(constant(S24)), sometime(NVV22(constant(S24)))])), 
always(or([not NVV21(constant(S4)), sometime(NVV22(constant(S4)))])), 
always(or([not NVV21(constant(S37)), sometime(NVV22(constant(S37)))])), 
always(or([not NVV21(constant(S7)), sometime(NVV22(constant(S7)))])), 
always(or([not NVV21(constant(S3)), sometime(NVV22(constant(S3)))])), 
always(or([not NVV21(constant(S31)), sometime(NVV22(constant(S31)))])), 
always(or([not NVV21(constant(S1)), sometime(NVV22(constant(S1)))])), 
always(or([not NVV21(constant(S2)), sometime(NVV22(constant(S2)))])), 
always(or([not NVV21(constant(S10)), sometime(NVV22(constant(S10)))])), 
always(or([not NVV21(constant(S19)), sometime(NVV22(constant(S19)))])), 
always(or([not NVV21(constant(S35)), sometime(NVV22(constant(S35)))])), 
always(or([not NVV21(constant(S33)), sometime(NVV22(constant(S33)))])), 
always(or([not NVV21(constant(S26)), sometime(NVV22(constant(S26)))])), 
always(or([not NVV21(constant(S25)), sometime(NVV22(constant(S25)))])), 
always(or([not NVV21(constant(S34)), sometime(NVV22(constant(S34)))])), 
always(or([not NVV21(constant(John)), sometime(NVV22(constant(John)))])), 
always(or([not NVV21(constant(S15)), sometime(NVV22(constant(S15)))])), 
always(or([not NVV21(constant(S29)), sometime(NVV22(constant(S29)))])), 
always(or([not NVV46(X), sometime(NVV47(X))])), 
always(or([not NVV46(constant(dSalary)), sometime(NVV47(constant(dSalary)))])), 
always(or([not NVV46(constant(dSalaryInv)), sometime(NVV47(constant(dSalaryInv)))])), 
always(or([not NVV46(constant(S14)), sometime(NVV47(constant(S14)))])), 
always(or([not NVV46(constant(S12)), sometime(NVV47(constant(S12)))])), 
always(or([not NVV46(constant(S16)), sometime(NVV47(constant(S16)))])), 
always(or([not NVV46(constant(S21)), sometime(NVV47(constant(S21)))])), 
always(or([not NVV46(constant(S27)), sometime(NVV47(constant(S27)))])), 
always(or([not NVV46(constant(S23)), sometime(NVV47(constant(S23)))])), 
always(or([not NVV46(constant(S18)), sometime(NVV47(constant(S18)))])), 
always(or([not NVV46(constant(S32)), sometime(NVV47(constant(S32)))])), 
always(or([not NVV46(constant(S38)), sometime(NVV47(constant(S38)))])), 
always(or([not NVV46(constant(S40)), sometime(NVV47(constant(S40)))])), 
always(or([not NVV46(constant(S39)), sometime(NVV47(constant(S39)))])), 
always(or([not NVV46(constant(S6)), sometime(NVV47(constant(S6)))])), 
always(or([not NVV46(constant(S13)), sometime(NVV47(constant(S13)))])), 
always(or([not NVV46(constant(S11)), sometime(NVV47(constant(S11)))])), 
always(or([not NVV46(constant(S17)), sometime(NVV47(constant(S17)))])), 
always(or([not NVV46(constant(S36)), sometime(NVV47(constant(S36)))])), 
always(or([not NVV46(constant(S8)), sometime(NVV47(constant(S8)))])), 
always(or([not NVV46(constant(S28)), sometime(NVV47(constant(S28)))])), 
always(or([not NVV46(constant(S9)), sometime(NVV47(constant(S9)))])), 
always(or([not NVV46(constant(S30)), sometime(NVV47(constant(S30)))])), 
always(or([not NVV46(constant(S20)), sometime(NVV47(constant(S20)))])), 
always(or([not NVV46(constant(S22)), sometime(NVV47(constant(S22)))])), 
always(or([not NVV46(constant(S5)), sometime(NVV47(constant(S5)))])), 
always(or([not NVV46(constant(S24)), sometime(NVV47(constant(S24)))])), 
always(or([not NVV46(constant(S4)), sometime(NVV47(constant(S4)))])), 
always(or([not NVV46(constant(S37)), sometime(NVV47(constant(S37)))])), 
always(or([not NVV46(constant(S7)), sometime(NVV47(constant(S7)))])), 
always(or([not NVV46(constant(S3)), sometime(NVV47(constant(S3)))])), 
always(or([not NVV46(constant(S31)), sometime(NVV47(constant(S31)))])), 
always(or([not NVV46(constant(S1)), sometime(NVV47(constant(S1)))])), 
always(or([not NVV46(constant(S2)), sometime(NVV47(constant(S2)))])), 
always(or([not NVV46(constant(S10)), sometime(NVV47(constant(S10)))])), 
always(or([not NVV46(constant(S19)), sometime(NVV47(constant(S19)))])), 
always(or([not NVV46(constant(S35)), sometime(NVV47(constant(S35)))])), 
always(or([not NVV46(constant(S33)), sometime(NVV47(constant(S33)))])), 
always(or([not NVV46(constant(S26)), sometime(NVV47(constant(S26)))])), 
always(or([not NVV46(constant(S25)), sometime(NVV47(constant(S25)))])), 
always(or([not NVV46(constant(S34)), sometime(NVV47(constant(S34)))])), 
always(or([not NVV46(constant(John)), sometime(NVV47(constant(John)))])), 
always(or([not NVV46(constant(S15)), sometime(NVV47(constant(S15)))])), 
always(or([not NVV46(constant(S29)), sometime(NVV47(constant(S29)))])), 
always(or([not NVV53(X), sometime(NVV54(X))])), 
always(or([not NVV53(constant(dSalary)), sometime(NVV54(constant(dSalary)))])), 
always(or([not NVV53(constant(dSalaryInv)), sometime(NVV54(constant(dSalaryInv)))])), 
always(or([not NVV53(constant(S14)), sometime(NVV54(constant(S14)))])), 
always(or([not NVV53(constant(S12)), sometime(NVV54(constant(S12)))])), 
always(or([not NVV53(constant(S16)), sometime(NVV54(constant(S16)))])), 
always(or([not NVV53(constant(S21)), sometime(NVV54(constant(S21)))])), 
always(or([not NVV53(constant(S27)), sometime(NVV54(constant(S27)))])), 
always(or([not NVV53(constant(S23)), sometime(NVV54(constant(S23)))])), 
always(or([not NVV53(constant(S18)), sometime(NVV54(constant(S18)))])), 
always(or([not NVV53(constant(S32)), sometime(NVV54(constant(S32)))])), 
always(or([not NVV53(constant(S38)), sometime(NVV54(constant(S38)))])), 
always(or([not NVV53(constant(S40)), sometime(NVV54(constant(S40)))])), 
always(or([not NVV53(constant(S39)), sometime(NVV54(constant(S39)))])), 
always(or([not NVV53(constant(S6)), sometime(NVV54(constant(S6)))])), 
always(or([not NVV53(constant(S13)), sometime(NVV54(constant(S13)))])), 
always(or([not NVV53(constant(S11)), sometime(NVV54(constant(S11)))])), 
always(or([not NVV53(constant(S17)), sometime(NVV54(constant(S17)))])), 
always(or([not NVV53(constant(S36)), sometime(NVV54(constant(S36)))])), 
always(or([not NVV53(constant(S8)), sometime(NVV54(constant(S8)))])), 
always(or([not NVV53(constant(S28)), sometime(NVV54(constant(S28)))])), 
always(or([not NVV53(constant(S9)), sometime(NVV54(constant(S9)))])), 
always(or([not NVV53(constant(S30)), sometime(NVV54(constant(S30)))])), 
always(or([not NVV53(constant(S20)), sometime(NVV54(constant(S20)))])), 
always(or([not NVV53(constant(S22)), sometime(NVV54(constant(S22)))])), 
always(or([not NVV53(constant(S5)), sometime(NVV54(constant(S5)))])), 
always(or([not NVV53(constant(S24)), sometime(NVV54(constant(S24)))])), 
always(or([not NVV53(constant(S4)), sometime(NVV54(constant(S4)))])), 
always(or([not NVV53(constant(S37)), sometime(NVV54(constant(S37)))])), 
always(or([not NVV53(constant(S7)), sometime(NVV54(constant(S7)))])), 
always(or([not NVV53(constant(S3)), sometime(NVV54(constant(S3)))])), 
always(or([not NVV53(constant(S31)), sometime(NVV54(constant(S31)))])), 
always(or([not NVV53(constant(S1)), sometime(NVV54(constant(S1)))])), 
always(or([not NVV53(constant(S2)), sometime(NVV54(constant(S2)))])), 
always(or([not NVV53(constant(S10)), sometime(NVV54(constant(S10)))])), 
always(or([not NVV53(constant(S19)), sometime(NVV54(constant(S19)))])), 
always(or([not NVV53(constant(S35)), sometime(NVV54(constant(S35)))])), 
always(or([not NVV53(constant(S33)), sometime(NVV54(constant(S33)))])), 
always(or([not NVV53(constant(S26)), sometime(NVV54(constant(S26)))])), 
always(or([not NVV53(constant(S25)), sometime(NVV54(constant(S25)))])), 
always(or([not NVV53(constant(S34)), sometime(NVV54(constant(S34)))])), 
always(or([not NVV53(constant(John)), sometime(NVV54(constant(John)))])), 
always(or([not NVV53(constant(S15)), sometime(NVV54(constant(S15)))])), 
always(or([not NVV53(constant(S29)), sometime(NVV54(constant(S29)))])), 
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(S14)), sometime(NVV61(constant(S14)))])), 
always(or([not NVV60(constant(S12)), sometime(NVV61(constant(S12)))])), 
always(or([not NVV60(constant(S16)), sometime(NVV61(constant(S16)))])), 
always(or([not NVV60(constant(S21)), sometime(NVV61(constant(S21)))])), 
always(or([not NVV60(constant(S27)), sometime(NVV61(constant(S27)))])), 
always(or([not NVV60(constant(S23)), sometime(NVV61(constant(S23)))])), 
always(or([not NVV60(constant(S18)), sometime(NVV61(constant(S18)))])), 
always(or([not NVV60(constant(S32)), sometime(NVV61(constant(S32)))])), 
always(or([not NVV60(constant(S38)), sometime(NVV61(constant(S38)))])), 
always(or([not NVV60(constant(S40)), sometime(NVV61(constant(S40)))])), 
always(or([not NVV60(constant(S39)), sometime(NVV61(constant(S39)))])), 
always(or([not NVV60(constant(S6)), sometime(NVV61(constant(S6)))])), 
always(or([not NVV60(constant(S13)), sometime(NVV61(constant(S13)))])), 
always(or([not NVV60(constant(S11)), sometime(NVV61(constant(S11)))])), 
always(or([not NVV60(constant(S17)), sometime(NVV61(constant(S17)))])), 
always(or([not NVV60(constant(S36)), sometime(NVV61(constant(S36)))])), 
always(or([not NVV60(constant(S8)), sometime(NVV61(constant(S8)))])), 
always(or([not NVV60(constant(S28)), sometime(NVV61(constant(S28)))])), 
always(or([not NVV60(constant(S9)), sometime(NVV61(constant(S9)))])), 
always(or([not NVV60(constant(S30)), sometime(NVV61(constant(S30)))])), 
always(or([not NVV60(constant(S20)), sometime(NVV61(constant(S20)))])), 
always(or([not NVV60(constant(S22)), sometime(NVV61(constant(S22)))])), 
always(or([not NVV60(constant(S5)), sometime(NVV61(constant(S5)))])), 
always(or([not NVV60(constant(S24)), sometime(NVV61(constant(S24)))])), 
always(or([not NVV60(constant(S4)), sometime(NVV61(constant(S4)))])), 
always(or([not NVV60(constant(S37)), sometime(NVV61(constant(S37)))])), 
always(or([not NVV60(constant(S7)), sometime(NVV61(constant(S7)))])), 
always(or([not NVV60(constant(S3)), sometime(NVV61(constant(S3)))])), 
always(or([not NVV60(constant(S31)), sometime(NVV61(constant(S31)))])), 
always(or([not NVV60(constant(S1)), sometime(NVV61(constant(S1)))])), 
always(or([not NVV60(constant(S2)), sometime(NVV61(constant(S2)))])), 
always(or([not NVV60(constant(S10)), sometime(NVV61(constant(S10)))])), 
always(or([not NVV60(constant(S19)), sometime(NVV61(constant(S19)))])), 
always(or([not NVV60(constant(S35)), sometime(NVV61(constant(S35)))])), 
always(or([not NVV60(constant(S33)), sometime(NVV61(constant(S33)))])), 
always(or([not NVV60(constant(S26)), sometime(NVV61(constant(S26)))])), 
always(or([not NVV60(constant(S25)), sometime(NVV61(constant(S25)))])), 
always(or([not NVV60(constant(S34)), sometime(NVV61(constant(S34)))])), 
always(or([not NVV60(constant(John)), sometime(NVV61(constant(John)))])), 
always(or([not NVV60(constant(S15)), sometime(NVV61(constant(S15)))])), 
always(or([not NVV60(constant(S29)), sometime(NVV61(constant(S29)))])), 
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(S14)), sometime(NVV64(constant(S14)))])), 
always(or([not NVV63(constant(S12)), sometime(NVV64(constant(S12)))])), 
always(or([not NVV63(constant(S16)), sometime(NVV64(constant(S16)))])), 
always(or([not NVV63(constant(S21)), sometime(NVV64(constant(S21)))])), 
always(or([not NVV63(constant(S27)), sometime(NVV64(constant(S27)))])), 
always(or([not NVV63(constant(S23)), sometime(NVV64(constant(S23)))])), 
always(or([not NVV63(constant(S18)), sometime(NVV64(constant(S18)))])), 
always(or([not NVV63(constant(S32)), sometime(NVV64(constant(S32)))])), 
always(or([not NVV63(constant(S38)), sometime(NVV64(constant(S38)))])), 
always(or([not NVV63(constant(S40)), sometime(NVV64(constant(S40)))])), 
always(or([not NVV63(constant(S39)), sometime(NVV64(constant(S39)))])), 
always(or([not NVV63(constant(S6)), sometime(NVV64(constant(S6)))])), 
always(or([not NVV63(constant(S13)), sometime(NVV64(constant(S13)))])), 
always(or([not NVV63(constant(S11)), sometime(NVV64(constant(S11)))])), 
always(or([not NVV63(constant(S17)), sometime(NVV64(constant(S17)))])), 
always(or([not NVV63(constant(S36)), sometime(NVV64(constant(S36)))])), 
always(or([not NVV63(constant(S8)), sometime(NVV64(constant(S8)))])), 
always(or([not NVV63(constant(S28)), sometime(NVV64(constant(S28)))])), 
always(or([not NVV63(constant(S9)), sometime(NVV64(constant(S9)))])), 
always(or([not NVV63(constant(S30)), sometime(NVV64(constant(S30)))])), 
always(or([not NVV63(constant(S20)), sometime(NVV64(constant(S20)))])), 
always(or([not NVV63(constant(S22)), sometime(NVV64(constant(S22)))])), 
always(or([not NVV63(constant(S5)), sometime(NVV64(constant(S5)))])), 
always(or([not NVV63(constant(S24)), sometime(NVV64(constant(S24)))])), 
always(or([not NVV63(constant(S4)), sometime(NVV64(constant(S4)))])), 
always(or([not NVV63(constant(S37)), sometime(NVV64(constant(S37)))])), 
always(or([not NVV63(constant(S7)), sometime(NVV64(constant(S7)))])), 
always(or([not NVV63(constant(S3)), sometime(NVV64(constant(S3)))])), 
always(or([not NVV63(constant(S31)), sometime(NVV64(constant(S31)))])), 
always(or([not NVV63(constant(S1)), sometime(NVV64(constant(S1)))])), 
always(or([not NVV63(constant(S2)), sometime(NVV64(constant(S2)))])), 
always(or([not NVV63(constant(S10)), sometime(NVV64(constant(S10)))])), 
always(or([not NVV63(constant(S19)), sometime(NVV64(constant(S19)))])), 
always(or([not NVV63(constant(S35)), sometime(NVV64(constant(S35)))])), 
always(or([not NVV63(constant(S33)), sometime(NVV64(constant(S33)))])), 
always(or([not NVV63(constant(S26)), sometime(NVV64(constant(S26)))])), 
always(or([not NVV63(constant(S25)), sometime(NVV64(constant(S25)))])), 
always(or([not NVV63(constant(S34)), sometime(NVV64(constant(S34)))])), 
always(or([not NVV63(constant(John)), sometime(NVV64(constant(John)))])), 
always(or([not NVV63(constant(S15)), sometime(NVV64(constant(S15)))])), 
always(or([not NVV63(constant(S29)), sometime(NVV64(constant(S29)))])), 
always(or([not NVV70(X), sometime(NVV71(X))])), 
always(or([not NVV70(constant(dSalary)), sometime(NVV71(constant(dSalary)))])), 
always(or([not NVV70(constant(dSalaryInv)), sometime(NVV71(constant(dSalaryInv)))])), 
always(or([not NVV70(constant(S14)), sometime(NVV71(constant(S14)))])), 
always(or([not NVV70(constant(S12)), sometime(NVV71(constant(S12)))])), 
always(or([not NVV70(constant(S16)), sometime(NVV71(constant(S16)))])), 
always(or([not NVV70(constant(S21)), sometime(NVV71(constant(S21)))])), 
always(or([not NVV70(constant(S27)), sometime(NVV71(constant(S27)))])), 
always(or([not NVV70(constant(S23)), sometime(NVV71(constant(S23)))])), 
always(or([not NVV70(constant(S18)), sometime(NVV71(constant(S18)))])), 
always(or([not NVV70(constant(S32)), sometime(NVV71(constant(S32)))])), 
always(or([not NVV70(constant(S38)), sometime(NVV71(constant(S38)))])), 
always(or([not NVV70(constant(S40)), sometime(NVV71(constant(S40)))])), 
always(or([not NVV70(constant(S39)), sometime(NVV71(constant(S39)))])), 
always(or([not NVV70(constant(S6)), sometime(NVV71(constant(S6)))])), 
always(or([not NVV70(constant(S13)), sometime(NVV71(constant(S13)))])), 
always(or([not NVV70(constant(S11)), sometime(NVV71(constant(S11)))])), 
always(or([not NVV70(constant(S17)), sometime(NVV71(constant(S17)))])), 
always(or([not NVV70(constant(S36)), sometime(NVV71(constant(S36)))])), 
always(or([not NVV70(constant(S8)), sometime(NVV71(constant(S8)))])), 
always(or([not NVV70(constant(S28)), sometime(NVV71(constant(S28)))])), 
always(or([not NVV70(constant(S9)), sometime(NVV71(constant(S9)))])), 
always(or([not NVV70(constant(S30)), sometime(NVV71(constant(S30)))])), 
always(or([not NVV70(constant(S20)), sometime(NVV71(constant(S20)))])), 
always(or([not NVV70(constant(S22)), sometime(NVV71(constant(S22)))])), 
always(or([not NVV70(constant(S5)), sometime(NVV71(constant(S5)))])), 
always(or([not NVV70(constant(S24)), sometime(NVV71(constant(S24)))])), 
always(or([not NVV70(constant(S4)), sometime(NVV71(constant(S4)))])), 
always(or([not NVV70(constant(S37)), sometime(NVV71(constant(S37)))])), 
always(or([not NVV70(constant(S7)), sometime(NVV71(constant(S7)))])), 
always(or([not NVV70(constant(S3)), sometime(NVV71(constant(S3)))])), 
always(or([not NVV70(constant(S31)), sometime(NVV71(constant(S31)))])), 
always(or([not NVV70(constant(S1)), sometime(NVV71(constant(S1)))])), 
always(or([not NVV70(constant(S2)), sometime(NVV71(constant(S2)))])), 
always(or([not NVV70(constant(S10)), sometime(NVV71(constant(S10)))])), 
always(or([not NVV70(constant(S19)), sometime(NVV71(constant(S19)))])), 
always(or([not NVV70(constant(S35)), sometime(NVV71(constant(S35)))])), 
always(or([not NVV70(constant(S33)), sometime(NVV71(constant(S33)))])), 
always(or([not NVV70(constant(S26)), sometime(NVV71(constant(S26)))])), 
always(or([not NVV70(constant(S25)), sometime(NVV71(constant(S25)))])), 
always(or([not NVV70(constant(S34)), sometime(NVV71(constant(S34)))])), 
always(or([not NVV70(constant(John)), sometime(NVV71(constant(John)))])), 
always(or([not NVV70(constant(S15)), sometime(NVV71(constant(S15)))])), 
always(or([not NVV70(constant(S29)), sometime(NVV71(constant(S29)))]))]).

