diff --git a/nars-dist/Examples/Example-NAL5-edited.txt b/nars-dist/Examples/Example-NAL5-edited.txt
index cba70a2aafbf4aebede249b1e39db5c1ed1b936f..5b19782755c0143fc3d91c6dad3c2ce3ef0cc6d7 100644
--- a/nars-dist/Examples/Example-NAL5-edited.txt
+++ b/nars-dist/Examples/Example-NAL5-edited.txt
@@ -208,7 +208,7 @@
 // It is unlikely that if robin is not a type of bird then robin can fly. 
 <(--,<robin --> [flying]>) ==> <robin --> bird>>?  
 // If robin cannot fly then is robin a type of bird?
-29
+3
  OUT: <(--,<robin --> [flying]>) ==> <robin --> bird>>. %0.00;0.45%
 // I guess it is unlikely that if robin cannot fly then robin is a type of bird.
 
@@ -273,6 +273,6 @@
 // If robin can fly and robin chirps, then robin is a bird
 <<robin --> [flying]> ==> <robin --> [with-beak]>>. %0.90%  
 // If robin can fly then usually robin has a beak.
-18
+22
  OUT: <(&&,<robin --> [chirping]>,<robin --> [with-beak]>) ==> <robin --> bird>>. %1.00;0.42%
 // I guess that if robin chirps and robin has a beak, then robin is a bird.
diff --git a/nars-dist/Examples/Example-NAL5-unedited.txt b/nars-dist/Examples/Example-NAL5-unedited.txt
index 0a06948c134663e2638aa712a49fc9895997e48e..fd00cfcebc6a59295adc4ce367fc2dc6ee569acf 100644
--- a/nars-dist/Examples/Example-NAL5-unedited.txt
+++ b/nars-dist/Examples/Example-NAL5-unedited.txt
@@ -1,4 +1,3 @@
-*****RESET*****
 ********** revision
   IN: <<robin --> [flying]> ==> <robin --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> [flying]> ==> <robin --> bird>>. %0.00;0.60% {0 : 2} 
@@ -19,7 +18,9 @@
 ********** induction
   IN: <<robin --> bird> ==> <robin --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> bird> ==> <robin --> [flying]>>. %0.80;0.90% {0 : 2} 
-14
+2
+ OUT: <(--,<robin --> [flying]>) ==> (--,<robin --> bird>)>. %0.00;0.15% {2 : 2} 
+12
  OUT: <<robin --> bird> ==> (||,<robin --> animal>,<robin --> [flying]>)>. %1.00;0.81% {14 : 1;2} 
  OUT: <<robin --> bird> ==> (&&,<robin --> animal>,<robin --> [flying]>)>. %0.80;0.81% {14 : 1;2} 
  OUT: <<robin --> [flying]> ==> <robin --> animal>>. %1.00;0.39% {14 : 1;2} 
@@ -28,7 +29,11 @@
 ********** abduction
   IN: <<robin --> bird> ==> <robin --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> [flying]> ==> <robin --> animal>>. %0.80;0.90% {0 : 2} 
-19
+2
+ OUT: <(--,<robin --> animal>) ==> (--,<robin --> [flying]>)>. %0.00;0.15% {2 : 2} 
+16
+ OUT: <(--,<robin --> animal>) ==> (--,<robin --> [flying]>)>. %0.00;0.15% {18 : 2} 
+1
  OUT: <(&&,<robin --> bird>,<robin --> [flying]>) ==> <robin --> animal>>. %1.00;0.81% {19 : 1;2} 
  OUT: <(||,<robin --> bird>,<robin --> [flying]>) ==> <robin --> animal>>. %0.80;0.81% {19 : 1;2} 
  OUT: <<robin --> bird> ==> <robin --> [flying]>>. %1.00;0.39% {19 : 1;2} 
@@ -47,7 +52,9 @@
 ********** comparison
   IN: <<robin --> bird> ==> <robin --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> bird> ==> <robin --> [flying]>>. %0.80;0.90% {0 : 2} 
