diff --git a/src/nal/deriver/matching.clj b/src/nal/deriver/matching.clj
index adf812d..a369e44 100644
--- a/src/nal/deriver/matching.clj
+++ b/src/nal/deriver/matching.clj
@@ -9,7 +9,7 @@
      [set-functions :refer [f-map not-empty-diff? not-empty-inter?]]
      [substitution :refer [munification-map substitute]]
      [preconditions :refer [sets compound-precondition get-terms
-                            implications-and-equivalences
+                            implications-and-equivalences abs
                             preconditions-transformations]]
      [normalization :refer [commutative-ops sort-commutative reducible-ops]
       :as n]
@@ -22,42 +22,37 @@
     `substitute `sets `some `deref `do `vreset! `volatile! `fn `mapv `if
     `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
-    `implications-and-equivalences `get-terms `empty? `intersection
-    })
+    `n/reduce-int-inter `n/reduce-neg `n/reduce-or `nil? `not `or `abs
+    `implications-and-equivalences `get-terms `empty? `intersection})
 
 (defn quote-operators
   [statement]
   (walk statement
-    (reserved-operators el) el
-    (and (symbol? el) (or (operator? el) (#{'Y 'X} el))) `'~el
-    (and (coll? el) (= 'quote (first el))
-         (= 'quote (first (second el))))
-    `(quote ~(second (second el)))
-    (and (coll? el) (= \a (first (str (first el)))))
-    (concat '() el)
-    (and (coll? el)
-         ((complement map?) el)
-         (let [f (first el)]
+    (and
+      (not (reserved-operators :el))
+      (symbol? :el)
+      (or (operator? :el) (#{'Y 'X} :el))) `'~:el
+    (and (coll? :el)
+         ((complement map?) :el)
+         (let [f (first :el)]
            (and (not (reserved-operators f))
                 (not (fn? f)))))
-    (vec el)))
+    (vec :el)))
 
 (defn form-conclusion
+  "Formation of cocnlusion in terms of task and truth/desire functions"
   [{:keys [t1 t2 task-type]}
    {c :statement tf :t-function pj :p/judgement df :d-function}]
   (let [conclusion-type (if pj :judgement task-type)
         conclusion {:statement c
-                    :task-type conclusion-type}
-        conclusion (if (= :judgement conclusion-type)
-                     (assoc conclusion :truth (list tf t1 t2))
-                     conclusion)
-        conclusion (if (= :goal conclusion-type)
-                     (assoc conclusion :desire (list df t1 t2))
-                     conclusion)]
-    conclusion))
+                    :task-type conclusion-type}]
+    (case conclusion-type
+      :judgement (assoc conclusion :truth (list tf t1 t2))
+      :goal (assoc conclusion :desire (list df t1 t2))
+      conclusion)))
 
 (defn traverse-node
+  "Generates code for precondition node."
   [vars result {:keys [conclusions children condition]}]
   `(when ~(quote-operators condition)
      ~(when-not (zero? (count conclusions))
@@ -66,30 +61,40 @@
                              (quote-operators conclusions)))))
      ~@(map (fn [n] (traverse-node vars result n)) children)))
 
-(defn traverse [vars tree]
+(defn traversal
+  "Walk through preconditions tree and generates code for matcher."
+  [vars tree]
   (let [results (gensym)]
     `(let [~results (volatile! [])]
        ~(traverse-node vars results tree)
        @~results)))
 
+(defn replace-occurences
+  "Reblaces occurrences keywords from matcher's code by generated symbols."
+  [code]
+  (let [t-occurence (gensym) b-occurence (gensym)]
+    (walk code
+      (= :el :t-occurence) t-occurence
+      (= :el :b-occurence) b-occurence)))
+
 (defn match-rules
-  [pattern rules task-type]
+  "Generates code of function that will match premises. Generated function
+  should be called with task and beleif as arguments."
+  [rules pattern task-type]
   (let [t1 (gensym) t2 (gensym)
         task (gensym) belief (gensym)
-        t-occurence (gensym) b-occurence (gensym)
         truth-kw (if (= :goal task-type) :desire :truth)]
-    (walk `(fn [{p1# :statement ~t1 ~truth-kw :t-occurence :occurence :as ~task}
-                {p2# :statement ~t2 :truth :b-occurence :occurence :as ~belief}]
-             (match [p1# p2#] ~(quote-operators pattern)
-               ~(traverse {:t1        t1
-                           :t2        t2
-                           :task      task
-                           :belief    belief
-                           :task-type task-type}
-                          rules)
-               :else nil))
-      (= :el :t-occurence) t-occurence
-      (= :el :b-occurence) b-occurence)))
+    (replace-occurences
+      `(fn [{p1# :statement ~t1 ~truth-kw :t-occurence :occurence :as ~task}
+            {p2# :statement ~t2 :truth :b-occurence :occurence :as ~belief}]
+         (match [p1# p2#] ~(quote-operators pattern)
+           ~(traversal {:t1        t1
+                        :t2        t2
+                        :task      task
+                        :belief    belief
+                        :task-type task-type}
+                       rules)
+           :else nil)))))
 
 (defn find-and-replace-symbols
   "Replaces all terms in statemnt to placeholders that will be used in pattern
@@ -112,7 +117,9 @@
                    s))]
     [@sym-map result]))
 
