diff --git a/nars-dist/Examples/Example-NAL5-unedited.txt b/nars-dist/Examples/Example-NAL5-unedited.txt
index 163d79c5a4a3f15c8a45e18615ea3894318c2627..0a06948c134663e2638aa712a49fc9895997e48e 100644
--- a/nars-dist/Examples/Example-NAL5-unedited.txt
+++ b/nars-dist/Examples/Example-NAL5-unedited.txt
@@ -1,71 +1,72 @@
+*****RESET*****
 ********** revision
   IN: <<robin --> [flying]> ==> <robin --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> [flying]> ==> <robin --> bird>>. %0.00;0.60% {0 : 2} 
 1
- OUT: <<robin --> [flying]> ==> <robin --> bird>>. %0.86;0.91% {1 : 1;2} 
+ OUT: <<robin --> [flying]> ==> <robin --> bird>>. %0.86;0.91% {1 : 2;1} 
 ********** deduction
   IN: <<robin --> bird> ==> <robin --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> [flying]> ==> <robin --> bird>>. %1.00;0.90% {0 : 2} 
 14
- OUT: <<robin --> [flying]> ==> <robin --> animal>>. %1.00;0.81% {1 : 2;1} 
- OUT: <<robin --> animal> ==> <robin --> [flying]>>. %1.00;0.45% {1 : 2;1} 
+ OUT: <<robin --> [flying]> ==> <robin --> animal>>. %1.00;0.81% {14 : 1;2} 
+ OUT: <<robin --> animal> ==> <robin --> [flying]>>. %1.00;0.45% {14 : 1;2} 
 ********** exemplification
   IN: <<robin --> [flying]> ==> <robin --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> bird> ==> <robin --> animal>>. %1.00;0.90% {0 : 2} 
 19
- OUT: <<robin --> [flying]> ==> <robin --> animal>>. %1.00;0.81% {1 : 2;1} 
- OUT: <<robin --> animal> ==> <robin --> [flying]>>. %1.00;0.45% {1 : 2;1} 
+ OUT: <<robin --> [flying]> ==> <robin --> animal>>. %1.00;0.81% {19 : 1;2} 
+ OUT: <<robin --> animal> ==> <robin --> [flying]>>. %1.00;0.45% {19 : 1;2} 
 ********** induction
   IN: <<robin --> bird> ==> <robin --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> bird> ==> <robin --> [flying]>>. %0.80;0.90% {0 : 2} 
 14
- OUT: <<robin --> bird> ==> (||,<robin --> animal>,<robin --> [flying]>)>. %1.00;0.81% {1 : 2;1} 
- OUT: <<robin --> bird> ==> (&&,<robin --> animal>,<robin --> [flying]>)>. %0.80;0.81% {1 : 2;1} 
- OUT: <<robin --> [flying]> ==> <robin --> animal>>. %1.00;0.39% {1 : 2;1} 
- OUT: <<robin --> animal> ==> <robin --> [flying]>>. %0.80;0.45% {1 : 2;1} 
- OUT: <<robin --> animal> <=> <robin --> [flying]>>. %0.80;0.45% {1 : 2;1} 
+ 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} 
+ OUT: <<robin --> animal> ==> <robin --> [flying]>>. %0.80;0.45% {14 : 1;2} 
+ OUT: <<robin --> animal> <=> <robin --> [flying]>>. %0.80;0.45% {14 : 1;2} 
 ********** abduction
   IN: <<robin --> bird> ==> <robin --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> [flying]> ==> <robin --> animal>>. %0.80;0.90% {0 : 2} 
 19
- OUT: <(&&,<robin --> bird>,<robin --> [flying]>) ==> <robin --> animal>>. %1.00;0.81% {1 : 2;1} 
- OUT: <(||,<robin --> bird>,<robin --> [flying]>) ==> <robin --> animal>>. %0.80;0.81% {1 : 2;1} 
- OUT: <<robin --> bird> ==> <robin --> [flying]>>. %1.00;0.39% {1 : 2;1} 
- OUT: <<robin --> [flying]> ==> <robin --> bird>>. %0.80;0.45% {1 : 2;1} 
- OUT: <<robin --> bird> <=> <robin --> [flying]>>. %0.80;0.45% {1 : 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} 
+ OUT: <<robin --> [flying]> ==> <robin --> bird>>. %0.80;0.45% {19 : 1;2} 
+ OUT: <<robin --> bird> <=> <robin --> [flying]>>. %0.80;0.45% {19 : 1;2} 
 ********** detachment
   IN: <<robin --> bird> ==> <robin --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <robin --> bird>. %1.00;0.90% {0 : 2} 
 1
- OUT: <robin --> animal>. %1.00;0.81% {1 : 1;2} 
+ OUT: <robin --> animal>. %1.00;0.81% {1 : 2;1} 
 ********** detachment
   IN: <<robin --> bird> ==> <robin --> animal>>. %0.70;0.90% {0 : 1} 
   IN: <robin --> animal>. %1.00;0.90% {0 : 2} 
 1
- OUT: <robin --> bird>. %1.00;0.36% {1 : 1;2} 
+ OUT: <robin --> bird>. %1.00;0.36% {1 : 2;1} 
 ********** comparison
   IN: <<robin --> bird> ==> <robin --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> bird> ==> <robin --> [flying]>>. %0.80;0.90% {0 : 2} 
 14
- OUT: <<robin --> bird> ==> (||,<robin --> animal>,<robin --> [flying]>)>. %1.00;0.81% {1 : 2;1} 
- OUT: <<robin --> bird> ==> (&&,<robin --> animal>,<robin --> [flying]>)>. %0.80;0.81% {1 : 2;1} 
- OUT: <<robin --> [flying]> ==> <robin --> animal>>. %1.00;0.39% {1 : 2;1} 
- OUT: <<robin --> animal> ==> <robin --> [flying]>>. %0.80;0.45% {1 : 2;1} 
- OUT: <<robin --> animal> <=> <robin --> [flying]>>. %0.80;0.45% {1 : 2;1} 
+ 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} 
+ OUT: <<robin --> animal> ==> <robin --> [flying]>>. %0.80;0.45% {14 : 1;2} 
+ OUT: <<robin --> animal> <=> <robin --> [flying]>>. %0.80;0.45% {14 : 1;2} 
 ********** comparison
   IN: <<robin --> bird> ==> <robin --> animal>>. %0.70;0.90% {0 : 1} 
   IN: <<robin --> [flying]> ==> <robin --> animal>>. %1.00;0.90% {0 : 2} 
 19
- OUT: <(&&,<robin --> bird>,<robin --> [flying]>) ==> <robin --> animal>>. %1.00;0.81% {1 : 2;1} 
- OUT: <(||,<robin --> bird>,<robin --> [flying]>) ==> <robin --> animal>>. %0.70;0.81% {1 : 2;1} 
- OUT: <<robin --> bird> ==> <robin --> [flying]>>. %0.70;0.45% {1 : 2;1} 
- OUT: <<robin --> [flying]> ==> <robin --> bird>>. %1.00;0.36% {1 : 2;1} 
- OUT: <<robin --> bird> <=> <robin --> [flying]>>. %0.70;0.45% {1 : 2;1} 
+ 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} 
+ OUT: <<robin --> [flying]> ==> <robin --> bird>>. %1.00;0.36% {19 : 1;2} 
+ OUT: <<robin --> bird> <=> <robin --> [flying]>>. %0.70;0.45% {19 : 1;2} 
 ********** analogy
   IN: <<robin --> bird> ==> <robin --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> bird> <=> <robin --> [flying]>>. %0.80;0.90% {0 : 2} 
 14
- OUT: <<robin --> [flying]> ==> <robin --> animal>>. %0.80;0.65% {1 : 2;1} 
+ OUT: <<robin --> [flying]> ==> <robin --> animal>>. %0.80;0.65% {14 : 1;2} 
 ********** analogy
   IN: <robin --> bird>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> bird> <=> <robin --> [flying]>>. %0.80;0.90% {0 : 2} 
@@ -75,97 +76,96 @@
   IN: <<robin --> animal> <=> <robin --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> bird> <=> <robin --> [flying]>>. %0.90;0.90% {0 : 2} 
 19
- OUT: <<robin --> animal> <=> <robin --> [flying]>>. %0.90;0.81% {1 : 2;1} 
+ OUT: <<robin --> animal> <=> <robin --> [flying]>>. %0.90;0.81% {19 : 1;2} 
 ********** 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
- OUT: <<robin --> bird> <=> <robin --> [flying]>>. %0.81;0.81% {1 : 2;1} 
+ 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
- OUT: <<robin --> bird> ==> (||,<robin --> animal>,<robin --> [flying]>)>. %1.00;0.81% {1 : 2;1} 
- OUT: <<robin --> bird> ==> (&&,<robin --> animal>,<robin --> [flying]>)>. %0.90;0.81% {1 : 2;1} 
- OUT: <<robin --> [flying]> ==> <robin --> animal>>. %1.00;0.42% {1 : 2;1} 
- OUT: <<robin --> animal> ==> <robin --> [flying]>>. %0.90;0.45% {1 : 2;1} 
- OUT: <<robin --> animal> <=> <robin --> [flying]>>. %0.90;0.45% {1 : 2;1} 
+ 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} 
+ OUT: <<robin --> animal> ==> <robin --> [flying]>>. %0.90;0.45% {14 : 1;2} 
+ OUT: <<robin --> animal> <=> <robin --> [flying]>>. %0.90;0.45% {14 : 1;2} 
 ********** 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
- OUT: <(&&,<robin --> bird>,<robin --> [flying]>) ==> <robin --> animal>>. %1.00;0.81% {1 : 2;1} 
- OUT: <(||,<robin --> bird>,<robin --> [flying]>) ==> <robin --> animal>>. %0.90;0.81% {1 : 2;1} 
- OUT: <<robin --> bird> ==> <robin --> [flying]>>. %1.00;0.42% {1 : 2;1} 
- OUT: <<robin --> [flying]> ==> <robin --> bird>>. %0.90;0.45% {1 : 2;1} 
- OUT: <<robin --> bird> <=> <robin --> [flying]>>. %0.90;0.45% {1 : 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} 
+ OUT: <<robin --> [flying]> ==> <robin --> bird>>. %0.90;0.45% {19 : 1;2} 
+ OUT: <<robin --> bird> <=> <robin --> [flying]>>. %0.90;0.45% {19 : 1;2} 
 ********** compound decomposition, two premises
   IN: <<robin --> bird> ==> (&&,<robin --> animal>,<robin --> [flying]>)>. %0.00;0.90% {0 : 1} 
   IN: <<robin --> bird> ==> <robin --> [flying]>>. %1.00;0.90% {0 : 2} 
 8
- OUT: <<robin --> bird> ==> <robin --> animal>>. %0.00;0.81% {1 : 2;1} 
+ OUT: <<robin --> bird> ==> <robin --> animal>>. %0.00;0.81% {8 : 1;2} 
+ OUT: <robin --> animal>. %0.00;0.45% {8 : 1;2} 
 ********** compound decomposition, two premises
   IN: (&&,<robin --> swimmer>,<robin --> [flying]>). %0.00;0.90% {0 : 1} 
   IN: <robin --> [flying]>. %1.00;0.90% {0 : 2} 
 6
- OUT: <robin --> swimmer>. %0.00;0.81% {4 : 2;1} 
+ OUT: <robin --> swimmer>. %0.00;0.81% {6 : 1;2} 
 ********** compound decomposition, two premises
   IN: (||,<robin --> swimmer>,<robin --> [flying]>). %1.00;0.90% {0 : 1} 
   IN: <robin --> swimmer>. %0.00;0.90% {0 : 2} 
 2
- OUT: <robin --> [flying]>. %1.00;0.81% {1 : 1;2} 
+ OUT: <robin --> [flying]>. %1.00;0.81% {2 : 2;1} 
 ********** compound composition, one premises
   IN: <robin --> [flying]>. %1.00;0.90% {0 : 1} 
   IN: (||,<robin --> swimmer>,<robin --> [flying]>)?  {0 : 2} 
 1
  OUT: <robin --> swimmer>?  {1 : 2} 
 2
- OUT: <[flying] --> swimmer>?  {3 : 1;2} 
- OUT: <swimmer --> [flying]>?  {3 : 1;2} 
- OUT: <swimmer <-> [flying]>?  {3 : 1;2} 
+ OUT: <[flying] --> swimmer>?  {3 : 2;1} 
+ OUT: <swimmer --> [flying]>?  {3 : 2;1} 
+ OUT: <swimmer <-> [flying]>?  {3 : 2;1} 
 2
- OUT: <robin --> swimmer>?  {5 : 1;2} 
+ OUT: <robin --> swimmer>?  {5 : 2;1} 
 1
  OUT: (||,<robin --> swimmer>,<robin --> [flying]>). %1.00;0.81% {6 : 1} 
 ********** compound decomposition, one premises
   IN: (&&,<robin --> swimmer>,<robin --> [flying]>). %0.90;0.90% {0 : 1} 
 1
- OUT: <robin --> swimmer>. %0.90;0.73% {2 : 1} 
+ OUT: <robin --> swimmer>. %0.90;0.73% {1 : 1} 
 3
- OUT: <robin --> [flying]>. %0.90;0.73% {8 : 1} 
+ OUT: <robin --> [flying]>. %0.90;0.73% {4 : 1} 
 ********** negation
   IN: (--,<robin --> [flying]>). %0.10;0.90% {0 : 1} 
 3
