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