diff --git a/RELEASE b/RELEASE
index 6f39d505b..5d4f5a3f0 100644
--- a/RELEASE
+++ b/RELEASE
@@ -1,5 +1,7 @@
                                   EYE release
 
+v9.0.10 (2023-12-11) using lingua:varCount to make rules safe
+v9.0.10 (2023-12-11) using lingua:varCount to make rules safe
 v9.0.9 (2023-12-08) adding experimental log:callNotBind built-in
 v9.0.8 (2023-12-06) using linear lists for surfaces
 v9.0.7 (2023-12-06) using linear lists for lingua
diff --git a/VERSION b/VERSION
index ea0877382..6d98d162b 100644
--- a/VERSION
+++ b/VERSION
@@ -1 +1 @@
-9.0.9
+9.0.10
diff --git a/eye.pl b/eye.pl
index 438b54273..df2f67d08 100644
--- a/eye.pl
+++ b/eye.pl
@@ -21,7 +21,7 @@
 :- use_module(library(pcre)).
 :- catch(use_module(library(http/http_open)), _, true).
 
-version_info('EYE v9.0.9 (2023-12-08)').
+version_info('EYE v9.0.10 (2023-12-11)').
 
 license_info('MIT License
 
@@ -646,33 +646,28 @@
     % forward rule
     assertz(implies((
             '<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>'(R, '<http://www.w3.org/2000/10/swap/lingua#ForwardRule>'),
-            '<http://www.w3.org/2000/10/swap/lingua#vars>'(R, U),
-            getlist(U, V),
             '<http://www.w3.org/2000/10/swap/lingua#premise>'(R, K),
             getconj(K, A),
             '<http://www.w3.org/2000/10/swap/lingua#conclusion>'(R, H),
             getconj(H, B),
-            (   flag(explain),
-                B \= false
-            ->  conj_append(B, remember(answer('<http://www.w3.org/2000/10/swap/lingua#bindings>', R, U)), D)
-            ;   D = B
-            ),
-            makevars([A, D], [Q, I], beta(V))
+            '<http://www.w3.org/2000/10/swap/lingua#varCount>'(R, N),
+            findvars([A, B], U, beta),
+            distinct(U, V),
+            length(V, N),
+            makevars([A, B], [Q, I], beta(V))
             ), '<http://www.w3.org/2000/10/swap/log#implies>'(Q, I), '<>')),
     % backward rule
     assertz(implies((
             '<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>'(R, '<http://www.w3.org/2000/10/swap/lingua#BackwardRule>'),
-            '<http://www.w3.org/2000/10/swap/lingua#vars>'(R, U),
-            getlist(U, V),
             '<http://www.w3.org/2000/10/swap/lingua#premise>'(R, K),
             getconj(K, A),
             '<http://www.w3.org/2000/10/swap/lingua#conclusion>'(R, H),
             getconj(H, B),
-            (   flag(explain)
-            ->  conj_append(A, remember(answer('<http://www.w3.org/2000/10/swap/lingua#bindings>', R, U)), D)
-            ;   D = A
-            ),
-            makevars(':-'(B, D), C, beta(V)),
+            '<http://www.w3.org/2000/10/swap/lingua#varCount>'(R, N),
+            findvars([A, B], U, beta),
+            distinct(U, V),
+            length(V, N),
+            makevars(':-'(B, A), C, beta(V)),
             copy_term_nat(C, CC),
             labelvars(CC, 0, _, avar),
             (   \+cc(CC)
@@ -684,18 +679,16 @@
     % query rule
     assertz(implies((
             '<http://www.w3.org/1999/02/22-rdf-syntax-ns#type>'(R, '<http://www.w3.org/2000/10/swap/lingua#QueryRule>'),
-            '<http://www.w3.org/2000/10/swap/lingua#vars>'(R, U),
-            getlist(U, V),
             '<http://www.w3.org/2000/10/swap/lingua#premise>'(R, K),
             getconj(K, A),
             '<http://www.w3.org/2000/10/swap/lingua#conclusion>'(R, H),
             getconj(H, B),
             djiti_answer(answer(B), J),
-            (   flag(explain)
-            ->  conj_append(A, remember(answer('<http://www.w3.org/2000/10/swap/lingua#bindings>', R, U)), D)
-            ;   D = A
-            ),
-            makevars(implies(D, J, '<>'), C, beta(V)),
+            '<http://www.w3.org/2000/10/swap/lingua#varCount>'(R, N),
+            findvars([A, B], U, beta),
+            distinct(U, V),
+            length(V, N),
+            makevars(implies(A, J, '<>'), C, beta(V)),
             copy_term_nat(C, CC),
             labelvars(CC, 0, _, avar),
             (   \+cc(CC)
diff --git a/eye.zip b/eye.zip
index db6fb7e72..e145c3c41 100644
Binary files a/eye.zip and b/eye.zip differ
diff --git a/reasoning/lingua/acp.ttl b/reasoning/lingua/acp.ttl
index 1111e349a..19feb8ff5 100644
--- a/reasoning/lingua/acp.ttl
+++ b/reasoning/lingua/acp.ttl
@@ -15,12 +15,6 @@
     :noneOf :D.
 
 :acp_rule1 a lingua:BackwardRule;
-    lingua:vars (
-        _:Pol
-        _:Test
-        _:Field
-        _:X
-    );
     lingua:conclusion (
         _:Pol :pass :allOfTest
     );
@@ -35,17 +29,11 @@
                 _:Test :has _:Field
             )
         ) log:forAllIn _:X
-    ).
+    );
+    lingua:varCount 4.
 
 :acp_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:Pol
-        _:Test
-        _:Field
-        _:List
-        _:X
-        _:L
-    );lingua:conclusion (
+    lingua:conclusion (
         _:Pol :pass :anyOfTest
     );
     lingua:premise (
@@ -61,17 +49,10 @@
         ) log:collectAllIn _:X
         _:List list:length _:L
         _:L log:notEqualTo 0
-    ).
+    );
+    lingua:varCount 6.
 
 :acp_rule3 a lingua:BackwardRule;
-    lingua:vars (
-        _:Pol
-        _:Test
-        _:Field
-        _:List
-        _:X
-        _:L
-    );
     lingua:conclusion (
         _:Pol :pass :noneOfTest
     );
@@ -84,13 +65,11 @@
             ) _:List) log:collectAllIn _:X
         _:List list:length _:L
         _:L log:equalTo 0
-    ).
+    );
+    lingua:varCount 6.
 
 # query
 :acp_query a lingua:QueryRule;
-    lingua:vars (
-        _:Pol
-    );
     lingua:premise (
         _:Pol rdf:type :Policy
         _:Pol :pass :allOfTest
@@ -100,4 +79,5 @@
     lingua:conclusion (
         :test :for _:Pol
         :test :is true
-    ).
+    );
+    lingua:varCount 1.
diff --git a/reasoning/lingua/append.ttl b/reasoning/lingua/append.ttl
index 0fd6c9ac6..fb18bc082 100644
--- a/reasoning/lingua/append.ttl
+++ b/reasoning/lingua/append.ttl
@@ -16,11 +16,6 @@
 
 # query
 :append_query a lingua:QueryRule;
