The performance of Branch-and-Bound algorithms is severely impaired by the presence of symmetric optima in a given problem. We describe a method for the automatic detection of formulation symmetries in MINLP instances. A software implementation of this method is used to conjecture the group structure of the problem symmetries of packing equal circles in a square. We provide a proof of the conjecture and compare the performance of spatial Branch-and-Bound on the original problem with the performance on a reformulation that cuts away symmetric optima.