$(A \Rightarrow B \land \neg C) \land \neg(A \Rightarrow D) \Rightarrow \neg (B \Rightarrow D \lor C)$ is tautology, contradiction, or a satisfiable?

Question

All this step should be correct

$(A \Rightarrow B \land \neg C) \land \neg(A \Rightarrow D) \Rightarrow \neg (B \Rightarrow D \lor C)$

$(\neg A \lor (B \land \neg C)) \land \neg(\neg A \lor D) \Rightarrow \neg (\neg B \lor D \lor C)$

$(\neg A \lor (B \land \neg C)) \land (A \land \neg D) \Rightarrow (B \land \neg D \land \neg C)$

$\neg ((\neg A \lor (B \land \neg C)) \land (A \land \neg D)) \lor (B \land \neg D \land \neg C)$

$\neg (\neg A \lor (B \land \neg C)) \lor \neg (A \land \neg D) \lor (B \land \neg D \land \neg C)$

$(A \land \neg (B \land \neg C)) \lor (\neg A \lor D) \lor (B \land \neg D \land \neg C)$

$(A \land (\neg B \lor C)) \lor (\neg A \lor D) \lor (B \land \neg D \land \neg C)$

$(A \land \neg B) \lor (A \land C) \lor (\neg A \lor D) \lor (B \land \neg D \land \neg C)$

How to continue?

Answer 1

It is a tautology; we can derive with Natural Deduction : $¬(B⇒D∨C)$ from premises : $(A⇒B∧¬C)$ and $¬(A⇒D)$ and then use $\to$-intro and soundness.

1) $A \to (B∧¬C)$ --- premise

2) $¬(A \to D)$ --- premise

3) $B \to (D∨C)$ --- assumed [a]

4) $A$ --- assumed [b]

5) $B∧¬C$ --- $\to$-elim

6) $¬C$ --- $\land$-elim

7) $B$ --- $\land$-elim

8) $D∨C$ --- $\to$-elim

9) $D$ --- by Disjunctive syllogism (it is derivable in a sub-proof with $\lor$-elim)

10) $A \to D$ --- $\to$-intro, discharging [b]

11) contradiction ! --- from 2) and 10)

12) $\lnot (B \to (D∨C))$ --- from 3) and 11) by $\lnot$-intro, discharging [a].

---

We can check it also with Resolution deriving the empty clause ($\square$) from the conjunctive normal form of the three clauses :

1) $¬A∨(B∧¬C)$

2) $¬(¬A∨D)$

3) $¬B∨D∨C$.

Answer 2

Suppose that for a assignment d this is not true then $(A\implies B \land \neg C) \land \neg(A\implies D)$ should be true and $\neg(B\implies D\lor C)$ should be false.
From the first one we can easily deduce that A is true, D is false,B is true and C is false but then $\neg(B\implies D\lor C)$ is true so contradiction.
Therefore is tautology.