-    lingua:vars (
-        _:X1
-        _:X2
-        _:Y
-    );
     lingua:premise (
         :Let :param1 _:X1
         :Let :param2 _:X2
@@ -28,4 +23,5 @@
     );
     lingua:conclusion (
         (_:X1 _:X2) :append _:Y
-).
+    );
+    lingua:varCount 3.
diff --git a/reasoning/lingua/backward.ttl b/reasoning/lingua/backward.ttl
index c63fa0be5..0d810fda5 100644
--- a/reasoning/lingua/backward.ttl
+++ b/reasoning/lingua/backward.ttl
@@ -5,23 +5,20 @@
 # see https://www.w3.org/2000/10/swap/doc/tutorial-1.pdf page 17
 # something is more interesting if it is greater
 :backward_rule a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-    );
     lingua:conclusion (
         _:X :moreInterestingThan _:Y
     );
     lingua:premise (
         _:X math:greaterThan _:Y
-    ).
+    );
+    lingua:varCount 2.
 
 # query
 :backward_query a lingua:QueryRule;
-    lingua:vars ();
     lingua:premise (
         5 :moreInterestingThan 3
     );
     lingua:conclusion (
         :result :is (5 :moreInterestingThan 3)
-    ).
+    );
+    lingua:varCount 0.
diff --git a/reasoning/lingua/complex.ttl b/reasoning/lingua/complex.ttl
index b4e7faede..178cabd04 100644
--- a/reasoning/lingua/complex.ttl
+++ b/reasoning/lingua/complex.ttl
@@ -5,26 +5,6 @@
 
 # exponentiation
 :complex_numbers_exponentiation_rule a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-        _:B
-        _:C
-        _:D
-        _:E
-        _:F
-        _:R
-        _:T
-        _:Z1
-        _:Z2
-        _:Z3
-        _:Z4
-        _:Z5
-        _:Z6
-        _:Z7
-        _:Z8
-        _:Z9
-        _:Z10
-    );
     lingua:conclusion (
         ((_:A _:B) (_:C _:D)) complex:exponentiation (_:E _:F)
     );
@@ -42,33 +22,11 @@
         (_:Z1 _:Z4 _:Z9) math:product _:E
         _:Z8 math:sin _:Z10
         (_:Z1 _:Z4 _:Z10) math:product _:F
-    ).
+    );
+    lingua:varCount 18.
 
 # asin
 :complex_numbers_asin_rule a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-        _:B
-        _:C
-        _:D
-        _:E
-        _:F
-        _:Z1
-        _:Z2
-        _:Z3
-        _:Z4
-        _:Z5
-        _:Z6
-        _:Z7
-        _:Z8
-        _:Z9
-        _:Z10
-        _:Z11
-        _:Z12
-        _:Z13
-        _:Z14
-        _:Z15
-    );
     lingua:conclusion (
         (_:A _:B) complex:asin (_:C _:D)
     );
@@ -92,34 +50,11 @@
         (_:Z13 0.5) math:exponentiation _:Z14
         (_:F _:Z14) math:sum _:Z15
         (2.718281828459045 _:D) math:exponentiation _:Z15
-    ).
+    );
+    lingua:varCount 21.
 
 # acos
 :complex_numbers_acos_rule a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-        _:B
-        _:C
-        _:D
-        _:E
-        _:F
-        _:Z1
-        _:Z2
-        _:Z3
-        _:Z4
-        _:Z5
-        _:Z6
-        _:Z7
-        _:Z8
-        _:Z9
-        _:Z10
-        _:Z11
-        _:Z12
-        _:Z13
-        _:Z14
-        _:Z15
-        _:U
-    );
     lingua:conclusion (
         (_:A _:B) complex:acos (_:C _:D)
     );
@@ -144,22 +79,11 @@
         (_:F _:Z14) math:sum _:Z15
         (2.718281828459045 _:U) math:exponentiation _:Z15
         _:U math:negation _:D
-    ).
+    );
+    lingua:varCount 22.
 
 # polar
 :complex_numbers_polar_rule a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-        _:R
-        _:Tp
-        _:Z1
-        _:Z2
-        _:Z3
-        _:Z4
-        _:Z5
-        _:T
-    );
     lingua:conclusion (
         (_:X _:Y) complex:polar(_:R _:Tp)
     );
@@ -172,16 +96,11 @@
         (_:Z4 _:R) math:quotient _:Z5
         _:Z5 math:acos _:T
         (_:X _:Y _:T) complex:dial _:Tp
-    ).
+    );
+    lingua:varCount 10.
 
 # dial
 :complex_numbers_dial_rule1 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-        _:T
-        _:Tp
-    );
     lingua:conclusion (
         (_:X _:Y _:T) complex:dial _:Tp
     );
@@ -189,15 +108,10 @@
         _:X math:notLessThan 0
         _:Y math:notLessThan 0
         (0 _:T) math:sum _:Tp
-    ).
+    );
+    lingua:varCount 4.
 
 :complex_numbers_dial_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-        _:T
-        _:Tp
-    );
     lingua:conclusion (
         (_:X _:Y _:T) complex:dial _:Tp
     );
@@ -205,15 +119,10 @@
         _:X math:lessThan 0
         _:Y math:notLessThan 0
         (3.141592653589793 _:T) math:difference _:Tp
-    ).
+    );
+    lingua:varCount 4.
 
 :complex_numbers_dial_rule3 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-        _:T
-        _:Tp
-    );
     lingua:conclusion (
         (_:X _:Y _:T) complex:dial _:Tp
     );
@@ -221,16 +130,10 @@
         _:X math:lessThan 0
         _:Y math:lessThan 0
         (3.141592653589793 _:T) math:sum _:Tp
-    ).
+    );
+    lingua:varCount 4.
 
 :complex_numbers_dial_rule4 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-        _:T
-        _:Tp
-        _:Z1
-    );
     lingua:conclusion (
         (_:X _:Y _:T) complex:dial _:Tp
     );
@@ -239,18 +142,11 @@
         _:Y math:lessThan 0
         (3.141592653589793 2) math:product _:Z1
         (_:Z1 _:T) math:difference _:Tp
-    ).
+    );
+    lingua:varCount 5.
 
 # query
 :complex_numbers_query a lingua:QueryRule;
-    lingua:vars (
-        _:C1
-        _:C2
-        _:C3
-        _:C4
-        _:C5
-        _:C6
-    );
     lingua:premise (
         ((-1 0) (0.5 0)) complex:exponentiation _:C1
         ((2.718281828459045 0) (0 3.141592653589793)) complex:exponentiation _:C2
@@ -266,4 +162,5 @@
         ((2.718281828459045 0) (-1.57079632679 0)) complex:exponentiation _:C4
         (2 0) complex:asin _:C5
         (2 0) complex:acos _:C6
-    ).
+    );
+    lingua:varCount 6.
diff --git a/reasoning/lingua/control.ttl b/reasoning/lingua/control.ttl
index d2eda89d5..91222a81d 100644
--- a/reasoning/lingua/control.ttl
+++ b/reasoning/lingua/control.ttl
@@ -22,13 +22,6 @@
 
 # forward rules
 :control_rule1 a lingua:ForwardRule;
-    lingua:vars (
-        _:M1
-        _:D1
-        _:C1
-        _:C2
-        _:C
-    );
     lingua:premise (
         :input1 :measurement10 _:M1
         :input2 :measurement2 true
@@ -39,21 +32,10 @@
     );
     lingua:conclusion (
         :actuator1 :control1 _:C
-    ).
+    );
+    lingua:varCount 5.
 
 :control_rule2 a lingua:ForwardRule;
