From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 25 Jul 2007 09:43:35 +0000 (+0000)
Subject: used ;try assumption instead of .try assumption
X-Git-Tag: make_still_working~6130
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=4441b81ba3179696c42ebc8ab720d1ba0f67078a;p=helm.git

used ;try assumption instead of .try assumption
---

diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO001-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO001-1.p.ma
index 38c012e5a..87ee6a7c5 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO001-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO001-1.p.ma
@@ -59,7 +59,7 @@ theorem prove_inverse_is_self_cancelling:
 \forall H4:\forall V:Univ.\forall W:Univ.\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (multiply (multiply V W X) Y (multiply V W Z)) (multiply V W (multiply X Y Z)).eq Univ (inverse (inverse a)) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO003-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO003-2.p.ma
index cbbae8bea..a964a96ad 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO003-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO003-2.p.ma
@@ -68,7 +68,7 @@ theorem prove_a_times_a_is_a:
 \forall H13:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (multiply a a) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO003-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO003-4.p.ma
index b5fed12ac..efeca0198 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO003-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO003-4.p.ma
@@ -62,7 +62,7 @@ theorem prove_a_times_a_is_a:
 \forall H7:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (multiply a a) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO004-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO004-2.p.ma
index cd5cb41d8..ff3cd85f9 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO004-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO004-2.p.ma
@@ -68,7 +68,7 @@ theorem prove_a_plus_a_is_a:
 \forall H13:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (add a a) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO004-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO004-4.p.ma
index c173d004c..1821077fe 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO004-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO004-4.p.ma
@@ -62,7 +62,7 @@ theorem prove_a_plus_a_is_a:
 \forall H7:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (add a a) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO005-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO005-2.p.ma
index e3e65f488..5e3def47c 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO005-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO005-2.p.ma
@@ -69,7 +69,7 @@ theorem prove_a_plus_1_is_a:
 \forall H13:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (add a multiplicative_identity) multiplicative_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO005-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO005-4.p.ma
index 655401b34..9bd9ce8a9 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO005-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO005-4.p.ma
@@ -63,7 +63,7 @@ theorem prove_a_plus_1_is_a:
 \forall H7:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (add a multiplicative_identity) multiplicative_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO006-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO006-2.p.ma
index 69b96f774..77ea2d76b 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO006-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO006-2.p.ma
@@ -68,7 +68,7 @@ theorem prove_right_identity:
 \forall H13:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (multiply a additive_identity) additive_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO006-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO006-4.p.ma
index 6b9db399f..c05bd84fc 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO006-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO006-4.p.ma
@@ -62,7 +62,7 @@ theorem prove_right_identity:
 \forall H7:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (multiply a additive_identity) additive_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO009-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO009-2.p.ma
index 201ba75c3..ce93dc23b 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO009-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO009-2.p.ma
@@ -69,7 +69,7 @@ theorem prove_operation:
 \forall H13:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (multiply a (add a b)) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO009-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO009-4.p.ma
index 1987e3b12..67631beb7 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO009-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO009-4.p.ma
@@ -63,7 +63,7 @@ theorem prove_operation:
 \forall H7:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (multiply a (add a b)) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO010-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO010-2.p.ma
index f177f9c74..9517fa3ed 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO010-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO010-2.p.ma
@@ -69,7 +69,7 @@ theorem prove_a_plus_ab_is_a:
 \forall H13:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (add a (multiply a b)) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO010-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO010-4.p.ma
index 7b22061df..6cd030d5a 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO010-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO010-4.p.ma
@@ -63,7 +63,7 @@ theorem prove_a_plus_ab_is_a:
 \forall H7:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (add a (multiply a b)) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO011-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO011-2.p.ma
index b0c35a767..33f8f9a87 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO011-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO011-2.p.ma
@@ -69,7 +69,7 @@ theorem prove_inverse_of_1_is_0:
 \forall H13:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (inverse additive_identity) multiplicative_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO011-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO011-4.p.ma
index 3353f8df4..5855e8aee 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO011-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO011-4.p.ma
@@ -62,7 +62,7 @@ theorem prove_inverse_of_1_is_0:
 \forall H7:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (inverse additive_identity) multiplicative_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO012-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO012-2.p.ma
index 209840c60..3572d8750 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO012-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO012-2.p.ma
@@ -68,7 +68,7 @@ theorem prove_inverse_is_an_involution:
 \forall H13:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (inverse (inverse x)) x
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO012-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO012-4.p.ma
index a3bfe1c4b..fb67030b9 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO012-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO012-4.p.ma
@@ -62,7 +62,7 @@ theorem prove_inverse_is_an_involution:
 \forall H7:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (inverse (inverse x)) x
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO013-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO013-2.p.ma
index 1b7800d75..0f538a7da 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO013-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO013-2.p.ma
@@ -76,7 +76,7 @@ theorem prove_b_is_a:
 \forall H17:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ b c
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO013-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO013-4.p.ma
index 446b2b473..f4b986a97 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO013-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO013-4.p.ma
@@ -65,7 +65,7 @@ theorem prove_a_inverse_is_b:
 \forall H9:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ b (inverse a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO016-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO016-2.p.ma
index a8d1ab9e7..ee7c9969c 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO016-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO016-2.p.ma
@@ -71,7 +71,7 @@ theorem prove_sum:
 \forall H14:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (add x z) x
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO017-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO017-2.p.ma
index 60ded0c1a..5691fcfb0 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO017-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO017-2.p.ma
@@ -71,7 +71,7 @@ theorem prove_sum:
 \forall H14:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (multiply x z) x
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO018-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO018-4.p.ma
index 8e2774c34..32fe9a460 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO018-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO018-4.p.ma
@@ -62,7 +62,7 @@ theorem prove_inverse_of_1_is_0:
 \forall H7:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (inverse multiplicative_identity) additive_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO034-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO034-1.p.ma
index e1f26e13d..adab6c4ae 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO034-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO034-1.p.ma
@@ -68,7 +68,7 @@ theorem prove_single_axiom:
 \forall H4:\forall V:Univ.\forall W:Univ.\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (multiply (multiply V W X) Y (multiply V W Z)) (multiply V W (multiply X Y Z)).eq Univ (multiply (multiply a (inverse a) b) (inverse (multiply (multiply c d e) f (multiply c d g))) (multiply d (multiply g f e) c)) b
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO069-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO069-1.p.ma
index f76194c67..38bbe0e44 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO069-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO069-1.p.ma
@@ -31,7 +31,7 @@ theorem prove_tba_axioms_3:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.\forall D:Univ.\forall E:Univ.\forall F:Univ.\forall G:Univ.eq Univ (multiply (multiply A (inverse A) B) (inverse (multiply (multiply C D E) F (multiply C D G))) (multiply D (multiply G F E) C)) B.eq Univ (multiply a b (inverse b)) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO071-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO071-1.p.ma
index 806df9654..1cddbb9ae 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO071-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO071-1.p.ma
@@ -31,7 +31,7 @@ theorem prove_tba_axioms_5:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.\forall D:Univ.\forall E:Univ.\forall F:Univ.\forall G:Univ.eq Univ (multiply (multiply A (inverse A) B) (inverse (multiply (multiply C D E) F (multiply C D G))) (multiply D (multiply G F E) C)) B.eq Univ (multiply (inverse b) b a) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/BOO075-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/BOO075-1.p.ma
index 7f6d96d3c..971fa231a 100644
--- a/helm/software/matita/tests/TPTP/Veloci/BOO075-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/BOO075-1.p.ma
@@ -30,7 +30,7 @@ theorem prove_meredith_2_basis_1:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (nand (nand A (nand (nand B A) A)) (nand B (nand C A))) B.eq Univ (nand (nand a a) (nand b a)) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL004-3.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL004-3.p.ma
index d88025c42..f9a7712ee 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL004-3.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL004-3.p.ma
@@ -36,7 +36,7 @@ theorem prove_u_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply s X) Y) Z) (apply (apply X Z) (apply Y Z)).eq Univ (apply (apply (apply (apply s (apply k (apply s (apply (apply s k) k)))) (apply (apply s (apply (apply s k) k)) (apply (apply s k) k))) x) y) (apply y (apply (apply x x) y))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL007-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL007-1.p.ma
index 7018646d3..655b2a2ce 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL007-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL007-1.p.ma
@@ -35,7 +35,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL008-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL008-1.p.ma
index deee838a4..a3ff086db 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL008-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL008-1.p.ma
@@ -39,7 +39,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL010-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL010-1.p.ma
index 61e95267a..45bd7de31 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL010-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL010-1.p.ma
@@ -38,7 +38,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL012-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL012-1.p.ma
index 5aba07935..866be5178 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL012-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL012-1.p.ma
@@ -35,7 +35,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL013-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL013-1.p.ma
index ee3f5f7ba..07d594e3c 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL013-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL013-1.p.ma
@@ -38,7 +38,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL014-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL014-1.p.ma
index ef4e82edd..6e618736a 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL014-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL014-1.p.ma
@@ -38,7 +38,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL015-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL015-1.p.ma
index 2f4b47272..fcff6921c 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL015-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL015-1.p.ma
@@ -37,7 +37,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL016-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL016-1.p.ma
index b655e805a..37a3765cb 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL016-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL016-1.p.ma
@@ -40,7 +40,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL017-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL017-1.p.ma
index eb063cf1e..36d03e6e5 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL017-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL017-1.p.ma
@@ -40,7 +40,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL018-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL018-1.p.ma
index 87b023fdf..e218bae4a 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL018-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL018-1.p.ma
@@ -40,7 +40,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL021-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL021-1.p.ma
index 612537946..e8f9c3579 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL021-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL021-1.p.ma
@@ -40,7 +40,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL022-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL022-1.p.ma
index 866d0abd7..a311f146f 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL022-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL022-1.p.ma
@@ -40,7 +40,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL024-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL024-1.p.ma
index 5476a13a1..c38e40574 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL024-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL024-1.p.ma
@@ -40,7 +40,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL025-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL025-1.p.ma
index d5c98aabf..a7fa25856 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL025-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL025-1.p.ma
@@ -39,7 +39,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL045-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL045-1.p.ma
index 6ea3f3676..df48469b0 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL045-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL045-1.p.ma
@@ -40,7 +40,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL048-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL048-1.p.ma
index bee9580b0..a0435b2c2 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL048-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL048-1.p.ma
@@ -40,7 +40,7 @@ theorem prove_fixed_point:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL050-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL050-1.p.ma
index 716626e84..10f25dc2a 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL050-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL050-1.p.ma
@@ -47,7 +47,7 @@ theorem prove_all_fond_of_another:
 intros.
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL058-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL058-2.p.ma
index b0e94a980..5b216a3d2 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL058-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL058-2.p.ma
@@ -35,7 +35,7 @@ theorem prove_the_bird_exists:
 \forall H0:\forall X1:Univ.\forall X2:Univ.eq Univ (response (response lark X1) X2) (response X1 (response X2 X2)).eq Univ (response (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark))) (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)))) (response (response lark (response (response lark (response lark lark)) (response lark (response lark lark)))) (response lark (response lark lark)))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL058-3.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL058-3.p.ma
