Para entrar en CNF, distribuir ∨'s ∧'s. Así:
((A∧¬B)∨(B∧C))∨(¬A∨¬C)⇔
(((A∧¬B)∨B)∧(A∧¬B)∨C)))∨(¬A∨¬C)⇔
((A∨B)∧(¬B∨B)∧(A∨C)∧(¬B∨C))∨(¬A∨¬C)⇔
((A∨B)∧⊤∧(A∨C)∧(¬B∨C))∨(¬A∨¬C)⇔
((A∨B)∧(A∨C)∧(¬B∨C))∨(¬A∨¬C)⇔
((A∨B)∨(¬A∨¬C))∧((A∨C)∨(¬A∨¬C))∧((¬B∨C)∨(¬A∨¬C))⇔
(A∨B∨¬A∨¬C)∧(A∨C∨¬A∨¬C)∧(¬B∨C∨¬A∨¬C)⇔
⊤∧⊤∧⊤⇔
⊤
Hmmm....
OK, por lo que hemos tomado de la declaración es y probado que esto es una tautología!
... pero no a través de la resolución ...
De hecho, usted tiene el mal set-up! Para probar esta afirmación a ser una tautología a través de la resolución, primero debe anular la declaración, y luego lo puso en CNF, por lo tanto en las cláusulas, y a continuación se derivan de la cláusula vacía a través de la resolución:
¬(((¬A∨B)∧(¬B∨¬C))→(A→¬C))⇔
((¬A∨B)∧(¬B∨¬C))∧¬(A→¬C)⇔
(¬A∨B)∧(¬B∨¬C)∧A∧C
Esto es ahora en CNF! ... y usted encontrará que la resolución que ahora es trivial