-(defn main-pattern [premise]
+(defn symbols->placeholders
+  "Replaces "
+  [premise]
   (second (find-and-replace-symbols premise "x")))
 
 (defn symbol-ordering-keyfn
@@ -153,20 +160,30 @@
 
 (defn get-desire-fn [post] (find-kv-by-prefix ":d/" post))
 
+(defn get-aliases
+  "Filter map of symbols and keep only aliases of symbol that have lower
+  order-key (to avoid preconditions with swapped symbols, like (= x1 x2)
+  (= x2 x1)."
+  [symbols-map alias]
+  (let [sym (symbols-map alias)]
+    (->> (dissoc symbols-map alias)
+         (filter (fn [[a v]]
+                   (and (< (symbol-ordering-keyfn alias)
+                           (symbol-ordering-keyfn a))
+                        (= v sym))))
+         keys)))
+
+(defn aliases->conditins
+  [symbols-map alias]
+  (mapcat #(list `= alias %) (get-aliases symbols-map alias)))
+
 (defn check-conditions [syms]
-  (filter not-empty
-          (keep
-            (fn [[alias sym]]
-              (let [aliases (filter (fn [[a v]]
-                                      (and (< (symbol-ordering-keyfn alias)
-                                              (symbol-ordering-keyfn a)) (= v sym)))
-                                    (dissoc syms alias))]
-                (mapcat (fn [[a]] `(= ~alias ~a)) aliases)))
-            syms)))
+  (->> (keys syms)
+       (keep (partial aliases->conditins syms))
+       (filter not-empty)))
 
 (defn commutative? [st]
-  (and (coll? st)
-       (some commutative-ops st)))
+  (and (coll? st) (some commutative-ops st)))
 
 (defn check-commutative [conclusion]
   (if (commutative? conclusion)
@@ -213,16 +230,14 @@
                 (if-not (#{`munification-map `not-empty-diff?} f)
                   (concat (list f) (sort-placeholders tail))
                   el)))]
-    {:conclusion {:statement    (-> conclusion
-                                    (preconditions-transformations preconditions)
-                                    (replace-symbols sym-map)
-                                    check-commutative
-                                    check-reduction)
-                  :t-function   (t/tvtypes (get-truth-fn post))
-                  :t-function-n (get-truth-fn post)
-                  :d-function   (t/dvtypes (get-desire-fn post))
-                  :d-function-n (get-desire-fn post)
-                  :p/judgement  (some #{:p/judgment} post)}
+    {:conclusion {:statement   (-> conclusion
+                                   (preconditions-transformations preconditions)
+                                   (replace-symbols sym-map)
+                                   check-commutative
+                                   check-reduction)
+                  :t-function  (t/tvtypes (get-truth-fn post))
+                  :d-function  (t/dvtypes (get-desire-fn post))
+                  :p/judgement (some #{:p/judgement} post)}
      :conditions (walk (concat (check-conditions sym-map) pre)
                    (and (coll? el) (= \a (first (str (first el)))))
                    (concat '() el)
@@ -279,22 +294,26 @@
   [conds cpm]
   (map (fn [[cnds k]] [(sort-by cpm cnds) k]) conds))
 
-(defn gen-rules [pattern rules]
-  (let [main (main-pattern pattern)
-        rules (mapcat (fn [{:keys [p1 p2 conclusions pre]}]
+(defn gen-rules
+  "Prepeares data for generation of conditions tree and then generates tree."
+  [main-pattern rules]
+  (let [rules (mapcat (fn [{:keys [p1 p2 conclusions pre]}]
                         (map #(vector [p1 p2] % pre) conclusions))
                       rules)
-        cond-conclusions-m (conditions->conclusions-map main rules)
+        cond-conclusions-m (conditions->conclusions-map main-pattern rules)
         cpm (conds-priorities-map cond-conclusions-m)
         sorted-conds (sort-conds cond-conclusions-m cpm)]
     (generate-tree sorted-conds)))
 
-(defn generate-matching [rules task-type]
+(defn generate-matching
+  "Generates code for rule matcher."
+  [rules task-type]
   (->> rules
        (map (fn [[k {:keys [pattern rules] :as v}]]
-              (let [match-fn-code (match-rules (main-pattern pattern)
-                                               (gen-rules pattern rules)
-                                               task-type)]
+              (let [main-pattern (symbols->placeholders pattern)
+                    match-fn-code (-> main-pattern
+                                      (gen-rules rules)
+                                      (match-rules main-pattern task-type))]
                 [k (assoc v :matcher (eval match-fn-code)
                             :matcher-code match-fn-code)])))
        (into {})))
diff --git a/src/nal/deriver/normalization.clj b/src/nal/deriver/normalization.clj
index 5ce2802..37c5584 100644
--- a/src/nal/deriver/normalization.clj
+++ b/src/nal/deriver/normalization.clj
@@ -63,18 +63,18 @@
   (if (coll? conclusions)
     (let [f (first conclusions)]
       (if (commutative-ops f)
-        (into [] (conj (sort-by hash (drop 1 conclusions)) f))
+        (vec (conj (sort-by hash (drop 1 conclusions)) f))
         conclusions))
     conclusions))
 
 ;https://gist.github.com/TonyLo1/a3f8e05458c5e90c2e72
 (defn union
   ([c1 c2] (sort-by hash (set (concat c1 c2))))
-  ([op c1 c2] (into [] (conj (union c1 c2) op))))
+  ([op c1 c2] (vec (conj (union c1 c2) op))))
 
 (defn diff
   ([c1 c2] (into '() (set/difference (set c1) (set c2))))
-  ([op c1 c2] (into [] (conj (diff c1 c2) op))))
+  ([op c1 c2] (vec (conj (diff c1 c2) op))))
 
 (defn reduce-ext-inter
   [st]
@@ -121,7 +121,7 @@
 (defn reduce-production
   [st]
   (m/match st
-    ['* ['* & l1] & l2] (into [] (conj (concat l1 l2) '*))
+    ['* ['* & l1] & l2] (vec (conj (concat l1 l2) '*))
     :else st))
 
 (defn reduce-image
diff --git a/src/nal/deriver/preconditions.clj b/src/nal/deriver/preconditions.clj
index 9ac10e8..345ee81 100644
--- a/src/nal/deriver/preconditions.clj
+++ b/src/nal/deriver/preconditions.clj
@@ -5,12 +5,13 @@
             [nal.deriver.utils :refer [walk]]
             [nal.deriver.substitution :refer [substitute munification-map]]
             [nal.deriver.terms-permutation :refer [implications equivalences]]
-            [clojure.set :refer [union intersection]]))
+            [clojure.set :refer [union intersection]]
+            [narjure.defaults :refer [duration]]))
+
+(defn abs [^long n] (Math/abs n))
 
 ;TODO preconditions
 ;:shift-occurrence-forward :shift-occurrence-backward
-;:no-common-subterm
-;:measure-time :concurrent
 (defmulti compound-precondition
   "Expands compound precondition to clojure sequence
   that will be evaluted later"
@@ -20,7 +21,7 @@
 
 (defmethod compound-precondition :!=
   [[_ & args]]
-  [(concat (list `not=) args)])
+  [`(not= ~@args)])
 
 (defn check-set [set-type arg]
   `(and (coll? ~arg) (= ~set-type (first ~arg))))
@@ -85,7 +86,12 @@
 (defmethod compound-precondition :measure-time
   [_]
   [`(not= :eternal :t-occurence)
-   `(not= :eternal :b-occurence)])
+   `(not= :eternal :b-occurence)
+   `(<= ~duration (abs (- :t-occurence :b-occurence)))])
+
+(defmethod compound-precondition :concurrent
+  [_]
+  [`(> ~duration (abs (- :t-occurence :b-occurence)))])
 
 ;-------------------------------------------------------------------------------
 (defmulti precondition-transformation (fn [arg1 _] (first arg1)))
@@ -94,7 +100,7 @@
 
 (defn sets-transformation
   [[cond-name el1 el2 el3] conclusion]
-  (walk conclusion (= el el3)
+  (walk conclusion (= :el el3)
     `(~(f-map cond-name) ~el1 ~el2)))
 
 (doall (map
@@ -122,7 +128,7 @@
 (defmethod precondition-transformation :measure-time
   [[_ arg] conclusion]
   (let [mt (gensym)]
-    (walk `(let [k# 1 ~arg (- :t-occurence :b-occurence)]
+    (walk `(let [~arg (abs (- :t-occurence :b-occurence))]
              ~(walk conclusion
                 (= :el arg) [:interval arg]))
       (= :el arg) mt)))
diff --git a/src/nal/deriver/truth.clj b/src/nal/deriver/truth.clj
index 6acfef0..9b6b620 100644
--- a/src/nal/deriver/truth.clj
+++ b/src/nal/deriver/truth.clj
@@ -113,7 +113,7 @@
 (defn belief-structural-deduction [_ p2]
   (when p2 (deduction p2 [1 d/judgement-confidence])))
 
-(defn belief-structural-difference [p1 p2]
+(defn belief-structural-difference [_ p2]
   (when p2
     (let [[^double f ^double c] (deduction p2 [1 d/judgement-confidence])]
       [(- 1 f) c])))
diff --git a/src/nal/rules.clj b/src/nal/rules.clj
index cb2249c..f910407 100644
--- a/src/nal/rules.clj
+++ b/src/nal/rules.clj
@@ -6,9 +6,9 @@
 
 (defrules rules
   ;Similarity to Inheritance
-  #R[(S --> P) (S <-> P) |- (S --> P) :post (:t/struct-int :p/judgment) :pre (:question?)]
+  #R[(S --> P) (S <-> P) |- (S --> P) :post (:t/struct-int :p/judgement) :pre (:question?)]
   ;Inheritance to Similarity
-  #R[(S <-> P) (S --> P) |- (S <-> P) :post (:t/struct-abd :p/judgment) :pre (:question?)]
+  #R[(S <-> P) (S --> P) |- (S <-> P) :post (:t/struct-abd :p/judgement) :pre (:question?)]
   ;Set Definition Similarity to Inheritance
   #R[(S <-> {P}) S |- (S --> {P}) :post (:t/identity :d/identity :allow-backward)]
   #R[(S <-> {P}) {P} |- (S --> {P}) :post (:t/identity :d/identity :allow-backward)]
@@ -36,11 +36,11 @@
   ; Immediate Inference
   ; If S can stand for P P can to a certain low degree also represent the class S
   ; If after S usually P happens then it might be a good guess that usually before P happens S happens.
-  #R[(P --> S) (S --> P) |- (P --> S) :post (:t/conversion :p/judgment) :pre (:question?)]
-  #R[(P ==> S) (S ==> P) |- (P ==> S) :post (:t/conversion :p/judgment) :pre (:question?)]
-  #R[(P =|> S) (S =|> P) |- (P =|> S) :post (:t/conversion :p/judgment) :pre (:question?)]
-  #R[(P =\> S) (S =/> P) |- (P =\> S) :post (:t/conversion :p/judgment) :pre (:question?)]
-  #R[(P =/> S) (S =\> P) |- (P =/> S) :post (:t/conversion :p/judgment) :pre (:question?)]
+  #R[(P --> S) (S --> P) |- (P --> S) :post (:t/conversion :p/judgement) :pre (:question?)]
+  #R[(P ==> S) (S ==> P) |- (P ==> S) :post (:t/conversion :p/judgement) :pre (:question?)]
+  #R[(P =|> S) (S =|> P) |- (P =|> S) :post (:t/conversion :p/judgement) :pre (:question?)]
+  #R[(P =\> S) (S =/> P) |- (P =\> S) :post (:t/conversion :p/judgement) :pre (:question?)]
+  #R[(P =/> S) (S =\> P) |- (P =/> S) :post (:t/conversion :p/judgement) :pre (:question?)]
 
   ; "If not smoking lets you be healthy being not healthy may be the result of smoking"
   #R[(--S ==> P) P |- (--P ==> S) :post (:t/contraposition :allow-backward)]
@@ -308,17 +308,17 @@
                               (&& (S --> #Y) (P --> #Y)) :post (:t/intersection))
                                   :pre ((:!= S P))]
 
- #_#R[(S --> M) (P --> M) |- (((&/ (P --> $X) I) =/> (S --> $X)) :post (:t/induction :linkage-temporal)
+ #R[(S --> M) (P --> M) |- (((&/ (P --> $X) I) =/> (S --> $X)) :post (:t/induction :linkage-temporal)
                               ((S --> $X) =\> (&/ (P --> $X) I)) :post (:t/abduction :linkage-temporal)
                               ((&/ (P --> $X) I) </> (S --> $X)) :post (:t/comparison :linkage-temporal)
                               (&/ (P --> #Y) I (S --> #Y)) :post (:t/intersection :linkage-temporal))
             :pre ((:!= S P) (:measure-time I))]
 
-  #_#R[(S --> M) (P --> M) |- (((P --> $X) =|> (S --> $X)) :post (:t/abduction :linkage-temporal)
+  #R[(S --> M) (P --> M) |- (((P --> $X) =|> (S --> $X)) :post (:t/abduction :linkage-temporal)
                               ((S --> $X) =|> (P --> $X)) :post (:t/induction :linkage-temporal)
                               ((P --> $X) <|> (S --> $X)) :post (:t/comparison :linkage-temporal)
                               (&| (P --> #Y) (S --> #Y)) :post (:t/intersection :linkage-temporal))
-            :pre ((:!= S P) (concurrent Task Belief))]
+            :pre ((:!= S P) (:concurrent Task Belief))]
 
   #R[(M --> S) (M --> P) |- ((($X --> S) ==> ($X --> P)) :post (:t/induction)
                               (($X --> P) ==> ($X --> S)) :post (:t/abduction)
@@ -332,7 +332,7 @@
                               (&/ (#Y --> P) I (#Y --> S)) :post (:t/intersection :linkage-temporal))
      :pre ((:!= S P) (:measure-time I))]
 
-  #_#R[(M --> S) (M --> P) |- ((($X --> S) =|> ($X --> P)) :post (:t/induction :linkage-temporal)
+  #R[(M --> S) (M --> P) |- ((($X --> S) =|> ($X --> P)) :post (:t/induction :linkage-temporal)
                               (($X --> P) =|> ($X --> S)) :post (:t/abduction :linkage-temporal)
                               (($X --> S) <|> ($X --> P)) :post (:t/comparison :linkage-temporal)
                               (&| (#Y --> S) (#Y --> P)) :post (:t/intersection :linkage-temporal))
@@ -395,13 +395,13 @@
 
   ; Temporal induction:
   ; When P and then S happened according to an observation by induction (weak) it may be that alyways after P usually S happens.
-  #_#R[P S |- (((&/ S I) =/> P) :post (:t/induction :linkage-temporal)
+  #R[P S |- (((&/ S I) =/> P) :post (:t/induction :linkage-temporal)
               (P =\> (&/ S I)) :post (:t/abduction :linkage-temporal)
               ((&/ S I) </> P) :post (:t/comparison :linkage-temporal)
               (&/ S I P) :post (:t/intersection :linkage-temporal))
      :pre ((:measure-time I))]
-  #_#R[P S |- ((S =|> P) :post (:t/induction :linkage-temporal)
-              (P =|> S) :post (:t/induction :linkage-temporal)
+  #R[P S |- ((S =|> P) :post (:t/induction :linkage-temporal)
+              ;(P =|> S) :post (:t/induction :linkage-temporal)
               (S <|> P) :post (:t/comparison :linkage-temporal)
               (&| S P) :post (:t/intersection :linkage-temporal))
      :pre [(:concurrent Task Belief) (:not-implication-or-equivalence P) (:not-implication-or-equivalence S)]]
@@ -414,40 +414,40 @@
 
   ; and the backward inference driven forward inference:
   ; NAL2:
-  #R[([A] <-> [B]) (A <-> B) |- ([A] <-> [B]) :pre (:question?) :post (:t/belief-identity :p/judgment)]
-  #R[({A} <-> {B}) (A <-> B) |- ({A} <-> {B}) :pre (:question?) :post (:t/belief-identity :p/judgment)]
+  #R[([A] <-> [B]) (A <-> B) |- ([A] <-> [B]) :pre (:question?) :post (:t/belief-identity :p/judgement)]
+  #R[({A} <-> {B}) (A <-> B) |- ({A} <-> {B}) :pre (:question?) :post (:t/belief-identity :p/judgement)]
 
-  #R[([A] --> [B]) (A <-> B) |- ([A] --> [B]) :pre (:question?) :post (:t/belief-identity :p/judgment)]
-  #R[({A} --> {B}) (A <-> B) |- ({A} --> {B}) :pre (:question?) :post (:t/belief-identity :p/judgment)]
+  #R[([A] --> [B]) (A <-> B) |- ([A] --> [B]) :pre (:question?) :post (:t/belief-identity :p/judgement)]
+  #R[({A} --> {B}) (A <-> B) |- ({A} --> {B}) :pre (:question?) :post (:t/belief-identity :p/judgement)]
 
   ; NAL3:
   ; composition on both sides of a statement:
-  #R[((& B :list/A) --> (& A :list/A)) (B --> A) |- ((& B :list/A) --> (& A :list/A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
-  #R[((| B :list/A) --> (| A :list/A)) (B --> A) |- ((| B :list/A) --> (| A :list/A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
-  #R[((- S A) --> (- S B)) (B --> A) |- ((- S A) --> (- S B)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
-  #R[((~ S A) --> (~ S B)) (B --> A) |- ((~ S A) --> (~ S B)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
+  #R[((& B :list/A) --> (& A :list/A)) (B --> A) |- ((& B :list/A) --> (& A :list/A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
+  #R[((| B :list/A) --> (| A :list/A)) (B --> A) |- ((| B :list/A) --> (| A :list/A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
+  #R[((- S A) --> (- S B)) (B --> A) |- ((- S A) --> (- S B)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
+  #R[((~ S A) --> (~ S B)) (B --> A) |- ((~ S A) --> (~ S B)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
 
   ; composition on one side of a statement:
-  #R[(W --> (| B :list/A)) (W --> B) |- (W --> (| B :list/A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
-  #R[((& B :list/A) --> W) (B --> W) |- ((& B :list/A) --> W) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
-  #R[(W --> (- S B)) (W --> B) |- (W --> (- S B)) :pre (:question?) :post (:t/belief-structural-difference :p/judgment)]
-  #R[((~ S B) --> W) (B --> W) |- ((~ S B) --> W) :pre (:question?) :post (:t/belief-structural-difference :p/judgment)]
+  #R[(W --> (| B :list/A)) (W --> B) |- (W --> (| B :list/A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
+  #R[((& B :list/A) --> W) (B --> W) |- ((& B :list/A) --> W) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
+  #R[(W --> (- S B)) (W --> B) |- (W --> (- S B)) :pre (:question?) :post (:t/belief-structural-difference :p/judgement)]
+  #R[((~ S B) --> W) (B --> W) |- ((~ S B) --> W) :pre (:question?) :post (:t/belief-structural-difference :p/judgement)]
 
   ; NAL4:
   ; composition on both sides of a statement:
-  #R[((* B P) --> Z) (B --> A) |- ((* B P) --> (* A P)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
-  #R[((* P B) --> Z) (B --> A) |- ((* P B) --> (* P A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
-  #R[((* B P) <-> Z) (B <-> A) |- ((* B P) <-> (* A P)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
-  #R[((* P B) <-> Z) (B <-> A) |- ((* P B) <-> (* P A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
-  #R[((\ N A _) --> Z) (N --> R) |- ((\ N A _) --> (\ R A _)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
-  #R[((/ N _ B) --> Z) (S --> B) |- ((/ N _ B) --> (/ N _ S)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
+  #R[((* B P) --> Z) (B --> A) |- ((* B P) --> (* A P)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
+  #R[((* P B) --> Z) (B --> A) |- ((* P B) --> (* P A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
+  #R[((* B P) <-> Z) (B <-> A) |- ((* B P) <-> (* A P)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
+  #R[((* P B) <-> Z) (B <-> A) |- ((* P B) <-> (* P A)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
+  #R[((\ N A _) --> Z) (N --> R) |- ((\ N A _) --> (\ R A _)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
+  #R[((/ N _ B) --> Z) (S --> B) |- ((/ N _ B) --> (/ N _ S)) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
 
   ; NAL5:
-  #R[--A    A |- --A  :pre (:question?) :post (:t/belief-negation :p/judgment)]
-  #R[A  --A |-   A  :pre (:question?) :post (:t/belief-negation :p/judgment)]
+  #R[--A    A |- --A  :pre (:question?) :post (:t/belief-negation :p/judgement)]
+  #R[A  --A |-   A  :pre (:question?) :post (:t/belief-negation :p/judgement)]
 
   ; compound composition one premise
-  #R[(|| B :list/A) B |- (|| B :list/A) :pre (:question?) :post (:t/belief-structural-deduction :p/judgment)]
+  #R[(|| B :list/A) B |- (|| B :list/A) :pre (:question?) :post (:t/belief-structural-deduction :p/judgement)]
 )
 
 (defn freq [task-type]
diff --git a/src/narjure/defaults.clj b/src/narjure/defaults.clj
index b41a821..2bbe646 100644
--- a/src/narjure/defaults.clj
+++ b/src/narjure/defaults.clj
@@ -31,3 +31,5 @@
    :question question-budget})
 
 (def ^{:type double} horizon 1)
+
+(def duration 80)
diff --git a/test/nal/test/core.clj b/test/nal/test/core.clj
index a873f1e..96d94da 100644
--- a/test/nal/test/core.clj
+++ b/test/nal/test/core.clj
@@ -13,11 +13,13 @@
 
     '[{:statement [--> [ext-set tim] [int-set drunk]]
        :truth     [1 0.9]
-       :task-type :judgement}
+       :task-type :judgement
+       :occurence 1}
 
       {:statement [==> [&| [--> [ind-var X] [int-set drunk]] [--> [ind-var X] [int-set driving]]]
                    [--> [ind-var X] [int-set dead]]]
-       :truth     [1 0.9]}]
+       :truth     [1 0.9]
+       :occurence 0}]
 
 
     '({:statement [--> a1 [ext-image m _ a2 a3]]
@@ -25,37 +27,66 @@
        :task-type :judgement})
     '[{:statement [--> [* a1 a2 a3] m]
        :truth     [1 0.9]
-       :task-type :judgement}
+       :task-type :judgement
+       :occurence 1}
 
       {:statement a1
-       :truth     [1 0.9]}]
+       :truth     [1 0.9]
+       :occurence 0}]
 