index 32802b0c5..2235cb57d 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL058-3.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL058-3.p.ma
@@ -35,7 +35,7 @@ theorem prove_the_bird_exists:
 \forall H0:\forall X1:Univ.\forall X2:Univ.eq Univ (response (response lark X1) X2) (response X1 (response X2 X2)).eq Univ (response (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)))) (response (response (response lark lark) (response lark (response lark lark))) (response lark (response lark lark)))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL060-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL060-2.p.ma
index 8ed2fdd81..da151819a 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL060-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL060-2.p.ma
@@ -39,7 +39,7 @@ theorem prove_q_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t b)) (apply (apply b b) t)) x) y) z) (apply y (apply x z))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL060-3.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL060-3.p.ma
index e33abe6e7..d1ff7bc9b 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL060-3.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL060-3.p.ma
@@ -39,7 +39,7 @@ theorem prove_q_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t b)) b)) t) x) y) z) (apply y (apply x z))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL061-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL061-2.p.ma
index 14e0f74a0..81adc265d 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL061-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL061-2.p.ma
@@ -39,7 +39,7 @@ theorem prove_q1_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t t)) (apply (apply b b) b)) x) y) z) (apply x (apply z y))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL061-3.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL061-3.p.ma
index ca9a9653d..0359b3ce9 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL061-3.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL061-3.p.ma
@@ -39,7 +39,7 @@ theorem prove_q1_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t t)) b)) b) x) y) z) (apply x (apply z y))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL062-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL062-2.p.ma
index 839f6ae93..383a285e8 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL062-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL062-2.p.ma
@@ -39,7 +39,7 @@ theorem prove_c_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t (apply (apply b b) t))) (apply (apply b b) t)) x) y) z) (apply (apply x z) y)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL062-3.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL062-3.p.ma
index 5b8ad716e..8b65e0c4f 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL062-3.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL062-3.p.ma
@@ -39,7 +39,7 @@ theorem prove_c_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t (apply (apply b b) t))) b)) t) x) y) z) (apply (apply x z) y)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL063-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL063-2.p.ma
index 31a6ae8ec..02f91ef49 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL063-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL063-2.p.ma
@@ -39,7 +39,7 @@ theorem prove_f_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t t)) (apply (apply b b) (apply (apply b b) t))) x) y) z) (apply (apply z y) x)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL063-3.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL063-3.p.ma
index 1c5133b0e..70205ee89 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL063-3.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL063-3.p.ma
@@ -39,7 +39,7 @@ theorem prove_f_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t t)) b)) (apply (apply b b) t)) x) y) z) (apply (apply z y) x)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL063-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL063-4.p.ma
index b341b737b..38bb35318 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL063-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL063-4.p.ma
@@ -39,7 +39,7 @@ theorem prove_f_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t t)) (apply (apply b (apply (apply b b) b)) t)) x) y) z) (apply (apply z y) x)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL063-5.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL063-5.p.ma
index 22976148e..4c98273b5 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL063-5.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL063-5.p.ma
@@ -39,7 +39,7 @@ theorem prove_f_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t t)) (apply (apply b b) b))) t) x) y) z) (apply (apply z y) x)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL063-6.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL063-6.p.ma
index b7c423748..19fbd39fa 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL063-6.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL063-6.p.ma
@@ -39,7 +39,7 @@ theorem prove_f_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply (apply b (apply t t)) b)) b)) t) x) y) z) (apply (apply z y) x)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL064-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL064-2.p.ma
index 5b45bc7ea..4e6d8af15 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL064-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL064-2.p.ma
@@ -39,7 +39,7 @@ theorem prove_v_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t (apply (apply b b) t))) (apply (apply b b) (apply (apply b b) t))) x) y) z) (apply (apply z x) y)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL064-3.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL064-3.p.ma
index 88b85eb9b..5644d38c1 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL064-3.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL064-3.p.ma
@@ -39,7 +39,7 @@ theorem prove_v_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t (apply (apply b b) t))) b)) (apply (apply b b) t)) x) y) z) (apply (apply z x) y)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL064-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL064-4.p.ma
index c1690d065..34fbe9349 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL064-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL064-4.p.ma
@@ -39,7 +39,7 @@ theorem prove_v_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t (apply (apply b b) t))) (apply (apply b (apply (apply b b) b)) t)) x) y) z) (apply (apply z x) y)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL064-5.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL064-5.p.ma
index 989b3c1bf..414887588 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL064-5.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL064-5.p.ma
@@ -39,7 +39,7 @@ theorem prove_v_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t (apply (apply b b) t))) (apply (apply b b) b))) t) x) y) z) (apply (apply z x) y)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL064-6.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL064-6.p.ma
index cb5635f98..4d054e035 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL064-6.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL064-6.p.ma
@@ -39,7 +39,7 @@ theorem prove_v_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply (apply b (apply t (apply (apply b b) t))) b)) b)) t) x) y) z) (apply (apply z x) y)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL064-7.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL064-7.p.ma
index d7a0a9cab..1c3ddc2f2 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL064-7.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL064-7.p.ma
@@ -39,7 +39,7 @@ theorem prove_v_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t (apply (apply b b) t))) (apply (apply b b) (apply (apply b t) t))) x) y) z) (apply (apply z x) y)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL064-8.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL064-8.p.ma
index 89111c679..120a6d047 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL064-8.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL064-8.p.ma
@@ -39,7 +39,7 @@ theorem prove_v_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply (apply b (apply t (apply (apply b b) t))) b)) (apply (apply b t) t)) x) y) z) (apply (apply z x) y)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL064-9.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL064-9.p.ma
index 8e6ad6cdb..07591bb4c 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL064-9.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL064-9.p.ma
@@ -39,7 +39,7 @@ theorem prove_v_combinator:
 \forall H1:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (apply (apply (apply b X) Y) Z) (apply X (apply Y Z)).eq Univ (apply (apply (apply (apply (apply b (apply t (apply (apply b b) t))) (apply (apply b (apply (apply b b) t)) t)) x) y) z) (apply (apply z x) y)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL083-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL083-1.p.ma
