                                                    zip/down
                                                    zip/right
                                                    zip/right
+                                                   ;; Now we are at formula contents.
                                                    zip/node)))]
               ;; We replace all references to the bound-literal with replacement.
               (recur (replace-literal bound-literal replacement modified-loc)))

      (recur used-literals (map str/join (comb/cartesian-product alphabet literals)))
      next-candidate))))

(defn transform-unique-quantifiers
  ([tree] (transform-unique-quantifiers (zip/vector-zip tree) #{}))
  ([loc atoms]
   (if-let [formula (next-quantified-formula loc :FOREACH)]
     (let [literal (-extract-bound-literal formula)]
       (if (contains? atoms literal)
         ;; This literal was used before. Replace it with unused literal.
         (let [modified-loc (replace-literal literal
                                             [:LITERAL (next-unused-literal atoms)]
                                             formula)]
           (recur (-> modified-loc zip/down zip/right zip/right) (conj atoms literal)))
         (recur (-> formula zip/down zip/right zip/right) (conj atoms literal))))
     (zip/root loc))))

(defn wff->cnf
  "Converts a well-formed formula in string form to conjuctive-normal-form in

      transform-implications
      transform-negations
      transform-existential-quantifiers
      transform-universal-quantifiers
      extract-quantifiers))
