auto --> autobatch

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 4cc2223d110f70c9d265113ba78733e1a3667168..38c012e5a6acef152bb050c35bf534f9d99c7775 100644 (file)
--- 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.
-auto 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 93b11c287d87b6a7f34c18064bcade604e099d2e..cbbae8bea25b4317746db26a2c658ec7ae6aa86e 100644 (file)
--- 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.
-auto 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 89dfcf3149887b8dc3433b2362f6cc310d41af7b..b5fed12aca2086034c526b9417b5792948fd5e08 100644 (file)
--- 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.
-auto 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 4ea34f1e01624a6cc0b14702a420f500ad4915de..cd5cb41d879b7949db3762fd947bbaa62b30b64c 100644 (file)
--- 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.
-auto 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 9542f452a830ecd06856b4bb031d1ba0d8d14c3d..c173d004c30a58dbb1ba2bc4792f3b1fd4ce95c6 100644 (file)
--- 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.
-auto 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 c098b6cfb1965e8e09c98916f27aaaa8651cc317..e3e65f488601de6b050344711569f9f599629a74 100644 (file)
--- 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.
-auto 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 04f83193c4682e705fc7664a35debddf5f007ffa..655401b3430ca1f75779d6c6fed7c87da728b7b3 100644 (file)
--- 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.
-auto 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 0fd7e320c03679309c4e6c96e7bef1f00f9a8dce..69b96f774a3af4151c83b525a0315d35273a9331 100644 (file)
--- 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.
-auto 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 4a04acbd956d02d1431886baac30b5deba542083..6b9db399f168bb121a629ddd02d57b8a09f110fb 100644 (file)
--- 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.
-auto 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 3328ed780e7c6b913c7980629b5e961524e92efd..201ba75c35a65d9b48caa105b4b4653dd4a4bef2 100644 (file)
--- 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.
-auto 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 fd724a6a3f7d609658319c76b85a95a7d7d2b9f8..1987e3b12537f09fb03fe76446e59e52f0b3bba1 100644 (file)
--- 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.
-auto 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 8178f40434bc665bbe98b56c95135921ea00073a..f177f9c744440f3f9e00400a1294ce5957b8e4d3 100644 (file)
--- 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.
-auto 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 764399c396a4c9aaa193616b21a809e1d5681a4c..7b22061dfb57974ba5b6445fabaf6af8811ba7a8 100644 (file)
--- 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.
-auto 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 94fafbca736ba1861d87ae9ddf67a0fab5e63d6b..b0c35a76773c0145102f96e124c3218881ec569f 100644 (file)
--- 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.
-auto 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 6451f3bd7b0beb8e2a867e9d54f93867b0bac5fe..3353f8df4d77677a5e685873ea01e03230e04334 100644 (file)
--- 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.
-auto 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 2823a41140a01db13744d72c006605240b943e8b..209840c60ad95d439ce1da0f2fe60cc9c0bd4e38 100644 (file)
--- 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.
-auto 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 bdd9c07e8d4f50764f8d588a25258ce70fbeac93..a3bfe1c4bb6bb36d28c48aa199a9076f3e20d17a 100644 (file)
--- 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.
-auto 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 202b96c7d7e9fce0953606570d3985cfb3ea78ef..1b7800d75d328adbf9dae7164e852ca271bf0014 100644 (file)
--- 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.
-auto 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 2eab59e4fbc24fde8ec3e28e61119393b05cbaf3..446b2b4736f548961176eccf963f365694f63971 100644 (file)
--- 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.
-auto 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 91aec5ae7b363e46a1ca76bf2f793d140dadfac6..a8d1ab9e7e1bb4e03d2afb609fa11554fb06b99a 100644 (file)
--- 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.
-auto 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 ba23e0205acfe62ca30aeca2c39b0b131e14337c..60ded0c1a507e35f95b342f132d2c6b318a7e11a 100644 (file)
--- 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.
-auto 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 6d6f2ab0661732c17b223b34038ea2583918b85b..8e2774c340670c7d6eda610cd00b254f436fe998 100644 (file)
--- 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.
-auto 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 a1626bf6d9325eade289b397e29943d1194ff0ac..e1f26e13d0ab99f5d6af560cf7df7be95671939a 100644 (file)
--- 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.
-auto 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 123624d1bd09d93ff37cac8588aa46564ee26b4d..f76194c67a8484a824b8a60adf4a4509f1e2e422 100644 (file)
--- 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.
-auto 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 d76c4142ce60fc1f6cb41aafe3e89bdff8543397..806df9654167120a3c5ce045fa04d3117c70069c 100644 (file)
--- 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.
-auto 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 1f399f86220471c2e3640bcdb586d71a8c3585e9..7f6d96d3c4cf6f929eafe179fd9b166fb66bd139 100644 (file)
--- 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.
-auto 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 c2cf3ecbc486cda0e091fedd896c652e0318f629..d88025c42652e460d627bdedfa6fc6ff7a8e89b9 100644 (file)
--- 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.
-auto 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 6154d8a34ca4550b30ef47c34491190fa6157ed8..7018646d33cce008f686faabec5faa78c04f1513 100644 (file)
--- 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:
-auto 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 e8f9b346725afdc352175278e0828063db206856..deee838a4f14a535657e9bd31ea78e251001a327 100644 (file)
--- 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:
-auto 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 d8da7dbe8ed72f57802e44758a798bc2f2397fe6..61e95267a84f9403ea1535420a13ccd648c1e776 100644 (file)
--- 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:
-auto 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 5b38f0dd823ad64cef45f3f4ad489958d6205a03..5aba07935fb3a857e48222a59d3bdb0fb8d26a65 100644 (file)
--- 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:
-auto 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 6ff4fddd1dee4405db0001343c74dab9811f6b13..ee3f5f7ba8f5c6b74ac51778a0fd4fd24488f40c 100644 (file)
--- 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:
-auto 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 2e179255d44c10601a5cb53c83b4898858d360be..ef4e82eddbb388c3cf6b853f3101b07ea87468c8 100644 (file)
--- 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:
-auto 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 d2cc7be9fc92de48be6e1992076791be556c035b..2f4b472726b1de37974f696a7e882f1eefaa4e1f 100644 (file)
--- 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:
-auto 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 5e84cf2771b49e43b052803bcbe0438e5626fffe..b655e805ab5ff4513b4cf1f08b68c0a526bda465 100644 (file)
--- 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:
-auto 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 e6db2d319974b7c86e400de9c69d50834785b0e1..eb063cf1ec649cf5de944729128c637ea46f013f 100644 (file)
--- 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:
-auto 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 4aca85e92410d7c3d27b31485f4198301b9bc8a8..87b023fdf767ddb0357123ec0a86159bf69cbbec 100644 (file)
--- 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:
-auto 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 144fac75baa5e964c31ce4dc40b4aa6a8c64dfcf..6125379462a0a143b2abbed42046bc3b0be06a1c 100644 (file)
--- 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:
-auto 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 b8b90725bbe50a51909fe37dffe80a9ba95ee492..866d0abd70a72aa12d6446f7b5df26064c06d8dd 100644 (file)
--- 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:
-auto 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 0ade23762faa026f01e6649c1ad0d448c99c013f..5476a13a10b6192fbe24b9033a30cc8c5f03d84f 100644 (file)
--- 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:
-auto 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 7a21954e57840dfaf27f067e98e652d858082c50..d5c98aabfe802f7ff26b22d526b70f1a120633c4 100644 (file)
--- 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:
-auto 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 724503625bb679fa5a967bdbb5cbb5862b16561f..6ea3f3676dd92e3833ae2e727fb23992e36ca1d6 100644 (file)
--- 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:
-auto 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 728762834a4910a16904411ae18efe8127efc7f1..bee9580b08c91ed76d2dca01528309101d620325 100644 (file)
--- 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:
-auto 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 662e3d7cd0782d990f5c3791106337db465e9950..716626e843c933c49bb3df72d0a14d53736ac34c 100644 (file)
--- 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:
-auto 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 86a05a99bf51b3a31016e2d727684e54a17f21c8..b0e94a980c1e776ead4d1c311e84f3a27c59a91e 100644 (file)
--- 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.
-auto 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 f3e5b5d5221f91b2e1178c60fd33c7abb23cdbd2..32802b0c56177bcd74497892b06722531bb7103b 100644 (file)
--- 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.
-auto 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 746e14da2a0f24a62e0aaed910620c9d3e04a057..8ed2fdd81a03e4b84c40e1db6db16553ae54e896 100644 (file)
--- 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.
-auto 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 24ccd93b498461492c954837fbac4e0e38d7b6c9..e33abe6e76eb5eaf5d5f9d5630565051abc693ca 100644 (file)
--- 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.
-auto 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 41779cae6bbf4caff1578e1aee5fc54131b0496d..14e0f74a0378636bda13328112d6875a0064fdb1 100644 (file)
--- 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.
-auto 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 a59f55f4b5b7fc83dbe0ed07a94047a3f63d9d3e..ca9a9653d69ad03525cd49477680160a4bc07d9f 100644 (file)
--- 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.
-auto 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 b366a3f9f7e1e209f34121e8cbde6e7b8ad9d0fc..839f6ae9376d5869c217fc461dc08a9a17955141 100644 (file)
--- 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.
-auto 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 3734fb97180239b01706d2bd91dcc6ed06a647ca..5b8ad716ec42d3c069c5b712b8a48628c56c73c3 100644 (file)
--- 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.
-auto 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 1857b0fbaba86854f6486b6ce3910acb371fb63a..31a6ae8ec3241d86dc109b2f036e9e4820255139 100644 (file)
--- 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.
-auto 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 fddb0328a780afeda189ea9962547f02621ba705..1c5133b0ef3f1cf7492e810f38e54d71e70a2cbb 100644 (file)
--- 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.
-auto 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 6f4ebb66470a30ec2263c90aa334d552d01a7a95..b341b737b43cc10d435958c451484aa7ef24e49d 100644 (file)
--- 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.
-auto 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 636fa6b6db88b2290173c5e224c0f2e33ab37330..22976148e4b600aae95a4e6af2ca837738eb6377 100644 (file)
--- 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.
-auto 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 e60af56ceff98ff7d3ca1e9e8e1c21f3586027f4..b7c423748ff7c9f06362870f5114faee8e8421d4 100644 (file)
--- 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.
-auto 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 a179ccebad2b6b0eb9dd3fc1bd3ef84ee123f4c6..5b45bc7ea1452aa3bfac6e95ecdb4dfb2a0c82b4 100644 (file)
--- 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.
-auto 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 2d2bbc7c53807ffc400fa89539d90f670bdb3731..88b85eb9bda68fb51a0f0a7164aab7cc1a267738 100644 (file)
--- 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.
-auto 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 9c6113adaf432be0f43ff5ae21286a1948525625..c1690d0652a167cffcfa94a5b149b74c094e152e 100644 (file)
--- 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.
-auto 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 dd0f1ffbeb4bf8f2e461dc75c3dd87c6c836e69c..989b3c1bff71b1f9556cdcd8e459c6d1feadb3b0 100644 (file)
--- 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.
-auto 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 dfdc9b00deba455d4da47a0e88983d6c3b3ea41d..cb5635f98c969850cfea8d9b98b91e1088d5e197 100644 (file)
--- 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.
-auto 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 f2cb5118ffc461e3317b48aeaa8160f4fce28003..d7a0a9cabf5f7882288a9a6c20aeb63abf5483f4 100644 (file)
--- 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.
-auto 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 cc05447be0f8d2df6f149b762cf357f2fef992da..89111c67994fe927718c431725412674bb86922f 100644 (file)
--- 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.
-auto 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 36233810860966d7595a527dff10e0d982ee71c8..8e6ad6cdb5640fb859382b4795d2a83c1e8a59e8 100644 (file)
--- 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.
-auto 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 02fbbcabbab97d7fd3b7c39d42b5a863f2f61c17..870b7d8629351676345276025fda2c1d6c043a0c 100644 (file)
--- 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:
-auto 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 a1c8dd0abbc1b33aac8af66abfd07bcc4f459b2e..f345021bf5ff2ab0abdac09d0c9785bd21e5c279 100644 (file)
--- 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:
-auto 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 fe71489cf369f52b910c8f556811d520a9bc1744..ff1981363c952a82d8e533bc52c5a2db3c51607b 100644 (file)
--- 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:
-auto 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 0f7c24aa0dfd705bf664a91ac840e75b269cbc8d..030c2cd33498cbfef8ba8c1a52989c4467da1bc9 100644 (file)
--- 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:
-auto 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 fcb3b6afd38e2b299a28b60cbcca4f7972124451..c695b7f80d96bfa778a938e02eac126d723b8799 100644 (file)
--- 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.
-auto 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 1011802d4ddc1a62d2f7becff087e90604c8ea80..ea943fdd8e170267dd986afb65f9e86e0efdf6e8 100644 (file)
--- 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.
-auto 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 83be67ecfd4c385f07397b11de764e6e1f2b5b79..ce5111529eb0bdecd5b2b82e5817f366dd244344 100644 (file)
--- 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.
-auto 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 3bf8fe21ae1b3eb2af325bf9e9cf28b5605de3f1..d11f4a5f4f3ee40b2f4f53570cc1e77947299a55 100644 (file)
--- 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.
-auto 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 f97360370f53f2062f761ed0244481d3e586d86f..4d7966963ded817604664732f9292372addfc7a3 100644 (file)
--- 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.
-auto 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 4e0da1e47d95eae0da970c2e0f9a49f41d5684ac..034f854c3a203463db8a7c08a99695d6a2823d29 100644 (file)
--- 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.
-auto 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 afeda0d1fbeccbad17291200457a4e1c687507c2..f5cb3725201b299016314831ac2870321d946a49 100644 (file)
--- 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.
-auto 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 773068e1f4d7f084931c700fd16a68dbe328b583..dafda9a6ed4a254191a47dd14bd74a1e293da8ae 100644 (file)
--- 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.
-auto 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 e6bf5c0b28a5c4f2806c53dde4199420124aea9f..d7895138bc93f38493202e2f5c7bd76c103af0a3 100644 (file)
--- 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.
-auto 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 e33eac2ac9a898e2ae63c8a9ec83fb66cc827c1e..2d04443b6716fd2448588b48966bc28e59936e4c 100644 (file)
--- 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.
-auto 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 562cd181147582543a900d0239140d9aa2963f7d..d348a57dbc1e2f0bb246c3450b8a4f200e0c8255 100644 (file)
--- 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.
-auto 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 7736d1567b95f01cf33a6408b3861f5ee8a0573c..b3380a855d81488f79aa764178478b7b7d988a0f 100644 (file)
--- 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.
-auto 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 f570845cdef12b4b6ae02a95d9781caef8450a94..34885590c0390a164e840efaf91bc89d19733fd7 100644 (file)
--- 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.
-auto 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 6847c52b6986d6d1c8653d378882066c3cc33a9b..1e3644eae889f5d21b5643976aa9e043556717c9 100644 (file)
--- 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.
-auto 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 40442e00ae9eb333d1d4b0de395dd8ad0abbdcaa..6b7b50871462459639ac3178601c9561a13b78cd 100644 (file)
--- 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.
-auto 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 0727c7051ccc90990566d9ae56368ec870cb0b15..ac52f8966b158b3e35704f96abef5d39c35c1353 100644 (file)
--- 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.
-auto 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 887c1ba02b7baf6e9a5b5e605066b3e8a658feb2..cefbb9734eba03bf391cf47c9360f60c74a10d67 100644 (file)
--- 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.
-auto 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 3d19c2c0274fcfe968e744dc91acc8eeea7cddc5..920463e1224ae949e48c1ae6bba5616e235df5db 100644 (file)
--- 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.
-auto 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 bbce5c045bb709889f7c0f004616332eee4d4787..63b6c5087e7a8c0eca1abc9e03ad9a9ffd7c140c 100644 (file)
--- 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.
-auto 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 ce184d7d14b527903305cde399c9c30143ae0a8d..2c39e935df1ac2cb50c67cdf5dfc3a41d7aacb99 100644 (file)
--- 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.
-auto 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 bdbd3df361008b8fd2515f9344f38a5b4823730b..9030600cb1095a9b282ea081bb57f7577ec54068 100644 (file)
--- 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.
-auto 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 bb79b6b400a04385c43846f8733ddbdd08de4892..ceae0141049d9c0c021e1a61226ba30ab55a0fb3 100644 (file)
--- 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.
-auto 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 d1f8a8f4e5376a0271599ae088ed5b53114636b4..454c6154687cb9385cd57b92c29e362b2ab4d1dc 100644 (file)
--- 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.
-auto 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 a657802e9877fb657aab02094083ff9c4aa09c39..941fc726c9413e911661af6f9d8d89a54fa2bdc7 100644 (file)
--- 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.
-auto 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 5fb6b69282f615ef2954cfb2c40f1d2bd2b7088e..c677c140c1eed38c85af098ab14e1944f98debb4 100644 (file)
--- 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.
-auto 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 0212ea9038a9d543037a7b12036e997ec965eaba..04245f9de6e3f5645e3fe571e851954704a1d1cb 100644 (file)
--- 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.
-auto 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 7531e2af3926075aa6fca2147d49f33cff640cdd..b7149e55f31790792df7e53ab6d434139cbacb2d 100644 (file)
--- 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.
-auto 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 0f55687c183ef7ff25bebc47ddbaabf85036efc9..db0a9b38f11b5c03b581b55a1500ddef9a1e929e 100644 (file)
--- 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.
-auto 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 98bb065228cb64469fee32dd6262802c583b1b5d..10948cac5da819da0c63eb65e8d29625b6670fa5 100644 (file)
--- 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.
-auto 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 f725b2f7b760d5ccce8d79a014d3128ab0557f12..269be40420b01e9157738de1438dc0dc1b5bcd70 100644 (file)
--- 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.
-auto 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 90c11d85a4fdbb73558e2e726d0782fe78426874..1a9471a66d7d41a51b4c2812a16c2ea9faad094e 100644 (file)
--- 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.
-auto 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 383b0e2d10f58c5a1b3dcdb8c454d340948e1dad..0aa320f7d637c0add10046425e311cb201c2db7c 100644 (file)
--- 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.
-auto 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 29a70eadcb1100b966fdbce861c014945be58efc..473d47bc4e7fe86b71c0c8799fc5aa11e61a0132 100644 (file)
--- 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.
-auto 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 03ee7c53f9024302afa2b5d26b66d9362b54cf17..c1af39429208356f0b64e92b2d2c850cd448d43a 100644 (file)
--- 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.
-auto 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 e6fc69f78c792d63a1c477cb7b7f7258c377cc91..964662f6cc607ee0e980d26a05a313ec59bb3f8c 100644 (file)
--- 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.
-auto 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 18243968e41ee32f6a76d21fbdd3a5b8216023aa..162fcd775cc4c4a89594aff60b2cdf4a5350874d 100644 (file)
--- a/helm/software/matita/tests/TPTP/Veloci/GRP168-1.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP168-1.p.ma
@@ -4,7 +4,7 @@ include "logic/equality.ma".
 (* -------------------------------------------------------------------------- *)
 (*  File     : GRP168-1 : TPTP v3.1.1. Bugfixed v1.2.1. *)
 (*  Domain   : Group Theory (Lattice Ordered) *)