index 870b7d862..89d991761 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL083-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL083-1.p.ma
@@ -35,7 +35,7 @@ exists[
 2:
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL084-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL084-1.p.ma
index f345021bf..4d2d057bc 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL084-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL084-1.p.ma
@@ -35,7 +35,7 @@ exists[
 2:
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL085-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL085-1.p.ma
index ff1981363..7fd4279ce 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL085-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL085-1.p.ma
@@ -33,7 +33,7 @@ exists[
 2:
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/COL086-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/COL086-1.p.ma
index 030c2cd33..e4527c48b 100644
--- a/helm/software/matita/tests/TPTP/Veloci/COL086-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/COL086-1.p.ma
@@ -33,7 +33,7 @@ exists[
 2:
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP001-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP001-2.p.ma
index c695b7f80..d4e79c748 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP001-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP001-2.p.ma
@@ -79,7 +79,7 @@ theorem prove_b_times_a_is_c:
 \forall H6:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (multiply b a) c
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP001-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP001-4.p.ma
index ea943fdd8..544eaf116 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP001-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP001-4.p.ma
@@ -40,7 +40,7 @@ theorem prove_b_times_a_is_c:
 \forall H3:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).eq Univ (multiply b a) c
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP010-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP010-4.p.ma
index ce5111529..b6a3f51c1 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP010-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP010-4.p.ma
@@ -38,7 +38,7 @@ theorem prove_b_times_c_is_e:
 \forall H3:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).eq Univ (multiply b c) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP011-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP011-4.p.ma
index d11f4a5f4..6391656ba 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP011-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP011-4.p.ma
@@ -39,7 +39,7 @@ theorem prove_left_cancellation:
 \forall H3:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (multiply (multiply X Y) Z) (multiply X (multiply Y Z)).eq Univ b d
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP012-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP012-4.p.ma
index 4d7966963..ed5338825 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP012-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP012-4.p.ma
@@ -71,7 +71,7 @@ theorem prove_inverse_of_product_is_product_of_inverses:
 \forall H4:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (inverse (multiply a b)) (multiply (inverse b) (inverse a))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP022-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP022-2.p.ma
index 034f854c3..db2519fe6 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP022-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP022-2.p.ma
@@ -71,7 +71,7 @@ theorem prove_inverse_of_inverse_is_original:
 \forall H4:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (inverse (inverse a)) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP023-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP023-2.p.ma
index f5cb37252..4ad352201 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP023-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP023-2.p.ma
@@ -68,7 +68,7 @@ theorem prove_inverse_of_id_is_id:
 \forall H4:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (inverse identity) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP115-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP115-1.p.ma
index dafda9a6e..6c605ee94 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP115-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP115-1.p.ma
@@ -29,7 +29,7 @@ theorem prove_order3:
 \forall H0:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (multiply X (multiply (multiply X (multiply (multiply X Y) Z)) (multiply identity (multiply Z Z)))) Y.eq Univ (multiply a (multiply a a)) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP116-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP116-1.p.ma
index d7895138b..3cc4b5719 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP116-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP116-1.p.ma
@@ -29,7 +29,7 @@ theorem prove_order3:
 \forall H0:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (multiply X (multiply (multiply X (multiply (multiply X Y) Z)) (multiply identity (multiply Z Z)))) Y.eq Univ (multiply identity a) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP117-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP117-1.p.ma
index 2d04443b6..8768d0eab 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP117-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP117-1.p.ma
@@ -29,7 +29,7 @@ theorem prove_order3:
 \forall H0:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (multiply X (multiply (multiply X (multiply (multiply X Y) Z)) (multiply identity (multiply Z Z)))) Y.eq Univ (multiply a identity) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP118-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP118-1.p.ma
index d348a57db..4d01353ea 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP118-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP118-1.p.ma
@@ -31,7 +31,7 @@ theorem prove_order3:
 \forall H0:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (multiply X (multiply (multiply X (multiply (multiply X Y) Z)) (multiply identity (multiply Z Z)))) Y.eq Univ (multiply (multiply a b) c) (multiply a (multiply b c))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP136-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP136-1.p.ma
index b3380a855..e108ae55b 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP136-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP136-1.p.ma
@@ -112,7 +112,7 @@ theorem prove_ax_antisyma:
 \forall H16:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ a b
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP137-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP137-1.p.ma
index 34885590c..322702cc5 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP137-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP137-1.p.ma
@@ -112,7 +112,7 @@ theorem prove_ax_antisymb:
 \forall H16:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ a b
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP139-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP139-1.p.ma
index 1e3644eae..cf868c306 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP139-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP139-1.p.ma
@@ -115,7 +115,7 @@ theorem prove_ax_glb1b:
 \forall H16:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (greatest_lower_bound a b) c) c
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP141-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP141-1.p.ma
index 6b7b50871..3706a25d7 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP141-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP141-1.p.ma
@@ -115,7 +115,7 @@ theorem prove_ax_glb1d:
 \forall H16:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (greatest_lower_bound a b) c) c
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP142-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP142-1.p.ma
index ac52f8966..1f13705e1 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP142-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP142-1.p.ma
@@ -110,7 +110,7 @@ theorem prove_ax_glb2a:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (greatest_lower_bound a b) a) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP143-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP143-1.p.ma
index cefbb9734..be00186ae 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP143-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP143-1.p.ma
@@ -110,7 +110,7 @@ theorem prove_ax_glb2b:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (greatest_lower_bound a b) a) (greatest_lower_bound a b)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP144-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP144-1.p.ma
index 920463e12..be20f1901 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP144-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP144-1.p.ma
@@ -110,7 +110,7 @@ theorem prove_ax_glb3a:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (greatest_lower_bound a b) b) b
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP145-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP145-1.p.ma
index 63b6c5087..032cdfd55 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP145-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP145-1.p.ma
@@ -110,7 +110,7 @@ theorem prove_ax_glb3b:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (greatest_lower_bound a b) b) (greatest_lower_bound a b)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP146-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP146-1.p.ma
index 2c39e935d..6bacee188 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP146-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP146-1.p.ma
@@ -115,7 +115,7 @@ theorem prove_ax_lub1a:
 \forall H16:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (least_upper_bound a b) c) c
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP149-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP149-1.p.ma
index 9030600cb..e6c7d4ff6 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP149-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP149-1.p.ma
@@ -115,7 +115,7 @@ theorem prove_ax_lub1d:
 \forall H16:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (least_upper_bound a b) c) c
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP150-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP150-1.p.ma
index ceae01410..f612ede8e 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP150-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP150-1.p.ma
@@ -110,7 +110,7 @@ theorem prove_ax_lub2a:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound a (least_upper_bound a b)) (least_upper_bound a b)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP151-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP151-1.p.ma
index 454c61546..240c266b2 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP151-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP151-1.p.ma
@@ -110,7 +110,7 @@ theorem prove_ax_lub2b:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound a (least_upper_bound a b)) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP152-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP152-1.p.ma
index 941fc726c..d9078e5fb 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP152-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP152-1.p.ma
@@ -110,7 +110,7 @@ theorem prove_ax_lub3a:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound b (least_upper_bound a b)) (least_upper_bound a b)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP153-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP153-1.p.ma
index c677c140c..7dc86aa7e 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP153-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP153-1.p.ma
@@ -110,7 +110,7 @@ theorem prove_ax_lub3b:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound b (least_upper_bound a b)) b
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP154-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP154-1.p.ma
index 04245f9de..51832886c 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP154-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP154-1.p.ma
@@ -114,7 +114,7 @@ theorem prove_ax_mono1a:
 \forall H15:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (multiply a c) (multiply b c)) (multiply b c)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP155-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP155-1.p.ma
