Complicated Logic Proof involving Tautology and Law of Excluded Middle I'm having great difficulty solving the following problem, and even figuring out where to start with the proof.
$$
\neg A\lor\neg(\neg B\land(\neg A\lor B))
$$
Please see the following examples of how to do proofs, I would appreciate it if you could attempt to give me guidance using the tools and the line numbers that it cites similar to those below:
This is a sample proof:

This is another sample proof (law of excluded middles):

 A: first of all the statement is true (checking truth values for $A$ and $B$), even though ive now given two incorrect answers... here we go again!
$\begin{align}
& \neg A \lor \neg (\neg B \land (\neg A \lor B))\\
& =\neg A \lor \neg [(\neg B \land \neg A) \lor (\neg B \land B)]\\
& =\neg A \lor \neg [(\neg B \land \neg A) \lor FALSE]\\
& =\neg A \lor \neg(\neg B\land\neg A)\\
& =\neg A\lor(B\lor A) \text{ using } \neg(X\land Y)=\neg X\lor\neg Y\\
& =TRUE
\end{align}$
formalize this in whatever system youre using, you might have to prove a few things beforehand...
A: Seems like assuming the negation would give you a contradiction:
use ~ for 'negation', and & for 'and'; then your negated assumption becomes:
A&(~B&(~A\/B))                     (Assumption)
From which you get:
~B&(~A\/B)                        (By & elimination)
I think you can show from here that your (negated) assumption leads to a contradiction, by arguing by cases, from ~A\/B, and showing neither case is possible.
Now, ~A\/B follows using a second & elimination. Show neither ~A nor B is possible
  from the premises in your negated statement. Then from ~A\/B and ~(~A) and ~B,
  a contradiction to your negated assumption follows.  
Edit: this may be much simpler, tho yoyo's answer may be better than
   mine in that he gives a direct proof, and mine is by contradiction:
Assume the negation of your statement:
i)A& (~B&(~A\/B))
ii)Conclude A, by detachment.
iii)Conclude ~A by detachment inside of parenthesis.
iv)Negation of 'i)' follows by contradiction A&~A
Where detachment--more precisely, &-detachment-- is the rule that allows us to conclude either A, or B, from a statement A&B. To show it is a valid rule, you can either use a truth table to show it is a tautology/logical truth, derive it from the empty set of premises (this is the definition of theorem I am more familiar with), or,equivalently, show that the negation of either of :(A&B-->A) or of (A&B-->A), is a contradiction.For the second approach, assume A&B, and just conclude A (seems tautological, but it works; many of these arguments in sentence logic seem tautological anyway), or transform the implication A&B->A into the equivalent statement ~(A&B)\/A == ~A\/~B\/A== ~A\/A\/B==(~A\/A)\/B (I'm using here the result that A->B is truth-functionally equiv. to ~A\/B), which is a tautology.
A: The "complicated" formula :

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

can be re-written, due to the equivalence between $P \rightarrow Q$ and $\lnot P \lor Q$, as :

$A \rightarrow \lnot ((A \rightarrow B) \land \lnot B)$.

But $P \rightarrow Q$ is also equivalent to $\lnot (P \land \lnot Q)$; so the formula it is simply :


$A \rightarrow ((A \rightarrow B) \rightarrow B)$.


Now, a Natural Deduction proof is quite easy :
(1) $A$ - assumed
(2) $A \rightarrow B$ --- assumed
(3) $B$ --- from (1) and (2) by $\rightarrow$-elimination
(4) $(A \rightarrow B) \rightarrow B$ --- from (2) and (3) by $\rightarrow$-introduction
(5) $A \rightarrow ((A \rightarrow B) \rightarrow B)$ --- from (1) and (4) by $\rightarrow$-introduction.
A: Here is a proof using a Fitch-style proof checker. 

Assume the negation of what one is trying to prove on line 1 to attempt to derive a contradiction.
From lines 2 to 9, use De Morgan rule (DeM), conjunction elimination (∧E), double negative elimination (DNE) and disjunctive syllogism (DS) to simplify so one can arrive at two lines, 4 and 9, which are contradictory. That contradiction allows one to derive the goal on line 11 using indirect proof (IP).
Links to the proof checker and associated text are below.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf
