diff --git a/fol/kb.py b/fol/kb.py
index 53ffb8a..0663e8a 100644
--- a/fol/kb.py
+++ b/fol/kb.py
@@ -7,7 +7,7 @@ class Kb:
         self.counter = fol.cnf.Counter()
 
     def make_f(self, h):
-        self.counter.begin()
+
         f = h
         if type(f) is str:
             f = fol.p(f)
@@ -68,9 +68,8 @@ class Kb:
         return res
 
     def exists(self, f):
-        h = self.make_f(f)
         for g in self.base:
-            if self.clause_equals(h, g):
+            if self.clause_equals([f], g):
                 return True
         return False
 
@@ -90,7 +89,10 @@ class Kb:
 
     def clause_in(self, clause, lst):
         for other in lst:
-            same = fol.unify(clause, other) is not None
+            same = clause.equals(other)
+
+            s = fol.unify(clause, other)
+            # same = s is not None
             if same:
                 return True
         return False
@@ -101,7 +103,7 @@ class Kb:
         self.base.append(req)
 
     def ask(self, request):
-        for i in range(20):
+        while True:
             n = len(self.base)
             self.update()
             if n == len(self.base):
@@ -113,7 +115,12 @@ class Kb:
         for f in self.base:
             s = fol.unify(f, req)
             if s is not None:
-                results.append(s)
+                ok = True
+                for k in s.keys():
+                    if len(s[k].find_by_name('VAR')) > 0:
+                        ok = False
+                if ok:
+                    results.append(s)
 
         return results
 
@@ -125,7 +132,8 @@ class Kb:
             self.solve(rule, self.conds(rule), self.facts, solution, solutions)
             for sol in solutions:
                 concl = conclusion.subst(sol)
-                if not self.exists(concl):
+
+                if not self.exists(concl) and concl.depth() < 4:
                     self.base.append([concl])
                     return
 
diff --git a/fol/node.py b/fol/node.py
index 7730fca..c6add42 100644
--- a/fol/node.py
+++ b/fol/node.py
@@ -100,3 +100,11 @@ class Node:
             res.extend(c.find_by_name(name))
 
         return res
+
+    def depth(self):
+        if len(self.children) == 0:
+            return 0
+        res = 0
+        for child in self.children:
+            res = max(res, child.depth())
+        return res + 1
diff --git a/sine_patre.py b/sine_patre.py
index a9154e7..6e8d812 100644
--- a/sine_patre.py
+++ b/sine_patre.py
@@ -3,11 +3,26 @@ import fol
 if __name__ == '__main__':
     kb = fol.kb.Kb()
     try:
-        kb.tell('Friend(ALICE, BOB)')
-        kb.tell('Friend(BOB, CLAIRE)')
-        kb.tell('Friend(x, y) -> Friend(y, x)')
-        kb.tell('(Friend(x, y) & Friend(y, z)) -> Friend(x, z)')
+        if False:
+            kb.tell('Est(ALICE, X0, S0)')
+            kb.tell('Proche(X0, X1)')
+            kb.tell('Proche(X1, X2)')
+            kb.tell('Proche(X2, X3)')
+            kb.tell('Proche(X3, X4)')
+            kb.tell('(Est(ALICE, x, s) & Proche(x, y)) -> Poss(go(x, y), s)')
+            kb.tell('Poss(go(x, y), s) -> Est(ALICE, y, do(go(x, y), s))')
+            answer = kb.ask('Est(ALICE, x, y)')
+            print(answer)
+        else:
+            kb.tell('Friend(ALICE, BOB)')
+            kb.tell('Friend(BOB, CLAIRE)')
+            kb.tell('Friend(x, y) -> Friend(y, x)')
+            kb.tell('(Friend(x, y) & Friend(y, z)) -> Friend(x, z)')
+            answer = kb.ask('Friend(ALICE, x)')
+            print(answer)
+
+        # print('--------------------------------')
+        # [print(b) for b in kb.base]
 
-        print(kb.ask('Friend(ALICE, x)'))
     except KeyboardInterrupt:
         pass