-    lingua:vars (
-        _:M3
-        _:P3
-        _:M4
-        _:T2
-        _:E
-        _:D
-        _:C1
-        _:N
-        _:C2
-        _:C
-    );
     lingua:premise (
         :input3 :measurement3 _:M3
         :state3 :observation3 _:P3
@@ -68,18 +50,11 @@
     );
     lingua:conclusion (
         :actuator2 :control1 _:C
-    ).
+    );
+    lingua:varCount 10.
 
 # backward rules
 :control_rule3 a lingua:BackwardRule;
-    lingua:vars (
-        _:I
-        _:M
-        _:M1
-        _:M2
-        _:M3
-        _:M
-    );
     lingua:conclusion (
         _:I :measurement10 _:M
     );
@@ -88,31 +63,25 @@
         _:M1 math:lessThan _:M2
         (_:M2 _:M1) math:difference _:M3
         (_:M3 0.5) math:exponentiation _:M
-    ).
+    );
+    lingua:varCount 5.
 
 :control_rule4 a lingua:BackwardRule;
-    lingua:vars (
-        _:I
-        _:M1
-        _:M2
-    );
     lingua:conclusion (
         _:I :measurement10 _:M1
     );
     lingua:premise (
         _:I :measurement1 (_:M1 _:M2)
         _:M1 math:notLessThan _:M2
-    ).
+    );
+    lingua:varCount 3.
 
 # query
 :control_query a lingua:QueryRule;
-    lingua:vars (
-        _:O
-        _:C
-    );
     lingua:premise (
         _:O :control1 _:C
     );
     lingua:conclusion (
         _:O :control1 _:C
-    ).
+    );
+    lingua:varCount 2.
diff --git a/reasoning/lingua/fibonacci.ttl b/reasoning/lingua/fibonacci.ttl
index e70203e54..ec4ba4744 100644
--- a/reasoning/lingua/fibonacci.ttl
+++ b/reasoning/lingua/fibonacci.ttl
@@ -4,46 +4,29 @@
 
 # backward rules
 :fibonacci_rule1 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-    );
     lingua:conclusion (
         _:X :fibonacci _:Y
     );
     lingua:premise (
         (_:X 0 1) :fib _:Y
-    ).
+    );
+    lingua:varCount 2.
 
 :fibonacci_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-        _:B
-    );
     lingua:conclusion (
         (0 _:A _:B) :fib _:A
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 2.
 
 :fibonacci_rule3 a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-        _:B
-    );
     lingua:conclusion (
         (1 _:A _:B) :fib _:B
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 2.
 
 :fibonacci_rule4 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:A
-        _:B
-        _:Y
-        _:C
-        _:D
-    );
     lingua:conclusion (
         (_:X _:A _:B) :fib _:Y
     );
@@ -52,23 +35,18 @@
         (_:X 1) math:difference _:C
         (_:A _:B) math:sum _:D
         (_:C _:B _:D) :fib _:Y
-    ).
+    );
+    lingua:varCount 6.
 
 # query
 :fibonacci_query a lingua:QueryRule;
-    lingua:vars (
-        _:F1
-        _:F2
-        _:F3
-        _:F4
-        _:F5
-    );
     lingua:premise (
         0 :fibonacci _:F1
         1 :fibonacci _:F2
         6 :fibonacci _:F3
         91 :fibonacci _:F4
         283 :fibonacci _:F5
+        3674 :fibonacci _:F6
     );
     lingua:conclusion (
         () :fibonacci (0 _:F1)
@@ -76,4 +54,6 @@
         () :fibonacci (6 _:F3)
         () :fibonacci (91 _:F4)
         () :fibonacci (283 _:F5)
-    ).
+        () :fibonacci (3674 _:F6)
+    );
+    lingua:varCount 6.
diff --git a/reasoning/lingua/forward.ttl b/reasoning/lingua/forward.ttl
index 3881aff56..5dd6e024a 100644
--- a/reasoning/lingua/forward.ttl
+++ b/reasoning/lingua/forward.ttl
@@ -7,24 +7,20 @@
 
 # humans are mortal
 :forward_rule a lingua:ForwardRule;
-    lingua:vars (
-        _:S
-    );
     lingua:premise (
         _:S rdf:type :Human
     );
     lingua:conclusion (
         _:S rdf:type :Mortal
-    ).
+    );
+    lingua:varCount 1.
 
 # query
 :forward_query a lingua:QueryRule;
-    lingua:vars (
-        _:S
-    );
     lingua:premise (
         _:S rdf:type :Mortal
     );
     lingua:conclusion (
         _:S rdf:type :Mortal
-    ).
+    );
+    lingua:varCount 1.
diff --git a/reasoning/lingua/gen.ttl b/reasoning/lingua/gen.ttl
index c3b0534d9..ac0574252 100644
--- a/reasoning/lingua/gen.ttl
+++ b/reasoning/lingua/gen.ttl
@@ -4,17 +4,12 @@
 @prefix : <http://example.org/ns#>.
 
 :gen_rule a lingua:ForwardRule;
-    lingua:vars ();
     lingua:premise ();
     lingua:conclusion (
         :Socrates rdf:type :Human
         :Human rdfs:subClassOf :Mortal
+
         :rdfs_subclass_rule rdf:type lingua:ForwardRule
-        :rdfs_subclass_rule lingua:vars (
-            _:A
-            _:B
-            _:S
-        )
         :rdfs_subclass_rule lingua:premise (
             _:A rdfs:subClassOf _:B
             _:S rdf:type _:A
@@ -22,14 +17,15 @@
         :rdfs_subclass_rule lingua:conclusion (
             _:S rdf:type _:B
         )
+        :rdfs_subclass_rule lingua:varCount 3
+
         :socrates_query rdf:type lingua:QueryRule
-        :socrates_query lingua:vars (
-            _:S
-        )
         :socrates_query lingua:premise (
             _:S rdf:type :Mortal
         )
         :socrates_query lingua:conclusion (
             _:S rdf:type :Mortal
         )
-    ).
+        :socrates_query lingua:varCount 1
+    );
+    lingua:varCount 3.
diff --git a/reasoning/lingua/gps.ttl b/reasoning/lingua/gps.ttl
index 83328e731..2e32bcb3c 100644
--- a/reasoning/lingua/gps.ttl
+++ b/reasoning/lingua/gps.ttl
@@ -7,18 +7,6 @@
 
 # find paths in the state space from initial state to goal state within limits
 :gps_rule1 a lingua:BackwardRule;
-    lingua:vars (
-        _:Goal
-        _:Path
-        _:Duration
-        _:Cost
-        _:Belief
-        _:Comfort
-        _:MaxDuration
-        _:MaxCost
-        _:MinBelief
-        _:MinComfort
-    );
     lingua:conclusion (
         () gps:findpath (_:Goal _:Path _:Duration _:Cost _:Belief _:Comfort
             (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort))
@@ -26,22 +14,10 @@
     lingua:premise (
         () gps:findpaths (() _:Goal () 0.0 0.0 1.0 1.0 _:Path _:Duration _:Cost _:Belief _:Comfort
             (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort 1))
-    ).
+    );
+    lingua:varCount 10.
 
 :gps_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:Goal
-        _:Path
-        _:Duration
-        _:Cost
-        _:Belief
-        _:Comfort
-        _:MaxDuration
-        _:MaxCost
-        _:MinBelief
-        _:MinComfort
-        _:MaxStagecount
-    );
     lingua:conclusion (
         () gps:findpath (_:Goal _:Path _:Duration _:Cost _:Belief _:Comfort
             (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort _:MaxStagecount))
@@ -49,67 +25,20 @@
     lingua:premise (
         () gps:findpaths (() _:Goal () 0.0 0.0 1.0 1.0 _:Path _:Duration _:Cost _:Belief _:Comfort
             (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort _:MaxStagecount))
-    ).
+    );
+    lingua:varCount 11.
 
 :gps_rule3 a lingua:BackwardRule;