-14
+2
+ OUT: <(--,<robin --> [flying]>) ==> (--,<robin --> bird>)>. %0.00;0.15% {2 : 2} 
+12
  OUT: <<robin --> bird> ==> (||,<robin --> animal>,<robin --> [flying]>)>. %1.00;0.81% {14 : 1;2} 
  OUT: <<robin --> bird> ==> (&&,<robin --> animal>,<robin --> [flying]>)>. %0.80;0.81% {14 : 1;2} 
  OUT: <<robin --> [flying]> ==> <robin --> animal>>. %1.00;0.39% {14 : 1;2} 
@@ -56,7 +63,9 @@
 ********** comparison
   IN: <<robin --> bird> ==> <robin --> animal>>. %0.70;0.90% {0 : 1} 
   IN: <<robin --> [flying]> ==> <robin --> animal>>. %1.00;0.90% {0 : 2} 
-19
+14
+ OUT: <(--,<robin --> animal>) ==> (--,<robin --> bird>)>. %0.00;0.21% {14 : 1} 
+5
  OUT: <(&&,<robin --> bird>,<robin --> [flying]>) ==> <robin --> animal>>. %1.00;0.81% {19 : 1;2} 
  OUT: <(||,<robin --> bird>,<robin --> [flying]>) ==> <robin --> animal>>. %0.70;0.81% {19 : 1;2} 
  OUT: <<robin --> bird> ==> <robin --> [flying]>>. %0.70;0.45% {19 : 1;2} 
@@ -80,12 +89,16 @@
 ********** conversions between Implication and Equivalence
   IN: <<robin --> [flying]> ==> <robin --> bird>>. %0.90;0.90% {0 : 1} 
   IN: <<robin --> bird> ==> <robin --> [flying]>>. %0.90;0.90% {0 : 2} 
-7
+2
+ OUT: <(--,<robin --> [flying]>) ==> (--,<robin --> bird>)>. %0.00;0.08% {2 : 2} 
+5
  OUT: <<robin --> bird> <=> <robin --> [flying]>>. %0.81;0.81% {7 : 1;2} 
 ********** compound composition, two premises
   IN: <<robin --> bird> ==> <robin --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> bird> ==> <robin --> [flying]>>. %0.90;0.90% {0 : 2} 
-14
+2
+ OUT: <(--,<robin --> [flying]>) ==> (--,<robin --> bird>)>. %0.00;0.08% {2 : 2} 
+12
  OUT: <<robin --> bird> ==> (||,<robin --> animal>,<robin --> [flying]>)>. %1.00;0.81% {14 : 1;2} 
  OUT: <<robin --> bird> ==> (&&,<robin --> animal>,<robin --> [flying]>)>. %0.90;0.81% {14 : 1;2} 
  OUT: <<robin --> [flying]> ==> <robin --> animal>>. %1.00;0.42% {14 : 1;2} 
@@ -94,7 +107,11 @@
 ********** compound composition, two premises
   IN: <<robin --> bird> ==> <robin --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> [flying]> ==> <robin --> animal>>. %0.90;0.90% {0 : 2} 
-19
+2
+ OUT: <(--,<robin --> animal>) ==> (--,<robin --> [flying]>)>. %0.00;0.08% {2 : 2} 
+16
+ OUT: <(--,<robin --> animal>) ==> (--,<robin --> [flying]>)>. %0.00;0.08% {18 : 2} 
+1
  OUT: <(&&,<robin --> bird>,<robin --> [flying]>) ==> <robin --> animal>>. %1.00;0.81% {19 : 1;2} 
  OUT: <(||,<robin --> bird>,<robin --> [flying]>) ==> <robin --> animal>>. %0.90;0.81% {19 : 1;2} 
  OUT: <<robin --> bird> ==> <robin --> [flying]>>. %1.00;0.42% {19 : 1;2} 
@@ -106,6 +123,7 @@
 8
  OUT: <<robin --> bird> ==> <robin --> animal>>. %0.00;0.81% {8 : 1;2} 
  OUT: <robin --> animal>. %0.00;0.45% {8 : 1;2} 
