Formally prove that these two premises are contradictory

Question

1. Clever(a) ∧ ¬Happy(a)
2. ∀x (Clever(x) → Happy(x))

So far I have something like this

[EDIT]

Thanks to Bram28 I got the correct proof.

Answer 1

Don't use subproofs!

Just eliminate the universal and after a few more lines you are done.

Here's a tip: Do not start any subproofs unless you know exactly what you are going to use those subproofs for. In Fitch, there are only 6 reasons for starting a subproof:

1. You are setting up a Proof by Contradiction (i.e $\neg$ Intro)

2. You are setting up a Proof by Cases (i.e $\lor$ Elim)

3. You are setting up a Conditional Proof (i.e $\rightarrow$ Intro)

4. You are setting up a BiConditional Proof (i.e $\leftrightarrow$ Intro)

5. You are setting up a Universal Proof (i.e $\forall$ Intro)

6. You are eliminating an existential (i.e $\exists$ Elim)

Note that in your case none of these rules make sense: you are not trying to prove a negation, conditional, biconditional, or universal, and you are not eliminating a disjunction or an existential.

Also, to force you to think about what you are using any subproof for, make it a habit to follow the following steps if you ever do start a subproof:

1. Start a (the) subproof(s) and write down the assumption(s)

2. Write down what you what at the end of (each of) the subproof(s)

3. Close the subproof(s) and apply the rule for which the subproof(s) was meant

4. Finally, go back inside the subproof and think: how can I get to the last line of my subproof given what I have?

So note that step 4 is the last thing you do, but note that in your partial proof you have been opening up a whole bunch of subproofs without indicating how you intend to use them. That's a really bad habit, and it's exactly what gets you stuck! Here's a post where I describe the 'correct' thought process for doing a specific Fitch proof.