-    lingua:vars (
-        _:Maps
-        _:Goal
-        _:Path
-        _:Duration
-        _:Cost
-        _:Belief
-        _:Comfort
-        _:MaxDuration
-        _:MaxCost
-        _:MinBelief
-        _:MinComfort
-        _:MaxStagecount
-    );
     lingua:conclusion (
         () gps:findpaths (_:Maps _:Goal _:Path _:Duration _:Cost _:Belief _:Comfort _:Path _:Duration _:Cost _:Belief _:Comfort
             (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort _:MaxStagecount))
     );
     lingua:premise (
         _:Goal log:call true
-    ).
+    );
+    lingua:varCount 12.
 
 :gps_rule4 a lingua:BackwardRule;
-    lingua:vars (
-        _:Maps_s
-        _:Goal
-        _:Path_s
-        _:Duration_s
-        _:Cost_s
-        _:Belief_s
-        _:Comfort_s
-        _:Path
-        _:Duration
-        _:Cost
-        _:Belief
-        _:Comfort
-        _:MaxDuration
-        _:MaxCost
-        _:MinBelief
-        _:MinComfort
-        _:MaxStagecount
-        _:Map
-        _:From
-        _:Transition
-        _:To
-        _:Action
-        _:Duration_n
-        _:Cost_n
-        _:Belief_n
-        _:Comfort_n
-        _:Maps_t
-        _:Stagecount
-        _:Duration_t
-        _:Cost_t
-        _:Belief_t
-        _:Comfort_t
-        _:Path_t
-    );
     lingua:conclusion (
         () gps:findpaths (_:Maps_s _:Goal _:Path_s _:Duration_s _:Cost_s _:Belief_s _:Comfort_s _:Path _:Duration _:Cost _:Belief _:Comfort
             (_:MaxDuration _:MaxCost _:MinBelief _:MinComfort _:MaxStagecount))
@@ -135,26 +64,18 @@
         ) log:callWithCleanup (
             _:To log:becomes _:From
         )
-    ).
+    );
+    lingua:varCount 33.
 
 # counting the number of stages (a stage is a sequence of steps in the same map)
 :gps_rule5 a lingua:BackwardRule;
-    lingua:vars ();
     lingua:conclusion (
         () gps:stagecount 1
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 0.
 
 :gps_rule6 a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-        _:B
-        _:C
-        _:D
-        _:E
-        _:F
-        _:G
-    );
     lingua:conclusion (
         _:A gps:stagecount _:B
     );
@@ -164,88 +85,65 @@
         _:C log:notEqualTo _:E
         _:D gps:stagecount _:G
         (_:G 1) math:sum _:B
-    ).
+    );
+    lingua:varCount 7.
 
 :gps_rule7 a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-        _:B
-        _:C
-        _:D
-    );
     lingua:conclusion (
         _:A gps:stagecount _:B
     );
     lingua:premise (
         _:A list:firstRest (_:C _:D)
         _:D gps:stagecount _:B
-    ).
+    );
+    lingua:varCount 4.
 
 # current state as practical example
 :i1 :location :Gent.
 
 # map of Belgium
 :gps_rule8 a lingua:BackwardRule;
-    lingua:vars (
-        _:S
-        _:L
-    );
     lingua:conclusion (
         :map-BE gps:description ((_:S :location :Gent) () (_:S :location :Brugge) :drive_gent_brugge 1500.0 0.006 0.96 0.99)
     );
     lingua:premise (
         _:S :location _:L
-    ).
+    );
+    lingua:varCount 2.
 
 :gps_rule9 a lingua:BackwardRule;
-    lingua:vars (
-        _:S
-        _:L
-    );
     lingua:conclusion (
         :map-BE gps:description ((_:S :location :Gent) () (_:S :location :Kortrijk) :drive_gent_kortrijk 1600.0 0.007 0.96 0.99)
     );
     lingua:premise (
         _:S :location _:L
-    ).
+    );
+    lingua:varCount 2.
 
 :gps_rule10 a lingua:BackwardRule;
-    lingua:vars (
-        _:S
-        _:L
-    );
     lingua:conclusion (
         :map-BE gps:description ((_:S :location :Kortrijk) () (_:S :location :Brugge) :drive_kortrijk_brugge 1600.0 0.007 0.96 0.99)
     );
     lingua:premise (
         _:S :location _:L
-    ).
+    );
+    lingua:varCount 2.
 
 :gps_rule11 a lingua:BackwardRule;
-    lingua:vars (
-        _:S
-        _:L
-    );
     lingua:conclusion (
         :map-BE gps:description ((_:S :location :Brugge) () (_:S :location :Oostende) :drive_brugge_oostende 900.0 0.004 0.98 1.0)
     );
     lingua:premise (
         _:S :location _:L
-    ).
+    );
+    lingua:varCount 2.
 
 # query
 :gps_query a lingua:QueryRule;
-    lingua:vars (
-        _:SUBJECT
-        _:PATH
-        _:DURATION
-        _:COST
-        _:BELIEF
-        _:COMFORT
-    );
     lingua:premise (
         () gps:findpath ((_:SUBJECT :location :Oostende) _:PATH _:DURATION _:COST _:BELIEF _:COMFORT (5000.0 5.0 0.2 0.4 1))
     );
     lingua:conclusion (
         _:SUBJECT gps:path (_:PATH _:DURATION _:COST _:BELIEF _:COMFORT)
-    ).
+    );
+    lingua:varCount 6.
diff --git a/reasoning/lingua/graph.ttl b/reasoning/lingua/graph.ttl
index 1961e4cac..3be1315a6 100644
--- a/reasoning/lingua/graph.ttl
+++ b/reasoning/lingua/graph.ttl
@@ -15,40 +15,31 @@
 
 # oneway subproperty of path
 :graph_rule1 a lingua:ForwardRule;
-    lingua:vars (
-        _:A
-        _:B
-    );
     lingua:premise (
         _:A :oneway _:B
     );
     lingua:conclusion (
         _:A :path _:B
-    ).
+    );
+    lingua:varCount 2.
 
 # path transitive property
 :graph_rule2 a lingua:ForwardRule;
-    lingua:vars (
-        _:A
-        _:B
-        _:C
-    );
     lingua:premise (
         _:A :path _:B
         _:B :path _:C
     );
     lingua:conclusion (
         _:A :path _:C
-    ).
+    );
+    lingua:varCount 3.
 
 # query
 :graph_query a lingua:QueryRule;
-    lingua:vars (
-        _:A
-    );
     lingua:premise (
         _:A :path :nantes
     );
     lingua:conclusion (
         _:A :path :nantes
-    ).
+    );
+    lingua:varCount 1.
diff --git a/reasoning/lingua/hanoi.ttl b/reasoning/lingua/hanoi.ttl
index 74897f22c..9aec5c5ca 100644
--- a/reasoning/lingua/hanoi.ttl
+++ b/reasoning/lingua/hanoi.ttl
@@ -5,16 +5,6 @@
 
 # _:M is the sequence of moves to move _:N disks from _:X to _:Y using _:Z as intermediary
 :hanoi_rule1 a lingua:BackwardRule;
