\begin{frame}[t]{Translating into Predicate Logic}
  \vspace{-3ex}
  \begin{talign}
  \mpause[1]{\sentence{Marie and Jan are clever}} & & &
  \mpause{\formula{\logand{\unpred{C}{\const{m}}}{\unpred{C}{\const{j}}}}}
  \\  
  \mpause{\sentence{Not everybody is clever}} & & &
  \mpause{\formula{\lognot{\forallst{x}{\,\unpred{C}{x}}}}}
  \\
  \mpause{\sentence{Somebody has learned logic}} & & &
  \mpause{\formula{\existsst{x}{\,\unpred{LL}{x}}}}
  \\
  \parbox{0.51\textwidth}{\mpause{\forestgreen{Not everybody has learned logic,\\\hspace*{\fill} but Marie and Jan have}}} & & &
  \mpause{\formula{\logand{\lognot{\forallst{x}{\,\unpred{LL}{x}}}}
                          {\logand{\unpred{LL}{\const{m}}}{\unpred{LL}{\const{j}}}}}}
  \end{talign}
  
  \begin{block}{Specification and model used}
    \begin{malign}
      \formula{\unpred{C}{x}} & \funin \sentence{$\black{x}$ is clever}
      & \const{m} & \funin \sentence{Marie}
      \\
      \formula{\unpred{LL}{x}} & \funin \sentence{$\black{x}$ has learned logic}
      & \const{j} & \funin \sentence{Jan}     
    \end{malign}
    \smallskip

    So we use the following model $\model{\amodel}\,$:  
    \begin{itemize}\vspace*{0.25ex}\setlength{\itemsep}{0.25ex}
      \item
        domain $\model{\adomain} = \text{the set of all humans}$
      \item
        $\intin{\sunpred{C}}{\model{\amodel}} = \descsetexp{x\in\model{\adomain}}{\sentence{\black{$x$} is clever}}$
      \item
        $\intin{\sunpred{LL}}{\model{\amodel}} = \descsetexp{x\in\model{\adomain}}{\sentence{\black{$x$} has learned logic}}$    
      \item
        $\intin{\sunpred{j}}{\model{\amodel}} = \sentence{Jan}$, and
        $\intin{\sunpred{m}}{\model{\amodel}} = \sentence{Marie}$.  
    \end{itemize}
  \end{block}
\end{frame}