\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 $ \\ 
 $ E1SalaryF(John) \land $ \\ 
 $ E1SalaryInvF(S1) \land $ \\ 
 $ PersonF(John))$ 
\end{document}