- OUT: <robin --> [flying]>. %0.90;0.90% {1 : 1} 
+ OUT: <robin --> [flying]>. %0.90;0.90% {3 : 1} 
 ********** negation
   IN: <robin --> [flying]>. %0.90;0.90% {0 : 1} 
   IN: (--,<robin --> [flying]>)?  {0 : 2} 
 1
- OUT: <robin --> [flying]>?  {1 : 1 : <robin --> [flying]>} 
+ OUT: <robin --> [flying]>?  {1 : 1} 
  OUT: <robin --> [flying]>?  {1 : 2} 
  OUT: <robin --> [flying]>?  {1 : 2} 
 11
  OUT: <robin --> [flying]>?  {12 : 2} 
  OUT: <robin --> [flying]>?  {12 : 2} 
- OUT: <robin --> [flying]>?  {12 : 1 : <robin --> [flying]>} 
+ OUT: <robin --> [flying]>?  {12 : 1} 
 3
  OUT: (--,<robin --> [flying]>). %0.10;0.90% {15 : 1} 
 ********** 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 : <(--,<robin --> bird>) ==> <robin --> [flying]>>} 
+ OUT: <(--,<robin --> [flying]>) ==> <robin --> bird>>?  {8 : 1} 
 16
- OUT: <(--,<robin --> bird>) ==> <robin --> [flying]>>?  {24 : 1 : <(--,<robin --> bird>) ==> <robin --> [flying]>>} 
- OUT: <(--,<robin --> bird>) ==> <robin --> [flying]>>?  {24 : 1 : <(--,<robin --> bird>) ==> <robin --> [flying]>>} 
- OUT: <(--,<robin --> bird>) ==> <robin --> [flying]>>?  {24 : 1 : <(--,<robin --> bird>) ==> <robin --> [flying]>>} 
-5
- OUT: <(--,<robin --> [flying]>) ==> <robin --> bird>>. %0.00;0.45%
+ OUT: <(--,<robin --> bird>) ==> <robin --> [flying]>>?  {24 : 1} 
+ OUT: <(--,<robin --> bird>) ==> <robin --> [flying]>>?  {24 : 1} 
+ OUT: <(--,<robin --> bird>) ==> <robin --> [flying]>>?  {24 : 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} 
 1
- OUT: <<robin --> [with-wings]> ==> <robin --> bird>>. %1.00;0.81% {3 : 2;1} 
+ OUT: <<robin --> [with-wings]> ==> <robin --> bird>>. %1.00;0.81% {1 : 2;1} 
 ********** conditional deduction
   IN: <(&&,<robin --> [chirping]>,<robin --> [flying]>,<robin --> [with-wings]>) ==> <robin --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <robin --> [flying]>. %1.00;0.90% {0 : 2} 
@@ -175,25 +175,26 @@
   IN: <(&&,<robin --> bird>,<robin --> [living]>) ==> <robin --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <<robin --> [flying]> ==> <robin --> bird>>. %1.00;0.90% {0 : 2} 
 1
- OUT: <(&&,<robin --> [flying]>,<robin --> [living]>) ==> <robin --> animal>>. %1.00;0.81% {14 : 2;1} 
+ OUT: <(&&,<robin --> [flying]>,<robin --> [living]>) ==> <robin --> animal>>. %1.00;0.81% {1 : 1;2} 
 ********** conditional abduction
   IN: <<robin --> [flying]> ==> <robin --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <(&&,<robin --> swimmer>,<robin --> [flying]>) ==> <robin --> bird>>. %1.00;0.90% {0 : 2} 
 7
- OUT: <robin --> swimmer>. %1.00;0.45% {15 : 1;2} 
+ OUT: <robin --> swimmer>. %1.00;0.45% {7 : 2;1} 
+ OUT: <robin --> swimmer>. %1.00;0.45% {7 : 2;1} 
 ********** conditional abduction
   IN: <(&&,<robin --> [chirping]>,<robin --> [with-wings]>) ==> <robin --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <(&&,<robin --> [chirping]>,<robin --> [flying]>,<robin --> [with-wings]>) ==> <robin --> bird>>. %1.00;0.90% {0 : 2} 
 5
- OUT: <robin --> [flying]>. %1.00;0.45% {8 : 1;2} 
+ OUT: <robin --> [flying]>. %1.00;0.45% {5 : 2;1} 
 ********** 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
- OUT: <<robin --> bird> ==> <robin --> [with-wings]>>. %1.00;0.42% {8 : 2;1} 
- OUT: <<robin --> [with-wings]> ==> <robin --> bird>>. %0.90;0.45% {8 : 2;1} 
+ 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% {11 : 1;2} 
+ OUT: <(&&,<robin --> [chirping]>,<robin --> [with-beak]>) ==> <robin --> bird>>. %1.00;0.42% {18 : 2;1} 
diff --git a/nars-dist/Examples/Example-NAL6-edited.txt b/nars-dist/Examples/Example-NAL6-edited.txt
index 72908d86ffc16097819aaf8c3f1c8fba5a26cfbe..a64d15274d3728c50f5ffeef3daf0aefa5437e86 100644
--- a/nars-dist/Examples/Example-NAL6-edited.txt
+++ b/nars-dist/Examples/Example-NAL6-edited.txt
@@ -57,7 +57,7 @@
 // If something can fly and chirp, then it is a bird.
 <<$y --> [with-wings]> ==> <$y --> flyer>>. 
 // If something has wings, then it can fly.
-8
+4
  OUT: <(&&,<$1 --> [chirping]>,<$1 --> [with-wings]>) ==> <$1 --> bird>>. %1.00;0.81% 
 // If something can chirp and has wings, then it is a bird.
 
@@ -66,7 +66,7 @@
 // If something can fly, chirp, and eats worms, then it is a bird.
 <(&&,<$y --> [chirping]>,<$y --> [with-wings]>) ==> <$y --> bird>>.
 // If something can chirp and has wings, then it is a bird.
-6
+10
  OUT: <(&&,<$1 --> flyer>,<(*,$1,worms) --> food>) ==> <$1 --> [with-wings]>>. %1.00;0.45%  
 // If something can fly and eats worms, then I guess it has wings.
  OUT: <<$1 --> [with-wings]> ==> (&&,<$1 --> flyer>,<(*,$1,worms) --> food>)>. %1.00;0.45% 
@@ -77,7 +77,7 @@
 // If something can fly and eats worms, then it is a bird.
 <<$y --> flyer> ==> <$y --> [with-wings]>>.
 // If something can fly, then it has wings.
-4
+12
  OUT: <(&&,<$1 --> [with-wings]>,<worms --> (/,food,$1,_)>) ==> <$1 --> bird>>. %1.00;0.45% 
 // If something has wings and eats worms, then I guess it is a bird.
 
@@ -122,7 +122,7 @@
 // Tweety has wings.
 <(&&,<$x --> [chirping]>,<$x --> [with-wings]>) ==> <$x --> bird>>.
 // If something can chirp and has wings, then it is a bird.
