Questionnaire-2024/equivalence_checking/0008_sol.tex

$$
  \underbracket{
    \underbracket{
      \lnot
      \underbracket{
        (a \lor \underbracket{\lnot b}_{x_4})
      }_{x_3}
    }_{x_1}
    \lor
    \underbracket{
      (\underbracket{\lnot a}_{x_5} \land c)
    }_{x_2}
  }_{x_\varphi}
$$




\begin{align*}
\varphi' = \ &x_\phi \land \\
              &\tseitinOr{x_\varphi}{x_1}{x_2} \land \\
              &\tseitinNot{x_1}{x_3} \land \\
              &\tseitinOr{x_3}{a}{x_4} \land \\
              &\tseitinAnd{x_2}{x_5}{c} \land \\
              &\tseitinNot{x_4}{b} \land \\
              &\tseitinNot{x_5}{a}
\end{align*}