Worked on group example.
Clean group example, debug z3 translation.