index b7149e55f..7a940e531 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP155-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP155-1.p.ma
@@ -112,7 +112,7 @@ theorem prove_ax_mono1b:
 \forall H15:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (multiply a c) (multiply b c)) (multiply a c)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP156-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP156-1.p.ma
index db0a9b38f..544290f56 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP156-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP156-1.p.ma
@@ -114,7 +114,7 @@ theorem prove_ax_mono1c:
 \forall H15:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (multiply a c) (multiply b c)) (multiply a c)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP157-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP157-1.p.ma
index 10948cac5..63868e1bf 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP157-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP157-1.p.ma
@@ -112,7 +112,7 @@ theorem prove_ax_mono2a:
 \forall H15:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (multiply c a) (multiply c b)) (multiply c b)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP158-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP158-1.p.ma
index 269be4042..710c30a1b 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP158-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP158-1.p.ma
@@ -112,7 +112,7 @@ theorem prove_ax_mono2b:
 \forall H15:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (multiply c a) (multiply c b)) (multiply c a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP159-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP159-1.p.ma
index 1a9471a66..ca0b0ffdf 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP159-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP159-1.p.ma
@@ -112,7 +112,7 @@ theorem prove_ax_mono2c:
 \forall H15:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (multiply c a) (multiply c b)) (multiply c b)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP160-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP160-1.p.ma
index 0aa320f7d..1d49bcea1 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP160-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP160-1.p.ma
@@ -109,7 +109,7 @@ theorem prove_ax_refla:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound a a) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP161-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP161-1.p.ma
index 473d47bc4..ff4878fbc 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP161-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP161-1.p.ma
@@ -109,7 +109,7 @@ theorem prove_ax_reflb:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound a a) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP162-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP162-1.p.ma
index c1af39429..4d4fa4e5e 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP162-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP162-1.p.ma
@@ -113,7 +113,7 @@ theorem prove_ax_transa:
 \forall H16:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound a c) c
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP163-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP163-1.p.ma
index 964662f6c..3065332b9 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP163-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP163-1.p.ma
@@ -113,7 +113,7 @@ theorem prove_ax_transb:
 \forall H16:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound a c) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP168-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP168-1.p.ma
index 162fcd775..905257851 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP168-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP168-1.p.ma
@@ -116,7 +116,7 @@ theorem prove_p01a:
 \forall H15:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (multiply (inverse c) (multiply a c)) (multiply (inverse c) (multiply b c))) (multiply (inverse c) (multiply b c))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP168-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP168-2.p.ma
index ff7f06967..8e6697270 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP168-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP168-2.p.ma
@@ -114,7 +114,7 @@ theorem prove_p01b:
 \forall H15:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound (multiply (inverse c) (multiply a c)) (multiply (inverse c) (multiply b c))) (multiply (inverse c) (multiply a c))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP173-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP173-1.p.ma
index 34791231e..d6b61595c 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP173-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP173-1.p.ma
@@ -115,7 +115,7 @@ theorem prove_p05a:
 \forall H16:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ identity a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP174-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP174-1.p.ma
index 77177b3f5..bd8fecc10 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP174-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP174-1.p.ma
@@ -112,7 +112,7 @@ theorem prove_p05b:
 \forall H16:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ identity a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP176-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP176-1.p.ma
index 485cd7c0e..fe03f9f02 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP176-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP176-1.p.ma
@@ -118,7 +118,7 @@ theorem prove_p07:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (multiply c (multiply (least_upper_bound a b) d)) (least_upper_bound (multiply c (multiply a d)) (multiply c (multiply b d)))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP176-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP176-2.p.ma
index e5dbe4ab7..153ac5806 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP176-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP176-2.p.ma
@@ -114,7 +114,7 @@ theorem prove_p07:
 \forall H15:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (multiply c (multiply (least_upper_bound a b) d)) (least_upper_bound (multiply c (multiply a d)) (multiply c (multiply b d)))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP182-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP182-1.p.ma
index 25f4ec89d..b2166c28f 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP182-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP182-1.p.ma
@@ -120,7 +120,7 @@ theorem prove_p17a:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound identity (greatest_lower_bound a identity)) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP182-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP182-2.p.ma
index 99d2f2272..f8955ab0e 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP182-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP182-2.p.ma
@@ -121,7 +121,7 @@ theorem prove_p17a:
 \forall H17:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound identity (greatest_lower_bound a identity)) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP182-3.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP182-3.p.ma
index ad3388fcf..fa4e6ce23 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP182-3.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP182-3.p.ma
@@ -113,7 +113,7 @@ theorem prove_p17b:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound identity (least_upper_bound a identity)) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP182-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP182-4.p.ma
index c5f686a70..95fb312fb 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP182-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP182-4.p.ma
@@ -114,7 +114,7 @@ theorem prove_p17b:
 \forall H17:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound identity (least_upper_bound a identity)) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP186-3.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP186-3.p.ma
index d5ba153b9..a39543178 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP186-3.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP186-3.p.ma
@@ -112,7 +112,7 @@ theorem prove_p23x:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (multiply a b) identity) (multiply a (least_upper_bound (inverse a) b))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP186-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP186-4.p.ma
index eb035cbbb..be8354b19 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP186-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP186-4.p.ma
@@ -113,7 +113,7 @@ theorem prove_p23x:
 \forall H17:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound (multiply a b) identity) (multiply a (least_upper_bound (inverse a) b))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP188-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP188-1.p.ma
index 2ad492bcf..da64fdee3 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP188-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP188-1.p.ma
@@ -111,7 +111,7 @@ theorem prove_p38a:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound b (least_upper_bound a b)) (least_upper_bound a b)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP188-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP188-2.p.ma
index 9008f3ef0..771056e01 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP188-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP188-2.p.ma
@@ -112,7 +112,7 @@ theorem prove_p38a:
 \forall H17:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (least_upper_bound b (least_upper_bound a b)) (least_upper_bound a b)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP189-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP189-1.p.ma
index d2fff5b3d..183e7b772 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP189-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP189-1.p.ma
@@ -111,7 +111,7 @@ theorem prove_p38b:
 \forall H14:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound b (least_upper_bound a b)) b
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP189-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP189-2.p.ma
index eedb47810..0b47a1614 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP189-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP189-2.p.ma
@@ -112,7 +112,7 @@ theorem prove_p38b:
 \forall H17:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (greatest_lower_bound b (least_upper_bound a b)) b
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP192-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP192-1.p.ma
index 8463afd62..01ca783b0 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP192-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP192-1.p.ma
@@ -111,7 +111,7 @@ theorem prove_p40a:
 \forall H15:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP206-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP206-1.p.ma
index bec8aa7f7..9c5b5bcce 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP206-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP206-1.p.ma
@@ -46,7 +46,7 @@ theorem prove_moufang1:
 \forall H8:\forall X:Univ.eq Univ (multiply identity X) X.eq Univ (multiply (multiply a (multiply b c)) a) (multiply (multiply a b) (multiply c a))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP454-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP454-1.p.ma
