# CTL satisfied by Kripke Structure

given a Kripke Structure I want to check if a CTL formula is satisfied or not. the CTL is: $$AG(c \vee AX\neg E((a\vee b)Uc))$$ I have read that it is better to write to CTL in terms of $\wedge$ and E so for instance for an inner part $AX \neg E((a\vee b)Uc)$ I have re-written as: $$\neg EX\neg(\neg E(\neg(\neg a\wedge\neg b)Uc)$$ but it seems to be illegal CTL.

generally what is the best approach for these kinds of problems to solve. re-write the formula in terms of other operations or just draw the parse tree.