-    lingua:vars (
-        _:N
-        _:X
-        _:Y
-        _:Z
-        _:M
-        _:N1
-        _:M1
-        _:M2
-    );
     lingua:conclusion (
         (_:N _:X _:Y _:Z) :moves _:M
     );
@@ -24,27 +14,22 @@
         (_:N1 _:X _:Z _:Y) :moves _:M1
         (_:N1 _:Z _:Y _:X) :moves _:M2
         (_:M1 ((_:X _:Y)) _:M2) list:append _:M
-    ).
+    );
+    lingua:varCount 8.
 
 :hanoi_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-        _:Z
-    );
     lingua:conclusion (
         (1 _:X _:Y _:Z) :moves ((_:X _:Y))
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 3.
 
 # query
 :hanoi_query a lingua:QueryRule;
-    lingua:vars (
-        _:M
-    );
     lingua:premise (
         (7 :left :right :center) :moves _:M
     );
     lingua:conclusion (
         (7 :left :right :center) :moves _:M
-    ).
+    );
+    lingua:varCount 1.
diff --git a/reasoning/lingua/negation.ttl b/reasoning/lingua/negation.ttl
index 9bf672ebf..cd91ea98d 100644
--- a/reasoning/lingua/negation.ttl
+++ b/reasoning/lingua/negation.ttl
@@ -3,38 +3,32 @@
 
 # saying A means saying C
 :negation_predicates_rule1 a lingua:ForwardRule;
-    lingua:vars (
-        _:S
-    );
     lingua:premise (
         _:S :saying :A
     );
     lingua:conclusion (
         _:S :saying :C
-    ).
+    );
+    lingua:varCount 1.
 
 :negation_predicates_rule2 a lingua:ForwardRule;
-    lingua:vars (
-        _:S
-    );
     lingua:premise (
         _:S :not_saying :C
     );
     lingua:conclusion (
         _:S :not_saying :A
-    ).
+    );
+    lingua:varCount 1.
 
 # saying B means saying C
 :negation_predicates_rule3 a lingua:ForwardRule;
-    lingua:vars (
-        _:S
-    );
     lingua:premise (
         _:S :saying :B
     );
     lingua:conclusion (
         _:S :saying :C
-    ).
+    );
+    lingua:varCount 1.
 
 :negation_predicates_rule4 a lingua:ForwardRule;
     lingua:premise (
@@ -46,26 +40,22 @@
 
 # saying A or saying B
 :negation_predicates_rule5 a lingua:ForwardRule;
-    lingua:vars (
-        _:S
-    );
     lingua:premise (
         _:S :not_saying :A
     );
     lingua:conclusion (
         _:S :saying :B
-    ).
+    );
+    lingua:varCount 1.
 
 :negation_predicates_rule6 a lingua:ForwardRule;
-    lingua:vars (
-        _:S
-    );
     lingua:premise (
         _:S :not_saying :B
     );
     lingua:conclusion (
         _:S :saying :A
-    ).
+    );
+    lingua:varCount 1.
 
 # assuming the negation of the query so that
 # it can be discharged when the query succeeds
@@ -73,10 +63,10 @@
 
 # query
 :negation_predicates_query a lingua:QueryRule;
-    lingua:vars ();
     lingua:premise (
         :alice :saying :C
     );
     lingua:conclusion (
         :alice :saying :C
-    ).
+    );
+    lingua:varCount 0.
diff --git a/reasoning/lingua/notequal.ttl b/reasoning/lingua/notequal.ttl
index eddc70e59..cf41ff2af 100644
--- a/reasoning/lingua/notequal.ttl
+++ b/reasoning/lingua/notequal.ttl
@@ -18,14 +18,6 @@
 
 #query
 :union_query a lingua:QueryRule;
-    lingua:vars (
-        _:X1
-        _:X2
-        _:X3
-        _:Y
-        _:Y_RT
-        _:X3_RT
-    );
     lingua:premise (
         :Let :param1 _:X1
         :Let :param2 _:X2
@@ -37,4 +29,5 @@
     );
     lingua:conclusion (
         :test :is true
-).
+    );
+    lingua:varCount 6.
diff --git a/reasoning/lingua/out/fibonacci.ttl b/reasoning/lingua/out/fibonacci.ttl
index 1fbba576f..4b8136bbd 100644
--- a/reasoning/lingua/out/fibonacci.ttl
+++ b/reasoning/lingua/out/fibonacci.ttl
@@ -5,3 +5,4 @@
 () :fibonacci (6 8).
 () :fibonacci (91 4660046610375530309).
 () :fibonacci (283 62232491515607091882574410635924603070626544377175485625797).
+() :fibonacci (3674 295872959797101479478634366815157108100573212705250690577871041398423606408217262643449728342664061812585639168722421830407677671667740585806703531229882783069925750619720511808616484846128237251921414441458265138672827487722512845223115526738192067144721087756159352711138340620702266509343657403678256247195010013499661223527119909308682062873140767135468966093474944529418214755911968500799987099146489838560114063096775586903976827512299123202488315139397181279903459556726060805948910609527571241968534269554079076649680403030083743420820438603816095671532163428933363322524736324029745871445486444623006627119156710782085648303485296149604974010598940800770684835758031137479033374229914629583184427269638360355586190323578625395157899987377625662075558684705457).
diff --git a/reasoning/lingua/patch.ttl b/reasoning/lingua/patch.ttl
index 0d7d0be56..2694ed531 100644
--- a/reasoning/lingua/patch.ttl
+++ b/reasoning/lingua/patch.ttl
@@ -12,9 +12,6 @@
 
 # patch rule
 :patch_rule a lingua:ForwardRule;
-    lingua:vars (
-        _:person
-    );
     lingua:premise (
         _:person :familyName "Garcia"
         (
@@ -23,15 +20,11 @@
             _:person :givenName "Alex"
         )
     );
-    lingua:conclusion ().
+    lingua:conclusion ();
+    lingua:varCount 1.
 
 # query
 :patch_query a lingua:QueryRule;
-    lingua:vars (
-        _:person
-        _:fname
-        _:gname
-    );    
     lingua:premise (
         _:person :familyName _:fname
         _:person :givenName _:gname
@@ -39,4 +32,5 @@
     lingua:conclusion (
         _:person :familyName _:fname
         _:person :givenName _:gname
-    ).
+    );
+    lingua:varCount 3.
diff --git a/reasoning/lingua/peano.ttl b/reasoning/lingua/peano.ttl
index 97fca3802..89d93bdfc 100644
--- a/reasoning/lingua/peano.ttl
+++ b/reasoning/lingua/peano.ttl
@@ -3,96 +3,68 @@
 
 # add
 :peano_add_rule1 a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-    );
     lingua:conclusion (
         (_:A 0) :add _:A
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 1.
 
 :peano_add_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-        _:B
-        _:C
-    );
     lingua:premise (
         (_:A _:B) :add _:C
     );
     lingua:conclusion (
         (_:A (:s _:B)) :add (:s _:C)
-    ).
+    );
+    lingua:varCount 3.
 
 # multiply
 :peano_multiply_rule1 a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-    );
     lingua:conclusion (
         (_:A 0) :multiply 0
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 1.
 
 :peano_multiply_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-        _:B
-        _:C
-        _:D
-    );
     lingua:conclusion (
         (_:A (:s _:B)) :multiply _:C
     );
     lingua:premise (
         (_:A _:B) :multiply _:D
         (_:A _:D) :add _:C
-    ).
+    );
+    lingua:varCount 4.
 
 # factorial
 :peano_factorial_rule1 a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-        _:B