index a3f949d3e..257fdd49a 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP454-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP454-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity (divide A (divide B (divide (divide (divide A A) A) C)))) C) B.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP455-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP455-1.p.ma
index c70c4f672..deaa9a2f0 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP455-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP455-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity (divide A (divide B (divide (divide (divide A A) A) C)))) C) B.eq Univ (multiply identity a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP456-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP456-1.p.ma
index c5b9d8c5d..228a4f3a6 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP456-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP456-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_3:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity (divide A (divide B (divide (divide (divide A A) A) C)))) C) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP457-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP457-1.p.ma
index 3358805bc..acd2050d2 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP457-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP457-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide (divide A A) (divide A (divide B (divide (divide identity A) C)))) C) B.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP458-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP458-1.p.ma
index e297b3b08..44091f50e 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP458-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP458-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide (divide A A) (divide A (divide B (divide (divide identity A) C)))) C) B.eq Univ (multiply identity a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP459-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP459-1.p.ma
index c3302ae0c..303f73741 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP459-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP459-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_3:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide (divide A A) (divide A (divide B (divide (divide identity A) C)))) C) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP460-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP460-1.p.ma
index 7dcd0f698..698ac8a23 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP460-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP460-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide A (divide (divide (divide identity B) C) (divide (divide (divide A A) A) C))) B.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP463-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP463-1.p.ma
index be1180422..fcd04c0c5 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP463-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP463-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide A (divide (divide (divide (divide A A) B) C) (divide (divide identity A) C))) B.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP467-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP467-1.p.ma
index f7723d3c0..1107f4b98 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP467-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP467-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_2:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.\forall D:Univ.eq Univ (divide (divide A A) (divide B (divide (divide C (divide D B)) (inverse D)))) C.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP481-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP481-1.p.ma
index e5f0a50ed..bf063d591 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP481-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP481-1.p.ma
@@ -35,7 +35,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.\forall D:Univ.eq Univ (double_divide (double_divide (double_divide A (double_divide B identity)) (double_divide (double_divide C (double_divide D (double_divide D identity))) (double_divide A identity))) B) C.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP484-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP484-1.p.ma
index 746cf9541..e8588f917 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP484-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP484-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide (double_divide A B) C) (double_divide B identity))) (double_divide identity identity)) C.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP485-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP485-1.p.ma
index 63fe7d2a1..2a015e13e 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP485-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP485-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide (double_divide A B) C) (double_divide B identity))) (double_divide identity identity)) C.eq Univ (multiply identity a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP486-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP486-1.p.ma
index b8ecfd815..ccdaf0ea9 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP486-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP486-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_3:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide (double_divide A B) C) (double_divide B identity))) (double_divide identity identity)) C.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP487-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP487-1.p.ma
index b679645fe..a26acef17 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP487-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP487-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide A (double_divide (double_divide (double_divide identity (double_divide (double_divide A identity) (double_divide B C))) B) identity)) C.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP488-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP488-1.p.ma
index c6b63cbcf..ff1c3c177 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP488-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP488-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide A (double_divide (double_divide (double_divide identity (double_divide (double_divide A identity) (double_divide B C))) B) identity)) C.eq Univ (multiply identity a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP490-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP490-1.p.ma
index 326e72502..78e958798 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP490-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP490-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide identity A) (double_divide identity (double_divide (double_divide (double_divide A B) identity) (double_divide C B)))) C.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP491-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP491-1.p.ma
index 39482784f..221fdb592 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP491-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP491-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide identity A) (double_divide identity (double_divide (double_divide (double_divide A B) identity) (double_divide C B)))) C.eq Univ (multiply identity a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP492-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP492-1.p.ma
index 3af993fcf..e9f198d2d 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP492-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP492-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_3:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide identity A) (double_divide identity (double_divide (double_divide (double_divide A B) identity) (double_divide C B)))) C.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP493-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP493-1.p.ma
index 059f6e300..fc0bf16ce 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP493-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP493-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide identity A) (double_divide (double_divide (double_divide B C) (double_divide identity identity)) (double_divide A C))) B.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP494-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP494-1.p.ma
index 888ad8576..ea863067a 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP494-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP494-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide identity A) (double_divide (double_divide (double_divide B C) (double_divide identity identity)) (double_divide A C))) B.eq Univ (multiply identity a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP495-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP495-1.p.ma
index 8c6d03b3d..225028412 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP495-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP495-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_3:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide identity A) (double_divide (double_divide (double_divide B C) (double_divide identity identity)) (double_divide A C))) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP496-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP496-1.p.ma
index f96492e13..efe2d3a94 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP496-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP496-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide identity (double_divide A (double_divide B identity))) (double_divide (double_divide B (double_divide C A)) identity)) C.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP497-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP497-1.p.ma
index 79e82ae64..c2f5d7be9 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP497-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP497-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide identity (double_divide A (double_divide B identity))) (double_divide (double_divide B (double_divide C A)) identity)) C.eq Univ (multiply identity a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP498-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP498-1.p.ma
index d2cac96d0..c5875b0b2 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP498-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP498-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_3:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide identity (double_divide A (double_divide B identity))) (double_divide (double_divide B (double_divide C A)) identity)) C.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP509-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP509-1.p.ma
index dfbaf1362..25618b46a 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP509-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP509-1.p.ma
@@ -31,7 +31,7 @@ theorem prove_these_axioms_1:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (multiply (multiply (multiply A B) C) (inverse (multiply A C))) B.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP510-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP510-1.p.ma
index 7806668c0..1003a4014 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP510-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP510-1.p.ma
@@ -31,7 +31,7 @@ theorem prove_these_axioms_2:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (multiply (multiply (multiply A B) C) (inverse (multiply A C))) B.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP511-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP511-1.p.ma
index 34d3bab74..ff8c9f4c0 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP511-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP511-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_3:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (multiply (multiply (multiply A B) C) (inverse (multiply A C))) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP512-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP512-1.p.ma
index 790814570..19a8c4a94 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP512-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP512-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_4:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (multiply (multiply (multiply A B) C) (inverse (multiply A C))) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP513-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP513-1.p.ma
index 022817297..03409c949 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP513-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP513-1.p.ma
@@ -30,7 +30,7 @@ theorem prove_these_axioms_1:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (multiply A (multiply (multiply B C) (inverse (multiply A C)))) B.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP514-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP514-1.p.ma
index 44411f118..90593b6c8 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP514-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP514-1.p.ma
@@ -30,7 +30,7 @@ theorem prove_these_axioms_2:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (multiply A (multiply (multiply B C) (inverse (multiply A C)))) B.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP515-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP515-1.p.ma
index 2ad540b74..7b526ef97 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP515-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP515-1.p.ma
@@ -31,7 +31,7 @@ theorem prove_these_axioms_3:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (multiply A (multiply (multiply B C) (inverse (multiply A C)))) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP516-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP516-1.p.ma
index 59a8da6ac..af15eb7ee 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP516-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP516-1.p.ma
@@ -31,7 +31,7 @@ theorem prove_these_axioms_4:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (multiply A (multiply (multiply B C) (inverse (multiply A C)))) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP517-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP517-1.p.ma
index e268d2534..a488717cd 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP517-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP517-1.p.ma
@@ -30,7 +30,7 @@ theorem prove_these_axioms_1:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (multiply A (multiply (multiply (inverse (multiply A B)) C) B)) C.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP518-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP518-1.p.ma
index 89a742ca1..a953ab610 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP518-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP518-1.p.ma
@@ -30,7 +30,7 @@ theorem prove_these_axioms_2:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (multiply A (multiply (multiply (inverse (multiply A B)) C) B)) C.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP520-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP520-1.p.ma
index 879b8f0a9..ea992df71 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP520-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP520-1.p.ma
@@ -31,7 +31,7 @@ theorem prove_these_axioms_4:
 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (multiply A (multiply (multiply (inverse (multiply A B)) C) B)) C.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP541-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP541-1.p.ma
