You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
11 lines
360 B
11 lines
360 B
\begin{prooftree}
|
|
\AxiomC{$ \circled{6} \; c \lor \lnot e$}
|
|
\AxiomC{$ \circled{7} \; c \lor e$}
|
|
\BinaryInfC{$c$}
|
|
\AxiomC{$\circled{1} \; \lnot a \lor \lnot c \lor \lnot d$}
|
|
\BinaryInfC{$\lnot a \lor \lnot d$}
|
|
\AxiomC{$\circled{3} \; b \lor d$}
|
|
\BinaryInfC{$\lnot a \lor b$}
|
|
\end{prooftree}
|
|
|
|
The new learned clause is therefore Cl. 8: $\lnot a \lor b$
|