Доказать методом резолюций ⊩ (A∨C→B)→(A→B)∧C→B

Имеется только следствие F1=(A∨C→B)→(A→B)∧C→B. Берем его отрицание и упрощаем, используя законы дистрибутивности и де Моргана:
F1= A∨C→B→A→B∧C→B= A∨C→B∨A∨B∧С∨B=
=A∨C)∨B∨A∨B∧С∨B=AС∨B∨A С ∨A B∨BС∨B=AС∨B∨A С ∨B=
=(AС∨B) ∧A С∧B=(A∨B)∧ (C∨B)∧ (A∨C)∧B.
Получено множество дизъюнктов: 1) A∨B, 2) C∨B, 3) A∨C, 4) B.
Строим вывод пустого дизъюнкта.
1) A∨B
2) C∨B
3) A∨C
4) B
5) A (1,4)
6) C (3,5)
7) B (2,6)
8) ⊡ (4,7)
Пустой дизъюнкт выведен