\documentclass[a4paper,10pt]{article}
\usepackage[utf8]{inputenc}
\usepackage{pdfpages}
\usepackage{latexsym}
\usepackage{amssymb,amsthm,amsmath}
\usepackage{amsthm}

\begin{document}
 \newcommand{\nxt}{{\ensuremath\raisebox{0.25ex}{\text{\scriptsize$\bigcirc$}}}}
\newcommand{\Rdiamond}{\Diamond_{\!F}}
\newcommand{\Rbox}{\Box_{\!F}}
\newcommand{\Rnext}{\nxt_{\!F}}
\newcommand{\Ldiamond}{\Diamond_{\!P}}
\newcommand{\Lbox}{\Box_{\!P}}
\newcommand{\Lnext}{\nxt_{\!P}}
\newcommand{\SVdiamond}{\mathop{\ooalign{$\Diamond$ \cr \kern0.5ex
    \raisebox{0.35ex}{\scalebox{0.7}{$*$}}} \kern-0.9ex}}
\newcommand{\SVbox}{\mathop{\ooalign{$\Box$ \cr \kern0.42ex
    \raisebox{0.3ex}{\scalebox{0.7}{$*$}}} \kern-0.9ex}}


$( \SVbox (E1Salary_{S13} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{dSalaryInv} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S31} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S9} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S14} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S2} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S24} \rightarrow E1Salary_{S24}) \land $ \\ 
 $ (Person_{S24} \rightarrow  \lnot E2Salary_{S24}) \land $ \\ 
 $ (E2Salary_{S24} \rightarrow E1Salary_{S24})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{S30} \rightarrow E1Salary_{S30}) \land $ \\ 
 $ (Person_{S30} \rightarrow  \lnot E2Salary_{S30}) \land $ \\ 
 $ (E2Salary_{S30} \rightarrow E1Salary_{S30})) \land $ \\ 
 $  \SVbox (E1Salary_{S37} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S38} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{S34} \rightarrow E1Salary_{S34}) \land $ \\ 
 $ (Person_{S34} \rightarrow  \lnot E2Salary_{S34}) \land $ \\ 
 $ (E2Salary_{S34} \rightarrow E1Salary_{S34})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S32} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S26} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S24} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S25} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S39} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox ((Person_{S29} \rightarrow E1Salary_{S29}) \land $ \\ 
 $ (Person_{S29} \rightarrow  \lnot E2Salary_{S29}) \land $ \\ 
 $ (E2Salary_{S29} \rightarrow E1Salary_{S29})) \land $ \\ 
 $  \SVbox (E1Salary_{S26} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S11} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S14} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S28} \rightarrow E1Salary_{S28}) \land $ \\ 
 $ (Person_{S28} \rightarrow  \lnot E2Salary_{S28}) \land $ \\ 
 $ (E2Salary_{S28} \rightarrow E1Salary_{S28})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{John} \rightarrow E1Salary_{John}) \land $ \\ 
 $ (Person_{John} \rightarrow  \lnot E2Salary_{John}) \land $ \\ 
 $ (E2Salary_{John} \rightarrow E1Salary_{John})) \land $ \\ 
 $  \SVbox (E1Salary_{S34} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S17} \rightarrow E1Salary_{S17}) \land $ \\ 
 $ (Person_{S17} \rightarrow  \lnot E2Salary_{S17}) \land $ \\ 
 $ (E2Salary_{S17} \rightarrow E1Salary_{S17})) \land $ \\ 
 $  \SVbox (E1Salary_{S27} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S33} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox ((Person_{S9} \rightarrow E1Salary_{S9}) \land $ \\ 
 $ (Person_{S9} \rightarrow  \lnot E2Salary_{S9}) \land $ \\ 
 $ (E2Salary_{S9} \rightarrow E1Salary_{S9})) \land $ \\ 
 $  \SVbox (E1Salary_{S5} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S39} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S30} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S36} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S4} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S7} \rightarrow E1Salary_{S7}) \land $ \\ 
 $ (Person_{S7} \rightarrow  \lnot E2Salary_{S7}) \land $ \\ 
 $ (E2Salary_{S7} \rightarrow E1Salary_{S7})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S16} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S20} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S5} \rightarrow E1Salary_{S5}) \land $ \\ 
 $ (Person_{S5} \rightarrow  \lnot E2Salary_{S5}) \land $ \\ 
 $ (E2Salary_{S5} \rightarrow E1Salary_{S5})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{John} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S15} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S21} \rightarrow E1Salary_{S21}) \land $ \\ 
 $ (Person_{S21} \rightarrow  \lnot E2Salary_{S21}) \land $ \\ 
 $ (E2Salary_{S21} \rightarrow E1Salary_{S21})) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S7} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S16} \rightarrow E1Salary_{S16}) \land $ \\ 
 $ (Person_{S16} \rightarrow  \lnot E2Salary_{S16}) \land $ \\ 
 $ (E2Salary_{S16} \rightarrow E1Salary_{S16})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S6} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S29} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{dSalaryInv} \rightarrow E1Salary_{dSalaryInv}) \land $ \\ 
 $ (Person_{dSalaryInv} \rightarrow  \lnot E2Salary_{dSalaryInv}) \land $ \\ 
 $ (E2Salary_{dSalaryInv} \rightarrow E1Salary_{dSalaryInv})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S3} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S23} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S13} \rightarrow E1Salary_{S13}) \land $ \\ 
 $ (Person_{S13} \rightarrow  \lnot E2Salary_{S13}) \land $ \\ 
 $ (E2Salary_{S13} \rightarrow E1Salary_{S13})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{S35} \rightarrow E1Salary_{S35}) \land $ \\ 
 $ (Person_{S35} \rightarrow  \lnot E2Salary_{S35}) \land $ \\ 
 $ (E2Salary_{S35} \rightarrow E1Salary_{S35})) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox ((Person_{S33} \rightarrow E1Salary_{S33}) \land $ \\ 
 $ (Person_{S33} \rightarrow  \lnot E2Salary_{S33}) \land $ \\ 
 $ (E2Salary_{S33} \rightarrow E1Salary_{S33})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S24} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S3} \rightarrow E1Salary_{S3}) \land $ \\ 
 $ (Person_{S3} \rightarrow  \lnot E2Salary_{S3}) \land $ \\ 
 $ (E2Salary_{S3} \rightarrow E1Salary_{S3})) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S0} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{dSalaryInv} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S31} \rightarrow E1Salary_{S31}) \land $ \\ 
 $ (Person_{S31} \rightarrow  \lnot E2Salary_{S31}) \land $ \\ 
 $ (E2Salary_{S31} \rightarrow E1Salary_{S31})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S17} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S12} \rightarrow E1Salary_{S12}) \land $ \\ 
 $ (Person_{S12} \rightarrow  \lnot E2Salary_{S12}) \land $ \\ 
 $ (E2Salary_{S12} \rightarrow E1Salary_{S12})) \land $ \\ 
 $  \SVbox ((Person_{S0} \rightarrow E1Salary_{S0}) \land $ \\ 
 $ (Person_{S0} \rightarrow  \lnot E2Salary_{S0}) \land $ \\ 
 $ (E2Salary_{S0} \rightarrow E1Salary_{S0})) \land $ \\ 
 $  \SVbox (E1Salary_{S8} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S22} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{S26} \rightarrow E1Salary_{S26}) \land $ \\ 
 $ (Person_{S26} \rightarrow  \lnot E2Salary_{S26}) \land $ \\ 
 $ (E2Salary_{S26} \rightarrow E1Salary_{S26})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{S38} \rightarrow E1Salary_{S38}) \land $ \\ 
 $ (Person_{S38} \rightarrow  \lnot E2Salary_{S38}) \land $ \\ 
 $ (E2Salary_{S38} \rightarrow E1Salary_{S38})) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S30} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S31} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S36} \rightarrow E1Salary_{S36}) \land $ \\ 
 $ (Person_{S36} \rightarrow  \lnot E2Salary_{S36}) \land $ \\ 
 $ (E2Salary_{S36} \rightarrow E1Salary_{S36})) \land $ \\ 
 $  \SVbox (E1Salary_{S6} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S10} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S35} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S25} \rightarrow E1Salary_{S25}) \land $ \\ 
 $ (Person_{S25} \rightarrow  \lnot E2Salary_{S25}) \land $ \\ 
 $ (E2Salary_{S25} \rightarrow E1Salary_{S25})) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S5} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S33} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S1} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S9} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S10} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S15} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S12} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S11} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S37} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{dSalary} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S2} \rightarrow E1Salary_{S2}) \land $ \\ 
 $ (Person_{S2} \rightarrow  \lnot E2Salary_{S2}) \land $ \\ 
 $ (E2Salary_{S2} \rightarrow E1Salary_{S2})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S32} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{S6} \rightarrow E1Salary_{S6}) \land $ \\ 
 $ (Person_{S6} \rightarrow  \lnot E2Salary_{S6}) \land $ \\ 
 $ (E2Salary_{S6} \rightarrow E1Salary_{S6})) \land $ \\ 
 $  \SVbox ((Person_{S1} \rightarrow E1Salary_{S1}) \land $ \\ 
 $ (Person_{S1} \rightarrow  \lnot E2Salary_{S1}) \land $ \\ 
 $ (E2Salary_{S1} \rightarrow E1Salary_{S1})) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{S32} \rightarrow E1Salary_{S32}) \land $ \\ 
 $ (Person_{S32} \rightarrow  \lnot E2Salary_{S32}) \land $ \\ 
 $ (E2Salary_{S32} \rightarrow E1Salary_{S32})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S8} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S19} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S28} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S35} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S19} \rightarrow E1Salary_{S19}) \land $ \\ 
 $ (Person_{S19} \rightarrow  \lnot E2Salary_{S19}) \land $ \\ 
 $ (E2Salary_{S19} \rightarrow E1Salary_{S19})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S20} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox ((Person_{S11} \rightarrow E1Salary_{S11}) \land $ \\ 
 $ (Person_{S11} \rightarrow  \lnot E2Salary_{S11}) \land $ \\ 
 $ (E2Salary_{S11} \rightarrow E1Salary_{S11})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S25} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S23} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S17} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S13} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S23} \rightarrow E1Salary_{S23}) \land $ \\ 
 $ (Person_{S23} \rightarrow  \lnot E2Salary_{S23}) \land $ \\ 
 $ (E2Salary_{S23} \rightarrow E1Salary_{S23})) \land $ \\ 
 $  \SVbox ((Person_{S8} \rightarrow E1Salary_{S8}) \land $ \\ 
 $ (Person_{S8} \rightarrow  \lnot E2Salary_{S8}) \land $ \\ 
 $ (E2Salary_{S8} \rightarrow E1Salary_{S8})) \land $ \\ 
 $  \SVbox (E1Salary_{S22} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S27} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S20} \rightarrow E1Salary_{S20}) \land $ \\ 
 $ (Person_{S20} \rightarrow  \lnot E2Salary_{S20}) \land $ \\ 
 $ (E2Salary_{S20} \rightarrow E1Salary_{S20})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S0} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S1} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S22} \rightarrow E1Salary_{S22}) \land $ \\ 
 $ (Person_{S22} \rightarrow  \lnot E2Salary_{S22}) \land $ \\ 
 $ (E2Salary_{S22} \rightarrow E1Salary_{S22})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S36} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S16} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S27} \rightarrow E1Salary_{S27}) \land $ \\ 
 $ (Person_{S27} \rightarrow  \lnot E2Salary_{S27}) \land $ \\ 
 $ (E2Salary_{S27} \rightarrow E1Salary_{S27})) \land $ \\ 
 $  \SVbox (E1Salary_{S3} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S12} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox ((Person_{S18} \rightarrow E1Salary_{S18}) \land $ \\ 
 $ (Person_{S18} \rightarrow  \lnot E2Salary_{S18}) \land $ \\ 
 $ (E2Salary_{S18} \rightarrow E1Salary_{S18})) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S7} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S39} \rightarrow E1Salary_{S39}) \land $ \\ 
 $ (Person_{S39} \rightarrow  \lnot E2Salary_{S39}) \land $ \\ 
 $ (E2Salary_{S39} \rightarrow E1Salary_{S39})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{S10} \rightarrow E1Salary_{S10}) \land $ \\ 
 $ (Person_{S10} \rightarrow  \lnot E2Salary_{S10}) \land $ \\ 
 $ (E2Salary_{S10} \rightarrow E1Salary_{S10})) \land $ \\ 
 $  \SVbox (E1Salary_{dSalary} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S37} \rightarrow E1Salary_{S37}) \land $ \\ 
 $ (Person_{S37} \rightarrow  \lnot E2Salary_{S37}) \land $ \\ 
 $ (E2Salary_{S37} \rightarrow E1Salary_{S37})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{S14} \rightarrow E1Salary_{S14}) \land $ \\ 
 $ (Person_{S14} \rightarrow  \lnot E2Salary_{S14}) \land $ \\ 
 $ (E2Salary_{S14} \rightarrow E1Salary_{S14})) \land $ \\ 
 $  \SVbox (E1Salary_{S18} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S21} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S2} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S4} \rightarrow E1Salary_{S4}) \land $ \\ 
 $ (Person_{S4} \rightarrow  \lnot E2Salary_{S4}) \land $ \\ 
 $ (E2Salary_{S4} \rightarrow E1Salary_{S4})) \land $ \\ 
 $  \SVbox (E1Salary_{S29} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S28} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S4} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S34} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S19} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S21} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S18} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1Salary_{John} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{dSalary} \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (Person_{dSalary} \rightarrow  \lnot E2Salary_{dSalary}) \land $ \\ 
 $ (E2Salary_{dSalary} \rightarrow E1Salary_{dSalary})) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S38} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox ((Person_{S15} \rightarrow E1Salary_{S15}) \land $ \\ 
 $ (Person_{S15} \rightarrow  \lnot E2Salary_{S15}) \land $ \\ 
 $ (E2Salary_{S15} \rightarrow E1Salary_{S15})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S33} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S23} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S26} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S34} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S4} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S10} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S19} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S13} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S38} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S12} \land $ \\ 
 $  \Rnext E1SalaryInv_{S1} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S9} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S31} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S36} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S22} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S8} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S15} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S17} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S29} \land $ \\ 
 $  \Rnext  \Rnext E1SalaryInv_{S2} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S32} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S35} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S27} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S28} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S11} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S39} \land $ \\ 
 $  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S6} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S14} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S16} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S30} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S37} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E1SalaryInv_{S3} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S5} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S25} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S21} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S18} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S7} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S24} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInv_{S20} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E1Salary_{John} \land $ \\ 
 $ E1SalaryInv_{S0} \land $ \\ 
 $ E1Salary_{John} \land $ \\ 
 $ Person_{John})$ 
\end{document}