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


$((PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (BOX2F_{dSalary} \leftrightarrow BOX19P_{dSalary}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (PersonF_{John} \leftrightarrow PersonP_{John}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (PersonF_{S1} \leftrightarrow PersonP_{S1}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX14F_{John} \leftrightarrow BOX7P_{John}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX1F_{John} \leftrightarrow BOX18P_{John}) \land $ \\ 
 $ (BOX1F_{S1} \leftrightarrow BOX18P_{S1}) \land $ \\ 
 $  \Rbox ((BOX12F_{S1} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S1} \leftrightarrow ( \Rnext ((PersonP_{S1} \rightarrow E1SalaryP_{S1}) \land $ \\ 
 $ (PersonP_{S1} \rightarrow  \lnot E2SalaryP_{S1}) \land $ \\ 
 $ (E2SalaryP_{S1} \rightarrow E1SalaryP_{S1})) \land $ \\ 
 $ BOX9P_{S1})) \land $ \\ 
 $ ( \Rnext BOX14F_{S1} \leftrightarrow ( \Rnext BOX15F_{S1} \land $ \\ 
 $ BOX14F_{S1})) \land $ \\ 
 $ (BOX17P_{S1} \leftrightarrow  \Rbox BOX3P_{S1}) \land $ \\ 
 $ (BOX13F_{S1} \leftrightarrow  \Rbox (E1SalaryInvF_{S1} \rightarrow BOX14F_{S1})) \land $ \\ 
 $ (BOX10F_{S1} \leftrightarrow  \Rbox (E1SalaryF_{S1} \rightarrow BOX11F_{S1})) \land $ \\ 
 $ ( \Rnext BOX8P_{S1} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S1})) \land $ \\ 
 $ (BOX7P_{S1} \leftrightarrow  \Rbox BOX8P_{S1}) \land $ \\ 
 $ ( \Rnext BOX5P_{S1} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S1})) \land $ \\ 
 $ (BOX18P_{S1} \leftrightarrow  \Rbox BOX6P_{S1}) \land $ \\ 
 $ ( \Rnext BOX11F_{S1} \leftrightarrow ( \Rnext BOX12F_{S1} \land $ \\ 
 $ BOX11F_{S1})) \land $ \\ 
 $ ( \Rnext BOX1F_{S1} \leftrightarrow ( \Rnext BOX13F_{S1} \land $ \\ 
 $ BOX1F_{S1})) \land $ \\ 
 $ (BOX19P_{S1} \leftrightarrow  \Rbox BOX9P_{S1}) \land $ \\ 
 $ ( \Rnext BOX6P_{S1} \leftrightarrow ( \Rnext (E1SalaryInvP_{S1} \rightarrow BOX7P_{S1}) \land $ \\ 
 $ BOX6P_{S1})) \land $ \\ 
 $ ( \Rnext BOX3P_{S1} \leftrightarrow ( \Rnext (E1SalaryP_{S1} \rightarrow BOX4P_{S1}) \land $ \\ 
 $ BOX3P_{S1})) \land $ \\ 
 $ ( \Rnext BOX2F_{S1} \leftrightarrow ( \Rnext BOX16F_{S1} \land $ \\ 
 $ BOX2F_{S1})) \land $ \\ 
 $ (BOX4P_{S1} \leftrightarrow  \Rbox BOX5P_{S1}) \land $ \\ 
 $ (BOX15F_{S1} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S1} \leftrightarrow  \Rbox ((PersonF_{S1} \rightarrow E1SalaryF_{S1}) \land $ \\ 
 $ (PersonF_{S1} \rightarrow  \lnot E2SalaryF_{S1}) \land $ \\ 
 $ (E2SalaryF_{S1} \rightarrow E1SalaryF_{S1}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S1} \leftrightarrow ( \Rnext BOX10F_{S1} \land $ \\ 
 $ BOX0F_{S1}))) \land $ \\ 
 $ (PersonF_{dSalary} \leftrightarrow PersonP_{dSalary}) \land $ \\ 
 $ (BOX0F_{John} \leftrightarrow BOX17P_{John}) \land $ \\ 
 $ (BOX13F_{dSalaryInv} \leftrightarrow BOX6P_{dSalaryInv}) \land $ \\ 
 $ (BOX0F_{S1} \leftrightarrow BOX17P_{S1}) \land $ \\ 
 $ (E1SalaryInvF_{dSalary} \leftrightarrow E1SalaryInvP_{dSalary}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (PersonF_{dSalaryInv} \leftrightarrow PersonP_{dSalaryInv}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (BOX16F_{dSalaryInv} \leftrightarrow BOX9P_{dSalaryInv}) \land $ \\ 
 $ (BOX2F_{S1} \leftrightarrow BOX19P_{S1}) \land $ \\ 
 $ (BOX13F_{John} \leftrightarrow BOX6P_{John}) \land $ \\ 
 $ (E2SalaryF_{dSalaryInv} \leftrightarrow E2SalaryP_{dSalaryInv}) \land $ \\ 
 $ (E2SalaryF_{dSalary} \leftrightarrow E2SalaryP_{dSalary}) \land $ \\ 
 $ (BOX10F_{S1} \leftrightarrow BOX3P_{S1}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX15F_{dSalary} \leftrightarrow BOX8P_{dSalary}) \land $ \\ 
 $ (BOX0F_{dSalaryInv} \leftrightarrow BOX17P_{dSalaryInv}) \land $ \\ 
 $ (E1SalaryInvF_{John} \leftrightarrow E1SalaryInvP_{John}) \land $ \\ 
 $ (BOX15F_{John} \leftrightarrow BOX8P_{John}) \land $ \\ 
 $ (BOX1F_{dSalaryInv} \leftrightarrow BOX18P_{dSalaryInv}) \land $ \\ 
 $ (BOX11F_{dSalaryInv} \leftrightarrow BOX4P_{dSalaryInv}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (BOX10F_{John} \leftrightarrow BOX3P_{John}) \land $ \\ 
 $ (BOX11F_{S1} \leftrightarrow BOX4P_{S1}) \land $ \\ 
 $ (BOX1F_{dSalary} \leftrightarrow BOX18P_{dSalary}) \land $ \\ 
 $ (BOX16F_{John} \leftrightarrow BOX9P_{John}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX12F_{John} \leftrightarrow BOX5P_{John}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (E2SalaryF_{John} \leftrightarrow E2SalaryP_{John}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (BOX11F_{John} \leftrightarrow BOX4P_{John}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (BOX0F_{dSalary} \leftrightarrow BOX17P_{dSalary}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX14F_{dSalaryInv} \leftrightarrow BOX7P_{dSalaryInv}) \land $ \\ 
 $ (BOX15F_{dSalaryInv} \leftrightarrow BOX8P_{dSalaryInv}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX11F_{dSalary} \leftrightarrow BOX4P_{dSalary}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX16F_{S1} \leftrightarrow BOX9P_{S1}) \land $ \\ 
 $ (E2SalaryF_{S1} \leftrightarrow E2SalaryP_{S1}) \land $ \\ 
 $ (BOX10F_{dSalary} \leftrightarrow BOX3P_{dSalary}) \land $ \\ 
 $ (BOX2F_{dSalaryInv} \leftrightarrow BOX19P_{dSalaryInv}) \land $ \\ 
 $ (E1SalaryF_{S1} \leftrightarrow E1SalaryP_{S1}) \land $ \\ 
 $ (BOX12F_{S1} \leftrightarrow BOX5P_{S1}) \land $ \\ 
 $ (E1SalaryInvF_{S1} \leftrightarrow E1SalaryInvP_{S1}) \land $ \\ 
 $ (BOX15F_{S1} \leftrightarrow BOX8P_{S1}) \land $ \\ 
 $ (BOX10F_{dSalaryInv} \leftrightarrow BOX3P_{dSalaryInv}) \land $ \\ 
 $ (E1SalaryF_{John} \leftrightarrow E1SalaryP_{John}) \land $ \\ 
 $  \Rbox ((BOX12F_{dSalary} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{dSalary} \leftrightarrow ( \Rnext ((PersonP_{dSalary} \rightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (PersonP_{dSalary} \rightarrow  \lnot E2SalaryP_{dSalary}) \land $ \\ 
 $ (E2SalaryP_{dSalary} \rightarrow E1SalaryP_{dSalary})) \land $ \\ 
 $ BOX9P_{dSalary})) \land $ \\ 
 $ ( \Rnext BOX14F_{dSalary} \leftrightarrow ( \Rnext BOX15F_{dSalary} \land $ \\ 
 $ BOX14F_{dSalary})) \land $ \\ 
 $ (BOX17P_{dSalary} \leftrightarrow  \Rbox BOX3P_{dSalary}) \land $ \\ 
 $ (BOX13F_{dSalary} \leftrightarrow  \Rbox (E1SalaryInvF_{dSalary} \rightarrow BOX14F_{dSalary})) \land $ \\ 
 $ (BOX10F_{dSalary} \leftrightarrow  \Rbox (E1SalaryF_{dSalary} \rightarrow BOX11F_{dSalary})) \land $ \\ 
 $ ( \Rnext BOX8P_{dSalary} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{dSalary})) \land $ \\ 
 $ (BOX7P_{dSalary} \leftrightarrow  \Rbox BOX8P_{dSalary}) \land $ \\ 
 $ ( \Rnext BOX5P_{dSalary} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{dSalary})) \land $ \\ 
 $ (BOX18P_{dSalary} \leftrightarrow  \Rbox BOX6P_{dSalary}) \land $ \\ 
 $ ( \Rnext BOX11F_{dSalary} \leftrightarrow ( \Rnext BOX12F_{dSalary} \land $ \\ 
 $ BOX11F_{dSalary})) \land $ \\ 
 $ ( \Rnext BOX1F_{dSalary} \leftrightarrow ( \Rnext BOX13F_{dSalary} \land $ \\ 
 $ BOX1F_{dSalary})) \land $ \\ 
 $ (BOX19P_{dSalary} \leftrightarrow  \Rbox BOX9P_{dSalary}) \land $ \\ 
 $ ( \Rnext BOX6P_{dSalary} \leftrightarrow ( \Rnext (E1SalaryInvP_{dSalary} \rightarrow BOX7P_{dSalary}) \land $ \\ 
 $ BOX6P_{dSalary})) \land $ \\ 
 $ ( \Rnext BOX3P_{dSalary} \leftrightarrow ( \Rnext (E1SalaryP_{dSalary} \rightarrow BOX4P_{dSalary}) \land $ \\ 
 $ BOX3P_{dSalary})) \land $ \\ 
 $ ( \Rnext BOX2F_{dSalary} \leftrightarrow ( \Rnext BOX16F_{dSalary} \land $ \\ 
 $ BOX2F_{dSalary})) \land $ \\ 
 $ (BOX4P_{dSalary} \leftrightarrow  \Rbox BOX5P_{dSalary}) \land $ \\ 
 $ (BOX15F_{dSalary} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{dSalary} \leftrightarrow  \Rbox ((PersonF_{dSalary} \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (PersonF_{dSalary} \rightarrow  \lnot E2SalaryF_{dSalary}) \land $ \\ 
 $ (E2SalaryF_{dSalary} \rightarrow E1SalaryF_{dSalary}))) \land $ \\ 
 $ ( \Rnext BOX0F_{dSalary} \leftrightarrow ( \Rnext BOX10F_{dSalary} \land $ \\ 
 $ BOX0F_{dSalary}))) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX12F_{dSalaryInv} \leftrightarrow BOX5P_{dSalaryInv}) \land $ \\ 
 $ (BOX14F_{dSalary} \leftrightarrow BOX7P_{dSalary}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $  \Rbox ((BOX12F_{John} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{John} \leftrightarrow ( \Rnext ((PersonP_{John} \rightarrow E1SalaryP_{John}) \land $ \\ 
 $ (PersonP_{John} \rightarrow  \lnot E2SalaryP_{John}) \land $ \\ 
 $ (E2SalaryP_{John} \rightarrow E1SalaryP_{John})) \land $ \\ 
 $ BOX9P_{John})) \land $ \\ 
 $ ( \Rnext BOX14F_{John} \leftrightarrow ( \Rnext BOX15F_{John} \land $ \\ 
 $ BOX14F_{John})) \land $ \\ 
 $ (BOX17P_{John} \leftrightarrow  \Rbox BOX3P_{John}) \land $ \\ 
 $ (BOX13F_{John} \leftrightarrow  \Rbox (E1SalaryInvF_{John} \rightarrow BOX14F_{John})) \land $ \\ 
 $ (BOX10F_{John} \leftrightarrow  \Rbox (E1SalaryF_{John} \rightarrow BOX11F_{John})) \land $ \\ 
 $ ( \Rnext BOX8P_{John} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{John})) \land $ \\ 
 $ (BOX7P_{John} \leftrightarrow  \Rbox BOX8P_{John}) \land $ \\ 
 $ ( \Rnext BOX5P_{John} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{John})) \land $ \\ 
 $ (BOX18P_{John} \leftrightarrow  \Rbox BOX6P_{John}) \land $ \\ 
 $ ( \Rnext BOX11F_{John} \leftrightarrow ( \Rnext BOX12F_{John} \land $ \\ 
 $ BOX11F_{John})) \land $ \\ 
 $ ( \Rnext BOX1F_{John} \leftrightarrow ( \Rnext BOX13F_{John} \land $ \\ 
 $ BOX1F_{John})) \land $ \\ 
 $ (BOX19P_{John} \leftrightarrow  \Rbox BOX9P_{John}) \land $ \\ 
 $ ( \Rnext BOX6P_{John} \leftrightarrow ( \Rnext (E1SalaryInvP_{John} \rightarrow BOX7P_{John}) \land $ \\ 
 $ BOX6P_{John})) \land $ \\ 
 $ ( \Rnext BOX3P_{John} \leftrightarrow ( \Rnext (E1SalaryP_{John} \rightarrow BOX4P_{John}) \land $ \\ 
 $ BOX3P_{John})) \land $ \\ 
 $ ( \Rnext BOX2F_{John} \leftrightarrow ( \Rnext BOX16F_{John} \land $ \\ 
 $ BOX2F_{John})) \land $ \\ 
 $ (BOX4P_{John} \leftrightarrow  \Rbox BOX5P_{John}) \land $ \\ 
 $ (BOX15F_{John} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{John} \leftrightarrow  \Rbox ((PersonF_{John} \rightarrow E1SalaryF_{John}) \land $ \\ 
 $ (PersonF_{John} \rightarrow  \lnot E2SalaryF_{John}) \land $ \\ 
 $ (E2SalaryF_{John} \rightarrow E1SalaryF_{John}))) \land $ \\ 
 $ ( \Rnext BOX0F_{John} \leftrightarrow ( \Rnext BOX10F_{John} \land $ \\ 
 $ BOX0F_{John}))) \land $ \\ 
 $ (BOX14F_{S1} \leftrightarrow BOX7P_{S1}) \land $ \\ 
 $ (BOX16F_{dSalary} \leftrightarrow BOX9P_{dSalary}) \land $ \\ 
 $ (E1SalaryF_{dSalaryInv} \leftrightarrow E1SalaryP_{dSalaryInv}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (BOX13F_{dSalary} \leftrightarrow BOX6P_{dSalary}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (BOX2F_{John} \leftrightarrow BOX19P_{John}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX13F_{S1} \leftrightarrow BOX6P_{S1}) \land $ \\ 
 $ (BOX12F_{dSalary} \leftrightarrow BOX5P_{dSalary}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $  \Rbox ((BOX12F_{dSalaryInv} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{dSalaryInv} \leftrightarrow ( \Rnext ((PersonP_{dSalaryInv} \rightarrow E1SalaryP_{dSalaryInv}) \land $ \\ 
 $ (PersonP_{dSalaryInv} \rightarrow  \lnot E2SalaryP_{dSalaryInv}) \land $ \\ 
 $ (E2SalaryP_{dSalaryInv} \rightarrow E1SalaryP_{dSalaryInv})) \land $ \\ 
 $ BOX9P_{dSalaryInv})) \land $ \\ 
 $ ( \Rnext BOX14F_{dSalaryInv} \leftrightarrow ( \Rnext BOX15F_{dSalaryInv} \land $ \\ 
 $ BOX14F_{dSalaryInv})) \land $ \\ 
 $ (BOX17P_{dSalaryInv} \leftrightarrow  \Rbox BOX3P_{dSalaryInv}) \land $ \\ 
 $ (BOX13F_{dSalaryInv} \leftrightarrow  \Rbox (E1SalaryInvF_{dSalaryInv} \rightarrow BOX14F_{dSalaryInv})) \land $ \\ 
 $ (BOX10F_{dSalaryInv} \leftrightarrow  \Rbox (E1SalaryF_{dSalaryInv} \rightarrow BOX11F_{dSalaryInv})) \land $ \\ 
 $ ( \Rnext BOX8P_{dSalaryInv} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{dSalaryInv})) \land $ \\ 
 $ (BOX7P_{dSalaryInv} \leftrightarrow  \Rbox BOX8P_{dSalaryInv}) \land $ \\ 
 $ ( \Rnext BOX5P_{dSalaryInv} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{dSalaryInv})) \land $ \\ 
 $ (BOX18P_{dSalaryInv} \leftrightarrow  \Rbox BOX6P_{dSalaryInv}) \land $ \\ 
 $ ( \Rnext BOX11F_{dSalaryInv} \leftrightarrow ( \Rnext BOX12F_{dSalaryInv} \land $ \\ 
 $ BOX11F_{dSalaryInv})) \land $ \\ 
 $ ( \Rnext BOX1F_{dSalaryInv} \leftrightarrow ( \Rnext BOX13F_{dSalaryInv} \land $ \\ 
 $ BOX1F_{dSalaryInv})) \land $ \\ 
 $ (BOX19P_{dSalaryInv} \leftrightarrow  \Rbox BOX9P_{dSalaryInv}) \land $ \\ 
 $ ( \Rnext BOX6P_{dSalaryInv} \leftrightarrow ( \Rnext (E1SalaryInvP_{dSalaryInv} \rightarrow BOX7P_{dSalaryInv}) \land $ \\ 
 $ BOX6P_{dSalaryInv})) \land $ \\ 
 $ ( \Rnext BOX3P_{dSalaryInv} \leftrightarrow ( \Rnext (E1SalaryP_{dSalaryInv} \rightarrow BOX4P_{dSalaryInv}) \land $ \\ 
 $ BOX3P_{dSalaryInv})) \land $ \\ 
 $ ( \Rnext BOX2F_{dSalaryInv} \leftrightarrow ( \Rnext BOX16F_{dSalaryInv} \land $ \\ 
 $ BOX2F_{dSalaryInv})) \land $ \\ 
 $ (BOX4P_{dSalaryInv} \leftrightarrow  \Rbox BOX5P_{dSalaryInv}) \land $ \\ 
 $ (BOX15F_{dSalaryInv} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{dSalaryInv} \leftrightarrow  \Rbox ((PersonF_{dSalaryInv} \rightarrow E1SalaryF_{dSalaryInv}) \land $ \\ 
 $ (PersonF_{dSalaryInv} \rightarrow  \lnot E2SalaryF_{dSalaryInv}) \land $ \\ 
 $ (E2SalaryF_{dSalaryInv} \rightarrow E1SalaryF_{dSalaryInv}))) \land $ \\ 
 $ ( \Rnext BOX0F_{dSalaryInv} \leftrightarrow ( \Rnext BOX10F_{dSalaryInv} \land $ \\ 
 $ BOX0F_{dSalaryInv}))) \land $ \\ 
 $ BOX1F_{dSalaryInv} \land $ \\ 
 $ BOX1F_{dSalary} \land $ \\ 
 $ BOX1F_{John} \land $ \\ 
 $ BOX1F_{S1} \land $ \\ 
 $ BOX2F_{dSalaryInv} \land $ \\ 
 $ BOX2F_{dSalary} \land $ \\ 
 $ BOX2F_{John} \land $ \\ 
 $ BOX2F_{S1} \land $ \\ 
 $ BOX0F_{dSalaryInv} \land $ \\ 
 $ BOX0F_{dSalary} \land $ \\ 
 $ BOX0F_{John} \land $ \\ 
 $ BOX0F_{S1} \land $ \\ 
 $ E1SalaryF_{John} \land $ \\ 
 $ E1SalaryInvF_{S1} \land $ \\ 
 $ PersonF_{John})$ 
\end{document}