       result
       (recur result))))
 
-(defn depth-tree-seq [tree] (tree-seq #(vector? (second %)) rest tree))
-
-(defn walk-tree
-  ([tree f]
-   (walk-tree [] tree (constantly true) f))
-  ([path tree filter-by f]
-   "Walks the syntax tree depth-first, filtering nodes with filter-by, and then
-   applying f to matched nodes (f takes path and node)."
-   (let [tree-seq (depth-tree-seq tree)
-         [subpath matched] (split-with (complement filter-by) tree-seq)
-         path (concat path subpath)]
-     (f path (first matched))
-     (if (empty? (rest matched))
-       nil
-       (recur path (rest matched) filter-by f)))))
+(def example-expr "\\A x { Cigla(x) => ((\\E y {Na(x, y) && ~Piramida(y)}) && (~\\E y {Na(x,y) && Na(y,x) }) && (\\A y { ~Cigla(y) => ~Jednako(x,y)}))}")
+
+(defn quantified-formula? [loc] (nonterm? (zip/node loc) :QuantifiedFormula))
+
+(defn- -extract-bound-literal [loc]
+  (if (quantified-formula? loc)
+    (-> loc zip/down zip/right zip/down zip/right zip/right zip/down zip/right zip/node)
+   nil))
+
+(defn- -extract-quantifier [loc]
+  (if (quantified-formula? loc)
+    (-> loc zip/down zip/right zip/down zip/right zip/down zip/node)
+   nil))
+
+(defn next-quantified-formula [loc quantifier]
+  (if (zip/end? loc)
+    nil
+    (if (= quantifier (zip/node loc))
+      (-> loc zip/up zip/up zip/up)
+      (recur (zip/next loc) quantifier))))
+
+(defn collect-quantifier-bound-atoms
+  ([loc] (collect-quantifier-bound-atoms (zip/up loc) []))
+  ([loc bound-atoms]
+   (if (nil? loc)
+     ;; Reached the root.
+     bound-atoms
+    (recur (zip/up loc)
+      (if (and (quantified-formula? loc) (= :FOREACH (-extract-quantifier loc)))
+        (conj bound-atoms (-extract-bound-literal loc))
+        bound-atoms)))))
+
+(defn replace-literal
+  [literal replacement loc]
+  (letfn [(recursive? [loc]
+            (if (zip/end? loc)
+              false
+              (if (nonterm? (zip/node loc) :LITERAL literal)
+                true
+                (recur (zip/next loc)))))
+          (alter-subtree [loc]
+            (if (zip/end? loc)
+              ;; Grab the whole modified subtree.
+              (zip/root loc)
+              (if (nonterm? (zip/node loc) :LITERAL literal)
+                ;; Replace literal.
+                (recur (zip/next (zip/edit loc (constantly replacement))))
+                ;; No literal here, move on.
+                (recur (zip/next loc)))))]
+    ;; Check for infinite recursion.
+    (if (recursive? (zip/vector-zip replacement))
+      (throw (IllegalArgumentException.
+               (str "Replacement " replacement " contains literal to replace " literal " !")))
+      (zip/edit loc #(alter-subtree (zip/vector-zip %))))))
+
+(def replacement-predicate-index (atom 0))
+(defn next-replacement-predicate! []
+  (str "F" (swap! replacement-predicate-index + 1)))
+
+(defn transform-existential-quantifiers
+  [tree]
+  (let [loc (zip/vector-zip tree)
+        replace-next-existential-formula
+        (fn [loc]
+          (if-let [existential-formula (next-quantified-formula loc :EXISTS)]
+            (let [bound-literal (-extract-bound-literal existential-formula)
+                  bound-atoms (collect-quantifier-bound-atoms existential-formula)
+                  replacement (reduce #(conj %1 (vector :LITERAL %2))
+                                      [:Predicate [:PRED (next-replacement-predicate!)]]
+                                      bound-atoms)
+                  ;; Remove the existential formula and replace it with its
+                  ;; contents.
+                  modified-loc (zip/edit existential-formula
+                                         (constantly (-> existential-formula
+                                                   zip/down
+                                                   zip/right
+                                                   zip/right
+                                                   zip/node)))]
+              ;; We replace all references to the bound-literal with replacement.
+              (recur (replace-literal bound-literal replacement modified-loc)))
+            ;; Nothing more to do.
+            (zip/root loc)))]
+    (replace-next-existential-formula loc)))
 
 (defn wff->cnf
-  [formula]
   "Converts a well-formed formula in string form to conjuctive-normal-form in
   tree form."
+  [formula]
   (-> (logic-parser formula)
       simplify-tree
       transform-implications
-      transform-negations))
-
-(def example-expr "\\A x { Cigla(x) => ((\\E y {Na(x, y) && ~Piramida(y)}) && (~\\E y {Na(x,y) && Na(y,x) }) && (\\A y { ~Cigla(y) => ~Jednako(x,y)}))}")
+      transform-negations
+      transform-existential-quantifiers))

(ns formlogic.parser
  (:require [instaparse.core :as insta]
            [clojure.tools.logging :as log]))

(def logic-parser (insta/parser (clojure.java.io/resource "logic.bnf")
                                :auto-whitespace :standard))

(def nonterms ^{:doc "Vector of all non-terminals"}
  [:WellFormedFormula
   :QuantifiedFormula
   :Quantifier

     (fn [& children]
       (let [[lhs rhs] children]
         [:Disjunction (-negate-formula lhs) rhs]))} tree))

(defn- -transform-term-negation
  [& children]