-    []
+    '[{:statement [&| [--> [* a1 a2 a3] m] a1]
+       :task-type :judgement
+       :truth     [1.0 0.81]}
+      {:statement [<|> a1 [--> [* a1 a2 a3] m]]
+       :task-type :judgement
+       :truth     [1.0 0.44751381215469616]}
+      {:statement [=|> [--> [* a1 a2 a3] m] a1]
+       :task-type :judgement
+       :truth     [1 0.44751381215469616]}
+      {:statement [=|> a1 [--> [* a1 a2 a3] m]]
+       :task-type :judgement
+       :truth     [1 0.44751381215469616]}]
     '[{:statement a1
        :truth     [1 0.9]
-       :task-type :judgement}
+       :task-type :judgement
+       :occurence 1}
 
       {:statement [--> [* a1 a2 a3] m]
-       :truth     [1 0.9]}]
+       :truth     [1 0.9]
+       :occurence 0}]
 
     '({:statement a1 :truth [1 0.44751381215469616] :task-type :judgement})
     '[{:statement [conj a1 a2 a3]
        :truth     [1 0.9]
-       :task-type :judgement}
+       :task-type :judgement
+       :occurence 1}
 
       {:statement a1
-       :truth     [1 0.9]}]
+       :truth     [1 0.9]
+       :occurence 0}]
 