-(*  Problem  : Inner group automorphisms are order preserving *)
+(*  Problem  : Inner group autobatchmorphisms are order preserving *)
 (*  Version  : [Fuc94] (equality) axioms. *)
 (*  English  :  *)
 (*  Refs     : [Fuc94] Fuchs (1994), The Application of Goal-Orientated Heuri *)
@@ -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.
-auto 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 bcf26d5d95399270d42dd2280a1cbd6ec703a5ec..ff7f0696703ec37e5af526eab87c3ca9605599be 100644 (file)
--- a/helm/software/matita/tests/TPTP/Veloci/GRP168-2.p.ma
+++ b/helm/software/matita/tests/TPTP/Veloci/GRP168-2.p.ma
@@ -4,7 +4,7 @@ include "logic/equality.ma".
 (* -------------------------------------------------------------------------- *)
 (*  File     : GRP168-2 : TPTP v3.1.1. Bugfixed v1.2.1. *)
 (*  Domain   : Group Theory (Lattice Ordered) *)
-(*  Problem  : Inner group automorphisms are order preserving *)
+(*  Problem  : Inner group autobatchmorphisms are order preserving *)
 (*  Version  : [Fuc94] (equality) axioms. *)
 (*             Theorem formulation : Dual. *)
 (*  English  :  *)