+ OUT: <(--,(&&,<robin --> animal>,<robin --> [flying]>)) ==> (--,<robin --> bird>)>. %0.00;0.47% {8 : 1} 
 ********** compound decomposition, two premises
   IN: (&&,<robin --> swimmer>,<robin --> [flying]>). %0.00;0.90% {0 : 1} 
   IN: <robin --> [flying]>. %1.00;0.90% {0 : 2} 
@@ -155,12 +173,8 @@
 ********** contraposition
   IN: <(--,<robin --> bird>) ==> <robin --> [flying]>>. %0.10;0.90% {0 : 1} 
   IN: <(--,<robin --> [flying]>) ==> <robin --> bird>>?  {0 : 2} 
-8
- OUT: <(--,<robin --> [flying]>) ==> <robin --> bird>>?  {8 : 1} 
-16
- OUT: <(--,<robin --> bird>) ==> <robin --> [flying]>>?  {24 : 1} 
- OUT: <(--,<robin --> bird>) ==> <robin --> [flying]>>?  {24 : 1} 
- OUT: <(--,<robin --> bird>) ==> <robin --> [flying]>>?  {24 : 1} 
+3
+ OUT: <(--,<robin --> [flying]>) ==> <robin --> bird>>. %0.00;0.45% {3 : 1} 
 ********** conditional deduction
   IN: <(&&,<robin --> [flying]>,<robin --> [with-wings]>) ==> <robin --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <robin --> [flying]>. %1.00;0.90% {0 : 2} 
@@ -190,11 +204,17 @@
 ********** conditional abduction
   IN: <(&&,<robin --> [flying]>,<robin --> [with-wings]>) ==> <robin --> [living]>>. %0.90;0.90% {0 : 1} 
   IN: <(&&,<robin --> bird>,<robin --> [flying]>) ==> <robin --> [living]>>. %1.00;0.90% {0 : 2} 
-18
+13
+ OUT: <(--,<robin --> [living]>) ==> (--,(&&,<robin --> [flying]>,<robin --> [with-wings]>))>. %0.00;0.08% {13 : 1} 
+5
  OUT: <<robin --> bird> ==> <robin --> [with-wings]>>. %1.00;0.42% {18 : 1;2} 
  OUT: <<robin --> [with-wings]> ==> <robin --> bird>>. %0.90;0.45% {18 : 1;2} 
 ********** conditional induction
   IN: <(&&,<robin --> [chirping]>,<robin --> [flying]>) ==> <robin --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> [flying]> ==> <robin --> [with-beak]>>. %0.90;0.90% {0 : 2} 