-    []
+    '[{:statement [&| [--> M S] [[--> M S] [--> M P]]]
+       :task-type :judgement
+       :truth     [1.0 0.81]}
+      {:statement [<|> [--> M S] [[--> M S] [--> M P]]]
+       :task-type :judgement
+       :truth     [1.0 0.44751381215469616]}
+      {:statement [=|> [--> M S] [[--> M S] [--> M P]]]
+       :task-type :judgement
+       :truth     [1 0.44751381215469616]}
+      {:statement [=|> [[--> M S] [--> M P]] [--> M S]]
+       :task-type :judgement
+       :truth     [1 0.44751381215469616]}]
     '[{:statement [[--> M S] [--> M P]]
        :truth     [1 0.9]
-       :task-type :judgement}
+       :task-type :judgement
+       :occurence 1}
 
       {:statement [--> M S]
-       :truth     [1 0.9]}]
+       :truth     [1 0.9]
+       :occurence 0}]
 
-    '({:statement [conj
-                   [--> [dep-var Y] [int-set B]]
+    '({:statement [conj [--> [dep-var Y] [int-set B]]
                    [==> [--> [ext-set A] [int-set Y]] [--> [dep-var Y] P]]]
        :truth     [1.0 0.81]
        :task-type :judgement}
@@ -66,7 +97,9 @@
         :task-type :judgement})
     '[{:statement [==> [--> [ext-set A] [int-set Y]] [--> [ext-set A] P]]
        :truth     [1 0.9]
