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


$((PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1NameInv_{N14} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N6} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox ((Person_{N8} \rightarrow E1Name_{N8}) \land $ \\ 
 $ (Person_{N8} \rightarrow  \lnot E2Name_{N8}) \land $ \\ 
 $ (E2Name_{N8} \rightarrow E1Name_{N8}) \land $ \\ 
 $ (E1Name_{N8} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N8}) \land $ \\ 
 $ (E2Name_{N8} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N8})) \land $ \\ 
 $  \SVbox ((Person_{John} \rightarrow E1Name_{John}) \land $ \\ 
 $ (Person_{John} \rightarrow  \lnot E2Name_{John}) \land $ \\ 
 $ (E2Name_{John} \rightarrow E1Name_{John}) \land $ \\ 
 $ (E1Name_{John} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{John}) \land $ \\ 
 $ (E2Name_{John} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{John})) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1Name_{dName} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N16} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N30} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N37} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox ((Person_{N17} \rightarrow E1Name_{N17}) \land $ \\ 
 $ (Person_{N17} \rightarrow  \lnot E2Name_{N17}) \land $ \\ 
 $ (E2Name_{N17} \rightarrow E1Name_{N17}) \land $ \\ 
 $ (E1Name_{N17} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N17}) \land $ \\ 
 $ (E2Name_{N17} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N17})) \land $ \\ 
 $  \SVbox (E1Name_{N17} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox ((Person_{N49} \rightarrow E1Name_{N49}) \land $ \\ 
 $ (Person_{N49} \rightarrow  \lnot E2Name_{N49}) \land $ \\ 
 $ (E2Name_{N49} \rightarrow E1Name_{N49}) \land $ \\ 
 $ (E1Name_{N49} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N49}) \land $ \\ 
 $ (E2Name_{N49} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N49})) \land $ \\ 
 $  \SVbox ((Person_{N18} \rightarrow E1Name_{N18}) \land $ \\ 
 $ (Person_{N18} \rightarrow  \lnot E2Name_{N18}) \land $ \\ 
 $ (E2Name_{N18} \rightarrow E1Name_{N18}) \land $ \\ 
 $ (E1Name_{N18} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N18}) \land $ \\ 
 $ (E2Name_{N18} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N18})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N12} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox ((Person_{N12} \rightarrow E1Name_{N12}) \land $ \\ 
 $ (Person_{N12} \rightarrow  \lnot E2Name_{N12}) \land $ \\ 
 $ (E2Name_{N12} \rightarrow E1Name_{N12}) \land $ \\ 
 $ (E1Name_{N12} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N12}) \land $ \\ 
 $ (E2Name_{N12} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N12})) \land $ \\ 
 $  \SVbox (E1NameInv_{John} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1NameInv_{N29} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1NameInv_{dName} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N32} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox ((Person_{N41} \rightarrow E1Name_{N41}) \land $ \\ 
 $ (Person_{N41} \rightarrow  \lnot E2Name_{N41}) \land $ \\ 
 $ (E2Name_{N41} \rightarrow E1Name_{N41}) \land $ \\ 
 $ (E1Name_{N41} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N41}) \land $ \\ 
 $ (E2Name_{N41} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N41})) \land $ \\ 
 $  \SVbox (E1Name_{N48} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1Name_{N33} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{N32} \rightarrow E1Name_{N32}) \land $ \\ 
 $ (Person_{N32} \rightarrow  \lnot E2Name_{N32}) \land $ \\ 
 $ (E2Name_{N32} \rightarrow E1Name_{N32}) \land $ \\ 
 $ (E1Name_{N32} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N32}) \land $ \\ 
 $ (E2Name_{N32} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N32})) \land $ \\ 
 $  \SVbox (E1NameInv_{N8} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1NameInv_{N49} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox ((Person_{N24} \rightarrow E1Name_{N24}) \land $ \\ 
 $ (Person_{N24} \rightarrow  \lnot E2Name_{N24}) \land $ \\ 
 $ (E2Name_{N24} \rightarrow E1Name_{N24}) \land $ \\ 
 $ (E1Name_{N24} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N24}) \land $ \\ 
 $ (E2Name_{N24} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N24})) \land $ \\ 
 $  \SVbox ((Person_{N10} \rightarrow E1Name_{N10}) \land $ \\ 
 $ (Person_{N10} \rightarrow  \lnot E2Name_{N10}) \land $ \\ 
 $ (E2Name_{N10} \rightarrow E1Name_{N10}) \land $ \\ 
 $ (E1Name_{N10} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N10}) \land $ \\ 
 $ (E2Name_{N10} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N10})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1Name_{N8} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N38} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N5} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N48} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1Name_{N47} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox ((Person_{N19} \rightarrow E1Name_{N19}) \land $ \\ 
 $ (Person_{N19} \rightarrow  \lnot E2Name_{N19}) \land $ \\ 
 $ (E2Name_{N19} \rightarrow E1Name_{N19}) \land $ \\ 
 $ (E1Name_{N19} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N19}) \land $ \\ 
 $ (E2Name_{N19} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N19})) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1NameInv_{N41} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1NameInv_{N21} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N1} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N11} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1Name_{N24} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N26} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox ((Person_{N11} \rightarrow E1Name_{N11}) \land $ \\ 
 $ (Person_{N11} \rightarrow  \lnot E2Name_{N11}) \land $ \\ 
 $ (E2Name_{N11} \rightarrow E1Name_{N11}) \land $ \\ 
 $ (E1Name_{N11} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N11}) \land $ \\ 
 $ (E2Name_{N11} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N11})) \land $ \\ 
 $  \SVbox (E1NameInv_{N13} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N47} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox ((Person_{N4} \rightarrow E1Name_{N4}) \land $ \\ 
 $ (Person_{N4} \rightarrow  \lnot E2Name_{N4}) \land $ \\ 
 $ (E2Name_{N4} \rightarrow E1Name_{N4}) \land $ \\ 
 $ (E1Name_{N4} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N4}) \land $ \\ 
 $ (E2Name_{N4} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N4})) \land $ \\ 
 $  \SVbox (E1NameInv_{N34} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N28} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{N44} \rightarrow E1Name_{N44}) \land $ \\ 
 $ (Person_{N44} \rightarrow  \lnot E2Name_{N44}) \land $ \\ 
 $ (E2Name_{N44} \rightarrow E1Name_{N44}) \land $ \\ 
 $ (E1Name_{N44} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N44}) \land $ \\ 
 $ (E2Name_{N44} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N44})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1Name_{dNameInv} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1Name_{N49} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox ((Person_{N0} \rightarrow E1Name_{N0}) \land $ \\ 
 $ (Person_{N0} \rightarrow  \lnot E2Name_{N0}) \land $ \\ 
 $ (E2Name_{N0} \rightarrow E1Name_{N0}) \land $ \\ 
 $ (E1Name_{N0} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N0}) \land $ \\ 
 $ (E2Name_{N0} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N0})) \land $ \\ 
 $  \SVbox (E1Name_{N16} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{N36} \rightarrow E1Name_{N36}) \land $ \\ 
 $ (Person_{N36} \rightarrow  \lnot E2Name_{N36}) \land $ \\ 
 $ (E2Name_{N36} \rightarrow E1Name_{N36}) \land $ \\ 
 $ (E1Name_{N36} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N36}) \land $ \\ 
 $ (E2Name_{N36} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N36})) \land $ \\ 
 $  \SVbox (E1NameInv_{N42} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N23} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox ((Person_{N9} \rightarrow E1Name_{N9}) \land $ \\ 
 $ (Person_{N9} \rightarrow  \lnot E2Name_{N9}) \land $ \\ 
 $ (E2Name_{N9} \rightarrow E1Name_{N9}) \land $ \\ 
 $ (E1Name_{N9} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N9}) \land $ \\ 
 $ (E2Name_{N9} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N9})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1Name_{N19} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N3} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1Name_{N12} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox ((Person_{N30} \rightarrow E1Name_{N30}) \land $ \\ 
 $ (Person_{N30} \rightarrow  \lnot E2Name_{N30}) \land $ \\ 
 $ (E2Name_{N30} \rightarrow E1Name_{N30}) \land $ \\ 
 $ (E1Name_{N30} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N30}) \land $ \\ 
 $ (E2Name_{N30} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N30})) \land $ \\ 
 $  \SVbox ((Person_{N27} \rightarrow E1Name_{N27}) \land $ \\ 
 $ (Person_{N27} \rightarrow  \lnot E2Name_{N27}) \land $ \\ 
 $ (E2Name_{N27} \rightarrow E1Name_{N27}) \land $ \\ 
 $ (E1Name_{N27} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N27}) \land $ \\ 
 $ (E2Name_{N27} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N27})) \land $ \\ 
 $  \SVbox (E1Name_{N44} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1Name_{N27} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{N21} \rightarrow E1Name_{N21}) \land $ \\ 
 $ (Person_{N21} \rightarrow  \lnot E2Name_{N21}) \land $ \\ 
 $ (E2Name_{N21} \rightarrow E1Name_{N21}) \land $ \\ 
 $ (E1Name_{N21} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N21}) \land $ \\ 
 $ (E2Name_{N21} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N21})) \land $ \\ 
 $  \SVbox (E1NameInv_{N45} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1Name_{N37} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox ((Person_{N48} \rightarrow E1Name_{N48}) \land $ \\ 
 $ (Person_{N48} \rightarrow  \lnot E2Name_{N48}) \land $ \\ 
 $ (E2Name_{N48} \rightarrow E1Name_{N48}) \land $ \\ 
 $ (E1Name_{N48} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N48}) \land $ \\ 
 $ (E2Name_{N48} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N48})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N24} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1Name_{N23} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox ((Person_{N6} \rightarrow E1Name_{N6}) \land $ \\ 
 $ (Person_{N6} \rightarrow  \lnot E2Name_{N6}) \land $ \\ 
 $ (E2Name_{N6} \rightarrow E1Name_{N6}) \land $ \\ 
 $ (E1Name_{N6} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N6}) \land $ \\ 
 $ (E2Name_{N6} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N6})) \land $ \\ 
 $  \SVbox (E1Name_{N43} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N35} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N43} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox ((Person_{N20} \rightarrow E1Name_{N20}) \land $ \\ 
 $ (Person_{N20} \rightarrow  \lnot E2Name_{N20}) \land $ \\ 
 $ (E2Name_{N20} \rightarrow E1Name_{N20}) \land $ \\ 
 $ (E1Name_{N20} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N20}) \land $ \\ 
 $ (E2Name_{N20} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N20})) \land $ \\ 
 $  \SVbox (E1Name_{N4} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{dNameInv} \rightarrow E1Name_{dNameInv}) \land $ \\ 
 $ (Person_{dNameInv} \rightarrow  \lnot E2Name_{dNameInv}) \land $ \\ 
 $ (E2Name_{dNameInv} \rightarrow E1Name_{dNameInv}) \land $ \\ 
 $ (E1Name_{dNameInv} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{dNameInv}) \land $ \\ 
 $ (E2Name_{dNameInv} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{dNameInv})) \land $ \\ 
 $  \SVbox ((Person_{N35} \rightarrow E1Name_{N35}) \land $ \\ 
 $ (Person_{N35} \rightarrow  \lnot E2Name_{N35}) \land $ \\ 
 $ (E2Name_{N35} \rightarrow E1Name_{N35}) \land $ \\ 
 $ (E1Name_{N35} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N35}) \land $ \\ 
 $ (E2Name_{N35} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N35})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox ((Person_{N39} \rightarrow E1Name_{N39}) \land $ \\ 
 $ (Person_{N39} \rightarrow  \lnot E2Name_{N39}) \land $ \\ 
 $ (E2Name_{N39} \rightarrow E1Name_{N39}) \land $ \\ 
 $ (E1Name_{N39} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N39}) \land $ \\ 
 $ (E2Name_{N39} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N39})) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1Name_{N9} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{N28} \rightarrow E1Name_{N28}) \land $ \\ 
 $ (Person_{N28} \rightarrow  \lnot E2Name_{N28}) \land $ \\ 
 $ (E2Name_{N28} \rightarrow E1Name_{N28}) \land $ \\ 
 $ (E1Name_{N28} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N28}) \land $ \\ 
 $ (E2Name_{N28} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N28})) \land $ \\ 
 $  \SVbox ((Person_{N38} \rightarrow E1Name_{N38}) \land $ \\ 
 $ (Person_{N38} \rightarrow  \lnot E2Name_{N38}) \land $ \\ 
 $ (E2Name_{N38} \rightarrow E1Name_{N38}) \land $ \\ 
 $ (E1Name_{N38} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N38}) \land $ \\ 
 $ (E2Name_{N38} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N38})) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1NameInv_{N2} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox ((Person_{N3} \rightarrow E1Name_{N3}) \land $ \\ 
 $ (Person_{N3} \rightarrow  \lnot E2Name_{N3}) \land $ \\ 
 $ (E2Name_{N3} \rightarrow E1Name_{N3}) \land $ \\ 
 $ (E1Name_{N3} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N3}) \land $ \\ 
 $ (E2Name_{N3} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N3})) \land $ \\ 
 $  \SVbox (E1NameInv_{N40} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1NameInv_{N17} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox ((Person_{N37} \rightarrow E1Name_{N37}) \land $ \\ 
 $ (Person_{N37} \rightarrow  \lnot E2Name_{N37}) \land $ \\ 
 $ (E2Name_{N37} \rightarrow E1Name_{N37}) \land $ \\ 
 $ (E1Name_{N37} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N37}) \land $ \\ 
 $ (E2Name_{N37} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N37})) \land $ \\ 
 $  \SVbox ((Person_{N47} \rightarrow E1Name_{N47}) \land $ \\ 
 $ (Person_{N47} \rightarrow  \lnot E2Name_{N47}) \land $ \\ 
 $ (E2Name_{N47} \rightarrow E1Name_{N47}) \land $ \\ 
 $ (E1Name_{N47} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N47}) \land $ \\ 
 $ (E2Name_{N47} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N47})) \land $ \\ 
 $  \SVbox (E1NameInv_{N19} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox ((Person_{N7} \rightarrow E1Name_{N7}) \land $ \\ 
 $ (Person_{N7} \rightarrow  \lnot E2Name_{N7}) \land $ \\ 
 $ (E2Name_{N7} \rightarrow E1Name_{N7}) \land $ \\ 
 $ (E1Name_{N7} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N7}) \land $ \\ 
 $ (E2Name_{N7} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N7})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N0} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1NameInv_{N30} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox ((Person_{N29} \rightarrow E1Name_{N29}) \land $ \\ 
 $ (Person_{N29} \rightarrow  \lnot E2Name_{N29}) \land $ \\ 
 $ (E2Name_{N29} \rightarrow E1Name_{N29}) \land $ \\ 
 $ (E1Name_{N29} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N29}) \land $ \\ 
 $ (E2Name_{N29} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N29})) \land $ \\ 
 $  \SVbox (E1NameInv_{N44} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N25} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1Name_{N3} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N10} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N2} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1Name_{N38} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1Name_{N22} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1Name_{N35} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1Name_{N11} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{N22} \rightarrow E1Name_{N22}) \land $ \\ 
 $ (Person_{N22} \rightarrow  \lnot E2Name_{N22}) \land $ \\ 
 $ (E2Name_{N22} \rightarrow E1Name_{N22}) \land $ \\ 
 $ (E1Name_{N22} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N22}) \land $ \\ 
 $ (E2Name_{N22} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N22})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N36} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N26} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1Name_{John} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1Name_{N42} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N18} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox ((Person_{N2} \rightarrow E1Name_{N2}) \land $ \\ 
 $ (Person_{N2} \rightarrow  \lnot E2Name_{N2}) \land $ \\ 
 $ (E2Name_{N2} \rightarrow E1Name_{N2}) \land $ \\ 
 $ (E1Name_{N2} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N2}) \land $ \\ 
 $ (E2Name_{N2} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N2})) \land $ \\ 
 $  \SVbox (E1Name_{N39} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{N14} \rightarrow E1Name_{N14}) \land $ \\ 
 $ (Person_{N14} \rightarrow  \lnot E2Name_{N14}) \land $ \\ 
 $ (E2Name_{N14} \rightarrow E1Name_{N14}) \land $ \\ 
 $ (E1Name_{N14} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N14}) \land $ \\ 
 $ (E2Name_{N14} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N14})) \land $ \\ 
 $  \SVbox (E1Name_{N34} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{dNameInv} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N7} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1Name_{N29} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N28} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N40} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N22} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox ((Person_{N43} \rightarrow E1Name_{N43}) \land $ \\ 
 $ (Person_{N43} \rightarrow  \lnot E2Name_{N43}) \land $ \\ 
 $ (E2Name_{N43} \rightarrow E1Name_{N43}) \land $ \\ 
 $ (E1Name_{N43} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N43}) \land $ \\ 
 $ (E2Name_{N43} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N43})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox ((Person_{N5} \rightarrow E1Name_{N5}) \land $ \\ 
 $ (Person_{N5} \rightarrow  \lnot E2Name_{N5}) \land $ \\ 
 $ (E2Name_{N5} \rightarrow E1Name_{N5}) \land $ \\ 
 $ (E1Name_{N5} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N5}) \land $ \\ 
 $ (E2Name_{N5} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N5})) \land $ \\ 
 $  \SVbox (E1NameInv_{N5} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N1} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N41} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox ((Person_{N31} \rightarrow E1Name_{N31}) \land $ \\ 
 $ (Person_{N31} \rightarrow  \lnot E2Name_{N31}) \land $ \\ 
 $ (E2Name_{N31} \rightarrow E1Name_{N31}) \land $ \\ 
 $ (E1Name_{N31} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N31}) \land $ \\ 
 $ (E2Name_{N31} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N31})) \land $ \\ 
 $  \SVbox (E1NameInv_{N15} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N36} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{N23} \rightarrow E1Name_{N23}) \land $ \\ 
 $ (Person_{N23} \rightarrow  \lnot E2Name_{N23}) \land $ \\ 
 $ (E2Name_{N23} \rightarrow E1Name_{N23}) \land $ \\ 
 $ (E1Name_{N23} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N23}) \land $ \\ 
 $ (E2Name_{N23} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N23})) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1NameInv_{N25} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N45} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox ((Person_{N40} \rightarrow E1Name_{N40}) \land $ \\ 
 $ (Person_{N40} \rightarrow  \lnot E2Name_{N40}) \land $ \\ 
 $ (E2Name_{N40} \rightarrow E1Name_{N40}) \land $ \\ 
 $ (E1Name_{N40} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N40}) \land $ \\ 
 $ (E2Name_{N40} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N40})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1NameInv_{N20} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N32} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{N33} \rightarrow E1Name_{N33}) \land $ \\ 
 $ (Person_{N33} \rightarrow  \lnot E2Name_{N33}) \land $ \\ 
 $ (E2Name_{N33} \rightarrow E1Name_{N33}) \land $ \\ 
 $ (E1Name_{N33} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N33}) \land $ \\ 
 $ (E2Name_{N33} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N33})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox ((Person_{N16} \rightarrow E1Name_{N16}) \land $ \\ 
 $ (Person_{N16} \rightarrow  \lnot E2Name_{N16}) \land $ \\ 
 $ (E2Name_{N16} \rightarrow E1Name_{N16}) \land $ \\ 
 $ (E1Name_{N16} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N16}) \land $ \\ 
 $ (E2Name_{N16} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N16})) \land $ \\ 
 $  \SVbox (E1Name_{N6} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{N15} \rightarrow E1Name_{N15}) \land $ \\ 
 $ (Person_{N15} \rightarrow  \lnot E2Name_{N15}) \land $ \\ 
 $ (E2Name_{N15} \rightarrow E1Name_{N15}) \land $ \\ 
 $ (E1Name_{N15} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N15}) \land $ \\ 
 $ (E2Name_{N15} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N15})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox ((Person_{N46} \rightarrow E1Name_{N46}) \land $ \\ 
 $ (Person_{N46} \rightarrow  \lnot E2Name_{N46}) \land $ \\ 
 $ (E2Name_{N46} \rightarrow E1Name_{N46}) \land $ \\ 
 $ (E1Name_{N46} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N46}) \land $ \\ 
 $ (E2Name_{N46} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N46})) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N27} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox ((Person_{N45} \rightarrow E1Name_{N45}) \land $ \\ 
 $ (Person_{N45} \rightarrow  \lnot E2Name_{N45}) \land $ \\ 
 $ (E2Name_{N45} \rightarrow E1Name_{N45}) \land $ \\ 
 $ (E1Name_{N45} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N45}) \land $ \\ 
 $ (E2Name_{N45} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N45})) \land $ \\ 
 $  \SVbox (E1Name_{N13} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1Name_{N10} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1Name_{N15} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{N1} \rightarrow E1Name_{N1}) \land $ \\ 
 $ (Person_{N1} \rightarrow  \lnot E2Name_{N1}) \land $ \\ 
 $ (E2Name_{N1} \rightarrow E1Name_{N1}) \land $ \\ 
 $ (E1Name_{N1} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N1}) \land $ \\ 
 $ (E2Name_{N1} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N1})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N46} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox ((Person_{N25} \rightarrow E1Name_{N25}) \land $ \\ 
 $ (Person_{N25} \rightarrow  \lnot E2Name_{N25}) \land $ \\ 
 $ (E2Name_{N25} \rightarrow E1Name_{N25}) \land $ \\ 
 $ (E1Name_{N25} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N25}) \land $ \\ 
 $ (E2Name_{N25} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N25})) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1Name_{N20} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N7} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1Name_{N0} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{dName} \rightarrow E1Name_{dName}) \land $ \\ 
 $ (Person_{dName} \rightarrow  \lnot E2Name_{dName}) \land $ \\ 
 $ (E2Name_{dName} \rightarrow E1Name_{dName}) \land $ \\ 
 $ (E1Name_{dName} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{dName}) \land $ \\ 
 $ (E2Name_{dName} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{dName})) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1Name_{N21} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox ((Person_{N26} \rightarrow E1Name_{N26}) \land $ \\ 
 $ (Person_{N26} \rightarrow  \lnot E2Name_{N26}) \land $ \\ 
 $ (E2Name_{N26} \rightarrow E1Name_{N26}) \land $ \\ 
 $ (E1Name_{N26} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N26}) \land $ \\ 
 $ (E2Name_{N26} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N26})) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox ((Person_{N34} \rightarrow E1Name_{N34}) \land $ \\ 
 $ (Person_{N34} \rightarrow  \lnot E2Name_{N34}) \land $ \\ 
 $ (E2Name_{N34} \rightarrow E1Name_{N34}) \land $ \\ 
 $ (E1Name_{N34} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N34}) \land $ \\ 
 $ (E2Name_{N34} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N34})) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox ((Person_{N42} \rightarrow E1Name_{N42}) \land $ \\ 
 $ (Person_{N42} \rightarrow  \lnot E2Name_{N42}) \land $ \\ 
 $ (E2Name_{N42} \rightarrow E1Name_{N42}) \land $ \\ 
 $ (E1Name_{N42} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N42}) \land $ \\ 
 $ (E2Name_{N42} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N42})) \land $ \\ 
 $  \SVbox (E1NameInv_{N31} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1Name_{N31} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1NameInv_{N39} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1NameInv_{N33} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox ((Person_{N13} \rightarrow E1Name_{N13}) \land $ \\ 
 $ (Person_{N13} \rightarrow  \lnot E2Name_{N13}) \land $ \\ 
 $ (E2Name_{N13} \rightarrow E1Name_{N13}) \land $ \\ 
 $ (E1Name_{N13} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E1Name_{N13}) \land $ \\ 
 $ (E2Name_{N13} \rightarrow  \Rnext  \Rbox  \Lnext  \Lbox E2Name_{N13})) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1Name_{N18} \rightarrow  \SVbox PName) \land $ \\ 
 $  \SVbox (E1Name_{N46} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PinvName \rightarrow E1Name_{dName}) \land $ \\ 
 $  \SVbox (E1NameInv_{N4} \rightarrow  \SVbox PinvName) \land $ \\ 
 $  \SVbox (E1Name_{N14} \rightarrow  \SVbox PName) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $ (PName \rightarrow E1NameInv_{dNameInv}) \land $ \\ 
 $  \SVbox (E1NameInv_{N9} \rightarrow  \SVbox PinvName) \land $ \\ 
 $ Person_{John} \land $ \\ 
 $ E2Name_{John} \land $ \\ 
 $ E1NameInv_{N21} \land $ \\ 
 $ E1NameInv_{N7} \land $ \\ 
 $ E1NameInv_{N45} \land $ \\ 
 $ E1NameInv_{N22} \land $ \\ 
 $ E1NameInv_{N13} \land $ \\ 
 $ E1NameInv_{N2} \land $ \\ 
 $ E1NameInv_{N43} \land $ \\ 
 $ E1NameInv_{N48} \land $ \\ 
 $ E1NameInv_{N29} \land $ \\ 
 $ E1NameInv_{N15} \land $ \\ 
 $ E1NameInv_{N32} \land $ \\ 
 $ E1NameInv_{N47} \land $ \\ 
 $ E1NameInv_{N20} \land $ \\ 
 $ E1NameInv_{N28} \land $ \\ 
 $ E1NameInv_{N49} \land $ \\ 
 $ E1NameInv_{N12} \land $ \\ 
 $ E1NameInv_{N4} \land $ \\ 
 $ E1NameInv_{N34} \land $ \\ 
 $ E1NameInv_{N33} \land $ \\ 
 $ E1NameInv_{N37} \land $ \\ 
 $ E1NameInv_{N41} \land $ \\ 
 $ E1NameInv_{N39} \land $ \\ 
 $ E1NameInv_{N26} \land $ \\ 
 $ E1NameInv_{N44} \land $ \\ 
 $ E1NameInv_{N1} \land $ \\ 
 $ E1NameInv_{N46} \land $ \\ 
 $ E1NameInv_{N35} \land $ \\ 
 $ E1NameInv_{N6} \land $ \\ 
 $ E1NameInv_{N36} \land $ \\ 
 $ E1NameInv_{N25} \land $ \\ 
 $ E1NameInv_{N40} \land $ \\ 
 $ E1NameInv_{N16} \land $ \\ 
 $ E1NameInv_{N42} \land $ \\ 
 $ E1NameInv_{N8} \land $ \\ 
 $ E1NameInv_{N3} \land $ \\ 
 $ E1NameInv_{N24} \land $ \\ 
 $ E1NameInv_{N30} \land $ \\ 
 $ E1NameInv_{N0} \land $ \\ 
 $ E1NameInv_{N31} \land $ \\ 
 $ E1NameInv_{N27} \land $ \\ 
 $ E1NameInv_{N9} \land $ \\ 
 $ E1NameInv_{N17} \land $ \\ 
 $ E1NameInv_{N18} \land $ \\ 
 $ E1NameInv_{N10} \land $ \\ 
 $ E1NameInv_{N5} \land $ \\ 
 $ E1NameInv_{N19} \land $ \\ 
 $ E1NameInv_{N11} \land $ \\ 
 $ E1NameInv_{N23} \land $ \\ 
 $ E1NameInv_{N14} \land $ \\ 
 $ E1NameInv_{N38})$ 
\end{document}