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


$( \SVbox ((PersonF_{dNameInv} \leftrightarrow PersonP_{dNameInv}) \land $ \\ 
 $ (PersonF_{dName} \rightarrow  \lnot E2NameF_{dName}) \land $ \\ 
 $ (E1NameInvF_{dNameInv} \rightarrow StringF_{dNameInv}) \land $ \\ 
 $ (StringF_{dName} \rightarrow  \lnot PersonF_{dName}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameF) \land $ \\ 
 $ (BOX1F_{John} \leftrightarrow BOX7P_{John}) \land $ \\ 
 $ (E2NameF_{N0} \rightarrow BOX0F_{N0}) \land $ \\ 
 $ (BOX2F_{N0} \leftrightarrow BOX9P_{N0}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameF) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (BOX3F_{dNameInv} \leftrightarrow BOX18P_{dNameInv}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameF) \land $ \\ 
 $ (E1NameInvF_{N0} \rightarrow StringF_{N0}) \land $ \\ 
 $ (E1NameF_{John} \rightarrow BOX4F_{John}) \land $ \\ 
 $ (BOX13F_{N0} \leftrightarrow BOX6P_{N0}) \land $ \\ 
 $  \Rbox ((BOX1F_{dNameInv} \leftrightarrow  \Rbox BOX14F_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX3F_{dNameInv} \leftrightarrow ( \Rnext BOX16F_{dNameInv} \land $ \\ 
 $ BOX3F_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX12P_{dNameInv} \leftrightarrow ( \Rnext PNameP \land $ \\ 
 $ BOX12P_{dNameInv})) \land $ \\ 
 $ (BOX10P_{dNameInv} \leftrightarrow  \Rbox E1NameP_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX4F_{dNameInv} \leftrightarrow ( \Rnext BOX17F_{dNameInv} \land $ \\ 
 $ BOX4F_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX14F_{dNameInv} \leftrightarrow ( \Rnext E1NameInvF_{dNameInv} \land $ \\ 
 $ BOX14F_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX7P_{dNameInv} \leftrightarrow ( \Rnext BOX8P_{dNameInv} \land $ \\ 
 $ BOX7P_{dNameInv})) \land $ \\ 
 $ ( \Rnext BOX13F_{dNameInv} \leftrightarrow ( \Rnext E2NameF_{dNameInv} \land $ \\ 
 $ BOX13F_{dNameInv})) \land $ \\ 
 $ (BOX18P_{dNameInv} \leftrightarrow  \Rbox BOX11P_{dNameInv}) \land $ \\ 
 $ (BOX8P_{dNameInv} \leftrightarrow  \Rbox E1NameInvP_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX15F_{dNameInv} \leftrightarrow ( \Rnext E1NameF_{dNameInv} \land $ \\ 
 $ BOX15F_{dNameInv})) \land $ \\ 
 $ (BOX6P_{dNameInv} \leftrightarrow  \Rbox E2NameP_{dNameInv}) \land $ \\ 
 $ (BOX16F_{dNameInv} \leftrightarrow  \Rbox PinvNameF) \land $ \\ 
 $ ( \Rnext BOX9P_{dNameInv} \leftrightarrow ( \Rnext BOX10P_{dNameInv} \land $ \\ 
 $ BOX9P_{dNameInv})) \land $ \\ 
 $ (BOX19P_{dNameInv} \leftrightarrow  \Rbox BOX12P_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX11P_{dNameInv} \leftrightarrow ( \Rnext PinvNameP \land $ \\ 
 $ BOX11P_{dNameInv})) \land $ \\ 
 $ (BOX17F_{dNameInv} \leftrightarrow  \Rbox PNameF) \land $ \\ 
 $ (BOX2F_{dNameInv} \leftrightarrow  \Rbox BOX15F_{dNameInv}) \land $ \\ 
 $ ( \Rnext BOX5P_{dNameInv} \leftrightarrow ( \Rnext BOX6P_{dNameInv} \land $ \\ 
 $ BOX5P_{dNameInv})) \land $ \\ 
 $ (BOX0F_{dNameInv} \leftrightarrow  \Rbox BOX13F_{dNameInv})) \land $ \\ 
 $ (E1NameInvF_{dName} \rightarrow BOX1F_{dName}) \land $ \\ 
 $ (E1NameInvF_{dNameInv} \leftrightarrow E1NameInvP_{dNameInv}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (PersonF_{John} \rightarrow  \lnot E2NameF_{John}) \land $ \\ 
 $ (E1NameInvF_{dName} \rightarrow BOX3F_{dName}) \land $ \\ 
 $ (PersonF_{dNameInv} \rightarrow  \lnot E2NameF_{dNameInv}) \land $ \\ 
 $ (E1NameF_{John} \leftrightarrow E1NameP_{John}) \land $ \\ 
 $ (BOX4F_{dNameInv} \leftrightarrow BOX19P_{dNameInv}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameF) \land $ \\ 
 $ (BOX15F_{John} \leftrightarrow BOX10P_{John}) \land $ \\ 
 $ (StringF_{John} \leftrightarrow StringP_{John}) \land $ \\ 
 $ (BOX3F_{John} \leftrightarrow BOX18P_{John}) \land $ \\ 
 $ (BOX16F_{N0} \leftrightarrow BOX11P_{N0}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (E1NameF_{dNameInv} \rightarrow BOX4F_{dNameInv}) \land $ \\ 
 $ (BOX17F_{N0} \leftrightarrow BOX12P_{N0}) \land $ \\ 
 $ (PersonF_{N0} \leftrightarrow PersonP_{N0}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameF) \land $ \\ 
 $ (E1NameInvF_{John} \rightarrow BOX3F_{John}) \land $ \\ 
 $ (E2NameF_{John} \rightarrow BOX0F_{John}) \land $ \\ 
 $ (BOX2F_{dNameInv} \leftrightarrow BOX9P_{dNameInv}) \land $ \\ 
 $ (E1NameF_{dName} \leftrightarrow E1NameP_{dName}) \land $ \\ 
 $ (BOX17F_{dNameInv} \leftrightarrow BOX12P_{dNameInv}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (BOX15F_{N0} \leftrightarrow BOX10P_{N0}) \land $ \\ 
 $ (E1NameInvF_{dNameInv} \rightarrow BOX1F_{dNameInv}) \land $ \\ 
 $ (BOX4F_{John} \leftrightarrow BOX19P_{John}) \land $ \\ 
 $ (StringF_{dName} \leftrightarrow StringP_{dName}) \land $ \\ 
 $ (PersonF_{N0} \rightarrow  \lnot E2NameF_{N0}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (BOX1F_{dNameInv} \leftrightarrow BOX7P_{dNameInv}) \land $ \\ 
 $ (BOX14F_{John} \leftrightarrow BOX8P_{John}) \land $ \\ 
 $ (StringF_{N0} \rightarrow  \lnot PersonF_{N0}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameF) \land $ \\ 
 $ (E2NameF_{dName} \leftrightarrow E2NameP_{dName}) \land $ \\ 
 $ (E1NameInvF_{dNameInv} \rightarrow BOX3F_{dNameInv}) \land $ \\ 
 $ (PersonF_{N0} \rightarrow E1NameF_{N0}) \land $ \\ 
 $ (E2NameF_{dNameInv} \leftrightarrow E2NameP_{dNameInv}) \land $ \\ 
 $ (E1NameF_{John} \rightarrow BOX2F_{John}) \land $ \\ 
 $ (BOX16F_{dNameInv} \leftrightarrow BOX11P_{dNameInv}) \land $ \\ 
 $ (E1NameF_{dNameInv} \leftrightarrow E1NameP_{dNameInv}) \land $ \\ 
 $ (BOX2F_{dName} \leftrightarrow BOX9P_{dName}) \land $ \\ 
 $ (E2NameF_{N0} \rightarrow E1NameF_{N0}) \land $ \\ 
 $ (E1NameF_{N0} \rightarrow BOX2F_{N0}) \land $ \\ 
 $ (E1NameF_{dName} \rightarrow BOX4F_{dName}) \land $ \\ 
 $ (BOX3F_{dName} \leftrightarrow BOX18P_{dName}) \land $ \\ 
 $ (PersonF_{dNameInv} \rightarrow E1NameF_{dNameInv}) \land $ \\ 
 $ (BOX14F_{dName} \leftrightarrow BOX8P_{dName}) \land $ \\ 
 $ (E1NameF_{N0} \leftrightarrow E1NameP_{N0}) \land $ \\ 
 $ (E2NameF_{dName} \rightarrow E1NameF_{dName}) \land $ \\ 
 $ (BOX14F_{N0} \leftrightarrow BOX8P_{N0}) \land $ \\ 
 $ (BOX15F_{dName} \leftrightarrow BOX10P_{dName}) \land $ \\ 
 $ (BOX0F_{dName} \leftrightarrow BOX5P_{dName}) \land $ \\ 
 $ (StringF_{dNameInv} \rightarrow  \lnot PersonF_{dNameInv}) \land $ \\ 
 $ (E1NameInvF_{dName} \rightarrow StringF_{dName}) \land $ \\ 
 $ (E1NameF_{dNameInv} \rightarrow BOX2F_{dNameInv}) \land $ \\ 
 $ (E2NameF_{John} \rightarrow E1NameF_{John}) \land $ \\ 
 $ (StringF_{N0} \leftrightarrow StringP_{N0}) \land $ \\ 
 $ (BOX13F_{John} \leftrightarrow BOX6P_{John}) \land $ \\ 
 $ (BOX14F_{dNameInv} \leftrightarrow BOX8P_{dNameInv}) \land $ \\ 
 $ (BOX1F_{dName} \leftrightarrow BOX7P_{dName}) \land $ \\ 
 $ (E1NameInvF_{John} \rightarrow BOX1F_{John}) \land $ \\ 
 $ (E1NameInvF_{N0} \leftrightarrow E1NameInvP_{N0}) \land $ \\ 
 $ (BOX0F_{N0} \leftrightarrow BOX5P_{N0}) \land $ \\ 
 $ (BOX16F_{John} \leftrightarrow BOX11P_{John}) \land $ \\ 
 $ (PersonF_{John} \rightarrow E1NameF_{John}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameP) \land $ \\ 
 $ (E2NameF_{John} \leftrightarrow E2NameP_{John}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (E1NameF_{dName} \rightarrow BOX2F_{dName}) \land $ \\ 
 $ (PersonF_{dName} \leftrightarrow PersonP_{dName}) \land $ \\ 
 $ (E1NameInvF_{N0} \rightarrow BOX3F_{N0}) \land $ \\ 
 $ (StringF_{John} \rightarrow  \lnot PersonF_{John}) \land $ \\ 
 $ (E1NameInvF_{dName} \leftrightarrow E1NameInvP_{dName}) \land $ \\ 
 $ (StringF_{dNameInv} \leftrightarrow StringP_{dNameInv}) \land $ \\ 
 $  \Rbox ((BOX1F_{John} \leftrightarrow  \Rbox BOX14F_{John}) \land $ \\ 
 $ ( \Rnext BOX3F_{John} \leftrightarrow ( \Rnext BOX16F_{John} \land $ \\ 
 $ BOX3F_{John})) \land $ \\ 
 $ ( \Rnext BOX12P_{John} \leftrightarrow ( \Rnext PNameP \land $ \\ 
 $ BOX12P_{John})) \land $ \\ 
 $ (BOX10P_{John} \leftrightarrow  \Rbox E1NameP_{John}) \land $ \\ 
 $ ( \Rnext BOX4F_{John} \leftrightarrow ( \Rnext BOX17F_{John} \land $ \\ 
 $ BOX4F_{John})) \land $ \\ 
 $ ( \Rnext BOX14F_{John} \leftrightarrow ( \Rnext E1NameInvF_{John} \land $ \\ 
 $ BOX14F_{John})) \land $ \\ 
 $ ( \Rnext BOX7P_{John} \leftrightarrow ( \Rnext BOX8P_{John} \land $ \\ 
 $ BOX7P_{John})) \land $ \\ 
 $ ( \Rnext BOX13F_{John} \leftrightarrow ( \Rnext E2NameF_{John} \land $ \\ 
 $ BOX13F_{John})) \land $ \\ 
 $ (BOX18P_{John} \leftrightarrow  \Rbox BOX11P_{John}) \land $ \\ 
 $ (BOX8P_{John} \leftrightarrow  \Rbox E1NameInvP_{John}) \land $ \\ 
 $ ( \Rnext BOX15F_{John} \leftrightarrow ( \Rnext E1NameF_{John} \land $ \\ 
 $ BOX15F_{John})) \land $ \\ 
 $ (BOX6P_{John} \leftrightarrow  \Rbox E2NameP_{John}) \land $ \\ 
 $ (BOX16F_{John} \leftrightarrow  \Rbox PinvNameF) \land $ \\ 
 $ ( \Rnext BOX9P_{John} \leftrightarrow ( \Rnext BOX10P_{John} \land $ \\ 
 $ BOX9P_{John})) \land $ \\ 
 $ (BOX19P_{John} \leftrightarrow  \Rbox BOX12P_{John}) \land $ \\ 
 $ ( \Rnext BOX11P_{John} \leftrightarrow ( \Rnext PinvNameP \land $ \\ 
 $ BOX11P_{John})) \land $ \\ 
 $ (BOX17F_{John} \leftrightarrow  \Rbox PNameF) \land $ \\ 
 $ (BOX2F_{John} \leftrightarrow  \Rbox BOX15F_{John}) \land $ \\ 
 $ ( \Rnext BOX5P_{John} \leftrightarrow ( \Rnext BOX6P_{John} \land $ \\ 
 $ BOX5P_{John})) \land $ \\ 
 $ (BOX0F_{John} \leftrightarrow  \Rbox BOX13F_{John})) \land $ \\ 
 $ (BOX2F_{John} \leftrightarrow BOX9P_{John}) \land $ \\ 
 $ (E2NameF_{dNameInv} \rightarrow BOX0F_{dNameInv}) \land $ \\ 
 $ (BOX4F_{dName} \leftrightarrow BOX19P_{dName}) \land $ \\ 
 $ (BOX0F_{John} \leftrightarrow BOX5P_{John}) \land $ \\ 
 $ (PinvNameF \leftrightarrow PinvNameF) \land $ \\ 
 $  \Rbox ((BOX1F_{dName} \leftrightarrow  \Rbox BOX14F_{dName}) \land $ \\ 
 $ ( \Rnext BOX3F_{dName} \leftrightarrow ( \Rnext BOX16F_{dName} \land $ \\ 
 $ BOX3F_{dName})) \land $ \\ 
 $ ( \Rnext BOX12P_{dName} \leftrightarrow ( \Rnext PNameP \land $ \\ 
 $ BOX12P_{dName})) \land $ \\ 
 $ (BOX10P_{dName} \leftrightarrow  \Rbox E1NameP_{dName}) \land $ \\ 
 $ ( \Rnext BOX4F_{dName} \leftrightarrow ( \Rnext BOX17F_{dName} \land $ \\ 
 $ BOX4F_{dName})) \land $ \\ 
 $ ( \Rnext BOX14F_{dName} \leftrightarrow ( \Rnext E1NameInvF_{dName} \land $ \\ 
 $ BOX14F_{dName})) \land $ \\ 
 $ ( \Rnext BOX7P_{dName} \leftrightarrow ( \Rnext BOX8P_{dName} \land $ \\ 
 $ BOX7P_{dName})) \land $ \\ 
 $ ( \Rnext BOX13F_{dName} \leftrightarrow ( \Rnext E2NameF_{dName} \land $ \\ 
 $ BOX13F_{dName})) \land $ \\ 
 $ (BOX18P_{dName} \leftrightarrow  \Rbox BOX11P_{dName}) \land $ \\ 
 $ (BOX8P_{dName} \leftrightarrow  \Rbox E1NameInvP_{dName}) \land $ \\ 
 $ ( \Rnext BOX15F_{dName} \leftrightarrow ( \Rnext E1NameF_{dName} \land $ \\ 
 $ BOX15F_{dName})) \land $ \\ 
 $ (BOX6P_{dName} \leftrightarrow  \Rbox E2NameP_{dName}) \land $ \\ 
 $ (BOX16F_{dName} \leftrightarrow  \Rbox PinvNameF) \land $ \\ 
 $ ( \Rnext BOX9P_{dName} \leftrightarrow ( \Rnext BOX10P_{dName} \land $ \\ 
 $ BOX9P_{dName})) \land $ \\ 
 $ (BOX19P_{dName} \leftrightarrow  \Rbox BOX12P_{dName}) \land $ \\ 
 $ ( \Rnext BOX11P_{dName} \leftrightarrow ( \Rnext PinvNameP \land $ \\ 
 $ BOX11P_{dName})) \land $ \\ 
 $ (BOX17F_{dName} \leftrightarrow  \Rbox PNameF) \land $ \\ 
 $ (BOX2F_{dName} \leftrightarrow  \Rbox BOX15F_{dName}) \land $ \\ 
 $ ( \Rnext BOX5P_{dName} \leftrightarrow ( \Rnext BOX6P_{dName} \land $ \\ 
 $ BOX5P_{dName})) \land $ \\ 
 $ (BOX0F_{dName} \leftrightarrow  \Rbox BOX13F_{dName})) \land $ \\ 
 $ (PersonF_{dName} \rightarrow E1NameF_{dName}) \land $ \\ 
 $  \Rbox ((BOX1F_{N0} \leftrightarrow  \Rbox BOX14F_{N0}) \land $ \\ 
 $ ( \Rnext BOX3F_{N0} \leftrightarrow ( \Rnext BOX16F_{N0} \land $ \\ 
 $ BOX3F_{N0})) \land $ \\ 
 $ ( \Rnext BOX12P_{N0} \leftrightarrow ( \Rnext PNameP \land $ \\ 
 $ BOX12P_{N0})) \land $ \\ 
 $ (BOX10P_{N0} \leftrightarrow  \Rbox E1NameP_{N0}) \land $ \\ 
 $ ( \Rnext BOX4F_{N0} \leftrightarrow ( \Rnext BOX17F_{N0} \land $ \\ 
 $ BOX4F_{N0})) \land $ \\ 
 $ ( \Rnext BOX14F_{N0} \leftrightarrow ( \Rnext E1NameInvF_{N0} \land $ \\ 
 $ BOX14F_{N0})) \land $ \\ 
 $ ( \Rnext BOX7P_{N0} \leftrightarrow ( \Rnext BOX8P_{N0} \land $ \\ 
 $ BOX7P_{N0})) \land $ \\ 
 $ ( \Rnext BOX13F_{N0} \leftrightarrow ( \Rnext E2NameF_{N0} \land $ \\ 
 $ BOX13F_{N0})) \land $ \\ 
 $ (BOX18P_{N0} \leftrightarrow  \Rbox BOX11P_{N0}) \land $ \\ 
 $ (BOX8P_{N0} \leftrightarrow  \Rbox E1NameInvP_{N0}) \land $ \\ 
 $ ( \Rnext BOX15F_{N0} \leftrightarrow ( \Rnext E1NameF_{N0} \land $ \\ 
 $ BOX15F_{N0})) \land $ \\ 
 $ (BOX6P_{N0} \leftrightarrow  \Rbox E2NameP_{N0}) \land $ \\ 
 $ (BOX16F_{N0} \leftrightarrow  \Rbox PinvNameF) \land $ \\ 
 $ ( \Rnext BOX9P_{N0} \leftrightarrow ( \Rnext BOX10P_{N0} \land $ \\ 
 $ BOX9P_{N0})) \land $ \\ 
 $ (BOX19P_{N0} \leftrightarrow  \Rbox BOX12P_{N0}) \land $ \\ 
 $ ( \Rnext BOX11P_{N0} \leftrightarrow ( \Rnext PinvNameP \land $ \\ 
 $ BOX11P_{N0})) \land $ \\ 
 $ (BOX17F_{N0} \leftrightarrow  \Rbox PNameF) \land $ \\ 
 $ (BOX2F_{N0} \leftrightarrow  \Rbox BOX15F_{N0}) \land $ \\ 
 $ ( \Rnext BOX5P_{N0} \leftrightarrow ( \Rnext BOX6P_{N0} \land $ \\ 
 $ BOX5P_{N0})) \land $ \\ 
 $ (BOX0F_{N0} \leftrightarrow  \Rbox BOX13F_{N0})) \land $ \\ 
 $ (E2NameF_{dName} \rightarrow BOX0F_{dName}) \land $ \\ 
 $ (BOX0F_{dNameInv} \leftrightarrow BOX5P_{dNameInv}) \land $ \\ 
 $ (E2NameF_{N0} \leftrightarrow E2NameP_{N0}) \land $ \\ 
 $ (PersonF_{John} \leftrightarrow PersonP_{John}) \land $ \\ 
 $ (BOX13F_{dNameInv} \leftrightarrow BOX6P_{dNameInv}) \land $ \\ 
 $ (BOX17F_{John} \leftrightarrow BOX12P_{John}) \land $ \\ 
 $ (E1NameInvF_{N0} \rightarrow BOX1F_{N0}) \land $ \\ 
 $ (E2NameF_{dNameInv} \rightarrow E1NameF_{dNameInv}) \land $ \\ 
 $ (BOX1F_{N0} \leftrightarrow BOX7P_{N0}) \land $ \\ 
 $ (E1NameInvF_{John} \rightarrow StringF_{John}) \land $ \\ 
 $ (E1NameF_{N0} \rightarrow BOX4F_{N0}) \land $ \\ 
 $ (PNameF \leftrightarrow PNameF) \land $ \\ 
 $ (PNameF \leftrightarrow PNameP) \land $ \\ 
 $ (BOX3F_{N0} \leftrightarrow BOX18P_{N0}) \land $ \\ 
 $ (E1NameInvF_{John} \leftrightarrow E1NameInvP_{John}) \land $ \\ 
 $ (BOX15F_{dNameInv} \leftrightarrow BOX10P_{dNameInv}) \land $ \\ 
 $ (BOX4F_{N0} \leftrightarrow BOX19P_{N0}) \land $ \\ 
 $ (BOX13F_{dName} \leftrightarrow BOX6P_{dName}) \land $ \\ 
 $ (BOX17F_{dName} \leftrightarrow BOX12P_{dName}) \land $ \\ 
 $ (BOX16F_{dName} \leftrightarrow BOX11P_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv})) \land $ \\ 
 $ PersonF_{John} \land $ \\ 
 $ E1NameF_{John} \land $ \\ 
 $ E1NameInvF_{N0})$ 
\end{document}