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


$( \forall X. ((PinvSalaryF \rightarrow E1SalaryF(dSalary)) \land $ \\ 
 $ BOX2F(X) \land $ \\ 
 $ BOX0F(X) \land $ \\ 
 $ BOX1F(X) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF(dSalaryInv)) \land $ \\ 
 $  \Rbox (( \Rnext BOX11F(X) \leftrightarrow (BOX11F(X) \land $ \\ 
 $  \Rnext BOX12F(X))) \land $ \\ 
 $ (BOX7P(X) \leftrightarrow  \Rbox BOX8P(X)) \land $ \\ 
 $ ( \Rnext BOX8P(X) \leftrightarrow (BOX8P(X) \land $ \\ 
 $  \Rnext PinvSalaryF)) \land $ \\ 
 $ (BOX16F(X) \leftrightarrow  \Rbox ((PersonF(X) \rightarrow E1SalaryF(X)) \land $ \\ 
 $ (PersonF(X) \rightarrow  \lnot E2SalaryF(X)) \land $ \\ 
 $ (E2SalaryF(X) \rightarrow E1SalaryF(X)))) \land $ \\ 
 $ (BOX19P(X) \leftrightarrow  \Rbox BOX9P(X)) \land $ \\ 
 $ (BOX4P(X) \leftrightarrow  \Rbox BOX5P(X)) \land $ \\ 
 $ (BOX12F(X) \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ (BOX17P(X) \leftrightarrow  \Rbox BOX3P(X)) \land $ \\ 
 $ ( \Rnext BOX9P(X) \leftrightarrow (BOX9P(X) \land $ \\ 
 $  \Rnext ((PersonP(X) \rightarrow E1SalaryP(X)) \land $ \\ 
 $ (PersonP(X) \rightarrow  \lnot E2SalaryP(X)) \land $ \\ 
 $ (E2SalaryP(X) \rightarrow E1SalaryP(X))))) \land $ \\ 
 $ (BOX18P(X) \leftrightarrow  \Rbox BOX6P(X)) \land $ \\ 
 $ ( \Rnext BOX14F(X) \leftrightarrow (BOX14F(X) \land $ \\ 
 $  \Rnext BOX15F(X))) \land $ \\ 
 $ (BOX13F(X) \leftrightarrow  \Rbox (E1SalaryInvF(X) \rightarrow BOX14F(X))) \land $ \\ 
 $ (BOX15F(X) \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ ( \Rnext BOX2F(X) \leftrightarrow (BOX2F(X) \land $ \\ 
 $  \Rnext BOX16F(X))) \land $ \\ 
 $ ( \Rnext BOX1F(X) \leftrightarrow (BOX1F(X) \land $ \\ 
 $  \Rnext BOX13F(X))) \land $ \\ 
 $ ( \Rnext BOX3P(X) \leftrightarrow (BOX3P(X) \land $ \\ 
 $  \Rnext (E1SalaryP(X) \rightarrow BOX4P(X)))) \land $ \\ 
 $ ( \Rnext BOX5P(X) \leftrightarrow (BOX5P(X) \land $ \\ 
 $  \Rnext PSalaryF)) \land $ \\ 
 $ (BOX10F(X) \leftrightarrow  \Rbox (E1SalaryF(X) \rightarrow BOX11F(X))) \land $ \\ 
 $ ( \Rnext BOX0F(X) \leftrightarrow (BOX0F(X) \land $ \\ 
 $  \Rnext BOX10F(X))) \land $ \\ 
 $ ( \Rnext BOX6P(X) \leftrightarrow (BOX6P(X) \land $ \\ 
 $  \Rnext (E1SalaryInvP(X) \rightarrow BOX7P(X))))) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (E2SalaryF(X) \leftrightarrow E2SalaryP(X)) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX0F(X) \leftrightarrow BOX17P(X)) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (BOX10F(X) \leftrightarrow BOX3P(X)) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX2F(X) \leftrightarrow BOX19P(X)) \land $ \\ 
 $ (E1SalaryInvF(X) \leftrightarrow E1SalaryInvP(X)) \land $ \\ 
 $ (BOX15F(X) \leftrightarrow BOX8P(X)) \land $ \\ 
 $ (BOX13F(X) \leftrightarrow BOX6P(X)) \land $ \\ 
 $ (E1SalaryInvF(dSalaryInv) \leftrightarrow E1SalaryInvP(dSalaryInv)) \land $ \\ 
 $ (E1SalaryF(dSalary) \leftrightarrow E1SalaryP(dSalary)) \land $ \\ 
 $ (BOX1F(X) \leftrightarrow BOX18P(X)) \land $ \\ 
 $ (BOX14F(X) \leftrightarrow BOX7P(X)) \land $ \\ 
 $ (E1SalaryF(X) \leftrightarrow E1SalaryP(X)) \land $ \\ 
 $ (BOX12F(X) \leftrightarrow BOX5P(X)) \land $ \\ 
 $ (BOX16F(X) \leftrightarrow BOX9P(X)) \land $ \\ 
 $ (PersonF(X) \leftrightarrow PersonP(X)) \land $ \\ 
 $ (BOX11F(X) \leftrightarrow BOX4P(X))) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S20) \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 E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(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 E1SalaryF(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 E1SalaryInvF(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 E1SalaryInvF(S28) \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 E1SalaryF(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 E1SalaryInvF(S30) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S21) \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 E1SalaryInvF(S39) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(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 E1SalaryInvF(S36) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S7) \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 E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S16) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext E1SalaryInvF(S2) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S19) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $ E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S13) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E1SalaryInvF(S3) \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 E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S4) \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 E1SalaryF(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 E1SalaryInvF(S32) \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 E1SalaryF(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 E1SalaryInvF(S24) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S15) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S14) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(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 E1SalaryInvF(S38) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(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 E1SalaryF(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 E1SalaryF(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 E1SalaryInvF(S23) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext E1SalaryInvF(S1) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S18) \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 E1SalaryF(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 E1SalaryInvF(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 E1SalaryInvF(S27) \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 E1SalaryInvF(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  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(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 E1SalaryInvF(S33) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(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 E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(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  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S12) \land $ \\ 
 $  \Rnext E1SalaryF(John) \land $ \\ 
 $ E1SalaryInvF(S0) \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 E1SalaryF(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 E1SalaryInvF(S37) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S22) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S6) \land $ \\ 
 $ PersonF(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 E1SalaryInvF(S29) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S8) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(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 E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S10) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(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 E1SalaryInvF(S34) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF(S9) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext E1SalaryF(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 E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(John) \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryF(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 E1SalaryInvF(S25))$ 
\end{document}