We have introduced operators other than negation, conjunction and disjunction as macros. You must therefore expand them to apply the rules of the sequent calculus. Apart from that, you should not make simplifications, since otherwise, you may already solve the problem without using sequent calculus at all. The above formula is however quite difficult for the sequent calculus (I mean to handle manually).
