\begin{frame}[t]{At Most Two}
  \examplemodel
  \pause\bigskip
  
  \sentence{At most two $P$-values:}
  \pause
  \begin{talign}
    \model{\amodel} 
    \malt[1]{\gray{\satisfiesblack}}{\satisfies} 
    \formula{\forallst{x}{\forallst{y}{\forallst{z}{(
      \unpred{\mediumblue{P}}{x} \logandinf \unpred{\mediumblue{P}}{y} \logandinf \unpred{\mediumblue{P}}{z}
              \logimpinf \equalto{x}{y} \logorinf \equalto{x}{z} \logorinf \equalto{y}{z}
    )}}}}    
  \end{talign}
  \updatepause
  \sentence{Not at least three $P$-values:}
  \begin{talign}
    \model{\amodel} 
    \malt[1]{\gray{\satisfiesblack}}{\satisfies}
    \formula{\lognot{\existsst{x}{\existsst{y}{\existsst{z}{(
      \unpred{\mediumblue{P}}{x} \logandinf \unpred{\mediumblue{P}}{y} \logandinf \unpred{\mediumblue{P}}{z}
              \logandinf \notequalto{x}{y} \logandinf \notequalto{x}{z} \logandinf \notequalto{y}{z}
    )}}}}}  
  \end{talign}
  \updatepause
  Both are equivalent because:
  \begin{scenter}
    \sentence{at most two} ($\le 2$) $\iff$ \sentence{not: at least three} (not $\ge 3$)
  \end{scenter}
\end{frame}