-23
+6
  OUT: <<{Tweety} --> [chirping]> ==> <{Tweety} --> bird>>. %1.00;0.81%
 // If Tweety can chirp, then it is a bird.
 
@@ -131,8 +131,8 @@
 // If something can fly, chirp, and eats worms, then it is a bird.
 <{Tweety} --> flyer>.
 // Tweety can fly.
-7
- OUT: <(&&,<(*,{Tweety},worms) --> food>,<{Tweety} --> [chirping]>) ==> <{Tweety} --> bird>>. %1.00;0.81%
+3
+ OUT: <(&&,<{Tweety} --> [chirping]>,<(*,{Tweety},worms) --> food>) ==> <{Tweety} --> bird>>. %1.00;0.81%
 // If Tweety can chirp and eats worms, then it is a bird.
 
 ********** multiple variable elimination
@@ -140,7 +140,7 @@
 // Every lock can be opened by every key.
 <{lock1} --> lock>. 
 // Lock-1 is a lock.
-20
+5
  OUT: <<$1 --> key> ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.81%
 // Lock-1 can be opened by every key.
 
@@ -149,7 +149,7 @@
 // Every lock can be opened by some key.
 <{lock1} --> lock>. 
 // Lock-1 is a lock.
-9
+3
  OUT: (&&,<#1 --> key>,<{lock1} --> (/,open,#1,_)>). %1.00;0.81% 
 // Some key can open Lock-1.
 
@@ -158,7 +158,7 @@
 // There is a lock that can be opened by every key.
 <{lock1} --> lock>.
 // Lock-1 is a lock.
-9
+3
  OUT: <<$1 --> key> ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.43% 
 // I guess Lock-1 can be opened by every key.
 
@@ -167,8 +167,8 @@
 // There is a key that can open some lock.
 <{lock1} --> lock>.
 // Lock-1 is a lock.
-18
- OUT: (&&,<#1 --> key>,<{lock1} --> (/,open,#1,_)>). %1.00;0.43%
+4
+ OUT: (&&,<#1 --> key>,<(*,#1,{lock1}) --> open>). %1.00;0.43%
 // I guess there is a key that can open Lock-1.
 
 ********** variable introduction
@@ -217,7 +217,7 @@
 // Lock-1 can be opened by every key.
 <{lock1} --> lock>. 
 // Lock-1 is a lock.
-166
+15
  OUT: (&&,<#1 --> lock>,<<$2 --> key> ==> <#1 --> (/,open,$2,_)>>). %1.00;0.81%
 // There is a lock that can be opened by every key.
  OUT: <(&&,<$1 --> key>,<$2 --> lock>) ==> <$2 --> (/,open,$1,_)>>. %1.00;0.45%
@@ -228,32 +228,9 @@
 // Lock-1 can be opened by some key.
 <{lock1} --> lock>. 
 // Lock-1 is a lock.
-17
+15
  OUT: (&&,<#1 --> key>,<#2 --> lock>,<#2 --> (/,open,#1,_)>). %1.00;0.81%
 // There is a key that can open some lock.
  OUT: <<$1 --> lock> ==> (&&,<#2 --> key>,<$1 --> (/,open,#2,_)>)>. %1.00;0.45% 
 // I guess every lock can be opened by some key.
 
-***** second level 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 level 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} 
-
-
-********** recursion (multistep)
-  IN: <0 --> num>. %1.00;0.90% {0 : 1} 
-// 0 is a number
-  IN: <<$1 --> num> ==> <(*,$1) --> num>>. %1.00;0.90% {0 : 2} 
-// If n is a number, n+1 is also a number
-  IN: <(*,(*,(*,0))) --> num>?  {0 : 3} 
-// 3 is a number?
-1029
- OUT: <(*,(*,(*,0))) --> num>. %1.00;0.66%
-// I guess 3 is a number
diff --git a/nars-dist/Examples/Example-NAL6-unedited.txt b/nars-dist/Examples/Example-NAL6-unedited.txt
index 5430f88dc81a217083e1effe5a2ffe2c7a911017..b08019c3762c70d103350feeab077fe81de8e3a0 100644
--- a/nars-dist/Examples/Example-NAL6-unedited.txt
+++ b/nars-dist/Examples/Example-NAL6-unedited.txt
@@ -2,42 +2,41 @@
   IN: <<$1 --> bird> ==> <$1 --> flyer>>. %1.00;0.90% {0 : 1} 
   IN: <<$1 --> bird> ==> <$1 --> flyer>>. %0.00;0.70% {0 : 2} 
 1
- OUT: <<$1 --> bird> ==> <$1 --> flyer>>. %0.79;0.92% {1 : 1;2} 
+ OUT: <<$1 --> bird> ==> <$1 --> flyer>>. %0.79;0.92% {1 : 2;1} 
 ********** variable unification
   IN: <<$1 --> bird> ==> <$1 --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <<$1 --> robin> ==> <$1 --> bird>>. %1.00;0.90% {0 : 2} 
 3
- OUT: <<$1 --> robin> ==> <$1 --> animal>>. %1.00;0.81% {5 : 2;1} 
- OUT: <<$1 --> animal> ==> <$1 --> robin>>. %1.00;0.45% {5 : 2;1} 
+ OUT: <<$1 --> robin> ==> <$1 --> animal>>. %1.00;0.81% {3 : 1;2} 
+ OUT: <<$1 --> animal> ==> <$1 --> robin>>. %1.00;0.45% {3 : 1;2} 
 ********** variable unification
   IN: <<$1 --> swan> ==> <$1 --> bird>>. %1.00;0.80% {0 : 1} 
   IN: <<$1 --> swan> ==> <$1 --> swimmer>>. %0.80;0.90% {0 : 2} 
 3
- OUT: <<$1 --> swan> ==> (||,<$1 --> bird>,<$1 --> swimmer>)>. %1.00;0.72% {5 : 2;1} 
- OUT: <<$1 --> swan> ==> (&&,<$1 --> bird>,<$1 --> swimmer>)>. %0.80;0.72% {5 : 2;1} 
- OUT: <<$1 --> swimmer> ==> <$1 --> bird>>. %1.00;0.37% {5 : 2;1} 
- OUT: <<$1 --> bird> ==> <$1 --> swimmer>>. %0.80;0.42% {5 : 2;1} 
- OUT: <<$1 --> bird> <=> <$1 --> swimmer>>. %0.80;0.42% {5 : 2;1} 
+ OUT: <<$1 --> swan> ==> (||,<$1 --> bird>,<$1 --> swimmer>)>. %1.00;0.72% {3 : 1;2} 
+ OUT: <<$1 --> swan> ==> (&&,<$1 --> bird>,<$1 --> swimmer>)>. %0.80;0.72% {3 : 1;2} 
+ OUT: <<$1 --> swimmer> ==> <$1 --> bird>>. %1.00;0.37% {3 : 1;2} 
+ OUT: <<$1 --> bird> ==> <$1 --> swimmer>>. %0.80;0.42% {3 : 1;2} 
+ OUT: <<$1 --> bird> <=> <$1 --> swimmer>>. %0.80;0.42% {3 : 1;2} 
 ********** variable unification
   IN: <<bird --> $1> ==> <robin --> $1>>. %1.00;0.90% {0 : 1} 
   IN: <<swimmer --> $1> ==> <robin --> $1>>. %0.70;0.90% {0 : 2} 
 3
- OUT: <(&&,<bird --> $1>,<swimmer --> $1>) ==> <robin --> $1>>. %1.00;0.81% {5 : 2;1} 
- OUT: <(||,<bird --> $1>,<swimmer --> $1>) ==> <robin --> $1>>. %0.70;0.81% {5 : 2;1} 
- OUT: <<bird --> $1> ==> <swimmer --> $1>>. %1.00;0.36% {5 : 2;1} 
- OUT: <<swimmer --> $1> ==> <bird --> $1>>. %0.70;0.45% {5 : 2;1} 
- OUT: <<bird --> $1> <=> <swimmer --> $1>>. %0.70;0.45% {5 : 2;1} 
+ OUT: <(&&,<bird --> $1>,<swimmer --> $1>) ==> <robin --> $1>>. %1.00;0.81% {3 : 1;2} 
+ OUT: <(||,<bird --> $1>,<swimmer --> $1>) ==> <robin --> $1>>. %0.70;0.81% {3 : 1;2} 
+ OUT: <<bird --> $1> ==> <swimmer --> $1>>. %1.00;0.36% {3 : 1;2} 
+ OUT: <<swimmer --> $1> ==> <bird --> $1>>. %0.70;0.45% {3 : 1;2} 
+ OUT: <<bird --> $1> <=> <swimmer --> $1>>. %0.70;0.45% {3 : 1;2} 
 ********** variable unification
   IN: <(&&,<$1 --> flyer>,<$1 --> [chirping]>) ==> <$1 --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <<$1 --> [with-wings]> ==> <$1 --> flyer>>. %1.00;0.90% {0 : 2} 
-8
- OUT: <(&&,<$1 --> [chirping]>,<$1 --> [with-wings]>) ==> <$1 --> bird>>. %1.00;0.81% {1 : 2;1} 
+4
+ OUT: <(&&,<$1 --> [chirping]>,<$1 --> [with-wings]>) ==> <$1 --> bird>>. %1.00;0.81% {4 : 1;2} 
 ********** variable unification
   IN: <(&&,<$1 --> flyer>,<$1 --> [chirping]>,<(*,$1,worms) --> food>) ==> <$1 --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <(&&,<$1 --> [chirping]>,<$1 --> [with-wings]>) ==> <$1 --> bird>>. %1.00;0.90% {0 : 2} 
-6
- OUT: <(&&,<$1 --> flyer>,<(*,$1,worms) --> food>) ==> <$1 --> [with-wings]>>. %1.00;0.45% {4 : 1;2} 
- OUT: <<$1 --> [with-wings]> ==> (&&,<$1 --> flyer>,<(*,$1,worms) --> food>)>. %1.00;0.45% {4 : 1;2} 
+10
+ OUT: <(&&,<$1 --> flyer>,<$1 --> [chirping]>,<worms --> (/,food,$1,_)>) ==> <$1 --> bird>>. %1.00;0.90% {10 : 1} 
 ********** variable unification
   IN: <(&&,<$1 --> flyer>,<(*,$1,worms) --> food>) ==> <$1 --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <<$1 --> flyer> ==> <$1 --> [with-wings]>>. %1.00;0.90% {0 : 2} 
@@ -46,222 +45,120 @@
 2
  OUT: <<(*,$1,worms) --> food> ==> <worms --> (/,food,$1,_)>>. %1.00;0.45% {3 : 1;1} 
  OUT: <<worms --> (/,food,$1,_)> ==> <(*,$1,worms) --> food>>. %1.00;0.45% {3 : 1;1} 
-1
- OUT: <(&&,<$1 --> [with-wings]>,<worms --> (/,food,$1,_)>) ==> <$1 --> bird>>. %1.00;0.45% {4 : 2;1} 
+9
+ OUT: <(&&,<$1 --> [with-wings]>,<worms --> (/,food,$1,_)>) ==> <$1 --> bird>>. %1.00;0.45% {12 : 1;2} 
 ****** variable elimination
   IN: <<$1 --> bird> ==> <$1 --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <robin --> bird>. %1.00;0.90% {0 : 2} 
 3
- OUT: <robin --> animal>. %1.00;0.81% {5 : 2;1} 
+ OUT: <robin --> animal>. %1.00;0.81% {3 : 1;2} 
 ********** variable elimination
   IN: <<$1 --> bird> ==> <$1 --> animal>>. %1.00;0.90% {0 : 1} 
   IN: <tiger --> animal>. %1.00;0.90% {0 : 2} 
 3
- OUT: <tiger --> bird>. %1.00;0.45% {5 : 2;1} 
+ OUT: <tiger --> bird>. %1.00;0.45% {3 : 1;2} 
 ********** variable elimination
   IN: <<$1 --> animal> <=> <$1 --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <robin --> bird>. %1.00;0.90% {0 : 2} 
 3
- OUT: <robin --> animal>. %1.00;0.81% {5 : 2;1} 
+ OUT: <robin --> animal>. %1.00;0.81% {3 : 1;2} 
 ********** variable elimination
   IN: (&&,<#1 --> bird>,<#1 --> swimmer>). %1.00;0.90% {0 : 1} 
   IN: <swan --> bird>. %0.90;0.90% {0 : 2} 
 3
- OUT: <swan --> swimmer>. %0.90;0.43% {5 : 2;1} 
+ OUT: <swan --> swimmer>. %0.90;0.43% {3 : 1;2} 
 ********** variable elimination
   IN: <{Tweety} --> [with-wings]>. %1.00;0.90% {0 : 1} 
   IN: <(&&,<$1 --> [chirping]>,<$1 --> [with-wings]>) ==> <$1 --> bird>>. %1.00;0.90% {0 : 2} 
-23
- OUT: <<{Tweety} --> [chirping]> ==> <{Tweety} --> bird>>. %1.00;0.81% {18 : 2;1} 
+6
+ OUT: <<{Tweety} --> [chirping]> ==> <{Tweety} --> bird>>. %1.00;0.81% {6 : 1;2} 
 ********** variable elimination
   IN: <(&&,<$1 --> flyer>,<$1 --> [chirping]>,<(*,$1,worms) --> food>) ==> <$1 --> bird>>. %1.00;0.90% {0 : 1} 
   IN: <{Tweety} --> flyer>. %1.00;0.90% {0 : 2} 
-7
- OUT: <(&&,<{Tweety} --> [chirping]>,<(*,{Tweety},worms) --> food>) ==> <{Tweety} --> bird>>. %1.00;0.81% {3 : 1;2} 
+3
+ OUT: <(&&,<{Tweety} --> [chirping]>,<(*,{Tweety},worms) --> food>) ==> <{Tweety} --> bird>>. %1.00;0.81% {3 : 2;1} 
+ OUT: <(&&,<{Tweety} --> [chirping]>,<(*,{Tweety},worms) --> food>) ==> <{Tweety} --> bird>>. %1.00;0.81% {3 : 2;2;1} 
 ********** multiple variable elimination
   IN: <(&&,<$1 --> key>,<$2 --> lock>) ==> <$2 --> (/,open,$1,_)>>. %1.00;0.90% {0 : 1} 
   IN: <{lock1} --> lock>. %1.00;0.90% {0 : 2} 
 2
  OUT: <(&&,<$1 --> key>,<$2 --> lock>) ==> <(*,$1,$2) --> open>>. %1.00;0.90% {2 : 1} 
-13
- OUT: <(&&,<$1 --> key>,<$2 --> lock>) ==> <(*,$1,$2) --> open>>. %1.00;0.90% {15 : 1} 
-5
- OUT: <<$1 --> key> ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.81% {20 : 1;2}
+3
+ OUT: <<$1 --> key> ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.81% {5 : 2;1} 
 ********** multiple variable elimination
   IN: <<$1 --> lock> ==> (&&,<#2 --> key>,<$1 --> (/,open,#2,_)>)>. %1.00;0.90% {0 : 1} 
   IN: <{lock1} --> lock>. %1.00;0.90% {0 : 2} 
-9
+3
  OUT: (&&,<#1 --> key>,<{lock1} --> (/,open,#1,_)>). %1.00;0.81% {3 : 2;1} 
 ********** multiple variable elimination
   IN: (&&,<#1 --> lock>,<<$2 --> key> ==> <#1 --> (/,open,$2,_)>>). %1.00;0.90% {0 : 1} 
   IN: <{lock1} --> lock>. %1.00;0.90% {0 : 2} 
-9
+3
  OUT: <<$1 --> key> ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.43% {3 : 2;1} 
 ********** multiple variable elimination
   IN: (&&,<#1 --> lock>,<#1 --> (/,open,#2,_)>,<#2 --> key>). %1.00;0.90% {0 : 1} 
   IN: <{lock1} --> lock>. %1.00;0.90% {0 : 2} 
 1
  OUT: (&&,<#1 --> lock>,<#2 --> key>,<(*,#2,#1) --> open>). %1.00;0.90% {1 : 1} 
-13
- OUT: (&&,<#1 --> lock>,<#2 --> key>,<(*,#2,#1) --> open>). %1.00;0.90% {14 : 1} 
-4
- OUT: (&&,<#1 --> key>,<{lock1} --> (/,open,#1,_)>). %1.00;0.43% {18 : 2;1} 
+3
+ OUT: (&&,<#1 --> key>,<(*,#1,{lock1}) --> open>). %1.00;0.43% {4 : 2;1} 
 ********** variable introduction
   IN: <swan --> bird>. %1.00;0.90% {0 : 1} 
   IN: <swan --> swimmer>. %0.80;0.90% {0 : 2} 
 3
- OUT: <swan --> (|,bird,swimmer)>. %1.00;0.81% {5 : 2;1} 
- OUT: <swan --> (&,bird,swimmer)>. %0.80;0.81% {5 : 2;1} 
- OUT: <<$1 --> bird> ==> <$1 --> swimmer>>. %0.80;0.45% {5 : 2;1} 
- OUT: <<$1 --> swimmer> ==> <$1 --> bird>>. %1.00;0.39% {5 : 2;1} 
- OUT: <<$1 --> bird> <=> <$1 --> swimmer>>. %0.80;0.45% {5 : 2;1} 
- OUT: (&&,<#1 --> bird>,<#1 --> swimmer>). %0.80;0.81% {5 : 2;1} 
- OUT: <swimmer --> bird>. %1.00;0.39% {5 : 2;1} 
- OUT: <bird --> swimmer>. %0.80;0.45% {5 : 2;1} 
- OUT: <bird <-> swimmer>. %0.80;0.45% {5 : 2;1} 
+ OUT: <swan --> (|,bird,swimmer)>. %1.00;0.81% {3 : 1;2} 
+ OUT: <swan --> (&,bird,swimmer)>. %0.80;0.81% {3 : 1;2} 
+ OUT: <<$1 --> bird> ==> <$1 --> swimmer>>. %0.80;0.45% {3 : 1;2} 
+ OUT: <<$1 --> swimmer> ==> <$1 --> bird>>. %1.00;0.39% {3 : 1;2} 
+ OUT: <<$1 --> bird> <=> <$1 --> swimmer>>. %0.80;0.45% {3 : 1;2} 
+ OUT: (&&,<#1 --> bird>,<#1 --> swimmer>). %0.80;0.81% {3 : 1;2} 
+ OUT: <swimmer --> bird>. %1.00;0.39% {3 : 1;2} 
+ OUT: <bird --> swimmer>. %0.80;0.45% {3 : 1;2} 
+ OUT: <bird <-> swimmer>. %0.80;0.45% {3 : 1;2} 
 ********** variable introduction
   IN: <gull --> swimmer>. %1.00;0.90% {0 : 1} 
   IN: <swan --> swimmer>. %0.80;0.90% {0 : 2} 
 3
- OUT: <(&,gull,swan) --> swimmer>. %1.00;0.81% {5 : 2;1} 
- OUT: <(|,gull,swan) --> swimmer>. %0.80;0.81% {5 : 2;1} 
- OUT: <<gull --> $1> ==> <swan --> $1>>. %0.80;0.45% {5 : 2;1} 
- OUT: <<swan --> $1> ==> <gull --> $1>>. %1.00;0.39% {5 : 2;1} 
- OUT: <<gull --> $1> <=> <swan --> $1>>. %0.80;0.45% {5 : 2;1} 
- OUT: (&&,<gull --> #1>,<swan --> #1>). %0.80;0.81% {5 : 2;1} 
- OUT: <gull --> swan>. %1.00;0.39% {5 : 2;1} 
- OUT: <swan --> gull>. %0.80;0.45% {5 : 2;1} 
- OUT: <gull <-> swan>. %0.80;0.45% {5 : 2;1} 
+ OUT: <(&,gull,swan) --> swimmer>. %1.00;0.81% {3 : 1;2} 
+ OUT: <(|,gull,swan) --> swimmer>. %0.80;0.81% {3 : 1;2} 
+ OUT: <<gull --> $1> ==> <swan --> $1>>. %0.80;0.45% {3 : 1;2} 
+ OUT: <<swan --> $1> ==> <gull --> $1>>. %1.00;0.39% {3 : 1;2} 
+ OUT: <<gull --> $1> <=> <swan --> $1>>. %0.80;0.45% {3 : 1;2} 
+ OUT: (&&,<gull --> #1>,<swan --> #1>). %0.80;0.81% {3 : 1;2} 
+ OUT: <gull --> swan>. %1.00;0.39% {3 : 1;2} 
+ OUT: <swan --> gull>. %0.80;0.45% {3 : 1;2} 
+ OUT: <gull <-> swan>. %0.80;0.45% {3 : 1;2} 
 ********** variables introduction
   IN: <{key1} --> (/,open,_,{lock1})>. %1.00;0.90% {0 : 1} 
   IN: <{key1} --> key>. %1.00;0.90% {0 : 2} 
 6
- OUT: <{key1} --> (|,key,(/,open,_,{lock1}))>. %1.00;0.81% {3 : 1;2} 
- OUT: <{key1} --> (&,key,(/,open,_,{lock1}))>. %1.00;0.81% {3 : 1;2} 
- OUT: <<$1 --> key> ==> <$1 --> (/,open,_,{lock1})>>. %1.00;0.45% {3 : 1;2} 
- OUT: <<$1 --> (/,open,_,{lock1})> ==> <$1 --> key>>. %1.00;0.45% {3 : 1;2} 
- OUT: <<$1 --> key> <=> <$1 --> (/,open,_,{lock1})>>. %1.00;0.45% {3 : 1;2} 
- OUT: (&&,<#1 --> key>,<#1 --> (/,open,_,{lock1})>). %1.00;0.81% {3 : 1;2} 
- OUT: <(/,open,_,{lock1}) --> key>. %1.00;0.45% {3 : 1;2} 
- OUT: <key --> (/,open,_,{lock1})>. %1.00;0.45% {3 : 1;2} 
- OUT: <key <-> (/,open,_,{lock1})>. %1.00;0.45% {3 : 1;2} 
+ OUT: <{key1} --> (|,key,(/,open,_,{lock1}))>. %1.00;0.81% {6 : 2;1} 
+ OUT: <{key1} --> (&,key,(/,open,_,{lock1}))>. %1.00;0.81% {6 : 2;1} 
+ OUT: <<$1 --> key> ==> <$1 --> (/,open,_,{lock1})>>. %1.00;0.45% {6 : 2;1} 
+ OUT: <<$1 --> (/,open,_,{lock1})> ==> <$1 --> key>>. %1.00;0.45% {6 : 2;1} 
+ OUT: <<$1 --> key> <=> <$1 --> (/,open,_,{lock1})>>. %1.00;0.45% {6 : 2;1} 
+ OUT: (&&,<#1 --> key>,<#1 --> (/,open,_,{lock1})>). %1.00;0.81% {6 : 2;1} 
+ OUT: <(/,open,_,{lock1}) --> key>. %1.00;0.45% {6 : 2;1} 
+ OUT: <key --> (/,open,_,{lock1})>. %1.00;0.45% {6 : 2;1} 
+ OUT: <key <-> (/,open,_,{lock1})>. %1.00;0.45% {6 : 2;1} 
 ********** multiple variables introduction
-  IN: <<$1 --> key> ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.90% {0 : 1} 
-  IN: <{lock1} --> lock>. %1.00;0.90% {0 : 2} 
-1
- OUT: (&&,<#1 --> lock>,<<$2 --> key> ==> <#1 --> (/,open,$2,_)>>). %1.00;0.81% {1 : 2;1} 
- OUT: <(&&,<$1 --> key>,<$2 --> lock>) ==> <$2 --> (/,open,$1,_)>>. %1.00;0.45% {1 : 2;1} 
-
   IN: <<$1 --> key> ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.90% {0 : 1} 
   IN: <{lock1} --> lock>. %1.00;0.90% {0 : 2} 
 2
  OUT: <<$1 --> key> ==> <(*,$1,{lock1}) --> open>>. %1.00;0.90% {2 : 1} 
-11
- OUT: <<$1 --> key> ==> (||,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>)>. %1.00;0.81% {13 : 1;1} 
- OUT: <<$1 --> key> ==> (&&,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>)>. %1.00;0.81% {13 : 1;1} 
- OUT: <<(*,$1,{lock1}) --> open> ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.45% {13 : 1;1} 
- OUT: <<{lock1} --> (/,open,$1,_)> ==> <(*,$1,{lock1}) --> open>>. %1.00;0.45% {13 : 1;1} 
- OUT: <<{lock1} --> (/,open,$1,_)> <=> <(*,$1,{lock1}) --> open>>. %1.00;0.45% {13 : 1;1} 
-1
- OUT: <<$1 --> key> ==> <(*,$1,{lock1}) --> open>>. %1.00;0.90% {14 : 1} 
-3
- OUT: <<$1 --> key> ==> <(*,$1,{lock1}) --> open>>. %1.00;0.40% {17 : 1;1;1} 
- OUT: <<(*,$1,{lock1}) --> open> ==> <$1 --> key>>. %1.00;0.29% {17 : 1;1;1} 
-7
- OUT: <(&&,<$1 --> key>,<(*,$1,{lock1}) --> open>) ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.40% {24 : 1;1;1} 
- OUT: <(||,<$1 --> key>,<(*,$1,{lock1}) --> open>) ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.40% {24 : 1;1;1} 
- OUT: <<$1 --> key> ==> <(*,$1,{lock1}) --> open>>. %1.00;0.29% {24 : 1;1;1} 
- OUT: <<(*,$1,{lock1}) --> open> ==> <$1 --> key>>. %1.00;0.29% {24 : 1;1;1} 
- OUT: <<$1 --> key> <=> <(*,$1,{lock1}) --> open>>. %1.00;0.29% {24 : 1;1;1} 
-8
- OUT: <(&&,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>) ==> (||,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>)>. %1.00;0.40% {32 : 1;1;1;1} 
- OUT: <(||,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>) ==> (&&,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>)>. %1.00;0.40% {32 : 1;1;1;1} 
- OUT: <(&&,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>) <=> (||,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>)>. %1.00;0.40% {32 : 1;1;1;1} 
-5
- OUT: <(||,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>) ==> (&&,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>)>. %1.00;0.40% {37 : 1;1;1;1} 
- OUT: <(&&,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>) ==> (||,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>)>. %1.00;0.40% {37 : 1;1;1;1} 
- OUT: <(&&,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>) <=> (||,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>)>. %1.00;0.40% {37 : 1;1;1;1} 
-26
- OUT: (&&,<#1 --> lock>,<<(*,$2,#1) --> open> ==> <#1 --> (/,open,$2,_)>>). %1.00;0.40% {63 : 1;2;1} 
- OUT: <(&&,<$1 --> lock>,<(*,$2,$1) --> open>) ==> <$1 --> (/,open,$2,_)>>. %1.00;0.29% {63 : 1;2;1} 
-2
- OUT: <#1 --> lock>. %1.00;0.36% {65 : 1;2;1} 
-1
- OUT: <<(*,$1,#2) --> open> ==> <#2 --> (/,open,$1,_)>>. %1.00;0.10% {66 : 1;1;2;2;1;1} 
-7
- OUT: <(&,#1,{lock1}) --> lock>. %1.00;0.33% {73 : 1;2;2;1} 
- OUT: <(|,#1,{lock1}) --> lock>. %1.00;0.33% {73 : 1;2;2;1} 
- OUT: <<#1 --> $2> <=> <{lock1} --> $2>>. %1.00;0.25% {73 : 1;2;2;1} 
- OUT: (&&,<#1 --> #2>,<{lock1} --> #2>). %1.00;0.33% {73 : 1;2;2;1} 
- OUT: <#1 <-> {lock1}>. %1.00;0.25% {73 : 1;2;2;1} 
-5
- OUT: <(&,#1,{lock1}) --> lock>. %1.00;0.33% {78 : 1;2;2;1} 
- OUT: <(|,#1,{lock1}) --> lock>. %1.00;0.33% {78 : 1;2;2;1} 
- OUT: <<#1 --> $2> <=> <{lock1} --> $2>>. %1.00;0.25% {78 : 1;2;2;1} 
- OUT: (&&,<#1 --> #2>,<{lock1} --> #2>). %1.00;0.33% {78 : 1;2;2;1} 
- OUT: <#1 <-> {lock1}>. %1.00;0.25% {78 : 1;2;2;1} 
-1
- OUT: <<(*,$1,#2) --> open> ==> <#2 --> (/,open,$1,_)>>. %1.00;0.36% {79 : 1;2;1} 
-5
- OUT: <<$1 --> key> ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.40% {84 : 1;1;1} 
 10
- OUT: <(&,#1,{lock1}) --> lock>. %1.00;0.33% {94 : 1;2;2;1} 
- OUT: <(|,#1,{lock1}) --> lock>. %1.00;0.33% {94 : 1;2;2;1} 
- OUT: <<#1 --> $2> <=> <{lock1} --> $2>>. %1.00;0.25% {94 : 1;2;2;1} 
- OUT: (&&,<#1 --> #2>,<{lock1} --> #2>). %1.00;0.33% {94 : 1;2;2;1} 
- OUT: <#1 <-> {lock1}>. %1.00;0.25% {94 : 1;2;2;1} 
-5
- OUT: <(&&,<$1 --> key>,<(*,$1,{lock1}) --> open>) ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.40% {99 : 1;1;1} 
- OUT: <(||,<$1 --> key>,<(*,$1,{lock1}) --> open>) ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.40% {99 : 1;1;1} 
- OUT: <<$1 --> key> ==> <(*,$1,{lock1}) --> open>>. %1.00;0.29% {99 : 1;1;1} 
- OUT: <<(*,$1,{lock1}) --> open> ==> <$1 --> key>>. %1.00;0.29% {99 : 1;1;1} 
- OUT: <<$1 --> key> <=> <(*,$1,{lock1}) --> open>>. %1.00;0.29% {99 : 1;1;1} 
-6
- OUT: <<(*,$1,#2) --> open> ==> <#2 --> (/,open,$1,_)>>. %1.00;0.36% {105 : 1;2;1} 
+ OUT: <<$1 --> key> ==> <(*,$1,{lock1}) --> open>>. %1.00;0.90% {12 : 1} 
 3
- OUT: <<$1 --> key> ==> (||,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>)>. %1.00;0.81% {108 : 1;1} 
- OUT: <<$1 --> key> ==> (&&,<{lock1} --> (/,open,$1,_)>,<(*,$1,{lock1}) --> open>)>. %1.00;0.81% {108 : 1;1} 
- OUT: <<(*,$1,{lock1}) --> open> ==> <{lock1} --> (/,open,$1,_)>>. %1.00;0.45% {108 : 1;1} 
- OUT: <<{lock1} --> (/,open,$1,_)> ==> <(*,$1,{lock1}) --> open>>. %1.00;0.45% {108 : 1;1} 
- OUT: <<{lock1} --> (/,open,$1,_)> <=> <(*,$1,{lock1}) --> open>>. %1.00;0.45% {108 : 1;1} 
-15
- OUT: <<(*,$1,#2) --> open> ==> <#2 --> (/,open,$1,_)>>. %1.00;0.36% {123 : 1;2;1} 
-12
- OUT: <<(*,$1,(&,#2,{lock1})) --> open> ==> <(&,#2,{lock1}) --> (/,open,$1,_)>>. %1.00;0.09% {135 : 1;1;2;2;2;1;1} 
-10
- OUT: <<(*,$1,(&,#2,{lock1})) --> open> ==> <(&,#2,{lock1}) --> (/,open,$1,_)>>. %1.00;0.09% {145 : 1;1;2;2;2;1;1} 
-7
- OUT: <<(*,$1,#2) --> open> ==> <#2 --> (/,open,$1,_)>>. %1.00;0.36% {152 : 1;2;1} 
-14
- OUT: (&&,<#1 --> lock>,<<$2 --> key> ==> <#1 --> (/,open,$2,_)>>). %1.00;0.81% {166 : 1;2} 
- OUT: <(&&,<$1 --> key>,<$2 --> lock>) ==> <$2 --> (/,open,$1,_)>>. %1.00;0.45% {166 : 1;2} 
-
+ 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} 
 2
  OUT: (&&,<#1 --> key>,<(*,#1,{lock1}) --> open>). %1.00;0.90% {2 : 1} 
-12
- OUT: (&&,<#1 --> key>,<(*,#1,{lock1}) --> open>). %1.00;0.90% {14 : 1} 
+10
+ OUT: (&&,<#1 --> key>,<(*,#1,{lock1}) --> open>). %1.00;0.90% {12 : 1} 
 3
- OUT: (&&,<#1 --> key>,<#2 --> lock>,<#2 --> (/,open,#1,_)>). %1.00;0.81% {17 : 2;1} 
- OUT: <<$1 --> lock> ==> (&&,<#2 --> key>,<$1 --> (/,open,#2,_)>)>. %1.00;0.45% {17 : 2;1} 
-
-***** second level 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 level 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} 
-
-********** recursion (multistep)
-  IN: <0 --> num>. %1.00;0.90% {0 : 1} 
-  IN: <<$1 --> num> ==> <(*,$1) --> num>>. %1.00;0.90% {0 : 2} 
-  IN: <(*,(*,(*,0))) --> num>?  {0 : 3} 
-1029
- OUT: <(*,(*,(*,0))) --> num>. %1.00;0.66%
+ 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}