-18
- OUT: <(&&,<robin --> [chirping]>,<robin --> [with-beak]>) ==> <robin --> bird>>. %1.00;0.42% {18 : 2;1} 
+2
+ OUT: <(--,<robin --> [with-beak]>) ==> (--,<robin --> [flying]>)>. %0.00;0.08% {2 : 2} 
+11
+ OUT: <(--,<robin --> [with-beak]>) ==> (--,<robin --> [flying]>)>. %0.00;0.08% {13 : 2} 
+9
+ OUT: <(&&,<robin --> [chirping]>,<robin --> [with-beak]>) ==> <robin --> bird>>. %1.00;0.42% {22 : 2;1} 
diff --git a/nars-dist/Examples/Example-NAL6-edited.txt b/nars-dist/Examples/Example-NAL6-edited.txt
index a64d15274d3728c50f5ffeef3daf0aefa5437e86..5f7592bfdefa491a36cb85d437fd166939f54b0c 100644
--- a/nars-dist/Examples/Example-NAL6-edited.txt
+++ b/nars-dist/Examples/Example-NAL6-edited.txt
@@ -234,3 +234,47 @@
  OUT: <<$1 --> lock> ==> (&&,<#2 --> key>,<$1 --> (/,open,#2,_)>)>. %1.00;0.45% 
 // I guess every lock can be opened by some key.
 
+***** second level variable unification
+  IN: (&&,<#1 --> lock>,<<$2 --> key> ==> <#1 --> (/,open,$2,_)>>). %1.00;0.90% 
+//there is a lock which is opened by all keys
+  IN: <{key1} --> key>. %1.00;0.90% 
+//key1 is a key
+5
+ OUT: (&&,<#1 --> lock>,<#1 --> (/,open,{key1},_)>). %1.00;0.81%
+//there is a lock which is opened by key1
+
+***** second level variable unification
+  IN: <<$1 --> lock> ==> (&&,<#2 --> key>,<$1 --> (/,open,#2,_)>)>. %1.00;0.90% 
+//all locks are opened by some key
+  IN: <{key1} --> key>. %1.00;0.90% 
+//key1 is a key
+5
+ OUT: <<$1 --> lock> ==> <$1 --> (/,open,{key1},_)>>. %1.00;0.43%  
+//maybe all locks are opened by key1
+
+***** second variable introduction (induction)
+  IN: <<lock1 --> (/,open,$1,_)> ==> <$1 --> key>>.
+//if something opens lock1, it is a key
+  IN: <lock1 --> lock>.
+//lock1 is a key
+7
+ OUT: <(&&,<#1 --> lock>,<#1 --> (/,open,$2,_)>) ==> <$2 --> key>>. %1.00;0.45%
+//there is a lock with the property that when opened by something, this something is a key (induction)
+
+***** variable elimination (deduction)
+  IN: <lock1 --> lock>. %1.00;0.90%
+//lock1 is a lock
+  IN: <(&&,<#1 --> lock>,<#1 --> (/,open,$2,_)>) ==> <$2 --> key>>. %1.00;0.90% 
+//there is a lock with the property that when opened by something, this something is a key
+4
+ OUT: <<lock1 --> (/,open,$1,_)> ==> <$1 --> key>>. %1.00;0.43%
+//whatever opens lock1 is a key
+
+***** abduction with variable elimination (abduction)
+  IN: <<lock1 --> (/,open,$1,_)> ==> <$1 --> key>>. %1.00;0.90% {0 : 1} 
+//whatever opens lock1 is a key
+  IN: <(&&,<#1 --> lock>,<#1 --> (/,open,$2,_)>) ==> <$2 --> key>>. %1.00;0.90% {0 : 2} 
+//there is a lock with the property that when opened by something, this something is a key
+10
+ OUT: <lock1 --> lock>. %1.00;0.45% {10 : 1;2} 
+//lock1 is a lock
diff --git a/nars-dist/Examples/Example-NAL6-unedited.txt b/nars-dist/Examples/Example-NAL6-unedited.txt
index b08019c3762c70d103350feeab077fe81de8e3a0..706024778c0e529eb2cc5e506b9c0e33fc9591d6 100644
--- a/nars-dist/Examples/Example-NAL6-unedited.txt
+++ b/nars-dist/Examples/Example-NAL6-unedited.txt
@@ -151,7 +151,6 @@
 3
  OUT: (&&,<#1 --> lock>,<<$2 --> key> ==> <#1 --> (/,open,$2,_)>>). %1.00;0.81% {15 : 1;2} 
  OUT: <(&&,<$1 --> key>,<$2 --> lock>) ==> <$2 --> (/,open,$1,_)>>. %1.00;0.45% {15 : 1;2} 
- OUT: <<$1 --> key> ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.45% {15 : 1;2} 
 ********** multiple variables introduction
   IN: (&&,<#1 --> key>,<{lock1} --> (/,open,#1,_)>). %1.00;0.90% {0 : 1} 
   IN: <{lock1} --> lock>. %1.00;0.90% {0 : 2} 
@@ -162,3 +161,40 @@
 3
  OUT: (&&,<#1 --> key>,<#2 --> lock>,<#2 --> (/,open,#1,_)>). %1.00;0.81% {15 : 1;2} 
  OUT: <<$1 --> lock> ==> (&&,<#2 --> key>,<$1 --> (/,open,#2,_)>)>. %1.00;0.45% {15 : 1;2} 
+***** second level variable unification
+  IN: (&&,<#1 --> lock>,<<$2 --> key> ==> <#1 --> (/,open,$2,_)>>). %1.00;0.90% {0 : 1} 
+  IN: <{key1} --> key>. %1.00;0.90% {0 : 2} 
+5
+ OUT: (&&,<#1 --> lock>,<#1 --> (/,open,{key1},_)>). %1.00;0.81% {5 : 2;1} 
+***** second level variable unification
+  IN: <<$1 --> lock> ==> (&&,<#2 --> key>,<$1 --> (/,open,#2,_)>)>. %1.00;0.90% {0 : 1} 
+  IN: <{key1} --> key>. %1.00;0.90% {0 : 2} 
+5
+ OUT: <<$1 --> lock> ==> <$1 --> (/,open,{key1},_)>>. %1.00;0.43% {5 : 2;1} 
+***** second variable introduction (induction)
+  IN: <<lock1 --> (/,open,$1,_)> ==> <$1 --> key>>. %1.00;0.90% {0 : 1} 
+  IN: <lock1 --> lock>. %1.00;0.90% {0 : 2} 
+2
+ OUT: <<(*,$1,lock1) --> open> ==> <$1 --> key>>. %1.00;0.90% {2 : 1} 
+5
+ OUT: <(&&,<#1 --> lock>,<#1 --> (/,open,$2,_)>) ==> <$2 --> key>>. %1.00;0.45% {7 : 1;2} 
+***** variable elimination (deduction)
+  IN: <lock1 --> lock>. %1.00;0.90% {0 : 1} 
+  IN: <(&&,<#1 --> lock>,<#1 --> (/,open,$2,_)>) ==> <$2 --> key>>. %1.00;0.90% {0 : 2} 
+2
+ OUT: <(&&,<#1 --> lock>,<(*,$2,#1) --> open>) ==> <$2 --> key>>. %1.00;0.90% {2 : 2} 
+2
+ OUT: <<lock1 --> (/,open,$1,_)> ==> <$1 --> key>>. %1.00;0.43% {4 : 1;2} 
+***** abduction with variable elimination (abduction)
+  IN: <<lock1 --> (/,open,$1,_)> ==> <$1 --> key>>. %1.00;0.90% {0 : 1} 
+  IN: <(&&,<#1 --> lock>,<#1 --> (/,open,$2,_)>) ==> <$2 --> key>>. %1.00;0.90% {0 : 2} 
+5
+ OUT: <<(*,$1,lock1) --> open> ==> <$1 --> key>>. %1.00;0.90% {5 : 1} 
+5
+ OUT: <(&&,<#1 --> lock>,<#1 --> (/,open,$2,_)>,<lock1 --> (/,open,$3,_)>) ==> <$3 --> key>>. %1.00;0.81% {10 : 1;2} 
+ OUT: <(||,(&&,<#1 --> lock>,<#1 --> (/,open,$2,_)>),<lock1 --> (/,open,$3,_)>) ==> <$3 --> key>>. %1.00;0.81% {10 : 1;2} 
+ OUT: <<lock1 --> (/,open,$1,_)> ==> (&&,<#2 --> lock>,<#2 --> (/,open,$3,_)>)>. %1.00;0.45% {10 : 1;2} 
+ OUT: <(&&,<#1 --> lock>,<#1 --> (/,open,$2,_)>) ==> <lock1 --> (/,open,$3,_)>>. %1.00;0.45% {10 : 1;2} 
+ OUT: <(&&,<#1 --> lock>,<#1 --> (/,open,$2,_)>) <=> <lock1 --> (/,open,$3,_)>>. %1.00;0.45% {10 : 1;2} 
+ OUT: <lock1 --> lock>. %1.00;0.45% {10 : 1;2} 
+ OUT: <lock1 --> (/,open,$1,_)>. %1.00;0.45% {10 : 1;2} 
diff --git a/nars-dist/NARS.jar b/nars-dist/NARS.jar
index b7901076317e1ddacd759a63dd284be17fbd57ad..a48a9ec4f5d4ebe7b45d2dced7b84391e50b8c6d 100644
Binary files a/nars-dist/NARS.jar and b/nars-dist/NARS.jar differ