$(A \Rightarrow B \land \neg C) \land \neg(A \Rightarrow D) \Rightarrow \neg (B \Rightarrow D \lor C)$ is tautology, contradiction, or a satisfiable? 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?
 A: 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$.
A: 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. 
