It depends what you mean here with "correct". The two formulas are obviously equivalent to each other and both are only using ITE operations, variables and the Boolean constants. However, SNF as defined in the tool (and the slides) continues making case distinctions even when a variable is given, so you must not end with a variable "a" and should rather create its SNF as (a ? true : false). This is done to make SNF more comparable to BDDs which also make case distinctions for variables. You may have a more liberal definition that still will generate equivalent formulas, but then the canonical normal form property would be lost also.