-    );
     lingua:conclusion (
         _:A :factorial _:B
     );
     lingua:premise (
         (_:A (:s 0)) :fac _:B
-    ).
+    );
+    lingua:varCount 2.
 
 :peano_factorial_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-    );
     lingua:conclusion (
         (0 _:A) :fac _:A
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 1.
 
 :peano_factorial_rule3 a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-        _:B
-        _:C
-        _:D
-    );
     lingua:conclusion (
         ((:s _:A) _:B) :fac _:C
     );
     lingua:premise (
         (_:B (:s _:A)) :multiply _:D
         (_:A _:D) :fac _:C
-    ).
+    );
+    lingua:varCount 4.
 
 # query
 :peano_query a lingua:QueryRule;
-    lingua:vars (
-        _:A
-        _:B
-        _:C
-    );
     lingua:premise (
         ((:s 0) (:s 0)) :add _:A
         (_:A (:s (:s 0))) :multiply _:B
@@ -100,4 +72,5 @@
     );
     lingua:conclusion (
         :result :is _:C
-    ).
+    );
+    lingua:varCount 3.
diff --git a/reasoning/lingua/pi.ttl b/reasoning/lingua/pi.ttl
index 074d9bfb0..296d674bc 100644
--- a/reasoning/lingua/pi.ttl
+++ b/reasoning/lingua/pi.ttl
@@ -3,12 +3,6 @@
 @prefix : <http://example.org/ns#>.
 
 :pi_rule1 a lingua:BackwardRule;
-    lingua:vars (
-        _:N
-        _:Pi
-        _:P
-        _:A
-    );
     lingua:conclusion (
         (_:N _:Pi) :pi true
     );
@@ -16,35 +10,17 @@
         (1 _:N 0 _:P 1) :pi true
         (4 _:P) math:product _:A
         (3 _:A) math:sum _:Pi
-    ).
+    );
+    lingua:varCount 4.
 
 :pi_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:N
-        _:P
-        _:S
-    );
     lingua:conclusion (
         (_:N _:N _:P _:P _:S) :pi true
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 3.
 
 :pi_rule3 a lingua:BackwardRule;
-    lingua:vars (
-        _:K
-        _:N
-        _:P0
-        _:P
-        _:S
-        _:K1
-        _:K2
-        _:A
-        _:B
-        _:C
-        _:D
-        _:P1
-        _:S1
-    );
     lingua:conclusion (
         (_:K _:N _:P0 _:P _:S) :pi true
     );
@@ -59,16 +35,15 @@
         (_:P0 _:D) math:sum _:P1
         _:S math:negation _:S1
         (_:K1 _:N _:P1 _:P _:S1) :pi true
-    ).
+    );
+    lingua:varCount 13.
 
 # query
 :pi_query a lingua:QueryRule;
-    lingua:vars (
-        _:Pi
-    );
     lingua:premise (
         (1000 _:Pi) :pi true
     );
     lingua:conclusion (
         (1000 _:Pi) :pi true
-    ).
+    );
+    lingua:varCount 1.
diff --git a/reasoning/lingua/sdcoding.ttl b/reasoning/lingua/sdcoding.ttl
index 260779a0d..585ec9181 100644
--- a/reasoning/lingua/sdcoding.ttl
+++ b/reasoning/lingua/sdcoding.ttl
@@ -40,146 +40,102 @@
 
 # KG
 :sdcoding_rule1 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-        _:Z
-    );
     lingua:conclusion (
         _:X :kg _:Y
     );
     lingua:premise (
         _:X :g _:Z
         _:Z :k _:Y
-    ).
+    );
+    lingua:varCount 3.
 
 # GK
 :sdcoding_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-        _:Z
-    );
     lingua:conclusion (
         _:X :gk _:Y
     );
     lingua:premise (
         _:X :k _:Z
         _:Z :g _:Y
-    ).
+    );
+    lingua:varCount 3.
 
 # Alice
 :sdcoding_rule3 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-    );
     lingua:conclusion (
         0 :alice (_:X _:Y)
     );
     lingua:premise (
         _:X :id _:Y
-    ).
+    );
+    lingua:varCount 2.
 
 :sdcoding_rule4 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-    );
     lingua:conclusion (
         1 :alice (_:X _:Y)
     );
     lingua:premise (
         _:X :g _:Y
-    ).
+    );
+    lingua:varCount 2.
 
 :sdcoding_rule5 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-    );
     lingua:conclusion (
         2 :alice (_:X _:Y)
     );
     lingua:premise (
         _:X :k _:Y
-    ).
+    );
+    lingua:varCount 2.
 
 :sdcoding_rule6 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-    );
     lingua:conclusion (
         3 :alice (_:X _:Y)
     );
     lingua:premise (
         _:X :kg _:Y
-    ).
+    );
+    lingua:varCount 2.
 
 # Bob
 :sdcoding_rule7 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-    );
     lingua:conclusion (
         (_:X _:Y) :bob 0
     );
     lingua:premise (
         _:X :gk _:Y
-    ).
+    );
+    lingua:varCount 2.
 
 :sdcoding_rule8 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-    );
     lingua:conclusion (
         (_:X _:Y) :bob 1
     );
     lingua:premise (
         _:X :k _:Y
-    ).
+    );
+    lingua:varCount 2.
 
 :sdcoding_rule9 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-    );
     lingua:conclusion (
         (_:X _:Y) :bob 2
     );
     lingua:premise (
         _:X :g _:Y
-    ).
+    );
+    lingua:varCount 2.
 
 :sdcoding_rule10 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-    );
     lingua:conclusion (
         (_:X _:Y) :bob 3
     );
     lingua:premise (
         _:X :id _:Y
-    ).
+    );
+    lingua:varCount 2.
 
 # superdense coding
 :sdcoding_rule11 a lingua:ForwardRule;
-    lingua:vars (
-        _:N
-        _:A
-        _:B
-        _:M
-        _:X
-        _:Y
-        _:Z
-        _:L
-        _:S
-        _:I
-    );
     lingua:premise (
         _:N :alice _:A
         _:B :bob _:M
@@ -197,17 +153,15 @@
     );
     lingua:conclusion (
         _:N :sdcoding _:M
-    ).
+    );
+    lingua:varCount 10.
 
 # query
 :sdcoding_query a lingua:QueryRule;
-    lingua:vars (
-        _:N
-        _:M
-    );
     lingua:premise (
         _:N :sdcoding _:M
     );
     lingua:conclusion (
         () :sdcoding (_:N _:M)
-    ).
+    );
+    lingua:varCount 2.
diff --git a/reasoning/lingua/sha512.ttl b/reasoning/lingua/sha512.ttl
index b6ad78515..6b0316641 100644
--- a/reasoning/lingua/sha512.ttl
+++ b/reasoning/lingua/sha512.ttl
@@ -6,14 +6,11 @@
 
 # query
 :sha512_query a lingua:QueryRule;
-    lingua:vars (
-        _:X
-        _:Y
-    );
     lingua:premise (
         :Let :param _:X
         _:X crypto:sha512 _:Y
     );
     lingua:conclusion (
         () :sha512 (_:X _:Y)
-    ).
+    );
+    lingua:varCount 2.
diff --git a/reasoning/lingua/socrates.ttl b/reasoning/lingua/socrates.ttl
index 2d0b36313..4bd34bdad 100644
--- a/reasoning/lingua/socrates.ttl
+++ b/reasoning/lingua/socrates.ttl
@@ -9,27 +9,21 @@
 
 # rdfs subclass
 :rdfs_subclass_rule a lingua:ForwardRule;
