\begin{frame}[t]{\alt<-5>{Satisfiable Formula (Example)}{Consistent Set of Formulas (Example)}}
  \exampleloverlover
  \pause\bigskip
  
  The formula $\aform$ is \emph{satisfiable}:
  \pause
  \begin{exampleblock}{}
    Consider model $\model{\amodeli{1}}$ with domain $\model{\adomaini{1}} = \setexp{ a, g, f, w }$ and: 
    \begin{talign}
      \intin{\const{alma}}{\model{\amodeli{1}}} & = a 
        & & &
      \intin{\sbinpred{loves}}{\model{\amodeli{1}}} & = \setexp{ \pair{g}{a}, \pair{f}{a}, \pair {w}{a} }
    \end{talign}
    \pause
    In this model there are not any lovers of lovers.
    \pause\medskip
    
    Hence: $\model{\amodeli{1}} \satisfies \aform$. 
  \end{exampleblock}
  \pause\medskip

  The set $\Gamma = \setexp{\aform, \, \formula{\lognot{\binpred{loves}{\const{alma}}{\const{alma}}}} }$ is \emph{consistent}:\\
  \hfill since it also holds: $\model{\amodeli{1}  } \satisfies \formula{\lognot{\binpred{loves}{\const{alma}}{\const{alma}}}}$.
  \vspace{10cm}
\end{frame}