-       :task-type :judgement}
+       :task-type :judgement
+       :occurence 1}
 
       {:statement [--> [ext-set A] [int-set B]]
-       :truth     [1 0.9]}]))
+       :truth     [1 0.9]
+       :occurence 1}]))
diff --git a/test/nal/test/deriver.clj b/test/nal/test/deriver.clj
index 90637a2..e31e692 100644
--- a/test/nal/test/deriver.clj
+++ b/test/nal/test/deriver.clj
@@ -5,50 +5,94 @@
 
 (deftest test-generate-conclusions
   (is (= (set
-           '({:statement [--> [int-dif chess sport] competition]
-              :truth [0.0 0.81]
-              :task-type :judgement}
+           '({:statement [==> [--> chess [ind-var X]] [--> sport [ind-var X]]]
+              :task-type :judgement
+              :truth [1 0.44751381215469616]}
+              {:statement [==> [--> chess [ind-var X]] [--> sport [ind-var X]]]
+               :task-type :judgement
+               :truth [1 0.44751381215469616]}
               {:statement [conj [--> chess [dep-var Y]] [--> sport [dep-var Y]]]
-               :truth [1.0 0.81]
-               :task-type :judgement}
-              {:statement [--> [int-dif sport chess] competition]
-               :truth [0.0 0.81]
-               :task-type :judgement}
-              {:statement [--> [| chess sport] competition]
-               :truth [1.0 0.81]
-               :task-type :judgement}
-              {:statement [--> chess sport]
-               :truth [1 0.44751381215469616]
-               :task-type :judgement}
+               :task-type :judgement
+               :truth [1.0 0.81]}
+              {:statement [==> [--> sport [ind-var X]] [--> chess [ind-var X]]]
+               :task-type :judgement
+               :truth [1 0.44751381215469616]}
               {:statement [--> sport chess]
-               :truth [1 0.44751381215469616]
-               :task-type :judgement}
-              {:statement [--> [ext-inter chess sport] competition]
-               :truth [1.0 0.81]
-               :task-type :judgement}
+               :task-type :judgement
+               :truth [1 0.44751381215469616]}
               {:statement [<-> sport chess]
-               :truth [1.0 0.44751381215469616]
-               :task-type :judgement}
-              {:statement [==> [--> chess [ind-var X]] [--> sport [ind-var X]]]
-               :truth [1 0.44751381215469616]
-               :task-type :judgement}
-              {:statement [==> [--> sport [ind-var X]] [--> chess [ind-var X]]]
-               :truth [1 0.44751381215469616]
-               :task-type :judgement}
-              {:statement [==> [--> sport [ind-var X]] [--> chess [ind-var X]]]
-               :truth [1 0.44751381215469616]
-               :task-type :judgement}
+               :task-type :judgement
+               :truth [1.0 0.44751381215469616]}
               {:statement [<=> [--> chess [ind-var X]] [--> sport [ind-var X]]]
-               :truth [1.0 0.44751381215469616]
-               :task-type :judgement}
-              {:statement [==> [--> chess [ind-var X]] [--> sport [ind-var X]]]
-               :truth [1 0.44751381215469616]
-               :task-type :judgement}))
+               :task-type :judgement
+               :truth [1.0 0.44751381215469616]}
+              {:statement [--> chess sport]
+               :task-type :judgement
+               :truth [1 0.44751381215469616]}
+              {:statement [==> [--> sport [ind-var X]] [--> chess [ind-var X]]]
+               :task-type :judgement
+               :truth [1 0.44751381215469616]}
+              {:statement [pred-impl
+                           [seq-conj [--> chess [ind-var X]] [:interval 1000]]
+                           [--> sport [ind-var X]]]
+               :task-type :judgement
+               :truth [1 0.44751381215469616]}
+              {:statement [</>
+                           [seq-conj [--> chess [ind-var X]] [:interval 1000]]
+                           [--> sport [ind-var X]]]
+               :task-type :judgement
+               :truth [1.0 0.44751381215469616]}
+              {:statement [seq-conj
+                           [--> chess [dep-var Y]]
+                           [:interval 1000]
+                           [--> sport [dep-var Y]]]
+               :task-type :judgement
+               :truth [1.0 0.81]}
+              {:statement [retro-impl
+                           [--> sport [ind-var X]]
+                           [seq-conj [--> chess [ind-var X]] [:interval 1000]]]
+               :task-type :judgement
+               :truth [1 0.44751381215469616]}
+              {:statement [--> [int-dif sport chess] competition]
+               :task-type :judgement
+               :truth [0.0 0.81]}
+              {:statement [--> [ext-inter chess sport] competition]
+               :task-type :judgement
+               :truth [1.0 0.81]}
+              {:statement [--> [| chess sport] competition]
+               :task-type :judgement
+               :truth [1.0 0.81]}
+              {:statement [--> [int-dif chess sport] competition]
+               :task-type :judgement
+               :truth [0.0 0.81]}
+              {:statement [</>
+                           [seq-conj [--> chess competition] [:interval 1000]]
+                           [--> sport competition]]
+               :task-type :judgement
+               :truth [1.0 0.44751381215469616]}
+              {:statement [seq-conj
+                           [--> chess competition]
+                           [:interval 1000]
+                           [--> sport competition]]
+               :task-type :judgement
+               :truth [1.0 0.81]}
+              {:statement [pred-impl
+                           [seq-conj [--> chess competition] [:interval 1000]]
+                           [--> sport competition]]
+               :task-type :judgement
+               :truth [1 0.44751381215469616]}
+              {:statement [retro-impl
+                           [--> sport competition]
+                           [seq-conj [--> chess competition] [:interval 1000]]]
+               :task-type :judgement
+               :truth [1 0.44751381215469616]}))
          (set (generate-conclusions
                 (r/rules :judgement)
                 '{:statement [--> sport competition]
                   :truth     [1 0.9]
-                  :task-type :judgement}
+                  :task-type :judgement
+                  :occurence 1000}
 
                 '{:statement [--> chess competition]