index 446167f51..a8f428a0d 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP541-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP541-1.p.ma
@@ -35,7 +35,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity (divide (divide (divide A B) C) A)) C) B.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP542-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP542-1.p.ma
index 6e084eef4..848748d87 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP542-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP542-1.p.ma
@@ -35,7 +35,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity (divide (divide (divide A B) C) A)) C) B.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP543-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP543-1.p.ma
index 2e80e0158..cfc5bab58 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP543-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP543-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_3:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity (divide (divide (divide A B) C) A)) C) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP544-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP544-1.p.ma
index 3a5257ed0..96fb69f73 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP544-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP544-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_4:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity (divide (divide (divide A B) C) A)) C) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP545-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP545-1.p.ma
index e4caec04b..302fb8916 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP545-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP545-1.p.ma
@@ -35,7 +35,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity (divide A B)) (divide (divide B C) A)) C.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP546-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP546-1.p.ma
index ba46f7f71..2488a9484 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP546-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP546-1.p.ma
@@ -35,7 +35,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity (divide A B)) (divide (divide B C) A)) C.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP547-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP547-1.p.ma
index 981df2d12..24ede0fe7 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP547-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP547-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_3:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity (divide A B)) (divide (divide B C) A)) C.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP548-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP548-1.p.ma
index 8750ac7e8..a065d3f1b 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP548-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP548-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_4:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity (divide A B)) (divide (divide B C) A)) C.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP549-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP549-1.p.ma
index 9e5165b72..0bf4dbf1c 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP549-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP549-1.p.ma
@@ -35,7 +35,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity A) (divide (divide (divide B A) C) B)) C.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP550-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP550-1.p.ma
index ceb1fcb92..a7482f9b5 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP550-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP550-1.p.ma
@@ -35,7 +35,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity A) (divide (divide (divide B A) C) B)) C.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP551-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP551-1.p.ma
index 69b83f64d..3144369c2 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP551-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP551-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_3:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity A) (divide (divide (divide B A) C) B)) C.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP552-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP552-1.p.ma
index 72d8dbb1a..9a776c962 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP552-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP552-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_4:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide identity A) (divide (divide (divide B A) C) B)) C.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP556-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP556-1.p.ma
index 7ff2cf4fc..f314261a2 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP556-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP556-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_4:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide A (inverse (divide B (divide A C)))) C) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP558-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP558-1.p.ma
index d3ffe8859..35670d9cb 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP558-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP558-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_2:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide A (inverse (divide (divide B C) (divide A C)))) B.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP560-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP560-1.p.ma
index f145a3af9..113f49edf 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP560-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP560-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_4:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide A (inverse (divide (divide B C) (divide A C)))) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP561-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP561-1.p.ma
index d6d1ef6ed..dc788b109 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP561-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP561-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_1:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide (divide A (inverse B)) C) (divide A C)) B.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP562-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP562-1.p.ma
index 118adfa7a..99ea92789 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP562-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP562-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_2:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide (divide A (inverse B)) C) (divide A C)) B.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP564-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP564-1.p.ma
index c46fb73d6..63b1c2d97 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP564-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP564-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_4:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (divide (divide (divide A (inverse B)) C) (divide A C)) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP565-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP565-1.p.ma
index e9151448c..ad4f93570 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP565-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP565-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide A C)) (double_divide identity C))) (double_divide identity identity)) B.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP566-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP566-1.p.ma
index 23b805f00..71a827e47 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP566-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP566-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide A C)) (double_divide identity C))) (double_divide identity identity)) B.eq Univ (multiply identity a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP567-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP567-1.p.ma
index e77e2b762..6fbd3492b 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP567-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP567-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_3:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide A C)) (double_divide identity C))) (double_divide identity identity)) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP568-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP568-1.p.ma
index 07adcfd9b..884ed5e5c 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP568-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP568-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_4:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide A C)) (double_divide identity C))) (double_divide identity identity)) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP569-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP569-1.p.ma
index 260522c05..931c933ba 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP569-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP569-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide A C)) (double_divide C identity))) (double_divide identity identity)) B.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP570-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP570-1.p.ma
index d74cd154f..d6bdbbfc6 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP570-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP570-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide A C)) (double_divide C identity))) (double_divide identity identity)) B.eq Univ (multiply identity a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP572-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP572-1.p.ma
index 270768037..c3e517cef 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP572-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP572-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_4:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide A C)) (double_divide C identity))) (double_divide identity identity)) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP573-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP573-1.p.ma
index 1ae737d5b..8076345cc 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP573-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP573-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide C A)) (double_divide C identity))) (double_divide identity identity)) B.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP574-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP574-1.p.ma
index a3d3395f5..e6f9dfcec 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP574-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP574-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide C A)) (double_divide C identity))) (double_divide identity identity)) B.eq Univ (multiply identity a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP576-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP576-1.p.ma
index d192c0455..aed52d2de 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP576-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP576-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_4:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide B (double_divide C A)) (double_divide C identity))) (double_divide identity identity)) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP577-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP577-1.p.ma
index e0836fded..ad7c58b9e 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP577-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP577-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide (double_divide B A) C) (double_divide B identity))) (double_divide identity identity)) C.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP578-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP578-1.p.ma
index ef7d1793f..7c9843da7 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP578-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP578-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide (double_divide B A) C) (double_divide B identity))) (double_divide identity identity)) C.eq Univ (multiply identity a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP580-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP580-1.p.ma
index aee50acd9..4d729b995 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP580-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP580-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_4:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide (double_divide B A) C) (double_divide B identity))) (double_divide identity identity)) C.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP581-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP581-1.p.ma
index 76b98c5a2..d826e2af1 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP581-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP581-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_1:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide identity B) (double_divide C (double_divide B A)))) (double_divide identity identity)) C.eq Univ (multiply (inverse a1) a1) identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP582-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP582-1.p.ma
index 2c1a81a7d..4c09bb39c 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP582-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP582-1.p.ma
@@ -34,7 +34,7 @@ theorem prove_these_axioms_2:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide identity B) (double_divide C (double_divide B A)))) (double_divide identity identity)) C.eq Univ (multiply identity a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP583-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP583-1.p.ma
index eb1c927ec..fa95c336a 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP583-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP583-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_3:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide identity B) (double_divide C (double_divide B A)))) (double_divide identity identity)) C.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP584-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP584-1.p.ma
index b66e93f43..db36e336b 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP584-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP584-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_these_axioms_4:
 \forall H3:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A (double_divide (double_divide identity B) (double_divide C (double_divide B A)))) (double_divide identity identity)) C.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP586-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP586-1.p.ma
index 9c4c69ed0..f38467e27 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP586-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP586-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_2:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide A (inverse (double_divide (inverse (double_divide (double_divide A B) (inverse C))) B))) C.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP588-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP588-1.p.ma
index 1c32572b0..1d13edfbe 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP588-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP588-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_4:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide A (inverse (double_divide (inverse (double_divide (double_divide A B) (inverse C))) B))) C.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP590-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP590-1.p.ma
index 3a8c3f132..f678b3d83 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP590-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP590-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_2:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (inverse (double_divide (double_divide A B) (inverse (double_divide A (inverse C))))) B) C.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP592-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP592-1.p.ma
index c2c748817..5612e2720 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP592-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP592-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_4:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (inverse (double_divide (double_divide A B) (inverse (double_divide A (inverse C))))) B) C.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP595-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP595-1.p.ma
index d17416172..e97f64cd3 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP595-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP595-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_3:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (inverse (double_divide (double_divide A B) (inverse (double_divide A (inverse (double_divide C B)))))) C.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP596-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP596-1.p.ma
index 45b171485..1d8e313ac 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP596-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP596-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_4:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (inverse (double_divide (double_divide A B) (inverse (double_divide A (inverse (double_divide C B)))))) C.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP597-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP597-1.p.ma
index 3076cda7d..5923b8e70 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP597-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP597-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_1:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A B) (inverse (double_divide A (inverse (double_divide (inverse C) B))))) C.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP598-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP598-1.p.ma
index dfd966562..133ed30f6 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP598-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP598-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_2:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A B) (inverse (double_divide A (inverse (double_divide (inverse C) B))))) C.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP599-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP599-1.p.ma
index f703d7b6b..31716a710 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP599-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP599-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_3:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A B) (inverse (double_divide A (inverse (double_divide (inverse C) B))))) C.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP600-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP600-1.p.ma
index d8180ca64..07535f9bb 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP600-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP600-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_4:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (double_divide A B) (inverse (double_divide A (inverse (double_divide (inverse C) B))))) C.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP602-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP602-1.p.ma
index d2d0d3305..620ddb94e 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP602-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP602-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_2:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (inverse (double_divide (inverse (double_divide A (inverse (double_divide B (double_divide A C))))) C)) B.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP603-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP603-1.p.ma
index 6ee5d33c5..6d7b92f84 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP603-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP603-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_3:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (inverse (double_divide (inverse (double_divide A (inverse (double_divide B (double_divide A C))))) C)) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP604-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP604-1.p.ma
index 4e083dea9..9e228851d 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP604-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP604-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_4:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (inverse (double_divide (inverse (double_divide A (inverse (double_divide B (double_divide A C))))) C)) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP605-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP605-1.p.ma
index 0145a313e..89084a07b 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP605-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP605-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_1:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (inverse (double_divide A (inverse (double_divide (inverse B) (double_divide A C))))) C) B.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP606-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP606-1.p.ma
index 4f4e2bea1..09742e1ac 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP606-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP606-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_2:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (inverse (double_divide A (inverse (double_divide (inverse B) (double_divide A C))))) C) B.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP608-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP608-1.p.ma
index 811ae06bc..de5945331 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP608-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP608-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_4:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (inverse (double_divide A (inverse (double_divide (inverse B) (double_divide A C))))) C) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP612-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP612-1.p.ma
index 936eedbaa..3dec26708 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP612-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP612-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_4:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (inverse (double_divide (inverse (double_divide (inverse (double_divide A B)) C)) (double_divide A C))) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP613-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP613-1.p.ma
index 5f5960ed6..206e1edcb 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP613-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP613-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_1:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (inverse (double_divide (inverse (double_divide A (inverse B))) C)) (double_divide A C)) B.eq Univ (multiply (inverse a1) a1) (multiply (inverse b1) b1)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP614-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP614-1.p.ma
index 389785f55..203d3f216 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP614-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP614-1.p.ma
@@ -32,7 +32,7 @@ theorem prove_these_axioms_2:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (inverse (double_divide (inverse (double_divide A (inverse B))) C)) (double_divide A C)) B.eq Univ (multiply (multiply (inverse b2) b2) a2) a2
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP615-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP615-1.p.ma
index 2f656b223..2fe6234f6 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP615-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP615-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_3:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (inverse (double_divide (inverse (double_divide A (inverse B))) C)) (double_divide A C)) B.eq Univ (multiply (multiply a3 b3) c3) (multiply a3 (multiply b3 c3))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/GRP616-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/GRP616-1.p.ma
index 619a0f5bb..6649a53d8 100644
--- a/helm/software/matita/tests/TPTP/Veloci/GRP616-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP616-1.p.ma
@@ -33,7 +33,7 @@ theorem prove_these_axioms_4:
 \forall H1:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (double_divide (inverse (double_divide (inverse (double_divide A (inverse B))) C)) (double_divide A C)) B.eq Univ (multiply a b) (multiply b a)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LAT008-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LAT008-1.p.ma
