diff --git a/project.clj b/project.clj
index a594835..4610816 100644
--- a/project.clj
+++ b/project.clj
@@ -15,6 +15,7 @@
             [jonase/eastwood "0.2.3"]
             [lein-kibit "0.1.2"]
             [cider/cider-nrepl "0.11.0-SNAPSHOT"]]
+  :eastwood {:exclude-namespaces [nal.rules]}
   :target-path "target/%s"
   :repl-options {:init-ns          narjure.repl
                  :nrepl-middleware [narjure.repl/narsese-handler]}
diff --git a/src/nal/deriver.clj b/src/nal/deriver.clj
index 31e9d7a..5c493d3 100644
--- a/src/nal/deriver.clj
+++ b/src/nal/deriver.clj
@@ -1,36 +1,22 @@
 (ns nal.deriver
   (:require
     [nal.deriver.utils :refer [walk]]
-    [nal.deriver.key-path :refer [mall-paths all-paths path mpath-invariants]]
+    [nal.deriver.key-path :refer [mall-paths all-paths mpath-invariants
+                                  path-with-max-level]]
     [nal.deriver.rules :refer [rule]]))
 
-;!s.contains("task(") && !s.contains("measure_time(") && !s.contains("Structural") && !s.contains("Identity") && !s.contains("Negation")
-(defn child? [parent child]
-  (when-not (= child parent)
-    (let [[f _ l] child
-          [pf _ pl] parent
-          fp-inv (set (mpath-invariants pf))
-          fl-inv (set (mpath-invariants pl))]
-      (and (fp-inv f) (fl-inv l)))))
-
-(defn remove-children [paths]
-  (reduce #(remove (partial child? %2) %1) paths paths))
-
 (defn get-matcher [rules p1 p2]
-  (let [paths (->> (mall-paths p1 p2)
-                   (filter rules)
-                   remove-children)
-        matchers (->> (filter rules paths)
+  (let [matchers (->> (mall-paths p1 p2)
+                      (filter rules)
                       (select-keys rules)
-                      vals
-                      (map :matcher))]
+                      (map (fn [el] (:matcher (second el)))))]
     (case (count matchers)
       0 (constantly [])
       1 (first matchers)
       (fn [t1 t2] (mapcat #(% t1 t2) matchers)))))
 
 (def mget-matcher (memoize get-matcher))
-(def mpath (memoize path))
+(def mpath (memoize path-with-max-level))
 (defn generate-conclusions
   [rules {p1 :statement :as t1} {p2 :statement :as t2}]
   (let [matcher (mget-matcher rules (mpath p1) (mpath p2))]
diff --git a/src/nal/deriver/key_path.clj b/src/nal/deriver/key_path.clj
index 65052d7..f0d8d91 100644
--- a/src/nal/deriver/key_path.clj
+++ b/src/nal/deriver/key_path.clj
@@ -8,6 +8,18 @@
       (conj (map path tail) fst))
     :any))
 
+(defn path-with-max-level
+  ([statement] (path-with-max-level 0 statement))
+  ([level statement]
+   (if (coll? statement)
+     (let [[fst & tail] statement]
+       (cons fst
+             (if (> 1 level)
+               (let [next-level (if (= 'conj fst) level (inc level))]
+                 (map #(path-with-max-level next-level %) tail))
+               (repeat (count tail) :any))))
+     :any)))
+
 (defn rule-path
   "Generates detailed pattern for the rule."
   [p1 p2]
@@ -35,6 +47,7 @@
 
 (def mpath-invariants (memoize path-invariants))
 
+;(all-paths 'Y '(==> (seq-conj X A1 A2 A3) B))
 (defn all-paths
   "Generates all pathes for pair of premises."
   [p1 p2]
diff --git a/src/nal/deriver/list_expansion.clj b/src/nal/deriver/list_expansion.clj
index bf1e0bd..d765c81 100644
--- a/src/nal/deriver/list_expansion.clj
+++ b/src/nal/deriver/list_expansion.clj
@@ -2,6 +2,8 @@
   (:require [nal.deriver.utils :refer [walk]]
             [clojure.string :as s]))
 
+(def max-elements-in-list 7)
+
 (defn get-list
   "Finds the first :list element in the rule."
   [prefix statement]
@@ -49,7 +51,7 @@
               (if-let [from-name (get-list ":from" st)]
                 (expand-:from-element st from-name l-name %)
                 [st]))
-            (range 1 6))))
+            (range 1 (inc max-elements-in-list)))))
 
 (defn contains-list?
   "Checks if rule contains any :list element."
diff --git a/src/nal/deriver/matching.clj b/src/nal/deriver/matching.clj
index 42429cb..d367ae4 100644
--- a/src/nal/deriver/matching.clj
+++ b/src/nal/deriver/matching.clj
@@ -8,7 +8,7 @@
     [nal.deriver
      [set-functions :refer [f-map not-empty-diff? not-empty-inter?]]
      [substitution :refer [munification-map substitute]]
-     [preconditions :refer [sets compound-precondition shift-transformation
+     [preconditions :refer [sets compound-precondition conclusion-transformation
                             implications-and-equivalences get-terms abs
                             preconditions-transformations]]
      [normalization :refer [commutative-ops sort-commutative reducible-ops]
@@ -23,7 +23,8 @@
     `sort-commutative `n/reduce-ext-inter `n/reduce-symilarity `complement
     `n/reduce-int-dif `n/reduce-and `n/reduce-ext-dif `n/reduce-image
     `n/reduce-int-inter `n/reduce-neg `n/reduce-or `nil? `not `or `abs
-    `implications-and-equivalences `get-terms `empty? `intersection})
+    `implications-and-equivalences `get-terms `empty? `intersection
+    `n/reduce-seq-conj})
 
 (defn quote-operators
   [statement]
@@ -53,7 +54,7 @@
                      :goal (assoc conclusion :desire (list df t1 t2))
                      conclusion)]
     (if sc
-      (shift-transformation sc conclusion)
+      (conclusion-transformation sc conclusion)
       conclusion)))
 
 (defn traverse-node
diff --git a/src/nal/deriver/normalization.clj b/src/nal/deriver/normalization.clj
index 37c5584..57e2006 100644
--- a/src/nal/deriver/normalization.clj
+++ b/src/nal/deriver/normalization.clj
@@ -85,7 +85,7 @@
     [_ ['ext-inter & l1] l2] (union 'ext-inter l1 [l2])
     [_ l1 ['ext-inter & l2]] (union 'ext-inter [l1] l2)
     [_ ['int-set & l1] ['int-set & l2]] (union 'int-set l1 l2)
-    [_ ['ext-set & l1] ['ext-set & l2]] (union 'ext-set l1 l2)
+    ;[_ ['ext-set & l1] ['ext-set & l2]] (union 'ext-set l1 l2)
     :else st))
 
 (defn reduce-int-inter
@@ -156,6 +156,14 @@
     ['conj t1 t2] (if (= t1 t2) t1 st)
     :else st))
 
+(defn reduce-seq-conj
+  [st]
+  (let [cnt (count st)]
+    (cond
+      (= 3 cnt) (second st)
+      (odd? cnt) (vec (butlast st))
+      :else st)))
+
 (def reducible-ops
   {'ext-inter `reduce-ext-inter
    '|         `reduce-int-inter
diff --git a/src/nal/deriver/preconditions.clj b/src/nal/deriver/preconditions.clj
index c7f054f..ca97834 100644
--- a/src/nal/deriver/preconditions.clj
+++ b/src/nal/deriver/preconditions.clj
@@ -1,12 +1,13 @@
 (ns nal.deriver.preconditions
   (:require [nal.deriver.set-functions
              :refer [f-map not-empty-diff? not-empty-inter?]]
-            [nal.deriver.substitution :refer [munification-map]]
             [nal.deriver.utils :refer [walk]]
             [nal.deriver.substitution :refer [substitute munification-map]]
             [nal.deriver.terms-permutation :refer [implications equivalences]]
             [clojure.set :refer [union intersection]]
-            [narjure.defaults :refer [duration]]))
+            [narjure.defaults :refer [duration]]
+            [clojure.core.match :as m]
+            [nal.deriver.normalization :refer [reduce-seq-conj]]))
 
 (defn abs [^long n] (Math/abs n))
 
@@ -144,22 +145,57 @@
   [conclusion preconditions]
   (reduce check-precondition conclusion preconditions))
 
-(defn shift-transformation
-  [[type arg1 [_ arg2]] conclusion]
-  (let [dur (if (= :shift-occurrence-forward type)
-              duration
-              (- duration))]
-    (cond
-      (and (= :unused arg1) ('#{=|> ==>} arg2)) conclusion
-      (and (= :unused arg1) (not ('#{=|> ==>} arg2)))
-      `(let [:t-occurrence (~(if (= arg2 'pred-impl) `+ `-)
-                            :t-occurrence ~dur)]
-         ~conclusion)
-      ('#{=|> ==>} arg2)
-      `(let [:t-occurrence (+ :t-occurrence ~arg1)]
-         ~conclusion)
-      :default
-      `(let [:t-occurrence (+ (~(if (= arg2 'pred-impl) `+ `-)
-                               :t-occurrence ~dur)
-                              ~arg1)]
-         ~conclusion))))
+;-------------------------------------------------------------------------------
+(defmulti conclusion-transformation (fn [arg1 _] (first arg1)))
+
+(defn shift-forward-let
+  ([sym conclusion] (shift-forward-let sym nil conclusion nil))
+  ([sym op conclusion duration]
+   `(let [interval# ~sym
+          ~@(if duration
+              `[:t-occurrence (~op :t-occurrence ~duration)]
+              [])
+          :t-occurrence (if interval# (+ :t-occurrence interval#)
+                                      :t-occurrence)]
+      ~conclusion)))
+
+(defmethod conclusion-transformation :shift-occurrence-forward
+  [args concl]
+  (m/match (mapv #(if (and (coll? %) (= 'quote (first %)))
+                   (second %) %) (rest args))
+    [(:or '=|> '==>)] concl
+    ['pred-impl] `(let [:t-occurrence (+ :t-occurrence ~duration)] ~concl)
+    ['retro-impl] `(let [:t-occurrence (- :t-occurrence ~duration)] ~concl)
+    [sym (:or '=|> '==>)] (shift-forward-let sym concl)
+    [sym 'pred-impl] (shift-forward-let sym `+ concl duration)
+    [sym 'retro-impl] (shift-forward-let sym `- concl duration)))
+
+(defn backward-interval-check [sym]
+  `(and (coll? ~sym) (= (first ~sym) (quote ~'seq-conj))
+        (let [cnt# (count ~sym)]
+          (and (odd? cnt#) (get-in ~sym [(dec cnt#) 1])))))
+
+(defn shift-backward-let
+  ([sym conclusion] (shift-backward-let sym nil conclusion nil))
+  ([sym op conclusion duration]
+   `(let [interval# ~(backward-interval-check sym)
+          ~@(if duration
+              `[:t-occurrence (~op :t-occurrence ~duration)]
+              [])
+          :t-occurrence (if interval# (+ :t-occurrence interval#)
+                                      :t-occurrence)]
+      (if interval#
+        (update ~conclusion :statement reduce-seq-conj)
+        ~conclusion))))
+
+(defmethod conclusion-transformation :shift-occurrence-backward
+  [args concl]
+  (let [duration (- duration)]
+    (m/match (mapv #(if (and (coll? %) (= 'quote (first %)))
+                     (second %) %) (rest args))
+      [(:or '=|> '==>)] concl
+      ['pred-impl] `(let [:t-occurrence (+ :t-occurrence ~duration)] ~concl)
+      ['retro-impl] `(let [:t-occurrence (- :t-occurrence ~duration)] ~concl)
+      [sym (:or '=|> '==>)] (shift-backward-let sym concl)
+      [sym 'pred-impl] (shift-backward-let sym `+ concl duration)
+      [sym 'retro-impl] (shift-backward-let sym `- concl duration))))
diff --git a/src/nal/deriver/rules.clj b/src/nal/deriver/rules.clj
index c272d6e..81344a8 100644
--- a/src/nal/deriver/rules.clj
+++ b/src/nal/deriver/rules.clj
@@ -2,7 +2,7 @@
   (:require [clojure.string :as s]
             [clojure.set :refer [map-invert]]
             [nal.deriver
-             [key-path :refer [rule-path all-paths path-invariants]]
+             [key-path :refer [rule-path all-paths path-invariants path]]
              [utils :refer [walk]]
              [list-expansion :refer [contains-list? generate-all-lists]]
              [premises-swapping :refer [allow-swapping? swap]]
@@ -81,7 +81,7 @@
   of rules that matches [[--> [- :any :any] :any] :and [--> [:any :any]]] path."
   [ac [k {:keys [all starts-with]}]]
   (let [rules (mapcat :rules (vals (select-keys ac all)))]
-    (-> ac
+    ac #_(-> ac
         (update-in [k :rules] concat rules)
         (update-in [k :rules] set))))
 
@@ -92,7 +92,7 @@
   (-> ac
       (update-in [full-path :rules] conj rule)
       (assoc-in [full-path :pattern] [p1 p2])
-      (assoc-in [full-path :all] (all-paths p1 p2))
+      (assoc-in [full-path :all] (all-paths (path p1) (path p2)))
       (assoc-in [full-path :starts-with] (set (path-invariants p1)))
       (assoc-in [full-path :end-with] (set (path-invariants p2)))))
 
diff --git a/src/nal/deriver/substitution.clj b/src/nal/deriver/substitution.clj
index a3e1b00..1459099 100644
--- a/src/nal/deriver/substitution.clj
+++ b/src/nal/deriver/substitution.clj
@@ -3,20 +3,20 @@
             [clojure.core.unify :as u]
             [clojure.string :as s]))
 
-(def vars-map {"$" 'ind-var "#" 'dep-var})
-
 (defn replace-vars
   "Defn replaces var-elements from statemts by placeholders for unification."
   [var-type statement]
   (walk statement
-    (and (coll? el) (= var-type (first el)))
-    (->> el second (str "?") symbol)))
+    (and (coll? :el) (= var-type (first :el)))
+    (->> :el second (str "?") symbol)))
 
 (defn unification-map
   "Returns map of inified elements from both collections."
   [var-symbol p2 p3]
-  (let [var-type (vars-map var-symbol)]
-    (u/unify (replace-vars var-type p2) p3)))
+  (let [var-type (if (= var-symbol "$")
+                   'ind-var
+                   'dep-var)]
+    ((u/make-occurs-unify-fn #(and (coll? %) (= var-type (first %)))) p2 p3)))
 
 (def munification-map (memoize unification-map))
 
@@ -35,7 +35,5 @@
   "Unifies p2 and p3, then replaces elements from the unification map
   inside the conclusion."
   [var-symbol p2 p3 conclusion]
-  (let [var-type (vars-map var-symbol)
-        u-map (munification-map var-symbol p2 p3)
-        u-map (replace-placeholders var-type u-map)]
+  (let [u-map (munification-map var-symbol p2 p3)]
     (walk conclusion (u-map el) (u-map el))))
diff --git a/src/nal/deriver/utils.clj b/src/nal/deriver/utils.clj
index 64a2a4e..2ea8e56 100644
--- a/src/nal/deriver/utils.clj
+++ b/src/nal/deriver/utils.clj
@@ -11,7 +11,7 @@
   "Macro that helps to replace elements during walk. The first argument
   is collection, rest of the arguments are cond-like
   expressions. Default result of cond is element itself.
-  el is reserved name for current element of collection."
+  el (optionally :el) is reserved name for current element of collection."
   [coll & conditions]
   (let [el (gensym)
         replace-el (fn [coll]
diff --git a/src/nal/rules.clj b/src/nal/rules.clj
index c3cfed6..e13bbb0 100644
--- a/src/nal/rules.clj
+++ b/src/nal/rules.clj
@@ -261,10 +261,10 @@
 
   ; conditional syllogism
   ; If after M P usually happens and M happens it means P is expected to happen
-  #R[M (M ==> P) |- P :post (:t/deduction :d/induction :order-for-all-same) :pre ((:shift-occurrence-forward :unused ==>))]
-  #R[M (P ==> M) |- P :post (:t/abduction :d/deduction :order-for-all-same) :pre ((:shift-occurrence-backward :unused ==>))]
-  #R[M (S <=> M) |- S :post (:t/analogy :d/strong :order-for-all-same) :pre ((:shift-occurrence-backward :unused <=>))]
-  #R[M (M <=> S) |- S :post (:t/analogy :d/strong :order-for-all-same) :pre ((:shift-occurrence-forward :unused ==>))]
+  #R[M (M ==> P) |- P :post (:t/deduction :d/induction :order-for-all-same) :pre ((:shift-occurrence-forward ==>))]
+  #R[M (P ==> M) |- P :post (:t/abduction :d/deduction :order-for-all-same) :pre ((:shift-occurrence-backward ==>))]
+  #R[M (S <=> M) |- S :post (:t/analogy :d/strong :order-for-all-same) :pre ((:shift-occurrence-backward <=>))]
+  #R[M (M <=> S) |- S :post (:t/analogy :d/strong :order-for-all-same) :pre ((:shift-occurrence-forward ==>))]
 
   ; conjunction decompose
   #R[(&& :list/A) Ai |- Ai :pre (:contains? (:list/A) Ai) :post (:t/structural-deduction :d/structural-strong)]
@@ -371,11 +371,11 @@
 
 
   ; independent variable elimination
-  #R[B (A ==> C) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-forward :unused ==>))]
-  #R[B (C ==> A) |- C :post (:t/abduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-backward :unused ==>))]
+  #R[B (A ==> C) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-forward ==>))]
+  #R[B (C ==> A) |- C :post (:t/abduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-backward C ==>))]
 
-  #R[B (A <=> C) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-backward :unused <=>))]
-  #R[B (C <=> A) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-forward :unused <=>))]
+  #R[B (A <=> C) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-backward <=>))]
+  #R[B (C <=> A) |- C :post (:t/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" A B) (:shift-occurrence-forward <=>))]
 
   ; second level variable handling rules
   ; second level variable elimination (termlink level2 growth needed in order for these rules to work)
@@ -390,7 +390,7 @@
 
   ; NAL7 specific inference
   ; Reasoning about temporal statements. those are using the ==> relation because relation in time is a relation of the truth between statements.
-#R[X ((&/ K (:interval I)) ==> B) |- B  :post (:t/deduction :d/induction :order-for-all-same) :pre ((:substitute-if-unifies "$" K X) (:shift-occurrence-forward I ==>))]
+  #R[X ((&/ K (:interval I)) ==> B) |- B  :post (:t/deduction :d/induction :order-for-all-same) :pre ((:substitute-if-unifies "$" K X) (:shift-occurrence-forward I ==>))]
   #_#R[X (XI ==> B) |- B  :post (:t/deduction :d/induction :order-for-all-same) :pre ((:substitute-if-unifies "$" XI (&/ X :interval)) (:shift-occurrence-forward XI ==>))]
   #_#R[X (BI ==> Y) |- BI :post (:t/abduction :d/deduction :order-for-all-same) :pre ((:substitute-if-unifies "$" Y X) (:shift-occurrence-backward BI ==>))]
 
diff --git a/test/nal/test/core.clj b/test/nal/test/core.clj
index 950c8c2..b32923f 100644
--- a/test/nal/test/core.clj
+++ b/test/nal/test/core.clj
@@ -22,10 +22,31 @@
        :truth     [1 0.9]
        :occurrence 0}]
 
-    '({:statement [--> a1 [ext-image m _ a2 a3]]
-       :truth     [1 0.9]
-       :task-type :judgement
-       :occurrence 1})
+    '({:occurrence 1
+       :statement  [&| a1 [--> [* a1 a2 a3] m]]
+       :task-type  :judgement
+       :truth      [1.0
+                    0.81]}
+       {:occurrence 1
+        :statement  [--> a1 [ext-image m _ a2 a3]]
+        :task-type  :judgement
+        :truth      [1
+                     0.9]}
+       {:occurrence 1
+        :statement  [<|> a1 [--> [* a1 a2 a3] m]]
+        :task-type  :judgement
+        :truth      [1.0
+                     0.44751381215469616]}
+       {:occurrence 1
+        :statement  [=|> [--> [* a1 a2 a3] m] a1]
+        :task-type  :judgement
+        :truth      [1
+                     0.44751381215469616]}
+       {:occurrence 1
+        :statement  [=|> a1 [--> [* a1 a2 a3] m]]
+        :task-type  :judgement
+        :truth      [1
+                     0.44751381215469616]})
     '[{:statement [--> [* a1 a2 a3] m]
        :truth     [1 0.9]
        :task-type :judgement
@@ -60,9 +81,28 @@
        :truth     [1 0.9]
        :occurrence 0}]
 
-    '({:statement a1 :truth [1 0.44751381215469616]
-       :task-type :judgement
-       :occurrence 1})
+    '({:occurrence 1
+       :statement  [&| a1 [conj a1 a2 a3]]
+       :task-type  :judgement
+       :truth      [1.0 0.81]}
+       {:occurrence 1
+        :statement  [<|> a1 [conj a1 a2 a3]]
+        :task-type  :judgement
+        :truth      [1.0 0.44751381215469616]}
+       {:occurrence 1
+        :statement  [=|> [conj a1 a2 a3] a1]
+        :task-type  :judgement
+        :truth      [1
+                     0.44751381215469616]}
+       {:occurrence 1
+        :statement  [=|> a1 [conj a1 a2 a3]]
+        :task-type  :judgement
+        :truth      [1
+                     0.44751381215469616]}
+       {:occurrence 1
+        :statement  a1
+        :task-type  :judgement
+        :truth      [1 0.44751381215469616]})
     '[{:statement [conj a1 a2 a3]
        :truth     [1 0.9]
        :task-type :judgement
diff --git a/test/nal/test/deriver.clj b/test/nal/test/deriver.clj
index ea1c937..6fc7a23 100644
--- a/test/nal/test/deriver.clj
+++ b/test/nal/test/deriver.clj
@@ -3,110 +3,112 @@
             [nal.deriver :refer :all]
             [nal.rules :as r]))
 
+(def result
+  '({:statement  [</>
+                  [seq-conj [--> chess competition] [:interval 1000]]
+                  [--> sport competition]],
+     :task-type  :judgement,
+     :occurrence 1000,
+     :truth      [1.0 0.44751381215469616]}
+     {:statement  [seq-conj
+                   [--> chess competition]
+                   [:interval 1000]
+                   [--> sport competition]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1.0 0.81]}
+     {:statement  [pred-impl
+                   [seq-conj [--> chess competition] [:interval 1000]]
+                   [--> sport competition]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1 0.44751381215469616]}
+     {:statement  [retro-impl
+                   [--> sport competition]
+                   [seq-conj [--> chess competition] [:interval 1000]]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1 0.44751381215469616]}
+     {:statement  [--> sport chess],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1 0.44751381215469616]}
+     {:statement  [--> chess sport],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1 0.44751381215469616]}
+     {:statement  [<=> [--> chess [ind-var X]] [--> sport [ind-var X]]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1.0 0.44751381215469616]}
+     {:statement  [conj [--> chess [dep-var Y]] [--> sport [dep-var Y]]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1.0 0.81]}
+     {:statement  [<-> sport chess],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1.0 0.44751381215469616]}
+     {:statement  [==> [--> chess [ind-var X]] [--> sport [ind-var X]]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1 0.44751381215469616]}
+     {:statement  [==> [--> chess [ind-var X]] [--> sport [ind-var X]]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1 0.44751381215469616]}
+     {:statement  [==> [--> sport [ind-var X]] [--> chess [ind-var X]]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1 0.44751381215469616]}
+     {:statement  [==> [--> sport [ind-var X]] [--> chess [ind-var X]]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1 0.44751381215469616]}
+     {:statement  [--> [int-dif chess sport] competition],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [0.0 0.81]}
+     {:statement  [--> [| chess sport] competition],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1.0 0.81]}
+     {:statement  [--> [int-dif sport chess] competition],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [0.0 0.81]}
+     {:statement  [--> [ext-inter chess sport] competition],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1.0 0.81]}
+     {:statement  [pred-impl
+                   [seq-conj [--> chess [ind-var X]] [:interval 1000]]
+                   [--> sport [ind-var X]]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1 0.44751381215469616]}
+     {:statement  [</>
+                   [seq-conj [--> chess [ind-var X]] [:interval 1000]]
+                   [--> sport [ind-var X]]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1.0 0.44751381215469616]}
+     {:statement  [retro-impl
+                   [--> sport [ind-var X]]
+                   [seq-conj [--> chess [ind-var X]] [:interval 1000]]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1 0.44751381215469616]}
+     {:statement  [seq-conj
+                   [--> chess [dep-var Y]]
+                   [:interval 1000]
+                   [--> sport [dep-var Y]]],
+      :task-type  :judgement,
+      :occurrence 1000,
+      :truth      [1.0 0.81]}))
+
 (deftest test-generate-conclusions
-  (is (= (set
-           '({:statement [</>
-                          [seq-conj [--> chess competition] [:interval 1000]]
-                          [--> sport competition]],
-              :task-type :judgement,
-              :occurrence 1000,
-              :truth [1.0 0.44751381215469616]}
-              {:statement [seq-conj
-                           [--> chess competition]
-                           [:interval 1000]
-                           [--> sport competition]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1.0 0.81]}
-              {:statement [pred-impl
-                           [seq-conj [--> chess competition] [:interval 1000]]
-                           [--> sport competition]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1 0.44751381215469616]}
-              {:statement [retro-impl
-                           [--> sport competition]
-                           [seq-conj [--> chess competition] [:interval 1000]]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1 0.44751381215469616]}
-              {:statement [--> sport chess],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1 0.44751381215469616]}
-              {:statement [--> chess sport],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1 0.44751381215469616]}
-              {:statement [<=> [--> chess [ind-var X]] [--> sport [ind-var X]]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1.0 0.44751381215469616]}
-              {:statement [conj [--> chess [dep-var Y]] [--> sport [dep-var Y]]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1.0 0.81]}
-              {:statement [<-> sport chess],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1.0 0.44751381215469616]}
-              {:statement [==> [--> chess [ind-var X]] [--> sport [ind-var X]]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1 0.44751381215469616]}
-              {:statement [==> [--> chess [ind-var X]] [--> sport [ind-var X]]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1 0.44751381215469616]}
-              {:statement [==> [--> sport [ind-var X]] [--> chess [ind-var X]]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1 0.44751381215469616]}
-              {:statement [==> [--> sport [ind-var X]] [--> chess [ind-var X]]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1 0.44751381215469616]}
-              {:statement [--> [int-dif chess sport] competition],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [0.0 0.81]}
-              {:statement [--> [| chess sport] competition],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1.0 0.81]}
-              {:statement [--> [int-dif sport chess] competition],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [0.0 0.81]}
-              {:statement [--> [ext-inter chess sport] competition],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1.0 0.81]}
-              {:statement [pred-impl
-                           [seq-conj [--> chess [ind-var X]] [:interval 1000]]
-                           [--> sport [ind-var X]]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1 0.44751381215469616]}
-              {:statement [</>
-                           [seq-conj [--> chess [ind-var X]] [:interval 1000]]
-                           [--> sport [ind-var X]]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1.0 0.44751381215469616]}
-              {:statement [retro-impl
-                           [--> sport [ind-var X]]
-                           [seq-conj [--> chess [ind-var X]] [:interval 1000]]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1 0.44751381215469616]}
-              {:statement [seq-conj
-                           [--> chess [dep-var Y]]
-                           [:interval 1000]
-                           [--> sport [dep-var Y]]],
-               :task-type :judgement,
-               :occurrence 1000,
-               :truth [1.0 0.81]}))
+  (is (= (set result)
          (set (generate-conclusions
                 (r/rules :judgement)
                 '{:statement  [--> sport competition]
diff --git a/test/nal/test/deriver/list_expansion.clj b/test/nal/test/deriver/list_expansion.clj
index 465c9ef..b5a7fe9 100644
--- a/test/nal/test/deriver/list_expansion.clj
+++ b/test/nal/test/deriver/list_expansion.clj
@@ -112,6 +112,22 @@
         :pre
         (:question?)
         :post
+        (:t/belief-structural-deduction :p/judgment)]
+       [(W --> (| B A1 A2 A3 A4 A5 A6))
+        (W --> B)
+        |-
+        (W --> (| B A1 A2 A3 A4 A5 A6))
+        :pre
+        (:question?)
+        :post
+        (:t/belief-structural-deduction :p/judgment)]
+       [(W --> (| B A1 A2 A3 A4 A5 A6 A7))
+        (W --> B)
+        |-
+        (W --> (| B A1 A2 A3 A4 A5 A6 A7))
+        :pre
+        (:question?)
+        :post
         (:t/belief-structural-deduction :p/judgment)])
     '[(W --> (| B :list/A))
       (W --> B)
diff --git a/test/nal/test/deriver/normalization.clj b/test/nal/test/deriver/normalization.clj
index f65a08b..39f0571 100644
--- a/test/nal/test/deriver/normalization.clj
+++ b/test/nal/test/deriver/normalization.clj
@@ -39,9 +39,9 @@
     '[ext-inter 2 1] '[ext-inter [ext-inter 1] 2]
     '[ext-inter 2 1] '[ext-inter 1 [ext-inter 2]]
     '[int-set 2 1] '[ext-inter [int-set 1] [int-set 2]]
-    '[ext-set 2 1] '[ext-inter [ext-set 1] [ext-set 2]]
     '[int-set 2 1] '[ext-inter [int-set 1] [int-set 2]]
-    '[ext-set 2 1] '[ext-inter [ext-set 1] [ext-set 2]]
+    '[ext-inter [ext-set 1] [ext-set 2]]
+    '[ext-inter [ext-set 1] [ext-set 2]]
 
     2 '[| 2]
     '[| 1] '[| [| 1] [| 1]]
diff --git a/test/nal/test/deriver/substitution.clj b/test/nal/test/deriver/substitution.clj
index 98ebaef..1b7a3a0 100644
--- a/test/nal/test/deriver/substitution.clj
+++ b/test/nal/test/deriver/substitution.clj
@@ -27,7 +27,7 @@
 (deftest test-unification-map
   (are [a1 a2] (= a1 (apply unification-map a2))
     ;successfully unifies
-    '{?X tim} ["$" '[--> [ind-var X] alcoholic] '[--> tim alcoholic]]
+    '{[ind-var X] tim} ["$" '[--> [ind-var X] alcoholic] '[--> tim alcoholic]]
 
     ;unifies even if there is no vars
     {} ["$" '[--> tim alcoholic] '[--> tim alcoholic]]
@@ -37,7 +37,7 @@
          '[==> [--> ok a] [--> boss b]]]
 
     ;unifies, different vars can contain the same values
-    '{?X ok ?Y ok}
+    '{[ind-var X] ok [ind-var Y] ok}
     ["$" '[==> [--> [ind-var X] a] [--> [ind-var Y] b]]
      '[==> [--> ok a] [--> ok b]]]))