@@ -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.
-auto 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 849057bc54e2faf3dc646debd38a9b41ed257ab6..34791231e8b5e95fb23ad4d77da125867cb734cb 100644 (file)
--- 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.
-auto 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 076784ef82708fc2d5bcec15e0e7fbe12a8b47b6..77177b3f52acbbba6287e780aed586d55f8d98e0 100644 (file)
--- 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.
-auto 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 b67193505fb031ae12bda1e43040bf97c04554e3..485cd7c0e532309081238e625cf1745edc729b60 100644 (file)
--- 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.
-auto 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 33d15dcc3effc6c617f81ea0e5762f586c8e74d6..e5dbe4ab7dd391ce5fb07bd4087b63e1f38048ce 100644 (file)
--- 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.
-auto 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 3b13987b5c6b457c6faba669cc9f76e5adbb7310..25f4ec89dffcb63263875b0d22ec65058bebdd3a 100644 (file)
--- 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.
-auto 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 59f725c19e43cc3df43b2cb47f9e758fea1db076..99d2f2272ac434d9d3fcfd229def58cf7f65d614 100644 (file)
--- 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.
-auto 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 4c890fbd175c13c180d53cfc16ee8d913d9dcd40..ad3388fcf9e4986ac0587cf5206467e45652c453 100644 (file)
--- 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.
-auto 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 1942f7064097a84600e6e6bc0ff3b1deeeb2f038..c5f686a70a6639765092f99e02613598761d10c6 100644 (file)
--- 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.
-auto 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 a358b5fd3bd52441e1847fa96759b50f3b38ee41..d5ba153b9e44693f97517b7d9ebdffd118267c07 100644 (file)
--- 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.
-auto 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 aac5c99e71c5998fa1f17910f653e592a6a4d2b7..eb035cbbbdb4f577e89a5ecd7a2eea3b7c58e9d3 100644 (file)
--- 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.
-auto 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 a4142e5c94c6c4373eeb28b12723911e75ea3621..2ad492bcfd7e78b0172545ae0a88293c8147a1b2 100644 (file)
--- 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.
-auto 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 043fc5af7c90c055a464c78cb3d00e67ce6490f9..9008f3ef0e1f3b6e368d8800db074638199208bf 100644 (file)
--- 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.
-auto 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 47d76e5e258d3fa0979397d271a80718d207a1f4..d2fff5b3d0c31ee1e4b3e30a6d861e10cbc2f2b0 100644 (file)
--- 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.
-auto 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 7d83966759574459a810d258decfeef6192bf59d..eedb47810f62fa399a2718d6c16dbbafae2451e5 100644 (file)
--- 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.
-auto 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 cbfcff30c07528dec7cb5db5b600a1498b2954a0..8463afd62ba1ba9addad67e68bb293c4d830e474 100644 (file)
--- 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.
-auto 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 62ad0624cee90f5b298a7ad01895f4435e0af508..bec8aa7f77c5dc75c0be152b9f10adf43519dffa 100644 (file)
--- 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.
-auto 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 9281a270ae34b5113728ccd27077c589826a4c7c..a3f949d3ef705d7f7458fe40ff69e45ea0ff8454 100644 (file)
--- 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.
-auto 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 ef2028982032601a18700b97016393600b972f1c..c70c4f672750dd4128c375f14a43b75335158e4d 100644 (file)
--- 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.
-auto 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 1804cdb7806294c3914faae4ca9bb62bc7c14eed..c5b9d8c5d5917ff490df521e318cd3f86928bf74 100644 (file)
--- 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.
-auto 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 fcba4e4e7be7f2da215e5874938a556490a9c495..3358805bc9408d96d13d04ecf241914acbba3703 100644 (file)
--- 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.
-auto 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 3d782b025a9bccd2c7f61a30dd476d985ab402b9..e297b3b08085b2e8e7929164a4e4d93129fb662c 100644 (file)
--- 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.
-auto 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 3ade697807165137cd4cb230404310cad2419c36..c3302ae0c486c0cc9fc9ac6adb9c5ec8811bdaa6 100644 (file)
--- 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.
-auto 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 6413b57436b0c335d1f20d240156426ab1a8a625..7dcd0f6989a1415adf1a717dc9b02007caf1da18 100644 (file)
--- 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.
-auto 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 6bf79424052646fdaa2721d97628702c57fd947e..be1180422cccc0de7950eedccd20b1a7f40f7686 100644 (file)
--- 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.
-auto 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 2ebeb9f5d11b2f26eb2e4abc1cfce0a769f8f3a5..f7723d3c077c8302ebb01bf192e68b9ccc59992a 100644 (file)
--- 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.
-auto 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 c4eaf586110e166ccdce790307e96873a6b57b1b..e5f0a50ed172a5ddeaa6cf419504073c277f9634 100644 (file)
--- 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.
-auto 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 b673ea1fe23a08a0b3918f45b37257e28b13b8a6..746cf9541c0d7235268b6885246a16702b760200 100644 (file)
--- 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.
-auto 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 21831160b07a52757bb343f3916649468647553e..63fe7d2a12eabee90aa036243698335c96299846 100644 (file)
--- 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.
-auto 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 264794f5095e6b0d43030c32ab3068750f5095be..b8ecfd815755435c70e86a122836eb3265ed5088 100644 (file)
--- 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.
-auto 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 51a728493f532e3fe019ba4c70f679c7fde27b10..b679645fe2a0f4f9d80e94ae46509b31615ca989 100644 (file)
--- 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.
-auto 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 0026f5c894124afad4facd1396b539065dd5aa44..c6b63cbcf0a6b1d9bf111e7129d6fa5403fc0d58 100644 (file)
--- 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.
-auto 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 fe07b798dd04b16a952f5e6240b15883d85faa3c..326e725021ab233cbf3388d5ffebd4665e502bce 100644 (file)
--- 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.
-auto 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 600af87e1ed5154f91b023c3ce4e14cd70bf9eac..39482784f94ecb3987af66c7909552c61e34d12f 100644 (file)
--- 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.
-auto 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 921714afd8d5802d41186134bcc80f6f919dccbd..3af993fcf64b1b30f5a993687581f9f909af480e 100644 (file)
--- 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.
-auto 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 8963ddaf8c14bba1bbb5c1bf201ac222784b12ae..059f6e300ef901825cf9294323f524d5dbdf7006 100644 (file)
--- 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.
-auto 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 0e280132b5812d2cb7be19cd8641ef5662cf5442..888ad8576dd204c80833d8be96cb25ad4cb4621f 100644 (file)
--- 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.
-auto 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 af079e663ea86e0e5cccdea20f343b861dd9a8f5..8c6d03b3d3c8a2d80d68da59c78a358362359e84 100644 (file)
--- 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.
-auto 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 d655496c5a7b95234d59ae884ecb19487f9747a3..f96492e1323cb460407be3b2f65a2743532cacdd 100644 (file)
--- 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.
-auto 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 a7d1d5a8eed7a1e903e0de5fcd28d061198a7503..79e82ae64824dee08d529b2fdb0a960352f36639 100644 (file)
--- 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.
-auto 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 e26c08db4e3f407cfb2ee0078ab6d91798c675f8..d2cac96d095dde1ceec5a3fd5e3b8d96fdc81b12 100644 (file)
--- 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.
-auto 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 0458df1fab5df73bfc2c04b515bffe2d03a9753a..dfbaf1362c1bb08431df81b81ef49e865db60456 100644 (file)
--- 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.
-auto 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 146e6a8141932c3b219b1f6ec872bcdb49588375..7806668c00f452bb83d6ddf688e9f0dffad40564 100644 (file)
--- 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.
-auto 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 466126222903977608cdab6cde51ad70a7535802..34d3bab743d45b47937422ae8818306461c288a1 100644 (file)
--- 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.
-auto 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 e78bed00fb5f380785cceaf18fd758be001331e5..790814570ef377da7c921589977228887820594f 100644 (file)
--- 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.
-auto 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 fdf42d7482fbf94d8176f055e6e8e2d3de830d63..0228172975cacf3c5d0c54c1ef258dc640c48f40 100644 (file)
--- 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.
-auto 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 74dc8a63a312f584cdb10222a59219dc40a15c28..44411f118e6ac4fa0b8c7052e138376c558ba645 100644 (file)
--- 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.
-auto 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 83eb4b753ff39076281bfd1d204a48fdbb49e811..2ad540b74a9f876e270b5792bdaf4eeeffdbaed0 100644 (file)
--- 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.
-auto 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 dde992a18be11a2553064a53aee52ec94a05327e..59a8da6ac7efdbe48ecbdab1bdbffb5cf4a552cd 100644 (file)
--- 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.
-auto 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 ee9bff2fc5e764654976c5fd72f49937992fe076..e268d2534e0b5a087409f015648c196d603ac05d 100644 (file)
--- 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.
-auto 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 6ff2950a60a8cb9655d4d8e3900a5a2fab6dec36..89a742ca10f22f9b2f123dbf01fce9d0b8723376 100644 (file)
--- 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.
-auto 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 33f0bd79af30580fac1b799a500bb88e79ee4893..879b8f0a9112a786119a34d99fe24b0ae05e2291 100644 (file)
--- 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.
-auto 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 ab4a5010442ad01b08c5112c449739719c8105f0..446167f51702bb90033cb15b27d4ec3c9efd11a5 100644 (file)
--- 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.
-auto 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 37900e2ec9452e89b8bdcc99d77a80c146240e43..6e084eef48c4c3c846c9730d22120e877a6ac7ec 100644 (file)
--- 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.
-auto 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 efe72032bc7eb19bf7480fedd97cc837d85b576e..2e80e0158a1757d8f080bf22ca1578357dea2256 100644 (file)
--- 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.
-auto 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 66b15a5cfb001f90d4b5a90bb9660d86075d4185..3a5257ed0861d394eeb918d7ae6fc83c5a61773c 100644 (file)
--- 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.
-auto 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 1e66b6585a6feb9be4f167ed9db945ca3d5ce754..e4caec04b8e504ad744817fee1182ff64d41a0e9 100644 (file)
--- 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.
-auto 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 bc5433839ccbef7000d6fd1e167a365660f5239f..ba46f7f716c80732cddb05e1fe1c750dc72bb959 100644 (file)
--- 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.
-auto 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 5256be7249b1df2a86a8ed7031c0a595d539f862..981df2d128d13a3ea5964acfd388126671eb80e8 100644 (file)
--- 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.
-auto 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 91748c17f64b0e6f72f5e00017500f585bdca1c7..8750ac7e8b0a55b641ecff9e22f97608272b6098 100644 (file)
--- 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.
-auto 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 eb94e08e2ef0bfe1cb737ac03a0e0a6266b7b2e1..9e5165b72a604c50f782294c8061951339b07cc2 100644 (file)
--- 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.
-auto 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 69d89ee91f74c3c9bb2b42a97614447dae81472c..ceb1fcb92843ca028592a3d0eb7811e77cf1d8c9 100644 (file)
--- 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.
-auto 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 77abdbeea86449f98142fabe5baf9c93441f905f..69b83f64d9405685dbc778654be7cb5017dadcaf 100644 (file)
--- 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.
-auto 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 f04d0b10cd69dc232a4687af26f9bd2d96263e15..72d8dbb1ac034540e7b12a27cc5898fc344c9124 100644 (file)
--- 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.
-auto 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 f9dbfb85ef4b2d9139c407510e68ddaeb6a5d41e..7ff2cf4fc9383ebc325d885c747a5ff7ff9551b5 100644 (file)
--- 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.
-auto 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 09e45674e91206425563b756fcb890184fe5c82d..d3ffe8859e78ba4626e0cbe69ca6b5ea1a8c91e3 100644 (file)
--- 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.
-auto 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 e411b5724eb3e56c861d5ec0480b1e2a05eaefb1..f145a3af95a32589f88dc493ad2f996621b17d6e 100644 (file)
--- 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.
-auto 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 396c9dd37dc5f40bc4085d7c9ecf66d72eb0059c..d6d1ef6ed7e4bdcc188bb0454172dd562a00b5a0 100644 (file)
--- 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.
-auto 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 0a2a60ff2d035c8b67cea160897435b7f680523f..118adfa7a770288b5faf3632d107c9ab88a9d7f8 100644 (file)
--- 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.
-auto 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 df8fe3ff816b141ef62d80800ae6b9ce6ed5b1ae..c46fb73d6c217c20d14eb1bc4abc812ca0892073 100644 (file)
--- 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.
-auto 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 5a76d9981c6c94125ed6f7f4c24d408f6836c882..e9151448c31fd25e05eef1f0c3d0c37d61195cbb 100644 (file)
--- 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.
-auto 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 b647dce22c5cf613e125ddf01de314fdc43fdc70..23b805f007ef413fff59a1e77f63ce3f29a02a83 100644 (file)
--- 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.
-auto 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 cf0a795d9d0eea82edfbf468ea6c171638e9124a..e77e2b7620aef78c5b4225015fc61967dba54dd3 100644 (file)
--- 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.
-auto 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 16cd566aafe5d39204d07792670a95776d312bc7..07adcfd9b2c0bae5ad15162e3f7d046a5f51afb1 100644 (file)
--- 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.
-auto 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 118437264c9152daea23bf360c01f62780c6ab33..260522c0536d33ae2e5bbd488141847d90c5e98d 100644 (file)
--- 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.
-auto 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 9720c564a00617e339a5e2271326b47ddc3f1640..d74cd154f12d300456a5f7e6644a8fed437feb78 100644 (file)
--- 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.
-auto 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 f740a647f82b0525c3d4106bba2baf2e54bec7bc..270768037c78bbe72df1dcbb2db4acb841f8f007 100644 (file)
--- 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.
-auto 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 760a125648fcf34ea367236cffd39bf00e1867f4..1ae737d5bf7484be68eec50fcb71d41f6636003f 100644 (file)
--- 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.
-auto 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 1f6da909a86bf0e873704f4a8ec0ac500139a329..a3d3395f5b525479bed478a4d11371749aaf5238 100644 (file)
--- 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.
-auto 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 0f9ec0dbb788cffd3bdcc57cd2cabe647d63c89e..d192c04554f4c1a0b35899e238226da003a7ec9e 100644 (file)
--- 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.
-auto 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 4189216495b9f856caeb22b12257043a1e561846..e0836fded57745e7bcfbebf624b935920c3e5267 100644 (file)
--- 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.
-auto 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 e44ea55db0a29ecb3e442f7b897c1bc5f759a690..ef7d1793f9d28bedb76a0f5d682963668724fc02 100644 (file)
--- 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.
-auto 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 c37de12c23a4026677abd7d9b39c4f451db64845..aee50acd9f383533039ba2ad73831f077e043f7a 100644 (file)
--- 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.
-auto 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 ccaa5e80ed9117015c7cfab17685338fbde67c13..76b98c5a29040b22e690a8bb84e1b2511d8867fa 100644 (file)
--- 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.
-auto 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 74691ad6d993db1c94400fa0e23b3da7bc55ff3f..2c1a81a7d9776e7b13018ae096e1d6e046201ed8 100644 (file)
--- 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.
-auto 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 a82d60e8853d60b6d10547752a3807d1f87af845..eb1c927ecebc608f56a77553ef6259413779a422 100644 (file)
--- 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.
-auto 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 e743542a3a2f5492fbc4ff6701852b9fb04d8a0f..b66e93f4326c5ac1bb39a30b55e0620de36a973b 100644 (file)
--- 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.
-auto 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 5b2a189eca6ea48fcee3e08329aa125d17897cd9..9c4c69ed04e6c21b2f965b155eab93fedb30ffac 100644 (file)
--- 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.
-auto 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 66ef7c5558379639f65ac844bad7c4dec6d1c1a0..1c32572b03639601d6187d0d7af774c9574e6712 100644 (file)
--- 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.
-auto 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 c89d132522e546aa1db50261ca66db7fece65d28..3a8c3f1323da3d19638f2aeaccb768d769f7f973 100644 (file)
--- 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.
-auto 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 0e9eac4745f98db0ab41fa1be27db298171c12d7..c2c748817dc6a0a91900a4c3e295f94fcd124baf 100644 (file)
--- 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.
-auto 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 354515802b3494f2f2836b55e56cc010999d0667..d17416172d31725d31a5890b577058ac808bda13 100644 (file)
--- 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.
-auto 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 9def73c5ffc4122105796d648f8ae6cc0ea13766..45b171485926b697e088a209829ad9f6726ef17f 100644 (file)
--- 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.
-auto 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 dd33c8ed7934b70447283f1cdf99c655b3571f10..3076cda7d3021200388fff7f9607a24038fe0dd3 100644 (file)
--- 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.
-auto 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 06dfd2c5e67657df196dda52ac94c0fcd9aa4120..dfd96656205e4ae78fc81f33d65596c032509da1 100644 (file)
--- 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.
-auto 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 1305cf6ce697abbedd06b26ab36547c0c028676c..f703d7b6ba6c3e13099102ec6fa6d852cdcb29b3 100644 (file)
--- 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.
-auto 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 965637bc7f8e67e5afc257ae5ee4992a8c3cc3d3..d8180ca64c32b13a19d155eefe9112601a180986 100644 (file)
--- 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.
-auto 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 19b676eca5eb93297ab49e943195426d36d4e1ce..d2d0d3305ee7b09099836b7dc9aa29402a7ed1f6 100644 (file)
--- 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.
-auto 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 3c25c6ffe16decf017a6fe3a14bf9eaf70f8d21e..6ee5d33c5538dbb0130e67eac25c6cf7fcc247c3 100644 (file)
--- 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.
-auto 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 5b583615e33045c3e639f5d07344ef0137d80dec..4e083dea9edd95f2d15c759c7ab6633afcae4ae3 100644 (file)
--- 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.
-auto 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 e637e7d4ae1d4ff7861b9bb172602024417d8053..0145a313e9ce45ec47d93689af586fb30ba3bd62 100644 (file)
--- 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.
-auto 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 6f271dd691935c2a4d4e0cf753a978f6ca380fd7..4f4e2bea1150ab554ca4faac99c0ad2f46acb029 100644 (file)
--- 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.
-auto 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 77eef1f7348b6656130b56cda1704d5ca09e8ea0..811ae06bcf0b1c95b88ca9d86f1f1c4e41eb3cf9 100644 (file)
--- 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.
-auto 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 c2656bf79a7bfbb19129c66e31d9d599d11d6feb..936eedbaa22130ff2f7a62707376a7f5a063ce53 100644 (file)
--- 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.
-auto 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 6bf34a8065f4b8bfb9089ac5472cde1d9f364f7f..5f5960ed6530ac0da48fb49e719bc62d83ba2643 100644 (file)
--- 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.
-auto 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 15eeca8092690919c8f7358f2de7b7e586f2ddb5..389785f55b9bc36056a5e327dc0bb9d1f5f6d96a 100644 (file)
--- 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.
-auto 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 ee30724b27669acce4d0eeed05f82fd08eef7806..2f656b223e38a8d7ee8b6c8ef230d92f6a838c1a 100644 (file)
--- 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.
-auto 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 413d5d0d0ae2111e71b2b4cd4e661cd9a3831f7f..619a0f5bba45a9613322910e2ea806758817ec4f 100644 (file)
--- 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.
-auto 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 c9075f2e3d960abb7cd093f1e51f1b9c047cd6c7..789549d1ceff5eb49dafede47b78616242476de9 100644 (file)
--- 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.
-auto 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 ba2e724eb7f4d59f21fc50ed45360a38dfa2de50..b5548d960ccbee5befeae577895a2ec13e11dd13 100644 (file)
--- 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.
-auto 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 548df9d84689b87a07c2141a8b6aa95817c48219..801451c4332c97508d0ffcd0f39f380f562e9993 100644 (file)
--- 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.
-auto 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 570d2372434417a723d37f31646cbc0159160bc0..61d6cef0429f814f2791def4f22947bac8efa2db 100644 (file)
--- 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.
-auto 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 05e4b3cfdf3710308a0b8e99cc797af948a5abaf..c7af583bd8e7957e37ae4df2fb3394e5f6047227 100644 (file)
--- 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.
-auto 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 ea3be43e0cc565d3fdbca082377979461c2d09a8..9982a8eab832137c907583f0ff0814d451a318f9 100644 (file)
--- 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.
-auto 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 e2a7df88456b79ca4a2f9b9199c5ac54f35981ff..f998f72e92809091ceb9f1391bb87a0bf53d9e45 100644 (file)
--- 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.
-auto 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 1bc6a7ee45f8a4a2288e57189932f4029c3c25b3..9515feec6f45bae1cf3c41eb84ebd35c937050b2 100644 (file)
--- 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.
-auto 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 8c38afbd9455d75efdef35a71c5719f252018ca2..ef68697fe81bf8ffd739af13e88738eb3e54860b 100644 (file)
--- 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.
-auto 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 766232ffd23b405013ec932446e4da0d0395203a..534c7fb7e58f35103fee19c3bb08d2ff973fd5ea 100644 (file)
--- 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.
-auto 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 f71b12e5795ebb3f6099d2d16c6db33ccb65e528..2fce65768ef1a4c4ae63e53cacdf145ab04ee9b7 100644 (file)
--- 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.
-auto 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 919437549e3b8f26c108e2a1f1182f7b4ae5cbb7..934852d6e823158b83c04e888c2e2bf578c5de9a 100644 (file)
--- 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.
-auto 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 e69046020a357bc7cbd52363dbd596776d10151d..f13905176908ca35b1b84d380772dfef8de6d3d1 100644 (file)
--- 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.
-auto 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 4ed8eaa55416a09cb3200d6d62354ca4b5265e63..48138a19a4214fe4efa9c74cd315e2bbce5ccc42 100644 (file)
--- 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.
-auto 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 4e85774004fa4d46f5decdb2fafc7b5908cdd45e..96e607cea1befd994dfa4ff682c67a800ea29842 100644 (file)
--- 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.
-auto 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 072bd65e8b4715ceca8176643ea1dc77d513b6c4..1534861ebfdb9db73a92f70571a73543ad680470 100644 (file)
--- 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.
-auto 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 cf69fbdd75cbb4e9186eb4a70b54fae0badfc764..c05658d20d7a83bcb56bff25cc89778edd540e12 100644 (file)
--- 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.
-auto 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 6d42028e093254c710cac425c7c1ef4cb2a9fc72..a134410a2e4a92c7808f7a1e0d8b207e2ede5209 100644 (file)
--- 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.
-auto 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 45c5189c7af88c3e0e7b232b8eda7e70d476d8f3..e70a70c3bc0e0f97074a3b6984cd2bb6c03bd266 100644 (file)
--- 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.
-auto 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 87a148225062a6a710b472ca5a62c189c076fc08..3919360134358eb64da826bbaddb517f55c7305b 100644 (file)
--- 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.
-auto 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 c4c03e265cfe993bb444377ae746c4dd0a05ece6..4c0c98507b8d77d67f93de008738d3f8a9595809 100644 (file)
--- 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.
-auto 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 bf43acb8306c26d9bed162251fe2549ba9d67f1f..71ed352dd6bc4d209d89cf2ed12bce8647411fc1 100644 (file)
--- 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.
-auto 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 83f8399f9e4ebd11090c75600fa59bda4bae3785..c01872fb9b5b311518d2e314dcc0041026d7f81d 100644 (file)
--- 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.
-auto 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 d4cd09aedd1d6623209cf006bb4c8c149cb77e51..e336e3a3a58031c2f64f7742334660bf942e51b6 100644 (file)
--- 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.
-auto 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 22f1826a9d5840d1524007eb791c436ffa2f565d..ed138bd52de7f2fa39d75f9a3d1b5863ccf476e6 100644 (file)
--- 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.
-auto 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 6e86e46db308d02a906c4747714c49190dfd6c1b..57fb55ec71b1699cec89372eb5486a6f471d92c8 100644 (file)
--- 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.
-auto 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 1b7c4e2853345c3b93d0f884b6a468b45f0e55b8..a84605051ca7819dbb30bdec5d0b698e4655a86f 100644 (file)
--- 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.
-auto 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 e5c9a4810d8cdf817c3d24db7f2af6772bafd2c1..051af57e853fe500be7000f8c047c7e8d8e05c6a 100644 (file)
--- 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.
-auto 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 c82d5ad140c26c731b5c818f426380a90dcbda6c..11d43b6a2bb112b4842705ecae83bb14b05c2e9d 100644 (file)
--- 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.
-auto 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 a5656dbb8268212c2e8da2abeac629c3aefec831..e981ee5ba591fab1776750e5e12e555f1e455230 100644 (file)
--- 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.
-auto 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 90502489c992720d46b8bc903179f52ab4f2ba60..26341ce46275bc22b9ed069e9540e0d9f707e910 100644 (file)
--- 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.
-auto 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 249f09a22f8b6cc53c815acc3b1d5665457801b6..fcf4367135a9c035b74bfa28340d4be475cd88e9 100644 (file)
--- 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.
-auto 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 e14e0768e5da91d26cd0bf32f8363939bf6b90da..8397d426f5b7e7d3389943389ea96491748609cc 100644 (file)
--- 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.
-auto 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 2cc1a75360b5c182f2c567f775118f45099e403b..01e94c6a7426358985969b3e66482c9cccedc779 100644 (file)
--- 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.
-auto 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 6a77615a3f3aa20a1755a7a1ddaac2abad5ea516..3785a9204f832cd5eea848e4f85a6c6dd9c01186 100644 (file)
--- 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.
-auto 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 7b76445f470f83a5ab69426563d1324ccc2101ad..135db3ff2e84de52f111fa7efb3d1120dd4348bf 100644 (file)
--- 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.
-auto 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 9373a9beda203bd0b5c9ad864c524cf7c7b361b5..883467d612c5502ca568b9db7671d7499d67e63d 100644 (file)
--- 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.
-auto 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 d4571bf7f58cd9ddba8bbb5efdda4d8c4a6a62bb..90f1c10c9b42ac455bd5545379a98d232cdb6c0b 100644 (file)
--- 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.
-auto 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 34f8df65a12ab118c387996bf192f86b694aa89a..7658986681a86f9ddfb82531c54a6e6223656c7e 100644 (file)
--- 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.
-auto 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 e8091c2ab9e09065968fd48e0be5a097d15ed71b..fe79d15506511fd9cbdac8556fae56d07c2b5d8c 100644 (file)
--- 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.
-auto 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 6fac0285c98f783de5338283a6a14e5ff0f36be4..9868ec4d5dd564ce4406cfcf8a4473614b835be1 100644 (file)
--- 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:
-auto 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 0fcc15b76486d65898593527e56bea675c6c21b0..1dc7202c9f28e5339a212ceb8199a4b578d227f9 100644 (file)
--- 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.
-auto paramodulation timeout=100.
+autobatch paramodulation timeout=100.
 try assumption.
 print proofterm.
 qed.