index 789549d1c..a8ee942e6 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LAT008-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LAT008-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_absorbtion_dual:
 \forall H1:\forall X:Univ.\forall Y:Univ.eq Univ (meet X (join X Y)) X.eq Univ (join a (meet a b)) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LAT033-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LAT033-1.p.ma
index b5548d960..e1897a414 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LAT033-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LAT033-1.p.ma
@@ -39,7 +39,7 @@ theorem idempotence_of_join:
 \forall H5:\forall X:Univ.\forall Y:Univ.eq Univ (meet X (join X Y)) X.eq Univ (join xx xx) xx
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LAT034-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LAT034-1.p.ma
index 801451c43..37ce834ab 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LAT034-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LAT034-1.p.ma
@@ -39,7 +39,7 @@ theorem idempotence_of_meet:
 \forall H5:\forall X:Univ.\forall Y:Univ.eq Univ (meet X (join X Y)) X.eq Univ (meet xx xx) xx
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LAT039-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LAT039-1.p.ma
index 61d6cef04..8ad8654fc 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LAT039-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LAT039-1.p.ma
@@ -70,7 +70,7 @@ theorem rhs:
 \forall H10:\forall X:Univ.eq Univ (meet X X) X.eq Univ (join xx (meet yy zz)) (meet yy (join xx zz))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LAT039-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/LAT039-2.p.ma
index c7af583bd..de4e55ffa 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LAT039-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LAT039-2.p.ma
@@ -69,7 +69,7 @@ theorem rhs:
 \forall H10:\forall X:Univ.eq Univ (meet X X) X.eq Univ (join xx (meet yy zz)) (meet (join xx yy) (join xx zz))
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LAT040-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LAT040-1.p.ma
index 9982a8eab..a4ff6eff6 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LAT040-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LAT040-1.p.ma
@@ -70,7 +70,7 @@ theorem rhs:
 \forall H11:\forall X:Univ.eq Univ (meet X X) X.eq Univ yy zz
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LAT045-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LAT045-1.p.ma
index f998f72e9..0b58207db 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LAT045-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LAT045-1.p.ma
@@ -77,7 +77,7 @@ theorem prove_orthomodular_law:
 \forall H13:\forall X:Univ.eq Univ (meet X X) X.eq Univ (join a (meet (complement a) (join a b))) (join a b)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL110-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL110-2.p.ma
index 9515feec6..442ce5958 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL110-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL110-2.p.ma
@@ -64,7 +64,7 @@ theorem prove_mv_24:
 \forall H3:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (implies (not (not x)) x) truth
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL112-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL112-2.p.ma
index ef68697fe..473cf328c 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL112-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL112-2.p.ma
@@ -65,7 +65,7 @@ theorem prove_mv_29:
 \forall H3:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (implies x (not (not x))) truth
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL113-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL113-2.p.ma
index 534c7fb7e..c310916a7 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL113-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL113-2.p.ma
@@ -64,7 +64,7 @@ theorem prove_mv_33:
 \forall H3:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (implies (implies (not x) y) (implies (not y) x)) truth
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL114-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL114-2.p.ma
index 2fce65768..46cc01727 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL114-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL114-2.p.ma
@@ -65,7 +65,7 @@ theorem prove_mv_36:
 \forall H3:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (implies (implies x y) (implies (not y) (not x))) truth
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL115-2.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL115-2.p.ma
index 934852d6e..158fef7e8 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL115-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL115-2.p.ma
@@ -64,7 +64,7 @@ theorem prove_mv_39:
 \forall H3:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (implies (not (implies a b)) (not b)) truth
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL132-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL132-1.p.ma
index f13905176..330e40369 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL132-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL132-1.p.ma
@@ -59,7 +59,7 @@ theorem prove_wajsberg_lemma:
 \forall H3:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (implies x x) truth
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL133-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL133-1.p.ma
index 48138a19a..acd9538be 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL133-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL133-1.p.ma
@@ -61,7 +61,7 @@ theorem prove_wajsberg_lemma:
 \forall H4:\forall X:Univ.eq Univ (implies truth X) X.eq Univ x y
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL134-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL134-1.p.ma
index 96e607cea..d400f7cff 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL134-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL134-1.p.ma
@@ -59,7 +59,7 @@ theorem prove_wajsberg_lemma:
 \forall H3:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (implies x truth) truth
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL135-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL135-1.p.ma
index 1534861eb..9a982d8af 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL135-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL135-1.p.ma
@@ -64,7 +64,7 @@ theorem prove_wajsberg_lemma:
 \forall H3:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (implies x (implies y x)) truth
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL139-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL139-1.p.ma
index c05658d20..21a301128 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL139-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL139-1.p.ma
@@ -59,7 +59,7 @@ theorem prove_wajsberg_lemma:
 \forall H3:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (implies x (not truth)) (not x)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL140-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL140-1.p.ma
index a134410a2..c5148d2a8 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL140-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL140-1.p.ma
@@ -59,7 +59,7 @@ theorem prove_wajsberg_lemma:
 \forall H3:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (not (not x)) x
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL141-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL141-1.p.ma
index e70a70c3b..5f816e926 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL141-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL141-1.p.ma
@@ -64,7 +64,7 @@ theorem prove_wajsberg_lemma:
 \forall H3:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (implies (not x) (not y)) (implies y x)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL153-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL153-1.p.ma
index 391936013..827b99214 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL153-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL153-1.p.ma
@@ -129,7 +129,7 @@ theorem prove_alternative_wajsberg_axiom:
 \forall H15:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (not x) (xor x truth)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL154-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL154-1.p.ma
