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


$( \Rbox ((BOX12F_{S18} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S18} \leftrightarrow ( \Rnext ((PersonP_{S18} \rightarrow E1SalaryP_{S18}) \land $ \\ 
 $ (PersonP_{S18} \rightarrow  \lnot E2SalaryP_{S18}) \land $ \\ 
 $ (E2SalaryP_{S18} \rightarrow E1SalaryP_{S18})) \land $ \\ 
 $ BOX9P_{S18})) \land $ \\ 
 $ ( \Rnext BOX14F_{S18} \leftrightarrow ( \Rnext BOX15F_{S18} \land $ \\ 
 $ BOX14F_{S18})) \land $ \\ 
 $ (BOX17P_{S18} \leftrightarrow  \Rbox BOX3P_{S18}) \land $ \\ 
 $ (BOX13F_{S18} \leftrightarrow  \Rbox (E1SalaryInvF_{S18} \rightarrow BOX14F_{S18})) \land $ \\ 
 $ (BOX10F_{S18} \leftrightarrow  \Rbox (E1SalaryF_{S18} \rightarrow BOX11F_{S18})) \land $ \\ 
 $ ( \Rnext BOX8P_{S18} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S18})) \land $ \\ 
 $ (BOX7P_{S18} \leftrightarrow  \Rbox BOX8P_{S18}) \land $ \\ 
 $ ( \Rnext BOX5P_{S18} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S18})) \land $ \\ 
 $ (BOX18P_{S18} \leftrightarrow  \Rbox BOX6P_{S18}) \land $ \\ 
 $ ( \Rnext BOX11F_{S18} \leftrightarrow ( \Rnext BOX12F_{S18} \land $ \\ 
 $ BOX11F_{S18})) \land $ \\ 
 $ ( \Rnext BOX1F_{S18} \leftrightarrow ( \Rnext BOX13F_{S18} \land $ \\ 
 $ BOX1F_{S18})) \land $ \\ 
 $ (BOX19P_{S18} \leftrightarrow  \Rbox BOX9P_{S18}) \land $ \\ 
 $ ( \Rnext BOX6P_{S18} \leftrightarrow ( \Rnext (E1SalaryInvP_{S18} \rightarrow BOX7P_{S18}) \land $ \\ 
 $ BOX6P_{S18})) \land $ \\ 
 $ ( \Rnext BOX3P_{S18} \leftrightarrow ( \Rnext (E1SalaryP_{S18} \rightarrow BOX4P_{S18}) \land $ \\ 
 $ BOX3P_{S18})) \land $ \\ 
 $ ( \Rnext BOX2F_{S18} \leftrightarrow ( \Rnext BOX16F_{S18} \land $ \\ 
 $ BOX2F_{S18})) \land $ \\ 
 $ (BOX4P_{S18} \leftrightarrow  \Rbox BOX5P_{S18}) \land $ \\ 
 $ (BOX15F_{S18} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S18} \leftrightarrow  \Rbox ((PersonF_{S18} \rightarrow E1SalaryF_{S18}) \land $ \\ 
 $ (PersonF_{S18} \rightarrow  \lnot E2SalaryF_{S18}) \land $ \\ 
 $ (E2SalaryF_{S18} \rightarrow E1SalaryF_{S18}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S18} \leftrightarrow ( \Rnext BOX10F_{S18} \land $ \\ 
 $ BOX0F_{S18}))) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX11F_{S9} \leftrightarrow BOX4P_{S9}) \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 $ \\ 
 $  \Rbox ((BOX12F_{S4} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S4} \leftrightarrow ( \Rnext ((PersonP_{S4} \rightarrow E1SalaryP_{S4}) \land $ \\ 
 $ (PersonP_{S4} \rightarrow  \lnot E2SalaryP_{S4}) \land $ \\ 
 $ (E2SalaryP_{S4} \rightarrow E1SalaryP_{S4})) \land $ \\ 
 $ BOX9P_{S4})) \land $ \\ 
 $ ( \Rnext BOX14F_{S4} \leftrightarrow ( \Rnext BOX15F_{S4} \land $ \\ 
 $ BOX14F_{S4})) \land $ \\ 
 $ (BOX17P_{S4} \leftrightarrow  \Rbox BOX3P_{S4}) \land $ \\ 
 $ (BOX13F_{S4} \leftrightarrow  \Rbox (E1SalaryInvF_{S4} \rightarrow BOX14F_{S4})) \land $ \\ 
 $ (BOX10F_{S4} \leftrightarrow  \Rbox (E1SalaryF_{S4} \rightarrow BOX11F_{S4})) \land $ \\ 
 $ ( \Rnext BOX8P_{S4} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S4})) \land $ \\ 
 $ (BOX7P_{S4} \leftrightarrow  \Rbox BOX8P_{S4}) \land $ \\ 
 $ ( \Rnext BOX5P_{S4} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S4})) \land $ \\ 
 $ (BOX18P_{S4} \leftrightarrow  \Rbox BOX6P_{S4}) \land $ \\ 
 $ ( \Rnext BOX11F_{S4} \leftrightarrow ( \Rnext BOX12F_{S4} \land $ \\ 
 $ BOX11F_{S4})) \land $ \\ 
 $ ( \Rnext BOX1F_{S4} \leftrightarrow ( \Rnext BOX13F_{S4} \land $ \\ 
 $ BOX1F_{S4})) \land $ \\ 
 $ (BOX19P_{S4} \leftrightarrow  \Rbox BOX9P_{S4}) \land $ \\ 
 $ ( \Rnext BOX6P_{S4} \leftrightarrow ( \Rnext (E1SalaryInvP_{S4} \rightarrow BOX7P_{S4}) \land $ \\ 
 $ BOX6P_{S4})) \land $ \\ 
 $ ( \Rnext BOX3P_{S4} \leftrightarrow ( \Rnext (E1SalaryP_{S4} \rightarrow BOX4P_{S4}) \land $ \\ 
 $ BOX3P_{S4})) \land $ \\ 
 $ ( \Rnext BOX2F_{S4} \leftrightarrow ( \Rnext BOX16F_{S4} \land $ \\ 
 $ BOX2F_{S4})) \land $ \\ 
 $ (BOX4P_{S4} \leftrightarrow  \Rbox BOX5P_{S4}) \land $ \\ 
 $ (BOX15F_{S4} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S4} \leftrightarrow  \Rbox ((PersonF_{S4} \rightarrow E1SalaryF_{S4}) \land $ \\ 
 $ (PersonF_{S4} \rightarrow  \lnot E2SalaryF_{S4}) \land $ \\ 
 $ (E2SalaryF_{S4} \rightarrow E1SalaryF_{S4}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S4} \leftrightarrow ( \Rnext BOX10F_{S4} \land $ \\ 
 $ BOX0F_{S4}))) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (PersonF_{S1} \leftrightarrow PersonP_{S1}) \land $ \\ 
 $ (BOX14F_{S4} \leftrightarrow BOX7P_{S4}) \land $ \\ 
 $ (E1SalaryF_{S17} \leftrightarrow E1SalaryP_{S17}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (BOX12F_{S13} \leftrightarrow BOX5P_{S13}) \land $ \\ 
 $ (BOX13F_{John} \leftrightarrow BOX6P_{John}) \land $ \\ 
 $ (BOX16F_{S14} \leftrightarrow BOX9P_{S14}) \land $ \\ 
 $ (E1SalaryF_{S3} \leftrightarrow E1SalaryP_{S3}) \land $ \\ 
 $ (BOX15F_{S20} \leftrightarrow BOX8P_{S20}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX10F_{S9} \leftrightarrow BOX3P_{S9}) \land $ \\ 
 $ (BOX2F_{S10} \leftrightarrow BOX19P_{S10}) \land $ \\ 
 $ (BOX16F_{John} \leftrightarrow BOX9P_{John}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (BOX10F_{S6} \leftrightarrow BOX3P_{S6}) \land $ \\ 
 $ (E2SalaryF_{S19} \leftrightarrow E2SalaryP_{S19}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (E2SalaryF_{John} \leftrightarrow E2SalaryP_{John}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX0F_{S16} \leftrightarrow BOX17P_{S16}) \land $ \\ 
 $ (BOX2F_{S18} \leftrightarrow BOX19P_{S18}) \land $ \\ 
 $ (BOX13F_{S4} \leftrightarrow BOX6P_{S4}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \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 $ \\ 
 $ (BOX10F_{S13} \leftrightarrow BOX3P_{S13}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (BOX13F_{S5} \leftrightarrow BOX6P_{S5}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (E1SalaryInvF_{S11} \leftrightarrow E1SalaryInvP_{S11}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (PersonF_{S16} \leftrightarrow PersonP_{S16}) \land $ \\ 
 $ (BOX16F_{S18} \leftrightarrow BOX9P_{S18}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX12F_{S16} \leftrightarrow BOX5P_{S16}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX1F_{S13} \leftrightarrow BOX18P_{S13}) \land $ \\ 
 $ (BOX2F_{S16} \leftrightarrow BOX19P_{S16}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX10F_{S16} \leftrightarrow BOX3P_{S16}) \land $ \\ 
 $ (PersonF_{S5} \leftrightarrow PersonP_{S5}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX10F_{S14} \leftrightarrow BOX3P_{S14}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (PersonF_{dSalary} \leftrightarrow PersonP_{dSalary}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (E2SalaryF_{S9} \leftrightarrow E2SalaryP_{S9}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (BOX16F_{S7} \leftrightarrow BOX9P_{S7}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (E1SalaryInvF_{S16} \leftrightarrow E1SalaryInvP_{S16}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX2F_{S17} \leftrightarrow BOX19P_{S17}) \land $ \\ 
 $ (E1SalaryInvF_{S2} \leftrightarrow E1SalaryInvP_{S2}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX15F_{S4} \leftrightarrow BOX8P_{S4}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (E1SalaryF_{dSalaryInv} \leftrightarrow E1SalaryP_{dSalaryInv}) \land $ \\ 
 $ (BOX14F_{S8} \leftrightarrow BOX7P_{S8}) \land $ \\ 
 $ (BOX15F_{S3} \leftrightarrow BOX8P_{S3}) \land $ \\ 
 $ (BOX14F_{S5} \leftrightarrow BOX7P_{S5}) \land $ \\ 
 $ (BOX2F_{S4} \leftrightarrow BOX19P_{S4}) \land $ \\ 
 $ (E2SalaryF_{S8} \leftrightarrow E2SalaryP_{S8}) \land $ \\ 
 $ (E2SalaryF_{S17} \leftrightarrow E2SalaryP_{S17}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (BOX12F_{S20} \leftrightarrow BOX5P_{S20}) \land $ \\ 
 $ (BOX12F_{S10} \leftrightarrow BOX5P_{S10}) \land $ \\ 
 $ (BOX16F_{S5} \leftrightarrow BOX9P_{S5}) \land $ \\ 
 $  \Rbox ((BOX12F_{S6} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S6} \leftrightarrow ( \Rnext ((PersonP_{S6} \rightarrow E1SalaryP_{S6}) \land $ \\ 
 $ (PersonP_{S6} \rightarrow  \lnot E2SalaryP_{S6}) \land $ \\ 
 $ (E2SalaryP_{S6} \rightarrow E1SalaryP_{S6})) \land $ \\ 
 $ BOX9P_{S6})) \land $ \\ 
 $ ( \Rnext BOX14F_{S6} \leftrightarrow ( \Rnext BOX15F_{S6} \land $ \\ 
 $ BOX14F_{S6})) \land $ \\ 
 $ (BOX17P_{S6} \leftrightarrow  \Rbox BOX3P_{S6}) \land $ \\ 
 $ (BOX13F_{S6} \leftrightarrow  \Rbox (E1SalaryInvF_{S6} \rightarrow BOX14F_{S6})) \land $ \\ 
 $ (BOX10F_{S6} \leftrightarrow  \Rbox (E1SalaryF_{S6} \rightarrow BOX11F_{S6})) \land $ \\ 
 $ ( \Rnext BOX8P_{S6} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S6})) \land $ \\ 
 $ (BOX7P_{S6} \leftrightarrow  \Rbox BOX8P_{S6}) \land $ \\ 
 $ ( \Rnext BOX5P_{S6} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S6})) \land $ \\ 
 $ (BOX18P_{S6} \leftrightarrow  \Rbox BOX6P_{S6}) \land $ \\ 
 $ ( \Rnext BOX11F_{S6} \leftrightarrow ( \Rnext BOX12F_{S6} \land $ \\ 
 $ BOX11F_{S6})) \land $ \\ 
 $ ( \Rnext BOX1F_{S6} \leftrightarrow ( \Rnext BOX13F_{S6} \land $ \\ 
 $ BOX1F_{S6})) \land $ \\ 
 $ (BOX19P_{S6} \leftrightarrow  \Rbox BOX9P_{S6}) \land $ \\ 
 $ ( \Rnext BOX6P_{S6} \leftrightarrow ( \Rnext (E1SalaryInvP_{S6} \rightarrow BOX7P_{S6}) \land $ \\ 
 $ BOX6P_{S6})) \land $ \\ 
 $ ( \Rnext BOX3P_{S6} \leftrightarrow ( \Rnext (E1SalaryP_{S6} \rightarrow BOX4P_{S6}) \land $ \\ 
 $ BOX3P_{S6})) \land $ \\ 
 $ ( \Rnext BOX2F_{S6} \leftrightarrow ( \Rnext BOX16F_{S6} \land $ \\ 
 $ BOX2F_{S6})) \land $ \\ 
 $ (BOX4P_{S6} \leftrightarrow  \Rbox BOX5P_{S6}) \land $ \\ 
 $ (BOX15F_{S6} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S6} \leftrightarrow  \Rbox ((PersonF_{S6} \rightarrow E1SalaryF_{S6}) \land $ \\ 
 $ (PersonF_{S6} \rightarrow  \lnot E2SalaryF_{S6}) \land $ \\ 
 $ (E2SalaryF_{S6} \rightarrow E1SalaryF_{S6}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S6} \leftrightarrow ( \Rnext BOX10F_{S6} \land $ \\ 
 $ BOX0F_{S6}))) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (E1SalaryInvF_{S7} \leftrightarrow E1SalaryInvP_{S7}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX13F_{S17} \leftrightarrow BOX6P_{S17}) \land $ \\ 
 $ (BOX1F_{S19} \leftrightarrow BOX18P_{S19}) \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 $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (E2SalaryF_{S11} \leftrightarrow E2SalaryP_{S11}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX14F_{S7} \leftrightarrow BOX7P_{S7}) \land $ \\ 
 $ (E1SalaryInvF_{S3} \leftrightarrow E1SalaryInvP_{S3}) \land $ \\ 
 $ (BOX16F_{S3} \leftrightarrow BOX9P_{S3}) \land $ \\ 
 $ (BOX16F_{S4} \leftrightarrow BOX9P_{S4}) \land $ \\ 
 $ (BOX12F_{S12} \leftrightarrow BOX5P_{S12}) \land $ \\ 
 $ (BOX13F_{dSalaryInv} \leftrightarrow BOX6P_{dSalaryInv}) \land $ \\ 
 $ (BOX2F_{S7} \leftrightarrow BOX19P_{S7}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (BOX10F_{S18} \leftrightarrow BOX3P_{S18}) \land $ \\ 
 $  \Rbox ((BOX12F_{S13} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S13} \leftrightarrow ( \Rnext ((PersonP_{S13} \rightarrow E1SalaryP_{S13}) \land $ \\ 
 $ (PersonP_{S13} \rightarrow  \lnot E2SalaryP_{S13}) \land $ \\ 
 $ (E2SalaryP_{S13} \rightarrow E1SalaryP_{S13})) \land $ \\ 
 $ BOX9P_{S13})) \land $ \\ 
 $ ( \Rnext BOX14F_{S13} \leftrightarrow ( \Rnext BOX15F_{S13} \land $ \\ 
 $ BOX14F_{S13})) \land $ \\ 
 $ (BOX17P_{S13} \leftrightarrow  \Rbox BOX3P_{S13}) \land $ \\ 
 $ (BOX13F_{S13} \leftrightarrow  \Rbox (E1SalaryInvF_{S13} \rightarrow BOX14F_{S13})) \land $ \\ 
 $ (BOX10F_{S13} \leftrightarrow  \Rbox (E1SalaryF_{S13} \rightarrow BOX11F_{S13})) \land $ \\ 
 $ ( \Rnext BOX8P_{S13} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S13})) \land $ \\ 
 $ (BOX7P_{S13} \leftrightarrow  \Rbox BOX8P_{S13}) \land $ \\ 
 $ ( \Rnext BOX5P_{S13} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S13})) \land $ \\ 
 $ (BOX18P_{S13} \leftrightarrow  \Rbox BOX6P_{S13}) \land $ \\ 
 $ ( \Rnext BOX11F_{S13} \leftrightarrow ( \Rnext BOX12F_{S13} \land $ \\ 
 $ BOX11F_{S13})) \land $ \\ 
 $ ( \Rnext BOX1F_{S13} \leftrightarrow ( \Rnext BOX13F_{S13} \land $ \\ 
 $ BOX1F_{S13})) \land $ \\ 
 $ (BOX19P_{S13} \leftrightarrow  \Rbox BOX9P_{S13}) \land $ \\ 
 $ ( \Rnext BOX6P_{S13} \leftrightarrow ( \Rnext (E1SalaryInvP_{S13} \rightarrow BOX7P_{S13}) \land $ \\ 
 $ BOX6P_{S13})) \land $ \\ 
 $ ( \Rnext BOX3P_{S13} \leftrightarrow ( \Rnext (E1SalaryP_{S13} \rightarrow BOX4P_{S13}) \land $ \\ 
 $ BOX3P_{S13})) \land $ \\ 
 $ ( \Rnext BOX2F_{S13} \leftrightarrow ( \Rnext BOX16F_{S13} \land $ \\ 
 $ BOX2F_{S13})) \land $ \\ 
 $ (BOX4P_{S13} \leftrightarrow  \Rbox BOX5P_{S13}) \land $ \\ 
 $ (BOX15F_{S13} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S13} \leftrightarrow  \Rbox ((PersonF_{S13} \rightarrow E1SalaryF_{S13}) \land $ \\ 
 $ (PersonF_{S13} \rightarrow  \lnot E2SalaryF_{S13}) \land $ \\ 
 $ (E2SalaryF_{S13} \rightarrow E1SalaryF_{S13}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S13} \leftrightarrow ( \Rnext BOX10F_{S13} \land $ \\ 
 $ BOX0F_{S13}))) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (BOX16F_{S15} \leftrightarrow BOX9P_{S15}) \land $ \\ 
 $ (BOX0F_{S15} \leftrightarrow BOX17P_{S15}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $  \Rbox ((BOX12F_{S7} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S7} \leftrightarrow ( \Rnext ((PersonP_{S7} \rightarrow E1SalaryP_{S7}) \land $ \\ 
 $ (PersonP_{S7} \rightarrow  \lnot E2SalaryP_{S7}) \land $ \\ 
 $ (E2SalaryP_{S7} \rightarrow E1SalaryP_{S7})) \land $ \\ 
 $ BOX9P_{S7})) \land $ \\ 
 $ ( \Rnext BOX14F_{S7} \leftrightarrow ( \Rnext BOX15F_{S7} \land $ \\ 
 $ BOX14F_{S7})) \land $ \\ 
 $ (BOX17P_{S7} \leftrightarrow  \Rbox BOX3P_{S7}) \land $ \\ 
 $ (BOX13F_{S7} \leftrightarrow  \Rbox (E1SalaryInvF_{S7} \rightarrow BOX14F_{S7})) \land $ \\ 
 $ (BOX10F_{S7} \leftrightarrow  \Rbox (E1SalaryF_{S7} \rightarrow BOX11F_{S7})) \land $ \\ 
 $ ( \Rnext BOX8P_{S7} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S7})) \land $ \\ 
 $ (BOX7P_{S7} \leftrightarrow  \Rbox BOX8P_{S7}) \land $ \\ 
 $ ( \Rnext BOX5P_{S7} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S7})) \land $ \\ 
 $ (BOX18P_{S7} \leftrightarrow  \Rbox BOX6P_{S7}) \land $ \\ 
 $ ( \Rnext BOX11F_{S7} \leftrightarrow ( \Rnext BOX12F_{S7} \land $ \\ 
 $ BOX11F_{S7})) \land $ \\ 
 $ ( \Rnext BOX1F_{S7} \leftrightarrow ( \Rnext BOX13F_{S7} \land $ \\ 
 $ BOX1F_{S7})) \land $ \\ 
 $ (BOX19P_{S7} \leftrightarrow  \Rbox BOX9P_{S7}) \land $ \\ 
 $ ( \Rnext BOX6P_{S7} \leftrightarrow ( \Rnext (E1SalaryInvP_{S7} \rightarrow BOX7P_{S7}) \land $ \\ 
 $ BOX6P_{S7})) \land $ \\ 
 $ ( \Rnext BOX3P_{S7} \leftrightarrow ( \Rnext (E1SalaryP_{S7} \rightarrow BOX4P_{S7}) \land $ \\ 
 $ BOX3P_{S7})) \land $ \\ 
 $ ( \Rnext BOX2F_{S7} \leftrightarrow ( \Rnext BOX16F_{S7} \land $ \\ 
 $ BOX2F_{S7})) \land $ \\ 
 $ (BOX4P_{S7} \leftrightarrow  \Rbox BOX5P_{S7}) \land $ \\ 
 $ (BOX15F_{S7} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S7} \leftrightarrow  \Rbox ((PersonF_{S7} \rightarrow E1SalaryF_{S7}) \land $ \\ 
 $ (PersonF_{S7} \rightarrow  \lnot E2SalaryF_{S7}) \land $ \\ 
 $ (E2SalaryF_{S7} \rightarrow E1SalaryF_{S7}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S7} \leftrightarrow ( \Rnext BOX10F_{S7} \land $ \\ 
 $ BOX0F_{S7}))) \land $ \\ 
 $ (BOX2F_{S5} \leftrightarrow BOX19P_{S5}) \land $ \\ 
 $ (E1SalaryInvF_{S18} \leftrightarrow E1SalaryInvP_{S18}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (E1SalaryF_{S6} \leftrightarrow E1SalaryP_{S6}) \land $ \\ 
 $ (BOX11F_{S8} \leftrightarrow BOX4P_{S8}) \land $ \\ 
 $ (BOX2F_{S9} \leftrightarrow BOX19P_{S9}) \land $ \\ 
 $ (BOX13F_{S1} \leftrightarrow BOX6P_{S1}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX12F_{John} \leftrightarrow BOX5P_{John}) \land $ \\ 
 $ (BOX13F_{S7} \leftrightarrow BOX6P_{S7}) \land $ \\ 
 $ (BOX15F_{S16} \leftrightarrow BOX8P_{S16}) \land $ \\ 
 $ (BOX13F_{S9} \leftrightarrow BOX6P_{S9}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (BOX2F_{S14} \leftrightarrow BOX19P_{S14}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $  \Rbox ((BOX12F_{S3} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S3} \leftrightarrow ( \Rnext ((PersonP_{S3} \rightarrow E1SalaryP_{S3}) \land $ \\ 
 $ (PersonP_{S3} \rightarrow  \lnot E2SalaryP_{S3}) \land $ \\ 
 $ (E2SalaryP_{S3} \rightarrow E1SalaryP_{S3})) \land $ \\ 
 $ BOX9P_{S3})) \land $ \\ 
 $ ( \Rnext BOX14F_{S3} \leftrightarrow ( \Rnext BOX15F_{S3} \land $ \\ 
 $ BOX14F_{S3})) \land $ \\ 
 $ (BOX17P_{S3} \leftrightarrow  \Rbox BOX3P_{S3}) \land $ \\ 
 $ (BOX13F_{S3} \leftrightarrow  \Rbox (E1SalaryInvF_{S3} \rightarrow BOX14F_{S3})) \land $ \\ 
 $ (BOX10F_{S3} \leftrightarrow  \Rbox (E1SalaryF_{S3} \rightarrow BOX11F_{S3})) \land $ \\ 
 $ ( \Rnext BOX8P_{S3} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S3})) \land $ \\ 
 $ (BOX7P_{S3} \leftrightarrow  \Rbox BOX8P_{S3}) \land $ \\ 
 $ ( \Rnext BOX5P_{S3} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S3})) \land $ \\ 
 $ (BOX18P_{S3} \leftrightarrow  \Rbox BOX6P_{S3}) \land $ \\ 
 $ ( \Rnext BOX11F_{S3} \leftrightarrow ( \Rnext BOX12F_{S3} \land $ \\ 
 $ BOX11F_{S3})) \land $ \\ 
 $ ( \Rnext BOX1F_{S3} \leftrightarrow ( \Rnext BOX13F_{S3} \land $ \\ 
 $ BOX1F_{S3})) \land $ \\ 
 $ (BOX19P_{S3} \leftrightarrow  \Rbox BOX9P_{S3}) \land $ \\ 
 $ ( \Rnext BOX6P_{S3} \leftrightarrow ( \Rnext (E1SalaryInvP_{S3} \rightarrow BOX7P_{S3}) \land $ \\ 
 $ BOX6P_{S3})) \land $ \\ 
 $ ( \Rnext BOX3P_{S3} \leftrightarrow ( \Rnext (E1SalaryP_{S3} \rightarrow BOX4P_{S3}) \land $ \\ 
 $ BOX3P_{S3})) \land $ \\ 
 $ ( \Rnext BOX2F_{S3} \leftrightarrow ( \Rnext BOX16F_{S3} \land $ \\ 
 $ BOX2F_{S3})) \land $ \\ 
 $ (BOX4P_{S3} \leftrightarrow  \Rbox BOX5P_{S3}) \land $ \\ 
 $ (BOX15F_{S3} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S3} \leftrightarrow  \Rbox ((PersonF_{S3} \rightarrow E1SalaryF_{S3}) \land $ \\ 
 $ (PersonF_{S3} \rightarrow  \lnot E2SalaryF_{S3}) \land $ \\ 
 $ (E2SalaryF_{S3} \rightarrow E1SalaryF_{S3}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S3} \leftrightarrow ( \Rnext BOX10F_{S3} \land $ \\ 
 $ BOX0F_{S3}))) \land $ \\ 
 $ (BOX1F_{S3} \leftrightarrow BOX18P_{S3}) \land $ \\ 
 $ (E1SalaryF_{S20} \leftrightarrow E1SalaryP_{S20}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (BOX12F_{S3} \leftrightarrow BOX5P_{S3}) \land $ \\ 
 $ (E1SalaryF_{John} \leftrightarrow E1SalaryP_{John}) \land $ \\ 
 $ (BOX14F_{S11} \leftrightarrow BOX7P_{S11}) \land $ \\ 
 $ (BOX0F_{S13} \leftrightarrow BOX17P_{S13}) \land $ \\ 
 $ (BOX12F_{S8} \leftrightarrow BOX5P_{S8}) \land $ \\ 
 $ (BOX16F_{S8} \leftrightarrow BOX9P_{S8}) \land $ \\ 
 $ (BOX13F_{S10} \leftrightarrow BOX6P_{S10}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX14F_{S19} \leftrightarrow BOX7P_{S19}) \land $ \\ 
 $ (BOX15F_{S10} \leftrightarrow BOX8P_{S10}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX10F_{S10} \leftrightarrow BOX3P_{S10}) \land $ \\ 
 $ (BOX13F_{S15} \leftrightarrow BOX6P_{S15}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $  \Rbox ((BOX12F_{S15} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S15} \leftrightarrow ( \Rnext ((PersonP_{S15} \rightarrow E1SalaryP_{S15}) \land $ \\ 
 $ (PersonP_{S15} \rightarrow  \lnot E2SalaryP_{S15}) \land $ \\ 
 $ (E2SalaryP_{S15} \rightarrow E1SalaryP_{S15})) \land $ \\ 
 $ BOX9P_{S15})) \land $ \\ 
 $ ( \Rnext BOX14F_{S15} \leftrightarrow ( \Rnext BOX15F_{S15} \land $ \\ 
 $ BOX14F_{S15})) \land $ \\ 
 $ (BOX17P_{S15} \leftrightarrow  \Rbox BOX3P_{S15}) \land $ \\ 
 $ (BOX13F_{S15} \leftrightarrow  \Rbox (E1SalaryInvF_{S15} \rightarrow BOX14F_{S15})) \land $ \\ 
 $ (BOX10F_{S15} \leftrightarrow  \Rbox (E1SalaryF_{S15} \rightarrow BOX11F_{S15})) \land $ \\ 
 $ ( \Rnext BOX8P_{S15} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S15})) \land $ \\ 
 $ (BOX7P_{S15} \leftrightarrow  \Rbox BOX8P_{S15}) \land $ \\ 
 $ ( \Rnext BOX5P_{S15} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S15})) \land $ \\ 
 $ (BOX18P_{S15} \leftrightarrow  \Rbox BOX6P_{S15}) \land $ \\ 
 $ ( \Rnext BOX11F_{S15} \leftrightarrow ( \Rnext BOX12F_{S15} \land $ \\ 
 $ BOX11F_{S15})) \land $ \\ 
 $ ( \Rnext BOX1F_{S15} \leftrightarrow ( \Rnext BOX13F_{S15} \land $ \\ 
 $ BOX1F_{S15})) \land $ \\ 
 $ (BOX19P_{S15} \leftrightarrow  \Rbox BOX9P_{S15}) \land $ \\ 
 $ ( \Rnext BOX6P_{S15} \leftrightarrow ( \Rnext (E1SalaryInvP_{S15} \rightarrow BOX7P_{S15}) \land $ \\ 
 $ BOX6P_{S15})) \land $ \\ 
 $ ( \Rnext BOX3P_{S15} \leftrightarrow ( \Rnext (E1SalaryP_{S15} \rightarrow BOX4P_{S15}) \land $ \\ 
 $ BOX3P_{S15})) \land $ \\ 
 $ ( \Rnext BOX2F_{S15} \leftrightarrow ( \Rnext BOX16F_{S15} \land $ \\ 
 $ BOX2F_{S15})) \land $ \\ 
 $ (BOX4P_{S15} \leftrightarrow  \Rbox BOX5P_{S15}) \land $ \\ 
 $ (BOX15F_{S15} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S15} \leftrightarrow  \Rbox ((PersonF_{S15} \rightarrow E1SalaryF_{S15}) \land $ \\ 
 $ (PersonF_{S15} \rightarrow  \lnot E2SalaryF_{S15}) \land $ \\ 
 $ (E2SalaryF_{S15} \rightarrow E1SalaryF_{S15}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S15} \leftrightarrow ( \Rnext BOX10F_{S15} \land $ \\ 
 $ BOX0F_{S15}))) \land $ \\ 
 $ (BOX1F_{S2} \leftrightarrow BOX18P_{S2}) \land $ \\ 
 $  \Rbox ((BOX12F_{S12} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S12} \leftrightarrow ( \Rnext ((PersonP_{S12} \rightarrow E1SalaryP_{S12}) \land $ \\ 
 $ (PersonP_{S12} \rightarrow  \lnot E2SalaryP_{S12}) \land $ \\ 
 $ (E2SalaryP_{S12} \rightarrow E1SalaryP_{S12})) \land $ \\ 
 $ BOX9P_{S12})) \land $ \\ 
 $ ( \Rnext BOX14F_{S12} \leftrightarrow ( \Rnext BOX15F_{S12} \land $ \\ 
 $ BOX14F_{S12})) \land $ \\ 
 $ (BOX17P_{S12} \leftrightarrow  \Rbox BOX3P_{S12}) \land $ \\ 
 $ (BOX13F_{S12} \leftrightarrow  \Rbox (E1SalaryInvF_{S12} \rightarrow BOX14F_{S12})) \land $ \\ 
 $ (BOX10F_{S12} \leftrightarrow  \Rbox (E1SalaryF_{S12} \rightarrow BOX11F_{S12})) \land $ \\ 
 $ ( \Rnext BOX8P_{S12} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S12})) \land $ \\ 
 $ (BOX7P_{S12} \leftrightarrow  \Rbox BOX8P_{S12}) \land $ \\ 
 $ ( \Rnext BOX5P_{S12} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S12})) \land $ \\ 
 $ (BOX18P_{S12} \leftrightarrow  \Rbox BOX6P_{S12}) \land $ \\ 
 $ ( \Rnext BOX11F_{S12} \leftrightarrow ( \Rnext BOX12F_{S12} \land $ \\ 
 $ BOX11F_{S12})) \land $ \\ 
 $ ( \Rnext BOX1F_{S12} \leftrightarrow ( \Rnext BOX13F_{S12} \land $ \\ 
 $ BOX1F_{S12})) \land $ \\ 
 $ (BOX19P_{S12} \leftrightarrow  \Rbox BOX9P_{S12}) \land $ \\ 
 $ ( \Rnext BOX6P_{S12} \leftrightarrow ( \Rnext (E1SalaryInvP_{S12} \rightarrow BOX7P_{S12}) \land $ \\ 
 $ BOX6P_{S12})) \land $ \\ 
 $ ( \Rnext BOX3P_{S12} \leftrightarrow ( \Rnext (E1SalaryP_{S12} \rightarrow BOX4P_{S12}) \land $ \\ 
 $ BOX3P_{S12})) \land $ \\ 
 $ ( \Rnext BOX2F_{S12} \leftrightarrow ( \Rnext BOX16F_{S12} \land $ \\ 
 $ BOX2F_{S12})) \land $ \\ 
 $ (BOX4P_{S12} \leftrightarrow  \Rbox BOX5P_{S12}) \land $ \\ 
 $ (BOX15F_{S12} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S12} \leftrightarrow  \Rbox ((PersonF_{S12} \rightarrow E1SalaryF_{S12}) \land $ \\ 
 $ (PersonF_{S12} \rightarrow  \lnot E2SalaryF_{S12}) \land $ \\ 
 $ (E2SalaryF_{S12} \rightarrow E1SalaryF_{S12}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S12} \leftrightarrow ( \Rnext BOX10F_{S12} \land $ \\ 
 $ BOX0F_{S12}))) \land $ \\ 
 $ (BOX12F_{S1} \leftrightarrow BOX5P_{S1}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX11F_{S13} \leftrightarrow BOX4P_{S13}) \land $ \\ 
 $ (BOX16F_{S17} \leftrightarrow BOX9P_{S17}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (BOX13F_{S8} \leftrightarrow BOX6P_{S8}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX14F_{S2} \leftrightarrow BOX7P_{S2}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX12F_{S17} \leftrightarrow BOX5P_{S17}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (E1SalaryF_{S11} \leftrightarrow E1SalaryP_{S11}) \land $ \\ 
 $ (BOX2F_{S11} \leftrightarrow BOX19P_{S11}) \land $ \\ 
 $  \Rbox ((BOX12F_{S17} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S17} \leftrightarrow ( \Rnext ((PersonP_{S17} \rightarrow E1SalaryP_{S17}) \land $ \\ 
 $ (PersonP_{S17} \rightarrow  \lnot E2SalaryP_{S17}) \land $ \\ 
 $ (E2SalaryP_{S17} \rightarrow E1SalaryP_{S17})) \land $ \\ 
 $ BOX9P_{S17})) \land $ \\ 
 $ ( \Rnext BOX14F_{S17} \leftrightarrow ( \Rnext BOX15F_{S17} \land $ \\ 
 $ BOX14F_{S17})) \land $ \\ 
 $ (BOX17P_{S17} \leftrightarrow  \Rbox BOX3P_{S17}) \land $ \\ 
 $ (BOX13F_{S17} \leftrightarrow  \Rbox (E1SalaryInvF_{S17} \rightarrow BOX14F_{S17})) \land $ \\ 
 $ (BOX10F_{S17} \leftrightarrow  \Rbox (E1SalaryF_{S17} \rightarrow BOX11F_{S17})) \land $ \\ 
 $ ( \Rnext BOX8P_{S17} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S17})) \land $ \\ 
 $ (BOX7P_{S17} \leftrightarrow  \Rbox BOX8P_{S17}) \land $ \\ 
 $ ( \Rnext BOX5P_{S17} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S17})) \land $ \\ 
 $ (BOX18P_{S17} \leftrightarrow  \Rbox BOX6P_{S17}) \land $ \\ 
 $ ( \Rnext BOX11F_{S17} \leftrightarrow ( \Rnext BOX12F_{S17} \land $ \\ 
 $ BOX11F_{S17})) \land $ \\ 
 $ ( \Rnext BOX1F_{S17} \leftrightarrow ( \Rnext BOX13F_{S17} \land $ \\ 
 $ BOX1F_{S17})) \land $ \\ 
 $ (BOX19P_{S17} \leftrightarrow  \Rbox BOX9P_{S17}) \land $ \\ 
 $ ( \Rnext BOX6P_{S17} \leftrightarrow ( \Rnext (E1SalaryInvP_{S17} \rightarrow BOX7P_{S17}) \land $ \\ 
 $ BOX6P_{S17})) \land $ \\ 
 $ ( \Rnext BOX3P_{S17} \leftrightarrow ( \Rnext (E1SalaryP_{S17} \rightarrow BOX4P_{S17}) \land $ \\ 
 $ BOX3P_{S17})) \land $ \\ 
 $ ( \Rnext BOX2F_{S17} \leftrightarrow ( \Rnext BOX16F_{S17} \land $ \\ 
 $ BOX2F_{S17})) \land $ \\ 
 $ (BOX4P_{S17} \leftrightarrow  \Rbox BOX5P_{S17}) \land $ \\ 
 $ (BOX15F_{S17} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S17} \leftrightarrow  \Rbox ((PersonF_{S17} \rightarrow E1SalaryF_{S17}) \land $ \\ 
 $ (PersonF_{S17} \rightarrow  \lnot E2SalaryF_{S17}) \land $ \\ 
 $ (E2SalaryF_{S17} \rightarrow E1SalaryF_{S17}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S17} \leftrightarrow ( \Rnext BOX10F_{S17} \land $ \\ 
 $ BOX0F_{S17}))) \land $ \\ 
 $ (BOX11F_{S16} \leftrightarrow BOX4P_{S16}) \land $ \\ 
 $ (PersonF_{S7} \leftrightarrow PersonP_{S7}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (E2SalaryF_{S14} \leftrightarrow E2SalaryP_{S14}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (BOX10F_{dSalary} \leftrightarrow BOX3P_{dSalary}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX13F_{S18} \leftrightarrow BOX6P_{S18}) \land $ \\ 
 $ (BOX0F_{S17} \leftrightarrow BOX17P_{S17}) \land $ \\ 
 $ (BOX0F_{S3} \leftrightarrow BOX17P_{S3}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (BOX0F_{S18} \leftrightarrow BOX17P_{S18}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (BOX14F_{S13} \leftrightarrow BOX7P_{S13}) \land $ \\ 
 $ (BOX11F_{S5} \leftrightarrow BOX4P_{S5}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (E1SalaryInvF_{S19} \leftrightarrow E1SalaryInvP_{S19}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (BOX16F_{S11} \leftrightarrow BOX9P_{S11}) \land $ \\ 
 $ (PersonF_{S8} \leftrightarrow PersonP_{S8}) \land $ \\ 
 $ (BOX15F_{S14} \leftrightarrow BOX8P_{S14}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX1F_{dSalary} \leftrightarrow BOX18P_{dSalary}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX11F_{S4} \leftrightarrow BOX4P_{S4}) \land $ \\ 
 $  \Rbox ((BOX12F_{S11} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S11} \leftrightarrow ( \Rnext ((PersonP_{S11} \rightarrow E1SalaryP_{S11}) \land $ \\ 
 $ (PersonP_{S11} \rightarrow  \lnot E2SalaryP_{S11}) \land $ \\ 
 $ (E2SalaryP_{S11} \rightarrow E1SalaryP_{S11})) \land $ \\ 
 $ BOX9P_{S11})) \land $ \\ 
 $ ( \Rnext BOX14F_{S11} \leftrightarrow ( \Rnext BOX15F_{S11} \land $ \\ 
 $ BOX14F_{S11})) \land $ \\ 
 $ (BOX17P_{S11} \leftrightarrow  \Rbox BOX3P_{S11}) \land $ \\ 
 $ (BOX13F_{S11} \leftrightarrow  \Rbox (E1SalaryInvF_{S11} \rightarrow BOX14F_{S11})) \land $ \\ 
 $ (BOX10F_{S11} \leftrightarrow  \Rbox (E1SalaryF_{S11} \rightarrow BOX11F_{S11})) \land $ \\ 
 $ ( \Rnext BOX8P_{S11} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S11})) \land $ \\ 
 $ (BOX7P_{S11} \leftrightarrow  \Rbox BOX8P_{S11}) \land $ \\ 
 $ ( \Rnext BOX5P_{S11} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S11})) \land $ \\ 
 $ (BOX18P_{S11} \leftrightarrow  \Rbox BOX6P_{S11}) \land $ \\ 
 $ ( \Rnext BOX11F_{S11} \leftrightarrow ( \Rnext BOX12F_{S11} \land $ \\ 
 $ BOX11F_{S11})) \land $ \\ 
 $ ( \Rnext BOX1F_{S11} \leftrightarrow ( \Rnext BOX13F_{S11} \land $ \\ 
 $ BOX1F_{S11})) \land $ \\ 
 $ (BOX19P_{S11} \leftrightarrow  \Rbox BOX9P_{S11}) \land $ \\ 
 $ ( \Rnext BOX6P_{S11} \leftrightarrow ( \Rnext (E1SalaryInvP_{S11} \rightarrow BOX7P_{S11}) \land $ \\ 
 $ BOX6P_{S11})) \land $ \\ 
 $ ( \Rnext BOX3P_{S11} \leftrightarrow ( \Rnext (E1SalaryP_{S11} \rightarrow BOX4P_{S11}) \land $ \\ 
 $ BOX3P_{S11})) \land $ \\ 
 $ ( \Rnext BOX2F_{S11} \leftrightarrow ( \Rnext BOX16F_{S11} \land $ \\ 
 $ BOX2F_{S11})) \land $ \\ 
 $ (BOX4P_{S11} \leftrightarrow  \Rbox BOX5P_{S11}) \land $ \\ 
 $ (BOX15F_{S11} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S11} \leftrightarrow  \Rbox ((PersonF_{S11} \rightarrow E1SalaryF_{S11}) \land $ \\ 
 $ (PersonF_{S11} \rightarrow  \lnot E2SalaryF_{S11}) \land $ \\ 
 $ (E2SalaryF_{S11} \rightarrow E1SalaryF_{S11}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S11} \leftrightarrow ( \Rnext BOX10F_{S11} \land $ \\ 
 $ BOX0F_{S11}))) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (BOX0F_{S10} \leftrightarrow BOX17P_{S10}) \land $ \\ 
 $  \Rbox ((BOX12F_{S20} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S20} \leftrightarrow ( \Rnext ((PersonP_{S20} \rightarrow E1SalaryP_{S20}) \land $ \\ 
 $ (PersonP_{S20} \rightarrow  \lnot E2SalaryP_{S20}) \land $ \\ 
 $ (E2SalaryP_{S20} \rightarrow E1SalaryP_{S20})) \land $ \\ 
 $ BOX9P_{S20})) \land $ \\ 
 $ ( \Rnext BOX14F_{S20} \leftrightarrow ( \Rnext BOX15F_{S20} \land $ \\ 
 $ BOX14F_{S20})) \land $ \\ 
 $ (BOX17P_{S20} \leftrightarrow  \Rbox BOX3P_{S20}) \land $ \\ 
 $ (BOX13F_{S20} \leftrightarrow  \Rbox (E1SalaryInvF_{S20} \rightarrow BOX14F_{S20})) \land $ \\ 
 $ (BOX10F_{S20} \leftrightarrow  \Rbox (E1SalaryF_{S20} \rightarrow BOX11F_{S20})) \land $ \\ 
 $ ( \Rnext BOX8P_{S20} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S20})) \land $ \\ 
 $ (BOX7P_{S20} \leftrightarrow  \Rbox BOX8P_{S20}) \land $ \\ 
 $ ( \Rnext BOX5P_{S20} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S20})) \land $ \\ 
 $ (BOX18P_{S20} \leftrightarrow  \Rbox BOX6P_{S20}) \land $ \\ 
 $ ( \Rnext BOX11F_{S20} \leftrightarrow ( \Rnext BOX12F_{S20} \land $ \\ 
 $ BOX11F_{S20})) \land $ \\ 
 $ ( \Rnext BOX1F_{S20} \leftrightarrow ( \Rnext BOX13F_{S20} \land $ \\ 
 $ BOX1F_{S20})) \land $ \\ 
 $ (BOX19P_{S20} \leftrightarrow  \Rbox BOX9P_{S20}) \land $ \\ 
 $ ( \Rnext BOX6P_{S20} \leftrightarrow ( \Rnext (E1SalaryInvP_{S20} \rightarrow BOX7P_{S20}) \land $ \\ 
 $ BOX6P_{S20})) \land $ \\ 
 $ ( \Rnext BOX3P_{S20} \leftrightarrow ( \Rnext (E1SalaryP_{S20} \rightarrow BOX4P_{S20}) \land $ \\ 
 $ BOX3P_{S20})) \land $ \\ 
 $ ( \Rnext BOX2F_{S20} \leftrightarrow ( \Rnext BOX16F_{S20} \land $ \\ 
 $ BOX2F_{S20})) \land $ \\ 
 $ (BOX4P_{S20} \leftrightarrow  \Rbox BOX5P_{S20}) \land $ \\ 
 $ (BOX15F_{S20} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S20} \leftrightarrow  \Rbox ((PersonF_{S20} \rightarrow E1SalaryF_{S20}) \land $ \\ 
 $ (PersonF_{S20} \rightarrow  \lnot E2SalaryF_{S20}) \land $ \\ 
 $ (E2SalaryF_{S20} \rightarrow E1SalaryF_{S20}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S20} \leftrightarrow ( \Rnext BOX10F_{S20} \land $ \\ 
 $ BOX0F_{S20}))) \land $ \\ 
 $ (BOX12F_{dSalary} \leftrightarrow BOX5P_{dSalary}) \land $ \\ 
 $ (BOX16F_{S19} \leftrightarrow BOX9P_{S19}) \land $ \\ 
 $ (E1SalaryInvF_{S8} \leftrightarrow E1SalaryInvP_{S8}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (BOX14F_{S16} \leftrightarrow BOX7P_{S16}) \land $ \\ 
 $ (BOX16F_{S20} \leftrightarrow BOX9P_{S20}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (PersonF_{S15} \leftrightarrow PersonP_{S15}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (E1SalaryInvF_{S20} \leftrightarrow E1SalaryInvP_{S20}) \land $ \\ 
 $  \Rbox ((BOX12F_{S9} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S9} \leftrightarrow ( \Rnext ((PersonP_{S9} \rightarrow E1SalaryP_{S9}) \land $ \\ 
 $ (PersonP_{S9} \rightarrow  \lnot E2SalaryP_{S9}) \land $ \\ 
 $ (E2SalaryP_{S9} \rightarrow E1SalaryP_{S9})) \land $ \\ 
 $ BOX9P_{S9})) \land $ \\ 
 $ ( \Rnext BOX14F_{S9} \leftrightarrow ( \Rnext BOX15F_{S9} \land $ \\ 
 $ BOX14F_{S9})) \land $ \\ 
 $ (BOX17P_{S9} \leftrightarrow  \Rbox BOX3P_{S9}) \land $ \\ 
 $ (BOX13F_{S9} \leftrightarrow  \Rbox (E1SalaryInvF_{S9} \rightarrow BOX14F_{S9})) \land $ \\ 
 $ (BOX10F_{S9} \leftrightarrow  \Rbox (E1SalaryF_{S9} \rightarrow BOX11F_{S9})) \land $ \\ 
 $ ( \Rnext BOX8P_{S9} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S9})) \land $ \\ 
 $ (BOX7P_{S9} \leftrightarrow  \Rbox BOX8P_{S9}) \land $ \\ 
 $ ( \Rnext BOX5P_{S9} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S9})) \land $ \\ 
 $ (BOX18P_{S9} \leftrightarrow  \Rbox BOX6P_{S9}) \land $ \\ 
 $ ( \Rnext BOX11F_{S9} \leftrightarrow ( \Rnext BOX12F_{S9} \land $ \\ 
 $ BOX11F_{S9})) \land $ \\ 
 $ ( \Rnext BOX1F_{S9} \leftrightarrow ( \Rnext BOX13F_{S9} \land $ \\ 
 $ BOX1F_{S9})) \land $ \\ 
 $ (BOX19P_{S9} \leftrightarrow  \Rbox BOX9P_{S9}) \land $ \\ 
 $ ( \Rnext BOX6P_{S9} \leftrightarrow ( \Rnext (E1SalaryInvP_{S9} \rightarrow BOX7P_{S9}) \land $ \\ 
 $ BOX6P_{S9})) \land $ \\ 
 $ ( \Rnext BOX3P_{S9} \leftrightarrow ( \Rnext (E1SalaryP_{S9} \rightarrow BOX4P_{S9}) \land $ \\ 
 $ BOX3P_{S9})) \land $ \\ 
 $ ( \Rnext BOX2F_{S9} \leftrightarrow ( \Rnext BOX16F_{S9} \land $ \\ 
 $ BOX2F_{S9})) \land $ \\ 
 $ (BOX4P_{S9} \leftrightarrow  \Rbox BOX5P_{S9}) \land $ \\ 
 $ (BOX15F_{S9} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S9} \leftrightarrow  \Rbox ((PersonF_{S9} \rightarrow E1SalaryF_{S9}) \land $ \\ 
 $ (PersonF_{S9} \rightarrow  \lnot E2SalaryF_{S9}) \land $ \\ 
 $ (E2SalaryF_{S9} \rightarrow E1SalaryF_{S9}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S9} \leftrightarrow ( \Rnext BOX10F_{S9} \land $ \\ 
 $ BOX0F_{S9}))) \land $ \\ 
 $ (BOX13F_{S13} \leftrightarrow BOX6P_{S13}) \land $ \\ 
 $ (BOX10F_{S19} \leftrightarrow BOX3P_{S19}) \land $ \\ 
 $ (BOX12F_{S9} \leftrightarrow BOX5P_{S9}) \land $ \\ 
 $ (BOX1F_{S16} \leftrightarrow BOX18P_{S16}) \land $ \\ 
 $ (BOX0F_{S9} \leftrightarrow BOX17P_{S9}) \land $ \\ 
 $ (BOX13F_{S19} \leftrightarrow BOX6P_{S19}) \land $ \\ 
 $ (BOX2F_{dSalary} \leftrightarrow BOX19P_{dSalary}) \land $ \\ 
 $ (BOX16F_{S10} \leftrightarrow BOX9P_{S10}) \land $ \\ 
 $ (E2SalaryF_{S13} \leftrightarrow E2SalaryP_{S13}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX14F_{dSalary} \leftrightarrow BOX7P_{dSalary}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (E1SalaryF_{S15} \leftrightarrow E1SalaryP_{S15}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (BOX11F_{S14} \leftrightarrow BOX4P_{S14}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (PersonF_{S11} \leftrightarrow PersonP_{S11}) \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 $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX10F_{S5} \leftrightarrow BOX3P_{S5}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (PersonF_{S17} \leftrightarrow PersonP_{S17}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX13F_{S20} \leftrightarrow BOX6P_{S20}) \land $ \\ 
 $ (BOX12F_{S7} \leftrightarrow BOX5P_{S7}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (PersonF_{S10} \leftrightarrow PersonP_{S10}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (PersonF_{S4} \leftrightarrow PersonP_{S4}) \land $ \\ 
 $ (BOX12F_{S15} \leftrightarrow BOX5P_{S15}) \land $ \\ 
 $ (BOX2F_{S20} \leftrightarrow BOX19P_{S20}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (BOX13F_{S12} \leftrightarrow BOX6P_{S12}) \land $ \\ 
 $ (PersonF_{S19} \leftrightarrow PersonP_{S19}) \land $ \\ 
 $ (BOX15F_{S8} \leftrightarrow BOX8P_{S8}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (BOX14F_{S17} \leftrightarrow BOX7P_{S17}) \land $ \\ 
 $ (BOX2F_{S1} \leftrightarrow BOX19P_{S1}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (BOX13F_{S16} \leftrightarrow BOX6P_{S16}) \land $ \\ 
 $ (PersonF_{S6} \leftrightarrow PersonP_{S6}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX15F_{S12} \leftrightarrow BOX8P_{S12}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (BOX16F_{dSalary} \leftrightarrow BOX9P_{dSalary}) \land $ \\ 
 $ (BOX15F_{S13} \leftrightarrow BOX8P_{S13}) \land $ \\ 
 $ (BOX15F_{S5} \leftrightarrow BOX8P_{S5}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX0F_{S5} \leftrightarrow BOX17P_{S5}) \land $ \\ 
 $ (BOX1F_{S20} \leftrightarrow BOX18P_{S20}) \land $ \\ 
 $ (BOX0F_{S2} \leftrightarrow BOX17P_{S2}) \land $ \\ 
 $ (E1SalaryF_{S9} \leftrightarrow E1SalaryP_{S9}) \land $ \\ 
 $ (BOX11F_{John} \leftrightarrow BOX4P_{John}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX16F_{S16} \leftrightarrow BOX9P_{S16}) \land $ \\ 
 $ (E1SalaryF_{S13} \leftrightarrow E1SalaryP_{S13}) \land $ \\ 
 $ (BOX10F_{S8} \leftrightarrow BOX3P_{S8}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (BOX11F_{S12} \leftrightarrow BOX4P_{S12}) \land $ \\ 
 $  \Rbox ((BOX12F_{S14} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S14} \leftrightarrow ( \Rnext ((PersonP_{S14} \rightarrow E1SalaryP_{S14}) \land $ \\ 
 $ (PersonP_{S14} \rightarrow  \lnot E2SalaryP_{S14}) \land $ \\ 
 $ (E2SalaryP_{S14} \rightarrow E1SalaryP_{S14})) \land $ \\ 
 $ BOX9P_{S14})) \land $ \\ 
 $ ( \Rnext BOX14F_{S14} \leftrightarrow ( \Rnext BOX15F_{S14} \land $ \\ 
 $ BOX14F_{S14})) \land $ \\ 
 $ (BOX17P_{S14} \leftrightarrow  \Rbox BOX3P_{S14}) \land $ \\ 
 $ (BOX13F_{S14} \leftrightarrow  \Rbox (E1SalaryInvF_{S14} \rightarrow BOX14F_{S14})) \land $ \\ 
 $ (BOX10F_{S14} \leftrightarrow  \Rbox (E1SalaryF_{S14} \rightarrow BOX11F_{S14})) \land $ \\ 
 $ ( \Rnext BOX8P_{S14} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S14})) \land $ \\ 
 $ (BOX7P_{S14} \leftrightarrow  \Rbox BOX8P_{S14}) \land $ \\ 
 $ ( \Rnext BOX5P_{S14} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S14})) \land $ \\ 
 $ (BOX18P_{S14} \leftrightarrow  \Rbox BOX6P_{S14}) \land $ \\ 
 $ ( \Rnext BOX11F_{S14} \leftrightarrow ( \Rnext BOX12F_{S14} \land $ \\ 
 $ BOX11F_{S14})) \land $ \\ 
 $ ( \Rnext BOX1F_{S14} \leftrightarrow ( \Rnext BOX13F_{S14} \land $ \\ 
 $ BOX1F_{S14})) \land $ \\ 
 $ (BOX19P_{S14} \leftrightarrow  \Rbox BOX9P_{S14}) \land $ \\ 
 $ ( \Rnext BOX6P_{S14} \leftrightarrow ( \Rnext (E1SalaryInvP_{S14} \rightarrow BOX7P_{S14}) \land $ \\ 
 $ BOX6P_{S14})) \land $ \\ 
 $ ( \Rnext BOX3P_{S14} \leftrightarrow ( \Rnext (E1SalaryP_{S14} \rightarrow BOX4P_{S14}) \land $ \\ 
 $ BOX3P_{S14})) \land $ \\ 
 $ ( \Rnext BOX2F_{S14} \leftrightarrow ( \Rnext BOX16F_{S14} \land $ \\ 
 $ BOX2F_{S14})) \land $ \\ 
 $ (BOX4P_{S14} \leftrightarrow  \Rbox BOX5P_{S14}) \land $ \\ 
 $ (BOX15F_{S14} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S14} \leftrightarrow  \Rbox ((PersonF_{S14} \rightarrow E1SalaryF_{S14}) \land $ \\ 
 $ (PersonF_{S14} \rightarrow  \lnot E2SalaryF_{S14}) \land $ \\ 
 $ (E2SalaryF_{S14} \rightarrow E1SalaryF_{S14}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S14} \leftrightarrow ( \Rnext BOX10F_{S14} \land $ \\ 
 $ BOX0F_{S14}))) \land $ \\ 
 $ (E1SalaryF_{S2} \leftrightarrow E1SalaryP_{S2}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (E2SalaryF_{dSalaryInv} \leftrightarrow E2SalaryP_{dSalaryInv}) \land $ \\ 
 $ (BOX0F_{dSalary} \leftrightarrow BOX17P_{dSalary}) \land $ \\ 
 $ (E1SalaryInvF_{S1} \leftrightarrow E1SalaryInvP_{S1}) \land $ \\ 
 $ (BOX1F_{S7} \leftrightarrow BOX18P_{S7}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (E2SalaryF_{S1} \leftrightarrow E2SalaryP_{S1}) \land $ \\ 
 $ (BOX15F_{S11} \leftrightarrow BOX8P_{S11}) \land $ \\ 
 $ (BOX10F_{S2} \leftrightarrow BOX3P_{S2}) \land $ \\ 
 $ (PersonF_{S20} \leftrightarrow PersonP_{S20}) \land $ \\ 
 $ (BOX1F_{S15} \leftrightarrow BOX18P_{S15}) \land $ \\ 
 $ (BOX1F_{S4} \leftrightarrow BOX18P_{S4}) \land $ \\ 
 $ (BOX1F_{John} \leftrightarrow BOX18P_{John}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX11F_{S3} \leftrightarrow BOX4P_{S3}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (E1SalaryInvF_{S4} \leftrightarrow E1SalaryInvP_{S4}) \land $ \\ 
 $ (BOX12F_{S14} \leftrightarrow BOX5P_{S14}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX10F_{dSalaryInv} \leftrightarrow BOX3P_{dSalaryInv}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX14F_{John} \leftrightarrow BOX7P_{John}) \land $ \\ 
 $ (BOX0F_{S11} \leftrightarrow BOX17P_{S11}) \land $ \\ 
 $ (E2SalaryF_{S2} \leftrightarrow E2SalaryP_{S2}) \land $ \\ 
 $ (E1SalaryInvF_{S9} \leftrightarrow E1SalaryInvP_{S9}) \land $ \\ 
 $ (BOX15F_{S15} \leftrightarrow BOX8P_{S15}) \land $ \\ 
 $ (BOX13F_{S14} \leftrightarrow BOX6P_{S14}) \land $ \\ 
 $ (E1SalaryF_{S16} \leftrightarrow E1SalaryP_{S16}) \land $ \\ 
 $ (BOX14F_{S15} \leftrightarrow BOX7P_{S15}) \land $ \\ 
 $ (BOX11F_{S20} \leftrightarrow BOX4P_{S20}) \land $ \\ 
 $ (BOX1F_{S18} \leftrightarrow BOX18P_{S18}) \land $ \\ 
 $ (E2SalaryF_{S7} \leftrightarrow E2SalaryP_{S7}) \land $ \\ 
 $ (E2SalaryF_{S12} \leftrightarrow E2SalaryP_{S12}) \land $ \\ 
 $ (BOX1F_{S1} \leftrightarrow BOX18P_{S1}) \land $ \\ 
 $ (E1SalaryF_{S4} \leftrightarrow E1SalaryP_{S4}) \land $ \\ 
 $ (PersonF_{dSalaryInv} \leftrightarrow PersonP_{dSalaryInv}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (BOX15F_{dSalaryInv} \leftrightarrow BOX8P_{dSalaryInv}) \land $ \\ 
 $ (BOX11F_{S10} \leftrightarrow BOX4P_{S10}) \land $ \\ 
 $ (BOX1F_{dSalaryInv} \leftrightarrow BOX18P_{dSalaryInv}) \land $ \\ 
 $ (BOX12F_{S18} \leftrightarrow BOX5P_{S18}) \land $ \\ 
 $ (E1SalaryF_{S1} \leftrightarrow E1SalaryP_{S1}) \land $ \\ 
 $ (E1SalaryInvF_{S6} \leftrightarrow E1SalaryInvP_{S6}) \land $ \\ 
 $ (BOX1F_{S12} \leftrightarrow BOX18P_{S12}) \land $ \\ 
 $ (BOX0F_{S20} \leftrightarrow BOX17P_{S20}) \land $ \\ 
 $ (E2SalaryF_{S3} \leftrightarrow E2SalaryP_{S3}) \land $ \\ 
 $ (BOX13F_{S11} \leftrightarrow BOX6P_{S11}) \land $ \\ 
 $ (E1SalaryF_{S18} \leftrightarrow E1SalaryP_{S18}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (E1SalaryF_{S7} \leftrightarrow E1SalaryP_{S7}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (BOX11F_{S2} \leftrightarrow BOX4P_{S2}) \land $ \\ 
 $ (BOX0F_{S14} \leftrightarrow BOX17P_{S14}) \land $ \\ 
 $ (BOX10F_{S17} \leftrightarrow BOX3P_{S17}) \land $ \\ 
 $ (E2SalaryF_{S18} \leftrightarrow E2SalaryP_{S18}) \land $ \\ 
 $ (BOX0F_{S19} \leftrightarrow BOX17P_{S19}) \land $ \\ 
 $ (BOX0F_{S12} \leftrightarrow BOX17P_{S12}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (E1SalaryF_{S12} \leftrightarrow E1SalaryP_{S12}) \land $ \\ 
 $ (BOX12F_{S5} \leftrightarrow BOX5P_{S5}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (E1SalaryF_{S19} \leftrightarrow E1SalaryP_{S19}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX16F_{S12} \leftrightarrow BOX9P_{S12}) \land $ \\ 
 $ (BOX14F_{dSalaryInv} \leftrightarrow BOX7P_{dSalaryInv}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (E1SalaryInvF_{S17} \leftrightarrow E1SalaryInvP_{S17}) \land $ \\ 
 $  \Rbox ((BOX12F_{S2} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S2} \leftrightarrow ( \Rnext ((PersonP_{S2} \rightarrow E1SalaryP_{S2}) \land $ \\ 
 $ (PersonP_{S2} \rightarrow  \lnot E2SalaryP_{S2}) \land $ \\ 
 $ (E2SalaryP_{S2} \rightarrow E1SalaryP_{S2})) \land $ \\ 
 $ BOX9P_{S2})) \land $ \\ 
 $ ( \Rnext BOX14F_{S2} \leftrightarrow ( \Rnext BOX15F_{S2} \land $ \\ 
 $ BOX14F_{S2})) \land $ \\ 
 $ (BOX17P_{S2} \leftrightarrow  \Rbox BOX3P_{S2}) \land $ \\ 
 $ (BOX13F_{S2} \leftrightarrow  \Rbox (E1SalaryInvF_{S2} \rightarrow BOX14F_{S2})) \land $ \\ 
 $ (BOX10F_{S2} \leftrightarrow  \Rbox (E1SalaryF_{S2} \rightarrow BOX11F_{S2})) \land $ \\ 
 $ ( \Rnext BOX8P_{S2} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S2})) \land $ \\ 
 $ (BOX7P_{S2} \leftrightarrow  \Rbox BOX8P_{S2}) \land $ \\ 
 $ ( \Rnext BOX5P_{S2} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S2})) \land $ \\ 
 $ (BOX18P_{S2} \leftrightarrow  \Rbox BOX6P_{S2}) \land $ \\ 
 $ ( \Rnext BOX11F_{S2} \leftrightarrow ( \Rnext BOX12F_{S2} \land $ \\ 
 $ BOX11F_{S2})) \land $ \\ 
 $ ( \Rnext BOX1F_{S2} \leftrightarrow ( \Rnext BOX13F_{S2} \land $ \\ 
 $ BOX1F_{S2})) \land $ \\ 
 $ (BOX19P_{S2} \leftrightarrow  \Rbox BOX9P_{S2}) \land $ \\ 
 $ ( \Rnext BOX6P_{S2} \leftrightarrow ( \Rnext (E1SalaryInvP_{S2} \rightarrow BOX7P_{S2}) \land $ \\ 
 $ BOX6P_{S2})) \land $ \\ 
 $ ( \Rnext BOX3P_{S2} \leftrightarrow ( \Rnext (E1SalaryP_{S2} \rightarrow BOX4P_{S2}) \land $ \\ 
 $ BOX3P_{S2})) \land $ \\ 
 $ ( \Rnext BOX2F_{S2} \leftrightarrow ( \Rnext BOX16F_{S2} \land $ \\ 
 $ BOX2F_{S2})) \land $ \\ 
 $ (BOX4P_{S2} \leftrightarrow  \Rbox BOX5P_{S2}) \land $ \\ 
 $ (BOX15F_{S2} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S2} \leftrightarrow  \Rbox ((PersonF_{S2} \rightarrow E1SalaryF_{S2}) \land $ \\ 
 $ (PersonF_{S2} \rightarrow  \lnot E2SalaryF_{S2}) \land $ \\ 
 $ (E2SalaryF_{S2} \rightarrow E1SalaryF_{S2}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S2} \leftrightarrow ( \Rnext BOX10F_{S2} \land $ \\ 
 $ BOX0F_{S2}))) \land $ \\ 
 $  \Rbox ((BOX12F_{S8} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S8} \leftrightarrow ( \Rnext ((PersonP_{S8} \rightarrow E1SalaryP_{S8}) \land $ \\ 
 $ (PersonP_{S8} \rightarrow  \lnot E2SalaryP_{S8}) \land $ \\ 
 $ (E2SalaryP_{S8} \rightarrow E1SalaryP_{S8})) \land $ \\ 
 $ BOX9P_{S8})) \land $ \\ 
 $ ( \Rnext BOX14F_{S8} \leftrightarrow ( \Rnext BOX15F_{S8} \land $ \\ 
 $ BOX14F_{S8})) \land $ \\ 
 $ (BOX17P_{S8} \leftrightarrow  \Rbox BOX3P_{S8}) \land $ \\ 
 $ (BOX13F_{S8} \leftrightarrow  \Rbox (E1SalaryInvF_{S8} \rightarrow BOX14F_{S8})) \land $ \\ 
 $ (BOX10F_{S8} \leftrightarrow  \Rbox (E1SalaryF_{S8} \rightarrow BOX11F_{S8})) \land $ \\ 
 $ ( \Rnext BOX8P_{S8} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S8})) \land $ \\ 
 $ (BOX7P_{S8} \leftrightarrow  \Rbox BOX8P_{S8}) \land $ \\ 
 $ ( \Rnext BOX5P_{S8} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S8})) \land $ \\ 
 $ (BOX18P_{S8} \leftrightarrow  \Rbox BOX6P_{S8}) \land $ \\ 
 $ ( \Rnext BOX11F_{S8} \leftrightarrow ( \Rnext BOX12F_{S8} \land $ \\ 
 $ BOX11F_{S8})) \land $ \\ 
 $ ( \Rnext BOX1F_{S8} \leftrightarrow ( \Rnext BOX13F_{S8} \land $ \\ 
 $ BOX1F_{S8})) \land $ \\ 
 $ (BOX19P_{S8} \leftrightarrow  \Rbox BOX9P_{S8}) \land $ \\ 
 $ ( \Rnext BOX6P_{S8} \leftrightarrow ( \Rnext (E1SalaryInvP_{S8} \rightarrow BOX7P_{S8}) \land $ \\ 
 $ BOX6P_{S8})) \land $ \\ 
 $ ( \Rnext BOX3P_{S8} \leftrightarrow ( \Rnext (E1SalaryP_{S8} \rightarrow BOX4P_{S8}) \land $ \\ 
 $ BOX3P_{S8})) \land $ \\ 
 $ ( \Rnext BOX2F_{S8} \leftrightarrow ( \Rnext BOX16F_{S8} \land $ \\ 
 $ BOX2F_{S8})) \land $ \\ 
 $ (BOX4P_{S8} \leftrightarrow  \Rbox BOX5P_{S8}) \land $ \\ 
 $ (BOX15F_{S8} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S8} \leftrightarrow  \Rbox ((PersonF_{S8} \rightarrow E1SalaryF_{S8}) \land $ \\ 
 $ (PersonF_{S8} \rightarrow  \lnot E2SalaryF_{S8}) \land $ \\ 
 $ (E2SalaryF_{S8} \rightarrow E1SalaryF_{S8}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S8} \leftrightarrow ( \Rnext BOX10F_{S8} \land $ \\ 
 $ BOX0F_{S8}))) \land $ \\ 
 $ (BOX13F_{S6} \leftrightarrow BOX6P_{S6}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (BOX15F_{S6} \leftrightarrow BOX8P_{S6}) \land $ \\ 
 $ (E1SalaryInvF_{dSalary} \leftrightarrow E1SalaryInvP_{dSalary}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX12F_{S6} \leftrightarrow BOX5P_{S6}) \land $ \\ 
 $ (E2SalaryF_{S5} \leftrightarrow E2SalaryP_{S5}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (BOX11F_{S15} \leftrightarrow BOX4P_{S15}) \land $ \\ 
 $ (BOX12F_{S4} \leftrightarrow BOX5P_{S4}) \land $ \\ 
 $ (BOX1F_{S6} \leftrightarrow BOX18P_{S6}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (E1SalaryF_{S8} \leftrightarrow E1SalaryP_{S8}) \land $ \\ 
 $ (BOX11F_{dSalary} \leftrightarrow BOX4P_{dSalary}) \land $ \\ 
 $ (E1SalaryInvF_{S15} \leftrightarrow E1SalaryInvP_{S15}) \land $ \\ 
 $ (BOX11F_{S19} \leftrightarrow BOX4P_{S19}) \land $ \\ 
 $ (BOX0F_{John} \leftrightarrow BOX17P_{John}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (BOX11F_{S17} \leftrightarrow BOX4P_{S17}) \land $ \\ 
 $ (BOX1F_{S5} \leftrightarrow BOX18P_{S5}) \land $ \\ 
 $ (BOX10F_{S15} \leftrightarrow BOX3P_{S15}) \land $ \\ 
 $ (BOX10F_{S12} \leftrightarrow BOX3P_{S12}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (E1SalaryF_{S10} \leftrightarrow E1SalaryP_{S10}) \land $ \\ 
 $ (PersonF_{S3} \leftrightarrow PersonP_{S3}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX10F_{S20} \leftrightarrow BOX3P_{S20}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX16F_{S6} \leftrightarrow BOX9P_{S6}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (BOX14F_{S12} \leftrightarrow BOX7P_{S12}) \land $ \\ 
 $ (BOX10F_{S1} \leftrightarrow BOX3P_{S1}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (E1SalaryInvF_{S10} \leftrightarrow E1SalaryInvP_{S10}) \land $ \\ 
 $ (BOX13F_{S2} \leftrightarrow BOX6P_{S2}) \land $ \\ 
 $ (BOX13F_{dSalary} \leftrightarrow BOX6P_{dSalary}) \land $ \\ 
 $ (E1SalaryF_{S5} \leftrightarrow E1SalaryP_{S5}) \land $ \\ 
 $ (PersonF_{S2} \leftrightarrow PersonP_{S2}) \land $ \\ 
 $ (E2SalaryF_{S15} \leftrightarrow E2SalaryP_{S15}) \land $ \\ 
 $ (BOX16F_{S2} \leftrightarrow BOX9P_{S2}) \land $ \\ 
 $ (BOX15F_{S2} \leftrightarrow BOX8P_{S2}) \land $ \\ 
 $ (BOX0F_{dSalaryInv} \leftrightarrow BOX17P_{dSalaryInv}) \land $ \\ 
 $ (BOX14F_{S18} \leftrightarrow BOX7P_{S18}) \land $ \\ 
 $ (E1SalaryInvF_{S14} \leftrightarrow E1SalaryInvP_{S14}) \land $ \\ 
 $ (BOX14F_{S3} \leftrightarrow BOX7P_{S3}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (BOX10F_{S11} \leftrightarrow BOX3P_{S11}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (BOX11F_{S1} \leftrightarrow BOX4P_{S1}) \land $ \\ 
 $ (BOX14F_{S10} \leftrightarrow BOX7P_{S10}) \land $ \\ 
 $ (BOX10F_{John} \leftrightarrow BOX3P_{John}) \land $ \\ 
 $ (BOX15F_{S7} \leftrightarrow BOX8P_{S7}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (BOX12F_{S11} \leftrightarrow BOX5P_{S11}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX15F_{S1} \leftrightarrow BOX8P_{S1}) \land $ \\ 
 $ (BOX12F_{S2} \leftrightarrow BOX5P_{S2}) \land $ \\ 
 $ (BOX11F_{S11} \leftrightarrow BOX4P_{S11}) \land $ \\ 
 $ (BOX2F_{S2} \leftrightarrow BOX19P_{S2}) \land $ \\ 
 $ (E1SalaryF_{S14} \leftrightarrow E1SalaryP_{S14}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (BOX10F_{S7} \leftrightarrow BOX3P_{S7}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (PersonF_{S12} \leftrightarrow PersonP_{S12}) \land $ \\ 
 $ (BOX14F_{S1} \leftrightarrow BOX7P_{S1}) \land $ \\ 
 $ (PersonF_{S14} \leftrightarrow PersonP_{S14}) \land $ \\ 
 $ (E2SalaryF_{dSalary} \leftrightarrow E2SalaryP_{dSalary}) \land $ \\ 
 $ (BOX1F_{S8} \leftrightarrow BOX18P_{S8}) \land $ \\ 
 $ (BOX2F_{S6} \leftrightarrow BOX19P_{S6}) \land $ \\ 
 $ (BOX2F_{S3} \leftrightarrow BOX19P_{S3}) \land $ \\ 
 $ (BOX14F_{S6} \leftrightarrow BOX7P_{S6}) \land $ \\ 
 $ (E2SalaryF_{S16} \leftrightarrow E2SalaryP_{S16}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX15F_{S18} \leftrightarrow BOX8P_{S18}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX1F_{S10} \leftrightarrow BOX18P_{S10}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX16F_{S1} \leftrightarrow BOX9P_{S1}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX2F_{S19} \leftrightarrow BOX19P_{S19}) \land $ \\ 
 $ (E1SalaryInvF_{S12} \leftrightarrow E1SalaryInvP_{S12}) \land $ \\ 
 $ (BOX13F_{S3} \leftrightarrow BOX6P_{S3}) \land $ \\ 
 $ (BOX0F_{S6} \leftrightarrow BOX17P_{S6}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryF) \land $ \\ 
 $ (BOX14F_{S9} \leftrightarrow BOX7P_{S9}) \land $ \\ 
 $ (E2SalaryF_{S6} \leftrightarrow E2SalaryP_{S6}) \land $ \\ 
 $  \Rbox ((BOX12F_{S10} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S10} \leftrightarrow ( \Rnext ((PersonP_{S10} \rightarrow E1SalaryP_{S10}) \land $ \\ 
 $ (PersonP_{S10} \rightarrow  \lnot E2SalaryP_{S10}) \land $ \\ 
 $ (E2SalaryP_{S10} \rightarrow E1SalaryP_{S10})) \land $ \\ 
 $ BOX9P_{S10})) \land $ \\ 
 $ ( \Rnext BOX14F_{S10} \leftrightarrow ( \Rnext BOX15F_{S10} \land $ \\ 
 $ BOX14F_{S10})) \land $ \\ 
 $ (BOX17P_{S10} \leftrightarrow  \Rbox BOX3P_{S10}) \land $ \\ 
 $ (BOX13F_{S10} \leftrightarrow  \Rbox (E1SalaryInvF_{S10} \rightarrow BOX14F_{S10})) \land $ \\ 
 $ (BOX10F_{S10} \leftrightarrow  \Rbox (E1SalaryF_{S10} \rightarrow BOX11F_{S10})) \land $ \\ 
 $ ( \Rnext BOX8P_{S10} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S10})) \land $ \\ 
 $ (BOX7P_{S10} \leftrightarrow  \Rbox BOX8P_{S10}) \land $ \\ 
 $ ( \Rnext BOX5P_{S10} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S10})) \land $ \\ 
 $ (BOX18P_{S10} \leftrightarrow  \Rbox BOX6P_{S10}) \land $ \\ 
 $ ( \Rnext BOX11F_{S10} \leftrightarrow ( \Rnext BOX12F_{S10} \land $ \\ 
 $ BOX11F_{S10})) \land $ \\ 
 $ ( \Rnext BOX1F_{S10} \leftrightarrow ( \Rnext BOX13F_{S10} \land $ \\ 
 $ BOX1F_{S10})) \land $ \\ 
 $ (BOX19P_{S10} \leftrightarrow  \Rbox BOX9P_{S10}) \land $ \\ 
 $ ( \Rnext BOX6P_{S10} \leftrightarrow ( \Rnext (E1SalaryInvP_{S10} \rightarrow BOX7P_{S10}) \land $ \\ 
 $ BOX6P_{S10})) \land $ \\ 
 $ ( \Rnext BOX3P_{S10} \leftrightarrow ( \Rnext (E1SalaryP_{S10} \rightarrow BOX4P_{S10}) \land $ \\ 
 $ BOX3P_{S10})) \land $ \\ 
 $ ( \Rnext BOX2F_{S10} \leftrightarrow ( \Rnext BOX16F_{S10} \land $ \\ 
 $ BOX2F_{S10})) \land $ \\ 
 $ (BOX4P_{S10} \leftrightarrow  \Rbox BOX5P_{S10}) \land $ \\ 
 $ (BOX15F_{S10} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S10} \leftrightarrow  \Rbox ((PersonF_{S10} \rightarrow E1SalaryF_{S10}) \land $ \\ 
 $ (PersonF_{S10} \rightarrow  \lnot E2SalaryF_{S10}) \land $ \\ 
 $ (E2SalaryF_{S10} \rightarrow E1SalaryF_{S10}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S10} \leftrightarrow ( \Rnext BOX10F_{S10} \land $ \\ 
 $ BOX0F_{S10}))) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $  \Rbox ((BOX12F_{S16} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S16} \leftrightarrow ( \Rnext ((PersonP_{S16} \rightarrow E1SalaryP_{S16}) \land $ \\ 
 $ (PersonP_{S16} \rightarrow  \lnot E2SalaryP_{S16}) \land $ \\ 
 $ (E2SalaryP_{S16} \rightarrow E1SalaryP_{S16})) \land $ \\ 
 $ BOX9P_{S16})) \land $ \\ 
 $ ( \Rnext BOX14F_{S16} \leftrightarrow ( \Rnext BOX15F_{S16} \land $ \\ 
 $ BOX14F_{S16})) \land $ \\ 
 $ (BOX17P_{S16} \leftrightarrow  \Rbox BOX3P_{S16}) \land $ \\ 
 $ (BOX13F_{S16} \leftrightarrow  \Rbox (E1SalaryInvF_{S16} \rightarrow BOX14F_{S16})) \land $ \\ 
 $ (BOX10F_{S16} \leftrightarrow  \Rbox (E1SalaryF_{S16} \rightarrow BOX11F_{S16})) \land $ \\ 
 $ ( \Rnext BOX8P_{S16} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S16})) \land $ \\ 
 $ (BOX7P_{S16} \leftrightarrow  \Rbox BOX8P_{S16}) \land $ \\ 
 $ ( \Rnext BOX5P_{S16} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S16})) \land $ \\ 
 $ (BOX18P_{S16} \leftrightarrow  \Rbox BOX6P_{S16}) \land $ \\ 
 $ ( \Rnext BOX11F_{S16} \leftrightarrow ( \Rnext BOX12F_{S16} \land $ \\ 
 $ BOX11F_{S16})) \land $ \\ 
 $ ( \Rnext BOX1F_{S16} \leftrightarrow ( \Rnext BOX13F_{S16} \land $ \\ 
 $ BOX1F_{S16})) \land $ \\ 
 $ (BOX19P_{S16} \leftrightarrow  \Rbox BOX9P_{S16}) \land $ \\ 
 $ ( \Rnext BOX6P_{S16} \leftrightarrow ( \Rnext (E1SalaryInvP_{S16} \rightarrow BOX7P_{S16}) \land $ \\ 
 $ BOX6P_{S16})) \land $ \\ 
 $ ( \Rnext BOX3P_{S16} \leftrightarrow ( \Rnext (E1SalaryP_{S16} \rightarrow BOX4P_{S16}) \land $ \\ 
 $ BOX3P_{S16})) \land $ \\ 
 $ ( \Rnext BOX2F_{S16} \leftrightarrow ( \Rnext BOX16F_{S16} \land $ \\ 
 $ BOX2F_{S16})) \land $ \\ 
 $ (BOX4P_{S16} \leftrightarrow  \Rbox BOX5P_{S16}) \land $ \\ 
 $ (BOX15F_{S16} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S16} \leftrightarrow  \Rbox ((PersonF_{S16} \rightarrow E1SalaryF_{S16}) \land $ \\ 
 $ (PersonF_{S16} \rightarrow  \lnot E2SalaryF_{S16}) \land $ \\ 
 $ (E2SalaryF_{S16} \rightarrow E1SalaryF_{S16}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S16} \leftrightarrow ( \Rnext BOX10F_{S16} \land $ \\ 
 $ BOX0F_{S16}))) \land $ \\ 
 $ (BOX14F_{S14} \leftrightarrow BOX7P_{S14}) \land $ \\ 
 $ (BOX2F_{S13} \leftrightarrow BOX19P_{S13}) \land $ \\ 
 $ (BOX11F_{S18} \leftrightarrow BOX4P_{S18}) \land $ \\ 
 $ (BOX2F_{John} \leftrightarrow BOX19P_{John}) \land $ \\ 
 $ (BOX2F_{S15} \leftrightarrow BOX19P_{S15}) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (BOX16F_{dSalaryInv} \leftrightarrow BOX9P_{dSalaryInv}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (E2SalaryF_{S10} \leftrightarrow E2SalaryP_{S10}) \land $ \\ 
 $ (E1SalaryInvF_{John} \leftrightarrow E1SalaryInvP_{John}) \land $ \\ 
 $ (BOX2F_{S8} \leftrightarrow BOX19P_{S8}) \land $ \\ 
 $ (PersonF_{S18} \leftrightarrow PersonP_{S18}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX15F_{John} \leftrightarrow BOX8P_{John}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX0F_{S4} \leftrightarrow BOX17P_{S4}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (E1SalaryInvF_{S13} \leftrightarrow E1SalaryInvP_{S13}) \land $ \\ 
 $ (BOX2F_{dSalaryInv} \leftrightarrow BOX19P_{dSalaryInv}) \land $ \\ 
 $ (BOX14F_{S20} \leftrightarrow BOX7P_{S20}) \land $ \\ 
 $ (BOX15F_{S19} \leftrightarrow BOX8P_{S19}) \land $ \\ 
 $ (E2SalaryF_{S4} \leftrightarrow E2SalaryP_{S4}) \land $ \\ 
 $ (BOX0F_{S7} \leftrightarrow BOX17P_{S7}) \land $ \\ 
 $  \Rbox ((BOX12F_{S5} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S5} \leftrightarrow ( \Rnext ((PersonP_{S5} \rightarrow E1SalaryP_{S5}) \land $ \\ 
 $ (PersonP_{S5} \rightarrow  \lnot E2SalaryP_{S5}) \land $ \\ 
 $ (E2SalaryP_{S5} \rightarrow E1SalaryP_{S5})) \land $ \\ 
 $ BOX9P_{S5})) \land $ \\ 
 $ ( \Rnext BOX14F_{S5} \leftrightarrow ( \Rnext BOX15F_{S5} \land $ \\ 
 $ BOX14F_{S5})) \land $ \\ 
 $ (BOX17P_{S5} \leftrightarrow  \Rbox BOX3P_{S5}) \land $ \\ 
 $ (BOX13F_{S5} \leftrightarrow  \Rbox (E1SalaryInvF_{S5} \rightarrow BOX14F_{S5})) \land $ \\ 
 $ (BOX10F_{S5} \leftrightarrow  \Rbox (E1SalaryF_{S5} \rightarrow BOX11F_{S5})) \land $ \\ 
 $ ( \Rnext BOX8P_{S5} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S5})) \land $ \\ 
 $ (BOX7P_{S5} \leftrightarrow  \Rbox BOX8P_{S5}) \land $ \\ 
 $ ( \Rnext BOX5P_{S5} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S5})) \land $ \\ 
 $ (BOX18P_{S5} \leftrightarrow  \Rbox BOX6P_{S5}) \land $ \\ 
 $ ( \Rnext BOX11F_{S5} \leftrightarrow ( \Rnext BOX12F_{S5} \land $ \\ 
 $ BOX11F_{S5})) \land $ \\ 
 $ ( \Rnext BOX1F_{S5} \leftrightarrow ( \Rnext BOX13F_{S5} \land $ \\ 
 $ BOX1F_{S5})) \land $ \\ 
 $ (BOX19P_{S5} \leftrightarrow  \Rbox BOX9P_{S5}) \land $ \\ 
 $ ( \Rnext BOX6P_{S5} \leftrightarrow ( \Rnext (E1SalaryInvP_{S5} \rightarrow BOX7P_{S5}) \land $ \\ 
 $ BOX6P_{S5})) \land $ \\ 
 $ ( \Rnext BOX3P_{S5} \leftrightarrow ( \Rnext (E1SalaryP_{S5} \rightarrow BOX4P_{S5}) \land $ \\ 
 $ BOX3P_{S5})) \land $ \\ 
 $ ( \Rnext BOX2F_{S5} \leftrightarrow ( \Rnext BOX16F_{S5} \land $ \\ 
 $ BOX2F_{S5})) \land $ \\ 
 $ (BOX4P_{S5} \leftrightarrow  \Rbox BOX5P_{S5}) \land $ \\ 
 $ (BOX15F_{S5} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S5} \leftrightarrow  \Rbox ((PersonF_{S5} \rightarrow E1SalaryF_{S5}) \land $ \\ 
 $ (PersonF_{S5} \rightarrow  \lnot E2SalaryF_{S5}) \land $ \\ 
 $ (E2SalaryF_{S5} \rightarrow E1SalaryF_{S5}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S5} \leftrightarrow ( \Rnext BOX10F_{S5} \land $ \\ 
 $ BOX0F_{S5}))) \land $ \\ 
 $ (BOX12F_{S19} \leftrightarrow BOX5P_{S19}) \land $ \\ 
 $ (PersonF_{S13} \leftrightarrow PersonP_{S13}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryF) \land $ \\ 
 $ (BOX0F_{S1} \leftrightarrow BOX17P_{S1}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (E1SalaryInvF_{dSalaryInv} \leftrightarrow E1SalaryInvP_{dSalaryInv}) \land $ \\ 
 $ (BOX1F_{S14} \leftrightarrow BOX18P_{S14}) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX11F_{dSalaryInv} \leftrightarrow BOX4P_{dSalaryInv}) \land $ \\ 
 $ (BOX10F_{S4} \leftrightarrow BOX3P_{S4}) \land $ \\ 
 $ (BOX11F_{S6} \leftrightarrow BOX4P_{S6}) \land $ \\ 
 $ (BOX16F_{S9} \leftrightarrow BOX9P_{S9}) \land $ \\ 
 $ (E1SalaryInvF_{S5} \leftrightarrow E1SalaryInvP_{S5}) \land $ \\ 
 $ (BOX15F_{S9} \leftrightarrow BOX8P_{S9}) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (PSalaryF \rightarrow E1SalaryInvF_{dSalaryInv}) \land $ \\ 
 $ (BOX1F_{S17} \leftrightarrow BOX18P_{S17}) \land $ \\ 
 $ (BOX0F_{S8} \leftrightarrow BOX17P_{S8}) \land $ \\ 
 $ (BOX11F_{S7} \leftrightarrow BOX4P_{S7}) \land $ \\ 
 $ (PinvSalaryF \rightarrow E1SalaryF_{dSalary}) \land $ \\ 
 $ (BOX2F_{S12} \leftrightarrow BOX19P_{S12}) \land $ \\ 
 $ (E2SalaryF_{S20} \leftrightarrow E2SalaryP_{S20}) \land $ \\ 
 $ (BOX1F_{S11} \leftrightarrow BOX18P_{S11}) \land $ \\ 
 $  \Rbox ((BOX12F_{S19} \leftrightarrow  \Rbox PSalaryF) \land $ \\ 
 $ ( \Rnext BOX9P_{S19} \leftrightarrow ( \Rnext ((PersonP_{S19} \rightarrow E1SalaryP_{S19}) \land $ \\ 
 $ (PersonP_{S19} \rightarrow  \lnot E2SalaryP_{S19}) \land $ \\ 
 $ (E2SalaryP_{S19} \rightarrow E1SalaryP_{S19})) \land $ \\ 
 $ BOX9P_{S19})) \land $ \\ 
 $ ( \Rnext BOX14F_{S19} \leftrightarrow ( \Rnext BOX15F_{S19} \land $ \\ 
 $ BOX14F_{S19})) \land $ \\ 
 $ (BOX17P_{S19} \leftrightarrow  \Rbox BOX3P_{S19}) \land $ \\ 
 $ (BOX13F_{S19} \leftrightarrow  \Rbox (E1SalaryInvF_{S19} \rightarrow BOX14F_{S19})) \land $ \\ 
 $ (BOX10F_{S19} \leftrightarrow  \Rbox (E1SalaryF_{S19} \rightarrow BOX11F_{S19})) \land $ \\ 
 $ ( \Rnext BOX8P_{S19} \leftrightarrow ( \Rnext PinvSalaryF \land $ \\ 
 $ BOX8P_{S19})) \land $ \\ 
 $ (BOX7P_{S19} \leftrightarrow  \Rbox BOX8P_{S19}) \land $ \\ 
 $ ( \Rnext BOX5P_{S19} \leftrightarrow ( \Rnext PSalaryF \land $ \\ 
 $ BOX5P_{S19})) \land $ \\ 
 $ (BOX18P_{S19} \leftrightarrow  \Rbox BOX6P_{S19}) \land $ \\ 
 $ ( \Rnext BOX11F_{S19} \leftrightarrow ( \Rnext BOX12F_{S19} \land $ \\ 
 $ BOX11F_{S19})) \land $ \\ 
 $ ( \Rnext BOX1F_{S19} \leftrightarrow ( \Rnext BOX13F_{S19} \land $ \\ 
 $ BOX1F_{S19})) \land $ \\ 
 $ (BOX19P_{S19} \leftrightarrow  \Rbox BOX9P_{S19}) \land $ \\ 
 $ ( \Rnext BOX6P_{S19} \leftrightarrow ( \Rnext (E1SalaryInvP_{S19} \rightarrow BOX7P_{S19}) \land $ \\ 
 $ BOX6P_{S19})) \land $ \\ 
 $ ( \Rnext BOX3P_{S19} \leftrightarrow ( \Rnext (E1SalaryP_{S19} \rightarrow BOX4P_{S19}) \land $ \\ 
 $ BOX3P_{S19})) \land $ \\ 
 $ ( \Rnext BOX2F_{S19} \leftrightarrow ( \Rnext BOX16F_{S19} \land $ \\ 
 $ BOX2F_{S19})) \land $ \\ 
 $ (BOX4P_{S19} \leftrightarrow  \Rbox BOX5P_{S19}) \land $ \\ 
 $ (BOX15F_{S19} \leftrightarrow  \Rbox PinvSalaryF) \land $ \\ 
 $ (BOX16F_{S19} \leftrightarrow  \Rbox ((PersonF_{S19} \rightarrow E1SalaryF_{S19}) \land $ \\ 
 $ (PersonF_{S19} \rightarrow  \lnot E2SalaryF_{S19}) \land $ \\ 
 $ (E2SalaryF_{S19} \rightarrow E1SalaryF_{S19}))) \land $ \\ 
 $ ( \Rnext BOX0F_{S19} \leftrightarrow ( \Rnext BOX10F_{S19} \land $ \\ 
 $ BOX0F_{S19}))) \land $ \\ 
 $ (PersonF_{S9} \leftrightarrow PersonP_{S9}) \land $ \\ 
 $ (PSalaryF \leftrightarrow PSalaryP) \land $ \\ 
 $ (PinvSalaryF \leftrightarrow PinvSalaryP) \land $ \\ 
 $ (BOX10F_{S3} \leftrightarrow BOX3P_{S3}) \land $ \\ 
 $ (BOX1F_{S9} \leftrightarrow BOX18P_{S9}) \land $ \\ 
 $ (BOX16F_{S13} \leftrightarrow BOX9P_{S13}) \land $ \\ 
 $ (BOX12F_{dSalaryInv} \leftrightarrow BOX5P_{dSalaryInv}) \land $ \\ 
 $ (E1SalaryF_{dSalary} \leftrightarrow E1SalaryP_{dSalary}) \land $ \\ 
 $ (BOX15F_{dSalary} \leftrightarrow BOX8P_{dSalary}) \land $ \\ 
 $ (BOX15F_{S17} \leftrightarrow BOX8P_{S17}) \land $ \\ 
 $ (PersonF_{John} \leftrightarrow PersonP_{John}) \land $ \\ 
 $  \Rnext E1SalaryInvF_{S3} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E2SalaryF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E2SalaryF_{John} \land $ \\ 
 $  \Rnext E2SalaryF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S14} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E2SalaryF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E2SalaryF_{John} \land $ \\ 
 $  \Rnext  \Rnext E1SalaryInvF_{S5} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S20} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E2SalaryF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S8} \land $ \\ 
 $  \Rnext  \Rnext E2SalaryF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S13} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S15} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S12} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S9} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E2SalaryF_{John} \land $ \\ 
 $  \Rnext  \Rnext E1SalaryInvF_{S6} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E2SalaryF_{John} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S10} \land $ \\ 
 $  \Rnext E1SalaryInvF_{S4} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S7} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S11} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S16} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S17} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S18} \land $ \\ 
 $  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext  \Rnext E1SalaryInvF_{S19} \land $ \\ 
 $ BOX1F_{S6} \land $ \\ 
 $ BOX1F_{S3} \land $ \\ 
 $ BOX1F_{S4} \land $ \\ 
 $ BOX1F_{S5} \land $ \\ 
 $ BOX1F_{S14} \land $ \\ 
 $ BOX1F_{S16} \land $ \\ 
 $ BOX1F_{S12} \land $ \\ 
 $ BOX1F_{S18} \land $ \\ 
 $ BOX1F_{S13} \land $ \\ 
 $ BOX1F_{S7} \land $ \\ 
 $ BOX1F_{S8} \land $ \\ 
 $ BOX1F_{S9} \land $ \\ 
 $ BOX1F_{John} \land $ \\ 
 $ BOX1F_{dSalaryInv} \land $ \\ 
 $ BOX1F_{dSalary} \land $ \\ 
 $ BOX1F_{S19} \land $ \\ 
 $ BOX1F_{S2} \land $ \\ 
 $ BOX1F_{S15} \land $ \\ 
 $ BOX1F_{S20} \land $ \\ 
 $ BOX1F_{S17} \land $ \\ 
 $ BOX1F_{S10} \land $ \\ 
 $ BOX1F_{S1} \land $ \\ 
 $ BOX1F_{S11} \land $ \\ 
 $ BOX2F_{S3} \land $ \\ 
 $ BOX2F_{S4} \land $ \\ 
 $ BOX2F_{S12} \land $ \\ 
 $ BOX2F_{S5} \land $ \\ 
 $ BOX2F_{S6} \land $ \\ 
 $ BOX2F_{S7} \land $ \\ 
 $ BOX2F_{S10} \land $ \\ 
 $ BOX2F_{dSalary} \land $ \\ 
 $ BOX2F_{S8} \land $ \\ 
 $ BOX2F_{S13} \land $ \\ 
 $ BOX2F_{S1} \land $ \\ 
 $ BOX2F_{S14} \land $ \\ 
 $ BOX2F_{S9} \land $ \\ 
 $ BOX2F_{S11} \land $ \\ 
 $ BOX2F_{John} \land $ \\ 
 $ BOX2F_{dSalaryInv} \land $ \\ 
 $ BOX2F_{S16} \land $ \\ 
 $ BOX2F_{S15} \land $ \\ 
 $ BOX2F_{S19} \land $ \\ 
 $ BOX2F_{S2} \land $ \\ 
 $ BOX2F_{S20} \land $ \\ 
 $ BOX2F_{S17} \land $ \\ 
 $ BOX2F_{S18} \land $ \\ 
 $ BOX0F_{S11} \land $ \\ 
 $ BOX0F_{S3} \land $ \\ 
 $ BOX0F_{S4} \land $ \\ 
 $ BOX0F_{S5} \land $ \\ 
 $ BOX0F_{S6} \land $ \\ 
 $ BOX0F_{S14} \land $ \\ 
 $ BOX0F_{dSalary} \land $ \\ 
 $ BOX0F_{S13} \land $ \\ 
 $ BOX0F_{S19} \land $ \\ 
 $ BOX0F_{S2} \land $ \\ 
 $ BOX0F_{S7} \land $ \\ 
 $ BOX0F_{S8} \land $ \\ 
 $ BOX0F_{S16} \land $ \\ 
 $ BOX0F_{S1} \land $ \\ 
 $ BOX0F_{S12} \land $ \\ 
 $ BOX0F_{S18} \land $ \\ 
 $ BOX0F_{S9} \land $ \\ 
 $ BOX0F_{S15} \land $ \\ 
 $ BOX0F_{John} \land $ \\ 
 $ BOX0F_{dSalaryInv} \land $ \\ 
 $ BOX0F_{S17} \land $ \\ 
 $ BOX0F_{S10} \land $ \\ 
 $ BOX0F_{S20} \land $ \\ 
 $ E1SalaryInvF_{S1} \land $ \\ 
 $ E1SalaryInvF_{S2} \land $ \\ 
 $ PersonF_{John} \land $ \\ 
 $ E2SalaryF_{John})$ 
\end{document}