-                  :truth     [1 0.9]})))))
+                  :truth     [1 0.9]
+                  :occurence 0})))))
diff --git a/test/nal/test/deriver/matching.clj b/test/nal/test/deriver/matching.clj
new file mode 100644
index 0000000..8ab9f94
--- /dev/null
+++ b/test/nal/test/deriver/matching.clj
@@ -0,0 +1,26 @@
+(ns nal.test.deriver.matching
+  (:require [clojure.test :refer :all]
+            [nal.deriver.matching :refer :all]))
+
+(deftest test-quote-operators
+  (are [a1 a2] (= a1 (quote-operators a2))
+    `(let
+        [~'G__57753
+         (nal.deriver.preconditions/abs (- :t-occurence :b-occurence))]
+        [:interval ~'G__57753])
+    `(let
+       [~'G__57753
+        (nal.deriver.preconditions/abs (- :t-occurence :b-occurence))]
+       [:interval ~'G__57753])
+
+    `(let
+       [~'G__57753
+        (nal.deriver.preconditions/abs (- :t-occurence :b-occurence))]
+       [(quote ~'ext-set) ~'G__57753])
+    `(let
+       [~'G__57753
+        (nal.deriver.preconditions/abs (- :t-occurence :b-occurence))]
+       [~'ext-set ~'G__57753])
+
+    '[(quote ext-set) x1 x2]
+    '(ext-set x1 x2)))