index 4c0c98507..169be886a 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL154-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL154-1.p.ma
@@ -129,7 +129,7 @@ theorem prove_alternative_wajsberg_axiom:
 \forall H15:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (xor x falsehood) x
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL155-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL155-1.p.ma
index 71ed352dd..d5cb7fb5e 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL155-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL155-1.p.ma
@@ -129,7 +129,7 @@ theorem prove_alternative_wajsberg_axiom:
 \forall H15:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (xor x x) falsehood
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL156-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL156-1.p.ma
index c01872fb9..3d5df92b6 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL156-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL156-1.p.ma
@@ -129,7 +129,7 @@ theorem prove_alternative_wajsberg_axiom:
 \forall H15:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (and_star x truth) x
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL157-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL157-1.p.ma
index e336e3a3a..97ea2cad9 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL157-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL157-1.p.ma
@@ -129,7 +129,7 @@ theorem prove_alternative_wajsberg_axiom:
 \forall H15:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (and_star x falsehood) falsehood
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL158-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL158-1.p.ma
index ed138bd52..32a4518b7 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL158-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL158-1.p.ma
@@ -129,7 +129,7 @@ theorem prove_alternative_wajsberg_axiom:
 \forall H15:\forall X:Univ.eq Univ (implies truth X) X.eq Univ (and_star (xor truth x) x) falsehood
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL161-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL161-1.p.ma
index 57fb55ec7..3961b05d8 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL161-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL161-1.p.ma
@@ -78,7 +78,7 @@ theorem prove_wajsberg_axiom:
 \forall H12:\forall X:Univ.eq Univ (not X) (xor X truth).eq Univ (implies truth x) x
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LCL164-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LCL164-1.p.ma
index a84605051..8850280e9 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LCL164-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LCL164-1.p.ma
@@ -79,7 +79,7 @@ theorem prove_wajsberg_axiom:
 \forall H12:\forall X:Univ.eq Univ (not X) (xor X truth).eq Univ (implies (implies (not x) (not y)) (implies y x)) truth
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LDA001-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/LDA001-1.p.ma
index 051af57e8..48e8b32cc 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LDA001-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LDA001-1.p.ma
@@ -36,7 +36,7 @@ theorem prove_equation:
 \forall H3:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (f X (f Y Z)) (f (f X Y) (f X Z)).eq Univ (f (f n3 n2) u) (f (f u u) u)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/LDA007-3.p.ma b/helm/software/matita/tests/TPTP/Veloci/LDA007-3.p.ma
index 11d43b6a2..534a5a9fd 100644
--- a/helm/software/matita/tests/TPTP/Veloci/LDA007-3.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/LDA007-3.p.ma
@@ -44,7 +44,7 @@ theorem prove_equation:
 \forall H5:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (f X (f Y Z)) (f (f X Y) (f X Z)).eq Univ (f t tsk) (f tt_ts tk)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/RNG007-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/RNG007-4.p.ma
index e981ee5ba..a9cdabd1d 100644
--- a/helm/software/matita/tests/TPTP/Veloci/RNG007-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/RNG007-4.p.ma
@@ -83,7 +83,7 @@ theorem prove_inverse:
 \forall H14:\forall X:Univ.eq Univ (add additive_identity X) X.eq Univ (add a a) additive_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/RNG008-4.p.ma b/helm/software/matita/tests/TPTP/Veloci/RNG008-4.p.ma
index 26341ce46..c56142d62 100644
--- a/helm/software/matita/tests/TPTP/Veloci/RNG008-4.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/RNG008-4.p.ma
@@ -87,7 +87,7 @@ theorem prove_commutativity:
 \forall H15:\forall X:Univ.eq Univ (add additive_identity X) X.eq Univ (multiply b a) c
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/RNG011-5.p.ma b/helm/software/matita/tests/TPTP/Veloci/RNG011-5.p.ma
index fcf436713..f7df33340 100644
--- a/helm/software/matita/tests/TPTP/Veloci/RNG011-5.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/RNG011-5.p.ma
@@ -76,7 +76,7 @@ theorem prove_equality:
 \forall H20:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (multiply (multiply (associator a a b) a) (associator a a b)) additive_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/RNG023-6.p.ma b/helm/software/matita/tests/TPTP/Veloci/RNG023-6.p.ma
index 8397d426f..e69e40345 100644
--- a/helm/software/matita/tests/TPTP/Veloci/RNG023-6.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/RNG023-6.p.ma
@@ -84,7 +84,7 @@ theorem prove_left_alternative:
 \forall H14:\forall X:Univ.eq Univ (add additive_identity X) X.eq Univ (associator x x y) additive_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/RNG023-7.p.ma b/helm/software/matita/tests/TPTP/Veloci/RNG023-7.p.ma
index 01e94c6a7..49260d096 100644
--- a/helm/software/matita/tests/TPTP/Veloci/RNG023-7.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/RNG023-7.p.ma
@@ -92,7 +92,7 @@ theorem prove_left_alternative:
 \forall H21:\forall X:Univ.eq Univ (add additive_identity X) X.eq Univ (associator x x y) additive_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/RNG024-6.p.ma b/helm/software/matita/tests/TPTP/Veloci/RNG024-6.p.ma
index 3785a9204..bdb4c04a7 100644
--- a/helm/software/matita/tests/TPTP/Veloci/RNG024-6.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/RNG024-6.p.ma
@@ -84,7 +84,7 @@ theorem prove_right_alternative:
 \forall H14:\forall X:Univ.eq Univ (add additive_identity X) X.eq Univ (associator x y y) additive_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/RNG024-7.p.ma b/helm/software/matita/tests/TPTP/Veloci/RNG024-7.p.ma
index 135db3ff2..afb63d9f6 100644
--- a/helm/software/matita/tests/TPTP/Veloci/RNG024-7.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/RNG024-7.p.ma
@@ -92,7 +92,7 @@ theorem prove_right_alternative:
 \forall H21:\forall X:Univ.eq Univ (add additive_identity X) X.eq Univ (associator x y y) additive_identity
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/ROB002-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/ROB002-1.p.ma
index 883467d61..81aabc975 100644
--- a/helm/software/matita/tests/TPTP/Veloci/ROB002-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/ROB002-1.p.ma
@@ -59,7 +59,7 @@ theorem prove_huntingtons_axiom:
 \forall H3:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (add (negate (add a (negate b))) (negate (add (negate a) (negate b)))) b
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/ROB009-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/ROB009-1.p.ma
index 90f1c10c9..e3e2ad2b4 100644
--- a/helm/software/matita/tests/TPTP/Veloci/ROB009-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/ROB009-1.p.ma
@@ -58,7 +58,7 @@ theorem prove_result:
 \forall H3:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ a b
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/ROB010-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/ROB010-1.p.ma
index 765898668..76f06f1af 100644
--- a/helm/software/matita/tests/TPTP/Veloci/ROB010-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/ROB010-1.p.ma
@@ -60,7 +60,7 @@ theorem prove_result:
 \forall H3:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (negate (add c (negate (add b a)))) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/ROB013-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/ROB013-1.p.ma
index fe79d1550..3039f3412 100644
--- a/helm/software/matita/tests/TPTP/Veloci/ROB013-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/ROB013-1.p.ma
@@ -58,7 +58,7 @@ theorem prove_result:
 \forall H3:\forall X:Univ.\forall Y:Univ.eq Univ (add X Y) (add Y X).eq Univ (negate (add c (negate (add (negate b) a)))) a
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.
diff --git a/helm/software/matita/tests/TPTP/Veloci/ROB030-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/ROB030-1.p.ma
index 9868ec4d5..72fe9de94 100644
--- a/helm/software/matita/tests/TPTP/Veloci/ROB030-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/ROB030-1.p.ma
@@ -64,7 +64,7 @@ exists[
 2:
 exists[
 2:
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 |
 skip]
diff --git a/helm/software/matita/tests/TPTP/Veloci/SYN083-1.p.ma b/helm/software/matita/tests/TPTP/Veloci/SYN083-1.p.ma
index 1dc7202c9..c8ac354f0 100644
--- a/helm/software/matita/tests/TPTP/Veloci/SYN083-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/SYN083-1.p.ma
@@ -31,7 +31,7 @@ theorem prove_this:
 \forall H0:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (f X (f Y Z)) (f (f X Y) Z).eq Univ (f a (f b (f c d))) (f (f (f a b) c) d)
 .
 intros.
-autobatch paramodulation timeout=100.
+autobatch paramodulation timeout=100;
 try assumption.
 print proofterm.
 qed.