docs: 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