-    lingua:vars (
-        _:A
-        _:B
-        _:S
-    );
     lingua:premise (
         _:A rdfs:subClassOf _:B
         _:S rdf:type _:A
     );
     lingua:conclusion (
         _:S rdf:type _:B
-    ).
+    );
+    lingua:varCount 3.
 
 # query
 :socrates_query a lingua:QueryRule;
-    lingua:vars (
-        _:S
-    );
     lingua:premise (
         _:S rdf:type :Mortal
     );
     lingua:conclusion (
         _:S rdf:type :Mortal
-    ).
+    );
+    lingua:varCount 1.
diff --git a/reasoning/lingua/turing.ttl b/reasoning/lingua/turing.ttl
index 5bad6ae64..7a8696e43 100644
--- a/reasoning/lingua/turing.ttl
+++ b/reasoning/lingua/turing.ttl
@@ -5,28 +5,16 @@
 
 # interpreter for Turing machine
 :turing_rule1 a lingua:BackwardRule;
-    lingua:vars (
-        _:OutTape
-        _:Machine
-        _:I
-    );
     lingua:conclusion (
         () :compute _:OutTape
     );
     lingua:premise (
         _:Machine :start _:I
         (_:I () "#" ()) :find _:OutTape
-    ).
+    );
+    lingua:varCount 3.
 
 :turing_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:List
-        _:OutTape
-        _:Head
-        _:Tail
-        _:Machine
-        _:I
-    );
     lingua:conclusion (
         _:List :compute _:OutTape
     );
@@ -34,22 +22,10 @@
         _:List list:firstRest (_:Head _:Tail)
         _:Machine :start _:I
         (_:I () _:Head _:Tail) :find _:OutTape
-    ).
+    );
+    lingua:varCount 6.
 
 :turing_rule3 a lingua:BackwardRule;
-    lingua:vars (
-        _:State
-        _:Left
-        _:Cell
-        _:Right
-        _:OutTape
-        _:Write
-        _:Move
-        _:Next
-        _:A
-        _:B
-        _:C
-    );
     lingua:conclusion (
         (_:State _:Left _:Cell _:Right) :find _:OutTape
     );
@@ -57,17 +33,10 @@
         (_:State _:Cell _:Write _:Move) :tape _:Next
         (_:Move _:Left _:Write _:Right _:A _:B _:C) :move true
         (_:Next _:A _:B _:C) :continue _:OutTape
-    ).
+    );
+    lingua:varCount 11.
 
 :turing_rule4 a lingua:BackwardRule;
-    lingua:vars (
-        _:Left
-        _:Cell
-        _:Right
-        _:OutTape
-        _:R
-        _:List
-    );
     lingua:conclusion (
         (:halt _:Left _:Cell _:Right) :continue _:OutTape
     );
@@ -75,109 +44,71 @@
         _:Left :reverse _:R
         _:List list:firstRest (_:Cell _:Right)
         (_:R _:List) list:append _:OutTape
-    ).
+    );
+    lingua:varCount 6.
 
 :turing_rule5 a lingua:BackwardRule;
-    lingua:vars (
-        _:State
-        _:Left
-        _:Cell
-        _:Right
-        _:OutTape
-    );
     lingua:conclusion (
         (_:State _:Left _:Cell _:Right) :continue _:OutTape
     );
     lingua:premise (
         (_:State _:Left _:Cell _:Right) :find _:OutTape
-    ).
+    );
+    lingua:varCount 5.
 
 :turing_rule6 a lingua:BackwardRule;
-    lingua:vars (
-        _:Cell
-        _:Right
-        _:L
-    );
     lingua:conclusion (
         (:left () _:Cell _:Right () "#" _:L) :move true
     );
     lingua:premise (
         _:L list:firstRest (_:Cell _:Right)
-    ).
+    );
+    lingua:varCount 3.
 
 :turing_rule7 a lingua:BackwardRule;
-    lingua:vars (
-        _:List
-        _:Cell
-        _:Right
-        _:Tail
-        _:Head
-        _:L
-    );
     lingua:conclusion (
         (:left _:List _:Cell _:Right _:Tail _:Head _:L) :move true
     );
     lingua:premise (
         _:List list:firstRest (_:Head _:Tail)
         _:L list:firstRest (_:Cell _:Right)
-    ).
+    );
+    lingua:varCount 6.
 
 :turing_rule8 a lingua:BackwardRule;
-    lingua:vars (
-        _:Left
-        _:Cell
-        _:Right
-    );
     lingua:conclusion (
         (:stop _:Left _:Cell _:Right _:Left _:Cell _:Right) :move true
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 3.
 
 :turing_rule9 a lingua:BackwardRule;
-    lingua:vars (
-        _:Left
-        _:Cell
-        _:L
-    );
     lingua:conclusion (
         (:right _:Left _:Cell () _:L "#" ()) :move true
     );
     lingua:premise (
         _:L list:firstRest (_:Cell _:Left)
-    ).
+    );
+    lingua:varCount 3.
 
 :turing_rule10 a lingua:BackwardRule;
-    lingua:vars (
-        _:Left
-        _:Cell
-        _:List
-        _:L
-        _:Head
-        _:Tail
-    );
     lingua:conclusion (
         (:right _:Left _:Cell _:List _:L _:Head _:Tail) :move true
     );
     lingua:premise (
         _:List list:firstRest (_:Head _:Tail)
         _:L list:firstRest (_:Cell _:Left)
-    ).
+    );
+    lingua:varCount 6.
 
 :turing_rule11 a lingua:BackwardRule;
-    lingua:vars ();
     lingua:conclusion (
         () :reverse ()
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 0.
 
 :turing_rule12 a lingua:BackwardRule;
-    lingua:vars (
-        _:List
-        _:Reverse
-        _:Head
-        _:Tail
-        _:R
-    );
     lingua:conclusion (
         _:List :reverse _:Reverse
     );
@@ -185,7 +116,8 @@
         _:List list:firstRest (_:Head _:Tail)
         _:Tail :reverse _:R
         (_:R (_:Head)) list:append _:Reverse
-    ).
+    );
+    lingua:varCount 5.
 
 # a Turing machine to add 1 to a binary number
 :add1 :start 0.
@@ -199,12 +131,6 @@
 
 # query
 :turing_query a lingua:QueryRule;
-    lingua:vars (
-        _:A1
-        _:A2
-        _:A3
-        _:A4
-    );
     lingua:premise (
         (1 0 1 0 0 1) :compute _:A1
         (1 0 1 1 1 1) :compute _:A2
@@ -216,4 +142,5 @@
         (1 0 1 1 1 1) :compute _:A2
         (1 1 1 1 1 1) :compute _:A3
         () :compute _:A4
-    ).
+    );
+    lingua:varCount 4.
diff --git a/reasoning/lingua/union.ttl b/reasoning/lingua/union.ttl
index d531952cb..dfc9933cd 100644
--- a/reasoning/lingua/union.ttl
+++ b/reasoning/lingua/union.ttl
@@ -16,11 +16,6 @@
 
 #query
 :union_query a lingua:QueryRule;
-    lingua:vars (
-        _:X1
-        _:X2
-        _:Y
-    );
     lingua:premise (
         :Let :param1 _:X1
         :Let :param2 _:X2
@@ -28,4 +23,5 @@
     );
     lingua:conclusion (
         (_:X1 _:X2) :union _:Y
-).
+    );
+    lingua:varCount 3.
diff --git a/reasoning/lingua/universal.ttl b/reasoning/lingua/universal.ttl
index 59d94421a..02b250c3c 100644
--- a/reasoning/lingua/universal.ttl
+++ b/reasoning/lingua/universal.ttl
@@ -6,53 +6,42 @@
 
 # \Every x: type(x, Resource
 :universal_statements_rule1 a lingua:BackwardRule;
