added cnf computing before computing prenex