\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}}


$((PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S26} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S2} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{dSalaryInv} \rightarrow E1Salary_{dSalaryInv}) \land $ \\ 
 $ (Person_{dSalaryInv} \rightarrow  \lnot E2Salary_{dSalaryInv}) \land $ \\ 
 $ (E2Salary_{dSalaryInv} \rightarrow E1Salary_{dSalaryInv})) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{John} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S24} \rightarrow E1Salary_{S24}) \land $ \\ 
 $ (Person_{S24} \rightarrow  \lnot E2Salary_{S24}) \land $ \\ 
 $ (E2Salary_{S24} \rightarrow E1Salary_{S24})) \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 (E1SalaryInv_{S20} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S8} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \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 (E1SalaryInv_{S19} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S18} \rightarrow E1Salary_{S18}) \land $ \\ 
 $ (Person_{S18} \rightarrow  \lnot E2Salary_{S18}) \land $ \\ 
 $ (E2Salary_{S18} \rightarrow E1Salary_{S18})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S9} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S22} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S25} \rightarrow E1Salary_{S25}) \land $ \\ 
 $ (Person_{S25} \rightarrow  \lnot E2Salary_{S25}) \land $ \\ 
 $ (E2Salary_{S25} \rightarrow E1Salary_{S25})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S24} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S15} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S29} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S21} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{dSalaryInv} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S4} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S11} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S17} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S20} \rightarrow E1Salary_{S20}) \land $ \\ 
 $ (Person_{S20} \rightarrow  \lnot E2Salary_{S20}) \land $ \\ 
 $ (E2Salary_{S20} \rightarrow E1Salary_{S20})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \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 $ \\ 
 $  \SVbox (E1SalaryInv_{S3} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S15} \rightarrow E1Salary_{S15}) \land $ \\ 
 $ (Person_{S15} \rightarrow  \lnot E2Salary_{S15}) \land $ \\ 
 $ (E2Salary_{S15} \rightarrow E1Salary_{S15})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S29} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S5} \rightarrow E1Salary_{S5}) \land $ \\ 
 $ (Person_{S5} \rightarrow  \lnot E2Salary_{S5}) \land $ \\ 
 $ (E2Salary_{S5} \rightarrow E1Salary_{S5})) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox ((Person_{S10} \rightarrow E1Salary_{S10}) \land $ \\ 
 $ (Person_{S10} \rightarrow  \lnot E2Salary_{S10}) \land $ \\ 
 $ (E2Salary_{S10} \rightarrow E1Salary_{S10})) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S27} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S7} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S12} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{dSalary} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S10} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S28} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S6} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{John} \rightarrow E1Salary_{John}) \land $ \\ 
 $ (Person_{John} \rightarrow  \lnot E2Salary_{John}) \land $ \\ 
 $ (E2Salary_{John} \rightarrow E1Salary_{John})) \land $ \\ 
 $  \SVbox (E1Salary_{S13} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S14} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S18} \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 ((Person_{S19} \rightarrow E1Salary_{S19}) \land $ \\ 
 $ (Person_{S19} \rightarrow  \lnot E2Salary_{S19}) \land $ \\ 
 $ (E2Salary_{S19} \rightarrow E1Salary_{S19})) \land $ \\ 
 $  \SVbox ((Person_{S6} \rightarrow E1Salary_{S6}) \land $ \\ 
 $ (Person_{S6} \rightarrow  \lnot E2Salary_{S6}) \land $ \\ 
 $ (E2Salary_{S6} \rightarrow E1Salary_{S6})) \land $ \\ 
 $  \SVbox (E1Salary_{S3} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S19} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S22} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S4} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S5} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S14} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S6} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S23} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox ((Person_{S1} \rightarrow E1Salary_{S1}) \land $ \\ 
 $ (Person_{S1} \rightarrow  \lnot E2Salary_{S1}) \land $ \\ 
 $ (E2Salary_{S1} \rightarrow E1Salary_{S1})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S1} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S16} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{John} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S23} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S25} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S12} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S17} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S16} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S15} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S20} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S0} \rightarrow E1Salary_{S0}) \land $ \\ 
 $ (Person_{S0} \rightarrow  \lnot E2Salary_{S0}) \land $ \\ 
 $ (E2Salary_{S0} \rightarrow E1Salary_{S0})) \land $ \\ 
 $  \SVbox (E1Salary_{S0} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S8} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{dSalaryInv} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1Salary_{S2} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox ((Person_{S28} \rightarrow E1Salary_{S28}) \land $ \\ 
 $ (Person_{S28} \rightarrow  \lnot E2Salary_{S28}) \land $ \\ 
 $ (E2Salary_{S28} \rightarrow E1Salary_{S28})) \land $ \\ 
 $  \SVbox (E1Salary_{S1} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S13} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S11} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox ((Person_{S22} \rightarrow E1Salary_{S22}) \land $ \\ 
 $ (Person_{S22} \rightarrow  \lnot E2Salary_{S22}) \land $ \\ 
 $ (E2Salary_{S22} \rightarrow E1Salary_{S22})) \land $ \\ 
 $  \SVbox ((Person_{S29} \rightarrow E1Salary_{S29}) \land $ \\ 
 $ (Person_{S29} \rightarrow  \lnot E2Salary_{S29}) \land $ \\ 
 $ (E2Salary_{S29} \rightarrow E1Salary_{S29})) \land $ \\ 
 $  \SVbox ((Person_{S17} \rightarrow E1Salary_{S17}) \land $ \\ 
 $ (Person_{S17} \rightarrow  \lnot E2Salary_{S17}) \land $ \\ 
 $ (E2Salary_{S17} \rightarrow E1Salary_{S17})) \land $ \\ 
 $  \SVbox ((Person_{dSalary} \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (Person_{dSalary} \rightarrow  \lnot E2Salary_{dSalary}) \land $ \\ 
 $ (E2Salary_{dSalary} \rightarrow E1Salary_{dSalary})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{dSalary} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S26} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S16} \rightarrow E1Salary_{S16}) \land $ \\ 
 $ (Person_{S16} \rightarrow  \lnot E2Salary_{S16}) \land $ \\ 
 $ (E2Salary_{S16} \rightarrow E1Salary_{S16})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{S7} \rightarrow E1Salary_{S7}) \land $ \\ 
 $ (Person_{S7} \rightarrow  \lnot E2Salary_{S7}) \land $ \\ 
 $ (E2Salary_{S7} \rightarrow E1Salary_{S7})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S18} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S21} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1Salary_{S27} \rightarrow  \SVbox PSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S24} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S25} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S26} \rightarrow E1Salary_{S26}) \land $ \\ 
 $ (Person_{S26} \rightarrow  \lnot E2Salary_{S26}) \land $ \\ 
 $ (E2Salary_{S26} \rightarrow E1Salary_{S26})) \land $ \\ 
 $  \SVbox ((Person_{S13} \rightarrow E1Salary_{S13}) \land $ \\ 
 $ (Person_{S13} \rightarrow  \lnot E2Salary_{S13}) \land $ \\ 
 $ (E2Salary_{S13} \rightarrow E1Salary_{S13})) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S7} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox ((Person_{S12} \rightarrow E1Salary_{S12}) \land $ \\ 
 $ (Person_{S12} \rightarrow  \lnot E2Salary_{S12}) \land $ \\ 
 $ (E2Salary_{S12} \rightarrow E1Salary_{S12})) \land $ \\ 
 $  \SVbox ((Person_{S4} \rightarrow E1Salary_{S4}) \land $ \\ 
 $ (Person_{S4} \rightarrow  \lnot E2Salary_{S4}) \land $ \\ 
 $ (E2Salary_{S4} \rightarrow E1Salary_{S4})) \land $ \\ 
 $  \SVbox ((Person_{S9} \rightarrow E1Salary_{S9}) \land $ \\ 
 $ (Person_{S9} \rightarrow  \lnot E2Salary_{S9}) \land $ \\ 
 $ (E2Salary_{S9} \rightarrow E1Salary_{S9})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox ((Person_{S23} \rightarrow E1Salary_{S23}) \land $ \\ 
 $ (Person_{S23} \rightarrow  \lnot E2Salary_{S23}) \land $ \\ 
 $ (E2Salary_{S23} \rightarrow E1Salary_{S23})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox ((Person_{S8} \rightarrow E1Salary_{S8}) \land $ \\ 
 $ (Person_{S8} \rightarrow  \lnot E2Salary_{S8}) \land $ \\ 
 $ (E2Salary_{S8} \rightarrow E1Salary_{S8})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S5} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S10} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1Salary_{S9} \rightarrow  \SVbox PSalary) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S28} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S11} \rightarrow E1Salary_{S11}) \land $ \\ 
 $ (Person_{S11} \rightarrow  \lnot E2Salary_{S11}) \land $ \\ 
 $ (E2Salary_{S11} \rightarrow E1Salary_{S11})) \land $ \\ 
 $ (PSalary \rightarrow E1SalaryInv_{dSalaryInv}) \land $ \\ 
 $  \SVbox (E1SalaryInv_{S0} \rightarrow  \SVbox PinvSalary) \land $ \\ 
 $  \SVbox ((Person_{S2} \rightarrow E1Salary_{S2}) \land $ \\ 
 $ (Person_{S2} \rightarrow  \lnot E2Salary_{S2}) \land $ \\ 
 $ (E2Salary_{S2} \rightarrow E1Salary_{S2})) \land $ \\ 
 $ (PinvSalary \rightarrow E1Salary_{dSalary}) \land $ \\ 
 $ E1SalaryInv_{S18} \land $ \\ 
 $ E1SalaryInv_{S29} \land $ \\ 
 $ E1SalaryInv_{S0} \land $ \\ 
 $ E1SalaryInv_{S25} \land $ \\ 
 $ E1SalaryInv_{S17} \land $ \\ 
 $ E1SalaryInv_{S11} \land $ \\ 
 $ E1SalaryInv_{S15} \land $ \\ 
 $ E1SalaryInv_{S19} \land $ \\ 
 $ E1SalaryInv_{S12} \land $ \\ 
 $ E1SalaryInv_{S9} \land $ \\ 
 $ E1SalaryInv_{S16} \land $ \\ 
 $ E1SalaryInv_{S14} \land $ \\ 
 $ E1SalaryInv_{S2} \land $ \\ 
 $ E1SalaryInv_{S1} \land $ \\ 
 $ E1SalaryInv_{S10} \land $ \\ 
 $ E1SalaryInv_{S5} \land $ \\ 
 $ E1SalaryInv_{S13} \land $ \\ 
 $ E1SalaryInv_{S26} \land $ \\ 
 $ E1SalaryInv_{S27} \land $ \\ 
 $ E1SalaryInv_{S24} \land $ \\ 
 $ E1SalaryInv_{S4} \land $ \\ 
 $ E1SalaryInv_{S7} \land $ \\ 
 $ E1SalaryInv_{S3} \land $ \\ 
 $ E1SalaryInv_{S23} \land $ \\ 
 $ E1SalaryInv_{S22} \land $ \\ 
 $ E1SalaryInv_{S20} \land $ \\ 
 $ E1SalaryInv_{S21} \land $ \\ 
 $ E1SalaryInv_{S8} \land $ \\ 
 $ E1SalaryInv_{S28} \land $ \\ 
 $ E1SalaryInv_{S6} \land $ \\ 
 $ Person_{John} \land $ \\ 
 $ E2Salary_{John})$ 
\end{document}