-    lingua:vars (
-        _:X
-    );
     lingua:conclusion (
         _:X rdf:type rdfs:Resource
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 1.
 
 # Everybody loves somebody who is lonely
 :universal_statements_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:A
-        _:B
-    );
     lingua:conclusion (
         _:A :loves _:B
     );
     lingua:premise (
         (_:A) log:skolem _:B
-    ).
+    );
+    lingua:varCount 2.
 
 :universal_statements_rule3 a lingua:BackwardRule;
-    lingua:vars (
-        _:B
-        _:A
-    );
     lingua:conclusion (
         _:B :is :lonely
     );
     lingua:premise (
         (_:A) log:skolem _:B
-    ).
+    );
+    lingua:varCount 2.
 
 # queries
 :universal_statements_query1 a lingua:QueryRule;
-    lingua:vars ();
     lingua:premise (
         :pat rdf:type rdfs:Resource
     );
     lingua:conclusion (
         :pat rdf:type rdfs:Resource
-    ).
+    );
+    lingua:varCount 0.
 
 :universal_statements_query2 a lingua:QueryRule;
-    lingua:vars (
-        _:X
-    );
     lingua:premise (
         :bob :loves _:X
         _:X :is :lonely
@@ -60,4 +49,5 @@
     lingua:conclusion (
         :bob :loves _:X
         _:X :is :lonely
-    ).
+    );
+    lingua:varCount 1.
diff --git a/reasoning/lingua/unpack.ttl b/reasoning/lingua/unpack.ttl
index de5a792f3..a3a2cb8e9 100644
--- a/reasoning/lingua/unpack.ttl
+++ b/reasoning/lingua/unpack.ttl
@@ -31,21 +31,13 @@ _:b1 :data (
 
 # the logic for unpack using backward rules
 :unpack_rule1 a lingua:BackwardRule;
-    lingua:vars ();
     lingua:conclusion (
         () :unpackl ()
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 0.
 
 :unpack_rule2 a lingua:BackwardRule;
-    lingua:vars (
-        _:g
-        _:h
-        _:f
-        _:r
-        _:a
-        _:b
-    );
     lingua:conclusion (
         _:g :unpackl _:h
     );
@@ -54,19 +46,10 @@ _:b1 :data (
         _:f :unpack _:a
         _:r :unpackl _:b
         (_:a _:b) list:append _:h
-    ).
+    );
+    lingua:varCount 6.
 
 :unpack_rule3 a lingua:BackwardRule;
-    lingua:vars (
-        _:b
-        _:p
-        _:f
-        _:l
-        _:a
-        _:c
-        _:t
-        _:d
-    );
     lingua:conclusion (
         (_:b :package _:p) :unpack _:f
     );
@@ -77,17 +60,10 @@ _:b1 :data (
         (:tomorrow :next_week) list:member _:t
         _:c list:lott _:d
         _:d :unpackl _:f
-    ).
+    );
+    lingua:varCount 8.
 
 :unpack_rule4 a lingua:BackwardRule;
-    lingua:vars (
-        _:b
-        _:p
-        _:l
-        _:a
-        _:c
-        _:t
-    );
     lingua:conclusion (
         (_:b :package _:p) :unpack ()
     );
@@ -96,47 +72,33 @@ _:b1 :data (
         _:l list:member (_:a :content _:c)
         _:l list:member (_:a :usable_until _:t)
         (:yesterday :last_week) list:member _:t
-    ).
+    );
+    lingua:varCount 6.
 
 :unpack_rule5 a lingua:BackwardRule;
-    lingua:vars (
-        _:b
-        _:p
-    );
     lingua:conclusion (
         (_:b :tag _:p) :unpack ()
     );
-    lingua:premise ().
+    lingua:premise ();
+    lingua:varCount 2.
 
 :unpack_rule6 a lingua:BackwardRule;
-    lingua:vars (
-        _:g
-        _:a
-        _:p
-        _:b
-        _:q
-    );
     lingua:conclusion (
         _:g :unpack (_:g)
     );
     lingua:premise (
         (_:g) list:notMember (_:a :package _:p)
         (_:g) list:notMember (_:b :tag _:q)
-    ).
+    );
+    lingua:varCount 5.
 
 # unpack the triples that are usable in the future
 :unpack_query a lingua:QueryRule;
-    lingua:vars (
-        _:b
-        _:g
-        _:l
-        _:m
-        _:u
-    );
     lingua:premise (
         _:b :data _:g
         _:g list:lott _:l
         _:l :unpackl _:m
         _:u list:lott _:m
     );
-    lingua:conclusion _:u.
+    lingua:conclusion _:u;
+    lingua:varCount 5.
diff --git a/reasoning/lingua/witch.ttl b/reasoning/lingua/witch.ttl
index c815dea1e..8ddebea15 100644
--- a/reasoning/lingua/witch.ttl
+++ b/reasoning/lingua/witch.ttl
@@ -4,60 +4,51 @@
 
 # \forall x : BURNS(x) /\ WOMAN(x) => WITCH(x
 :witch_rule1 a lingua:ForwardRule;
-    lingua:vars (
-        _:X
-    );
     lingua:premise (
         _:X rdf:type :BURNS
         _:X rdf:type :WOMAN
     );
     lingua:conclusion (
         _:X rdf:type :WITCH
-    ).
+    );
+    lingua:varCount 1.
 
 # WOMAN(GIRL
 :GIRL a :WOMAN.
 
 # \forall x : ISMADEOFWOOD(x) => BURNS(x
 :witch_rule2 a lingua:ForwardRule;
-    lingua:vars (
-        _:X
-    );
     lingua:premise (
         _:X rdf:type :ISMADEOFWOOD
     );
     lingua:conclusion (
         _:X rdf:type :BURNS
-    ).
+    );
+    lingua:varCount 1.
 
 # \forall x : FLOATS(x) => ISMADEOFWOOD(x
 :witch_rule3 a lingua:ForwardRule;
-    lingua:vars (
-        _:X
-    );
     lingua:premise (
         _:X rdf:type :FLOATS
     );
     lingua:conclusion (
         _:X rdf:type :ISMADEOFWOOD
-    ).
+    );
+    lingua:varCount 1.
 
 # FLOATS(DUCK
 :DUCK a :FLOATS.
 
 # \forall x,y : FLOATS(x) /\ SAMEWEIGHT(x,y) => FLOATS(y
 :witch_rule4 a lingua:ForwardRule;
-    lingua:vars (
-        _:X
-        _:Y
-    );
     lingua:premise (
         _:X rdf:type :FLOATS
         _:X :SAMEWEIGHT _:Y
     );
     lingua:conclusion (
         _:Y rdf:type :FLOATS
-    ).
+    );
+    lingua:varCount 2.
 
 # and, by experiment
 # SAMEWEIGHT(DUCK,GIRL
@@ -65,12 +56,10 @@
 
 # who's a witch?
 :witch_query a lingua:QueryRule;
-    lingua:vars (
-        _:S
-    );
     lingua:premise (
         _:S rdf:type :WITCH
     );
     lingua:conclusion (
         _:S rdf:type :WITCH
-    ).
+    );
+    lingua:varCount 1.