def negate(self, topv=None):
        """
            Given a CNF formula :math:`\mathcal{F}`, this method creates a CNF
            formula :math:`\\neg{\mathcal{F}}`. The negation of the formula is
            encoded to CNF with the use of *auxiliary* Tseitin variables [1]_.
            A new CNF formula is returned keeping all the newly introduced
            variables that can be accessed through the ``auxvars`` variable.

            **Note** that the negation of each clause is encoded with one
            auxiliary variable if it is not unit size. Otherwise, no auxiliary
            variable is introduced.

            :param topv: top variable identifier if any.
            :type topv: int

            :return: an object of class :class:`CNF`.

            .. [1] G. S. Tseitin. *On the complexity of derivations in the
                propositional calculus*.  Studies in Mathematics and
                Mathematical Logic, Part II. pp.  115–125, 1968

            .. code-block:: python

                >>> from pysat.formula import CNF
                >>> pos = CNF(from_clauses=[[-1, 2], [3]])
                >>> neg = pos.negate()
                >>> print neg.clauses
                [[1, -4], [-2, -4], [-1, 2, 4], [4, -3]]
                >>> print neg.auxvars
                [4, -3]
        """

        negated = CNF()

        negated.nv = topv
        if not negated.nv:
            negated.nv = self.nv

        negated.clauses = []
        negated.auxvars = []

        for cl in self.clauses:
            auxv = -cl[0]
            if len(cl) > 1:
                negated.nv += 1
                auxv = negated.nv

                # direct implication
                for l in cl:
                    negated.clauses.append([-l, -auxv])

                # opposite implication
                negated.clauses.append(cl + [auxv])

            # keeping all Tseitin variables
            negated.auxvars.append(auxv)

        negated.clauses.append(negated.auxvars)
        return negated
Given a CNF formula :math:`\mathcal{F}`, this method creates a CNF
            formula :math:`\\neg{\mathcal{F}}`. The negation of the formula is
            encoded to CNF with the use of *auxiliary* Tseitin variables [1]_.
            A new CNF formula is returned keeping all the newly introduced
            variables that can be accessed through the ``auxvars`` variable.

            **Note** that the negation of each clause is encoded with one
            auxiliary variable if it is not unit size. Otherwise, no auxiliary
            variable is introduced.

            :param topv: top variable identifier if any.
            :type topv: int

            :return: an object of class :class:`CNF`.

            .. [1] G. S. Tseitin. *On the complexity of derivations in the
                propositional calculus*.  Studies in Mathematics and
                Mathematical Logic, Part II. pp.  115–125, 1968

            .. code-block:: python

                >>> from pysat.formula import CNF
                >>> pos = CNF(from_clauses=[[-1, 2], [3]])
                >>> neg = pos.negate()
                >>> print neg.clauses
                [[1, -4], [-2, -4], [-1, 2, 4], [4, -3]]
                >>> print neg.auxvars
                [4, -3]