First, you don't have to work in predicate calculus, i.e., there is no need to have the argument x. There is only one person in this problem, and different statements about him can be considered propositions.

Your translation of English into formulas seems correct.

In fact, I am not sure H is derivable from the rules you listed. The following explanation probably goes far beyond the scope of the course you are taking, but here it is anyway. The reason I am saying that H is not derivable is that there is a so-called constructive logic where you can prove strictly less than in regular logic. In particular, ¬¬P → P is not derivable in constructive logic. All the rules that you listed are valid in constructive logic. But the only way I see to derive H is by showing the negation of the premise of the first formula ¬(¬H v ¬S), which would imply H ∧ S in regular logic and therefore H. However, I believe that in constructive logic one can only derive ¬¬H ∧ ¬¬S and so ¬¬H. So I don't see a way to prove H.

However, this is probably a minor point and we can assume that we have the rule that derives P from ¬¬P.

The first step in constructing a derivation is to convince yourself that the conclusion indeed follows from the premises in a common-sense way, without thinking about particular inference rules. This is also probably the most important part because you may forget the inference rules used in this course, but the ability to think logically will often help you in life in general and especially if your work is related to exact sciences. By common-sense way I don't mean that the reasoning should depend on the particular plot of this problem. On the contrary, it is better to forget what propositional letters stand for and think just in terms of letters themselves.

I suggest you do this and post some informal reasoning of why H is true.

To convert the informal inference into a formal one may sometimes be tricky because the inference rules were specifically chosen to be few in number, so you have to reduce a large amount of logic to those few rules. I have not worked with these particular rules and I don't know if there is any general method, but probably you just need to look at what rule is applicable or will get you closer to the goal. For example, the only rule in the list that derives a negation is Modus Tollens, so this is a good rule to try in order to derive a negation.